[klee-dev] Klee Dump States Question

[Cristian Cadar]

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, eric.rizzi at huskers.unl.edu 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:* markrtuttle at gmail.com <markrtuttle at gmail.com> on behalf of Mark
> R. Tuttle <mrtuttle at alum.mit.edu>
> *Sent:* Friday, January 16, 2015 1:59 PM
> *To:* eric.rizzi at huskers.unl.edu
> *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, eric.rizzi at huskers.unl.edu
> <mailto:eric.rizzi at huskers.unl.edu> <eric.rizzi at huskers.unl.edu
> <mailto:eric.rizzi at huskers.unl.edu>> 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
>     klee-dev at imperial.ac.uk <mailto:klee-dev at imperial.ac.uk>
>     https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
> 
> 
> 
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>