[klee-dev] Unexpected behaviour while learning how to use KLEE

[Manuel Carrasco]

Dear klee-dev,

I am learning how to use KLEE and the results I am getting are not the
ones I would expect. Thus, I would be more than grateful if anyone could
spot what I am doing/understanding incorrectly.

To the best of my knowledge, in the following example, there are two
possible paths starting from main, although KLEE (v2.2) only reports one.

|declare void @klee_make_symbolic(i8*, i64, i8*)||
|| ||
||@.stra = private unnamed_addr constant [2 x i8] c"a\00", align 1||
||@.strb = private unnamed_addr constant [2 x i8] c"b\00", align 1||
|| ||
||define i32 @main() {||
||entry:||
||  %a = alloca i32, align 4||
||  %b = alloca i32, align 4||
||  %a_bitcast = bitcast i32* %a to i8*||
||  %b_bitcast = bitcast i32* %b to i8*||
||   ||
||  call void @klee_make_symbolic(i8* %a_bitcast, i64 4, i8*
getelementptr inbounds ([2 x i8], [2 x i8]* @.stra, i64 0, i64 0))||
||  %a_value = load i32, i32* %a, align 4||
|| ||
||  call void @klee_make_symbolic(i8* %b_bitcast, i64 4, i8*
getelementptr inbounds ([2 x i8], [2 x i8]* @.strb, i64 0, i64 0))||
||  %b_value = load i32, i32* %b, align 4||
|| ||
||  %original_result = call i1 @original(i32 %a_value, i32 %b_value)||
||  %final_result = call i1 @final(i32 %a_value, i32 %b_value)||
|| ||
||  %equal = icmp eq i1 %original_result, %final_result||
||  br i1 %equal, label %IfEqual, label %IfUnequal||
|| ||
||IfEqual:||
||    ret i32 0||
|| ||
||IfUnequal:||
||    ret i32 1  ||
||}||
|| ||
||define i1 @original(i32 %"a", i32 %"b") {||
||  %"c" = icmp ugt i32 %"a", %"b"||
||  ret i1 %"c"||
||}||
|| ||
||define i1 @final(i32 %"a", i32 %"b") {||
||  %"c" = icmp sgt i32 %"a", %"b"||
||  ret i1 %"c"||
|

|||}|

Storing the above code as /query.ll/, the command/klee query.ll/ prints|:
|

|||klee at 2444e54c9f66:/shared/test$ klee query.ll
KLEE: output directory is "/shared/test/klee-out-28"
KLEE: Using STP solver backend

KLEE: done: total instructions = 17
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1
|

For instance, these are two possible inputs that would allow me to
explore both paths:

  * "a" = 0x80000000, "b" = 0x1 (/IfUnequal label/)
  * "a" = 0x0, "b" = 0x0 (this is the only one reported by KLEE -
    /IfEqual label/)

Yet, only one is reported and so far I cannot understand the reason why.
Is this related to how i32 integers are represented by KLEE? Conversely,
I would not be surprised if I am doing something wrong.

Kind regards,

Manuel.


||

|
|

|
|

-------------- next part --------------
HTML attachment scrubbed and removed