From c29b69ab49ceca27216d24c54dd6aee442bb4a2a Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Thu, 6 May 2021 14:12:20 +0000 Subject: [PATCH] Support for empty assigns clause CBMC currently doesn't enforce assigns clauses if there isn't one. However, whenever enforcing a function contract, the absence of an assigns clause should be interpreted as an empty write set (i.e., no inputs will be modified by this function). CBMC now properly checks for empty assigns clause behavior. Signed-off-by: Felipe R. Monteiro --- .../contracts/assigns_enforce_05/test.desc | 8 ++- .../contracts/assigns_enforce_15/main.c | 29 ++++++++ .../contracts/assigns_enforce_15/test.desc | 12 ++++ regression/contracts/function_check_02/main.c | 8 ++- .../quantifiers-exists-ensures-01/main.c | 10 +-- .../quantifiers-forall-ensures-01/main.c | 10 +-- .../contracts/quantifiers-nested-01/main.c | 18 ++--- .../contracts/quantifiers-nested-03/main.c | 2 +- src/goto-instrument/code_contracts.cpp | 71 ++++++++----------- 9 files changed, 104 insertions(+), 64 deletions(-) create mode 100644 regression/contracts/assigns_enforce_15/main.c create mode 100644 regression/contracts/assigns_enforce_15/test.desc diff --git a/regression/contracts/assigns_enforce_05/test.desc b/regression/contracts/assigns_enforce_05/test.desc index 52c7a660e1f..cd77e245ca1 100644 --- a/regression/contracts/assigns_enforce_05/test.desc +++ b/regression/contracts/assigns_enforce_05/test.desc @@ -1,9 +1,11 @@ CORE main.c --enforce-all-contracts -^EXIT=10$ +^EXIT=0$ ^SIGNAL=0$ -^VERIFICATION FAILED$ +^\[f1.1\] line \d+ .*: SUCCESS$ +^VERIFICATION SUCCESSFUL$ -- -- -This test checks that verification fails when a function with an assigns clause calls a function without an assigns clause. +This test checks that verification succeeds when enforcing a contract +for functions, without assigns clauses, that don't modify anything. diff --git a/regression/contracts/assigns_enforce_15/main.c b/regression/contracts/assigns_enforce_15/main.c new file mode 100644 index 00000000000..aa0813b2622 --- /dev/null +++ b/regression/contracts/assigns_enforce_15/main.c @@ -0,0 +1,29 @@ +int global = 0; + +int foo(int *x) __CPROVER_assigns(*x) + __CPROVER_ensures(__CPROVER_return_value == *x + 5) +{ + int z = 5; + int y = bar(&z); + return *x + 5; +} + +int bar(int *a) __CPROVER_ensures(__CPROVER_return_value >= 5) +{ + *a = *a + 2; + return *a; +} + +int baz() __CPROVER_ensures(__CPROVER_return_value == global) +{ + global = global + 1; + return global; +} + +int main() +{ + int n; + n = foo(&n); + n = baz(); + return 0; +} diff --git a/regression/contracts/assigns_enforce_15/test.desc b/regression/contracts/assigns_enforce_15/test.desc new file mode 100644 index 00000000000..bd91dedff9f --- /dev/null +++ b/regression/contracts/assigns_enforce_15/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=10$ +^SIGNAL=0$ +^\[bar.1\] line \d+ .*: FAILURE$ +^\[baz.1\] line \d+ .*: FAILURE$ +^VERIFICATION FAILED$ +-- +-- +Checks whether verification fails when enforcing a contract +for functions, without assigns clauses, that modify an input. diff --git a/regression/contracts/function_check_02/main.c b/regression/contracts/function_check_02/main.c index 020113bd1d5..d0b17f5fc34 100644 --- a/regression/contracts/function_check_02/main.c +++ b/regression/contracts/function_check_02/main.c @@ -4,10 +4,16 @@ // A known bug (resolved in PR #2278) causes the use of quantifiers // in ensures to fail. +// clang-format off int initialize(int *arr) + __CPROVER_assigns(*arr) __CPROVER_ensures( - __CPROVER_forall {int i; (0 <= i && i < 10) ==> arr[i] == i} + __CPROVER_forall { + int i; + (0 <= i && i < 10) ==> arr[i] == i + } ) +// clang-format on { for(int i = 0; i < 10; i++) { diff --git a/regression/contracts/quantifiers-exists-ensures-01/main.c b/regression/contracts/quantifiers-exists-ensures-01/main.c index 45f066045ba..ad4d3964ed3 100644 --- a/regression/contracts/quantifiers-exists-ensures-01/main.c +++ b/regression/contracts/quantifiers-exists-ensures-01/main.c @@ -1,8 +1,10 @@ // clang-format off -int f1(int *arr) __CPROVER_ensures(__CPROVER_exists { - int i; - (0 <= i && i < 10) ==> arr[i] == i -}) +int f1(int *arr) + __CPROVER_assigns(*arr) + __CPROVER_ensures(__CPROVER_exists { + int i; + (0 <= i && i < 10) ==> arr[i] == i + }) // clang-format on { for(int i = 0; i < 10; i++) diff --git a/regression/contracts/quantifiers-forall-ensures-01/main.c b/regression/contracts/quantifiers-forall-ensures-01/main.c index b558cc6aedc..7e601ea0282 100644 --- a/regression/contracts/quantifiers-forall-ensures-01/main.c +++ b/regression/contracts/quantifiers-forall-ensures-01/main.c @@ -1,8 +1,10 @@ // clang-format off -int f1(int *arr) __CPROVER_ensures(__CPROVER_forall { - int i; - (0 <= i && i < 10) ==> arr[i] == 0 -}) +int f1(int *arr) + __CPROVER_assigns(*arr) + __CPROVER_ensures(__CPROVER_forall { + int i; + (0 <= i && i < 10) ==> arr[i] == 0 + }) // clang-format on { for(int i = 0; i < 10; i++) diff --git a/regression/contracts/quantifiers-nested-01/main.c b/regression/contracts/quantifiers-nested-01/main.c index 7c10be47028..d26dda4fb79 100644 --- a/regression/contracts/quantifiers-nested-01/main.c +++ b/regression/contracts/quantifiers-nested-01/main.c @@ -1,12 +1,14 @@ // clang-format off -int f1(int *arr) __CPROVER_ensures(__CPROVER_forall { - int i; - __CPROVER_forall - { - int j; - (0 <= i && i < 10 && i <= j && j < 10) ==> arr[i] <= arr[j] - } -}) +int f1(int *arr) + __CPROVER_assigns(*arr) + __CPROVER_ensures(__CPROVER_forall { + int i; + __CPROVER_forall + { + int j; + (0 <= i && i < 10 && i <= j && j < 10) ==> arr[i] <= arr[j] + } + }) // clang-format on { for(int i = 0; i < 10; i++) diff --git a/regression/contracts/quantifiers-nested-03/main.c b/regression/contracts/quantifiers-nested-03/main.c index 7a52ffd4142..eb991a2c8b2 100644 --- a/regression/contracts/quantifiers-nested-03/main.c +++ b/regression/contracts/quantifiers-nested-03/main.c @@ -1,4 +1,4 @@ -int f1(int *arr) +int f1(int *arr) __CPROVER_assigns(*arr) __CPROVER_ensures(__CPROVER_return_value == 0 && __CPROVER_exists { int i; (0 <= i && i < 10) && arr[i] == i diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index 79de7f0a457..28b6eec8aaa 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -513,50 +513,38 @@ void code_contractst::instrument_call_statement( exprt called_assigns = to_code_with_contract_type(called_symbol.type).assigns(); - if(called_assigns.is_nil()) // Called function has no assigns clause - { - // Create a false assertion, so the analysis - // will fail if this function is called. - goto_programt failing_assertion; - failing_assertion.add(goto_programt::make_assertion( - false_exprt(), instruction_iterator->source_location)); - program.insert_before_swap(instruction_iterator, failing_assertion); - ++instruction_iterator; - - return; - } - else // Called function has assigns clause + if(!called_assigns.is_nil()) // 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) { - 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()) { - if(!p_it->get_identifier().empty()) - { - symbol_exprt p(p_it->get_identifier(), p_it->type()); - replace.insert(p, *a_it); - } + symbol_exprt p(p_it->get_identifier(), p_it->type()); + replace.insert(p, *a_it); } - - replace(called_assigns); - - // check compatibility of assigns clause with the called function - assigns_clauset called_assigns_clause( - called_assigns, *this, function_id, log); - exprt compatible = - assigns_clause.compatible_expression(called_assigns_clause); - goto_programt alias_assertion; - alias_assertion.add(goto_programt::make_assertion( - compatible, instruction_iterator->source_location)); - program.insert_before_swap(instruction_iterator, alias_assertion); - ++instruction_iterator; } + + replace(called_assigns); + + // check compatibility of assigns clause with the called function + assigns_clauset called_assigns_clause( + called_assigns, *this, function_id, log); + exprt compatible = + assigns_clause.compatible_expression(called_assigns_clause); + goto_programt alias_assertion; + alias_assertion.add(goto_programt::make_assertion( + compatible, instruction_iterator->source_location)); + program.insert_before_swap(instruction_iterator, alias_assertion); + ++instruction_iterator; + } } bool code_contractst::check_for_looped_mallocs(const goto_programt &program) @@ -634,9 +622,6 @@ bool code_contractst::add_pointer_checks(const std::string &function_name) const auto &type = to_code_with_contract_type(function_symbol.type); exprt assigns_expr = type.assigns(); - // Return if there are no reference checks to perform. - if(assigns_expr.is_nil()) - return false; assigns_clauset assigns(assigns_expr, *this, function_id, log);