Static analysis of a program allows to predict the properties of its executions without actually executing the program. Abstract interpretation provides the mathematical theory to design such analysis. In particular, it helps design relational analyses, which keep track of the relations between variables. These analyses are costly because they usually require computations at every program points (they are flow-sensitive). To reduce these computations, we design a flow insensitive static analysis that can provide a relational invariant on the variables. This invariant is global, there is only one for the program analysed, but it must have the same precision as if we used a flow-sensitive one. A specific representation of the program, namely the Static Single Information (SSI) form, allows us to preserve precision thanks to the indexing of the variables. This report presents the concepts of abstract interpretation and the SSI form then details the designed analysis, ensuring its soundness at each step.

Remark The Section 2 is a recap from the bibliographic study. We added the Definition 2.4 of a semilattice and the Theorem 2.2 of transfer fixpoint. In Section 2.1.2 we formalized the semantics of a program using the equational approach rather than the denotational semantics we used to present, as it is the approach we choose for our analysis. This Section also introduces partial functions for environments and handy operations on them, such as projection on a set of variables. Finally, the presentation of the intermediate representations has been developed, in particular the SSI form.

Introduction

It is mandatory to properly check the behaviour of a critical software before running it, when an error can have disastrous results, such as putting lives at risk. This is what we call program verification. Its purpose is to prevent any "bad" behaviour of a program. The guarantees provided should be stronger than tests, that can only explore part of all the possible executions. As Dijkstra said, if a test can prove the existence of a bug, it cannot prove its absence [START_REF] Edsger | On the reliability of programs[END_REF].

Automatic verification can take several forms, such as static analysis or model checking. The latter needs to have a model of the program and a specification that we want to satisfy. Model checking [START_REF] Baier | Principles of model checking[END_REF] refers to the tools and techniques to ensure that the model complies with the specification. Static analysis, on the other hand, performs the analysis directly on the code, not on a model. But this analysis is necessarily limited: it has been proved by Rice in 1951 that the properties of a program cannot be inferred in general from its code alone (unless the property is trivial, that is always true or false). Properties can be for example "the program terminates" or "the final value of X is twice the initial value of Y".

To ascertain whether such a property holds on a program requires explaining what the program actually does. This is what we call the semantics of the program. It is not possible to design an algorithm that automatically computes the complete semantics of any program. In other words, it is not possible to compute all possible executions of any program. Analyzers thus rely on an approximate abstract semantics of the program that is computable. We call the complete, uncomputable semantics the concrete semantics. The link between the two semantics must be properly expressed.

The abstract semantics can claim a wide variety of properties. Most common ones include asserting the safety of a program, asserting the absence of undefined behaviour or bugs. Because of the approximation, there can be false alarms (Figure 1): the analysis reports a property violation, while it cannot happen in the concrete semantics. A precise analysis will report few false alarms. However, for safety properties, we want a sound analysis, where no alarm is silent: if the analysis asserts that all properties are satisfied, then in the concrete semantics it must also be the case. This corresponds to an overapproximation of all possible execution paths.

Abstract interpretation is a framework used to design static analyses. It defines a generic formalization of such analyses, and provides proofs on the guarantees they claim. More precisely, it helps defining the abstract domain (what properties one can express) of the abstract semantics, and how the analysis is performed on the program (the algorithm to compute the properties).

The domains of abstract interpretation will usually approximate the state of the variables, that is for each variable or expression depending on them, approximates its value. The goal is to have numerical invariants of these variables. The domains chosen for the variables are often classified into two categories: relational and non-relational domains. A relational domain allows inferring comparisons between the variables of the program, for instance X -Y < 2, while a non-relational one only allows comparison to constants (X < 2 ∧ Y = 3).

Choosing the best abstraction for a given problem is not trivial. Typically, increasing the precision of an abstraction will lead in a higher memory and time consumption.

Besides the domain, the algorithm computing it calls for reflection too. Textbook abstract interpretation algorithms compute the abstract state at each program points. It can be done by induction on the syntax (denotational semantics) or by a system of equations to solve. Such dense computation is heavy in memory or computation time. We would like to perform sparser analyses, that would not have one abstract state per program point. The less abstract states are kept, the The approximation of the executions must at least cover the concrete executions. In case of intersection between the forbidden executions and the approximation, an alarm is raised sparser the analysis is. This sparsity should not however deteriorate the precision of the analysis. Less dense analyses that are sill precise were made using a specific representation of the program: the Single Static Assignment (SSA). This representation allows to have distinct versions of each variable. Thanks to that, one abstract state can represent the variable at several program point.

With this internship we want to reach the sparsest analysis with only one invariant for the whole program. Our idea is to use the Single Static Information (SSI) form that introduces even more distinct versions for each variable. It can be used to make non-relational sparse analysis, but there is no guarantee that it can help design a relational sparse analysis with a decent precision and efficiency (adding new versions for each variable has a cost). Designing the sparse relational analysis and ensuring its correctness is the main goal of this internship. Evaluating its precision and efficiency is an ongoing work.

Outline The main principles of abstract interpretation are introduced in Section 2.1. Section 2.2 presents the SSA and SSI forms and their interesting properties to build sparse analyses. Finally, Section 2. [START_REF] Baier | Principles of model checking[END_REF] gives some examples of relational analyses taking advantage of intermediate representations and abstract interpretation. In Section 3 we develop the core of the internship: the building of a sparse, flow insensitive analysis. We first give the concrete semantics of the SSI form in Section 3.1. Then, in Section 3.2, we detail the abstract domain we used. Indeed, our will to build a global invariant imposes that we craft a specific abstract domain to maintain precision. The abstract semantics, which is the core of the analysis, is given in Section 3.3. The proof of correctness of this analysis is detailed in this section. A quick look at an OCaml prototype is provided at the end, in Section 3.4. Section 4 summarizes our approach to design a sparse, flow-insensitive analysis and the pros and cons of it.

For instance, for any set of elements S, the set of its parts, P(S) with the inclusion partial order ⊆ is a poset.

In a poset (X, ), an upper bound of two elements a, b ∈ X is defined as any element c ∈ X such that a c and b c. A lower bound is defined similarly by c a and c b. If c is the smallest upper bound, it is called the least upper bound, or join, and is noted c = a b. Similarly, we define the greatest lower bound, or meet, noted c = a b.

In (P(S), ⊆), the join is the union ∪ and the meet is the intersection ∩.

A convenient way of representing a poset is by using a Hasse diagram. In such a diagram, elements of X are nodes organized such that the greater elements are higher. Order relation are represented by edges between elements. The one obtained by reflexivity and transitivity are omitted. Figure 2 pictures several examples of Hasse diagrams.

In abstract interpretation, elements of a poset will often represent the properties about values of variables. For instance, consider the sign poset of Figure 2c. Let us suppose we want to know the sign of some variable x after a branching. Our variable is equal to zero in the first branch and strictly inferior to zero in the other one. At the join point, the variable will be associated to the element (= 0) (< 0) = (≤ 0) of the poset. Now suppose we have a condition x < 0 to enter a branch. Then in the branch we will associate the value of x to the element (≤ 0) (< 0) = (< 0) in the poset. Poset may not be enough in this case, as we want to be able to compute the join or meet of any two elements. A lattice is then preferred.

Definition 2.2. [Lattice]

A lattice (X, , , ) is a poset such that for every two elements of X, the least upper bound and the greatest lower bound are defined.

The definition of join and meet can be extended to a set of elements A ⊆ X, and are then noted A and A. Notice that this set A can be infinite.

If it exists, the least element X is denoted ⊥, called bottom. The greatest element X is denoted , called top, if it exists. Definition 2.3. [Complete lattice] A complete lattice (X, , , , ⊥, ) is a poset such that for any subset of X (even infinite ones), the least upper bound and the greatest lower bound are defined.

Notice that ⊥ = ∅. In a complete lattice both and ⊥ always exist. Figures 2b and2c both represent complete lattices, while Figure 2a is not as it does not have an upper element .

Complete lattices offer convenient properties for soundness but it is not always possible to define a join or a meet for any subset of our poset. Posets which can define them only on non-empty finite subset are called semilattices.

Definition 2.4. [Semilattice]

A join-semilattice is a poset were the join is defined for any non-empty finite subset. Dually, a meet-semilattice is a poset were the meet is defined for any non-empty finite subset.

Fixpoints

As soon as a language includes loops, the analysis needs to build a loop invariant, holding before entering the loop and after each iteration, upon reentering the body. This invariant corresponds to a fixpoint.

For a function f : X → X, called an operator, a fixpoint is any point x ∈ X such that f (x) = x. What the function f is exactly in the case of static analysis will be precised in the next subsection.

In poset, we can identify more elements related to fixpoints: Definition 2.5.

[Fixpoints] Given a poset (X, ) and an operator f :

X → X • x is a postfixpoint of f if f (x) x • lfp(f ) = min{x ∈ X|f (x) = x}, if it exists, is the least fixpoint of f .
In the semantics, the least fixpoint will represent the tightest invariant. Tarski's theorem ensures its existence in complete lattices and expresses it as the least postfixpoint.

