Hi,
On 10/27/21 10:24 PM, Weiqi Wang wrote:
> I'm wondering if it's possible for s2e to not ask the solver during
> runtime since it's guided by concrete value. In my case, I want to
> collect constraints along the concrete execution path. I've already
> disable the fork so solver invocation there has been disabled.
> However, I found that s2e still queries the solver. e.g. [1]. I
> commented it out but resulted in segmentation fault. My questions are:
toUnique() has to prove that there is only one solution for x, so it
must use the solver. We could argue if it's necessary to use this api
from the call site you mentioned. I'd say probably not, since we can
fall back to fork and concretize anyway, so you could only keep the else
branch [1]
> 1. Apart from the fork time query, why does s2e invoke the solver?
I can't tell from the top of my head. Best approach is to put
breakpoints in the solver layer and see what hits it.
> 2. Apart from [1], are there other places where s2e invoke the solver?
> Could you please show me where they are?
> 3. Is it possible to disable all the solver invocation?
Probably, we'd have to understand the context for each solver call.
Vitaly
[1]
https://github.com/S2E/s2e/blob/master/klee/lib/Core/Executor.cpp#L1561