reads and writes, so the code sequence
--
a[i] = 10;
a[0] = 2;
x = a[j]
--
would translate to something like Read(Write(Write(a, i, 10), 0, 2),
j). STP has various tricks to try and make the solving of such
expressions more efficient, but in general these expressions are
expensive (they transform to many nested if-then-elses). Especially
when there are many writes to an array.
In klee terms, arrays are modified using UpdateLists, which is just an
ordered (index,value) pair representing modifications to the array.
Reads are ReadExpr's referencing an array (UpdateList) and an index.
klee lazily builds STP arrays when these ReadExprs appear in a
constraint being solved.
In order to make array access more efficient, klee implements a
"concrete" cache for object values which are known to be constant.
When a constant value is written to an object, klee caches that value
directly and uses it to satisfy any subsequent reads. Additionally,
klee delays adding the write to the object's UpdateList. Instead, klee
just sets a bit marking this index in the object as dirty. The write
to the array is only "flushed" to the UpdateList when klee ends up
constructing an expression which uses the UpdateList.
As an additional optimization, when klee flushes on reads it does not
actually need to clear the concrete cache (the read does not
invalidate the cache). Instead it just keeps track of what data needs
to be flushed, but still keeps the cache around to satisfy subsequent
reads at concrete indices. Finally, in terms of the actual
implementation there are some other small tricks to avoid doing any
extra allocations to keep track of the masks for the common case of
objects which are never accessed symbolically.
As an example, consider the following code:
---
// a maps to some STP array "arr1", and has a 4-byte concrete cache
and with 4 bits indicating if the cache is in use.
char a[4]; // cache: {undef, undef, undef, undef}, concrete mask:
{false, false, false, false}, update list: []
a[0] = 10; // cache: {10, undef, undef, undef}, concrete mask: {true,
false, false, false}, update list: []
/* assuming i is symbolic, this triggers a flush of the previous
concrete write. however, it is only a read, so the cache is preserved.
*/
int x = a[i]; // cache: {10, undef, undef, undef}, concrete mask:
{true, false, false, false}, update list: [(0, 10)]
int y = a[0]; // this will hit the cache
a[1] = 2; // cache: {10, 2, undef, undef}, concrete mask: {true,
true, false, false}, update list: [(0, 10)]
/* assuming j is symbolic, this triggers a flush of the previous
concrete write (a[0] = 10 was already flushed, this is tracked in a
separate bitmask. additionally, this is a write so we can no longer
preserve the concrete cache. */
a[j] = 10; // cache: {undef, undef, undef, undef}, concrete mask:
{false, false, false, false} [(0, 10), (1, 2)]
--
Does that make sense/help?
Unfortunately, making symbolic access to large buffers efficient is
difficult (although very worthwhile). An effective solution to this
problem is probably going to require a number of optimizations in klee
and STP. I'm reaching my single-email-length limit, but here are some
ideas about what can be done:
1. I would like to extend the UpdateList data structure to be more
abstract so that it is possible to have multiple implementations. In
particular, it would be very useful for the UpdateList to keep track
of basic aliasing relations so that writes which are clearly
overwritten by a subsequent value can be discarded. This is
conceptually simple, the main trick is playing well with the
immutability and lazy interaction with STP.
2. When indexing by a symbolic value, we should do some simple range
analysis of the index expression. This will succeed in many common
cases and can be used to bound the values which must be flushed to
STP. Done right, I expect this to be very effective -- intuitively
most pointers will be constrained to be in bounds of some small array
contained in the larger object and we should only need to flush the
contents of the smaller array.
3. In conjunction with (1), many times two indices can be proven to be
distinct quite simply. For example, x*4 + 1 is trivially not equal to
y*4 + 2. We can exploit this information to avoid flushing values.
4. I suspect that there is room for improvement in STP's abstraction
refinement for arrays. Implementing the array refinement in klee
itself could potentially offer significant improvements in constraint
solving time. In fact, this is almost necessary as STP uses a number
of recursive algorithms on arrays and this is simply not scalable when
considering large arrays. We will have to fix STP or move array
handling to klee to truly solve this.
Sorry for the delayed reply, but I hope this helps.
- Daniel
> Thanks for your help,
> Vitaly C.
> _______________________________________________
> klee-dev mailing list
> klee-dev at keeda.Stanford.EDU
> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
>
