From 320a9f87485b242944126e35de6e233df3d3665c Mon Sep 17 00:00:00 2001 From: Remi Delmas Date: Fri, 3 Dec 2021 23:38:37 +0000 Subject: [PATCH] Havoc the function call's return value when replacing it by its contract. This was not done previously and could result in vacuous proofs when multiple calls to a same function were replaced in a same scope. --- .../replace-nondet-return-value/main.c | 23 +++++++++++ .../replace-nondet-return-value/test.desc | 20 +++++++++ src/goto-instrument/contracts/contracts.cpp | 41 ++++++++++++++----- 3 files changed, 74 insertions(+), 10 deletions(-) create mode 100644 regression/contracts/replace-nondet-return-value/main.c create mode 100644 regression/contracts/replace-nondet-return-value/test.desc diff --git a/regression/contracts/replace-nondet-return-value/main.c b/regression/contracts/replace-nondet-return-value/main.c new file mode 100644 index 00000000000..9b2d3684cfa --- /dev/null +++ b/regression/contracts/replace-nondet-return-value/main.c @@ -0,0 +1,23 @@ +int cmp(int i1, int i2) + // clang-format off + __CPROVER_ensures((i1 == i2) ==> (__CPROVER_return_value == 0)) + __CPROVER_ensures((i1 != i2) ==> (__CPROVER_return_value == -1)) +// clang-format on +{ + if(i1 == i2) + return 0; + else + return -1; +} + +int main() +{ + int ret = -1; + ret = cmp(0, 0); + __CPROVER_assert(ret == 0, "expecting SUCCESS"); + ret = cmp(0, 1); + __CPROVER_assert(ret == 0, "expecting FAILURE"); + __CPROVER_assert(ret == -1, "expecting SUCCESS"); + __CPROVER_assert(0, "expecting FAILURE"); + return 0; +} diff --git a/regression/contracts/replace-nondet-return-value/test.desc b/regression/contracts/replace-nondet-return-value/test.desc new file mode 100644 index 00000000000..d49794446bd --- /dev/null +++ b/regression/contracts/replace-nondet-return-value/test.desc @@ -0,0 +1,20 @@ +CORE +main.c +--replace-call-with-contract cmp +^EXIT=10$ +^SIGNAL=0$ +^\[main\.assertion\.1\] line \d+ expecting SUCCESS: SUCCESS$ +^\[main\.assertion\.2\] line \d+ expecting FAILURE: FAILURE$ +^\[main\.assertion\.3\] line \d+ expecting SUCCESS: SUCCESS$ +^\[main\.assertion\.4\] line \d+ expecting FAILURE: FAILURE$ +^\*\* 2 of 4 failed +^VERIFICATION FAILED$ +-- +-- +This test checks that the return value of a replaced function call is made +nondet at each replacement site. +The replaced function is called twice. Each call is expected to have a different +return value. If the return value of the call is not made nondet at each +replacement, it would be subject to contradictory constraints +(from the post conditions) and the assertions expected to fail would +be vacuously satisfied. diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index 0d5424c9df6..54f766be01f 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -23,6 +23,7 @@ Date: February 2016 #include #include +#include #include #include @@ -631,6 +632,10 @@ bool code_contractst::apply_function_contract( // with expressions from the call site (e.g. the return value). // This object tracks replacements that are common to ENSURES and REQUIRES. replace_symbolt common_replace; + + // keep track of the call's return expression to make it nondet later + optionalt call_ret_opt = {}; + if(type.return_type() != empty_typet()) { // Check whether the function's return value is not disregarded. @@ -640,9 +645,10 @@ bool code_contractst::apply_function_contract( // 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", const_target->call_lhs().type()); - common_replace.insert(ret_val, const_target->call_lhs()); + auto &lhs_expr = const_target->call_lhs(); + call_ret_opt = lhs_expr; + symbol_exprt ret_val(CPROVER_PREFIX "return_value", lhs_expr.type()); + common_replace.insert(ret_val, lhs_expr); } else { @@ -663,7 +669,9 @@ bool code_contractst::apply_function_contract( ns, symbol_table); symbol_exprt ret_val(CPROVER_PREFIX "return_value", type.return_type()); - common_replace.insert(ret_val, fresh.symbol_expr()); + auto fresh_sym_expr = fresh.symbol_expr(); + common_replace.insert(ret_val, fresh_sym_expr); + call_ret_opt = fresh_sym_expr; } } } @@ -736,8 +744,10 @@ bool code_contractst::apply_function_contract( targets.add_to_operands(std::move(target)); common_replace(targets); - // Create a series of non-deterministic assignments to havoc the variables - // in the assigns clause. + // Create a sequence of non-deterministic assignments... + goto_programt havoc_instructions; + + // ...for assigns clause targets if(!assigns.empty()) { assigns_clauset assigns_clause( @@ -747,14 +757,25 @@ bool code_contractst::apply_function_contract( modifiest modifies; modifies.insert(targets.operands().cbegin(), targets.operands().cend()); - goto_programt assigns_havoc; havoc_assigns_targetst havoc_gen(modifies, ns); - havoc_gen.append_full_havoc_code(location, assigns_havoc); + havoc_gen.append_full_havoc_code(location, havoc_instructions); + } - // Insert the non-deterministic assignment immediately before the call site. - insert_before_swap_and_advance(function_body, target, assigns_havoc); + // ...for the return value + if(call_ret_opt.has_value()) + { + auto &call_ret = call_ret_opt.value(); + auto &loc = call_ret.source_location(); + auto &type = call_ret.type(); + side_effect_expr_nondett expr(type, location); + auto target = havoc_instructions.add( + goto_programt::make_assignment(call_ret, expr, loc)); + target->code_nonconst().add_source_location() = loc; } + // Insert havoc instructions immediately before the call site. + insert_before_swap_and_advance(function_body, target, havoc_instructions); + // To remove the function call, insert statements related to the assumption. // Then, replace the function call with a SKIP statement. if(!ensures.is_false())