Update CLI for applyin loop contracts with dfcc

Author: qinheping

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

@@ -121,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)
 {
@@ -137,6 +138,7 @@ void dfcc(
     allow_recursive_calls,
     to_replace_map,
     apply_loop_contracts,
+    unwind_transformed_loops,
     to_exclude_from_nondet_static,
     message_handler);
 }
@@ -149,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,6 +163,7 @@ void dfcc(
     allow_recursive_calls,
     to_replace,
     apply_loop_contracts,
+    unwind_transformed_loops,
     message_handler,
     to_exclude_from_nondet_static};
 }
@@ -172,6 +176,7 @@ dfcct::dfcct(
   const bool allow_recursive_calls,
   const std::map<irep_idt, irep_idt> &to_replace,
   const bool apply_loop_contracts,
+  const bool unwind_transformed_loops,
   message_handlert &message_handler,
   const std::set<std::string> &to_exclude_from_nondet_static)
   : options(options),
@@ -213,9 +218,16 @@ dfcct::dfcct(
       library,
       spec_functions,
       contract_clauses_codegen),
-    instrument(goto_model, message_handler, utils, loop_instrument, library),
+    instrument(
+      goto_model,
+      message_handler,
+      utils,
+      loop_instrument,
+      apply_loop_contracts,
+      library),
     max_assigns_clause_size(0)
 {
+  instrument.unwind_transformed_loops = unwind_transformed_loops;
   transform_goto_model();
 }
 

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

@@ -60,7 +60,7 @@ class optionst;
 // clang-format off
 #define HELP_DFCC                                                              \
   "--dfcc <harness>   activate dynamic frame condition checking for function\n"\
-  "                   contracts using the given harness as entry point"
+  "                   contracts using the given harness as 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);
 
@@ -159,6 +165,8 @@ class dfcct
   /// \param to_replace functions-to-contract mapping for replacement
   /// \param apply_loop_contracts apply loop contract transformations iff true
   /// havocing static program symbols.
+  /// \param unwind_transformed_loops unwind transformed loops after 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(
@@ -169,6 +177,7 @@ class dfcct
     const bool allow_recursive_calls,
     const std::map<irep_idt, irep_idt> &to_replace,
     const bool apply_loop_contracts,
+    const bool unwind_transformed_loops,
     message_handlert &message_handler,
     const std::set<std::string> &to_exclude_from_nondet_static);
 
@@ -194,7 +203,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();
 
@@ -278,7 +287,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_instrument.cpp

@@ -29,6 +29,8 @@ Author: Remi Delmas, [email protected]
 #include <goto-instrument/contracts/dynamic-frames/dfcc_loop_utils.h>
 #include <goto-instrument/contracts/utils.h>
 #include <goto-instrument/generate_function_bodies.h>
+#include <goto-instrument/unwind.h>
+#include <goto-instrument/unwindset.h>
 #include <langapi/language_util.h>
 
 #include "dfcc_is_freeable.h"
@@ -47,12 +49,14 @@ dfcc_instrumentt::dfcc_instrumentt(
   message_handlert &message_handler,
   dfcc_utilst &utils,
   dfcc_loop_instrumentt &loop_instrument,
+  const bool apply_loop_contracts,
   dfcc_libraryt &library)
   : goto_model(goto_model),
     message_handler(message_handler),
     log(message_handler),
     utils(utils),
     loop_instrument(loop_instrument),
+    apply_loop_contracts(apply_loop_contracts),
     library(library),
     ns(goto_model.symbol_table)
 {
@@ -260,6 +264,31 @@ void dfcc_instrumentt::instrument_harness_function(
   dfcc_obeys_contractt obeys_contract(library, message_handler);
   obeys_contract.rewrite_calls(body, null_expr, function_pointer_contracts);
 
+  if(apply_loop_contracts)
+  {
+    // DECL write_set_to_check
+    // ASSIGN write_set_to_check := NULL
+    auto &goto_function =
+      goto_model.goto_functions.function_map.at(function_id);
+    const auto &write_set = utils.create_new_parameter_symbol(
+      function_id,
+      "write_set_to_check",
+      library.dfcc_type[dfcc_typet::WRITE_SET_PTR]);
+    auto first_instr = goto_function.body.instructions.begin();
+    goto_function.body.insert_before(
+      first_instr, goto_programt::make_decl(write_set.symbol_expr()));
+    goto_function.body.insert_before(
+      first_instr,
+      goto_programt::make_assignment(write_set.symbol_expr(), null_expr));
+
+    goto_function.body.update();
+    instrument_loops(
+      function_id,
+      goto_function,
+      write_set.symbol_expr(),
+      function_pointer_contracts);
+  }
+
   // rewrite calls
   Forall_goto_program_instructions(it, body)
   {
@@ -346,7 +375,6 @@ void dfcc_instrumentt::instrument_loops(
   const irep_idt &function_id,
   goto_functiont &goto_function,
   const exprt &write_set,
-  cfg_infot &cfg_info,
   std::set<irep_idt> &function_pointer_contracts)
 {
   auto &function_body = goto_function.body;
@@ -385,10 +413,14 @@ void dfcc_instrumentt::instrument_loops(
       addr_of_loop_write_set;
   }
 
+  /// \brief Names of loops we are going to unwind.
+  std::list<std::string> unwind_loop_names;
+
   // Iterate over the (natural) loops in the function, in topo-sorted order,
   // and apply any loop contracts that we find.
   for(const auto &idx : loop_nesting_graph.topsort())
   {
+    const auto loop_number = loop_nesting_graph[idx].latch_target->loop_number;
     const auto &loop_node = loop_nesting_graph[idx];
     if(
       loop_node.assigns_clause.is_nil() && loop_node.invariant.is_nil() &&
@@ -430,9 +462,9 @@ void dfcc_instrumentt::instrument_loops(
     }
     const auto write_set_ptr = expr_try_dynamic_cast<symbol_exprt>(write_set);
     const symbol_exprt &outer_write_set =
-      (outer_idx == idx)
-        ? *write_set_ptr
-        : loop_nesting_graph[outer_idx].write_set_symbol.symbol_expr();
+      (outer_idx == idx) ? *write_set_ptr
+                         : loop_nesting_graph[outer_idx]
+                             .addr_of_loop_write_set_symbol.symbol_expr();
 
     loop_instrument.instrument(
       function_id,
@@ -446,6 +478,25 @@ void dfcc_instrumentt::instrument_loops(
       outer_write_set,
       loop_nesting_graph.get_reachable(idx, false),
       utils.get_function_symbol(function_id).mode);
+
+    // We will unwind all transformed loops twice. Store the names of
+    // to-unwind-loops here and perform the unwinding after transformation done.
+    // As described in `check_apply_loop_contracts`, loops with loop contracts
+    // will be transformed to a loop that execute exactly twice: one for base
+    // case and one for step case. So we unwind them here to avoid users
+    // incorrectly unwind them only once.
+    std::string to_unwind =
+      id2string(function_id) + "." + std::to_string(loop_number) + ":2";
+    unwind_loop_names.push_back(to_unwind);
+  }
+
+  // unwind all transformed loops twice.
+  if(unwind_transformed_loops)
+  {
+    unwindsett unwindset{goto_model};
+    unwindset.parse_unwindset(unwind_loop_names, log.get_message_handler());
+    goto_unwindt goto_unwind;
+    goto_unwind(goto_model, unwindset, goto_unwindt::unwind_strategyt::ASSUME);
   }
 
   remove_skip(goto_model);
@@ -475,12 +526,11 @@ void dfcc_instrumentt::instrument_function_body(
   auto &body = goto_function.body;
 
   // Instrument all loops in the function.
-  instrument_loops(
-    function_id,
-    goto_function,
-    write_set,
-    cfg_info,
-    function_pointer_contracts);
+  if(apply_loop_contracts)
+  {
+    instrument_loops(
+      function_id, goto_function, write_set, function_pointer_contracts);
+  }
 
   const auto &not_in_loop_filter =
     [&](const goto_programt::instructiont::targett &target) {

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

@@ -45,6 +45,7 @@ class dfcc_instrumentt
     message_handlert &message_handler,
     dfcc_utilst &utils,
     dfcc_loop_instrumentt &loop_instrument,
+    const bool apply_loop_contracts,
     dfcc_libraryt &library);
 
   /// True if id has `CPROVER_PREFIX` or `__VERIFIER` or `nondet` prefix,
@@ -149,19 +150,22 @@ class dfcc_instrumentt
     const irep_idt &function_id,
     goto_functiont &goto_function,
     const exprt &write_set,
-    cfg_infot &cfg_info,
     std::set<irep_idt> &function_pointer_contracts);
 
   /// Adds the names of instrumented functions to \p dest.
   /// The names are kept track of in the \ref function_cache field.
   void get_instrumented_functions(std::set<irep_idt> &dest) const;
 
+  /// \brief Unwind transformed loops after applying loop contracts or not.
+  bool unwind_transformed_loops = true;
+
 protected:
   goto_modelt &goto_model;
   message_handlert &message_handler;
   messaget log;
   dfcc_utilst &utils;
   dfcc_loop_instrumentt &loop_instrument;
+  const bool apply_loop_contracts;
   dfcc_libraryt &library;
   namespacet ns;
 

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

@@ -115,6 +115,10 @@ void dfcc_loop_instrumentt::instrument(
     addr_of_loop_write_set, symbol_mode, assigns_instrs, nof_targets);
   write_set_populate_instrs.copy_from(assigns_instrs);
 
+  // replace bound variables by fresh instances
+  if(has_subexpr(invariant, ID_exists) || has_subexpr(invariant, ID_forall))
+    add_quantified_variable(symbol_table, invariant, symbol_mode);
+
   // ---------- Start to add instrumented instructions ----------
   const auto &history_var_map = add_prehead_instructions(
     function_id,
@@ -244,7 +248,7 @@ std::map<exprt, exprt> dfcc_loop_instrumentt::add_prehead_instructions(
   goto_programt::targett loop_head,
   goto_programt::targett loop_latch,
   goto_programt &assigns_instrs,
-  exprt invariant,
+  exprt &invariant,
   const exprt::operandst &assigns,
   const symbol_exprt &loop_write_set,
   const symbol_exprt &addr_of_loop_write_set,
@@ -372,8 +376,8 @@ dfcc_loop_instrumentt::add_step_instructions(
   goto_programt::targett loop_head,
   goto_programt::targett loop_latch,
   goto_programt &havoc_instrs,
-  exprt invariant,
-  exprt decreases_clause,
+  const exprt &invariant,
+  const exprt &decreases_clause,
   const symbol_exprt &addr_of_loop_write_set,
   const symbol_exprt &outer_write_set,
   const symbol_exprt &initial_invariant_val,
@@ -696,7 +700,7 @@ void dfcc_loop_instrumentt::add_exit_instructions(
 
     goto_programt pre_loop_exit_instrs;
     // Assertion to check that step case was checked if we entered the loop.
-    source_locationt annotated_location = loop_head_location;
+    source_locationt annotated_location = exit_target->source_location();
     annotated_location.set_comment(
       "Check that loop instrumentation was not truncated");
     pre_loop_exit_instrs.add(goto_programt::make_assertion(

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

@@ -166,7 +166,7 @@ class dfcc_loop_instrumentt
     goto_programt::targett loop_head,
     goto_programt::targett loop_latch,
     goto_programt &assigns_instrs,
-    exprt invariant,
+    exprt &invariant,
     const exprt::operandst &assigns,
     const symbol_exprt &loop_write_set,
     const symbol_exprt &addr_of_loop_write_set,
@@ -209,8 +209,8 @@ class dfcc_loop_instrumentt
     goto_programt::targett loop_head,
     goto_programt::targett loop_latch,
     goto_programt &havoc_instrs,
-    exprt invariant,
-    exprt decreases_clause,
+    const exprt &invariant,
+    const exprt &decreases_clause,
     const symbol_exprt &loop_write_set,
     const symbol_exprt &outer_write_set,
     const symbol_exprt &initial_invariant_val,