CONTRACTS: add loop contracts support in DFCC

Author: Remi Delmas

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

@@ -38,7 +38,6 @@ Author: Remi Delmas, delmarsd@amazon.com
 #include <ansi-c/c_object_factory_parameters.h>
 #include <ansi-c/cprover_library.h>
 #include <goto-instrument/contracts/cfg_info.h>
-#include <goto-instrument/contracts/instrument_spec_assigns.h>
 #include <goto-instrument/contracts/utils.h>
 #include <goto-instrument/nondet_static.h>
 #include <langapi/language.h>
@@ -122,6 +121,7 @@ void dfcc(
   const bool allow_recursive_calls,
   const std::set<irep_idt> &to_replace,
   const bool apply_loop_contracts,
+  const bool unwind_transformed_loops,
   const std::set<std::string> &to_exclude_from_nondet_static,
   message_handlert &message_handler)
 {
@@ -138,6 +138,7 @@ void dfcc(
     allow_recursive_calls,
     to_replace_map,
     apply_loop_contracts,
+    unwind_transformed_loops,
     to_exclude_from_nondet_static,
     message_handler);
 }
@@ -150,6 +151,7 @@ void dfcc(
   const bool allow_recursive_calls,
   const std::map<irep_idt, irep_idt> &to_replace,
   const bool apply_loop_contracts,
+  const bool unwind_transformed_loops,
   const std::set<std::string> &to_exclude_from_nondet_static,
   message_handlert &message_handler)
 {
@@ -160,7 +162,8 @@ void dfcc(
     to_check,
     allow_recursive_calls,
     to_replace,
-    apply_loop_contracts,
+    dfcc_loop_contract_mode_from_bools(
+      apply_loop_contracts, unwind_transformed_loops),
     message_handler,
     to_exclude_from_nondet_static};
 }
@@ -172,7 +175,7 @@ dfcct::dfcct(
   const optionalt<std::pair<irep_idt, irep_idt>> &to_check,
   const bool allow_recursive_calls,
   const std::map<irep_idt, irep_idt> &to_replace,
-  const bool apply_loop_contracts,
+  const dfcc_loop_contract_modet loop_contract_mode,
   message_handlert &message_handler,
   const std::set<std::string> &to_exclude_from_nondet_static)
   : options(options),
@@ -181,22 +184,23 @@ dfcct::dfcct(
     to_check(to_check),
     allow_recursive_calls(allow_recursive_calls),
     to_replace(to_replace),
-    apply_loop_contracts(apply_loop_contracts),
+    loop_contract_mode(loop_contract_mode),
     to_exclude_from_nondet_static(to_exclude_from_nondet_static),
     message_handler(message_handler),
     log(message_handler),
     utils(goto_model, message_handler),
     library(goto_model, utils, message_handler),
     ns(goto_model.symbol_table),
-    instrument(goto_model, message_handler, utils, library),
-    memory_predicates(goto_model, utils, library, instrument, message_handler),
-    spec_functions(goto_model, message_handler, utils, library, instrument),
-    contract_clauses_codegen(
+    spec_functions(goto_model, message_handler, utils, library),
+    contract_clauses_codegen(goto_model, message_handler, utils, library),
+    instrument(
       goto_model,
       message_handler,
       utils,
       library,
-      spec_functions),
+      spec_functions,
+      contract_clauses_codegen),
+    memory_predicates(goto_model, utils, library, instrument, message_handler),
     contract_handler(
       goto_model,
       message_handler,
@@ -340,7 +344,7 @@ void dfcct::instrument_harness_function()
                << messaget::eom;
 
   instrument.instrument_harness_function(
-    harness_id, function_pointer_contracts);
+    harness_id, loop_contract_mode, function_pointer_contracts);
 
   other_symbols.erase(harness_id);
 }
