Function contracts: check target validity, simplify snapshot instrumentation

regression/contracts/assigns-enforce-malloc-zero/main.c

@@ -6,7 +6,7 @@ int foo(char *a, int size)
   // clang-format off
   __CPROVER_requires(0 <= size && size <= __CPROVER_max_malloc_size)
   __CPROVER_requires(a == NULL || __CPROVER_is_fresh(a, size))
-  __CPROVER_assigns(__CPROVER_POINTER_OBJECT(a))
+  __CPROVER_assigns(a: __CPROVER_POINTER_OBJECT(a))
   __CPROVER_ensures(
     a && __CPROVER_return_value >= 0 ==> a[__CPROVER_return_value] == 0)
 // clang-format on

regression/contracts/assigns_enforce_free_dead/main.c

@@ -1,7 +1,7 @@
 #include <assert.h>
 #include <stdlib.h>
 
-int foo(int *x, int **p) __CPROVER_assigns(*x, *p, **p)
+int foo(int *x, int **p) __CPROVER_assigns(*x; p : *p; p && *p : **p)
 {
   if(p && *p)
     **p = 0;
@@ -44,12 +44,12 @@ int foo(int *x, int **p) __CPROVER_assigns(*x, *p, **p)
     // q goes DEAD here, unconditionally
   }
 
-  free(z);
+  free(z); // should not fail because free(NULL) is allowed in C
 
   z = malloc(sizeof(int));
   if(nondet_bool())
   {
-    free(z);
+    free(z); // should not fail because free(NULL) is allowed in C
     // here z is deallocated, conditionally
   }
 

regression/contracts/assigns_enforce_free_dead/test.desc

@@ -1,8 +1,8 @@
 CORE
 main.c
 --enforce-contract foo _ --malloc-may-fail --malloc-fail-null --pointer-primitive-check
-^\[foo.\d+\] line \d+ Check that \*\(\*p\) is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that \*\(\*p\) is assignable: FAILURE$
+^\[foo.\d+\] line 7 Check that \*\(\*p\) is assignable: SUCCESS$
+^\[foo.\d+\] line 24 Check that \*\(\*p\) is assignable: FAILURE$
 ^\[foo.\d+\] line \d+ Check that \*p is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that \*q is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that \*w is assignable: SUCCESS$

regression/contracts/assigns_enforce_offsets_2/test.desc

@@ -1,10 +1,15 @@
-KNOWNBUG
+CORE
 main.c
---enforce-contract foo
+--enforce-contract foo _ --pointer-check
+^\[.*\d+\].* line 5 Check assigns target validity 'TRUE: \*x': SUCCESS$
+^\[.*\d+\].* line 8 Check that x\[\(.*\)1\] is assignable: (SUCCESS|FAILURE)$
+^\[.*\d+\].* line 8 Check assigns target validity 'TRUE: x\[\(.*\)1\]': FAILURE$
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 --
 --
-Check that a write at *x fails when the assigns clause specifies *(x + 1) and
-the actual underlying object is of size 1.
+Check that a write at *x+1 fails when the assigns clause specifies a valid *x
+and the actual underlying object is of size 1.
+In this case the specified target is valid, the lhs of the assignment is invalid
+so the inclusion check passes, but the pointer check must fail with an OOB.

regression/contracts/assigns_enforce_offsets_4/main.c

@@ -13,8 +13,8 @@ int main()
 {
   int *x = malloc(2 * sizeof(int));
   *x = 0;
-  *(x + 1) == 0
-    // write should fail because x points to a size 2 object and the contracts expects size 10 at least.
-    foo(x);
+  *(x + 1) == 0;
+  // write should fail because x points to a size 2 object and the contracts expects size 10 at least.
+  foo(x);
   return 0;
 }

regression/contracts/assigns_enforce_offsets_4/test.desc

@@ -1,9 +1,13 @@
-KNOWNBUG
+CORE
 main.c
