search

S2E / s2e-env

Your S2E project management tools. Visit https://s2e.systems/docs to get started.
Other
92 stars 51 forks source link

`module.bc` contains traced functions from only one state during symbolic execution #462

Closed michaelbrownuc closed 2 years ago

michaelbrownuc commented 2 years ago

When I run S2E on a binary with symbolic arguments specified, the output LLVM bitcode file module.bc seems to contain only functions traced from the last forked state. I looked around the source code and it appears that each new forked state in S2E starts with a clean version of op_helper. I am not sure if this is the intended behavior or not.

I am curious - is there a way to indicate I want all traced functions across all explored states to be captured in module.bc? It looks like I could probably build a plugin to write each state to disk separately on state forks and switches to merge them later, but I am hoping there is an easier way.

vitalych commented 2 years ago

S2E removes unused translation blocks from the bitcode file to reduce memory usage. This happens when the reference count to an LLVM translation block drops to zero. https://github.com/S2E/s2e/blob/master/libs2ecore/src/S2ETranslationBlock.cpp#L39

module.bc is shared among all states and its content is non-deterministic, state scheduling and system events may affect translation block generation.

michaelbrownuc commented 2 years ago

Thanks for the info! It sounds like to collect these functions I will need to produce a plugin to capture the content at the specific analysis points I care about. I will close this issue.