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@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. || | | | |
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev