Hi Manuel, hi Alastair, Currently, KLEE runs still the `CFGSimplificationPass` even with `—optimize` off. https://github.com/klee/klee/blob/24badb5bf17ff586dc3f1856901f27210713b2ac/lib/Module/KModule.cpp#L288
This might be not necessary anymore for recent LLVM versions. The best way forward is indeed using the `optnone` attribute for functions you are interested in, e.g. compile your code with `-O0` explicitly. There is an option `—klee-call-optimisation=false` which marks functions as `optnone` that contain klee function calls (`klee_make_symbolic`, `klee_assume`, ...), maybe this option might be already sufficient for your use case. Alternatively, try to comment out the line referenced in the link. This might help you in general to workaround this problem. Hope that helps, Martin On 2. Jun 2021, at 19:02, Alastair Reid <[email protected]<mailto:[email protected]>> wrote: I think a KLEE dev will need to suggest how to prevent the optimization from happening. KLEE has a flag controlling optimization "--optimize" - but it is supposed to be off by default -- Alastair On Wed, Jun 2, 2021 at 4:49 PM Manuel Carrasco <[email protected]<mailto:[email protected]>> wrote: Thanks for your answer! You hit the nail on the head. The assembly.ll file contains: %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 %spec.select = select i1 %equal, i32 0, i32 1 ret i32 %spec.select What I understand from this is that KLEE doesn't consider the select instruction as a control flow instruction. Thus, only one path is explored. Is it correct? How would you prevent this optimization from happening? The way I'm using KLEE is by directly inputting a .ll file (the one I originally shared). The only thing that comes to my mind is setting the optnone attribute. In other words, how would you make sure that KLEE doesn't optimize feasible paths? Kind regards, Manuel. On 1/6/21 16:58, Alastair Reid wrote: Hi Manuel, Maybe your code is being optimized to avoid the conditional branch. That is, maybe the preprocessing/transformations performed by KLEE are replacing the last three instructions of main with "ret not(%equal)". I'm not certain that this is what's happening but the klee-last/assembly.ll file shows you what KLEE actually executes so it should be easy to check. -- Alastair On Mon, May 31, 2021 at 9:27 PM Manuel Carrasco <[email protected]<mailto:[email protected]>> wrote: 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 [email protected]<mailto:[email protected]> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev _______________________________________________ klee-dev mailing list [email protected]<mailto:[email protected]> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
