[klee-dev] Solving path constraints incrementally

[Andrew Santosa]

Hi Sergey,
Although this is only a guess, my guess is that this is because KLEE is worklist-based, where an item in the worklist represents an execution state. The executor (Executor class) has a field searcher, whose runtime type determines the kind of exploration strategy used by KLEE. Executor::run calls searcher->selectState() to get the worklist item (program state) to symbolically execute. In case of depth-first search, the item returned by selectState() is just the last item added into the worklist (see the implementation in DFSSearcher class), other strategy may return different item. The point here, is that KLEE's path exploration may not necessarily use depth-first strategy, so it may not be correct to reuse the solving environment when switching between different worklist items.

Best,
Andrew 

    On Sunday, 24 July 2016, 23:17, Sergey Mechtaev <mechtaev at gmail.com> wrote:
 

 Hello, 
It seems like KLEE does not use SMT solver incrementality when solving path conditions. Specifically, I refer to the STPSolverImpl::computeInitialValues that asserts all clauses from the query and, after solving, removes them using pop. However, since KLEE explicitly maintains execution states, I expected that it would reuse previous solving environment in subsequent queries. I didn't manage to find any explanation of this design choice in the KLEE publications.
Can you please tell me if my understanding is correct? What was the motivation behind this choice? 
Regards,Sergey Mechtaev
_______________________________________________
klee-dev mailing list
klee-dev at imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev


  
-------------- next part --------------
HTML attachment scrubbed and removed