Theorem 2.1. [Tarski's Theorem] If f : X → X is a monotonic operator in a complete lattice (X, , , , ⊥, ), then the set of fixpoints of f is a non-empty complete lattice. In particular, lfpf = {x ∈ X, f (x) x} exists.

Approximations

In abstract interpretation we use the posets to rank information. For static analysis, the common information collected includes the values of variables or the possibles states of the system at some program points. Partial order are helpful to compare, to join and to restrict this information. Higher elements represent less precise information, as they represent the union of information. In the concrete world, the properties of variables are elements of some poset (C, ≤). It is quite common to use (P(Z), ⊆) as a poset for concrete values: an element represents the exact set of values a variable can hold. Another poset (A, ) is used for the abstract representation. For instance, elements of A can be intervals.

These two posets must be linked at least through the concretization function, noted γ. The abstract domain must overapproximates the concrete world, so that no possible execution can be ignored. This overapproximation property, which we referred as soundness, can be formalized.

Definition 2.7. [Soundness] a ∈ A is a sound approximation of c ∈ C if and only if c ≤ γ(a). It is exact in case of equality.
As we will see in the next subsection, fixpoints are essential for the analysis. But the approximation chosen may not satisfy the condition of Tarski's theorem of being a complete lattice. In our case, the abstract domain is only a meet-semilattice. Luckily, the Tarskian fixpoint approximation theorem, also referred as the fixpoint transfer theorem, asserts that the postfixpoints in the abstract world are sound approximations of the least fixpoints. Proof. Let us consider a post-fixpoint

. If X ∈ A is a post-fixpoint of F , that is F (X) X, then having F • γ ⊆ γ • F is enough to guarantee that lfp(F ) ⊆ γ(X). stmt : : = V ← expr (assignment, V ∈ V) | assert ( cond ) (
X ∈ A. γ is monotonic, that is A B implies γ(A) ⊆ γ(B).
So by applying γ on the post-fixpoint relation

F (X) X, we get that γ • F (X) ⊆ γ(X). Also, let us suppose that F • γ ⊆ γ • F . Then F • γ(X) ⊆ γ • F (X) ⊆ γ(X).
So γ(X) is a post-fixpoint of F . By Tarski's theorem, the least fixpoint of F is equal to the meet of all post-fixpoints, which is equivalent to saying that lfp(F ) is lower (in the lattice) than any post-fixpoint. Thus lfp(F ) ⊆ γ(X).

Finally, we do not have guarantees that this (post-)fixpoint is computable in a finite time, and even though, we would like to reach it fast. To accelerate convergence toward a fixpoint, Cousot and Cousot introduced the widening operator ∇ [START_REF] Cousot | Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF]. In this original definition, this binary operator must ensure that a sequence s 0 = X 0 , s 1 = s 0 ∇X 1 , . . . s n = s n-1 ∇X n . . . , where X i are arbitrary values, is not strictly increasing. The operator must also be an overapproximation of its arguments. In practice and in more recent works, the definition of the widening operator has been simplified and the first condition is that any sequence X n+1 = X 0 ∇X n will converge in finite time [START_REF] Miné | Tutorial on static inference of numeric invariants by abstract interpretation[END_REF].

Concrete and abstract semantics of programs

The semantics of a program is the mathematical meaning associated to it. It can be the final value returned by the program, the values of its variables or even whether it terminates or not. Here we will illustrate two approaches to present semantics using a simple imperative language called the While language. Its syntax is presented in Figure 3. The atomic statements are the variable assignment, the assertion and the skip instructions. Statements are composed with the sequence, the conditional or the while loop. The syntax of expressions and conditionals is not detailed here. Arithmetic expressions include constants, variables and binary operations. Conditionals include boolean constants, arithmetic comparisons and logical conjunction and disjunction. This is a quite common language and we will not detail it more here.

Let us first start with the concrete semantics. It is the most precise representation of the program behavior. If we could compute it, it would correspond exactly to the actual executions of the program. Alas, this is not possible due to Rice's theorem. Nonetheless, it is possible to express it mathematically. Here, we are interested into numerical invariants, we want to know the possible values of each variable or expression of the program. What we call the concrete semantic of the program will thus be a map from each program point ∈ L to a set of memory states. In Miné's tutorial [START_REF] Miné | Tutorial on static inference of numeric invariants by abstract interpretation[END_REF], the memory states are total functions from the variables V to the domain of value I (= R, Z, N, . . . ). But for our work, to be able to express that a variable is not defined, we manipulate partial functions instead.

Definition 2.8. [Partial function] A partial function from

A to B if a function from A to B where A is a subset of A. It is noted f : A B. Its domain of definition A is noted dom(f ) ⊆ A.
From this point we will use the term domain for the domain of definition.

A partial function can be represented as its set of associations. For instance let f be a partial function such that dom(f ) = {a 1 , a 2 , . . . , a k } ⊆ A, and for all

i ∈ [1, k], f (a i ) = b i ∈ B, then f can be noted f = {a 1 → b 1 , . . . a k → b k }. Given a function f , the function g = f [a → b]
is the updated version of f . It evaluates to b for a and for any x = a in the domain of f , it evaluates to f (x). We have that dom(g) = dom(f ) ∪ {a}, g(a) = b and for any c ∈ dom(f ), c = a =⇒ g(c) = f (c). In some cases, we will need to have a restricted version of a partial function where some variables have been forgotten.

Definition 2.9. [Restriction] Let f ∈ A B be a partial function and A ⊆ dom(f ), the restricted partial function f | A is defined such that dom(f | A ) = A and for all a ∈ A , f | A (a) = f (a).
Environment Let V be the set of variables in the program, I the set of values these variables can be assigned to. An environment is a partial function s : V I. The domain of s is the set of defined variables in s.

E def = V
I is the set of environments. The framework for abstract interpretation presented by Miné [START_REF] Miné | Tutorial on static inference of numeric invariants by abstract interpretation[END_REF] and the one of Cousot [START_REF] Cousot | Systematic design of program analysis frameworks[END_REF] both use total functions to represent environment. In this mindset, a variable that has not been assigned a value yet can have any value.

Projection Concrete and abstract domains for numerical invariants can be provided with an existential projection operator, noted proj and proj . The existential projection of some value S onto a set of variables V consists in forgetting all the variables of V that do not belong to V . In the concrete domains, this means that any concrete environment s of the projection of S is equal to a concrete environment of S restricted to V :

proj V (S) = s s ∈ S, s | V = s | V
The abstract projection should overapproximate the concrete one:

proj V •γ(S) ⊆ γ • proj V (S)
It is exact in case of equality. We require that for any abstract value S and set of variables V :

S proj V (S)
Invariant The concrete semantics computes an invariant I : L → P (E) of the program, it associates to each program point the set of environments possible at this point during the execution of the program. Notice that the domain P (E) can be organized as a complete lattice: (P (E) , ⊆, ∪, ∩, ∅, E). There are two approaches to define this invariant: the denotational-style semantics and the equational-based semantics. While in the denotational-style we compute invariants inductively on the syntax of statements, an equational-based semantics will rely on a system of equations to determine the environments possible at each program points. We will only detail the latter. It is computed for the control-flow graph of the program.

Control-flow graph

We define the set of program points L where we will compute the invariant. The control-flow graph (CFG) of the program is a graph where each node is a program point ∈ L, and each edge corresponds to an atomic instruction.

Atomic instruction An atomic instruction is either an assignment [x ← e] or an arithmetic condition [e 1 e 2 ] ( ∈ {=, <, ≤}). The set of variables used in an expression e is noted vars(e). Sometimes, we do not specify any instruction on an edge, and instead put the identity function id.

It is semantically equivalent to put an arithmetic condition always true such as [0 = 0].

CFG The CFG can be build inductively on the syntax of a program.

cfg[ 1 skip 2 ] def = {( 1 , id, 2 )} (1) cfg[ 1 x ← e 2 ] def = {( 1 , [x ← e], 2 )} (2) cfg[ 1 assert (c) 2 ] def = {( 1 , id, 2 )} (3) cfg[ 1 s 1 ; 2 s 2 3 ] def = cfg[ 1 s 1 2 ] ∪ cfg[ 2 s 2 3 ] (4) cfg[ 1 if c then 2 s 1 3 else 4 s 2 5 endif 6 ] def = {( 1 , [c], 2 ), ( 1 , [¬c], 4 ), ( 3 , id, 6 ), ( 5 , id, 6 )} ∪ cfg[ 2 s 1 3 ] ∪ cfg[ 4 s 2 5 ] (5)
cfg[ 1 while 2 c do 3 body 4 done 5 ] def = {( 1 , id, 2 ), ( 2 , [c], 3 ), ( 3 , id, 2 ), ( 2 , [¬c], 5 )} ∪ cfg[ 3 body 4 ] (6)
Figure 4 pictures the CFG of a program in the While language.

Equational semantics

The invariant of each program point is built by applying the effect of the incoming edges onto the environments of predecessor program points1 . The effect of the incoming is actually the semantics of the atomic instruction attached to the edge in the CFG. Let us define the semantics of expressions first, then the one of atomic expressions.

Semantics of expressions

The semantics of an expression e is a function E e : E → P (I) that outputs all possible evaluations of the expression given an environment. Such semantics allows undeterminism, for instance the expression [0, 20] has the semantics {v ∈ I|0 ≤ v ≤ 20} and [-∞, +∞] has the semantics I. The semantics is defined inductively on the syntax of the expression, with rules such as

E n s = {n} if n is a constant, E x s = {s(x)} if x ∈ dom(s), else E x s = ∅.
Let vars(e) be the variables appearing in the expression e. Then if s is not defined over vars(e), then the set outputted by the semantics is empty. i := 1 ; j := 0 ; while ( j < 1 0 ) do i := i + 1 ; j := j + 1 ; assert ( i = j + 1 ) done ; assert ( i = 1 1 ) (a) An example of program in the while language, with assertions Semantics of atomic instructions The semantics of assignment, S • , and arithmetic condition, C • are both functions from a set of environments to another one. In the case of assignment, the semantics outputs the environments of the input updated with the new value for x. As for condition, it filters the environments in the input that satisfy the test.

0 1 i ← 1 2 j ← 0 3 j < 10 4 i ← i + 1 5 j ← j + 1 6 (i = j + 1)

S x ← e :

P (E) → P (E)

S → {s[x → v]|s ∈ S, v ∈ E e s}
C e 1 e 2 : P (E) → P (E)

S → {s|s ∈ S, v 1 ∈ E e 1 s, v 2 ∈ E e 2 s, v 1 v 2 }
Given some atomic instruction a, we note a its corresponding semantics, that is either S a if a is an assignment or C a if it is an arithmetic condition.

For example, let us start with the environment ρ = {x → 3} ∈ E, that is the environment associating x with 3. Then the semantics of the expression x + 2 is defined inductively on the syntax:

E x + 2 ρ = {v 1 + v 2 |v 1 ∈ E x ρ, v 2 ∈ E 2 ρ} = {v 1 + 2|v 1 ∈ ρ(x)} = {3 + 2} = {5}
For a condition, such as x + 2 > 0, with R as the input set of environments.

C x + 2 > 0 R = {ρ|ρ ∈ R, v 1 ∈ E x + 2 ρ, v 2 ∈ E 0 ρ, v 1 > v 2 } = {ρ|ρ ∈ R, v ∈ ρ(x), v + 2 > 0}
These semantics are monotonic functions.

Remark Notice that for all s ∈ C e 1 e 2 then s is defined over the variables of e 1 and the ones of e 2 .

Equational system For each program point, the set of environments possible is the union of the environments of the predecessors, where the semantics of the edge has been applied. The entry point is a special case: having no predecessors, its set of environments is composed of all partial functions where the arguments of the program are associated to any value. Let S 0 be the set of such states, a 1 , . . . , a n be the argument of the program.

S 0 def = i 1 ,...,in∈I n {a 1 → i 1 , . . . , a n → i n }
The equational system defines for each program point its set of memory state X . The equational system of the program is thus:

∀ ∈ L, X = S 0 if is an entry point ( ,a, )∈CF G a (X )
Definition 2.10. We say that a pair (s, ) is a reachable state if s is in X .

Solution This system of equations always has a smallest solution with respect to the order ⊆. If we consider the vector of invariants X def = (X 1 , . . . , X |L| ) ∈ P (E) |L| , then the system of equations can be seen as the fixpoint of some function F such that X = F ( X ). P (E) |L| is organized on a complete lattice, and one can show that the semantic functions for atomic instructions are monotonic in P (E), which induces that F is monotonic in P (E) |L| . Therefore, Tarski's fixpoint theorem ensures the existence of the least fixpoint for F .

The equational semantics needs to keep in memory the environments at each program points, which can have a dreadful impact on memory consumption. On the other hand, the denotational semantics is defined inductively on the syntax. It does not memorize previous results, the environments at each program points. But in consequence it may spend time into re-exploring statements, for instance in the case of nested loops Abstract semantics Abstract semantics also can be defined with one of these two styles. The difference is the domain: instead of a set of environments in P (E), semantics are defined for an abstract domain D, usually organized on a complete lattice. When D is not organized on a complete lattice, we can still use the transfer theorem 2.2 to ensure the soundness of our analysis. It is possible to have a relaxed framework for such cases. All domains and semantics referring to the abstraction are traditionally noted with a : S • , C • , . . . We do not have guarantee on the monotonicity of the abstract semantics.

The system of equation for the abstract semantics can be solved with different algorithms, one of them being the chaotic iteration introduced by Cousot and Cousot in 1977.

Abstract domains for numeric invariants

Concrete numeric invariants are usually comprehensive representations of the program states. These invariants are possibly infinite sets of values or relations. They are not computable in the general case nor representable in a machine. An abstract domain approximates sets of invariants, so that they are representable and computable. This section presents several classical abstract domains. Some of these domains are illustrated in Figure 5. We consider an analysis that keeps track of two variables x and y. Each dot on the figures corresponds to a concrete state of the program. The gray areas correspond to the sets of states approximated by the different domains.

Non-relational abstract domains refer to domains where relations (comparison) between variables are forgotten. This includes the sign domain, the constant and constant set domains, the interval domain and finally the congruence domain. In this last numeric domains, each variable is associated to an invariant.

Interval domain This is a very common domain, which associates to each variable an interval, with possibly infinite bounds, in 5a illustrates the shape of the representation. In this domain, x is associated to the interval [START_REF] Alpern | Detecting equality of variables in programs[END_REF][START_REF] Cousot | Systematic design of program analysis frameworks[END_REF] and y to [-2, 5]. It is sometimes also referred as the box domain, given its shape in a 3-variables space.

{[a, b]|a ∈ I ∪ -∞, b ∈ I ∪ +∞, a ≤ b}. Figure
Congruence domain This representation can be useful for loop analysis where the step increment is different from one. It associates to each variable the abstraction aZ + b, meaning the variable is equal to a multiple of a plus b (a and b being constants). The shape is given on Figure 5b, with the same concrete states as before. Only the domain of x is pictured. It is 2Z + 1.

Non-relational domains might not be precise enough. Relations between variables can be useful to deduce if a test x < y holds or not. Which relations are kept is up to choice, but the most common domains are the octagon and polyhedra ones.

Octagon domain This domain keeps relations of the form ±x ± y ≤ c where c is a constant or +∞. It besides adds an artificial variable v 0 , always equal to zero, so that the octagon domain include intervals: 5c pictures the shape of the domain. For instance, the relation -x -y ≤ -1 holds in this example. It defines the lower-left side of the octagon. In a two-variables space, the domain is a polygon with at most eight sides, hence the name octagon.

x ∈ [a, b] is equivalent to x -v 0 ≤ b and v 0 -x ≤ -a. Figure
Polyhedra domain To extend the type of relations tracked, the polyhedra domain represents any affine inequalities between variables. Such inequalities are of the form a 1 x + a 2 y + • • • ≥ b where a 1 , a 2 , . . . and b are constants in I. Figure 5d pictures the shape of this new representation. It is the most precise seen here. This precision however comes with a cost in memory and computation time when update is needed.

Choosing the most adapted domain clearly depends on the analysis performed. For instance, the Astrée analyzer [START_REF] Cousot | The ASTRÉE analyzer[END_REF], which aimed at synchronous programs in the realm of aviation, uses specific domains such as the non-relational Arithmetic-Geometric Progression abstract domain and the Clock domain. This analyzer actually combines several domains to achieve the precision wanted. For relations, it does not use the polyhedra domain but the octagon one. Although it is less precise, it is sufficient combined with other domains while being lighter in term of analysis runtime efficiency.

Intermediate Representations for numerical static analysis

An intermediate representation of a program is a representation of a program that respects useful properties for analysis or compilation purposes. This representation should keep the semantics of the original program. Besides the useful properties, the intermediate representation is also convenient to design one analysis that can perform on several languages, as long as there exists a front-end from the language to the intermediate form. For instance, the LLVM compiler uses the SSA form as an intermediate representation for its analyses, but has front-end for languages such as C, C++ or Java. In our case, we will design our analysis on the Static Single Information (SSI) form, as its properties allow flow-insensitivity in the case of non-relational analyses. We hope to be flow-insensitive for relational analyses thanks to this representation. Any language that can be transformed into this SSI form can thus be analysed.

But the SSI form is the results of an incremental construction of intermediate representation with the Static Single Assignment (SSA) form being a milestone. Thus we will first see the SSA form, then complete it with a new operator to get the SSI form.

These two representations targets a similar goal: make explicit in the code the def-use or the use-def chains. A def-use chain associates to each definition of a variable, the instruction that may use it. In other word, if a variable is defined at instruction and is used at instruction then → is in the def-use chain if there exists a path from to such that no instruction on this path re-defines the variable. Conversely, → is in the use-def chain if the variable used at may have been defined at . (That is there is a path from to such that the variable is not re-defined.) To do so, the analyses split the live-range of the variables. The live-range is the set of program points where the variable is alive (it is defined and may be used in a successor).

0 1 2 3 4 x > 0 x ≤ 0 x ← 2 x ← 3 y ← x + 1 (a) Original program 0 1 2 x 3 φ ← (x 1 , x 2 ) 3 4 x 0 > 0 x 0 ≤ 0 x 1 ← 2 x 2 ← 3 y ← x 3 + 1 (b) Program in SSA form 0 1 2 1 2 3 4 x 0 > 0 x 0 ≤ 0 x 1 ← 2 x 3 ← x 1 x 2 ← 3 x 3 ← x 2 y ← x 3 + 1 (c) Executable program

Static Single Assignment form

The Static Single Assignment (SSA) form is a property for intermediate representations of programs proposed back in 1988 by Rosen et al. [START_REF] Barry K Rosen | Global value numbers and redundant computations[END_REF]. It has since become a standard for intermediate representation used by compilers, for instance LLVM [START_REF] Lattner | LLVM: A compilation framework for lifelong program analysis & transformation[END_REF] used it by default, and a middle-end using it was verified for CompCert [START_REF] Barthe | Formal verification of an SSA-based middle-end for CompCert[END_REF]. The reason for this popularity is that a representation satisfying this property makes def-use chains explicit. In this form, one can know which instructions use a given declaration. Optimizations and analysis are usually simpler with this form. Besides, it is a relatively light property: the size of the SSA form is linear in the size of the original, non-SSA, program representation. SSA form guarantees that a variable is assigned at only one program point. This is done by indexing the variable at each assignment of the original program. It does not mean the variable can be assigned only once during the execution of the program: the assignment can be in a loop. That is why it is called static single assignment form.

This property faces an issue when two branches of a program meet, for instance after a conditional statement. Consider the example illustrated in Figure 6. We represented the structured program below as its CFG. The φ-function is added to a node, that is to a program point.

The structured program on the right can be represented as a CFG. In that case, the condition will result in a diamond shaped graph. The edges on the left correspond to the if branch and the right-ones to the else branch. The two branches meet at the end of the if.

i f ( x > 0 ) then x ← 2 e l s e x ← 3 endif y ← x + 1
The variable x is assigned a value in both branch and we indexed each definition: x 1 ← 2 and x 2 ← 3. After the conditional, the original program computes y ← x + 1. Which x should we use here, x 1 or x 2 ? SSA form addresses this issue by introducing the φ-function, which selects the appropriate variable, depending on the branch the execution is coming from. After the conditional statement, when the two branches meet, the assignment x 3 φ ← (x 1 , x 2 ) is introduced. Then in the assignment for y, we use x 3 : y ← x 3 + 1. Notice that this φ-function is attached to the program point 3 , it is not an instruction on an edge.

The φ-function solely exists in the intermediate representation. In the executable representation of the program, the φ-function will be replaced by the statements x 3 ← x 1 and x 3 ← x 2 respectively in each branch as seen in Figure 6c.

Inserting φ-function is the main challenge of the SSA-form, re-indexing the variables being trivial. Although φ-function could be put after each join point of the program (after conditionals and at each loop iteration in our While language), and for each variable, this is unnecessary and wasteful.

Given the graph of the program, the path-convergence criterion [START_REF] Appel | Modern Compiler Implementation in Java[END_REF] states that a φ is needed for variable v at node n if two nodes have a definition of v and if there is a path from them to n. The paths should not meet anywhere before n, the final node of the path.

Determining these points requires to compute the dominance frontier. The best algorithm currently is the Lengauer-Tarjan's one, which time complexity is almost linear (N • α(N ) with N the size of the program and α the slowly growing inverse of the Ackermann function).

Each variable can insert φ-functions at the beginning of a node. The semantics of these different φ-functions must be applied in parallel.

Formally, the semantics of a parallel assignment of variables a 1 , . . . a n to expressions e 1 , . . . , e n consists in taking the values v 1 , . . . , v n of e 1 , . . . , e n and assign these values to a 1 , . . . a n .

S a 1 ← e 1 | . . . |a n ← e n S def = {s[a 1 → v 1 ] . . . [a n → v n ]|s ∈ S, v 1 ∈ E e 1 s, . . . , v n ∈ E e n }
In this program, the set of environments at the end of the if branch should be the singleton {s}, with s = {x 1 → 2, y 1 → 4}. The semantics of the φ-function should assign in parallel the value for y 3 and x 3 .

S x 3 ← x 1 |y 3 ← y 1 {s} = {s[x 3 → v][y 3 → w] |v ∈ E x 1 s, w ∈ E y 1 s} = {s[x 3 → 2][y 3 → 4]} i f ( x > 0 ) then x 1 ← 2 y 1 ← 4 e l s e x 2 ← 3 y 2 ← 6 endif y 3 φ ← (y 1 , y 2 ) x 3 φ ← (x 1 , x 2 )
After the renaming, a copy propagation is often applied to reduce the number of variables. The consequence is that a block of φ-function can take this form:

y 1 φ ← (x 1 , y 2 ) x 1 φ ← (y 1 , x 2 )
In that case, the assignments must be made in parallel to preserve the semantics of the original program.

Static Single Information form 2.2.2.1 Introducing the σ-function

In the SSA form, the live-range is split at each definition and it is enough to infer the def-use chains. This is useful for forward analysis that infers information from the definition site (for instance constant propagation). But other analyses may infer information from the use sites, and perform a backward analysis. When an intermediate representation needs to distinguish the usage of its variables, it needs an operator dual of the φ-function, called the σ-function. Placed before branches, it combines the information on usage from both branches.

The σ-function takes one variable as argument, and its semantics is to copy the value of this variable in several new variables. Each one of this new variables will be used in only one branch. The example below shows where the σ-function is added. Here, x 0 is copied into x 1 , used in the then branch, and x 2 , used in the else branch.

i f (x > 0) then y 1 ← x + 1 e l s e y 2 ← 2 × x endif y 3 φ ← (y 1 , y 2 ) → (x 1 , x 2 ) σ ← x 0 i f (x > 0) then y 1 ← x 1 + 1 // x 1 > 0 e l s e y 2 ← 2 × x 2 // x 2 ≤ 0 endif y 3 φ ← (y 1 , y 2 )
What is interesting is that we have two properties for the new variables: x 1 > 0 and x 2 ≤ 0. Unlike the original code, we no longer need the flow-sensitivity to ensure that y 1 > 1 in the first branch, and that y 2 ≤ 0 in the other.

With these two functions, φ and σ, various analyses do not need to track information at each program points, they can jump directly from and to program points where information is provided or necessary. From dense analyses, we get sparse ones. But the class of analyses that can benefit from it is limited.

Limitations

Given an analysis, it is possible to define whether an intermediate representation allows a sparse analysis or not. Both the analysis and the program representation need to satisfy the Static Single Information [START_REF] Pereira | Static Single Information form[END_REF] property. Informally, the property is respected if the information on a variable is valid from its definition to its usage and only during this time, that is, during its live-range. Thus, transforming a program into a representation satisfying the property requires to split the live-range whenever the information changes (before condition, at a join, at assignment, or any other program point that modifies the information). Notice that what we call information depends on the analysis, and thus the SSI form of a program is defined with respect to an analysis. In our case, we deal with numerical analysis and will thus present the definition of the SSI form that satisfies the SSI property for this class of problems.

In this context, the SSI form is an extension of the SSA form that includes the σ-functions. Figure 7 pictures the SSI form of the example Figure 4. The SSI form satisfies the SSI property for analyses in the class of Partitioned Variable Problems (PVP) [START_REF] Pereira | Static Single Information form[END_REF]. In this class of problems, the information at each program point can be partitioned between each variable: the information is collected per variable. If we consider non-relational numerical analyses, we are in the case of PVP. For instance a range analysis associates to each variable its range of value, independently of the other variables. In PVP, it is possible to define an equational system on the information of each variable rather than on each program point. This result in one invariant for the whole program, making the analysis sparse. While a dense analysis needs one invariant per program point, which has a significant memory cost, a sparse analysis can have one invariant, and potentially even update it in-place, which is both time and memory saving. Let N be the size of the program, V the number

0 1 i 0 ← 1 i 1 φ ← (i 0 , i 4 ) j 1 φ ← (j 0 , j 4 ) 2 (i 2 , i 3 ) σ ← i 1 (j 2 , j 3 ) σ ← j 1 j 0 ← 0 3 j 2 < 10 4 i 4 ← i 2 + 1 5 j 4 ← j 2 + 1 6 (i 4 = j 4 + 1) 7 8 j 3 ≥ 10 (i 3 = 11)
Figure 7: SSI form of the example of variables. A dense analysis would need a memory space in O(N × V ). The number of variables introduced by the SSA or SSI form is linear in the size of the program [START_REF] Appel | Modern Compiler Implementation in Java[END_REF], so the invariant of a sparse analysis using this form will be in O(N ).

In the rest of this paper, we define a sparse relational analysis as an analysis able to compute one (relational) invariant for the whole program. This invariant can associate to any combination of variables (depending on the domain used to represent this invariant), the relation between them. The invariant can be seen as the set of constraints on the variables. For instance, in Figure 7, the variables i 2 and j 2 satisfy the constraint i 2 = j 2 + 1. Unfortunately, relational analyses are not PVP as the information deals with pairs (actually any tuple) of variables. This is a limitation stated in [START_REF] Pereira | Static Single Information form[END_REF]. In the case of relational analyses, the information is collected for tuples of variables, thus if the information on one variable changes, then the information on all other changes too. The SSI form only reasons on the live-range of one variable to ensure the property of single information. In our case, we need to consider the live-range of combinations of variables, thus the live-range of variables would be split every time one of them acquire new information. This would mean that the SSI form would introduce about V × N variables, ruining the benefit of the sparse analysis. This limit of O(V × N ) variables is our definition of the cost of a dense analysis, while O(N ) would be the ideal sparse analysis.

In practice, the analysis of a program does not need to infer all the relations between the variables. Most traditionally, an analyzer will look for assertions to prove in the code [START_REF] Henry | PAGAI: A path sensitive static analyser[END_REF]. With this objective, not all relations are necessary and we can potentially decrease the amount of variables needed.

Construction and destruction

The construction of the SSI form of a program relies on the dominance tree, where nodes are the labels, and a label dominates another one if every path from the entry points to must pass by . Then is a parent of in the dominance tree. The dominance frontier gives for each label , the sets of labels that is not dominated by but that has a parent dominated by . If a variable is defined at , will probably need a φ-function to join this definition from the one coming from another parent of .

Construction The construction of the SSI form of a program is a three-steps algorithm [START_REF] Pereira | Static Single Information form[END_REF], done for each variable.

The first step consists in computing the split live-range of the variable. It is split when the information on the variable may change and we need a new version of it. This step depends on the splitting strategy, which specifies which instructions change the information. In our case, it changes after each assignment, but also after a test where the variable appears, as we now know more precise information on it. Notice that for other PVP, the splitting strategy may be different. For instance let us consider a null pointer analysis in an object-oriented language. Then calling a method on an object brings information (if the program did not fail after this instruction, the object was not null).

The splitting strategy will induce other splitting points: at join and at branching, if two different information on a variable flow into each branch, then the live-range of the variable must be split at this join or branch. This steps needs the dominance frontier to determine these new splitting points. Once all splitting points for a variable have been computed, the φ-and σ-functions are added at branch and join. (In case of a splitting point that is not at a branch or join, then a simple copy is added.)

The second step consists in the renaming of the variable with indexes. It is a traversal of the dominance tree that stacks each new definition. The top of the stack is the name used for each use encountered during the traversal, as long as this definition dominates the use.

Finally, the third step removes dead code (copies not needed, σ copy that is not use in one branch, etc).

Destruction As traditional instruction sets do not provided the φ-and σ-functions, it is necessary to destruct the SSI form. This consists in replacing the φ and σ by copies and then proceed to a copy propagation to clean the code.

Cost Computing the dominance tree and the dominance frontier of a program from its CFG can be done efficiently with the Lengauer-Tarjan algorithm, as we saw for the SSA form [START_REF] Appel | Modern Compiler Implementation in Java[END_REF]. Its time complexity is almost linear in the size N of the program (N • α(N )). Now let us detail the cost of the transformation for one variable. First, the splitting strategy gives the set of program points where information changes. Computing this strategy is linear in N , as it simply consists in examining each instruction (an edge of the CFG) and determine if its program points (the node defining this edge) are splitting points. Then this set of splitting points is extended with the dominance frontier of the predecessors or successors (depending on the SSI form built) of the splitting points. We extend this set to detect where φ-and σ-functions may be needed. This extension is done in one iteration on the set of splitting points, and given that the dominance frontier has already been computed, it has a complexity in O(N ). Once the set is complete, the φ-and σ-functions are inserted, which is also in O(N ) as it is a mere iteration on the extended set of splitting points.

Then the algorithm proceeds to the renaming. It is done through a traversal of the dominance tree, exactly like the SSA transformation, with a stack of definition to remember the last definition used in this path. All nodes of the dominance graph are transformed, and for each of them the successors are examined. Like for SSA, this step is almost linear in N [START_REF] Appel | Modern Compiler Implementation in Java[END_REF]. Finally the dead code elimination is greatly simplified by the SSA-aspect of the SSI form: the uses of a definition can be extracted easily thanks to the re-indexing. This elimination can be performed in linear time with respect to the size of the program.

Overall the construction of the SSI form for a variable is almost linear in the size of the program.

Relational analyses

While non-relational analysis are now easier to perform sparsely thanks to convenient intermediate representations, there is no satisfying fits-all representation of the program in the literature for general relational analyses. Yet, there exists several relational analyses with good performance. These analyses are highly valuable to detect bad behaviour of a program such as out of bound array accesses, or violation of assertions. With different objectives, different contexts or usages of the results, they are designed more efficiently and with better precision. However, they are also heterogeneous in their method and proofs, making it hard to reproduce the result on a different analysis. Abstract interpretation is a step to homogenize the results, giving a template that is easier to reproduce and adapt. Despite not using abstract interpretation, some of these analyses are relevant thanks to the representation of the program or of the information they use, as well as the optimized treatment they applied. This section pictures three examples of such relational analyzers, performing on the SSA form or a variation of it. They are sorted chronologically, and one can observe on one hand the development of intermediate representations of programs and on the other the representation of the information.

Global Value Numbering

Global Value Numbering (GVN) is a technique to detect when two computations in a program have equivalent results. The equivalence is then used for optimizations. For instance, if the result of the first computation is stored in a variable v, the second computation can be replaced by v, avoiding repeating it. This optimization is the Common Sub-expression Elimination (CSE). An other optimization consists in moving a computation made in two branches outside of it, shortening the code. For these reasons GVN is often found in optimizations of compilers. In a local value numbering, the scope of the computations is restricted to basic blocks, while it is extended to the whole control graph in a global one.

In 1988, Alpern et al. [START_REF] Alpern | Detecting equality of variables in programs[END_REF] proposed an algorithm for GVN. Their main contribution was to detect equivalence of expressions despite control structures such as conditionals. To work properly, the GVN needs a program respecting the SSA form, so that it can associate a unique value (or more exactly a symbolic expression) to each variable. For this expression to be unique, the variable must have only one static definition. Alpern et al.'s algorithm builds a value graph based on the SSA form of the program. It is a directed graph representing the symbolic computations of the program made at each assignment. There are two types of nodes, and in both cases, the order of the arguments is important, so the edges are ordered too.

Executable function It can be an operator such as +, or a constant (function of arity 0). The node representing the operator is linked to the arguments.

φ-function The transformation to SSA form creates φ-function at join points. In the case of x = φ(e 1 , e 2 ), then the value graph of x will start with a φ-node. Each φ is labeled, to distinguish from the others. The φ-node is linked to each of its arguments, in our case, the value graph of e 1 and e 2 .

Two variables are equivalent at some program point p if the last assignments of the variables before p correspond to congruent nodes in the value graph. Congruence of nodes is defined recursively: the nodes must have the same function symbol, applied to congruent arguments. In other words, for each leaving edge, taken in order, the destinations must be congruent. Congruence is a symmetric, reflexive and transitive relation, and the GVN algorithm must build its classes of equivalence. However, cycles can appear in the value graph. The current definition of the congruence is not enough. There are different sets of classes that can be solutions. Under the (strong) assumption that all variables are initially equivalent, the solution is the maximal fix point satisfying the relation. It is built starting with all expressions in the same set, which is separated when two expressions are proven to be non-equivalent. Finding such a fixpoint due to cycle in a graph is actually the same issue as the one faced when defining the semantics of loops in Section 2.1.2. Hopcroft's partitioning algorithm allows the construction of the classes in O(E log E) where E is the number of edges in the value graph.

As it is, this analysis does not take into account control structures. To do so, Alpern et al. observe that the results of assignments in two conditionals are equivalent if i) they are given the same values in each corresponding branches and ii) the predicates of the conditionals are congruent. To integrate this pattern in the value graph, they introduce a new function φ if .

