Thanks a lot. I am going to move forward taking into account your suggestions.
Kind regards, Manuel On 2/6/21 21:39, Nowack, Martin wrote: > 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 > <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 >>> <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
