Pascal Sotin

Xavier Rival

Hierarchical Shape Abstraction of Dynamic Structures in Static Blocks ⋆

We propose a hierarchical shape abstract domain, so as to infer structural invariants of dynamic structures such as lists living inside static structures, such as arrays. This programming pattern is often used in safety critical embedded software as an alternative to dynamic memory allocation. Our abstract domain precisely describes such hierarchies of structures. It combines several instances of simple shape abstract domains, dedicated to the representation of elementary shape properties, and also embeds a numerical abstract domain. This modular construction greatly simplifies the design and the implementation of the abstract domain. We provide an implementation, and show the effectiveness of our approach on a problem taken from a real code.

Introduction

Safety critical embedded systems as found in avionics should meet safety requirements fixed by regulation standards [START_REF]Software considerations in airborne systems and equipment certification[END_REF]. In particular, software providers should supply evidence that the real time applications will not fail due to resource exhaustion. In practice, this constraint forbids the use of dynamic memory allocation in highly critical software. Though, this does not mean that dynamic data-structures (that is linked structures where pointers may be modified at any time in the execution of the program) cannot be used: indeed, structure elements may be allocated statically (in arrays or in other static sections) and links across elements may be re-computed at any time. Such statically allocated dynamic structures are found in many programs such as the USB driver considered in [START_REF] Monniaux | Verification of device drivers and intelligent controllers: a case study[END_REF] or the multi-threaded avionic software considered in [START_REF] Miné | Static analysis of run-time errors in embedded critical parallel c programs[END_REF].

In the last decade, dramatic progresses have been accomplished in the verification of absence of runtime errors in safety critical programs [START_REF] Blanchet | A static analyzer for large safety-critical software[END_REF][START_REF] Bertrane | Static analysis and verification of aerospace software by abstract interpretation[END_REF], yet statically allocated dynamic structures are still very challenging for static analysis tools. Static analyzers such as Astrée [START_REF] Blanchet | A static analyzer for large safety-critical software[END_REF][START_REF] Bertrane | Static analysis and verification of aerospace software by abstract interpretation[END_REF] do offer some support for the summarization of large memory regions, but will not capture inductive properties of linked data structures such as lists. Inferring that such a structure is a well formed list may require maintaining large disjunctions of cases depending on the elements order. Failure to do so would lead to false alarms, as proving the absence of runtime errors may require proving that the dynamic structures are well formed.

On the other hand, shape analysis techniques are very smart at summarizing unbounded linked structures [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] Berdine | Shape analysis for composite data structures[END_REF] but typically do not track the fact that some pieces of data are stored in a fixed, static block, which may be accessed to as an array. Furthermore, existing shape analyses cannot be interfaced with a powerful numerical domain such as the one used in [START_REF] Bertrane | Static analysis and verification of aerospace software by abstract interpretation[END_REF].

In this paper, we exploit the ability of the shape analysis framework proposed in [START_REF] Chang | Relational inductive shape analysis[END_REF][START_REF] Laviron | Separating shape graphs[END_REF] to attach numeric predicates to shape graph "nodes" that represent concrete values of arbitrary size (addresses or contents of physical memory cells) in order to tie a complex property to a memory region, in a fully modular way from the static analysis design point of view. In particular, the contents of a static region (as a sequence of bytes) is represented by a symbolic variable, which may be characterized in a value abstract domain; we can then choose to consider this sequence of bytes as a "store inside the store", and let another instance of our shape abstract domain take care of its abstraction. In this setup, the analysis uses two instances of the shape abstract domain: one is used to abstract the memory states, whereas the other is used in order to abstract the contents of the static region. The main advantage of this technique is the modularity of the abstraction, as it alleviates the need for a complex monolithic abstract domain expressing all data-structure invariants. It also allows to reuse the abstract domain of [START_REF] Chang | Relational inductive shape analysis[END_REF] as is, and can be combined with a powerful numerical abstract domain. Our main contributions are [START_REF] Berdine | Shape analysis for composite data structures[END_REF] the design of a framework for the abstraction of hierarchical memory states, where some memory regions are viewed as sub-memories, (2) the integration of an array abstraction in a shape abstract domain, to automatically infer sub-memory boundaries and (3) the implementation of the hierarchical abstraction in the MemCAD static analyzer, which implements the framework of [START_REF] Chang | Relational inductive shape analysis[END_REF] using the Apron [START_REF] Jeannet | Apron: A library of numerical abstract domains for static analysis[END_REF] numerical domain library, and the verification of a simplified excerpt from the avionic code discussed in [START_REF] Miné | Static analysis of run-time errors in embedded critical parallel c programs[END_REF] (leaving out features out of the scope of the issue considered in this paper).

Running example

Fig. 1 describes the function considered in our running example, a simplified excerpt of the safety critical application considered in [START_REF] Miné | Static analysis of run-time errors in embedded critical parallel c programs[END_REF]. The data-type (Fig. 1a) is a form of singly linked list (which represents message queues), yet all elements manipulated in the program live in a global array free pool [100] . A fragment of a concrete state is shown in Fig. 1b. At any point in the execution some of the array elements are active and are members of an existing list structure (the gray elements in the figure) whereas the others are "invalid". We call such an array a free-pool. Furthermore, other structural invariants are maintained throughout the program: the list is ordered by increasing priorities and its first and last cells are respectively pointed to by hd and tl . The code inserts a set of elements in the list stored in the free-pool. For each element, it searches the position and performs the insertion. Several cases were omitted for the sake of concision, and we only focus on the case of an insertion within the list, after a traversal to determine the right position. The goal of the analysis discussed in Fig. 1: A dynamic structure in a static area the paper is to establish both the preservation of the list structural invariant, and memory safety. In particular, the inner loop should cause no null pointer dereference (although the loop condition does not explicitly check that cur is not null). Moreover, it should verify the assertion at line 14, i.e., that the insertion is not made at the tail of the list in that branch.

Existing memory abstractions: Fig. 1b shows a (simplified) concrete state encountered at the head of the main loop in our example program. At the end of the execution, the list has length 100 and occupies the whole array. Due to the size of the structure, an efficient analysis requires it be summarized. The abstraction of [START_REF] Laviron | Separating shape graphs[END_REF] allows to summarize the whole list into a predicate which expresses that hd points to a list. However, that abstraction fails to capture the fact the list is allocated inside an array, and does not allow to analyze accesses using array selectors. In the other hand, preserving a fully precise abstraction of the array would not allow the summarization of the list and would require a large case analysis over the list elements ordering, which would be prohibitively expensive. The limitation of all the abstractions examined so far is that they fail to capture both the list structure and the fact that it lives inside a contiguous memory region. A solution is to perform a two steps abstraction:

1. The whole array occupies an 800 bytes long contiguous region, which can be abstracted by a single points-to predicate α → β where symbolic variables α and β respectively represent the address of the array and its whole contents viewed as a sequence of bytes, as shown in the left part of Fig. 2, whereas variable hd points into the array at some offset o (i.e. from base address α). 2. Symbolic variable β which denotes the array contents can be constrained by any abstraction over the sequence of bytes it represents. The trick is then to view it as a memory state in itself (which we later refer to as the submemory), and apply a classical shape abstraction to it, which expresses that it stores a well-formed singly linked list structure, the first element of which is at offset o, as shown in the right part of Fig. 2. This abstraction relies on the user-defined list inductive predicate below:

α • list := (emp ∧ α = 0) ∨ (α • next → β 0 * α • prio → β 1 * β 0 • list) .
In this view, the analysis should use two levels of memory abstractions: one to describe the main memory, and another one to describe the contents of a contiguous region of the memory, viewed as a sub-memory. In that sense, our abstraction is hierarchical. Furthermore, we are going to show that both abstractions may share a single implementation, where the memory abstraction consists of a general and parametric shape analysis abstract domain. This approach handles arbitrary nesting of dynamic and static structures (e.g., lists of arrays containing lists...). We formalize this abstraction in Sect. 3.3.

Static analysis in the hierarchical abstract domain. Our static analysis should establish properties of array initialization and list construction routines as well as common list operations (traversal, insertion...). Overall, the analysis algorithms in the hierarchical shape abstract domain are standard shape analysis algorithms including unfolding of inductive definitions and widening over shape graphs [START_REF] Chang | Relational inductive shape analysis[END_REF]. However, a number of specific issues need be solved, such as:

reasoning about array regions (and about the border between the free zone and the active list) effectively requires integrating array analysis techniques such as those proposed in [START_REF] Cousot | A parametric segmentation functor for fully automatic and scalable array content analysis[END_REF] into a shape abstract domain; -designing clear interfaces between domains, so as to make the analysis fully modular, letting the main memory abstraction devolve the analysis of operations to the sub-memory abstraction when possible. Those issues will be considered carefully in Sect. 4.

A Hierarchical Shape Abstract Domain

We formalize our abstract domain in this section, and recall elements of the abstract domain introduced in [START_REF] Chang | Shape analysis with structural invariant checkers[END_REF][START_REF] Chang | Relational inductive shape analysis[END_REF] it is based on.

A Shape Graph Abstract Domain

Concrete model. Intuitively, a concrete store can be viewed as a partial function σ from addresses (a ∈ A) into values (V, where A ⊆ V). In fact, the structure of memory states is more complex as values of various sizes may be read, so a store is actually characterized by its domain dom(σ) ∈ P(A), and the read operation, which maps pair of addresses a < a ′ ∈ A to the value read(σ, a, a ′ ) ∈ V that can be read in σ between a and a ′ , when [a, a ′ [ ⊑ dom(σ). A concrete value v ∈ V thus consists of a sequence of bytes.

Abstraction based on shape graphs. In the abstract level, symbolic variables (noted as Greek letters α, β, . . . ∈ V ♯ ) represent concrete values. These symbolic variables may appear in constraints on the stores structure, on their contents, and possibly simultaneously on both. A shape graph G ∈ D ♯ G describes the structure of concrete stores, as a separating conjunction of predicates, called edges, which express e.g., that some symbolic variable α is the address of a memory cell containing a value abstracted by another symbolic variable β: this constraint is described by a points-to edge of the form α → β (the more general format of points-to edges is shown below). Therefore, concretization γ G (G) of shape graph G ∈ D ♯ G is defined indirectely. Instead of returning a set of stores, it returns a set of pairs (σ, ν) where ν ∈ Val = V ♯ → V is a valuation, mapping each symbolic variable to the concrete value it abstracts, i.e., performing a physical mapping of the shape graph.

Shape graphs and concretization. The abstract domain is parameterized by the data of a finite set I of inductive definitions, such as the list definition shown in Sect. 2. The complete grammar of shape graphs is defined below: edges is defined by syntactic unfolding of their definitions, using rewrite relation unfold . For instance, the unfolding rules of inductive definition list are:

G ::= e 0 * e 1 * . . . * e k separating conjunction e ::= α [o0,o1[ → β + o 2 points-to edge (α, β ∈ V ♯ ) | α • ι inductive edge | α • ι * = β • ι segment edge Points-to edge α [o0,o1[ → β + o 2 ,
α • list unfold (emp ∧ α = 0) α • list unfold (α • next → β 0 * α • prio → β 1 * β 0 • list) . α • list * = δ • list unfold (emp ∧ α = δ) α • list * = δ • list unfold (α • next → β 0 * α • prio → β 1 * β 0 • list * = δ • list.) .
Concretization. We can now formalize the concretization γ G : D ♯ G → P(M × Val) of edges and of shape graphs. First, let us consider an edge e, and define its concretization γ G (e).

-

If e is α [o0,o1[ → β + o 2 , then (σ, ν) ∈ γ G (e)
if and only if:

dom(σ) = [ν L (α + o 0 ), ν L (α + o 1 )[ read(σ, ν L (α + o 0 ), ν L (α + o 1 )) = ν L (β + o 2 )
where ν L denotes the extension of ν to linear expressions over symbolic variables (for instance, ν L (8 + α + 2β) = 8 + ν(α) + 2ν(β)). This indeed captures the property that this points-to edge covers the range of addresses corresponding to symbolic range [α + o 0 , α + o 1 [ and contains symbolic value

β + o 2 .
-If e is either an inductive edge α • ι or a segment edge α • ι * = β • ι, then its concretization is defined by unfolding; thus (σ, ν) ∈ γ G (e) if and only if:

∃G, e unfold G ∧ (σ, ν) ∈ γ G (G).
Concretization γ G calculates the separating conjunction of the concretizations of the edges of shape graphs:

γ G (e 0 * e 1 * . . . * e k ) = {(σ 0 σ 1 . . . σ k , ν) | ∀i, (σ i , ν) ∈ γ G (e i )}.
where is the fusion of functions with disjoint domains (σ 0 σ 1 is defined if and only if dom(σ 0 ) ∩ dom(σ 1 ) = ∅ and then read(

σ 0 σ 1 , a, a ′ ) = read(σ i , a, a ′ ) if [a, a ′ [⊆ dom(σ i )).
In general, due to inductive and segment edges, the concretization of a shape graph has to be defined as a least-fixpoint.

Examples. In practice, a contiguous concrete memory region (or block) may be described by one or more points-to edges from one single node, that denote fragments of that memory region. We call such a set of points-to edges starting from a same source node α a segmentation of the block. As a very simple example, Fig. 3 shows two possible segmentations (with two edges in Fig. 3b or with one edge in Fig. 3c) to abstract a concrete array of two unsigned 2-bytes integers shown in Fig. 3a. As a convention, we insert segmentation offsets between pointsto edges (offsets 0, 2 and 4 in Fig. 3b) and destination offsets at the end of points-to edges (offsets +0 in Fig. 3b): Fig. 3b represents shape graph α [0,2[ →

β 0 + 0 * α [2,4[ → β 1 + 0.
Segmentations with linear expressions over symbolic variables as offsets rely on the same principle and will appear in Sect. 4.

Combination with a Value Domain

The advantage of the notion of shape graphs presented in Sect. 3.1 is that they allow a nice decomposition of the abstract domain: in particular, other forms of properties (such as arithmetic constraints) over symbolic variables can be described in a separate value abstract domain D ♯ V , with concretization γ V :

D ♯ V → P(Val). An abstract memory state is a pair (G, V ) ∈ D ♯ G × D ♯ V , and concretizes into {σ | ∃ν ∈ γ V (V ), (σ, ν) ∈ γ G (G)}.
In most cases, D ♯ V can be chosen among numerical abstractions. For instance, in the case of Fig. 3b, the octagon abstract domain [START_REF] Miné | The octagon abstract domain[END_REF] allows to express relation β 0 < β 1 which is satisfied in valuation ν used to concretize that shape graph into the concrete store of Fig. 3a. However, non purely numerical abstractions may be used as well. For instance, in the case of the shape graph of Fig. 3c, symbolic variable β denotes an array of unsigned 2-bytes integers, and array specific abstractions may be used to abstract β; for instance, that array is sorted, so we could choose D ♯ V in order to express array sortedness. Moreover, a concrete state M also encloses an environment E ∈ E = X → A mapping program variables into addresses, thus is a pair M = (E, σ). Likewise, an abstract state M ♯ ∈ S ♯ also includes an abstract environment E ♯ ∈ E ♯ = X → V ♯ , and the concretization simply asserts the compatibility of the concrete environment with the abstract environment up to the valuation. We write S for E × M and S ♯ for

E ♯ × D ♯ G × D ♯ V .
The concretization writes down as follows:

(E, σ) ∈ γ S (E ♯ , G, V ) ⇐⇒ ∃ν ∈ γ V (V ), E = ν • E ♯ ∧ (σ, ν) ∈ γ G (G).

Hierarchical Abstraction

At this stage, we are ready to formalize the final step of our hierarchical abstraction: indeed, we noticed in Sect. 3.2 that symbolic variables denote values (as sequences of bytes), that can be constrained both in the shape graph and in some underlying value abstraction; thus, we simply need to let our shape abstraction be a possible instance of the value abstraction.

In order to ensure correct mapping with the main memory, the sub-memory abstraction should carry not only a shape graph, but also a local environment describing how sub-memory cells are accessed. Therefore, the general form of a sub-memory value abstract domain predicate is:

Mem β, α + o 0 , α + o 1 , E s , G s &hd = 0xa0 &cur = 0xa4 0xb0 0xb4 0xb8 0xbc 0xb4 0xbc 0xbc 0xb0 0x0 0xb8 (a) Concrete store. α0 &hd α1 &cur α2 β 0 16 +4 +12 ν :        α 0 → 0xa0 α 1 → 0xa4 α 2 → 0xb0 β → 0xbc, 0xb0, 0x0, 0xb8 (
E s : 4 → δ 0 12 → δ 1 ν s : δ 0 → 0xb4 δ 1 → 0xbc (c) Sub-memory.
Fig. 4: Hierarchical abstraction where:

β ∈ V ♯ denotes the sub-memory contents; -[α + o 0 , α + o 1 [ denotes the range of addresses covered by the sub-memory (where α ∈ V ♯ is the base address of the block the sub-memory belongs to);

-G s ∈ D ♯
G is a shape graph describing the sub-memory; -E s : V ♯ L → V ♯ is a partial map from symbolic offsets (linear combination of symbolic variables) relative to α into nodes of sub-shape graph G s .

In practice, a store may contain several sub-memories, thus an abstract value of D ♯ V consists of a finite set of sub-memory predicates together with a regular abstract element of some other numerical domain to express arithmetic constraints among symbolic variables. We write

D ♯ V [sub] (resp., γ V [sub]
) for the sub-memory abstract domain (resp., concretization). Concretization function γ V [sub] : D ♯ V [sub] → P(Val) is formally defined as follows:

ν ∈ γ V [sub] (Mem β, α + o 0 , α + o 1 , E s , G s ) ⇐⇒ ∃(σ s , ν s ) ∈ γ G (G s ),    dom(σ s ) = [ν L (α + o 0 ), ν L (α + o 1 )[ ν(β) = read(σ s , ν L (α + o 0 ), ν L (α + o 1 )) ∀l ∈ V ♯ L , E s (l) = δ =⇒ ν L (α + l) = ν s (δ)
As an example, we consider in Fig. 4 the case of an array, used as a sub-memory which contains a list occupying the whole array (for the sake of simplicity, we assume list elements only have a next field). Fig 4a shows a concrete state, where the array has length 4, and all cells are part of a list. All physical addresses are shown and thin edges help visualize pointers. Fig. 4b shows the shape graph which abstracts the main memory together with the valuation used to concretize it into the store of Fig. 4a. Note that symbolic variable β is mapped into the concatenation of four 4-bytes values (we assume a 32 bits architecture), hence a value of length 16 bytes. The associated sub-memory predicate is displayed in Fig. 4c, with its shape graph, its environment and the valuation ν s used to concretize it appropriately. As G s summarizes the list into a segment predicate and an inductive predicate, some physical addresses (0xb0 and 0xb8) do not even appear in ν s .

In practice, the abstract states manipulated in order to analyze programs such as the code shown in Fig. 1c are more complex, yet the principle is the same as in the example of Fig. 4:

list elements have additional fields, so that the size of one structure element is 8 bytes or more, and the strides of the pointers in the free-pool region are multiple of that size s; -the overall size of the free-pool may be much larger, and could actually be kept abstract (i.e., the analysis would only know it is an unsigned number, that would be a multiple of s); -the sub-memory may not occupy the whole free-pool space (as is the case in the concrete store shown in Fig. 1b), so the free-pool corresponds to a segmentation with several outgoing edges; -the offsets in the main shape graph and in the sub-environment are non constant linear expressions over symbolic variables.

Static Analysis Algorithms in the Hierarchical Abstract Domain

We now describe the static analysis algorithms, which allow to infer precise invariants over both the main memory and the sub-memory for programs such as the insertion routine in Fig. 1c.

Structure of the analysis

For the most part, the analysis consists of a standard shape analysis following the principles of [START_REF] Chang | Shape analysis with structural invariant checkers[END_REF][START_REF] Chang | Relational inductive shape analysis[END_REF], which can be formalized as a 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]. The concrete semantics P of program P collects the set of states (l , M ) which are reachable from the entry point of P , after any sequence of execution steps: (l , M ) ∈ P if and only if (l 0 , M 0 ) → (l 1 , M 1 ) → . . . → (l n , M n ) → (l , M ), where l 0 is the entry point of P and → denotes the transition relation of P . The analysis computes invariants I l for all control states l , which consist of finite disjunctions of abstract states. The analysis is sound in the following sense:

Theorem 1 (Soundness). For all (l , M ) ∈ P , there exists M ♯ ∈ I l such that M ∈ γ S (M ♯ ).

To achieve this, we use sound transfer functions to compute abstract postconditions and sound abstract join and widening operators to over-approximate the effect of control flow joins. The abstract join operator is especially interesting in the sense that it may introduce or merge existing sub-memory predicates, which is why we consider it first (Sect. 4.2). Furthermore, another novelty is the need for all abstraction layers (main memory, sub-memory and other value abstract domains) to exchange information, as one analysis step typically requires some steps of computation be done in all layers (Sect. 4.3).

Abstract join and management of sub-memory predicates

In the beginning of the analysis, the contents of the memory is unknown, so no information is available in D ♯ V [sub] (the empty set of sub-memory predicates denotes the absence of sub-memory information). As the analysis progresses, sub-memory predicates may be introduced or be combined into new sub-memory predicates. Those operations are performed at control flow join points, by the shape abstract join (which serves both as an abstract union and as a widening).

The abstract join operator takes two inputs

M ♯ l = (E ♯ l , G l , V l ), M ♯ r = (E ♯ r , G r , V r ),

and computes an over-approximation

M ♯ o = (E ♯ o , G o , V o ).
To achieve such a result, the shape graph join computes matching partitions of the edges of G l and G r and approximates such corresponding sets of edges with edges into G o . These partitions are described by functions Ψ l , Ψ r : V ♯ → V ♯ , where Ψ l (resp., Ψ r ) maps nodes of G o into the nodes of G l (resp., G r ) that they over-approximate. In the following, we let Ψ (G) (resp., Ψ (o)) denote the renaming of all symbolic variables in graph G (resp., in offset o) by applying function Ψ . Then, the computation of G o takes the form of a sequence of rewriting steps over graph tuples:

(G l , G r , emp) = (G 0 l , G 0 r , G 0 o ) ⊔ (G 1 l , G 1 r , G 1 o ) ⊔ . . . . . . ⊔ (G k-1 l , G k-1 r , G k-1 o ) ⊔ (G k l , G k r , G k o ) = (emp, emp, G o ) where each step i is sound in the sense that ∀s ∈ {l, r}, γ S (E ♯ s , G i s * Ψ s (G i o ), V s ) ⊆ γ S (E ♯ s , G i+1 s * Ψ s (G i+1 o ), V s )
Each step corresponds to a rule, as defined in [START_REF] Chang | Relational inductive shape analysis[END_REF], such as, for instance:

-Rule (r-pt) over-approximates a pair of points-to edges with a new one:

  Ψ l (α) [Ψ l (o),Ψ l (o ′ )[ → Ψ l (β), Ψ r (α) [Ψr (o),Ψr(o ′ )[ → Ψ r (β), emp   ⊔   emp, emp, α [o,o ′ [ → β   .
-Rule (r-emp-seg) matches an empty region in G l with a region of G r that can be proved a particular case of a segment; one case of (r-emp-seg) is:

  emp, Ψ r (α) [Ψr (o),Ψr(o ′ )[ → Ψ r (β), emp   ⊔   emp, emp, α • list * = β • list   if Ψ l (α) = Ψ l (β).
All rules are shown in [START_REF] Chang | Relational inductive shape analysis[END_REF]. The soundness of each step guarantees the soundness of the result, given value the abstract element

V o = (Ψ l ) -1 (V l )▽ V (Ψ r ) -1 (V r ),
where ▽ V is a widening operator in D ♯ V (symbolic variables of inputs need be renamed using Ψ l , Ψ r to make value abstractions consistent), and environment

E ♯ o = (Ψ l ) -1 • E ♯ l .
In our setup, with points-to edges of non statically known size (Sect. 3.1) and with sub-memory predicates (Sect. 3.3), additional join rewriting rules need be considered, resulting in the introduction and in the fusion of submemory predicates, as part of ▽ V .

Theorem 2 (Soundness). For all

s ∈ {l, r}, γ S (E ♯ s , G s , V s ) ⊆ γ S (E ♯ o , G o , V o ). α o0 o1 β ⇐⇒ α o0 o1 β β = δ 0 o1 -o0 η E s : o 0 → δ V = [. . . ∧ η = β]
(a) Introduction of a sub-memory predicate.

α o0 o1 o2 β0 β1 Mem β 0 , α + o 0 , α + o 1 , E s,0 , G s,0 Mem β 1 , α + o 1 , α + o 2 , E s,1 , G s,1 =⇒ α β o0 o2 Mem β, α + o 0 , α + o 2 , E s,0 ⊎ E s,1 , G s,0 * G s,1
(b) Fusion of sub-memory predicates.

Fig. 5: Management of sub-memory predicates

Join over contiguous points-to edges. Unlike the abstract domain of [START_REF] Chang | Relational inductive shape analysis[END_REF], the abstraction shown in Sect. 3 copes with arrays, thus new rewriting rules need be added for the case where matching nodes Ψ l (α), Ψ r (α) are the origin of different numbers of points-to edges in both arguments. Thus, the extended algorithm adds a general rule (r-fusion) to re-partition such segmentations from a same node, as in array analyses such as [START_REF] Cousot | A parametric segmentation functor for fully automatic and scalable array content analysis[END_REF]. When the left segmentation has one edge and the right segmentation has two, (r-fusion) writes down as follows:

  Ψ l (α) [Ψ l (o),Ψ l (o ′′ )[ → Ψ l (β), Ψ r (α) [Ψr (o),Ψr(o ′ )[ → β 0 * Ψ r (α) [Ψr (o ′ ),Ψr(o ′′ )[ → β 1 , emp   ⊔   emp, emp, α [o,o ′′ [ → β  
where Ψ r maps β into the sequence β 0 , β 1 , i.e. expresses that symbolic variable β should over-approximate values corresponding to the concatenation of the values represented by β 0 and β 1 in G r . General (r-fusion) subsumes (r-pt).

Introduction and fusion of a sub-memory predicate. Whenever a shape graph contains a points-to edge, a sub-memory predicate can be introduced, as shown in Fig. 5a. When applying rule (r-fusion), such sub-memory predicates can be introduced in both join inputs, so as to capture the meaning of points-to edges in both inputs. However, this process generates two sub-memory predicates in the right hand side (and one in the left hand side), thus those sub-memory predicates need be combined together. This operation can be performed as shown in Fig. 5b.

Example of an abstract join. Fig. 6 shows a join similar to those found in the analysis of the code of Fig. 1c. For the sake of clarity, we show only a relevant fragment of the abstract states, and we express the relation between β 1 1 and α 1 in the value abstraction (in the analysis, it is actually represented as a looping points-to edge α 1

[o ′ 1 ,o ′ 1 +4[ → α 1 + o ′′ 1 )
. The abstract state shown in Fig. 6a describes a list stored in a sub-memory and pointed to by cur. Fig. 6b describes the situation after allocating an additional element in the free-pool, pointed to by cur. Join (Fig. 6c) applies rule (r-fusion) to the first two edges, introduces

α 0 β 0 0 β 0 1 &cur &hd 0 o0 o ′ 0 +o ′′ 0 +o ′′ 0 Mem β 0 0 , α 0 , α 0 + o 0 , E 0 s , G 0 s G 0 s : δ 0 0 list E 0 s : +o ′′ 0 → δ 0 0 V 0 = o 0 ≤ o ′ 0 ∧ 0 ≤ o ′′ 0 < o 0 (a) Left input (G0, V0). α 1 β 1 0 β 1 1 β 1 2 &cur &hd 0 o1 o1 + 4 o ′ 1 +o ′′ 1 +o 1 Mem β 1 0 , α 1 , α 1 + o 1 , E 1 s , G 1 s G 1 s : δ 1 0 list E 1 s : +o ′′ 1 → δ 1 0 V 1 =   o 1 + 4 ≤ o ′ 1 ∧ 0 ≤ o ′′ 1 < o 1 ∧ β 1 1 = α 1 + o ′′ 1   (b) Right input (G1, V1). α β0 β1 &cur &hd 0 o o ′ +o ′′ +o ′′′ Mem β 0 , α, α + o, E s , G s G s : δ0 δ1 list list E 0 s : +o ′′ → δ 1 +o ′′′ → δ 0 V =   o ≤ o ′ ∧ 0 ≤ o ′′ < o ∧ 0 ≤ o ′′′ < o   (c) Output (Go, Vo).
Fig. 6: Abstract join at the second iteration a sub-memory in G 1 , merges that sub-memory with the pre-existing one, and then performs an abstract join in the sub-memory. This sub-memory join then introduces a segment, thanks to rule (r-emp-seg).

Soundness of the abstract join and termination of the widening can be proved as in [START_REF] Chang | Relational inductive shape analysis[END_REF]. The implementation is also similar (in particular, the algorithm actually infers partitions Ψ l , Ψ r as part of the sequence of rewriting steps leading to G o ).

Abstract transfer functions

Abstract transfer functions compute over-approximated abstract post-conditions for each elementary concrete operations. When analyzing a statement (such as an allocation, an assignment, a test...) between control states l and l ′ , the analyzer should evaluate a transfer function transfer ♯ l ,l ′ . This transfer function should satisfy the soundness condition below:

M ∈ γ S (M ♯ ) ∧ (l , M ) → (l ′ , M ′ ) =⇒ M ′ ∈ γ S (transfer ♯ l ,l ′ (M ♯ ))
Analysis of an assignment: In the following, we consider the analysis of the assignment lv := ex between l and l ′ , where lv is an l-value and ex an expression (the other transfer functions are similar, thus we formalize only assign). In the concrete level, lv (resp., ex ) denotes the semantics of lv (resp., ex); it maps a memory state into an address (resp., a numeric or pointer value). Then, the concrete transitions corresponding to that assignment are of the form (E, σ) → (E, σ ′ ), where

σ ′ = σ[ lv (E, σ) ← ex (E, σ)].
In the abstract level, lv ♯ (resp., ex ♯ ) returns a node with offset α + o denoting the address of the cell to modify (resp., a node with offset β ′ + o ′ denoting the value to assign). When the abstract pre-condition shape graph G contains a points-to edge α+o → β, assign should simply replace this edge with points-to edge α + o → β ′ + o ′ . However, some transformations may need be done on G before this trivial assign can be applied:

α0 &cur α β 0 o1 +o 0 Mem β, α, α + o 1 , E s , G s G s : δ0 δ1 next list E s : o 0 → δ 0 (a) Pre-condition. α0 &cur α β 0 o1 +o ′ 0 Mem β, α, α + o 1 , E s , G s G s : δ0 δ1 next list E s : o 0 → δ 0 o ′ 0 → δ 1 (b) Post-condition.
Fig. 7: Analysis of the assignment cur = cur->next -When the evaluation of either lv or ex requires accessing fields which are not materialized, as they are summarized as part of inductive or segment edges, those should be unfolded first [START_REF] Chang | Relational inductive shape analysis[END_REF]. -When ex is a non trivial numeric expression, it should be analyzed in the value domain. Let us consider the case where ex is 4 * x + 8. That expression should be transformed by replacing all l-values with nodes corresponding to their addresses, which gives an expression of the form 4 • δ + 8. A fresh node β ′ should be added to G. The assignment β ′ ← 4 • δ + 8 should be analyzed in the value domain, using sound abstract transfer function assign V ♯ . Then, the assign proceeds as above, by switching a points-to edge. In the following, we extend this operator to the hierarchical abstract domain. We assume abstract pre-condition (E ♯ , G, V ) contains at least one sub-memory Mem β, α + o 0 , α + o 1 , E s , G s , and describe the analysis assignment lv := ex. As cases where the assignment only affects the main memory are unchanged, we consider only the cases where it involves a read or a write into the sub-memory, and show what changes need be done to the classic assign operator.

Read in a sub-memory. Let us consider statement cur = cur->next, with the abstract pre-condition shown in Fig. 7a. Then, l-value cur evaluates into α 0 , which is the origin of points-to edge α 0 → α + o 0 . The evaluation of r-value cur->next is more complex, as cur points into the sub-memory, at offset o 0 . However, the environment maps o 0 into sub-memory node δ 0 , which has a next field, pointing to δ 1 . Thus, in the sub-memory, the r-value evaluates to δ 1 . The effect of the assignment is thus captured by an update to the main memory edge destination offset (o ′ 0 instead of o 0 ) and an update to the sub-environment to reflect this new mapping (Fig. 7b). To summarize, sub-memory pointer reads can be handled like normal pointer reads, where the base address is represented by the sub-memory based node.

When the read operation returns a node that does not appear in the submemory environment (and thus, cannot be seen from the outside), an equality constraint between that node and an external fresh node should be generated in V ♯ , so as to capture the effect of the assignment. G s,0 :

δ 0 0 list E s,0 : o 0 → δ 0 0 Mem β 1 , α + o ′ 0 , α + o ′ 0 + 4, E s,1 , G s,1
G s,1 :

δ 1 0 δ 1 1 next E s,1 : o 1 → δ 1 0 (a) Pre-condition. α β0 β1 &a &b 0 o ′ 0 o ′ 0 + 4 +o 0 +o 1 Mem β 0 , α, α + o ′ 0 , E s,0 , G s,0
G s,0 :

δ 0 0 list E s,0 : o 0 → δ 0 0 Mem β 1 , α + o ′ 0 , α + o ′ 0 + 4, E s,1 , G s,1
G s,1 :

δ 1 0 δ 1 2 δ 1 1 next E s,1 : o 1 → δ 1 0 V = [δ 0 0 = δ 1 2 ]
(b) Post-condition. Write in a sub-memory. We now consider the case of an assignment to a structure field inside a sub-memory. In Fig. 8, we show an abstract pre-condition and an abstract post-condition computed from it, in the case of assignment b->next = a where a and b are two pointers into a free-pool. This abstract state arises after introduction of two sub-memories, and before their fusion by a join operator (Sect. 4.2). The effect of the assignment is local to the sub-memory where b points to:

a new node δ 1 2 is created with the equality constraint that it is equal to δ 0 0 ; -sub-memory points-to edge δ 1 0

• next → δ 1 1 is replaced with δ 1 0 • next → δ 1 2 .
The second operation is actually performed as part of the evaluation of assign V ♯ over the sub-memory which content is bound to β 1 . Past this step, the invariant attached to that sub-memory includes pointers leaving the sub-memory itself (to the other sub-memory). Similar situations arise in the program of Fig. 1c, when updates are done inside the free-pool. Moreover, when the sub-memory cell that need be assigned is part of a folded inductive predicate, classical inductive predicate unfolding techniques [START_REF] Chang | Relational inductive shape analysis[END_REF] apply.

Soundness. Operator assign is sound:

Theorem 3 (Soundness). Let M = (E, σ) ∈ γ S (M ♯ ). If we let a = lv (M ) and v = ex (M ), then (E, σ[a ← v]) ∈ γ S (assign(lv, ex, M ♯ )).

Prototype and Implementation

We integrated the hierarchical abstraction into the MemCAD analyzer (Memory Compositional Abstract Domain, http://www.di.ens.fr/˜rival/memcad.html). It was implemented as a functor, which lifts a shape abstract domain into a value abstract domain, which can in turn be fed into the shape abstract domain functor. Numerical abstract invariants (D ♯ V ) are represented in a numerical domain complying with the Apron [START_REF] Jeannet | Apron: A library of numerical abstract domains for static analysis[END_REF] interface. The experiments below use convex polyedra [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF]. The results obtained when running it on a series of routines that build and manipulate a sub-structure in a free-pool are shown in the table below (in the third column), and are compared with times to analyze similar routines using regular memory allocation system call malloc (second column), which do not require the hierarchical abstraction. Run-times are given in seconds, as observed with an Intel Core i3 CPU laptop running at 2.10 GHz, with 4 Gb of RAM. The analysis is fully automatic and inputs only a generic list inductive definition (Sect. 2) and the unannotated source code. The set of codes considered in the table below includes running, our main example (Fig. 1c), as well as other basic operations on the dynamic structure (head and tail insertion, flipping of cells, drop of a cell). Those comprise all typical features of a the user defined allocator based on a static free-pool as found in running. While the industrial code of [START_REF] Miné | Static analysis of run-time errors in embedded critical parallel c programs[END_REF] never "deallocates" cells (instead, it sometimes reset the free-pool, before building a new structure in it), we included a drop example, where a cell is selected and removed from the linked list, yet cannot be reused; such cells are abstracted from the sub-memory contents (those cells are abstracted into a . . . * true predicate [23] i.e., a heap region nothing is known about In all those examples, MemCAD infers a precise abstract description of all dynamic structures in the free-pool or in the main memory, and proves memory safety. We observe a 2X to 3X slowdown in the analyses of codes using a free-pool. The difference is justified by the extra burden of maintaining the sub-memory predicates together with the array segmentation and side numerical predicates over offsets. While noticeable, this slowdown is very reasonable, as the properties which are inferred are strong and memory safety is proved. Last, we remarked that the current implementation of the MemCAD analyzer does not feature a very efficient management of symbolic disjunctions of abstract states; addressing that separate issue would improve timings significantly.

Related Works and Conclusion

Our hierarchical abstract domain allows to design memory abstractions in a modular way, which relates to the layout of data-structures used in programs. This modularity makes the analysis design simpler while preserving its characteristics (precision and performance). Our abstract domain is parametric in the data of an underlying value abstraction (so that more complex abstract domains could be used in order to deal with values), and in the data of a set of structure inductive definitions (our test case uses only lists, but the analysis would be very similar if doubly-linked lists or trees were built inside the free-pool instead of singly linked lists). Furthermore, our proposal integrates much of the power of array analyses such as [START_REF] Gopan | A framework for numeric analysis of array operations[END_REF][START_REF] Halbwachs | Discovering properties about arrays in simple programs[END_REF][START_REF] Cousot | A parametric segmentation functor for fully automatic and scalable array content analysis[END_REF] into a shape analysis framework [START_REF] Chang | Shape analysis with structural invariant checkers[END_REF][START_REF] Chang | Relational inductive shape analysis[END_REF]. This was made possible by the structure of the abstraction proposed in [START_REF] Chang | Relational inductive shape analysis[END_REF], which allows a nice combination with a value abstraction. While that value abstraction was initially set to be a numerical abstraction, our hierarchical abstract domain shows that much more complex structures can be devolved to an underlying domain. This allows a very modular design for the static analyses. We notice that the notion of array partition of [START_REF] Cousot | A parametric segmentation functor for fully automatic and scalable array content analysis[END_REF] plays a similar role as the partition used in abstract join [START_REF] Chang | Relational inductive shape analysis[END_REF] of shape graphs. Like [START_REF] Cousot | A parametric segmentation functor for fully automatic and scalable array content analysis[END_REF], our analysis does not require a pre-analysis to discover array partitions, following the principles of the shape join of [START_REF] Chang | Relational inductive shape analysis[END_REF]. Composite structures are a common issue in the shape analysis field [START_REF] Marron | Heap analysis in the presence of collection libraries[END_REF][START_REF] Distefano | A local shape analysis based on separation logic[END_REF][START_REF] Dillig | Precise reasoning for programs using containers[END_REF]. An important contribution of our proposal is to decompose the abstract domain into smaller domains, which are easier to implement and to reason about.

Gulwani et al. [START_REF] Gulwani | A combination framework for tracking partition sizes[END_REF] enhance shape abstract domains with numerical information so as to reason about the size of arrays stored in linked list elements. Their analysis does not allow to reason about the structure contents whereas our approach allows to delegate such a description to a generic value domain (which may store shape information, when the arrays store complex structures). In [START_REF] Calcagno | Beyond reachability: Shape abstraction in the presence of pointer arithmetic[END_REF], Calcagno et al. address the safety of general memory allocators, like the C malloc, using an ad-hoc abstract domain based on separation logic, which embeds both shape and numerical information. Their work addresses a separate set of cases than ours, as their approach could not deal with our user-defined pseudoallocator whereas MemCAD does not handle their examples at this point. As this analysis considers the allocator separately from the code, it can abstract away the contents of memory block. The analysis of [START_REF] Lee | Program analysis for overlaid data structures[END_REF] targets overlaid dynamic structures, which is also a completely separate issue than that of our application specific memory allocator, and relies on very different techniques.

The most important future work is the integration of our shape abstraction into an analyzer such as Astrée [START_REF] Blanchet | A static analyzer for large safety-critical software[END_REF], which would effectively improve the analysis of embedded applications such as those considered in [START_REF] Monniaux | Verification of device drivers and intelligent controllers: a case study[END_REF][START_REF] Miné | Static analysis of run-time errors in embedded critical parallel c programs[END_REF]. This represents a considerable amount of work as no standard interface has been set up so far for memory abstractions, unlike numerical abstractions. We believe our work actually achieves a step in that direction, as the design of the hierarchical abstraction imposed a careful assessment of abstract domain component interfaces. Other future works include the support of non-contiguous segmentations, which would allow the analysis of a wide family of memory allocators. Last, our framework supports the composition of more than two levels of hierarchical abstractions, e.g., to analyze lists of elements containing arrays, that are stored inside large static zones, thus we could consider such examples.

1

  typedef struct Cell { struct Cell * nex t ; 3 i n t p r i o ; / * other f i e l d s * / 5 } Cell ; Cell f r e e p o o l [ 1 0 0 ] ; (a) Data-type and free-pool.1 . . .

  f r e e i d x ; Cell * hd , * t l ; 4 hd = n u l l ; t l = n u l l ; 6 f o r ( f r e e i d x = 0 ; f r e e i d x < 1 0 0 ; f r e e i d x ++) { i n t p r i o r i t y ; / * = computation ( ) ; * / 8 i f ( hd == n u l l ) { / * i n s e r t f i r s t c e l l * / } e l s e i f ( p r i o r i t y < hd->p r i o ) { / * i n s e r t as head * / } e l s e i f ( p r i o r i t y >= t l ->p r i o ) { / * i n s e r t as queue * / } e l s e { Cell * c u r = hd ; while ( p r i o r i t y >= cur->next->p r i o ) { c u r = cur->nex t ; } a s s e r t ( c u r != t l ) ; // p o s i t i o n f ound f r e e p o o l [ f r e e i d x ] . nex t = cur->nex t ; f r e e p o o l [ f r e e i d x ] . p r i o = p r i o r i t y ; cur->nex t = &f r e e p o o l [ f r e e i d x ] ; } } } (c) Insertion routine.

Fig. 2 :

 2 Fig. 2: Hierarchical abstraction

  where o 0 , o 1 , o 2 are linear expressions over symbolic variables, describes a contiguous region between the addresses represented by α + o 0 and α + o 1 and storing the value represented by β + o 2 (thus its size corresponds to o 1o 0 ). Edge α • ι abstracts complete structures described by inductive definition ι, at address α. Segment α • ι * = β • ι abstracts incomplete structures, that is a structures starting at address α with a hole at address β, i.e. a missing sub-structure at address β. The semantics of inductive and segment

ν

  : β → 24 × 65536 + 48 (c) Single edge.

Fig. 3 :

 3 Fig. 3: Segmentations representing an array of two unsigned short integers

1

 1 Mem β 0 , α, α + o ′ 0 , E s,0 , G s,0

Fig. 8 :

 8 Fig. 8: Analysis of the assignment b->next = a

  b) Main memory abstraction. β, α 2 , α 2 + 16, E s , G s

	Mem δ0	δ1
	list	list

  ).

	Program	Allocation method Description malloc free-pool array
	running	0.195	0.520 The running example
	head	0.019	0.034 List, head-insertion
	tail	0.027	0.050 List, tail-insertion
	traversal 0.056	0.107 List, tail-insertion then traversal
	flip	0.139	0.323 List, flipping two cells after selection
	drop	0.104	0.289 List, dropping a cell after selection
	integers	NA	0.016 Initialization of an array to zeros

Acknowledgments. We thank the members of the MemCAD group for discussions and the reviewers for suggestions that helped improving this paper.

⋆ The research leading to these results has received funding from the European Research Council under the FP7 grant agreement 278673, Project MemCAD.