Constantin Enea
email: cenea@irif.fr

Ondřej Lengál
email: lengal@fit.vutbr.cz

Sighireanu Mihaela

Tomáš × Vojnar
email: vojnar@fit.vutbr.cz

Mihaela Sighireanu
email: sighirea@irif.fr

Compositional Entailment Checking for a Fragment of Separation Logic

Keywords: program analysis, separation logic, decision procedure, tree automata

HAL is

Introduction

Automatic verification of programs manipulating dynamic data structures is challenging because it requires reasoning about complex program configurations having the form of graphs of an unbounded size. One needs expressive formalisms to represent such configurations that are also efficient when used for checking or synthesising inductive invariants. Separation logic (SL) [?,?] has emerged as one of the most promising formalisms, offering both high expressiveness and scalability. The latter is due to its support of compositional reasoning based on the separating conjunction * and the frame rule, which states that if a Hoare triple {φ}P {ψ} holds and P does not alter free variables in σ, then {φ * σ}P {ψ * σ} also holds. Therefore, when reasoning about P , one has to manipulate only specifications for the heap region altered by P . SL is usually combined with higher-order inductive definitions describing the data structures manipulated. Since general inductive definitions entail undecidability [?], various decidable fragments of SL have been defined in the literature [?,?,?,?] by restricting the syntax of inductive definitions and the Boolean structure of formulas.

In this work, we focus on a fragment of SL with inductive definitions expressive enough to describe program configurations (heaps) containing finite nestings of various kinds of singly linked lists (acyclic, cyclic, skip lists, etc.) that are common in practice (Section 8 defines an extension to doubly linked lists). Moreover, if we abstract arrays into lists, this fragment can be used to specify chaining hash tables or data structures used in device drivers [?]. The formulas in this fragment are of the form ∃ #‰ X : Π ∧ Σ where #‰ X is a set of variables, Π is a conjunction of (dis)equalities, and Σ is a set of spatial atoms connected by the separating conjunction. Spatial atoms can be points-to atoms, describing values of pointer fields of a given heap location, or inductively defined predicates, describing data structures of an unbounded size.

We propose a decision procedure for checking the validity of entailments of the form ϕ ⇒ ψ where ϕ is existentially quantified and ψ is a quantifier-free formula. In addition, this procedure includes a sub-procedure for satisfiability checking of existentially quantified formulas. The decision procedure for entailment can be used R#3 in Hoare-style reasoning to check inductive invariants, but also in program analysis frameworks to decide termination of fixpoint computations. As usual, checking entailments of the form i ϕ i ⇒ j ψ j can be soundly approximated by checking that for each i there exists j such that ϕ i ⇒ ψ j .

The key idea for deciding ϕ ⇒ ψ is to partition the spatial part of ϕ into several sub-formulas, each sub-formula corresponding to one spatial atom of ψ. The semantics of the separating conjunction implies that there must exist a partition such that each sub-formula of ϕ implies a different atom of ψ. In this way, we reduce the original entailment problem to the problem of checking a set of simpler entailments ϕ P ⇒ P (. . .), where ϕ P is a sub-formula of ϕ and P (. . .) is an inductive predicate from ψ. This reduction shows that the compositionality principle holds not only for deciding the validity of Hoare triples, but also for deciding the validity of entailments. Identifying a suitable partition of ϕ requires being able to infer all (dis)equalities implied by the spatial atoms. The inference step is performed by translating ϕ into an equisatisfiable Boolean formula and checking whether Boolean formulas denoting individual (dis)equalities are consistent with it.

Checking simple entailments ϕ P ⇒ P (. . .) relies on representing all possible unfoldings of an inductive predicate using a tree automaton (TA). The validity of ϕ P ⇒ P (. . .) is reduced to testing membership of a tree derived from ϕ P in the language of a TA A[P ] derived from P (. . .). The tree encoding of ϕ P preserves certain edges of its Gaifman graph (cf. [?]), called backbone edges, and re-directs other edges to new nodes, related to the original destination by special symbols. Roughly, such a symbol may be a variable labelling the original destination, or it may show how to reach the original destination using backbone edges only.

