一句话：提出一种非语义保持但失败保持的编译期控制流变换，消除昂贵符号分支以提升动态符号执行的可扩展性。
动态符号执行（DSE）在目标程序含大量条件分支时面临路径爆炸问题。经典对策是动态状态合并，通过合并相似的符号状态避免状态数指数增长，但状态合并在每个分支处仍需调用求解器，即便两条路径都可行；而且 DSE 的最优路径搜索策略未必能创造最佳合并机会。已有工作尝试用编译期状态合并（把控制流转换为数据流以消除分支）来缓解这些缺陷。本文进一步提出一种非语义保持但失败保持（failure-preserving）的编译器变换，用于移除程序中代价高昂的符号分支，从而提升 DSE 的可扩展性。由于变换可能引入伪 bug，作者还构建了一个检测此类伪 bug 的框架。实验表明，该变换在多个基准程序上显著提升 DSE 性能，并在大型真实程序上改善了覆盖率与缺陷发现的效果。
Dynamic Symbolic Execution (DSE) suffers from the path explosion problem when the target program has many conditional branches. The classical approach for managing the path explosion problem is dynamic state merging. Dynamic state merging combines similar symbolic program states to avoid the exponential growth in the number of states during DSE. However, state merging still requires solver invocations at each program branch, even when both paths of the branch are feasible. Moreover, the best path search strategy for DSE may not create the best state merging opportunities. Some drawbacks of state merging can be mitigated by compile-time state merging (i.e., branch elimination by converting control-flow into dataflow). In this paper, we propose a non-semantics-preserving but failure-preserving compiler transformation for removing expensive symbolic branches in a program to improve the scalability of DSE. We have developed a framework for detecting spurious bugs that our transformation can insert. Finally, we show that our transformation can significantly improve the performance of DSE on various benchmark programs and help improve the performance of coverage and bug discovery of large real-world programs.
@article{paperbot3828,
title = {Taming the Hydra: Targeted Control-Flow Transformations for Dynamic Symbolic Execution},
author = {Charitha Saumya and Muhammad Hassan and Rohan Gangaraju and Milind Kulkarni and Kirshanthan Sundararajah},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {OOPSLA1},
year = {2026},
doi = {10.1145/3798202}
}