diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index ca8189ff846..aa46dfe1cda 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -42,6 +42,7 @@ Date: February 2016 #include "instrument_spec_assigns.h" #include "memory_predicates.h" #include "utils.h" +#include "utils_kani.h" #include #include @@ -53,6 +54,7 @@ void code_contractst::check_apply_loop_contracts( goto_programt::targett loop_head, goto_programt::targett loop_end, const loopt &loop, + const goto_programt::instructionst &eval_ins, exprt assigns_clause, exprt invariant, exprt decreases_clause, @@ -165,6 +167,15 @@ void code_contractst::check_apply_loop_contracts( .symbol_expr(); pre_loop_head_instrs.add( goto_programt::make_decl(initial_invariant_val, loop_head_location)); + + // instrument instructions to evaluate invariants before assert(inv) + // or assume(inv) + for(const auto &in : eval_ins) + { + auto new_in = goto_programt::instructiont(in); + pre_loop_head_instrs.add(std::move(new_in)); + } + { // Although the invariant at this point will not have side effects, // it is still a C expression, and needs to be "goto_convert"ed. @@ -326,6 +337,14 @@ void code_contractst::check_apply_loop_contracts( pre_loop_head_instrs.add( goto_programt::make_assignment(in_loop_havoc_block, false_exprt{})); + // instrument instructions to evaluate invariants before assert(inv) + // or assume(inv) + for(const auto &in : eval_ins) + { + auto new_in = goto_programt::instructiont(in); + pre_loop_head_instrs.add(std::move(new_in)); + } + // Insert the second block of pre_loop_head_instrs: the havocing code. // We do not `add_pragma_disable_assigns_check`, // so that the enclosing scope's assigns clause instrumentation @@ -336,6 +355,13 @@ void code_contractst::check_apply_loop_contracts( // We use a block scope for assumption, since it's immediately goto converted, // and doesn't need to be kept around. { + // instrument instructions to evaluate invariants before assert(inv) + // or assume(inv) + for(const auto &in : eval_ins) + { + auto new_in = goto_programt::instructiont(in); + pre_loop_head_instrs.add(std::move(new_in)); + } code_assumet assumption{invariant}; assumption.add_source_location() = loop_head_location; converter.goto_convert(assumption, pre_loop_head_instrs, mode); @@ -437,6 +463,13 @@ void code_contractst::check_apply_loop_contracts( // We use a block scope for assertion, since it's immediately goto converted, // and doesn't need to be kept around. { + // instrument instructions to evaluate invariants before assert(inv) + // or assume(inv) + for(const auto &in : eval_ins) + { + auto new_in = goto_programt::instructiont(in); + pre_loop_end_instrs.add(std::move(new_in)); + } code_assertt assertion{invariant}; assertion.add_source_location() = loop_head_location; assertion.add_source_location().set_comment( @@ -839,8 +872,15 @@ void code_contractst::apply_loop_contract( return; inlining_decoratort decorated(log.get_message_handler()); - goto_function_inline( - goto_functions, function_name, ns, log.get_message_handler()); + + // For kani loop contracts, we postponed the inlining after + // get the loop invariants as they are a sequence of instructions + // rather than only an expression + if(!apply_kani_loop_contracts) + { + goto_function_inline( + goto_functions, function_name, ns, log.get_message_handler()); + } INVARIANT( decorated.get_recursive_call_set().size() == 0, @@ -866,18 +906,21 @@ void code_contractst::apply_loop_contract( { const typename natural_loops_mutablet::loopt &content; const goto_programt::targett head_target, end_target; + goto_programt::instructionst eval_instrs; exprt assigns_clause, invariant, decreases_clause; loop_graph_nodet( const typename natural_loops_mutablet::loopt &loop, const goto_programt::targett head, const goto_programt::targett end, + const goto_programt::instructionst ins, const exprt &assigns, const exprt &inv, const exprt &decreases) : content(loop), head_target(head), end_target(end), + eval_instrs(ins), assigns_clause(assigns), invariant(inv), decreases_clause(decreases) @@ -894,6 +937,12 @@ void code_contractst::apply_loop_contract( goto_programt::target_less_than> loop_head_ends; + // Preprocess loops from kani + if(apply_kani_loop_contracts) + { + annotate_kani_loop_invariants(goto_function.body, log); + } + for(const auto &loop_head_and_content : natural_loops.loop_map) { const auto &loop_body = loop_head_and_content.second; @@ -966,6 +1015,8 @@ void code_contractst::apply_loop_contract( goto_function.body, loop_head, goto_programt::make_skip()); loop_end->set_target(loop_head); + goto_programt::instructionst eval_instrs; + exprt assigns_clause = static_cast(loop_end->condition().find(ID_C_spec_assigns)); exprt invariant = static_cast( @@ -973,6 +1024,13 @@ void code_contractst::apply_loop_contract( exprt decreases_clause = static_cast( loop_end->condition().find(ID_C_spec_decreases)); + // get kani loop invariants and the evaluation instructions. + if(apply_kani_loop_contracts) + { + get_kani_invariants( + goto_function, loop_head, invariant.operands(), eval_instrs); + } + if(invariant.is_nil()) { if(decreases_clause.is_not_nil() || assigns_clause.is_not_nil()) @@ -1005,6 +1063,7 @@ void code_contractst::apply_loop_contract( loop_head_end.second.second, loop_head, loop_end, + eval_instrs, assigns_clause, invariant, decreases_clause); @@ -1017,6 +1076,13 @@ void code_contractst::apply_loop_contract( to_check_contracts_on_children.push_back(idx); } + // The postponed inlining + if(apply_kani_loop_contracts) + { + goto_function_inline( + goto_functions, function_name, ns, log.get_message_handler()); + } + for(size_t outer = 0; outer < loop_nesting_graph.size(); ++outer) { for(size_t inner = 0; inner < loop_nesting_graph.size(); ++inner) @@ -1104,6 +1170,7 @@ void code_contractst::apply_loop_contract( loop_node.head_target, loop_node.end_target, updated_loops.loop_map[loop_node.head_target], + loop_node.eval_instrs, loop_node.assigns_clause, loop_node.invariant, loop_node.decreases_clause, diff --git a/src/goto-instrument/contracts/contracts.h b/src/goto-instrument/contracts/contracts.h index ddf4358bc57..ce6906d8cbd 100644 --- a/src/goto-instrument/contracts/contracts.h +++ b/src/goto-instrument/contracts/contracts.h @@ -33,6 +33,10 @@ Date: February 2016 #define HELP_LOOP_CONTRACTS \ " {y--apply-loop-contracts} \t check and use loop contracts when provided\n" +#define FLAG_KANI_LOOP_CONTRACTS "apply-kani-loop-contracts" +#define HELP_KANI_LOOP_CONTRACTS \ + " {y--apply-kani-loop-contracts} \t check loop contracts from kani\n" + #define FLAG_LOOP_CONTRACTS_NO_UNWIND "loop-contracts-no-unwind" #define HELP_LOOP_CONTRACTS_NO_UNWIND \ " {y--loop-contracts-no-unwind} \t do not unwind transformed loops\n" @@ -122,6 +126,7 @@ class code_contractst goto_programt::targett loop_head, goto_programt::targett loop_end, const loopt &loop, + const goto_programt::instructionst &eval_ins, exprt assigns_clause, exprt invariant, exprt decreases_clause, @@ -144,6 +149,9 @@ class code_contractst // Unwind transformed loops after applying loop contracts or not. bool unwind_transformed_loops = true; + // Unwind transformed loops after applying loop contracts or not. + bool apply_kani_loop_contracts = false; + protected: goto_modelt &goto_model; symbol_tablet &symbol_table; diff --git a/src/goto-instrument/contracts/utils_kani.cpp b/src/goto-instrument/contracts/utils_kani.cpp new file mode 100644 index 00000000000..5743d914f8d --- /dev/null +++ b/src/goto-instrument/contracts/utils_kani.cpp @@ -0,0 +1,156 @@ +/*******************************************************************\ + +Module: Utility functions for Kani code contracts. + +Author: Qinheping Hu, qinhh@amazon.com + +\*******************************************************************/ + +#include "utils_kani.h" + +#include + +bool is_kani_loop_invariant(const goto_programt::instructiont instr) +{ + if(!instr.is_function_call()) + return false; + + auto s = id2string(to_symbol_expr(instr.call_function()).get_identifier()); + return (s.find("kani_loop_invariant") != std::string::npos) && + (s.find("kani_loop_invariant_") == std::string::npos); +} + +bool is_kani_loop_invariant_begin(const goto_programt::instructiont instr) +{ + if(!instr.is_function_call()) + return false; + + auto s = id2string(to_symbol_expr(instr.call_function()).get_identifier()); + return s.find("kani_loop_invariant_begin") != std::string::npos; +} + +bool is_kani_loop_invariant_end(const goto_programt::instructiont instr) +{ + if(!instr.is_function_call()) + return false; + + auto s = id2string(to_symbol_expr(instr.call_function()).get_identifier()); + return s.find("kani_loop_invariant_end") != std::string::npos; +} + +void annotate_kani_loop_invariants(goto_programt &body, messaget &log) +{ + // The place holder function call + // kani_loop_invariant(cond) + // indicate its successor loop latch contains loop invariants. + // So for each such function call, we find the loop end for it and + // annotate loop contracts to the loop end. + // Note that here we only annotate 'true' to indicate it contains + // loop contracts. And will later get the loop contracts with another pass. + + natural_loops_mutablet natural_loops(body); + std::set + loop_latches; + + // Collect all latches + for(const auto &loop_head_and_content : natural_loops.loop_map) + { + const auto &loop_content = loop_head_and_content.second; + // Skip empty loops and self-looped node. + if(loop_content.size() <= 1) + continue; + + auto loop_head = loop_head_and_content.first; + auto loop_end = loop_head; + + // Find the last back edge to `loop_head` + for(const auto &t : loop_content) + { + if( + t->is_goto() && t->get_target() == loop_head && + t->location_number > loop_end->location_number) + loop_end = t; + } + + if(loop_end == loop_head) + { + log.error() << "Could not find end of the loop starting at: " + << loop_head->source_location() << messaget::eom; + throw 0; + } + loop_latches.insert(loop_end); + } + + // Go through all instructions in the body to find the placeholder + // kani_loop_invariant() + for(auto it = body.instructions.begin(); it != body.instructions.end(); it++) + { + if(is_kani_loop_invariant(*it)) + { + auto temp_it = it; + while(!loop_latches.count(temp_it)) + { + temp_it = body.get_successors(temp_it).front(); + } + + auto op = and_exprt(true_exprt(), true_exprt()); + + temp_it->condition_nonconst().add(ID_C_spec_loop_invariant).swap(op); + } + } +} + +void get_kani_invariants( + const goto_functiont &goto_function, + const goto_programt::const_targett &loop_head, + exprt::operandst &invariant_clauses, + goto_programt::instructionst &eval_instructions) +{ + // The loop invariants in kani goto are passed as the instructions + // right before the loop head, and between two placeholder function + // calls kani_loop_invariant_begin() and kani_loop_invariant_end(). + auto &body = goto_function.body; + + for(auto it = body.instructions.begin(); it != body.instructions.end(); it++) + { + // first find the loop head + if(it == loop_head) + { + // skip irrelevant instructions until we see the placeholder + while(!is_kani_loop_invariant_end(*it)) + { + it--; + } + // skip the placeholder + it--; + + // copy and store all instructions between the two placeholders + while(!is_kani_loop_invariant_begin(*it)) + { + // except for goto and dead + // because here the goto is not a real goto, but just goto the next + // instruction. + // Dead instructions are for those temporary variables and can be + // safely ignored here. + if(!it->is_goto() && !it->is_dead()) + { + auto new_instruction = goto_programt::instructiont(*it); + new_instruction.target_number = + goto_programt::instructiont::nil_target; + eval_instructions.push_front(new_instruction); + } + + // The only function call assign the evaluated result to a boolean + // variable. We will use the result variable as loop invariants. + if(it->is_function_call()) + { + invariant_clauses.push_back( + typecast_exprt(it->call_lhs(), bool_typet())); + } + it--; + } + return; + } + } + UNREACHABLE; +} diff --git a/src/goto-instrument/contracts/utils_kani.h b/src/goto-instrument/contracts/utils_kani.h new file mode 100644 index 00000000000..3622d352e4e --- /dev/null +++ b/src/goto-instrument/contracts/utils_kani.h @@ -0,0 +1,51 @@ +/*******************************************************************\ + +Module: Utility functions for Kani code contracts. + +Author: Qinheping Hu, qinhh@amazon.com + +\*******************************************************************/ + +#ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_KANI_H +#define CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_KANI_H + +#include +#include +#include +#include + +#include +#include + +#include + +#include +#include +#include + +/// Decide if an instruction is call to the kani placeholder +/// kani_loop_invariant(cond); +bool is_kani_loop_invariant(const goto_programt::instructiont instr); + +/// Decide if an instruction is call to the kani placeholder +/// kani_loop_invariant_begin(); +bool is_kani_loop_invariant_begin(const goto_programt::instructiont instr); + +/// Decide if an instruction is call to the kani placeholder +/// kani_loop_invariant_end(); +bool is_kani_loop_invariant_end(const goto_programt::instructiont instr); + +/// Find loops end with the call to placeholder +/// kani_loop_invariant(cond); +/// and set the spec_loop_invariants sub of the latch node to true +void annotate_kani_loop_invariants(goto_programt &body, messaget &log); + +/// Get the instructions `eval_instructions` to evaluate the kani loop +/// invariants. The evaluation result will be `invariant_clause` +void get_kani_invariants( + const goto_functiont &goto_function, + const goto_programt::const_targett &loop_head, + exprt::operandst &invariant_clauses, + goto_programt::instructionst &eval_instructions); + +#endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_KANI_H diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index b26f65efe26..8bf3d78873f 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1236,9 +1236,12 @@ void goto_instrument_parse_optionst::instrument_goto_program() to_exclude_from_nondet_static, log.get_message_handler()); } - else if((cmdline.isset(FLAG_LOOP_CONTRACTS) || - cmdline.isset(FLAG_REPLACE_CALL) || - cmdline.isset(FLAG_ENFORCE_CONTRACT))) + + if( + !use_dfcc && + (cmdline.isset(FLAG_LOOP_CONTRACTS) || cmdline.isset(FLAG_REPLACE_CALL) || + cmdline.isset(FLAG_ENFORCE_CONTRACT) || + cmdline.isset(FLAG_KANI_LOOP_CONTRACTS))) { do_indirect_call_and_rtti_removal(); log.status() << "Trying to force one backedge per target" << messaget::eom; @@ -1264,7 +1267,9 @@ void goto_instrument_parse_optionst::instrument_goto_program() contracts.replace_calls(to_replace); contracts.enforce_contracts(to_enforce, to_exclude_from_nondet_static); - if(cmdline.isset(FLAG_LOOP_CONTRACTS)) + if( + cmdline.isset(FLAG_LOOP_CONTRACTS) || + cmdline.isset(FLAG_KANI_LOOP_CONTRACTS)) { if(cmdline.isset(FLAG_LOOP_CONTRACTS_NO_UNWIND)) { @@ -1280,6 +1285,10 @@ void goto_instrument_parse_optionst::instrument_goto_program() << "them at least twice to pass unwinding-assertions." << messaget::eom; } + + if(cmdline.isset(FLAG_KANI_LOOP_CONTRACTS)) + contracts.apply_kani_loop_contracts = true; + contracts.apply_loop_contracts(to_exclude_from_nondet_static); } } diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 5b64af490e5..9e69eb22210 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -101,6 +101,7 @@ Author: Daniel Kroening, kroening@kroening.com "(horn)(skip-loops):(model-argc-argv):" \ OPT_DFCC \ "(" FLAG_LOOP_CONTRACTS ")" \ + "(" FLAG_KANI_LOOP_CONTRACTS ")" \ "(" FLAG_LOOP_CONTRACTS_NO_UNWIND ")" \ "(" FLAG_LOOP_CONTRACTS_FILE "):" \ "(" FLAG_REPLACE_CALL "):" \