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

Simple item page
dc.contributor.advisorKhurshid, Sarfraz
dc.creatorDong, Shiyuen
dc.date.accessioned2014-09-18T19:05:53Zen
dc.date.accessioned2018-01-22T22:26:31Z
dc.date.available2018-01-22T22:26:31Z
dc.date.issued2014-05en
dc.date.submittedMay 2014en
dc.date.updated2014-09-18T19:05:53Zen
dc.descriptiontexten
dc.description.abstractCompiler 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.en
dc.description.departmentElectrical and Computer Engineeringen
dc.format.mimetypeapplication/pdfen
dc.identifier.urihttp://hdl.handle.net/2152/26000en
dc.language.isoenen
dc.subjectCompiler optimizationen
dc.subjectSymbolic executionen
dc.subjectKLEEen
dc.subjectLLVMen
dc.titleAn empirical study of the influence of compiler optimizations on symbolic executionen
dc.typeThesisen

Files

Collections

University of Texas at Austin