Merge pull request #7216 from qinheping/assigns_inference

CONTRACTS: Fix inferring assigns clause with symbols out of scope

Author: remi-delmas-3000

regression/contracts/loop_assigns_inference/main.c

@@ -0,0 +1,58 @@
+#include <assert.h>
+
+int j;
+
+int lowerbound()
+{
+  return 0;
+}
+
+int upperbound()
+{
+  return 10;
+}
+
+void incr(int *i)
+{
+  (*i)++;
+}
+
+void body_1(int i)
+{
+  j = i;
+}
+
+void body_2(int *i)
+{
+  (*i)++;
+  (*i)--;
+}
+
+int body_3(int *i)
+{
+  (*i)++;
+  if(*i == 4)
+    return 1;
+
+  (*i)--;
+  return 0;
+}
+
+int main()
+{
+  for(int i = lowerbound(); i < upperbound(); incr(&i))
+    // clang-format off
+    __CPROVER_loop_invariant(0 <= i && i <= 10)
+    __CPROVER_loop_invariant(i != 0 ==> j + 1 == i)
+    // clang-format on
+    {
+      body_1(i);
+
+      if(body_3(&i))
+        return 1;
+
+      body_2(&i);
+    }
+
+  assert(j == 9);
+}

regression/contracts/loop_assigns_inference/test.desc

@@ -0,0 +1,17 @@
+CORE
+main.c
+--apply-loop-contracts
+^EXIT=0$
+^SIGNAL=0$
+^\[body_1.assigns.\d+\] .* Check that j is assignable: SUCCESS$
+^\[body_2.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$
+^\[body_3.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$
+^\[incr.assigns.\d+\] .* Check that \*i is assignable: SUCCESS$
+^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.assertion.\d+\] .* assertion j == 9: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks loop locals are correctly removed during assigns inference so
+that the assign clause is correctly inferred.

src/goto-instrument/contracts/cfg_info.h

@@ -19,6 +19,7 @@ Date: June 2022
 
 #include <util/byte_operators.h>
 #include <util/expr_cast.h>
+#include <util/find_symbols.h>
 #include <util/message.h>
 
 #include <goto-programs/goto_model.h>
@@ -172,8 +173,12 @@ class loop_cfg_infot : public cfg_infot
     auto it = exprs.begin();
     while(it != exprs.end())
     {
+      const std::unordered_set<irep_idt> symbols = find_symbol_identifiers(*it);
+
       if(
-        it->id() == ID_symbol && is_local(to_symbol_expr(*it).get_identifier()))
+        std::find_if(symbols.begin(), symbols.end(), [this](const irep_idt &s) {
+          return is_local(s);
+        }) != symbols.end())
       {
         it = exprs.erase(it);
       }