Josselin Giet

Félix Ridoux

Xavier Rival

A Product of Shape and Sequence Abstractions

Keywords: ∃α l, αr, v

Traditional separation logic-based shape analyses utilize inductive summarizing predicates so as to capture general properties of the layout of data-structures, to verify accurate manipulations of, e.g., various forms of lists or trees. However, they also usually abstract away contents properties, so that they may only verify memory safety and invariance of data-structure shapes. In this paper, we introduce a novel abstract domain to describe sequences of values of unbounded size, and track constraints on their length and on extremal values contained in them. We define a reduced product of such a sequence abstraction together with an existing shape abstraction so as to infer both shape and contents properties of data-structures. We report on the implementation of the sequence domain, its integration into a static analyzer for C code, and we evaluate its ability to verify partial functional correctness properties for list and tree algorithms.

   

&t → α0 * &c → α1 * α0.l → α1 * α0.d → δ * α0.r → α2 * trees(α1, S l ) * trees(α2, Sr)    

Introduction

Dynamically allocated data-structures based on lists, trees or graphs are common due to their flexibility as containers. However, programs using them are notoriously difficult to get right, especially in presence of destructive updates. Indeed, the correctness of such programs relies on a wide spectrum of properties that comprise memory safety (the absence of illegal pointer operations such as the dereference of a null pointer), the preservation of structural invariants like acyclicity, and subtle functional properties and relationships between the structure layout and its contents such as sortedness. For instance, let us consider a program that inserts an element in a binary search tree. First, it should not cause any runtime error or memory leak. Second, it should not create a cycle or break the tree structure. Third, it should preserve the binary search tree property and be functionally correct, namely ensure that the elements in the tree after insertion are the same as before plus the new element, inserted at the correct position, with respect to the order. | ∃α l , αr, δ, α.l → α l * α.r → αr * α.d → δ * tree(α l ) * tree(αr) ∧ α ̸ = 0x0 trees(α, S) := | emp ∧ α = 0x0

| ∃α l , αr, δ, S l , Sr, α.l → α l * α.r → αr * α.d → δ * trees(α l , S l ) * trees(αr, Sr)

∧ α ̸ = 0x0 ∧ S = S l .[δ].Sr Fig. 1. A C tree data-type and associated inductive summarizing predicates

Abstract interpretation [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] provides a general framework to build a sound static analysis from a basic semantics and an abstraction relation, and to verify semantic properties. Notably, it has been applied to verify numerical properties [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF][START_REF] Jeannet | Apron: A library of numerical abstract domains for static analysis[END_REF], the absence of runtime errors [START_REF] Blanchet | A static analyzer for large safety-critical software[END_REF], string properties [START_REF] Dor | Cssv: towards a realistic tool for statically detecting all buffer overflows in c[END_REF][START_REF] Arceri | Relational string abstract domains[END_REF], array properties [START_REF] Gopan | A framework for numeric analysis of array operations[END_REF][START_REF] Gulwani | Lifting abstract interpreters to quantified logical domains[END_REF][START_REF] Halbwachs | Discovering properties about arrays in simple programs[END_REF][START_REF] Cousot | A parametric segmentation functor for fully automatic and scalable array content analysis[END_REF], liveness properties [START_REF] Urban | The abstract domain of segmented ranking functions[END_REF], and security properties [START_REF] Assaf | Hypercollecting semantics and its application to static analysis of information flow[END_REF][START_REF] Ferrara | Security analysis of the OWASP benchmark with julia[END_REF][START_REF] Distefano | Scaling static analyses at facebook[END_REF]. Several families of shape analyses have also been designed to infer properties of programs manipulating dynamic data-structures, including TVLA [START_REF] Sagiv | Solving shape-analysis problems in languages with destructive updating[END_REF] and shape analyses based on separation logic [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF]. They can reason over structures like lists [START_REF] Calcagno | Footprint analysis : A shape analysis that discovers preconditions[END_REF][START_REF] Calcagno | Compositional shape analysis by means of bi-abduction[END_REF] or more general families of structures with an inductive layout [START_REF] Chang | Relational inductive shape analysis[END_REF][START_REF] Holík | Fully automated shape analysis based on forest automata[END_REF] such as binary trees. However, few shape analyses reason not only about the layout of data-structures but also about their contents, so as to verify, e.g., that a container consists of the expected collection of elements with the expected multiplicity. While [START_REF] Li | Shape analysis for unstructured sharing[END_REF][START_REF] Cox | Automatic analysis of open objects in dynamic language programs[END_REF] handle set predicates, they do not track properties related to element multiplicities or order. Similarly, [START_REF] Liu | Automatic verification of embedded system code manipulating dynamic structures stored in contiguous regions[END_REF] handles sorting properties of specific families of composite structures in arrays but does not consider general lists or trees. The analyses presented in [START_REF] Bouajjani | Accurate invariant checking for programs manipulating lists and arrays with infinite data[END_REF][START_REF] Bouajjani | Abstract domains for automated reasoning about list-manipulating programs with infinite data[END_REF][START_REF] Bouajjani | On inter-procedural analysis of programs with lists and data[END_REF] precisely abstract singly-linked lists storing numerical data. They compute numerical properties over these data such as "variable x is the sum of all elements in list l", or relation between element values and indexes to express sorting. However, it does not handle trees or doubly linked lists. Therefore, in this paper, we seek for an abstraction of data-structure contents that can verify complex invariants (e.g., involving elements orders or multiplicities) as well as some functional properties (like sorting). To illustrate our approach, we consider the classical tree type definition shown in Figure 1 and assume that we only consider acyclic instances. The inductive predicate tree summarizes valid memory regions storing exactly a complete and acyclic tree. More precisely, the predicate tree(α) either describes an empty tree (then, α is the null pointer), or a memory region where α points to a valid tree block, the l and r fields of which point to the roots of disjoint (possibly empty) subtrees, as expressed by predicates tree(α l ) and tree(α r ). Note that separating conjunction * [52] combines disjoint memory regions. A basic region is either an atomic cell described by a points-to predicate such as α.d → δ or an instance of some inductive predicate. While predicate tree describes the layout of memory cells and pointers, it does not convey any information about their contents. By contrast, tree s extends tree with an additional symbolic parameter S to expose the sequence of values stored in the tree, read from left to right. When the tree is empty, so is its sequence of elements. The sequence stored in a non-empty tree is obtained by first considering the left subtree, then the contents of the root node and finally the right tree. If we additionally require the elements of S be sorted, then tree s (α, S) describes binary search trees with root α.

An advantage of this approach is that it allows to split the abstraction into two rather independent components, namely a separation logic based abstraction of the data-structures and another abstraction for properties of sequences of values stored in them. While [START_REF] Li | Shape analysis for unstructured sharing[END_REF] extends inductive predicates in a similar manner, it only supports set constraints. Therefore, we introduce a new abstract domain devoted to the representation of constraints over sequences. Existing sequence abstractions typically rely on regular expressions or finite automata [START_REF] Midtgaard | A parametric abstract domain for latticevalued regular expressions[END_REF][START_REF] Arceri | An automata-based abstract semantics for string manipulation languages[END_REF][START_REF] Negrini | Twinning automata and regular expressions for string static analysis[END_REF]. More recently, [START_REF] Arceri | Relational string abstract domains[END_REF] extends such an abstraction with sub-string, length, and element position constraints. However, these abstractions lack predicates such as constraints over extremal elements or sortedness. Our sequence abstract domain expresses not only relational constraints (it can express that a symbolic sequence is a fragment of another) but also constraints over length, extremal values, and specific predicates like sortedness. Although we use this sequence abstract domain for shape analysis, it could be used independently for other kinds of analyses.

To take advantage of this abstraction in shape analysis, we define a reduced product with a separation logic-based shape abstract domain. This product ties symbolic parameters of inductive predicates in separation logic together with sequence constraints. Sequence constraints that are inferred during the analysis (for instance when unfolding inductive predicates) are passed to the sequence domain. The reduced product also ensures communication between both domains for the computation of abstract operators such as union.

To summarize, we make the following contributions: -After we overview our analysis in Section 2, we introduce a relational abstract domain dedicated to reasoning over sequences in Section 3; -We define a reduced product between the new sequence domain and a separation logic-based abstract domain so as to extend a shape analysis with sequence reasoning capability. We first introduce the basic elements of the reduced product in Section 4 in the context of singly-linked lists. We discuss issues related to general inductive predicates in Section 5. -We report on the implementation of our analysis in the MemCAD static analyzer [START_REF] Li | Semantic-directed clumping of disjunctive abstract states[END_REF] and on its evaluation in Section 6. We show that it can cope with the verification of sorting programs and operations over binary search trees.

Overview

In this section, we give an overview of the main principles of our static analysis by demonstrating it on the insertion program shown in Figure 2. When applied to a binary search tree, this function inserts an element at the expected position to preserve sortedness. We study the verification of functional correctness expressed as partial correctness with respect to a pre-condition and a post-condition (Figure 2).

To formalize these, we let sort be a symbolic function over sequences of values that

∧ (S = sort(S) ∧ α0 ̸ = 0x0) (a) Abstract state at the end of line 6   ∧     S = S1.S0.S2 ∧ S = sort(S) ∧ Si = sort(Si) i ∈ {0, 1, 2} ∧ maxS 1 ≤ i ≤ maxS 2 ∧ maxS 1 ≤ maxS 0 ∧ minS 0 ≤ maxS 2 ∧ α0, α ′ ̸ = 0x0    
(c) Abstract state after the first widening Fig. 3. Selected abstract states maps any sequence to its sorted permutation. Then, the pre-condition assumption assumes that t is a well-formed tree described with predicate tree s (t, S) and such that S = sort(S) (i.e., such that the elements S in t are sorted). Likewise, the post-condition asserts that t is still a well-formed tree, the contents of which is sorted and comprises exactly the elements in S plus the added value i.

We now discuss the abstraction used by our static analysis. We combine an existing memory abstraction, inspired by separation logic-based shape analyses such as [START_REF] Calcagno | Footprint analysis : A shape analysis that discovers preconditions[END_REF][START_REF] Chang | Relational inductive shape analysis[END_REF], a relational numerical abstraction such as convex polyhedra [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF], and a novel abstract domain for sequences. Intuitively, the latter describes conjunctions of constraints over both symbolic sequences of values (such as S) and values manipulated by the program. These constraints consist of equalities of pairs of symbolic sequence expressions such as S ′ = sort(S.[i]). Moreover, the inductive predicates used in the memory abstraction are instances of the tree s predicate of Figure 1. For instance, the abstract pre-condition simply consists of the memory predicate tree s (t, S) and the sequence predicate S = sort(S), for some existentially quantified symbolic sequence variable S.

The analysis proceeds by forward abstract interpretation [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF]: it computes over-approximate abstract post-conditions for basic statements, and uses widening to enforce the convergence of abstract iterations for loops. Since the analysis uses a reduced product [START_REF] Cousot | Systematic design of program analysis frameworks[END_REF], an abstract state consists of a pair of components, namely the shape abstraction that describes the layout of data-structures and the contents' abstraction made of constraints over values and sequences of values. For each analysis step, information stored in either component may be used in order to refine the other, which we discuss next.

We focus on the analysis of the loop that searches for the insertion point in the else branch. First, the analysis of the condition test enriches the pre-condition with the constraint t ̸ = null as shown in the abstract state in Figure 3(a). Then, the analysis continues with the loop. The condition is a disjunction thus the analysis considers each case separately. For the first case, it refines the abstract state to reflect that the condition c->d <= i && c->l != null evaluates to true. Since both memory cells c->d and c->l are abstracted by the predicate tree s (α 0 , S), this predicate needs to be unfolded to enable the analysis of the condition. The first disjunct of inductive predicate tree s (Figure 1), which corresponds to the null pointer, is ruled out by constraint t ̸ = null. Therefore, only the second disjunct (non-empty tree) needs be considered. This shows how one component of the abstract state can refine the other. Thus, the analysis generates a new abstract state that exposes the root of the tree and lets α 1 , α 2 , and δ denote the contents of its l, r, and d fields. We remark that the inductive predicate unfolding also splits the symbolic sequence into S = S l .[δ].S r . Then the sequence domain derives that S l and S r are sorted since they are subsequences of a sorted sequence. It also infers that all values in S l are less than δ that is itself less than all values in S r by definition of sort, which writes down max S l ≤ δ ≤ min Sr . Last, it also retains the numerical constraint i ≤ δ. Figure 3(b) shows the resulting abstract state after the assignment line 9. In the case of the other disjunct, the tree is also unfolded but c points to α 2 instead of α 1 and the constraint over i and δ is δ < i.

