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

[Andrew Santosa]

Hi Boris,

The select instruction can typically be handled by an SMT solver primitive, usually called "ite",
hence it seems advantageous in terms of efficiency not to fork a new branch for it.

It looks benign enough to remove the whole statement

pm3.add(createCFGSimplificationPass());
in KModule::prepare(). If I were you I would just try it out.

Best,
Andrew
 

    On Monday, 16 April 2018, 6:37:14 pm GMT+8, Boris Yakobowski <yakobowski at adacore.com> wrote:  
 
 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 at imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
  
-------------- next part --------------
HTML attachment scrubbed and removed