---enforce-contract foo
+--enforce-contract foo _ --pointer-check
+^\[.*\d+\].* line 8 Check assigns target validity 'TRUE: x\[\(.*\)10\]': FAILURE$
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 --
 --
-Check that a write at *x fails when the assigns clause specifies *(x + 1) and the actual underlying object is of size 1.
+Check that a write at *(x+10) fails when the assigns clause specifies *(x + 10)
+and the actual underlying object is too small.
+In that case the target inclusion succeeds because the LHS is in an invalid
+state, but the target validity check must fail.

regression/contracts/assigns_enforce_structs_07/test.desc

@@ -3,13 +3,14 @@ main.c
 --enforce-contract f1 --enforce-contract f2 _ --malloc-may-fail --malloc-fail-null --pointer-check
 ^EXIT=10$
 ^SIGNAL=0$
-^\[f1.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: SUCCESS$
-^\[f1.pointer\_dereference.\d+\] line \d+ dereference failure: pointer invalid in p->buf\[\(.*\)0\]: FAILURE$
-^\[f1.pointer\_dereference.\d+\] line \d+ dereference failure: pointer NULL in p->buf: FAILURE$
-^\[f2.\d+\] line \d+ Check that pp->p->buf\[\(.*\)0\] is assignable: SUCCESS$
-^\[f2.pointer\_dereference.\d+\] line \d+ dereference failure: pointer invalid in pp->p->buf\[\(.*\)0\]: FAILURE$
+^\[f1.*\d+\].*line 18 Check assigns target validity 'TRUE: p->buf\[\(.*\)0\]': FAILURE$
+^\[f2.*\d+\].*line 23 Check assigns target validity 'TRUE: pp->p->buf\[\(.*\)0\]': FAILURE$
 ^VERIFICATION FAILED$
 --
 --
-Checks whether CBMC properly evaluates write set of members
-from invalid objects. In this case, they are not writable.
+In f1, the assigns clause specifies `*(p->buf)` as target (which can be invalid)
+and assigns `p->buf[0]` unconditionally. When both target and lhs are invalid,
+its inclusion check can be trivially satisfied (or not) but we expect the target
+validity check to fail.
+
+In f2 tests this behaviour with chained dereferences.

regression/contracts/assigns_enforce_structs_08/main.c

@@ -0,0 +1,48 @@
+#include <assert.h>
+#include <stdint.h>
+#include <stdlib.h>
+
+struct pair
+{
+  uint8_t *buf;
+  size_t size;
+};
+
+struct pair_of_pairs
+{
+  struct pair *p;
+};
+
+void f1(struct pair *p) __CPROVER_assigns(p && p->buf : *(p->buf))
+{
+  if(p && p->buf)
+    p->buf[0] = 0;
+}
+
+void f2(struct pair_of_pairs *pp)
+  // clang-format off
+__CPROVER_assigns(pp && pp->p && pp->p->buf: *(pp->p->buf))
+// clang-format on
+{
+  if(pp && pp->p && pp->p->buf)
+    pp->p->buf[0] = 0;
+}
+
+int main()
+{
+  struct pair *p = malloc(sizeof(*p));
+  if(p)
+    p->buf = malloc(100 * sizeof(uint8_t));
+  f1(p);
+
+  struct pair_of_pairs *pp = malloc(sizeof(*pp));
+  if(pp)
+  {
+    pp->p = malloc(sizeof(*(pp->p)));
+    if(pp->p)
+      pp->p->buf = malloc(100 * sizeof(uint8_t));
+  }
+  f2(pp);
+
+  return 0;
+}

regression/contracts/assigns_enforce_structs_08/test.desc

@@ -0,0 +1,21 @@
+CORE
+main.c
+--enforce-contract f1 --enforce-contract f2 _ --malloc-may-fail --malloc-fail-null --pointer-check
+^\[f1.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: SUCCESS$
+^\[f2.\d+\] line \d+ Check that pp->p->buf\[\(.*\)0\] is assignable: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^\[f1.pointer\_dereference.\d+\] line \d+ dereference failure: pointer NULL in p->buf: FAILURE$
+^\[f1.pointer\_dereference.\d+\] line \d+ dereference failure: pointer invalid in p->buf\[\(.*\)0\]: FAILURE$
+^\[f2.pointer\_dereference.\d+\] line \d+ dereference failure: pointer NULL in pp->p->buf\[\(.*\)0\]: FAILURE$
+^\[f2.pointer\_dereference.\d+\] line \d+ dereference failure: pointer invalid in pp->p->buf\[\(.*\)0\]: FAILURE$
+--
+In f1, the assigns clause specifies `*(p->buf)` as target (which can be invalid)
+and assigns `p->buf[0]` unconditionally. When both target and lhs are invalid,
+its  inclusion check can be trivially satisfied or not but we expect in all
+cases a  null pointer failure and an invalid pointer error to occur 
+on the assignment.
+
+In f2 tests this behaviour with chained dereferences.

regression/contracts/assigns_enforce_subfunction_calls/test.desc

@@ -4,15 +4,13 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^main.c function baz$
-^\[baz.1\] line \d+ Check that \*x is assignable: SUCCESS$
-^\[baz.2\] line \d+ Check that \*x is assignable: SUCCESS$
-^\[baz.3\] line \d+ Check that \*x is assignable: FAILURE$
-^\[baz.4\] line \d+ Check that \*x is assignable: FAILURE$
+^\[baz.\d+\] line 6 Check that \*x is assignable: SUCCESS$
+^\[baz.\d+\] line 6 Check that \*x is assignable: FAILURE$
 ^main.c function foo$
-^\[foo.assertion.1\] line \d+ foo.x.set: SUCCESS$
-^\[foo.assertion.2\] line \d+ foo.local.set: SUCCESS$
-^\[foo.assertion.3\] line \d+ foo.y.set: SUCCESS$
-^\[foo.assertion.4\] line \d+ foo.z.set: SUCCESS$
+^\[foo.assertion.\d+\] line 20 foo.x.set: SUCCESS$
+^\[foo.assertion.\d+\] line 25 foo.local.set: SUCCESS$
+^\[foo.assertion.\d+\] line 29 foo.y.set: SUCCESS$
+^\[foo.assertion.\d+\] line 33 foo.z.set: SUCCESS$
 ^VERIFICATION FAILED$
 --
 --

regression/contracts/assigns_replace_04/main.c

@@ -1,6 +1,6 @@
 #include <assert.h>
 
-void f2(int *x2, int *y2) __CPROVER_assigns(*x2) __CPROVER_ensures(*x2 > 5)
+void f2(int *x2, int *y2) __CPROVER_assigns(*x2) __CPROVER_ensures(*x2 == 10)
 {
   *x2 = 10;
 }
@@ -28,6 +28,7 @@ int main()
   }
   assert(p > 100);
   assert(q == 2);
+  __CPROVER_assert(0, "reachability test");
 
   return 0;
 }

regression/contracts/assigns_replace_04/test.desc

@@ -1,9 +1,16 @@
 CORE
 main.c
 --replace-call-with-contract f2 --replace-call-with-contract f3
-^EXIT=0$
+main.c function main
+^\[.*\d+\] line 29 assertion p > 100: SUCCESS$
+^\[.*\d+\] line 30 assertion q == 2: SUCCESS$
+^\[.*\d+\] line 31 reachability test: FAILURE$
+^\*\* 1 of 3 failed
+^VERIFICATION FAILED$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
 --
 --
-This test checks that verification succeeds when an assigns clause is combined with a function contract in a loop properly.
+This test checks that replacing function calls with their contracts within a
+loop, when the contracts impose contradictory post conditions at different loop
+iterations on a same program variable, do not cause vacuity.

regression/contracts/assigns_replace_05/main.c

@@ -1,8 +1,8 @@
 #include <assert.h>
 
-void f2(int *x2, int *y2) __CPROVER_assigns(*x2) __CPROVER_ensures(*x2 > 5)
+void f2(int *x2, int *y2) __CPROVER_assigns(*x2) __CPROVER_ensures(*x2 < 5)
 {
-  *x2 = 10;
+  *x2 = 1;
 }
 
 void f3(int *x3, int *y3) __CPROVER_ensures(*x3 > 100)
