instruments loops per given assigns clauses

Author: SaswatPadhi

regression/contracts/invar_assigns_alias_analysis/test.desc

@@ -2,14 +2,8 @@
 
 int main()
 {
-  int r;
-  __CPROVER_assume(r >= 0);
-  while(r > 0)
-    __CPROVER_assigns() __CPROVER_loop_invariant(r >= 0)
+  while(1 == 1)
+    __CPROVER_assigns() __CPROVER_loop_invariant(1 == 1)
     {
-      r--;
     }
-  assert(r == 0);
-
-  return 0;
 }

regression/contracts/invar_assigns_empty/main.c

@@ -5,7 +5,6 @@ main.c
 ^SIGNAL=0$
 ^\[main.1\] .* Check loop invariant before entry: SUCCESS$
 ^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.1\] .* assertion r == 0: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 --

regression/contracts/invar_assigns_empty/test.desc

@@ -3,14 +3,16 @@ main.c
 --apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.3\] .* Check decreases clause on loop iteration: SUCCESS$
-^\[main.assertion.1\] .* assertion r1 == 0: SUCCESS$
-^\[main.4\] .* Check loop invariant before entry: SUCCESS$
-^\[main.5\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.6\] .* Check decreases clause on loop iteration: SUCCESS$
-^\[main.assertion.2\] .* assertion r2 == 0: SUCCESS$
+^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.\d+\] .* Check decreases clause on loop iteration: SUCCESS$
+^\[main.assertion.\d+\] .* assertion r1 == 0: SUCCESS$
+^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main.\d+\] .* Check that s2 is assignable: SUCCESS$
+^\[main.\d+\] .* Check that r2 is assignable: SUCCESS$
+^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.\d+\] .* Check decreases clause on loop iteration: SUCCESS$
+^\[main.assertion.\d+\] .* assertion r2 == 0: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 --

regression/contracts/invar_assigns_opt/test.desc

@@ -0,0 +1,27 @@
+#include <assert.h>
+#include <stdlib.h>
+
+#define SIZE 8
+
+struct blob
+{
+  char *data;
+};
+
+void main()
+{
+  struct blob *b = malloc(sizeof(struct blob));
+  b->data = malloc(SIZE);
+
+  b->data[5] = 0;
+  for(unsigned i = 0; i < SIZE; i++)
+    // clang-format off
+    __CPROVER_assigns(i, __CPROVER_POINTER_OBJECT(b->data))
+    __CPROVER_loop_invariant(i <= SIZE)
+    // clang-format on
+    {
+      b->data[i] = 1;
+    }
+
+  assert(b->data[5] == 0);
+}

regression/contracts/loop_assigns-01/main.c

@@ -0,0 +1,16 @@
+CORE
+main.c
+--apply-loop-contracts
+^EXIT=10$
+^SIGNAL=0$
+^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main.\d+\] .* Check that i is assignable: SUCCESS$
+^\[main.\d+\] .* Check that b->data\[(.*)i\] is assignable: SUCCESS$
+^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.assertion.\d+\] .* assertion b->data\[5\] == 0: FAILURE$
+^VERIFICATION FAILED$
+--
+--
+This test (taken from #6021) shows the need for assigns clauses on loops.
+The alias analysis in this case returns `unknown`,
+and so we must manually annotate an assigns clause on the loop.

regression/contracts/loop_assigns-01/test.desc

@@ -16,7 +16,7 @@ void main()
   b->data[5] = 0;
   for(unsigned i = 0; i < SIZE; i++)
     // clang-format off
-    __CPROVER_assigns(b->data)
+    __CPROVER_assigns(i, b->data[i])
     __CPROVER_loop_invariant(i <= SIZE)
     // clang-format on
     {

regression/contracts/invar_assigns_alias_analysis/main.c renamed to regression/contracts/loop_assigns-02/main.c

@@ -0,0 +1,20 @@
+CORE
+main.c
+--apply-loop-contracts
+^EXIT=10$
+^SIGNAL=0$
+^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main.\d+\] .* Check that i is assignable: SUCCESS$
+^\[main.\d+\] .* Check that b->data\[(.*)i\] is assignable: FAILURE$
+^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.assertion.\d+\] .* assertion b->data\[5\] == 0: FAILURE$
+^VERIFICATION FAILED$
+--
+--
+This test (taken from #6021) shows the need for assigns clauses on loops.
+The alias analysis in this case returns `unknown`,
+and so we must manually annotate an assigns clause on the loop.
+
+Note that the annotated assigns clause in this case is an underapproximation,
+per the current semantics of the assigns clause -- it must model ALL memory
+being assigned to by the loop, not just a single symbolic iteration.

regression/contracts/loop_assigns-02/test.desc

@@ -0,0 +1,27 @@
+#include <assert.h>
+#include <stdlib.h>
+
+#define SIZE 8
+
+struct blob
+{
+  char *data;
+};
+
+void main()
+{
+  struct blob *b = malloc(sizeof(struct blob));
+  b->data = malloc(SIZE);
+
+  b->data[5] = 0;
+  for(unsigned i = 0; i < SIZE; i++)
+    // clang-format off
+    __CPROVER_assigns(__CPROVER_POINTER_OBJECT(b->data))
+    __CPROVER_loop_invariant(i <= SIZE)
+    // clang-format on
+    {
+      b->data[i] = 1;
+    }
+
+  assert(b->data[5] == 0);
+}

regression/contracts/loop_assigns-03/main.c

@@ -0,0 +1,19 @@
+CORE
+main.c
+--apply-loop-contracts
+^EXIT=10$
+^SIGNAL=0$
+^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main.\d+\] .* Check that i is assignable: FAILURE$
+^\[main.\d+\] .* Check that b->data\[(.*)i\] is assignable: SUCCESS$
+^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.assertion.\d+\] .* assertion b->data\[5\] == 0: SUCCESS$
+^VERIFICATION FAILED$
+--
+--
+This test (taken from #6021) shows the need for assigns clauses on loops.
+The alias analysis in this case returns `unknown`,
+and so we must manually annotate an assigns clause on the loop.
+
+Note that the annotated assigns clause in this case is an underapproximation,
+because `i` is also assigned in the loop and should be marked as assignable.