Hi, thanks for the feedback! I modelled the constraints using online Z3 modeller, it looks like entirely possible. The only trick I don't know is how to duplicate all current constraints, make them refer to two different sets of symbolic variables, and then join those sets using asserts like (A(x1, y1, z1) == false, A(x2, y2, z2) == true, B(x1, y1, z1) == Bfixed, B(x2, y2, z2) == Bfixed etc).
Can you please elaborate, how preprocessing can help? пн, 9 мая 2016 г. в 18:32, David Lightstone <david.lightst...@prodigy.net>: > I dug into this years ago. At the time KLEE could not do it. Whether KLEE > is now able to do so is doubtful (pure guts evaluation) > > i did however discover a possible work around ( possibility dependent upon > the subset of C used) > > That work around being to preprocess the source code thru George Necula's > CIL, and use the preprocesser result instead of the original code > > The test cases which you will generate will probably be a superset of the > MC/DC test cases of the original source. > > Dave Lightstone > > Sent from my iPad > > On May 9, 2016, at 4:55 AM, Damir <lost...@gmail.com> wrote: > > > Hello everyone! > > I've recently started using KLEE, and I'm wondering how hard it would be > to implement full MC/DC testcases generation in KLEE. > > You can read about MC/DC on Wiki > > https://en.wikipedia.org/wiki/Modified_condition/decision_coverage > > I've done some analysis, and figured out how it can be done in klee, > theoretically, > > As I see it, implementing such feature would require tampering with > forking mechanism in KLEE, in following ways: > > 1) Allow breaking a complex decision into conditions, for example > > if (A && B && C) > the decision is (A && B && C) here, and conditions are A, B and C. > > All conditions are functions of symbolic variables, returning boolean, > and combined into decision using only boolean logic. > > 2) Instead of forking on whether decision is true or false, forks are > based on conditions. > > Before (current KLEE): > > fork 1: Decision(A, B, C) == false > fork 2: Decision(A, B, C) == true > > MC/DC way: > > Before forking, set of conditions (in addition to previous ones) must be > solved: > > For example, for condition A: > > A(x1, y1, ... z1) == false > A(x2, y2, ... z2) == true > > B(x1, y1, ... z1) == Bfixed > B(x2, y2, .... z2) == Bfixed > > C(x1, y1, ... z1) == Cfixed > C(x2, y2, .... z2) == Cfixed > > Decision(x1, y1, ... z1) != Decision(x2, y2, ... z2) > > If there is a solution (Bfixed, Cfixed) to those constraints, two forks > are created with following conditions on them: > > fork 1: A == true, B == Bfixed, C == Cfixed > fork 2: A == false, B == Bfixed, C == Cfixed > > If there is no solution to those constraints, then the decision cannot be > covered by MC/DC criteria, this can be reported, and forking on this > condition can be done in a simple way (condition coverage): > > fork1: A == true > fork2: A == false > and then the usual way, fork on (Decision(A,B,C) == false and Decision(A, > B, C) == true) > > So, basically during MC/DC, maximum number of forks is 4 * number of > conditions. > > 3) Testcases can be optimized by removing duplicates. > > Example 1: > > if x is a symbolic variable, and decision is (x > 0 && x < 10), here how > it can be handled in MC/DC way: > > 1) Determine that there are two separate conditions, A(x) = (x > 0) and > B(x) = (x < 10). > 2) For condition A, following set of constraints is introduced: > A(x1) == false > A(x2) == true > B(x1) == Bfixed > B(x2) == Bfixed > A(x1) && B(x1) != A(x2) && B(x2) > > It is solved, and is found that Bfixed is true. > So, fork is created with following conditions: > > Fork1: (x > 0) == true , (x < 10) == true, satisfied, testcase is x == 1 > Fork2: (x > 0) == false , (x < 10) == true, satisfied, testcase is x == > 0 > > For condition B, the same procedure applies. > set of constaints is following: > A(x1) == Afixed > A(x2) == Afixed > B(x1) == false > B(x2) == true > A(x1) && B(x1) != A(x2) && B(x2) > > It is solved, and is found that Afixed is true. > > Fork is created with following conditions: > Fork3: x > 0) == true, (x < 10) == true, satisfied, testcase is x == 1 > Fork4: x > 0) == true, (x < 10) == false, satisfied, testcase is x == > 10 > > since condition for fork3 is the same as for fork1, it will produce the > same testcases, and duplicates can be discarded. > > So, three testcases are generated, x == 0, x == 1 and x == 10. When > combined, they satisfy MC/DC criteria on given decision. > > Example 2: > The same as Example 1, but decision is now (x > 0 && x > 10) > > 1) There are two separate conditions, A(x) = (x > 0) and B(x) = (x > 10) > 2) Constraints set for condition A is > A(x1) == false > A(x2) == true > B(x1) == Bfixed > B(x2) == Bfixed > A(x1) && B(x1) != A(x2) && B(x2) > > This set of restraints is unsatisfiable, so MC/DC cannot be reached on > condtion A. Most probably, condition A is redundant. > Then, forking is created using condition coverage: > > Fork1: (x > 0) == true > Fork2: (x > 0) == false > > Then additional forks are created as usual, > Fork 11: (x > 0) == true, (x > 0 && x > 10) == true - satisfied, testcase > is x = 11 > Fork 12: (x > 0) == true, (x > 0 && x > 10) == false - satisfied, testcase > is x == 1 > > Fork 21: (x > 0) == false, (x > 0 && x > 10) == true - unsatisfied > Fork 22: (x > 0) == false, (x > 0 && x > 10) == false, satisfied, testcase > is x = 0 > > For condition B, constraint is: > A(x1) == Afixed > A(x2) == Afixed > B(x1) == false > B(x2) == true > A(x1) && B(x1) != A(x2) && B(x2) > > When solved, it gives Afixed = true. > > Fork3: (x > 0) == true, (x > 10) == true, satisfied, testcase is x == 11 > Fork4: (x > 0) == true, (x > 10) == false, satisfied, testcase is x == 1 > > After removing duplicate testcases, three testcases remain: x == 0,. x > == 1 and x == 11. They do not satisfy MC/DC criteria though, and warning > can be produced, > that condition A cannot be covered by MC/DC on every path. > > Thanks for reading up to this point! > > The question is, any idea, how this procedure can be implemented in KLEE? > I see it as an option to klee, turning it on would enable MC/DC analysis, > generate more testcases > and produce warnings if some decisions cannot satisfy MC/DC criteria. > > Where can I start, what files I should change to implement it? > > --- > With best regards, > Damir Shaykhutdinov (lost...@gmail.com) > > _______________________________________________ > klee-dev mailing list > klee-dev@imperial.ac.uk > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > >
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