The widening operator over-approximates abstract union of successive abstract iterates at loop head. In this case, it generalizes abstract states such as the ones shown in Figure 3(a) and Figure 3(b) by weakening them locally. Indeed, in all three states, c points to a well-formed tree containing a sequence S 0 . Moreover, the remaining of the memory region corresponds to a (possibly empty) partial tree: if it was completed by a tree with root pointed by c, the whole region would form a complete tree with root pointed by t. We call such a partial tree a tree segment predicate (the name segments comes from the analogy with list segments) and observe that it is can be automatically derived from tree s and defined by induction in Figure 4. When widening synthesizes an instance of treeseg s in Figure 3(c), it needs to infer its sequence argument. The sequence S of elements stored into the whole tree can be split into three parts, S 0 , S 1 , and S 2 where S 0 is the sequence of elements stored in the subtree pointed to by c and S 1 (resp., S 2 ) denote the sequence of elements stored in the "left" (resp., "right") part of the tree segment. This implies that the sequence argument of treeseg s is not a contiguous sequence. Therefore, it is represented as S 1 S 2 in the loop invariant Figure 3(c) where the

treeseg s (α, α ′ , S S ′ ) := | emp ∧ α = α ′ ∧ S = S ′ = [] | ∃α l , αr, v, S l , S ′ l , Sr, α.l → α l * α.r → αr * α.d → v * treeseg s (α l , α ′ , S l S ′ l )
Fig. 4. Inductive summarizing predicate describing tree segment placeholder notation stands for the sequence of elements in the "missing subtree" of the segment. When composing treeseg s and tree s the analysis operations resolve sequences using such symbol. Based on this loop invariant, the analysis of the final few assignments of the insertion function produces an abstract state that implies the desired post-condition.

Abstract Domain for Sequences

In this section, we define the sequence abstract domain, including its elements and the constraints they denote, its concretization, and its main abstract operators.

Sequences abstraction

An element of the abstract domain of sequences is a conjunction of constraints over a finite set of symbolic variables that stand either for sequences of base values, for base values, or for sets of values. Beside sequence equalities and predicates like sortedness, we also consider numerical upper/lower bounds over the values in sequences and multi-set constraints over the collections of values in sequences.

Concrete states. Let V denote a set of values. Although V usually denotes a set of scalar values (including addresses), our only assumptions on V is that it has a total ordering ⪯ with extremal values +∞, -∞. Since our domain constrains both variables that range over V and variables that range over sequences of values in V, we need several kinds of symbolic variables. In the following, we let symbols α, α 0 , α ′ 0 , β, . . . ∈ X n denote value symbolic variables, namely, variables that stand for a value in V. To express constraints on the set V * of all the finite words on alphabet V, we let a separate set X s , represent sequence symbolic variables. We note S, S 1 , S ′ , P, . . . ∈ X s such sequence variables. Finally, we write M(V) for the set of multisets of values in V and let X m be the set of multi-set valued symbolic variables. Moreover, if S ∈ X s is a sequence variable, we attach to it three numerical variables len S , min S , max S in X n that respectively denote the length, minimum and maximum value of S, and that there exists a multi-set variable multi S ∈ X m that denotes the multi-set of its elements.

A concrete state comprises three functions that map each kind of symbolic variables to elements of the corresponding type. Due to the relationship between a

E ::= [] | [α] | S | E.E | sort(E)
C (∈ C) ::= S = E (a) Syntax of expressions (E) and constraints (C)

