From c29c44e2994f4267e0d2624eaaf7395485fcffd8 Mon Sep 17 00:00:00 2001 From: theyoucheng Date: Tue, 9 Aug 2016 14:06:08 +0100 Subject: [PATCH 1/9] Improved the implementation of "--cover mcdc". --- src/goto-instrument/cover.cpp | 481 +++++++++++++++++++++++++++++++++- 1 file changed, 478 insertions(+), 3 deletions(-) diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index 648f8441e85..0b11612e6f6 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -252,6 +252,29 @@ void collect_mcdc_controlling_rec( if(is_condition(op)) { + if(src.id()==ID_or) + { + std::vector others1, others2; + if(not conditions.empty()) + { + others1.push_back(conjunction(conditions)); + others2.push_back(conjunction(conditions)); + } + + for(unsigned j=0; j o=operands; // 'o[i]' needs to be true and false @@ -289,7 +312,17 @@ void collect_mcdc_controlling_rec( else if(src.id()==ID_not) { exprt e=to_not_expr(src).op(); - collect_mcdc_controlling_rec(e, conditions, result); + if(not is_condition(e)) + collect_mcdc_controlling_rec(e, conditions, result); + else + { + std::vector new_conditions1=conditions; + new_conditions1.push_back(src); + result.insert(conjunction(new_conditions1)); + std::vector new_conditions2=conditions; + new_conditions2.push_back(e); + result.insert(conjunction(new_conditions2)); + } } } @@ -315,9 +348,447 @@ std::set collect_mcdc_controlling( return result; } + +/*******************************************************************\ + +Function: replacement_conjunction + + Inputs: + + Outputs: + + Purpose: To replace the i-th exprt of operands with each + exprt inside new_exprts. + +\*******************************************************************/ + +std::set replacement_conjunction( + const std::set &replacement_exprts, + const std::vector &operands, + const int i) +{ + std::set result; + for(auto &y : replacement_exprts) + { + std::vector others; + for(unsigned j=0; j collect_mcdc_controlling_nested( + const std::set &decisions) +{ + std::set controlling = collect_mcdc_controlling(decisions); + std::set result; + for(auto &src : controlling) + { + std::set s1, s2; + s1.insert(src); + + while(true) //dual-loop structure to eliminate complex non-conditional terms + { + 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(not is_condition(no)) + { + changed=true; + std::set ctrl_no; + ctrl_no.insert(no); + res=collect_mcdc_controlling(ctrl_no); + } + } + else if(not is_condition(operands[i])) + { + changed=true; + std::set ctrl; + ctrl.insert(operands[i]); + res=collect_mcdc_controlling(ctrl); + } + + std::set co=replacement_conjunction(res, operands, i); + s2.insert(co.begin(), co.end()); + if(res.size() > 0) break; + } + if(not changed) s2.insert(x); + } + s1=s2; + if(not changed) {break;} + s2.clear(); + } + + result.insert(s1.begin(), s1.end()); + } + + return result; +} + +/*******************************************************************\ + +Function: sign_of_exprt + + Inputs: E should be the pre-processed output by + ''collect_mcdc_controlling_nested'' + + Outputs: +1 : not negated + 0 : not contained in E + -1 : negated + + Purpose: The sign of exprt ''e'' within the super-exprt ''E'' + +\*******************************************************************/ + +void sign_of_exprt(const exprt &e, const exprt &E, std::set &signs) +{ + auto &ops = E.operands(); + 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(not is_condition(y)) + { + sign_of_exprt(e, y, signs); + } + } + else if(not is_condition(y)) + { + sign_of_exprt(e, y, signs); + } + } +} + +/*******************************************************************\ + +Function: remove_repetition + + Inputs: + + Outputs: + + Purpose: After the ''collect_mcdc_controlling_nested'', there + can be the recurrence of the same exprt in the resulted + set of exprts, and this method will remove the + repetitive ones. + +\*******************************************************************/ + +void remove_repetition(std::set &exprts) +{ + // to obtain the set of atomic conditions + std::set conditions; + for(auto &x: exprts) + { + std::set new_conditions = collect_conditions(x); + conditions.insert(new_conditions.begin(), new_conditions.end()); + } + // exprt that contains multiple signs should be removed + std::set new_exprts; + for(auto &x : exprts) + { + bool kept=true; + for(auto &c : conditions) + { + std::set signs; + sign_of_exprt(c, x, signs); + if(signs.size()>1) + { + kept=false; + break; + } + } + if(kept) new_exprts.insert(x); + } + exprts=new_exprts; + new_exprts.clear(); + + for(auto &x: exprts) + { + bool red=false; + for(auto &y: new_exprts) + { + bool iden = true; + for(auto &c : conditions) + { + std::set signs1, signs2; + sign_of_exprt(c, x, signs1); + sign_of_exprt(c, y, signs2); + int s1=signs1.size(), s2=signs2.size(); + if(s1!=s2) + { + iden=false; + break; + } + else + { + if(s1==0 && s2==0) continue; + if(*(signs1.begin())!=*(signs2.begin())) + { + iden=false; + break; + } + } + } + if(iden) + { + red=true; + break; + } + } + if(not red) new_exprts.insert(x); + } + exprts = new_exprts; +} + +/*******************************************************************\ + +Function: eval_exprt + + Inputs: + + Outputs: + + Purpose: To evaluate the value of exprt ''E'', according to + the atomic exprt values + +\*******************************************************************/ +bool eval_exprt( + const std::map &atomic_exprts, + const exprt &src) +{ + // src is AND + if(src.id()==ID_and) + { + for(auto &x : src.operands()) + if(not eval_exprt(atomic_exprts, x)) + return false; + return true; + } + // src is OR + else if(src.id()==ID_or) + { + unsigned fcount=0; + for(auto &x : src.operands()) + if(not eval_exprt(atomic_exprts, x)) + fcount++; + if(fcountsecond; + } +} + +/*******************************************************************\ + +Function: values_of_atomic_exprts + + Inputs: + + Outputs: + + Purpose: To obtain values of atomic exprts within the super exprt + +\*******************************************************************/ + +std::map values_of_atomic_exprts( + const exprt &e, + const std::set &conditions) +{ + std::map atomic_exprts; + for(auto &c : conditions) + { + std::set signs; + sign_of_exprt(c, e, signs); + if(signs.size()!=1) continue; + if(*signs.begin()==1) atomic_exprts.insert(std::pair(c, true)); + if(*signs.begin()==-1) atomic_exprts.insert(std::pair(c, false)); + } + return atomic_exprts; +} + +/*******************************************************************\ + +Function: is_mcdc_pair + + Inputs: + + Outputs: + + Purpose: To check if the two input exprts are mcdc pairs regarding + the given atomic exprt ''c'' + +\*******************************************************************/ + +bool is_mcdc_pair( + const exprt &e1, + const exprt &e2, + const exprt &c, + const std::set &conditions, + const exprt &decision) +{ + if(e1==e2) return false; + std::map atomic_exprts_e1=values_of_atomic_exprts(e1, conditions); + std::map atomic_exprts_e2=values_of_atomic_exprts(e2, conditions); + if(eval_exprt(atomic_exprts_e1, decision)==eval_exprt(atomic_exprts_e2, decision)) + return false; + if(atomic_exprts_e1.find(c)->second==atomic_exprts_e2.find(c)->second) + return false; + int diff_count=0; + auto eit=atomic_exprts_e1.begin(); + auto xit=atomic_exprts_e2.begin(); + while(eit!=atomic_exprts_e1.end()) + { + if(eit->second!=xit->second) + diff_count++; + if(diff_count>1) break; + eit++; + xit++; + } + if(diff_count==1) return true; + else return false; +} + +/*******************************************************************\ + +Function: find_mcdc_pair + + Inputs: + + Outputs: + + Purpose: To check if we can find the mcdc pair of the + input ''exprt_set'' regarding the atomic exprt ''c'' + +\*******************************************************************/ + +bool find_mcdc_pair( + const exprt &c, + const std::set &exprt_set, + const std::set &conditions, + const exprt &decision) +{ + for(auto y1 : exprt_set) + { + for(auto y2 : exprt_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 + +\*******************************************************************/ + +void minimize_mcdc_controlling( + std::set &controlling, + const exprt &decision) +{ + // to obtain the set of atomic conditions + std::set conditions; + for(auto &x: controlling) + { + std::set new_conditions = collect_conditions(x); + conditions.insert(new_conditions.begin(), new_conditions.end()); + } + + while(true) + { + std::set new_controlling; + bool ctrl_update=false; + for(auto &x : controlling) + { + new_controlling.clear(); + for(auto &y : controlling) + if(y!=x) new_controlling.insert(y); + + bool removing_x=true; + for(auto &c : conditions) + { + bool cOK=find_mcdc_pair(c, new_controlling, conditions, decision); + if(not cOK) + { + removing_x=false; + break; + } + } + + if(removing_x) + { + ctrl_update=true; + break; + } + } + if(ctrl_update) + { + controlling=new_controlling; + } + else break; + } +} + +/*******************************************************************\ + Function: collect_decisions_rec Inputs: @@ -662,7 +1133,10 @@ void instrument_cover_goals( } std::set controlling; - controlling=collect_mcdc_controlling(decisions); + //controlling=collect_mcdc_controlling(decisions); + controlling=collect_mcdc_controlling_nested(decisions); + remove_repetition(controlling); + minimize_mcdc_controlling(controlling, *decisions.begin()); for(const auto & p : controlling) { @@ -672,7 +1146,8 @@ void instrument_cover_goals( "MC/DC independence condition `"+p_string+"'"; goto_program.insert_before_swap(i_it); - i_it->make_assertion(p); + 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_property_class("coverage"); From b4c8ec51620c66a0462603c6a0ed234a6ef4aaf4 Mon Sep 17 00:00:00 2001 From: theyoucheng Date: Tue, 9 Aug 2016 16:52:41 +0100 Subject: [PATCH 2/9] Added test cases for mcdc coverage. --- regression/cbmc-cover/mcdc1/test.desc | 8 +++++++- regression/cbmc-cover/mcdc2/main.c | 17 +++++++++++++++++ regression/cbmc-cover/mcdc2/test.desc | 13 +++++++++++++ regression/cbmc-cover/mcdc3/main.c | 6 ++++++ regression/cbmc-cover/mcdc3/test.desc | 12 ++++++++++++ regression/cbmc-cover/mcdc4/main.c | 18 ++++++++++++++++++ regression/cbmc-cover/mcdc4/test.desc | 14 ++++++++++++++ regression/cbmc-cover/mcdc5/main.c | 17 +++++++++++++++++ regression/cbmc-cover/mcdc5/test.desc | 14 ++++++++++++++ 9 files changed, 118 insertions(+), 1 deletion(-) create mode 100644 regression/cbmc-cover/mcdc2/main.c create mode 100644 regression/cbmc-cover/mcdc2/test.desc create mode 100644 regression/cbmc-cover/mcdc3/main.c create mode 100644 regression/cbmc-cover/mcdc3/test.desc create mode 100644 regression/cbmc-cover/mcdc4/main.c create mode 100644 regression/cbmc-cover/mcdc4/test.desc create mode 100644 regression/cbmc-cover/mcdc5/main.c create mode 100644 regression/cbmc-cover/mcdc5/test.desc diff --git a/regression/cbmc-cover/mcdc1/test.desc b/regression/cbmc-cover/mcdc1/test.desc index ea1f3ed221a..501ac9b0a4a 100644 --- a/regression/cbmc-cover/mcdc1/test.desc +++ b/regression/cbmc-cover/mcdc1/test.desc @@ -3,7 +3,13 @@ main.c --cover mcdc ^EXIT=0$ ^SIGNAL=0$ +^\[main.coverage.1\] file main.c line 25 function main MC/DC independence condition `C && D && !E && A && !B.*: SATISFIED$ +^\[main.coverage.2\] file main.c line 25 function main MC/DC independence condition `C && !D && E && A && !B.*: SATISFIED$ +^\[main.coverage.3\] file main.c line 25 function main MC/DC independence condition `!C && D && E && A && !B.*: SATISFIED$ +^\[main.coverage.4\] file main.c line 25 function main MC/DC independence condition `C && D && E && A && !B.*: SATISFIED$ +^\[main.coverage.5\] file main.c line 25 function main MC/DC independence condition `C && D && E && !A && B.*: SATISFIED$ +^\[main.coverage.6\] file main.c line 25 function main MC/DC independence condition `C && D && E && !A && !B.*: SATISFIED$ ^\*\* .* of .* covered (100.0%)$ -^\*\* Used 6 iterations$ +^\*\* Used 10 iterations$ -- ^warning: ignoring diff --git a/regression/cbmc-cover/mcdc2/main.c b/regression/cbmc-cover/mcdc2/main.c new file mode 100644 index 00000000000..65956a8cdcc --- /dev/null +++ b/regression/cbmc-cover/mcdc2/main.c @@ -0,0 +1,17 @@ +int main() +{ + + __CPROVER_bool A, B, C; + + __CPROVER_input("A", A); + __CPROVER_input("B", B); + __CPROVER_input("C", C); + + if(A||B||C) + { + } + else + { + } + +} diff --git a/regression/cbmc-cover/mcdc2/test.desc b/regression/cbmc-cover/mcdc2/test.desc new file mode 100644 index 00000000000..6c69a4144b5 --- /dev/null +++ b/regression/cbmc-cover/mcdc2/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--cover mcdc +^EXIT=0$ +^SIGNAL=0$ +^\[main.coverage.1\] file main.c line 10 function main MC/DC independence condition `A && !B && !C.*: SATISFIED$ +^\[main.coverage.2\] file main.c line 10 function main MC/DC independence condition `!A && B && !C.*: SATISFIED$ +^\[main.coverage.3\] file main.c line 10 function main MC/DC independence condition `!A && !B && C.*: SATISFIED$ +^\[main.coverage.4\] file main.c line 10 function main MC/DC independence condition `!A && !B && !C.*: SATISFIED$ +^\*\* .* of .* covered (100.0%)$ +^\*\* Used 6 iterations$ +-- +^warning: ignoring diff --git a/regression/cbmc-cover/mcdc3/main.c b/regression/cbmc-cover/mcdc3/main.c new file mode 100644 index 00000000000..721382878d9 --- /dev/null +++ b/regression/cbmc-cover/mcdc3/main.c @@ -0,0 +1,6 @@ +int main() +{ + unsigned x, y; + if (!(x>3) && y<5) + ; +} diff --git a/regression/cbmc-cover/mcdc3/test.desc b/regression/cbmc-cover/mcdc3/test.desc new file mode 100644 index 00000000000..bfbf4d6d094 --- /dev/null +++ b/regression/cbmc-cover/mcdc3/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--cover mcdc +^EXIT=0$ +^SIGNAL=0$ +^\[main.coverage.1\] file main.c line 4 function main MC/DC independence condition `!(x > (unsigned int)3) && !(y < (unsigned int)5).*: SATISFIED$ +^\[main.coverage.2\] file main.c line 4 function main MC/DC independence condition `y < (unsigned int)5 && !(x > (unsigned int)3).*: SATISFIED$ +^\[main.coverage.3\] file main.c line 4 function main MC/DC independence condition `y < (unsigned int)5 && x > (unsigned int)3.*: SATISFIED$ +^\*\* .* of .* covered (100.0%)$ +^\*\* Used 4 iterations$ +-- +^warning: ignoring diff --git a/regression/cbmc-cover/mcdc4/main.c b/regression/cbmc-cover/mcdc4/main.c new file mode 100644 index 00000000000..de87a034783 --- /dev/null +++ b/regression/cbmc-cover/mcdc4/main.c @@ -0,0 +1,18 @@ +int main() +{ + + __CPROVER_bool A, B, C, D; + + __CPROVER_input("A", A); + __CPROVER_input("B", B); + __CPROVER_input("C", C); + __CPROVER_input("D", D); + + if((A && B) || (C && D)) + { + } + else + { + } + +} diff --git a/regression/cbmc-cover/mcdc4/test.desc b/regression/cbmc-cover/mcdc4/test.desc new file mode 100644 index 00000000000..9d55f2ebf19 --- /dev/null +++ b/regression/cbmc-cover/mcdc4/test.desc @@ -0,0 +1,14 @@ +CORE +main.c +--cover mcdc +^EXIT=0$ +^SIGNAL=0$ +^\[main.coverage.1\] file main.c line 11 function main MC/DC independence condition `A && B && C && !D.*: SATISFIED$ +^\[main.coverage.2\] file main.c line 11 function main MC/DC independence condition `A && !B && C && D.*: SATISFIED$ +^\[main.coverage.3\] file main.c line 11 function main MC/DC independence condition `A && !B && C && !D.*: SATISFIED$ +^\[main.coverage.4\] file main.c line 11 function main MC/DC independence condition `!C && D && A && !B.*: SATISFIED$ +^\[main.coverage.5\] file main.c line 11 function main MC/DC independence condition `!A && B && C && !D.*: SATISFIED$ +^\*\* .* of .* covered (100.0%)$ +^\*\* Used 9 iterations$ +-- +^warning: ignoring diff --git a/regression/cbmc-cover/mcdc5/main.c b/regression/cbmc-cover/mcdc5/main.c new file mode 100644 index 00000000000..bab33a4ffe3 --- /dev/null +++ b/regression/cbmc-cover/mcdc5/main.c @@ -0,0 +1,17 @@ +int main() +{ + __CPROVER_bool A, B, C, D; + + __CPROVER_input("A", A); + __CPROVER_input("B", B); + __CPROVER_input("C", C); + __CPROVER_input("D", D); + + if((A || B) && (C || D)) + { + } + else + { + } + +} diff --git a/regression/cbmc-cover/mcdc5/test.desc b/regression/cbmc-cover/mcdc5/test.desc new file mode 100644 index 00000000000..f511684f22e --- /dev/null +++ b/regression/cbmc-cover/mcdc5/test.desc @@ -0,0 +1,14 @@ +CORE +main.c +--cover mcdc +^EXIT=0$ +^SIGNAL=0$ +^\[main.coverage.1\] file main.c line 10 function main MC/DC independence condition `A && !B && C && !D.*: SATISFIED$ +^\[main.coverage.2\] file main.c line 10 function main MC/DC independence condition `!C && D && A && !B.*: SATISFIED$ +^\[main.coverage.3\] file main.c line 10 function main MC/DC independence condition `!C && !D && A && !B.*: SATISFIED$ +^\[main.coverage.4\] file main.c line 10 function main MC/DC independence condition `!A && B && C && !D.*: SATISFIED$ +^\[main.coverage.5\] file main.c line 10 function main MC/DC independence condition `!A && !B && C && !D.*: SATISFIED$ +^\*\* .* of .* covered (100.0%)$ +^\*\* Used 8 iterations$ +-- +^warning: ignoring From 32a10788b7bbfd2fc2b0190dc29177f0791504a1 Mon Sep 17 00:00:00 2001 From: theyoucheng Date: Tue, 9 Aug 2016 17:27:51 +0100 Subject: [PATCH 3/9] Updated the test.desc file of test case cbmc-cover/mcdc1/ --- regression/cbmc-cover/mcdc1/test.desc | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/regression/cbmc-cover/mcdc1/test.desc b/regression/cbmc-cover/mcdc1/test.desc index 501ac9b0a4a..060d9040829 100644 --- a/regression/cbmc-cover/mcdc1/test.desc +++ b/regression/cbmc-cover/mcdc1/test.desc @@ -3,12 +3,12 @@ main.c --cover mcdc ^EXIT=0$ ^SIGNAL=0$ -^\[main.coverage.1\] file main.c line 25 function main MC/DC independence condition `C && D && !E && A && !B.*: SATISFIED$ -^\[main.coverage.2\] file main.c line 25 function main MC/DC independence condition `C && !D && E && A && !B.*: SATISFIED$ -^\[main.coverage.3\] file main.c line 25 function main MC/DC independence condition `!C && D && E && A && !B.*: SATISFIED$ -^\[main.coverage.4\] file main.c line 25 function main MC/DC independence condition `C && D && E && A && !B.*: SATISFIED$ -^\[main.coverage.5\] file main.c line 25 function main MC/DC independence condition `C && D && E && !A && B.*: SATISFIED$ -^\[main.coverage.6\] file main.c line 25 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 `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.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$ -- From c7343b33dc043a6b8069b5cb4082edca5b1b4c60 Mon Sep 17 00:00:00 2001 From: theyoucheng Date: Tue, 9 Aug 2016 22:06:30 +0100 Subject: [PATCH 4/9] Refactored the code for mcdc coverage; added a debug test case "cbmc-cover/mcdc6/". --- regression/cbmc-cover/mcdc1/main.c | 2 ++ regression/cbmc-cover/mcdc2/main.c | 1 + regression/cbmc-cover/mcdc3/main.c | 2 ++ regression/cbmc-cover/mcdc4/main.c | 1 + regression/cbmc-cover/mcdc5/main.c | 1 + regression/cbmc-cover/mcdc5/test.desc | 2 +- regression/cbmc-cover/mcdc6/main.c | 8 +++++ regression/cbmc-cover/mcdc6/test.desc | 11 ++++++ src/goto-instrument/cover.cpp | 49 ++++++++++++++++----------- 9 files changed, 57 insertions(+), 20 deletions(-) create mode 100644 regression/cbmc-cover/mcdc6/main.c create mode 100644 regression/cbmc-cover/mcdc6/test.desc diff --git a/regression/cbmc-cover/mcdc1/main.c b/regression/cbmc-cover/mcdc1/main.c index 5f8f3869543..002fc28c9a6 100644 --- a/regression/cbmc-cover/mcdc1/main.c +++ b/regression/cbmc-cover/mcdc1/main.c @@ -17,4 +17,6 @@ int main() else { } + + return 1; } diff --git a/regression/cbmc-cover/mcdc2/main.c b/regression/cbmc-cover/mcdc2/main.c index 65956a8cdcc..147fe9eb47c 100644 --- a/regression/cbmc-cover/mcdc2/main.c +++ b/regression/cbmc-cover/mcdc2/main.c @@ -14,4 +14,5 @@ int main() { } + return 1; } diff --git a/regression/cbmc-cover/mcdc3/main.c b/regression/cbmc-cover/mcdc3/main.c index 721382878d9..312cf1a35b6 100644 --- a/regression/cbmc-cover/mcdc3/main.c +++ b/regression/cbmc-cover/mcdc3/main.c @@ -3,4 +3,6 @@ int main() unsigned x, y; if (!(x>3) && y<5) ; + + return 1; } diff --git a/regression/cbmc-cover/mcdc4/main.c b/regression/cbmc-cover/mcdc4/main.c index de87a034783..08ea1146922 100644 --- a/regression/cbmc-cover/mcdc4/main.c +++ b/regression/cbmc-cover/mcdc4/main.c @@ -15,4 +15,5 @@ int main() { } + return 1; } diff --git a/regression/cbmc-cover/mcdc5/main.c b/regression/cbmc-cover/mcdc5/main.c index bab33a4ffe3..65a7761db1b 100644 --- a/regression/cbmc-cover/mcdc5/main.c +++ b/regression/cbmc-cover/mcdc5/main.c @@ -14,4 +14,5 @@ int main() { } + return 1; } diff --git a/regression/cbmc-cover/mcdc5/test.desc b/regression/cbmc-cover/mcdc5/test.desc index f511684f22e..c65bbc9cd1d 100644 --- a/regression/cbmc-cover/mcdc5/test.desc +++ b/regression/cbmc-cover/mcdc5/test.desc @@ -9,6 +9,6 @@ main.c ^\[main.coverage.4\] file main.c line 10 function main MC/DC independence condition `!A && B && C && !D.*: SATISFIED$ ^\[main.coverage.5\] file main.c line 10 function main MC/DC independence condition `!A && !B && C && !D.*: SATISFIED$ ^\*\* .* of .* covered (100.0%)$ -^\*\* Used 8 iterations$ +^\*\* Used 9 iterations$ -- ^warning: ignoring diff --git a/regression/cbmc-cover/mcdc6/main.c b/regression/cbmc-cover/mcdc6/main.c new file mode 100644 index 00000000000..cebf2b427a0 --- /dev/null +++ b/regression/cbmc-cover/mcdc6/main.c @@ -0,0 +1,8 @@ +int main() +{ + unsigned x; + if(x<3) + ; + + return 1; +} diff --git a/regression/cbmc-cover/mcdc6/test.desc b/regression/cbmc-cover/mcdc6/test.desc new file mode 100644 index 00000000000..900c9bd09e0 --- /dev/null +++ b/regression/cbmc-cover/mcdc6/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--cover mcdc +^EXIT=0$ +^SIGNAL=0$ +^\[main.coverage.1\] file main.c line 4 function main MC/DC independence condition `!(x < (unsigned int)3).*: SATISFIED$ +^\[main.coverage.2\] file main.c line 4 function main MC/DC independence condition `x < (unsigned int)3.*: SATISFIED$ +^\*\* .* of .* covered (100.0%)$ +^\*\* Used 2 iterations$ +-- +^warning: ignoring diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index 0b11612e6f6..442287e8cc8 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -312,17 +312,19 @@ void collect_mcdc_controlling_rec( else if(src.id()==ID_not) { exprt e=to_not_expr(src).op(); - if(not is_condition(e)) - collect_mcdc_controlling_rec(e, conditions, result); - else - { - std::vector new_conditions1=conditions; - new_conditions1.push_back(src); - result.insert(conjunction(new_conditions1)); - std::vector new_conditions2=conditions; - new_conditions2.push_back(e); - result.insert(conjunction(new_conditions2)); - } + collect_mcdc_controlling_rec(e, conditions, result); + } + else if(is_condition(src)) + { + exprt e=src; + std::vector new_conditions1=conditions; + new_conditions1.push_back(e); + result.insert(conjunction(new_conditions1)); + + //e.make_not(); + std::vector new_conditions2=conditions; + new_conditions2.push_back(not_exprt(e)); + result.insert(conjunction(new_conditions2)); } } @@ -357,8 +359,8 @@ Function: replacement_conjunction Outputs: - Purpose: To replace the i-th exprt of operands with each - exprt inside new_exprts. + Purpose: To replace the i-th exprt of ''operands'' with each + exprt inside ''replacement_exprts''. \*******************************************************************/ @@ -391,9 +393,9 @@ Function: collect_mcdc_controlling_nested Outputs: - Purpose: The nested method iteratively applies + Purpose: This nested method iteratively applies ''collect_mcdc_controlling'' to every non-atomic exprt - of a decision + within a decision \*******************************************************************/ @@ -412,6 +414,11 @@ std::set collect_mcdc_controlling_nested( bool changed=false; for(auto &x : s1) { + if(is_condition(x)) + { + s2.insert(x); + continue; + } std::vector operands; collect_operands(x, operands); for(int i=0; i &signs) { - auto &ops = E.operands(); + std::vector ops; + collect_operands(E, ops); + //auto &ops = E.operands(); for(auto &x : ops) { exprt y(x); @@ -589,10 +598,12 @@ bool eval_exprt( const std::map &atomic_exprts, const exprt &src) { + std::vector operands; + collect_operands(src, operands); // src is AND if(src.id()==ID_and) { - for(auto &x : src.operands()) + for(auto &x : operands) if(not eval_exprt(atomic_exprts, x)) return false; return true; @@ -601,10 +612,10 @@ bool eval_exprt( else if(src.id()==ID_or) { unsigned fcount=0; - for(auto &x : src.operands()) + for(auto &x : operands) if(not eval_exprt(atomic_exprts, x)) fcount++; - if(fcount Date: Wed, 10 Aug 2016 12:01:06 +0100 Subject: [PATCH 5/9] Added more comments; formatted several functions; removed dangling if-else statement. --- src/goto-instrument/cover.cpp | 184 +++++++++++++++++++++++++++------- 1 file changed, 149 insertions(+), 35 deletions(-) diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index 442287e8cc8..a37d254540d 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -224,7 +224,8 @@ Function: collect_mcdc_controlling_rec Outputs: - Purpose: + Purpose: To recursively collect controlling exprts for + for mcdc coverage. \*******************************************************************/ @@ -233,6 +234,7 @@ void collect_mcdc_controlling_rec( 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) { @@ -326,6 +328,10 @@ void collect_mcdc_controlling_rec( new_conditions2.push_back(not_exprt(e)); result.insert(conjunction(new_conditions2)); } + else + { + throw "Unexpected exprt for MC/DC coverage"; + } } /*******************************************************************\ @@ -402,28 +408,49 @@ Function: collect_mcdc_controlling_nested 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 exprts for(auto &src : controlling) { std::set s1, s2; + /** + * The final controlling conditions resulted from ''src'' + * will be stored in ''s1''; ''s2'' is usd to hold the + * temporary expansion. + **/ s1.insert(src); - while(true) //dual-loop structure to eliminate complex non-conditional terms + // dual-loop structure to eliminate complex + // non-atomic-conditional terms + while(true) { bool changed=false; + // the 2nd loop for(auto &x : s1) { + // if ''x'' is atomic conditional term, there + // is no expansion if(is_condition(x)) { s2.insert(x); continue; } + // otherwise, we apply the ''nested'' method to + // each of its operands std::vector operands; collect_operands(x, operands); for(int 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(); @@ -443,17 +470,24 @@ std::set collect_mcdc_controlling_nested( res=collect_mcdc_controlling(ctrl); } - std::set co=replacement_conjunction(res, operands, i); + // To replace a non-atomic exprt with its expansion + std::set co= + replacement_conjunction(res, operands, i); s2.insert(co.begin(), co.end()); if(res.size() > 0) break; } + // if there is no change x.r.t current operands of ''x'', + // i.e., they are all atomic, we reserve ''x'' if(not changed) s2.insert(x); } + // update ''s1'' and check if change happens s1=s2; if(not changed) {break;} s2.clear(); } + // The expansions of each ''src'' should be added into + // the ''result'' result.insert(s1.begin(), s1.end()); } @@ -475,11 +509,12 @@ Function: sign_of_exprt \*******************************************************************/ -void sign_of_exprt(const exprt &e, const exprt &E, std::set &signs) +std::set sign_of_exprt(const exprt &e, const exprt &E) { + std::set signs; + std::vector ops; collect_operands(E, ops); - //auto &ops = E.operands(); for(auto &x : ops) { exprt y(x); @@ -490,14 +525,18 @@ void sign_of_exprt(const exprt &e, const exprt &E, std::set &signs) if(y==e) signs.insert(-1); if(not is_condition(y)) { - sign_of_exprt(e, y, signs); + std::set re=sign_of_exprt(e, y); + signs.insert(re.begin(), re.end()); } } else if(not is_condition(y)) { - sign_of_exprt(e, y, signs); + std::set re=sign_of_exprt(e, y); + signs.insert(re.begin(), re.end()); } } + + return signs; } /*******************************************************************\ @@ -524,15 +563,15 @@ void remove_repetition(std::set &exprts) std::set new_conditions = collect_conditions(x); conditions.insert(new_conditions.begin(), new_conditions.end()); } - // exprt that contains multiple signs should be removed + // exprt that contains multiple (inconsistent) signs should + // be removed std::set new_exprts; for(auto &x : exprts) { bool kept=true; for(auto &c : conditions) { - std::set signs; - sign_of_exprt(c, x, signs); + std::set signs=sign_of_exprt(c, x); if(signs.size()>1) { kept=false; @@ -547,15 +586,21 @@ void remove_repetition(std::set &exprts) for(auto &x: exprts) { bool red=false; + /** + * To check if ''x'' is identical with some + * exprt in ''new_exprts''. Two exprts ''x'' + * and ''y'' are identical iff they have the + * same sign for every atomic condition ''c''. + **/ for(auto &y: new_exprts) { bool iden = true; for(auto &c : conditions) { - std::set signs1, signs2; - sign_of_exprt(c, x, signs1); - sign_of_exprt(c, y, signs2); + std::set signs1=sign_of_exprt(c, x); + std::set signs2=sign_of_exprt(c, y); int s1=signs1.size(), s2=signs2.size(); + // it is easy to check non-equivalence; if(s1!=s2) { iden=false; @@ -564,6 +609,7 @@ void remove_repetition(std::set &exprts) else { if(s1==0 && s2==0) continue; + // it is easy to check non-equivalence if(*(signs1.begin())!=*(signs2.begin())) { iden=false; @@ -571,14 +617,23 @@ void remove_repetition(std::set &exprts) } } } + /** + * If ''x'' is found identical w.r.t some + * exprt in ''new_conditions, we label it + * and break. + **/ if(iden) { red=true; break; } } + // an exprt is added into ''new_exprts'' + // if it is not found repetitive if(not red) new_exprts.insert(x); } + + // update the original ''exprts'' exprts = new_exprts; } @@ -590,7 +645,7 @@ Function: eval_exprt Outputs: - Purpose: To evaluate the value of exprt ''E'', according to + Purpose: To evaluate the value of exprt ''src'', according to the atomic exprt values \*******************************************************************/ @@ -631,6 +686,10 @@ bool eval_exprt( { return atomic_exprts.find(src)->second; } + else + { + throw "Unexpected exprt when evaluating a boolean expression"; + } } /*******************************************************************\ @@ -652,11 +711,12 @@ std::map values_of_atomic_exprts( std::map atomic_exprts; for(auto &c : conditions) { - std::set signs; - sign_of_exprt(c, e, signs); + std::set signs=sign_of_exprt(c, e); if(signs.size()!=1) continue; - if(*signs.begin()==1) atomic_exprts.insert(std::pair(c, true)); - if(*signs.begin()==-1) atomic_exprts.insert(std::pair(c, false)); + if(*signs.begin()==1) + atomic_exprts.insert(std::pair(c, true)); + if(*signs.begin()==-1) + atomic_exprts.insert(std::pair(c, false)); } return atomic_exprts; } @@ -669,8 +729,11 @@ Function: is_mcdc_pair Outputs: - Purpose: To check if the two input exprts are mcdc pairs regarding - the given atomic exprt ''c'' + Purpose: To check if the two input controlling exprts are mcdc + pairs regarding an atomic exprt ''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. \*******************************************************************/ @@ -681,31 +744,52 @@ bool is_mcdc_pair( const std::set &conditions, const exprt &decision) { + // An controlling exprt cannot be mcdc pair of itself if(e1==e2) return false; - std::map atomic_exprts_e1=values_of_atomic_exprts(e1, conditions); - std::map atomic_exprts_e2=values_of_atomic_exprts(e2, conditions); - if(eval_exprt(atomic_exprts_e1, decision)==eval_exprt(atomic_exprts_e2, decision)) + + // To obtain values of each atomic condition within ''e1'' + // and ''e2'' + std::map atomic_exprts_e1= + values_of_atomic_exprts(e1, conditions); + std::map atomic_exprts_e2= + values_of_atomic_exprts(e2, conditions); + + // A mcdc pair should result in different ''decision'' + if(eval_exprt(atomic_exprts_e1, decision) + ==eval_exprt(atomic_exprts_e2, decision)) return false; - if(atomic_exprts_e1.find(c)->second==atomic_exprts_e2.find(c)->second) + + // A mcdc pair regarding an atomic exprt ''c'' + // should have different values of ''c'' + if(atomic_exprts_e1.find(c)->second== + atomic_exprts_e2.find(c)->second) return false; + + /** + * A mcdc pair of controlling exprts regarding ''c'' + * can have different values for only one atomic + * exprt, i.e., ''c''. Otherwise, they are not + * a mcdc pair. + **/ int diff_count=0; - auto eit=atomic_exprts_e1.begin(); - auto xit=atomic_exprts_e2.begin(); - while(eit!=atomic_exprts_e1.end()) + auto e1_it=atomic_exprts_e1.begin(); + auto e2_it=atomic_exprts_e2.begin(); + while(e1_it!=atomic_exprts_e1.end()) { - if(eit->second!=xit->second) + if(e1_it->second!=e2_it->second) diff_count++; if(diff_count>1) break; - eit++; - xit++; + e1_it++; + e2_it++; } + if(diff_count==1) return true; else return false; } /*******************************************************************\ -Function: find_mcdc_pair +Function: has_mcdc_pair Inputs: @@ -716,7 +800,7 @@ Function: find_mcdc_pair \*******************************************************************/ -bool find_mcdc_pair( +bool has_mcdc_pair( const exprt &c, const std::set &exprt_set, const std::set &conditions, @@ -741,13 +825,15 @@ Function: minimize_mcdc_controlling Inputs: The input ''controlling'' should have been processed by ''collect_mcdc_controlling_nested'' - and + and ''remove_repetition'' Outputs: Purpose: This method minimizes the controlling conditions for - mcdc coverage + 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. \*******************************************************************/ @@ -767,16 +853,41 @@ void minimize_mcdc_controlling( { std::set new_controlling; bool ctrl_update=false; + /** + * Iteratively, we test that after removing an item ''x'' + * from the ''controlling'', can a complete mcdc coverage + * over ''decision'' still be reserved? + * + * If yes, we update ''controlling'' with the + * ''new_controlling'' without ''x''; otherwise, we should + * keep ''x'' within ''controlling''. + * + * If in the end all elements ''x'' in ''controlling'' are + * reserved, this means that current ''controlling'' set is + * minimum and the ''while'' loop should be breaked. + * + * Note: implementaion here for the above procedure is + * not (meant to be) optimal. + **/ for(auto &x : controlling) { + // To create a new ''controlling'' set without ''x'' new_controlling.clear(); for(auto &y : controlling) if(y!=x) new_controlling.insert(y); bool removing_x=true; + // For each atomic exprt condition ''c'', to check if its is + // covered by at least a mcdc pair. for(auto &c : conditions) { - bool cOK=find_mcdc_pair(c, new_controlling, conditions, decision); + 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(not cOK) { removing_x=false; @@ -784,12 +895,15 @@ void minimize_mcdc_controlling( } } + // If ''removing_x'' is valid, it is safe to remove ''x'' + // from the original ''controlling'' if(removing_x) { ctrl_update=true; break; } } + // Update ''controlling'' or break the while loop if(ctrl_update) { controlling=new_controlling; From a0d01d02a8ee5e28d4e115c82c813a034dd25b6b Mon Sep 17 00:00:00 2001 From: theyoucheng Date: Wed, 10 Aug 2016 12:07:54 +0100 Subject: [PATCH 6/9] formatted --- src/goto-instrument/cover.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index a37d254540d..60febcdb238 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -755,14 +755,14 @@ bool is_mcdc_pair( values_of_atomic_exprts(e2, conditions); // A mcdc pair should result in different ''decision'' - if(eval_exprt(atomic_exprts_e1, decision) - ==eval_exprt(atomic_exprts_e2, decision)) + if(eval_exprt(atomic_exprts_e1, decision)== + eval_exprt(atomic_exprts_e2, decision)) return false; // A mcdc pair regarding an atomic exprt ''c'' // should have different values of ''c'' if(atomic_exprts_e1.find(c)->second== - atomic_exprts_e2.find(c)->second) + atomic_exprts_e2.find(c)->second) return false; /** From 18c4d53d9300c092ac622af72d78833801469368 Mon Sep 17 00:00:00 2001 From: theyoucheng Date: Thu, 11 Aug 2016 16:17:22 +0100 Subject: [PATCH 7/9] Do not directly handle an atomic condition within "collect_mcdc_controlling_rec". --- regression/cbmc-cover/mcdc6/test.desc | 4 ++-- src/goto-instrument/cover.cpp | 33 +++++++++++++++------------ 2 files changed, 21 insertions(+), 16 deletions(-) diff --git a/regression/cbmc-cover/mcdc6/test.desc b/regression/cbmc-cover/mcdc6/test.desc index 900c9bd09e0..d920e78a57e 100644 --- a/regression/cbmc-cover/mcdc6/test.desc +++ b/regression/cbmc-cover/mcdc6/test.desc @@ -3,8 +3,8 @@ main.c --cover mcdc ^EXIT=0$ ^SIGNAL=0$ -^\[main.coverage.1\] file main.c line 4 function main MC/DC independence condition `!(x < (unsigned int)3).*: SATISFIED$ -^\[main.coverage.2\] file main.c line 4 function main MC/DC independence condition `x < (unsigned int)3.*: SATISFIED$ +^\[main.coverage.1\] file main.c line 4 function main decision/condition `x < (unsigned int)3.* false: SATISFIED$ +^\[main.coverage.2\] file main.c line 4 function main decision/condition `x < (unsigned int)3.* true: SATISFIED$ ^\*\* .* of .* covered (100.0%)$ ^\*\* Used 2 iterations$ -- diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index 60febcdb238..a1b3df2f586 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -314,23 +314,28 @@ void collect_mcdc_controlling_rec( else if(src.id()==ID_not) { exprt e=to_not_expr(src).op(); - collect_mcdc_controlling_rec(e, conditions, result); - } - else if(is_condition(src)) - { - exprt e=src; - std::vector new_conditions1=conditions; - new_conditions1.push_back(e); - result.insert(conjunction(new_conditions1)); - - //e.make_not(); - std::vector new_conditions2=conditions; - new_conditions2.push_back(not_exprt(e)); - result.insert(conjunction(new_conditions2)); + if(not 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 { - throw "Unexpected exprt for MC/DC coverage"; + /** + * 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. + **/ } } From 8af80a735dafaa09b8f79bbf0308108da4c75ebd Mon Sep 17 00:00:00 2001 From: theyoucheng Date: Thu, 11 Aug 2016 18:27:29 +0100 Subject: [PATCH 8/9] When evaluating the value of an expr, the result now will be among +1/-1/0, instead of true/false, as 0 is used to specify that the expr does not exist (in the considered parent-expr context). --- regression/cbmc-cover/mcdc7/main.c | 8 ++ regression/cbmc-cover/mcdc7/test.desc | 13 ++ src/goto-instrument/cover.cpp | 198 +++++++++++++++----------- 3 files changed, 139 insertions(+), 80 deletions(-) create mode 100644 regression/cbmc-cover/mcdc7/main.c create mode 100644 regression/cbmc-cover/mcdc7/test.desc diff --git a/regression/cbmc-cover/mcdc7/main.c b/regression/cbmc-cover/mcdc7/main.c new file mode 100644 index 00000000000..939c0644000 --- /dev/null +++ b/regression/cbmc-cover/mcdc7/main.c @@ -0,0 +1,8 @@ +int main() +{ + signed x, y; + + y = x*123<0 ? 0 : (x*123>100 ? 100 : x*123 ); + + return 1; +} diff --git a/regression/cbmc-cover/mcdc7/test.desc b/regression/cbmc-cover/mcdc7/test.desc new file mode 100644 index 00000000000..f43810e9e45 --- /dev/null +++ b/regression/cbmc-cover/mcdc7/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--cover mcdc +^EXIT=0$ +^SIGNAL=0$ +^\[main.coverage.1\] file main.c line 5 function main decision/condition `x \* 123 > 100.* false: SATISFIED$ +^\[main.coverage.2\] file main.c line 5 function main decision/condition `x \* 123 > 100.* true: SATISFIED$ +^\[main.coverage.3\] file main.c line 5 function main decision/condition `x \* 123 < 0.* false: SATISFIED$ +^\[main.coverage.4\] file main.c line 5 function main decision/condition `x \* 123 < 0.* true: SATISFIED$ +^\*\* .* of .* covered (100.0%)$ +^\*\* Used 2 iterations$ +-- +^warning: ignoring diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index a1b3df2f586..fcd3e5e3eb4 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -224,7 +224,7 @@ Function: collect_mcdc_controlling_rec Outputs: - Purpose: To recursively collect controlling exprts for + Purpose: To recursively collect controlling exprs for for mcdc coverage. \*******************************************************************/ @@ -370,18 +370,18 @@ Function: replacement_conjunction Outputs: - Purpose: To replace the i-th exprt of ''operands'' with each - exprt inside ''replacement_exprts''. + Purpose: To replace the i-th expr of ''operands'' with each + expr inside ''replacement_exprs''. \*******************************************************************/ std::set replacement_conjunction( - const std::set &replacement_exprts, + const std::set &replacement_exprs, const std::vector &operands, const int i) { std::set result; - for(auto &y : replacement_exprts) + for(auto &y : replacement_exprs) { std::vector others; for(unsigned j=0; j collect_mcdc_controlling_nested( std::set result; // For each controlling condition, to check if it contains - // non-atomic exprts + // non-atomic exprs for(auto &src : controlling) { std::set s1, s2; @@ -475,7 +475,7 @@ std::set collect_mcdc_controlling_nested( res=collect_mcdc_controlling(ctrl); } - // To replace a non-atomic exprt with its expansion + // To replace a non-atomic expr with its expansion std::set co= replacement_conjunction(res, operands, i); s2.insert(co.begin(), co.end()); @@ -501,23 +501,44 @@ std::set collect_mcdc_controlling_nested( /*******************************************************************\ -Function: sign_of_exprt +Function: sign_of_expr Inputs: E should be the pre-processed output by ''collect_mcdc_controlling_nested'' Outputs: +1 : not negated - 0 : not contained in E -1 : negated - Purpose: The sign of exprt ''e'' within the super-exprt ''E'' + Purpose: The sign of expr ''e'' within the super-expr ''E'' \*******************************************************************/ -std::set sign_of_exprt(const exprt &e, const exprt &E) +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) @@ -530,13 +551,13 @@ std::set sign_of_exprt(const exprt &e, const exprt &E) if(y==e) signs.insert(-1); if(not is_condition(y)) { - std::set re=sign_of_exprt(e, y); + std::set re=sign_of_expr(e, y); signs.insert(re.begin(), re.end()); } } else if(not is_condition(y)) { - std::set re=sign_of_exprt(e, y); + std::set re=sign_of_expr(e, y); signs.insert(re.begin(), re.end()); } } @@ -553,57 +574,57 @@ Function: remove_repetition Outputs: Purpose: After the ''collect_mcdc_controlling_nested'', there - can be the recurrence of the same exprt in the resulted - set of exprts, and this method will remove the + can be the recurrence of the same expr in the resulted + set of exprs, and this method will remove the repetitive ones. \*******************************************************************/ -void remove_repetition(std::set &exprts) +void remove_repetition(std::set &exprs) { // to obtain the set of atomic conditions std::set conditions; - for(auto &x: exprts) + 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_exprts; - for(auto &x : exprts) + std::set new_exprs; + for(auto &x : exprs) { bool kept=true; for(auto &c : conditions) { - std::set signs=sign_of_exprt(c, x); + std::set signs=sign_of_expr(c, x); if(signs.size()>1) { kept=false; break; } } - if(kept) new_exprts.insert(x); + if(kept) new_exprs.insert(x); } - exprts=new_exprts; - new_exprts.clear(); + exprs=new_exprs; + new_exprs.clear(); - for(auto &x: exprts) + for(auto &x: exprs) { bool red=false; /** * To check if ''x'' is identical with some - * exprt in ''new_exprts''. Two exprts ''x'' + * 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_exprts) + for(auto &y: new_exprs) { bool iden = true; for(auto &c : conditions) { - std::set signs1=sign_of_exprt(c, x); - std::set signs2=sign_of_exprt(c, y); + std::set signs1=sign_of_expr(c, x); + std::set signs2=sign_of_expr(c, y); int s1=signs1.size(), s2=signs2.size(); // it is easy to check non-equivalence; if(s1!=s2) @@ -624,7 +645,7 @@ void remove_repetition(std::set &exprts) } /** * If ''x'' is found identical w.r.t some - * exprt in ''new_conditions, we label it + * expr in ''new_conditions, we label it * and break. **/ if(iden) @@ -633,29 +654,29 @@ void remove_repetition(std::set &exprts) break; } } - // an exprt is added into ''new_exprts'' + // an expr is added into ''new_exprs'' // if it is not found repetitive - if(not red) new_exprts.insert(x); + if(not red) new_exprs.insert(x); } - // update the original ''exprts'' - exprts = new_exprts; + // update the original ''exprs'' + exprs = new_exprs; } /*******************************************************************\ -Function: eval_exprt +Function: eval_expr Inputs: Outputs: - Purpose: To evaluate the value of exprt ''src'', according to - the atomic exprt values + Purpose: To evaluate the value of expr ''src'', according to + the atomic expr values \*******************************************************************/ -bool eval_exprt( - const std::map &atomic_exprts, +bool eval_expr( + const std::map &atomic_exprs, const exprt &src) { std::vector operands; @@ -664,7 +685,7 @@ bool eval_exprt( if(src.id()==ID_and) { for(auto &x : operands) - if(not eval_exprt(atomic_exprts, x)) + if(not eval_expr(atomic_exprs, x)) return false; return true; } @@ -673,7 +694,7 @@ bool eval_exprt( { unsigned fcount=0; for(auto &x : operands) - if(not eval_exprt(atomic_exprts, x)) + if(not eval_expr(atomic_exprs, x)) fcount++; if(fcountsecond; + if(atomic_exprs.find(src)->second==+1) + return true; + else if(atomic_exprs.find(src)->second==-1) + return false; } else { - throw "Unexpected exprt when evaluating a boolean expression"; + throw "Unexpected expr when evaluating a boolean expression"; } } /*******************************************************************\ -Function: values_of_atomic_exprts +Function: values_of_atomic_exprs Inputs: Outputs: - Purpose: To obtain values of atomic exprts within the super exprt + Purpose: To obtain values of atomic exprs within the super expr \*******************************************************************/ -std::map values_of_atomic_exprts( +std::map values_of_atomic_exprs( const exprt &e, const std::set &conditions) { - std::map atomic_exprts; + std::map atomic_exprs; for(auto &c : conditions) { - std::set signs=sign_of_exprt(c, e); + std::set signs=sign_of_expr(c, e); + if(signs.size()==0) + { + // ''c'' is not contained in ''e'' + atomic_exprs.insert(std::pair(c, 0)); + continue; + } + // we do not consider inconsistent expr ''e'' if(signs.size()!=1) continue; - if(*signs.begin()==1) - atomic_exprts.insert(std::pair(c, true)); - if(*signs.begin()==-1) - atomic_exprts.insert(std::pair(c, false)); + + atomic_exprs.insert( + std::pair(c, *signs.begin())); } - return atomic_exprts; + return atomic_exprs; } /*******************************************************************\ @@ -734,8 +764,8 @@ Function: is_mcdc_pair Outputs: - Purpose: To check if the two input controlling exprts are mcdc - pairs regarding an atomic exprt ''c''. A mcdc pair of + 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. @@ -749,37 +779,43 @@ bool is_mcdc_pair( const std::set &conditions, const exprt &decision) { - // An controlling exprt cannot be mcdc pair of itself + // 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_exprts_e1= - values_of_atomic_exprts(e1, conditions); - std::map atomic_exprts_e2= - values_of_atomic_exprts(e2, conditions); + 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 should result in different ''decision'' - if(eval_exprt(atomic_exprts_e1, decision)== - eval_exprt(atomic_exprts_e2, decision)) + // A mcdc pair regarding an atomic expr ''c'' + // should have different values of ''c'' + if(cs1==cs2) return false; - // A mcdc pair regarding an atomic exprt ''c'' - // should have different values of ''c'' - if(atomic_exprts_e1.find(c)->second== - atomic_exprts_e2.find(c)->second) + // 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 exprts regarding ''c'' + * A mcdc pair of controlling exprs regarding ''c'' * can have different values for only one atomic - * exprt, i.e., ''c''. Otherwise, they are not + * expr, i.e., ''c''. Otherwise, they are not * a mcdc pair. **/ int diff_count=0; - auto e1_it=atomic_exprts_e1.begin(); - auto e2_it=atomic_exprts_e2.begin(); - while(e1_it!=atomic_exprts_e1.end()) + 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++; @@ -801,19 +837,19 @@ Function: has_mcdc_pair Outputs: Purpose: To check if we can find the mcdc pair of the - input ''exprt_set'' regarding the atomic exprt ''c'' + input ''expr_set'' regarding the atomic expr ''c'' \*******************************************************************/ bool has_mcdc_pair( const exprt &c, - const std::set &exprt_set, + const std::set &expr_set, const std::set &conditions, const exprt &decision) { - for(auto y1 : exprt_set) + for(auto y1 : expr_set) { - for(auto y2 : exprt_set) + for(auto y2 : expr_set) { if(is_mcdc_pair(y1, y2, c, conditions, decision)) { @@ -882,7 +918,7 @@ void minimize_mcdc_controlling( if(y!=x) new_controlling.insert(y); bool removing_x=true; - // For each atomic exprt condition ''c'', to check if its is + // For each atomic expr condition ''c'', to check if its is // covered by at least a mcdc pair. for(auto &c : conditions) { @@ -1249,14 +1285,16 @@ void instrument_cover_goals( std::string comment_t=description+" `"+p_string+"' true"; goto_program.insert_before_swap(i_it); - i_it->make_assertion(p); + //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_property_class("coverage"); 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(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_property_class("coverage"); From 90905321b7bf6c6a6d6bf7a2788f13a915884123 Mon Sep 17 00:00:00 2001 From: theyoucheng Date: Thu, 11 Aug 2016 19:11:24 +0100 Subject: [PATCH 9/9] Removed dangling if-else statements. --- src/goto-instrument/cover.cpp | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/goto-instrument/cover.cpp b/src/goto-instrument/cover.cpp index fcd3e5e3eb4..66411824d9f 100644 --- a/src/goto-instrument/cover.cpp +++ b/src/goto-instrument/cover.cpp @@ -708,17 +708,15 @@ bool eval_expr( no_op.make_not(); return not 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; } - else - { - throw "Unexpected expr when evaluating a boolean expression"; - } } /*******************************************************************\ @@ -1304,6 +1302,8 @@ void instrument_cover_goals( //controlling=collect_mcdc_controlling(decisions); controlling=collect_mcdc_controlling_nested(decisions); remove_repetition(controlling); + // for now, we restrict to the case of a single ''decision''; + // however, this is not true, e.g., ''? :'' operator. minimize_mcdc_controlling(controlling, *decisions.begin()); for(const auto & p : controlling)