Online citations, reference lists, and bibliographies.

Hierarchical Shape Abstraction For Analysis Of Free List Memory Allocators

B. Fang, M. Sighireanu
Published 2016 · Computer Science

Cite This
Download PDF
Analyze on Scholarcy
We propose a hierarchical abstract domain for the analysis of free list memory allocators that tracks shape and numerical properties about both the heap and the free lists. Our domain is based on Separation Logic extended with predicates that capture the pointer arithmetics constraints for the heap list and the shape of the free list. These predicates are combined using a hierarchical composition operator to specify the overlapping of the heap list by the free list. In addition to expressiveness, this operator leads to a compositional and compact representation of abstract values and simplifies the implementation of the abstract domain. The shape constraints are combined with numerical constraints over integer arrays to track properties about the allocation policies (best-fit, first-fit, etc.). Such properties are out of the scope of the existing analyzers. We implemented this domain and we show its effectiveness on several implementations of free list allocators.
This paper references
Memory allocation in C. Embedded Systems Programming
L Aldridge (2008)
Local Shape Analysis for Overlaid Data Structures
Cezara Dragoi (2013)
Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite Data
Ahmed Bouajjani (2012)
Shape Analysis with Structural Invariant Checkers
B. E. Chang (2007)
Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic
C. Calcagno (2006)
A combination framework for tracking partition sizes
Sumit Gulwani (2009)
Recency-Abstraction for Heap-Allocated Storage
G. Balakrishnan (2006)
Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints
P. Cousot (1977)
A Local Shape Analysis Based on Separation Logic
Dino Distefano (2006)
Modular Construction of Shape-Numeric Analyzers
Bor-Yuh Evan Chang (2013)
Automated verification of heap-manipulating programs with infinite data
C. Dragoi (2011)
On inter-procedural analysis of programs with lists and data
A. Bouajjani (2011)
Memory allocation in C
L. Aldridge (1989)
Frama-C - A Software Analysis Perspective
Pascal Cuoq (2012)
Abstraction of Arrays Based on Non Contiguous Partitions
Jiangchao Liu (2015)
On Automated Lemma Generation for Separation Logic with Inductive Definitions
C. Enea (2015)
Discovering properties about arrays in simple programs
N. Halbwachs (2008)
Program Analysis for Overlaid Data Structures
O. Lee (2011)
Lifting abstract interpreters to quantified logical domains
Sumit Gulwani (2008)
Hierarchical Shape Abstraction of Dynamic Structures in Static Blocks
Pascal Sotin (2012)
Dynamic Storage Allocation: A Survey and Critical Review
P. R. Wilson (1995)
The Art of Computer Programming, Volume I: Fundamental Algorithms, 2nd Edition
D. Knuth (1968)
The C++ programming language (2nd ed.)
B. Stroustrup (1991)
Field-Sensitive Value Analysis by Field-Insensitive Analysis
E. Albert (2009)
Local Reasoning about Programs that Alter Data Structures
P. O'Hearn (2001)
The C++ Programming Language, Second Edition
B. Stroustrup (1991)
Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics
Antoine Miné (2006)
Apron: A Library of Numerical Abstract Domains for Static Analysis
B. Jeannet (2009)

This paper is referenced by
Semantic Scholar Logo Some data provided by SemanticScholar