@@ -369,6 +373,7 @@ void dfcct::wrap_checked_function()
                  << contract_id << "' in CHECK mode" << messaget::eom;
 
     swap_and_wrap.swap_and_wrap_check(
+      loop_contract_mode,
       wrapper_id,
       contract_id,
       function_pointer_contracts,
@@ -377,7 +382,7 @@ void dfcct::wrap_checked_function()
     if(other_symbols.find(wrapper_id) != other_symbols.end())
       other_symbols.erase(wrapper_id);
 
-    // upate max contract size
+    // update max contract size
     const std::size_t assigns_clause_size =
       contract_handler.get_assigns_clause_size(contract_id);
     if(assigns_clause_size > max_assigns_clause_size)
@@ -485,20 +490,11 @@ void dfcct::instrument_other_functions()
 
     log.status() << "Instrumenting '" << function_id << "'" << messaget::eom;
 
-    instrument.instrument_function(function_id, function_pointer_contracts);
+    instrument.instrument_function(
+      function_id, loop_contract_mode, function_pointer_contracts);
   }
 
   goto_model.goto_functions.update();
-
-  // TODO specialise the library functions for the max size of
-  // loop and function contracts
-  if(to_check.has_value())
-  {
-    log.status() << "Specializing cprover_contracts functions for assigns "
-                    "clauses of at most "
-                 << max_assigns_clause_size << " targets" << messaget::eom;
-    library.specialize(max_assigns_clause_size);
-  }
 }
 
 void dfcct::transform_goto_model()
@@ -511,6 +507,17 @@ void dfcct::transform_goto_model()
   wrap_replaced_functions();
   wrap_discovered_function_pointer_contracts();
   instrument_other_functions();
+
+  // take the max of function of loop contracts assigns clauses
+  auto assigns_clause_size = instrument.get_max_assigns_clause_size();
+  if(assigns_clause_size > max_assigns_clause_size)
+    max_assigns_clause_size = assigns_clause_size;
+
+  log.status() << "Specializing cprover_contracts functions for assigns "
+                  "clauses of at most "
+               << max_assigns_clause_size << " targets" << messaget::eom;
+  library.specialize(max_assigns_clause_size);
+
   library.inhibit_front_end_builtins();
 
   // TODO implement a means to inhibit unreachable functions (possibly via the

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

@@ -38,6 +38,7 @@ Author: Remi Delmas, delmasrd@amazon.com
 #include "dfcc_instrument.h"
 #include "dfcc_library.h"
 #include "dfcc_lift_memory_predicates.h"
+#include "dfcc_loop_contract_mode.h"
 #include "dfcc_spec_functions.h"
 #include "dfcc_swap_and_wrap.h"
 #include "dfcc_utils.h"
@@ -50,17 +51,16 @@ class messaget;
 class message_handlert;
 class symbolt;
 class conditional_target_group_exprt;
-class cfg_infot;
 class optionst;
 
 #define FLAG_DFCC "dfcc"
 #define OPT_DFCC "(" FLAG_DFCC "):"
 
 // clang-format off
 #define HELP_DFCC                                                              \
-  " --dfcc <harness>             activate dynamic frame condition checking\n"\
-  "                              for function contracts using the given\n"\
-  "                              harness as entry point\n"
+  " --dfcc <harness>              activate dynamic frame condition checking\n" \
+  "                               for contracts using the given harness as\n"  \
+  "                               entry point\n"
 
 #define FLAG_ENFORCE_CONTRACT_REC "enforce-contract-rec"
 #define OPT_ENFORCE_CONTRACT_REC "(" FLAG_ENFORCE_CONTRACT_REC "):"
@@ -100,6 +100,8 @@ class invalid_function_contract_pair_exceptiont : public cprover_exception_baset
 /// \param allow_recursive_calls Allow the checked function to be recursive
 /// \param to_replace set of functions to replace with their contract
 /// \param apply_loop_contracts apply loop contract transformations iff true
+/// \param unwind_transformed_loops unwind transformed loops after applying loop
+///                                 contracts.
 /// \param to_exclude_from_nondet_static set of symbols to exclude when havocing
 /// static program symbols.
 /// \param message_handler used for debug/warning/error messages
@@ -111,6 +113,7 @@ void dfcc(
   const bool allow_recursive_calls,
   const std::set<irep_idt> &to_replace,
   const bool apply_loop_contracts,
+  const bool unwind_transformed_loops,
   const std::set<std::string> &to_exclude_from_nondet_static,
   message_handlert &message_handler);
 
