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