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

[Damir]

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