Testing the Satisfiability of Formulas in Separation Logic with Permissions

Abstract

We investigate the satisfiability problem for a fragment of Separation Logic (SL) with inductively defined spatial predicates and permissions. We show that the problem is undecidable in general, but decidable under some restrictions on the rules defining the semantics of the spatial predicates. Furthermore, if the satisfiability of permission formulas can be tested in exponential time for the considered permission model then SL satisfiability is Exptime complete.

1 Introduction

Separation Logic [14, 22] (SL) is a dialect of bunched logic [18] that is widely used in verification for reasoning on programs manipulating pointer-based data structures. It constitutes the theoretical basis of several industrial scale automated static program analyzers [1, 2, 7]. SL formulas describe heaps, with atoms asserting that some location (i.e., a memory address) is allocated and refers to some tuple of locations (i.e., a record), combined with a special connective $*$, called separating conjunction, which is used to compose heaps. Custom data structures may be described in this setting by using spatial predicates, the semantics of which is defined using inductive rules, similar to those used for defining recursive structures in usual programming languages. Such rules allow one to describe heaps of unbounded size with some particular structure such as lists or trees. In this setting, existing work usually focuses on the fragment of SL called symbolic heaps (defined as separating conjunctions of SL atoms).

Usually, SL formulas are interpreted in the standard heap model, where heaps are defined as partial finite functions mapping locations to tuples of locations and where the separating conjunction $*$ is interpreted as the disjoint union of heaps. Both the satisfiability and entailment problems have been extensively investigated for this heap model. It was proven that the satisfiability problem is Exptime complete [6], whereas the entailment problem is undecidable in general, and 2-Exptime complete provided the inductive rules meet some syntactic conditions [11,12,13, 15] which are general enough to capture usual data structures used in programming. The combination of spatial reasoning with theory reasoning has also been thoroughly investigated, see for instance [16, 19,20,21, 23]).

However, richer models exist (see for instance [8]) accounting for additional features of dynamic memory. The automation of reasoning in these models received little attention. One such model that is of practical relevance is separation logic with permissions [3, 5], where allocated locations are associated with so called permissions used to model the ownership of a given heap region (e.g., a process may have read or write permission over some location). The heap composition operator that is used to define the interpretation of the separating conjunction is more complex in this framework than in the above case: non disjoint heaps can be combined if they agree on all the locations on which they are both defined and if the corresponding permissions can be combined (for instance it is natural to assume that read permissions can be freely combined but not write permissions). The framework is thus parameterized by some permission model describing which permissions are available and how they can be combined. In [10] algorithms are provided to decide the satisfiability and entailment problems for SL formulas (symbolic heaps) with permissions in the case of lists, i.e., when all allocated locations refer to a single location (i.e., to a record of size 1) and when there is only one spatial predicate $\texttt{lseg}_{p}(x,y)$ denoting a list segment from x to y, with permission p. The provided algorithms are generic w.r.t. the permission model, and it is proven that these problems are in Np and co-Np, respectively, assuming that some oracle exists for testing the satisfiability of permission formulas in the considered model.

In the present paper, we investigate the satisfiability problem for SL formulas with permission defined over arbitrary spatial predicates, with user-defined inductive rules. The goal is to allow for more genericity by tackling custom data structures (such as trees, cyclic lists, doubly linked lists etc.) with arbitrary permissions. The addition of permissions makes satisfiability testing much more difficult: we prove that the problem is undecidable in general, and we devise syntactic conditions on the inductive rules for which the problem is Exptime-complete. The restrictions are similar – but stronger – to those given in [13] to ensure the decidability of the entailment problem in the standard heap model. In particular, the inductive rules defining the predicate $\texttt{lseg}$ mentioned above fulfill these restrictions¹, as well as other usual data structures such as cyclic list, trees etc. (however, doubly linked lists or trees with parent links are not captured). The considered inductive rules use a special connective $\circ$ (different from $*$) that is interpreted as a disjoint union. As we shall see, this is both more natural for defining data structures (see also [5]) and required for deciding satisfiability.

2 Definitions

Syntax. We first briefly review some basic notations. If $\pmb {x}$ and $\pmb {y}$ are finite sequences, then we denote by $\pmb {x}.\pmb {y}$ the concatenation of $\pmb {x}$ and $\pmb {y}$. We denote by $|\pmb {x}|$ the length of $\pmb {x}$ and by $\pmb {x}|_{i}$ its i-th element (if $1 \le i \le |\pmb {x}|$). If $E \subseteq \{ 1,\dots ,|\pmb {x}| \}$ then $\pmb {x}|_{E}$ denotes the set $\{ \pmb {x}|_{i} \mid i \in E \}$. With a slight abuse of notations, a finite sequence $\pmb {x}$ is sometimes identified with the set $\{ \pmb {x}|_{i} \mid i = 1,\dots ,|\pmb {x}| \}$, for instance, we may write $x \in (\pmb {u} \cup \pmb {v}) \setminus \pmb {w}$ to state that x occurs in $\pmb {u}$ or $\pmb {v}$ but not in $\pmb {w}$.

We consider a multisorted framework, with two sorts $\texttt{l}$ (for locations) and $\texttt{p}$ (for permissions). Let $\mathcal{V}_\texttt{l}$ and $\mathcal{V}_\texttt{p}$ be two countably infinite disjoint sets of variables with , where $\mathcal{V}_\texttt{l}$ and $\mathcal{V}_\texttt{p}$ denote location variables and permission variables, respectively. The set of permission terms $\mathcal{T}_{\texttt{p}}$ denotes the set of terms built inductively as usual on the set of variables $\mathcal{V}_\texttt{p}$ and the binary function $\oplus$ (written in infix notation). A points-to atom is an expression of the form $x {\mathop {\mapsto }\limits ^{p}} (y_1,\dots ,y_k)$ with $x,y_1,\dots ,y_k\in \mathcal{V}_\texttt{l}$ and $p\in \mathcal{T}_{\texttt{p}}$. An equational atom is an expression of the form $x \simeq y$ or $x \not \simeq y$ with either $x,y \in \mathcal{V}_\texttt{l}$ or $x,y \in \mathcal{T}_{\texttt{p}}$.

We consider two disjoint sets of predicate symbols $\mathcal{P}_{\texttt{p}}$ and $\mathcal{P}$. The set $\mathcal{P}_{\texttt{p}}$ denotes permission predicates, where each predicate $\hat{P}\in \mathcal{P}_{\texttt{p}}$ is associated with a unique arity $\#(\hat{P})$. A permission atom is an expression of the form $\hat{P}(p_1,\dots ,p_n)$, $\hat{P}\in \mathcal{P}_{\texttt{p}}$, $n = \#(\hat{P})$ and $p_1,\dots ,p_n \in \mathcal{T}_{\texttt{p}}$. $\mathcal{P}$ is a finite set of spatial predicate symbols. Each symbol $P\in \mathcal{P}$ is associated with a spatial arity and with an arity , with $\#(P)> \#_{\texttt{l}}(P) > 0$ ($\#_{\texttt{l}}(P)$ and $\#(P)-\#_{\texttt{l}}(P)$ denote the number of arguments of $P$ that are of sort $\texttt{l}$ and $\texttt{p}$, respectively). A predicate atom is an expression of the form $P(x_1,\dots ,x_n,p_1,\dots ,p_m)$, with $n = \#_{\texttt{l}}(P)$, $n+m = \#(P)$, $x_1,\dots ,x_n \in \mathcal{V}_{\texttt{l}}$ and $p_1,\dots ,p_m \in \mathcal{T}_{\texttt{p}}$. A spatial atom is either a points-to atom or a predicate atom.

The set of formulas is built inductively as usual on the logical constants $\texttt{emp}$, and $\bot$ and on the set of spatial, equational and permission atoms, using the special connectives $*$ and $\circ$ and existential quantification on variables of sort $\texttt{l}$ only (existential quantification over variables of type $\texttt{p}$ is not allowed). The connective $*$ is usually called separating conjunction, and we call $\circ$ the disjoint conjunction (it is intended to capture the disjoint union of heaps²). Formulas are taken up to associativity and commutativity of the symbols $*$ and $\circ$, up to the commutativity of $\simeq ,\not \simeq$ and up to prenex form. We denote by $|\phi |$ the size of $\phi$. For technical convenience, we assume that the symbols $\circ$ and $*$ have weight of 1 and 2, respectively, and that all atoms have size 1. For conciseness, a formula $\exists x_1 \dots \exists x_n\, \phi$ will often be written $\exists \pmb {x}\, \phi$, with $\pmb {x} = (x_1,\dots ,x_n)$. A permission formula is a formula containing no spatial atoms and no equational atom of the form $x \simeq y$ or $x \not \simeq y$ with $x,y \in \mathcal{V}_\texttt{l}$ (note that $\texttt{emp}$ is a permission formula). A formula is spatial if all the atoms occurring in it are spatial. A pure formula is a formula that contains no spatial atom (it is not necessarily a permission formula, as it may contain equations or disequations between locations) A symbolic heap is a formula containing no occurrence of $\circ$, and a $\circ$-formula is a formula containing no occurrence of $*$.

A variable x is free in a formula $\phi$ if it occurs in $\phi$ outside of the scope of any quantifier binding x. The set of variables (freely) occurring in a term (or formula) $\phi$ is denoted by $fv (\phi )$. A substitution is a function mapping every variable in $\mathcal{V}_{\texttt{l}}$ to a variable in $\mathcal{V}_{\texttt{l}}$ and every variable in $\mathcal{V}_{\texttt{p}}$ to a term in $\mathcal{T}_{\texttt{p}}$. The domain of a substitution $\sigma$ (denoted by $dom (\sigma )$) is the set of variables x such that $\sigma (x) \not = x$. A substitution of domain $\{ x_1,\dots ,x_n \}$ with $\sigma (x_i) = t_i$ is denoted by $\{ x_i \leftarrow t_i \mid i = 1,\dots ,n\}$, or $\{ \pmb {x} \leftarrow \pmb {t} \}$, with $\pmb {x} = (x_1,\dots ,x_n)$ and $\pmb {t} = (t_1,\dots ,t_n)$. For all formulas or terms $\phi$, we denote by $\phi \sigma$ the formula or term obtained from $\phi$ by replacing every free occurrence of a variable x by $\sigma (x)$.

