Boundary value analysis (do not merge)

[lucasccordeiro]

No description provided.

[kroening]

Can you restore this change, please? You have overwritten some commits.

[kroening]

Please make 'boundary-values' and MC/DC independent. One can give two --cover options to get both together.

[theyoucheng]

Unfortunately, the 'boundary-value-analysis' here is not really independent from the MC/DC criterion. It applies to the test cases generated by MC/DC.

For example, given a the decision 'x<3 && y<=5', three tests will be generated following MC/DC:

1. x<3 && y<=5
2. x>=3 && y<=5
3. x<3 && y>5
   The boundary value analysis then applies to each test generated, the 2nd one (similar for the 1st one) will be split into
   2.1) x>3 && y<5
   2.2) x==3 && y<5
   2.3) x>3 && y==5
   2.4) x==3 && y==5

Is it possible to

1. create a criterion named (let's say) 'MCDC_BOUNDARY'
   or 2) add an option 'boundary-values' to --cover and its combination with 'mcdc' triggers the boundary value analysis after normal MC/DC?

[kroening]

Let's go for option 2, I would consider that cleaner.

[theyoucheng]

Sent the implementation to Lucas. While I only changed several lines of codes, the diff seems to be quite big.

The 'cover.cpp' becomes more complex day by day. Thinking to refactor the coverage codes. A class like 'class coveraget'?

[tautschnig]

This approach seems rather inefficient: iterate over all the instructions multiple times? Wouldn't it be possible to turn the criteria into several Booleans and then stick with the previous code that primarily iterates over the instructions? For each instruction, then test, e.g., is_assert() && cover_assertions (with cover_assertions being such a Boolean variable that equals criteria.find(coverage_criteriont::ASSERTION)!=criteria.end().

[tautschnig]

Why is this change necessary?

[tautschnig]

Is there a particular reason for using sets over hash_set_cont?

[tautschnig]

Do all these functions genuinely need to go in the global namespace? Wouldn't it be sufficient to have them as static procedures in the cpp file?

[tautschnig]

Wouldn't it be simpler to copy the entire expression and replace the id()? That is, do exprt e1(src); e1.id(ID_lt);

[tautschnig]

if(!res.empty()) break; (.size() may have linear complexity, empty() is constant time)

[tautschnig]

Avoid while(true) loops - pull bool changed out of the loop and explicitly use while(changed) or while(!changed)

[tautschnig]

changed=!res.empty() || changed;

[tautschnig]

return src.id()==ID_lt || ...;

[tautschnig]

No need to keep old code, we have version control.

[theyoucheng]

On 11/10/16 10:24 PM, Michael Tautschnig wrote:

@tautschnig requested changes on this pull request.

---

In src/goto-instrument/cover.cpp
#298 (review):

{

• switch(criterion)
• const irep_idt coverage_criterion=as_string(criterion);
• const irep_idt property_class="coverage";

• Forall_goto_program_instructions(i_it, goto_program)

This approach seems rather inefficient: iterate over all the
instructions multiple times? Wouldn't it be possible to turn the
criteria into several Booleans and then stick with the previous code
that primarily iterates over the instructions? For each instruction,
then test, e.g., is_assert() && cover_assertions (with
cover_assertions being such a Boolean variable that equals
criteria.find(coverage_criteriont::ASSERTION)!=criteria.end().

Agree. I guess the initial implementation put the emphasis on simplicity.

---

In src/goto-instrument/cover.cpp
#298 (review):

 collect_mcdc_controlling_rec(d, { }, result);

• }

Why is this change necessary?

---

In src/goto-instrument/cover.h
#298 (review):

void instrument_cover_goals(
const symbol_tablet &symbol_table,
goto_functionst &goto_functions,

• coverage_criteriont);
• const std::set<coverage_criteriont> &criteria);

+// functions for boundary values analysis
+std::set non_ordered_expr_expansion(const exprt &src);

Is there a particular reason for using sets over hash_set_cont?

I don't think so.

In src/goto-instrument/cover.h
#298 (review):

• coverage_criteriont);
• const std::set<coverage_criteriont> &criteria);

