ABSTRACT
This paper proposes a novel approach to shape analysis: using local reasoning about individual heap locations instead of global reasoning about entire heap abstractions. We present an inter-procedural shape analysis algorithm for languages with destructive updates. The key feature is a novel memory abstraction that differs from traditional abstractions in two ways. First, we build the shape abstraction and analysis on top of a pointer analysis. Second, we decompose the shape abstraction into a set of independent configurations, each of which characterizes one single heap location. Our approach: 1) leads to simpler algorithm specifications, because of local reasoning about the single location; 2) leads to efficient algorithms, because of the smaller granularity of the abstraction; and 3) makes it easier to develop context-sensitive, demand-driven, and incremental shape analyses.We also show that the analysis can be used to enable the static detection of memory errors in programs with explicit deallocation. We have built a prototype tool that detects memory leaks and accesses through dangling pointers in C programs. The experiments indicate that the analysis is sufficiently precise to detect errors with low false positive rates; and is sufficiently lightweight to scale to larger programs. For a set of three popular C programs, the tool has analyzed about 70K lines of code in less than 2 minutes and has produced 97 warnings, 38 of which were actual errors.
- S. Amarasinghe, J. Anderson, M. Lam, and C. Tseng. The SUIF compiler for scalable parallel machines. In Proceedings of the Eighth SIAM Conference on Parallel Processing for Scientific Computing, San Francisco, CA, February 1995.]]Google Scholar
- T. Ball, R. Majumdar, T. Millstein, and S. Rajamani. Automatic predicate abstraction of C programs. In Proceedings of the SIGPLAN '01 Conference on Program Language Design and Implementation, Snowbird, UT, June 2001.]] Google ScholarDigital Library
- T. Ball and S. Rajamani. The SLAM project: Debugging system software via static analysis. In Proceedings of the 29th Annual ACM Symposium on the Principles of Programming Languages, Portland, OR, January 2002.]] Google ScholarDigital Library
- W. Bush, J. Pincus, and D. Sielaff. A static analyzer for finding dynamic programming errors. Software -- Practice and Experience, 30(7):775--802, August 2000.]] Google ScholarDigital Library
- S. Chong and R. Rugina. Static analysis of accessed regions in recursive data structures. In Proceedings of the 10th International Static Analysis Symposium, San Diego, CA, June 2003.]] Google ScholarDigital Library
- M. Das, S. Lerner, and M. Seigle. ESP: Path-sensitive program verification in polynomial time. In Proceedings of the SIGPLAN '02 Conference on Program Language Design and Implementation, Berlin, Germany, June 2002.]] Google ScholarDigital Library
- R. DeLine and M. Fahndrich. Enforcing high-level protocols in low-level software. In Proceedings of the SIGPLAN '01 Conference on Program Language Design and Implementation, Snowbird, UT, June 2001.]] Google ScholarDigital Library
- N. Dor, M. Rodeh, and M. Sagiv. Checking cleanness in linked lists. In Proceedings of the 7th International Static Analysis Symposium, Santa Barbara, CA, July 2000.]] Google ScholarDigital Library
- D. Engler, B. Chelf, A. Chou, and S. Hallem. Checking system rules using system-specific, programmer-written compiler extensions. In Proceedings of the SIGPLAN '02 Conference on Program Language Design and Implementation, Berlin, Germany, June 2002.]]Google Scholar
- M. Fahndrich, J. Rehof, and M. Das. Scalable context-sensitive flow analysis using instantiation constraints. In Proceedings of the SIGPLAN '00 Conference on Program Language Design and Implementation, Vancouver, Canada, June 2000.]] Google ScholarDigital Library
- R. Ghiya and L. Hendren. 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, January 1996.]] Google ScholarDigital Library
- B. Hackett and R. Rugina. Region-based shape analysis with tracked locations. Technical Report TR2004-1968, Cornell University, October 2004.]]Google Scholar
- R. Hastings and B. Joyce. Purify: Fast detection of memory leaks and access errors. In Proceedings of the 1992 Winter Usenix Conference, January 1992.]]Google Scholar
- M. Hauswirth and T. Chilimbi. 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, October 2004.]] Google ScholarDigital Library
- D. Heine and M. Lam. A practical flow-sensitive and context-sensitive C and C++ memory leak detector. In Proceedings of the SIGPLAN '03 Conference on Program Language Design and Implementation, San Diego, CA, June 2003.]] Google ScholarDigital Library
- N. Heintze and O. Tardieu. Demand-driven pointer analysis. In Proceedings of the SIGPLAN '01 Conference on Program Language Design and Implementation, Snowbird, UT, June 2001.]] Google ScholarDigital Library
- L. Hendren, J. Hummel, and A. Nicolau. A general data dependence test for dynamic, pointer-based data structures. In Proceedings of the SIGPLAN '94 Conference on Program Language Design and Implementation, Orlando, FL, June 1994.]] Google ScholarDigital Library
- L. Hendren and A. Nicolau. Parallelizing programs with recursive data structures. IEEE Transactions on Parallel and Distributed Systems, 1(1):35--47, January 1990.]] Google ScholarDigital Library
- S. Ishtiaq and P. O'Hearn. BI as an assertion language for mutable data structures. In Proceedings of the 28th Annual ACM Symposium on the Principles of Programming Languages, London, UK, January 2001.]] Google ScholarDigital Library
- B. Jeannet, A. Loginov, T. Reps, and M. Sagiv. A relational approach to interprocedural shape analysis. In Proceedings of the 11th International Static Analysis Symposium, Verona, Italy, August 2004.]]Google ScholarCross Ref
- V. Kuncak, P. Lam, and M. Rinard. Role analysis. In Proceedings of the 29th Annual ACM Symposium on the Principles of Programming Languages, Portland, OR, January 2002.]] Google ScholarDigital Library
- T. Lev-ami, T. Reps, M. Sagiv, and R. Wilhelm. Putting static analysis to work for verification: A case study. In 2000 International Symposium on Software Testing and Analysis, August 2000.]] Google ScholarDigital Library
- T. Lev-Ami and M. Sagiv. TVLA: A system for implementing static analyses. In Proceedings of the 7th International Static Analysis Symposium, Santa Barbara, CA, July 2000.]] Google ScholarDigital Library
- D. Liang and M.J. Harrold. Efficient points-to analysis for whole-program analysis. In Proceedings of the ACM SIGSOFT '99 Symposium on the Foundations of Software Engineering, Toulouse,France, September 1999.]] Google ScholarDigital Library
- G. Necula, S. McPeak, and W. Weimer. CCured: type-safe retrofitting of legacy code. In Proceedings of the 29th Annual ACM Symposium on the Principles of Programming Languages, Portland, OR, January 2002.]] Google ScholarDigital Library
- P. O'Hearn, H. Yang, and J. Reynolds. Separation and information hiding. In Proceedings of the 31th Annual ACM Symposium on the Principles of Programming Languages, Venice, Italy, January 2004.]] Google ScholarDigital Library
- J. Reynolds. Separation logic: A logic for shared mutable data structures. In Proceedings of the Seventeenth Annual IEEE Symposium on Logic in Computer Science, Copenhagen, Denmark, July 2002.]] Google ScholarDigital Library
- N. Rinetzky and M. Sagiv. Interprocedural shape analysis for recursive programs. In Proceedings of the 2001 International Conference on Compiler Construction, Genova, Italy, April 2001.]] Google ScholarDigital Library
- M. Sagiv, T. Reps, and R. Wilhelm. Solving shape-analysis problems in languages with destructive updating. ACM Transactions on Programming Languages and Systems, 20(1):1--50, January 1998.]] Google ScholarDigital Library
- M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. In Proceedings of the 26th Annual ACM Symposium on the Principles of Programming Languages, San Antonio, TX, January 1999.]] Google ScholarDigital Library
- M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. ACM Transactions on Programming Languages and Systems, 24(3), May 2002.]] Google ScholarDigital Library
- Bjarne Steensgaard. 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, January 1996.]] Google ScholarDigital Library
- F. Vivien and M. Rinard. Incrementalized pointer and escape analysis. In Proceedings of the SIGPLAN '01 Conference on Program Language Design and Implementation, Snowbird, UT, June 2001.]] Google ScholarDigital Library
- R. Wilhelm, M. Sagiv, and T. Reps. Shape analysis. In Proceedings of the 2000 International Conference on Compiler Construction, Berlin, Germany, April 2000.]] Google ScholarDigital Library
- E. Yahav. Verifying safety properties of concurrent Java programs using 3-valued logic. In Proceedings of the 28th Annual ACM Symposium on the Principles of Programming Languages, London, UK, January 2001.]] Google ScholarDigital Library
- E. Yahav and G. Ramalingam. Verifying safety properties using separation and heterogeneous abstractions. In Proceedings of the SIGPLAN '04 Conference on Program Language Design and Implementation, Washington, DC, June 2004.]] Google ScholarDigital Library
Index Terms
- Region-based shape analysis with tracked locations
Recommendations
Region-based shape analysis with tracked locations
Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languagesThis paper proposes a novel approach to shape analysis: using local reasoning about individual heap locations instead of global reasoning about entire heap abstractions. We present an inter-procedural shape analysis algorithm for languages with ...
Practical memory leak detection using guarded value-flow analysis
PLDI '07: Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and ImplementationThis 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 ...
Practical memory leak detection using guarded value-flow analysis
Proceedings of the 2007 PLDI conferenceThis 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 ...
Comments