CONTRACTS: introduce __CPROVER_assignable_t and related built-in functions

doc/cprover-manual/contracts-assigns.md

@@ -18,25 +18,44 @@ value(s) therein are not modified.
 The following functions can be used in assigns clause to specify ranges of 
 assignable addresses.
 
+Given an lvalue expression `expr` with a complete type `expr_t`,
+ `__CPROVER_typed_target(expr)` specifies that the range 
+ of `sizeof(expr_t)` bytes starting at `&expr` is assignable:
+```c
+__CPROVER_assignable_t __CPROVER_typed_target(expr_t expr);
+```
+
+Given a pointer `ptr` pointing into some object `o`, 
+`__CPROVER_whole_object(ptr)` specifies that all bytes of the object `o`
+are assignable:
+```c
+__CPROVER_assignable_t __CPROVER_whole_object(void *ptr);
+```
+
 Given a pointer `ptr` pointing into some object `o`, `__CPROVER_object_from(ptr)` 
-specifies that all bytes starting from the given pointer and until the end of 
-the object are assignable:
+specifies that the range of bytes starting from the pointer and until the end of 
+the object `o` are assignable:
 ```c
-__CPROVER_size_t __CPROVER_object_from(void *ptr); 
+__CPROVER_assignable_t __CPROVER_object_from(void *ptr);
 ```
 
-Given a pointer `ptr` pointing into some object `o`, `__CPROVER_object_from(ptr, size)` 
-specifies that `size` bytes starting from the given pointer and until the end of the object are assignable.
-The `size` value must such that `size <= __CPROVER_object_size(ptr) - __CPROVER_pointer_offset(ptr)` holds:
+Given a pointer `ptr` pointing into some object `o`, `__CPROVER_object_upto(ptr, size)` 
+specifies that the range of `size` bytes of `o` starting at `ptr` are assignable:
+The `size` value must such that the range does not exceed the object boundary,
+that is, `__CPROVER_object_size(ptr) - __CPROVER_pointer_offset(ptr) >= size` must hold:
 
 ```c
-__CPROVER_size_t __CPROVER_object_slice(void *ptr, __CPROVER_size_t size);
+__CPROVER_assignable_t __CPROVER_object_upto(void *ptr, __CPROVER_size_t size);
 ```
 
