Merge pull request #6034 from padhi-aws-forks/invariant_struct_fix

Fix havocing of struct members when enforcing invariants

Author: NlightNFotis

regression/contracts/invar_dynamic_struct_member/main.c

@@ -0,0 +1,30 @@
+typedef struct test
+{
+  int x;
+} test;
+
+void main()
+{
+  struct test *t = malloc(sizeof(test));
+  t->x = 0;
+
+  unsigned n;
+  for(unsigned i = 0; i < n; ++i)
+    __CPROVER_loop_invariant(i <= n)
+    {
+      switch(i % 4)
+      {
+      case 0:
+        break;
+
+      case 1:
+      case 2:
+        t->x += 1;
+
+      default:
+        t->x += 2;
+      }
+    }
+
+  assert(t->x == 0 || t->x == 1 || t->x == 2);
+}

regression/contracts/invar_dynamic_struct_member/test.desc

@@ -0,0 +1,18 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^\[main.1\] .* Check loop invariant before entry: SUCCESS$
+^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.assertion.1\] .* assertion .*: FAILURE$
+^VERIFICATION FAILED$
+--
+--
+This test checks that  members of typedef'd and dynamically allocated structs
+are correctly havoced when enforcing loop invariants.
+The assertion is expected to fail when `t->x` is correctly havoced (so would be
+set to a nondet value).
+However, it `t->x` is not havoced then it stays at value `0` and would satisfy
+the assertion when the loop is replaced by a single nondet iteration.
+

regression/contracts/invar_struct_member/main.c

@@ -0,0 +1,19 @@
+struct test
+{
+  int x;
+};
+
+void main()
+{
+  struct test t;
+  t.x = 0;
+
+  unsigned n;
+  for(unsigned i = 0; i < n; ++i)
+    __CPROVER_loop_invariant(i <= n)
+    {
+      t.x += 2;
+    }
+
+  assert(t.x == 0 || t.x == 2);
+}

regression/contracts/invar_struct_member/test.desc

@@ -0,0 +1,17 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=10$
+^SIGNAL=0$
+^\[main.1\] .* Check loop invariant before entry: SUCCESS$
+^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.assertion.1\] .* assertion t.x == 0 || t.x == 2: FAILURE$
+^VERIFICATION FAILED$
+--
+--
+This test checks that members of statically allocated are correctly havoced
+when enforcing loop invariants.
+The `t.x == 0 || t.x == 2` assertion is expected to fail when `t.x` is correctly
+havoced (so would be set to a nondet value).
+However, it `t.x` is not havoced then it stays at value `0` and would satisfy
+the assertion when the loop is replaced by a single nondet iteration.

src/goto-instrument/loop_utils.cpp

@@ -61,17 +61,14 @@ void get_modifies_lhs(
   const exprt &lhs,
   modifiest &modifies)
 {
-  if(lhs.id()==ID_symbol)
+  if(lhs.id() == ID_symbol || lhs.id() == ID_member)
     modifies.insert(lhs);
   else if(lhs.id()==ID_dereference)
   {
     const auto &pointer = to_dereference_expr(lhs).pointer();
     for(const auto &mod : local_may_alias.get(t, pointer))
       modifies.insert(dereference_exprt{mod});
   }
-  else if(lhs.id()==ID_member)
-  {
-  }
   else if(lhs.id()==ID_index)
   {
   }