Merge pull request #6249 from aalok-thakkar/loop-contract-assigns-clauses

Add support for assigns clauses on loops

Author: SaswatPadhi

regression/contracts/assigns_enforce_20/test.desc

@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=10$
 ^SIGNAL=0$
-^\[foo.\d+\] line \d+ Check that \*y is assignable: FAILURE$
+^\[foo.\d+\] line \d+ Check that POINTER_OBJECT\((\(.+\))?y\) is assignable: FAILURE$
 ^\[foo.\d+\] line \d+ Check that x is assignable: FAILURE$
 ^VERIFICATION FAILED$
 --

regression/contracts/assigns_enforce_address_of/test.desc

@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: illegal target in assigns clause$
+^.*error: non-lvalue target in assigns clause$
 ^CONVERSION ERROR$
 --
 --

regression/contracts/assigns_enforce_arrays_05/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-contract assigns_ptr --enforce-contract assigns_range
+--enforce-contract assigns_range
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

regression/contracts/assigns_enforce_elvis_4/test.desc

@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: void-typed targets not permitted$
+^.*error: void-typed targets not permitted in assigns clause$
 --
 --
 Check that Elvis operator expressions '*(cond ? if_true : if_false)' with different types in true and false branches are rejected.

regression/contracts/assigns_enforce_function_calls/test.desc

@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: illegal target in assigns clause$
+^.*error: non-lvalue target in assigns clause$
 ^CONVERSION ERROR$
 --
 --

regression/contracts/assigns_enforce_literal/test.desc

@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: illegal target in assigns clause$
+^.*error: non-lvalue target in assigns clause$
 ^CONVERSION ERROR$
 --
 --

regression/contracts/assigns_enforce_side_effects_1/test.desc

@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: void-typed targets not permitted$
+^.*error: void-typed targets not permitted in assigns clause$
 ^CONVERSION ERROR$
 --
 --

regression/contracts/assigns_enforce_side_effects_2/test.desc

@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: illegal target in assigns clause$
+^.*error: non-lvalue target in assigns clause$
 ^CONVERSION ERROR$
 --
 --

regression/contracts/assigns_enforce_side_effects_3/test.desc

@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: illegal target in assigns clause$
+^.*error: non-lvalue target in assigns clause$
 ^CONVERSION ERROR$
 --
 --

regression/contracts/assigns_type_checking_invalid_case_01/test.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=(1|64)$
 ^SIGNAL=0$
 ^CONVERSION ERROR$
-error: illegal target in assigns clause
+error: non-lvalue target in assigns clause
 --
 Checks whether type checking reports illegal target in assigns clause.

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

@@ -18,4 +18,9 @@ to pass -- we should not mistakenly havoc the allocations, just their values.
 However, the `data[1][2][3] == 0` assertion is expected to fail since `data`
 is havoced.
 
-Blocked on issue #6021 -- alias analysis is imprecise and returns `unknown`.
+Blocked on #6326:
+The assigns clause in this case would have an entire 3D space,
+and some of it must be re-established, to the original objects
+but with different values at certain locations, by the loop invariant.
+However, currently we cannot restrict same_object for pointers
+within loop invariants.

regression/contracts/invar_havoc_dynamic_multi-dim_array/test.desc

@@ -17,7 +17,10 @@ void main()
   data[4][5][6] = 0;
 
   for(unsigned i = 0; i < SIZE; i++)
+    // clang-format off
+    __CPROVER_assigns(i, data[4][5][6])
     __CPROVER_loop_invariant(i <= SIZE)
+    // clang-format on
     {
       data[4][5][6] = 1;
     }

regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/main.c

@@ -1,12 +1,14 @@
-KNOWNBUG
+CORE
 main.c
 --apply-loop-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 data\[4\]\[5\]\[6\] == 0: FAILURE$
-^\[main.assertion.2\] .* assertion data\[1\]\[2\]\[3\] == 0: SUCCESS$
+^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main.\d+\] .* Check that i is assignable: SUCCESS$
+^\[main.\d+\] .* Check that data\[(.*)4\]\[(.*)5\]\[(.*)6\] is assignable: SUCCESS$
+^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main.assertion.\d+\] .* assertion data\[4\]\[5\]\[6\] == 0: FAILURE$
+^\[main.assertion.\d+\] .* assertion data\[1\]\[2\]\[3\] == 0: SUCCESS$
 ^VERIFICATION FAILED$
 --
 --
@@ -17,5 +19,3 @@ The `data[4][5][6] == 0` assertion is expected to fail since `data[4][5][6]`
 is havoced and the invariant does not reestablish its value.
 However, the `data[1][2][3] == 0` assertion is expected to pass -- we should
 not havoc the entire `data` array, if only a constant index if being modified.
-
-Blocked on issue #6021 -- alias analysis is imprecise and returns `unknown`.

regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/test.desc

@@ -19,4 +19,9 @@ We _could_ do a more precise analysis in future where we only havoc
 `data[4][5][6]` but not `data[1][2][3]` since the latter clearly cannot be
 modified in the given loop.
 
-Blocked on issue #6021 -- alias analysis is imprecise and returns `unknown`.
+Blocked on #6326:
+The assigns clause in this case would have an entire 2D grid,
+and some of it must be re-established, to the original objects
+but with different values at certain locations, by the loop invariant.
+However, currently we cannot restrict same_object for pointers
+within loop invariants.

regression/contracts/invar_havoc_dynamic_multi-dim_array_partial_const_idx/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

@@ -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, b->data[i])
+    __CPROVER_loop_invariant(i <= SIZE)
+    // clang-format on
+    {
+      b->data[i] = 1;
+    }
+
+  assert(b->data[5] == 0);
+}

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,17 @@
+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$
+^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.

regression/contracts/loop_assigns-03/test.desc

@@ -0,0 +1,41 @@
+#include <assert.h>
+#include <stdlib.h>
+
+#define SIZE 8
+
+struct blob
+{
+  char *data;
+};
+
+void main()
+{
+  int y;
+  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;
+
+      int x;
+      for(unsigned j = 0; j < i; j++)
+        // clang-format off
+        // y is not assignable by outer loop, so this should be flagged
+        __CPROVER_assigns(j, y, x, b->data[i])
+        __CPROVER_loop_invariant(j <= i)
+        // clang-format on
+        {
+          x = b->data[j] * b->data[j];
+          b->data[i] += x;
+          y += j;
+        }
+    }
+
+  assert(b->data[5] == 0);
+}