Ah ha! Thanks! I was looking at the llvm-dis output not the assembly.ll. The ordering in the assembly.ll is indeed what is being executed. I tried --disable-opt when running klee but it didn't seem to restore the original ordering scheme. Any other ideas?
Neha On Mon, Feb 13, 2012 at 3:51 PM, David A. Ramos <[email protected]>wrote: > 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/ > -------------------------------------------------- > > -- ------------------------------------------------- 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
