Sumit Gulwani
Tal Lev-Ami
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.
- Annotated outline of collections framework. Sun Microsystems. Available at http://java.sun.com/j2se/1.5.0/docs/guide/collections/reference.html.Google Scholar
- R. Bagnara, P. M. Hill, and E. 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, 2008. To appear. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- A. R. Bradley, Z. Manna, and H. B. Sipma. The polyranking principle. In ICALP, pages 1349--1361, 2005. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL, pages 238--252, 1977. Google ScholarDigital Library
- P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In POPL, pages 269--282, 1979. Google ScholarDigital Library
- P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In POPL, pages 84--96, 1978. Google ScholarDigital Library
- A. Deutsch. On determining lifetime and aliasing of dynamically allocated data in higher-order functional specifications. In POPL, pages 157--168, 1990. Google ScholarDigital Library
- 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.Google Scholar
- A. Deutsch. Interprocedural may-alias analysis for pointers: Beyond k-limiting. In PLDI, pages 230--241, 1994. Google ScholarDigital Library
- D. Distefano, P. W. O'Hearn, and H. Yang. A local shape analysis based on separation logic. In TACAS, pages 287--302, 2006. Google ScholarDigital Library
- N. Dor, M. Rodeh, and M. Sagiv. CSSV: towards a realistic tool for statically detecting all buffer overflows in C. In PLDI, pages 155--167, 2003. Google ScholarDigital Library
- D. Gopan, F. DiMaio, N. Dor, T. W. Reps, and M. Sagiv. Numeric domains with summarized dimensions. In TACAS, pages 512--529, 2004.Google ScholarCross Ref
- D. Gopan, T. Reps, and M. Sagiv. A framework for numeric analysis of array operations. In POPL, pages 338--350, 2005. Google ScholarDigital Library
- 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.Google ScholarDigital Library
- S. Gulwani and A. Tiwari. Combining abstract interpreters. In PLDI, pages 376--386, 2006. Google ScholarDigital Library
- M. Hofmann and S. Jost. Static prediction of heap space usage for first-order functional programs. In POPL, pages 185--197, 2003. Google ScholarDigital Library
- J. Hughes and L. Pareto. Recursion and dynamic data-structures in bounded space: Towards embedded ML programming. In ICFP, pages 70--81, 1999. Google ScholarDigital Library
- M. Karr. Affine relationships among variables of a program. Acta Inf., 6:133--151, 1976.Google ScholarDigital Library
- V. Kuncak and M. C. Rinard. Towards efficient satisfiability checking for boolean algebra with presburger arithmetic. In CADE, pages 215--230, 2007. Google ScholarDigital Library
- T. Lev-Ami and M. Sagiv. TVLA: A system for implementing static analyses. In SAS, pages 280--301, 2000. Google ScholarDigital Library
- S. Magill, J. Berdine, E. M. Clarke, and B. Cook. Arithmetic strengthening for shape analysis. In SAS, pages 419--436, 2007. Google ScholarDigital Library
- R. Manevich, M. Sagiv, G. Ramalingam, and J. Field. Partially disjunctive heap abstraction. In SAS, pages 265--279, 2004.Google ScholarCross Ref
- R. Manevich, E. Yahav, G. Ramalingam, and M. Sagiv. Predicate abstraction and canonical abstraction for singly-linked lists. In VMCAI, pages 181--198, 2005. Google ScholarDigital Library
- A. Mine. The octagon abstract domain. In WCRE, pages 310--319, 2001. Google ScholarDigital Library
- G. Nelson and D. Oppen. Fast decision procedures based on congruence closure. JACM, 27(2):356--364, Apr. 1980. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- A. Podelski and A. Rybalchenko. Transition invariants. In LICS, pages 32--41, 2004. Google ScholarDigital Library
- A. Podelski and T. Wies. Boolean heaps. In SAS, pages 268--283, 2005. Google ScholarDigital Library
- J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS, pages 55--74, 2002. Google ScholarDigital Library
- R. Rugina. Quantitative shape analysis. In SAS, pages 228--245, 2004.Google ScholarCross Ref
- M. Sagiv, T. W. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. ACM TOPLAS, 24(3):217--298, 2002. Google ScholarDigital Library
- A. Turing. Checking a large routine. In The early British computer conferences, pages 70--72. MIT Press, Cambridge, MA, USA, 1989. Google ScholarDigital Library
- T. Yavuz-Kahveci and T. Bultan. Automated verification of concurrent linked lists with counters. In SAS, pages 69--84, 2002. Google ScholarDigital Library
Index Terms
- A combination framework for tracking partition sizes
Recommendations
A combination framework for tracking partition sizes
POPL '09We 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 ...
Automatically Proving Termination and Memory Safety for Programs with Pointer Arithmetic
While automated verification of imperative programs has been studied intensively, proving termination of programs with explicit pointer arithmetic fully automatically was still an open problem. To close this gap, we introduce a novel abstract domain ...
Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics
LCTES '06: Proceedings of the 2006 ACM SIGPLAN/SIGBED conference on Language, compilers, and tool support for embedded systemsWe propose a memory abstraction able to lift existing numerical static analyses to C programs containing union types, pointer casts, and arbitrary pointer arithmetics. Our framework is that of a combined points-to and data-value analysis. We abstract ...
Comments