Merge pull request #7786 from remi-delmas-3000/contracts-fix-quantifier-vars

CONTRACTS: fix fresh symbols for quantified vars

Author: tautschnig

regression/contracts-dfcc/quantifiers-loops-fresh-bound-vars-smt/main.c

@@ -0,0 +1,32 @@
+#include <stdlib.h>
+void foo(char *dst, const char *src, size_t n)
+  // clang-format off
+  __CPROVER_requires(__CPROVER_is_fresh(src, n))
+  __CPROVER_requires(__CPROVER_is_fresh(dst, n))
+  __CPROVER_assigns(__CPROVER_object_from(dst))
+  __CPROVER_ensures(__CPROVER_forall {
+    size_t j;
+    j < n ==> dst[j] == src[j]
+  })
+// clang-format on
+{
+  for(size_t i = 0; i < n; i++)
+    // clang-format off
+    __CPROVER_assigns(i, __CPROVER_object_from(dst))
+    __CPROVER_loop_invariant(i <= n)
+    __CPROVER_loop_invariant(
+      __CPROVER_forall { size_t j; j < i ==> dst[j] == src[j] })
+    // clang-format on
+    {
+      dst[i] = src[i];
+    }
+}
+
+int main()
+{
+  char *dst;
+  char *src;
+  size_t n;
+  foo(dst, src, n);
+  return 0;
+}

regression/contracts-dfcc/quantifiers-loops-fresh-bound-vars-smt/test.desc

@@ -0,0 +1,15 @@
+CORE dfcc-only smt-backend broken-cprover-smt-backend
+main.c
+--dfcc main --apply-loop-contracts --enforce-contract foo --malloc-may-fail --malloc-fail-null _ --z3 --slice-formula
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Tests support for quantifiers in loop contracts with the SMT backend.
+When quantified loop invariants are used, they are inserted three times
+in the transformed program (base case assertion, step case assumption,
+step case assertion), and each occurrence needs to be rewritten with fresh
+symbols for the quantified variables. The SMT solver would with an error
+whenever this renaming is not properly done.

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

@@ -129,15 +129,10 @@ void dfcc_instrument_loopt::operator()(
     write_set_populate_instrs,
     nof_targets);
 
-  // Replace bound variables by fresh instances in quantified formulas.
-  exprt invariant = loop.invariant;
-  if(has_subexpr(invariant, ID_exists) || has_subexpr(invariant, ID_forall))
-    add_quantified_variable(symbol_table, invariant, language_mode);
-
   // ---------- Add instrumented instructions ----------
   goto_programt::targett loop_latch =
     loop.find_latch(goto_function.body).value();
-
+  exprt invariant(loop.invariant);
   const auto history_var_map = add_prehead_instructions(
     loop_id,
     goto_function,
@@ -240,7 +235,9 @@ dfcc_instrument_loopt::add_prehead_instructions(
   //   GOTO HEAD;
   // ```
 
-
+  // Replace bound variables by fresh instances in quantified formulas.
+  if(has_subexpr(invariant, ID_exists) || has_subexpr(invariant, ID_forall))
+    add_quantified_variable(symbol_table, invariant, language_mode);
   // initialize loop_entry history vars;
   auto replace_history_result = replace_history_loop_entry(
     symbol_table, invariant, loop_head_location, language_mode);
@@ -329,7 +326,7 @@ dfcc_instrument_loopt::add_step_instructions(
   goto_programt::targett loop_head,
   goto_programt::targett loop_latch,
   goto_programt &havoc_instrs,
-  const exprt &invariant,
+  exprt &invariant,
   const exprt::operandst &decreases_clauses,
   const symbol_exprt &addr_of_loop_write_set,
   const exprt &outer_write_set,
@@ -432,6 +429,9 @@ dfcc_instrument_loopt::add_step_instructions(
     dfcc_utilst::get_function_symbol(symbol_table, function_id).mode;
   {
     // Assume the loop invariant after havocing the state.
+    // Replace bound variables by fresh instances in quantified formulas.
+    if(has_subexpr(invariant, ID_exists) || has_subexpr(invariant, ID_forall))
+      add_quantified_variable(symbol_table, invariant, language_mode);
     code_assumet assumption{invariant};
     assumption.add_source_location() = loop_head_location;
     converter.goto_convert(assumption, step_instrs, language_mode);
@@ -461,7 +461,7 @@ void dfcc_instrument_loopt::add_body_instructions(
   symbol_table_baset &symbol_table,
   goto_programt::targett loop_head,
   goto_programt::targett loop_latch,
-  const exprt &invariant,
+  exprt &invariant,
   const exprt::operandst &decreases_clauses,
   const symbol_exprt &entered_loop,
   const symbol_exprt &in_base_case,
@@ -512,6 +512,10 @@ void dfcc_instrument_loopt::add_body_instructions(
       "Check invariant after step for loop " +
       id2string(check_location.get_function()) + "." +
       std::to_string(cbmc_loop_id));
+    // Assume the loop invariant after havocing the state.
+    // Replace bound variables by fresh instances in quantified formulas.
+    if(has_subexpr(invariant, ID_exists) || has_subexpr(invariant, ID_forall))
+      add_quantified_variable(symbol_table, invariant, language_mode);
     code_assertt assertion{invariant};
     assertion.add_source_location() = check_location;
     converter.goto_convert(assertion, pre_loop_latch_instrs, language_mode);

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

@@ -184,7 +184,7 @@ class dfcc_instrument_loopt
   /// \param[inout] loop_latch Latch node of the loop.
   /// \param[out] assigns_instrs `goto_programt` that contains instructions of
   ///                       populating assigns into the loop write set.
-  /// \param[out] invariant Loop invariants.
+  /// \param[in] invariant Loop invariants.
   /// \param[in] assigns Assigns targets of the loop.
   /// \param[in] loop_write_set Stack allocated loop write set variable.
   /// \param[in] addr_of_loop_write_set Loop write set pointer variable.
@@ -250,7 +250,7 @@ class dfcc_instrument_loopt
     goto_programt::targett loop_head,
     goto_programt::targett loop_latch,
     goto_programt &havoc_instrs,
-    const exprt &invariant,
+    exprt &invariant,
     const exprt::operandst &decreases_clauses,
     const symbol_exprt &loop_write_set,
     const exprt &outer_write_set,
@@ -296,7 +296,7 @@ class dfcc_instrument_loopt
     symbol_table_baset &symbol_table,
     goto_programt::targett loop_head,
     goto_programt::targett loop_latch,
-    const exprt &invariant,
+    exprt &invariant,
     const exprt::operandst &decreases_clauses,
     const symbol_exprt &entered_loop,
     const symbol_exprt &in_base_case,