+// functions for boundary values analysis
+std::set non_ordered_expr_expansion(const exprt &src);
+std::set decision_expansion(const exprt &dec);
+std::set non_ordered_predicate_expansion(const exprt &src);
+std::set ordered_negation(const exprt &src);
+bool is_arithmetic_predicate(const exprt &src);
+
+// a set of help methods
+void collect_operands(const exprt &src, std::vector &dest);
+std::set replacement_and_conjunction(

• const std::set &replacement_exprs,
• const std::vector &operands,
• const std::size_t i);

Do all these functions genuinely need to go in the global namespace?
Wouldn't it be sufficient to have them as static procedures in the cpp
file?

I do not like puting them here either. To avoid growing the cover.cpp
file unlimitedly, I try to seperate some functionalities into different
files (i.e., cover_boundary_values.cpp). But I definitely agree it is
not really good to put these functions at their current place.

---

In src/goto-instrument/cover_boundary_values.cpp
#298 (review):

• 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());

Wouldn't it be simpler to copy the entire expression and replace the
id()? That is, do exprt e1(src); e1.id(ID_lt);

got it.

In src/goto-instrument/cover_boundary_values.cpp
#298 (review):

• 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"
  

Use || instead of "or"

OK.

In src/goto-instrument/cover_boundary_values.cpp
#298 (review):

• 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"

src.op0().is_true() - relying on text output WILL break.

When I obtain an expert 'e' that is 'A!=FALSE', if I call
'e.op1().is_false()' I will get '0'. This is why I instead go for
'from_expr'. I feel also confused here.

---

In src/goto-instrument/cover_boundary_values.cpp
#298 (review):

+*******************************************************************/
+
+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);
  

s1.insert(res.begin(), res.end())

OK.

In src/goto-instrument/cover_boundary_values.cpp
#298 (review):

• 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);

if(src.id()!=ID_not || !is_arithmetic_predicate(src.op0()))
s1.insert(src);

would simplify the code below.

OK.

In src/goto-instrument/cover_boundary_values.cpp
#298 (review):

•    }
  

•    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<exprt> co=replacement_and_conjunction(res, operands, i);
  

•    s2.insert(co.begin(), co.end());
  

•    if(res.size()>0) break;
  

•  }
  

•  if(not changed) s2.insert(x);
  

use ! instead of "not"

OK.

In src/goto-instrument/cover_boundary_values.cpp
#298 (review):

•      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<exprt> 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;

|s1.swap(s2);| since you are destroying the contents afterwards.

OK.

In src/goto-instrument/cover_boundary_values.cpp
#298 (review):

•        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<exprt> co=replacement_and_conjunction(res, operands, i);
  

•    s2.insert(co.begin(), co.end());
  

•    if(res.size()>0) break;
  

|if(!res.empty()) break;| (.size() may have linear complexity, empty()
is constant time)

OK.

In src/goto-instrument/cover_boundary_values.cpp
#298 (review):

• 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)

Avoid while(true) loops - pull |bool changed| out of the loop and
explicitly use |while(changed)| or |while(!changed)|

OK.

In src/goto-instrument/cover_boundary_values.cpp
#298 (review):

