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

[David B Lightstone]

have reconstructed my test platform enough to run an experiment

The platform is based on LLVM 2.9 

 

Build is in 2 stages

Perform CIL transformation

Compile using llvm-gcc to get the LLVM IR file

 

 

My results for your test problem ((a && b) || c) differ from your results

I get 5 test cases without having to modify the CIL translation

 

( a  b  c)

( 0  0  0)

( 0  0  1)

( 1  0  0)

( 1  1  0)

( 1  0  1)

 

 

gcc -D_GNUCC -E -I /home/dbl/Projects/KLEE/klee-2.9-2015/Source/KLEE/klee/include/klee -DCIL=1 /home/dbl/Projects/CIL/Test/test.c -o ./test.i

/home/dbl/.opam/system/bin/cilly.native --out ./test.cil.c ./test.i

llvm-gcc --emit-llvm -c -g -B /home/dbl/Projects/KLEE/klee-2.9-2015/Source/KLEE/klee/object-basic-uclib-stp/Release+Asserts/lib test.cil.c -o test.cil.bc

/home/dbl/Projects/KLEE/klee-2.9-2015/Source/KLEE/klee/object-basic-uclib-stp/Release+Asserts/bin/klee test.cil.bc

 

The difference relates to the LLVM compilation probably compiler options 

 

 

 

 

From: Damir [mailto:lost404 at gmail.com] 
Sent: Thursday, May 12, 2016 8:54 AM
To: David Lightstone; klee-dev
Subject: Re: [klee-dev] Option for generating MC/DC test cases

 

I found that optimization, it's called simplify cfg, basically it removes short circuiting, it is applied in Klee, that's why klee only provides decision coverage.
If you comment out line in lib/Module/KModule.cpp
pm3.add(createCFGSimplificationPass());
and rebuild klee, then klee will produce short-circuit MCC by default without optimize option and without CIL! 
This pass is enabled by O1 in clang.
So clang with optimization produces non short circuit Boolean evaluation.

 

чт, 12 мая 2016, 15:16 David B Lightstone <david.lightstone at prodigy.net>:

I am going to have to locate my implementation of CIL and KLEE (or reconstruct) before properly responding to this e-mail

Right now I am relying on memory of something that I did about 4 years ago using KLEE 2.7 or 2.9.

 

The question of concern that I have relates to optimization.

 

Both LLVM and KLEE are capable of optimizing in some sense (I do not recall the nature of the KLEE optimization)

When I initially played with the problem I concluded that one of the optimizations (don’t remember which) needed to be eliminated.

 

 

From: Damir [mailto:lost404 at gmail.com] 
Sent: Wednesday, May 11, 2016 2:31 PM
To: david.lightstone at prodigy.net


Cc: klee-dev at imperial.ac.uk
Subject: Re: [klee-dev] Option for generating MC/DC test cases

 

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

You are right, what  you describe is called Short-circuit MC/DC.

I found a very interesting paper about Short-circuit MC/DC and MCC (Multiple Condition Coverage), here: http://link.springer.com/article/10.1007/s00607-014-0418-5 

 

Basically, for non-short-circuit languages like Ada, MCC with N conditions requires 2^n testcases. But, as shown in abovementioned paper, for short-circuit languages, MCC is only a little worse in terms of number of testcases than MC/DC (which is minumum n+1 testcases), so it can be practical to aim to MCC instead. MCC is a superset of MC/DC.

 

So, returning to klee and CIL, I can provide you with another counterexample, taken directly from aforementioned paper.

 

Condition is now  (a && b || c) (or with extra paretheses for readability, (a && b) || c).

 

Basic klee testcases: 

(0 0 0)

(0 0 1) (just decision coverage)

 

Cilly + klee testcases: 

(1 1 0)

 (0 0 0)

 (0 0 1) - (condition coverage and decision coverage)

 

As you can see, CIL + klee cannot provide enough  testcases in this case, it should include (1, 0, 0) for short-circuit MC/DC.

 

Basically, this is what CIL does to the condition:

it replaces

 

if (a && b || c)

      do_then();

else

      do_else();

 

with following:

 

if (a) {

   if (b) {

         do_then();

   }

   else

         goto check_C;

}

else

check_C:

if (c) {

    do_then();

}

else

   do_else();

 

But, if I manually replace "goto check_C" with a copy of the code after that label, klee is finally able to produce 5 testcases:

(0 0 0)

(0 0 1)

(1 1 0)

(1 0 1)

(1 0 0)

 

As you can see, those 5 testcases produce short-circuit MCC, which is a superset of short-circuit MC/DC! That's why you told me earlier that testcases by cilly + klee will be a superset of MC/DC.

 

Unfortunatley, that's not the case, cilly + klee alone cannot produce the desired testcases, but that just gave me an idea of how klee can be changed to produce short-circuit MCC instead of just decision coverage. It just needs not to filter out the testcases that were covering the same block, but came through different paths during evaluation of short-circuit boolean expression.

 

I will run some tests and will get back with the results.

-------------- next part --------------
HTML attachment scrubbed and removed