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 <lost...@gmail.com> 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 <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