[[]] s (σ) = ε [S] s (σ) = σs(S) [[α]] s (σ) = σn(α) [E1.E2] s (σ) = [E1] s (σ).[E2] s (σ) [sort(E)] s (σ) = a π(1) . . . a π(n) where    [E](σ) = a1 . . . an ∀i ∈ [1, n -1], a π(i) ⪯ a π(i+1) π is a permutation of [1, n] (σn, σs) |=s S = E iff σs(S) = [E] s (σn,
σ n : X n → V, σ m : X m → M(V), σ s : X s → V * are such that, for all S in X s , σ s (S) = a 1 . . . a n ⇒ σ n (min S ) = min i a i ∧ σ n (max S ) = max i a i ∧ σ n (len S ) = n ∧ σ m (multi S ) = {a 1 , . . . , a n } σ s (S) = ε ⇒ σ n (min S ) = +∞ ∧ σ n (max S ) = -∞ ∧ σ n (len S ) = 0 ∧ σ m (multi S ) = ∅
For short, given a state σ, we note its components σ n , σ m , and σ s . We write Σ for the set of all such concrete states. Abstract sequence constraints. The sequence abstract domain relies on expressions and constraints over symbolic variables. Their syntax is shown in Figure 5(a). An expression is either the empty sequence, or a sequence of length one that consists of a value symbolic variable, or a sequence symbolic variable, or a concatenation of expressions, or the sorting of a sequence expression returned by the function sort : E → E, (introduced in Section 2). Given a state σ, a sequence expression E evaluates into a sequence of values [E] s (σ), as shown in Figure 5(b). Sequence constraints are definition constraints of the form S = E, as shown in Figure 5(a). Allowing only symbolic sequence variables in the left-hand side of equalities somewhat limits expressiveness but simplifies the machine representation of abstract elements. The semantics of constraints is defined based on a satisfaction relation |= s that is spelled out in Figure 5(b): we write (σ n , σ s ) |= s C when constraint C holds in concrete state (σ n , σ s ). We note C for the set of sequence constraints.

Parameter abstract domains. In the following, we assume two abstract domains are fixed, taken as parameters by the sequence abstraction. First, D ♯ n represents numerical constraints and provides a concretization function γ n : D ♯ n → P(X n → V). Possible choices for D ♯ n include intervals [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF], octagons [START_REF] Miné | The octagon abstract domain[END_REF], or convex polyhedra [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF] abstract domains. Second, D ♯ m represents multi-set constraints and provides a concretization function γ m : D ♯ m → P(X m → M(V)). Our implementation uses a variation of the set domain of [START_REF] Li | Shape analysis for unstructured sharing[END_REF] that describes multi-set constraints.

Sequence abstraction. An abstract state consists either of a special element ⊥ that denotes the empty set of concrete states or of a finite conjunction of sequence constraints together with numerical and multi-set constraints: Definition 2 (Sequence abstraction). The abstract sequence domain Σ ♯ is defined as

{⊥} ⊎ {(σ ♯ n , σ ♯ m , C 0 ∧ . . . ∧ C n ) | σ ♯ n ∈ D ♯ n , σ ♯ m ∈ D ♯ m , C 0 , . . . , C n ∈ C}. Furthermore, its concretization γ Σ : Σ ♯ -→ P(Σ) is defined by γ Σ (⊥) = ∅ and: γ Σ (σ ♯ n , σ ♯ m , C 0 ∧ . . . ∧ C n ) = (σ n , σ m , σ s ) σ n ∈ γ n (σ ♯ n ) ∧ σ m ∈ γ m (σ ♯ m ) ∧ ∀i, σ n , σ s |= s C i
For consistency, we use σ ♯ s as a generic notation for a finite conjunction of constraints C 0 ∧ . . . ∧ C n and σ ♯ for a generic triple (σ ♯ n , σ ♯ m , σ ♯ s ). We remark that the empty conjunction of constraints concretizes into Σ thus we note it ⊤.

Machine representation. For the sake of algorithmic efficiency, we rely on an optimized machine representation for sequence constraints in non-bottom abstract states. First, we let equality constraints between variables be described by unionfind data-structures, which enables the incremental computation of equality classes representatives. Emptiness constraints (S = []) and sortedness constraints (S = sort(S)) are marked by tags over sequence variables. Finally, other equality constraints are represented with a map data type, the keys of which are the left hand side variables. For instance, S = [α] boils down to a map entry S → [α].

Abstract operations

We now discuss abstract operations on sequence abstract states. In this subsection, we discuss two operations: guard Σ refines an abstract sequence element into its conjunction with an additional constraint and verify Σ attempts to discharge a sequence constraint (so as to, e.g., verify an assertion). We assume that the underlying domains also implement similar operators. For instance, we require the numerical domain to provide an operator guard n that inputs a numerical constraint and a σ ♯ n ∈ D ♯ n and refines the latter with that constraint.

Abstract sequence condition. First, we consider the abstract sequence condition operator guard Σ : C × Σ ♯ → Σ ♯ which refines an abstract state with an additional sequence constraint. While a naive implementation of guard Σ (C, σ ♯ ) would simply add the constraint C to the conjunction σ ♯ s component, this would be imprecise in general. Indeed, the conjunction C ∧ σ ♯ s may be equivalent to ⊥. Moreover, C ∧ σ ♯ s may entail constraints that are strictly more precise than those in σ ♯ s . At a high level, guard Σ performs three kinds of operations: 1. Compaction simplifies constraints by rewriting the right hand side of definition constraints into the left hand side, wherever possible. For example, S = S

′ .[α].S ′′ ∧ S 1 = S ′ .[α] simplifies into S = S 1 .S ′′ ∧ S 1 = S ′ .[α]. 2.
Saturation synthesizes additional numerical and multi-set constraints that can be derived from a newly added constraint. For instance, S = S ′ .[α] entails that len S = 1 + len S ′ . Likewise, some constraints may entail that a sequence is empty. Another special kind of saturation occurs when the whole state can be reduced to ⊥ as incompatible constraints are detected. As saturation is the most complex part of guard Σ , we detail it below. 3. Detection of cyclic constraints prevents compaction and saturation from adding too many, redundant constraints, and it ensures the termination of algorithms iterating on definitions. We discuss this in Example 2. We now discuss constraint saturation more in detail:

-The length constraints saturation derives numerical constraints from the equality of the length of both sides of a new definition constraint S = E. Indeed, such a constraint implies len S = τ len (E), which can be added to the σ ♯ n component using guard n , where τ len is defined by:

τ len ([]) = 0 τ len (E.E ′ ) = τ len (E) + τ len (E ′ ) τ len (S) = len S τ len ([α]) = 1 τ len (sort(E)) = τ len (E)
-The multi-set contents constraints saturation operates similarly, and derives multi-set equalities from definition constraints. Surely, S = E entails multi S = τ mul (E), which can refine the σ ♯ m part using guard m where τ mul is defined by:

τ mul ([]) = ∅ τ mul (E.E ′ ) = τ mul (E) ⊎ τ mul (E ′ ) τ mul (S) = multi S τ mul ([α]) = {α} τ mul (sort(E)) = τ mul (E)
-The detection of empty sequence variables derives new definition constraints of the form S = [] when either sequence constraints or numerical constraints entail the emptiness of S. For instance:

• when σ ♯ s contains constraints S ′ = [] and S ′′ = [], the constraint S = S ′ .S ′′ simplifies into S = [];
• when σ ♯ n contains the constraint len S = 0, then it follows that S = [].

-The detection of sorted sequence variables do the same for constraints of the form S = sort(S) thanks to definitions of S and to numerical inequalities:

S = S 1 . . . . .S n ∀i, S i = sort(S i ) ∀i < j, max Si ≤ max Sj S = sort(S)
Such rule is very costly as it checks a quadratic amount of numerical inequalities. Nevertheless, relaxing the rule by only considering the case j = i + 1 is not sound, since sequence variables may be empty. Therefore, two consecutive elements in σ s (S) can come from non-consecutive sequence variables.

-The extremal values inequalities saturation derives numerical inequalities from a definition constraint S = E by case analysis over the right hand side E, and can be summarized by a set of derivation rules. The rules below describe such reasoning steps:

S = E α ∈ fv(E) min S ≤ α ≤ max S S = E S ′ ∈ fv(E) min S ≤ min S ′ max S ′ ≤ max S S = [] α ∈ X n max S < α < min S S ′ = sort(S ′ ) S ′ = . . . .[α].S. . . . α ≤ min S
As an example, the first rule states that numerical constraints can be derived from the knowledge that S is a concatenation of several components including a numerical variable α; in this case novel numeric constraints expressing that α is bounded by the extremal values of S can be added to σ ♯ n using operator guard n . Similarly, the second rule states that the extremal values of a sequence are bounded by the extremal values of any sequence containing it. The third rule states that an empty sequence supports arbitrary bounds. Finally, the fourth rule allows to reason over bounds when a sequence is known to be sorted.

-The decomposition of equality constraints synthesizes additional equality constraints that can be derived when two definition constraints S = E 0 and S = E 1 over the same name can be found in σ ♯ s . Indeed, when both E 0 and E 1 can be decomposed simultaneously, new equalities can be immediately derived:

[α 0 ].E 0 = [α 1 ].E 1 α 0 = α 1 E 0 = E 1 S.E 0 = E 1 S = [] E 0 = E 1
In less obvious decomposition cases, further constraints can still be derived with the help of the numerical constraints. Indeed:

S 0 .E 0 = S 1 .E 1 len S0 = len S1 S 0 = S 1 E 0 = E 1
Obviously, this inference may take place only when len S0 = len S1 can be proved in the numerical domain. A special case of saturation occurs when incompatible constraints are detected. Then, the whole abstract state is reduced to ⊥, following the principles of reduced product [START_REF] Cousot | Systematic design of program analysis frameworks[END_REF]. As an example, when the abstract state contains the constraints S = [α] and len S = 0, such a reduction is performed.

To summarize, the computation of guard Σ (C, σ ♯ ) involves the addition to σ ♯ of a set of constraints that are derived from C. It is conservative in general. The termination of this computation follows from the fact that the added constraints only involve syntactic subcomponents of the elements of C and σ ♯ s . Example 1. We consider the abstract state of Figure 3(b) and the constraint S 1 = S l .[δ] where S 1 is a new symbolic sequence variable. First, the constraint is added to the abstract state. Second, compaction replaces the pattern S l .[δ] with S 1 in all other constraints. Third, the numerical inequality α ≥ max S1 and the sortedness of S 1 entails that S 1 is sorted. Then, S 1 = sort(S 1 ) implies that δ is the maximum value of S 1 . Moreover, the fact that S l is a subsequence of S 1 entails that min S1 ≤ min S l and max S l ≤ max S1 . Finally, since δ ≤ i, guard Σ also derives max S1 ≤ i. Finally, guard Σ produces:

S = S 1 .S r ∧ S 1 = S l .[δ] ∧ S = sort(S) ∧ S i = sort(S i ), i ∈ {l, r, 1} ∧ max S l ≤ max S1 = δ ≤ max Sr ∧ min S1 ≤ max S l ∧ δ ≤ i ∧ α 0 , α 1 ̸ = 0x0
Example 2. In this example, we show the detection of mutually cyclic constraints. We consider the abstract state S 1 = S 2 .S ′ ∧ S 2 = S ′′ .S 3 , and the addition of S 3 = S 1 .S ′′′ . Inlining definition constraints for S 2 and S 3 would produce the cyclic constraint S 1 = S ′′ .S 1 .S ′′′ .S ′ . Thus, this also implies that S ′ , S ′′ , S ′′′ are empty and that S 1 , S 2 and S 3 are equal. After removal of the cycle, guard Σ produces:

S ′ = S ′′ = S ′′′ = [] ∧ S 1 = S 2 = S 3 ∧ S 1 = S 2 .S ′ ∧ S 2 = S ′′ .S 3
The operator guard Σ is sound in the following sense:

Theorem 1 (Soundness of guard Σ ). For all abstract state σ ♯ and constraint C,

we have {σ ∈ γ Σ (σ ♯ ) | σ |= s C} ⊆ γ Σ (guard Σ (C, σ ♯ )).
Verification of a sequence constraint. Second, we define the constraint verification operator verify Σ : Σ ♯ × C → {false, true} which inputs a constraint C and an abstract state σ ♯ and returns true when it can prove that σ ♯ entails C. It is conservative in the sense that it may return false even when the constraint is satisfied. The computation of verify Σ (C, (σ ♯ n , σ ♯ m , σ ♯ s )) proceeds as follows:

1. If σ ♯ s is ⊥, it returns true. 2.
For definition constraints S = E, verify Σ inlines the definitions of variables, and returns true when both sides rewrite into syntactically equal expressions. The absence of cyclic constraints ensures this exploration terminates. 3. Otherwise, it returns false.

For constraints of the form S = sort(E), the operator uses a specific rule (shown below) since variables inside the sort function may be arbitrarily reordered. Instead, we take advantage of the multi-set abstract domain to establish that S and E have the same contents.

S = sort(S) multi S = τ mul (E) S = sort(E)
The operator verify Σ is sound in the following sense:

Theorem 2 (Soundness of verify Σ ). For all abstract state σ ♯ and constraint C,

if verify Σ (σ ♯ , C) = true then, we have γ Σ (σ ♯ ) ⊆ {σ ∈ Σ | σ |= s C}.

Lattice operations

We now discuss join, widening and inclusion checking operations for loop analysis. We assume that D ♯ n provides a conservative inclusion test operator is_le n (it inputs two elements of σ ♯ n and returns true only when it succeeds proving the first is included in the second), an over-approximate join operator join n and a widening widen n , and that D ♯ m provides similar operators is_le m , join m , and widen m , and we build similar operators for Σ ♯ .

Inclusion checking. The inclusion test operator inputs two abstract states and returns a boolean. When it returns true, the concretization of the first abstract state is included into that of the second one. The inclusion checking algorithm is based on the constraint representation of abstract states and boils down to a repeated application of verify Σ .

Definition 3 (Inclusion checking operator). The operator is_le

Σ : Σ ♯ × Σ ♯ → {true, false} is defined by: is_le Σ ((σ ♯ n,0 , σ ♯ m,0 , σ ♯ s,0 ), (σ ♯ n,1 , σ ♯ m,1 , ∧ i C i )) := is_le n (σ ♯ n,0 , σ ♯ n,1 ) ∧ is_le m (σ ♯ m,0 , σ ♯ m,1 ) ∧ (∧ i verify Σ (C i , σ ♯ s,0
)) The soundness of is_le Σ follows from that of is_le n , is_le m , and verify Σ :

Theorem 3. The operator is_le Σ is sound in the sense that, for all σ ♯ 0 , σ ♯ 1 ∈ Σ ♯ , if is_le Σ (σ ♯ 0 , σ ♯ 1 ) = true, then γ Σ (σ ♯ 0 ) ⊆ γ Σ (σ ♯ 1 ).
Upper bounds. As usual, we define two over-approximate upper-bound operators, namely, a classical join operator join Σ : Σ ♯ × Σ ♯ → Σ ♯ and a widening widen Σ :

Σ ♯ × Σ ♯ → Σ ♯ that ensures termination.
Essentially, the join Σ operator proceeds component-wise (like is_le Σ as defined in Definition 3) and essentially preserves sequence constraints that appear in both arguments. In the case of definition constraint, it first saturates the conjunctions of constraints, so as to maximize the possible sets of common constraints. The algorithm of widen Σ is similar, except that it does not saturate its left argument for the sake of termination. This implies that widen Σ always returns a conjunction of constraints that forms a subset of the constraints of its left argument.

Both operators are sound and furthermore, widen Σ guarantees termination.

Theorem 4 (Soundness of join Σ and widen Σ , termination of widen Σ ). For all abstract states σ ♯ 0 , σ ♯ 1 , we have:

γ Σ (σ ♯ 0 ) ∪ γ Σ (σ ♯ 1 ) ⊆ γ Σ (join Σ (σ ♯ 0 , σ ♯ 1 )) γ Σ (σ ♯ 0 ) ∪ γ Σ (σ ♯ 1 ) ⊆ γ Σ (widen Σ (σ ♯ 0 , σ ♯ 1 )
). Moreover, the operator widen Σ ensures termination, that is, for all sequence (σ ♯ n ) n∈N of abstract states the sequence

((σ ♯ ) ′ n ) n∈N defined by (σ ♯ ) ′ 0 = σ ♯ 0 and (σ ♯ ) ′ n+1 = widen Σ ((σ ♯ ) ′ n , σ ♯ n+1
) is ultimately stationary. Example 3 (Join). In this example, we consider the computation of the join of two abstract states taken from the analysis of the program of Figure 2. The analysis of the loop at line 7 involves the computation of the join of the three abstract states below. For concision, we omit inequality constraints involving extremal values of empty sequences.

σ ♯ 0 ::= S = S 0 ∧ S 1 = S 2 = [] ∧ S = sort(S) ∧ S i = sort(S i ), i ∈ {0, 1, 2} σ ♯ 1 ::= S = S 0 .S 2 ∧ S 1 = [] ∧ max S0 ≤ min S2 ∧ i ≤ min S2 ∧ S = sort(S) ∧ S i = sort(S i ), i ∈ {0, 1, 2} σ ♯ 2 ::= S = S 1 .S 0 ∧ S 2 = [] ∧ max S1 ≤ min S0 ∧ max S1 ≤ i ∧ S = sort(S) ∧ S i = sort(S i ), i ∈ {0, 1, 2}
The most notable step is the saturation of the first argument, that injects constraint S = S 1 .S 0 .S 2 , as a consequence of S = S 0 and

S 1 = S 2 = [] in σ ♯ 0 , S = S 0 .S 2 and S 1 = [] in σ ♯ 1 and S = S 1 .S 0 and S 2 = [] in σ ♯ 2 .
After this, constraints that hold in only either argument are dropped, as, e.g., constraint

S 1 = [] in σ ♯ 1 .
The result of the union corresponds to the abstract state in Figure 3(c). In this section, we define a shape analysis with inductive predicates that infers invariants about both the layout of data-structures and the sequences of values they store. For the sake of simplicity, we consider only a singly-linked list predicate (Figure 6) throughout this section, although our analysis and its implementation are parameterized by user-defined inductive predicates [START_REF] Chang | Relational inductive shape analysis[END_REF][START_REF] Chang | Shape analysis[END_REF]. The generalization to other structures will be discussed in Section 5.

struct list { struct list* next; int data; }; lseg s (α0, α1, S ) := | emp ∧ α0 = α1 ∧ S = [] | ∃ α ′ , δ, S ′ , α0.next → α ′ * α0.data → δ * lseg s (α ′ , α1, S ′ ) ∧ α0 ̸ = 0x0 ∧ S = [δ].S ′

Language and semantics

Although our implementation is based on the MemCAD analyzer [START_REF] Li | Semantic-directed clumping of disjunctive abstract states[END_REF] and targets the C language, our formalization only considers a restricted fragment. We let X denote a finite set of program variables. We consider a basic imperative language, where commands are assignments, conditional statements, loops, and sequences of commands. Expressions are either l-values that evaluate to addresses, or r-values, that evaluate to scalars. An l-value l is either a program variable v ∈ X, the access to an l-value field l.f (for concision, we let f denote both the field name and the corresponding memory offset), or the dereference * e of an expression e. An r-value e is either a constant n ∈ V, or the reading of the memory cell defined by an l-value l, or the address &l or an l-value l, or the application e 0 ⊕ e 1 of a binary operator to two sub-expressions. For simplicity, we assume here that operators are deterministic and cause no errors. The grammar is shown below: We note A for the set of addresses, which is a subset of the set of values V. A memory state m is a partial function from addresses to values. We note M for the set of memory states and let ∅ denote the empty memory. Furthermore, we assume that each program variable x has a fixed address denoted by x ∈ A. Based on these definitions, we set up the program semantics as follows. First, we define the semantics of expressions by induction over their syntax. The semantics of an l-value l is a function [l] l : M → A that maps a memory state m to the address l evaluates to in m. Similarly, the semantics [e] e : M → V of an expression e maps a memory state to a value. Finally, the semantics [c] : P(M) → P(M) of a command c maps any set of input memory states M to the set of all possible output memory states when starting from any m ∈ M . The definition of all three semantics is classical and shown in Figure 7, where f ⊕ : V 2 → V denotes the semantics of operator ⊕. where

l ::= v | l.f | *
F (M ′ ) = M ∪ [c](m ∈ M ′ | [e] e (m) ̸ = 0}) [c0; c1](M ) := [c1] • [c0](M )

