[klee-dev] Klee Dump States Question

Tue Jan 20 19:24:35 GMT 2015

Yes, I believe that code could be optimised in this way, but the 
independence solver is usually very fast.  But please let us know if you 
see any cases in which it takes significant time.

Best,
Cristian

On 19/01/15 22:57, eric.rizzi at huskers.unl.edu wrote:
> 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
>
> _______________________________________________ klee-dev mailing
> list klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>