Analysis Of Programs With Pointer Arithmetic Based On Abstract Interpretation

As the basic syntax elements of C language, pointers are used with a high degree of flexibility in programs. This flexibility has brought great convenience for the writing of C program, but also makes the improper use of pointers become one of the main cases of null pointer dereference, array out of bound and other illegal memory access. Pointer arithmetic is a common class of pointers usage in embedded program. Researching on the analysis with pointer arithmetic program is of great significance to improve the software credibility of aerospace and other safety critical field.interpretation provides a general theoretical framework for program static analysis. The analysis of program numerical properties based on abstract interpretation can effectively analyze the value ranges of the program numerical variables. Pointer analysis technique can effectively analyze the point-to information and the alias information of the pointer variables in the program. But single numerical analysis technology or pointer analysis techniques cannot effectively deal with pointer arithmetic. Therefore, in the framework of abstract interpretation, we present the method for analysis of programs with pointer arithmetic, which has combined the numerical analysis with the point-to analysis.Firstly, we design a precise pointer memory model to characterize point-to information of pointer variable, and provide the abstract memory model for the analysis of pointer arithmetic. Then based on the abstract memory model, we design and implement a point-to domain to support the analysis of point-to relationship. Finally, we combine numerical analysis and point-to analysis to get numerical invariants and point-to invariants of pointer arithmetic program staticly. Based on these invariants, we can automatically look up all the possible runtime errors of pointer arithmetic program.Using the open-source numerical abstract domain library Apron and the point-to domain we have implemented, we develop a static analysis tool prototype for pointer arithmetic program based on abstract interpretation.Our tool is divided into four parts: front end preprocessing module, the abstract domain library module, the fix-point solution module and alarm module. Presently, our tool has owned the ability to effectively analyze part of the C programs with pointer arithmetic. We have carried out some experiments based on our tool. The experimental results show that our tool can effectively get the point-to information and the numerical properties of the pointer program, and we can also obtain a reasonable trade-off between efficiency and accuracy during the analysis.