Greetings, I was experimenting with Klee and tried to set up the following scenario: one Klee instance executes a portion of the symbolic tree, then another Klee instance picks up paths from the first instance and resumes exploration having those paths as seeds. The second instance would perform a replay (basically, start from root, and select states to explore only along the seed paths), before resuming execution.
This approach seems to work in general. However, there are cases when the seeds replay on the second Klee instance is broken, which means that the original path could not be totally reproduced on the second instance. I tracked down the problem and found that the replay is broken (at least) in the runtime/POSIX/fd.c:903 point, in the ioctl() function, after executing a syscall. Moreover, the code that calls ioctl() is _stdio_init(), in klee-uclibc, when getting information about standard file descriptors 0 and 1. Regarding this issue, I have two questions: 1) Does the file system model keep track of each symbolic state individually? In other words, does one symbolic state depend on the previous execution of other symbolic states? [It shouldn't be so, in my opinion, but that would be an explanation for getting a different behavior depending on state exploration history.] 2) How does the replay code in Klee deal with internal forks? My replay code replays every fork, be it external or internal, but as far as I studied Executor.cpp, the replay feature in Klee deals only with external forks. If there are multiple paths stemming from an internal fork, how does Klee know which one to pick during replay? This is something which I didn't find obvious from studying the source code. Thanks, Stefan
