Hi,
I've been trying to use Klee on top of gnat-llvm, an experimental Ada to
LLVM bitcode compiler which is being developed right now. I've ported
the example of the Sign tutorial to Ada, but the results are not exactly
what we expected. This is the intermediate IL produced by the compiler
for the sign function:
define i32 @get_sign(i32 %x) !dbg !9 {
entry:
%0 = icmp eq i32 %x, 0, !dbg !11
br i1 %0, label %true, label %false, !dbg !11
true: ; preds = %entry
ret i32 0, !dbg !12
false: ; preds = %entry
%1 = icmp slt i32 %x, 0, !dbg !13
br i1 %1, label %true1, label %false2, !dbg !13
true1: ; preds = %false
ret i32 -1, !dbg !14
false2: ; preds = %false
ret i32 1, !dbg !15
end: ; preds =
%unreachable4, %unreachable3, %unreachable
unreachable, !dbg !15
unreachable: ; No predecessors!
br label %end, !dbg !12
unreachable3: ; No predecessors!
br label %end, !dbg !14
unreachable4: ; No predecessors!
br label %end, !dbg !15
}
This is significantly more optimized than what is obtained by default
with clang, and Klee is apparently smart enough to further simplify
this. This is what I get using -debug-print-instructions=all:stderr:
sign.adb:8:21: %0 = icmp eq i32 %x, 0, !dbg !31
sign.adb:10:22: %1 = icmp slt i32 %x, 0, !dbg !32
sign.adb:10:23: %. = select i1 %1, i32 -1, i32 1
sign.adb:8:24: %merge = select i1 %0, i32 0, i32 %., !dbg !31
sign.adb:9:25: ret i32 %merge, !dbg !33
The 'br' instructions have been transformed into a 'select', and Klee
finds only 1 path, instead of the expected 3. I found this related
question
https://mailman.ic.ac.uk/mailman/htdig/klee-dev/2016-April/001332.html,
and removing the call to createCFGSimplificationPass() in
KModule::prepare is enough. But I still have two questions:
- why is the 'select' instruction not recognized as creating paths?
- is it safe to remove this particular call to createCFGSimplificationPass.
(All this has been done with LLVM 5.0, in case this makes a difference.)
Thanks for any input!
--
Boris Yakobowski
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
