Heap analysis in the presence of collection libraries

ABSTRACT

Memory analysis techniques have become sophisticated enough to model, with a high degree of accuracy, the manipulation of simple memory structures (finite structures, single/double linked lists and trees). However, modern programming languages provide extensive library support including a wide range of generic collection objects that make use of complex internal data structures. While these data structures ensure that the collections are efficient, often these representations cannot be effectively modeled by existing methods (either due to excessive analysis runtime or due to the inability to represent the required information). This paper presents a method to represent collections using an abstraction of their semantics. The construction of the abstract semantics for the collection objects is done in a manner that allows individual elements in the collections to be identified. Our construction also supports iterators over the collections and is able to model the position of the iterators with respect to the elements in the collection. By ordering the contents of the collection based on the iterator position, the model can represent a notion of progress when iteratively manipulating the contents of a collection. These features allow strong updates to the individual elements in the collection as well as strong updates over the collections themselves.

REFERENCES

• 1: Francisco Bueno , Maria J. García de la Banda , Manuel V. Hermenegildo , Kim Marriott , German Puebla , Peter J. Stuckey, A Model for Inter-module Analysis and Optimizing Compilation, Selected Papers form the 10th International Workshop on Logic Based Program Synthesis and Transformation, p.86-102, July 24-28, 2000
• 2: Brendon Cahoon , Kathryn S. McKinley, Data Flow Analysis for Software Prefetching Linked Data Structures in Java, Proceedings of the 2001 International Conference on Parallel Architectures and Compilation Techniques, p.280-291, September 08-12, 2001
• 3: 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
• 4: Michael Codish , Saumya K. Debray , Roberto Giacobazzi, Compositional analysis of modular logic programs, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.451-464, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158703]
• 5: Rakesh Ghiya , Laurie J. Hendren , Yingchun Zhu, Detecting Parallelism in C Programs with Recursive Darta Structures, Proceedings of the 7th International Conference on Compiler Construction, p.159-173, March 28-April 04, 1998
• 6: 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
• 7: Brian Hackett , Radu Rugina, Region-based shape analysis with tracked locations, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.310-323, January 12-14, 2005, Long Beach, California, USA
• 8: L. J. Hendren , A. Nicolau, Parallelizing Programs with Recursive Data Structures, IEEE Transactions on Parallel and Distributed Systems, v.1 n.1, p.35-47, January 1990 [doi>10.1109/71.80123]
• 9: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar, Permissive interfaces, Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering, September 05-09, 2005, Lisbon, Portugal
• 10: Neil D. Jones , Steven S. Muchnick, Flow analysis and optimization of LISP-like structures, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.244-256, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567776]
• 11: Viktor Kuncak , Patrick Lam , Karen Zee , Martin C. Rinard, Modular Pluggable Analyses for Data Structure Consistency, IEEE Transactions on Software Engineering, v.32 n.12, p.988-1005, December 2006 [doi>10.1109/TSE.2006.125]
• 12: T. Lev-Ami, N. Immerman, and S. Sagiv. Abstraction for shape analysis with fast and precise transformers. In CAV, 2006.
• 13: M. Marron, D. Kapur, D. Stefanovic, and M. Hermenegildo. A static heap analysis for shape and connectivity. In LCPC, 2006.
• 14: Atanas Rountev , Barbara G. Ryder, Points-to and Side-Effect Analyses for Programs Built with Precompiled Libraries, Proceedings of the 10th International Conference on Compiler Construction, p.20-36, April 02-06, 2001
• 15: Mooly Sagiv , Thomas Reps , Reinhard Wilhelm, Solving shape-analysis problems in languages with destructive updating, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.16-31, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237725]
• 16: Mooly Sagiv , Thomas Reps , Reinhard Wilhelm, Parametric shape analysis via 3-valued logic, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.105-118, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292552]
• 17: 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
• 18: Craig B. Zilles, Benchmark health considered harmful, ACM SIGARCH Computer Architecture News, v.29 n.3, p.4-5, June 2001 [doi>10.1145/503205.503206]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Program analysis

General Terms:
Languages, Performance, Verification

Keywords:
collection library, shape analysis, static analysis