From 3fee77e659c77e4b3e4c7f2bf142f5257b75fea4 Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Mon, 7 Nov 2016 12:25:59 +0000 Subject: [PATCH 01/17] add test cases related to boundary values by Youcheng Signed-off-by: Lucas Cordeiro --- .../cbmc-cover/mcdc-boundary-values1/main.c | 11 ++++++++++ .../mcdc-boundary-values1/test.desc | 14 ++++++++++++ .../cbmc-cover/mcdc-boundary-values2/main.c | 12 ++++++++++ .../mcdc-boundary-values2/test.desc | 22 +++++++++++++++++++ .../cbmc-cover/mcdc-boundary-values3/main.c | 13 +++++++++++ .../mcdc-boundary-values3/test.desc | 14 ++++++++++++ .../cbmc-cover/mcdc-boundary-values4/main.c | 18 +++++++++++++++ .../mcdc-boundary-values4/test.desc | 13 +++++++++++ 8 files changed, 117 insertions(+) create mode 100644 regression/cbmc-cover/mcdc-boundary-values1/main.c create mode 100644 regression/cbmc-cover/mcdc-boundary-values1/test.desc create mode 100644 regression/cbmc-cover/mcdc-boundary-values2/main.c create mode 100644 regression/cbmc-cover/mcdc-boundary-values2/test.desc create mode 100644 regression/cbmc-cover/mcdc-boundary-values3/main.c create mode 100644 regression/cbmc-cover/mcdc-boundary-values3/test.desc create mode 100644 regression/cbmc-cover/mcdc-boundary-values4/main.c create mode 100644 regression/cbmc-cover/mcdc-boundary-values4/test.desc 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..c7192130ec5 --- /dev/null +++ b/regression/cbmc-cover/mcdc-boundary-values1/test.desc @@ -0,0 +1,14 @@ +CORE +main.c +--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..38c34b6c859 --- /dev/null +++ b/regression/cbmc-cover/mcdc-boundary-values2/test.desc @@ -0,0 +1,22 @@ +CORE +main.c +--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..ab20b309e6d --- /dev/null +++ b/regression/cbmc-cover/mcdc-boundary-values3/test.desc @@ -0,0 +1,14 @@ +CORE +main.c +--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..eb14ca3a588 --- /dev/null +++ b/regression/cbmc-cover/mcdc-boundary-values4/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--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 From 858c36f7b7c71b3ad2683ea1bdcd2bcc4abd210f Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Mon, 19 Dec 2016 10:38:37 +0000 Subject: [PATCH 02/17] Fixed merge conflicts Updated cover.cpp and cover.h files to fix merge conflicts. --- src/cbmc/Makefile | 1 + src/cbmc/cbmc_parse_options.cpp | 2 + src/goto-instrument/Makefile | 2 +- src/goto-instrument/cover.cpp | 482 ++++++++++++++++-------------- src/goto-instrument/cover.h | 2 +- src/symex/Makefile | 1 + src/symex/symex_parse_options.cpp | 2 + 7 files changed, 261 insertions(+), 231 deletions(-) diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile index 79f7a4fd982..e11b6c0be4a 100644 --- a/src/cbmc/Makefile +++ b/src/cbmc/Makefile @@ -22,6 +22,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../goto-instrument/full_slicer$(OBJEXT) \ ../goto-instrument/nondet_static$(OBJEXT) \ ../goto-instrument/cover$(OBJEXT) \ + ../goto-instrument/cover_boundary_values$(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..fb430a96a7f 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; diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index 0d1e4d6f741..854e5be00f6 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.cpp cover_boundary_values.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..07aeafd1714 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -357,14 +357,15 @@ std::set collect_mcdc_controlling( std::set result; for(const auto &d : decisions) + { collect_mcdc_controlling_rec(d, { }, result); - + } return result; } /*******************************************************************\ -Function: replacement_conjunction +Function: replacement_and_conjunction Inputs: @@ -375,7 +376,7 @@ Function: replacement_conjunction \*******************************************************************/ -std::set replacement_conjunction( +std::set replacement_and_conjunction( const std::set &replacement_exprs, const std::vector &operands, const std::size_t i) @@ -477,7 +478,7 @@ std::set collect_mcdc_controlling_nested( // To replace a non-atomic expr with its expansion std::set co= - replacement_conjunction(res, operands, i); + replacement_and_conjunction(res, operands, i); s2.insert(co.begin(), co.end()); if(res.size() > 0) break; } @@ -1058,7 +1059,7 @@ Function: instrument_cover_goals void instrument_cover_goals( const symbol_tablet &symbol_table, goto_programt &goto_program, - coverage_criteriont criterion) + const std::set &criteria) { const namespacet ns(symbol_table); basic_blockst basic_blocks(goto_program); @@ -1069,290 +1070,313 @@ void instrument_cover_goals( 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; + const irep_idt coverage_criterion=as_string(criterion); + const irep_idt property_class="coverage"; - case coverage_criteriont::COVER: - // turn __CPROVER_cover(x) into 'assert(!x)' - if(i_it->is_function_call()) + Forall_goto_program_instructions(i_it, goto_program) + { + switch(criterion) { - 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) + case coverage_criteriont::ASSERTION: + // turn into 'assert(false)' to avoid simplification + if(i_it->is_assert()) { - 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->guard=false_exprt(); 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; - - case coverage_criteriont::LOCATION: - if(i_it->is_assert()) - i_it->make_skip(); + break; - { - unsigned block_nr=basic_blocks[i_it]; - if(blocks_done.insert(block_nr).second) + case coverage_criteriont::COVER: + // turn __CPROVER_cover(x) into 'assert(!x)' + if(i_it->is_function_call()) { - 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]!='<') + 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) { - std::string comment="block "+b; - goto_program.insert_before_swap(i_it); - i_it->make_assertion(false_exprt()); - i_it->source_location=source_location; + 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++; } } - } - break; - - case coverage_criteriont::BRANCH: - if(i_it->is_assert()) - 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= - "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); - } + else if(i_it->is_assert()) + i_it->make_skip(); + 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: + if(i_it->is_assert()) + i_it->make_skip(); - case coverage_criteriont::CONDITION: - if(i_it->is_assert()) - i_it->make_skip(); + { + 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; - // Conditions are all atomic predicates in the programs. - { - const std::set conditions=collect_conditions(i_it); + case coverage_criteriont::BRANCH: + if(i_it->is_assert()) + i_it->make_skip(); - const source_locationt source_location=i_it->source_location; + 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); + } - for(const auto & c : conditions) + if(i_it->is_goto() && !i_it->guard.is_true()) { - const std::string c_string=from_expr(ns, "", c); + 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; - const std::string comment_t="condition `"+c_string+"' true"; goto_program.insert_before_swap(i_it); - i_it->make_assertion(c); + i_it->make_assertion(not_exprt(guard)); i_it->source_location=source_location; - i_it->source_location.set_comment(comment_t); + 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); - 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->make_assertion(guard); i_it->source_location=source_location; - i_it->source_location.set_comment(comment_f); + 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); - } - for(std::size_t i=0; iis_assert()) - i_it->make_skip(); + case coverage_criteriont::CONDITION: + if(i_it->is_assert()) + i_it->make_skip(); - // Decisions are maximal Boolean combinations of conditions. - { - const std::set decisions=collect_decisions(i_it); + // 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; + const source_locationt source_location=i_it->source_location; - for(const auto & d : decisions) - { - const std::string d_string=from_expr(ns, "", d); + for(const auto & c : conditions) + { + const std::string c_string=from_expr(ns, "", c); - 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_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="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); + 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::MCDC: - if(i_it->is_assert()) - i_it->make_skip(); + // Decisions are maximal Boolean combinations of conditions. + { + const std::set decisions=collect_decisions(i_it); - // 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); + 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); + } - std::set both; - std::set_union(conditions.begin(), conditions.end(), - decisions.begin(), decisions.end(), - inserter(both, both.end())); + for(std::size_t i=0; isource_location; + case coverage_criteriont::MCDC: + if(i_it->is_assert()) + i_it->make_skip(); - for(const auto & p : both) + // 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. { - bool is_decision=decisions.find(p)!=decisions.end(); - bool is_condition=conditions.find(p)!=conditions.end(); + const std::set conditions=collect_conditions(i_it); + const std::set decisions=collect_decisions(i_it); - std::string description= - (is_decision && is_condition)?"decision/condition": - is_decision?"decision":"condition"; + std::set both; + std::set_union(conditions.begin(), conditions.end(), + decisions.begin(), decisions.end(), + inserter(both, both.end())); - std::string p_string=from_expr(ns, "", p); + const source_locationt source_location=i_it->source_location; - 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); + for(const auto & p : both) + { + bool is_decision=decisions.find(p)!=decisions.end(); + bool is_condition=conditions.find(p)!=conditions.end(); - 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::string description= + (is_decision && is_condition)?"decision/condition": + is_decision?"decision":"condition"; - 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()); + std::string p_string=from_expr(ns, "", p); - for(const auto & p : controlling) - { - 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 description= - "MC/DC independence condition `"+p_string+"'"; + 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); + } - 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); - } + 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()); + } - for(std::size_t i=0; i 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); + } - case coverage_criteriont::PATH: - if(i_it->is_assert()) - i_it->make_skip(); - break; - default:; + 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:; + } } } - } /*******************************************************************\ diff --git a/src/goto-instrument/cover.h b/src/goto-instrument/cover.h index 8081ad77396..50c02567f80 100644 --- a/src/goto-instrument/cover.h +++ b/src/goto-instrument/cover.h @@ -15,7 +15,7 @@ Date: May 2016 enum class coverage_criteriont { LOCATION, BRANCH, DECISION, CONDITION, - PATH, MCDC, ASSERTION, COVER }; + PATH, MCDC, ASSERTION, COVER, BOUNDARY }; void instrument_cover_goals( const symbol_tablet &symbol_table, diff --git a/src/symex/Makefile b/src/symex/Makefile index 5a66801eec4..177492bb3b1 100644 --- a/src/symex/Makefile +++ b/src/symex/Makefile @@ -16,6 +16,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../goto-symex/rewrite_union$(OBJEXT) \ ../pointer-analysis/dereference$(OBJEXT) \ ../goto-instrument/cover$(OBJEXT) \ + ../goto-instrument/cover_boundary_values$(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..ecef9c97386 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; From 9369f2d07233fc63a21de90e39ca2b8982c6b384 Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Mon, 7 Nov 2016 16:59:26 +0000 Subject: [PATCH 03/17] add cover_boundary_values.cpp implemented by Youcheng Signed-off-by: Lucas Cordeiro --- src/goto-instrument/cover_boundary_values.cpp | 314 ++++++++++++++++++ 1 file changed, 314 insertions(+) create mode 100644 src/goto-instrument/cover_boundary_values.cpp diff --git a/src/goto-instrument/cover_boundary_values.cpp b/src/goto-instrument/cover_boundary_values.cpp new file mode 100644 index 00000000000..d3abccf01bc --- /dev/null +++ b/src/goto-instrument/cover_boundary_values.cpp @@ -0,0 +1,314 @@ +/*******************************************************************\ + +Module: Coverage Instrumentation for Boundary Values + +Author: Youcheng Sun + +Date: Oct 2016 + +\*******************************************************************/ + +#include +#include + +#include +#include +#include + +#include "cover.h" + +/*******************************************************************\ + +Function: non_ordered_predicate_expansion + + Inputs: + + Outputs: + + Purpose: expand a non-ordered predicate: <=, !=, >= + +\*******************************************************************/ + +std::set non_ordered_predicate_expansion(const exprt &src) +{ + std::set result; + // the expansion of "<=" is "<" and "==" + if(src.id()==ID_le) + { + exprt e1(ID_lt); + e1.type().id(src.type().id()); + e1.operands().push_back(src.op0()); + e1.operands().push_back(src.op1()); + result.insert(e1); + + exprt e2(ID_equal); + e2.type().id(src.type().id()); + e2.operands().push_back(src.op0()); + e2.operands().push_back(src.op1()); + result.insert(e2); + } + if(src.id()==ID_ge) + { + 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_equal); + e2.type().id(src.type().id()); + e2.operands().push_back(src.op0()); + e2.operands().push_back(src.op1()); + result.insert(e2); + } + if(src.id()==ID_notequal) + { + + if(from_expr(src.op0())=="TRUE" + or from_expr(src.op0())=="FALSE" + or from_expr(src.op1())=="TRUE" + or from_expr(src.op1())=="FALSE") + { + return result; + } + 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(ID_le); + e1.type().id(src.type().id()); + e1.operands().push_back(src.op0()); + e1.operands().push_back(src.op1()); + result.insert(e1); + + exprt e2(ID_ge); + e2.type().id(src.type().id()); + e2.operands().push_back(src.op0()); + e2.operands().push_back(src.op1()); + result.insert(e2); + } + // the negation of "<" is "==" and ">" + if(src.id()==ID_lt) + { + exprt e1(ID_equal); + e1.type().id(src.type().id()); + e1.operands().push_back(src.op0()); + e1.operands().push_back(src.op1()); + result.insert(e1); + + exprt e2(ID_gt); + e2.type().id(src.type().id()); + e2.operands().push_back(src.op0()); + e2.operands().push_back(src.op1()); + result.insert(e2); + } + // the negation of "<=" is ">" + if(src.id()==ID_le) + { + 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); + } + // the negation of ">=" is "<" + if(src.id()==ID_ge) + { + exprt e1(ID_lt); + e1.type().id(src.type().id()); + e1.operands().push_back(src.op0()); + e1.operands().push_back(src.op1()); + result.insert(e1); + } + // the negation of ">" is "==" and "<" + if(src.id()==ID_gt) + { + exprt e1(ID_equal); + 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); + } + // the negation of "!=" is "==" + if(src.id()==ID_notequal) + { + exprt e1(ID_equal); + e1.type().id(src.type().id()); + e1.operands().push_back(src.op0()); + e1.operands().push_back(src.op1()); + result.insert(e1); + } + + return result; + +} + +/*******************************************************************\ + +Function: non_ordered_expr_expansion + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +std::set non_ordered_expr_expansion(const exprt &src) +{ + std::set result; + + std::set s1, s2; + + if(src.id()!=ID_not) s1.insert(src); + else + { + exprt no=src.op0(); + if(is_arithmetic_predicate(no)) + { + auto res=ordered_negation(no); + for(auto &e: res) s1.insert(e); + } + else result.insert(src); + } + + // expand negations and non-ordered predicates + while(true) + { + bool changed=false; + for(auto &x: s1) + { + std::vector operands; + collect_operands(x, operands); + for(int i=0; i res; + if(operands[i].id()==ID_not) + { + exprt no=operands[i].op0(); + if(is_arithmetic_predicate(no)) + { + res=ordered_negation(no); + if(res.size()>0) changed=true; + } + } + else + { + if(operands[i].id()==ID_le + or operands[i].id()==ID_ge + or operands[i].id()==ID_notequal) + { + res=non_ordered_predicate_expansion(operands[i]); + if(res.size()>0) changed=true; + } + } + std::set co=replacement_and_conjunction(res, operands, i); + s2.insert(co.begin(), co.end()); + if(res.size()>0) break; + } + if(not changed) s2.insert(x); + } + if(not changed) break; + s1=s2; + s2.clear(); + } + + return s1; + +} + +/*******************************************************************\ + +Function: decision_expansion + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +std::set 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_predicate_expansion(d); + if(not res.empty()) + ctrl.insert(res.begin(), res.end()); + else ctrl.insert(d); + d.make_not(); + res=non_ordered_predicate_expansion(d); + if(not res.empty()) + ctrl.insert(res.begin(), res.end()); + else ctrl.insert(d); + } + return ctrl; +} + +/*******************************************************************\ + +Function: is_arithmetic_predicate + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +bool is_arithmetic_predicate(const exprt &src) +{ + if(src.id()==ID_lt + or src.id()==ID_le + or src.id()==ID_equal + or src.id()==ID_ge + or src.id()==ID_gt + or src.id()==ID_notequal) + return true; + + return false; +} From a282cb327f6aa7a72353dafe1a2ea80d8a201b01 Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Thu, 10 Nov 2016 16:47:13 +0000 Subject: [PATCH 04/17] add boundary values to mcdc coverage by Youcheng Signed-off-by: Lucas Cordeiro --- .../mcdc-boundary-values1/test.desc | 2 +- .../mcdc-boundary-values2/test.desc | 2 +- .../mcdc-boundary-values3/test.desc | 2 +- .../mcdc-boundary-values4/test.desc | 2 +- src/cbmc/cbmc_parse_options.cpp | 3 +- src/goto-instrument/cover.cpp | 47 ++++++++++--------- src/goto-instrument/cover.h | 6 +-- src/goto-instrument/cover_boundary_values.cpp | 2 +- src/symex/symex_parse_options.cpp | 3 +- 9 files changed, 37 insertions(+), 32 deletions(-) diff --git a/regression/cbmc-cover/mcdc-boundary-values1/test.desc b/regression/cbmc-cover/mcdc-boundary-values1/test.desc index c7192130ec5..724ebfef074 100644 --- a/regression/cbmc-cover/mcdc-boundary-values1/test.desc +++ b/regression/cbmc-cover/mcdc-boundary-values1/test.desc @@ -1,6 +1,6 @@ CORE main.c ---cover boundary-values +--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$ diff --git a/regression/cbmc-cover/mcdc-boundary-values2/test.desc b/regression/cbmc-cover/mcdc-boundary-values2/test.desc index 38c34b6c859..b01aad0f49c 100644 --- a/regression/cbmc-cover/mcdc-boundary-values2/test.desc +++ b/regression/cbmc-cover/mcdc-boundary-values2/test.desc @@ -1,6 +1,6 @@ CORE main.c ---cover boundary-values +--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$ diff --git a/regression/cbmc-cover/mcdc-boundary-values3/test.desc b/regression/cbmc-cover/mcdc-boundary-values3/test.desc index ab20b309e6d..43d8b882fc4 100644 --- a/regression/cbmc-cover/mcdc-boundary-values3/test.desc +++ b/regression/cbmc-cover/mcdc-boundary-values3/test.desc @@ -1,6 +1,6 @@ CORE main.c ---cover boundary-values +--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$ diff --git a/regression/cbmc-cover/mcdc-boundary-values4/test.desc b/regression/cbmc-cover/mcdc-boundary-values4/test.desc index eb14ca3a588..fe3d82783be 100644 --- a/regression/cbmc-cover/mcdc-boundary-values4/test.desc +++ b/regression/cbmc-cover/mcdc-boundary-values4/test.desc @@ -1,6 +1,6 @@ CORE main.c ---cover boundary-values +--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$ diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index fb430a96a7f..985b3955195 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -943,8 +943,7 @@ 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_goals(symbol_table, goto_functions, criteria); goto_functions.update(); } diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index 07aeafd1714..0a5330b9fd2 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -1089,7 +1089,7 @@ void instrument_cover_goals( 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()) @@ -1114,7 +1114,7 @@ void instrument_cover_goals( else if(i_it->is_assert()) i_it->make_skip(); break; - + case coverage_criteriont::LOCATION: if(i_it->is_assert()) i_it->make_skip(); @@ -1138,13 +1138,13 @@ void instrument_cover_goals( 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(); @@ -1165,7 +1165,7 @@ void instrument_cover_goals( t->source_location.set(ID_coverage_criterion, coverage_criterion); t->source_location.set_property_class(property_class); } - + if(i_it->is_goto() && !i_it->guard.is_true()) { std::string b=i2string(basic_blocks[i_it]); @@ -1190,12 +1190,12 @@ void instrument_cover_goals( 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::CONDITION: if(i_it->is_assert()) i_it->make_skip(); @@ -1209,7 +1209,7 @@ void instrument_cover_goals( 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); @@ -1226,12 +1226,12 @@ void instrument_cover_goals( 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(); @@ -1245,7 +1245,7 @@ void instrument_cover_goals( 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); @@ -1262,7 +1262,7 @@ void instrument_cover_goals( 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; i 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(), @@ -1292,13 +1292,13 @@ void instrument_cover_goals( { 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); @@ -1317,7 +1317,7 @@ void instrument_cover_goals( i_it->source_location.set(ID_coverage_criterion, coverage_criterion); i_it->source_location.set_property_class(property_class); } - + bool boundary_values_analysis= criteria.find(coverage_criteriont::BOUNDARY)!=criteria.end(); std::set controlling; @@ -1353,7 +1353,7 @@ void instrument_cover_goals( 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); @@ -1362,7 +1362,7 @@ void instrument_cover_goals( 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:; } } @@ -1394,14 +1394,19 @@ Function: instrument_cover_goals void instrument_cover_goals( const symbol_tablet &symbol_table, goto_functionst &goto_functions, - coverage_criteriont criterion) + const std::set &criteria) { Forall_goto_functions(f_it, goto_functions) { if(f_it->first==ID__start || f_it->first=="__CPROVER_initialize") continue; +<<<<<<< ed57692cda52670fb84c6a282155f7d6e6bd6923 instrument_cover_goals(symbol_table, f_it->second.body, criterion); +======= + + instrument_cover_goals(symbol_table, f_it->second.body, criteria); +>>>>>>> add boundary values to mcdc coverage by Youcheng } } diff --git a/src/goto-instrument/cover.h b/src/goto-instrument/cover.h index 50c02567f80..b47b06ad0da 100644 --- a/src/goto-instrument/cover.h +++ b/src/goto-instrument/cover.h @@ -15,16 +15,16 @@ Date: May 2016 enum class coverage_criteriont { LOCATION, BRANCH, DECISION, CONDITION, - PATH, MCDC, ASSERTION, COVER, BOUNDARY }; + PATH, MCDC, BOUNDARY, ASSERTION, COVER}; void instrument_cover_goals( const symbol_tablet &symbol_table, goto_programt &goto_program, - coverage_criteriont); + const std::set &criteria); void instrument_cover_goals( const symbol_tablet &symbol_table, goto_functionst &goto_functions, - coverage_criteriont); + const std::set &criteria); #endif // CPROVER_GOTO_INSTRUMENT_COVER_H diff --git a/src/goto-instrument/cover_boundary_values.cpp b/src/goto-instrument/cover_boundary_values.cpp index d3abccf01bc..fadbe6daa20 100644 --- a/src/goto-instrument/cover_boundary_values.cpp +++ b/src/goto-instrument/cover_boundary_values.cpp @@ -218,7 +218,7 @@ std::set non_ordered_expr_expansion(const exprt &src) { std::vector operands; collect_operands(x, operands); - for(int i=0; i res; if(operands[i].id()==ID_not) diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp index ecef9c97386..3038cf52dad 100644 --- a/src/symex/symex_parse_options.cpp +++ b/src/symex/symex_parse_options.cpp @@ -397,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_goals(symbol_table, goto_model.goto_functions, {c}); + //instrument_cover_goals(symbol_table, goto_model.goto_functions, c); goto_model.goto_functions.update(); } From 2ec531041e5f96510face1d72fdfe33ac425e6eb Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Mon, 21 Nov 2016 16:25:03 +0000 Subject: [PATCH 05/17] implement Michael's comments by Youcheng Signed-off-by: Lucas Cordeiro --- src/cbmc/Makefile | 1 - src/goto-instrument/Makefile | 2 +- src/goto-instrument/cover.cpp | 341 ++++++++++++++++-- src/goto-instrument/cover_boundary_values.cpp | 314 ---------------- src/symex/Makefile | 1 - src/symex/symex_parse_options.cpp | 1 - 6 files changed, 315 insertions(+), 345 deletions(-) delete mode 100644 src/goto-instrument/cover_boundary_values.cpp diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile index e11b6c0be4a..79f7a4fd982 100644 --- a/src/cbmc/Makefile +++ b/src/cbmc/Makefile @@ -22,7 +22,6 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../goto-instrument/full_slicer$(OBJEXT) \ ../goto-instrument/nondet_static$(OBJEXT) \ ../goto-instrument/cover$(OBJEXT) \ - ../goto-instrument/cover_boundary_values$(OBJEXT) \ ../analyses/analyses$(LIBEXT) \ ../langapi/langapi$(LIBEXT) \ ../xmllang/xmllang$(LIBEXT) \ diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index 854e5be00f6..0d1e4d6f741 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 cover_boundary_values.cpp + code_contracts.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 0a5330b9fd2..e19fa5f1d9b 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -218,6 +218,299 @@ void collect_operands(const exprt &src, std::vector &dest) /*******************************************************************\ +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) + { + std::vector others; + for(std::size_t j=0; j non_ordered_expr_expansion(const exprt &src) +{ + std::set result; + + std::set s1, s2; + + if(src.id()!=ID_not||!is_arithmetic_predicate(src.op0())) + s1.insert(src); + else + { + auto res=ordered_negation(src.op0()); + s1.insert(res.begin(), res.end()); + } + + // expand negations and non-ordered predicates + bool changed=true; + while(changed) + { + changed=false; + for(auto &x: s1) + { + std::vector operands; + collect_operands(x, operands); + for(std::size_t i=0; i res; + if(operands[i].id()==ID_not) + { + exprt no=operands[i].op0(); + if(is_arithmetic_predicate(no)) + { + res=ordered_negation(no); + if(!res.empty()) changed=true; + } + } + else + { + if(operands[i].id()==ID_le + || operands[i].id()==ID_ge + || operands[i].id()==ID_notequal) + { + res=non_ordered_predicate_expansion(operands[i]); + if(!res.empty()) changed=true; + } + } + std::set co=replacement_and_conjunction(res, operands, i); + s2.insert(co.begin(), co.end()); + if(!res.empty()) break; + } + if(!changed) s2.insert(x); + } + if(!changed) break; + s1.swap(s2); + s2.clear(); + } + + return s1; +} + +/*******************************************************************\ + +Function: decision_expansion + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +std::set 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_predicate_expansion(d); + if(not res.empty()) + ctrl.insert(res.begin(), res.end()); + else ctrl.insert(d); + d.make_not(); + res=non_ordered_predicate_expansion(d); + if(not res.empty()) + ctrl.insert(res.begin(), res.end()); + else ctrl.insert(d); + } + return ctrl; +} + +/*******************************************************************\ + Function: collect_mcdc_controlling_rec Inputs: @@ -235,8 +528,7 @@ void collect_mcdc_controlling_rec( std::set &result) { // src is conjunction (ID_and) or disjunction (ID_or) - if(src.id()==ID_and || - src.id()==ID_or) + if(src.id()==ID_and || src.id()==ID_or) { std::vector operands; collect_operands(src, operands); @@ -363,6 +655,7 @@ std::set collect_mcdc_controlling( return result; } + /*******************************************************************\ Function: replacement_and_conjunction @@ -376,7 +669,7 @@ Function: replacement_and_conjunction \*******************************************************************/ -std::set replacement_and_conjunction( +static std::set replacement_and_conjunction( const std::set &replacement_exprs, const std::vector &operands, const std::size_t i) @@ -384,12 +677,9 @@ std::set replacement_and_conjunction( std::set result; for(auto &y : replacement_exprs) { - std::vector others; - for(std::size_t j=0; ji); + std::vector others(operands); + others[i]=y; exprt c=conjunction(others); result.insert(c); } @@ -410,7 +700,7 @@ Function: collect_mcdc_controlling_nested \*******************************************************************/ -std::set collect_mcdc_controlling_nested( +static std::set collect_mcdc_controlling_nested( const std::set &decisions) { // To obtain the 1st-level controlling conditions @@ -424,16 +714,17 @@ std::set collect_mcdc_controlling_nested( std::set s1, s2; /** * The final controlling conditions resulted from ''src'' - * will be stored in ''s1''; ''s2'' is usd to hold the + * 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 - while(true) + bool changed=true; + while(changed) { - bool changed=false; + changed=false; // the 2nd loop for(auto &x : s1) { @@ -480,16 +771,16 @@ std::set collect_mcdc_controlling_nested( std::set co= replacement_and_conjunction(res, operands, i); s2.insert(co.begin(), co.end()); - if(res.size() > 0) break; + 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;} + s1.swap(s2); s2.clear(); + if(!changed) {break;} } // The expansions of each ''src'' should be added into @@ -626,7 +917,7 @@ void remove_repetition(std::set &exprs) { std::set signs1=sign_of_expr(c, x); std::set signs2=sign_of_expr(c, y); - int s1=signs1.size(), s2=signs2.size(); + std::size_t s1=signs1.size(), s2=signs2.size(); // it is easy to check non-equivalence; if(s1!=s2) { @@ -661,7 +952,7 @@ void remove_repetition(std::set &exprs) } // update the original ''exprs'' - exprs = new_exprs; + exprs.swap(new_exprs); } /*******************************************************************\ @@ -742,7 +1033,7 @@ std::map values_of_atomic_exprs( for(auto &c : conditions) { std::set signs=sign_of_expr(c, e); - if(signs.size()==0) + if(signs.empty()) { // ''c'' is not contained in ''e'' atomic_exprs.insert(std::pair(c, 0)); @@ -891,10 +1182,11 @@ void minimize_mcdc_controlling( conditions.insert(new_conditions.begin(), new_conditions.end()); } - while(true) + bool ctrl_update=true; + while(ctrl_update) { + ctrl_update=false; 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 @@ -948,7 +1240,7 @@ void minimize_mcdc_controlling( // Update ''controlling'' or break the while loop if(ctrl_update) { - controlling=new_controlling; + controlling.swap(new_controlling); } else break; } @@ -1401,12 +1693,7 @@ void instrument_cover_goals( if(f_it->first==ID__start || f_it->first=="__CPROVER_initialize") continue; -<<<<<<< ed57692cda52670fb84c6a282155f7d6e6bd6923 - - instrument_cover_goals(symbol_table, f_it->second.body, criterion); -======= instrument_cover_goals(symbol_table, f_it->second.body, criteria); ->>>>>>> add boundary values to mcdc coverage by Youcheng } } diff --git a/src/goto-instrument/cover_boundary_values.cpp b/src/goto-instrument/cover_boundary_values.cpp deleted file mode 100644 index fadbe6daa20..00000000000 --- a/src/goto-instrument/cover_boundary_values.cpp +++ /dev/null @@ -1,314 +0,0 @@ -/*******************************************************************\ - -Module: Coverage Instrumentation for Boundary Values - -Author: Youcheng Sun - -Date: Oct 2016 - -\*******************************************************************/ - -#include -#include - -#include -#include -#include - -#include "cover.h" - -/*******************************************************************\ - -Function: non_ordered_predicate_expansion - - Inputs: - - Outputs: - - Purpose: expand a non-ordered predicate: <=, !=, >= - -\*******************************************************************/ - -std::set non_ordered_predicate_expansion(const exprt &src) -{ - std::set result; - // the expansion of "<=" is "<" and "==" - if(src.id()==ID_le) - { - exprt e1(ID_lt); - e1.type().id(src.type().id()); - e1.operands().push_back(src.op0()); - e1.operands().push_back(src.op1()); - result.insert(e1); - - exprt e2(ID_equal); - e2.type().id(src.type().id()); - e2.operands().push_back(src.op0()); - e2.operands().push_back(src.op1()); - result.insert(e2); - } - if(src.id()==ID_ge) - { - 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_equal); - e2.type().id(src.type().id()); - e2.operands().push_back(src.op0()); - e2.operands().push_back(src.op1()); - result.insert(e2); - } - if(src.id()==ID_notequal) - { - - if(from_expr(src.op0())=="TRUE" - or from_expr(src.op0())=="FALSE" - or from_expr(src.op1())=="TRUE" - or from_expr(src.op1())=="FALSE") - { - return result; - } - 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(ID_le); - e1.type().id(src.type().id()); - e1.operands().push_back(src.op0()); - e1.operands().push_back(src.op1()); - result.insert(e1); - - exprt e2(ID_ge); - e2.type().id(src.type().id()); - e2.operands().push_back(src.op0()); - e2.operands().push_back(src.op1()); - result.insert(e2); - } - // the negation of "<" is "==" and ">" - if(src.id()==ID_lt) - { - exprt e1(ID_equal); - e1.type().id(src.type().id()); - e1.operands().push_back(src.op0()); - e1.operands().push_back(src.op1()); - result.insert(e1); - - exprt e2(ID_gt); - e2.type().id(src.type().id()); - e2.operands().push_back(src.op0()); - e2.operands().push_back(src.op1()); - result.insert(e2); - } - // the negation of "<=" is ">" - if(src.id()==ID_le) - { - 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); - } - // the negation of ">=" is "<" - if(src.id()==ID_ge) - { - exprt e1(ID_lt); - e1.type().id(src.type().id()); - e1.operands().push_back(src.op0()); - e1.operands().push_back(src.op1()); - result.insert(e1); - } - // the negation of ">" is "==" and "<" - if(src.id()==ID_gt) - { - exprt e1(ID_equal); - 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); - } - // the negation of "!=" is "==" - if(src.id()==ID_notequal) - { - exprt e1(ID_equal); - e1.type().id(src.type().id()); - e1.operands().push_back(src.op0()); - e1.operands().push_back(src.op1()); - result.insert(e1); - } - - return result; - -} - -/*******************************************************************\ - -Function: non_ordered_expr_expansion - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -std::set non_ordered_expr_expansion(const exprt &src) -{ - std::set result; - - std::set s1, s2; - - if(src.id()!=ID_not) s1.insert(src); - else - { - exprt no=src.op0(); - if(is_arithmetic_predicate(no)) - { - auto res=ordered_negation(no); - for(auto &e: res) s1.insert(e); - } - else result.insert(src); - } - - // expand negations and non-ordered predicates - while(true) - { - bool changed=false; - for(auto &x: s1) - { - std::vector operands; - collect_operands(x, operands); - for(size_t i=0; i res; - if(operands[i].id()==ID_not) - { - exprt no=operands[i].op0(); - if(is_arithmetic_predicate(no)) - { - res=ordered_negation(no); - if(res.size()>0) changed=true; - } - } - else - { - if(operands[i].id()==ID_le - or operands[i].id()==ID_ge - or operands[i].id()==ID_notequal) - { - res=non_ordered_predicate_expansion(operands[i]); - if(res.size()>0) changed=true; - } - } - std::set co=replacement_and_conjunction(res, operands, i); - s2.insert(co.begin(), co.end()); - if(res.size()>0) break; - } - if(not changed) s2.insert(x); - } - if(not changed) break; - s1=s2; - s2.clear(); - } - - return s1; - -} - -/*******************************************************************\ - -Function: decision_expansion - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -std::set 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_predicate_expansion(d); - if(not res.empty()) - ctrl.insert(res.begin(), res.end()); - else ctrl.insert(d); - d.make_not(); - res=non_ordered_predicate_expansion(d); - if(not res.empty()) - ctrl.insert(res.begin(), res.end()); - else ctrl.insert(d); - } - return ctrl; -} - -/*******************************************************************\ - -Function: is_arithmetic_predicate - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -bool is_arithmetic_predicate(const exprt &src) -{ - if(src.id()==ID_lt - or src.id()==ID_le - or src.id()==ID_equal - or src.id()==ID_ge - or src.id()==ID_gt - or src.id()==ID_notequal) - return true; - - return false; -} diff --git a/src/symex/Makefile b/src/symex/Makefile index 177492bb3b1..5a66801eec4 100644 --- a/src/symex/Makefile +++ b/src/symex/Makefile @@ -16,7 +16,6 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../goto-symex/rewrite_union$(OBJEXT) \ ../pointer-analysis/dereference$(OBJEXT) \ ../goto-instrument/cover$(OBJEXT) \ - ../goto-instrument/cover_boundary_values$(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 3038cf52dad..10ae4f433ea 100644 --- a/src/symex/symex_parse_options.cpp +++ b/src/symex/symex_parse_options.cpp @@ -398,7 +398,6 @@ 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_goals(symbol_table, goto_model.goto_functions, c); goto_model.goto_functions.update(); } From 70f74097c61f435019721ce0600b20e97edf41fa Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Mon, 19 Dec 2016 10:16:58 +0000 Subject: [PATCH 06/17] Refactor the code related to cover.cpp Expand a decision by non_ordered_expr_expansion instead of non_ordered_predicate_expansion. Additionally, remove white space and unnecessary line break. --- src/goto-instrument/cover.cpp | 159 ++++++++++++++++------------------ 1 file changed, 75 insertions(+), 84 deletions(-) diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index e19fa5f1d9b..9abfd5dd907 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -106,7 +106,7 @@ Function: is_condition \*******************************************************************/ -bool is_condition(const exprt &src) +static bool is_condition(const exprt &src) { if(src.type().id()!=ID_bool) return false; @@ -130,7 +130,9 @@ Function: collect_conditions_rec \*******************************************************************/ -void collect_conditions_rec(const exprt &src, std::set &dest) +static void collect_conditions_rec( + const exprt &src, + std::set &dest) { if(src.id()==ID_address_of) { @@ -156,7 +158,7 @@ Function: collect_conditions \*******************************************************************/ -std::set collect_conditions(const exprt &src) +static std::set collect_conditions(const exprt &src) { std::set result; collect_conditions_rec(src, result); @@ -175,7 +177,8 @@ Function: collect_conditions \*******************************************************************/ -std::set collect_conditions(const goto_programt::const_targett t) +static std::set collect_conditions( + const goto_programt::const_targett t) { switch(t->type) { @@ -205,7 +208,9 @@ Function: collect_operands \*******************************************************************/ -void collect_operands(const exprt &src, std::vector &dest) +static void collect_operands( + const exprt &src, + std::vector &dest) { for(const exprt &op : src.operands()) { @@ -228,7 +233,8 @@ Function: non_ordered_predicate_expansion \*******************************************************************/ -std::set non_ordered_predicate_expansion(const exprt &src) +static std::set non_ordered_predicate_expansion( + const exprt &src) { std::set result; // the expansion of "<=" is "<" and "==" @@ -289,7 +295,7 @@ Function: ordered_negation \*******************************************************************/ -std::set ordered_negation(const exprt &src) +static std::set ordered_negation(const exprt &src) { std::set result; // the negation of "==" is "<" and ">" @@ -362,7 +368,7 @@ Function: is_arithmetic_predicate \*******************************************************************/ -bool is_arithmetic_predicate(const exprt &src) +static bool is_arithmetic_predicate(const exprt &src) { return (src.id()==ID_lt || src.id()==ID_le @@ -385,7 +391,7 @@ Function: replacement_and_conjunction \*******************************************************************/ -std::set replacement_and_conjunction( +static std::set replacement_and_conjunction( const std::set &replacement_exprs, const std::vector &operands, const std::size_t i) @@ -393,12 +399,9 @@ std::set replacement_and_conjunction( std::set result; for(auto &y : replacement_exprs) { - std::vector others; - for(std::size_t j=0; ji); + std::vector others(operands); + others[i]=y; exprt c=conjunction(others); result.insert(c); } @@ -417,63 +420,51 @@ Function: non_ordered_expr_expansion \*******************************************************************/ -std::set non_ordered_expr_expansion(const exprt &src) +static std::set non_ordered_expr_expansion(const exprt &src) { - std::set result; - - std::set s1, s2; - - if(src.id()!=ID_not||!is_arithmetic_predicate(src.op0())) - s1.insert(src); - else + if(src.id()==ID_not&&is_arithmetic_predicate(src.op0())) { - auto res=ordered_negation(src.op0()); - s1.insert(res.begin(), res.end()); + return ordered_negation(src.op0()); } + std::set result; + std::vector operands;; + collect_operands(src, operands); // expand negations and non-ordered predicates - bool changed=true; - while(changed) + for(std::size_t i=0; i=' or '!=' + std::set expanded_op; + if(operands[i].id()==ID_not) { - std::vector operands; - collect_operands(x, operands); - for(std::size_t i=0; i res; - if(operands[i].id()==ID_not) - { - exprt no=operands[i].op0(); - if(is_arithmetic_predicate(no)) - { - res=ordered_negation(no); - if(!res.empty()) changed=true; - } - } - else - { - if(operands[i].id()==ID_le - || operands[i].id()==ID_ge - || operands[i].id()==ID_notequal) - { - res=non_ordered_predicate_expansion(operands[i]); - if(!res.empty()) changed=true; - } - } - std::set co=replacement_and_conjunction(res, operands, i); - s2.insert(co.begin(), co.end()); - if(!res.empty()) break; + expanded_op=ordered_negation(no); } - if(!changed) s2.insert(x); } - if(!changed) break; - s1.swap(s2); - s2.clear(); + 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 s1; + return {src}; } /*******************************************************************\ @@ -488,7 +479,7 @@ Function: decision_expansion \*******************************************************************/ -std::set decision_expansion(const exprt &dec) +static std::set decision_expansion(const exprt &dec) { std::set ctrl; // dec itself may be a non-ordered predicate @@ -496,15 +487,11 @@ std::set decision_expansion(const exprt &dec) if(d.id()==ID_not) d=d.op0(); if(is_arithmetic_predicate(d)) { - auto res=non_ordered_predicate_expansion(d); - if(not res.empty()) - ctrl.insert(res.begin(), res.end()); - else ctrl.insert(d); + auto res=non_ordered_expr_expansion(d); + ctrl.insert(res.begin(), res.end()); d.make_not(); - res=non_ordered_predicate_expansion(d); - if(not res.empty()) - ctrl.insert(res.begin(), res.end()); - else ctrl.insert(d); + res=non_ordered_expr_expansion(d); + ctrl.insert(res.begin(), res.end()); } return ctrl; } @@ -522,13 +509,14 @@ Function: collect_mcdc_controlling_rec \*******************************************************************/ -void collect_mcdc_controlling_rec( +static 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) + if(src.id()==ID_and || + src.id()==ID_or) { std::vector operands; collect_operands(src, operands); @@ -643,7 +631,7 @@ Function: collect_mcdc_controlling \*******************************************************************/ -std::set collect_mcdc_controlling( +static std::set collect_mcdc_controlling( const std::set &decisions) { std::set result; @@ -652,6 +640,7 @@ std::set collect_mcdc_controlling( { collect_mcdc_controlling_rec(d, { }, result); } + return result; } @@ -805,7 +794,7 @@ Function: sign_of_expr \*******************************************************************/ -std::set sign_of_expr(const exprt &e, const exprt &E) +static std::set sign_of_expr(const exprt &e, const exprt &E) { std::set signs; @@ -872,7 +861,7 @@ Function: remove_repetition \*******************************************************************/ -void remove_repetition(std::set &exprs) +static void remove_repetition(std::set &exprs) { // to obtain the set of atomic conditions std::set conditions; @@ -967,8 +956,9 @@ Function: eval_expr the atomic expr values \*******************************************************************/ -bool eval_expr( - const std::map &atomic_exprs, + +static bool eval_expr( + const std::map &atomic_exprs, const exprt &src) { std::vector operands; @@ -1025,7 +1015,7 @@ Function: values_of_atomic_exprs \*******************************************************************/ -std::map values_of_atomic_exprs( +static std::map values_of_atomic_exprs( const exprt &e, const std::set &conditions) { @@ -1064,7 +1054,7 @@ Function: is_mcdc_pair \*******************************************************************/ -bool is_mcdc_pair( +static bool is_mcdc_pair( const exprt &e1, const exprt &e2, const exprt &c, @@ -1133,7 +1123,7 @@ Function: has_mcdc_pair \*******************************************************************/ -bool has_mcdc_pair( +static bool has_mcdc_pair( const exprt &c, const std::set &expr_set, const std::set &conditions, @@ -1170,7 +1160,7 @@ Function: minimize_mcdc_controlling \*******************************************************************/ -void minimize_mcdc_controlling( +static void minimize_mcdc_controlling( std::set &controlling, const exprt &decision) { @@ -1258,7 +1248,7 @@ Function: collect_decisions_rec \*******************************************************************/ -void collect_decisions_rec(const exprt &src, std::set &dest) +static void collect_decisions_rec(const exprt &src, std::set &dest) { if(src.id()==ID_address_of) { @@ -1299,7 +1289,7 @@ Function: collect_decisions \*******************************************************************/ -std::set collect_decisions(const exprt &src) +static std::set collect_decisions(const exprt &src) { std::set result; collect_decisions_rec(src, result); @@ -1318,7 +1308,8 @@ Function: collect_decisions \*******************************************************************/ -std::set collect_decisions(const goto_programt::const_targett t) +static std::set collect_decisions( + const goto_programt::const_targett t) { switch(t->type) { From 5aaa67ad240a19f81063966bfde0a8de49f90f81 Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Mon, 19 Dec 2016 10:23:23 +0000 Subject: [PATCH 07/17] Update test desc of mcdc1 and mcdc8 Two regression test outputs are adjusted, as the order of predicates in the output sometimes differs after the simplification. --- regression/cbmc-cover/mcdc1/test.desc | 7 +++---- regression/cbmc-cover/mcdc8/test.desc | 8 ++++---- 2 files changed, 7 insertions(+), 8 deletions(-) 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$ -- From 954f322172585a5bace9e38c2aad9648abcea2ab Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Mon, 19 Dec 2016 11:37:00 +0000 Subject: [PATCH 08/17] Refactor instrument_cover_goals Created a class called instrument_cover_goalst that contains methods and atributes related to instrumenting coverage goals --- src/cbmc/cbmc_parse_options.cpp | 3 +- src/goto-instrument/cover.cpp | 94 ++----------------------------- src/goto-instrument/cover.h | 79 +++++++++++++++++++++++--- src/symex/symex_parse_options.cpp | 3 +- 4 files changed, 79 insertions(+), 100 deletions(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 985b3955195..a53adc22a6d 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -943,7 +943,8 @@ bool cbmc_parse_optionst::process_goto_program( status() << "Instrumenting coverage goals" << eom; - instrument_cover_goals(symbol_table, goto_functions, criteria); + instrument_cover_goalst goals(symbol_table,criteria); + goals.instrument_cover_goals(goto_functions); goto_functions.update(); } diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index 9abfd5dd907..6b69de66822 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -17,55 +17,6 @@ Date: May 2016 #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'; - } -}; - /*******************************************************************\ Function: as_string @@ -645,36 +596,6 @@ static std::set collect_mcdc_controlling( } -/*******************************************************************\ - -Function: replacement_and_conjunction - - Inputs: - - Outputs: - - Purpose: To replace the i-th expr of ''operands'' with each - expr inside ''replacement_exprs''. - -\*******************************************************************/ - -static 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: collect_mcdc_controlling_nested @@ -1339,12 +1260,9 @@ Function: instrument_cover_goals \*******************************************************************/ -void instrument_cover_goals( - const symbol_tablet &symbol_table, - goto_programt &goto_program, - const std::set &criteria) +void instrument_cover_goalst::instrument_cover_goals( + goto_programt &goto_program) { - const namespacet ns(symbol_table); basic_blockst basic_blocks(goto_program); std::set blocks_done; @@ -1674,10 +1592,8 @@ Function: instrument_cover_goals \*******************************************************************/ -void instrument_cover_goals( - const symbol_tablet &symbol_table, - goto_functionst &goto_functions, - const std::set &criteria) +void instrument_cover_goalst::instrument_cover_goals( + goto_functionst &goto_functions) { Forall_goto_functions(f_it, goto_functions) { @@ -1685,6 +1601,6 @@ void instrument_cover_goals( f_it->first=="__CPROVER_initialize") continue; - instrument_cover_goals(symbol_table, f_it->second.body, criteria); + instrument_cover_goals(f_it->second.body); } } diff --git a/src/goto-instrument/cover.h b/src/goto-instrument/cover.h index b47b06ad0da..2fa1b7a2d7d 100644 --- a/src/goto-instrument/cover.h +++ b/src/goto-instrument/cover.h @@ -17,14 +17,75 @@ enum class coverage_criteriont { LOCATION, BRANCH, DECISION, CONDITION, PATH, MCDC, BOUNDARY, ASSERTION, COVER}; -void instrument_cover_goals( - const symbol_tablet &symbol_table, - goto_programt &goto_program, - const std::set &criteria); - -void instrument_cover_goals( - const symbol_tablet &symbol_table, - goto_functionst &goto_functions, - const std::set &criteria); +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_goalst +{ + public: + instrument_cover_goalst( + const symbol_tablet &_symbol_table, + const std::set &_criteria): + ns(_symbol_table), + criteria(_criteria) + { + } + + void instrument_cover_goals( + goto_programt &goto_program); + + void instrument_cover_goals( + goto_functionst &goto_functions); + + private: + const namespacet ns; + const std::set &criteria; +}; #endif // CPROVER_GOTO_INSTRUMENT_COVER_H diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp index 10ae4f433ea..4b07bd9651f 100644 --- a/src/symex/symex_parse_options.cpp +++ b/src/symex/symex_parse_options.cpp @@ -397,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(); } From 2c1b84d1f7ec7e5dd3dd8e08e58e5c99d961487b Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Mon, 19 Dec 2016 14:57:45 +0000 Subject: [PATCH 09/17] Refactor instrument_cover_goals Created methods for assertion, cover, location, branch, condition, decision, and mcdc. --- src/goto-instrument/cover.cpp | 663 ++++++++++++++++++++-------------- src/goto-instrument/cover.h | 42 ++- 2 files changed, 434 insertions(+), 271 deletions(-) diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index 6b69de66822..b64e8d2f35e 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -1250,6 +1250,393 @@ static std::set collect_decisions( /*******************************************************************\ +Function: instrument_assertion + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void instrument_cover_goalst::instrument_assertion( + goto_programt::instructionst::iterator &i_it) +{ + if(i_it->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); + } +} + +/*******************************************************************\ + +Function: instrument_cover + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void instrument_cover_goalst::instrument_cover( + goto_programt::instructionst::iterator &i_it) +{ + 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(); +} + +/*******************************************************************\ + +Function: instrument_location + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void instrument_cover_goalst::instrument_location( + goto_programt::instructionst::iterator &i_it, + goto_programt &goto_program, + basic_blockst &basic_blocks, + std::set &blocks_done) +{ + if(i_it->is_assert()) + i_it->make_skip(); + + 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++; + } + } +} + +/*******************************************************************\ + +Function: instrument_branch + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void instrument_cover_goalst::instrument_branch( + goto_programt::instructionst::iterator &i_it, + goto_programt &goto_program, + basic_blockst &basic_blocks) +{ + if(i_it->is_assert()) + 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= + "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); + } + + 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++; + } +} + +/*******************************************************************\ + +Function: instrument_condition + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void instrument_cover_goalst::instrument_condition( + goto_programt::instructionst::iterator &i_it, + goto_programt &goto_program) +{ + if(i_it->is_assert()) + i_it->make_skip(); + + // 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(); + + // 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; i &blocks_done) +{ + if(i_it->is_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. + + 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(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(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); + } + + 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(i_it); + i_it->make_assertion(not_exprt(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->guard=false_exprt(); - i_it->source_location.set(ID_coverage_criterion, coverage_criterion); - i_it->source_location.set_property_class(property_class); - } + instrument_assertion(i_it); 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(); + instrument_cover(i_it); break; case coverage_criteriont::LOCATION: - if(i_it->is_assert()) - i_it->make_skip(); - - { - 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++; - } - } - } + instrument_location(i_it,goto_program,basic_blocks,blocks_done); break; case coverage_criteriont::BRANCH: - if(i_it->is_assert()) - 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= - "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); - } - - 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++; - } + instrument_branch(i_it,goto_program,basic_blocks); break; case coverage_criteriont::CONDITION: - if(i_it->is_assert()) - i_it->make_skip(); - - // 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(); - - // 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(); - - // 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); - } - - 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(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; i &_criteria): @@ -83,9 +83,43 @@ class instrument_cover_goalst void instrument_cover_goals( goto_functionst &goto_functions); - private: - const namespacet ns; - const std::set &criteria; +private: + + void instrument_assertion( + goto_programt::instructionst::iterator &i_it); + + void instrument_cover( + goto_programt::instructionst::iterator &i_it); + + void instrument_location( + goto_programt::instructionst::iterator &i_it, + goto_programt &goto_program, + basic_blockst &basic_blocks, + std::set &blocks_done); + + void instrument_branch( + goto_programt::instructionst::iterator &i_it, + goto_programt &goto_program, + basic_blockst &basic_blocks); + + void instrument_condition( + goto_programt::instructionst::iterator &i_it, + goto_programt &goto_program); + + void instrument_decision( + goto_programt::instructionst::iterator &i_it, + goto_programt &goto_program); + + void instrument_mcdc( + goto_programt::instructionst::iterator &i_it, + goto_programt &goto_program, + basic_blockst &basic_blocks, + std::set &blocks_done); + + const namespacet ns; + const std::set &criteria; + irep_idt coverage_criterion; + irep_idt property_class; }; #endif // CPROVER_GOTO_INSTRUMENT_COVER_H From a7e27eacf02302f9cec42a7daa5d5bfe4935c09f Mon Sep 17 00:00:00 2001 From: theyoucheng Date: Mon, 19 Dec 2016 15:20:32 +0000 Subject: [PATCH 10/17] Enforced the coding rules in cover.cpp --- src/goto-instrument/cover.cpp | 80 ++++++++++++++++++----------------- 1 file changed, 42 insertions(+), 38 deletions(-) diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index b64e8d2f35e..cd506a220af 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -141,7 +141,7 @@ static std::set collect_conditions( case FUNCTION_CALL: return collect_conditions(t->code); - default:; + default: {} } return std::set(); @@ -358,7 +358,7 @@ static std::set replacement_and_conjunction( } return result; } - + /*******************************************************************\ Function: non_ordered_expr_expansion @@ -373,7 +373,7 @@ Function: non_ordered_expr_expansion static std::set non_ordered_expr_expansion(const exprt &src) { - if(src.id()==ID_not&&is_arithmetic_predicate(src.op0())) + if(src.id()==ID_not && is_arithmetic_predicate(src.op0())) { return ordered_negation(src.op0()); } @@ -406,7 +406,7 @@ static std::set non_ordered_expr_expansion(const exprt &src) } if(expanded_op.empty()) continue; auto re=replacement_and_conjunction(expanded_op, operands, i); - for(auto &x: re) + for(auto &x : re) { auto rec_result=non_ordered_expr_expansion(x); result.insert(rec_result.begin(), rec_result.end()); @@ -632,7 +632,7 @@ static std::set collect_mcdc_controlling_nested( // dual-loop structure to eliminate complex // non-atomic-conditional terms bool changed=true; - while(changed) + while(changed) { changed=false; // the 2nd loop @@ -746,7 +746,7 @@ static std::set sign_of_expr(const exprt &e, const exprt &E) for(auto &x : ops) { exprt y(x); - if(y == e) signs.insert(+1); + if(y==e) signs.insert(+1); else if(y.id()==ID_not) { y.make_not(); @@ -786,7 +786,7 @@ static void remove_repetition(std::set &exprs) { // to obtain the set of atomic conditions std::set conditions; - for(auto &x: exprs) + for(auto &x : exprs) { std::set new_conditions = collect_conditions(x); conditions.insert(new_conditions.begin(), new_conditions.end()); @@ -811,7 +811,7 @@ static void remove_repetition(std::set &exprs) exprs=new_exprs; new_exprs.clear(); - for(auto &x: exprs) + for(auto &x : exprs) { bool red=false; /** @@ -820,7 +820,7 @@ static void remove_repetition(std::set &exprs) * and ''y'' are identical iff they have the * same sign for every atomic condition ''c''. **/ - for(auto &y: new_exprs) + for(auto &y : new_exprs) { bool iden = true; for(auto &c : conditions) @@ -879,7 +879,7 @@ Function: eval_expr \*******************************************************************/ static bool eval_expr( - const std::map &atomic_exprs, + const std::map &atomic_exprs, const exprt &src) { std::vector operands; @@ -913,13 +913,13 @@ static bool eval_expr( no_op.make_not(); return !eval_expr(atomic_exprs, no_op); } - else //if(is_condition(src)) + 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) + else // if(atomic_exprs.find(src)->second==-1) return false; } } @@ -996,7 +996,7 @@ static bool is_mcdc_pair( 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) + if(cs1==0 || cs2==0) return false; // A mcdc pair regarding an atomic expr ''c'' @@ -1028,7 +1028,8 @@ static bool is_mcdc_pair( } if(diff_count==1) return true; - else return false; + else + return false; } /*******************************************************************\ @@ -1087,7 +1088,7 @@ static void minimize_mcdc_controlling( { // to obtain the set of atomic conditions std::set conditions; - for(auto &x: controlling) + for(auto &x : controlling) { std::set new_conditions = collect_conditions(x); conditions.insert(new_conditions.begin(), new_conditions.end()); @@ -1153,7 +1154,8 @@ static void minimize_mcdc_controlling( { controlling.swap(new_controlling); } - else break; + else + break; } } @@ -1242,7 +1244,7 @@ static std::set collect_decisions( case FUNCTION_CALL: return collect_decisions(t->code); - default:; + default: {} } return std::set(); @@ -1591,7 +1593,7 @@ void instrument_cover_goalst::instrument_mcdc( bool boundary_values_analysis= criteria.find(coverage_criteriont::BOUNDARY)!=criteria.end(); std::set controlling; - for(auto &dec: decisions) + for(auto &dec : decisions) { std::set ctrl=collect_mcdc_controlling_nested({dec}); if(boundary_values_analysis) @@ -1607,7 +1609,7 @@ void instrument_cover_goalst::instrument_mcdc( if(boundary_values_analysis) { std::set boundary_controlling; - for(auto &x: controlling) + for(auto &x : controlling) { auto res=non_ordered_expr_expansion(x); boundary_controlling.insert(res.begin(), res.end()); @@ -1655,11 +1657,13 @@ void instrument_cover_goalst::instrument_cover_goals( // 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->make_skip(); break; - - default:; + + default: {} } } } @@ -1729,7 +1733,7 @@ void instrument_cover_goalst::instrument_cover_goals( if(f_it->first==ID__start || f_it->first=="__CPROVER_initialize") continue; - + instrument_cover_goals(f_it->second.body); } } From cd2b2fc3589e18aa0d0f7a5c9967a4ba65697c84 Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Mon, 19 Dec 2016 15:29:18 +0000 Subject: [PATCH 11/17] Enforced the coding rules in cover.h Signed-off-by: Lucas Cordeiro --- src/goto-instrument/cover.h | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/goto-instrument/cover.h b/src/goto-instrument/cover.h index cdb210605b3..42ae01021cd 100644 --- a/src/goto-instrument/cover.h +++ b/src/goto-instrument/cover.h @@ -13,9 +13,11 @@ Date: May 2016 #include -enum class coverage_criteriont { +enum class coverage_criteriont +{ LOCATION, BRANCH, DECISION, CONDITION, - PATH, MCDC, BOUNDARY, ASSERTION, COVER}; + PATH, MCDC, BOUNDARY, ASSERTION, COVER +}; class basic_blockst { @@ -84,7 +86,6 @@ class instrument_cover_goalst goto_functionst &goto_functions); private: - void instrument_assertion( goto_programt::instructionst::iterator &i_it); From 9699a9024fb126afa95807e163eae3fd4642ac42 Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Mon, 19 Dec 2016 15:35:29 +0000 Subject: [PATCH 12/17] Enforced the coding rules in cbmc_parse_options.cpp and symex_parse_options.cpp Signed-off-by: Lucas Cordeiro --- src/cbmc/cbmc_parse_options.cpp | 2 +- src/symex/symex_parse_options.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index a53adc22a6d..9f1af784d22 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -943,7 +943,7 @@ bool cbmc_parse_optionst::process_goto_program( status() << "Instrumenting coverage goals" << eom; - instrument_cover_goalst goals(symbol_table,criteria); + instrument_cover_goalst goals(symbol_table, criteria); goals.instrument_cover_goals(goto_functions); goto_functions.update(); diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp index 4b07bd9651f..a11581d37fc 100644 --- a/src/symex/symex_parse_options.cpp +++ b/src/symex/symex_parse_options.cpp @@ -397,7 +397,7 @@ bool symex_parse_optionst::process_goto_program(const optionst &options) } status() << "Instrumenting coverge goals" << eom; - instrument_cover_goalst goals(symbol_table,{c}); + instrument_cover_goalst goals(symbol_table, {c}); goals.instrument_cover_goals(goto_model.goto_functions); goto_model.goto_functions.update(); } From 4847351d2e3ed5a8ea82c6e1bea46f5c9075f23b Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Tue, 20 Dec 2016 09:39:24 +0000 Subject: [PATCH 13/17] replace parameter 'i_it' by 'insn' for instrumentation Signed-off-by: Lucas Cordeiro --- src/goto-instrument/cover.cpp | 242 +++++++++++++++++----------------- src/goto-instrument/cover.h | 14 +- 2 files changed, 128 insertions(+), 128 deletions(-) diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index cd506a220af..2389a96b323 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -1263,13 +1263,13 @@ Function: instrument_assertion \*******************************************************************/ void instrument_cover_goalst::instrument_assertion( - goto_programt::instructionst::iterator &i_it) + goto_programt::instructionst::iterator &insn) { - if(i_it->is_assert()) + if(insn->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); + insn->guard=false_exprt(); + insn->source_location.set(ID_coverage_criterion, coverage_criterion); + insn->source_location.set_property_class(property_class); } } @@ -1286,12 +1286,12 @@ Function: instrument_cover \*******************************************************************/ void instrument_cover_goalst::instrument_cover( - goto_programt::instructionst::iterator &i_it) + goto_programt::instructionst::iterator &insn) { - if(i_it->is_function_call()) + if(insn->is_function_call()) { const code_function_callt &code_function_call= - to_code_function_call(i_it->code); + 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" && @@ -1299,16 +1299,16 @@ void instrument_cover_goalst::instrument_cover( { 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); + 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(i_it->is_assert()) - i_it->make_skip(); + else if(insn->is_assert()) + insn->make_skip(); } /*******************************************************************\ @@ -1324,19 +1324,19 @@ Function: instrument_location \*******************************************************************/ void instrument_cover_goalst::instrument_location( - goto_programt::instructionst::iterator &i_it, + goto_programt::instructionst::iterator &insn, goto_programt &goto_program, basic_blockst &basic_blocks, std::set &blocks_done) { - if(i_it->is_assert()) - i_it->make_skip(); + if(insn->is_assert()) + insn->make_skip(); - unsigned block_nr=basic_blocks[i_it]; + unsigned block_nr=basic_blocks[insn]; if(blocks_done.insert(block_nr).second) { std::string b=i2string(block_nr); - std::string id=id2string(i_it->function)+"#"+b; + std::string id=id2string(insn->function)+"#"+b; source_locationt source_location= basic_blocks.source_location_map[block_nr]; @@ -1344,14 +1344,14 @@ void instrument_cover_goalst::instrument_location( 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++; + 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++; } } } @@ -1369,23 +1369,23 @@ Function: instrument_branch \*******************************************************************/ void instrument_cover_goalst::instrument_branch( - goto_programt::instructionst::iterator &i_it, + goto_programt::instructionst::iterator &insn, goto_programt &goto_program, basic_blockst &basic_blocks) { - if(i_it->is_assert()) - i_it->make_skip(); + if(insn->is_assert()) + insn->make_skip(); - if(i_it==goto_program.instructions.begin()) + if(insn==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"; + "function "+id2string(insn->function)+" entry point"; - source_locationt source_location=i_it->source_location; + source_locationt source_location=insn->source_location; - goto_programt::targett t=goto_program.insert_before(i_it); + 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); @@ -1393,33 +1393,33 @@ void instrument_cover_goalst::instrument_branch( t->source_location.set_property_class(property_class); } - if(i_it->is_goto() && !i_it->guard.is_true()) + if(insn->is_goto() && !insn->guard.is_true()) { - std::string b=i2string(basic_blocks[i_it]); + std::string b=i2string(basic_blocks[insn]); std::string true_comment= - "function "+id2string(i_it->function)+" block "+b+" branch true"; + "function "+id2string(insn->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++; + "function "+id2string(insn->function)+" block "+b+" branch false"; + + 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); + + 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); + + insn++; + insn++; } } @@ -1436,41 +1436,41 @@ Function: instrument_condition \*******************************************************************/ void instrument_cover_goalst::instrument_condition( - goto_programt::instructionst::iterator &i_it, + goto_programt::instructionst::iterator &insn, goto_programt &goto_program) { - if(i_it->is_assert()) - i_it->make_skip(); + if(insn->is_assert()) + insn->make_skip(); // Conditions are all atomic predicates in the programs. { - const std::set conditions=collect_conditions(i_it); + const std::set conditions=collect_conditions(insn); - const source_locationt source_location=i_it->source_location; + const source_locationt source_location=insn->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); + 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(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); + 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); } for(std::size_t i=0; iis_assert()) - i_it->make_skip(); + if(insn->is_assert()) + insn->make_skip(); // Decisions are maximal Boolean combinations of conditions. { - const std::set decisions=collect_decisions(i_it); + const std::set decisions=collect_decisions(insn); - const source_locationt source_location=i_it->source_location; + const source_locationt source_location=insn->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); + 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(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); + 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); } for(std::size_t i=0; i &blocks_done) { - if(i_it->is_assert()) - i_it->make_skip(); + if(insn->is_assert()) + insn->make_skip(); // 1. Each entry and exit point is invoked // 2. Each decision takes every possible outcome @@ -1552,15 +1552,15 @@ void instrument_cover_goalst::instrument_mcdc( // 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); + 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=i_it->source_location; + const source_locationt source_location=insn->source_location; for(const auto & p : both) { @@ -1574,20 +1574,20 @@ void instrument_cover_goalst::instrument_mcdc( 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(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); + 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(i_it); - 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); + 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= @@ -1625,16 +1625,16 @@ void instrument_cover_goalst::instrument_mcdc( 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->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); + 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 &blocks_done); void instrument_branch( - goto_programt::instructionst::iterator &i_it, + goto_programt::instructionst::iterator &insn, goto_programt &goto_program, basic_blockst &basic_blocks); void instrument_condition( - goto_programt::instructionst::iterator &i_it, + goto_programt::instructionst::iterator &insn, goto_programt &goto_program); void instrument_decision( - goto_programt::instructionst::iterator &i_it, + goto_programt::instructionst::iterator &insn, goto_programt &goto_program); void instrument_mcdc( - goto_programt::instructionst::iterator &i_it, + goto_programt::instructionst::iterator &insn, goto_programt &goto_program, basic_blockst &basic_blocks, std::set &blocks_done); From aa9696d3a279d73b839bdb060f582961700a111c Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Thu, 22 Dec 2016 14:48:44 +0000 Subject: [PATCH 14/17] Split cover.cpp into separate files We have created a base class called cover_utils, which contains all attributes and methods used by all coverage analysis (e.g., location, branch, condition, etc). We have then inhereted instrument_cover_goalst and instrument_mcdc_goalst from that base class. --- src/cbmc/Makefile | 2 + src/goto-instrument/Makefile | 2 +- src/goto-instrument/cover.cpp | 1328 +-------------------------- src/goto-instrument/cover.h | 65 +- src/goto-instrument/cover_mcdc.cpp | 126 +++ src/goto-instrument/cover_mcdc.h | 44 + src/goto-instrument/cover_utils.cpp | 1227 +++++++++++++++++++++++++ src/goto-instrument/cover_utils.h | 141 +++ src/symex/Makefile | 2 + 9 files changed, 1552 insertions(+), 1385 deletions(-) create mode 100644 src/goto-instrument/cover_mcdc.cpp create mode 100644 src/goto-instrument/cover_mcdc.h create mode 100644 src/goto-instrument/cover_utils.cpp create mode 100644 src/goto-instrument/cover_utils.h 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/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 2389a96b323..ee44ada7186 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -16,6 +16,7 @@ Date: May 2016 #include #include "cover.h" +#include "cover_mcdc.h" /*******************************************************************\ @@ -47,1211 +48,6 @@ const char *as_string(coverage_criteriont c) /*******************************************************************\ -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(const exprt &src) -{ - std::set result; - collect_conditions_rec(src, result); - return result; -} - -/*******************************************************************\ - -Function: collect_conditions - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -static 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: - -\*******************************************************************/ - -static 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 <=, !=, >= - -\*******************************************************************/ - -static 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: - -\*******************************************************************/ - -static 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: - -\*******************************************************************/ - -static 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''. - -\*******************************************************************/ - -static 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 - -\*******************************************************************/ - -static std::set 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: - -\*******************************************************************/ - -static std::set 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. - -\*******************************************************************/ - -static 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. - **/ - } -} - -/*******************************************************************\ - -Function: collect_mcdc_controlling - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -static 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: collect_mcdc_controlling_nested - - Inputs: - - Outputs: - - Purpose: This nested method iteratively applies - ''collect_mcdc_controlling'' to every non-atomic expr - within a decision - -\*******************************************************************/ - -static 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 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'' - -\*******************************************************************/ - -static 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; -} - -/*******************************************************************\ - -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. - -\*******************************************************************/ - -static 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); - 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 - -\*******************************************************************/ - -static 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; - } -} - -/*******************************************************************\ - -Function: values_of_atomic_exprs - - Inputs: - - Outputs: - - Purpose: To obtain values of atomic exprs within the super expr - -\*******************************************************************/ - -static 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; -} - -/*******************************************************************\ - -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. - -\*******************************************************************/ - -static 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; -} - -/*******************************************************************\ - -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'' - -\*******************************************************************/ - -static 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; -} - -/*******************************************************************\ - -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. - -\*******************************************************************/ - -static 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()); - } - - 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: - -\*******************************************************************/ - -static 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); - } -} - -/*******************************************************************\ - -Function: collect_decisions - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -static std::set collect_decisions(const exprt &src) -{ - std::set result; - collect_decisions_rec(src, result); - return result; -} - -/*******************************************************************\ - -Function: collect_decisions - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -static 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(); -} - -/*******************************************************************\ - Function: instrument_assertion Inputs: @@ -1527,118 +323,6 @@ void instrument_cover_goalst::instrument_decision( /*******************************************************************\ -Function: instrument_mcdc - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void instrument_cover_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; iis_assert()) i_it->make_skip(); break; + case coverage_criteriont::MCDC: + mcdc.instrument_mcdc(i_it, goto_program, basic_blocks, blocks_done); + break; + default: {} } } diff --git a/src/goto-instrument/cover.h b/src/goto-instrument/cover.h index 6e1f94d8dbf..420360f9b5b 100644 --- a/src/goto-instrument/cover.h +++ b/src/goto-instrument/cover.h @@ -11,64 +11,9 @@ 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, 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_goalst +class instrument_cover_goalst : public instrument_cover_utilst { public: instrument_cover_goalst( @@ -111,12 +56,6 @@ class instrument_cover_goalst goto_programt::instructionst::iterator &insn, goto_programt &goto_program); - void instrument_mcdc( - goto_programt::instructionst::iterator &insn, - goto_programt &goto_program, - basic_blockst &basic_blocks, - std::set &blocks_done); - const namespacet ns; const std::set &criteria; irep_idt coverage_criterion; 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_MCDC_H diff --git a/src/goto-instrument/cover_utils.cpp b/src/goto-instrument/cover_utils.cpp new file mode 100644 index 00000000000..4d043f65903 --- /dev/null +++ b/src/goto-instrument/cover_utils.cpp @@ -0,0 +1,1227 @@ +/*******************************************************************\ + +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 .. From c4bf37100a183f0d1d70ed0686c63cd9fdcc0f28 Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Thu, 22 Dec 2016 15:04:08 +0000 Subject: [PATCH 15/17] Enforced the coding rules in cover_mcdc.h Signed-off-by: Lucas Cordeiro --- src/goto-instrument/cover_mcdc.h | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/src/goto-instrument/cover_mcdc.h b/src/goto-instrument/cover_mcdc.h index a1674174ad4..f43732e4637 100644 --- a/src/goto-instrument/cover_mcdc.h +++ b/src/goto-instrument/cover_mcdc.h @@ -8,23 +8,23 @@ Date: May 2016 \*******************************************************************/ -#ifndef CPROVER_GOTO_INSTRUMENT_MCDC_H -#define CPROVER_GOTO_INSTRUMENT_MCDC_H +#ifndef CPROVER_GOTO_INSTRUMENT_COVER_MCDC_H +#define CPROVER_GOTO_INSTRUMENT_COVER_MCDC_H #include "cover_utils.h" class instrument_mcdc_goalst: public instrument_cover_utilst { public: - instrument_mcdc_goalst( - const namespacet &_ns, - const std::set &_criteria, - const irep_idt &_coverage_criterion, - const irep_idt &_property_class): - ns(_ns), - criteria(_criteria), - coverage_criterion(_coverage_criterion), - property_class(_property_class) + instrument_mcdc_goalst( + const namespacet &_ns, + const std::set &_criteria, + const irep_idt &_coverage_criterion, + const irep_idt &_property_class): + ns(_ns), + criteria(_criteria), + coverage_criterion(_coverage_criterion), + property_class(_property_class) { } @@ -41,4 +41,4 @@ class instrument_mcdc_goalst: public instrument_cover_utilst const irep_idt property_class; }; -#endif // CPROVER_GOTO_INSTRUMENT_MCDC_H +#endif // CPROVER_GOTO_INSTRUMENT_COVER_MCDC_H From 9ed799a39db27dcb9f307746244bd7c94589dbb4 Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Thu, 22 Dec 2016 15:07:34 +0000 Subject: [PATCH 16/17] Enforced the coding rules in cover_utils.cpp Signed-off-by: Lucas Cordeiro --- src/goto-instrument/cover_utils.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/goto-instrument/cover_utils.cpp b/src/goto-instrument/cover_utils.cpp index 4d043f65903..80c480f1f0b 100644 --- a/src/goto-instrument/cover_utils.cpp +++ b/src/goto-instrument/cover_utils.cpp @@ -689,7 +689,8 @@ Function: sign_of_expr \*******************************************************************/ -std::set instrument_cover_utilst::sign_of_expr(const exprt &e, const exprt &E) +std::set instrument_cover_utilst::sign_of_expr( + const exprt &e, const exprt &E) { std::set signs; From 632b21b02985ee91b93c2f2736c39116ca45a10d Mon Sep 17 00:00:00 2001 From: Lucas Cordeiro Date: Thu, 22 Dec 2016 15:09:34 +0000 Subject: [PATCH 17/17] Enforced the coding rules in cover.cpp Signed-off-by: Lucas Cordeiro --- src/goto-instrument/cover.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index ee44ada7186..a63981d4b6e 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -352,7 +352,8 @@ void instrument_cover_goalst::instrument_cover_goals( coverage_criterion=as_string(criterion); property_class="coverage"; - instrument_mcdc_goalst mcdc(ns, criteria, coverage_criterion, property_class); + instrument_mcdc_goalst mcdc( + ns, criteria, coverage_criterion, property_class); Forall_goto_program_instructions(i_it, goto_program) { @@ -390,7 +391,7 @@ void instrument_cover_goalst::instrument_cover_goals( break; case coverage_criteriont::MCDC: - mcdc.instrument_mcdc(i_it, goto_program, basic_blocks, blocks_done); + mcdc.instrument_mcdc(i_it, goto_program, basic_blocks, blocks_done); break; default: {}