An Entailment Checker for Separation Logic with Inductive Definitions Electronic Communications of the EASST Volume 076 (2019) Automated Verification of Critical Systems 2018 (AVoCS 2018) An Entailment Checker for Separation Logic with Inductive Definitions Radu Iosif and Cristina Serban 21 pages Guest Editors: David Pichardie, Mihaela Sighireanu ECEASST Home Page: http://www.easst.org/eceasst/ ISSN 1863-2122 http://www.easst.org/eceasst/ ECEASST An Entailment Checker for Separation Logic with Inductive Definitions Radu Iosif and Cristina Serban CNRS/VERIMAG/Université Grenoble Alpes Radu.Iosif@univ-grenoble-alpes.fr, Cristina.Serban@univ-grenoble-alpes.fr Abstract: In this paper, we present Inductor, a checker for entailments between mu- tually recursive predicates, whose inductive definitions contain ground constraints belonging to the quantifier-free fragment of Separation Logic. Our tool implements a proof-search method for a cyclic proof system that we have shown to be sound and complete, under certain semantic restrictions involving the set of constraints in a given inductive system. Dedicated decision procedures from the DPLL(T )-based SMT solver CVC4 are used to establish the satisfiability of Separation Logic formu- lae. Given inductive predicate definitions, an entailment query, and a proof-search strategy, Inductor uses a compact tree structure to explore all derivations enabled by the strategy. A successful result is accompanied by a proof, while an unsuccessful one is supported by a counterexample. Keywords: cyclic proofs, inductive definitions, infinite descent, separation logic 1 Introduction Inductive definitions play an important role in computing, being an essential component of pro- gramming languages, databases, automated reasoning and program verification systems. The main advantage of using inductive definitions is the ability of recursively reasoning about sets of logical objects. The semantics of these definitions is defined in terms of least fixed points of higher-order functions on assignments mapping predicates to sets of models. A natural problem is the entailment, that asks whether the least solution of one predicate is included in the least solution of another. Examples of entailments are language inclusion between finite-state (tree) automata, context-free grammars or verification conditions generated by shape analysis tools using specifications of recursive data structures as contracts of program correctness. The interest for automatic proof generation is two-fold. On one hand, machine-checkable proofs are certificates for the correctness of the answer given by an automated checker, that in- crease our trust in the reliability of a particular implementation [SOR+13]. On the other hand, the existence of a sound and complete proof system provides a (theoretical) decision procedure for the entailment problem. Assuming that the sets of models and derivations are both recur- sively enumerable, one can interleave the enumeration of counter-models with the enumeration of derivations; if the entailment holds one finds a finite proof (provided that the proof system is complete), or a finite counterexample, otherwise. Moreover, proof generation can be made ef- fective by providing suitable strategies that limit the possibilities of applying the inference rules and guide the search towards finding a proof or a counterexample. 1 / 21 Volume 076 (2019) mailto:Radu.Iosif@univ-grenoble-alpes.fr mailto:Cristina.Serban@univ-grenoble-alpes.fr An Entailment Checker for Separation Logic with Inductive Definitions In this paper we consider inductive systems with constraints written in Separation Logic [Rey02] with the classical (strict) interpretation of spatial atoms. We introduce a set of inference rules tailored for proving inductive entailments in Separation Logic, which have been shown to be sound [IS17] under a ranking assumption for the constraints of the inductive definitions. Completeness is assured under three additional restrictions and only for a particular interpreta- tion of the least solution of the inductive system, taking into account the coverage trees of the heap generated by the inductive definitions. We then describe Inductor [Ser17], a prototype im- plementation for the more general proof search algorithm given in [IS17] and reprised in §2.4, and discuss several case studies involving both valid and invalid entailments. Related Work The problem of entailment in Separation Logic with inductive definitions has been approached by other solvers. The generic cyclic proof framework CYCLIST [BGP12] has an instantiation for this fragment and allows for the discovery of inductive arguments during proof construction. CYCLIST builds proofs in which infinite traces can be cut by induction when they satisfy a global trace condition requiring them to visit infinitely many progress points. SLEEK [CDNQ12] and SPEN [ELS17, ESW15] both provide methods of proving entailments by relying on lemmas that relate the inductive definitions. However, SLEEK utilizes a database of user- provided lemmas, while SPEN is able to automatically discover and synthesize concatenation lemmas. Chu et al. [CJT15] propose a proof system that extends the basic cyclic proof method with a cut rule type that uses previously encountered sequents as inductive hypotheses and applies them by matching and replacing the left with the right-hand side of such a hypothesis. This method can prove entailments between predicates whose coverage trees differ and only soundness is guaranteed. An automata-based decision procedure that also tackles such entailments is given in [IRV14]. This method translates the entailment problem to a language inclusion between tree automata and uses a closure operation on automata to match divergent predicates. Unlike proof search, this method uses existing tree automata inclusion algorithms, which do not produce proof witnesses. 2 Cyclic Proofs for Inductive Entailments in Separation Logic 2.1 Preliminaries For two integers 0 ≤ i ≤ j, we denote by [i, j] the set {i,i + 1,..., j} and by [i] the set [1,i], where [0] = /0. ||S|| denotes the cardinality of the finite set S. We consider a signature Σ = (Σs,Σf), where Σs is a set of sort symbols and Σf is a set of function symbols. For the purpose of this paper, we restrict the signature such that Σs = {Loc,Bool} and Σ f contains only equality, the constant symbol nil of sort Loc and the boolean constants > and ⊥. Let Var be a countable set of first order variables, each xσ ∈ Var having a sort σ. We write x,y,... for both sets and ordered tuples of variables and, for brevity, we use ∈, ∪, ∩, ⊆ on tuples such that x ∈ x iff x occurs in x, x∪y ={x | x ∈ x or x ∈ y}, x∩y ={x | x ∈ x and x ∈ y}, x ⊆ y iff x ∈ y for any x ∈ x. A term t σ is either a constant or a variable of sort σ ∈ Σs. Separation Logic (SL) formulae are generated by the following syntax: AVoCS 2018 2 / 21 ECEASST φ ::=>|⊥| t σ1 ≈ t σ 2 |emp | x Loc 7→ (t Loc1 ,...,t Loc k ) | φ1 ∗φ2 |¬φ1 | φ1 ∧φ2 | φ1 ∨φ2 | ∃x.φ1 | ∀x.φ1 where k > 0 is a fixed constant. Given a set of formulae F = {φ1,...,φn}, we write ∗F for φ1 ∗ ...∗φn, which is equivalent to emp if F = /0. For a formula φ (set of formulae F ), FV(φ) ( ⋃ φ∈F FV(φ)) is the set of variables not occurring under a quantifier scope, and φ(x) (F(x)) means that, for every x ∈ x, we have x ∈ FV(φ) (x ∈ ⋃ φ∈F FV(φ)). Given sets of variables x and y, a flat substitution θ : x → y is a mapping of the variables in x to variables in y. We denote by xθ = {θ(x) | x ∈ x} its image under the substitution θ. For a formula φ(x), φθ is the formula obtained by replacing each occurrence of x ∈ x with the term θ(x). Observe that θ is always a surjective mapping between FV(φ) and FV(φθ). We lift this notation to sets as F θ ={φθ | φ ∈ F}. We fix an interpretation I such that I (>) = true, I (⊥) = false, I (Loc) is a countably infinite set L, and I (nil) = `nil is a fixed element of L. A valuation ν maps each variable xBool to true or false and each variable yLoc to an element of L. Given a term t σ, by writing t I ν we mean either I (t) (if t is a constant symbol) or ν(t) (if t is a variable). A heap is a finite partial mapping h : L ⇀fin Lk associating locations with k-tuples of locations. We denote by dom(h) the set of locations on which h is defined, by img(h) the set of locations occurring in the range of h, and by Heaps the set of heaps. Two heaps h1 and h2 are disjoint if dom(h1)∩dom(h2) = /0. In this case, h1 ]h2 denotes their union, which is undefined if h1 and h2 are not disjoint. Given a valuation ν and a heap h, the semantics of SL formulae is defined as: ν,h |=sl t1 ≈ t2 ⇔ (t1)Iν = (t2)Iν ν,h |=sl emp ⇔ h = /0 ν,h |=sl x 7→ (t1,...,tk) ⇔ h ={ 〈 ν(x),((t1)Iν,...,(tk) I ν ) 〉 } ν,h |=sl φ1 ∗φ2 ⇔ ∃h1,h2 ∈Heaps.h = h1 ]h2 and ν,hi |=sl φi,i ∈ [2] The semantics of boolean and first order connectives is the usual one, omitted for brevity. Given SL formulae φ and ψ, we say that φ entails ψ (i.e. φ |=sl ψ) iff ν,h |=sl φ implies ν,h |=sl ψ, for any valuation ν and heap h. 2.2 Inductive Systems of Predicates in Separation Logic Let Pred be a countable set of predicates, each pσ1...σn ∈ Pred having an associated tuple of argument sorts. Given a tuple of terms (t σ11 ,...,t σn n ), we call p(t1,...,tn) a predicate atom. A predicate rule is a pair 〈{φ(x,x1,...,xn),q1(x1),...,qn(xn)}, p(x)〉, where x,x1,...,xn are tuples whose corresponding sets of variables are pairwise disjoint, φ is a formula, called the constraint, p(x) is a predicate atom called the goal and q1(x1),...,qn(xn) are predicate atoms called sub- goals. The variables x are the goal variables, whereas ⋃n i=1 xi are the subgoal variables. An inductive system S (system, for short) is a finite set of predicate rules. In this paper, we con- sider inductive systems whose constraints belong to the SL fragment described in §2.1. We as- sume w.l.o.g. that each predicate p∈Pred is the goal of at least one rule of S and that there are no goals with the same predicate and different goal variables. We write p(x) :=S R1 | ... | Rm when {〈R1, p(x)〉,...,〈Rm, p(x)〉} is the set of all predicate rules in S with goal p(x). We consider only quantifier-free constraints, in which no disjunction occurs positively and no conjunction occurs negatively, and assume that the set of constraints of a system has a decidable satisfiability 3 / 21 Volume 076 (2019) An Entailment Checker for Separation Logic with Inductive Definitions problem. Disjunctions can be eliminated by splitting 〈{φ1 ∨ ...∨φm,q1(x1),...,qn(xn)}, p(x)〉 into m rules 〈{φi,q1(x1),...,qn(xn)}, p(x)〉, one for each i ∈ [m]. Example 1 Consider the SL inductive system SAB consisting of the predicate rules: p(x) :=SAB x 7→ (x1,x2), p1(x1), p2(x2) q(x) :=SAB x 7→ (x1,x2),q1(x1),q2(x2) | x 7→ (x1,x2),q2(x1),q1(x2) p1(x) :=SAB x 7→ (x1,nil), p1(x1) | x 7→ (nil,x) q1(x) :=SAB x 7→ (x1,nil),q1(x1) | x 7→ (nil,x) p2(x) :=SAB x 7→ (x1,nil), p2(x1) | x 7→ (nil,nil) q2(x) :=SAB x 7→ (x1,nil),q2(x1) | x 7→ (nil,nil) Broadly speaking, the predicates define binary trees in which the root node points to two lists and one leaf is not nil, but its position differs in each definition. Given an SL inductive system S , an assignment X maps each predicate pσ1...σn ∈ Pred to a set X (p) ⊆ Ln ×Heaps. For a set F = {φ,q1(x1),...,qn(xn)}, where φ is an SL formula and q1(x1),...,qn(xn) are predicate atoms, we define X (∗F) = {(ν,h0 ]⊎mi=1 hi) | ν,h0 |=sl φ,(ν(xi),hi)∈ X (qi),∀i ∈ [m]}. Then S induces a function FslS (X ) on assignments, which maps each predicate p ∈ Pred into the set ⋃m i=1{(ν(x),h) | (ν,h) ∈ X (∗Ri)}, where p(x) :=S R1 | ... | Rm. A solution of S is an assignment X such that FslS (X )⊆ X , where inclusion between assignments is defined pointwise. It can be shown that the set of all assignments, together with the ⊆ relation, is a complete lattice and that FIS is monotone. Therefore, by the Knaster-Tarski theorem, µS sl = ⋂ {X | FIS (X ) ⊆ X} is the least fixed point of FslS and the least solution of S . Example 2 Considering the SAB inductive system from Example 1, the set µS slAB(q) consists of trees of both following forms, where n ≥ 1 and m ≥ 1: x x11 ... nil x12 ... nil xn1 nil nil xn1 xm2 nil nil nil x x11 ... nil x12 ... nil xn1 nil nil nil xm2 nil nil xm2 while the set µS slAB(p) contains trees of the first above form, but not the second. We are concerned with the following entailment problem: given an inductive system S and predicates pσ1...σm , qσ1...σm1 ,...,q σ1...σm n , is it true that µS sl(p) ⊆ ⋃n i=1 µS sl(qi)? We denote entail- ment problems as p |=slS q1,...,qn. Example 3 Given the least solution of the SAB inductive system from Example 2, observe that the entailment p |=slSAB q holds, while q |= sl SAB p does not. 2.3 Tree Automata Inclusion as Cyclic Proof Search We consider top-down nondeterministic finite tree automata (NFTA), where a tree over a ranked alphabet F is either a symbol a ∈ F of rank (or arity) 0, or f (t1,...,tn) such that f ∈ F is of rank n and t1,...,tn are, in turn, trees. The actions of an NFTA are described by transition rules AVoCS 2018 4 / 21 ECEASST q f−→ (q1,...,qn), with the following meaning: if the automaton is in state q and the input is a tree f (t1,...,tn), then it moves simultaneously on each ti changing its state to qi, for all i ∈ [n]. A tree is accepted by an automaton A if each leaf can be eventually read by a transition of the form q a−→ (). The language of a state q in A, denoted L(A,q), is the set of trees accepted by A starting with state q. An NFTA can be naturally viewed as an inductive system, where predicates represent states and predicate rules are obtained directly from transition rules. For instance, q f−→ (q1,...,qn) can be written as 〈{x ≈ f (x1,...,xn), q1(x1),...,qn(xn)},q(x)〉, where variables range over trees and the function symbols are interpreted in the canonical (Herbrand) sense. To further obtain an SL inductive system, an encoding of the constraints in each predicate rule using SL connectives is required. Example 4 The SL inductive system SAB from Example 1 encodes two NFTA A and B with states {p, p1, p2} and {q,q1,q2}, respectively, where p and q are initial states, using the alphabet { f (,),g(),a,b} and having the transition sets {p f → (p1, p2), p1 g → p1, p1 a→ (), p2 g → p2, p2 b→ ()} and {q f → (q1,q2),q f → (q2,q1),q1 g → q1,q1 a→ (),q2 g → q2, q2 b→ ()}, respectively. We en- coded the binary symbol f as x 7→ (x1,x2), the unary symbol g as x 7→ (x1,nil), and the constant symbols a and b as x 7→ (nil,x) and x 7→ (nil,nil), respectively, where x, x1 and x2 are always allocated, thus different from nil. Since language inclusion is decidable for NFTA [CDG+05, Corollary 1.7.9], we leverage an existing algorithm for this problem by Holı́k et al. [HLSV11] to build a set of inference rules and derive a proof search technique. This algorithm searches for counterexamples of the inclusion problem L(A, p)⊆ ⋃n i=1 L(B,qi) by enumerating pairs (r,{s1,...,sm}), where r is a state that can be reached via a series of transitions from p, and {s1,...,sm} are all the states that can be reached via the same series of transitions from q1,...,qk. A counterexample is found when reaching a pair (r,{s1,...,sm}) such that there exists a transition r f → (r1,...,rk), but there is no transition si f → (s1i ,...,s k i ) for any i ∈ [m]. Example 5 Consider the NFTA A and B from Example 4. To check L(A, p)⊆ L(B,q), we start with (p,{q}). A possible run is: (p,{q}) ((p1, p2),{(q1,q2),(q2,q1)}) (p1,{q1,q2}) (p1,{q1}) (p2,{q2}) (p2,{q2,q1}) ((),{()}) (p1,{q1,q2}) ((),{()}) (p1,{q1}) ((),{()}) (p2,{q2}) ((),{()}) (p2,{q2,q1}) f a g a g b g b g The algorithm performs two types of moves: transitions and split actions. The arrows labeled by symbols f ,g,a and b are transitions, for instance the arrow labeled by f takes p into the tuple (p1, p2) by the transition p f−→ (p1, p2) and {q} into the set of tuples {(q1,q2),(q2,q1)}, 5 / 21 Volume 076 (2019) An Entailment Checker for Separation Logic with Inductive Definitions by the transitions q f−→ (q1,q2) and q f−→ (q2,q1). However, the pair ((p1, p2),{(q1,q2),(q2,q1)}) is problematic because it asserts that L(A, p1)×L(A, p2) ⊆ L(B,q1)×L(B,q2)∪L(B,q2)× L(B,q1). Using several properties of the Cartesian product [HLSV11, Theorem 1] there are multiple ways to split this proof obligation into several simpler conjunctive subgoals. If at least one split move leads to a proof, then the inital proof obligation holds. The split move used above simultaneously considers (p1,{q1,q2}), (p1,{q1}), (p2,{q2}) and (p2,{q2,q1}), together asserting that L(A, p1)⊆ L(B,q1) and L(A, p2)⊆ L(B,q2). The other options are: (1) (p1,{q1,q2}) (p1,{q1}), (p1,{q2}), and (p2,{q2,q1}); (2) (p1,{q1,q2}), (p2,{q1}), (p1,{q2}), and (p2,{q2,q1}); (3) (p1,{q1,q2}), (p2,{q1}), (p2,{q2}), and (p2,{q2,q1}). The algorithm does not expand nodes (p,S) with p ∈ S, for which inclusion holds trivially, or having a predecessor (p,S′) with S′ ⊆ S (enclosed in dashed boxes), since any counterexample that can be found from (p,S) could have been discovered from (p,S′). 2.4 A Proof Search Semi-algorithm (IR) Γ1 ` ∆1 ... Γn ` ∆n Γ ` ∆ side conditions .... C Γp ` ∆p We denote sequents as Γ ` ∆, where Γ and ∆ are sets of formulae and commas are read as set union, thus con- traction rules are not necessary. We omit braces and a sequent of the form p(x)` q1(x),...,qn(x) is called ba- sic. An inference rule schema IR is a possibly infinite set of inference rules, called instances of the schema, sharing the same pattern. An inference rule has antecedents Γ1 ` ∆1,...,Γn ` ∆n, and a consequent Γ ` ∆. We write > for an empty antecedent list and an inference rule without antecedents may have a pivot Γp ` ∆p, which is an ancestor of the consequent or, in other words, a sequent preceding the consequent in the transitive closure of the consequent-antecedent relation. The sequence of inference rules applied along the path between the pivot and the consequent is subject to a pivot condition C. A proof system is a set R of inference rule schemata. A derivation built with R is a possibly infinite tree D = (V,v0,S,R,P,B), where V is a set of vertices (or nodes) and v0 ∈V is the root. Every v ∈V is labeled with sequent S(v) and an inference rule schema R(v) ∈ R such that S(v) is the consequent of the instance of R(v) applied at v. Moreover, B(v) ∈ V is a node such that S(B(v)) is the pivot for R(v), if it has one. We call (v,B(v)) a backlink. If v 6= v0, P(v) is the parent of v in the derivation and S(v) is an antecedent for the instance of R(P(v)) with consequent S(P(v)). A proof is a finite derivation in which S(v) = > for all leaves v ∈ V – i.e. on every branch of the derivation, the last inference rule application generates an empty list of antecedents. Given an inductive system S and predicates pσ1,...,σn , qσ1,...,σn1 , ..., q σ1,...,σn k ∈Pred, a proof sys- tem R is: (i) sound if, for any proof D = (V,v0,S,R,P,B) with S(v0) = p(x) ` q1(x),...,qn(x), we have p |=slS q1,...,qn, (ii) complete if p |= sl S q1,...,qn implies the existence of a proof D = (V,v0,S,R,P,B) with S(v0) = p(x)` q1(x),...,qn(x). A sequence π = v1,...,vn of vertices is a trace if, for any i ∈ [n −1], either vi = P(vi+1) or vi+1 = B(vi). π is path if only the former condition holds and, moreover, a direct path if v1 = B(vn). We denote by Λ(π) = R(v1),...,R(vn −1) the sequence of inference rule schemata AVoCS 2018 6 / 21 ECEASST applied between v1 and vn. An inference rule schema IR is applicable on vn and π if there exists an instance ir of IR whose consequent matches S(vn) and whose pivot (if it exists) matches S(vi) for some i < n, such that both the side conditions of ir are satisfied and and Λ(vi,...,vn) abides by its pivot condition. A strategy is a set S of inference rule schemata sequences. A sequence s is a valid prefix for S if there exists another sequence s′ such that their concatenation s·s′ ∈ S. A derivation (proof) D is an S-derivation (S-proof) if, for each maximal path π in D , Λ(π)∈ S. Algorithm 1 Proof search semi-algorithm. data structure: Node(sequent,rule,parent,pivot,children), where: • sequent is the sequent that labels the node, • rule is the inference rule with consequent sequent. • parent is the link to the parent of the node, • pivot is the pivot for the instance of rule applied on sequent • children is the list of children nodes input: inductive system S , sequent p(x)` q1(x),...,qn(x), proof system R , strategy S output: an S-proof built with R , whose root is labeled with sequent p(x)` q1(x),...,qn(x) 1: Root←Node(p(x)` q1(x),...,qn(x),null,null,null,[]) 2: WorkList←{Root} 3: while WorkList 6= /0 do 4: remove N from WorkList 5: let π be the path between Root and N 6: let RN ⊆ R be the inference rule schemata applicable on N and π 7: let R 0N ⊆ RN be the subset of RN with empty antecedent lists 8: if Λ(π)·IR is a valid prefix of S for some IR ∈ R 0N then 9: let ir be an instance of IR such that N.sequent is the consequent of ir 10: N.rule ← IR 11: if ir has pivot N′.sequent for some N′ ∈ π then N.pivot ←N′ 12: mark N as Closed 13: if N not Closed and Λ(π)·IR is a valid prefix of S for some IR ∈ RN then 14: let ir be an instance of IR such that N.sequent is the consequent of ir 15: for each antecedent Γ′ ` ∆′ of ir do 16: N′ ←Node(Γ′ ` ∆′,null,N,null,[]) 17: add N′ to N.children and to WorkList 18: if N.children is empty then mark N as Closed Given an input sequent p(x) ` q1(x),...,qn(x), a set R of inference rules and a strategy S, the proof search semi-algorithm 1 uses a worklist iteration to build a derivation of p(x) ` q1(x),...,qn(x). When a node is removed from the worklist, it chooses (non-deterministically) an inference rule and an instance whose consequent matches the sequent of the node, if one exists. To speed up termination, inference rule schemata without antecedents are considered ea- gerly (line 8). If a proof of the input sequent exists, then there exists a finite execution of the semi-algorithm 1 leading to it. 7 / 21 Volume 076 (2019) An Entailment Checker for Separation Logic with Inductive Definitions 2.5 The Set R slInd of Inference Rules for Separation Logic Entailments Figure 1 gives a set R slInd of inference rule schemata for the entailment problem in SL, which generalize the transitions and split actions performed by the NFTA language inclusion algorithm described in §2.3. To shorten the presentation, we write 〈Γi ` ∆i〉 n i=1 for Γ1 ` ∆1,...,Γn ` ∆n. (LU) and (RU) unfold a predicate atom p(x) by replacing it with the set of predicate rules p(x) :=S R1(x) | ... | Rn(x), with goal variables x and fresh subgoal variables. The left unfolding yields a set of sequents, one for each Ri(x) with i ∈ [n], that must be all proved, whereas the right unfolding replaces p(x) with the set of formulae obtained from R1(x) | ... | Rn(x) in which the subgoal variables are existentially quantified. (LU) 〈Ri(x,yi),Γ\ p(x)` ∆〉 n i=1 Γ ` ∆ p(x)∈Γ, p(x):=S R1(x,y1)|...|Rn(x,yn) y1,...,yn fresh variables (RU) Γ `{∃yi .∗Ri(x,yi)}ni=1 ,∆\ p(x) Γ ` ∆ p(x)∈∆, y1,...,yn fresh p(x):=S R1(x,y1)|...|Rn(x,yn) (RD) p1(x1),..., pn(xn)`{Q jθ | θ ∈ S j}ij=1 φ(x,x1,...,xn), p1(x1),..., pn(xn)`{∃y j .ψ j(x,y j)∗Q j(y j)}kj=1 φ|=sl ∧i j=1∃y j.ψ j φ6|=sl ∨k j=i+1∃y j.ψ j S j⊆Sk(φ,ψ j), j∈[i] (AX) > Γ ` ∆ ∗Γ|=sl ∨ ∆ (ID) > Γθ ` ∆′θ θ flat injective substitution ∆ ⊆ ∆′ .... (R sl Ind) ∗·LU·(R slInd) ∗ Γ ` ∆ (SP) 〈pı̄ j (x)`{q ` ı̄ j (x) | `∈ [k], f j(Q `) = ı̄ j}〉 nk j=1 p1(x1),..., pn(xn)` Q1(x1,...,xn),...,Qk(x1,...,xn) ∀i, j∈[n].xi∩x j=/0, ı̄∈[n]n k Qi=∗nj=1 qij(x j),Q i=〈qi1,...,qin〉 F (Q 1,...,Q k)={ f1,..., fnk} Figure 1: The set R slInd of inference rule schemata for inductive entailments in SL. (RD) eliminates constraints from both sides of a sequent. The existentially quantified variables on the right-hand side are replaced using a (subset of) the finite set Sk(φ,ψ j) = {θ : ⋃k i=1 yi → {nil}∪x∪ ⋃n i=1 xi) | φ |=sl ψ jθ} of substitutions that witness the entailments φ(x,x1,...,xn) |=sl ∃y j .ψ j between the left and right constraints. A transition move in the language inclusion algorithm of [HLSV11] (Example 5) performs (LU), (RU) and (RD) all at once. This is natural because the transition rules of tree automata are controlled uniquely by the function symbols labeling the root of the current input tree, which can be matched unambiguously. When considering more general constraints, matching amounts to discovering non-trivial substitutions that prove an entailment between existentially quantified constraints. (SP) generalizes the split moves performed by the language inclusion algorithm of [HLSV11] and breaks a sequent p1(x1),..., pn(xn) ` Q1(x1,...,xn),...,Qn(x1,...,xn) into basic sequents. Given tuples {Q 1,...,Q k}⊆ Pred n with n ≥ 1, a choice function f maps each tuple Q i into an index f (Q i)∈ [n] corresponding to a position in the tuple. Let F (Q 1,...,Q k) be the set of such choice functions, having cardinality nk ≤ n||Pred|| n . Given a tuple ı̄ ∈ [n]n k , associating a value in [n] to each choice function f ∈ F (Q 1,...,Q k), there exists an application of (SP) generating nk antecedents with left hand-side pı̄ j (xı̄ j ), j ∈ [n k] and right hand-side consisting of all predicate AVoCS 2018 8 / 21 ECEASST atoms q`ı̄ j (xı̄ j ),` ∈ [k] obtained from predicates at position ı̄ j in the tuples Q ` which are mapped to ı̄ j by the choice function f j. In order to obtain a proof, there must exist some application of (SP) – and, therefore, some ı̄ ∈ [n]n k – for which all the generated antecedents can be proven. As shown in [HLSV11, Section 3], the tuples ı̄ ∈ [n]n k encode the transformation of a formula from CNF to DNF and, as such, not all are relevant. More precisely, any ı̄ for which there exists j ∈ [nk] such that ı̄ j 6∈ img( f j) can be discarded. (AX) closes the current branch of the proof if the sequent can be proved using a decision procedure for the underlying constraint logic, by treating predicate symbols as uninterpreted boolean functions. This is a generalization of encountering a pair (p,S) with p ∈ S in the NFTA language inclusion algorithm of [HLSV11]. (ID) introduces backlinks in a derivation, from the consequent Γθ ` ∆′θ to a pivot Γ ` ∆. The pivot condition (R slInd) ∗ ·LU ·(R slInd)∗ requires that (LU) must be applied on the direct path between the pivot and the consequent. Observe that, if Γθ ` ∆′θ denotes a non-valid entailment, there exists (ν,h) ∈ µS sl(∗Γθ)\µS sl(∨ ∆′θ). Since θ is surjective by construction and injective by the side condition, the restriction of θ to FV(Γ∪∆′) has an inverse and, because ∆′ ⊆ ∆, we obtain that (ν◦θ−1,h)∈ µS sl(∗Γ)\µS sl(∨ ∆) is a counterexample for the pivot. The local soundness of R slInd \{ID} is given by [IS17, Lemma 15], whereas the soundness of proofs containing (ID) is established by [IS17, Theorem 6] through the following argument. If the root sequent of a proof denotes an entailment that admits a counterexample, then, by the local soundness, there exists a path in the proof on which this counterexample can be propagated. This path may not end with an application of (AX), as it would violate its side condition, and, thus, must end with an application of (ID), which allows it to be extended to an infinite trace. Then, using the reasoning above to additionally propagate counterexamples through a backlinks, we obtain that the counterexample for the root sequent can also be propagated along a trace with an infinite number of direct paths [IS17, Proposition 1]. We use an additional ranking assumption given by a pre-established well-founded ordering of the counterexamples. In SL, we consider the subheap ordering, where h1 � h2 iff there exists h ∈ Heaps such that h2 = h1 ]h and h1 � h2 if, moreover, h 6= /0. An SL inductive system is ranked if the constraints of every predicate rule with at least one subgoal do not admit an empty heap model. Since (LU) is required on each direct path, this leads to an infinite sequence of counterexamples (ν1,h1),(ν2,h2),... with strictly decreasing heaps h1 � h2 � ... (see [IS17, Lemma 15] and the proof of [IS17, Theorem 6]). However, since the subheap ordering is well-founded, the existence of such sequences is prohibited. We have reached a contradiction and may conclude that there was no counterexample to begin with. Analogously, the language inclusion algorithm of [HLSV11] stops expanding a branch in the search tree whenever it has discovered a pair (p,S) that has a predecessor (p,S′), with S′ ⊆ S. Just as for the (ID) inference rules, backtracking relies on the Infinite Descent principle [Bus18], that forbids infinitely descending sequences of counterexamples. Example 6 Given the system SAB from Example 1, we can use R slInd to build a proof for p(x) ` q(x), partially shown below – we only include the subproof for the first sequent obtained after split. Note the similarities with the proof tree in Example 5. 9 / 21 Volume 076 (2019) An Entailment Checker for Separation Logic with Inductive Definitions p1(x)` q1(x),q2(x) x 7→ (nil,x)` q1(x),q2(x) x 7→ (nil,x)`x 7→ (nil,x),q2(x), ∃y1 .x 7→ (y1,nil)∗q1(y1) > x 7→ (x1,nil), p1(x1)` q1(x),q2(x) x 7→ (x1,nil), p1(x1)` x 7→ (nil,x),∃y1 .x 7→ (y1,nil)∗q1(y1),q2(x) x 7→ (x1,nil), p1(x1)`x 7→ (nil,x),∃y1 .x 7→ (y1,nil)∗q1(y1), x 7→ (nil,nil),∃y1 .x 7→ (y1,nil)∗q2(y1) p1(x)` q1(x),q2(x) > LU RU AX RU RU RD ID p(x)` q(x) x 7→ (x1,x2), p1(x1), p2(x2)` q(x) x 7→ (x1,x2), p1(x1), p2(x2)`∃y1,y2 .x 7→ (y1,y2)∗q1(y1)∗q2(y2), ∃y1,y2 .x 7→ (y1,y2)∗q2(y1)∗q1(y2) p1(x1), p2(x2)` q1(x1)∗q2(x2),q2(x1)∗q1(x2) p1(x)` q1(x),q2(x) p1(x)` q1(x) p2(x)` q2(x) p2(x)` q2(x),q1(x) LU RU RD SP For (SP), let Q 1 = (q1,q2) and Q 2 = (q2,q1) be the tuples of predicates on the right-hand side. The set of choice functions is F (Q 1,Q 2) ={ f1 ={(Q 1,1),(Q 2,1)}, f2 ={(Q 1,1),(Q 2,2)}, f3 = {(Q 1,2),(Q 2,1)}, f4 = {(Q 1,2),(Q 2,2)}}. Out of the 16 index choice tuples for F (Q 1,Q 2), only (1,1,1,2), (1,1,2,2), (1,2,1,2) and (1,2,2,2) are relevant. To obtain the above proof, we chose ı̄ = (1,1,2,2). Only the ranking assumption is necessary to ensure soundness of R slInd. Three additional restric- tions required for completeness are given in [IS17, Section 4.2]. Effectively checking whether a given inductive system satisfies these restrictions requires the existence of a decision procedure for the ∃∗∀∗-quantified fragment of the underlying logic. In general, this problem is undecidable for SL [EIP18, Theorem 1], but the fragment decribed in §2.1 omits the −−∗ operator (primarily responsible for loss of decidability), while the 7→ operator only maps elements in L to tuples in Lk. As such, the satisfiability of ∃∗∀∗-quantified formulae is PSPACE-complete in the fragment we consider [EIP18, Theorems 2 and 3]. A suitable decision procedure for this fragment of SL is given in [RIS17]. Completeness is then assured for entailments involving inductive definitions which generate matching coverage trees of the heap (see [IS17, Section 4.3]). Example 7 Consider the following definitions for doubly-linked lists: dlls(hd, p,tl,n) :=S hd ≈ tl ∧hd 7→ (p,n) | hd 7→ (p,x),dlls(x,hd,tl,n) dllsr(hd, p,tl,n) :=S hd ≈ tl ∧hd 7→ (p,n) | tl 7→ (n,tl′),dllsr(hd, p,x,tl) t1 = {(1,〈0,2〉)} {(2,〈1,3〉)} {(3,〈2,4〉)} t2 = {(3,〈2,4〉)} {(2,〈1,3〉)} {(1,〈0,2〉)} The predicate dlls unfolds the list starting at the head, while dllsr unfolds it starting at the tail. Both dlls |=slS dlls r and dllsr |=slS dlls hold, but they cannot be proven using our inference rules. Take, for instance, the tuple ` = 〈0,1,3,4〉 and the heap h = {(1,〈0,2〉),(2,〈1,3〉),(3,〈2,4〉)}. The pair (`,h) belongs to both µS sl(dlls) and µS sl(dllsr), but dlls generates the coverage tree t1 for h, while dllsr generates the coverage tree t2. Since the trees do not match, R slInd cannot built proofs for either entailment. AVoCS 2018 10 / 21 ECEASST 3 An Inductive Entailment Checker for Separation Logic In this section we describe Inductor, an entailment checker tool that implements the proof-search semi-algorithm 1 from §2.4, using the set R slInd of inference rules for inductive entailments in SL. Inductor is written in C++ and uses the DPLL(T )-based SMT solver CVC4 [BCD+11] as a back- end that it queries in order to establish the satisfiability of SL formulae, in which the occurrences of inductive predicates are treated as uninterpreted functions. More specifically, these queries are handled by the decision procedures provided in [RISK16, RIS17] and integrated into CVC4. The inputs mainly handled by Inductor are SMT-LIB scripts, abiding by the SMT-LIB Stan- dard: Version 2.6 [BFT17]. Theory and logic files are loaded automatically, based on the logic set in the input script being handled. Additionally, proof strategies are specified as nondetermin- istic finite word automata (NFA), in a language similar to that accepted by libVATA [LSV+] (for more details, see Appendix A.1). The front-end interprets these input files using custom parsers constructed with Flex1 and Bison2. 3.1 A Breadth-First Proof Search Implementation The proof search method sketched by algorithm 1 is reliant on the choice of IR made at lines 8 and 13. Whenever there are more than one applicable inference rules, only one is selected and the rest are discarded. Furthermore, as is the case for SP, some inference rules can have multiple possible instances for the same sequent, where only one is required to succeed in obtaining a proof. Algorithm 1 again only chooses one of them. In our implementation, we wanted to explore all the potential derivations resulting from the inference rule instances available at any point. Moreover, since we use a queue for the nodes still needing to be explored, we generate derivations in a breadth-first fashion. Thus, proofs or counterexample are obtained from the shortest possible paths. We use a different tree-like structure to compactly store all the derivations explored. This structure accepts two types of nodes, depicted in Figure 2, which represent sequents (SNode) and inference rule instances (RNode), respectively. The node types alternate in the tree, thus an SNode only has RNode children, and vice-versa. SNode { sequent : A sequent Γ ` ∆, RNode { rule : An inference rule schema states : A list of states in the strategy pivot : SNode pivot for this rule instance, parent : RNode parent of the current node parent : SNode parent of the current node, children : A list of RNode children } children : A list of SNode children } Figure 2: The data structures representing sequents and inference rule instances With these new data structures, we say that an inference rule IR ∈ R slInd is applicable on a given SNode N whenever there exists an instance ir of IR for which: (i) the consequent of ir matches N.sequent and the pivot of ir matches N′.sequent, for some SNode ancestor N′ of N, such that the side conditions of ir are satisfied, and (ii) if R1,...,Rn is the RNode sequence extracted from 1 Flex – The Fast Lexical Analyzer, github.com/westes/flex 2 GNU Bison – The Yacc-compatible Parser Generator, www.gnu.org/software/bison 11 / 21 Volume 076 (2019) An Entailment Checker for Separation Logic with Inductive Definitions the path starting at N′ and ending at N, then the sequence R1.rule,...,Rn.rule satisfies the pivot condition of ir. Algorithm 2 Sketch of our exhaustive proof search implementation input: an SL inductive system S , a basic sequent p(x)` q1(x),...,qn(x), and a proof strategy NFA S = (QS,R slInd,TS,q0,FS) output: VALID and an S-proof starting with p(x)` q1(x),...,qn(x), built with R slInd; INVALID and a counterexample for p(x)` q1(x),...,qn(x); UNKNOWN and the proof search tree constructed by the algorithm 1: Root←SNode(p(x)` q1(x),...,qn(x),[q0],null,[]) 2: Queue←{Root} 3: while Queue 6= [] and Root is Unknown do 4: dequeue N from Queue 5: let QIRN ={q ′ | (q,IR)→ q′ ∈ TS and q ∈N.states} for any IR ∈ R slInd 6: let RN ={IR | QIRN 6= /0 and IR applicable on N} 7: if AX ∈ RN and QAXN ∩FS 6= /0 then 8: R←RNode(AX,null,N,[]) and add R to N.children 9: N′ ←SNode(>,QAXN ,R,[]), add N ′ to R.children and mark it as Closed 10: else if ID ∈ RN and QIDN ∩FS 6= /0 then 11: R←RNode(ID,N′,N,[]) for some pivot N′ of ID and add R to N.children 12: N′ ←SNode(>,QIDN ,R,[]), add N ′ to R.children and mark it as Closed 13: else 14: for each instance ir of each IR ∈ RN do 15: R←RNode(IR,null,N,[]) and add R to N.children 16: let k be the number of antecedents generated by ir 17: if k = 0 and QIRN ∩FS 6= /0 then 18: N′ ←SNode(>,QIRN ,R,[]), add N ′ to R.children and mark it as Closed 19: for each antecedent Γi ` ∆i of ir with i ∈ [k] do 20: Ni ←SNode(Γi ` ∆i,QIRN ,R,[]) and add Ni to R.children 21: if ∆i = /0 then mark Ni as Failed 22: if R is not Failed then enqueue N1,...,Nk in Queue 23: if Root is Closed then 24: return VALID and ExtractProof(Root) 25: else if Root is Failed then 26: return INVALID and ExtractCounterexamples(Root) 27: else return UNKNOWN and Root Both types of nodes are marked with either a Closed, Failed or Unknown status. All nodes are initially Unknown. The status of an SNode can be changed to Closed whenever: (i) its sequent is >, or (ii) at least one of its RNode children is Closed. An RNode becomes Closed when all of its SNode children are Closed. Conversely, an SNode is marked as Failed whenever: (i) its sequent is of the form Γ ` /0, or (ii) all of its RNode children are Failed. An RNode is marked Failed when at least one of its SNode children is Failed. Changing the status of a node prompts AVoCS 2018 12 / 21 ECEASST a status update for all of its ancestors. Algorithm 2 sketches our proof search implementation for R slInd, which, given an input sequent p(x) ` q1(x),...,qn(x) and an NFA S = (QS,R slInd,TS,q0,FS) describing the proof strategy, ex- plores all derivations rooted at the input sequent. The default strategy is (LU ·RU∗ ·RD ·SP?)∗ · LU?·RU∗ ·(AX | ID) from [IS17, Theorem 7]. We construct a node Root and add it to the work queue. While the work queue is not empty and the status of Root is Unknown, we dequeue an SNode N. We denote by QIRN the set of states in S towards which we transition from N.states by applying IR, and build a set RN of applicable inference rule schemata that are also accepted by the strategy. If AX or ID are in RN and, moreover, their application leads S to transition to some final states, then this branch of the derivation has been successful. We add a > leaf, which is marked as Closed. Otherwise, for each IR ∈ RN we consider each instance ir of IR with antecedents Γ1 ` ∆1,...,Γk ` ∆k. If k = 0 and we reach some final state in S by transition with IR, then this branch is successful and we add a > leaf that we mark as Closed. Otherwise, if k > 1, we create an RNode R for ir and an SNode Ni for each of its antecedents. If ∆i = /0 for some i ∈ [k], then Ni is marked as Failed. If this is not the case for any i ∈ [k], then we add N1,...,Nk to the work queue and continue. When the status of Root changes to Closed, then a proof has been obtained. The proof is extracted from the proof search tree and offered as a certificate. Otherwise, if it changes to Failed, then at least one counterexample has been discovered. We extract the counterexamples from the proof search tree and give them as witnesses. If the work queue becomes empty, but the status of Root is still Unknown, then the proof search was inconclusive and our entire proof search tree is returned as justification. 3.2 Case Study: Binary Trees Consider the following ranked definitions for binary trees. The predicate tree accepts any tree model, tree+1 accepts trees with at least one node, and tree + 2 accepts trees with at least one node in which the children of a node are either both allocated or both nil. tree(x) :=St x ≈nil∧emp | x 7→ (l,r),tree(l),tree(r) tree+1 (x) :=St x 7→ (nil,nil) | x 7→ (l,r),tree + 1 (l),tree(r) | x 7→ (l,r),tree(l),tree + 1 (r) tree+2 (x) :=St x 7→ (nil,nil) | x 7→ (l,r),tree + 2 (l),tree + 2 (r) The entailments tree+1 |= sl St tree, tree + 2 |= sl St tree and tree + 2 |= sl St tree + 1 hold, facts corroborated by Inductor. A branch of the proof for tree+2 (x)` tree + 1 (x) is depicted below. However, the reversed entailments do not hold and the counterexamples provided are: • x ≈nil∧emp for tree(x)` tree+1 (x) and tree(x)` tree + 2 (x); • x 7→ (l0,r0)∗tree+1 (l0)∗(r0 ≈nil∧emp) for tree + 1 (x)` tree + 2 (x). Note that predicate atoms can occur within counterexamples and indicate that they can be substituted by any model to obtain a more concrete one. In this case, an immediate substitution with the base case of tree+1 (l0) gives us x 7→ (l0,r0)∗ l0 7→ (nil,nil)∗(r0 ≈ nil∧emp), which can be further simplified to x 7→ (l0,nil)∗l0 7→ (nil,nil). 13 / 21 Volume 076 (2019) An Entailment Checker for Separation Logic with Inductive Definitions tree+2 (x)` tree + 1 (x) x 7→ (l0,r0),tree+2 (l0),tree + 2 (r0)` tree + 1 (x) x 7→ (l0,r0),tree+2 (l0),tree + 2 (r0)`x 7→ (nil,nil),∃l1∃r1 .x 7→ (l1,r1)∗tree + 1 (l1)∗tree(r1), ∃l1∃r1 .x 7→ (l1,r1)∗tree(l1)∗tree+1 (r1) tree+2 (l0),tree + 2 (r0)` tree + 1 (l0)∗tree(r0),tree(l0)∗tree + 1 (r0) tree+2 (l0)` tree(l0) l0 7→ (l00,r00),tree+2 (l00),tree + 2 (r00)` tree(l0) l0 7→ (l00,r00),tree+2 (l00),tree + 2 (r00)`l0 7→ (nil,nil),∃l11∃r11 .l0 7→ (l11,r11)∗tree(l11)∗tree(r11) tree+2 (l00),tree + 2 (r00)` tree(l00)∗tree(r00) tree+2 (l00)` tree(l00) > LU RU RD SP LU RU RD SP ID 3.3 Case Study: Possibly Cyclic and Acyclic List Segments Consider the following ranked definitions for possibly cyclic and acyclic list segments. ls(x,y) :=Sl x ≈ y∧emp | x 7→ z,ls(z,y) ls a(x,y) :=Sl x ≈ y∧emp |¬(x ≈ y)∧x 7→ z,ls a(z,y) Naturally, the entailment lsa |=slSl ls holds, while ls |= sl Sl ls a does not. The proof for the former case is shown below. In the latter case, the counterexample provided by Inductor for ls(x,y)` lsa(x,y) is x≈y∧x 7→z0∗ls(z0,y), from which we can obtain the more concrete one x≈y∧x 7→z0∗(z0 ≈ y∧emp), further simplified to x 7→ x. lsa(x,y)` ls(x,y) x ≈ y∧emp` ls(x,y) x ≈ y∧emp`x ≈ y∧emp,ls(x,y) > ¬(x ≈ y)∧x 7→ z0,lsa(z0,y)` ls(x,y) ¬(x ≈ y)∧x 7→ z0,lsa(z0,y)`x ≈ y∧emp,∃z1.x 7→ z1 ∗ls(z1,y) lsa(z0,y)` ls(z1,y) > LU RU AX RU RD ID 3.4 Case Study: List Segments of Even and Odd Length Consider the following ranked definitions for list segments of even and odd length, together with two alternate definitions of list segments with at least one element. lse(x,y)←Seo x ≈ y∧emp | x 7→ z,ls o(z,y) lso(x,y)←Seo x 7→ y | x 7→ z,ls e(z,y) ls+(x,y)←Seo x 7→ y | x 7→ z,ls +(z,y) l̂s + (x,y)←Seo x 7→ z,ls e(z,y) | x 7→ z,lso(z,y) The entailments lso |=slSeo l̂s + , ls+ |=slSeo l̂s + , ls+ |=slSeo ls e,lso and l̂s + |=slSeo ls e,lso hold, while en- tailments such as lse |=slSeo l̂s + , lse |=slSeo ls o, ls+ |=slSeo ls e or l̂s + |=slSeo ls o do not. A branch of the proof for ls+(x,y) ` l̂s + (x,y) is shown below. For the invalid entailments, Inductor gives the counterexamples: x ≈ y∧emp for both lse(x,y) ` l̂s + (x,y) and lse(x,y) ` lso(x,y); x 7→ y for ls+(x,y)` lse(x,y); x 7→ z0 ∗z0 7→ y for l̂s + (x,y)` lso(x,y). AVoCS 2018 14 / 21 ECEASST ls+(x,y)` l̂s + (x,y) x 7→ z0,ls+(z0,y)` l̂s + (x,y) x 7→ z0,ls+(z0,y)`∃z1 .x 7→ z1 ∗lse(z1,y),∃z1 .x 7→ z1 ∗lso(z1,y) ls+(z0,y)` lse(z0,y),lso(z0,y) z0 7→ z00,ls+(z00,y)` lse(z0,y),lso(z0,y) z0 7→ z00,ls+(z00,y)` z0 ≈ y∧emp,∃z01 .z0 7→ z01 ∗lso(z01,y),lso(z0,y) z0 7→ z00,ls+(z00,y)`z0 ≈ y∧emp,∃z01 .z0 7→ z01 ∗lso(z01,y),z0 7→ y,∃z11 .z0 7→ z11 ∗lse(z11,y) ls+(z00,y)` lso(z00,y),lse(z00,y) > LU RU RD LU RU RU RD ID 3.5 Case Study: Lists of Possibly Cyclic and Acyclic List Segments We adapt our definitions from §3.3 to a fragment in which each memory location points to a pair of locations, and use them to define lists whose elements point at possibly cyclic or acyclic list segments. The last elements of these list segments are, in turn, linked backwards and the last element of the primary list points to the last element of the last secondary list segment. ls(x,y) :=Sll x ≈ y∧emp | x 7→ (z,nil),ls(z,y) lsa(x,y) :=Sll x ≈ y∧emp |¬(x ≈ y)∧x 7→ (z,nil),ls a(z,y) lls(x,v) :=Sll x ≈ v∧emp | x 7→ (z,u)∗w 7→ (v,nil),ls(u,v),lls(z,w) llsa(x,v) :=Sll x ≈ v∧emp | x 7→ (z,u)∗w 7→ (v,nil),ls a(u,v),llsa(z,w) The entailment llsa |=slSll lls holds, while its reverse lls |= sl Sll lls a does not. Part of the proof for llsa(x,v)` lls(x,v) is shown below. The subproof for lsa(u0,v)` ls(u0,v) is mostly skipped as it is identical to the one from §3.3 modulo a variable renaming. llsa(x,v)` lls(x,v) x 7→ (z0,u0)∗w0 7→ (v,nil),lsa(u0,v),llsa(z0,w0)` lls(x,v) x 7→ (z0,u0)∗w0 7→ (v,nil),lsa(u0,v),llsa(z0,w0)`x ≈nil∧emp, ∃z1∃u1∃w1 .x 7→ (z1,u1)∗w1 7→ (v,nil)∗ls(u1,v)∗lls(z1,w1) lsa(u0,v),lls a(z0,w0)` ls(u0,v)∗lls(z0,w0) lsa(u0,v)` ls(u0,v) ... lsa(u00,v)` ls(u00,v) > llsa(z0,w0)` lls(u0,w0) > LU RU RD SP LU ID ID The counterexample provided by Inductor for lls(x,v)` llsa(x,v) is x 7→(z0,u0)∗w0 7→(v,nil)∗ (u0 ≈ v∧u0 7→ (u00,nil)∗ ls(u00,v))∗ lls(z0,w0), from which we obtain the more concrete one x 7→(z0,u0)∗w0 7→(v,nil)∗(u0 ≈ v∧u0 7→(u00,nil)∗(u00 ≈ v∧emp))∗(z0 ≈ w0∧emp), further simplified to x 7→ (z0,v)∗z0 7→ (v,nil)∗v 7→ (v,nil). 15 / 21 Volume 076 (2019) An Entailment Checker for Separation Logic with Inductive Definitions 3.6 Experimental results Table 1 summarizes the experimental results obtained for the entailments discussed in §3.2-3.5. All experiments were run on a 2.10GHz Intel R© CoreTM i7-4600U CPU machine with 4MB of cache. For each case, we indicate: (i) the result (column R), which can be V for VALID or I for INVALID, (ii) the total number of sequent nodes (column Seq), the maximum number of sequent nodes along a branch (column H) and the maximum number of (LU) and (SP) applications along a branch (columns HLU and HSP) of the tree structure defined in Figure 2, which encodes the derivation, (iii) the run time for the proof search algorithm (column T), and (iv) the total number of calls to CVC4 (column CVC4). LHS RHS R Seq HSeq HLU HSP T CVC4 LHS RHS R Seq HSeq HLU HSP T CVC4 tree+1 tree V 34 7 2 1 0.096s 9 tree tree + 1 I 7 4 1 0 0.033s 7 tree+2 tree V 21 7 2 1 0.053s 7 tree tree + 2 I 7 4 1 0 0.028s 5 tree+2 tree + 1 V 1477 11 3 2 5.515s 37 tree + 1 tree + 2 I 38 8 2 1 0.096s 14 lsa ls V 8 5 1 0 0.014s 2 ls lsa I 7 4 1 0 0.015s 2 llsa lls V 21 9 2 1 0.048s 4 lls llsa I 20 8 2 1 0.043s 4 lso l̂s + V 10 6 1 0 0.032s 5 lse l̂s + I 7 4 1 0 0.024s 4 ls+ l̂s + V 16 8 2 0 0.049s 9 lse lso I 7 4 1 0 0.030s 5 ls+ lse,lso V 8 5 1 0 0.020s 4 ls+ lse I 13 6 2 0 0.075s 8 l̂s + lse,lso V 9 5 1 0 0.028s 8 l̂s + lso I 20 9 3 0 0.143s 12 Table 1: Experimental results As shown by the T column in both halves of the table, the execution times are fairly low. The size of the derivations is influenced by how elaborate the inductive definitions are. For instance, tree+1 is defined by three predicate rules, thus when encountered on the left-hand side of an entailment will generate a larger number of nodes due to left-unfolding. On the right-hand side, the number of predicate rules in a definition and the number of subgoals in each predicate rule both influence the complexity of (SP), which can lead to higher execution times than expected, given the size of the derivation, since all instances of (SP) need to be generated and then checked. 4 Conclusions We describe an entailment checker tool called Inductor, which implements a cyclic proof system for Separation Logic with inductive definitions and utilizes dedicated decision procedures in the SMT solver CVC4 to establish the satisfiability of quantifier-free or ∃∗∀∗-quantified Separation Logic formulae. The tool outputs a proof whenever an entailment is found to be valid, or coun- terexamples when it is not. Soundness is warranted by imposing a ranking restriction on the inductive system given as input. It is possible, although the results may be inconclusive, to use Inductor outside of these boundaries. We discuss several case studies and provide experimental results showing fairly low execution times and moderate sizes for the derivations built by the tool in order to obtain proofs or counterexamples. Our inference rules build cyclic proofs with backlinks in similar fashion as CYCLIST [BGP12], AVoCS 2018 16 / 21 ECEASST closing recurring branches of a proof with (ID). We restrict backlinks to ancestral nodes, which allows us to embed the condition necessary to ensure progress along an infinite trace directly into (ID). Because we allow disjunctions on the right-hand side of sequents and (RU) introduces all the cases of an inductive definition – as opposed to CYCLIST and [CJT15], which always choose only one – Inductor can tackle entailments such as ls+(x,y) |=slSeo l̂s + (x,y) in §3.4, which CYCLIST and [CJT15] cannot prove. However, the cut rule in [CJT15] and the canonical rotation relation between trees in SLIDE [IRV14] enable these systems to show entailments such as the ones in Example 7, for which Inductor cannot build proofs. On a different note, the fragment of inductive definitions that SLIDE can translate to tree automata does not allow disequalities between variables, thus it cannot handle predicates and entailments such as lsa(x,y) |=slSl ls(x,y) in §3.3. SLEEK [CDNQ12] and SPEN [ELS17, ESW15] go further than Inductor and are able to check much more complex verification conditions, involving, for instance, concatenations of predi- cates, formulae equivalent to several unfoldings of a predicate and various combinations of allo- cated heap cells and predicate calls. Although most of the inductive definitions for data structures used in these entailments fall into the fragment accepted by Inductor, the entailments themselves are out of the scope of our current implementation. Multiple extensions of the inference rules are possible in order to allow the building of proofs for such entailments (e.g. right unfolding inside the same formula multiple times, reducing any subset of constraints) and are considered for future work. Bibliography [BCD+11] C. Barrett, C. L. Conway, M. Deters, L. Hadarean, D. Jovanović, T. King, A. Reynolds, C. Tinelli. CVC4. In Gopalakrishnan and Qadeer (eds.), Computer Aided Verification: 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings. Pp. 171–177. Springer Berlin Heidelberg, Berlin, Heidelberg, 2011. [BFT17] C. Barrett, P. Fontaine, C. Tinelli. The SMT-LIB Standard: Version 2.6. Technical report, Department of Computer Science, The University of Iowa, 2017. Available at www.SMT-LIB.org. [BGP12] J. Brotherston, N. Gorogiannis, R. L. Petersen. A Generic Cyclic Theorem Prover. In Programming Languages and Systems: 10th Asian Symposium (APLAS’12). Pp. 350–367. Springer, 2012. [Bus18] W. H. Bussey. Fermat’s Method of Infinite Descent. The American Mathematical Monthly 25(8):333–337, 1918. [CDG+05] H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, C. Löding, S. Tison, M. Tommasi. Tree Automata Techniques and Applications. 2005. URL: http://www.grappa.univ-lille3.fr/tata. 17 / 21 Volume 076 (2019) An Entailment Checker for Separation Logic with Inductive Definitions [CDNQ12] W.-N. Chin, C. David, H. H. Nguyen, S. Qin. Automated Verification of Shape, Size and Bag Properties via User-defined Predicates in Separation Logic. Sci. Comput. Program. 77(9):1006–1036, Aug. 2012. doi:10.1016/j.scico.2010.07.004 http://dx.doi.org/10.1016/j.scico.2010.07.004 [CJT15] D. Chu, J. Jaffar, M. Trinh. Automatic Induction Proofs of Data-Structures in Im- perative Programs. In Proc. of the 36th ACM SIGPLAN Conference on Program- ming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015. Pp. 457–466. ACM, New York, NY, USA, 2015. [EIP18] M. Echenim, R. Iosif, N. Peltier. On the Expressive Completeness of Bernays- Schönfinkel-Ramsey Separation Logic. ArXiv e-prints, feb 2018. https://arxiv.org/abs/1802.00195v2 [ELS17] C. Enea, O. Lengál, M. Sighireanu, T. V. . SPEN: A Solver for Separation Logic. In Barrett et al. (eds.), NASA Formal Methods. Pp. 302–309. Springer International Publishing, Cham, 2017. [ESW15] C. Enea, M. Sighireanu, Z. Wu. On Automated Lemma Generation for Separa- tion Logic with Inductive Definitions. In Automated Technology for Verification and Analysis: 13th International Symposium, ATVA 2015, Shanghai, China, October 12- 15, 2015, Proc. Pp. 80–96. Springer International Publishing, Cham, Switzerland, 2015. [HLSV11] L. Holı́k, O. Lengál, J. Simácek, T. Vojnar. Efficient Inclusion Checking on Explicit and Semi-symbolic Tree Automata. In ATVA 2011, Proc. Pp. 243–258. 2011. [IRV14] R. Iosif, A. Rogalewicz, T. Vojnar. Deciding Entailments in Inductive Separation Logic with Tree Automata. In Automated Technology for Verification and Analysis: 12th International Symposium, ATVA 2014, Sydney, NSW, Australia, November 3- 7, 2014, Proc. Pp. 201–218. Springer International Publishing, Cham, Switzerland, 2014. [IS17] R. Iosif, C. Serban. Complete Cyclic Proof Systems for Inductive Entailments. CoRR abs/1707.02415, 2017. http://arxiv.org/abs/1707.02415 [LSV+] O. Lengál, J. Simácek, T. Vojnar, M. Hruska, L. Holı́k. libVATA - A C++ library for efficient manipulation with non-deterministic finite (tree) automata. URL: https://github.com/ondrik/libvata. [Rey02] J. C. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. In Proc. of LICS. Pp. 55–74. 2002. [RIS17] A. Reynolds, R. Iosif, C. Serban. Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic. In Verification, Model Checking, and Abstract In- terpretation: 18th International Conference, VMCAI 2017, Paris, France, January AVoCS 2018 18 / 21 http://dx.doi.org/10.1016/j.scico.2010.07.004 http://dx.doi.org/10.1016/j.scico.2010.07.004 https://arxiv.org/abs/1802.00195v2 http://arxiv.org/abs/1707.02415 ECEASST 15–17, 2017, Proc. Pp. 462–482. Springer International Publishing, Cham, Switzer- land, 2017. [RISK16] A. Reynolds, R. Iosif, C. Serban, T. King. A Decision Procedure for Separation Logic in SMT. In Artho et al. (eds.), Automated Technology for Verification and Analysis: 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings. Pp. 244–261. Springer International Publishing, 2016. [Ser17] C. Serban. Inductor: an entailment checker for inductive systems. URL: https://github.com/cristina-serban/inductor, 2017. [SOR+13] A. Stump, D. Oe, A. Reynolds, L. Hadarean, C. Tinelli. SMT Proof Checking Using a Logical Framework. Formal Methods in System Design 42(1):91–118, 2013. doi:10.1007/s10703-012-0163-3 19 / 21 Volume 076 (2019) http://dx.doi.org/10.1007/s10703-012-0163-3 An Entailment Checker for Separation Logic with Inductive Definitions A Additional Material A.1 Specifying Proof Strategies as Automata Inductor can also accept a proof strategy as input – if no proof strategy is given, then S = (LU ·RU∗ ·RD ·SP?)∗ ·LU? ·RU∗ ·(AX | ID) from [IS17, Theorem 7] will be used as default. By Kleene’s Theorem, it is known that, given a regular expression, there exists an equivalent nondeterministic finite word automaton (NFA), possibly with ε-transitions (NFA-ε). Figure 3 depicts a straightforward NFA-ε that is equivalent to S. q0start q1 q2 q3 q4 q5 LU RU RD SP LU RU AX ID ε ε ε ε Figure 3: An NFA-ε equivalent to our default proof strategy S We are more interested in such a representation because, after applying a certain inference rule, we want to easily check which inference rules that comply with the strategy could be ap- plied next. However, given an NFA-ε, the ε-transitions are cumbersome and, thus, we prefer an equivalent NFA – which is guaranteed to exist, since the two classes of automata are known to be equivalent. As such, the proof strategies that Inductor accepts as input are given as NFA, rather than regular expressions. The definition of such an NFA is specified in a language inspired by the simplicity of the one used by libVATA [LSV+] and whose grammar is depicted in Listing 1. : ’Rules’ : ... : ’Automaton’ string ’States’ ’Initial State’ ’Final States’ ’Transitions’ : ... : string : ... : ’(’ ’,’ ’)’ ’->’ : string Listing 1: Grammar for files specifying proof strategies as NFA Using this language, Listing 2 defines an NFA that is equivalent with the NFA-ε from Figure 3, and consequently, is also equivalent with our default proof search strategy. Rules LU RU RD SP ID AX Automaton Default States q0 q1 q2 q3 q4 q5 Initial state q0 Final states q5 Transitions (q0, LU) -> q1 (q1, RD) -> q3 (q2, RI) -> q3 (q3, LU) -> q4 (q0, LU) -> q4 (q1, RD) -> q4 (q2, RI) -> q4 (q3, RU) -> q4 AVoCS 2018 20 / 21 ECEASST (q0, RU) -> q4 (q2, LU) -> q1 (q2, SP) -> q0 (q3, AX) -> q5 (q0, AX) -> q5 (q2, LU) -> q4 (q2, SP) -> q3 (q3, ID) -> q5 (q0, ID) -> q5 (q2, RU) -> q4 (q2, SP) -> q4 (q4, RU) -> q4 (q1, RU) -> q1 (q2, RI) -> q0 (q2, AX) -> q5 (q4, AX) -> q5 (q1, RD) -> q0 (q2, RI) -> q2 (q2, ID) -> q5 (q4, ID) -> q5 (q1, RD) -> q2 Listing 2: The definition of the NFA corresponding to the default proof search strategy 21 / 21 Volume 076 (2019) Introduction Cyclic Proofs for Inductive Entailments in Separation Logic Preliminaries Inductive Systems of Predicates in Separation Logic Tree Automata Inclusion as Cyclic Proof Search A Proof Search Semi-algorithm The Set RIndsl of Inference Rules for Separation Logic Entailments An Inductive Entailment Checker for Separation Logic A Breadth-First Proof Search Implementation Case Study: Binary Trees Case Study: Possibly Cyclic and Acyclic List Segments Case Study: List Segments of Even and Odd Length Case Study: Lists of Possibly Cyclic and Acyclic List Segments Experimental results Conclusions Additional Material Specifying Proof Strategies as Automata