From f567e02dc1597841a6cafffab86db55726076442 Mon Sep 17 00:00:00 2001 From: Christopher Wagner Date: Tue, 30 Jun 2020 16:50:54 -0400 Subject: [PATCH 1/5] Add scalar assigns clause to code contracts. Expanding CBMC code contracts to include an assigns clause for scalar variables and their pointers. --- doc/cprover-manual/assigns-clause.md | 51 ++ .../contracts/assigns_enforce_01/main.c | 21 + .../contracts/assigns_enforce_01/test.desc | 13 + .../contracts/assigns_enforce_02/main.c | 18 + .../contracts/assigns_enforce_02/test.desc | 9 + .../contracts/assigns_enforce_03/main.c | 28 + .../contracts/assigns_enforce_03/test.desc | 9 + .../contracts/assigns_enforce_04/main.c | 28 + .../contracts/assigns_enforce_04/test.desc | 9 + .../contracts/assigns_enforce_05/main.c | 25 + .../contracts/assigns_enforce_05/test.desc | 9 + .../contracts/assigns_enforce_06/main.c | 43 ++ .../contracts/assigns_enforce_06/test.desc | 9 + .../contracts/assigns_enforce_07/main.c | 43 ++ .../contracts/assigns_enforce_07/test.desc | 9 + .../contracts/assigns_enforce_08/main.c | 19 + .../contracts/assigns_enforce_08/test.desc | 9 + .../contracts/assigns_enforce_09/main.c | 19 + .../contracts/assigns_enforce_09/test.desc | 9 + .../contracts/assigns_enforce_10/main.c | 22 + .../contracts/assigns_enforce_10/test.desc | 9 + .../contracts/assigns_enforce_11/main.c | 22 + .../contracts/assigns_enforce_11/test.desc | 9 + .../contracts/assigns_enforce_12/main.c | 15 + .../contracts/assigns_enforce_12/test.desc | 9 + .../contracts/assigns_enforce_13/main.c | 16 + .../contracts/assigns_enforce_13/test.desc | 9 + .../assigns_enforce_malloc_01/main.c | 16 + .../assigns_enforce_malloc_01/test.desc | 9 + .../assigns_enforce_malloc_02/main.c | 19 + .../assigns_enforce_malloc_02/test.desc | 9 + .../assigns_enforce_scoping_01/main.c | 20 + .../assigns_enforce_scoping_01/test.desc | 11 + .../assigns_enforce_scoping_02/main.c | 20 + .../assigns_enforce_scoping_02/test.desc | 11 + .../contracts/assigns_replace_01/main.c | 15 + .../contracts/assigns_replace_01/test.desc | 9 + .../contracts/assigns_replace_02/main.c | 16 + .../contracts/assigns_replace_02/test.desc | 9 + .../contracts/assigns_replace_03/main.c | 17 + .../contracts/assigns_replace_03/test.desc | 9 + .../contracts/assigns_replace_04/main.c | 33 + .../contracts/assigns_replace_04/test.desc | 9 + .../contracts/assigns_replace_05/main.c | 33 + .../contracts/assigns_replace_05/test.desc | 11 + .../contracts/function_check_01/test.desc | 8 +- src/ansi-c/c_typecheck_base.cpp | 29 +- src/ansi-c/c_typecheck_base.h | 5 + src/ansi-c/c_typecheck_code.cpp | 67 +- src/ansi-c/c_typecheck_expr.cpp | 7 +- src/ansi-c/parser.y | 44 +- src/ansi-c/scanner.l | 1 + src/goto-instrument/code_contracts.cpp | 574 +++++++++++++++--- src/goto-instrument/code_contracts.h | 41 ++ src/util/irep_ids.def | 2 + 55 files changed, 1448 insertions(+), 97 deletions(-) create mode 100644 doc/cprover-manual/assigns-clause.md create mode 100644 regression/contracts/assigns_enforce_01/main.c create mode 100644 regression/contracts/assigns_enforce_01/test.desc create mode 100644 regression/contracts/assigns_enforce_02/main.c create mode 100644 regression/contracts/assigns_enforce_02/test.desc create mode 100644 regression/contracts/assigns_enforce_03/main.c create mode 100644 regression/contracts/assigns_enforce_03/test.desc create mode 100644 regression/contracts/assigns_enforce_04/main.c create mode 100644 regression/contracts/assigns_enforce_04/test.desc create mode 100644 regression/contracts/assigns_enforce_05/main.c create mode 100644 regression/contracts/assigns_enforce_05/test.desc create mode 100644 regression/contracts/assigns_enforce_06/main.c create mode 100644 regression/contracts/assigns_enforce_06/test.desc create mode 100644 regression/contracts/assigns_enforce_07/main.c create mode 100644 regression/contracts/assigns_enforce_07/test.desc create mode 100644 regression/contracts/assigns_enforce_08/main.c create mode 100644 regression/contracts/assigns_enforce_08/test.desc create mode 100644 regression/contracts/assigns_enforce_09/main.c create mode 100644 regression/contracts/assigns_enforce_09/test.desc create mode 100644 regression/contracts/assigns_enforce_10/main.c create mode 100644 regression/contracts/assigns_enforce_10/test.desc create mode 100644 regression/contracts/assigns_enforce_11/main.c create mode 100644 regression/contracts/assigns_enforce_11/test.desc create mode 100644 regression/contracts/assigns_enforce_12/main.c create mode 100644 regression/contracts/assigns_enforce_12/test.desc create mode 100644 regression/contracts/assigns_enforce_13/main.c create mode 100644 regression/contracts/assigns_enforce_13/test.desc create mode 100644 regression/contracts/assigns_enforce_malloc_01/main.c create mode 100644 regression/contracts/assigns_enforce_malloc_01/test.desc create mode 100644 regression/contracts/assigns_enforce_malloc_02/main.c create mode 100644 regression/contracts/assigns_enforce_malloc_02/test.desc create mode 100644 regression/contracts/assigns_enforce_scoping_01/main.c create mode 100644 regression/contracts/assigns_enforce_scoping_01/test.desc create mode 100644 regression/contracts/assigns_enforce_scoping_02/main.c create mode 100644 regression/contracts/assigns_enforce_scoping_02/test.desc create mode 100644 regression/contracts/assigns_replace_01/main.c create mode 100644 regression/contracts/assigns_replace_01/test.desc create mode 100644 regression/contracts/assigns_replace_02/main.c create mode 100644 regression/contracts/assigns_replace_02/test.desc create mode 100644 regression/contracts/assigns_replace_03/main.c create mode 100644 regression/contracts/assigns_replace_03/test.desc create mode 100644 regression/contracts/assigns_replace_04/main.c create mode 100644 regression/contracts/assigns_replace_04/test.desc create mode 100644 regression/contracts/assigns_replace_05/main.c create mode 100644 regression/contracts/assigns_replace_05/test.desc diff --git a/doc/cprover-manual/assigns-clause.md b/doc/cprover-manual/assigns-clause.md new file mode 100644 index 00000000000..f40fcbe6500 --- /dev/null +++ b/doc/cprover-manual/assigns-clause.md @@ -0,0 +1,51 @@ +## CBMC Assigns Clause + +### Introduction +Here is described the syntax and semantics of the "assigns" clause as implemented in CBMC. This construct 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 captured by the assigns clause must not be written within the given scope, even if the value(s) therein are not modified. + +### Scalar Variables +The initial iteration of this design focuses on specifying an assigns clause for simple variable types and their pointers. Arrays, structured data, and pointers are left to future contributions. + + +##### Syntax +A special construct is introduced to specify assigns clauses. Its syntax is defined as follows. + +``` + := __CPROVER_assigns ( ) +``` +``` + := + | , +``` +``` + := + | * +``` + + +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. + +##### 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 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. + +Let the ith expression in some assigns clause *c* be denoted *exprs**c*[i], the jth formal parameter of some function *f* be denoted *params**f*[j], and the kth argument passed 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. + +###### 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 is a predicate indicating that the two pointers reference the same object in the CBMC memory model. Additionally, for each function call without an assigns clause, 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. + + + diff --git a/regression/contracts/assigns_enforce_01/main.c b/regression/contracts/assigns_enforce_01/main.c new file mode 100644 index 00000000000..786f9990813 --- /dev/null +++ b/regression/contracts/assigns_enforce_01/main.c @@ -0,0 +1,21 @@ +#include + +int z; + +// z is not assigned, but it *may* be assigned. +// The assigns clause does not need to exactly match the +// set of variables which are assigned in the function. +int foo(int *x) __CPROVER_assigns(z, *x) + __CPROVER_ensures(__CPROVER_return_value == *x + 5) +{ + *x = *x + 0; + return *x + 5; +} + +int main() +{ + int n = 4; + n = foo(&n); + + return 0; +} diff --git a/regression/contracts/assigns_enforce_01/test.desc b/regression/contracts/assigns_enforce_01/test.desc new file mode 100644 index 00000000000..7c24b33faf7 --- /dev/null +++ b/regression/contracts/assigns_enforce_01/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks that verification succeeds if only expressions inside the assigns clause are assigned within the function. + +Note: For all 'enforce' tests, nothing can be assumed about the return value of the function (as the function call is not replaced at this point). + +To make such assumptions would cause verification to fail. diff --git a/regression/contracts/assigns_enforce_02/main.c b/regression/contracts/assigns_enforce_02/main.c new file mode 100644 index 00000000000..6062fa60282 --- /dev/null +++ b/regression/contracts/assigns_enforce_02/main.c @@ -0,0 +1,18 @@ +#include + +int z; + +int foo(int *x) __CPROVER_assigns(z) + __CPROVER_ensures(__CPROVER_return_value == *x + 5) +{ + *x = *x + 0; + return *x + 5; +} + +int main() +{ + int n = 4; + n = foo(&n); + + return 0; +} diff --git a/regression/contracts/assigns_enforce_02/test.desc b/regression/contracts/assigns_enforce_02/test.desc new file mode 100644 index 00000000000..f0dbbe8ceaa --- /dev/null +++ b/regression/contracts/assigns_enforce_02/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +This test checks that verification fails if an expression outside the assigns clause is assigned within the function. diff --git a/regression/contracts/assigns_enforce_03/main.c b/regression/contracts/assigns_enforce_03/main.c new file mode 100644 index 00000000000..293f69d2d89 --- /dev/null +++ b/regression/contracts/assigns_enforce_03/main.c @@ -0,0 +1,28 @@ +#include + +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(*x3, *y3, *z3) +{ + *x3 = *x3 + 1; + *y3 = *y3 + 1; + *z3 = *z3 + 1; +} + +int main() +{ + int p = 1; + int q = 2; + int r = 3; + f1(&p, &q, &r); + + return 0; +} diff --git a/regression/contracts/assigns_enforce_03/test.desc b/regression/contracts/assigns_enforce_03/test.desc new file mode 100644 index 00000000000..05315288ad2 --- /dev/null +++ b/regression/contracts/assigns_enforce_03/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks that verification succeeds when assigns clauses are respected through multiple function calls. diff --git a/regression/contracts/assigns_enforce_04/main.c b/regression/contracts/assigns_enforce_04/main.c new file mode 100644 index 00000000000..4964f30cd8e --- /dev/null +++ b/regression/contracts/assigns_enforce_04/main.c @@ -0,0 +1,28 @@ +#include + +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; +} + +int main() +{ + int p = 1; + int q = 2; + int r = 3; + f1(&p, &q, &r); + + return 0; +} diff --git a/regression/contracts/assigns_enforce_04/test.desc b/regression/contracts/assigns_enforce_04/test.desc new file mode 100644 index 00000000000..ce340df66a7 --- /dev/null +++ b/regression/contracts/assigns_enforce_04/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +This test checks that verification fails when an assigns clause is not respected through multiple function calls. diff --git a/regression/contracts/assigns_enforce_05/main.c b/regression/contracts/assigns_enforce_05/main.c new file mode 100644 index 00000000000..73830619f9b --- /dev/null +++ b/regression/contracts/assigns_enforce_05/main.c @@ -0,0 +1,25 @@ +#include + +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) +{ +} + +int main() +{ + int p = 1; + int q = 2; + int r = 3; + f1(&p, &q, &r); + + return 0; +} diff --git a/regression/contracts/assigns_enforce_05/test.desc b/regression/contracts/assigns_enforce_05/test.desc new file mode 100644 index 00000000000..52c7a660e1f --- /dev/null +++ b/regression/contracts/assigns_enforce_05/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +This test checks that verification fails when a function with an assigns clause calls a function without an assigns clause. diff --git a/regression/contracts/assigns_enforce_06/main.c b/regression/contracts/assigns_enforce_06/main.c new file mode 100644 index 00000000000..a330fefee8d --- /dev/null +++ b/regression/contracts/assigns_enforce_06/main.c @@ -0,0 +1,43 @@ +#include + +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(*x3, *y3, *z3) +{ + *x3 = *x3 + 1; + *y3 = *y3 + 1; + *z3 = *z3 + 1; +} + +int main() +{ + int p = 1; + int q = 2; + int r = 3; + + for(int i = 0; i < 3; ++i) + { + if(i == 0) + { + f1(&p, &q, &r); + } + if(i == 1) + { + f2(&p, &q, &r); + } + if(i == 2) + { + f3(&p, &q, &r); + } + } + + return 0; +} diff --git a/regression/contracts/assigns_enforce_06/test.desc b/regression/contracts/assigns_enforce_06/test.desc new file mode 100644 index 00000000000..42959abee29 --- /dev/null +++ b/regression/contracts/assigns_enforce_06/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks that verification succeeds when functions with assigns clauses are called from within a loop. diff --git a/regression/contracts/assigns_enforce_07/main.c b/regression/contracts/assigns_enforce_07/main.c new file mode 100644 index 00000000000..50fe90deea3 --- /dev/null +++ b/regression/contracts/assigns_enforce_07/main.c @@ -0,0 +1,43 @@ +#include + +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; +} + +int main() +{ + int p = 1; + int q = 2; + int r = 3; + + for(int i = 0; i < 3; ++i) + { + if(i == 0) + { + f1(&p, &q, &r); + } + if(i == 1) + { + f2(&p, &q, &r); + } + if(i == 2) + { + f3(&p, &q, &r); + } + } + + return 0; +} diff --git a/regression/contracts/assigns_enforce_07/test.desc b/regression/contracts/assigns_enforce_07/test.desc new file mode 100644 index 00000000000..00878112f4c --- /dev/null +++ b/regression/contracts/assigns_enforce_07/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +This test checks that verification fails when functions with assigns clauses are called within a loop and one of them does not obey its assigns clause. diff --git a/regression/contracts/assigns_enforce_08/main.c b/regression/contracts/assigns_enforce_08/main.c new file mode 100644 index 00000000000..286dd50650f --- /dev/null +++ b/regression/contracts/assigns_enforce_08/main.c @@ -0,0 +1,19 @@ +#include + +void f1(int *x) __CPROVER_assigns(*x) +{ + int *a = x; + f2(&a); +} +void f2(int **y) __CPROVER_assigns(**y) +{ + **y = 5; +} + +int main() +{ + int n = 3; + f1(&n); + + return 0; +} diff --git a/regression/contracts/assigns_enforce_08/test.desc b/regression/contracts/assigns_enforce_08/test.desc new file mode 100644 index 00000000000..9799f7ee5aa --- /dev/null +++ b/regression/contracts/assigns_enforce_08/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks that verification succeeds when a function with an assigns clause calls another with an additional level of indirection, and that functions respects the assigns clause of the caller. diff --git a/regression/contracts/assigns_enforce_09/main.c b/regression/contracts/assigns_enforce_09/main.c new file mode 100644 index 00000000000..a1135d31341 --- /dev/null +++ b/regression/contracts/assigns_enforce_09/main.c @@ -0,0 +1,19 @@ +#include + +void f1(int **x) __CPROVER_assigns(*x) +{ + f2(x); +} +void f2(int **y) __CPROVER_assigns(**y) +{ + **y = 5; +} + +int main() +{ + int p = 3; + int *q = &p; + f1(&q); + + return 0; +} diff --git a/regression/contracts/assigns_enforce_09/test.desc b/regression/contracts/assigns_enforce_09/test.desc new file mode 100644 index 00000000000..da304d4adc9 --- /dev/null +++ b/regression/contracts/assigns_enforce_09/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +This test checks that verification fails when a function with an assigns clause calls another with an assigns clause that adds one too many dereferences. diff --git a/regression/contracts/assigns_enforce_10/main.c b/regression/contracts/assigns_enforce_10/main.c new file mode 100644 index 00000000000..4398c4f9ac2 --- /dev/null +++ b/regression/contracts/assigns_enforce_10/main.c @@ -0,0 +1,22 @@ +#include + +void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1) +{ + f2(x1, y1, z1); +} + +void f2(int *x2, int *y2, int *z2) __CPROVER_assigns(*y2, *z2) +{ + *y2 = 5; + *z2 = 5; +} + +int main() +{ + int p = 1; + int q = 2; + int r = 3; + f1(&p, &q, &r); + + return 0; +} diff --git a/regression/contracts/assigns_enforce_10/test.desc b/regression/contracts/assigns_enforce_10/test.desc new file mode 100644 index 00000000000..4dab3e42137 --- /dev/null +++ b/regression/contracts/assigns_enforce_10/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +This test checks that verification fails when a function with an assigns clause calls another function with an assigns clause that is incompatible with the caller's assigns clause. diff --git a/regression/contracts/assigns_enforce_11/main.c b/regression/contracts/assigns_enforce_11/main.c new file mode 100644 index 00000000000..5cf4f989262 --- /dev/null +++ b/regression/contracts/assigns_enforce_11/main.c @@ -0,0 +1,22 @@ +#include + +void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1) +{ + f2(x1, y1, z1); +} + +void f2(int *x2, int *y2, int *z2) __CPROVER_assigns(*x2, *y2) +{ + *y2 = 5; + *z2 = 5; +} + +int main() +{ + int p = 1; + int q = 2; + int r = 3; + f1(&p, &q, &r); + + return 0; +} diff --git a/regression/contracts/assigns_enforce_11/test.desc b/regression/contracts/assigns_enforce_11/test.desc new file mode 100644 index 00000000000..9129b3828e5 --- /dev/null +++ b/regression/contracts/assigns_enforce_11/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +This test checks that verification fails when a function with an assigns clause calls another function with a compatible assigns clause, but the callee does not abide by the shared assigns clause. diff --git a/regression/contracts/assigns_enforce_12/main.c b/regression/contracts/assigns_enforce_12/main.c new file mode 100644 index 00000000000..1f3e9fb8622 --- /dev/null +++ b/regression/contracts/assigns_enforce_12/main.c @@ -0,0 +1,15 @@ +#include + +void f1(int *x) __CPROVER_assigns(*x) +{ + int *a = x; + *a = 5; +} + +int main() +{ + int n = 3; + f1(&n); + + return 0; +} diff --git a/regression/contracts/assigns_enforce_12/test.desc b/regression/contracts/assigns_enforce_12/test.desc new file mode 100644 index 00000000000..a24b653bc85 --- /dev/null +++ b/regression/contracts/assigns_enforce_12/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks that verification still succeeds if an expression in the assigns clause is written via an aliasing variable. diff --git a/regression/contracts/assigns_enforce_13/main.c b/regression/contracts/assigns_enforce_13/main.c new file mode 100644 index 00000000000..44acdcbe5f1 --- /dev/null +++ b/regression/contracts/assigns_enforce_13/main.c @@ -0,0 +1,16 @@ +#include + +void f1(int *x, int *y) __CPROVER_assigns(*y) +{ + int *a = x; + *a = 5; +} + +int main() +{ + int m = 3; + int n = 3; + f1(&n, &m); + + return 0; +} diff --git a/regression/contracts/assigns_enforce_13/test.desc b/regression/contracts/assigns_enforce_13/test.desc new file mode 100644 index 00000000000..32fb21ce7c1 --- /dev/null +++ b/regression/contracts/assigns_enforce_13/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +This test checks that verification fails if an expression outside of the assigns clause is written via an aliasing local variable. diff --git a/regression/contracts/assigns_enforce_malloc_01/main.c b/regression/contracts/assigns_enforce_malloc_01/main.c new file mode 100644 index 00000000000..60d061cb537 --- /dev/null +++ b/regression/contracts/assigns_enforce_malloc_01/main.c @@ -0,0 +1,16 @@ +#include + +int f1(int *a, int *b) __CPROVER_assigns(*a) +{ + b = (int *)malloc(sizeof(int)); + *b = 5; +} + +int main() +{ + int m = 4; + int n = 3; + f1(&m, &n); + + return 0; +} diff --git a/regression/contracts/assigns_enforce_malloc_01/test.desc b/regression/contracts/assigns_enforce_malloc_01/test.desc new file mode 100644 index 00000000000..72c6afae2e1 --- /dev/null +++ b/regression/contracts/assigns_enforce_malloc_01/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks that verification succeeds when a formal parameter pointer outside of the assigns clause is instead pointed as freshly allocated memory before being assigned. diff --git a/regression/contracts/assigns_enforce_malloc_02/main.c b/regression/contracts/assigns_enforce_malloc_02/main.c new file mode 100644 index 00000000000..eba0016c1e5 --- /dev/null +++ b/regression/contracts/assigns_enforce_malloc_02/main.c @@ -0,0 +1,19 @@ +#include + +int f1(int *a, int *b) __CPROVER_assigns(*a) +{ + while(*a > 0) + { + int *b = (int *)malloc(sizeof(int)); + *b = 5; + } +} + +int main() +{ + int m = 4; + int n = 3; + f1(&m, &n); + + return 0; +} diff --git a/regression/contracts/assigns_enforce_malloc_02/test.desc b/regression/contracts/assigns_enforce_malloc_02/test.desc new file mode 100644 index 00000000000..fdd13a65204 --- /dev/null +++ b/regression/contracts/assigns_enforce_malloc_02/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=6$ +^SIGNAL=0$ +malloc may be in a loop.$ +-- +-- +This test checks that an error is thrown when malloc is called within a loop. diff --git a/regression/contracts/assigns_enforce_scoping_01/main.c b/regression/contracts/assigns_enforce_scoping_01/main.c new file mode 100644 index 00000000000..900251d0af2 --- /dev/null +++ b/regression/contracts/assigns_enforce_scoping_01/main.c @@ -0,0 +1,20 @@ +#include + +int f1(int *a, int *b) __CPROVER_assigns(*a) +{ + if(*a > 0) + { + int *b = a; + *b = 5; + } + *b = 5; +} + +int main() +{ + int m = 4; + int n = 3; + f1(&m, &n); + + return 0; +} diff --git a/regression/contracts/assigns_enforce_scoping_01/test.desc b/regression/contracts/assigns_enforce_scoping_01/test.desc new file mode 100644 index 00000000000..ac134e83d35 --- /dev/null +++ b/regression/contracts/assigns_enforce_scoping_01/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=10$ +^SIGNAL=0$ +assertion: SUCCESS$ +assertion: FAILURE$ +^VERIFICATION FAILED$ +-- +-- +This test checks that variables which mask a formal parameter are logically distinct from the formal parameter itself. Specifically, we check that the masked variable may alias a parameter in the assigns clause, while the formal parameter does not, so verification fails, but not because of the masking variable. diff --git a/regression/contracts/assigns_enforce_scoping_02/main.c b/regression/contracts/assigns_enforce_scoping_02/main.c new file mode 100644 index 00000000000..11a80ee8c79 --- /dev/null +++ b/regression/contracts/assigns_enforce_scoping_02/main.c @@ -0,0 +1,20 @@ +#include + +int f1(int *a, int *b) __CPROVER_assigns(*a) +{ + if(*a > 0) + { + int *b = (int *)malloc(sizeof(int)); + *b = 5; + } + *b = 5; +} + +int main() +{ + int m = 4; + int n = 3; + f1(&m, &n); + + return 0; +} diff --git a/regression/contracts/assigns_enforce_scoping_02/test.desc b/regression/contracts/assigns_enforce_scoping_02/test.desc new file mode 100644 index 00000000000..d746bd0f0da --- /dev/null +++ b/regression/contracts/assigns_enforce_scoping_02/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=10$ +^SIGNAL=0$ +assertion: SUCCESS$ +assertion: FAILURE$ +^VERIFICATION FAILED$ +-- +-- +This test checks that variables which mask a formal parameter are logically distinct from the formal parameter itself. In this test, we check that the masked variable may point to freshly-allocated memory, while the masked parameter may not be assigned, so verification fails, but not because of the masking variable. diff --git a/regression/contracts/assigns_replace_01/main.c b/regression/contracts/assigns_replace_01/main.c new file mode 100644 index 00000000000..64337adf9bd --- /dev/null +++ b/regression/contracts/assigns_replace_01/main.c @@ -0,0 +1,15 @@ +#include + +void foo(int *x) __CPROVER_assigns(*x) +{ + *x = 7; +} + +int main() +{ + int n = 6; + foo(&n); + assert(n == 6); + + return 0; +} diff --git a/regression/contracts/assigns_replace_01/test.desc b/regression/contracts/assigns_replace_01/test.desc new file mode 100644 index 00000000000..05341195e1c --- /dev/null +++ b/regression/contracts/assigns_replace_01/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--replace-all-calls-with-contracts +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +This test checks that a variable inside the assigns clause is havocked. diff --git a/regression/contracts/assigns_replace_02/main.c b/regression/contracts/assigns_replace_02/main.c new file mode 100644 index 00000000000..8487c6564c9 --- /dev/null +++ b/regression/contracts/assigns_replace_02/main.c @@ -0,0 +1,16 @@ +#include + +void foo(int *x, int *y) __CPROVER_assigns(*x) +{ + *x = 7; +} + +int main() +{ + int n; + int m = 4; + bar(&n); + assert(m == 4); + + return 0; +} diff --git a/regression/contracts/assigns_replace_02/test.desc b/regression/contracts/assigns_replace_02/test.desc new file mode 100644 index 00000000000..8c1d2534916 --- /dev/null +++ b/regression/contracts/assigns_replace_02/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--replace-all-calls-with-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks that a variable outside the assigns clause is not havocked. diff --git a/regression/contracts/assigns_replace_03/main.c b/regression/contracts/assigns_replace_03/main.c new file mode 100644 index 00000000000..e96665bee44 --- /dev/null +++ b/regression/contracts/assigns_replace_03/main.c @@ -0,0 +1,17 @@ +#include + +int y; +double z; + +void bar(char **c) __CPROVER_assigns(y, z, **c) __CPROVER_ensures(**c == 6) +{ +} + +int main() +{ + char **b; + bar(b); + assert(**b == 6); + + return 0; +} diff --git a/regression/contracts/assigns_replace_03/test.desc b/regression/contracts/assigns_replace_03/test.desc new file mode 100644 index 00000000000..93cd2e13787 --- /dev/null +++ b/regression/contracts/assigns_replace_03/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--replace-all-calls-with-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks that a havocked variable can be constrained by a function post-condition. diff --git a/regression/contracts/assigns_replace_04/main.c b/regression/contracts/assigns_replace_04/main.c new file mode 100644 index 00000000000..6ec35cf8d29 --- /dev/null +++ b/regression/contracts/assigns_replace_04/main.c @@ -0,0 +1,33 @@ +#include + +void f2(int *x2, int *y2) __CPROVER_assigns(*x2) __CPROVER_ensures(*x2 > 5) +{ + *x2 = 10; +} + +void f3(int *x3, int *y3) __CPROVER_assigns(*x3) __CPROVER_ensures(*x3 > 100) +{ + *x3 = 101; +} + +int main() +{ + int p = 1; + int q = 2; + + for(int i = 0; i < 5; ++i) + { + if(p < 3) + { + f2(&p, &q); + } + else + { + f3(&p, &q); + } + } + assert(p > 100); + assert(q == 2); + + return 0; +} diff --git a/regression/contracts/assigns_replace_04/test.desc b/regression/contracts/assigns_replace_04/test.desc new file mode 100644 index 00000000000..01b0f878661 --- /dev/null +++ b/regression/contracts/assigns_replace_04/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--replace-all-calls-with-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks that verification succeeds when an assigns clause is combined with a function contract in a loop properly. diff --git a/regression/contracts/assigns_replace_05/main.c b/regression/contracts/assigns_replace_05/main.c new file mode 100644 index 00000000000..42d98843653 --- /dev/null +++ b/regression/contracts/assigns_replace_05/main.c @@ -0,0 +1,33 @@ +#include + +void f2(int *x2, int *y2) __CPROVER_assigns(*x2) __CPROVER_ensures(*x2 > 5) +{ + *x2 = 10; +} + +void f3(int *x3, int *y3) __CPROVER_ensures(*x3 > 100) +{ + *x3 = 101; +} + +int main() +{ + int p = 1; + int q = 2; + + for(int i = 0; i < 5; ++i) + { + if(i < 3) + { + f2(&p, &q); + } + else + { + f3(&p, &q); + } + } + assert(p > 100); + assert(q == 2); + + return 0; +} diff --git a/regression/contracts/assigns_replace_05/test.desc b/regression/contracts/assigns_replace_05/test.desc new file mode 100644 index 00000000000..9be0fb6b811 --- /dev/null +++ b/regression/contracts/assigns_replace_05/test.desc @@ -0,0 +1,11 @@ +KNOWNBUG +main.c +--replace-all-calls-with-contracts +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +This test checks that verification fails when assigns clauses are combined with function contracts in a loop improperly. + +BUG: Currently, function call replacement using 'ensures' specifications encodes an implicit assumption that any memory not mentioned in the ensures clause remains unchanged throughout the function, even when an 'assigns' clause is not present. diff --git a/regression/contracts/function_check_01/test.desc b/regression/contracts/function_check_01/test.desc index 7dafb10d751..1031d65d2e5 100644 --- a/regression/contracts/function_check_01/test.desc +++ b/regression/contracts/function_check_01/test.desc @@ -1,11 +1,9 @@ -KNOWNBUG +CORE main.c ---apply-code-contracts +--replace-all-calls-with-contracts ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- -- ---check-code-contracts not implemented yet. ---apply-code-contracts is the current name for the flag. This should be -updated as the flag changes. +--replace-all-calls-with-contracts is the current name for the flag. This should be updated as the flag changes. diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp index 4979fab69fc..0377fa97a1b 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -17,9 +17,9 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include "c_storage_spec.h" #include "expr2c.h" #include "type2name.h" -#include "c_storage_spec.h" std::string c_typecheck_baset::to_string(const exprt &expr) { @@ -645,6 +645,10 @@ void c_typecheck_baset::typecheck_declaration( irept contract; { + exprt spec_assigns= + static_cast(declaration.find(ID_C_spec_assigns)); + contract.add(ID_C_spec_assigns).swap(spec_assigns); + exprt spec_requires= static_cast(declaration.find(ID_C_spec_requires)); contract.add(ID_C_spec_requires).swap(spec_requires); @@ -725,6 +729,12 @@ void c_typecheck_baset::typecheck_declaration( irep_idt identifier=symbol.name; declarator.set_name(identifier); + // If the declarator is for a function definition, typecheck it. + if(can_cast_type(declarator.type())) + { + typecheck_assigns(to_code_type(declarator.type()), contract); + } + typecheck_symbol(symbol); // add code contract (if any); we typecheck this after the @@ -732,6 +742,8 @@ void c_typecheck_baset::typecheck_declaration( // available symbolt &new_symbol = symbol_table.get_writeable_ref(identifier); + typecheck_assigns_exprs( + static_cast(contract), ID_C_spec_assigns); typecheck_spec_expr(static_cast(contract), ID_C_spec_requires); typet ret_type = void_type(); @@ -743,12 +755,15 @@ void c_typecheck_baset::typecheck_declaration( typecheck_spec_expr(static_cast(contract), ID_C_spec_ensures); parameter_map.clear(); - if(contract.find(ID_C_spec_requires).is_not_nil()) - new_symbol.type.add(ID_C_spec_requires)= - contract.find(ID_C_spec_requires); - if(contract.find(ID_C_spec_ensures).is_not_nil()) - new_symbol.type.add(ID_C_spec_ensures)= - contract.find(ID_C_spec_ensures); + irept assigns_to_add = contract.find(ID_C_spec_assigns); + if(assigns_to_add.is_not_nil()) + new_symbol.type.add(ID_C_spec_assigns) = assigns_to_add; + irept requires_to_add = contract.find(ID_C_spec_requires); + if(requires_to_add.is_not_nil()) + new_symbol.type.add(ID_C_spec_requires) = requires_to_add; + irept ensures_to_add = contract.find(ID_C_spec_ensures); + if(ensures_to_add.is_not_nil()) + new_symbol.type.add(ID_C_spec_ensures) = ensures_to_add; } } } diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h index 01981f9d99c..650eac010da 100644 --- a/src/ansi-c/c_typecheck_base.h +++ b/src/ansi-c/c_typecheck_base.h @@ -144,6 +144,11 @@ class c_typecheck_baset: virtual void typecheck_dowhile(code_dowhilet &code); virtual void typecheck_start_thread(codet &code); virtual void typecheck_spec_expr(codet &code, const irep_idt &spec); + virtual void + typecheck_assigns(const code_typet &function_declarator, const irept &spec); + virtual void + typecheck_assigns(const ansi_c_declaratort &declarator, const exprt &assigns); + virtual void typecheck_assigns_exprs(codet &code, const irep_idt &spec); 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 041b9b3bf4f..513277e4b59 100644 --- a/src/ansi-c/c_typecheck_code.cpp +++ b/src/ansi-c/c_typecheck_code.cpp @@ -794,16 +794,75 @@ void c_typecheck_baset::typecheck_dowhile(code_dowhilet &code) typecheck_spec_expr(code, ID_C_spec_loop_invariant); } -void c_typecheck_baset::typecheck_spec_expr( +void c_typecheck_baset::typecheck_spec_expr(codet &code, const irep_idt &spec) +{ + if(code.find(spec).is_not_nil()) + { + exprt &constraint = static_cast(code.add(spec)); + + typecheck_expr(constraint); + implicit_typecast_bool(constraint); + } +} + +void c_typecheck_baset::typecheck_assigns( + const code_typet &function_declarator, + const irept &contract) +{ + exprt assigns = static_cast(contract.find(ID_C_spec_assigns)); + + // Make sure there is an assigns clause to check + if(assigns.is_not_nil()) + { + for(code_typet::parametert curr_param : function_declarator.parameters()) + { + if(curr_param.id() == ID_declaration) + { + ansi_c_declarationt ¶m_declaration = + to_ansi_c_declaration(curr_param); + + for(auto &decl : param_declaration.declarators()) + { + typecheck_assigns(decl, assigns); + } + } + } + } +} + +void c_typecheck_baset::typecheck_assigns( + const ansi_c_declaratort &declarator, + const exprt &assigns) +{ + for(exprt curr_op : assigns.operands()) + { + if(curr_op.id() != ID_symbol) + { + continue; + } + const symbol_exprt &symbol_op = to_symbol_expr(curr_op); + + if(symbol_op.get(ID_C_base_name) == declarator.get_base_name()) + { + error().source_location = declarator.source_location(); + error() << "Formal parameter " << declarator.get_name() << " without " + << "dereference appears in ASSIGNS clause. Assigning this " + << "parameter will never affect the state of the calling context." + << " Did you mean to write *" << declarator.get_name() << "?" + << eom; + throw 0; + } + } +} + +void c_typecheck_baset::typecheck_assigns_exprs( codet &code, const irep_idt &spec) { if(code.find(spec).is_not_nil()) { - exprt &constraint= - static_cast(code.add(spec)); + exprt &constraint = static_cast(code.add(spec)); typecheck_expr(constraint); - implicit_typecast_bool(constraint); } } diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 6a455ccdd38..2618c1fd928 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -470,10 +470,15 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr) { // already type checked } + else if(expr.id() == ID_C_spec_assigns || expr.id() == ID_target_list) + { + // already type checked + } else { error().source_location = expr.source_location(); - error() << "unexpected expression: " << expr.pretty() << eom; + error() << "expression categorized improperly during parsing: " + << expr.pretty() << eom; throw 0; } } diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y index b4455369e0c..8bd13ee94f3 100644 --- a/src/ansi-c/parser.y +++ b/src/ansi-c/parser.y @@ -204,6 +204,7 @@ extern char *yyansi_ctext; %token TOK_CPROVER_LOOP_INVARIANT "__CPROVER_loop_invariant" %token TOK_CPROVER_REQUIRES "__CPROVER_requires" %token TOK_CPROVER_ENSURES "__CPROVER_ensures" +%token TOK_CPROVER_ASSIGNS "__CPROVER_assigns" %token TOK_IMPLIES "==>" %token TOK_EQUIVALENT "<==>" %token TOK_XORXOR "^^" @@ -510,6 +511,36 @@ ensures_opt: { $$=$3; } ; +assigns_opt: + /* nothing */ + { init($$); parser_stack($$).make_nil(); } + | TOK_CPROVER_ASSIGNS '(' target_list ')' + { $$=$3; } + ; + +target_list: + target + { + init($$, ID_target_list); + mto($$, $1); + } + | target_list ',' target + { + $$=$1; + mto($$, $3); + } + ; + +target: + identifier + | '*' target + { + $$=$1; + set($$, ID_dereference); + mto($$, $2); + } + ; + statement_expression: '(' compound_statement ')' { $$=$1; @@ -2853,14 +2884,21 @@ asm_definition: function_definition: function_head + assigns_opt requires_opt ensures_opt function_body { + + // Capture assigns clause if(parser_stack($2).is_not_nil()) - parser_stack($1).add(ID_C_spec_requires).swap(parser_stack($2)); + parser_stack($1).add(ID_C_spec_assigns).swap(parser_stack($2)); + + // Capture code contract if(parser_stack($3).is_not_nil()) - parser_stack($1).add(ID_C_spec_ensures).swap(parser_stack($3)); + parser_stack($1).add(ID_C_spec_requires).swap(parser_stack($3)); + if(parser_stack($4).is_not_nil()) + parser_stack($1).add(ID_C_spec_ensures).swap(parser_stack($4)); // The head is a declaration with one declarator, // and the body becomes the 'value'. $$=$1; @@ -2868,7 +2906,7 @@ function_definition: to_ansi_c_declaration(parser_stack($$)); assert(ansi_c_declaration.declarators().size()==1); - ansi_c_declaration.add_initializer(parser_stack($4)); + ansi_c_declaration.add_initializer(parser_stack($5)); // Kill the scope that 'function_head' creates. PARSER.pop_scope(); diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l index d3eeceaf08c..2b45492e515 100644 --- a/src/ansi-c/scanner.l +++ b/src/ansi-c/scanner.l @@ -1277,6 +1277,7 @@ __decltype { if(PARSER.cpp98 && {CPROVER_PREFIX}"loop_invariant" { loc(); return TOK_CPROVER_LOOP_INVARIANT; } {CPROVER_PREFIX}"requires" { loc(); return TOK_CPROVER_REQUIRES; } {CPROVER_PREFIX}"ensures" { loc(); return TOK_CPROVER_ENSURES; } +{CPROVER_PREFIX}"assigns" { loc(); return TOK_CPROVER_ASSIGNS; } "\xe2\x88\x80" | "\\forall" { /* Non-standard, obviously. Found in ACSL syntax. */ diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index e0115fb34fa..545c2271a1f 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -12,20 +12,25 @@ Date: February 2016 /// Verify and use annotated invariants and pre/post-conditions #include "code_contracts.h" +#include "loop_utils.h" -#include -#include -#include - -#include +#include +#include +#include +#include #include +#include + #include +#include +#include +#include #include - -#include "loop_utils.h" +#include +#include /// Predicate to be used with the exprt::visit() function. The function /// found_return_value() will return `true` iff this predicate is called on an @@ -62,18 +67,15 @@ static void check_apply_invariants( const goto_programt::targett loop_head, const loopt &loop) { - assert(!loop.empty()); + PRECONDITION(!loop.empty()); // find the last back edge - goto_programt::targett loop_end=loop_head; - for(loopt::const_iterator - it=loop.begin(); - it!=loop.end(); - ++it) - if((*it)->is_goto() && - (*it)->get_target()==loop_head && - (*it)->location_number>loop_end->location_number) - loop_end=*it; + goto_programt::targett loop_end = loop_head; + for(loopt::const_iterator it = loop.begin(); it != loop.end(); ++it) + if( + (*it)->is_goto() && (*it)->get_target() == loop_head && + (*it)->location_number > loop_end->location_number) + loop_end = *it; // see whether we have an invariant exprt invariant = static_cast( @@ -136,7 +138,7 @@ static void check_apply_invariants( // change the back edge into assume(false) or assume(guard) loop_end->targets.clear(); - loop_end->type=ASSUME; + loop_end->type = ASSUME; if(loop_head->is_goto()) loop_end->set_condition(false_exprt()); else @@ -145,11 +147,12 @@ static void check_apply_invariants( bool code_contractst::has_contract(const irep_idt fun_name) { - const symbolt &f_sym = ns.lookup(fun_name); - const code_typet &type = to_code_type(f_sym.type); - const exprt ensures = - static_cast(type.find(ID_C_spec_ensures)); - return ensures.is_not_nil(); + const symbolt &function_symbol = ns.lookup(fun_name); + const code_typet &type = to_code_type(function_symbol.type); + const irept assigns = type.find(ID_C_spec_assigns); + const irept ensures = type.find(ID_C_spec_ensures); + + return ensures.is_not_nil() || assigns.is_not_nil(); } bool code_contractst::apply_contract( @@ -158,39 +161,47 @@ bool code_contractst::apply_contract( { const code_function_callt &call = target->get_function_call(); - // we don't handle function pointers - if(call.function().id()!=ID_symbol) + // 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; - const irep_idt &function= - to_symbol_expr(call.function()).get_identifier(); - const symbolt &f_sym=ns.lookup(function); - const code_typet &type=to_code_type(f_sym.type); + // Retrieve the function type, which is needed to extract the contract + // components. + const irep_idt &function = to_symbol_expr(call.function()).get_identifier(); + const symbolt &function_symbol = ns.lookup(function); + const code_typet &type = to_code_type(function_symbol.type); - exprt requires= - static_cast(type.find(ID_C_spec_requires)); - exprt ensures= - static_cast(type.find(ID_C_spec_ensures)); + // Isolate each component of the contract. + exprt assigns = static_cast(type.find(ID_C_spec_assigns)); + exprt requires = static_cast(type.find(ID_C_spec_requires)); + exprt ensures = static_cast(type.find(ID_C_spec_ensures)); - // is there a contract? - if(ensures.is_nil()) + // Check to see if the function contract actually constrains its effect on + // the program state; if not, return. + if(ensures.is_nil() && assigns.is_nil()) return false; + // Create a replace_symbolt object, for replacing expressions in the callee + // with expressions from the call site (e.g. the return value). replace_symbolt replace; - // Replace return value if(type.return_type() != empty_typet()) { + // Check whether the function's return value is not disregarded. if(call.lhs().is_not_nil()) { - // foo() ensures that its return value is > 5. Then rewrite calls to foo: + // If so, have it replaced appropriately. + // For example, if foo() ensures that its return value is > 5, then + // rewrite calls to foo as follows: // x = foo() -> assume(__CPROVER_return_value > 5) -> assume(x > 5) symbol_exprt ret_val(CPROVER_PREFIX "return_value", call.lhs().type()); replace.insert(ret_val, call.lhs()); } else { - // Function does have a return value, but call is not being assigned to - // anything so we can't use the trick above. + // If the function does return a value, but the return value is + // disregarded, check if the postcondition includes the return value. return_value_visitort v; ensures.visit(v); if(v.found_return_value()) @@ -212,22 +223,25 @@ bool code_contractst::apply_contract( } // Replace formal parameters - code_function_callt::argumentst::const_iterator a_it= + code_function_callt::argumentst::const_iterator a_it = call.arguments().begin(); - for(code_typet::parameterst::const_iterator - p_it=type.parameters().begin(); - p_it!=type.parameters().end() && - a_it!=call.arguments().end(); + for(code_typet::parameterst::const_iterator p_it = type.parameters().begin(); + p_it != type.parameters().end() && a_it != call.arguments().end(); ++p_it, ++a_it) + { if(!p_it->get_identifier().empty()) { symbol_exprt p(p_it->get_identifier(), p_it->type()); replace.insert(p, *a_it); } + } + // Replace expressions in the contract components. + replace(assigns); replace(requires); replace(ensures); + // Insert assertion of the precondition immediately before the call site. if(requires.is_not_nil()) { goto_programt::instructiont a = @@ -237,9 +251,51 @@ bool code_contractst::apply_contract( ++target; } - // overwrite the function call - *target = goto_programt::make_assumption(ensures, target->source_location); + // Create a series of non-deterministic assignments to havoc the variables + // 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) + { + assigns_tgts.insert(curr_op); + } + else if(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); + + // Insert the non-deterministic assignment immediately before the call site. + goto_program.insert_before_swap(target, assigns_havoc); + std::advance(target, assigns_tgts.size()); + } + + // To remove the function call, replace it with an assumption statement + // assuming the postcondition, if there is one. Otherwise, replace the + // function call with a SKIP statement. + if(ensures.is_not_nil()) + { + *target = goto_programt::make_assumption(ensures, target->source_location); + } + else + { + *target = goto_programt::make_skip(); + } + // Add this function to the set of replaced functions. summarized.insert(function); return false; } @@ -251,15 +307,12 @@ void code_contractst::code_contracts( natural_loops_mutablet natural_loops(goto_function.body); // iterate over the (natural) loops in the function - for(natural_loops_mutablet::loop_mapt::const_iterator - l_it=natural_loops.loop_map.begin(); - l_it!=natural_loops.loop_map.end(); + for(natural_loops_mutablet::loop_mapt::const_iterator l_it = + natural_loops.loop_map.begin(); + l_it != natural_loops.loop_map.end(); l_it++) check_apply_invariants( - goto_function, - local_may_alias, - l_it->first, - l_it->second); + goto_function, local_may_alias, l_it->first, l_it->second); // look at all function calls Forall_goto_program_instructions(ins, goto_function.body) @@ -282,24 +335,388 @@ const symbolt &code_contractst::new_tmp_symbol( symbol_table); } +exprt create_alias_expression( + const exprt &assigns, + const exprt &lhs, + std::vector &aliasable_references) +{ + bool first_iter = true; + exprt running = false_exprt(); + for(auto aliasable : aliasable_references) + { + exprt leftPtr = address_of_exprt{lhs}; + exprt rightPtr = aliasable; + exprt same = same_object(leftPtr, rightPtr); + + 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 code_typet &type = to_code_type(function_symbol.type); + exprt assigns = static_cast(type.find(ID_C_spec_assigns)); + + exprt::operandst &targets = assigns.operands(); + for(exprt curr_op : targets) + { + exprt op_addr = address_of_exprt{curr_op}; + + // 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(op_addr)), function_symbol.location)); + + // Add a map entry from the original operand to the new symbol + created_references.push_back(standin); + } +} + +void code_contractst::instrument_assn_statement( + goto_programt::instructionst::iterator &instruction_iterator, + goto_programt &program, + exprt &assigns, + std::vector &assigns_references, + std::set &freely_assignable_exprs) +{ + INVARIANT( + instruction_iterator->is_assign(), + "The first argument of instrument_assn_statement should always be" + " an assignment"); + const exprt &lhs = instruction_iterator->get_assign().lhs(); + if(freely_assignable_exprs.find(lhs) != freely_assignable_exprs.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)); + program.insert_before_swap(instruction_iterator, alias_assertion); + ++instruction_iterator; +} + +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) +{ + 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; + local_instruction_iterator++; + if( + local_instruction_iterator->is_assign() && + local_instruction_iterator->get_assign().lhs().is_not_nil()) + { + freely_assignable_exprs.insert( + local_instruction_iterator->get_assign().lhs()); + } + return; // assume malloc edits no currently-existing memory objects. + } + + if(call.lhs().is_not_nil()) + { + exprt alias_expr = + create_alias_expression(assigns, call.lhs(), 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; + } + + // 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; + } + + exprt called_assigns = static_cast( + called_func->second.type.find(ID_C_spec_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; + + return; + } + else // Called function has assigns clause + { + replace_symbolt replace; + // Replace formal parameters + code_function_callt::argumentst::const_iterator a_it = + call.arguments().begin(); + for(code_typet::parameterst::const_iterator p_it = + called_type.parameters().begin(); + p_it != called_type.parameters().end() && + a_it != call.arguments().end(); + ++p_it, ++a_it) + { + if(!p_it->get_identifier().empty()) + { + symbol_exprt p(p_it->get_identifier(), p_it->type()); + replace.insert(p, *a_it); + } + } + + 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; + } + } + } +} + +bool code_contractst::check_for_looped_mallocs(const goto_programt &program) +{ + // Collect all GOTOs and mallocs + std::vector back_gotos; + std::vector malloc_calls; + + int idx = 0; + for(goto_programt::instructiont instruction : program.instructions) + { + if(instruction.is_backwards_goto()) + { + back_gotos.push_back(instruction); + } + if(instruction.is_function_call()) + { + code_function_callt call = instruction.get_function_call(); + const irep_idt &called_name = + to_symbol_expr(call.function()).get_identifier(); + + if(std::strcmp(called_name.c_str(), "malloc") == 0) + { + malloc_calls.push_back(instruction); + } + } + idx++; + } + // 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) + { + for(auto malloc_entry : malloc_calls) + { + if( + 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 + << " and it's destination at location " + << target->location_number << ". " + << "Unable to complete instrumentation, as this malloc " + << "may be in a loop." << messaget::eom; + throw 0; + } + } + } + } + return false; +} + +bool code_contractst::add_pointer_checks(const std::string &function_name) +{ + // Get the function object before instrumentation. + auto old_function = goto_functions.function_map.find(function_name); + if(old_function == goto_functions.function_map.end()) + { + log.error() << "Could not find function '" << function_name + << "' in goto-program; not enforcing contracts." + << messaget::eom; + return true; + } + goto_programt &program = old_function->second.body; + if(program.instructions.empty()) // empty function body + { + return false; + } + + const irep_idt function_id(function_name); + const symbolt &function_symbol = ns.lookup(function_id); + const code_typet &type = to_code_type(function_symbol.type); + + exprt assigns = static_cast(type.find(ID_C_spec_assigns)); + + // Return if there are no reference checks to perform. + if(assigns.is_nil()) + return false; + + goto_programt::instructionst::iterator instruction_iterator = + 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 a list of variables that are okay to assign. + std::set freely_assignable_exprs; + for(code_typet::parametert param : type.parameters()) + { + freely_assignable_exprs.insert(param); + } + + int lines_to_iterate = standin_decls.instructions.size(); + program.insert_before_swap(instruction_iterator, standin_decls); + std::advance(instruction_iterator, lines_to_iterate); + + if(check_for_looped_mallocs(program)) + { + return true; + } + + // Insert aliasing assertions + for(; instruction_iterator != program.instructions.end(); + std::advance(instruction_iterator, 1)) + { + if(instruction_iterator->is_decl()) + { + freely_assignable_exprs.insert(instruction_iterator->get_decl().symbol()); + } + else if(instruction_iterator->is_assign()) + { + instrument_assn_statement( + instruction_iterator, + program, + assigns, + original_references, + freely_assignable_exprs); + } + else if(instruction_iterator->is_function_call()) + { + instrument_call_statement( + instruction_iterator, + program, + assigns, + original_references, + freely_assignable_exprs); + } + } + return false; +} + bool code_contractst::enforce_contract(const std::string &fun_to_enforce) { - // Rename old function + // Add statements to the source function to ensure assigns clause is + // respected. + add_pointer_checks(fun_to_enforce); + + // Rename source function std::stringstream ss; ss << CPROVER_PREFIX << "contracts_original_" << fun_to_enforce; const irep_idt mangled(ss.str()); const irep_idt original(fun_to_enforce); - auto old_fun = goto_functions.function_map.find(original); - if(old_fun == goto_functions.function_map.end()) + auto old_function = goto_functions.function_map.find(original); + if(old_function == goto_functions.function_map.end()) { log.error() << "Could not find function '" << fun_to_enforce << "' in goto-program; not enforcing contracts." << messaget::eom; return true; } - std::swap(goto_functions.function_map[mangled], old_fun->second); - goto_functions.function_map.erase(old_fun); + + std::swap(goto_functions.function_map[mangled], old_function->second); + goto_functions.function_map.erase(old_function); // Place a new symbol with the mangled name into the symbol table source_locationt sl; @@ -318,9 +735,9 @@ bool code_contractst::enforce_contract(const std::string &fun_to_enforce) " in the symbol table because that name is a mangled name"); // Insert wrapper function into goto_functions - auto nexist_old_fun = goto_functions.function_map.find(original); + auto nexist_old_function = goto_functions.function_map.find(original); INVARIANT( - nexist_old_fun == goto_functions.function_map.end(), + nexist_old_function == goto_functions.function_map.end(), "There should be no function called " + fun_to_enforce + " in the function map because that function should have had its" " name mangled"); @@ -346,19 +763,24 @@ void code_contractst::add_contract_check( const irep_idt &mangled_fun, goto_programt &dest) { - assert(!dest.instructions.empty()); + PRECONDITION(!dest.instructions.empty()); goto_functionst::function_mapt::iterator f_it = goto_functions.function_map.find(mangled_fun); - assert(f_it!=goto_functions.function_map.end()); + PRECONDITION(f_it != goto_functions.function_map.end()); - const goto_functionst::goto_functiont &gf=f_it->second; + const goto_functionst::goto_functiont &gf = f_it->second; - const exprt &requires= - static_cast(gf.type.find(ID_C_spec_requires)); - const exprt &ensures= - static_cast(gf.type.find(ID_C_spec_ensures)); - assert(ensures.is_not_nil()); + const exprt &assigns = + static_cast(gf.type.find(ID_C_spec_assigns)); + const exprt &requires = + static_cast(gf.type.find(ID_C_spec_requires)); + const exprt &ensures = + static_cast(gf.type.find(ID_C_spec_ensures)); + INVARIANT( + ensures.is_not_nil() || assigns.is_not_nil(), + "Code conract enforcement is trivial without an ensures or assigns " + "clause."); // build: // if(nondet) @@ -367,7 +789,6 @@ void code_contractst::add_contract_check( // assume(requires) [optional] // ret=function(parameter1, ...) // assert(ensures) - // assume(false) // skip: ... // build skip so that if(nondet) can refer to it @@ -389,7 +810,7 @@ void code_contractst::add_contract_check( replace_symbolt replace; // decl ret - if(gf.type.return_type()!=empty_typet()) + if(gf.type.return_type() != empty_typet()) { symbol_exprt r = new_tmp_symbol( gf.type.return_type(), @@ -399,7 +820,7 @@ void code_contractst::add_contract_check( .symbol_expr(); check.add(goto_programt::make_decl(r, skip->source_location)); - call.lhs()=r; + call.lhs() = r; symbol_exprt ret_val(CPROVER_PREFIX "return_value", call.lhs().type()); replace.insert(ret_val, r); @@ -443,12 +864,11 @@ void code_contractst::add_contract_check( replace(ensures_cond); // assert(ensures) - check.add( - goto_programt::make_assertion(ensures_cond, ensures.source_location())); - - // assume(false) - check.add( - goto_programt::make_assumption(false_exprt(), ensures.source_location())); + if(ensures.is_not_nil()) + { + check.add( + goto_programt::make_assertion(ensures_cond, ensures.source_location())); + } // prepend the new code to dest check.destructive_append(tmp_skip); diff --git a/src/goto-instrument/code_contracts.h b/src/goto-instrument/code_contracts.h index 9aa3554a0e2..955294beb55 100644 --- a/src/goto-instrument/code_contracts.h +++ b/src/goto-instrument/code_contracts.h @@ -92,6 +92,47 @@ class code_contractst /// \brief Enforce contract of a single function bool enforce_contract(const std::string &); + /// Insert assertion statements into the goto program to ensure that + /// assigned memory is within the assignable memory frame. + bool add_pointer_checks(const std::string &); + + /// Check if there are any malloc statements which may be repeated because of + /// 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_assn_statement( + goto_programt::instructionst::iterator &ins_it, + goto_programt &program, + exprt &assigns, + std::vector &original_references, + std::set &freely_assignable_exprs); + + /// 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 + /// aliased by some expression in assigns_references,unless it is contained + /// in freely_assignable_exprs. + void instrument_call_statement( + goto_programt::instructionst::iterator &ins_it, + goto_programt &program, + exprt &assigns, + std::vector &assigns_references, + std::set &freely_assignable_exprs); + + /// 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, + /// 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, + std::vector &created_references); + void code_contracts(goto_functionst::goto_functiont &goto_function); /// \brief Does the named function have a contract? diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 917e1e79af6..f6943c80aa7 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -573,6 +573,8 @@ IREP_ID_ONE(is_used) IREP_ID_TWO(C_spec_loop_invariant, #spec_loop_invariant) IREP_ID_TWO(C_spec_requires, #spec_requires) IREP_ID_TWO(C_spec_ensures, #spec_ensures) +IREP_ID_TWO(C_spec_assigns, #spec_assigns) +IREP_ID_ONE(target_list) IREP_ID_ONE(virtual_function) IREP_ID_TWO(element_type, element_type) IREP_ID_ONE(working_directory) From 67891bbf679fcec925c1d17a7c69beea615de1ad Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Fri, 25 Sep 2020 10:21:59 -0400 Subject: [PATCH 2/5] Extends ansi_c_declarationt to include accessors for assigns clauses --- src/ansi-c/ansi_c_declaration.h | 15 +++++++++++++++ src/ansi-c/c_typecheck_base.cpp | 13 +++++-------- 2 files changed, 20 insertions(+), 8 deletions(-) diff --git a/src/ansi-c/ansi_c_declaration.h b/src/ansi-c/ansi_c_declaration.h index e98b3ef27f2..d1b2d3c2ce1 100644 --- a/src/ansi-c/ansi_c_declaration.h +++ b/src/ansi-c/ansi_c_declaration.h @@ -244,6 +244,21 @@ class ansi_c_declarationt:public exprt assert(!declarators().empty()); declarators().back().value().swap(value); } + + const exprt &spec_assigns() const + { + return static_cast(find(ID_C_spec_assigns)); + } + + const exprt &spec_requires() const + { + return static_cast(find(ID_C_spec_requires)); + } + + const exprt &spec_ensures() const + { + return static_cast(find(ID_C_spec_ensures)); + } }; inline ansi_c_declarationt &to_ansi_c_declaration(exprt &expr) diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp index 0377fa97a1b..5c0d114b1ed 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -645,17 +645,14 @@ void c_typecheck_baset::typecheck_declaration( irept contract; { - exprt spec_assigns= - static_cast(declaration.find(ID_C_spec_assigns)); + exprt spec_assigns = declaration.spec_assigns(); contract.add(ID_C_spec_assigns).swap(spec_assigns); - exprt spec_requires= - static_cast(declaration.find(ID_C_spec_requires)); - contract.add(ID_C_spec_requires).swap(spec_requires); - - exprt spec_ensures= - static_cast(declaration.find(ID_C_spec_ensures)); + exprt spec_ensures = declaration.spec_ensures(); contract.add(ID_C_spec_ensures).swap(spec_ensures); + + exprt spec_requires = declaration.spec_requires(); + contract.add(ID_C_spec_requires).swap(spec_requires); } // Now do declarators, if any. From cf8e8cbe4660286c112889ba28c7627e1e179f37 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Wed, 14 Oct 2020 23:46:29 -0400 Subject: [PATCH 3/5] Improves documentation for assigns clause support Signed-off-by: Felipe R. Monteiro --- doc/cprover-manual/assigns-clause.md | 82 ++++++++++++++++++++-------- 1 file changed, 60 insertions(+), 22 deletions(-) diff --git a/doc/cprover-manual/assigns-clause.md b/doc/cprover-manual/assigns-clause.md index f40fcbe6500..c949125de00 100644 --- a/doc/cprover-manual/assigns-clause.md +++ b/doc/cprover-manual/assigns-clause.md @@ -1,15 +1,24 @@ ## CBMC Assigns Clause + ### Introduction -Here is described the syntax and semantics of the "assigns" clause as implemented in CBMC. This construct 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 captured by the assigns clause must not be written within the given scope, even if the value(s) therein are not modified. +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 +captured by the assigns clause must not be written within the given scope, even +if the value(s) therein are not modified. + ### Scalar Variables -The initial iteration of this design focuses on specifying an assigns clause for simple variable types and their pointers. Arrays, structured data, and pointers are left to future contributions. +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 -A special construct is introduced to specify assigns clauses. Its syntax is defined as follows. +A special construct is introduced to specify assigns clauses. Its syntax is +defined as follows. ``` := __CPROVER_assigns ( ) @@ -24,28 +33,57 @@ A special construct is introduced to specify assigns clauses. Its syntax is defi ``` -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. +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. + ##### 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 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. +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. + +Let the ith expression in some assigns clause *c* be denoted +*exprs**c*[i], the jth formal parameter of some function +*f* be denoted *params**f*[j], and the kth argument passed +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). -Let the ith expression in some assigns clause *c* be denoted *exprs**c*[i], the jth formal parameter of some function *f* be denoted *params**f*[j], and the kth argument passed 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. - -###### 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 is a predicate indicating that the two pointers reference the same object in the CBMC memory model. Additionally, for each function call without an assigns clause, 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. - +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. From 9678a3d0a159e0cfab87e1b361c058fac3199a40 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Thu, 15 Oct 2020 00:29:29 -0400 Subject: [PATCH 4/5] Cleans-up all regression tests for assigns clauses Signed-off-by: Felipe R. Monteiro --- .../contracts/assigns_enforce_01/main.c | 9 +-------- .../contracts/assigns_enforce_02/main.c | 2 -- .../contracts/assigns_enforce_03/main.c | 2 -- .../contracts/assigns_enforce_04/main.c | 2 -- .../contracts/assigns_enforce_05/main.c | 2 -- .../contracts/assigns_enforce_06/main.c | 2 -- .../contracts/assigns_enforce_07/main.c | 2 -- .../contracts/assigns_enforce_08/main.c | 2 -- .../contracts/assigns_enforce_08/test.desc | 4 +++- .../contracts/assigns_enforce_09/main.c | 2 -- .../contracts/assigns_enforce_10/main.c | 2 -- .../contracts/assigns_enforce_11/main.c | 2 -- .../contracts/assigns_enforce_12/main.c | 2 -- .../contracts/assigns_enforce_13/main.c | 2 -- .../contracts/assigns_enforce_14/main.c | 19 +++++++++++++++++++ .../contracts/assigns_enforce_14/test.desc | 13 +++++++++++++ .../assigns_enforce_malloc_01/main.c | 2 +- .../assigns_enforce_malloc_02/main.c | 2 +- .../assigns_enforce_malloc_02/test.desc | 2 ++ .../assigns_enforce_scoping_01/main.c | 2 -- .../assigns_enforce_scoping_02/main.c | 2 +- .../contracts/assigns_replace_01/main.c | 2 +- .../contracts/assigns_replace_01/test.desc | 2 ++ .../contracts/assigns_replace_05/test.desc | 3 ++- .../contracts/function_check_01/test.desc | 2 +- 25 files changed, 47 insertions(+), 41 deletions(-) create mode 100644 regression/contracts/assigns_enforce_14/main.c create mode 100644 regression/contracts/assigns_enforce_14/test.desc diff --git a/regression/contracts/assigns_enforce_01/main.c b/regression/contracts/assigns_enforce_01/main.c index 786f9990813..102a3870a72 100644 --- a/regression/contracts/assigns_enforce_01/main.c +++ b/regression/contracts/assigns_enforce_01/main.c @@ -1,11 +1,4 @@ -#include - -int z; - -// z is not assigned, but it *may* be assigned. -// The assigns clause does not need to exactly match the -// set of variables which are assigned in the function. -int foo(int *x) __CPROVER_assigns(z, *x) +int foo(int *x) __CPROVER_assigns(*x) __CPROVER_ensures(__CPROVER_return_value == *x + 5) { *x = *x + 0; diff --git a/regression/contracts/assigns_enforce_02/main.c b/regression/contracts/assigns_enforce_02/main.c index 6062fa60282..e581b827ee6 100644 --- a/regression/contracts/assigns_enforce_02/main.c +++ b/regression/contracts/assigns_enforce_02/main.c @@ -1,5 +1,3 @@ -#include - int z; int foo(int *x) __CPROVER_assigns(z) diff --git a/regression/contracts/assigns_enforce_03/main.c b/regression/contracts/assigns_enforce_03/main.c index 293f69d2d89..5886f49e080 100644 --- a/regression/contracts/assigns_enforce_03/main.c +++ b/regression/contracts/assigns_enforce_03/main.c @@ -1,5 +1,3 @@ -#include - void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1) { f2(x1, y1, z1); diff --git a/regression/contracts/assigns_enforce_04/main.c b/regression/contracts/assigns_enforce_04/main.c index 4964f30cd8e..0d0e4e4da39 100644 --- a/regression/contracts/assigns_enforce_04/main.c +++ b/regression/contracts/assigns_enforce_04/main.c @@ -1,5 +1,3 @@ -#include - void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1) { f2(x1, y1, z1); diff --git a/regression/contracts/assigns_enforce_05/main.c b/regression/contracts/assigns_enforce_05/main.c index 73830619f9b..fb891d002db 100644 --- a/regression/contracts/assigns_enforce_05/main.c +++ b/regression/contracts/assigns_enforce_05/main.c @@ -1,5 +1,3 @@ -#include - void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1) { f2(x1, y1, z1); diff --git a/regression/contracts/assigns_enforce_06/main.c b/regression/contracts/assigns_enforce_06/main.c index a330fefee8d..e4d12d140f6 100644 --- a/regression/contracts/assigns_enforce_06/main.c +++ b/regression/contracts/assigns_enforce_06/main.c @@ -1,5 +1,3 @@ -#include - void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1) { f2(x1, y1, z1); diff --git a/regression/contracts/assigns_enforce_07/main.c b/regression/contracts/assigns_enforce_07/main.c index 50fe90deea3..384807e6218 100644 --- a/regression/contracts/assigns_enforce_07/main.c +++ b/regression/contracts/assigns_enforce_07/main.c @@ -1,5 +1,3 @@ -#include - void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1, *z1) { f2(x1, y1, z1); diff --git a/regression/contracts/assigns_enforce_08/main.c b/regression/contracts/assigns_enforce_08/main.c index 286dd50650f..8f562a91cee 100644 --- a/regression/contracts/assigns_enforce_08/main.c +++ b/regression/contracts/assigns_enforce_08/main.c @@ -1,5 +1,3 @@ -#include - void f1(int *x) __CPROVER_assigns(*x) { int *a = x; diff --git a/regression/contracts/assigns_enforce_08/test.desc b/regression/contracts/assigns_enforce_08/test.desc index 9799f7ee5aa..f2b63278a84 100644 --- a/regression/contracts/assigns_enforce_08/test.desc +++ b/regression/contracts/assigns_enforce_08/test.desc @@ -6,4 +6,6 @@ main.c ^VERIFICATION SUCCESSFUL$ -- -- -This test checks that verification succeeds when a function with an assigns clause calls another with an additional level of indirection, and that functions respects the assigns clause of the caller. +This test checks that verification succeeds when a function with an assigns +clause calls another with an additional level of indirection, and that +functions respects the assigns clause of the caller. diff --git a/regression/contracts/assigns_enforce_09/main.c b/regression/contracts/assigns_enforce_09/main.c index a1135d31341..f0ddf187eca 100644 --- a/regression/contracts/assigns_enforce_09/main.c +++ b/regression/contracts/assigns_enforce_09/main.c @@ -1,5 +1,3 @@ -#include - void f1(int **x) __CPROVER_assigns(*x) { f2(x); diff --git a/regression/contracts/assigns_enforce_10/main.c b/regression/contracts/assigns_enforce_10/main.c index 4398c4f9ac2..232d68a4ea7 100644 --- a/regression/contracts/assigns_enforce_10/main.c +++ b/regression/contracts/assigns_enforce_10/main.c @@ -1,5 +1,3 @@ -#include - void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1) { f2(x1, y1, z1); diff --git a/regression/contracts/assigns_enforce_11/main.c b/regression/contracts/assigns_enforce_11/main.c index 5cf4f989262..ac7a36c56d0 100644 --- a/regression/contracts/assigns_enforce_11/main.c +++ b/regression/contracts/assigns_enforce_11/main.c @@ -1,5 +1,3 @@ -#include - void f1(int *x1, int *y1, int *z1) __CPROVER_assigns(*x1, *y1) { f2(x1, y1, z1); diff --git a/regression/contracts/assigns_enforce_12/main.c b/regression/contracts/assigns_enforce_12/main.c index 1f3e9fb8622..0af9f968420 100644 --- a/regression/contracts/assigns_enforce_12/main.c +++ b/regression/contracts/assigns_enforce_12/main.c @@ -1,5 +1,3 @@ -#include - void f1(int *x) __CPROVER_assigns(*x) { int *a = x; diff --git a/regression/contracts/assigns_enforce_13/main.c b/regression/contracts/assigns_enforce_13/main.c index 44acdcbe5f1..65e7795a3b7 100644 --- a/regression/contracts/assigns_enforce_13/main.c +++ b/regression/contracts/assigns_enforce_13/main.c @@ -1,5 +1,3 @@ -#include - void f1(int *x, int *y) __CPROVER_assigns(*y) { int *a = x; diff --git a/regression/contracts/assigns_enforce_14/main.c b/regression/contracts/assigns_enforce_14/main.c new file mode 100644 index 00000000000..9d205896302 --- /dev/null +++ b/regression/contracts/assigns_enforce_14/main.c @@ -0,0 +1,19 @@ +int z; + +// z is not assigned, but it *may* be assigned. +// The assigns clause does not need to exactly match the +// set of variables which are assigned in the function. +int foo(int *x) __CPROVER_assigns(z, *x) + __CPROVER_ensures(__CPROVER_return_value == *x + 5) +{ + *x = *x + 0; + return *x + 5; +} + +int main() +{ + int n = 4; + n = foo(&n); + + return 0; +} diff --git a/regression/contracts/assigns_enforce_14/test.desc b/regression/contracts/assigns_enforce_14/test.desc new file mode 100644 index 00000000000..7c24b33faf7 --- /dev/null +++ b/regression/contracts/assigns_enforce_14/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +This test checks that verification succeeds if only expressions inside the assigns clause are assigned within the function. + +Note: For all 'enforce' tests, nothing can be assumed about the return value of the function (as the function call is not replaced at this point). + +To make such assumptions would cause verification to fail. diff --git a/regression/contracts/assigns_enforce_malloc_01/main.c b/regression/contracts/assigns_enforce_malloc_01/main.c index 60d061cb537..f3b91ea8147 100644 --- a/regression/contracts/assigns_enforce_malloc_01/main.c +++ b/regression/contracts/assigns_enforce_malloc_01/main.c @@ -1,4 +1,4 @@ -#include +#include int f1(int *a, int *b) __CPROVER_assigns(*a) { diff --git a/regression/contracts/assigns_enforce_malloc_02/main.c b/regression/contracts/assigns_enforce_malloc_02/main.c index eba0016c1e5..e634c9cb058 100644 --- a/regression/contracts/assigns_enforce_malloc_02/main.c +++ b/regression/contracts/assigns_enforce_malloc_02/main.c @@ -1,4 +1,4 @@ -#include +#include int f1(int *a, int *b) __CPROVER_assigns(*a) { diff --git a/regression/contracts/assigns_enforce_malloc_02/test.desc b/regression/contracts/assigns_enforce_malloc_02/test.desc index fdd13a65204..b5cae815df3 100644 --- a/regression/contracts/assigns_enforce_malloc_02/test.desc +++ b/regression/contracts/assigns_enforce_malloc_02/test.desc @@ -3,6 +3,8 @@ main.c --enforce-all-contracts ^EXIT=6$ ^SIGNAL=0$ +Call to malloc at location 18 falls between goto source location 23 and it's +destination at location 15. Unable to complete instrumentation, as this malloc may be in a loop.$ -- -- diff --git a/regression/contracts/assigns_enforce_scoping_01/main.c b/regression/contracts/assigns_enforce_scoping_01/main.c index 900251d0af2..e5ae6e48376 100644 --- a/regression/contracts/assigns_enforce_scoping_01/main.c +++ b/regression/contracts/assigns_enforce_scoping_01/main.c @@ -1,5 +1,3 @@ -#include - int f1(int *a, int *b) __CPROVER_assigns(*a) { if(*a > 0) diff --git a/regression/contracts/assigns_enforce_scoping_02/main.c b/regression/contracts/assigns_enforce_scoping_02/main.c index 11a80ee8c79..89e176e1e76 100644 --- a/regression/contracts/assigns_enforce_scoping_02/main.c +++ b/regression/contracts/assigns_enforce_scoping_02/main.c @@ -1,4 +1,4 @@ -#include +#include int f1(int *a, int *b) __CPROVER_assigns(*a) { diff --git a/regression/contracts/assigns_replace_01/main.c b/regression/contracts/assigns_replace_01/main.c index 64337adf9bd..d3f93979d10 100644 --- a/regression/contracts/assigns_replace_01/main.c +++ b/regression/contracts/assigns_replace_01/main.c @@ -9,7 +9,7 @@ int main() { int n = 6; foo(&n); + assert(n == 7); assert(n == 6); - return 0; } diff --git a/regression/contracts/assigns_replace_01/test.desc b/regression/contracts/assigns_replace_01/test.desc index 05341195e1c..6ca65891f80 100644 --- a/regression/contracts/assigns_replace_01/test.desc +++ b/regression/contracts/assigns_replace_01/test.desc @@ -3,6 +3,8 @@ main.c --replace-all-calls-with-contracts ^EXIT=10$ ^SIGNAL=0$ +assertion n == 7: FAILURE +assertion n == 6: FAILURE ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts/assigns_replace_05/test.desc b/regression/contracts/assigns_replace_05/test.desc index 9be0fb6b811..5e2bdc834ac 100644 --- a/regression/contracts/assigns_replace_05/test.desc +++ b/regression/contracts/assigns_replace_05/test.desc @@ -6,6 +6,7 @@ main.c ^VERIFICATION FAILED$ -- -- -This test checks that verification fails when assigns clauses are combined with function contracts in a loop improperly. +This test checks that verification fails when assigns clauses are combined with function contracts +in a loop improperly, i.e., always assumes memory not mention in ensures clauses are unchanged. BUG: Currently, function call replacement using 'ensures' specifications encodes an implicit assumption that any memory not mentioned in the ensures clause remains unchanged throughout the function, even when an 'assigns' clause is not present. diff --git a/regression/contracts/function_check_01/test.desc b/regression/contracts/function_check_01/test.desc index 1031d65d2e5..947fd5207b4 100644 --- a/regression/contracts/function_check_01/test.desc +++ b/regression/contracts/function_check_01/test.desc @@ -6,4 +6,4 @@ main.c ^VERIFICATION SUCCESSFUL$ -- -- ---replace-all-calls-with-contracts is the current name for the flag. This should be updated as the flag changes. +This tests a simple example of a function with requires and ensures which should both be satisfied. From 071a7258044d886d8640f370cffba387dbdeb438 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Thu, 15 Oct 2020 01:07:57 -0400 Subject: [PATCH 5/5] Cleans-up the implementation to support assigns clauses Signed-off-by: Felipe R. Monteiro --- .../assigns_enforce_malloc_02/test.desc | 4 +- src/ansi-c/c_typecheck_code.cpp | 6 +- src/ansi-c/c_typecheck_expr.cpp | 3 +- src/goto-instrument/code_contracts.cpp | 76 +++++++++---------- src/goto-instrument/code_contracts.h | 2 +- 5 files changed, 43 insertions(+), 48 deletions(-) diff --git a/regression/contracts/assigns_enforce_malloc_02/test.desc b/regression/contracts/assigns_enforce_malloc_02/test.desc index b5cae815df3..6acfd6a0854 100644 --- a/regression/contracts/assigns_enforce_malloc_02/test.desc +++ b/regression/contracts/assigns_enforce_malloc_02/test.desc @@ -3,9 +3,7 @@ main.c --enforce-all-contracts ^EXIT=6$ ^SIGNAL=0$ -Call to malloc at location 18 falls between goto source location 23 and it's -destination at location 15. Unable to complete instrumentation, as this -malloc may be in a loop.$ +Unable to complete instrumentation, as this malloc may be in a loop.$ -- -- This test checks that an error is thrown when malloc is called within a loop. diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp index 513277e4b59..480d80b0bb2 100644 --- a/src/ansi-c/c_typecheck_code.cpp +++ b/src/ansi-c/c_typecheck_code.cpp @@ -814,14 +814,14 @@ void c_typecheck_baset::typecheck_assigns( // Make sure there is an assigns clause to check if(assigns.is_not_nil()) { - for(code_typet::parametert curr_param : function_declarator.parameters()) + for(const auto &curr_param : function_declarator.parameters()) { if(curr_param.id() == ID_declaration) { - ansi_c_declarationt ¶m_declaration = + const ansi_c_declarationt ¶m_declaration = to_ansi_c_declaration(curr_param); - for(auto &decl : param_declaration.declarators()) + for(const auto &decl : param_declaration.declarators()) { typecheck_assigns(decl, assigns); } diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 2618c1fd928..802a6daa23f 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -477,8 +477,7 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr) else { error().source_location = expr.source_location(); - error() << "expression categorized improperly during parsing: " - << expr.pretty() << eom; + error() << "unexpected expression: " << expr.pretty() << eom; throw 0; } } diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index 545c2271a1f..23a369a2391 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -11,12 +11,7 @@ Date: February 2016 /// \file /// Verify and use annotated invariants and pre/post-conditions -#include "code_contracts.h" -#include "loop_utils.h" - #include -#include -#include #include #include @@ -32,6 +27,9 @@ Date: February 2016 #include #include +#include "code_contracts.h" +#include "loop_utils.h" + /// Predicate to be used with the exprt::visit() function. The function /// found_return_value() will return `true` iff this predicate is called on an /// expr that contains `__CPROVER_return_value`. @@ -70,12 +68,15 @@ static void check_apply_invariants( PRECONDITION(!loop.empty()); // find the last back edge - goto_programt::targett loop_end = loop_head; - for(loopt::const_iterator it = loop.begin(); it != loop.end(); ++it) - if( - (*it)->is_goto() && (*it)->get_target() == loop_head && - (*it)->location_number > loop_end->location_number) - loop_end = *it; + goto_programt::targett loop_end=loop_head; + for(loopt::const_iterator + it=loop.begin(); + it!=loop.end(); + ++it) + if((*it)->is_goto() && + (*it)->get_target()==loop_head && + (*it)->location_number>loop_end->location_number) + loop_end=*it; // see whether we have an invariant exprt invariant = static_cast( @@ -138,7 +139,7 @@ static void check_apply_invariants( // change the back edge into assume(false) or assume(guard) loop_end->targets.clear(); - loop_end->type = ASSUME; + loop_end->type=ASSUME; if(loop_head->is_goto()) loop_end->set_condition(false_exprt()); else @@ -149,10 +150,11 @@ bool code_contractst::has_contract(const irep_idt fun_name) { const symbolt &function_symbol = ns.lookup(fun_name); const code_typet &type = to_code_type(function_symbol.type); - const irept assigns = type.find(ID_C_spec_assigns); - const irept ensures = type.find(ID_C_spec_ensures); + if(type.find(ID_C_spec_assigns).is_not_nil()) + return true; - return ensures.is_not_nil() || assigns.is_not_nil(); + return type.find(ID_C_spec_requires).is_not_nil() || + type.find(ID_C_spec_ensures).is_not_nil(); } bool code_contractst::apply_contract( @@ -223,7 +225,7 @@ bool code_contractst::apply_contract( } // Replace formal parameters - code_function_callt::argumentst::const_iterator a_it = + code_function_callt::argumentst::const_iterator a_it= call.arguments().begin(); for(code_typet::parameterst::const_iterator p_it = type.parameters().begin(); p_it != type.parameters().end() && a_it != call.arguments().end(); @@ -260,11 +262,7 @@ bool code_contractst::apply_contract( const exprt::operandst &targets = assigns.operands(); for(const exprt &curr_op : targets) { - if(curr_op.id() == ID_symbol) - { - assigns_tgts.insert(curr_op); - } - else if(curr_op.id() == ID_dereference) + if(curr_op.id() == ID_symbol || curr_op.id() == ID_dereference) { assigns_tgts.insert(curr_op); } @@ -335,7 +333,7 @@ const symbolt &code_contractst::new_tmp_symbol( symbol_table); } -exprt create_alias_expression( +static exprt create_alias_expression( const exprt &assigns, const exprt &lhs, std::vector &aliasable_references) @@ -344,9 +342,9 @@ exprt create_alias_expression( exprt running = false_exprt(); for(auto aliasable : aliasable_references) { - exprt leftPtr = address_of_exprt{lhs}; - exprt rightPtr = aliasable; - exprt same = same_object(leftPtr, rightPtr); + exprt left_ptr = address_of_exprt{lhs}; + exprt right_ptr = aliasable; + exprt same = same_object(left_ptr, right_ptr); if(first_iter) { @@ -372,13 +370,12 @@ void code_contractst::populate_assigns_references( std::vector &created_references) { const code_typet &type = to_code_type(function_symbol.type); - exprt assigns = static_cast(type.find(ID_C_spec_assigns)); + const exprt &assigns = + static_cast(type.find(ID_C_spec_assigns)); - exprt::operandst &targets = assigns.operands(); - for(exprt curr_op : targets) + const exprt::operandst &targets = assigns.operands(); + for(const exprt &curr_op : targets) { - exprt op_addr = address_of_exprt{curr_op}; - // Declare a new symbol to stand in for the reference symbol_exprt standin = new_tmp_symbol( pointer_type(curr_op.type()), @@ -391,14 +388,15 @@ void code_contractst::populate_assigns_references( goto_programt::make_decl(standin, function_symbol.location)); created_decls.add(goto_programt::make_assignment( - code_assignt(standin, std::move(op_addr)), function_symbol.location)); + 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); } } -void code_contractst::instrument_assn_statement( +void code_contractst::instrument_assigns_statement( goto_programt::instructionst::iterator &instruction_iterator, goto_programt &program, exprt &assigns, @@ -407,7 +405,7 @@ void code_contractst::instrument_assn_statement( { INVARIANT( instruction_iterator->is_assign(), - "The first argument of instrument_assn_statement should always be" + "The first argument of instrument_assigns_statement should always be" " an assignment"); const exprt &lhs = instruction_iterator->get_assign().lhs(); if(freely_assignable_exprs.find(lhs) != freely_assignable_exprs.end()) @@ -569,7 +567,7 @@ bool code_contractst::check_for_looped_mallocs(const goto_programt &program) const irep_idt &called_name = to_symbol_expr(call.function()).get_identifier(); - if(std::strcmp(called_name.c_str(), "malloc") == 0) + if(called_name == "malloc") { malloc_calls.push_back(instruction); } @@ -666,7 +664,7 @@ bool code_contractst::add_pointer_checks(const std::string &function_name) // Insert aliasing assertions for(; instruction_iterator != program.instructions.end(); - std::advance(instruction_iterator, 1)) + ++instruction_iterator) { if(instruction_iterator->is_decl()) { @@ -674,7 +672,7 @@ bool code_contractst::add_pointer_checks(const std::string &function_name) } else if(instruction_iterator->is_assign()) { - instrument_assn_statement( + instrument_assigns_statement( instruction_iterator, program, assigns, @@ -779,7 +777,7 @@ void code_contractst::add_contract_check( static_cast(gf.type.find(ID_C_spec_ensures)); INVARIANT( ensures.is_not_nil() || assigns.is_not_nil(), - "Code conract enforcement is trivial without an ensures or assigns " + "Code contract enforcement is trivial without an ensures or assigns " "clause."); // build: @@ -810,7 +808,7 @@ void code_contractst::add_contract_check( replace_symbolt replace; // decl ret - if(gf.type.return_type() != empty_typet()) + if(gf.type.return_type()!=empty_typet()) { symbol_exprt r = new_tmp_symbol( gf.type.return_type(), @@ -820,7 +818,7 @@ void code_contractst::add_contract_check( .symbol_expr(); check.add(goto_programt::make_decl(r, skip->source_location)); - call.lhs() = r; + call.lhs()=r; symbol_exprt ret_val(CPROVER_PREFIX "return_value", call.lhs().type()); replace.insert(ret_val, r); diff --git a/src/goto-instrument/code_contracts.h b/src/goto-instrument/code_contracts.h index 955294beb55..0c696de4437 100644 --- a/src/goto-instrument/code_contracts.h +++ b/src/goto-instrument/code_contracts.h @@ -104,7 +104,7 @@ class code_contractst /// 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_assn_statement( + void instrument_assigns_statement( goto_programt::instructionst::iterator &ins_it, goto_programt &program, exprt &assigns,