CONTRACTS: avoid circular dependency between classes

Do not instrument code in `dfcc_spec_functionst` but
rather one layer above in `dfcc_contract_functionst`.
This allows to avoid creating a circular depedency on
`dfcc_instrumentt` later.

Author: Remi Delmas

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

@@ -23,6 +23,7 @@ Date: August 2022
 #include <langapi/language_util.h>
 
 #include "dfcc_contract_clauses_codegen.h"
+#include "dfcc_instrument.h"
 #include "dfcc_library.h"
 #include "dfcc_spec_functions.h"
 #include "dfcc_utils.h"
@@ -34,7 +35,8 @@ dfcc_contract_functionst::dfcc_contract_functionst(
   dfcc_utilst &utils,
   dfcc_libraryt &library,
   dfcc_spec_functionst &spec_functions,
-  dfcc_contract_clauses_codegent &contract_clauses_codegen)
+  dfcc_contract_clauses_codegent &contract_clauses_codegen,
+  dfcc_instrumentt &instrument)
   : pure_contract_symbol(pure_contract_symbol),
     code_with_contract(to_code_with_contract_type(pure_contract_symbol.type)),
     spec_assigns_function_id(
@@ -50,6 +52,7 @@ dfcc_contract_functionst::dfcc_contract_functionst(
     library(library),
     spec_functions(spec_functions),
     contract_clauses_codegen(contract_clauses_codegen),
+    instrument(instrument),
     ns(goto_model.symbol_table)
 {
   gen_spec_assigns_function();
@@ -66,6 +69,28 @@ dfcc_contract_functionst::dfcc_contract_functionst(
 
   spec_functions.to_spec_frees_function(
     spec_frees_function_id, nof_frees_targets);
+
+  instrument_without_loop_contracts_check_no_pointer_contracts(
+    spec_assigns_function_id);
+
+  instrument_without_loop_contracts_check_no_pointer_contracts(
+    spec_frees_function_id);
+}
+
+void dfcc_contract_functionst::
+  instrument_without_loop_contracts_check_no_pointer_contracts(
+    const irep_idt &spec_function_id)
+{
+  std::set<irep_idt> function_pointer_contracts;
+  instrument.instrument_function(
+    spec_function_id,
+    dfcc_loop_contract_modet::NONE,
+    function_pointer_contracts);
+
+  INVARIANT(
+    function_pointer_contracts.empty(),
+    id2string(spec_function_id) + " shall not contain calls to " CPROVER_PREFIX
+                                  "obeys_contract");
 }
 
 const symbolt &

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

@@ -29,31 +29,34 @@ class goto_modelt;
 class message_handlert;
 class dfcc_libraryt;
 class dfcc_utilst;
+class dfcc_instrumentt;
 class dfcc_spec_functionst;
 class dfcc_contract_clauses_codegent;
 class code_with_contract_typet;
 class conditional_target_group_exprt;
 
 /// Generates GOTO functions modelling a contract assigns and frees clauses.
 ///
-/// The generated functions are the following.
+/// The generated functions are the following:
 ///
-/// Populates write_set_to_fill with targets of the assigns clause
-/// checks its own body against write_set_to_check:
 /// ```c
+/// // Populates write_set_to_fill with targets of the assigns clause
+/// // checks its own body against write_set_to_check:
 /// void contract_id::assigns(
 ///     function-params,
 ///     write_set_to_fill,
 ///     write_set_to_check);
 /// ```
-/// Havocs the targets specified in the assigns clause, assuming
-/// write_set_to_havoc is a snapshot created using contract_id::assigns:
+///
 /// ```c
+/// // Havocs the targets specified in the assigns clause, assuming
+/// // write_set_to_havoc is a snapshot created using contract_id::assigns
 /// void contract_id::assigns::havoc(write_set_to_havoc);
 /// ```
-/// Populates write_set_to_fill with targets of the frees clause
-/// checks its own body against write_set_to_check:
+///
 /// ```c
+/// // Populates write_set_to_fill with targets of the frees clause
+/// // checks its own body against write_set_to_check:
 /// void contract_id::frees(
 ///     function-params,
 ///     write_set_to_fill,
@@ -70,14 +73,21 @@ class dfcc_contract_functionst
   /// \param spec_functions provides translation methods for assignable set
   /// \param contract_clauses_codegen provides GOTO code generation methods
   /// for assigns and free clauses.
+  /// \param instrument Used to instrument generated functions for side effects
   dfcc_contract_functionst(
     const symbolt &pure_contract_symbol,
     goto_modelt &goto_model,
     message_handlert &message_handler,
     dfcc_utilst &utils,
     dfcc_libraryt &library,
     dfcc_spec_functionst &spec_functions,
-    dfcc_contract_clauses_codegent &contract_clauses_codegen);
+    dfcc_contract_clauses_codegent &contract_clauses_codegen,
+    dfcc_instrumentt &instrument);
+
+  /// Instruments the given function without loop contracts and checks that no
+  /// function pointer contracts were discovered.
+  void instrument_without_loop_contracts_check_no_pointer_contracts(
+    const irep_idt &spec_function_id);
 
   /// Returns the contract::assigns function symbol
   const symbolt &get_spec_assigns_function_symbol() const;
@@ -120,6 +130,7 @@ class dfcc_contract_functionst
   dfcc_libraryt &library;
   dfcc_spec_functionst &spec_functions;
   dfcc_contract_clauses_codegent &contract_clauses_codegen;
+  dfcc_instrumentt &instrument;
   namespacet ns;
   std::size_t nof_assigns_targets;
   std::size_t nof_frees_targets;

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

@@ -17,20 +17,19 @@ Author: Remi Delmas, [email protected]
 #include <langapi/language_util.h>
 
 #include "dfcc_library.h"
+#include "dfcc_loop_contract_mode.h"
 #include "dfcc_utils.h"
 
 dfcc_spec_functionst::dfcc_spec_functionst(
   goto_modelt &goto_model,
   message_handlert &message_handler,
   dfcc_utilst &utils,
-  dfcc_libraryt &library,
-  dfcc_instrumentt &instrument)
+  dfcc_libraryt &library)
   : goto_model(goto_model),
     message_handler(message_handler),
     log(message_handler),
     utils(utils),
     library(library),
-    instrument(instrument),
     ns(goto_model.symbol_table)
 {
 }
@@ -111,6 +110,8 @@ void dfcc_spec_functionst::generate_havoc_function(
     havoc_program,
     nof_targets);
 
+  havoc_program.add(goto_programt::make_end_function());
+
   goto_model.goto_functions.update();
 
   std::set<irep_idt> no_body;
@@ -246,7 +247,6 @@ void dfcc_spec_functionst::generate_havoc_instructions(
     }
   }
   nof_targets = next_idx;
