Hi Vitaly, On Thu, Feb 19, 2009 at 6:03 AM, Vitaly Chipounov <vitaly.chipounov at epfl.ch> wrote: > I am integrating Klee to QEMU to be able to symbolically execute x86 > applications (especially device drivers).
Cool! I assume you are aware of the LLVM project to integrate the LLVM JIT with QEMU? (Part of Google Summer of Code, don't have a link handy). > I treat the physical memory as a MemoryObject. To avoid exhausting > memory on forks I implemented a sparse ObjectState class, which avoids > copying the whole concrete memory buffer (which can be a hundred MB > large, size of emulated physical memory), since most of its content is > never modified (and only a few hundred bytes are symbolic in my > application). Very cool. Would you be in interested in contributing it back? This is something we definitely will need in klee proper. > So far it works well, however I get in troubles when dealing with > symbolic memory offsets (like switches / jump tables). I saw that the > ObjectState class maintains an update list which is extended with the > content of the whole object and some warnings saying "flushing %d bytes > on read, may be slow and/or crash". I would like to have some hints > about how the update lists/flushing work to implement something more > efficient for my need. Ok. Let me start by describing what is currently being done (and why): klee represents C objects (contiguous regions of memory) using a single STP "array". An STP "array" is merely an abstraction which allows symbolic access to bitvectors; STP arrays are unsized (although the index bitwidth is fixed, so in practice they are bounded by 2^32).