@@ -26,8 +26,9 @@ int main()
       f3(&p, &q);
     }
   }
-  assert(p > 100);
-  assert(q == 2);
+  assert(p < 0);
+  assert(q == 32);
+  __CPROVER_assert(0, "reachability test");
 
   return 0;
 }

regression/contracts/assigns_replace_05/test.desc

@@ -1,12 +1,16 @@
-KNOWNBUG
+CORE
 main.c
 --replace-call-with-contract f2 --replace-call-with-contract f3
-^EXIT=10$
+main.c function main
+^\[.*\d+\] line 29 assertion p < 0: SUCCESS$
+^\[.*\d+\] line 30 assertion q == 32: SUCCESS$
+^\[.*\d+\] line 31 reachability test: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
 ^SIGNAL=0$
-^VERIFICATION FAILED$
 --
 --
-This test checks that verification fails when assigns clauses are combined with function contracts
-in a loop improperly, i.e., always assumes memory not mention in ensures clauses are unchanged.
-
-BUG: Currently, function call replacement using 'ensures' specifications encodes an implicit assumption that any memory not mentioned in the ensures clause remains unchanged throughout the function, even when an 'assigns' clause is not present.
+This test demonstrates that replacing a function call with a contract that has
+an empty assigns clause and a post condition involving its input parameters can 
+causes vacuous proofs. Checking the contract against the function would fail
+the assigns clause checks. *This is not a bug*.

regression/contracts/loop_contracts_binary_search/test.desc

@@ -6,9 +6,9 @@ main.c
 ^\[binary_search\.\d+\] .* Check loop invariant before entry: SUCCESS$
 ^\[binary_search\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
 ^\[binary_search\.\d+\] .* Check decreases clause on loop iteration: SUCCESS$
-^\[binary_search\.2\] .* Check that lb is assignable: SUCCESS$
-^\[binary_search\.3\] .* Check that ub is assignable: SUCCESS$
-^\[binary_search\.4\] .* Check that mid is assignable: SUCCESS$
+^\[binary_search\.\d+\] .* Check that lb is assignable: SUCCESS$
+^\[binary_search\.\d+\] .* Check that ub is assignable: SUCCESS$
+^\[binary_search\.\d+\] .* Check that mid is assignable: SUCCESS$
 ^\[main\.assertion\.\d+\] .* assertion buf\[idx\] == val: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --

regression/contracts/variant_init_inside_loop/test.desc

@@ -4,10 +4,10 @@ main.c
 ^\[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\.2\] .* Check that i is assignable: SUCCESS$
-^\[main\.overflow\.1\] .* arithmetic overflow on unsigned - in max - i: SUCCESS$
-^\[main\.overflow\.3\] .* arithmetic overflow on unsigned - in max - i: SUCCESS$
-^\[main\.overflow\.2\] .* arithmetic overflow on unsigned \+ in i \+ 1u: SUCCESS$
+^\[main\.\d+\] .* Check that i is assignable: SUCCESS$
+^\[main\.overflow\.\d+\] .* arithmetic overflow on unsigned - in max - i: SUCCESS$
+^\[main\.overflow\.\d+\] .* arithmetic overflow on unsigned - in max - i: SUCCESS$
+^\[main\.overflow\.\d+\] .* arithmetic overflow on unsigned \+ in i \+ 1u: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$