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
| Identifer | oai:union.ndltd.org:UTEXAS/oai:repositories.lib.utexas.edu:2152/26000 |
| Date | 18 September 2014 |
| Creators | Dong, Shiyu |
| Source Sets | University of Texas |
| Language | English |
| Detected Language | English |
| Type | Thesis |
| Format | application/pdf |
Page generated in 0.002 seconds