CONTRACTS: Front-end extensions for assigns clauses.

Add new functions to specify assignable
targets in assigns clauses:
- add polymorhpic builtin __CPROVER_typed_target
- add builtin __CPROVER_assignable
- add builtin __CPROVER_object_whole
- add builtin __CPROVER_object_from
- add builtin __CPROVER_object_upto
- allow function call expressions as assigns
  clause targets as long as they are one of
  the new built-ins

Using __CPROVER_POINTER_OBJECT is still allowed (for loop contracts),
will be deprecated in an ulterior PR.

Author: Remi Delmas

doc/cprover-manual/contracts-assigns.md

@@ -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(a: __CPROVER_POINTER_OBJECT(a))
+  __CPROVER_assigns(a: __CPROVER_object_whole(a))
   __CPROVER_ensures(
     a && __CPROVER_return_value >= 0 ==> a[__CPROVER_return_value] == 0)
 // clang-format on

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

@@ -1,7 +1,7 @@
 CORE
 main.c
 --enforce-contract foo _ --malloc-may-fail --malloc-fail-null
-^\[foo.assigns.\d+\] line 9 Check that POINTER_OBJECT\(\(const void \*\)a\) is valid when a != \(\(char \*\)NULL\): SUCCESS$
+^\[foo.assigns.\d+\] line 9 Check that __CPROVER_object_whole\(\(.* \*\)a\) is valid when a != \(\(.* \*\)NULL\): SUCCESS$
 ^\[foo.assigns.\d+\] line 19 Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$
 ^EXIT=0$
 ^SIGNAL=0$

regression/contracts/assigns-enforce-malloc-zero/test.desc

@@ -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_rw_ok(a, size))
-__CPROVER_assigns(__CPROVER_POINTER_OBJECT(a))
+__CPROVER_assigns(__CPROVER_object_whole(a))
 __CPROVER_ensures(
     a && __CPROVER_return_value >= 0 ==> a[__CPROVER_return_value] == 0)
 // clang-format on

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

@@ -7,11 +7,14 @@ struct st
   int c;
 };
 
-void foo(struct st *s)
+void foo(struct st *s, struct st *ss)
   // clang-format off
   __CPROVER_requires(__CPROVER_is_fresh(s, sizeof(*s)))
-  __CPROVER_assigns(__CPROVER_object_slice(s->arr1, 5))
-  __CPROVER_assigns(__CPROVER_object_from(s->arr2 + 5))
+  __CPROVER_assigns(
+    __CPROVER_object_upto(s->arr1, 5);
+    __CPROVER_object_from(s->arr2 + 5);
+    __CPROVER_object_whole(ss);
+)
 // clang-format on
 {
   // PASS
@@ -41,13 +44,24 @@ void foo(struct st *s)
   s->arr2[7] = 0;
   s->arr2[8] = 0;
   s->arr2[9] = 0;
+
+  // PASS
+  ss->a = 0;
+  ss->arr1[0] = 0;
+  ss->arr1[7] = 0;
+  ss->arr1[9] = 0;
+  ss->b = 0;
+  ss->arr2[6] = 0;
+  ss->arr2[8] = 0;
+  ss->c = 0;
 }
 
 int main()
 {
   struct st s;
+  struct st ss;
 
-  foo(&s);
+  foo(&s, &ss);
 
   return 0;
 }

regression/contracts/assigns-slice-targets/main-enforce.c

@@ -7,11 +7,14 @@ struct st
   int c;
 };
 
-void foo(struct st *s)
+void foo(struct st *s, struct st *ss)
   // clang-format off
   __CPROVER_requires(__CPROVER_is_fresh(s, sizeof(*s)))
