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