Cette dernière décennie a vu l'essor des analyses statiques plus seulement réservées aux systèmes embarqués critiques (avions, métros, fusées, etc.), mais maintenant disponibles plus largement, comme le montre l'implication de compagnies telles que Google ou Facebook dans le domaine.

Néanmoins, prouver l'absence de bugs d'un logiciel, (problème que nous savons depuis Turing et Cook être intrinsèquement difficile) n'est pas le seul challenge en développement logiciel. En effet, la complexité toujours croissante des logiciels induit un besoin toujours croissant d'optimisations fiables.

La résolution de ces deux problèmes (fiabilité, optimisation) impose le développement de méthodes d'analyse statique sûres (sans faux négatifs), efficaces (en temps et en mémoire), mais suffisamment précises (avec un taux faible de faux positifs). La recherche de tels compromis est au coeur de mes travaux, qu'ils s'appliquent à la vérification formelle ou au domaine plus contraint des analyses pour les compilateurs.

Les travaux détaillés dans ce manuscrit décrivent mes activités de recherche pendant la période de 2009 à 2017. Durant cette période, j'ai contribué aux développements d'analyses statiques appliquées aux deux domaines connexes que sont la vérification de logiciels et la compilation. Les analyses proposées sont développées dans le cadre de l'interprétation abstraite, pour des domaines numériques, et plus récemment, des domaines mémoire. Elles font de plus l'objet de validation expérimentale en terme de précision et de coût, ainsi que de leur impact dans des analyses clientes (terminaison, optimisations) lorsque cela est pertinent.

HDR Laure Gonnord II/92

Summary

This last decade was the occasion to see the rise of static analyses that are now no longer reserved for critical embedded systems (airplanes, subways, rockets, etc.). They are now more widely available, as evidenced by the novel implication of companies like Google or Facebook in the domain.

Nevertheless, proving the absence of bugs in a given software (problem which has been known to be intrinsically hard since Turing and Cook) is not the only challenge in software development. Indeed, the ever growing complexity of software increases the need for more trustable optimisations.

Solving these two problems (reliability, optimisation) implies the development of safe (without false negative answers) and efficient (wrt memory and time) analyses, yet precise enough (with few false positive answers). Finding such compromises is the core of my works, whether it deals with formal verification or the more specific domain of analyses inside compilers.

The work which is detailed in this manuscript was done over a period going from 2009 to 2017. During this period, I contributed to static analyses in the two related domains that are software verification and compilation. The proposed analyses have been developed within the abstract interpretation framework, for numerical domains, or, more recently, memory domains. They are also experimentally validated, according to precision and cost criteria, and also according to their impact on client analyses (termination, code optimisation) whenever appropriate.

HDR Laure Gonnord III/92

Program Optimisation

Software reliability has always been one of the major issues in Computer Science, as the spectacular accident of Ariane 5 in 1996 illustrated. The accident is described in these terms in the accident report 1 : "Only about 40 seconds after initiation of the flight sequence, at an altitude of about 3700m, the launcher veered off its flight path, broke up and exploded". The cause of this accident was the use of the code of the preceding rocket model, Ariane 4, which was not retested in the correct environment. In the last two decades, a series of accidents caused by software has led the NASA to refresh their validation methodology [START_REF] Brat | Experimental evaluation of verification and validation tools on martian rover software[END_REF]. Other software related accidents were even more critical in terms of human lives, for instance the Panama radiotherapy accident [START_REF] Borrás | Overexposure of radiation therapy patients in Panama: problem recognition and follow-up measures[END_REF] in 2000, that caused the death of 21 patients who received an overdose of radiotherapy treatment induced by a bug in the software.

Many complementary approaches exist to deal with software reliability, from software engineering, development methodology, formal methods based development, as well as testing and proofs [START_REF] Jackson | A direct path to dependable software[END_REF]. All these techniques have proved their efficiency in the development of safety critical systems such as space rockets, airplanes, nuclear plant controllers, automatic subways. Among all the tools of this ecosystem, let us cite the ASTRÉE code analyser [START_REF] Blanchet | A static analyzer for large safety-critical software[END_REF] which was capable of proving the absence of runtime errors of the "primary flight control software of an Airbus model" 2 . However, all these techniques cause a huge overhead on the software development process, and for the moment, they did not have a huge impact on the development of non critical systems such as laptop operating systems or hardware. This is especially due to the fact that:

• They have a huge impact on the development duration.

• They have a cost in terms of human resources.

• The analyses and tools were developed for the specific domain of safety critical systems, where code rules can be imposed to developers, and assumptions can be made on the shape of the code they produce. These constraints are clearly unreasonable in other contexts.

• The analyses and tools were developed for development environments that do not include aggressive code optimisation, since safety-critical systems are designed to be simple and usually run on over-sized platforms.

In the last decade nevertheless, the ever-growing number of static analysis tools demonstrated the need for safer (mode generalist, less critical) code as well as the visibility of the scientific community of static analysis 3 . Start-ups as well as major companies have developed their tools for the growing market of software validation. Among the commercial tools we can cite GrammaTech's Code Sonar 4which focuses on code security and Facebook's Infer 5 that provides a precise diagnostic of memory management.

All these techniques and tools mainly prove the absence of bugs in their specialised area of application, or gives hints to the developer for a better understanding of his code, but they address only a part of the challenges toward software reliability. I believe that the effort to design a better code and prove the absence of errors has to be continued in two complementary directions: applicability (static analysis for every developer) and expressivity (static analysis for everyday problems). My work on static analyses for verification and compilation follows this philosophy: static analyses must verify but also be used to optimise runtime and memory footprint of programs. However, static analyses inside compilers are lagging far behind the state-of-the-art of static analyses for software verification or bug tracking. Clearly, the usage in compilers avoid the use of unsound techniques (all faulty behaviours should be detected); moreover, the complexity of the compiler code itself advocates for the design of "easy-to-implement" static analyses and code optimisations (bugs in compilers are frequent and a major issue [START_REF] Sun | Toward understanding compiler bugs in GCC and LLVM[END_REF]).

The success story of the Compcert compiler 6 and the Verasco 7 project show that we can design certified (proved by the Coq theorem prover) compilers and static analysers for general C programs. However the optimisations that are proposed in these two tools are still very far from the current production compilers, in which aggressive and clever optimisations are made. To bridge the gap between the two communities (static analysis and code optimisation), we propose to design abstractinterpretation based static analyses, which are correct by-construction (as opposed to formally validated in Coq) and scalable enough to provide useful information for further optimisations.

My current research concerns the development of dedicated static analyses for verification and compilation, that are capable to express complex properties at a reasonable cost. My contributions were driven by the idea that the world of verification and the world of compilation do not sufficiently use their cross-fertilisation potential. This was declined in all topics, from my Phd [START_REF] Danthony-Gonnord | Accélération abstraite pour l'amélioration de la précision en Analyse des Relations Linéaires[END_REF] where verification of embedded systems was the only application domain to the synthesis of numerical invariants, to my current activities where compute-intensive code (High Performance Computing kernels) as well as general purpose programs are under concern.

Static analysis for verification

Program analysis for verification aims at automatically checking that programs fit their specifications, these specification being explicit ("this program sorts an array") or implicit ("this program does not make any array out-of-bounds access"). In the general case, a perfect (sound and complete) program analysis is impossible (due to the undecidability of the halting problem). In order to render it possible, at least one of the following must hold: unsoundness (some violations of the specification are not detected), incompleteness (some correct programs are rejected because spurious violations are detected), or the state space should be finite (and not too large, so as to be enumerated explicitly or implicitly).

Among various techniques for program analysis, Abstract interpretation [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF] is sound, but incomplete: it over-approximates the set of behaviours of the analysed program; if the over-approximated set contains incorrect behaviours that do not exist in the concrete program, then false alarms are produced. A central question in abstract interpretation for verification is to reduce the number of false alarms, while keeping memory and time costs reasonable [START_REF] Blanchet | A static analyzer for large safety-critical software[END_REF].

Static analysis for compilation of general purpose software

The rise of embedded systems and high performance computers in the last decade has revealed an increasing need for code optimisation. The applications are diverse, from compute-intensive embedded applications to massively parallel scientific code on large grids, as well as general purpose programs like web browsers or system schedulers.

Program analysis has two different usage in compilers:

• reject the program or print warnings if the program is not well-formed or has undefined behaviour.

• compute information and propagate to further code optimisation/transformation.

The central question in program analysis for optimising compilers is to design specialised analyses that scale well, while remaining expressive. In addition, these analyses must remain simple enough to be implemented in production compilers and usable for client analyses inside these compilers (like loop transformations to optimise locality, scheduling, automatic parallelization etc.).

Challenges for static analyses

The success of abstract interpretation for safety-critical programs demonstrates the robustness of the framework as well as its capability to provide precise analysers for complex properties (from array out-of-bounds to non interference of variables in parallel programs). However, if we want to cope with more generalist programs, or use abstract-interpretation invariant generation inside production compilers, there still remains numerous challenges that are partially addressed in this manuscript.

• Analyses must apply to more generalist programming languages (as opposed to a very specific subset of C or Java) ([SMO+14, GMR15], . . . ), or, at the opposite, be specially designed for domain-specific languages ( [GG11], [START_REF] Feautrier | Enhancing the Compilation of Synchronous Dataflow Programs with a Combined Numerical-Boolean Abstraction[END_REF]).

• Analyses must be scalable, in order to deal with the increasing size of programs, and to be used as pre-analyses for code optimisation [SMO+14, PMB+16, MPR+17], . . . ).

• Nevertheless, analyses must remain expressive enough to be capable of deriving precise information when necessary ([MG11, MG16], . . . )

Related publications

