Research And Implementation Of Analysis For Numerical Properties Of Program Variables Based On Abstract Interpretation

With the rapid development of computer technology, software has become the dominant factor to system safety. As numerical computation is an indispensable part of the software, a small numerical error of program variables may cause safety accidents. How to guarantee the correctness of the numerical properties of program variables in software has become an important research topic in academia and industry. Abstract interpretation theory that constructing and approximating the program?s fixpoint semantics, abstracting the numerical properties of the undecidable program variable, is the most suitable method to analyze the numerical properties of the program variables.In this thesis we transform the source program to the control flow graph, and call the abstract domain operators by traversing the control flow graph to transform the numerical properties of program variables into the abstract domain. Then we simulate the actual operations of the program in the abstract environment by computing the least fixpoints of program variables. At last, we analyze and verify numerical properties of program variables, in order to find out numerical errors in the program. The main contents of this thesis include:(1) We construct the abstract environment of the program, and transform the concrete program into the abstract domain. Firstly, we give the method of improving the traditional control flow graph, and transform the source program into the control flow graph. Then, we construct the abstract environment of each node in the control flow graph according to the transformation algorithm of abstract domain elements. Finally, we traverse the control flow graph, call the abstract operators and generate the abstract value of each node.(2) We verify the numerical properties of program variables by the simulation of actual program in the abstract environment. Firstly, we give a fixpoint iterative algorithm of the abstract value of program variables in abstract domain. Then, we give a method to transform the fixpoint value into the constraint relation between variables. Finally, we verify the constraint relation of the program variables according to the system requirements and analyze the results.(3) We design and implement a prototyping tool to analyze and verify the numerical properties of program variables, and analyze the SFCU using the prototyping tool. Firstly, we give the design scheme and implementation method of each module. Then, we analyze the SFCU with the tool. Finally, we verify the numerical properties of program variables by using the prototype tool and find 3 errors, and the programming team confirmed that they are real errors in the original C code. We correct the errors, in order to ensure the safety and reliability of the system.