CONTRACTS: remove mentions of DSL-style contracts

Author: Remi Delmas

src/goto-instrument/Makefile

@@ -23,9 +23,9 @@ SRC = accelerate/accelerate.cpp \
       contracts/dynamic-frames/dfcc_is_freeable.cpp \
       contracts/dynamic-frames/dfcc_instrument.cpp \
       contracts/dynamic-frames/dfcc_spec_functions.cpp \
-      contracts/dynamic-frames/dfcc_dsl_contract_functions.cpp \
-      contracts/dynamic-frames/dfcc_dsl_wrapper_program.cpp \
-      contracts/dynamic-frames/dfcc_dsl_contract_handler.cpp \
+      contracts/dynamic-frames/dfcc_contract_functions.cpp \
+      contracts/dynamic-frames/dfcc_wrapper_program.cpp \
+      contracts/dynamic-frames/dfcc_contract_handler.cpp \
       contracts/dynamic-frames/dfcc_swap_and_wrap.cpp \
       contracts/dynamic-frames/dfcc.cpp \
       contracts/havoc_assigns_clause_targets.cpp \

src/goto-instrument/contracts/doc/developer/contracts-dev-arch.md

@@ -30,10 +30,10 @@ Each of these translation passes is implemented in a specific class:
  @ref dfcc_is_fresht             | Implements @ref contracts-dev-spec-is-fresh
  @ref dfcc_is_freeablet          | Implements @ref contracts-dev-spec-is-freeable
  @ref dfcc_spec_functionst       | Implements @ref contracts-dev-spec-spec-rewriting
- @ref dfcc_dsl_wrapper_programt  | Implements @ref contracts-dev-spec-contract-checking for DSL-style contracts
- ^                               | Implements @ref contracts-dev-spec-contract-replacement for DSL-style contracts
- @ref dfcc_dsl_contract_handlert | Implements @ref contracts-dev-spec-codegen for DSL-style contracts
- ^                               | Implements the interface @ref dfcc_contract_handlert for DSL-style contract by delegating operations to @ref dfcc_dsl_wrapper_programt
+ @ref dfcc_wrapper_programt  | Implements @ref contracts-dev-spec-contract-checking for contracts
+ ^                               | Implements @ref contracts-dev-spec-contract-replacement for contracts
+ @ref dfcc_contract_handlert | Implements @ref contracts-dev-spec-codegen for contracts
+ ^                               | Implements the interface @ref dfcc_contract_handlert for contract by delegating operations to @ref dfcc_wrapper_programt
  @ref dfcc_swap_and_wrapt        | Implements @ref contracts-dev-spec-contract-checking by delegating basic operations to @ref dfcc_contract_handlert
  ^                               | Implements @ref contracts-dev-spec-contract-replacement by delegating basic operations to @ref dfcc_contract_handlert
  ^                               | Implements @ref contracts-dev-spec-contract-checking-rec by delegating basic operations to @ref dfcc_contract_handlert

src/goto-instrument/contracts/dynamic-frames/dfcc.cpp