Combined memory and sequence abstraction

Sequence aware shape abstraction. We start with the definition of abstract memory predicates, following an approach similar to that of separation logic based shape analyses with inductive definitions [START_REF] Calcagno | Footprint analysis : A shape analysis that discovers preconditions[END_REF][START_REF] Chang | Relational inductive shape analysis[END_REF], extended with sequence information. As explained early in the section, our formalization considers a single inductive predicate describing list segments, and parameterized with a symbolic sequence variable that stands for the sequence of the values contained in them (Figure 6). Considering only list segments has two advantages. First, complete lists can be expressed as list segments the last element of which has a "next" field equal to 0x0. Second, it simplifies reasoning over sequences as it avoids branching structures (considered in Section 5). Abstract states rely on scalar symbolic variables in X n to denote values and addresses and consist of separating conjunctions [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF] of points-to predicates and of list segment predicates: Definition 4 (Abstract memory states). The set of abstract memory states M ♯ is described by the grammar below, where α 0 , α 1 ∈ X n and S ∈ X s :

m ♯ ::= emp | m ♯ * m ♯ | α 0 .f → α 1 | lseg s (α 0 , α 1 , S )
We note M ♯ for the set of abstract memory states.

As usual, emp denotes the empty memory region and m ♯ 0 * m ♯ 1 denotes the disjoint union of memory regions described by m ♯ 0 (resp., m ♯ 1 ). The abstract predicate α 0 .f → α 1 denotes a single memory cell, the address of which is described by α 0 plus the offset of f and the contents of which is described by α 1 . Finally, lseg s (α 0 , α 1 , S) stands for a (possibly empty) list segment that starts at an address described by α 0 , ending with a pointer to address α 1 , where each list element consists of two fields, namely, a pointer to the next element and a data field, and such that the sequence of the values of the data fields is described by sequence variable S. In logical terms, the predicate lseg s (α 0 , α 1 , S) is defined inductively as shown in Figure 6.

As the definition of lseg s in Figure 6 shows, the concretization of abstract memory states indirectly involves sequence variables (and also multi-set variables). Indeed, given an abstract memory state m ♯ and a sequence variable S that appears in m ♯ , the concretization of m ♯ also constrains S, len S , and multi S . To reflect this, we let the concretization of an abstract memory m ♯ return a set of tuples that comprise not only a memory state m, but also a valuation that maps each symbolic variable in m ♯ to a value of the corresponding type (scalar, multi-set, or sequence). Such a valuation boils down to a triple (σ n , σ m , σ s ) (Definition 2). The definition of the concretization is based on a set of inductive derivation rules that follow the syntax of abstract memories and unfold the list segment predicates (Figure 8).

∅, σ |=M emp m = [σn(α0) + f → σn(α1)] m, (σn, σm, σs) |=M α0.f → α1 ∀i, mi, σ |=M m ♯ i m0 ⊎ m1, σ |=M m ♯ 0 * m ♯
Definition 5 (Concretization of abstract memory states). The concretization of abstract memory states γ M maps an abstract memory m ♯ to a set of pairs (m, σ) ∈ M × Σ and is defined by:

γ M (m ♯ ) = {(m, σ) | (m, σ) |= M m ♯ }
As examples of abstract memory states, we refer the reader to the left conjuncts of the three abstract states shown in Figure 3.

Combined abstract domain. The analysis needs to reason accurately over sequence variables not only when they are bound in an inductive predicate, but also when these predicates are unfolded. Thus, it requires a product abstract domain based on the memory abstract domain fixed in Definition 4 and Definition 5 and on the sequence abstract domain introduced in Section 3. Moreover, like most shape analyses, it sometimes needs to make case splits due to the disjunctive nature of the inductive predicate lseg s . Thus, the combined abstraction is defined as follows:

Definition 6 (Combined abstraction). The elements of the combined state abstract domain S ♯ are finite disjunctions of pairs of the form (m ♯ , σ ♯ ) ∈ M ♯ × Σ ♯ . Furthermore, the concretization γ S maps an element s ♯ of S ♯ into a set of memories m and is defined by:

γ S ((m ♯ , σ ♯ )) := {m | ∃σ ∈ γ Σ (σ ♯ ), (m, σ) ∈ γ M (m ♯ )} γ S ( i s ♯ i ) := i γ S (s ♯ i )
Concatenating segments. Before we move to the analysis algorithms, we discuss a principle for logical reasoning over segments that many analysis operations rely on. Intuitively, a pair of consecutive segments may be merged into a single segment, that stores a sequence of elements that is the concatenation of the elements in the two initial segments. Reciprocally, it is possible to split a segment based on a partition of the sequence of its elements. The lemma below formalizes this.

Lemma 1 (Concatenation (list predicates)). We assume α 0 , α 1 , α 2 distinct symbolic variables and let m ♯ 0 := lseg s (α 0 , α 1 , S 1 ) * lseg s (α 1 , α 2 , S 2 ), m ♯ 1 := lseg s (α 0 , α 2 , S ), and σ ♯ := S = S 1 .S 2 . Then:

-γ S (m ♯ 0 , σ ♯ ) ⊆ γ S (m ♯ 1 , σ ♯ ); -if (m, σ 1 ) ∈ γ S (m ♯
1 , σ ♯ ), then there exists σ 0 such that (m, σ 0 ) ∈ γ S (m ♯ 0 , σ ♯ ) and, for all β ∈ V such that β ̸ = α 1 , σ 0 (β) = σ 1 (β).

Computation of abstract post-conditions

Abstract post-conditions are computed by a pair of families of functions:

given l-value l and expression e, assign S,l=e : S ♯ → S ♯ computes an overapproximation for the assignment command l = e; -given expression e, guard S,e : S ♯ → S ♯ computes an over-approximation for the effect of the condition expression e. In the following paragraphs, we give the main steps of the algorithms to compute them. They both ensure the soundness conditions below, for all l-value l, expression e, and abstract state s ♯ ∈ S ♯ :

[l = e](γ S (s ♯ )) ⊆ γ S (assign S,l=e (s ♯ )) {m ∈ γ S (s ♯ ) | [e] e (m) ̸ = 0} ⊆ γ S (guard S,e (s ♯ ))
Simple cases. The computation of post-conditions for assignments and tests that involve only fully exposed cells is straightforward and follows classical shape analysis techniques [START_REF] Chang | Shape analysis[END_REF]. For instance:

assign S,x.f=y (x.f → α 0 * y → α 1 * m ♯ , (σ n , σ m , σ s )) = (x.f → α 1 * y → α 1 * m ♯ , (σ n , σ m , σ s )) guard S,x.f̸ =0x0 (x.f → α 0 * m ♯ , (σ n , σ m , σ s )) = (x.f → α 0 * m ♯ , (guard n (α 0 ̸ = 0, σ n ), σ m , σ s ))
where guard n denotes a sound condition test for the numerical domain [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF].

Unfolding inductive predicates. The more difficult cases in post-conditions arise when some of the memory cells that are affected by the statement are summarized as part of an inductive predicate as, e.g., in assign S,x=x.next (x → α 0 * lseg s (α 0 , α 1 , S )). In such cases, some inductive predicates need to be unfolded, before falling back to the simpler situation shown in the two aforementioned cases. The unfolding operation is based on rewriting rules that follow directly from the inductive nature of lseg s . We note ⇝ the unfolding relation that rewrites an abstract state into another. Basic cases of ⇝ proceed as follows:

(lseg s (α 0 , α 1 , S ) * m ♯ , (σ ♯ n , σ ♯ m , σ ♯ s )) ⇝    (m ♯ , guard Σ (S = [], guard n (α 0 = α 1 , σ ♯ n ), σ ♯ m , σ ♯ s )) ∨ α 0 .next → α 2 * α 0 .data → α 3 * lseg s (α 2 , α 1 , S 1 ) * m ♯ , guard Σ (S = [α 3 ].S 1 , guard n (α 0 ̸ = 0, σ ♯ n ), σ ♯ m , σ ♯ s )
where α 2 , α 3 , S 1 are fresh. Unfolding is proved sound by the rules of Figure 8 in the sense that, for all

s ♯ 0 , s ♯ 1 ∈ S ♯ , if s ♯ 0 ⇝ s ♯ 1 , then γ S (s ♯ 0 ) ⊆ γ S (s ♯ 1
). The soundness of assign S,. and guard S,. follows from that of the unfolding relation, from that of the assignment and condition test of the underlying abstract domains, and from the (straightforward) handling of the unfolded cases.

We remark that the main difference compared to baseline shape analyses is that unfolding produces additional predicates about the sequence variables, which are added into the sequence domain. In turn, the addition of these constraints may yield increased precision due to internal reduction.

Computation of lattice operations

The lattice operations required for the analysis of loops comprise the conservative inclusion test and the over-approximation of concrete upper bounds. Moreover, the former is used in the definition of the latter. Again, the algorithms to compute them are based on those of classical shape analyses. Thus, we emphasize the extensions that are required to infer sequence information and refer the reader to [START_REF] Chang | Shape analysis[END_REF] for a full description of shape abstraction inclusion and widening algorithms.

Inclusion checking. The inclusion test function performs a proof search to try to establish inclusion. Although the rule system actually used is more complex, the inclusion proof system can be summarized down to three basic principles. First, when two abstract states have the same abstract memory component, proving inclusion boils down to checking the inclusion in Σ ♯ . Second, when the left-hand side contains several inductive predicate instances that can be summarized into one in the right-hand side, the analysis tries to concatenate them using Lemma 1. Third, when the right-hand side can be unfolded and the left-hand side is included into one of the unfolded disjuncts, then the inclusion holds for the initial pair. The rules below formalize these three principles.

is_le Σ (σ ♯ l , σ ♯ r ) = true (m ♯ , σ ♯ l ) ⊑ (m ♯ , σ ♯ r ) verify Σ (σ ♯ l , S = S 1 .S 2 ) = true (lseg s (α, β, S 1 ) * lseg s (β, δ, S 2 ) * m ♯ l , σ ♯ l ) ⊑ (lseg s (α, δ, S ), σ ♯ r ) s ♯ r ⇝∨ i s ♯ i (m ♯ i , guard Σ (σ ♯ i , C i )) ∃j, verify Σ (C j , σ ♯ l ) = true ∧ (m ♯ l , σ ♯ l ) ⊑ s ♯ j (m ♯ l , σ ♯ l ) ⊑ s ♯ r
The is_le S function takes two abstract states and attempts to construct a proof tree that establishes inclusion based on these principles. The main specificities of the product with a sequence abstract domain are the requirement for is_le S to track sequence concatenation constraints and the use of the inclusion checking function of the sequence abstract domain. The soundness of is_le S follows from the soundness of the shape inclusion algorithm and of the underlying domains operations:

Theorem 5 (Soundness of is_le S ). For all s ♯ 0 , s

♯ 1 ∈ S ♯ , if is_le S (s ♯ 0 , s ♯ 1 ) = true then γ S (s ♯ 0 ) ⊆ γ S (s ♯ 1 ).
Join and Widening. The cases of join and widening are more subtle, since these operators may need to introduce lseg s predicates together with fresh symbolic sequence variables, and to infer accurate relations over these new variables. Indeed, these algorithms are based on the following two principles:

