Change number of symbolic bits in symbolic pointers

[Weiqi Wang]

Hi,

Currently s2e allows lower 12 bits to be symbolic. Is there an easy way to change it to something smaller?

I tried to modify [1] and [2] to use 7 instead of 12. But s2e segmentation faults.

[1] https://github.com/S2E/s2e/blob/master/libcpu/include/cpu/se_libcpu_config.h#L38

[2] https://github.com/S2E/s2e/blob/master/libcpu/include/cpu/se_libcpu_config.h#L46

Best,

Weiqi

[Vitaly Chipounov]

Hi,

S2E used to have a mechanism to split 4K pages into smaller chunks to
reduce the load on the solver. The code is still there [1,2], though I
don't know if it works and I didn't test it after upgrading the engine
from the old S2E. I forgot if SE_RAM_OBJECT_BITS is the right place to
modify, it seems like there is a 128 byte size assumption here [3].
I'll try to look into it when I get a chance. In the meantime, if
there is a crash, run the debug build and attach the stack trace,
maybe it will help.

Vitaly

[1] https://github.com/S2E/s2e/blob/master/klee/lib/Core/AddressSpace.cpp#L170
[2] https://github.com/S2E/s2e/blob/0be5c89df54b534025ea078488889ccbf20d6344/klee/lib/Core/Executor.cpp#L1882
[3] https://github.com/S2E/s2e/blob/0be5c89df54b534025ea078488889ccbf20d6344/klee/lib/Core/AddressSpace.cpp#L191

> --
> --
> You received this message because you are a member of the S2E Developer Forum.
> To post to this group, send email to s2e...@googlegroups.com
> To unsubscribe from this group, send email to s2e-dev+u...@googlegroups.com
> For more options, visit this group at http://groups.google.com/group/s2e-dev
>
> ---
> You received this message because you are subscribed to the Google Groups "S2E Developer Forum" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to s2e-dev+u...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/s2e-dev/a114029d-3296-468d-b04c-d8b3f27e7bddn%40googlegroups.com.

[Weiqi Wang]

Hi Vitaly,

Thanks for your reply. I've attached the backtrace. The program is the same as this thread.

Best,

Weiqi

[Vitaly Chipounov]

Hi,

I created an issue for this: https://github.com/S2E/s2e-env/issues/438

Vitaly

On 8/13/21, Weiqi Wang <wqwa...@gmail.com> wrote:
> Hi Vitaly,
>
> Thanks for your reply. I've attached the backtrace. The program is the same
>

> as this thread <https://groups.google.com/g/s2e-dev/c/7WZ4HEfo3MU>.

> https://groups.google.com/d/msgid/s2e-dev/234eb6ac-cdff-43d3-a5ef-43c1e18eb62bn%40googlegroups.com.
>

[Weiqi Wang]

Hi Vitaly,

Thanks. Is there a way to just reduce the number of symbolic bits instead of splitting the pages? I thought it would be a simple fix. Because in some cases the array which the symbolic pointer indexes into is <=128 bytes (containing ASCII characteres for example). 7 symbolic bits are enough to explore the array. Please correct me if I am wrong as I'm not familiar with s2e's internals.

Best,

Weiqi

[Vitaly Chipounov]

Hi,

You could try to add constraints on these bits, but that won't change the fact that KLEE will still send the whole page to the solver, which is what makes it hard. It will also not handle various cases where the pointer overlaps adjacent pages. Note that the approach of splitting pages like I described is more of a hack than a solution anyway. It would be good to understand why the solver struggles with these expressions and perhaps rewrite them in a more efficient way. Perhaps someone knowledgeable here could give more insights about this.

Vitaly

[Weiqi Wang]

Got it. Thanks!