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 ???
// During execution, Klee builds up constraints in its own Expr data
// structures and keeps them along with each state as its path condition
// 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)
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)
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?
- 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)
- 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)?
- 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?
- is my mental model missing something significant about how Klee uses
STP? are there important functions I'm ignoring?
Thanks in advance for your patience with my n00b questions :)
Philip
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20081216/e532504f/attachment.html
