CONTRACTS: Front-end extensions for assigns clauses

Add new functions to specify assignable
targets in assigns clauses:
- add type __CPROVER_assignable_t
- 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 have the
  return type __CPROVER_assignable_t and
  are one of the built-ins.

Author: Remi Delmas

doc/cprover-manual/contracts-assigns.md

@@ -1,50 +1,144 @@
 [CPROVER Manual TOC](../../)
 
-# Assigns Clause
+# Assigns Clauses
 
-## In Function Contracts
+An _assigns_ clause lets the user to specify which memory locations may be
+assigned to by a function or a loop.
 
-### Syntax
+The set of locations described by the contract is the union of the locations
+specified by each of its assigns clauses, or the empty set of no _assigns_
+clause is specified.
+
+The assigns clause may only refer to locations that exist in the calling context
+of the function or before entering the loop, i.e. that are part of the _frame_
+of the function call or loop execution.
+
+Any memory that is locally stack- or heap-allocated during function or loop
+execution is by definition not part of the frame and always assignable by the
+function or the loop.
+
+## Syntax
 
 ```c
-__CPROVER_assigns(*identifier*, ...)
+__CPROVER_assigns(*targets*)
+```
+
+Where targets have the following syntax:
+
+```
+targets ::= conditional-target-group (';' conditional-target-group)* ';'?
+conditional-target-group ::= (condition ':')? target (',' target)*
+target ::= l-value
+        | __CPROVER_typed_target(l-value)
+        | __CPROVER_object_whole(pointer-typed-expression)
+        | __CPROVER_object_from(pointer-typed-expression)
+        | __CPROVER_object_upto(pointer-typed-expression,
+                                unsigned-integer-typed-expression)
 ```
 
-An _assigns_ clause allows the user to specify that a memory location may be written by a function. The set of locations writable by a function is the union of the locations specified by the assigns clauses, or the empty set of no _assigns_ clause is specified. While, in general, an _assigns_ clause could be interpreted with either _writes_ or _modifies_ semantics, this
-design is based on the former. This means that memory not captured by an
-_assigns_ clause must not be written within the given function, even if the
-value(s) therein are not modified.
+We use the _assigns_ interpretation for these locations (as opposed to _modifies_)
+meaning that locations not listed in the contract must not be assigned to
+by the function or the loop, even if they end up holding the same value as they
+held before the function call or before entering the loop.
 
-### Object slice expressions
+### Lvalue targets
 
-The following functions can be used in assigns clause to specify ranges of 
-assignable addresses.
+An l-value target `expr` with a complete type `expr_t` specifies that the range
+ of `sizeof(expr_t)` bytes starting at `&expr` is assignable.
 
-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:
+Similarly, given an l-value 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_size_t __CPROVER_object_from(void *ptr); 
+__CPROVER_assignable_t __CPROVER_typed_target(expr_t expr);
 ```
 
-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:
+To specify assignable memory locations
+that are interpreted as pointers by the program, one must use
+`__CPROVER_assigns(ptr)` or `__CPROVER_assigns(__CPROVER_typed_target(ptr))`.
+
+This is to ensure that during call by contract replacement they will be havoced
+as pointers, in a type directed way. For instance:
 
 ```c
-__CPROVER_size_t __CPROVER_object_slice(void *ptr, __CPROVER_size_t size);
+struct circular_buffer_t {
+  int *first;
+  int *last;
+  int *current;
+}
+
+void step(struct circular_buffer_t *buf)
+// correct
+__CPROVER_assigns(__CPROVER_typed_target(buf->current))
+// not correct
+__CPROVER_assigns(__CPROVER_object_upto(&(buf->current), sizeof(buf->current))
+{
+  if(buf->current == buf->last)
+    buf->current = buf->first;
+  else
+    buf->current += 1;
+}
 ```
 
-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. 
-### Parameters
+### Object slice targets
 
-An _assigns_ clause currently supports simple variable types and their pointers,
-structs, and arrays.  Recursive pointer structures are left to future work, as
-their support would require changes to CBMC's memory model.
+Given a pointer `ptr` pointing into some object `o`,
+`__CPROVER_object_whole(ptr)` specifies that all bytes of the object `o`
+are assignable:
+```c
+__CPROVER_assignable_t __CPROVER_object_whole(void *ptr);
+```
+REMARK: this also includes bytes in the object that are before the address given
+by `ptr`;
+
+
+Given a pointer `ptr` pointing into some object `o`, `__CPROVER_object_from(ptr)`
+specifies that the range of bytes starting from the pointer and until the end of
+the object `o` are assignable:
+```c
+__CPROVER_assignable_t __CPROVER_object_from(void *ptr);
+```
 
+```c
+const size_t SIZE = 100;
+
+void init_slice_all(char *arr)
+__CPROVER_assigns(__CPROVER_object_from(arr))
+{
+  for(size_t i=0; i<SIZE; i++)
+    arr[i] = 0;
+}
+```
+
+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_assignable_t __CPROVER_object_upto(void *ptr, __CPROVER_size_t size);
+```
+
+```c
+const size_t SIZE = 100;
+
+void init_slice_n(char *arr, size_t n)
+__CPROVER_requires(n <= SIZE)
+__CPROVER_assigns(__CPROVER_object_upto(arr, n))
+{
+  for(size_t i=0; i<n; i++)
+    arr[i] = 0;
+}
+```
+### Function parameters
+
+The memory locations storing function parameters values are considered local
+to the function and are hence always assignable.
+
+### Inductive data structures
+Inductive data structures are not supported yet in assigns clauses.
+
+## Examples
 ```c
 /* Examples */
 int err_signal; // Global variable
@@ -59,17 +153,18 @@ int sum(const uint32_t a, const uint32_t b, uint32_t* out)
 __CPROVER_assigns(*out, err_signal)
 ```
 
-### Semantics
+## Semantics
 
 The semantics of an _assigns_ clause of a given function can be understood
-in two contexts: enforcement and replacement.
+in two contexts: contract enforcement and replacement.
 
-#### Enforcement
+### Enforcement
 
-In order to determine whether an _assigns_ clause is a sound abstraction of
-the write set of a function *f*, the body of the function is instrumented with
+In order to determine whether a function (or loop) complies with the _assigns_
+clause of the contract, the body of the function (or loop) is instrumented with
 assertion statements before each statement which may write to memory (e.g., an
-assignment).  These assertions are based on the writable locations identified by the _assigns_ clauses.
+assignment). These assertions check that  the location about to be assigned to
+is among the targets specified by the _assigns_ clauses.
 
 For example, consider the following implementation of `sum` function.
 
