State Merge For A Symbolic Execution Engine With Shape Analysis

The C programming language has been widely used in the fields of operating sys-tem, embedded software and the underlying drivers which require high efficiency for its flexibility and efficient control to the machine. For the consideration of flexibility and efficiency, the C programming language gives programmers the ability to control computer completely at the expense of a certain degree of safety:invalid pointer deref-erence, memory leak, buffer overflow and etc. These issues related to memory safety is particularly prominent in the C programming language. Due to the special application fields of the C programming language, the loss caused by the unsafety of this language becomes more and more severe, but the cost of debugging, testing and maintenance of these software written by the C programming language is getting higher nowadays.To improve the reliability of software is always one goal in software development. Dynamic testing, static analysis and program verification are the three main methods to ensure the quality of software. As the most strict way to ensure the correctness of pro-grams, verification uses formal methods giving strict mathematical proof for a program satisfying its specifications; however the verification process needs large man power to prove the theorems in the procedure, and therefore can not get extensive application in the industry. The results of dynamic test depend on a given test set. When testing a complex software, it is difficult to create a test set to achieve high code coverage, and it is often risky and expensive to run the code for dynamic testing. Static analysis gives a way to analyze the code without running the program. It can find the defects in the code earlier with a lower cost.Symbolic execution is widely used in static code annlysis for its well controlled precision and code coverage. When applied to analyze a program, symbolic execution traversals all possible states by simulating the execution of the program. High precision and code coverage request detailed and complete description of program states, which will lead to the path-explosion problem in almost all implementations of symbolic ex-ecution, results in bad scalability. We have implemented a C program static analysis tool with shape analysis based on symbolic execution which also suffer from the path-explosion problem. The main work of this paper is designing and implementing the state merge algorithm in our tool to attack the path-explosion problem. The contributions are as follows:● Designing and implementing the state merge algorithm for the symbolic execution engine with shape analysis. The challenge in this work is to ensure the analysis results will retain its precision after the state merge is introduced, especially to design the merge rules for the shape predicates.● According to the actual effect of state merge, put forward an optimization scheme which considers the ability of constraint solver and the time cost by the constraint solver. We analyze the data dependency in LLVM IR code to get the changes in time cost caused by state merge.● Take part in the develop of the demo tool ShapeChecker, which can find some memory safety related defects in the C programming language.