For the sake of brevity and uniformity, this manuscript does not cover the publications related to my Phd ( [START_REF] Danthony-Gonnord | Accélération abstraite pour l'amélioration de la précision en Analyse des Relations Linéaires[END_REF], [START_REF] Gonnord | Combining widening and acceleration in linear relation analysis[END_REF], [START_REF] Halbwachs | Some ways to reduce the space dimension in polyhedra computations[END_REF], [START_REF] Gonnord | Abstract Acceleration in Linear Relation Analysis[END_REF]), or made during my master studies [START_REF] Gonnord | From discrete duration calculus to symbolic automata[END_REF] and my postdoctoral studies ([GB09], [GB09], [START_REF] Gonnord | Runtime resource assurance and adaptation with Qinna framework: a case study[END_REF]). The work we made on theoretical aspects of Domain Specific Languages [START_REF] Rusu | A generic tool for formally tracing executions back to a dsml's operational semantics[END_REF] is also not exposed in this manuscript. This document is a synthesis of the research articles, journals, or research reports, listed below.

Numerical Domains [START_REF] Feautrier | Enhancing the Compilation of Synchronous Dataflow Programs with a Combined Numerical-Boolean Abstraction[END_REF]

Outline of the document

This manuscript develops the contributions made in the domain of static analysis. Each chapter exposes a different application domain and the techniques we developed for enhancing precision, scalability and applicability:

• Chapter 2 exposes our works around the correct design of static analyses for numerical programs (in our context, numerical programs are programs that manipulate integer variables), with a particular focus on scalability and applicability inside specialised or general purpose compilers.

• Chapter 3 summarises our contributions on proving termination of sequential numerical programs. This chapter illustrates how verification can take advantage of compilation techniques.

• Chapter 4 reports our works on the effective design of static analyses to deal with memory properties inside production compilers, and a more fundamental work on proving complex array properties.

• Chapter 5 gives the conclusion and draws future research directions.

Numerical domains

Since the seminal paper [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF], abstract interpretation has proved its success for the verification of safety properties. The success story of ASTRÉE [START_REF] Blanchet | A static analyzer for large safety-critical software[END_REF] shows the applicability of the method for safety critical systems (avionics). However, there still remain numerous motivations to continue working on the effective design of numerical domains:

• Classical abstract interpretation suffers from a lack of semantic-driven iteration heuristics (the algorithm usually scans the program under analysis in a deep-first search manner, regardless the meaning of the program itself). Some attempts have been made to design clever iteration strategies [START_REF] Costan | A Policy Iteration Algorithm for Computing Fixed Points in Static Analys is of Programs[END_REF]. However they often fail when the invariant to be proved is disjunctive. Like abstract acceleration [START_REF] Danthony-Gonnord | Accélération abstraite pour l'amélioration de la précision en Analyse des Relations Linéaires[END_REF], semantic driven strategies would enable to gain both in terms of precision and time.

• The expressivity potentiality of some numerical analyses are not exploited as they could be. Synchronous languages compilers are an example of such missed opportunity of code optimisation. From the beginning of Lustre [START_REF] Halbwachs | Programming and verifying critical systems by means of the synchronous data-flow programming language LUSTRE[END_REF] and Signal [START_REF] Le Guernic | Polychrony for System Design[END_REF], the choice has been make to design syntax directed simple code generation, and to avoid clever analyses as much as possible, in order to simplify the validation process of the compiler itself. However there is a need for more powerful analyses, especially to be able to compile for parallel platforms, while remaining simple enough to be embedded in synchronous compilers.

• Production compilers (GCC, LLVM, ICC) do not currently use the most advanced techniques/ abstract domains produced by the static analysis community in the last decades. Despite the original relationship between dataflow analyses inside compilers (liveness of variables, constant propagation), the actual number of abstract-interpretation based analyses actually implemented in production compilers are very few, mainly because of their algorithmic complexity 1 . Thus, designing numerical abstract domain that scale enough to be embedded in production compilers still remain a challenge.

Summary and Outline

This chapter summarises the contributions made to improve expressivity, scalability and applicability of numerical abstract domains. Section 2.1 describes the model of programs we use and the main context, which is abstract interpretation, and SMT-solving. Some of the tools we use are described in Section 2.2. Then, the chapter presents two contributions that follow the recent advances in SMT solving and combine abstractions and SMT-solving: • Section 2.3 explains how to use SMT-solvers to drive the fixpoint iterations in order to get more precise numerical invariants.

• Section 2.4 shows how a new Numerical Boolean abstraction can improve the capabilities of synchronous language compilers. The last contribution of the chapter, described in Section 2.5 is a new abstract domain based on intervals, whose design focuses on the effectivity as well as expressivity.

Model of programs, abstract interpretation, SMT-solving

We write matrices with capital letters (as A) and column vectors in boldface (as x). If x has dimension d , its components are denoted x[i ], with 0 ≤ i < d . Thus, its i -th component is x[i -1]. Sets are represented with calligraphic letters such as W , K , etc.

Integer Interpreted Automata

In the tradition of most previous work on program termination and static analysis, we first transform the program to be analysed into an abstraction: the associated integer interpreted automaton. This is similar to the flowcharts used a long time ago to express programs (see, e.g., Manna's book [START_REF] Manna | Mathematical Theory of Computing[END_REF]) until the advent of structured programming. In fact, when one looks at real-life programs, many deviations from the strict structured model can occur, including premature loop termination, exceptions, and even the occasional goto. Reasoning with flowcharts abstracts the details of the syntax and semantics of the source language, which can be dealt with by an appropriate pre-processor. In our work, a program is represented by an affine (integer) interpreted automaton.

Definition 1 (affine (integer) interpreted automaton). An affine (integer) interpreted automaton (AIA)

is a tuple A = (K , n, k i ni t , T ) defined by: • a finite set K of control points;

• n integer variables represented by a vector x of size n;

• an initial control point k i ni t ∈ K ;

• a finite set T of 4-tuples (k, g , a, k ), called transitions, , where k ∈ K (resp. k ∈ K ) is the source (resp. target) control point, g : Z n → B = {true, false}, the guard, is a logical formula expressed with affine inequalities G x + g ≥ 0, and a : Z n → Z n , the action, assigns, to each variable valuation x, a vector x of size n, expressed by an affine expression x = Ax + a. Here, G and A are matrices, g and a are vectors.

To represent non-determinism or to approximate non-affine or non-analysable assignments in the program, we may have to assign the value "?", representing an arbitrary integer, to a variable, but we will not elaborate on this point.

k 0 t2 x ≤ 10 ∧ 0 ≤ y x := x + 1 y := y -1 t1 0 ≤ x ∧ 0 ≤ y x := x -1 y := y -1
Semantics The set of states is Σ = K × Z n . A trace from (k 0 , x 0 ) to (k, x) is a sequence of states (k 0 , x 0 ), (k 1 , x 1 ), . . . , (k p , x p ) such that k p = k, x p = x and for each i , 0 ≤ i < p, there exists in T a transition (k i , g i , a i , k i +1 ) such that g i (x i ) = true and x i +1 = a i (x i ). Given an initial valuation v , a state (k, x) is reachable from v iff (if and only if) there is a trace from (k i ni t , v ) to (k, x). A state (k, x) is reachable if there exists v ∈ Z n such that (k, x) is reachable from v . The set of reachable states is denoted by R.

Invariants

The guard g in a transition t = (k, g , a, k ) gives a necessary condition on variables x to traverse the transition t and to apply its corresponding action a. To get the exact valuations x of variables for which the action a can be performed, one would need to take into account the initial valuations and the successive conditions that led to the control point k. We denote by R k set of possible valuations x of variables when the control is in k:

R k = {x ∈ Z n | (k, x) ∈ R}.
Then, there exists a trace containing the transition (k, g , a, k ) iff x ∈ R k and g (x) is true. Note that R k does not depend on any initial valuation. More precisely, it is the union, for all initial valuations v , of the set of vectors x such that (k, x) is reachable from v . In practice, it is difficult to determine the set R k exactly but it is possible to give over-approximations, thanks to the notion of invariants. An invariant on a control point k is a formula φ k (x) that is true for all reachable states (k, x). It is affine if it is the conjunction of a finite number of affine conditions on program variables. The set R k is then over-approximated by the integer points within a polyhedron P k . To compute invariants, we rely on standard abstract interpretation techniques, widely studied since the seminal paper of Cousot and Halbwachs [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF]. These sets P k represent all the information on the values of variables that can be deduced from the program by state-of-the-art analysis techniques.

Background and Notations in Abstract Interpretation

Let us denote by τ k,k the concrete set semantics of the edge (k, k ), ie a function that maps a set of states before the transition (k, k ) to the set of states after the transition. Thus given a control point k, the set R k of reachable values at this control point is the least solution of a system of semantic equations [START_REF] Cousot | Abstract interpretation frameworks[END_REF]:

R k = I k ∪ (k ,k)∈T τ (k ,k) (R k ),
where I k designs the possible initial values at control point k, i.e., in our case

I k = Z n if k = k i ni t else. .
Abstract interpretation replaces the concrete sets of states R k by elements of an abstract domain D. In lieu of applying exact operations τ to sets of concrete program states, we apply abstract counterparts τ . 2 An abstraction τ of a concrete operation τ is deemed to be correct if it never "forgets" states:

∀X ∈ D τ(X ) ⊆ τ (X ) (2.1)
We also assume an "abstract union" operation , such that X ∪Y ⊆ X Y . For instance, Σ can be Q n , D can be the set of convex polyhedra and the convex hull operation [START_REF] Bagnara | The Parma Polyhedra Library[END_REF][START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF][START_REF] Halbwachs | Détermination automatique de relations linéaires vérifiées par les variables d'un programme[END_REF].

Solving the abstract system

In order to find an inductive invariant 3 , one solves a system of abstract semantic inequalities (X k denotes possible valuations at control point k):

∀k I k ⊆ X k ∀(k , k ) ∈ T τ (k ,k) (X k ) ⊆ X k . (2.2)
Since the τ e are correct abstractions, it follows that any solution of such a system defines an inductive invariant; one wishes to obtain one that is as strong as possible ("strong" meaning "small with respect to ⊆"), or at least sufficiently strong as to imply the desired properties.

Assuming that all functions τ e are monotonic with respect to ⊆, and that is the least upper bound operation in D with respect to ⊆, one obtains a system of monotonic abstract equations:

X k = I k (k ,k)∈T τ (k ,k) (X k ).
If (D, ⊆) has no infinite ascending sequences (d 1 d 2 . . . with d 1 , d 2 , • • • ∈ D), then one can solve such a system by iteratively replacing the contents of the variable on the left hand side by the value of the right hand side, until a fixed point is reached. The order in which equations are iterated does not change the final result ( [START_REF] Cousot | Méthodes itératives de construction et d'approximation de points fixes d'opérateurs monotones sur un treillis, analyse sémantique des programmes[END_REF], "cahotic iterations" chapter).

Solving with extrapolation Many interesting abstract domains, including that of convex polyhedra, have infinite ascending sequences. One then classically uses an extrapolation operator known as and denoted by in order to enforce convergence within finite time. The iterations then follow the "upward iteration scheme":

X k := X k X k (k ,k)∈T τ (k ,k) (X k ) (2.3)
where the contents of the left hand side gets replaced by the value of the right hand side. The convergence property is that any sequence u n of elements of D of the form u n+1 = u n v n , where v n is another sequence, is stationary [START_REF] Cousot | Abstract interpretation frameworks[END_REF]. It is sufficient to apply widening only at a set of program control nodes P W such that all cycles in the control flow graph are cut. Then, through a process of chaotic iterations [39, Def. 4.1.2.0.5, p. 127], one converges within finite time to an inductive invariant satisfying Rel. 2.2.

Definition 2 (Widening for intervals). The widening operator on intervals is defined as

[x l , x r ] [x l , x r ] = [x" l , x" r ] where x" l = x l if x l = x l -∞ else.
, and x" r = x r if x r = x r +∞ else. . Choose

Algorithm 1 Abstract Interpretation: classic Algorithm

k 1 ∈ A 4: A ← A \ {k 1 } 5:
for all outgoing edge (e) from k 1 do

6:

Let k 2 be the destination of e : 7:

if k 2 ∈ P W then 8: X t emp ← X k 2 X k 2 τ e (X k 1 )
Widening node; 9: else 10:

X t emp ← X k 2 τ e (X k 1 ) ; 11: end if 12: if X t emp ⊆ X k 2 then
The value must be updated Algorithm, implementation A naive implementation of the upward iteration scheme described above is to maintain a work-list of program points k such that X k has recently been updated and replaced by a strictly larger value (with respect to ⊆), pick and remove the foremost member k, apply the corresponding rule X k := . . . , and insert into the work-list all k such that (k, k ) ∈ T (This algorithm is formally described in Algorithm 1). This algorithm also performs an improvement of the obtained invariant; once an inductive invariant is found, it is possible to improve it by iterating the ψ function defined as

Y = ψ (X ), noting X = (X k ) k∈K and Y = (Y k ) k∈K , with Y k = I k (k ,k)∈T τ (k ,k) (X k ).
If X is an inductive invariant, then for any n, ψ n (X ) is also an invariant. This technique is an instance of narrowing iterations, which may help recover some of the imprecision induced by widening [41, §4]. x := 0

x := x + 1 x ≥ 100 x := 0 x < 100 (b) Its CFG Figure 2.1 -A simple example
The classic algorithm (with the interval abstract domain) performs on this control flow graph (Control Flow Graph (CFG)) the following iterations :

• Initialisation : X k 1 ← (-∞, +∞), X k 2 ← X k 3 ← X k 4 ← . • Step 1: X k 2 ← [0, 0], then the transition to k 3 is enabled, X k 3 ← [1, 1]
, then the return edge to k 2 gives the new point x = 1 to X k 2 , the new interval is then X k 2 = [0, 1] after performing the convex hull. Widening according to Definition 2 gives the interval

X k 2 = [0, ∞). • Step 2: X k 3 becomes [1, +∞).
The second transition from k 3 to k 2 is thus enabled, and the back edge to k 2 gives the point x = 0 to X k 2 . At the end of step 2 the convergence is reached. • The narrowing sequence on the interval X k 2 = [0, ∞) performs an intersection with the constraint x < 100. After propagation, we end up with the stable invariant X k 2 = [0, 100].

In the rest of the manuscript, we will denote by I k any inductive invariant at control k.

SMT-solving

Satisfiability modulo theory (SMT) solving consists in deciding the satisfiability of a first-order formula with unknowns and relations lying in certain theories. For instance, the following formula taken from [START_REF] Monniaux | A survey of satisfiability modulo theory[END_REF]:

(x ≤ 0 ∨ x + y ≤ 0) ∧ y ≥ 1 ∧ x ≥ 1 has no solution in R 2 .
A SMT-solver reports whether a formula is satisfiable, and if so, may provide a model of this satisfaction, for instance (x = 0, y = 1) is such a model for (x

≤ 0 ∨ x + y ≤ 0) ∧ y ≥ 1.
SMT encompasses various theories as diverse as character strings, inductive data structures, bitvector arithmetic, and ordinary differential equations. In all the following work however, we focus on the numerical fragments such as quantifier-free linear integer arithmetic (QF_LIA) or quantifierfree linear real arithmetic (QF_LRA) like in the previous example. These theories subsume Boolean satisfiability (SAT), the canonical NP-complete problem. However they remain decidable.

The reader might refer to [START_REF] Monniaux | A survey of satisfiability modulo theory[END_REF], [17] and [START_REF] Kroening | Decision procedures[END_REF] for a more complete introduction on SMT and the different state-of-the-art solvers/techniques, as well as its applications to program analysis.

Tools for Abstract Interpretation and SMT-solving

Computing numerical invariants from C-programs

There are many tools for the computations of numerical invariants. Here is a non exhaustive list of some recent ones:

• NBAC 4 implements the classic LRA in combination to dynamic partitioning ( [START_REF] Jeannet | Dynamic partitioning in analyses of numerical properties[END_REF]). Contrary to ASPIC, the tool is dedicated to the verification of properties of LUSTRE programs. The method performs forward and backward analysis from a minimal control structure, and the CFG is partitioned w.r.t. the analysis results (and the proof goal). Our technique can be used to improve the precision of invariants during each forward/backward analysis.

• LASH 5 and FASTER 6 use acceleration techniques to compute, when possible, the exact reachability sets of counter automata. Theoretical results concerning the acceleration of some subclasses of loop have been obtained this last ten years (for difference bound constraints [START_REF] Comon | Multiple counters automata, safety analysis and Presburger arithmetic[END_REF], a subclass of affine guarded functions [START_REF] Boigelot | Symbolic methods for exploring infinite state spaces[END_REF][START_REF] Finkel | How to compose Presburger-accelerations: Applications to broadcast protocols[END_REF] and more recently for octagonal relations [START_REF] Bozga | Iterating Octagons[END_REF]). However, the tools based on these algorithms are not fully automatic (LASH), or are not guaranteed to terminate (FASTER), in particular for nested loops.

• STING 7 , and INVGEN 8 use a combination of LRA and Farkas' lemma to discover numerical invariants. The main drawback of the method is the use of template invariants, which prevents the analysis to discover any invariant which is not of the right form. To improve the precision, INVGEN performs an execution of the program to add some additional constraints, which increase the global analysis time.

• There are many C parsers and experimental compilers, including CIL [START_REF] Necula | CIL: Intermediate language and tools for analysis and transformation of C programs[END_REF], LLVM [START_REF] Lattner | LLVM: A compilation framework for lifelong program analysis & transformation[END_REF] and Suif [START_REF] Wilson | The SUIF compiler system: a parallelizing and optimizing research compiler[END_REF]. Extracting an automaton from their intermediate representation, let alone do the complex approximations and transformations that are necessary prior to precise numerical invariant generation is not a straightforward activity. Moreover, at the time of the RANK toolchain design (see Chapter 3), LLVM was not mature enough to make the bet of designing a preprocessing based on it.

• Pagai [START_REF] Henry | The Pagai static analyser[END_REF] is a numerical invariant generation designed at Verimag (Grenoble) since 2012. It implements the more recent developments in abstract interpretation with numerical abstract domains, such as [START_REF] Henry | PAGAI: a path sensitive static analyzer[END_REF]. Pagai performs classic abstract interpretation on the LLVM intermediate representation.

During my PhD and since then, I maintain ASPIC, a numerical polyhedral invariant generator for interpreted automata (based on a variation on abstract interpretation called abstract acceleration, that was the main contribution of my Phd thesis). In 2009/2010, Paul Feautrier made a C parser that is able to generate automata in the ASPIC input format. We used this tool chain for some of the works detailed in the manuscript. Some implementation details are described in [START_REF] Feautrier | Accelerated Invariant Generation for C Programs with Aspic and C2fsm[END_REF].

SMT-solvers

SMT solvers can be used as a library, from an application programming interface, typically from C/C++ or Python, or as an independent process, that reads and writes outputs from a common format called SMT-lib [START_REF] Barrett | The Satisfiability Modulo Theories Library (SMT-LIB)[END_REF]. In the prototypes we developed we often used the SMT-lib format to first prototype examples, then either we chose to use their API (TERMITE-see section 3.2.3 -uses Z3's API) or a pipe to the SMT-lib format (this is the case for SYNC2SMT in Section 2.4 ) which uses a Yices version of the format).

Enhancing fixpoint iterations with SMT-solvers

In this section, I detail the contribution of the SAS' However, if we focus on the loop: assume(nondet()); x = x+1; assume(x < 100);, we could iterate on this loop first, compute the result [0, 99] and continue to perform the classic analysis, this invariant is inductive for the original loop, thus the analysis stops with this invariant. Our method will formalise this idea. In order to prove that there cannot be a division by zero in the first branch of the second if-then-else, one would need the non-convex property that x ≥ 0.01 ∨ x ≤ -0.01. An analysis representing the invariant at that point in a domain of convex properties (intervals, polyhedra, etc.) will fail to prove the absence of division by zero (incompleteness). Obviously, we could represent such properties using disjunctions of convex polyhedra [START_REF] Bagnara | Precise widening operators for convex polyhedra[END_REF], but this leads to combinatorial explosion as the number of polyhedra grows: at some point heuristics are needed for merging polyhedra in order to limit their number; it is also unclear how to obtain good widening operators on such domains. The same expressive power can alternatively be obtained by considering all program paths separately ("merge over all paths") and analysing them independently of each other. In order to avoid combinatorial explosion, the trace partitioning approach [START_REF] Rival | The trace partitioning abstract domain[END_REF] applies merging heuristics. In contrast, our method will rely on the power of modern SMT-solving techniques.

We have seen two examples of programs where classic polyhedral analysis fails to compute good invariants. How could we improve on these results?

• In order to get rid of the imprecision in Example 3, one could "explode" the control-flow graph: in lieu of a sequence of n if-then-else, with n merge nodes with 2 input edges, one could distinguish the 2 n program paths, and having a single merge node with 2 n input edges. As already pointed out, this would lead to exponential blowup in both time and space.

• One way to get rid of imprecision of classic analysis on the program from Fig. 2.2 would be to consider each path through the loop at a time and compute a local invariant for this path.

Again, the number of such paths could be exponential in the number of tests inside the loop.

The contribution of our article [MG11] is a generic method that addresses both of these difficulties. First, we encode the program in a way that enables the search for "interesting paths" for which we will compute a precise invariant. Then, we transform Algorithm 1 in order to integrate this "path focusing." In the rest of the section, I describe an instantiation of the algorithm on affine automata, but the article deals with arbitrary transitions systems.

Finding interesting paths in a program

We first give a way to express the concrete semantics of the program in term of an SMT formula called ρ. The Control Flow Graph of the program is first transformed into the Single Static Assignment (SSA) form, where all variables are statically assigned once [START_REF] Cytron | Efficiently computing static single assignment form and the control dependence graph[END_REF]; standard techniques exist for converting to SSA.

As usual in abstract interpretation, we consider a set K W ⊆ K of widening nodes. Let us take a superset K R of K W "abstraction points". K R can be taken equal to K W , or may include other nodes.

In the sequel, the nodes in K R are in bold.

Example 2 (continuing from p. 12). In Figure 2.3 we depict the transformations we do on the SSA CFG of the program of Figure 2.2 in order to encode its semantics inside a first-order affine formula. Figure 2.3(a) gives the SSA version of the CFG:

x 2 = φ(x 1 , x 4 , x 3 , x 2
) is a merge SSA statement that encodes the fact that the x 2 variable is updated with one of the four values x 1 , x 2 , x 3 , x 4 depending on the preceding node/transition: for instance, if the previous node was k 1 , now x 2 has the value x 1 . We apply SMT-solving over that formula. The result is either "unsatisfiable", in which case there is no path from k 1 , with variable values x 1 , to k 2 , with variable values x 2 , such that x 1 ∈ X k 1 and x 2 ∉ X k 2 , or "satisfiable", in which case SMT-solving also provides a model of the formula (a satisfying assignment of its free variables); from this model we easily obtain such a path, unique by construction of ρ. Indeed, a model of this formula yields a trace of execution: those b k predicates that are true designate the program points through which the trace goes, and the other variables give the values of the program variables.

1 k 2 : x 2 = φ(x 1 , x 4 , x 3 , x 2 ) k 3 x 1 = 0 x 3 := x 2 + 1 x 3 ≥ 100 x 4 = 0 x 3 < 100 (a) SSA CFG k s 1 k s 2 k 3 k d 2 : x 2 = φ(x 1 , x 4 , x 3 , x 2 ) e 3 x 3 = x 2 + 1 e 5 x 3 ≥ 100 x 4 = 0 e 4 x 3 < 100 e 2 e 1 x 1 = 0 (b) Disconnected (SSA) CFG e 1 = (x 1 = 0) ∧ b s 1 ) ∧ (e 2 = b s 2 ∧ ¬c s 2 ) ∧ (e 3 = (x 3 = x 2 + 1) ∧ b s 2 ∧ c s 2 ) ∧ (e 4 = b 3 ∧ x 3 < 100) ∧ (e 5 = b 3 ∧ x 3 ≥ 100 ∧ x 4 = 0) ∧ (b d 2 = e 1 ∨ e 4 ∨ e 5 ∨ e 2 ) ∧ (b 3 = e 3 ) ∧ (x 2 = ite(e 1 ,

Final algorithm: path focusing for abstract interpretation

Algorithm 2 consists in the iteration of the path finding method of Sec. 2.3.1, coupled with forward abstract interpretation along the paths found and, optionally, path acceleration. The proof of correctness and termination is done in the paper. We also extend the algorithm, in the spirit of [START_REF] Gonnord | Combining widening and acceleration in linear relation analysis[END_REF] on the special case of self loops, in order to perform more precise iterations. Let us illustrate this algorithm on the motivating example.

Example 2 (continuing from p. 12). Let us perform Algorithm 2 on the modified CFG of the running example, that we recall in Figure 2.4:

• Initialisation: K R = {k 1 , k 2 }, A ← {k 1 }.
•

r es ← SmtSolve ρ ∧ b k 1 ∧ x 1 ∈ X k 1 ∧ k 2 |(k 1 ,k 2 )∈E b k 2 ∧ x 2 ∈ X k 2 13:
if r es is not "unsat" then The iteration thus ends with the desired invariant.

Validation

We validated this technique manually, the implementation inside ASPIC was unfortunately not mature enough to perform more experiments. However the method was implemented in the PAGAI tool [START_REF] Henry | The Pagai static analyser[END_REF] by Julien Henry, combined with other methods [START_REF] Gopan | Lookahead widening[END_REF] and the impact of path focusing has been evaluated in the paper [START_REF] Henry | PAGAI: a path sensitive static analyzer[END_REF].

A combined numerical-Boolean abstraction for synchronous programs

This contribution has been published in the conference paper [GG11] and an extended version in the journal [START_REF] Feautrier | Enhancing the Compilation of Synchronous Dataflow Programs with a Combined Numerical-Boolean Abstraction[END_REF].

In this work, we propose an enhancement of the compilation of synchronous programs with a combined numerical-Boolean abstraction. While our approach applies to synchronous dataflow languages in general, here, we consider the SIGNAL language for illustration. With this new abstraction, we determine the absence of reaction captured by empty clocks; mutual exclusion captured by two or more clocks whose associated signals never occur at the same time; or hierarchical control of component activations via clock inclusion. The abstraction we propose can be used early in the development process (validate simple properties while writing code), or be used to provide information to optimise or improve the quality of the generated code.

Overview of the approach Given the performance level reached by recent progress in Satisfiability Modulo Theory (SMT) (see Section 2.1.3) we use an SMT solver to reason on the new abstraction. The advocated approach is depicted by Fig. 2.5. Given a synchronous dataflow program P , we define a corresponding abstraction, used to check the satisfiability of properties of interest, i.e., those involving numerical expressions. Once identified, all properties of interest are concretized into synchronous dataflow programs, which are later composed with the initial program P . The resulting composed program is equivalent to P in which properties involving numerical expressions have been made explicit in a form that is suitably addressable by a synchronous language compiler. Then, it becomes easier for the compiler to do an efficient analysis and code generation. Notice that an important advantage of this contribution is its modular, i.e., non-intrusive, implementation regarding compilers. This clearly facilitates its integration to a given compiler and makes it easy to isolate a bug in the global framework (in comparison to a compiler-intrusive solution).

= ^x ∩ [b] (where [b] ∪ [¬b] = ^b and [b] ∩ [¬b] = ),
• Deterministic merging: z:= x default y where x, y and z are signals. This construct imposes i) z to be present when either x or y are present, i.e. ^z = ^x ∪ ^y, while ii) z holds the value of x if present, otherwise that of y.

• Composition: P ≡ P 1 |P 2 where P 1 and P 2 are processes. It denotes the union of equations defined in processes, leading to the conjunction of the constraints associated with these processes. A signal variable cannot be assigned a value in both processes P 1 and P 2 . SIGNAL adopts single assignment. A variable defined in P 1 can be an input of P 2 , and vice versa. The composition operator is commutative and associative.

• Restriction (or Hiding): P ≡ P 1 where x, where P 1 and x are respectively a process and a signal. It states that x is a local signal of process P 1 . Process P holds the same constraints as P 1 .

Syntactic sugar: clock operators, sub-processes. The core language of SIGNAL is expressive enough to derive new constructs of the language for programming comfort and structuring. In particular, SIGNAL allows one to explicitly manipulate clocks through some derived constructs that can be rewritten in terms of primitive ones. For instance, the clock extraction statement y:= ^x, meaning y is defined as the clock of x, is equivalent to y:= (x = x) in the core language.

For syntactical convenience, SIGNAL enables a modular definition of processes by providing a notion of sub-process (or local process). The statement P 1 where P 2 , where P 1 and P 2 are processes, denotes the fact that the latter process is a sub-process of the former process. The signal level, defined at line 04, reflects the water level in the bathtub at any instant. It is determined by considering two signals, faucet and pump, which are respectively used to increase and decrease the water level. These signals are increased by one under some specific conditions (lines 06 and 08), in order to maintain the water level in a suitable range of values. An alarm signal is defined at line 12 whenever the water overflows (line 10) or becomes scarce (line 11) in the bathtub. An additional "ghost" alarm is defined at line 13/14, which is not expected to occur. Here, it is just introduced to illustrate one limitation of the static analysis of SIGNAL. The clock of this signal is not completely specified in Bathtub. As stated before, this clock is the union of those associated with the two arguments of the default operator. The clock of the left argument is exactly known. The clock of the right-hand one is contextual because the argument is a constant (that is, a constant signal is always available whenever required by its context of usage): it is equal to the difference of ghost_alarm's clock and first argument's clock. Since, this difference cannot be defined exactly from the program, further clock constraints on ghost_alarm will be required from the environment of Bathtub for an execution. Our abstraction will demonstrate that the ghost_alarm signal will never occur as well as both signals pump and faucet.

A new numerical-boolean abstraction for SIGNAL traces

We define an abstraction for SIGNAL program analysis. All considered programs are supposed to be in the syntax of the core language. Our abstraction for program P is a logical formula Φ on the variables and clocks of P in a decidable theory (here, linear arithmetic of integers or reals) such that at any logical instant in an execution of P , the current values of signals and clocks satisfy Φ. In other words, at any instant in an execution of P , its variables and clocks are a model of Φ.

Let P be a SIGNAL program. We denote by X P = {x 1 , x 2 . . . x n } the set of all variables of P. Here, we consider scalar variables only. With each variable x i (numerical, Boolean or event), we associate two abstract values: x i and x i encoding respectively its clock and values. Intuitively, in such a couple, the first component encodes the clock of a signal, where true and false respectively mean presence and absence of instant in the clock. The second component encodes the value taken by a signal according to its presence.

The abstract semantics of the program, is a set of couples of the form ( , ) where:

• function : X P → B = {true, false} assigns to a variable a Boolean value;

• function : X P → R ∪ B assigns to a variable a numerical or Boolean value.

The abstract semantics (a set of couples ( , )) will be represented as a first order logic formula Φ P in which atoms are x i and x i , and the operators are usual logic operators and integer comparison functions. This abstraction into a first order logic formula naturally induces a loss of precision, as we will see later. Intuitively, the abstract semantics encodes in the Φ formula all Boolean and numeric relations between variables and clocks that are valid "for all instants." This semantics will not be sufficient to prove any relation between variables at a given instant and their value an instant before, for instance.

Abstraction for expressions

The abstraction of a given numerical SIGNAL expression nexp (resp. a Boolean expression bexp) is a numerical expression (resp. a Boolean expression) that expresses its behaviour in terms of a SMT formula φ. The abstraction is straightforward (expressions are the same at every instant), more details can be found in [GG11].

Abstraction of signal primitives

The abstraction Φ P of a given process P is the intersection of the abstractions of all its statements st m i :

Φ P = n i Φ(st m i )
where each Φ(st mt ) is a formula in quantifier-free linear integer arithmetic (QF_LIA) or quantifierfree linear real arithmetic (QF_LRA), defined according to the syntax of process definition.

• Instantaneous relations: y:= R(x1,...,xn). The abstraction Φ of instantaneous relations is defined as follows:

n i =1 ( y ⇔ x i ) ∧ y ⇒ y = φ(exp)
where R(x1,...xn) is denoted by exp (for boolean expressions, = means ⇔ ).

These expressions express the equalities between clocks and values that are induced by SIGNAL semantics.

• Delay: y:= x $ 1 init c. The abstraction Φ of the delay construct is defined as follows:

y ⇔ x HDR Laure Gonnord 19/92
The abstraction here only expresses the equalities between clocks. A better abstraction could be performed if the user (or a pre-analysis) provides invariants for numerical variables. In that case, the global abstraction would be :

y ⇔ x y ⇒ i nv ar ( x)[ x/ y] ∨ ( y = c)
where i nv ar ( x)[ x/ y] denotes the substitution of y in a formula that expresses a constraint on x's values. Such an invariant can be a result of abstract interpretation techniques.

• Under-sampling: y:= x when b. The abstraction Φ of the under-sampling construct is defined as follows:

y ⇔ ( x ∧ b ∧ b) y ⇒ y = x
which expresses the fact that the signal y is present if and only if both signals b and x are present and b is true. The constraints on values are straightforward.

• Deterministic merging: z:= x default y. The abstraction Φ of the deterministic merging construct is defined as follows:

y ⇔ ( x ∨ z) y ⇒ ( x ∧ ( y = x)) ∨ (¬ x ∧ ( y = z))
The clock of variable y is the union of the clocks of x and z, and values are determined according to the presence of x.

• Composition: P ≡ P 1 |P 2 . The abstraction Φ of the composition operator is defined as follows:

Φ ≡ Φ P 1 ∧ Φ P 2
Example 4 (continuing from p. 18). By applying our abstraction to the Bathtub code, which is divided into P 1 (lines 04 to 09) and P 2 (lines 10 to 14) according to the process hierarchy, we obtain Φ Bathtub = Φ P 1 ∧ Φ P 2 , where Φ P 1 equals to:

Φ P 1 = ( l evel ⇔ zl evel ⇔ f aucet ⇔ pump ⇔ bz f aucet ) ∧ ( l evel = zl evel + f aucet -pump) ∧ z f aucet ⇔ ( zl evel ∧ zl evel ≤ 4) ∧ z f aucet ⇒ f aucet = ( z f aucet + 1) ∧ ( pump ⇔ zpump) ∧ zpump ⇔ ( zl evel ∧ zl evel ≥ 7) ∧ zpump ⇒ pump = ( zpump + 1)
For Φ P 2 , we first rewrite equation at line 13/14 as follows:

(| y1 := true when scarce | y2 := y1 when overflow | ghost_alarm := y2 default false |)
Then, we obtain:

Φ P 2 = ( over f l ow ⇔ l evel ⇔ sc ar ce) ∧ over f l ow ⇔ ( l evel ≥ 9) ∧ ( sc ar ce ⇔ ( l evel ≤ 0) ∧ ( al ar m ⇔ sc ar ce ⇔ over f l ow) ∧ al ar m ⇒ al ar m ⇔ ( sc ar ce ∨ over f l ow) ∧ y 2 ⇔ ( sc ar ce ∧ over f l ow ∧ sc ar ce ∧ over f l ow) ∧ ( y 2 ⇒ y 2 ) ∧ ( g host ⇔ ( y 2 ∨ f al se)) ∧ g host ⇒ y 2 ∧ ( g host ⇔ y 2 ) ∨ ¬ y 2 ∧ ¬ g host
Our abstraction is sound, in the sense that it preserves the behaviours of the abstracted programs: if a (safety) property is true on the abstraction, then it is also the case on the program. A proof of its soundness is given in [GG11].

HDR Laure Gonnord 20/92

Application to the analysis and compilation of SIGNAL programs

We have implemented the previous abstraction as a standalone tool called Sync2Smt (5k Ocaml LOC). Our toolchain is depicted in Figure 2.5.

Validation on common patterns

We first validate our method on a few SIGNAL program patterns for which our abstraction helps in detecting some "clocks bugs" ("timing anomalies", in the literature). Such properties cannot be detected currently by the SIGNAL compiler because they involve numerical expressions, which are not addressed by a Boolean abstraction. Our abstraction allows their easy detection. These examples can be found in [START_REF] Feautrier | Enhancing the Compilation of Synchronous Dataflow Programs with a Combined Numerical-Boolean Abstraction[END_REF].

Using the abstraction for clock analysis

In [START_REF] Feautrier | Enhancing the Compilation of Synchronous Dataflow Programs with a Combined Numerical-Boolean Abstraction[END_REF], we also demonstrate the relevance of our abstraction for analysing clock properties that combine both logical and numerical expressions. For instance, checking the mutual exclusion between multiple computation nodes whose activation conditions consist of such clocks, is useful to address sharing problems in a GALS system 10 . The GALS model is used to design multi-clock distributed system where each computation node holds its own clock providing a local (synchronous) vision of time. In addition, establishing that some nodes or events in a system never occur, via empty clocks, can serve to guarantee that undesired behaviours never happen, or conversely to detect that some expected behaviours are never observed. This kind of observation can sightly improve the quality of the C code generated by the SIGNAL compiler, compared to the quite simplistic actual compilation scheme. On the one hand, dead code elimination is made possible thanks to information resulting from the analysis of our abstraction. As an example, we explain the impact of our analysis on the compilation of the Bathtub example. The conjunction of these three properties will be sufficient to prove that the ghost_alarm signal never occurs (equivalently, has an empty clock), and also that all other signals have empty clocks.

These properties are easily verified on the abstraction of Bathtub process. As a result, their corresponding concretisations can be safely composed with Bathtub without changing its semantics. Possible concretisations of the above properties in SIGNAL are as follows:

1. faucet ^* pump ^= ^0 (^= denotes the equality on clocks, ^* the intersection) 2. true when scarce when overflow ^= ^0 3. alarm ^= level By composing these statements with Bathtub, one obtains the semantically equivalent process, named Bathtub_Bis, shown in the following: The result of its analysis performed by the compiler is now as follows: The whole set of constraints inferred by the compiler is now restricted to the fact that the ghost_alarm signal is always equal to false. The compiler has also detected that the clocks of the other signals are all empty (lines 04/04b). Finally, the corresponding generated code is provided below, where the dead code is avoided.

01:

{ ghost_alarm = FALSE ; 02:

/* produce output value 03:

for the signal ghost_alarm */ } ...

Revisiting interval analysis for scalability

In this section we present our contribution on improving both precision and scalability of range analyses. This work is the first analysis of the paper [SMO+14], whose goal was to design a complete toolchain for securing memory accesses in the C programming language, and will be explained in detail in Chapter 4.

Range analysis, as originally defined by Cousot and Cousot [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF], associates variables with integer intervals. This approach enables several compiler optimisations, but it is not effective to validate memory accesses, as demonstrated by Logozzo and Fähndrich [START_REF] Logozzo | Pentagons: A weakly relational abstract domain for the efficient validation of array accesses[END_REF]. The program in Figure 2.6 illustrates this deficiency: a traditional range analysis will not find, in this program, constants onto which to rely upon, to prove that variables i and j only access valid positions of array p.

Example 6 (Motivating example). Figure 2.6 shows examples of three types of analyses, including the

Symbolic Range Analysis that we describe in Section 2.5.1. The information associated with a variable depends on which part of the program we are; hence, the figure shows the results of each analysis at three different regions of the code. In this example, classic range analysis can only infer positiveness of variables. Pentagons can infer also that j is always strictly less than N inside the loop. Octagons are more precise since they are able to find that m = i at control points b and c, for instance.

We could also use state-of-the-art relational analyses from the abstract interpretation community like octagons, but they do not scale enough for our target which is compilation. The objective of this work is thus:

• to improve the precision of range analysis by considering symbolic ranges, originally defined by Blume and Eigenmann [START_REF] Blume | Symbolic range propagation[END_REF];

• while still remaining scalable, that's why we design a sparse analysis.

Sparse Symbolic Range Analysis

To scale an analysis, the Static Single Information (Static Single Information (SSI)) framework [START_REF] Ananian | The static single information form[END_REF] propose to focus on the preservation of the following invariants:

unsigned N = read(); int* p = alloc(N); int i = 0; int m = 0; int j = N -1; while (i < j) { p[i] = -1; p[j] = 1; i++; j--; m++; } p[m] = 0;
Range analysis Symbolic range analysis Pentagons • The abstract state of any variable must be invariant in every program point where this variable is alive. A variable v is alive at a label if there is a path in the program's control flow graph from to another label where (i) v is used and (ii) v is not redefined along this path.

F(N) = [0, +∞] F(i) = [0, 0] F(j) = [-1, +∞] F(m) = [0, 0] F(i) = [0, +∞] F(j) = [1, +∞] F(m) = [0, +∞] F(i) = [0, +∞] F(j) = [-1, +∞] F(m) = [0, +∞] F(N) = {}, [0, +∞] F(i) = {}, [0, 0] F(j) = {N}, [-1, +∞] F(m) = {}, [0, 0] F(i) = {N}, [0, +∞] F(j) = {N}, [-1, +∞] F(m) = {}, [0, +∞] F(N) = [N, N] F(i) = [0, 0] F(j) = [N-1, N-1] F(m) = [0, 0] F(i) = {j, N}, [0, +∞] F(j) = {N}, [1, +∞] F(m) = {}, [0, +∞] (a) (b) (c) Octagons F(i, i, +) = i ≥ 0 F(i, i, -) = -i ≥ 0 F(N, j, +) = N -j ≥ 1 F(N, j, -) = j -N ≥ -1 F(m, i, +) = i -m ≥ 0 F(m, i, -) = m -i ≥ 0 F(i, i, +) = i ≥ 0 F(j, i, -) = j -i ≥ 0 F(j, i, +) = j + i ≥ 1 F(i, i, +) = i ≥ 0 F(m, i, -) = m -i ≥ 0 F(m, i, +) = m + i ≥ 0 F(i) = [0, N-2] F(j) = [1, N-1] F(m) = [0, +∞] F(i) = [0, max(0, N-1)] F(j) = [-1, max(0, N-2)] F(m) = [0, +∞] (a) (b) (c)
The strategy for the second point is to split the live ranges of variables: splitting a given variable v, at program label , by inserting a copy v = v at and renaming every use of v to v in points dominated 12 by . According to Tavares et al. [START_REF] Andre | Parameterized construction of program representations for sparse dataflow analyses[END_REF], it is enough to split live ranges at places (control points) where information originates: for instance, for a numeric range analysis, a new version of x should be "invented" each time a new value is assigned to x (which is what is done in the classical SSA form), but also after each test, which we will see in the sequel in the context of Symbolic Range Analysis.

Splitting Required by Symbolic Range Analysis. For the range analysis we want to perform, it is sufficient to propagate the information from the definition of variables and from conditional tests that use these variables. Thus, to make this analysis sparse, we must split live ranges at these places.

Splitting at definitions creates the Static Single Assignment representation. Splitting at conditionals creates the representation that Bodik et al. have called the Extended Static Single Assignment form (Extended Static Single Assignment Form (eSSA)) [START_REF] Bodik | ABCD: eliminating array bounds checks on demand[END_REF]. In the sequel, we consider programs into eSSA form 13 : for each conditional, we name the variables created at the "true" side of the branch a t and b t and the variables created at the "false" side of it a f and b f . As a convenience, we shall mark these copies with a σ, indicating that they have been introduced due to live range splitting at conditionals. We emphasise that these σ's are just a notation to help the reader to understand our way to split live ranges and have no semantics other than being ordinary copies 14 . We borrow this notation from Ananian's work [START_REF] Ananian | The static single information form[END_REF].

Example 6 (continuing from p. 22). Figure 2.7b shows the program in Figure 2.6 after live range splitting.

N = • p = alloc(N ) i 0 = 0 m 0 = 0 j 0 = N -1 i 1 = φ(i 0 , i 2 ) j 1 = φ(j 0 , i 2 ) m 1 = φ(m 0 , m 2 ) (i 1 < j 1 )? i f = σ(i 1 ) j f = σ(j 1 ) p m = p + m f * p m = 0 i t = σ(i 1 ) j t = σ(j 1 ) p i = p + i t * p i = -1 p j = p + j t * p j = 1 i 2 = i t + 1 j 2 = j t -1 m 2 = m t + 1 (a) The program in Figure 2.6 converted into extended static single assignment form 0 t h 1 t h 2 nd 3 r d (+∇) N [0, N ] [0, N ] [0, N ] i 0 [0, 0] [0, 0] [0, 0] m 0 [0, 0] [0, 0] [0, 0] j 0 [-1, N -1] [-1, N -1] [-1, N -1] i 1 [0, 0] [0, max] [0, max] j 1 [-1, N -1] [-1, N -1] [-1, N -1] m 1 [0, 0] [0, 1] [0, +∞] i t [0, N -2] [0, N -2] [0, N -2] j t [1, N -1] [1, N -1] [1, N -1] i 2 [1, N -1] [1, N -1] [1, N -1] j 2 [0, N -2] [0, N -2] [0, N -2] m 2 [1, 1] [1, 2] [1, +∞] i f - -[-1, max] j f - -[-1, max]

Symbolic Range Analysis on E-SSA control flow

From the tailored intermediate representation that is the E-SSA form, we now have to construct our symbolic abstract domain SymBoxes that will associate to each variable x of the program a symbolic range R(x).

A symbolic interval is a pair R = [l , u], where l and u are symbolic expressions (ie expressions on variables that are either constants known at compile time, or input values: random values, userprovided values, function arguments. . . ). We denote by (R ↓ , R ↑ ) the lower (l) and upper-bound (u) of the interval R.

We define the partially ordered set of (symbolic) intervals S 2 = (S ×S, ), where the ordering operator is defined as:

[l 0 , u 0 ] [l 1 , u 1 ], if l 1 ≤ l 0 ∧ u 1 ≥ u 0
We then define the semi-lattice SymBoxes of symbolic intervals as (S 2 , , , , [-∞, +∞]), where the join operator " " is defined as:

[a 1 , a 2 ] [b 1 , b 2 ] = [min(a 1 , b 1 ), max(a 2 , b 2 )].
Our lattice has a least element and a greatest element [-∞, +∞].

Clearly, this lattice is infinite; therefore, in order to end up the computation of the set of constraints we use a widening operator defined by (under the assumption R 1 R 2 ):

R 1 ∇R 2 = [l , u],
where

           l = R 1↓ if R 1↓ = R 2↓ l = -∞ otherwise u = R 1↑ if R 1↑ = R 2↑ u = +∞ otherwise
This is the extension of the classic widening on intervals to symbolic intervals: a lower (resp. upper) bound of a given symbolic interval can only be stable or diverge towards -∞ (resp. +∞), thus our widening operator will ensure the convergence of our analysis.

Abstract Interpretation with constraints

To apply the abstract interpretation framework, we also have to give an interpretation of the operations of the program. This is done in Figure 2.8.

• assignments after reads give only symbolic information.

• assignments to expressions makes use of "abstract transformers."

• φ functions are "join nodes", thus we perform a (symbolic) interval union.

• On intersection nodes (tests), we perform a (symbolic) interval intersection.

v = • ⇒ R(v) = [v, v] v = o ⇒ R(v) = R(o) v = v 1 ⊕ v 2 ⇒ R(v) = R(v 1 ) ⊕ I R(v 2 ) v = φ(v 1 , v 2 ) ⇒ R(v) = R(v 1 ) R(v 2 )
other instructions ⇒ The abstract transformers denoted by ⊕ I in Figure 2.8 are for instance:

-[l 0 , u 0 ] + I [l 1 , u 1 ] = [l 0 + l 1 , u 0 + u 1 ], [l , u] + I = [l , u]. -[l 0 , u 0 ]× I [l 1 , u 1 ] = [min(T ), max(T )],
where

T = {l 0 ×l 1 , l 0 ×u 1 , u 0 ×l 1 , u 0 ×u 1 }, [l , u]× I = [l , u].
Solving From a given program we thus generate a system of constraints that we solve using a Kleene iteration. The analysis is sparse since we do not need the control points any more. The information is only attached to variables. Widening is applied on a φ node only after 3 iterations of symbolic evaluation ("delayed widening"). This decision is arbitrary, and a larger number of iterations might increase the precision of our results. However, in our experiments we only observed very marginal gains when using more iterations.

Example 6 (continuing from p. 22). Figure 2.7b shows the steps that our analysis performs on the program of Figure 2.7a. The order in which we evaluate constraints is given by the reverse post-ordering of the program's control flow graph. This ordering tends to reduce the number of iterations of our fixpoint algorithm [86, p.421]. However, any order of evaluation would led to the same result. In this example, we let "max" be max(0, N -1).

On the evaluation of symbolic expressions. As shown in the preceding paragraphs, we have to evaluate symbolic expressions (simplification of expressions like max(e 1 , e 2 ), equality tests, . . . ). We rely on GiNaC [START_REF] Bauer | Introduction to the GiNaC framework for symbolic computation within the C++ programming language[END_REF], a library for symbolic manipulation, to perform these operations 15 . For the equality test, if GiNaC is not able to prove a given equality between symbolic expressions, we conservatively assume that the two expressions are not comparable. As a consequence, we may widen an expression to +∞ even if it was stable.

Proposition 1. The former analysis always returns an over-approximation of the actual ranges of the variables of the program (no matter the valuations of the symbols would be).

Validation

Runtime We run our experiments in a twelve-core Intel(R) Xeon(R) CPU E5-2620 at 2.00GHz, with 15,360KB of cache, and 16GB of RAM. Neither our compiler, nor our benchmarks, run in parallel.

The run time of our analysis compares favourably to the run time of equivalent algorithms, as Figure 2.9 shows.

The figure compares the runtime of our symbolic range analysis, Rodrigue et al.'s range analysis, and Pentagons, for the 60 largest benchmarks in the LLVM test suite and SPEC CPU 2006. These programs gave us over 5.18 million bytecodes to analyse. We tried to our best to be as faithful to the original description of Pentagons as possible. [START_REF] Rodrigues | A fast and low-overhead technique to secure programs again integer overflows[END_REF]. Pentagons [START_REF] Logozzo | Pentagons: A weakly relational abstract domain for the efficient validation of array accesses[END_REF]. Y axis is runtime, in seconds. Each X point is a benchmark, sorted by size (from 4k to 1M instructions).

Precision

The precision of our analysis is evaluated through its use in a bigger framework called GreenArrays, that we will study later (Section 4.2).

Conclusion

In this chapter I summarised the contributions made in the domain of numerical programs analysis. This chapter is an illustration of the impact of combining techniques from different communities, from SMT-solving to abstract interpretation or compilation, or from abstract interpretation to compilation. One lesson of this work is that the effort of bringing a technique to another community is non trivial, however, it deserves to be made. The last contribution advocates for the design of more scalable abstract domains. We strongly believe that such abstract domains must be thought in term of scalability and expressivity at the same time. The SSI-framework proposes guidelines to design such abstract domains, however, there is still an open research question for fully relational analyses: can they scale? are there ways to degrade their expressivity in a generic way so as to improve their precision?

Static Termination Analysis

Proving termination is one key application of invariant generation and static analyses techniques. This problem, which was studied since the early days of Computer Science, and its companion problem, which is the computation of the WCCC (worst-case computational complexity), has many applications:

• for proving full correctness: since the seminal paper of Floyd [START_REF] Floyd | Assigning meaning to programs[END_REF], termination and partial correctness are complementary. However, much more attention has been given to partial correctness: we affix assertions to each program point and prove that they are consequences of the assertions of its predecessors in the program control graph. The assertions at the entry point of the program are its preconditions, the assertions at loop entry points are invariants, while the assertions at its exit point must entail correctness, according to some set of requirements 1 ). However, this method proves only partial correctness, i.e., that the program gives the correct result if and when it terminates. Termination thus still has to be proved to fully prove the correctness of programs, and despite the early definition of the problem, has clearly received less attention from the program analysis community.

• for proving safety of reactive programs: in reactive programs, we have to prove functional correctness as well as reactivity, i.e. that the code inside the infinite reactive loop executes itself in finite bounded time. Moreover, in order to parametrise the sensors and actuators of a given platform, we have to compute a safe bound on the sampling rate. An accurate worst-case execution time can be derived from WCCC results, with the help of abstract static cache analyses such as [START_REF] Asavoae | Program semantics in model-based WCET analysis: A state of the art perspective[END_REF]. Static analyses can improve the precision of the global worst-case execution time computation, as shown for instance in [START_REF] Henry | How to compute worst-case execution time by optimization modulo theory and a clever encoding of program semantics[END_REF].

• for detecting hotspots in intensive computations and thus perform best-effort optimisation in these particular pieces of code. This is a particular case of prediction. In static compilers, loops with a high number of iterations may benefit from aggressive code motion strategies, or polyhedral-based optimisation [START_REF] Feautrier | The polyhedron model[END_REF] whose cost might be too high to be applied at any point of the program.

Summary of the chapter

The main idea of this work was initially to explore the link between scheduling and termination [START_REF] Darte | Understanding loops: The influence of the decomposition of Karp, Miller, and Winograd[END_REF][START_REF] Darte | Optimal parallelism detection in nested loops[END_REF], through making a parallel between schedules and ranking functions. Using a classical algorithm of the program scheduling literature, combined with numerical invariants computed by abstract interpretation, we first demonstrate the expressivity of the method in [ADFG10]. This work was further extended to deal with larger programs [AAG12] by classical static analyses techniques adapted to the particular case of termination.

More recently, in [GMR15] we showed how to drastically decrease the size of the constraint systems we solve while computing ranking functions using ideas from the static analysis community (namely, counter-example guided refinement). Another experience in termination was the study [START_REF] Raphael Ernani Rodrigues | Realworld loops are easy to predict : a case study[END_REF] of the Mozilla Firefox Just-In-Time compiler in which detecting "intensive" loops is crucial for performance. In all these works, from theory to practice, the results we obtain show the relationships and the cross fertilisation of compilation techniques and static analyses techniques.

Outline Section 3.1 defines the main theoretical tools used for proving termination of sequential programs. Section 3.2 exposes the two main algorithmic contributions published in [ADFG10] and [GMR15] as well as their experimental evaluation. Section 3.3 describes our techniques to improve the scalability of the tools. Finally Section 3.4 summarises our case study on the Mozilla JIT compiler.

Model of programs, termination, ranking functions

In this chapter, we also consider programs as Integer Interpreted automata, as described in Section 2.1.1. We also assume that they have been obtained through a safe abstraction procedure. The problem is now to prove termination of a given automaton, i.e. to prove that there is no infinite path from the initial states.

The standard technique for proving termination is to consider ranking functions to well-founded sets. A well-founded set W is a set with a (total or partial) order (we write a ≺ b if a b and a = b) such that there is no infinite descending chain, i.e., no infinite sequence (x i ) i ∈N with x i ∈ W and

x i +1 ≺ x i for all i ∈ N. Definition 3. A ranking function (ρ) is a function ρ : K × Z n → W
, from the automaton states to a well-founded set (W , ), whose values decrease at each transition t = (k, g , a, k ):

x ∈ R k ∧ g (x) = true ∧ x = a(x) ⇒ ρ(k , x ) ≺ ρ(k, x) (3.1)
where R k are the reachable valuations at control point k (any over-approximation I k can replace i).

It is said affine if it is affine in the second parameter (the variables). x := m; y := 0 0 x ∧ 0 y x < 0 ∨ y < 0 true true y m y := y + 1 by ASPIC (an abstract-interpretation based invariant generator, see Section 2.2.1), followed by the bidimensional rankings and the corresponding WCCC computed by RANK, our tool that implements the algorithms of [ADFG10]. These rankings expressions are positive and lexicographically decrease along each transition. For instance, the first component of the ranking function decreases from 2x +3 at l bl 5 to 2x + 2 at l bl 6 , then 2x + 3 at l bl 10 , but since x is changed to x -1 by the corresponding transition, the ranking has really decreased.

Definition 4. A ranking function is one-dimensional if its co-domain is (N, ≤). It is k-dimensional (or multi-dimensional of dimension k) if its co-domain is (N k , k ),
x := x -1 y := y -1 c. point Invariant l bl 4 m ≥ x > 0, m ≥ y > 0 l bl 5 m ≥ x ≥ 0, m ≥ y ≥ 0 l bl 6 m ≥ x ≥ 0, m + 1 ≥ y ≥ 0 l bl 10 m ≥ x ≥ -1, m + 1 ≥ y ≥ 0 2m ≥ x + y c.

Computing ranking functions of imperative programs

Unlike previous work [START_REF] Bradley | Linear ranking with reachability[END_REF][START_REF] Gulwani | SPEED: Precise and efficient static estimation of program computational complexity[END_REF] where the construction of invariants is coupled with the termination proof or evaluation of iteration bounds, the invariants I k on all control points of the programs are pre-computed (The non-precision of the invariant will be the unique source of loss of precision of our method, as we will see later). In both papers [ADFG10] and [GMR15], we use ASPIC 3 to compute these invariants.

Key observation: ranking functions are schedules

The polyhedral model is a collection of techniques developed around a common intermediate representation of programs: integer polyhedra. Such a mathematical representation of programs inherits nice properties from the underlying mathematical structure. For instance, when loop transformations are represented as affine functions, compositions of transformations are also affine functions due to closure. The polyhedral representation was linked to loop programs by an analysis proposed by Feautrier [START_REF] Feautrier | Dataflow analysis of array and scalar references[END_REF] that provides exact dependence analysis4 information where statement instances (i.e., statements executed at different loop iterations) and array elements are distinguished. The exact dependence information through this analysis and the use of linear programming techniques to explore the space of legal schedules [START_REF] Feautrier | Some efficient solutions to the affine scheduling problem, II, multidimensional time[END_REF] is what constitutes the base of the polyhedral model for loop transformations. The key idea of all these techniques is that any loop transformation is valid if dependencies are not broken (in other words, if statement A depends on statement B, then B will be always scheduled before A).

In the polyhedral framework, a schedule can be described as a function that associates (logical) dates with operations that is strictly increasing from some starting date (say, 0) and fulfilling the dependencies, as described in Example 8. From these dependencies, we are able to describe valid schedules, for instance S(i , j ) → (i , j ) or S(i , j ) = i + j are valid since they respect dependencies. Clearly these two schedules grow from 0 and are bounded.

i ; k ++) m1 [ i ][ j ] = max ( m1 [i ][ j ] , H [i -k ][ j ] + W [ k ]); m2 [ i ][ j ] = Integer . MIN_VALUE ; for ( k =1; k <= j ; k ++) m2 [ i ][ j ] = max ( m2 [i ][ j ] , H [ i ][ j -k ] + W [ k ]); H [ i ][ j ] = max (0 , H (i -1 ,j -1)+ s ( a[ i ] , b [ i ]) , m1 [ i ][ j ] , m2 [ i ][ j ]); } j i
Similarly, in a numerical automaton, a ranking function associates a non-negative expression to each computation of the program that strictly decreases each time the program takes a transition (e.g., change in loop iterators). The main idea was to use the previous work on multidimensional polyhedral loop scheduling [START_REF] Feautrier | Some efficient solutions to the affine scheduling problem, II, multidimensional time[END_REF], but in the larger scope of general control flow graphs (instead of static for loops and array optimisation) and programs operating on numerical variables.

