From 61b9e655bdac9ef6fb2705ad744265a3385bed5d Mon Sep 17 00:00:00 2001 From: klaas Date: Wed, 23 May 2018 14:55:12 -0400 Subject: [PATCH 01/14] Splits code contracts into check(WIP) and apply The previous implementation of code-contracts has a single flag --apply-code-contracts, which created checks to verify that the contracts are satisfied and also used the contracts to abstract out the portions of code which had contracts provided. This commit splits that process into two parts, one of which only uses the contracts, without checking that they hold (--apply-code-contracts) and the other of which (incomplete as of this commit) both checks and applies, in a similar manner to the existing method. While it is clear that applying contracts without checking them is unsound, it is nevertheless useful in verifying large pieces of software in a modular fashion. If we verify a function to satisfy its specification from an arbitrary environment, then we can avoid needing to check that function again by using --apply-code-contracts. --- .../contracts/function_apply_01/test.desc | 3 +- .../contracts/function_check_04/test.desc | 2 +- regression/contracts/invar_check_01/test.desc | 2 +- regression/contracts/invar_check_02/test.desc | 2 +- regression/contracts/invar_check_03/test.desc | 2 +- regression/contracts/invar_check_04/test.desc | 2 +- src/goto-instrument/code_contracts.cpp | 244 +++++++++++++++--- src/goto-instrument/code_contracts.h | 3 +- .../goto_instrument_parse_options.cpp | 10 +- .../goto_instrument_parse_options.h | 4 +- 10 files changed, 220 insertions(+), 54 deletions(-) diff --git a/regression/contracts/function_apply_01/test.desc b/regression/contracts/function_apply_01/test.desc index abc8686ad8e..4f37c84c808 100644 --- a/regression/contracts/function_apply_01/test.desc +++ b/regression/contracts/function_apply_01/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c --apply-code-contracts ^EXIT=0$ @@ -6,4 +6,3 @@ main.c ^VERIFICATION SUCCESSFUL$ -- -- -Applying code contracts currently also checks them. diff --git a/regression/contracts/function_check_04/test.desc b/regression/contracts/function_check_04/test.desc index db7ee5aa32a..85a0fe836ba 100644 --- a/regression/contracts/function_check_04/test.desc +++ b/regression/contracts/function_check_04/test.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG main.c --apply-code-contracts ^\[main.assertion.1\] assertion x == 0: SUCCESS$ diff --git a/regression/contracts/invar_check_01/test.desc b/regression/contracts/invar_check_01/test.desc index d9a2ec0a8ca..7dafb10d751 100644 --- a/regression/contracts/invar_check_01/test.desc +++ b/regression/contracts/invar_check_01/test.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG main.c --apply-code-contracts ^EXIT=0$ diff --git a/regression/contracts/invar_check_02/test.desc b/regression/contracts/invar_check_02/test.desc index d9a2ec0a8ca..7dafb10d751 100644 --- a/regression/contracts/invar_check_02/test.desc +++ b/regression/contracts/invar_check_02/test.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG main.c --apply-code-contracts ^EXIT=0$ diff --git a/regression/contracts/invar_check_03/test.desc b/regression/contracts/invar_check_03/test.desc index d9a2ec0a8ca..7dafb10d751 100644 --- a/regression/contracts/invar_check_03/test.desc +++ b/regression/contracts/invar_check_03/test.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG main.c --apply-code-contracts ^EXIT=0$ diff --git a/regression/contracts/invar_check_04/test.desc b/regression/contracts/invar_check_04/test.desc index 7414b7f58a6..d2f31f91916 100644 --- a/regression/contracts/invar_check_04/test.desc +++ b/regression/contracts/invar_check_04/test.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG main.c --apply-code-contracts ^\[main.1\] Loop invariant violated before entry: SUCCESS$ diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index 7a8412afcce..22cbad1d54d 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -24,6 +24,8 @@ Date: February 2016 #include "loop_utils.h" +enum class contract_opst { APPLY, CHECK }; + class code_contractst { public: @@ -37,7 +39,7 @@ class code_contractst { } - void operator()(); + void operator()(contract_opst op_type); protected: namespacet ns; @@ -48,12 +50,21 @@ class code_contractst std::unordered_set summarized; + void apply_code_contracts(); + void check_code_contracts(); + void code_contracts(goto_functionst::goto_functiont &goto_function); void apply_contract( goto_programt &goto_program, goto_programt::targett target); + void apply_invariant( + goto_functionst::goto_functiont &goto_function, + const local_may_aliast &local_may_alias, + const goto_programt::targett loop_head, + const loopt &loop); + void add_contract_check( const irep_idt &function, goto_programt &dest); @@ -69,25 +80,28 @@ static void check_apply_invariants( const goto_programt::targett loop_head, const loopt &loop) { - assert(!loop.empty()); + PRECONDITION(!loop.empty()); // find the last back edge goto_programt::targett loop_end=loop_head; - for(loopt::const_iterator - it=loop.begin(); - it!=loop.end(); - ++it) - if((*it)->is_goto() && - (*it)->get_target()==loop_head && - (*it)->location_number>loop_end->location_number) - loop_end=*it; + for(const goto_programt::targett &inst : loop) + { + if(inst->is_goto() && + inst->get_target() == loop_head && + inst->location_number>loop_end->location_number) + { + loop_end = inst; + } + } // see whether we have an invariant exprt invariant= static_cast( loop_end->guard.find(ID_C_spec_loop_invariant)); if(invariant.is_nil()) + { return; + } // change H: loop; E: ... // to @@ -175,14 +189,24 @@ void code_contractst::apply_contract( const symbolt &f_sym=ns.lookup(function); const code_typet &type=to_code_type(f_sym.type); - exprt requires= + exprt requires = static_cast(type.find(ID_C_spec_requires)); - exprt ensures= + exprt ensures = static_cast(type.find(ID_C_spec_ensures)); - // is there a contract? if(ensures.is_nil()) - return; + { + // If there is no contract at all, we skip this function. + if(requires.is_nil()) + { + return; + } + else + { + // If there's no ensures but is a requires, treat it as ensures(true) + ensures = true_exprt(); + } + } // replace formal parameters by arguments, replace return replace_symbolt replace; @@ -215,12 +239,104 @@ void code_contractst::apply_contract( goto_program.insert_before_swap(target, a); ++target; } + // TODO: Havoc write set of the function between assert and ensure. target->make_assumption(ensures); summarized.insert(function); } +void code_contractst::apply_invariant( + goto_functionst::goto_functiont &goto_function, + const local_may_aliast &local_may_alias, + const goto_programt::targett loop_head, + const loopt &loop) +{ + PRECONDITION(!loop.empty()); + + // find the last back edge + goto_programt::targett loop_end=loop_head; + for(const goto_programt::targett &inst : loop) + { + if(inst->is_goto() && + inst->get_target()==loop_head && + inst->location_number>loop_end->location_number) + { + loop_end=inst; + } + } + + exprt invariant = static_cast( + loop_end->guard.find(ID_C_spec_loop_invariant)); + if(invariant.is_nil()) + { + return; + } + + // change H: loop; E: ... + // to + // H: assert(invariant); + // havoc; + // assume(invariant); + // assume(!guard); + // E: ... + + // find out what can get changed in the loop + modifiest modifies; + get_modifies(local_may_alias, loop, modifies); + + // build the havocking code + goto_programt havoc_code; + + // assert the invariant + { + goto_programt::targett a=havoc_code.add_instruction(ASSERT); + a->guard=invariant; + a->function=loop_head->function; + a->source_location=loop_head->source_location; + a->source_location.set_comment("Loop invariant violated before entry"); + } + + // havoc variables being written to + build_havoc_code(loop_head, modifies, havoc_code); + + // assume the invariant + { + goto_programt::targett assume=havoc_code.add_instruction(ASSUME); + assume->guard=invariant; + assume->function=loop_head->function; + assume->source_location=loop_head->source_location; + } + + // assume !guard + // TODO: consider breaks snd how they're implemented. + // TODO: Also consider continues and whether they jump to loop end or head + { + goto_programt::targett assume = havoc_code.add_instruction(ASSUME); + if(loop_head->is_goto()) + { + assume->guard = loop_head->guard; + } + else + { + assume->guard = loop_end->guard; + assume->guard.make_not(); + } + assume->function = loop_head->function; + assume->source_location = loop_head->source_location; + } + + // Clear out loop body + for(const goto_programt::targett &inst : loop) + { + inst->make_skip(); + } + + // Now havoc at the loop head. Use insert_swap to + // preserve jumps to loop head. + goto_function.body.insert_before_swap(loop_head, havoc_code); +} + void code_contractst::code_contracts( goto_functionst::goto_functiont &goto_function) { @@ -228,15 +344,14 @@ void code_contractst::code_contracts( natural_loops_mutablet natural_loops(goto_function.body); // iterate over the (natural) loops in the function - for(natural_loops_mutablet::loop_mapt::const_iterator - l_it=natural_loops.loop_map.begin(); - l_it!=natural_loops.loop_map.end(); - l_it++) + for(const auto &l_it : natural_loops.loop_map) + { check_apply_invariants( goto_function, local_may_alias, - l_it->first, - l_it->second); + l_it.first, + l_it.second); + } // look at all function calls Forall_goto_program_instructions(it, goto_function.body) @@ -253,7 +368,7 @@ const symbolt &code_contractst::new_tmp_symbol( id2string(source_location.get_function()), "tmp_cc", source_location, - irep_idt(), + ID_C, symbol_table); } @@ -261,7 +376,7 @@ void code_contractst::add_contract_check( const irep_idt &function, goto_programt &dest) { - assert(!dest.instructions.empty()); + PRECONDITION(!dest.instructions.empty()); goto_functionst::function_mapt::iterator f_it= goto_functions.function_map.find(function); @@ -269,10 +384,8 @@ void code_contractst::add_contract_check( const goto_functionst::goto_functiont &gf=f_it->second; - const exprt &requires= - static_cast(gf.type.find(ID_C_spec_requires)); - const exprt &ensures= - static_cast(gf.type.find(ID_C_spec_ensures)); + exprt requires = static_cast(gf.type.find(ID_C_spec_requires)); + exprt ensures = static_cast(gf.type.find(ID_C_spec_ensures)); assert(ensures.is_not_nil()); // build: @@ -323,26 +436,27 @@ void code_contractst::add_contract_check( } // decl parameter1 ... - for(code_typet::parameterst::const_iterator - p_it=gf.type.parameters().begin(); - p_it!=gf.type.parameters().end(); - ++p_it) + for(const auto &p_it : gf.type.parameters()) { goto_programt::targett d=check.add_instruction(DECL); d->function=skip->function; d->source_location=skip->source_location; symbol_exprt p= - new_tmp_symbol(p_it->type(), + new_tmp_symbol(p_it.type(), d->source_location).symbol_expr(); d->code=code_declt(p); call.arguments().push_back(p); - if(!p_it->get_identifier().empty()) - replace.insert(p_it->get_identifier(), p); + if(!p_it.get_identifier().empty()) + replace.insert(p_it.get_identifier(), p); } + // rewrite any use of parameters + replace(requires); + replace(ensures); + // assume(requires) if(requires.is_not_nil()) { @@ -350,9 +464,6 @@ void code_contractst::add_contract_check( a->make_assumption(requires); a->function=skip->function; a->source_location=requires.source_location(); - - // rewrite any use of parameters - replace(a->guard); } // ret=function(parameter1, ...) @@ -367,9 +478,6 @@ void code_contractst::add_contract_check( a->function=skip->function; a->source_location=ensures.source_location(); - // rewrite any use of __CPROVER_return_value - replace(a->guard); - // assume(false) goto_programt::targett af=check.add_instruction(); af->make_assumption(false_exprt()); @@ -381,10 +489,42 @@ void code_contractst::add_contract_check( dest.destructive_insert(dest.instructions.begin(), check); } -void code_contractst::operator()() +void code_contractst::apply_code_contracts() +{ + Forall_goto_functions(it, goto_functions) + { + goto_functionst::goto_functiont &goto_function = it->second; + + // TODO: This aliasing check is insufficiently strong, in general. + local_may_aliast local_may_alias(goto_function); + natural_loops_mutablet natural_loops(goto_function.body); + + for(const auto &l_it : natural_loops.loop_map) + { + apply_invariant(goto_function, + local_may_alias, + l_it.first, + l_it.second); + } + + Forall_goto_program_instructions(it, goto_function.body) + { + if(it->is_function_call()) + { + apply_contract(goto_function.body, it); + } + } + } + + goto_functions.update(); +} + +void code_contractst::check_code_contracts() { Forall_goto_functions(it, goto_functions) + { code_contracts(it->second); + } goto_functionst::function_mapt::iterator i_it= goto_functions.function_map.find(INITIALIZE_FUNCTION); @@ -399,7 +539,27 @@ void code_contractst::operator()() goto_functions.update(); } -void code_contracts(goto_modelt &goto_model) +void code_contractst::operator()(contract_opst op_type) +{ + switch(op_type) + { + case contract_opst::APPLY: + apply_code_contracts(); + break; + case contract_opst::CHECK: + check_code_contracts(); + break; + } +} + +void check_code_contracts(goto_modelt &goto_model) +{ + code_contractst(goto_model.symbol_table, goto_model.goto_functions) + (contract_opst::CHECK); +} + +void apply_code_contracts(goto_modelt &goto_model) { - code_contractst(goto_model.symbol_table, goto_model.goto_functions)(); + code_contractst(goto_model.symbol_table, goto_model.goto_functions) + (contract_opst::APPLY); } diff --git a/src/goto-instrument/code_contracts.h b/src/goto-instrument/code_contracts.h index dc02902c142..7c7c02c09c0 100644 --- a/src/goto-instrument/code_contracts.h +++ b/src/goto-instrument/code_contracts.h @@ -16,6 +16,7 @@ Date: February 2016 class goto_modelt; -void code_contracts(goto_modelt &); +void apply_code_contracts(goto_modelt &); +void check_code_contracts(goto_modelt &); #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 4582509df7d..a0b8c41c28b 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1046,11 +1046,17 @@ void goto_instrument_parse_optionst::instrument_goto_program() goto_model.goto_functions.update(); } - // verify and set invariants and pre/post-condition pairs if(cmdline.isset("apply-code-contracts")) { status() << "Applying Code Contracts" << eom; - code_contracts(goto_model); + apply_code_contracts(goto_model); + } + + // verify and set invariants and pre/post-condition pairs + if(cmdline.isset("check-code-contracts")) + { + status() << "Checking Code Contracts" << eom; + check_code_contracts(goto_model); } // replace function pointers, if explicitly requested diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 706083df63e..d8286c53c74 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -87,8 +87,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):" \ - "(show-threaded)(list-calls-args)" \ + "(horn)(skip-loops):(apply-code-contracts)(check-code-contracts)" \ + "(model-argc-argv):(show-threaded)(list-calls-args)" \ "(undefined-function-is-assume-false)" \ "(remove-function-body):"\ OPT_AGGRESSIVE_SLICER \ From e15b47903d1a14f96affa47148b3d2d82a70ffff Mon Sep 17 00:00:00 2001 From: klaas Date: Fri, 25 May 2018 15:33:37 -0400 Subject: [PATCH 02/14] Reworks checking of code contracts This commit completes the work started in the previous commit by revising the existing contract-handling code into the new pass --check-code-contracts, which first applies all contracts and then checks them. By applying the contracts before checking begins, this checks the relative correctness of each function/loop with respect to the functions called by/loops contained in it. Since there can be no infinite sequence of nested functions/loops, these relative correctness results together imply the correctness of the overall program. We take this approach rather than checking entirely without using contracts because it allows significant reuse of results --- a function that is called many times only needs to be checked once, and all of its invocations will be abstracted out by the contract application. --- .../contracts/function_check_01/test.desc | 5 +- .../contracts/function_check_04/test.desc | 7 +- .../contracts/function_check_mem_01/main.c | 2 +- .../contracts/function_check_mem_01/test.desc | 2 +- regression/contracts/invar_check_01/test.desc | 7 +- regression/contracts/invar_check_02/test.desc | 7 +- regression/contracts/invar_check_03/test.desc | 7 +- regression/contracts/invar_check_04/test.desc | 7 +- src/goto-instrument/code_contracts.cpp | 354 ++++++++++++++++-- .../goto_instrument_parse_options.cpp | 3 +- src/goto-instrument/loop_utils.cpp | 39 ++ src/goto-instrument/loop_utils.h | 6 + 12 files changed, 379 insertions(+), 67 deletions(-) diff --git a/regression/contracts/function_check_01/test.desc b/regression/contracts/function_check_01/test.desc index d9a2ec0a8ca..a44b7e292f5 100644 --- a/regression/contracts/function_check_01/test.desc +++ b/regression/contracts/function_check_01/test.desc @@ -1,11 +1,8 @@ CORE main.c ---apply-code-contracts +--check-code-contracts ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- -- ---check-code-contracts not implemented yet. ---apply-code-contracts is the current name for the flag. This should be -updated as the flag changes. diff --git a/regression/contracts/function_check_04/test.desc b/regression/contracts/function_check_04/test.desc index 85a0fe836ba..1a229ae78d6 100644 --- a/regression/contracts/function_check_04/test.desc +++ b/regression/contracts/function_check_04/test.desc @@ -1,11 +1,8 @@ -KNOWNBUG +CORE main.c ---apply-code-contracts +--check-code-contracts ^\[main.assertion.1\] assertion x == 0: SUCCESS$ ^\[foo.1\] : FAILURE$ ^VERIFICATION FAILED$ -- -- ---check-code-contracts not implemented yet. ---apply-code-contracts is the current name for the flag. This should be -updated as the flag changes. diff --git a/regression/contracts/function_check_mem_01/main.c b/regression/contracts/function_check_mem_01/main.c index b63364f4d57..10d79cf8190 100644 --- a/regression/contracts/function_check_mem_01/main.c +++ b/regression/contracts/function_check_mem_01/main.c @@ -33,7 +33,7 @@ void foo(bar *x) __CPROVER_requires(__CPROVER_VALID_MEM(x, sizeof(bar))) { x->x += 1; - return + return; } int main() diff --git a/regression/contracts/function_check_mem_01/test.desc b/regression/contracts/function_check_mem_01/test.desc index b46799f781b..c45406ad744 100644 --- a/regression/contracts/function_check_mem_01/test.desc +++ b/regression/contracts/function_check_mem_01/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c --check-code-contracts ^EXIT=0$ diff --git a/regression/contracts/invar_check_01/test.desc b/regression/contracts/invar_check_01/test.desc index 7dafb10d751..a44b7e292f5 100644 --- a/regression/contracts/invar_check_01/test.desc +++ b/regression/contracts/invar_check_01/test.desc @@ -1,11 +1,8 @@ -KNOWNBUG +CORE main.c ---apply-code-contracts +--check-code-contracts ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- -- ---check-code-contracts not implemented yet. ---apply-code-contracts is the current name for the flag. This should be -updated as the flag changes. diff --git a/regression/contracts/invar_check_02/test.desc b/regression/contracts/invar_check_02/test.desc index 7dafb10d751..a44b7e292f5 100644 --- a/regression/contracts/invar_check_02/test.desc +++ b/regression/contracts/invar_check_02/test.desc @@ -1,11 +1,8 @@ -KNOWNBUG +CORE main.c ---apply-code-contracts +--check-code-contracts ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- -- ---check-code-contracts not implemented yet. ---apply-code-contracts is the current name for the flag. This should be -updated as the flag changes. diff --git a/regression/contracts/invar_check_03/test.desc b/regression/contracts/invar_check_03/test.desc index 7dafb10d751..a44b7e292f5 100644 --- a/regression/contracts/invar_check_03/test.desc +++ b/regression/contracts/invar_check_03/test.desc @@ -1,11 +1,8 @@ -KNOWNBUG +CORE main.c ---apply-code-contracts +--check-code-contracts ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ -- -- ---check-code-contracts not implemented yet. ---apply-code-contracts is the current name for the flag. This should be -updated as the flag changes. diff --git a/regression/contracts/invar_check_04/test.desc b/regression/contracts/invar_check_04/test.desc index d2f31f91916..f24cdd9f7e4 100644 --- a/regression/contracts/invar_check_04/test.desc +++ b/regression/contracts/invar_check_04/test.desc @@ -1,12 +1,9 @@ -KNOWNBUG +CORE main.c ---apply-code-contracts +--check-code-contracts ^\[main.1\] Loop invariant violated before entry: SUCCESS$ ^\[main.2\] Loop invariant not preserved: SUCCESS$ ^\[main.assertion.1\] assertion r == 0: FAILURE$ ^VERIFICATION FAILED$ -- -- ---check-code-contracts not implemented yet. ---apply-code-contracts is the current name for the flag. This should be -updated as the flag changes. diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index 22cbad1d54d..3d2087dafd0 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -65,6 +65,17 @@ class code_contractst const goto_programt::targett loop_head, const loopt &loop); + void check_contract( + const irep_idt &function_id, + goto_functionst::goto_functiont &goto_function, + goto_programt &dest); + + void check_apply_invariant( + goto_functionst::goto_functiont &goto_function, + const local_may_aliast &local_may_alias, + const goto_programt::targett loop_head, + const loopt &loop); + void add_contract_check( const irep_idt &function, goto_programt &dest); @@ -106,73 +117,117 @@ static void check_apply_invariants( // change H: loop; E: ... // to // H: assert(invariant); - // havoc; + // if(nondet) goto E: + // havoc reads and writes of loop; // assume(invariant); - // if(guard) goto E: + // assume(guard) [only for for/while loops] // loop; // assert(invariant); // assume(false); - // E: ... + // E: havoc writes of loop; + // assume(invariant) + // assume(!guard) + // ... // find out what can get changed in the loop modifiest modifies; get_modifies(local_may_alias, loop, modifies); + // find out what is used by the loop + usest uses; + get_uses(local_may_alias, loop, uses); + // build the havocking code - goto_programt havoc_code; + goto_programt havoc_all_code; + goto_programt havoc_writes_code; // assert the invariant { - goto_programt::targett a=havoc_code.add_instruction(ASSERT); + goto_programt::targett a=havoc_all_code.add_instruction(ASSERT); a->guard=invariant; a->function=loop_head->function; a->source_location=loop_head->source_location; a->source_location.set_comment("Loop invariant violated before entry"); } + // nondeterministically skip the loop + { + goto_programt::targett jump=havoc_all_code.add_instruction(GOTO); + jump->guard=side_effect_expr_nondett(bool_typet()); + jump->targets.push_back(loop_end); + jump->function=loop_head->function; + jump->source_location=loop_head->source_location; + } + // havoc variables being written to - build_havoc_code(loop_head, modifies, havoc_code); + build_havoc_code(loop_head, uses, havoc_all_code); // assume the invariant { - goto_programt::targett assume=havoc_code.add_instruction(ASSUME); + goto_programt::targett assume=havoc_all_code.add_instruction(ASSUME); assume->guard=invariant; assume->function=loop_head->function; assume->source_location=loop_head->source_location; } - // non-deterministically skip the loop if it is a do-while loop - if(!loop_head->is_goto()) + // assert the invariant at the end of the loop body { - goto_programt::targett jump=havoc_code.add_instruction(GOTO); - jump->guard = - side_effect_expr_nondett(bool_typet(), loop_head->source_location); - jump->targets.push_back(loop_end); - jump->function=loop_head->function; + goto_programt::targett a = goto_function.body.insert_before(loop_end); + a->type=ASSERT; + a->guard=invariant; + a->function=loop_end->function; + a->source_location=loop_end->source_location; + a->source_location.set_comment("Loop invariant not preserved"); } - // Now havoc at the loop head. Use insert_swap to - // preserve jumps to loop head. - goto_function.body.insert_before_swap(loop_head, havoc_code); + // assume false at the end of the loop to discharge the havocking + { + goto_programt::targett assume = goto_function.body.insert_before(loop_end); + assume->type=ASSUME; + assume->guard.make_false(); + assume->function=loop_end->function; + assume->source_location=loop_end->source_location; + } - // assert the invariant at the end of the loop body + build_havoc_code(loop_end, modifies, havoc_writes_code); + + // Assume the invariant (now after the loop) { - goto_programt::instructiont a(ASSERT); - a.guard=invariant; - a.function=loop_end->function; - a.source_location=loop_end->source_location; - a.source_location.set_comment("Loop invariant not preserved"); - goto_function.body.insert_before_swap(loop_end, a); - ++loop_end; + goto_programt::targett assume=havoc_writes_code.add_instruction(ASSUME); + assume->guard=invariant; + assume->function=loop_head->function; + assume->source_location=loop_head->source_location; } - // change the back edge into assume(false) or assume(guard) + // change the back edge into assume(!guard) loop_end->targets.clear(); loop_end->type=ASSUME; if(loop_head->is_goto()) - loop_end->guard.make_false(); + { + loop_end->guard = loop_head->guard; + } else + { loop_end->guard.make_not(); + } + + // Change the loop head to assume the guard if a for/while loop. + // This needs to be done after we case on what loop_head is in the previous + // section of setup. + if(loop_head->is_goto()) + { + exprt guard = loop_head->guard; + guard.make_not(); + loop_head->make_assumption(guard); + } + + // Now havoc at the loop head. Use insert_swap to + // preserve jumps to loop head. + goto_function.body.insert_before_swap(loop_head, havoc_all_code); + + // Now havoc at the loop end. Use insert_swap to + // preserve jumps to loop end. + goto_function.body.insert_before_swap(loop_end, havoc_writes_code); } void code_contractst::apply_contract( @@ -273,6 +328,8 @@ void code_contractst::apply_invariant( return; } + // TODO: Allow for not havocking in the for/while case + // change H: loop; E: ... // to // H: assert(invariant); @@ -309,7 +366,7 @@ void code_contractst::apply_invariant( } // assume !guard - // TODO: consider breaks snd how they're implemented. + // TODO: consider breaks and how they're implemented. // TODO: Also consider continues and whether they jump to loop end or head { goto_programt::targett assume = havoc_code.add_instruction(ASSUME); @@ -335,6 +392,211 @@ void code_contractst::apply_invariant( // Now havoc at the loop head. Use insert_swap to // preserve jumps to loop head. goto_function.body.insert_before_swap(loop_head, havoc_code); + + // Remove all the skips we created. + remove_skip(goto_function.body); +} + +void code_contractst::check_contract( + const irep_idt &function_id, + goto_functionst::goto_functiont &goto_function, + goto_programt &dest) +{ + PRECONDITION(!dest.instructions.empty()); + + exprt requires = + static_cast(goto_function.type.find(ID_C_spec_requires)); + exprt ensures = + static_cast(goto_function.type.find(ID_C_spec_ensures)); + + // Nothing to check if ensures is nil. + if(ensures.is_nil()) { + return; + } + + // build: + // if(nondet) + // decl ret + // decl parameter1 ... + // assume(requires) [optional] + // ret = function(parameter1, ...) + // assert(ensures) + + // build skip so that if(nondet) can refer to it + goto_programt tmp_skip; + goto_programt::targett skip=tmp_skip.add_instruction(SKIP); + skip->function=dest.instructions.front().function; + skip->source_location=ensures.source_location(); + + goto_programt check; + + // if(nondet) + goto_programt::targett g=check.add_instruction(); + g->make_goto(skip, side_effect_expr_nondett(bool_typet())); + g->function=skip->function; + g->source_location=skip->source_location; + + // prepare function call including all declarations + code_function_callt call; + call.function()=ns.lookup(function_id).symbol_expr(); + replace_symbolt replace; + + // decl ret + // TODO: Handle void functions + // void functions seem to be handled by goto-cc + if(goto_function.type.return_type()!=empty_typet()) + { + goto_programt::targett d=check.add_instruction(DECL); + d->function=skip->function; + d->source_location=skip->source_location; + + symbol_exprt r= + new_tmp_symbol(goto_function.type.return_type(), + d->source_location).symbol_expr(); + d->code=code_declt(r); + + call.lhs()=r; + + replace.insert("__CPROVER_return_value", r); + } + + // decl parameter1 ... + for(const auto &p_it : goto_function.type.parameters()) + { + goto_programt::targett d=check.add_instruction(DECL); + d->function=skip->function; + d->source_location=skip->source_location; + + symbol_exprt p= + new_tmp_symbol(p_it.type(), d->source_location).symbol_expr(); + d->code=code_declt(p); + + call.arguments().push_back(p); + + if(!p_it.get_identifier().empty()) + replace.insert(p_it.get_identifier(), p); + } + + // assume(requires) + if(requires.is_not_nil()) + { + goto_programt::targett a=check.add_instruction(); + a->make_assumption(requires); + a->function=skip->function; + a->source_location=requires.source_location(); + + // rewrite any use of parameters + replace(a->guard); + } + + // ret=function(parameter1, ...) + goto_programt::targett f=check.add_instruction(); + f->make_function_call(call); + f->function=skip->function; + f->source_location=skip->source_location; + + // assert(ensures) + goto_programt::targett a=check.add_instruction(); + a->make_assertion(ensures); + a->function=skip->function; + a->source_location=ensures.source_location(); + + // rewrite any use of __CPROVER_return_value + replace(a->guard); + + // prepend the new code to dest + check.destructive_append(tmp_skip); + dest.destructive_insert(dest.instructions.begin(), check); +} + +void code_contractst::check_apply_invariant( + goto_functionst::goto_functiont &goto_function, + const local_may_aliast &local_may_alias, + const goto_programt::targett loop_head, + const loopt &loop) +{ + PRECONDITION(!loop.empty()); + + // find the last back edge + goto_programt::targett loop_end=loop_head; + for(const goto_programt::targett &inst : loop) + if(inst->is_goto() && + inst->get_target()==loop_head && + inst->location_number>loop_end->location_number) + loop_end=inst; + + // see whether we have an invariant + exprt invariant= + static_cast( + loop_end->guard.find(ID_C_spec_loop_invariant)); + if(invariant.is_nil()) + return; + + // change H: loop; E: ... + // to + // H: assert(invariant); + // havoc writes of loop; + // assume(invariant); + // loop (minus the ending goto); + // assert(invariant); + // assume(!guard) + // E: + // ... + + // find out what can get changed in the loop + modifiest modifies; + get_modifies(local_may_alias, loop, modifies); + + // build the havocking code + goto_programt havoc_code; + + // assert the invariant + { + goto_programt::targett a=havoc_code.add_instruction(ASSERT); + a->guard=invariant; + a->function=loop_head->function; + a->source_location=loop_head->source_location; + a->source_location.set_comment("Loop invariant violated before entry"); + } + + // havoc variables being written to + build_havoc_code(loop_head, modifies, havoc_code); + + // assume the invariant + { + goto_programt::targett assume=havoc_code.add_instruction(ASSUME); + assume->guard=invariant; + assume->function=loop_head->function; + assume->source_location=loop_head->source_location; + } + + // assert the invariant at the end of the loop body + { + goto_programt::instructiont a(ASSERT); + a.guard=invariant; + a.function=loop_end->function; + a.source_location=loop_end->source_location; + a.source_location.set_comment("Loop invariant not preserved"); + + goto_function.body.insert_before_swap(loop_end, a); + ++loop_end; + } + + // change the back edge into assume(!guard) + loop_end->targets.clear(); + loop_end->type=ASSUME; + if(loop_head->is_goto()) + { + loop_end->guard = loop_head->guard; + } + else + { + loop_end->guard.make_not(); + } + + // Now havoc at the loop head. Use insert_swap to + // preserve jumps to loop head. + goto_function.body.insert_before_swap(loop_head, havoc_code); } void code_contractst::code_contracts( @@ -521,17 +783,39 @@ void code_contractst::apply_code_contracts() void code_contractst::check_code_contracts() { + goto_functionst::function_mapt::iterator i_it= + goto_functions.function_map.find(INITIALIZE_FUNCTION); + CHECK_RETURN(i_it!=goto_functions.function_map.end()); + Forall_goto_functions(it, goto_functions) { - code_contracts(it->second); - } + goto_functionst::goto_functiont &goto_function = it->second; - goto_functionst::function_mapt::iterator i_it= - goto_functions.function_map.find(INITIALIZE_FUNCTION); - assert(i_it!=goto_functions.function_map.end()); + // TODO: This aliasing check is insufficiently strong, in general. + local_may_aliast local_may_alias(goto_function); + natural_loops_mutablet natural_loops(goto_function.body); - for(const auto &contract : summarized) - add_contract_check(contract, i_it->second.body); + for(const auto &l_it : natural_loops.loop_map) + { + check_apply_invariant(goto_function, + local_may_alias, + l_it.first, + l_it.second); + } + + Forall_goto_program_instructions(it, goto_function.body) + { + if(it->is_function_call()) + { + apply_contract(goto_function.body, it); + } + } + } + + Forall_goto_functions(it, goto_functions) + { + check_contract(it->first, it->second, i_it->second.body); + } // remove skips remove_skip(i_it->second.body); diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index a0b8c41c28b..6f629b46463 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1046,13 +1046,14 @@ void goto_instrument_parse_optionst::instrument_goto_program() goto_model.goto_functions.update(); } + // Uses (without checking) invariants and pre/post-condition pairs. if(cmdline.isset("apply-code-contracts")) { status() << "Applying Code Contracts" << eom; apply_code_contracts(goto_model); } - // verify and set invariants and pre/post-condition pairs + // Uses invariants and pre/post-condition pairs and verifies that they hold. if(cmdline.isset("check-code-contracts")) { status() << "Checking Code Contracts" << eom; diff --git a/src/goto-instrument/loop_utils.cpp b/src/goto-instrument/loop_utils.cpp index 4ab59238bc9..9d8c9a51c8b 100644 --- a/src/goto-instrument/loop_utils.cpp +++ b/src/goto-instrument/loop_utils.cpp @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "loop_utils.h" #include +#include #include #include @@ -108,3 +109,41 @@ void get_modifies( } } } + +// TODO handle aliasing at all +void get_uses( + const local_may_aliast &local_may_alias, + const loopt &loop, + usest &uses) +{ + for(loopt::const_iterator + i_it=loop.begin(); i_it!=loop.end(); i_it++) + { + const goto_programt::instructiont &instruction=**i_it; + if(instruction.code.is_not_nil()) + { + for(const_depth_iteratort it=instruction.code.depth_begin(); + it!=instruction.code.depth_end(); + ++it) + { + if((*it).id()==ID_symbol) + { + uses.insert(*it); + } + } + } + + if(instruction.guard.is_not_nil()) + { + for(const_depth_iteratort it=instruction.guard.depth_begin(); + it!=instruction.guard.depth_end(); + ++it) + { + if((*it).id()==ID_symbol) + { + uses.insert(*it); + } + } + } + } +} diff --git a/src/goto-instrument/loop_utils.h b/src/goto-instrument/loop_utils.h index 57407ecec1b..1296374eff7 100644 --- a/src/goto-instrument/loop_utils.h +++ b/src/goto-instrument/loop_utils.h @@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com class local_may_aliast; typedef std::set modifiest; +typedef std::set usest; typedef const natural_loops_mutablet::natural_loopt loopt; void get_modifies( @@ -24,6 +25,11 @@ void get_modifies( const loopt &loop, modifiest &modifies); +void get_uses( + const local_may_aliast &local_may_alias, + const loopt &loop, + usest &uses); + void build_havoc_code( const goto_programt::targett loop_head, const modifiest &modifies, From 679e219c373065756a12bd5a7ad25f2c4635eaaa Mon Sep 17 00:00:00 2001 From: klaas Date: Wed, 1 Aug 2018 16:35:35 -0400 Subject: [PATCH 03/14] Removes some dead code. Several functions from the old implementation of code-contracts that were made dead by the previous commits are removed by this commit. Additionally, some variables which were formerly in use are no longer needed, and so are removed. --- src/goto-instrument/code_contracts.cpp | 298 +------------------------ src/goto-instrument/loop_utils.cpp | 39 ---- src/goto-instrument/loop_utils.h | 6 - 3 files changed, 1 insertion(+), 342 deletions(-) diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index 3d2087dafd0..f4bae2406bd 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -34,8 +34,7 @@ class code_contractst goto_functionst &_goto_functions): ns(_symbol_table), symbol_table(_symbol_table), - goto_functions(_goto_functions), - temporary_counter(0) + goto_functions(_goto_functions) { } @@ -46,10 +45,6 @@ class code_contractst symbol_tablet &symbol_table; goto_functionst &goto_functions; - unsigned temporary_counter; - - std::unordered_set summarized; - void apply_code_contracts(); void check_code_contracts(); @@ -76,160 +71,11 @@ class code_contractst const goto_programt::targett loop_head, const loopt &loop); - void add_contract_check( - const irep_idt &function, - goto_programt &dest); - const symbolt &new_tmp_symbol( const typet &type, const source_locationt &source_location); }; -static void check_apply_invariants( - goto_functionst::goto_functiont &goto_function, - const local_may_aliast &local_may_alias, - const goto_programt::targett loop_head, - const loopt &loop) -{ - PRECONDITION(!loop.empty()); - - // find the last back edge - goto_programt::targett loop_end=loop_head; - for(const goto_programt::targett &inst : loop) - { - if(inst->is_goto() && - inst->get_target() == loop_head && - inst->location_number>loop_end->location_number) - { - loop_end = inst; - } - } - - // see whether we have an invariant - exprt invariant= - static_cast( - loop_end->guard.find(ID_C_spec_loop_invariant)); - if(invariant.is_nil()) - { - return; - } - - // change H: loop; E: ... - // to - // H: assert(invariant); - // if(nondet) goto E: - // havoc reads and writes of loop; - // assume(invariant); - // assume(guard) [only for for/while loops] - // loop; - // assert(invariant); - // assume(false); - // E: havoc writes of loop; - // assume(invariant) - // assume(!guard) - // ... - - // find out what can get changed in the loop - modifiest modifies; - get_modifies(local_may_alias, loop, modifies); - - // find out what is used by the loop - usest uses; - get_uses(local_may_alias, loop, uses); - - // build the havocking code - goto_programt havoc_all_code; - goto_programt havoc_writes_code; - - // assert the invariant - { - goto_programt::targett a=havoc_all_code.add_instruction(ASSERT); - a->guard=invariant; - a->function=loop_head->function; - a->source_location=loop_head->source_location; - a->source_location.set_comment("Loop invariant violated before entry"); - } - - // nondeterministically skip the loop - { - goto_programt::targett jump=havoc_all_code.add_instruction(GOTO); - jump->guard=side_effect_expr_nondett(bool_typet()); - jump->targets.push_back(loop_end); - jump->function=loop_head->function; - jump->source_location=loop_head->source_location; - } - - // havoc variables being written to - build_havoc_code(loop_head, uses, havoc_all_code); - - // assume the invariant - { - goto_programt::targett assume=havoc_all_code.add_instruction(ASSUME); - assume->guard=invariant; - assume->function=loop_head->function; - assume->source_location=loop_head->source_location; - } - - // assert the invariant at the end of the loop body - { - goto_programt::targett a = goto_function.body.insert_before(loop_end); - a->type=ASSERT; - a->guard=invariant; - a->function=loop_end->function; - a->source_location=loop_end->source_location; - a->source_location.set_comment("Loop invariant not preserved"); - } - - // assume false at the end of the loop to discharge the havocking - { - goto_programt::targett assume = goto_function.body.insert_before(loop_end); - assume->type=ASSUME; - assume->guard.make_false(); - assume->function=loop_end->function; - assume->source_location=loop_end->source_location; - } - - build_havoc_code(loop_end, modifies, havoc_writes_code); - - // Assume the invariant (now after the loop) - { - goto_programt::targett assume=havoc_writes_code.add_instruction(ASSUME); - assume->guard=invariant; - assume->function=loop_head->function; - assume->source_location=loop_head->source_location; - } - - // change the back edge into assume(!guard) - loop_end->targets.clear(); - loop_end->type=ASSUME; - if(loop_head->is_goto()) - { - loop_end->guard = loop_head->guard; - } - else - { - loop_end->guard.make_not(); - } - - // Change the loop head to assume the guard if a for/while loop. - // This needs to be done after we case on what loop_head is in the previous - // section of setup. - if(loop_head->is_goto()) - { - exprt guard = loop_head->guard; - guard.make_not(); - loop_head->make_assumption(guard); - } - - // Now havoc at the loop head. Use insert_swap to - // preserve jumps to loop head. - goto_function.body.insert_before_swap(loop_head, havoc_all_code); - - // Now havoc at the loop end. Use insert_swap to - // preserve jumps to loop end. - goto_function.body.insert_before_swap(loop_end, havoc_writes_code); -} - void code_contractst::apply_contract( goto_programt &goto_program, goto_programt::targett target) @@ -297,8 +143,6 @@ void code_contractst::apply_contract( // TODO: Havoc write set of the function between assert and ensure. target->make_assumption(ensures); - - summarized.insert(function); } void code_contractst::apply_invariant( @@ -599,28 +443,6 @@ void code_contractst::check_apply_invariant( goto_function.body.insert_before_swap(loop_head, havoc_code); } -void code_contractst::code_contracts( - goto_functionst::goto_functiont &goto_function) -{ - local_may_aliast local_may_alias(goto_function); - natural_loops_mutablet natural_loops(goto_function.body); - - // iterate over the (natural) loops in the function - for(const auto &l_it : natural_loops.loop_map) - { - check_apply_invariants( - goto_function, - local_may_alias, - l_it.first, - l_it.second); - } - - // look at all function calls - Forall_goto_program_instructions(it, goto_function.body) - if(it->is_function_call()) - apply_contract(goto_function.body, it); -} - const symbolt &code_contractst::new_tmp_symbol( const typet &type, const source_locationt &source_location) @@ -634,124 +456,6 @@ const symbolt &code_contractst::new_tmp_symbol( symbol_table); } -void code_contractst::add_contract_check( - const irep_idt &function, - goto_programt &dest) -{ - PRECONDITION(!dest.instructions.empty()); - - goto_functionst::function_mapt::iterator f_it= - goto_functions.function_map.find(function); - assert(f_it!=goto_functions.function_map.end()); - - const goto_functionst::goto_functiont &gf=f_it->second; - - exprt requires = static_cast(gf.type.find(ID_C_spec_requires)); - exprt ensures = static_cast(gf.type.find(ID_C_spec_ensures)); - assert(ensures.is_not_nil()); - - // build: - // if(nondet) - // decl ret - // decl parameter1 ... - // assume(requires) [optional] - // ret=function(parameter1, ...) - // assert(ensures) - // assume(false) - // skip: ... - - // build skip so that if(nondet) can refer to it - goto_programt tmp_skip; - goto_programt::targett skip=tmp_skip.add_instruction(SKIP); - skip->function=dest.instructions.front().function; - skip->source_location=ensures.source_location(); - - goto_programt check; - - // if(nondet) - goto_programt::targett g=check.add_instruction(); - g->make_goto( - skip, side_effect_expr_nondett(bool_typet(), skip->source_location)); - g->function=skip->function; - g->source_location=skip->source_location; - - // prepare function call including all declarations - code_function_callt call; - call.function()=ns.lookup(function).symbol_expr(); - replace_symbolt replace; - - // decl ret - if(gf.type.return_type()!=empty_typet()) - { - goto_programt::targett d=check.add_instruction(DECL); - d->function=skip->function; - d->source_location=skip->source_location; - - symbol_exprt r= - new_tmp_symbol(gf.type.return_type(), - d->source_location).symbol_expr(); - d->code=code_declt(r); - - call.lhs()=r; - - replace.insert("__CPROVER_return_value", r); - } - - // decl parameter1 ... - for(const auto &p_it : gf.type.parameters()) - { - goto_programt::targett d=check.add_instruction(DECL); - d->function=skip->function; - d->source_location=skip->source_location; - - symbol_exprt p= - new_tmp_symbol(p_it.type(), - d->source_location).symbol_expr(); - d->code=code_declt(p); - - call.arguments().push_back(p); - - if(!p_it.get_identifier().empty()) - replace.insert(p_it.get_identifier(), p); - } - - // rewrite any use of parameters - replace(requires); - replace(ensures); - - // assume(requires) - if(requires.is_not_nil()) - { - goto_programt::targett a=check.add_instruction(); - a->make_assumption(requires); - a->function=skip->function; - a->source_location=requires.source_location(); - } - - // ret=function(parameter1, ...) - goto_programt::targett f=check.add_instruction(); - f->make_function_call(call); - f->function=skip->function; - f->source_location=skip->source_location; - - // assert(ensures) - goto_programt::targett a=check.add_instruction(); - a->make_assertion(ensures); - a->function=skip->function; - a->source_location=ensures.source_location(); - - // assume(false) - goto_programt::targett af=check.add_instruction(); - af->make_assumption(false_exprt()); - af->function=skip->function; - af->source_location=ensures.source_location(); - - // prepend the new code to dest - check.destructive_append(tmp_skip); - dest.destructive_insert(dest.instructions.begin(), check); -} - -void code_contractst::apply_code_contracts() { Forall_goto_functions(it, goto_functions) { diff --git a/src/goto-instrument/loop_utils.cpp b/src/goto-instrument/loop_utils.cpp index 9d8c9a51c8b..4ab59238bc9 100644 --- a/src/goto-instrument/loop_utils.cpp +++ b/src/goto-instrument/loop_utils.cpp @@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "loop_utils.h" #include -#include #include #include @@ -109,41 +108,3 @@ void get_modifies( } } } - -// TODO handle aliasing at all -void get_uses( - const local_may_aliast &local_may_alias, - const loopt &loop, - usest &uses) -{ - for(loopt::const_iterator - i_it=loop.begin(); i_it!=loop.end(); i_it++) - { - const goto_programt::instructiont &instruction=**i_it; - if(instruction.code.is_not_nil()) - { - for(const_depth_iteratort it=instruction.code.depth_begin(); - it!=instruction.code.depth_end(); - ++it) - { - if((*it).id()==ID_symbol) - { - uses.insert(*it); - } - } - } - - if(instruction.guard.is_not_nil()) - { - for(const_depth_iteratort it=instruction.guard.depth_begin(); - it!=instruction.guard.depth_end(); - ++it) - { - if((*it).id()==ID_symbol) - { - uses.insert(*it); - } - } - } - } -} diff --git a/src/goto-instrument/loop_utils.h b/src/goto-instrument/loop_utils.h index 1296374eff7..57407ecec1b 100644 --- a/src/goto-instrument/loop_utils.h +++ b/src/goto-instrument/loop_utils.h @@ -17,7 +17,6 @@ Author: Daniel Kroening, kroening@kroening.com class local_may_aliast; typedef std::set modifiest; -typedef std::set usest; typedef const natural_loops_mutablet::natural_loopt loopt; void get_modifies( @@ -25,11 +24,6 @@ void get_modifies( const loopt &loop, modifiest &modifies); -void get_uses( - const local_may_aliast &local_may_alias, - const loopt &loop, - usest &uses); - void build_havoc_code( const goto_programt::targett loop_head, const modifiest &modifies, From 69e25fac6adc249ffd1bec45b524b8e76096280d Mon Sep 17 00:00:00 2001 From: klaas Date: Wed, 1 Aug 2018 09:51:41 -0400 Subject: [PATCH 04/14] Cleans up some loops to have braces --- src/analyses/dependence_graph.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp index 24c0320af66..ada58117611 100644 --- a/src/analyses/dependence_graph.cpp +++ b/src/analyses/dependence_graph.cpp @@ -175,7 +175,9 @@ void dep_graph_domaint::data_dependencies( { bool found=false; for(const auto &wr : w_range.second) + { for(const auto &r_range : r_ranges) + { if(!found && may_be_def_use_pair(wr.first, wr.second, r_range.first, r_range.second)) @@ -184,6 +186,8 @@ void dep_graph_domaint::data_dependencies( data_deps.insert(w_range.first); found=true; } + } + } } dep_graph.reaching_definitions()[to].clear_cache(it->first); From 9a93af6ced126a4c07942bf39a7f3f6057047484 Mon Sep 17 00:00:00 2001 From: klaas Date: Thu, 28 Jun 2018 12:04:05 -0400 Subject: [PATCH 05/14] Disambiguates two exprts with the same ID. This commit resolves an issue where ID_dynamic_object was used to label two semantically distinct exprts. One, with a single operand, was a boolean expression meaning that the operand is a pointer to a dynamic object. This has been renamed to ID_is_dynamic_object. The second, with two operands, is an exprt representing a dynamic object itself. This has stayed ID_dynamic_object. Disambiguating which meaning was intended in each case was relatively easy, as uses of these exprts frequently come with assertions about the number of operands, and so this was used to inform which instances of ID_dynamic_object should be changed and which should be left the same. --- regression/goto-instrument/slice19/test.desc | 2 +- src/ansi-c/c_typecheck_expr.cpp | 7 ++- src/ansi-c/expr2c.cpp | 4 +- src/solvers/flattening/bv_pointers.cpp | 4 +- src/solvers/smt2/smt2_conv.cpp | 2 +- src/util/irep_ids.def | 1 + src/util/pointer_predicates.cpp | 2 +- src/util/simplify_expr.cpp | 4 +- src/util/simplify_expr_class.h | 2 +- src/util/simplify_expr_int.cpp | 4 +- src/util/simplify_expr_pointer.cpp | 12 ++--- src/util/std_expr.h | 48 ++++++++++++++++++++ 12 files changed, 70 insertions(+), 22 deletions(-) diff --git a/regression/goto-instrument/slice19/test.desc b/regression/goto-instrument/slice19/test.desc index 03cff4a4fac..3793f7374e1 100644 --- a/regression/goto-instrument/slice19/test.desc +++ b/regression/goto-instrument/slice19/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c --full-slice ^EXIT=0$ diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index b8b0e7fe595..b598822b084 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -2139,11 +2139,10 @@ exprt c_typecheck_baset::do_special_functions( throw 0; } - exprt dynamic_object_expr=exprt(ID_dynamic_object, expr.type()); - dynamic_object_expr.operands()=expr.arguments(); - dynamic_object_expr.add_source_location()=source_location; + exprt is_dynamic_object_expr = is_dynamic_object_exprt(expr.arguments()[0]); + is_dynamic_object_expr.add_source_location() = source_location; - return dynamic_object_expr; + return is_dynamic_object_expr; } else if(identifier==CPROVER_PREFIX "POINTER_OFFSET") { diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 80b5515dd0f..e5318b5e730 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -3580,8 +3580,8 @@ std::string expr2ct::convert_with_precedence( else if(src.id()==ID_invalid_pointer) return convert_function(src, "__CPROVER_invalid_pointer", precedence=16); - else if(src.id()==ID_dynamic_object) - return convert_function(src, "DYNAMIC_OBJECT", precedence=16); + else if(src.id()==ID_is_dynamic_object) + return convert_function(src, "IS_DYNAMIC_OBJECT", precedence=16); else if(src.id()=="is_zero_string") return convert_function(src, "IS_ZERO_STRING", precedence=16); diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index 5cf7ade92c8..5de771c07e9 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -45,7 +45,7 @@ literalt bv_pointerst::convert_rest(const exprt &expr) } } } - else if(expr.id()==ID_dynamic_object) + else if(expr.id()==ID_is_dynamic_object) { if(operands.size()==1 && operands[0].type().id()==ID_pointer) @@ -735,7 +735,7 @@ void bv_pointerst::add_addr(const exprt &expr, bvt &bv) void bv_pointerst::do_postponed( const postponedt &postponed) { - if(postponed.expr.id()==ID_dynamic_object) + if(postponed.expr.id()==ID_is_dynamic_object) { const pointer_logict::objectst &objects= pointer_logic.objects; diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index c1b14961d76..95493bce85e 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -1367,7 +1367,7 @@ void smt2_convt::convert_expr(const exprt &expr) if(ext>0) out << ")"; // zero_extend } - else if(expr.id()==ID_dynamic_object) + else if(expr.id()==ID_is_dynamic_object) { convert_is_dynamic_object(expr); } diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index d0066054482..95f7bb6db77 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -448,6 +448,7 @@ IREP_ID_TWO(overflow_minus, overflow--) IREP_ID_TWO(overflow_mult, overflow-*) IREP_ID_TWO(overflow_unary_minus, overflow-unary-) IREP_ID_ONE(object_descriptor) +IREP_ID_ONE(is_dynamic_object) IREP_ID_ONE(dynamic_object) IREP_ID_TWO(C_dynamic, #dynamic) IREP_ID_ONE(object_size) diff --git a/src/util/pointer_predicates.cpp b/src/util/pointer_predicates.cpp index 668054bc493..0185d222e54 100644 --- a/src/util/pointer_predicates.cpp +++ b/src/util/pointer_predicates.cpp @@ -70,7 +70,7 @@ exprt dynamic_size(const namespacet &ns) exprt dynamic_object(const exprt &pointer) { - exprt dynamic_expr(ID_dynamic_object, bool_typet()); + exprt dynamic_expr(ID_is_dynamic_object, bool_typet()); dynamic_expr.copy_to_operands(pointer); return dynamic_expr; } diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index f7e442e40ef..23e19a4c239 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -2266,8 +2266,8 @@ bool simplify_exprt::simplify_node(exprt &expr) result=simplify_byte_extract(to_byte_extract_expr(expr)) && result; else if(expr.id()==ID_pointer_object) result=simplify_pointer_object(expr) && result; - else if(expr.id()==ID_dynamic_object) - result=simplify_dynamic_object(expr) && result; + else if(expr.id()==ID_is_dynamic_object) + result=simplify_is_dynamic_object(expr) && result; else if(expr.id()==ID_invalid_pointer) result=simplify_invalid_pointer(expr) && result; else if(expr.id()==ID_object_size) diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h index 5e192292666..3dd7d8601e1 100644 --- a/src/util/simplify_expr_class.h +++ b/src/util/simplify_expr_class.h @@ -96,7 +96,7 @@ class simplify_exprt bool simplify_pointer_object(exprt &expr); bool simplify_object_size(exprt &expr); bool simplify_dynamic_size(exprt &expr); - bool simplify_dynamic_object(exprt &expr); + bool simplify_is_dynamic_object(exprt &expr); bool simplify_invalid_pointer(exprt &expr); bool simplify_same_object(exprt &expr); bool simplify_good_pointer(exprt &expr); diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index 6856c6a38fc..9c6c12635ab 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -1699,7 +1699,7 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr) expr.op0().operands().size()==1) { if(expr.op0().op0().id()==ID_symbol || - expr.op0().op0().id()==ID_dynamic_object || + expr.op0().op0().id()==ID_is_dynamic_object || expr.op0().op0().id()==ID_member || expr.op0().op0().id()==ID_index || expr.op0().op0().id()==ID_string_constant) @@ -1715,7 +1715,7 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr) expr.op0().op0().operands().size()==1) { if(expr.op0().op0().op0().id()==ID_symbol || - expr.op0().op0().op0().id()==ID_dynamic_object || + expr.op0().op0().op0().id()==ID_is_dynamic_object || expr.op0().op0().op0().id()==ID_member || expr.op0().op0().op0().id()==ID_index || expr.op0().op0().op0().id()==ID_string_constant) diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp index b183c81890b..f0e44fc9d2f 100644 --- a/src/util/simplify_expr_pointer.cpp +++ b/src/util/simplify_expr_pointer.cpp @@ -464,7 +464,7 @@ bool simplify_exprt::simplify_inequality_pointer_object(exprt &expr) { if(op.operands().size()!=1 || (op.op0().id()!=ID_symbol && - op.op0().id()!=ID_dynamic_object && + op.op0().id()!=ID_is_dynamic_object && op.op0().id()!=ID_string_constant)) return true; } @@ -508,18 +508,18 @@ bool simplify_exprt::simplify_pointer_object(exprt &expr) return result; } -bool simplify_exprt::simplify_dynamic_object(exprt &expr) +bool simplify_exprt::simplify_is_dynamic_object(exprt &expr) { - if(expr.operands().size()!=1) - return true; + // This should hold as a result of the expr ID being is_dynamic_object. + PRECONDITION(expr.operands().size() == 1); exprt &op=expr.op0(); if(op.id()==ID_if && op.operands().size()==3) { if_exprt if_expr=lift_if(expr, 0); - simplify_dynamic_object(if_expr.true_case()); - simplify_dynamic_object(if_expr.false_case()); + simplify_is_dynamic_object(if_expr.true_case()); + simplify_is_dynamic_object(if_expr.false_case()); simplify_if(if_expr); expr.swap(if_expr); diff --git a/src/util/std_expr.h b/src/util/std_expr.h index e979f45ee69..bf44ed8451a 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -2106,6 +2106,54 @@ inline void validate_expr(const dynamic_object_exprt &value) } +/*! \brief Evaluates to true if the operand is a pointer to a dynamic object. +*/ +class is_dynamic_object_exprt:public unary_predicate_exprt +{ +public: + is_dynamic_object_exprt():unary_predicate_exprt(ID_is_dynamic_object) + { + } + + explicit is_dynamic_object_exprt(const exprt &op): + unary_predicate_exprt(ID_is_dynamic_object, op) + { + } +}; + +/*! \brief Cast a generic exprt to a \ref is_dynamic_object_exprt + * + * This is an unchecked conversion. \a expr must be known to be \ref + * is_dynamic_object_exprt. + * + * \param expr Source expression + * \return Object of type \ref is_dynamic_object_exprt + * + * \ingroup gr_std_expr +*/ +inline const is_dynamic_object_exprt &to_is_dynamic_object_expr( + const exprt &expr) +{ + PRECONDITION(expr.id()==ID_is_dynamic_object); + DATA_INVARIANT( + expr.operands().size()==1, + "is_dynamic_object must have one operand"); + return static_cast(expr); +} + +/*! \copydoc to_is_dynamic_object_expr(const exprt &) + * \ingroup gr_std_expr +*/ +inline is_dynamic_object_exprt &to_is_dynamic_object_expr(exprt &expr) +{ + PRECONDITION(expr.id()==ID_is_dynamic_object); + DATA_INVARIANT( + expr.operands().size()==1, + "is_dynamic_object must have one operand"); + return static_cast(expr); +} + + /*! \brief semantic type conversion */ class typecast_exprt:public unary_exprt From 27b885843e8fab7dc59b75f63a56e10ebaa2f5ac Mon Sep 17 00:00:00 2001 From: klaas Date: Thu, 2 Aug 2018 16:54:10 -0400 Subject: [PATCH 06/14] Turns some checks into DATA_INVARIANTs --- src/solvers/flattening/bv_pointers.cpp | 22 +++++++++++----------- src/util/simplify_expr_pointer.cpp | 6 ++++-- 2 files changed, 15 insertions(+), 13 deletions(-) diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index 5de771c07e9..5a69827092c 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -47,19 +47,19 @@ literalt bv_pointerst::convert_rest(const exprt &expr) } else if(expr.id()==ID_is_dynamic_object) { - if(operands.size()==1 && - operands[0].type().id()==ID_pointer) - { - // we postpone - literalt l=prop.new_variable(); + DATA_INVARIANT(operands.size() == 1 && + operands[0].type().id() == ID_pointer, + std::string("is_dynamic_object_exprt should have one") + + "operand, which should have pointer type."); + // we postpone + literalt l=prop.new_variable(); - postponed_list.push_back(postponedt()); - postponed_list.back().op=convert_bv(operands[0]); - postponed_list.back().bv.push_back(l); - postponed_list.back().expr=expr; + postponed_list.push_back(postponedt()); + postponed_list.back().op=convert_bv(operands[0]); + postponed_list.back().bv.push_back(l); + postponed_list.back().expr=expr; - return l; - } + return l; } else if(expr.id()==ID_lt || expr.id()==ID_le || expr.id()==ID_gt || expr.id()==ID_ge) diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp index f0e44fc9d2f..82764d52b10 100644 --- a/src/util/simplify_expr_pointer.cpp +++ b/src/util/simplify_expr_pointer.cpp @@ -510,8 +510,10 @@ bool simplify_exprt::simplify_pointer_object(exprt &expr) bool simplify_exprt::simplify_is_dynamic_object(exprt &expr) { - // This should hold as a result of the expr ID being is_dynamic_object. - PRECONDITION(expr.operands().size() == 1); + DATA_INVARIANT(expr.operands().size() == 1 && + expr.op0().type().id() == ID_pointer, + std::string("is_dynamic_object_exprt should have one") + + "operand, which should have pointer type."); exprt &op=expr.op0(); From 7f60508f75501d97f5dc74a16900e243eeb661ec Mon Sep 17 00:00:00 2001 From: klaas Date: Wed, 1 Aug 2018 09:55:54 -0400 Subject: [PATCH 07/14] Fixes bugs making goto_rw too conservative When handling the case of pointers, goto_rw would mark both the object pointed to and the pointer itself as written. For example, if x = &i, the line `*x = 1' would yield a write set containing both x and i, instead of just i. This resolves that issue by ensuring that value_set_dereference always gives at least one object that the dereference can refer to. This also resolves a bug wherein &a is marked as reading from a by removing the ID_symbol special case from get_objects_address_of.A --- src/analyses/goto_rw.cpp | 23 +++++++++++-------- src/analyses/reaching_definitions.cpp | 14 +++++------ .../value_set_dereference.cpp | 8 +++++-- 3 files changed, 26 insertions(+), 19 deletions(-) diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp index 61e7467669b..4c9acbd01de 100644 --- a/src/analyses/goto_rw.cpp +++ b/src/analyses/goto_rw.cpp @@ -128,8 +128,6 @@ void rw_range_sett::get_objects_dereference( { const exprt &pointer=deref.pointer(); get_objects_rec(get_modet::READ, pointer); - if(mode!=get_modet::READ) - get_objects_rec(mode, pointer); } void rw_range_sett::get_objects_byte_extract( @@ -414,16 +412,19 @@ void rw_range_sett::get_objects_typecast( void rw_range_sett::get_objects_address_of(const exprt &object) { - if(object.id() == ID_string_constant || + if(object.id() == ID_symbol || + object.id() == ID_string_constant || object.id() == ID_label || object.id() == ID_array || object.id() == ID_null_object) // constant, nothing to do + { return; - else if(object.id()==ID_symbol) - get_objects_rec(get_modet::READ, object); + } else if(object.id()==ID_dereference) + { get_objects_rec(get_modet::READ, object); + } else if(object.id()==ID_index) { const index_exprt &index=to_index_expr(object); @@ -524,6 +525,11 @@ void rw_range_sett::get_objects_rec( get_objects_array(mode, to_array_expr(expr), range_start, size); else if(expr.id()==ID_struct) get_objects_struct(mode, to_struct_expr(expr), range_start, size); + else if(expr.id()==ID_dynamic_object) + { + const auto obj_instance = to_dynamic_object_expr(expr).get_instance(); + add(mode, "goto_rw::dynamic_object-" + std::to_string(obj_instance), 0, -1); + } else if(expr.id()==ID_symbol) { const symbol_exprt &symbol=to_symbol_expr(expr); @@ -564,11 +570,6 @@ void rw_range_sett::get_objects_rec( { // dereferencing may yield some weird ones, ignore these } - else if(mode==get_modet::LHS_W) - { - forall_operands(it, expr) - get_objects_rec(mode, *it); - } else throw "rw_range_sett: assignment to `"+expr.id_string()+"' not handled"; } @@ -605,6 +606,8 @@ void rw_range_set_value_sett::get_objects_dereference( exprt object=deref; dereference(target, object, ns, value_sets); + PRECONDITION(object.is_not_nil()); + range_spect new_size= to_range_spect(pointer_offset_bits(object.type(), ns)); diff --git a/src/analyses/reaching_definitions.cpp b/src/analyses/reaching_definitions.cpp index 7788835f0db..e3fae64dceb 100644 --- a/src/analyses/reaching_definitions.cpp +++ b/src/analyses/reaching_definitions.cpp @@ -307,19 +307,19 @@ void rd_range_domaint::transform_assign( { const irep_idt &identifier=it->first; // ignore symex::invalid_object - const symbolt *symbol_ptr; - if(ns.lookup(identifier, symbol_ptr)) + const symbolt *symbol_ptr = nullptr; + bool not_found = ns.lookup(identifier, symbol_ptr); + if(not_found && has_prefix(id2string(identifier), "symex::invalid_object")) + { continue; - INVARIANT_STRUCTURED( - symbol_ptr!=nullptr, - nullptr_exceptiont, - "Symbol is in symbol table"); + } const range_domaint &ranges=rw_set.get_ranges(it); if(is_must_alias && (!rd.get_is_threaded()(from) || - (!symbol_ptr->is_shared() && + (symbol_ptr != nullptr && + symbol_ptr->is_shared() && !rd.get_is_dirty()(identifier)))) for(const auto &range : ranges) kill(identifier, range.first, range.second); diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index b22ced28326..4b4ee52609e 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -358,8 +358,12 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to( // this is also our guard result.pointer_guard = dynamic_object(pointer_expr); - // can't remove here, turn into *p - result.value=dereference_exprt(pointer_expr, dereference_type); + // TODO should this be object or root_object? + // TODO It's unclear whether this is a good approach to take --- it + // successfully ensures that every (non-null) dereference points to + // something, making the write set computation work correctly, but dynamic + // objects do not seem to be intended to be used in this way. + result.value = object; if(options.get_bool_option("pointer-check")) { From 2fe3ecd498a6e65db6e864145500503601d2456e Mon Sep 17 00:00:00 2001 From: klaas Date: Tue, 31 Jul 2018 10:54:06 -0400 Subject: [PATCH 08/14] Adds slice24 test. --- regression/goto-instrument/slice24/main.c | 14 ++++++++++++++ regression/goto-instrument/slice24/test.desc | 8 ++++++++ 2 files changed, 22 insertions(+) create mode 100644 regression/goto-instrument/slice24/main.c create mode 100644 regression/goto-instrument/slice24/test.desc diff --git a/regression/goto-instrument/slice24/main.c b/regression/goto-instrument/slice24/main.c new file mode 100644 index 00000000000..2149d6ba087 --- /dev/null +++ b/regression/goto-instrument/slice24/main.c @@ -0,0 +1,14 @@ +#include +#include + +static void f(int *x) { *x = 5; } +static void g(int *x) { assert(*x == 5); } + +int main(int argc, char **argv) +{ + int *x = (int*)malloc(sizeof(int)); + f(x); + g(x); + + return 0; +} diff --git a/regression/goto-instrument/slice24/test.desc b/regression/goto-instrument/slice24/test.desc new file mode 100644 index 00000000000..3906443eafc --- /dev/null +++ b/regression/goto-instrument/slice24/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +main.c +--full-slice --add-library +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +Data dependencies across function calls are still not working correctly. From f9512d5296670789115be7add9bc386458edd3e8 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 5 Jun 2018 11:19:42 +0000 Subject: [PATCH 09/14] Code contracts: match up introducing/removing parameter map modifications Code contracts that introduce local declarations result in nested typecheck_declaration calls. The artificial __CPROVER_return_value symbol must then be added/removed by a single call only. --- regression/ansi-c/code_contracts1/main.c | 17 +++++++++++++++++ regression/ansi-c/code_contracts1/test.desc | 8 ++++++++ src/ansi-c/c_typecheck_base.cpp | 8 ++++++-- 3 files changed, 31 insertions(+), 2 deletions(-) create mode 100644 regression/ansi-c/code_contracts1/main.c create mode 100644 regression/ansi-c/code_contracts1/test.desc diff --git a/regression/ansi-c/code_contracts1/main.c b/regression/ansi-c/code_contracts1/main.c new file mode 100644 index 00000000000..19f8efb226b --- /dev/null +++ b/regression/ansi-c/code_contracts1/main.c @@ -0,0 +1,17 @@ +int foo() +__CPROVER_ensures(__CPROVER_forall {int i; 1 == 1}) +{ + return 1; +} + +int bar() +__CPROVER_ensures(__CPROVER_forall {int i; 1 == 1} && + __CPROVER_return_value == 1) +{ + return 1; +} + +int main() { + foo(); + bar(); +} diff --git a/regression/ansi-c/code_contracts1/test.desc b/regression/ansi-c/code_contracts1/test.desc new file mode 100644 index 00000000000..466da18b2b5 --- /dev/null +++ b/regression/ansi-c/code_contracts1/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +^CONVERSION ERROR$ diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp index ee120fe00fd..07f3bf25910 100644 --- a/src/ansi-c/c_typecheck_base.cpp +++ b/src/ansi-c/c_typecheck_base.cpp @@ -760,11 +760,15 @@ void c_typecheck_baset::typecheck_declaration( typet ret_type=empty_typet(); if(new_symbol.type.id()==ID_code) ret_type=to_code_type(new_symbol.type).return_type(); - assert(parameter_map.empty()); if(ret_type.id()!=ID_empty) + { + DATA_INVARIANT( + parameter_map.empty(), "parameter map should be cleared"); parameter_map["__CPROVER_return_value"]=ret_type; + } typecheck_spec_expr(contract, ID_C_spec_ensures); - parameter_map.clear(); + if(ret_type.id()!=ID_empty) + parameter_map.clear(); if(contract.find(ID_C_spec_requires).is_not_nil()) new_symbol.type.add(ID_C_spec_requires)= From 0e51e56c225e1bf2757dbbcc234340f6dcd71c60 Mon Sep 17 00:00:00 2001 From: klaas Date: Wed, 1 Aug 2018 16:35:29 -0400 Subject: [PATCH 10/14] Adds havocking for function calls This commit changes the behaviour of --apply-code-contracts on function calls. Previously, when applying contracts, a function call would be replaced by an assertion that the precondition holds, followed by an assumption that the postcondition holds. This change inserts between that assert/assume pair code that sets all variables that could be modified by the function being called to be nondeterministic. --- src/goto-instrument/code_contracts.cpp | 43 +++++++++++++++++--------- 1 file changed, 29 insertions(+), 14 deletions(-) diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index f4bae2406bd..72b3d9b7bb5 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -23,6 +23,7 @@ Date: February 2016 #include #include "loop_utils.h" +#include "function_modifies.h" enum class contract_opst { APPLY, CHECK }; @@ -52,6 +53,7 @@ class code_contractst void apply_contract( goto_programt &goto_program, + const local_may_aliast &local_may_alias, goto_programt::targett target); void apply_invariant( @@ -78,6 +80,7 @@ class code_contractst void code_contractst::apply_contract( goto_programt &goto_program, + const local_may_aliast &local_may_alias, goto_programt::targett target) { const code_function_callt &call=to_code_function_call(target->code); @@ -109,6 +112,23 @@ void code_contractst::apply_contract( } } + // find out what can be written by the function + // TODO Use a better write-set analysis. + modifiest modifies; + function_modifiest function_modifies(goto_functions); + + // Handle return value of the function + if(call.lhs().is_not_nil()) + { + function_modifies.get_modifies_lhs(local_may_alias, target, + call.lhs(), modifies); + } + function_modifies(call.function(), modifies); + + // build the havocking code + goto_programt havoc_code; + build_havoc_code(target, modifies, havoc_code); + // replace formal parameters by arguments, replace return replace_symbolt replace; @@ -140,7 +160,9 @@ void code_contractst::apply_contract( goto_program.insert_before_swap(target, a); ++target; } - // TODO: Havoc write set of the function between assert and ensure. + + // TODO some sort of replacement on havoc code + goto_program.destructive_insert(target, havoc_code); target->make_assumption(ensures); } @@ -172,8 +194,6 @@ void code_contractst::apply_invariant( return; } - // TODO: Allow for not havocking in the for/while case - // change H: loop; E: ... // to // H: assert(invariant); @@ -210,8 +230,6 @@ void code_contractst::apply_invariant( } // assume !guard - // TODO: consider breaks and how they're implemented. - // TODO: Also consider continues and whether they jump to loop end or head { goto_programt::targett assume = havoc_code.add_instruction(ASSUME); if(loop_head->is_goto()) @@ -321,6 +339,10 @@ void code_contractst::check_contract( replace.insert(p_it.get_identifier(), p); } + // rewrite any use of parameters + replace(requires); + replace(ensures); + // assume(requires) if(requires.is_not_nil()) { @@ -328,9 +350,6 @@ void code_contractst::check_contract( a->make_assumption(requires); a->function=skip->function; a->source_location=requires.source_location(); - - // rewrite any use of parameters - replace(a->guard); } // ret=function(parameter1, ...) @@ -345,9 +364,6 @@ void code_contractst::check_contract( a->function=skip->function; a->source_location=ensures.source_location(); - // rewrite any use of __CPROVER_return_value - replace(a->guard); - // prepend the new code to dest check.destructive_append(tmp_skip); dest.destructive_insert(dest.instructions.begin(), check); @@ -477,7 +493,7 @@ const symbolt &code_contractst::new_tmp_symbol( { if(it->is_function_call()) { - apply_contract(goto_function.body, it); + apply_contract(goto_function.body, local_may_alias, it); } } } @@ -511,7 +527,7 @@ void code_contractst::check_code_contracts() { if(it->is_function_call()) { - apply_contract(goto_function.body, it); + apply_contract(goto_function.body, local_may_alias, it); } } } @@ -521,7 +537,6 @@ void code_contractst::check_code_contracts() check_contract(it->first, it->second, i_it->second.body); } - // remove skips remove_skip(i_it->second.body); goto_functions.update(); From b25eab658c1ad389dd58edc6512ad12bebac09b5 Mon Sep 17 00:00:00 2001 From: klaas Date: Thu, 2 Aug 2018 13:46:31 -0400 Subject: [PATCH 11/14] Fixes initialization for code contracts Because code contracts should be checked in an environment constrained only by the preconditions, we want to check contracts before initializing the dead and deallocated objects --- otherwise, we fail to check the cases where a pointer argument to a function points to a dead or deallocated object but is not NULL. This commit resolves these issues by temporarily initializing dead and deallocated objects to be the same fixed object before checking contracts, and then performing the standard initialization to NULL. --- src/goto-instrument/code_contracts.cpp | 50 ++++++++++++++++++++++++-- 1 file changed, 48 insertions(+), 2 deletions(-) diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index 72b3d9b7bb5..2a192ef681c 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -13,6 +13,9 @@ Date: February 2016 #include "code_contracts.h" +#include +#include +#include #include #include @@ -506,6 +509,7 @@ void code_contractst::check_code_contracts() goto_functionst::function_mapt::iterator i_it= goto_functions.function_map.find(INITIALIZE_FUNCTION); CHECK_RETURN(i_it!=goto_functions.function_map.end()); + goto_programt &init_function = i_it->second.body; Forall_goto_functions(it, goto_functions) { @@ -534,10 +538,52 @@ void code_contractst::check_code_contracts() Forall_goto_functions(it, goto_functions) { - check_contract(it->first, it->second, i_it->second.body); + check_contract(it->first, it->second, init_function); } - remove_skip(i_it->second.body); + // Partially initialize state + goto_programt init_code; + + goto_programt::targett d = init_code.add_instruction(DECL); + d->function = i_it->first; + // TODO add source location + // d->source_location = + + symbol_exprt tmp_var = + new_tmp_symbol(void_typet(), d->source_location).symbol_expr(); + d->code = code_declt(tmp_var); + d->code.add_source_location() = d->source_location; + + { + const symbol_exprt &deallocated_expr = + ns.lookup(CPROVER_PREFIX "deallocated").symbol_expr(); + + goto_programt::targett a = init_code.add_instruction(ASSIGN); + a->function = i_it->first; + // TODO add source location + // a->source_location = + address_of_exprt rhs(tmp_var, to_pointer_type(deallocated_expr.type())); + a->code = code_assignt(deallocated_expr, rhs); + a->code.add_source_location() = a->source_location; + } + + { + const symbol_exprt &dead_expr = + ns.lookup(CPROVER_PREFIX "dead_object").symbol_expr(); + + goto_programt::targett a = init_code.add_instruction(ASSIGN); + a->function = i_it->first; + // TODO add source location + // a->source_location = + address_of_exprt rhs(tmp_var, to_pointer_type(dead_expr.type())); + a->code = code_assignt(dead_expr, rhs); + a->code.add_source_location() = a->source_location; + } + + init_function.destructive_insert(init_function.instructions.begin(), + init_code); + + remove_skip(init_function); goto_functions.update(); } From 930086d5ff38f9d586e239609c5dd4caab31a293 Mon Sep 17 00:00:00 2001 From: klaas Date: Thu, 14 Jun 2018 15:36:58 -0400 Subject: [PATCH 12/14] Makes code contracts use goto_rw for write sets This change replaces the use of local_may_alias analysis in code contracts with the more accurate goto_rw analysis. These analyses are used to find the set of variables written to by a loop or function so that we know which variables to make nondeterministic when abstracting out those pieces of code. --- .../contracts/function_check_05/test.desc | 5 +- src/goto-instrument/code_contracts.cpp | 119 +++++++++++++----- 2 files changed, 93 insertions(+), 31 deletions(-) diff --git a/regression/contracts/function_check_05/test.desc b/regression/contracts/function_check_05/test.desc index 77e210f10d8..49cdb0a73fe 100644 --- a/regression/contracts/function_check_05/test.desc +++ b/regression/contracts/function_check_05/test.desc @@ -1,10 +1,9 @@ -KNOWNBUG +CORE main.c --check-code-contracts ^\[main.assertion.1\] assertion y == 0: FAILURE$ ^\[main.assertion.2\] assertion z == 1: SUCCESS$ ^\[foo.1\] : SUCCESS$ -^VERIFICATION SUCCESSFUL$ +^VERIFICATION FAILED$ -- -- -Contract checking does not properly havoc function calls. diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index 2a192ef681c..888ef09f5f1 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -17,16 +17,18 @@ Date: February 2016 #include #include #include +#include #include #include -#include +#include #include +#include + #include "loop_utils.h" -#include "function_modifies.h" enum class contract_opst { APPLY, CHECK }; @@ -56,12 +58,12 @@ class code_contractst void apply_contract( goto_programt &goto_program, - const local_may_aliast &local_may_alias, + value_setst &value_sets, goto_programt::targett target); void apply_invariant( goto_functionst::goto_functiont &goto_function, - const local_may_aliast &local_may_alias, + value_setst &value_sets, const goto_programt::targett loop_head, const loopt &loop); @@ -72,7 +74,7 @@ class code_contractst void check_apply_invariant( goto_functionst::goto_functiont &goto_function, - const local_may_aliast &local_may_alias, + value_setst &value_sets, const goto_programt::targett loop_head, const loopt &loop); @@ -83,7 +85,7 @@ class code_contractst void code_contractst::apply_contract( goto_programt &goto_program, - const local_may_aliast &local_may_alias, + value_setst &value_sets, goto_programt::targett target) { const code_function_callt &call=to_code_function_call(target->code); @@ -116,17 +118,27 @@ void code_contractst::apply_contract( } // find out what can be written by the function - // TODO Use a better write-set analysis. modifiest modifies; - function_modifiest function_modifies(goto_functions); - // Handle return value of the function - if(call.lhs().is_not_nil()) + rw_range_set_value_sett rw_set(ns, value_sets); + goto_rw(goto_functions, function, rw_set); + forall_rw_range_set_w_objects(it, rw_set) { - function_modifies.get_modifies_lhs(local_may_alias, target, - call.lhs(), modifies); + // Skip over local variables of the function being called, as well as + // variables not in the namespace (e.g. symex::invalid_object) + const symbolt *symbol_ptr; + if(!ns.lookup(it->first, symbol_ptr)) + { + const std::string &name_string = id2string(symbol_ptr->name); + std::string scope_prefix(id2string(ns.lookup(function).name)); + scope_prefix += "::"; + + if(name_string.find(scope_prefix) == std::string::npos) + { + modifies.insert(ns.lookup(it->first).symbol_expr()); + } + } } - function_modifies(call.function(), modifies); // build the havocking code goto_programt havoc_code; @@ -137,7 +149,9 @@ void code_contractst::apply_contract( // TODO: return value could be nil if(type.return_type()!=empty_typet()) + { replace.insert("__CPROVER_return_value", call.lhs()); + } // formal parameters code_function_callt::argumentst::const_iterator a_it= @@ -153,6 +167,18 @@ void code_contractst::apply_contract( replace(requires); replace(ensures); + // Havoc the return value of the function call. + if(type.return_type()!=empty_typet()) + { + const exprt &lhs = call.lhs(); + const exprt &rhs = side_effect_expr_nondett(call.lhs().type()); + target->make_assignment(code_assignt(lhs, rhs)); + } + else + { + target->make_skip(); + } + if(requires.is_not_nil()) { goto_programt::instructiont a(ASSERT); @@ -164,15 +190,19 @@ void code_contractst::apply_contract( ++target; } - // TODO some sort of replacement on havoc code goto_program.destructive_insert(target, havoc_code); - target->make_assumption(ensures); + { + goto_programt::targett a=goto_program.insert_after(target); + a->make_assumption(ensures); + a->function=target->function; + a->source_location=target->source_location; + } } void code_contractst::apply_invariant( goto_functionst::goto_functiont &goto_function, - const local_may_aliast &local_may_alias, + value_setst &value_sets, const goto_programt::targett loop_head, const loopt &loop) { @@ -207,7 +237,20 @@ void code_contractst::apply_invariant( // find out what can get changed in the loop modifiest modifies; - get_modifies(local_may_alias, loop, modifies); + + rw_range_set_value_sett rw_set(ns, value_sets); + for(const goto_programt::targett &inst : loop) + { + goto_rw(inst, rw_set); + } + forall_rw_range_set_w_objects(it, rw_set) + { + const symbolt *symbol_ptr; + if(!ns.lookup(it->first, symbol_ptr)) + { + modifies.insert(ns.lookup(it->first).symbol_expr()); + } + } // build the havocking code goto_programt havoc_code; @@ -275,7 +318,8 @@ void code_contractst::check_contract( static_cast(goto_function.type.find(ID_C_spec_ensures)); // Nothing to check if ensures is nil. - if(ensures.is_nil()) { + if(ensures.is_nil()) + { return; } @@ -374,7 +418,7 @@ void code_contractst::check_contract( void code_contractst::check_apply_invariant( goto_functionst::goto_functiont &goto_function, - const local_may_aliast &local_may_alias, + value_setst &value_sets, const goto_programt::targett loop_head, const loopt &loop) { @@ -393,7 +437,9 @@ void code_contractst::check_apply_invariant( static_cast( loop_end->guard.find(ID_C_spec_loop_invariant)); if(invariant.is_nil()) + { return; + } // change H: loop; E: ... // to @@ -408,7 +454,20 @@ void code_contractst::check_apply_invariant( // find out what can get changed in the loop modifiest modifies; - get_modifies(local_may_alias, loop, modifies); + + rw_range_set_value_sett rw_set(ns, value_sets); + for(const goto_programt::targett &inst : loop) + { + goto_rw(inst, rw_set); + } + forall_rw_range_set_w_objects(it, rw_set) + { + const symbolt *symbol_ptr; + if(!ns.lookup(it->first, symbol_ptr)) + { + modifies.insert(ns.lookup(it->first).symbol_expr()); + } + } // build the havocking code goto_programt havoc_code; @@ -476,18 +535,20 @@ const symbolt &code_contractst::new_tmp_symbol( } { + auto vs = util_make_unique(ns); + (*vs)(goto_functions); + std::unique_ptr value_sets = std::move(vs); + Forall_goto_functions(it, goto_functions) { goto_functionst::goto_functiont &goto_function = it->second; - // TODO: This aliasing check is insufficiently strong, in general. - local_may_aliast local_may_alias(goto_function); natural_loops_mutablet natural_loops(goto_function.body); for(const auto &l_it : natural_loops.loop_map) { apply_invariant(goto_function, - local_may_alias, + *value_sets, l_it.first, l_it.second); } @@ -496,7 +557,7 @@ const symbolt &code_contractst::new_tmp_symbol( { if(it->is_function_call()) { - apply_contract(goto_function.body, local_may_alias, it); + apply_contract(goto_function.body, *value_sets, it); } } } @@ -506,6 +567,10 @@ const symbolt &code_contractst::new_tmp_symbol( void code_contractst::check_code_contracts() { + auto vs = util_make_unique(ns); + (*vs)(goto_functions); + std::unique_ptr value_sets = std::move(vs); + goto_functionst::function_mapt::iterator i_it= goto_functions.function_map.find(INITIALIZE_FUNCTION); CHECK_RETURN(i_it!=goto_functions.function_map.end()); @@ -515,14 +580,12 @@ void code_contractst::check_code_contracts() { goto_functionst::goto_functiont &goto_function = it->second; - // TODO: This aliasing check is insufficiently strong, in general. - local_may_aliast local_may_alias(goto_function); natural_loops_mutablet natural_loops(goto_function.body); for(const auto &l_it : natural_loops.loop_map) { check_apply_invariant(goto_function, - local_may_alias, + *value_sets, l_it.first, l_it.second); } @@ -531,7 +594,7 @@ void code_contractst::check_code_contracts() { if(it->is_function_call()) { - apply_contract(goto_function.body, local_may_alias, it); + apply_contract(goto_function.body, *value_sets, it); } } } From 0e1c9b8ed097a0ccaddbcc9832907d7e02465bbd Mon Sep 17 00:00:00 2001 From: klaas Date: Wed, 18 Jul 2018 14:33:00 -0400 Subject: [PATCH 13/14] Cleans up comments in code_contracts This commit adds some documentation to code-contracts, as well as fixing up small errors or confusing wording in existing comments. --- src/goto-instrument/code_contracts.cpp | 47 ++++++++++++++++--- src/goto-instrument/code_contracts.h | 12 +++++ .../goto_instrument_parse_options.cpp | 2 + 3 files changed, 55 insertions(+), 6 deletions(-) diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index 888ef09f5f1..775beead2e1 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -56,23 +56,56 @@ class code_contractst void code_contracts(goto_functionst::goto_functiont &goto_function); + /// Applies (but does not check) a function contract. + /// This will assume that the contract holds, and then use that assumption + /// to remove the function call located at target. + /// \param goto_program The goto program containing the target callsite. + /// \param value_sets A value_setst object containing information about + /// aliasing in the goto program being analyzed + /// \param target An iterator pointing to the function call to be removed. void apply_contract( goto_programt &goto_program, value_setst &value_sets, goto_programt::targett target); + /// Applies (but does not check) a loop invariant. + /// This will assume that the loop invariant is indeed an invariant, and then + /// use that assumption to remove the loop. + /// \param goto_function The goto function containing the target loop. + /// \param value_sets A value_setst object containing information about + /// aliasing in the goto program being analyzed + /// \param loop_head An iterator pointing to the first instruction of the + /// target loop. + /// \param loop The loop being removed. void apply_invariant( goto_functionst::goto_functiont &goto_function, value_setst &value_sets, const goto_programt::targett loop_head, const loopt &loop); + /// Checks (but does not apply) a function contract. + /// This will build a code snippet to be inserted at dest which will check + // that the function contract is satisfied. + /// \param function_id The id of the function being checked. + /// \param goto_function The goto_function object for the function + /// being checked. + /// \param dest An iterator pointing to the place to insert checking code. void check_contract( const irep_idt &function_id, goto_functionst::goto_functiont &goto_function, goto_programt &dest); - void check_apply_invariant( + /// Checks and applies a loop invariant + /// This will replace the loop with a code snippet (based on the loop) which + /// will check that the loop invariant is indeed ian invariant, and then + /// use that invariant in what follows. + /// \param goto_function The goto function containing the target loop. + /// \param value_sets A value_setst object containing information about + /// aliasing in the goto program being analyzed + /// \param loop_head An iterator pointing to the first instruction of the + /// target loop. + /// \param loop The loop being removed. + void check_apply_invariant( goto_functionst::goto_functiont &goto_function, value_setst &value_sets, const goto_programt::targett loop_head, @@ -297,7 +330,7 @@ void code_contractst::apply_invariant( inst->make_skip(); } - // Now havoc at the loop head. Use insert_swap to + // Now havoc at the loop head. Use insert_before_swap to // preserve jumps to loop head. goto_function.body.insert_before_swap(loop_head, havoc_code); @@ -323,13 +356,15 @@ void code_contractst::check_contract( return; } - // build: - // if(nondet) + // We build the following checking code: + // if(nondet) goto end // decl ret // decl parameter1 ... // assume(requires) [optional] // ret = function(parameter1, ...) // assert(ensures) + // end: + // skip // build skip so that if(nondet) can refer to it goto_programt tmp_skip; @@ -481,7 +516,7 @@ void code_contractst::check_apply_invariant( a->source_location.set_comment("Loop invariant violated before entry"); } - // havoc variables being written to + // havoc variables that can be modified by the loop build_havoc_code(loop_head, modifies, havoc_code); // assume the invariant @@ -516,7 +551,7 @@ void code_contractst::check_apply_invariant( loop_end->guard.make_not(); } - // Now havoc at the loop head. Use insert_swap to + // Now havoc at the loop head. Use insert_before_swap to // preserve jumps to loop head. goto_function.body.insert_before_swap(loop_head, havoc_code); } diff --git a/src/goto-instrument/code_contracts.h b/src/goto-instrument/code_contracts.h index 7c7c02c09c0..87395007fff 100644 --- a/src/goto-instrument/code_contracts.h +++ b/src/goto-instrument/code_contracts.h @@ -19,4 +19,16 @@ class goto_modelt; void apply_code_contracts(goto_modelt &); void check_code_contracts(goto_modelt &); +// clang-format off +#define HELP_APPLY_CODE_CONTRACTS \ + " --apply-code-contracts Assume (without checking) that the contracts used in code hold\n" \ + " This will use __CPROVER_requires, __CPROVER_ensures,\n" \ + " and __CPROVER_loop_invariant as assumptions in order to avoid\n" \ + " checking code that is assumed to satisfy a specification.\n" +#define HELP_CHECK_CODE_CONTRACTS \ + " --check-code-contracts Assume (with checking) that the contracts used in code hold.\n" \ + " This differs from --apply-code-contracts in that in addition to\n" \ + " assuming specifications, it checks that they are correct.\n" +// clang-format on + #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 6f629b46463..23e28c97a94 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1581,6 +1581,8 @@ void goto_instrument_parse_optionst::help() " --undefined-function-is-assume-false\n" // NOLINTNEXTLINE(whitespace/line_length) " convert each call to an undefined function to assume(false)\n" + HELP_APPLY_CODE_CONTRACTS + HELP_CHECK_CODE_CONTRACTS HELP_REPLACE_FUNCTION_BODY "\n" "Loop transformations:\n" From a41ea4d760cb9d7bfef2d2fd330d976d3974cd4e Mon Sep 17 00:00:00 2001 From: klaas Date: Fri, 20 Jul 2018 12:12:35 -0400 Subject: [PATCH 14/14] Makes code contracts depend on other passes This changes the code-contracts passes (both apply and check) to rely on the remove_function_pointers and remove_returns passes. This avoids problems that arose beforehand wherein those passes interfered with the code-contracts passes. --- src/goto-instrument/code_contracts.cpp | 35 +++++++------------ .../goto_instrument_parse_options.cpp | 34 ++++++++++++------ 2 files changed, 36 insertions(+), 33 deletions(-) diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index 775beead2e1..3409fbb8c12 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -20,6 +20,7 @@ Date: February 2016 #include #include +#include #include #include @@ -122,9 +123,9 @@ void code_contractst::apply_contract( goto_programt::targett target) { const code_function_callt &call=to_code_function_call(target->code); - // we don't handle function pointers - if(call.function().id()!=ID_symbol) - return; + // we don't handle function pointers. remove_function_pointers should have + // been invoked by this point. + PRECONDITION(call.function().id() == ID_symbol); const irep_idt &function= to_symbol_expr(call.function()).get_identifier(); @@ -180,10 +181,12 @@ void code_contractst::apply_contract( // replace formal parameters by arguments, replace return replace_symbolt replace; + const irep_idt symbol_name = id2string(function) + RETURN_VALUE_SUFFIX; + const symbolt *existing_symbol = symbol_table.lookup(symbol_name); // TODO: return value could be nil - if(type.return_type()!=empty_typet()) + if(existing_symbol != nullptr) { - replace.insert("__CPROVER_return_value", call.lhs()); + replace.insert("__CPROVER_return_value", existing_symbol->symbol_expr()); } // formal parameters @@ -358,10 +361,9 @@ void code_contractst::check_contract( // We build the following checking code: // if(nondet) goto end - // decl ret // decl parameter1 ... // assume(requires) [optional] - // ret = function(parameter1, ...) + // function(parameter1, ...) // assert(ensures) // end: // skip @@ -385,23 +387,12 @@ void code_contractst::check_contract( call.function()=ns.lookup(function_id).symbol_expr(); replace_symbolt replace; - // decl ret + const irep_idt symbol_name = id2string(function_id) + RETURN_VALUE_SUFFIX; + const symbolt *existing_symbol = symbol_table.lookup(symbol_name); // TODO: Handle void functions - // void functions seem to be handled by goto-cc - if(goto_function.type.return_type()!=empty_typet()) + if(existing_symbol != nullptr) { - goto_programt::targett d=check.add_instruction(DECL); - d->function=skip->function; - d->source_location=skip->source_location; - - symbol_exprt r= - new_tmp_symbol(goto_function.type.return_type(), - d->source_location).symbol_expr(); - d->code=code_declt(r); - - call.lhs()=r; - - replace.insert("__CPROVER_return_value", r); + replace.insert("__CPROVER_return_value", existing_symbol->symbol_expr()); } // decl parameter1 ... diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 23e28c97a94..5d7a7a9b885 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1046,9 +1046,25 @@ void goto_instrument_parse_optionst::instrument_goto_program() goto_model.goto_functions.update(); } - // Uses (without checking) invariants and pre/post-condition pairs. + // replace function pointers, if explicitly requested + if(cmdline.isset("remove-function-pointers")) + { + do_indirect_call_and_rtti_removal(); + } + else if(cmdline.isset("remove-const-function-pointers")) + { + do_remove_const_function_pointers_only(); + } + + // Use invariants and pre/post-condition pairs without checking them. if(cmdline.isset("apply-code-contracts")) { + // Code contracts depends on these other passes. + remove_function_pointers( + get_message_handler(), + goto_model, + cmdline.isset("pointer-check")); + do_remove_returns(); status() << "Applying Code Contracts" << eom; apply_code_contracts(goto_model); } @@ -1056,20 +1072,16 @@ void goto_instrument_parse_optionst::instrument_goto_program() // Uses invariants and pre/post-condition pairs and verifies that they hold. if(cmdline.isset("check-code-contracts")) { + // Code contracts depends on these other passes. + remove_function_pointers( + get_message_handler(), + goto_model, + cmdline.isset("pointer-check")); + do_remove_returns(); status() << "Checking Code Contracts" << eom; check_code_contracts(goto_model); } - // replace function pointers, if explicitly requested - if(cmdline.isset("remove-function-pointers")) - { - do_indirect_call_and_rtti_removal(); - } - else if(cmdline.isset("remove-const-function-pointers")) - { - do_remove_const_function_pointers_only(); - } - if(cmdline.isset("function-inline")) { std::string function=cmdline.get_value("function-inline");