instrument loops per given assigns clauses

SaswatPadhi · SaswatPadhi · commit 49a75bf4286c · 2021-11-23T17:00:41.000Z
diff --git a/regression/contracts/assigns_enforce_arrays_05/test.desc b/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$
diff --git a/regression/contracts/invar_assigns_alias_analysis/test.desc b/regression/contracts/invar_assigns_alias_analysis/test.desc
diff --git a/regression/contracts/invar_assigns_empty/main.c b/regression/contracts/invar_assigns_empty/main.c
@@ -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;
 }
diff --git a/regression/contracts/invar_assigns_empty/test.desc b/regression/contracts/invar_assigns_empty/test.desc
@@ -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$
 --
 --
diff --git a/regression/contracts/invar_assigns_opt/test.desc b/regression/contracts/invar_assigns_opt/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$
 --
 --
diff --git a/regression/contracts/invar_havoc_dynamic_multi-dim_array/test.desc b/regression/contracts/invar_havoc_dynamic_multi-dim_array/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.
diff --git a/regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/main.c b/regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/main.c
@@ -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;
     }
diff --git a/regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/test.desc b/regression/contracts/invar_havoc_dynamic_multi-dim_array_all_const_idx/test.desc
@@ -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`.
diff --git a/regression/contracts/invar_havoc_dynamic_multi-dim_array_partial_const_idx/test.desc b/regression/contracts/invar_havoc_dynamic_multi-dim_array_partial_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.
diff --git a/regression/contracts/loop_assigns-01/main.c b/regression/contracts/loop_assigns-01/main.c
@@ -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);
+}
diff --git a/regression/contracts/loop_assigns-01/test.desc b/regression/contracts/loop_assigns-01/test.desc
@@ -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.
diff --git a/regression/contracts/loop_assigns-02/main.c b/regression/contracts/loop_assigns-02/main.c
@@ -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);
+}
diff --git a/regression/contracts/loop_assigns-02/test.desc b/regression/contracts/loop_assigns-02/test.desc
@@ -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.
diff --git a/regression/contracts/loop_assigns-03/main.c b/regression/contracts/loop_assigns-03/main.c
@@ -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);
+}
diff --git a/regression/contracts/loop_assigns-03/test.desc b/regression/contracts/loop_assigns-03/test.desc
@@ -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.
diff --git a/regression/contracts/loop_assigns-04/main.c b/regression/contracts/loop_assigns-04/main.c
@@ -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);
+}
diff --git a/regression/contracts/loop_assigns-04/test.desc b/regression/contracts/loop_assigns-04/test.desc
@@ -0,0 +1,18 @@
+CORE
+main.c
+--apply-loop-contracts
+^EXIT=10$
+^SIGNAL=0$
+^\[main.\d+\] .* Check that i is assignable: SUCCESS$
+^\[main.\d+\] .* Check that j is assignable: SUCCESS$
+^\[main.\d+\] .* Check that b->data\[(.*)i\] is assignable: SUCCESS$
+^\[main.\d+\] .* Check that y is assignable: 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,
+because `i` is also assigned in the loop and should be marked as assignable.
diff --git a/regression/contracts/loop_assigns-fail/main.c b/regression/contracts/loop_assigns-fail/main.c
@@ -16,7 +16,6 @@ void main()
   b->data[5] = 0;
   for(unsigned i = 0; i < SIZE; i++)
     // clang-format off
-    __CPROVER_assigns(b->data)
     __CPROVER_loop_invariant(i <= SIZE)
     // clang-format on
     {
diff --git a/regression/contracts/loop_assigns-fail/test.desc b/regression/contracts/loop_assigns-fail/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+--apply-loop-contracts
+activate-multi-line-match
+Failed to infer variables being modified by the loop at file main.c line \d+ function main\.\nPlease specify an assigns clause\.\nReason:\nAlias analysis returned UNKNOWN!
+^EXIT=6$
+^SIGNAL=0$
+--
+--
+This test (taken from #6021) shows the need for assigns clauses on loops.
+The alias analysis in this case returns `unknown`.
diff --git a/regression/contracts/variant_missing_invariant_warning/test.desc b/regression/contracts/variant_missing_invariant_warning/test.desc
@@ -1,7 +1,8 @@
 CORE
 main.c
 --apply-loop-contracts
-^The loop at file main.c line 4 function main does not have a loop invariant, but has a decreases clause. Hence, a default loop invariant \('true'\) is being used.$
+activate-multi-line-match
+^The loop at file main.c line 4 function main does not have an invariant.*.\nHence, a default invariant \('true'\) is being used to prove those.$
 ^\[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$
diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp
diff --git a/src/goto-instrument/contracts/contracts.h b/src/goto-instrument/contracts/contracts.h
diff --git a/src/goto-instrument/loop_utils.cpp b/src/goto-instrument/loop_utils.cpp

Original file line number	Diff line number	Diff line change
`@@ -2,14 +2,8 @@`
`2`	`2`
`3`	`3`	`int main()`
`4`	`4`	`{`
`5`		`- int r;`
`6`		`- __CPROVER_assume(r >= 0);`
`7`		`- while(r > 0)`
`8`		`- __CPROVER_assigns() __CPROVER_loop_invariant(r >= 0)`
	`5`	`+ while(1 == 1)`
	`6`	`+ __CPROVER_assigns() __CPROVER_loop_invariant(1 == 1)`
`9`	`7`	`{`
`10`		`- r--;`
`11`	`8`	`}`
`12`		`- assert(r == 0);`
`13`		`-`
`14`		`- return 0;`
`15`	`9`	`}`
Original file line number	Diff line number	Diff line change
`@@ -17,7 +17,10 @@ void main()`
`17`	`17`	`data[4][5][6] = 0;`
`18`	`18`
`19`	`19`	`for(unsigned i = 0; i < SIZE; i++)`
	`20`	`+ // clang-format off`
	`21`	`+ __CPROVER_assigns(i, data[4][5][6])`
`20`	`22`	`__CPROVER_loop_invariant(i <= SIZE)`
	`23`	`+ // clang-format on`
`21`	`24`	`{`
`22`	`25`	`data[4][5][6] = 1;`
`23`	`26`	`}`