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..4e8404eb5e4 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,15 @@ 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); + + goto_programt + make_ensures_assertion_for_call(const code_function_callt &call); + void add_contract_check( const irep_idt &function, goto_programt &dest); @@ -242,6 +262,82 @@ void code_contractst::code_contracts( apply_contract(goto_function.body, it); } +goto_programt code_contractst::make_ensures_assertion_for_call( + const code_function_callt &call) +{ + goto_programt goto_assertion; + + // we don't handle function pointers + if(call.function().id() != ID_symbol) + return goto_assertion; + + 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 goto_assertion; + + // 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); + + code_assertt assertion(ensures); + null_message_handlert message_handler; + // We first need to convert the expression to a goto_program + goto_convert(assertion, symbol_table, goto_assertion, message_handler, ID_C); + + 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( + 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 +468,39 @@ 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); + INVARIANT( + i_it != goto_functions.function_map.end(), + "There must exist an INITIALIZE_FUNCTION"); - // 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..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)(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):"\