The presented decision procedure is sound and complete for the fragment (defined in Section 2), and it is polynomial-time modulo an oracle for deciding unsatisfiability of Boolean formulas. Practically, we have applied it successfully on verification conditions obtained from programs using singly/doubly linked nested lists and skip lists. The results show that our procedure does not only have a theoretically favorable com-plexity, but also behaves nicely in practice (our implementation in the tool SPEN won one gold and two silver medals in the competition of SL solvers SL-COMP'14 [?]). The procedure also offers the benefit of compositionality, which can be exploited within larger verification frameworks by caching simple entailment queries. Related Work. Several decision procedures for fragments of SL have been introduced, e.g., [?,?,?,?,?,?,?,?,?,?,?]. Some of these works [?,?,?,?] consider the restriction of our SL fragment to a single inductive predicate describing singly linked lists. In particular, Cook et al. [?] prove that the satisfiability/entailment problem can be solved in polynomial time. Piskac et al. [?] show that the Boolean closure of the fragment in [?] can be translated to a decidable fragment of first-order logic, which implies that the satisfiability/entailment problem can be decided in NP/co-NP. A similar idea has been used in [?] to deal with an SL fragment able to describe tree-shaped data structures. A fragment of SL covering overlaid nested lists has been introduced in Enea et al. [?]. This fragment is incomparable to the one proposed in this paper, e.g., it cannot describe nestings of cyclic or doubly linked lists while it is able to deal with data structures sharing the same set of objects. Iosif et al. [?,?] consider more expressive SL fragments (able to describe, for instance, trees with parent pointers or trees with linked leaves), for which the complexity of the entailment problem is much higher compared to the decision procedure proposed in this paper. In particular, [?] reduces the validity of an entailment ϕ ⇒ ψ to language inclusion on TAs recognising models of ϕ and ψ respectively (which is EXPTIME-complete in general). In contrast, our decision procedure deals with the Boolean structure of the SL formulas using SAT solvers and reduces the validity of the simple entailments ϕ P ⇒ P (. . .) to the membership problem for TAs (which is in PTIME). Moreover, [?] can also deal with various forms of trees, but it cannot deal with structures of zero length and with some forms of structure concatenation (such as concatenation of two DLL segments), which we can handle.

Several decision procedures for extensions of SL with data constraints have been proposed. The decision procedure [?,?] discussed above allows to include data constraints over list and tree shape predicates, but fails to encode size and multiset constraints. The fragment introduced in [?] captures Presburger constraints over data and sizes of linear data structures, mainly singly and doubly liked lists and lists with tail pointers. The authors show that satisfiability and entailment is decidable for this fragment. The procedure for satisfiability checking extends our Boolean abstraction to an abstraction that uses quantifier free Presburger formulas, which leads to a complexity in NP. The entailment checking is based on graph homomorphism and shown to be in Π P 3 mainly due to checking entailment over size and data constraints. The authors say that they believe that an extension to more complex shapes, including nested data structures, is possible, but leave this question open. For a general frag-R#3 ment with inductive definitions and data constraints (including size and multiset), [?] designs incomplete proof search techniques based on user-provided lemmas and translation to SMT. For the sub-fragment dealing only with trees and nested lists with data, size, and multiset constraints, Enea et al. [?] propose an incomplete entailment checking procedure based on proof search, which applies lemmas generated automatically from the inductive definitions. In comparison, our work does not consider data constraints, but allows more general nested list shapes, such as circular nested lists.

Brotherston et al.

[?] define a generic automated theorem prover relying on the notion of cyclic proofs and instantiate it to prove entailments in a fragment of SL with inductive definitions and disjunctions more general than what we consider. Their entailment checking procedure is, however, incomplete in general. Brotherston et al. [?] define a decision procedure for satisfiability checking in a more expressive fragment of SL, which is EXPTIME-complete in general and in NP when restricted to our fragment. As discussed above, our procedure also tests satisfiability by means of a reduction to Boolean satisfiability, which is also used to infer (dis)equalities implied by the spatial atoms of an SL formula. Satisfiability checking for fragments of SL with data constraints are considered in [?,?]. Le et al. [?] present a semi-decision procedure for satisfiability based on unfolding of inductive definitions combined with over-approximation of SL formulas by first-order logic formulas using SMT solvers.

R#3

This work is an extension of [?]. We consider a slightly smaller class of inductive definitions with an additional restriction on the nesting of lists (see Constraint 2 in Section 2.3). This simplification allows a simpler presentation and, to the best of our knowledge, does not remove any inductive definition of practical interest. Thanks to new insights, we improved the construction in Section 7.3, decreasing the complexity of the complete decision procedure from exponential to polynomial. We also optimise the implementation of the decision procedure and provide an updated evaluation.

Contribution. Overall, the contribution of this work is a novel decision procedure for a rich class of verification conditions with singly (or doubly) linked lists, nested lists, and skip lists. As discussed in more detail in the previous paragraphs, decision procedures for expressive fragments of SL are still rare. Indeed, we are not aware of any techniques that could decide the class of verification conditions considered in this work at the same level of efficiency. In particular, compared to other approaches using TAs [?], our procedure is (i) compositional as it uses TAs recognising formulas entailing one predicate atom, not arbitrary formulas, and (ii) based on the (PTIME) membership problem for TAs compared to their (EXPTIME) inclusion problem.

Separation Logic Fragment

Our logic is a fragment of the symbolic heaps fragment [?] of Separation Logic [?]. The fragment specifies sets of configurations of programs manipulating the heap. A program configuration is given by the state of its stack and of its heap. We consider a memory model where the heap is abstracted by a collection of disjoint memory regions, called records. We denote by Locs the set of locations at which heap records are stored. Records are sets of fields, each field storing a reference to a record location. The record types are fixed by type definitions that also define F, the set of field names. Wlog, we assume that different record types declare pairwise disjoint sets of field names. A program manipulates the heap by creating records, setting and accessing their fields, and freeing them. For this, it uses a set of of program variables Vars stored on the program stack. We assume that Vars contains the null constant.

Syntax

The syntax of the Separation Logic fragment we consider is given in Fig. 1. Record locations that are not stored in program variables are addressed using a set of logical variables LVars disjoint from Vars.

x, y ∈ Vars

program variables f ∈ F fields X, Y ∈ LVars logical variables P ∈ P predicates #‰ F ∈ (Vars ∪ LVars) * vectors of variables E, F ::= x | X ρ ::= (f, E) | ρ, ρ records
Π ::= E = F | E = F | Π ∧ Π pure formulas Σ ::= emp | E → {ρ} | P (E, #‰ F ) | Σ * Σ spatial formulas ϕ ::= ∃ #‰ X : Π ∧ Σ formulas
Fig. 1 The syntax of the considered separation logic fragment

An SL formula is an existentially quantified conjunction of a pure formula Π and a spatial formula Σ. Wlog, we assume that existentially quantified logical variables have unique names. The set of program variables used in a formula ϕ is denoted by pv (ϕ). By ϕ(

#‰ E) (resp. ρ( #‰ E))
, we denote a formula (resp. a set of field-variable pairs) whose set of free variables is #‰ E, and we use free(ϕ( #‰ E)) and free(ρ( #‰ E)) to denote #‰ E. Pure formulas characterise the stack of the program using (dis)equalities between location variables. Given a formula ϕ, pure(ϕ) denotes its pure part Π. We allow set operations to be applied on vectors, i.e., vectors can be treated as sets of their elements. Moreover, E = #‰ F is a shorthand for Fi∈ #‰ F E = F i . The atomic spatial formula emp denotes an empty heap. The points-to atom E → {(f i , F i )} i∈I denotes a heap containing a record at the location labelled by E whose field f i points to F i , for all i. Wlog, we assume that each field f i appears at most once in the set of pairs {(f i , F i )} i∈I . The separating conjunction * specifies the union of two disjoint heaps. The predicate atom P (E, #‰ F ) specifies a heap fragment described by the predicate P and delimited by its arguments, i.e., all locations it represents are reachable from E and allocated on the heap, except the locations in #‰ F . The fragment is parameterised by a set P of inductively defined predicates. An inductive definition of P ∈ P is a finite set of rules of the form P (X, #‰ Y ) ::= ∃ #‰ Z : Π ∧Σ. In this work, we consider only inductive definitions for possibly empty nested list segments, defined formally in Section 2.3.

Semantics

Formulas of our SL fragment are interpreted over pairs (S, H) where S models the program stack and H the program heap. The stack S : Vars ∪ LVars → Locs maps variables to locations. The heap H : Locs × F Locs is a partial function that defines values of fields for some of the locations in Locs. The domain of H is denoted by dom(H), and the set of locations in the domain of H is denoted by ldom(H). We say that a location is allocated in (S, H) or that (S, H) allocates iff belongs to ldom(H), and we say that a variable E is allocated iff the location S(E) is allocated. A location (resp. variable) which is not allocated is called dangling. A sub-model of (S, H) is a pair (S , H ) such that S ⊆ S , H ⊆ H , and for any ∈ ldom(H ) and f ∈ F, it holds that H ( , f ) = H( , f ), i.e., a location in the domain of a sub-model is included with all its fields defined in the model.

The set of models satisfying a formula ϕ is given by the relation (S, H) |= ϕ defined in Fig. 2. The semantic rules are standard except the predicate atom where the model satisfying a predicate P (E, #‰ F ) cannot allocate any variable in #‰ F as these variables are considered not to be in its domain (which differs, e.g., from the semantics in [?]). A model satisfying this property is called well-formed wrt the atom P (E, #‰ F ). The set of models of a formula ϕ is denoted by [[ϕ]]. Given two formulas ϕ 1 and ϕ 2 , we say that ϕ 1 entails ϕ 2 , denoted by

(S, H) |= E = F iff S(E) = S(F ) (S, H) |= E = F iff S(E) = S(F ) (S, H) |= ϕ ∧ ψ iff (S, H) |= ϕ and (S, H) |= ψ (S, H) |= emp iff dom(H) = ∅ (S, H) |= E → {ρ} iff dom(H) = {(S(E), f i ) | (f i , E i ) ∈
::= ∃ #‰ Z : Π ∧ Σ) ∈ P s.t. (S, H) |= ∃ #‰ Z : (Π ∧ Σ)[E/X, #‰ F / #‰ Y ] and ldom(H) ∩ {S(F ) | F ∈ #‰ F } = ∅ (S, H) |= ∃X : ϕ iff ∃ ∈ Locs s.t. (S[X ← ], H) |= ϕ
ϕ 1 ⇒ ϕ 2 , iff [[ϕ 1 ]] ⊆ [[ϕ 2 ]]
. By an abuse of notation, ϕ ⇒ E = F (resp. ϕ ⇒ E = F ) denotes the fact that E and F are interpreted to the same location (resp. different locations) in all models of ϕ.

Inductive Definitions for Nested Lists

We consider a class of restricted inductive definitions that are expressive enough to deal with intricate singly linked lists (including simple lists, lists of circular lists, skip lists of fixed depth, etc.) while also enabling efficient entailment checking (we also extend our fragment to doubly linked lists in Section 8). We define this class by requiring the following restrictions on the general inductive definitions. Examples of inductive predicates conforming to our restrictions are in Fig. 3. Constraint 1 (Linearity): Each predicate P ∈ P has at least two formal parameters and exactly two rules: (i) an empty base rule of the form P (E, F, #‰ B) ::= E = F ∧ emp specifying an empty list segment, and (ii) an inductive rule with the following syntax, where Σ does not contain occurrences of the atom P :

P (E, F, #‰ B) ::= ∃X tl , #‰ Z : E = {F } ∪ #‰ B ∧ E → {ρ} * Σ mat(P ) * P (X tl , F, #‰ B) (1)
The parameters are divided into three categories: the source (or root) parameter E, the target parameter F , and the vector of border parameters #‰ B. The formula E → {ρ} * Σ is called the matrix of P and denoted by mat(P ).

We use the constraint E = {F } ∪ #‰ B to syntactically denote the semantic constraint that locations for target and border parameters are not allocated in a non-empty heap specified by the predicate (see Fig. 2). Intuitively, the inductive rule of P defines a heap composed of a sequence of sub-heaps specified by the matrix of P between the locations given by the actual source and target parameters.

nlcl(E, F ) ::= ∃Xtl, Z : E = F ∧ E → {(s, Xtl), (h, Z)} * 1+ ls[Z] * nlcl(Xtl, F )
skip lists with three levels: The linear form of inductive definition is essential for our decision procedure in (i) computing the Boolean abstraction and (ii) obtaining an elegant translation of Gaifman graphs of formulas into trees. Relaxing this constraint by allowing nonlinear rules (e.g., trees) or several linear rules (e.g., a list with different next fields) causes awkward form of labels for the tree and tree automata obtained from the rules.

skl 3 (E, F ) ::= ∃Xtl, Z 1 , Z 2 : E = F ∧ E → {(f 3 , Xtl), (f 2 , Z 2 ), (f 1 , Z 1 )} * skl 1 (Z 1 , Z 2 ) * skl 2 (Z 2 , Xtl) * skl 3 (Xtl, F ) skl 2 (E, F ) ::= ∃Xtl, Z 1 : E = F ∧ E → {(f 3 , null), (f 2 , Xtl), (f 1 , Z 1 )} * skl 1 (Z 1 , Xtl) * skl 2 (Xtl, F ) skl 1 (E, F ) ::= ∃Xtl : E = F ∧ E → {(f 3 , null), (f 2 , null), (f 1 , Xtl)} * skl 1 (Xtl, F )
Constraint 2 (Root atom): For each predicate P ∈ P, the formula Σ does not contain points-to atoms. The atom E → {ρ} is called the root atom, and it is denoted by root(P ). Furthermore, the free variables of ρ contain all existentially quantified variables of the inductive rule, and they can only also contain border parameters, i.e.,

{X tl } ∪ #‰ Z ⊆ free(ρ) ⊆ {X tl } ∪ #‰ Z ∪ #‰ B.
Intuitively, this constraint requires that the occurrence of mat(P ) in the next unfolding of P , which has X tl as the root, is pointed to by at least one field from E. This condition is satisfied by all inductive definitions in Fig. 3, but forbids the following inductive definition of list segments of even length (we often omit the base rule):

evenls(E, F ) ::= ∃X 1 , X tl : E = F ∧ E → {(f, X 1 )} * X 1 → {(f, X tl )} * evenls(X tl , F ).
Also, this restriction forbids inductive definitions that are not compositional (see Property 4, pg. 11), such as list segments with fast-forward pointers to the end node:

lstf(E, F ) ::= ∃X tl : E = F ∧ E → {(f, X tl ), (g, F )} * lstf(X tl , F ).
Note that this is not at a loss of expressiveness because such list segments may be obtained using the inductive definition below that defines list segments with all elements pointing to some border location B:

lsb(E, F, B) ::= ∃X tl : E = {F, B} ∧ E → {(f, X tl ), (g, B)} * lsb(X tl , F, B).
Then, lsb(E, F, F ) specifies list segments with pointers to the end node of the list.

Moreover, the constraint forbids inductive definitions where the matrix uses an existentially quantified variable Z not pointed to by the root atom1 , such as, e.g.: nfls(E, F, B) ::= ∃X tl , Y, Z : E = {F, B} ∧ E → {(f, X tl ), (g, Y ), (h, B)} * ls(Y, Z) * nfls(X tl , F, B). To sum up, the second constraint discharges our decision procedure from manipulation of arithmetic constraints on the length of list segments or enumeration of aliasings between the existentially quantified variables #‰ Z used by a rule. Lifting this constraint increases the overall complexity.

Constraint 3 (Nested list segments): For each P ∈ P, the matrix of P contains the root atom * -connected with formulas of the following form (for Q = P ):

Σ ::= Q(Z, U, #‰ Y ) | 1+ Q[Z, #‰ Y ] | Σ * Σ | emp (2) for Z ∈ #‰ Z , U ∈ #‰ Z ∪ #‰ B ∪ {E, X tl }, #‰ Y ⊆ #‰ B ∪ {E, X tl } 1+ Q[Z, #‰ Y ] ≡ ∃Z : mat(Q)(Z, Z , #‰ Y ) * Q(Z , Z, #‰ Y ) (3)
Notice that F does not appear in the matrix of P . The macro

1+ Q[Z, #‰ Y ]
is used to represent a non-empty cyclic (nested) list segment on Z whose shape is described by the predicate Q. We call predicate atoms

Q(Z, U, #‰ Y ) and macros 1+ Q[Z, #‰ Y ] extended predicate atoms.
Intuitively, this constraint requires nested lists to have their sources in #‰ Z , i.e., in a variable referenced by a field from the location of E (due to the previous constraint). Except for X tl , the target of these nested list segments is either a location pointed to by the fields of E (e.g., skl 3 in Fig. 3), a border location in #‰ B (e.g., nll), or E.

The 1+ Q[Z, #‰ Y ]
macro is needed to define nested (non-empty) circular lists; defining them as Q(Z, Z, #‰ Y ) would make them empty (the only rule allowed for instances of predicates with matching source and target parameter is the empty base rule).

The next constraint on the matrix of P is defined using its Gaifman graph [?]. Let Σ be the matrix of some inductive definition P ∈ P. The Gaifman graph of Σ, denoted Gf [Σ], is a labelled graph where: -The set of vertices is given by the set of free and existentially quantified variables in Σ, i.e., {E,

X tl } ∪ #‰ B ∪ #‰ Z .
-Edges represent spatial atoms as follows: let E → {ρ} be the root atom of Σ, then for every (f, X) in {ρ}, Gf [Σ] contains an edge from E to X labelled by f ; for every

Q(Z, U, #‰ Y ), Gf [Σ] contains an edge from Z to U labelled by Q; and for every macro 1+ Q[Z, #‰ Y ], Gf [Σ]
contains a self-loop on Z labelled by Q. See Fig. 4 for an example of a Gaifman graph for the matrix of nlcl.

E X tl Z s h ls Fig. 4 Gf [Σnlcl]
Constraint 4 (Matrix connectedness): Let Σ be the matrix of P ∈ P. Then all infinite paths of Gf [Σ] either form a cycle going through E or start in E and end in a self-loop built from some macro

1+ Q[Z, #‰ Y ]
, and all maximal finite paths start in E and end in a node from #‰ B ∪ {X tl }. Moreover, we require that every vertex of Gf [Σ] has at most one outgoing edge labelled by a predicate.

Intuitively, the constraint requires that every existential variable in an inductive rule appears as the source parameter of exactly one extended predicate atom. This ensures that every existential variable Z is either allocated in the matrix (when the list segment from Z is non-empty or ends in E) or it aliases the target or a border parameter. The inductive definitions given in Fig. 3 satisfy the above constraint. The following inductive definition is, however, forbidden because it contains a dangling variable Z:

npls(E, F, B) ::= ∃X tl , Y, Z : E = {F, B} ∧ E → {(f, X tl ), (g, Y ), (h, Z)} * ls(Y, B) * npls(X tl , F, B
). The constraint also forbids the following inductive definition:

nls2(E, F, B) ::= ∃X tl , Y, Z : E = {F, B} ∧ E → {(f, X tl ), (f 1 , Y ), (f 2 , Z)} * ls(Y, Z) * ls(Z, Y ) * nls2(X tl , F, B
). This is because the Gaifman graph of its matrix contains a loop which is not a selfloop-it traverses the inner vertices represented by variables Y and Z. Such loops are forbidden because they may produce dangling variables when the list segments composing the loop are all empty. Dangling variables are problematic because they may be aliased with any variable occurring outside the occurrence of a predicate, which is difficult to encode in our procedure. The following inductive definition satisfies the matrix constraint because the list segment from Z is a self-loop:

nlls(E, F, B) ::= ∃X tl , Y, Z : E = {F, B} ∧ E → {(f, X tl ), (f 1 , Y ), (f 2 , Z)} * ls(Y, Z) * 1+ ls[Z] * nlls(X tl , F, B).
Finally, the following restrictions limit the use of predicate atoms and fields in inductive definitions of P. For this, we define the relation ≺ P on P by P 1 ≺ P P 2 iff P 2 appears in the matrix of P 1 ; we denote by ≺ * P the reflexive and transitive closure of ≺ P . For example, if P = {skl 1 , skl 2 , skl 3 } (cf. Fig. 3), then skl 3 ≺ P skl 2 ≺ P skl 1 and skl 3 ≺ * P skl 1 . Constraint 5 (No mutual recursion): Given a set of inductive definitions P, ≺ * P is a partial order.

Let F → (P ) denote the set of fields occurring in root(P ). For example, in the inductive definitions in Fig. 3, it holds that F → (nll) = {s, h} and F → (skl 3 ) = F → (skl 1 ) = {f 3 , f 2 , f 1 }. Also, let F * → (P ) denote the union of F → (P ) for all P ≺ * P P . For example, F * → (nll) = {s, h, f }. Constraint 6 (No shared fields): For any two predicates P 1 and P 2 that are incomparable wrt ≺ * P , it holds that F → (P 1 ) ∩ F → (P 2 ) = ∅. Therefore, we forbid predicates named differently but having exactly the same set of models. The last two constraints ensure the soundness of our compositional approach for entailment checking, which selects predicates atoms in the order given by ≺ P .

Moreover, to obtain a unique tree from a formula in our procedure, we require the existence of a total ordering on fields, denoted ≺ F , that complies with the inductive definition of predicates in P. Intuitively, ≺ F shall reflect the order in which the inductive definition of P is unfolded. Therefore, fields used in the root atom E → {ρ} of the matrix of P are ordered before fields of any other predicate called by P . Fields appearing in ρ and going "one-step forward" (i.e. occurring in a pair (f, X tl )) are ordered before fields leading to "inner" locations (i.e. occurring in a pair (f, Z) with Z ∈ #‰ Z ), which are ordered before fields going to the border parameters (i.e. occurring in a pair (f, B) with B ∈ #‰ B). We consider null a constant, not a border variable.

Formally, for a predicate P defined by an inductive rule as in Equation ( 1) (pg. 6), we partition F → (P ) into four sub-sets: (a) F →Xtl (P ) is the set of fields f occurring in a pair (f, X tl ) of ρ, (b) F →Z (P ) is the set of fields f occurring in a pair (f, Z) with Z ∈ #‰ Z , (c) F →B (P ) is the set of fields f occurring in a pair (f, X) with X ∈ #‰ B \ {null}, and (d) F →null (P ) is the set of fields f occurring in a pair (f, null).

Constraint 7 (Totally ordered fields): There exists a total order ≺ F on F such that for all P , P 1 , and P 2 in P:

∀f 1 ∈ F →Xtl (P ), ∀f 2 ∈ F →Z (P ), ∀f 3 ∈ F →B (P ) : f 1 ≺ F f 2 ≺ F f 3 and (4) (f 1 ∈ F → (P 1 ) ∧ f 2 ∈ F → (P 2 ) ∧ f 1 = f 2 ∧ P 1 ≺ P P 2 ) ⇒ f 1 ≺ F f 2 . (5) For instance, if P = {nll, ls} or P = {nlcl, ls}, then s ≺ F h ≺ F f satisfies the constraints above. Also, if P = {skl 2 , skl 1 }, then both f 2 ≺ F f 1 ≺ F f 3 and f 3 ≺ F f 2 ≺ F f 1 are
correct total orderings of fields. Only the last one, however, complies with the constraint above for P = {skl 3 , skl 2 , skl 1 }. So, fields in F →null (P ) shared with another predicate Q are ordered to agree with the ordering of fields in Q; in absence of any ordering constraint, they may be ordered by ≺ F in any possible way.

Properties of Models for Predicate Atoms

The constraints on the inductive definitions, together with the basic syntax and semantics of the introduced SL fragment, including the restriction to well-formed models, induce some properties of the considered models of predicate atoms that are important for the soundness of our procedure. These properties are given in this section.

Some of the properties on well-formed models (S, H) of a predicate atom P (E, F, #‰ B) are expressed using their representation as labelled directed graphs. The heap graph of a model (S, H) has as vertices the locations in ldom(H) ∪ img(H); these locations are labelled by sets of program and logic variables using S -1 . The heap graph edges are labelled by fields such that ( , f, ) is an edge iff H( , f ) = . (Notice that, for certain satisfiable formulas that use only points-to atoms, the Gaifman graph and the heap graph of its model are the same.)

Property 1 (Reachability from root): Any location in (S, H) is reachable from the location S(E).

Proof Constraints 1 and 2 ensure there is a path from the source to the target of a predicate edge and Constraint 4 ensures connectedness of the predicate's matrix.

Property 2 (No inner dangling): Any maximal path of (S, H) starting in S(E) is either cyclic or ends in a location labelled by a variable in {F } ∪ #‰ B. Therefore, only locations labelled by {F } ∪ #‰ B are dangling.

Proof Follows from Property 1 and Constraint 4.

The next property is a consequence of the semantics of formulas-in particular, the restriction to well-formed models of predicate atoms. Property 3 (Precise assertions): For any model (S, H) of a formula ϕ including some predicate atom P (E, F, #‰ B), there exists at most one well-formed sub-model

(S , H ) of (S, H) such that (S , H ) |= P (E, F, #‰ B).
Proof By contradiction. Suppose (S , H ) is the smallest well-formed sub-model (there is at most one due to determinism of heaps) of (S, H) such that (S , H ) |= P (E, F, #‰ B) and that there exists another well-formed sub-model (S , H ) such that (S , H ) |= P (E, F, #‰ B) and (S , H ) is a proper sub-model of (S , H ). It follows that (S , H ) contains an allocated location that is not in (S , H ). From Property 1, it follows that is reachable from S(E), and from the fact that heaps are deterministic, we know that there is an allocated location in (S , H ) such that it is a dangling node of (S , H ), and is reachable from . From Property 2, it follows that ∈ S -1 ({F } ∪ #‰ B). Therefore, (S , H ) allocates a node from {F } ∪ #‰ B, so it is not a well-formed model of P (E, F, #‰ B), which is a contradiction.

Constraints 2-4 imply that inductive definitions are compositional:

Property 4 (Compositional List Segments): For any P ∈ P and any well-formed model (S, H) such that (S, H)

|= P (E, F, #‰ B) * P (F, G, #‰ B) and G is not allocated in (S, H), it holds that (S, H) |= P (E, G, #‰ B).
Proof By induction on the length of left-hand side occurrence of P . For the base rule

E = F , a model (S 1 , H 1 ) |= E = F ∧ emp * P (F, G, #‰ B) also models P (E, G, #‰ B). For the inductive rule, assume that if (S 2 , H 2 ) |= P (X tl , F, #‰ B) * P (F, G, #‰ B) and (S 2 , H 2 ) does not allocate G, then it holds that (S 2 , H 2 ) |= P (X tl , G, #‰ B). Let us consider P (E, F, #‰ B) * P (F, G, #‰ B) such that if we once unfold P (E, F, #‰ B), we get ψ ::= ∃X tl , #‰ Z . E = {F } ∪ #‰ B ∧ mat(P ) * P (X tl , F, #‰ B) * P (F, G, #‰ B). Suppose (S, H) is a model of ψ that does not allocate G. By the induction hypothesis, we infer that (S, H) |= ∃X tl , #‰ Z . E = {G} ∪ #‰ B ∧ mat(P ) * P (X tl , G, #‰ B). From the inductive rule of P , it follows that (S, H) |= P (E, G, #‰ B).
The key for the encoding of SL formulas entailing predicate atoms P (E, F, #‰ B) as trees (see Section 6) is given by the following properties. We call a path simple if it does not pass through the same node repeatedly.

Property 5 (Joining paths): Let (S, H) be a well-formed model of P (E, F, #‰ B) and be an allocated location in (S, H) with multiple incoming edges such that = S(E).

Then there is a unique edge f → with f minimal wrt ≺ F . Moreover, the other incoming edges are last edges of simple paths starting from or .

Proof Constraints 1 and 3 imply that there are two cases: (a) corresponds to the first node of a predicate atom R(. . .) (resp. a macro 1+ R[. . .]) s.t. P ≺ * P R, or (b) is an internal (i.e. not the first) node of R(. . .) (resp. 1+ R[. . .]) or P (E, F, #‰ B). Case (a): From Constraint 1, corresponds to some variable Z ∈ #‰ Z from the non-empty rule of a predicate T s.t. P ≺ * P T ≺ P R. Then, from Constraint 2, the root atom root(T ) contains a pair (f, Z) s.t. f is, by Constraint 7, the least label of edges entering (wrt ≺ F ). Moreover, also by Constraint 7, there are no more fedges entering . Hence, the source of root(T ) plays the role of .

Case (b): From Constraints 2 and 7, there is a pair (f, X tl ) in root(R) or root(P ), respectively, such that f is smaller (wrt ≺ F ) than any other edge entering (which may be, e.g., edges in nested list segments from some #‰ Z variables). Hence, is the predecessor of according to f . The last sentence of the property follows from Constraints 3 and 4, in particular from requirements on the use of inductive predicates and the macro 1+ Q[Z, #‰ Y ], respectively, in the matrix of an inductive rule.

A corollary of the previous property is that for any allocated location with several incoming edges, there exist paths σ, σ , a location that is not an internal location of σ , and an edge label f such that the following holds: S(E)

σ f
→ and either

(i) S(E) σ σ , or (ii) S(E) σ f → σ
. Then, given σσ (resp. σf σ ) and f , we can unambiguously determine σf . In particular, for (i), we can obtain σf by traversing (S, H) from backwards along σσ up to the first node (in fact, ) that defines an f edge to a non-null location. Similarly for (ii). This property is important for the selection of aliasing relations in encoding graphs as trees in Section 6.

Property 6 (Minimal path): For any allocated location in (S, H), there is a path σ min in its heap graph from S(E) to such that for any edge i fi → i+1 in σ min , the label f i is the least (wrt ≺ F ) label among labels of edges entering i+1 .

Proof Follows from the requirement of well-formedness of models of predicate atoms and Properties 1 and 5.

Due to this property, removing edges entering a node that are not labelled by the minimal field keeps the model connected, so we can represent it using a tree.

Compositional Entailment Checking

Algorithm 1: Compositional entailment checking of ϕ 1 ⇒ ϕ 2 for ≺ being any total order compatible with

≺ * P 1 ϕ n 1 ← norm(ϕ 1 ); // normalisation 2 ϕ n 2 ← norm(ϕ 2 ); 3 if ϕ n 1 = false then return true; 4 if ϕ n 2 = false then return false; // pure parts 5 if pure(ϕ n 1 ) ⇒ pure(ϕ n 2 ) then return false; // points-to atoms 6 foreach points-to atom a 2 in ϕ n 2 do 7 ϕ n 1 [a 2 ] ← select(ϕ n 1 , a 2 ); 8 if ϕ n 1 [a 2 ] ⇒ a 2 then return false; 9 mark(ϕ n 1 [a 2 ]); // predicate atoms 10 for P 2 ← max ≺ (P) downto min ≺ (P) do 11 foreach a 2 = P 2 (E, F, #‰ B) in ϕ n 2 s.t. pure(ϕ n 1 ) ⇒ E = F do 12 ϕ n 1 [a 2 ] ← select(ϕ n 1 , a 2 ); 13 if ϕ n 1 [a 2 ] ⇒ sh a 2 then return false; 14 mark(ϕ n 1 [a 2 ]); 15 return isMarked(ϕ n 1 );
We now provide our procedure for reducing the problem of checking validity of entailment between a pair of formulas to the problem of checking validity of entailment between a formula and an atom. In particular, we consider the problem of deciding validity of entailments ϕ 1 ⇒ ϕ 2 where ϕ 2 is free of quantifiers and free(ϕ 2 ) ⊆ free(ϕ 1 ), which usually suffices for checking verification conditions in practice. We assume pv (ϕ 2 ) ⊆ pv (ϕ 1 ); otherwise, the entailment is trivially invalid. The reduction is described in Algorithm 1. The reduction starts by normalisation (described in Section 4), which adds to both formulas all (dis-)equalities implied by their spatial sub-formulas and removes all atoms P (E, F, #‰ B) representing empty list segments, i.e. those where E = F occurs in the pure part. The normalisation of a formula returns false iff the formula is unsatisfiable.

The second step tests entailment between the pure parts of the normalised formulas. This can be done using any decision procedure for quantifier-free formulas in the first-order theory of equality.

Next, for the spatial parts, the procedure uses the function select, described in Sect. 5, to build a mapping from spatial atoms of ϕ n 2 to sub-formulas of ϕ n 1 . The subformula of ϕ n 1 to which an atom a 2 of ϕ n 2 is mapped in this way is denoted as

ϕ n 1 [a 2 ].
The mapping is built by first enumerating the points-to atoms of ϕ n 2 and only then by enumerating its predicate atoms, in a decreasing order wrt ≺ * P . The decreasing order is important for the completeness of the procedure (see Section 9). Intuitively, the formula ϕ n 1 [a 2 ] associated with an atom a 2 of ϕ n 2 describes the region of a heap modelled by ϕ n 1 that should satisfy a 2 . The construction of ϕ n 1 [a 2 ] may fail, implying that the entailment ϕ 1 ⇒ ϕ 2 is not valid. In such a case, select returns emp, causing the algorithm to return false.

For predicate atoms a 2 = P 2 (E, F, #‰ B), handled in the second loop of the algorithm, select is called only if there exists a model of ϕ n 1 where the heap region that should satisfy a 2 is non-empty, i.e. E = F does not occur in ϕ n 1 . In this case, select also checks that for any model of ϕ n 1 , the sub-heap corresponding to the atoms in ϕ n 1 [a 2 ] is well-formed wrt a 2 . This check is needed since all heaps described by a 2 are well-formed (see Section 2.2).

Note that in the well-formedness check above, one cannot speak about ϕ n 1 [a 2 ] alone. Indeed, without the rest of ϕ n 1 , the formula ϕ n 1 [a 2 ] may have models that are not well-formed wrt a 2 even if the sub-heap corresponding to ϕ n 1 [a 2 ] is well-formed for any model of ϕ n 1 . For example, let ϕ n 1 = ls(x, y) * ls(y, z) * z → {(f, t)}, a 2 = ls(x, z), and ϕ n 1 [a 2 ] = ls(x, y) * ls(y, z). If we take models of ϕ n 1 only, the sub-heaps corresponding to ϕ n 1 [a 2 ] are all well-formed wrt a 2 , i.e. they do not allocate the location bound to z. The formula ϕ n 1 [a 2 ] alone has, however, lasso-shaped models where the location bound to z is allocated on the path between x and y.

Once ϕ n 1 [a 2 ] is obtained, one needs to check that all sub-heaps modelled by ϕ n 1 [a 2 ] are also models of a 2 . For points-to atoms a 2 , this boils down to a syntactic identity (modulo some renaming given by the equalities in the pure part of ϕ n 1 ). For predicate atoms a 2 , a special entailment operator ⇒ sh is used. We cannot use the usual entailment ⇒ since ϕ n 1 [a 2 ] may have models that are not sub-heaps of models of ϕ n 1 (as we have seen in the example above).

Definition 1 ϕ n 1 [a 2 ] ⇒ sh a 2 iff all models of ϕ n 1 [a 2
] that are well-formed wrt a 2 are also models of a 2 . Given a formula ϕ and an atom P (E, F, #‰ B), the entailment ϕ ⇒ sh P (E, F, #‰ B) is checked as follows: (1) G[ϕ] is transformed into a tree T [ϕ] by splitting nodes that have multiple incoming edges, (2) the inductive definition of

P (E, F, #‰ B) is used to construct a TA A[P ] such that T [ϕ] belongs to the language of A[P ] only if ϕ ⇒ sh P (E, F, #‰ B). The transformation of graphs G[ϕ] into trees T [ϕ]
is presented in Section 6 while the construction of the TA A[P ] is introduced in Section 7.

If there exists an atom a 2 of ϕ n 2 that is not entailed by the associated sub-formula, then ϕ 1 ⇒ ϕ 2 is not valid. By the semantics of the separating conjunction, the subformulas of ϕ n 1 associated with two different atoms of ϕ n 2 must not share spatial atoms. In order to avoid such a scenario, the spatial atoms obtained from each application of select are marked by the algorithm and cannot be reused in the future. If all entailments between formulas and atoms are valid, then ϕ 1 ⇒ ϕ 2 holds provided that all spatial atoms of ϕ n 1 are marked (which is tested by isMarked).

Graph representations. Some of the sub-procedures mentioned above work on a graph representation of the input formulas, called SL graphs (which are different from the Gaifman graphs of matrices of inductive definitions).

Definition 2 (SL graph) Given a formula ϕ, its SL graph, denoted by G[ϕ], is a directed labelled graph where:

-Each node n represents an equivalence class over the set of variables, i.e., it represents a maximal set of variables equal wrt the pure part of ϕ, and it is labelled by the set of variables Var(n) it represents. For every variable E, we then use Node(E) to denote the node n such that E ∈ Var(n). -The following edges can appear: (1) Undirected disequality edges from Node(E)

to Node(F

) encoding disequalities E = F . (2) Directed points-to edges from Node(E) to Node(E i ) labelled by f i that encode spatial atoms E → {(f 1 , E 1 ), . . . , (f n , E n )}, for 1 ≤ i ≤ n.
(3) Directed predicate edges from Node(E) to Node(F ) labelled by P ( #‰ B) encoding spatial atoms P (E, F, #‰ B).

For simplicity, we identify a formula ϕ with its graph representation G[ϕ]. This representation generalises the one proposed in [?] mainly by labelling directed edges with fields and predicates.

Running example. Below, we use as a running example the entailment ψ 1 ⇒ ψ 2 between the following formulas:

ψ 1 ≡ ∃Y 1 , Y 2 , Y 3 , Y 4 , Z 1 , Z 2 , Z 3 : x = z ∧ Z 2 = z ∧ x → {(s, Z 2 ), (h, Z 1 )} * Z 2 → {(s, y), (h, Z 3 )} * ls(Z 1 , z) * ls(Z 3 , z) * ls(y, Y 1 ) * (6) skl 2 (y, Y 3 ) * ls(Y 1 , Y 2 ) * Y 3 → {(f 2 , t), (f 1 , Y 4 )} * t → {(s, Y 2 )} * Y 4 → {(f 2 , null), (f 1 , t)} ψ 2 ≡ y = t ∧ nll(x, y, z) * skl 2 (y, t) * t → {(s, y)}
The graph representations of these formulas are shown in Fig. 5(a) and (b)2 . The formula ψ 1 specifies a heap including a cell whose location is referenced by the (program) variable x and whose fields s and h point to locations Z 2 and Z 1 The heap between Y 3 and t is a fragment of a two-level skip list with a single element on the ground level. Moreover, the variable t references a cell with the field s pointing to the location of the end of the list segment starting from Y 1 . The only explicit non-aliasing constraint on program variables is x = z. The formula ψ 2 specifies a heap with a nested list segment between locations x and y where all nested list segments end in z (atom nll(x, y, z)) and a skip list segment between locations y and t. It also requires y and t be not aliased.

F Π ::= E=F ∈Π [E = F ] ∧ E =F ∈Π ¬[E = F ] F * ::= E,F variables in ϕ, a =a atoms in Σ [E = F ] ∧ [E, a] ⇒ ¬[F, a ] F Σ ::= a=E →{ρ}∈Σ [E, a] ∧ a=P (E,F, #‰ B )∈Σ ([E, a] ⊕ [E = F ]) ∧ ([E, a] ⇒ B∈ #‰ B ¬[E = B]) F= ::= E 1 ,E 2 ,E 3 variables in ϕ ( [E 1 = E 1 ] ∧ [E 1 = E 2 ] ⇔ [E 2 = E 1 ] ∧ [E 1 = E 2 ] ∧ [E 2 = E 3 ] ⇒ [E 1 = E 3 ] )

Normalisation

Given a formula ϕ, the normalisation procedure norm computes a new formula ϕ that contains all (dis-)equalities among the variables of ϕ that are implied by the existing ones in ϕ and the semantics of separating conjunction. This process may discover that ϕ contains contradictory constraints, i.e., it is unsatisfiable. To infer the implicit (dis-)equalities in a formula, we adapt the Boolean abstraction proposed in [?] for the fragment considered in this paper.

Definition 3 (Boolean abstraction) Given a formula ϕ ∃ #‰ X : Π ∧ Σ, we define the Boolean formula BoolAbs[ϕ] ::= F Π ∧ F Σ ∧ F = ∧ F * where the components of BoolAbs[ϕ] are defined in Fig. 6. The set BV (ϕ) of Boolean variables occurring in BV (ϕ) is defined as:

-[E = F ] ∈ BV (ϕ) for every two variables E and F occurring in ϕ, -[E, a] ∈ BV (ϕ) for every variable E and a spatial atom of the form a = E → {ρ} or a = P (E, F,

#‰ B) in ϕ.
Intuitively, the variable [E = F ] denotes the equality between E and F , while [E, a] denotes the fact that the atom a describes a heap where E is allocated. The components of BoolAbs[ϕ], defined in Fig. 6, have the following meaning: F Π and F Σ encode the atoms of ϕ, F = encodes reflexivity, symmetry, and transitivity of equality, and F * encodes the semantics of the separating conjunction.

Proposition 1 Let ϕ be a formula. Then, BoolAbs[ϕ] is equisatisfiable with ϕ, and, for any variables E and F of ϕ,

BoolAbs[ϕ] ⇒ [E = F ] (resp. BoolAbs[ϕ] ⇒ ¬[E = F ]) iff ϕ ⇒ E = F (resp. ϕ ⇒ E = F ).
For the formula ψ 1 in our running example, i.e. Equation ( 6), BoolAbs[ψ 1 ] is a conjunction of several formulas including:

1. [y, skl 2 (y, Y 3 )] ⊕ [y = Y 3 ], which encodes the atom skl 2 (y, Y 3 ), 2. [Y 3 , Y 3 → {(f 2 , t), (f 1 , Y 4 )}] and [t, t → {(s, Y 2 )}], encoding points-to atoms of ψ 1 , 3. [t = y] ∧ [t, t → {(s, Y 2 )}] ⇒ ¬[y, skl 2 (y, Y 3 )], which encodes the separating conjunction between t → {(s, Y 2 )} and skl 2 (y, Y 3 ), 4. [t = Y 3 ]∧[t, t → {(s, Y 2 )}] ⇒ ¬[Y 3 , Y 3 → {(f 2 , t), (f 1 , Y 4 )}], which encodes the separating conjunction between t → {(s, Y 2 )} and Y 3 → {(f 2 , t), (f 1 , Y 4 )}.
If BoolAbs[ϕ] is unsatisfiable, norm(ϕ) returns false. Otherwise, the output of norm(ϕ) is the formula ϕ obtained from ϕ by (1) adding all (dis-)equalities

E = F (resp. E = F ) such that [E = F ] (resp. ¬[E = F ]) is implied by BoolAbs[ϕ] and
(2) removing all predicate atoms P (E, F, #‰ B) s.t. E = F occurs in the pure part. For example, the normalisations of ψ 1 and ψ 2 are given in Fig. 5(c) and (b). Note that the ls atoms reachable from y are removed because BoolAbs[ψ 1 ] implies that Y 1 and Y 2 are aliasing y (from heap determinism and the non-emptiness of the subheap at location Y 3 ), and thus the list segments between y, Y 1 , and Y 2 are empty. Moreover, BoolAbs[ψ 1 ] implies that y is different from t and z. BoolAbs[ψ 2 ] does not imply additional (dis-)equalities, so ψ 2 is unchanged after normalisation.

The following result is important for the completeness of the select procedure.

Proposition 2 Let norm(ϕ) be the result of the normalisation of a formula ϕ. For any two distinct nodes n and n in the SL graph of norm(ϕ), there cannot exist two disjoint sets of atoms A and A in norm(ϕ) such that both A and A form paths between n and n .

Proof Suppose that norm(ϕ) contains two such sets of atoms between nodes n and n labelled by variables E and F respectively. By the semantics of the separating conjunction, it holds that one of the paths is empty, so that ϕ ⇒ E = F . Therefore, norm(ϕ) does not include all ϕ-implied equalities, contradicting its construction.

Selection of Spatial Atoms

After normalisation and testing entailment of pure parts of the checked formulas, the algorithm starts matching every spatial atom from ϕ n 2 to a set of atoms of ϕ n 1 . For this, it uses the select procedure described in this section.

Points-to atoms. Let ϕ

1 ::= ∃ #‰ X : Π 1 ∧ Σ 1 be a normalised formula. The procedure select(ϕ 1 , E 2 → {ρ 2 }) outputs either the sub-formula ∃ #‰ X : E 1 = E 2 ∧ E 1 → {ρ 1 } if E 1 = E 2 occurs in Π 1 ,
or the sub-formula emp otherwise. The procedure select is called only if ϕ 1 is satisfiable. Consequently, because of the semantics of the separating conjunction, ϕ 1 cannot contain two different atoms E 1 → {ρ 1 } and E 1 → {ρ 1 } such that E 1 = E 1 = E 2 . Also, if there exists no such points-to atom, then ϕ 1 ⇒ ϕ 2 is not valid. Indeed, since ϕ 2 does not contain existentially quantified variables, a points-to atom in ϕ 2 could be entailed only by a points-to atom in ϕ 1 .

In the running example, select(ψ n 1 , t → {(s, y)}) = ∃Y 2 : y = Y 2 ∧ . . . ∧ t → {(s, Y 2 )}. For readability, we have omitted some existential variables and pure atoms.

Predicate atoms. Given an atom a 2 = P 2 (E 2 , F 2 , # ‰ B 2 ), the call to select(ϕ 1 , a 2 ) first builds a sub-graph G of G[ϕ 1 ], which is a candidate for representing a partial unfolding of a 2 in ϕ 1 , and then it checks whether the sub-heaps described by G are well-formed wrt a 2 . If this is not true or if G is empty, then select(ϕ 1 , a 2 ) outputs emp. Otherwise, it outputs the formula ∃ #‰ X : Π 1 ∧ Σ where Σ consists of all atoms represented by edges of the sub-graph G , and Π 1 contains all equalities E 1 = E 2 of Π 1 where either E 1 or E 2 occur in G .

We now have a look at the construction of G in more detail. It is based on

Constraint 4. Let Dangling[a 2 ] = Node(F 2 ) ∪ {Node(B) | B ∈ # ‰ B 2 }. Notice that {F 2 } ∪ # ‰
B 2 are also free variables of ϕ 1 . The sub-graph G is defined as the union of all paths of G[ϕ 1 ] that (1) start in the node labelled by E 2 , (2) consist of edges labelled by fields in F * → (P 2 ) or predicates Q with P 2 ≺ * P Q, and (3) end either in a node from Dangling[a 2 ] or in a cycle, in both cases not traversing through nodes in Dangling[a 2 ]. Therefore, G does not contain edges that start in a node from Dangling[a 2 ], but shall contain a path from Node(E 2 ) to each node in Dangling[a 2 ]. In the running example, the subgraphs returned by select(ψ n 1 , nll(x, y, z)) and select(ψ n 1 , skl 2 (y, t)) are highlighted in Fig. 5(c). If the construction of G succeeds, the procedure select checks that, in every model (S 1 , H 1 ) of ϕ 1 , the sub-heap (S 1 , H 1 ) described by G is well-formed wrt a 2 , i.e., nodes of Dangling[a 2 ] are not interpreted by S 1 in ldom(H 1 ), the set of allocated locations in H 1 . For our running example, for any model of ψ 1 , in the sub-heap modelled by the graph select(ψ n 1 , skl 2 (y, t)) in Fig. 5(c), the variable t should not be (1) interpreted as an allocated location in the list segment skl 2 (y, Y 3 ) or (2) aliased to one of the nodes labelled by Y 3 and Y 4 . The well-formedness test is performed using the below proposition.

Proposition 3 (Well-formedness test) Let a graph G represent a sub-formula of ϕ 1 and a 2 = P 2 (E 2 , F 2 , # ‰ B 2 ) be a predicate atom such that free(G ) ⊇ free(a 2 ). G is well-formed wrt a 2 iff the following conditions hold for each variable V ∈ {F 2 }∪ # ‰ B 2 :

1. For every variable V labelling the source of a points-to edge of G , it holds that ϕ 1 ⇒ V = V . 2. For every predicate edge e included in G that does not end in Node(V ), V is allocated in all models of E = F ∧ (ϕ 1 \ G ) where E and F are variables labelling the source and the destination of e, respectively, and ϕ 1 \G is a formula obtained from ϕ 1 by deleting all spatial atoms represented by edges of G .

Proof (⇒) If G is well-formed, then condition (1) is trivially satisfied. Notice that, if G contains only one predicate edge e, it shall end in Dangling[a 2 ] (by construction of G ), so condition (2) is trivially true. Otherwise, let V ∈ {F 2 } ∪ # ‰ B 2 and e be a predicate edge of G such that Node(V ) ∈ Dangling[e] as in condition (2). Let (S 1 , H 1 ) be a model of ϕ 1 s.t. the sub-heap described by e is not empty. From

E Z 1 Z 2 Z 2 X Z 3 Z 4 F s f 1 f 2 ff ls f f s f 1 f 2 ff f f a) An SL graph G E alias ↑↓[s] alias ↑↓[f 2 ] alias ↑[f 2 ] alias [F ] alias ↑↓[f 2 ] alias ↑[f 2 ] alias [F ] s f 1 f 2 ff ls f f s f 1 f 2 ff f f b)
The tree encoding T [G] of G Fig. 7 An example of encoding an SL graph into a tree Constraint 1, it follows that (S 1 , H 1 ) is also a model of E = F ∧ ϕ 1 , where E and F are the destination and target parameters of e respectively. The hypothesis implies that, for the sub-heap H 1 described by G , S 1 (V ) ∈ ldom(H 1 ). From the semantics of separating conjunction, ldom(H 1 ) = ldom(H 1 ) ldom(H 1 ), where H 1 is the sub-heap described by ϕ 1 \ G . Thus, S(V ) shall belong to ldom(H 1 ) because it is the only set disjoint from ldom(H 1 ) in the model (S 1 , H 1 ) of ϕ 1 .

(⇐) Condition ( 1) guarantees that V is different from all allocated locations represented by sources of points-to edges in G . Condition (2) guarantees that V is not interpreted as an allocated location in a list segment described by a predicate edge of G (this trivially holds for predicate edges ending in Node(V )). If V were not allocated in some model

(S 1 , H 1 ) of E = F ∧ (ϕ 1 \ G ), then one could construct a model (S 1 , H 1 )
of G where e would be interpreted to a non-empty list and S(V ) would equal an allocated location inside this list. Therefore, there would exist a model of ϕ 1 , defined as the union of (S 1 , H 1 ) and (S 1 , H 1 ), in which the heap region described by G would not be well-formed wrt a 2 .

The following proposition provides a test for checking that variables are allocated based on checking unsatisfiability of SL formulas. Note that, by Proposition 1, unsatisfiability of formulas can be decided using the Boolean abstraction BoolAbs.

Proposition 4 Let ϕ ::= ∃ #‰ X : Π ∧ Σ be a formula and V a program variable such that V ∈ pv (ϕ). Let V 1 and f 1 be symbols not occurring in ϕ. V is allocated in every

model of ϕ iff ∃ #‰ X : Π ∧ Σ * V → {(f 1 , V 1 )} is unsatisfiable.

Representing SL Graphs as Trees

We define a canonical representation of SL graphs in the form of trees, which we use for checking ⇒ sh . In this representation, disequality edges are ignored because they have been dealt with previously when checking entailment of pure parts.

Example: We start by explaining the main concepts of the tree encoding using the labelled graph G in Fig. 7(a), which is well-formed wrt some predicate atom P (E, F ) where P specifies some special kind of list segments with nested circular lists (chosen to completely illustrate all the relevant issues). We assume that all nodes in G are reachable from the node labelled by E, which is guaranteed for the graphs constructed by select because of Property 1.

To construct a tree representation of G, we start with its spanning tree (highlighted using bold edges) built using minimal paths as in Property 6. Then, any node with at least two incoming edges, called a join node, is split into several copies, one for each incoming edge not contained in the spanning tree. The obtained tree is given in Fig. 7(b). In order not to lose any information, the copies of nodes are labelled with the identity of the original node, which is kept in the spanning tree. If the original node is labelled by a program variable, say x, the original node and its copies are labelled by alias [x]. Otherwise, since the representation does not use node identities, we assign to every copy of the node a "routing" label describing how the copy can reach the original node using paths in the spanning tree.

For example, if a node n has the label alias ↑[f 2 ], this means that n is a copy of some join node m, where m is the first ancestor of n with an incoming edge labelled by f 2 . Further, n labelled by alias ↑↓[f 2 ] means that the original node m can be reached from n by going up in the tree until the first node with an outgoing edge labelled by f 2 , and then down via the f 2 -labelled edge. The exact definition of these labels can be found later in this section. Intuitively, a label of the form alias ↑[f ] will be used when breaking loops, while a label of the form alias ↑↓[f ] will be used when breaking parallel paths between nodes. Due to Property 5, this set of routing labels is enough to convert an SL graph into a canonical tree representation that can entail a spatial atom from the considered fragment; for arbitrary graphs, this is not the case.

Let G be an SL graph well-formed wrt the predicate atom P (E, F, #‰ B) such that all nodes of G are reachable from the node Root labelled by E. An f -edge of an SL graph is a points-to edge labelled by f or a predicate edge labelled by Q( #‰ Y ) such that the minimum field in F → (Q) wrt ≺ F is f . The tree encoding of G is computed by the procedure toTree(G, P (E, F, #‰ B)) that consists of four consecutive steps that are presented below.

Node marking. First, toTree computes a mapping M, called node marking, that maps each node n to a field in F as follows:

M(n) ::= min ≺ F (F → (P )) if n = Root, min ≺ F {f | f -edge enters n} otherwise. ( 7
)
This means that M(n) is the minimum field wrt ≺ F * among the fields of (points-to or predicate) edges entering node n. For technical reasons, we add the minimum field (wrt ≺ F ) in F → (P ) as the marking of node Root.

For any join node n not labelled by a variable in {E, F } ∪ #‰ B, the spanning tree edge is the f -edge (m, n) such that M(n) = f ; for Root, no incoming edge is in the spanning tree. The soundness of this construction is obtained due to Property 6, which ensures that in any model of P (E, F, #‰ B), all allocated nodes are reachable via paths built using only minimum fields. Subsequently, G is transformed into a tree by splitting the remaining join nodes as follows. Let n be a join node and (m, n) an edge not in the spanning tree of G (and G). The edge (m, n) is replaced in the tree by an edge (m, n ) with the same edge label, where n is a fresh copy of n labelled by:

alias ↑[M(n)] if m is reachable from n in G and n is the first predecessor of n marked with M(n). In Fig. 7(a), this labelling is used on cutting the edge from Z 2 to Z 2 , and substituting it by an edge to a node labelled alias ↑[f 2 ] in Fig. 7(b). -alias ↑↓[M(n)] if there is a node p that is the first predecessor of n with a (nonnull) successor over edge M(n), and the successor is n. In Fig. 7(a), this labelling is illustrated on cutting the edge from Z 1 to Z 2 , and substituting it by an edge to a node labelled alias ↑↓[f 2 ] in Fig. 7(b).

If the relation between n and n does not satisfy the constraints mentioned above, i.e. the formula does not belong to the considered fragment, the result of this step is an error represented by the ⊥ tree. Also note that in the example in Fig. 7, edges over ff were split in two ways, depending on whether the target node is labelled by a variable or not. This will later be important in the construction of the TA recognising unfoldings of predicates. We denote the set of all aliasings over variables Vars ∪ LVars and fields F with ALIAS, formally,

ALIAS = {alias [X] | X ∈ Vars ∪ LVars} ∪ {alias ↑[f ], alias ↑↓[f ] | f ∈ F}.
At the end of these steps, we obtain a tree with labels on edges (using fields f ∈ F or predicates Q( #‰ B)) and labels on nodes of the form alias [. . .]; the root of the tree is labelled by E.

Updating the labels. In the last step, two transformations are done on the tree. First, the labels of predicate edges are changed in order to replace each argument X from the set {F } ∪ #‰ B by alias [X], and the rest of the arguments by alias ↑[M(n)] or alias ↑↓[M(n)], depending on the position of the node n labelled by X wrt the source node of the predicate edge. In the case this is not possible, the algorithm returns ⊥.

Second, as the generated trees will be tested for membership in the language of a TA that accepts node-labelled trees only, the labels of edges are moved to the labels of their source nodes and concatenated in the order given by ≺ F (predicates in the labels are ordered according to the minimum field in their matrix).

We now formally define the structure of the output of the algorithm. Let L denote the set of possible node labels obtained in the previous transformation, i.e. elements of F * (ordered wrt ≺ F ), elements of ALIAS, and predicates P ( #‰ B) for all P ∈ P and #‰ B ∈ ALIAS * . Then the output of toTree(G, P (E, F, #‰ B)) is a tree over labels of the tree encoding, i.e. a mapping t : N * → L such that dom(t) is prefix-closed with the following conditions. Let chlds(n) be the set {i | ni ∈ dom(t)}. Then,

-if t(n) = f 1 • • • f k ∈ F * , then chlds(n) = {1, . . . , k}, -if t(n) = P ( #‰ B) for some P ∈ P and #‰ B ∈ ALIAS * , then chlds(n) = {1}, and -if t(n) ∈ ALIAS, then chlds(n) = ∅.
The following property ensures the completeness of the entailment procedure:

Proposition 5 Let P (E, F, #‰ B) be a predicate atom and G an SL graph. If the procedure toTree(G, P (E, F,

#‰ B)) returns ⊥, then G ⇒ sh P (E, F, #‰ B).
Proof It follows from Properties 5 and 6 that a model of a predicate in our fragment can be translated into a tree using the considered aliasing relations. Therefore, if the procedure toTree(G, P (E, F, #‰ B)) returns ⊥, then G can only correspond to a model of a predicate not in the considered fragment.

7 Tree Automata Recognising Tree Encodings of SL Graphs Next, we proceed to the construction of tree automata A[P ] that recognise tree encodings of SL graphs that entail atoms of the form P (E, F, #‰ B). After defining TAs, we continue with an intuitive description on a typical example, and give a full description of the TA construction later.

Definition 4 (Tree automata) A (nondeterministic) tree automaton (TA) recognising tree encodings of SL graphs is a tuple A = (Q, q 0 , ∆) where Q is a finite set of states, q 0 ∈ Q is the initial state, and ∆ is a finite set of transitions of the form (q, a 1 • • • a n , q 1 • • • q n ) or (q, a, ), where n > 0, q, q 1 , . . . , q n ∈ Q, a i is an SL graph edge label (we assume them to be ordered wrt the same ordering of fields ≺ F as for tree encodings), and a ∈ ALIAS. We use q → a 1 (q 1 ), . . . , a n (q n ) to denote (q, a 1 • • • a n , q 1 • • • q n ) and q → a to denote (q, a, ).

A tree encoding t : N * → L is accepted by A if there exists a mapping ρ :

dom(t) → Q such that: (i) ρ( ) = q 0 , and (ii) for all n ∈ dom(t), if chlds(n) = {1, . . . , k}, then (ρ(n), t(n), ρ(n•1) • • • ρ(n•k)) ∈ ∆.
The set of trees L(A) accepted by A is called the language of A.

Overview of the Construction

q 0 q 1 q 2 q 3 f 1 f 1 P 1 (B) P 1 (B) alias [F ] alias ↑↓[f 1 ] alias [B] f 2 f 3 f 2 f 3 (1) q 0 → f 1 (q 0 ), f 2 (q 3 ), f 3 (q 2 ) (2) q 3 → alias ↑↓[f 1 ] (3) q 2 → alias [B] (4) q 0 → f 1 (q 1 ), f 2 (q 1 ), f 3 (q 2 ) (5) q 1 → alias [F ] (6) q 0 → P 1 (B)(q 0 ) (7) q 0 → P 1 (B)(q 1 ) Fig. 8 Automaton A[P 1 ]
The tree automaton A[P ] is constructed by a procedure starting from the inductive definition of P . If P does not call other predicates, the TA simply recognises the tree encodings of the SL graphs that are obtained by "concatenating" a sequence of either Gaifman graphs representing the matrix of P , Σ(E, X tl , #‰ B), or predicate edges P (E, X tl , #‰ B). In these sequences, occurrences of both types can be mixed in an arbitrary order and in an arbitrary number due to Property 4 (compositional list segments) of inductive definitions in our fragment. Intuitively, this corresponds to a partial unfolding of the predicate P in which there appear concrete segments described by points-to edges as well as (possibly multiple) segments described by predicate edges. Concatenating two Gaifman graphs means that the node labelled by X tl in the first graph is merged with the node labelled by E in the other graph. We first illustrate this on a simplified example.

Consider a predicate P 1 (E, F, B) that does not invoke any other predicates and whose matrix is Σ 1 ::= E → {(f 1 , X tl ), (f 2 , X tl ), (f 3 , B)}. The tree automaton A[P 1 ] for P 1 (E, F, B) has transitions given in Fig. 8. Transitions 1-3 recognise the tree encoding of the Gaifman graph of Σ 1 , assuming the following total order on the fields: f 1 ≺ F f 2 ≺ F f 3 . Transition 4 is used to distinguish the "last" instance of this tree encoding, which ends in the node labelled by alias [F ] accepted by Transition 5. Finally, Transitions 6 and 7 recognise predicate edges labelled by P 1 (B). As in the previous case, we distinguish the predicate edge that ends in the node labelled by alias [F ]. Note that the TA given above exhibits the simple and generic skeleton of TAs accepting tree encodings of list segments of our SL fragment: The initial state q 0 is used in a loop to traverse over an arbitrary number of folded (Transition 6) and unfolded (Transition 1) occurrences of list segments, and the state q 1 is used to recognise the end of the backbone (Transition 5). The other states (here, q 2 and q 3 ) are used to accept alias labels only.

When P invokes other predicates, the automaton recognises tree encodings of concatenations of more general SL graphs, obtained from Gf [mat(P )] by replacing predicate edges with unfoldings of these predicates. On the level of TAs, this operation corresponds to a substitution of transitions labelled by predicates with TAs for the nested predicates. During this substitution, alias [. . .] labels occurring in the TA for the nested predicate need to be modified, in particular, labels of the form alias [V ] are substituted by the marking of Node(V ) wrt the higher-level matrix.

Basic Algorithm for Non-Empty List Segments

We present our algorithm for translating a predicate into a TA in two steps. In this section, we start with the basic algorithm for a predicate that for each nested predicate allows at least one unfolding, and in the next section, we extend the construction to allow empty nested predicates.

Consider the definition of the matrix of a predicate P (E, F, #‰ B) as given in Equations (1) and (2) in Section 2.3. The construction of the automaton A[P ] is described in the following. To ease its presentation, let us suppose that the matrix of P is of the form

Σ(E, X tl , #‰ B) ::= ∃ #‰ Z : E → {(f 1 , Z 1 = X tl ), . . . , (f n , Z n )} * Σ . Wlog, we further assume that f 1 ≺ F • • • ≺ F f n , i.e., f 1 is the minimum field in F → (P ).
The construction uses the SL graph of the formula that represents two unfoldings of the recursive definition of the predicate:3

∃X tl : Σ(E, X tl , #‰ B) * Σ(X tl , F, #‰ B). (8)
The unfolding is done twice in order to capture all markings that may appear in tree encodings that shall be recognised by A[P ], including the ones of the nodes allocated inside the list segment. (Note that in the example in Fig. 7, a single unfolding of the predicate P would not create the marking alias ↑↓[ff ]; the corresponding node would be marked with alias [F ]. On the other hand, any more unfoldings of P do not create any new marking.) We obtain a graph G P by transforming the formula in Equation ( 8) to its SL graph (macros of the form 1+ Q[Z, #‰ Y ] are first expanded according to Equation ( 3)). In the following, we use variables Z 1 , . . . , Z n to denote existentially quantified variables from the first unfolding Σ(E, X tl , #‰ B) and variables Z 1 , . . . , Z n to denote existentially quantified variables from the second unfolding Σ(X tl , F, #‰ B). In the following step, we get T [G P ], the tree encoding of G P , and check that it is not equal to ⊥, otherwise we abort the procedure. Notice that the variable X tl is existentially quantified in the formula, so T [G P ] does not use the aliasing relation alias [X tl ]. Instead, a node that is a copy of the node labelled with X tl in G needs to use either the relation alias ↑[f 1 ] or the relation alias ↑↓[f 1 ], because the marking of Node(X tl ) is f 1 . Recall also that the nodes of G labelled by parameters or existentially quantified variables are kept in the structure of T [G P ] (the tree encoding only cuts some edges and adds new nodes). Therefore, we overload the notation Node(Z) in the following to denote the (non-alias) node of T [G P ] obtained from the node of G P labelled by Z.

The construction starts with an empty automaton A[P ]. It calls the procedure buildTA(P, σ, q 0 , q 1 , m 0 ), which adds states and transitions to A[P ] to recognise tree encodings of unfoldings of the atom P (E, F, #‰ B). This procedure is recursive, because it is called for all atoms Q(U, V, # ‰ W ) inside the formula in Equation ( 8). The arguments of buildTA are the following: P is the predicate called, σ is the mapping of the formal parameters of the predicate to an aliasing relation, q 0 and q 1 are the states to be used for the source resp. the continuation of the construction, and m 0 is the marking of the state q 0 . The state q 0 is chosen as the initial state of A[P ].

Let σ = {E → alias [E], F → alias [F ], # ‰ B → alias [B]} where # ‰ B → alias [B] denotes the set of mappings {B → alias [B] | B ∈ #‰ B}.
The procedure buildTA(P, σ, q 0 , q 1 , f 1 ) consists of the following four steps. . . , v k in this order, we add the transition q(u) → h 1 (q(v 1 )), . . . , h k (q(v k )).

Note that this rule also creates the backbone transitions q 0 →f 1 (q(Node(X tl ))), f 2 (q(Node(Z 2 ))), . . . , f n (q(Node(Z n ))), (9) q(Node(X tl )) →f 1 (q 1 ), f 2 (q(Node(Z 2 ))), . . . , f n (q(Node(Z n ))).

(10) (e) If the call to buildTA is not nested, we also add the transition q 1 → σ(F ).

Observe that the created skeleton is able to accept precisely two unfoldings of the predicate P between E and F such that nested predicates are not unfolded.

II. Accepting non-empty list segments. Next, we make A[P ] accept an arbitrary number of these unfoldings along the minimum field, i.e. f 1 , of the predicate P . To do this, we add in state q 0 the following transitions:

(a) a transition that accepts exactly one unfolding: q 0 → f 1 (q 1 ), f 2 (q(Node(Z 2 ))), . . . , f n (q(Node(Z n ))), (b) a looping transition that allows to insert arbitrarily many unfoldings: q 0 → f 1 (q 0 ), f 2 (q(Node(Z 2 ))), . . . , f n (q(Node(Z n ))).

III. Interleave with predicate edges. We add transitions allowing an arbitrary interleaving of folded and unfolded occurrences of the predicate P :

q 0 →P (σ( #‰ B))(q 0 ) (11)
q 0 →P (σ( #‰ B))(q(Node(X tl ))) (12)
q(Node(X tl )) →P (σ( #‰ B))(q 1 ).

Moreover, if the call to buildTA is not nested, we also add the transition

q 0 →P (σ( #‰ B))(q 1 ) (14)
to accept exactly one instance of predicate P .

IV. Inserting tree automata of nested predicate edges. For each transition inserted in A[P ] of the form: q(Node(R)) → Q( #‰ Y )(q(Node(S))), with Q = P representing a nested predicate atom Q(R, S, #‰ Y ), we recursively call buildTA(Q, σ , q(Node(R)), q(Node(S)), m R ) where σ

= {E → r R , F → r S , # ‰ B → r Y } (note that the definition of Q uses E, F, and #‰ B) such that for any Z ∈ {R, S} ∪ #‰ Y : -if Z ∈ {E, F } ∪ #‰ B then r Z is σ(Z), -if Z ∈ #‰
Z (the set of existentially quantified variables in P ) then r Z is the aliasing relation between Node(R) and Node(Z) in T [G P ],

x 1 x 2 x 3 x 4 x 5 x 6 f 1 f 1 f 2 f 3 f 2 f 1 f 1 f 3 f 2 f 1 a)
The SL graph of a 3-level skip list

x 1 x 2 alias ↑↓[f 2 ] x 3 alias ↑↓[f 3 ] alias ↑↓[f 3 ] x 4 alias ↑↓[f 3 ] x 5 alias ↑↓[f 3 ] x 6 f 1 f 1 f 2 f 3 f 1 f 2 f 1 f 3 f 2 f 1 b)
The tree encoding of the graph in (a)

Fig. 9 Illustration of the issue with possibly empty nested list segments on skl 3 . The label of the node accessible from x 5 over f 1 (labelled with alias ↑↓[f 3 ]) reflects the fact that the second-level skip list from the node x 4 to the node x 6 is empty.

Note that the size of A[P ] (number of states and transitions) is polynomial in the size of the inductive definition (number of variables and atoms) of P and of Q with P ≺ * P Q. The procedure itself is also polynomial, and the membership problem for tree automata is solvable in polynomial time (wrt the size of the input). As a consequence, we conclude that the entailment decision procedure described in this section is polynomial in the size of the input.

The following result states the correctness of the tree automata construction.

Theorem 1 For any predicate atom P (E, F, #‰ B) and any SL graph G, if the tree generated by toTree(G, P (E, F, #‰ B)) is accepted by A[P ], then G ⇒ sh P (E, F, #‰ B).

Proof Follows from the fact that A[P ] accepts trees corresponding to two unfoldings of P (using transitions created in Step I), one unfolding (Step II(a)), and more than two unfoldings (Step II(b)). Moreover, partial unfoldings of P (any interleaving of occurrences of unfoldings of P and P itself along the backbone) are accepted using transitions created in Step III. Transitions that accept all possible (non-empty) unfoldings for nested predicates are inserted in Step IV.

Extending the Basic Algorithm to Possibly Empty Nested List Segments

We now modify the above algorithm to generate TAs accepting unfoldings of P with not only non-empty occurrences of nested predicates, but also empty ones. To show the difficulties of this construction, we consider the SL graph in Fig. 9(a), which is an unfolding of the predicate atom skl 3 (x 1 , x 6 ). The skip list segment between nodes x 1 and x 4 contains a non-empty level-2 skip list, while the level-2 skip list between

x 4 and x 6 is empty. The emptiness of the second segment causes that the tree for the graph uses the alias relation alias ↑↓[f 3 ] for the node reachable from x 5 over f 1 instead of alias ↑↓[f 2 ] (used, e.g., in the node reachable from x 2 over f 1 ). Such trees are, however, rejected by the TA built by the procedure buildTA presented previously.

To fix this problem, apart from allowing empty occurrences of nested predicates in the TA returned by buildTA, we also need to extend the occurrences of aliasing relations alias ↑↓[. . .] to consider all combinations of empty/non-empty occurrences of nested predicates. Indeed, such aliasing relations are used to address the target node of nested predicate atoms in the tree encoding of the matrix of a predicate. The aliasing relations of the form alias ↑[. . .] are not considered because they are used to encode the 1+ Q[Z, #‰ Y ] macro, which describes a non-empty list segment. In [?], we created an exponentially large TA that encodes all possible combinations of empty/non-empty occurrences of nested predicates. Here, we improve the algorithm and construct a TA of a polynomial size that accepts trees that have the right structure but may have some wrong alias labels. An additional polynomial-time check on the result of the membership test determines whether the alias labelling is valid.

Intuitively, the new procedure has the following steps:

1. The tree encoding of G, T [G], is computed using toTree(G, P (E, F, #‰ B)), and the TA A[P ] is obtained using buildTA as in the previous section. 2. Further, A[P ] is modified in such a way that for every predicate-labelled transition, an -transition with the same source and destination nodes is added. After we remove the -transitions using a standard algorithm for -transition elimination, we obtain A • . The automaton A • accepts the same trees as A[P ], but also trees obtained by removing some of the predicate-labelled edges (and for every such a removed edge, merging the source and target nodes together). The aliasing relations in the leaves of these trees may, however, be wrong. For example, A • obtained for skl 3 would reject trees with alias ↑↓[f 3 ] in the nodes accessible from x 5 and x 3 through f 1 in Fig. 9 , where the TA A [P ] is built by pumping all (exponentially many) legal combinations of empty predicate atoms and membership is tested in the standard way.

We now formalise steps 3-5 of isIn(G, P (E, F, #‰ B)). In step 3, we first create the TA A = (Q, q 0 , ∆ ) from A[P ] in such a way, that for every transition of A[P ] of the form q → P ( #‰ B)(p) representing a predicate atom P (. . .) in the matrix of P , we add an -transition of the form q → (p). Then, A • = (Q, q 0 , ∆ • ) is the TA obtained by applying a standard algorithm for removing epsilon transitions on A .

In step 4, a saturation procedure first computes the mapping ω : Q → (F ∪ #‰ B) * such that ω(q) is the sequence of aliases that the node labelled by q in the run of A • on T [G]can (possibly via other aliases) refer to. More precisely, let q ∈ Q be a state such that ∆ • contains a transition q → alias ↑↓[f ] with f ∈ F; due to our construction of A[P ] and A • , there is at most one such transition from q. Let r → g 1 (s 1 ) • • • g n (s n ) be the first transition obtained by traversing the graph of A • backwards from q to q 0 satisfying the following constraints: (i) its right-hand side contains a term g i (s i ) with g i = f , and (ii) ∆ • contains a transition starting in s i and expressing an aliasing relation, i.e., it has one of the forms s i → alias ↑↓[f ] for f ∈ F or s i → alias [X] for X ∈ #‰ B \ {null} (there is at most one such transition from s i , by the construction of A • ). Then, we define ω(q) = f • ω(s i ).

If there is no transition from s i satisfying the above constraints but ∆

• contains s i → alias [null] (if null ∈ #‰ B)
, then we define ω(q) = f • null. (We treat null in a special way in order to match the definition of alias ↑↓[. . .].) For any state q ∈ Q that does not satisfy the above constraints, ω(q) = . Notice that if ω(q) = f 1 • • • f n , then f 1 is the marking used in the alias transition from q; if f i ∈ #‰ B, then i = n, i.e., variables can only occur at the end of the sequence. The saturation returns the TA A [P ] = (Q, q 0 , ∆ ) such that ∆ = ∆ • ∪ q∈Q C(q) where C(q) contains all leaf transitions accepting aliases with markings in ω(q), formally,

C(q) = {q → alias ↑↓[f i ] | f i ∈ ω(q) ∩ F} ∪ {q → alias [X] | X ∈ ω(q) ∩ #‰ B}.
In step 5, the modified tree membership checking algorithm creates a partial mapping µ : T

[G] (F ∪ #‰ B) * that is defined for some leaves of T [G].
Intuitively, µ is used to determine which nested lists of P are assumed to have empty occurrences in T

[G]. Formally, let u ∈ dom(T [G]) be a leaf labelled by alias ↑↓[f i ] (for a field f i ∈ F) or alias [f i ] (for a variable f i ∈ #‰ B).If u is labelled by q in the accept- ing run of A [P ] on T [G], then µ(u) = f 1 • • • f i if ω(q) = f 1 • • • f n for i ≤ n.
Then, for all labelled leaves u of T [G], the modified membership test performs the following checks. Suppose µ(u) = f 1 • • • f i . Then, for all 1 ≤ j < i, we test that the node v accessible from u via alias ↑↓[f j ] references the same node as u, i.e. T [G](v) = T [G](u). Intuitively, this validates that if an alias relation assumes that there is an empty list segment in T [G], there really is one. Moreover, if f i ∈ F, we also test that the node accessible via alias ↑↓[f i ] is not an alias node. If any of the above checks fails, the procedure isIn(G, P (E, F, #‰ B)) returns false, otherwise it returns true.

Theorem 2 For any predicate atom P (E, F, #‰ B) and any SL graph G, the result of isIn(G, P

(E, F, #‰ B)) is true iff G ⇒ sh P (E, F, #‰ B).
Proof (Idea) From the idea of the proof of Theorem 1, we know that the TA A[P ] accepts tree encodings of all models of P with no empty predicate occurrences. The new construction of A [P ] ensures that A [P ] will also accept any tree T obtained from a tree accepted by A[P ] by allowing any predicate that occurs in it to be empty. This shows completeness of the method. On the other hand, the construction of A [P ] accepts trees that do not correspond to any model of P , since some nested list may jump out of the list in which it should be nested. The modified membership test ensures that such trees are rejected, re-establishing soundness of the procedure. The procedure presented above can be extended to check validity of entailments between formulas using more general inductively defined predicates. In this section, we sketch the main idea for the extension to list segments that are finite nestings of both singly linked and doubly linked lists.

E M : h M : f M : f M : s M : s M : h M : f F s s h h f f f b b b f b b f E alias ↑↓ last [f ] alias ↑[h] alias ↑ 2 [f ] alias ↑[h] alias ↑↓ last [f ] alias ↑[h] alias ↑[h] alias [F ] s s h h f f
To describe doubly linked list segments, we extend the class of inductive definitions allowed by Constraint 1 (page 6) by including the following rules: In Equation ( 16), variable P corresponds to the predecessor of E and variable L corresponds to the predecessor of F , i.e. the last element of the list segment. Notice that the above constraints extend the definition used for DLL segments introduced in SL by, e.g., [?]. For instance, to describe DLL segments starting in E, ending in L, and going to F , one can use the following inductive rule: dll(E, F, P, L) ::= ∃X tl : E = F ∧ P = L ∧ E → {(f, X tl ), (b, P )} * dll(X tl , F, E, L). To describe a singly linked list of cyclic doubly linked lists, one may use the following inductive rule: nlcdl(E, F ) ::= ∃X tl , Z : E = F ∧ E → {(s, X tl ), (h, Z)} *

1+ dll[Z] * nlcdl(X tl , F ). (In both cases, we omitted the base rule.)

To deal with the above introduced class of inductive definitions, the main modification of our decision procedure concerns the conversion of SL graphs to trees, i.e. the toTree procedure described in Section 6. More precisely, we have to extend the splitting of join nodes used by this procedure as follows. Recall that, given a join node n in an SL graph G and an edge (m, n) that is not in the spanning tree of G, the splitting operation replaces (m, n) by an edge (m, n ) with the same edge label and n being a fresh copy of n. For the new class of inductive definitions, we have to introduce two additional aliasing labels to describe the path from n to n:

alias ↑ 2 [M(n)] will be used if m is reachable from n in G and n is the second predecessor of n marked with M(n). Intuitively, this label is needed to handle inner nodes of doubly linked lists, which have two incoming edges: one from their successor and one from their predecessor (see Fig. 10). -alias ↑↓ last [M(n)] will be used if there is a node p that is the first predecessor of n marked with M(n), n is reachable from p by going only via M(n) edges, and n has no non-alias successors with the marking M(n). Intuitively, the label is needed for a doubly linked cyclic list to allow referring to the predecessor of the head node of the list (see Fig. 10).

The construction of TAs from Section 7 has to be adapted too since it is based on the tree encoding of SL graphs obtained by unfolding the inductive definition of predicates to be represented. In order to generate all the aliasing relations, it turns out that we have to consider three unfoldings (instead of two) for these predicates. (Note that in the example in Fig. 10, the two unfoldings of the nested DLL do not create the marking alias ↑ 2 [M(f )]-three unfoldings are necessary. On the other hand, four or more unfoldings do not yield any new marking.)

Step I (importing tree encodings) of the algorithm from Section 7.2 can be extended in a trivial way for the new aliasing relations.

Step IV (inserting tree automata of nested predicate edges) is adapted in a similar way to the tree encoding of SL graphs. The other steps are not modified because they are independent of the set of aliasing relations.

Soundness, Completeness, and Complexity

We can now finally state that Algorithm 1 is a decision procedure for our SL fragment.

Theorem 3 Let ϕ 1 and ϕ 2 be a pair of formulas such that ϕ 2 is quantifier-free. Then, Algorithm 1 returns true iff ϕ 1 ⇒ ϕ 2 .

Proof The first part of Algorithm 1 (until line 6) saturates the input formulas with all (non-)aliasing relations between logic variables. It follows from Proposition 1 that this transformation preserves the models of the input formulas. Thus the soundness and completeness of the algorithm is proved for the normalised formulas ϕ n 1 and ϕ n 2 . Soundness, i.e., the fact that if Algorithm 1 returns true, then ϕ 1 ⇒ ϕ 2 . The procedure may return true either at line 3 or line 15. At line 3, the test of unsatisfiability for ϕ n 1 is sound (by Proposition 1) and by the semantics of entailment, false ⇒ ϕ 2 . At line 15, the result is true if (1) the normalised formulas ϕ n 1 and ϕ n 2 are satisfiable, (2) their pure parts satisfy pure(ϕ n 1 ) ⇒ pure(ϕ n 2 ), (3) there is a mapping σ that associates to each spatial atom a 2 of ϕ n 2 a sub-formula σ(a 2 ) of ϕ n 1 entailing a 2 , and Moreover, SPEN participated in three divisions of the first competition of separation logic solvers SL-COMP'14 [?]: division FDB entl containing entailment problems with extended acyclic lists, such as doubly linked lists, nested lists, or skip lists, and divisions sll0a entl and sll0a sat containing entailment respectively satisfiability problems with singly linked lists. The procedure for satisfiability checking computes the Boolean abstraction of the input formula and checks its satisfiability using SAT solvers; its correctness is implied by Proposition 1 and the well-formedness of the inductive definition used (cf. the ls predicate in Fig. 3). SPEN won division FDB entl by a huge margin, solving the set containing all problems in less than a minute; further, note that SPEN is the only tool that correctly answered all problems in this division. In addition to this, SPEN was also placed second in both divisions with singly linked lists, where the first place was won by ASTERIX. Detailed results of this competition are in Table 2 (cf. [?] for the complete description).

Conclusion

This article presents a novel decision procedure for a fragment of SL with inductive predicates describing various forms of lists (singly or doubly linked, nested, circular, with skip links, etc.). The procedure is compositional in that it reduces the given entailment query to a set of simpler queries between a formula and an atom. For solving them, we proposed a novel reduction to testing membership of a tree derived from the formula in the language of a TA derived from a predicate. We implemented the procedure, and our experiments show that it has not only a favourable theoretical complexity, but also efficiently handles practical verification conditions. Moreover, when compared with other tools which competed in the first competition of separation logic solvers SL-COMP'14 [?], SPEN won the first place in one division (being by several orders of magnitude faster and even more successful in correctly deciding some problems), and the second place in two divisions.

In the future, we plan to investigate extensions of our approach to formulas with a more general Boolean structure or using more general inductive definitions. We intend to combine our procedure with some proof search techniques to support formulas with existentially quantified variables or to deal more precisely with disjunctions. Concerning general inductive definitions, we plan to investigate whether some ideas from [?] could be used to extend our decision procedure for entailments between formulas and atoms. From a practical point of view, apart from improving the implementation of our procedure, we plan to integrate it into a complete program analysis framework. In this context, the diagnosis provided by the TA library for a failing membership test may be exploited to provide support for frame inference.

Fig. 2

 2 Fig. 2 The |= relation ( denotes the disjoint union of sets, P is the set of inductively defined predicates, [X/Y ] denotes a substitution of Y by X, and S[X ← ] denotes the function S such that S (X) = and S (Y ) = S(Y ) for any Y = X)

  singly linked lists:ls(E, F ) ::= ∃Xtl : E = F ∧ E → {(f, Xtl)} * ls(Xtl, F ) lists of acyclic lists: nll(E, F, B) ::= ∃Xtl, Z : E = {F, B} ∧ E → {(s, Xtl), (h, Z)} * ls(Z, B) * nll(Xtl, F, B)lists of cyclic lists:

Fig. 3

 3 Fig. 3 Examples of inductive definitions used throughout this paper (we omit all base rules P (E, F, #‰ B) ::= E = F ∧ emp for all predicates P )

Fig. 5 A

 5 Fig.5A running example of an entailment test ψ 1 =⇒ ψ 2 .

Fig. 6

 6 Fig. 6 Definition of the components of BoolAbs[ϕ] with ⊕ denoting xor(atom x → {(s, Z 2 ), (h, Z 1 )}). The list cell at location Z 2 contains a field s referencing the location stored in the program variable y, and a field h referencing the location of Z 3 . The nodes Z 1 and Z 3 are initial nodes of two disjoint singly linked list segments ending in the location z (atoms ls(Z 1 , z) and ls(Z 3 , z)). The node y is the beginning of a singly linked list segment ending in the location of Y 1 (atom ls(y, Y 1 )) and a skip list segment ending in the location of Y 3 (atom skl 2 (y, Y 3 )). The heap between Y 3 and t is a fragment of a two-level skip list with a single element on the ground level. Moreover, the variable t references a cell with the field s pointing to the location of the end of the list segment starting from Y 1 . The only explicit non-aliasing constraint on program variables is x = z.The formula ψ 2 specifies a heap with a nested list segment between locations x and y where all nested list segments end in z (atom nll(x, y, z)) and a skip list segment between locations y and t. It also requires y and t be not aliased.

  Splitting join nodes. The way join nodes are split depends on whether they are labelled by variables in {E, F } ∪ #‰ B or not. First, a graph G is obtained from G by replacing any edge (m, n) with n labelled by some V ∈ {E, F } ∪ #‰ B by an edge (m, n ) with the same label, where n is a fresh copy of n labelled by alias [V ]. In our example, the node labelled with F in Fig. 7(a) is split, and we obtain three nodes labelled by alias [F ] in Fig. 7(b).

I

  . Importing the tree encoding T [G P ]. In the first step, we construct the skeleton of A[P ] by taking T [G P ] and transforming it in the following way:(a) For each node u of T [G P ], we create a unique state q(u) in A[P ], except for the nodes Node(E) and Node(F ), for which we use the states q 0 and q 1 respectively. (b) If the node u is labelled in T [G P ] with an aliasing relation r ∈ ALIAS, we add the transition q(u)→ σ(r) if r is of the form alias [B] for any B ∈ #‰ B and q(u) → r if r is a relation alias [m] for ∈ {↑, ↑↓}. (c) If there is a predicate edge from u to v labelled with Q( #‰ Y ), we add the transition q(u) → Q(β ( #‰ Y , σ))(q(v)) where β ( #‰ Y , σ) changes every Y in #‰ Y according to the following rules: -If Y is an argument of buildTA, it is changed to σ(Y ); if Y isan existentially quantified variable in the formula in Equation (8), m is the marking of Node(Y ), and the relation between u and Node(Y ) is alias [m] for ∈ {↑, ↑↓}, we change Y to alias [m]; otherwise, we abort the procedure. (d) If the node u is the source of points-to edges e 1 , . . . , e k labelled with the fields h 1 , . . . , h k respectively, assuming that h 1 ≺ F • • • ≺ F h k , and entering nodes v 1 , .

Fig. 10

 10 Fig. 10 Tree encodings for lists of nested cyclic doubly linked lists: (left) an SL graph that entails nlcdl(E, F ), (right) the tree encoding of the graph from the left 8 Extension to Doubly Linked Lists

R

  dl (E, F, P, L, #‰ B) ::= E = F ∧ P = L ∧ emp (and Σ from Constraint 3 is changed to Σ ::= Q(Z, U, #‰ Y ) | Q dl (Z, U, Z p , Z l , ∃Z , Z p : mat(Q dl )(Z, Z , Z p , #‰ Y ) * Q dl (Z , Z, Z, Z p , #‰ Y ).

  (b); it would only consider the label alias ↑↓[f 2 ]. 3. A saturation algorithm is applied on A • to obtain A [P ], where more aliasing transitions are introduced. Some of these added transitions do not, however, correspond to aliasings generated by the presence of empty predicate atoms. 4. For this reason, a modified membership algorithm is applied to T [G] and A [P ]. The above procedure, further called isIn(G, P (E, F, #‰ B)), runs in the time polynomial to the size of G and of the inductive definitions in P. It improves the procedure in [?]

It consists of first testing T [G]

∈ A [P ] using a standard algorithm; if it answers false, the procedure returns false. Otherwise, the procedure checks that the aliasing transitions of A [P ] used in the standard membership test correspond to empty occurrences of predicates in T

[G]

. If this check succeeds, the final result is true; otherwise the procedure returns false.

Our former work [?] does not include this constraint, thus the procedure proposed was incomplete.

Points-to edges are depicted as simple lines, predicate edges as double lines, and disequality edges as dotted lines. For readability, we omit some of the labelling with existentially-quantified variables and some of the disequality edges in the normalised graphs.

Note that in the example in Fig.8, we performed some manual minimisation of the result.

Our experiments were performed on a PC with an Intel Core 2 Duo @2.53 GHz processor and 4 GiB DDR3 @1067 MHz running a virtual machine with Fedora 20 (64-bit).

Acknowledgement. This work was supported by the French ANR project Vecolib, the Czech Science Foundation (project 14-11384S), the EU/Czech IT4Innovations Excellence in Science project LQ1602, and by the European Research Council (ERC) under the European Unions Horizon 2020 research and innovation programme (grant agreement No 678177).

(4) all atoms of ϕ n 1 are used at most once in the image of σ (i.e. are marked once). Let M = (S, H) be a model of ϕ n 1 . From Point (2), it follows that M |= pure(ϕ n 2 ). Let a 1 2 , . . . , a k 2 be the spatial atoms of ϕ n 2 . From the semantics of spatial formulas and Points (3) and ( 4), the heap H may be partitioned into domain-disjoint heaps H 1 , . . . , H k such that they are well-formed models of sub-formulas of ϕ n 1 in the image of σ, i.e., for any 1 ≤ i ≤ k, (S, H i ) is well-formed wrt a i and (S, H i ) |= σ(a i ).

From the soundness of selection and Proposition 5, we obtain that (S, H i ) |= a i . Thus, (S, H) is a model of ϕ n 2 . Completeness, meaning that if Algorithm 1 returns false, then ϕ 1 ⇒ ϕ 2 . At line 4, the procedure return false when ϕ n 1 is satisfiable and ϕ n 2 is not. By the soundness of the satisfiability checking, then trivially ϕ 1 ⇒ ϕ 2 . The next result false is obtained at line 5 when the test of the entailment of pure parts fails. This trivially implies ϕ 1 ⇒ ϕ 2 . In the first for loop (line 6), the result false is returned when a pointsto atom E 2 → ρ 2 of ϕ n 2 cannot be mapped to an unmarked points-to atom a 1 of ϕ n 1 such that pure(ϕ n 1 ) ∧ a 1 ⇒ pure(ϕ n 2 ) ∧ a 2 . Notice that, because ϕ n 1 is satisfiable, it cannot contain two different points-to atoms from the node labelled by E 2 in G(ϕ n 1 ). So if there is such an atom but it is already marked, i.e. used for another atom of ϕ n 2 , the semantics of separating conjunction implies that ϕ 1 ⇒ ϕ 2 . If E 2 is not allocated in ϕ n 1 , i.e. there is no spatial atom in G(ϕ n 1 ) having E 2 as origin, then the entailment is also invalid because E 2 is allocated in ϕ n 2 . If the node labelled by E 2 in G(ϕ n 1 ) is the origin of a predicate atom, the entailment is also invalid because the logic cannot constraint the length of list segments to be one. In the second for loop (line 10), the false result is returned when the select procedure fails to build the subformula ϕ n 1 [a 2 ] with unmarked atoms of ϕ n 1 such that it is well-formed wrt a 2 . From Proposition 2, ϕ n 1 cannot contain two disjoint sets of atoms that could correspond to the sub-formula

If such a set of atoms exists, but includes marked atoms, it follows that some of the atoms are shared with the selection for another atom a 2 of ϕ n 2 ; this is excluded by the semantics of separating conjunction, so the entailment is invalid. If such a set does not exist, no model of ϕ n 1 can include a model of a 2 , and Property 1 implies that it cannot be a model of the predicate atom a 2 . If select returns emp because the well-formedness test failed on the selected set of atoms, then due to the completeness of the test (Proposition 3), no well-formed model of a 2 exists in ϕ 1 . If the selection succeeds but the algorithm proposed for ϕ n 1 [a 2 ] ⇒ sh a 2 returns false, then (Theorem 2) there are well-formed models of ϕ n 1 [a 2 ] that are not models of a 2 , so the initial entailment is invalid. Finally, if there are unmarked atoms of ϕ n 1 , the precise semantics of our logic implies that the models of ϕ n 1 contain more allocated locations than the models of ϕ n 2 , meaning the entailment is invalid.

The overall complexity of the decision procedure is dominated by the complexity of (a) the Boolean satisfiability and unsatisfiability checking used in the normalisation and well-formedness tests (in select), which are NP and co-NP complete respectively, and (b) the algorithms presented in Section 7.3 to build tree automata and check tree automaton membership, which are both polynomial-time. In conclusion, the overall complexity of the algorithm is polynomial wrt the sizes of the formulas ϕ 1 and ϕ 2 modulo an oracle for deciding (un-)satisfiability of a Boolean formula. We implemented our decision procedure in a solver called SPEN (SeParation logic ENtailment). The tool takes as the input an entailment problem ϕ 1 ⇒ ϕ 2 (including the definition of the predicates used) encoded in the SMTLIB2 format. For non-valid entailments, SPEN prints the atom of ϕ 2 which is not entailed by a sub-formula of ϕ 1 . The tool is based on the MINISAT solver for deciding unsatisfiability of Boolean formulas and the VATA library [?] as the tree automata backend. We applied SPEN to entailment problems that use various recursive predicates. First, we considered the benchmark provided in [?], which uses only the ls predicate. It consists of two classes of entailment problems: the first class contains 110 problems each (split into 11 groups) generated randomly according to the rules specified in [?], whereas the second class contains 100 problems (split into 10 groups) obtained from the verification conditions generated by the tool SMALLFOOT [?]. In all experiments 4 , SPEN finished in less than 1 second with the deviation of running times ±100 ms wrt the ones reported for ASTERIX [?], the most efficient tool for deciding entailments of SL formulas with singly linked lists we are aware of. The TA for the predicate ls is quite small, and so the above experiments did not evaluate much the performance of our procedure for checking entailments between formulas and atoms. For a more thorough evaluation, we further considered the experiments listed in Table 1 (among which, skl 3 required the extension discussed in Section 7.3). The full benchmark is available with our tool [?]. The entailment problems are extracted from verification conditions of operations like adding or deleting an element in various positions of list segments. Table 1 gives for each example the running time, whether the entailment is valid or invalid, and the size of the tree encoding and TA for ϕ 1 and ϕ 2 , respectively. We find the resulting times quite encouraging.

Implementation and Experimental Results