Solving shape-analysis problems in languages with destructive updating

ABSTRACT

This article concerns the static analysis of programs that perform destructive updating on heap-allocated storage. We give an algorithm that uses finite shape graphs to approximate conservatively the possible “shapes” that heap-allocated structures in a program can take on. For certain programs, our technique is able to determine such properties as (1) when the input to the program is a list, the output is also a list and (2) when the input to the program is a tree, the output is also a tree. For example, the method can determine that “listness” is preserved by (1) a program that performs list reversal via destructive updating of the input list and (2) a program that searches a list and splices a new element into the list. None of the previously known methods that use graphs to model the program's store are capable of determining that “listness” is preserved on these examples (or examples of similar complexity). In contrast with most previous work, our shape analysis algorithm is even accurate for certain programs that update cyclic data structures; that is, it is sometimes able to show that when the input to the program is a circular list, the output is also a circular list. For example, the shape-analysis algorithm can determine that an insertion into a circular list preserves “circular listness.”

REFERENCES

• 1: ASSMANN, W. AND WEINHARDT, M. 1993. Interprocedural heap analysis for parallelizing imperative programs. In Programming Models For Massively Parallel Computers, W. K. Giloi, S. JS~hnichen, and B. D. Shriver, Eds. IEEE Computer Society, Washington, D.C., 74-82.
• 2: 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
• 3: Jong-Deok Choi , Michael Burke , Paul Carini, Efficient flow-sensitive interprocedural computation of pointer-induced aliases and side effects, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.232-245, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158639]
• 4: 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]
• 5: DEUTSCH, t. 1992. A storeless model for aliasing and its abstractions using finite representations of right-regular equivalence relations. In Proceedings of the IEEE International Conference on Computer Languages. IEEE Computer Society, Washington, D.C., 2-13.
• 6: Alain Deutsch, Interprocedural may-alias analysis for pointers: beyond k-limiting, Proceedings of the ACM SIGPLAN 1994 conference on Programming language design and implementation, p.230-241, June 20-24, 1994, Orlando, Florida, United States
• 7: Rakesh Ghiya , Laurie J. Hendren, Is it a tree, a DAG, or a cyclic graph? A shape analysis for heap-directed pointers in C, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-15, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237724]
• 8: Nevin Charles Heintze, Set based program analysis, Carnegie Mellon University, Pittsburgh, PA, 1992
• 9: Laurie Jane Hendren, Parallelizing programs with recursive data structures, Cornell University, Ithaca, NY, 1990
• 10: HENDREN, L. AND GAO, G. 1992. Designing programming languages for analyzability: A fresh look at pointer data structures. In Proceedings of the International Conference on Computer Languages. IEEE Computer Society, Washington, D.C., 242-251.
• 11: Laurie J. Hendren , Joseph Hummell , Alexandru Nicolau, Abstractions for recursive pointer data structures: improving the analysis and transformation of imperative programs, Proceedings of the ACM SIGPLAN 1992 conference on Programming language design and implementation, p.249-260, June 15-19, 1992, San Francisco, California, United States
• 12: 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]
• 13: S. Horwitz , P. Pfeiffer , T. Reps, Dependence analysis for pointer variables, Proceedings of the ACM SIGPLAN 1989 Conference on Programming language design and implementation, p.28-40, June 19-23, 1989, Portland, Oregon, United States
• 14: JONES, N. AND MUCHNICK, S. 1981. Flow analysis and optimization of Lisp-like structures. In Program Flow Analysis: Theory and Applications, S. Muchnick and N. Jones, Eds. Prentice- Hall, Englewood Cliffs, N.J., Chapter 4, 102-131.
• 15: Neil D. Jones , Steven S. Muchnick, A flexible approach to interprocedural data flow analysis and programs with recursive data structures, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.66-74, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582161]
• 16: Donald E. Knuth, The art of computer programming, volume 1 (3rd ed.): fundamental algorithms, Addison Wesley Longman Publishing Co., Inc., Redwood City, CA, 1997
• 17: William Landi, Undecidability of static analysis, ACM Letters on Programming Languages and Systems (LOPLAS), v.1 n.4, p.323-337, Dec. 1992 [doi>10.1145/161494.161501]
• 18: William Landi , Barbara G. Ryder, Pointer-induced aliasing: a problem taxonomy, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.93-103, January 21-23, 1991, Orlando, Florida, United States [doi>10.1145/99583.99599]
• 19: James Richard Larus , Paul Hifinger, Restructuring symbolic programs for concurrent execution on multiprocessors, 1989
• 20: J. R. Larus , P. N. Hilfinger, Detecting conflicts between structure accesses, Proceedings of the ACM SIGPLAN 1988 conference on Programming Language design and Implementation, p.24-31, June 20-24, 1988, Atlanta, Georgia, United States
• 21: LINDSTROM, G. 1973. Scanning list structures without stacks or tag bits. Inf. Process. Lett. 2, 2 (June), 47-51.
• 22: MOGENSEN, T. 1988. Partially static structures in a self-applicable partial evaluator. In Partial Evaluation and Mixed Computation: Proceedings of the IFIP TC2 Workshop on Partial Evaluation and Mixed Computation (Gammel Avernaes, Denmark, Oct 18-24, 1987). North-Holland, Amsterdam, 325-347.
• 23: Torben Æ Mogensen, Separating binding times in language specifications, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.12-25, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99372]
• 24: Eugene M. Myers, A precise inter-procedural data flow algorithm, Proceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.219-230, January 26-28, 1981, Williamsburg, Virginia [doi>10.1145/567532.567556]
• 25: John Plevyak , Andrew A. Chien , Vijay Karamcheti, Analysis of Dynamic Structures for Efficient Parallel Execution, Proceedings of the 6th International Workshop on Languages and Compilers for Parallel Computing, p.37-56, August 12-14, 1993
• 26: Raghu Ramakrishnan , Divesh Srivastava , S. Sudarshan , Praveen Seshadri, Implementation of the CORAL deductive database system, Proceedings of the 1993 ACM SIGMOD international conference on Management of data, p.167-176, May 25-28, 1993, Washington, D.C., United States
• 27: G. Ramalingam, The undecidability of aliasing, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.5, p.1467-1471, Sept. 1994 [doi>10.1145/186025.186041]
• 28: Thomas Reps, Shape analysis as a generalized path problem, Proceedings of the 1995 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.1-11, June 21-23, 1995, La Jolla, California, United States [doi>10.1145/215465.215466]
• 29: REYNOLDS, J. 1968. Automatic computation of data set definitions. In Information Processing 68: Proceedings of the IFIP Congress. North-Holland, Amsterdam, 456-461.
• 30: SAGIV, ~/{., REP$, T., AND WILHELM, R. 1995. Solving shape-anMysis problems in languages with destructive updating. Tech. Rep. TR-1276, Computer Sciences Dept., Univ. of Wisconsin, Madison, Wisc. July. Available via http:////www.cs.wisc.edu//trs.html.
• 31: R. Sedgewick, Algorithms (2nd ed.), Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1988
• 32: SHARIR, ~/{. AND PNUELI, t. 1981. Two approaches to interprocedurM data flow analysis. In Program Flow Analysis: Theory and Applications, S. Muchnick and N. Jones, Eds. Prentice- Hall, Englewood Cliffs, N.J., 189-234.
• 33: Jan Stransky, A lattice for abstract interpretation of dynamic (LISP-like) structures, Information and Computation, v.101 n.1, p.70-102, Nov. 1992 [doi>10.1016/0890-5401(92)90076-R]
• 34: David S. Warren, Memoing for logic programs, Communications of the ACM, v.35 n.3, p.93-111, March 1992 [doi>10.1145/131295.131299]

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

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging
          Subjects: Symbolic execution
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Data types and structures
      D.3.4 Processors
          Subjects: Optimization

  E. Data
  E.1 DATA STRUCTURES
      Subjects: Trees; Graphs and networks; Lists, stacks, and queues
  E.2 DATA STORAGE REPRESENTATIONS
      Subjects: Linked representations

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

General Terms:
Algorithms, Languages, Theory, Verification

Keywords:
abstract interpretation, alias analysis, dataflow analysis, destructive updating, pointer analysis, shape analysis, shape graphs, static analysis