Hi, I am integrating Klee to QEMU to be able to symbolically execute x86 applications (especially device drivers). 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). 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.
Thanks for your help, Vitaly C.
