Alain Gély
email: alain.gely@loria.fr

Miguel Couceiro
email: miguel.couceiro@loria.fr

Amedeo Napoli
email: amedeo.napoli@loria.fr

Towards Distributivity in FCA for Phylogenetic Data

It is known that a distributive lattice is a median graph, and that a distributive ∨-semilattice can be thought of as a median graph iff every triple of elements such that the infimum of each couple of its elements exists, has an infimum. Since a lattice without its bottom element is obviously a ∨-semilattice, using the FCA formalism, we investigate the following problem: Given a semilattice L obtained from a lattice by deletion of the bottom element, is there a minimum distributive ∨-semilattice L d such that L can be order embedded into L d ? We give a negative answer to this question by providing a counter-example.

Motivation

Lattices and median graphs are two structures with many applications, in particular in classification and knowledge discovery. Median graphs are especially used in biology, for example in phylogeny, for modeling inter-species relationships. In phylogeny, one of the main problems is to find evolution trees for representing existing species from accessible DNA fragments. When several trees are leading to the same inter-species phylogenetic relationship, the preferred ones are the most "parsimonious", where the number of modifications such as mutations for example, is minimal for the considered species. However, several possible parsimonious trees may exist simultaneously. Such a situation arises with inverse or parallel mutations,

e.g., when a gene goes back to a previous state or the same mutation appears for two non-linked species. This calls for a generic representation of such a family of trees.

Bandelt et al. [START_REF] Bandelt | Median algebras[END_REF][START_REF] Bandelt | Median-joining networks for inferring intraspecific phylogenies[END_REF] propose the notion of median graph to overcome this issue, since it was noticed that a median graph may encode all parsimonious trees. It is known that median graphs are related to lattices (see, e.g., [START_REF] Avann | Median algebras[END_REF][START_REF] Bandelt | Median algebras[END_REF]). Any distributive lattice is a median graph, and any median graph can be thought of as a distributive ∨-semilattice such that for all x, y, z if the supremum of each pair exists, then the supremum {x, y, z} also exists.

Formal Concept Analysis (FCA) is based on lattice theory and can be used in classification and knowledge discovery. Uta Priss [START_REF] Priss | Concept lattices and median networks[END_REF][START_REF] Priss | Representing median networks with concept lattices[END_REF] made a first attempt to use the algorithmic machinery of FCA and the links between distributive lattices and median graphs, to analyze phylogenetic trees. However, not every concept lattice is distributive, and thus FCA alone does not necessarily outputs median graphs. A transformation should be designed to build a median graph from a concept lattice. In [START_REF] Priss | Representing median networks with concept lattices[END_REF] Uta Priss sketches an algorithm to convert any lattice into a median graph. The key step is to transform any lattice into a distributive lattice. However, how to transform a lattice into a distributive one is not detailled in this paper.

In [START_REF] Bandelt | Median networks: speedy construction and greedy reduction, one simulation, and two case studies from human mtdna[END_REF], Bandelt uses a data set from [START_REF] Vigilant | Mitochondrial dna sequences in single hairs from a southern african population[END_REF] to illustrate and evaluate a median graph. In this introduction, we will re-use it to show the differences between median graph and FCA approaches. The example is an extract of mitochondrial DNA for 15 Kung individuals from a Khoisan-speaking hunter-gathered population in southern Africa. For some sequences in mitochondrial DNA (nucleotide positions, denoted by a, b, . . . , j in table), a binary information indicates if a group of individuals owns the consensus version of the sequence (empty cell) or a variation for this sequence (× value). Eight individual groups are studied because some individuals share the same variants. For example, group 0 stands for 4 similar individuals in [START_REF] Bandelt | Median networks: speedy construction and greedy reduction, one simulation, and two case studies from human mtdna[END_REF]. Individual group with no variation on any nucleotide positions (consensus group) is not shown on the table. These data are shown in Fig. 1.a For these data, the median graph is shown in Fig. 1.b. Vertices are either individual group (numbered from 0 to 7) or latent vertices (spotted as Lx), added such that from a group to an adjacent one, only one variation exists for nucleotide sequences (principle of parsimony supposes that there is no chance that two variations arise exactly at the same moment for the same population in evolutionary process). This variation is indicated on edges. As an example, from consensus group to vertex L4, the only variation occurs in sequence k, from vertex L4 to vertex 0 the only variation occurs in sequence j.

As stated, this graph contains every parsimonious tree as covering tree. Median graph owns others good properties: remove edges labeled with a sequence variation produces two disconnected parts. One corresponds to individuals with the variation, the other without the variation. For example, with edges labelled j, one can partition the vertices in two connected components: vertices L1, 0, 2, 4 and 7 are individuals with a variant on position j. Vertices in the other connected component represent individuals without this variant.

For individuals represented by vertex 0, there is not enough data to determine if the evolutionary path from the consensus started with a variant on k position (giving latent vertex L4) or started with a variant on j (giving latent vertex L1)? Strength of median graph is to display these two possibilities, which is not possible with a parsimonious tree.

Since data is a binary table, Formal Concept Analysis can be applied. The concept lattice obtained from the data is shown in Fig. 1.c. In general, it does not correspond to a median graph. To build a median graph, a necessary condition is to have a distributive ∨-semilattice. In [START_REF] Gély | Steps towards achieving distributivity in formal concept analysis[END_REF], based on the work of Birkhoff and FCA formalism, we propose an algorithm to compute such a semilattice (and the corresponding data table). The result of this algorithm, transforming a concept lattice into a median graph, is given in Fig. 1.d. Since FCA is supported by a wide community, the main idea of this research is to be able to use FCA results and software to deal with phylogenetic data and median graphs.

Remark that, for this particular data set the algorithm computes the median graph obtained by Bandelt in [START_REF] Bandelt | Median networks: speedy construction and greedy reduction, one simulation, and two case studies from human mtdna[END_REF]. Unfortunately, in some cases the algorithm returns a distributive ∨-semilattice L d that is not minimal: There exists L d such that L can be embedded in L d and L d can be embedded L d .

The continuation of [START_REF] Gély | Steps towards achieving distributivity in formal concept analysis[END_REF] is to search for an algorithm which outputs a minimal distributive ∨-semilattice. Since we look for minimality, a natural question arises: does a unique minimal distributive ∨-semilattice L d exist? In this paper, we propose a counter-example which shows that a minimum distributive ∨-semilattice does not always exist.

In the following section, we recall definitions and notation for the understanding of this paper. We then sketch the limitations of our algorithm and show in Sect. 4 that a minimum distributive ∨-semilattice does not exist. We conclude this paper by some remarks and perspectives in Sect. 5.

Models: Lattices, Semilattices, Median Algebras and Median Graphs

In this section we recall basic notions and notation needed throughout the paper. We will mainly adopt the formalism of [START_REF] Ganter | Formal Concept Analysis: Mathematical Foundations[END_REF], and we refer the reader to [START_REF] Caspard | Finite ordered sets: concepts, results and uses[END_REF][START_REF] Davey | Introduction to Lattices and Order[END_REF] for further background. In this paper, all sets are supposed to be finite.

Lattices and FCA

A partially ordered set (or poset for short) is a pair (P, ≤) where P is a set and ≤ is a partial order on P, that is, a reflexive, antisymmetric and transitive binary relation on P. An upper (resp. lower) bound of X ⊆ P is an element y ∈ P such that ∀x ∈ X, x ≤ y (resp y ≤ x). For X ∈ P, the lowest upper bound, if it exists, is called the join or the supremum. The greatest lower bound, if it exists, is called the meet or the infimum.

a b c d e f g h i j k 0 × × × 1 × × 2 × × 3 × × 4 × × × × 5 × 6 × × × 7 × × × a. b. c. d.
A ∨-semilattice (L, ≤) is an ordered set such that the supremum exists for all X ⊆ L, X = / 0. For x, y ∈ L, x ∨ y denotes the supremum. Such an order has a lowest element (bottom) denoted by ⊥ = L. A ∧-semilattice (L, ≤) is an ordered set such that the infimum exists for all X ⊆ L. For x, y ∈ L, x ∧ y denotes the infimum. Such an order owns a greatest element (top) denoted by = L. A lattice (L, ≤) is an ordered set such that a supremum and an infimum exist for all X ⊆ L.

An element ≤). e (J (L), ≤) poset for ideal lattice in d. Note that N 5 can be order-embedded in the lattice . Concepts (X,Y) are maximal rectangles of the contexts. For an element e of the lattice, the corresponding concept

x ∈ L such that x = y∨z implies x = y or x = z is called a ∨-irreducible element. Dually, an element x ∈ L such that x = y ∧ z implies x = y or x = z is (J (L), M (L), ≤) a b c 1 × × 2 × 3 × a. (J (L), J (L), ≥) 1(c) 2(d) 3(b) 1 × × 2 × 3 × × b. c. d. e.
(X,Y ) is X = { j ∈ J (L) | j ≤ e} and Y = {m ∈ M (L) | m ≥ e}.
For example, the element with label d is the concept ({1, 3}, {d}).

called a ∧-irreducible element. We will denote the set of ∧-irreducible elements and ∨-irreducible elements of L by M (L) and J (L), respectively. Observe that both M (L) and J (L) are posets when ordered by ≤.

Posets and lattices can be represented and visualized by their Hasse-diagrams [START_REF] Davey | Introduction to Lattices and Order[END_REF]. Examples of lattices are given in Fig. 2 and Fig. 3. N 5 and M 3 lattices are involved in non distributivity (see Sect. 2.2). In Figs. 2 and3, ∨-irreducible elements are labeled with numbers and ∧-irreducible elements are labeled with letters. Some elements, doubly irreducible, have two labels. This is the case in Fig. 3.c for element which is labeled either by 1 and a and for element which is labeled either by 3 and c. Elements with labels d and e are ∧-irreducible (but no ∨-irreducible). Element with label 2 is ∨-irreducible (but no ∧-irreducible). Formal Concept Analysis [START_REF] Ganter | Formal Concept Analysis: Mathematical Foundations[END_REF] uses concept lattices for data analysis tasks. Concept lattices are built from a binary table, which is called a formal context, by the way of prime ( ) operators

