Online citations, reference lists, and bibliographies.
← Back to Search

Hierarchical Shape Abstraction For Analysis Of Free List Memory Allocators

Bin Fang, M. Sighireanu
Published 2016 · Computer Science

Save to my Library
Download PDF
Analyze on Scholarcy Visualize in Litmaps
Reduce the time it takes to create your bibliography by a factor of 10 by using the world’s favourite reference manager
Time to take this seriously.
Get Citationsy
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
The Art of Computer Programming, Volume I: Fundamental Algorithms, 2nd Edition
D. Knuth (1968)
Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints
P. Cousot (1977)
Memory allocation in C
L. Aldridge (1989)
The C++ Programming Language, Second Edition
B. Stroustrup (1991)
The C++ programming language (2nd ed.)
B. Stroustrup (1991)
Dynamic Storage Allocation: A Survey and Critical Review
P. R. Wilson (1995)
Local Reasoning about Programs that Alter Data Structures
P. O'Hearn (2001)
Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics
Antoine Miné (2006)
Recency-Abstraction for Heap-Allocated Storage
G. Balakrishnan (2006)
Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic
Cristiano Calcagno (2006)
A Local Shape Analysis Based on Separation Logic
Dino Distefano (2006)
Shape Analysis with Structural Invariant Checkers
B. E. Chang (2007)
Lifting abstract interpreters to quantified logical domains
Sumit Gulwani (2008)
Discovering properties about arrays in simple programs
N. Halbwachs (2008)
Memory allocation in C. Embedded Systems Programming
L Aldridge (2008)
A combination framework for tracking partition sizes
Sumit Gulwani (2009)
Field-Sensitive Value Analysis by Field-Insensitive Analysis
E. Albert (2009)
Apron: A Library of Numerical Abstract Domains for Static Analysis
B. Jeannet (2009)
Automated verification of heap-manipulating programs with infinite data
C. Dragoi (2011)
Program Analysis for Overlaid Data Structures
O. Lee (2011)
On inter-procedural analysis of programs with lists and data
A. Bouajjani (2011)
Hierarchical Shape Abstraction of Dynamic Structures in Static Blocks
Pascal Sotin (2012)
Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite Data
A. Bouajjani (2012)
Frama-C - A Software Analysis Perspective
Pascal Cuoq (2012)
Modular Construction of Shape-Numeric Analyzers
B. E. Chang (2013)
Local Shape Analysis for Overlaid Data Structures
C. Dragoi (2013)
Abstraction of Arrays Based on Non Contiguous Partitions
Jiangchao Liu (2015)
On Automated Lemma Generation for Separation Logic with Inductive Definitions
C. Enea (2015)

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