Berhard Scholz
ABSTRACT
It is well accepted that pointers are a common source of memory anomalies such as loosing references to dynamic records without deallocating them (also known as memory leaks). This paper presents a novel pointer analysis framework that detects memory leaks by statically analyzing the behavior of programs.
Our approach is based on symbolic evaluation of programs. Symbolic evaluation is an advanced static symbolic analysis that is centered around symbolic variable values, assumptions about and constraints between variable values, and control flow information (path conditions). As part of symbolic evaluation we introduce a new symbolic heap algebra for modeling heap operations. Predicates — defined over the program's input — are derived which allow to detect memory leaks. Our approach goes beyond previous work in the field of statically detecting memory leaks by considering also path conditions which increases the accuracy of our results, symbolically modeling heap data structures and heap operations. Examples are used to illustrate the effectiveness of our approach.
- 1.T. Austin, S. Breach, and G. Sohi. Efficient detection of all pointer and array access errors. In Conference on Programming Language Design and Implementation, Jun. 1994.]] Google Scholar
Digital Library
- 2.J. Blieberger, B. Burgstaller, and B. Scholz. Interprocedural Symbolic Evaluation of Ada Programs with Aliases. In Ada-Europe'99 International Conference on Reliable So.ware Technologies, pages 136-145, Santander, Spain, June 1999.]] Google ScholarDigital Library
- 3.J. Blieberger, T. Fahringer, and B. Scholz. Symbolic cache analysis for real-time systems. To appear in Real- Time Systems Journal., 1999.]] Google ScholarDigital Library
- 4.M. Burke, P. Carini, J.-D. Choi, and M. Hind. Flowinsensitive interprocedural alias analysis in the presence of pointers. In K. Pingali, U. Banerjee, D. Gelernter, A. Nicolau, and D. Padua, editors, Proceedings of the 7th International Workshop on Languages and Compilers for Parallel Computing, Lecture Notes in Computer Science, pages 234-250, ithaca, New York, Aug. 8-10, 1994. Springer-Verlag.]] Google ScholarDigital Library
- 5.A. Deutsch. Semantic models and abstract interpretation techniques for inductive data structures and pointers. In Symposium on Partial Evaluation and Semantics-Based Program Manipulation, June 1995.]] Google ScholarDigital Library
- 6.E. Dijkstra. A discipline of programming. Prentice Hall, New Jersey, 1976.]] Google ScholarDigital Library
- 7.N. Dot, M. Rodeh, and M. Sagiv. Detecting memory errors via static pointer analysis. In Workshop on Program Analysis for Software Tools and Engineering PARLE'98. ACM Press, 1998.]]Google Scholar
- 8.M. Emami, R. Ghiya, and L. J. Hendren. Contextsensitive interprocedural points-to analysis in the presence of function pointers. A CM SIGPLAN Notices, 29(6):242-256, June 1994.]] Google ScholarDigital Library
- 9.D. Evans. Static detection of dynamic memory errors. In SIGPLAN Conference on Programming Language Design and Implementation (PLDI '96), May 1996.]] Google ScholarDigital Library
- 10.T. Fahringer. Efficient Symbolic Analysis for Parallelizing Compilers and Performance Estimators. Journal of Supercomputing, Kluwer Academic Publishers, 12(3), 1998.]] Google ScholarDigital Library
- 11.T. Fahringer. Symbolic Analysis Techniques for Program Parallelization. Journal of Future Generation Computer Systems, Elsevier Science, North-Holland, 13(1997/98):385-396, March 1998.]] Google ScholarDigital Library
- 12.T. Fahringer and B. Scholz. Symbolic Evaluation for Parallelizing Compilers. In Proc. of the A CM International Conference on Supercomputing, July 1997.]] Google ScholarDigital Library
- 13.T. Fahringer and B. Scholz. A unified symbolic evaluation framework for parallelizing compilers. Submitted, http://ww-w.par.univie.ac.at/~tf/papers/ symbolic/symbol_eval, ps, 1998.]]Google Scholar
- 14.P. Fradet, R. Caugne, and D. L. M@tayer. Static detection of pointer errors: An axiomatisation and a checking algorithm. In H. R. Nielson, editor, Programming Languages and Systems--ESOP'96, 6th European Symposium on Programming, volume 1058 of LNCS, LinkSping, Sweden, 22-24 Apr. 1996. Springer.]] Google ScholarDigital Library
- 15.1%. Ghiya and L. Hendren. Is it a tree, a DAG, or a cyclic graph? A shape analysis for heap-directed pointers in C. In Symposium on Principles of Programming Languages. ACM Press, Jan. 1996.]] Google ScholarDigital Library
- 16.R. Ghiya and L. Hendren. Putting pointer analysis to work. In Symposium on Principles of Programming Languages, Jan. 1998.]] Google ScholarDigital Library
- 17.R. Ghiya and L. J. Hendren. Connection analysis: A practical interprocedural heap analysis for C. International Journal of Parallel Programming, 24(6):547-578, Dec. 1996.]]Google ScholarDigital Library
- 18.L. Hendren and A. Nicolau. Parallelizing programs with recursive data structures. IEEE Transactions on Parallel and Distributed Systems, 1(1):35-47, jan. 1990.]] Google ScholarDigital Library
- 19.J. L. Jensen, M. E. Jorgensen, M. I. Schwartzbach, and N. Klarlund. Automatic verification of pointer programs using monadic second-order logic. In Proceedings of the A CM SIGPLAN Conference on Programming Language Design and Implementation (PLDI-97), volume 32, 5 of A CM SIGPLAN Notices, pages 226-234, New York, June15-18 1997. ACM Press.]] Google ScholarDigital Library
- 20.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, pages 102-131. Englewood Cliffs, N.J.: Prentice-Hall, 1981.]]Google Scholar
- 21.W. Landi and B. G. Ryder. Safe approximate algorithm for interprocedural pointer aliasing. A CM SIGPLAN Notices, 27(7):235-248, 1992.]] Google ScholarDigital Library
- 22.M. Sagiv, T. Reps, and R. Wilhelm. Solving shapeanalysis problems in languages with destructive updating. In Symposium on Principles of Programming Languages, St. Petersburg Beach, FL, Jan.Jan. 1996.]] Google ScholarDigital Library
- 23.M. Sagiv, T. Reps, and 1%. Wilhelm. Solving shapeanalysis problems in languages with destructive updating. A CM Transactions on Programming Languages and Systems, 20(1):1-50, Jan. 1998.]] Google ScholarDigital Library
- 24.R. Tennent. Denotational semantics of programming languages. Communication o} the A CM, 19(8), Aug. 1976.]] Google ScholarDigital Library
- 25.R. P. Wilson and M. S. Lain. Efficient context-sensitive pointer analysis for C programs. In Proceedings of the ACM SIGPLAN'95 Con}erenc~ on Programmin9 Language Design and Implementation (PLDI), La Jolla, California, 18-21 June 1995.]] Google ScholarDigital Library
Index Terms
- Symbolic pointer analysis for detecting memory leaks
Recommendations
Symbolic pointer analysis for detecting memory leaks
It is well accepted that pointers are a common source of memory anomalies such as loosing references to dynamic records without deallocating them (also known as memory leaks). This paper presents a novel pointer analysis framework that detects memory ...
Detecting Memory Leaks Statically with Full-Sparse Value-Flow Analysis
We introduce a static detector, Saber, for detecting memory leaks in C programs. Leveraging recent advances on sparse pointer analysis, Saber is the first to use a full-sparse value-flow analysis for detecting memory leaks statically. Saber tracks the ...
Detecting memory errors via static pointer analysis (preliminary experience)
PASTE '98: Proceedings of the 1998 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineeringPrograms which manipulate pointers are hard to debug. Pointer analysis algorithms (originally aimed at optimizing compilers) may provide some remedy by identifying potential errors such as dereferencing NULL pointers by statically analyzing the behavior ...
Comments