[klee-dev] Option for generating MC/DC testcases
David Lightstone
david.lightstone at prodigy.net
Mon May 9 21:27:54 BST 2016
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 <lost404 at 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 <lost404 at 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.lightstone at 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 <lost404 at 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 (lost404 at gmail.com)
>>>>
>>>>> _______________________________________________
>>>>> klee-dev mailing list
>>>>> klee-dev at imperial.ac.uk
>>>>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
-------------- next part --------------
HTML attachment scrubbed and removed
More information about the klee-dev
mailing list