when the memory components of the two arguments are equal, we use it for the shape specific part of the result; -when the memory components of the two arguments differ, they need to be weakened by replacing memory fragments with novel instances of lseg s , with fresh symbolic sequence variables, and by checking inclusion holds using is_le S . To illustrate the second case, we consider the over-approximation of the two abstract states below:

s ♯ 0 := (α 0 .next → α 1 * α 0 .data → α 3 * lseg s (α 1 , α 2 , S ), σ ♯ 0 ) s ♯ 1 := (lseg s (α 0 , α 1 , S ) * α 1 .next → α 2 * α 1 .data → α 3 , σ ♯ 1 )
Clearly, the memory part of both states may be weakened to the same abstract memory lseg s (α 0 , α 2 , S ′′ ) where S ′′ is fresh. This gives the shape specific part of the result. However, in the case of s ♯ 0 , this weakening holds under the constraint S ′′ = [α 3 ].S, whereas it holds under the constraint S ′′ = S ′ .[α 3 ] in the case of s ♯ 1 . Therefore, the sequence abstract states should be updated according to these two constraints before calling the corresponding operator in the sequence domain, which produces:

join Σ (guard Σ (S ′′ = [α 3 ].S, σ ♯ 0 ), guard Σ (S ′′ = S ′ .[α 3 ], σ ♯ 1 )).
Note that this weakening also generates numerical and multi-set constraints. This constraint synthesis issue is carried out by an extension of the inclusion checking algorithm that keeps track of the fresh variables introduced by the widening and accumulates constraints over these.

Theorem 6 (Soundness of join S , widen S and its termination). The upper bound operator join S , widen S : S ♯ × S ♯ → S ♯ are sound in the sense that, for all

s ♯ 0 , s ♯ 1 ∈ S ♯ , then γ S (s ♯ 0 ) ∪ γ S (s ♯ 1 ) ⊆ γ S (join S (s ♯ 0 , s ♯ 1 )) γ S (s ♯ 0 ) ∪ γ S (s ♯ 1 ) ⊆ γ S (widen S (s ♯ 0 , s ♯ 1 ))
Moreover, widen S also ensures the termination property [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF].

Static analysis of a simple language

The analysis of a command c is a function c ♯ : S ♯ → S ♯ that over-approximates [c]. It is defined by induction over the syntax in Figure 9. Note that the convergence of the sequence of abstract iterates follows from the termination property of widen S , and the analysis uses is_le S to detect stabilization. For conditional statements, we l = e ♯ (s ♯ ) := assign S,l=e (s ♯ ) if(e){c0} ♯ (s ♯ ) := joinS c0 ♯ (guard S,e̸ =0 (s ♯ )), guard S,e=0 (s ♯ ) while(e){c} ♯ (s ♯ ) := guard S,e=0 (limn s ♯ n ) where s ♯ 0 := s ♯ and s analyze the two branches separately after assuming the corresponding constraint, and we merge the two resulting states using join S . It is sound (the proof of soundness is classical [START_REF] Chang | Shape analysis[END_REF] and proceeds by induction over the syntax):

♯ n+1 := widenS(s ♯ n , c ♯ (guard S,e̸ =0 (s ♯ n ))) c0; c1 ♯ (s ♯ ) := c1 ♯ • c0 ♯ (s ♯ )
Theorem 7 (Soundness). For all command c, [c] • γ S . ⊆ γ S • c ♯ .

Shape and sequence predicates for non-linear structures

This section discusses the general inductive predicates used by our analysis. While Section 4 only considered basic list predicates so as to introduce the analysis in a simpler setup, we now show our analysis handles m-ary trees (thus including lists when m = 1), possibly with parent pointers. We require that the sequence arguments of inductive definitions denote (sub-)sets of elements stored in structure (we comment on this restriction in Remark 1). The following paragraphs show the specificities of sequence predicates for such data-structures, the derivation of segment predicates and how it affects analysis operations.

Segment predicates and sequence information. Segment predicates such as lseg play a very important role in the analysis, e.g., to analyze data-structure traversals, as in Section 2. Basic analysis operations split or merge inductive predicates that describe full structures and segments. As we remarked in Section 4, sequence information needs to be maintained when such steps are performed and Lemma 1 provides the method to do so for lseg. As observed in Section 2, the method derived from Lemma 1 will not work for non linear structures. Indeed, let us consider the tree segment predicate treeseg s shown in Figure 4, which describes all the possible ways to decompose memory states that store a full tree at node α 0 and where α 1 is the address of one of its subtrees. Equivalently, the memory can be decomposed into a tree segment between α 0 and α 1 and a full tree at root α 1 . We note S 0 (resp., S 1 ) the sequence of elements in the whole structure (resp., the subtree). Figure 10 depicts all possible configurations. In the first case, the subtree and the tree are equal, so the segment is empty and S 0 = S 1 . In the second case, the subtree at α 1 is a leftmost subtree and S 0 = S 1 .S r for some S r . The third case is symmetric. The fourth case is the most general and S 0 = S l .S 1 .S r for some S l , S r . Therefore, the most general definition of the sequence(s) of elements in the segment (when the subtree in shown blue is excluded) is S 0 = S l S r , where is a placeholder that abstracts the sequence of the elements in the "missing" subtree, and where S l , S r may denote the empty sequence.

Derivation of segment predicates from full predicates. While inductive predicates (e.g., the definition of lists or trees) are user-supplied, our analysis automatically derives the corresponding segment predicates. Indeed, given a full predicate (like tree s ) for an m-ary form of tree (including lists), the segment predicate is obtained by the sequence of steps below:

each sequence argument S i is replaced by a marked sequence S i S ′ i , -a rule describes empty segments; it abstracts an empty memory region, constrains its extremal points to be equal and its sequence contents to be empty; -for each inductive rule that contains recursive calls to the inductive predicate, and for each such call c, the segment predicate should include a rule replacing c with a segment instance; moreover, in each such segment rule, the linearity of the sequence concatenations should be reflected by sequence constraints. As an example, we illustrate this in the case of tree s :

Example 4 (Tree segments). The definition of tree s is shown in Figure 1. As it has one sequence parameter, the corresponding segment predicate has two, that we note S 0 and S 1 and writes down treeseg s (α, α ′ , S 0 S 1 ). We now detail the derivation of the treeseg s predicate shown in Figure 4. As stated above, treeseg s includes a rule for empty segments (the first one in Figure 4), which corresponds to an empty region, two equal pointers and two empty sequences. The first rule of tree s corresponds to the empty tree; it has no recursive call and cannot appear in segments. The second rule of tree s has two recursive calls (for the left and right subtrees), thus, it gives rise to two rules in treeseg s , that stand for cases where the segment is in the left (resp., right) subtree. Finally, we consider the constraints over sequences in the last rule (right subtree). Given the notation in Figure 4, the sequence of values in the whole tree is the argument S S ′ of treeseg s which is equal to S l . [v].S r S ′ r in the last rule. This equality entails the constraints S = S l . [v].S r and S ′ = S ′ r which thus appear in the last rule of treeseg s . Remark 1 (Limitation of sequence arguments). We observe that the inference of the sequence constraints by linearity as shown in Example 4 can only be achieved since the sequence constraints in tree s specify that its segment argument collects a set of elements found at some fields in the structure. As an example, the analysis would not support an alternative definition of tree s where the inductive rule would have the sequence constraint S = sort(S l .[v].S r ), as it does not allow the derivation of precise constraints over sub-sequences for segments. We note that this limitation does not prevent capturing precisely binary search trees in the product abstract domain of Definition 5 with element tree s (α, S) ∧ S = sort(S); instead, it only requires the shape predicate be written in a certain way.

Analysis. The analysis requires users to supply inductive predicates for full structures as well as target pre-and post-conditions. Segment predicates are inferred automatically as shown in the previous paragraph, as well as the appropriate concatenation lemma. Finally, the analysis operators are similar to those shown in Section 4, except that they use the concatenation property inferred from the definition of the full structure inductive predicate. For instance, when using the tree inductive predicate of Figure 1, the analysis infers the segment of Figure 4 and the concatenation lemma 2. The analysis satisfies the soundness property of Theorem 7. To conclude the section, we discuss a couple of steps of the computation of widening in the analysis of the program in Figure 2.

Example 5 (Inclusion checking). We consider the following abstract states:

-

s ♯ 0 = (α.l → α 0 * α.d → α 1 * α.r → α 2 * tree s (α 2 , S r ), σ ♯ 0 ); -s ♯ 1 = (treeseg s (α, α 0 , S S ′ ), σ ♯ 1 )
. Both s ♯ 0 and s ♯ 1 appear during the widening at the first iteration. We study the evaluation of the inclusion test is_le S (s ♯ 0 , s ♯ 1 ). We first remark the following unfoldings (where α 3 , α 4 , α 5 , S l , and S ′ l are fresh) yield a similar abstract memory, up to existentially quantified symbolic variable names:

s ♯ 1 ⇝ (α.l → α 3 * α.d → α 4 * α.r → α 5 * treeseg s (α 3 , α 0 , S l S ′ l ) * tree s (α 5 , S r ), σ ♯ 0 ) ∧ S = S l ∧ S ′ = S ′ l .[α 4 ].S r ⇝ (α.l → α 3 * α.d → α 4 * α.r → α 5 * emp * tree s (α 5 , S r ), σ ♯ 0 ) ∧ S = S l ∧ S ′ = S ′ l .[α 4 ].S r ∧ S l = [] ∧ S ′ l = [] ∧ α 0 = α 3
By the definition of is_le S in Section 4.4, is_le S (s ♯ 0 , s ♯ 1 ) returns true if and only if Example 6 (Widening). We now study the computation of the first widening in the analysis of the program shown in Section 2. For brevity, we only consider the second disjunct after the condition. The arguments of widening of abstract memory states and the result are shown in Figure 11. As mentioned in Section 4.4, the widening operator seeks for regions that can be described in a similar manner in the both of its arguments, possibly after weakening them. Matching colors in Figure 11 highlight pairings of similar regions. Recall that all symbolic variables (α, α 0 , . . .) are existentially quantified within a same state. We observe the terms in blue, green and purple are pairwise equal and require no weakening. The areas in red though are not equal. For clarity, we add an emp term in m ♯ 0 . As observed in Example 5, the matching terms in m ♯ 1 can be weakened into treeseg s (α 0 , α 1 , S 1 S 2 ), provided S 1 = [] and S 2 = [δ].S r . The same holds for emp in m ♯ 0 . The table in the bottom of Figure 11 summarizes the correspondence between existentially quantified symbolic variables that realizes the association of regions.

is_le Σ (σ ♯ 0 , σ ♯ 1 ), verify Σ (σ ♯ 0 , S = []) and verify Σ (σ ♯ 0 , S ′ = [α 1 ].S r ) all return true.     &t → α0 * &c → α0 * emp * trees(α0, S)     m ♯ 0     &t → α0 * &c → α1 * α0.l → α1 * α0.d → α2 * α0.r → α3 * trees(α1, S l ) * trees(α3, Sr)     m ♯ 1     &t → α * &c → α ′ * treeseg s (α, α ′ , S1 S2) * trees(α ′ , S0)     m ♯ f m ♯ f α α ′ S0 S1 S2 m ♯ 0 α0 α0 S [] [] m ♯ 1 α0 α1 S l [] [α2].Sr
The above paragraph describes the computation of the abstract memory state shown in Figure 3(c). The computation of the sequence abstract state of Figure 3(c) proceeds by application of widen Σ .

Implementation and evaluation

In this section, we report on the implementation and evaluation of the product shape and sequence analysis. We consider the following research questions:

-(RQ1) Is the combined analysis of Section 4 and Section 5 precise enough to prove functional properties on programs implementing classical algorithms over dynamic data-structures (like lists, sorted lists, and binary search trees), and does it help a baseline analysis verify structural invariants are preserved? -(RQ2) Can this analysis successfully verify real-world C libraries? -(RQ3) How significant is the overhead of the combined analysis compared to the baseline?

