1 Introduction

For analyzing programs with dynamic memory, separation logic (SL) is an established and fairly popular logic introduced by Reynolds et al. [11]. The high expressivity of SL, its ability to generate compact proofs, and its support for local reasoning motivated development of many tools for automatic reasoning about programs with complex dynamic linked data structures. These tools aim at establishing memory safety properties and/or inferring shape properties of the heap. The tools often build on (semi-)decision procedures for checking satisfiability and entailment problems in SL.

Our tool Spen Footnote 1 provides (semi-)decision procedures for the most commonly considered symbolic heaps fragment of SL, extended with user-defined inductive predicates to specify data structures of an unbounded size. Because unrestricted definitions of inductive predicates make the entailment problem for the fragment undecidable [3], only semi-decision procedures have been proposed, e.g., in [2, 4]. Iosif et al. [10] identified a rather large class of inductive definitions for which the entailment problem is decidable, although with a high complexity. Spen focuses on a smaller class of inductive definitions that is, however, expressive enough to specify complex dynamic data structures, such as skip lists, lists of circular lists, AVL trees, or binary search trees.

The chosen class of inductive definitions enables the design of efficient (semi-)decision procedures for satisfiability and entailment [6, 8]. The key idea used for satisfiability checking in Spen is to exploit the semantics of restricted inductive definitions and of separating conjunction to build an equisatisfiable boolean abstraction of the formula. For entailment checking, the idea is to reduce the problem of checking \(\varphi \Rightarrow \psi \) to the problem of checking a set of simple entailments where the right-hand side is an inductive predicate atom. The compositionality of this reduction leads to high efficiency (the simple entailments can be checked independently) and to a capability to provide fine diagnosis for invalid entailments.

The current version of Spen improves on the ones reported in [6, 8] in several directions. First, we introduced caching of constructions and results obtained from checking simple entailments in order to increase its efficiency. Second, the wrappers calling the SAT and SMT solvers have been refined to generate smaller formulas and to exploit the incrementality feature of underlying solvers. Third, we improved the diagnosis produced by Spen. For satisfiability checking, Spen now provides either a model of a satisfiable formula or an unsatisfiable core; for entailment checking, Spen provides a proof witness for valid entailments and a diagnostic information otherwise.

Spen has been successfully tested on a quite large benchmark. The first version of Spen participated in the SL-COMP’14 contest [15] where it won one of its divisions and was second in another one. The later extensions now allow Spen to handle a richer fragment than those considered in the competition. Moreover, the improvements above lead to better execution times (e.g., by 10% within the SL-COMP’14 division won by the first version of Spen and by 30% on the division where Spen was the second).

Spen is not the only solver for SL. The existing solvers differ in the fragment considered (Cyclist [2], Slide [9]) and/or the techniques used (Asterix [12], Dryad [14], GRASShopper [13], Sleek [4]). A detailed comparison with these solvers is beyond the scope of this paper—we refer the reader to the survey in [6, 8, 15].

2 Logic Fragment

Spen deals with decision problems in a fragment of SL, denoted as \(\mathsf {SL^{ID}}\), that combines the symbolic heaps fragment of SL [1] with user-defined inductive predicates describing various kinds of lists (possibly nested, cyclic, or equipped with skip links) or trees, possibly extended with data constraints.

Syntax: We write X, Y, Z to denote location variables, d to denote data variables, and x, y, z for both kinds of variables. We use the vector notation \(\vec {x}\) to abbreviate tuples. We denote by \(\rho \) the tuples built from pairs of field labels and variables that specify structured values. We assume a finite set \(\mathcal {P}=\{P_1, \ldots , P_n\}\) of predicate symbols, each with an associated arity, and a special location variable \(\mathsf{nil}\). A symbolic heap formula \(\psi \) is a formula of the form \(\exists \vec {x}\cdot \varPi \wedge \varSigma \) where \(\varPi \) is a pure formula and \(\varSigma \) is a spatial formula with the following syntax:

Here, \(\varDelta \) is a constraint over data variables. We let it unspecified, though Spen presently supports the first-order theory over multisets of integers with integer linear constraints. The spatial atoms (i.e., the empty heap, the heap cell allocated at X, resp. the heap region shaped by some predicate \(P\in \mathcal {P}\)) are composed by the separating conjunction “\(*\)”. An \(\mathsf {SL^{ID}}\) formula \(\varphi \) is a set of symbolic heaps interpreted as a disjunction \(\vee _i\psi _i\).

Predicates \(P\in \mathcal {P}\) are defined by a set of inductive rules of the form \(\psi \Rightarrow P(X,\vec {x})\) where \((X,\vec {x})\) is a tuple of distinct variables including all free variables in the symbolic heap \(\psi \) (the rule body). X is called the root node of the heap segment defined by P. A rule is called a base rule if its spatial part is \(\mathtt {emp}\), i.e., an empty heap; otherwise, it is an inductive rule.

