A Specification Language For Precise Shape Analysis Of C Program

With the rapid development of computer science and technology, computer software is getting larger and more complex. The increasing of the difficulty and the cost for software testing and maintenance made the software safety more important. Particularly in safety-critical areas,(e.g., aerospace, high-speed rail, nuclear power, medical and so on), the demand for high-confidence software is growing. In these areas, C programing language is still the most commonly used. Null pointer dereference, memory leak, buffer overflow and many other memory safety issues of C program are still highlighted problems in software development.There are many approaches to improve the quality of software, such as software testing, program analysis and program verification and so on. Among these methods, a relatively efficient and economical one is static program analysis. Our laboratory research group has developed a static analysis tool to check C program memory safety issues. We use a static analysis via symbolic execution, with shape analysis support. In order to reduce the false positive rate and false negative rate of static analysis and improve the efficiency of analysis, we design a proper specification language to describe program states and function behaviors.The proposed specification language is used to describe function behaviors, including assertions for program states, predicates for memory states, shape predicates for single-linked lists, doubly-linked lists and binary trees. The tool is based on a compiler framework LLVM and symbolic execution tool KLEE. The tool analyses and builds specifications for each function. In this process, we use an assertion language to describe program states and abstract the program states into shape predicates whenever needed. Since, we design a series of rules to do the normalization and abstraction on assertions.The main contributions of this paper are as follows:Firstly, this paper designs and implements a specification language for describing function behaviors, including assertions for program states, predicates for memory, shape predicates for single-linked lists, doubly-linked lists and binary trees. Using the specification language to record analyzed function behaviors, we avoid duplicated analysis and improve the efficiency of analysis. Our tool can check memory leak, double free and other memory safety issues and can do shape analysis with the help of the proposed predicates. Secondly, we design and implement a series of rules to do the normalization and abstraction on assertions. The rules abstract the program states into shape predicates and do shape analysis. Thirdly, we use the proposed specification language to construct function behaviors for C language standard library functions manually. C library functions are frequently called in many programs, so constructing function behaviors for these functions can improve the precision and efficiency of analysis.In short, this paper proposes a specification language for C language memory safety issues and a series of abstraction rules for shape anslysis. The rules are used to check the memory safety issues for single-linked lists, doubly-linked lists and binary trees in programs. This work lays a foundation for the future research and tool extensions.