Hierarchical Shape Abstraction for Analysis of Free-List Memory Allocators

TL;DR

This paper introduces a hierarchical abstract domain based on Separation Logic for analyzing free-list memory allocators, capturing shape and numerical properties to improve precision and support various allocation policies.

Contribution

It presents a novel hierarchical abstraction combining shape and numerical constraints, enabling more precise analysis of free-list allocators compared to prior methods.

Findings

Effective in analyzing multiple free-list allocator implementations

Captures shape and numerical properties simultaneously

Supports various allocation policies like best-fit and first-fit

Abstract

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.