Re: [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 :

> 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  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 > >:
>>
>>> 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  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 

Re: [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  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  >:
>
>> 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  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, 

Re: [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 :

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