Implementation of assigns clauses based on CARs

This change is a complete rewrite of the assigns clause, based on a new
formalization. Each assigns clause target represents a "conditional
address range" (CAR) that an address range guarded by a validity
constraint.

Author: SaswatPadhi

regression/contracts/assigns_enforce_18/test.desc

@@ -3,21 +3,21 @@ main.c
 --enforce-contract foo --enforce-contract bar --enforce-contract baz _ --pointer-primitive-check
 ^EXIT=10$
 ^SIGNAL=0$
-^\[bar.\d+\] line \d+ Check that \*a is assignable: SUCCESS$
+^\[bar.\d+\] line \d+ Check that __CPROVER_object\(\(void \*\)a\) is assignable: SUCCESS$
 ^\[bar.\d+\] line \d+ Check that \*b is assignable: SUCCESS$
-^\[baz.\d+\] line \d+ Check that \*c is assignable: FAILURE$
+^\[baz.\d+\] line \d+ Check that __CPROVER_object\(\(void \*\)c\) is assignable: FAILURE$
 ^\[baz.\d+\] line \d+ Check that \*a is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that a is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that yp is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that z is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that \*xp is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that y is assignable: FAILURE$
+^\[foo.\d+\] line \d+ Check that __CPROVER_object\(\(void \*\)yp\) is assignable: SUCCESS$
 ^.* 2 of \d+ failed \(\d+ iteration.*\)$
 ^VERIFICATION FAILED$
 --
 ^\[foo.\d+\] line \d+ Check that a is assignable: FAILURE$
 ^\[foo.pointer\_primitives.\d+\] line \d+ deallocated dynamic object in POINTER_OBJECT\(tmp\_cc\$\d+\): FAILURE$
-^.* 3 of \d+ failed (\d+ iterations)$
 --
 Checks whether contract enforcement works with functions that deallocate memory.
 We had problems before when freeing a variable, but still keeping it on

regression/contracts/assigns_enforce_23/main.c

@@ -0,0 +1,46 @@
+#include <stdint.h>
+#include <stdlib.h>
+
+typedef struct
+{
+  uint8_t *buf;
+  size_t size;
+} blob;
+
+void foo(blob *b, uint8_t *value)
+  // clang-format off
+__CPROVER_requires(b->size == 5)
+#if 0
+__CPROVER_assigns(__CPROVER_object(b->buf))
+__CPROVER_assigns(__CPROVER_object(value))
+#else
+__CPROVER_assigns(*(b->buf))
+__CPROVER_assigns(*(value))
+#endif
+__CPROVER_ensures(b->buf[0] == 1)
+__CPROVER_ensures(b->buf[1] == 1)
+__CPROVER_ensures(b->buf[2] == 1)
+__CPROVER_ensures(b->buf[3] == 1)
+__CPROVER_ensures(b->buf[4] == 1)
+// clang-format on
+{
+  b->buf[0] = *value;
+  b->buf[1] = *value;
+  b->buf[2] = *value;
+  b->buf[3] = *value;
+  b->buf[4] = *value;
+
+  *value = 2;
+}
+
+int main()
+{
+  blob b;
+  b.size = 5;
+  b.buf = malloc(b.size * (sizeof(*(b.buf))));
+  uint8_t value = 1;
+
+  foo(&b, &value);
+
+  return 0;
+}

regression/contracts/assigns_enforce_23/test.desc

@@ -0,0 +1,13 @@
+KNOWNBUG
+main.c
+--enforce-contract foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that verification succeeds if only expressions inside the assigns clause are assigned within the function.
+
+Note: For all 'enforce' tests, nothing can be assumed about the return value of the function (as the function call is not replaced at this point).
+
+To make such assumptions would cause verification to fail.

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: Illegal target in assigns clause$
 ^CONVERSION ERROR$
 --
 --

regression/contracts/assigns_enforce_arrays_02/main.c

@@ -1,24 +1,24 @@
 #include <assert.h>
+#include <stdlib.h>
 
-int idx = 4;
+int *arr;
 
-int nextIdx() __CPROVER_assigns(idx)
+void f1(int *a, int len) __CPROVER_assigns(*a)
 {
-  idx++;
-  return idx;
+  a[0] = 0;
+  a[5] = 5;
 }
 
-void f1(int a[], int len) __CPROVER_assigns(*a, idx)
+void f2(int *a, int len) __CPROVER_assigns(__CPROVER_object(a))
 {
-  a[nextIdx()] = 5;
+  a[0] = 0;
+  a[5] = 5;
+  free(a);
 }
 
 int main()
 {
-  int arr[10];
-  f1(arr, 10);
-
-  assert(idx == 5);
-
-  return 0;
+  arr = malloc(100 * sizeof(int));
+  f1(arr, 100);
+  f2(arr, 100);
 }

regression/contracts/assigns_enforce_arrays_02/test.desc

@@ -1,14 +1,15 @@
 CORE
 main.c
---enforce-contract f1 --enforce-contract nextIdx
-^EXIT=0$
+--enforce-contract f1 --enforce-contract f2
+^\[f1.\d+\] line \d+ Check that a\[.*0\] is assignable: SUCCESS$
+^\[f1.\d+\] line \d+ Check that a\[.*5\] is assignable: FAILURE$
+^\[f2.\d+\] line \d+ Check that a\[.*0\] is assignable: SUCCESS$
+^\[f2.\d+\] line \d+ Check that a\[.*5\] is assignable: SUCCESS$
+^\[f2.\d+\] line \d+ Check that __CPROVER_object\(\(void \*\)a\) is assignable: SUCCESS$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
+^VERIFICATION FAILED$
 --
 --
-Checks whether the instrumentation process does not duplicate function calls
-used as part of array-index operations, i.e., if a function call is used in
-the computation of the index of an array assignment, then instrumenting that
-statement with an assigns clause will not result in multiple function calls.
-This test also ensures that assigns clauses correctly check for global
-variables modified by subcalls.
+This test ensures that assigns clauses correctly check for global variables,
+and access using *ptr vs __CPROVER_object(ptr).

regression/contracts/assigns_enforce_elvis_4/main.c

@@ -2,7 +2,7 @@
 #include <stdbool.h>
 #include <stdlib.h>
 
-int foo(bool a, int *x, long *y) __CPROVER_assigns(*(a ? x : y))
+int foo(bool a, int *x, long long *y) __CPROVER_assigns(*(a ? x : y))
 {
   if(a)
   {

regression/contracts/assigns_enforce_elvis_4/test.desc

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

regression/contracts/assigns_enforce_elvis_5/test.desc

@@ -8,3 +8,5 @@ main.c
 --
 Check that Elvis operator expressions of form '(cond ? *if_true : *if_false)'
 are supported in assigns clauses.
+
+BUG: `is_lvalue` in goto is not consistent with `target.get_bool(ID_C_lvalue)`.

regression/contracts/assigns_enforce_function_calls/main.c

@@ -17,5 +17,5 @@ int main()
 {
   int x;
   foo(&x);
-  return 0;
+  baz(&x);
 }