Keep quantified symbols unique during symex_assume

qinheping · Jun 27, 2024 · 73ef5ef · 73ef5ef
1 parent 7e5d539
commit 73ef5ef
Show file tree

Hide file tree

Showing 4 changed files with 36 additions and 4 deletions.
diff --git a/...ntracts-dfcc/quantifiers-loop-fail/main.c → ...contracts-dfcc/quantifiers-loop-05/main.c b/...ntracts-dfcc/quantifiers-loop-fail/main.c → ...contracts-dfcc/quantifiers-loop-05/main.c
@@ -9,7 +9,13 @@ void main()
   a[10] = 0;
   bool flag = true;
   for(int j = 0; j < N; ++j)
+    // clang-format off
     __CPROVER_loop_invariant(j <= N)
+    __CPROVER_loop_invariant((j != 0) ==> __CPROVER_forall {
+        int k;
+        (0 <= k && k < N) ==> (a[k] == 1)
+    })
+    // clang-format on
     {
       for(int i = 0; i < N; ++i)
         // clang-format off

diff --git a/...acts-dfcc/quantifiers-loop-fail/test.desc → ...tracts-dfcc/quantifiers-loop-05/test.desc b/...acts-dfcc/quantifiers-loop-fail/test.desc → ...tracts-dfcc/quantifiers-loop-05/test.desc
@@ -1,11 +1,9 @@
 CORE dfcc-only
 main.c
 --dfcc main --apply-loop-contracts _ --smt2
-^EXIT=6$
+^EXIT=0$
 ^SIGNAL=0$
-^SMT2 solver returned error message:$
-^.*\"line \d+ column \d+: unknown constant .*$
-^VERIFICATION ERROR$
+^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
 --

diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
@@ -802,6 +802,8 @@ class goto_symext
   virtual void symex_output(statet &state, const codet &code);
 
   void rewrite_quantifiers(exprt &, statet &);
+  /// We record all bounded variable and keep unique by means of L2 renaming
+  void record_bounded_variables(exprt &, statet &);
 
   /// \brief Symbolic execution paths to be resumed later
   /// \remarks

diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
@@ -196,12 +196,38 @@ void goto_symext::vcc(
     state.guard.as_expr(), guarded_condition, property_id, msg, state.source);
 }
 
+void goto_symext::record_bounded_variables(exprt &expr, statet &state)
+{
+  if(expr.id() == ID_forall || expr.id() == ID_exists)
+  {
+    auto &quant_expr = to_quantifier_expr(expr);
+    symbol_exprt tmp0 =
+      to_symbol_expr(to_ssa_expr(quant_expr.symbol()).get_original_expr());
+    symex_decl(state, tmp0);
+    instruction_local_symbols.push_back(tmp0);
+    exprt tmp = quant_expr.where();
+    record_bounded_variables(tmp, state);
+  }
+  else if(expr.id() == ID_or || expr.id() == ID_and)
+  {
+    for(auto &op : expr.operands())
+      record_bounded_variables(op, state);
+  }
+}
+
 void goto_symext::symex_assume(statet &state, const exprt &cond)
 {
   exprt simplified_cond = clean_expr(cond, state, false);
   simplified_cond = state.rename(std::move(simplified_cond), ns).get();
   do_simplify(simplified_cond);
 
+  if(
+    has_subexpr(simplified_cond, ID_exists) ||
+    has_subexpr(simplified_cond, ID_forall))
+  {
+    record_bounded_variables(simplified_cond, state);
+  }
+
   // It would be better to call try_filter_value_sets after apply_condition,
   // but it is not currently possible. See the comment at the beginning of
   // \ref apply_goto_condition for more information.