Mnacho Echenim

Radu Iosif

Nicolas Peltier

Prenex Separation Logic with One Selector Field

We show that infinite satisfiability can be reduced to finite satisfiability for all prenex formulas of Separation Logic with k ≥ 1 selector fields (SL k ). This fact entails the decidability of the finite and infinite satisfiability problems for the class of prenex formulas of SL 1 , by reduction to the first-order theory of a single unary function symbol and an arbitrary number of unary predicate symbols. We also prove that the complexity of this fragment is not elementary recursive, by reduction from the first-order theory of one unary function symbol. Finally, we prove that the Bernays-Schönfinkel-Ramsey fragment of prenex SL 1 formulas with quantifier prefix in the language ∃ * ∀ * is PSPACE-complete.

Introduction

Separation Logic [START_REF] Samin | Bi as an assertion language for mutable data structures[END_REF][START_REF] Reynolds | Separation Logic: A Logic for Shared Mutable Data Structures[END_REF] (SL) is a logical framework used to describe properties of the heap memory, such as the placement of pointer variables within the topology of complex data structures (lists, trees, etc.). The features that make SL attractive for program verification are the ability of defining (i) weakest pre-and post-condition calculi that capture the semantics of programs with pointers, and (ii) compositional verification methods, based on inferring local specifications of methods and threads independently of the context in which they evolve. The search for automated push-button program verification methods motivates the understanding of the decidability, complexity and expressive power of various dialects of SL, used as assertion languages in Hoare-style proofs [START_REF] Samin | Bi as an assertion language for mutable data structures[END_REF], or logic-based abstract domains in static analysis [START_REF] Calcagno | Infer: An Automatic Program Verifier for Memory Safety of C Programs[END_REF].

Formal definitions are provided later, but essentially, SL can be viewed as the first order theory of one partial finite function from U → U k , called a heap, where U denotes the universe of memory locations (i.e., addresses), to which two non-classical connectives are added: (i) the separating conjunction φ 1 * φ 2 , that asserts a split of the heap into disjoint heaps satisfying φ 1 and φ 2 respectively, and (ii) the separating implication or magic wand φ 1 - * φ 2 , stating that each extension of the heap by a disjoint heap satisfying φ 1 must satisfy φ 2 . The number k denotes the number of selector fields and we use the notation SL k to make this number explicit. Quantification over elements of U is allowed. A fragment of separation logic that is practically relevant in verification is when k = 1, i.e., every allocated cell points to a unique cell. This fragment allows, e.g., to describe simply linked lists.

As a simple example of application, let us consider the following Hoare triple with left-hand side that is the weakest precondition of an arbitrary formula φ with respect to a selector update in a program handling lists:

{∃x . i → x * (i → j - * φ)} i.next = j {φ}
Informally, the formula ∃x . i → x * (i → j - * φ) holds when the heap can be separated into disjoint parts, one in which cell i is allocated (the formula i → x states that the heap maps i to x), and one that, when extended by allocating cell i to j, satisfies φ. In other words, the formula states that cell i is allocated and that φ holds after i is redirected to j. A typical verification condition checks whether this formula is entailed by another precondition ψ, generated by a program verifier or supplied by the user. The entailment ψ | = ∃x . i → x * (i → j - * φ) is valid if and only if the formula θ def = ψ ∧ ∀x . ¬(i → x * (i → j - * φ)) is unsatisfiable. In addition, if φ and ψ are formulas in prenex form 3 then, because the assertions i → x and i → j unambiguously define a specific part of the heap (the cell corresponding to i), the quantifiers of φ can be hoisted outside of the separating conjunction and implication, and the formula θ can be written in prenex form.

Deciding the satisfiability of (prenex) SL formulas is thus an important ingredient for push-button program verification. Unlike first order logic, some SL formulas do not have a prenex form (see Example 2 on Page 7). Moreover, satisfiability is decidable (and PSPACE-complete) for quantifier-free SL-formulas, but it is undecidable for firstorder SL-formulas, even when k = 1. In fact SL 1 is as expressive as second-order logic in the presence of * and - * whereas the fragment of SL 1 without - * is decidable but not elementary recursive [START_REF] Brochenin | On the almighty wand[END_REF]. In [START_REF] Echenim | The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary Domains[END_REF], we investigated the Bernays-Schönfinkel-Ramsey fragment of SL k , i.e., the fragment containing formulas of the form ∃x 1 , . . . , x n ∀y 1 , . . . , y m . φ where φ is a quantifier-free formula of SL k . We proved that for k > 1, satisfiability is undecidable in general and decidable if - * only occurs in the scope of an odd number of negations. However, nothing is known concerning the prenex fragment of SL 1 . In this paper we fill in this gap and show that:

1. the prenex fragment of SL 1 is decidable but not elementary recursive, and 2. the Bernays-Schönfinkel-Ramsey fragment of SL 1 is PSPACE-complete.

The results are established using reductions to and from the fragment of first order logic with one monadic function symbol [START_REF] Börger | The Classical Decision Problem[END_REF]. The decidability of this fragment is a consequence of the celebrated Rabin Tree Theorem [START_REF] Michael | Decidability of Second-Order Theories and Automata on Infinite Trees[END_REF], which established the decidability of monadic second order logic of infinite binary tree (S2S). As in our previous work [START_REF] Echenim | The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary Domains[END_REF] and unlike most existing approaches, we consider both the finite and infinite satisfiability problems (other approaches usually assume that the universe is infinite). Essential to our reductions to and from this fragment is a result (proven in [START_REF] Echenim | The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary Domains[END_REF]) stating that each quantifier-free SL k formula, for k ≥ 1, is equivalent to a boolean combination of formulas of some specific forms, called test formulas. Similar translations exist for quantifier-free SL 1 [START_REF] Lozes | Expressivité des logiques spatiales[END_REF][START_REF] Brochenin | On the almighty wand[END_REF] and for SL 1 with one quantified variable [START_REF] Demri | Separation Logic with One Quantified Variable[END_REF]. In addition we show in the present paper that the infinite satisfiability reduces to the finite satisfiability for quantified boolean quantifications of test formulas.

Preliminaries

In this section, we briefly review some usual definitions and notations (missing definitions can be found in, e.g., [START_REF] Fitting | First-Order Logic and Automated Theorem Proving[END_REF] or [START_REF] Börger | The Classical Decision Problem[END_REF]). We denote by Z the set of integers and by N the set of positive integers including zero. We define

Z ∞ = Z ∪ {∞} and N ∞ = N ∪ {∞},
where for each n ∈ Z we have n + ∞ = ∞ and n < ∞. For two positive integers m ≤ n, we denote by m . . n the set {m, m + 1, . . . , n}. For a countable set S we denote by ||S || ∈ N ∞ the cardinality of S . A decision problem is in (N)SPACE(n) if it can be decided by a (nondeterministic) Turing machine in space O(n) and in PSPACE if it is in SPACE(n c ) for some input-independent integer c ≥ 1.

First Order Logic

Syntax Let Var be a countable set of variables, denoted by x, y, z and B and U be distinct sorts, where B denotes booleans and U denotes memory locations. A function symbol f has #( f ) ≥ 0 arguments of sort U and a sort σ( f ), which is either B or U. If #( f ) = 0, we call f a constant. We use ⊥ and for the boolean constants false and true, respectively. First-order (FO) terms t and formulas ϕ are defined by the following grammar:

t := x | f (t, . . . , t #( f ) ) ϕ := ⊥ | | ϕ ∧ ϕ | ¬ϕ | ∃x . ϕ | t ≈ t | p(t, . . . , t #(p)
)

where x ∈ Var, f and p are function symbols, σ( f ) = U and σ(p) = B. We write

ϕ 1 ∨ ϕ 2 for ¬(¬ϕ 1 ∧ ¬ϕ 2 ), ϕ 1 → ϕ 2 for ¬ϕ 1 ∨ ϕ 2 , ϕ 1 ↔ ϕ 2 for ϕ 1 → ϕ 2 ∧ ϕ 2 → ϕ 1 and ∀x . ϕ for ¬∃x . ¬ϕ.
The size of a formula ϕ, denoted by size(ϕ), is the number of occurrences of symbols in ϕ. A variable is free in ϕ if it occurs in ϕ but not in the scope of a quantifier. We denote by fv(ϕ) the set of variables that are free in ϕ. A sentence is a formula ϕ such that fv(ϕ) = ∅. The Bernays-Schönfinkel-Ramsey fragment of FO [BSR(FO)] is the set of sentences of the form ∃x 1 . . . ∃x n ∀y 1 . . . ∀y m . ϕ, where ϕ is a quantifier-free formula in which all function symbols f of arity #( f ) > 0 have sort σ( f ) = B. We denote by FO 1 the set of formulas built on a signature containing only one function symbol of arity 1, the equality predicate and an arbitrary number of unary predicate symbols 4 .

Semantics First-order formulas are interpreted over FO-structures (called structures, when no confusion arises) S = (U, s, i), where U is a nonempty countable set, called the universe, the elements of which are called locations, s : Var → U is a function mapping variables to locations called a store, and i interprets each function symbol f by a function

f i : U #( f ) → U, if σ( f ) = U and f i : U #( f ) → {⊥, } if σ( f ) = B.
A structure (U, s, i) is finite when ||U|| ∈ N and infinite otherwise. We write S | = ϕ iff ϕ is true when interpreted in S. This relation is defined recursively on the structure of ϕ, as usual. When S | = ϕ, we say that S is a model of ϕ. A formula is satisfiable when it has a model. We write ϕ 1 | = ϕ 2 when every model of ϕ 1 is also a model of ϕ 2 and by ϕ 1 ≡ ϕ 2 we mean ϕ 1 | = ϕ 2 and ϕ 1 | = ϕ 2 . The (in)finite satisfiability problem asks, given a formula ϕ, whether a (in)finite model exists for this formula. We now recall and refine an essential known result concerning the satisfiability problem for formulas in FO 1 : Theorem 1. The finite satisfiability problem is decidable for first-order formulas in FO 1 . Furthermore, the problem is nonelementary even if the formula contains no unary predicate symbols.