-  havoc_program.add(goto_programt::make_end_function());
 }
 
 void dfcc_spec_functionst::to_spec_assigns_function(
@@ -272,13 +272,6 @@ void dfcc_spec_functionst::to_spec_assigns_function(
 
   goto_model.goto_functions.update();
 
-  // instrument for side-effects checking
-  std::set<irep_idt> function_pointer_contracts;
-  instrument.instrument_function(function_id, function_pointer_contracts);
-  INVARIANT(
-    function_pointer_contracts.empty(),
-    "discovered function pointer contracts unexpectedly");
-
   goto_model.goto_functions.function_map.at(function_id).make_hidden();
 }
 
@@ -362,13 +355,6 @@ void dfcc_spec_functionst::to_spec_frees_function(
 
   goto_model.goto_functions.update();
 
-  // instrument for side-effects checking
-  std::set<irep_idt> function_pointer_contracts;
-  instrument.instrument_function(function_id, function_pointer_contracts);
-  INVARIANT(
-    function_pointer_contracts.empty(),
-    "discovered function pointer contracts unexpectedly");
-
   goto_model.goto_functions.function_map.at(function_id).make_hidden();
 }
 

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

@@ -21,7 +21,6 @@ Author: Remi Delmas, [email protected]
 #include <util/std_expr.h>
 #include <util/std_types.h>
 
-#include "dfcc_instrument.h"
 #include "dfcc_library.h"
 #include "dfcc_utils.h"
 
@@ -32,28 +31,23 @@ class goto_modelt;
 class message_handlert;
 class symbolt;
 class conditional_target_group_exprt;
-class cfg_infot;
 
-/// This class transforms (in place) declarative assigns clause and frees clause
-/// specification functions expressed in terms of the builtins:
+/// This class rewrites GOTO functions that use the built-ins:
 /// - `__CPROVER_assignable`,
 /// - `__CPROVER_object_whole`,
 /// - `__CRPOVER_object_from`,
 /// - `__CPROVER_object_upto`,
 /// - `__CPROVER_freeable`
-/// into active functions by transforming the builtin calls into calls to
-/// dfcc library functions that actually built frame descriptions.
-/// The resulting function is then itself instrumented for frame condition
-/// checking to be able to prove the absence of side effects.
+/// into GOTO functions that populate a write set instance or havoc a write set
+/// by calling the library implementation of these built-ins.
 class dfcc_spec_functionst
 {
 public:
   dfcc_spec_functionst(
     goto_modelt &goto_model,
     message_handlert &message_handler,
     dfcc_utilst &utils,
-    dfcc_libraryt &library,
-    dfcc_instrumentt &instrument);
+    dfcc_libraryt &library);
 
   /// From a function:
   ///
@@ -122,13 +116,11 @@ class dfcc_spec_functionst
   /// void function_id(
   ///   params,
   ///   __CPROVER_assignable_set_t write_set_to_fill,
-  ///   __CPROVER_assignable_set_t write_set_to_check
   /// )
   /// ```
   ///
   /// Where:
   /// - `write_set_to_fill` is the write set to populate.
-  /// - `write_set_to_check` is the write set to use for checking side effects.
   ///
   /// \param function_id function to transform in place
   /// \param nof_targets receives the estimated size of the write set
@@ -174,13 +166,11 @@ class dfcc_spec_functionst
   /// void function_id(
   ///   params,
   ///   __CPROVER_assignable_set_t write_set_to_fill,
-  ///   __CPROVER_assignable_set_t write_set_to_check
   /// )
   /// ```
   ///
   /// Where:
   /// - `write_set_to_fill` is the write set to populate.
-  /// - `write_set_to_check` is the write set to use for checking side effects.
   ///
   /// The function must be fully inlined and loop free.
   ///
@@ -219,7 +209,6 @@ class dfcc_spec_functionst
   messaget log;
   dfcc_utilst &utils;
   dfcc_libraryt &library;
-  dfcc_instrumentt &instrument;
   namespacet ns;
 
   /// Extracts the type of an assigns clause target expression