Implementation. We have implemented the sequence abstract domain and the product with the shape abstraction of the MemCAD static analyzer [START_REF] Li | Semantic-directed clumping of disjunctive abstract states[END_REF][START_REF]Artifact for "A Product of Shape and Sequence Abstractions[END_REF]. The analysis inputs C programs and user-supplied inductive predicates describing datastructures together with pre-and post-conditions and attempts to verify them, as well as absence of runtime errors. We set convex polyhedra [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF] implemented in the Apron library [START_REF] Jeannet | Apron: A library of numerical abstract domains for static analysis[END_REF] as numerical abstraction and an extension of [START_REF] Li | Shape analysis for unstructured sharing[END_REF] as multi-set abstraction.

Experiments. We consider two sets of experiments. The first one (Table 1) consists of custom implementations of classical algorithms over lists, sorted lists, and binary search trees and includes sorting, insertion and deletion algorithms. The second (Table 2) collects list data-structure implementations taken from the Linux [START_REF] Torvalds | The linux kernel[END_REF] and FreeRTOS [START_REF] Inc | The freertos kernel[END_REF] operating systems as well as the Generic data-structure library (GDSL) [START_REF] Darnis | The generic data-structure library[END_REF], which all involve specificities like back pointers or sentinel nodes.

For each data-structure, we provide an inductive definition written in the DSL of MemCAD. This amounts to a single definition a few lines long for each series of tests. For each test, we also specify the pre-and post-condition of procedures. When a procedure may behave differently depending on the shape of their input, we provide two pre-/post-condition pairs. This occurs for the "Pop" function, which does nothing when applied to the empty list. Two target properties are studied:

-PrSafe: absence of memory errors and structural preservation (with respect to list or tree invariants but without checking anything about their contents); For loop iterations, disjoint loops are separated by a semicolon, nested loops by a comma, and the first number corresponds to the outer loop. For inner loops, we take the maximum number of iterations needed to stabilize it.)

-Fc: partial functional correctness (including sortedness and the preservation of the elements stored in data-structures). We ran the experiments on a machine with an i7-8700 processor with 32 Gb of RAM running Ubuntu 18.04. For each test case, we run the analysis without and then with sequence abstraction to compare runtimes and check if the analyses prove the expected property. When using the analysis without sequence abstraction, only PrSafe is considered (this abstraction cannot express Fc), whereas the analysis of sequences attempts to discharge both PrSafe and Fc. Table 1 displays raw results for the first series of tests. Table 2 shows the results of the main tests in the second series of tests(for brevity, all results are given in appendix in Table 3).

Verification of complex properties. As shown in Table 1, the analysis with sequences fully verifies both memory safety and functional correctness (PrSafe and Fc) for all target codes including three different list sorting programs, operations on binary search trees as well as heap sort (elements of a list are all inserted in an empty binary search tree and collected in a left to right order back into a list). These examples all require the inference of fairly involved invariants. The analysis without sequences can only verify PrSafe, yet it fails to do so in several examples, where the use of sequences actually also lets the analysis verify PrSafe (in addition to Fc). This result is somewhat surprising, as we would not expect sequence information be required to establish basic safety. One caveat is that one example (bubble sort) required the manual insertion of a directive to MemCAD to delay folding. We conjecture the shape folding operator could be improved to avoid this. All other analyses are fully automatic. We conclude the product with sequences not only allows to prove Fc even in challenging cases, but may also help with PrSafe.

Verification of real-world libraries. We now consider Table 2. These examples involve lists with invariants that are considerably more sophisticated than lseg s , as they are all doubly-linked lists with headers. While GDSL lists contain a pointer to stored value blocks, both Linux and FreeRTOS lists are intrusive lists in the sense of the Linux kernel terminology: the C struct containing the next and prev fields is a substructure of the list node, which implies structure accesses require more complex pointer operations. FreeRTOS lists explicitly store a pointer from substructures to owners, whereas Linux lists rely on pointer arithmetic to access containing blocks. Finally, both FreeRTOS and GDSL lists have a header that stores the number of elements in the lists. FreeRTOS list nodes store a pointer to this header. The analysis with sequences proves both PrSafe and Fc for all Linux and FreeRTOS primitives. It was also able to fully verify almost all the GDSL list library, although two cases required a manual directive to prevent aggressive folding both with and without sequences (as for bubblesort in Table 1) (they are marked with ( †) in the tables). Only two functions for the extraction of minimal/maximal values could not be fully verified with respect to Fc (note that PrSafe still gets proved): in these codes, the memory widening is too aggressive and folds the node storing the function results, which prevents proving that the returned value is indeed the extremal value in the sequence. The examples only shown in Table 3 are all verified. We conclude the analysis handles real-world programs.

Overhead. We now compare performance between the analyses with/without sequences in Tables 1 and2. While the overhead is modest for the smaller programs, it becomes higher for the more challenging cases, up to roughly 10x-20x. While significant, this cost should be considered in comparison to the much stronger properties proved (i.e., not only PrSafe but also partial correctness Fc in addition to PrSafe). We found two reasons for this increase. First, as shown in the tables, most of the increase is accounted for by the numerical abstract domain partly due to the larger number of symbolic variables that stand for sequence bounds. We believe this overhead could be much reduced with a finer-grained numerical domain packing [START_REF] Blanchet | A static analyzer for large safety-critical software[END_REF][START_REF] Singh | Fast polyhedra abstract domain[END_REF]. By contrast, the time spent in memory and sequence domains remains reasonable. Second, the analysis with sequences requires greater numbers of abstract iterates to stabilize loop iterates, as shown in the tables, which explains an important slowdown. This is to be expected due to the more complex value constraints (including polyhedra) used in the analysis with sequences.

Related works

In this section, we discuss previous works on the abstractions of sequences stored in data-structures.

Linear and contiguous structures (arrays and strings). Several previous works have tried to tie properties of container data-structures with properties of their contents. In particular, [START_REF] Gopan | A framework for numeric analysis of array operations[END_REF][START_REF] Gulwani | Lifting abstract interpreters to quantified logical domains[END_REF] have extended array abstractions with basic contents properties. More recently [START_REF] Halbwachs | Discovering properties about arrays in simple programs[END_REF] introduced array segmentations and [START_REF] Cousot | A parametric segmentation functor for fully automatic and scalable array content analysis[END_REF] made the computation of the array segmentations dynamic during the analysis. The latter two can express that an array is sorted and verify that a function produces sorted arrays. However, they do so with specific predicates rather than an abstraction for sequences. Thus, they cannot express that the set of elements in an array is preserved, which is required to prove a sorting function correct. By contrast, our sequence abstraction handles both sortedness and contents preservation.

Strings and buffers also motivated many research works, as operations on them may incur a security risk. In particular, improper handling of zero terminated strings make opens the door to buffer overrun attacks. Therefore, works such as CSSV [START_REF] Dor | Cssv: towards a realistic tool for statically detecting all buffer overflows in c[END_REF] abstract the presence or absence of zeroes in strings and their positions in order to verify buffer operations. Besides zeroes, these works do not keep any contents' information.

As noted earlier, several recent works applied concepts such as regular expressions and automata in order to build string abstract domains, that convey precise contents information [START_REF] Midtgaard | A parametric abstract domain for latticevalued regular expressions[END_REF][START_REF] Arceri | An automata-based abstract semantics for string manipulation languages[END_REF][START_REF] Negrini | Twinning automata and regular expressions for string static analysis[END_REF]. These works are typically aimed at inferring precise information on strings that denote pieces of programs meant to be computed and evaluated at runtime as in the case of JavaScript's eval construction. Automata and regular expressions are most adequate for such target properties. More recently, [START_REF] Arceri | Relational string abstract domains[END_REF] extended these works with length and element position constraints. These abstractions are not aimed at numerical sequences, and fail to express sortedness. By contrast, our sequence abstraction relies on length, extremal elements and sortedness constraints and fails to express regular expressions-based properties as these would not be useful for our intended application. An interesting area of future work would be to build a reduced product of sequence abstractions to combine the expressiveness of these works and of ours.

Shape analyses for dynamic data-structures. Many abstractions for dynamic datastructures have been proposed. Sagiv et al. introduced a shape analysis based on three value logic in [START_REF] Sagiv | Solving shape-analysis problems in languages with destructive updating[END_REF], that was later extended to handle more complex data-structures such as tree [START_REF] Loginov | Automated verification of the deutsch-schorr-waite tree-traversal algorithm[END_REF]. The seminal work by Reynolds [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF], introduced separation logic, that many analyses including ours rely upon. Separation logic has been used in order to reason over not only sequential programs [START_REF] Calcagno | Footprint analysis : A shape analysis that discovers preconditions[END_REF] but also concurrent programs [START_REF] O'hearn | Resources, concurrency and local reasoning[END_REF][START_REF] Vafeiadis | A marriage of rely/guarantee and separation logic[END_REF] and to prove properties like linearizability of concurrent data structures [START_REF] Vafeiadis | Shape-value abstraction for verifying linearizability[END_REF]. It serves as a basis for structure abstraction in several static analyzers like Smallfoot [START_REF] Calcagno | Footprint analysis : A shape analysis that discovers preconditions[END_REF], Facebook Infer [START_REF] Calcagno | Compositional shape analysis by means of bi-abduction[END_REF] (which also performs bi-abduction to synthesize pre-and post-condition pairs), Forester [START_REF] Holík | Fully automated shape analysis based on forest automata[END_REF] (which uses automata to represent abstract states), and MemCAD [START_REF] Li | Semantic-directed clumping of disjunctive abstract states[END_REF] (which features a modularized abstract domain). Bi-abduction methods have also been extended to infer inductive predicates on a per-function basis [START_REF] Le | Shape analysis via second-order bi-abduction[END_REF] or to infer pre-and postconditions for programs manipulating lists and using bit-level memory accesses and pointer arithmetic [START_REF] Holík | Low-level bi-abduction[END_REF]. All the shape abstractions mentioned so far can only keep track of very limited contents properties. Indeed, inferring precise information about the contents of dynamic datastructures is notoriously difficult, since the memory abstraction layout changes depending on the program point which makes abstraction complex. A first approach to this issue consists in splitting the analysis in two phases, where the first analysis infers only structural invariants and translates the initial program into a purely numerical program, that is taken as input by the second analysis, that discovers numerical invariants. This technique has been applied by [START_REF] Magill | Automatic numeric abstractions for heap-manipulating programs[END_REF][START_REF] Fiedor | From shapes to amortized complexity[END_REF] in order to infer complexity bounds and verify termination of programs based on information on the size of the data-structures. A second approach [START_REF] Chang | Relational inductive shape analysis[END_REF] consists of a reduced product between a memory abstract domain and a numerical abstract domain. While harder to implement, it ensures information can be communicated in both directions between the memory and the value abstract domains, whereas the staged analysis approach only lets the value abstract domain benefit from memory layout information. More recently, [START_REF] Li | Shape analysis for unstructured sharing[END_REF] combines shape and set abstractions with a reduced product which allows verifying programs on graphs. As it only considers set constraints, it does not capture any order information.

The tools CINV [START_REF] Bouajjani | Invariant synthesis for programs manipulating lists with unbounded data[END_REF] and CELIA [START_REF] Bouajjani | Abstract domains for automated reasoning about list-manipulating programs with infinite data[END_REF] (extended with interprocedural analysis support in [START_REF] Bouajjani | On inter-procedural analysis of programs with lists and data[END_REF]) are the most closely related to our approach. These static analyzers handle list manipulating programs and are parameterized by an abstract domain called a data-word domain to reason on the structure and contents of lists by attaching size or set constraints to them, or constraints quantified over the position of elements, which allows expressing sortedness. Although the heap abstraction does not make explicit use of separation logic the list abstraction follows a similar structure. A first important difference with our work is that CINV and CELIA only handle singly-linked lists, whereas our analysis supports a large range of inductive definitions included doubly linked-lists, trees, binary search trees with and without parent pointers. Indeed, our approach integrates sequence reasoning into a shape analysis that can be parameterized by a wide variety of inductive predicates. This more general scope requires extensions to the analysis algorithms, such as the automatical inference of concatenation lemmas (Lemma 1 and 2) and the use of abstract operators based on them. A second difference comes from the sequence domain and the interaction with it. The data-word domain to handle sortedness relies on a decidable fragment of first order array theory based on constraints of the form ∀y, P (y) ⇒ U (y, Q 1 , . . . ), where the guard constraint P (y) belongs to a predefined, user-provided set of guard-patterns constraining the index variables y j , and U is a conjunction of linear constraints on y j and Q i [y j ]. This domain does not manipulate symbolic sequence expressions but rather follows a structural approach. For example, the concatenation constraint S = S 1 .S 2 is expressed as

