A Decision Procedure for Satisfiability in Separation Logic with Inductive Predicates James Brotherston ∗ Carsten Fuhs † Juan A. Navarro P´erez ‡ University College London {j.brotherston,c.fuhs,juan.navarro}@ucl.ac.uk Abstract We show that the satisfiability problem for the “symbolic heap” fragment of separation logic with general inductively defined predicates — which includes most fragments employed in program verification — is decidable. Our decision procedure is based on the computation of a certain fixed point from the definition of an inductive predicate, called its “base”, that exactly characterises its satisfiability. A complexity analysis of our decision procedure shows that it runs, in the worst case, in exponential time. In fact, we show that the satisfiability problem for our inductive predicates is EXPTIMEcomplete, and becomes NP-complete when the maximum arity over all predicates is bounded by a constant. Finally, we provide an implementation of our decision procedure, and analyse its performance both on a synthetically generated set of test formulas, and on a second test set harvested from the separation logic literature. For the large majority of these test cases, our tool reports times in the low milliseconds. Categories and Subject Descriptors F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs—Mechanical verification, assertions; F.2.2 [Analysis of Algorithms and Problem Complexity]: Nonnumerical Algorithms and Problems—Complexity of proof procedures General Terms Algorithms, Theory, Verification Keywords separation logic, inductive predicates, satisfiability, decision procedure 1. Introduction Separation logic [26] is an established and fairly popular formalism for verifying imperative, heap-manipulating programs. At the ∗ Research supported by an EPSRC Career Acceleration Fellowship. supported by EPSRC grants EP/K040863/1 and EP/H008373/2. ‡ Research supported by EPSRC grants EP/K040863/1 and EP/K032542/1. † Research Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the owner/author(s). CSL-LICS 2014, July 14–18, 2014, Vienna, Austria. Copyright is held by the owner/author(s). ACM 978-1-4503-2886-9/14/07. http://dx.doi.org/10.1145/2603088.2603091 Nikos Gorogiannis Middlesex University London [email protected] time of writing, there are a number of automatic program verification tools based on separation logic, such as SLAYER [5] and A BDUCTOR [12], capable of establishing memory safety properties of code bases extending into millions of lines [28]. These verification tools are highly dependent on the use of inductively defined predicates to describe the shape of data structures held in memory, such as linked lists or trees. Currently, such predicates must be hard-coded into these verification tools, which limits the range of data structures that they can handle automatically. Thus, the next step in automation is to handle general inductive predicates, which might be provided to the analysis by the user, or even inferred automatically [10]. When one considers arbitrary inductive predicates, however, it becomes much more difficult to determine whether a given formula is satisfiable or not. This may lead to performance degradation when time is spent on the analysis of inconsistent scenarios. In this paper we address the latter problem by showing that the satisfiability problem for the most commonly considered symbolic heap fragment of separation logic, extended with general inductive predicates, is in fact decidable. Our decision procedure rests upon the observation that the satisfiability of each inductive predicate can be precisely characterised by an approximation of its set of models, an object which we refer to as the base of the predicate. Roughly speaking, the base of a predicate records, for each distinct way of constructing a satisfying model, the subset of arguments of the predicate that are required to be allocated and distinct in memory, as well as the equalities and disequalities that must hold between these arguments. Since there are clearly only finitely many possible such subsets and equality/disequality relations between predicate arguments, the base can be straightforwardly computed in finite time. Having computed the base of all required predicates, deciding the satisfiability of arbitrary formulas in the fragment then becomes a straightforward matter. A complexity analysis of our decision procedure shows that, in the worst case, it runs in exponential time (in the size of the underlying set of inductive definitions). Essentially, this is because our inductive definition schema allows us to construct predicates that admit an exponential number of elements in their base. Indeed, we show that the satisfiability problem for our inductive predicates is EXPTIME-complete. Additionally, if the maximum arity of all inductive predicates is bounded, then the satisfiability problem becomes NP-complete. We also provide an implementation of our decision procedure, which is available online [1], and evaluate its performance over three test sets: (a) a collection of example formulas drawn from the literature on separation logic verification; (b) a large set of inductive predicates automatically generated by the C ABER predicate inference tool [10]; and (c) a set of synthetically generated examples, varying in parameters such as the number of arguments or recursive calls. Although exponential time performance can be produced by a suitable choice of parameters, we find that for the vast majority of examples, the algorithm terminates in a matter of milliseconds. Consequently, we believe our decision procedure is highly suitable for use as a black-box satisfiability checker in automated separation logic verification. We propose a number of direct applications of such a satisfiability checker at the end of this paper (in Section 7). The problem of satisfiability for separation logic with inductive definitions was also recently considered by Iosif et al. [20]. Their paper establishes decidability results for both satisfiability and entailment problems via an embedding into monadic second order logic, but for technical reasons their results are restricted to a fragment of the logic from which many natural data structure definitions are excluded; for example, inductive predicates may not define structures with dangling data pointers (cf. Section 6.1). In contrast, the fragment of separation logic for which we decide satisfiability includes a much larger class of inductive predicates, but we do not consider the entailment problem for this fragment, which is undecidable [2]. We also provide complexity results on the satisfiability problem for our fragment, and an implementation of our decision procedure. The remainder of this paper is structured as follows. We introduce our fragment of separation logic with inductive definitions in Section 2, and then present our decision procedure and the proof of its correctness in Section 3. Section 4 contains our complexity analysis of our algorithm and of the satisfiability problem itself. Section 5 describes the implementation of our decision procedure and its evaluation. Section 6 surveys related work in the area, and Section 7 concludes. 2. Inductive definitions in separation logic Here we present our fragment of inductive definitions in separation logic, following the approach in [9]. 2.1 Syntax First, some preliminaries. A term is either a variable drawn from the infinite set Var, or the constant symbol nil. We write Term for the set of all terms. We also assume a fixed finite set P1 , . . . , Pn of predicate symbols, each with an associated arity. We often write vector notation to abbreviate tuples; e.g. we typically write x rather than (x1 , . . . , xm ). We write πi (−) for the i-th projection function on tuples, and sometimes abuse notation slightly by writing x ∈ x to mean that x occurs in the tuple x. Finally, we write Pow(X) for the powerset of a set X. Definition 2.1. Spatial formulas F and pure formulas G are given by the following grammar: heap, Pi is a predicate symbol of arity ai , and x is a tuple of ai distinct variables. Variables in the body, Π : F , but not the head, Pi (x), of a rule are implicitly existentially quantified, while multiple bodies of the same head are interpreted as a disjunction. The formal semantics is given in the next section. Our strict formatting of the heads of inductive rules, with variable repetitions and occurrences of nil disallowed, is for technical convenience. It does not restrict expressivity since we can achieve the same effect by placing equalities in the bodies of inductive rules. For example, a rule of the form ⇒ P (x, x, nil) is not allowed by our schema, but the equivalent inductive rule x = y, z = nil ⇒ P (x, y, z) is allowed. 2.2 Semantics We use a typical RAM model employing heaps of records. An infinite set Val of values is assumed, of which an infinite subset Loc ⊂ Val are locations, i.e., the addresses of heap cells. We also assume a “nullary” value nil ∈ Val\Loc which is not the address of any heap cell. A stack is a function s : Var → Val; we extend stacks to terms by setting s(nil) =def nil , and extend stacks pointwise to act on tuples of terms. We write s[x 7→ v] for the stack defined as s except that (s[x 7→ v])(x) = v. A heap is a partial function h : Loc *fin (Val List) mapping finitely many locations to (arbitrary-length) tuples of values; we define dom(h) =def {` ∈ Loc | h(`) is defined} and e to be the empty heap that is undefined everywhere. We write ◦ to denote composition of heaps: if h1 and h2 are heaps, then h1 ◦ h2 is the union of (partial functions) h1 and h2 when dom(h1 ) ∩ dom(h2 ) = ∅, and undefined otherwise. We write h[` 7→ v] for the heap defined as h except that (h[` 7→ v])(`) = v, and just [` 7→ v] as a shorthand for e[` 7→ v]. We write Heap for the set of all heaps. Given an inductive rule set Φ, the relation s, h |=Φ F for satisfaction of a pure or spatial formula F by the stack s and heap h is defined as follows: s, h |=Φ t1 = t2 s, h |=Φ t1 = 6 t2 ⇔ ⇔ s(t1 ) = s(t2 ) s(t1 ) 6= s(t2 ) s, h |=Φ emp ⇔ h=e s, h |=Φ t 7→ t ⇔ dom(h) = {s(t)} and h(s(t)) = s(t) s, h |=Φ Pi t ⇔ s, h |=Φ F1 ∗ F2 ⇔ (s(t), h) ∈ JPi KΦ h = h1 ◦ h2 and s, h1 |=Φ F1 and s, h2 |=Φ F2 where t ranges over terms, Pi over the predicate symbols and t over tuples of terms (matching the arity of Pi in Pi t). We write PureSet for the set of all finite sets of pure formulas. A symbolic heap is given by Π : F , where F is a spatial formula and Π ∈ PureSet (note that Π should be read intuitively as the conjunction of its elements). Whenever one of Π, F is empty, we will omit the colon. We write the substitution notation F [t/x] for the result of simultaneously replacing all occurrences of the variable x by the term t in the formula F . Substitution extends to sets of formulas in the obvious way. where the semantics JPi KΦ of the inductive predicate Pi under Φ is defined below. If Π : F is a symbolic heap then we write s, h |=Φ Π : F to mean that s, h |=Φ F and s, h |=Φ G for all G ∈ Π; equivalently, we say that (s, h) is a model of Π : F (w.r.t. Φ). A symbolic heap Π : F is satisfiable (w.r.t. Φ) if it has at least one model. We remark that satisfaction of pure formulas does not depend on the heap nor on the inductive rules: we write s |= Π, where Π ∈ PureSet, to mean that s, h |=Φ Π for any heap h and inductive definition set Φ. The following definition gives the standard semantics of the inductive predicate symbols P according to a fixed inductive rule set Φ, i.e., as the least fixed point of an n-ary monotone operator constructed from Φ: Definition 2.2. An inductive rule set is a finite set of inductive rules, each of the form Π : F ⇒ Pi x, where Π : F is a symbolic Definition 2.3. First, for each predicate Pi ∈ P with arity ai say, we define τi = Pow(Val ai × Heap). Furthermore, we partition F ::= emp | t 7→ t | Pi t | F ∗ F G ::= t = t | t 6= t the rule set Φ into Φ1 , . . . , Φn , where Φi is the set of all inductive rules in Φ of the form Π : F ⇒ Pi x. We let each Φi be indexed by j (i.e., Φi,j is the j-th rule defining Pi ), and for each inductive rule Φi,j of the form Π : F ⇒ Pi x, we define the operator ϕi,j : τ1 × . . . × τn → τi by: ϕi,j (Y) =def {(s(x), h) | s, h |=X Π : F } where Y ∈ τ1 ×. . .×τn and |=Y is the satisfaction relation defined above, except that JPi KY =def πi (Y). We then finally define the tuple JPKΦ ∈ τ1 × . . . × τn by: S S JPKΦ =def µY. ( j ϕ1,j (Y), . . . , j ϕn,j (Y)) We write JPi KΦ as an abbreviation for πi (JPKΦ ). As in [9], Definition 2.3 interprets the inductive rules Φi as exhaustive, disjunctive clauses of the definition of the predicate Pi . 3. A decision procedure for satisfiability of inductive predicates In this section, we present our decision procedure for satisfiability in the symbolic heap fragment of separation logic with inductive predicates, given in Section 2. Our first definition is used to normalise terms in pure formulas with respect to a given set of variables. This is then used in our second definition, which provides a satisfiability-preserving means of restricting the variables which occur in a set of pure formulas. Definition 3.1. Let Π ∈ PureSet and let x be a tuple of distinct variables. The equalities in Π determine an equivalence relation among terms. We say that an equivalence class is observable (from x with respect to Π), if the class contains some term in x ∪ {nil}. A term is observable just in case it belongs to an observable equivalence class. For each equivalence class, we choose a term from the class, called its canonical representative. For observable classes, we choose nil to be the representative if nil is in the class, otherwise we choose a variable from x. For non-observable classes, the choice is arbitary. The normal form of a term t, denoted htiΠ,x , is defined to be t itself when t ∈ x ∪ {nil}, or the canonical representative of its equivalence class otherwise. Definition 3.2. Let Π ∈ PureSet and let x be a tuple of distinct variables. We denote by Π x the formula obtained after: (i) removing all pure formulas, t1 = t2 or t1 6= t2 , where at least one of t1 or t2 is not observable; and (ii) replacing all remaining terms t by their normal forms htiΠ,x . Note that Definition 3.2 ensures every term occurring in Π x is either nil, or a variable from x. The satisfiability-preserving nature of this variable restriction is formalised by the following pair of lemmas. Lemma 3.3. Let Π be a finite set of pure formulas. If s |= Π and s(x) = s0 (x) then s0 |= Π x. Proof. Since s |= Π, we know that s must assign the same value to all variables sharing the same equivalence class. Thus s |= Π x, since both dropping formulas from Π and replacing terms by their normal forms preserve its satisfiability. Now, Π x is restricted to contain only variables from x and, since s and s0 agree on those variables, s0 |= Π x. Lemma 3.4. Let Π be a finite set of pure formulas. If Π is satisfiable and s |= Π x then there exists a stack s0 with s0 (x) = s(x) such that s0 |= Π. Furthermore, given any finite set W ⊆ Loc, we can choose s0 such that s0 (y) ∈ / W for all non-observable variables y. define base Φ P: Y := (λt1 . ∅, . . . , λtn . ∅) repeat until Y reaches a fixed point: pick a rule Φi,j ∈ Φ with head Pi x for each Pj` (x` ) in the body of Φi,j : pick a base pair (V` , Π` ) ∈ Yj` (x` ) take y1 , . . . , yk from all y` 7→ u` in the body of Φi,j take Π0 the pure part in the body of Φi,j V := V1 ∪ · · · ∪ Vm ∪ {y1 , . . . , yk } N Π := V ∪ Π0 ∪ Π1 ∪ · · · ∪ Πm if Π is satisfiable: add alloced (V, x, Π)[t/x], (Π x)[t/x] to Yi (t) return Y Figure 1. Pseudocode for the computation of base Φ P in Defn. 3.5. Proof. Let Y1 , . . . , Yn be the equivalence classes of all variables occurring in, and determined by, Π. Choose distinct values `1 , . . . , `n in Loc such that each `i ∈ / s(x ∪ {nil}) ∪ W . This is possible because the number of locations in Loc is infinite, while the number of forbidden locations is finite. We then define ( s(hxiΠ,x ) if x is observable 0 s (x) = `i otherwise, where x ∈ Yi . By construction s and s0 agree on variables from x, i.e. directly observable ones, and s0 (y) ∈ / W when y is not observable. It is easy to check now that s0 satisfies all pure formulas in Π. • For every t1 = t2 ∈ Π: By definition, t1 and t2 are in the same equivalence class. Thus if t1 is observable then so, necessarily, is t2 , and furthermore the formula ht1 iΠ,x = ht2 iΠ,x is in Π x. Therefore, by assumption, s |= ht1 iΠ,x = ht2 iΠ,x , and since s0 (ti ) = s(hti iΠ,x ), we have s0 |= t1 = t2 . Otherwise, if t1 is not observable, then neither is t2 ; but, since they share an equivalence class, we have s0 (t1 ) = `i = s0 (t2 ) for some i by construction, and so s0 |= t1 = t2 as required. • For every t1 6= t2 ∈ Π: If both t1 and t2 are observable, then ht1 iΠ,x 6= ht2 iΠ,x is in Π x, so s |= ht1 iΠ,x 6= ht2 iΠ,x by assumption. Since s0 (ti ) = s(hti iΠ,x ), it follows that s0 |= t1 6= t2 . If one of the terms, say t1 , is observable but the other, t2 , is not, then s0 (t2 ) was explicitly chosen to be different to s(ht1 iΠ,x ) = s0 (t1 ), and so s0 |= t1 6= t2 . If neither t1 nor t2 is observable, then they must be in different equivalence classes, otherwise Π would be unsatisfiable, contrary to assumption. Thus, by construction, s0 |= t1 6= t2 . We now present our main definition, which explains how to extract from a fixed inductive rule set Φ all the information needed to decide the satisfiability of any symbolic heap over Φ. The pseudocode in Figure 1 provides an informal aid to navigate the steps of the computation. Definition 3.5 (Base pair computation). First, for each predicate symbol Pi with associated arity ai , where 1 ≤ i ≤ n, we define σi =def Termai → Pow(MPow(Var) × PureSet) where MPow(Var) denotes the set of allN multisets of variables. For any finite V ∈ MPow(Var) we define V ∈ PureSet to be the set of pure formulas comprising: • all formulas of the form x 6= x0 such that x and x0 are different elements N of V (note this means that if V contains duplicates then V is unsatisfiable); • the formula x 6= nil for every element x of V . For any finite multiset V of variables, any tuple of variables x, and any Π ∈ PureSet, let alloced (V, x, Π) denote the multiset containing the term hyiΠ,x for each y N∈ V observable from x with respect to Π. Note that if Π ∪ V is satisfiable, then alloced (V, x, Π) contains only variables (no nil) and no duplicates. In this way we represent, using only variables from x, the observable locations allocated via V . The inductive rule set Φ is partitioned into Φ1 , . . . , Φn with each Φi further indexed by j as in Definition 2.3. Without loss of generality, we consider each Φi,j ∈ Φ to be written in the form Π0 : y1 7→ u1 ∗ . . . ∗ yk 7→ uk ∗ Pj1 (x1 ) ∗ . . . ∗ Pjm (xm ) ⇒ Pi x, (IndRule) where Π0 ∈ PureSet. We use the inductive rule Φi,j to define an operator Ψi,j : σ1 × . . . × σn → σi as follows. If Y = (Y1 , . . . , Yn ) where each Yi ∈ σi , and t is a tuple of ai terms, then Ψi,j (Y) : σi sends t to the set of pairs (we shall call these pairs also base pairs) alloced (V, x, Π)[t/x], (Π x)[t/x] that satisfy the following: V = V1 ∪ · · · ∪ Vm ∪ {y1 , . . . , yk }, N Π= V ∪ Π0 ∪ Π1 ∪ · · · ∪ Πm is satisfiable, and ∀1 ≤ ` ≤ m. (V` , Π` ) ∈ Yj` (x` ). Note that the substitution [t/x] in the above is defined pointwise over tuples; this is well defined since x is a tuple of distinct variables, as per Definition 2.2. Note also that while alloced (V, x, Π) might be viewed as a set (i.e., without repetitions), it is important to understand alloced (V, x, Π)[t/x] as a multiset since the substitution may map different variables to the same term. We then define base Φ P ∈ σ1 × . . . × σn as follows: S S base Φ P =def µY. ( j Ψ1,j (Y), . . . , j Ψn,j (Y)) where,Sby pointwise extension of the union to act on functions, we write j Ψi,j (Y) to denote the function mapping a tuple of terms S t to the set j Ψi,j (Y)(t). We also write base Φ Pi to abbreviate πi (base Φ P). Example 3.6. Consider the following set Φ of inductive rules: Φ1,1 : x = nil ⇒ P (x) Φ1,2 : Φ2,1 : x 6= nil : Q(x, x) ⇒ P (x) y = nil, x 6= nil : x 7→ (d, c) ∗ P (d) ⇒ Q(x, y) Φ2,2 : y 6= nil : y 7→ (d, c) ∗ Q(x, c) ⇒ Q(x, y). These rules are an intermediate product of the analysis done by the tool C ABER [10] on code that traverses a list of lists, and are found to be ultimately unsatisfiable by our algorithm, triggering backtracking in C ABER. In accordance with Definition 3.5, we define: σ1 = Term → Pow(MPow(Var) × PureSet) σ2 = Term × Term → Pow(MPow(Var) × PureSet) . That is, σ1 and σ2 are function spaces mapping suitably many terms to sets of base pairs for P and Q, respectively. We can compute base Φ (P, Q) by iteratively computing the sequence of its fixed point approximants ((Y1i , Y2i ) ∈ σ1 × σ2 )i≥0 in the standard way. That is, we begin with an empty base for both predicates, namely Y0 = (λx. ∅, λx, y. ∅), and iteratively apply the operators Ψi,j given by Definition 3.5. First iteration: The inductive rule Φ1,1 for P (x) can be applied to Y0 , yielding V = ∅ and Π = {x = nil}. The set Π is satisfiable and, therefore, Ψ1,1 (Y10 , Y20 ) = λx. (∅, {x = nil}) . Since Y0 does not contain any base pairs, the remaining rules cannot be applied to it, and so Y1 = (Y11 , Y21 ) where Y11 = λx. (∅, {x = nil}) Y21 = λx, y. ∅ . Second iteration: The inductive rule Φ1,1 generates the same base pair as before, while Φ1,2 and Φ2,2 are still not applicable to Y1 . However, the rule Φ2,1 defining Q(x, y) can be now applied, taking (∅, {x = nil}) from the current base Y11 of P (x). After restricting and normalising to the set of observable variables, this produces the new base pair ({x}, {y = nil, x 6= nil}). Thus, at the end of the iteration, Y2 = (Y12 , Y22 ) where Y12 = λx. (∅, {x = nil}) Y22 = λx, y. ({x}, {y = nil, x 6= nil}) . Third iteration: The rule Φ1,2 is now applicable to Y2 , instantiating the current pair for Q(x, x), but yields an unsatisfiable Π. Similarly, the rule Φ2,2 can be applied, taking the base pair ({x}, {c = nil, x 6= nil}) from Y22 instantiated to Q(x, c). After a suitable variable restriction and normalisation, this produces the following new base pair for Q(x, y): ({x, y}, {x 6= y, y 6= nil, x 6= nil}) 3 Thus Y = (Y13 , Y23 ) where Y13 = λx. (∅, {x = nil}) ({x}, {y = nil, x 6= nil}), Y23 = λx, y. . ({x, y}, {x 6= y, y 6= nil, x 6= nil}) On the fourth iteration no new base pairs are produced — both Φ1,2 and Φ2,2 can be applied to the newly created base pair from the latest iteration, but the former yields an unsatisfiable Π and the latter reproduces the same base pair — so we have reached a fixed point, and base Φ (P, Q) = (Y13 , Y23 ). The next two lemmas formalise the fact that base Φ P (x) precisely characterises the satisfiability of P (x). Lemma 3.7 (Soundness). Given a base pair (V, Π) ∈ (base Φ Pi )(t), a stack s such that s |= Π, and a finite set W ⊆ Loc \ s(V ), there exists a heap h such that s, h |=Φ Pi t and dom(h) ∩ W = ∅. Proof. We proceed by fixed point induction on the definition of base Φ P. That is, we assume the lemma holds for a tuple of functions Y = (Y1 , . .S. , Yn ) ∈ σ1 × · S · · × σn , and we must show it also holds for ( j Ψ1,j (Y), . . . , j Ψn,j (Y)). Thus, assume (V, Π) ∈ Ψi,j (Y)(t) with s |= Π and s(V ) ∩ W = ∅. We require to find an h with s, h |= Pi t and dom(h) ∩ W = ∅. By assumption, there is a rule Φi,j of the form (IndRule) with (V, Π) ∈ Ψi,j (Y)(t). Therefore V = alloced (V 0 , x, Π0 )[t/x] and Π = (Π0 x)[t/x], where the following hold: V 0 = V1 ∪ · · · ∪ Vm ∪ {y1 , . . . , yk }, N 0 Π0 = V ∪ Π0 ∪ Π1 ∪ · · · ∪ Πm is satisfiable, ∀1 ≤ ` ≤ m. (V` , Π` ) ∈ Yj` (x` ). By the lemma assumption and usual substitution facts, we have that s[x 7→ s(t)] |= Π0 x and s[x 7→ s(t)](alloced (V 0 , x, Π0 )) ∩ W = ∅. Since Π0 is satisfiable, we can apply Lemma 3.4 to obtain s0 with s0 (x) = s[x 7→ s(t)](x) = s(t) and s0 |= Π0 . Furthermore, the lemma tells us that for any non-observable y ∈ V 0 , we have y∈ / W . Otherwise, if y ∈ V 0 is observable from x w.r.t. Π0 , there is an x ∈ x such that y and x are in the same Π0 -equivalence class. It follows that s0 (y) = s0 (x) = s[x 7→ s(t)](x) and, as x ∈ alloced (V 0 , x, Π0 ) but s[x 7→ s(t)](alloced (V 0 , x, Π0 )) ∩ W = ∅, it must be the case that s0 (y) ∈ / W . Thus, for all y ∈ V 0 0 0 0 we have s (y) ∈ / W , that is s (V ) ∩ W = ∅. We now show that there are heaps h1 , . . . , hm such that, for all 1 ≤ ` ≤ m, we have both s0 , h` |=Φ Pj` x` and dom(h` ) ∩ W` = ∅, where W` is defined as follows: [ [ 0 s (Vq ) . W` =def W ∪ s0 ({y1 , . . . , yk }) ∪ dom(hp ) ∪ p<` `<q≤m To do this, we inductively assume that we have constructed the chain of heaps (hp )1≤p<` , and show how to construct h` . Inductive construction of h` from (hp )1≤p<` : We claim and prove that s0 (V` ) ∩ W` = ∅. We have shown that s0 (V 0 ) ∩ W = ∅; since V` ⊆ V 0 , it follows that s0 (V` ) ∩ W = ∅. Next, let p < ` and note that the induction hypothesis implies dom(hp ) ∩ Wp = ∅, 0 which in turn implies S dom(hp ) ∩ s (V` ) = ∅ by definition of 0 Wp . Thus s (V` ) ∩ p<` dom(hp ) = ∅. Next, let q > ` and N 0 notice that s0 (V` ) ∩ s0 (Vq ) = ∅ because s0 |= V , which 0 0 guarantees that s S is injective on V ⊇ V` , Vq . It therefore follows that s0 (V` ) ∩ `<q≤m s0 (Vq ) = ∅. Also, for a similar reason, s0 (V` ) ∩ s0 ({y1 , . . . , yk }) = ∅. Now (V` , Π` ) ∈ Yj` (x` ), where s0 |= Π` and s0 (V` )∩W` = ∅, so by the main induction hypothesis (of the fixed point induction for the present lemma) there is a heap h` such that s0 , h` |=Φ Pj` x` and dom(h` ) ∩ W` = ∅. This completes the construction of h` . We continue with the main proof. Note that h1 ◦ . . . ◦ hm is defined because dom(h` ) ∩ W` = ∅ for all 1 ≤ ` ≤ m implies that dom(h1 ), . . . , dom(hm ) are all disjoint from each other. Now we define a heap h0 whose domain is s0 ({y1 , . . . , yk }) as follows: h0 (s0 (yi )) =def s0 (ui ) for each 1N ≤ i ≤ k. Note that h0 ◦ (h1 ◦ . . . ◦ hm ) is defined because s0 |= V 0 ensures that s0 is injective on {y1 , . . . , yk } ⊆ V 0 and dom(h` ) ∩ W` = ∅ ensures that dom(h` ) ∩ dom(h0 ) = ∅ for each 1 ≤ ` ≤ m. Thus, defining h =def h0 ◦ h1 ◦ . . . ◦ hm , we obtain: s0 , h |=Φ Π0 : y1 7→ u1 ∗ . . . ∗ yk 7→ uk ∗ Pj1 x1 ∗ . . . ∗ Pjm xm 0 which implies that s , h |=Φ Pi x (by applying the operator ϕi,j ). Thus, since s0 (x) = s(t), we obtain s, h |=Φ Pi t. We have dom(h) ∩ W = ∅ as required because dom(h` ) ∩ W ⊆ dom(h` ) ∩ W` = ∅, for each 1 ≤ ` ≤ m, and dom(h0 ) = s0 ({y1 , . . . , yk }) ⊆ s0 (V 0 ) while s0 (V 0 ) ∩ W = ∅. Lemma 3.8 (Completeness). If s, h |=Φ Pi t, there is a base pair (V, Π) ∈ (base Φ Pi )(t) such that s(V ) ⊆ dom(h) and s |= Π. Proof. We have that (s(t), h) ∈ JPi KΦ , and apply fixed point induction on the definition of JPKΦ . That is, we assume the lemma holds for X = (X S1 , . . . , Xn ) ∈ τS1 × . . . × τn and must show that it holds for ( j ϕ1,j (X), . . . , j ϕn,j (X)). Thus, assuming that (s(t), h) ∈ ϕi,j (X), we must then find a pair (V, Π) ∈ (base Φ Pi )(t) with s(V ) ⊆ dom(h) and s |= Π. By assumption, there is an inductive rule Φi,j of the form (IndRule) such that (s(t), h) ∈ ϕi,j (X). By construction this means that s(t) = s0 (x) for some stack s0 , and we have s0 , h |=X Π0 : y1 7→ u1 ∗ . . . ∗ yk 7→ uk ∗ Pj1 x1 ∗ . . . Pjm xm Thus s0 |= Π0 and h = h1 ◦ . . . ◦ hk ◦ h01 ◦ . . . ◦ h0m , where s0 , h` |=Φ y` 7→ u` for all 1 ≤ ` ≤ k, and (s0 (x` ), h0` ) ∈ Xj` for all 1 ≤ ` ≤ m. Then, by the induction hypothesis, for all 1 ≤ ` ≤ m there are pairs (V` , Π` ) ∈ (base Φ Pj` )(x` ), such that s0 (V` ) ⊆ dom(h0` ) and s0 |= Π` . Now we define [ V` ∪ {y1 , . . . , yk } . V =def 1≤`≤m As dom(h1 ), . . . , dom(hk ), dom(h01 ), . . . , dom(h0m ) are all disjoint, where dom(h` ) = {s0 (y` )} for each 1 ≤ ` ≤ kNand dom(h0` ) ⊇ s0 (V` ) for each 1 ≤ ` ≤ m, we have s0 |= V (i.e., h would be undefined if s0 were not injective on V ). Putting everything together, we have N s0 |= Π0 ∪ V ∪ Π1 ∪ · · · ∪ Πm and s0 (V ) ⊆ dom(h) . N Thus Π = Π0 ∪ V ∪ Π1 ∪ · · · ∪ Πm is satisfiable, and so (V ∩ x)[t/x], (Π x)[t/x] ∈ (base Φ Pi )(t) where the substitution [t/x] is well defined as x is a tuple of distinct variables. From the fact that s0 (x) = s(t), it also follows that s0 (x) = s[x 7→ s(t)](x). By Lemma 3.3, this gives us s[x 7→ s(t)] |= Π x and s[x 7→ s(t)](V ∩ x) ⊆ dom(h) . Thus, from usual facts about substitution, we obtain s |= (Π x)[t/x] and s(V ∩ x)[t/x] ⊆ dom(h) . Thus there exists (V, Π) ∈ (base Φ Pi )(t) such that s |= Π and s(V ) ⊆ dom(h) as required. We are now positioned to state our main decidability results. Theorem 3.9. A formula Pi t is satisfiable w.r.t. an inductive rule set Φ iff there is a base pair (V, Π) ∈ (base Φ Pi )(t) such that Π is satisfiable. Furthermore, for any given Φ, the fixed point computation of base Φ P terminates after a finite number of steps. Thus it is decidable whether a formula of the form Pi t is satisfiable w.r.t. Φ. Proof. Regarding correctness, the “if” direction is immediate from Lemma 3.7 by taking W = ∅; the “only if” direction follows from Lemma 3.8. For termination, each predicate Pi has a finite arity ai and, since each of the pairs (V, Π) ∈ base Φ Pi (t) may only use terms from the finitely many in t, the final total number of pairs in base Φ Pi (t) is bounded by a finite constant. All of the functions in the tuple base Φ P, mapping terms to base pairs, are thus finitely described in a straightforward way. Corollary 3.10. It is decidable whether an arbitrary symbolic heap is satisfiable w.r.t. an inductive rule set Φ. Proof. Let Π : F be a symbolic heap, and let Ψ be the inductive rule set Φ ∪ {Π : F ⇒ Q}, where Q is a new 0-ary predicate not occurring in Φ or Π : F . Clearly the symbolic heap Π : F is satisfiable w.r.t. Φ if and only if Q is satisfiable w.r.t. Ψ, which is a decidable problem according to Theorem 3.9. 4. Complexity In this section, we investigate the complexity of the satisfiability problem for inductive predicates in separation logic, which is addressed by the decision procedure in the previous section. Definition 4.1. We define the decision problem PREDSAT as having instances (Φ, P ) where Φ is an inductive rule set and P is a predicate defined in Φ. The pair (Φ, P ) is a yes-instance of PREDSAT if P x is satisfiable w.r.t. Φ, where x is an arbitrary tuple of distinct variables. For any k ∈ N, define k-PREDSAT to be PREDSAT restricted to the situation where all predicates in Φ have arity ≤ k. In the following, the length of the encoding of a mathematical object o (e.g., set, pair, formula, etc.) under some reasonable (non-unary) encoding scheme will be denoted by kok. Clearly, k(Φ, P )k = O(kΦk), as P can be represented by a pointer of dlog2 |Φ|e bits. Finally we fix B =def {>, ⊥}. Let α be the maximum arity of any predicates in Φ plus one; clearly, α = O(kΦk) as the maximum arity must be of the order of the length of the entire object. The length of a base pair is bounded by α + 2α2 = O(kΦk2 ) (size of the variable set plus the size of the longest pure formula), and the number of distinct base pairs for any predicate in Φ is bounded by 2 N =def 2α+2α . Finally L is the maximum number of predicate occurrences in any rule; as such, L = O(kΦk). Lemma 4.2. Let Φi,j be a rule in the form of (IndRule) and let T = hB1 , . . . , Bm i be a tuple of base pairs for the formulas Pj1 (x1 ), . . . , Pjm (xm ) respectively. Computing whether a base pair B 0 can be generated from T and Φi,j via Definition 3.5 takes time polynomial in kΦi,j k and kT k. Proof. Immediate from Definition 3.5 and the fact that satisfiability of conjunctions of pure formulas is in P (see, e.g., [3]). Definition 4.3. Let Φ be a set of inductive rules. A rule instance r = (B, i, j, r1 , . . . , rm ), for i, j, m ≥ 0 is such that: (a) the rule Φi,j has m predicates in its body; (b) B is a base pair for Pi ; (c) r1 , . . . , rm are rule instances; and (d) B can be produced by running the body of the loop in Fig. 1 using Φi,j and the base pairs associated with r1 , . . . , rm . We say that the rule instance r defined as above supports predicate Pi . In effect, a rule instance is a base pair together with the witnessing information for its production via our algorithm. Lemma 4.4. A predicate P defined in Φ is satisfiable iff there is a rule instance that supports P . Proof sketch. It is simple to modify the algorithm in Definition 3.5 so that instead of base pairs, it generates rule instances. Note that the rule instances within a rule instance r must be generated prior to r and thus can be represented by pointers, therefore not altering the space complexity of the algorithm. Lemma 4.5. k-PREDSAT is in NP, for any k ∈ N. Proof. We define a non-deterministic algorithm as follows. Let (Φ, P ) be the input instance. As stated in the beginning of this section, there can be up to N distinct base pairs for each predicate in Φ. Thus, for each predicate Pi in Φ we guess a set of up to N entries of − → −→ the form hB, i, j, E1 , . . . , Em i, where B is a base pair, i, j, m ≥ 0, − → and E` is a pointer to an entry for 1 ≤ ` ≤ m. Each entry requires O(kΦk3 ) time to generate: B takes O(α + 2α2 ) = O(kΦk2 ) time; pointers i, j take 2dlog2 |Φ|e = O(kΦk) time; pointers − → −→ E1 , . . . , Em take mdlog2 N e = O(L(α + 2α2 )) = O(kΦk3 ) time. By assumption, the arity of all predicates in Φ is bounded by a constant k, thus N is also constant. This means the total number of guesses is polynomial in the input size. We now check that this set of entries represents a rule instance supporting P . To do this we check: (a) that each entry is wellformed, i.e., that rule Φi,j involves m predicates, and that each − → E` points to an entry for predicate Pj` ; and (b) that each entry E can be generated through our algorithm using entries E1 , . . . , Em and rule Φi,j . Then, we check that the set of entries represents a directed acyclic graph when we view the pointers E` as edges. This will guarantee that there are no cycles and that, therefore, the set of entries represents a set of rule instances. These operations take polynomial time in N and |Φ| by Lemma 4.2 and standard facts from graph theory. Finally, we check for an entry (rule instance) supporting P . Since we can check the guessed entries in polynomial time, we can decide satisfiability in non-deterministic polynomial time. Lemma 4.6. PREDSAT is in EXPTIME. Proof. Each step of the algorithm in Definition 3.5 picks a rule from Φ and looks for a combination of base pairs that yields a new base pair. Thus it may go through up to N L combinations of base pairs. In the worst case all rules have to be scanned, checking up to |Φ|N L combinations. If no new base pair can be generated then the algorithm has reached a fixed point. As argued above, there can be at most |Φ|N distinct base pairs. In the worst case one pair is generated in each step. Thus |Φ|N steps are required with total time |Φ|N |Φ|N L p(kΦk) = O(2poly(kΦk) ) where p(kΦk) is the time taken to check a single combination of base pairs according to Lemma 4.2. Our lower bound results use standard facts about boolean circuits, with and without inputs. We make a few common simplifying assumptions: (a) inputs and constants are gates with no inputs and one output; (b) every circuit includes exactly two constants, > and ⊥; (c) there is one more kind of gate, the NAND gate (denoted by ↑); (d) gates are ordered so that if gate i has inputs l, r, then i > l and i > r; (e) inputs, >, ⊥ and NAND gates appear in this order; (f) the output of the maximal gate is the output of the circuit. We first define a mapping from circuits to inductive rule sets. Definition 4.7. Let C be a boolean circuit with n gates and k inputs. Thus, the constant gates are k + 1 and k + 2 (> and ⊥ respectively). Define a set of rules Ψ as follows. x 6= nil ⇒ T (x) x = nil ⇒ F (x) F (x) ∗ T (z) ⇒ N (x, y, z) Ψ =def F (y) ∗ T (z) ⇒ N (x, y, z) T (x) ∗ T (y) ∗ F (z) ⇒ N (x, y, z) Also define the set of rules ΦC as follows. ) ∗ F (xk+2 ) ∗ T (xk+1 ∗ni=k+3 N (xli , xri , xi ) ⇒ P (xn ) ΦC =def ∪Ψ P (x ) ∗ T (x ) ⇒ Q n n > P (xn ) ∗ F (xn ) ⇒ Q⊥ Above, li (resp. ri ) denotes the left (right) input of gate i. Clearly, kΦC k = O(kCk) and the maximum arity is 3. We will often have to go from boolean tuples to stacks and back. The following definition provides appropriate mappings. Definition 4.8. Fix some τ ∈ Val such that τ 6= nil . Let b ∈ B, B ∈ Bn and x ∈ Varn . Define functions sval : B → Val, bval : Val → B, stack sxB and boolean n-tuple Bsx as ( ( τ if b = > > if v 6= nil sval(b) =def bval(v) =def nil if b = ⊥ ⊥ if v = nil sxB (xi ) =def sval(Bi ) (Bsx )i =def bval(s(xi )) where i = 1, . . . , n. Theorem 4.9. k-PREDSAT is NP-complete for k ≥ 3. Proof. Membership in NP follows from Lemma 4.5. Hardness follows by reducing from CIRCUITSAT via Definition 4.7. We show that there is a boolean k-tuple B such that C(B) = > iff (ΦC , Q> ) ∈ k-PREDSAT, by proving that for any b there exists B such that C(B) = b iff (ΦC , Qb ) ∈ k-PREDSAT. (⇒) Suppose there exists B such that C(B) = b. Extend B to the n-tuple B0 such that for all i = 1, . . . , n, Bi0 is equal to the output of gate i. Clearly, B0 is well defined. Let sˆ =def sxB0 . It is easy to see that if b = > = Bn0 then sˆ |=Ψ T (xn ) and that if b = ⊥ then sˆ |=Ψ F (xn ). Thus in order to show that sˆ |=ΦC Qb it remains to show that sˆ |=ΦC P (xn ). If n ≤ k + 2 this is immediate as the output of C is either a constant or an input. If n is a NAND gate then we must show that for every i = k + 3, . . . , n, Bl0i ↑ Br0 i = Bi0 implies sˆ |=ΦC N (xli , xri , xi ), where li , ri are the inputs of gate i. This holds by the definitions of predicate N and stack sˆ. (⇐) Suppose there is a stack s such that s |=ΦC Qb . We assume ˆ =def Bsx . Set B as the kw.l.o.g. that s |=ΦC P (xn ) also. Let B ˆ We use induction to prove that for every i = 1, . . . , n, prefix of B. ˆi . The if the inputs are set to B then the output of gate i is B case where i = 1, . . . , k + 2 is trivial. If i = k + 3, . . . , n then it is a NAND gate and has inputs li , ri < i whose values ˆl , B ˆr . It is then simple to verify that if we know are equal to B i i ˆl ↑ B ˆr = B ˆi , by the s |=Ψ N (xli , xri , xi ) then it follows that B i i ˆ definitions of N and B. If b = > then by assumption s |=ΦC P (xn ) ∗ T (xn ), so ˆn = > and thus C(B) = >. The case b = ⊥ is similar. B For EXPTIME-hardness we will encode natural numbers as boolean tuples as well as formulas, as follows. Definition 4.10. We use iB to denote the boolean n-tuple encoding an integer 1 ≤ i ≤ 2n . Note that, for convenience, we set 1B = ⊥n and (2n )B = >n . In addition, we use a formula encoding in terms of the predicates T and F as seen above. ( T (x) if b = > frmb (x) =def F (x) if b = ⊥ boolB (x) =def frmB1 (x1 ) ∗ . . . ∗ frmBn (xn ) numi (x) =def bool(iB ) (x) The circuit value problem (CVP) has as instances input-free circuits. A circuit C is a yes-instance of CVP iff C() = >. The succinct circuit value problem (SCVP) has as instances input-free circuits generated by a pair of circuits as explained below. An instance of SCVP is a yes-instance iff for the generated circuit C, C() = >. Formally, an instance SC = (L, R) of SCVP consists of two circuits, each of 2n inputs. In the represented circuit C, for all i, j ∈ {1, . . . , 2n } such that L(iB , j B ) = > (resp. R(iB , j B ) = >), it holds that i > j, i is a NAND gate and its left (right) input is j. For simplicity we assume that circuits always use 2n gates and that their output is that of gate 2n . Also recall that for a k-input circuit, gates k +1 and k +2 are > and ⊥ respectively. Definition 4.11. Let C be a k-input circuit with n gates. Then, define ΦrC as follows, where Ψ is as in Definition 4.7. T (xk+1 ) ∗ F (xk+2 ) ∗ T (xn ) ∗ ΦrC =def Ψ ∪ ∗n i=k+3 N (xli , xri , xi ) ⇒ P (x1 , . . . , xk ) This definition turns the circuit C into a relation P over the variables representing the inputs of C. This will simplify presentation when we are only interested for inputs that make the output equal to >. In particular, the following lemma holds. Lemma 4.12. For any circuit C on k-inputs and any B ∈ Bk , C(B) = > iff s |=ΦrC P (x) ∗ boolB (x) for some stack s. Proof. Analogous to the proof of Theorem 4.9. Lemma 4.13. For any k-input circuit C and stacks s, s0 , if 0 Bsx = Bsx then s |=ΦrC P (x) if and only if s0 |=ΦrC P (x). 0 Proof. Observe that Bsx = Bsx entails that for any variable xi , s(xi ) = nil iff s0 (xi ) = nil . The result follows by verifying that satisfaction of predicates T, F, N by a stack s depends only on whether their arguments evaluate to nil or not. We now present the reduction from SCVP to PREDSAT. Definition 4.14. Let SC = (L, R) be an instance of SCVP. Let ΦrL , ΦrR be as in Definition 4.11 (we assume names PL , PR for the corresponding P predicate). Define rules (U1), (U2), (U3), and inductive rule sets X and ΦSC as follows. num1 (x) ∗ T (v) ⇒ U (x, v) num2 (x) ∗ F (v) ⇒ U (x, v) (U1) (U2) PL (x, l) ∗ PR (x, r) ∗ ⇒ U (x, v) U (l, w) ∗ U (r, z) ∗ N (w, z, v) (U3) X =def {(U1), (U2), (U3)} ∪ ΦrL ∪ ΦrR U (x, v) ∗ T (v) ⇒ Q> (x) U (x, v) ∗ F (v) ⇒ Q⊥ (x) ∪ X ΦSC =def num2n (x) ∗ Q> (x) ⇒ R Thus SC is mapped to the PREDSAT instance (ΦSC , R). Theorem 4.15. PREDSAT is EXPTIME-complete. Proof. By Lemma 4.6, PREDSAT is in EXPTIME. Hardness follows by exhibiting a reduction from SCVP (which is EXPTIMEcomplete [23]) via Definition 4.14. This follows from the stronger fact that for all i ∈ {1, . . . , 2n } and for any boolean b, the output of gate i is b iff there is a stack s such that s |=ΦSC numi (x) ∗ Qb (x). We use induction on i. (⇒) Assume i = 1. By assumption, gate 1 is the constant > thus its output is also b = >. Let B =def iB . Define the stack sˆ =def sxB [v 7→ sval(>)]. By applying (U1) we obtain that sˆ |=X U (x, v) and as sˆ |=ΦSC T (v) by construction, it must be that sˆ |=ΦSC numi (x) ∗ Q> (x). The case where i = 2 is similar. Suppose i > 2 and that the output of gate i is b. Gate i is a NAND gate thus there are l, r < i such that L(iB , lB ) = >, R(iB , rB ) = >, the values of gates l, r are c, d and c ↑ d = b. By the inductive hypothesis we obtain two stacks sl , sr with sl |=ΦSC numl (l) ∗ Qc (l) and sr |=ΦSC numr (r) ∗ Qd (r). In particular, regardless of the values c, d take, sl |=ΦSC U (l, w) and sr |=ΦSC U (r, z) (we set sl (w) = sl (v) and sr (z) = sr (v) w.l.o.g.). By Lemma 4.12, there exist two stacks s0l , s0r such that (a) Solved in (b) Solved in Vars ≤ 1s ≤ 30 s Sat. Rules ≤ 1s ≤ 30 s Sat. 20 30 40 50 60 70 80 94 88 86 89 91 85 89 99 96 95 98 97 97 97 9 17 20 37 28 46 41 2×2 3×2 2×3 3×3 4×3 3×4 4×4 100 100 91 89 86 57 47 100 100 98 98 96 81 75 34 19 32 37 31 24 23 Arity ≤ 1s ≤ 30 s Sat. Recs ≤ 1s ≤ 30 s Sat. 1 2 3 4 5 99 96 89 80 72 100 100 98 90 80 22 24 37 30 24 0 1 2 3 4 100 100 89 88 85 100 100 98 96 93 21 42 37 13 9 s0l |=ΦrL PL (x, l) ∗ numi (x) ∗ numl (l) s0r |=ΦrR PR (x, r) ∗ numi (x) ∗ numr (r) where Lemma 4.13 lets us assume s0l (x) = s0r (x), s0l (l) = sl (l) and s0r (r) = sr (r). Thus there exists sˆ such that sˆ(w) = sl (w), sˆ(z) = sr (z) and sˆ |=ΦSC PL (x, l) ∗ PR (x, r) ∗ U (l, w) ∗ U (r, z) ∗ N (w, z, v) and by (U3), sˆ |= U (x, v). A case analysis on the definition of N allows us to conclude that sˆ |=ΦSC numi (x) ∗ Qb (x). (c) (⇐) Let s be a stack such that s |=ΦSC numi (x) ∗ Qb (x). Thus s |=ΦSC U (x, v). If i ∈ {1, 2} then gate i is a constant and the result follows from (U1), (U2). If i > 2 then gate i is a NAND gate and rule (U3) applies: s |=ΦSC PL (x, l) ∗ PR (x, r) ∗ U (l, w) ∗ U (r, z) ∗ N (w, z, v). Let l, r ∈ {1, . . . , 2n } be such that lB = Bsl and rB = Bsr . By Lemma 4.12 we can conclude that L(iB , lB ) = > and R(iB , rB ) = >, meaning that l, r are the inputs of gate i. As such, there exist booleans c, d such that s |=ΦSC Qc (l) ∗ Qd (r) and by the inductive hypothesis we obtain that the outputs of gates l, r are c, d respectively. It remains to show that c ↑ d = b which follows by a case analysis on the definition of N . The worst case can be exhibited easily through counting. Proposition 4.16. There is a family of predicates Φn of size O(n) such that the algorithm in Defn. 3.5 runs in Ω(2n ) time and space. Proof. It should be clear that circuits can be rendered as predicates in linear space. In particular, the successor relation over two n-bit numbers can be encoded as a predicate succ(x, y), for n-variable tuples x, y. Consider the set of predicates Φn . num1 (y) ⇒ Q(y) succ(x, y) ∗ Q(x) ⇒ Q(y) Φn =def num(2n ) (x) ∗ Q(x) ⇒ P Given (Φn , P ), the algorithm starts with the base case for Q and counts from 1 to 2n , creating a base pair encoding each number in between. This will happen irrespective of which strategy is used to select rules or base pairs for instantiation. Clearly, the algorithm will take Ω(2n ) time. 5. Implementation and experiments We implemented our decision procedure as a straightforward rendition of Definition 3.5 (in about 1000 lines of OCaml code) in the theorem proving framework C YCLIST [11], which provides support for logics with inductive predicates. Here we report on the performance of this algorithm on various data sets. The code, the tool and test files are available online at [1]. 5.1 Benchmarks on handwritten predicates First, we collected a set of 17 standard predicates (defined by 36 rules) from the separation logic literature, defining data structures such as singly- or doubly-linked list segments, possibly-cyclic lists, trees and tree segments. Our decision procedure takes just 4 ms to prove satisfiability of this set of definitions. This is rather to be expected, since all predicates in this test set are easily seen to be satisfiable. In order to exhibit the worst-case behaviour of our algorithm, we also tested our tool on the family Φn of predicates given in Solved in (d) Solved in Figure 2. Synthetic benchmark performance of our algorithm. Proposition 4.16, using a binary adder implementation of the successor relation. Runtimes, as expected, are exponential in n: cases with n ≤ 4 are solved in a fraction of a second, the case n = 5 is solved in about half a minute, n = 6 takes almost 16 minutes, and n = 7 times out after 40 minutes. 5.2 Benchmarks on automatically abduced predicates Next, we tested our algorithm on a large collection of predicates generated automatically by the C ABER tool, which attempts to abduce inductively defined safety and/or termination preconditions in our logical fragment for pointer programs [10]. We recorded all candidate preconditions generated by C ABER over 29 test programs, including back-tracking attempts. This produced 45 945 syntactically unique inductive rule sets, defining from 1–37 predicates with up to 11 parameters and two recursive invocations each. The majority of these definition sets (94%) had no more than 20 predicates; sets with 19 predicates were the most numerous (15%). We found that our algorithm terminates in less than 50 ms on all tests in this suite, and most definition sets (83%) were satisfiable. We believe this is probably due to the relatively simple recursive structure of the predicates produced by C ABER. 5.3 Synthetic benchmarks To evaluate the scalability of our procedure, we generated test cases drawn from a random distribution with parameters: • Vars: the number of variables in Var; • Rules = Preds × Cases: the number of predicates and induc- tive rules for each predicate; • Arity: the arity of all predicates; • Eqs, Neqs, Points, and Recs: the average numbers of equal- ities, disequalities, points-to literals, and recursive predicate calls, respectively, in each rule. Each instance consists of Rules = Preds × Cases independently generated inductive definitions, with all predicates of the same Arity. On the rule body, the number for each kind of literal is drawn from a Poisson distribution where the parameter λ is set to, respectively, Eqs, Neqs, Points, and Recs. This yields a mix of short and long rule bodies with a specified average length. Furthermore, to have on average one base case for the rule system, with probability p = 1/Rules all the recursive calls in the body of a rule are discarded. Figure 2 reports our algorithm’s performance on instances drawn from this distribution. Each row collects the results of 100 instances randomly generated with various parameter values; the second and third columns report the number of tests solved in under 1 and 30 seconds, while the last one shows the number of solved instances found to be satisfiable. Each of the four sub-tables shows how the statistics vary as one parameter changes while all the rest remain fixed. Although most cases are fairly easy to solve, a few hard instances consistently show up on all parameter settings. For example, with parameters Vars = 50, Rules = 3×3, Arity = 3, and all Eqs, Neqs, Points, and Recs set to 2 (that is the bold line repeated on all four tables), we find that two very hard instances remain unsolved after the 30 s timeout. 6. Related work Here we survey the main categories of work related to the contribution of this paper. 6.1 Satisfiability in separation logic with inductive predicates Recently, interesting progress has been made on satisfiability and entailment problems in various fragments of separation logic with user-defined inductive predicates as considered here (see Section 2). In particular, Iosif et al. [20] propose a sub-fragment of our setting, imposing significant syntactic restrictions on the inductive definitions to enforce bounded treewidth for all models of a predicate. Here the treewidth of a heap h is determined by a corresponding graph structure. These restrictions allow them to use a reduction to monadic second-order logic (MSO) for their proof that both satisfiability and entailment are decidable in their fragment of separation logic with inductive definitions. However, these syntactic restrictions disallow many natural inductive predicates; in particular, predicates describing structures with dangling data pointers, such as list or tree segments with extra arbitrary data fields, or structures where potentially no memory is allocated.1 In this paper, we only consider satisfiability, not entailment (which is undecidable [2]), but we are not restricted to boundedtreewidth predicates. In addition, we provide a direct decision procedure for satisfiability (as opposed to a reduction proof of decidability) and contribute an analysis of the complexity of satisfiability checking for our fragment. Considerable research effort has also been expended on the symbolic heap fragment of separation logic with a list segment predicate only. Berdine et al. [3] provided the first decidability result for satisfiability and entailment in this fragment, with a polynomial time procedure given later by Cook et al. [15]. Piskac et al. recently presented another decision procedure, which also works for structures such as sorted list segments and doubly linked lists, based on translating entailments to an intermediate logic that can be handled by an SMT solver [24]. (In very recent work [25], Piskac et al. extended their approach to support also tree-shaped data structures.) Finally, Navarro P´erez and Rybalchenko [22] provided an SMT encoding for satisfiability and entailment in another extension of the fragment allowing pure formulas from arbitrary SMT theories, rather than simple (dis)equalities. 6.2 Satisfiability in other logics with inductive definitions The evaluation of Datalog queries was shown to be decidable by Shmueli [27] and EXPTIME-complete (see e.g. [16, Theorem 4.5]). However, the interaction between spatial conjunction (∗), allocation (7→) and recursion makes a direct translation to Datalog impractical because it imposes a global constraint; at the same time we found that reducing from Datalog for our lower bounds is possible but no simpler than our circuit-based method. More recently, Hoder et al. [19] describe a Datalog-based engine, µZ, for the fixed point computation of inductive definitions. In contrast to our approach, they compute concrete fixed points based on explicit underlying ground facts (i.e., they focus on model checking, as opposed to satisfiability checking). More generally, there has been some interest from the program analysis and verification community in the satisfiability of Horn and Horn-like clauses. Bjørner et al. [7] advocate such clauses as an interchange format for software model checking tools, while Grebenshchikov et al. [18] describe an abstraction-based procedure for finding models and checking satisfiability of Horn-like clauses in the context of program analysis. 6.3 Separation logic tools with general inductive predicates Several analysis tools based on separation logic allow the user to provide their own inductive definitions for spatial predicates. We have already mentioned in our evaluation (Section 5) the theorem prover C YCLIST [11], which treats separation logic with user-defined inductive predicates, and the related abductive prover C ABER [10], which automatically infers inductive predicate definitions as safety/termination preconditions for while programs. Another such tool is T HOR [21], which proves memory safety and generates sound arithmetic abstractions of heap programs (w.r.t. safety and termination). In T HOR the specification and predicate definitions must be entered manually. User-defined inductive predicates are also employed in H IP /S LEEK [14], a combined theorem prover and verification system for a C-like language. Finally, the shape analysis in [13] infers inductive definitions based on “structural invariant checkers” provided by the user. 7. Conclusion and future work The decidability status of satisfiability in the symbolic heap fragment of separation logic with general inductive predicates has stood open for some time. Following the recent achievement of a partial positive answer to this question in [20], here we resolve the general case affirmatively. Our decidability proof has the advantage of being constructive: we give a decision procedure for checking the satisfiability of inductively defined predicates and of individual rules defining those predicates. We show that our satisfiability problem is EXPTIME-complete in the general case, and that it is still NP-complete when the inductive predicates are restricted to at most k ≥ 3 arguments. Despite these high complexities, our experiments indicate that, for predicate definitions arising in practice, our prototype implementation is typically able to solve the decision problem in a matter of milliseconds. This opens up a number of interesting potential applications in the automatic verification of programs based on our fragment of separation logic (which could be used, e.g., to consider heap-based programs employing arbitrary data structures, rather than just lists): The consistency of inductive predicates defined by first-order Horn clauses has been widely studied in different contexts. One wellknown application of such clausal definitions is Datalog, a rulebased query language for relational databases with ties to logic programming. Datalog rules roughly correspond to our inductive rules where the spatial component of rule bodies is always emp. • First, automatic verification or shape analysis based on sepa- 1 For • Second, although our decision procedure for satisfiability can- further discussion of the limitations of this fragment of separation logic we refer to [20]. ration logic (cf. [4, 5, 12]) typically employs symbolic states based on disjunctions of symbolic heaps. Our algorithm could thus be used to quickly eliminate unsatisfiable disjuncts from symbolic states; it seems plausible that this might yield nontrivial reductions in the time and space costs of such analyses. not be used to decide the validity of entailments (which is im- possible in general), it does nevertheless provide a quick partial method for proving or disproving such entailments. On the one hand, any entailment F ` G with an unsatisfiable antecedent F is trivially valid. On the other hand, F ` G must be invalid if the base pairs for F and G imply the existence of a model satisfying F but not G. To illustrate this point, consider the usual “list segment” predicate of separation logic, defined by x = y : emp ⇒ ls(x, y) x 7→ z ∗ ls(z, y) ⇒ ls(x, y) Now, consider the (invalid) entailment ls(x, y) ` ls(y, x). Computing the base pairs for both sides yields (base ls)(x, y) = {(∅, {x = y}), ({x}, ∅)} (base ls)(y, x) = {(∅, {y = x}), ({y}, ∅)} The second base pair for ls(x, y) implies the existence of a model for ls(x, y) in which x is allocated and y is not, and hence x 6= y in this model. However, the base pairs for ls(y, x) tell us that y must be allocated in any model of ls(y, x) where x 6= y. That is, there is a model of ls(x, y) that is not a model of ls(y, x). We believe that this sort of reasoning should be quite straightforward to automate. • Third, our satisfiability procedure can be used to check the san- ity of, and/or remove unsatisfiable clauses from, the definitions of inductive predicates either written by programmers, or inferred automatically (cf. [10]). • Finally, beyond deciding the satisfiability of inductive predi- cates, the set of base pairs computed by our procedure also provides a useful partition of the space to search for models. While Gherghina et al. [17] have shown that a manual case analysis of inductive definitions can guide proof techniques and improve their efficiency; our decision procedure could automate the case analysis required to do so. Taking a different direction for future work, one could investigate whether our techniques for deciding satisfiability extend to more general variants of separation logic, where general inductive predicates are still allowed, but the general format of formulas is less restricted. Possible candidates for such extensions include: higher-order separation logic [6]; the fragment in which formulas may contain pure assertions beyond (dis)equalities [22]; and separation logic with fractional permissions [8]. [6] B. Biering, L. Birkedal, and N. Torp-Smith. BI-hyperdoctrines, higher-order separation logic, and abstraction. ACM TOPLAS, 29(5), 2007. [7] N. Bjørner, K. McMillan, and A. Rybalchenko. Program verification as satisfiability modulo theories. In SMT’12, pages 3–11, 2012. [8] R. Bornat, C. Calcagno, P. W. O’Hearn, and M. J. Parkinson. Permission accounting in separation logic. In POPL’05, pages 259–270, 2005. [9] J. Brotherston. Formalised inductive reasoning in the logic of bunched implications. In SAS’07, volume 4634 of LNCS, pages 87–103, 2007. [10] J. Brotherston and N. Gorogiannis. Cyclic abduction of inductively defined safety and termination preconditions. Technical Report RN/13/14, University College London, 2013. [11] J. Brotherston, N. Gorogiannis, and R. L. Petersen. A generic cyclic theorem prover. In APLAS’12, volume 7705 of LNCS, pages 350–367, 2012. [12] C. Calcagno, D. Distefano, P. W. O’Hearn, and H. Yang. Compositional shape analysis by means of bi-abduction. J. of the ACM, 58(6): 26, 2011. [13] B.-Y. E. Chang, X. Rival, and G. Necula. Shape analysis with structural invariant checkers. In SAS’07, volume 4634 of LNCS, pages 384– 401, 2007. [14] W.-N. Chin, C. David, H. H. Nguyen, and S. Qin. Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Science of Computer Programming, 77(9):1006– 1036, 2012. [15] B. Cook, C. Haase, J. Ouaknine, M. J. Parkinson, and J. Worrell. Tractable reasoning in a fragment of separation logic. In CONCUR’11, volume 6901 of LNCS, pages 235–249, 2011. [16] E. Dantsin, T. Eiter, G. Gottlob, and A. Voronkov. Complexity and expressive power of logic programming. ACM Comput. Surv., 33(3): 374–425, 2001. [17] C. Gherghina, C. David, S. Qin, and W.-N. Chin. Structured specifications for better verification of heap-manipulating programs. In FM’11, volume 6664 of LNCS, pages 386–401, 2011. [18] S. Grebenshchikov, N. P. Lopes, C. Popeea, and A. Rybalchenko. Synthesizing software verifiers from proof rules. In PLDI’12, pages 405–416, 2012. [19] K. Hoder, N. Bjørner, and L. de Moura. µZ– an efficient engine for fixed points with constraints. In CAV’11, volume 6806 of LNCS, pages 457–462, 2011. [20] R. Iosif, A. Rogalewicz, and J. Simacek. The tree width of separation logic with recursive definitions. In CADE’13, volume 7898 of LNAI, pages 21–38, 2013. Acknowledgements. We wish to thank the anonymous reviewers for their valuable comments, which have helped us greatly in improving the presentation of the paper. [21] S. Magill, M.-H. Tsai, P. Lee, and Y.-K. Tsay. Automatic numeric abstractions for heap-manipulating programs. In POPL’10, pages 211–222, 2010. References [22] J. A. Navarro P´erez and A. Rybalchenko. Separation logic modulo theories. In APLAS’13, volume 8301 of LNCS, pages 90–106, 2013. [23] C. H. Papadimitriou and M. Yannakakis. A note on succinct representations of graphs. Inf. Control, 71(3):181–185, Dec. 1986. [1] Satisfiability checker for separation logic with inductive definitions. https://github.com/ngorogiannis/cyclist/releases/ tag/CSL-LICS14. [2] T. Antonopoulos, N. Gorogiannis, C. Haase, M. Kanovich, and J. Ouaknine. Foundations for decision problems in separation logic with general inductive predicates. In FoSSaCS’14, volume 8412 of LNCS, pages 411–425, 2014. [3] J. Berdine, C. Calcagno, and P. W. O’Hearn. A decidable fragment of separation logic. In FSTTCS’04, volume 3328 of LNCS, pages 97– 109, 2004. [4] J. Berdine, C. Calcagno, B. Cook, D. Distefano, P. W. O’Hearn, T. Wies, and H. Yang. Shape analysis for composite data structures. In CAV’07, volume 4590 of LNCS, pages 178–192, 2007. [5] J. Berdine, B. Cook, and S. Ishtiaq. SLAyer: Memory safety for systems-level code. In CAV’11, volume 6806 of LNCS, pages 178– 183, 2011. [24] R. Piskac, T. Wies, and D. Zufferey. Automating separation logic using SMT. In CAV’13, volume 8044 of LNCS, pages 773–789, 2013. [25] R. Piskac, T. Wies, and D. Zufferey. Enabling automated reasoning about separation logic of trees with data. In CAV’14, 2014. To appear. [26] J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS’02, pages 55–74, 2002. [27] O. Shmueli. Decidability and expressiveness aspects of logic queries. In PODS’87, pages 237–249, 1987. [28] H. Yang, O. Lee, J. Berdine, C. Calcagno, B. Cook, D. Distefano, and P. O’Hearn. Scalable shape analysis for systems code. In CAV’08, volume 5123 of LNCS, pages 385–398, 2008.

© Copyright 2018 ExploreDoc