Hugo Illous
email: hugo.illous@ens.fr

Matthieu Lemerre
email: matthieu.lemerre@cea.fr

Xavier Rival
email: xavier.rival@ens.fr

A Relational Shape Abstract Domain

Keywords: Static analysis, Abstract interpretation, Shape analysis, Separation Logic, Relational properties 1 Symbolic Values V α, β , δ

Static analyses aim at inferring semantic properties of programs. We distinguish two important classes of static analyses: state analyses and relational analyses. While state analyses aim at computing an over-approximation of reachable states of programs, relational analyses aim at computing functional properties over the input-output states of programs. Several advantages of relational analyses are their ability to analyze incomplete programs, such as libraries or classes, but also to make the analysis modular, using input-output relations as composable summaries for procedures. In the case of numerical programs, several analyses have been proposed that utilize relational numerical abstract domains to describe relations. On the other hand, designing abstractions for relations over input-output memory states and taking shapes into account is challenging. In this paper, we propose a set of novel logical connectives to describe such relations, which are inspired by separation logic. This logic can express that certain memory areas are unchanged, freshly allocated, or freed, or that only part of the memory was modified. Using these connectives, we build an abstract domain and design a static analysis that over-approximates relations over memory states containing inductive structures. We implement this analysis and report on the analysis of basic libraries of programs manipulating lists and trees.

While state analyses aim at computing an over-approximation of the set of the reachable states of programs, relational analyses aim at computing an over-approximation for the relations between the input and output states of programs.

Benefits of Relational Analyses. In general, sets of states are easier to abstract than state relations, which often makes states analyses simpler to design. On the other hand, abstracting relations brings several advantages.

First, state relations allow to make the analyses modular [START_REF] Cousot | Modular static program analysis[END_REF][START_REF] Popeea | Inferring disjunctive postconditions[END_REF][START_REF] Jeannet | A relational approach to interprocedural shape analysis[END_REF][START_REF] Chatterjee | Relevant context inference[END_REF][START_REF] Calcagno | Compositional shape analysis by means of bi-abduction[END_REF] and compositional. Indeed, to analyze a sequence of two sub-programs, relational analyses can simply analyze each sub-program separately, and compose the resulting state relations. When subprograms are functions, relational analyses may analyze each function separately, and compute one summary per function, so that the analysis of a function call does not require re-analyzing the body of the function, which is an advantage for scalability.

Second, some properties can be expressed on state relations but not on sets of states, which makes relational analyses intrinsically more expressive. For example, contract languages [START_REF] Baudin | ACSL: ANSI C specification language[END_REF][START_REF] Gary T Leavens | Jml: a java modeling language[END_REF][START_REF] Huu | Automated verification of shape and size properties via separation logic[END_REF][START_REF] Jacobs | The verifast program verifier[END_REF] let functions be specified by formulas that may refer both to the input and to the output states. Such properties cannot be expressed using abstractions of sets of states, thus state analyses cannot be used to infer precise function contracts.

The Need of Relational Abstractions. In general, the increased expressiveness of relational analyses requires more expressive abstractions. Let us discuss, as an example, the case of numerical programs. A common way to express relations between input and output states consists in defining for each variable x a primed version x that describes the value of x in the output state whereas the non-primed version denotes the value of x in the input state. In this context, non-relational numerical abstract domains such as intervals [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] cannot capture any interesting relation between input and output states. Conversely, relational numerical abstract domains such as convex polyhedra [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF] can effectively capture relations between input and output states, as shown in [START_REF] Popeea | Inferring disjunctive postconditions[END_REF]: for instance, when applied to a program that increments x by one, this analysis can infer the relation x = x + 1.

In the context of programs manipulating complex data structures, relational analysis could allow to compute interesting classes of program properties. For instance, such analyses could express and verify that some memory areas were not physically modified by a program. State analyses such as [START_REF] Sagiv | Parametric shape analysis via 3-valued logic[END_REF][START_REF] Distefano | A local shape analysis based on separation logic[END_REF][START_REF] Bor-Yuh | Relational inductive shape analysis[END_REF] cannot distinguish a program p 1 from a different program p 2 that has a similar behavior. For example, if p 1 inputs a list and leaves it unmodified and p 2 inputs a list, copies it into an identical version and deallocates the input list, only a relational analysis could distinguish p 1 from p 2 . More generally, it is often interesting to infer that a memory region is not modified by a program.

Separation logic [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF] provides an elegant description for sets of memory states and is at the foundation of many state analyses for heap properties. In particular, the separating conjunction connective * expresses that two regions are disjoint and allows local reasoning. On the other hand, it cannot describe relations.

Our Approach and Contributions. In this paper, we propose a logic inspired by separation logics and that can describe such relational properties. It provides connectives to describe that a memory region has been left unmodified by a program fragment, or that memory states can be split into disjoint sub-regions that undergo different transformations. It also enriches these relational connectives with sets of predicates that can describe specific transformations. We build an abstract domain upon this logic, and apply it to design an analysis for procedures 1 t y p e d e f s t r u c t list { s t r u c t list * next ; i n t data ; } list ; manipulating simple list or tree data structures, thereby automatically inferring relational function contracts for these procedures. We make the following contributions:

-In Section 2, we demonstrate the abstraction of heap relations using a specific family of heap predicates. We also propose an extension of this abstraction, that improves the expressiveness of heap relations; -In Section 4, we set up a logic to describe heap relations and lift it into an abstract domain that describes concrete relations defined in Section 3; -In Section 5, we design static analysis algorithms to infer memory state relations from abstract pre-conditions; -In Section 6, we report on experiments on basic linked data structures (lists and trees); -Finally, we discuss related works in Section 7 and conclude in Section 8.

Overview

In this section, we first compare the use of states and relational abstractions for a relational analysis. We then present an extension of the relational abstraction that improves the precision of the analysis.

Relational Analysis With State Abstraction

We consider the example code shown in Figure 1 which implements the insertion of an element inside a non empty singly linked list containing integer values. When applied to a pointer to an existing non empty list and an integer value, this function traverses the list partially (based on a condition on the values stored in list elements that is elided in the figure). It then allocates a new list element, inserts it at the selected position and copies the integer argument into the data field. For instance, Figure 2a shows an input list containing elements 0, 8, 6, 1 and an output list where value 9 is inserted as a new element in the list. We observe that all elements of the input list are left physically unmodified except the element right before the insertion point.

We now discuss a relational analysis of this program that does not use relational abstraction, but only states abstraction. We consider an abstraction based on separation logics with inductive predicates as used in [START_REF] Distefano | A local shape analysis based on separation logic[END_REF][START_REF] Bor-Yuh | Relational inductive shape analysis[END_REF]. We assume that the predicate list(α) describes heap regions that consist of a well-formed linked list starting at address α (α is a symbolic value used in the abstraction to denote a concrete address). This predicate is intuitively defined by induction as follows: it means either the region is empty and α is the null pointer, or the region is not empty, and consists of a list element of address α and with a next field containing a value described by a symbolic variable β and a region that can be described by list(β ). Thus, the valid input states for the insertion function can be abstracted by the abstract state shown on the top of Figure 2b. The analysis of the function needs to express that the insertion occurs somewhere in the middle of the list. This requires a list segment predicate listseg(α, α ), that is defined in a similar way as for list: it describes a region that stores a sub list starting at address α and the last element of which has a next field pointing to address α (note that the empty region can be described by listseg(α, α)). Using this predicate, we can now also express an abstraction for the output states of the insertion function: the abstract state shown in the bottom of Figure 2b describes the states where the new element was inserted in the middle of the structure (the list starts with a segment, then the predecessor of the inserted element, then the inserted element, and finally the list tail).

We observe that this abstraction allows to express and to verify that the function is memory safe (when applied to non-empty linked lists), and returns a well-formed list. Indeed, it captures the fact that no null or dangling pointer is ever dereferenced. Moreover, all states described by the abstract post-condition consist of a well-formed list, made of a segment, followed by two elements and a list tail. On the other hand, it does not say anything about the location of the list in the output state with respect to the list in the input state. More precisely, it cannot capture the fact that the elements of addresses a 0 , a 1 , a 3 are left unmodified physically. Finally, it does not express that the element of address a 4 has been freshly allocated by the function (this abstraction allows this element to be an element of the input list). This is a consequence of the fact that each abstract state in Figure 2b independently describes a set of concrete heaps.

Simple Heap Relations Abstraction

We now discuss a relational analysis of the code of Figure 1 using a relational abstraction based on heap abstractions.

To abstract heap relations instead of sets of heaps, we now propose to define a new structure in Figure 2c, that is based on new predicates inspired by separation logic and that partially overlays the abstractions of input and output heaps.

First, we observe that the tail of the list is not modified at all, thus, we describe it with a single predicate Id(list(β )), that denotes pairs made of an input heap and an output heap, that are physically equal and can both be described by list(β ). The same predicate can be used to describe that the initial segment has not changed between the two heaps: Id(listseg(α, α )).

Second, we need to define a counterpart for separating conjunction at the relation level. Indeed, the effect of the insertion function can be decomposed into its effect on the initial segment (which is left unchanged), its effect on the tail (which is also left unchanged) and its effect on the insertion point (where a new element is allocated and a next pointer is modified). This relation separating conjunction is noted * R. To avoid confusion, from now on, we write * S for the usual separating conjunction.

Last, the insertion function allocates a new element and modifies the value of the next field of an existing element. Thus, we need to describe relations between states where a region has been modified or allocated. To account for this, we need a new connective [• •] which is applied to two abstract heaps: if h 0 , h 1 are abstract heaps (described by formulas in the usual separation logic with inductive predicates), then [h 0 h 1 ] describes the transformation of an input heap described by h 0 into an output heap described by h 1 . This is presented with different colors in Figure 2.

Heap Relations Abstraction Extension

We now consider the code shown in Figure 3, that implements a sort of a linked list. We observe this is an in-place sort: it works directly on the input list, without allocating or deleting cells. Figure 4 illustrates this property using different colors. We can see that exactly all the memory cells in the input list (at addresses a 0 , a 1 , a 2 and a 3 ) are physically present in the output list. We also notice that each value of the data field of each list element is unchanged (the data field at address a 0 is 1, at address a 1 is 8, ...), but that only the next field of some list elements has been modified. For instance, the next field of the list element at address a 3 pointed to the null pointer, now it points to the address a 1 . We can say that the list is partially modified.

With a relational analysis using only states abstraction, we can only show that if this function inputs a well formed linked list list(α), then it outputs a well form linked list list(β ). Here again, we cannot deduce any information about how the output list is obtained. However, using the heap relations abstraction described above, we could not infer more interesting properties than an analysis using states abstraction. Indeed, we could only express the transformation of a well formed linked list into an other, that is potentially the same. The first version of our heap relation abstraction is expressive enough for programs that strictly do not modify a heap region or only modify a finite number of memory cells. It reaches its limit of precision when a program modifies partially an unbounded number of memory cells.

In this paper, we propose an extension of our heap relations abstraction, that improves a lot its precision, in a generic way. We consider first the basic version of our heap relations abstraction, where the relation [h 0 h 1 ] expresses that the input heap described by h 0 has been transformed into the output heap described by h 1 . Intuitively, for the program in Figure 3, we would like to add to this relation that the output heap contains exactly the same physical memory cells as the input list, and that the value of each of these cells is left unchanged. To achieve this, we adjoin to the [• •] connective transformation predicates that can capture various properties of the transformation. More precisely, given a set of transformation predicates T , and an element t of T , we let the relation [h 0 h 1 ] t denote pairs of heaps where the input heap is described by h 0 has been transformed into an output heap described by h 1 , and such that this pair of heaps meets the condition expressed by t . In order to keep the construction general so that other transformation predicates can easily be integrated to the analysis, we do not fix a unique T . Instead, we define a generic transformation predicate interface that comprises a set T and some analysis operations that are subject to soundness conditions. Moreover, we present several instances of this generic interface, including the one described above.

In Section 4 we formalize the heap states abstraction based on Separation logic [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF], and the new relational connectives and the relational abstraction that they define. We also formalize the extension of these connectives for any set T of transformation predicates and give examples of such predicates that describe the properties for the sort function of Figure 3.

In Section 5, we define the analysis algorithm that uses these new connectives to compute a sound over-approximation of the input-output memory states relations. It 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 starts with the identity relation of a given pre-condition at the function's entry, and computes input-output heap relations step by step. The analysis algorithms need to unfold inductive predicates to materialize cells (for instance to analyze the test at line

loc (∈ L) ::= x (x ∈ X) | loc 1 • f (loc 1 ∈ L; f ∈ F) | * exp (exp ∈ E) exp (∈ E) ::= loc (loc ∈ L) | &loc (loc ∈ L) | v (v ∈ V) | exp 1 ⊕ exp 2 (exp 1 , exp 2 ∈ E) ⊕ ::= +| -| = | = | ... p (∈ P) ::= loc = exp (loc ∈ L; exp ∈ E) | loc = malloc({f 1 , . . . , f n }) (loc ∈ L; f i ∈ F) | free(loc) (loc ∈ L) | p 1 ; p 2 (p 1 , p 2 ∈ P) | if (exp) p 1 else p 2 (exp ∈ E; p 1 , p 2 ∈ P) | while (exp) p 1 (exp ∈ E; p 1 ∈ P)
Fig. 5: Syntax of the C-like imperative programming language 5), and to fold inductive predicates in order to analyze loops. In addition to this, it also needs to reason over Id, [• •] and * R predicates, and perform operations similar to unfolding and folding on them.

Concrete Semantics

In this section, we define a concrete program semantics for a C-like imperative programming language.

Programming Language

We first consider a C-like imperative programming language, whose syntax is described in Figure 5. This language handles assignment, memory allocation and deallocation, sequences, conditionals and loops. It does not handle arrays. The sets L and E define respectively the sets of locations and expressions, and X defines the set of program variables. A location loc ∈ L designates the address of a memory cell. It can be either a program variable x, a location offset by a field (loc • f), or the value of a pointer expression ( * exp). We assume that all field names f ∈ F are implicitly converted into numerical offsets, and that 0 designates the null offset (scalars are viewed as records with only one field, which is 0). We also write exp -> f the syntactic sugar for the location ( * exp) • f. An expression exp ∈ E denotes a value. It can be the content at a memory location (loc), the address of a memory location (&loc), any value v, or a binary expression exp 1 ⊕ exp 2 . The operator ⊕ designates any standard binary operator, like addition, subtraction, equality test, etc...

Concrete Memory States

Let A be the set of addresses and V the set of values, we assume that any address a

∈ A is also a value v ∈ V, i.e. A ⊆ V. A concrete heap h ∈ H = A V is a partial function from addresses to values. We write [a 1 → v 1 ; . . . ; a n → v n ]
for the concrete heap where each cell at address a i contains the value v i , with 1 ≤ i ≤ n. We admit that all cells have the same size. We also note h[a ← v] the heap where we update the content of the cell at address a with value v in the heap h.

L x (e, h)

de f = e(x) L loc • f (e, h) de f = L loc (e, h) + f L * exp (e, h) de f = E exp (e, h) E loc (e, h) de f = h(L loc (e, h)) E &loc (e, h) de f = L loc (e, h) E v (e, h) de f = v E exp 1 ⊕ exp 2 (e, h) de f = E exp 1 (e, h) ⊕ E exp 2 (e, h)
Fig. 6: Concrete semantics for memory locations and expressions

E exp (e, h) = v L loc (e, h) = a loc = exp (e, h) ⇓ (e, h[a ← v]) p 1 (e, h) ⇓ (e , h ) p 1 ; p 2 (e, h) ⇓ p 2 (e , h ) L loc (e, h) = a h = [a + f 1 → v 1 ; . . . ; a + f n → v n ] a ∈ A, v 1 , . . . , v n ∈ V loc = malloc({f 1 , . . . , f n }) (e, h) ⇓ (e, h[a ← a ] h ) E loc (e, h) = a h = h 0 h 1 dom(h 1 ) = {a + f | f ∈ F} free(loc) (e, h) ⇓ (e, h 0 ) E exp (e, h) = 0 if (exp) p 1 else p 2 (e, h) ⇓ p 1 (e, h) E exp (e, h) = 0 if (exp) p 1 else p 2 (e, h) ⇓ p 2 (e, h) E exp (e, h) = 0 p (e, h) ⇓ (e , h ) while (exp) p (e, h) ⇓ while (exp) p (e , h ) E exp (e, h) = 0 while (exp) p (e, h) ⇓ (e, h)
Fig. 7: Concrete big-step semantics for programs

We let the domain of h, noted dom(h), be the set of addresses at which it is defined. For example, the domain for the concrete heap [a 1 → v 1 ; a 2 → v 2 ; a 3 → v 3 ] is {a 1 , a 2 , a 3 }. Additionally, if h 0 and h 1 are two concrete heaps such that dom(h 0 ) ∩ dom(h 1 ) = / 0, we let h 0 h 1 denote the concrete heap obtained by merging h 0 and h 1 (its domain is dom(h 0 ) ∪ dom(h 1 )). We also denote the null pointer by 0x0 such that 0x0 ∈ V ∧ 0x0 / ∈ A. That is, the null pointer can be considered like a value, but not like an address.

Let X be the set of program variables. A concrete environment e ∈ E = [X → A] binds each program variable x ∈ X to its numerical address a ∈ A. Thus, an environment indicates the address of a variable in the heap.

A concrete memory state m ∈ M = E × H is simply a pair made of a concrete environment and a concrete heap. Note that we do not use a stack. Consequently, the addresses of variables are also allocated in the heap.

Concrete Program Semantics

Big-step operational semantics. We assume that the semantics of a program p ∈ P is defined by a function p that maps its input memory state into its set of reachable outputs memory states (thus p : M → P(M)).

The semantics of locations and expressions are also defined by two functions, L loc : M → A and E exp : M → V, respectively from memory states into addresses and from memory

Program Syntax Name Set Element Evaluation Field F f, 0 Location L loc L loc : M → A Expression E exp E exp : M → V Program P p p : M → P(M) Memory State Name Set Element Property Value V v Address A a A ⊆ V Variable X x Heap H h H = [A V] Environment E e E = [X → A] Memory M m M = E × H
Table 1: Notations for the concrete semantics states into values. They are mutually defined by induction on the structures of locations and expressions, as shown in Figure 6. The environment provides the address of the variable x for L x (e, h) whereas E loc (e, h) first evaluates the address of the location loc, then returns the value contained in h at this address. Figure 7 describes the evaluations of programs for assignment, conditionals, loops, allocation and deallocation. An important feature with our program semantics is that we should consider that the set of addresses A is infinite, and that every allocation generates fresh addresses. In a real imperative programming language like C, the same address can be deallocated, then allocated randomly (if it is available) during the execution of a program. This feature does not allow to express that some parts of memory have been freshly allocated or deallocated between two program points whereas these are exactly the kind of properties that our work attempts to prove. Therefore, we admit for sake of simplicity that when a program needs to allocate a memory region, fresh addresses and values are generated. Note: the actual behavior of C programs could be modeled by considering addresses as pairs of (numerical address, number of allocations in the program). As this makes the formalization heavier, we have chosen to simplify it by fresh allocations.

