[klee-dev] Some questions about SMT solvers

[Dan Liew]

Hi Fabrizio,

On 15 April 2016 at 13:10, 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:

Your example is missing from the e-mail.

> 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?

Yes your understanding is incorrect here.

See the comments on the ``computeValidity(...)`` method [1].

You are confusing validity and satisfiability which are two different
but related concepts. Validity is in general concerned with some
formula being true for all possible variable substitutions whereas
satisfiability is in general concerned with some formula being true
for at least one variable substitution.

In KLEE a ``Query`` object is made up of a "query expression" and a
set of constraints.

The ``computeValidity()`` method computes the value of

∀ X : C(X) → Q(X)

which is either true (valid) or false (invalid). Here X is a set of
free variables, C is the set of constraints conjuncted that may use
the free variables and Q is the "query expression" which may use the
free variables.

This is equivalent to

¬ ∃ X : C(X) ∧ ¬ Q(X)

> 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?

Ideally KLEE should simplify expressions as much as possible to try to
avoid expressions from growing large as execution continues.
We assume that the underlying SMT solver can do some simplification
but currently for Z3 we are missing an opportunity to do further
simplificiation
because Z3 exposes an API (Z3_simplify()) which we aren't currently using.

See [2]. I think it would be useful to investigate doing this.

> 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?

KLEE continues to use C. Even so are you assuming that C' and C are
equivalent or equisatisifiable?
The SMT solver and KLEE are currently decoupled from each other so
this is unlikely to change any time soon.


[1] https://github.com/klee/klee/blob/master/include/klee/SolverImpl.h#L60
[2] https://github.com/klee/klee/blob/master/lib/Solver/Z3Builder.cpp#L416

Hope that helps,
Dan.