At each conditional, for each variable assigned in the conditional, a φ if node is added to the value graph with three arguments: the value given in the then branch, the value given in the else branch and finally the predicate. If the partitioning algorithm found two expressions with root φ if to be congruent, it means the two expressions have congruent predicates and thus branch on the same direction. It also means that the values given are congruent.

Similarly, they introduce new functions for loops: φ enter and φ exit . Here the conditions for two variables to be equivalent while assigned in a loop body are that i) they have the same initial value, ii) they are modified the same way and iii) loops are executed the same number of time.

φ enter is inserted at the beginning of the loop, before evaluating the exit predicate. Its arguments are the variable coming in the loop and the one modified at the end of the loop body. This function is similar to the φ in the SSA form: it joins the value before entering the loop the first time with the one at the end of the loop body. If the partition algorithm find two congruent expressions with root φ enter , this means the variables have started with congruent values and are modified the same way: they remain congruent in the loop body.

φ exit is inserted after the loop, when the predicate has stated its end. Its arguments are the predicate and the variable assigned before (the one assigned by a φ enter ). If the partition algorithm finds two congruent expressions with root φ exit , this means the variables are congruent at each step of the loop (the first argument should be an expression with φ enter ) and the loop should end at the same number of steps, as the exit predicates are congruent too. The end values should then be congruent too.

