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

[Damir]

Hello Dan, thanks for the answer!


> Your analysis here isn't really correct here. If KLEE worked directly
> on C code your analysis might be in some cases but that is not how
> KLEE is implemented. KLEE works on LLVM IR so that needs to be
> considered when thinking about implementing new features. I also don't
> think you are trying to do will work in general as it assumes
> "conditions" are simple expressions that don't contain forking.
>

In fact, the fact that KLEE works on LLVM IR is very good, since clang
 does the job
of splitting boolean expressions (decisions) into conditions by itself, by
implementing short-circuting.
For example, this is how "if (a && b || c)" looks like in IR (simplified
for readability):
...
check_a:
%1 = icmp ne i32 %a, 0
br i1 %1, check_b, check_c

check_b:
%2 = icmp ne i32 %b, 0
br i1 %2, do_then, check_c

check_c:
%3 = icmp ne i32 %c, 0
br i1 %3, do_then, do_else

As you can see, clang really does  a very nice thing and split the
expression for us.

First in the LLVM IR that KLEE interprets the conditions will likely
> appear as separate branch instructions as they are short-circuiting
> operators (they might not depending on if LLVM's optimizer modifies
> the branches)
>
As stated previously, this is an advantage really.


> Second your conditions in general might not be plain expressions. They
> could be function calls for example which may contain forking. E.g.
>
> ```
> void foo(const char* a) {
>   if ( strlen(a) == 5 && a[0]='h' && (a[1] == 'i] || a[1] == 'x')) {
>       // do something
>   }
>
> }
> ```
>
> one or more of the conditionals may change the state of the program too.
>

That is true. And it really prevents correct implementation of MC/DC in a
way I expressed earlier. But by changing the goal from providing MC/DC
coverage to providing short-circuit Multiple Condition Coverage, which is a
superset of short-circuit MC/DC.

All we need is to provide testcases that cover all short-circuit decision
paths.

For example above, we need to provide tests for following paths:
check_a -> check_c -> do_then (a = 0, b = 0 or 1, c = 1)
check_a -> check_c -> do_else (a = 0, b = 0 or 1, c = 0)
check_a -> check_b -> do_then (a = 1, b = 1, c = 0 or 1)
check_a -> check_b -> check-c -> do_then (a = 1, b = 0, c = 1)
check_a -> check_b -> check_c -> do_else (a = 1, b = 0, c = 0)

Those 5 cases are enough to provide Multimple Condition Coverage, a
superset of short-circuit MC/DC. And it looks like it's much easier to
implement in KLEE, since all you do is not to filter out the testcases that
come from different paths on the way of evaluating any short-curcuit
boolean expressions.

Can you tell me what would need to be changed in KLEE to make it possible?

For these merged branches we would handle them specially by trying for
> each condition to fork on that condition while holding the other
> conditions as the having the same value on either side of the fork. If
> for a particular condition we can't fork then we know that the
> condition can't affect the branch and that for the particular path we
> are on that condition is irrelevant. Note I said "particular path"
> here! There could be another path where the condition could affect the
> branch.



> I'm not sure if MC/DC says anything about this (i.e. whether a
> condition must independently effect a branch for all paths leading to
> the condition or if just a single path must do this).
>

In MC/DC, last C stands for Coverage, so it's a coverage metrics, based on
all paths demonstrated during running the test cases. So, just a single
path should do it, as long as there are enough such paths to cover
conditions and decision outcome.
-------------- next part --------------
HTML attachment scrubbed and removed