@@ -129,7 +132,9 @@ void dfcc(
 /// \param to_check (function,contract) pair for contract checking
 /// \param allow_recursive_calls Allow the checked function to be recursive
 /// \param to_replace Functions-to-contract mapping for replacement
-/// \param apply_loop_contracts Spply loop contract transformations iff true
+/// \param apply_loop_contracts Apply loop contract transformations iff true
+/// \param unwind_transformed_loops unwind transformed loops after applying loop
+///                                 contracts.
 /// \param to_exclude_from_nondet_static Set of symbols to exclude when havocing
 /// static program symbols.
 /// \param message_handler used for debug/warning/error messages
@@ -141,6 +146,7 @@ void dfcc(
   const bool allow_recursive_calls,
   const std::map<irep_idt, irep_idt> &to_replace,
   const bool apply_loop_contracts,
+  const bool unwind_transformed_loops,
   const std::set<std::string> &to_exclude_from_nondet_static,
   message_handlert &message_handler);
 
@@ -157,8 +163,7 @@ class dfcct
   /// \param to_check (function,contract) pair for contract checking
   /// \param allow_recursive_calls Allow the checked function to be recursive
   /// \param to_replace functions-to-contract mapping for replacement
-  /// \param apply_loop_contracts apply loop contract transformations iff true
-  /// havocing static program symbols.
+  /// \param loop_contract_mode mode to use for loop contracts
   /// \param message_handler used for debug/warning/error messages
   /// \param to_exclude_from_nondet_static set of symbols to exclude when
   dfcct(
@@ -168,7 +173,7 @@ class dfcct
     const optionalt<std::pair<irep_idt, irep_idt>> &to_check,
     const bool allow_recursive_calls,
     const std::map<irep_idt, irep_idt> &to_replace,
-    const bool apply_loop_contracts,
+    const dfcc_loop_contract_modet loop_contract_mode,
     message_handlert &message_handler,
     const std::set<std::string> &to_exclude_from_nondet_static);
 
@@ -194,7 +199,7 @@ class dfcct
   ///   (replacement mode)
   /// - instrument all remaining functions GOTO model
   /// - (this includes standard library functions).
-  /// - specialise the instrumentation functions by unwiding loops they contain
+  /// - specialise the instrumentation functions by unwinding loops they contain
   /// to the maximum size of any assigns clause involved in the model.
   void transform_goto_model();
 
@@ -205,7 +210,7 @@ class dfcct
   const optionalt<std::pair<irep_idt, irep_idt>> &to_check;
   const bool allow_recursive_calls;
   const std::map<irep_idt, irep_idt> &to_replace;
-  const bool apply_loop_contracts;
+  const dfcc_loop_contract_modet loop_contract_mode;
   const std::set<std::string> &to_exclude_from_nondet_static;
   message_handlert &message_handler;
   messaget log;
@@ -215,10 +220,10 @@ class dfcct
   dfcc_utilst utils;
   dfcc_libraryt library;
   namespacet ns;
-  dfcc_instrumentt instrument;
-  dfcc_lift_memory_predicatest memory_predicates;
   dfcc_spec_functionst spec_functions;
   dfcc_contract_clauses_codegent contract_clauses_codegen;
+  dfcc_instrumentt instrument;
+  dfcc_lift_memory_predicatest memory_predicates;
   dfcc_contract_handlert contract_handler;
   dfcc_swap_and_wrapt swap_and_wrap;
 
@@ -277,7 +282,7 @@ class dfcct
   /// for each instrumented function
   ///
   /// A call to `nondet_static` will re-generate the initialize function with
-  /// nondet values. The intrumentation statics will not get nondet initialised
+  /// nondet values. The instrumentation statics will not get nondet initialised
   /// by virtue of being tagged with ID_C_no_nondet_initialization.
   ///
   /// However, nondet_static expects instructions to be either function calls

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

@@ -8,11 +8,13 @@ Date: February 2023
 \*******************************************************************/
 #include "dfcc_contract_clauses_codegen.h"
 
+#include <util/c_types.h>
 #include <util/expr_util.h>
 #include <util/fresh_symbol.h>
 #include <util/invariant.h>
 #include <util/mathematical_expr.h>
 #include <util/namespace.h>
+#include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
 #include <util/std_expr.h>
 
@@ -23,21 +25,18 @@ Date: February 2023
 #include <langapi/language_util.h>
 
 #include "dfcc_library.h"
-#include "dfcc_spec_functions.h"
 #include "dfcc_utils.h"
 
 dfcc_contract_clauses_codegent::dfcc_contract_clauses_codegent(
   goto_modelt &goto_model,
   message_handlert &message_handler,
   dfcc_utilst &utils,
-  dfcc_libraryt &library,
-  dfcc_spec_functionst &spec_functions)
+  dfcc_libraryt &library)
   : goto_model(goto_model),
     message_handler(message_handler),
     log(message_handler),
     utils(utils),
     library(library),
