Hey Phil, I think the basic insight you are missing is that many things are lazily translated to STP (as part of lib/util/STPBuilder). Most of these things are not cached, but the update lists are, so that we do not constantly rebuild large update lists. The actual STP array which backs a MemoryObject, for example, is constructed and cached in STPBuilder::getInitialArray.
Another notable detail is that the STP construction is done in the main process, whereas the query itself is run in a separate process by default (--use-forked-stp). The key point here is that the construction is done before the fork so that the cached values are actually used. The main reason for this design is that I wanted klee's Solver interface to be separate from STP; I would like to experiment with plugging other constraint solvers in as Solver backends. This isn't exactly feasible at the moment, but it is quite close. The other reason is to work around design flaws in STP's public API which mean that one must tread very carefully in order to make sure everything is free'd properly (which is important). More details inline: On Tue, Dec 16, 2008 at 7:06 PM, Philip Guo <pg at cs.stanford.edu> wrote: > Hi guys, > > I'm trying to experiment with how Klee uses STP, so I started by digging > through the code, and now I have some questions. Here's my current > impression of how Klee interacts with the STP c_interface API: > > // execution begins > VC vc = vc_createValidityChecker() > > // ??? presumably some objects are made symbolic here ??? A symbolic value just corresponds to an STP array. These are lazily constructed whenever a ReadExpr is "constructed" (sent to STP). > // During execution, Klee builds up constraints in its own Expr data > // structures and keeps them along with each state as its path condition Yup. > // execute one STP query: > at each branch (or other place where STP is called): > vc_push(vc) > > for c in current_state.constraints: > vc_assertFormula(vc, c) Almost. The missing part is a call to builder->construct to turn the klee::Expr c into an STP expression. > res = vc_query(vc, FALSE) > > // find concrete counterexample if query unsat.: > if res == UNSATISFIABLE: > for object in symbolic objects: > object.concrete_value = vc_getCounterExample(vc, object) Yup. Although you got the sense of unsatisfiable backwards, a satisfiable query has a counterexample, an unsatisfiable query has no counterexample, i.e., it is provably false. > vc_pop(vc) > > > // execution ends > vc_Destroy(vc) > > --- > I have the following questions: > - what's the effect on STP of making a value symbolic from within > Klee? If I make, say, a 10-byte array symbolic, what does that > translate to in STP? I presume a variable declaration, right? What > API call does this? There is no effect, this is all done lazily (unlike what EXE/FT did). > - i noticed that if i do a simple klee_make_symbolic_name(), even with > a sensible name: > > char x; > klee_make_symbolic_name(&x, sizeof(x), "input"); > > the .cvc file still prints out that variable with a > garbled name like: > > arr149 : ARRAY BITVECTOR(32) OF BITVECTOR(8); - > - first, is there a way to make these names friendlier than arr149 > (or to get the names in some deterministic manner) Yes to the first part of this question. Just modify STPBuilder::getInitialArray. I think the only key feature here is that the names need to be distinct. To be honest I have forgotten if STP actually requires them to be distinct, or I just wanted them to be distinct so we were guaranteed to be able to read the CVC back in. I would like to kill off the id field anyway; just keeping a map on the side of (names -> unsigned) which we bump each time we use a name would be fine I think. As to getting the names in a deterministic way, there isn't an easy one depending on how much determinism you want. Deriving the name from the user provided name and allocation site would be fairly deterministic, but if you unique these names with id's then that could still change depending on the order that things are made symbolic (and shipped to the constraint solver, where the actual array is created). The path to the allocation site would be deterministic, but hard to encode into a name and probably quite verbose (and still not technically guaranteed to be unique). > - second, why is this variable a ARRAY BITVECTOR(32) OF > BITVECTOR(8)? I can understand making it BITVECTOR(8) since > it's a 'char' variable, but why ARRAY BITVECTOR(32)? This is the domain and range of the array (the new Expr language Cristi and I are working on will have the same concept). klee always thinks of arrays as being indexed by 32-bit values but (a) this is flawed in a 64-bit world, and (b) STP is more general. > - if there is only one global vc object that persists throughout > execution, how does its state 'reset' between queries? is that what > vc_push() and vc_pop() does? vc_push and vc_pop reset the asserted constraints (and the counterexample, which ends up modifying other parts of STP state), yes. > - is my mental model missing something significant about how Klee uses > STP? are there important functions I'm ignoring? The role of STPBuilder. > Thanks in advance for your patience with my n00b questions :) No problem, fire away! - Daniel
