Deciding Separation Logic with Pointer Arithmetic and Inductive Definitions
Wanyun Su, Zhilin Wu, Mihaela Sighireanu
TL;DR
This paper introduces SLAH, a separation-logic fragment that permits pointer arithmetic inside inductive definitions to specify heap-list structures. It develops decision procedures for satisfiability (NP-complete) and entailment (coNP-complete) by translating SLAH formulas into Presburger arithmetic via equi-satisfiable abstractions, with a polynomial-time computable summary for heap-list predicates. A key technical contribution is the forward-thinking abstraction Abs^+ for the hls predicate, enabling a sound equi-satisfiable PA formula, together with a sophisticated ordered-entailment framework that handles address arithmetic and atom splitting. The authors implement the procedures in CompSPEN+ and demonstrate strong practical performance on benchmarks from memory allocator verification, highlighting both efficiency and the need for atom-splitting in challenging entailments. This work advances automated verification of low-level programs that manipulate heap lists using pointer arithmetic inside inductive definitions, with implications for memory-safe systems and allocator correctness.
Abstract
Pointer arithmetic is widely used in low-level programs, e.g. memory allocators. The specification of such programs usually requires using pointer arithmetic inside inductive definitions to define the common data structures, e.g. heap lists in memory allocators. In this work, we investigate decision problems for SLAH, a separation logic fragment that allows pointer arithmetic inside inductive definitions, thus enabling specification of properties for programs manipulating heap lists. Pointer arithmetic inside inductive definitions is challenging for automated reasoning. We tackle this challenge and achieve decision procedures for both satisfiability and entailment of SLAH formulas. The crux of our decision procedure for satisfiability is to compute summaries of inductive definitions. We show that although the summary is naturally expressed as an existentially quantified non-linear arithmetic formula, it can actually be transformed into an equivalent linear arithmetic formula. The decision procedure for entailment, on the other hand, has to match and split the spatial atoms according to the arithmetic relation between address variables. We report on the implementation of these decision procedures and their good performance in solving problems issued from the verification of building block programs used in memory allocators.