TY - GEN
T1 - Studying the influence of standard compiler optimizations on symbolic execution
AU - Dong, Shiyu
AU - Olivo, Oswaldo
AU - Zhang, Lingming
AU - Khurshid, Sarfraz
N1 - Funding Information:
This work was funded in part by the National Science Foundation (NSF Grant Nos. CCF-0845628 and CCF-1319688).
Publisher Copyright:
© 2015 IEEE.
PY - 2016/1/13
Y1 - 2016/1/13
N2 - Systematic testing plays a vital role in increasing software reliability. A particularly effective and popular approach for systematic testing is symbolic execution, which analyzes a large number of program behaviors using symbolic inputs. Even though symbolic execution is among the most studied analyses during the last decade, scaling it to real-world applications remains a key challenge. This paper studies how a class of semantics-preserving program transformations, namely compiler optimizations, which are designed to enhance performance of standard program execution (using concrete inputs), influence traditional symbolic execution. As an enabling technology, the study uses KLEE, a well-known symbolic execution engine based on the LLVM compiler infrastructure, and focuses on 33 optimization flags of LLVM. Our specific research questions include: (1) how different optimizations influence the performance of symbolic execution for Unix Coreutils, (2) how the influence varies across two different program classes, and (3) how the influence varies across three different back-end constraint solvers. Some of our findings surprised us. For example, applying the 33 optimizations in a pre-defined order provides a slowdown (compared to applying no optimization) for a majority of the Coreutils when using the basic depth-first search with no constraint caching. The key finding of our work is that standard compiler optimizations need to be used with care when performing symbolic execution for creating tests that provide high code coverage. We hope our study motivates future research on harnessing the power of symbolic execution more effectively for enhancing software reliability, e.g., by designing program transformations specifically to scale symbolic execution or by studying broader classes of traditional compiler optimizations in the context of different search heuristics, memoization, and other strategies employed by modern symbolic execution tools.
AB - Systematic testing plays a vital role in increasing software reliability. A particularly effective and popular approach for systematic testing is symbolic execution, which analyzes a large number of program behaviors using symbolic inputs. Even though symbolic execution is among the most studied analyses during the last decade, scaling it to real-world applications remains a key challenge. This paper studies how a class of semantics-preserving program transformations, namely compiler optimizations, which are designed to enhance performance of standard program execution (using concrete inputs), influence traditional symbolic execution. As an enabling technology, the study uses KLEE, a well-known symbolic execution engine based on the LLVM compiler infrastructure, and focuses on 33 optimization flags of LLVM. Our specific research questions include: (1) how different optimizations influence the performance of symbolic execution for Unix Coreutils, (2) how the influence varies across two different program classes, and (3) how the influence varies across three different back-end constraint solvers. Some of our findings surprised us. For example, applying the 33 optimizations in a pre-defined order provides a slowdown (compared to applying no optimization) for a majority of the Coreutils when using the basic depth-first search with no constraint caching. The key finding of our work is that standard compiler optimizations need to be used with care when performing symbolic execution for creating tests that provide high code coverage. We hope our study motivates future research on harnessing the power of symbolic execution more effectively for enhancing software reliability, e.g., by designing program transformations specifically to scale symbolic execution or by studying broader classes of traditional compiler optimizations in the context of different search heuristics, memoization, and other strategies employed by modern symbolic execution tools.
UR - http://www.scopus.com/inward/record.url?scp=84964812504&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84964812504&partnerID=8YFLogxK
U2 - 10.1109/ISSRE.2015.7381814
DO - 10.1109/ISSRE.2015.7381814
M3 - Conference contribution
AN - SCOPUS:84964812504
T3 - 2015 IEEE 26th International Symposium on Software Reliability Engineering, ISSRE 2015
SP - 205
EP - 215
BT - 2015 IEEE 26th International Symposium on Software Reliability Engineering, ISSRE 2015
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 26th IEEE International Symposium on Software Reliability Engineering, ISSRE 2015
Y2 - 2 November 2015 through 5 November 2015
ER -