驯服 Hydra：面向动态符号执行的定向控制流转换
Taming the Hydra: Targeted Control-Flow Transformations for Dynamic Symbolic Execution
AI总结：
本文提出一种非语义保持但失败保持的编译器转换，用于移除程序中的昂贵符号分支，以提升动态符号执行的可扩展性。通过检测虚假bug，该方法在多个基准程序和大型实际程序中显著提高了性能。
摘要：
动态符号执行（DSE）在目标程序有大量条件分支时会遭遇路径爆炸问题。经典方法是动态状态合并，通过合并相似的符号程序状态来避免状态数量的指数增长。然而，状态合并仍需要在每个程序分支调用求解器，即使分支的两个路径都可行。此外，DSE的最佳路径搜索策略可能不会创建最佳的状态合并机会。一些状态合并的缺点可以通过编译时状态合并（即通过将控制流转换为数据流来消除分支）来缓解。在本文中，我们提出了一种非语义保持但失败保持的编译器转换，用于移除程序中的昂贵符号分支，以提高DSE的可扩展性。我们开发了一个框架来检测我们的转换可能插入的虚假bug。最后，我们展示了我们的转换在各种基准程序上显著提高了DSE的性能，并帮助提高大型实际程序的覆盖率和bug发现性能。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
