[klee-dev] Some questions about SMT solvers

[Andrew Santosa]

Hi Fabrizio,
1. Your example is missing from your email, but I think validity in KLEE means that any valuation is a model (as in model theory). Whereas it seems your understanding of validity (some valuations are models) is more commonly known as satisfiability.2. I don't recall ever seeing KLEE extracts more information from the solver other than satisfiability decision. Perhaps others would know more.3. I prefer more comments in the code rather than separate documentation. 
Regards,Andrew

    On Friday, 15 April 2016, 20:53, Fabrizio Biondi <fabrizio.biondi at inria.fr> wrote:
 

 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

_______________________________________________
klee-dev mailing list
klee-dev at imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev


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