Computer Engineering & Science >
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
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.
HOU Suning,CHEN Liqian,WANG Zhaofei,WANG Ji . A Static Analyzer for Numerical Programs in C and Fortran[J]. Computer Engineering & Science, 2011 , 33(3) : 94 -102 . DOI: 10.3969/j.issn.1007130X.2011.
［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.
/
| 〈 |
|
〉 |