Inquiry About Compositional Symbolic Execution and Function Summary Generation in S2E

[qiaosen liu]

I hope this message finds you well. I am currently researching tools for compositional symbolic execution and am interested in exploring S2E’s capabilities in this domain. My work focuses on generating function summaries to improve the scalability of symbolic execution for complex programs.

I understand that S2E is a powerful platform for whole-system symbolic execution, leveraging QEMU and LLVM for analyzing both user-space and kernel-space code. However, I am unclear whether S2E supports compositional symbolic execution, particularly the generation of function summaries (e.g., encoding preconditions and postconditions for function paths).

Could you please confirm if S2E includes support for generating function summaries as part of compositional symbolic execution? If this feature is available, could you provide guidance on how to enable or implement it? If not, are there any known extensions, plugins, or related tools that integrate compositional analysis with S2E?

Thank you for your time and support. I greatly appreciate any insights or references to relevant documentation or resources.

Best regards,
Lqs66

[Vitaly Chipounov]

Hi,

S2E does not support automatically generating summaries. You can write them manually if you want though. They are called function models [1].

Vitaly

[1] https://github.com/S2E/s2e/tree/master/libs2eplugins/src/s2e/Plugins/Models