On Sat, Mar 6, 2010 at 3:38 PM, Chung-chieh Shan <ccshan at rutgers.edu> wrote: > Hello, > > I just enjoyed the OSDI 2008 paper about KLEE. ?I hope this list is a good > place to ask questions about it!
Sure! > Footnote 9 caught my attention because it suggests that the way KLEE lays out > its state representations in memory affects the results of the run. ?But if I > write code like > ? assert((int)(malloc(1)) % 3); > then shouldn't KLEE deterministically generate a test case that is triggered > by unfortunate behavior of malloc in the C runtime? ?Or is the goal of KLEE > only to find bugs that can be reliably triggered? KLEE doesn't try to control the results of malloc. This isn't an inherent flaw, it just requires some work to fix it. Currently there are two main limitations: (1) KLEE doesn't use a deterministic assignment of address for malloc. This is unfortunate for replaying test cases that depend on the actual address of a malloc call (hash tables on pointers, for example). Fixing this just requires implementing a custom allocator in KLEE which assigns deterministic address, and providing a native implementation to override the system malloc. Another approach would be to actually compile in the native system version of malloc and use that directly, and implement low level primitives like sbrk(). (2) KLEE doesn't attempt to model the result of malloc as being symbolic. This is a harder problem to solve, and I'm not sure of its utility in practice. However, there is one pro of the current approach, which is that because the states share the same memory addresses as the host process, it is possible to transparently pass pointers to memory to external functions (i.e., native code). > A broader question is about how KLEE explores its search space of states. ?It > seems that states only fork (on branches), never rejoin. ?Might it be > profitable to identify states that are equivalent and merge them (so the > search space is a DAG rather than tree)? ?Or is it pretty clear that the cost > of merging states outweighs the benefits? Yes, KLEE as described in the OSDI paper only forks. And yes, it can be very very profitable to merge states, and the repository contains some basic functionality for experimenting with this. It is relatively cheap to (precisely) merge two states whose heaps haven't diverged, but there are a number of non-trivial problems: (1) How to decide when to merge states? (2) What to do with states whose heaps have diverged? This is hard to solve given the current memory model in KLEE. Solving it is possible, but then impacts performance in other areas. (3) What is the impact of merging states on the constraint solver? In general merging states is going to introduce disjunctions, which lead to more expensive queries. It will often be a win since the disjunctions can be simplified, but it may sometimes be a loss. All in all, there is lots of potential for merging and it is a good direction for future work, but definitely a research project. An interesting approach is to do something like "speculative merging", as in: http://www.doc.ic.ac.uk/~cristic/papers/exe-rwset-tacas-08.pdf - Daniel > Thanks for any comments! ?(I am not subscribed to the list - please let me > know if I should be.) > _______________________________________________ > klee-dev mailing list > klee-dev at keeda.stanford.edu > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev > >
