[klee-dev] Number of paths in presence of 'select' instruction

[Boris Yakobowski]

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