diff --git a/doc/cprover-manual/assigns-clause.md b/doc/cprover-manual/assigns-clause.md index c949125de00..e8e5dcb0ae2 100644 --- a/doc/cprover-manual/assigns-clause.md +++ b/doc/cprover-manual/assigns-clause.md @@ -1,22 +1,20 @@ -## CBMC Assigns Clause +# CBMC Assigns Clause +## Introduction -### Introduction The _assigns_ clause allows the user to specify a list of memory locations which may be written within a particular scope. While an assigns clause may, in general, be interpreted with either _writes_ or _modifies_ -semantics, this design is based on the former. This means that memory not +semantics, this design is based on the former. This means that memory not captured by the assigns clause must not be written within the given scope, even if the value(s) therein are not modified. +Assigns clauses currently support 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. -### Scalar Variables -The initial iteration of this design focuses on specifying an assigns clause for -primitive types and their pointers. Arrays, structured data, and pointers are -left to future contributions. - -##### Syntax +## Syntax A special construct is introduced to specify assigns clauses. Its syntax is defined as follows. @@ -24,29 +22,82 @@ defined as follows. := __CPROVER_assigns ( ) ``` ``` - := - | , + := __CPROVER_nothing + | + | , +``` +``` + := + | [ array_index ] + | [ array_range ] + + := | + := , +``` +``` + := + | * ``` ``` - := - | * + := + | . + | -> +``` +``` + := + | ( ) +``` + +The assigns clause identifies a list of targets, which may be an identifier +(e.g. `x`), a member of a struct (e.g. `myStruct.someMember` or +`myStructPtr->otherMember`), a dereferenced pointer (e.g. `*myPtr`), or an +array range (e.g. `myArr[5, lastIdx]`). The `` states that only +memory identified in the target list may be written within the function, as +described in the next section. + +For example, consider the following declarations. + +```c +struct pair +{ + int x; + int y; +}; + +void foo(int *myInt1, int *myInt2, struct pair *myPair, int myArr[], int lastIdx) +__CPROVER_assigns(*myInt1, myPair->y, myArr[5, lastIdx]); ``` +This code declares a struct type, called `pair` with 2 members `x` and `y`, +as well as a function `foo` which takes two integer pointer arguments +`myInt1` and `myInt2`, one pair struct pointer `myPair`, and an array +argument `myArr` with an associated last index `lastIdx`. The assigns +clause attached to this definition states that most of the arguments +can be assigned. However, `myInt2`, `myPair->x`, and the first four +elements of `myArr` should not be assigned in the body of `foo`. + +## Semantics +The semantics of an assigns clause *c* of some function *f* can +be understood in two contexts. First, one may consider how the expressions in +*c* are treated when a call to *f* is replaced by its contract specification, +assuming the contract specification is a sound characterization of the behavior +of *f*. Second, one may consider how *c* is applied to the function body of *f* +in order to determine whether *c* is a sound characterization of the behavior of +*f*. To illustrate these two perspectives, consider the following definition of +`foo`. -The `` states that only the memory identified by the dereference -expressions and identifiers listed in the contained `` may be -written within the associated scope, as follows. +```c +void foo(int *myInt1, int *myInt2, struct pair *myPair, int myArr[], int lastIdx) +{ + *myInt1 = 34; + myPair->y = 55; + myArr[5] = 89; +} +``` -##### Semantics -The semantics of an assigns clause *c* of some function *f* can be understood in -two contexts. First, one may consider how the expressions in *c* are treated -when a call to *f* is replaced by its contract specification, assuming the -contract specification is a sound characterization of the behavior of *f*. -Second, one may consider how *c* is applied to the function body of *f* in order -to determine whether *c* is a sound characterization of the behavior of *f*. We -begin by exploring these two perspectives for assigns clauses which contain only -scalar expressions. +We begin by exploring these two perspectives with a formal definition, and then +an example. Let the ith expression in some assigns clause *c* be denoted *exprs**c*[i], the jth formal parameter of some function @@ -55,35 +106,160 @@ in a call to function *f* be denoted *args**f*[k] (an identifying index may be added to distinguish a *particular* call to *f*, but for simplicity it is omitted here). +## Replacement +Assuming an assigns clause *c* is a sound characterization of +the behavior of the function *f*, a call to *f* may be replaced a series of +non-deterministic assignments. For each expression *e* ∈ +*exprs**c*, let there be an assignment ɸ := ∗, where +ɸ is *args**f*[i] if *e* is identical to some +*params**f*[i], and *e* otherwise. For array ranges, create an +assignment for each element in the array range. + +In the case where *f* is `foo`, and some function `bar` calls `foo` + +```c +void bar() +{ + int a, b; + int arr[8]; + struct pair p; + + foo(&a, &b, &p, arr, 7); +} +``` + +the call to `foo` is replaced by the following series of assignments. + +```c +void bar() +{ + int a, b; + int arr[10]; + struct pair p; + + a = *; + p.y = *; + arr[5] = *; + arr[6] = *; + arr[7] = *; +} +``` + +## Enforcement +In order to determine whether an assigns clause *c* is a +sound characterization of the behavior of a function *f*, the body of the +function is instrumented with assertion statements before each statement which +may write to memory (e.g. an assignment). These assertions are based on the +assignable targets *exprs**c* identified in the assigns clause. + +While sequentially traversing the function body, CBMC instruments statements +that might modify memory a preceding assertion to ensure that they only +modify assignable memory. These assertions consist of a disjunction +where each disjunct depends on the type of the assignable target. + +- For an assignable target expression *e* of scalar type: + +```c +__CPROVER_POINTER_OBJECT(&lhs) == __CPROVER_POINTER_OBJECT(&e) && +__CPROVER_POINTER_OFFSET(&lhs) == __CPROVER_POINTER_OFFSET(&e) +``` + +- For an assignable target expression *e* of struct type, a similar disjunct is + created, with an additional size comparison: + +```c +__CPROVER_POINTER_OBJECT(&lhs) == __CPROVER_POINTER_OBJECT(&e) && +__CPROVER_POINTER_OFFSET(&lhs) == __CPROVER_POINTER_OFFSET(&e) && +sizeof(lhs) == sizeof(e) +``` + +Additionally, for each member m of *e*, we add an extra disjunct: + +```c +__CPROVER_POINTER_OBJECT(&lhs) == __CPROVER_POINTER_OBJECT(&(e->m)) && +__CPROVER_POINTER_OFFSET(&lhs) == __CPROVER_POINTER_OFFSET(&(e->m)) && +sizeof(lhs) == sizeof(e->m) +``` + +This extension is performed recursively in the +case that some member of a struct is also a struct. + +- For an assignable target expression *e* of array range type, `a[lo, hi]`, a + disjunct is created using the array pointer `a` and the range bounds `lo` and +`hi`: + +```c +__CPROVER_POINTER_OBJECT(&lhs) == __CPROVER_POINTER_OBJECT(a) && +__CPROVER_POINTER_OFFSET(&lhs) >= lo * sizeof(a[0]) && +__CPROVER_POINTER_OFFSET(&lhs) <= hi * sizeof(a[0]) +``` + +This effectively creates an assertion that the memory location being assigned +falls within the assignable memory identified by the assigns clause. In +practice, temporary variables are used to ensure that the assignable memory +doesn't change during function execution, but here we have used the assignable +targets directly for readability. Function calls are handled similarly, based +on the memory their assigns clause indicates that they can modify. +Additionally, for each function call without an assigns clause, we add an +assertion assert(*false*) to ensure that the assigns contract will only hold if +all called functions have an assigns clause which is compatible with that of the +calling function. + +For the earlier example, `foo` would be instrumented as follows: + + +```c +void foo(int *myInt1, int *myInt2, struct pair *myPair, int myArr[], int lastIdx) +{ + int *temp1 = myInt1; + int *temp2 = &(myPair->y); + int *temp3 = myArr; + int temp4 = 5 * sizeof(iint); + int temp5 = lastIdx * sizeof(int); + + assert((__CPROVER_POINTER_OBJECT(myInt1) == __CPROVER_POINTER_OBJECT(temp1) && + __CPROVER_POINTER_OFFSET(myInt1) == __CPROVER_POINTER_OFFSET(temp1)) || + (__CPROVER_POINTER_OBJECT(myInt1) == __CPROVER_POINTER_OBJECT(temp2) && + __CPROVER_POINTER_OFFSET(myInt1) == __CPROVER_POINTER_OFFSET(temp2)) || + (__CPROVER_POINTER_OBJECT(myInt1) == __CPROVER_POINTER_OBJECT(temp3) && + __CPROVER_POINTER_OFFSET(myInt1) >= temp4 && + __CPROVER_POINTER_OFFSET(myInt1) <= temp5) + ); + *myInt1 = 34; + + assert((__CPROVER_POINTER_OBJECT(&(myPair->y)) == __CPROVER_POINTER_OBJECT(temp1) && + __CPROVER_POINTER_OFFSET(&(myPair->y)) == __CPROVER_POINTER_OFFSET(temp1)) || + (__CPROVER_POINTER_OBJECT(&(myPair->y)) == __CPROVER_POINTER_OBJECT(temp2) && + __CPROVER_POINTER_OFFSET(&(myPair->y)) == __CPROVER_POINTER_OFFSET(temp2)) || + (__CPROVER_POINTER_OBJECT(&(myPair->y)) == __CPROVER_POINTER_OBJECT(temp3) && + __CPROVER_POINTER_OFFSET(&(myPair->y)) >= temp4 && + __CPROVER_POINTER_OFFSET(&(myPair->y)) <= temp5) + ); + myPair->y = 55; + + assert((__CPROVER_POINTER_OBJECT(&(myArr[5])) == __CPROVER_POINTER_OBJECT(temp1) && + __CPROVER_POINTER_OFFSET(&(myArr[5])) == __CPROVER_POINTER_OFFSET(temp1)) || + (__CPROVER_POINTER_OBJECT(&(myArr[5])) == __CPROVER_POINTER_OBJECT(temp2) && + __CPROVER_POINTER_OFFSET(&(myArr[5])) == __CPROVER_POINTER_OFFSET(temp2)) || + (__CPROVER_POINTER_OBJECT(&(myArr[5])) == __CPROVER_POINTER_OBJECT(temp3) && + __CPROVER_POINTER_OFFSET(&(myArr[5])) >= temp4 && + __CPROVER_POINTER_OFFSET(&(myArr[5])) <= temp5) + ); + myArr[5] = 89; +} +``` + +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 -Assuming an assigns clause *c* is a sound characterization of the behavior of -the function *f*, a call to *f* may be replaced a series of non-deterministic -assignments. For each expression *e* ∈ *exprs**c*, let there be -an assignment ɸ := ∗, where ɸ is *args**f*[i] if *e* -is identical to some *params**f*[i], and *e* otherwise. - - -###### Enforcement -In order to determine whether an assigns clause *c* is a sound characterization -of the behavior of a function *f*, the body of the function should be -instrumented with additional statements as follows. - -- For each expression *e* ∈ *exprs**c*, create a temporary - variable *tmp**e* to store \&(*e*), the address of *e*, at the -start of *f*. -- Before each assignment statement, *lhs* := *rhs*, add an assertion (structured - as a disjunction) -assert(∃ *tmp**e*. \_\_CPROVER\_same\_object(\&(*lhs*), -*tmp**e*) -- Before each function call with an assigns clause *a*, add an assertion for - each *e**a* ∈ *exprs**a* (also formulated as a -disjunction) -assert(∃ *tmp**e*. -\_\_CPROVER\_same\_object(\&(*e**a*), *tmp**e*) - -Here, \_\_CPROVER\_same\_object returns true if two pointers -reference the same object in the CBMC memory model. Additionally, for each -function call without an assigns clause, CBMC adds an assertion assert(*false*) -to ensure that the assigns contract will only hold if all called functions -have an assigns clause which is compatible with that of the calling function. +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 *free*. Assignment statements (i.e., +where the left-hand-side is in *free*) are not instrumented with +the above assertions. diff --git a/regression/contracts/assigns_enforce_arrays_01/main.c b/regression/contracts/assigns_enforce_arrays_01/main.c new file mode 100644 index 00000000000..1ec59383c7e --- /dev/null +++ b/regression/contracts/assigns_enforce_arrays_01/main.c @@ -0,0 +1,15 @@ +void f1(int a[], int len) __CPROVER_assigns(a) +{ + int b[10]; + a = b; + int *indr = a + 2; + *indr = 5; +} + +int main() +{ + int arr[10]; + f1(arr, 10); + + return 0; +} diff --git a/regression/contracts/assigns_enforce_arrays_01/test.desc b/regression/contracts/assigns_enforce_arrays_01/test.desc new file mode 100644 index 00000000000..bcdff5d2a3a --- /dev/null +++ b/regression/contracts/assigns_enforce_arrays_01/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Checks their assigns clause behavior when it reasons (indirectly) +over a freshly-allocated variable. diff --git a/regression/contracts/assigns_enforce_arrays_02/main.c b/regression/contracts/assigns_enforce_arrays_02/main.c new file mode 100644 index 00000000000..6f0330dedeb --- /dev/null +++ b/regression/contracts/assigns_enforce_arrays_02/main.c @@ -0,0 +1,24 @@ +#include + +int idx = 4; + +int nextIdx() __CPROVER_assigns(idx) +{ + idx++; + return idx; +} + +void f1(int a[], int len) +{ + a[nextIdx()] = 5; +} + +int main() +{ + int arr[10]; + f1(arr, 10); + + assert(idx == 5); + + return 0; +} diff --git a/regression/contracts/assigns_enforce_arrays_02/test.desc b/regression/contracts/assigns_enforce_arrays_02/test.desc new file mode 100644 index 00000000000..6bda4077707 --- /dev/null +++ b/regression/contracts/assigns_enforce_arrays_02/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Checks whether the instrumentation process does not duplicate function calls +used as part of array-index operations, i.e., if a function call is used in +the computation of the index of an array assignment, then instrumenting that +statement with an assigns clause will not result in multiple function calls. diff --git a/regression/contracts/assigns_enforce_arrays_03/main.c b/regression/contracts/assigns_enforce_arrays_03/main.c new file mode 100644 index 00000000000..9a51b358f75 --- /dev/null +++ b/regression/contracts/assigns_enforce_arrays_03/main.c @@ -0,0 +1,12 @@ +void assign_out_under(int a[], int len) __CPROVER_assigns(a) +{ + a[1] = 5; +} + +int main() +{ + int arr[10]; + assign_out_under(arr, 10); + + return 0; +} diff --git a/regression/contracts/assigns_enforce_arrays_03/test.desc b/regression/contracts/assigns_enforce_arrays_03/test.desc new file mode 100644 index 00000000000..e5c01665aa6 --- /dev/null +++ b/regression/contracts/assigns_enforce_arrays_03/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +Checks whether verification fails when an array is assigned at an index +below its lower bound. diff --git a/regression/contracts/assigns_enforce_arrays_04/main.c b/regression/contracts/assigns_enforce_arrays_04/main.c new file mode 100644 index 00000000000..6e51934a449 --- /dev/null +++ b/regression/contracts/assigns_enforce_arrays_04/main.c @@ -0,0 +1,21 @@ +void assigns_single(int a[], int len) __CPROVER_assigns(a) +{ +} + +void assigns_range(int a[], int len) __CPROVER_assigns(a) +{ +} + +void assigns_big_range(int a[], int len) __CPROVER_assigns(a) +{ + assigns_single(a, len); + assigns_range(a, len); +} + +int main() +{ + int arr[10]; + assigns_big_range(arr, 10); + + return 0; +} diff --git a/regression/contracts/assigns_enforce_arrays_04/test.desc b/regression/contracts/assigns_enforce_arrays_04/test.desc new file mode 100644 index 00000000000..4ce2c8bc8d2 --- /dev/null +++ b/regression/contracts/assigns_enforce_arrays_04/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Checks whether verification succeeds when an array is assigned through +calls to functions with array assigns clauses which are compatible with +that of the caller. diff --git a/regression/contracts/assigns_enforce_arrays_05/main.c b/regression/contracts/assigns_enforce_arrays_05/main.c new file mode 100644 index 00000000000..4eade02f201 --- /dev/null +++ b/regression/contracts/assigns_enforce_arrays_05/main.c @@ -0,0 +1,18 @@ +void assigns_ptr(int *x) __CPROVER_assigns(*x) +{ + *x = 200; +} + +void assigns_range(int a[], int len) __CPROVER_assigns(a) +{ + int *ptr = &(a[7]); + assigns_ptr(ptr); +} + +int main() +{ + int arr[10]; + assigns_range(arr, 10); + + return 0; +} diff --git a/regression/contracts/assigns_enforce_arrays_05/test.desc b/regression/contracts/assigns_enforce_arrays_05/test.desc new file mode 100644 index 00000000000..948fc5eb2e3 --- /dev/null +++ b/regression/contracts/assigns_enforce_arrays_05/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +Checks whether verification fails when an array is assigned via a +function call which assigns a pointer to an element out of the +allowable range. diff --git a/regression/contracts/assigns_enforce_multi_file_01/header.h b/regression/contracts/assigns_enforce_multi_file_01/header.h new file mode 100644 index 00000000000..170fd37498c --- /dev/null +++ b/regression/contracts/assigns_enforce_multi_file_01/header.h @@ -0,0 +1,22 @@ +void f1(int *x1, int *y1, int *z1); + +void f2(int *x2, int *y2, int *z2); + +void f3(int *x3, int *y3, int *z3); + +void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1) +{ + f2(x1, y1, z1); +} + +void f2(int *x2, int *y2, int *z2) __CPROVER_assigns(*x2, *y2, *z2) +{ + f3(x2, y2, z2); +} + +void f3(int *x3, int *y3, int *z3) __CPROVER_assigns(*y3, *z3) +{ + *x3 = *x3 + 1; + *y3 = *y3 + 1; + *z3 = *z3 + 1; +} diff --git a/regression/contracts/assigns_enforce_multi_file_01/main.c b/regression/contracts/assigns_enforce_multi_file_01/main.c new file mode 100644 index 00000000000..01e3878af6e --- /dev/null +++ b/regression/contracts/assigns_enforce_multi_file_01/main.c @@ -0,0 +1,11 @@ +#include "header.h" + +int main() +{ + int p = 1; + int q = 2; + int r = 3; + f1(&p, &q, &r); + + return 0; +} diff --git a/regression/contracts/assigns_enforce_multi_file_01/test.desc b/regression/contracts/assigns_enforce_multi_file_01/test.desc new file mode 100644 index 00000000000..2d5f2976228 --- /dev/null +++ b/regression/contracts/assigns_enforce_multi_file_01/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +This test replicates the behavior of assigns_enforce_04, but separates +the function headers and contracts into a separate file header.h. diff --git a/regression/contracts/assigns_enforce_multi_file_02/header.h b/regression/contracts/assigns_enforce_multi_file_02/header.h new file mode 100644 index 00000000000..267565a2ed5 --- /dev/null +++ b/regression/contracts/assigns_enforce_multi_file_02/header.h @@ -0,0 +1,23 @@ +#include + +struct pair +{ + int x; + int y; +}; + +struct pair_of_pairs +{ + struct pair p1; + struct pair p2; +}; + +int f1(int *a, struct pair *b); + +int f1(int *a, struct pair *b) __CPROVER_assigns(*a) +{ + struct pair_of_pairs *pop = + (struct pair_of_pairs *)malloc(sizeof(struct pair_of_pairs)); + b = &(pop->p2); + b->y = 5; +} diff --git a/regression/contracts/assigns_enforce_multi_file_02/main.c b/regression/contracts/assigns_enforce_multi_file_02/main.c new file mode 100644 index 00000000000..f18a61dd1c2 --- /dev/null +++ b/regression/contracts/assigns_enforce_multi_file_02/main.c @@ -0,0 +1,10 @@ +#include "header.h" + +int main() +{ + int m = 4; + struct pair n; + f1(&m, &n); + + return 0; +} diff --git a/regression/contracts/assigns_enforce_multi_file_02/test.desc b/regression/contracts/assigns_enforce_multi_file_02/test.desc new file mode 100644 index 00000000000..ac43a1c0a71 --- /dev/null +++ b/regression/contracts/assigns_enforce_multi_file_02/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test replicates the behavior of assigns_enforce_structs_03, but separates +the structs, function headers, and contracts into a separate file header.h. diff --git a/regression/contracts/assigns_enforce_structs_01/main.c b/regression/contracts/assigns_enforce_structs_01/main.c new file mode 100644 index 00000000000..0e03b35338d --- /dev/null +++ b/regression/contracts/assigns_enforce_structs_01/main.c @@ -0,0 +1,23 @@ +#include + +struct pair +{ + int x; + int y; +}; + +int f1(int *a, int *b) __CPROVER_assigns(*a) +{ + struct pair *p = (struct pair *)malloc(sizeof(struct pair)); + b = &(p->y); + *b = 5; +} + +int main() +{ + int m = 4; + int n = 3; + f1(&m, &n); + + return 0; +} diff --git a/regression/contracts/assigns_enforce_structs_01/test.desc b/regression/contracts/assigns_enforce_structs_01/test.desc new file mode 100644 index 00000000000..56e272577a3 --- /dev/null +++ b/regression/contracts/assigns_enforce_structs_01/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Checks whether verification succeeds when a formal parameter pointer outside +of the assigns clause is instead pointed at the location of a member of a +freshly allocated struct before being assigned. diff --git a/regression/contracts/assigns_enforce_structs_02/main.c b/regression/contracts/assigns_enforce_structs_02/main.c new file mode 100644 index 00000000000..5e893871daf --- /dev/null +++ b/regression/contracts/assigns_enforce_structs_02/main.c @@ -0,0 +1,30 @@ +#include + +struct pair +{ + int x; + int y; +}; + +struct pair_of_pairs +{ + struct pair p1; + struct pair p2; +}; + +int f1(int *a, int *b) __CPROVER_assigns(*a) +{ + struct pair_of_pairs *pop = + (struct pair_of_pairs *)malloc(sizeof(struct pair_of_pairs)); + b = &(pop->p2.x); + *b = 5; +} + +int main() +{ + int m = 4; + int n = 3; + f1(&m, &n); + + return 0; +} diff --git a/regression/contracts/assigns_enforce_structs_02/test.desc b/regression/contracts/assigns_enforce_structs_02/test.desc new file mode 100644 index 00000000000..fe467282fb5 --- /dev/null +++ b/regression/contracts/assigns_enforce_structs_02/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Checks whether verification succeeds when a formal parameter pointer outside +of the assigns clause is assigned after being pointed at the location of a +member of a sub-struct of a freshly allocated struct before being assigned. +This is meant to show that all contained members (and their contained members) +of assignable structs are valid to assign. diff --git a/regression/contracts/assigns_enforce_structs_03/main.c b/regression/contracts/assigns_enforce_structs_03/main.c new file mode 100644 index 00000000000..d225d739bd1 --- /dev/null +++ b/regression/contracts/assigns_enforce_structs_03/main.c @@ -0,0 +1,30 @@ +#include + +struct pair +{ + int x; + int y; +}; + +struct pair_of_pairs +{ + struct pair p1; + struct pair p2; +}; + +int f1(int *a, struct pair *b) __CPROVER_assigns(*a) +{ + struct pair_of_pairs *pop = + (struct pair_of_pairs *)malloc(sizeof(struct pair_of_pairs)); + b = &(pop->p2); + b->y = 5; +} + +int main() +{ + int m = 4; + struct pair n; + f1(&m, &n); + + return 0; +} diff --git a/regression/contracts/assigns_enforce_structs_03/test.desc b/regression/contracts/assigns_enforce_structs_03/test.desc new file mode 100644 index 00000000000..2bbffe0670f --- /dev/null +++ b/regression/contracts/assigns_enforce_structs_03/test.desc @@ -0,0 +1,14 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Checks whether verification succeeds when a member of formal parameter +(with type of pointer to struct) outside of the assigns clause is assigned +after being pointed at the location of a member sub-struct of a freshly +allocated struct before being assigned. This is meant to show that all +contained members (and their contained members) of assignable structs +are valid to assign. diff --git a/regression/contracts/assigns_replace_06/main.c b/regression/contracts/assigns_replace_06/main.c new file mode 100644 index 00000000000..dc54f4ff8e2 --- /dev/null +++ b/regression/contracts/assigns_replace_06/main.c @@ -0,0 +1,48 @@ +#include + +void foo(char c[]) __CPROVER_assigns(c) +{ +} + +void bar(char d[]) __CPROVER_assigns(d) +{ +} + +int main() +{ + char b[10]; + b[0] = 'a'; + b[1] = 'b'; + b[2] = 'c'; + b[3] = 'd'; + b[4] = 'e'; + b[5] = 'f'; + b[6] = 'g'; + b[7] = 'h'; + b[8] = 'i'; + b[9] = 'j'; + foo(b); + assert(b[0] == 'a'); + assert(b[1] == 'b'); + assert(b[5] == 'f'); + assert(b[6] == 'g'); + assert(b[7] == 'h'); + assert(b[8] == 'i'); + assert(b[9] == 'j'); + + b[2] = 'c'; + b[3] = 'd'; + b[4] = 'e'; + bar(b); + assert(b[0] == 'a'); + assert(b[1] == 'b'); + assert(b[2] == 'c'); + assert(b[3] == 'd'); + assert(b[4] == 'e'); + assert(b[5] == 'f'); + assert(b[6] == 'g'); + assert(b[8] == 'i'); + assert(b[9] == 'j'); + + return 0; +} diff --git a/regression/contracts/assigns_replace_06/test.desc b/regression/contracts/assigns_replace_06/test.desc new file mode 100644 index 00000000000..13d942ed25e --- /dev/null +++ b/regression/contracts/assigns_replace_06/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--replace-all-calls-with-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Checks whether the values outside the array range specified by the assigns +target are not havocked when calling the associated function. diff --git a/regression/contracts/assigns_replace_07/main.c b/regression/contracts/assigns_replace_07/main.c new file mode 100644 index 00000000000..84e534f6562 --- /dev/null +++ b/regression/contracts/assigns_replace_07/main.c @@ -0,0 +1,24 @@ +#include + +void bar(char d[]) __CPROVER_assigns(d[7]) +{ +} + +int main() +{ + char b[10]; + b[0] = 'a'; + b[1] = 'b'; + b[2] = 'c'; + b[3] = 'd'; + b[4] = 'e'; + b[5] = 'f'; + b[6] = 'g'; + b[7] = 'h'; + b[8] = 'i'; + b[9] = 'j'; + bar(b); + assert(b[7] == 'h'); + + return 0; +} diff --git a/regression/contracts/assigns_replace_07/test.desc b/regression/contracts/assigns_replace_07/test.desc new file mode 100644 index 00000000000..db3a9dbd079 --- /dev/null +++ b/regression/contracts/assigns_replace_07/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--replace-all-calls-with-contracts +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +Checks whether the value inside a single-index array assigns target is +havocked when calling the associated function. diff --git a/regression/contracts/function-calls-02-1/test-enf.desc b/regression/contracts/function-calls-02-1/test-enf.desc index 817b7b9c8d8..b2cdcc29e00 100644 --- a/regression/contracts/function-calls-02-1/test-enf.desc +++ b/regression/contracts/function-calls-02-1/test-enf.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c --enforce-all-contracts ^EXIT=0$ @@ -11,6 +11,3 @@ Verification: ---------|----------|---------- f1 | assumed | asserted f2 | assumed | asserted - -Known bug: -Enforce flag not handled correctly for function calls within functions. diff --git a/regression/contracts/function-calls-02/test-enf.desc b/regression/contracts/function-calls-02/test-enf.desc index 817b7b9c8d8..b2cdcc29e00 100644 --- a/regression/contracts/function-calls-02/test-enf.desc +++ b/regression/contracts/function-calls-02/test-enf.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c --enforce-all-contracts ^EXIT=0$ @@ -11,6 +11,3 @@ Verification: ---------|----------|---------- f1 | assumed | asserted f2 | assumed | asserted - -Known bug: -Enforce flag not handled correctly for function calls within functions. diff --git a/regression/contracts/function-calls-03/test-enf.desc b/regression/contracts/function-calls-03/test-enf.desc index fdbd93aacd0..4370e783ea9 100644 --- a/regression/contracts/function-calls-03/test-enf.desc +++ b/regression/contracts/function-calls-03/test-enf.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c --enforce-all-contracts _ --unwind 20 --unwinding-assertions ^EXIT=0$ @@ -14,6 +14,3 @@ Verification: Recursion: The base case for the recursive call to f2 provides the same behavior as the common case (given the pre-conditions). - -Known bug: -Enforce flag not handled correctly for function calls within functions. diff --git a/regression/contracts/function-calls-04/test-enf.desc b/regression/contracts/function-calls-04/test-enf.desc index 808cdab1356..ca946db95ad 100644 --- a/regression/contracts/function-calls-04/test-enf.desc +++ b/regression/contracts/function-calls-04/test-enf.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c --enforce-all-contracts _ --unwind 20 --unwinding-assertions ^EXIT=0$ @@ -15,6 +15,3 @@ Verification: Recursion: The base case for the recursive call to f2 provides the same behavior as the common case (given the pre-conditions). - -Known bug: -Enforce flag not handled correctly for function calls within functions. diff --git a/regression/contracts/function-calls-04/test-mix-2.desc b/regression/contracts/function-calls-04/test-mix-2.desc index 243d70b6f19..766a17a3f70 100644 --- a/regression/contracts/function-calls-04/test-mix-2.desc +++ b/regression/contracts/function-calls-04/test-mix-2.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c --enforce-contract f1 --enforce-contract f2_out --replace-call-with-contract f2_in ^EXIT=0$ @@ -17,6 +17,3 @@ Recursion (1) This test checks the mutualy recursive f2_out and f2-in functions by enforcing f2_out and replacing the internal f2_in call with its contract. (2) This test does not require unwinding. (3) The base case for the recursive call to f2 provides the same behavior as the common case (given the pre-conditions). - -Known bug: -Enforce flag not handled correctly for function calls within functions. diff --git a/scripts/expected_doxygen_warnings.txt b/scripts/expected_doxygen_warnings.txt index affa60f29cb..ca71fda3f18 100644 --- a/scripts/expected_doxygen_warnings.txt +++ b/scripts/expected_doxygen_warnings.txt @@ -21,15 +21,15 @@ warning: Include graph for 'goto_instrument_parse_options.cpp' not generated, too many nodes (97), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'goto_functions.h' not generated, too many nodes (66), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'goto_model.h' not generated, too many nodes (111), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. -warning: Included by graph for 'arith_tools.h' not generated, too many nodes (181), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. -warning: Included by graph for 'c_types.h' not generated, too many nodes (141), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. +warning: Included by graph for 'arith_tools.h' not generated, too many nodes (182), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. +warning: Included by graph for 'c_types.h' not generated, too many nodes (142), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'config.h' not generated, too many nodes (88), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'exception_utils.h' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'expr.h' not generated, too many nodes (87), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'expr_util.h' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'invariant.h' not generated, too many nodes (186), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'irep.h' not generated, too many nodes (62), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. -warning: Included by graph for 'message.h' not generated, too many nodes (117), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. +warning: Included by graph for 'message.h' not generated, too many nodes (118), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'namespace.h' not generated, too many nodes (110), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'pointer_expr.h' not generated, too many nodes (116), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'prefix.h' not generated, too many nodes (85), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index 3765c63ab67..c1788326964 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -11,8 +11,9 @@ Date: February 2016 /// \file /// Verify and use annotated invariants and pre/post-conditions +#include "code_contracts.h" + #include -#include #include @@ -20,15 +21,17 @@ Date: February 2016 #include +#include #include #include +#include #include +#include #include -#include +#include #include #include -#include "code_contracts.h" #include "loop_utils.h" /// Predicate to be used with the exprt::visit() function. The function @@ -37,7 +40,7 @@ Date: February 2016 class return_value_visitort : public const_expr_visitort { public: - return_value_visitort() : const_expr_visitort() + return_value_visitort() : const_expr_visitort(), found(false) { } @@ -60,6 +63,15 @@ class return_value_visitort : public const_expr_visitort bool found; }; +exprt get_size(const typet &type, const namespacet &ns, messaget &log) +{ + auto size_of_opt = size_of_expr(type, ns); + CHECK_RETURN(size_of_opt.has_value()); + exprt result = size_of_opt.value(); + result.add(ID_C_c_sizeof_type) = type; + return result; +} + static void check_apply_invariants( goto_functionst::goto_functiont &goto_function, const local_may_aliast &local_may_alias, @@ -152,6 +164,7 @@ bool code_contractst::has_contract(const irep_idt fun_name) } bool code_contractst::apply_function_contract( + const irep_idt &function_id, goto_programt &goto_program, goto_programt::targett target) { @@ -159,9 +172,7 @@ bool code_contractst::apply_function_contract( // Return if the function is not named in the call; currently we don't handle // function pointers. - // TODO: handle function pointers. - if(call.function().id() != ID_symbol) - return false; + PRECONDITION(call.function().id() == ID_symbol); // Retrieve the function type, which is needed to extract the contract // components. @@ -251,28 +262,14 @@ bool code_contractst::apply_function_contract( // in the assigns clause. if(assigns.is_not_nil()) { - goto_programt assigns_havoc; - modifiest assigns_tgts; - const exprt::operandst &targets = assigns.operands(); - for(const exprt &curr_op : targets) - { - if(curr_op.id() == ID_symbol || curr_op.id() == ID_dereference) - { - assigns_tgts.insert(curr_op); - } - else - { - log.error() << "Unable to apply assigns clause for expression of type '" - << curr_op.id() << "'; not enforcing assigns clause." - << messaget::eom; - return true; - } - } - build_havoc_code(target, assigns_tgts, assigns_havoc); + assigns_clauset assigns_cause(assigns, *this, function_id, log); + goto_programt assigns_havoc = assigns_cause.havoc_code( + function_symbol.location, function_id, function_symbol.mode); // Insert the non-deterministic assignment immediately before the call site. + std::size_t lines_to_iterate = assigns_havoc.instructions.size(); goto_program.insert_before_swap(target, assigns_havoc); - std::advance(target, assigns_tgts.size()); + std::advance(target, lines_to_iterate); } // To remove the function call, replace it with an assumption statement @@ -319,133 +316,104 @@ const symbolt &code_contractst::new_tmp_symbol( symbol_table); } -static exprt create_alias_expression( - const exprt &assigns, +exprt code_contractst::create_alias_expression( const exprt &lhs, std::vector &aliasable_references) { - bool first_iter = true; - exprt running = false_exprt(); + exprt::operandst operands; + operands.reserve(aliasable_references.size()); for(auto aliasable : aliasable_references) { - exprt left_ptr = address_of_exprt{lhs}; - exprt right_ptr = aliasable; - exprt same = same_object(left_ptr, right_ptr); - - if(first_iter) - { - running = same; - first_iter = false; - } - else - { - exprt::operandst disjuncts; - disjuncts.push_back(same); - disjuncts.push_back(running); - running = disjunction(disjuncts); - } - } - - return running; -} - -void code_contractst::populate_assigns_references( - const symbolt &function_symbol, - const irep_idt &function_id, - goto_programt &created_decls, - std::vector &created_references) -{ - const auto &type = to_code_with_contract_type(function_symbol.type); - const exprt &assigns = type.assigns(); - - const exprt::operandst &targets = assigns.operands(); - for(const exprt &curr_op : targets) - { - // Declare a new symbol to stand in for the reference - symbol_exprt standin = new_tmp_symbol( - pointer_type(curr_op.type()), - function_symbol.location, - function_id, - function_symbol.mode) - .symbol_expr(); - - created_decls.add( - goto_programt::make_decl(standin, function_symbol.location)); - - created_decls.add(goto_programt::make_assignment( - code_assignt(standin, std::move(address_of_exprt{curr_op})), - function_symbol.location)); - - // Add a map entry from the original operand to the new symbol - created_references.push_back(standin); + operands.push_back(equal_exprt(lhs, typecast_exprt(aliasable, lhs.type()))); } + return disjunction(operands); } -void code_contractst::instrument_assigns_statement( +void code_contractst::instrument_assign_statement( goto_programt::instructionst::iterator &instruction_iterator, goto_programt &program, exprt &assigns, - std::vector &assigns_references, - std::set &freely_assignable_exprs) + std::set &freely_assignable_symbols, + assigns_clauset &assigns_clause) { INVARIANT( instruction_iterator->is_assign(), - "The first argument of instrument_assigns_statement should always be" + "The first instruction of instrument_assign_statement should always be" " an assignment"); + const exprt &lhs = instruction_iterator->get_assign().lhs(); - if(freely_assignable_exprs.find(lhs) != freely_assignable_exprs.end()) + + if( + lhs.id() == ID_symbol && + freely_assignable_symbols.find(to_symbol_expr(lhs).get_identifier()) != + freely_assignable_symbols.end()) { return; } - exprt alias_expr = create_alias_expression(assigns, lhs, assigns_references); goto_programt alias_assertion; alias_assertion.add(goto_programt::make_assertion( - alias_expr, instruction_iterator->source_location)); + assigns_clause.alias_expression(lhs), + instruction_iterator->source_location)); + + int lines_to_iterate = alias_assertion.instructions.size(); program.insert_before_swap(instruction_iterator, alias_assertion); - ++instruction_iterator; + std::advance(instruction_iterator, lines_to_iterate); } void code_contractst::instrument_call_statement( goto_programt::instructionst::iterator &instruction_iterator, goto_programt &program, exprt &assigns, - std::vector &aliasable_references, - std::set &freely_assignable_exprs) + const irep_idt &function_id, + std::set &freely_assignable_symbols, + assigns_clauset &assigns_clause) { INVARIANT( instruction_iterator->is_function_call(), "The first argument of instrument_call_statement should always be " "a function call"); + code_function_callt call = instruction_iterator->get_function_call(); const irep_idt &called_name = to_symbol_expr(call.function()).get_identifier(); - // Malloc allocates memory which is not part of the caller's memory - // frame, so we want to capture the newly-allocated memory and - // treat it as assignable. if(called_name == "malloc") { - aliasable_references.push_back(call.lhs()); - - // Make the variable, where result of malloc is stored, freely assignable. goto_programt::instructionst::iterator local_instruction_iterator = instruction_iterator; + // malloc statments return a void pointer, which is then cast and assigned + // to a result variable. We iterate one line forward to grab the result of + // the malloc once it is cast. local_instruction_iterator++; - if( - local_instruction_iterator->is_assign() && - local_instruction_iterator->get_assign().lhs().is_not_nil()) + if(local_instruction_iterator->is_assign()) { - freely_assignable_exprs.insert( - local_instruction_iterator->get_assign().lhs()); + const exprt &rhs = local_instruction_iterator->get_assign().rhs(); + INVARIANT( + rhs.id() == ID_typecast, + "malloc is called but the result is not cast. Excluding result from " + "the assignable memory frame."); + typet cast_type = rhs.type(); + + // Make freshly allocated memory assignable, if we can determine its type. + assigns_clause_targett *new_target = + assigns_clause.add_pointer_target(rhs); + goto_programt &pointer_capture = new_target->get_init_block(); + + int lines_to_iterate = pointer_capture.instructions.size(); + program.insert_before_swap(local_instruction_iterator, pointer_capture); + std::advance(instruction_iterator, lines_to_iterate + 1); } - return; // assume malloc edits no currently-existing memory objects. + return; // assume malloc edits no pre-existing memory objects. } - if(call.lhs().is_not_nil()) + if( + call.lhs().is_not_nil() && call.lhs().id() == ID_symbol && + freely_assignable_symbols.find( + to_symbol_expr(call.lhs()).get_identifier()) == + freely_assignable_symbols.end()) { - exprt alias_expr = - create_alias_expression(assigns, call.lhs(), aliasable_references); + exprt alias_expr = assigns_clause.alias_expression(call.lhs()); goto_programt alias_assertion; alias_assertion.add(goto_programt::make_assertion( @@ -454,41 +422,24 @@ void code_contractst::instrument_call_statement( ++instruction_iterator; } - // TODO we don't handle function pointers - if(call.function().id() == ID_symbol) - { - const symbolt &called_sym = ns.lookup(called_name); - const code_typet &called_type = to_code_type(called_sym.type); - - auto called_func = goto_functions.function_map.find(called_name); - if(called_func == goto_functions.function_map.end()) - { - log.error() << "Could not find function '" << called_name - << "' in goto-program; not enforcing assigns clause." - << messaget::eom; - return; - } + PRECONDITION(call.function().id() == ID_symbol); + const symbolt &called_symbol = ns.lookup(called_name); + const code_typet &called_type = to_code_type(called_symbol.type); - exprt called_assigns = - to_code_with_contract_type(called_sym.type).assigns(); - if(called_assigns.is_nil()) // Called function has no assigns clause - { - // Fail if called function has no assigns clause. - log.error() << "No assigns specification found for function '" - << called_name - << "' in goto-program; not enforcing assigns clause." - << messaget::eom; - - // Create a false assertion, so the analysis will fail if this function - // is called. - goto_programt failing_assertion; - failing_assertion.add(goto_programt::make_assertion( - false_exprt(), instruction_iterator->source_location)); - program.insert_before_swap(instruction_iterator, failing_assertion); - ++instruction_iterator; + exprt called_assigns = + to_code_with_contract_type(called_symbol.type).assigns(); + if(called_assigns.is_nil()) // Called function has no assigns clause + { + // Create a false assertion, so the analysis + // will fail if this function is called. + goto_programt failing_assertion; + failing_assertion.add(goto_programt::make_assertion( + false_exprt(), instruction_iterator->source_location)); + program.insert_before_swap(instruction_iterator, failing_assertion); + ++instruction_iterator; - return; - } + return; + } else // Called function has assigns clause { replace_symbolt replace; @@ -509,28 +460,18 @@ void code_contractst::instrument_call_statement( } replace(called_assigns); - for(exprt::operandst::const_iterator called_op_it = - called_assigns.operands().begin(); - called_op_it != called_assigns.operands().end(); - called_op_it++) - { - if( - freely_assignable_exprs.find(*called_op_it) != - freely_assignable_exprs.end()) - { - continue; - } - exprt alias_expr = - create_alias_expression(assigns, *called_op_it, aliasable_references); - - goto_programt alias_assertion; - alias_assertion.add(goto_programt::make_assertion( - alias_expr, instruction_iterator->source_location)); - program.insert_before_swap(instruction_iterator, alias_assertion); - ++instruction_iterator; - } + + // check compatibility of assigns clause with the called function + assigns_clauset called_assigns_clause( + called_assigns, *this, function_id, log); + exprt compatible = + assigns_clause.compatible_expression(called_assigns_clause); + goto_programt alias_assertion; + alias_assertion.add(goto_programt::make_assertion( + compatible, instruction_iterator->source_location)); + program.insert_before_swap(instruction_iterator, alias_assertion); + ++instruction_iterator; } - } } bool code_contractst::check_for_looped_mallocs(const goto_programt &program) @@ -539,7 +480,7 @@ bool code_contractst::check_for_looped_mallocs(const goto_programt &program) std::vector back_gotos; std::vector malloc_calls; - int idx = 0; + int index = 0; for(goto_programt::instructiont instruction : program.instructions) { if(instruction.is_backwards_goto()) @@ -557,10 +498,10 @@ bool code_contractst::check_for_looped_mallocs(const goto_programt &program) malloc_calls.push_back(instruction); } } - idx++; + index++; } - // Make sure there are no gotos that go back such that a malloc is between - // the goto and its destination (possible loop). + // Make sure there are no gotos that go back such that a malloc + // is between the goto and its destination (possible loop). for(auto goto_entry : back_gotos) { for(const auto &target : goto_entry.targets) @@ -571,14 +512,6 @@ bool code_contractst::check_for_looped_mallocs(const goto_programt &program) malloc_entry.location_number >= target->location_number && malloc_entry.location_number < goto_entry.location_number) { - // In order to statically keep track of all the memory we should - // be able to assign, we need to create ghost variables to store - // references to that memory. - // If a malloc is in a loop, we can't generally determine how many - // times it will run in order to create an appropriate number of - // references for the assignable memory. - // So, if we have a malloc in a loop, we can't statically create the - // assertion statements needed to enforce the assigns clause. log.error() << "Call to malloc at location " << malloc_entry.location_number << " falls between goto " << "source location " << goto_entry.location_number @@ -615,32 +548,32 @@ bool code_contractst::add_pointer_checks(const std::string &function_name) const symbolt &function_symbol = ns.lookup(function_id); const auto &type = to_code_with_contract_type(function_symbol.type); - exprt assigns = type.assigns(); - + exprt assigns_expr = type.assigns(); // Return if there are no reference checks to perform. - if(assigns.is_nil()) + if(assigns_expr.is_nil()) return false; - goto_programt::instructionst::iterator instruction_iterator = + assigns_clauset assigns(assigns_expr, *this, function_id, log); + + goto_programt::instructionst::iterator instruction_it = program.instructions.begin(); - // Create temporary variables to hold the assigns clause targets before - // they can be modified. - goto_programt standin_decls; - std::vector original_references; - populate_assigns_references( - function_symbol, function_id, standin_decls, original_references); + // Create temporary variables to hold the assigns + // clause targets before they can be modified. + goto_programt standin_decls = assigns.init_block(function_symbol.location); + goto_programt mark_dead = assigns.dead_stmts( + function_symbol.location, function_name, function_symbol.mode); // Create a list of variables that are okay to assign. - std::set freely_assignable_exprs; + std::set freely_assignable_symbols; for(code_typet::parametert param : type.parameters()) { - freely_assignable_exprs.insert(param); + freely_assignable_symbols.insert(param.get_identifier()); } int lines_to_iterate = standin_decls.instructions.size(); - program.insert_before_swap(instruction_iterator, standin_decls); - std::advance(instruction_iterator, lines_to_iterate); + program.insert_before_swap(instruction_it, standin_decls); + std::advance(instruction_it, lines_to_iterate); if(check_for_looped_mallocs(program)) { @@ -648,39 +581,62 @@ bool code_contractst::add_pointer_checks(const std::string &function_name) } // Insert aliasing assertions - for(; instruction_iterator != program.instructions.end(); - ++instruction_iterator) + for(; instruction_it != program.instructions.end(); ++instruction_it) { - if(instruction_iterator->is_decl()) + if(instruction_it->is_decl()) { - freely_assignable_exprs.insert(instruction_iterator->decl_symbol()); + freely_assignable_symbols.insert( + instruction_it->get_decl().symbol().get_identifier()); + + assigns_clause_targett *new_target = + assigns.add_target(instruction_it->get_decl().symbol()); + goto_programt &pointer_capture = new_target->get_init_block(); + + lines_to_iterate = pointer_capture.instructions.size(); + for(auto in : pointer_capture.instructions) + { + program.insert_after(instruction_it, in); + ++instruction_it; + } } - else if(instruction_iterator->is_assign()) + else if(instruction_it->is_assign()) { - instrument_assigns_statement( - instruction_iterator, + instrument_assign_statement( + instruction_it, program, - assigns, - original_references, - freely_assignable_exprs); + assigns_expr, + freely_assignable_symbols, + assigns); } - else if(instruction_iterator->is_function_call()) + else if(instruction_it->is_function_call()) { instrument_call_statement( - instruction_iterator, + instruction_it, program, - assigns, - original_references, - freely_assignable_exprs); + assigns_expr, + function_id, + freely_assignable_symbols, + assigns); } } + + // Walk the iterator back to the last statement + while(!instruction_it->is_end_function()) + { + --instruction_it; + } + + // Make sure the temporary symbols are marked dead + lines_to_iterate = mark_dead.instructions.size(); + program.insert_before_swap(instruction_it, mark_dead); + return false; } bool code_contractst::enforce_contract(const std::string &fun_to_enforce) { - // Add statements to the source function to ensure assigns clause is - // respected. + // Add statements to the source function + // to ensure assigns clause is respected. add_pointer_checks(fun_to_enforce); // Rename source function @@ -773,17 +729,12 @@ void code_contractst::add_contract_check( goto_programt check; - // if(nondet) - check.add(goto_programt::make_goto( - skip, - side_effect_expr_nondett(bool_typet(), skip->source_location), - skip->source_location)); - // prepare function call including all declarations code_function_callt call(function_symbol.symbol_expr()); replace_symbolt replace; // decl ret + code_returnt return_stmt; if(code_type.return_type() != empty_typet()) { symbol_exprt r = new_tmp_symbol( @@ -795,6 +746,7 @@ void code_contractst::add_contract_check( check.add(goto_programt::make_decl(r, skip->source_location)); call.lhs()=r; + return_stmt = code_returnt(r); symbol_exprt ret_val(CPROVER_PREFIX "return_value", call.lhs().type()); replace.insert(ret_val, r); @@ -818,6 +770,8 @@ void code_contractst::add_contract_check( parameter_symbol.mode) .symbol_expr(); check.add(goto_programt::make_decl(p, skip->source_location)); + check.add(goto_programt::make_assignment( + p, parameter_symbol.symbol_expr(), skip->source_location)); call.arguments().push_back(p); @@ -849,6 +803,11 @@ void code_contractst::add_contract_check( goto_programt::make_assertion(ensures_cond, ensures.source_location())); } + if(code_type.return_type() != empty_typet()) + { + check.add(goto_programt::make_return(return_stmt, skip->source_location)); + } + // prepend the new code to dest check.destructive_append(tmp_skip); dest.destructive_insert(dest.instructions.begin(), check); @@ -880,18 +839,22 @@ bool code_contractst::replace_calls( { const code_function_callt &call = ins->get_function_call(); - // TODO we don't handle function pointers + PRECONDITION(call.function().id() != ID_dereference); + if(call.function().id() != ID_symbol) continue; - const irep_idt &fun_name = + const irep_idt &function_name = to_symbol_expr(call.function()).get_identifier(); auto found = std::find( - funs_to_replace.begin(), funs_to_replace.end(), id2string(fun_name)); + funs_to_replace.begin(), + funs_to_replace.end(), + id2string(function_name)); if(found == funs_to_replace.end()) continue; - fail |= apply_function_contract(goto_function.second.body, ins); + fail |= apply_function_contract( + function_name, goto_function.second.body, ins); } } } @@ -961,3 +924,609 @@ bool code_contractst::enforce_contracts( } return fail; } + +assigns_clause_scalar_targett::assigns_clause_scalar_targett( + const exprt &object_ptr, + code_contractst &contract, + messaget &log_parameter, + const irep_idt &function_id) + : assigns_clause_targett( + Scalar, + pointer_for(object_ptr), + contract, + log_parameter), + local_standin_variable(typet()) +{ + const symbolt &function_symbol = contract.ns.lookup(function_id); + + // Declare a new symbol to stand in for the reference + symbolt standin_symbol = contract.new_tmp_symbol( + pointer_object.type(), + function_symbol.location, + function_id, + function_symbol.mode); + + local_standin_variable = standin_symbol.symbol_expr(); + + // Build standin variable initialization block + init_block.add( + goto_programt::make_decl(local_standin_variable, function_symbol.location)); + init_block.add(goto_programt::make_assignment( + code_assignt(local_standin_variable, pointer_object), + function_symbol.location)); +} + +std::vector +assigns_clause_scalar_targett::temporary_declarations() const +{ + std::vector result; + result.push_back(local_standin_variable); + return result; +} + +exprt assigns_clause_scalar_targett::alias_expression(const exprt &ptr) +{ + return same_object(ptr, local_standin_variable); +} + +exprt assigns_clause_scalar_targett::compatible_expression( + const assigns_clause_targett &called_target) +{ + if(called_target.target_type == Scalar) + { + return alias_expression(called_target.get_direct_pointer()); + } + else // Struct or Array + { + return false_exprt(); + } +} + +goto_programt +assigns_clause_scalar_targett::havoc_code(source_locationt location) const +{ + goto_programt assigns_havoc; + + exprt lhs = dereference_exprt(pointer_object); + side_effect_expr_nondett rhs(lhs.type(), location); + + goto_programt::targett target = + assigns_havoc.add(goto_programt::make_assignment( + code_assignt(std::move(lhs), std::move(rhs)), location)); + target->code_nonconst().add_source_location() = location; + + return assigns_havoc; +} + +assigns_clause_struct_targett::assigns_clause_struct_targett( + const exprt &object_ptr, + code_contractst &contract, + messaget &log_parameter, + const irep_idt &function_id) + : assigns_clause_targett( + Struct, + pointer_for(object_ptr), + contract, + log_parameter), + main_struct_standin(typet()) +{ + const symbolt &struct_symbol = + contract.ns.lookup(to_tag_type(object_ptr.type())); + const symbolt &function_symbol = contract.ns.lookup(function_id); + + // Declare a new symbol to stand in for the reference + symbolt struct_temp_symbol = contract.new_tmp_symbol( + pointer_object.type(), + function_symbol.location, + function_id, + function_symbol.mode); + main_struct_standin = struct_temp_symbol.symbol_expr(); + local_standin_variables.push_back(main_struct_standin); + + // Build standin variable initialization block + init_block.add( + goto_programt::make_decl(main_struct_standin, function_symbol.location)); + init_block.add(goto_programt::make_assignment( + code_assignt(main_struct_standin, pointer_object), + function_symbol.location)); + + // Handle component members + std::vector component_members; + const struct_typet &struct_type = to_struct_type(struct_symbol.type); + for(struct_union_typet::componentt component : struct_type.components()) + { + exprt current_member = member_exprt(object_ptr, component); + component_members.push_back(current_member); + } + + while(!component_members.empty()) + { + exprt current_operation = component_members.front(); + exprt operation_address = pointer_for(current_operation); + + // Declare a new symbol to stand in for the reference + symbolt standin_symbol = contract.new_tmp_symbol( + operation_address.type(), + function_symbol.location, + function_id, + function_symbol.mode); + + symbol_exprt current_standin = standin_symbol.symbol_expr(); + local_standin_variables.push_back(current_standin); + + // Add to standin variable initialization block + init_block.add( + goto_programt::make_decl(current_standin, function_symbol.location)); + init_block.add(goto_programt::make_assignment( + code_assignt(current_standin, operation_address), + function_symbol.location)); + + if(current_operation.type().id() == ID_struct_tag) + { + const symbolt ¤t_struct_symbol = + contract.ns.lookup(to_tag_type(current_operation.type())); + + const struct_typet &curr_struct_t = + to_struct_type(current_struct_symbol.type); + for(struct_union_typet::componentt component : curr_struct_t.components()) + { + exprt current_member = member_exprt(current_operation, component); + component_members.push_back(current_member); + } + } + component_members.erase(component_members.begin()); + } +} + +std::vector +assigns_clause_struct_targett::temporary_declarations() const +{ + return local_standin_variables; +} + +exprt assigns_clause_struct_targett::alias_expression(const exprt &ptr) +{ + exprt::operandst disjuncts; + disjuncts.reserve(local_standin_variables.size()); + for(symbol_exprt symbol : local_standin_variables) + { + const typet &ptr_concrete_type = to_pointer_type(ptr.type()).subtype(); + auto left_size = size_of_expr(ptr_concrete_type, contract.ns); + const typet &standin_concrete_type = + to_pointer_type(symbol.type()).subtype(); + auto right_size = size_of_expr(standin_concrete_type, contract.ns); + INVARIANT(left_size.has_value(), "Unable to determine size of type (lhs)."); + INVARIANT( + right_size.has_value(), "Unable to determine size of type (rhs)."); + if(*left_size == *right_size) + { + exprt same_obj = same_object(ptr, symbol); + exprt same_offset = + equal_exprt(pointer_offset(ptr), pointer_offset(symbol)); + + disjuncts.push_back(and_exprt{same_obj, same_offset}); + } + } + + return disjunction(disjuncts); +} + +exprt assigns_clause_struct_targett::compatible_expression( + const assigns_clause_targett &called_target) +{ + if(called_target.target_type == Scalar) + { + return alias_expression(called_target.get_direct_pointer()); + } + else if(called_target.target_type == Struct) + { + const assigns_clause_struct_targett &struct_target = + static_cast(called_target); + + exprt same_obj = + same_object(this->main_struct_standin, struct_target.pointer_object); + // the size of the called struct should be less than or + // equal to that of the assignable target struct. + exprt current_size = + get_size(this->pointer_object.type(), contract.ns, log); + exprt curr_upper_offset = + pointer_offset(plus_exprt(this->main_struct_standin, current_size)); + exprt called_size = + get_size(struct_target.pointer_object.type(), contract.ns, log); + exprt called_upper_offset = + pointer_offset(plus_exprt(struct_target.pointer_object, called_size)); + + exprt in_range_lower = binary_predicate_exprt( + pointer_offset(struct_target.pointer_object), + ID_ge, + pointer_offset(this->main_struct_standin)); + exprt in_range_upper = + binary_predicate_exprt(curr_upper_offset, ID_ge, called_upper_offset); + + exprt in_range = and_exprt(in_range_lower, in_range_upper); + return and_exprt(same_obj, in_range); + } + else // Array + { + return false_exprt(); + } +} + +goto_programt +assigns_clause_struct_targett::havoc_code(source_locationt location) const +{ + goto_programt assigns_havoc; + + exprt lhs = dereference_exprt(pointer_object); + side_effect_expr_nondett rhs(lhs.type(), location); + + goto_programt::targett target = + assigns_havoc.add(goto_programt::make_assignment( + code_assignt(std::move(lhs), std::move(rhs)), location)); + target->code_nonconst().add_source_location() = location; + + return assigns_havoc; +} + +assigns_clause_array_targett::assigns_clause_array_targett( + const exprt &object_ptr, + code_contractst &contract, + messaget &log_parameter, + const irep_idt &function_id) + : assigns_clause_targett(Array, object_ptr, contract, log_parameter), + lower_offset_object(), + upper_offset_object(), + array_standin_variable(typet()), + lower_offset_variable(typet()), + upper_offset_variable(typet()) +{ + const symbolt &function_symbol = contract.ns.lookup(function_id); + + // Declare a new symbol to stand in for the reference + symbolt standin_symbol = contract.new_tmp_symbol( + pointer_object.type(), + function_symbol.location, + function_id, + function_symbol.mode); + + array_standin_variable = standin_symbol.symbol_expr(); + + // Add array temp to variable initialization block + init_block.add( + goto_programt::make_decl(array_standin_variable, function_symbol.location)); + init_block.add(goto_programt::make_assignment( + code_assignt(array_standin_variable, pointer_object), + function_symbol.location)); + + if(object_ptr.id() == ID_address_of) + { + exprt constant_size = + get_size(object_ptr.type().subtype(), contract.ns, log); + lower_offset_object = typecast_exprt( + mult_exprt( + typecast_exprt(object_ptr, unsigned_long_int_type()), constant_size), + signed_int_type()); + + // Declare a new symbol to stand in for the reference + symbolt lower_standin_symbol = contract.new_tmp_symbol( + lower_offset_object.type(), + function_symbol.location, + function_id, + function_symbol.mode); + + lower_offset_variable = lower_standin_symbol.symbol_expr(); + + // Add array temp to variable initialization block + init_block.add(goto_programt::make_decl( + lower_offset_variable, function_symbol.location)); + init_block.add(goto_programt::make_assignment( + code_assignt(lower_offset_variable, lower_offset_object), + function_symbol.location)); + + upper_offset_object = typecast_exprt( + mult_exprt( + typecast_exprt(object_ptr, unsigned_long_int_type()), constant_size), + signed_int_type()); + + // Declare a new symbol to stand in for the reference + symbolt upper_standin_symbol = contract.new_tmp_symbol( + upper_offset_object.type(), + function_symbol.location, + function_id, + function_symbol.mode); + + upper_offset_variable = upper_standin_symbol.symbol_expr(); + + // Add array temp to variable initialization block + init_block.add(goto_programt::make_decl( + upper_offset_variable, function_symbol.location)); + init_block.add(goto_programt::make_assignment( + code_assignt(upper_offset_variable, upper_offset_object), + function_symbol.location)); + } +} + +std::vector +assigns_clause_array_targett::temporary_declarations() const +{ + std::vector result; + result.push_back(array_standin_variable); + result.push_back(lower_offset_variable); + result.push_back(upper_offset_variable); + + return result; +} + +goto_programt +assigns_clause_array_targett::havoc_code(source_locationt location) const +{ + goto_programt assigns_havoc; + + modifiest assigns_tgts; + typet lower_type = lower_offset_variable.type(); + exprt array_type_size = + get_size(pointer_object.type().subtype(), contract.ns, log); + + for(mp_integer i = lower_bound; i < upper_bound; ++i) + { + irep_idt offset_string(from_integer(i, integer_typet()).get_value()); + irep_idt offset_irep(offset_string); + constant_exprt val_const(offset_irep, lower_type); + dereference_exprt array_deref(plus_exprt( + pointer_object, typecast_exprt(val_const, signed_long_int_type()))); + + assigns_tgts.insert(array_deref); + } + + for(auto lhs : assigns_tgts) + { + side_effect_expr_nondett rhs(lhs.type(), location); + + goto_programt::targett target = + assigns_havoc.add(goto_programt::make_assignment( + code_assignt(std::move(lhs), std::move(rhs)), location)); + target->code_nonconst().add_source_location() = location; + } + + return assigns_havoc; +} + +exprt assigns_clause_array_targett::alias_expression(const exprt &ptr) +{ + exprt ptr_offset = pointer_offset(ptr); + exprt::operandst conjuncts; + + conjuncts.push_back(same_object(ptr, array_standin_variable)); + conjuncts.push_back(binary_predicate_exprt( + ptr_offset, + ID_ge, + typecast_exprt(lower_offset_variable, ptr_offset.type()))); + conjuncts.push_back(binary_predicate_exprt( + typecast_exprt(upper_offset_variable, ptr_offset.type()), + ID_ge, + ptr_offset)); + + return conjunction(conjuncts); +} + +exprt assigns_clause_array_targett::compatible_expression( + const assigns_clause_targett &called_target) +{ + if(called_target.target_type == Scalar) + { + return alias_expression(called_target.get_direct_pointer()); + } + else if(called_target.target_type == Array) + { + const assigns_clause_array_targett &array_target = + static_cast(called_target); + exprt same_obj = + same_object(this->array_standin_variable, array_target.pointer_object); + exprt in_range_lower = binary_predicate_exprt( + array_target.lower_offset_object, ID_ge, this->lower_offset_variable); + exprt in_range_upper = binary_predicate_exprt( + this->upper_offset_variable, ID_ge, array_target.upper_offset_object); + exprt in_range = and_exprt(in_range_lower, in_range_upper); + return and_exprt(same_obj, in_range); + } + else // Struct + { + return false_exprt(); + } +} + +assigns_clauset::assigns_clauset( + const exprt &assigns, + code_contractst &contract, + const irep_idt function_id, + messaget log_parameter) + : assigns_expr(assigns), + parent(contract), + function_id(function_id), + log(log_parameter) +{ + for(exprt current_operation : assigns_expr.operands()) + { + add_target(current_operation); + } +} +assigns_clauset::~assigns_clauset() +{ + for(assigns_clause_targett *target : targets) + { + delete target; + } +} + +assigns_clause_targett *assigns_clauset::add_target(exprt current_operation) +{ + if(current_operation.id() == ID_address_of) + { + assigns_clause_array_targett *array_target = + new assigns_clause_array_targett( + current_operation, parent, log, function_id); + targets.push_back(array_target); + return array_target; + } + else if(current_operation.type().id() == ID_struct_tag) + { + assigns_clause_struct_targett *struct_target = + new assigns_clause_struct_targett( + current_operation, parent, log, function_id); + targets.push_back(struct_target); + return struct_target; + } + else + { + assigns_clause_scalar_targett *scalar_target = + new assigns_clause_scalar_targett( + current_operation, parent, log, function_id); + targets.push_back(scalar_target); + return scalar_target; + } +} + +assigns_clause_targett * +assigns_clauset::add_pointer_target(exprt current_operation) +{ + return add_target(dereference_exprt(current_operation)); +} + +goto_programt assigns_clauset::init_block(source_locationt location) +{ + goto_programt result; + for(assigns_clause_targett *target : targets) + { + for(goto_programt::instructiont inst : + target->get_init_block().instructions) + { + result.add(goto_programt::instructiont(inst)); + } + } + return result; +} + +goto_programt &assigns_clauset::temporary_declarations( + source_locationt location, + irep_idt function_name, + irep_idt language_mode) +{ + if(standin_declarations.empty()) + { + for(assigns_clause_targett *target : targets) + { + for(symbol_exprt symbol : target->temporary_declarations()) + { + standin_declarations.add( + goto_programt::make_decl(symbol, symbol.source_location())); + } + } + } + return standin_declarations; +} + +goto_programt assigns_clauset::dead_stmts( + source_locationt location, + irep_idt function_name, + irep_idt language_mode) +{ + goto_programt dead_statements; + for(assigns_clause_targett *target : targets) + { + for(symbol_exprt symbol : target->temporary_declarations()) + { + dead_statements.add( + goto_programt::make_dead(symbol, symbol.source_location())); + } + } + return dead_statements; +} + +goto_programt assigns_clauset::havoc_code( + source_locationt location, + irep_idt function_name, + irep_idt language_mode) +{ + goto_programt havoc_statements; + for(assigns_clause_targett *target : targets) + { + for(goto_programt::instructiont instruction : + target->havoc_code(location).instructions) + { + havoc_statements.add(std::move(instruction)); + } + } + return havoc_statements; +} + +exprt assigns_clauset::alias_expression(const exprt &lhs) +{ + if(targets.empty()) + { + return false_exprt(); + } + + exprt left_ptr = assigns_clause_targett::pointer_for(lhs); + + bool first_iter = true; + exprt result = false_exprt(); + for(assigns_clause_targett *target : targets) + { + if(first_iter) + { + result = target->alias_expression(left_ptr); + first_iter = false; + } + else + { + result = or_exprt(result, target->alias_expression(left_ptr)); + } + } + return result; +} + +exprt assigns_clauset::compatible_expression( + const assigns_clauset &called_assigns) +{ + if(called_assigns.targets.empty()) + { + return true_exprt(); + } + + bool first_clause = true; + exprt result = true_exprt(); + for(assigns_clause_targett *called_target : called_assigns.targets) + { + bool first_iter = true; + exprt current_target_compatible = false_exprt(); + for(assigns_clause_targett *target : targets) + { + if(first_iter) + { + current_target_compatible = + target->compatible_expression(*called_target); + first_iter = false; + } + else + { + current_target_compatible = or_exprt( + current_target_compatible, + target->compatible_expression(*called_target)); + } + } + if(first_clause) + { + result = current_target_compatible; + first_clause = false; + } + else + { + exprt::operandst conjuncts; + conjuncts.push_back(result); + conjuncts.push_back(current_target_compatible); + result = conjunction(conjuncts); + } + } + + return result; +} diff --git a/src/goto-instrument/code_contracts.h b/src/goto-instrument/code_contracts.h index 74c084b2e0e..402885ecf5e 100644 --- a/src/goto-instrument/code_contracts.h +++ b/src/goto-instrument/code_contracts.h @@ -21,9 +21,13 @@ Date: February 2016 #include #include +#include +#include #include +#include class messaget; +class assigns_clauset; class code_contractst { @@ -79,8 +83,15 @@ class code_contractst /// \return `true` on failure, `false` otherwise bool replace_calls(); -protected: + const symbolt &new_tmp_symbol( + const typet &type, + const source_locationt &source_location, + const irep_idt &function_id, + const irep_idt &mode); + namespacet ns; + +protected: symbol_tablet &symbol_table; goto_functionst &goto_functions; @@ -100,16 +111,16 @@ class code_contractst /// a goto statement that jumps back. bool check_for_looped_mallocs(const goto_programt &); - /// Inserts an assertion statement into program before the assignment ins_it, - /// to ensure that the left-hand-side of the assignment aliases some - /// expression in original_references, unless it is contained in - /// freely_assignable_exprs. - void instrument_assigns_statement( - goto_programt::instructionst::iterator &ins_it, + /// Inserts an assertion statement into program before the assignment + /// instruction_it, to ensure that the left-hand-side of the assignment + /// aliases some expression in original_references, unless it is contained + /// in freely_assignable_exprs. + void instrument_assign_statement( + goto_programt::instructionst::iterator &instruction_it, goto_programt &program, exprt &assigns, - std::vector &original_references, - std::set &freely_assignable_exprs); + std::set &freely_assignable_symbols, + assigns_clauset &assigns_clause); /// Inserts an assertion statement into program before the function call at /// ins_it, to ensure that any memory which may be written by the call is @@ -119,37 +130,41 @@ class code_contractst goto_programt::instructionst::iterator &ins_it, goto_programt &program, exprt &assigns, - std::vector &assigns_references, - std::set &freely_assignable_exprs); + const irep_idt &function_id, + std::set &freely_assignable_symbols, + assigns_clauset &assigns_clause); - /// Creates a local variable declaration for each expression in the assigns - /// clause (of the function given by f_sym), and stores them in created_decls. - /// Then creates assignment statements to capture the memory addresses of each - /// expression in the assigns clause within the associated local variable, + /// Creates a local variable declaration for each expression in operands, + /// and stores them in created_declarations. Then creates assignment + /// statements to capture the memory addresses of each expression + /// in the assigns clause within the associated local variable, /// populating a vector created_references of these local variables. - void populate_assigns_references( - const symbolt &f_sym, - const irep_idt &func_id, - goto_programt &created_decls, + void populate_assigns_reference( + std::vector operands, + const symbolt &function_symbol, + const irep_idt &function_id, + goto_programt &created_declarations, std::vector &created_references); + /// Creates a boolean expression which is true when there exists an expression + /// in aliasable_references with the same pointer object and pointer offset as + /// the address of lhs. + exprt create_alias_expression( + const exprt &lhs, + std::vector &aliasable_references); + void apply_loop_contract(goto_functionst::goto_functiont &goto_function); /// \brief Does the named function have a contract? bool has_contract(const irep_idt); bool apply_function_contract( + const irep_idt &function_id, goto_programt &goto_program, goto_programt::targett target); void add_contract_check(const irep_idt &, const irep_idt &, goto_programt &dest); - - const symbolt &new_tmp_symbol( - const typet &type, - const source_locationt &source_location, - const irep_idt &function_id, - const irep_idt &mode); }; #define FLAG_REPLACE_CALL "replace-call-with-contract" @@ -170,4 +185,168 @@ class code_contractst #define HELP_ENFORCE_ALL_CONTRACTS \ " --enforce-all-contracts as above for all functions with a contract\n" +/// \brief A base class for assigns clause targets +class assigns_clause_targett +{ +public: + enum target_type + { + Scalar, + Struct, + Array + }; + + assigns_clause_targett( + target_type type, + const exprt object_ptr, + const code_contractst &contract, + messaget &log_parameter) + : target_type(type), + pointer_object(object_ptr), + contract(contract), + init_block(), + log(log_parameter) + { + INVARIANT( + pointer_object.type().id() == ID_pointer, + "Assigns clause targets should be stored as pointer expressions."); + } + + virtual ~assigns_clause_targett() + { + } + + virtual std::vector temporary_declarations() const = 0; + virtual exprt alias_expression(const exprt &lhs) = 0; + virtual exprt + compatible_expression(const assigns_clause_targett &called_target) = 0; + virtual goto_programt havoc_code(source_locationt location) const = 0; + + const exprt &get_direct_pointer() const + { + return pointer_object; + } + + goto_programt &get_init_block() + { + return init_block; + } + + static exprt pointer_for(const exprt &exp) + { + return address_of_exprt(exp); + } + + const target_type target_type; + +protected: + const exprt pointer_object; + const code_contractst &contract; + goto_programt init_block; + messaget &log; +}; + +class assigns_clause_scalar_targett : public assigns_clause_targett +{ +public: + assigns_clause_scalar_targett( + const exprt &object_ptr, + code_contractst &contract, + messaget &log_parameter, + const irep_idt &function_id); + + std::vector temporary_declarations() const; + exprt alias_expression(const exprt &lhs); + exprt compatible_expression(const assigns_clause_targett &called_target); + goto_programt havoc_code(source_locationt location) const; + +protected: + symbol_exprt local_standin_variable; +}; + +class assigns_clause_struct_targett : public assigns_clause_targett +{ +public: + assigns_clause_struct_targett( + const exprt &object_ptr, + code_contractst &contract, + messaget &log_parameter, + const irep_idt &function_id); + + std::vector temporary_declarations() const; + exprt alias_expression(const exprt &lhs); + exprt compatible_expression(const assigns_clause_targett &called_target); + goto_programt havoc_code(source_locationt location) const; + +protected: + symbol_exprt main_struct_standin; + std::vector local_standin_variables; +}; + +class assigns_clause_array_targett : public assigns_clause_targett +{ +public: + assigns_clause_array_targett( + const exprt &object_ptr, + code_contractst &contract, + messaget &log_parameter, + const irep_idt &function_id); + + std::vector temporary_declarations() const; + exprt alias_expression(const exprt &lhs); + exprt compatible_expression(const assigns_clause_targett &called_target); + goto_programt havoc_code(source_locationt location) const; + +protected: + mp_integer lower_bound; + mp_integer upper_bound; + + exprt lower_offset_object; + exprt upper_offset_object; + + symbol_exprt array_standin_variable; + symbol_exprt lower_offset_variable; + symbol_exprt upper_offset_variable; +}; + +class assigns_clauset +{ +public: + assigns_clauset( + const exprt &assigns, + code_contractst &contract, + const irep_idt function_id, + messaget log_parameter); + ~assigns_clauset(); + + assigns_clause_targett *add_target(exprt current_operation); + assigns_clause_targett *add_pointer_target(exprt current_operation); + goto_programt init_block(source_locationt location); + goto_programt &temporary_declarations( + source_locationt location, + irep_idt function_name, + irep_idt language_mode); + goto_programt dead_stmts( + source_locationt location, + irep_idt function_name, + irep_idt language_mode); + goto_programt havoc_code( + source_locationt location, + irep_idt function_name, + irep_idt language_mode); + exprt alias_expression(const exprt &lhs); + + exprt compatible_expression(const assigns_clauset &called_assigns); + +protected: + const exprt &assigns_expr; + + std::vector targets; + goto_programt standin_declarations; + + code_contractst &parent; + const irep_idt function_id; + messaget log; +}; + #endif // CPROVER_GOTO_INSTRUMENT_CODE_CONTRACTS_H