Fragments: Spen considers a restricted class of inductive rules such that the defined predicates specify (possibly empty) heap segments connecting (by location fields) the root location X with all locations in the heap or \(\mathsf{nil}\). The restrictions have been defined formally in [6, 8]. They mainly require, for each inductive predicate P, the presence of a unique base rule and inductive rules where the root X points to a memory cell that contains at least one field from which another heap specified by P starts. The fragment defined in [6], called \(\mathsf {SL^{ID}_{L}}\), can describe various kinds of lists that can be singly- or doubly-linked, cyclic, nested, and can have skip links. It does not permit data constraints and inductive tree structures. On the other hand, the fragment \(\mathsf {SL^{ID}_{D}}\) defined in [8] permits data constraints and can describe tree structures of bounded width, such as sorted list segments, AVL trees, binary search trees, but not nested cyclic lists.

Decision Problems: For both fragments above, Spen considers the problems of checking satisfiability of a formula, i.e., checking whether \(\models \varphi \) holds, and the validity of an entailment \(\varphi \Rightarrow \varphi '\) where the symbolic heaps of \(\varphi '\) can be quantified only over data variables. A simple example of an entailment problem in \(\mathsf {SL^{ID}_{L}}\) considered by Spen is:

$$\begin{aligned} \exists Y,W .~\mathtt {X} \ne \mathtt {Z}~\wedge ~ \mathtt {X} \mapsto \{(\mathtt {next}, Y)\} *\mathtt {sll}(Y, W) *W \mapsto \{(\mathtt {next}, \mathtt {Z})\} \quad \mathop {\Rightarrow }\limits ^{?}\quad \mathtt {sll}(\mathtt {X}, \mathtt {Z}), \end{aligned}$$

which, intuitively, checks whether a composition of two memory cells specified by the points-to atoms \(\mathtt {X} \mapsto \{(\mathtt {next}, Y)\}\) and \(W \mapsto \{(\mathtt {next}, \mathtt {Z})\}\) and the predicate atom \(\mathtt {sll}(Y, W)\) describes a set of heaps that are all also models of the predicate \(\mathtt {sll}(\mathtt {X}, \mathtt {Z})\) defining an acyclic singly-linked list segment between \(\mathtt {X}\) and \(\mathtt {Z}\).

Fig. 1.
figure 1

Spen workflow for satisfiability checking

Full size image

3 Satisfiability Checking

Given a set of inductive definitions \(\mathcal {P}\) and a symbolic heap \(\psi \), the procedures for checking satisfiability in Spen follow the workflow given in Fig. 1. The satisfiability checking of an \(\mathsf {SL^{ID}}\) formula \(\varphi \) makes a classic use of this basic procedure. The crux of the procedures for both fragments is the definition of a boolean formula \({B}[{\psi }]\), called boolean abstraction, such that the data-free part of \(\psi \) is satisfiable iff \({B}[{\psi }]\) is satisfiable [6, 7].

Once the boolean abstraction \({B}[{\psi }]\) is computed, Spen queries a SAT solver (currently, minisat Footnote 2) for the satisfiability of \({B}[{\psi }]\). If \({B}[{\psi }]\) is unsatisfiable, Spen can return an unsatisfiable core of \(\psi \), deduced from an unsatisfiable core of \({B}[{\psi }]\). If \({B}[{\psi }]\) is satisfiable and \(\psi \in \mathsf {SL^{ID}_{L}}\), Spen has the option of returning a model of \(\psi \) obtained from a model of \({B}[{\psi }]\) by unfolding predicate atoms corresponding to non-empty heap segments. The unfolding of predicate atoms is done twice to emphasize the non-emptiness of the segment. For \(\psi \in \mathsf {SL^{ID}_{D}}{}\), the satisfiability checking continues by constructing a formula \(\varDelta _\psi \) that conjuncts the data part of \(\psi \) with the data parts obtained by unfolding the non-empty heap segments given by the model of \({B}[{\psi }]\). To check the satisfiability of \(\varDelta _\psi \), Spen queries an SMT solver for the theory of multisets with integer data (currently, Spen implements a wrapper for the UFLIA theory of z3 [5]).