The proof of correctness provided by [START_REF] Alpern | Detecting equality of variables in programs[END_REF] proceed by contradiction to assert that congruent variables have the same value2 . This proof does not follow the abstract interpretation principles. This analysis is efficient, but specialized to one class of problem. Our goal is to make a more general analysis, which would also have a proof more in the spirit of abstract interpretation theory.

Elimination of array bounds checks

Access to an array is made by index, which can in times be out of the bounds of said array. While memory unsafe languages, such as C, do not check if an access to an array is valid, others, like Java, do. To do so, array accesses A[i] are guarded by a bound check (0 ≤ i < A.length ?). In case the condition is violated, an exception is raised during execution precisely at the access instruction. But this systematic instrumentation of code is cumbersome for the execution (a lot of conditions to evaluate) and for optimizations (they cannot freely reorder the instructions as the exception must be raised at the moment precised by the semantics of the original program). Thus, removing as much as possible of the guards, while staying safe, is a major issue.

ABCD [START_REF] Bodík | ABCD: eliminating array bounds checks on demand[END_REF] is an example of such analysis. It relies on the e-SSA form, a variant of SSA, to perform a sparse analysis. The variant adds extra copies for variables after conditionals (and also after array accesses as, if it is passed, the index must be within bound). The π-function is in charge of the copies.

i f ( y > 0 ) then ( . . . ) e l s e ( . . . )

i f (y 0 > 0 ) then y 1 ← π(y 0 ) ( . . . ) e l s e y 2 ← π(y 0 ) ( . . . )
The behaviour of the π-function is really similar to the σ-function, despite its different placement: it copies a variable for each branch of a condition. Now, in the analysis it is possible to states that y 1 > 0 and y 2 ≤ 0. In the branches, this information is propagated by the use of y 1 and y 2 instead of y 0 . In this form, a property between two variables (for instance i < A.length) holds for all their common live-range (the set of program points where they are both alive). The analysis can be sparse, with only one invariant for the whole program. This form respects the SSI property for the elimination of array bounds checks. Yet, the analysis is relational: both the index of the access and the size of the array are variables.

ABCD proceeds in two steps to determine whether the indexes are within bounds. First, it checks the upper-bound (i ≤ A.length ?) then the lower-bound (0 ≤ i ?). The two analyses are similar. Relations tracked in the first case are of the form v i -v j ≤ c where c is a constant. This domain is more restricted than the octagon seen previously, it actually corresponds to the zone domain [START_REF] Miné | Tutorial on static inference of numeric invariants by abstract interpretation[END_REF]. It is a convenient domain, where constraints can be represented on a graph. Vertices are variables, sizes of arrays and constants appearing in the program. An edge v i → c v j denotes the constraint v j -v i ≤ c. With a graph, it is not necessary to represent the constraints for all pair (v i , v j ): it is assumed that c = +∞ if there is no direct edge. The careful choice of this abstract domain for this application is a key-aspect of its efficiency. In our case, the abstract domain will be free to choose by a user of the analyzer, and thus we cannot assume its efficiency.

An important aspect of ABCD is that it is demand-driven. It will not compute the constraints for all array accesses, only the "hot" ones, the most executed ones. Thus, it will only ask to determine if i < A.length for some A and i. With the graph representation, determining if i < A.length is equivalent to find if i -A.length ≤ -1, that is, no path from i to A.length must weight less than -1. The algorithm answering must find the shortest path from i to A.length and ensure that its weight is at least -1. In our case we will not consider all relations possible and the analysis will be demand driven too. Instead of an array bound check, we target assertions in the code that need to be proven. The variables used at these assertions should respect the information property: any information on these variables should be valid during all their common live-range.

Path sensitive static analysis

PAGAI [START_REF] Henry | PAGAI: A path sensitive static analyser[END_REF] is a path sensitive static analyzer that uses abstract interpretation principles. The analysis checks whether assert statements in the program always hold or not and computes invariants for loop-headers. The abstract domain is left to the choice of the user, with the polyhedra domain by default. The convergence accelerators are also free to choose. The tool is built upon the LLVM compiler infrastructure, and it takes as input the program in the LLVM bytecode, which is already in SSA form [START_REF] Lattner | LLVM: A compilation framework for lifelong program analysis & transformation[END_REF]. It then outputs invariants for a subset of program points that includes loop-headers. This tool is close to what we want to achieve: a configurable tool to perform static relational analysis. The analysis is only performed forward, although they claim that the techniques are not specific to it.

PAGAI benefits from the SSA form to perform a sparse analysis instead of a dense one. However, it is not as sparse as GVN or ABCD as it keeps track of invariants at several points in the program. We want to reach higher sparsity, as the cost in memory of several invariants can be prohibitive in some abstract domains. This means we need a better representation of the program: having several program points spares them the need of the SSI property.

Unfortunately, the formalism of PAGAI is not detailed in the article. Yet they present a noteworthy feature: quite surprisingly, the tool does not simply apply the least upper bound at join points of the program. Unlike classical abstract interpretation, it relies on a SMT solver to determine the paths possible and it only joins the outcome of these paths. Joining only what could be joined is an efficient way to keep precision. PAGAI benefits from the efficiency of modern SMT-solver to have a more precise result on the possible paths. This also means the expressiveness of SMT-solvers bounds the efficiency: for instance, congruence relationships are not dealt with properly. In that case, an impossible path may have to be taken into account. Whether the path will be considered or not depends on the SMT-solvers, not the abstract domain.

Other optimization brought by PAGAI includes removing variables from the abstract domain if it can be defined as a linear combination of other variables. This alleviates the polyhedra operations, that perform badly on high dimensions. This optimization actually concerns the abstract domain and we will not reproduce it here.

The goal of PAGAI is to ease comparison of different abstract domains, in terms of precision and computation times. Surprisingly, although the polyhedra domain should be more precise statically, it loses in precision because of its widening operators. The octagon and interval domains do not suffer such detrimental operators. Without surprise, the octagon domain gives more precise invariants than the interval one.

A sparse flow-insensitive relational static analysis

As we saw, the existing relational analyses are either very specific and achieve sparsity (GVN and ABCD) or they stay general but still need several invariants (PAGAI). We want to show that it is possible to have one invariant, that remains precise, for the whole program, using the SSI form. For the precision, we rely on the partition of the variables' lifetime, guaranteed by SSI. Thanks to that we were able to design a static analysis that is

Sparse and flow-insensitive

There is only one invariant for the whole program.

Domain independent

The abstract domain used to represent the invariant is left free to chose by the end-user. A few proofs of soundness requires additional conditions on the domain, in particular the projection should be exact. These conditions are satisfied by the interval, octagon and polyhedra domains presented before.

Relational It can keep track of the relations between variables.

Abstract interpretation-oriented It is described and proven using the abstract interpretation theory.

Our analysis must be able to give an abstract invariant for the program, such that it is a sound abstraction of the concrete semantic of the program. This correctness is evaluated with respect to the concrete semantics of the SSI form of the program.

Outline This section starts with the formal definition of the SSI form of a program as well as the concrete semantics we consider. As you will see, the invariant for such semantics needs an abstract domain able to express partial environments. We thus detail in the following subsection the overlay of our abstract domain that will allow this expressiveness. Then, the abstract semantics of the program can be defined, using the principles of abstract interpretation stated in the previous section. This abstract semantics consists in a single invariant that can be concretized as an overapproximation of the set of environments of the concrete semantics. Although the single invariant constraint imposes the join of information and a potential loss of precision, the properties of the SSI form actually ensures a satisfying level of precision. This is discussed in a dedicated subsection. Finally, this section ends with an overlook of the implementation in OCaml of a prototype of the analysis.

SSI form and concrete semantics

Our analysis is performed on the SSI form of the original program. Unlike the work presented in [START_REF] Pereira | Static Single Information form[END_REF], where the algorithms are performed on a graph where the atomic instructions are the nodes of a graph, we build our SSI form from its CFG. This allows a definition of the semantics in the framework of abstract interpretation. This section does not detail the algorithms to build the form, as they are similar to the one in [START_REF] Pereira | Static Single Information form[END_REF], but it presents the notations, as well as the concrete collecting semantics of the SSI form.

The SSI form of the program is built from its CFG. Besides the renaming of variables, this process attached φ-and σ-functions to labels. The SSI program is a graph with nodes representing the labels. These nodes can be annotated with the φ-and σ-function. The edges of the graph are annotated with the atomic instructions.

Notation The SSI intermediate representation of the program is a tuple (E, A, J, B) such that:

• E is the set of edges ( 1 → 2 ) in the CFG.

• A ∈ E → Atom associates to each edge 1 → 2 its atomic instruction given by the CFG.

• J (join) is a map from a label to the set of φ-functions defined at this label.

• B (branch) is the equivalent map for σ-functions.

3 φ ← ( 1 : i 1 , 2 : i 2 ) j 3 φ ← ( 1 : j 1 , 2 : j 2 ) 3 ( 4 : i 4 , 5 : i 5 ) σ ← i 3 ( 4 : j 4 , 5 : j 5 ) σ ← j 3 1 2 4 5
In this example, the program point 3 has two predecessors ( 1 and 2 ) and two successors ( 4 and 5 ).

In the φ-functions we precise for each arguments the label associated. That is to say, i 3 is assigned i 1 when coming from

1 . Similarly, we annotate the assigned variables of a σ-function with the label where the variable is defined. Here, i 4 is the version used for label 4 .

Figure 8: The representation for a program in SSI form is the same as the CFG of the program, but we add the φ-and σ-functions to the nodes.

A φ-function x φ ← ( 1 : x 1 , . . . , k : x k ) at is represented as a partial function from labels to the variable copied. J( ) is thus the φ bloc at program point . It is a partial function that associates to each variable its φ-function.

