Jiangchao Liu
email: jliu@di.ens.fr

Xavier Rival
email: rival@di.ens.fr

Abstraction of Arrays Based on Non Contiguous Partitions ⋆

Array partitioning analyses split arrays into contiguous partitions to infer properties of cell sets. Such analyses cannot group together non contiguous cells, even when they have similar properties. In this paper, we propose an abstract domain which utilizes semantic properties to split array cells into groups. Cells with similar properties will be packed into groups and abstracted together. Additionally, groups are not necessarily contiguous. This abstract domain allows to infer complex array invariants in a fully automatic way. Experiments on examples from the Minix 1.1 memory management demonstrate its effectiveness.

Introduction

Arrays are ubiquitous, yet their mis-use often causes software defects. Therefore, a large number of works address the automatic verification of array manipulating programs. In particular, partitioning abstractions [START_REF] Cousot | A parametric segmentation functor for fully automatic and scalable array content analysis[END_REF][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] split arrays in sets of contiguous groups of cells, in order to, hopefully, infer they enjoy similar properties. A traditional example is that of an initialization loop, with the usual invariant that splits the array in an initialized zone and an uninitialized region.

However, when cells that have similar properties are not contiguous, these approaches cannot infer adequate array partitions. This happens for unsorted arrays of structures, when there is no relation between indexes and cell fields. Then, there are usually relations among cell fields. This phenomenon can be observed in low-level software, such as operating system services and critical embedded systems drivers, which rely on static array zones instead of dynamically allocated blocks [START_REF] Sotin | Hierarchical shape abstraction of dynamic structures in static blocks[END_REF]. When cells with similar properties are not contiguous, traditional partition based techniques are unlikely to infer relevant partitions / precise array invariants. Figure 1 illustrates the Minix 1.1 Memory Management Process Table (MMPT) main structure. The array of structures mproc defined in Figure 1(a) stores the process descriptors. Each descriptor comprises a field mparent that stores the index of the parent process in mproc, and a field mpflag that stores the process status. [0] : mm [START_REF] Alberti | Decision procedures for flat array properties[END_REF] : fs [START_REF] Beyer | Invariant synthesis for combined theories[END_REF] : init [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] : usr1

[4] : usr0

[5] : free slot [START_REF] Cox | Automatic analysis of open objects in dynamic language programs[END_REF] : usr2 of mproc is a process descriptor when its field mpflag is strictly positive and a free slot if it is null. Minix 1.1 uses the three initial elements of mproc to store the descriptor of the memory management service, the file system service and the init process. Descriptors of other processes appear in a random order. In the example of Figure 1, init has two children whose descriptors are in mproc [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] and mproc [START_REF] Cousot | Systematic design of program analysis frameworks[END_REF]; similarly, the process corresponding to mproc [START_REF] Cousot | Systematic design of program analysis frameworks[END_REF] has a single child the descriptor of which is in mproc [START_REF] Cox | Automatic analysis of open objects in dynamic language programs[END_REF]. Moreover, Minix assumes a parent-child relation between mm and fs, as mm has index 0 and the parent field of fs stores 0. To abstract the process table state, valid process descriptors and free slots should be partitioned into different groups.

Traditional, contiguous partitioning cannot achieve this for two reasons: (1) the order of process descriptors in mproc cannot be predicted, hence is random in practice, and (2) there is no simple description of the boundaries between these regions (or even their sizes) in the program state. The symbolic abstract domain by Dillig, Dillig and Aiken [START_REF] Dillig | Fluid updates: Beyond strong vs. weak updates[END_REF] also fails here as it cannot attach arbitrary abstract properties to summarized cells.

In this paper, we set up an abstract domain to partition the array into non contiguous groups for process descriptors and free slot so as to infer this partitioning and precise invariants (Section 2) automatically. Our contributions are:

1. An abstract domain that partitions array elements according to semantic properties, and can represent non contiguous partitions (Section 3). 2. Static analysis algorithms for the computation of abstract post-conditions (Sections 4 and Section 5), widening and inclusion check (Section 6). 3. The implementation and the evaluation of the analysis on the inference of tricky invariants in an excerpt of the Minix 1. (a) A concrete state of mproc

G0 Idx 0 = 2 G1 0 ≤ Idx 1 ≤ 23 G2 0 ≤ Idx 2 ≤ 23
Numeric relations:

Sz 0 = 1 ∧ 0 ≤ Sz 1 ≤ 23 ∧ 0 ≤ Sz 2 ≤ 23 ∧ 1 ≤ mpflag 0 ≤ 63 ∧ mpflag 1 = 0 ∧ 1 ≤ mpflag 2 ≤ 63 ∧ mparent 0 = 0 ∧ 0 ≤ mparent 2 ≤ 23
Group relations:

mparent 2 ⊳ G0 ∪ G2
(b) Abstract state with partition Fig. 2. A partitioning of mproc based on non contiguous groups

Overview

The Minix MMPT requires mproc to permanently satisfy two invariants:

1. Each valid process descriptor has a mparent field, that should store a value in [0, 23], hence represents a valid index in mproc: this entails the absence of out-of-bound accesses in process table management functions. 2. The mparent field of any valid process descriptor should be the index of a valid process descriptor: as a process can only complete its exit phase when its parent calls wait, failure to maintain a parent for each process could cause a terminating process to become dangling and never be eliminated. To verify these invariants, we propose to check that all system calls preserve them. We design an automatic analysis to verify that, if they are called in a state that satisfies these invariants, they return in a state that also satisfies them. A concrete state is displayed in Figure 2(a), and its abstraction is shown in Figure 2(b). Group 0 contains only the process descriptor of init. Group 1 collects all free slots. Group 2 consists of all the valid process descriptors except that of init. The reason why we split init out into a separate group is that it is often treated in a special manner by OS routines. We let G i denote the set of indexes of all the elements in group i.

The abstract state shown in Figure 2(b) ties each group to properties of its elements. These will be formally defined in Section 3. By the Minix specification, the elements of group 2 satisfy the following correctness conditions C:

their indexes are in [0, 23], which we note 0 ≤ Idx 2 ≤ 23 in Figure 2(b); -their flags are in [START_REF] Alberti | Decision procedures for flat array properties[END_REF]63] (valid process descriptors have a strictly positive flag), which we note 1 ≤ mpflag 2 ≤ 63; -their parents are valid indexes, which we note 0 ≤ mparent 2 ≤ 23; -their parents are indexes of valid process descriptors, hence are also in group 0 or group 2, which we note mparent 2 ⊳ G 0 ∪ G 2 ; -the size of group 2 is between 0 and 23, which we note 0 ≤ Sz 2 ≤ 23. Our abstraction relies on disjoint groups as other array partitioning abstractions [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]. However, our abstraction does not assume each group consists of a contiguous set of cells. The non-contiguousness of groups is represented by winding separation lines in Figure 2(b). To characterize groups, our abstraction relies void cleanup(int child){ . . . not only on constraints on indexes, but also on semantic properties of the cell contents: while groups 1 and 2 correspond to a similar range, the mpflag values of their elements are different (0 in group 1 and any value in [START_REF] Alberti | Decision procedures for flat array properties[END_REF]63] in group 2). Therefore our abstraction can express both contiguous and non contiguous partitions. In this example, we believe the abstract state of Figure 2(b) is close to the programmer's intent, where the array is a collection of unsorted elements. We now consider the verification of Minix MMPT management procedures. We focus on cleanup, which turns elements of mproc that describe hanging processes into free slots. Figure 3(a) displays an excerpt of a simplified, recursion free version of cleanup, which is chosen to highlight the analysis difficulties. The call cleanup(4) in the state of Figure 2(a) will remove process usr0 and falls in that case; the result is shown in Figure 3(b): process usr2 becomes a child of init, while the record formerly associated to usr0 turns into a free slot.

