Merge pull request #8361 from qinheping/issue/8329

Keep quantified symbols unique during smt2_conv

Author: qinheping

regression/contracts-dfcc/quantifiers-loop-05/main.c

@@ -0,0 +1,34 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stddef.h>
+
+#define N 16
+
+void main()
+{
+  int a[N];
+  a[10] = 0;
+  bool flag = true;
+  for(size_t j = 0; j < N; ++j)
+    // clang-format off
+  __CPROVER_assigns(j, __CPROVER_object_whole(a))
+  __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(size_t i = 0; i < N; ++i)
+        // clang-format off
+      __CPROVER_assigns(i, __CPROVER_object_whole(a))
+      __CPROVER_loop_invariant(0 <= i && i <= N)
+      __CPROVER_loop_invariant(__CPROVER_forall { int k; k < i ==> a[k] == 1 })
+
+        // clang-format on
+        {
+          a[i] = 1;
+        }
+    }
+  assert(a[10] == 1);
+}

regression/contracts-dfcc/quantifiers-loop-05/test.desc

@@ -0,0 +1,11 @@
+CORE dfcc-only
+main.c
+--dfcc main --apply-loop-contracts _ --smt2
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+This test case checks the handling of quantifiers in a nested loop's
+loop contracts.

src/solvers/smt2/smt2_conv.cpp

@@ -4721,11 +4721,11 @@ void smt2_convt::set_to(const exprt &expr, bool value)
         identifier_map.find(identifier) == identifier_map.end() &&
         equal_expr.lhs() != equal_expr.rhs())
       {
-        identifiert &id=identifier_map[identifier];
-        CHECK_RETURN(id.type.is_nil());
+        auto id_entry = identifier_map.insert(
+          {identifier, identifiert{equal_expr.lhs().type(), false}});
+        CHECK_RETURN(id_entry.second);
 
-        id.type=equal_expr.lhs().type();
-        find_symbols(id.type);
+        find_symbols(id_entry.first->second.type);
         exprt prepared_rhs = prepare_for_convert_expr(equal_expr.rhs());
 
         std::string smt2_identifier=convert_identifier(identifier);
@@ -4908,17 +4908,30 @@ void smt2_convt::find_symbols(const exprt &expr)
 
   if(expr.id() == ID_exists || expr.id() == ID_forall)
   {
+    std::unordered_map<irep_idt, std::optional<identifiert>> shadowed_syms;
+
     // do not declare the quantified symbol, but record
     // as 'bound symbol'
     const auto &q_expr = to_quantifier_expr(expr);
     for(const auto &symbol : q_expr.variables())
     {
       const auto identifier = symbol.get_identifier();
-      identifiert &id = identifier_map[identifier];
-      id.type = symbol.type();
-      id.is_bound = true;
+      auto id_entry =
+        identifier_map.insert({identifier, identifiert{symbol.type(), true}});
+      shadowed_syms.insert(
+        {identifier,
+         id_entry.second ? std::nullopt
+                         : std::optional{id_entry.first->second}});
     }
     find_symbols(q_expr.where());
+    for(const auto &[id, shadowed_val] : shadowed_syms)
+    {
+      auto previous_entry = identifier_map.find(id);
+      if(!shadowed_val.has_value())
+        identifier_map.erase(previous_entry);
+      else
+        previous_entry->second = std::move(*shadowed_val);
+    }
     return;
   }
 
@@ -4941,12 +4954,11 @@ void smt2_convt::find_symbols(const exprt &expr)
       identifier="nondet_"+
         id2string(to_nondet_symbol_expr(expr).get_identifier());
 
-    identifiert &id=identifier_map[identifier];
+    auto id_entry =
+      identifier_map.insert({identifier, identifiert{expr.type(), false}});
 
-    if(id.type.is_nil())
+    if(id_entry.second)
     {
-      id.type=expr.type();
-
       std::string smt2_identifier=convert_identifier(identifier);
       smt2_identifiers.insert(smt2_identifier);
 

src/solvers/smt2/smt2_conv.h

@@ -242,13 +242,16 @@ class smt2_convt : public stack_decision_proceduret
   // keeps track of all non-Boolean symbols and their value
   struct identifiert
   {
+    // We do not currently read any of the following members, but might do so in
+    // future. At this time, we just care about (not) having an entry in
+    // `identifier_map`.
     bool is_bound;
     typet type;
     exprt value;
 
-    identifiert() : is_bound(false)
+    identifiert(typet type, bool is_bound)
+      : is_bound(is_bound), type(std::move(type))
     {
-      type.make_nil();
       value.make_nil();
     }
   };