Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Extended Version)

TL;DR

Addresses scalability of symbolic execution by introducing a formal compositional symbolic execution (CSE) engine with local function specifications validated in an underlying separation logic. It provides an axiomatic consume/produce interface that supports both SL-based pre/post conditions $\{ \vec{x} = \vec{x} \star P \} f(\vec{x}) \{ ok: Q_{ok} \}$ and ISL-based UX specs $[ \vec{x} = \vec{x} \star P ] f(\vec{x}) [ ok: Q_{ok} ]$, enabling interoperability and a unified semantics that covers both OX and UX. A general soundness result shows that, assuming the axiomatic properties of consume/produce and the validity of function specs with respect to the underlying logic, the CSE engine is sound; switching between satisfiability and validity yields the same framework for correctness and incorrectness reasoning. The paper provides a demonstrator Haskell implementation and extends the Gillian platform with automatic UX true-bug finding via UX bi-abduction, evaluated on real-world code such as the Collections-C library.

Abstract

The introduction of separation logic has led to the development of symbolic execution techniques and tools that are (functionally) compositional with function specifications that can be used in broader calling contexts. Many of the compositional symbolic execution tools developed in academia and industry have been grounded on a formal foundation, but either the function specifications are not validated with respect to the underlying separation logic of the theory, or there is a large gulf between the theory and the implementation of the tool. We introduce a formal compositional symbolic execution engine which creates and uses function specifications from an underlying separation logic and provides a sound theoretical foundation for, and indeed was partially inspired by, the Gillian symbolic execution platform. This is achieved by providing an axiomatic interface which describes the properties of the consume and produce operations used in the engine to update compositionally the symbolic state, for example when calling function specifications. This consume-produce technique is used by VeriFast, Viper, and Gillian, but has not been previously characterised independently of the tool. As part of our result, we give consume and produce operations inspired by the Gillian implementation that satisfy the properties described by our axiomatic interface. A surprising property is that our engine semantics provides a common foundation for both correctness and incorrectness reasoning, with the difference in the underlying engine only amounting to the choice to use satisfiability or validity. We use this property to extend the Gillian platform, which previously only supported correctness reasoning, with incorrectness reasoning and automatic true bug-finding using incorrectness bi-abduction.

Figures (1)

• Figure 1: Definition and symbolic execution of function f