> > 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)
Thanks, this was very helpful. I understand now. > > 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. Yes, I am assuming they are equivalent or at least equisatisfiable. I will investigate a little into this. > [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. It does! Thank you again, Fabrizio _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