J( )(x) = { 1 → x 1 , . . . , k → x k } : L V J( ) : V (L V)
The labels 1 , . . . , k are exactly the source labels of the incoming edges of , noted In( ). The term J( )(x)( 1 ) = x 1 can be read as "At , when coming from 1 , the program assign x 1 to x".

A σ-function

( 1 : x 1 , . . . , k : x k ) σ ←
x is represented the same way with 1 , . . . , k ∈ Out( ).

B( )(x) = {l 1 → x 1 , . . . , l k → x k } : L V
The term B( )(x)( 1 ) = x 1 can be read as "At , when going to 1 , the program assign x to x 1 ". From now on, it is the SSI form of the program that we call "the program" and we note P = (E, A, J, B). The set of programs is noted P.

In the rest of the section, we define the concrete semantic of a program in SSI form using this notation. It closely ressembles the concrete semantics given in Section 2.1, but adds the effect of φ-and σ-functions.

Single entry point

We consider that the CFG has only one entry point 0 and that this entry point has no predecessors. Any CFG can be transformed to respect this condition, without loosing its semantics. All it needs is to add this program point, and add edges from it to the previous entry points, with the atomic instruction on these edges being the test (0 = 0), for instance.

Concrete semantics of programs

The concrete semantics of the program is given by the function • : P → P (L × E). It is defined as the least fixed point of a global transfer function F which applies the transfer function of each edge of the CFG, then joins the results.

P def = lfp(F )
We will first detail the transfer function of an edge then detail F .

Edge transfer function At a given program point , the possible set of environments depends on the predecessors. Let be a predecessor of in the CFG. A state ( , s) is reachable only if there exists an environment s at such that s is s on which was applied (i) the potential σ-copies from to , (ii) the atomic instruction from to , and finally (iii) the φ-copies at , coming from . For every edge ( → ) ∈ E, we define a transfer function T → : P (E) → P (E). This transfer function is the composition of the transfer functions for step (i), (ii) and (iii), respectively T σ , T f and T φ :

T → def = T φ • T f • T σ
The functions T σ and T φ are based on the same principle: collect all copies for the edge to and get the semantics functions of the corresponding parallel assignments.

Let dom(B( )) = {x 1 , . . . , x n } be the variables for which there is a σ-copy at . These are the variables that will be copied. For every x i , let x i = B( )(x i )( ). They are the new copies for . Then

T σ def = S x 1 ← x 1 | . . . |x n ← x n
As for φ-functions, let dom(J( )) = {y 1 , . . . , y m } be the variables resulting from a φ-copy and y i = J( )(y i )( ) be the ones copied when coming from . Then

T φ def = S y 1 ← y 1 | . . . |y m ← y m
In case where there is no φ of σ then these parallel assignments becomes identity functions in the semantics. Finally, if A( → ), the atomic instruction associated to the edge, is an assign x ← v,

then T f def = S x ← v , else, it is an arithmetic condition e 1 e 2 , then T f def = C e 1 e 2 .
Example Figure 9 gives an example of tranfer function for an edge. As for the example of Figure 7, let us consider the edge 1 → 2 . There is no σ at 1 , so T σ = id.

T 1 → 2 = T φ • T f • T σ = S i 1 ← i 0 |j 1 ← j 0 • S j 0 ← 0
Let us consider the edge 2 → 3 . There is no φ at 3 so T φ = id.

T 2 → 3 = T φ • T f • T σ = C j 2 < 10 • S i 2 ← i 1 |j 2 ← j 1
Global transfer function Let S ∈ P (L × E) represents the current invariant of the program. Each of its elements is a pair of a label with an environment s, such that ( , s) is a reachable state. Several environments can be associated to the same program point. P (L × E) is actually isomorphic to L → P (E) and we will use either definition at our convenience. More precisely, for a given label ∈ L we note S = {s ∈ E|( , s) ∈ S} the set of environments attached to in the invariant S.

The transfer function F : (L → P (E)) → (L → P (E)) transforms an invariant S by applying the transfer function of each edge of the CFG and joining the resulting sets of states. We note to . The new environments at are the union of all environments S at the predecessors composed with the transfer functions of the edge → .

T σ = S i 2 ← i 1 |j 2 ← j 1 T f = S i 3 ← e(i 2 , j 2 ) T φ = S i 4 ← i 3 |j 4 ← j 2 T 1 → 2 = T φ • T f • T σ
S def = ( → )∈E T → (S )
From the invariant S we can build the invariant at a next step S . Let S k be the S at iteration k. Then in the end, the semantics of the SSI program is the union of all these S k once the fixpoint has been reached.

P = lfp   ∈L S k  

Domain coherence

As a result from this union, we have a set of partial functions that may not have the same domain (some variables have been defined on an edge and not on the others). In our example, the joining point 2 is associated with the union of the environments from 1 and the ones from 6 . The environments from 1 , after applying the transfer function from 1 to 2 , have as a domain {i 0 , j 0 , i 1 , j 1 }. On the other hand, the environments of 6 have as a domain {i 0 , j 0 , i 1 , j 1 , i 2 , j 2 , i 4 , j 4 }. So the environments at 2 can have different domains.

Abstract domain

In the state of the art [START_REF] Jeannet | Apron: A library of numerical abstract domains for static analysis[END_REF], abstract domains represent environments where the numerical information of each variable is tracked. These abstract environments concretize into total functions from variables to values. However, we want to be able to represent partial functions. That is why we build an overlay around some abstract domain D, which can be any numerical abstract domains introduced previously. This section describes this overlay. We want to use the framework of abstract interpretation described by Miné [START_REF] Miné | Tutorial on static inference of numeric invariants by abstract interpretation[END_REF]. To be able to use its tool, we provide useful properties for our overlay, such as the monotony of its concretization function. We first define the requirements of the original abstract domain D.

Domain for environments

The overlay is an abstract domain parametrized by another abstract domain that abstracts the environments. The domain for environments can be any relational or non-relational domain that allow expressing properties on the value of the variables. Still, it must satisfies a couple of properties. The set of abstract environments is noted D, and it must be provided with a complete lattice (D, , , , ⊥, ). Also, there must exist a monotone concretization function from elements of the abstract domain to a set of environments γ D : D → P (E). Finally, the abstract domain must be provided with sound abstractions of assignments and arithmetic conditions. The library Apron, which can manipulate abstract domains for environments provides these properties on its domains [START_REF] Jeannet | Apron: A library of numerical abstract domains for static analysis[END_REF].

S x ← e : D → D S x 1 ← e 1 | . . . |x n ← e n : D → D C e 1 e 2 : D → D such that ∀X ∈ D : S x ← e • γ D (X) ⊆ γ D • S x ← e (X) ∀X ∈ D : S x 1 ← e 1 | . . . |x n ← e n • γ D (X) ⊆ γ D • S x 1 ← e 1 | . . . |x n ← e n (X) ∀X ∈ D : C e 1 e 2 • γ D (X) ⊆ γ D • C e 1 e 2 (X)
Domain for partial functions In the concrete environments, we were able to state that some variables are not defined, using partial functions. This is not possible in an abstract environment of D. A variable is either unconstrained (it can have any value) or bound by some constraints, but it always exists. Still, to increase precision, it is important to know which variables can be defined, and which cannot. We define an overlay of the abstract domain. The elements of this overlay are denoted by a superscript +. The new set of abstract environments for our abstract domain pairs an element of D with a set of variables: D + def = ((D \ {⊥}) × P (V)) ∪ {⊥ + }. The bottom element ⊥ + represents the empty set of environments. Informally, an abstract environment (X, V ) represents the set of concrete environments included in γ D (X) and defined over a set of variables included in V . Abstract states such as (⊥, V ) are not allowed, as they would all concretized in an empty set of environments (under the assumption that γ(⊥) = ∅). To avoid the redundancy, we only use ⊥ + .

Example Let X ∈ D be an abstract environment. In the following examples, we will note

X def = {i = 0, j = i + 1} to state that X def = {s|s ∈ γ D (X), i = 0, j = i + 1} Let V = {i, j}, then (X, V ) ∈ D + .
We did not precise it formally, but the variables constrained in X must be in V for (X, V ) to be an element of D + . In other word, the projection of X on any subset V ⊆ V should be equal to X. This rule is preserved by the operators we will introduce and the analysis.

Projection In our framework of abstract interpretation ( [START_REF] Miné | Tutorial on static inference of numeric invariants by abstract interpretation[END_REF]), we need to have a partial order of the elements of D + . Given the interpretation of abstract environments, we decided to define the order using projections. In Mine's tutorial [START_REF] Miné | Tutorial on static inference of numeric invariants by abstract interpretation[END_REF], the abstract projection we presented in Section 2.1 is rather called a non-deterministic assignment and is defined by:

V \ V = {x 1 , . . . , x n }, proj V (X) = S x 1 ← [-∞, +∞]| . . . |x n ← [-∞, +∞] X
We will use this definition from now on.

Polyhedra and octagon abstract domain both have an exact non-deterministic assignment [14][15]. Remark that with this definition, for any X ∈ D, X proj V (X).

Example The projection of X from the previous example onto U = {j} is defined by the set of constraints {j = 1}. For any c ∈ I, the environment f = {j → 1, i → c} is in the concretization of proj U (X) (we forgot the value of i). There exists f

∈ γ D (X), such that f | U = f | U , for instance f = {j → 1, i → 0}.
Partial order Informally, all environments represented by (A, V ) are also represented by (B, W ) if (i) W at least contains V and if (ii) when we restrict B to the variables V , it contains at least A.

For (ii), we say that A is included in the existential projection of B on V .

(A, V ) + (B, W ) def ⇔ V ⊆ W ∧ A proj V (B)
Example Let us take (X, V ) ∈ D + from the previous example. Let (Y, W ) ∈ D + such that

Y def = {i = k, j = i+1, 0 ≤ k} and W = V ∪{k}.
Compared to X, we added a positive variable k and specified it is equal to i. Then (X,

V ) + (Y, W ) as V ⊆ W and proj V (Y ) = {0 ≤ i, j = i + 1} X.
We consider that (Y, W ) is less precise even if it has a new variable k, as it makes us loose the constraint i = 0. Now consider

Z def = {i = 1, j = i + 1} then there is no telling that (X, V ) + (Z, V ) or (Z, V ) + (X, V ) because neither X Z nor Z X.

Concretization function

The concretization function gives all possible partial functions represented by an abstract value X + ∈ D + . If X + = (X, V ), then the concretization is all partial functions defined over a subset of V that coincide with a (total) function of the concretization of X.

γ D + : D + → P (E) γ D + (X, V ) def = s | W s ∈ γ D (X), W ⊆ V γ D + (⊥ + ) def = ∅
Example Let us take (X, V ) from the previous example. Let us assume that V = {i, j} and that the concretization of

X in D is γ D (X) = {i → v, j → v + 1} v ∈ I, v ≥ 0 Then the concretization of (X, V ) in D + is γ D + (X, V ) = {i → v, j → v + 1} v ∈ I, v ≥ 0 W = V ∪ {i → v} v ∈ I, v ≥ 0 W = {i} ⊆ V ∪ {j → v + 1} v ∈ I, v ≥ 0 W = {j} ⊆ V ∪ {} W = ∅ ⊆ V
Monotony We want our partial order to be organized such that higher elements in D + represent larger elements in the concrete world P (E). These abstract elements represents more program behaviours. This condition is respected if the concretization function is monotonic with respect to our partial order.

Theorem 3.1. [Monotony] If the projection is exact, that is γ D • proj V (X) = proj V •γ D (X)
for any X and V , then the concretization function is monotonic:

X + + Y + =⇒ γ D + (X + ) ⊆ γ D + (Y + ) Proof. If X + or Y + is ⊥ + then the implication trivially holds. Else, let us define X + = (X, V ) and Y + = (Y, U ). Let s | W ∈ γ D + (X, V ) with W ⊆ V and s ∈ γ D (X). Then s | W ∈ γ D + (Y, U ), as W ⊆ V ⊆ U and by monotony of γ D , s ∈ γ D (X) ⊆ γ D • proj V (Y ) = proj V •γ D (Y ). So there exists s ∈ γ D (Y ) such that s | V = s | V . As W ⊆ V , necessarily, s | W = s | W and so we find a s ∈ γ D (Y ) that guarantees s | W ∈ γ D + (Y, U ).
The exactness of the projection is a restrictive condition for our abstract domain D. In the case of the polyhedron domain, the condition holds as the Fourier-Motzkin elimination provides an exact abstraction of the projection. It is also exact in the octagon domain.

Following the methodology of abstract interpretation (as proposed by Miné [START_REF] Miné | Tutorial on static inference of numeric invariants by abstract interpretation[END_REF]), to give an abstract semantics mostly consists in finding the good abstraction of the concrete world and its operations. We need to find a sound abstraction for the concrete lattice (P (E) , ⊆, ∪, ∩, ∅, E). We already have the abstraction for P (E), ⊆, and ∅.

Semilattice (D + , + ) is a poset, but we cannot define a join + necessary to make it a lattice. We will instead simply define an abstract union ∪ . However, we have a meet-semilattice (D + , + , + , ⊥ + , + ). The top is defined as + = ( , V).

Meet

The meet, which abstracts the intersection of concrete states, can be defined as

(A, V ) + (B, W ) def = ⊥ + If C = ⊥ (C, V ∩ W ) Otherwise with C = proj V ∩W (A) proj V ∩W (B) X + + ⊥ + = ⊥ + + X + def = ⊥ + Proof.
Let us check that it is indeed the greatest lower bound by using the definition of our order + . First, let us check that it is a lower bound. We do have the inclusion of the set of variables V ∩ W into V and W . Then we need to check the inclusion of C in the projection of A and B onto the set of variables V ∩ W . This is guaranteed by the definition of C which is exactly the intersection of the projection, thus included in proj V ∩W (A) and proj V ∩W (B). Hence, it is a lower bound.

