Relational inductive shape analysis

ABSTRACT

Shape analyses are concerned with precise abstractions of the heap to capture detailed structural properties. To do so, they need to build and decompose summaries of disjoint memory regions. Unfortunately, many data structure invariants require relations be tracked across disjoint regions, such as intricate numerical data invariants or structural invariants concerning back and cross pointers. In this paper, we identify issues inherent to analyzing relational structures and design an abstract domain that is parameterized both by an abstract domain for pure data properties and by user-supplied specifications of the data structure invariants to check. Particularly, it supports hybrid invariants about shape and data and features a generic mechanism for materializing summaries at the beginning, middle, or end of inductive structures. Around this domain, we build a shape analysis whose interesting components include a pre-analysis on the user-supplied specifications that guides the abstract interpretation and a widening operator over the combined shape and data domain. We then demonstrate our techniques on the proof of preservation of the red-black tree invariants during insertion.

REFERENCES

• 1: Gilad Arnold. Specialized 3-valued logic shape analysis using structure-based refinement and loose embedding. In Static Analysis (SAS), 2006.
• 2: Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O'Hearn, Thomas Wies, and Hongseok Yang. Shape analysis for composite data structures. In Computer-Aided Verification (CAV), 2007.
• 3: Bor-Yuh Evan Chang, Xavier Rival, and George C. Necula. Shape analysis with structural invariant checkers. In Static Analysis (SAS), 2007.
• 4: Shaunak Chatterjee, Shuvendu K. Lahiri, Shaz Qadeer, and Zvonimir Rakamaric. A reachability predicate for analyzing low-level software. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2007.
• 5: Sigmund Cherem and Radu Rugina. Maintaining doubly-linked list invariants in shape analysis with local reasoning. In Verification, Model Checking, and Abstract Interpretation (VMCAI), 2007.
• 6: Patrick Cousot. Verification by abstract interpretation. In Verification: Theory and Practice, 2003.
• 7: 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]
• 8: Dino Distefano, Peter W. O'Hearn, and Hongseok Yang. A local shape analysis based on separation logic. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2006.
• 9: Denis Gopan , Thomas Reps , Mooly Sagiv, A framework for numeric analysis of array operations, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.338-350, January 12-14, 2005, Long Beach, California, USA
• 10: Sumit Gulwani and Ashish Tiwari. An abstract domain for analyzing heapmanipulating low-level software. In Computer-Aided Verification (CAV), 2007.
• 11: Bolei Guo , Neil Vachharajani , David I. August, Shape analysis with inductive recursion synthesis, Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
• 12: Michael Karr. Affine relationships among variables of a program. Acta Inf., 6, 1976.
• 13: Oukseh Lee, Hongseok Yang, and Kwangkeun Yi. Automatic verification of pointer programs using grammar-based shape analysis. In European Symposium on Programming (ESOP), 2005.
• 14: Tal Lev-Ami , Thomas Reps , Mooly Sagiv , Reinhard Wilhelm, Putting static analysis to work for verification: A case study, Proceedings of the 2000 ACM SIGSOFT international symposium on Software testing and analysis, p.26-38, August 21-24, 2000, Portland, Oregon, United States
• 15: Stephen Magill, Josh Berdine, Edmund Clarke, and Byron Cook. Arithmetic strengthening for separation logic based shape analyses. In Static Analysis (SAS), 2007.
• 16: Scott McPeak and George C. Necula. Data structure specifications via local equality axioms. In Computer-Aided Verification (CAV), 2005.
• 17: Antoine Miné, The octagon abstract domain, Higher-Order and Symbolic Computation, v.19 n.1, p.31-100, March 2006 [doi>10.1007/s10990-006-8609-1]
• 18: Anders Møller , Michael I. Schwartzbach, The pointer assertion logic engine, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.221-231, June 2001, Snowbird, Utah, United States
• 19: Huu Hai Nguyen, Cristina David, Shengchao Qin, and Wei-Ngan Chin. Automated verification of shape and size properties via separation logic. In Verification, Model Checking, and Abstract Interpretation (VMCAI), 2007.
• 20: John C. Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, p.55-74, July 22-25, 2002
• 21: Radu Rugina. Quantitative shape analysis. In Static Analysis (SAS), 2004.
• 22: 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]
• 23: Arnaud Venet, Abstract Cofibered Domains: Application to the Alias Analysis of Untyped Programs, Proceedings of the Third International Symposium on Static Analysis, p.366-382, September 24-26, 1996

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

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

General Terms:
Languages, Verification

Keywords:
heap analysis, inductive definitions, materialization, separation logic, shape analysis, symbolic abstract domain