From monodimensional ranking function to multidimensional

Another observation is that a multidimensional (affine) ranking function can be computed iteratively using an algorithm that generates a monodimensional (affine) function on a maximal set of transitions. This algorithm relies on a notion of "maximal termination power" property that we enforce for the ranking functions synthesised in both papers. In the same way, we prove that despite this greedy approach, our technique is weakly complete (which means that if our invariants are precise enough to prove that there exist a multidimensional affine ranking function, then we find it). Furthermore the multidimensional affine ranking functions that our algorithms compute have the least possible number of dimensions.

Synthesising 1D-ranking functions

To find a suitable function ρ at Line 3 for a subset T of transitions (T ), we use linear programming. The set of inequalities that we need to solve are the following:

• The ρ function must be non-negative on T Algorithm 3 Multidimensional Termination Input: An automaton with T its set of transitions, I k invariants Output: Yes+ρ/Abort 1: i = 0; T = T ; Initialise T to the set of all transitions 2: while T is not empty do 3:

Find a 1D affine function ρ which is decreasing on all t ∈ T and strictly decreasing on a maximal subset T ⊆ T .

4:

Let

ρ i = ρ ; i = i + 1; ρ i defines the i -th component of ρ 5:
If T = return false No multi-dimensional affine ranking. In the sequel, I will denote by: • ρ = x → λ • x + λ 0 the (monodimensional) ranking function to be discovered, where λs are unknown. • I the invariant on the (unique) control point we are considering with m affine constraints

I = {x | m i =1 a i .x -b i ≥ 0}. • τ = ∪ t ∈T τ t
the transition relation for the whole program. For a given transition t ∈ T we denote by Q t the polyhedron that encodes the input/output transition relation on (x, x ) induced by t :

Q t = {y = (x, x ) | Q t y + q t ≥ 0}.
The constraint we have on ρ are thus expressed by:

∀x ∈ I, ρ(x) ≥ 0 (3.2) ∀(x, x ) ∈ τ, x ∈ I, ρ(x) -ρ(x ) ≥ 0 (3.3)
The way we solve them will be different in the following next sections. We will illustrate them on the running example.

The two methods rely on the affine form of Farkas' lemma [START_REF] Schrijver | Theory of linear and integer programming[END_REF]:

Lemma 1 (Farkas' lemma, affine form). An affine form φ : R n → R with φ(x) = c.x +c 0 is non-negative everywhere in a non-empty polyhedron {x | Ax + a ≥ 0} iff:

∃λ ∈ (R + ) n , λ 0 ∈ R + such that φ(x) ≡ λ.(Ax + a) + λ 0
The notation ≡ is a formal equality, which means that x can be eliminated and coefficients identified (from now on, we will use a simple equality sign = for it). In other words:

∃λ ∈ (R + ) n , λ 0 ∈ R + such that c = λ.A and c 0 = λ.a + λ 0
This lemma transforms the search for a ranking function (with an infinite number of unknown coefficients) into the solving of a finite set of affine equations. In other words, it provides a template for the ranking function to be discovered. The rest of the section is devoted to the explanation of the two algorithms (SAS10, PLDI15) on the simple case of programs with one control point 6 and the search for a monodimensional ranking function of maximal termination power. Both methods will be illustrated by the same running example depicted in Example 9.

Example 9 (Running example ). Consider the following automaton, where transitions are specified by ( g uar d ac t i on ):

k 0 t2 x ≤ 10 ∧ 0 ≤ y x := x + 1 y := y -1 t1 0 ≤ x ∧ 0 ≤ y x := x -1 y := y -1
Under initial assumptions x = 5, y = 10, an invariant generator (ASPIC) gives the following inductive invariant for I:

I = {0 ≤ x + 1, x ≤ 11, 0 ≤ y + 1, y ≤ x + 5, x + y ≤ 15}
In other words

I = {x | m i =1 a i .x -b i ≥ 0}. with a = 1 0 -1 0 0 1 1 -1 -1 -1 b = -1 -11 -1 -5 -15
A possible monodimensional strict linear ranking function for this automaton is ρ(x, y) = y + 1: this expression is always non-negative on I, and both t 1 and t 2 make this expression strictly decrease.

SAS10 method

The contributions of [ADFG10] are the following:

• An efficient algorithm to compute ranking functions on arbitrary C numerical programs. Our method, although greedy, is provably complete.

• A new method to derive polynomial upper bounds for the computational complexity (number of transitions) of the source program from the ranking functions.

• The method is implemented as a tool-chain and validated on a collection of test cases from the literature.

Method First, Equation 3.3 is rewritten as:

∀(x, x ) ∈ τ, x ∈ I, ρ(x) -ρ(x ) ≥ t with 0 ≤ t ≤ 1 (3.4)
which express a "weak" positivity constraint, and will allow us to define the "termination power" of a (weak) ranking function as the number of transitions t with t = 1 7 . Of course we want to maximise this number.

In this paper, the LP problem we solve is deducted from the use of the Farkas' Lemma to linearize the constraints coming from equations 3.2 and 3.4:

• On equation 3.2, the ρ function we search for is an affine form, which is positive on the invariant I.

As I = {x | m i =1 a i .x -b i ≥ 0}
, there exist constants α, α 0 such that for all x the following equality holds:

ρ = λ • x + λ 0 = α(Ax -b) + α 0 (3.5)
by identifying the expressions on all lines of this last equality, we obtain one equation per λ i , with m unknowns α i .

• On equation 3.4, the "one-step difference function" ρ(x)ρ(x ) -1 should be positive on each Q t , thus for each transition t there exists constants µ, µ 0 such that for all x, x the following equality holds:

ρ(x) -ρ(x ) -1 = µ t (Q t x -r t ) + µ t 0 .
We obtain a number of equations proportional to the number of transitions times the number of constraints appearing in the sets

Q t s.
• The objective is then to maximise t t , that is, the total number of transitions t where the ranking function is strictly positive.

The result of the LP invocation is the values of α and β unknowns, from with we can derive λs, thus ρ, as well as the transitions on which this ranking function is not strictly positive.

Algorithm 4 Monolithic Monodimensional Termination (SAS10)

Input: A control point with τ its set of transitions, I invariant Output: Yes+ρ/Abort 1: Apply Farkas on I to compute the positivity constraints.

2: Apply Farkas on each t ∈ T to compute the decreasing constraints.

3: Construct the LP instance, call the PIP solver. 4: From the result, compute λs and ρ and return ρ Example 9 (continuing from p. 32). On our running example, recall that I = (A.xb ≥ 0) with:

A = 1 -1 0 1 -1 0 0 1 -1 -1 T and b = -1 -11 -1 -5 -15 T .
• Equations3.5 expressing positivity are thus obtained by identifying terms of the following equality:

λ 1 λ 2 • x y + λ 0 =      α 1 α 2 α 3 α 4 α 5           1 0 -1 0 0 1 1 -1 -1 -1      • x y -      -1 -11 -1 -5 -15      + α 0 ,
i.e.:

λ 1 x + λ 2 y + λ 0 = α 1 (x + 1) + α 2 (-x + 11) + α 3 (y + 1) + α 4 (xy + 5) + α 5 (-xy + 15) + α 0 and finally the system:

     λ 1 = α 1 -α 2 + α 4 -α 5 λ 2 = α 3 -α 4 -α 5 λ 0 = α 1 + 11α 2 + α 3 + 5α 4 + 15α 5
• Now for the equations expressing decrease:

-Q t 1 is the polyhedron defined by the set of 11 (affine) constraints {(x, x ) such that x ∈ I ∧ x ≥ 0 ∧ y ≥ 0 ∧ x = x -1 ∧ y = y -1} (5 constraints coming from I, 6 from the transition, since equalities are transformed into 2 inequalities). Thus, we obtain the existence of µ 1 i , i ∈ [0, 11] such that:

(λ 1 x +λ 2 y +λ 0 )-(λ 1 x +λ 2 y +λ 0 )-1 = µ 1 0 +µ 1 1 (x +1)+. . .+µ 1 10 (y -y +1)+µ 1 11 (y -y -1).
The term µ 1 1 (x +1) comes from the invariant I and the terms µ 1 10 (yy +1) and µ 1 10 (yy -1) come from the transition relation t 1 (y := y -1 provides the two inequalities y ≥ y -1 and y ≤ y -1).

After identification, we obtain the following set of equations:

                 λ 1 = µ 1 1 -µ 1 2 + µ 1 4 -µ 1 5 + µ 1 6 -µ 1 8 + µ 1 9 -λ 1 = µ 1 8 -µ 9 λ 2 = µ 1 3 -µ 1 4 -µ 1 5 + µ 1 7 -µ 1 10 + µ 1 11 -λ 2 = µ 1 10 -µ 1 11 1 = µ 1 1 + 11µ 1 2 + µ 1 3 + 5µ 1 4 + 15µ 1 5 + µ 1 8 -µ 1 9 + µ 1 10 -µ 1 11 -Q t 2
is the polyhedron defined by the set of (affine) constraints {(x, x ) such that x ∈ I ∧ x ≤ 10 ∧ y ≥ 0 ∧ x = x + 1 ∧ y = y -1}. We obtain a set of 5 equalities with 11 new unknowns µ 2 i .

All these equations, with positivity constraints for all the λ, α, µ and variables, as well as i ≤ 1, form a set of equations that we solve with a LP solver under the objective : Max( 1 + 2 ). The LP solver we use (PIP) gives us a solution with 1 = 2 = 1, λ 1 = 0, λ 2 = 1, λ 0 = 1, thus we have found our ranking function ρ : (x, y) → y + 1.

PLDI15 method

The contributions of [GMR15] are the following:

• A reformulation of the problem of finding ranking functions in a more compact Linear Programming instance than in [ADFG10].

• A way to build this instance lazily according to extremal counterexamples (a counterexample is a path where a candidate ranking function increases) inspired by the CEGAR 8 approach.

• The method is implemented as a standalone tool and benchmarked it against existing analysers.

Intuition The intuition we had came from experiments: our LP problems were quite huge comparing to the relative simplicity of the final outputs (in reality, ranking functions are often simple, they do not imply all program variables, in particular). We thus had the intuition that we could use a CEGAR-like approach that could iteratively refine a ranking function candidate. This approach is depicted in Figure 3.3: the algorithm we use takes the form of an iterative loop that stops if it is able to synthetize a ranking function or, like before, if the program may non terminate. To improve a given ranking function candidate, we search in the program if there is a path that makes this ranking function strictly increase (the "counter example"). From this path, we update the system of constraints for the computation for the next candidate.

Is there a path that negates the fact ρ is a strict ranking function?

No Yes Method As we saw on the running example, the number of unknowns in the LP instance we solve is growing quickly with the number of transitions and the number of constraints of the underlying polyhedra. However, the result we obtain is quite simple, and could have been generated with a lesser set of constraints. The first difference with the previous paper is that now we consider the whole transition system τ as a big first order formula with disjunctions, thus the notion of "individual transition" is lost. Then, from the two constraints 3.2 and 3.3 we will only apply Farkas on the positivity constraints, which will enable us to construct LP instances with less unknown variables:

• For positivity, Equation 3.5 is still valid, which we simplify into:

∃α i s.t. λ = m i =1 α i a i (3.6)
since once the condition λ = m i =1 γ i a i is met then an appropriate choice of λ 0 can always be made.

• For the decreasing constraints, we show that they are equivalent to a finite number of constraints obtained by iterating on the generators of a polyhedron:

Definition 5.
Let us denote by P I ,τ the set of all reachable 1-step differences:

P I ,τ = {x -x | x ∈ I ∧ (x, x ) ∈ τ}
The closure of its convex hull will be denoted by P H I ,τ .

From 3.3 we can derive, using linearity, that λ•u ≥ 0 for all u ∈ P I ,τ . Remark that this condition is left unchanged if we replace P I ,τ by P H I ,τ . Without loss of generality, we can now assume that P H I ,τ can be described by a finite number (m) of generators v i , and the equation becomes

∀1 ≤ i ≤ m, λ • v i ≥ 0.
• Now the objective is to maximise the number of v i such that λ • v i > 0.

In order not to explicitly enumerate all the v i s, we define a family of Linear programming instances parametrised by a set V : Definition 6. Given V = {v j |1 ≤ j ≤ N } a set of generators of (the convex hull of) P I ,τ and a set of vectors Constraints(I) = {a i |1 ≤ i ≤ m}, we denote by LP (V, Constraints(I)) the following linear programming instance where α i and i are the unknowns:

     Maximise i i s.t. α 1 , . . . , α m ≥ 0 0 ≤ j ≤ 1 for all 1 ≤ j ≤ N m i =1 α i (v j .a i ) ≥ j for all 1 ≤ j ≤ N
The result of such an LP problem is None if the problem is unfeasible, or a valuation of the α i and i variables maximising the objective function. In the following, we denote as α the vector with α i components. The main result is the following: • LP (V, Constraints(I)) is always feasible.

Proposition 2. Let V = {v j |1 ≤ j ≤ N }
• LP (V, Constraints(I)) gives α i s such that ρ(x) = λ•x+λ 0 with λ = m i =1 α i a i and λ 0 = m i =1 α i b i is a weak ranking function of maximal power on V .

Computing this set V (or, equivalently, any finite set between it and P I,τ ) may be expensive (and the cardinal of V may be exponential in the number of constraints). Obviously, we could compute a disjunctive normal form (DNF) for τ∧I, each disjunct denoting a convex polyhedron [14], compute their generators (x, x ) and collect all resulting x -x ; computing the DNF has exponential cost even if not all disjuncts are needed. The new approach described in this article will only compute extremal points as needed, as opposed to eagerly expanding the DNF.

A Wrong but Intuitive Algorithm Following a quite common technique [START_REF] Clarke | Counterexampleguided abstraction refinement[END_REF] in the static analysis literature, we propose to compute the set of generators and the ranking function incrementally and at the same time. We propose a candidate (weak) ranking function, and search for generators v i where this ranking is only weak. If it is not, we won, if not, we add this generator in a set C . We first propose a simple but somewhat wrong incremental algorithm, which gives the intuition of the correct algorithm detailed in [GMR15]. C is a set of vectors and ρ(x) = λ • x + λ 0 a candidate ranking function. Ask an SMT-solver if ∃u s.t.

I ∧ τ ∧ λ • u ≤ 0. 4:
If Unsat, ρ is a strict ranking function. return ρ 5:

If Sat, we get u from the SMT model.

6:

Add u to C . Let us illustrate this algorithm on our running example.

Example 9 (continuing from p. 32). Let us recall the automaton and its transition relation:

k 0 t2 x ≤ 10 ∧ 0 ≤ y x := x + 1 y := y -1 t1 0 ≤ x ∧ 0 ≤ y x := x -1 y := y -1 τ = (x, y, x , y ) x ≤ 10 ∧ 0 ≤ y ∧ x = x + 1 ∧ y = y -1 ∨ 0 ≤ x ∧ 0 ≤ y ∧ x = x -1 ∧ y = y -1
Recall that we are looking for ρ(x) = λ • x + λ 0 with λ a positive linear combination of the a i s. We will follow Algorithm 5 step by step, repeated steps will be denoted by '.

1.

Beginning with C = {} and ρ(x) = 0, that is: λ = 0 and λ 0 = 0. The unknown vector u is always x-x y-y . First iteration.

2. Sat (I ∧ τ ∧ 0 • u ≤ 0) ? Yes and we have the model u = -1

1 3. C ← -1 1 4. Call LP (C , Constraints(I)) =      Maximise 1 s.t. α 1 , α 2 , α 3 , α 4 , α 5 ≥ 0 0 ≤ 1 ≤ 1 -α 1 + α 2 + α 3 -2α 4 ≥ 1
(The last constraint comes from u • a i for each i .)

The solver answers

α 2 = 1, α 1 = α 3 = α 4 = α 5 = 0.
We deduce λ = a 2 = -1 0 and λ 0 = b 2 = 11.

Second iteration. 2'. Sat

I ∧ τ ∧ -1 0 • u ≤ 0 ? Yes and we have the model u = 1 1 3'. C ← -1 1 ; 1 1 4'. Call LP (C , Constraints(I)) =          Maximise 1 + 2 s.t. α 1 , α 2 , α 3 , α 4 , α 5 ≥ 0 0 ≤ 1 , 2 ≤ 1 -α 1 + α 2 + α 3 -2α 4 ≥ 1 α 1 -α 2 + α 3 -2α 5 ≥ 2
The solver answers

α 3 = 1, α 1 = α 2 = α 4 = α 5 = 0. We deduce λ = a 3 = 0 1 and λ 0 = b 3 = 1. Third iteration.
2". Sat (I ∧ τ ∧ yy ≤ 0) ? No, we stop. Return. We have λ = 0 1 and λ 0 = 1. We obtain ρ(x, y) = y + 1, a strict ranking function for (τ, I). Let us point out the fact that the two models u we obtained correspond to the two transitions t 1 and

t 2 .
Remarks Unfortunately, this simple algorithm suffers from two problems which may prevent its termination:

• First, termination is guaranteed only if the models provided by the SMT tests come from a finite set (then the number of iterations is bounded by the cardinality of that set) and also lie in the boundary of the convex hull P H I ,τ (if not we could accumulate unoptimally tight constraints). To solve this problem, we impose that the model for the SMT-test should minimise λ • u, as in "optimisation modulo theory [START_REF] Nieuwenhuis | On SAT modulo theories and optimization problems[END_REF][START_REF] Sebastiani | Optimization in SMT with L A (Q) cost functions[END_REF]."

• Second, even if the first issue is resolved, the above algorithm terminates only if there is a strict ranking function (λ• v > 0 for all v ∈ V ). Indeed, termination is ensured by the algorithm never choosing twice the same u = xx , which is the case if there exists a (weak/quasi) ranking function such that λ • u > 0. But what if the SMT-solver picks u such that all weak ranking functions λ satisfy λ • u = 0? In this case, the algorithm may not terminate, always picking the same u. To solve that purpose, we force the SMT solver to always search for us that are not linear combinations of the preceding us.

From this remark, we finally construct an algorithm that satisfies the following proposition:

Proposition 3. Algorithm 1 of [GMR15] always terminates and returns a weak ranking function of maximal termination power.

Comparison of the two approaches

Despite the fact that they use the same initial ideas and Linear Programming to search for a monodimensional ranking function of maximal ranking function and finally build a multidimensional one with an iterative algorithm, the two preceding articles have some crucial differences:

• In SAS10, the transition system is given as a union of disjoint functional transitions, in PLDI15 it can be any first order formula.

• In SAS10, the Farkas' lemma is applied to both decreasing constraints and positivity constraints, in PLDI15 we only apply Farkas on the positivity constraints.

• For decreasing constraints, in SAS10 we construct a LP instance whose size is proportional to the number of constraints of a given transition, for all individual transitions. In PLDI15 we enumerate the generators of a bigger set, but lazily. We expected the number of generators actually enumerated to be rather small in practice since "actual programs have simple ranking functions" (build on a limited number of variables, thus can be obtained with a limited number of linear combination of constraints/generators). This has been confirmed by our experiments.

• In SAS10 we only rely on the use of a LP (rational) solver, in PLDI15 we also rely on a Max-SMT solver, which is capable of maximising a linear function on any first order affine formula.

• Experiments show that in PLDI15's implementation our LP instances are one-two orders of magnitude smaller than in SAS10's one (see Section 3.2.6).

From ranking to worst-case

We define the Worst-case Computational Complexity (WCCC) as an upper bound on the number of transitions that are executed, given an initial value of the counter variables.

With this definition, one could over-approximate the WCCC of a terminating program by the total number of reachable states (because a finite trace cannot contain twice the same state), i.e., WCCC ≤ k # Rk or even more conservatively WCCC ≤ k # Ĩk as R k is itself over-approximated by 9 This is a very rough over-approximation but, even worse, this technique can lead to an infinite WCCC, even for a terminating automaton, if some invariant I k is unbounded. Rather, we can use the ranking function itself to prune the invariant sets. Indeed, consider a trace (k 0 , x 0 ), . . . , (k p , x p ) in the execution of the automaton. By definition of a ranking function,

I k .
ρ(k i +1 , x i +1 ) ≺ ρ(k i , x i ).
Since ≺ is a strict order, it follows by transitivity that all ρ(k i , x i ) are distinct in W . Hence, the length of the trace is bounded by the cardinal of the co-domain of ρ:

WCCC ≤ # k ρ(k, Ĩk ) ≤ k #ρ(k, Ĩk ) (3.7)
The first inequality is more accurate but harder to compute as it involves a union of sets. Instead, we use the second less accurate inequality. In [ADFG10] we propose a simple solution based on a computation of the number of the numerical points of a given Z-polyhedron (intersection of an integral lattice, here Z n , and a polyhedron, here I ). The main tool we use for that purpose are Ehrhart polynomials [START_REF] Clauss | Handling memory cache policy with integer points counting[END_REF][START_REF] Verdoolaege | Counting integer points in parametric polytopes using Barvinok's rational functions[END_REF]. The experimental results of Section 3.2.6 show that these evaluations are precise enough for classical algorithms of the literature.

Experimental results

Implementation For SAS10, we implemented a tool suite with C2FSM and ASPIC as front-ends (See Section 2.2.1) The third tool, RANK (3000 lines of C++) , from the integer interpreted automaton and the invariants given by ASPIC, tries to prove the termination of the program by computing (multidimensional affine) ranking functions. In case of success, RANK computes the worst-case computational complexity of the program. Also, in case of failure (denoted by "Don't Know"), RANK tries to exhibit a counterexample that causes non-termination. The linear programs involved in the termination part are solved thanks to the PIP tool. The PIP tool may fail if the generated LP instance is too big.

For PLDI15, we implemented our prototype TERMITE in 3k lines of OCAML 10 . As depicted in Figure 3.5 Termite uses LLVM 11 to compile C code into a Single Static Assignment intermediate representation [START_REF] Cytron | Efficiently computing static single assignment form and the control dependence graph[END_REF]. PAGAI [START_REF] Henry | PAGAI: a path sensitive static analyzer[END_REF][START_REF] Henry | The Pagai static analyser[END_REF] is used to compute invariants from the LLVM IR. The transition relation 9 Here, the notation S means the integral points in a set S , and # S denotes the cardinal of S .

Results

The experimental results first show that the method is expressive enough to prove termination and compute the WCCC of challenging polynomial programs from the literature. Both tools RANK (SAS10) and TERMITE (PLDI15) perform well on these benchmarks. We also show that the size of the LP instances are drastically decreased by the use of our incremental technique implemented in TERMITE. Finally, we compare TERMITE with existing state-of-the art tools, and show that despite the fact the tool is only a prototype, it compares well with other more mature tools.

Expressivity of the tools Our tool chain has been tested on a set of benchmarks from the literature. Most of the examples were collected in [START_REF] Chawdhary | Ranking abstractions[END_REF] from many other papers dealing with termination analysis. They can be found at the following web address: http://compsys-tools.ens-lyon.fr/wtc/ index.html.

On Tables 3.1 and 3.1, the first two columns identify the test cases. The symbol ♣ indicates a test case we developed to check our algorithm 13 . Columns 3 to 5 give statistics about the (generated) automaton: number of relevant variables, of control points, of transitions. The next column gives the dimension of the ranking function found by our algorithm. The next column gives the timing measurements on a 2 GHz Pentium with 1 GByte of memory running Debian 2.6. The "Analysis" measures include the invariants computation time from the ASPIC file, the computation of the ranking function, and the evaluation of the WCCC. In general, the WCCC is the maximum of several parametric expressions valid on different domains of the program inputs. To make the table simpler, the last column gives only the expression that can reach the maximum value.

Scalability of TERMITE compared to RANK

We compared the two tools on an modified version of the WTC test suite. On these benchmarks, due to limitations in its front-end and invariant generator, RANK could only run on 46 files from the WTC test suite, solving 25 of them in total time 76 ms, with average linear programming problem (lines, columns) = (584, 229), much higher than TERMITE's (5, 2). On some examples however, RANK is able to prove termination that TERMITE is unable to prove. This essentially comes from the combination of its front-end C2FSM and its invariant generator ASPIC that sometimes perform clever graph transformations on the control-flow graph and thus are able to synthesise better invariants than PAGAI (the invariant generator used for TERMITE).

Comparison of TERMITE and state-of-the-art tools

In Table 3.3 We have compared TERMITE with LOOPUS14 [START_REF] Zuleger | Bound analysis of imperative programs with the size-change abstraction[END_REF], APROVE 15 [55], Ultimate Büchi Automizer 16 , RANK [START_REF] Alias | Rank: a tool to check program termination and computational complexity[END_REF] (with the C2FSM frontend and ASPIC 17 [GS14] accelerating invariant generator), on examples from POLYBENCH 18 , WTC (V2) 19 , the termination competition 20 and some sorting algorithms (Table 3.3). TERMITE solves 33% more examples than LOOPUS, in twice the time. APROVE and ULTIMATE are considerably slower.

All these tools have different approaches to prove termination:

• APROVE uses a complex front-end and relies on term rewriting systems.

• The ULTIMATE technique essentially consist in covering the set of program traces by ω-regular languages of terminating traces ("modules"). The termination argument for each module can be obtained from a variety of approaches; thus their approach truly is a meta-approach since a variety of sub-provers can be used. We in fact think that our technique could be adapted into a sub-prover for their system.

• The algorithm in LOOPUS [START_REF] Zuleger | Bound analysis of imperative programs with the size-change abstraction[END_REF] is similar to ours in some ways; however, it explores all paths in a given loop, and uses heuristics to syntactically derive ranking functions from the transitions of the loop. In our experiments, Loopus is able to quickly conclude for termination in many cases since simple arguments are very often sufficient to prove that a given loop terminates Difficulties A termination analyser typically consists in 1) a front-end 2) an invariant generator 3) a termination analysis. One therefore compares whole tool-chains instead of only the termination analyses. One difficulty is that some front-ends are more picky than others; for instance, APROVE's front-end crashes on some LLVM opcodes. We have made some reasonable efforts to have our examples accepted by the various tools when we could identify some obvious reason why they could not be processed by the front-end or invariant generator.

Improving scalability

Improving the scalability of a given termination algorithm might not be sufficient, and clearly none of our two analysers is capable to deal with large C programs:

• Because of technical reasons: the robustness of the parsers, the fact that we have to deal with possibly a large number of statement types.

• Because the underlying invariant generators do not scale well: for challenging programs polyhedral invariants are really necessary, but their generation is expensive. Improving the scalability of such techniques is a challenging problem as we saw in the previous chapter.

• Because of more intrinsic reasons: a given program is made of a possibly large number of procedures, and only examining each at its turn might not be sufficient. Moreover for a given procedure, the number of constraints that are generated might be too big for some LP solvers.

In the research report [START_REF] Andrieu | Christophe Alias and Laure Gonnord Modular termination of C programs[END_REF], we propose an incremental scalable analysis implemented in a tool called STOP (short paper [AAG12]). This tool is based on two classical techniques of static analysis, slicing, and summaries. The experiments were made above the RANK tool-chain.

Example 10 (Running example: mergesort). We detail our method on an implementation of the merge sort of an array. The code is taken from [START_REF] Michael | Practical methods for proving program termination[END_REF] and is depicted in Figure 3.6. For sake of readability, we drew boxes around inner-loops, and commented the end of outer loops. For this example, the RANK tool-suite fails with TWO_MANY_VARIABLES error because the size of the underlying linear programming instance given to PIP pis too big. end for 12: end function Example 10 (continuing from p. 42). The result of the slicing algorithm on the end the motivating example code is depicted in Figure 3.7 lation between initial variables x 0 , y 0 , . . . and final variables x, y, . . .. Then the following code is called a summary of C : x0 = x; y0 = y; ... x = random(); y = random();... if(!R_C(x0,y0, ..., x, y, ..

Method

A slicing for termination

.)) abort

The summary of C is obviously an abstraction of C and thus can be used for proving the termination of C.

Example 10 (continuing from p. 42). In the running example, loop3 can be replaced by: i0=i;n0=n; i=random();y=random(); if (i > n) abort cont ext ← g etC ont ext (st at ement , pci nv s) provides precise invariants for the sub-automaton to be analysed. Compute a summary of the loop and replace in the code.

end if 17: end function

The main function MODULARTERM takes as input a statement and a structure that is able to give an over approximation of the context of each statement of the program under analysis. These invariants are computed using ASPIC as input/output relations. MODULARTERM proceeds the abstract syntactic tree with a depth-first traversal, evaluating each subtree to the value OK if it terminates, or Don't Know if the analysis does not succeed to answer. If a sub-tree is evaluated to Don't Know, the analysis fails and stops with Don't Know output.

Computing summaries can also be applied at the granularity of functions, but we didn't implement it.

Experimental results

