PathWalker: A dynamic symbolic execution tool based on LLVM byte code instrumentation

Dynamic symbolic execution (or concolic execution) is a powerful method for program analysis and software testing by attaching symbolic execution to the concrete running of a program. This paper proposes an approach to handle aggregate types (e.g., pointers, arrays, structures) and their complex combinations for the dynamic symbolic execution of C programs. The main idea of the approach is splitting a complex type program variable into a series of primitive type variables. During the concrete execution of a program, a con- colic execution engine is provided to observe the operations on every program variable at the level of primitive types, and then the symbolic state of the program is updated. The path constraints which must be satisfied to drive the program running along the current execution path are collected to generate new test data for other paths. Our approach guarantees that only primitive type variables can appear in the symbolic states and path constraints. Based on LLVM byte code instrumentation, we present a new tool, called PathWalker, which implements this approach. Experimental results reveal that PathWalker is effective to deal with complex types in C codes.