∀y 1 , y 2 , y 1 < len S1 ∧ y 2 < len S2 ⇒ S 1 [y 1 ] = S[y 1 ] ∧ S 2 [y 2 ] = S[y 2 + len S2 ].
Therefore, it requires the user to specify prior to the analysis the appropriate guard pattern. Our sequence abstraction requires no such parameterization.

Provers for memory and contents properties. Separation logic has also been used as foundation for verification tools based on entailment checking procedures, some of which also consider contents properties. Songbird [START_REF] Ta | Automated mutual explicit induction proof in separation logic[END_REF] uses a sequent-based approach to attempt deciding implication in a fragment of separation logic enriched with pure predicates. The procedure presented in [START_REF] Iosif | Deciding entailments in inductive separation logic with tree automata[END_REF] relies on tree automata to decide implications that involve inductive predicates. CSL [START_REF] Bouajjani | A logic-based framework for reasoning about composite data structures[END_REF] and SLAD [START_REF] Bouajjani | Accurate invariant checking for programs manipulating lists and arrays with infinite data[END_REF] decide entailment on a logic for singly-linked lists and the data stored in them. It handles order constraints on linear structures like lists and arrays. More recently, [START_REF] Curry | Bi-abduction for shapes with ordered data[END_REF] used bi-abduction to reason about ordered data by explicitly storing bounds on elements in the inductive predicate. This work only considers full structure predicates and does not handle segment predicates. All these tools can be used to discharge implication proof obligations and can be used in verification tools where invariants are either manually written or inferred by some other means.

Additionally, separation logic is also heavily used in approaches based on proof assistants [START_REF] Charguéraud | Characteristic formulae for the verification of imperative programs[END_REF][START_REF] Jung | Iris from the ground up: A modular foundation for higher-order concurrent separation logic[END_REF]. In that case, contents properties are naturally expressed in the proof assistant language.

Solvers for sequence properties. Finally, we remark that our language of sequence constraints based on concatenation of atoms has some similarity with the string logic that can be found in some decision procedures. Though the logic of word equations with at least two atoms is known to be undecidable [START_REF] Quine | Concatenation as a basis for arithmetic[END_REF], its quantifier free fragment has a PSPACE complete decision procedure [START_REF] Makanin | The problem of solvability of equations in a free semigroup[END_REF]. Following the work of [START_REF] Amadini | A survey on string constraint solving[END_REF] that classifies the field of string constraints solving in three main branches, the automata based approach, using finite state automata to represent the set of constraints [START_REF] Liang | A dpll(t) theory solver for a theory of strings and regular expressions[END_REF], the word based approach, that decomposes constraints using algebraic results such as Levi's lemma [START_REF] Berzish | Z3str3: A string solver with theory-aware heuristics[END_REF], and the unfolding based approach, which expresses each string variable as a bounded sequence of variables such as bit vectors [START_REF] Kiezun | Hampi: A solver for word equations over strings, regular expressions, and context-free grammars[END_REF], our abstraction can be categorized as mostly word-based. To the best of our knowledge, no SMT solver is able to reason on the sortedness of word expressions. We refer the reader to [START_REF] Amadini | A survey on string constraint solving[END_REF] for a comprehensive survey on string constraint solving. By comparison with these works, we provide an abstract domain interface on top of the sequence operation, which allows its use in a static analysis tool, following an instance of reduced product [START_REF] Cousot | Systematic design of program analysis frameworks[END_REF].

Conclusion and future works

In this paper, we presented a novel sequence abstract domain that relies on existing numerical and set abstractions, and extended a shape analysis with sequence reasoning. We demonstrated that the resulting analysis can be used in order to verify not only memory safety or structural preservation but also far more advanced correctness properties on a wide variety of inductive structures including various kinds of lists and trees. In particular, it could prove the functional correctness of several list sorting programs and of operations over binary search trees.

A combination of our analysis with a termination analysis [START_REF] Urban | The abstract domain of segmented ranking functions[END_REF][START_REF] Fiedor | From shapes to amortized complexity[END_REF] could verify not only partial correctness but also full correctness, which would be a first interesting direction for future works. Defining a reduced product over abstract domains for sequences would be also a useful research direction, as it would allow to strengthen the expressiveness of the analysis. Last, the evaluation also shows that performance of the combined analysis could be improved with the use of a more efficient dynamic packing [START_REF] Singh | Fast polyhedra abstract domain[END_REF] for relational constraints. B Detailed presentation of sequence operators ∀i ∈ [1, k -1], ∀j, j ′ , maxS i,j ≤ δi ≤ minS i+1,j ′ ∀i, ∀j, Si,j = sort(Si,j) ∀i, ∀j < j ′ , maxS i,j ≤ minS i,j ′ S = sort(S) (e) Inference rules for sortedness Fig. 12. Inference rules for guard in sequence domain So, we can apply the induction hypothesis: We know there exists some σ ′ 0 such that it only differs from σ ′ 1 when evaluated on α 1 and such that m ′ , σ ′ 0 |= M lseg s (α ′ 0 , α 1 , S ′ 1 ) * lseg s (α 1 , α 2 , S 2 ). This means that there is two disjoint

A Experimental results

Example

lenS = 0 S = [] minS > maxS S = [] S = [] S = E S ′ ∈ fv(E) ∩ Xs S ′ = [] S = E fv(E) ∩ Xn = ∅ ∀S ′ ∈ fv(E), S ′ = [] S = [] (a) Inference rules for empty sequence [α].E1 = [β].E2 α = β E1 = E2 S1.E1 = S2.E2 lenS 1 = lenS 2 S1 = S2 E1 = E2 S.E = E ′ S = [] E = E ′ (b) Inference rules to decompose equality constraints S = E S ′ ∈ fv(E) ∩ Xs minS ≤ min S ′ max S ′ ≤ maxS S = [] α ∈ Xn maxS ≤ α ≤ minS S = [α] minS = α = maxS S = E δ ∈ fv(E) ∩ Xn minS ≤ δ ≤ maxS (c)
concrete memories m ′ 1 , m ′ 2 such that -m ′ = m ′ 1 ⊎ m ′ 2 -m ′ 1 , σ ′ 0 |= M lseg s (α ′ 0 , α 1 , S ′ 1 ) -m ′
2 , σ ′ 0 |= M lseg s (α 1 , α 2 , S 2 ) Therefore, we can establish using the non-empty segment rule that: m ′′ ⊎m ′ 1 , σ ′ 0 |= M lseg s (α 0 , α 1 , S 1 ). If, we define σ 0 := σ ′ 0 {S ′ 1 → cs 1 (S ′ 1 )}, the latter still holds since S ′ 1 does not occur free in the abstract memory state, and we also know that m ′ 2 , σ 0 |= M lseg s (α 1 , α 2 , S 2 ). And σ 0 only differs from σ 1 when evaluated on α 1 . And since m = m ′′ ⊎ m ′ = m ′′ ⊎ m ′ 1 ⊎ m ′ 2 , we infer that m, σ 0 |= M m ♯ 0 . To conclude we have: m, σ 0 ∈ γ S (m ♯ 0 , σ ♯ ).

The proof of Lemma 2 is established in a similar manner, by induction on the first segment. Proof. (Concatenation lemma for binary trees, Lemma 2) We here prove the segment/full predicate concatenation. Let (m 0 , σ) be an abstract state in the concretization of (m ♯ 0 , σ ♯ m ). Therefore, we know that there exists two disjoint concrete memories m 1 and m 2 such that m 1 , σ |= M treeseg s (α, α ′ , S ′ l S ′ r ), m 2 , σ |= M tree s (α ′ , S ′ ), and m 1 ⊎ m 2 = m 0 .

Proof. The first rule is a direct consequence of the fact that for any concrete state (σ n , σ m , σ s ) ∈ Σ, σ s (S) = ε ⇔ σ n (len S ) = 0.

To establish the second one, we observe that σ s (S) = a 1 . . . a n ̸ = ε ⇒ σ n (min S ) ≤ a 1 ≤ σ n (max S ). The contraposition gives the expected result.

For the third rule, let's assume there is a sequence variable S ′ ∈ fv(E) ∩ X s such that σ s (S) ̸ = ε. By induction on E we prove that [E] s (σ n , σ s ) ̸ = ε. This contradicts the hypothesis S = [].

The fourth rule is demonstrated by induction on E. The sequence variable case is proved using the assumption that all free-variables of E are empty. The value symbolic variable case is impossible since E does not have such free variables. The other three cases (empty sequence, sort and concatenation) are straightforward. Proof. The first two rules, are a result of the fact same-length prefixes of a word are equals. For the third rule, this is a consequence of lemma 3.

Lemma 7 (Soundness of bound saturation rules). All rules described in figures 12(c) and (d) are sound.

Proof. For the first rule, the case where σ s (S ′ ) = ε is straightforward. Now consider the case that σ s (S ′ ) is non-empty, then so is σ s (S). And since any element of σ s (S ′ ) is also an element of σ s (S), the inequalities on extremal values hold.

The next three rules are straightforward.

Remark 2. We emphasize that stating that for any sequence variable S, min S ≤ max S is unsound, since we have by convention that S = [] ⇒ min S = +∞ and max S = -∞. Generally bounding from below max S and from above min S should be done with extreme care. That's why the two rules doing so are the ones implying that S is non-empty.

Lemma 8 (Soundness of inference rule for sortedness). All rules presented in figure 12(e) are sound.

Proof. The first two rules are straightforward. The third one is established by induction on E where E is the definition of S where S ′ occurs. Notice that the premise S = . . . .S ′ . . . . forbids S ′ to occur inside a call to sort.

For the last rule, let's define σ s (S) = a 1 . . . a m and take n ∈ [1, m -1]. We reason by case disjunction by considering all possible sources of a n and a i+1 .

-If both a n and a n+1 come from evaluation of value symbolic variables

[δ i ], [δ i+1 ],
then the second premise, ensures that a n ⪯ a n+1 . This case occurs when l k = 0. -If a n comes from a value symbolic variable [δ i ], and a n+1 , from a sequence variable S i+1,j , then the third hypothesis gives the expected result. -The case where a n comes from a sequence variable and a n+1 , from value symbolic variable, is proved likewise.

-Finally, let's consider the case where both a n and a n+1 come from a sequence variable. It is impossible they come from sequence variables with distinct first indexes S i,j , S i ′ ,j ′ where i ̸ = i ′ , because there is necessarily a value between the evaluation of these sequence variables. Therefore, a n and n+1 come from S i,j and S i,j ′ , respectively.

• If j = j ′ , then we conclude directly using the fourth premise.

• Otherwise, thanks to the last premise, we infer: a n ⪯ σ n (max Si,j ) ⪯ σ n (min S i,j ′ ) ⪯ a n+1 .

Remark 3. As observed in Section 3 the final premise cannot be weakened by only considering the case where j ′ = j + 1. To provide a clear counter-example, consider the abstract value defined as S = S 1 .S ′ .S 2 ∧ max S1 ≤ min S ′ ∧ max S ′ ≤ max S2 . These constraints are not sufficient to ensure that S is sorted. Indeed, one possible concrete state of this abstract value, where σ s (S) is not sorted is:

