I tried out using seeds, but haven't found any real value out of it. My initial thought was that using seeds might be able to make Klee explore some paths in a new session that were not explored before (in previous Klee sessions), but I didn't seem to find any progress after several trials using seeds. Using seeds makes Klee dump the path constraints of each state. My thought was that those saved constraints are probably used to guide Klee not to repeat those paths again or do something different, but it doesn't seem to be the case.
I think that I was wrong in assuming that using seeds can make Klee explore more paths. I found the following description at line 148 in Executor.h: /// When non-empty the Executor is running in "seed" mode. The /// states in this map will be executed in an arbitrary order /// (outside the normal search interface) until they terminate. When /// the states reach a symbolic branch then either direction that /// satisfies one or more seeds will be added to this map. What /// happens with other states (that don't satisfy the seeds) depends /// on as-yet-to-be-determined flags. This makes me unable to understand what the real value seeds have. It seems that the only difference with seeds is that Klee uses an "arbitrary scheduling" which is not controlled through the search interface. What is this supposed to give us? I either missed something very important to seeds, or seeds are just a very premature concept that has not been played well in Klee? I can imagine that replay might need seeds, but I have no idea how replay is actually done in Klee, and I think there are other simpler ways to implement replay than using seeds. Please help me more in understanding seeds. Thanks. Lu On 08/03/2011 04:37 PM, Paul Marinescu wrote: > You can provide seeds with the --seed-out=<list of ktest files> and --seed-out-dir=<list of dirs containing ktest files> options. For more seed-related options see klee --help | grep seed > > Paul > > On 4 Aug 2011, at 00:28, Lu Zhao wrote: > >> Does that means that I can save a tree that Klee executes in a session >> and resume execution from that tree in next session? What are the APIs >> that implement this? More specifically, how to provide a seed to Klee? >> >> Hi Paul, I'm sorry if my previous email went out and reached your >> mailbox. I cancelled the sending when I noticed that I didn't sent to >> the list. >> >> Thanks. >> Lu >> >> On 07/13/2011 02:59 PM, Paul Marinescu wrote: >>> t (i.e., no seeds), KLEE starts with a tree that has only one node, the program entry point, and explores from there. A seed is essentially a tree that you can provide as the starting point for the explorat >> _______________________________________________ >> klee-dev mailing list >> [email protected] >> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev On 08/03/2011 04:37 PM, Paul Marinescu wrote: > You can provide seeds with the --seed-out=<list of ktest files> and > --seed-out-dir=<list of dirs containing ktest files> options. For more > seed-related options see klee --help | grep seed > > Paul > > On 4 Aug 2011, at 00:28, Lu Zhao wrote: > >> Does that means that I can save a tree that Klee executes in a session >> and resume execution from that tree in next session? What are the APIs >> that implement this? More specifically, how to provide a seed to Klee? >> >> Hi Paul, I'm sorry if my previous email went out and reached your >> mailbox. I cancelled the sending when I noticed that I didn't sent to >> the list. >> >> Thanks. >> Lu >> >> On 07/13/2011 02:59 PM, Paul Marinescu wrote: >>> t (i.e., no seeds), KLEE starts with a tree that has only one node, the >>> program entry point, and explores from there. A seed is essentially a tree >>> that you can provide as the starting point for the explorat >> _______________________________________________ >> klee-dev mailing list >> [email protected] >> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev _______________________________________________ klee-dev mailing list [email protected] http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
