Hi Neha, Is that the assemble shown in klee-out/assembly.ll? If not, the LLVM optimization passes that KLEE runs on startup are probably reordering the instructions. Try running without --optimize to disable this.
-David Sent from my iPhone On Feb 13, 2012, at 3:42 PM, Neha Rungta <[email protected]> wrote: > Hi, > I am running the following bit of code in klee > > if((x + (y + z)) == 0) { > x = (y+z); > } else { > x = (y-z); > } > > The corresponding disassembled bitcode is as follows: > > %4 = add nsw i32 %2, %3, !dbg !31 > %5 = icmp eq i32 %4, 0, !dbg !31 > br i1 %5, label %bb, label %bb1, !dbg !31 > > bb: ; preds = %entry > %6 = load i32* %y_addr, align 4, !dbg !40 > %7 = load i32* %z_addr, align 4, !dbg !40 > %8 = add nsw i32 %6, %7, !dbg !40 > store i32 %8, i32* %x_addr, align 4, !dbg !40 > br label %bb2, !dbg !40 > > bb1: ; preds = %entry > %9 = load i32* %y_addr, align 4, !dbg !46 > %10 = load i32* %z_addr, align 4, !dbg !46 > %11 = sub nsw i32 %9, %10, !dbg !46 > > The sequence of instructions executed by klee is > > cmp --> %6 = load --> %7 load --> br, %8 ... > > When the search eventually backtracks to explore the other choice at the > branch location the other choice starts from %11. I was unable to observe the > execution of %9 and %10. These instructions, however, are loading the values > of %y and %z the same as the ones in %4, and %5. I changed the load values in > the other blocks to see if I could then observe the execution of those > instructions, and I was able to do so. This leads me to believe that Klee is > somewhere caching the information that loads in one target basic block are > the same as the other. Is that the case? Is it pssible to turn it off? Or is > there a way to detect on the fly when such caching happens? Also, why is the > target basic block instruction followed by the cmp, and not the conditional > branch instruction itself? > > Thanks, > Neha > > -- > ------------------------------------------------- > Neha Rungta, Ph.D > SGT/NASA Ames Research Center > http://ti.arc.nasa.gov/profile/nrungta/ > --------------------------------------------------
_______________________________________________ klee-dev mailing list [email protected] http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