S → 3 1 S ′ → ε S 1 → 3 S 2 → 1
Proof (Soundness of verify Σ , Theorem 2). For the cases where σ ♯ s is ⊥ or the constraint is a bound constraint, the inclusion is a consequence of the definition of γ Σ .

For definition constraints, the soundness is a result of lemma 3. Let's prove the soundness of the following rule:

S = sort(S) multi S = τ mul (E) S = sort(E)
Let (σ n , σ m , σ s ) be a well-formed concrete state, Since multi S = τ mul (E) holds, there is a bijection π such that σ s (S) = a 1 . . . a k and [E] s = a π(1) . . . a π(k) . Moreover, S = sort(S), ensures that ∀i ∈ [1, k -1], a i ⪯ a i+1 .

  struct tree { struct tree *l, *r; int d; };tree(α) := | emp ∧ α = 0x0

1 / 2 if 9 // ... 10 } 11 }Fig. 2 .

 12910112 Fig. 2. Function for insertion in a binary search tree

Fig. 6 .

 6 Fig. 6. A C list data-type and the inductive summarizing predicate describing list segments

  e e ::= n | l | &l | e ⊕ e c ::= l = e | if(e){c} | while(e){c} | c; c

  [x] l (m) := x [l.f] l (m) := [l] l (m) + f [ * e] l (m) := [e] e (m) [n] e (m) := n [l] e (m) := m([l] l (m)) [&l] e (m) := [l] l (m) [e0 ⊕ e1] e (m) := f⊕([e0] e (m), [e1] e (m)) [l = e](M ) := {m[[l] l (m) → [e] e (m)] | m ∈ M } [if(e){c0}](M ) := [c0] {m ∈ M | [e] e (m) ̸ = 0} ∪ {m ∈ M | [e] e (m) = 0} [while(e){c}](M ) := {m ∈ lfpF | [e] e (m) = 0}

Fig. 7 .

 7 Fig. 7. Semantics of programs

1Fig. 8 .

 8 Fig. 8. Concretization of abstract memory states

Fig. 9 .

 9 Fig. 9. Abstract interpretation of a command

Fig. 11 .

 11 Fig. 11. Shape union between states from Figures 3(a) and 3(b) (Greek letters denote existentially quantified symbolic variables; identical colors denote similar regions).

  Inference rules for bound constraints (general case) S = sort(S) S = . . . S ′ . . . S ′′ . . . max S ′ ≤ min S ′′ S = sort(S) S = . . . [α] . . . S ′ . . . α ≤ min S ′ S = sort(S) S = . . . [α] . . . [β] . . . α ≤ β S = sort(S) S = [α] . . . α = minS (d) Inference rules for bound constraints (sorted case) S = [] S = sort(S) S = sort(E) S = sort(S) S = sort(S) S = . . . .S ′ . . . . S ′ = sort(S ′ )S = S1,1 . . . S 1,l 1 .[δ1].S2,1 . . . S k-1,l k-1 .[δ k-1 ].S k,1 . . . S k,l k ∀i, δi ≤ δi+1

Fig. 13 .

 13 Fig. 13. Concretization of tree memory predicates

Lemma 6 (

 6 Soundness of decomposition of equality constraints). All rules presented in figure 12(b) are sound.

  Sequence expressions and constraints: syntax and semantics sequence symbolic variable S and len S , min S , max S , and multi S , a concrete state is valid if and only if it maps these five variables into consistent objects. Formally: Definition 1. A concrete state is a tuple σ = (σ n , σ m , σ s ) where the functions

	σs)
	(b) Semantics
	Fig. 5.

Table 1 .

 1 Experimental results on custom examples (Time in milliseconds averaged over 100 runs. For loop iterations, disjoint loops are separated by a semicolon, nested loops by a comma, and the first number corresponds to the outer loop. For inner loops, we take the maximum number of iterations needed to stabilize it.)

			without seq		with seq parameters
	Example	time #iter all	PrSafe verified	time all num seq shape	#iter	PrSafe + Fc verified
			Singly linked list
	Push	4.0		✓	4.8	0.5 0.5	0.9		✓
	Pop	5.1		✓	5.4	0.9 1.4	0.8		✓
	Pop (empty)	4.9		✓	4.7	0.8 0.5	1.4		✓
	concat	6.5	2	✓	15.7	3.4 3.3	2.7	2	✓
	deep copy	12.1	2	✓	20.4	3.7 2.9	5.5	2	✓
	length	9.5	3	✓	45.0 22.5 5.0	8.1	3	✓
	insert at position	19.0	3	✓	101.9 61.3 7.9 12.2	3	✓
	remove at position	17.2	3	✓	92.5 55.5 6.5 12.5	3	✓
	inserting in a sorted list 13.5	3	✓	82.5 39.0 10.0	9.2	3	✓
	minimum	11.8	3	✓	92.3 42.4 11.1 16.8	3	✓
	maximum	11.8	3	✓	93.2 42.9 11.2 17.0	3	✓
	insertion sort	24.6	2, 2	✓	714.6 328.6 90.0 126.3	4, 3	✓
	bubble sort	40.6 2;2,3 ✓( †) 776.3 399.5 89.2 141.5 3;3,3	✓( †)
	merge	36.8	4	✓	352.2 180.9 41.0 54.9	4	✓
			Binary trees
	Delete leftmost	11.2	3	✓	80.5 38.2 9.4 12.0	3	✓
	Delete rightmost	11.5	2	✓	58.1 27.5 6.8	7.6	2	✓
			Binary search trees
	Insertion	25.2	2	✓	150.4 58.0 17.2 15.5	2	✓
	Delete max	22.9	2	✗	141.2 68.6 15.2 17.2	2	✓
	Delete min	22.0	3	✗	177.9 87.9 19.2 22.8	3	✓
	Search (present)	26.6	2	✓	107.2 48.6 15.7 14.4	2	✓
	Search (absent)	24.0	3	✓	76.7 29.4 11.4 11.7	3	✓
	BST to list (heap sort) 23.8	3	✓	76.5 29.2 11.4 11.7	3	✓
	list to BST (heap sort) 34.2	2,2	✓	408.0 188.0 56.5 68.4	3,2	✓

Table 2 .

 2 Experimental results on libraries programs (Time in milliseconds averaged over 100 runs.

Table 3 .

 3 Experimental results (Time in milliseconds averaged over 100 runs. For loop iterations, disjoint loops are separated by a semicolon, nested loops by a comma, and the first number corresponds to the outer loop. For inner loops, we take the maximum number of iterations needed to stabilize it.)

Acknowledgment The authors want to thank Thierry Martinez for his work on libraries used by the MemCAD analyzer. This work was supported by the VeriAMOS ANR-18-CE25-0010 French ANR project.

Following this discussion, we now study concatenation of tree segment predicates. Let us assume two disjoint regions respectively abstracted by treeseg s (α, α ′ , S ′ l S ′ r ) and by treeseg s (α ′ , α ′′ , S ′′ l S ′′ r ). Then, the union of these two regions may be abstracted by treeseg s (α, α ′′ , S l S r ) where S l = S ′ l .S ′′ l and S r = S ′′ r .S ′ r . Note that the sequence expression attached to the latter segment is calculated as

. Similar reasoning may be carried out to concatenate a segment and a full tree predicate. Based on these observations, we propose a concatenation lemma for treeseg s : Lemma 2 (Concatenation (tree case)). We assume symbolic variables α, α ′ , α ′′ and sequence variables S, S ′ , S l , S r , S

C Proof of concatenation lemma

Proof. (Concatenation lemma for list, Lemma 1) Let (m 0 , σ) be a concrete state in the concretization of m ♯ 0 , σ ♯ m . This means that there exists m ′ , m ′′ , two disjoint memory such that:

We prove that m 1 ⊎ m 1 , σ |= M lseg s (α 0 , α 2 , S ) by structural induction on the judgments used to establish that m 1 , σ |= M lseg s (α 0 , α 1 , S 1 ).

Empty case. In that situation, σ n (α 0 ) = σ n (α 1 ), σ s (S 1 ) = σ s (S), and m 0 = m 2 . By hypothesis on m 2 , we establish that m 0 , σ |= M lseg s (α 0 , α 2 , S )

Non-empty case. From the premise of this rules it follows that there exist two disjoint concrete memories m ′ 1 , m ′′ 1 , and symbolic variables α ′ 0 δ, S ′ 1 such that the following hold:

Finally, from the premise on m ′′ 1 and the latter, we apply the non-empty list segment rule to conclude that:

Furthermore, let (m, σ 1 ) be a concrete state in γ S (m ♯ 1 , σ ♯ ). We prove by induction on |σ 1 (S 1 )| that there exists σ 0 such that ∀β ̸ = α 1 , σ 0 (β) = σ 1 (β), and (m, σ 0 ) ∈ γ S (m ♯ 0 , σ ♯ ). Null case If σ 1 (S 1 ) = ε, this means that σ 1 |= s S = S 2 . So we simply define σ 0 := σ 1 {α 1 → σ 1 (α 0 )}, and we have:

-

), Therefore, we conclude that: (σ 0 , mem) ∈ γ S (m ♯ 0 , σ ♯ ). Successor case If |σ 1 (S 1 )| > 0, then σ 1 (S) ̸ = ε, and we know that the only possible rule used to establish that m, σ 1 |= M lseg s (α 0 , α 2 , S ) is the non-empty one. So we deduce that there exist m ′ , m ′′ such that for some fresh variables S ′ , α ′ 0 , δ:

That is to say σ ′ 1 maps to some fresh auxiliary sequence variable S ′ 1 the valuation of S 1 , without the first character. Note that σ ′ 1 differs from σ 1 only when evaluated at S ′ 1 (and min S1 , ...). The following holds:

We prove that m 1 ⊎ m 1 , σ |= M tree s (α 0 , S) by structural induction on the judgments used to establish that m 1 , σ |= M lseg s (α 0 , α 1 , S 1 ).

Empty case In that situation, σ n (α) = σ n (α ′ ), σ s (S ′ ) = σ s (S), and m 0 = m 2 . By hypothesis on m 2 , we establish that m 0 , σ |= M tree s (α, S)

Left case From the premise of this rules it follows that there exist two disjoint concrete memories m ′ 1 , m ′′ 1 , and symbolic variables α l , α r , α d , S ′′ , S ′′ l ; S ′′ r such that the following hold:

By induction hypothesis, we establish that m ′ 1 ⊎ m 2 , σ |= M tree s (α l , α ′ , S ′′ ). Finally, from the premise on m ′′ 1 and the latter, we apply the non-empty list segment rule to conclude that: mσ |= M tree s (α, S)

The right case is proved similarly.

D Proofs of sequence abstract operators

Proof. (Soundness of guard Σ , Theorem 1)

Lemma 3 (Soundness of definition inlining). For any definition constraints S = E and S ′ = E ′ , and any concrete state

Proof. This is proved by a simple induction on E.

Lemma 4 (Length constraints saturation). For any concrete state (σ n , σ m , σ s ) ∈ Σ, any definition constraint S = E, if σ n , σ s |= s S = E, then σ n |= n len S = τ len (E).

Proof. First, we prove by induction on

The only interesting case is when E is only a sequence variable S ′ . We simply use the hypothesis of (σ n , σ m , σ s ) ∈ Σ to conclude that σ n (len S ′ ) = |σ s (S ′ )|.

Finally, since σ n , σ s |= s S = E, we have that σ s (S) = [E] s (σ n , σ s ) = a 1 . . . a k , and because the concrete state is well-formed, we conclude that σ n (len S ) = k = [τ len ] n (σ n ).

The soundness of multi-set constraints saturation is proved in a similar manner.

Lemma 5 (Soundness of empty sequence variables detection). The rules presented in figure 12(a) are sound. That is to say, for any concrete state (σ n , σ m , σ s ) and a rule whose premises (resp. conclusions) are P i , . . . , P k (resp. C 1 , . . . , C l ), if ∀i, (σ n , σ m , σ s ) |= P i , then ∀j, (σ n , σ m , σ s ) |= C j .