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 <[email protected]>
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
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