We implemented our method as a driver over the RANK tool-chain, written in C++. The total number of LOC is 3000 for the driver itself, and 150 additional lines for statistics. The code intensively uses Table 3.4 -Experiments detailed in [START_REF] Andrieu | Christophe Alias and Laure Gonnord Modular termination of C programs[END_REF] . For each benchmark, we give its number of programs, the average number of lines of codes before (LoCA) and after (LoCB) slicing, Regressions denote the number of regressions (examples that were proved OK with WTC and for which STOP now answers Don't Know). We also give average execution times of each method. the method shows it pertinence in terms of timing results and in terms of precision (it handles sipmamergesort, which was not handled by RANK before, as the generated LP instance was too big for PIP) in 22 seconds, but we had to manage the very last step by hand by providing a coarser abstraction than the one obtained by ASPIC). Thus STOP is able to deal with larger programs than WTC and seems to scale well. Unfortunately, due to lack of time and manpower we did not make any further experiments, and STOP is no longer maintained.

Benchmark #Progs

A case study: termination for JIT compilers

In the paper [START_REF] Raphael Ernani Rodrigues | Realworld loops are easy to predict : a case study[END_REF], we study the relevance of fast and simple solutions to compute approximations of the number of iterations of loops (loop trip count) of imperative real-world programs. The context of this work is the use of these approximations in compiler optimisations: most of the time, the optimisations yield greater benefits for large trip counts, and are either innocuous or detrimental for small ones.

In this particular work, we argue that, although predicting exactly the trip count of a loop is undecidable, most of the time, there is no need to use computationally expensive state-of-the-art methods to compute (an approximation of) it. We support our position with an actual case study. We show that a fast predictor can be used to speedup the JavaScript JIT compiler of Firefox -one of the most well-engineered runtime environments in use today.

Method

Key observation: real-world loops are simple The motivation of using simple heuristics come from our early work on abstract acceleration ([GH06], [START_REF] Gonnord | Abstract Acceleration in Linear Relation Analysis[END_REF]), in which we compute an overapproximation of the transitive closure of loops at low cost. The experiments show that in many of the analysed programs, static analysers get more precise results just because they are able to precisely deal with loops of the form for (int i = M; i < N; i++) (which is an example of a accelerable loop) in the most precise way.

Following these experiments, we decided to implement a light and fast heuristic to dynamically compute an approximation of the number of executions of loop to be executed, whose main specification is to be as precise as possible in the case of such simple loops.

Fast Trip Count Prediction at runtime

We apply our heuristic dynamically. In other words, we instrument a program -or its interpreter -to estimate the trip count immediately before the first iteration of the loops. Our instrumentation inspects the state of the variables used in the stop condition of each loop.

In the sequel, we only consider perfect loops with a single "interval" exit-condition, i.e. loops of the form : while (e1 e2) { some computation }. For this kind of loops, we assume that the trip count will be the absolute difference between e 1 and e 2 . For instance, in a loop such as for (int i = M; i < N; i++), we say that its trip count will be |val(N) -val(i)| (val(x) is the runtime value of x when the test is performed).

For each loop of this form, we insert a new instruction before the loop, according to Algorithm 8 21 . Let us point out that this algorithm only performs a single O(1) operation per loop, without actually looking inside the body of the loop.

However, for loops of the form for (int i = M; i < N; i=i+s) (s and N invariants in the loops), this heuristic gives an overapproximation of the total number of loops, and the most precise result if s = 1. There is no guarantee of precision for the general case, of course, but the experiments will show that this simple-blind instrumentation fits our needs in practice. Because our heuristic is so simple, we can execute it quickly. This perfectly suits the needs of a JIT compiler. Insert instruction t r i pcount = |e 1 -e 2 | before L, giving L .

3: end if

Application: Hot code detection in JIT compilers

Virtual environments that combine interpretation and compilation face a difficult question: when to invoke the JIT compiler [START_REF] Duesterwald | Software profiling for hot path prediction: Less is more[END_REF]? Premature compilation might produce binaries that do not run long enough to amortise the cost of the JIT transformation. On the other hand, late compilation might delay the optimisation of critical parts of the program. As an example, the Firefox browser separates native execution in two parts. After a few rounds of interpretation, the baseline compiler translates the program into non-optimised native code. Once this basic native code is deemed hot, it is recompiled, this time by IonMonkey, an optimising compiler. Figure 3.8 illustrates this behaviour.

First-level compila0on

Second-level compila0on 3.5 -Hit rate of our simple heuristic for JavaScript (Bottom). N denotes the number of iterations of a loop observed via profiling, so the interval [N , N ] gives us the exact predictions. We only produce estimates for interval loops, that account for 71% of the loops in our benchmarks. We have deployed our predictor in the interpreter and in the baseline compiler used in Firefox, as we illustrate in Figure 3.8. The current distribution of Firefox calls the baseline compiler after 10 events, and the optimising compiler after 1,000 events. If we predict that a loop will run for more than 10 iterations, we call the baseline compiler immediately, bypassing the warm-up period. Similarly, once in native mode, we call the optimising compiler immediately upon finding a loop that we estimate to run more than 1,000 times. The experiments depicted in Table 3.5 show that although our method is neither sound or complete, it is capable of precise approximation of the actual trip count of interval loops (approximately 90% of the loops in the JavaScript benchmarks where correcly predicted). Figure 3.9 shows the speedup that we obtain using our trip count predictor to perform earlier invocation of the JIT compiler. Each number is the average of 100 runs. We call the baseline compiler immediately once we predict that a loop will iterate 10 times, and we call IonMonkey immediately once we predict that a loop will iterate 1,000 times. Figure 3.9, reveals that our technique has been able to speed up some benchmarks by a substantial factor. We have also detected slowdowns in a few scripts. This negative behaviour happens in benchmarks that iterate for a very short time. In this case, early compilation is not able to pay off the cost of code generation. All these results advocate the use of simple preprocessing for proving the termination (or counting the number of loops) of real-world programs that may include proper slicing and simple patternmatching.

JavaScript ]1, N ] ] N , N /2] ]N /2, N ] [N , N ] [N , 2N [ [2N , N 2 [ [N 2 ,

Conclusion

This chapter is a synthesis of my contributions in the area of termination. The combination of powerful static analyses with techniques coming from the compilation community has demonstrated its great potentiality in this particular domain. I believe that there is a continuum to be explored from the kernel algorithms to their implementation and their application to specific domain benchmarks. In this work we particularly focused on the termination of numerical programs with complex control, for which scalability was already a major concern. Our contributions significantly improved both the applicability and the scalability of termination provers for this kind of programs. The next step is now to handle complex data structures or pointer variables, which are in our current setting abstracted away by a coarse abstraction. Proving termination or functional correctness of work-list algorithms would be the next challenge. Being able to express and prove properties of pointers and array is a necessary step toward that purpose, that we will examine in the next chapter.

Dealing with memory

There are numerous motivations for developing static analyses to deal with memory:

• The previous static analyses on numerical variables are only valid when the variables are stored in different memory locations. If numerical variables and pointer variables coexist in a given program, we must be sure that the numerical variables locations are only accessed by their name. If they also can be accessed via their address, then we must take aliasing into account. This advocates for the design of precise alias analyses.

• Some crucial safety properties such as the absence of array-out-of-bound accesses need to be ensured in low level like C where there is no clever mechanism such as typing or size tracking that ensures them. In the case of the C language particularly, there is a need for analyses that are capable of ensuring such safety properties for general purpose big programs. This advocates for the design of low cost algorithms that can run in a reasonable amount of time inside production compilers.

• Many compiler optimisations, such as loop transformations, tiling, are very limited in practice. Indeed one particular feature of imperative programming languages remains to be handled satisfactorily by the current state-of-the-art approaches: the disambiguation of pointer intervals. This advocates for the design of specialised analyses tailored for some application characteristics (here, array intensive-computations kernels).

• Static analyses for array properties are still suffering from a certain lack of precision. Indeed the main difficulty is to generate universally quantified invariants with arrays, as we have to deal with an unbounded number of cells and their content at the same time. We believe that the design of such static analyses will benefit to the two communities of verification and compilation.

This chapter summarises my contributions to the design of static memory analyses, with a focus on scalability as well as expressivity and applicability.

Summary and outline Section 4.1 describes the model of programs we use to design most of the analyses of the chapter. Then the chapter presents three contributions in the domain of sparse analyses of pointers. Section 4.2 exposes the design of sparse memory region analysis that is capable of eliminating useless array bound checks. This technique is based on our previous work on symbolic range analyses of numerical variables (section 2.5). Section 4.3 then details two static analyses designed to improve the precision of compiler pointer disambiguation.

The last contribution of the chapter, described in Section 4.4, is a new abstraction of programs with arrays. This technique transforms a given program and a property to be proved into a formula without arrays, whose satisfiability entails the property.

Model of programs

In this chapter, we particularly focus on the design of scalable analyses for C programs with pointers. This led us to choose the SSA intermediate representation variant e-SSA (to be able to transfer information from tests, as we already saw in section 2.5), and a syntax/semantics which mimics the LLVM Intermediate Representation [START_REF] Lattner | LLVM: A compilation framework for lifelong program analysis & transformation[END_REF]. Our analyses will be described on the mini language we describe in Figure 4.1, whose semantics will not be described here (it can be found in [SMO+14] for instance). Branches and jump instructions will not be represented in our CFGs. All the instructions in this mini-language have the property to be atomic in the sens that they generate only one new information for a given analysis. This knowledge appears due to memory allocation (malloc), deallocation (free), pointer arithmetic, intersections and phi-functions. Each of these instructions defines new variables, whose names are associated with information. For instance, the instruction p 0 = free(p 1 ) copies p 1 to p 0 , and binds p 0 to a memory chunk of size 0. Moreover, in our language, there is no more &x instruction since in LLVM, when the address of a variable is taken, then this variable is no longer in SSA form, it will be represented in memory (thus it becomes a pointer).

Validation of memory accesses through symbolic analyses

The C programming language does not prevent out-of-bounds memory accesses. There exist several techniques to secure C programs; however, these methods tend to slow down these programs substantially, because they populate the binary code with runtime checks. To deal with this problem, in [SMO+14] we have designed and tested two static analyses -symbolic region and range analysis (described in Section 2.5) -which we combine to remove the majority of these guards. In addition to the analyses themselves, we bring the following other contributions :

• We describe live range splitting strategies that improve the efficiency and the precision of our analyses.

• We show how to deal with integer overflows, a phenomenon that can compromise the correctness of static algorithms that validate memory accesses.

• A complete tool chain combined with Address Sanitizer, which improves its applicability.

HDR Laure Gonnord 50/92

Context : Address Sanitizer

AddressSanitizer [START_REF] Serebryany | AddressSanitizer: a fast address sanity checker[END_REF] is an industrial-quality tool built on top of the LLVM compiler [START_REF] Lattner | LLVM: A compilation framework for lifelong program analysis & transformation[END_REF]. This tool produces instrumented binaries out of C source code, to either log or prevent any out-of-bounds memory access. AddressSanitizer has a fairly large community of users, having been employed to instrument browsers such as Firefox and Chromium. This instrumentation has a cost: in general it slows down computationally intensive programs by approximately 70%. The analyses we will design in this section will enable us to remove about half of this overhead, keeping all the guarantees that AddressSanitizer provides. Unlike Java where arrays are associated with their sizes, in C, arrays are not packed together with size information. We have to infer this size automatically. This is the object of the symbolic region analysis.

Symbolic Region Analysis

To solve this problem, we resort to static analysis. We have designed a novel region analysis, which binds each pointer to an interval of valid offsets. This analysis makes use of the symbolic region analysis we depicted in Section 2.5 Like the symbolic range analysis from Section 2.5.1, the region analysis also associates with each variable an abstract state given by an interval. However, here this abstract state has a very different interpretation. If we say that W (p) = [ , u], then we mean that all the addresses between the offsets p + and p + u are valid. As we will state in Proposition 4, it is always safe to dereference a pointer if it includes the address zero among its valid offsets.

v1 = alloc(n) v1 v2 = v1 + 1 W(v1) = [0, n -1] v2 W(v2) = [-1, n -2] v3 = v1 + n v2 W(v3) = [-n, -1] n Figure 4.
2 -Semantics for "valid offsets."

Splitting Required by Symbolic Region Analysis

Our symbolic region analysis takes information from instructions that define pointers and instructions that free memory. We deal with the first source of information via the standard static single assignment form, as we do for the symbolic range analysis. Splitting after free is also simple, although this operation requires guidance from alias analysis. If we free the region bound to a pointer p at a program label , we know that after every alias of p will point to empty memory space. To make this information clear to our region analysis, we rename every alias p k of p to a fresh name p k ". We then initialise each of these new names with the constant zero. In this way, our region analysis will bind these variables to empty array sizes.

The SymRegion abstract domain Our analysis of regions rests on the semi-lattice SymRegion (S 2 , , , [-∞, +∞], ), which is the inverse of the structure used in the symbolic range analysis of Section 2.5. Here, we have a meet operator " ", such that: The least element of our semi-lattice is , the greatest is [-∞, +∞]. Therefore, whereas in Section 2.5 we were always expanding ranges, here we are always contracting them. In other words, the symbolic range analysis finds the largest ranges covered by variables, i.e., it is a may analysis. On the other hand, the symbolic region analysis finds the narrowest regions that pointers can dereference, i.e., it is a must analysis. In the abstract interpretation jargon, we say that we are computing under-approximations.

[a 1 , a 2 ] [b 1 , b 2 ] = , if a 2 < b 1 or b 2 < a 1 [max(a 1 , b 1 ), min(a 2 , b 2 )], otherwise HDR Laure Gonnord 51/92 CHAPTER 4. MEMORY DOMAINS v = c, c ∈ N W (v) = v 1 = alloc(v 2 ) W (v 1 ) = [0, R(v 2 ) ↓ -1] a = b W (a) = W (b) free(v); v 1 = 0; v 2 = 0 . . . v 1 , v 2 , . . . ∈ Π(v) W (v 1 ) = W (v 2 ) = . . . = v = φ(v 0 , v 1 ) W (v) = W (v 0 ) W (v 1 )
v 1 = v 2 + n with n ∈ N W (v 1 ) = if W (v 2 ) = , else [W (v 2 ) ↓ -n,W (v 2 ) ↑ -n] v 1 = v 2 + v 3 with v 3 scalar W (v 1 ) =      if W (v 2 ) = else [W (v 2 ) ↓ -R(v 3 ) ↓ , W (v 2 ) ↑ -R(v 3 ) ↑ ]
The widening we use is thus a lower widening1 , under the terminology of [START_REF] Miné | Backward under-approximations in numeric abstract domains to automatically infer sufficient program conditions[END_REF]. This operator is defined as follows:

W 1 ∇W 2 = if W 2↓ > W 1↓ or W 2↑ < W 1↑ W 2 otherwise where [a, b] ↓ = a and [a, b] ↑ = b.
An instance of region analysis is thus a set of constraints that we solve with Kleene iterations with widening points at phi-nodes points. These constraints are extracted from the program's source code, according to the rules in Figure 4.3. The figure naturally distinguish between scalars and pointers. Pointers are variables that have been initialised with the alloc instruction, or that are computed as functions of other pointers. Scalars are all the other variables; hence, they are always bound to the region . For the last constraint, we must encode the fact that we cannot add a pointer and a variable, thus v 3 must be a scalar. Therefore, if p 1 is defined as p 1 = p 2 + v, then its region is given by the admissible region of p 2 added to all the possible values of v. That is why we must consider the interval range of v. Before moving on, we draw the reader's attention to the abstract semantics of the free(v) instruction. As we explained in Section 2.5.1, this instruction leads us to rename every alias of v, and all these new names will be bound to the new region .

Our region analysis uses a widening operator for φ-functions, to ensure that our algorithm terminates in face of pointer arithmetic. These ranges correctly tell us, for instance, that the largest (safely) addressable offset from address p is N -1. The ranges that we find for the program in Figure 4.4a let us remove bound checks for the memory accesses at lines 7 and 11. The region of p i tells us that p i = p[i ] and p i -1 are safe addresses. The region of p j indicates that p j = p[ j ] and p j + 1 are also safe addresses. On the other hand, the range of p m tells us that it is not safe to dereference this pointer without a bound check. In this case, we have a false-positive, because we conservatively assume that a memory access is unsafe.

Example 6 (continuing from p. 22). If we run our region analysis on the program of Figure 4.4a, then we get that W

(p) = [0, N -1], W (p i ) = [0, 1], W (p j ) = [-1, 0], and W (p m ) = [0, -∞] = . N = • p = alloc(N ) i 0 = 0 m 0 = 0 j 0 = N -1 i 1 = φ(i 0 , i 2 ) j 1 = φ(j 0 , i 2 ) m 1 = φ(m 0 , m 2 ) (i 1 < j 1 )? i f = σ(i 1 ) j f = σ(j 1 ) p m = p + m f * p m = 0 i t = σ(i 1 ) j t = σ(j 1 ) p i = p + i t * p i = -1 p j = p + j t * p j = 1 i 2 = i t + 1 j 2 = j t -1 m 2 = m t + 1
Correctness of the Symbolic Region Analysis. Proposition 4 states the key property of our symbolic region analysis, which comes from the fact we follow the Abstract Interpretation framework. We have defined the proposition for loads, but it is also true for instructions such as * v 1 = v 2 , which store the contents of v 2 into the address pointed by v 1 .

Proposition 4. Let P be a program and pc

∈ N, such that P [pc] is v 2 = * v 1 . If 0 ∈ W (v 1 )
, then P cannot be stuck at pc.

The paper contains other contributions sketched in Figure 4.5:

• The safety of the two previous analyses (Symbolic Ranges, Symbolic Regions) is guaranteed if and only if there is no buffer overflow. We designed a slicing algorithm to find variables and expressions that should be prevented from buffer overflows. For that purpose, we use the Sparse Evaluation Graph [START_REF] Cytron | Efficiently computing static single assignment form and the control dependence graph[END_REF], and propagate data dependencies as well as control dependencies. The result of this analysis is given to an instrumentation tool to add additional overflow guards before the problematic instructions.

• We have included an optional tainted flow analysis [START_REF] Schwartz | All you ever wanted to know about dynamic taint analysis and forward symbolic execution (but might have been afraid to ask)[END_REF] in our framework. If we are interested in preventing only buffer overflows caused by malicious inputs, then we can restrict our attention to operations that are influenced by values produced by external functions. We designed a constraint-based static analysis to identify which memory accesses can be manipulated by malicious users, in such a way that the other accesses do not need to be guarded. More details can be found in [SMO+14].

• We have designed an interprocedural analysis to propagate "less than information" from a given procedure to all the functions it calls. After we analyse the body of a function g , we have enough information to compute a less-than relationship between variables declared in its body. We compute such relationship for every pair of variables that are used as actual parameters of other functions called in the body of g . Let f (v 1 , v 2 , . . . , v n ) be an instruction, within the body of g , that calls a certain function f with actual parameters v i , 1 ≤ i ≤ n. We determine the less-than relation between each v i , v j , 1 ≤ i , j ≤ n. Additionally, we also determine minimum lower bounds to all the scalar variables v i .

Instrument the program to prevent integer overflows from compromising the correctness of our analyses. Only instructions that influence memory accesses need instrumentation.

Integer Overflow Analysis

LLVM +

AddressSanitizer Check if a memory access can be controlled by an adversary, e.g, is function of the program's input. If this is not possible, avoid inserting the guard

Tainted Flow Analysis

Find R(i) = [l, u], the lower and the upper symbolic bounds of variable i. Symbols are made of unknown inputs and constants that we find in the program code.

Symbolic Range Analysis

Find W(v) = [0, N], the valid addressable offsets that can be dereferenced from pointer v, using the results of symbolic range analysis.

Region Analysis

int x = v[i] Original program Efficient, but unsafe if (inBounds(i, v)) int x = v[i]; else error();

Instrumented program

Safe, but inefficient

int x = v[i]

Optimized program Safe and efficient

If l >= 0, and u < n, then remove guard

The tainted flow analysis is an optional part of our framework.

Validation

Experimental setting We run our experiments in a twelve-core Intel(R) Xeon(R) CPU E5-2620 at 2.00GHz, with 15,360KB of cache, and 16GB of RAM. Neither our compiler, nor our benchmarks, run in parallel. The GREENARRAYS toolchain is tested over the integer programs available in the SPEC CPU 2006 benchmark suite. The paper [SMO+14] reports the experiments, that show that:

• our approach is practical -all our analyses run in acceptable time;

• it is effective -we can eliminate a reasonable number of bound checks, hence speeding up safe code and reducing its energy consumption; and • it is competitive with state-of-the-art approaches to bound check elimination. I only report a few of them here.

Analyses Numbers and Run Times In section 2.5, Figure 2.9, we already show the comparison of the runtime of our symbolic range analysis with existing other techniques. The overflow analyses cause the insertion of an overflow test on 77% of all the arithmetic instructions, which represent themselves 3.5% of the total of the instructions of the LLVM bytecode. Figure 4.6 depicts the relative times (in seconds) of all the static analyses of the toolchain for some of the most representative programs of the SPEC benchmark. The less-than tests represent the overhead for our analysis to be interprocedural, the Figure shows here clearly a possibility of improve-ment. However, the total analysis time shows that our toolchain scales well and the total analysis time is compatible with their use inside production compilers. Impact of the analysis Figure 4.7 shows how much we speed up the binaries produced by Address-Sanitizer with our analyses. On average, we achieve a speedup of 17%. This is less than the 48% of bound checks that we eliminate, but these instructions account for only a small part of the entire execution cost. The compulsory cost of a guard consists of two loads, two comparisons, and two branches. By eliminating these guards, we improve also the quality of the code produced by the register allocator, as we increase the average size of basic blocks. We are still 15.2% slower than unsafe programs, i.e., programs without runtime bound checks.

! " " # $ % & % ' " ( ) * # + , -& ( , ' " . # ! / ( ) * # / ) ' , 0 + + # . 1 2 3 -, 4 # . ) ) , -# 5

Static pointer analyses for optimising compilers

Pointer analysis is one of the most fundamental compiler technologies. This analysis lets the compiler distinguish one memory location from others; hence, it provides the necessary information to transform code that manipulates memory. Given this importance, it comes as no surprise that pointer analysis has been one of the most researched topics within the field of compiler construction [START_REF] Hind | Pointer analysis: Haven't we solved this problem yet?[END_REF]. This research has contributed to make the present algorithms more precise [START_REF] Hardekopf | The ant and the grasshopper: fast and accurate pointer analysis for millions of lines of code[END_REF][START_REF] Zhang | Efficient subcubic alias analysis for C[END_REF], and faster [START_REF] Hardekopf | Flow-sensitive pointer analysis for millions of lines of code[END_REF][START_REF] Shang | On-demand dynamic summary-based points-to analysis[END_REF]. Pointer and heap analyses have also been designed for other imperative languages like Java, where the size of allocated regions are statically known, but where some optimizations can be done if an analysis can precisely capture the relationship between method calls [107]2 . Nevertheless, one particular feature of imperative programming languages remains to be handled satisfactorily by the current state-of-the-art approaches: the disambiguation of pointer intervals: state-ofthe-art pointer analyses often fail to disambiguate regions addressed from a common base pointer via different offsets, as explained by Yong and Horwitz [START_REF] Hsi | Pointer-range analysis[END_REF]. Therefore, we claim that, to reach their full potential, compilers need to be provided with more effective alias analyses. In this particular example, messages have two parts: an identifier, which is stored in the beginning of the array, and a payload, which is stored right after. This behaviour is depicted in Figure 4.9.

The loops in lines 3-6 and 7-10 fill up each of these parts with data If a compiler can prove that the stores at lines 4 and 8 are always independent, then it can perform optimisations that would not be possible otherwise. For instance, it can parallelize the loops, or switch them, or merge them into a single body.

No alias analysis currently available in either GCC or LLVM is able to disambiguate the stores at lines 4 and 8. These analyses are limited because they do not contain range information.

Example 12 (Running example for "less-than" based pointer disambiguation). To motivate the need for a new points-to analysis that is capable of deriving "less than" information, we show its application

The notion of abstract location Our analysis binds variable names to sets of locations and ranges. We denote the set of locations in a program by L oc: L oc = {loc 0 , loc 1 . . . , loc n-1 } where n is the number of allocation sites. In our representation, i.e., Figure 4.1, new locations are created by malloc operations.

Z = atoi(...) b = malloc(Z) "loc 0 s = malloc(...) "loc 1 p = b N = Z m 0 = s i 0 = p e = p + N i 1 = φ(i 0 , i 3 ) (i 1 < e)? i 2 = i 1 ∩ [-∞, e1] * i 2 = 0 t 0 = i 2 + 1 * t 0 = 0xF F i 3 = i 2 + 1 i 4 = i 1 ∩ [e, +∞] f = e + strlen(m 0 ) i 5 = φ(i 4 , i 7 ) m 1 = φ(m 0 , m 2 ) (i 5 < f )? i 6 = i 5 ∩ [-∞, f -1] * i 6 = * m 1 m 2 = m 1 + 1 i 7 = i 6 + 1

Collecting information for pointers

We already saw in Section 2.5 that we want the collected abstract information to be invariant in the live range of all variables. For pointers, new information appear at memory allocation (malloc), deallocation (free), pointer arithmetic, intersections and φfunctions. Each of these instructions defines new variables, whose names are associated with information. For instance, the instruction p 0 = free(p 1 ) copies p 1 to p 0 , and binds p 0 to a memory chunk of size 0.

MemLocs , an Abstract Domain of Pointer Locations. We associate pointers with tuples of size n:

(SymBoxes • ∪ ⊥) n
; n being the number of program sites where memory is allocated (the cardinal of L oc) and • ∪ is the disjoint union. Let @(loc i ) denotes the actual address value returned by the i t h malloc of the program. By construction, all actual addresses are supposed to be offsets of a given @(loc i ). The abstract value GR(p) = (p 0 , . . . , p n-1 ) represents (an abstract version) of the set of memory locations that pointer variable p can address throughout the execution of a program: Definition 8 (Abstraction). A set of actual addresses, S = {s | ∃i ∈ N, d ∈ N, s = @(loc i )+d } is abstracted by α(S) = (p 0 , p 1 . . . , p n-1 ) where :

• p i = ⊥ if there is no address in S which is an offset of @(loc i )

• p i = α SymBoxes ({d ∈ Z | s = @(loc i ) + d ∈ S}), otherwise.
The offsets from a given pointer are abstracted all-together in the SymBoxes lattice.

The goal of our Global Range (GR)analysis is to compute such an abstract value for each pointer of the program. Some elements in a tuple GR(p) are bound to the undefined location, e.g., ⊥. These elements are not interesting to us, as they do not encode any useful information. Thus, to avoid keeping track of them, we rely on the concept of support, which we state in Definition 9.

Definition 9 (Support). We denote by supp GR (p) the set of indexes for which p i is not ⊥ :

supp GR (p) = {i | p i =⊥}.
For sake of readability, let us denote for instance GR

(p) = (⊥, [l 1 , u 1 ], ⊥, [l 3 , u 3 ], ⊥), by the set GR(p) = {loc 1 +[l 1 , u 1 ], loc 3 +[l 3 , u 3 ]}.
In the concrete world, this notation will mean that pointer p can address any memory location from @(loc 1 ) + l 1 to @(loc 1 ) + u 1 , and from @(loc 3 ) + l 3 to @(loc 3 ) + u 3 .

For instance, consider that l 1 = 3, u 1 = 5, l 3 = 3 and u 3 = 8. GR(p) = {loc 1 + [3, 5], loc 3 + [3, 8]} is then depicted in Figure 4.12. Given the two abstract values GR(p 1 ) = (p 1 0 , . . . p 1 n-1 ) and GR(p 2 ) = (p 2 0 , . . . p 2 n-1 ), the union GR(p 1 ) GR(p 2 ) is the tuple (q 0 , . . . , q n-1 ) where:

loc0 loc1 + l1 loc1 + u1 loc1 loc2 loc3 loc3 + l3 loc3 + u3
q i = ⊥ if p 1 i = p 2 i = ⊥ p 1 p 2 else
and GR(p 1 ) GR(p 2 ) if an only if all involved (symbolic) intervals of p 1 are included in the ones of

p 2 : ∀i ∈ [0..(n -1)], p 1 i p 2
i (considering ⊥ R and ⊥ R = R for all non-empty intervals R). We how have to define the widening operator for our abstract domain: We call the new abstract domain we have just defined MemLocs .

Example 11 (continuing from p. 56). For the example depicted in Figure 4.11 where we only have two malloc sites denoted by loc 0 and loc 1 , we will obtain the following results:

GR(p) = GR(b) = {loc 0 + [0, 0]}, GR(m 0 ) = GR(s) = {loc 1 + [0, 0]}, GR(e) = loc 0 + [N , N ], GR(m 1 ) = loc 1 + [1, +∞], GR(i 7 ) = loc 0 + [N + st r l en(m 0 ), N + st r l en(m 0 ) + 1].

Constraint generation for the MemLocs abstract domain (GR)

The abstract semantics of each instruction in our core language is given by Figure 4.13. Figure 4.13 defines a system of equations whose fixed point gives us an approximation on the locations that each pointer may dereference.

Definition 11 (Concretization). Given GR(p) an abstract value (a set of "abstract addresses for p"), denoted by GR(p)

= (p 0 , . . . , p n-1 ), we define its concretization as follows:

γ(GR(p)) = i ∈supp GR (p) {@(loc i ) + o, o ∈ p i }
The concretization function of this abstract value is thus a set of (concrete) addresses, obtained by shifting a set of base addresses by a certain value in SymBoxes . Without any surprise, (α, γ) is a Galois connection. We solve the constraint system by Kleene iteration over the system of constraints, with one step of descending iteration.

j : p = malloc (v) with v scalar ⇒ GR(p) = (⊥, . . . , [0, 0] j t h component , . . .) p = free (v) with v scalar ⇒ GR(p) = (⊥, . . . , ⊥ ) v = v 1 ⇒ GR(v) = GR(v 1 ) q = p + c with c scalar variable ⇒     
GR(q) = (q 0 , . . . , q n-1 ) with

q i = ⊥ if p i = ⊥ p i + R(c) else q = φ(p 1 , p 2 ) ⇒ GR(q) = GR(p 1 ) GR(p 2 ) q = p 1 ∩ [-∞, p 2 ] ⇒       
GR(q) = (q 0 , . . . , q n-1 ) with

q i = ⊥ if (p 1 i = ⊥ or p 2 i =⊥) p 1 i [-∞, p 2 i ↑ ] else q = p 1 ∩ [p 2 , +∞] ⇒       
GR(q) = (q 0 , . . . , q n-1 ) with Answering GR Queries Our queries are based on the following result, that is an immediate consequence of the fact our analysis is an abstract interpretation:

q i = ⊥ if (p 1 i = ⊥ or p 2 i = ⊥ ) p 1 i [p 2 i ↓ , +∞] else q = * p ⇒ GR(q) = ([-∞, ∞], . . . , [-∞, ∞]) * q = p ⇒ Nothing
Proposition 5 (Correctness). Let p and p be two pointers in a given program then :

if supp GR (p) ∩ supp GR (p ) = or ∀i ∈ supp GR (p) ∩ supp GR (p ), p i p i = then γ(GR(p)) ∩ γ(GR(p )) = .
In other words, if the abstract values of two different pointers of the program have a null intersection, then the two concrete pointers do not alias. This result is directly implied by the abstract interpretation framework. Thanks to this result, we implement the query Q GR (p, p ) as:

• If GR(p) and GR(p ) have an empty intersection, then "they do not alias."

• Else "they may alias."

Example 11 (continuing from p. 56). In the example, since GR(i 7 ) = loc 0 +[N +st r l en(m 0 ), N +st r l en(m 0 )+ 1] and GR(i 2 ) = loc 0 + [0, N -1], i 7 and i 2 never alias.

About local analysis

The global pointer analysis is not path sensitive. As a consequence, this analysis cannot, for instance, distinguish the effects of different iterations of a loop upon the actual value of a pointer, or the effects of different branches of a conditional test on that very pointer. To solve this issue, we propose to combine the global analysis with a local analysis (called LR) where we create information at merge nodes (a new abstract location is created). The detail of this analysis can be found in [START_REF] Vitor Paisante | Symbolic Range Analysis of Pointers[END_REF].

CGO 17 : Pointer Disambiguation via Strict Inequalities

The contribution of the paper [MPR+17] is the (scalable) combination of pointer analysis with a "Pentagon-like" analysis which is capable to derive "less than" information for numerical variables as well as pointer variables. This analysis also relies on the symbolic interval lattice SymBoxes described in Section 2.5. We report the main ideas of the analysis, the complete formalisation can be found in the paper.

An additional splitting strategy

The objective of the analysis is to derive less-than information (Less Than Analysis (CGO'17) (LT)) a program into SSA form, for numerical variables as well as pointer variables.

To derive such information that still have to stay invariant on live ranges, we propose a new splitting strategy depicted in Figure 4.14. The idea is to derive from an instruction x 1 = x 2 + n and a precomputed range for n that implies that n < 0, the information x 1 < x 2 . However, this information is only valid after the instruction, thus we invent a new name for x 2 , namely x 3 (Figure 4.14b). We let x 1 = x 2 + n ∥ 〈x 3 = x 2 〉 denote a composition of two statements, x 1 = x 2 + n and x 3 = x 2 . The second instruction splits the live range of x 2 . Both statements happen in parallel. Thus, x 1 = x 2 +n ∥ 〈x 3 = x 2 〉 does not represent an actual assembly instruction; it is only used for notation convenience. Similarly, when transforming conditional tests, we let 〈x 1t = x 1 , x 2t = x 2 〉 denote two copies that happen in parallel: x 1t = x 1 , and x 2t = x 2 . Whenever there is no risk of ambiguity, we write simply 〈x 1t , x 2t 〉. As usual, parallel copies and φ-functions are removed before code generation, after the analyses that require them have already run. Constraints are solved via a worklist algorithm. We initialise LT(x) to V , for every variable x. During the resolution process, elements are removed from each LT, until a fixed point is achieved. We prove that this process terminates and its correction.

x 1 = x 2 + n || x 3 = x 2 renaming x 2 to x 3 at if dominates R(n)=[l,u],u<0 ----------→ x 1 = x 2 + n (a) (x 4 < x 1 )? x 4t = x 4 x 1t = x 1 x 4f = x 4 x 1f =
Example 13 (continuing from p. 61). The rules in Figure 4.16 produce the following constraints for the program in Figure 4.15a LT(x 0 ) = , LT(x 1 ) = {x 0 } ∪ LT(x 0 ), LT(x 2 ) = LT(x 1 ) ∩ LT(x 3 ), LT(x 3 ) =

x 0 = [0, 1] x 1 = x 0 + 1 x 2 = φ(x 1 , x 3 ) x 4 = x 2 -2 x 3 = x 2 + 1 (x 4 < x 1 )? x 6 = φ(x 4t , x 3 , x 4 ) • true f alse (a) Initial CFG x 0 = • x 1 = x 0 + 1 x 2 = φ(x 1 , x 3 ) x 4 = x 2 -2|| x 5 = x 2 x 3 = x 2 + 1 (x 4 < x 1 )? x 4t = x 4 x 1t = x 1 x 4f = x 4 x 1f = x 1 x 6 = φ(x 5 , x 3 , x 4t ) • (b) CFG after splitting
x = • 1 LT(x) = x 1 = x 2 + n 2 LT(x 1 ) = {x 2 } ∪ LT(x 2 ) x 1 = x 2 -n ∥ 〈x 3 = x 2 〉 3 LT(x 3 ) = {x 1 } ∪ LT(x 2 ) LT(x 1 ) = x = φ(x 1 , . . . , x n ) 4 LT(x) = LT(x 1 ) ∩ . . . ∩ LT(x n ) (x 1 < x 2 )? t : 〈x 1t , x 2t 〉 f : 〈x 1 f , x 2 f 〉 5                  LT(x 2t ) = {x 1t } ∪ LT(x 1 ) LT(x 1 f ) = LT(x 2 )
LT(x 1t ) = LT(x 1 ) {x 2 }∪LT(x 2 ), LT(x 4 ) = , LT(x 5 ) = {x 4 }∪LT(x 3 ), LT(x 1t ) = {x 4t }∩LT(x 4t ), LT(x 1 f ) = LT(x 1 ), LT(x 4 f ) = LT(x 1 ), LT(x 4t ) = LT(x 4 ), LT(x 6 ) = LT(x 3 ) ∩ LT(x 4 f ) ∩ LT(x 5 ).

LT(x 2 f ) = LT(x 2 )
To solve them, we initialise every LT set to {x 0 , x 1 , x 2 , x 3 , x 4 , x 6 , x 1 f , x 1t , x 4 f , x 4t }, i.e., the set of program variables.

Chaotic iterations on those constraints achieves the following fixed point:

LT(x 0 ) = LT(x 4 ) = LT(x 4t ) = ; LT(x 1 ) = LT(x 2 ) = LT(x 4 f ) = LT(x 1 f ) = LT(x 6 ) = {x 0 }; LT(x 3 ) = {x 0 , x 2 }; LT(x 5 ) = {x 0 , x 4 }; and LT(x 1t ) = {x 4t }.
Answering Queries The less-than check that we have discussed in this section lets us compare pointers directly, if they are bound to a less-than relation, or indirectly, if they are derived from a common base. This observation gives the query Q LT (p 1 , p 2 ):

• If p 1 ∈ LT(p 2 ) or p 2 ∈ LT(p 1 ), then "they do not alias."

• Else if p 1 = p + x 1 and p 2 = p + x 2 with the same base pointer p and x 1 ∈ LT(x 2 ) or x 2 ∈ LT(x 1 ), then "they do not alias." • Else "they may alias."

Example 12 (continuing from p. 56). On the example of Figure 4.10, we are able to disambiguate the two accesses to v + i and v + j of the partition procedure, since we are able to infer j ∈ LT (i ) at lines 9-11. The C standard refers to arithmetic types and pointer types collectively as scalar types [START_REF]The C programming language[END_REF]{ §6.2.5.21}. Notice that the less-than analysis that we have discussed thus far works seamlessly for scalars; thus, it also builds relations between pointers. For instance, the common idiom "for(int* pi = p; pi < pe; pi++);" gives us that pi < pe inside the loop.

Experimental Evaluation

Implementation We have implemented our range analysis in the LLVM compiler, version 3.5. An interprocedural version of the "less-than" analysis has been implemented in LLVM version 3.7. In this section, we show a few numbers that we have obtained with these two implementations. All our experiments have been run in a standard machine, Intel i7-4770K, with 8GB of memory, running a Linux Desktop system. Our goal with these experiments is to show:

• that our alias analyses are more precise than other alternatives of practical runtime;

• that it scales up to large programs.

It is worth underling that these two evaluations have been reproduced by an independent committee "Artefact Evaluation Committee"4 at CGO'16 and CGO'17.

Runtime

The chart in Figure 4.17 shows how our CGO 16 analysis scales when applied on programs of different sizes. We have used the 50 largest programs in the LLVM benchmark suite. These programs gave us a total of 800,720 instructions in the LLVM intermediate representation, and a total of 241,658 different pointer variables. We analysed all these 50 programs in 8.36 seconds. We caneffectively -analyse 100,000 instructions in about one second. In this case, we are counting only the time to map variables to values in SymBoxes . We do not count the time to query each pair of pointers, because usually compiler optimisations perform these queries selectively, for instance, only for pairs of pointers within a loop. Also, we do not count the time to run the out-of-the-box implementation of range analysis. The chart provides strong visual indication of the linear behaviour of our algorithm, the linear correlation between time and number of instructions being 0.98.

Charts in Figure 4.18 compares the two approaches for middle-sized benchmarks (from 2000 to 15000 instructions). While the CGO'17 implementation is faster in average for these benchmarks, figure 4.18b demonstrates an exponential behaviour. We believe that some of our implementation choices could clearly be improved in further versions of this implementation. However, for middlesized benchmarks, the solving time is already less than 10 ms, which is already a satisfactory result. Pointer analyses evaluation in LLVM To measure the precision of our methods, we compare them against the techniques already in place in the LLVM compiler. Our metric is the percentage of pointer queries disambiguated. To generate queries, we resort to LLVM's aa-eval pass, which tries to disambiguate every pair of pointers in the program. Our main competitor will be LLVM's basic disambiguation technique, the basic-aa algorithm. This analysis uses several heuristics to disambiguate pointers, relying mostly on the fact that pointers derived from different allocation sites cannot alias in well-formed programs 5 . We also compare the results obtained by the the "scalar-evolution-based" (SCEV) alias analysis. This analysis tries to infer closed-form expressions to the induction variables used in loops. With this information, SCEV can track the ranges of indices which dereference array a within the loop. Contrary to our analysis, SCEV is only effective to disambiguate pointers accessed within loops and indexed by variables in the expected closed-form.

Precision of the CGO'16 method

To evaluate the precision of the CGO'16 method, we have chosen three benchmarks that have been used in previous work that compares pointer analyses: Prolangs [START_REF] Ryder | A schema for interprocedural modification side-effect analysis with pointer aliasing[END_REF], PtrDist [START_REF] Zhao | Dynamic memory optimization using pool allocation and prefetching[END_REF] and MallocBench [START_REF] Grunwald | Improving the cache locality of memory allocation[END_REF]. Figure 4.19 reports the the results in terms of percentage of pairs of pointers that are reported not to alias compared with the total number of pointer pairs. We first notice that in general all the pointer analyses in LLVM disambiguate a relatively low number of pointers. This happens because many pointers are passed as arguments of functions, and, not knowing if these functions will be called from outside the program, the analyses must, conservatively, assume that these parameters may alias. Second, we notice that our pointer analysis is one order of magnitude more precise than the scalar-evolution based implementation available in LLVM. Finally, we notice that we are able to disambiguate more queries than the basic analysis. Furthermore, our results complements it in non-trivial ways. In total, we tried to disambiguate 3.093 million pairs of pointers. Our analysis found out that 1.29 million pairs reference non-overlapping regions. The basic analysis has been able to distinguish 953 thousand pairs. By combining these two analyses, we extended this number to 1.439 thousand pairs of pointers. SCEV could not increase this number any further. McCat's qbsort (Total: .20 -Effectiveness of our alias analysis (LT), when compared to LLVM's basic alias analysis on the 100 largest benchmarks in the LLVM test suite. Each point in the X-axis represents one benchmark. The Y-axis represents total number of queries (one query per pair of pointers), and number of queries in which each algorithm got a "no-alias" response (the higher the better). Figure 4.20 shows the results of the three alias analyses when applied on the 100 largest benchmarks in the LLVM test suite. Our method rarely disambiguates more pairs of pointers than BA. Such result is expected: most of the queries consist of pairs of pointers derived from different memory allocation sites, which BA disambiguates, and we do not analyse. Figure 4.21 compares our analysis (LT), the basic analysis (BA) of LLVM and a variant of Andersen's analysis (CF) Our numbers have been obtained in LLVM 3.7, whereas CF's has been produced via LLVM 4.0 6 We emphasise that both versions of this compiler produce exactly the same number of alias queries, and, more importantly, BA outputs exactly the same answers in both cases. This experiment reveals that there is no clear winner in this alias analysis context. BA+LT is more than 20% more precise than BA+CF in three benchmarks: lbm, milc and gobmk. BA+CF, in turn, is three times more precise in omnetpp. The main conclusions that we draw from this comparison are the following: • These analysis are complementary.

Precision of the CGO'17 method

• Mainstream compilers still miss opportunities to disambiguate alias queries.

Impact on further analyses and optimisations

Applicability of the CGO'17 method: program dependence graph construction. We show how our new alias analysis improves the construction of a client analysis, the Program Dependence Graph (PDG) construction, a classic data structure introduced by Ferrante et al. [START_REF] Ferrante | The program dependence graph and its use in optimization[END_REF]. We use the implementation of PDGs available in the FlowTracker system [START_REF] Rodrigues | Sparse representation of implicit flows with applications to side-channel detection[END_REF], which has a distribution for LLVM 3.7. The PDG is a graph whose vertices represent program variables and memory locations, and the edges represent dependences between these entities. An instruction such as a[i ] = b creates a data dependence edge from b to the memory node a[i ]. The more memory nodes the PDG contains, the more precise it is, because if two locations alias, they fall into the same node. In the absence of any alias information, the PDG contains at most one memory node; perfect alias information yields one memory node for each independent location in the program. The full methodology of these experiments can be found in the [MPR+17] paper. The results depicted in Figure 4.22 show that our analysis combined with BA clearly improves the size of the resulting PDG.

Impact on LLVM memory optimisations

We also studied the impact of our analyses on further optimisations in the context of Maroua Maalej's Phd thesis. A more detailed study can be found in her manuscript. In this paragraph, we show how (a modified and extended version of) our CGO'17 analysis [MPMQPG17] does not only outperform the state-of-the-art pointer LLVM analyses in terms of the total number of pointer pairs that are proved to be non aliasing, but also the additional information is relevant for further analyses and optimisations, and in particular LICM, as we show in Example 14.

Example 14 (Loop invariant code motion (LICM)). In Figure 4.23 we depict a toy example in which the underlined statement could be moved from inside the loop to its pre-header at line 5 (N is supposed to be positive). This optimisation is valid if the statement is invariant in the loop, and also the loop is guaranteed to execute at least once. The first condition is true since the two pointers p 2 and p 1 do not alias. An improved alias analysis thus benefits to the LICM pass.

Figure 4.24 shows that our analysis improves the performance of the LICM optimisation by a factor of 1.77. This factor does not include the programs for which our analysis combined with the other LLVM passes reports errors. These experiments demonstrate that there is still a need for more precise analyses. Moreover, our experience in the understanding of the LLVM optimisation phases shows that their design should be rethought in order to benefit more from generic analyses passes like ours: the tests they perform in order to perform a given optimisation are often too restrictive.

Static analyses of programs manipulating arrays

As we saw previously , verifying safety properties of numerical programs is already a hard job, and it is even harder if the program acts upon arrays or other forms of maps. Contrarily to the preceding analyses where the properties to prove were only about sets of addresses, here we want to express and find relational properties between a given (set of ) address(es) and its (their) content, which is much harder. The main difficulty is to find a way to express and decide properties that may depend on the content of an unbounded number of memory addresses, or "cells." Transposing the approaches for verifying programs operating upon Boolean and integer values (e.g. abstract interpretation, counterexampleguided abstraction refinement. . . ), is not immediate.

In the SAS paper [MG16], together with D. Monniaux, we propose an alternative approach to ad-hoc array abstract domains. Instead, we generate an abstraction as a scalar problem and feed it to a preexisting SMT solver, with tunable precision. Our transformed problem is expressed using Horn clauses, a common format with clear and unambiguous logical semantics for verification problems.

Models of programs

The syntax of the (CFG of the) programs we consider is depicted in Figure 4.25. This is a simple language with numerical and array variables. Any statement in the program (control flow graph) will be: i) either an array read to a fresh variable, v=a[i]; the variables of the program are (x, i , v) where x is a vector of arbitrarily many variables; ii) either an array write, a[i]=v; (where v and i are variables) the variables of the program are (x, i , v) before and after the statement; iii) or a scalar operation, including assignments and guards over scalar variables. More complex statements can be transformed to a sequence of such statements, by introducing temporary variables if needed: for instance, a

[i ] = a[ j ] is transformed into temp = a[ j ]; a[i ] = temp.

Program Verification with Horn Clauses

As we already saw in Chapter 2, Section 2.1.1, the classical approach to program verification consists in computing inductive invariants on control-flow graphs. In this work, we propose to express these invariants to be found as predicates on the program variables, and the control-flow graph itself as a whole Horn formula.

P i (x) ∧ f (x, x ) =⇒ P (x )
where for all i :

• P i and P are predicates.

• x, x are variables that are local to the clause.

• f is a formula over a given theory (here, integer arithmetic with or without arrays). A Horn formula is a set of CHCs.

The property to be proved is also expressed in term of a formula, and the verification problems consists in checking if the program semantics implies the property. This is illustrated in example 15. Various tools can solve systems of Horn clauses (depending on the underlying theory, of course), that is, can synthesise suitable predicates I , which constitute inductive invariants. In this article, we tried Z3 7 with the PDR fixed point solver [START_REF] Hoder | Generalized property directed reachability[END_REF], Z3 with the SPACER solver [START_REF] Komuravelli | Automatic Abstraction in SMT-Based Unbounded Software Model Checking[END_REF][START_REF] Komuravelli | Smt-based model checking for recursive programs[END_REF], 8

i := 0 i < n a[i] := 42 i := i + 1 i ≥ n (b) Its CFG,
∀n ∈ Z ∀a ∈ Arr (Z, Z) n > 0 =⇒ loop(n, 0, a) (4.1) ∀n, i ∈ Z ∀a ∈ Arr (Z, Z) i < n ∧ loop(n, i , a) =⇒ loop(n, i + 1, store(a, i , 42)) (4.2) ∀n, i ∈ Z ∀a ∈ Arr (Z, Z) i ≥ n ∧ loop(n, i , a) =⇒ end(n, i , a) (4.3) ∀x, n, i ∈ Z ∀a ∈ Arr (Z, Z) 0 ≤ x < n ∧ end(n, i , a) =⇒ sel ec t (a, x) = 42 (4.4)
where store(a, i , v) is array a where the value at index i has been replaced by v and select(a, x) denotes a[x]. Equation 4.4 encodes the property to prove. The encoding of the problem is then given to solvers: if a given solver returns "sat", it means that it has been able to synthesise invariants for each unknown predicate, namely init, state and end.

None of the tools we have tried (Z3, SPACER, ELDARICA) has been able to solve this system, presumably because they cannot infer universally quantified invariants over arrays. 10 Indeed, here the loop invariant needed is 0

≤ i ≤ n ∧ (∀k 0 ≤ k < i =⇒ a[k] = 42). While 0 ≤ i ≤ n is
inferred by a variety of approaches, the rest is tougher.

Most software model checkers attempt constructing invariants from Craig interpolants obtained from refutations [START_REF] Christ | Interpolation Modulo Theories[END_REF] of the accessibility of error states in local [START_REF] Hoder | Generalized property directed reachability[END_REF] or global [START_REF] Mcmillan | Lazy abstraction with interpolants[END_REF] unfoldings of the problem. However, interpolation over array properties is difficult, especially since the goal is not to provide any interpolant, but interpolants that generalise well to invariants [START_REF] Alberti | An extension of lazy abstraction with interpolation for programs with arrays[END_REF][START_REF] Alberti | Polyhedra to the rescue of array interpolants[END_REF]. This contribution instead introduces a way to derive universally quantified invariants from the analysis of a system of Horn clauses on scalar variables (without array variables).

An encoding of programs with arrays

To use the power of Horn solvers, we soundly abstract problems with arrays to problems without arrays. In the Horn clauses for Ex. This is the same Galois connection [START_REF] Cousot | Abstract interpretation frameworks[END_REF] as some earlier works [START_REF] Monniaux | A simple abstraction of arrays and maps by program translation[END_REF] [40, Sec. 2.1]; yet, as we shall see, our abstract transformers are more precise. For simplicity, in the sequel, we will consider that the vector of values of all variables (except arrays) of the program lies in Z d , the array indexes as well as the content of each cell also being of type Z.

Definition 13. The "one distinguished cell" abstraction

of I ⊆ Z d × Arr (Z, Z) is α(I ) = {(x, i , a[i ]) | x ∈ Z d , i ∈ Z}. The concretization of I ⊆ Z d × (Z × Z) is γ(I ) = {(x, a) | ∀i ∈ Z (x, i , a[i ]) ∈ I }.
In other words, during the abstraction, the array variable a will be replaced by a couple (i , a i ) ∈ Z 2 , and predicates on a will be transformed into predicates on (i , a i ).

We depict in Figure 4.27 the abstract semantics of the statements of our mini-language. All the variables inside predicates are universally quantified.

• For scalar only statements, the abstract transformers are straightforward, they express the numerical semantics of each transition → on scalar values, the array being unchanged. For instance, for a program with two variables x, y and a unique array a, a transition from control points 1 to 2 of the form x = y + 1 is abstracted into

I 1 (x, y, i , a i ) ∧ x = y + 1 ∧ y = y =⇒ I 2 (x , y , i , a i ).
10 Some of these tools can however infer some simpler array invariants. 11 For instance, I l oop = l oop(n, i , a), I end = end (n, i , a). new(a) I (x) =⇒ I (x, k, a k )

x 0 = c, c ∈ N I (x, x 0 , k, a k ) =⇒ I (x, c, k, a k ) x 0 = numexpr I (x, k, a k ) ∧ R(x, x ) =⇒ I (x , k, a k ) x 0 = x 1 (test example) I (x, k, a k ) ∧ x 0 = x 1 =⇒ I (x, k, a k ) x 0 = a[i ](read) k = i ∧ I (x, i , x 0 ), (k, a k ) ∧ I (x, i , x 0 ), (i , a i ) =⇒ I (x, i , a i ), (k, a k ) I (x, i , x 0 ), (i , a i ) =⇒ I (x, i , a i ), (i , a i ) a[i ] = x 0 (write) I (x, i , v), (k, a k ) ∧ i = k =⇒ I (x, i , v), (k, a k ) I (x, i , v), (i , a i ) =⇒ I (x, i , v), (i , v) Φ(x, k, a[k])(property at ) I (x, k, a k ) =⇒ Φ(x, k, a k ).
Figure 4.27 -Horn Clauses Generation (Abstract transformers). All statements are considered to be from the control point to , x designs the vector of all scalar variables. Properties are also abstracted.

• For a write statement a[i ] = v the semantics is expressed as two formulas, depending on whether the distinguished cell is i or not.

• For a read statement, the second formula expresses that a i is assigned to variable v. The (first) nonlinear rule may be more difficult to comprehend. The intuition is that, to have both a i = a[i ] and a k = a[k] at the read instruction with a given valuation (x, i ) of the other variables, both a i = a[i ] and a k = a[k] had to be reachable with the same valuation. We use two separate rules for k = i and k = i for better precision. A single rule I 1 (x, i , v), (k, a k ) ∧ I 1 (x, i , v), (i , a i ) =⇒ I 2 (x, i , a i ), (k, a k ) would not enforce that if i = k then a i = a k in the consequent.

Applying this transformation on a programs thus gives a set of Horn Clauses that describes the abstract semantics of the program. This transformation is sound and incomplete.

0 ≤ k < n =⇒ loop(n, 0, k, a k ) (4.5) 0 ≤ k < n ∧ i < n ∧ loop(n, i , k, a k ) =⇒ write(n, i , k, a k ) (4.6) 0 ≤ k < n ∧ i = k ∧ write(n, i , k, a k ) =⇒ incr(n, i , k, a k ) (4.7) write(n, i , i , a i ) =⇒ incr(n, i , i , 42) (4.8) 0 ≤ k < n ∧ incr(n, i , k, a k ) =⇒ loop(n, i + 1, k, a k ) (4.9) 0 ≤ k < n ∧ i ≥ n ∧ loop(n, i , k, a k ) =⇒ end(n, i , k, a k ) (4.10)
Finally, we add the postcondition:

0 ≤ k < n ∧ end(n, i , k, a k ) ⇒ a k = 42 (4.11)
A solution to the resulting system of Horn clauses is found by Z3, thus the property is proved.

Extensions

In [MG16] we provide several extensions to the previous transformation:

• Maps. Maps can be considered as arrays with cells of a given type. Nothing in our abstraction uses the fact that the cells suppose that our indices are integers, thus our transformations is also valid for maps.

• 2D arrays. 2D arrays can be classically expressed as 2-indices maps. Our abstraction can thus be easily adapted to deal with them.

• Expressing sortedness and relations between k-cells. The Galois connection of Def. 13 expresses relations of the form ∀k ∈ Z ϕ(x, k, a[k]) where x are variables from the program, a a map and k an index into the map a; in other words, relations between each array element individually and the rest of the variables. It cannot express properties such as sortedness, which link two array elements:

∀k 1 , k 2 ∈ Z k 1 < k 2 =⇒ a[k 1 ] ≤ a[k 2 ]
. For such properties, we need two "distinguished cells", with indices k 1 and k 2 . In the paper we provide adaptations of the abstraction for the case of multiple cells.

• Multisets. Our abstraction for maps may be used to abstract (multi)sets, which permits to express for instance that a given array is a permutation of the input.

Experiments

Implementation We implemented our prototype VAPHOR in 2k lines of OCAML. VAPHOR takes as input a mini-Java program (a variation of WHILE with array accesses, and assertions) and produces a SMTLIB2 file 13 . The core analyser implements the translation for one and two-dimensional arrays described in Section 4.4.3.

A second prototype was re-factored later by J. Braine, which first computes a SMTLIB2 file within the theory of Arrays, then computes its array abstraction and then produces a SMTLIB2 without arrays.

A demo page can be found at the following URL: http://laure.gonnord.org/pro/demopage/ vaphor/ Experiments We have tested our analyser on several examples from the literature, including the array benchmark proposed in [START_REF] Dillig | Fluid updates: Beyond strong vs. weak updates[END_REF] also used in [START_REF] Bjørner | On solving universally quantified Horn clauses[END_REF] (Table 4.1); and other classical array algorithms including selection sort, bubble sort and insertion sort (Table 4.2). We compared our approach to existing Horn clause solvers capable of dealing with arrays. All these files are provided in the demo page. Limitations Our tool does not currently implement the reasoning over array contents (multiset of values). Experiments for these were thus conducted by manually applying the transformations described in this article in order to obtain a system of Horn clauses. For this reason, because applying rules manually is tedious and error-prone, the only sorting algorithm for which we have checked that the multiset of the output is equal to the multiset of the inputs is selection sort. Some examples from Dillig et al. [START_REF] Dillig | Fluid updates: Beyond strong vs. weak updates[END_REF] involve invariants with even/odd constraints. The Horn solvers we tried do not seem to be able to infer invariants involving divisibility predicates unless these predicates were given by the user. For these cases we added these even/odd properties as additional invariants to prove.

Efficiency caveats Our tool does not currently simplify the system of Horn clauses that it produces. We have observed that, in some cases, manually simplifying the clauses (removing useless variables, inlining single antecedents by substitution. . . ) dramatically reduces solving times. Also, precomputing some simple scalar invariants on the Horn clauses (e.g. 0 ≤ k < i for a loop from k to i -1) and asserting them as assertions to prove in the Horn system sometimes reduces solving time.

We have observed that the execution time of a Horn solver may dramatically change depending on minor changes in the input, pseudo-random number generator seed, or version of the solver. For instance, the same version of Z3 solves the same system of Horn clauses (proving the correctness of selection sort) in 3m 40s or 3h 52m depending on whether the random seed is 1 or 0.14 Furthermore, we have run into numerous problems with solvers, including one example that, on successive versions of the same solver, produced "sat" then "unknown" and finally "unsat", as well as crashes.

For all these reasons, we believe that solving times should not be regarded too closely. The purpose of our experimental evaluation is not to benchmark solvers relative to each other, but to show that our abstraction, even though it is incomplete, is powerful enough to lead to fully automated proofs of functional correctness of nontrivial array manipulations, including sorting algorithms. Tools for solving Horn clauses are still in their infancy and we thus expect performance and reliability to increase dramatically.

Conclusion

In this chapter I summarised the contributions made in the domain of memory analyses, from scalable static analyses for pointer regions to a very expressive program abstraction to prove functional properties of programs with arrays.

The first contributions on memory abstract domains show that the sparse dataflow framework is the appropriate technique to design pointer analyses that scale. They also illustrate the need for specialised analyses to handle more or less restricted classes of programs/classes of properties. These analyses must be designed by carefully looking at the structural properties of the program to analyse. The last contribution shows that we can design expressive abstractions that are capable of generating array invariants with a relatively low solving cost. We think that this work deserves to be pursued in the direction of more expressive data-structures and also revisited in the compilation community for instance to generate information for further code optimisation.

Conclusion and perspectives

The contributions made in this document addressed the design of efficient and expressive static verifiers or compilers. The approach we consider is the study of each class of properties (numerical properties, termination, memory properties) through various static approaches that explore the limits of expressivity and scalability. The algorithms are implemented and validated through examples of the literature or state-of-the art benchmarks. This choice was motivated by the numerous applications we can find in software validation and compilation/code optimisation.

Since I joined the LIP lab in Lyon (France) in 2013, I have been developing a new vision which fosters the combination of abstract interpretation algorithms with compilation-inspired techniques and tools. Compilation is both an application domain and an inspiration for the design of new solutions. I also benefit from the proximity of the ever growing French Community of Compilation, Code Generation, Analysis1 that I co-animate with Florian Brandner and Fabrice Rastello.

Summary of the manuscript

This manuscript developed the contributions made in the domain of static analysis. Each chapter exposed a different application domain and the techniques we developed for enhancing precision, scalability and applicability.

Chapter 2 presented the design of numerical static analyses for numerical programs. The first contribution of the chapter is a novel iteration strategy for abstract interpreters that compute numerical invariants ( [MG11]). The "path focusing" algorithm enhanced abstract interpretation with a more "semantic-directed" computation which results in more accurate numerical invariants. The second part of the chapter exposes our work on the design of a novel abstraction for synchronous languages [GG11], [START_REF] Feautrier | Enhancing the Compilation of Synchronous Dataflow Programs with a Combined Numerical-Boolean Abstraction[END_REF], having in mind the performance and the readability of the code produced by synchronous compilers. The third contribution of the chapter is a novel abstract domain for parametric intervals [SMO+14] whose goal is to provide efficient information on the range of variables inside SSA (Single Static Assignment)-based compilers.

Chapter 3 exposed a set of contributions that were made in the domain of static analyses for proving termination of sequential programs. Working on the relationship between program scheduling and termination, we first proposed a (quasi-complete) algorithm [ADFG10] to compute multidimensional ranking functions from program invariants. This algorithm was implemented in a standalone tool called RANK, around which we tried to design heuristic strategies ([AAG12], [START_REF] Andrieu | Christophe Alias and Laure Gonnord Modular termination of C programs[END_REF]) to scale better. Then we proposed an enhancement of the algorithm [GMR15] based on algebraic properties of polyhedra. Finally, in [START_REF] Raphael Ernani Rodrigues | Realworld loops are easy to predict : a case study[END_REF], we demonstrated that proving termination and computing worst-cases can sometimes be done with relatively simple strategies for general purpose programs.

Chapter 4 presented more recent contributions focusing more on memory properties and optimisation. The first contribution [SMO+14] is the design of a novel array-out-of-bound detection toolchain inside the LLVM compiler. This work relied on precise yet scalable set of static analyses specially tailored for the application. The chapter then exposed two sparse static analyses for pointers ([PMB+16], [MPR+17]) that were designed with a particular thorough effort on splitting strategies to improve both scalability and precision. The chapter then described a more fundamental work on array properties [MG16] that can be seen as one of the foundations of my future work, especially from an expressivity perspective.

Future research topics

My contributions strongly promote the cross-fertilisation of abstract-interpretation techniques with compiler techniques (scheduling, thorough work on intermediate representations). I believe that the link between the two communities should be reinforced in the following directions:

• Code optimisations are potential clients for code analyses. The tiny link between them is still currently mainly unexplored, and code optimisations do not often clearly state which kind of information they rely on. The properties to find would most probably be simple from the static analysis community, however there will remain two challenges: the design of scalable analyses to infer them, and their efficient use for code optimisation. The Phd thesis of Maroua Maalej is only the first step toward a better understanding of this link.

• Code analysis techniques are potentially a source of inspiration in the design of more expressive compilation techniques. We believe that the use of abstractions is still at its early age inside compilers, especially in the domain of aggressive compilation of HPC kernels. The design of expressive code analyses for code (scheduling) optimisation will be enabled by a thorough study of the notion of dependencies with various techniques from the static analysis and the rewriting communities, in order to deal with approximation and complex data structures.

Below I give three major subtopics that I would like to address in the years to come, which concern the synergic exploitation of static analyses and compilation techniques. It will largely benefit from the results and experience already presented in the document.

Scalable static analyses for compilers

This research project is an ongoing research project in the more general context of the PROSPIEL Inria associate team led by Sylvain Collange, Inria Rennes, for the period 2015-2017.

The long term objective of this work is to enhance the capabilities of state-of-the-art compilers, so as for the optimisations phases to benefit from accurate information concerning the program and its properties. In the particular context of the project static analyses are used in combination with runtime checks to improve compiler optimisation opportunities [START_REF] Virouleau | Using data dependencies to improve task-based scheduling strategies on NUMA architectures[END_REF].

The means we choose is to start from the knowledge we recently gained during the Phd of Maroua Maalej and mostly described in Chapter 4. The contribution of this PhD thesis is double: the demonstration that current state-of-the art compiler optimisations do not reach their maximal power since the knowledge they get from the preceding analyses is not as precise as it could be ; and also three novel sparse thus scalable pointer analyses capable of capturing pointer arithmetic properties.

The particular memory analyses we designed all share the common point that they were designed to address the particular problem induced by pointer arithmetic in production compilers: all optimisations done in a given compiler operate on intermediate representations where the data structures (arrays, lists, structs) accesses are all expressed in terms of loads and stores from base pointers. Any clever optimisation (loop code motion, loop fusions, array compaction, . . . ) thus strongly relies on a precise handling of the semantics of all these operations. From that perspective, we only made a first step while designing our analyses: a huge amount of work remains to be done in order to redesign optimisations that are capable to be generic enough to benefit from any gain in the previous analyses steps.

In future work we plan to continue the work into the direction of scaling analyses for compilers. In particular, we have the objective to design specialised analyses but with an explicit notion of cost/precision compromise, in the spirit of the paper [START_REF] Oh | Selective contextsensitivity guided by impact pre-analysis[END_REF] that tries to formalise the cost/precision compromise of interprocedural analyses with respect to a "context sensitivity parameter". Another challenge is to find a generic way of adapting existing (relational) abstract domains in the Single Static Information framework so as to improve their scalability.

Collaborators on this topic Sylvain Collange (Inria Rennes), Fabrice Rastello (Inria Rhône Alpes), David Monniaux (Verimag), Fernando Pereira (University of Mineas Gerais, Brasil).

Complex data structures, from expressive analyses to efficient scheduling

This research project is the subject of a ANR JCJC (Young researcher funding) project that was accepted in July 2017. I am the principal investigator of this project.

The long term objective of this work is to give a general way to reason and manipulate programs with general control flow and complex data structures, so as to be able to extract parallelism information and schedule them properly.

The means we choose is to start with the current state of the polyhedral model (Section 3.2.1), which has proved its success in the aggressive compilation and code generation of computation-intensive kernels 2 . We want to enhance the framework theoretically and algorithmically in order to be able to deal with more general programs. As a first step, we first investigate general control flow and focus on specific data structures, such as lists and trees.

This research project takes inspiration from the termination work we described in Chapter 3, where the programs had complex control, but the complex data structures were abstracted away by a coarse abstraction. For instance, write operations were ignored, and read operations were assumed to return random values. Our array abstractions of Section 4.4 are a first step toward the understanding of more complex data structures, however we cannot rely on complex solvers for compilation.

In the context of the ANR submission we studied the relationship between termination and the parallel complexity of programs operating on abstract data types such as lists and trees. In the preliminary paper [START_REF] Alias | Estimation of Parallel Complexity with Rewriting Techniques[END_REF], we revisited the ideas that were at the origin of the SAS'10 paper ([ADFG10]) by replacing the termination algorithm for numerical programs by a termination algorithm from the rewriting community (termination of rewriting systems are powerful to deal with abstract data types). From a termination proof we are capable to infer the "parallel complexity" of the program under analysis, which gives an upper bound on the complexity of the program if it were executed on multiprocessors platforms.

In future work we plan to continue the work around this relationship, especially by designing abstractions that will scale enough to capture the behaviour of bigger size programs. These abstractions should also be precise enough to capture all the computation dependences in complex programs/data structures. We may draw inspiration of our work on array properties ( [MG16]). The challenge will also to be able to deal with the approximation induced by the abstractions, especially when we have to generate code, so as to avoid too many useless computations, or worse, optimisations which would cause the final optimised program to be incorrect.

Collaborators on this topic Christophe Alias (Inria Rhône Alpes), Carsten Fuhs (University of Birbeck, UK), Lionel Morel (Insa Lyon), David Monniaux (Verimag, Grenoble), Tomofumi Yuki (Inria Rennes).

Dataflow model: from semantics to efficient parallel compilation

This research project is part of a current Inria joint-team proposal at LIP.

The long term objective of this work is to propose a novel intermediate representation to compile to and from. The novel representation should be expressive enough to be able to deal with all kinds of parallelism, and simple enough to be able to reason on it and provide scalable analyses on it.

The means we choose is the study of the dataflow model for programs: the dataflow formalism expresses a computation on an infinite number of values, that can be viewed as successive values of a variable during time. A dataflow program is structured as a set of communicating processes that communicate values through communicating buffers. Examples of dataflow languages include the synchronous languages Lustre and Signal for which we already produced static analyses (Section 2.4), as well as SigmaC [START_REF] Aubry | Extended Cyclostatic Dataflow Program Compilation and Execution for an Integrated Manycore Processor. In Alchemy 2013 -Architecture, Languages, Compilation and Hardware support for Emerging ManYcore systems[END_REF]; the DPN representation [START_REF] Alias | Data-aware Process Networks[END_REF] (data-aware process network, in the context of hardware compilation) is an example of a dataflow intermediate representation for a parallelizing compiler.

The dataflow model, which expresses at the same time data parallelism and task parallelism, is in our opinion one of the best models for analysis, verification and synthesis of parallel systems. This model will be our favourite representation for our programs. Indeed, it shares the "equational" description of computation and data with the polyhedral model, and the static single assignment representation inside compilers.

We plan to work on various application domains, from algebra HPC kernels to more complex applications like software radio or deep learning applications where the main challenge is to be able to transfer big amount of data between computation units. The work on these various domains will be driven by the idea that exploring various topics is a way to converge on unifying representations and algorithms even for specific applications.

All these applications led to the same research goal: finding a way to integrate computations, data, scheduling, distribution in a common analysis and compilation framework. We will study each of these problems from the intermediate representation point of view, like in Section 5.2.2. Abstractions, partial evaluation, and other formal tools will be used in order to revisit the already plethoric literature on Kahn process network variants [START_REF] Aubry | Extended Cyclostatic Dataflow Program Compilation and Execution for an Integrated Manycore Processor. In Alchemy 2013 -Architecture, Languages, Compilation and Hardware support for Emerging ManYcore systems[END_REF][START_REF] Kahn | The semantics of simple language for parallel programming[END_REF] where static scheduling is very often the main purpose. In this research project, we specifically want to take into account the code of the tasks as well as there producer/consumer characteristics, in a general expressive framework from the program to the code generation.

Collaborators on this topic

1

  Introduction: from Program Verification to

Example 1 ( 1 k 2 k 3

 1123 Simple example for abstract interpretation). Consider the simple example of Figure 2.1. int x = 0; while ( true ) { x = x +1; if ( x >= 100) x = 0; } (a) Listing for the simple example k

Figure 2 . 2 -

 22 Figure 2.2 -The circular buffer example

Figure 2 .

 2 3(b) gives the disconnected SSA form graph where k 1 and k 2 have been split. The resulting formula is depicted below. For instance , the transition from k s 1 to k d 2 is encoded as (e 1 = (x 1 = 0) ∧ b s 1 ) and b d 2 = e 1 ∨ . . .. This kind of transformation is classic in model-checking.

  k

Example 4 (

 4 Bathtub example). The simple SIGNAL process shown in Listing 4 specifies the status of a bathtub[16]. It has no input signal (line 02), but has three output signals (line 03). process Bathtub = (? ! integer level ; boolean alarm , ghost_alarm ; ) (|(| level := zlevel + faucet -pump | zlevel := level$1 init 1 | faucet := zfaucet + (1 when zlevel <= 4) | zfaucet := faucet$1 init 0 | pump := zpump + (1 when zlevel >= 7) | zpump := pump$1 init 0 |) |(| overflow := level >= 9 | scarce := 0 >= level | alarm := scarce or overflow | ghost_alarm := ( true when scarce when overflow ) default false |) |) where integer zlevel , zfaucet , zpump , faucet , pump ; boolean overflow , scarce ; end ;

Example 5 .

 5 Let b = (x + y = 4) and (y < 10) be a Boolean expression. Its abstraction is φ(b) = x + y = 4 ∧ y < 10.

Example 4 (

 4 continuing from p. 18). Given the formula Φ Bathtub obtained previously, as the abstraction of the bathtub SIGNAL specification, the main properties of interest are the following11 : 1. pump and faucet have disjoint clocks: ¬( f aucet ∧ pump), 2. The water cannot overflow and be scarce at the same time: ¬ scar ce ∧ over f l ow ∧ scar ce ∧ over f l ow , 3. alarm and level have the same clock: al ar m ⇔ l evel .

  ; boolean alarm , ghost_alarm ; ) (|(| level := zlevel + faucet -pump ... | ghost_alarm :=( true when scarce when overflow ) default false |) |(| true when scarce when overflow ^= ^0 | faucet ^* pump ^= ^0 | alarm ^= level |) |) where 10 Globally Asynchronous Locally Synchronous 11 These properties cannot be verified by the current version of the SIGNAL compiler.integer zlevel , zfaucet , zpump , faucet , pump ; boolean overflow , scarce ; end ;

(

  | CLK_ghost_alarm := ^ghost_alarm | CLK_ghost_alarm ^= ghost_alarm | (| ghost_alarm := not CLK_ghost_alarm |) |) ;%^0 ^= level ^= alarm ^= zlevel ^= zfaucet ^= zpump *** WARNING : null clock signals %

Figure 2 . 6 -

 26 Figure 2.6 -A comparison between four different types of static analyses. Only a few relations are shown for Octagons.

Figure 2 . 7 -

 27 Figure 2.7 -Running example: steps of the analysis within the SymBoxes domain, max = max(0, N -1).

Figure 2 . 8 -

 28 Figure 2.8 -Constraints for the symbolic range analysis.

Figure 2 . 9 -

 29 Figure 2.9 -Runtime comparison of three non-relational analysis. Timings are in seconds. S: symbolic range analysis. I: integer overflow elimination. RA: Rodrigues et al.'s range analysis [93]. Pen-

Figure 3 . 1 -

 31 Figure 3.1 -Illustrating example of [ADFG10]. True guards and ε actions are ommited.

Figure 3 . 2 -

 32 Figure 3.2 -Polyhedral scheduling: an example. The Smith-Waterman sequence alignment algorithm and its dependencies. Each point (i , j ) represents an execution of the block S, denoted by 〈S, i , j 〉.

6 :

 6 T ← TThe transitions have level i 7: end while; 8: d = i ; return true; There is a d -dimensional ranking • The ρ function should decrease on all transitions of T , and strictly decrease on a maximal subset of T .

Figure 3 . 3 -

 33 Figure 3.3 -Counter-example guided ranking function generation

  be a set of generators of the convex hull of P I ,τ and the set of vectors Constraints(I) = {a i |1 ≤ i ≤ m} (constraints of I ). Then :

Algorithm 5

 5 Incremental Monodimensional Termination Input: A control point with τ its set of transitions, I invariant Output: Yes+ρ/Abort 1: C := , ρ(x) := 0, thus λ = 0. Initialisation 2: while true do 3:

7 :

 7 Call LP (C , Constraints(I))compute a new (candidate) ranking function 8: end while;

Figure 3 . 4 -

 34 Figure 3.4 -RANK tool-chain. DK is "I do not know". Too much variables indicates that we generated a LP instance that is too big for PIP

Figure 3 . 5 -

 35 Figure 3.5 -TERMITE tool-chain

8 : 3

 83 r es ← Rank(cont ext , st at ement ) launch of the whole toolchain depicted in Figure

Figure 3 . 8 -

 38 Figure 3.8 -Life cycle of a JavaScript program in the Mozilla runtime: We can perform trip count prediction at two different execution stages.

Figure 3 . 9 -

 39 Figure 3.9 -Speedup due to trip count predictor for benchmarks distributed with Firefox.

-Figure 4 . 1 -

 41 Figure 4.1 -The syntax of our language of pointers.

Figure 4 .

 4 2 clarifies the semantic of W (p). The first instruction of Figure 4.2 allocates n words in memory and assigns the newly created region to pointer v 1 . Thus, given a stack S, if b 1 = S(v 1 ) is the value of v 1 , then any address between b 1 + 0 and b 2 + n -1 is valid. The second instruction increments v 1 and calls the new address v 2 . Similarly, if b 2 = S(v 2 ), then the address b 2 -1 is valid and the address b 2 -n -2 is also valid.

Figure 4 . 3 -

 43 Figure 4.3 -Constraint generation for the symbolic region analysis. R(x) denotes the (symbolic) range of x obtained from Section 2.5

  (a) Our running example (b) Useless bound checks elimination

Figure 4 . 4 -

 44 Figure 4.4 -Array bound check elimination. Highlighted code is useless.

Figure 4 . 5 -

 45 Figure 4.5 -Overview of our pipeline of static analyses.

Figure 4 . 6 -

 46 Figure 4.6 -Time taken by static analyses. Split: live range splitting and Overflow instrumentation.Symb.RA: Symbolic range analysis. Region: Region analysis. Less-than: Less-than test.

Figure 4 . 7 -

 47 Figure 4.7 -Impact of our analyses: run time of program after bound check elimination, compared to run time of program with all the bound checks. The shorter the bar, the faster the program. Pentagon: Logozzo et al [79]. T: Tainted flow analysis. I: Integer overflow analysis. S: Symbolic range analysis. R: Region analysis. Average speedup: Pentagons = 9.1%, S+R+I = 15.8%, T+S+R+I=17.0%, Unsafe = 26.4%.

Example 11 (

 11 Running example for range-based pointer disambiguation).

Figure 4 .

 4 8 shows a pattern typically found in distributed systems implemented in C. Messages are represented as arrays of bytes.

Figure 4 . 8 -

 48 Figure 4.8 -Example of program that builds up messages as sequences of serialised bytes. We are interested in disambiguating the locations accessed at lines 4 and 8.

Figure 4 . 9 -

 49 Figure 4.9 -Behaviour of the prepare procedure.

Figure 4 .

 4 Figure 4.11 -CFG of the motivating example of Figure 4.8

Figure 4 .

 4 11 shows the control flow graph of the program seen in

Figure 4 . 8 .

 48 Figure 4.8. The two allocations at lines 14 and 15 are associated respectively with loc 0 and loc 1 .

Figure 4 . 12 -

 412 Figure 4.12 -The concrete semantics of GR(p) = {loc 1 + [3, 5], loc 3 + [3, 8]}. Dark grey cells denote possible (concrete) values of p.

Definition 10 .

 10 Given GR(p) and GR(p ) with GR(p) GR(p ), we define the widening operator: GR(p)∇GR(p ) = (p 0 ∇p 0 , . . . , p n-1 ∇p n-1 ), where ∇ denotes the widening on SymBoxes , extended with ⊥∇⊥ = ⊥ and ⊥∇[l , u] = [l , u].

Figure 4 . 13 -

 413 Figure 4.13 -Constraint generation for GR with GR(p) = (p 0 , . . . , p n-1 ) given p in the right hand side of rules

Figure 4 . 14 -Example 13 (

 41413 Figure 4.14 -Splitting strategy for the less-than analysis.

Figure 4 .

 4 [START_REF] Amir | Program termination analysis in polynomial time[END_REF] illustrates the splitting strategy on a toy example.Constraint generation, solving Once we have a suitable program representation, we use the rules inFigure 4.16 to generate constraints. These constraints determine the less-than set of variables. Constraint generation is O(|V |), where V is the set of variables in the target program.

Figure 4 . 15 -

 415 Figure 4.15 -Illustration of the splitting strategy on a toy example

Figure 4 . 16 -

 416 Figure 4.16 -Constraint generation rules. n is a variable such that R(n) = [l , u], l > 0.

Figure 4 . 17 -

 417 Figure 4.17 -Runtime of CGO'16 analysis for the 50 largest benchmarks in the LLVM test suite. Each point on the X-axis represents a different benchmark. Benchmarks are ordered by size. This experiment took less than 10 seconds.

Figure 4 . 18 -

 418 Figure 4.18 -Runtime of our CGO'16 (classic scale) and CGO'17 (log scale) analyses. The experiments were launched on 20 middle-sized benchmarks from LLVM Multisources. This experiment took less than 20 seconds for CGO16 and CGO17

Figure 4 . 19 -

 419 Figure 4.19 -Precision of the offset range analysis compared and combined to other LLVM analyses

Figure 4

 4 Figure 4.20 -Effectiveness of our alias analysis (LT), when compared to LLVM's basic alias analysis on the 100 largest benchmarks in the LLVM test suite. Each point in the X-axis represents one benchmark. The Y-axis represents total number of queries (one query per pair of pointers), and number of queries in which each algorithm got a "no-alias" response (the higher the better).

Figure 4 . 21 -

 421 Figure 4.21 -How two different alias analysis (LT and CF) increase the capacity of LLVM's basic alias analysis (BA) to disambiguate pointers. The Y-axis shows the percentage of no-alias responses. The higher the bar, the better.

Figure 4 . 22 -

 422 Figure 4.22 -Precision of dependence graph.All benchmarks with the same number of memory locations (X-axis) are considered together. For each set, we depict the repartition of the number of nodes of the generated Program Dependence Graphs, with Basic Alias (in blue), and Basic Alias combined with LT (in red). The more memory nodes the PDG contains, the more precise it is.

1 :

 1 int * p = malloc (2*N*sizeof(int)) 2: int * p 1 , * p 2 , * a 3: * p = 8; * a = 10 4: p 1 = p + N 5: p 2 = p + 2 × N 6: while p 2 > p 1 do 7: * a = * p 8: * p 2

Figure 4 .

 4 Figure 4.23 -LICM hoisting load optimisation.

Figure 4 . 26 -

 426 Figure 4.26 -The array fill example The flat encoding into Horn clauses assigns a predicate (set of states) to each of the control nodes (Fig. 4.26b), and turns each transition into a Horn rule with variables ranging in Arr (A, B ), the type of

  PMB+16] Vitor Paisante, Maroua Maalej, Leonardo Barbosa, Laure Gonnord, and Fernando Magno Quintao Pereira. Symbolic Range Analysis of Pointers. In International Symposium on Code Generation and Optimization, pages 791-809, Barcelon, Spain, March 2016. Selection rate 23% (25/108). [SMO+14] Henrique Nazaré Willer Santos, Izabella Maffra, Leonardo Oliveira, Fernando Pereira, and Laure Gonnord. Validation of Memory Accesses Through Symbolic Analyses. In Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages And Applications (OOPSLA'14), Portland, Oregon, United States, October 2014.

	Selection rate 27% (52/186)

Paul Feautrier, Abdoulaye Gamatié, and Laure Gonnord. Enhancing the Compilation of Synchronous Dataflow Programs with a Combined Numerical-Boolean Abstraction. CSI Journal of Computing, 1(4):8:86-8:99, 2012. Unknown impact factor.

[

  [START_REF] Bagnara | The Parma Polyhedra Library[END_REF] paper[MG11]. The method is based on the study of the two following examples, where classic abstract interpretation with widening and narrowing fail to compute precise invariants. Here again, the abstract domain we choose is the interval abstract domain.

Example 2 (Motivating example 1). Consider Figure 2.2 that depicts a simplification of a fragment of an actual industrial reactive program: indexing of a circular buffer used only at certain iterations of the main loop of the program, chosen non-deterministically. Its representation with an affine automaton is depicted in the right of the figure.

  x 1 , ite(e 5 , x 4 , ite(e 4 , x 3 , x 2 ))) Figure2.3 -SSA CFG and its disconnected version for the motivating example, and the corresponding SMT formula (ρ). ite(b, e 1 , e 2 ) is "if b then the value of e 1 else the value of e 2 ". To each node k x corresponds a Boolean b x and an optional choice variable c x ; to each edge, a Boolean e y .In order to find a path from program point k 1 ∈ K R , with variable state x 1 , to program point k 2 ∈ K R , with variable state x 2 , we simply conjoin ρ with the formulas x 1 ∈ X k 1 and x 2 ∉ X k 2 , with x 1 , x 2 , expressed in terms of the SSA variables. For instance, if X k 1 and X k 2 are convex polyhedra defined by systems of linear inequalities, one simply writes these inequalities using the names of the SSAvariables at program points k 1 and k 2 .

  ) t ∈N , called signals, implicitly indexed by discrete time, and denoted as x. For instance, a signal can be either of Boolean or integer or real types. At any logical instant t ∈ N, a signal may be present, at which point it holds a value; or absent and denoted by ⊥ in the semantic notation. There is a particular type of signal called event. A signal of this type always holds the value true when it is present. The set of instants at which a signal x is present is referred to as its clock, noted ^x. A process is a system of equations over signals, specifying relations between values and clocks of the signals. A program is a process. where y, x are signals and c is an initialisation constant. It imposes i) x and y to be synchronous, i.e. ^y = ^x, while ii) y must hold the value carried by x on its previous occurrence. • Under-sampling: y:= x when b where y, x are signals and b is of Boolean type. This construct imposes (i) y to be present only when x is present and b holds the value true while (ii) y holds the value of x at those logical instants. Let us denote by [b] (resp. [¬b]) denotes the set of instants where b is true (resp. false). Then i) rephrases itself into ^y

						5
	SIGNAL Program	Pre-Analyzer Interval 1	4	Formulas of Proven Identification	SIGNAL Compiler	SIGNAL Program
		2	Abstraction & Property Definition	3	Solver SMT	Code C, C++, Java
		Figure 2.5 -An overview of our approach: steps and tools.
	2.4.1 Preliminaries: the SIGNAL language
	SIGNAL [54, 78] is a data-flow relational language that handles unbounded series of typed values
	(x t Primitive constructs SIGNAL relies on six primitive constructs: the core language. The syntax of the
	constructs is given below, with some informal explanations. Their formal semantics can be found in
	the paper.
	• Instantaneous relations: y:= R(x1,...,xn) where y, x1, . . . xn are signals and R is a point-
	wise n-ary relation extended canonically to signals. This construct imposes y, x1, . . . xn i) to
	be simultaneously present, i.e. ^y = ^x1 = . . . = ^xn (i.e. synchronous signals), and ii) to hold
	values satisfying y = R(x1,...,xn) whenever they occur.
	• Delay: y:= x $ 1 init c

  Obviously, the existence of a ranking function implies program termination for any valuation v at the initial control point k i ni t . A well-known property is that an integer interpreted automaton terminates for any initial valuation if and only if it has a ranking function (not necessarily expressible in our (N k , k ) setting). Furthermore, if it terminates and has bounded non-determinism2 , there is a one-dimensional ranking function, which is not necessarily affine.

			start
	y = 0; x = m;	lbl 4
	while(x>=0 && y>=0){
		if(indet()){
		while(y <= m && indet())
		y++;	lbl 5
		x--;
		}
	}	y--;	stop	lbl 6
				lbl 10
	Example 7 (Motivating example ). An example program is given in Fig. 3.1, with its corresponding
	automaton. The control points are labelled for convenience, and transitions are depicted with arrows indexed by g a (g is omitted when g = true). State names are assigned arbitrarily by our parser. The C code features two nested loops, which do not fit into the structured programming model, since
	the inner counter, y, is modified in the outer loop. The indet function abstracts non-determinism or
	an intractable test.