0 int parent = mproc[child].mparent; 1 if (parent == 2){ 2 mproc[parent].mpflag = 1; 3 mproc[child].mpflag = 0; 4 for(i = 0; i < 24; i++){ 5 if (mproc[i].mpflag > 0) if (i! = parent) if (mproc[i].mparent == child) mproc[i].mparent = 2; } 6 }else{. . .} . . .} (
Function cleanup should be called in a correct Minix process table state and be applied to a child process in group 2, which we note child⊳ G 2 . Figure 4 overviews the steps of the automatic static analysis of the excerpt of cleanup. The analysis proceeds by computing abstract post-conditions and loop invariants [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF]. In this section, we focus on (1) cell materialization, (2) termination of the loop analysis and (3) removal of unnecessary groups.

From the precondition, fields mparent of all elements in group 2 are indexes in groups G 0 or G 2 (abstract state at point 0 ). The test entails mparent is 2 at point

At point 0 C ∧ child ⊳ G2 At point 1 C ∧ child ⊳ G2 ∧ parent ⊳ G2 ∪ G0 At point 2 C ∧ child ⊳ G2 ∧ parent ⊳ G0 At point 3 C ∧ child ⊳ G2 ∧ parent ⊳ G0 ∧ mpflag 0 = 1 At point 4 group 0 . . . group 1 . . . group 2 0 ≤ Idx 2 ≤ 23 group 3 0 ≤ Idx 3 ≤ 23 Numeric relations: 0 ≤ Sz 2 ≤ 22 ∧ Sz 3 = 1 ∧ 1 ≤ mpflag 2 ≤ 63 ∧ mpflag 3 = 0 ∧ 0 ≤ mparent 2 ≤ 23 ∧ 0 ≤ mparent 3 ≤ 23 Group relations: child ⊳ G3 ∧ mparent 2 ⊳ G0 ∪ G2 ∪ G3 ∧ mparent 3 ⊳ G0 ∪ G2 ∪ G3
   0 ≤ i ∧ 0 ≤ Sz 2 ≤ 22 ∧ 0 ≤ Sz 4 ≤ 22 ∧ 1 ≤ mpflag 2 ≤ 63 ∧ 1 ≤ mpflag 4 ≤ 63 ∧ 0 ≤ mparent 2 ≤ 23 ∧ 1 ≤ mparent 4 ≤ 63 ∧ 0 ≤ mparent 4 ≤ 23 Group relations: child ⊳ G3 ∧ mparent 2 ⊳ G0 ∪ G2 ∪ G3 ∪ G4 ∧ mparent 4 ⊳ G0 ∪ G2 ∪ G4
At point 6 group 0

Idx 0 = 2 group 1 0 ≤ Idx 1 ≤ 23 group 3 0 ≤ Idx 3 ≤ 23 group 4 0 ≤ Idx 4 ≤ 23
Numeric relations:

   Sz 0 = 1 ∧ 0 ≤ Sz 1 ≤ 22 ∧ Sz 3 = 1 ∧ 0 ≤ Sz 4 ≤ 22 ∧ mpflag 0 = 1 ∧ mpflag 1 = 0 ∧ mpflag 3 = 0 ∧ 1 ≤ mpflag 4 ≤ 63 ∧ 0 ≤ mparent 0 ≤ 23 ∧ 0 ≤ mparent 3 ≤ 23 ∧ 0 ≤ mparent 4 ≤ 23
Group relations: The analysis of all the statements in the program follows similar principles. We only discuss the termination of the analysis here, as our abstract domain has infinite chains (the number of groups is not bounded), hence the analysis of loops requires a terminating binary widening operator [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF]. Widening associates groups of its inputs with groups of its result (ensuring the number of groups can only decrease to guarantee termination), and over-approximates group properties. After two widening iterations, our analysis produces abstract post-fixpoint 5 , where group 1 describes free slots, group 0 describes init, group 3 consists of child (just cleaned up) and groups 2 (resp., 4) represent valid process descriptors with indexes greater (resp., lower) than i. Our analysis can also decrease the number of groups, when some become redundant, e.g., when the analysis proves a group empty. For instance, the loop fixpoint 5 shows that indexes of elements in group 2 are greater than i. Thus, after the loop exit, any element of group 2 should have an index greater than 24, which implies this group is empty. Hence, this group is removed, and the analysis produces post-condition 6 , which entails correctness condition C (note that group 3, corresponding to child now describes a free slot).

mparent 4 ⊳ G0 ∪ G4 ∧ child ⊳ G3

Abstract domain and abstraction relation

In this section, we formalize abstract elements and their concretization. We describe the abstraction of the contents of arrays, using numeric constraints, in Section 3.1. Then, we extend it with relations between groups in Section 3.2.

The non-contiguous array partition domain

Concrete States. Our domain abstracts arrays of complex data structures. To highlight its core principle and simplify the formalization, we make two assumptions on the programs to analyze. First, there is no array access through pointer dereference (handling them would only require a product with a pointer domain), thus all array index expressions are of the form a[ex]. Secondly, all variables are either base type (e.g., scalar) variables (denoted by X) or arrays of structures (denoted by A). Structures are considered arrays of length 1, and arrays of scalars are considered arrays of structures made of a single field. A concrete state σ is a partial function mapping basic cells (base variables and fields of array elements) into values (which are denoted by V). We let N denote non-negative integers and F denote the set of fields. Thus, the set S of concrete states is defined by S = (A × N × F ∪ X) → V. More specifically, the set of all fields of elements of array a are denoted by F a , and the set of valid indexes in a is denoted by N a .

Non-contiguous array partition. Our analysis partitions each array into one or several groups of cells. A group is represented by an abstraction G i of the set of indexes of its elements, where subscript i identifies the group. We let G denote the set of group names {G i | i ≥ 0}. An array partition is a function p : A → P(G) which maps each array variable to a set of groups. We always enforce the constraint that groups of distinct arrays should have distinct names, to avoid confusion (∀a 1 , a 2 ∈ A, a 1 = a 2 ⇒ p(a 1 ) ∩ p(a 2 ) = ∅). To express properties of group contents, sizes, and indexes, we adjoin numeric abstract values to partition p. This numeric information is split into a conjunction made of two parts.

First, a global component n g constrains base type variables, group sizes and group fields. Group fields are marked as summary dimensions [START_REF] Gopan | Numeric domains with summarized dimension[END_REF] in n g , that is as numeric abstract domain dimensions that account for one or more concrete cell(s), whereas base type variables and group sizes are non-summary dimension, i.e., each of them represents exactly one concrete cell.

Second, for each group G i , the index Idx i is constrained by a numeric abstract value n i . This second component is needed because our abstract domain allows empty groups, and when group G i is empty, Idx i has no value, which is expressed by n i = ⊥. Intuitively, in the concrete level, Idx i denotes a possibly empty set of values (an empty group example will be provided in Section 7.2).

To sum up, an abstract element is a pair (p, -→ n ) where -→ n is a tuple (n g , n 0 , . . . , n k-1 ), and p defines k array partitions. Our abstract domain is parameterized by the choice of a numeric abstract domain N ♯ , so as to tune the analysis precision and cost. In this paper, we use the octagon abstract domain [START_REF] Miné | The octagon abstract domain[END_REF].

a[0] value = 2 a[1] value = -110 a[2]
value = 2 a [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] value = -120 a [START_REF] Cousot | Systematic design of program analysis frameworks[END_REF] value = 8 a [START_REF] Cousot | A parametric segmentation functor for fully automatic and scalable array content analysis[END_REF] value = -100 a [START_REF] Cox | Automatic analysis of open objects in dynamic language programs[END_REF] value = -100

(a) Concrete array X p(a) = {G0, G1} G0 0 ≤ Idx 0 ≤ 4 G1 1 ≤ Idx 1 ≤ 6 n g : 2 ≤ value0 ≤ 8 ∧ -120 ≤ value1 ≤ -100 ∧ Sz 0 = 3 ∧ Sz 1 = 4 (b) Abstract state a ♯

Concretization.

A concrete numeric mapping is a function ν, mapping each base type variable to one value, each structure field to a non empty set of values and each index to a possibly empty set of values. We write γ N ♯ for the concretization of numeric elements, which maps a set of numeric constraints -→ n into a set of functions ν as defined above. The concretization γ N ♯ (n i ) of constraints over group G i is such that, when

n i = ⊥ and ν ∈ γ N ♯ (n i ), then ν(Idx i ) = ∅. Then, γ N ♯ (n g , n 0 , . . . , n k-1 ) = γ N ♯ (n g )∩γ N ♯ (n 0 ) . . . γ N ♯ (n k-1 ). A valuation is a function ψ ∈ Ψ = G → P(Z)
, and interprets each group by the set of indexes it represents in a given concrete state. Additionally, we use the following four predicates to break up the definition of concretization:

P v (ψ) def. ⇐⇒ ∀a ∈ A, Gi∈p(a) ψ(G i ) = N a ∧ (∀G i , G j ∈ p(a), i = j ⇒ ψ(G i ) ∩ ψ(G j ) = ∅) P b (σ, ν) def. ⇐⇒ ∀v ∈ X, ν(v) = σ(v) P i (ν, ψ) def. ⇐⇒ ∀a ∈ A, G i ∈ p(a), ψ(G i ) = ν(Idx i ) ∧ |ψ(G i )| = ν(Sz i ) P c (σ, ψ, ν) def. ⇐⇒ ∀a ∈ A, f ∈ F a , G i ∈ p(a), j ∈ ψ(G i ), σ(a, j, f) ∈ ν( f i )
Predicate P v (ψ) states that each array element belongs to exactly one group (equivalently, groups form a partition of the array indexes). Predicate P b (σ, ν) expresses that ν and σ consistently abstract base type variables. Predicate P i (ν, ψ) expresses that ν and ψ consistently abstract group indexes. Last, predicate P c (σ, ψ, ν) states σ and ν define compatible abstractions of groups contents.

Definition 1 (Concretization). Concretization γ P is defined by:

γ P (p, -→ n ) def. ::= {(σ, ψ, ν) | ν ∈ γ N ♯ ( -→ n ) ∧ P v (ψ) ∧ P b (σ, ν) ∧ P i (ν, ψ) ∧ P c (σ, ψ, ν)}

Relation predicates

The abstraction we have defined so far can describe non-contiguous groups of cells, yet lacks important predicates, that are necessary for the analysis. Let us consider assignment parent = mproc [child].mparent in cleanup (Figure 3(a)). Numeric constraints localize child in [0, 23], but this information does not determine precisely which group does cell mproc[child] belong to. In particular, the analysis will ignore from that point whether parent is the index of a valid process descriptor or not. To avoid this imprecision, we extend abstract states with relation predicates, that express properties such as the membership of the value of a variable in a group. They are defined by the grammar below:

Definition 2 (Relation predicates).

r ::= r ∧ r a conjunction of predicates | true empty | v ⊳ G a where v ∈ X var-index predicate | f i ⊳ G a where f ∈ F a , G i ∈ p(a) content-index predicate G a ::= G a ∪ G i where G i ∈ p(a) a disjunction of groups in a | G i where G i ∈ p(a)
A relation predicate r is a conjunction of atomic predicates. Predicate v⊳G a means the value of variable v is an index in G a , where G a is a disjunction of a set of groups of array a. Similarly, predicate f i ⊳ G a means that all fields f of cells in group i are indexes of elements of G a . As an example, if

G a = G 1 ∪ G 3 , then v ⊳ G a expresses that the value of v is either the index of a cell in G 1 or the index of a cell in G 3 .
Example 2. We consider function cleanup of Figure 3(a). The pre-condition for the analysis of Figure 4 is based on correctness property C, hence partitions mproc in three groups, thus p(mproc) = {G 0 , G 1 , G 2 }. Additionally, cleanup should be called on a valid process descriptor different from that of init, hence child should be in group G 2 , which corresponds to predicate child ⊳ G 2 . Then parent is initialized as the parent of child. Since mparent 2 ⊳ G 0 ∪ G 2 , parent is a valid process descriptor index, and the analysis derives parent ⊳ G 0 ∪ G 2 . Hence, at point 1 , the analysis will derive relations r

= child ⊳ G 2 ∧ parent ⊳ G 0 ∪ G 2 ∧ . . ..
Similarly, in the else branch of condition if (parent == 2), the analysis derives that parent ⊳ G 2 .

Concretization. We now extend the concretization to account for relations. First, we let ψ be defined on disjunction of groups, and let ψ(G 0 ∪ . . .

∪ G i ) = ψ(G 0 ) ∪ . . . ∪ ψ(G i ).
We write D ♯ for the set of triples (p, -→ n , r). Definition 3 (Abstract states and their concretization). An abstract state a ♯ is a triple (p, -→ n , r) ∈ D ♯ . The concretization γ D ♯ is defined by:

γ D ♯ (p, -→ n , r) ::= {σ | ∃ψ, ν, (σ, ψ, ν) ∈ γ aux (p, -→ n , r)} γ aux (p, -→ n , true) ::= γ P (p, -→ n ) γ aux (p, -→ n , v ⊳ G a ) ::= {(σ, ψ, ν) ∈ γ P (p, -→ n ) | σ(v) ∈ ψ(G a )} γ aux (p, -→ n , f i ⊳ G a ) ::= {(σ, ψ, ν) ∈ γ P (p, -→ n ) | ∀k ∈ ψ(G i ), σ(a, k, f) ∈ ψ(G a )} γ aux (p, -→ n , r 0 ∧ r 1 ) ::= γ aux (p, -→ n , r 0 ) ∩ γ aux (p, -→ n , r 1 ) G0 0 ≤ Idx 0 ≤ 99 n g : value0 = 0 ∧ Sz 0 = 100 r : i ⊳ G0 (a) a ♯ G0 0 ≤ Idx 0 ≤ 99 G1 0 ≤ Idx 1 ≤ 99 n g : value0 = 0 ∧ value1 = 0 ∧ Sz 0 = 99 ∧ Sz 1 = 1 r : i ⊳ G1 (b) split(a ♯ , i) G0 0 ≤ Idx 0 ≤ 99 G1 0 ≤ Idx 1 ≤ 99 n g : value0 = 0 ∧ value1 = 1 ∧ Sz 0 = 100 ∧ Sz 1 = 0 r : i ⊳ G0 (c) create(a ♯ )
Fig. 6. Partition splitting and creation in array a from abstract state a ♯

Basic operators on partitions

In this section, we define basic operations on partitions (such as creation and merge), that abstract transfer functions and operators rely on.

Splitting and creation. Unless specified otherwise, our analysis initially partitions each array into a single group, with no contents constraint. Additional groups get introduced during the analysis, by two basic operations: 1. Operator split replaces a group with two groups, that inherit the properties of the group they replace (also, membership in the old group turns into membership in the join of the new groups). It is typically applied to materialize a cell of a given index (in the group bounds) and enable a strong update. 2. Operator create introduces an empty group and is used to generalize abstract states in join and widening (note any field property is satisfied by the empty group; the analysis selects properties depending on the context). Both operators preserve concretization.

Example 3. Figure 6(a) defines an abstract state (p, -→ n , r) with a single array, fully initialized to 0, and represented by a single group. Applying operator split to that abstract state and to index i produces the abstract state of Figure 6(b), where G 1 is a group with exactly one element, with the same constraints Idx and value as in the previous state. Similarly, Figure 6(c) shows a possible result for create.

Merging groups. Fine partitions with many groups can provide great precision but may incur increased analysis cost. Therefore, the analysis can also force the fusion of several groups into one by calling operation merge on a set of groups. This is performed either as part of join and widening or when transfer functions detect some groups get assigned similar values. Example 4. Figure 7(a) defines an abstract state a ♯ which describes an array with two groups. Applying merge to a ♯ and set {0, 1} produces the state shown in Figure 7(b), with a single group and coarser predicates, obtained by joining the constraints over the contents of the initial groups.

G0 0 ≤ Idx 0 ≤ 99 G1 0 ≤ Idx 1 ≤ 99 n g : 3 ≤ value0 ≤ 5 ∧ value1 = 1 ∧ Sz 0 = 50 ∧ Sz 1 = 50 r : i ⊳ G0 ∪ G1 (a) a ♯ G0 0 ≤ Idx 0 ≤ 99 n g : 1 ≤ value0 ≤ 5 ∧ Sz 0 = 100 r : i ⊳ G0
(b) merge(a ♯ , {0, 1}) Fig. 7. Merging in abstract state a ♯ Reduction. Our abstract domain can be viewed as a product abstraction and can benefit from reduction [START_REF] Cousot | Systematic design of program analysis frameworks[END_REF]. In a ♯ = (p, -→ n , r), components -→ n and r may help refining each other. For instance, in Figure 4, the analysis infers at point 1 that parent ⊳ G 0 ∪ G 2 and Idx 0 = 2. Combining this with the numerical information derived from test parent == 2, the analysis should derive that parent ⊳ G 0 (i.e., parent is the index of init). Conversely, r may refine the information on -→ n : if child ⊳ G 2 , then group G 2 has at least one element, thus Sz 2 ≥ 1. Such steps are performed by a partial reduction operator reduce, which strengthens the numeric and relation predicates, without changing the global concretization [START_REF] Cousot | Systematic design of program analysis frameworks[END_REF] (the optimal reduction would be overly costly to compute). This reduction is done lazily: for instance, the analysis will attempt to generate relations between i and Idx i only when i is used as an index to access the array G i corresponds to.

Basic operations split, create, merge and reduce are sound:

Theorem 1 (Soundness). If a ♯ is an abstract state, t an array, G i a group, then

γ D ♯ (a ♯ ) ⊆ γ D ♯ (split(a ♯ , t, G i )) and γ D ♯ (create(a ♯ , t)) = γ D ♯ (a ♯ ).
Moreover, if S is a set of groups, γ D ♯ (a ♯ ) ⊆ γ D ♯ (merge(a ♯ , t, S)). Similarly, reduce does not change concretization.

Transfer functions

Our analysis of C programs proceeds by forward abstract interpretation [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF]. In this section, we study the abstract transfer functions for tests and assignments.

Analysis of conditions

In the concrete level, if ex is an expression, test ex? filters out states that do not let ex evaluate into TRUE. Its concrete semantics can thus be defined as a function over sets of states, by ∀S ⊆ S, ex? (S) = {σ ∈ S | ex (σ) = TRUE}.

Intuitively, the abstract interpretation of a test from abstract state a ♯ = (p, -→ n , r) can directly improve the constraints in the numeric component -→ n , which can then be propagated into r by reduce. The numeric test will derive new constraints only over non summary dimensions, thus tests over fields of groups that contain more than one element will not refine abstract values.

When a test involves an array cell as in a[i] == 0?, and if the group that cell belongs to cannot be known precisely, a more precise post-condition can be derived by performing a locally disjunctive analysis, that applies numeric test to each possible group, and then joins the abstract states. For instance, if i ⊳ G 0 ∪ G 1 , the analysis will analyze test a[i] == 0? for both i ⊳ G 0 and i ⊳ G 1 , join the results of both tests, and apply operator reduce afterwards. Note that the abstract test operator does not change the partition, thus this join boils down to applying the abstract join join N ♯ of numeric abstract domain N ♯ and set intersection to relations viewed as sets of atomic relations. The resulting join operator, limited to cases where both arguments have the same partitioning is defined by join ≡ ((p, -→ n 0 , r 0 ), (p,

-→ n 1 , r 1 )) = (p, join N ♯ ( -→ n 0 , - → n 1 ), r 0 ∩ r 1 ). It is sound: ∀i ∈ {0, 1}, γ D ♯ (p, -→ n i , r i ) ⊆ γ D ♯ (join ≡ ((p, -→ n 0 , r 0 ), (p, -→ n 1 , r 1 ))).
Abstract transfer function test is sound in the sense that:

∀σ ∈ γ D ♯ (a ♯ ), ex = TRUE =⇒ σ ∈ γ D ♯ (test(ex, a ♯ ))
Example 5. We consider the analysis of the code studied in Section 2. At the beginning of the first iteration of the loop, i is equal to 0, so mproc[i] may be in

G 1 or in G 2 .
Then, the analysis of test mproc[i].mpflag > 0 will locally create two disjuncts corresponding to each of these groups. However, in the case of G 1 , mpflag 1 = 0, thus the numeric test mpflag 1 > 0 will produce abstract value ⊥ denoting the empty set of states. Therefore, only the second disjunct contributes to the abstract post-condition. Thus, the analysis derives i ⊳ G 2 .

Assignment

Given l-value lv and expression ex, the concrete semantics of assignment lv = ex writes the value of ex into the cell lv evaluates to. It can thus be defined as a function over states, by lv = ex (σ) = σ[ lv (σ) ← ex (σ)].

In the abstract level, given abstract pre-condition a ♯ = (p, -→ n , r), an abstract post-condition for lv = ex can be done in three steps: (1) materialization of the memory cell that gets updated, (2) call to assign N ♯ in N ♯ [START_REF] Jeannet | Apron: A library of numerical abstract domains for static analysis[END_REF], and update of the relations, and (3) reduction of the resulting abstract state.

Materialization. When lv denotes an array cell, it should get materialized into a group consisting of a single cell, before strong updates can be performed on -→ n and r. To achieve this, the analysis computes which group(s) lv may evaluate into in abstract state a ♯ . If there is a single such group G i , that contains a single cell (i.e., Sz i = 1), then materialization is already achieved. If there is a single such group G i , but Sz i may be greater than 1, then the analysis calls split in order to divide G i into a group of size 1 and a group containing the other elements. Last, when there are several such groups (e.g., when lv is a[i] and i ⊳ G 0 ∪ G 1 ), the analysis first calls merge to merge all such groups and then falls back to the case where lv can only evaluate into a single group.

Note that in the last case, the merge of several groups may incur a loss in precision since the properties of several groups get merged before the abstract

G0 0 ≤ Idx 0 ≤ 99 G1 0 ≤ Idx 1 ≤ 99 n g : value0 = 0 ∧ Sz 0 = 99 ∧ value1 = 1 ∧ Sz 1 = 1 r : i ⊳ G1 ∧ value1 ⊳ G0 ∪ G1 Fig. 8. Post-condition of assignment a[i] = 1
assignment takes place. We believe this loss in precision is acceptable here. The other option would be to produce a disjunction of abstract states, yet it would increase significantly the analysis cost and the gain in precision would be unclear, as programmers typically view those disjunctions of groups of cells as having similar roles. Our experiments (Section 7) did confirm this observation.

Constraints. New relations can be inferred after assignment operations in two ways. First, when both sides are base variables, they get propagated: for instance, if u ⊳ G i , then after assignment v = u, we get v ⊳ G i . Second, when the right hand side is an array cell as in parent = mproc[child].mparent in the example of Section 2, the analysis first looks for relations between fields and indexes such as mparent 2 ⊳ G 0 ∪ G 2 , and propagate them to the l-value. In this phase, the numeric assignment relies on local disjuncts that are merged right after the abstract assignment, as we have shown in the case of condition tests (Section 5.1). The abstract transfer function for assignment is sound in the sense that:

∀σ ∈ γ D ♯ (a ♯ ), σ[ lv (σ) ← ex (σ)] ∈ γ D ♯ (assign(a ♯ , lv, ex))
Example 6. We consider a[i] = 1 and abstract the pre-condition shown in Figure 6(a). The l-value evaluates into an index in G 0 , but this group has several elements, thus it is split, as shown in Figure 6(b). Then, the assignment boils down to a strong update in G 1 , and produces the post-condition shown in Figure 8. Note that reduction strengthens relations with value 1 ⊳ G 0 ∪ G 1 .

Join, widening and inclusion check

Our analysis proceeds by standard abstract interpretation, and uses widening and inclusion tests to compute abstract post-fixpoints for loops and abstract join for control flow union (e.g., after an if statement). All these operators face the same difficulties: when their inputs do not have a similar of clearly "matching" groups they have to re-partition the arrays so that precise information can be computed. We discuss this issue in detail in the case of join.

Join and the group matching problem

Let us consider two abstract states a ♯ 0 , a ♯ 1 with the same number of groups for each array, that we assume to have the same names. Then, the operator join ≡ introduced in Section 5.1 computes an over-approximation for a ♯ 0 , a ♯ 1 , by joining

G0 0 ≤ Idx 0 ≤ 4 G1 1 ≤ Idx 1 ≤ 6 n g 0 : 2 ≤ value0 ≤ 8 ∧ -120 ≤ value1 ≤ -100 ∧ Sz 0 = 3 ∧ Sz 1 = 4 r0 : i ⊳ G0 (a) Abstract state a ♯ 0 G0 1 ≤ Idx 0 ≤ 6 G1 0 ≤ Idx 1 ≤ 4 n g 1 : -120 ≤ value0 ≤ -100 ∧ 2 ≤ value1 ≤ 8 ∧ Sz 0 = 4 ∧ Sz 1 = 3 r1 : i ⊳ G1 (b) Abstract state a ♯ 1 G0 0 ≤ Idx 0 ≤ 6 G1 0 ≤ Idx 1 ≤ 6 n g : -120 ≤ value0 ≤ 8 ∧ -120 ≤ value1 ≤ 8 ∧ 3 ≤ Sz 0 ≤ 4 ∧ 3 ≤ Sz 1 ≤ 4 r : true (c) Imprecise join result G0 1 ≤ Idx 0 ≤ 6 G1 0 ≤ Idx 1 ≤ 4 n g : -120 ≤ value0 ≤ -100 ∧ 2 ≤ value1 ≤ 8 ∧ Sz 0 = 4 ∧ Sz 1 = 3 r : i ⊳ G1
(d) Precise join result Fig. 9. Impact of the group matching on the abstract join predicates for each group name, the global numeric invariants and the side relations. However, this straightforward approach may produce very imprecise results if applied directly. As an example, we show two abstract states a ♯ 0 and a ♯ 1 in Figure 9(a) and Figure 9(b), that are similar up to a group name permutation. The direct join is shown in Figure 9(c). We note that the exact size of groups and the tight constraints over value were lost. Conversely, if the same operation is done after a permutation of group names, an optimal result is found, as shown in Figure 9(d). This group matching problem is actually even more complicated in general as a ♯ 0 , a ♯ 1 usually do not have the same number of groups. To properly associate G 0 in Figure 9(a) with G 1 in Figure 9(b), the analysis should take into account the group field properties. This is achieved with the help of a ranking function rank : G × G → N, which computes a distance between groups in different abstract states by comparing their properties: rank(G i , G j ) returns a monotone function of the number of common constraints over the fields and indexes of G i and G j in -→ n 0 and -→ n 1 . A high value of rank(G i , G j ) indicates G i of a ♯ 0 and G j of a ♯ 1 are likely to describe sets of cells with similar properties. Using the set of rank(G i , G j ) values, the analysis computes a pairing ↔, that is a relation between groups of a ♯ 0 and groups of a ♯ 1 (this step relies on heuristics; a non optimal pairing will impact only precision, but not soundness) and then apply a group matching which transforms both arguments into "compatible" abstract states using the following (symmetric) principles:

-if there is no G j such that G i ↔ G j , then an empty such group is created with create; -if G i ↔ G j and G i ↔ G k , then G i is split into two groups, respectively paired
with G j and G k ; -if G i is mapped only to G j , G j is mapped only to G i , and i = j, then one of them is renamed accordingly. After this process has completed, a pair of abstract states are produced that have the same number of groups, and join ≡ can be applied. This defines abstract join operator join. The soundness of join follows from the soundness of join ≡ (trivial), and the soundness of split and create:

0 : if (random()){ 1 : a[i] = 1; 2 : } 3 : . . . (a) Simple join G0 0 ≤ Idx 0 ≤ 99 G1 0 ≤ Idx 1 ≤ 99 n g : value0 = 0 ∧ value1 = 1 r : i ⊳ G0 ∪ G1 ∧ 99 ≤ Sz 0 ≤ 100 ∧ 0 ≤ Sz 1 ≤ 1 (b) Join result
Theorem 2 (Soundness). ∀a ♯ 0 , a ♯ 1 , γ D ♯ (a ♯ 0 ) ⊆ γ D ♯ (join(a ♯ 0 , a ♯ 1 )) ∧ γ D ♯ (a ♯ 1 ) ⊆ γ D ♯ (join(a ♯ 0 , a ♯ 1 )) Example 7.
We assume a is an integer array of length 100 and i is an integer variable storing a value in [0, 99], and consider the program of Figure 10(a). At the exit of the if statement, the analysis needs to join the abstract states shown in Figure 6(a) (that has a single group) and in Figure 8 (that has two groups). We note that G 0 in Figure 6(a) has similar properties as G 0 in Figure 8, thus they get paired. Moreover, G 1 in Figure 8 is paired to no group, so a new group is created (as in Figure 6(c), and paired to it. At that stage join ≡ applies, and returns the abstract state shown in Figure 10(b).

Widening

The widening algorithm is similar to that of join. The restriction of widening to compatible abstract states is defined by widen ≡ ((p, -→ n 0 , r 0 ), (p, -→ n 1 , r 1 )) = (p, widen N ♯ ( -→ n 0 , -→ n 1 ), r 0 ∩ r 1 ) (note that r 0 , r 1 are finite sets of relations, and intersections of finite sets of relations naturally terminates).

The group matching algorithm of Section 6.1 does not ensure termination, as it could create more and more groups. Therefore widen relies on a slightly modified group matching algorithm, which will never call split and create. Instead, it will always match each group of an argument to at least one group of the other argument, and call merge when two (or more) groups of one argument are paired with a group of the other. This group matching ensures termination. Therefore, the resulting widen operator is a sound and terminating widening operator [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF]. For better precision, the analysis always uses join for the first abstract iteration for a loop, and uses widening afterwards.

Inclusion check

To check the termination of sequences of abstract iterates over loops, and the entailment of post-conditions, the analysis uses a sound inclusion check operator is_le: when is_le(a ♯ 0 , a ♯ 1 ) returns TRUE, then γ D ♯ (a ♯ 0 ) ⊆ γ D ♯ (a ♯ 1 ). Like join, such an operator is easy to define on compatible abstract states, using an inclusion check operator is_le N ♯ for N ♯ : if is_le N ♯ ( -→ n 0 , -→ n 1 ) = TRUE and r 1 is included in r 0 (as a set of constraints), then γ D ♯ (p, -→ n 0 , r 0 ) ⊆ γ D ♯ (p, -→ n 1 , r 1 ), hence we let is_le ≡ return TRUE in that case.

The group matching algorithm for is_le is different, although it is based on similar principles. Indeed, it modifies the groups in the left argument so as to construct an abstract state with the same groups as the right argument, using create, split and merge.

Verification of the Minix Memory Management Process Table and experimental evaluation

We have implemented our analysis and evaluated how it copes with two classes of programs: (1) the Minix Memory Management Process Table, and ( 2) academic examples used in related works, where contiguity of groups is sometimes unnecessary for the verification. Our analyzer uses the MemCAD analyzer front-end, and the Apron [14] implementation of octagons [START_REF] Miné | The octagon abstract domain[END_REF].

Verification of memory management part in Minix

The main data-structure of the Memory Management operating system service of Minix 1.1 is the MMPT mproc, which contains memory management information for each process. At start up, it is initialized by function mm_init, which creates process descriptors for mm, fs and init. After that, mproc should satisfy property C (Section 2). Then, it gets updated by system calls fork, wait and exit, which respectively create a process, wait for terminated children process descriptors be removed, and terminate a process. Each of these functions should be called only in a state that satisfies C, and should return a state that also satisfies C. System calls wait and exit call the complex utility function cleanup discussed in Section 2, to reclaim descriptors of terminated processes. If property C was violated, several critical issues could occur. First, system calls could crash due to out-of-bound accesses, e.g., when accessing mproc through field mparent. Moreover, higher level, hard to debug issues could occur, such as the persistence of dangling processes, that would never be eliminated.

Therefore, we verified (1) that mm_init properly establishes C (with no precondition), and (2) that fork, wait and exit preserve C using our analysis (i.e., the analysis of each of these functions from pre-condition C returns a post-condition that also satisfies C). Note that function cleanup was inlined in wait and fork in a recursion free form (currently not supported by our analyzer), as well as statements irrelevant to mproc. Our tool achieves the verification of all these four functions. The results are shown in the first four lines of the table in Figure 11, including analysis time and peak number of groups for array mproc.

The analysis of mm_init and fork is very fast. The analysis of exit and wait also succeeds, although it is more complex due to the intricate structure of cleanup (which consists of five loops and many conditions) which requires 194 joins. Despite this, the maximum number of groups remains reasonable (seven in the worst case).

Application on other cases

We now consider a couple of examples from the literature, where arrays are used as containers, i.e., where the relative order of groups does not matter for the program's correctness. The purpose of this study is to examplify other examples of cases our abstract domain is adequate for. Program int_init consists of a simple initialization loop. Our analysis succeeds here, and can handle other cases relying on basic segments, although our algorithms are not specific to segments (and are geared towards the abstraction of non contiguous partitions). Moreover, Figure 12 shows complex, an excerpt of an example from [START_REF] Cousot | A parametric segmentation functor for fully automatic and scalable array content analysis[END_REF]. The second example is challenging for most existing techniques, as observed in [START_REF] Cousot | A parametric segmentation functor for fully automatic and scalable array content analysis[END_REF] since resolving a[index] at line 10 is tricky. As shown in Figure 11, our analysis handles these two loops well, with respectively 4 and 3 groups.

The invariant of the first initialization loop in Figure 12 is abstract state 1 (at line 4): group G 1 accounts for initialized cells, whereas cells of G 0 remain to be initialized. The analysis of a[i] = 0; from 1 materializes a single uninitialized cell, so that a strong update produces abstract state 2 . At the next iteration, and after increment operation i++, widening merges G 2 with G 1 , which produces abstract state 1 again. At loop exit, the analysis derives G 0 is empty as 56 ≤ Idx 0 ≤ 55. At this stage, this group is eliminated. The analysis of the second loop converges after two widening iterations, and produces abstract state 3 . We note that group G 3 is kept separate, while groups G 1 and G 2 get merged when the assignment at line 10 is analyzed (Section 5.2). This allows to prove the assertion at line 11.

Related work and conclusion

In this paper, we have presented a novel abstract domain that is tailored for arrays, and that relies on partitioning, without imposing the constraint that the cells of a given group be contiguous.

Most array analyses require each group be a contiguous array segment. This view is used both in abstract interpretation based static analysis tools [START_REF] Cousot | A parametric segmentation functor for fully automatic and scalable array content analysis[END_REF][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] and in tools based on invariant generation, model checking and theorem proving [START_REF] Alberti | Decision procedures for flat array properties[END_REF][START_REF] Jhala | Array abstraction from proofs[END_REF][START_REF] Kovac | Finding loop invariants for programs over array using a theorem prover[END_REF][START_REF] Mcmillan | Quantified invariant generation using an interpolation saturation prover[END_REF][START_REF] Seghir | Abstraction refinement for quantified array assertions[END_REF]. We believe that both approaches are adequate for different sets of problems: segment based approaches are adequate to verify algorithms that use array to order elements, such as sorting algorithms, while our segmentless approach works better to verify programs that use arrays as dictionaries.

Other works target dictionary structures and summarize non contiguous sets of cells, that are not necessarily part of arrays. In particular, [START_REF] Dillig | Fluid updates: Beyond strong vs. weak updates[END_REF][START_REF] Dillig | Precise reasoning for programs using containers[END_REF] seeks for a unified way to reason about pointers, scalars and arrays. These works are orthogonal to our approach, as we strive to use properties specific to arrays in order to reason about the structure of groups. Therefore, [START_REF] Dillig | Fluid updates: Beyond strong vs. weak updates[END_REF][START_REF] Dillig | Precise reasoning for programs using containers[END_REF] cannot express the invariants presented in Section 2 for two reasons: (1) the access paths cannot describe the contents of array elements as an interval or with other numeric constraints; (2) they cannot express content-index predicates. Similarly, HOO [START_REF] Cox | Automatic analysis of open objects in dynamic language programs[END_REF] is an effective abstract domain for containers and JavaScript open objects. As it uses a set abstract domain [START_REF] Cox | Quic graphs: Relational invariant generation for containers[END_REF], it has a very general scope but does not exploit the structure of arrays, hence would sacrifice efficiency in such cases.

Last, template-base methods [START_REF] Beyer | Invariant synthesis for combined theories[END_REF][START_REF] Gulwani | Lifting abstract interpreters to quantified logical domains[END_REF] are very powerful invariant generation techniques, yet require user supplied templates and can be quite costly.

Our approach has several key distinguishing factors. First, it not only relies on index relation, but also exploits semantic properties of array elements, to select groups. Second, relation predicates track lightweight properties, that would not be captured in a numerical domain. Last, it allows empty groups, which eliminated the need for any global disjunction in our examples (a few assignments and tests benefit from cheap, local disjunctions). Finally, experiments show it is effective at inferring non trivial array invariants with non contiguous groups, and verify a challenging operating system data-structure.

Figure 1 (

 1 c) depicts the concrete values stored in mproc to describe the process topology shown in Figure 1(b) (we show only 8 processes). An element 1 struct mproc { 2 unsigned mpflag; 3 int mparent; 4. } mproc[24]; (a) Definition of array mproc

Fig. 1 .

 1 Fig. 1. Minix 1.1 Memory Management Process Table (MMPT) structure

  Fig. 3. Minix 1.1 process table management, system function cleanup

Fig. 4 .

 4 Fig. 4. Overview of the analysis of cleanup

Fig. 5 .

 5 Fig. 5. An abstraction in our domain

  Figure 5(b) shows an abstraction a ♯ = (p, -→ n ) into two groups G 0 , G 1 , where G 0 (resp., G 1 ) contains all cells storing a positive (resp., negative) values. This abstraction reveals the array stores no value in [-99, 1].

Fig. 10 .

 10 Fig.10. Join of a one group state with a two groups state

2 2 } 5 a 3 7 2 G0i + 1 ≤G1 0 ≤ 1 G2Idx 2

 25321012 int a[56]; 3 for(int i = 0; i < 56; i++){ [55] = random(); 6 for(int i = 0; i < 55; i++){ int index = 21 * i%55;8 int num = random(); 9 if (num < 0){num = -1; } 10 a[index] = num; } 11 assert(∀i ∈ [0, 54], a[i] ≥ -1); (a) Test case complex state 1 G0 i ≤ Idx 0 ≤ 55 G1 0 ≤ Idx 1 ≤ i -1 n g : Sz 0 = 56i ∧ Sz 1 = i ∧ value1 = 0 r : i ⊳ G0 state Idx 0 ≤ 55 Idx 1 ≤ i -= i n g : Sz 0 = 55i ∧ Sz 1 = i ∧ Sz 2 = 1 value1 = 0 ∧ value2 = 0 r : i ⊳ G2 state 3 G1 0 ≤ Idx 1 ≤ 54 G2 0 ≤ Idx 2 ≤ 54 G3 Idx 3 = 55 n g : Sz 1 = 54 ∧ Sz 2 = 1 ∧ Sz 3 = 1 -1 ≤ value1 ∧ -1 ≤ value2 r : i ⊳ G1 ∪ G2 (b) Invariants

Fig. 12 .

 12 Fig. 12. Array random accesses

  1 Memory Management Process Table (MMPT) and other challenging array examples (Section 7).

	G2 = {0, 1, 3, 4, 6, . . .}	G0 = {2}
	0	mm		2 init
	1	fs	4 usr0	3 usr1
	6 usr2	5 free	7 free
			G1 = {5, 7, . . .}

  3. Minix 1.1 process table management, system function cleanup

(corresponding to process init). Combining this, with the fact that group 0 has exactly one element (Sz 0 = 1) at index 2 (Idx 0 = 2), the analysis infers that parent can only be in group 0 (point 2 ). Therefore, the update at point 2 affects a group with a single element, hence, is a strong update, and produces predicate at point

. However, at that point, the next update is not strong, since mproc[child] may be any element of group 2, which may have more than one element (it has at least one element since child ⊳ G 2 , thus Sz 2 ≥ 1). Therefore, our domain materializes the array element being assigned by splitting group 2 into two groups, labeled 2 and 3. Both groups inherit predicates from former group 2. Additionally,

⋆ The research leading to these results has received funding from the European Research Council under the FP7 grant agreement 278673, Project MemCAD, and from the ARTEMIS Joint Undertaking no 269335 (see Article II.9 of the JU Grant Agreement).