It is also the greatest. First, the set of variables cannot be augmented or there would be variables that are not elements of V and W . Second, let us suppose that there exists C C such that C is in the projection of A and B onto V ∩ W : C proj V ∩W (A) and C proj V ∩W (B). Then necessarily, by definition of the meet ,

C proj V ∩W (A) proj V ∩W (B) = C. So C is the greatest lower bound. b c a B + A + C + 2 C + 1
The different lines are defined by the following constraints.

• A + , in the plane (a,c), by a = c As for the elements of D, all represented in the space (a, b, c), the projection of C 1 and C 2 are both the plane defined by a = c, that is exactly A. C 1 and C 2 both includes A in their projections on V A = {a, c} and B in their projection on

• B + , in
V B = {b, c}. Yet neither C 1 ⊆ C 2 nor C 2 ⊆ C 1 .
Besides, they are minimal: removing a part of C 1 or C 2 would break the inclusion of A in their projection. ). These two elements are represented on the Figure 10. B + is represented as a segment, in the plane {b, c}. We want to find (C, V C ) that would be the least upper bound of (A, V A ) and (B, V B ). First, we must have V C = V A ∪ V B = {a, b, c} to guarantee the order and to be a least element (by Lemma 3.1). So C + will be a 3D object in the space {a, b, c}. Then, the projection of C on {a, c} must contain the line A, and its projection on {b, c} must contain the segment B. But a unique minimal C cannot be found. Let us consider two candidates C 1 and C 2 . C 1 is defined by the constraints a = c and is segmented for the constraints on b: if c ≤ 4, then b = 4, if 4 ≤ c ≤ 6, then b = c and finally if c ≥ 6 then b = 6. Its projection on {a, c} is exactly A. Its projection on {b, c} contains the segment B. It is a valid upper bound of both (A, V A ) and (B, V B ). Now, C 2 is defined by the constraint a = c = b, that is it is a line in the 3D space. Its projection on {a, c} and {b, c} respectively are both lines that contains A and B respectively. So (C 2 , V C ) is also a valid upper bound for (A, V A ) and (B, V B ). But there is no telling whether C 1 is greater than C 2 or the contrary: none of this 3D object contains the other. Also, removing any part of C 1 or C 2 would break the order A proj V A (C i ). They are minimal elements but not unique. This prevents us from defining a join.

Abstract union

We define our abstraction of the union, noted ∪ , as the meet of two information. On the one hand we combine the information on the common variables (V A ∩ V B ) and on the other we combine the information from the other variables.

(A, V A )∪ (B, V B ) def = proj V A ∩V B (A) proj V A ∩V B (B) proj V A \V B (A) proj V B \V A (B), V A ∪ V B And X + ∪ ⊥ + def = ⊥ + ∪ X + def = X +
In practice this operator will be applied on values such that V A ⊆ V B , so the projection on V A \V B = ∅ will be .

Example Let X def = {i = 0, j = i+1}, Y def = {i = 1, j = i+1, k = i}, V = {i
, j}, W = {i, j, k}. First, we do not have (X, V ) + (Y, W ) as the information i = 0 is not included in Y . As for the abstract union of these two elements, let us detail the result of each projection.

proj V ∩W (X) = proj V (X) = X proj V ∩W (Y ) = {i = 1, j = i + 1} proj V \W (X) = proj ∅ (X) = proj W \V (Y ) = {k = 1}
And so

(X, V ) + (Y, W ) = (X {i = 1, j = i + 1}) {k = 1}, W = {0 ≤ i ≤ 1, j = i + 1} {k = 1}, W = {0 ≤ i ≤ 1, j = i + 1, k = 1}, W
In the end, the link between k and i has been lost. This abstract union must be proven sound. This can be proved easily once we proved that the abstract union is an upper bound of each of its operands.

Lemma 3.2. [Abstract union is upper bound]

For any A + , B + ∈ D + ,

A + + A + ∪ B + and B + + A + ∪ B +
Proof. Let us prove the order A + + A + ∪ B + , the proof is symmetrical for B. Let A + = (A, V A ) and B + = (B, V B ). First, the set of variables V A is included in the set of variables of the abstract union (V A ∪ V B ). Then, let us consider the different terms of the meet.

A proj V A ∩V B (A) proj V A ∩V B (A) proj V A ∩V B (B) and A proj V A \V B (A)
This give us that A is less than the meet of two of the operands.

A proj V A ∩V B (A) proj V A ∩V B (B) proj V A \V B (A) proj V A proj V A ∩V B (A) proj V A ∩V B (B) proj V A \V B (A)
This proves a first part:

A + + proj V A ∩V B (A) proj V A ∩V B (B) proj V A \V B (A), V A ∪ V B .
We still have to prove that the remaining of the meet is an upper bound of A + . It corresponds to the projection of B onto the variables V B not in V A . The projection on V A of this projection is necessarily .

A proj V A • proj V B \V A (B) = proj V A ∩(V B \V A ) (B) = proj ∅ (B) = Thus, A + + (proj V B \V A (B), V A ∪ V B ).
As we proved that A + is less than all operands, we do have that it is less than the meet.

A + + proj V A ∩V B (A) proj V A ∩V B (B) proj V A \V B (A), V A ∪ V B + proj V B \V A (B), V A ∪ V B = proj V A ∩V B (A) proj V A ∩V B (B) proj V B \V A (B) proj V A \V B (A), V A ∪ V B = A + ∪ B +
In the case where V A ⊆ V B , the abstract union is indeed an upper bound.

Theorem 3.2. [Soundness of abstract union]

The abstract union ∪ is sound with respect to the concretization function γ D + : for any A + and B + ∈ D + ,

γ D + (A + ) ∪ γ D + (B + ) ⊆ γ D + A + ∪ B +
Proof. This is simply the result of applying the monotonicity of γ D + onto the result of the previous lemma.

Abstract atomic instructions To be able to use the theory of abstract interpretation we still need to define the abstract assignments and conditions in our domain. For assignments and conditions, let (X, V ) ∈ D + be an abstract environment.

