Abstract
We present a novel leak detection algorithm. To prove the absence of a memory leak, the algorithm assumes its presence and runs a backward heap analysis to disprove this assumption. We have implemented this approach in a memory leak analysis tool and used it to analyze several routines that manipulate linked lists and trees. Because of the reverse nature of the algorithm, the analysis can locally reason about the absence of memory leaks. We have also used the tool as a scalable, but unsound leak detector for C programs. The tool has found several bugs in larger programs from the SPEC2000 suite.
This work was supported by NSF grant CNS-0406345, DARPA grant FA8750-04-2-0011, and AFOSR grant F9550-06-1-0244 .
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Dor, N., Rodeh, M., Sagiv, M.: Checking cleanness in linked lists. In: Proceedings of the 8th International Static Analysis Symposium, Santa Barbara, CA (2000)
Shaham, R., Kolodner, E.K., Sagiv, M.: Automatic removal of array memory leaks in java. In: Watt, D.A. (ed.) CC 2000. LNCS, vol. 1781, p. 50. Springer, Heidelberg (2000)
Heine, D., Lam, M.: A practical flow-sensitive and context-sensitive C and C++ memory leak detector. In: Proceedings of the SIGPLAN 2003 Conference on Program Language Design and Implementation, San Diego, CA (2003)
Hackett, B., Rugina, R.: Shape analysis with tracked locations. In: Proceedings of the 32nd Annual ACM Symposium on the Principles of Programming Languages, Long Beach, CA (2005)
Xie, Y., Aiken, A.: Context- and path-sensitive memory leak detection. In: ACM SIGSOFT Symposium on the Foundations of Software Engineering, Lisbon, Portugal (2005)
Heine, D., Lam, M.: A practical flow-sensitive and context-sensitive C and C++ memory leak detector. In: Proceedings of PLDI, San Diego, CA (2003)
Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Transactions on Programming Languages and Systems 24(3) (2002)
Steensgaard, B.: Points-to analysis in almost linear time. In: Proceedings of the 23rd Annual ACM Symposium on the Principles of Programming Languages, St. Petersburg Beach, FL (1996)
Andersen, L.O.: Program Analysis and Specialization for the C Programming Language. PhD thesis, DIKU, University of Copenhagen (1994)
Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. In: Muchnick, S., Jones, N. (eds.) Program Flow Analysis: Theory and Applications, Prentice Hall Inc., Englewood Cliffs (1981)
Orlovich, M., Rugina, R.: Memory leak analysis by contradiction. Technical report, Cornell University (2006)
Rinetzky, N., Sagiv, M.: Interprocedural shape analysis for recursive programs. In: Wilhelm, R. (ed.) CC 2001. LNCS, vol. 2027, p. 133. Springer, Heidelberg (2001)
Manevich, R., Sridharan, M., Adams, S., Das, M., Yang, Z.: PSE: Explaining program failures via postmortem static analysis. In: Proceedings of the ACM SIGSOFT 1999 Symposium on the Foundations of Software Engineering, Newport Beach, CA (2002)
Strom, R., Yellin, D.: Extending typestate checking using conditional liveness analysis. IEEE Transactions on Software Engineering 19(5), 478–485 (1993)
Duesterwald, E., Gupta, R., Soffa, M.: Demand-driven computation of interprocedural data flow. In: Proceedings of the 22nd Annual ACM Symposium on the Principles of Programming Languages, San Francisco, CA (1995)
Horwitz, S., Reps, T., Sagiv, M.: Demand interprocedural dataflow analysis. In: Proceedings of the ACM Symposium on the Foundations of Software Engineering, Washington, DC (1995)
Sagiv, S., Reps, T., Horwitz, S.: Precise interprocedural dataflow analysis with applications to constant propagation. Theoretical Computer Science 167(1&2), 131–170 (1996)
Ghiya, R., Hendren, L.: Is is a tree, a DAG or a cyclic graph? a shape analysis for heap-directed pointers in C. In: Proceedings of the 23rd Annual ACM Symposium on the Principles of Programming Languages, St. Petersburg Beach, FL (1996)
Hastings, R., Joyce, B.: Purify: Fast detection of memory leaks and access errors. In: Proceedings of the 1992 Winter Usenix Conference (1992)
Hauswirth, M., Chilimbi, T.: Low-overhead memory leak detection using adaptive statistical profiling. In: Proceedings of the 11th International Conference on Architectural Support for Programming Languages and Operating Systems, Boston, MA (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Orlovich, M., Rugina, R. (2006). Memory Leak Analysis by Contradiction. In: Yi, K. (eds) Static Analysis. SAS 2006. Lecture Notes in Computer Science, vol 4134. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11823230_26
Download citation
DOI: https://doi.org/10.1007/11823230_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37756-6
Online ISBN: 978-3-540-37758-0
eBook Packages: Computer ScienceComputer Science (R0)