ECOOP 2018
Sun 15 - Sat 21 July 2018 Amsterdam, Netherlands
co-located with ECOOP and ISSTA
Thu 19 Jul 2018 14:15 - 14:40 at Zurich II - Testing Chair(s): Alastair Donaldson

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 Jul

ecoop-2018-papers
13:50 - 15:30: ECOOP Research Papers - Testing at Zurich II
Chair(s): Alastair DonaldsonImperial College London
ecoop-2018-papers13:50 - 14:15
Research paper
Wing LamUniversity of Illinois at Urbana-Champaign, Siwakorn SrisakaokulUniversity of Illinois at Urbana-Champaign, USA, Blake BassettUniversity of Illinois at Urbana-Champaign, USA, Peyman MahdianUniversity of Illinois at Urbana-Champaign, USA, Tao Xie, Pratap LakshmanMicrosoft, India, Peli de HalleuxMicrosoft Research
DOI
ecoop-2018-papers14:15 - 14:40
Research paper
Junjie ChenPeking University, Wenxiang HuPeking University, Lingming Zhang, Dan HaoPeking University, Sarfraz KhurshidUniversity of Texas at Austin, Lu ZhangPeking University
DOI
ecoop-2018-papers14:40 - 15:05
Research paper
Gianluca MezzettiAarhus University, Denmark, Anders MøllerAarhus University, Martin Toldam TorpAarhus University
DOI
ecoop-2018-papers15:05 - 15:30
Research paper
Sihan Li, Farah HaririUniversity of Illinois at Urbana-Champaign, Gul AghaUniversity of Illinois at Urbana-Champaign, USA
DOI