S x ← e + (X, V ) = (S x ← e X, V ∪ {x}) If vars(e) ⊆ V ⊥ + Otherwise S x 1 ← e 1 | . . . |x n ← e n + (X, V ) =    (S x 1 ← e 1 | . . . |x n ← e n X, V ∪ {x 1 , . . . , x n }) If vars(e 1 ) ∪ • • • ∪ vars(e n ) ⊆ V ⊥ + Otherwise C e 1 e 2 + (X, V ) = (C e 1 e 2 X,
∀X + ∈ D + : S x ← e • γ D + (X + ) ⊆ γ D + • S x ← e + (X + ) ∀X + ∈ D + : S x 1 ← e 1 | . . . |x n ← e n • γ D + (X + ) ⊆ γ D + • S x 1 ← e 1 | . . . |x n ← e n + (X + ) ∀X + ∈ D + : C e 1 e 2 • γ D + (X + ) ⊆ γ D + • C e 1 e 2 + (X + )
Proof. In the case where X + = ⊥ + , all these inclusions trivially hold. Let us prove the soundness of our new assign for x ← e. Let (X, V ) ∈ D + be an abstract environment. We first develop each side of the relation to prove (the concrete environments will be noted s in the left side, t is the right one).

S x ← e • γ D + (X, V ) = S x ← e ({s | W |s ∈ γ D (X), W ⊆ V }) = s = s | W [x → v] s ∈ γ D (X), W ⊆ V, v ∈ E e s | W
If vars(e) ⊆ V , then there is no v ∈ E e s | W and the term becomes

S x ← e • γ D + (X, V ) = ∅ = γ D + (⊥ + ) = γ D + • S
x ← e + (X, V ) Else, vars(e) ⊆ V . We develop the right-hand term, defining an auxiliary term T .

γ D + • S x ← e + (X, V ) = γ D + (S x ← e (X), V ∪ {x}) = t | U t ∈ γ D • S x ← e (X), U ⊆ V ∪ {x} ⊇ t | U t ∈ S x ← e • γ D (X), U ⊆ V ∪ {x} ⊇ t | U t ∈ γ D (X), t = t[x → u], u ∈ E e t, U ⊆ V ∪ {x} def = T
Let us show that for all s ∈ S x ← e • γ D + (X, V ) def = S, then s ∈ T . We have to find the corresponding t, U and u ∈ E e t. s ∈ S implies the existence of an environment s and a value v.

Let t = s ∈ γ D (X), u = v, U = W ∪ {x} and t = t[x → u]. The equality s = s | W [x → v] = (s[x → v]) | W ∪{x} = t | U
is valid on the whole domain W ∪ {x}. Now, we must show that t | U is in T . First, we do have that t ∈ γ D (X) as s = t and s is an element of the concretization. Then, we must show that u ∈ E e t. The equality s = t implies that u = v ∈ E e s = E e t. Finally, U ⊆ V ∪ {x} as U = W ∪ {x} ⊆ V ∪ {x}. This concludes the proof that s ∈ T , and so

S x ← e • γ D + (X, V ) ⊆ γ D + • S x ← e + (X, V )
The proof for the parallel assignment can be done likewise. The proof for the arithmetic condition is similar. We used the fact that if an expression e can be computed on a environment s restricted over the set of variables W , that is E e s | W = ∅, then extending the domain will yield the same set: E e s | W = E e s. If vars(e 1 ) and vars(e 2 ) ⊆ V then

C e 1 e 2 • γ D + (X, V ) = C e 1 e 2 ({s | W |s ∈ γ D (X), W ⊆ V }) = s | W s ∈ γ D (X), W ⊆ V v 1 ∈ E e 1 s | W , v 2 ∈ E e 2 s | W , v 1 v 2 = {s | W |s ∈ C e 1 e 2 • γ D (X), W ⊆ V } ⊆ {s | W |s ∈ γ D • C e 1 e 2 (X), W ⊆ V } = γ D + (C e 1 e 2 (X), V ) = γ D + • C e 1 e 2 + (X, V )
Else, if V is too small, then the second line will be equal to the empty set as no W and no v 1 or v 2 can be found. The empty set is equal to the concretization of γ D + • C e 1 e 2 + (X, V ) in the case where V does not contain the variables of e 1 and e 2 .

From global to local invariant We saw that in traditional flow-sensitive analysis, the semantics of the program is computed with a function F applied on an element S of D |L| . F itself applies transfer functions on each abstract environment S of D. The soundness of the abstract semantics with respect to the concrete one is proven with the concretization function γ D from abstract environments in D to set of concrete environments in P (E). Then, we link these different sets to their labels, obtaining the set of states P (L × E). In our case, we won't have one abstract environment per label, so we do not have an element of D |L| for our invariant, but instead a single environment in our overlay D + for all labels. So we will still have a concretization function γ D + from D + to P (E) but then we have to define how to get the set of states P (L × E).

We decided to leave this job to a concretization function γ : D + → P (L × E). Let us consider a definition where every label is associated to any environment from the concretization.

γ(X + ) = {( , s)| ∈ L, s ∈ γ D + (X + )}
This concretization function is monotone in X + , as γ D + is also monotone in X + .

Associating the complete concretization to each program point is a significant overapproximation. We can actually be more precise by considering s ∈ γ D + (X + ) for label only if the variables of s, its domain, may all be defined at . Consider for instance the program of Figure 7. At program point 1 , only i 1 is defined. There is no need to consider the partial function {i 1 → 1, j 1 → 0} as j 1 cannot be defined. We did not present this more precise γ for the sake of concision.

Abstract semantics

In this Section, we define the abstract semantics computed by the analysis. We prove that it is sound, with respect to the concrete semantics given to the SSI form of the program.

Abstract semantics soundness Let F be the abstract transfer function of the program. Any post-fixpoint X + ∈ D + of F is a sound approximation of the concrete semantics if P ⊆ γ(X + ). Where P is the concrete semantics of P given in the previous section, that is to say the least fixed point of the concrete transfer function F ( P = lfp(F )). We saw with the fixpoint transfer theorem that this condition on post-fixpoint is a consequence of F • γ ⊆ γ • F , provided that F and γ are monotonic (Theorem 2.2). We already proved the monotonicity of F and γ. Let us define F , prove that it is monotonic and that it respects the condition of the fixpoint transfer theorem.

Transfer function In the concrete semantics, we defined for each edge → ∈ E, a transfer function T → = T φ • T f • T σ , where T φ and T σ are parallel assignments transfer functions, and T f corresponds either to the semantics of an assignment or an arithmetic condition, depending on the edge → . We defined the abstract semantics of an edge similarly. Let us suppose that,

T σ = S x 1 ← x 1 | . . . |x n ← x n T φ = S y 1 ← y 1 | . . . |y m ← y m Then T → def = T φ • T f • T σ T σ def = S x 1 ← x 1 | . . . |x n ← x n T φ def = S y 1 ← y 1 | . . . |y m ← y m Also, if T f = S x ← e then T f def = S x ← e . Else, if T f = C e 1 e 2 then T f def = C e 1 e 2 .
As the abstract semantics of assignment and arithmetic condition are sound, one can show that their composition is sound too. Thus T → is a sound approximation of T → : for any X + ∈ D + ,

T → • γ D + (X + ) ⊆ γ D + • T → (X + )
F as a composition Let us define a new F as a composition of transfer functions F → each associated to one edge (the order of the composition does not matter for soundness, only for efficiency of the fixpoint iteration). We also define F 0 , the transfer function that will add the abstract environment for the entry point, that we note X + 0 (S 0 ⊆ γ D + (X + 0 )).

F def = F 0 • ( → )∈E F → Let F → (X + ) def = X + ∪ T → (X + ) and F 0 (X + ) def = X + 0 ∪ X + .
We will make all our proofs using the facts that

X + + F → (X + ) and T → (X + ) + F → (X + ) X + + F 0 (X + ) and X + 0 + F 0 (X + )
We need to ensure that this F is sound with respect to F and γ. To do so, we will use a small lemma, that ensures that F is monotonic.

Lemma 3.3.

[Monotony] F is monotonic, that is for any X + and Y + in D + ,

X + + Y + =⇒ F (X + ) + F (Y + )
Proof. For each edge e, F e is monotonic so their composition is monotonic too. Finally, F 0 is monotonic, so F is monotonic. Theorem 3.4. [Soundness] F respects the condition of the fixpoint transfer Theorem 2.2 with respect to F and γ, that is to say

F • γ ⊆ γ • F . Proof. Let X + ∈ D + and S def = γ(X + ) = {( , s)| ∈ L, s ∈ γ D + (X + )}.
The proof consists in proving the two inclusions:

F • γ = F (S) ⊆ γ(X + 0 ) ∪ ( 1 → 2 )∈E γ • T 1 → 2 (X + ) ⊆ γ • F (X + ) = γ • F 0 • e∈E F e (X + )
Let us show the first one, F • γ is included in the union of γ • X + 0 and the union of γ • T 1 → 2 over the edges 1 → 2 ∈ E. First, at line 3, we unpair in each state the label from the environment s. As any label can be associated with any environment, we did overapproximate the set of states. At line 4 we no longer give only the set of environments S 1 to the transfer function T 1 → 2 , but instead we give all the environments computed, for all labels. This overapproximation is possible as the T 1 → 2 are monotonic. We then exploit the soundness of T 1 → 2 and X + O at line 5.

F • γ(X + ) = F (S) (1)
= ( , s) ( → ) ∈ E, s ∈ T → (S ) ∪ {( 0 , s)|s ∈ S 0 } (2) ⊆ ( , s) ( 1 → 2 ) ∈ E, s ∈ T 1 → 2 (S 1 ) ∪ ( , s) ∈ L, s ∈ S 0 (3)
⊆ ( , s) ( 1 → 2 ) ∈ E, s ∈ T 1 → 2 ( ∈L S γ D + (X + ) ) ∪ ( , s) ∈ L, s ∈ γ D + (X + 0 ) ( * ) (4)
⊆ ( , s) ( 1 → 2 ) ∈ E, s ∈ γ D + • T 1 → 2 (X + ) ∪ γ(X + 0 ) (5)
= γ(X + 0 ) ∪

( 1 → 2 )∈E γ • T 1 → 2 (X + ) (6)
This final result is included in γ • F . First, let us show by induction on the number of edges that the right term is a subset of γ • e∈E F e (X + ).

• If E = ∅, then the union is an empty set. The inclusion is trivial.

• If there is only one edge e ∈ E, then we can conclude by simply applying the monotonicity of γ γ • T e (X + ) ⊆ γ • F e (X + )

• Else, let us suppose that E = E ∪ {e} and that we have proved the inclusion on E :

e ∈E γ • T e (X + ) ⊆ γ • e ∈E F e (X + ). Also, we have X + + e ∈E F e (X + ). Then

e ∈E γ • T e (X + ) = γ • T e (X + ) ∪ e ∈E γ • T e (X + ) (1)
⊆ γ • T e (X + ) ∪ γ • e ∈E F e (X + ) def = C(X + ) (2) = γ • T e (X + ) ∪ γ • C(X + ) (3)
⊆ γ • T e • C(X + ) ∪ γ • C(X + ) (4)
⊆ γ • F e • C(X + ) = γ • F e • e ∈E F e (X + ) (5) = γ • e ∈E F e (X + ) (6)
We use the monotonicity of T e to get line 4 from the previous one. We then use the hypotheses on F e and the soundness of ∪ to get the next line.

Thus the inclusion holds for any set of edges E. In the end,

F • γ(X + ) ⊆ γ(X + 0 ) ∪ ( 1 → 2 )∈E γ • T 1 → 2 (X + ) ⊆ γ(X + 0 ) ∪ e ∈E F e (X + ) ⊆ γ • F 0 • e ∈E F e (X + ) = γ • F (X + )
So F satisfies the condition of the fixpoint transfer theorem.

Precision In the beginning of this last proof, the line ( * ) raises an issue for precision. From this line, we no longer say that s is an element of S 1 = T 1 → 2 (S 1 ). This set of environments corresponds to the application of the transfer function of an edge 1 → 2 on the environments at 1 . Now we apply this transfer function on all environments. Especially, we apply the transfer function even if the set of environments at 1 could be empty (the branch is never taken). From this point, we loose all information on the control flow.

Example Consider that the current abstract environment is (X, V ) with

X def = {j 2 ∈ [0, 4], i 2 = j 2 + 1, j 4 ∈ [0, 4], i 4 = j 4 + 1}, V = {i 2 ,
j 2 , i 4 , j 4 } and we are examining the program of Figure 7 3 . We need to apply the transfer function of the edges 3 → 4 and 4 → 5 . With the first one, the invariant forget that i 4 = j 4 + 1 as we assign it a new value. But we also loose the relation between i 2 and i 4 , as we make an abstract union with (X, V ) which does not have such relation.

F 3 → 4 (X, V ) = S i 4 ← i 2 + 1 + (X, V ) ∪ (X, V ) = ({j 2 ∈ [0, 4], i 2 = j 2 + 1, j 4 ∈ [0, 4], i 4 = i 2 + 1}, V ∪ {i 4 }) ∪ (X, V ) = ({j 2 ∈ [0, 4], i 2 = j 2 + 1, j 4 ∈ [0, 4], i 4 ∈ [1, 6]}, V ) = (X , V )
Then we apply the transfer function of the other edge.

F 4 → 5 (X , V ) = S j 4 ← j 2 + 1 + (X , V ) ∪ (X , V ) = ({j 2 ∈ [0, 4], i 2 = j 2 + 1, j 4 = j 2 + 1, i 4 ∈ [1, 6], }, V ∪ {j 4 }) ∪ (X , V ) = ({j 2 ∈ [0, 4], i 2 = j 2 + 1, j 4 ∈ [0, 5], i 4 ∈ [1, 6]}, V )
There we see that the relation between i 4 and j 4 has been lost. Because we have one invariant for the whole program, we cannot prevent the application of the transfer function on all environments. To still retain some information, we need to delay this broad application as much as possible. Instead of applying the transfer function per edge, we want to apply them per bloc. A bloc is a path with no ingoing or outgoing edges in the intermediate program points, for instance, in Figure 4a The transformation to SSI is not our main contribution, as it is based on an already existing algorithm [START_REF] Pereira | Static Single Information form[END_REF]. However we choose a different formalism, based on the CFG, to conform to the state of the art in abstract interpretation.

0 → 1 → 2 → 7 → 8 .
What we mean by "apply per block" is that if in the CFG, there is a bloc from 1 to 2 , then the composition of all transfer functions along this path can be applied on the abstract environment.

F 6 → 2 • • • • • F 2 → 3 (X + ) Becomes =⇒ X + ∪ T 6 → 2 • • • • • T 2 → 3 (X +
) Thus, if an arithmetic condition is not satisfied along the path, resulting in a bottom abstract environment, none of the next transfer functions will be applied.

Example In the case of our example program, we build the paths p

1 def = 0 → 1 → 2 , p 2 def = 2 → 3 → 4 → 5 → 6 → 2 and p 3 def = 2 → 7 → 8 . The path p 1 has the transfer function S i 1 ← i 0 |j 1 ← j 0 • S j 0 ← 0 • S i 0 ← 1 . The path p 2 has the transfer function S i 1 ← i 4 |j 1 ← j 4 • id •S j 4 ← j 2 + 1 • S i 4 ← i 2 + 1 • C j 2 < 10 • S i 2 ← i 1 |j 2 ← j 1
By composition, this last transfer function only requires i 1 and j 1 to be defined in the abstract value. Also, if j 1 is never strictly less than 10, then the condition C j 2 < 10 will always result in a ⊥ + value. Then none of the following semantic functions will define the variables i 2 , j 2 , i 4 , j 4 which will not be defined in the final invariant.

Implementation

The analysis presented before, which consists in finding the least fixpoint of some abstract transfer function, was implemented in OCaml. It takes as input a program in While language with assertions. The analysis has an option to choose between an octagon or polyhedra abstract domain. The output is the global invariant of the program (expressed as a value of the abstract domain). The analysis is iterative and does not implement acceleration techniques. If the fixpoint is indeed found, then each assertion of the original program is checked, and whether it passes or not is printed.

This analysis is based on a existing parser for the While language which outputed the CFG of the input program. The algorithm to transform this CFG into an SSI form will not be detailed here as an efficient transformation can be found in [START_REF] Appel | Modern Compiler Implementation in Java[END_REF] (efficient computation of the dominance tree necessary) and [START_REF] Pereira | Static Single Information form[END_REF] (actual transformation). The main difference between our algorithm and the one cited is that we perform the algorithm on a CFG, so the nodes are program points, while in the cited one the nodes are instructions. In our implementation, the output is a value of type ssiPrgm. This structure contains information on the program such as its variables, the CFG, or also the φ-and σ-nodes attached to each label. (Arrays are often used to represent a total map with labels as key.) For abstract domains we used the Apron library [START_REF] Jeannet | Apron: A library of numerical abstract domains for static analysis[END_REF]. The Apron module is a OCaml interface to the C implementation of the library. It offers a common interface for various abstract domains (such as interval, octagon, polyhedra, etc). Its architecture separates the manager of the abstract domain from the user-interface that can for example ask the creation of a new abstract value, join or meet existing ones, perform assignment or restrict an abstract value to satisfy a linear constraint. Thanks to this library, we were able to write an analysis using the user-interface, and then test it for different abstract domains.

As for the analysis itself, it is composed of two main steps: the extraction of the transfer functions and the iteration until a fixpoint is found. The first step begins with the extraction of the blocs from the SSI form. Then for each of these blocs 1 → • • • → n we compute its transfer function

T 1 →•••→ n (X + ) def = T n-1 → n • • • • • T 1 → 2 (X + ).
After that, the analysis starts from S + 0 (that is the abstract state where only the arguments are defined, without any constraint on them), and iterates

until a fixpoint is reached. Let F 1 →•••→ n (X + ) def = X + ∪ T 1 →•••→ n . At each step, the analysis applies all F 1 →•••→ n in composition.
A verbose option allows to observe the change on the abstract value each time a transfer function is applied. It also highlights the transfer function that can be applied or not (due to our abstract semantics in D + that only apply the transfer function of D if all the necessary variables are present).

The analysis, which take the SSI program as input and displays the invariant and the summary of assertions, corresponds to about 500 lines of OCaml code. The transformation to SSI, which do not include a cleanup phase (to propagate copy and remove useless variables), corresponds to the same amount.

The prototype currently does not handle convergence acceleration, in the form of a widening operator for instance. Its iterations are bounded by an arbitrary number. (If the fixpoint is not reached in this time, the resulting invariant is not correct.) If the fixpoint is found, each assertion in the original program is evaluated with respect to this invariant to check whether they can be verified by the analysis. As invariant can be complex to read this also significantly help measure precision of the analysis. Notice that the assertion are merely conditions with only one successor and can be extracted after the conversion to SSI. This means that the variables used in it are correctly indexed with the accessible version of the variable, and there is no other transformation to perform. Apron already provides the necessary function to test whether an abstract value satisfies or not a constraint.

Example Let us consider the program from Figure 4a.

First, the program is put in SSI form. Then the Blocs are created. The assertion points are extracted from the CFG. A condition in the CFG is an assertion if it has only one successor. (That is why the condition 5 → 2 , is considered to be an assertion.)

> ./ analyse -invaroct 16 example / ex . c Transforms made (3 blocs ) - ----------------------- -------------------------

The number of iteration has been here fixed to 16, and the abstract domain used is the octagon one. It takes 14 iterations for the analysis to reach a fixpoint without any convergence acceleration. The invariant in the octagon domain is very verbose and we elude it here.

Variables : [|0 > i : int ; 1 > i_0 : int ; 2 > i_1 : int ; 3 > i_2 : int ; 4 > i_3 : int ; 5 > i_4 : int ; 6 > j : int ; 7 > j_0 : int ; 8 > j_1 : int ; 9 > j_2 : int ; In this case, the fixpoint is reached and so the assertion points are checked.

For the polyhedra domain, the fixpoint is reached in the same amount of steps and the assertions are satisfied, but the invariant is concise. [| -i_1 + j_1 +1=0; -i_2 + j_4 =0; -i_2 + j_2 +1=0; -i_2 + i_4 -1=0; j_3 -10=0; j_0 =0; i_3 -11=0; i_0 -1=0; -i_1 + i_2 +1 >=0; -i_2 +10 >=0; i_2 -1 >=0; i_1 -1 >=0|]

In this invariant, one can observe that the relation i = j +1 is preserved for all matching versions (same index) of i and j.

We then also tested the implementation on a variant of the program. This variant has an argument c, which we constraint to be between 1 and 9.

i f ( c > 0 and c < 1 0 ) then i = 1 ; j = 0 ; while ( j <= c ) do i = i + 1 ; j = j + 1 ; done ; assert ( i >= c + 2 ) ; s a t assert ( i = j + 1 ) ; s a t i f ( 5 < i ) then assert ( 4 < j ) ; s a t e l s e assert ( 4 >= j ) ; s a t endif e l s e skip endif With the octagon domain the fixpoint is reached in 13 iterations. However the polyhedra domain needs 22 iterations. This echoes with Astrée [START_REF] Cousot | The ASTRÉE analyzer[END_REF] using the more time efficient octagon domain rather than the polyhedra one. Loosing in precision by making broader approximations accelerates the convergence.

Efficiency One global invariant was the solution to avoid multiple memory-consuming invariants. However in practice we do not have one invariant at any time. Indeed, we define the abstract semantics of path transfer function as a union of the previous invariant and the one on which the transfer functions of the edges have been applied. Thus we need two abstract values to be able to compute the abstract union. Apron does provide an in-place union of assignment: the fold operator [START_REF] Gopan | Numeric domains with summarized dimensions[END_REF] (also called weak-update). Folding the variable w in v on the abstract value X is the same as making the union of X and S v ← w X and then remove w from the possible variables:

γ D • fold (w,v) (X) def = {s[v ← w] | V\{w} |s ∈ γ D (X)} ∪ {s | V\{w} |s ∈ γ D (X)}
Unfortunately this operator can only perform a weak-update for one variable at a time. We saw in the previous section that applying the union between each assignment makes us lost all precision. The fold is thus not a solution. Thus for now, the prototype keeps in memory two invariants.

Conclusion

The goal of this internship was to design a static analysis that combines efficiency -the analysis must be sparse with only one invariant for the whole program -with precision -it must keep properties between several variables, not just properties on single variables. Static analyses allows to check the correct behaviour of a program without executing it, only by looking at its source code. Besides safety verification, it is also used to perform sound optimizations. For instance ABCD [START_REF] Bodík | ABCD: eliminating array bounds checks on demand[END_REF] removes unnecessary bound checks and GVN [START_REF] Barry K Rosen | Global value numbers and redundant computations[END_REF] removes redundant computations, both optimizations being safe with respect to the semantics of the program. These analyses are efficient, but their techniques are not easily reusable for other analyses. They are designed for specific purposes. The theory of Abstract interpretation is a framework of mathematical concepts and theorems that allow the design of analyses in a more generic way. It also provides generic proof of the soundness of such analyses, unlike the specific proofs of ABCD or GVN. The principles of this theory are versatile, the precision of the analysis (dependent of the abstract domain) or the semantics of the language can be easily changed. That is why we chose Abstract interpretation to design our analysis.

We target numerical analyses, that is analyses tracking the values of variables. Depending on the abstract domain chosen, the expressivity available for these properties varies, and can allow more precise conclusions. Numerical domains are usually classified into two categories: relational or non-relational. In a relational domain, one can express properties between several variables, for instance "x is less than y", while it is not possible in a non-relationnal one.

State-of-the-art analyses for non-relational properties are quite efficient as they benefit from representations of the program that helped them by giving more information, in a more practical way. A popular example of such representation is the SSA form [START_REF] Lattner | LLVM: A compilation framework for lifelong program analysis & transformation[END_REF]. It makes explicit the defuse chains, and gives for each program point, for each variable used at this program point, the last definition of the variable, using indexing of variables to ensure the unicity of this definition. Unfortunately, such representation of the program is not enough to perform efficient relational static analyses.

Our goal was to design a sparse static relational analysis based on Abstract Interpretation and on a convenient representation of the program, the SSI form [START_REF] Pereira | Static Single Information form[END_REF]. We define an analysis as sparse if it computes one invariant for the whole program, instead of one per program point. For instance ABCD is sparse. Abstract Interpretation theory designs analyses with one invariant per program point, but sparser relational analysis are possible, as shown with the tool PAGAI [START_REF] Henry | PAGAI: A path sensitive static analyser[END_REF]. This analyzer computes invariant per assertion points (chosen by the end user) and at the loop head. We want to reach higher sparsity.

To compute a unique invariant, while keeping precision, we used or designed several elements for the analysis. First, we needed to have several versions of the variables, to distinguish in the invariant several moments of their lives. More concretely, the live-range of the variables is split when the information about them changes. The SSI form guarantees this property. Then, we needed to define an overlay of abstract domains that can represent partial functions. This is new in Abstract Interpretation, where abstract domains represent total functions (both in theoretical explanations [START_REF] Miné | Tutorial on static inference of numeric invariants by abstract interpretation[END_REF] or concrete implementation of abstract domains [START_REF] Jeannet | Apron: A library of numerical abstract domains for static analysis[END_REF]). In this report, we showed that such overlay does not allow an abstract domain organized on a complete lattice, which is more convenient but not mandatory for Abstract interpretation. Despite the weaker property on our overlay, we were still able to design a sparse analysis that uses it, and we were able to prove its soundness with respect to the concrete semantics of the program.

In addition, we implement a prototype of this analysis in OCaml, using the Apron library [START_REF] Jeannet | Apron: A library of numerical abstract domains for static analysis[END_REF] to manage abstract domains, and an existing parser to extract the CFG of a program. This prototype helped evaluate the precision and efficiency of the program on concrete cases. The concrete benefits of such analysis should now be studied on real-life examples. Its efficiency is a balance between the number of variables introduced by the SSI form (at worst O(N ) for each variable, with N the size of the program) and the number of invariants removed with the sparsity policy (N , that is one per program point). The abstract domain plays an important role here, as the linear increase of number of variable can be a polynomial increase of time cost depending on the domain. For instance, the polyhedra domain is known [START_REF] Henry | PAGAI: A path sensitive static analyser[END_REF] to perform badly with more variables. A solution, implemented in PAGAI [START_REF] Henry | PAGAI: A path sensitive static analyser[END_REF], is to remove variables when they are equal to an affine combination of the other variables. Such solution is domain-specific and was thus not studied here.

In conclusion, this works proves the possibility of designing a sparse relational static analysis. It should now be compared with existing analyzer such as PAGAI, to determine its benefits or drawbacks on efficiency on concrete cases. This a future work that requires a more clever implementation than the current prototype. This prototype still lack a widening operator to guarantee convergence of the analysis. Also, the precision of the analysis should be compared to a flow-sensitive one. Although some intuition was given during the proofs of correctness, we need now to prove the importance of the SSI form to keep precision.

  Intersection detected, but there is no concrete execution in the intersection. It is a false alarm.

  Intersection detected, and there is concrete executions in the intersection. The program is unsafe

Figure 1 :

 1 Figure1: The approximation of the executions must at least cover the concrete executions. In case of intersection between the forbidden executions and the approximation, an alarm is raised

  Hasse diagram of (N, ≤). {a, b, c} {a, c} {a, b} {b, c} {a} {b} {c} ∅ (b) Hasse diagram of (P(X), ⊆) where X = {a, b, c}. Hasse diagram of the sign poset.

Figure 2 :

 2 Figure 2: Hasse diagrams of different posets.

Definition 2 . 6 .

 26 [Concretization] Let (A, ) and (C, ≤) be two posets. A concretization function γ : (A, ) → (C, ≤) is a monotonic (i.e. ∀x, y ∈ A, x y =⇒ γ(x) ≤ γ(y)) function associating to each abstract element of A a concrete element in C. For instance, let us consider a concrete poset for sets of integers: (C, ≤) = (P(Z), ⊆). We decide to use the intervals to represent the sets: A = {[a, b]|a ∈ Z ∪ {-∞}, b ∈ Z ∪ {+∞}, a ≤ b}. For the order, we choose the inclusion of intervals: [a, b] [c, d] if and only if a ≥ c and b ≤ d. (A, , , ) is the lattice of intervals. Then the concretization simply corresponds to all integers between the bounds γ([a, b]) = {x ∈ Z|a ≤ x ≤ b}. It is important to understand that [a, b] is merely a notation, not the actual set of integers between the bounds.

Theorem 2 . 2 .

 22 [Fixpoint transfer] Let C be a complete lattice and A a poset, with the concretization function γ : A → C being monotonic. Let F : C → C be a monotonic function in the concrete realm, and F : A → A be a function in the abstract one

Figure 3 :

 3 Figure 3: Syntax of the While language

  The CFG of the program

Figure 4 :

 4 Figure 4: The CFG of some program in the While language

Figure 5 :

 5 Figure 5: Some examples of abstract domains. The dots represent concrete configurations. The gray zone is the abstract representation of the configurations, depending on the domain.

Figure 6 :

 6 Figure 6: Example of representation in SSA form and then back to an executable one

  i

=. 1 (← (j 1 ) i 4 φ← 4 φ←

 144 F (S) the result (and we note F (S)( ) = S ). S is the set of environments attached to in the invariant S . Let us define what should be S for each . Recall that the set of environments at the entry point 0 was defined as S 0 . Then, S 0 def = S 0 . Let T → be the transfer function of an edge from . . . . . , i 2 : 2 , . . . ) σ ← (i 1 ) (. . . , j 2 : 2 , . . . ) σ (. . . , i 3 : 1 , . . . ) j (. . . , j 2 : 1 , . . . ) 2 . . .i 3 ← e(i 2 , j 2 )

Figure 9 :

 9 Figure 9: Transfer function for some edge 1 → 2

6 • C + 2 ,

 62 the plane (b,c), by b = c ∈ [4, 6] • C + 1 , in the space (a,b,c), by a = c and if c ≤ 4, b = 4, if c ∈ [4, 6], c = b and if c ≥ 6, b = in the space (a,b,c), by a = c = b

Figure 10 :

 10 Figure 10: Example of impossible least upper bound with three variables

  V ) If vars(e 1 ) ∪ vars(e 2 ) ⊆ V ⊥ + Otherwise S x ← e + ⊥ + = ⊥ + and S x 1 ← e 1 | . . . |x n ← e n + ⊥ + = ⊥ + and C e 1 e 2 + ⊥ + = ⊥ + Theorem 3.3.[Soundness of the new operators] The operators of the new abstract domain are sound with respect to the concrete semantics.

  -Bloc 0 [| j_3 <-j_1 | i_3 <-i_1 |] /* Parallel assignements */ (\/ [| j_3 -_i , n 10 >= 0|]) /* Condition . Dijunction of conjunctions */ {\/ [|11 -_i , n i_3 = 0|]} /* Assertion . Idem */ Bloc 1 [| j_2 <-j_1 | i_2 <-i_1 |] (\/ [|10 -_i , n j_2 > 0|]) [| j_4 <-j_2 + _i , n 1|] [| i_4 <-i_2 + _i , n 1|] {\/ [| j_4 + _i , n 1 -_i , n i_4 = 0|]} {\/ [|0 -_i , n 0 = 0|]} [| j_1 <-j_4 | i_1 <-i_4 |] Bloc 2 [| j_0 <-0|] [| i_0 <-1|] [| j_1 <-j_0 | i_1 <-i_0 |]

40 10 >

 10 j_3 : int ; 11 > j_4 : int |] Checking the assertion points l7 : Assert {\/ [|11 -_i , n i_3 = 0|]} is satisfied l5 : Assert {\/ [|0 -_i , n 0 = 0|]} is satisfied l4 : Assert {\/ [| j_4 + _i , n 1 -_i , n i_4 = 0|]} is satisfied

  , 2 → 3 → 4 → 5 → 6 → 2 is a block, but not

				Our work
	Program (with assertions)	to CFG	to SSI	Analysis	Assertions checked and Invariant
	Abstract domain			Apron
	Figure 11: Workload of the prototype

