Function contracts: new method for havocking assigns clause targets

that works when there are dependencies between targets.

We now take a snapshot of the target addresses if they are valid and
havoc them in a second step if they are valid.  Previously we were
havocking targets directly in an arbitrary sequence, and havocking
s->ptr before *(s->ptr) before __CPROVER_POINTER_OBJECT(s->ptr) would
cause spurious errors.

Author: Remi Delmas

regression/contracts/assigns_enforce_21/test.desc

@@ -4,8 +4,8 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 main.c function bar
-^\[bar.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
-^\[bar.\d+\] line \d+ Check that x is assignable: FAILURE$
+^\[bar\.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
+^\[bar\.\d+\] line \d+ Check that x \(assigned by the contract of quz\) is assignable: FAILURE
 ^VERIFICATION FAILED$
 --
 --

regression/contracts/assigns_replace_08/test.desc

@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo --replace-call-with-contract bar _ --pointer-primitive-check
 ^EXIT=10$
 ^SIGNAL=0$
-\[foo.\d+\] line \d+ Check that \*z is assignable: FAILURE$
+\[foo.\d+\] line \d+ Check that \*z \(assigned by the contract of bar\) is assignable: FAILURE$
 ^.* 1 of \d+ failed \(\d+ iteration.*\)$
 ^VERIFICATION FAILED$
 --

regression/contracts/assigns_replace_09/test.desc

@@ -3,7 +3,7 @@ main.c
 --replace-call-with-contract bar --enforce-contract foo
 ^EXIT=0$
 ^SIGNAL=0$
-\[foo.\d+\] line \d+ Check that \*z is assignable: SUCCESS$
+\[foo.\d+\] line \d+ Check that \*z \(assigned by the contract of bar\) is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^Condition: \!not\_found$

regression/contracts/assigns_replace_havoc_dependent_targets_fail/enforce.desc

@@ -0,0 +1,9 @@
+CORE
+main_enforce.c
+--enforce-contract resize_vec _ --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Verifies the contract being replaced in `replace.desc`.

regression/contracts/assigns_replace_havoc_dependent_targets_fail/main_enforce.c

@@ -0,0 +1,9 @@
+#include "vect.h"
+
+int main()
+{
+  vect *v;
+  size_t incr;
+  resize_vec(v, incr);
+  return 0;
+}

regression/contracts/assigns_replace_havoc_dependent_targets_fail/main_replace.c

@@ -0,0 +1,8 @@
+#include "vect.h"
+
+int main()
+{
+  vect *v;
+  resize_vec_incr10(v);
+  return 0;
+}

regression/contracts/assigns_replace_havoc_dependent_targets_fail/replace.desc

@@ -0,0 +1,16 @@
+CORE
+main_replace.c
+--replace-call-with-contract resize_vec --enforce-contract resize_vec_incr10 _ --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check
+^\[.*\] .* Check that v->size \(assigned by the contract of resize_vec\) is assignable: SUCCESS
+^\[.*\] .* Check that v->arr \(assigned by the contract of resize_vec\) is assignable: FAILURE
+^\[.*\] .* Check that POINTER_OBJECT\(\(const void \*\)v->arr\) \(assigned by the contract of resize_vec\) is assignable: FAILURE
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Shows that when an assigns clause contains targets that are dependent, 
+in this case, a pointer variable `v->arr` and
+the object it points to `__CPROVER_POINTER_OBJECT(v->arr)`, we can correctly
+havoc them when replacing the call by the contract.
+In this version of the test the inclusion check must fail.

regression/contracts/assigns_replace_havoc_dependent_targets_fail/vect.h

@@ -0,0 +1,48 @@
+#include <assert.h>
+#include <stdlib.h>
+
+typedef struct vect
+{
+  char *arr;
+  size_t size;
+} vect;
+
+void resize_vec(vect *v, size_t incr)
+  // clang-format off
+__CPROVER_requires(
+  __CPROVER_is_fresh(v, sizeof(vect)) &&
+  0 < v->size && v->size <= __CPROVER_max_malloc_size &&
+  0 < incr && incr < __CPROVER_max_malloc_size - v->size &&
+  __CPROVER_is_fresh(v->arr, v->size)
+)
+__CPROVER_assigns(v->size, v->arr, __CPROVER_POINTER_OBJECT(v->arr))
+__CPROVER_ensures(
+  v->size == __CPROVER_old(v->size) + __CPROVER_old(incr) &&
+  __CPROVER_is_fresh(v->arr, v->size)
+)
+// clang-format on
+{
+  free(v->arr);
+  v->size += incr;
+  v->arr = malloc(v->size);
+  return;
+}
+
+void resize_vec_incr10(vect *v)
+  // clang-format off
+__CPROVER_requires(
+  __CPROVER_is_fresh(v, sizeof(vect)) &&
+  0 < v->size && v->size <= __CPROVER_max_malloc_size &&
+  v->size + 10 < __CPROVER_max_malloc_size &&
+  __CPROVER_is_fresh(v->arr, v->size)
+)
+__CPROVER_assigns(v->size)
+__CPROVER_ensures(
+  v->size == __CPROVER_old(v->size) + 10 &&
+  __CPROVER_is_fresh(v->arr, v->size)
+)
+// clang-format on
+{
+  resize_vec(v, 10);
+  return;
+}

regression/contracts/assigns_replace_havoc_dependent_targets_pass/enforce.desc

@@ -0,0 +1,9 @@
+CORE
+main_enforce.c
+--enforce-contract resize_vec _ --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Verifies the contract being replaced in `replace.desc`.

regression/contracts/assigns_replace_havoc_dependent_targets_pass/main_enforce.c

@@ -0,0 +1,9 @@
+#include "vect.h"
+
+int main()
+{
+  vect *v;
+  size_t incr;
+  resize_vec(v, incr);
+  return 0;
+}