Hi John, It's possible your -77 offset is landing in-bounds in another allocated buffer. Since the standard version of KLEE doesn't track referents (that is, which buffer a particular pointer SHOULD reference), it doesn't know the difference between an in-bounds access in the correct buffer from an in-bounds access in a different buffer. We have an internal version with this functionality, but it would be difficult to port back to the open source version.
When KLEE hits an array dereference at a symbolic offset (storage[index]), it tries to resolve that symbolic address into every allocated buffer in the current state. If it's possible for the offset to lie outside all of these objects (given the arbitrary concrete addresses on a particular execution), then KLEE will report the error. If all feasible indices will land the pointer inside of valid buffers, then there's no error for KLEE to report. You might want to try values other than -77, running KLEE multiple times, enabling ASLR, etc. to confirm the transient nature of this type of error. -David ----- Original Message ----- From: "John Regehr" <[email protected]> To: "Ott Tinn" <[email protected]> Cc: [email protected] Sent: Tuesday, January 24, 2012 2:16:49 PM Subject: Re: [klee-dev] blog post and a question 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
