Shape analysis with inductive recursion synthesis

ABSTRACT

Separation logic with recursively defined predicates allows for concise yet precise description of the shapes of data structures. However, most uses of separation logic for program analysis rely on pre-defined recursive predicates, limiting the class of programs analyzable to those that manipulate only a priori data structures. This paper describes a general algorithm based on inductive program synthesis that automatically infers recursive shape invariants, yielding a shape analysis based on separation logic that can be applied to any program.

A key strength of separation logic is that it facilitates, via explicit expression of structural separation, local reasoning about heap where the effects of altering one part of a data structure are analyzed in isolation from the rest. The interaction between local reasoning and the global invariants given by recursive predicates is a difficult area, especially in the presence of complex internal sharing in the data structures. Existing approaches, using logic rules specifically designed for the list predicate to unfold and fold linked-lists, again require a priori knowledge about the shapes of the data structures and do not easily generalize to more complex data structures. We introduce a notion of "truncation points" in a recursive predicate, which gives rise to generic algorithms for unfolding and folding arbitrary data structures.

REFERENCES

• 1: David R. Chase , Mark Wegman , F. Kenneth Zadeck, Analysis of pointers and structures, Proceedings of the ACM SIGPLAN 1990 conference on Programming language design and implementation, p.296-310, June 1990, White Plains, New York, United States
• 2: N. D. Jones and S. S. Muchnick, "Flow analysis and optimization of Lisp-like structures," in Program Flow Analysis: Theory and Applications (S. S. Muchnick and N. D. Jones, eds.), pp. 102--131, Englewood Cliffs, NJ: Prentice-Hall, 1981.
• 3: 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
• 4: D. Distefano, P. W. O'Hearn, and H. Yang, "A local shape analysis based on separation logic," in Lecture Notes in Computer Science, vol. 3920, pp. 287--302, Springer-Verlag, 2006.
• 5: S. Magill, A. Nanevski, E. Clarke, and P. Lee, "Inferring invariants in separation logic for imperative list-processing programs," in Workshop on Semantics, Program Analysis, and Computing Environments for Memory Management (SPACE), January 2006.
• 6: O. Lee, H. Yang, and K. Yi, "Automatic verification of pointer programs using grammar-based shape analysis," in Prceedings of the 2005 European Symposium on Programming (ESOP), 2005.
• 7: Phillip D. Summers, A Methodology for LISP Program Construction from Examples, Journal of the ACM (JACM), v.24 n.1, p.161-175, Jan. 1977 [doi>10.1145/321992.322002]
• 8: U. Schmid, Inductive Synthesis of Functional Programs: Universal Planning, Folding of Finite Programs, and Schema Abstraction by Analogical Reasoning, Springer-Verlag New York, Inc., Secaucus, NJ, 2003
• 9: 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
• 10: A. Gotsman, J. Berdine, and B. Cook, "Interprocedural shape analysis with separated heap abstractions," in Proceedings of the 13th International Static Analysis Symposium (SAS), August 2006.
• 11: Noam Rinetzky , Jörg Bauer , Thomas Reps , Mooly Sagiv , Reinhard Wilhelm, A semantics for procedure local heaps and its abstractions, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.296-309, January 12-14, 2005, Long Beach, California, USA
• 12: Bolei Guo , Matthew J. Bridges , Spyridon Triantafyllis , Guilherme Ottoni , Easwaran Raman , David I. August, Practical and Accurate Low-Level Pointer Analysis, Proceedings of the international symposium on Code generation and optimization, p.291-302, March 20-23, 2005 [doi>10.1109/CGO.2005.27]
• 13: J. Berdine, C. Calcagno, and P. W. O'Hearn, "Symbolic execution with separation logic," in Lecture Notes in Computer Science, vol. 3780, pp. 52--68, Springer-Verlag, 2005.
• 14: Peter W. O'Hearn , Hongseok Yang , John C. Reynolds, Separation and information hiding, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.268-280, January 14-16, 2004, Venice, Italy
• 15: J. Berdine, C. Calcagno, and P. W. O'Hearn, "A decidable fragment of separation logic," in Lecture Notes in Computer Science, vol. 3328, pp. 97--109, Springer-Verlag, 2004.
• 16: G. Tan and A. W. Appel, "A compositional logic for control flow," in Lecture Notes in Computer Science, vol. 3855, pp. 80--94, Springer-Verlag, 2006.
• 17: 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
• 18: N. Rinetzky, M. Sagiv, and E. Yahav, "Interprocedural shape analysis for cutpoint-free programs," Tech. Rep. 26, Tel Aviv University, November 2004.
• 19: C. Calcagno, D. Distefano, P. W. O'Hearn, and H. Yang, "Beyong reachability: Shape abstraction in the presence of pointer arithmeetic," in Lecture Notes in Computer Science, vol. 4134, pp. 182--203, Springer-Verlag, 2006.
• 20: A. Loginov, T. Reps, and M. Sagiv, "Abstraction refinement via inductive learning," in Proceedings of the 17th International Conference on Computer Aided Verification, pp. 519--533, 2005.

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: Invariants

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Logics of programs
      F.3.2 Semantics of Programming Languages
          Subjects: Program analysis

General Terms:
Languages, Theory

Keywords:
artificial intelligence, inductive recursion synthesis, loop invariant inference, separation logic, shape analysis