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

Reply via email to