Hi Eric, Mark's answer was basically right: when the timeout is exceeded, any state/path which hasn't finished generates a test case. That is, its current path constraints are solved to generate a concrete test case, which is written into a .ktest file.
I'm not sure what you mean by a "path" when you say that a particular path generates 20 new queries, but give us more details if things are still unclear. Best, Cristian On 16/01/2015 19:26, [email protected] wrote: > Thanks Mark, I'm glad to hear UNL'ers never give up on their Klee quests. > > > I completely forgot to include the following observation I made: > > > I modified Klee so that the path that led to a state that generates a > particular query is included in the header information sent to the > solver. I did this for two reasons > > > 1) I was interested in tracking which queries were associated with a > particular path though the states. > > 2) I wanted to see whether it was true that Klee just solved all of the > states remaining in the queue. > > > It turns out that Klee generates up to 20 new queries along a particular > path after the timeout. Are these 20 queries just part of solving this > final state? Why wouldn't Klee just bundle all of them into a single > query and rely on the solver chain to handle it? > > > Finally, after some quick parsing, it seems like there is a lot of > repetition in these "finalizing queries." Why wouldn't Klee just create > a single query that encodes ALL of the information required to pass > through that particular state and leave it at that. > > > ------------------------------------------------------------------------ > *From:* [email protected] <[email protected]> on behalf of Mark > R. Tuttle <[email protected]> > *Sent:* Friday, January 16, 2015 1:59 PM > *To:* [email protected] > *Subject:* Re: [klee-dev] Klee Dump States Question > > Hi, Eric. > > I was an undergraduate student at Nebraska computer science... > > The pros will answer you more exactly, but here is what I think is going > on. KLEE maintains a work queue of symbolic states. Each state > represents a collection of constraints on the inputs (the symbolic > values) that will cause the code to reach a given branch branch. Klee > takes a symbolic state off the work queue, executes symbolically until > the next branch, and then splits the state into two, one for each > outcome of the branch. So when your timer goes off, KLEE stops doing > symbolic execution and starts dumping states. But each state on the > work queue is just a set of constraints, and KLEE has to send each set > of constraints to the constraint solver to get a concrete representation > to dump. > > Mark > > > On Fri, Jan 16, 2015 at 12:25 PM, [email protected] > <mailto:[email protected]> <[email protected] > <mailto:[email protected]>> wrote: > > Hello, > > I have been working with Klee for the past few weeks and I have a > question related to what happens when Klee reaches it’s timeout > (-max-time) and dumps it’s states. > > It seems that this “wrapping up” period requires significant time, > often exceeding the initial timeout. In addition, when examining > the output sent to the solver, the number of queries being generated > is significantly higher after the timeout than before. > > My question is, why is this happening? It seems that upon wrapping > up, the states on the edge of the exploration should be solved for, > creating one test that will pass through each of these states. My > intuition, however, is clearly wrong. > > In case it helps, I used the following command line to run Klee > > % klee --libc=uclibc --posix-runtime --use-query-log=solver:smt2 > --max-time=1000 program.bc --sym-args 1 3 12 --sym-files 2 100 > > Thanks, > Eric Rizzi > > > _______________________________________________ > klee-dev mailing list > [email protected] <mailto:[email protected]> > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > > > > > _______________________________________________ > klee-dev mailing list > [email protected] > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
