[klee-dev] Some questions about SMT solvers

[Cristian Cadar]

On 17/04/2016 02:35, Andrew Santosa wrote:
> 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.
Indeed, that' correct.

> 2. I don't recall ever seeing KLEE extracts more information from the
> solver other than satisfiability decision. Perhaps others would know more.
KLEE does several constraint simplification and optimisation passes, but 
does not extract any information from the solver other than 
satisfiability/validity results and solutions/counterexamples.

> 3. I prefer more comments in the code rather than separate documentation.
I think it depends on the type of documentation.  I agree that in many 
cases, it makes sense to just add comments in the code, which can also 
be displayed in HTML form via doxygen.  However, I would welcome a 
tutorial-style separate document on how to add a new solver to the chain.

Best,
Cristian

>
> 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 <mailto:klee-dev at imperial.ac.uk>
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>