Table 1 summarizes the notations for the concrete semantics of this language.

Concrete Program Relational Semantics. Given a program p ∈ P, we define its relational semantics p R ∈ P(M × M) by:

p R = {(m in , m out ) | m in ∈ M ∧ m out ∈ p (m in )}
We observe that p R describes the set of pairs made of an input memory state m in and an output memory state m out , where m out is obtained by executing the program p from m in .

In the following, we define an analysis to compute an over-approximation of p R .

Abstraction

In this section, we first define abstract heaps, that describe sets of memory heaps (as in [START_REF] Bor-Yuh | Relational inductive shape analysis[END_REF]). We then set up abstract heap relations that describe binary relations over memory heaps. We also extend abstract heap relations with abstract heap transformation predicates to express more Table 2: Notations for the abstract domains and meta-variables used to denote an element of the corresponding domain. precise relations between heaps. Finally we define abstract memory relations that describe relations between two memory states.

h (∈ H ) ::= emp | α • f → β (α, β ∈ V ; f ∈ F) | h 1 * S h 2 (h 1 , h 2 ∈ H ) | ind (ind ∈ Ind ) (a) Abstract heaps r (∈ R ) ::= Id(h ) (h ∈ H ) | [h i h o ] t (h i , h o ∈ H , t ∈ T ) | r 1 * R r 2 (r 1 , r 2 ∈ R ) (b) Abstract heap relations
= α (α ∈ V ) | v (v ∈ V) | p 1 ⊕ p 2 (p 1 , p 2 ∈ P ) | not(p ) (p ∈ P ) | true | false ⊕ ::= +| -| = | =, ...

Abstract Heaps

An exact heap abstraction based on separation logic.

We first consider an exact heap abstraction without unbounded dynamic data structures, that is, an abstraction of a finite number of memory cells. We assume a countable set V = {α, β , δ , . . .} of symbolic values that abstract concrete addresses and values. An abstract heap h ∈ H is a separating conjunction of region predicates that abstract separate memory regions [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF] (as mentioned above, separating conjunction is denoted by * S). Thus we write h 1 * S h 2 the abstract heap that can be split into the two independent sub-abstract heaps h 1 and h 2 . An individual cell is abstracted by an exact points-to predicate α • f → β where the memory cell at the address abstracted by α with the offset f contains the value abstracted by β . We note α → β as syntactic sugar of α • 0 → β (0 is the null offset). We also use emp to describe an empty memory region.

We now define the meaning of exact abstract heaps using a concretization function [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF], that associates abstract elements to the set of concrete elements that they describe. To concretize an abstract heap, we first need a valuation ν : V → V, a function that defines how symbolic values are bound to concrete values and addresses. We remind that h 1 h 2 denotes the concrete heap obtained by merging h 1 and h 2 when dom(h 1 ) ∩ dom(h 2 ) = / 0.

Definition 1 (Concretization of exact abstract heaps) The concretization function γ H :

H → P(H × [V → V]
) maps an abstract heap into a set of pairs made of a concrete heap and a valuation. It is defined by induction on the structure of abstract heaps as follows:

γ H (emp) = {([], ν) | ν : V → V} γ H (α • f → β ) = {([ν(α) + f → ν(β )], ν) | ν : V → V} γ H (h 1 * S h 2 ) = {(h 1 h 2 , ν) | (h 1 , ν) ∈ γ H (h 1 ) ∧ (h 2 , ν) ∈ γ H (h 2 )}
Example 1 (Exact abstract heap) The following exact abstract heap

α 0 → α 1 * S α 1 • data → α 2 * S α 1 • next → α 3 * S β 0 → β 1
describes a possible input heap for the insert function of Figure 1, where the address of l is α 0 and l points to a list of one element, and the address of v is β 0 .

Heap abstraction with summarization.

This exact abstraction of memory cells does not allow to describe all the states of unbounded dynamic data structures, such as singly linked list or trees. Thus, abstract heaps should be extended with inductive predicates to summarize memory regions of unbounded size. An inductive predicate ind ∈ Ind is defined by a finite set of rules. Each rule is a pair made of an abstract heap h and a pure formula p ∈ P that describes numerical constraints over symbolic values (although, in this paper we do not consider relational numerical constraints-in general the issue of extending a shape abstraction with numerical reasoning is non trivial and orthogonal to the scope of this paper). Figure 8a describes the syntax that defines abstract heaps while Figure 9 describes the syntax of pure formulas. The ⊕ operators of pure formulas are exactly the same as in Figure 5.

Example 2 (List inductive predicate) In the rest of the paper, we assume that data and next denote two fields corresponding to distinct offsets. The list predicate describes the structure of a singly linked list and is defined by induction as follows:

list(α) ::= {(emp, α = 0x0), (α • data → δ * S α • next → β * S list(β ), α = 0x0)}
The first rule of that definition corresponds to the empty list, so that α is the null pointer. The second rule describes the case where the list contains one element and points to an other list (α cannot be the null pointer).

Example 3 (Binary tree inductive predicate) We can define similarly the tree predicate to describe the structure of a binary tree. We assume that e, l, and r denote three fields corresponding to distinct offsets. We also can enrich the numerical constraint of the second rule to specify that all the elements of the tree are strictly positive: tree(α) ::= {(emp, α = 0x0),

(α • e → δ * S α • l → β l * S α • r → β r * S tree(β l ) * S tree(β r ), α = 0x0 ∧ δ > 0)}
Generally, inductive predicates such as list or tree summarize a memory region from a specific address. However, we often need to describe properties on different parts of a whole summarized memory region and inductive predicates are not precise enough to do that. For instance, in Figure 1, we need to express that that the insertion of the new element occurs somewhere at least after the first element of the list. Such property require a segment predicate to be expressed. Segment predicates summarize a memory region between two addresses and permit to split a whole summarized region into many contiguous summarized sub-regions. In this paper, for the sake of simplicity, we consider segment predicates as inductive predicates with an additional parameter that specifies the ending address of the summarized region. For example, the list segment predicate listseg is defined by induction as follows:

listseg(α, β ) ::= {(emp, α = β ), (α • data → δ * S α • next → γ * S listseg(γ, β ), α = 0x0 ∧ α = β )}
Thus, the listseg predicate denotes a list of any length starting at α and ending at β (when the list is empty, we have α = β ).

The concretization of inductive predicates requires a function ∆ : Ind → P fin (H × P ) that maps an inductive predicate into the finite set of rules of its definition.

Definition 2 (Concretization of inductive predicates)

The concretization function γ P :

P → P(V × [V → V]
) maps a pure formula into a set of pairs made of its concrete value and a valuation whereas γ Σ : H × P → P(H × [V → V]) concretizes pairs of abstract heap and pure formula. The concretization of inductive predicates extends the concretization of abstract heaps γ H :

γ P (α) = {(ν(α), ν) | ν : V → V} γ P (v) = {(v, ν) | ν : V → V} γ P (p 1 ⊕ p 2 ) = {(v 1 ⊕ v 2 , ν) | (v 1 , ν) ∈ γ P (p 1 ) ∧ (v 2 , ν) ∈ γ P (p 2 )} γ P (not(p )) = {(v, ν) | (0, ν) ∈ γ P (p ) ∧ v = 0} ∪ {(0, ν) | ∃v, (v, ν) ∈ γ P (p ) ∧ v = 0} γ P (true) = {(v, ν) | v = 0 ∧ ν : V → V} γ P (false) = {(0, ν) | ν : V → V} γ Σ (h , p ) = {(h, ν) | (h, ν) ∈ γ H (h ) ∧ ∃v, (v, ν) ∈ γ P (p ) ∧ v = 0} γ H (ind) = (h ,p )∈∆ (ind) γ Σ (h , p )
We remark that abstract states may contain incompatible constraints such as α = 0x0 and α → β (the address of any memory cell is non null); the above concretization function naturally maps such abstract states into the empty set.

Note that the rules of inductive predicates should not contain unsatisfiable pure formulas. Indeed such a rule would describe the empty set of states and adding it would only clutter the inductive predicate. Still it would not pose any problem to the analysis, as an unsatisfiable rule would never be unfolded or folded. In the rest of the paper we pay attention to never write such inconsistent inductive predicates.

Remark 1 (Value in the concretization of pure formulas) Let p ∈ P a pure formula and (v, ν) ∈ γ P (p ). If v = 0, that means that p is not a satisfiable pure formula (0 means false in the concrete semantics). As an example, consider that p = (α = 1) ∧ (α = 2). It is obvious that p cannot be satisfied, its concretization is thus {(0, ν) | ν : V → V}. Therefore, we can express that a pure formula p is satisfiable using the constraint v = 0 if (v, ν) ∈ γ P (p ), like we did in the definition of γ Σ in Definition 2.

Example 4 (Abstract heap with a summarized region) The following abstract heap

α 0 → α 1 * S list(α 1 )
describes all the possible input heaps for the sort function of Figure 3, where the address of l is α 0 and l points to a list of unknown length.

Abstract Heap Relations

As explained in Section 2, two abstract heaps at different program points cannot describe relations (they describe two independent sets of concrete memory heaps). Thus, we propose abstract heap relations that describe a set of pairs made of an input heap h i and an output heap h o . Abstract heap relations are defined by new logical connectives over abstract heaps (syntax is given in Figure 8b) as follows:

the identity relation Id(h ) describes pairs of heaps that are equal and both abstracted by h .

the transform-into relation [h i

h o ] describes pairs corresponding to the transformation of a heap abstracted by h i into a heap abstracted by h o . Note that we will only consider the t symbol that appears in Figure 8b from Section 4.3, for the sake of simplicity.

-the relational separating conjunction r 1 * R r 2 of two abstract heap relations r 1 and r 2 denotes a relation that can be described by combining independently the relations described by r 1 and r 2 on disjoint memory regions. The concretization of abstract heap relations also requires using valuations as it also needs to define the concrete values that symbolic values denote.

Definition 3 (Concretization of abstract heap relations)

The concretization function γ R ∈ P(H × H × [V → V]) maps an abstract heap relation into a set of triples made of an input heap, an output heap and a valuation. It is defined by induction on the structure of r :

γ R (Id(h )) = {(h, h, ν) | (h, ν) ∈ γ H (h )} γ R ([h i h o ]) = {(h i , h o , ν) | (h i , ν) ∈ γ H (h i ) ∧ (h o , ν) ∈ γ H (h o )} γ R (r 1 * R r 2 ) = {(h i,1 h i,2 , h o,1 h o,2 , ν) | (h i,1 , h o,1 , ν) ∈ γ R (r 1 ) ∧ dom(h i,1 ) ∩ dom(h o,2 ) = / 0 ∧ (h i,2 , h o,2 , ν) ∈ γ R (r 2 ) ∧ dom(h i,2 ) ∩ dom(h o,1 ) = / 0}
We remark that * R is commutative and associative. We can also define the neutral element emp R for * R that is syntactic sugar for Id(emp) and [emp emp]: we have γ R (Id(emp)) = γ R ([emp emp]).

Example 5 (Expressiveness 1) Let r 1 = Id(list(α)) and r 2 = [list(α) list(α)]. We observe that r 1 describes the identity relation applied to a well-formed linked list starting from the address α, whereas r 2 describes any transformation that inputs such a list and outputs such a list, but may modify its content, add or remove elements, or may modify the order of list elements (except for the first one which remains at address α). This means that γ R (r

1 ) ⊂ γ R (r 2 ). Example 6 (Expressiveness 2) Let r 1 = [list(α) emp] * R [emp list(β )] and r 2 = [list(α) list(β )].
The abstract heap relation r 1 describes two distinct transformations: the first one expresses the deallocation of a list starting from the address α and the second one expresses the allocation of a list starting from the address β . The abstract heap relation r 2 describes simply the transformation of a list starting from α into a list starting from β . In r 1 , we know that the two lists are physically different but in r 2 , we have no information about the output list is obtained from the input list. This means that the two lists can be either physically different, can share some memory cells, or can even be totally equal. Actually, we have γ R (r 1 ) ⊂ γ R (r 2 ).

More generally, we have the following properties:

Theorem 1 (Properties on abstract heap relations)

Let h , h 0 , h 1 , h i,0 , h i,1 , h o,0 , h o,1 be abstract heaps. Then, we have the following properties:

1. γ R (Id(h 0 * S h 1 )) = γ R (Id(h 0 ) * R Id(h 1 )) 2. γ R (Id(h )) ⊆ γ R ([h h ]) (the opposite inclusion may not hold, as observed in Exam- ple 5); 3. γ R ([h i,0 h o,0 ] * R [h i,1 h o,1 ]) ⊆ γ R ([(h i,0 * S h i,1 ) (h o,0 * S h o,1
)]) (the opposite inclusion may not hold, as observed in Example 6).

Property 1 allows to split and merge identity relations as we like. Property 2 allows to loose the identity relation on a heap, weakening it into a transform-into relation whereas Property 3 allows to forget that two relations are independent by merging respectively their inputs and output states. These properties will be useful in our static analysis described in Section 5 to compute new abstract heap relations.

Proof (Proof of Theorem 1) We are now going to prove Theorem 1. For each property, we just reduce both concretizations using their definition to show that the equality (for Property 1) or the inclusion (for Property 2 and Property 3) holds:

1. Proof of γ R (Id(h 0 * S h 1 )) = γ R (Id(h 0 ) * R Id(h 1 )): γ R (Id(h 0 * S h 1 )) = {(h, h, ν) | (h, ν) ∈ γ H (h 0 * S h 1 )} = {(h 0 h 1 , h 0 h 1 , ν) | (h 0 , ν) ∈ γ H (h 0 ) ∧ (h 1 , ν) ∈ γ H (h 1 )} γ R (Id(h 0 ) * R Id(h 1 )) = {(h 0 h 1 , h 0 h 1 , ν) | (h 0 , h 0 , ν) ∈ γ R (Id(h 0 )) ∧ (h 1 , h 1 , ν) ∈ γ R (Id(h 1 ))∧ dom(h 0 ) ∩ dom(h 1 ) = / 0 ∧ dom(h 1 ) ∩ dom(h 0 ) = / 0} = {(h 0 h 1 , h 0 h 1 , ν) | (h 0 , ν) ∈ γ H (h 0 ) ∧ (h 1 , ν) ∈ γ H (h 1 )}} So γ R (Id(h 0 * S h 1 )) = γ R (Id(h 0 ) * R Id(h 1 )) 2. Proof of γ R (Id(h )) ⊆ γ R ([h h ]): γ R (Id(h )) = {(h, h, ν) | (h, ν) ∈ γ H (h )} γ R ([h h ]) = {(h 0 , h 1 , ν) | (h 0 , ν) ∈ γ H (h ) ∧ (h 1 , ν) ∈ γ H (h )} We clearly have: γ R (Id(h )) ⊆ γ R ([h h ]) 3. Proof of γ R ([h i,0 h o,0 ] * R [h i,1 h o,1 ]) ⊆ γ R ([(h i,0 * S h i,1 ) (h o,0 * S h o,1 )]): γ R ([h i,0 h o,0 ] * R [h i,1 h o,1 ]) = {(h i,0 h i,1 , h o,0 h o,1 , ν) | (h i,0 , h o,0 , ν) ∈ γ R ([h i,0 h o,0 ])∧ (h i,1 , h o,1 , ν) ∈ γ R ([h i,1 h o,1 ])∧ dom(h i,0 ) ∩ dom(h o,1 ) = / 0 ∧ dom(h i,1 ) ∩ dom(h o,0 ) = / 0} = {(h i,0 h i,1 , h o,0 h o,1 , ν) | (h i,0 , ν) ∈ γ H (h i,0 ) ∧ (h o,0 , ν) ∈ γ H (h o,0 )∧ (h i,1 , ν) ∈ γ H (h i,1 ) ∧ (h o,1 , ν) ∈ γ H (h o,1 )∧ dom(h i,0 ) ∩ dom(h o,1 ) = / 0 ∧ dom(h i,1 ) ∩ dom(h o,0 ) = / 0} γ R ([(h i,0 * S h i,1 ) (h o,0 * S h o,1 )]) = {(h i , h o , ν) | (h i , ν) ∈ γ H (h i,0 * S h i,1 ) ∧ (h o , ν) ∈ γ H (h o,0 * S h o,1 )} = {(h i,0 h i,1 , h o,0 h o,1 , ν) | (h i,0 , ν) ∈ γ H (h i,0 ) ∧ (h o,0 , ν) ∈ γ H (h o,0 )∧ (h i,1 , ν) ∈ γ H (h i,1 ) ∧ (h o,1 , ν) ∈ γ H (h o,1 )} So finally: γ R ([h i,0 h o,0 ] * R [h i,1 h o,1 ]) ⊆ γ R ([h i,0 * S h i,1 h o,0 * S h o,1 ])

Abstract Heap Transformation Predicates

From now, we have two relational connectives that describe heap transformations: the identity relation and the transform-into relation. While the identity relation is very strong (it ensures that the heap is left unmodified), the transform-into relation is quite weak. Indeed, it just indicates that the input heap abstracted by h i has been transformed into the output heap abstracted by h o , but without describing specifically how the transformation occurred. For instance in Figure 3, the function sort performs a list sort in place, modifying only the order of its elements. A reasonable abstraction of the effects of this function is that the output list is a permutation in place of the input list.

Remark 2 (Properties to ensure) We remark that a permutation in place of a list can be expressed ensuring these two properties:

(a) the permutation is in-place, so that the output list is obtained by manipulating directly the input list (the footprint of the two lists is the same). (b) the data in the input and output lists are exactly the same (but may appear in a different order).

If we look at the abstract heap relation computed for the function sort:

[list(α) list(β )]
We observe that this abstraction is too weak to ensure the points (a) and (b), as it describes only a transformation of a well formed linked list into a well formed linked list. More generally, to capture stronger relations, abstract heap relations should be extended.

To fix this imprecision, we could enrich abstract heap relations with a new connective that would express specifically these two points. The problem with this approach is that it would be certainly useless to describe the behavior of other functions using other data structures. Moreover, creating a relational connective in abstract heap relations to express a specific property when needed is too costly. Indeed, this requires to update all the functions related to abstract heap relations for each new relational connective.

An elegant and efficient approach to describe any binary relational properties between memory heaps without adding new connectives is to annotate transform-into relations by abstract heap transformation predicates. We henceforth write [h i h o ] t for the transform-into relation annotated by the abstract heap transformation predicate t . It describes the transformation abstracted by t of the heaps abstracted by h i into the heaps abstracted by h o .

We name an abstract heap transformation predicates domain a set T of abstract heap transformation predicates. To be as generic as possible, we do not fix a specific abstract heap transformation predicates domain T . Instead, we parametrize the analysis with an interface of such T .

The concretization function γ T of an abstract heap transformation predicates domain T should have the signature: Condition 1 (Concretization) Let T be an abstract heap transformation predicates domain. Its concretization should have the following signature:

γ T : T → P(H × H × [V → V])
It simply maps an abstract heap transformation predicate into a set of triples made of an input concrete heap, an output concrete heap and a valuation function.

We can now update the concretization function γ R defined in Definition 3 (page 13) of abstract heap relations to take into account transform-into relations annotated by the abstract heap transformation predicates.

Definition 4 (Concretization of annotated transform-into relations) Let T be an abstract heap transformation predicates domain and t ∈ T , h i , h o ∈ H . Then, the concretization of transform-into relations annotated by abstract heap transformation predicates is defined as follows:

γ R ([h i h o ] t ) = {(h i , h o , ν) | (h i , ν) ∈ γ H (h i ) ∧ (h o , ν) ∈ γ H (h o ) ∧ (h i , h o , ν) ∈ γ T (t )}
Like abstract heap relations, abstract heap transformation predicates can express identity (resp. independent transformations).

To that end, each abstract heap transformation predicates domain T should define the identity id T : H → T (resp. the separating conjunction operator * T : T × T → T ), for abstract heap transformation predicates. These operators should satisfy the following conditions:

Condition 2 (Soundness of id T ) Let T be an abstract heap transformation predicates domain, t ∈ T and h ∈ H . Then id T (h ) is sound if:

{(h, h, ν) | (h, ν) ∈ γ H (h )} ⊆ γ T (id T (h ))
Condition 3 (Soundness of * T) Let T be an abstract heap transformation predicates domain and t 0 , t 1 ∈ T . Then t 0 * T t 1 is sound if:

γ T (t 0 * T t 1 ) ⊇ {(h i,0 h i,1 , h o,0 h o,1 , ν) | (h i,0 , h o,0 , ν) ∈ γ T (t 0 ) ∧ (h i,1 , h o,1 , ν) ∈ γ T (t 1 )}
Using these two operators, we can define new properties, similar to Theorem 1 (page 14), on abstract heap relations taking into account abstract heap transformation predicates.

Theorem 2 (Properties on abstract heap relations with abstract heap transformation predicates)

Let h , h i,0 , h i,1 , h o,0 , h o,1 be abstract heaps, T be an abstract heap transformation predicates domain and t , t 0 , t 1 ∈ T . Then, we have the following properties:

1. γ R (Id(h )) ⊆ γ R ([h h ] t ) with t = id T (h ) 2. γ R ([h i,0 h o,0 ] t 0 * R [h i,1 h o,1 ] t 1 ) ⊆ γ R ([(h i,0 * S h i,1 ) (h o,0 * S h o,1 )] t ) with t = t 0 * T t 1
We observe with the property 1. that the identity of abstract heap transformation predicates may be less precise than the identity relation of abstract heap relations.

Proof (Proof of Theorem 2)

To prove Theorem 2, we use the proof of the properties 2 and 3 of Theorem 1.

1. Proof of γ R (Id(h )) ⊆ γ R ([h h ] t ) with t = id T (h ):
We can prove this property exactly like we proved the property 2 of Theorem 1.

γ R (Id(h )) = {(h, h, ν) | (h, ν) ∈ γ H (h )} γ R ([h h ] t ) = {(h 0 , h 1 , ν) | (h 0 , ν) ∈ γ H (h ) ∧ (h 1 , ν) ∈ γ H (h ) ∧ (h 0 , h 1 , ν) ∈ γ T (id T (h ))}
By soundness of id T , it is obvious that:

γ R (Id(h )) ⊆ γ R ([h h ] t ), with t = id T (h ) 2. Proof of γ R ([h i,0 h o,0 ] t 0 * R [h i,1 h o,1 ] t 1 ) ⊆ γ R ([(h i,0 * S h i,1 ) (h o,0 * S h o,1 )] t ) with t = t 0 * T t 1 :
A major part of this property has been proven in the proof of Theorem 1 (property 3), the rest only relates to t 0 , t 1 and t . So for the sake of clarity, we write ". . ." for the parts of the proof that already are in the proof of Theorem 1, property 3.

γ R ([h i,0 h o,0 ] t 0 * R [h i,1 h o,1 ] t 1 ) = {(h i,0 h i,1 , h o,0 h o,1 , ν) | (h i,0 , h o,0 , ν) ∈ γ R ([h i,0 h o,0 ] t 0 )∧ (h i,1 , h o,1 , ν) ∈ γ R ([h i,1 h o,1 ] t 1 )∧ . . .} = {(h i,0 h i,1 , h o,0 h o,1 , ν) | (h i,0 , h o,0 , ν) ∈ γ T (t 0 )∧ (h i,1 , h o,1 , ν) ∈ γ T (t 1 )∧ . . .} γ R ([(h i,0 * S h i,1 ) (h o,0 * S h o,1 )] t ) = {(h i , h o , ν) | (h i , ν) ∈ γ H (h i,0 * S h i,1 )∧ (h o , ν) ∈ γ H (h o,0 * S h o,1 )∧ (h i , h o , ν) ∈ γ T (t )} = {(h i,0 h i,1 , h o,0 h o,1 , ν) | (h i,0 h i,1 , h o,0 h o,1 , ν) ∈ γ T (t ) ∧ . . .} = {(h i,0 h i,1 , h o,0 h o,1 , ν) | (h i,0 h i,1 , h o,0 h o,1 , ν) ∈ γ T (t 0 * T t 1 ) ∧ . . .}
By the soundness of * T, we observe that:

{(h i,0 h i,1 , h o,0 h o,1 , ν) | (h i,0 , h o,0 , ν) ∈ γ T (t 0 ) ∧ (h i,1 , h o,1 , ν) ∈ γ T (t 1 )} ⊆ {(h i,0 h i,1 , h o,0 h o,1 , ν) | (h i,0 h i,1 , h o,0 h o,1 , ν) ∈ γ T (t 0 * T t 1 )} So finally: γ R ([h i,0 h o,0 ] t 0 * R [h i,1 h o,1 ] t 1 ) ⊆ γ R ([(h i,0 * S h i,1 ) (h o,0 * S h o,1 )] t )
In the following, we give two examples of abstract heap transformation predicates that, when combined together, are expressive enough to ensure the properties (a) and (b) of Remark 2. The first one describes relations between the sets of addresses that define the input and output heaps. The second one describes the set of fields for which the value of all cells may have been modified. Finally we define the combination of two abstract heap transformation predicates domains.

The Footprint Predicates Domain

Recall the property (a) of Remark 2. To ensure that the sorting algorithm operates in-place, we need to express that the set of addresses of the input and the output lists are strictly equal. To do that, we can design an abstract heap transformation predicates domain that compares the set of addresses of the input and output heaps. We name the footprint predicates domain the abstract heap transformation predicates domain where T = {= , ⊆ , ⊇ , }. Each element of T compares the set of addresses that defines the input heap with the set of addresses that defines the output heap. They do not provide relations between the content of the memory cells.

Let [h i h o ] t be a transform-into relation annotated by t . Then: -If t is = , then the input heaps abstracted by h i and the output heaps abstracted h o both span over the exact same set of addresses. Obviously, this property holds when no allocation and no deallocation takes place. More generally, it also holds for all executions where no existing cell is freed and where any cell that is allocated during the execution is freed before the end of the program is reached. -If t is ⊆ (respectively ⊇ ), the set of addresses of the heaps abstracted by h i is included in (respectively includes) or is equal to the set of addresses of the heaps abstracted by h o . This indicates that only allocations (respectively deallocations) may have taken place, as the output heap is bigger than (respectively smaller than) or is equal to the input heap. -Finally, if t = , then it indicates no specific relations between the input and the output heap.

Definition 5 (Concretization of the footprint predicates domain) We give a formal meaning to the set footprint predicates domain by defining its concretization function γ T :

T → P(H × H × [V → V]): γ T (= ) = {(h i , h o , ν) ∈ H × H × [V → V] | dom(h i ) = dom(h o )} γ T (⊆ ) = {(h i , h o , ν) ∈ H × H × [V → V] | dom(h i ) ⊆ dom(h o )} γ T (⊇ ) = {(h i , h o , ν) ∈ H × H × [V → V] | dom(h i ) ⊇ dom(h o )} γ T ( ) = H × H × [V → V]
Example 7 (Expressiveness) In this example, we discuss the expressiveness of the footprint predicates domain, for each value of t in the following transform-into relation:

[list(α) list(β )] t
If t is = , then the input heap and the output heap have exactly the same footprint. When no allocation/deallocation takes place, this predicate holds (even if the order of the elements inside the list may have changed). More generally, it holds whenever no existing cell is freed and when any cell allocated during the execution is also freed during the execution. In any case, when t is = , the length and physical size of the list have not been modified. However, we have no information about the order or the value of each memory cell. If t = ⊆ (respectively t = ⊇ ), then the output list may contain more (respectively fewer) elements than the input list.

Here too, any information about the order or the value of the elements. Finally, if t = , we have any interesting information about the transformation of the input list into the output list.

More generally, we have the following properties:

Lemma 1 (Properties of the footprint predicates domain) We observe the following properties about the footprint predicates domain:

1. γ T (= ) ⊆ γ T (⊆ ) ⊆ γ T ( ) 2. γ T (= ) ⊆ γ T (⊇ ) ⊆ γ T ( ) 3. γ T (⊆ ) ∪ γ T (⊇ ) ⊆ γ T ( ) Proof (Proof of Lemma 1)
The proof of these three properties is trivial using the definition of the concretization function. Thus we do not detail it.

We can deduce from these properties that is the less precise element of T (it provides any relation). On the contrary, = is the most precise: the set of addresses of the input and output heaps are the same but not necessarily the content of each memory cell. As well, it is relevant to express that the input heap has been manipulated in place (point (a)).

Definition 6 (Function id T of the footprint predicates domain)

Let h ∈ H , then: id T (h ) = = Definition 7 (Operator * T of the footprint predicates domain) For simplicity, we define this operator with a table as follows: * T

= ⊆ ⊇ = = ⊆ ⊇ ⊆ ⊆ ⊆ ⊇ ⊇ ⊇
Theorem 3 (Soundness of id T and * T) The functions id T and * T of the footprint predicates domain satisfy respectively Condition 2 and Condition 3.

Proof (Proof of Theorem 3) The proof of this theorem is trivial. For id T , we could choose any other predicate of the domain, but the chosen one is the most precise, as expressed by Lemma 1.

The Fields Predicates Domain

When manipulating data structures, it is common that a function modifies partially the memory. For instance in Figure 3, the sort function may modify the order of the input list manipulating the next fields whereas the values of the data fields do not change. However, as data structures like linked lists are abstracted by inductive predicates that summarize memory heaps, we cannot capture the partial modification property. In our sort function, proving that only the values of the next fields may have been modified would prove that the values of data fields have not been modified. More specifically, it would ensure that all the data that are both in the input and output lists are the same. We can express the set of structure fields whose value may have changed designing an abstract heap transformation predicates domain such as T = P(F). We name this domain the fields predicates domain. Let [h i h o ] F be the transform-into relation annotated by F ∈ P(F). If f is a structure field that is not in F, then each field f of elements of the structure that is both in the input and output heaps abstracted respectively by h i and h o has the same value.

Definition 8 (Concretization of the fields predicates domain) Let F ∈ P(F). We define the concretization of the fields predicates domain γ T : P

(F) → P(H × H × [V → V]) as follows: γ T (F) = {(h i , h o , ν) ∈ H × H × [V → V] | ∀f / ∈ F, ∀a ∈ A, (a + f) ∈ dom(h i ) ∧ (a + f) ∈ dom(h o ) ⇒ h i (a + f) = h o (a + f)}
Example 8 (Expressiveness) We now discuss the expressiveness of the fields predicates domain for the following transformation-into relation:

[list(α) list(β )] t
If t = {next}, then only the next fields of the elements of the two lists may have been modified. Consequently, all the data fields of the lists elements are unchanged. We observe that the lists may have a different number of elements. For instance, the output list can be the input where we deallocated randomly some elements, without modifying the value of the data fields.

Lemma 2 (Property of the fields predicates domain) We observe the following property about the fields predicates domain:

∀F 1 , F 2 ∈ P(F), F 1 ⊆ F 2 ⇒ γ T (F 1 ) ⊆ γ T (F 2 )
Proof (Proof of Lemma 2) This proof is trivial using the definition of the concretization function.

We made the choice to use the set of fields that may have changed instead of the set of fields that have not changed for the sake of simplicity. Indeed, if we took the latest, we would have the following property:

∀F 1 , F 2 ∈ P(F), F 1 ⊇ F 2 ⇒ γ T (F 1 ) ⊆ γ T (F 2 )
that is not relevant and easy to manipulate.

Definition 9 (Function id T of the fields predicates domain)

Let h ∈ H , then: id T (h ) = {} Definition 10 (Operator * T of the fields predicates domain) Proof (Proof of Theorem 4) The proof of this theorem is trivial. For id T , we can see from Lemma 2 that the empty set is the most precise element of T . This is why we use it to define this function.

Let F 1 , F 2 ∈ P(F), then: F 1 * T F 2 = F 1 ∪ F 2

The Combined Predicates Domain

The footprint predicates domain expresses relations between the set of addresses of the input and the output heaps but does not express information about the content of memory cells. On the other side, the fields predicates domain provides information about the content of memory cells but not about addresses. If we can combine the informations given by both of these abstract heap predicates domains, we can ensure the properties (a) and (b) of Remark 2.

A reduced product [START_REF] Cousot | Systematic design of program analysis frameworks[END_REF] between the footprint and the fields predicates domains is sufficient but not modular enough. Indeed, to analyze other programs, we have to combine other abstract heap transformation predicates domains. To be the most generic as possible, we define the combined predicates domain, the abstract heap transformation predicates domain T = T 1 × T 2 as a partially reduced product of any abstract heap transformation predicates domains T 1 and T 2 , where reduction is computed as part of the abstract operations over transformation predicates (we call this produce partially reduced, since we do not require the optimum reduction to be computed by all operators).

Let [h i h o ] t be a transform-into relation annotated by t . If t is the product between two abstract heap transformation predicates t 1 ∈ T 1 and t 2 ∈ T 2 , then it describes the transformation of the heap abstracted by h i into the heap abstracted by h o by combining the transformations described both by t 1 and t 2 .

Definition 11 (Concretization of the combined predicates domain) Let T 1 and T 2 be two abstract heap transformation predicates domains and t 1 ∈ T 1 and t 2 ∈ T 2 . Let γ T 1 and γ T 2 be the concretization function of respectively T 1 and T 2 , we define the concretization function of the product between t 1 and t 2 , γ T :

T 1 × T 2 → P(H × H × [V → V]) as follows: γ T (t 1 , t 2 ) = γ T 1 (t 1 ) ∩ γ T 2 (t 2 )
Theorem 5 (Property of the combined predicates domain) Let T 1 and T 2 be two abstract heap transformation predicates domains and let T be their product. Let γ T 1 , γ T 2 and γ T be respectively their concretization functions. Then:

∀t 1,a , t 1,b ∈ T 1 , ∀t 2,a , t 2,b ∈ T 2 , γ T 1 (t 1,a ) ⊆ γ T 1 (t 1,b ) ∧ γ T 2 (t 2,a ) ⊆ γ T 2 (t 2,b ) ⇒ γ T (t 1,a , t 2,a ) ⊆ γ T (t 1,b , t 2,b )
Proof (Proof of Theorem 5) To prove this property we simply substitute γ T by its definition and we obtain:

∀t 1,a , t 1,b ∈ T 1 , ∀t 2,a , t 2,b ∈ T 2 , γ T 1 (t 1,a ) ⊆ γ T 1 (t 1,b ) ∧ γ T 2 (t 2,a ) ⊆ γ T 2 (t 2,b ) ⇒ γ T 1 (t 1,a ) ∩ γ T 2 (t 2,a ) ⊆ γ T 1 (t 1,b ) ∩ γ T 2 (t 2,b )
Definition 12 (Function id T of the combined predicates domain) Let T 1 and T 2 be two abstract heap transformation predicates domains and T their product. Let h ∈ H , then :

id T (h ) = (id T 1 (h ), id T 2 (h ))
Definition 13 (Operator * T of the combined predicates domain) Let T 1 and T 2 be two abstract heap transformation predicates domains and T their product. If t 1,a , t 1,b ∈ T 1 and t 2,a , t 2,b ∈ T 2 then:

(t 1,a , t 2,a ) * T (t 1,b , t 2,b ) = (t 1,a * T 1 t 1,b , t 2,a * T 2 t 2,b )
Theorem 6 (Soundness of id T and * T) We assume that the two abstract heap transformation predicates domains T 1 and T 2 are equiped with sound id T and * T operators. The functions id T and * T of the combined predicates domain satisfy respectively Condition 2 and Condition 3.

Proof (Proof of Theorem 6) The function id T is simply the product of the functions id T 1 and id T 2 of the sub-domains. It is easy to prove its soundness if we suppose that id T 1 and id T 2 are both sound. Similarly, we can prove that * T is sound supposing that * T 1 and * T 2 are sound.

Example 9 (Computed transform-into relation for the list sort) Using the product of the fields and the footprints predicates domains, we obtain the following transform-into relation for the list sort program in Figure 3:

[list(α) list(β )] t , with t = ({next}, = )
This abstract heap relation describes exactly the points (a) and (b) of Remark 2: the function works in place and the input and output lists have the same length, as they are defined by the same set of addresses (a). Furthermore, only the next fields of the list may have been modified, so this implies that the lists have exactly the same data (b).

The footprint and the fields predicates domains offer the advantages to be complementary and totally independent from data structures (they are not specific to linked lists). They can also express other properties like for example, if we traverse a binary tree and increment its data elements, the product of these domains is able to prove that only data may have been modified. For more specific relational properties, designing new abstract heap transformation predicates domains is possible.

Abstract Memory Relations and Disjunction Abstract Domain

Until now, we have defined abstractions for relations between two heaps. In this section, we give an abstraction for relations between two memory states. We also define an abstraction for a disjunction of memory relations.

Abstract Memory Relation

Numerical Abstract Domains. In our heap abstraction, we simply name addresses and values with symbolic values. We have no information about their concrete values. However, it is crucial in our analysis to remember whether that a pointer is null or not. Moreover, it is also necessary to be able to capture numerical invariants to increase the precision of the analysis. Such information can be captured with numerical abstract domains such as intervals [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] or convex polyhedra [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF]. Thus, we enrich our abstraction with a numerical abstract domain N . We do not fix a particular numerical abstract domain, as it does not change our analysis. It just requires to implement all the functions for numerical abstract domains and to respect their conditions of soundness provided all along in Section 5.

A numerical abstract value n ∈ N abstracts the numerical value of the symbolic values that appear in an abstract heap relation. The concretization of abstract numerical domains γ N gives a concrete value to each symbolic value. Thus, it just binds a numerical abstract value into a set a valuations:

γ N : N → P([V → V])
Abstract Memory Relations. To have a complete abstraction of memory relations, we only have to abstract environments. An abstract environment e ∈ E is simply a function that maps program variables to symbolic values that correspond to their concrete addresses (thus

E = [X → V ]).
Finally, an abstract memory relation

m R ∈ M R = E × R × N is
γ M R (e , r , n ) = {((ν • e , h i ), (ν • e , h o )) | (h i , h o , ν) ∈ γ R (r ) ∧ ν ∈ γ N (n )}
We observe that the concrete environment is always the same in the input and in the output memory as the address of a variable never changes between two program points.

Disjunction Abstract Domain

The analysis algorithm may require to unfold inductive predicates (see Section 5.2). Unfolding such predicates may generate a finite set of abstract memory relations. Consequently, the analysis needs an abstraction layer that reasons over it. We thus let D = P fin (M R ) be the disjunction abstract domain. An abstract disjunction d ∈ D simply represents a finite set of abstract memory relations.

Definition 15 (Concretization of the disjunction abstract domain)

The concretization function γ D : D → P(M × M) maps an abstract disjunction d into the pairs of its concrete input and output memories.

γ D (d ) = m R ∈d γ M R (m R )

Static Analysis Operations

We now propose a static analysis to compute the abstract memory relations that we defined in 4.4. It 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], starting from the abstract heap relation Id(h ) where h , supplied by the user, describes the heap at the function entry (e.g. states that e (x) = α eval L (x, e , r ) = (α, 0)

eval L (loc, e , r ) = (α, f) eval L (loc • g, e , r ) = (α, f + g) eval E (exp, e , r ) = (α, α) eval L ( * exp, e , r ) = (α, 0) eval L (loc, e , r ) = (α, f) r = r 0 * R Id(h * S α • f → β ) eval E (loc, e , r ) = (β , β ) eval L (loc, e , r ) = (α, f) r = r 0 * R [h i (h o * S α • f → β )] t eval E (loc, e , r ) = (β , β ) eval L (loc, e , r ) = (α, 0) eval E (&loc, e , r ) = (α, α) α fresh eval E (v, e , r ) = (α, v) eval E (exp 1 , e , r ) = (α 1 , p 1 ) eval E (exp 2 , e , r ) = (α 2 , p 2 ) α 3 fresh eval E (exp 1 ⊕ exp 2 , e , r ) = (α 3 , p 1 ⊕ p 2 ) Fig. 10: Abstract evaluation of locations eval L : L × E × R → V × F and expressions eval E : E × E × R → V × P .
We remind that 0 designs the null offset.

the first argument is a linked list). Indeed, before executing a program, any transformation has been performed on its initial state, so the initial relation of the analysis is the identity relation.

More generally, the analysis of a program p ∈ P is a function p R that over-approximates the concrete program relational semantics p R defined in Section 3.3. It inputs an abstract disjunction describing a previous transformation T done on the input before running p and returns an other abstract disjunction describing that transformation T followed by the execution of p. Thus, p R should meet the following soundness condition:

∀d ∈ D , ∀(m 0 , m 1 ) ∈ γ D (d ), ∀m 2 ∈ M, (m 1 , m 2 ) ∈ p R =⇒ (m 0 , m 2 ) ∈ γ D ( p R (d ))

Abstract Evaluation of Locations and Expressions

In this section, we define how locations and expressions are evaluated in our static analysis from abstract memory relations. We first consider only the abstract heap relations that do not contain inductive predicates. We start by defining the abstract evaluation of locations eval L : L × E × R → V × F and expressions eval E : E × E × R → V × P from an abstract environment e and an abstract heap relations r . They follow the same principles as L loc and E exp defined in 3.3 and their definition rules are given in Figure 10.

The function eval L evaluates a location into a pair of an abstract value and an offset that correspond to the address of the location in r .

The abstract evaluation eval E should return the symbolic value α ∈ V in r corresponding to the result of the concrete evaluation of an expression exp. However, if exp is of the form exp 1 ⊕ exp 2 or v, then there is no symbolic value α in r that can result from the abstract evaluation of exp. To deal with this, the function eval E returns a pair of a symbolic value α ∈ V and a pure formula p ∈ P . The pure formula p is simply a translation of the expression, and α is a (potentially fresh) name for p . The concretization of this pair is such that if (v, ν) ∈ γ P (p ), then ν(α) = v.

When the evaluation needs to read the content of a cell (when we apply eval E on a location loc), we need to look at the value stored in the cell. For instance, if eval L (loc, e , r ) = (α, f), in the case where r = Id(α • f → β ), it is obvious that the cell at address α • f contains β . In the case where r = [(α

• f → δ ) (α • f → β )] t ,
we remark that δ was the value in the cell at address α • f in the heap at the beginning of the analysis whereas β corresponds to its last value. Thus, eval E (loc, e , r ) should return (β , β ).

Theorem 7 (Soundness of eval L and eval E ) The functions eval L and eval E are sound: Let

e ∈ E , r ∈ R , (h i , h o , ν) ∈ γ R (r ), exp ∈ E and loc ∈ L then: eval L (loc, e , r ) = (α, f) ⇒ L loc (ν • e , h o ) = ν(α) + f eval E (exp, e , r ) = (α, p ) ⇒ E exp (ν • e , h o ) = ν(α) ∧ (ν(α), ν) ∈ γ P (p )
Example 10 (Abstract evaluation of the expression

(( * x) • f) + 2) We assume that e (x) = α 0 and r = Id(α 0 → α 1 ) * R [(α 1 • f → α 2 ) (α 1 • f → α 3 )] t .
We remark that eval L ( * x, e , r ) = (α 1 , 0), that eval E (( * x) • f, e , r ) = (β 1 , α 3 ) and that eval E (2, e , r ) = (β 2 , 2) where β 1 and β 2 are fresh symbolic values.

Finally, we obtain that eval E ((( * x)

• f) + 2, e , r ) = (β 3 , α 3 + 2)
, where β 3 is a fresh symbolic value.

Inductive Predicates Unfolding

In the previous section, we considered only abstract memory relations without inductive predicates. We now remove this restriction.

Unfolding Abstract Memory Relations

The abstract evaluation of a location may require to unfold inductive predicates. Indeed, when a location is summarized by an inductive predicate, there is no points-to predicate corresponding to this location and so, its abstract evaluation cannot be done. The analysis first proceeds to the unfolding [START_REF] Bor-Yuh | Relational inductive shape analysis[END_REF] of the inductive predicate in order to materialize it into points-to predicates. This is performed by the function unfold M R . This step generates a finite disjunction of abstract memory relations, where the inductive predicate has been syntactically substituted by the rules of its definition, as defined is Section 4.1 (one disjunct per rule of the inductive predicate). Also, the pure formula of each rule is evaluated and added in each disjunct of abstract memory relations. The irrelevant disjuncts with the location are discarded (for example the case where the summarized cell is null). The abstract evaluation of the location is then performed for each valid disjunct. This process is known in shape analysis as materialization of cells [START_REF] Sagiv | Parametric shape analysis via 3-valued logic[END_REF][START_REF] Distefano | A local shape analysis based on separation logic[END_REF][START_REF] Bor-Yuh | Relational inductive shape analysis[END_REF]. The abstract memory relations unfolding operator unfold M R builds upon the abstract heap relations unfolding operator unfold R , itself building upon the (defined below) abstract heap unfolding operator unfold H . The definition of unfold R requires an unfolding operation over abstract heaps unfold H : V × H → P fin (H × P ). It takes a symbolic value α which is the origin of an inductive predicate and an abstract heap h that contains this inductive predicate. It returns the set of pairs {(h u , p )} where each h u refines h following each definition rule of the inductive predicate and p is the pure formula of the corresponding rule. For instance, unfold H (α, list(α)) is

{(emp, α = 0x0), (α • next → α n * S α • data → α d * S list(α n ), α = 0x0)}. If there is no inductive predicate attached to α in h , we let unfold H (α, h ) = {(h , true)}. This operator is sound in the sense that, γ H (h ) is included in ∪{γ Σ (h u , p ) | (h u , p ) ∈ unfold H (α, h )}.
The unfolding operation over abstract heap relations unfold R : V × R → P fin (R × P ) uses unfold H to unfold the inductive predicate at abstract heap relations level.

Definition 16 (Abstract Heap Relation Unfolding) Let r ∈ R , we define the unfolding operator for abstract heap relations unfold R : V × R → P fin (R × P ):

-unfold R (α, Id(h )) = {(Id(h u ), p ) | (h u , p ) ∈ unfold H (α, h )} -unfold R (α, [h i h o ] t ) = {([h i,u h o,u ] t , p i,u ∧ p o,u ) | (h i,u , p i,u ) ∈ unfold H (α, h i ) ∧ (h o,u , p o,u ) ∈ unfold H (α, h o )} -unfold R (α, r 0 * R r 1 ) = {(r 0,u * R r 1 , p ) | (r 0,u , p ) ∈ unfold R (α, r 0 )}, when α carries an
inductive predicate in r 0 .

Unfolding an inductive predicate under an identity relation only consists on unfolding the abstract heap and conserving the identity relation over the unfolded abstract heap. Unfolding under a transform-into relation requires to unfold independently both the input and the output abstract heaps of the relation. Then, the resulting pure formula is the conjunction of the pure formulas of each unfolded abstract heaps. We remark that the unfolding does not modify the transformation predicates: indeed, as unfolding refines an existing description of a relation, the transformation that is described by this relation still holds. However, we later comment on possible precision gains where the transformation predicates also get unfolded. Finally, unfolding an inductive predicate under a relational separating conjunction consists on unfolding locally the abstract heap relation where the inductive predicate appears.

Definition 17 (Abstract Memory Relation Unfolding)

Let m R = (e , r , n ) ∈ M R , we define the unfolding operator for abstract memory relations

unfold M R : V × M R → P fin (M R ): unfold M R (α, m R ) = {(e , r u , guard N (p , n )) | (r u , p ) ∈ unfold R (α, r )}
The function unfold M R applies the pure conditions returned by unfold R using guard N . This relies on the numerical guard guard N : P × N → N that updates an abstract numerical value n taking into account the effects of a pure formula p . This numerical guard should satisfy the following condition:

Condition 4 (Soundness of guard N ) Let p ∈ P , n ∈ N . The function guard N is sound if: ν ∈ γ N (n ) ∧ (v, ν) ∈ γ P (p ) ∧ v = 0 =⇒ ν ∈ γ N (guard N (p , n ))
Intuitively, this condition asserts that the condition test operator guard N should always return an over-approximation of the valuations that satisfy the condition. It is standard in all value abstract domains that we know of.

Theorem 8 (Soundness of unfolding operators) Let γ Π : R ×

P → P(H × H × [V → V])
be the concretization function of pairs of abstract heap relation and pure formula defined as follow:

γ Π (r , p ) = {(h i , h o , ν) | (h i , h o , ν) ∈ γ R (r ) ∧ (v, ν) ∈ γ P (p ) ∧ v = 0} Let r ∈ R , m R ∈ M R and α ∈ V .
Then, the unfolding operators are sound, in the sense that:

γ R (r ) ⊆ {γ Π (r u , p ) | (r u , p ) ∈ unfold R (α, r )} γ M R (m R ) ⊆ {γ M R (m R,u ) | (m R,u ) ∈ unfold M R (α, m R )}
Example 11 (Unfolding a transform-into relation) Consider the following abstract heap relation r = [list(α) list(α)] t . Unfolding r at symbolic value α should generate four pairs of abstract heap relation and pure formula, included two cases where the pure formula is α = 0x0 ∧ α = 0x0. These cases should be discarded by guard N at the abstract memory relation level. The other remaining cases are thus:

([emp emp] t , α = 0x0 ∧ α = 0x0)
and

([(α • data → δ i * S α • next → β i * S list(β i )) (α • data → δ o * S α • next → β o * S list(β o ))] t , α = 0x0 ∧ α = 0x0).
Remark that in the latter case we obtained different symbolic values for the data and next fields of α because we have unfolded independently each abstract heap.

Example 12 (Abstract memory relation unfolding) Let us consider the analysis of the insertion function of Figure 1. This function should be applied to states where l is a non null list pointer (the list should have at least one element). The analysis should start from Id(&l → α * S list(α)) (in this example, we omit v for the sake of concision). Note that we did not specify that α is not null. Before the loop entry, the analysis computes the abstract heap relation

Id(&l → α * S list(α)) * R [emp &c → α] t .
To deal with the test c->next != NULL, the analysis should materialize α. This unfolding is performed under the Id connective, and produces:

(Id(&l → α * S α • next → α 0 * S α • data → β 0 * S list(α 0 )) * R [emp (&c → α))] t , α = 0x0)
Then, the condition α = 0x0 is kept in the numerical abstract value. We observe that we have automatically inferred that the input of the function should be non-empty, as this condition also applies to the abstract input memory. In turn, the effect of the condition test and of the assignment in the loop body can be precisely analyzed from this abstract memory relation.

Refining unfolding with abstract heap transformation predicates

Abstract heap transformation predicates can also help to gain more precision. As an example, we consider the following abstract heap relation:

[list(α 0 ) list(α 0 )] t . Unfolding α 0 will generate the disjuncts ([emp emp] t , α 0 = 0x0) and ([(α 0 • data → β 1 * S α 0 • next → β 2 * S list(β 2 )) (α 0 • data → δ 1 * S α 0 • next → δ 2 * S list(δ 2 ))] t , α 0 = 0x0).
In the second disjunct, we observe that we have no information that says whether the values of the fields next and data of α 0 are respectively the same in both sides of the

[.

.] relation. However, if we consider that we use the fields predicates domain defined in Section 4.3 and that t = {data}, we know that all next fields in this abstract relation are left unmodified. Thus, unfolding α 0 taking in account this information will generate as

second disjunct ([(α 0 • data → β 1 * S α 0 • next → α 2 * S list(α 2 )) (α 0 • data → δ 1 * S α 0 • next → α 2 * S list(α 2
))] t , α 0 = 0x0) (as only data fields may be different, we can use the same variable α 2 in both sides of the relation).

The refinement of materialization is performed by the function unfold T : V × H × H × T → P fin (H × H × P ) that refines the unfolded input and output abstract heaps at the given address, taking in account the information provided by the transformation predicate. This function should satisfy the following condition:

Condition 5 (Soundness of unfold T ) Before giving the soundness condition of unfold T , we define the concretization function γ Π :

H × H × P → P(H × H × [V → V]) of a triplet (h i,u , h o,u , p ) ∈ unfold T (α, h i , h o , t ): γ Π (h i,u , h o,u , p ) = {(h i , h o , ν) | (h i , ν) ∈ γ H (h i,u ) ∧ (h o , ν) ∈ γ H (h o,u ) ∧∃v, (v, ν) ∈ γ P (p ) ∧ v = 0}
Let T be an abstract heap transformation predicates domain, t ∈ T , h i , h o ∈ H and α ∈ V . Then unfold T is sound if:

{(h i , h o , ν) | (h i , h o , ν) ∈ γ T (t ) ∧ (h i , ν) ∈ γ H (h i ) ∧ (h o , ν) ∈ γ H (h o )} ⊆ {γ Π (h i,u , h o,u , p ) | (h i,u , h o,u , p ) ∈ unfold T (α, h i , h o , t )}}
Intuitively, we can see that unfold T (α, h i , h o , t ) propagates the information provided by t into h i and h o . The result of this propagation should not introduce more information than t .

Definition 18 (Extended definition of unfold R ) We now extend the definition of unfold R taking into account abstract heap transformations predicates:

unfold R (α, [h i h o ] t ) = {([h i,t h o,t ] t , p t ∧ p i,u ∧ p o,u ) | (h i,u , p i,u ) ∈ unfold H (α, h i ) ∧ (h o,u , p o,u ) ∈ unfold H (α, h o ) ∧(h i,t , h o,t , p t ) ∈ unfold T (α, h i,u , h o,u , t )} Remark 3
In the remainder of this paper, we assume that unfolding is already performed before reading a location or an expression. So that we do not explicit the steps when unfolding occurs.

Assignment

In this section, we define the transfer function for assignments assign M R :

L × E × M R → M R .
Remind that the concrete assignment over a pair of memory states (m i , m o ) results in an other pair of memory states (m i , m o ) where only the output state m o has been modified. Likewise the abstract assignment will keep the abstract input state unmodified. It will also preserve as many relations between the abstract input and output states as possible.

The main part of the algorithm consists in the function assign R that inputs a symbolic value α and a field f (the address), a symbolic value β (the value) and an abstract heap relation r . It performs the following steps:

1. Decompose inductively r when it is of the form r 0 * R r 1 until we find the points-to predicate whose address is α • f. The remainder of the abstract relation is integrally preserved.

If the found abstract heap relation is of the form [h i h o ] t , replace it by [h i h o ]

t where h o and t reflect respectively the assignment in the abstract heap domain and the abstract heap transformation predicates domain.

If the found abstract heap relation is of the form

Id(h ), decompose it into Id(h 1 ) * R Id(h 2 )
where h 2 only contains the points-to predicate whose address is α • f. Then decay Id(h 2 ) into [h 2 h 2 ] t where t = id T (h 2 ) tries to recover a part of the lost identity relation.

Finally, proceed to the assignment in [h 2 h 2 ] t and let Id(h 1 ) unchanged. For example (forgetting about abstract heap transformation predicates):

assign R (α, f, β , Id(h * S α • f → δ )) = Id(h ) * R [(α • f → δ ) (α • f → β )]
On top of this algorithm, assign M R evaluates the assignment loc = exp over the abstract memory relation m R = (e , r , n ) using the following steps: 1. Evaluate loc and exp with respectively eval L and eval E . Note that this may require prior unfoldings. 2. Update the abstract numerical value n with the result of the evaluation of exp, using the function assign N . 3. Update r with assign R .

Definition 19 (Assignments for abstract heap relations) We define the assignment function for abstract heap relations assign

R : V × F × V × R → R : assign R (α, f, β , r 1 ) = r 2 assign R (α, f, β , r 0 * R r 1 ) = r 0 * R r 2 t 2 = assign T (α, f, β , t 1 ) assign R (α, f, β , [h i h o * S (α • f → γ)] t 1 ) = [h i h o * S (α • f → β )] t 2 t = assign T (α, f, β , id T (α • f → δ )) assign R (α, f, β , Id(h 0 * S α • f → δ )) = Id(h 0 ) * R [α • f → δ α • f → β ] t
Case of a Relational Separating Conjunction. We now assume that r = r 0 * R r 1 . The points-to predicate at address α • f can only appear in one of r 0 or r 1 . If it appears in r 0 , the assignment should have no effect on r 1 (and vice versa).

The function assign R can thus be applied recursively on the sub-abstract heap relation where the points-to predicate appears. This relies on the same principle as the Frame rule [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF] for separation logic, but for abstract heap relations. More generally, if assign R (α, f, β , r 1 ) = r 2 ,

then assign R (α, f, β , r 0 * R r 1 ) = r 0 * R r 2 .
Case of a Transform-into Relation. In the case when r = [h 0 h 1 ] t 1 , assign R applies on h 1 the Frame rule [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF] of separation logic (separating the points-to predicate at address α • f from the rest). Then it updates this points-to predicate to point to β , producing a new abstract heap h 2 . The algorithm also needs to take into account the effects of the assignment in the abstract heap transformation predicate t 1 . This is done by assign T (α, f, β , t 1 ) that produces the abstract heap transformations predicate t 2 . So a valid definition for this assignment is

[h 0 h 2 ] t 2 .
Case of an Identity Relation. We now assume that r = Id(h ).

If h = α • f → δ * S h 0 , two preliminary steps are necessary before updating α • f. Indeed, two important points should be considered: first the points-to predicate α • f → δ cannot be substituted by α • f → β under the Id connective, because the assignment breaks the identity relation. Second, the assignment should only modify the points-to predicate α • f → δ , and should preserve the identity relation over h 0 , to improve precision. The first step consists in splitting the identity relation into two identity relations. As observed in Theorem 1, γ R (Id(h 0 * S h 1 )) = γ R (Id(h 0 ) * R Id(h 1 )). In our case, r is split into Id(α • f → δ ) * R Id(h 0 ). The first identity relation contains only the points-to predicate that is going to be modified and the second identity relation contains the other parts of h that are only read or useless during the assignment. The second step consists on weakening Id(α

• f → δ ) into a transform-into relation. In Theorem 2, we have γ R (Id(h )) ⊆ γ R ([h h ] t ) with t = id T (h ). This property allows to weaken Id(α • f → δ ) into [(α • f → δ ) (α • f → δ )] t 0 where t 0 = id T (α • f → δ ).
Recall that id T has been introduced in Section 4.3 and depends on the abstract heap transformation predicates domain T used by the analysis. After these steps, the analysis can perform the assignment in the obtained transforminto relation and preserve the split identity relation. This relies on the combination of the assignment in the cases of relational separating conjunction relations and transform-into relations. Thus, a valid definition for this assignment is

Id(h 0 ) * R [α • f → γ α • f → β ] t , with t = assign T (α, f, β , t 0 ).
Recall that h[a ← v] is the concrete heap where we update the content of the cell at address a with the value v in the concrete heap h. We now give the soundness conditions for the function assign T and the theorem soundness for the functions assign R .

Condition 6 (Soundness of assign T ) Let T be an abstract heap transformation predicates domain and t ∈ T . Let α, β ∈ V and f ∈ F, then assign T is sound if:

{(h i , h o [ν(α) + f ← ν(β )], ν) | (h i , h o ν) ∈ γ T (t )} ⊆ γ T (assign T (α, f, β , t ))
Theorem 9 (Soundness of assign R ) We assume that function assign T is sound. Let α, β ∈ V , f ∈ F and r 0 ∈ R . Assuming that Condition 6 is satisfied, the function assign R is sound:

(h 0 , h 1 , ν) ∈ γ R (r 0 ) =⇒ (h 0 , h 1 [ν(α) + f ← ν(β )], ν) ∈ γ R (assign R (α, f, β , r 0 ))
The analysis algorithm for assignments also needs to update the numerical constraints. To do this, we assume that the numerical abstract domain provides a function assign N : V × P × N → N , which satisfies the following soundness condition:

Condition 7 (Soundness of assign N ) Let β ∈ V , p ∈ P and n ∈ N , then assign N is sound if: ν ∈ γ N (n ) ∧ (v, ν) ∈ γ P (β = p ) ∧ v = 0 =⇒ ν ∈ γ N (assign N (β , p , n ))

Definition 20 (Assignment in abstract memory relations)

Let m R = (e , r 0 , n 0 ) be an abstract memory relation. If eval L (loc, e , r 0 ) = (α, f) and eval E (exp, e , r 0 ) = (β , p ), and if assign N (β , p , n 0 ) = n 1 and assign R (α, f, β , r 0 ) = r 1 , then:

assign M R (loc, exp, (e , r 0 , n 0 )) = (e , r 1 , n 1 )

The function assign M R applies respectively eval L and eval E on loc and exp. Remark that this step may unfold inductive predicates, as explained in the previous section. It then applies assign R on the address returned by eval L and the value returned by eval E . Remind that eval E returns a pair (β , p ), such as β ∈ V and p ∈ P . To keep track of the numerical constraint β = p , the abstract assignment requires a function that over-approximates this constraint and put it in the abstract numerical value n . The assign N function allows to perform this last step.

Theorem 10 (Soundness of assign M R ) We assume that function assign

N is sound. Let loc ∈ L, exp ∈ E. Let m R ∈ M R . For all (m 0 , m 1 ) ∈ γ M R (m R
) such that m 1 = (e 1 , h 1 ), then:

(m 0 , (e 1 , h 1 [L loc (m 1 ) ← E exp (m 1 )])) ∈ γ M R (assign M R (loc, exp, m R ))
Definition 21 (Assignment for abstract heap transformation predicates domains) We define the assignment function assign T : V × F × V × T → T for each abstract heap transformation predicates domain defined in Section 4.3.

1. The footprint predicates domain, T = {= , ⊆ , ⊇ , }:

assign T (α, f, β , t ) = t 2.
The fields predicates domain, T = P(F):

assign T (α, f, β , t ) = t ∪ {f}
3. The combined predicates domain, T = T 1 × T 2 :

assign T (α, f, β , (t 1 , t 2 )) = (assign T 1 (α, f, β , t 1 ), assign T 2 (α, f, β , t 2 ))
Theorem 11 (Soundness of Definition 21) The operators from Definition 21 are sound in the sense of Condition 6.

Example 13 (Assignment in transform-into relation) In this example, we consider the effect of assign

R (α 1 , f, β 2 , [h 0 h 1 ] t 1 ), with h 1 = α 1 • f → β 1 * S α 2 • g → β 2 ,
and t 1 = (= , {g}).

Applying the assignment in the combined predicates domain leads to apply the assignment in the footprint and the fields predicates abstract domains. We obtain that assign T (α 1 , f, β 2 , t 1 ) = (= , {g, f}). Then performing the assignment in h 1 produces that abstract heap h

2 = α 1 • f → β 2 * S α 2 • g → β 2 . Finally, assign R (α 1 , f, β 2 , [h 0 h 1 ] t 1 ) = [h 0 h 2 ] t 2 with t 2 = (= , {g, f}).
Example 14 (Assignment in identity relation) In this example, we consider the effect of assign R (α 0 , f, β 1 , r ) with r = Id(α 0 • f → β 0 * S h 1 ). We also admit that the analysis is using the combined predicates domain of the footprint and the fields predicates domains. After splitting r into r 0 * R r 1 such as r 0 = Id(α 0 • f → β 0 ) and r 1 = Id(h 1 ), the analysis needs to call id T on α 0 • f → β 0 to weaken r 0 . Applying the Definitions 6 , 9 and 12, id

T (α 0 • f → β 0 )
should return t 0 = (= , {}). Then, the weakening of r 0 is

[(α 0 • f → β 0 ) (α 0 • f → β 0 )] t 0 .
In turn, the analysis performs the assignment for abstract heap relations on the form r 0 * R r 1

and results

[(α 0 • f → β 0 ) (α 0 • f → β 1 )] t 2 * R Id(h 1 )
with t 2 = (= , {f}).

Allocations and Deallocations

In this section, we define the transfer functions for allocations alloc M R and deallocations free M R from abstract memory relations. We first comment on allocations.

Allocations.

The The major part of the algorithm consists in the creation of a single memory cell. This is performed by the function alloc R that inputs an abstract value β , a field f and an abstract heap relation r . It creates the cell β • f → δ (where δ is a fresh abstract value) and returns an abstract heap relation that expresses the allocation of this cell. The function alloc R also builds upon the allocation for abstract heap transformation predicates alloc T .

Definition 22 (Allocation for abstract heap relations) We define the allocation function for abstract heap relations alloc

R : V × F × R → R : alloc R (β , f, r ) = r * R [emp (β • f → δ )] t ,
where δ is fresh and t = alloc T (β , f, δ )

The definition of alloc R ensures that the new cell has been freshly allocated thanks to the transform-into relation [emp (β • f → δ )] t . It also ensures that the input abstract heap r is not affected by the allocation, by separating it from the latter transform-into relation with the relational separating conjunction * R. The function alloc T (β , f, δ ) generates a new abstract heap transformation predicate t that over-approximates the allocation of the cell β • f → δ .

Condition 8 (Soundness of alloc T ) Let T be an abstract heap predicates domain. Let β , δ ∈ V and f ∈ F. The function alloc T :

V × F × V → T is sound if: {([], [ν(β ) + f → ν(δ )], ν) ∈ H × H × [V → V]} ⊆ γ T (alloc T (β , f, δ )) Theorem 12 (Soundness of alloc R ) Let β ∈ V , f ∈ F and r ∈ R . The function alloc R is sound if: (h i , h o , ν) ∈ γ R (r ) =⇒ ∃v ∈ V, (h i , h o [ν(β ) + f → v], ν) ∈ γ R (alloc R (β , f, r ))
Definition 23 (Allocation in abstract memory relations)

Let (e , r 0 , n 0 ) be an abstract memory relation and n 1 the number of cells to allocate. We assume that eval L (loc, e , r 0 ) = (α, g) and that β is a fresh symbolic value. The abstract heap relations r 1 , . . . , r n are defined as follow: ∀i s.t.

1 i n, r i = alloc R (β , f i , r i-1 ).
Finally, if n 1 = guard N ((β = 0x0), n 0 ) and r n+1 = assign R (α, g, β , r n ), then:

alloc M R (loc, {f 1 , . . . , f n }, (e , r 0 , n 0 )) = (e , r n+1 , n 1 )
Like abstract assignments, the function alloc M R evaluates the location loc with eval L into a pair (α, g) (this step may also unfold inductive predicates). It then generates a fresh symbolic value β , that is the base address of the block being created. For each fields

f i ∈ {f 1 , . . . , f n }, it applies assign R (β , f i , r i-1 )
, where r i-1 has accumulated the allocations of the previous cells. Once the full block is allocated, it saves the fact that the address of the new block is not null with guard N ((β = 0x0), n 0 ) and assigns this address to the given location with assign R (α, g, β , r n ).

Theorem 13 (Soundness of alloc

M R ) Let loc ∈ L, f 1 , . . . , f n ∈ F and m R ∈ M R . If (m 0 , (e, h)) ∈ γ M R (m R ) then: ∃a ∈ A, v 1 , . . . , v n ∈ V, (m 0 , (e, h[L loc (e, h) ← a ] [a + f 1 → v 1 , . . . , a + f n → v n ])) ∈ γ M R (alloc M R (loc, {f 1 , . . . , f n }, m R )
Definition 24 (Allocation for abstract heap transformation predicates domains) We define the allocation function alloc T : V × F × V → T for each abstract heap transformation predicates domain defined in Section 4.3.

1. The footprint predicates domain, T = {= , ⊆ , ⊇ , }:

alloc T (β , f, δ ) = ⊆ 2.
The fields predicates domain, T = P(F):

alloc T (β , f, δ ) = {} 3. The combined predicates domain, T = T 1 × T 2 : alloc T (β , f, δ ) = (alloc T 1 (β , f, δ ), alloc T 2 (β , f, δ ))
Theorem 14 (Soundness of Definition 24) The operators from Definition 24 are sound in the sense of Condition 8.

Example 15 (Allocation of a list element) We consider the analysis of the following statement, from the abstract memory relation (e , r , n ), with e (p) = α 0 and r = Id(α 0 → α 1 ):

p = malloc({next; data})
The abstract heap relation computed in this case is:

[(α 0 → α 1 ) (α 0 → β )] t 0 * R [emp (β • next → β 1 )] t 1 * R [emp (β • data → β 2 )] t 2
with t 0 = (= , {0}) and t 1 = t 2 = (⊆ , {}).

Deallocations.

The function free M R (loc, (e , r , n )) returns an abstract memory relation that over-approximates the effect of the statement free(loc). It represents the deletion of the memory block pointed by loc. The resulting abstract memory relation should express the absence of cells that were present in its input state. Similarly to abstract allocation, the abstract deallocation of the memory block can be done cell per cell. The function free R inputs a symbolic value α, a field f and an abstract heap relation r . It returns an abstract heap relation where the points-to predicate whose address is α • f has been deleted in the output abstract heap of r . It also builds upon the function for deallocation of abstract heap transformation predicates free T .

Definition 25 (Deallocation for abstract heap relations) We define the deallocation function for abstract heap relations free

R : V × F × R → R : t 1 = free T (α, f, t 0 ) free R (α, f, [h i h o * S (α • f → β )] t 0 ) = [h i h o ] t 1 free R (α, f, r 1 ) = r 2 free R (α, f, r 0 * R r 1 ) = r 0 * R r 2 t = free T (α, f, id T (α • f → β )) free R (α, f, Id(h * S α • f → β )) = Id(h ) * R [α • f → β emp] t
To perform the deallocation in an abstract heap relation r , the function free R (α, f, r ) should express the absence of the memory cell at address α • f in the concrete output heaps of r .

If (h i , h o [ν(α) + f → v], ν) ∈ γ R (r ), then (h i , h o , ν) should be in γ R (free R (α, f, r )).
The definition of free R follows the same principles than assign R in Section 5.3:

-When r = [h i (h o * S α • f → β )] t 0 , the function free R (α, f, r ) should return the abstract heap relation [h i h o ] t 1 .
The function free T (α, f, t 0 ) returns the abstract heap transformation predicate t 1 that over-approximates the deallocation of the cell from t 0 .

-When r = r 0 * R r 1 , if the cell to delete is in r 0 , free R is called recursively on r 0 (we apply the Frame rule [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF] but for abstract heap relations). Similarly to abstract assignment, if free R (α, f, r 1 ) = r 2 , then free R (α, f, r 0 * R r 1 ) = r 0 * R r 2 .

-When r = Id(h * S α • f → β ), the abstract deallocation proceeds exactly like the abstract assignment. It first splits r into Id(h ) * R Id(α • f → β ), then weakens the right hand

identity relation into [(α •f → β ) (α •f → β )] t 0 with t 0 = id T (α •f → β ),
{(h i , h o , ν) | ∃v ∈ V, (h i , h o [ν(α) + f → v], ν) ∈ γ T (t )} ⊆ γ T (free T (α, f, t )) Theorem 15 (Soundness of free R ) Let α ∈ V , f ∈ F and r ∈ R . Then the function free R is sound: ∃v ∈ V, (h i , h o [ν(α) + f → v], ν) ∈ γ R (r ) =⇒ (h i , h o , ν) ∈ γ R (free R (α, f, r ))
The function free M R mainly builds upon free R . It also requires to evaluate the base address of the block to delete and to obtain the set of fields of the block. For simplicity, we admit that those fields are provided by the function get_fields. It inputs an abstract value α (that corresponds to the base address of the block), an abstract heap relation r and returns the set of fields attached to α in r .

Definition 26 (Deallocation in abstract memory relations)

Let (e , r 0 , n ) be an abstract memory relation and n 1 the number of cells to deallocate. We assume that eval E (loc, e , r 0 ) = (α, α) and { f 1 , . . . , f n } = get_fields(α, r 0 ). The abstract heap relations r 1 , . . . , r n are defined as follow:

∀i,

1 i n, r i = free R (α, f i , r i-1
).

Finally we have: free M R (loc, (e , r 0 , n )) = (e , r n , n )

The function free M R evaluated the base address α of the block pointed by loc with eval E .

It obtains the fields of the cells to delete { f 1 , . . . , f n } with get_fields(α, r 0 ). For each field

f i ∈ { f 1 , . . . , f n }, it applies free R (α, f i , r i-1
) where r i-1 has accumulated the deletion of the previous cells. Finally, r n describes the deallocation of the entire block.

Theorem 16 (Soundness of free

M R ) Let loc ∈ L and m R ∈ M R . If (m 0 , (e, h 1 h 1 )) ∈ γ M R (m R ) such that: dom(h 1 ) = {E loc (e, h 1 ) + f | f ∈ F} then: (m 0 , (e, h 1 )) ∈ γ M R (free M R (loc, m R ))
Definition 27 (Deallocation for abstract heap transformation predicates domains) We define the deallocation function free T : V ×F×T → T for each abstract heap transformation predicates domain defined in Section 4.3.

1. The footprint predicates domain, T = {= , ⊆ , ⊇ , }:

free T (α, f, = ) = ⊇ free T (α, f, ⊇ ) = ⊇ free T (α, f, ⊆ ) = free T (α, f, ) =
2. The fields predicates domain, T = P(F):

free T (α, f, t ) = t 3. The combined predicates domain, T = T 1 × T 2 : free T (α, f, (t 1 , t 2 )) = (free T 1 (α, f, t 1 ), free T 2 (α, f, t 2 )) Theorem
0 → α 1 * S α 1 • next → α 2 ) * R [h i (h o * S α 1 • data → α 3 )] t 0 .
Thus, the abstract heap relation computed for the instruction free(p) is:

Id(α 0 → α 1 ) * R [(α 1 • next → α 2 ) emp] t 1 * R [h i h o ] t 2
with t 1 = (⊇ , {}) and t 2 = (⊇ , {data}).

Local Variables Initialization and Deletion.

The declaration or the initialization of a local variable to a program block is also considered as an allocation. This is justified by the fact that we do not distinguish the heap and the stack, and that a new program variable does not belong to the initial input memory state. Similarly, when we exit a program block, we deallocate all the addresses of local variables to this block.

Condition Tests

In this section, we define the transfer function

guard M R : E × M R → M R for condition tests. It
evaluates the boolean expression of a condition test and returns an abstract memory relation that has taken into account the effects of the expression. It first translates the expression into a pure formula with eval E (note that this step may perform materialization). Finally, it updates the abstract numerical value interpreting the pure formula with the function guard N , introduced in Section 5.2.

Definition 28 (Condition test in abstract memory relations)

Let (e , r , n 0 ) be an abstract memory relation and exp an expression.

If eval E (exp, e , r ) = (α, p ) and n 1 = guard N (p , n 0 ), then:

guard M R (exp, (e , r , n 0 )) = (e , r , n 1 )
Theorem 18 (Soundness of guard M R )

Let exp ∈ E and m R,0 , m R,1 ∈ M R . If m R,1 = guard M R (exp, m R,0 ), then: ∀(m i , m o ) ∈ γ M R (m R,0 ), E exp (m o ) = 0 =⇒ (m i , m o ) ∈ γ M R (m R,1 )
Example 17 (Condition test) Consider the following condition test:

if(l -> next == 0x0)
applied to the abstract memory relation m R = (e , r , n ) where

r = Id(α 0 → α 1 * S list(α 1 )
) and e (l) = α 0

The analysis first unfolds the inductive predicate list(α 1 ) into a points-to predicate and obtains the following abstract heap relation:

Id(α 0 → α 1 * S α 1 • data → δ * S α 1 • next → α 2 * S list(α 2 ))
It then saves the constraint α 2 = 0x0 in the numerical abstract value n .

Inclusion Checking

Like classical shape analyses [START_REF] Distefano | A local shape analysis based on separation logic[END_REF][START_REF] Bor-Yuh | Relational inductive shape analysis[END_REF], our analysis needs to fold inductive predicates so as to (conservatively) decide inclusion and join abstract states. We first present the inclusion checking algorithm in this section. Inclusion checking is used to verify logical entailment, to check the convergence of loop iterates, and to support the join / widening algorithm. It consists of a conservative function isle M R that inputs two abstract memory relations m R,0 = (e 0 , r 0 , n 0 ) and m R,1 = (e 1 , r 1 , n 1 ), that either returns true (meaning that the inclusion of concretizations holds) or false (meaning that the analysis cannot conclude that inclusion holds). An important feature of inclusion checking is that the underlying abstract heaps may have distinct sets of symbolic values. Yet, to compare abstract heaps, the algorithm requires to compare symbolic values. That is, the inclusion checking algorithm requires a renaming function Ψ : V → V that maps symbolic values of m R,1 into symbolic values of m R,0 in order to maintain a notion of equivalence between symbolic values.

The definition of inclusion checking consists in three steps: the generation of an initial renaming function from the abstract environments of the two abstract memory relations, the inclusion checking in abstract heap relations that checks inclusion but also refines the renaming function, and the inclusion checking in the numerical abstract domain that makes use of the latter renaming function.

Generation of an initial renaming function. First, the abstract environment domain generates an initial renaming function Ψ init . It is clear that each program variable should be mapped to the same address, thus the initial renaming function is defined as follows: ∀x ∈ X,Ψ init (e 1 (x)) = e 0 (x).

h is not of the form h 0 * S h 1 h H h ( = ) h H list(β ) listseg(α, β ) * S h H list(α) ( seg ) h 0,0 H h 1,0 h 0,1 H h 1,1 h 0,0 * S h 0,1 H h 1,0 * S h 1,1 ( * S ) α carries an inductive predicate in r 1 (r u , p ) ∈ unfold R (α, r 1 ) r 0 R r u r 0 R r 1 ( unfold ) h 0 H h 1 Id(h 0 ) R Id(h 1 ) ( Id ) t 0 T t 1 h i,0 H h i,1 h o,0 H h o,1 [h i,0 h o,0 ] t 0 R [h i,1 h o,1 ] t 1 ( ) r 0,0 R r 1,0 r 0,1 R r 1,1 r 0,0 * R r 0,1 R r 1,0 * R r 1,1 ( * R ) Id(h 0 ) * R Id(h 1 ) * R r R r 1 Id(h 0 * S h 1 ) * R r R r 1 ( Id-split L ) r 0 R Id(h 0 ) * R Id(h 1 ) * R r r 0 R Id(h 0 * S h 1 ) * R r ( Id-split R ) t 0 = id T (h ) r * R [h h ] t 0 R [h i h o ] t 1 r * R Id(h ) R [h i h o ] t 1 ( Id-weak ) t 2 = t 0 * T t 1 r * R [h i,0 * S h i,1 h o,0 * S h o,1 ] t 2 R [h i h o ] t r * R [h i,0 h o,0 ] t 0 * R [h i,1 h o,1 ] t 1 R [h i h o ] t ( -weak )

Fig. 11: Inclusion checking rules

Inclusion checking in abstract heap relations. Then, the analysis proceeds to the inclusion checking of two abstract heap relations. It consists of a function isle R (Ψ , r 0 , r 1 ) over the abstract heap relations r 0 and r 1 where Ψ is an initial renaming function. The inclusion holds if it returns (Ψ , true) where Ψ is the final renaming function. It requires a function isle H (Ψ , h 0 , h 1 ) that returns (Ψ , true) if the inclusion of abstract heaps h 0 and h 1 holds and extends Ψ into Ψ . It also requires a conservative function isle T over abstract heap transformation predicates. The definition of isle R , isle H and isle T relies on a conservative algorithm, that implements a proof search, based on the rules shown in Figure 11 (for clarity, we omit the pure formulas inclusion checking). We do not detail the algorithm to compute isle R , isle H and isle T , we rather focus on the correctness of the rules system on which they are based.

In this rules system, we assume that the renaming function has already been performed on abstract heaps. Thus, we do not show how the renaming function is extended (this is made fully explicit in [10, Figure 6]), as the issue is orthogonal to the reasoning over abstract heap relations which is the goal of this paper. This rules system is based on three operators, H , R and T , that respectively reason over abstract heaps, abstract heap relations and abstract heap transformation predicates. They satisfy the following properties:

h 0 H h 1 =⇒ γ H (h 0 ) ⊆ γ H (h 1 ) r 0 R r 1 =⇒ γ R (r 0 ) ⊆ γ R (r 1 ) t 0 T t 1 =⇒ γ T (t 0 ) ⊆ γ T (t 1 )
The rules ( = ), ( seg ) and ( * S ) are specific to reasoning about abstract heaps, and are directly inspired from [10, Figure 6] (they allow to reason over equal abstract regions, over segments, and over separating conjunction). The rule ( unfold ) allows to unfold inductive predicates as part of the inclusion checking process, at the level of relations. The rules ( Id ) and (

) are the canonic rules for abstract heap relations. They apply H on the abstract heaps contained in the abstract heap relations. The rule ( * R ) makes inclusion checking as local. Finally, the rules ( Id-split L ), ( Id-split R ), ( Id-weak ), and ( -weak ) allow to derive inclusion over abstract heap relations, and implement the properties observed in Theorem 1 (page 14) and Theorem 2 (page 17). Thus, their correctness derives from these properties. The proof search algorithm starts from the goal to prove, and attempts to apply these rules so as to get a complete derivation (i.e. a formal proof for which each step is one of the inclusion rule). Inclusion checking in the numerical abstract domain. Finally, the analysis proceeds to the inclusion checking between the two abstract numerical values n 0 and n 1 , modulo the renaming function Ψ that results from isle R . Thus the numerical abstract domain should provide a function isle N :

[V → V ] × N × N → {true, false}. Definition 29 (Inclusion checking in abstract memory relations) Let m R,0 = (e 0 , r 0 , n 0 ) ∈ M R and m R,1 = (e 1 , r 1 , n 1 ) ∈ M R . ∀x ∈ X, Let Ψ init (e 1 (x)) = e 0 (x).
If isle R (Ψ init , r 0 , r 1 ) = (Ψ , true) and isle N (Ψ , n 0 , n 1 ) = true, then:

isle M R (m R,0 , m R,1 ) = true
That is, the function isle M R calls isle R with the initial renaming function Ψ init . If the inclusion holds for the two abstract heap relations r 0 and r 1 , it tests the inclusion of the abstract numerical values n 0 and n 1 with the resulting renaming function of isle R .

Theorem 19 (Soundness of inclusion checking)

If h 0 , h 1 ∈ H , r 0 , r 1 ∈ R , Ψ ,Ψ : V → V and m R,0 , m R,1 ∈ M R then: isle H (Ψ , h 0 , h 1 ) = (Ψ , true) =⇒ ∀(h, ν) ∈ γ H (h 0 ), (h,Ψ • ν) ∈ γ H (h 1 ) ∧ ∀α, β ∈ V ,Ψ (α) = β ⇒ Ψ (α) = β isle R (Ψ , r 0 , r 1 ) = (Ψ , true) =⇒ ∀(h i , h o , ν) ∈ γ R (r 0 ), (h i , h o ,Ψ • ν) ∈ γ R (r 1 ) ∧ ∀α, β ∈ V ,Ψ (α) = β ⇒ Ψ (α) = β isle M R (m R,0 , m R,1 ) = true =⇒ γ M R (m R,0 ) ⊆ γ M R (m R,1 )
The soundness of this definition requires that the functions isle N and isle T satisfy respectively the following conditions:

Condition 10 (Soundness of isle N ) Let Ψ : (V → V ) and n 0 , n 1 ∈ N . Then:

isle N (Ψ , n 0 , n 1 ) = true ⇒ ∀ν ∈ γ N (n 0 ), Ψ • ν ∈ γ N (n 1 )
Condition 11 (Soundness of isle T ) Let Ψ : V → V and t 0 , t 1 ∈ T , if isle T (Ψ , t 0 , t 1 ) = true then:

(h i , h o , ν) ∈ γ T (t 0 ) ⇒ (h i , h o ,Ψ • ν) ∈ γ T (t 1 )
Definition 30 (Inclusion in abstract heap transformation predicates domains) We define the inclusion function isle T :

[V → V ] × T × T →
isle T (Ψ , t 0 , t 1 ) = t 0 ⊆ t 1 3. The combined predicates domain, T = T a × T b : isle T (Ψ , (t a,0 , t b,0 ), (t a,1 , t b,1 )) = isle T a (Ψ , t a,0 , t a,1 ) ∧ isle T b (Ψ , t b,0 , t b,1 )
Theorem 20 (Soundness of Definition 30) The operators from Definition 30 are sound in the sense of Condition 11.

The soundness of this definition is proven using respectively Lemma 1 (page 19), Lemma 2 (page 21) and Theorem 5 (page 22).

Example 18 (Inclusion checking) Let us consider the following abstract heap relations r 0 and r 1 , and discuss the computation of isle R (Ψ , r 0 , r 1 ). For simplicity, we suppose that r 0 and r 1 share the same set of symbolic values (i.e. the renaming function Ψ has been already computed and applied):

r 0 = Id(α • next → α 0 * S list(α 0 )) * R [α • data → α 1 α • data → α 2 ] t 0 , with t 0 = (= , {data}) r 1 = [list(α) list(α)] t 1 , with t 1 = (= , {data, next})
Using first the rule ( Id-weak ) then the rule ( -weak ), this goal gets reduced into checking the inclusion

[h 0 h 1 ] t 2 R r 1 , where h 0 = α • next → α 0 * S list(α 0 ) * S α • data → α 1 and h 1 = α • next → α 0 * S list(α 0 ) * S α • data → α 2
and t 2 = (= , {data}). In turn, this inclusion follows from rule ( unfold ). In the following, we define the abstract operator join M R . This operator computes an overapproximation of the union of abstract memory relations. Like for the inclusion checking, join M R inputs two abstract memory relations m R,0 = (e 0 , r 0 , n 0 ) and m R,1 = (e 1 , r 1 , n 1 ), but instead of a boolean, outputs a new abstract memory relation m R = (e , r , n ). It is defined such that the union of the concretizations of m R,0 and m R,1 is included in the concretization of m R .

h 0 H h 1 h Id(h 0 ) R Id(h 1 ) Id(h ) ( Id ) t 0 T t 1 t h i,0 H h i,1 h i h o,0 H h o,1 h o [h i,0 h o,0 ] t 0 R [h i,1 h o,1 ] t 1 [h i h o ] t ( ) r 0,0 R r 1,0 r 0 r 0,1 R r 1,1 r 1 r 0,0 * R r 0,1 R r 1,0 * R r 1,1 r 0 * R r 1 ( * R ) t 0 = id T (h 0 ) [h 0 h 0 ] t 0 R [h i,1 h o,1 ] t 1 r Id(h 0 ) R [h i,1 h o,1 ] t 1 r ( Id-weak ) Id(h 0 * S h 1 ) * R r 0 R r 1 r Id(h 0 ) * R Id(h 1 ) * R r 0 R r 1 r ( Id-merge ) t = t 0 * T t 1 [h i,0 * S h i,1 h o,0 * S h o,1 ] t * R r 0 R r 1 r [h i,0 h o,0 ] t 0 * R [h i,1 h o,1 ] t 1 * R r 0 R r 1 r ( -weak ) t 0 = id T (h 0 ) [h 0 h 0 ] t 0 * R [h i,1 h o,1 ] t 1 * R r 0 R r 1 r Id(h 0 ) * R [h i,1 h o,1 ] t 1 * R r 0 R r 1 r ( -intro )
The creation of a new abstract memory relation implies the creation of new symbolic values. Thus, the join operator needs to maintain a relation between the symbolic values of its two arguments and the resulting symbolic values. Slightly differently than the inclusion checking, the join requires a pair of renaming functions Φ = (Ψ 0 ,Ψ 1 ) that map each output symbolic value to the pair of the two corresponding input symbolic values. For instance, if α is a resulting symbolic value of the join operator, we note Φ(α) = (α 0 , α 1 ) if Ψ 0 (α) = α 0 and Ψ 1 (α) = α 1 . The join algorithm proceeds in the same way as the inclusion checking, following the three same main steps: initialization that creates the initial pair of renaming functions, join of abstract heap relations that joins two abstract heap relations and join in the numerical abstract domain that joins the two abstract numerical values.

Initialization. The join operation starts with the initialization of the pair of renaming functions and the generation of the resulting abstract environment e as follows: ∀x ∈ X, Φ init (α) = (e 0 (x), e 1 (x)) and e (x) = α.

Join of abstract heap relations. The join operation then proceeds to the computation of the new abstract heap relation r . This is done by the functions, join R , join H and join T that operate respectively on abstract heap relations, abstract heaps and abstract heap predicate transformations. The functions join R , join H also input and extend the pair of renaming functions.

The algorithm to compute these functions follows the same principle than inclusion checking. It implements rewriting rules, given in Figure 12. This rules system is based on three operators: H reasoning on abstract heaps , R reasoning on abstract heap relations and T reasoning on abstract heap transformation predicates. They satisfy the following properties:

h 0 H h 1 h =⇒ γ H (h 0 ) ∪ γ H (h 1 ) ⊆ γ H (h ) r 0 R r 1 r =⇒ γ R (r 0 ) ∪ γ R (r 1 ) ⊆ γ R (r ) t 0 T t 1 t =⇒ γ T (t 0 ) ∪ γ T (t 1 ) ⊆ γ T (t )
Note that the rules for H are given in [10, Figure 7]. Here, we discuss the rules of Figure 12. The rules ( Id ) and (

) are applied on two abstract heap relations that consist of the same relational connective (respectively Id(.) and [. .] . ). They simply apply H on the abstract heaps they contain and conserve the relational connective. The rule ( * R ) is based on the separation principle and allows to apply the other rules independently. The next rules can all be applied symmetrically and follow the principles of Theorem 1 (page 14) and Theorem 2 (page 17). When applied to an identity relation and a transform-into relation, the rule ( Id-weak ) first weakens the identity relation into a transform-into relation and applies recursively R . When the left operand of R contains two identity relations, the rule ( Id-merge ) merges them (in this rule, r 0 is needed to handle the cases where more than two identity relations need to be merged). When the left operand contains two transform-into relations, the rule ( -weak ) weakens them into one transform-into relation. Finally, when the left operand contains an identity relation and a transform-into relation, the rule ( -intro ) weakens the identity relation into a transform-into relation and applies recursively R .

Join in the numerical abstract domain. Finally, the join operation proceeds to the join in the numerical abstract domain. Like for the inclusion checking, the numerical abstract values have to take into account the renaming performed by the abstract heap relations. Thus, the join in the numerical abstract domain is performed by the function join

N : [V → V ] 2 × N × N → N .

Definition 31 (Join in abstract memory relations)

Let m R,0 = (e 0 , r 0 , n 0 ) and m R,1 = (e 1 , r 1 , n 1 ) be two abstract memory relations.

∀x ∈ X, Let Φ init (α) = (e 0 (x), e 1 (x)) and e (x) = α.

If join R (Φ init , r 0 , r 1 ) = (Φ , r ) and join N (Φ , n 0 , n 1 ) = n then:

join M R (m R,0 , m R,1 ) = (e , r , n )
Similarly as inclusion checking, join M R firsts initializes the pair of renaming functions Φ init and creates the joined environment e . It then proceeds to the join of the abstract heap relations and to the join with Φ init . Finally, it joins the abstract numerical values with the final pair of renaming functions returned by join R .

Condition 12 (Soundness of join N ) Let Ψ 0 ,Ψ 1 : V → V and n 0 , n 1 ∈ N , then:

(Ψ 0 • ν) ∈ γ N (n 0 ) ∨ (Ψ 1 • ν) ∈ γ N (n 1 ) =⇒ ν ∈ γ N (join N ((Ψ 0 ,Ψ 1 ), n 0 , n 1 ))
Condition 13 (Soundness of join H ) Let Ψ 0 ,Ψ 1 : V → V and h 0 , h 1 ∈ H .

If join H ((Ψ 0 ,Ψ 1 ), h 0 , h 1 ) = ((Ψ 0 ,Ψ 1 ), h ), then:

∀α, β ∈ V ,Ψ 0 (α) = β =⇒ Ψ 0 (α) = β ∀α, β ∈ V ,Ψ 1 (α) = β =⇒ Ψ 1 (α) = β (h,Ψ 0 • ν) ∈ γ H (h 0 ) ∨ (h,Ψ 1 • ν) ∈ γ H (h 1 ) =⇒ (h, ν) ∈ γ H (h ) Theorem 21 (Soundness of join R ) Let r 0 , r 1 ∈ R and Ψ 0 ,Ψ 1 : V → V .
If join R ((Ψ 0 ,Ψ 1 ), r 0 , r 1 ) = ((Ψ 0 ,Ψ 1 ), r ) then:

∀α, β ∈ V ,Ψ 0 (α) = β =⇒ Ψ 0 (α) = β ∀α, β ∈ V ,Ψ 1 (α) = β =⇒ Ψ 1 (α) = β (h i , h o ,Ψ 0 • ν) ∈ γ R (r 0 ) ∨ (h i , h o ,Ψ 1 • ν) ∈ γ R (r 1 ) =⇒ (h i , h o , ν) ∈ γ R (r ) Theorem 22 (Soundness of join M R ) Let m R,0 , m R,1 ∈ M R . If join M R (m R,0 , m R,1 ) = m R then: γ M R (m R,0 ) ∪ γ M R (m R,1 ) ⊆ γ M R (m R )
Condition 14 (Soundness of join T ) Let Ψ 0 ,Ψ 1 : V → V and t 0 , t 1 ∈ T .

If join T ((Ψ 0 ,Ψ 1 ), t 0 , t 1 ) = t , then:

(h i , h o ,Ψ 0 • ν) ∈ γ T (t 0 ) ∨ (h i , h o ,Ψ 1 • ν) ∈ γ T (t 1 ) =⇒ (h i , h o , ν) ∈ γ T (t )
Definition 32 (Join in abstract heap transformation predicates domains) We define the join function join T : [V → V ] 2 × T × T → T for each abstract heap transformation predicates domain defined in Section 4.3.

1. The footprint predicates domain, T = {= , ⊆ , ⊇ , }: the definition of the operation join T (Φ, t 0 , t 1 ) = t is given by the following tabular (each line for t 0 and each column for t 1 ).

t = ⊆ ⊇ = = ⊆ ⊇ ⊆ ⊆ ⊆ ⊇ ⊇ ⊇
2. The fields predicates domain, T = P(F):

join T (Φ, t 0 , t 1 ) = t 0 ∪ t 1 3. The combined predicates domain, T = T a × T b :

join T (Φ, (t a,0 , t b,0 ), (t a,1 , t b,1 )) = (join T a (Φ, t a,0 , t a,1 ), join T b (Φ, t b,0 , t b,1 ))

Theorem 23 (Soundness of Definition 32) The operators from Definition 32 are sound in the sense of Condition 14.

Widening operator.

During the analysis of loops and recursive programs, the number of iterations of the static analysis has to be finite. To always terminate in a finite number of steps, the analysis requires a widening operator wid M R that joins abstract memory relations and provides a convergence acceleration for the iteration process.

The widening operator wid R for abstract heap relations can be implemented using the same rules system of Figure 12. Indeed, each rule strictly decreases the number of abstract heap relations, which ensures termination in a finite number of steps. Moreover, H is already a widening operator, as it converges in a finite number of steps, as explained in [START_REF] Bor-Yuh | Relational inductive shape analysis[END_REF].

However, join N cannot be used as a widening operator. Indeed, some numerical abstract domains such as intervals [START_REF] Cousot | Static determination of dynamic properties of programs[END_REF] or convex polyhedra [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF] require a specific widening operation. Thus, the abstract numerical domain should implement its own widening operator wid N .

Condition 15 (Soundness of wid N ) Let Ψ 0 ,Ψ 1 : V → V and n 0 , n 1 ∈ N , then:

(Ψ 0 • ν) ∈ γ N (n 0 ) ∨ (Ψ 1 • ν) ∈ γ N (n 1 ) =⇒ ν ∈ γ N (wid N ((Ψ 0 ,Ψ 1 ), n 0 , n 1 ))
The function wid N also enforces termination.

The operator T cannot be used as a widening operator: it may not converge in a finite number of steps. Indeed, the used abstract heap transformation predicates domain T may denote an infinite set. The solution is to define a converging widening operator T for abstract heap transformation predicates. This operator is then implemented by a function wid T : [V → V ] 2 × T × T → T that is assumed to ensure termination. Its soundness property is the same as the function join T , except that it also enforces termination.

Condition 16 (Soundness of wid T ) Let Ψ 0 ,Ψ 1 : V → V and t 0 , t 1 ∈ T .

If wid T ((Ψ 0 ,Ψ 1 ), t 0 , t 1 ) = t , then:

(h i , h o ,Ψ 0 • ν) ∈ γ T (t 0 ) ∨ (h i , h o ,Ψ 1 • ν) ∈ γ T (t 1 ) =⇒ (h i , h o , ν) ∈ γ T (t )
The function wid T also enforces termination. wid T (Φ, t 0 , t 1 ) = join T (Φ, t 0 , t 1 )

The fields predicates domain, T = P(F):

wid T (Φ, t 0 , t 1 ) = join T (Φ, t 0 , t 1 )

3. The combined predicates domain, T = T a × T b : wid T (Φ, (t a,0 , t b,0 ), (t a,1 , t b,1 )) = (wid T a (Φ, t a,0 , t a,1 ), wid T b (Φ, t b,0 , t b,1 ))

Theorem 24 (Soundness of Definition 33) The operators from Definition 33 are sound in the sense of Condition 16.

Regarding to the footprint and the fields predicates domains, the function wid T is defined similary as the function join T . These definitions are valid because the footprint and the fields predicate domains are both finite. On the other hand, the combined predicates domain applies recursively the widening of its two sub-predicates domains.

Finally, the widening of abstract memory relation wid M R can be defined like join M R by substituting in its definition join N by wid R and by substituting join R by wid N .

Definition 34 (Widening for abstract memory relations) Let m R,0 = (e 0 , r 0 , n 0 ) and m R,1 = (e 1 , r 1 , n 1 ) be two abstract memory relations.

∀x ∈ X, Let Φ init (α) = (e 0 (x), e 1 (x)) and e (x) = α.

If wid R (Φ init , r 0 , r 1 ) = (Φ , r ) and wid N (Φ , n 0 , n 1 ) = n then:

wid M R (m R,0 , m R,1 ) = (e , r , n ) Theorem 25 (Soundness of wid M R ) Let m R,0 , m R,1 ∈ M R . If wid M R (m R,0 , m R,1 ) = m R then: γ M R (m R,0 ) ∪ γ M R (m R,1 ) ⊆ γ M R (m R )
The function wid M R also enforces termination Example 19 (Widening) We consider the analysis of the program of Figure 1, and more specifically, the widening after the first abstract iteration over the loop. We assume that wid M R ((e 0 , r 0 , n 0 ), ((e 1 , r 1 , n 1 ))) = (e , r , n ) where e 0 , r 0 , e 1 and r 1 are detailed below:

e 0 = [l → α 0 ; v → β 0 ; c → δ 0 ] r 0 = Id(α 0 → α 0 * S list(α 0 ) * S β 0 → β 0 ) * R [emp (δ 0 → α 0 )] t 0 with t 0 = (⊆ , {}) e 1 = [l → α 1 ; v → β 1 ; c → δ 1 ] r 1 = Id(α 1 → α 1 * S α 1 • data → δ 1 * S α 1 • next → α 1 * S list(α 1 ) * S β 1 → β 1 ) * R [emp (δ 1 → α 1 )] t 1 with t 1 = (⊆ , {0}) (0 represents the null offset)
First, the initialization produces the initial pair of renaming functions Φ init such as Φ init (α) = (α 0 , α 1 ), Φ init (β ) = (β 0 , β 1 ) and Φ init (δ ) = (δ 0 , δ 1 ). Thus, the resulting abstract environment

is e = [l → α; v → β ; c → δ ].
Then, wid R (Φ init , r 0 , r 1 ) is applied and produces: This abstract widening performs some generalization and introduces a list segment inductive predicate, that over-approximates an empty segment in the left argument, and a segment of length one. It also extends Φ init into Φ with Φ(α ) = (α 0 , α 1 ), Φ(β ) = (β 0 , β 1 ) and Φ(α ) = (α 0 , α 1 ).

r = Id(α → α * S listseg(α , α ) * S list(α ) * S β → β ) * R [emp (δ → α )] t with t = (⊆ , {0})
In turn, wid N can be applied with Φ, n 0 and n 1 .

Analysis

Manipulating Disjunctions in the Analysis

Because of unfolding operations, the analysis should deal with disjunctions. This is exactly the role of the disjunction abstract domain, defined in Section 4.4.2. It is build on top of abstract memory relations domain and permit to perform standard abstract operations (assignment, allocation, ...) over finite sets of abstract memory relations. Its interface is given in Figure 13. Each function of this interface applies the function of the same name, but at the abstract memory relation level. In doing so, it carries disjunctions and may create additional disjuncts when unfolding is performed. Although we do not formalize this operator here, an implementation of this abstract domain may rely on a function collapse D : D → D that transforms a disjunctive abstraction into another disjunctive abstraction with fewer disjuncts, which helps keeping the analysis cost down. The soundness of the functions of this interface and more details are discussed in [START_REF] Bor-Yuh | Modular construction of shape-numeric analyzers[END_REF].

Abstract Relational Semantics

The abstract semantics . R relies on the abstract operations defined in Sections 5.3, 5.4 and 5.5, on the unfolding of Section 5.2 to analyze basic statements, and on the folding operations defined in Sections 5.6 and 5.7 to cope with control flow joins and loop invariants computation. It is defined by induction over the syntax of the programming language defined in Section 3.3 and operates over abstract disjunctions, as shown in Figure 14. Soundness of . R follows from the soundness of the basic operations.

Theorem 26 (Soundness) The analysis is sound in the sense that, for all program p and for all abstract disjunction d : Fig. 14: Abstract semantics for the programing language defined in Section 3.3. The expression ¬exp is the negation of exp.

∀(m 0 , m 1 ) ∈ γ D (d ), ∀m 2 ∈ M, (m 1 , m 2 ) ∈ p R =⇒ (m 0 , m 2 ) ∈ γ D ( p R (d )) loc = exp R (d ) = assign D (loc, exp, d ) loc = malloc({f 1 , . . . , f n }) R (d ) = alloc D (loc, {f 1 , . . . , f n }, d ) free(loc) R (d ) = free D (loc, d ) p 1 ; p 2 R (d ) = p 2 R ( p 1 R (d )) if (exp) p 1 else p 2 R (d ) = join D ( p 1 R (guard D (exp, d )), p 2

Experimental Evaluation

In this section, we report on the implementation and on the evaluation of our relational shape abstraction. The purpose of this evaluation is to assess whether it is able to represent and compute strong relational properties, how it compares with standard state shape analyses, and whether it is adapted to verify programs. More precisely, we intend to evaluate how the relational predicates (both the relational connectors and the transformation predicates) behave in practice. To reach these goals, our evaluation is split into two parts: 1. in the first part, we consider basic data-structure libraries and check that the relational analysis infers interesting input-output relations and we compare it with more conventional state analyses (such test cases are often used to assess state analyses thus results of such analyses are known quantity in this part of the evaluation); 2. in the second part, we apply the relational analysis to the verification of the list module of the Contiki operating system and compare our results with those obtained with an approach based on deductive verification [START_REF] Blanchard | Ghosts for lists: A critical module of contiki verified in frama-c[END_REF]. Note that our evaluation focuses on the relational shape abstract domain, thus we do not include test cases relying on sophisticated data invariants or that would involve many static analysis design choices unrelated to the abstraction of shapes and relations. As an example, the analysis of a large interprocedural code using relations as procedure summaries would necessarily evaluate the way procedures are handled (bottom-up or top-down, etc) as much as, if not more than, the shape abstraction itself, thus it would not provide an ideal target for our study.

On Basics Library of Lists and Trees

In a first time, we report on the implementation of our analysis and try to evaluate: 1. whether it can infer precise and useful relational properties, 2. how abstract heap transformation predicates domains can improve its precision, and 3. how it compares with a state shape analysis that does not use relations. Our implementation supports built-in inductive predicates to describe singly linked lists and binary trees. It provides both the analysis described in this paper, and a basic state shape analysis in the style of [START_REF] Bor-Yuh | Relational inductive shape analysis[END_REF], and supporting the same inductive predicates. It was implemented as a Frama-C [START_REF] Kirchner | Frama-c: A software analysis perspective[END_REF] plug-in consisting of roughly 15000 lines of OCaml.

We have ran both the state shape analysis and the relational shape analysis (in a first time without abstract heap transformation predicates, and a second with) on series of small programs manipulating lists and trees listed in Table 3. This allows us to not only assess the results of the analysis computing abstract state relations, but also to compare them with an analysis that infers abstract states. Each program requires a short (1-line) precondition stating that the argument of the function are well-formed linked-list and trees.

The results obtained are listed in Table 3. The column 'State' corresponds to the execution time of the state analysis. The column 'Rel.', the basic relational analysis, corresponds to the relational analysis without abstract heap transformation predicates. The column 'Rel.+', the extended relational analysis, corresponds to the abstract heap relation analysis with the abstract heap transformation predicates. As a transformation predicate, we use the combined predicates domain of the fields and the footprint predicates domains, defined in Section 4.3. The analysis runtimes are averaged over 1000 runs of the analysis. The last two columns compare the logical strength of the results of the analyses. This is indicated in the cells by comparison symbols (<, > or =). For instance, if we find '<' in a cell of the State vs Rel. column, that means that the basic relational analysis inferred a stronger property than the state analysis for the given function.

Logical Strength Comparison

We first discuss on the logical strength. We observe that both the basic and the extended relational analyses never infer weaker properties than the state analysis (for instance, there is no '>' in the State vs Rel. column). In most cases, the basic relational analysis is sufficient to infer stronger properties than the state analysis. In these cases, the extended relational analysis often does not infer more information. The main reason is that the inferred relation already describes a very precise relation. Otherwise, when the basic relational analysis did not infer a stronger property than the state analysis, the extended relational analysis infers in all the cases a stronger relational property.

The most important observation is that for all the cases, we have that the basic relational analysis or the extended relational analysis inferred a strictly stronger property than the state analysis. We discuss some of cases in the next paragraphs.

When the result of the basic relational analysis is stronger than the state analysis. In this case, we consider the functions head_insertion and deep_copy:

-head_insertion: the basic relational analysis inferred the following abstract heap relation:

[α 0 → α 1 α 0 → β ] * R [emp β • next → α 1 ] * R [emp β • data → δ ] * R Id(list(α 1 ))
It describes exactly the effects of the insertion of a new allocated element at the head of a given list. Indeed, it expresses explicitly that the input list (abstracted by the inductive predicate list(α 1 )) has not been modified by the function. Moreover, it expresses the allocation of a new list element β that next field points to the input list. This abstract relation is clearly more expressive than the result of the state analysis, that cannot capture the relational properties described above. However, adding abstract heap transformation predicates to the relational analysis did not add more interesting relational properties: in this case, the basic relational analysis is already precise enough.

-deep_copy: this function traverses a list and copies its data fields in a new list. The inferred basic abstract heap relation by the basic relational analysis is:

Id(list(α)) * R [emp list(β )]
It indicates that the input list list(α) has not been modified and that a new list list(β ) has been freshly allocated. These properties cannot be inferred by the state analysis. Neverless, the abstract heap transformation predicate (⊆ , {data, next}) inferred by the extended relational analysis does not provide more information. Indeed, the predicate ⊆ is useless because we already knew that list(β ) has been allocated (its abstract input heap is emp) and the predicate {data, next} indicates that both the data and the next fields may have been modified.

When the result of the extended relational analysis is stronger than the basic relational analysis.

The second case is when the result of the basic relational analysis is not stronger than the result of the state analysis but when the result of the extended relational analysis is stronger than the result of the basic relational analysis. We discuss the map, reverse, filter and partition functions that are in that situation:

map: this function traverses a list and increments each data field. The inferred abstract heap relation for this function is [list(α) list(α)]. It just indicates that the input and output lists start at the same address. We have no more information compared to the state analysis. However, using abstract heap transformation predicates, we obtained the predicate (= , {data}) for the previous transform-into relation. It indicates that the footprint of the two lists is the same and that only the data fields may have been modified. This describes much more accurately the behavior of this function.

reverse: this function reverses (in place) the order of the elements of a list. The inferred abstract heap relation of this function is [list(α) list(β )]. It does not express any interesting relation compared to the state analysis (only the transformation of a list into another). However, the inferred abstract heap transformation predicate (= , {next}) expresses a permutation in place of the list, without modifying the data fields. This is the same abstraction obtained for the sort function of Figure 3. We remark that this is not the most precise property that we may think of (it does not imply that the elements of the list were properly reversed; it just says they were re-ordered). This is due to the fact that the transformation predicates that we have used cannot capture this most precise property, and can at most state that the footprint and values were preserved. Of course, one may design a specific transformation predicate to account for the reversal operation.

filter: this function deallocates all the negative elements of the input list. The inferred abstract heap relation is the same as the function reverse but the inferred abstract heap transformation predicates is (⊇ , {next}). This means that some deallocations may occur and no data field has been modified. partition: this function partitions (in place) the input list into two lists. The first one contains all the positive elements of the input list and the second all the negative elements. The inferred abstract heap relation of this function [list(α) list(β 1 ) * S list(β 2 )] only indicates the presence of two well formed linked lists in the output state, but nothing more than the state analysis does. However, the inferred abstract heap transformation predicate (= , {next}) indicates that these two output lists are composed by the elements of the input list, and that the data fields of the latter have not been modified.

Runtime Comparison

We now compare the runtime of the relational analysis and of the state analysis. We observe in most cases that the relational analysis is slower than the state analysis, although the slow down factor is reasonable. Indeed, the time of relational analysis rarely exceeds the double of the state analysis (this is the case for the functions partition, filter and tree insert). An exception is the list sort, which is approximately 5 times slower. This is explained by the fact that this function contains a condition test in a nested loop and another condition test in the main loop. This implies to perform an important number of abstract joins and widenings. Conversely, the function head_insertion, that does not perform either abstract join or widening, avoids any slowdown. Moreover, we believe that we can optimize the implementation of these operators in our prototype analyzer, using a better strategy to detect the rules to apply. To do that, we could draw inspiration from the work in [START_REF] Li | Semantic-directed clumping of disjunctive abstract states[END_REF] that proposes an elegant solution to solve this problem. While these test cases are not large, these results show that the relational analyses have a reasonable overhead and that they bring additional information compared to a classical state analysis. The difference time between the analyses is due to the fact that the relational analysis manipulates pairs of states whereas the state analysis manipulates only one state. In general, the relational analysis infers stronger properties.

In order to be able to analyze large programs, we consider for future works to perform a compositional analysis where abstract relations are used as function summaries and composed at call sites. This avoids to reanalyze a function every time it is called, which is an advantage for scalability.

On The List Module of The Operating System Contiki

In this section, we run experiments to evaluate the ability of our relational analysis to infer and verify desired function contracts about procedures manipulating linked data structures. We also check that our analysis is sound, i.e. raises an alarm when a program contains a bug. Finally, we evaluate the effort one can gain by using a fully-automated analysis like ours.

For this, we compare our approach with the one of Blanchard et al. [START_REF] Blanchard | Ghosts for lists: A critical module of contiki verified in frama-c[END_REF] for the verification of the linked list module of the operating system Contiki [START_REF] Dunkels | Contiki-a lightweight and flexible operating system for tiny networked sensors[END_REF]. Their work performs a deductive verification of this list module and is based on a parallel view of a linked list via a companion ghost array. In particular, the modifications of the lists performed by the function are described as relations between ghost arrays in the input and output states.

This approach requires the user to specify both the pre and post conditions of each function, to annotate the source code with many invariants (mostly loop invariants), to write ghost functions and to prove different lemmas using SMT solvers or the Coq proof assistant. In total, for about 176 lines of C code in the list module, they wrote 46 lines of for ghost functions and about 1400 lines of annotations. Their verification has generated 798 goals to prove. Among these goals, 770 have been proven automatically by SMT solvers, 4 interactively and 24 proven using the Coq proof assistant. By comparison we only need to write one or two lines of annotations for preconditions, which only state that the input of the function is a well-formed linked list, and, when there is another argument, whether this argument is separated or belongs to that list.

Since the contracts of these functions were written manually in [START_REF] Blanchard | Ghosts for lists: A critical module of contiki verified in frama-c[END_REF], they provide an accurate description of the properties that one wants to prove about these functions. For instance, the contract for list_length states that the function inputs a list and returns its length but does not modify the list, which is the expected contract for a function with this name.

We aimed to check if our relational abstract domain was able to express and verify the same properties than those stated in these contracts, but more automatically. More precisely, we assessed whether our approach could verify the exact shape properties (e.g., a list head insertion function preserves the existing elements of the list and adds an element at the head), under the data of the abstract pre-condition. Due to the radical approach difference, we need to use a different formalism than theirs (while they use ghost arrays, we rely on relational separation logic). Therefore, the properties that we check are equivalent to theirs, in the sense that the input/output states described by their contracts correspond to those infered by our analysis. Note that as we do not need to reason over ghost arrays, the contracts cannot be strictly the same.

We have analyzed all the functions given in their paper, using the source code that they provide. These functions are listed in Table 4. It shows that for all of the functions (except for list_length), the contracts inferred by our analysis are equivalent to those given by Blanchard et al. For list_length we do infer the relational shape property that the list is not modified, but we cannot prove that the returned integer corresponds to the length of the list. We did not analyze the files that only manipulate arrays such as array_pop.c, as our relational abstract domain does not require ghost array companions.

An important feature in this list module is that each element of a list has to be unique. So if a function adds an element into a list, and if this element is already in this list, the element first has to be removed from the list and then added at the desired position. This is why all the functions that add an element into a list (list_push, list_add) call the function list_remove. This latter removes the given list element from the input list if it is inside, or leaves the list unchanged otherwise. For these functions we run our analysis twice with these 2 different preconditions: when the input list contains the given element and when it does not contain it. We could have to run the analysis once with only one pre-condition consisting of a disjunction of these to previous pre-conditions, but these disjuncts may have been joined during a widening. This would have begotten a too high loss of precision.

The function list_insert inserts a given list element into a list at a given position. We analyzed this function with three different pre-conditions: when the element to insert is not in the list, when the element is in the list but before the position it is supposed to be inserted, and when the element is in the list but after the desired position for insertion. This function actually contains a bug. Indeed, if the element is already in the list (no matter before or after the position of insertion), the function adds directly the element at the given position without removing it from the list. This breaks the structure of the list. Like Blanchard et al., we found this bug with our analysis.

7 Related Works

Extension of Separation Logic

Separation logic is used in program verification systems that can be separated in three kinds:

-Verification tools based on interactive proof assistants (e.g. [START_REF] Bengtson | Charge! a framework for higher-order separation logic in coq[END_REF]) requires the tool to apply or check the use of the separation logic inference rules [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF]. -Semi-automated tools based on deductive verification (e.g. [START_REF] Huu | Automated verification of shape and size properties via separation logic[END_REF][START_REF] Jacobs | The verifast program verifier[END_REF]) avoids the need to write many intermediate proof steps, by additionally providing automated entailment checking procedure. -Fully-automated tools based on abstract interpretation (e.g. [START_REF] Calcagno | Compositional shape analysis by means of bi-abduction[END_REF][START_REF] Bor-Yuh | Relational inductive shape analysis[END_REF]) can automatically infer shape properties as separation logic formulas; for this the separation logic formulas must be manipulable as elements of an abstract domain (e.g. a join and widening operators must be defined). A sound (but not complete) automated entailment checking is also provided as an inclusion operator of the abstract domain.

Our work takes place in the context of the latter, and extends it to infer not only shape invariants on the memory, but relational invariants (e.g. function contracts) between different program locations, using an extension of separation logic.

In the past, several works have enriched separation logic in order to perform specific analyses. To our knowledge, our work is the first to propose logical connectives based on separation logic that support inductive predicates and describe input-output heap relations.

Extensions expressing immutability Classical separation logic cannot directly express immutability, and the classical way to express such a property in a Hoare triple is to state that the values stored in memory in the pre-and post-condition are the same. Several authors have proposed extensions to separation logic to work around this limitation.

In the context of interactive proof, Charguéraud et al. [START_REF] Charguéraud | Temporary read-only permissions for separation logic[END_REF] introduced the temporary read-only permission through a new connective for separation logic. This connective offers read-only access to any heap fragment described with a separation logic formula. David et al. [START_REF] David | Immutable specifications for more concise and precise verification[END_REF] introduced a similar concept in the context of deductive verification.

Like our relational connectives, this read-only connective can express that some part of the heap is left unchanged, as it can only be read. Note however that immutability is only one example among many of the relations that we can express: for instance the footprint predicate domain of Section 4.3.1 allows expressing relational properties that are not immutability properties, such as whether a sorting algorithm is in-place.

Costea et al. [START_REF] Costea | Hipimm: Verifying granular immutability guarantees[END_REF] introduced read-only permission at the field level, which is similar in expressivity to our Fields predicate domain of Section 4.3.2.

Another important difference with these works is that our analysis is able to infer postconditions for programs in the presence of loops; whereas the first work focuses on manual proofs, and the second and third on the verification (based on automatic entailment checking procedures) of user-supplied invariants.

Other extensions of separation logic An important extension of separation logic is the concurrent separation logic [START_REF] Peter | Resources, concurrency, and local reasoning[END_REF], which allows independent reasoning about threads that access separate storage. The new connective allows to evaluate two terms of separation logic in parallel.

Like the read-only permission extensions, an important difference of these separation logic extensions compared to ours is that they modify directly the original separation logic; whereas in our extension, the relational connectives encompasses the terms of separation logic, without modifying them.

Fu et al. [START_REF] Fu | Reasoning about optimistic concurrency using a program logic for history[END_REF] introduced extension of separation logic to specify historical execution traces of heaps in the context of concurrent programs. They also have a new separating conjunction connective but for disjoint traces, whereas our relational separating conjunction expresses independent transformations. Desynchronized separation [START_REF] Cox | Desynchronized multi-state abstractions for open programs in dynamic languages[END_REF] also introduces a notion of overlaid state in separation logic, but does not support inductive predicates as our analysis does. Instead, it allows to reason on abstractions of JavaScript open objects seen as dictionaries.

Relational Analysis

Our analysis computes an abstraction of the relational semantics of programs so as to capture the effect of a function or other blocks of code using an element of some specifically designed abstract domain.

This technique has been applied to other abstractions in the past, and often applied to design modular static analyses [START_REF] Cousot | Modular static program analysis[END_REF], where program components can be analyzed once and separately. For numerical domains, it simply requires duplicating each variable into two instances respectively describing the old and the new value, and using a relational domain to the inputs and outputs. For instance, [START_REF] Popeea | Inferring disjunctive postconditions[END_REF] implements this idea using convex polyhedra and so as to infer abstract state relations for numerical programs. It has also been applied to shape analyses based on Three Valued Logic [START_REF] Sagiv | Parametric shape analysis via 3-valued logic[END_REF] in [START_REF] Jeannet | A relational approach to interprocedural shape analysis[END_REF]. This work is probably the closest to ours, but it relies on a very different abstraction using a TVLA whereas we use a set of abstract predicates based on separation logic. It uses the same variable duplication technique as mentioned above. Our analysis also has a notion of overlaid old / new predicates, but these are described heap regions, inside separation logic formulas.

Several other techniques have been used to specify memory properties. For instance, [START_REF] Yahav | Verifying temporal heap properties specified via evolution logic[END_REF] uses temporal logic to specify temporal properties of heap evolutions and [START_REF] Taghdiri | Inferring specifications to detect errors in code[END_REF] checks structural properties of codes using a specification language.

In the context of concurrent programs, [START_REF] Amit | Comparison under abstraction for verifying linearizability[END_REF] verifies linearizability of concurrent objects (unbounded linked list) maintaining isomorphism between two instances of memory layout. Also, [START_REF] Distefano | Who is pointing when to whom?[END_REF] uses an extension of temporal linear temporal logic and a tableau-based modelchecking algorithm to specify the dynamic evolution of pointer structures. This latter technique has been applied in [START_REF] Distefano | Safety and liveness in concurrent pointer programs[END_REF] to prove the correctness of concurrent programs manipulating linked lists.

In the context of functional languages, [START_REF] Kaki | A relational framework for higher-order shape analysis[END_REF] allows to write down relations between function inputs and outputs, and relies on a solver to verify that constraints hold and [START_REF] Zhu | Automatically learning shape specifications[END_REF] computes shape specification by learning.

Regarding to shape analyses based on separation logic, [START_REF] Bouajjani | Invariant synthesis for programs manipulating lists with unbounded data[END_REF] infers combined list-data relations and has been extended in [START_REF] Bouajjani | On inter-procedural analysis of programs with lists and data[END_REF] for inter-procedural analysis. They can infer precise relations between the data contained in a list, such as the sum of all data in a list is inferior to the length of this list. They also use a multi-set to represent the data of a list. For example, to prove a function sort, they compare the multi-set of the input list with the multi-set of the output list. If these multi-sets are the same (this means a permutation), and if the output list is sorted, then the sort function is proven. However, they do not have this notion of physical equality between the different memory cells that our relational domain can express. Consequently, they cannot capture whether a program treats some data in-place or not. Moreover, our relational properties do not focus on a specific data structure, but aims at being generic for any data structure.

Modular analyses that compute invariants by separate analysis of program components [START_REF] Chatterjee | Relevant context inference[END_REF][START_REF] Dillig | Precise and compact modular procedure summaries for heap manipulating programs[END_REF][START_REF] Castelnuovo | Modularity in lattices: A case study on the correspondence between top-down and bottom-up analysis[END_REF] use various sorts of abstractions for the behavior of program components. A common pattern uses tables of pairs made of an abstract pre-condition and a corresponding abstract post-condition, effectively defining a sort of cardinal power abstraction [START_REF] Cousot | Systematic design of program analysis frameworks[END_REF]. This technique has been used in several shape analyses based on separation logic [START_REF] Calcagno | Compositional shape analysis by means of bi-abduction[END_REF][START_REF] Bhargav S Gulavani | Bottom-up shape analysis[END_REF][START_REF] Loc | Shape analysis via second-order bi-abduction[END_REF][START_REF] Calcagno | Footprint analysis : A shape analysis that discovers preconditions[END_REF]. We believe this tabular approach could benefit from abstractions of relations such as ours to infer stronger properties, and more concise summaries.

Conclusion

While relational properties are harder to abstract than state properties, they are intrinsically more expressive and they offer the ability to make the analysis modular and compositional. In the context of data structures, shape analyses based on separation logic rely on the separating conjunction ( * ) that ensures that two memory regions are disjoint, and on inductive predicates that describe precise structural invariant over complex dynamic data structures. However, separation logic formulas describe a set of states, they cannot describe relations. In this paper, we have introduced a set of logical connectives inspired by separation logic, to describe inputoutput relations rather than states. We have built upon this logic an abstract domain, and a static analysis based on abstract interpretation that computes conservative abstract relations. We also have extended the relational abstract domain to express more specific and stronger relational properties, in a modular way. Experiments prove its ability to infer expressive relational properties for basic libraries of data structures. Furthermore, it would be more adapted to a compositional inter-procedural analysis.

2 3Fig 9 Fig. 2 :

 292 Fig. 1: A list insertion program

1Fig. 3 :

 3 Fig. 3: A list sort program

Fig. 4 :

 4 Fig. 4: Example of concrete input and output states for the program of Figure 3

Fig. 8 :

 8 Fig. 8: Syntax of abstract heaps and abstract heap relations

Fig. 9 :

 9 Fig.9: Pure Formulas Syntax.The ⊕ operators correspond to those in Figure5.

Theorem 4 (

 4 Soundness of id T and * T) The functions id T and * T of the fields predicates domain satisfy respectively Condition 2 and Condition 3.

  a triplet made of an abstract environment e , that binds program variables into their symbolic values in the abstract heap relation r , and a numerical abstract value n that abstracts the value of symbolic values of r . Definition 14 (Concretization of abstract memory relations) The concretization of abstract memory relations γ M R : M R → P(M × M) maps an abstract memory relation m R = (e , r , n ) into the pairs of its concrete input and output memories.

17 (

 17 Soundness of Definition 27) The operators from Definition 27 are sound in the sense of Condition 9. Example 16 (Deallocation of a list element) We show the effect of the analysis of the deallocation of a list element, from the abstract memory relation (e , r , n ), with e (p) = α 0 , t 0 = (= , {data}) and r = Id(α

⊇ 2 .

 2 {true, false} for each abstract heap transformation predicates domain defined in Section 4.3. 1. The footprint predicates domain, T = {= , ⊆ , ⊇ , }: the function isle T is defined using the Hasse diagram of T : = ⊆ The fields predicates domain, T = P(F):

Fig. 12 :

 12 Fig. 12: Join rewriting rules

Definition 33 (

 33 Widening for abstract heap transformation predicates domains) We define the widening function wid T : [V → V ] 2 × T × T → T for each abstract heap transformation predicates domain defined respectively in Section 4.3.1, Section 4.3.2 and Section 4.3.3. 1. The footprint predicates domain, T = {= , ⊆ , ⊇ , }:

Fig. 13 :

 13 Fig. 13: Disjunction Abstract Domain Interface (D = P fin (M R )).

  R (guard D (¬exp, d ))) while(exp) p R (d 0 ) = Let d 1 = p R (guard D (exp, d 0 )) in If isle D (d 1 , d 0 ) = true Then guard D (¬exp, join D (d 0 , d 1 )) Else while(exp) p R (wid D (join D (d 0 , d 1 ), d 0 ))

  and perform the deallocation in the obtained transform into relation. It finally produces Id(h ) * R [α • f → βemp] t with t = free T (α, f, t 0 ). Soundness of free T ) Let T be an abstract heap transformation predicates domain and t ∈ T . Let α ∈ V and f ∈ F. The function free T is sound if:

	Condition 9 (

Table 3 :

 3 Experiment results (sll: singly linked lists; bst: binary search trees; time in seconds averaged over 1000 runs on a laptop with Intel Core i5 running at 2.4 GHz, with 4 Gb RAM, for the state, basic and extended relational analyses; the last column compares the logical strength of the inferred result of each analysis).

	Struct.	Function		Time (in s)		Logical Strength
			State	Rel.	Rel.+	State vs Rel.	Rel. vs Rel.+
	sll	allocation	0.56	0.77	0.78	<	=
	sll	deallocation	0.46	0.80	0.79	<	=
	sll	traversal	0.58	0.79	0.77	<	=
	sll	head_insertion	0.43	0.43	0.44	<	=
	sll	insert (Figure 1)	1.11	1.92	1.93	<	=
	sll	reverse	0.60	1.01	1.06	=	<
	sll	map	0.59	0.92	0.91	=	<
	sll	tail	0.42	0.55	0.54	<	=
	sll	nth	0.70	1.17	1.15	<	=
	sll	partition	2.18	4.85	4.93	=	<
	sll	appends	0.88	1.60	1.59	<	=
	sll	contains	0.82	1.22	1.24	<	=
	sll	deep_copy	1.15	2.08	2.16	<	=
	sll	sort (Figure 3)	4.09	21.95	22.16	=	<
	sll	filter	1.21	2.70	2.79	=	<
	bst	allocation	0.71	1.11	1.45	<	=
	bst	search	0.97	1.63	1.67	<	=
	bst	insert	2.25	6.10	6.22	<	=

Table 4 :

 4 Experimental results for the linked list module of the operating system Contiki. It indicates if our relational analysis infered a function contract equivalent to the one manually specified by Blanchard et al.'s. The third column indicates with how many different preconditions we run the analysis of the function. The last column indicates the execution times (in ms) for each pre-condition of the function

	Function	Equivalent contract	Num. of pre-conditions	Times (in ms)
	list_add	yes	2	211 + 207
	list_chop	yes	1	204
	list_copy	yes	1	207
	list_head	yes	1	201
	list_init	yes	1	203
	list_insert	yes	3	208 + 203 + 204
	list_item_next	yes	1	202
	list_length	relational shape only	1	203
	list_pop	yes	1	200
	list_push	yes	2	208 + 204
	list_remove	yes	2	201 + 202
	list_tail	yes	1	201

Acknowledgments. We acknowledge the anonymous reviewers for their constructive comments.