I'm back with results from using cilly and klee. I used very simple testcase, which declares 3 symbolic variables (a, b and c), and then uses simple decision:
if (a && b && c) do_then(); else do_else(); KLEE gives two testcases on unaltered sources: (0, 0, 0) and (1, 1, 1). They provide condition/decision coverage, but not MC/DC. KLEE with CIL provides 4 testcases, with two extra testcases compared to just KLEE: (0, 0, 0) (1, 0, 0) (1, 1, 0) (1, 1, 1) Unfortunately, it fails to provide MC/DC MC/DC testcase set in this case would be: (1, 1, 1) (0, 1, 1) (1, 0, 1) (1, 1, 0) So, while I can definitely recommend using CIL as a way to generate more testcases than usual KLEE, the initial need for providing a way to automatically generate MC/DC testcases (or emitting warning if such coverage is unattainable) still remains. Thank you for suggestions, they were very helpful! пн, 9 мая 2016 г. в 22:57, Damir <lost...@gmail.com>: > 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 <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