[klee-dev] Klee Dump States Question

[eric.rizzi at huskers.unl.edu]

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


-------------- next part --------------
HTML attachment scrubbed and removed