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

[Damir]

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