[klee-dev] Some questions about SMT solvers

[Fabrizio Biondi]

Hi all, 

I have been tinkering with KLEE's SMT solver chain, and I have a few doubts some of you may find the time to address. 

1) I have noticed that computeValidity returns 0 (Unknown) a lot. This is an example: 

Since in the example above there is no constraint on word number 6 and the query is on word number 6, I would expect the solver to return 1 (True), meaning that there exists a model satisfying the query under the constraints. Is my understanding of what 'validity' and 'invalid' mean wrong? 

2) I have noticed that KLEE does not simplify SMT statements much, I guess this is because it expects the underlying SMT solver (STP or Z3) to take care of the simplification. However, is the simplified version of the constraints obtained from the solver and used in the rest of the symbolic execution? 

Allow me to elaborate. I have some large set of constraints C, and I query the solver for e.g. its validity. The solver internally simplifies C to a smaller set C', computes its validity, and answers. Does KLEE henceforth use C' as its set of constraints for that trace, or does it use C? 

3) After studying the code a little, I think I have a very clear idea of which files are to be modified and how to add a solver to the solver chain. Would it be useful if I wrote a small guide on how to do this? 

Let me add that KLEE is a beautifully written and structured software project, and studying it is very educational. Still, I think it would benefit from some more extensive documentation. 

Thank you and best regards, 
Fabrizio 

Fabrizio Biondi , Ph. D. 
Post-doctoral researcher 
TAMIS research group 
INRIA/IRISA Rennes 

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