Browsing by Subject "KLEE"
Now showing 1 - 3 of 3
Results Per Page
Sort Options
Item An empirical study of the influence of compiler optimizations on symbolic execution(2014-05) Dong, Shiyu; Khurshid, SarfrazCompiler 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.Item Non-semantics-preserving transformations for higher-coverage test generation using symbolic execution(2016-05) Converse, Hayes Elliott; Khurshid, Sarfraz; Perry, DewayneSymbolic execution is a well-studied method that can produce high-quality test suites for programs. However, scaling it to real-world applications is a significant challenge, as it depends on the expensive process of solving constraints on program inputs. Our insight is that non-semantics-preserving program transformations can reduce the cost of symbolic execution and the tests generated for the transformed programs can still serve as quality suites for the original program. We present several such transformations that are designed to improve test input generation and/or provide faster symbolic execution. We evaluated these optimizations using a suite of small examples and a substantial subset of Unix's Coreutils. In more than 50% of cases, our approach reduces the test generation time and increases the code coverage.Item Using KLEE to generate test cases for the Texas Instruments® Stellaris® Peripheral Driver Library(2014-08) Mainor, Fredrick Dean; Khurshid, SarfrazSoftware engineers spend much of their time checking the correctness of software. Software testing is the most widely used technique for accomplishing this task. Most of the test cases used for checking software are manually created, and may not always cover all execution paths of the software. If key test cases are not executed, then the possibility of errors within the software still exists. By using tools that can automate the testing of software, software engineers can run exhaustive tests on their applications to provide verification and validation. Symbolic execution is a program analysis technique that can be utilized to achieve this. KLEE is an open-source dynamic test generation tool based on symbolic execution. In this report I present my results from evaluating KLEE on the Texas Instruments® Stellaris® Peripheral Driver Library. The Stellaris® Peripheral Driver Library consists of software drivers for controlling the peripherals on the Stellaris suite of ARM® Cortex-M based microcontrollers. In total 554 functions within the library were tested, and a total of 14763 test cases were generated. There were 32 bugs found in the software, which include assertion violations, memory errors, and arithmetic errors (division by zero, and shift errors).