There is another call to the CFGSimplification Pass in the KModule class that does not get disabled by the -disable-opt flag. Turning that off fixed my problem.
Neha On Mon, Feb 13, 2012 at 4:16 PM, Neha Rungta <[email protected]> wrote: > 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/ > -------------------------------------------------- > -- ------------------------------------------------- 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
