A new implementation for assigns clauses

regression/contracts/assigns_enforce_18/test.desc

@@ -3,21 +3,18 @@ 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 POINTER_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 POINTER_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$
-^.* 2 of \d+ failed \(\d+ iteration.*\)$
+^\[foo.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)yp\) is assignable: SUCCESS$
 ^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,41 @@
+#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)
+__CPROVER_assigns(__CPROVER_POINTER_OBJECT(b->buf))
+__CPROVER_assigns(__CPROVER_POINTER_OBJECT(value))
+__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,9 @@
+CORE
+main.c
+--enforce-contract foo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+This test checks that POINTER_OBJECT can be used both on arrays and scalars.

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_POINTER_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 POINTER_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 POINTER_OBJECT(ptr).

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);
 }

regression/contracts/assigns_enforce_function_calls/test.desc

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

regression/contracts/assigns_enforce_object_wrong_args/main.c

@@ -0,0 +1,15 @@
+#include <assert.h>
+#include <stdbool.h>
+#include <stdlib.h>
+
+int baz(int *x) __CPROVER_assigns(__CPROVER_POINTER_OBJECT())
+{
+  *x = 0;
+  return 0;
+}
+
+int main()
+{
+  int x;
+  baz(&x);
+}

regression/contracts/assigns_enforce_object_wrong_args/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--enforce-contract baz
+^EXIT=(1|64)$
+^SIGNAL=0$
+^.*error: pointer_object expects one argument$
+^CONVERSION ERROR$
+--
+--
+Check that `__CPROVER_POINTER_OBJECT` in assigns clauses are invoked correctly.

regression/contracts/assigns_enforce_offsets_1/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --enforce-contract foo
 ^EXIT=10$

regression/contracts/assigns_enforce_side_effects_1/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_side_effects_1/test.desc

@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: Assigns clause is not side-effect free.$
+^.*error: void-typed targets not permitted$
 ^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: Assigns clause is not side-effect free.$
+^.*error: illegal 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: Assigns clause is not side-effect free.$
+^.*error: illegal target in assigns clause$
 ^CONVERSION ERROR$
 --
 --

regression/contracts/assigns_enforce_statics/main.c

@@ -0,0 +1,19 @@
+#include <assert.h>
+#include <stdlib.h>
+
+static int x;
+
+void foo() __CPROVER_assigns(x)
+{
+  int *y = &x;
+
+  static int x;
+  x++;
+
+  (*y)++;
+}
+
+int main()
+{
+  foo();
+}

regression/contracts/assigns_enforce_statics/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--enforce-contract foo _ --pointer-primitive-check
+^EXIT=0$
+^SIGNAL=0$
+^\[foo.\d+\] line \d+ Check that y is assignable: SUCCESS$
+^\[foo.\d+\] line \d+ Check that foo\$\$1\$\$x is assignable: SUCCESS$
+^\[foo.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Checks whether static local and global variables are correctly tracked
+in assigns clause verification.

regression/contracts/assigns_enforce_structs_06/main.c

@@ -8,7 +8,7 @@ struct pair
   size_t size;
 };
 
-void f1(struct pair *p) __CPROVER_assigns(*(p->buf))
+void f1(struct pair *p) __CPROVER_assigns(__CPROVER_POINTER_OBJECT(p->buf))
 {
   p->buf[0] = 0;
   p->buf[1] = 1;

regression/contracts/assigns_enforce_structs_07/main.c

@@ -26,11 +26,17 @@ void f2(struct pair_of_pairs *pp) __CPROVER_assigns(*(pp->p->buf))
 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_replace_06/main.c

@@ -1,6 +1,7 @@
 #include <assert.h>
+#include <stdlib.h>
 
-void foo(char c[]) __CPROVER_assigns(c)
+void foo(char c[]) __CPROVER_assigns(__CPROVER_POINTER_OBJECT(c))
 {
 }
 
@@ -28,6 +29,4 @@ int main()
   assert(b[1] == '1');
   assert(b[2] == 'c');
   assert(b[3] == '3');
-
-  return 0;
 }

regression/contracts/assigns_type_checking_valid_cases/main.c

@@ -59,7 +59,7 @@ void foo7(int a, struct buf *buffer) __CPROVER_assigns(*buffer)
   buffer->len = 1;
 }
 
-void foo8(int array[]) __CPROVER_assigns(*array)
+void foo8(int array[]) __CPROVER_assigns(__CPROVER_POINTER_OBJECT(array))
 {
   array[0] = 1;
   array[1] = 1;

regression/contracts/function_check_02/main.c

@@ -6,7 +6,7 @@
 
 // clang-format off
 int initialize(int *arr)
-  __CPROVER_assigns(*arr)
+  __CPROVER_assigns(__CPROVER_POINTER_OBJECT(arr))
   __CPROVER_ensures(
     __CPROVER_forall {
       int i;

regression/contracts/history-pointer-both-01/test.desc

@@ -4,13 +4,8 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
-ASSUME .*::tmp_cc\$\d ≠ NULL
-ASSERT foo::n ≠ NULL
-ASSUME .*::tmp_cc = \*foo::n
-ASSERT .*::tmp_cc\$\d = \*.*::tmp_cc\$\d
 --
 --
-Verification:
 This test checks that history variables are supported for parameters of the
 the function under test. By using the --enforce-contract flag,
 the post-condition (which contains the history variable) is asserted.

regression/contracts/quantifiers-forall-ensures-enforce/main.c

@@ -4,7 +4,7 @@
 
 // clang-format off
 int f1(int *arr, int len)
-  __CPROVER_assigns(*arr)
+  __CPROVER_assigns(__CPROVER_POINTER_OBJECT(arr))
   __CPROVER_ensures(__CPROVER_forall {
     int i;
     // test enforcement with symbolic bound

regression/contracts/quantifiers-nested-01/main.c

@@ -1,6 +1,6 @@
 // clang-format off
 int f1(int *arr)
-  __CPROVER_assigns(*arr)
+  __CPROVER_assigns(__CPROVER_POINTER_OBJECT(arr))
   __CPROVER_ensures(__CPROVER_forall {
     int i;
     __CPROVER_forall

regression/contracts/quantifiers-nested-03/main.c

@@ -1,6 +1,6 @@
 // clang-format off
 int f1(int *arr)
-__CPROVER_assigns(*arr)
+__CPROVER_assigns(__CPROVER_POINTER_OBJECT(arr))
   __CPROVER_ensures(
     __CPROVER_return_value == 0 &&
     __CPROVER_exists {

regression/contracts/test_array_memory_enforce/main.c

@@ -14,7 +14,7 @@ bool return_ok(int ret_value, int *x)
 
 // clang-format off
 int foo(int *x)
-  __CPROVER_assigns(*x)
+  __CPROVER_assigns(__CPROVER_POINTER_OBJECT(x))
   __CPROVER_requires(
     __CPROVER_is_fresh(x, sizeof(int) * 10) &&
     x[0] > 0 &&

regression/contracts/test_struct_member_enforce/main.c

@@ -8,7 +8,7 @@ struct string
 
 // clang-format off
 int foo(struct string *x)
-  __CPROVER_assigns(*(x->str))
+  __CPROVER_assigns(x->str[x->len-1])
   __CPROVER_requires(
     x->len == 128 &&
     __CPROVER_is_fresh(x->str, x->len * sizeof(char)))