If you are looking for a means to determine if MC/DC coverage has been achieved look into Couverture
At one time I had it operational ( about 2 years ago). Can't comment on its evolution since then Dave Lightstone Send remotely > On May 9, 2016, at 3:57 PM, Damir <lost...@gmail.com> wrote: > > 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