-  __CPROVER_assigns(__CPROVER_object_slice(s->arr1, 5))
-  __CPROVER_assigns(__CPROVER_object_from(s->arr2 + 5))
+  __CPROVER_assigns(
+    __CPROVER_object_upto(s->arr1, 5);
+    __CPROVER_object_from(s->arr2 + 5);
+    __CPROVER_object_whole(ss);
+  )
 // clang-format on
 {
   s->arr1[0] = 0;
@@ -54,7 +57,32 @@ int main()
   s.arr2[9] = 0;
   s.c = 0;
 
-  foo(&s);
+  struct st ss;
+  ss.a = 0;
+  ss.arr1[0] = 0;
+  ss.arr1[1] = 0;
+  ss.arr1[2] = 0;
+  ss.arr1[3] = 0;
+  ss.arr1[4] = 0;
+  ss.arr1[5] = 0;
+  ss.arr1[6] = 0;
+  ss.arr1[7] = 0;
+  ss.arr1[8] = 0;
+  ss.arr1[9] = 0;
+
+  ss.arr2[0] = 0;
+  ss.arr2[1] = 0;
+  ss.arr2[2] = 0;
+  ss.arr2[3] = 0;
+  ss.arr2[4] = 0;
+  ss.arr2[5] = 0;
+  ss.arr2[6] = 0;
+  ss.arr2[7] = 0;
+  ss.arr2[8] = 0;
+  ss.arr2[9] = 0;
+  ss.c = 0;
+
+  foo(&s, &ss);
 
   // PASS
   assert(s.a == 0);
@@ -92,5 +120,31 @@ int main()
 
   // PASS
   assert(s.c == 0);
+
+  // FAIL
+  assert(ss.a == 0);
+  assert(ss.arr1[0] == 0);
+  assert(ss.arr1[1] == 0);
+  assert(ss.arr1[2] == 0);
+  assert(ss.arr1[3] == 0);
+  assert(ss.arr1[4] == 0);
+  assert(ss.arr1[5] == 0);
+  assert(ss.arr1[6] == 0);
+  assert(ss.arr1[7] == 0);
+  assert(ss.arr1[8] == 0);
+  assert(ss.arr1[9] == 0);
+  assert(ss.b == 0);
+  assert(ss.arr2[0] == 0);
+  assert(ss.arr2[1] == 0);
+  assert(ss.arr2[2] == 0);
+  assert(ss.arr2[3] == 0);
+  assert(ss.arr2[4] == 0);
+  assert(ss.arr2[5] == 0);
+  assert(ss.arr2[6] == 0);
+  assert(ss.arr2[7] == 0);
+  assert(ss.arr2[8] == 0);
+  assert(ss.arr2[9] == 0);
+  assert(ss.c == 0);
+
   return 0;
 }

regression/contracts/assigns-slice-targets/main-replace.c

@@ -1,8 +1,6 @@
 CORE
 main-enforce.c
 --enforce-contract foo
-^\[foo.assigns.\d+\].* Check that __CPROVER_object_slice\(\(void \*\)s->arr1, \(.*\)5\) is valid: SUCCESS$
-^\[foo.assigns.\d+\].* Check that __CPROVER_object_from\(\(void \*\)\(s->arr2 \+ \(.*\)5\)\) is valid: SUCCESS$
 ^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)0\] is assignable: SUCCESS$
 ^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)1\] is assignable: SUCCESS$
 ^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)2\] is assignable: SUCCESS$
@@ -23,6 +21,14 @@ main-enforce.c
 ^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)7\] is assignable: SUCCESS$
 ^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)8\] is assignable: SUCCESS$
 ^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)9\] is assignable: SUCCESS$
+^\[foo.assigns.\d+\].* Check that ss->a is assignable: SUCCESS$
+^\[foo.assigns.\d+\].* Check that ss->arr1\[\(.*\)0\] is assignable: SUCCESS$
+^\[foo.assigns.\d+\].* Check that ss->arr1\[\(.*\)7\] is assignable: SUCCESS$
+^\[foo.assigns.\d+\].* Check that ss->arr1\[\(.*\)9\] is assignable: SUCCESS$
+^\[foo.assigns.\d+\].* Check that ss->b is assignable: SUCCESS$
+^\[foo.assigns.\d+\].* Check that ss->arr2\[\(.*\)6\] is assignable: SUCCESS$
+^\[foo.assigns.\d+\].* Check that ss->arr2\[\(.*\)8\] is assignable: SUCCESS$
+^\[foo.assigns.\d+\].* Check that ss->c is assignable: SUCCESS$
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

regression/contracts/assigns-slice-targets/test-enforce.desc

@@ -24,6 +24,29 @@ main-replace.c
 ^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[\(.*\)8\] == 0: FAILURE$
 ^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[\(.*\)9\] == 0: FAILURE$
 ^\[main.assertion.\d+\].*assertion s.c == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion ss.a == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)0\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)1\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)2\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)3\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)4\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)5\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)6\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)7\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)8\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)9\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion ss.b == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)0\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)1\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)2\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)3\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)4\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)5\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)6\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)7\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)8\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)9\] == 0: FAILURE$
+^\[main.assertion.\d+\].*assertion ss.c == 0: FAILURE$
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$

regression/contracts/assigns-slice-targets/test-replace.desc

@@ -10,8 +10,8 @@ typedef struct
 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_assigns(__CPROVER_object_whole(b->buf))
+__CPROVER_assigns(__CPROVER_object_whole(value))
 __CPROVER_ensures(b->buf[0] == 1)
 __CPROVER_ensures(b->buf[1] == 1)
 __CPROVER_ensures(b->buf[2] == 1)

regression/contracts/assigns_enforce_23/main.c

@@ -6,4 +6,4 @@ main.c
 ^VERIFICATION SUCCESSFUL$
 --
 --
-This test checks that POINTER_OBJECT can be used both on arrays and scalars.
+This test checks that __CPROVER_object_whole can be used both on arrays and scalars.