From 94cd8be06c14448ff209c17e856b17b7fcbac1c8 Mon Sep 17 00:00:00 2001 From: klaas Date: Wed, 23 May 2018 14:55:12 -0400 Subject: [PATCH 1/3] 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 98d0d1248eb..494d2517e19 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: @@ -322,26 +435,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()) { @@ -349,9 +463,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, ...) @@ -366,9 +477,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()); @@ -380,10 +488,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); @@ -398,7 +538,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 0c727f383b9cd0a3f5395e9ea75376bb8c9b5725 Mon Sep 17 00:00:00 2001 From: klaas Date: Fri, 25 May 2018 15:33:37 -0400 Subject: [PATCH 2/3] 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 494d2517e19..4c36c354a0a 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()); - jump->targets.push_back(loop_end); - jump->function=loop_head->function; - jump->source_location=loop_head->source_location; + 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( @@ -520,17 +782,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 ee02a3b1695..2ddd960f30b 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 @@ -107,3 +108,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 c3c6b8b4d42920f50c2a5cd4a2b9d75ae8dcb506 Mon Sep 17 00:00:00 2001 From: klaas Date: Wed, 1 Aug 2018 16:35:35 -0400 Subject: [PATCH 3/3] 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 | 296 +------------------------ src/goto-instrument/loop_utils.cpp | 39 ---- src/goto-instrument/loop_utils.h | 6 - 3 files changed, 1 insertion(+), 340 deletions(-) diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index 4c36c354a0a..e5139b90da4 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,122 +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())); - 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 2ddd960f30b..ee02a3b1695 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 @@ -108,41 +107,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,