I should have been a little more specific. For loads, the issue only occurs
when you're reading a symbolic object at a symbolic offset. For stores, it
happens for both concrete and symbolic objects at symbolic offsets.
Simple illustrative example:
int x[] = {0, 1, 2, 3, 4, 5};
int y;
klee_make_symbolic(&y, sizeof(y), "y");
x[y] = -1;
int z = x[0];
The variable 'z' could hold values 0 or -1, depending on 'y'. KLEE represents
this internally by using a Read expression with an update list showing the
write of -1 at symbolic offset 'y'.
In your initial example, the object was huge, and KLEE had to flush 162KB of
writes into an update list. Looking at the backtrace you reported, the actual
crash occurred while trying to query STP. Without a more complete backtrace, I
don't know if the crash happened while executing the same instruction that
performed the symoffset read, or a subsequent instruction.
> So when I set the pointer to that symbolic offset, it generates an
> expression of all possible pointers pointing to possible datastructs.
To be precise, it's all possible 8-byte reads within a single memory object.
> Then when i dereference it, one of the symbolic offsets reads is invalid
> and crashes and/or there are too many possibilities?
It crashes while generating an STP query... probably due overflowing a buffer
or the stack.
> Would putting
> bounds checks on the pointer after assigning it help to limit the number
> of possible reads?
> Maybe asserting it to make sure any possible read is
> inbounds? That would maybe weed out uneccesary possibilities?
Probably not. It would certainly limit the range of feasible values, but only
STP reasons about that, and the crash occurs before getting to STP. Your two
options are to (1) make the object much smaller, or to (2) make KLEE fork and
concretize each possible offset.
For my above example, you could do this with something like:
unsigned i;
for (i = 0; i < 6; i++) {
if (y == i)
x[y] = -1;
}
KLEE will fork a new state at the if-statement during each iteration, and then
the read will be at a concrete offset. Make sure to use the
--simplify-sym-indices option or KLEE might still create an update list.
-David
_______________________________________________
klee-dev mailing list
klee-dev@keeda.stanford.edu
http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