If the boolean abstraction \({B}[{\psi }]\) is satisfiable, it is then used to normalize the spatial part of \(\psi \), which is a step used by entailment checking too. This process saturates the pure part of \(\psi \) with (dis-)equalities between locations variables and removes predicate atoms that correspond to empty heap segments, producing a normalized formula \(\psi '\).

Fig. 2.
figure 2

Spen workflow for entailment in \(\mathsf {SL^{ID}_{L}}\)

Full size image

4 Entailment Checking

To check the validity of an entailment \(\varphi _1\Rightarrow \varphi _2\), Spen uses a sound procedure to deal with disjunctive formulas: it checks that for every disjunct \(\psi _1\) in \(\varphi _1\), there is a disjunct \(\psi _2\) of \(\varphi _2\) such that \(\psi _1\Rightarrow \psi _2\). The procedure for deciding the validity of entailments between symbolic heaps follows the workflows given in Figs. 2 and 3 (the theoretical foundations were established in [6, 8]). The two formulas are first checked for satisfiability and normalized using the procedures from Sect. 3. If one of the two formulas is unsatisfiable, then the validity of the entailment can be already determined, e.g., if \(\psi _1\) is unsatisfiable then the entailment is valid. When both formulas are satisfiable, Spen offers two different procedures tuned for each fragment of \(\mathsf {SL^{ID}}\).

For the fragment \(\mathsf {SL^{ID}_{L}}\), Spen reduces the entailment problem \(\psi _1\Rightarrow \psi _2\) to a set of entailment queries of the form \(\psi _1[a]\Rightarrow a\), called simple entailments, where \(\psi _1[a]\) is a sub-formula of \(\psi _1\) and a is a (points-to or inductive) spatial atom of \(\psi _2\) (there will be one such entailment for each spatial atom a in \(\psi _2\)). Intuitively, the sub-formula \(\psi _1[a]\) describes the region of a heap modelled by \(\psi _1\) that should satisfy a. The procedures for computing \(\psi _1[a]\) and testing simple entailments use an intermediary graph representation of symbolic heap formulas, called an SL-graph and denoted \(G[\psi ]\). Basically, nodes of \(G[\psi ]\) represent sets of aliased variables according to the pure part of \(\psi \), and edges represent dis-equalities and spatial atoms of \(\psi \), e.g., a spatial atom \(P(X,Y,\vec {x})\) is represented by a directed edge from X to Y labeled by \(P(\vec {x})\). Thus, when a is a predicate atom \(P(X,Y,\vec {x})\), \(\psi _1[a]\) is obtained from the SL-graph of \(\psi _1\) by selecting the edges reachable from X and co-reachable from Y. The graph selected for \(\psi _1[a]\) is transformed into a tree \(t_1\), which is tested for membership in the language of a tree automaton built from the rules defining P for the atom \(a = P(X,Y,\vec {x})\).

Fig. 3.
figure 3

Spen workflow for entailment in \(\mathsf {SL^{ID}_{D}}\)

Full size image

For the fragment \(\mathsf {SL^{ID}_{D}}\), Spen implements a proof search strategy for the entailment problem \(\psi _1\Rightarrow \exists \vec {d}.\ \psi _2\). The strategy computes a sequence of formulas \(\exists \vec {d}^1.\ \psi _1^1,\ldots ,\exists \vec {d}^n.\ \psi _1^n\) such that (1) \(\exists \vec {d}^i.\ \psi _1^i\Rightarrow \exists \vec {d}^{i+1}.\ \psi _1^{i+1}\) and (2) \(\exists \vec {d}^n.\ \psi _1^n\) is syntactically equivalent to \(\exists \vec {d}.\ \psi _2\). The entailments in point (1) are obtained by applying the inductive rules and lemmas obtained automatically thanks to restriction required on inductive definitions. The procedure requires to check entailments between data constraints, which is done using the previously mentioned wrapper to the SMT solver.

For both procedures, when the input entailment \(\psi _1\Rightarrow \exists \vec {d}.\ \psi _2\) holds, Spen has the option of providing a proof witness that either indicates the fact that \(\psi _1\) is unsatisfiable or it consists of the normalized forms of \(\psi _1\) and \(\psi _2\) and the mapping of sub-formulas in \(\psi _1\) to atoms of \(\psi _2\). When the input entailment is not valid and the procedure terminates, Spen provides a diagnosis that explains why the entailment fails.

Table 1. Experimental results on an Intel(R) Core(TM) i7-2600 CPU at 1.60 GHz
Full size table

5 Experimental Results

Spen has been applied to a benchmark of 578 problems (available in the repository), 90% obtained from verification conditions of iterative programs on complex dynamic data structures. The remaining problems are crafted to test the capabilities of the solver. Tables 1 and 2 provide an overview of results obtained by Spen on this benchmark.

The benchmark of \(\mathsf {SL^{ID}_{L}}\) problems includes three divisions of SL-COMP’14: satisfiability and entailment problems for acyclic singly linked lists (sll0_sat resp. sll0_entl), and entailment checking for formulas describing more complicated types of linked lists, e.g., doubly-linked lists, skip lists, and nested lists (FDB_entl). Spen spends less than 0.05 s on 90% of the problems with the maximum time of 0.5 s; these times include calls to a SAT solver. The benchmark FDB_entl \(^+\) includes the problems not in the SL-COMP’14 benchmark (e.g., formulas describing lists of cyclic lists). The reported times in the last column have been obtained in 2014 on the StarExecFootnote 3 platform.

Table 2. Results for \(\mathsf {SL^{ID}_{D}}\)
Full size table

The benchmark of \(\mathsf {SL^{ID}_{D}}\) problems (see Table 2) includes verification conditions for proving the correctness of iterative procedures (delete, insert, search) over recursive data structures storing integer data: sorted lists, binary search trees, AVL trees, and red-black trees. Spen spends less than 0.4 s on each problem, including calls to SAT and SMT solvers. The first three lines of Table 1 demonstrate that the two approaches implemented in Spen (based on tree automata—column “\(\textsc {Spen}_{\mathsf {L}}\)”—and on proof search—column “\(\textsc {Spen}_{\mathsf {D}}\)”) are not only complementary but also comparable on the common fragment. The improvements discussed in this paper reduce the execution times by 10% within the division sll0_entl and by 30% within FDB_entl w.r.t. the old version [6].