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.
Partially supported by the Technion and the Israeli Academy of Science.
Chapter PDF
Similar content being viewed by others
Keywords
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
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.
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.
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.
A. Deutsch. On determining lifetime and aliasing of dynamically allocated data in higher-order functional specifications. In Symp. on Princ. of Prog. Lang., 1990.
N. Dor, M. Rodeh, and M. Sagiv. Checking cleanness in linked lists. In SAS’00, Static Analysis Symposium. Springer, 2000.
R. Ghiya and L. Hendren. Putting pointer analysis to work. In Symp. on Princ. of Prog. Lang., New York, NY, 1998. ACM Press.
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.
L. Hendren. Parallelizing Programs with Recursive Data Structures. PhD thesis, Cornell Univ., Ithaca, NY, Jan 1990.
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.
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.
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.
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.
T. Lev-Ami and M. Sagiv. TVLA: A framework for Kleene based static analysis. In SAS’00, Static Analysis Symposium. Springer, 2000.
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.
M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. In Symp. on Princ. of Prog. Lang., 1999.
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.
B. Steensgaard. Points-to analysis in almost-linear time. In Symp. on Princ. Of Prog. Lang., pages 32–41, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Rinetzky, N., Sagiv, M. (2001). Interprocedural Shape Analysis for Recursive Programs. In: Wilhelm, R. (eds) Compiler Construction. CC 2001. Lecture Notes in Computer Science, vol 2027. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45306-7_10
Download citation
DOI: https://doi.org/10.1007/3-540-45306-7_10
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41861-0
Online ISBN: 978-3-540-45306-2
eBook Packages: Springer Book Archive