diff --git a/doc/cprover-manual/contracts-assigns.md b/doc/cprover-manual/contracts-assigns.md index ffec6fa373c..dde47d8696c 100644 --- a/doc/cprover-manual/contracts-assigns.md +++ b/doc/cprover-manual/contracts-assigns.md @@ -6,7 +6,7 @@ __CPROVER_assigns(*identifier*, ...) ``` -An _assigns_ clause allows the user to specify that a memory location may be written by a function. The set of locations writable by a function is the union of the locations specified by the assigns clauses, or the empty set of no _assigns_ clause is specified. While, in general, an _assigns_ clause could be interpreted with wither _writes_ or _modifies_ semantics, this +An _assigns_ clause allows the user to specify that a memory location may be written by a function. The set of locations writable by a function is the union of the locations specified by the assigns clauses, or the empty set of no _assigns_ clause is specified. While, in general, an _assigns_ clause could be interpreted with either _writes_ or _modifies_ semantics, this design is based on the former. This means that memory not captured by an _assigns_ clause must not be written within the given function, even if the value(s) therein are not modified. @@ -15,10 +15,11 @@ value(s) therein are not modified. An _assigns_ clause currently supports simple variable types and their pointers, structs, and arrays. Recursive pointer structures are left to future work, as -their support would require changes to CBMC's memory model. For example, +their support would require changes to CBMC's memory model. ```c -int *err_signal; // Global variable +/* Examples */ +int err_signal; // Global variable int sum(const uint32_t a, const uint32_t b, uint32_t* out) __CPROVER_assigns(*out) @@ -49,10 +50,10 @@ int sum(const uint32_t a, const uint32_t b, uint32_t* out) /* Writable Set */ __CPROVER_assigns(*out) { - const uint64_t result = ((uint64_t) a) + ((uint64_t) b); - if (result > UINT32_MAX) return FAILURE; - *out = (uint32_t) result; - return SUCCESS; + const uint64_t result = ((uint64_t) a) + ((uint64_t) b); + if (result > UINT32_MAX) return FAILURE; + *out = (uint32_t) result; + return SUCCESS; } ``` @@ -65,28 +66,28 @@ is one of those options. ```c int __CPROVER_contracts_original_sum(const uint32_t a, const uint32_t b, uint32_t* out) { - const uint64_t result; - __CPROVER_assert((__CPROVER_POINTER_OBJECT(&result) == __CPROVER_POINTER_OBJECT(out) && - __CPROVER_POINTER_OFFSET(&result) == __CPROVER_POINTER_OFFSET(out)) || - (__CPROVER_POINTER_OBJECT(&result) == __CPROVER_POINTER_OBJECT(&result) && - __CPROVER_POINTER_OFFSET(&result) == __CPROVER_POINTER_OFFSET(&result)) - , "Check that result is assignable"); - result = ((uint64_t) *a) + ((uint64_t) *b); - if (result > UINT32_MAX) return FAILURE; - __CPROVER_assert((__CPROVER_POINTER_OBJECT(out) == __CPROVER_POINTER_OBJECT(out) && - __CPROVER_POINTER_OFFSET(out) == __CPROVER_POINTER_OFFSET(out)) || - (__CPROVER_POINTER_OBJECT(out) == __CPROVER_POINTER_OBJECT(&result) && - __CPROVER_POINTER_OFFSET(out) == __CPROVER_POINTER_OFFSET(&result)) - , "Check that result is assignable"); - *out = (uint32_t) result; - return SUCCESS; + const uint64_t result; + __CPROVER_assert((__CPROVER_POINTER_OBJECT(&result) == __CPROVER_POINTER_OBJECT(out) && + __CPROVER_POINTER_OFFSET(&result) == __CPROVER_POINTER_OFFSET(out)) || + (__CPROVER_POINTER_OBJECT(&result) == __CPROVER_POINTER_OBJECT(&result) && + __CPROVER_POINTER_OFFSET(&result) == __CPROVER_POINTER_OFFSET(&result)) + , "Check that result is assignable"); + result = ((uint64_t) a) + ((uint64_t) b); + if (result > UINT32_MAX) return FAILURE; + __CPROVER_assert((__CPROVER_POINTER_OBJECT(out) == __CPROVER_POINTER_OBJECT(out) && + __CPROVER_POINTER_OFFSET(out) == __CPROVER_POINTER_OFFSET(out)) || + (__CPROVER_POINTER_OBJECT(out) == __CPROVER_POINTER_OBJECT(&result) && + __CPROVER_POINTER_OFFSET(out) == __CPROVER_POINTER_OFFSET(&result)) + , "Check that result is assignable"); + *out = (uint32_t) result; + return SUCCESS; } /* Function Contract Enforcement */ int sum(const uint32_t a, const uint32_t b, uint32_t* out) { - int return_value_sum = __CPROVER_contracts_original_sum(a, b, out); - return return_value_sum; + int return_value_sum = __CPROVER_contracts_original_sum(a, b, out); + return return_value_sum; } ``` @@ -101,7 +102,8 @@ considered assignable as well. Finally, a set of freely-assignable symbols *free* is tracked during the traversal of the function body. These are locally-defined variables and formal parameters without dereferences. For example, in a variable declaration ` -x = `, `x` would be added to *free*. Assignment statements where the left-hand-side is in *free* are not instrumented with the above assertions. +x = `, `x` would be added to the *free* set. Assignment statements +where the left-hand-side is in the *free* set are not instrumented with the above assertions. #### Replacement @@ -112,7 +114,7 @@ Clauses](contracts-requires-and-ensures.md) - Replacement section, and it will a non-deterministic assignments for each object listed in the `__CPROVER_assigns` clause. Since these objects might be modified by the function, CBMC uses non-deterministic assignments to havoc them and restrict their values only by -assuming the postconditions. +assuming the postconditions (i.e., requires clauses). In our example, consider that a function `foo` may call `sum`. @@ -126,21 +128,21 @@ __CPROVER_ensures((__CPROVER_return_value == SUCCESS) ==> (*out == (a + b))) /* Writable Set */ __CPROVER_assigns(*out) { - const uint64_t result = ((uint64_t) a) + ((uint64_t) b); - if (result > UINT32_MAX) return FAILURE; - *out = (uint32_t) result; - return SUCCESS; + const uint64_t result = ((uint64_t) a) + ((uint64_t) b); + if (result > UINT32_MAX) return FAILURE; + *out = (uint32_t) result; + return SUCCESS; } int foo() { - uint32_t a; - uint32_t b; - uint32_t out; - int rval = sum(a, b, &out); - if (rval == SUCCESS) - return out; - return rval; + uint32_t a; + uint32_t b; + uint32_t out; + int rval = sum(a, b, &out); + if (rval == SUCCESS) + return out; + return rval; } ``` @@ -150,26 +152,25 @@ wherever the function is called. ```c int foo() { - uint32_t a; - uint32_t b; - uint32_t out; + uint32_t a; + uint32_t b; + uint32_t out; + /* Function Contract Replacement */ + /* Precondition */ + __CPROVER_assert(__CPROVER_is_fresh(out, sizeof(*out)), "Check requires clause"); - /* Function Contract Replacement */ - /* Precondition */ - __CPROVER_assert(__CPROVER_is_fresh(out, sizeof(*out)), "Check requires clause"); + /* Writable Set */ + *(&out) = nondet_uint32_t(); - /* Writable Set */ - *(&out) = nondet_uint32_t(); - - /* Postconditions */ - int return_value_sum = nondet_int(); - __CPROVER_assume(return_value_sum == SUCCESS || return_value_sum == FAILURE); - __CPROVER_assume((return_value_sum == SUCCESS) ==> (*out == (*a + *b))); - - int rval = return_value_sum; - if (rval == SUCCESS) - return out; - return rval; + /* Postconditions */ + int return_value_sum = nondet_int(); + __CPROVER_assume(return_value_sum == SUCCESS || return_value_sum == FAILURE); + __CPROVER_assume((return_value_sum == SUCCESS) ==> (*out == (a + b))); + + int rval = return_value_sum; + if (rval == SUCCESS) + return out; + return rval; } ``` diff --git a/doc/cprover-manual/contracts-history-variables.md b/doc/cprover-manual/contracts-history-variables.md index 90f3eaa5dda..ad096ada3a6 100644 --- a/doc/cprover-manual/contracts-history-variables.md +++ b/doc/cprover-manual/contracts-history-variables.md @@ -14,8 +14,7 @@ _ensures_ clause. ### Parameters `__CPROVER_old` takes a single argument, which is the identifier corresponding to -a parameter of the function. For now, only scalar, structs, or pointer types are supported. - +a parameter of the function. For now, only scalar or pointer types are supported. ### Semantics @@ -24,13 +23,12 @@ bellow. If the function returns a failure code, the value of `*out` should not have been modified. ```c -int sum(uint32_t* a, uint32_t* b, uint32_t* out) - +int sum(const uint32_t a, const uint32_t b, uint32_t* out) /* Postconditions */ __CPROVER_ensures((__CPROVER_return_value == FAILURE) ==> (*out == __CPROVER_old(*out))) /* Writable Set */ __CPROVER_assigns(*out) { - /* ... */ + /* ... */ } ``` diff --git a/doc/cprover-manual/contracts-memory-predicates.md b/doc/cprover-manual/contracts-memory-predicates.md index f1a9b9fcc5d..90784cf3928 100644 --- a/doc/cprover-manual/contracts-memory-predicates.md +++ b/doc/cprover-manual/contracts-memory-predicates.md @@ -1,6 +1,5 @@ # Memory Predicates - ### Syntax ```c @@ -8,7 +7,7 @@ bool __CPROVER_is_fresh(void *p, size_t size); ``` To specify memory footprint we use a special function called `__CPROVER_is_fresh `. The meaning of `__CPROVER_is_fresh` is that we are borrowing a pointer from the -external environment (in a precondition), or returning it to the calling context (in a postcondition). +external environment (in a precondition), or returning it to the calling context (in a postcondition). ### Parameters @@ -33,12 +32,12 @@ __CPROVER_requires(__CPROVER_is_fresh(out, sizeof(*out))) __CPROVER_ensures(__CPROVER_is_fresh(err_signal, sizeof(*err_signal))) __CPROVER_assigns(*out, err_signal) { - const uint64_t result = ((uint64_t) a) + ((uint64_t) b); - err_signal = malloc(sizeof(*err_signal)); - if (!err_signal) return; - if (result > UINT32_MAX) *err_signal = FAILURE; - *out = (uint32_t) result; - *err_signal = SUCCESS; + const uint64_t result = ((uint64_t) a) + ((uint64_t) b); + err_signal = malloc(sizeof(*err_signal)); + if (!err_signal) return; + if (result > UINT32_MAX) *err_signal = FAILURE; + *out = (uint32_t) result; + *err_signal = SUCCESS; } ``` @@ -53,21 +52,21 @@ int *err_signal; // Global variable int __CPROVER_contracts_original_sum(const uint32_t a, const uint32_t b, uint32_t* out) { - const uint64_t result = ((uint64_t) a) + ((uint64_t) b); - err_signal = malloc(sizeof(*err_signal)); - if (!err_signal) return; - if (result > UINT32_MAX) *err_signal = FAILURE; - *out = (uint32_t) result; - *err_signal = SUCCESS; + const uint64_t result = ((uint64_t) a) + ((uint64_t) b); + err_signal = malloc(sizeof(*err_signal)); + if (!err_signal) return; + if (result > UINT32_MAX) *err_signal = FAILURE; + *out = (uint32_t) result; + *err_signal = SUCCESS; } /* Function Contract Enforcement */ int sum(const uint32_t a, const uint32_t b, uint32_t* out) { - __CPROVER_assume(__CPROVER_is_fresh(out, sizeof(*out))); // Assumes out is freshly allocated - int return_value_sum = __CPROVER_contracts_original_sum(a, b, out); - __CPROVER_assert(__CPROVER_is_fresh(err_signal, sizeof(*err_signal)), "Check ensures clause"); - return return_value_sum; + __CPROVER_assume(__CPROVER_is_fresh(out, sizeof(*out))); // Assumes out is freshly allocated + int return_value_sum = __CPROVER_contracts_original_sum(a, b, out); + __CPROVER_assert(__CPROVER_is_fresh(err_signal, sizeof(*err_signal)), "Check ensures clause"); + return return_value_sum; } ``` @@ -80,11 +79,11 @@ int *err_signal; // Global variable int foo() { - uint32_t a; - uint32_t b; - uint32_t out; - sum(a, b, &out); - return *err_signal; + uint32_t a; + uint32_t b; + uint32_t out; + sum(a, b, &out); + return *err_signal; } ``` @@ -98,21 +97,21 @@ int *err_signal; // Global variable int foo() { - uint32_t a; - uint32_t b; - uint32_t out; + uint32_t a; + uint32_t b; + uint32_t out; - /* Function Contract Replacement */ - /* Precondition */ - __CPROVER_assert(__CPROVER_is_fresh(out, sizeof(*out)), "Check requires clause"); + /* Function Contract Replacement */ + /* Precondition */ + __CPROVER_assert(__CPROVER_is_fresh(out, sizeof(*out)), "Check requires clause"); - /* Writable Set */ - *(&out) = nondet_uint32_t(); - err_signal = nondet_int_pointer(); + /* Writable Set */ + *(&out) = nondet_uint32_t(); + err_signal = nondet_int_pointer(); - /* Postconditions */ - __CPROVER_assume(__CPROVER_is_fresh(err_signal, sizeof(*err_signal))); // Assumes out is allocated + /* Postconditions */ + __CPROVER_assume(__CPROVER_is_fresh(err_signal, sizeof(*err_signal))); // Assumes out is allocated - return *err_signal; + return *err_signal; } -``` \ No newline at end of file +``` diff --git a/doc/cprover-manual/contracts-requires-and-ensures.md b/doc/cprover-manual/contracts-requires-and-ensures.md index 5863ecd3286..3006ddfed14 100644 --- a/doc/cprover-manual/contracts-requires-and-ensures.md +++ b/doc/cprover-manual/contracts-requires-and-ensures.md @@ -37,17 +37,17 @@ contexts: enforcement and replacement. To illustrate these two perspectives, consider the following implementation of the `sum` function. ```c -int sum(uint32_t a, uint32_t b, uint32_t* out) -/* Preconditions */ +int sum(const uint32_t a, const uint32_t b, uint32_t* out) +/* Precondition */ __CPROVER_requires(__CPROVER_is_fresh(out, sizeof(*out))) /* Postconditions */ __CPROVER_ensures(__CPROVER_return_value == SUCCESS || __CPROVER_return_value == FAILURE) -__CPROVER_ensures((__CPROVER_return_value == SUCCESS) ==> (*out == (*a + *b))) +__CPROVER_ensures((__CPROVER_return_value == SUCCESS) ==> (*out == (a + b))) { - const uint64_t result = ((uint64_t) a) + ((uint64_t) b); - if (result > UINT32_MAX) return FAILURE; - *out = (uint32_t) result; - return SUCCESS; + const uint64_t result = ((uint64_t) a) + ((uint64_t) b); + if (result > UINT32_MAX) return FAILURE; + *out = (uint32_t) result; + return SUCCESS; } ``` @@ -97,13 +97,13 @@ In our example, consider that a function `foo` may call `sum`. ```c int foo() { - uint32_t a; - uint32_t b; - uint32_t out; - int rval = sum(a, b, &out); - if (rval == SUCCESS) - return out; - return rval; + uint32_t a; + uint32_t b; + uint32_t out; + int rval = sum(a, b, &out); + if (rval == SUCCESS) + return out; + return rval; } ``` @@ -113,22 +113,22 @@ wherever the function is called. ```c int foo() { - uint32_t a; - uint32_t b; - uint32_t out; + uint32_t a; + uint32_t b; + uint32_t out; - /* Function Contract Replacement */ - /* Precondition */ - __CPROVER_assert(__CPROVER_is_fresh(out, sizeof(*out)), "Check requires clause"); + /* Function Contract Replacement */ + /* Precondition */ + __CPROVER_assert(__CPROVER_is_fresh(out, sizeof(*out)), "Check requires clause"); - /* Postconditions */ - int return_value_sum = nondet_int(); - __CPROVER_assume(return_value_sum == SUCCESS || return_value_sum == FAILURE); - __CPROVER_assume((return_value_sum == SUCCESS) ==> (*out == (*a + *b))); - - int rval = return_value_sum; - if (rval == SUCCESS) - return out; - return rval; + /* Postconditions */ + int return_value_sum = nondet_int(); + __CPROVER_assume(return_value_sum == SUCCESS || return_value_sum == FAILURE); + __CPROVER_assume((return_value_sum == SUCCESS) ==> (*out == (*a + *b))); + + int rval = return_value_sum; + if (rval == SUCCESS) + return out; + return rval; } ``` diff --git a/doc/cprover-manual/contracts.md b/doc/cprover-manual/contracts.md index 8d86f43d7fb..963910c9a0e 100644 --- a/doc/cprover-manual/contracts.md +++ b/doc/cprover-manual/contracts.md @@ -26,21 +26,21 @@ Take a look at the example below. int sum(const uint32_t a, const uint32_t b, uint32_t* out) { - const uint64_t result = ((uint64_t) a) + ((uint64_t) b); - if (result > UINT32_MAX) return FAILURE; - *out = (uint32_t) result; - return SUCCESS; + const uint64_t result = ((uint64_t) a) + ((uint64_t) b); + if (result > UINT32_MAX) return FAILURE; + *out = (uint32_t) result; + return SUCCESS; } int foo() { - uint32_t a; - uint32_t b; - uint32_t out; - int rval = sum(a, b, &out); - if (rval == SUCCESS) - return out; - return rval; + uint32_t a; + uint32_t b; + uint32_t out; + int rval = sum(a, b, &out); + if (rval == SUCCESS) + return out; + return rval; } ``` @@ -112,21 +112,21 @@ __CPROVER_requires(__CPROVER_is_fresh(out, sizeof(*out))) /* Postconditions */ __CPROVER_ensures(__CPROVER_return_value == SUCCESS || __CPROVER_return_value == FAILURE) __CPROVER_ensures((__CPROVER_return_value == SUCCESS) ==> (*out == (a + b))) -__CPROVER_ensures((__CPROVER_return_value == SUCCESS) ==> (*out == __CPROVER_old(*out))) +__CPROVER_ensures((__CPROVER_return_value == FAILURE) ==> (*out == __CPROVER_old(*out))) /* Write Set */ __CPROVER_assigns(*out) { - const uint64_t result = ((uint64_t) a) + ((uint64_t) b); - if (result > UINT32_MAX) return FAILURE; - *out = (uint32_t) result; - return SUCCESS; + const uint64_t result = ((uint64_t) a) + ((uint64_t) b); + if (result > UINT32_MAX) return FAILURE; + *out = (uint32_t) result; + return SUCCESS; } ``` First, we have to prove that the function satisfies the contract. ```shell - goto-cc -o sum.goto *.c + goto-cc -o sum.goto *.c --function sum goto-instrument --enforce-contract sum sum.goto sum-checking-contracts.goto cbmc sum-checking-contracts.goto --function sum ``` @@ -140,9 +140,9 @@ contract in place of the function implementation wherever the function is called. ```shell - goto-cc -o foo.goto *.c - goto-instrument --replace-call-with-contract foo foo.goto sum-using-contracts.goto - cbmc foo-using-contracts.goto --function foo + goto-cc -o foo.goto *.c --function foo + goto-instrument --replace-call-with-contract sum foo.goto foo-using-sum-contract.goto + cbmc foo-using-sum-contract.goto --function foo ``` The first command just compiles the GOTO program as usual, the second command @@ -157,4 +157,4 @@ program using contracts. - [Memory Predicates](contracts-memory-predicates.md) - [History Variables](contracts-history-variables.md) - [Quantifiers](contracts-quantifiers.md) -- [Loop Invariants \& Loop Variants]() +- [Loop Contracts]() diff --git a/regression/contracts/trivial_contract_enforce/main.c b/regression/contracts/trivial_contract_enforce/main.c new file mode 100644 index 00000000000..7c566446339 --- /dev/null +++ b/regression/contracts/trivial_contract_enforce/main.c @@ -0,0 +1,14 @@ +#include +#include + +int foo(int *x) __CPROVER_requires(x != NULL) +{ + return *x + 5; +} + +int main() +{ + int n = 10; + assert(foo(&n) != 15); + return 0; +} diff --git a/regression/contracts/trivial_contract_enforce/test.desc b/regression/contracts/trivial_contract_enforce/test.desc new file mode 100644 index 00000000000..6152a27cbcc --- /dev/null +++ b/regression/contracts/trivial_contract_enforce/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=10$ +^SIGNAL=0$ +^\[main.assertion.\d+\] line \d+ assertion foo\(\&n\) != 15\: FAILURE$ +^VERIFICATION FAILED$ +-- +-- +Check whether CBMC doesn't crash when enforcing trivial contracts, i.e., +the postcondition is true (default when missing) and therefore there is +nothing to check/assert. diff --git a/regression/contracts/trivial_contract_replace/main.c b/regression/contracts/trivial_contract_replace/main.c new file mode 100644 index 00000000000..6e6cb282db6 --- /dev/null +++ b/regression/contracts/trivial_contract_replace/main.c @@ -0,0 +1,13 @@ +#include + +int foo(int *x) __CPROVER_ensures(__CPROVER_return_value == *x + 5) +{ + return *x + 5; +} + +int main() +{ + int n = 10; + assert(foo(&n) != 15); + return 0; +} diff --git a/regression/contracts/trivial_contract_replace/test.desc b/regression/contracts/trivial_contract_replace/test.desc new file mode 100644 index 00000000000..ce065cb1fe6 --- /dev/null +++ b/regression/contracts/trivial_contract_replace/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=10$ +^SIGNAL=0$ +^\[main.assertion.\d+\] line \d+ assertion foo\(\&n\) != 15\: FAILURE$ +^VERIFICATION FAILED$ +-- +-- +Check whether CBMC doesn't crash when replacing trivial contracts, i.e., +the precondition is true (default when missing) and therefore there is +nothing to check/assert. diff --git a/src/goto-instrument/contracts/assigns.cpp b/src/goto-instrument/contracts/assigns.cpp index e41f9ebf8e0..76fa2f16cfb 100644 --- a/src/goto-instrument/contracts/assigns.cpp +++ b/src/goto-instrument/contracts/assigns.cpp @@ -38,7 +38,6 @@ assigns_clause_targett::assigns_clause_targett( symbolt standin_symbol = contract.new_tmp_symbol( pointer_object.type(), function_symbol.location, - function_id, function_symbol.mode); local_target = standin_symbol.symbol_expr(); diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index b60a2aa4706..23dc0519afa 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -51,7 +51,6 @@ exprt get_size(const typet &type, const namespacet &ns, messaget &log) void code_contractst::check_apply_loop_contracts( goto_functionst::goto_functiont &goto_function, - const irep_idt &function_name, const local_may_aliast &local_may_alias, const goto_programt::targett loop_head, const loopt &loop, @@ -161,12 +160,10 @@ void code_contractst::check_apply_loop_contracts( for(const auto &clause : decreases_clause.operands()) { old_temporary_variables.push_back( - new_tmp_symbol( - clause.type(), loop_head->source_location, function_name, mode) + new_tmp_symbol(clause.type(), loop_head->source_location, mode) .symbol_expr()); new_temporary_variables.push_back( - new_tmp_symbol( - clause.type(), loop_head->source_location, function_name, mode) + new_tmp_symbol(clause.type(), loop_head->source_location, mode) .symbol_expr()); } @@ -396,14 +393,12 @@ void code_contractst::replace_old_parameter( exprt &expr, std::map ¶meter2history, source_locationt location, - const irep_idt &function, const irep_idt &mode, goto_programt &history) { for(auto &op : expr.operands()) { - replace_old_parameter( - op, parameter2history, location, function, mode, history); + replace_old_parameter(op, parameter2history, location, mode, history); } if(expr.id() == ID_old) @@ -425,8 +420,7 @@ void code_contractst::replace_old_parameter( // 1. Create a temporary symbol expression that represents the // history variable symbol_exprt tmp_symbol = - new_tmp_symbol(dereference_expr.type(), location, function, mode) - .symbol_expr(); + new_tmp_symbol(dereference_expr.type(), location, mode).symbol_expr(); // 2. Associate the above temporary variable to it's corresponding // expression @@ -458,15 +452,13 @@ std::pair code_contractst::create_ensures_instruction( codet &expression, source_locationt location, - const irep_idt &function, const irep_idt &mode) { std::map parameter2history; goto_programt history; // Find and replace "old" expression in the "expression" variable - replace_old_parameter( - expression, parameter2history, location, function, mode, history); + replace_old_parameter(expression, parameter2history, location, mode, history); // Create instructions corresponding to the ensures clause goto_programt ensures_program; @@ -479,7 +471,6 @@ code_contractst::create_ensures_instruction( } bool code_contractst::apply_function_contract( - const irep_idt &function_id, goto_programt &goto_program, goto_programt::targett target) { @@ -500,11 +491,6 @@ bool code_contractst::apply_function_contract( auto requires = conjunction(type.requires()); auto ensures = conjunction(type.ensures()); - // Check to see if the function contract actually constrains its effect on - // the program state; if not, return. - if(ensures.is_true() && 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). // This object tracks replacements that are common to ENSURES and REQUIRES. @@ -568,7 +554,7 @@ bool code_contractst::apply_function_contract( is_fresh.create_declarations(); // Insert assertion of the precondition immediately before the call site. - if(requires.is_not_nil()) + if(!requires.is_true()) { replace_symbolt replace(common_replace); code_contractst::add_quantified_variable(requires, replace, mode); @@ -593,7 +579,7 @@ bool code_contractst::apply_function_contract( // Gather all the instructions required to handle history variables // as well as the ensures clause std::pair ensures_pair; - if(ensures.is_not_nil()) + if(!ensures.is_false()) { replace_symbolt replace(common_replace); code_contractst::add_quantified_variable(ensures, replace, mode); @@ -603,7 +589,6 @@ bool code_contractst::apply_function_contract( ensures_pair = create_ensures_instruction( assumption, ensures.source_location(), - function, symbol_table.lookup_ref(function).mode); // add all the history variable initialization instructions @@ -617,9 +602,9 @@ bool code_contractst::apply_function_contract( // in the assigns clause. if(assigns.is_not_nil()) { - assigns_clauset assigns_cause(assigns, *this, function_id, log); + assigns_clauset assigns_cause(assigns, *this, function, log); goto_programt assigns_havoc = assigns_cause.havoc_code( - function_symbol.location, function_id, function_symbol.mode); + function_symbol.location, function, function_symbol.mode); // Insert the non-deterministic assignment immediately before the call site. std::size_t lines_to_iterate = assigns_havoc.instructions.size(); @@ -629,7 +614,7 @@ bool code_contractst::apply_function_contract( // To remove the function call, insert statements related to the assumption. // Then, replace the function call with a SKIP statement. - if(ensures.is_not_nil()) + if(!ensures.is_false()) { is_fresh.update_ensures(ensures_pair.first); auto lines_to_iterate = ensures_pair.first.instructions.size(); @@ -644,7 +629,7 @@ bool code_contractst::apply_function_contract( } void code_contractst::apply_loop_contract( - const irep_idt &function_name, + const irep_idt &function, goto_functionst::goto_functiont &goto_function) { local_may_aliast local_may_alias(goto_function); @@ -656,34 +641,27 @@ void code_contractst::apply_loop_contract( { check_apply_loop_contracts( goto_function, - function_name, local_may_alias, loop.first, loop.second, - symbol_table.lookup_ref(function_name).mode); + symbol_table.lookup_ref(function).mode); } } const symbolt &code_contractst::new_tmp_symbol( const typet &type, const source_locationt &source_location, - const irep_idt &function_id, const irep_idt &mode) { return get_fresh_aux_symbol( type, - id2string(function_id) + "::tmp_cc", + id2string(source_location.get_function()) + "::tmp_cc", "tmp_cc", source_location, mode, symbol_table); } -const namespacet &code_contractst::get_namespace() const -{ - return ns; -} - symbol_tablet &code_contractst::get_symbol_table() { return symbol_table; @@ -736,7 +714,6 @@ void code_contractst::instrument_call_statement( goto_programt::instructionst::iterator &instruction_iterator, goto_programt &program, exprt &assigns, - const irep_idt &function_id, std::set &freely_assignable_symbols, assigns_clauset &assigns_clause) { @@ -832,7 +809,7 @@ void code_contractst::instrument_call_statement( // check compatibility of assigns clause with the called function assigns_clauset called_assigns_clause( - called_assigns, *this, function_id, log); + called_assigns, *this, called_name, log); exprt compatible = assigns_clause.compatible_expression(called_assigns_clause); goto_programt alias_assertion; @@ -997,7 +974,6 @@ void code_contractst::check_frame_conditions( instruction_it, program, assigns_expr, - target.name, freely_assignable_symbols, assigns); } @@ -1078,24 +1054,19 @@ bool code_contractst::enforce_contract(const irep_idt &function) } void code_contractst::add_contract_check( - const irep_idt &wrapper_fun, - const irep_idt &mangled_fun, + const irep_idt &wrapper_function, + const irep_idt &mangled_function, goto_programt &dest) { PRECONDITION(!dest.instructions.empty()); - const symbolt &function_symbol = ns.lookup(mangled_fun); + const symbolt &function_symbol = ns.lookup(mangled_function); const auto &code_type = to_code_with_contract_type(function_symbol.type); exprt assigns = code_type.assigns(); exprt requires = conjunction(code_type.requires()); exprt ensures = conjunction(code_type.ensures()); - INVARIANT( - !ensures.is_true() || assigns.is_not_nil(), - "Code contract enforcement is trivial without an ensures or assigns " - "clause."); - // build: // if(nondet) // decl ret @@ -1128,7 +1099,6 @@ void code_contractst::add_contract_check( symbol_exprt r = new_tmp_symbol( code_type.return_type(), skip->source_location, - wrapper_fun, function_symbol.mode) .symbol_expr(); check.add(goto_programt::make_decl(r, skip->source_location)); @@ -1142,7 +1112,7 @@ void code_contractst::add_contract_check( // decl parameter1 ... goto_functionst::function_mapt::iterator f_it = - goto_functions.function_map.find(mangled_fun); + goto_functions.function_map.find(mangled_function); PRECONDITION(f_it != goto_functions.function_map.end()); const goto_functionst::goto_functiont &gf = f_it->second; @@ -1153,7 +1123,6 @@ void code_contractst::add_contract_check( symbol_exprt p = new_tmp_symbol( parameter_symbol.type, skip->source_location, - wrapper_fun, parameter_symbol.mode) .symbol_expr(); check.add(goto_programt::make_decl(p, skip->source_location)); @@ -1165,11 +1134,11 @@ void code_contractst::add_contract_check( common_replace.insert(parameter_symbol.symbol_expr(), p); } - is_fresh_enforcet visitor(*this, log, wrapper_fun); + is_fresh_enforcet visitor(*this, log, wrapper_function); visitor.create_declarations(); // Generate: assume(requires) - if(requires.is_not_nil()) + if(!requires.is_false()) { // extend common_replace with quantified variables in REQUIRES, // and then do the replacement @@ -1189,7 +1158,7 @@ void code_contractst::add_contract_check( std::pair ensures_pair; // Generate: copies for history variables - if(ensures.is_not_nil()) + if(!ensures.is_true()) { // extend common_replace with quantified variables in ENSURES, // and then do the replacement @@ -1202,7 +1171,7 @@ void code_contractst::add_contract_check( auto assertion = code_assertt(ensures); assertion.add_source_location() = ensures.source_location(); ensures_pair = create_ensures_instruction( - assertion, ensures.source_location(), wrapper_fun, function_symbol.mode); + assertion, ensures.source_location(), function_symbol.mode); ensures_pair.first.instructions.back().source_location.set_comment( "Check ensures clause"); ensures_pair.first.instructions.back().source_location.set_property_class( @@ -1213,7 +1182,7 @@ void code_contractst::add_contract_check( check.destructive_append(ensures_pair.second); } - // ret=mangled_fun(parameter1, ...) + // ret=mangled_function(parameter1, ...) check.add(goto_programt::make_function_call(call, skip->source_location)); // Generate: assert(ensures) @@ -1232,15 +1201,14 @@ void code_contractst::add_contract_check( dest.destructive_insert(dest.instructions.begin(), check); } -bool code_contractst::replace_calls( - const std::set &funs_to_replace) +bool code_contractst::replace_calls(const std::set &functions) { bool fail = false; - for(const auto &fun : funs_to_replace) + for(const auto &function : functions) { - if(!has_contract(fun)) + if(!has_contract(function)) { - log.error() << "Function '" << fun + log.error() << "Function '" << function << "' does not have a contract; " "not replacing calls with contract." << messaget::eom; @@ -1261,17 +1229,14 @@ bool code_contractst::replace_calls( if(call.function().id() != ID_symbol) continue; - const irep_idt &function_name = + const irep_idt &called_function = to_symbol_expr(call.function()).get_identifier(); auto found = std::find( - funs_to_replace.begin(), - funs_to_replace.end(), - id2string(function_name)); - if(found == funs_to_replace.end()) + functions.begin(), functions.end(), id2string(called_function)); + if(found == functions.end()) continue; - fail |= apply_function_contract( - function_name, goto_function.second.body, ins); + fail |= apply_function_contract(goto_function.second.body, ins); } } } @@ -1295,52 +1260,51 @@ void code_contractst::apply_loop_contracts() bool code_contractst::replace_calls() { - std::set funs_to_replace; + std::set functions; for(auto &goto_function : goto_functions.function_map) { if(has_contract(goto_function.first)) - funs_to_replace.insert(id2string(goto_function.first)); + functions.insert(id2string(goto_function.first)); } - return replace_calls(funs_to_replace); + return replace_calls(functions); } bool code_contractst::enforce_contracts() { - std::set funs_to_enforce; + std::set functions; for(auto &goto_function : goto_functions.function_map) { if(has_contract(goto_function.first)) - funs_to_enforce.insert(id2string(goto_function.first)); + functions.insert(id2string(goto_function.first)); } - return enforce_contracts(funs_to_enforce); + return enforce_contracts(functions); } -bool code_contractst::enforce_contracts( - const std::set &funs_to_enforce) +bool code_contractst::enforce_contracts(const std::set &functions) { bool fail = false; - for(const auto &fun : funs_to_enforce) + for(const auto &function : functions) { - auto goto_function = goto_functions.function_map.find(fun); + auto goto_function = goto_functions.function_map.find(function); if(goto_function == goto_functions.function_map.end()) { fail = true; - log.error() << "Could not find function '" << fun + log.error() << "Could not find function '" << function << "' in goto-program; not enforcing contracts." << messaget::eom; continue; } - if(!has_contract(fun)) + if(!has_contract(function)) { fail = true; - log.error() << "Could not find any contracts within function '" << fun - << "'; nothing to enforce." << messaget::eom; + log.error() << "Could not find any contracts within function '" + << function << "'; nothing to enforce." << messaget::eom; continue; } if(!fail) - fail = enforce_contract(fun); + fail = enforce_contract(function); } return fail; } diff --git a/src/goto-instrument/contracts/contracts.h b/src/goto-instrument/contracts/contracts.h index 6afd15a8f6a..18e13f3976c 100644 --- a/src/goto-instrument/contracts/contracts.h +++ b/src/goto-instrument/contracts/contracts.h @@ -84,7 +84,7 @@ class code_contractst /// it using `cbmc --function F`. /// /// \return `true` on failure, `false` otherwise - bool replace_calls(const std::set &); + bool replace_calls(const std::set &functions); /// \brief Turn requires & ensures into assumptions and assertions for each of /// the named functions @@ -102,7 +102,7 @@ class code_contractst /// then asserts `CF`'s `ensures` clause. /// /// \return `true` on failure, `false` otherwise - bool enforce_contracts(const std::set &); + bool enforce_contracts(const std::set &functions); /// \brief Call enforce_contracts() on all functions that have a contract /// \return `true` on failure, `false` otherwise @@ -118,19 +118,15 @@ class code_contractst const symbolt &new_tmp_symbol( const typet &type, const source_locationt &source_location, - const irep_idt &function_id, const irep_idt &mode); void check_apply_loop_contracts( goto_functionst::goto_functiont &goto_function, - const irep_idt &function_name, const local_may_aliast &local_may_alias, const goto_programt::targett loop_head, const loopt &loop, const irep_idt &mode); - const namespacet &get_namespace() const; - // for "helper" classes to update symbol table. symbol_tablet &get_symbol_table(); goto_functionst &get_goto_functions(); @@ -158,7 +154,7 @@ class code_contractst /// 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 &); + bool check_for_looped_mallocs(const goto_programt &program); /// Inserts an assertion statement into program before the assignment /// instruction_it, to ensure that the left-hand-side of the assignment @@ -179,22 +175,9 @@ class code_contractst goto_programt::instructionst::iterator &ins_it, goto_programt &program, exprt &assigns, - const irep_idt &function_id, std::set &freely_assignable_symbols, assigns_clauset &assigns_clause); - /// Creates a local variable declaration for each expression in operands, - /// and stores them in created_declarations. Then creates assignment - /// statements to capture the memory addresses of each expression - /// in the assigns clause within the associated local variable, - /// populating a vector created_references of these local variables. - void populate_assigns_reference( - std::vector operands, - const symbolt &function_symbol, - const irep_idt &function_id, - goto_programt &created_declarations, - std::vector &created_references); - /// Creates a boolean expression which is true when there exists an expression /// in aliasable_references with the same pointer object and pointer offset as /// the address of lhs. @@ -202,20 +185,28 @@ class code_contractst const exprt &lhs, std::vector &aliasable_references); + /// Apply loop contracts, whenever available, to all loops in `function`. + /// Loop invariants, loop variants, and loop assigns clauses. void apply_loop_contract( - const irep_idt &function_name, + const irep_idt &function, goto_functionst::goto_functiont &goto_function); /// \brief Does the named function have a contract? bool has_contract(const irep_idt); + /// Replaces function calls with assertions based on requires clauses, + /// non-deterministic assignments for the write set, and assumptions + /// based on ensures clauses. bool apply_function_contract( - const irep_idt &function_id, goto_programt &goto_program, goto_programt::targett target); - void - add_contract_check(const irep_idt &, const irep_idt &, goto_programt &dest); + /// Instruments `wrapper_function` adding assumptions based on requires + /// clauses and assertions based on ensures clauses. + void add_contract_check( + const irep_idt &wrapper_function, + const irep_idt &mangled_function, + goto_programt &dest); /// This function recursively searches the expression to find nested or /// non-nested quantified expressions. When a quantified expression is found, @@ -232,7 +223,6 @@ class code_contractst exprt &expr, std::map ¶meter2history, source_locationt location, - const irep_idt &function, const irep_idt &mode, goto_programt &history); @@ -242,7 +232,6 @@ class code_contractst std::pair create_ensures_instruction( codet &expression, source_locationt location, - const irep_idt &function, const irep_idt &mode); }; diff --git a/src/goto-instrument/contracts/memory_predicates.cpp b/src/goto-instrument/contracts/memory_predicates.cpp index 2c98e0a24c6..8d1725399e0 100644 --- a/src/goto-instrument/contracts/memory_predicates.cpp +++ b/src/goto-instrument/contracts/memory_predicates.cpp @@ -227,8 +227,6 @@ void is_fresh_baset::update_fn_call( // fixing the function name. to_symbol_expr(call.function()).set_identifier(fn_name); - log.debug() << "printing updated call expression: " - << expr2c(call, parent.get_namespace()) << "\n"; ins->set_function_call(call); }