Return to search

An empirical study of the influence of compiler optimizations on symbolic execution

Compiler optimizations in the context of traditional program execution is a
well-studied research area, and modern compilers typically offer a suite of
optimization options. This thesis reports the first study (to our knowledge) on
how standard compiler optimizations influence symbolic execution. We
study 33 optimization flags of the LLVM compiler infrastructure, which are used
by the KLEE symbolic execution engine. Specifically, we study (1) how different
optimizations influence the performance of KLEE 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, KLEE's setting for applying the 33 optimizations in
a pre-defined order provides sub-optimal performance for a majority of the
Coreutils when using the basic depth-first search; moreover, in our experimental
setup, applying no optimization performs better for many of the Coreutils. / text

Identiferoai:union.ndltd.org:UTEXAS/oai:repositories.lib.utexas.edu:2152/26000
Date18 September 2014
CreatorsDong, Shiyu
Source SetsUniversity of Texas
LanguageEnglish
Detected LanguageEnglish
TypeThesis
Formatapplication/pdf

Page generated in 0.0018 seconds