We denote by (G, M, I) a formal context where G is a set of objects, M a set of attributes and I an incidence relation between objects and attributes. In phylogenetic data, objects are usually species, attributes are mutations, and (g, m) ∈ I -or gImindicates that mutation m is spotted in species g. Definition 1. For a set X ⊆ G, Y ⊆ M we define:

X = {y ∈ M | xIy for all x ∈ X} Y = {x ∈ G | xIy for all y ∈ Y } (J (M 3 ), M (M 3 ), ≤) a b c 1 × 2 × 3 × a. c. (J (L), M (L), ≤) a c d e 1 × × 2 × × 3 × × b. d. Fig. 3 a the standard context for lattice M 3 . b the standard context (J (L), M (L), ≤) for L in Fig. 3.d c M 3 is a non distributive lattice. d A non distributive lattice L such that (J (L), ≤) = (J (M 3 ), ≤).
Then a formal concept is a pair (X,Y ) where X ⊆ G, Y ⊆ M and X = Y and Y = X. X is the extent and Y is the intent of the concept. They are closed sets as they verify X = X and Y = Y . The set of all formal concepts ordered by inclusion of the extents -dually the intents-denoted by ≤ generates the concept lattice of the context (G, M, I). The existence of a supremum and an infimum allows to use lattices for classification process. Concepts can be viewed as classes, indeed a concept (X,Y ) is a representation of a maximal set of objects X which share a maximal set of attributes Y . If another concept (X 1 ,Y 1 ) is greater than (X,Y ), it contains more objects, but described by fewer attributes. X 1 is a class, more general than X.

A clarified context is a context such that x = y implies x = y for any element of G and any element of M. In a clarified context, the set of attributes of two distinct objects are distinct, and dually for objects. Moreover, a clarified context is reduced iff it does not contain:

• a vertex g ∈ G such that g = X with X ⊆ G, g ∈ X • a vertex m ∈ M such that m = Y with Y ⊆ M, m ∈ Y Indeed, a vertex x ∈ G such that x = X with X ⊆ G, x ∈ X
is a reducible element (since it intent may be obtained by elements in the set X). Only irreducible elements, which are not join or meet of other elements, are necessary to build a lattice. The reduced context is also called a standard context [START_REF] Ganter | Formal Concept Analysis: Mathematical Foundations[END_REF]. The standard context of lattice L is such that G = J (L) and M = M (L). Examples of standard contexts are given in Fig. 2 and Fig. 3 with their corresponding concept lattice.

Distributive Lattices

As stated in the motivations, median graphs are used for phylogenetic purposes, and encode a family of trees. It is known that theses graphs can be considered as particular distributive ∨-semilattices. This subsection provides basic notions about distributive (semi)lattices.

A lattice is distributive if ∧ and ∨ are distributive with respect to each other. Formally, a lattice L is distributive if for every x, y, z ∈ L, we have that one (or, equivalently, both) of the following identities holds:

(i) x ∨ (y ∧ z) = (x ∨ y) ∧ (x ∨ z), (ii) x ∧ (y ∨ z) = (x ∧ y) ∨ (x ∧ z).
Distributive lattices appear a natural choice for any classification task or as computation and semantic models; see, e.g., [START_REF] Caspard | Finite ordered sets: concepts, results and uses[END_REF][START_REF] Davey | Introduction to Lattices and Order[END_REF][START_REF] Hopcroft | Introduction to Automata Theory, Languages and Computability[END_REF][START_REF] Mattern | Virtual time and global states of distributed systems[END_REF]. This is partially due to the fact that any distributive lattice can be thought of as a sublattice of a power-set lattice, i.e., the set P(X) of subsets of a given set X.

Note that the definition of a sublattice is more constraint than the definition of a suborder: A subset X ⊆ L is a sublattice of L if for every x, y ∈ X we have that x ∧ y, x ∨ y ∈ X. For example, N 5 (Fig. 2.c) is a suborder of the lattice in Fig. 2.d, but is not a sublattice. Indeed, 1 ∨ 3 is not the same element in the two lattices.

The distributivity property of lattices has been equivalently described in several ways. One of these properties relies on the notion of sublattice, as follows: Property 1. L is a distributive lattice iff it contains neither N 5 nor M 3 as sublattices.

This property describes distributive lattices in terms of two forbidden structures, namely, M 3 and N 5 that are, up to isomorphism, the smallest non distributive lattices. N 5 is represented in Fig. 2.c and M 3 is represented in Fig. 3.c. In Fig. 2.d the lattice does not contain N 5 nor M 3 as sublattices, and so is distributive. In Fig. 3.d the lattice does not contain M 3 as sublattice, but contains N 5 as a sublattice, and so, is not distributive.

Our goal is to transform a lattice into a distributive one. For this particular task, the Birkhoff's representation of distributive lattice is of practical interest. It uses the notion of order ideal, recalled here: Definition 2 (Order Ideal). Let (P, ≤) be a poset. For a subset X ⊆ P, let ↓ X = {y ∈ P : y ≤ x for some x ∈ X} and ↑ X = {y ∈ P : x ≤ y for some x ∈ X}. A set

X ⊆ P is a (poset) ideal (resp. filter) if X =↓ X (resp. X =↑ X). If X =↓ {x} (resp.
X =↑ {x}) for some x ∈ P, then X is said to be a principal ideal (resp. filter) of P. For principal ideals, we omit brackets, so that ↑ x (resp. ↓ x) stands for ↑ {x} (resp.

↓ {x})

Birkhoff's representation of distributive lattices. Let (P, ≤) be a poset and consider the set O(P) of ideals of P, i.e.,