Semantics. Permissions are interpreted in some permission model:

Definition 1

(Adapted from [10]). A permission model ${\mathfrak {P}}$ is a triple

$$\begin{aligned} (\mathcal{P}_{{\mathfrak {P}}},\oplus _{\mathfrak {P}},(\hat{P}_{\mathfrak {P}})_{\hat{P}\in \mathcal{P}_{\texttt{p}}}) \end{aligned}$$

where $\mathcal{P}_{{\mathfrak {P}}}$ is a non empty set, called the set of permissions, $\oplus _{\mathfrak {P}}: \mathcal{P}_{{\mathfrak {P}}}^2 \rightarrow \mathcal{P}_{{\mathfrak {P}}}$ is a binary partial function that is commutative, associative and cancellative, and $\hat{P}_{\mathfrak {P}}\subseteq \mathcal{P}_{{\mathfrak {P}}}^{\#(\hat{P})}$, for all $\hat{P}\in \mathcal{P}_{\texttt{p}}$. If $\pi ,\pi '\in \mathcal{P}_{{\mathfrak {P}}}$, we write $\pi \le _{{\mathfrak {P}}}\pi '$ if $\pi = \pi ' \vee (\exists \pi '' \in \mathcal{P}_{{\mathfrak {P}}}\; \pi ' = \pi \oplus \pi '')$.

In what follows, ${\mathfrak {P}}$ always denotes a permission model. If $\pi \in \mathcal{P}_{{\mathfrak {P}}}$ and , we denote by $\pi ^n$ the permission $\pi \oplus _{\mathfrak {P}}\dots \oplus _{\mathfrak {P}}\pi$ (n times), note that $\pi ^n$ is not necessarily defined and implicitly depends on the considered permission model, which will always be clear from the context. In contrast to [10], we do not assume that a maximal “total” permission $1_{{\mathfrak {P}}}$ exists, we allow instead for arbitrary predicates over permissions (the total permission can be encoded as a unary predicate symbol $T$, with $T _{\mathfrak {P}}= \{ 1_{{\mathfrak {P}}} \}$).

Example 2

Assume that $\mathcal{P}_{\texttt{p}}= \emptyset$. A simple example of permission model is $\mathfrak {w}= (\{ \texttt{read},\texttt{write}\}, \oplus _{\mathfrak {w}}, \emptyset )$, with $\texttt{read}\oplus _{\mathfrak {w}}\texttt{read}= \texttt{read}$ and $\texttt{write}\oplus _{\mathfrak {w}}\pi$ is undefined for all $\pi \in \{ \texttt{read},\texttt{write}\}$. Another example (from [4]) is $\mathfrak {f}= (]0,1], \oplus _{\mathfrak {f}}, \emptyset )$ where ]0, 1] denotes the interval of rational numbers, with $\pi \oplus _{\mathfrak {f}}\pi ' = \pi +\pi '$ if $\pi +\pi ' \le 1$ and $\pi \oplus _{\mathfrak {f}}\pi '$ is undefined otherwise ($\mathfrak {f}$ stands for fractional).

Let $\mathcal{L}$ be a countably infinite set of locations. A store (for a given permission model ${\mathfrak {P}}$) is a total mapping associating every variable in $\mathcal{V}_\texttt{l}$ to an element of $\mathcal{L}$ and every variable in $\mathcal{V}_\texttt{p}$ to an element of $\mathcal{P}_{{\mathfrak {P}}}$. A store can be extended into a partial mapping from $\mathcal{T}_{\texttt{p}}$ to $\mathcal{P}_{{\mathfrak {P}}}$ inductively defined as follows: . Note that the obtained mapping is partial since $\mathfrak {s}(p_1) \oplus _{{\mathfrak {P}}} \mathfrak {s}(p_2)$ is not always defined. If $x_1,\dots ,x_n$ are pairwise distinct variables in $\mathcal{V}_{\texttt{l}}$ and $\ell _1,\dots ,\ell _n \in \mathcal{L}$, we denote by $\mathfrak {s}\{ x_i \leftarrow \ell _i \mid i = 1,\dots ,n \}$ the store $\mathfrak {s}'$ coinciding with $\mathfrak {s}$ on every variable not occurring in $\{ x_1,\dots ,x_n \}$ and such that $\mathfrak {s}'(x_i) = \ell _i$ for all $i = 1,\dots ,n$.

A heap (for a given permission model ${\mathfrak {P}}$) is a partial finite function from $\mathcal{L}$ to $\mathcal{L}^* \times \mathcal{P}_{{\mathfrak {P}}}$. The domain of a heap $\mathfrak {h}$ is denoted by $dom (\mathfrak {h})$, and we denote by $|\mathfrak {h}|$ the finite cardinality of $dom (\mathfrak {h})$. A heap of domain $\ell _1,\dots ,\ell _n$ such that $\mathfrak {h}(\ell _i) = (\ell ^i_1,\dots ,\ell ^i_{k_i}, \pi _i)$ (for all $i \in \{ 1,\dots ,n\}$) will be denoted as a set $\{ (\ell _i,\ell ^i_1,\dots ,\ell ^i_{k_i}, \pi _i) \mid i = 1,\dots ,n \}$. For every heap $\mathfrak {h}$ we denote by $loc (\mathfrak {h})$ the set $\{ \ell _i \mid \ell _0\in dom (\mathfrak {h}), \mathfrak {h}(\ell _0) = (\ell _1,\dots ,\ell _k,\pi ), 0 \le i \le k \}$. A heap may be viewed as a directed (labeled) graph: the locations in $loc (\mathfrak {h})$ are the vertices of the graph and there is a edge from $\ell$ to $\ell '$ if $\mathfrak {h}(\ell ) = (\ell _1,\dots ,\ell _n,\pi )$ and $\ell ' = \ell _i$ for some $i\in \{ 1,\dots ,n\}$.

