diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile index 74e73632d96..df1a5df8279 100644 --- a/src/cbmc/Makefile +++ b/src/cbmc/Makefile @@ -34,6 +34,15 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../goto-instrument/full_slicer$(OBJEXT) \ ../goto-instrument/nondet_static$(OBJEXT) \ ../goto-instrument/cover$(OBJEXT) \ + ../goto-instrument/cover_basic_blocks$(OBJEXT) \ + ../goto-instrument/cover_filter$(OBJEXT) \ + ../goto-instrument/cover_instrument_branch$(OBJEXT) \ + ../goto-instrument/cover_instrument_condition$(OBJEXT) \ + ../goto-instrument/cover_instrument_decision$(OBJEXT) \ + ../goto-instrument/cover_instrument_location$(OBJEXT) \ + ../goto-instrument/cover_instrument_mcdc$(OBJEXT) \ + ../goto-instrument/cover_instrument_other$(OBJEXT) \ + ../goto-instrument/cover_util$(OBJEXT) \ ../analyses/analyses$(LIBEXT) \ ../langapi/langapi$(LIBEXT) \ ../xmllang/xmllang$(LIBEXT) \ diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index cccea229ada..052017763ff 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -117,7 +117,7 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) options.set_option("show-vcc", true); if(cmdline.isset("cover")) - options.set_option("cover", cmdline.get_values("cover")); + parse_cover_options(cmdline, options); if(cmdline.isset("mm")) options.set_option("mm", cmdline.get_value("mm")); @@ -810,10 +810,7 @@ bool cbmc_parse_optionst::process_goto_program( // instrument cover goals if(cmdline.isset("cover")) { - if(instrument_cover_goals( - cmdline, - goto_model, - get_message_handler())) + if(instrument_cover_goals(options, goto_model, get_message_handler())) return true; } diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index da86474e7f1..720a3981d3c 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -19,6 +19,15 @@ SRC = accelerate/accelerate.cpp \ concurrency.cpp \ count_eloc.cpp \ cover.cpp \ + cover_basic_blocks.cpp \ + cover_filter.cpp \ + cover_instrument_branch.cpp \ + cover_instrument_condition.cpp \ + cover_instrument_decision.cpp \ + cover_instrument_location.cpp \ + cover_instrument_mcdc.cpp \ + cover_instrument_other.cpp \ + cover_util.cpp \ document_properties.cpp \ dot.cpp \ dump_c.cpp \ diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index 5fe8e6c469d..bb32c61ccd8 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -11,1544 +11,221 @@ Date: May 2016 /// \file /// Coverage Instrumentation - #include "cover.h" -#include -#include -#include -#include - -#include -#include -#include -#include #include - #include - -namespace -{ -class basic_blockst -{ -public: - explicit basic_blockst(const goto_programt &_goto_program) - { - bool next_is_target=true; - unsigned current_block=0; - - forall_goto_program_instructions(it, _goto_program) - { - // Is it a potential beginning of a block? - if(next_is_target || it->is_target()) - { - // We keep the block number if this potential block - // is a continuation of a previous block through - // unconditional forward gotos; otherwise we increase the - // block number. - bool increase_block_nr=true; - if(it->incoming_edges.size()==1) - { - goto_programt::targett in_t=*it->incoming_edges.begin(); - if(in_t->is_goto() && - !in_t->is_backwards_goto() && - in_t->guard.is_true()) - { - current_block=block_map[in_t]; - increase_block_nr=false; - } - } - if(increase_block_nr) - { - block_infos.push_back(block_infot()); - block_infos.back().representative_inst=it; - block_infos.back().source_location=source_locationt::nil(); - current_block=block_infos.size()-1; - } - } - - INVARIANT( - current_blocksource_location.get_line(); - if(!line.empty()) - block_info.lines.insert(unsafe_string2unsigned(id2string(line))); - - // set representative program location to instrument - if(!it->source_location.is_nil() && - !it->source_location.get_file().empty() && - !it->source_location.get_line().empty() && - block_info.source_location.is_nil()) - { - block_info.representative_inst=it; // update - block_info.source_location=it->source_location; - } - - next_is_target= -#if 0 - // Disabled for being too messy - it->is_goto() || it->is_function_call() || it->is_assume(); -#else - it->is_goto() || it->is_function_call(); -#endif - } - - for(auto &block_info : block_infos) - update_covered_lines(block_info); - } - - /// \param t a goto instruction - /// \return the block number of the block - /// the given goto instruction is part of - unsigned block_of(goto_programt::const_targett t) - { - block_mapt::const_iterator it=block_map.find(t); - INVARIANT(it!=block_map.end(), "instruction must be part of a block"); - return it->second; - } - - /// \param block_nr a block number - /// \return the instruction selected for - /// instrumentation representative of the given block - goto_programt::const_targett instruction_of(unsigned block_nr) - { - INVARIANT(block_nr blocks_seen; - std::set bytecode_indices_seen; - - forall_goto_program_instructions(it, goto_program) - { - unsigned block_nr=block_of(it); - if(blocks_seen.find(block_nr)!=blocks_seen.end()) - continue; - - INVARIANT(block_nrsource_location.get_java_bytecode_index().empty()) - { - // search for a representative - if(bytecode_indices_seen.insert( - it->source_location.get_java_bytecode_index()).second) - { - block_info.representative_inst=it; - block_info.source_location=it->source_location; - update_covered_lines(block_info); - blocks_seen.insert(block_nr); - msg.debug() << it->function - << " block " << (block_nr+1) - << ": location " << it->location_number - << ", bytecode-index " - << it->source_location.get_java_bytecode_index() - << " selected for instrumentation." << messaget::eom; - } - } - } - else if(it==block_info.representative_inst) - { - // check the existing representative - if(!it->source_location.get_java_bytecode_index().empty()) - { - if(bytecode_indices_seen.insert( - it->source_location.get_java_bytecode_index()).second) - { - blocks_seen.insert(block_nr); - } - else - { - // clash, reset to search for a new one - block_info.representative_inst=goto_program.instructions.end(); - block_info.source_location=source_locationt::nil(); - msg.debug() << it->function - << " block " << (block_nr+1) - << ", location " << it->location_number - << ": bytecode-index " - << it->source_location.get_java_bytecode_index() - << " already instrumented." - << " Searching for alternative instruction" - << " to instrument." << messaget::eom; - } - } - } - } - } - - /// Output warnings about ignored blocks - /// \param goto_program The goto program - /// \param message_handler The message handler - void report_block_anomalies( - const goto_programt &goto_program, - message_handlert &message_handler) - { - messaget msg(message_handler); - std::set blocks_seen; - forall_goto_program_instructions(it, goto_program) - { - unsigned block_nr=block_of(it); - const block_infot &block_info=block_infos.at(block_nr); - - if(blocks_seen.insert(block_nr).second && - block_info.representative_inst==goto_program.instructions.end()) - { - msg.warning() << "Ignoring block " << (block_nr+1) << " location " - << it->location_number << " " - << it->source_location - << " (bytecode-index already instrumented)" - << messaget::eom; - } - else if(block_info.representative_inst==it && - block_info.source_location.is_nil()) - { - msg.warning() << "Ignoring block " << (block_nr+1) << " location " - << it->location_number << " " - << it->function - << " (missing source location)" - << messaget::eom; - } - // The location numbers printed here are those - // before the coverage instrumentation. - } - } - - void output(std::ostream &out) const - { - for(block_mapt::const_iterator - b_it=block_map.begin(); - b_it!=block_map.end(); - b_it++) - out << b_it->first->source_location - << " -> " << b_it->second - << '\n'; - } - -protected: - // map program locations to block numbers - typedef std::map block_mapt; - block_mapt block_map; - - struct block_infot - { - /// the program location to instrument for this block - goto_programt::const_targett representative_inst; - - /// the source location representative for this block - // (we need a separate copy of source locations because we attach - // the line number ranges to them) - source_locationt source_location; - - // map block numbers to source code locations - /// the set of lines belonging to this block - std::unordered_set lines; - }; - - typedef std::vector block_infost; - block_infost block_infos; - - /// create list of covered lines as CSV string and set as property of source - /// location of basic block, compress to ranges if applicable - void update_covered_lines(block_infot &block_info) - { - if(block_info.source_location.is_nil()) - return; - - const auto &cover_set=block_info.lines; - INVARIANT(!cover_set.empty(), - "covered lines set must not be empty"); - std::vector - line_list{cover_set.begin(), cover_set.end()}; - - format_number_ranget format_lines; - std::string covered_lines=format_lines(line_list); - block_info.source_location.set_basic_block_covered_lines(covered_lines); - } -}; -} - -const char *as_string(coverage_criteriont c) -{ - switch(c) - { - case coverage_criteriont::LOCATION: return "location"; - case coverage_criteriont::BRANCH: return "branch"; - case coverage_criteriont::DECISION: return "decision"; - case coverage_criteriont::CONDITION: return "condition"; - case coverage_criteriont::PATH: return "path"; - case coverage_criteriont::MCDC: return "MC/DC"; - case coverage_criteriont::ASSERTION: return "assertion"; - case coverage_criteriont::COVER: return "cover instructions"; - default: return ""; - } -} - -bool is_condition(const exprt &src) -{ - if(src.type().id()!=ID_bool) - return false; - - // conditions are 'atomic predicates' - if(src.id()==ID_and || src.id()==ID_or || - src.id()==ID_not || src.id()==ID_implies) - return false; - - return true; -} - -void collect_conditions_rec(const exprt &src, std::set &dest) -{ - if(src.id()==ID_address_of) - { - return; - } - - for(const auto &op : src.operands()) - collect_conditions_rec(op, dest); - - if(is_condition(src) && !src.is_constant()) - dest.insert(src); -} - -std::set collect_conditions(const exprt &src) -{ - std::set result; - collect_conditions_rec(src, result); - return result; -} - -std::set collect_conditions(const goto_programt::const_targett t) -{ - switch(t->type) - { - case GOTO: - case ASSERT: - return collect_conditions(t->guard); - - case ASSIGN: - case FUNCTION_CALL: - return collect_conditions(t->code); - - default: - { - } - } - - return std::set(); -} - -void collect_operands(const exprt &src, std::vector &dest) -{ - for(const exprt &op : src.operands()) - { - if(op.id()==src.id()) - collect_operands(op, dest); - else - dest.push_back(op); - } -} - -/// To recursively collect controlling exprs for for mcdc coverage. -void collect_mcdc_controlling_rec( - const exprt &src, - const std::vector &conditions, - std::set &result) -{ - // src is conjunction (ID_and) or disjunction (ID_or) - if(src.id()==ID_and || - src.id()==ID_or) - { - std::vector operands; - collect_operands(src, operands); - - if(operands.size()==1) - { - exprt e=*operands.begin(); - collect_mcdc_controlling_rec(e, conditions, result); - } - else if(!operands.empty()) - { - for(std::size_t i=0; i others1, others2; - if(!conditions.empty()) - { - others1.push_back(conjunction(conditions)); - others2.push_back(conjunction(conditions)); - } - - for(std::size_t j=0; j o=operands; - - // 'o[i]' needs to be true and false - std::vector new_conditions=conditions; - new_conditions.push_back(conjunction(o)); - result.insert(conjunction(new_conditions)); - - o[i].make_not(); - new_conditions.back()=conjunction(o); - result.insert(conjunction(new_conditions)); - } - else - { - std::vector others; - others.reserve(operands.size()-1); - - for(std::size_t j=0; j new_conditions=conditions; - new_conditions.push_back(c); - - collect_mcdc_controlling_rec(op, new_conditions, result); - } - } - } - } - else if(src.id()==ID_not) - { - exprt e=to_not_expr(src).op(); - if(!is_condition(e)) - collect_mcdc_controlling_rec(e, conditions, result); - else - { - // to store a copy of ''src'' - std::vector new_conditions1=conditions; - new_conditions1.push_back(src); - result.insert(conjunction(new_conditions1)); - - // to store a copy of its negation, i.e., ''e'' - std::vector new_conditions2=conditions; - new_conditions2.push_back(e); - result.insert(conjunction(new_conditions2)); - } - } - else - { - /** - * It may happen that ''is_condition(src)'' is valid, - * but we ignore this case here as it can be handled - * by the routine decision/condition detection. - **/ - } -} - -std::set collect_mcdc_controlling( - const std::set &decisions) -{ - std::set result; - - for(const auto &d : decisions) - collect_mcdc_controlling_rec(d, { }, result); - - return result; -} - -/// To replace the i-th expr of ''operands'' with each expr inside -/// ''replacement_exprs''. -std::set replacement_conjunction( - const std::set &replacement_exprs, - const std::vector &operands, - const std::size_t i) -{ - std::set result; - for(auto &y : replacement_exprs) - { - std::vector others; - for(std::size_t j=0; j collect_mcdc_controlling_nested( - const std::set &decisions) -{ - // To obtain the 1st-level controlling conditions - std::set controlling=collect_mcdc_controlling(decisions); - - std::set result; - // For each controlling condition, to check if it contains - // non-atomic exprs - for(auto &src : controlling) - { - std::set s1, s2; - /** - * The final controlling conditions resulted from ''src'' - * will be stored in ''s1''; ''s2'' is usd to hold the - * temporary expansion. - **/ - s1.insert(src); - - // dual-loop structure to eliminate complex - // non-atomic-conditional terms - while(true) - { - bool changed=false; - // the 2nd loop - for(auto &x : s1) - { - // if ''x'' is atomic conditional term, there - // is no expansion - if(is_condition(x)) - { - s2.insert(x); - continue; - } - // otherwise, we apply the ''nested'' method to - // each of its operands - std::vector operands; - collect_operands(x, operands); - - for(std::size_t i=0; i res; - /** - * To expand an operand if it is not atomic, - * and label the ''changed'' flag; the resulted - * expansion of such an operand is stored in ''res''. - **/ - if(operands[i].id()==ID_not) - { - exprt no=operands[i].op0(); - if(!is_condition(no)) - { - changed=true; - std::set ctrl_no; - ctrl_no.insert(no); - res=collect_mcdc_controlling(ctrl_no); - } - } - else if(!is_condition(operands[i])) - { - changed=true; - std::set ctrl; - ctrl.insert(operands[i]); - res=collect_mcdc_controlling(ctrl); - } - - // To replace a non-atomic expr with its expansion - std::set co= - replacement_conjunction(res, operands, i); - s2.insert(co.begin(), co.end()); - if(!res.empty()) - break; - } - // if there is no change x.r.t current operands of ''x'', - // i.e., they are all atomic, we reserve ''x'' - if(!changed) - s2.insert(x); - } - // update ''s1'' and check if change happens - s1=s2; - if(!changed) - break; - s2.clear(); - } - - // The expansions of each ''src'' should be added into - // the ''result'' - result.insert(s1.begin(), s1.end()); - } - - return result; -} - -/// The sign of expr ''e'' within the super-expr ''E'' -/// \par parameters: E should be the pre-processed output by -/// ''collect_mcdc_controlling_nested'' -/// \return +1 : not negated -1 : negated -std::set sign_of_expr(const exprt &e, const exprt &E) -{ - std::set signs; - - // At fist, we pre-screen the case such that ''E'' - // is an atomic condition - if(is_condition(E)) - { - if(e==E) - signs.insert(+1); - return signs; - } - - // or, ''E'' is the negation of ''e''? - if(E.id()==ID_not) - { - if(e==E.op0()) - { - signs.insert(-1); - return signs; - } - } - - /** - * In the general case, we analyze each operand of ''E''. - **/ - std::vector ops; - collect_operands(E, ops); - for(auto &x : ops) - { - exprt y(x); - if(y==e) - signs.insert(+1); - else if(y.id()==ID_not) - { - y.make_not(); - if(y==e) - signs.insert(-1); - if(!is_condition(y)) - { - std::set re=sign_of_expr(e, y); - signs.insert(re.begin(), re.end()); - } - } - else if(!is_condition(y)) - { - std::set re=sign_of_expr(e, y); - signs.insert(re.begin(), re.end()); - } - } - - return signs; -} - -/// After the ''collect_mcdc_controlling_nested'', there can be the recurrence -/// of the same expr in the resulted set of exprs, and this method will remove -/// the repetitive ones. -void remove_repetition(std::set &exprs) -{ - // to obtain the set of atomic conditions - std::set conditions; - for(auto &x : exprs) - { - std::set new_conditions=collect_conditions(x); - conditions.insert(new_conditions.begin(), new_conditions.end()); - } - // exprt that contains multiple (inconsistent) signs should - // be removed - std::set new_exprs; - for(auto &x : exprs) - { - bool kept=true; - for(auto &c : conditions) - { - std::set signs=sign_of_expr(c, x); - if(signs.size()>1) - { - kept=false; - break; - } - } - if(kept) - new_exprs.insert(x); - } - exprs=new_exprs; - new_exprs.clear(); - - for(auto &x : exprs) - { - bool red=false; - /** - * To check if ''x'' is identical with some - * expr in ''new_exprs''. Two exprs ''x'' - * and ''y'' are identical iff they have the - * same sign for every atomic condition ''c''. - **/ - for(auto &y : new_exprs) - { - bool iden=true; - for(auto &c : conditions) - { - std::set signs1=sign_of_expr(c, x); - std::set signs2=sign_of_expr(c, y); - int s1=signs1.size(), s2=signs2.size(); - // it is easy to check non-equivalence; - if(s1!=s2) - { - iden=false; - break; - } - else - { - if(s1==0 && s2==0) - continue; - // it is easy to check non-equivalence - if(*(signs1.begin())!=*(signs2.begin())) - { - iden=false; - break; - } - } - } - /** - * If ''x'' is found identical w.r.t some - * expr in ''new_conditions, we label it - * and break. - **/ - if(iden) - { - red=true; - break; - } - } - // an expr is added into ''new_exprs'' - // if it is not found repetitive - if(!red) - new_exprs.insert(x); - } - - // update the original ''exprs'' - exprs=new_exprs; -} - -/// To evaluate the value of expr ''src'', according to the atomic expr values -bool eval_expr( - const std::map &atomic_exprs, - const exprt &src) -{ - std::vector operands; - collect_operands(src, operands); - // src is AND - if(src.id()==ID_and) - { - for(auto &x : operands) - if(!eval_expr(atomic_exprs, x)) - return false; - return true; - } - // src is OR - else if(src.id()==ID_or) - { - std::size_t fcount=0; - - for(auto &x : operands) - if(!eval_expr(atomic_exprs, x)) - fcount++; - - if(fcountsecond==+1) - return true; - else // if(atomic_exprs.find(src)->second==-1) - return false; - } -} - -/// To obtain values of atomic exprs within the super expr -std::map values_of_atomic_exprs( - const exprt &e, - const std::set &conditions) +#include +#include +#include + +#include "cover_basic_blocks.h" +#include "cover_filter.h" +#include "cover_instrument.h" + +/// Applies instrumenters to given goto program +/// \param goto_program: the goto program +/// \param instrumenters: the instrumenters +/// \param message_handler: a message handler +void instrument_cover_goals( + goto_programt &goto_program, + const cover_instrumenterst &instrumenters, + message_handlert &message_handler) { - std::map atomic_exprs; - for(auto &c : conditions) - { - std::set signs=sign_of_expr(c, e); - if(signs.empty()) - { - // ''c'' is not contained in ''e'' - atomic_exprs.insert(std::pair(c, 0)); - continue; - } - // we do not consider inconsistent expr ''e'' - if(signs.size()!=1) - continue; + cover_basic_blockst basic_blocks(goto_program); + basic_blocks.select_unique_java_bytecode_indices( + goto_program, message_handler); + basic_blocks.report_block_anomalies(goto_program, message_handler); - atomic_exprs.insert( - std::pair(c, *signs.begin())); - } - return atomic_exprs; + instrumenters(goto_program, basic_blocks); } -/// To check if the two input controlling exprs are mcdc pairs regarding an -/// atomic expr ''c''. A mcdc pair of (e1, e2) regarding ''c'' means that ''e1'' -/// and ''e2'' result in different ''decision'' values, and this is caused by -/// the different choice of ''c'' value. -bool is_mcdc_pair( - const exprt &e1, - const exprt &e2, - const exprt &c, - const std::set &conditions, - const exprt &decision) +/// Instruments goto program for a given coverage criterion +/// \param symbol_table: the symbol table +/// \param goto_program: the goto program +/// \param criterion: the coverage criterion +/// \param message_handler: a message handler +void instrument_cover_goals( + const symbol_tablet &symbol_table, + goto_programt &goto_program, + coverage_criteriont criterion, + message_handlert &message_handler) { - // An controlling expr cannot be mcdc pair of itself - if(e1==e2) - return false; - - // To obtain values of each atomic condition within ''e1'' - // and ''e2'' - std::map atomic_exprs_e1= - values_of_atomic_exprs(e1, conditions); - std::map atomic_exprs_e2= - values_of_atomic_exprs(e2, conditions); + goal_filterst goal_filters; + goal_filters.add(util_make_unique(message_handler)); - // the sign of ''c'' inside ''e1'' and ''e2'' - signed cs1=atomic_exprs_e1.find(c)->second; - signed cs2=atomic_exprs_e2.find(c)->second; - // a mcdc pair should both contain ''c'', i.e., sign=+1 or -1 - if(cs1==0 || cs2==0) - return false; + cover_instrumenterst instrumenters; + instrumenters.add_from_criterion(criterion, symbol_table, goal_filters); - // A mcdc pair regarding an atomic expr ''c'' - // should have different values of ''c'' - if(cs1==cs2) - return false; - - // A mcdc pair should result in different ''decision'' - if(eval_expr(atomic_exprs_e1, decision)== - eval_expr(atomic_exprs_e2, decision)) - return false; - - /** - * A mcdc pair of controlling exprs regarding ''c'' - * can have different values for only one atomic - * expr, i.e., ''c''. Otherwise, they are not - * a mcdc pair. - **/ - int diff_count=0; - auto e1_it=atomic_exprs_e1.begin(); - auto e2_it=atomic_exprs_e2.begin(); - while(e1_it!=atomic_exprs_e1.end()) - { - if(e1_it->second!=e2_it->second) - diff_count++; - if(diff_count>1) - break; - e1_it++; - e2_it++; - } - - if(diff_count==1) - return true; - else - return false; -} - -/// To check if we can find the mcdc pair of the input ''expr_set'' regarding -/// the atomic expr ''c'' -bool has_mcdc_pair( - const exprt &c, - const std::set &expr_set, - const std::set &conditions, - const exprt &decision) -{ - for(auto y1 : expr_set) - { - for(auto y2 : expr_set) - { - if(is_mcdc_pair(y1, y2, c, conditions, decision)) - { - return true; - } - } - } - return false; + instrument_cover_goals(goto_program, instrumenters, message_handler); } -/// This method minimizes the controlling conditions for mcdc coverage. The -/// minimum is in a sense that by deleting any controlling condition in the set, -/// the mcdc coverage for the decision will be not complete. -/// \par parameters: The input ''controlling'' should have been processed by -/// ''collect_mcdc_controlling_nested'' and -/// ''remove_repetition'' -void minimize_mcdc_controlling( - std::set &controlling, - const exprt &decision) +/// Create and add an instrumenter based on the given criterion +/// \param criterion: the coverage criterion +/// \param symbol_table: the symbol table +/// \param goal_filters: goal filters to discard certain goals +void cover_instrumenterst::add_from_criterion( + coverage_criteriont criterion, + const symbol_tablet &symbol_table, + const goal_filterst &goal_filters) { - // to obtain the set of atomic conditions - std::set conditions; - for(auto &x : controlling) - { - std::set new_conditions=collect_conditions(x); - conditions.insert(new_conditions.begin(), new_conditions.end()); - } - - while(true) - { - std::set new_controlling; - bool ctrl_update=false; - /** - * Iteratively, we test that after removing an item ''x'' - * from the ''controlling'', can a complete mcdc coverage - * over ''decision'' still be reserved? - * - * If yes, we update ''controlling'' with the - * ''new_controlling'' without ''x''; otherwise, we should - * keep ''x'' within ''controlling''. - * - * If in the end all elements ''x'' in ''controlling'' are - * reserved, this means that current ''controlling'' set is - * minimum and the ''while'' loop should be broken out of. - * - * Note: implementation here for the above procedure is - * not (meant to be) optimal. - **/ - for(auto &x : controlling) - { - // To create a new ''controlling'' set without ''x'' - new_controlling.clear(); - for(auto &y : controlling) - if(y!=x) - new_controlling.insert(y); - - bool removing_x=true; - // For each atomic expr condition ''c'', to check if its is - // covered by at least a mcdc pair. - for(auto &c : conditions) - { - bool cOK= - has_mcdc_pair(c, new_controlling, conditions, decision); - /** - * If there is no mcdc pair for an atomic condition ''c'', - * then ''x'' should not be removed from the original - * ''controlling'' set - **/ - if(!cOK) - { - removing_x=false; - break; - } - } - - // If ''removing_x'' is valid, it is safe to remove ''x'' - // from the original ''controlling'' - if(removing_x) - { - ctrl_update=true; - break; - } - } - // Update ''controlling'' or break the while loop - if(ctrl_update) - { - controlling=new_controlling; - } - else - break; + switch(criterion) + { + case coverage_criteriont::LOCATION: + instrumenters.push_back( + util_make_unique( + symbol_table, goal_filters)); + break; + case coverage_criteriont::BRANCH: + instrumenters.push_back( + util_make_unique(symbol_table, goal_filters)); + break; + case coverage_criteriont::DECISION: + instrumenters.push_back( + util_make_unique( + symbol_table, goal_filters)); + break; + case coverage_criteriont::CONDITION: + instrumenters.push_back( + util_make_unique( + symbol_table, goal_filters)); + break; + case coverage_criteriont::PATH: + instrumenters.push_back( + util_make_unique(symbol_table, goal_filters)); + break; + case coverage_criteriont::MCDC: + instrumenters.push_back( + util_make_unique(symbol_table, goal_filters)); + break; + case coverage_criteriont::ASSERTION: + instrumenters.push_back( + util_make_unique( + symbol_table, goal_filters)); + break; + case coverage_criteriont::COVER: + instrumenters.push_back( + util_make_unique(symbol_table, goal_filters)); } } -void collect_decisions_rec(const exprt &src, std::set &dest) +/// Parses a coverage criterion +/// \param criterion_string: a string +/// \return a coverage criterion or throws an exception +coverage_criteriont +parse_coverage_criterion(const std::string &criterion_string) { - if(src.id()==ID_address_of) - { - return; - } - - if(src.type().id()==ID_bool) - { - if(src.is_constant()) - { - // ignore me - } - else if(src.id()==ID_not) - { - collect_decisions_rec(src.op0(), dest); - } - else - { - dest.insert(src); - } - } + coverage_criteriont c; + + if(criterion_string == "assertion" || criterion_string == "assertions") + c = coverage_criteriont::ASSERTION; + else if(criterion_string == "path" || criterion_string == "paths") + c = coverage_criteriont::PATH; + else if(criterion_string == "branch" || criterion_string == "branches") + c = coverage_criteriont::BRANCH; + else if(criterion_string == "location" || criterion_string == "locations") + c = coverage_criteriont::LOCATION; + else if(criterion_string == "decision" || criterion_string == "decisions") + c = coverage_criteriont::DECISION; + else if(criterion_string == "condition" || criterion_string == "conditions") + c = coverage_criteriont::CONDITION; + else if(criterion_string == "mcdc") + c = coverage_criteriont::MCDC; + else if(criterion_string == "cover") + c = coverage_criteriont::COVER; else { - for(const auto &op : src.operands()) - collect_decisions_rec(op, dest); - } -} - -std::set collect_decisions(const exprt &src) -{ - std::set result; - collect_decisions_rec(src, result); - return result; -} - -std::set collect_decisions(const goto_programt::const_targett t) -{ - switch(t->type) - { - case GOTO: - case ASSERT: - return collect_decisions(t->guard); - - case ASSIGN: - case FUNCTION_CALL: - return collect_decisions(t->code); - - default: - { - } + std::stringstream s; + s << "unknown coverage criterion " << '\'' << criterion_string << '\''; + throw s.str(); } - return std::set(); + return c; } -void instrument_cover_goals( - const symbol_tablet &symbol_table, - goto_programt &goto_program, - coverage_criteriont criterion, - message_handlert &message_handler, - bool function_only) -{ - instrument_cover_goals( - symbol_table, - goto_program, - criterion, - message_handler, - function_only, - false); -} - -/// Call a goto_program trivial unless it has: * Any declarations * At least 2 -/// branches * At least 5 assignments -/// \par parameters: Program `goto_program` -/// \return Returns true if trivial -bool program_is_trivial(const goto_programt &goto_program) +/// Parses coverage-related command line options +/// \param cmdline: the command line +/// \param options: the options +void parse_cover_options(const cmdlinet &cmdline, optionst &options) { - unsigned long count_assignments=0, count_goto=0; - forall_goto_program_instructions(i_it, goto_program) - { - if(i_it->is_goto()) - { - if((++count_goto)>=2) - return false; - } - else if(i_it->is_assign()) - { - if((++count_assignments)>=5) - return false; - } - else if(i_it->is_decl()) - return false; - } - - return true; + options.set_option("cover", cmdline.get_values("cover")); + std::string cover_include_pattern = + cmdline.get_value("cover-include-pattern"); + if(cmdline.isset("cover-function-only")) + { + std::regex special_characters( + "\\.|\\\\|\\*|\\+|\\?|\\{|\\}|\\[|\\]|\\(|\\)|\\^|\\$|\\|"); + cover_include_pattern = + ".*" + std::regex_replace(config.main, special_characters, "\\$&") + ".*"; + } + options.set_option("cover-include-pattern", cover_include_pattern); + options.set_option("no-trivial-tests", cmdline.isset("no-trivial-tests")); + options.set_option( + "cover-traces-must-terminate", + cmdline.isset("cover-traces-must-terminate")); } +/// Applies instrumenters to given goto functions +/// \param goto_functions: the goto functions +/// \param instrumenters: the instrumenters +/// \param function_filters: function filters to discard certain functions +/// \param message_handler: a message handler void instrument_cover_goals( - const symbol_tablet &symbol_table, - goto_programt &goto_program, - coverage_criteriont criterion, - message_handlert &message_handler, - bool function_only, - bool ignore_trivial) -{ - // exclude trivial coverage goals of a goto program - if(ignore_trivial && program_is_trivial(goto_program)) - return; - - // ignore if built-in library - if(!goto_program.instructions.empty() && - goto_program.instructions.front().source_location.is_built_in()) - return; - - const namespacet ns(symbol_table); - basic_blockst basic_blocks(goto_program); - basic_blocks.select_unique_java_bytecode_indices( - goto_program, message_handler); - basic_blocks.report_block_anomalies(goto_program, message_handler); - - const irep_idt coverage_criterion=as_string(criterion); - const irep_idt property_class="coverage"; - - Forall_goto_program_instructions(i_it, goto_program) - { - std::string curr_function=id2string(i_it->function); - - // if the --cover-function-only flag is set, then we only add coverage - // instrumentation for the entry function - bool cover_curr_function= - !function_only || - curr_function.find(config.main)!=std::string::npos; - - switch(criterion) - { - case coverage_criteriont::ASSERTION: - // turn into 'assert(false)' to avoid simplification - if(i_it->is_assert() && cover_curr_function) - { - i_it->guard=false_exprt(); - i_it->source_location.set(ID_coverage_criterion, coverage_criterion); - i_it->source_location.set_property_class(property_class); - i_it->source_location.set_function(i_it->function); - } - break; - - case coverage_criteriont::COVER: - // turn __CPROVER_cover(x) into 'assert(!x)' - if(i_it->is_function_call() && cover_curr_function) - { - const code_function_callt &code_function_call= - to_code_function_call(i_it->code); - if(code_function_call.function().id()==ID_symbol && - to_symbol_expr(code_function_call.function()).get_identifier()== - "__CPROVER_cover" && - code_function_call.arguments().size()==1) - { - const exprt c=code_function_call.arguments()[0]; - std::string comment="condition `"+from_expr(ns, "", c)+"'"; - i_it->guard=not_exprt(c); - i_it->type=ASSERT; - i_it->code.clear(); - i_it->source_location.set_comment(comment); - i_it->source_location.set(ID_coverage_criterion, coverage_criterion); - i_it->source_location.set_property_class(property_class); - i_it->source_location.set_function(i_it->function); - } - } - else if(i_it->is_assert()) - i_it->make_skip(); - break; - - case coverage_criteriont::LOCATION: - if(i_it->is_assert()) - i_it->make_skip(); - - { - unsigned block_nr=basic_blocks.block_of(i_it); - goto_programt::const_targett in_t=basic_blocks.instruction_of(block_nr); - // we only instrument the selected instruction - if(in_t==i_it) - { - std::string b=std::to_string(block_nr+1); // start with 1 - std::string id=id2string(i_it->function)+"#"+b; - source_locationt source_location= - basic_blocks.source_location_of(block_nr); - - // check whether the current goal needs to be covered - if( - !source_location.get_file().empty() && - !source_location.is_built_in() && cover_curr_function) - { - std::string comment="block "+b; - const irep_idt function=i_it->function; - goto_program.insert_before_swap(i_it); - i_it->make_assertion(false_exprt()); - i_it->source_location=source_location; - i_it->source_location.set_comment(comment); - i_it->source_location.set( - ID_coverage_criterion, coverage_criterion); - i_it->source_location.set_property_class(property_class); - i_it->source_location.set_function(function); - i_it->function=function; - i_it++; - } - } - } - break; - - case coverage_criteriont::BRANCH: - if(i_it->is_assert()) - i_it->make_skip(); - - if(i_it==goto_program.instructions.begin() && - cover_curr_function) - { - // we want branch coverage to imply 'entry point of function' - // coverage - std::string comment="entry point"; - - source_locationt source_location=i_it->source_location; - - goto_programt::targett t=goto_program.insert_before(i_it); - t->make_assertion(false_exprt()); - t->source_location=source_location; - t->source_location.set_comment(comment); - t->source_location.set(ID_coverage_criterion, coverage_criterion); - t->source_location.set_property_class(property_class); - t->source_location.set_function(i_it->function); - t->function=i_it->function; - } - - if(i_it->is_goto() && !i_it->guard.is_true() && cover_curr_function && - !i_it->source_location.is_built_in()) - { - std::string b= - std::to_string(basic_blocks.block_of(i_it)+1); // start with 1 - std::string true_comment="block "+b+" branch true"; - std::string false_comment="block "+b+" branch false"; - - exprt guard=i_it->guard; - const irep_idt function=i_it->function; - source_locationt source_location=i_it->source_location; - source_location.set_function(function); - - goto_program.insert_before_swap(i_it); - i_it->make_assertion(not_exprt(guard)); - i_it->source_location=source_location; - i_it->source_location.set_comment(true_comment); - i_it->source_location.set(ID_coverage_criterion, coverage_criterion); - i_it->source_location.set_property_class(property_class); - i_it->function=function; - - goto_program.insert_before_swap(i_it); - i_it->make_assertion(guard); - i_it->source_location=source_location; - i_it->source_location.set_comment(false_comment); - i_it->source_location.set(ID_coverage_criterion, coverage_criterion); - i_it->source_location.set_property_class(property_class); - i_it->function=function; - - i_it++; - i_it++; - } - break; - - case coverage_criteriont::CONDITION: - if(i_it->is_assert()) - i_it->make_skip(); - - // Conditions are all atomic predicates in the programs. - if(cover_curr_function && !i_it->source_location.is_built_in()) - { - const std::set conditions=collect_conditions(i_it); - - const source_locationt source_location=i_it->source_location; - - for(const auto &c : conditions) - { - const std::string c_string=from_expr(ns, "", c); - - const std::string comment_t="condition `"+c_string+"' true"; - const irep_idt function=i_it->function; - goto_program.insert_before_swap(i_it); - i_it->make_assertion(c); - i_it->source_location=source_location; - i_it->source_location.set_comment(comment_t); - i_it->source_location.set(ID_coverage_criterion, coverage_criterion); - i_it->source_location.set_property_class(property_class); - i_it->source_location.set_function(function); - i_it->function=function; - - const std::string comment_f="condition `"+c_string+"' false"; - goto_program.insert_before_swap(i_it); - i_it->make_assertion(not_exprt(c)); - i_it->source_location=source_location; - i_it->source_location.set_comment(comment_f); - i_it->source_location.set(ID_coverage_criterion, coverage_criterion); - i_it->source_location.set_property_class(property_class); - i_it->source_location.set_function(function); - i_it->function=function; - } - - for(std::size_t i=0; iis_assert()) - i_it->make_skip(); - - // Decisions are maximal Boolean combinations of conditions. - if(cover_curr_function && !i_it->source_location.is_built_in()) - { - const std::set decisions=collect_decisions(i_it); - - const source_locationt source_location=i_it->source_location; - - for(const auto &d : decisions) - { - const std::string d_string=from_expr(ns, "", d); - - const std::string comment_t="decision `"+d_string+"' true"; - const irep_idt function=i_it->function; - goto_program.insert_before_swap(i_it); - i_it->make_assertion(d); - i_it->source_location=source_location; - i_it->source_location.set_comment(comment_t); - i_it->source_location.set(ID_coverage_criterion, coverage_criterion); - i_it->source_location.set_property_class(property_class); - i_it->source_location.set_function(function); - i_it->function=function; - - const std::string comment_f="decision `"+d_string+"' false"; - goto_program.insert_before_swap(i_it); - i_it->make_assertion(not_exprt(d)); - i_it->source_location=source_location; - i_it->source_location.set_comment(comment_f); - i_it->source_location.set(ID_coverage_criterion, coverage_criterion); - i_it->source_location.set_property_class(property_class); - i_it->source_location.set_function(function); - i_it->function=function; - } - - for(std::size_t i=0; iis_assert()) - i_it->make_skip(); - - // 1. Each entry and exit point is invoked - // 2. Each decision takes every possible outcome - // 3. Each condition in a decision takes every possible outcome - // 4. Each condition in a decision is shown to independently - // affect the outcome of the decision. - if(cover_curr_function && !i_it->source_location.is_built_in()) - { - const std::set conditions=collect_conditions(i_it); - const std::set decisions=collect_decisions(i_it); - - std::set both; - std::set_union( - conditions.begin(), - conditions.end(), - decisions.begin(), - decisions.end(), - inserter(both, both.end())); - - const source_locationt source_location=i_it->source_location; - - for(const auto &p : both) - { - bool is_decision=decisions.find(p)!=decisions.end(); - bool is_condition=conditions.find(p)!=conditions.end(); - - std::string description= - (is_decision && is_condition)?"decision/condition": - is_decision?"decision":"condition"; - - std::string p_string=from_expr(ns, "", p); - - std::string comment_t=description+" `"+p_string+"' true"; - const irep_idt function=i_it->function; - goto_program.insert_before_swap(i_it); - // i_it->make_assertion(p); - i_it->make_assertion(not_exprt(p)); - i_it->source_location=source_location; - i_it->source_location.set_comment(comment_t); - i_it->source_location.set(ID_coverage_criterion, coverage_criterion); - i_it->source_location.set_property_class(property_class); - i_it->source_location.set_function(function); - i_it->function=function; - - std::string comment_f=description+" `"+p_string+"' false"; - goto_program.insert_before_swap(i_it); - // i_it->make_assertion(not_exprt(p)); - i_it->make_assertion(p); - i_it->source_location=source_location; - i_it->source_location.set_comment(comment_f); - i_it->source_location.set(ID_coverage_criterion, coverage_criterion); - i_it->source_location.set_property_class(property_class); - i_it->source_location.set_function(function); - i_it->function=function; - } - - std::set controlling; - // controlling=collect_mcdc_controlling(decisions); - controlling=collect_mcdc_controlling_nested(decisions); - remove_repetition(controlling); - // for now, we restrict to the case of a single ''decision''; - // however, this is not true, e.g., ''? :'' operator. - INVARIANT(!decisions.empty(), "There must be at least one decision"); - minimize_mcdc_controlling(controlling, *decisions.begin()); - - for(const auto &p : controlling) - { - std::string p_string=from_expr(ns, "", p); - - std::string description= - "MC/DC independence condition `"+p_string+"'"; - - const irep_idt function=i_it->function; - goto_program.insert_before_swap(i_it); - i_it->make_assertion(not_exprt(p)); - // i_it->make_assertion(p); - i_it->source_location=source_location; - i_it->source_location.set_comment(description); - i_it->source_location.set(ID_coverage_criterion, coverage_criterion); - i_it->source_location.set_property_class(property_class); - i_it->source_location.set_function(function); - i_it->function=function; - } - - for(std::size_t i=0; iis_assert()) - i_it->make_skip(); - break; - - default: - { - } - } - } -} - -void instrument_cover_goals( - const symbol_tablet &symbol_table, goto_functionst &goto_functions, - coverage_criteriont criterion, - message_handlert &message_handler, - bool function_only, - bool ignore_trivial, - const std::string &cover_include_pattern) + const cover_instrumenterst &instrumenters, + const function_filterst &function_filters, + message_handlert &message_handler) { - std::smatch string_matcher; - std::regex regex_matcher(cover_include_pattern); - bool do_include_pattern_match=!cover_include_pattern.empty(); - Forall_goto_functions(f_it, goto_functions) { - if(f_it->first==goto_functions.entry_point() || - f_it->first==(CPROVER_PREFIX "initialize") || - f_it->second.is_hidden() || - (do_include_pattern_match && - !std::regex_match( - id2string(f_it->first), string_matcher, regex_matcher)) || - // ignore Java array built-ins - has_prefix(id2string(f_it->first), "java::array")) + if(!function_filters(f_it->first, f_it->second)) continue; - instrument_cover_goals( - symbol_table, - f_it->second.body, - criterion, - message_handler, - function_only, - ignore_trivial); + instrument_cover_goals(f_it->second.body, instrumenters, message_handler); } } -void instrument_cover_goals( - const symbol_tablet &symbol_table, - goto_functionst &goto_functions, - coverage_criteriont criterion, - message_handlert &message_handler, - bool function_only) -{ - instrument_cover_goals( - symbol_table, - goto_functions, - criterion, - message_handler, - function_only, - false, - ""); -} - +/// Instruments goto functions based on given command line options +/// \param options: the options +/// \param symbol_table: the symbol table +/// \param goto_functions: the goto functions +/// \param message_handler: a message handler bool instrument_cover_goals( - const cmdlinet &cmdline, + const optionst &options, const symbol_tablet &symbol_table, goto_functionst &goto_functions, message_handlert &message_handler) { messaget msg(message_handler); - std::list criteria_strings=cmdline.get_values("cover"); - std::set criteria; + + function_filterst function_filters; + function_filters.add( + util_make_unique(message_handler)); + + goal_filterst goal_filters; + goal_filters.add(util_make_unique(message_handler)); + + cover_instrumenterst instrumenters; + + optionst::value_listt criteria_strings = options.get_list_option("cover"); bool keep_assertions=false; for(const auto &criterion_string : criteria_strings) { - coverage_criteriont c; - - if(criterion_string=="assertion" || criterion_string=="assertions") + try { - keep_assertions=true; - c=coverage_criteriont::ASSERTION; + coverage_criteriont c = parse_coverage_criterion(criterion_string); + + if(c == coverage_criteriont::ASSERTION) + keep_assertions = true; + + instrumenters.add_from_criterion(c, symbol_table, goal_filters); } - else if(criterion_string=="path" || criterion_string=="paths") - c=coverage_criteriont::PATH; - else if(criterion_string=="branch" || criterion_string=="branches") - c=coverage_criteriont::BRANCH; - else if(criterion_string=="location" || criterion_string=="locations") - c=coverage_criteriont::LOCATION; - else if(criterion_string=="decision" || criterion_string=="decisions") - c=coverage_criteriont::DECISION; - else if(criterion_string=="condition" || criterion_string=="conditions") - c=coverage_criteriont::CONDITION; - else if(criterion_string=="mcdc") - c=coverage_criteriont::MCDC; - else if(criterion_string=="cover") - c=coverage_criteriont::COVER; - else + catch(const std::string &e) { - msg.error() << "unknown coverage criterion " - << '\'' << criterion_string << '\'' - << messaget::eom; + msg.error() << e << messaget::eom; return true; } - - criteria.insert(c); } if(keep_assertions && criteria_strings.size()>1) @@ -1575,21 +252,29 @@ bool instrument_cover_goals( } } - msg.status() << "Instrumenting coverage goals" << messaget::eom; - - for(const auto &criterion : criteria) + // cover entry point function only + std::string cover_include_pattern = + options.get_option("cover-include-pattern"); + if(!cover_include_pattern.empty()) { - instrument_cover_goals( - symbol_table, - goto_functions, - criterion, - message_handler, - cmdline.isset("cover-function-only"), - cmdline.isset("no-trivial-tests"), - cmdline.get_value("cover-include-pattern")); + function_filters.add( + util_make_unique( + message_handler, cover_include_pattern)); } - if(cmdline.isset("cover-traces-must-terminate")) + if(options.get_bool_option("no-trivial-tests")) + function_filters.add( + util_make_unique(message_handler)); + + msg.status() << "Instrumenting coverage goals" << messaget::eom; + + instrument_cover_goals( + goto_functions, instrumenters, function_filters, message_handler); + + function_filters.report_anomalies(); + goal_filters.report_anomalies(); + + if(options.get_bool_option("cover-traces-must-terminate")) { // instrument an additional goal in CPROVER_START. This will rephrase // the reachability problem by asking BMC to provide a solution that @@ -1599,35 +284,28 @@ bool instrument_cover_goals( if(sf_it==goto_functions.function_map.end()) { msg.error() << "cover-traces-must-terminate: invalid entry point [" - << goto_functions.entry_point() << "]" - << messaget::eom; + << goto_functions.entry_point() << "]" << messaget::eom; return true; } - auto if_it=sf_it->second.body.instructions.end(); - while(!if_it->is_function_call()) - if_it--; - if_it++; - const std::string &comment= - "additional goal to ensure complete trace coverage."; - sf_it->second.body.insert_before_swap(if_it); - if_it->make_assertion(false_exprt()); - if_it->source_location.set_comment(comment); - if_it->source_location.set_property_class("reachability_constraint"); - if_it->source_location.set_function(goto_functions.entry_point()); - if_it->function=goto_functions.entry_point(); + + cover_instrument_end_of_function(sf_it->first, sf_it->second.body); } goto_functions.update(); return false; } +/// Instruments a goto model based on given command line options +/// \param options: the options +/// \param goto_model: the goto model +/// \param message_handler: a message handler bool instrument_cover_goals( - const cmdlinet &cmdline, + const optionst &options, goto_modelt &goto_model, message_handlert &message_handler) { return instrument_cover_goals( - cmdline, + options, goto_model.symbol_table, goto_model.goto_functions, message_handler); diff --git a/src/goto-instrument/cover.h b/src/goto-instrument/cover.h index 158b50b5f5e..d8dd994e700 100644 --- a/src/goto-instrument/cover.h +++ b/src/goto-instrument/cover.h @@ -15,55 +15,45 @@ Date: May 2016 #define CPROVER_GOTO_INSTRUMENT_COVER_H #include -#include class message_handlert; -class messaget; +class cmdlinet; +class optionst; enum class coverage_criteriont { - LOCATION, BRANCH, DECISION, CONDITION, - PATH, MCDC, ASSERTION, COVER }; + LOCATION, + BRANCH, + DECISION, + CONDITION, + PATH, + MCDC, + ASSERTION, + COVER // __CPROVER_cover(x) annotations +}; void instrument_cover_goals( const symbol_tablet &, goto_functionst &, coverage_criteriont, - message_handlert &message_handler, - bool function_only=false); + message_handlert &message_handler); void instrument_cover_goals( const symbol_tablet &, goto_programt &, coverage_criteriont, - message_handlert &message_handler, - bool function_only=false); + message_handlert &message_handler); -void instrument_cover_goals( - const symbol_tablet &, - goto_functionst &, - coverage_criteriont, - message_handlert &message_handler, - bool function_only=false, - bool ignore_trivial=false, - const std::string &cover_inclue_pattern=""); - -void instrument_cover_goals( - const symbol_tablet &, - goto_programt &, - coverage_criteriont, - message_handlert &message_handler, - bool function_only=false, - bool ignore_trivial=false); +void parse_cover_options(const cmdlinet &, optionst &); bool instrument_cover_goals( - const cmdlinet &, + const optionst &, const symbol_tablet &, goto_functionst &, message_handlert &); bool instrument_cover_goals( - const cmdlinet &, + const optionst &, goto_modelt &, message_handlert &); diff --git a/src/goto-instrument/cover_basic_blocks.cpp b/src/goto-instrument/cover_basic_blocks.cpp new file mode 100644 index 00000000000..87a40c0708f --- /dev/null +++ b/src/goto-instrument/cover_basic_blocks.cpp @@ -0,0 +1,229 @@ +/*******************************************************************\ + +Module: Coverage Instrumentation + +Author: Peter Schrammel + +\*******************************************************************/ + +/// \file +/// Basic blocks detection for Coverage Instrumentation + +#include "cover_basic_blocks.h" + +#include +#include +#include + +cover_basic_blockst::cover_basic_blockst(const goto_programt &_goto_program) +{ + bool next_is_target = true; + unsigned current_block = 0; + + forall_goto_program_instructions(it, _goto_program) + { + // Is it a potential beginning of a block? + if(next_is_target || it->is_target()) + { + // We keep the block number if this potential block + // is a continuation of a previous block through + // unconditional forward gotos; otherwise we increase the + // block number. + bool increase_block_nr = true; + if(it->incoming_edges.size() == 1) + { + goto_programt::targett in_t = *it->incoming_edges.begin(); + if( + in_t->is_goto() && !in_t->is_backwards_goto() && + in_t->guard.is_true()) + { + current_block = block_map[in_t]; + increase_block_nr = false; + } + } + if(increase_block_nr) + { + block_infos.push_back(block_infot()); + block_infos.back().representative_inst = it; + block_infos.back().source_location = source_locationt::nil(); + current_block = block_infos.size() - 1; + } + } + + INVARIANT( + current_block < block_infos.size(), "current block number out of range"); + block_infot &block_info = block_infos.at(current_block); + + block_map[it] = current_block; + + // update lines belonging to block + const irep_idt &line = it->source_location.get_line(); + if(!line.empty()) + block_info.lines.insert(unsafe_string2unsigned(id2string(line))); + + // set representative program location to instrument + if( + !it->source_location.is_nil() && + !it->source_location.get_file().empty() && + !it->source_location.get_line().empty() && + block_info.source_location.is_nil()) + { + block_info.representative_inst = it; // update + block_info.source_location = it->source_location; + } + + next_is_target = +#if 0 + // Disabled for being too messy + it->is_goto() || it->is_function_call() || it->is_assume(); +#else + it->is_goto() || it->is_function_call(); +#endif + } + + for(auto &block_info : block_infos) + update_covered_lines(block_info); +} + +unsigned cover_basic_blockst::block_of(goto_programt::const_targett t) const +{ + block_mapt::const_iterator it = block_map.find(t); + INVARIANT(it != block_map.end(), "instruction must be part of a block"); + return it->second; +} + +goto_programt::const_targett +cover_basic_blockst::instruction_of(unsigned block_nr) const +{ + INVARIANT(block_nr < block_infos.size(), "block number out of range"); + return block_infos.at(block_nr).representative_inst; +} + +const source_locationt & +cover_basic_blockst::source_location_of(unsigned block_nr) const +{ + INVARIANT(block_nr < block_infos.size(), "block number out of range"); + return block_infos.at(block_nr).source_location; +} + +void cover_basic_blockst::select_unique_java_bytecode_indices( + const goto_programt &goto_program, + message_handlert &message_handler) +{ + messaget msg(message_handler); + std::set blocks_seen; + std::set bytecode_indices_seen; + + forall_goto_program_instructions(it, goto_program) + { + unsigned block_nr = block_of(it); + if(blocks_seen.find(block_nr) != blocks_seen.end()) + continue; + + INVARIANT(block_nr < block_infos.size(), "block number out of range"); + block_infot &block_info = block_infos.at(block_nr); + if(block_info.representative_inst == goto_program.instructions.end()) + { + if(!it->source_location.get_java_bytecode_index().empty()) + { + // search for a representative + if( + bytecode_indices_seen + .insert(it->source_location.get_java_bytecode_index()) + .second) + { + block_info.representative_inst = it; + block_info.source_location = it->source_location; + update_covered_lines(block_info); + blocks_seen.insert(block_nr); + msg.debug() << it->function << " block " << (block_nr + 1) + << ": location " << it->location_number + << ", bytecode-index " + << it->source_location.get_java_bytecode_index() + << " selected for instrumentation." << messaget::eom; + } + } + } + else if(it == block_info.representative_inst) + { + // check the existing representative + if(!it->source_location.get_java_bytecode_index().empty()) + { + if( + bytecode_indices_seen + .insert(it->source_location.get_java_bytecode_index()) + .second) + { + blocks_seen.insert(block_nr); + } + else + { + // clash, reset to search for a new one + block_info.representative_inst = goto_program.instructions.end(); + block_info.source_location = source_locationt::nil(); + msg.debug() << it->function << " block " << (block_nr + 1) + << ", location " << it->location_number + << ": bytecode-index " + << it->source_location.get_java_bytecode_index() + << " already instrumented." + << " Searching for alternative instruction" + << " to instrument." << messaget::eom; + } + } + } + } +} + +void cover_basic_blockst::report_block_anomalies( + const goto_programt &goto_program, + message_handlert &message_handler) +{ + messaget msg(message_handler); + std::set blocks_seen; + forall_goto_program_instructions(it, goto_program) + { + unsigned block_nr = block_of(it); + const block_infot &block_info = block_infos.at(block_nr); + + if( + blocks_seen.insert(block_nr).second && + block_info.representative_inst == goto_program.instructions.end()) + { + msg.warning() << "Ignoring block " << (block_nr + 1) << " location " + << it->location_number << " " << it->source_location + << " (bytecode-index already instrumented)" + << messaget::eom; + } + else if( + block_info.representative_inst == it && + block_info.source_location.is_nil()) + { + msg.warning() << "Ignoring block " << (block_nr + 1) << " location " + << it->location_number << " " << it->function + << " (missing source location)" << messaget::eom; + } + // The location numbers printed here are those + // before the coverage instrumentation. + } +} + +void cover_basic_blockst::output(std::ostream &out) const +{ + for(const auto &block_pair : block_map) + out << block_pair.first->source_location << " -> " << block_pair.second + << '\n'; +} + +void cover_basic_blockst::update_covered_lines(block_infot &block_info) +{ + if(block_info.source_location.is_nil()) + return; + + const auto &cover_set = block_info.lines; + INVARIANT(!cover_set.empty(), "covered lines set must not be empty"); + std::vector line_list(cover_set.begin(), cover_set.end()); + + format_number_ranget format_lines; + std::string covered_lines = format_lines(line_list); + block_info.source_location.set_basic_block_covered_lines(covered_lines); +} diff --git a/src/goto-instrument/cover_basic_blocks.h b/src/goto-instrument/cover_basic_blocks.h new file mode 100644 index 00000000000..daab1ab0447 --- /dev/null +++ b/src/goto-instrument/cover_basic_blocks.h @@ -0,0 +1,87 @@ +/*******************************************************************\ + +Module: Coverage Instrumentation + +Author: Daniel Kroening + +\*******************************************************************/ + +/// \file +/// Basic blocks detection for Coverage Instrumentation + +#ifndef CPROVER_GOTO_INSTRUMENT_COVER_BASIC_BLOCKS_H +#define CPROVER_GOTO_INSTRUMENT_COVER_BASIC_BLOCKS_H + +#include + +#include + +class message_handlert; + +class cover_basic_blockst +{ +public: + explicit cover_basic_blockst(const goto_programt &_goto_program); + + /// \param t a goto instruction + /// \return the block number of the block + /// the given goto instruction is part of + unsigned block_of(goto_programt::const_targett t) const; + + /// \param block_nr a block number + /// \return the instruction selected for + /// instrumentation representative of the given block + goto_programt::const_targett instruction_of(unsigned block_nr) const; + + /// \param block_nr a block number + /// \return the source location selected for + /// instrumentation representative of the given block + const source_locationt &source_location_of(unsigned block_nr) const; + + /// Select an instruction to be instrumented for each basic block such that + /// the java bytecode indices for each basic block is unique + /// \param goto_program The goto program + /// \param message_handler The message handler + void select_unique_java_bytecode_indices( + const goto_programt &goto_program, + message_handlert &message_handler); + + /// Output warnings about ignored blocks + /// \param goto_program The goto program + /// \param message_handler The message handler + void report_block_anomalies( + const goto_programt &goto_program, + message_handlert &message_handler); + + /// Outputs the list of blocks + void output(std::ostream &out) const; + +protected: + // map program locations to block numbers + typedef std::map block_mapt; + block_mapt block_map; + + struct block_infot + { + /// the program location to instrument for this block + goto_programt::const_targett representative_inst; + + /// the source location representative for this block + // (we need a separate copy of source locations because we attach + // the line number ranges to them) + source_locationt source_location; + + // map block numbers to source code locations + /// the set of lines belonging to this block + std::unordered_set lines; + }; + + typedef std::vector block_infost; + block_infost block_infos; + + /// create list of covered lines as CSV string and set as property of source + /// location of basic block, compress to ranges if applicable + void update_covered_lines(block_infot &block_info); +}; + +#endif // CPROVER_GOTO_INSTRUMENT_COVER_BASIC_BLOCKS_H diff --git a/src/goto-instrument/cover_filter.cpp b/src/goto-instrument/cover_filter.cpp new file mode 100644 index 00000000000..ee1f0859dfa --- /dev/null +++ b/src/goto-instrument/cover_filter.cpp @@ -0,0 +1,108 @@ +/*******************************************************************\ + +Module: Coverage Instrumentation + +Author: Peter Schrammel + +\*******************************************************************/ + +/// \file +/// Filters for the Coverage Instrumentation + +#include "cover_filter.h" + +#include + +#include + +/// Filter out functions that are not considered provided by the user +/// \param identifier: a function name +/// \param goto_function: a goto function +/// \return: returns true if function is considered user-provided +bool internal_functions_filtert::operator()( + const irep_idt &identifier, + const goto_functionst::goto_functiont &goto_function) const +{ + if(identifier == goto_functionst::entry_point()) + return false; + + if(identifier == (CPROVER_PREFIX "initialize")) + return false; + + if(goto_function.is_hidden()) + return false; + + // ignore Java built-ins + if( + has_prefix(id2string(identifier), "java::array[") || + has_prefix(id2string(identifier), "java::org.cprover") || + has_prefix(id2string(identifier), "java::java.")) + return false; + + // ignore if built-in library + if( + !goto_function.body.instructions.empty() && + goto_function.body.instructions.front().source_location.is_built_in()) + return false; + + return true; +} + +/// Filter functions whose name match the regex +/// \param identifier: a function name +/// \param goto_function: a goto function +/// \return: returns true if the function name matches +bool include_pattern_filtert::operator()( + const irep_idt &identifier, + const goto_functionst::goto_functiont &goto_function) const +{ + std::smatch string_matcher; + return std::regex_match(id2string(identifier), string_matcher, regex_matcher); +} + +/// Call a goto_program non-trivial if it has: +/// * Any declarations +/// * At least 2 branches +/// * At least 5 assignments +/// These criteria are arbitrarily chosen. +/// \param identifier: a function name +/// \param goto_function: a goto function +/// \return: returns true if non-trivial +bool trivial_functions_filtert::operator()( + const irep_idt &identifier, + const goto_functionst::goto_functiont &goto_function) const +{ + unsigned long count_assignments = 0, count_goto = 0; + forall_goto_program_instructions(i_it, goto_function.body) + { + if(i_it->is_goto()) + { + if((++count_goto) >= 2) + return true; + } + else if(i_it->is_assign()) + { + if((++count_assignments) >= 5) + return true; + } + else if(i_it->is_decl()) + return true; + } + + return false; +} + +/// Filter goals at source locations considered internal +/// \param source_location: source location of the current goal +/// \return true : if the given source location is not considered internal +bool internal_goals_filtert:: +operator()(const source_locationt &source_location) const +{ + if(source_location.get_file().empty()) + return false; + + if(source_location.is_built_in()) + return false; + + return true; +} diff --git a/src/goto-instrument/cover_filter.h b/src/goto-instrument/cover_filter.h new file mode 100644 index 00000000000..f2e954dfc9d --- /dev/null +++ b/src/goto-instrument/cover_filter.h @@ -0,0 +1,204 @@ +/*******************************************************************\ + +Module: Coverage Instrumentation + +Author: Daniel Kroening + +\*******************************************************************/ + +/// \file +/// Filters for the Coverage Instrumentation + +#ifndef CPROVER_GOTO_INSTRUMENT_COVER_FILTER_H +#define CPROVER_GOTO_INSTRUMENT_COVER_FILTER_H + +#include +#include + +#include +#include + +#include + +/// Base class for filtering functions +class function_filter_baset : public messaget +{ +public: + explicit function_filter_baset(message_handlert &message_handler) + : messaget(message_handler) + { + } + + virtual ~function_filter_baset() + { + } + + /// Returns true if the function passes the filter criteria + virtual bool operator()( + const irep_idt &identifier, + const goto_functionst::goto_functiont &goto_function) const = 0; + + /// Can be called after final filter application to report + /// on unexpected situations encountered + virtual void report_anomalies() const + { + // do nothing by default + } +}; + +/// Base class for filtering goals +class goal_filter_baset : public messaget +{ +public: + explicit goal_filter_baset(message_handlert &message_handler) + : messaget(message_handler) + { + } + + virtual ~goal_filter_baset() + { + } + + /// Returns true if the goal passes the filter criteria + virtual bool operator()(const source_locationt &) const = 0; + + /// Can be called after final filter application to report + /// on unexpected situations encountered + virtual void report_anomalies() const + { + // do nothing by default + } +}; + +/// A collection of function filters to be applied in conjunction +class function_filterst +{ +public: + /// Adds a function filter + /// \param filter: transfers ownership of filter to the filter collection + void add(std::unique_ptr filter) + { + filters.push_back(std::move(filter)); + } + + /// Applies the filters to the given function + /// \param identifier: function name + /// \param goto_function: goto function + bool operator()( + const irep_idt &identifier, + const goto_functionst::goto_functiont &goto_function) const + { + for(const auto &filter : filters) + if(!(*filter)(identifier, goto_function)) + return false; + + return true; + } + + /// Can be called after final filter application to report + /// on unexpected situations encountered + void report_anomalies() const + { + for(const auto &filter : filters) + filter->report_anomalies(); + } + +private: + std::vector> filters; +}; + +/// A collection of goal filters to be applied in conjunction +class goal_filterst +{ +public: + /// Adds a function filter + /// \param filter: transfers ownership of filter to the filter collection + void add(std::unique_ptr filter) + { + filters.push_back(std::move(filter)); + } + + /// Applies the filters to the given source location + /// \param source_location: a source location where a goal is instrumented + bool operator()(const source_locationt &source_location) const + { + for(const auto &filter : filters) + if(!(*filter)(source_location)) + return false; + + return true; + } + + /// Can be called after final filter application to report + /// on unexpected situations encountered + void report_anomalies() const + { + for(const auto &filter : filters) + filter->report_anomalies(); + } + +private: + std::vector> filters; +}; + +/// Filters out CPROVER internal functions +class internal_functions_filtert : public function_filter_baset +{ +public: + explicit internal_functions_filtert(message_handlert &message_handler) + : function_filter_baset(message_handler) + { + } + + bool operator()( + const irep_idt &identifier, + const goto_functionst::goto_functiont &goto_function) const override; +}; + +/// Filters functions that match the provided pattern +class include_pattern_filtert : public function_filter_baset +{ +public: + explicit include_pattern_filtert( + message_handlert &message_handler, + const std::string &cover_include_pattern) + : function_filter_baset(message_handler), + regex_matcher(cover_include_pattern) + { + } + + bool operator()( + const irep_idt &identifier, + const goto_functionst::goto_functiont &goto_function) const override; + +private: + std::regex regex_matcher; +}; + +/// Filters out trivial functions +class trivial_functions_filtert : public function_filter_baset +{ +public: + explicit trivial_functions_filtert(message_handlert &message_handler) + : function_filter_baset(message_handler) + { + } + + bool operator()( + const irep_idt &identifier, + const goto_functionst::goto_functiont &goto_function) const override; +}; + +/// Filters out goals with source locations considered internal +class internal_goals_filtert : public goal_filter_baset +{ +public: + explicit internal_goals_filtert(message_handlert &message_handler) + : goal_filter_baset(message_handler) + { + } + + bool operator()(const source_locationt &) const override; +}; + +#endif // CPROVER_GOTO_INSTRUMENT_COVER_FILTER_H diff --git a/src/goto-instrument/cover_instrument.h b/src/goto-instrument/cover_instrument.h new file mode 100644 index 00000000000..baeed5330c7 --- /dev/null +++ b/src/goto-instrument/cover_instrument.h @@ -0,0 +1,255 @@ +/*******************************************************************\ + +Module: Coverage Instrumentation + +Author: Peter Schrammel + +\*******************************************************************/ + +/// \file +/// Coverage Instrumentation + +#ifndef CPROVER_GOTO_INSTRUMENT_COVER_INSTRUMENT_H +#define CPROVER_GOTO_INSTRUMENT_COVER_INSTRUMENT_H + +#include + +#include +#include + +enum class coverage_criteriont; +class cover_basic_blockst; +class goal_filterst; + +/// Base class for goto program coverage instrumenters +class cover_instrumenter_baset +{ +public: + cover_instrumenter_baset( + const symbol_tablet &_symbol_table, + const goal_filterst &_goal_filters, + const irep_idt &_coverage_criterion) + : coverage_criterion(_coverage_criterion), + ns(_symbol_table), + goal_filters(_goal_filters) + { + } + + /// Instruments a goto program + /// \param goto_program: a goto program + /// \param basic_blocks: detected basic blocks + virtual void operator()( + goto_programt &goto_program, + const cover_basic_blockst &basic_blocks) const + { + Forall_goto_program_instructions(i_it, goto_program) + { + instrument(goto_program, i_it, basic_blocks); + } + } + + const irep_idt property_class = "coverage"; + const irep_idt coverage_criterion; + +protected: + const namespacet ns; + const goal_filterst &goal_filters; + + /// Override this method to implement an instrumenter + virtual void instrument( + goto_programt &, + goto_programt::targett &, + const cover_basic_blockst &) const = 0; + + void initialize_source_location( + goto_programt::targett t, + const std::string &comment, + const irep_idt &function) const + { + t->source_location.set_comment(comment); + t->source_location.set(ID_coverage_criterion, coverage_criterion); + t->source_location.set_property_class(property_class); + t->source_location.set_function(function); + t->function = function; + } + + bool is_non_cover_assertion(goto_programt::const_targett t) const + { + return t->is_assert() && + t->source_location.get_property_class() != property_class; + } +}; + +/// A collection of instrumenters to be run +class cover_instrumenterst +{ +public: + void add_from_criterion( + coverage_criteriont, + const symbol_tablet &, + const goal_filterst &); + + /// Applies all instrumenters to the given goto program + /// \param goto_program: a goto program + /// \param basic_blocks: detected basic blocks of the goto program + void operator()( + goto_programt &goto_program, + const cover_basic_blockst &basic_blocks) const + { + for(const auto &instrumenter : instrumenters) + (*instrumenter)(goto_program, basic_blocks); + } + +protected: + std::vector> instrumenters; +}; + +/// Basic block coverage instrumenter +class cover_location_instrumentert : public cover_instrumenter_baset +{ +public: + cover_location_instrumentert( + const symbol_tablet &_symbol_table, + const goal_filterst &_goal_filters) + : cover_instrumenter_baset(_symbol_table, _goal_filters, "location") + { + } + +protected: + void instrument( + goto_programt &, + goto_programt::targett &, + const cover_basic_blockst &) const override; +}; + +/// Branch coverage instrumenter +class cover_branch_instrumentert : public cover_instrumenter_baset +{ +public: + cover_branch_instrumentert( + const symbol_tablet &_symbol_table, + const goal_filterst &_goal_filters) + : cover_instrumenter_baset(_symbol_table, _goal_filters, "branch") + { + } + +protected: + void instrument( + goto_programt &, + goto_programt::targett &, + const cover_basic_blockst &) const override; +}; + +/// Condition coverage instrumenter +class cover_condition_instrumentert : public cover_instrumenter_baset +{ +public: + cover_condition_instrumentert( + const symbol_tablet &_symbol_table, + const goal_filterst &_goal_filters) + : cover_instrumenter_baset(_symbol_table, _goal_filters, "condition") + { + } + +protected: + void instrument( + goto_programt &, + goto_programt::targett &, + const cover_basic_blockst &) const override; +}; + +/// Decision coverage instrumenter +class cover_decision_instrumentert : public cover_instrumenter_baset +{ +public: + cover_decision_instrumentert( + const symbol_tablet &_symbol_table, + const goal_filterst &_goal_filters) + : cover_instrumenter_baset(_symbol_table, _goal_filters, "decision") + { + } + +protected: + void instrument( + goto_programt &, + goto_programt::targett &, + const cover_basic_blockst &) const override; +}; + +/// MC/DC coverage instrumenter +class cover_mcdc_instrumentert : public cover_instrumenter_baset +{ +public: + cover_mcdc_instrumentert( + const symbol_tablet &_symbol_table, + const goal_filterst &_goal_filters) + : cover_instrumenter_baset(_symbol_table, _goal_filters, "MC/DC") + { + } + +protected: + void instrument( + goto_programt &, + goto_programt::targett &, + const cover_basic_blockst &) const override; +}; + +/// Path coverage instrumenter +class cover_path_instrumentert : public cover_instrumenter_baset +{ +public: + cover_path_instrumentert( + const symbol_tablet &_symbol_table, + const goal_filterst &_goal_filters) + : cover_instrumenter_baset(_symbol_table, _goal_filters, "path") + { + } + +protected: + void instrument( + goto_programt &, + goto_programt::targett &, + const cover_basic_blockst &) const override; +}; + +/// Assertion coverage instrumenter +class cover_assertion_instrumentert : public cover_instrumenter_baset +{ +public: + cover_assertion_instrumentert( + const symbol_tablet &_symbol_table, + const goal_filterst &_goal_filters) + : cover_instrumenter_baset(_symbol_table, _goal_filters, "assertion") + { + } + +protected: + void instrument( + goto_programt &, + goto_programt::targett &, + const cover_basic_blockst &) const override; +}; + +/// __CPROVER_cover coverage instrumenter +class cover_cover_instrumentert : public cover_instrumenter_baset +{ +public: + cover_cover_instrumentert( + const symbol_tablet &_symbol_table, + const goal_filterst &_goal_filters) + : cover_instrumenter_baset(_symbol_table, _goal_filters, "cover") + { + } + +protected: + void instrument( + goto_programt &, + goto_programt::targett &, + const cover_basic_blockst &) const override; +}; + +void cover_instrument_end_of_function( + const irep_idt &function, + goto_programt &goto_program); + +#endif // CPROVER_GOTO_INSTRUMENT_COVER_INSTRUMENT_H diff --git a/src/goto-instrument/cover_instrument_branch.cpp b/src/goto-instrument/cover_instrument_branch.cpp new file mode 100644 index 00000000000..0060ff72629 --- /dev/null +++ b/src/goto-instrument/cover_instrument_branch.cpp @@ -0,0 +1,62 @@ +/*******************************************************************\ + +Module: Coverage Instrumentation + +Author: Daniel Kroening + +\*******************************************************************/ + +/// \file +/// Coverage Instrumentation for Branches + +#include "cover_instrument.h" +#include "cover_basic_blocks.h" + +void cover_branch_instrumentert::instrument( + goto_programt &goto_program, + goto_programt::targett &i_it, + const cover_basic_blockst &basic_blocks) const +{ + if(is_non_cover_assertion(i_it)) + i_it->make_skip(); + + if(i_it == goto_program.instructions.begin()) + { + // we want branch coverage to imply 'entry point of function' + // coverage + std::string comment = "entry point"; + + source_locationt source_location = i_it->source_location; + + goto_programt::targett t = goto_program.insert_before(i_it); + t->make_assertion(false_exprt()); + t->source_location = source_location; + initialize_source_location(t, comment, i_it->function); + } + + if( + i_it->is_goto() && !i_it->guard.is_true() && + !i_it->source_location.is_built_in()) + { + std::string b = + std::to_string(basic_blocks.block_of(i_it) + 1); // start with 1 + std::string true_comment = "block " + b + " branch true"; + std::string false_comment = "block " + b + " branch false"; + + exprt guard = i_it->guard; + const irep_idt function = i_it->function; + source_locationt source_location = i_it->source_location; + + goto_program.insert_before_swap(i_it); + i_it->make_assertion(not_exprt(guard)); + i_it->source_location = source_location; + initialize_source_location(i_it, true_comment, function); + + goto_program.insert_before_swap(i_it); + i_it->make_assertion(guard); + i_it->source_location = source_location; + initialize_source_location(i_it, false_comment, function); + + std::advance(i_it, 2); + } +} diff --git a/src/goto-instrument/cover_instrument_condition.cpp b/src/goto-instrument/cover_instrument_condition.cpp new file mode 100644 index 00000000000..d5b3778d649 --- /dev/null +++ b/src/goto-instrument/cover_instrument_condition.cpp @@ -0,0 +1,52 @@ +/*******************************************************************\ + +Module: Coverage Instrumentation + +Author: Daniel Kroening + +\*******************************************************************/ + +/// \file +/// Coverage Instrumentation for Conditions + +#include "cover_instrument.h" + +#include "cover_util.h" + +void cover_condition_instrumentert::instrument( + goto_programt &goto_program, + goto_programt::targett &i_it, + const cover_basic_blockst &basic_blocks) const +{ + if(is_non_cover_assertion(i_it)) + i_it->make_skip(); + + // Conditions are all atomic predicates in the programs. + if(!i_it->source_location.is_built_in()) + { + const std::set conditions = collect_conditions(i_it); + + const source_locationt source_location = i_it->source_location; + + for(const auto &c : conditions) + { + const std::string c_string = from_expr(ns, "", c); + + const std::string comment_t = "condition `" + c_string + "' true"; + const irep_idt function = i_it->function; + goto_program.insert_before_swap(i_it); + i_it->make_assertion(c); + i_it->source_location = source_location; + initialize_source_location(i_it, comment_t, function); + + const std::string comment_f = "condition `" + c_string + "' false"; + goto_program.insert_before_swap(i_it); + i_it->make_assertion(not_exprt(c)); + i_it->source_location = source_location; + initialize_source_location(i_it, comment_f, function); + } + + for(std::size_t i = 0; i < conditions.size() * 2; i++) + i_it++; + } +} diff --git a/src/goto-instrument/cover_instrument_decision.cpp b/src/goto-instrument/cover_instrument_decision.cpp new file mode 100644 index 00000000000..9c5fc59074d --- /dev/null +++ b/src/goto-instrument/cover_instrument_decision.cpp @@ -0,0 +1,53 @@ +/*******************************************************************\ + +Module: Coverage Instrumentation + +Author: Daniel Kroening + +\*******************************************************************/ + +/// \file +/// Coverage Instrumentation for Decisions + +#include "cover_instrument.h" + +#include "cover_util.h" + +void cover_decision_instrumentert::instrument( + goto_programt &goto_program, + goto_programt::targett &i_it, + const cover_basic_blockst &basic_blocks) const +{ + if(is_non_cover_assertion(i_it)) + i_it->make_skip(); + + // Decisions are maximal Boolean combinations of conditions. + if(!i_it->source_location.is_built_in()) + { + const std::set decisions = collect_decisions(i_it); + + const source_locationt source_location = i_it->source_location; + + for(const auto &d : decisions) + { + const std::string d_string = from_expr(ns, "", d); + + const std::string comment_t = "decision `" + d_string + "' true"; + const irep_idt function = i_it->function; + goto_program.insert_before_swap(i_it); + i_it->make_assertion(d); + i_it->source_location = source_location; + initialize_source_location(i_it, comment_t, function); + + const std::string comment_f = "decision `" + d_string + "' false"; + goto_program.insert_before_swap(i_it); + i_it->make_assertion(not_exprt(d)); + i_it->source_location = source_location; + initialize_source_location(i_it, comment_f, function); + } + + // advance iterator beyond the inserted instructions + for(std::size_t i = 0; i < decisions.size() * 2; i++) + i_it++; + } +} diff --git a/src/goto-instrument/cover_instrument_location.cpp b/src/goto-instrument/cover_instrument_location.cpp new file mode 100644 index 00000000000..214b00248c2 --- /dev/null +++ b/src/goto-instrument/cover_instrument_location.cpp @@ -0,0 +1,47 @@ +/*******************************************************************\ + +Module: Coverage Instrumentation + +Author: Daniel Kroening + +\*******************************************************************/ + +/// \file +/// Coverage Instrumentation for Location, i.e. Basic Blocks + +#include "cover_instrument.h" + +#include "cover_basic_blocks.h" +#include "cover_filter.h" + +void cover_location_instrumentert::instrument( + goto_programt &goto_program, + goto_programt::targett &i_it, + const cover_basic_blockst &basic_blocks) const +{ + if(is_non_cover_assertion(i_it)) + i_it->make_skip(); + + unsigned block_nr = basic_blocks.block_of(i_it); + goto_programt::const_targett in_t = basic_blocks.instruction_of(block_nr); + // we only instrument the selected instruction + if(in_t == i_it) + { + std::string b = std::to_string(block_nr + 1); // start with 1 + std::string id = id2string(i_it->function) + "#" + b; + source_locationt source_location = + basic_blocks.source_location_of(block_nr); + + // filter goals + if(goal_filters(source_location)) + { + std::string comment = "block " + b; + const irep_idt function = i_it->function; + goto_program.insert_before_swap(i_it); + i_it->make_assertion(false_exprt()); + i_it->source_location = source_location; + initialize_source_location(i_it, comment, function); + i_it++; + } + } +} diff --git a/src/goto-instrument/cover_instrument_mcdc.cpp b/src/goto-instrument/cover_instrument_mcdc.cpp new file mode 100644 index 00000000000..a708583c559 --- /dev/null +++ b/src/goto-instrument/cover_instrument_mcdc.cpp @@ -0,0 +1,731 @@ +/*******************************************************************\ + +Module: Coverage Instrumentation + +Author: Daniel Kroening + +\*******************************************************************/ + +/// \file +/// Coverage Instrumentation for MC/DC + +#include "cover_instrument.h" + +#include + +#include "cover_util.h" + +/// To recursively collect controlling exprs for for mcdc coverage. +void collect_mcdc_controlling_rec( + const exprt &src, + const std::vector &conditions, + std::set &result) +{ + // src is conjunction (ID_and) or disjunction (ID_or) + if(src.id() == ID_and || src.id() == ID_or) + { + std::vector operands; + collect_operands(src, operands); + + if(operands.size() == 1) + { + exprt e = *operands.begin(); + collect_mcdc_controlling_rec(e, conditions, result); + } + else if(!operands.empty()) + { + for(std::size_t i = 0; i < operands.size(); i++) + { + const exprt op = operands[i]; + + if(is_condition(op)) + { + if(src.id() == ID_or) + { + std::vector others1, others2; + if(!conditions.empty()) + { + others1.push_back(conjunction(conditions)); + others2.push_back(conjunction(conditions)); + } + + for(std::size_t j = 0; j < operands.size(); j++) + { + others1.push_back(not_exprt(operands[j])); + if(i != j) + others2.push_back(not_exprt(operands[j])); + else + others2.push_back((operands[j])); + } + + result.insert(conjunction(others1)); + result.insert(conjunction(others2)); + continue; + } + + std::vector o = operands; + + // 'o[i]' needs to be true and false + std::vector new_conditions = conditions; + new_conditions.push_back(conjunction(o)); + result.insert(conjunction(new_conditions)); + + o[i].make_not(); + new_conditions.back() = conjunction(o); + result.insert(conjunction(new_conditions)); + } + else + { + std::vector others; + others.reserve(operands.size() - 1); + + for(std::size_t j = 0; j < operands.size(); j++) + if(i != j) + { + if(src.id() == ID_or) + others.push_back(not_exprt(operands[j])); + else + others.push_back(operands[j]); + } + + exprt c = conjunction(others); + std::vector new_conditions = conditions; + new_conditions.push_back(c); + + collect_mcdc_controlling_rec(op, new_conditions, result); + } + } + } + } + else if(src.id() == ID_not) + { + exprt e = to_not_expr(src).op(); + if(!is_condition(e)) + collect_mcdc_controlling_rec(e, conditions, result); + else + { + // to store a copy of ''src'' + std::vector new_conditions1 = conditions; + new_conditions1.push_back(src); + result.insert(conjunction(new_conditions1)); + + // to store a copy of its negation, i.e., ''e'' + std::vector new_conditions2 = conditions; + new_conditions2.push_back(e); + result.insert(conjunction(new_conditions2)); + } + } + else + { + /** + * It may happen that ''is_condition(src)'' is valid, + * but we ignore this case here as it can be handled + * by the routine decision/condition detection. + **/ + } +} + +std::set collect_mcdc_controlling(const std::set &decisions) +{ + std::set result; + + for(const auto &d : decisions) + collect_mcdc_controlling_rec(d, {}, result); + + return result; +} + +/// To replace the i-th expr of ''operands'' with each expr inside +/// ''replacement_exprs''. +std::set replacement_conjunction( + const std::set &replacement_exprs, + const std::vector &operands, + const std::size_t i) +{ + std::set result; + for(auto &y : replacement_exprs) + { + std::vector others; + for(std::size_t j = 0; j < operands.size(); j++) + if(i != j) + others.push_back(operands[j]); + + others.push_back(y); + exprt c = conjunction(others); + result.insert(c); + } + return result; +} + +/// This nested method iteratively applies ''collect_mcdc_controlling'' to every +/// non-atomic expr within a decision +std::set +collect_mcdc_controlling_nested(const std::set &decisions) +{ + // To obtain the 1st-level controlling conditions + std::set controlling = collect_mcdc_controlling(decisions); + + std::set result; + // For each controlling condition, to check if it contains + // non-atomic exprs + for(auto &src : controlling) + { + std::set s1, s2; + /** + * The final controlling conditions resulted from ''src'' + * will be stored in ''s1''; ''s2'' is usd to hold the + * temporary expansion. + **/ + s1.insert(src); + + // dual-loop structure to eliminate complex + // non-atomic-conditional terms + while(true) + { + bool changed = false; + // the 2nd loop + for(auto &x : s1) + { + // if ''x'' is atomic conditional term, there + // is no expansion + if(is_condition(x)) + { + s2.insert(x); + continue; + } + // otherwise, we apply the ''nested'' method to + // each of its operands + std::vector operands; + collect_operands(x, operands); + + for(std::size_t i = 0; i < operands.size(); i++) + { + std::set res; + /** + * To expand an operand if it is not atomic, + * and label the ''changed'' flag; the resulted + * expansion of such an operand is stored in ''res''. + **/ + if(operands[i].id() == ID_not) + { + exprt no = operands[i].op0(); + if(!is_condition(no)) + { + changed = true; + std::set ctrl_no; + ctrl_no.insert(no); + res = collect_mcdc_controlling(ctrl_no); + } + } + else if(!is_condition(operands[i])) + { + changed = true; + std::set ctrl; + ctrl.insert(operands[i]); + res = collect_mcdc_controlling(ctrl); + } + + // To replace a non-atomic expr with its expansion + std::set co = replacement_conjunction(res, operands, i); + s2.insert(co.begin(), co.end()); + if(!res.empty()) + break; + } + // if there is no change x.r.t current operands of ''x'', + // i.e., they are all atomic, we reserve ''x'' + if(!changed) + s2.insert(x); + } + // update ''s1'' and check if change happens + s1 = s2; + if(!changed) + break; + s2.clear(); + } + + // The expansions of each ''src'' should be added into + // the ''result'' + result.insert(s1.begin(), s1.end()); + } + + return result; +} + +/// The sign of expr ''e'' within the super-expr ''E'' +/// \par parameters: E should be the pre-processed output by +/// ''collect_mcdc_controlling_nested'' +/// \return +1 : not negated -1 : negated +std::set sign_of_expr(const exprt &e, const exprt &E) +{ + std::set signs; + + // At fist, we pre-screen the case such that ''E'' + // is an atomic condition + if(is_condition(E)) + { + if(e == E) + signs.insert(+1); + return signs; + } + + // or, ''E'' is the negation of ''e''? + if(E.id() == ID_not) + { + if(e == E.op0()) + { + signs.insert(-1); + return signs; + } + } + + /** + * In the general case, we analyze each operand of ''E''. + **/ + std::vector ops; + collect_operands(E, ops); + for(auto &x : ops) + { + exprt y(x); + if(y == e) + signs.insert(+1); + else if(y.id() == ID_not) + { + y.make_not(); + if(y == e) + signs.insert(-1); + if(!is_condition(y)) + { + std::set re = sign_of_expr(e, y); + signs.insert(re.begin(), re.end()); + } + } + else if(!is_condition(y)) + { + std::set re = sign_of_expr(e, y); + signs.insert(re.begin(), re.end()); + } + } + + return signs; +} + +/// After the ''collect_mcdc_controlling_nested'', there can be the recurrence +/// of the same expr in the resulted set of exprs, and this method will remove +/// the repetitive ones. +void remove_repetition(std::set &exprs) +{ + // to obtain the set of atomic conditions + std::set conditions; + for(auto &x : exprs) + { + std::set new_conditions = collect_conditions(x); + conditions.insert(new_conditions.begin(), new_conditions.end()); + } + // exprt that contains multiple (inconsistent) signs should + // be removed + std::set new_exprs; + for(auto &x : exprs) + { + bool kept = true; + for(auto &c : conditions) + { + std::set signs = sign_of_expr(c, x); + if(signs.size() > 1) + { + kept = false; + break; + } + } + if(kept) + new_exprs.insert(x); + } + exprs = new_exprs; + new_exprs.clear(); + + for(auto &x : exprs) + { + bool red = false; + /** + * To check if ''x'' is identical with some + * expr in ''new_exprs''. Two exprs ''x'' + * and ''y'' are identical iff they have the + * same sign for every atomic condition ''c''. + **/ + for(auto &y : new_exprs) + { + bool iden = true; + for(auto &c : conditions) + { + std::set signs1 = sign_of_expr(c, x); + std::set signs2 = sign_of_expr(c, y); + int s1 = signs1.size(), s2 = signs2.size(); + // it is easy to check non-equivalence; + if(s1 != s2) + { + iden = false; + break; + } + else + { + if(s1 == 0 && s2 == 0) + continue; + // it is easy to check non-equivalence + if(*(signs1.begin()) != *(signs2.begin())) + { + iden = false; + break; + } + } + } + /** + * If ''x'' is found identical w.r.t some + * expr in ''new_conditions, we label it + * and break. + **/ + if(iden) + { + red = true; + break; + } + } + // an expr is added into ''new_exprs'' + // if it is not found repetitive + if(!red) + new_exprs.insert(x); + } + + // update the original ''exprs'' + exprs = new_exprs; +} + +/// To evaluate the value of expr ''src'', according to the atomic expr values +bool eval_expr(const std::map &atomic_exprs, const exprt &src) +{ + std::vector operands; + collect_operands(src, operands); + // src is AND + if(src.id() == ID_and) + { + for(auto &x : operands) + if(!eval_expr(atomic_exprs, x)) + return false; + return true; + } + // src is OR + else if(src.id() == ID_or) + { + std::size_t fcount = 0; + + for(auto &x : operands) + if(!eval_expr(atomic_exprs, x)) + fcount++; + + if(fcount < operands.size()) + return true; + else + return false; + } + // src is NOT + else if(src.id() == ID_not) + { + exprt no_op(src); + no_op.make_not(); + return !eval_expr(atomic_exprs, no_op); + } + else // if(is_condition(src)) + { + // ''src'' should be guaranteed to be consistent + // with ''atomic_exprs'' + if(atomic_exprs.find(src)->second == +1) + return true; + else // if(atomic_exprs.find(src)->second==-1) + return false; + } +} + +/// To obtain values of atomic exprs within the super expr +std::map +values_of_atomic_exprs(const exprt &e, const std::set &conditions) +{ + std::map atomic_exprs; + for(auto &c : conditions) + { + std::set signs = sign_of_expr(c, e); + if(signs.empty()) + { + // ''c'' is not contained in ''e'' + atomic_exprs.insert(std::pair(c, 0)); + continue; + } + // we do not consider inconsistent expr ''e'' + if(signs.size() != 1) + continue; + + atomic_exprs.insert(std::pair(c, *signs.begin())); + } + return atomic_exprs; +} + +/// To check if the two input controlling exprs are mcdc pairs regarding an +/// atomic expr ''c''. A mcdc pair of (e1, e2) regarding ''c'' means that ''e1'' +/// and ''e2'' result in different ''decision'' values, and this is caused by +/// the different choice of ''c'' value. +bool is_mcdc_pair( + const exprt &e1, + const exprt &e2, + const exprt &c, + const std::set &conditions, + const exprt &decision) +{ + // An controlling expr cannot be mcdc pair of itself + if(e1 == e2) + return false; + + // To obtain values of each atomic condition within ''e1'' + // and ''e2'' + std::map atomic_exprs_e1 = + values_of_atomic_exprs(e1, conditions); + std::map atomic_exprs_e2 = + values_of_atomic_exprs(e2, conditions); + + // the sign of ''c'' inside ''e1'' and ''e2'' + signed cs1 = atomic_exprs_e1.find(c)->second; + signed cs2 = atomic_exprs_e2.find(c)->second; + // a mcdc pair should both contain ''c'', i.e., sign=+1 or -1 + if(cs1 == 0 || cs2 == 0) + return false; + + // A mcdc pair regarding an atomic expr ''c'' + // should have different values of ''c'' + if(cs1 == cs2) + return false; + + // A mcdc pair should result in different ''decision'' + if( + eval_expr(atomic_exprs_e1, decision) == + eval_expr(atomic_exprs_e2, decision)) + return false; + + /** + * A mcdc pair of controlling exprs regarding ''c'' + * can have different values for only one atomic + * expr, i.e., ''c''. Otherwise, they are not + * a mcdc pair. + **/ + int diff_count = 0; + auto e1_it = atomic_exprs_e1.begin(); + auto e2_it = atomic_exprs_e2.begin(); + while(e1_it != atomic_exprs_e1.end()) + { + if(e1_it->second != e2_it->second) + diff_count++; + if(diff_count > 1) + break; + e1_it++; + e2_it++; + } + + if(diff_count == 1) + return true; + else + return false; +} + +/// To check if we can find the mcdc pair of the input ''expr_set'' regarding +/// the atomic expr ''c'' +bool has_mcdc_pair( + const exprt &c, + const std::set &expr_set, + const std::set &conditions, + const exprt &decision) +{ + for(auto y1 : expr_set) + { + for(auto y2 : expr_set) + { + if(is_mcdc_pair(y1, y2, c, conditions, decision)) + { + return true; + } + } + } + return false; +} + +/// This method minimizes the controlling conditions for mcdc coverage. The +/// minimum is in a sense that by deleting any controlling condition in the set, +/// the mcdc coverage for the decision will be not complete. +/// \par parameters: The input ''controlling'' should have been processed by +/// ''collect_mcdc_controlling_nested'' and +/// ''remove_repetition'' +void minimize_mcdc_controlling( + std::set &controlling, + const exprt &decision) +{ + // to obtain the set of atomic conditions + std::set conditions; + for(auto &x : controlling) + { + std::set new_conditions = collect_conditions(x); + conditions.insert(new_conditions.begin(), new_conditions.end()); + } + + while(true) + { + std::set new_controlling; + bool ctrl_update = false; + /** + * Iteratively, we test that after removing an item ''x'' + * from the ''controlling'', can a complete mcdc coverage + * over ''decision'' still be reserved? + * + * If yes, we update ''controlling'' with the + * ''new_controlling'' without ''x''; otherwise, we should + * keep ''x'' within ''controlling''. + * + * If in the end all elements ''x'' in ''controlling'' are + * reserved, this means that current ''controlling'' set is + * minimum and the ''while'' loop should be broken out of. + * + * Note: implementation here for the above procedure is + * not (meant to be) optimal. + **/ + for(auto &x : controlling) + { + // To create a new ''controlling'' set without ''x'' + new_controlling.clear(); + for(auto &y : controlling) + if(y != x) + new_controlling.insert(y); + + bool removing_x = true; + // For each atomic expr condition ''c'', to check if its is + // covered by at least a mcdc pair. + for(auto &c : conditions) + { + bool cOK = has_mcdc_pair(c, new_controlling, conditions, decision); + /** + * If there is no mcdc pair for an atomic condition ''c'', + * then ''x'' should not be removed from the original + * ''controlling'' set + **/ + if(!cOK) + { + removing_x = false; + break; + } + } + + // If ''removing_x'' is valid, it is safe to remove ''x'' + // from the original ''controlling'' + if(removing_x) + { + ctrl_update = true; + break; + } + } + // Update ''controlling'' or break the while loop + if(ctrl_update) + { + controlling = new_controlling; + } + else + break; + } +} + +void cover_mcdc_instrumentert::instrument( + goto_programt &goto_program, + goto_programt::targett &i_it, + const cover_basic_blockst &basic_blocks) const +{ + if(is_non_cover_assertion(i_it)) + i_it->make_skip(); + + // 1. Each entry and exit point is invoked + // 2. Each decision takes every possible outcome + // 3. Each condition in a decision takes every possible outcome + // 4. Each condition in a decision is shown to independently + // affect the outcome of the decision. + if(!i_it->source_location.is_built_in()) + { + const std::set conditions = collect_conditions(i_it); + const std::set decisions = collect_decisions(i_it); + + std::set both; + std::set_union( + conditions.begin(), + conditions.end(), + decisions.begin(), + decisions.end(), + inserter(both, both.end())); + + const source_locationt source_location = i_it->source_location; + + for(const auto &p : both) + { + bool is_decision = decisions.find(p) != decisions.end(); + bool is_condition = conditions.find(p) != conditions.end(); + + std::string description = (is_decision && is_condition) + ? "decision/condition" + : is_decision ? "decision" : "condition"; + + std::string p_string = from_expr(ns, "", p); + + std::string comment_t = description + " `" + p_string + "' true"; + const irep_idt function = i_it->function; + goto_program.insert_before_swap(i_it); + // i_it->make_assertion(p); + i_it->make_assertion(not_exprt(p)); + i_it->source_location = source_location; + i_it->source_location.set_comment(comment_t); + i_it->source_location.set(ID_coverage_criterion, coverage_criterion); + i_it->source_location.set_property_class(property_class); + i_it->source_location.set_function(function); + i_it->function = function; + + std::string comment_f = description + " `" + p_string + "' false"; + goto_program.insert_before_swap(i_it); + // i_it->make_assertion(not_exprt(p)); + i_it->make_assertion(p); + i_it->source_location = source_location; + i_it->source_location.set_comment(comment_f); + i_it->source_location.set(ID_coverage_criterion, coverage_criterion); + i_it->source_location.set_property_class(property_class); + i_it->source_location.set_function(function); + i_it->function = function; + } + + std::set controlling; + // controlling=collect_mcdc_controlling(decisions); + controlling = collect_mcdc_controlling_nested(decisions); + remove_repetition(controlling); + // for now, we restrict to the case of a single ''decision''; + // however, this is not true, e.g., ''? :'' operator. + INVARIANT(!decisions.empty(), "There must be at least one decision"); + minimize_mcdc_controlling(controlling, *decisions.begin()); + + for(const auto &p : controlling) + { + std::string p_string = from_expr(ns, "", p); + + std::string description = + "MC/DC independence condition `" + p_string + "'"; + + const irep_idt function = i_it->function; + goto_program.insert_before_swap(i_it); + i_it->make_assertion(not_exprt(p)); + // i_it->make_assertion(p); + i_it->source_location = source_location; + i_it->source_location.set_comment(description); + i_it->source_location.set(ID_coverage_criterion, coverage_criterion); + i_it->source_location.set_property_class(property_class); + i_it->source_location.set_function(function); + i_it->function = function; + } + + for(std::size_t i = 0; i < both.size() * 2 + controlling.size(); i++) + i_it++; + } +} diff --git a/src/goto-instrument/cover_instrument_other.cpp b/src/goto-instrument/cover_instrument_other.cpp new file mode 100644 index 00000000000..d2f37d598e7 --- /dev/null +++ b/src/goto-instrument/cover_instrument_other.cpp @@ -0,0 +1,85 @@ +/*******************************************************************\ + +Module: Coverage Instrumentation + +Author: Daniel Kroening + +\*******************************************************************/ + +/// \file +/// Further coverage instrumentations + +#include "cover_instrument.h" + +#include "cover_util.h" + +void cover_path_instrumentert::instrument( + goto_programt &goto_program, + goto_programt::targett &i_it, + const cover_basic_blockst &basic_blocks) const +{ + if(is_non_cover_assertion(i_it)) + i_it->make_skip(); + + // TODO: implement +} + +void cover_assertion_instrumentert::instrument( + goto_programt &goto_program, + goto_programt::targett &i_it, + const cover_basic_blockst &basic_blocks) const +{ + // turn into 'assert(false)' to avoid simplification + if(is_non_cover_assertion(i_it)) + { + i_it->guard = false_exprt(); + initialize_source_location( + i_it, id2string(i_it->source_location.get_comment()), i_it->function); + } +} + +void cover_cover_instrumentert::instrument( + goto_programt &goto_program, + goto_programt::targett &i_it, + const cover_basic_blockst &basic_blocks) const +{ + // turn __CPROVER_cover(x) into 'assert(!x)' + if(i_it->is_function_call()) + { + const code_function_callt &code_function_call = + to_code_function_call(i_it->code); + if( + code_function_call.function().id() == ID_symbol && + to_symbol_expr(code_function_call.function()).get_identifier() == + "__CPROVER_cover" && + code_function_call.arguments().size() == 1) + { + const exprt c = code_function_call.arguments()[0]; + std::string comment = "condition `" + from_expr(ns, "", c) + "'"; + i_it->guard = not_exprt(c); + i_it->type = ASSERT; + i_it->code.clear(); + initialize_source_location(i_it, comment, i_it->function); + } + } + else if(is_non_cover_assertion(i_it)) + i_it->make_skip(); +} + +void cover_instrument_end_of_function( + const irep_idt &function, + goto_programt &goto_program) +{ + auto if_it = goto_program.instructions.end(); + while(!if_it->is_function_call()) + if_it--; + if_it++; + const std::string &comment = + "additional goal to ensure reachability of end of function"; + goto_program.insert_before_swap(if_it); + if_it->make_assertion(false_exprt()); + if_it->source_location.set_comment(comment); + if_it->source_location.set_property_class("reachability_constraint"); + if_it->source_location.set_function(function); + if_it->function = function; +} diff --git a/src/goto-instrument/cover_util.cpp b/src/goto-instrument/cover_util.cpp new file mode 100644 index 00000000000..7fbc015d1cd --- /dev/null +++ b/src/goto-instrument/cover_util.cpp @@ -0,0 +1,134 @@ +/*******************************************************************\ + +Module: Coverage Instrumentation + +Author: Daniel Kroening + +\*******************************************************************/ + +/// \file +/// Coverage Instrumentation Utilities + +#include "cover_util.h" + +bool is_condition(const exprt &src) +{ + if(src.type().id() != ID_bool) + return false; + + // conditions are 'atomic predicates' + if( + src.id() == ID_and || src.id() == ID_or || src.id() == ID_not || + src.id() == ID_implies) + return false; + + return true; +} + +void collect_conditions_rec(const exprt &src, std::set &dest) +{ + if(src.id() == ID_address_of) + { + return; + } + + for(const auto &op : src.operands()) + collect_conditions_rec(op, dest); + + if(is_condition(src) && !src.is_constant()) + dest.insert(src); +} + +std::set collect_conditions(const exprt &src) +{ + std::set result; + collect_conditions_rec(src, result); + return result; +} + +std::set collect_conditions(const goto_programt::const_targett t) +{ + switch(t->type) + { + case GOTO: + case ASSERT: + return collect_conditions(t->guard); + + case ASSIGN: + case FUNCTION_CALL: + return collect_conditions(t->code); + + default: + { + } + } + + return std::set(); +} + +void collect_operands(const exprt &src, std::vector &dest) +{ + for(const exprt &op : src.operands()) + { + if(op.id() == src.id()) + collect_operands(op, dest); + else + dest.push_back(op); + } +} + +void collect_decisions_rec(const exprt &src, std::set &dest) +{ + if(src.id() == ID_address_of) + { + return; + } + + if(src.type().id() == ID_bool) + { + if(src.is_constant()) + { + // ignore me + } + else if(src.id() == ID_not) + { + collect_decisions_rec(src.op0(), dest); + } + else + { + dest.insert(src); + } + } + else + { + for(const auto &op : src.operands()) + collect_decisions_rec(op, dest); + } +} + +std::set collect_decisions(const exprt &src) +{ + std::set result; + collect_decisions_rec(src, result); + return result; +} + +std::set collect_decisions(const goto_programt::const_targett t) +{ + switch(t->type) + { + case GOTO: + case ASSERT: + return collect_decisions(t->guard); + + case ASSIGN: + case FUNCTION_CALL: + return collect_decisions(t->code); + + default: + { + } + } + + return std::set(); +} diff --git a/src/goto-instrument/cover_util.h b/src/goto-instrument/cover_util.h new file mode 100644 index 00000000000..32cb75ea214 --- /dev/null +++ b/src/goto-instrument/cover_util.h @@ -0,0 +1,33 @@ +/*******************************************************************\ + +Module: Coverage Instrumentation + +Author: Daniel Kroening + +\*******************************************************************/ + +/// \file +/// Coverage Instrumentation Utilities + +#ifndef CPROVER_GOTO_INSTRUMENT_COVER_UTIL_H +#define CPROVER_GOTO_INSTRUMENT_COVER_UTIL_H + +#include + +bool is_condition(const exprt &src); + +void collect_conditions_rec(const exprt &src, std::set &dest); + +std::set collect_conditions(const exprt &src); + +std::set collect_conditions(const goto_programt::const_targett t); + +void collect_operands(const exprt &src, std::vector &dest); + +void collect_decisions_rec(const exprt &src, std::set &dest); + +std::set collect_decisions(const exprt &src); + +std::set collect_decisions(const goto_programt::const_targett t); + +#endif // CPROVER_GOTO_INSTRUMENT_COVER_UTIL_H diff --git a/src/jbmc/Makefile b/src/jbmc/Makefile index bd6a2b5d962..cbb784bce2d 100644 --- a/src/jbmc/Makefile +++ b/src/jbmc/Makefile @@ -20,6 +20,15 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../goto-instrument/full_slicer$(OBJEXT) \ ../goto-instrument/nondet_static$(OBJEXT) \ ../goto-instrument/cover$(OBJEXT) \ + ../goto-instrument/cover_basic_blocks$(OBJEXT) \ + ../goto-instrument/cover_filter$(OBJEXT) \ + ../goto-instrument/cover_instrument_branch$(OBJEXT) \ + ../goto-instrument/cover_instrument_condition$(OBJEXT) \ + ../goto-instrument/cover_instrument_decision$(OBJEXT) \ + ../goto-instrument/cover_instrument_location$(OBJEXT) \ + ../goto-instrument/cover_instrument_mcdc$(OBJEXT) \ + ../goto-instrument/cover_instrument_other$(OBJEXT) \ + ../goto-instrument/cover_util$(OBJEXT) \ ../analyses/analyses$(LIBEXT) \ ../langapi/langapi$(LIBEXT) \ ../xmllang/xmllang$(LIBEXT) \ diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp index 7d3da461fd5..15bcf5af4d1 100644 --- a/src/jbmc/jbmc_parse_options.cpp +++ b/src/jbmc/jbmc_parse_options.cpp @@ -115,7 +115,7 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options) options.set_option("show-vcc", true); if(cmdline.isset("cover")) - options.set_option("cover", cmdline.get_values("cover")); + parse_cover_options(cmdline, options); if(cmdline.isset("no-simplify")) options.set_option("simplify", false); @@ -734,10 +734,7 @@ bool jbmc_parse_optionst::process_goto_program( // instrument cover goals if(cmdline.isset("cover")) { - if(instrument_cover_goals( - cmdline, - goto_model, - get_message_handler())) + if(instrument_cover_goals(options, goto_model, get_message_handler())) return true; }