Merge pull request #8356 from qinheping/feature/use_loop_contract_config

[CONTRACTS] Use unified loop contract config

Author: qinheping

src/goto-instrument/Makefile

@@ -21,7 +21,6 @@ SRC = accelerate/accelerate.cpp \
       contracts/dynamic-frames/dfcc_utils.cpp \
       contracts/dynamic-frames/dfcc_loop_nesting_graph.cpp \
       contracts/dynamic-frames/dfcc_contract_mode.cpp \
-      contracts/dynamic-frames/dfcc_loop_contract_mode.cpp \
       contracts/dynamic-frames/dfcc_loop_tags.cpp \
       contracts/dynamic-frames/dfcc_check_loop_normal_form.cpp \
       contracts/dynamic-frames/dfcc_root_object.cpp \

src/goto-instrument/contracts/contracts.cpp

@@ -1500,7 +1500,7 @@ void code_contractst::apply_loop_contracts(
   nondet_static(goto_model, to_exclude_from_nondet_init);
 
   // unwind all transformed loops twice.
-  if(unwind_transformed_loops)
+  if(loop_contract_config.unwind_transformed_loops)
   {
     unwindsett unwindset{goto_model};
     unwindset.parse_unwindset(loop_names, log.get_message_handler());

src/goto-instrument/contracts/contracts.h

@@ -22,6 +22,8 @@ Date: February 2016
 
 #include <goto-instrument/loop_utils.h>
 
+#include "loop_contract_config.h"
+
 #include <map>
 #include <set>
 #include <string>
@@ -55,12 +57,16 @@ class local_may_aliast;
 class code_contractst
 {
 public:
-  code_contractst(goto_modelt &goto_model, messaget &log)
+  code_contractst(
+    goto_modelt &goto_model,
+    messaget &log,
+    const loop_contract_configt &loop_contract_config)
     : ns(goto_model.symbol_table),
       goto_model(goto_model),
       symbol_table(goto_model.symbol_table),
       goto_functions(goto_model.goto_functions),
-      log(log)
+      log(log),
+      loop_contract_config(loop_contract_config)
   {
   }
 
@@ -138,9 +144,6 @@ class code_contractst
 
   namespacet ns;
 
-  // Unwind transformed loops after applying loop contracts or not.
-  bool unwind_transformed_loops = true;
-
 protected:
   goto_modelt &goto_model;
   symbol_tablet &symbol_table;
@@ -164,6 +167,9 @@ class code_contractst
   std::unordered_set<goto_programt::const_targett, const_target_hash>
     loop_havoc_set;
 
+  // Loop contract configuration
+  loop_contract_configt loop_contract_config;
+
 public:
   /// \brief Enforce contract of a single function
   void enforce_contract(const irep_idt &function);

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

@@ -119,52 +119,25 @@ void dfcc(
   const std::optional<irep_idt> &to_check,
   const bool allow_recursive_calls,
   const std::set<irep_idt> &to_replace,
-  const bool apply_loop_contracts,
-  const bool unwind_transformed_loops,
+  const loop_contract_configt loop_contract_config,
   const std::set<std::string> &to_exclude_from_nondet_static,
   message_handlert &message_handler)
 {
   std::map<irep_idt, irep_idt> to_replace_map;
   for(const auto &cli_flag : to_replace)
     to_replace_map.insert(parse_function_contract_pair(cli_flag));
 
-  dfcc(
+  dfcct(
     options,
     goto_model,
     harness_id,
     to_check.has_value() ? parse_function_contract_pair(to_check.value())
                          : std::optional<std::pair<irep_idt, irep_idt>>{},
     allow_recursive_calls,
     to_replace_map,
-    apply_loop_contracts,
-    unwind_transformed_loops,
-    to_exclude_from_nondet_static,
-    message_handler);
-}
-
-void dfcc(
-  const optionst &options,
-  goto_modelt &goto_model,
-  const irep_idt &harness_id,
-  const std::optional<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 bool unwind_transformed_loops,
-  const std::set<std::string> &to_exclude_from_nondet_static,
-  message_handlert &message_handler)
-{
-  dfcct{
-    options,
-    goto_model,
-    harness_id,
-    to_check,
-    allow_recursive_calls,
-    to_replace,
-    dfcc_loop_contract_mode_from_bools(
-      apply_loop_contracts, unwind_transformed_loops),
+    loop_contract_config,
     message_handler,
-    to_exclude_from_nondet_static};
+    to_exclude_from_nondet_static);
 }
 
 dfcct::dfcct(
@@ -174,7 +147,7 @@ dfcct::dfcct(
   const std::optional<std::pair<irep_idt, irep_idt>> &to_check,
   const bool allow_recursive_calls,
   const std::map<irep_idt, irep_idt> &to_replace,
-  const dfcc_loop_contract_modet loop_contract_mode,
+  const loop_contract_configt loop_contract_config,
   message_handlert &message_handler,
   const std::set<std::string> &to_exclude_from_nondet_static)
   : options(options),
@@ -183,7 +156,7 @@ dfcct::dfcct(
     to_check(to_check),
     allow_recursive_calls(allow_recursive_calls),
     to_replace(to_replace),
-    loop_contract_mode(loop_contract_mode),
+    loop_contract_config(loop_contract_config),
     to_exclude_from_nondet_static(to_exclude_from_nondet_static),
     message_handler(message_handler),
     log(message_handler),
@@ -339,7 +312,7 @@ void dfcct::instrument_harness_function()
                << messaget::eom;
 
   instrument.instrument_harness_function(
-    harness_id, loop_contract_mode, function_pointer_contracts);
+    harness_id, loop_contract_config, function_pointer_contracts);
 
   other_symbols.erase(harness_id);
 }
@@ -368,7 +341,7 @@ void dfcct::wrap_checked_function()
                  << contract_id << "' in CHECK mode" << messaget::eom;
 
     swap_and_wrap.swap_and_wrap_check(
-      loop_contract_mode,
+      loop_contract_config,
       wrapper_id,
       contract_id,
       function_pointer_contracts,
@@ -486,7 +459,7 @@ void dfcct::instrument_other_functions()
     log.status() << "Instrumenting '" << function_id << "'" << messaget::eom;
 
     instrument.instrument_function(
-      function_id, loop_contract_mode, function_pointer_contracts);
+      function_id, loop_contract_config, function_pointer_contracts);
   }
 
   goto_model.goto_functions.update();

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

@@ -38,7 +38,6 @@ Author: Remi Delmas, [email protected]
 #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"
 
@@ -96,9 +95,7 @@ class invalid_function_contract_pair_exceptiont : public cprover_exception_baset
 /// \param to_check function to check against its contract
 /// \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 loop_contract_config configuration for 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
@@ -109,41 +106,7 @@ void dfcc(
   const std::optional<irep_idt> &to_check,
   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);
-
-/// \ingroup dfcc-module
-/// \brief Applies function contracts and loop contracts transformation to GOTO
-/// model, using the dynamic frame condition checking approach.
-///
-/// Functions to check/replace are explicitly mapped to contracts.
-/// When checking function `foo` against contract `bar`, we require the
-/// actual contract symbol to exist as `contract::bar` in the symbol table.
-///
-/// \param options CLI options (used to lookup options for language config when
-/// re-defining the model's entry point)
-/// \param goto_model GOTO model to transform
-/// \param harness_id Proof harness name, must be the entry point of the model
-/// \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
-/// \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
-void dfcc(
-  const optionst &options,
-  goto_modelt &goto_model,
-  const irep_idt &harness_id,
-  const std::optional<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 bool unwind_transformed_loops,
+  const loop_contract_configt loop_contract_config,
   const std::set<std::string> &to_exclude_from_nondet_static,
   message_handlert &message_handler);
 
@@ -160,7 +123,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 loop_contract_mode mode to use for loop contracts
+  /// \param loop_contract_config configuration for applying loop contracts
   /// \param message_handler used for debug/warning/error messages
   /// \param to_exclude_from_nondet_static set of symbols to exclude when
   dfcct(
@@ -170,7 +133,7 @@ class dfcct
     const std::optional<std::pair<irep_idt, irep_idt>> &to_check,
     const bool allow_recursive_calls,
     const std::map<irep_idt, irep_idt> &to_replace,
-    const dfcc_loop_contract_modet loop_contract_mode,
+    const loop_contract_configt loop_contract_config,
     message_handlert &message_handler,
     const std::set<std::string> &to_exclude_from_nondet_static);
 
@@ -207,7 +170,7 @@ class dfcct
   const std::optional<std::pair<irep_idt, irep_idt>> &to_check;
   const bool allow_recursive_calls;
   const std::map<irep_idt, irep_idt> &to_replace;
-  const dfcc_loop_contract_modet loop_contract_mode;
+  const loop_contract_configt loop_contract_config;
   const std::set<std::string> &to_exclude_from_nondet_static;
   message_handlert &message_handler;
   messaget log;

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

@@ -506,7 +506,7 @@ dfcc_cfg_infot::dfcc_cfg_infot(
   const irep_idt &function_id,
   goto_functiont &goto_function,
   const exprt &top_level_write_set,
-  const dfcc_loop_contract_modet loop_contract_mode,
+  const loop_contract_configt &loop_contract_config,
   symbol_table_baset &symbol_table,
   message_handlert &message_handler,
   dfcc_libraryt &library)
@@ -517,7 +517,7 @@ dfcc_cfg_infot::dfcc_cfg_infot(
 {
   dfcc_loop_nesting_grapht loop_nesting_graph;
   goto_programt &goto_program = goto_function.body;
-  if(loop_contract_mode != dfcc_loop_contract_modet::NONE)
+  if(loop_contract_config.apply_loop_contracts)
   {
     messaget log(message_handler);
     dfcc_check_loop_normal_form(goto_program, log);

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

@@ -23,7 +23,7 @@ Date: March 2023
 
 #include <goto-programs/goto_program.h>
 
-#include "dfcc_loop_contract_mode.h"
+#include <goto-instrument/contracts/loop_contract_config.h>
 
 #include <map>
 #include <set>
@@ -238,7 +238,7 @@ class dfcc_cfg_infot
     const irep_idt &function_id,
     goto_functiont &goto_function,
     const exprt &top_level_write_set,
-    const dfcc_loop_contract_modet loop_contract_mode,
+    const loop_contract_configt &loop_contract_config,
     symbol_table_baset &symbol_table,
     message_handlert &message_handler,
     dfcc_libraryt &library);

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

@@ -80,9 +80,7 @@ void dfcc_contract_functionst::
 {
   std::set<irep_idt> function_pointer_contracts;
   instrument.instrument_function(
-    spec_function_id,
-    dfcc_loop_contract_modet::NONE,
-    function_pointer_contracts);
+    spec_function_id, loop_contract_configt{false}, function_pointer_contracts);
 
   INVARIANT(
     function_pointer_contracts.empty(),