where the order k is the standard lexicographic order on integer vectors. The outcome of non-determinism is that, in the corresponding automaton, both transitions out of state l bl 5 have a true guard. The right of Fig.

3

.1 successively gives, assuming m > 0, the invariants as found

  Example 8 (Illustration for the polyhedral model framework ). Figure3.2 is a loop kernel computing the Smith-Waterman optimal sequence alignment algorithm5 . The polyhedral model provide us tools to automatically compute the dependencies that are depicted on the right: each point represents an execution of the block S computing H[i][j] for a given i and j in 0, N . Such an operation is written 〈S, i , j 〉. The arrows represent the dependencies towards a given 〈S, i , j 〉. For instance the diagonal arrow means that H[i][j] requires the value of H[i-1][j-1] to be computed.

	for ( i =0; i <= N ; i ++)
	for ( j =0; j <= N ; j ++)
	// Block S
	{
	m1 [ i ][ j ] = Integer . MIN_VALUE ;
	for ( k =1; k <=

Table 3 .

 3 1 -Experimental results SAS10 for RANK (WTC benchmark)

	Name	Ref Vars States Trans dim ρ Time (s)	WCCC
	easy1	[29] 3	4	5	1	0.2	43
	easy2 ackermann [15] 2 [29] 3 terminate [33] 3 gcd [25] 2 rsd ♣ 3 nd_loop 2 ♣ wcet2 ♣ 2 relation1 2 ♣ ndecr ♣ 2 perfect [27] 4 cousot16 [38] 2	3 7 1 5 3 4 3 4 4 5 3	3 7 1 1 4 6 5 4 4 12 4	1 1 1 1 1 1 1 1 1 3 1	0.07 0.07 0.08 0.2 0.2 0.05 0.15 0.14 0.08 0.35 0.05	z 0 + 3 4m 0 + 5 i 0 + j 0 + k 0 + 102 x 0 + y 0 + 2 r 2 o 2 + 5r 0 2 + 5 22 55 -12i 0 4 i 0 + 2 2 + 3x 0 2 x 2 0 + 2 106
	random2d [29] 5 random1d [29] 3 wise ♣ 2 wcet1 ♣ 3 complex [58] 2 nestedLoop [58] 6 exmini ♣ 4 aaron2 [29] 3 while2 ♣ 3 cousot9 [38] 3 ax ♣ 4 loops [89] 3 counterex1 ♣ 4 determinant [27] 4 maccarthy91 [34] 4 speedpldi2 [58] 4 speedpldi3 [58] 4 speedpldi4 [58] 3 speedFails4 [58] 5	10 4 6 6 4 5 3 6 3 4 3 4 5 6 5 4 6 6 4	21 6 10 8 11 12 6 10 4 5 6 5 13 7 18 9 11 11 10	1 2 2 2 2 3 2 2 2 2 3 2 3 4 2 2 3 2 2	1.1 0.1 0.11 0.25 0.28 1.3 0.1 0.2 0.1 0.2 0.16 0.15 1.1 0.15 1.2 1.0 1.3 1.1 1.1	6N 0 + 3 max + 3 1 + x 0 -y 0 n 0 + 2 1560 -9b 0 -45a 0 n 0 m 0 + 2N 0 + n 0 + 3 104 + k 0 -j 0 -x 0 2(x 0 -y 0 ) + 5 3 + 2N + N 2 3 + 7/2N + 5/2N 2 n 2 0 -n 0 + 2 N 2 -N + 5 x 0 + 2 N 3 3 + N 2 2 + N 6 + 3 13773/11 -1363/110x 2n 0 -m 0 + 3 n 0 m 0 + n 0 + 4 2n 0 -2m 0 + 5 n 0 -x 0 + 4

Table 3 .

 3 2 -Experimental results SAS10 for RANK (Sorting programs)

	Name realselect insertsort sipmabubble [29] 4 Ref Vars States Trans dim ρ Time (s) ♣ 7 5 10 3 0.4 ♣ 3 6 7 2 0.22 10 17 3 0.33 realbubble ♣ 6 5 11 3 0.4 realshellsort ♣ 8 8 13 4 1.1 realheapsort ♣ 10 11 31 3 2.8	WCCC + 3N 2 + 3N 2 N 2 + 2N + 3 N 2 2 + 1 N 2 2 + 1 N 2 + 2 N 3 6 N -6 4N 2 -11N + 9

Table 3 .

 3 3 -PLDI15: Comparison of TERMITE and some of the state-of-the-art Termination tools. For each benchmark suite, the total number of benchmarks and the number of benchmarks proved to terminate by each tool are given. Timings, in milliseconds, exclude the front-end for TERMITE and LOOPUS and the invariant generator for TERMITE. (l , c) are the average number of lines and columns of the linear programming instances.

	Suite	# benchmarks	# success	Termite time	(l , c)	Loopus # success	time	AProVE # success	time	Ultimate # success time
	PolyBench Sorts TermComp WTC	30 6 129 58	22 5 119 46	117 126 12 64	(9, 3) (15, 4) (2, 1) (5, 2)	30 3 78 33	37 67 15 48	0 0 111 36	2100 12230 9757 11740	0 0 85 40	2750 2980 5863 4536

LoCB LoCA Regressions WTC(s) SToP(s)

	WTC	50	28	21	3	0.92	2.45
	Sorting	6	55	39	0	3.66	3.52
	the source-to-source compiler infrastructure Rose ([90]) : functions for parsing, constructing flow
	graphs, searching in the code structure, pretty printing and instrumenting C codes.

Table 3 .

 3 [START_REF] Alias | Data-aware Process Networks[END_REF] give an extract of the experiments on we made with our tool STOP (the entire benchmark is available on http://compsys-tools.ens-lyon.fr/stop). experiments were done on a Dual Core 2Ghz. As we expected, the execution times on middlesized examples are much larger with STOP than WTC, mainly because of the cost of slicing and producing intermediate files. These results could be enhanced by hand by calling WTC on larger subprograms (some nested loops can be handled with a unique call to WTC). For sorting functions,

	The

  ∞[

	SunSpider 1.0 V8 v6 Kraken 1.1	0.0% 0.6% 0.8%	0.0% 1.7% 0.0%	0.0% 0.0% 3.2%	89.2% 94.8% 83.9%	2.0% 2.3% 1.6%	4.7% 0.0% 2.4%	4.1% 0.6% 8.1%
		SunSpider 1.0		SunSpider 1.0		Kraken 1.1
		3d-cube	--1%	math-cordic	2%	ai-astar	1%
		3d-morph	--1%	math-partial-sums	--1%	audio-beat-detect	0%
		3d-raytrace	1%	math-spectral-norm	--1%	audio-dft	--4%
		access-binary-trees	0%	regexp-dna	0%	audio-fft	0%
		access-fannkuch	2%	string-base64	24%	audio-oscillator	1%
		access-nbody	--1%	string-fasta	--7%	img-gaussian-blur	--3%
		access-nsieve	2%	string-tagcloud	1%	imaging-darkroom	--3%
		bitops-3bit-in-byte	0%	string-unpack-code	0%	imaging-desaturate	0%
		bitops-bits-in-byte	1%	string-validate-input	--5%	json-parse-financial	1%
		bitops-bitwise-and	3%			json-stringify-tinder	1%
		bitops-nsieve-bits	3%	V8 version 6.0		crypto-aes	6%
		ctrlflow-recursive	--1%	crypto	0%	crypto-ccm	2%
		crypto-aes	0%	deltablue	2%	crypto-pbkdf2	7%
		crypto-md5	3%	earley-boyer	0%	crypto-sha256-itrv	6%
		crypto-sha1	10%	raytrace	0%
		date-format-tofte	2%	regexp	3%
		date-format-xparb	2%	richards	--1%
				splay	1%

  and ELDAR-ICA[START_REF] Rümmer | Disjunctive interpolants for Horn-clause verification[END_REF].[START_REF] Aubry | Extended Cyclostatic Dataflow Program Compilation and Execution for an Integrated Manycore Processor. In Alchemy 2013 -Architecture, Languages, Compilation and Hardware support for Emerging ManYcore systems[END_REF] Since program verification is undecidable, such tools, in general, may fail to terminate, or may return "unknown." Example 15 (Motivating example). Consider the program of Figure4.26 where a given array of unknown size is filled with the same constant value 42. We would like to prove that this program truly fills array a[] with value 42.

		start	init
	void array_fill1 ( int n , int a[ n ]) {	n > 0
		for ( int i =0; i < n; i ++)
		a[ i ]=42;	loop
	}	/* assert ∀0 ≤ k < n, a[k] = 42 */
		(a) Listing for array fill	end

if Example 15

  Algorithm 9 describes how to use it to prove a given safety property Φ of a program. Let us recall that the property to prove is also abstracted according to 4.27. Proving array properties on a CFG Input: CFG + Φ a property to prove Output: Yes/I do not know 1: To each control point p , with vector of scalar variables x , associate a predicate I (x , k, a k ) 2: For each transition of the program, generate Horn rules according to Figure 4.27. (continuing from p. 69). Let us now apply Algorithm 9 where the predicates I k are simply denoted by the label of the control point i .

	Algorithm 9 6: return Yes
	7: else
	8:	return I do not know
	9: end

3: Also Generate Horn queries from desired properties. 4: Call a solver. 5: if it answers SAT then

Table 4 .

 4 1 -Comparison on the array benchmarks of[START_REF] Dillig | Fluid updates: Beyond strong vs. weak updates[END_REF]. (Average) timing are in seconds, CPU time. Abstraction with N = 1. "sat" means the property was proved, "unsat" that it could not be proved. "hints" means that some invariants had to be manually supplied to the solver (e.g. even/odd conditions). A star means that we used another version of the solver. Timeout was 5 mn unless otherwise noted. The machine has 32 i3-3110M cores, 64 GiB RAM, C/C++ solvers were compiled with gcc 4.8.4, the JVM is OpenJDK 1.7.0-85.

	Benchmark	Z3/PDR Res Time	Z3/Spacer Res Time	Eldarica Res Time	Comment
		Correct problems, "sat" expected
	append	sat	2.11	sat	0.85	sat	22.61
	copy	sat	4.66	sat	0.44	timeout(300s)
	find	sat	0.20	sat	0.14	sat	12.93
	findnonnull	sat	0.50	sat	0.34	sat	12.04
	initcte	sat	0.16	sat	0.26	sat	13.28
	init2i	sat	0.31	sat	0.16	sat	14.67
	partialcopy	sat	1.88	sat	0.34	timeout(300s)
	reverse	sat	40.70	sat	2.19	timeout(300s)
	strcpy	sat	0.92	sat	0.37	sat*	66.69
	strlen	sat	0.24	sat	0.22	sat	36.69
	swapncopy	sat	71.16	timeout(300s)	timeout(300s)
	memcpy	sat	3.54	sat	0.39	timeout(300s)
	initeven	sat	1.32	sat	0.71	timeout(300s)	"hints"
	mergeinterleave	sat	39.49	sat	4.61	timeout	322.39	"hints"
		Incorrect problems, "unsat" expected
	copyodd_buggy	unsat	0.08	unsat	0.04	unsat	7.42
	initeven_buggy	unsat	0.06	unsat	0.06	unsat	6.28
	reverse_buggy	unsat	1.88	unsat	1.28	unsat	58.96
	swapncopy_buggy	unsat	3.13	unsat	0.74	unsat	27.54
	mergeinterleave_buggy	unsat	1.16	unsat	0.56	unsat	31.22

Table 4 .

 4 2 -Other array-manipulating programs, including various sorting algorithms. a star means that we used another version of the solver, R1 means random_seed=1. The striked out result is likely a bug in Z3; the alternative is a bug in Spacer, since the same system cannot be satisfiable and unsatisfiable at the same time.

	Benchmark	N	Z3/PDR Res Time	Z3/Spacer Res Time	Eldarica Res Time	Comment
	bin_search_check	1	sat	0.71	sat	0.34	Crash
	find_mini_check	1	sat	4.22	sat	0.82	sat	110.58
	revrefill1D_check_buggy	1	unsat	0.03	unsat	0.07	unsat	9.21
	array_init_2D	1	sat	0.46	sat	0.22	sat	12.76
	array_sort_2D	1	sat	0.78	sat	0.30	sat	26.68
	selection_sort (sortedness)	2	sat*	99.04	timeout(300s)	timeout(300s)
	selection_sort (sortedness)	2	unsat	83	sat	48	timeout	334	manual translation
	selection_sort (permutation)	1	timeout	600	sat	9.24	timeout	336	manual translation
	bubble_sort_simplified	2	sat	5.98	sat	2.77	sat	158.70
	insertion_sort	2	sat(R1)	53.83	timeout(300s)	timeout(300s)

  Christophe Alias (Inria Rhône Alpes), Lionel Morel (Insa Lyon), Matthieu Moy (Verimag, Grenoble). W (p) Valid offsets from base p. 51 SymRegion Symbolic Region abstract domain. 51 L oc Set of all allocation sites of the program. 58 MemLocs Memory Locations abstract domain. 58 GR Global Range Analysis (CGO'16). 58 LT Less Than Analysis (CGO'17). 61 CFC Constrained Horn Clause. 69 I Abstract invariant predicate at control point (SAS'16). 69

http://sunnyday.mit.edu/accidents/Ariane5accidentreport.html

https://www.absint.com/astree/index.htm

https://en.wikipedia.org/wiki/List_of_tools_for_static_code_analysis

https://www.grammatech.com/products/codesonar

http://fbinfer.com/

http://compcert.inria.fr/

http://verasco.imag.fr/wiki/Main_Page HDR Laure Gonnord

While waiting an hour for a safety critical program to be analysed is accepted, in general it is not the case for a one-hour lasting compilation for a general purpose software package

Many presentations of abstract interpretation distinguish the abstract element x ∈ D from the set of states γ(x ) it represents. We opted not to, for the sake of brevity.

An inductive invariant is a formula which is true at the initial state(s) of the transition system, and which is stable: if the valuation of variables satisfy this formula at a given control point, then after each possible transition, the new valuation also satisfies this formula.

On this example, it is possible to compute the [0, 99] invariant by so called "widening up-to" [60, Sec. 3.2], or with "thresholds"[START_REF] Blanchet | A static analyzer for large safety-critical software[END_REF]: essentially, the analyser notices syntactically the comparison x <

and concludes that 99 is a "good value" for x, so instead of widening directly to +∞, it first tries 99. This method only works if the interesting value is a syntactic constant.

A node dominates a node n if every path from the entry node to n must go through .

We design a better splitting strategy in the paper, that we do not recall here for the sake of brevity.

Bodik et al. [21] would name similar instructions π-functions

GinaC is available at http://www.ginac.de/

The Frama-C tool, developed at the CEA, is capable of checking such Hoare triples http://frama-c.com/ HDR Laure Gonnord

Each non deterministic choice lies in a finite set.HDR Laure Gonnord

http://laure.gonnord.org/pro/aspic/aspic.html

In the context of polyhedral optimisation, a statement A depends on another statement B if computes a result which will be later used by A.

See https://en.wikipedia.org/wiki/Smith-Waterman_algorithm. We consider two sequences of the same length N .

This restriction is only for the sake of readability. The two papers contain algorithms to deal with any number of control points.

t can be an integer or a rational, for the rest of the section, we will suppose that it is an integer. HDR Laure Gonnord

https://github.com/Z3Prover

These examples have been integrated in the SVCOMP benchmark https://sv-comp.sosy-lab.org/2017/

http://forsyte.at/software/loopus/

http://aprove.informatik.rwth-aachen.de/

http://ultimate.informatik.uni-freiburg.de/BuchiAutomizer/

http://laure.gonnord.org/pro/aspic/aspic.html

http://www.cs.ucla.edu/~pouchet/software/polybench/

http://compsys-tools.ens-lyon.fr/wtc/index.html

http://termination-portal.org/wiki/Termination_Competition

Obvious adaptations are necessary to handle ≤ and ≥.

Let us point out the fact that, unlike the proposition of[START_REF] Miné | Backward under-approximations in numeric abstract domains to automatically infer sufficient program conditions[END_REF], we directly widen to when one of the bounds is not stable. HDR Laure Gonnord

A nice comparison of memory models used for analysing variants of C and Java can be found in the paper[START_REF] Sotin | Concrete Memory Models for Shape Analysis[END_REF]

The other motivating example of the[MPR+17] paper was actually not solved with the published analysis, for expressivity reasons due to the LLVM representation. We found a workaround which was one of the main motivation of the algorithms described in the journal paper[MPMQPG17].

See http://ctuning.org/ae/cgo2016.html and http://ctuning.org/ae/cgo2017.html

it is worth to mention that the LLVM 3.7 version contains other alias analyses, whose results we shall not use, because they have been able to resolve a very low number of queries in our experiments. Most probably there will be an increasing number of aliases analyses implemented in LLVM in a soon future, making these lines obsolete.

The complete methodology can be found in the[MPR+17] paper.HDR Laure Gonnord

https://github.com/Z3Prover hash 7f6ef0b6c0813f2e9e8f993d45722c0e5b99e152; due to various problems we preferred not to use results from later versions.

[START_REF] Aubry | Extended Cyclostatic Dataflow Program Compilation and Execution for an Integrated Manycore Processor. In Alchemy 2013 -Architecture, Languages, Compilation and Hardware support for Emerging ManYcore systems[END_REF] https://bitbucket.org/spacer/code hash

7e1f9af01b796750d9097b331bb66b752ea0ee3c 9 https://github.com/uuverifiers/eldarica/releases/tag/v1.1-rc

also denoted by I ((i , n), (k, a k )) for sake of readability.

http://smtlib.cs.uiowa.edu/

We suspect that different choices in SAT lead to different proofs of unsatisfiability, thus different interpolants and different refinements in the PDR algorithm.

http://compilfr.ens-lyon.fr/

http://polyhedral.info/

Acknowledgments

First of all, I am very grateful to Prof. Paul Kelly from Imperial College London (UK), Prof. Antoine Miné from Pierre et Marie Curie University (France) and Prof. A. Podelski from Freiburg university (Germany) for having kindly accepted to serve as reviewers on my Habilitation defense committee, and for the reports they wrote on my work.

I would also like to warmy thank Prof. Isabelle Guerin-Lassous from University of Lyon (France), Dr Albert Cohen from Inria Paris (France) and Prof Sebastien Hack from Saarland University (Germany) for their kind participation to my Habilitation defense committee as examiners, and for the interesting discussions we had during the defense.

CHAPTER 3. STATIC TERMINATION ANALYSIS i n t main ( ) { i n t n , i , j , k , l , t , h ,m, p , q , r ; A summary-based algorithm for termination Algorithm 7 depicts the modular algorithm we use to incrementally prove termination of a given piece of code.. For the sake of readability we only provide the algorithm for while loops. The rest is straightforward. This algorithm strongly depends on the notion of summary, that we recall here:

Definition 7 (Summary). Let C be a code and R C (x 0 , y 0 , . . . , x, y) be an over-approximation of the re- The figure displays a C implementation of the well known partition algorithm. We know that memory positions v[i] and v[j] can never alias within the same loop iteration, since i and j are never equal.

However, traditional points-to analyses cannot prove this fact.

Typical implementations of alias analyses, built on top of the work of Andersen [START_REF] Ole | Program Analysis and Specialization for the C Programming Language[END_REF] or Steensgaard [START_REF] Steensgaard | Points-to analysis in almost linear time[END_REF], can distinguish pointers that dereference different memory blocks; however, they do not say much about references ranging on the same array. In this work, we propose two new analyses based on the computation of offset range information (CGO'16, Section 4.3.1) or "less than" information (CGO'17, Section 4.3.2). These two analyses share the common "Single information" strategy.

Pointer disambiguation as queries For our pointer analyses to be useful for client analyses such as tool fusion, code motion, . . . , the analyses should be split into:

• An analysis phase which computes abstract values for all variables of the program. We want this analysis phase to be scalable and precise.

• A query interface for other compiler phases. This interface should be simple: given a pair of pointers, it should answer "they do not alias" or "they may alias." We want this query to be as fast as possible, so that the client analyses can make intensive calls to it.

CGO 16 : Symbolic range of pointers

The contribution of this work is the (scalable) combination of pointer analysis with range analysis on the symbolic interval lattice SymBoxes (described in Section 2.5) in the form of a constraint systems whose solution is a set of abstract states of the form loc i + R i j for each pointer p j . We use two different strategies to disambiguate pointers: the global and the local test. Our global pointer analysis goes over the entire code of the program, associating variables that have the pointer type with elements of an abstract domain that we will define soon. The local analysis, on the other hand, works only for small regions of the program text.

A Main Symbols and Acronyms

x Vector of program's variables. 7