Automatic modular abstractions for linear constraints

ABSTRACT

We propose a method for automatically generating abstract transformers for static analysis by abstract interpretation. The method focuses on linear constraints on programs operating on rational, real or floating-point variables and containing linear assignments and tests.

In addition to loop-free code, the same method also applies for obtaining least fixed points as functions of the precondition, which permits the analysis of loops and recursive functions. Our algorithms are based on new quantifier elimination and symbolic manipulation techniques.

Given the specification of an abstract domain, and a program block, our method automatically outputs an implementation of the corresponding abstract transformer. It is thus a form of program transformation.

The motivation of our work is data-flow synchronous programming languages, used for building control-command embedded systems, but it also applies to imperative and functional programming.

REFERENCES

• 1: Roberto Bagnara, Patricia M. Hill, Elena Mazzi, and Enea Zaffanella. Widening operators for weakly-relational numeric abstractions. In Static Analysis (SAS), volume 3672 of LNCS, pages 3--18. Springer, 2005. DOI: 10.1007/11547662_3.
• 2: Roberto Bagnara , Patricia M. Hill , Elisa Ricci , Enea Zaffanella, Precise widening operators for convex polyhedra, Science of Computer Programming, v.58 n.1-2, p.28-56, October 2005 [doi>10.1016/j.scico.2005.02.003]
• 3: Roberto Bagnara, Patricia M. Hill, and Enea Zaffanella. The Parma Polyhedra Library, version 0.9, 2006. URL http://www.cs.unipr.it/ppl.
• 4: Gogul Balakrishnan and Thomas Reps. Analyzing memory accesses in x86 executables. In Compiler Construction (CC), volume 2985 of LNCS, pages 5--23. Springer, 2004. DOI: 10.1007/b95956.
• 5: Bruno Blanchet , Patrick Cousot , Radhia Cousot , Jérôme Feret , Laurent Mauborgne , Antoine Miné , David Monniaux , Xavier Rival, Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software, The essence of computation: complexity, analysis, transformation, Springer-Verlag New York, Inc., New York, NY, 2002
• 6: Bruno Blanchet , Patrick Cousot , Radhia Cousot , Jérome Feret , Laurent Mauborgne , Antoine Miné , David Monniaux , Xavier Rival, A static analyzer for large safety-critical software, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 7: François Bourdoncle. Sémantique des langages impératifs d'ordre supérieur et interprétation abstraite. PhD thesis, École polytechnique, Palaiseau, 1992.
• 8: Aaron R. Bradley , Zohar Manna, The Calculus of Computation: Decision Procedures with Applications to Verification, Springer-Verlag New York, Inc., Secaucus, NJ, 2007
• 9: P. Caspi , D. Pilaud , N. Halbwachs , J. A. Plaice, LUSTRE: a declarative language for real-time programming, Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.178-188, January 21-23, 1987, Munich, West Germany [doi>10.1145/41625.41641]
• 10: Paul Caspi , Adrian Curic , Aude Maignan , Christos Sofronis , Stavros Tripakis , Peter Niebert, From simulink to SCADE/lustre to TTA: a layered approach for distributed embedded applications, ACM SIGPLAN Notices, v.38 n.7, July 2003
• 11: CAV05. Computer Aided Verification (CAV), number 4590 in LNCS, 2005. Springer. DOI: 10.1007/b138445.
• 12: Robert Clarisó and Jordi Cortadella. The octahedron abstract domain. In Static Analysis (SAS), number 3148 in LNCS, pages 312--327. Springer, 2004.
• 13: Michael Colon, Sriram Sankaranarayanan, and Henny Sipma. Linear invariant generation using non-linear constraint solving. Linear invariant generation using non-linear constraint solving. pages 420--433. Springer, 2003.
• 14: Patrick Cousot. Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. In VMCAI_2005, pages 1--24. DOI: 10.1007/b105073.
• 15: Patrick Cousot , Rahida Cousot, Abstract interpretation and application to logic programs, Journal of Logic Programming, v.13 n.2-3, p.103-179, July 1992 [doi>10.1016/0743-1066(92)90030-7]
• 16: Patrick Cousot and Radhia Cousot. Static determination of dynamic properties of programs. In Proceedings of the Second International Symposium on Programming, pages 106--130. Dunod, Paris, France, 1976.
• 17: Patrick Cousot , Nicolas Halbwachs, Automatic discovery of linear restraints among variables of a program, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.84-96, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512770]
• 18: Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. The ASTRÉE analyzer. In Programming Languages and Systems (ESOP), number 3444 in LNCS, pages 21--30, 2005.
• 19: ESOP07. Programming Languages and Systems (ESOP), volume 4421 of LNCS, 2007. DOI: 10.1007/978-3-540-71316-6.
• 20: Jeanne Ferrante and Charles Rackoff. A decision procedure for the first order theory of real addition with SIAM Journal of Computation, 4 (1): 69--76, March 1975.
• 21: Michael J. Fischer and Michael O. Rabin. Super-exponential complexity of Presburger arithmetic. In Complexity of Computation, number 7 in SIAM-AMS proceedings, pages 27--42. American Mathematical Society, 1974.
• 22: Stéphane Gaubert, Éric Goubault, Ankur Taly, and Sarah Zennou. Static analysis by policy iteration on relational domains. In ESOP_2007, pages 237--252. DOI: 10.1007/978-3-540-71316-6.
• 23: Thomas Gawlitza and Helmut Seidl. Precise fixpoint computation through strategy iteration. In ESOP_2007, pages 300--315. DOI: 10.1007/978-3-540-71316-6_21.
• 24: Laure Gonnord and Nicolas Halbwachs. Combining widening and acceleration in linear relation analysis. In Static Analysis (SAS), volume 4134 of LNCS, pages 144--160. Springer, 2006. DOI: 10.1007/11823230_10.
• 25: Denis Gopan and Thomas W. Reps. Lookahead widening. In Computer Aided Verification (CAV), volume 4144 of LNCS, pages 452--466. Springer, 2006. DOI: 10.1007/11817963_41.
• 26: Denis Gopan and Thomas W. Reps. Low-level library analysis and summarization. In Computer Aided Verification (CAV), volume 4590 of LNCS, pages 68--81. Springer, 2007. DOI: 10.1007/978-3-540-73368-3_10.
• 27: Sumit Gulwani , Saurabh Srivastava , Ramarathnam Venkatesan, Program analysis as constraint solving, Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation, June 07-13, 2008, Tucson, AZ, USA
• 28: Nicolas Halbwachs. Détermination automatique de relations linéaires vérifiées par les variables d'un programme. PhD thesis, Université scientifique et médicale de Grenoble, 1979.
• 29: IEEE standard for Binary floating-point arithmetic for microprocessor systems. IEEE, 1985. ANSI/IEEE Std 754--1985.
• 30: B. Jeannet, Dynamic Partitioning in Linear Relation Analysis: Application to the Verification of Reactive Systems, Formal Methods in System Design, v.23 n.1, p.5-37, July 2003 [doi>10.1023/A:1024480913162]
• 31: Deepak Kapur. Automatically generating loop invariants using quantifier elimination. In ACA (Applications of Computer Algebra), 2004.
• 32: Akash Lal, Gogul Balakrishnan, and Thomas Reps. Extended weighted pushdown systems. In CAV_2005, pages 343--357. DOI: 10.1007/11817963_32.
• 33: Francesco Logozzo and Manuel Fähndrich. On the relative completeness of bytecode analysis versus source code analysis. In Compiler Construction (CC), volume 4959 of LNCS, pages 197--212. Springer, 2008. DOI: 10.1007/978-3-540-78791-4_14.
• 34: Zohar Manna and John McCarthy. Properties of programs and partial function logic. In Machine Intelligence, 5, pages 27--38. Edinburgh University
• 35: Zohar Manna , Amir Pnueli, Formalization of Properties of Functional Programs, Journal of the ACM (JACM), v.17 n.3, p.555-569, July 1970 [doi>10.1145/321592.321606]
• 36: Ferdinand}DBLP:conf/cc/MartinAWF98 Florian Martin, Martin Alt, Reinhard Wilhelm, and Christian Ferdinand. Analysis of loops. In Compiler Construction (CC), volume 1383 of LNCS, pages 80--94. Springer, 1998.
• 37: Antoine Miné, The Octagon Abstract Domain, Proceedings of the Eighth Working Conference on Reverse Engineering (WCRE'01), p.310, October 02-05, 2001
• 38: Relational abstract domains for the detection of floating-point run-time errors. In Programming Languages and Systems (ESOP), volume 2986 of LNCS, pages 3--17. Springer, 2004.
• 39: David Monniaux. Compositional analysis of floating-point linear numerical filters. In CAV_2005, pages 199--212. DOI: 10.1007/b138445.
• 40: David Monniaux, A Quantifier Elimination Algorithm for Linear Real Arithmetic, Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, November 22-27, 2008, Doha, Qatar [doi>10.1007/978-3-540-89439-1_18]
• 41: David Monniaux. Optimal abstraction on real-valued programs. In Static analysis (SAS), number 4634 in LNCS, pages 104--120. Springer, 2007. DOI: 10.1007/978-3-540-74061-2_7.
• 42: David Monniaux, The pitfalls of verifying floating-point computations, ACM Transactions on Programming Languages and Systems (TOPLAS), v.30 n.3, p.1-41, May 2008 [doi>10.1145/1353445.1353446]
• 43: George C. Necula , Scott McPeak , Shree Prakash Rahul , Westley Weimer, CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs, Proceedings of the 11th International Conference on Compiler Construction, p.213-228, April 08-12, 2002
• 44: Radu Rugina , Martin C. Rinard, Symbolic bounds analysis of pointers, array indices, and accessed memory regions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.2, p.185-235, March 2005 [doi>10.1145/1057387.1057388]
• 45: Sriram Sankaranarayanan, Henny Sipma, and Zohar Manna. Constraint-based linear-relations analysis. In SAS, number 3148 in LNCS, pages 53--68. Springer, 2004.
• 46: Sriram Sankaranarayanan, Henny Sipma, and Zohar Manna. Scalable analysis of linear systems using mathematical programming. In VMCAI_2005, pages 21--47. DOI: 10.1007/b105073.
• 47: Helmut Seidl, Andrea Flexeder, and Michael Petter. Interprocedurally analysing linear inequality relations. In ESOP_2007, pages 284--299. DOI: 10.1007/978-3-540-71316-6_20.
• 48: Micha Sharir and Amir Pnueli. Two approaches to inter-procedural data-flow analysis. In Program Flow Analysis: Theory and Application. Prentice-Hall, 1981.
• 49: VMCAI05. Verification, Model Checking and Abstract Interpretation (VMCAI), number 3385 in LNCS, 2005. Springer. DOI: 10.1007/b105073.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Pre- and post-conditions; Invariants
      F.3.2 Semantics of Programming Languages
          Subjects: Program analysis
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Mechanical theorem proving

General Terms:
Algorithms, Languages, Theory, Verification

Keywords:
abstract interpretation, linear inequalities, program transformation, quantifier elimination