A combination framework for tracking partition sizes

ABSTRACT

We describe an abstract interpretation based framework for proving relationships between sizes of memory partitions. Instances of this framework can prove traditional properties such as memory safety and program termination but can also establish upper bounds on usage of dynamically allocated memory. Our framework also stands out in its ability to prove properties of programs manipulating both heap and arrays which is considered a difficult task. Technically, we define an abstract domain that is parameterized by an abstract domain for tracking memory partitions (sets of memory locations) and by a numerical abstract domain for tracking relationships between cardinalities of the partitions. We describe algorithms to construct the transfer functions for the abstract domain in terms of the corresponding transfer functions of the parameterized abstract domains. A prototype of the framework was implemented and used to prove interesting properties of realistic programs, including programs that could not have been automatically analyzed before.

REFERENCES

• 1: Annotated outline of collections framework. Sun Microsystems. Available at http://java.sun.com/j2se/1.5.0/docs/guide/collections/reference.html.
• 2: Roberto Bagnara , Patricia M. Hill , Enea Zaffanella, The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems, Science of Computer Programming, v.72 n.1-2, p.3-21, June, 2008 [doi>10.1016/j.scico.2007.08.001]
• 3: A. Bouajjani, M. Bozga, P. Habermehl, R. Iosif, P. Moro, and T. Vojnar. Programs with lists are counter automata. In CAV, pages 517--531, 2006.
• 4: A. R. Bradley, Z. Manna, and H. B. Sipma. The polyranking principle. In ICALP, pages 1349--1361, 2005.
• 5: C. Calcagno, D. Distefano, P. W. O'Hearn, and H. Yang. Beyond reachability: Shape abstraction in the presence of pointer arithmetic. In SAS, pages 182--203, 2006.
• 6: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 7: Patrick Cousot , Radhia Cousot, Systematic design of program analysis frameworks, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.269-282, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567778]
• 8: Patrick Cousot , Nicolas Halbwachs, Automatic discovery of linear restraints among variables of a program, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.84-96, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512770]
• 9: Alan Deutsch, On determining lifetime and aliasing of dynamically allocated data in higher-order functional specifications, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.157-168, December 1989, San Francisco, California, United States [doi>10.1145/96709.96725]
• 10: A. Deutsch. Operational Models of Programming Languages and Representations of Relations on Regular Languages with Application to the Static Determination of Dynamic Aliasing Properties of Data. PhD thesis, LIX, The Comp. Sci. Lab of Ecole Polytechnique, 1992.
• 11: Alain Deutsch, Interprocedural may-alias analysis for pointers: beyond k-limiting, Proceedings of the ACM SIGPLAN 1994 conference on Programming language design and implementation, p.230-241, June 20-24, 1994, Orlando, Florida, United States
• 12: D. Distefano, P. W. O'Hearn, and H. Yang. A local shape analysis based on separation logic. In TACAS, pages 287--302, 2006.
• 13: Nurit Dor , Michael Rodeh , Mooly Sagiv, CSSV: towards a realistic tool for statically detecting all buffer overflows in C, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 14: D. Gopan, F. DiMaio, N. Dor, T. W. Reps, and M. Sagiv. Numeric domains with summarized dimensions. In TACAS, pages 512--529, 2004.
• 15: Denis Gopan , Thomas Reps , Mooly Sagiv, A framework for numeric analysis of array operations, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.338-350, January 12-14, 2005, Long Beach, California, USA
• 16: S. Gulwani, T. Lev-Ami, and M. Sagiv. A combination framework for tracking partition sizes. Technical Report MSR-TR-2008-158, Microsoft Research, Oct. 2008.
• 17: Sumit Gulwani , Ashish Tiwari, Combining abstract interpreters, Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, June 11-14, 2006, Ottawa, Ontario, Canada
• 18: Martin Hofmann , Steffen Jost, Static prediction of heap space usage for first-order functional programs, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.185-197, January 15-17, 2003, New Orleans, Louisiana, USA
• 19: John Hughes , Lars Pareto, Recursion and dynamic data-structures in bounded space: towards embedded ML programming, Proceedings of the fourth ACM SIGPLAN international conference on Functional programming, p.70-81, September 27-29, 1999, Paris, France
• 20: M. Karr. Affine relationships among variables of a program. Acta Inf., 6:133--151, 1976.
• 21: Viktor Kuncak , Martin Rinard, Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic, Proceedings of the 21st international conference on Automated Deduction: Automated Deduction, July 17-20, 2007, Bremen, Germany [doi>10.1007/978-3-540-73595-3_15]
• 22: Tal Lev-Ami , Shmuel Sagiv, TVLA: A System for Implementing Static Analyses, Proceedings of the 7th International Symposium on Static Analysis, p.280-301, June 29-July 01, 2000
• 23: S. Magill, J. Berdine, E. M. Clarke, and B. Cook. Arithmetic strengthening for shape analysis. In SAS, pages 419--436, 2007.
• 24: R. Manevich, M. Sagiv, G. Ramalingam, and J. Field. Partially disjunctive heap abstraction. In SAS, pages 265--279, 2004.
• 25: R. Manevich, E. Yahav, G. Ramalingam, and M. Sagiv. Predicate abstraction and canonical abstraction for singly-linked lists. In VMCAI, pages 181--198, 2005.
• 26: Antoine Miné, The Octagon Abstract Domain, Proceedings of the Eighth Working Conference on Reverse Engineering (WCRE'01), p.310, October 02-05, 2001
• 27: Greg Nelson , Derek C. Oppen, Fast Decision Procedures Based on Congruence Closure, Journal of the ACM (JACM), v.27 n.2, p.356-364, April 1980 [doi>10.1145/322186.322198]
• 28: H. H. Nguyen, C. David, S. Qin, and W.-N. Chin. Automated verification of shape and size properties via separation logic. In VMCAI, pages 251--266, 2007.
• 29: Andreas Podelski , Andrey Rybalchenko, Transition Invariants, Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, p.32-41, July 13-17, 2004 [doi>10.1109/LICS.2004.50]
• 30: A. Podelski and T. Wies. Boolean heaps. In SAS, pages 268--283, 2005.
• 31: John C. Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, p.55-74, July 22-25, 2002
• 32: R. Rugina. Quantitative shape analysis. In SAS, pages 228--245, 2004.
• 33: Mooly Sagiv , Thomas Reps , Reinhard Wilhelm, Parametric shape analysis via 3-valued logic, ACM Transactions on Programming Languages and Systems (TOPLAS), v.24 n.3, p.217-298, May 2002 [doi>10.1145/514188.514190]
• 34: A. Turing, Checking a large routine, The early British computer conferences, MIT Press, Cambridge, MA, 1989
• 35: Tuba Yavuz-Kahveci , Tevfik Bultan, Automated Verification of Concurrent Linked Lists with Counters, Proceedings of the 9th International Symposium on Static Analysis, p.69-84, September 17-20, 2002

INDEX TERMS

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

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Reliability, Verification

Keywords:
combining analyses, memory safety, numerical analysis, set analysis, shape analysis, space bounds, termination