@@ -85,8 +180,11 @@ __CPROVER_assigns(*out)
 }
 ```
 
-Assignable variables in the function are just those specified so with
-`__CPROVER_assigns`, together with any local variables.
+Assignable locations for the `sum` function are the locations specified with
+`__CPROVER_assigns`, together with any location storing a function parameter,
+or any location that is locally stack- or heap-allocated as part of function (or loop)
+execution.
+
 In the case of `sum` that is `*out` and `result`.  Each assignment will be
 instrumented with an assertion to check that the target of the assignment
 is one of those options.
@@ -119,30 +217,40 @@ int sum(const uint32_t a, const uint32_t b, uint32_t* out)
 }
 ```
 
-Additionally, the set of assignable target expressions is updated while
-traversing the function body when new memory is allocated.  For example, the
-statement `x = (int *)malloc(sizeof(int))` would create a pointer, stored in
-`x`, to assignable memory. Since the memory is allocated within the current
-function, there is no way an assignment to this memory can affect the memory of
-the calling context.  If memory is allocated for a struct, the subcomponents are
-considered assignable as well.
+### Replacement
 
-Finally, a set of freely-assignable symbols *free* is tracked during the
-traversal of the function body. These are locally-defined variables and formal
-parameters without dereferences.  For example, in a variable declaration `<type>
-x = <initial_value>`, `x` would be added to the *free* set. Assignment statements
-where the left-hand-side is in the *free* set are not instrumented with the above assertions.
+Assuming the _assigns_ clause of the contract correctly captures the set of
+locations assigned to by a function (checked during _contract enforcement_),
+CBMC will use the contract's [Requires \& Ensures Clauses](../../contracts/requires-and-ensures/#replacement),
+and its _assigns clause_ to generate a sound abstraction of the function behaviour from the contract.
 
-#### Replacement
+Given the contract:
+
+```c
+int f(params)
+__CPROVER_requires(R);
+__CPROVER_assigns(A);
+__CPROVER_ensures(E);
+{ ... }
+```
 
-Assuming _assigns_ clauses are a sound abstraction of the write set for
-a given function, CBMC will use the function contract in place of the function
-implementation as described by
-[Requires \& Ensures Clauses](../../contracts/requires-and-ensures/#replacement), and it will add
-non-deterministic assignments for each object listed in the `__CPROVER_assigns`
-clause. Since these objects might be modified by the function, CBMC uses
-non-deterministic assignments to havoc them and restrict their values only by
-assuming the postconditions (i.e., ensures clauses).
+Function calls `f(args)` get replaced with a sequence of instuctions equivalent to:
+
+```c
+// check preconditions
+__CPROVER_assert(R[args/params], "Check f preconditions");
+
+// havoc the assignable targets
+// for each target t1, t2, ... of A[args/params];
+t1 = nondet();
+t2 = nondet();
+...
+// assume post conditions
+__CPROVER_assume(E[args/params]);
+```
+Where `R[args/params]`, `A[args/params]`, `E[args/params]` denote the contract
+clause expressions rewritten by substituting
+function parameters with the argyments passed at the call site.
 
 In our example, consider that a function `foo` may call `sum`.
 
@@ -202,7 +310,3 @@ int foo()
   return rval;
 }
 ```
-
-## In Loop Contracts
-
-TODO: Document `__CPROVER_assigns` for loops.

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
 {
   // 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;
 }