-Caveats and limitations: The slices in question must *not*
-be interpreted as pointers by the program. During call-by-contract replacement, 
-`__CPROVER_havoc_slice(ptr, size)` is used to havoc these targets, 
-and `__CPROVER_havoc_slice` does not support havocing pointers. 
+CAVEAT: The ranges specified by `__CPROVER_whole_object`,
+`__CPROVER_object_from` and `__CPROVER_object_upto` must *not*
+be interpreted as pointers by the program. This is because during 
+call-by-contract replacement, `__CPROVER_havoc_slice(ptr, size)` is used to
+havoc these byte ranges, and `__CPROVER_havoc_slice` does not support
+havocing pointers. `__CPROVER_typed_target` must be used to specify targets
+that are pointers.
+
 ### Parameters
 
 An _assigns_ clause currently supports simple variable types and their pointers,

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_whole_object(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-replace.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_whole_object(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/test-enforce.desc

@@ -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-replace.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_enforce_address_of/test.desc

@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$
+^.*error: assigns clause target must be an lvalue or a call to __CPROVER_POINTER_OBJECT or to a function returning __CPROVER_assignable_t$
 ^CONVERSION ERROR$
 --
 --

regression/contracts/assigns_enforce_conditional_non_lvalue_target/test.desc

@@ -1,7 +1,7 @@
 CORE
 main.c
 --enforce-contract foo
-^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$
+^.*error: assigns clause target must be an lvalue or a call to __CPROVER_POINTER_OBJECT or to a function returning __CPROVER_assignable_t$
 ^CONVERSION ERROR
 ^EXIT=(1|64)$
 ^SIGNAL=0$

regression/contracts/assigns_enforce_conditional_non_lvalue_target_list/test.desc

@@ -1,7 +1,7 @@
 CORE
 main.c
 --enforce-contract foo
-^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$
+^.*error: assigns clause target must be an lvalue or a call to __CPROVER_POINTER_OBJECT or to a function returning __CPROVER_assignable_t$
 ^CONVERSION ERROR
 ^EXIT=(1|64)$
 ^SIGNAL=0$

regression/contracts/assigns_enforce_function_calls/test.desc

@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: function calls in assigns clause targets must be to __CPROVER_object_from, __CPROVER_object_slice$
+^.*error: expecting __CPROVER_assignable_t return type for function bar called in assigns clause$
 ^CONVERSION ERROR$
 --
 --

regression/contracts/assigns_enforce_literal/test.desc

@@ -3,7 +3,7 @@ main.c
 --enforce-contract foo
 ^EXIT=(1|64)$
 ^SIGNAL=0$
-^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$
+^.*error: assigns clause target must be an lvalue or a call to __CPROVER_POINTER_OBJECT or to a function returning __CPROVER_assignable_t$
 ^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 target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$
+^.*error: assigns clause target must be an lvalue or a call to __CPROVER_POINTER_OBJECT or to a function returning __CPROVER_assignable_t$
 ^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 target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$
+^.*error: assigns clause target must be an lvalue or a call to __CPROVER_POINTER_OBJECT or to a function returning __CPROVER_assignable_t$
 ^CONVERSION ERROR$
 --
 --

regression/contracts/assigns_type_checking_invalid_case_01/test.desc

@@ -4,6 +4,6 @@ main.c
 ^EXIT=(1|64)$
 ^SIGNAL=0$
 ^CONVERSION ERROR$
-^.*error: assigns clause target must be an lvalue or a __CPROVER_POINTER_OBJECT, __CPROVER_object_from, __CPROVER_object_slice expression$
+^.*error: assigns clause target must be an lvalue or a call to __CPROVER_POINTER_OBJECT or to a function returning __CPROVER_assignable_t$
 --
 Checks whether type checking rejects literal constants in assigns clause.

regression/contracts/cprover-assignable-fail/main.c

@@ -0,0 +1,28 @@
+#include <stdlib.h>
+
+__CPROVER_assignable_t my_write_set(char *arr, size_t size)
+{
+  __CPROVER_assert(
+    !arr || __CPROVER_rw_ok(arr, size), "target null or writable");
+
+  if(arr && size > 0)
+  {
+    __CPROVER_whole_object(arr);
+    __CPROVER_object_upto(arr, size);
+    __CPROVER_object_from(arr);
+    __CPROVER_typed_target(arr[0]);
+  }
+}
+
+void main()
+{
+  size_t size;
+  char *arr;
+  int do_init;
+  if(do_init)
+  {
+    int nondet;
+    arr = nondet ? malloc(size) : NULL;
+  }
+  my_write_set(arr, size);
+}

regression/contracts/cprover-assignable-fail/test.desc

@@ -0,0 +1,26 @@
+CORE
+main.c
+
+^\[my_write_set.assertion.\d+\] .* target null or writable: FAILURE$
+^\[my_write_set.pointer_arithmetic.\d+\] .* pointer arithmetic: pointer NULL in \(char \*\)\(void \*\)arr - POINTER_OFFSET\(\(void \*\)arr\): FAILURE$
+^\[my_write_set.pointer_arithmetic.\d+\] .* pointer arithmetic: pointer invalid in \(char \*\)\(void \*\)arr - POINTER_OFFSET\(\(void \*\)arr\): FAILURE$
+^\[my_write_set.pointer_arithmetic.\d+\] .* pointer arithmetic: deallocated dynamic object in \(char \*\)\(void \*\)arr - POINTER_OFFSET\(\(void \*\)arr\): FAILURE$
+^\[my_write_set.pointer_arithmetic.\d+\] .* pointer arithmetic: dead object in \(char \*\)\(void \*\)arr - POINTER_OFFSET\(\(void \*\)arr\): FAILURE$
+^\[my_write_set.pointer_arithmetic.\d+\] .* pointer arithmetic: pointer outside object bounds in \(char \*\)\(void \*\)arr - POINTER_OFFSET\(\(void \*\)arr\): SUCCESS$
+^\[my_write_set.pointer_arithmetic.\d+\] .* pointer arithmetic: invalid integer address in \(char \*\)\(void \*\)arr - POINTER_OFFSET\(\(void \*\)arr\): SUCCESS$
+^\[my_write_set.overflow.\d+\] .* arithmetic overflow on unsigned - in OBJECT_SIZE\(\(void \*\)arr\) - POINTER_OFFSET\(\(void \*\)arr\): FAILURE$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+CALL __CPROVER_whole_object
+CALL __CPROVER_object_upto
+CALL __CPROVER_object_from
+CALL __CPROVER_typed_target
+--
+This test checks that:
+- the built-in functions used to specify assignable memory locations are
+  supported;
+- that GOTO conversion rewrites calls to __CPROVER_assignable(...) calls;
+- checks for invalid pointers and of overflows in the computations of
+  interval bounds are in place.

regression/contracts/cprover-assignable-pass/main.c

@@ -0,0 +1,24 @@
+#include <stdlib.h>
+
+__CPROVER_assignable_t my_write_set(char *arr, size_t size)
+{
+  __CPROVER_assert(
+    !arr || __CPROVER_rw_ok(arr, size), "target null or writable");
+
+  if(arr && size > 0)
+  {
+    __CPROVER_whole_object(arr);
+    __CPROVER_object_upto(arr, size);
+    __CPROVER_object_from(arr);
+    __CPROVER_typed_target(arr[0]);
+  }
+}
+
+void main()
+{
+  int nondet;
+  size_t size;
+  char *arr;
+  arr = nondet ? malloc(size) : NULL;
+  my_write_set(arr, size);
+}