Ok, thanks Christian and Ott! I was assuming that Klee's --optimize flag caused it use some enhanced search procedure or something and didn't realize this invoked the LLVM optimizers. I get the error now that the rest of you see.
Klee is a great tool, I was totally impressed that it inverted a small checksum computation. John -- John Regehr, [email protected] Associate Professor, School of Computing, University of Utah http://www.cs.utah.edu/~regehr/ On Wed, 25 Jan 2012, Cristian Cadar wrote: > Yes, I see the same behavior on my machine: KLEE finds the bug in unoptimized > mode, but does not find it with --optimize because that access is eliminated > by LLVM's optimizations. John, it would be interesting to look into > klee-last/assembly.ll to see if something more interesting is going on there. > > Cristian > > On 01/25/2012 09:53 AM, Ott Tinn wrote: >> Hi John, >> >> In this case the linkage of "storage" keeps it from being optimized >> away during the initial compilation but afterwards KLEE's optimization >> pass will internalize it anyway and then run the other optimizations. >> Thus at least on my machine the program that ends up being >> symbolically executed when -optimize is used is the following: >> >> define i32 @main(i32 %argc, i8** nocapture %argv) nounwind { >> entry: >> %i = alloca i32, align 4 >> %i1 = bitcast i32* %i to i8* >> call void @klee_make_symbolic(i8* %i1, i32 4, i8* getelementptr >> inbounds ([2 x i8]* @.str, i32 0, i32 0)) nounwind >> ret i32 0 >> } >> >> If the internalization is skipped by not using -optimize or >> specifically using -disable-internalize then the bug could be found. >> You can confirm the final code by looking at the assembly.ll file in >> the klee-out-N directory. If you didn't use KLEE's optimization pass >> at all then this is could be something more interesting as David >> suggested. >> >> Ott >> >> On Tue, Jan 24, 2012 at 10:16 PM, John Regehr<[email protected]> wrote: >>> Hi Ott, >>> >>> I'm pretty sure optimizations are not the problem. >>> >>> First, "storage" has external linkage -- the compiler cannot infer that it >>> is not subsequently used. >>> >>> Second, llvm-gcc's output for this code (even with optimizations turned >>> on) >>> is a pretty obvious translation of the C code. >>> >>> John >>> >>> >>> >>> On Tue, 24 Jan 2012, Ott Tinn wrote: >>> >>>> Hi John, >>>> >>>> The most obvious problem I see is that the code sample is too simple - >>>> the compiler optimizations could also see that the value you are >>>> storing to the storage array is never used. Since accessing array >>>> elements that are out of bounds is undefined in C then the compiler >>>> can optimize this away by assuming that it isn't out of bounds. To >>>> make this example work you could try compiling without any >>>> optimizations and without using KLEE's -optimize flag or otherwise >>>> making sure the dangerous operations can't be optimized away. >>>> >>>> Ott >>>> >>>> On Tue, Jan 24, 2012 at 9:18 PM, John Regehr<[email protected]> wrote: >>>>> >>>>> Perhaps interesting to people here: >>>>> >>>>> http://blog.regehr.org/archives/672 >>>>> >>>>> While writing this up I discovered that when "i" is symbolic Klee cannot >>>>> find a value for i that makes this code access an OOB array element: >>>>> >>>>> int indices[] = { 0,2,1,5,3,0,-77,0,3,6 }; >>>>> >>>>> value_t storage[7]; >>>>> >>>>> void stash (int i, value_t v) >>>>> { >>>>> if (i<0 || i>=10) { >>>>> error(); >>>>> } else { >>>>> int index = indices[i]; >>>>> // assert (index>=0); >>>>> // assert (index<7); >>>>> storage[index] = v; >>>>> } >>>>> } >>>>> >>>>> On the other hand, given the assertions, Klee generates the test case >>>>> where >>>>> i==6. >>>>> >>>>> I infer that Klee does not automatically assert in-boundedness of array >>>>> accesses. But these assertions seem obviously desirable, so I'm trying >>>>> to >>>>> figure out why not. Maybe Klee doesn't have enough runtime information >>>>> to >>>>> make this happen? >>>>> >>>>> John >>>>> _______________________________________________ >>>>> klee-dev mailing list >>>>> [email protected] >>>>> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev >> _______________________________________________ >> klee-dev mailing list >> [email protected] >> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev > _______________________________________________ klee-dev mailing list [email protected] http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
