[klee-dev] Option for generating MC/DC testcases

[Damir]

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 <lost404 at 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 <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