A Static Analyzer for Numerical Programs in C and Fortran

doi:10.3969/j.issn.1007130X.2011.

J4 ›› 2011, Vol. 33 ›› Issue (3): 94-102.doi: 10.3969/j.issn.1007130X.2011.

• 论文 • Previous Articles Next Articles

A Static Analyzer for Numerical Programs in C and Fortran

HOU Suning,CHEN Liqian,WANG Zhaofei,WANG Ji

（National Laboratory for Parallel and Distributed Processing,Changsha 410073,China）

Received:2009-10-17 Revised:2009-12-15 Online:2011-03-25 Published:2011-03-25

Abstract

Abstract:

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.

Key words: static analysis;abstract interpretation;value range analysis;numeric abstract domain;array abstraction

HOU Suning,CHEN Liqian,WANG Zhaofei,WANG Ji. A Static Analyzer for Numerical Programs in C and Fortran[J]. J4, 2011, 33(3): 94-102.

References

［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:238252.
［2］Cousot P, Cousot R. Static Determination of Dynamic Properties of Programs［C］∥Proc of the 2nd Int’l Symp on Programming,1976:106130.
［3］Cousot P, Halbwachs N. Automatic Discovery of Linear Restraints Among Variables of a Program［C］∥Proc of the 5th POPL,1978:8497.
［4］Mine A. The Octagon Abstract Domain［J］. HigherOrder and Symbolic Computation, 2006, 19(1):31100.
［5］李梦君, 李舟军, 陈火旺. 基于抽象解释理论的程序验证技术［J］. 软件学报, 2008, 19(1):1726.
［6］The LLVM Compiler Infrastructure［EB/OL］.［20090625］. http://www.llvm.org.
［7］Cooper K D, Harvey T J, Kennedy K. Iterative DataFlow 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:269282.
［9］Cousot P. The Verification Grand Challenge and Abstract Interpretation［C］∥Proc of the Verified Software:Tools, Theories, Experiments, 2007:227240.
［10］Blanchet B, Cousot P, Cousot R, et al. A Static Analyzer for Large SafetyCritical Software［C］∥Proc of the ACM SIGPLAN 2003 Conf on Programming Language Design and Implementation,2003:196207.
［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:231242.
［12］Wilson R P, Lam M S. Efficient ContextSensitive Pointer Analysis for C Programs［C］∥Proc of the ACM SIGPLAN 1995 Conf on Programming Language Design and Implementation, 1995:112.
［13］Karr M. Affine Relationships Among Variables of a Program［C］∥Proc of the Acta Inf, 1976:133151.
［14］Jeannet B,Miné A. Apron: A Library of Numerical Abstract Domains for Static Analysis［C］∥Proc of CAV’09,2009:661667.
［15］Halbwachs N,Peron M. Discovering Properties about Arrays in Simple Programs［C］∥Proc of PLDI’08, 2008:339348.
［16］Jeannet B.The Interproc Analyzer［EB/OL］.［20090625］.http://popart.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:338350.

A Static Analyzer for Numerical Programs in C and Fortran

PDF

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 0

Recommended Articles

Metrics

Comments