一个面向C和Fortran数值程序的静态分析工具
收稿日期: 2009-10-17
修回日期: 2009-12-15
网络出版日期: 2011-03-25
基金资助
国家自然科学基金资助项目(90818024,60803042)
A Static Analyzer for Numerical Programs in C and Fortran
Received date: 2009-10-17
Revised date: 2009-12-15
Online published: 2011-03-25
程序的正确性验证一直以来都是计算机科学中的一个挑战性问题，抽象解释理论为程序静态分析提供了一个通用框架，可以在编译时自动地推导程序的动态性质。基于抽象解释的数值程序分析可以自动推导程序中数值变量间的不变式关系，这对于编译优化、程序错误检查至关重要。本文建立并实现了一个面向C和Fortran程序并支持过程间分析的数值程序分析框架和工具，C或Fortran源程序经过预处理后转化为具有统一格式的中间表示形式，然后基于该中间表示抽取与源程序语义等价的语义等式，最后在该语义等式上进行不动点迭代计算从而得到程序不变式。在此基础上，本文还对数组等复杂语法结构进行了建模和抽象。实验结果表明，该工具具有较高的可扩展性、精度，并能够处理大部分因数组的使用而带来的程序分析上的问题。
侯苏宁，陈立前，王昭飞，王戟 . 一个面向C和Fortran数值程序的静态分析工具[J]. 计算机工程与科学, 2011 , 33(3) : 94 -102 . DOI: 10.3969/j.issn.1007130X.2011.
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.
［1］Cousot P, Cousot R. Abstract Interpretation:A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints［C］∥Proc of the 4th POPL,1977:238252.
［2］Cousot P, Cousot R. Static Determination of Dynamic Properties of Programs［C］∥Proc of the 2nd Int’l Symp on Programming,1976:106130.
［3］Cousot P, Halbwachs N. Automatic Discovery of Linear Restraints Among Variables of a Program［C］∥Proc of the 5th POPL,1978:8497.
［4］Mine A. The Octagon Abstract Domain［J］. HigherOrder and Symbolic Computation, 2006, 19(1):31100.
［5］李梦君, 李舟军, 陈火旺. 基于抽象解释理论的程序验证技术［J］. 软件学报, 2008, 19(1):1726.
［6］The LLVM Compiler Infrastructure［EB/OL］.［20090625］. http://www.llvm.org.
［7］Cooper K D, Harvey T J, Kennedy K. Iterative DataFlow Analysis, Revisited［C］∥Proc of PLDI’03, 2003.
［8］Cousot P,Cousot R. Systematic Design of Program Analysis Frameworks［C］∥Proc of Symp on Princ of Prog Lang,1979:269282.
［9］Cousot P. The Verification Grand Challenge and Abstract Interpretation［C］∥Proc of the Verified Software:Tools, Theories, Experiments, 2007:227240.
［10］Blanchet B, Cousot P, Cousot R, et al. A Static Analyzer for Large SafetyCritical Software［C］∥Proc of the ACM SIGPLAN 2003 Conf on Programming Language Design and Implementation,2003:196207.
［11］Venet A, Brat G. Precise and Efficient Static Array Bound Checking for Large Embedded C Programs［C］∥Proc of the ACM SIGPLAN 2004 Conf,2004:231242.
［12］Wilson R P, Lam M S. Efficient ContextSensitive Pointer Analysis for C Programs［C］∥Proc of the ACM SIGPLAN 1995 Conf on Programming Language Design and Implementation, 1995:112.
［13］Karr M. Affine Relationships Among Variables of a Program［C］∥Proc of the Acta Inf, 1976:133151.
［14］Jeannet B,Miné A. Apron: A Library of Numerical Abstract Domains for Static Analysis［C］∥Proc of CAV’09,2009:661667.
［15］Halbwachs N,Peron M. Discovering Properties about Arrays in Simple Programs［C］∥Proc of PLDI’08, 2008:339348.
［16］Jeannet B.The Interproc Analyzer［EB/OL］.［20090625］.http://popart.inrialpes.fr/interproc/interprocweb.cgi.
［17］Gopan D, Maio F Di, Dor N,et al. A Framework for Numeric Analysis of Array Operations［C］∥Proc of POPL’05, 2005:338350.
/
| 〈 |
|
〉 |