Hi David,
I tried a bunch of random offsets and wasn't able to get a failure. Not
sure how this squares with Raimondas's report, but perhaps I should use
the latest source instead of the self-contained executable version.
My program is here in case that's useful:
http://www.cs.utah.edu/~regehr/val.c
John
On Tue, 24 Jan 2012, David Antonio Ramos wrote:
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