-    spec_functions(spec_functions),
     ns(goto_model.symbol_table)
 {
 }
@@ -63,6 +62,7 @@ void dfcc_contract_clauses_codegent::gen_spec_assigns_instructions(
 
   // inline resulting program and check for loops
   inline_and_check_warnings(dest);
+  dest.update();
   PRECONDITION_WITH_DIAGNOSTICS(
     is_loop_free(dest, ns, log),
     "loops in assigns clause specification functions must be unwound before "

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

@@ -8,8 +8,6 @@ Date: February 2023
 \*******************************************************************/
 
 /// \file
-/// Translates assigns and frees clauses of a function contract or
-/// loop contract into goto programs that build write sets or havoc write sets.
 
 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CONTRACT_CLAUSES_CODEGEN_H
 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CONTRACT_CLAUSES_CODEGEN_H
@@ -29,25 +27,23 @@ class goto_modelt;
 class message_handlert;
 class dfcc_libraryt;
 class dfcc_utilst;
-class dfcc_spec_functionst;
 class code_with_contract_typet;
 class conditional_target_group_exprt;
 
+/// Translates assigns and frees clauses of a function contract or
+/// loop contract into GOTO programs that build write sets or havoc write sets.
 class dfcc_contract_clauses_codegent
 {
 public:
-  /// \param goto_model goto model being transformed
-  /// \param message_handler used debug/warning/error messages
-  /// \param utils utility class for dynamic frames
-  /// \param library the contracts instrumentation library
-  /// \param spec_functions provides translation methods for assignable set
-  /// or freeable set specification functions.
+  /// \param goto_model GOTO model being transformed
+  /// \param message_handler Used debug/warning/error messages
+  /// \param utils Utility class for dynamic frames
+  /// \param library The contracts instrumentation library
   dfcc_contract_clauses_codegent(
     goto_modelt &goto_model,
     message_handlert &message_handler,
     dfcc_utilst &utils,
-    dfcc_libraryt &library,
-    dfcc_spec_functionst &spec_functions);
+    dfcc_libraryt &library);
 
   /// \brief Generates instructions encoding the \p assigns_clause targets and
   /// adds them to \p dest.
@@ -85,7 +81,6 @@ class dfcc_contract_clauses_codegent
   messaget log;
   dfcc_utilst &utils;
   dfcc_libraryt &library;
-  dfcc_spec_functionst &spec_functions;
   namespacet ns;
 
   /// Generates GOTO instructions to build the representation of the given

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

@@ -24,7 +24,6 @@ Date: August 2022
 #include <goto-programs/remove_function_pointers.h>
 
 #include <ansi-c/c_expr.h>
-#include <goto-instrument/contracts/contracts.h>
 #include <goto-instrument/contracts/utils.h>
 #include <langapi/language_util.h>
 
@@ -79,7 +78,8 @@ dfcc_contract_handlert::get_contract_functions(const irep_idt &contract_id)
          utils,
          library,
          spec_functions,
-         contract_clauses_codegen)})
+         contract_clauses_codegen,
+         instrument)})
     .first->second;
 }