Learning to Accelerate Symbolic Execution via Code Transformation
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 methods 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.
Thu 19 JulDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
13:50 - 15:30 | |||
13:50 25mResearch paper | A Characteristic Study of Parameterized Unit Tests in .NET Open Source Projects ECOOP Research Papers Wing Lam University of Illinois at Urbana-Champaign, Siwakorn Srisakaokul University of Illinois at Urbana-Champaign, USA, Blake Bassett University of Illinois at Urbana-Champaign, USA, Peyman Mahdian University of Illinois at Urbana-Champaign, USA, Tao Xie , Pratap Lakshman Microsoft, India, Peli de Halleux Microsoft Research DOI | ||
14:15 25mResearch paper | Learning to Accelerate Symbolic Execution via Code Transformation ECOOP Research Papers Junjie Chen Peking University, Wenxiang Hu Peking University, Lingming Zhang , Dan Hao Peking University, Sarfraz Khurshid University of Texas at Austin, Lu Zhang Peking University DOI | ||
14:40 25mResearch paper | Type Regression Testing to Detect Breaking Changes in Node.js Libraries ECOOP Research Papers Gianluca Mezzetti Aarhus University, Denmark, Anders Møller Aarhus University, Martin Toldam Torp Aarhus University DOI | ||
15:05 25mResearch paper | Targeted Test Generation for Actor Systems ECOOP Research Papers Sihan Li , Farah Hariri University of Illinois at Urbana-Champaign, Gul Agha University of Illinois at Urbana-Champaign, USA DOI |