Thank you, I'll look into it. I run my examples through gcc -E. then cilly, then clang, and then klee, and got 3 testcases for each one, which satisfy MC/DC for example 1.
That's good enough for me now, though I wanted to get a warning, if MC/DC can be achieved on a decision. So far I suspect I don't get MC/DC, but a simple condition/decision coverage. Need to check it again, messing with syntactically correct transformation can give a too narrow testcase set. I'll try to find a counterexample. Thanks again! > It completely eliminates the syntatic sugar. Transforming the original > source into an equivalent which has no boolean expressions what-so-ever. > That means for the transformed code there is only branch coverage to > consider. KLEE can handle branch coverage. > > Google on the search criteria George Necula CIL > You will find the published paper's pdf and a source for the translater > > Dave Lightstone > > Sent from my iPad > > On May 9, 2016, at 11:58 AM, Damir <[email protected]> wrote: > > 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 <[email protected] > >: > >> 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 <[email protected]> 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 ([email protected]) >> >> _______________________________________________ >> klee-dev mailing list >> [email protected] >> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev >> >>
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
