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.

翻译：动态符号执行（DSE）在处理具有大量条件分支的目标程序时，面临路径爆炸问题。应对路径爆炸问题的经典方法是动态状态合并。动态状态合并将相似的符号程序状态合并，以避免DSE过程中状态数量的指数级增长。然而，即使程序分支的两个路径均可行，状态合并仍需在每个分支处调用求解器。此外，DSE的最佳路径搜索策略可能无法创造最优的状态合并机会。通过编译时状态合并（即，通过将控制流转换为数据流来消除分支），可以缓解状态合并的部分缺陷。本文提出一种非语义保持但故障保持的编译器变换方法，用于移除程序中代价高昂的符号分支，从而提升DSE的可扩展性。我们开发了一个框架，用于检测该变换可能引入的虚假缺陷。最后，我们通过实验表明，该变换能显著提升DSE在各种基准测试程序上的性能，并有助于提升大型真实世界程序的覆盖率与缺陷发现能力。