Disable solver invocation

25 views
Skip to first unread message

Weiqi Wang

unread,
Oct 27, 2021, 4:24:05 PM10/27/21
to S2E Developer Forum
Hi,

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:
1. Apart from the fork time query, why does s2e invoke the solver?
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?

Best,
Weiqi

Vitaly Chipounov

unread,
Oct 27, 2021, 5:00:35 PM10/27/21
to s2e...@googlegroups.com, Weiqi Wang
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

Weiqi Wang

unread,
Oct 28, 2021, 11:08:32 AM10/28/21
to S2E Developer Forum
Hi Vitaly,

Thanks for your reply! I'll experiment with the else branch.

Best,
Weiqi

Reply all
Reply to author
Forward
0 new messages