A subheap of $\mathfrak {h}$ is any heap $\mathfrak {h}'$ such that $dom (\mathfrak {h}') \subseteq dom (\mathfrak {h})$ and $\mathfrak {h}'(\ell ) = \mathfrak {h}(\ell )$ for all $\ell \in dom (\mathfrak {h}')$. A $\texttt{p}$-weakening of $\mathfrak {h}$ (w.r.t. some permission model ${\mathfrak {P}}$) is any heap $\mathfrak {h}'$ such that $dom (\mathfrak {h}') = dom (\mathfrak {h})$ and for all $\ell \in dom (\mathfrak {h})$, if $\mathfrak {h}(\ell ) = (\ell _1,\dots ,\ell _n,\pi )$ then $\mathfrak {h}'(\ell ) = (\ell _1,\dots ,\ell _n,\pi ')$ with $\pi ' \le _{{\mathfrak {P}}}\pi$. We write $\mathfrak {h}' \le _{\texttt{l}}\mathfrak {h}$ (resp. $\mathfrak {h}' \le _{\texttt{p}}\mathfrak {h}$) if $\mathfrak {h}'$ is a subheap (resp. a $\texttt{p}$-weakening) of $\mathfrak {h}$. The relation $\le$ denotes the composition of $\le _{\texttt{l}}$ and $\le _{\texttt{p}}$. We write $\mathfrak {h}\sim \mathfrak {h}'$ if $\mathfrak {h}$ and $\mathfrak {h}'$ only differ by the permissions, i.e., $dom (\mathfrak {h}) = dom (\mathfrak {h}')$ and for all $\ell \in dom (\mathfrak {h})$, if $\mathfrak {h}'(\ell ) = (\ell _1,\dots ,\ell _n,\pi ')$ then there exists $\pi$ such that $\mathfrak {h}(\ell ) = (\ell _1,\dots ,\ell _n,\pi )$.

Example 3

Consider the permission model $\mathfrak {f}$ defined in Example 2 with . Then

$$ \begin{array}{ccccccc} \mathfrak {h}_0 &{} = &{} \{ (0,0,1,0.1), (1,0,0,0.2)\}, &{} \qquad &{} \mathfrak {h}_1 &{} = &{} \{ (0,0,1,0.1) \}, \\ \mathfrak {h}_2 &{} = &{} \{ (0,0,1,0.1), (1,0,0,0.1) \} &{} &{} \mathfrak {h}_3 &{} = &{} \{ (1,0,0,0.1) \} \\ \end{array}$$

are heaps, and we have, e.g., $\mathfrak {h}_0(0) = (0,1,0.1)$ (meaning that the location 0 is allocated and refers to (0, 1), with permission 0.1), $\mathfrak {h}_1 \le _{\texttt{l}}\mathfrak {h}_0$, $\mathfrak {h}_2 \le _{\texttt{p}}\mathfrak {h}_0$, $\mathfrak {h}_3 \le _{\texttt{l}}\mathfrak {h}_2$, and $\mathfrak {h}_3 \le \mathfrak {h}_0$. Moreover, $\mathfrak {h}_0 \sim \mathfrak {h}_2$.

Heaps can be composed using the following partial operator. If $\mathfrak {h}_1,\mathfrak {h}_2$ are heaps, then $\mathfrak {h}_1 \sqcup \mathfrak {h}_2$ is defined iff for all $\ell \in dom (\mathfrak {h}_1) \cap dom (\mathfrak {h}_2)$, we have $\mathfrak {h}_i(\ell ) = (\ell ^i_1,\dots ,\ell ^i_{k_i},\pi _i)$ (for all $i = 1,2$) where $k_1 = k_2$, $\ell ^1_j = \ell ^2_j$ for all $j \in \{ 1,\dots ,k_1 \}$ and $\pi _1 \oplus _{\mathfrak {P}}\pi _2$ is defined. Then $\mathfrak {h}_1 \sqcup \mathfrak {h}_2$ is defined as follows: if $\ell \in dom (\mathfrak {h}_i) \setminus dom (\mathfrak {h}_j)$ with $(i,j) \in \{ (1,2),(2,1) \}$ then , and if $\ell \in dom (\mathfrak {h}_1) \cap dom (\mathfrak {h}_2)$ then .

Example 4

Consider the permission model $\mathfrak {f}$ defined in Example 2, with and the following heaps:

$$ \begin{array}{lllllll} \mathfrak {h}_0 &{} = &{} \{ (0,0,0.5), (1,0,0.6) \} &{} \quad &{} \mathfrak {h}_1 &{} = &{} \{ (0,0,0.5), (1,0,0.2), (2,0.1) \} \\ \mathfrak {h}_2 &{} = &{} \{ (0,0,0.5), (1,0,0.6) \} &{} &{} \mathfrak {h}_3 &{} = &{} \{ (0,0,0.1), (1,0.1) \} \end{array} $$

Then $\mathfrak {h}_0 \sqcup \mathfrak {h}_1$ is defined, and we have: $\mathfrak {h}_0 \sqcup \mathfrak {h}_1 = \{ (0,0,1), (1,0,0.8), (2,0.1) \}$. However, neither $\mathfrak {h}_0 \sqcup \mathfrak {h}_2$ nor $\mathfrak {h}_0 \sqcup \mathfrak {h}_3$ is defined (in the former case the permissions of location 1 cannot be combined (as $0.6+0.6>1$) and in the latter case the location 1 is associated with distinct tuples, (0) and (), respectively.

A structure (for a given permission model ${\mathfrak {P}}$) is a pair $(\mathfrak {s},\mathfrak {h})$ where $\mathfrak {s}$ is a store and $\mathfrak {h}$ is a heap for ${\mathfrak {P}}$. It is injective if $\mathfrak {s}$ is injective. A location $\ell$ is allocated in a structure $(\mathfrak {s},\mathfrak {h})$ or in a heap $\mathfrak {h}$ if $\ell \in dom (\mathfrak {h})$, and a variable x is allocated in $(\mathfrak {s},\mathfrak {h})$ if $\mathfrak {s}(x) \in dom (\mathfrak {h})$.

The semantics of spatial predicate is defined by inductive rules. A set of inductive definitions (SID) is a set of rules of the form $P(x_1,\dots ,x_n,y_1,\dots ,y_m)$ $\Leftarrow \phi$ where $n = \#_{\texttt{l}}(P)$, $n+m = \#(P)$, $x_1,\dots ,x_n$ are pairwise distinct variables in $\mathcal{V}_{\texttt{l}}$, $y_1,\dots ,y_m$ are pairwise distinct variables in $\mathcal{V}_{\texttt{p}}$, and $\phi$ is a formula such that $fv (\phi ) \subseteq \{ x_1,\dots ,x_n,y_1,\dots ,y_m \}$. We write $P(z_1,\dots ,z_n,p_1,\dots ,p_m) \Leftarrow _{\mathcal{R}} \psi$ iff $\mathcal{R}$ contains a rule $P(x_1,\dots ,x_n,y_1,\dots ,y_m) \Leftarrow \phi$ with $\psi = \phi \{ x_i \leftarrow z_i, y_j \leftarrow p_j \mid i \in \{ 1,\dots ,n \}, j \in \{ 1,\dots ,m \} \}$.

Definition 5

(Semantics) For every permission model ${\mathfrak {P}}$ and SID $\mathcal{R}$, the satisfiability relation $\models _{\mathcal{R}}^{{\mathfrak {P}}}$ is the smallest relation between structures (for ${\mathfrak {P}}$) and formulas such that:

• 1. $(\mathfrak {s},\mathfrak {h}) \models _{\mathcal{R}}^{{\mathfrak {P}}}\texttt{emp}$ iff $\mathfrak {h}= \emptyset$.

• 2. $(\mathfrak {s},\mathfrak {h}) \models _{\mathcal{R}}^{{\mathfrak {P}}}x {\mathop {\mapsto }\limits ^{p}} (y_1,\dots ,y_k)$ if $\mathfrak {s}(p)$ is defined and $\mathfrak {h}= \{ (\mathfrak {s}(x), \mathfrak {s}(y_1),\dots ,\mathfrak {s}(y_k),\mathfrak {s}(p)) \}$. Note that this entails that $dom (\mathfrak {h}) = \{ \mathfrak {s}(x) \}$.

• 3. $(\mathfrak {s},\mathfrak {h}) \models _{\mathcal{R}}^{{\mathfrak {P}}}x \simeq y$ (resp. $(\mathfrak {s},\mathfrak {h}) \models _{\mathcal{R}}^{{\mathfrak {P}}}x \not \simeq y$) if $\mathfrak {h}= \emptyset$, $\mathfrak {s}(x)$ and $\mathfrak {s}(y)$ are defined and $\mathfrak {s}(x) = \mathfrak {s}(y)$ (resp. $\mathfrak {s}(x) \not = \mathfrak {s}(y)$).

• 4. $(\mathfrak {s},\mathfrak {h}) \models _{\mathcal{R}}^{{\mathfrak {P}}}\hat{P}(p_1,\dots ,p_n)$ with $\hat{P}\in \mathcal{P}_{\texttt{p}}$ if $\mathfrak {s}(p_i)$ is defined for all $i \in \{ 1,\dots , n\}$, $(\mathfrak {s}(p_1),\dots ,\mathfrak {s}(p_n)) \in \hat{P}_{\mathfrak {P}}$ and $\mathfrak {h}= \emptyset$.

• 5. $(\mathfrak {s},\mathfrak {h}) \models _{\mathcal{R}}^{{\mathfrak {P}}}P(x_1,\dots ,x_n,\pi _1,\dots ,\pi _m)$ with $P\in \mathcal{P}$ if there exists $\phi$ such that $P(x_1,\dots ,x_n,\pi _1,\dots ,\pi _m) \Leftarrow _{\mathcal{R}} \phi$ and $(\mathfrak {s},\mathfrak {h}) \models _{\mathcal{R}}^{{\mathfrak {P}}}\phi$.

• 6. $(\mathfrak {s},\mathfrak {h}) \models _{\mathcal{R}}^{{\mathfrak {P}}}\phi _1 *\phi _2$ if there exist heaps $\mathfrak {h}_1,\mathfrak {h}_2$ such that $\mathfrak {h}_1 \sqcup \mathfrak {h}_2$ is defined, $\mathfrak {h}= \mathfrak {h}_1 \sqcup \mathfrak {h}_2$ and $(\mathfrak {s},\mathfrak {h}_i) \models _{\mathcal{R}}^{{\mathfrak {P}}}\phi _i$ for all $i = 1,2$.

• 7. $(\mathfrak {s},\mathfrak {h}) \models _{\mathcal{R}}^{{\mathfrak {P}}}\phi _1 \circ \phi _2$ if there exists heaps $\mathfrak {h}_1,\mathfrak {h}_2$ such that $dom (\mathfrak {h}_1) \cap dom (\mathfrak {h}_2) = \emptyset$, $\mathfrak {h}= \mathfrak {h}_1 \sqcup \mathfrak {h}_2$ and $(\mathfrak {s},\mathfrak {h}_i) \models _{\mathcal{R}}^{{\mathfrak {P}}}\phi _i$ for all $i = 1,2$.

• 8. $(\mathfrak {s},\mathfrak {h}) \models _{\mathcal{R}}^{{\mathfrak {P}}}\exists x\, \phi$ if $(\mathfrak {s}\{ x \leftarrow \ell \} ,\mathfrak {h}) \models _{\mathcal{R}}^{{\mathfrak {P}}}\phi$ for some $\ell \in \mathcal{L}$.

A structure $(\mathfrak {s},\mathfrak {h})$ such that $(\mathfrak {s},\mathfrak {h}) \models _{\mathcal{R}}^{{\mathfrak {P}}}\phi$ is an $(\mathcal{R},{\mathfrak {P}})$-model of $\phi$. A formula admitting an $(\mathcal{R},{\mathfrak {P}})$-model is $(\mathcal{R},{\mathfrak {P}})$-satisfiable. Two formulas are sat-equivalent (w.r.t. $\mathcal{R}$, ${\mathfrak {P}}$) if they are both $(\mathcal{R},{\mathfrak {P}})$-satisfiable or both $(\mathcal{R},{\mathfrak {P}})$-unsatisfiable.

Example 6

The formula $x {\mathop {\mapsto }\limits ^{u}} (y,z) \circ x {\mathop {\mapsto }\limits ^{u'}} (y',z')$ is $(\mathcal{R},{\mathfrak {P}})$-unsatisfiable, as x cannot be allocated in disjoint parts of the heap. $x {\mathop {\mapsto }\limits ^{u}} (y) * x {\mathop {\mapsto }\limits ^{u'}} (y') * y \not \simeq y'$ is also $(\mathcal{R},{\mathfrak {P}})$-unsatisfiable, as x cannot refer to two distinct records, but $x {\mathop {\mapsto }\limits ^{u}} (y,z) * x {\mathop {\mapsto }\limits ^{u'}} (y',z')$ admits the model (on the permission model $\mathfrak {f}$) $(\mathfrak {s},\mathfrak {h})$ with $\mathfrak {s}(x) = 0$, $\mathfrak {s}(y) = \mathfrak {s}(y') = 1$, $\mathfrak {s}(z) = \mathfrak {s}(z') = 2$, $\mathfrak {s}(u) = 0.5$, $\mathfrak {s}(u') = 0.2$ and $\mathfrak {h}= \{ (0,1,2,0.7) \}$.

Note that there is no logical constant $\top$ (true): no formula can be satisfied on all heaps. The constant $\texttt{emp}$ is similar to $\top$ but it states that the heap is empty. For all formulas $\phi ,\psi$, we write $\phi \models _{\mathcal{R}}^{{\mathfrak {P}}}\psi$ iff the implication $(\mathfrak {s},\mathfrak {h}) \models _{\mathcal{R}}^{{\mathfrak {P}}}\phi \implies (\mathfrak {s},\mathfrak {h}) \models _{\mathcal{R}}^{{\mathfrak {P}}}\psi$ holds for all structures $(\mathfrak {s},\mathfrak {h})$, and $\phi \equiv _{\mathcal{R}}^{{\mathfrak {P}}}\psi$ iff we have both $\phi \models _{\mathcal{R}}^{{\mathfrak {P}}}\psi$ and $\psi \models _{\mathcal{R}}^{{\mathfrak {P}}}\phi$. If $\phi$ contains no predicate symbols in $\mathcal{P}$, then the truth value of $\phi$ in $(\mathfrak {s},\mathfrak {h})$ does not depend on $\mathcal{R}$. We thus may write $(\mathfrak {s},\mathfrak {h}) \models ^{{\mathfrak {P}}}\phi$ instead of $(\mathfrak {s},\mathfrak {h}) \models _{\mathcal{R}}^{{\mathfrak {P}}}\phi$. If, moreover, $\phi$ is pure, then $(\mathfrak {s},\mathfrak {h}) \models ^{{\mathfrak {P}}}\phi$ holds only if $\mathfrak {h}$ is empty. We will write $\mathfrak {s}\models ^{{\mathfrak {P}}}\phi$ to state that $(\mathfrak {s},\emptyset ) \models ^{{\mathfrak {P}}}\phi$. Finally, if $\phi$ contains only equalities between variables then its semantics does not depend on $\mathcal{R}$ and ${\mathfrak {P}}$ thus we write $\mathfrak {s}\models \phi$ to state that $(\mathfrak {s},\emptyset ) \models _{\mathcal{R}}^{{\mathfrak {P}}}\phi$. Note that the semantics of $\phi _1 \circ \phi _2$ and $\phi _1 *\phi _2$ coincide if $\phi _1$ or $\phi _2$ is pure, and also coincide with that of the usual standard conjunction if both $\phi _1$ and $\phi _2$ are pure.

Shorthands. If $\pmb {x} = (x_1,\dots ,x_n)$ and $\pmb {y} = (y_1,\dots ,y_m)$ are sequences of variables in $\mathcal{V}_{\texttt{l}}$ then $\pmb {x} \simeq \pmb {y}$ denotes the formula $\bot$ if $n \not = m$ and $(x_1 \simeq y_1) \circ \dots \circ (x_n \simeq y_n)$ otherwise. For every permission term $p$, we denote by ${ def }(p)$ the atom $p\simeq p$. By definition, $(\mathfrak {s},\mathfrak {h}) \models _{\mathcal{R}}^{{\mathfrak {P}}}{ def }(p)$ iff $\mathfrak {s}(p)$ is defined and $\mathfrak {h}= \emptyset$.

3 $\mathfrak {h}$-Regular Systems

We focus on SIDs of some particular form, defined below.

Definition 7

A rule is $\mathfrak {h}$-regular if it is of the following form:

$$ P(x,\pmb {y}) \Leftarrow \exists u_1,\dots ,u_n\, (x {\mathop {\mapsto }\limits ^{p}} (v_1,\dots ,v_k) \circ Q_1(u_1,\pmb {y}_1) \dots \circ Q_n(u_n,\pmb {y}_n) \circ \phi ) $$

where $\{ u_1,\dots ,u_n \} \subseteq \{ v_1,\dots ,v_k \}$, $\pmb {y}_i$ is a vector of variables³, $Q_i\in \mathcal{P}$ and $\phi$ is pure. We assume by $\alpha$-renaming that $x,\pmb {y}$ do not occur in $\{u_1,\dots ,u_n\}$. A SID $\mathcal{R}$ is $\mathfrak {h}$-regular if all the rules in $\mathcal{R}$ are $\mathfrak {h}$-regular.

Note that the right-hand side formula contains only the disjoint separation connective $\circ$ and not the usual separating conjunction $*$. As we will see (Theorem 33) this is crucial for the decidability of the satisfiability problem. However, as already observed in [5], this is also justified from a practical point of view. Assume for instance that we want to define the predicate $\texttt{lseg}$ introduced in [10], denoting a list segment from x to y with some permission z. The following rules can be used⁴: $\texttt{lseg}(x,y,z) \Leftarrow x {\mathop {\mapsto }\limits ^{z}} (y) \quad \texttt{lseg}(x,y,z) \Leftarrow \exists u\; (x {\mathop {\mapsto }\limits ^{z}} (u) \circ \texttt{lseg}(u,y,z))$. A structure $(\mathfrak {s},\mathfrak {h})$ satisfies $\texttt{lseg}(x,y,z)$ if $\mathfrak {h}= \{ (\ell _i,\ell _{i+1},\mathfrak {s}(z)) \mid i = 1,\dots ,n \}$ with $n > 0$, $\mathfrak {s}(x) = \ell _1$, $\mathfrak {s}(y) = \ell _{n+1}$ and $\ell _i \not = \ell _j$ if $i \not = j$ and $i,j \in \{ 1,\dots ,n \}$. This fits in with the definition in [10] (except that $n > 0$). In contrast, if one uses instead the connective $*$: $\texttt{lseg}(x,y,z) \Leftarrow \exists u\; (x {\mathop {\mapsto }\limits ^{z}} (u) * \texttt{lseg}(u,y,z))$, then one could obtain models where the list “loops” on itself an arbitrary number of times, such as, for instance $(\mathfrak {s},\{ (\mathfrak {s}(x),\mathfrak {s}(x),p)) \})$, with $\mathfrak {s}(y) = \mathfrak {s}(x)$ and $p= \mathfrak {s}(z)^n$, for any $n > 0$ such that $\mathfrak {s}(z)^n$ is defined. In the former definition, $\mathfrak {s}(y)$ possibly occurs in $\{ \ell _1,\dots ,\ell _n\}$, but each location can only be allocated once.

Intuitively, $\mathfrak {h}$-regular sets of inductive rules generate heaps with a regular structure (in the sense that it may be represented by a tree automaton [9]), enriched with some additional edges (referring to the nodes corresponding to the variables passed as parameters to the spatial predicates at some recursive calls). These additional edges may refer to locations corresponding to free variables (e.g. the root of the structure) but also to existential variables (for instance they may refer to the parent node in the tree). $\mathfrak {h}$-Regular SID are related to the Pce systems introduced in [13] (for progressing, connected and established), extended to formulas with permissions, but our conditions are slightly stronger, because we require that every existential variable be allocated at the next recursive call. Note that structures with mixed permissions are allowed, for instance the rules $P(x,z_1,z_2) \Leftarrow x {\mathop {\mapsto }\limits ^{z_1}} ()$ and $P(x,z_1,z_2) \Leftarrow \exists u\, (x {\mathop {\mapsto }\limits ^{z_1}} (u) \circ P(u,z_2,z_1))$ defines a list with permissions alternating between $z_1$ and $z_2$. Rules with compound permission terms in points-to or permission atoms are allowed (such as $P(x,y_1,y_2) \Leftarrow x {\mathop {\mapsto }\limits ^{y_1 \oplus y_2}} () \circ { def }(y_1 \oplus y_1)$), but not those with compound permission terms in spatial predicate atoms⁵ (e.g., $P(x,y_1,y_2) \Leftarrow x {\mathop {\mapsto }\limits ^{y_1}} () \circ Q(x,y_1\oplus y_2)$ is not $\mathfrak {h}$-regular).

For every quantifier-free formula $\phi$, we denote by $roots (\phi )$ the set of variables x (called the roots of $\phi$) inductively defined as follows: , , $roots (\exists y\, \phi ) = roots (\phi ) \setminus \{ y \}$, $roots (\phi ) = \emptyset$ if $\phi$ is pure and $roots (\phi _1 * \phi _2) = roots (\phi _1 \circ \phi _2) = roots (\phi _1) \cup roots (\phi _2)$. By Definition 7, roots are always allocated:

Proposition 8

Let $\mathcal{R}$ be a $\mathfrak {h}$-regular SID. If $(\mathfrak {s},\mathfrak {h}) \models _{\mathcal{R}}^{{\mathfrak {P}}}\phi$ and $x \in roots (\phi )$ then $\mathfrak {s}(x) \in dom (\mathfrak {h})$. Consequently, every formula of the form $\phi _1 \circ \phi _2$ with $roots (\phi _1) \cap roots (\phi _2) \not = \emptyset$ is $(\mathcal{R},{\mathfrak {P}})$-unsatisfiable.

The conditions in Definition 7 are actually not sufficient to ensure that the satisfiability problem is decidable:

Theorem 9

If there exist (not necessary distinct) permissions $\pi _1,\pi _2\in \mathcal{P}_{\mathfrak {P}}$ such that $\pi _1 \oplus _{\mathfrak {P}}\pi _2$ is defined, then the $(\mathcal{R},{\mathfrak {P}})$-satisfiability problem is undecidable for $\mathfrak {h}$-regular SID $\mathcal{R}$.

To ensure decidability, we need to further restrict the way existential variables are passed as parameters during recursive calls. This is the goal of the next definition.

Definition 10

Assume that $\mathcal{R}$ is $\mathfrak {h}$-regular. Given two spatial predicates $P$ and $Q$, of arities n and m respectively, we write $P\bowtie _{\mathcal{R}}Q$ if $P(x,x_1,\dots ,x_{n-1}) * Q(x,y_1,\dots ,y_{m-1})$ is $(\mathcal{R},{\mathfrak {P}})$-unsatisfiable⁶ (where $x_1,\dots ,x_{n-1},y_1,\dots ,y_{m-1}$ denote pairwise distinct variables of the appropriate sorts). We denote by $\gamma _{\mathcal{R}}$ the function associating every predicate symbol $P$ of spatial arity n to a subset of $\{ 2,\dots ,n \}$ inductively defined as follows: for every rule $P(x_1,\dots ,x_n,\pmb {u}) \Leftarrow \exists y_1,\dots ,y_m\, \phi$ in $\mathcal{R}$, for every predicate atom $Q(z_1,\dots ,z_k,\pmb {u}_k)$ in $\phi$ with $\#_{\texttt{l}}(Q) = k$ and for all $i \in \{ 2,\dots ,k\}$:

• 1. $z_i \in \{ y_1,\dots ,y_m\} \Rightarrow i \in \gamma _{\mathcal{R}}(Q)$.

• 2. $z_i \in \{ x_j \mid j \in \gamma _{\mathcal{R}}(P) \} \implies i \in \gamma _{\mathcal{R}}(Q)$.

Let $\mathcal{P}^\star$ be a subset of $\mathcal{P}$, such that: (3) $P\in \mathcal{P}^\star \implies \gamma _{\mathcal{R}}(P)= \emptyset$; and (4) $P\in \mathcal{P}^\star \wedge Q\in \mathcal{P}\setminus \mathcal{P}^\star \implies P\bowtie _{\mathcal{R}}Q$. A $\mathfrak {h}$-regular rule is $\exists$-restricted (w.r.t. $\mathcal{R}$ and $\mathcal{P}^\star$) if it satisfies the following condition (using the notations of Definition 7):

• 5. $\forall i \in \{ 1,\dots ,n \}\, \forall j \in \{ 1,\dots ,n \}\, (u_i \in \pmb {y}_j \implies Q_i \in \mathcal{P}^\star )$.

A SID $\mathcal{R}$ is $\exists$-restricted if all the rules in $\mathcal{R}$ are $\exists$-restricted.

Conditions 1 and 2 in Definition 10 are meant to ensure that $\gamma _{\mathcal{R}}(P)$ denotes the indices of the parameters of $P$ that may (but do not have to) be instantiated by some existential variable introduced during the unfolding of the inductive rules in $\mathcal{R}$ (the other parameters may only be instantiated by variables occurring in the initial formula). Condition 1 corresponds to a base case, where an existential variable is passed as a parameter to a predicate symbol, and Condition 2 handles the inductive case, when the variable is carried through recursive calls⁷. Then, Condition 5 ensures that an existential variable may only be passed as a parameter to a predicate symbol if it is the root of a structure defined by an atom $Q_i(\pmb {y}_i)$ containing no variables introduced by unfolding (by Condition 3).

Example 11

The rules of the predicate $\texttt{lseg}$ are $\exists$-restricted (with $\mathcal{P}^\star = \emptyset$). Indeed, they contain only one existential variable u, which occurs only as the first argument of a predicate. Hence Condition 5 in Definition 10 trivially holds. If $\mathcal{R}$ contains no other rule then $\gamma _{\mathcal{R}}(\texttt{lseg}) = \emptyset$. Note that $\gamma _{\mathcal{R}}(\texttt{lseg})$ depends on the entire set $\mathcal{R}$. For instance, if $\mathcal{R}$ contains a rule $P(x,y) \Leftarrow \exists u\, (x {\mathop {\mapsto }\limits ^{y}} (u) \circ \texttt{lseg}(u,u,y))$ then the second argument of $\texttt{lseg}$ may be instantiated by an existential variable hence $\gamma _{\mathcal{R}}(\texttt{lseg}) = \{ 2 \}$, and the latter rule is not $\exists$-restricted. On the other hand, if $\mathcal{P}^\star = \{ Q\}$, then the rules $Q(x,y) \Leftarrow x {\mathop {\mapsto }\limits ^{y}} (), R(x,y) \Leftarrow \exists u,v\, (x {\mathop {\mapsto }\limits ^{y}} (u,v) \circ \texttt{lseg}(u,v,y) \circ Q(v,y))$ are $\exists$-restricted, with $\mathcal{P}^\star = \{ Q\}$. Indeed, the variable u occurs only at the root of a predicate, and the variable v is the root of $Q(v,y)$. Note that $\texttt{lseg}(x,y,z) * Q(x,u)$ and $R(x,y) * Q(x,u)$ are $(\mathcal{R},{\mathfrak {P}})$-unsatisfiable, thus $\texttt{lseg}\bowtie _{\mathcal{R}}Q$ and $R\bowtie _{\mathcal{R}}Q$.

Intuitively, the structures generated by $\exists$-restricted rules are regular tree-shaped structures, enriched with two kinds of additional edges: (i) a bounded number of arbitrary edges (corresponding to free variables, which may be freely passed as arguments to any predicate, thus may be referred to in an arbitrary way); (ii) an unbounded number of other edges (corresponding to existential variables) which are only allowed to point to structures that contain no edge of type (ii). Condition 4 ensures that the structures containing only edges of type (i) do not overlap with those containing both kinds of edges. Note that the conditions of Definition 10 always hold if the existential variables occur only as roots (with $\mathcal{P}^\star = \mathcal{P}$ or $\mathcal{P}^\star = \emptyset$). In this case there is no edge of type (ii), i.e., the obtained structures are regular sets of trees with a bounded number of additional edges (for instance trees with pointers to the root, or cyclic lists). Note that doubly linked lists cannot be captured (as they contain an unbounded number of additional edges from every node to the previous one). In the following we devise an algorithm to test the $(\mathcal{R},{\mathfrak {P}})$-satisfiability of symbolic heaps when $\mathcal{R}$ is $\exists$-restricted.

4 A Decision Procedure for Testing Satisfiability

Before entering into technical details we start with a general overview of the procedure for testing satisfiability (assuming the considered SID is $\exists$-restricted).

• 1. Starting with a formula of the form $\delta _1 * \dots * \delta _n$ where the $\delta _i$’s are atoms, we first reduce every spatial atom $\delta _i$ into an equivalent disjunction of $\circ$-conjunctions $\delta ^i_1 \circ \dots \circ \delta ^i_{m_i}$ such that the only free variables allocated by an atom $\delta ^i_j$ are its roots $roots (\delta ^i_j)$ (as $\delta ^i_j$ is an atom, $card ( roots (\delta ^i_j)) \le 1$). Due to the particular properties of the $\mathfrak {h}$-regular rules (more precisely, due to the fact that the rules satisfy the “establishment” property of [13], i.e., every existential variable is allocated), this entails that, for all structures $(\mathfrak {s},\mathfrak {h}_{i,j})$ satisfying $\delta ^i_j$, the domains of $\mathfrak {h}_{i,j}$ and $\mathfrak {h}_{i',j'}$ are either equal (if $\delta ^i_j$ and $\delta ^{i'}_{j'}$ have the same roots) or disjoint (otherwise). Indeed, the establishment property ensures that the considered heaps have no “pending edges” (i.e., no location that is referred to but not allocated), other than those denoted by free variables. This step can be considered as the key part of the procedure. It requires to (automatically) enrich the language with additional predicates and rules, and the termination of the transformation crucially depends on the conditions on $\exists$-restricted rules. For instance, an atom $\texttt{lseg}(x,x)$ occurring in a formula with free variables x, y could be written $(x \simeq y \circ \texttt{lseg}(x,x)) \vee \texttt{lseg}'(x,x,y) \vee (\texttt{lseg}'(x,y,y) \circ \texttt{lseg}'(y,x,x))$ where $\texttt{lseg}'(u,v,w)$ denotes a list segment from u to v not allocating w. The previous decomposition depends on whether y is equal to x and whether y occurs in the list segment from x to x.

• 2. By distributivity, we get at this point $*$-conjunctions of $\circ$-conjunctions of atoms. Taking advantage of the previous property, we then reduce these formulas into $\circ$-conjunctions of $*$-conjunctions of atoms, by regrouping the atoms with the same roots, e.g., $(P(x,y) \circ Q(y,x)) * (P'(x,y) \circ Q'(y,x))$ may be written $(P(x,y) * P'(x,y)) \circ (Q(y,x) * Q'(y,x))$.

• 3. Next, we show that a $*$-conjunction of atoms sharing the same root (such as $P(x,y) * P'(x,y)$ or $Q(y,x) * Q'(y,x)$) can be denoted by a single atom, the rules of which are obtained by “merging” the rules of the initial atoms.

• 4. At this point we get a $\circ$-conjunction of atoms. To ensure that the formula is satisfiable it suffices to test that all these atoms have a model and that all these models are compatible, w.r.t. the equality constraints, allocated locations and permission constraints. To this aim, we construct finite abstractions of the models of the considered atoms using a bottom-up fixpoint algorithm.

In the next subsections, each of these steps is explained in details.

4.1 Normalization

We first show that every formula can be transformed into an equivalent formula (that we call normalized) in which every allocated variable occurs as a root:

Definition 12

A formula $\phi$ is normalized if it is of the form $\exists \pmb {x}\, \psi$ where $\psi$ is quantifier-free and for all spatial atoms $\delta$ in $\psi$, for all $(\mathcal{R},{\mathfrak {P}})$-models $(\mathfrak {s},\mathfrak {h})$ of $\delta$ and for all variables $y \in fv (\psi )$: $\mathfrak {s}(y) \in dom (\mathfrak {h}) \iff y \in roots (\psi )$.

For instance, $\texttt{lseg}(x,y)$ is not normalized, because y may be allocated (e.g., if $\mathfrak {s}(x) = \mathfrak {s}(y)$) and does not occur in $roots (\texttt{lseg}(x,y)) = \{ x \}$. To enforce this condition, we introduce new predicate symbols (called derived predicates), the rules of which can be automatically computed from those of the predicates already occurring in this formula. We first define predicate symbols that ensure that some given variable is not allocated.

Definition 13

For all predicate atoms $P(\pmb {x},\pmb {p})$ (where $\pmb {x}$ and $\pmb {p}$ are vectors of location variables and permission terms, respectively) and for all location variables v, we denote by $P(\pmb {x},\pmb {p})[v]^-$ any atom of the form $Q(\pmb {x},v,\pmb {p})$, where $Q$ is a fresh predicate symbol, associated with the rules:

$$Q(\pmb {y},w,\pmb {z}) \Leftarrow \exists \pmb {u}\, (Q_1(\pmb {y}_1,\pmb {p}_1)[w]^- \circ \dots \circ Q_m(\pmb {y}_m,\pmb {p}_m)[w]^- \circ \phi \circ \pmb {y}|_{1} \not \simeq w)$$

for all rules $P(\pmb {y},\pmb {z}) \Leftarrow \exists \pmb {u}\, (Q_1(\pmb {y}_1, \pmb {p}_1) \circ \dots \circ Q_m(\pmb {y}_m, \pmb {p}_m) \circ \phi )$ in $\mathcal{R}$ (up to AC), where $\pmb {y},\pmb {y}_i$ are vectors of location variables, $\pmb {z}$, $\pmb {p}_i$ are vectors of permission variables, and $\phi$ contains no predicate atom.

For instance $\texttt{lseg}(x,y,z)[u]^-$ is a predicate atom $Q(x,y,u,z)$ defined by the following rules: $\{ Q(x,y,u,z) \Leftarrow \exists x' (x {\mathop {\mapsto }\limits ^{z}} (x') \circ Q(x',y,u,z) \circ x \not \simeq u), Q(x,y,u,z) \Leftarrow x {\mathop {\mapsto }\limits ^{z}} (y) \circ x \not \simeq u \}$. It denotes a list segment from x to y not allocating u. The following result is straightforward to prove:

Proposition 14

For every $\exists$-restricted SID $\mathcal{R}$, the set $\mathcal{R}$ enriched with the rules associated with the predicate $Q$ corresponding to $P(\pmb {x},p)[v]^-$ in Definition 13 is $\exists$-restricted, with $\gamma _{\mathcal{R}}(Q) = \gamma _{\mathcal{R}}(P)$ and $Q\in \mathcal{P}^\star \iff P\in \mathcal{P}^\star$.

Intuitively the structures that satisfy $P(\pmb {x},\pmb {p})[v]^-$ are exactly those that satisfy $P(\pmb {x},\pmb {p})$ and do not allocate v:

Lemma 15

For all $\mathfrak {h}$-regular SID $\mathcal{R}$, $(\mathfrak {s},\mathfrak {h}) \models _{\mathcal{R}}^{{\mathfrak {P}}}P(\pmb {x},p)[v]^-$ iff $(\mathfrak {s},\mathfrak {h}) \models _{\mathcal{R}}^{{\mathfrak {P}}}P(\pmb {x},p)$ and $\mathfrak {s}(v) \not \in dom (\mathfrak {h})$.

The operator $\delta \mapsto \delta [x]^-$ can be applied recursively, e.g., one can consider atoms of the form $\delta [x]^-[y]^-$, etc. For all predicate atoms $\delta$, we denote by $unalloc (\delta )$ the set of variables inductively defined as follows: , and . The following proposition is an immediate consequence of Lemma 15:

Proposition 16

If $(\mathfrak {s},\mathfrak {h}) \models _{\mathcal{R}}^{{\mathfrak {P}}}\delta$ then $\mathfrak {s}(x) \not \in dom (\mathfrak {h})$, for all $x\in unalloc (\delta )$.

Next, we define predicate symbols allowing one to remove some part of a structure. Intuitively, the expression will hold exactly in the structures that satisfy $\psi$ when a disjoint structure satisfying $\phi$ is added. For instance given the rules $\texttt{tree}(x,y) \Leftarrow \exists x_1,x_2\, x {\mathop {\mapsto }\limits ^{y}} (x_1,x_2) \circ \texttt{tree}(x_1,y) \circ \texttt{tree}(x_2,y)$ and $\texttt{tree}(x,y) \Leftarrow x {\mathop {\mapsto }\limits ^{y}} ()$, $\texttt{tree}(z,y)$ and $\texttt{tree}(x,y)$ denote binary trees with roots z and x, respectively, and denotes a tree of root x with a “hole” at z (the structures satisfying are obtained from models of $\texttt{tree}(x,y)$ by removing the part of the heap that corresponds to $\texttt{tree}(z,y)$). The formula is similar to the strong magic wand introduced in [17] and to the context predicates in [12] and also close in spirit to the separating implication of SL although the semantics are slightly different.

Definition 17

For all finite sequences of predicate atoms $P_i(\pmb {x}_i,\pmb {p}_i)$ (with $i = 0,\dots ,n$), where $\pmb {x}_i$ and $\pmb {p}_i$ are vectors of location variables and permission terms, respectively, we denote by any atom $P(\pmb {x},\pmb {p})$ with $\pmb {x} = \pmb {x}_0.\dots .\pmb {x}_n$, $\pmb {p} = \pmb {p}_0.\dots .\pmb {p}_n$, and such that $P= P_0$ if $n = 0$ and otherwise $P$ is a fresh symbol associated with rules of the form

$$P(\pmb {y},\pmb {z}) \Leftarrow \exists \pmb {w}\, (\psi _1 \circ \dots \circ \psi _m \circ \phi )$$

for all rules

$$\begin{aligned} P_0(\pmb {y}_0,\pmb {z}_0) \Leftarrow \exists \pmb {w}\, (Q_1(\pmb {u}_1, \pmb {q}_1) \circ \dots \circ Q_m(\pmb {u}_m, \pmb {q}_m) \circ \phi ) \end{aligned}$$

in $\mathcal{R}$ and for all decompositions $\alpha _1 \circ \dots \circ \alpha _m = P_1(\pmb {y}_1, \pmb {z}_1) \circ \dots \circ P_n(\pmb {y}_n,\pmb {z}_n)$ (up to AC, where the $\alpha _i$’s may be empty), where:

• $\pmb {y}_i$ and $\pmb {z}_i$ are sequences of pairwise distinct location and permission variables, respectively, with $|\pmb {y}_i| = |\pmb {x}_i|$ and $|\pmb {z}_i| = |\pmb {p}_i|$;

• $\pmb {y} = \pmb {y}_0.\dots .\pmb {y}_n$, $\pmb {z} = \pmb {z}_1.\dots .\pmb {z}_n$;

• $\psi _i$ is of one of the following forms:

  • either ;

  • or $\pmb {y}_j \simeq \pmb {u}_i \circ \pmb {z}_j \simeq \pmb {q}_i$, if $\alpha _i = P_j(\pmb {y}_j, \pmb {z}_j)$ and $P_j = Q_i$.

For instance denotes an atom $P(x,z,y,y)$ with the rules:

$$ \begin{array}{lll} P(x,z,y_1,y_2) &{} \Leftarrow &{} \exists x_1,x_2\; (x {\mathop {\mapsto }\limits ^{y_1}} (x_1,x_2) \circ P(x_1,z,y_1,y_2) \circ \texttt{tree}(x_2,z,y_1)) \\ P(x,z,y_1,y_2) &{} \Leftarrow &{} \exists x_1,x_2\; (x {\mathop {\mapsto }\limits ^{y_1}} (x_1,x_2) \circ \texttt{tree}(x_1,z,y_1) \circ P(x_2,z,y_1,y_2)) \\ P(x,z,y_1,y_2) &{} \Leftarrow &{} \exists x_1,x_2\; (x {\mathop {\mapsto }\limits ^{y_1}} (x_1,x_2) \circ x_1 \simeq z \circ y_1 \simeq y_2 \circ \texttt{tree}(x_2,z,y_1)) \\ P(x,z,y_1,y_2) &{} \Leftarrow &{} \exists x_1,x_2\; (x {\mathop {\mapsto }\limits ^{y_1}} (x_1,x_2) \circ \texttt{tree}(x_1,z,y_1) \circ x_2 \simeq z \circ y_1 \simeq y_2 ) \end{array} $$

For readability, all the expressions of the form have been replaced by $\texttt{tree}(x_2,z,y_1)$. Note that the rules are not $\mathfrak {h}$-regular, as $x_1$ and $x_2$ do not occur as roots in every rule, but they can easily be transformed into $\mathfrak {h}$-regular rules by replacing $x_1$ and $x_2$ by z in the third and fourth rule, respectively (using the equations $x_1 \simeq z$ and $x_2 \simeq z$). The definition can be applied recursively (i.e., $P_0,\dots ,P_n$ may be derived predicates). The next proposition is an immediate consequence of Definition 17:

Proposition 18

Let $\mathcal{R}$ be a $\mathfrak {h}$-regular SID. The rules associated with any predicate $P$ corresponding to an expression (Definition 17) are $\mathfrak {h}$-regular, up to the following equivalence: $\exists x\, (x \simeq y \circ \phi ) \equiv _{\mathcal{R}}^{{\mathfrak {P}}}\phi \{ x \leftarrow y \}$. Moreover, the rules are also $\exists$-restricted, with $\gamma _{\mathcal{R}}(P) = \gamma _{\mathcal{R}}(P_0)$ and $P\in \mathcal{P}^\star \iff P_0 \in \mathcal{P}^\star$. Finally if $\alpha = \texttt{emp}$ then .

Note that, however, the implication $P\in \mathcal{P}^\star \wedge Q\in \mathcal{P}\setminus \mathcal{P}^\star \implies P\bowtie _{\mathcal{R}}Q$ (Condition 4 in Definition 10) does not necessarily hold for derived predicates $P,Q$. The following lemma states a form of modus ponens, relating the connective $\circ$ with :

Lemma 19

If $\mathcal{R}$ is $\mathfrak {h}$-regular then .

The next lemma states that every predicate atom allocating x can be written as a $\circ$-formula in which x occurs as a root.

Lemma 20

Assume that $\mathcal{R}$ is $\exists$-restricted. Let $\pmb {y},\pmb {p}$ be vectors of location variables and permission terms, respectively. If $(\mathfrak {s},\mathfrak {h}) \models _{\mathcal{R}}^{{\mathfrak {P}}}Q(\pmb {y},\pmb {p})$, $\mathfrak {s}(x) \not = \mathfrak {s}(\pmb {y}|_{1})$ and $\mathfrak {s}(x) \in dom (\mathfrak {h})$, then there exist atoms of the form $P(x,\pmb {z},\pmb {q})$, $P_i(x_i,\pmb {y}_i,\pmb {q}_i)$ (with $i \in \{ 1,\dots ,n\}$), where $\pmb {z} \subseteq \pmb {y} \cup \{ x_1,\dots ,x_n \}$, $\pmb {y}_i \subseteq \{ \pmb {y}|_{j} \mid j \not \in \gamma _{\mathcal{R}}(Q) \}$, $\pmb {q} \subseteq \pmb {p}$ and $\pmb {q}_i \subseteq \pmb {p}$, such that: , with $\beta = P(x,\pmb {z},\pmb {q}) \circ \bigcirc _{i=1}^m P_i(x_i,\pmb {y}_i,\pmb {q}_i)$. Moreover, $P_i \in \mathcal{P}^\star$, $\{ x_1,\dots ,x_n \} \subseteq (x,\pmb {z})|_{\gamma _{\mathcal{R}}(P)}$ and $y \in \pmb {y} \cap \pmb {z} \wedge y \not \in \{ \pmb {y}|_{j} \mid j \not \in \gamma _{\mathcal{R}}(Q) \} \implies y \in (x,\pmb {z})|_{\gamma _{\mathcal{R}}(P)}$.

Intuitively, since x is allocated and the rules are $\mathfrak {h}$-regular, then necessarily some predicate atom of the form $P(x,\pmb {z},\pmb {q})$ must be called at some point during the unfolding of the rules. Using , this predicate can be removed from the call tree of $Q(\pmb {y},\pmb {p})$ and lifted at the root level in the formula. The atom $P(x,\pmb {z},\pmb {q})$ may contain variables not occurring in $Q(\pmb {y},\pmb {p})$ corresponding to existential variables introduced by unfolding. As the rules are $\exists$-restricted, all such variables $x_i$ must themselves appear as the root of some predicate atom $P_i(x_i,\pmb {y}_i,\pmb {q}_i)$ which contains (beside $x_i$) only variables occurring in $Q(\pmb {y},\pmb {p})$ (since $\gamma _{\mathcal{R}}(P_i) = \emptyset$, due to Condition 5 in Definition 10). Again, these atoms can be moved at the root level.

Definition 21

For all atoms $Q(\pmb {y},\pmb {p})$ we denote by $\delta [x]^+$ the set of formulas of the form as defined in Lemma 20. We also denote by $\delta [x]^=$ the formula: $\delta \circ (x \simeq \pmb {y}|_{1})$.

For every model of $\delta$, $\delta [x]^-$ holds if x is not allocated in $\delta$, $\delta [x]^=$ holds if x is equal to the root of $\delta$ and $\delta [x]^+$ holds if x is allocated but is not the root of $\delta$. The following result follows immediately from Lemmata 19 and 20:

Lemma 22

Assume that $\mathcal{R}$ is $\exists$-restricted. Let $x\in \mathcal{V}_\texttt{l}$. For every predicate atom $\delta$ such that $x \not \in roots (\delta )$, and for all structures $(\mathfrak {s},\mathfrak {h})$: $(\mathfrak {s},\mathfrak {h}) \models _{\mathcal{R}}^{{\mathfrak {P}}}\delta$ iff there exists $\psi \in \{ \delta [x]^-, \delta [x]^= \} \cup \delta [x]^+$ such that $(\mathfrak {s},\mathfrak {h}) \models _{\mathcal{R}}^{{\mathfrak {P}}}\psi$.

For instance the atom $\texttt{lseg}(x,y,z)$ holds iff one of the formulas $\texttt{lseg}(x,y,z) \circ x \simeq y$, $\texttt{lseg}(x,y,z)[y]^-$ or holds. The second formula corresponds to the case where y is not allocated, and the first and third ones correspond to the case where there is a loop on y. By applying repeatedly Lemma 22 on every variable x and atom $\delta$ we eventually obtain a disjunction of normalized formulas:

Lemma 23

Let $\mathcal{R}$ be a $\exists$-restricted SID. There exists an algorithm transforming any symbolic heap $\phi$ containing no points-to atom into a set of normalized formulas $\varPsi$ such that for all structures $(\mathfrak {s},\mathfrak {h})$: $(\mathfrak {s},\mathfrak {h}) \models _{\mathcal{R}}^{{\mathfrak {P}}}\phi$ iff there exists $\psi \in \varPsi$ such that $(\mathfrak {s},\mathfrak {h}) \models _{\mathcal{R}}^{{\mathfrak {P}}}\psi$. Furthermore, every formula in $\varPsi$ is a (quantified) separating conjunction of $\circ$-formulas.

4.2 Commuting Separating and Disjoint Connections

The next step consists in showing that – under some particular conditions enforced by the previous transformation – the operator $*$ can be pushed innermost in the formula (below the operator $\circ$). To this aim, we exploit an essential property of $\mathfrak {h}$-regular SIDs, namely that all the locations that occur in the heap of some model of a formula $\phi$ but are not allocated correspond to a variable in $fv (\phi )$. We shall denote by $cut (L,L',\mathfrak {h})$ the set of locations reachable from $L$ in $\mathfrak {h}$, from a path not crossing $L'$:

Definition 24

Let $\mathfrak {h}$ be a heap, let $L, L'\subseteq \mathcal{L}$. We denote by $cut (L,L',\mathfrak {h})$ the set of locations inductively defined as follows: $L\subseteq \ cut (L,L',\mathfrak {h})$, and if $\ell ' \in cut (L,L',\mathfrak {h})$, $\mathfrak {h}(\ell ') = (\ell _1,\dots ,\ell _k,\pi )$, $i \in \{ 1,\dots ,k\}$ and $\ell _i \not \in L'$ then $\ell _i \in cut (L,L',\mathfrak {h})$.

The following lemma characterizes the domain of the part of the heap satisfying some formula $\phi$:

Lemma 25

Let $\mathcal{R}$ be a $\mathfrak {h}$-regular SID and let $\phi$ be a $\circ$-formula containing no quantifier. Let $\mathfrak {s}$ be a store and let $\mathfrak {h},\mathfrak {h}'$ be heaps, with $\mathfrak {h}' \le \mathfrak {h}$ . Let V be a set of variables, with $fv (\phi ) \subseteq V \cup roots (\phi )$ and $\mathfrak {s}(V) \cap dom (\mathfrak {h}') = \emptyset$. If $(\mathfrak {s},\mathfrak {h}') \models _{\mathcal{R}}^{{\mathfrak {P}}}\phi$ then $dom (\mathfrak {h}') = cut (\mathfrak {s}( roots (\phi )),\mathfrak {s}(V),\mathfrak {h})$.

The commutation property, pushing $*$ below $\circ$, is given by Lemma 26:

Lemma 26

Let $\mathcal{R}$ be a $\mathfrak {h}$-regular SID. Let $V \subseteq \mathcal{V}_\texttt{l}$ and let $\phi$ be a normalized formula, of the form , where, for all $i \in \{ 1,\dots ,n \}$, $roots (\phi _i) = V$ and $( roots (\psi _i) \cup roots (\psi ')) \cap V = \emptyset$. Then $\phi$ is $(\mathcal{R},{\mathfrak {P}})$-satisfiable iff is $(\mathcal{R},{\mathfrak {P}})$-satisfiable.

Roughly speaking, as $roots (\phi _i) = V$ and $\phi _i$ is normalized, it is possible to prove, using the characterization given in Lemma 25, that the parts of the heap that correspond to the formulas $\phi _i$ have all the same domain. This entails that the heaps corresponding to the formulas $\psi _i$ and $\phi _{i'}$ are disjoint, which permits to prove that can be written , yielding the result.

4.3 Merging of Spatial Predicates

We show that, under some particular conditions, it is possible to replace the separating conjunction of two spatial atoms having the same root by a single spatial atom. The rules defining this atom are obtained by combining the rules of the two initial atoms. More precisely, consider any $\mathfrak {h}$-regular SID $\mathcal{R}$ and two spatial atoms $P(x,\pmb {y},\pmb {p})$ and $P'(x,\pmb {y}',\pmb {p}')$ sharing the same root x, where $\pmb {y},\pmb {y}'$ are vectors of location variables and $\pmb {p}$ and $\pmb {p}'$ are vectors of permission terms. We denote by $P(x,\pmb {y},\pmb {p})\triangledown P'(x,\pmb {y}',\pmb {p}')$ any atom $Q(x,\pmb {y},\pmb {y}', \pmb {p}, \pmb {p}')$ where $Q$ is associated with rules of the form:

$$\begin{aligned} Q(v,\pmb {w},\pmb {w}',\pmb {z},\pmb {z}'){} & {} \Leftarrow \exists u_1,\dots ,u_n\quad v {\mathop {\mapsto }\limits ^{q}} (v_1,\dots ,v_k) \\{} & {} \qquad \qquad \ \ \circ \bigcirc _{i=1}^n (Q_i(u_i,\pmb {y}_i,\pmb {q}_i)\triangledown Q_i'(u_i,\pmb {y}_i',\pmb {q_i}')) \circ \phi \circ \phi ' \circ \psi \end{aligned}$$

with , for all pairs of rules of the following forms in $\mathcal{R}$ (with the same numbers k and n, and up to $\alpha$-renaming, so that the rules share the same existential variables):

$$ \begin{array}{lll} P(v,\pmb {w},\pmb {z}) &{} \Leftarrow &{} \exists u_1,\dots ,u_n\quad v {\mathop {\mapsto }\limits ^{p}} (v_1,\dots ,v_k) \circ \bigcirc _{i=1}^n Q_i(u_i,\pmb {y}_i,\pmb {q}_i) \circ \phi \\ P'(v,\pmb {w}',\pmb {z}') &{} \Leftarrow &{} \exists u_1,\dots ,u_n\quad v {\mathop {\mapsto }\limits ^{p'}} (v_1',\dots ,v_k') \circ \bigcirc _{i=1}^n Q_i'(u_i,\pmb {y}_i',\pmb {q}_i') \circ \phi '\ \end{array} $$

where $\psi = \bigcirc _{i=1}^k (v_i \simeq v_i')$. Note that all the produced rules are $\mathfrak {h}$-regular⁸.

Lemma 27

Let $\mathcal{R}$ be a $\mathfrak {h}$-regular SID. Let $x\in \mathcal{V}_\texttt{l}$ and let $(\mathfrak {s},\mathfrak {h})$ be a structure such that $\mathfrak {s}(y) \not \in dom (\mathfrak {h})$ holds for all variables y such that $\mathfrak {s}(x) \not = \mathfrak {s}(y)$. Then $(\mathfrak {s},\mathfrak {h}) \models _{\mathcal{R}}^{{\mathfrak {P}}}P(x,\pmb {y},\pmb {p}) \triangledown P'(x,\pmb {y}',\pmb {p}') \iff (\mathfrak {s},\mathfrak {h}) \models _{\mathcal{R}}^{{\mathfrak {P}}}P(x,\pmb {y},\pmb {p}) *P'(x,\pmb {y}',\pmb {p}')$.

The result crucially depends on the fact that the parts of the heap that correspond to $P(x,\pmb {y},\pmb {p})$ and $P'(x,\pmb {y}',\pmb {p}')$ respectively must share the same domain, since otherwise, as $\mathcal{R}$ is $\mathfrak {h}$-regular, a free variable would be allocated, contradicting the hypothesis. This ensures that the heap can be generated by the above rules.

4.4 Heap Abstractions and Main Result

As we shall see later, the previous transformations can be used to transform any symbolic heap into a $\circ$-formula (while preserving satisfiability). The final step is to devise an algorithm to test the satisfiability of $\circ$-formulas. As it is done in [6] for standard heap models, the algorithm works by constructing relevant abstractions of the models of the predicate atoms. It suffices to keep track of the truth value of the equational atoms, of the allocated variables and of the permission atoms satisfied by the structure.

Definition 28

A heap abstraction is a tuple ${\mathfrak {a}}= (V_{{\mathfrak {a}}},\sim _{{\mathfrak {a}}},A_{{\mathfrak {a}}},\rho _{{\mathfrak {a}}})$ where $V_{{\mathfrak {a}}}$ is a finite set of variables, $\sim _{{\mathfrak {a}}}$ is an equivalence relation on the variables of sort $\texttt{l}$ occurring in $V_{{\mathfrak {a}}}$, $A_{{\mathfrak {a}}}$ is a subset of $V_{{\mathfrak {a}}}\cap \mathcal{V}_\texttt{l}$, closed under $\sim _{{\mathfrak {a}}}$ (i.e., for all $x,y \in \mathcal{V}_\texttt{l}$: $x \in A_{{\mathfrak {a}}} \wedge x \sim _{{\mathfrak {a}}} y \implies y \in A_{{\mathfrak {a}}}$), and $\rho _{{\mathfrak {a}}}$ is a permission formula (with variables in $V_{{\mathfrak {a}}}$).

Definition 29

Let $(\mathfrak {s},\mathfrak {h})$ be a structure and let ${\mathfrak {a}}= (V_{{\mathfrak {a}}},\sim _{{\mathfrak {a}}},A_{{\mathfrak {a}}},\rho _{{\mathfrak {a}}})$ be a heap abstraction. We write $(\mathfrak {s},\mathfrak {h}) \models ^{{\mathfrak {P}}}{\mathfrak {a}}$ if all the following conditions are satisfied: (i) For all variables $x,y \in V_{{\mathfrak {a}}} \cap \mathcal{V}_{\texttt{l}}$: $x \sim _{{\mathfrak {a}}} y \iff \mathfrak {s}(x) = \mathfrak {s}(y)$; (ii) for all $x \in V_{{\mathfrak {a}}} \cap \mathcal{V}_{\texttt{l}}$, $x \in A_{{\mathfrak {a}}} \iff \mathfrak {s}(x) \in dom (\mathfrak {h})$; and (iii) $\mathfrak {s}\models ^{{\mathfrak {P}}}\rho _{{\mathfrak {a}}}$. A heap abstraction is ${\mathfrak {P}}$-satisfiable if there exists a structure $(\mathfrak {s},\mathfrak {h})$ such that $(\mathfrak {s},\mathfrak {h}) \models ^{{\mathfrak {P}}}{\mathfrak {a}}$.

Proposition 30

A heap abstraction ${\mathfrak {a}}$ is ${\mathfrak {P}}$-satisfiable iff $\rho _{{\mathfrak {a}}}$ is ${\mathfrak {P}}$-satisfiable.

For all $\circ$-formulas $\phi$, we define a set of heap abstractions ${\mathfrak {A}}(\phi )$ by mutual induction as follows. The sets ${\mathfrak {A}}(\phi )$ are the least sets of heap abstractions satisfying the following properties, for all finite sets of variables⁹ $V\supseteq fv (\phi )$ and for all equivalence relations $\sim$ on $V\cap \mathcal{V}_\texttt{l}$: (i) if $\phi = x {\mathop {\mapsto }\limits ^{p}} (y_1,\dots ,y_n)$ then $(V,\sim ,\{ y \mid y \mid y \sim x \}, { def }(p)) \in {\mathfrak {A}}(\phi )$. (ii) if $\phi = x \simeq y$ (resp. $x \not \simeq y$) with $x,y\in \mathcal{V}_\texttt{l}$ and $x \sim y$ (resp. $x \not \sim y$) then $(V,\sim ,\emptyset ,\texttt{emp}) \in {\mathfrak {A}}(\phi )$; (iii) if $\phi$ is a permission formula then $(V,\sim ,\emptyset ,\phi ) \in {\mathfrak {A}}(\phi )$; (iv) if $\phi = \exists x\, \psi$, $(V,\sim ,A,\rho ) \in {\mathfrak {A}}(\psi )$ then $(V\setminus \{ x \}, \sim ',A\setminus \{ x \}, \rho ) \in {\mathfrak {A}}(\phi )$, where $\sim '$ denotes the restriction of $\sim$ to the variables distinct from x, i.e., (note that x cannot occur in $\rho$, since quantification over permission variables is not allowed); (v) if $\phi = \phi _1 \circ \phi _2$, $(V,\sim ,A_i,\rho _i) \in {\mathfrak {A}}(\phi _i)$ (for all $i = 1,2$) with $A_1 \cap A_2 = \emptyset$, then $(V,\sim ,A_1 \cup A_2, \rho _1 \circ \rho _2) \in {\mathfrak {A}}(\phi )$; (vi) if $\phi = P(\pmb {x},\pmb {p})$ and $\phi \Leftarrow _{\mathcal{R}} \xi$ then ${\mathfrak {A}}(\xi ) \subseteq {\mathfrak {A}}(\phi )$.

Lemma 31

A $\circ$-formula $\phi$ is $(\mathcal{R},{\mathfrak {P}})$-satisfiable iff at least one of the abstractions in ${\mathfrak {A}}(\phi )$ is ${\mathfrak {P}}$-satisfiable.

Putting things together we get the following result:

Theorem 32

If ${\mathfrak {P}}$-satisfiability is decidable for permission formulas, then there exists an algorithm that, for every $\exists$-restricted SID, decides whether a given formula $\phi$ is $(\mathcal{R},{\mathfrak {P}})$-satisfiable. If, moreover, ${\mathfrak {P}}$-satisfiability is in Exptime, then $(\mathcal{R},{\mathfrak {P}})$-satisfiability is also in Exptime (for $\exists$-restricted SID). Finally, for every permission model ${\mathfrak {P}}$, $(\mathcal{R},{\mathfrak {P}})$-satisfiability is Exptime-hard (for $\exists$-restricted SID).

5 Using Separating Conjunctions Inside Rules

To end the paper, we wish to point out that the satisfiability problem is undecidable from $\exists$-restricted SID if the disjoint separation $\circ$ is replaced by the standard separating connective $*$ in the inductive definitions (see Definition 7). We think that the result is of some theoretical interest, although, as explained above, rules using $\circ$ are actually more convenient for describing data structures. The notions of $*$-$\mathfrak {h}$-regular and $*$-$\exists$-restricted SID are defined exactly as $\mathfrak {h}$-regular SID and $\exists$-restricted SID (Definitions 7 and 10) except that the symbol $\circ$ is replaced by $*$ everywhere (for conciseness the formal definitions are omitted).

Theorem 33

Let ${\mathfrak {P}}$ be any permission model and assume that for every , there exists $\pi \in \mathcal{P}_{\mathfrak {P}}$ such that $\pi ^n$ is defined. The $(\mathcal{R},{\mathfrak {P}})$-satisfiability problem is undecidable for $*$-$\exists$-restricted SID.

6 Conclusion and Future Work

An algorithm was devised to test the satisfiability of symbolic heaps in Separation Logic with inductively defined predicates and permissions, under some (syntactic) conditions on the inductive rules giving the semantics of the spatial predicates. The algorithm runs in exponential time, provided the satisfiability of permission formulas is in Exptime. In addition, we showed that some natural relaxings of these conditions make the problem undecidable (under some minimal assumptions on the permission model). The next step is to investigate the entailment problem for the considered fragment. The techniques devised in the present paper for transforming symbolic heaps into disjoint conjunctions of atoms should serve as a basis for this purpose, but the extension is not straightforward. Another (much easier) extension that could be of practical relevance is to consider formulas with labels (in the sense of [5]) which allow one to express additional equality conditions on some parts of the structures. In our context, labels would simply yield additional conditions on the decomposition generated during the normalization step: two formulas sharing the same label should be decomposed into formulas with the same set of roots. It could also be interesting to relax some of the conditions on the rules, for instance to allow for existential variables not occurring as roots in the rules. This is required to encode data structures with forward pointers, such as skip lists. It is also unclear whether Condition 4 in Definition 10 is required for decidability. Finally, the decision algorithm could probably be extended to handle arbitrary combinations of disjoint and separating conjunctions.