Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics

ABSTRACT

We propose a memory abstraction able to lift existing numerical static analyses to C programs containing union types, pointer casts, and arbitrary pointer arithmetics. Our framework is that of a combined points-to and data-value analysis. We abstract the contents of compound variables in a field-sensitive way, whether these fields contain numeric or pointer values, and use stock numerical abstract domains to find an overapproximation of all possible memory states---with the ability to discover relationships between variables. A main novelty of our approach is the dynamic mapping scheme we use to associate a flat collection of abstract cells of scalar type to the set of accessed memory locations, while taking care of byte-level aliases---i.e., C variables with incompatible types allocated in overlapping memory locations. We do not rely on static type information which can be misleading in C programs as it does not account for all the uses a memory zone may be put to.Our work was incorporated within the Astrée static analyzer that checks for the absence of run-time-errors in embedded, safety-critical, numerical-intensive software. It replaces the former memory domain limited to well-typed, union-free, pointer-cast free data-structures. Early results demonstrate that this abstraction allows analyzing a larger class of C programs, without much cost overhead.

REFERENCES

• 1: AT&T and The Santa Cruz Operation Inc. System V application binary interface, 1997.
• 2: G. Balakrishnan and T. Reps. Analyzing memory accesses in x86 executables. In CC 2004, number 2985 in LNCS, pages 5--23. Springer, 2004.
• 3: 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
• 4: P. Cousot. Verification by abstract interpretation. In Verification: Theory and Practice: Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday, volume 2772, pages 243--268. Springer, 2003.
• 5: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 6: P. Cousot and R. Cousot. Abstract interpretation frameworks. Journal of Logic and Computation, 2(4):511--547, 1992.
• 7: Nurit Dor , Michael Rodeh , Shmuel Sagiv, Cleanness Checking of String Manipulations in C Programs via Integer Analysis, Proceedings of the 8th International Symposium on Static Analysis, p.194-212, July 16-18, 2001
• 8: J.-L. Lions et al. ARIANE 5, flight 501 failure, report by the inquiry board, 1996.
• 9: J. Feret. Static analysis of digital filters. In ESOP'04, volume 2986 of LNCS. Springer, 2004.
• 10: D. Gopan, F. DiMaio, N. Dor, T. Reps, and M. Sagiv. Numeric domains with summarized dimensions. In TACAS 2004, LNCS, pages 512--529. Springer, 2004.
• 11: P. Granger. Static analysis of arithmetical congruences. In International Journal of Computer Mathematics, volume 30, pages 165--190, 1989.
• 12: Michael Hind, Pointer analysis: haven't we solved this problem yet?, Proceedings of the 2001 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, p.54-61, June 2001, Snowbird, Utah, United States [doi>10.1145/379605.379665]
• 13: IEEE Computer Society. IEEE standard for binary floating-point arithmetic. Technical report, ANSI/IEEE Std. 745-1985, 1985.
• 14: International Organisation for Standardization. Programming languages -- C. Technical report, ISO/IEC 9899:1999, 1999.
• 15: Antoine Miné, The Octagon Abstract Domain, Proceedings of the Eighth Working Conference on Reverse Engineering (WCRE'01), p.310, October 02-05, 2001
• 16: A. Miné. Relational abstract domains for the detection of floating-point run-time errors. In ESOP'04, volume 2986 of LNCS, pages 3--17. Springer, 2004.
• 17: George C. Necula , Scott McPeak , Westley Weimer, CCured: type-safe retrofitting of legacy code, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.128-139, January 16-18, 2002, Portland, Oregon
• 18: A. Pioli and M. Hind. Combining interprocedural pointer analysis and conditional constant propagation. Technical Report 99-103, IBM, 1999.
• 19: Radu Rugina , Martin Rinard, Symbolic bounds analysis of pointers, array indices, and accessed memory regions, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.182-195, June 18-21, 2000, Vancouver, British Columbia, Canada
• 20: Mooly Sagiv , Thomas Reps , Reinhard Wilhelm, Parametric shape analysis via 3-valued logic, ACM Transactions on Programming Languages and Systems (TOPLAS), v.24 n.3, p.217-298, May 2002 [doi>10.1145/514188.514190]
• 21: Michael Siff , Satish Chandra , Thomas Ball , Krishna Kunchithapadam , Thomas Reps, Coping with type casts in C, Proceedings of the 7th European software engineering conference held jointly with the 7th ACM SIGSOFT international symposium on Foundations of software engineering, p.180-198, September 06-10, 1999, Toulouse, France
• 22: Bjarne Steensgaard, Points-to Analysis by Type Inference of Programs with Structures and Unions, Proceedings of the 6th International Conference on Compiler Construction, p.136-150, April 24-26, 1996
• 23: A. Venet. A scalable nonuniform pointer analysis for embedded programs. In SAS'04, number 3148 in LNCS, pages 149--164. Springer, 2004.
• 24: John Whaley , Monica S. Lam, An Efficient Inclusion-Based Points-To Analysis for Strictly-Typed Languages, Proceedings of the 9th International Symposium on Static Analysis, p.180-195, September 17-20, 2002
• 25: Robert P. Wilson , Monica S. Lam, Efficient context-sensitive pointer analysis for C programs, Proceedings of the ACM SIGPLAN 1995 conference on Programming language design and implementation, p.1-12, June 18-21, 1995, La Jolla, California, United States
• 26: S. Yong and S. Horwitz. Pointer-range analysis. In SAS'04, number 3148 in LNCS, pages 133--148. Springer, 2004.
• 27: Suan Hsi Yong , Susan Horwitz , Thomas Reps, Pointer analysis for programs with structures and casting, Proceedings of the ACM SIGPLAN 1999 conference on Programming language design and implementation, p.91-103, May 01-04, 1999, Atlanta, Georgia, United States

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Assertion checkers

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Validation; Formal methods
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification; Assertions; Invariants
      F.3.2 Semantics of Programming Languages
          Subjects: Program analysis

General Terms:
Experimentation, Languages, Reliability, Theory, Verification

Keywords:
abstract interpretation, critical software, numerical analysis, points-to analysis