From cb581d8c8881c4b5c5d8fc19a9995ca165f5c9bf Mon Sep 17 00:00:00 2001 From: Konstantinos Kallas Date: Wed, 31 Jul 2019 18:16:14 -0400 Subject: [PATCH 1/3] Add an --assert-ensures check that asserts the ensures part of a function's contract --- regression/contracts/assert_ensures_01/main.c | 18 +++ .../contracts/assert_ensures_01/test.desc | 7 + regression/contracts/assert_ensures_02/main.c | 21 +++ .../contracts/assert_ensures_02/test.desc | 7 + src/goto-instrument/code_contracts.cpp | 121 ++++++++++++++++-- src/goto-instrument/code_contracts.h | 5 + .../goto_instrument_parse_options.cpp | 17 +++ .../goto_instrument_parse_options.h | 2 +- 8 files changed, 184 insertions(+), 14 deletions(-) create mode 100644 regression/contracts/assert_ensures_01/main.c create mode 100644 regression/contracts/assert_ensures_01/test.desc create mode 100644 regression/contracts/assert_ensures_02/main.c create mode 100644 regression/contracts/assert_ensures_02/test.desc diff --git a/regression/contracts/assert_ensures_01/main.c b/regression/contracts/assert_ensures_01/main.c new file mode 100644 index 00000000000..bbbd6547b55 --- /dev/null +++ b/regression/contracts/assert_ensures_01/main.c @@ -0,0 +1,18 @@ +// This tests whether the flag --assert-ensures adds the assert of the +// ensures statement after the call + +#include + +int min(int a, int b) __CPROVER_ensures( + __CPROVER_return_value <= a && __CPROVER_return_value <= b && + (__CPROVER_return_value == a || __CPROVER_return_value == b)) +{ + return 100; +} + +int main() +{ + int x, y, z; + z = min(x, y); + return z; +} diff --git a/regression/contracts/assert_ensures_01/test.desc b/regression/contracts/assert_ensures_01/test.desc new file mode 100644 index 00000000000..2844b912707 --- /dev/null +++ b/regression/contracts/assert_ensures_01/test.desc @@ -0,0 +1,7 @@ +CORE +main.c +--assert-ensures min +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- diff --git a/regression/contracts/assert_ensures_02/main.c b/regression/contracts/assert_ensures_02/main.c new file mode 100644 index 00000000000..3aaac0d542c --- /dev/null +++ b/regression/contracts/assert_ensures_02/main.c @@ -0,0 +1,21 @@ +// This tests whether --assert-ensures correctly handles function +// calls in the contract + +#include + +int is_min(int min, int a, int b) +{ + return min <= a && min <= b && (min == a || min == b); +} + +int min(int a, int b) __CPROVER_ensures(is_min(__CPROVER_return_value, a, b)) +{ + return 100; +} + +int main() +{ + int x, y, z; + z = min(x, y); + return z; +} diff --git a/regression/contracts/assert_ensures_02/test.desc b/regression/contracts/assert_ensures_02/test.desc new file mode 100644 index 00000000000..35eb6c49e19 --- /dev/null +++ b/regression/contracts/assert_ensures_02/test.desc @@ -0,0 +1,7 @@ +CORE +main.c +--assert-ensures min +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- \ No newline at end of file diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index dfc5e8fd20e..10d60553aee 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -15,8 +15,10 @@ Date: February 2016 #include #include +#include #include +#include #include #include @@ -30,12 +32,18 @@ class code_contractst public: code_contractst( symbol_tablet &_symbol_table, - goto_functionst &_goto_functions): - ns(_symbol_table), + goto_functionst &_goto_functions, + std::list _functions_to_assert_ensures) + : ns(_symbol_table), symbol_table(_symbol_table), goto_functions(_goto_functions), + functions_to_assert_ensures(_functions_to_assert_ensures), temporary_counter(0) { + if(functions_to_assert_ensures.empty()) + mode_assert_ensures = false; + else + mode_assert_ensures = true; } void operator()(); @@ -44,9 +52,12 @@ class code_contractst namespacet ns; symbol_tablet &symbol_table; goto_functionst &goto_functions; + std::list functions_to_assert_ensures; unsigned temporary_counter; + bool mode_assert_ensures; + std::unordered_set summarized; void code_contracts(goto_functionst::goto_functiont &goto_function); @@ -55,6 +66,12 @@ class code_contractst goto_programt &goto_program, goto_programt::targett target); + void + assert_ensures_after_calls(goto_functionst::goto_functiont &goto_function); + + void + assert_ensures(goto_programt &goto_program, goto_programt::targett target); + void add_contract_check( const irep_idt &function, goto_programt &dest); @@ -242,6 +259,70 @@ void code_contractst::code_contracts( apply_contract(goto_function.body, it); } +void code_contractst::assert_ensures( + goto_programt &goto_program, + goto_programt::targett target) +{ + const code_function_callt &call = target->get_function_call(); + + // we don't handle function pointers + if(call.function().id() != ID_symbol) + return; + + 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); + + exprt ensures = static_cast(type.find(ID_C_spec_ensures)); + + // is there a contract? + if(ensures.is_nil()) + return; + + // replace formal parameters by arguments, replace return + replace_symbolt replace; + + // TODO: return value could be nil + if(type.return_type() != empty_typet()) + { + symbol_exprt ret_val(CPROVER_PREFIX "return_value", call.lhs().type()); + replace.insert(ret_val, call.lhs()); + } + + // formal parameters + 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(); + ++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(ensures); + + // assert the ensures part of the contract after the call + ++target; + code_assertt a(ensures); + goto_programt new_goto_program; + null_message_handlert message_handler; + // We first need to convert the expression to a goto_program + goto_convert(a, symbol_table, new_goto_program, message_handler, ID_C); + + goto_program.insert_before_swap(target, new_goto_program); +} + +void code_contractst::assert_ensures_after_calls( + goto_functionst::goto_functiont &goto_function) +{ + // look at all function calls + Forall_goto_program_instructions(it, goto_function.body) + if(it->is_function_call()) + assert_ensures(goto_function.body, it); +} + const symbolt &code_contractst::new_tmp_symbol( const typet &type, const source_locationt &source_location, @@ -372,23 +453,37 @@ void code_contractst::add_contract_check( void code_contractst::operator()() { - Forall_goto_functions(it, goto_functions) - code_contracts(it->second); - - goto_functionst::function_mapt::iterator i_it= - goto_functions.function_map.find(INITIALIZE_FUNCTION); - assert(i_it!=goto_functions.function_map.end()); + if(mode_assert_ensures) + { + Forall_goto_functions(it, goto_functions) + assert_ensures_after_calls(it->second); + } + else + { + Forall_goto_functions(it, goto_functions) + code_contracts(it->second); - for(const auto &contract : summarized) - add_contract_check(contract, i_it->second.body); + goto_functionst::function_mapt::iterator i_it = + goto_functions.function_map.find(INITIALIZE_FUNCTION); + assert(i_it != goto_functions.function_map.end()); - // remove skips - remove_skip(i_it->second.body); + for(const auto &contract : summarized) + add_contract_check(contract, i_it->second.body); + // remove skips + remove_skip(i_it->second.body); + } goto_functions.update(); } +void assert_ensures(goto_modelt &goto_model, std::list functions) +{ + code_contractst( + goto_model.symbol_table, goto_model.goto_functions, functions)(); +} + void code_contracts(goto_modelt &goto_model) { - code_contractst(goto_model.symbol_table, goto_model.goto_functions)(); + std::list empty; + code_contractst(goto_model.symbol_table, goto_model.goto_functions, empty)(); } diff --git a/src/goto-instrument/code_contracts.h b/src/goto-instrument/code_contracts.h index dc02902c142..9c3e1ca65cf 100644 --- a/src/goto-instrument/code_contracts.h +++ b/src/goto-instrument/code_contracts.h @@ -14,8 +14,13 @@ Date: February 2016 #ifndef CPROVER_GOTO_INSTRUMENT_CODE_CONTRACTS_H #define CPROVER_GOTO_INSTRUMENT_CODE_CONTRACTS_H +#include +#include + class goto_modelt; void code_contracts(goto_modelt &); +void assert_ensures(goto_modelt &goto_model, std::list functions); + #endif // CPROVER_GOTO_INSTRUMENT_CODE_CONTRACTS_H diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 6442032fc38..035d1c1c4cf 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1088,6 +1088,22 @@ void goto_instrument_parse_optionst::instrument_goto_program() code_contracts(goto_model); } + // assert the ensures part of the contract for the given functions + if(cmdline.isset("assert-ensures")) + { + log.status() << "Asserting code contract" << messaget::eom; + std::list functions_to_assert_ensures = + cmdline.get_values("assert-ensures"); + if(functions_to_assert_ensures.empty()) + { + log.error() + << "At least one function name has to be given with --assert-ensures" + << messaget::eom; + throw 0; + } + assert_ensures(goto_model, functions_to_assert_ensures); + } + // replace function pointers, if explicitly requested if(cmdline.isset("remove-function-pointers")) { @@ -1643,6 +1659,7 @@ void goto_instrument_parse_optionst::help() " --nondet-static-exclude e same as nondet-static except for the variable e\n" //NOLINT(*) " (use multiple times if required)\n" " --check-invariant function instruments invariant checking function\n" + " --assert-ensures function checks that function satisfies its contract ensures after each call\n" // NOLINT(*) " --remove-pointers converts pointer arithmetic to base+offset expressions\n" // NOLINT(*) " --splice-call caller,callee prepends a call to callee in the body of caller\n" // NOLINT(*) " --undefined-function-is-assume-false\n" diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 6db5ec4fe57..c88efcb7be2 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -94,7 +94,7 @@ Author: Daniel Kroening, kroening@kroening.com "(interpreter)(show-reaching-definitions)" \ "(list-symbols)(list-undefined-functions)" \ "(z3)(add-library)(show-dependence-graph)" \ - "(horn)(skip-loops):(apply-code-contracts)(model-argc-argv):" \ + "(horn)(skip-loops):(apply-code-contracts)(assert-ensures):(model-argc-argv):" \ "(show-threaded)(list-calls-args)" \ "(undefined-function-is-assume-false)" \ "(remove-function-body):"\ From 497b74003cfd06e1df69da6976179b1c5b4131c8 Mon Sep 17 00:00:00 2001 From: Konstantinos Kallas Date: Thu, 1 Aug 2019 15:56:25 -0400 Subject: [PATCH 2/3] Fix lint errors --- src/goto-instrument/code_contracts.cpp | 4 +++- src/goto-instrument/goto_instrument_parse_options.h | 3 ++- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index 10d60553aee..01e98127c86 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -465,7 +465,9 @@ void code_contractst::operator()() goto_functionst::function_mapt::iterator i_it = goto_functions.function_map.find(INITIALIZE_FUNCTION); - assert(i_it != goto_functions.function_map.end()); + INVARIANT( + i_it != goto_functions.function_map.end(), + "There must exist an INITIALIZE_FUNCTION"); for(const auto &contract : summarized) add_contract_check(contract, i_it->second.body); diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index c88efcb7be2..cf035cadcc5 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -94,7 +94,8 @@ Author: Daniel Kroening, kroening@kroening.com "(interpreter)(show-reaching-definitions)" \ "(list-symbols)(list-undefined-functions)" \ "(z3)(add-library)(show-dependence-graph)" \ - "(horn)(skip-loops):(apply-code-contracts)(assert-ensures):(model-argc-argv):" \ + "(horn)(skip-loops):(apply-code-contracts)" \ + "(assert-ensures):(model-argc-argv):" \ "(show-threaded)(list-calls-args)" \ "(undefined-function-is-assume-false)" \ "(remove-function-body):"\ From 167e36db0c6331bb436887fdd72f8f0975695de9 Mon Sep 17 00:00:00 2001 From: Konstantinos Kallas Date: Wed, 7 Aug 2019 10:43:55 -0400 Subject: [PATCH 3/3] Address style comments --- src/goto-instrument/code_contracts.cpp | 39 ++++++++++++++++++-------- 1 file changed, 27 insertions(+), 12 deletions(-) diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index 01e98127c86..4e8404eb5e4 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -72,6 +72,9 @@ class code_contractst void assert_ensures(goto_programt &goto_program, goto_programt::targett target); + goto_programt + make_ensures_assertion_for_call(const code_function_callt &call); + void add_contract_check( const irep_idt &function, goto_programt &dest); @@ -259,15 +262,14 @@ void code_contractst::code_contracts( apply_contract(goto_function.body, it); } -void code_contractst::assert_ensures( - goto_programt &goto_program, - goto_programt::targett target) +goto_programt code_contractst::make_ensures_assertion_for_call( + const code_function_callt &call) { - const code_function_callt &call = target->get_function_call(); + goto_programt goto_assertion; // we don't handle function pointers if(call.function().id() != ID_symbol) - return; + return goto_assertion; const irep_idt &function = to_symbol_expr(call.function()).get_identifier(); const symbolt &f_sym = ns.lookup(function); @@ -277,7 +279,7 @@ void code_contractst::assert_ensures( // is there a contract? if(ensures.is_nil()) - return; + return goto_assertion; // replace formal parameters by arguments, replace return replace_symbolt replace; @@ -295,23 +297,36 @@ void code_contractst::assert_ensures( 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(ensures); - // assert the ensures part of the contract after the call - ++target; - code_assertt a(ensures); - goto_programt new_goto_program; + code_assertt assertion(ensures); null_message_handlert message_handler; // We first need to convert the expression to a goto_program - goto_convert(a, symbol_table, new_goto_program, message_handler, ID_C); + goto_convert(assertion, symbol_table, goto_assertion, message_handler, ID_C); - goto_program.insert_before_swap(target, new_goto_program); + return goto_assertion; +} + +void code_contractst::assert_ensures( + goto_programt &goto_program, + goto_programt::targett target) +{ + const code_function_callt &call = target->get_function_call(); + + // Create the goto program for the assertion + goto_programt goto_assertion = make_ensures_assertion_for_call(call); + + // assert the ensures part of the contract after the call + ++target; + goto_program.insert_before_swap(target, goto_assertion); } void code_contractst::assert_ensures_after_calls(