[klee-dev] Option for generating MC/DC test cases

Tue May 10 20:55:27 BST 2016

Reply within body of original

From: Damir [mailto:lost404 at gmail.com] 
Sent: Tuesday, May 10, 2016 2:44 PM
To: David Lightstone
Cc: klee-dev at imperial.ac.uk
Subject: Re: [klee-dev] Option for generating MC/DC testcases

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)

>From a pure logic perspective you would expect the MC/DC test cases to be as you have describe ( above). That is each conditional term must be evaluated each time the Boolean expression must be evaluated

The C programming language is unfortunately short circuiting. Once it determines that further evaluation of a Boolean expression is unnecessary it cease to evaluate further conditional terms of the expression

In the table below X is used to indicate a conditional term not considered in the evaluation of the Boolean expression

a   b  c

(0, X, X)

(1, 0, X)

(1, 1, 0)

(1, 1, 1)

I disagree with your conclusion.

The test cases which you have declared inconsistent with MC/DC are consistent with my understanding of MC/DC (as applied to C).

My understanding of the goal of MC/DC is – establish that each term of the expression can independently influence the result of the evaluation

Term a is established by (0, X, X) 

                                            (1, 0, X)

Term b is established by (1, 0, X)

                                            (1, 1, 0)

Term c is established by (1, 1, 0) 

                                            (1, 1, 1)

Read CAST 10 at http://www.faa.gov/aircraft/air_cert/design_approvals/air_software/cast/cast_papers/archive/ 

It’s a bit confusing but it does address matters 

The key criteria (applicable here) are

1. Structural coverage guidelines are: 

a) Every statement in the program has been invoked at least once; 

b) Every point of entry and exit in the program has been invoked at least once; 

c) Every control statement (i.e., branch point) in the program has taken all possible outcomes (i.e., branches) at least once; 

d) Every non-constant Boolean expression in the program has evaluated to both a True and a False result; 

e) Every non-constant condition in a Boolean expression in the program has evaluated to both a True and a False result; 

f) Every non-constant condition in a Boolean expression in the program has been shown to independently affect that expression's outcome. 

2. Based upon these definitions: 

• Statement Coverage requires (a) only 

• DC requires (b, c, d) 

• MC/DC requires (b, c, d, e, f) 

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