Hi Stefan, On Wed, Mar 10, 2010 at 4:08 PM, Stefan Bucur <stefan.bucur at epfl.ch> wrote: > 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.]
The file system model is entirely in user code (except for the syscalls it makes), so it is always going to be per-state. > 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. It depends on what kind of replay you are doing, are you talking about the replay-path feature? Or the seeding feature? I have to be honest and admit I don't remember whether there are any known issues with internal forks. From looking at the code, I would expect it to work, because all forking in KLEE is built around the Executor::fork() call, which is where both features are implemented. As long as whatever code forks ends up adding something to the path condition that guarantees it will follow that path, then seeding would be constrained on re-execution, and would not be able to take a different fork. If you find problems, its probably worth filing just so its noted somewhere. - Daniel > Thanks, > Stefan > _______________________________________________ > klee-dev mailing list > klee-dev at keeda.stanford.edu > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev >
