Context- and path-sensitive memory leak detection

ABSTRACT

We present a context- and path-sensitive algorithm for detecting memory leaks in programs with explicit memory management. Our leak detection algorithm is based on an underlying escape analysis: any allocated location in a procedure P that is not deallocated in P and does not escape from P is leaked. We achieve very precise context- and path-sensitivity by expressing our analysis using boolean constraints. In experiments with six large open source projects our analysis produced 510 warnings of which 455 were unique memory leaks, a false positive rate of only 10.8%. A parallel implementation improves performance by over an order of magnitude on large projects; over five million lines of code in the Linux kernel is analyzed in 50 minutes.

REFERENCES

• 1: William R. Bush , Jonathan D. Pincus , David J. Sielaff, A static analyzer for finding dynamic programming errors, Software—Practice & Experience, v.30 n.7, p.775-802, June 2000 [doi>10.1002/(SICI)1097-024X(200006)30:7<775::AID-SPE309>3.0.CO;2-H]
• 2: Matthias Hauswirth , Trishul M. Chilimbi, Low-overhead memory leak detection using adaptive statistical profiling, Proceedings of the 11th international conference on Architectural support for programming languages and operating systems, October 07-13, 2004, Boston, MA, USA
• 3: Andy Chow Chou , Dawson Engler, Static analysis for bug finding in systems software, 2003
• 4: Maryam Emami , Rakesh Ghiya , Laurie J. Hendren, Context-sensitive interprocedural points-to analysis in the presence of function pointers, Proceedings of the ACM SIGPLAN 1994 conference on Programming language design and implementation, p.242-256, June 20-24, 1994, Orlando, Florida, United States
• 5: David Evans, Static detection of dynamic memory errors, Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation, p.44-53, May 21-24, 1996, Philadelphia, Pennsylvania, United States
• 6: Brian Hackett , Radu Rugina, Region-based shape analysis with tracked locations, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.310-323, January 12-14, 2005, Long Beach, California, USA
• 7: R. Hastings and B. Joyce. Purify: Fast detection of memory leaks and access errors. In Proceedings of the Winter USENIX Conference, Dec. 1992.
• 8: David L. Heine , Monica S. Lam, A practical flow-sensitive and context-sensitive C and C++ memory leak detector, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 9: F. Ivancic, Z. Yang, M. Ganai, A. Gupta, and P. Ashar. Efficient SAT-based bounded model checking for software verification. In Proceedings of the 1st International Symposium on Leveraging Applications of Formal Methods, 2004.
• 10: Daniel Jackson , Mandana Vaziri, Finding bugs with a constraint solver, Proceedings of the 2000 ACM SIGSOFT international symposium on Software testing and analysis, p.14-25, August 21-24, 2000, Portland, Oregon, United States
• 11: Edmund Clarke , Daniel Kroening , Karen Yorav, Behavioral consistency of C and verilog programs using bounded model checking, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA [doi>10.1145/775832.775928]
• 12: William Landi , Barbara G. Ryder, A safe approximate algorithm for interprocedural aliasing, Proceedings of the ACM SIGPLAN 1992 conference on Programming language design and implementation, p.235-248, June 15-19, 1992, San Francisco, California, United States
• 13: Donglin Liang , Mary Jean Harrold, Efficient Computation of Parameterized Pointer Information for Interprocedural Analyses, Proceedings of the 8th International Symposium on Static Analysis, p.279-298, July 16-18, 2001
• 14: Erik Ruf, Effective synchronization removal for Java, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.208-218, June 18-21, 2000, Vancouver, British Columbia, Canada
• 15: Luc Séméria , Giovanni De Micheli, SpC: synthesis of pointers in C: application of pointer analysis to the behavioral synthesis from C, Proceedings of the 1998 IEEE/ACM international conference on Computer-aided design, p.340-346, November 08-12, 1998, San Jose, California, United States [doi>10.1145/288548.289051]
• 16: John Whaley , Martin Rinard, Compositional pointer and escape analysis for Java programs, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.187-206, November 01-05, 1999, Denver, Colorado, United States
• 17: Robert P. Wilson , Monica S. Lam, Efficient context-sensitive pointer analysis for C programs, Proceedings of the ACM SIGPLAN 1995 conference on Programming language design and implementation, p.1-12, June 18-21, 1995, La Jolla, California, United States
• 18: Yichen Xie , Alex Aiken, Scalable error detection using boolean satisfiability, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.351-363, January 12-14, 2005, Long Beach, California, USA
• 19: Y. Xie and A. Chou. Path sensitive analysis using boolean satisfiability. Technical report, Stanford University, Nov. 2002.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.3 Coding Tools and Techniques
      D.2.5 Testing and Debugging

General Terms:
Algorithms, Experimentation, Languages, Verification

Keywords:
boolean satisfiability, error detection, memory leaks, memory management, program analysis