diff --git a/doc/cprover-manual/contracts-assigns.md b/doc/cprover-manual/contracts-assigns.md index 3c9a3048cc8..2ed3a226ed7 100644 --- a/doc/cprover-manual/contracts-assigns.md +++ b/doc/cprover-manual/contracts-assigns.md @@ -1,75 +1,373 @@ [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 +Knowing the memory footprint of a function contract or a loop contract in turn +allows us to replace a function call or a loop by an nondeterministic +approximation in which assignable locations are havoced. To make sure this +approximation is sound and is an actual abstraction of the original function +call or loop, we need to verify that the actual function or loop never assigns +memory locations not listed in the clause. + +For a function contract, if no assigns clause is provided, the default is the +empty set. For a loop contract, if no assigns clause is provided, CBMC attempts +to infer the set of locations assigned by the loop from the loop body, +and then checks that the inferred set is correct (as if specified by the user). + +For both functions and loop contracts, if more than one assigns clause is +provided, their contents are unioned into a single clause. + +We use the _assigns_ interpretation for these memory locations, which means that +memory locations that are not listed in the assigns clause +(or the _inferred_ assigns clause for a loop 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). + +Memory locations that are locally stack- or heap-allocated during function +execution or loop execution can always be assigned to by the function or the +loop. + +## Syntax ```c -__CPROVER_assigns(*identifier*, ...) +__CPROVER_assigns(targets) +``` + +Where `targets` has the following syntax: + +``` +targets ::= cond-target-group (';' cond-target-group)* ';'? +cond-target-group ::= (condition ':')? target (',' target)* +target ::= lvalue-expr + | __CPROVER_typed_target(lvalue-expr) + | __CPROVER_object_whole(ptr-expr) + | __CPROVER_object_from(ptr-expr) + | __CPROVER_object_upto(ptr-expr, uint-expr) ``` -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. -### Object slice expressions +For function contracts, the condition and target expressions +in the assigns clause may only involve function parameters, +global variables or type identifiers (in `sizeof` or cast expressions). +The target expression must be free of function calls and side-effects. +The condition expression may contain calls to side-effect-free functions. + +For a loop contract, the condition and target expressions in the assigns clause +may involve any identifier that is in scope at loop entry +(parameters of the surrounding function, local variables, global variables, +type identifiers in `sizeof` or cast expressions, etc.). +The target expression must be free of function calls and side-effects. +The condition expression may contain calls to side-effect-free functions. + +### Lvalue targets + +Roughly speaking, _lvalues_ are expressions that are associated with a memory +location, the address of which can be computed using the address-of operator +`&`. + +Examples of lvalues are: `x` if `x` is either a global or local variable +identifier, `*ptr` if `ptr` is a pointer expression, `ptr[i]` or `ptr + i` if +`ptr` is pointer variable or an array and `i` is an integer expression, etc. + +Examples of non-lvalues: literal constants like `0`, `1`, ..., arithmetic +expressions like `x + y` when `x` and `y` are both arithmetic variables, +function pointer expressions, etc. -The following functions can be used in assigns clause to specify ranges of -assignable addresses. +An lvalue target `expr` with a complete type `expr_t` specifies that the range +starting at `&expr` and of size `sizeof(expr_t)` bytes is assignable. + +Lvalues can also be wrapped in `__CPROVER_typed_target` with the same +meaning: for an lvalue `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: -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: ```c -__CPROVER_size_t __CPROVER_object_from(void *ptr); +void __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: +In order to specify that a memory location the contents of which is interpreted +as a pointer by the program is assignable, one must use the notation +`__CPROVER_assigns(ptr)` or the equivalent +`__CPROVER_assigns(__CPROVER_typed_target(ptr))`, as opposed to the slice +operators `__CPROVER_object_whole`, `__CPROVER_object_from`, +or `__CPROVER_object_upto`. +This ensures that during call-by-contract replacement the memory location gets +turned into a non-deterministic pointer. + +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 + +```c +void __CPROVER_object_upto(void *ptr, __CPROVER_size_t size); +``` + +Given a pointer `ptr` pointing into some object (possibly at some non-zero offset), +`__CPROVER_object_upto(ptr, size)` specifies that the range of `size` bytes starting +at `ptr` is assignable. -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. + +The value of `size` must such that the range does not exceed +the object's boundary, i.e. +`size <= __CPROVER_OBJECT_SIZE(ptr) - __CPROVER_POINTER_OFFSET(ptr)` must hold +(otherwise an assertion violation will occur and make the whole analysis fail). + +In the example below, the `struct vect_t`, its `data` array and an exta hidden +byte are packed together in a single object by the `vec_alloc` function. +The `vec_clear` function can only assign `vec->size` bytes starting from +`vec->data`. As a result the assignments to `vec->size` and the hidden byte +fail the verification. ```c -/* Examples */ -int err_signal; // Global variable +#include -int sum(const uint32_t a, const uint32_t b, uint32_t* out) -__CPROVER_assigns(*out) +#define MAX_SIZE 10 -int sum(const uint32_t a, const uint32_t b, uint32_t* out) -__CPROVER_assigns(err_signal) +struct vec_t { + size_t size; + char *data; +}; -int sum(const uint32_t a, const uint32_t b, uint32_t* out) -__CPROVER_assigns(*out, err_signal) +// Allocates a vect_t struct together with its data and a hidden byte +// in a same object. +struct vec_t *vec_alloc(size_t size) { + + if(size > MAX_SIZE) + size = MAX_SIZE; + + // allocate the struct + data + 1 extra hidden byte + struct vec_t *vec = malloc(sizeof(struct vec_t) + size + 1); + if (vec) { + vec->size = size; + vec->data = ((char *)vec) + sizeof(struct vec_t); + } + return vec; +} + +// Clear the vec->data array +void vec_clear(struct vec_t *vec) + __CPROVER_assigns( + vec && vec->data: __CPROVER_object_upto(vec->data, vec->size)) +{ + if (!vec) + return; + + vec->size = vec->size; // FAILURE + + for (size_t i = 0; i < vec->size; i++) + vec->data[i] = 0; // SUCCESS + + char *hidden_byte = ((char *)vec + sizeof(*vec) + vec->size); + *hidden_byte = 0; // FAILURE +} + +// Proof harness +int main() { + size_t size; + struct vec_t *vec = vec_alloc(size); + vec_clear(vec); +} +``` + +--- + +```c +void __CPROVER_object_from(void *ptr); +``` + +Given a pointer `ptr` pointing into some object (possibly at some non-zero offset), +`__CPROVER_object_from(ptr)` specifies that the range of bytes starting at `ptr` +and of size `__CPROVER_OBJECT_SIZE(ptr) - __CPROVER_POINTER_OFFSET(ptr)` is assignable. + +Revisiting our previous example, changing the target to +`__CPROVER_object_from(vec->data)` still rejects the assignment to `vec->size`, +but allows the assignment to the hidden byte which is located after the data +array in memory. + +```c +#include + +#define MAX_SIZE 10 + +struct vec_t { + size_t size; + char *data; +}; + +// Allocates a vect_t struct together with its data and a hidden byte +// in a same object. +struct vec_t *vec_alloc(size_t size) { + + if(size > MAX_SIZE) + size = MAX_SIZE; + + // allocate the struct + data + 1 extra hidden byte + struct vec_t *vec = malloc(sizeof(struct vec_t) + size + 1); + if (vec) { + vec->size = size; + vec->data = ((char *)vec) + sizeof(struct vec_t); + } + return vec; +} + +// Clear the vec->data array +void vec_clear(struct vec_t *vec) + __CPROVER_assigns( + vec && vec->data: __CPROVER_object_from(vec->data)) +{ + if (!vec) + return; + + vec->size = vec->size; // FAILURE + + for (size_t i = 0; i < vec->size; i++) + vec->data[i] = 0; // SUCCESS + + char *hidden_byte = ((char *)vec + sizeof(*vec) + vec->size); + *hidden_byte = 0; // SUCCESS +} + +// Proof harness +int main() { + size_t size; + struct vec_t *vec = vec_alloc(size); + vec_clear(vec); +} +``` +--- + +```c +void __CPROVER_object_whole(void *ptr); ``` -### Semantics +Given a pointer `ptr` pointing into some object (possibly at some non-zero offset), +`__CPROVER_object_whole(ptr)` specifies that the range of bytes of size +`__CPROVER_OBJECT_SIZE(ptr)` starting at address +`ptr - __CPROVER_POINTER_OFFSET(ptr)` is assignable: -The semantics of an _assigns_ clause of a given function can be understood -in two contexts: enforcement and replacement. +If the pointer has a positive offset into some object, the range includes +bytes that are in the object before the address pointed to by `ptr`. +Revisiting our example one last time, changing the target to +`__CPROVER_object_whole(vec->data)` allows the function (perhaps mistakenly) +to assign to `vec->size`, the whole array of size `vec->size` pointed to by +`vec->data` and the hidden byte. -#### Enforcement +```c +#include + +#define MAX_SIZE 10 + +struct vec_t { + size_t size; + char *data; +}; + +// Allocates a vect_t struct together with its data and a hidden byte +// in a same object. +struct vec_t *vec_alloc(size_t size) { + + if(size > MAX_SIZE) + size = MAX_SIZE; + + // allocate the struct + data + 1 extra hidden byte + struct vec_t *vec = malloc(sizeof(struct vec_t) + size + 1); + if (vec) { + vec->size = size; + vec->data = ((char *)vec) + sizeof(struct vec_t); + } + return vec; +} + +// Clear the vec->data array +void vec_clear(struct vec_t *vec) + __CPROVER_assigns( + vec && vec->data: __CPROVER_object_whole(vec->data)) +{ + if (!vec) + return; + + vec->size = vec->size; // SUCCESS + + for (size_t i = 0; i < vec->size; i++) + vec->data[i] = 0; // SUCCESS + + char *hidden_byte = ((char *)vec + sizeof(*vec) + vec->size); + *hidden_byte = 0; // SUCCESS +} -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 +// Proof harness +int main() { + size_t size; + struct vec_t *vec = vec_alloc(size); + vec_clear(vec); +} +``` +### Function parameters + +For a function contract, the memory locations storing function parameters are +considered as being local to the function and are hence always assignable. + +For a loop contract, the parameters of the enclosing function are not considered +local to the loop and must be explicitly added to the loop to become assignable. +### Inductive data structures +Inductive data structures are not supported yet in assigns clauses. + +## Semantics + +Each target listed in an assigns clause defines a +_conditionally assignable range_ of bytes represented by the following triple: + +```c +struct { + void *start_address; + size_t size; + bool is_writable; +} +``` + +where: +- `start_address` is the start address of the range of bytes, +- `size` is the size of the range in number of bytes, +- `is_writable` is true iff the target's `condition` holds and + `__CPROVER_w_ok(start_address, size)` holds at the program location + where the clause is interpreted: right before function invocation for + function contracts and at loop entry for loops; + +For contract enforcement, assigns clause targets are turned into checks, +to verify that the function only assigns locations allowed by the assigns clause. + +For contract replacement, assigns clause targets are turned into havoc statements, +to model the non-deterministic behaviour specified by the contract. +### Contract Enforcement + +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 +383,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 +420,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. +### Contract 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 ` -x = `, `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: -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). +```c +int f(params) +__CPROVER_requires(R); +__CPROVER_assigns(A); +__CPROVER_ensures(E); +{ ... } +``` + +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`. @@ -168,7 +479,7 @@ int foo() uint32_t b; uint32_t out; int rval = sum(a, b, &out); - if (rval == SUCCESS) + if (rval == SUCCESS) return out; return rval; } @@ -183,26 +494,22 @@ int foo() uint32_t a; uint32_t b; uint32_t out; - + /* Function Contract Replacement */ /* Precondition */ __CPROVER_assert(__CPROVER_is_fresh(out, sizeof(*out)), "Check requires clause"); - + /* Writable Set */ *(&out) = nondet_uint32_t(); - + /* Postconditions */ int return_value_sum = nondet_int(); __CPROVER_assume(return_value_sum == SUCCESS || return_value_sum == FAILURE); __CPROVER_assume((return_value_sum == SUCCESS) ==> (*out == (a + b))); int rval = return_value_sum; - if (rval == SUCCESS) + if (rval == SUCCESS) return out; return rval; } ``` - -## In Loop Contracts - -TODO: Document `__CPROVER_assigns` for loops. diff --git a/regression/contracts/assigns-enforce-malloc-zero/main.c b/regression/contracts/assigns-enforce-malloc-zero/main.c index 9592997ddd5..61f105f8a43 100644 --- a/regression/contracts/assigns-enforce-malloc-zero/main.c +++ b/regression/contracts/assigns-enforce-malloc-zero/main.c @@ -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 diff --git a/regression/contracts/assigns-enforce-malloc-zero/test.desc b/regression/contracts/assigns-enforce-malloc-zero/test.desc index eefba72ce5b..43dcf8ef277 100644 --- a/regression/contracts/assigns-enforce-malloc-zero/test.desc +++ b/regression/contracts/assigns-enforce-malloc-zero/test.desc @@ -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$ diff --git a/regression/contracts/assigns-replace-malloc-zero/main.c b/regression/contracts/assigns-replace-malloc-zero/main.c index 14c34366a18..444b33ce29f 100644 --- a/regression/contracts/assigns-replace-malloc-zero/main.c +++ b/regression/contracts/assigns-replace-malloc-zero/main.c @@ -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 diff --git a/regression/contracts/assigns-slice-targets/main-enforce.c b/regression/contracts/assigns-slice-targets/main-enforce.c index 7f39d6f06cd..115573b17a4 100644 --- a/regression/contracts/assigns-slice-targets/main-enforce.c +++ b/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; } diff --git a/regression/contracts/assigns-slice-targets/main-replace.c b/regression/contracts/assigns-slice-targets/main-replace.c index 5f21100ee7c..79d73588cc0 100644 --- a/regression/contracts/assigns-slice-targets/main-replace.c +++ b/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_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; } diff --git a/regression/contracts/assigns-slice-targets/test-enforce.desc b/regression/contracts/assigns-slice-targets/test-enforce.desc index 5b8f4fe5f58..d7c221d1a86 100644 --- a/regression/contracts/assigns-slice-targets/test-enforce.desc +++ b/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$ diff --git a/regression/contracts/assigns-slice-targets/test-replace.desc b/regression/contracts/assigns-slice-targets/test-replace.desc index 1f23fb0ae7e..1c7532841a1 100644 --- a/regression/contracts/assigns-slice-targets/test-replace.desc +++ b/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$ diff --git a/regression/contracts/assigns_enforce_23/main.c b/regression/contracts/assigns_enforce_23/main.c index 9c346ec0f68..1dba3cfb6da 100644 --- a/regression/contracts/assigns_enforce_23/main.c +++ b/regression/contracts/assigns_enforce_23/main.c @@ -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) diff --git a/regression/contracts/assigns_enforce_23/test.desc b/regression/contracts/assigns_enforce_23/test.desc index b06d561e188..be44bf08381 100644 --- a/regression/contracts/assigns_enforce_23/test.desc +++ b/regression/contracts/assigns_enforce_23/test.desc @@ -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. diff --git a/regression/contracts/assigns_enforce_address_of/test.desc b/regression/contracts/assigns_enforce_address_of/test.desc index 7500be4b1e4..6976ec2df0a 100644 --- a/regression/contracts/assigns_enforce_address_of/test.desc +++ b/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 a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$ ^CONVERSION ERROR$ -- -- diff --git a/regression/contracts/assigns_enforce_arrays_02/main.c b/regression/contracts/assigns_enforce_arrays_02/main.c index de5a2797aec..739bf7ae0e7 100644 --- a/regression/contracts/assigns_enforce_arrays_02/main.c +++ b/regression/contracts/assigns_enforce_arrays_02/main.c @@ -9,7 +9,7 @@ void f1(int *a, int len) __CPROVER_assigns(*a) a[5] = 5; } -void f2(int *a, int len) __CPROVER_assigns(__CPROVER_POINTER_OBJECT(a)) +void f2(int *a, int len) __CPROVER_assigns(__CPROVER_object_whole(a)) { a[0] = 0; a[5] = 5; diff --git a/regression/contracts/assigns_enforce_arrays_02/test.desc b/regression/contracts/assigns_enforce_arrays_02/test.desc index d4bd5df0a94..7476de365ce 100644 --- a/regression/contracts/assigns_enforce_arrays_02/test.desc +++ b/regression/contracts/assigns_enforce_arrays_02/test.desc @@ -4,14 +4,14 @@ main.c ^\[f1.assigns.\d+\] line 6 Check that \*a is valid: SUCCESS$ ^\[f1.assigns.\d+\] line 8 Check that a\[.*0\] is assignable: SUCCESS$ ^\[f1.assigns.\d+\] line 9 Check that a\[.*5\] is assignable: FAILURE$ -^\[f2.assigns.\d+\] line 12 Check that POINTER_OBJECT\(\(const void \*\)a\) is valid: SUCCESS$ +^\[f2.assigns.\d+\] line 12 Check that __CPROVER_object_whole\(\(.* \*\)a\) is valid: SUCCESS$ ^\[f2.assigns.\d+\] line 14 Check that a\[.*0\] is assignable: SUCCESS$ ^\[f2.assigns.\d+\] line 15 Check that a\[.*5\] is assignable: SUCCESS$ -^\[f2.assigns.\d+\] line 16 Check that POINTER_OBJECT\(\(void \*\)a\) is assignable: SUCCESS$ +^\[f2.assigns.\d+\] line 16 Check that POINTER_OBJECT\(\(.* \*\)a\) is assignable: SUCCESS$ ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -- -- This test ensures that assigns clauses correctly check for global variables, -and access using *ptr vs POINTER_OBJECT(ptr). +and access using *ptr vs __CPROVER_object_whole(ptr). diff --git a/regression/contracts/assigns_enforce_arrays_04/main.c b/regression/contracts/assigns_enforce_arrays_04/main.c index bf4d22fa028..0ac8d6f93a6 100644 --- a/regression/contracts/assigns_enforce_arrays_04/main.c +++ b/regression/contracts/assigns_enforce_arrays_04/main.c @@ -5,8 +5,7 @@ void assigns_single(int a[], int len) a[i] = 0; } -void uses_assigns(int a[], int len) - __CPROVER_assigns(__CPROVER_POINTER_OBJECT(a)) +void uses_assigns(int a[], int len) __CPROVER_assigns(__CPROVER_object_whole(a)) { assigns_single(a, len); } diff --git a/regression/contracts/assigns_enforce_conditional_non_lvalue_target/test.desc b/regression/contracts/assigns_enforce_conditional_non_lvalue_target/test.desc index 2a9141844c9..3a80f654b3b 100644 --- a/regression/contracts/assigns_enforce_conditional_non_lvalue_target/test.desc +++ b/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 a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$ ^CONVERSION ERROR ^EXIT=(1|64)$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns_enforce_conditional_non_lvalue_target_list/test.desc b/regression/contracts/assigns_enforce_conditional_non_lvalue_target_list/test.desc index 2a9141844c9..3a80f654b3b 100644 --- a/regression/contracts/assigns_enforce_conditional_non_lvalue_target_list/test.desc +++ b/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 a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$ ^CONVERSION ERROR ^EXIT=(1|64)$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns_enforce_conditional_pointer_object/main.c b/regression/contracts/assigns_enforce_conditional_pointer_object/main.c index bbf00141986..27857e726a9 100644 --- a/regression/contracts/assigns_enforce_conditional_pointer_object/main.c +++ b/regression/contracts/assigns_enforce_conditional_pointer_object/main.c @@ -3,8 +3,8 @@ int foo(bool a, char *x, char *y) // clang-format off __CPROVER_assigns( - a: __CPROVER_POINTER_OBJECT(x); - !a: __CPROVER_POINTER_OBJECT(y); + a: __CPROVER_object_whole(x); + !a: __CPROVER_object_whole(y); ) // clang-format on { diff --git a/regression/contracts/assigns_enforce_conditional_pointer_object/test.desc b/regression/contracts/assigns_enforce_conditional_pointer_object/test.desc index c46143c5847..59513d2907f 100644 --- a/regression/contracts/assigns_enforce_conditional_pointer_object/test.desc +++ b/regression/contracts/assigns_enforce_conditional_pointer_object/test.desc @@ -2,8 +2,8 @@ CORE main.c --enforce-contract foo main.c function foo -^\[foo.assigns.\d+\] line 6 Check that POINTER_OBJECT\(\(const void \*\)x\) is valid when a != FALSE: SUCCESS$ -^\[foo.assigns.\d+\] line 7 Check that POINTER_OBJECT\(\(const void \*\)y\) is valid when !\(a != FALSE\): SUCCESS$ +^\[foo.assigns.\d+\] line 6 Check that __CPROVER_object_whole\(\(.* \*\)x\) is valid when a != FALSE: SUCCESS$ +^\[foo.assigns.\d+\] line 7 Check that __CPROVER_object_whole\(\(.* \*\)y\) is valid when !\(a != FALSE\): SUCCESS$ ^\[foo.assigns.\d+\] line 13 Check that x\[\(signed (long )?long int\)0\] is assignable: SUCCESS$ ^\[foo.assigns.\d+\] line 14 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$ ^\[foo.assigns.\d+\] line 18 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$ @@ -15,5 +15,5 @@ main.c function foo ^SIGNAL=0$ -- -- -Check that conditional assigns clause `c ? __CPROVER_POINTER_OBJECT((p)` +Check that conditional assigns clause `c ? __CPROVER_object_whole((p)` match with control flow path conditions. diff --git a/regression/contracts/assigns_enforce_conditional_pointer_object_list/main.c b/regression/contracts/assigns_enforce_conditional_pointer_object_list/main.c index d8cd1db323e..cc6cd3df511 100644 --- a/regression/contracts/assigns_enforce_conditional_pointer_object_list/main.c +++ b/regression/contracts/assigns_enforce_conditional_pointer_object_list/main.c @@ -3,7 +3,7 @@ int foo(bool a, char *x, char *y) // clang-format off __CPROVER_assigns( - a : __CPROVER_POINTER_OBJECT(x), __CPROVER_POINTER_OBJECT(y) + a : __CPROVER_object_whole(x), __CPROVER_object_whole(y) ) // clang-format on { diff --git a/regression/contracts/assigns_enforce_conditional_pointer_object_list/test.desc b/regression/contracts/assigns_enforce_conditional_pointer_object_list/test.desc index 96fe0be031c..954c6a0cc92 100644 --- a/regression/contracts/assigns_enforce_conditional_pointer_object_list/test.desc +++ b/regression/contracts/assigns_enforce_conditional_pointer_object_list/test.desc @@ -2,8 +2,8 @@ CORE main.c --enforce-contract foo main.c function foo -^\[foo.assigns.\d+\] line 6 Check that POINTER_OBJECT\(\(const void \*\)x\) is valid when a != FALSE: SUCCESS$ -^\[foo.assigns.\d+\] line 6 Check that POINTER_OBJECT\(\(const void \*\)y\) is valid when a != FALSE: SUCCESS$ +^\[foo.assigns.\d+\] line 6 Check that __CPROVER_object_whole\(\(.*\)x\) is valid when a != FALSE: SUCCESS$ +^\[foo.assigns.\d+\] line 6 Check that __CPROVER_object_whole\(\(.*\)y\) is valid when a != FALSE: SUCCESS$ ^\[foo.assigns.\d+\] line 12 Check that x\[\(signed (long )?long int\)0\] is assignable: SUCCESS$ ^\[foo.assigns.\d+\] line 13 Check that y\[\(signed (long )?long int\)0\] is assignable: SUCCESS$ ^\[foo.assigns.\d+\] line 17 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$ diff --git a/regression/contracts/assigns_enforce_conditional_unions/main.c b/regression/contracts/assigns_enforce_conditional_unions/main.c index bbbf480132b..ca7223a91e1 100644 --- a/regression/contracts/assigns_enforce_conditional_unions/main.c +++ b/regression/contracts/assigns_enforce_conditional_unions/main.c @@ -70,10 +70,10 @@ __CPROVER_requires( sizeof(*(state->digest.high_level.second.ctx->digest)))) __CPROVER_assigns( is_high_level(): - __CPROVER_POINTER_OBJECT(state->digest.high_level.first.ctx->digest), + __CPROVER_object_whole(state->digest.high_level.first.ctx->digest), state->digest.high_level.first.ctx->flags; is_high_level() && also_second: - __CPROVER_POINTER_OBJECT(state->digest.high_level.second.ctx->digest), + __CPROVER_object_whole(state->digest.high_level.second.ctx->digest), state->digest.high_level.second.ctx->flags; ) // clang-format on diff --git a/regression/contracts/assigns_enforce_conditional_unions/test.desc b/regression/contracts/assigns_enforce_conditional_unions/test.desc index 13bc223c0b6..2e5c41421aa 100644 --- a/regression/contracts/assigns_enforce_conditional_unions/test.desc +++ b/regression/contracts/assigns_enforce_conditional_unions/test.desc @@ -1,9 +1,9 @@ CORE main.c --enforce-contract update _ --pointer-check --pointer-overflow-check --signed-overflow-check --unsigned-overflow-check --conversion-check -^\[update.assigns.\d+] line 73 Check that POINTER_OBJECT\(\(const void \*\)state->digest.high_level.first.ctx->digest\) is valid when .*: SUCCESS +^\[update.assigns.\d+] line 73 Check that __CPROVER_object_whole\(\(.*\)state->digest.high_level.first.ctx->digest\) is valid when .*: SUCCESS ^\[update.assigns.\d+] line 74 Check that state->digest.high_level.first.ctx->flags is valid when .*: SUCCESS -^\[update.assigns.\d+] line 76 Check that POINTER_OBJECT\(\(const void \*\)state->digest.high_level.second.ctx->digest\) is valid when .*: SUCCESS +^\[update.assigns.\d+] line 76 Check that __CPROVER_object_whole\(\(.*\)state->digest.high_level.second.ctx->digest\) is valid when .*: SUCCESS ^\[update.assigns.\d+] line 77 Check that state->digest.high_level.second.ctx->flags is valid when .*: SUCCESS ^\[is_high_level.assigns.\d+\] line 50 Check that latch is assignable: SUCCESS$ ^\[is_high_level.assigns.\d+\] line 51 Check that once is assignable: SUCCESS$ diff --git a/regression/contracts/assigns_enforce_conditional_void_target/test.desc b/regression/contracts/assigns_enforce_conditional_void_target/test.desc index 14f7eb2f2ba..23d56a07949 100644 --- a/regression/contracts/assigns_enforce_conditional_void_target/test.desc +++ b/regression/contracts/assigns_enforce_conditional_void_target/test.desc @@ -1,7 +1,7 @@ CORE main.c --enforce-contract foo -^.* error: (void-typed expressions not allowed as assigns clause targets|dereferencing void pointer)$ +^.* error: (dereferencing void pointer|lvalue expressions with void type not allowed in assigns clauses)$ ^CONVERSION ERROR$ ^EXIT=(1|64)$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns_enforce_conditional_void_target_list/test.desc b/regression/contracts/assigns_enforce_conditional_void_target_list/test.desc index 14f7eb2f2ba..23d56a07949 100644 --- a/regression/contracts/assigns_enforce_conditional_void_target_list/test.desc +++ b/regression/contracts/assigns_enforce_conditional_void_target_list/test.desc @@ -1,7 +1,7 @@ CORE main.c --enforce-contract foo -^.* error: (void-typed expressions not allowed as assigns clause targets|dereferencing void pointer)$ +^.* error: (dereferencing void pointer|lvalue expressions with void type not allowed in assigns clauses)$ ^CONVERSION ERROR$ ^EXIT=(1|64)$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns_enforce_function_calls/test.desc b/regression/contracts/assigns_enforce_function_calls/test.desc index 5f482125c08..3f29cee23a7 100644 --- a/regression/contracts/assigns_enforce_function_calls/test.desc +++ b/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: assigns clause target must be a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$ ^CONVERSION ERROR$ -- -- diff --git a/regression/contracts/assigns_enforce_havoc_object/main.c b/regression/contracts/assigns_enforce_havoc_object/main.c index 40eefb029e6..072c4bc9dce 100644 --- a/regression/contracts/assigns_enforce_havoc_object/main.c +++ b/regression/contracts/assigns_enforce_havoc_object/main.c @@ -15,7 +15,8 @@ typedef struct stb typedef struct sta { - union { + union + { stb *b; int i; int j; @@ -32,8 +33,7 @@ void bar(sta *a) return; } -void foo(sta *a1, sta *a2) - __CPROVER_assigns(__CPROVER_POINTER_OBJECT(a1->u.b->c)) +void foo(sta *a1, sta *a2) __CPROVER_assigns(__CPROVER_object_whole(a1->u.b->c)) { bar(a1); bar(a2); diff --git a/regression/contracts/assigns_enforce_havoc_object/test.desc b/regression/contracts/assigns_enforce_havoc_object/test.desc index 308b22c1da3..1ef1d909911 100644 --- a/regression/contracts/assigns_enforce_havoc_object/test.desc +++ b/regression/contracts/assigns_enforce_havoc_object/test.desc @@ -3,7 +3,7 @@ main.c --enforce-contract foo ^EXIT=10$ ^SIGNAL=0$ -^\[foo.assigns.\d+\] line \d+ Check that POINTER_OBJECT\(\(const void \*\)a1->u.b->c\) is valid: SUCCESS$ +^\[foo.assigns.\d+\] line \d+ Check that __CPROVER_object_whole\(\(.*\)a1->u.b->c\) is valid: SUCCESS$ ^\[bar.assigns.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)a->u\.b->c\) is assignable: SUCCESS$ ^\[bar.assigns.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)a->u\.b->c\) is assignable: FAILURE$ ^VERIFICATION FAILED$ diff --git a/regression/contracts/assigns_enforce_literal/test.desc b/regression/contracts/assigns_enforce_literal/test.desc index 74d1d576235..d1f35051245 100644 --- a/regression/contracts/assigns_enforce_literal/test.desc +++ b/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 a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$ ^CONVERSION ERROR$ -- -- diff --git a/regression/contracts/assigns_enforce_object_wrong_args/main.c b/regression/contracts/assigns_enforce_object_wrong_args/main.c index 404373b64e7..563ae82cf5f 100644 --- a/regression/contracts/assigns_enforce_object_wrong_args/main.c +++ b/regression/contracts/assigns_enforce_object_wrong_args/main.c @@ -2,7 +2,7 @@ #include #include -int baz(int *x) __CPROVER_assigns(__CPROVER_POINTER_OBJECT()) +int baz(int *x) __CPROVER_assigns(__CPROVER_object_whole()) { *x = 0; return 0; diff --git a/regression/contracts/assigns_enforce_object_wrong_args/test.desc b/regression/contracts/assigns_enforce_object_wrong_args/test.desc index ae78712952d..03d51e2a1c8 100644 --- a/regression/contracts/assigns_enforce_object_wrong_args/test.desc +++ b/regression/contracts/assigns_enforce_object_wrong_args/test.desc @@ -3,8 +3,8 @@ main.c --enforce-contract baz ^EXIT=(1|64)$ ^SIGNAL=0$ -^.*error: pointer_object expects one argument$ +^.*error: wrong number of function arguments: expected 1, but got 0$ ^CONVERSION ERROR$ -- -- -Check that `__CPROVER_POINTER_OBJECT` in assigns clauses are invoked correctly. +Check that incorrect uses of `__CPROVER_object_whole` in assigns clauses are detected. diff --git a/regression/contracts/assigns_enforce_side_effects_1/test.desc b/regression/contracts/assigns_enforce_side_effects_1/test.desc index 02be4389035..bfcae45fcfe 100644 --- a/regression/contracts/assigns_enforce_side_effects_1/test.desc +++ b/regression/contracts/assigns_enforce_side_effects_1/test.desc @@ -2,7 +2,7 @@ CORE main.c --enforce-contract foo activate-multi-line-match -.*error: (dereferencing void pointer|void-typed expressions not allowed as assigns clause targets) +.*error: (dereferencing void pointer|lvalue expressions with void type not allowed in assigns clauses) ^CONVERSION ERROR$ ^EXIT=(1|64)$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns_enforce_side_effects_2/test.desc b/regression/contracts/assigns_enforce_side_effects_2/test.desc index 8cab6884f92..77d004e7e30 100644 --- a/regression/contracts/assigns_enforce_side_effects_2/test.desc +++ b/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 a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$ ^CONVERSION ERROR$ -- -- diff --git a/regression/contracts/assigns_enforce_side_effects_3/test.desc b/regression/contracts/assigns_enforce_side_effects_3/test.desc index 8cab6884f92..77d004e7e30 100644 --- a/regression/contracts/assigns_enforce_side_effects_3/test.desc +++ b/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 a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$ ^CONVERSION ERROR$ -- -- diff --git a/regression/contracts/assigns_enforce_structs_06/main.c b/regression/contracts/assigns_enforce_structs_06/main.c index 9a8049574d5..2f3b3b27b18 100644 --- a/regression/contracts/assigns_enforce_structs_06/main.c +++ b/regression/contracts/assigns_enforce_structs_06/main.c @@ -8,7 +8,7 @@ struct pair size_t size; }; -void f1(struct pair *p) __CPROVER_assigns(__CPROVER_POINTER_OBJECT(p->buf)) +void f1(struct pair *p) __CPROVER_assigns(__CPROVER_object_whole(p->buf)) { p->buf[0] = 0; p->buf[1] = 1; diff --git a/regression/contracts/assigns_replace_06/main.c b/regression/contracts/assigns_replace_06/main.c index 9b0fd9bb878..60633d89ed5 100644 --- a/regression/contracts/assigns_replace_06/main.c +++ b/regression/contracts/assigns_replace_06/main.c @@ -1,7 +1,7 @@ #include #include -void foo(char c[]) __CPROVER_assigns(__CPROVER_POINTER_OBJECT(c)) +void foo(char c[]) __CPROVER_assigns(__CPROVER_object_whole(c)) { } diff --git a/regression/contracts/assigns_replace_conditional_targets/main.c b/regression/contracts/assigns_replace_conditional_targets/main.c index ec6a23306de..7226f2250f2 100644 --- a/regression/contracts/assigns_replace_conditional_targets/main.c +++ b/regression/contracts/assigns_replace_conditional_targets/main.c @@ -11,7 +11,7 @@ __CPROVER_requires(x && y && z) __CPROVER_assigns( a && nz(*x): *x; !a && nz(*y): *y; - !nz(*x) && !nz(*y): __CPROVER_POINTER_OBJECT(z); + !nz(*x) && !nz(*y): __CPROVER_object_whole(z); ) __CPROVER_ensures(true) // clang-format on diff --git a/regression/contracts/assigns_replace_havoc_dependent_targets_fail/replace.desc b/regression/contracts/assigns_replace_havoc_dependent_targets_fail/replace.desc index f3cd8965f37..338a948d5c8 100644 --- a/regression/contracts/assigns_replace_havoc_dependent_targets_fail/replace.desc +++ b/regression/contracts/assigns_replace_havoc_dependent_targets_fail/replace.desc @@ -3,7 +3,7 @@ main_replace.c --replace-call-with-contract resize_vec --enforce-contract resize_vec_incr10 _ --signed-overflow-check --unsigned-overflow-check --pointer-overflow-check ^\[.*\] .* Check that v->size \(assigned by the contract of resize_vec\) is assignable: SUCCESS ^\[.*\] .* Check that v->arr \(assigned by the contract of resize_vec\) is assignable: FAILURE -^\[.*\] .* Check that POINTER_OBJECT\(\(const void \*\)v->arr\) \(assigned by the contract of resize_vec\) is assignable: FAILURE +^\[.*\] .* Check that __CPROVER_object_whole\(\(.*\)v->arr\) \(assigned by the contract of resize_vec\) is assignable: FAILURE ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns_replace_havoc_dependent_targets_fail/vect.h b/regression/contracts/assigns_replace_havoc_dependent_targets_fail/vect.h index 73560893b05..7fbf6be618e 100644 --- a/regression/contracts/assigns_replace_havoc_dependent_targets_fail/vect.h +++ b/regression/contracts/assigns_replace_havoc_dependent_targets_fail/vect.h @@ -15,7 +15,7 @@ __CPROVER_requires( 0 < incr && incr < __CPROVER_max_malloc_size - v->size && __CPROVER_is_fresh(v->arr, v->size) ) -__CPROVER_assigns(v->size, v->arr, __CPROVER_POINTER_OBJECT(v->arr)) +__CPROVER_assigns(v->size, v->arr, __CPROVER_object_whole(v->arr)) __CPROVER_ensures( v->size == __CPROVER_old(v->size) + __CPROVER_old(incr) && __CPROVER_is_fresh(v->arr, v->size) diff --git a/regression/contracts/assigns_replace_havoc_dependent_targets_pass/replace.desc b/regression/contracts/assigns_replace_havoc_dependent_targets_pass/replace.desc index 207acb976ae..58368ddcb77 100644 --- a/regression/contracts/assigns_replace_havoc_dependent_targets_pass/replace.desc +++ b/regression/contracts/assigns_replace_havoc_dependent_targets_pass/replace.desc @@ -4,7 +4,7 @@ main_replace.c ^VERIFICATION SUCCESSFUL$ ^\[.*\] .* Check that v->size \(assigned by the contract of resize_vec\) is assignable: SUCCESS ^\[.*\] .* Check that v->arr \(assigned by the contract of resize_vec\) is assignable: SUCCESS -^\[.*\] .* Check that POINTER_OBJECT\(\(const void \*\)v->arr\) \(assigned by the contract of resize_vec\) is assignable: SUCCESS +^\[.*\] .* Check that __CPROVER_object_whole\(\(.*\)v->arr\) \(assigned by the contract of resize_vec\) is assignable: SUCCESS ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/contracts/assigns_replace_havoc_dependent_targets_pass/vect.h b/regression/contracts/assigns_replace_havoc_dependent_targets_pass/vect.h index 8591628104b..97f75521bc3 100644 --- a/regression/contracts/assigns_replace_havoc_dependent_targets_pass/vect.h +++ b/regression/contracts/assigns_replace_havoc_dependent_targets_pass/vect.h @@ -15,7 +15,7 @@ __CPROVER_requires( 0 < incr && incr < __CPROVER_max_malloc_size - v->size && __CPROVER_is_fresh(v->arr, v->size) ) -__CPROVER_assigns(v->size, v->arr, __CPROVER_POINTER_OBJECT(v->arr)) +__CPROVER_assigns(v->size, v->arr, __CPROVER_object_whole(v->arr)) __CPROVER_ensures( v->size == __CPROVER_old(v->size) + __CPROVER_old(incr) && __CPROVER_is_fresh(v->arr, v->size) @@ -36,7 +36,7 @@ __CPROVER_requires( v->size + 10 < __CPROVER_max_malloc_size && __CPROVER_is_fresh(v->arr, v->size) ) -__CPROVER_assigns(*v, __CPROVER_POINTER_OBJECT(v->arr)) +__CPROVER_assigns(*v, __CPROVER_object_whole(v->arr)) __CPROVER_ensures( v->size == __CPROVER_old(v->size) + 10 && __CPROVER_is_fresh(v->arr, v->size) diff --git a/regression/contracts/assigns_type_checking_invalid_case_01/test.desc b/regression/contracts/assigns_type_checking_invalid_case_01/test.desc index 51c84807dcb..d994c951202 100644 --- a/regression/contracts/assigns_type_checking_invalid_case_01/test.desc +++ b/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 a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$ -- Checks whether type checking rejects literal constants in assigns clause. diff --git a/regression/contracts/assigns_type_checking_valid_cases/main.c b/regression/contracts/assigns_type_checking_valid_cases/main.c index 52b071790fa..cc60cad45d0 100644 --- a/regression/contracts/assigns_type_checking_valid_cases/main.c +++ b/regression/contracts/assigns_type_checking_valid_cases/main.c @@ -61,7 +61,7 @@ void foo7(int a, struct buf *buffer) __CPROVER_assigns(*buffer) buffer->len = 1; } -void foo8(int array[]) __CPROVER_assigns(__CPROVER_POINTER_OBJECT(array)) +void foo8(int array[]) __CPROVER_assigns(__CPROVER_object_whole(array)) { array[0] = 1; array[1] = 1; diff --git a/regression/contracts/cprover-assignable-fail/main.c b/regression/contracts/cprover-assignable-fail/main.c new file mode 100644 index 00000000000..610ef93dc8a --- /dev/null +++ b/regression/contracts/cprover-assignable-fail/main.c @@ -0,0 +1,29 @@ +#include + +void 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_object_whole(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; + } + // pointer can be invalid expecting failed checks + my_write_set(arr, size); +} diff --git a/regression/contracts/cprover-assignable-fail/test.desc b/regression/contracts/cprover-assignable-fail/test.desc new file mode 100644 index 00000000000..0c7b693f918 --- /dev/null +++ b/regression/contracts/cprover-assignable-fail/test.desc @@ -0,0 +1,21 @@ +CORE +main.c + +CALL __CPROVER_object_whole +CALL __CPROVER_object_upto +CALL __CPROVER_object_from +CALL __CPROVER_assignable +^\[my_write_set.assertion.\d+\] .* target null or writable: FAILURE$ +^VERIFICATION FAILED$ +^EXIT=10$ +^SIGNAL=0$ +-- +CALL __CPROVER_typed_target +-- +This test checks that: +- built-ins __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_from, + __CPROVER_object_upto are supported; +- GOTO conversion preserves calls to __CPROVER_object_whole, + __CPROVER_object_upto, __CPROVER_object_from; +- GOTO conversion translates __CPROVER_typed_target to __CPROVER_assignable; +- user-defined checks embedded in `my_write_set` persist after conversion. diff --git a/regression/contracts/cprover-assignable-pass/main.c b/regression/contracts/cprover-assignable-pass/main.c new file mode 100644 index 00000000000..b7097e9cb10 --- /dev/null +++ b/regression/contracts/cprover-assignable-pass/main.c @@ -0,0 +1,25 @@ +#include + +void 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_object_whole(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; + // pointer is not invalid + my_write_set(arr, size); +} diff --git a/regression/contracts/cprover-assignable-pass/test.desc b/regression/contracts/cprover-assignable-pass/test.desc new file mode 100644 index 00000000000..182e8bc3021 --- /dev/null +++ b/regression/contracts/cprover-assignable-pass/test.desc @@ -0,0 +1,20 @@ +CORE +main.c + +CALL __CPROVER_object_whole +CALL __CPROVER_object_upto +CALL __CPROVER_object_from +CALL __CPROVER_assignable +^\[my_write_set.assertion.\d+\] .* target null or writable: SUCCESS$ +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +CALL __CPROVER_typed_target +-- +This test checks that: +- built-in __CPROVER_assignable_t functions are supported; +- GOTO conversion preserves calls to __CPROVER_object_whole, + __CPROVER_object_upto, __CPROVER_object_from; +- GOTO conversion translates __CPROVER_typed_target to __CPROVER_assignable; +- user-defined checks embedded in `my_write_set` persist after conversion. diff --git a/regression/contracts/function_check_02/main.c b/regression/contracts/function_check_02/main.c index 18be2525d8e..d065822bece 100644 --- a/regression/contracts/function_check_02/main.c +++ b/regression/contracts/function_check_02/main.c @@ -6,7 +6,7 @@ // clang-format off int initialize(int *arr) - __CPROVER_assigns(__CPROVER_POINTER_OBJECT(arr)) + __CPROVER_assigns(__CPROVER_object_whole(arr)) __CPROVER_ensures( __CPROVER_forall { int i; diff --git a/regression/contracts/loop-freeness-check/main.c b/regression/contracts/loop-freeness-check/main.c index 3840c6dcaec..73398202715 100644 --- a/regression/contracts/loop-freeness-check/main.c +++ b/regression/contracts/loop-freeness-check/main.c @@ -1,6 +1,6 @@ int foo(int *arr) // clang-format off - __CPROVER_assigns(__CPROVER_POINTER_OBJECT(arr)) + __CPROVER_assigns(__CPROVER_object_whole(arr)) // clang-format off { for(int i = 0; i < 10; i++) diff --git a/regression/contracts/quantifiers-forall-ensures-enforce/main.c b/regression/contracts/quantifiers-forall-ensures-enforce/main.c index 3e6335ab1f3..3dd6afe4295 100644 --- a/regression/contracts/quantifiers-forall-ensures-enforce/main.c +++ b/regression/contracts/quantifiers-forall-ensures-enforce/main.c @@ -4,7 +4,7 @@ // clang-format off int f1(int *arr, int len) - __CPROVER_assigns(__CPROVER_POINTER_OBJECT(arr)) + __CPROVER_assigns(__CPROVER_object_whole(arr)) __CPROVER_ensures(__CPROVER_forall { int i; // test enforcement with symbolic bound diff --git a/regression/contracts/quantifiers-nested-01/main.c b/regression/contracts/quantifiers-nested-01/main.c index f44da69dd13..cf274a29202 100644 --- a/regression/contracts/quantifiers-nested-01/main.c +++ b/regression/contracts/quantifiers-nested-01/main.c @@ -1,6 +1,6 @@ // clang-format off int f1(int *arr) - __CPROVER_assigns(__CPROVER_POINTER_OBJECT(arr)) + __CPROVER_assigns(__CPROVER_object_whole(arr)) __CPROVER_ensures(__CPROVER_forall { int i; __CPROVER_forall diff --git a/regression/contracts/quantifiers-nested-03/main.c b/regression/contracts/quantifiers-nested-03/main.c index ca586ae9f3e..c5fe0c6448e 100644 --- a/regression/contracts/quantifiers-nested-03/main.c +++ b/regression/contracts/quantifiers-nested-03/main.c @@ -1,6 +1,6 @@ // clang-format off int f1(int *arr) -__CPROVER_assigns(__CPROVER_POINTER_OBJECT(arr)) +__CPROVER_assigns(__CPROVER_object_whole(arr)) __CPROVER_ensures( __CPROVER_return_value == 0 && __CPROVER_exists { diff --git a/regression/contracts/reject_history_expr_in_assigns_clause/main.c b/regression/contracts/reject_history_expr_in_assigns_clause/main.c new file mode 100644 index 00000000000..b0ba3b9841b --- /dev/null +++ b/regression/contracts/reject_history_expr_in_assigns_clause/main.c @@ -0,0 +1,11 @@ +int foo(int *x) __CPROVER_assigns(__CPROVER_old(*x)) +{ + return 0; +} + +int main() +{ + int x; + int ret = foo(&x); + return 0; +} diff --git a/regression/contracts/reject_history_expr_in_assigns_clause/test.desc b/regression/contracts/reject_history_expr_in_assigns_clause/test.desc new file mode 100644 index 00000000000..c2afad9b49d --- /dev/null +++ b/regression/contracts/reject_history_expr_in_assigns_clause/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--enforce-contract foo +^main.c.*error: assigns clause target must be a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$ +^CONVERSION ERROR$ +^EXIT=(1|64)$ +^SIGNAL=0$ +-- +-- +This test checks that __CPROVER_old occurences in assigns clauses +are detected and rejected. diff --git a/regression/contracts/reject_history_expr_in_preconditions/main.c b/regression/contracts/reject_history_expr_in_preconditions/main.c new file mode 100644 index 00000000000..02e4e043a92 --- /dev/null +++ b/regression/contracts/reject_history_expr_in_preconditions/main.c @@ -0,0 +1,11 @@ +int foo(int *x) __CPROVER_requires(__CPROVER_old(*x)) +{ + return 0; +} + +int main() +{ + int x; + int retval = foo(&x); + return 0; +} diff --git a/regression/contracts/reject_history_expr_in_preconditions/test.desc b/regression/contracts/reject_history_expr_in_preconditions/test.desc new file mode 100644 index 00000000000..6c548ddfcd2 --- /dev/null +++ b/regression/contracts/reject_history_expr_in_preconditions/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--enforce-contract foo +^main.c.*error: __CPROVER_old is not allowed in preconditions.$ +^CONVERSION ERROR$ +^EXIT=(1|64)$ +^SIGNAL=0$ +-- +-- +This test checks that __CPROVER_old occurences in preconditions +are detected and rejected. diff --git a/regression/contracts/reject_return_value_in_assigns_clause/main.c b/regression/contracts/reject_return_value_in_assigns_clause/main.c new file mode 100644 index 00000000000..dfc0417b157 --- /dev/null +++ b/regression/contracts/reject_return_value_in_assigns_clause/main.c @@ -0,0 +1,10 @@ +int foo() __CPROVER_assigns(__CPROVER_return_value) +{ + return 0; +} + +int main() +{ + int x = foo(); + return 0; +} diff --git a/regression/contracts/reject_return_value_in_assigns_clause/test.desc b/regression/contracts/reject_return_value_in_assigns_clause/test.desc new file mode 100644 index 00000000000..ed7730dd1ae --- /dev/null +++ b/regression/contracts/reject_return_value_in_assigns_clause/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--enforce-contract foo +^main.c.*error: __CPROVER_return_value is not allowed in assigns clauses.$ +^CONVERSION ERROR$ +^EXIT=(1|64)$ +^SIGNAL=0$ +-- +-- +This test checks that __CPROVER_return_value occurences in assigns clauses +are detected and rejected. diff --git a/regression/contracts/reject_return_value_in_preconditions/main.c b/regression/contracts/reject_return_value_in_preconditions/main.c new file mode 100644 index 00000000000..ee9e6f00dd2 --- /dev/null +++ b/regression/contracts/reject_return_value_in_preconditions/main.c @@ -0,0 +1,10 @@ +int foo() __CPROVER_requires(__CPROVER_return_value == 0) +{ + return 0; +} + +int main() +{ + int x = foo(); + return 0; +} diff --git a/regression/contracts/reject_return_value_in_preconditions/test.desc b/regression/contracts/reject_return_value_in_preconditions/test.desc new file mode 100644 index 00000000000..3ab8474ce0e --- /dev/null +++ b/regression/contracts/reject_return_value_in_preconditions/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--enforce-contract foo +^main.c.*error: __CPROVER_return_value is not allowed in preconditions.$ +^CONVERSION ERROR$ +^EXIT=(1|64)$ +^SIGNAL=0$ +-- +-- +This test checks that __CPROVER_return_value occurences in preconditions +are detected and rejected. diff --git a/regression/contracts/test_array_memory_enforce/main.c b/regression/contracts/test_array_memory_enforce/main.c index 7c1218d5a30..e72cae1a7f9 100644 --- a/regression/contracts/test_array_memory_enforce/main.c +++ b/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(__CPROVER_POINTER_OBJECT(x)) + __CPROVER_assigns(__CPROVER_object_whole(x)) __CPROVER_requires( __CPROVER_is_fresh(x, sizeof(int) * 10) && x[0] > 0 && diff --git a/regression/contracts/typed_target_fail_wrong_nof_operand/main.c b/regression/contracts/typed_target_fail_wrong_nof_operand/main.c new file mode 100644 index 00000000000..b4c3509a20e --- /dev/null +++ b/regression/contracts/typed_target_fail_wrong_nof_operand/main.c @@ -0,0 +1,10 @@ +int foo(int x, int y) __CPROVER_assigns(__CPROVER_typed_target(x, y)) +{ + return 0; +} + +int main() +{ + int ret = foo(1, 2); + return 0; +} diff --git a/regression/contracts/typed_target_fail_wrong_nof_operand/test.desc b/regression/contracts/typed_target_fail_wrong_nof_operand/test.desc new file mode 100644 index 00000000000..2bb63198217 --- /dev/null +++ b/regression/contracts/typed_target_fail_wrong_nof_operand/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--enforce-contract foo +^main.c.*error: expected 1 argument for __CPROVER_typed_target, found 2$ +^CONVERSION ERROR$ +^EXIT=(1|64)$ +^SIGNAL=0$ +-- +-- +This test checks that incorrect uses of __CPROVER_typed_target are detected and +rejected. diff --git a/regression/contracts/typed_target_pointer/main.c b/regression/contracts/typed_target_pointer/main.c new file mode 100644 index 00000000000..c38602a9040 --- /dev/null +++ b/regression/contracts/typed_target_pointer/main.c @@ -0,0 +1,13 @@ +int foo(int *x, int *y) + __CPROVER_assigns(__CPROVER_typed_target(x), __CPROVER_typed_target(*y)) +{ + return 0; +} + +int main() +{ + int x; + int y; + int ret = foo(&x, &y); + return 0; +} diff --git a/regression/contracts/typed_target_pointer/test.desc b/regression/contracts/typed_target_pointer/test.desc new file mode 100644 index 00000000000..10f4d922ccb --- /dev/null +++ b/regression/contracts/typed_target_pointer/test.desc @@ -0,0 +1,14 @@ +CORE +main.c +--enforce-contract foo +^\[foo.assigns.\d+\].* Check that __CPROVER_assignable\(\(void \*\)&x, .*, TRUE\) is valid: SUCCESS$ +^\[foo.assigns.\d+\].* Check that __CPROVER_assignable\(\(void \*\)&\(\*y\), .*, FALSE\) is valid: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +-- +This test checks __CPROVER_typed_target calls with pointer arguments +get translated to __CPROVER_assignable(x, ... , TRUE), +and that calls with non pointer arguments get translated to +__CPROVER_assignable(x, ... , FALSE). diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp index 6ea08fb5b44..17c0dc34752 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/src/ansi-c/ansi_c_internal_additions.cpp @@ -216,6 +216,19 @@ void ansi_c_internal_additions(std::string &code) // This function needs to be declared, or otherwise can't be called // by the entry-point construction. "void " INITIALIZE_FUNCTION "(void);\n" + "\n" + // frame specifications for contracts + // Declares a range of bytes as assignable (internal representation) + "void " CPROVER_PREFIX "assignable(void *ptr,\n" + " " CPROVER_PREFIX "size_t size,\n" + " " CPROVER_PREFIX "bool is_ptr_to_ptr);\n" + // Declares a range of bytes as assignable + "void " CPROVER_PREFIX "object_upto(void *ptr, \n" + " " CPROVER_PREFIX "size_t size);\n" + // Declares bytes from ptr to the end of the object as assignable + "void " CPROVER_PREFIX "object_from(void *ptr);\n" + // Declares the whole object pointer to by ptr + "void " CPROVER_PREFIX "object_whole(void *ptr);\n" "\n"; // clang-format on diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp index a10ae5847e2..b91b168b256 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -674,6 +674,33 @@ void c_typecheck_baset::apply_asm_label( } } +void c_typecheck_baset::check_history_expr_return_value( + const exprt &expr, + std::string &clause_type) +{ + disallow_subexpr_by_id( + expr, ID_old, CPROVER_PREFIX "old is not allowed in " + clause_type + "."); + disallow_subexpr_by_id( + expr, + ID_loop_entry, + CPROVER_PREFIX "loop_entry is not allowed in " + clause_type + "."); + + const irep_idt id = CPROVER_PREFIX "return_value"; + auto pred = [&](const exprt &expr) { + if(!can_cast_expr(expr)) + return false; + + return to_symbol_expr(expr).get_identifier() == id; + }; + + if(!has_subexpr(expr, pred)) + return; + + throw invalid_source_file_exceptiont( + id2string(id) + " is not allowed in " + id2string(clause_type) + ".", + expr.source_location()); +} + void c_typecheck_baset::typecheck_declaration( ansi_c_declarationt &declaration) { @@ -768,15 +795,6 @@ void c_typecheck_baset::typecheck_declaration( typecheck_symbol(symbol); - auto check_history_expr = [&](const exprt expr) { - disallow_subexpr_by_id( - expr, ID_old, CPROVER_PREFIX "old is not allowed in preconditions."); - disallow_subexpr_by_id( - expr, - ID_loop_entry, - CPROVER_PREFIX "loop_entry is not allowed in preconditions."); - }; - // check the contract, if any symbolt &new_symbol = symbol_table.get_writeable_ref(identifier); if( @@ -822,7 +840,8 @@ void c_typecheck_baset::typecheck_declaration( for(auto &expr : code_type.requires_contract()) { typecheck_spec_function_pointer_obeys_contract(expr); - check_history_expr(expr); + std::string clause_type = "function pointer preconditions"; + check_history_expr_return_value(expr, clause_type); lambda_exprt lambda{temporary_parameter_symbols, expr}; lambda.add_source_location() = expr.source_location(); expr.swap(lambda); @@ -832,7 +851,8 @@ void c_typecheck_baset::typecheck_declaration( { typecheck_expr(requires); implicit_typecast_bool(requires); - check_history_expr(requires); + std::string clause_type = "preconditions"; + check_history_expr_return_value(requires, clause_type); lambda_exprt lambda{temporary_parameter_symbols, requires}; lambda.add_source_location() = requires.source_location(); requires.swap(lambda); @@ -841,6 +861,8 @@ void c_typecheck_baset::typecheck_declaration( typecheck_spec_assigns(code_type.assigns()); for(auto &assigns : code_type.assigns()) { + std::string clause_type = "assigns clauses"; + check_history_expr_return_value(assigns, clause_type); lambda_exprt lambda{temporary_parameter_symbols, assigns}; lambda.add_source_location() = assigns.source_location(); assigns.swap(lambda); diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h index 10dbb1f8196..09c3ef78da3 100644 --- a/src/ansi-c/c_typecheck_base.h +++ b/src/ansi-c/c_typecheck_base.h @@ -146,12 +146,22 @@ class c_typecheck_baset: virtual void typecheck_start_thread(codet &code); // contracts + virtual void + typecheck_typed_target_call(side_effect_expr_function_callt &expr); + /// Checks that no history expr or return_value exists in expr + virtual void + check_history_expr_return_value(const exprt &expr, std::string &clause_type); virtual void typecheck_spec_function_pointer_obeys_contract(exprt &expr); virtual void typecheck_spec_assigns(exprt::operandst &targets); - virtual void typecheck_spec_assigns_condition(exprt &condition); + virtual void typecheck_conditional_targets( + exprt::operandst &targets, + const std::function typecheck_target, + const std::string &clause_type); + virtual void typecheck_spec_condition(exprt &condition); virtual void typecheck_spec_assigns_target(exprt &target); virtual void typecheck_spec_loop_invariant(codet &code); virtual void typecheck_spec_decreases(codet &code); + virtual void throw_on_side_effects(const exprt &expr); bool break_is_allowed; bool continue_is_allowed; diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp index a27585d8022..8365e4216a0 100644 --- a/src/ansi-c/c_typecheck_code.cpp +++ b/src/ansi-c/c_typecheck_code.cpp @@ -847,7 +847,23 @@ void c_typecheck_baset::typecheck_dowhile(code_dowhilet &code) } } -void c_typecheck_baset::typecheck_spec_assigns_condition(exprt &condition) +void c_typecheck_baset::throw_on_side_effects(const exprt &expr) +{ + if(has_subexpr(expr, ID_side_effect)) + { + throw invalid_source_file_exceptiont{ + "side-effects not allowed in assigns clause targets", + expr.source_location()}; + } + if(has_subexpr(expr, ID_if)) + { + throw invalid_source_file_exceptiont{ + "ternary expressions not allowed in assigns clause targets", + expr.source_location()}; + } +} + +void c_typecheck_baset::typecheck_spec_condition(exprt &condition) { // compute type typecheck_expr(condition); @@ -869,15 +885,11 @@ void c_typecheck_baset::typecheck_spec_assigns_condition(exprt &condition) << eom; } - // fatal errors - bool must_throw = false; - if(condition.type().id() == ID_empty) { - must_throw = true; - error().source_location = condition.source_location(); - error() << "void-typed expressions not allowed as assigns clause conditions" - << eom; + throw invalid_source_file_exceptiont{ + "void-typed expressions not allowed as assigns clause conditions", + condition.source_location()}; } if(has_subexpr(condition, [&](const exprt &subexpr) { @@ -885,64 +897,100 @@ void c_typecheck_baset::typecheck_spec_assigns_condition(exprt &condition) !can_cast_expr(subexpr); })) { - must_throw = true; - error().source_location = condition.source_location(); - error() << "side-effects not allowed in assigns clause conditions" << eom; + throw invalid_source_file_exceptiont{ + "side-effects not allowed in assigns clause conditions", + condition.source_location()}; } if(has_subexpr(condition, ID_if)) { - must_throw = true; - error().source_location = condition.source_location(); - error() << "ternary expressions not allowed in assigns " - "clause conditions" - << eom; + throw invalid_source_file_exceptiont{ + "ternary expressions not allowed in assigns clause conditions", + condition.source_location()}; } - - if(must_throw) - throw 0; } -void c_typecheck_baset::typecheck_spec_assigns_target(exprt &target) +void c_typecheck_baset::typecheck_conditional_targets( + exprt::operandst &targets, + const std::function typecheck_target, + const std::string &clause_type) { - // compute type - typecheck_expr(target); + exprt::operandst new_targets; - // fatal errors - if(target.type().id() == ID_empty) + for(auto &target : targets) { - error().source_location = target.source_location(); - error() << "void-typed expressions not allowed as assigns clause targets" - << eom; - throw 0; - } + if(!can_cast_expr(target)) + { + throw invalid_source_file_exceptiont{ + "expected a conditional target group expression in " + clause_type + + "clause, found " + id2string(target.id()), + target.source_location()}; + } + + auto &conditional_target_group = to_conditional_target_group_expr(target); + validate_expr(conditional_target_group); + + // typecheck condition + auto &condition = conditional_target_group.condition(); + typecheck_spec_condition(condition); - // throws exception if expr contains side effect or ternary expr - auto throw_on_side_effects = [&](const exprt &expr) { - if(has_subexpr(expr, ID_side_effect)) + if(condition.is_true()) { - error().source_location = expr.source_location(); - error() << "side-effects not allowed in assigns clause targets" - << messaget::eom; - throw 0; + // if the condition is trivially true, + // simplify expr and expose the bare expressions + for(auto &actual_target : conditional_target_group.targets()) + { + typecheck_target(actual_target); + new_targets.push_back(actual_target); + } } - if(has_subexpr(expr, ID_if)) + else { - error().source_location = expr.source_location(); - error() << "ternary expressions not allowed in assigns " - "clause targets" - << messaget::eom; - throw 0; + // if the condition is not trivially true, typecheck in place + for(auto &actual_target : conditional_target_group.targets()) + { + typecheck_target(actual_target); + } + new_targets.push_back(std::move(target)); } + } + + // now each target is either: + // - a simple side-effect-free unconditional lvalue expression or + // - a conditional target group expression with a non-trivial condition + + // update original vector in-place + std::swap(targets, new_targets); +} + +void c_typecheck_baset::typecheck_spec_assigns(exprt::operandst &targets) +{ + const std::function typecheck_target = [&](exprt &target) { + typecheck_spec_assigns_target(target); }; + typecheck_conditional_targets(targets, typecheck_target, "assigns"); +} + +void c_typecheck_baset::typecheck_spec_assigns_target(exprt &target) +{ + // compute type + typecheck_expr(target); if(target.get_bool(ID_C_lvalue)) { + if(target.type().id() == ID_empty) + { + throw invalid_source_file_exceptiont{ + "lvalue expressions with void type not allowed in assigns clauses", + target.source_location()}; + } throw_on_side_effects(target); + return; } else if(target.id() == ID_pointer_object) { throw_on_side_effects(target); + return; } else if(can_cast_expr(target)) { @@ -951,38 +999,30 @@ void c_typecheck_baset::typecheck_spec_assigns_target(exprt &target) { const auto &ident = to_symbol_expr(funcall.function()).get_identifier(); if( - ident == CPROVER_PREFIX "object_from" || ident == CPROVER_PREFIX - "object_slice") + ident == CPROVER_PREFIX "assignable" || + ident == CPROVER_PREFIX "object_whole" || + ident == CPROVER_PREFIX "object_upto" || + ident == CPROVER_PREFIX "object_from") { for(const auto &argument : funcall.arguments()) throw_on_side_effects(argument); - } - else - { - error().source_location = target.source_location(); - error() << "function calls in assigns clause targets must be " - "to " CPROVER_PREFIX "object_from, " CPROVER_PREFIX - "object_slice" - << eom; - throw 0; + return; } } else { - error().source_location = target.source_location(); - error() << "function pointer calls not allowed in assigns targets" << eom; - throw 0; + throw invalid_source_file_exceptiont( + "function pointer calls not allowed in assigns clauses", + target.source_location()); } } - else - { - error().source_location = target.source_location(); - error() << "assigns clause target must be an lvalue or a " CPROVER_PREFIX - "POINTER_OBJECT, " CPROVER_PREFIX "object_from, " CPROVER_PREFIX - "object_slice expression" - << eom; - throw 0; - } + // if we reach this point the target did not pass the checks + throw invalid_source_file_exceptiont( + "assigns clause target must be a non-void lvalue or a call to one " + "of " CPROVER_PREFIX "POINTER_OBJECT, " CPROVER_PREFIX + "assignable, " CPROVER_PREFIX "object_whole, " CPROVER_PREFIX + "object_upto, " CPROVER_PREFIX "object_from", + target.source_location()); } void c_typecheck_baset::typecheck_spec_function_pointer_obeys_contract( @@ -1067,62 +1107,6 @@ void c_typecheck_baset::typecheck_spec_function_pointer_obeys_contract( } } -void c_typecheck_baset::typecheck_spec_assigns(exprt::operandst &targets) -{ - exprt::operandst tmp; - bool must_throw = false; - - for(auto &target : targets) - { - if(!can_cast_expr(target)) - { - must_throw = true; - error().source_location = target.source_location(); - error() << "expected ID_conditional_target_group expression in assigns " - "clause, found " - << id2string(target.id()) << eom; - } - - auto &conditional_target_group = to_conditional_target_group_expr(target); - validate_expr(conditional_target_group); - - // typecheck condition - auto &condition = conditional_target_group.condition(); - typecheck_spec_assigns_condition(condition); - - if(condition.is_true()) - { - // if the condition is trivially true, - // simplify expr and expose the bare expressions - for(auto &actual_target : conditional_target_group.targets()) - { - typecheck_spec_assigns_target(actual_target); - tmp.push_back(actual_target); - } - } - else - { - // if the condition is not trivially true, typecheck in place - for(auto &actual_target : conditional_target_group.targets()) - { - typecheck_spec_assigns_target(actual_target); - } - tmp.push_back(std::move(target)); - } - } - - // at least one target was not as expected - if(must_throw) - throw 0; - - // now each target is either: - // - a simple side-effect-free unconditional lvalue expression or - // - a conditional target group expression with a non-trivial condition - - // update original vector in-place - std::swap(targets, tmp); -} - void c_typecheck_baset::typecheck_spec_loop_invariant(codet &code) { if(code.find(ID_C_spec_loop_invariant).is_not_nil()) diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index fd58ba57e59..3e2372692b8 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -1922,6 +1922,61 @@ void c_typecheck_baset::typecheck_expr_side_effect(side_effect_exprt &expr) } } +void c_typecheck_baset::typecheck_typed_target_call( + side_effect_expr_function_callt &expr) +{ + INVARIANT( + expr.function().id() == ID_symbol && + to_symbol_expr(expr.function()).get_identifier() == CPROVER_PREFIX + "typed_target", + "expression must be a " CPROVER_PREFIX "typed_target function call"); + + auto &f_op = to_symbol_expr(expr.function()); + + if(expr.arguments().size() != 1) + { + throw invalid_source_file_exceptiont{ + "expected 1 argument for " CPROVER_PREFIX "typed_target, found " + + std::to_string(expr.arguments().size()), + expr.source_location()}; + } + + auto arg0 = expr.arguments().front(); + typecheck_expr(arg0); + if(!is_assignable(arg0) || !arg0.get_bool(ID_C_lvalue)) + { + throw invalid_source_file_exceptiont{ + "argument of " CPROVER_PREFIX "typed_target must be assignable", + arg0.source_location()}; + } + + const auto &size = size_of_expr(arg0.type(), *this); + if(!size.has_value()) + { + throw invalid_source_file_exceptiont{ + "sizeof not defined for argument of " CPROVER_PREFIX + "typed_target of type " + + to_string(arg0.type()), + arg0.source_location()}; + } + + // rewrite call to "assignable" + f_op.set_identifier(CPROVER_PREFIX "assignable"); + exprt::operandst arguments; + // pointer + arguments.push_back(address_of_exprt(arg0)); + // size + arguments.push_back(size.value()); + // is_pointer + if(arg0.type().id() == ID_pointer) + arguments.push_back(true_exprt()); + else + arguments.push_back(false_exprt()); + + expr.arguments().swap(arguments); + typecheck_side_effect_function_call(expr); +} + void c_typecheck_baset::typecheck_side_effect_function_call( side_effect_expr_function_callt &expr) { @@ -1949,8 +2004,14 @@ void c_typecheck_baset::typecheck_side_effect_function_call( if(symbol_table.symbols.find(identifier)==symbol_table.symbols.end()) { // This is an undeclared function. + + // Is it the polymorphic typed_target function ? + if(identifier == CPROVER_PREFIX "typed_target") + { + typecheck_typed_target_call(expr); + } // Is this a builtin? - if(!builtin_factory(identifier, symbol_table, get_message_handler())) + else if(!builtin_factory(identifier, symbol_table, get_message_handler())) { // yes, it's a builtin } diff --git a/src/ansi-c/cprover_builtin_headers.h b/src/ansi-c/cprover_builtin_headers.h index 17876ea8981..21a2b9c3bb5 100644 --- a/src/ansi-c/cprover_builtin_headers.h +++ b/src/ansi-c/cprover_builtin_headers.h @@ -134,6 +134,9 @@ __CPROVER_bool __CPROVER_overflow_unary_minus(); __CPROVER_bool __CPROVER_enum_is_in_range(); // contracts -__CPROVER_size_t __CPROVER_object_from(void *); -__CPROVER_size_t __CPROVER_object_slice(void *, __CPROVER_size_t); +void __CPROVER_assignable(void *ptr, __CPROVER_size_t size, + __CPROVER_bool is_ptr_to_ptr); +void __CPROVER_object_whole(void *ptr); +void __CPROVER_object_from(void *ptr); +void __CPROVER_object_upto(void *ptr, __CPROVER_size_t size); // clang-format on diff --git a/src/goto-instrument/contracts/instrument_spec_assigns.cpp b/src/goto-instrument/contracts/instrument_spec_assigns.cpp index f56f4a47d27..2d61047d28d 100644 --- a/src/goto-instrument/contracts/instrument_spec_assigns.cpp +++ b/src/goto-instrument/contracts/instrument_spec_assigns.cpp @@ -493,7 +493,9 @@ car_exprt instrument_spec_assignst::create_car_expr( return { condition, target, + // lb = ptr typecast_exprt::conditional_cast(ptr, pointer_type(char_type())), + // size = object_size(ptr) - pointer_offset(ptr) typecast_exprt::conditional_cast( minus_exprt{ typecast_exprt::conditional_cast( @@ -505,20 +507,63 @@ car_exprt instrument_spec_assignst::create_car_expr( upper_bound_var, car_havoc_methodt::HAVOC_SLICE}; } - if(ident == CPROVER_PREFIX "object_slice") + else if(ident == CPROVER_PREFIX "object_upto") { const auto &ptr = funcall.arguments().at(0); const auto &size = funcall.arguments().at(1); return { condition, target, + // lb = ptr typecast_exprt::conditional_cast(ptr, pointer_type(char_type())), + // size = size typecast_exprt::conditional_cast(size, size_type()), valid_var, lower_bound_var, upper_bound_var, car_havoc_methodt::HAVOC_SLICE}; } + else if(ident == CPROVER_PREFIX "object_whole") + { + const auto &ptr = funcall.arguments().at(0); + return { + condition, + target, + // lb = ptr - pointer_offset(ptr) + minus_exprt( + typecast_exprt::conditional_cast(ptr, pointer_type(char_type())), + pointer_offset(ptr)), + // size = object_size(ptr) + typecast_exprt::conditional_cast(object_size(ptr), size_type()), + valid_var, + lower_bound_var, + upper_bound_var, + car_havoc_methodt::HAVOC_OBJECT}; + } + else if(ident == CPROVER_PREFIX "assignable") + { + const auto &ptr = funcall.arguments().at(0); + const auto &size = funcall.arguments().at(1); + const auto &is_ptr_to_ptr = funcall.arguments().at(2); + return { + condition, + target, + // lb = ptr + typecast_exprt::conditional_cast(ptr, pointer_type(char_type())), + // size = size + typecast_exprt::conditional_cast(size, size_type()), + valid_var, + lower_bound_var, + upper_bound_var, + is_ptr_to_ptr.is_true() ? car_havoc_methodt::NONDET_ASSIGN + : car_havoc_methodt::HAVOC_SLICE}; + } + else + { + log.error().source_location = target.source_location(); + log.error() << "call to " << ident + << " in assigns clauses not supported in this version"; + } } } else if(is_assignable(target)) @@ -532,8 +577,10 @@ car_exprt instrument_spec_assignst::create_car_expr( return { condition, target, + // lb = &target typecast_exprt::conditional_cast( address_of_exprt{target}, pointer_type(char_type())), + // size = sizeof(target) typecast_exprt::conditional_cast(size.value(), size_type()), valid_var, lower_bound_var, diff --git a/src/linking/remove_internal_symbols.cpp b/src/linking/remove_internal_symbols.cpp index 5563b1b835c..db359a9e116 100644 --- a/src/linking/remove_internal_symbols.cpp +++ b/src/linking/remove_internal_symbols.cpp @@ -151,6 +151,10 @@ void remove_internal_symbols( special.insert(INITIALIZE_FUNCTION); special.insert(CPROVER_PREFIX "deallocated"); special.insert(CPROVER_PREFIX "dead_object"); + special.insert(CPROVER_PREFIX "assignable"); + special.insert(CPROVER_PREFIX "object_upto"); + special.insert(CPROVER_PREFIX "object_from"); + special.insert(CPROVER_PREFIX "object_whole"); special.insert(rounding_mode_identifier()); special.insert("__new"); special.insert("__new_array");