diff --git a/regression/cbmc-cover/mcdc-boundary-values1/main.c b/regression/cbmc-cover/mcdc-boundary-values1/main.c new file mode 100644 index 00000000000..c3aa903c471 --- /dev/null +++ b/regression/cbmc-cover/mcdc-boundary-values1/main.c @@ -0,0 +1,11 @@ +int main() +{ + unsigned x; + + __CPROVER_input("x", x); + + if(x<3) + ; + + return 1; +} diff --git a/regression/cbmc-cover/mcdc-boundary-values1/test.desc b/regression/cbmc-cover/mcdc-boundary-values1/test.desc new file mode 100644 index 00000000000..724ebfef074 --- /dev/null +++ b/regression/cbmc-cover/mcdc-boundary-values1/test.desc @@ -0,0 +1,14 @@ +CORE +main.c +--cover mcdc --cover boundary-values +^EXIT=0$ +^SIGNAL=0$ +^\[main.coverage.1\] file main.c line 7 function main MC/DC independence condition `x > (unsigned int)3.* SATISFIED$ +^\[main.coverage.2\] file main.c line 7 function main MC/DC independence condition `x == (unsigned int)3.* SATISFIED$ +^\[main.coverage.3\] file main.c line 7 function main MC/DC independence condition `x < (unsigned int)3.* SATISFIED$ +^\[main.coverage.4\] file main.c line 7 function main decision/condition `x < (unsigned int)3.*: SATISFIED$ +^\[main.coverage.5\] file main.c line 7 function main decision/condition `x < (unsigned int)3.*: SATISFIED$ +^\*\* .* of .* covered (100.0%)$ +^\*\* Used 3 iterations$ +-- +^warning: ignoring diff --git a/regression/cbmc-cover/mcdc-boundary-values2/main.c b/regression/cbmc-cover/mcdc-boundary-values2/main.c new file mode 100644 index 00000000000..5800ada9ee6 --- /dev/null +++ b/regression/cbmc-cover/mcdc-boundary-values2/main.c @@ -0,0 +1,12 @@ +int main() +{ + unsigned x, y; + + __CPROVER_input("x", x); + __CPROVER_input("y", y); + + if (!(x>3) && y<5) + ; + + return 1; +} diff --git a/regression/cbmc-cover/mcdc-boundary-values2/test.desc b/regression/cbmc-cover/mcdc-boundary-values2/test.desc new file mode 100644 index 00000000000..b01aad0f49c --- /dev/null +++ b/regression/cbmc-cover/mcdc-boundary-values2/test.desc @@ -0,0 +1,22 @@ +CORE +main.c +--cover mcdc --cover boundary-values +^EXIT=0$ +^SIGNAL=0$ +^\[main.coverage.1\] file main.c line 8 function main MC/DC independence condition `x == (unsigned int)3 && y > (unsigned int)5.* SATISFIED$ +^\[main.coverage.2\] file main.c line 8 function main MC/DC independence condition `x == (unsigned int)3 && y == (unsigned int)5.* SATISFIED$ +^\[main.coverage.3\] file main.c line 8 function main MC/DC independence condition `y < (unsigned int)5 && x > (unsigned int)3.* SATISFIED$ +^\[main.coverage.4\] file main.c line 8 function main MC/DC independence condition `y < (unsigned int)5 && x == (unsigned int)3.* SATISFIED$ +^\[main.coverage.5\] file main.c line 8 function main MC/DC independence condition `y < (unsigned int)5 && x < (unsigned int)3.* SATISFIED$ +^\[main.coverage.6\] file main.c line 8 function main MC/DC independence condition `x < (unsigned int)3 && y > (unsigned int)5.* SATISFIED$ +^\[main.coverage.7\] file main.c line 8 function main MC/DC independence condition `x < (unsigned int)3 && y == (unsigned int)5.* SATISFIED$ +^\[main.coverage.8\] file main.c line 8 function main decision `!(x > (unsigned int)3) && y < (unsigned int)5.* SATISFIED$ +^\[main.coverage.9\] file main.c line 8 function main decision `!(x > (unsigned int)3) && y < (unsigned int)5.* SATISFIED$ +^\[main.coverage.10\] file main.c line 8 function main condition `x > (unsigned int)3.* SATISFIED$ +^\[main.coverage.11\] file main.c line 8 function main condition `x > (unsigned int)3.* SATISFIED$ +^\[main.coverage.12\] file main.c line 8 function main condition `y < (unsigned int)5.* SATISFIED$ +^\[main.coverage.13\] file main.c line 8 function main condition `y < (unsigned int)5.* SATISFIED$ +^\*\* .* of .* covered (100.0%)$ +^\*\* Used 8 iterations$ +-- +^warning: ignoring diff --git a/regression/cbmc-cover/mcdc-boundary-values3/main.c b/regression/cbmc-cover/mcdc-boundary-values3/main.c new file mode 100644 index 00000000000..ebc094c78d5 --- /dev/null +++ b/regression/cbmc-cover/mcdc-boundary-values3/main.c @@ -0,0 +1,13 @@ +int main() +{ + int altitude; + + __CPROVER_input("altitude", altitude); + + if (altitude > 2500) + { + /* instructions */ + } + + return 1; +} diff --git a/regression/cbmc-cover/mcdc-boundary-values3/test.desc b/regression/cbmc-cover/mcdc-boundary-values3/test.desc new file mode 100644 index 00000000000..43d8b882fc4 --- /dev/null +++ b/regression/cbmc-cover/mcdc-boundary-values3/test.desc @@ -0,0 +1,14 @@ +CORE +main.c +--cover mcdc --cover boundary-values +^EXIT=0$ +^SIGNAL=0$ +^\[main.coverage.1\] file main.c line 7 function main MC/DC independence condition `altitude > 2500.* SATISFIED$ +^\[main.coverage.2\] file main.c line 7 function main MC/DC independence condition `altitude == 2500.* SATISFIED$ +^\[main.coverage.3\] file main.c line 7 function main MC/DC independence condition `altitude < 2500.* SATISFIED$ +^\[main.coverage.4\] file main.c line 7 function main decision/condition `altitude > 2500.* SATISFIED$ +^\[main.coverage.5\] file main.c line 7 function main decision/condition `altitude > 2500.* SATISFIED$ +^\*\* .* of .* covered (100.0%)$ +^\*\* Used 3 iterations$ +-- +^warning: ignoring diff --git a/regression/cbmc-cover/mcdc-boundary-values4/main.c b/regression/cbmc-cover/mcdc-boundary-values4/main.c new file mode 100644 index 00000000000..40f4f35984e --- /dev/null +++ b/regression/cbmc-cover/mcdc-boundary-values4/main.c @@ -0,0 +1,18 @@ +int main() +{ + _Bool A, B, C; + + + __CPROVER_input("cold", A); + + if (A) + { + /* instructions */ + } + else + { + /* instructions */ + } + + return 1; +} diff --git a/regression/cbmc-cover/mcdc-boundary-values4/test.desc b/regression/cbmc-cover/mcdc-boundary-values4/test.desc new file mode 100644 index 00000000000..fe3d82783be --- /dev/null +++ b/regression/cbmc-cover/mcdc-boundary-values4/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--cover mcdc --cover boundary-values +^EXIT=0$ +^SIGNAL=0$ +^\[main.coverage.1\] file main.c line 8 function main MC/DC independence condition `A != FALSE.* SATISFIED$ +^\[main.coverage.2\] file main.c line 8 function main MC/DC independence condition `A == FALSE.* SATISFIED$ +^\[main.coverage.3\] file main.c line 8 function main decision/condition `A != FALSE.*: SATISFIED$ +^\[main.coverage.4\] file main.c line 8 function main decision/condition `A != FALSE.* SATISFIED$ +^\*\* .* of .* covered (100.0%)$ +^\*\* Used 2 iterations$ +-- +^warning: ignoring diff --git a/regression/cbmc-cover/mcdc1/test.desc b/regression/cbmc-cover/mcdc1/test.desc index 060d9040829..10a19361845 100644 --- a/regression/cbmc-cover/mcdc1/test.desc +++ b/regression/cbmc-cover/mcdc1/test.desc @@ -3,12 +3,11 @@ main.c --cover mcdc ^EXIT=0$ ^SIGNAL=0$ -^\[main.coverage.1\] file main.c line 14 function main MC/DC independence condition `C && D && !E && A && !B.*: SATISFIED$ -^\[main.coverage.2\] file main.c line 14 function main MC/DC independence condition `C && !D && E && A && !B.*: SATISFIED$ -^\[main.coverage.3\] file main.c line 14 function main MC/DC independence condition `!C && D && E && A && !B.*: SATISFIED$ +^\[main.coverage.1\] file main.c line 14 function main MC/DC independence condition `A && !B && C && D && !E.*: SATISFIED$ +^\[main.coverage.2\] file main.c line 14 function main MC/DC independence condition `A && !B && C && !D && E.*: SATISFIED$ +^\[main.coverage.3\] file main.c line 14 function main MC/DC independence condition `A && !B && !C && D && E.*: SATISFIED$ ^\[main.coverage.4\] file main.c line 14 function main MC/DC independence condition `C && D && E && A && !B.*: SATISFIED$ ^\[main.coverage.5\] file main.c line 14 function main MC/DC independence condition `C && D && E && !A && B.*: SATISFIED$ -^\[main.coverage.6\] file main.c line 14 function main MC/DC independence condition `C && D && E && !A && !B.*: SATISFIED$ ^\*\* .* of .* covered (100.0%)$ ^\*\* Used 10 iterations$ -- diff --git a/regression/cbmc-cover/mcdc8/test.desc b/regression/cbmc-cover/mcdc8/test.desc index bf8dabbfa0f..48099e5b89e 100644 --- a/regression/cbmc-cover/mcdc8/test.desc +++ b/regression/cbmc-cover/mcdc8/test.desc @@ -3,10 +3,10 @@ main.c --cover mcdc ^EXIT=0$ ^SIGNAL=0$ -^\[main.coverage.1\] file main.c line 9 function main MC/DC independence condition `c != FALSE && a != FALSE && !(b != FALSE).* SATISFIED$ -^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition `c != FALSE && !(a != FALSE) && b != FALSE.* SATISFIED$ -^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition `c != FALSE && !(a != FALSE) && !(b != FALSE).* SATISFIED$ -^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition `!(c != FALSE) && a != FALSE && !(b != FALSE).* SATISFIED$ +^\[main.coverage.1\] file main.c line 9 function main MC/DC independence condition `a != FALSE && !(b != FALSE) && c != FALSE.* SATISFIED$ +^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition `a != FALSE && !(b != FALSE) && !(c != FALSE).* SATISFIED$ +^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition `!(a != FALSE) && b != FALSE && c != FALSE.* SATISFIED$ +^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition `!(a != FALSE) && !(b != FALSE) && c != FALSE.* SATISFIED$ ^\*\* .* of .* covered (100.0%)$ ^\*\* Used 6 iterations$ -- diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile index 79f7a4fd982..1c1e947a79e 100644 --- a/src/cbmc/Makefile +++ b/src/cbmc/Makefile @@ -22,6 +22,8 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../goto-instrument/full_slicer$(OBJEXT) \ ../goto-instrument/nondet_static$(OBJEXT) \ ../goto-instrument/cover$(OBJEXT) \ + ../goto-instrument/cover_utils$(OBJEXT) \ + ../goto-instrument/cover_mcdc$(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 08955180271..9f1af784d22 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -930,6 +930,8 @@ bool cbmc_parse_optionst::process_goto_program( c=coverage_criteriont::MCDC; else if(criterion_string=="cover") c=coverage_criteriont::COVER; + else if(criterion_string=="boundary-values") + c=coverage_criteriont::BOUNDARY; else { error() << "unknown coverage criterion" << eom; @@ -941,8 +943,8 @@ bool cbmc_parse_optionst::process_goto_program( status() << "Instrumenting coverage goals" << eom; - for(const auto & criterion : criteria) - instrument_cover_goals(symbol_table, goto_functions, criterion); + instrument_cover_goalst goals(symbol_table, criteria); + goals.instrument_cover_goals(goto_functions); goto_functions.update(); } diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index 0d1e4d6f741..3ca752337ad 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -23,7 +23,7 @@ SRC = goto_instrument_parse_options.cpp rw_set.cpp \ wmm/event_graph.cpp wmm/pair_collection.cpp \ goto_instrument_main.cpp horn_encoding.cpp \ thread_instrumentation.cpp skip_loops.cpp loop_utils.cpp \ - code_contracts.cpp cover.cpp + code_contracts.cpp cover_utils.cpp cover_mcdc.cpp cover.cpp OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../cpp/cpp$(LIBEXT) \ diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index fba2f5fe4dc..a63981d4b6e 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -16,55 +16,7 @@ Date: May 2016 #include #include "cover.h" - -class basic_blockst -{ -public: - explicit basic_blockst(const goto_programt &_goto_program) - { - bool next_is_target=true; - unsigned block_count=0; - - forall_goto_program_instructions(it, _goto_program) - { - if(next_is_target || it->is_target()) - block_count++; - - block_map[it]=block_count; - - if(!it->source_location.is_nil() && - source_location_map.find(block_count)==source_location_map.end()) - source_location_map[block_count]=it->source_location; - - next_is_target= - it->is_goto() || it->is_function_call() || it->is_assume(); - } - } - - // map program locations to block numbers - typedef std::map block_mapt; - block_mapt block_map; - - // map block numbers to source code locations - typedef std::map source_location_mapt; - source_location_mapt source_location_map; - - inline unsigned operator[](goto_programt::const_targett t) - { - return block_map[t]; - } - - void output(std::ostream &out) - { - 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'; - } -}; +#include "cover_mcdc.h" /*******************************************************************\ @@ -96,31 +48,7 @@ const char *as_string(coverage_criteriont c) /*******************************************************************\ -Function: is_condition - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -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; -} - -/*******************************************************************\ - -Function: collect_conditions_rec +Function: instrument_assertion Inputs: @@ -130,23 +58,20 @@ Function: collect_conditions_rec \*******************************************************************/ -void collect_conditions_rec(const exprt &src, std::set &dest) +void instrument_cover_goalst::instrument_assertion( + goto_programt::instructionst::iterator &insn) { - if(src.id()==ID_address_of) + if(insn->is_assert()) { - return; + insn->guard=false_exprt(); + insn->source_location.set(ID_coverage_criterion, coverage_criterion); + insn->source_location.set_property_class(property_class); } - - for(const auto & op : src.operands()) - collect_conditions_rec(op, dest); - - if(is_condition(src) && !src.is_constant()) - dest.insert(src); } /*******************************************************************\ -Function: collect_conditions +Function: instrument_cover Inputs: @@ -156,192 +81,35 @@ Function: collect_conditions \*******************************************************************/ -std::set collect_conditions(const exprt &src) +void instrument_cover_goalst::instrument_cover( + goto_programt::instructionst::iterator &insn) { - std::set result; - collect_conditions_rec(src, result); - return result; -} - -/*******************************************************************\ - -Function: collect_conditions - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -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(); -} - -/*******************************************************************\ - -Function: collect_operands - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -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); - } -} - -/*******************************************************************\ - -Function: collect_mcdc_controlling_rec - - Inputs: - - Outputs: - - Purpose: 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) + if(insn->is_function_call()) + { + const code_function_callt &code_function_call= + to_code_function_call(insn->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) { - 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); - } - } + const exprt c=code_function_call.arguments()[0]; + std::string comment="condition `"+from_expr(ns, "", c)+"'"; + insn->guard=not_exprt(c); + insn->type=ASSERT; + insn->code.clear(); + insn->source_location.set_comment(comment); + insn->source_location.set(ID_coverage_criterion, coverage_criterion); + insn->source_location.set_property_class(property_class); } } - 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. - **/ - } + else if(insn->is_assert()) + insn->make_skip(); } /*******************************************************************\ -Function: collect_mcdc_controlling +Function: instrument_location Inputs: @@ -351,652 +119,160 @@ Function: collect_mcdc_controlling \*******************************************************************/ -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; -} - -/*******************************************************************\ - -Function: replacement_conjunction - - Inputs: - - Outputs: - - Purpose: 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.size() > 0) 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; -} - -/*******************************************************************\ - -Function: sign_of_expr - - Inputs: E should be the pre-processed output by - ''collect_mcdc_controlling_nested'' - - Outputs: +1 : not negated - -1 : negated - - Purpose: The sign of expr ''e'' within the super-expr ''E'' - -\*******************************************************************/ - -std::set sign_of_expr(const exprt &e, const exprt &E) +void instrument_cover_goalst::instrument_location( + goto_programt::instructionst::iterator &insn, + goto_programt &goto_program, + basic_blockst &basic_blocks, + std::set &blocks_done) { - 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; - } + if(insn->is_assert()) + insn->make_skip(); - // or, ''E'' is the negation of ''e''? - if(E.id()==ID_not) + unsigned block_nr=basic_blocks[insn]; + if(blocks_done.insert(block_nr).second) { - if(e==E.op0()) - { - signs.insert(-1); - return signs; - } - } + std::string b=i2string(block_nr); + std::string id=id2string(insn->function)+"#"+b; + source_locationt source_location= + basic_blocks.source_location_map[block_nr]; - /** - * 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) + if(!source_location.get_file().empty() && + source_location.get_file()[0]!='<') { - 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()); + std::string comment="block "+b; + goto_program.insert_before_swap(insn); + insn->make_assertion(false_exprt()); + insn->source_location=source_location; + insn->source_location.set_comment(comment); + insn->source_location.set(ID_coverage_criterion, coverage_criterion); + insn->source_location.set_property_class(property_class); + + insn++; } } - - return signs; } /*******************************************************************\ -Function: remove_repetition +Function: instrument_branch Inputs: Outputs: - Purpose: 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. + Purpose: \*******************************************************************/ -void remove_repetition(std::set &exprs) +void instrument_cover_goalst::instrument_branch( + goto_programt::instructionst::iterator &insn, + goto_programt &goto_program, + basic_blockst &basic_blocks) { - // 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(); + if(insn->is_assert()) + insn->make_skip(); - for(auto &x: exprs) + if(insn==goto_program.instructions.begin()) { - 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; -} + // we want branch coverage to imply 'entry point of function' + // coverage + std::string comment= + "function "+id2string(insn->function)+" entry point"; -/*******************************************************************\ - -Function: eval_expr + source_locationt source_location=insn->source_location; - Inputs: - - Outputs: - - Purpose: 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; + goto_programt::targett t=goto_program.insert_before(insn); + 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); } -} - -/*******************************************************************\ - -Function: values_of_atomic_exprs - - Inputs: - - Outputs: - - Purpose: 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) + if(insn->is_goto() && !insn->guard.is_true()) { - std::set signs=sign_of_expr(c, e); - if(signs.size()==0) - { - // ''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; + std::string b=i2string(basic_blocks[insn]); + std::string true_comment= + "function "+id2string(insn->function)+" block "+b+" branch true"; + std::string false_comment= + "function "+id2string(insn->function)+" block "+b+" branch false"; - atomic_exprs.insert( - std::pair(c, *signs.begin())); - } - return atomic_exprs; -} + exprt guard=insn->guard; + source_locationt source_location=insn->source_location; -/*******************************************************************\ + goto_program.insert_before_swap(insn); + insn->make_assertion(not_exprt(guard)); + insn->source_location=source_location; + insn->source_location.set_comment(true_comment); + insn->source_location.set(ID_coverage_criterion, coverage_criterion); + insn->source_location.set_property_class(property_class); -Function: is_mcdc_pair + goto_program.insert_before_swap(insn); + insn->make_assertion(guard); + insn->source_location=source_location; + insn->source_location.set_comment(false_comment); + insn->source_location.set(ID_coverage_criterion, coverage_criterion); + insn->source_location.set_property_class(property_class); - Inputs: - - Outputs: - - Purpose: 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++; + insn++; + insn++; } - - if(diff_count==1) return true; - else return false; } /*******************************************************************\ -Function: has_mcdc_pair +Function: instrument_condition Inputs: Outputs: - Purpose: To check if we can find the mcdc pair of the - input ''expr_set'' regarding the atomic expr ''c'' + Purpose: \*******************************************************************/ -bool has_mcdc_pair( - const exprt &c, - const std::set &expr_set, - const std::set &conditions, - const exprt &decision) +void instrument_cover_goalst::instrument_condition( + goto_programt::instructionst::iterator &insn, + goto_programt &goto_program) { - for(auto y1 : expr_set) - { - for(auto y2 : expr_set) - { - if(is_mcdc_pair(y1, y2, c, conditions, decision)) - { - return true; - } - } - } - return false; -} - -/*******************************************************************\ + if(insn->is_assert()) + insn->make_skip(); -Function: minimize_mcdc_controlling - - Inputs: The input ''controlling'' should have been processed by - ''collect_mcdc_controlling_nested'' - and - ''remove_repetition'' - - Outputs: - - Purpose: 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. - -\*******************************************************************/ - -void minimize_mcdc_controlling( - std::set &controlling, - const exprt &decision) -{ - // to obtain the set of atomic conditions - std::set conditions; - for(auto &x: controlling) + // Conditions are all atomic predicates in the programs. { - std::set new_conditions = collect_conditions(x); - conditions.insert(new_conditions.begin(), new_conditions.end()); - } + const std::set conditions=collect_conditions(insn); - 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 breaked. - * - * Note: implementaion 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; - } - } + const source_locationt source_location=insn->source_location; - // 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) + for(const auto & c : conditions) { - controlling=new_controlling; + const std::string c_string=from_expr(ns, "", c); + + const std::string comment_t="condition `"+c_string+"' true"; + goto_program.insert_before_swap(insn); + insn->make_assertion(c); + insn->source_location=source_location; + insn->source_location.set_comment(comment_t); + insn->source_location.set(ID_coverage_criterion, coverage_criterion); + insn->source_location.set_property_class(property_class); + + const std::string comment_f="condition `"+c_string+"' false"; + goto_program.insert_before_swap(insn); + insn->make_assertion(not_exprt(c)); + insn->source_location=source_location; + insn->source_location.set_comment(comment_f); + insn->source_location.set(ID_coverage_criterion, coverage_criterion); + insn->source_location.set_property_class(property_class); } - else break; - } -} - -/*******************************************************************\ -Function: collect_decisions_rec - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -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); + for(std::size_t i=0; i collect_decisions(const exprt &src) +void instrument_cover_goalst::instrument_decision( + goto_programt::instructionst::iterator &insn, + goto_programt &goto_program) { - std::set result; - collect_decisions_rec(src, result); - return result; -} - -/*******************************************************************\ - -Function: collect_decisions - - Inputs: - - Outputs: - - Purpose: + if(insn->is_assert()) + insn->make_skip(); -\*******************************************************************/ - -std::set collect_decisions(const goto_programt::const_targett t) -{ - switch(t->type) + // Decisions are maximal Boolean combinations of conditions. { - case GOTO: - case ASSERT: - return collect_decisions(t->guard); + const std::set decisions=collect_decisions(insn); - case ASSIGN: - case FUNCTION_CALL: - return collect_decisions(t->code); + const source_locationt source_location=insn->source_location; - default:; - } + for(const auto & d : decisions) + { + const std::string d_string=from_expr(ns, "", d); + + const std::string comment_t="decision `"+d_string+"' true"; + goto_program.insert_before_swap(insn); + insn->make_assertion(d); + insn->source_location=source_location; + insn->source_location.set_comment(comment_t); + insn->source_location.set(ID_coverage_criterion, coverage_criterion); + insn->source_location.set_property_class(property_class); + + const std::string comment_f="decision `"+d_string+"' false"; + goto_program.insert_before_swap(insn); + insn->make_assertion(not_exprt(d)); + insn->source_location=source_location; + insn->source_location.set_comment(comment_f); + insn->source_location.set(ID_coverage_criterion, coverage_criterion); + insn->source_location.set_property_class(property_class); + } - return std::set(); + for(std::size_t i=0; i blocks_done; // ignore if built-in library if(!goto_program.instructions.empty() && - has_prefix(id2string(goto_program.instructions.front().source_location.get_file()), - "is_assert()) - { - i_it->guard=false_exprt(); - i_it->source_location.set(ID_coverage_criterion, coverage_criterion); - i_it->source_location.set_property_class(property_class); - } - break; - - case coverage_criteriont::COVER: - // 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(); - 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); - } - } - else if(i_it->is_assert()) - i_it->make_skip(); - break; + coverage_criterion=as_string(criterion); + property_class="coverage"; - case coverage_criteriont::LOCATION: - if(i_it->is_assert()) - i_it->make_skip(); + instrument_mcdc_goalst mcdc( + ns, criteria, coverage_criterion, property_class); + Forall_goto_program_instructions(i_it, goto_program) + { + switch(criterion) { - unsigned block_nr=basic_blocks[i_it]; - if(blocks_done.insert(block_nr).second) - { - std::string b=i2string(block_nr); - std::string id=id2string(i_it->function)+"#"+b; - source_locationt source_location= - basic_blocks.source_location_map[block_nr]; - - if(!source_location.get_file().empty() && - source_location.get_file()[0]!='<') - { - std::string comment="block "+b; - 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++; - } - } - } - break; - - case coverage_criteriont::BRANCH: - if(i_it->is_assert()) - i_it->make_skip(); + case coverage_criteriont::ASSERTION: + // turn into 'assert(false)' to avoid simplification + instrument_assertion(i_it); + break; - if(i_it==goto_program.instructions.begin()) - { - // we want branch coverage to imply 'entry point of function' - // coverage - std::string comment= - "function "+id2string(i_it->function)+" 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); - } + case coverage_criteriont::COVER: + // turn __CPROVER_cover(x) into 'assert(!x)' + instrument_cover(i_it); + break; - if(i_it->is_goto() && !i_it->guard.is_true()) - { - std::string b=i2string(basic_blocks[i_it]); - std::string true_comment= - "function "+id2string(i_it->function)+" block "+b+" branch true"; - std::string false_comment= - "function "+id2string(i_it->function)+" block "+b+" branch false"; - - exprt guard=i_it->guard; - 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; - 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); - - 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++; - i_it++; - } - break; + case coverage_criteriont::LOCATION: + instrument_location(i_it, goto_program, basic_blocks, blocks_done); + break; - case coverage_criteriont::CONDITION: - if(i_it->is_assert()) - i_it->make_skip(); + case coverage_criteriont::BRANCH: + instrument_branch(i_it, goto_program, basic_blocks); + break; - // Conditions are all atomic predicates in the programs. - { - 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"; - 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); - - 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); - } - - for(std::size_t i=0; iis_assert()) - i_it->make_skip(); + case coverage_criteriont::DECISION: + instrument_decision(i_it, goto_program); + break; - // Decisions are maximal Boolean combinations of conditions. - { - 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"; - 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); - - 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); - } - - for(std::size_t i=0; iis_assert()) + i_it->make_skip(); + break; - case coverage_criteriont::MCDC: - if(i_it->is_assert()) - i_it->make_skip(); + case coverage_criteriont::MCDC: + mcdc.instrument_mcdc(i_it, goto_program, basic_blocks, blocks_done); + break; - // 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. - { - 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"; - 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); - - 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); - } - - 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. - 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+"'"; - - 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); - } - - for(std::size_t i=0; iis_assert()) - i_it->make_skip(); - break; - - default:; } } - } /*******************************************************************\ @@ -1367,10 +412,8 @@ Function: instrument_cover_goals \*******************************************************************/ -void instrument_cover_goals( - const symbol_tablet &symbol_table, - goto_functionst &goto_functions, - coverage_criteriont criterion) +void instrument_cover_goalst::instrument_cover_goals( + goto_functionst &goto_functions) { Forall_goto_functions(f_it, goto_functions) { @@ -1378,6 +421,6 @@ void instrument_cover_goals( f_it->first=="__CPROVER_initialize") continue; - instrument_cover_goals(symbol_table, f_it->second.body, criterion); + instrument_cover_goals(f_it->second.body); } } diff --git a/src/goto-instrument/cover.h b/src/goto-instrument/cover.h index 8081ad77396..420360f9b5b 100644 --- a/src/goto-instrument/cover.h +++ b/src/goto-instrument/cover.h @@ -11,20 +11,55 @@ Date: May 2016 #ifndef CPROVER_GOTO_INSTRUMENT_COVER_H #define CPROVER_GOTO_INSTRUMENT_COVER_H -#include +#include "cover_utils.h" -enum class coverage_criteriont { - LOCATION, BRANCH, DECISION, CONDITION, - PATH, MCDC, ASSERTION, COVER }; +class instrument_cover_goalst : public instrument_cover_utilst +{ +public: + instrument_cover_goalst( + const symbol_tablet &_symbol_table, + const std::set &_criteria): + ns(_symbol_table), + criteria(_criteria) + { + } -void instrument_cover_goals( - const symbol_tablet &symbol_table, - goto_programt &goto_program, - coverage_criteriont); + void instrument_cover_goals( + goto_programt &goto_program); -void instrument_cover_goals( - const symbol_tablet &symbol_table, - goto_functionst &goto_functions, - coverage_criteriont); + void instrument_cover_goals( + goto_functionst &goto_functions); + +private: + void instrument_assertion( + goto_programt::instructionst::iterator &insn); + + void instrument_cover( + goto_programt::instructionst::iterator &insn); + + void instrument_location( + goto_programt::instructionst::iterator &insn, + goto_programt &goto_program, + basic_blockst &basic_blocks, + std::set &blocks_done); + + void instrument_branch( + goto_programt::instructionst::iterator &insn, + goto_programt &goto_program, + basic_blockst &basic_blocks); + + void instrument_condition( + goto_programt::instructionst::iterator &insn, + goto_programt &goto_program); + + void instrument_decision( + goto_programt::instructionst::iterator &insn, + goto_programt &goto_program); + + const namespacet ns; + const std::set &criteria; + irep_idt coverage_criterion; + irep_idt property_class; +}; #endif // CPROVER_GOTO_INSTRUMENT_COVER_H diff --git a/src/goto-instrument/cover_mcdc.cpp b/src/goto-instrument/cover_mcdc.cpp new file mode 100644 index 00000000000..a94810c75d8 --- /dev/null +++ b/src/goto-instrument/cover_mcdc.cpp @@ -0,0 +1,126 @@ +/*******************************************************************\ + +Module: Coverage Instrumentation for MCDC + +Author: Daniel Kroening + +Date: May 2016 + +\*******************************************************************/ + +#include + +#include "cover_mcdc.h" + +/*******************************************************************\ + +Function: instrument_mcdc + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void instrument_mcdc_goalst::instrument_mcdc( + goto_programt::instructionst::iterator &insn, + goto_programt &goto_program, + basic_blockst &basic_blocks, + std::set &blocks_done) +{ + if(insn->is_assert()) + insn->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. + + const std::set conditions=collect_conditions(insn); + + const std::set decisions=collect_decisions(insn); + + std::set both; + std::set_union(conditions.begin(), conditions.end(), + decisions.begin(), decisions.end(), + inserter(both, both.end())); + + const source_locationt source_location=insn->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"; + goto_program.insert_before_swap(insn); + insn->make_assertion(not_exprt(p)); + insn->source_location=source_location; + insn->source_location.set_comment(comment_t); + insn->source_location.set(ID_coverage_criterion, coverage_criterion); + insn->source_location.set_property_class(property_class); + + std::string comment_f=description+" `"+p_string+"' false"; + goto_program.insert_before_swap(insn); + insn->make_assertion(p); + insn->source_location=source_location; + insn->source_location.set_comment(comment_f); + insn->source_location.set(ID_coverage_criterion, coverage_criterion); + insn->source_location.set_property_class(property_class); + } + + bool boundary_values_analysis= + criteria.find(coverage_criteriont::BOUNDARY)!=criteria.end(); + std::set controlling; + for(auto &dec : decisions) + { + std::set ctrl=collect_mcdc_controlling_nested({dec}); + if(boundary_values_analysis) + { + auto res=decision_expansion(dec); + ctrl.insert(res.begin(), res.end()); + } + remove_repetition(ctrl); + minimize_mcdc_controlling(ctrl, dec); + controlling.insert(ctrl.begin(), ctrl.end()); + } + + if(boundary_values_analysis) + { + std::set boundary_controlling; + for(auto &x : controlling) + { + auto res=non_ordered_expr_expansion(x); + boundary_controlling.insert(res.begin(), res.end()); + } + controlling=boundary_controlling; + remove_repetition(controlling); + } + + for(const auto & p : controlling) + { + std::string p_string=from_expr(ns, "", p); + + std::string description= + "MC/DC independence condition `"+p_string+"'"; + + goto_program.insert_before_swap(insn); + insn->make_assertion(not_exprt(p)); + insn->source_location=source_location; + insn->source_location.set_comment(description); + insn->source_location.set(ID_coverage_criterion, coverage_criterion); + insn->source_location.set_property_class(property_class); + } + + for(std::size_t i=0; i &_criteria, + const irep_idt &_coverage_criterion, + const irep_idt &_property_class): + ns(_ns), + criteria(_criteria), + coverage_criterion(_coverage_criterion), + property_class(_property_class) + { + } + + void instrument_mcdc( + goto_programt::instructionst::iterator &insn, + goto_programt &goto_program, + basic_blockst &basic_blocks, + std::set &blocks_done); + +private: + const namespacet ns; + const std::set &criteria; + const irep_idt coverage_criterion; + const irep_idt property_class; +}; + +#endif // CPROVER_GOTO_INSTRUMENT_COVER_MCDC_H diff --git a/src/goto-instrument/cover_utils.cpp b/src/goto-instrument/cover_utils.cpp new file mode 100644 index 00000000000..80c480f1f0b --- /dev/null +++ b/src/goto-instrument/cover_utils.cpp @@ -0,0 +1,1228 @@ +/*******************************************************************\ + +Module: Coverage Instrumentation + +Author: Daniel Kroening + +Date: May 2016 + +\*******************************************************************/ + +#include +#include + +#include +#include +#include + +#include "cover_utils.h" + +/*******************************************************************\ + +Function: is_condition + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +static 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; +} + +/*******************************************************************\ + +Function: collect_conditions_rec + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +static 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); +} + +/*******************************************************************\ + +Function: collect_conditions + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +static std::set collect_conditions_as_expr( + const exprt &src) +{ + std::set result; + collect_conditions_rec(src, result); + return result; +} + +/*******************************************************************\ + +Function: collect_conditions + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +std::set instrument_cover_utilst::collect_conditions( + const goto_programt::const_targett t) +{ + switch(t->type) + { + case GOTO: + case ASSERT: + return collect_conditions_as_expr(t->guard); + + case ASSIGN: + case FUNCTION_CALL: + return collect_conditions_as_expr(t->code); + + default: {} + } + + return std::set(); +} + +/*******************************************************************\ + +Function: collect_operands + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +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); + } +} + +/*******************************************************************\ + +Function: non_ordered_predicate_expansion + + Inputs: + + Outputs: + + Purpose: A non-ordered predicate contains <=, !=, >= + +\*******************************************************************/ + +std::set non_ordered_predicate_expansion( + const exprt &src) +{ + std::set result; + // the expansion of "<=" is "<" and "==" + if(src.id()==ID_le) + { + exprt e1(src); + e1.id(ID_lt); + result.insert(e1); + + exprt e2(src); + e1.id(ID_equal); + result.insert(e2); + } + // the expansion of ">=" is ">" and "==" + else if(src.id()==ID_ge) + { + exprt e1(src); + e1.id(ID_gt); + result.insert(e1); + + exprt e2(src); + e1.id(ID_equal); + result.insert(e2); + } + else if(src.id()==ID_notequal) + { + if(src.op0().type().id()==ID_c_bool + || src.op1().type().id()==ID_c_bool) + { + return result; + } + // the expansion of "==" is ">" and "<" + exprt e1(ID_gt); + e1.type().id(src.type().id()); + e1.operands().push_back(src.op0()); + e1.operands().push_back(src.op1()); + result.insert(e1); + + exprt e2(ID_lt); + e2.type().id(src.type().id()); + e2.operands().push_back(src.op0()); + e2.operands().push_back(src.op1()); + result.insert(e2); + } + + return result; +} + +/*******************************************************************\ + +Function: ordered_negation + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +std::set ordered_negation(const exprt &src) +{ + std::set result; + // the negation of "==" is "<" and ">" + if(src.id()==ID_equal) + { + exprt e1(src); + e1.id(ID_lt); + result.insert(e1); + + exprt e2(src); + e2.id(ID_gt); + result.insert(e2); + } + // the negation of "<" is "==" and ">" + else if(src.id()==ID_lt) + { + exprt e1(src); + e1.id(ID_equal); + result.insert(e1); + + exprt e2(src); + e2.id(ID_gt); + result.insert(e2); + } + // the negation of "<=" is ">" + else if(src.id()==ID_le) + { + exprt e1(src); + e1.id(ID_gt); + result.insert(e1); + } + // the negation of ">=" is "<" + else if(src.id()==ID_ge) + { + exprt e1(src); + e1.id(ID_lt); + result.insert(e1); + } + // the negation of ">" is "==" and "<" + else if(src.id()==ID_gt) + { + exprt e1(src); + e1.id(ID_equal); + result.insert(e1); + + exprt e2(src); + e2.id(ID_lt); + result.insert(e2); + } + // the negation of "!=" is "==" + else if(src.id()==ID_notequal) + { + exprt e1(src); + e1.id(ID_equal); + result.insert(e1); + } + + return result; +} + +/*******************************************************************\ + +Function: is_arithmetic_predicate + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +bool is_arithmetic_predicate(const exprt &src) +{ + return (src.id()==ID_lt + || src.id()==ID_le + || src.id()==ID_equal + || src.id()==ID_ge + || src.id()==ID_gt + || src.id()==ID_notequal); +} + +/*******************************************************************\ + +Function: replacement_and_conjunction + + Inputs: + + Outputs: + + Purpose: To replace the i-th expr of ''operands'' with each + expr inside ''replacement_exprs''. + +\*******************************************************************/ + +std::set replacement_and_conjunction( + const std::set &replacement_exprs, + const std::vector &operands, + const std::size_t i) +{ + std::set result; + for(auto &y : replacement_exprs) + { + assert(operands.size()>i); + std::vector others(operands); + others[i]=y; + exprt c=conjunction(others); + result.insert(c); + } + return result; +} + +/*******************************************************************\ + +Function: non_ordered_expr_expansion + + Inputs: + + Outputs: + + Purpose: To expand all non ordered predicates within an expr + +\*******************************************************************/ + +std::set instrument_cover_utilst::non_ordered_expr_expansion( + const exprt &src) +{ + if(src.id()==ID_not && is_arithmetic_predicate(src.op0())) + { + return ordered_negation(src.op0()); + } + + std::set result; + std::vector operands;; + collect_operands(src, operands); + // expand negations and non-ordered predicates + for(std::size_t i=0; i=' or '!=' + std::set expanded_op; + if(operands[i].id()==ID_not) + { + const exprt &no=operands[i].op0(); + if(is_arithmetic_predicate(no)) + { + expanded_op=ordered_negation(no); + } + } + else + { + if(operands[i].id()==ID_le + || operands[i].id()==ID_ge + || operands[i].id()==ID_notequal) + { + expanded_op=non_ordered_predicate_expansion(operands[i]); + } + } + if(expanded_op.empty()) continue; + auto re=replacement_and_conjunction(expanded_op, operands, i); + for(auto &x : re) + { + auto rec_result=non_ordered_expr_expansion(x); + result.insert(rec_result.begin(), rec_result.end()); + } + // The loop can terminate as long as one 'op' has been expanded, + // since the recursive call will handle other expansions. + return result; + } + return {src}; +} + +/*******************************************************************\ + +Function: decision_expansion + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +std::set instrument_cover_utilst::decision_expansion(const exprt &dec) +{ + std::set ctrl; + // dec itself may be a non-ordered predicate + exprt d(dec); + if(d.id()==ID_not) d=d.op0(); + if(is_arithmetic_predicate(d)) + { + auto res=non_ordered_expr_expansion(d); + ctrl.insert(res.begin(), res.end()); + d.make_not(); + res=non_ordered_expr_expansion(d); + ctrl.insert(res.begin(), res.end()); + } + return ctrl; +} + +/*******************************************************************\ + +Function: collect_mcdc_controlling_rec + + Inputs: + + Outputs: + + Purpose: To recursively collect controlling exprs for + for mcdc coverage. + +\*******************************************************************/ + +void instrument_cover_utilst::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. + **/ + } +} + +/*******************************************************************\ + +Function: collect_mcdc_controlling + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +std::set instrument_cover_utilst::collect_mcdc_controlling( + const std::set &decisions) +{ + std::set result; + + for(const auto &d : decisions) + { + collect_mcdc_controlling_rec(d, { }, result); + } + + return result; +} + + +/*******************************************************************\ + +Function: collect_mcdc_controlling_nested + + Inputs: + + Outputs: + + Purpose: This nested method iteratively applies + ''collect_mcdc_controlling'' to every non-atomic expr + within a decision + +\*******************************************************************/ + +std::set instrument_cover_utilst::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 used to hold the + * temporary expansion. + **/ + s1.insert(src); + + // dual-loop structure to eliminate complex + // non-atomic-conditional terms + bool changed=true; + while(changed) + { + 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_and_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.swap(s2); + s2.clear(); + if(!changed) {break;} + } + + // The expansions of each ''src'' should be added into + // the ''result'' + result.insert(s1.begin(), s1.end()); + } + + return result; +} + +/*******************************************************************\ + +Function: sign_of_expr + + Inputs: E should be the pre-processed output by + ''collect_mcdc_controlling_nested'' + + Outputs: +1 : not negated + -1 : negated + + Purpose: The sign of expr ''e'' within the super-expr ''E'' + +\*******************************************************************/ + +std::set instrument_cover_utilst::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; +} + +/*******************************************************************\ + +Function: remove_repetition + + Inputs: + + Outputs: + + Purpose: 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 instrument_cover_utilst::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_as_expr(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); + std::size_t 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.swap(new_exprs); +} + +/*******************************************************************\ + +Function: eval_expr + + Inputs: + + Outputs: + + Purpose: To evaluate the value of expr ''src'', according to + the atomic expr values + +\*******************************************************************/ + +bool instrument_cover_utilst::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; + } +} + +/*******************************************************************\ + +Function: values_of_atomic_exprs + + Inputs: + + Outputs: + + Purpose: To obtain values of atomic exprs within the super expr + +\*******************************************************************/ + +std::map instrument_cover_utilst::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; +} + +/*******************************************************************\ + +Function: is_mcdc_pair + + Inputs: + + Outputs: + + Purpose: 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 instrument_cover_utilst::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; +} + +/*******************************************************************\ + +Function: has_mcdc_pair + + Inputs: + + Outputs: + + Purpose: To check if we can find the mcdc pair of the + input ''expr_set'' regarding the atomic expr ''c'' + +\*******************************************************************/ + +bool instrument_cover_utilst::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; +} + +/*******************************************************************\ + +Function: minimize_mcdc_controlling + + Inputs: The input ''controlling'' should have been processed by + ''collect_mcdc_controlling_nested'' + and + ''remove_repetition'' + + Outputs: + + Purpose: 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. + +\*******************************************************************/ + +void instrument_cover_utilst::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_as_expr(x); + conditions.insert(new_conditions.begin(), new_conditions.end()); + } + + bool ctrl_update=true; + while(ctrl_update) + { + ctrl_update=false; + std::set new_controlling; + /** + * 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 breaked. + * + * Note: implementaion 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.swap(new_controlling); + } + else + break; + } +} + +/*******************************************************************\ + +Function: collect_decisions_rec + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void instrument_cover_utilst::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); + } +} + +/*******************************************************************\ + +Function: collect_decisions + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +std::set instrument_cover_utilst::collect_decisions(const exprt &src) +{ + std::set result; + collect_decisions_rec(src, result); + return result; +} + +/*******************************************************************\ + +Function: collect_decisions + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +std::set instrument_cover_utilst::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_utils.h b/src/goto-instrument/cover_utils.h new file mode 100644 index 00000000000..b167720de47 --- /dev/null +++ b/src/goto-instrument/cover_utils.h @@ -0,0 +1,141 @@ +/*******************************************************************\ + +Module: Coverage Instrumentation Utils + +Author: Daniel Kroening + +Date: May 2016 + +\*******************************************************************/ + +#ifndef CPROVER_GOTO_INSTRUMENT_COVER_UTILS_H +#define CPROVER_GOTO_INSTRUMENT_COVER_UTILS_H + +#include + +enum class coverage_criteriont +{ + LOCATION, BRANCH, DECISION, CONDITION, + PATH, MCDC, BOUNDARY, ASSERTION, COVER +}; + +class basic_blockst +{ +public: + explicit basic_blockst(const goto_programt &_goto_program) + { + bool next_is_target=true; + unsigned block_count=0; + + forall_goto_program_instructions(it, _goto_program) + { + if(next_is_target || it->is_target()) + block_count++; + + block_map[it]=block_count; + + if(!it->source_location.is_nil() && + source_location_map.find(block_count)==source_location_map.end()) + source_location_map[block_count]=it->source_location; + + next_is_target= + it->is_goto() || it->is_function_call() || it->is_assume(); + } + } + + // map program locations to block numbers + typedef std::map block_mapt; + block_mapt block_map; + + // map block numbers to source code locations + typedef std::map source_location_mapt; + source_location_mapt source_location_map; + + inline unsigned operator[](goto_programt::const_targett t) + { + return block_map[t]; + } + + void output(std::ostream &out) + { + 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'; + } +}; + +class instrument_cover_utilst +{ +public: + instrument_cover_utilst() + { + } + +protected: + std::set collect_conditions( + const goto_programt::const_targett t); + + static std::set non_ordered_expr_expansion( + const exprt &src); + + std::set decision_expansion( + const exprt &dec); + + void collect_mcdc_controlling_rec( + const exprt &src, + const std::vector &conditions, + std::set &result); + + std::set collect_mcdc_controlling( + const std::set &decisions); + + std::set collect_mcdc_controlling_nested( + const std::set &decisions); + + std::set sign_of_expr( + const exprt &e, + const exprt &E); + + void remove_repetition(std::set &exprs); + + bool eval_expr( + const std::map &atomic_exprs, + const exprt &src); + + std::map values_of_atomic_exprs( + const exprt &e, + const std::set &conditions); + + bool is_mcdc_pair( + const exprt &e1, + const exprt &e2, + const exprt &c, + const std::set &conditions, + const exprt &decision); + + bool has_mcdc_pair( + const exprt &c, + const std::set &expr_set, + const std::set &conditions, + const exprt &decision); + + void minimize_mcdc_controlling( + std::set &controlling, + const exprt &decision); + + void collect_decisions_rec( + const exprt &src, + std::set &dest); + + std::set collect_decisions( + const goto_programt::const_targett t); + + std::set collect_decisions( + const exprt &src); +}; + +#endif // CPROVER_GOTO_INSTRUMENT_COVER_UTILS_H diff --git a/src/symex/Makefile b/src/symex/Makefile index 5a66801eec4..35a32dda50a 100644 --- a/src/symex/Makefile +++ b/src/symex/Makefile @@ -16,6 +16,8 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../goto-symex/rewrite_union$(OBJEXT) \ ../pointer-analysis/dereference$(OBJEXT) \ ../goto-instrument/cover$(OBJEXT) \ + ../goto-instrument/cover_utils$(OBJEXT) \ + ../goto-instrument/cover_mcdc$(OBJEXT) \ ../path-symex/path-symex$(LIBEXT) INCLUDES= -I .. diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp index 7a9227e6f58..a11581d37fc 100644 --- a/src/symex/symex_parse_options.cpp +++ b/src/symex/symex_parse_options.cpp @@ -388,6 +388,8 @@ bool symex_parse_optionst::process_goto_program(const optionst &options) c=coverage_criteriont::MCDC; else if(criterion=="cover") c=coverage_criteriont::COVER; + else if(criterion=="boundary-values") + c=coverage_criteriont::BOUNDARY; else { error() << "unknown coverage criterion" << eom; @@ -395,7 +397,8 @@ bool symex_parse_optionst::process_goto_program(const optionst &options) } status() << "Instrumenting coverge goals" << eom; - instrument_cover_goals(symbol_table, goto_model.goto_functions, c); + instrument_cover_goalst goals(symbol_table, {c}); + goals.instrument_cover_goals(goto_model.goto_functions); goto_model.goto_functions.update(); }