•    {
  

•      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;
  

changed=!res.empty() || changed;

OK.

In src/goto-instrument/cover_boundary_values.cpp
#298 (review):

+/*******************************************************************
+
+Function: is_arithmetic_predicate
+

• Inputs:

• Outputs:
  +
• Purpose:
  +
  +*******************************************************************/
  +
  +bool is_arithmetic_predicate(const exprt &src)
  +{
• if(src.id()==ID_lt

|return src.id()==ID_lt || ...;|

OK.

In src/symex/symex_parse_options.cpp
#298 (review):

   else
    {
      error() << "unknown coverage criterion" << eom;
      return true;
    }

    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);
  

No need to keep old code, we have version control.

OK.

Thanks! Going to make changes.

—
You are receiving this because you commented.
Reply to this email directly, view it on GitHub
#298 (review),
or mute the thread
https://github.com/notifications/unsubscribe-auth/ATYfmwzC-KFNXU8gurieaG41ZPl2A5zoks5q85mDgaJpZM4KrMkX.

Youcheng Sun
Research Assistant
Department of Computer Science
University of Oxford
Wolfson Building, Parks Road
Oxford OX1 3QD
https://sites.google.com/site/theyoucheng/

[lucasccordeiro]

@tautschnig: Youcheng tried to implement all your comments related to the boundary value analysis. Let us know if there is still something that should be improved.

[tautschnig]

I still insist that these should be marked static - yes, the file is way too large and should be chopped up, but that shouldn't be stopping anyone from marking them static now so that later, when splitting up, those people understand what the usage scope is.

[tautschnig]

It seems the return type shouldn't even be a set, but a list: the elements are guaranteed to be unique and lookup is not required.

[tautschnig]

See above for comments on return type and marking it static.

[tautschnig]

Several problems here:

1. This assumes that the operands commute as the new element will be the last one.
2. What if operands.size()<=i?
3. Repeated push_back without prior reserve() is inefficient.

I would propose:

assert(operands.size()>i);
std::vector<exprt> others(operands);
others[i]=y;

[tautschnig]

Again, I'm not sure this should be a set - why not a list?

[tautschnig]

This loop looks like programming with gotos, except that gotos would at least have the possibility of meaningful labels. If at least there were some comments saying what the individual branches try to achieve. Also, the s2.insert(x) might be replicated and placed with the individual cases to make clear that x isn't lost in all those if(...) without an else case.

[tautschnig]

How about non_ordered_predicate_expansion just returns its argument when there was nothing to expand? That would avoid those subsequent if(empty) handling.

[tautschnig]

I don't see why that change is required?

[tautschnig]

No white-space changes, please.

[tautschnig]

I like those changes, but it would be great if they were in a separate commit or even pull request as the commit message of this one is not going to explain very well why they had been made.

[kroening]

This will now need a rebase.

[lucasccordeiro]

I have just talked to @theyoucheng.

He'll implement Michael's comments and apply a rebase as suggested by Daniel until 16/12.

[lucasccordeiro]

@tautschnig: This week @theyoucheng is expected to work on your comments.

What do you think if we break your comments into two parts (with two different pull requests): comments related to the boundary value analysis (BVA) and comments related to the existing cover.cpp implementation?

@theyoucheng mentioned that the comments related to the BVA is ok to implement, but most of your comments are related to the existing cover.cpp implementation, which I think it was written by @kroening.

[tautschnig]

@lucasccordeiro @theyoucheng It sounds like very good idea to have two pull requests here, even though there will be some management overhead for you. But hopefully the cover.cpp refactoring can be merged rather soon so that the overhead is kept low.

[lucasccordeiro]

Thanks, @tautschnig. I have talked to @kroening and @peterschrammel about this PR.

@peterschrammel agrees with all your comments. So @theyoucheng is already working on them. Additionally, @peterschrammel also asked me to:

(1) Split the cover.cpp into separate files, one for each instrumentation. Only the main loop should be in cover.cpp
(2) All C-style functions should disappear and become part of classes.

I'll synchronize with @theyoucheng so that we can have all those comments implemented.

[lucasccordeiro]

@tautschnig: There are several coding style errors if we run cpplint.py over cbmc_parse_options.cpp and symex_parse_options.cpp files. Should we fix all of them or just the ones we have introduced?

For cover.cpp and cover.h we believe we have fixed all coding style errors given that we have re-factored that code.

I still have to talk to @peterschrammel about splitting the cover.cpp file into separate files, one for each instrumentation.

[lucasccordeiro]

I have talked to @thk123 at Diffblue. He told me that there is already a pull request to fix the code guideline for cbmc_parse_options.cpp (see #338 #343).

I'm also facing some issues about the errors related to the code guideline, e.g., add space for "+" in expressions like "++it". @thk123 told me that he has already fixed some issues in the cpplint.py script via PR #342.

[lucasccordeiro]

@peterschrammel: I have just split cover.cpp into three separate files. In particular, I have created a base class called "cover_utilst", which contains all common attributes and methods used by all coverage analysis (e.g., location, branch, condition, etc). Thus, I have created the instrument_cover_goalst and instrument_mcdc_goalst classes by inhereting from that base class. If you're happy with this solution, I can replicate this for the other coverage analysis so that we can split cover.cpp into separate files, one for each instrumentation.

[forejtv]

@peterschrammel @lucasccordeiro Does this PR need more changes than a rebase before it can be reviewed in detail again?

[lucasccordeiro]

@forejtv: This PR is quite obsolete. We have to check with @peterschrammel whether it is still useful for CBMC since it will require a significant effort to rebase it again, given that I made structural changes to cover.cpp (e.g., breaking the different coverage metrics into separate files).

[hannes-steffenhagen-diffblue]

Closing since according to the author himself this PR is obsolete.