Advertisement

Interprocedural Shape Analysis for Recursive Programs

  • Noam Rinetzky
  • Mooly Sagiv
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2027)

Abstract

A shape-analysis algorithm statically analyzes a program to determine information about the heap-allocated data structures that the program manipulates. The results can be used to optimize, understand, debug, or verify programs. Existing algorithms are quite imprecise in the presence of recursive procedure calls. This is unfortunate, since recursion provides a natural way to manipulate linked data structures. We present a novel technique for shape analysis of recursive programs. An algorithm based on our technique has been implemented. It handles programs manipulating linked lists written in a subset of C. The algorithm is significantly more precise than existing algorithms. For example, it can verify the absence of memory leaks in many recursive programs; this is beyond the capabilities of existing algorithms.

Keywords

Operational Semantic Activation Record Predicate Symbol Unary Predicate Recursive Program 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    U. Assmann and M. Weinhardt. Interprocedural heap analysis for parallelizing imperative programs. In W. K. Giloi, S. Jahnichen, and B. D. Shriver, editors, Programming Models For Massively Parallel Computers, September 1993.Google Scholar
  2. 2.
    D.R. Chase, M. Wegman, and F. Zadeck. Analysis of pointers and structures. In SIGPLAN Conf. on Prog. Lang. Design and Impl., pages 296–310, 1990.Google Scholar
  3. 3.
    P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Symp. on Princ. of Prog. Lang., pages 269–282, New York, NY, 1979. ACM Press.Google Scholar
  4. 4.
    A. Deutsch. On determining lifetime and aliasing of dynamically allocated data in higher-order functional specifications. In Symp. on Princ. of Prog. Lang., 1990.Google Scholar
  5. 5.
    N. Dor, M. Rodeh, and M. Sagiv. Checking cleanness in linked lists. In SAS’00, Static Analysis Symposium. Springer, 2000.Google Scholar
  6. 6.
    R. Ghiya and L. Hendren. Putting pointer analysis to work. In Symp. on Princ. of Prog. Lang., New York, NY, 1998. ACM Press.Google Scholar
  7. 7.
    R. Ghiya and L.J. Hendren. Is it a tree, a dag, or a cyclic graph? In Symp. on Princ. of Prog. Lang., New York, NY, January 1996. ACM Press.Google Scholar
  8. 8.
    L. Hendren. Parallelizing Programs with Recursive Data Structures. PhD thesis, Cornell Univ., Ithaca, NY, Jan 1990.Google Scholar
  9. 9.
    L. Hendren, J. Hummel, and A. Nicolau. Abstractions for recursive pointer data structures: Improving the analysis and the transformation of imperative programs. In SIGPLAN Conf. on Prog. Lang. Design and Impl., pages 249–260, June 1992.Google Scholar
  10. 10.
    N.D. Jones and S.S. Muchnick. Flow analysis and optimization of Lisp-like structures. In S.S. Muchnick and N.D. Jones, editors, Program Flow Analysis: Theory and Applications, chapter 4. Prentice-Hall, Englewood Cliffs, NJ, 1981.Google Scholar
  11. 11.
    N.D. Jones and S.S. Muchnick. A flexible approach to interprocedural data flow analysis and programs with recursive data structures. In Symp. on Princ. of Prog. Lang., pages 66–74, New York, NY, 1982. ACM Press.Google Scholar
  12. 12.
    J.R. Larus and P.N. Hilfinger. Detecting conflicts between structure accesses. In SIGPLAN Conf. on Prog. Lang. Design and Impl., pages 21–34, 1988.Google Scholar
  13. 13.
    T. Lev-Ami and M. Sagiv. TVLA: A framework for Kleene based static analysis. In SAS’00, Static Analysis Symposium. Springer, 2000.Google Scholar
  14. 14.
    M. Sagiv, T. Reps, and R. Wilhelm. Solving shape-analysis problems in languages with destructive updating. Trans. on Prog. Lang. and Syst., 20(1):1–50, Jan 1998.CrossRefGoogle Scholar
  15. 15.
    M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. In Symp. on Princ. of Prog. Lang., 1999.Google Scholar
  16. 16.
    M. Sharir and A. Pnueli. Two approaches to interprocedural data flow analysis. In S.S. Muchnick and N.D. Jones, editors, Program Flow Analysis: Theory and Applications, chapter 7, pages 189–234. Prentice-Hall, Englewood Cliffs, NJ, 1981.Google Scholar
  17. 17.
    B. Steensgaard. Points-to analysis in almost-linear time. In Symp. on Princ. Of Prog. Lang., pages 32–41, 1996.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Noam Rinetzky
    • 1
  • Mooly Sagiv
    • 2
  1. 1.Computer Science DepartmentTechnion, Technion CityHaifaIsrael
  2. 2.Computer Sciences DepartmentTel-Aviv UniversityTel-AvivIsrael

Personalised recommendations