Program Loop Bounds Analysis Based On Abstract Interpretation

For the rapid development of computer science and widely application of computer technology,it turn out to be an important fact that people focus more and more on the issue about whether a computer program can execute correctly.Especially in some significant domain,the requirement for execute program correctly,not only ask for the right result from the program execution,for an error might induce severe safety accidents,but also need to execute the program in a limit time.In some safety critical field,once the program fail to finish the exact task in the limited time,may lead to heavy property loss or the killing of peoples life.Thus,it's an import subject to research about the execution time of programs.The first step for program execution time analysis is to analysis the process of the the computer program execution independent from the hardware environment.In the three basic structure of computer program,loop is the most complex one.The iteration of a loop during the execution of the computer program will have great influence on the execution time of computer program.In this thesis,we will focus on the iteration of the loop,so that we can get the loop bound of a program.The main content of the thesis is as follows:(1)Construct the control flow graph and data dependent graph from the data dependence relationship and control dependence relationship and construct the program dependence graph.The remove the redundancy points to reduce the program dependence graph.And use the reduced program dependence graph as a guideline for program slicing.(2)Construct the abstract expression of program variables and functions in an interval abstract domain.According to the constrains,which got form the first phase,to improve the method for loop bounds calculation,so that we can get an more precise loop bound.(3)Construct the frame for the program loop bound analysis.Then make a case analysis of the loop bounds calculation.In the end an open source framework Frama-C was used to verify the result the case analysis and to prove the correctness of loop bound analysis.