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.lightst...@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:lost...@gmail.com] > *Sent:* Wednesday, May 11, 2016 2:31 PM > *To:* david.lightst...@prodigy.net > > > *Cc:* klee-dev@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. >
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