Whether we take the predecessors or successors actually depends on the analysis performed. In this report we consider a forward analysis, where the predecessors are taken.

Actually, the variables have the same value if they are alive at the program point considered.

In practice i1 and j1 should also be in V in this example, but it has no influence on the precision lost we explain here.

Abstract union

We need to define an abstraction of the concrete union of sets of environments. However, it is not possible to define a join. A counter example can be found using a geometric approach.

Geometric approach Environments can be represented as points in a geometric space where the dimensions are the variables. An abstract environment overapproximates a set of environments, that is a set of points in the geometric view. All the elements of D can be represented as a set of points in the space defined by the variables V. However, elements of D + are defined over different sets of variables. We represent them in their respective subspace. For instance, let us consider that the variables are V = {a, b, c} and that we have A + = (A, {a, c}) such that the environments in the concretization of A satisfies a = c. A + is a line in the plane defined by {a, c}. But A is an element of D defined over the variables V. A has no constraint on b. A is thus a plane in the 3D-space defined by V. This is illustrated on Figure 10.

For the partial order A + B + , the two objects A + and B + may not be defined in the same geometric space: V A can be different of V B , but we still want to compare the abstract values. To do so we compare A with the projection of B onto the variables of V A (remember that V A ⊆ V B by the definition of the partial order). It is an existential projection: all variables not in V A are unconstrained by the projection. Let us consider A + as in the previous example and C + 2 = (C 2 , V) from the Figure 10, defined with the environments in its concretization satisfying a = c = b. Let us check that

Second, the projection of C 2 onto V A consists in forgetting the constraint on b. The projection of C 2 should thus be the plane in V defined by a = c, which is exactly A and thus confirm the order A C 2 , and then A + + C + 2 . To demonstrate that a join cannot be defined, we need the following lemma that guarantees that the least element that is greater than two other elements is necessarily defined over the union of their variables. Lemma 3.1. [Minimal variable size] Let (A, V A ), (B, V B ) and (C, V C ) be three elements of our abstract domain D + . Then if the latter is greater than the first two, (A, V A ) + (C, V C ) and (B, V B ) + (C, V C ), then we can define an intermediate element in the poset that is greater than the first two but is less than

Proof. By definition of the order, V C must include V A and V B . Also, by definition of the projection, for any set of variables V , C proj V (C). In particular, it holds when

As for the first order, A proj V A (C) by definition of the partial order and

This lemma ensures that the least upper bound of two elements must be defined over the union of their variables, or a lesser element could be deduced from it.

Counter example to join For this counter example we use the geometric approach to show that there exists at least one case where for two abstract environments (A, V A ) and (B, V B ), there does not exist a least element (C, V C ) such that (A, V A ) + (C, V C ) and (B, V B ) + (C, V C ). This means that we cannot define a join + for our domain: it would not be defined for any A + and B + . Let A be defined over V A = {a, c} with as a constraint (a = c), and B defined over V B = {b, c}