Stellis: A Strategy Language for Purifying Separation Logic Entailments

TL;DR

Stellis is a new strategy language designed to automate the purification of separation logic entailments, simplifying them by removing spatial formulas, and is proven sound and effective on verification benchmarks.

Contribution

We introduce Stellis, a flexible strategy language with soundness guarantees for automating the purification of separation logic entailments.

Findings

Automatically purified 95.6% of entailments in benchmarks.

Generated correctness proofs for the overall automation.

Effective on verification of linked data structures and microkernel memory modules.

Abstract

Automatically proving separation logic entailments is a fundamental challenge in verification. While rule-based methods rely on separation logic rules (lemmas) for automation, these rule statements are insufficient for describing automation strategies, which usually involve the alignment and elimination of corresponding memory layouts in specific scenarios. To overcome this limitation, we propose Stellis, a strategy language for purifying separation logic entailments, i.e., removing all spatial formulas to reduce the entailment to a simpler pure entailment. Stellis features a powerful matching mechanism and a flexible action description, enabling the straightforward encoding of a wide range of strategies. To ensure strategy soundness, we introduce an algorithm that generates a soundness condition for each strategy, thereby reducing the soundness of each strategy to the correctness of its soundness condition. Furthermore, based on a mechanized reduction soundness theorem, our prototype implementation generates correctness proofs for the overall automation. We evaluate our system on a benchmark of 229 entailments collected from verification of standard linked data structures and the memory module of a microkernel, and the evaluation results demonstrate that, with such flexibility and convenience provided, our system is also highly effective, which automatically purifies 95.6% (219 out of 229) of the entailments using 5 libraries with 98 strategies.