[klee-dev] Klee Dump States Question

[eric.rizzi at huskers.unl.edu]

I think I understand how it works now.  I have, however, dug a bit more into the code and I have one more question.

In the "Independent Solver" it seems that the reads involved in a particular Expression are recalculated over and over again (in the form of an IndependentElementSet).  

1) Is this correct?
2) Why wouldn't the information cached in some way to prevent iterating over the expression with every new query?  Or perhaps it's not as expensive as I'm imagining...

Thanks,
Eric Rizzi

________________________________________
From: klee-dev-bounces at imperial.ac.uk <klee-dev-bounces at imperial.ac.uk> on behalf of Cristian Cadar <c.cadar at imperial.ac.uk>
Sent: Sunday, January 18, 2015 4:04 PM
To: klee-dev at imperial.ac.uk
Subject: Re: [klee-dev] Klee Dump States Question

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
>

_______________________________________________
klee-dev mailing list
klee-dev at imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev