程序的正确性验证一直以来都是计算机科学中的一个挑战性问题,抽象解释理论为程序静态分析提供了一个通用框架,可以在编译时自动地推导程序的动态性质.基于抽象解释的数值程序分析可以自动推导程序中数值变量间的不变式关系,这对于编译优化、程序错误检查至关重要.本文建立并实现了一个面向C和Fortran程序并支持过程间分析的数值程序分析框架和工具,C或Fortran源程序经过预处理后转化为具有统一格式的中间表示形式,然后基于该中间表示抽取与源程序语义等价的语义等式,最后在该语义等式上进行不动点迭代计算从而得到程序不变式.在此基础上,本文还对数组等复杂语法结构进行了建模和抽象.实验结果表明,该工具具有较高的可扩展性、精度,并能够处理大部分因数组的使用而带来的程序分析上的问题.%The validation of program correctness is a challenge problem in computer science. The theory of abstract interpretation provides a general framework for static analysis which can deduce programs' dynamic property automatically. A value range analysis based on abstract interpretation can give the invariant relationship of variables at every program point, which is very important to compilation optimization and error examination. We propose an interprocedural framework that analyses the value range information of numerical programs, which can process C and Fortran programs. The C or Fortran source program is first preprocessed to an uniform representation, and then we draw the semantic equation which is equivalent to the source semantics. Finally, the iterative computation is done on this syntax equation to get the program invariant. Besides, we model some complex syntax structures such as array. The experiment indicates that our framework is very extensive and precise, and can process most problems brought by the usage of array.
展开▼
