Learning to Accelerate Symbolic Execution via Code Transformation
Learning to Accelerate Symbolic Execution via Code Transformation
复制标题
DOI：
10.4230/lipics.ecoop.2018.6
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Junjie Chen;Wenxiang Hu;Lingming Zhang;Dan Hao;S. Khurshid;Lu Zhang
中科院分区：
文献类型：
--
作者：
Junjie Chen;Wenxiang Hu;Lingming Zhang;Dan Hao;S. Khurshid;Lu Zhang
符号执行是一种自动测试生成的有效但昂贵的技术。多年来，已经提出了大量精致的符号执行技术来提高其效率。但是，符号执行效率问题仍然存在，并且在很大程度上限制了符号执行在实践中的应用。正交到精致的符号执行，在本文中，我们建议通过对目标程序上的语义代码转换来加速符号执行。在此方向的初始阶段，我们采用了特定的代码转换，编译器优化，最初提议通过将源程序转换为具有提高效率（例如，更快或更小）的另一个语义保留目标程序来加速程序具体执行。但是，编译器优化主要是为了加速程序具体执行而不是符号执行。最近的工作还报告说，统一的编译器优化设置可以加速任何程序的符号执行。因此，在这项工作中，我们提出了一种基于机器学习的方法来调整编译器优化以加速符号执行，其结果还可以帮助进一步设计特定代码转换以实现符号执行。尤其是，提出的方法LEO通过我们的程序 - 拼写器将源代码函数和库分开，并通过分析现有符号执行的性能，预测单个编译器优化（即是否选择了代码转换类型）。最后，Leo在编译器优化（通过我们的本地访问器）转换的代码上应用符号执行。我们使用KLEE象征性执行引擎对GNU Coreutils计划进行了实证研究。结果表明，LEO显着加速了符号执行，超过了默认的KLEE配置（即，在各种设置中打开/关闭所有编译器优化），例如，在默认的培训/测试时间中，Leo可以在50/68中获得最高线的覆盖率与转弯相比打开/关闭所有编译器优化。
Symbolic execution is an effective but expensive technique for automated test generation. Over the years, a large number of refined symbolic execution techniques have been proposed to improve its efficiency. However, the symbolic execution efficiency problem remains, and largely limits the application of symbolic execution in practice. Orthogonal to refined symbolic execution, in this paper we propose to accelerate symbolic execution through semantic-preserving code transformation on the target programs. During the initial stage of this direction, we adopt a particular code transformation, compiler optimization, which is initially proposed to accelerate program concrete execution by transforming the source program into another semantic-preserving target program with increased efficiency (e.g., faster or smaller). However, compiler optimizations are mostly designed to accelerate program concrete execution rather than symbolic execution. Recent work also reported that unified settings on compiler optimizations that can accelerate symbolic execution for any program do not exist at all. Therefore, in this work we propose a machine-learning based approach to tuning compiler optimizations to accelerate symbolic execution, whose results may also aid further design of specific code transformations for symbolic execution. In particular, the proposed approach LEO separates source-code functions and libraries through our program-splitter, and predicts individual compiler optimization (i.e., whether a type of code transformation is chosen) separately through analyzing the performance of existing symbolic execution. Finally, LEO applies symbolic execution on the code transformed by compiler optimization (through our local-optimizer). We conduct an empirical study on GNU Coreutils programs using the KLEE symbolic execution engine. The results show that LEO significantly accelerates symbolic execution, outperforming the default KLEE configurations (i.e., turning on/off all compiler optimizations) in various settings, e.g., with the default training/testing time, LEO achieves the highest line coverage in 50/68 programs, and its average improvement rate on all programs is 46.48%/88.92% in terms of line coverage compared with turning on/off all compiler optimizations.