Take a look at the new version of this page: [ beta version ]. Tell us what you think.

ABSTRACT

This paper presents a practical inter-procedural analysis algorithm for detecting memory leaks in C programs. Our algorithm tracks the flow of values from allocation points to deallocation points using a sparse representation of the program consisting of a value flow graph that captures def-use relations and value flows via program assignments. Edges in the graph are annotated with guards that describe branch conditions in the program. The memory leak analysis is reduced to a reachability problem over the guarded value flowgraph. Our implemented tool has been effective at detecting more than 60 memory leaks in the SPEC2000 benchmarks and in two open-source applications, bash and sshd, while keeping the false positive rate below 20%. The sparse program representation makes the tool efficient in practice, and allows it to report concise error messages.

REFERENCES

• 1: Thomas Ball , Rupak Majumdar , Todd Millstein , Sriram K. Rajamani, Automatic predicate abstraction of C programs, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.203-213, June 2001, Snowbird, Utah, United States
• 2: Thomas Ball , Sriram K. Rajamani, The SLAM project: debugging system software via static analysis, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-3, January 16-18, 2002, Portland, Oregon
• 3: R. Cytron , J. Ferrante , B. K. Rosen , M. N. Wegman , F. K. Zadeck, An efficient method of computing static single assignment form, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.25-35, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75280]
• 4: Manuvir Das , Sorin Lerner , Mark Seigle, ESP: path-sensitive program verification in polynomial time, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 5: Nurit Dor , Michael Rodeh , Shmuel Sagiv, Checking Cleanness in Linked Lists, Proceedings of the 7th International Symposium on Static Analysis, p.115-134, June 29-July 01, 2000
• 6: Dawson Engler , Benjamin Chelf , Andy Chou , Seth Hallem, Checking system rules using system-specific, programmer-written compiler extensions, Proceedings of the 4th conference on Symposium on Operating System Design & Implementation, p.1-1, October 22-25, 2000, San Diego, California
• 7: Jeffrey S. Foster , Robert Johnson , John Kodumal , Alex Aiken, Flow-insensitive type qualifiers, ACM Transactions on Programming Languages and Systems (TOPLAS), v.28 n.6, p.1035-1087, November 2006 [doi>10.1145/1186632.1186635]
• 8: Emden R. Gansner , Stephen C. North, An open graph visualization system and its applications to software engineering, Software—Practice & Experience, v.30 n.11, p.1203-1233, Sept. 2000 [doi>10.1002/1097-024X(200009)30:11<1203::AID-SPE338>3.3.CO;2-E]
• 9: 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
• 10: 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
• 11: David L. Heine , Monica S. Lam, Static detection of leaks in polymorphic containers, Proceeding of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China [doi>10.1145/1134285.1134321]
• 12: Gerard J. Holzmann. UNO: Static source code checking for userdefined properties. In Proceedings of the World Conference on Integrated Design and Process Technology, Pasadena, CA, June 2002.
• 13: V. Benjamin Livshits , Monica S. Lam, Tracking pointers with path and context sensitivity for bug detection in C programs, Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineering, September 01-05, 2003, Helsinki, Finland
• 14: Maksim Orlovich and Radu Rugina. Memory leak analysis by contradition. In Proceedings of the International Static Analysis Symposium, Seoul, Korea, August 2006.
• 15: Daniel Le Berre (project leader). SAT4J: A satisfiability library for java. http://www.sat4j.org/, January 2006.
• 16: Thomas Reps , Susan Horwitz , Mooly Sagiv, Precise interprocedural dataflow analysis via graph reachability, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.49-61, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199462]
• 17: Mooly Sagiv , Thomas Reps , Reinhard Wilhelm, Parametric shape analysis via 3-valued logic, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.105-118, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292552]
• 18: Gregor Snelting , Torsten Robschink , Jens Krinke, Efficient path conditions in dependence graphs for software safety analysis, ACM Transactions on Software Engineering and Methodology (TOSEM), v.15 n.4, p.410-457, October 2006 [doi>10.1145/1178625.1178628]
• 19: Bjarne Steensgaard, Points-to analysis in almost linear time, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.32-41, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237727]
• 20: Peng Tu , David Padua, Efficient building and placing of gating functions, Proceedings of the ACM SIGPLAN 1995 conference on Programming language design and implementation, p.47-55, June 18-21, 1995, La Jolla, California, United States
• 21: J. Uniejewski. SPEC Benchmark Suite: Designed for today's advanced systems. SPEC Newsletter Volume 1, Issue 1, SPEC, Fall 1989.
• 22: Yichen Xie , Alex Aiken, Context- and path-sensitive memory leak detection, Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering, September 05-09, 2005, Lisbon, Portugal
• 23: Junfeng Yang , Paul Twohey , Dawson Engler , Madanlal Musuvathi, Using model checking to find serious file system errors, Proceedings of the 6th conference on Symposium on Opearting Systems Design & Implementation, p.19-19, December 06-08, 2004, San Francisco, CA

INDEX TERMS

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

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Compilers

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Program analysis

General Terms:
Algorithms, Languages, Reliability, Verification

Keywords:
memory leaks, memory management, static error detection, value-flow analysis