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
