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, [email protected] 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:
[email protected] <[email protected]> on
behalf of Cristian Cadar <[email protected]> Sent: Sunday,
January 18, 2015 4:04 PM To: [email protected] 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, [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
_______________________________________________ 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