O(P) = { x∈X ↓ x | X ⊆ P}. (J (L), J (L), ≥) 1( f ) 2(e) 3(d) 1 × × 2 × × 3 × × a. b. c.
Fig. 4 a The context (J (L), J (L), ≥) for (J(L), ≤) the poset induced by ∨-irreducible elements of lattices in Fig. 3. b (J (L), ≤) for L (or equivalently M 3 in Fig. 3. c Ideal lattice for (J (L), ≤) (equivalently (J (M 3 ), ≤)). M 3 and L can be order-embedded in this lattice.

It is well-known that for every poset P, the set O(P) ordered by inclusion is a distributive lattice, called ideal lattice of P [START_REF] Birkhoff | Rings of sets[END_REF][START_REF] Birkhoff | Representations of lattices by sets[END_REF]. Furthermore, the poset of ∨irreducible elements of O(P) is J ((O(P))) = {↓ x | x ∈ P} and it is (order) isomorphic to P. This representation is used to provide a distributive lattice L d with the same poset of ∨-irreducible elements as an arbitrary lattice L. In this case, L is order-embedded in L d . For example, in Fig. 2.d, the lattice is the ideal lattice of (J (N 5 ), ≤). In the same way, the two lattices in Figs. [START_REF] Bandelt | Median algebras[END_REF].c and 3.d have the same poset of ∨-irreducible elements, and can be order embedded in the ideal lattice of this poset, represented in Fig. 4. In particular, in [START_REF] Nation | The lattice of completions of an ordered set[END_REF][START_REF] Bordalo | The lattice of strict completions of a poset[END_REF] it is shown that the family of lattices with the same poset of ∨-irreducible elements is itself a lattice, an so there exists a minimum element.

From a poset P, it is possible to obtain the context of the ideal lattice as C ideal(P) = (P, P, ≥). For a standard context C = (J (L), M (L), ≤), the standard context of the ideal lattice of (J (L), ≤) is C ideal(J) = (J (L), J (L), ≥). Note also that, for every distributive lattice L, the two posets J (L) and M (L) are dually-isomorphic. This is why the standard contexts of distributive lattices are "squares" (|J (L)| = |M (L)|), and are built with the information of only one of these two posets.

In the following subsection, we give some hints about median graphs and median algebras. As we will soon observe, the class of median graphs is in correspondence with a particular subclass of distributive ∨-semilattices.

Let L be a ∨-semilattice and x ∈ L, then ↑ x is a lattice (in the finite case, every ∨semilattice with a lowest element is a lattice). Then a ∨-semilattice L is distributive iff ↑ x is distributive, for all x [START_REF] Caspard | Finite ordered sets: concepts, results and uses[END_REF]. In practice, it is sufficient to check this property only for minimal elements of L. Indeed, filters of non minimal elements are sublattices of a minimal element filter, and sublattices of distributive lattices are distributive.

Median Graphs

As said in the introduction, a median graph encodes all parsimonious phylogenetic trees. A median graph is a connected graph having the median property, i.e. for any three vertices a, b, c, there is exactly one vertex x which lies on a shortest path between each pair of vertices in {a, b, c}.

The following characterization of distributive lattices explains some links of distributive lattice with median graphs and median algebras. Property 2. A lattice L is a distributive lattice iff for all x, y, z ∈ L,

(x ∧ y) ∨ (y ∧ z) ∨ (z ∧ x) = (x ∨ y) ∧ (y ∨ z) ∧ (z ∨ x).
This property establishes a correspondence between distributive lattices and median algebras. Indeed, a median algebra is a structure (M, m) where M is a nonempty set and m : M 3 → M is an operation, called median operation, that satisfies the following conditions m(a, a, b) = a and m(m(a, b, c), d, e) = m(a, m(b, c, d), m(b, c, e)), for every a, b, c, d, e ∈ M.

It is not difficult to see that if L is distributive, then m(a, b, c) = (a ∧ b) ∨ (b ∧ c) ∨ (c ∧ a)
is a median operation. The connection to median graphs was established by Avann [START_REF] Avann | Median algebras[END_REF] who showed that every median graph is the Hasse diagram of a median algebra (thought of as a semilattice). For further background on median structures see, e.g., [START_REF] Bandelt | Median algebras[END_REF]. This result was later used by Bandelt [START_REF] Bandelt | Median-joining networks for inferring intraspecific phylogenies[END_REF] to establish the link between distributive lattices and median graphs. Property 3. A graph is a median graph iff it is isomorphic to a ∨-semilattice L with the two following properties:

• L is distributive • for all x, y, z ∈ L such that (x ∧ y), (y ∧ z) and (z ∧ x) are defined, (x ∧ y ∧ z) is defined.

Algorithm to Produce a Distributive ∨-Semilattice

To build a median graph from a context using FCA, a necessary condition is to build a distributive ∨-semilattice. For the concept lattice L, it is always possible to consider the semilattice L ∨ = L\⊥ (L minus the lowest element). Minimal elements of this semilattice L ∨ are minimal elements of (J (L), ≤). It remains to transform the filter of these elements into a distributive lattice. Our previous work [START_REF] Gély | Steps towards achieving distributivity in formal concept analysis[END_REF] is based on Birkhoff's representation of a distributive lattice. Since sublattices of a distributive lattice are distributive, a simple way to obtain a distributive ∨-semilattice from a lattice L is to map L into the ideal lattice of (J(L), ≤). In practice, the bottom element exists because of the existence of infimum in lattice, but it usually does not carry semantic information for classification. For example, trees are median graphs and so distributive ∨-semilattice (considering the root as the greatest element) but obviously not lattices. With the addition of a bottom element ⊥, the trees become lattices. There is no reason that these lattices are distributive. Two trivial examples are N 5 and M 3 : Once the lowest element is removed, either N 5∨ = N 5 \⊥ and M 3∨ = M 3 \⊥, considered as ∨-semilattices, are distributive (N 5 and M 3 are isomorphic to path and tree). Nevertheless, neither N 5 nor M 3 are distributive. Now, the mapping of the concept lattice into its ideal lattice will produce a ∨semilattice, but this is not necessarily a minimal solution. For example, M 3 will be embedded in the Boolean lattice while M 3 \⊥ is already a distributive ∨-semilattice. Hence, the global approach that embeds a concept lattice into its ideal lattice is not efficient.

Alternatively, we can think of a local approach: instead of embedding the whole concept lattice into its ideal lattice, we do so for the sublattices corresponding to filters of minimal elements of J (L). The algorithm proposed in [START_REF] Gély | Steps towards achieving distributivity in formal concept analysis[END_REF] computes contexts of ↑ j for every minimal ∨-irreducible element j, and transforms these contexts so that they correspond to the context of a distributive lattice. Once these contexts are built, we merge them to build the whole lattice. However, this method Algorithm 1: Construction of context of a distributive ∨-semilattice.

Data: A context (J (L), M (L), I) of a lattice L Result: the context (J (L med ), M (L med ), I) of a distributive ∨-semilattice L med such that L can be order-embedded in L med foreach j ∈ J (L), minimal do (P j , ≤) ← / 0 repeat stability ← true; foreach j ∈ J (L), minimal do compute P j the poset of ∨-irreducible elements in ↑ j compute C j = (P j , P j , ≥) if P j modified since last iteration then stability ← false;

Merge all C j = (P j , P j , ≥) in a unique context Reduce this context until stability does not always output a minimal solution, i.e., there may exist L d a distributive ∨semilattice such that L can be embedded in L d , and

L d can be embedded in L d with |L| < |L d | < |L d | and (J (L), ≤) = (J (L d ), ≤) = (J (L d ), ≤)
. This result comes from the fact that each filter is processed independently. Nevertheless, it is possible that some elements are shared by several filters of minimal ∨-irreducible elements. This is illustrated in Fig. 5, and motivates the two following observations. First, it is possible that some elements added to a filter for achieving distributivity belong to other filters. These new elements may break a previously obtained distributivity in others filters. This is the case in Fig. 5.b with the two new elements r and g. At a first iteration of the loop of the algorithm, when the filters are merged, r and g are distinct elements. Neither the filter of 1 nor 2 are distributive. ↑ 1 (resp. ↑ 2) is not distributive because of r (resp. g). To overcome the problem, the algorithm loops while any filter is modified by the process. At worst, the algorithm computes the context corresponding to the ideal lattice of ∨-irreducible poset of L and the algorithm always terminates. Second, in some cases, a minimal solution cannot be reached when locally considering the filters. Such a solution is proposed if Fig. 5.d.

A Counter-example for the Existence of a Minimum

Distributive ∨-Semilattice

The local approach thus seems to be better than the global one. However, our algorithm does not always produce a minimal solution. The natural question is then whether, for a lattice L, there exists a minimum (i.e., minimal and unique) distributive ∨-semilattice L d such that L can be embedded into L d . We will now show through a counter-example that such minimum does not always exist. The proposed counter-example is given in Fig. 6: For the lattice shown in 6.a, either lattice in Figs. [START_REF] Birkhoff | Representations of lattices by sets[END_REF].b and 6.c are minimal distributive ∨-semilattices (since they differ by one element only) but it is obvious that lattices in Fig. 6.b and 6.c are not isomorphic. So, since a minimum solution does not exist, some choices remain to be done in order to use FCA algorithms for traditional application fields of median graphs, in particular for phylogeny.

Since phylogenetic parsimonious trees minimize the number of required evolutions to obtain species, lattice in Fig. 6.b may be prefered to lattice in Fig. 6.c In effect, in the first case, vertex b is obtained from a mutation at the root, in the latter, two mutations from the root are needed.

Discussion and Perspectives

We have seen that there is a lattice L for which there is not a unique minimum distributive ∨-semilattice L d such that L can be embedded in L d and with the same posets of ∨-irreducible elements ((J (L), ≤) = (J (L d ), ≤)).

So, even if we provide an algorithm that produces a minimal solution, the question of the meaning of this (not unique) solution should be addressed. A way to tackle it is to find an algorithm able to list all the minimal solutions. Alternatively, we could propose a measure of "interestingness" of these minimal solutions, so that an optimal solution could be reached based on such a measure. This remains a topic of current research. Also, this work was motivated by the study of the relations between distributive ∨-semilattices and median graphs. Not all distributive ∨-semilattices are median graphs. It remains to check the following condition: For every triple of elements x, y, z such that x ∧ y, x ∧ z and y ∧ z are defined, x ∧ y ∧ z is defined.

It is obvious that this condition is not satisfied for some distributive ∨-semilattices. A trivial example is the Boolean lattice (minus the bottom element) but in this particular case, the whole lattice is distributive, and so a median graph. Nevertheless, it remains open whether this is always the case.

Fig. 1 a

 1 Fig. 1 a Phylogenetic data of sequence variations for individual groups. b Median graph obtained from the data ([4]). c Concept lattice for phylogenetic data. d Concept lattice corresponding to the median graph. The new concept (046, k) corresponds to L4. To obtain this lattice, data must be modified replacing column g by k.

Fig. 2 a

 2 Fig. 2 a Standard context for lattice N 5 bThe context (J (N 5 ), J (N 5 ), ≥) of an ideal (and so, distributive) lattice. c N 5 , a non distributive lattice. d Ideal lattice for (J (N 5 ), ≤). e (J (L), ≤) poset for ideal lattice in d. Note that N 5 can be order-embedded in the lattice . Concepts (X,Y) are maximal rectangles of the contexts. For an element e of the lattice, the corresponding concept(X,Y ) is X = { j ∈ J (L) | j ≤ e} and Y = {m ∈ M (L) | m ≥ e}.For example, the element with label d is the concept ({1, 3}, {d}).

Fig. 5 a

 5 Fig. 5 a A lattice, with its two atom filters enlightened. b Result of the first step of the algorithm. c Result of the algorithm. d A minimal distributive ∨-semilattice (not reachable by the algorithm).

Fig. 6 a

 6 Fig.6a A lattice such that there two non isomorphic minimal distributive ∨-semilattices (when removing bottom element) shown in Figs.6b and 6c.


Olivier Nicole

Matthieu Lemerre

Xavier Rival

Lightweight Shape Analysis based on Physical Types

To understand and detect possible errors in programs manipulating memory, static analyses of various levels of precision have been introduced, yet it remains hard to capture both information about the byte-level layout and precise global structural invariants. Classical pointer analyses struggle with the latter, whereas advanced shape analyses incur a higher computational cost. In this paper, we propose a new memory analysis by abstract interpretation that summarizes the heap by means of a type invariant, using a novel kind of physical types, which express the byte-level layout of values in memory. In terms of precision and expressiveness, our abstraction aims at a middle point between typical pointer analyses and shape analyses, hence the lightweight shape analysis name. We pair this summarizing abstraction with a retained and staged points-to predicates abstraction which refines information about the memory regions that are in use, hereby allowing strong updates without introducing disjunctions. We show that this combination of abstractions suffices to verify spatial memory safety and non-trivial structural invariants in the presence of low-level constructs such as pointer arithmetic and dynamic memory allocation, on both C and binary code.

Introduction

Memory errors have long been a very important concern for programmers, due to the potential safety and security issues that they raise. In particular, programs that perform low-level pointer and memory operations are particularly tedious to reason about in languages like C/C++ or assembly. For instance, such patterns are very common in system software, which makes its correct implementation challenging.

Many verification techniques aimed at verifying the correctness of memory manipulating programs have been developed. In particular, several families of automatic and conservative static analysis focus on such errors. Pointer analyses [START_REF] Smaragdakis | Pointer Analysis[END_REF] based on abstractions of aliasing relations [START_REF] Andersen | Program Analysis and Specialization for the C Programming Language[END_REF] or access paths [START_REF] Deutsch | Interprocedural may-alias analysis for pointers: Beyond k -limiting[END_REF] infer basic conservative relations between pointer values and can tackle basic memory errors. However, they are of limited expressiveness, which implies they cannot establish safety when doing so requires reasoning over structural invariance. On the other hand, shape analyses based on three valued logics like TVLA [START_REF] Sagiv | Solving shape-analysis problems in languages with destructive updating[END_REF] or on separation logics [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF] such as Infer [START_REF] Distefano | A local shape analysis based on separation logic[END_REF] or Xisa [START_REF] Chang | Shape analysis with structural invariant checkers[END_REF] attempt to establish precise structural invariants such as the existence of some list or tree data-structures. Such analyses can cope with the verification of memory safety in presence of sophisticated structures, yet they are typically less scalable than basic pointer analyses and also less resilient to a local precision loss in the sense that losing precision over a fragment of the memory often entails no information can be recovered about that region. Another limitation is that such analyses are difficult to apply to low-level code, like low-level C or binary code, even though some abstractions have been adapted to deal with some forms of pointer arithmetics [START_REF] Kreiker | Shape analysis of low-level C with overlapping structures[END_REF][START_REF] Vincent Laviron | Separating shape graphs[END_REF]. Few analyses have been aimed for a precision level that sits in between those two large classes, like graph heap models [START_REF] Marron | Efficient context-sensitive shape analysis with graph based heap models[END_REF], but these do not cope with a low-level memory description.

In this paper, we are interested in memory abstractions expressive enough to verify type safety, i.e. the preservation of structural invariants expressed by types, in non-trivial linked data-structure manipulations in both high-and low-level code (such as assembly or low-level C). This type safety entails spatial memory safety, namely that each memory access is done on an address that was previously allocated (and thus that null or out-of-bound pointer dereferences are impossible). We also seek for a high level of automation (i.e., by avoiding the requirement of complex handwritten program annotations) and of efficiency.

To achieve this, we propose a novel memory abstraction that is inspired by the classical notion of types, but applies to the physical representation of datastructures (Section 4). Our abstract domain (Section 5) represents the heap in a flow-insensitive way, which is less expressive than shape analyses, but allows a simpler representation of abstract states and simpler, more efficient analysis operations (Section 6). Combined with two independent extensions of the domain to track "retained" and "staged" points-to predicates (Section 7), we show that the combination naturally deals with both C and binary code manipulating dynamic data structures (Section 8).

Overview example

We demonstrate the main features of our analysis on a low-level implementation of a classical union-find structure inspired by Kennedy [START_REF] Kennedy | Compiling with Continuations, Continued[END_REF]. The representation combines the union-find structure based on chains of pointers to class representatives in reverse tree shapes with doubly linked-lists for efficient iteration over the elements of an equivalence class. The whole code is presented in Figure 1. It is written in C for the sake of readability, but we are interested in analysis techniques that would also cope with the corresponding assembly code just as well. Structures uf and dll respectively represent the union find and doubly linked list structures. Following a pattern common in low-level and system code [START_REF] Brown | Linux kernel design patterns -part 2[END_REF], the structure node comprises both sub-structures uf and dll. Function uf_find returns the representative of the class of an element and halves [START_REF] Tarjan | Worst-Case Analysis of Set Union Algorithms[END_REF] the paths to the root to speed up subsequent calls. Functions dll_union and uf_union respectively merge doubly linked-lists and union-finds. Last, merge merges two node structures and make creates a new node.

Figure 2(a) displays an example concrete state, with a class made of three nodes (and where the node at address 0x60 is the representative). Such states contain a very high degree of sharing due to the interleaved union-find and doubly-linked list structures. Moreover, these structures are unbounded. Therefore, pointer analysis techniques would require tricky and ad hoc adaptations regarding sensitivity to be precise, so as to divide heaps in regions of pointers with similar properties; these techniques are too imprecise to verify type or memory safety for C or assembly. In the same time, shared data structures such as union-find are notoriously hard to handle for shape analysis abstractions and we are not aware of any successful shape analysis based verification for a structure similar to that of Figure 1.

Our key contribution is to propose an abstract interpretation framework based on a semantic interpretation of physical types, that simultaneously verifies the preservation of type-based structural invariants, and uses these invariants to perform and improve the precision of the analysis. This contrasts with the usual method where syntactic type checking and type-based pointer analyses are separate analyses, each insufficiently precise to verify type safety for low-level languages like C or binary. The type-based structural invariant implies dividing the heap into partitions, which are attached flow-insensitive information, allowing for efficient static analysis operations. To further improve precision, our analysis is strengthened by flow-sensitive points-to predicates, whose effect is comparable to materialization in shape analysis, but the memory summary is provided by the type-based structural invariants. In this section, we informally present the basic predicates of our analysis. ∀ν, ∀(σ, h, L, Γ ) well-typed state, ∀v value :

v ∈ node.(0) * =0 L,ν =⇒ v + 4 ∈ node.(4) * =0 L,ν (1) node.(4) * =0 L,ν ⊆ dll.(0) * =0 L,ν (2) v ∈ dll.(0) * =0 L,ν =⇒ h[v..v + 4] ∈ dll.(0) * =0 L,ν (3) uf.(0) * =0 L,ν ∩ dll.(0) * =0 L,ν = ∅ (4)
(d) Some structural invariants entailed by M Fig. 2. Concrete and abstract states based on physical types.

Let us examine the types and structural invariants on our example code. The types are given in Figure 2(b). They must be provided by the analysis user, and possibly derived in part from the C types, although they express stronger invariants. Note that our analysis is independent from C typing rules; in particular C is not type-safe, while we can verify type-safety on both C and compiled programs. Intuitively, dll.(0) * =0 denotes a non-null pointer to the base address of another, well-formed dll instance. In the case of uf, the parent pointer may be null, hence the subscript * =0 is absent. Finally, type node_kind is a type refined with a predicate restraining its possible values: it corresponds to 4-byte bit vectors whose unsigned value is lesser than 5. Thus, these types can be more precise than C types, although C types can be translated to our type language. But they are less precise than shape invariants, as they cannot represent the relation between different elements of a same type: our dll structure could e.g. represent a binary tree with leaves pointing to the root.

These types entail structural invariants, some of which are presented in Fig. 2(d), that a well-typed state must fulfill. These invariants relate types, interpreted as sets of values: t L,ν represents the set of values for type t. Equation (1) relates adjacent addresses; Equation (2) describes a subtyping relationship; Equation (3) relates the type of an address with its contents; and Equation (4) describes a partitioning of the heap in distinct regions. Note that the correctness of these invariants implies that the memory layout of the heap must be compatible with these equations (as is Figure 2(a)), which is why the interpretation of types depends on the heap layout L.

We now turn our attention to our abstract domain. The abstract state shown in Figure 2(c) represents the initial state when execution of the merge function begins (this function requires that it is given non-null pointers to node as arguments). Each variable is associated to both an abstract type describing possible values stored in the variable, and to a symbolic variable used to attach numerical constraints to this value. For instance, variable x is bound to physical type node.(0) * =0 , meaning that its value belongs to node.(0) * =0 L,ν ; furthermore it is bound to symbolic variable α which is constrained to be not null. Combined with structural invariants of Equations ( 1 &x->dll) points to a valid address, that can be safely casted as type dll.(0) * =0 , and that reading from this address will return a value that also has type dll.(0) * =0 . Eventually, using these invariants we can verify that all memory accesses performed by the call to dll_union are valid, but also that each statement preserves these structural invariants. However, this approach does not suffice when considering more complex functions, like uf_find. First, we remark that the function may run correctly only when argument x is non-null due to the dereference at line 15, although the uf physical type does not require pointers to parent be non-null. Therefore, the verification of this function will use semantic information coming from the numerical abstract domain. Next, we observe that to prove the validity of the access to parent->parent at line 17, the analysis needs to establish that parent is non-null, by observing that it is equal to x->parent, which is non-null due to the condition at line 15. Such reasoning cannot be performed solely using a combination of types and numerical predicates, because the type-based invariants cannot attach different information to different heap objects of the same type. Therefore, we augment variable-type predicates with additional boxes, also defined with a symbolic variable and a physical type, but that corresponds to some selected heap addresses. Only boxes that are reachable from a variable finite chain of points-to predicates may be retained this way. Figure 3 shows the abstract state at line 19 that enables to proves the parent->parent access. In the following, we call such predicates retained points-to predicates. Such predicates are obtained by retaining information about recent memory writes, loads, or condition tests and need to be abstracted away as soon as they cannot be proved to be preserved. Indeed, when the analysis encounters a memory write, it drops all such boxes for which the absence of aliasing cannot be established with the current information; some aliasing information (e.g. Equation( 4)) comes from the partitioning of the heap. This process will be referred to as blurring as it carries some similarity with the blurring encountered in some shape analyses. Note that the retained points-to predicates offer a very lightweight way to keep some memory cells represented precisely without resorting to unfolding/focusing which is generally more costly (but also more powerful in the logical point of view), as retaining a heap address or blurring it does not require modifying the summarized heap representation. Physical types coupled with retained points-to predicates allow to verify memory safety and typing preservation for the four functions dll_union, uf_find, uf_union and merge.

Finally, we consider function make. For the sake of simplicity, we assume that malloc always returns a non-null pointer. We note that variable n does not point to a valid node object until the very end of the function, thus attempting to prove it satisfies physical type node.(0) * =0 before that point will fail. In general, some code patterns like memory allocation or byte-per-byte copy temporarily do not preserve the structural invariants described by our types. To alleviate this, we augment our stmt ::= x := expr

(x ∈ X) | * expr := expr ( ∈ N) | x := malloct(expr ) (x ∈ X, t ∈ T) | skip | stmt; stmt | if expr then stmt else stmt end | while expr do stmt done expr ::= c (c ∈ V) | x (x ∈ X) | expr expr ( ∈ {+, -, ×, /, ≤, <, =, =, &, |, • • • }) | * expr ( ∈ N) Fig. 4. Language Whilemem
abstraction with a notion of staged points-to predicates that represent precisely the effect of sequences of store instructions such as the body of make, allowing to delay their abstraction into types at a later point.

The abstractions sketched so far may also be applied to binary code provided type information can be recovered from, e.g., debugging information. In the rest of the paper, we describe more precisely physical types in Section 4 whereas retained points-to predicates and buffered write predicates are formalized in Section 7.

Language and semantics

Although our analysis was implemented both for C and binary code, we adopt a simple imperative language for the sake of presentation. As the grammar in Figure 4 shows, While mem features basic assignments, usual arithmetic expressions, memory allocation, and standard control flow commands. Memory locations include a finite set of variables X and addresses A that can be computed using usual pointer arithmetic operations. The analysis is parameterized by the choice of an application binary interface (or ABI) that fixes endianness, basic types sizes and alignments. In the following, we assume a little-endian ABI is fixed and let W denote the size of words. Memory access patterns of C can be translated into While mem ; for instance, assuming a pointer size of 4 bytes, x->prev turns into * 4 (x + 4). We leave out functions, that our analysis handles in a context sensitive manner. We assume that instances of malloc are marked with a type t, though we define the set of types in Section 4.

The values manipulated by While mem are bit vectors, i.e., non-negative integers as fixed-size sequences of bytes, so the set of values V is defined by:

V = {( , v) | ∈ N, v ∈ [0, 2 8 -1]}
If n > 0, we let V n denote the set of bit vectors of length n. We extend the binary operator notation to bit vectors of the same byte length, i.e., ( , v 1 ) ( , v 2 ) means ( , v 1 v 2 ). The concatenation of any two bit vectors x and y is denoted x :: y and is defined by

( 1 , v 1 ) :: ( 2 , v 2 ) = (l 1 + l 2 , v 1 + 2 8 1 v 2 ). The set of addresses A is a subset of V W .
As usual, we let stores map variables to their contents (thus, Σ = X → V) and heaps be partial functions from addresses to their contents We denote by σ[x ← v] the store σ with x now mapped to v, and by h[a..a + ← v] the heap h with values at addresses a (included) to a + (excluded) replaced with the bytes from v. Finally, dropping a range of mappings from a heap is noted h

(H = A V 1 ). Moreover, the set of states is S = Σ × H. Given a heap h ∈ H, a ∈ A,
[a..a + ← ⊥].
The semantics of the language is given by a transition relation → ∈ (stmt × S) × (stmt × S) whose definition is standard (and given in the appendices of the paper [START_REF] Nicole | Lightweight shape analysis based on physical types (full version)[END_REF]). We let Ω denote the state after a run-time error (such as division by zero or null pointer dereference), and E e : S → V × {Ω} denote expression evaluation. Last, to express the soundness of the analysis, we define a collecting semantics as follows. Given a program p, the semantics p : P(S) → P(S) maps a set of input states into a set of output states and is such that (σ , h ) ∈ p (S) if and only if there exists (σ, h) ∈ S, and a sequence of transitions (p, (σ, h))

→ (p 1 , (σ 1 , h 1 )) → . . . → (p n , (σ n , h n )) → (skip, (σ , h )).

Physical representation types

In this section, we formalize physical representation types (or, for short, physical types) and a typed semantics, that serve as a basis for our analysis. The core idea here is to define a notion of well-typed state which will be used as the base invariant representing the summarized regions of memory.

Definition. As shown in Section 2, physical representation types are aimed at describing the memory layout of memory regions using predicates inspired by the standard types, but extended with additional properties. Therefore, the set of physical types comprise standard types for the representation of not only base values, but also structures and arrays. Moreover, they attach to each pointer variable not only the type of the structure that is pointed but also the offset in the block and information about the possible nullness of the pointer.

In order to describe additional constraints such as array indexes, physical types may be refined [START_REF] Freeman | Refinement types for ML[END_REF][START_REF] Maxim Rondon | Low-level liquid types[END_REF] with numerical constraints, that may bind not only the corresponding value, but also existentially quantified symbolic variables (representing e.g. the unknown size of an array). To this effect, we let V = {α 0 , α 1 , . . .} denote a countable set of symbolic variables. Moreover, the concretization of types needs to reason over the actual value of symbolic variables. Such a realization of symbolic variables to values is called a valuation and is usually noted

ν : V → V.
Finally, the analysis is parameterized by a fixed set of type names N , and a mapping M ∈ N → T binding type names to types. Type names have two uses: first they break cycles in the definition of recursive types; second they distinguish types otherwise structurally equal (i.e. it allows the type system to be nominal), and in particular pointers to two structurally equal types with different names will not alias. For instance, in Section 2, we considered recursive types dll and uf, and Figure 2(b) gives an example of a mapping M. Definition 1 (Physical representation types). The set T of physical representation types is defined by the grammar in Figure 5. Note that, a type refined by a predicate makes use of a local variable x that denotes the value of this type and is meant to be constrained in the matching pred (x) predicate, which is why grammar entries predexpr (x) and pred (x) take a variable as parameter. An address type t.(k) ∈ T A represents the k-th byte in a value of type t. Finally, the pointer types t a * and t a * =0 respectively account for the possibly null and definitely non-null cases. Thus, t.(k) * =0 should be interpreted as the address of the k-th byte of a value of type t and t.(k) * represents the same set of values, with the addition of the value 0.

predexpr (x) ::= x (constrained type variable) | c (constant c ∈ V) | α (symbolic variable α ∈ V ) | predexpr (x) predexpr (x) (binary op., ∈ {+, -, ×, • • • }) pred (x) ::= predexpr (x) predexpr (x)(comparison, ∈ {≤, <, =, =} | ¬pred (x) | pred (x) ∧ pred (x
Example 1 (Doubly linked-lists and structures). Based on Definition 1, the fact that a dll object boils down to a pair of non-null dll pointers can be expressed by the type dll.(0) * =0 × dll.(0) * =0 . We also remark that padding bytes added in structures to preserve field alignments can be added using . . . × word k .

Before we can formally define the denotation of types, we need to introduce a few notions. As usual in languages like C, we can compute the size of the representation of a type. Since arrays may not be of a statically known size, the size may depend on the actual value of symbolic variables, hence it needs to be parameterized by a valuation ν. Then, size is computed by the function size ν : T → N defined by:

size ν (word n ) = n size ν (t a * ) = size ν (t a * =0 ) = W size ν ({x : t | p(x)}) = size ν (t) size ν (t 1 × t 2 ) = size ν (t 1 ) + size ν (t 2 ) size ν (t[s]) = s • size ν (t) if s ∈ N ν(s) • size ν (t) if s ∈ V
Memory labeling. Physical types are aimed at describing not only variables like standard types do, but also memory locations. To formalize this, we introduce labelings as mappings from addresses to physical types.

Definition 2 (Labeling).

A labeling is a function L : A → T A such that each tagging of a region with a type is whole and contiguous, i.e., for all types t ∈ T, for all addresses a ∈ A, if we let n = size ν (t), and if there exists k ∈ [0, n -1] such that L(a + k) = t.(k), then:

L(a) = t.(0) ∧ L(a + 1) = t.(1) ∧ . . . ∧ L(a + n -1) = t.(n -1)
We extend this notion by letting labelings return a type: if L(a) = t, then it should satisfy the above property. Moreover, we let L denote the set of labelings. Intuitively, L(a) = t means both that a points to a value of type t, and that a has type t.(0) * =0 .

Example 2 (Labeling). We consider the state of Figure 2(a). In this case, the relations below form a valid labeling of the memory:

L : 0x20 → node.(0) 0x21 → node.(1) . . . 0x2c → node.(15) 0x60 → node.(0) 0x61 → node.(1) . . . 0x6c → node.(15) 0x80 → node.(0) 0x81 → node.(1) . . . 0x8c → node.( 15
)
Subtyping relation. In Example 2, the labeling L conveys that the type of address 0x24 is node.( 4). But we could also view this offset as the base address of a doublylinked list and give it type dll.(0), since node contains a dll at offset 4. However, the former is more precise: all memory cells that contain a node.( 4) contain a dll.(0), but the converse is not true. This remark motivates the definition of a physical form of subtyping relation. Intuitively, the above remark should be noted node.(4) dll.(0). More generally, t.(n) u.(m) means that t "contains" a u somewhere in its structure.

Definition 3 (Subtyping between address types). The relation ∈ T A ×T

A is defined inductively according to the rules below:

t.(k) t.(k) t = M(n) 0 ≤ k < size ν (t) n.(k) t.(k) t.(k) u.(l) u.(l) v.(m) t.(k) v.(m) 0 ≤ k < size ν (t 1 ) (t 1 × t 2 ).(k) t 1 .(k) 0 ≤ k < size ν (t 2 ) (t 1 × t 2 ).(size ν (t 1 ) + k) t 2 .(k) 0 ≤ q < s 0 ≤ k < size ν (t) t[s].(q • size ν (t) + k) t.(k)
Interpretation of types. We now give the meaning of types in terms of an interpretation function that maps each type into a set of values. Unlike classical notions of types, the interpretation of a physical type depends on the data of a labeling L to resolve field pointers to other structures and on a valuation ν : V → V in order to check that side predicates are satisfied. In the following, we let eval ν : pred × V → B be the function that maps a predicate to its boolean value for valuation ν (the definition of eval ν is classical thus omitted).

Definition 4 (Interpretation of types). Given labeling L and valuation ν the interpretation function • L,ν : T → P(N) is defined by:

word n L,ν = V n t a * =0 L,ν = {a ∈ A | L(a) t a } t 1 × t 2 L,ν = {v 1 :: v 2 | ∀i, v i ∈ t i L,ν } t a * L,ν = t a * =0 L,ν ∪ {0} {x : t | p(x)} L,ν = {v ∈ t L,ν | eval ν (p, v) = true} t[s] L,ν = {v 0 :: v 1 :: • • • :: v s-1 | v 0 , . . . , v s-1 ∈ t L,ν }
As shown below, the interpretation is monotone with respect to subtyping, which is consistent with Liskov's substitution principle [START_REF] Liskov | A behavioral notion of subtyping[END_REF], which means that all properties of addresses of type τ also hold for addresses of type υ, where υ τ : In the analysis, the notion of subtyping and its properties with respect to interpretation have two applications: first, they allow verifying memory safety and the preservation of structural invariants by checking subtyping is preserved by memory updates; second, they also allow to over-approximate aliasing relations as we demonstrate now.

Definition 5 (Set of addresses covered by a type). Let L ∈ L, ν : V → V, and t be a type. Then, the set of addresses covered by type t is:

addr L,ν (t) ::= {a ∈ A | ∃i, 0 ≤ i < size ν (t) ∧ L(a) t.(i)}.
Definition 6 (Type containment). Let ν : V → V be a valuation and t, u ∈ T be types. We say that "t contains u" if and only if:

∃i ∈ [0, size ν (t)) , ∀k ∈ [0, size ν (u)) , t.(i + k) u.(k).
Theorem 1 (Physical types and aliasing). Let t, u ∈ T. Then, either t and u cover disjoint regions, or one contains the other, i.e., if addr L,ν (t) ∩ addr L,ν (u) = ∅, then t contains u or u contains t.

Proof. This comes from the fact that is a tree relation.

This result entails that physical types can be used to compute must-not alias information. As an example, in Figure 2(a), if we consider types uf and dll, neither of them contains the other, thus their addresses are disjoint.

States in a typing environment. In the following paragraphs, we define a typed semantics for While mem . This semantics is conservative in the sense that it rejects some programs and executions that could be defined in the semantics of Section 3. In this second semantics, states are extended with typing information. Its goal is to serve as a step towards the verification of preservation of physical types. More precisely, a state should enclose not only a store and a heap, but also a labeling and a map from variables to types. Furthermore, such a state is well typed if the heap is consistent with the labeling and the variable values are consistent with their types.

x ∈ X, σ(x) ∈ Γ (x) L,ν . c ∈ Vn (σ, h, L, Γ ) c : wordn c ∈ A (σ, h, L, Γ ) c : L(c) * =0 (σ, h, L, Γ ) x : Γ (x) (σ, h, L, Γ ) e : t.(i) * =0 t.(i) u.(j) (σ, h, L, Γ ) e : u.(j) * =0 (σ, h, L, Γ ) e : t.(i) * t.(i) u.(j) (σ, h, L, Γ ) e : u.(j) * (σ, h, L, Γ ) e : t.(0) * =0 sizeν (t) = (σ, h, L, Γ ) * e : t (σ, h, L, Γ ) e1 : wordn s e2 : wordn (σ, h, L, Γ ) e1 e2 : wordn (σ, h, L, Γ ) e1 : t.(o) * =0 (σ, h, L, Γ ) e2 : wordW E e2 (σ, h) = v2 0 ≤ o + v2 < sizeν (t) (σ, h, L, Γ ) e1 + e2 : t.((o + v2)) * =0 (σ, h, L, Γ ) e : t evalν (p, E e (σ, h)) holds (σ, h, L, Γ ) e : {x : t | p(x)} (σ, h, L, Γ ) e : t.(0) * E e (σ, h) = 0 (σ, h, L, Γ ) e : t.(0) * =0
Fig. 6. Typing rules for Whilemem expressions.

Typed semantics of expressions. Typing of expressions aims at proving that the evaluation of an expression will either return a value consistent with the type or a runtime error. Unlike classical type systems, we do not use physical types to prevent runtime errors directly; instead, we let the analysis discharge the verification of memory safety as a second step, after types have been computed. Given a store σ, a heap h, a labeling L, a typing of variables Γ , an expression e, and a type t, we write (σ, h, L, Γ ) e : t when expression e can be given type t in the typing state (σ, h, L, Γ ). The typing of expressions are given in Figure 6. Intuitively, the type of addresses (resp., variables) is resolved by L (resp., Γ ). Rules for base values and binary operators are classical. Memory reads and pointer arithmetics are typed using corresponding offset calculation over physical types. Subtyping allows replacing a type to a container type at pointer dereference points. Finally, types of expressions can be refined by the values these expressions evaluate to. This typing is sound in the following sense:

Theorem 2 (Soundness of typing of expressions). Let an expression e, a valuation ν ∈ V → V, a typing state (σ, h, L, Γ ) and a type t ∈ T. Then, if (σ, h, L, Γ ) is well typed under ν, if (σ, h, L, Γ ) e : t, and if E e (σ, h) = v, then either v = Ω or v ∈ t L,ν .

Note that an expression may be given several types in a same state due not only to subtyping but also to pointer arithmetics. For instance, if 8 has type t.(0) * , and 16 has type u.(0) * , then 8 + 16 is at the same time of type t.( 16) * and u.(8) * .

Typed semantics of statements. The typed semantics of instructions is defined by a relation → t ∈ (stmt × S t ) × (stmt × S t ). It is mostly similar to the untyped semantics, but rules involving memory writes differ. Figure 7 displays the rules regarding memory writes. The rule for assignment not only updates the store but also the typing environment Γ . We note that this semantics is non-deterministic since the type of an expression is not unique in general. This semantics enjoys the type preservation property:

Theorem 3 (Preservation of typing of states). Let a valuation ν : V → V, and a typing state (σ 0 , h 0 , L 0 , Γ 0 ), well typed under ν, such that Therefore, as we consider executions starting in a well-typed state only, Theorem 3 entails that well-typedness is an invariant. This semantics is not computable in general.

(σ 0 , h 0 , L 0 , Γ 0 ) → t (σ 1 , h 1 , L 1 , Γ 1 ). Then, (σ 1 , h 1 , L 1 , Γ 1 ) is well typed under ν. (σ, h, L, Γ ) e : t E e (σ, h) = v x := e, (σ, h, L, Γ ) →t skip, (σ[x ← v], h, L, Γ [x ← t]) (σ, h, L, Γ ) e1 : t.(0) * =0 (σ, h, L, Γ ) e2 : t sizeν (t) = E e1 (σ, h) = (W, a) E e2 (σ, h) = ( , v) * e1 := e2, (σ, h, L, Γ ) →t skip, (σ, h[a..a + ← v], L, Γ )
Last, we note that the typed semantics is more restrictive than the untyped one:

Theorem 4 (Semantic comparison). If the typing states (σ 0 , h 0 , L 0 , Γ 0 ) and

(σ 1 , h 1 , L 1 , Γ 1 ) are such that (p 0 , (σ 0 , h 0 , L 0 , Γ 0 )) → t (p 1 , (σ 1 , h 1 , L 1 , Γ 1 )), then (p 0 , (σ 0 , h 0 )) → (p 1 , (σ 1 , h 1 )).
Intuitively, the typed semantics is more restrictive than the untyped semantics in two ways: first, it considers only well-typed initial states only; second, it considers ill-typed memory writes as blocking, even though such a write may be part of a program fragment that overall preserves invariants. Finally, note that malloc calls cannot be readily incorporated in the typed semantics; this is solved in Section 7.

Type-based shape domain

We now set up the type-based shape abstract domain which serves as a basis for our analysis by defining its abstract elements and concretization function. This abstract domain combines type information with numerical constraints. Types constrain the regions pointed to by variables and may contain symbolic variables denoting numerical values. To cope with numerical constraints, our abstract domain is parameterized by a numerical domain such as that of intervals [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] or any other abstract domain. Thus, we assume such an abstract domain D num is fixed, together with a concretization function γ N : D num → (V → V).

Abstract types. First, an abstract type defines a set of types where all symbolic variables are mapped into a numerical value. Due to the dependency on the association of symbolic variables to numerical values, its concretization returns pairs including a valuation ν : V → V. It boils down to either a physical type or either of the ⊥, constant elements. Definition 8 (Abstract types). The set of abstract types T is defined by the grammar below together with its concretization γ T :

T → P(T × (V → V)): T t ::= ⊥ | t.(α) * | t.(α) * =0 | γ T : ⊥ -→ ∅ -→ T × (V → V) t.(α) * -→ {(t.(ν(α)) * , ν) | 0 ≤ ν(α) < size ν (t)} t.(α) * =0 -→ {(t.(ν(α)) * =0 , ν) | 0 < ν(α) < size ν (t)}
Example 4 (Array type). As an example, the abstract type and numerical constraints below abstract the information that one would attach to a pointer to some array of 10 integers:

abstract type int [START_REF] Deutsch | Interprocedural may-alias analysis for pointers: Beyond k -limiting[END_REF].(α) states that we are looking at an address somewhere into such an array; numerical constraints α ∈ [0, 39] ∧ ∃k ∈ N, α = 4k (expressible in a reduced product of intervals and congruences) refines the above abstract type by filtering out misaligned pointers. Note that an address into an array of statically unknown length would write down int[α ].(α), with matching numerical constraints.

Type-based shape abstraction. At this point, we can formalize the type based shape domain as follows, by letting each variable be abstracted by an abstract type. In order to also express constraints over the contents of variables, this abstraction also needs to attach to each variable a symbolic variable denoting its value.

Definition 9 (Type-based shape domain). We let the type-based shape domain H denote the set of pairs (σ , Γ ) pairs called abstract stores, where:

σ : X → V is a mapping from variables to symbolic variables, and Γ ∈ X → T is a mapping from variables to abstract types. Moreover, the concretization for H is the function γ H : H → P(S t × (V → V)) defined by:

γ H Γ = (σ, h, L, Γ ), ν (σ, h, L, Γ ) is well typed under ν and ∀x ∈ X, Γ (x), ν ∈ γ T (Γ (x))
and ∀x ∈ X, σ(x) = ν(σ (x)) Definition 9 does not provide representable abstract states quite yet. Indeed, we still need to reason over the possible numerical values denoted by symbolic variables.

The numerical abstract domain allows completing this last step.

Definition 10 (Combined shape abstraction). The combined shape-numeric abstract domain S and its concretization γ S : S → P(S t × (V → V)) are defined as follows:

S ::= H × D num γ S (h , ν ) = {(s, ν) ∈ γ H (h ) | ν ∈ γ N (ν )}
Figure 2(c) provides an example of an abstract state in this combined abstraction.

Static analysis

Our static analysis is a standard, forward, abstract interpretation-based static analysis [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF]. We focus on important operations,like verifying that stores preserve type invariants, or the lattice operations. Both of these operations rely on a procedure called abstract type checking.

Structure of the interpreter. The analysis of While mem expressions and statements is respectively performed by the two functions E • : expr × S → (V × T ) × D num and • : stmt × S → S . The evaluation of expressions manipulates abstract values V t def = V × T , which are the counterpart of concrete values in the concrete semantics. An abstract value α t is just a pair (α, t ) ∈ V t with a symbolic variable α and an abstract type t respectively describing all the possible values and some possible types for an expression. The evaluation of symbolic variables is standard [START_REF] Bor-Yuh | Semantics, Abstract Interpretation, and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday[END_REF] (each node in the expression tree creates a fresh symbolic variable and updates the numerical domain accordingly), and the computation of abstract types follows closely the concrete typing rules given in Figure 6.

Abstract type checking. Abstract type checking verifies that, given the numerical constraints of ν , casting an abstract value α t into type u is safe (this is written as α : t ν u ). In most type checks (that we call upcasts), this is done by checking that t ν u , where is an ordering between abstract types which derives from the subtyping relation ( ) between concrete address types: Some other type checks, like verifying that it is safe to transform a t * pointer to a t * =0 pointer, or checking that the predicate of a refinement type holds, are downcast operations: to verify the safety of the cast, we examine not only the types, but also the numerical properties of the value being type checked: Example 6. (Downcasting to a * =0 pointer) In Figure 1, the merge function gives &x->dll, whose type is node.(α) * with α = 4, as an argument to dll union, which eventually gets written into y->prev, a memory location that may contain values in the abstract type dll.(β) * =0 with β = 0 : this requires to perform a type check. Casting to dll.(β) * can be done using the abstract subtyping relation node.(α) * ν dll.(β) * , but to cast to dll.(β) * =0 , we must additionally check that the value x->dll (i.e. &x + offset 4) cannot be 0; this makes use of the fact that pointer arithmetics inside a valid object cannot wrap around.

Theorem 5 (Soundness of abstract subtyping). Let ν ∈ D num , t , u ∈ T , t.(i) and u.(j) ∈ T A . If t ν u , then ∀ν ∈ γ N (ν ), (t.(i), ν) * ∈ γ T (t ) ∧ (u.(j), ν) * ∈ γ T (u ) =⇒ t.(i) u.(j).
The soundness of the abstract type checking operation and its proof are established using the interpretation of the types: Theorem 6 (Soundness of abstract type checking). Let (h , ν ) ∈ S . Let α ∈ V be a symbolic variable and t , u be two abstract types. If α : t ν u then

∀((σ, h, L, Γ ), ν) ∈ γ S (h , ν ), ν(α) ∈ t L,ν =⇒ ν(α) ∈ u L,ν .
Interpretation of base statements. As shown in Example 6, the analysis must ensure that all memory updates preserve the typing of states (Theorem 3), and abstract type checking is a central operation for doing this. The interpretation of memory updates is done as follows: * e 1 := e 2 (h , ν

) def = (h , ν 2 ) if α : t ν 2 u
where u is a non-null pointer type and (α, t , ν 1 ) = E e 1 (h , ν ) and (β, w , ν 2 ) = E e 2 (h , ν 1 ) and w is the type of the values pointed by (α, u ) * e 1 := e 2 (h , ν

) def = otherwise
Note that memory updates do not modify the representation of the abstract heap, and is thus a fast operation. The evaluation of assignments is also fast, since it only needs to evaluate an expression and to record the abstract value in the abstract store:

x := e ((σ , Γ ), ν ) def = (σ [x ← α], Γ [x ← t ], ν 1 )
where (α, t , ν 1 ) = E e ((σ , Γ ), ν )

Lattice operations. The analysis of condition and loop commands is based on approximations for concrete unions and on conservative inclusion checks Φ,S to test whether a post-fixpoint is reached [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF]. The latter relies on abstract type checking. This operation consists in type-checking every While mem variable, in addition to verifying the inclusion of the numerical constraints:

((σ 1 , Γ 1 ), ν 1 ) Φ,S ((σ 2 , Γ 2 ), ν 2 ) def = ν 1 Φ,D num ν 2 and ∀x ∈ X : (σ 1 (x) : Γ 1 (x) ν 1 Γ 2 (x))
where Φ : V → V is a renaming function that handles the fact that each abstract state refers to different variables [START_REF] Bor-Yuh | Semantics, Abstract Interpretation, and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday[END_REF]) (here it can be defined as ∀x ∈ X : Φ(σ 1 (x)) = σ 2 (x)).

Theorem 7 (Soundness of inclusion). Let s 1 , s 2 ∈ S . Then:

s 1 Φ,S s 2 =⇒ ∀(s, ν) ∈ γ S (s 1 ), (s, ν • Φ) ∈ γ S (s 2 )
The join operation can be deduced from the definition of Φ,S . These lattice operations are necessary to define the interpretation of while and if statements (which is standard). The interpretation of other statements is also standard.

Theorem 8 (Soundness of the abstract semantics). Let s ∈ S be an abstract state and c ∈ stmt be a statement. Then, γ S ( c (s )) ⊇ c (γ S (s )).

Retained and staged points-to predicates

The type-based shape abstraction suffers from two important limitations. First, the heap is represented only in a summarized form by the type constraints, and there is no way to retain additional information about the contents of the heap. Second, all stores to memory must preserve the type invariants-situations where the type invariants are temporarily violated are not handled. This happens when data is allocated but not yet initialized (as in function make in Figure 1), when updating a value with an invariant that spans multiple words, and in other situations. We solve both problems by tracking some points-to predicates and attaching specific properties to them. The meaning of a points-to predicate α t → β u is, that for all possible valuations ν, the value (of size ) stored in the heap at address ν(α) is ν(β) and that α satisfies the abstract type t and β the abstract type u . Points-to predicates are represented using a simple map p mapping a symbolic variable to another variable and size, and is concretized by considering all the possible values for each symbolic variable. In the following, we define and track the so-called retained and staged points-to predicates. Their combination is formally defined in Figure 8 (where each points-to predicate α t → β u is represented by bindings α t → ( , β u ) of a function p ∈ P ).

P def = V t N × V t U def = S × P × P γP : P → P H × (V → V) γP (p ) = {(h, ν) |∀(αt, βt) ∈ V t , ∀ ∈ N : p (αt) = ( , βt) =⇒ h[ν(α)..ν(α) + ] = ν(β)} γU : U → P S × (V → V) γU (s , r , p ) = { (σ, h h), ν | ∃Γ, L, h, h : (σ, Γ, h, L), ν ∈ γS(s ) and (h, ν) ∈ γP (r ) and (h , ν) ∈ γP (p ) } where h h : dom(h ) ∪ dom(h) → V is defined as (h h)(a) def = h (a) if a ∈ dom(h ) (h h)(a) def = h(a) otherwise
Retained points-to predicates. The type-based shape domain remembers flowsensitive information only about the store, as the heap is represented only using the type invariants. We use retained points-to predicates α t → β u to store flow-sensitive information about the heap: they provide symbolic variables, like β, to represent values stored in the heap, so that they can be attached numerical and type information. In practice, retained points-to predicates achieve an effect comparable to materialization in shape analyses 4 . The concretization of these predicates is done by standard intersection.

Example 7 (Retained points-to predicate). Consider the abstract state (Figure 3) at line 19 of Figure 1. The binding from (β, uf.(0) * ) to (δ, uf.(0) * ) (represented by an arrow) has been added by the read parent->parent at line 17. Having a variable δ materialized to represent the contents of β allows inferring δ = 0 from the test parent->parent != 0.

Staged points-to predicates. A staged points-to predicate α → β represents a store operation performed by the program, but that is not yet propagated to the main domain S . The idea is that if that if an invariant is temporarily violated, subsequent stores may restore it; by grouping and delaying the stores to the type-based abstract domain S , we prevent S from needing to take ill-typed states into account. In the concretization, the heap represented by the staged points-to predicates take precedence (operator ) over the heap represented by the type-based domain. Note this concretization allows describing states that are not well-typed, hence the codomain of γ U is P S × (V → V) instead of P S t × (V → V) .

Example 8 (Staged points-to predicate). The contents of the memory allocated at line at line 40 of Figure 1 are unconstrained, and may not correspond to the type node* of the address returned by malloc: the reachable states at this line include ill-typed states that are not representable by S . This is fixed by introducing staged points-to predicates from the address returned by malloc, which allows the abstract value of the typed domain to represent only well-typed states, but still take into account the call to malloc. These staged points-to predicates are modified by the subsequent statements, and from line 44, the staged points-to predicates can be dropped by performing the corresponding stores to the memory, because the reachable states are now well-typed.

Static analysis operations.

The addition of points-to predicates only changes the behaviour of memory operations (load,store, and malloc). The definition of these operations rely on determination of must and may-alias information between pairs (α t , β u ) of abstract values. This is done using both the types (Theorem 1) and numerical information about addresses (e.g. addresses of an array at two indices i and j with i < j will not alias), but this can be enhanced with information coming from other domains (like allocation sites [START_REF] Andersen | Program Analysis and Specialization for the C Programming Language[END_REF]).

A malloc t of type t is interpreted simply by adding a staged points-to predicate α t * → β t where both α and β are fresh symbolic variables.

Loading a value of size at address α t returns the value β u if a points-to predicate v → β u exists in the domain and we can prove α = . Otherwise we performs a "weak read" by evaluating the load on the type-based domain, and joining the result with the values of all the staged points-to predicates whose addresses may alias with α t . Finally, if β u is the result of this operation, the analysis adds a new retained points-to predicate α t → β u .

Storing a value δ u of size at address α t first needs to remove all points-to predicates that may alias with α t . Retained points-to predicates are simply dropped, but staged points-to predicate must be propagated by performing the corresponding stores to the type-based shape domain. Then, a new staged points-to predicate α t → δ u is added.

Example 9. Consider again the abstract state (Figure 3) at line 19 of Figure 1. The statement x->parent = parent->parent first reads parent->parent from mem-ory, and retrieves δ, from the points-to predicate β → δ. The store to x->parent (corresponding to address α) first needs to drop points-to predicates that may alias with α; on this abstract state, only β → δ is concerned. Finally, a new points-to predicate α → δ is added. Note that α = β is an invariant of the program; if the type based shape domain were complemented with a more precise abstraction, then the points-to predicate β → δ would not need to be dropped.

Experimental evaluation

Research questions. The goal of our experimental evaluation is to evaluate the performance and precision of our analysis, the effort required for its parametrization, its ability to handle low-level (binary and system) code and complex sharing patterns.

Methodology. We have implemented two analyses (available at https://zenodo. org/record/5512941) using the Codex library for abstract interpretation: one for C code using the Frama-C platform (Frama-C/Codex); one for binary code using the Binsec platform (Binsec/Codex). All analyses have been conducted on a standard laptop (Intel Xeon E3-1505M 3Ghz, 32GB RAM). We took the mean values between 10 runs, and report the mean (all standard deviations were below 4%).

We ran our analysis on all the C benchmarks from two shape analysis publications; moreover we analyze their compiled version using gcc 10.3.0 with different levels of optimizations. These benchmarks are challenging: the graph-* benchmarks from Li et al. [START_REF] Li | Shape analysis for unstructured sharing[END_REF] were used to verify unstructured sharing patterns; to complete this evaluation we extend this with our running example. The other benchmarks from Li et al. [START_REF] Li | Semantic-directed clumping of disjunctive abstract states[END_REF] were used to demonstrate scalability issues faced by shape analyzers. Both benchmarks were created to demonstrate shape analysis, which is a more precise abstraction than the one we propose. Thus, they are suitable to evaluate performance, ability to handle complex sharing patterns, and precision.

This evaluation completes that in Nicole et al. [START_REF] Nicole | No crash, no exploit: Automated verification of embedded kernels[END_REF], where we ran our analyzer on the kernel executable of an industrial embedded kernel (Asterios, developed by Krono-safe) to verify security properties (including full memory safety), with only 58 lines of manual annotations, which demonstrated the ability to handle low-level code, precision, performance and low amount of parametrization on a larger use case.

Results Table 1 provides the results of the evaluation. The benchmarks are grouped by the data structure they operate on; we report the number of lines describing physical types (generated from existing types information, or manually edited) shared by a group. The annotations mostly consist in constraining some pointers types to be non-null. The pre column describes necessary pre-conditions of the verified function (e.g. that a pointer argument must not be null). The LOC column is the number of lines of code of each function, excluding comments, blank lines and subroutines. The ratio of lines of manual annotations per line of code for a group, goes from 0% to 7.8%, with a mean of 3.2% and median of 2.7%.

The next columns in the table provide the Time taken by the full analysis (in s), the number of alarms of the full analysis ( → column) and the analysis without the retained and staged points-to predicates ( → column), for the C version of the code and the various binaries produced by GCC. For brevity we have omitted the time taken by the → analysis Table 1. Results of the evaluation in the benchmarks; on average this analysis takes 1.5% less time for the C, and 20% less for binary code (maximum: 45%). The number of alarms is counted differently in C (one possible alarm each time the analyzer evaluates a statement) and in binary (where alarms are uniquified per instruction), but in both 0 alarms means that the analyzer verified type-safety. We observe that the full analyzer succeeds in verifying 30 benchmarks (out of 34), both in C and binary code. Removing the points-to predicates makes the analysis significantly less precise, as only 13 benchmarks are verified in C, and between 16 (for -O0) and 21 (for -O1,-O2,-O3) in binary code.

Discussion and conclusions Our combination of domains is effective at verifying type safety (which entails spatial memory safety) on C and binary code, even for benchmarks that have complex sharing patterns, with a low amount of annotations. The analysis performs evenly well on all benchmarks, and scales well on javlinsert-32×, which is challenging even for shape analysis with disjunctive clumping [START_REF] Li | Semantic-directed clumping of disjunctive abstract states[END_REF]. We interpret the fact that binary analysis is faster than the C analysis by implementation issues in the C analyzer.

The points-to predicates are very important for precision, as otherwise the number of false alarms raises significantly. The analysis succeeds equally on binary programs and on C programs, despite the complex code patterns that the C compiler may produce. Note that without points-to predicates, more binary codes are verified than in C: indeed in some cases the compiler performs a register promotion of a heap value, which removes the need for a points-to predicate.

Related works and conclusion

Memory analyses based on type inference. Several analyses that partially verify spatial memory safety using static type inference have been proposed. As unification-based type inference is less expressive than abstract interpretation, it is insufficiently precise to verify spatial memory safety, which is generally addressed by also using dynamic verification (e.g. Cyclone [START_REF] Jim | Cyclone: A safe dialect of C[END_REF], CCured [START_REF] George C Necula | Ccured: Type-safe retrofitting of legacy software[END_REF], CheckedC [START_REF] Samuel | Checked C: Making C Safe by Extension[END_REF]). Still, the structural subtyping notion that we use is similar to the physical subtyping by Chandra and Reps [START_REF] Chandra | Physical type checking for C[END_REF], even if the physical type safety property that they verify does not include spatial memory safety (e.g. it does not check pointer arithmetics or null pointer dereferences). Liquid types [START_REF] Maxim Rondon | Low-level liquid types[END_REF] provide refinement types similar to ours, that are type checked by enhancing type inference with abstract interpretation and SMT solving. They discuss several limitations that our work solves: lack of structural subtyping (that we solve using our ordering on concrete and abstract types), and conservative decisions of when to fold and unfold variables (that we solve by using abstract interpretation instead of type inference [START_REF] Cousot | Types as abstract interpretations[END_REF], which allows our focusing decisions to be based on the current results of the analysis).

Other type-based memory analyses. Type-based alias analyses [START_REF] Diwan | Type-based alias analysis[END_REF] propose a system to determine aliasing based on subtyping relations, which is present in our work (Theorem 1). These analyses assume that type safety is verified by other means (e.g. type checking), while our abstract interpretation also verifies type safety, on unsafe languages like C and binary code. Data structure analysis [START_REF] Lattner | Macroscopic Data Structure Analysis and Optimization[END_REF] produces a flow-insensitive description of data structure layout similar to our description of types (excluding numerical predicates), which could be used to split our types into distinct subtypes, making our analysis more precise. The structural analysis by Marron et al. [START_REF] Marron | Structural analysis: Shape information via points-to computation[END_REF] is also an intermediate between pointer and shape analyses, which is more precise than our type-based shape domain as it builds a flow-sensitive abstract heap information (the storage shape graph), while our description of types is flow-invariant. But their analysis proceeds on a type-safe language with no type cast, pointer arithmetic, interior pointers, or uninitialized data. Contrary to their results, our experience indicates that strong updates are important to verify the preservation of structural invariants, which we believe comes from the lower-level nature of our source languages. In a previous work [START_REF] Nicole | No crash, no exploit: Automated verification of embedded kernels[END_REF] we used our type-based domain to verify security properties of an industrial embedded kernel; this work formally presents the analysis, extended with retained and staged points-to predicates and support for dynamic memory allocation.

Shape analyses. Many challenges arise in programs manipulating memory. These have been individually adressed by existing work on shape analyses, for instance to limit disjunctions [START_REF] Manevich | Partially disjunctive heap abstraction[END_REF][START_REF] Li | Semantic-directed clumping of disjunctive abstract states[END_REF], to adapt to custom data structures [START_REF] Sagiv | Parametric shape analysis via 3-valued logic[END_REF][START_REF] Chang | Shape analysis with structural invariant checkers[END_REF], to interpret low-level memory operations [START_REF] Kreiker | Shape analysis of low-level C with overlapping structures[END_REF][START_REF] Vincent Laviron | Separating shape graphs[END_REF][START_REF] Dudka | Byte-precise verification of low-level list manipulation[END_REF], to allow composite data structures [START_REF] Berdine | Shape analysis for composite data structures[END_REF][START_REF] Toubhans | Reduced product combination of abstract domains for shapes[END_REF], interaction with arrays [START_REF] Liu | An array content static analysis based on noncontiguous partitions[END_REF], data structure invariants [START_REF] Chang | Shape analysis with structural invariant checkers[END_REF], or unstructured sharing [START_REF] Li | Shape analysis for unstructured sharing[END_REF]. Our type-based analysis is less precise than a full shape analysis, as e.g. it cannot verify temporal memory safety (i.e. use-after-free errors), but it simultaneously handles all the above aspects in a simpler analysis, which is sufficiently precise to verify preservation of structural invariants and spatial memory safety.

1 typedef struct uf { 2 struct 23 }Fig. 1 .

 2231 Fig. 1. An algorithm for union-find and listing elements in a partition.

M

  : node kind → {x : word4 | x ≤ 5} uf → uf.(0) * dll → dll.(0) * =0 × dll.(0) * =0 node → node kind × dll × uf (b) Physical types. Analysis of merge.

Fig. 3 .

 3 Fig. 3. Abstract state before line 19.

  and ∈ N, we let h[a..a+ ] denote the reading of a cell of size at address a. It is defined by h[a..a+ ] = h(a) :: h(a+1) :: • • • :: h(a+ -1).

Lemma 1 (Example 3 .

 13 Monotonicity). Let t.(n) and u.(m) be two address types such that t.(n) u.(m). Then t.(n) * =0 L,ν ⊆ u.(m) * =0 L,ν . In Figure 2(a), and using the labeling of Example 2, node.(4) * =0 L,ν and dll.(0) * =0 L,ν both denote the set of addresses {0x24, 0x64, 0x84}.

Fig. 7 .

 7 Fig. 7. Selected transition rules for programs.

Example 5 .

 5 (Upcasting after pointer arithmetics) Following Definition 3, int[START_REF] Deutsch | Interprocedural may-alias analysis for pointers: Beyond k -limiting[END_REF].(α) * v int.(0) * holds when both numerical constraints α ∈ [0, 39] ∧ ∃k ∈ N, α = 4k hold. Thus the abstract type given in Example 4 can be safely casted into an int * . Note that querying the numerical abstract domain is necessary to check the safety of this cast.

Fig. 8 .

 8 Fig. 8. Extending the base domain (s ) with retained (r ) and staged (p ) points-to predicates

  T maps variables to types. We write S t for the set of such 4-tuples.Moreover, state (σ, h, L, Γ ) is well typed if and only if: 1. The labeling is consistent with the heap: for all address a ∈ A, if there exists a type t such that L(a) = t.(0), then h[a..a + size ν (t)] ∈ t L,ν ; 2. Variables are well-typed: for all variable

Definition 7 (Well-typed state). A state is a 4-tuple (σ, h, L, Γ ), where σ ∈ Σ, h ∈ H, L is a labeling, and Γ : X →

A difference is that retained point-to predicate only retains information about a given cell, instead of modifying the heap summary to be precise on this cell.