@@ -125,7 +125,7 @@ dfcct::dfcct(
     ns(goto_model.symbol_table),
     instrument(goto_model, message_handler, utils, library),
     spec_functions(goto_model, message_handler, utils, library, instrument),
-    dsl_contract_handler(
+    contract_handler(
       goto_model,
       message_handler,
       utils,
@@ -139,7 +139,7 @@ dfcct::dfcct(
       library,
       instrument,
       spec_functions,
-      dsl_contract_handler),
+      contract_handler),
     max_assigns_clause_size(0)
 {
   transform_goto_model();
@@ -162,7 +162,7 @@ void dfcct::check_transform_goto_model_preconditions()
         "' either not found or has no body");
 
     // triggers signature compatibility checking
-    dsl_contract_handler.get_pure_contract_symbol(pair.second);
+    contract_handler.get_pure_contract_symbol(pair.second);
 
     PRECONDITION_WITH_DIAGNOSTICS(
       pair.first != harness_id,
@@ -194,7 +194,7 @@ void dfcct::check_transform_goto_model_preconditions()
       "Function to replace '" + id2string(pair.first) + "' not found");
 
     // triggers signature compatibility checking
-    dsl_contract_handler.get_pure_contract_symbol(pair.second);
+    contract_handler.get_pure_contract_symbol(pair.second);
 
     PRECONDITION_WITH_DIAGNOSTICS(
       pair.first != harness_id,
@@ -288,7 +288,7 @@ void dfcct::wrap_checked_function()
 
     // upate max contract size
     const std::size_t assigns_clause_size =
-      dsl_contract_handler.get_assigns_clause_size(contract_id);
+      contract_handler.get_assigns_clause_size(contract_id);
     if(assigns_clause_size > max_assigns_clause_size)
       max_assigns_clause_size = assigns_clause_size;
   }
@@ -358,7 +358,7 @@ void dfcct::wrap_discovered_function_pointer_contracts()
         "Function pointer contract '" + str + "' not found.");
 
       // triggers signature compatibility checking
-      dsl_contract_handler.get_pure_contract_symbol(str);
+      contract_handler.get_pure_contract_symbol(str);
 
       log.status() << "Wrapping function pointer contract '" << fp_contract
                    << "' with itself in REPLACE mode" << messaget::eom;

src/goto-instrument/contracts/dynamic-frames/dfcc.h

@@ -17,9 +17,6 @@ Author: Remi Delmas, delmasrd@amazon.com
 /// \brief Main class orchestrating the the whole program transformation
 /// for function contracts with Dynamic Frame Condition Checking (DFCC)
 ///
-/// Contracts must be expressed in DSL-style, i.e. as contract clauses attached
-/// to the function declaration at the C level.
-///
 /// All functions of the model are extended with a ghost parameter representing
 /// a dynamic frame and all their assignments are instrumented and checked
 /// against the dynamic frame parameter.
@@ -36,7 +33,6 @@ Author: Remi Delmas, delmasrd@amazon.com
 #include <util/message.h>
 
 #include "dfcc_contract_handler.h"
-#include "dfcc_dsl_contract_handler.h"
 #include "dfcc_instrument.h"
 #include "dfcc_library.h"
 #include "dfcc_spec_functions.h"
@@ -203,7 +199,7 @@ class dfcct
   namespacet ns;
   dfcc_instrumentt instrument;
   dfcc_spec_functionst spec_functions;
-  dfcc_dsl_contract_handlert dsl_contract_handler;
+  dfcc_contract_handlert contract_handler;
   dfcc_swap_and_wrapt swap_and_wrap;
 
   /// Maps wrapper function to the wrapped function.

src/goto-instrument/contracts/dynamic-frames/dfcc_dsl_contract_functions.cpp renamed to src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.cpp

@@ -6,7 +6,7 @@ Author: Remi Delmas, delmasrd@amazon.com
 Date: August 2022
 
 \*******************************************************************/
-#include "dfcc_dsl_contract_functions.h"
+#include "dfcc_contract_functions.h"
 
 #include <util/expr_util.h>
 #include <util/fresh_symbol.h>
@@ -26,7 +26,7 @@ Date: August 2022
 #include "dfcc_spec_functions.h"
 #include "dfcc_utils.h"
 
-dfcc_dsl_contract_functionst::dfcc_dsl_contract_functionst(
+dfcc_contract_functionst::dfcc_contract_functionst(
   const symbolt &pure_contract_symbol,
   goto_modelt &goto_model,
   message_handlert &message_handler,
@@ -66,34 +66,33 @@ dfcc_dsl_contract_functionst::dfcc_dsl_contract_functionst(
 }
 
 const symbolt &
-dfcc_dsl_contract_functionst::get_spec_assigns_function_symbol() const
+dfcc_contract_functionst::get_spec_assigns_function_symbol() const
 {
   return ns.lookup(spec_assigns_function_id);
 }
 
 const symbolt &
-dfcc_dsl_contract_functionst::get_spec_assigns_havoc_function_symbol() const
+dfcc_contract_functionst::get_spec_assigns_havoc_function_symbol() const
 {
   return ns.lookup(spec_assigns_havoc_function_id);
 }
 
-const symbolt &
-dfcc_dsl_contract_functionst::get_spec_frees_function_symbol() const
+const symbolt &dfcc_contract_functionst::get_spec_frees_function_symbol() const
 {
   return ns.lookup(spec_frees_function_id);
 }
 
-const std::size_t dfcc_dsl_contract_functionst::get_nof_assigns_targets() const
+const std::size_t dfcc_contract_functionst::get_nof_assigns_targets() const
 {
   return nof_assigns_targets;
 }
 
-const std::size_t dfcc_dsl_contract_functionst::get_nof_frees_targets() const
+const std::size_t dfcc_contract_functionst::get_nof_frees_targets() const
 {
   return nof_frees_targets;
 }
 
-void dfcc_dsl_contract_functionst::gen_spec_assigns_function()
+void dfcc_contract_functionst::gen_spec_assigns_function()
 {
   const auto &spec_function_symbol = utils.clone_and_rename_function(
     pure_contract_symbol.name, spec_assigns_function_id, empty_typet());
@@ -151,7 +150,7 @@ void dfcc_dsl_contract_functionst::gen_spec_assigns_function()
   goto_model.goto_functions.update();
 }
 
-void dfcc_dsl_contract_functionst::encode_assignable_target_group(
+void dfcc_contract_functionst::encode_assignable_target_group(
   const conditional_target_group_exprt &group,
   goto_programt &dest)
 {
@@ -174,7 +173,7 @@ void dfcc_dsl_contract_functionst::encode_assignable_target_group(
   goto_instruction->complete_goto(label_instruction);
 }
 
-void dfcc_dsl_contract_functionst::encode_assignable_target(
+void dfcc_contract_functionst::encode_assignable_target(
   const exprt &target,
   goto_programt &dest)
 {
@@ -236,7 +235,7 @@ void dfcc_dsl_contract_functionst::encode_assignable_target(
   }
 }
 
-void dfcc_dsl_contract_functionst::gen_spec_frees_function()
+void dfcc_contract_functionst::gen_spec_frees_function()
 {
   // fetch pure contract symbol
   const auto &code_with_contract =
@@ -300,7 +299,7 @@ void dfcc_dsl_contract_functionst::gen_spec_frees_function()
   goto_model.goto_functions.update();
 }
 
-void dfcc_dsl_contract_functionst::inline_and_check_warnings(
+void dfcc_contract_functionst::inline_and_check_warnings(
   const irep_idt &function_id)
 {
   std::set<irep_idt> no_body;
@@ -341,7 +340,7 @@ void dfcc_dsl_contract_functionst::inline_and_check_warnings(
     "not enough arguments when inlining '" + id2string(function_id) + "'");
 }
 
-void dfcc_dsl_contract_functionst::encode_freeable_target_group(
+void dfcc_contract_functionst::encode_freeable_target_group(
   const conditional_target_group_exprt &group,
   goto_programt &dest)
 {
@@ -364,7 +363,7 @@ void dfcc_dsl_contract_functionst::encode_freeable_target_group(
   goto_instruction->complete_goto(label_instruction);
 }
 
-void dfcc_dsl_contract_functionst::encode_freeable_target(
+void dfcc_contract_functionst::encode_freeable_target(
   const exprt &target,
   goto_programt &dest)
 {

src/goto-instrument/contracts/dynamic-frames/dfcc_dsl_contract_functions.h renamed to src/goto-instrument/contracts/dynamic-frames/dfcc_contract_functions.h

@@ -11,8 +11,8 @@ Date: August 2022
 /// Translates assigns and frees clauses of a function contract into goto
 /// functions that allow to build and havoc write sets dynamically.
 
-#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_DSL_CONTRACT_FUNCTIONS_H
-#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_DSL_CONTRACT_FUNCTIONS_H
+#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CONTRACT_FUNCTIONS_H
+#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CONTRACT_FUNCTIONS_H
 
 #include <goto-programs/goto_convert_class.h>
 
@@ -59,7 +59,7 @@ class function_pointer_obeys_contract_exprt;
 ///     write_set_to_fill,
 ///     write_set_to_check);
 /// ```
-class dfcc_dsl_contract_functionst
+class dfcc_contract_functionst
 {
 public:
   /// \param pure_contract_symbol the contract to generate code from
@@ -69,7 +69,7 @@ class dfcc_dsl_contract_functionst
   /// \param library the contracts instrumentation library
   /// \param spec_functions provides translation methods for assignable set
   /// or freeable set specification functions.
-  dfcc_dsl_contract_functionst(
+  dfcc_contract_functionst(
     const symbolt &pure_contract_symbol,
     goto_modelt &goto_model,
     message_handlert &message_handler,

src/goto-instrument/contracts/dynamic-frames/dfcc_dsl_contract_handler.cpp renamed to src/goto-instrument/contracts/dynamic-frames/dfcc_contract_handler.cpp

@@ -7,7 +7,7 @@ Date: August 2022
 
 \*******************************************************************/
 
-#include "dfcc_dsl_contract_handler.h"
+#include "dfcc_contract_handler.h"
 
 #include <util/arith_tools.h>
 #include <util/c_types.h>
@@ -29,16 +29,16 @@ Date: August 2022
 #include <goto-instrument/contracts/utils.h>
 #include <langapi/language_util.h>
 
-#include "dfcc_dsl_wrapper_program.h"
 #include "dfcc_instrument.h"
 #include "dfcc_library.h"
 #include "dfcc_spec_functions.h"
 #include "dfcc_utils.h"
+#include "dfcc_wrapper_program.h"
 
-std::map<irep_idt, dfcc_dsl_contract_functionst>
-  dfcc_dsl_contract_handlert::contract_cache;
+std::map<irep_idt, dfcc_contract_functionst>
+  dfcc_contract_handlert::contract_cache;
 
-dfcc_dsl_contract_handlert::dfcc_dsl_contract_handlert(
+dfcc_contract_handlert::dfcc_contract_handlert(
   goto_modelt &goto_model,
   message_handlert &message_handler,
   dfcc_utilst &utils,
@@ -56,20 +56,20 @@ dfcc_dsl_contract_handlert::dfcc_dsl_contract_handlert(
 {
 }
 
-const dfcc_dsl_contract_functionst &
-dfcc_dsl_contract_handlert::get_contract_functions(const irep_idt &contract_id)
+const dfcc_contract_functionst &
+dfcc_contract_handlert::get_contract_functions(const irep_idt &contract_id)
 {
-  auto iter = dfcc_dsl_contract_handlert::contract_cache.find(contract_id);
+  auto iter = dfcc_contract_handlert::contract_cache.find(contract_id);
 
   // return existing value
-  if(iter != dfcc_dsl_contract_handlert::contract_cache.end())
+  if(iter != dfcc_contract_handlert::contract_cache.end())
     return iter->second;
 
   // insert new value
-  return dfcc_dsl_contract_handlert::contract_cache
+  return dfcc_contract_handlert::contract_cache
     .insert(
       {contract_id,
-       dfcc_dsl_contract_functionst(
+       dfcc_contract_functionst(
          get_pure_contract_symbol(contract_id),
          goto_model,
          message_handler,
@@ -80,12 +80,12 @@ dfcc_dsl_contract_handlert::get_contract_functions(const irep_idt &contract_id)
 }
 
 const std::size_t
-dfcc_dsl_contract_handlert::get_assigns_clause_size(const irep_idt &contract_id)
+dfcc_contract_handlert::get_assigns_clause_size(const irep_idt &contract_id)
 {
   return get_contract_functions(contract_id).get_nof_assigns_targets();
 }
 
-void dfcc_dsl_contract_handlert::add_contract_instructions(
+void dfcc_contract_handlert::add_contract_instructions(
   const dfcc_contract_modet contract_mode,
   const irep_idt &wrapper_id,
   const irep_idt &wrapped_id,
@@ -94,7 +94,7 @@ void dfcc_dsl_contract_handlert::add_contract_instructions(
   goto_programt &dest,
   std::set<irep_idt> &function_pointer_contracts)
 {
-  dfcc_dsl_wrapper_programt(
+  dfcc_wrapper_programt(
     contract_mode,
     utils.get_function_symbol(wrapper_id),
     utils.get_function_symbol(wrapped_id),
@@ -108,8 +108,8 @@ void dfcc_dsl_contract_handlert::add_contract_instructions(
     .add_to_dest(dest, function_pointer_contracts);
 }
 
-const symbolt &dfcc_dsl_contract_handlert::get_pure_contract_symbol(
-  const irep_idt &contract_id)
+const symbolt &
+dfcc_contract_handlert::get_pure_contract_symbol(const irep_idt &contract_id)
 {
   const auto &contract_symbol = utils.get_function_symbol(contract_id);
   auto pure_contract_id = "contract::" + id2string(contract_id);
@@ -149,7 +149,7 @@ const symbolt &dfcc_dsl_contract_handlert::get_pure_contract_symbol(
   }
 }
 
-void dfcc_dsl_contract_handlert::check_signature_compat(
+void dfcc_contract_handlert::check_signature_compat(
   const irep_idt &contract_id,
   const code_typet &contract_type,
   const irep_idt &pure_contract_id,
@@ -162,7 +162,7 @@ void dfcc_dsl_contract_handlert::check_signature_compat(
   if(!compatible)
   {
     std::ostringstream err_msg;
-    err_msg << "dfcc_dsl_contract_handlert: function '" << contract_id
+    err_msg << "dfcc_contract_handlert: function '" << contract_id
             << "' and the corresponding pure contract symbol '"
             << pure_contract_id << "' have incompatible type signatures:\n";