Proof. The decidability result is proven in [1, Corollary 7.2.12, page 341]. The complexity lower bound is established in [1, Theorem 7.2.15, page 342] for arbitrary domains, however a careful analysis of the proof reveals that it also holds for finite domains. Indeed, the proof goes by showing that a domino problem of nonelementary complexity can be polynomially reduced to the satisfiability problem for a first-order formula ϕ satisfying the conditions of the lemma. The initial domino problem is not important here and its definition is omitted. To establish the desired result, we only have to prove that satisfiability is actually equivalent to finite satisfiability for the obtained formula ϕ. The formula ϕ output of the reduction is of the following form (see [START_REF] Börger | The Classical Decision Problem[END_REF]Page 345]): ϕ = α ∧ γ ∧ η [D(x)/δ(x), P i (x, y)/π i (x, y), where:

α = ∃x∀y . f (x) ≈ x∧ f n+1 (y) ≈ x. This formula states that the domain can be viewed as a tree of height at most n + 1, where the (necessarily unique) element corresponding to the variable x is the root of the tree, and where f maps every other node to its parent. -The formula δ is based on an equivalence relation E n-1 on nodes in a (possibly infinite) tree, which is inductively defined as follows:

• All nodes are E 0 -equivalent.

• For m > 1, two nodes are E m -equivalent if for every E m-1 -equivalence class K, either both nodes have no child in K or both nodes have a child in K. The formula δ(x) states that x is a child of the root with at most one child in each E n-1 -equivalence class. We also denote by E the intersection n i=1 E i . -γ = ∀x, y . δ(x) ∧ δ(y) ∧ β n (x, y) → x ≈ y, where β n (x, y) is a formula stating that x and y have height at most n and are E n -equivalent. -For i = 0, . . . , r, π i (x, y) is a formula stating that there exists a z satisfying the following property denoted by P(i, a, b): z is a child of the root and for every E n-1equivalence class K and for all j, k ∈ {0, 1}, if x and y have exactly j and k children in K respectively, then z has exactly 2 + 4i + 2 j + k children in K. -η is equivalent to a closed formula defined over a signature containing a unary predicate symbol D and r + 1 binary predicate symbols P 0 ,. . . ,P r , in which every quantification ranges over elements x satisfying D(x). It is thus of the form ∃x . D(x) ∧ ψ or ∀x . D(x) → ψ. -η [D(x)/δ(x), P i (x, y)/π i (x, y)] denotes the formula η in which every occurrence of a formula D(x) (resp. P i (x, y)) is replaced by δ(x) (resp. π i (x, y)). Thus it is equivalent to a formula in which every quantification ranges over elements x satisfying δ(x).

The formal definitions of η , δ(x) and π i (x, y) are unimportant and omitted. Let I = (U, s, i) be a model of ϕ, with f = f i . We denote by r the root of the tree, i.e., the unique element of U with (U, s With each element a ∈ U and each E-equivalence class K, we associate a set ν(a, K) containing exactly one child of a in K if such a child exists, otherwise ν(a, K) is empty. We now consider the subset U of U defined as the set of elements a such that for every m ∈ N, f m (a) occurs either in {r} ∪ B ∪ Π or in a set ν(b, K), where b ∈ U and K is an E-equivalence class. Note that r ∈ U and that if a ∈ U then necessarily f(a

[x → r], i) | = ∀y . f (x) ≈ x ∧ f n+1 (y) ≈ x. Given i ∈ [0, r] and a, b ∈ U, if (U, s[x → a, y → b], i) | = π i (x,
) ∈ U . Furthermore, if f(b) ∈ U and b ∈ ν(f(b), K) then b ∈ U .
It is easy to check that U is finite. Indeed, since (U, s, i) | = α and no new node or edge is added, all nodes are of height less or equal to n + 1. Furthermore, all nodes have at most ||B|| + ||Π|| + #K children in U , where #K denotes the number of E-equivalence classes.

We denote by I = (U , s, i ) the restriction of I to the elements of U (we may assume that s is a store on U since ϕ is closed). We prove that I | = ϕ.

-Since U contains the root, and

I | = α, we must have I | = α. -Observe that U necessarily contains ν(b, K),
(U , s[x → a, y → a ], i ) | = β n (x, y) iff (U, s[x → a, y → a ], i) | = β n (x, y)
By definition, for every a ∈ B and m ∈ N, f m (a) ∈ {a, r}, thus B ⊆ U . Because no new edges are added, we deduce:

(U , s[x → a], i ) | = δ(x) ⇔ (U, s[x → a], i) | = δ(x) ⇔ a ∈ B Consequently, since I | = γ, we have I | = γ. -All elements in µ(i, a, a ) with a, a ∈ B occur in U (because if b ∈ µ(i, a, a ) and m ∈ N then f m (b) ∈ {r} ∪ B ∪ µ(i, a, a ))
, thus, for all a, a ∈ B:

(U , s[x → a, y → a ], i ) | = π i (x, y) ⇔ (U, s[x → a, y → a ], i) | = π i (x, y)
Since all quantifications in η range over elements in B, we deduce, by a straightforward induction on the formula, that I and I necessarily agree on the formula

η [D(x)/δ(x), P i (x, y)/π i (x, y)]. Consequently, I | = η [D(x)/δ(x), P i (x, y)/π i (x, y)].

Separation Logic

Syntax Let k ∈ N be a strictly positive integer. The logic SL k is the set of formulas generated by the grammar:

ϕ := ⊥ | | emp | x ≈ y | x → (y 1 , . . . , y k ) | ϕ ∧ ϕ | ¬ϕ | ϕ * ϕ | ϕ - * ϕ | ∃x . ϕ
where x, y, y 1 , . . . , y k ∈ Var. The connectives * and - * are respectively called the separating conjunction and separating implication (magic wand). The symbols ∨, →, ↔ and ∀ are defined as in first-order logic, and in addition, we write ϕ 1 ϕ 2 for ¬(ϕ 1 - * ¬ϕ 2 ) ( is called septraction).

A tuple (y 1 , . . . , y k ) ∈ Var k is sometimes denoted by y. The size and free variables of an SL k formula ϕ are defined as for first-order formulas. The prenex fragment of SL k (denoted by

PRE(SL k )) is the set of sentences Q 1 x 1 . . . Q n x n . φ, where Q 1 , . . . , Q n ∈ {∃, ∀} and φ is a quantifier-free SL k formula. The Bernays-Schönfinkel-Ramsey fragment of SL k [BSR(SL k )]
is the set of sentences ∃x 1 . . . ∃x n ∀y 1 . . . ∀y m . φ, where φ is a quantifierfree SL k formula. Since there are no function symbols of arity greater than zero in SL k , there are no restrictions, other than the form of the quantifier prefix, defining BSR(SL k ).

Semantics SL k formulas are interpreted over SL-structures (called structures when no confusion arises) I = (U, s, h), where U and s are defined as for first-order formulas 5and h : U fin U k is a finite partial mapping of locations to k-tuples of locations, called a heap. A structure (U, s, h) is finite when ||U|| ∈ N and infinite otherwise (note that the heap is always finite, but that the universe may be finite or infinite).

Given a heap h, we denote by dom(h) the domain of the heap, by img(h

) def = { i | ∃ ∈ dom(h), h( ) = ( 1 , . . . , k ), i ∈ 1 . . k } its range and we let elems(h) def = dom(h) ∪ img(h). A element x is allocated in (U, s, h) if it belongs to dom(h). For a store s, we define its range img(s) def = { | x ∈ Var, s(x) = }. If x = (x 1 , . . . , x n
) is a vector of pairwise distinct variables and e = (e 1 , . . . , e n ) is a vector of elements of U of the same length as x, then s[x → e] denotes the store that maps x i to e i (for all i ∈ 1 . . n ) and coincides with s on every variable distinct from x 1 , . . . , x n . Two heaps h 1 and h 2 are disjoint if and only if dom(h 1 ) ∩ dom(h 2 ) = ∅, in which case h 1 h 2 denotes their union (h 1 h 2 is undefined if h 1 and h 2 are not disjoint). The relation (U, s, h) | = ϕ is defined inductively, as follows:

(U, s, h) | = emp ⇔ h = ∅ (U, s, h) | = x ≈ y ⇔ s(x) = s(y) (U, s, h) | = x → (y 1 , . . . , y k ) ⇔ h(s(x)) = (s(y 1 ), . . . , s(y k )) ∧ dom(h) = {s(x)} (U, s, h) | = ϕ 1 ∧ ϕ 2 ⇔ (U, s, h) | = ϕ 1 and (U, s, h) | = ϕ 2 (U, s, h) | = ¬ϕ ⇔ (U, s, h) | = ϕ (U, s, h) | = ∃x . ϕ ⇔ there exists e ∈ U s.t. (U, s[x → e], h) | = ϕ (U, s, h) | = ϕ 1 * ϕ 2 ⇔ there exist disjoint heaps h 1 , h 2 such that h = h 1 h 2 and (U, s, h i ) | = ϕ i , for i = 1, 2 (U, s, h) | = ϕ 1 - * ϕ 2
⇔ for all heaps h disjoint from h such that (U, s, h

) | = ϕ 1 , we have (U, s, h h) | = ϕ 2
Satisfiability, entailment and equivalence are defined for SL k as for FO formulas. The finite [resp. infinite] satisfiability problem for SL k asks whether a finite [resp. an infinite] model exists for a given formula. We write φ

≡ fin ψ [φ ≡ inf ψ] whenever (U, s, h) | = φ ⇔ (U, s, h) | = ψ for every finite [infinite] structure (U, s, h).
As stated in the introduction, SL formulas do not admit prenex forms in general, because the quantifiers cannot be shifted outside of separating connectives. This is an essential difference with FO, where each formula is equivalent to a linear-size formula in prenex form. In particular, the equivalences φ * ∀x . ψ(x) ⇔ ∀x . φ * ψ(x) and φ - * ∃x . ψ(x) ⇔ ∃x . φ - * ψ(x) do not always hold.

Example 2. For instance, the formula (∀x . x → x) * is satisfiable only on universes of cardinality 1 (because ∀x . x → x entails that the domain of the heap is of size 1 and contains all locations), but the formula ∀x . (x → x * ) is satisfiable if and only if the universe is finite and each location points to itself.

Test formulas for SL k

This section presents the definitions and results from [START_REF] Echenim | The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary Domains[END_REF], needed for self-containment.

Definition 3. The following patterns are called test formulas of SL k , for any k ≥ 1:

x → y def = x → y * |U| ≥ n def = |h| ≥ n, n ∈ N alloc(x) def = x → (x, . . . , x) k times - * ⊥ |h| ≥ |U| -n def = |h| ≥ n + 1 - * ⊥, n ∈ N x ≈ y |h| ≥ n def = |h| ≥ n -1 * ¬emp, if n > 0 , if n = 0
where x, y ∈ Var, y ∈ Var k is a k-tuple of variables and n ∈ N is a positive integer. A literal is a test formula or its negation and a minterm is any conjunction of literals.

The semantics of test formulas is intuitive: x → y holds when x denotes a location and y is the image of that location in the heap, alloc(x) holds when x denotes a location in the domain of the heap (allocated The following result establishes a translation of quantifier-free SL k formulas into boolean combinations of test formulas. A literal is a test formula or its negation and a minterm is any conjunction of literals.

Lemma 4. Given a quantifier-free SL k formula φ, there exist finite sets of minterms µ fin (φ) and µ inf (φ) such that φ ≡ fin M∈µ fin (φ) M and φ ≡ inf M∈µ inf (φ) M. Furthermore, the size of every M ∈ µ fin (φ) ∪ µ inf (φ) is polynomial w.r.t. size(φ), and given a minterm M, the problem of checking whether M ∈ µ fin (φ) [resp. M ∈ µ inf (φ)] is in PSPACE.

Proof. See [START_REF] Echenim | The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary Domains[END_REF].

Given a quantifier-free SL k formula φ, the number of minterms in µ fin (φ) [resp. in µ inf (φ)] is exponential in the size of φ, in the worst case. An optimal decision procedure does not generate and store these sets explicitly, but rather enumerate minterms lazily.

Example 5. The formula x → y * y → x * ¬emp is equivalent to the minterm: x → y ∧ y → x ∧ x ≈ y ∧ |h| ≥ 3. Indeed, because the atoms x → y, y → x and ¬emp must be satisfied on disjoint heaps, the initial formula entails that x, y are distinct and that the heap contains at least 3 allocated elements (x, y and an additional element distinct from x and y). The formula x → y - * x → z is equivalent to the disjunction of minterms alloc(x) ∨ (¬|h| ≥ 1 ∧ y ≈ z). Indeed, if x is allocated then the heap cannot be extended by a disjoint heap satisfying x → y hence the separating implication trivially holds, otherwise the implication holds iff the heap is empty and y ≈ z.

From Infinite to Finite Satisfiability

We begin by showing that for prenex SL-formulas, the infinite satisfiability problem can be reduced to the finite satisfiability problem. The intuition is that two SL-structures defined on the same heap and store can be considered as equivalent if both have enough locations outside of the heap. Definition 6. Let X be a set of variables and let n ∈ N. Two SL-structures I = (U, s, h) and I = (U , s , h ) are (X, n)-similar (written I ∼ n X I ) iff the following conditions hold: -If m = 0, then we have φ = ψ, we show that I and I agree on every atomic formula in φ, which entails by an immediate induction that they agree on φ. By Condition 4 in Definition 6, we already have that I and I agree on every atom x ≈ x with x, x ∈ fv(φ). By Condition 1, I and I agree on all atoms |h| ≥ n. Consider an atom ∈ {y 0 → (y 1 , . . . , y k ), alloc(y 0 )}, with y 0 , . . . , y k ∈ fv(φ). If for every i ∈ 0 . . k we have s(y i ) ∈ elems(h) then by Condition 2 we deduce that s and s coincide on y 0 , . . . , y k hence I and I agree on because they share the same heap. The same holds if s (y i ) ∈ elems(h), ∀i ∈ 0 . . k . If both conditions are false, then we must have I | = and I | = , by definition of elems(h), thus I and I also agree on in this case.

1. h = h . 2. For every x ∈ X, if s(x) ∈ elems(h) or s (x) ∈ elems(h ) then s(x) = s (x).
-Assume that m ≥ 1 and Q 1 = ∃, i.e., φ = ∃x 1 . φ . Then there exists e ∈ U such that (U, s[x 1 → e], h) | = φ . We construct an element e ∈ U as follows. If e = s(y), for some y ∈ fv(φ), then we let e = s (y). If ∀y ∈ fv(φ), e s(y) and if e ∈ elems(h) then we let e = e. Otherwise, e is an arbitrarily chosen element in U \ (s (fv(φ)) ∪ elems(h)). Such an element necessarily exists, because by Condition 3 in Definition 6, U contains at least m + ||fv(φ)|| ≥ 1 + ||s(fv(φ))|| elements distinct from those in elems(h). Let J = (U, s[x 1 → e], h) and J = (U, s[x 1 → e], h), we prove that J ∼ m-1 fv(φ)∪{x 1 } J . This entails the required results since by the induction hypothesis we deduce J | = φ , so that I | = φ.

• Condition 1 trivially holds.

• For Condition 2, assume that there exists a variable x ∈ fv(φ) We define the following shorthands:

∪ {x 1 } such that either s[x 1 → e](x) ∈ elems(h) or s [x 1 → e ](x) ∈ elems(h), and s[x 1 → e](x) s [x 1 → e ](x). Since I ∼ m fv(φ) I , if x ∈ fv(φ) then [s(x) ∈ elems(h) ∨ s (x) ∈ elems(h)] ⇒ s(x) = s (x)
x ∈ h def = ∃y 0 , y 1 , . . . y k . y 0 → (y 1 , . . . , y k ) ∧ k i=0 x ≈ y i dist(x 1 , . . . , x n ) def = n i=1 i-1 j=1 ¬(x i ≈ x j ) λ p def = ∃x 1 , . . . , x p . (dist(x 1 , . . . , x p ) ∧ p i=1 ¬x i ∈ h) It is clear that (U, s, h) | = λ p iff ||U \ elems(h)|| ≥ p.
In particular, λ p is always true on an infinite universe. Observe, moreover, that λ p belongs to the PRE(SL k ) fragment, for any p ≥ 2 and any k ≥ 1.

The following lemma reduces the infinite satisfiability problem to the finite version of this problem. This is done by adding an axiom ensuring that there are enough locations outside of the heap. Note that there is no need to consider test formulas of the form |U| ≥ n [resp. |h| ≥ |U|n] because they always evaluate to true [resp. false] on infinite SL-structures.

Theorem 8. Let φ = Q 1 x 1 . . . Q m x m
. ψ be a prenex SL k formula, where Q i ∈ {∀, ∃} for i = 1, . . . , m and fv(φ) = ∅. Assume that ψ is a boolean combination of universe-independent test formulas. The two following assertions are equivalent.

1. φ admits an infinite model.

PRE(SL 1 ) is Decidable but Not Elementary Recursive

Using Lemma 4 and Theorem 8 we shall prove that the satisfiability problem is decidable for the prenex fragment of SL 1 . This shows that PRE(SL 1 ) is strictly less expressive than SL 1 , because SL 1 has an undecidable satisfiability problem [START_REF] Brochenin | On the almighty wand[END_REF]. For this purpose, we first define a translation of quantified boolean combination of test formulas into FO that is sat-preserving on finite structures. Let d be a unary predicate symbol and for i = 1, . . . , k, let f i be a unary function symbol. We define the following transformation from quantified boolean combinations of test formulas into first order formulas:

Θ(x ≈ y) def = x ≈ y Θ(x → (y 1 , . . . , y k )) def = d(x) ∧ k i=1 y i ≈ f i (x) Θ(alloc(x)) def = d(x) Θ(|U| ≥ n) def = ∃x 1 , . . . , x n . dist(x 1 , . . . , x n ) Θ(|h| ≥ n) def = ∃x 1 , . . . , x n . dist(x 1 , . . . , x n ) ∧ n i=1 d(x i ) Θ(|h| ≥ |U| -n) def = ∃x 1 , . . . , x n ∀y . n i=1 y ≈ x i → d(y) Θ(¬φ) def = ¬Θ(φ) Θ(φ 1 ∧ φ 2 ) def = Θ(φ 1 ) ∧ Θ(φ 2 ) Θ(∃x . φ) def = ∃x . Θ(φ)
Proposition 9. Let φ be a quantified boolean combination of test formulas. The formula φ has a finite SL model if and only if Θ(φ) has a finite FO model.

Proof. An FO-structure I = (U, s, i) on the signature d, f 1 ,. . . ,f k corresponds to an SLstructure I = (U , s , h) iff U = U , s = s , d i = dom(h) and for every j ∈ 1 . . k , f i j (x) = y j if h(x) = (y 1 , . . . , y k ). It is clear that for every finite first-order structure I there exists a finite SL-structure I such that I corresponds to I and vice-versa. Furthermore, if I corresponds to I then it is straightforward to check that

I | = φ ⇔ I | = Θ(φ).
If φ is an SL 1 formula, then clearly Θ(φ) is in FO 1 , with one monadic boolean function symbol d and one function symbol f 1 of sort σ( f ) = U. This yields the following result: Theorem 10. The finite and infinite satisfiability problems are decidable for PRE(SL 1 ).

Proof. Given a formula

ψ = Q 1 x 1 . . . Q n x n . φ of PRE(SL 1 )
, where φ is quantifier-free, let µ def = M∈µ inf (φ) M be the infinite-domain equivalent expansion of φ as a disjunction of minterms. We have ψ ≡ inf Q 1 x 1 . . . Q n x n . µ (Lemma 4) and Q 1 x 1 . . . Q n x n . µ admits an infinite model if and only if Q 1 x 1 . . . Q n x n . µ ∧ λ n admits a finite model (Theorem 8; note that µ contains no occurrence of universe-dependent formulas, as such formulas are always true or false in infinite universes). [START_REF] Lozes | Expressivité des logiques spatiales[END_REF]. Since the latter formula belongs to FO 1 , its finite satisfiability problem is decidable (Theorem 1). The finite case is similar.

But Q 1 x 1 . . . Q n x n . µ ∧ λ n has a finite SL model if and only if Θ(Q 1 x 1 . . . Q n x n . µ ∧ λ n ) has a finite FO model (Proposition

The complexity lower bound is established thanks to the following proposition.

Proposition 11. There is a polynomial reduction of the finite satisfiability problem for first-order formulas with one monadic function symbol f and no predicate symbols other than ≈ to the finite [resp. infinite] satisfiability problem for quantified boolean quantifications of test formulas in SL 1 .

Proof. By flattening we may assume that all the equations occurring in the considered first-order formula are of the form f (x) ≈ y or x ≈ y, where x, y are variables. For finite domains, the reduction is immediate: it suffices to add the axiom ∀x . alloc(x), stating that the heap is a total function, and to replace all equations of the form f (x) ≈ y by x → y. It is straightforward to check that satisfiability is preserved ( f is encoded in the heap). For infinite domains, it is not possible to add the axiom ∀x . alloc(x) as the resulting formula is unsatisfiable 6 , so the first-order formula is translated on one that holds on the (finite) domain of the heap. We thus add the axiom ¬emp ∧ ∀x, y . x → y → alloc(y), and we replace every quantification ∀x . φ (resp. ∃x . φ) by a quantification over the domain of the heap: ∀x . alloc(x) → φ (resp. ∃x . alloc(x) ∧ φ). It is straightforward to check that satisfiability is preserved. Note that infinite satisfiability is equivalent to finite satisfiability, since the quantifications range over elements occurring in the heap.

Note there is no obvious reduction from the usual first-order satisfiability problem (i.e., on arbitrary models), because the heap is always finite in SL-structures. This explains why we had to refine in Theorem 1 the complexity lower bound from [START_REF] Börger | The Classical Decision Problem[END_REF] to cope with finite satisfiability.

Theorem 12. The finite and infinite satisfiability problems are not elementary recursive for PRE(SL 1 ).

Proof. The proof follows immediately from the lower bound complexity result of Theorem 1 and from the reductions in Proposition 11.

The BSR(SL 1 ) Fragment is PSPACE-complete

The last result concerns the tight complexity of the BSR(SL 1 ) fragment. For k ≥ 2, we showed that BSR(SL k ) is undecidable, in general, and PSPACE-complete if the positive occurrences of the magic wand are forbidden7 [START_REF] Echenim | The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary Domains[END_REF]. Here we show that BSR(SL 1 ) is PSPACE-complete. The result does not directly follow from the Σ p 2 -complexity of the satisfiability problem for ∃ * ∀ * first-order formulas with one unary function symbol 8because only partial finite functions are considered in our context. The proof is based on the following definitions and results.

Definition 13. A model (U, s, h) of a formula ϕ is minimal if ϕ admits no model of the form (U , s , h ) with U U.
Proposition 14. Let ϕ = ∀y 1 , . . . , y m . φ be a prenex formula with free variables x 1 , . . . , x n (with n > 0) where φ is a boolean combination of universe-independent test formulas, and let I = (U, s, h) be a minimal model of ϕ. Then U = {h j (s

(x i )) | i ∈ 1 . . n , j ∈ N}. Proof. Let U = {h j (s(x i )) | i ∈ 1 .
. n , j ∈ N} and assume that U U; note that U ∅ since n > 0. Let s be a store on U coinciding with s on x 1 , . . . , x n and let h be the restriction of h to U . Both s and h are well-defined by construction of U , and h is a heap on U . Since U is minimal, (U , s , h ) | = ϕ, thus there exist b 1 , . . . , b m ∈ U such that by letting s

1 def = s [y i → b i | i ∈ 1 . . m ], we have (U , s 1 , h ) | = ¬φ.
Since the atomic formulas in φ are universe-independent, we deduce that (U, s 1 , h ) | = ¬φ. Further, s 1 and

s[y i → b i | i ∈ 1 . . m ]
coincide on all the variables x 1 , . . . , x n , y 1 , . . . , y m that are free in φ, thus (U, s[

y i → b i | i ∈ 1 . . m ], h ) | = ¬φ.
Finally, h and h coincide on every element of U and by definition we have s(

x i ), b j ∈ U for i ∈ 1 . . n and j ∈ 1 . . m , hence (U, s[y i → b i | i ∈ 1 . . m ], h) | = ¬φ,
and (U, s, h) | = ϕ, which contradicts our assumption.

Definition 15. Let ϕ be a formula with free variables x 1 , . . . , x n and let I = (U, s, h) be a structure. A line for (I, ϕ) is a sequence of pairwise distinct elements a 1 , . . . , a in U such that:

1. ∀i ∈ 1 . . -1 , a i+1 = h(a i ). 2. ∀i ∈ 1 . . -1 , ∀e ∈ U, if h(e) = a i+1 then e = a i . 3. ∀i ∈ 1 . . , ∀ j ∈ 1 . . n , a i s(x j ).
The next proposition shows that there is a bound on the length of any line in a minimal model.

Proposition 16. Let ϕ = ∀y 1 , . . . , y m . φ be a prenex formula with free variables x 1 , . . . , x n where φ is a boolean combination of domain-independent test formulas, and let I = (U, s, h) be a model of ϕ. If (I, ϕ) admits a line of length strictly greater than m + 2 then I is not minimal.

Proof. Let a 1 , . . . , a l be a sequence of elements satisfying the conditions of Definition 15 with l > m+2. Let I = (U , s , h ), where U def = U\{a 2 }, s is a store on U coinciding with s on all variables x such that s(x) ∈ U , dom(h We emphasize some useful consequences of the above definitions before proving that (U , s 1 , h ) | = φ. Let V = {x 1 , . . . , x n } ∪ {y j | j ∈ 1 . . m , s 1 (y j ) {a 3 , . . . , a i }}. By definition s and s coincide on x 1 , . . . , x n , and s 1 (y j ) = b j = b j = s 1 (y j ) if b j {a 3 , . . . , a i }, hence s 1 and s[y j → b j | j ∈ 1 . . m ] coincide on every variable in V. Furthermore, for every variable x ∈ V, s 1 (x) ∈ U \ {a 2 , . . . , a i }. Indeed, either x ∈ {x 1 , . . . , x n } and in this case s(x) {a 1 , . . . , a n } by Definition 15 (3); or x = y j for some j ∈ 1 . . m , and then s 1 (x) = b j = b j {a 3 , . . . , a i }, so that s 1 (x) ∈ U \ {a 3 , . . . , a i } = U \ {a 2 , . . . , a i }. Finally, if x occurs in φ and x V then x = y j for some j ∈ 1 . . m such that b j = a o , with o ∈ 3 . . i , thus s 1 (x) = a o and s 1 (x) = b j = a o-1 , and therefore s 1 (x) ∈ {a 3 , . . . , a i } and s 1 (x) ∈ {a 2 , . . . , a i-1 }. Let s

) def = dom(h) \ {a 2 }, h (a 1 ) def = a 3 and h (x) def = h(x) if x ∈ dom(h ) \ {a 1 }. Note
1 def = s[y j → b j | j ∈ 1 .
. m ]; we show that (U , s 1 , h) and (U, s 1 , h) coincide on every test formula in φ.

= x ≈ y. If x, y ∈ V then the proof is immediate since s 1 and s 1 coincide on x and y. If x ∈ V and y V then s 1 (x) = s 1 (x) ∈ U\{a 2 , . . . , a i } and s 1 (y), s 1 (y) ∈ {a 2 , . . . , a i } hence x ≈ y is false in both structures. The proof is symmetric if x V and y ∈ V. If x, y V then s 1 (x) = a o , s 1 (y) = a o , with s 1 (x) = a o-1 and s 1 (y) = a o -1 . Since the a 1 , . . . , a l are pairwise distinct we have

s 1 (x) = s 1 (y) ⇔ o = o ⇔ o -1 = o -1 ⇔ s 1 (x) = s 1 (y). = alloc(x). If x ∈ V then s 1 (x) = s 1 (x) a 2 Thus s 1 (x) ∈ dom(h) ⇔ s 1 (x) ∈ dom(h) ⇔ s 1 (x) ∈ dom(h ). If x V then s 1 (x) ∈ {a 3 , .
. . , a i } and s 1 (x) ∈ {a 2 , . . . , a i-1 } (with i < l) thus alloc(x) is true in both structures. = x → y. We distinguish several cases.

• If x, y ∈ V then s 1 (x) = s 1 (x) and s 1 (y) = s 1 (y), with s 1 (x) a 2 , hence h(s

1 (x)) = s 1 (y) ⇔ h(s 1 (x)) = s 1 (y) ⇔ h (s 1 (x)) = s 1 (y), thus (U, s 1 , h) | = ⇔ (U , s 1 , h ) | = . • If x, y V then s 1 (x) = a o , s 1 (y) = a o , with s 1 (x) = a o-1 , s 1 (y) = a o -1 and o, o ≥ 3 thus h (s 1 (x)) = s 1 (y) ⇔ o = o -1 ⇔ h(s 1 (x)) = s 1 (y).
• If x ∈ V and y V, then s 1 (y) = a o with s 1 (y) = a o-1 and o ∈ 3 . . i . We distinguish two cases. If x ∈ {x 1 , . . . , x n }, then h(s 1 (x)) {a 1 , . . . , a l } (by Definition 15 (2)) thus h(s 1 (x)) = h (s 1 (x)) s 1 (y), s 1 (y) and is false in both structures.

Otherwise, x = y j , for some j ∈ 1 . . m such that b j {a 3 , . . . , a i }. If b j = a 1 then h(s 1 (x)) = a 2 and h (s 1 (x)) = a 3 , thus h(s Lemma 17. Let ϕ = ∀y 1 , . . . , y m . φ be a prenex formula of SL 1 of free variables x 1 , . . . , x n (with n > 0) where φ is a boolean combination of universe-independent test formulas. If (U, s, h) is a finite minimal model of ϕ then ||U|| ≤ 2n • (m + 3).

1 (x)) = s 1 (y) ⇔ a 2 = s 1 (y) ⇔ a 2 = a o-1 ⇔ o = 3 ⇔ a 3 = s 1 (y) ⇔ h (s 1 (x)) = s (y),
Proof. Let I = (U, s, h) be a minimal finite model of ϕ and let a i = s(x i ) for i = 1, . . . , n. We inductively define a sequence l i (1 ≤ i ≤ n) of natural numbers as follows: l i is the minimal natural number such that either

h l i (a i ) dom(h) or h(h l i (a i )) ∈ {a 1 , . . . , a n } ∪ {h j (a i ) | j ∈ 1 . . l i -1 } ∪ {h j (a k ) | k ∈ 1 . . i -1 , j ∈ 1 . . l k }.
Because the domain of h is finite, the numbers l i always exist, for all i = 1, . . . , n. Note that by construction, given i ∈ 1 . . i , if h j (a i ) h k (a i ) for all k < j and h j (a i ) h k (a p ) k ∈ N for all p < i, then j ≤ l i . Hence, since by Proposition 14, we have U = {h j (s(x i )) | i ∈ 1 . . n , j ∈ N}, we deduce that U = n i=1 {h j (a i ) | j ∈ 0 . . l i }. Furthermore, by definition of l i , all locations h j (a i ), for i ∈ 1 . . n and j ∈ 1 . . l i , are pairwise distinct.

We define the following subsets of U: U

1 def = {a i | i ∈ 1 . . n }, U 2 def = {h l i (a i ) | i ∈ 1 . . n , h l i (a i ) dom(h)}, and U 3 def = {h(h l i (a i )) | i ∈ 1 . . n , h l i (a i ) ∈ dom(h)}. By def- inition, U 2 ∪ U 3 contains at most n elements, thus ||U 1 ∪ U 2 ∪ U 3 || ≤ 2n.
We have that every element c such that there exist a b with h(a) = h(b) = c is in U 3 . Indeed, assume that there exist two such elements a, b ∈ U. Then there exist i, j ∈ 1 . . n , i ∈ 0 . . l i , j ∈ 0 . . l j such that a = h i (a i ) and b = h j (a j ). We assume by symmetry that i ≤ j. Then by definition of l j we must have j = l j , so that h(b) = c ∈ U 3 . The reader may refer to Figure 1 for an illustration. Now, consider a sequence of the form (h j (a i ), . . . , h j (a i )) (with j ≤ j ) containing no element in U 1 ∪ U 2 ∪ U 3 . By definition, this sequence fulfills Conditions 3 and 1 from Definition 15. If the sequence does not fulfill Condition 2, then there exist k ∈ j . . j -1 such that h k+1 (a i ) is a fork element, hence h k+1 (a i ) ∈ U 3 , which contradicts our hypothesis. Consequently, (h j (a i ), . . . , h j (a i )) is a line for (I, ϕ). By Proposition 16 such lines cannot be of length greater than m+2, therefore U\(U 1 ∪U 2 ∪U 3 ) contains at most (m+2)• L elements, where L is the number of sequences (h j (a i ), . . . , h j (a i )) of maximal length not containing elements in U 1 ∪ U 2 ∪ U Corollary 18. The finite and infinite satisfiability problems for formulas of BSR(SL 1 ) are PSPACE-complete.

Proof. PSPACE-hardness follows from the proof that satisfiability of the quantifier free fragment of SL 2 is PSPACE-complete [4, Proposition 5]. Indeed, this proof does not depend on the universe being infinite or the fact that k = 2. There remains to show PSPACE-membership for both problems. Observe that this does not directly follow from Lemmas 4 and 17, because (i) the sets µ inf (φ) and µ fin (φ) are of exponential size hence no efficient algorithm can compute them and, (ii) Lemma 17 only holds for universe-independent formulas. W.l.o.g., we assume that the considered formula contains at least one free variable and is of the form ∀y 1 , . . . , y m . φ. It is sufficient to focus on the finite satisfiability problem. Indeed, by Lemma 4, ∀y 1 , . . . , y m . φ ≡ inf M∈µ inf (¬φ) M. By Theorem 8, ∀y 1 , . . . , y m . φ has an infinite model iff ∀y 1 , . . . , y m . φ ∧ λ n+m has a finite model, where the size of λ n+m is quadratic in n + m. Moreover, since λ n+m is a BSR(SL) formula, ∀y 1 , . . . , y m . φ ∧ λ n+m is also a BSR(SL) formula. Hence infinite satisfiability can be reduced polynomially to finite satisfiability.

Let ψ = M∈µ fin (¬φ) M (note that the size of ψ is exponential w.r.t. that of φ). Let L be the maximal number l such that a test formula |h| ≤ l or |h| ≤ |U|l occurs in µ inf (φ). By Lemma 4, the number L is polynomial w.r.t. size(φ). We guess a structure I = (U, s, h) and check that it is a model of ϕ as follows. We first guess the set C of literals of the form |U| ≤ i, |U| < i, |h| ≤ i, |h| > i, |h| ≤ |U|i, or |h| > |U|i with i ∈ 0 . . L that are true in I. It is clear that ϕ is satisfiable iff ϕ ∪ C is satisfiable for some such set C. Up to redundancy, C contains at most 6 literals (one literal of each kind). With each test formula ∈ C we may associate an equivalent formula γ( ) in BSR(SL1) built on atoms x ≈ y or alloc(x) using the following equivalence statements:

-|h| ≤ i ⇔ ∀x 1 , . . . , x i+1 . dist(x 1 , . . . , x i+1 ) → i+1 j=1 ¬alloc(x j ), -|h| ≤ |U|i ⇔ ∃x 1 , . . . , x i . dist(x 1 , . . . , x i ) ∧ i j=1 ¬alloc(x j ),

-|U| ≤ i ⇔ ∀x 1 , . . . , x i+1 ¬dist(x 1 , . . . , x i+1 ). Let ϑ be the conjunction of all formulas γ( ) where ∈ C. Note that ϑ contains (up to redundancy) at most 3L + 2 existential variables and 3L + 2 universal variables. Now consider the formula ψ obtained from ψ by replacing every test formula such that ∈ C (resp. ∈ C) by (resp. ⊥). Let ϕ be the formula obtained by putting ∀y 1 , . . . , y m . ¬ψ ∧ ϑ in prenex form. It is clear that ϕ is in BSR(SL1) and that all test formulas in ϕ are universe-independent, furthermore ϕ contains at most n = n + (3L + 2) free or existential variables and m = m + (3L + 2) universal variables. Moreover, ϕ ≡ ϕ ∧ ϑ, hence ϕ is satisfiable iff ϕ admits a model satisfying C. By Lemma 17, ϕ is satisfiable iff ϕ admits a model (U, s, h) such that ||U|| ≤ 2n × (m + 3). We may thus check that ϕ is satisfiable by fixing such a set U, guessing the value of s(x) on each variable x free in ϕ, guessing some heap h on U, and checking that (U, s, h) | = C and that (U, s, h) | = ϕ. The former test is easy to perform by counting the number of allocated and nonallocated cells. For the latter test, we check the negation (U, s, h) | = ϕ, by testing that there exists a store s coinciding with s on x 1 , . . . , x n such that (U, s , h) | = ¬φ, i.e., such that (U, s , h) | = M∈µ fin (¬φ) M. To this aim, we guess the value of each variable y i in s , guess a minterm M, check that M ∈ µ fin (¬φ) (which can be done in polynomial space by Lemma 4) and check that (U, s , h) validates every test formula in M (it is clear that this can be done in polynomial time).

Conclusion

We have shown that the prenex fragment of Separation Logic over heaps with one selector, denoted as SL 1 , is decidable in time not elementary recursive. Moreover, the Bernays-Schönfinkel-Ramsey BSR(SL 1 ) is PSPACE-complete. These results settle an open question raised in [START_REF] Echenim | The Bernays-Schönfinkel-Ramsey Class of Separation Logic on Arbitrary Domains[END_REF] and allow one to draw a precise boundary between decidable and undecidable cases inside BSR(SL k ). As far as applications are concerned, the logic BSR(SL 1 ) can be used to reason on singly linked data-structures, where * and - * are used to state dynamic transformations of the heap and the quantifiers are useful to state general properties of the considered data-structure (e.g., to check that a loop invariant is preserved). Theorem 8, relating infinite and finite satisfiability, holds for any k ≥ 1 and we believe that it could pave the way to further decidability results for prenex fragments of SL k .

  y), then we denote by µ(i, a, b) a set containing an arbitrarily chosen element z satisfying P(i, a, b) in the definition of π i (x, y) along with all the children of z, otherwise µ(i, a, b) is empty. Observe that µ(i, a, b) is always finite because the number of children of z in each equivalence class is bounded by 2 + 4 × i + 2 + 1 ≤ 2 + 4 × r + 2 + 1, moreover the number of E-equivalence classes is finite [1, bottom of Page 343]. We show that ϕ admits a finite model I . The set B of elements b such that (U, s[x → b], i) | = δ(x) is finite [1, Page 344, Lines 21-22]. Let Π be the set: Π = {µ(i, a, b) | a, b ∈ B, i ∈ [0, r]}. Since B is finite and every set µ(i, a, b) is finite, Π is also finite.

  for every b ∈ U , since by definition the parent of the (unique) element of ν(b, K) is b. Thus at least one child of b is kept in each equivalence class. Thus the relations E m on elements of U are preserved in the transformation: for every a, b ∈ U , a, b are E m -equivalent in the structure I iff they are equivalent in the structure I . Further, the height of the nodes cannot change. Therefore, for every a, a ∈ U :

3 .Proposition 7 .

 37 ||U \ elems(h)|| ≥ n + ||X|| and ||U \ elems(h)|| ≥ n + ||X||. 4. For all x, y ∈ X, I | = x ≈ y iff I | = x ≈ y. Condition 1 entails that elems(h) ⊆ U ∩ U . We prove that any two SL-structures that are (fv(φ), m)-similar are indistinguishable by any formula φ prefixed by m quantifiers. Let φ = Q 1 x 1 . . . Q m x m . ψ be a prenex SL k formula, with Q i ∈ {∀, ∃} for all i = 1, . . . , m, where ψ is a quantifier-free boolean combination of universe-independent test formulas. If I ∼ m fv(φ) I and I | = φ then I | = φ. Proof. Let I = (U, s, h) and I = (U , s , h ). Assume that I ∼ m fv(φ) I and I | = φ. By Condition 1 in Definition 6 we have h = h . We prove that I | = φ by induction on m.

  , thus necessarily x = x 1 . In this case, s[x 1 → e](x) = e and s [x 1 → e ](x) = e . Since e e by hypothesis, there can be no y ∈ fv(φ) such that s(y) = e because otherwise by construction we would have e = s(y) = s (y) = e . By definition of e we cannot have e ∈ elems(h) either, so e is necessarily in U \ (s (fv(φ)) ∪ elems(h)) and the disjunction e ∈ elems(h) ∨ e ∈ elems(h) cannot hold.• Condition 3 follows from the fact that I ∼ m fv(φ) I because we have m -1 + ||fv(φ) ∪ {x 1 }|| = m + ||fv(φ)||. • We now establish Condition 4. Let x, x ∈ fv(φ) ∪ {x 1 }. If x, x ∈ fv(φ) then s[x 1 → e]and s [x 1 → e ] coincide with s and s respectively on x and x , hence J and J must agree on x ≈ x since I ∼ m fv(φ) I . The result also trivially holds when x = x = x 1 . Now assume that x = x 1 and x x 1 . If e = s(y) for some y ∈ fv(φ), then J | = x ≈ x iff I | = y ≈ x . By definition of e , we also have e = s (y), hence J | = x ≈ x iff I | = y ≈ x . Since both y and x are in fv(φ), we have J | = x ≈ x ⇔ I | = y ≈ x ⇔ I | = y ≈ x ⇔ J | = x ≈ x . If the previous condition does not hold then necessarily e s(x ), and J | = x 1 ≈ x . If e ∈ elems(h), then by definition of e , we have e = e. If J | = x 1 ≈ x then we must have s (x ) = s (x 1 ) = e = e ∈ elems(h), which by Condition 2 entails that s (x ) = s(x ) = e, hence J | = x 1 ≈ x , a contradiction. Finally, if e elems(h), then by definition of e , e cannot occur in s (fv(φ)), thus J | = x 1 ≈ x . -Finally, assume that m ≥ 1 and Q 1 = ∀. Then φ = ∀x 1 . φ . Let φ 2 = ∃x 1 . φ 1 , where φ 1 denotes the nnf of ¬φ . Assume that I | = φ, then I | = φ 2 , because ¬φ ≡ ∃x 1 . ¬φ ≡ ∃x 1 . φ 1 = φ 2 . By the previous case, using the symmetry of ∼ m fv(φ) and the fact that φ and φ 2 have exactly the same free variables and number of quantifiers, we have I | = φ 2 , i.e. I | = φ, a contradiction.

  that s and s coincide on all variables x 1 , . . . , x n free in ϕ since ∀i ∈ 1 . . n , a 2 s(x i ), by Definition 15 (3). Since I is minimal, necessarilyI | = ϕ, thus there exist b 1 , . . . , b m ∈ U such that by letting s 1 def = s [y j → b j | j ∈ 1 . . m ], we have (U , s 1 , h ) | = ¬φ. Since l > m+2and a 1 , . . . , a l are distinct by Definition 15, there exists i ∈ 2 . . l -1 such that a i+1 {b 1 , . . . , b m }. We define a sequence b 1 , . . . , b m ∈ U as follows. For every j ∈ 1 . . m , if there exists o ∈ 3 . . i such that b j = a o , then we let b j def = a o-1 ; otherwise, b j def = b j . Note that b j is well-defined, because a 1 , . . . , a l are distinct, hence there exists at most one o satisfying the above condition.

3 .

 3 Thus ||U|| ≤ (m + 2) • L + 2n. By definition, all such sequences necessarily start by some element h(a), where a ∈ U 1 ∪ U 2 ∪ U 3 , thus there are at most ||U 1 ∪ U 2 ∪ U 3 || ≤ 2n such sequences. Hence L ≤ 2n and ||U|| ≤ 2n • (m + 3).

3 Fig. 1 .

 31 Fig. 1. Heap decomposition example. We have l 1 = 5, l 2 = 1, l 3 = 3 and l 4 = 1. Moreover, U 1 = {a 1 , a 2 , a 3 , a 4 }, U 2 = {u} and U 3 = {u, v, w}.

  2. φ ∧ λ m admits a finite model. As in the previous case, Conditions 1, 4 and 2 trivially hold, and Condition 3 holds since U is infinite and (U, s, h) | = λ m . By Proposition 7, we deduce that (U , s, h) | = φ.

Proof. (1) ⇒ (2): Assume that φ admits an infinite model (U, s, h). Let U be a finite subset of U containing elems(h) and m additional elements. It is clear that (U, s, h) ∼ m ∅ (U , s, h). Indeed, Condition 1 holds since the two structures share the same heap, Conditions 4 and 2 trivially hold since the considered set of variables is empty, and Condition 3 holds since U is infinite and the additional elements in U do not occur in elems(h). Thus (U , s, h) | = φ by Proposition 7, and (U , s, h) | = λ m , by definition of U .

(2) ⇒ (1): Assume that φ ∧ λ m has a finite model (U, s, h). Let U be any infinite set containing U. Again, we have (U, s, h) ∼ m ∅ (U , s, h).

  hence has the same truth value in (U, s 1 , h) and (U , s 1 , h ). If b j a 1 then h (s 1 (x)) = h(s 1 (x)), and s 1 (x) {a 1 , . . . , a i }, thus h(s 1 (x) {a 2 , . . . , a i+1 }, hence is false in both structures.• If y ∈ V and x V then there exists o ∈ 3 . . i such that s 1 (x) = a o-1 and s 1 (x) = a o , with s 1 (y) = s 1 (y) {a 2 , . . . , a i }. We have h (s 1 (x)) = a o+1 and h(s 1 (x)) = a o , thus h (s 1 (x)), h(s 1 (x)) ∈ {a 3 , . . . ,a i+1 }. By definition of i, a i+1 {b 1 , . . . , b m } (since a i+1 {b 1 , . . . , b m } and i + 1 > i), moreover a i+1 s({x 1 , . . . , x n }) by Definition 15 (3). Thus a i+1 s 1 (y). Since s 1 (y) {a 2 , . . . , a i } we deduce that s 1 (y) {a 3 , . . . , a i+1 }, thus is false in both structures. As a consequence, (U , s 1 , h ) and (U, s 1 , h) necessarily coincide on φ, and consequently (U, s 1 , h) | = ¬φ, hence (U, s, h) | = ∀y 1 , . . . , y m . φ which contradicts our hypothesis.

Q 1 x 1 . . . Q n x n . ϕ, where Q 1 , . . . , Q n are the first order quantifiers ∃ or ∀ and ϕ is quantifier-free.

The fragment FO 1 is denoted by [all, (ω), (1)] = in[START_REF] Börger | The Classical Decision Problem[END_REF].

In contrast to most existing work in Separation Logic, we do not assume that U is infinite.

Since the domain of the heap is finite.

For infinite satisfiability, it is enough to forbid positive occurrences of the magic wand containing universally quantified variables only.

8 See [1, Theorem 6.4.19].

Acknowledgments

The authors wish to thank Stéphane Demri, Etienne Lozes and Alessio Mansutti for the insightful discussions during the preparation of this paper.


Mnacho Echenim

Nicolas Peltier

Yanis Sellami

Ilinva: Using Abduction to Generate Loop Invariants

. Experiments show evidence of the practical relevance of our approach.

Introduction

Hoare logic -together with strongest post-conditions or weakest pre-conditions calculi -allow one to verify properties of programs defined by bounded sequences of instructions [START_REF] Hoare | An axiomatic basis for computer programming[END_REF]. Given a pre-condition φ satisfied by the inputs of program P, algorithms exist to compute the strongest formula ψ such that φ {P} ψ holds, meaning that if φ holds initially then ψ is satisfied after P is executed, and any formula ψ that holds after P is executed is such that ψ |= ψ . To check that the final state satisfies some formula ψ , we thus only have to check that ψ is a logical consequence of ψ. However, in order to handle programs containing loops, it is necessary to associate each loop occurring within the program with an inductive invariant. An inductive invariant for a given loop L is a formula that holds every time the program enters L (i.e., it must be a logical consequence of the preconditions of L), and is preserved by the sequence of instructions in L. Testing whether a formula is an inductive invariant is a straightforward task, and the difficulty resides in generating candidate invariants. These can be supplied by the programmer, but this is a rather tedious and time-consuming task; for usability and scalability, it is preferable to generate those formulas automatically when possible. In this paper, we describe a system to generate such invariants in a completely automated way, via abductive reasoning modulo theories, based on the methodology developed in [START_REF] Dillig | Inductive invariant generation via abductive inference[END_REF]. Roughly speaking, the algorithm works as follows. Given a program P decorated with a set of assertions that are to be established, all loops are first assigned the same candidate invariant . These invariants are obviously sound: they hold before the loops and are preserved by the sequence of instructions in the loop; however they are usually not strong enough to prove the assertions decorating the program. They are therefore strengthened by adding hypotheses that are sufficient to ensure that the assertions hold; these hypotheses are generated by a tool that performs abductive inferences, and the strengthened formulas are candidate invariants. Additional strengthening steps are taken to guarantee that these candidates are actual invariants, i.e., that they are preserved by the sequence of instructions in the loop. These steps are iterated until a set of candidate invariants that are indeed inductive is obtained.

We rely on two existing systems to accomplish this task. The first one is Why3 (see, e.g., http://why3.lri.fr/ or [START_REF] Filliâtre | Why3 -where programs meet provers[END_REF]), a well-known and widely-used platform for deductive program verification that is used to compute verification conditions and verify assertions. The second system, GPiD, is designed to generate implicants1 of quantifier-free formulas modulo theories [START_REF] Echenim | A generic framework for implicate generation modulo theories[END_REF]. This system is used as an abductive reasoning procedure, thanks to the following property: if φ |= ψ, finding a hypothesis φ such that φ ∧ φ |= ψ is equivalent to finding φ such that φ |= φ ⇒ ψ. GPiD is generic, since it only relies on the existence of a decision procedure for the considered theory (counter-examples are exploited when available to speed-up the generation of the implicants when available). Both systems are connected in the Ilinva framework. Related Work. A large number of different techniques have been proposed to generate loop invariants automatically, especially on numeric domains [START_REF] Bradley | IC3 and beyond: Incremental, inductive verification[END_REF][START_REF] Bradley | Property-directed incremental invariant generation[END_REF], but also in more expressive logics, for programs containing arrays or expressible using combination of theories [START_REF] Padon | Decidability of inferring inductive invariants[END_REF][START_REF] Beyer | Invariant synthesis for combined theories[END_REF][START_REF] Kovács | Finding loop invariants for programs over arrays using a theorem prover[END_REF][START_REF] Ghilardi | Backward reachability of array-based systems by SMT solving: Termination and invariant synthesis[END_REF][START_REF] Karbyshev | Propertydirected inference of universal invariants or proving their absence[END_REF][START_REF] Kovács | Interpolation and symbol elimination[END_REF]. We only briefly review the main ideas of the most popular and successful approaches. Methods based on abstract interpretations (see, e.g., [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF][START_REF] Miné | The octagon abstract domain[END_REF]) work by executing the program in a symbolic way, on some abstract domain, and try to compute over-estimations of the possible states of the memory after an unbounded number of iterations of the loop. Counter-examples generated from runs can be exploited to refine the considered abstraction [START_REF] Flanagan | Houdini, an annotation assistant for esc/java[END_REF][START_REF] Henzinger | Software verification with blast[END_REF]. The idea is that upon detection of a run for which the assertion is violated, if the run does not correspond to a concrete execution path, then the considered abstraction may be refined to dismiss it.

Candidate invariants can also be inferred by generating formulas of some user-provided patterns and testing them against some particular executions of the program [START_REF] Ernst | Dynamically discovering likely program invariants to support program evolution[END_REF]. Those formulas that are violated in any of the runs can be rejected, and the soundness of the remaining candidates can be checked afterwards. Invariants can be computed by using iterative backward algorithms [START_REF] Suzuki | Implementation of an array bound checker[END_REF], starting from the post-condition and computing weakest pre-conditions until a fixpoint is reached (if any). Other approaches [START_REF] Kapur | A quantifier-elimination based heuristic for automatically generating inductive assertions for programs[END_REF] have explored the use of quantifier elimination to refine properties obtained using a representation of all execution paths.

The work that is closest to our approach is [START_REF] Dillig | Inductive invariant generation via abductive inference[END_REF], which presents an algorithm to compute invariants as boolean combinations of linear constraints over integers. The algorithm is similar to ours, and also uses abduction to strengthen candi-date invariant so that verification conditions are satisfied. The algorithms differ by the way the verification conditions and abductive hypotheses are proceeded: in our approach the conditions always propagate forward from an invariant to another along execution paths, and we eagerly ensure that all the loop invariants are inductive. Another difference is that we use a completely different technique to perform abductive reasoning: in [START_REF] Dillig | Inductive invariant generation via abductive inference[END_REF] is based on model construction and quantifier elimination for Presburger arithmetic, whereas our approach uses a generic algorithm, assuming only the existence of a decision procedure for the underlying theory. This permits to generate invariants expressed in theories that are out of the scope of [START_REF] Dillig | Inductive invariant generation via abductive inference[END_REF].

Contribution. The main contribution is the implementation of a general framework for the generation of loop invariants, connecting the platform Why3 and GPiD. The evaluation demonstrates that the system permits to generate loop invariants for a wide range of theories, though it suffers from a large search space which may induce a large computation time.

Verification Conditions

In what follows, we consider formulas in a base logic expressing properties of the memory and assume that such formulas are closed under the usual boolean connectives. These formulas are interpreted modulo some theory T , where |= T denotes logical entailment w.r.t. T . The memory is modified by programs, which are sequences of instructions; they are inductively defined as follows:

P = empty | I ; P I = base-instruction | assume φ | assert φ | if C then P1 else P2 | while C do P1{φ} end
where P , P 1 and P 2 are programs, C is a condition on the state of the memory, φ is a formula and I is an instruction. Assumptions correspond to formulas that are taken as hypotheses, they are mostly useful to specify pre-conditions. Assertions correspond to formulas that are to be proved. Base instructions are left unspecified, they depend on the target language and application domain; they may include, for instance, assignments and pointer redirection. The formula φ in the while loop is a candidate loop invariant, it is meant to hold every time condition C is tested. In our setting each candidate loop invariant will be set to before invoking Ilinva (except when another formula is provided by, e.g., the user), and the program will iteratively update these formulas. We assume that conditions contain no instructions, i.e., that the evaluation of these conditions does not affect the memory. We write P ∼ P if programs P and P are identical up to the loop candidate invariants.

An example of a program is provided in Figure 1. It uses assignments on integers and usual constructors and functions on lists as base instructions. It contains one loop with candidate invariant (Line 3) and one assertion (Line 6). A location is a finite sequence of natural numbers. The empty location is denoted by ε and the concatenation of two locations and is denoted by . . If is a location and S is a set of locations then .S denotes the set { . | ∈ S}. The set of locations in a program P or in an instruction I is inductively defined as follows:

1 let i ← 1 ; 2 let L ← list(1, nil) ; 3 while unknown() do { } 4 i ← i + 1 ; 5 L ← list(i, L) ; 6 assert head(L) = length(L) ;
-If P is an empty sequence then loc(P) = {0}.

-If P = I ; P then loc(P) = {0} ∪ 0.loc(I) ∪ {(i + 1).p | i ∈ N, i.p ∈ loc(P )}.

-If I is a base instruction or an assumption/assertion, then loc(I) = ∅.

-If I = if C then P 1 else P 2 then loc(I) = 1.loc(P 1 ) ∪ 2.loc(P 2 ).

-If I = while C do P 1 {φ} end then loc(I) = 1.loc(P 1 ).

For instance, a program I 1 ; I 2 where I 1 , I 2 denote base instructions has three locations: 0 (beginning of the program), 1 (between I 1 and I 2 ) and 2 (end of the program). Note that there are no locations within an atomic instruction. The program in Figure 1 has eight locations, namely 0, 1, 2, 2.1.0, 2.1.1, 2.1.2, 3, 4. We denote by P| the instruction occurring just after location in P (if any):

-If P = I ; P then P| 0 = I, P| 0. = I| and P| (i+1). = P | i. . -If I = if C then P 1 else P 2 then I| 1. = P 1 | and I| 2. = P 2 | . -If I = while C do P 1 {φ} end then I| 1. = P 1 | .
Note that → P| is a partial function, since locations denoting the end of a sequence do not correspond to an instruction. We denote by lloc(P) the set of locations in P such that P| is a loop and by loops(P) = {P| | ∈ lloc(P)} the set of loops occurring in P. For instance, if P denotes the program in Figure 1, then P| 1 is let L ← list(1, nil), and lloc(P) = {2}.

We denote by < the usual order on locations: < iff either there exist numbers i, j and locations 1 , 2 , 3 such that = 1 .i. 2 , = 1 .j. 3 and i < j, or there exists a location such that = . . We assume the existence of a procedure VCgen that, given a program P, generates a set of verification conditions for P. These verification conditions are formulas of the form φ ⇒ ψ, each of which is meant to be valid. Given a program P, the set of conditions VCgen(P) can be decomposed as follows:

1. Assertion conditions, which ensure that the assertion formulas hold at the corresponding location in the program. These conditions also include additional properties to prevent memory access errors, e.g., to verify that the index of an array is within the defined valid range of indexes. The set of assertion conditions for program P is denoted by VCgen a (P). 2. Propagation conditions, ensuring that loop invariants do propagate. Given a loop L occurring at position in program P, we denote by VCgen ind (P, ) the set of assertions ensuring that the loop invariant for L propagates.

wp(φ, empty) = φ wp(φ, I ; P) = wp(wp(φ, P), I)

wp(φ, assume φ ) = φ ⇒ φ wp(φ, assert φ ) = φ ∧ φ wp(φ, if C then P1 else P2) = C ⇒ wp(φ, P1) ∧ ¬C ⇒ wp(φ, P2) wp(φ, while C do P1{ψ} end) = ψ ∧ ∀x. (ψ ⇒ wp(ψ, P1)) ∧ ∀x. (ψ ∧ ¬C ⇒ φ)
The formula in the last line states that the loop invariant holds when the loop is entered, that it propagates and that it entails the formula φ . The vector x denotes the vector of variables occurring in P1.

Fig. 2:

A Weakest Precondition Calculus sp(φ, empty) = φ sp(φ, I ; P ) = sp(sp(φ, I), P ) sp(φ, assume φ ) = φ ∧ φ sp(φ, assert φ ) = φ sp(φ, if C then P1 else P2) = sp(φ ∧ C, P1) ∨ sp(φ ∧ ¬C, P2) sp(φ, while C do P1{ψ} end) = ψ ∧ ¬C
sp(φ, P) describes the state of the memory after P. The conditions corresponding to loops are approximated by using the provided loop invariants (the corresponding verification conditions are not stated).

Fig. 3: A Strongest Postcondition Calculus

3. Loop pre-conditions, ensuring that the loop invariants hold when the corresponding loop is entered. Given a loop L occurring at position in program P, we denote by VCgen init (P, ) the set of assertions ensuring that the loop invariant holds before loop L is entered.

Thus, VCgen(P) = VCgen a (P) ∪ ∈lloc(P) (VCgen ind (P, ) ∪ VCgen init (P, )) . Such verification conditions are generally defined using standard weakest precondition or strongest post-condition calculi (see, e.g., [START_REF] Dijkstra | A Discipline of Programming[END_REF]), where loop invariant are used as under-approximations. Formal definitions are recalled in Figures 2 and3 (the definition for the basic instructions depends on the application language and is thus omitted). For the sake of readability, we assume, by a slight abuse of notation, that the condition C is also a formula in the base logic. This permits to define the goal of the paper in a more formal way: our aim is to define an algorithm that, given a program P, constructs a program P ∼ P (i.e., constructs loop invariants for each loop in P) such that VCgen(P ) only contains valid formulas. Note that all the loops and invariants must be handled globally since verification conditions depend on one another.

Algorithm 1: GPiD(φ, M, A, P)

1 if M unsatisfiable (modulo T ) or ¬P(M ) then 2 return ∅; 3 if M |= φ then 4 return {M }; 5 let m be a model of {¬φ} ∪ M ; 6 let φ = Simplify(φ, M ); 7 let A = {l ∈ A | M ∪ ¬φ |=T l, M |=T l c }; 8 foreach l ∈ A such that m |= l do 9 let A l = {l ∈ A | l < l ∧ m |= l } ∪ {l ∈ A | l < l }; 10 let P l = GPiD(φ, M ∪ {l} , A l , P);
11 return l∈A P l ;

Abduction

As mentioned above, abductive reasoning will be performed by generating implicants. Because it would not be efficient to blindly generate all implicants of a formula, this generation is controlled by fixing the literals that can occur in an implicant. We thus consider a set A of literals in the considered logic, called the abducible literals.

Definition 1. Let φ be a formula. An A-implicant of φ (modulo T ) is a con- junction (or set) of literals l 1 ∧ • • • ∧ l n such that l i ∈ A, for all i ∈ 1 . . n and l 1 ∧ • • • ∧ l n |= T φ.
We use the procedure GPiD described in [START_REF] Echenim | A generic framework for implicate generation modulo theories[END_REF] to generate A-implicants. A simplified version of this procedure is presented in Algorithm 1. A call to the procedure GPiD(φ, M, A, P) is meant to generate A-implicants of φ that: (i) are of the form M ∪ A , for some A ⊆ A; (ii) are as general as possible; and (iii) satisfy property P. When M itself is not an A-implicant of φ, a subset of relevant literals from A is computed (Line 7), and for each literal in this subset, a recursive call is made to the procedure after augmenting M with this literal and discarding all those that become irrelevant (Lines 9 and 10). In particular, the algorithm is parameterized by an ordering < on abducible literals which is used to ensure that sets of hypotheses are explored in a non-redundant way. The algorithm relies on the existence of a decision procedure for testing satisfiability in T (Line 1). In practice, this procedure does not need terminating or complete 2 , e.g., it may be called with a timeout (any "unknown" result is handled as "satisfiable"). At Line 8, a model of the formula {¬φ} ∪ M is used to prune the search space, by dismissing some abducible literals. In practice, no such model may be available, either because no model building algorithm exists for the considered theory or because of termination issues. In this case, no such pruning is performed. Property P denotes an abstract property of sets of literals. It is used to control the form of generated A-implicants, it is for example possible to force the algorithm to only generate A-implicants with a fixed maximal size. For Theorem 2 to hold, it is simply required that P be closed under subsets, i.e., that for all sets of abducible literals B and C, B ⊆ C ∧ P(C) ⇒ P(B).

Compared to [START_REF] Echenim | A generic framework for implicate generation modulo theories[END_REF], details that are irrelevant for the purpose of the present paper are skipped and the procedure has been adapted to generate A-implicants instead of implicates (implicants and implicates are dual notions).

Theorem 2 ( [START_REF] Echenim | A generic framework for implicate generation modulo theories[END_REF]). The call GPiD(φ, ∅, A, P) terminates and returns a set of A-implicants of φ satisfying P. Further, if P is closed under subsets, then for every A-implicant I of φ satisfying P, there exists I ∈ GPiD(φ, ∅, A, P) such that I |= T I .

This procedure also comes with generic algorithms for pruning redundant Aimplicants i.e., for removing all A-implicants I such that there exist another A-implicant I such that I |= T I , see [START_REF] Echenim | A generic framework for implicate generation modulo theories[END_REF]Section 4].

Generating Loop Invariants

In this section, we present an algorithm for the generation of loop invariants. As explained in Section 2, we distinguish between 3 kinds of verification conditions, which will be handled in different ways: assertion and propagation conditions; and loop pre-conditions. As can be seen from the rules in Figure 2, loop invariants can occur as antecedents in verification conditions, this is typically the case when a loop occurs just before an assertion in some execution path. In such a situation, we say that the considered condition depends on loop L. When a condition depends on a loop, a strengthening of the loop invariant of loop L yields a strengthening of the hypotheses of the verification condition, i.e., makes the condition less general (easier to prove).

This principle is used in Algorithm 2, which we briefly describe before going into details. Starting with a program P in which it is assumed that every loop invariant is inductive, the algorithm attempts to recursively generate invariants that make all assertion conditions in P valid. It begins by selecting a non-valid formula φ from VCgen a (P) and a location ∈ lloc(P) such that φ depends on , then generates a set of hypotheses that would make φ valid (Line 4). For each such hypothesis ξ, a loop location such that ≤ is selected, and a formula ξ that is a weakest precondition at causing ξ to hold at location is computed (Line 7). This formula is added to the invariant of the loop at location (Line 8), so that if this invariant was ψ, the new candidate invariant is ξ ∧ψ. If ξ does not hold before entering the loop then ξ is discarded (Line 9); otherwise, the program attempts to update the other loop invariants to ensure that ξ propagates (Line 10). When this succeeds, a recursive call is made with the updated invariants (Line 12) to handle the other non-valid assertion conditions.

Procedure Abduce(φ) (invoked Line 4 of Algorithm 2) is described in Algorithm 3. It generates formulas ξ that logically entail φ; it is used to generate the candidate hypotheses for strengthening. It first extracts a set of abducible Algorithm 3: Abduce(Formula φ, Program P, Location )

1 let A ←-GetAbducibles(φ) ; 2 let A ←-{l | l ∈ A ∧ φ |=T l} ; 3 let Ξ ←-GPiD(φ, ∅, A, P)) ; 4 let Ξ ←-{ξ1 ∨ • • • ∨ ξn | n ∈ N, ξi ∈ Ξ} ; 5 return Ξ
literals A by collecting variables and symbols from the program and/or from the theory T and combining them to create literals up to a certain depth (procedure GetAbducibles at Line 1). To avoid any redundancy, this task is actually done in two steps: a set of abducible literals for the entire program is initially constructed (this is done once at the beginning of the search), and depending on the considered program location, a subset of these literals is selected. The abducible literals that are logically entailed by φ modulo T are filtered out (Line 2), and procedure GPiD is called to generate A-implicants of φ. Finally, A-implicants are combined to form disjunctive formulas. Note that another way of generating disjunction of literals would be to add these disjunction in the initial set of abducible literals, but this solution would greatly increase the search space.

Each of the hypotheses ξ generated by Abduce(φ) is used to strengthen the invariant of a loop occurring at position ≤ (Line 8 in Algorithm 2). The strengthening formula is computed using the Weakest Precondition Calculus on ξ, on a program obtained from P by ignoring all loops between and , since they have corresponding invariants. To this purpose we define a function bp(φ, P, , ) which, for positions ≤ , back-propagates abductive hypotheses from a location to (see Figure 4). This is done by extracting the part of path(P, , ) = empty path(P, , .(i + 1)) = path(P, , .i) • P| .i if ≤ .i path(P, , .0) = path(P, , ) if ≤ path(P, .i. , .(i + 1)) = path(P, .i. , .i.m) m = max{j | .i.j ∈ loc(P)} bp(φ, P, , ) = wp(φ, P ) if P = path(RmLoops(P), , ) fp(φ, P, , ) = sp(φ, P ) if P = path(RmLoops(P), , )

RmLoops(P) denotes the program obtained from P by removing all while instructions and • denotes the concatenation operator on programs.

Fig. 4 the code path(P, , ) between the locations and while ignoring loops, and computing the weakest precondition corresponding to this part of the code and the formula φ.

The addition of hypothesis ξ to the invariant of the loop at position ensures that the considered assertion φ holds, but it is necessary to ensure that this strengthened invariant is still inductive. This is done as follows. Line 9 of Algorithm 2 filters away all candidates for which the precondition before entering the loop is no longer valid, and Algorithm 4 ensures that the candidate still propagates. This algorithm behaves similarly to Algorithm 2 (testing the verification conditions in VCgen ind (P, ) instead of those in VCgen a (P)), except that it strengthens the invariants that correspond either to the considered loop, or to other loops occurring within it (in the case of nested loops). Note that in this case, properties must be propagated forward, from location to the actual location of the strengthened invariant, using a Strongest Postcondition Calculus (Function fp(φ, P, , ) in Figure 4). This technique avoids considering hypotheses that do not propagate.

When applied on the program in Figure 1, Ilinva first sets the initial invariant of the loop to and considers the assertion φ : head(L) = length(L). As the entailment |= φ does not hold, it will call GPiD to get an implicant of ⇒ φ. Assume that GPiD returns the (trivial) solution φ. As φ indeed holds when the loop is entered3 , Ilinva will add φ to the invariant of the loop and call Ind. Since φ does not propagate Ind will further strengthen the invariant, yielding, e.g., the correct solution: φ ∧ i = head(L).

The efficiency of Algorithm 2 crucially depends on the order in which candidate hypotheses are processed at Line 5 for the strengthening operation. The heuristic used in our current implementation is to try the simplest hypotheses with the highest priority. Abducible atoms are therefore ordered as follows: first boolean variables, then equations between variables of the same sort, then applications of predicate symbols to variables (of the appropriate sorts) and finally deep literals involving function symbols (up to a certain depth). In every case, negative literals are also considered, with the same priority as the corresponding atom. Similarly, unit A-implicants are tested before non-unit ones, and single A-implicants before disjunctions of A-implicants. In the iteration on line 6 of Algorithm 2, the loops that are closest to the considered assertions are considered first. Due to the number of loops involved, numerous parameters are used to control the application of the procedures, by fixing limits on the number of abducible literals that may be considered and on the maximal size of A-implicants. When a call to Ilinva fails, these parameters are increased, using an iterative deepening search strategy. The parameter controlling the maximal number of A-implicants in the disjunctions (currently either 1 or 2) is fixed outside of the loop as it has a strong impact on the computation cost.

The following theorem states the main properties of the algorithm.

Theorem 3. Let P be a program such that VCgen ind (P, ) and VCgen init (P, ) are valid for all ∈ lloc(P). If Ilinva (P) terminates and returns a program P other than fail, then P ∼ P and VCgen(P ) is valid modulo T . Furthermore, if the considered set of abducible literals is finite ( i.e., if there exists a finite set A such that GetAbducibles(φ) ⊆ A for all formulas φ), then Ilinva (P) terminates.

Proof. The proof is provided in the extended version4 .

Implementation

Overview

The Ilinva algorithm described in Section 4 has been implemented by connecting Why3 with GPiD. A workflow graph of this implementation is detailed in the extended paper. Note that both systems themselves call external SMT solvers to check the satisfiability of formulas. In particular, the GPiD toolbox is easy to plug to any SMTlib2-compliant SMT solver. The framework is actually generic, in the sense that it could be plugged with other systems, both to generate and verify proof obligations and to strengthen loop invariants. It is also independent of the constructions used for defining the language: other constructions (e.g., for loops) can be considered, provided they are handled by the program verification framework.

Given an input program written in WhyML, Why3 generates a verification condition the validity of which will ensure that all the asserted properties are verified (including additional conditions related to, e.g., memory safety) This initial verification condition is split by Why3 into several subtasks. These conditions are enriched with all appropriate information (e.g., theories, axioms,. . . ) and sent to external SMT solvers to check satisfiability. The conditions we are interested in are those linked to the proofs of the program assertions, as well as those ensuring that the candidate loop invariants are inductive. In our implementation, Why3 is taken as a black box, and we merely recover the files that are passed from Why3 to the SMT solvers, together with additional configuration data for the solvers we can extract from Why3. If the proof obligation fails, then we relate the file to the corresponding assertion in the WhyML program and extract the set of abducible literals as explained in Section 4, restricting ourselves to symbols corresponding to WhyML variables, functions and predicates. We then tune the SMTlib2 file to adapt it for computations by GPiD and invoke GPiD with the same SMT-solver as the one used by Why3 to check satisfiability, as the problem is expected to be optimized/configured for it. We also configure GPiD to skip the exploration of subtrees that will produce candidate invariants that do not satisfy the loop preconditions. GPiD returns a stream of solutions to the abductive reasoning problem. We then backward-translate the formulas into the WhyML formalism and use them to strengthen loop invariants. For efficiency, the systems run in parallel: the generation of abductive hypotheses (by GPiD, via the procedure Abduce) and their processing in WhyML (via Ilinva) is organized as a pipe-line, where new abduction solutions are computed during the processing of the first ones.

To bridge Ilinva and Why3, we had to devise an interface, which is able to analyze WhyML programs and to identify loop locations and the corresponding invariants. It invokes Why3 to generate and prove the associated verification tasks, and it recovers the failed ones. The library also includes tools to extract and modify loop invariants, to extract variables and reference variables in WhyML files, as well as types, predicates and functions, and wrappers to call the Why3 executable and external tools, and to extract the files sent by WhyML to SMTsolvers.

Distribution

The Abdulot framework is available on GitHub [START_REF]Abdulot framework/GPiD-Ilinva tool suite[END_REF]. It contains an revamped interface to the GPiD libraries and algorithm, a generic library of the Ilinva algorithm automatically plugged with GPiD, the code interface for Why3 and the related executables. GPiD interfaces and related executables are generated for CVC4, Z3 and AltErgo5 via their SMTlib2 interface. Note that the SMT solvers are not provided by our framework, they must be installed separately (all versions with an SMTlib2-compatible interface are supported). Additional interfaces and executables can be produced using C++ libraries for MiniSAT, CVC4 and Z3 if their supported version is available 6 .

The framework also provides libraries and toolbox executables to work with abducible files, C++ libraries to handle WhyML files, helpers for the generation of abducible literals out of SMTlib2 files, and an extensive lisp parser. It also includes a documentation, which explains in particular how to extend it to other solvers and program verification framework. All the tools can be compiled using any C++ 11 compliant compiler. The whole list of dependencies is available in the documentation, as well as a dependency graph for the different parts of the framework.

Experiments

We use benchmarks collected from several sources [START_REF] Dillig | Inductive invariant generation via abductive inference[END_REF][START_REF]Invgen tool[END_REF][START_REF]Neclabs necla verification benchmarks[END_REF][START_REF]Satconv benchmarks[END_REF],1,2,3] (see also [START_REF]Abdulot framework/GPiD-Ilinva tool suite[END_REF] for a more detailed view of the benchmark sources), with additional examples corresponding to standard algorithms for division and exponentiation (involving lists, arrays, and non linear arithmetic). Some of these benchmarks have been translated7 from C or Java into WhyML. In all cases, the initial invariant associated with each loop is . We used Z3 for the benchmarks containing real arithmetic, AltErgo for lists and arrays and CVC4 in all the other cases. All examples are embedded with the source of the Ilinva tool.

Results

We ran Ilinva on each example, first without disjunctive invariants (i.e., taking n = 1 in Procedure Abduce) then with disjunctions of size 2. The results are reported in Figure 5. For each example, we report whether our tool was able generate invariants allowing Why3 to check the soundness of all program assertions before the timeout, in which case we also report the time Ilinva took to do so (columns T(C) when generating conjunctions only and T(D) when generating implicants containing disjunctions). We also report the number of candidate invariants that have been tried (columns C(D) and C(D)) and the number of abducible literals that were sent to the GPiD algorithm (column Abd). Note that the number of candidate invariants does not correspond to the number of SMT calls that are made by the system: those made by GPiD to generate these candidates are not taken into account. The timeout is set to 20 min. For some of the examples that we deemed interesting, we allowed the algorithm to run longer. We report those cases by putting the results between parentheses. Light gray cells indicate that the program terminates before the timeout without returning any solution, and dark gray cells indicate that the timeout was reached. Empty cells mean that the tool could not generate any candidate invariant. The last column of both tables report the time Why3 takes to prove all the assertions of an example when correct invariants are provided.

The tests were performed on a computer powered by a dual-core Intel i5 processor running at 1.3GHz with 4 GB of RAM, under macOS 10.14.3. We used Why3 version 1.2.0 and the SMT solvers AltErgo (version 2.2.0), CVC4 (prerelease of version 1.7) and Z3 (version 4.7.1).

An essential point concerns the handling of local solver timeouts. Indeed, most calls to the SMT solver in the abductive reasoning procedure will involve satisfiable formulas, and the solvers usually take a lot of time to terminate on such formulas (or in the worst case will not terminate at all if the theory is not decidable, e.g., for problems involving first-order axioms). We thus need to set a timeout after which a call will be considered as satisfiable (see Section 3). Obviously, we neither want this timeout to be too high as it can significantly increase computation time, nor too low, since it could make us miss solutions. We decided to set this timeout to 1 second, independently of the solver used, after measuring the computation time of the Why3 verification conditions already satisfied (for which the solver returns unsat) across all benchmarks. We worked under the assumption that the computation time required to prove the other verification conditions when possible would be roughly similar.

Discussion

As can be observed, Ilinva is able to generate solutions for a wide range of theories, although the execution time is usually high. The number of invariant candidates is relatively high, which has a major impact on the efficiency and scalability of the approach.

When applied to examples involving arithmetic invariants, the program is rather slow, compared to the approach based on minimization and quantifier elimination [START_REF] Dillig | Inductive invariant generation via abductive inference[END_REF]. This is not surprising, since it is very unlikely that a purely generic approach based on a model-based tree exploration algorithm involving many calls to an SMT solver can possibly compete with a more specific procedure exploiting particular properties of the considered theory. We also wish to emphasize that the fact that our framework is based on an external program verification system (which itself calls external solvers) involves a significant overcost compared to a more integrated approach: for instance, for the Oxy examples (taken from [START_REF] Dillig | Inductive invariant generation via abductive inference[END_REF]), the time used by Why3 to check the verification conditions once the correct invariants have been generated is often greater than the total time reported in [START_REF] Dillig | Inductive invariant generation via abductive inference[END_REF] for computing the invariants and checking all properties.

Fig. 5: Experimental Results

Of course, our choice also has clear advantages in terms of genericity, generality and evolvability. When applied to theories that are harder for SMT solvers, the algorithm can still generate satisfying invariants. However, due to the high number of candidates it tries, combined with the heavy time cost of a verification (which can be several seconds), it may take some time to do so.

The number of abducible literals has a strong impact on the efficiency of the process, leading to timeouts when the considered program contains many variables or function/predicate symbols. It can be observed that the abduction depth is rather low in all examples (1 or 2).

Our prototype has some technical limitations that have a significant impact on the time cost of the execution. For instance, we use SMTlib2 files for communication between GPiD and CVC4 or Z3, instead of using the available APIs. We went back to this solution, which is clearly not optimal for performance, because we experienced many problems coping with the numerous changes in the specifications when updating the solvers to always use the latest versions. The fact that Why3 is taken as a black box also yields some time consumption, first in the (backward and forward) translations (e.g., to associate program variables to their logical counterparts), but also in the verification tasks, which have to be rechecked from the beginning each time an invariant is updated. Our aim in the present paper was not to devise an efficient system, but rather to assess the feasability and usefulness of this approach. Still, the cost of the numerous calls to the SMT solvers and the size of the search tree of the abduction procedure remain the bottleneck of the approach, especially for hard theories (e.g., nonlinear arithmetics) for which most calls with satisfiable formulas yield to a local timeout (see Section 6.1).

Conclusion and Future Work

By combining our generic system GPiD for abductive reasoning modulo theories with the Why3 platform to generate verification conditions, we obtained a tool to check properties of WhyML programs, which is able to compute loop invariants in a purely automated way.

The main drawback of our approach is that the set of possible abducible literals is large, yielding a huge search space, especially if disjunctions of Aimplicants are considered. Therefore, we believe that our system in its current state is mainly useful when used in an interactive way. For instance, the user could provide the properties of interest for some of the loops and let the system automatically compute suitable invariants by combining these properties, or the program could rely on the user to choose between different solutions to the abduction problem before applying the strengthening. Beside, it is also useful for dealing with theories for which no specific abductive reasoning procedure exists, especially for reasoning in the presence of user-defined symbols or axioms.

In the future, we will focus on the definition of suitable heuristics for automatically selecting abducible literals and ordering them, to reduce the search space and avoid backtracking. The number of occurrences of symbols should be taken into account, as well as properties propagating from previous invariant strengthening. A promising approach is to use dynamic program analysis tools to select relevant abducibles. It would also be interesting to adapt the GPiD algorithm to explore the search space width-first, to ensure that simplest solutions are always generated first. Another option is to give Ilinva a more precise control on the GPiD algorithm, e.g., to explore some branches more deeply, based on information related to the verification conditions. GPiD could also be tuned to generate disjunctions of solutions in a more efficient way.

From a more technical point of view, a tighter integration with the Why3 platform would certainly be beneficial, as explained in Section 6.2. The framework could be extended to handle procedures and functions (with pre-and -post conditions).

A current limitation of our tool is that it cannot handle problems in which Why3 relies on a combination of different solvers to check the desired properties. In this case, Ilinva cannot generate the invariants, as the same SMT solver is used for each abduction problem (trying all solvers in parallel on every problem would be possible in theory but this would greatly increase the search space). This problem could be overcome by using heuristic approaches to select the most suited solver for a given problem.

From a theoretical point of view, it would be interesting to investigate the completeness of our approach. It is clear that no general completeness result possibly holds, due to usual theoretical limitations, however, if we assume that a program P ∼ P such that VCgen(P ) is valid exists, does the call Ilinva(P) always succeed? This of course would require that the invariants in P can be constructed from abducibles occurring in the set returned by the procedure GetAbducibles.

Fig. 1 :

 1 Fig. 1: A simple program on lists It contains one loop for which we will generate an invariant.A location is a finite sequence of natural numbers. The empty location is denoted by ε and the concatenation of two locations and is denoted by . . If is a location and S is a set of locations then .S denotes the set { . | ∈ S}. The set of locations in a program P or in an instruction I is inductively defined as follows:

Algorithm 2 : 9 if

 29 Ilinva (Program P)1 if all formulas in VCgen a (P) are valid then 2 return P;3 let φ be a non valid formula in VCgen a (P), depending on a loop at location ; 4 let Ξ ←-Abduce(φ, P, ); 5 foreach ξ ∈ Ξ do 6 foreach ∈ lloc(P) such that ≤ do 7 let ξ ←-bp(ξ, P, , ); 8 let P ξ ←-Strengthen(P, , ξ ) ; VCgen init (P ξ , ) is valid then 10 let P ξ ←-Ind(P ξ , ) ; 11 if P ξ = fail then 12 let P ξ ←-Ilinva(P ξ ); 13 if P ξ = fail then 14 return P ξ ; 15 return fail ;

:

  Backward and Forward Propagation of Abductive Hypotheses

Algorithm 4: Ind (Program P, Location ) 1 if all formulas in VCgen ind (P, ) are valid then 2 return P; 3 let φ be a non-valid formula in VCgen ind (P, ) ; 4 let Ξ ←-Abduce(φ, P, ); 5 foreach ξ ∈ Ξ do 6 foreach ∈ lloc(P) such that is a prefix of (with possibly = ) do 7 let ξ ←-fp(ξ, P, , ); 8 let P ξ ←-Strengthen(P, , ξ ) ; 9 if VCgen init (P ξ , ) is valid then 10 let P ξ ←-Ind(P ξ , ) ; 11 if P ξ = fail then 12 return P ξ ; 13 return fail ;

An implicant of a formula ψ is a formula φ such that φ |= ψ. It is the dual notion of that of implicates

However, Theorem 2 only holds if the proof procedure is terminating and complete.

This can be checked by computing the weakest precondition of φ w.r.t. Lines 1, 2. The obtained formula is head(list(1, nil)) = length(list(1, nil)) which is equivalent to (w.r.t. the usual definitions of list and head).

https://arxiv.org/abs/1906.11033

Those are the three solvers the Why3 documentation recommends to work with as an initial setup. (see also http://why3.lri.fr/@External Provers.)

The AltErgo interface provided by the tool uses an SMTlib2 interface that is under heavy development and that, in practice, does not work well with the examples we send it.

The translation was done by hand.