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 <fabrizio.bio...@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@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev


  
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Reply via email to