Analysis Of Pointer Programs And Inference Of Loop-Invariant Shape Graphs

In recent years, software systems are becoming more and more important for everyday life and work while the scale of software systems is larger and larger. Therefore, people must pay more attention to the properties such as correctness, safety and security of complicated software systems. It is necessary to use high-confidence software in some areas of safety-critical. Formal verification is a major method to improve the dependability of the software. However, in the phase of typical formal verification, it is inconvenient for programmers that they usually provide pre-/post-conditions and loop invariants manually. At the same time, there is not a prefect method for loop invariant inference. Thus, it is slowly that the product of formal verification be applied in the industry yet.It is of significance to find a method to inference loop invariant automatically for program analysis and program verification. To the programs dealing with pointers, we can obtain much useful information for loop invariant inference and program verification by shape analysis.This paper uses a new method to solve the problems of Analysis and verification of programs dealing with pointers and loop invariant inference. We have designed a system named shape system for the PointerC programming language. Programmers must declare the shapes that the recursive data structures intend to build, and the shapes that pointer variables point to. Compilers or other tools can use shape inference rules to infer shapes constructed by the programs via dynamically allocated structures, and then do shape checking to judge whether the shape confirms to what the programmer has declared, according to shape checking rules. At the same time, we have designed a method for shape analysis based on the shape graph logic. According this method, we can obtain the pre-/post-conditions and loop invariant shape graphs associated with pointers.Shape graphs are used to express the point-to relations of statically declared pointer variables and the pointer-typed fields in the dynamically allocated data structures. The shape graph precisely expresses the equalities between various pointers, and can provide other useful information, e.g. the alias of the given access path. Loop invariant shape graphs are the shape graphic description of loop invariant associated with pointers. The shape graph logic is an extension to Hoare logic from the viewpoint that the shape graph is a graphical expression of the assertions on pointers, and it and can be used in the program analysis and verification of programs manipulating mutable data structures.Based on the shape graph logic, we have implemented a program verifier for the PointerC language. It can verify programs dealing shapes defined in this paper. Programmers need not to provide pre-/post-conditions and loop-invariants concerning about shapes. The specifications about the structures are required. And, in some extent, the method which has been designed and implemented in this paper can be used to solve the difficult problem of loop invariant inference. It also can be used to alleviate burdens of program verification.