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 <[email protected]> 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
[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
