Laure Gonnord
email: laure.gonnord@ens-lyon.fr

David Monniaux
email: david.monniaux@imag.fr

Gabriel Radanne
email: gabriel.radanne@pps.univ-paris-diderot.fr

Synthesis of ranking functions using extremal counterexamples

Introduction

Program termination can be shown by providing a ranking function: a function from program states to a well-founded ordering, decreasing along any transition in the program.

In formal methods by assisted proofs (e.g. B method, Frama-C) the user typically has to provide a ranking function for each loop; automation may relieve that burden -but that is not all! In compilation, certain optimizations, such as lazy code motion, need to ensure that certain fragments of code terminate to be correct [START_REF] Tristan | Verified validation of lazy code motion[END_REF]; yet termination analysis is often considered too inefficient to be integrated into a compiler 1 -we show it needs not be. Also, from a ranking function and an invariant one may compute a bound (constant or parametric) on the number of iterations, which is necessary for worst-case execution time (WCET) 2 or for high-level synthesis ("C-to-silicon"). These applications need a fully automated, efficient algorithm providing the ranking function in most cases.

Because finding a ranking function is equivalent to proving termination, which is undecidable, automated approaches are incomplete. They typically search for ranking functions in restricted classes: if a ranking function is found, then the program necessarily terminates, but it may still terminate even though no function is found within the class. One popular class is linear ranking functions: such a function ρ maps the vector x ∈ Z n of program variables to an integer linear combination i α i x i such that ρ(x ) < ρ(x) for any possible program step x → x , and such that ρ(x) ≥ 0 for any reachable program state (remark that this entails proving an auxiliary invariant property). Furthermore, the α i may be allowed to depend on the program point k, thus the unknowns are α i,k : the decreasing condition becomes i α i,k x i < i α i,k x i for any transition (k, x) → (k , x ).

Various methods for the automated synthesis of such functions have been proposed [START_REF] Podelski | A complete method for the synthesis of linear ranking functions[END_REF]; they build a constraint system in the unknowns α i,k and solve it. This class is extended to lexicographic linear ranking functions: instead of a single function ρ(x), one uses a tuple of them ρ 1 (x), . . . , ρ m (x) , which is shown to be strictly decreasing with respect to lexicographic ordering. Again, the function ρ can be allowed to depend on the program point, and complete automated synthesis methods exist for this class [START_REF] Alias | Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs[END_REF], Ben-Amram and Genaim [2014].

A common weakness of many existing approaches is the need to solve for linear coefficients at all basic blocks, which leads to scalability and precision issues.

First, if the program has K basic blocks, n integer variables and one searches for a m-dimensional ranking function, then the number of unknowns in the constraint system is K.m.n, which might be too big [START_REF] Alias | Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs[END_REF]. Thus, it is desirable to limit the set of points to consider to heads of loops, or, more generally, a cut-set of K program points -a set such that removing these points cuts all cycles in the program [START_REF] Shamir | A linear time algorithm for finding minimum cutsets in reducible graphs[END_REF].

Second, considering each transition separately might also lead to a lack of precision: a loop might have a linear lexicographic ranking function that decreases along each of its paths as a whole, but none that decreases at each step of these paths, e.g., Listing 1. Thus, following [START_REF] Gulwani | The reachability-bound problem[END_REF], we will treat each path inside a loop as a single transition. Unfortunately the number of paths may be exponential in the size of the program (e.g. if the loop consists in t successive if-then-else tests, the number of paths is 2 t ), thus the constraint system may become very large, even though it features fewer variables. We propose a new approach which avoids the explicit computation of (all) the paths.

Contribution

We present an approach for computing lexicographic linear ranking functions when all paths inside a loop are treated separately. We lazily build a constraint system according to extremal counterexamples (a counterexample is a path where a candidate ranking function increases) -a naive approach with arbitrary counterexamples could fail to terminate. We implemented our approach and benchmarked it against existing analyzers.

Contents This article is organized as follows. After recalling the main definitions and notations (section 2), we present the main ideas of a first algorithm in section 3, and then the workarounds to ensure its own termination (section 4). Section 5 and section 6 discuss extensions to multidimensional ranking functions and multi control points. Section 7 discusses coNP-completeness and worst-case complexity. Section 8 gives some possible extensions w.r.t. the expressiveness of the method. Section 9 discusses implementation and experimental results. Finally, Section 10 highlights the improvements brought by our contribution.

Related Work

The use of ranking functions (a nonnegative strictly decreasing integer quantity) for proving the termination of programs goes back to [START_REF] Turing | Checking a large routine[END_REF]. We thus will not attempt to give a complete timeline of the topic; Ben-Amram and Genaim [2014] present a longer survey.

In proof assistants (such as e.g. the B method or PVS), it is customary to require from the user such a function for proving the termination of loops or recursive calls. Linear ranking functions are one of the simplest kind to generate automatically; yet not every interesting numerical program can be proved to terminate with such a function. Polynomial ranking functions are more powerful, but considerably more difficult to handle.

In recent years, two approaches have attracted particular attention. Lexicographic linear ranking functions [START_REF] Alias | Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs[END_REF], [START_REF] Cook | Ramsey vs. lexicographic termination proving[END_REF], Bradley et al. [2005b,a], Ben-Amram and Genaim [2014] are both much more powerful than linear ranking functions (e.g. one can easily prove the termination of the Ackermann-Péter function) and not much harder to obtain. A natural extension of this framework is, instead of requiring a single, monolithic ranking function at all program points, to make it dependent on the program point. Other extensions include piecewise linear ranking functions [START_REF] Urban | The abstract domain of segmented ranking functions[END_REF] and ordinal-value ranking functions [START_REF] Urban | An abstract domain to infer ordinal-valued ranking functions[END_REF], which subsume lexicographic orders.

Another approach is based on Ramsey's theorem [START_REF] Codish | Proving termination one loop at a time[END_REF], the idea being that a program is non-terminating if and only if there exists some feasible non-terminating loop in the control flow. As noted in [START_REF] Cook | Ramsey vs. lexicographic termination proving[END_REF], while some of the reasoning is local (one loop at a time), the method operates over the transitive closure of program transitions, which is not easy to approximate finely.

The problem of synthesizing a nonnegative linear function over a convex polyhedron satisfying certain properties was studied in the context of scheduling. Feautrier [1992a] proposed applying Farkas' lemma; others suggested an approach based on generators (vertices), as ours. A comparison of the two dual approaches (constraints vs generators) showed that constraints scaled better for scheduling problems [START_REF] Balev | Linear programming models for scheduling systems of affine recurrence equations -a comparative study[END_REF]. In contrast, [START_REF] Ben-Amram | Ranking functions for linear-constraint loops[END_REF] used the vertices of the integer hull of the transition relation. We improve on this approach by lazily enumerating the generators, without explicitly computing this convex hull.

Preliminary Definitions

In this section, we will define the concepts used in the rest of the article, following the notations of Ben-Amram and Genaim [2014]. Theses concepts will be illustrated in Example 1. We write column vectors in boldface (as x). Sets are represented with calligraphic letters such as W, P, etc.

Closed Convex Polyhedra

Schrijver [1998] presents this topic in detail.

Definition 1 (Polyhedra). A rational convex polyhedron P ∈ Q n is the set of solutions of a set of inequalities Ax ≤ b where A ∈ Q m×n is a rational matrix of n columns and m rows, x ∈ Q n and b ∈ Q m are columns vectors of n and m rational values respectively. We denote by Constraints(P) the set of constraints of P.

Definition 2 (Integer Hull). For a given polyhedron P ∈ Q n the set of integer points of P is denoted by I(P).

Definition 3 (Generator representation). The vertices and rays (if unbounded) of a closed convex polyhedron form a system of generators:

P = i α i v i + i β i r i α i ≥ 0, β i ≥ 0 i α i = 1
In the following, the expressions "convex polyhedron" and "polyhedron" refer to rational closed convex polyhedra as defined above.

Transitions and Invariants

We consider programs over a state space W × Z n , where W is the finite set of control states, defined by an initial state and a transition relation τ .

W needs not be the set of syntactic control points in the program (e.g. one per instruction, or one per basic block): it is sufficient that they form a cut-set of the syntactic control states, that is, a set of points such that removing them cuts all cycles in the program. This ensures that, for any k, k ∈ W, the transition relation (k, x) → τ (k, x ) can be expressed in the same theory as the individual transitions with a formula of linear size, using propositional variables to encode execution paths, as commonly practiced in predicate abstraction and other analysis methods using satisfiability modulo theory [START_REF] Monniaux | Using bounded model checking to focus fixpoint iterations[END_REF]. In block-structured programs the set of loop headers is a cut-set, and a minimal cut-set may be computed in linear time [START_REF] Shamir | A linear time algorithm for finding minimum cutsets in reducible graphs[END_REF].

Let us thus assume that τ is given as the solution over x 1 , . . . , x n and x 1 , . . . , x n , the values before and after the transition (all other variables being considered as implicitly existentially quantified), of a formula built from ∧, ∨ and non-strict linear inequalities and linear equations, excluding negation and strict inequalities. τ is then equivalent to a union U of closed convex polyhedra; intuitively each disjunct of {(x, x ) | (k, x, k , x ) ∈ τ } corresponds to a path from k to k in the program.

Definition 4 (Invariants). An invariant on a control point k ∈ W is a formula φ k (x) that is true for all reachable states (k, x). We will note invariants as I k (or I when the control point is implicit). PLDI'15 Gonnord, Monniaux, Radanne -Author Version -3/20 Definition 5 (Constraints). Let us consider an invariant I as a nonempty closed convex polyhedron whose integer hull is given by a set of inequalities

I = {x | m i=1 a i .x ≥ b i }. Constraints(I) denotes {a i , i ∈ [1, m]}
We assume that some external tool provides us with invariants: either affine invariants provided by e.g. polyhedral analysis [START_REF] Cousot | Automatic discovery of linear restraints among variables of a program[END_REF] or its refinements as in the Aspic 3 [START_REF] Gonnord | Combining widening and acceleration in linear relation analysis[END_REF], [START_REF] Feautrier | Accelerated Invariant Generation for C Programs with Aspic and C2fsm[END_REF] or the Pagai [START_REF] Monniaux | Using bounded model checking to focus fixpoint iterations[END_REF], Henry et al. [2012b[START_REF] Henry | The Pagai static analyser[END_REF] tools. In section 8 we shall relax this requirement.

Φ denotes a set of quadruples (k, x, k , x ), where k, k are control states and x, x vectors of numeric variables, such that for any possible transition (k, x) → τ (k , x ) of the program, (k, x, k , x ) ∈ Φ. Such a Φ may be obtained from invariants as follows:

(k, x, k , x ) ∈ Φ ⇐⇒ I k (x) ∧ (k , x) → τ (k, x ).
We only require that Φ may be expressed in a decidable theory in which it is possible to perform linear optimization; e.g. linear integer arithmetic, combined or not with uninterpreted functions; this is a form of large block encoding. Again, this includes the case considered by Ben-Amram and Genaim [2014]: for k, k fixed, the projection to x, x can be expressed as a union of polyhedra.

There is a crucial difference between our approach and that of Ben-Amram and Genaim [2014, §2.3-2.4] with respect to complexity. They consider an explicit list of polyhedra, which may contain 2 n polyhedra if the program from location k to location k consists in n successive if-then-else statement: in essence, they take Φ in disjunctive normal form. In contrast, in this article we seek to enumerate vertices of the convex hull of Φ lazily, never computing its disjunctive normal form.

In addition to allowing disjunctions ∨ inside the formula (not just at the outer level), we allow existential quantifiers ∃. Such a formula is equivalent to one of same size and in prenex form where all the variables not in x, x are existentially quantified. Again, this is important for complexity: even for a conjunction of linear constraints, eliminating a block of existential quantifiers (that is, projecting the polyhedron) may result in exponential blow-up.

Ranking Functions

Definition 6 (Linear ranking function). A (strict) lexicographic linear ranking function of dimension m is a function ρ

: W × Z n → Z m , such that 1. for any state k ∈ W, x → ρ(k, x) is affine; 2. for any (k, x, k , x ) ∈ Φ, ρ(k , x ) ≺ ρ(k, x)
where x 1 , . . . , x m ≺ y 1 , . . . , y m if and only if there exists an i such that x j = y j for all j < i and x i < y i ;

3. for any state (k, x) in the invariant I, all coordinates of ρ(k, x) are nonnegative.

It is said to be monodimensional, or a linear ranking function, if m = 1, and multidimensional otherwise.

We note ranking functions:

ρ(k, x) = λ k • x + λ k 0 or ρ(x) = λ • x + λ 0 when the control point is implicit.
Definition 7 (Quasi lexicographic linear ranking function). A quasi lexicographic linear ranking function replaces Condition 2 by ρ(k , x ) ρ(k, x) where is the lexicographic ordering.

The existence of a strict (lexicographic) linear ranking function entails the termination of the program. In the following, we deal with a unique control point k with I its invariant and τ its transition relation 4 . We will consider the situation with multiple control points section 6.

Example 1 (Monodimensional linear ranking function). Consider the following transition relation on Q 2 , where transitions are specified by ( guard action ): Under initial assumptions x = 5, y = 10, an invariant generator ( Aspic) gives the following inductive invariant for I (Figure 1):

k 0 t1 x ≤ 10 ∧ 0 ≤ y x := x + 1 y := y -1 t2 0 ≤ x ∧ 0 ≤ y x := x -1 y := y -1 PLDI'15 Gonnord, Monniaux, Radanne -Author Version -4/20
I = {0 ≤ x + 1, x ≤ 11, 0 ≤ y + 1, y ≤ x + 5, x + y ≤ 15}
from these invariants we compute the a i and b i :

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 nonnegative on I, and both t 1 and t 2 make this expression strictly decrease.

Cones

We first recall the definition of convex cones and orthogonality [Gärtner and Matoušek, 2012, §4.2].

Definition 8. A convex cone of Q n is a subset ∆ of Q n such that : i) For all x ∈ ∆, α > 0, αx is also in ∆. ii) For all x, y ∈ ∆, x + y is also in ∆. Definition 9. The orthogonal ∆ ⊥ of ∆ is defined as {u | ∀v ∈ ∆, u.v ≥ 0}. If ∆ is a convex cone, ∆ ⊥ is also a convex cone.
Proposition 1. The quasi ranking functions form a closed convex cone.

Quasi Monodimensional Ranking Functions of Maximal Termination Power

We shall now see that, for a program with one control state, finding a quasi monodimensional ranking function amounts to finding a vector in the intersection of the cone generated by the constraints of an inductive invariant (to ensure positiveness) and the orthogonal of the cone {x -x | (x, x ) ∈ τ } where τ is the transition relation. This suggests a naive (but wrong) algorithm, which incrementally constructs the desired cone as the solution set of a constraint system, generated through a counterexample-guided approach.

Quasi Ranking Functions in Terms of Cones

We assume here that Φ

= {(x, x ) | x ∈ I ∧ (x, x ) ∈ τ } where I is a (nonempty) invariant defined by I = {x | m i=1 a i .x ≥ b i }.
A quasi ranking function is considered to be a linear affine function that is nonincreasing when a τ step is taken, and stays nonnegative on I. The rest of the section recalls some results obtained in the field of polyhedral scheduling Feautrier [1992a,b].

Proposition 2. Under these assumptions, ρ = λ • x + λ 0 is a quasi ranking function if and only if the following conditions hold:

∀x, x x ∈ I ∧ (x, x ) ∈ τ =⇒ λ • (x -x ) ≥ 0 (1) ∃γ 1 ≥ 0, . . . , γ m ≥ 0, λ = m i=1 γ i a i (2)
Proof. First, Equation 1 is obtained by rewriting the decreasing condition using linearity. Secondly, Farkas' Lemma [START_REF] Schrijver | Theory of linear and integer programming[END_REF] applied to the nonempty polyhedron I, where vector inequality ρ(k, x) ≥ 0 holds, yields:

∃γ 1 ≥ 0, . . . , γ m ≥ 0, λ = m i=1 γ i a i ∧ λ 0 ≤ m i=1 γ i b i
Once the condition λ = m i=1 γ i a i is met then an appropriate choice of λ 0 can always be made, thus Equation 2 is verified.

Equation 2 means that λ belongs to the cone generated by the a i constraints, denoted as Cone constraints (I) from now on. Equation 1 is also equivalent to stating that λ belongs to some (other) cone, as we will see in the following. Let P I,τ = {x -x | x ∈ I ∧ (x, x ) ∈ τ } be the set of all reachable 1-step differences. 5Equation 1 is then equivalent to stating that λ belongs to the orthogonal of the convex cone generated by P I,τ .

Let us reexamine the condition that λ • u ≥ 0 for all u ∈ P I,τ . Remark that this condition is left unchanged if we replace P I,τ by its convex hull (a linear inequality is true over a set if and only if it is true over the convex hull of this set). Because I and τ are (finite unions of) convex closed polyhedra, so is P I,τ , and thus the closure of its convex hull P H I,τ is a closed convex polyhedron.6 If bounded, then this convex polyhedron is just the convex hull of its vertices, but if unbounded one has to include rays and lines as generators, as in Definition 3: the condition λ

• u ≥ 0 for all u ∈ P H I,τ is then replaced by ∀i λ • v i ≥ 0 ∧ ∀i λ • r i ≥ 0
For the sake of simplicity, we now group these three conditions into one: there is a finite set

V = {v 1 , . . . , v m } such that Equation 1 is equivalent to ∀1 ≤ i ≤ m, λ • v i ≥ 0,
otherwise said λ belongs to the polyhedral convex cone with faces defined by the v i , denoted by Cone(V I,τ ).

We have expressed both conditions of Definition 6 as membership of λ in polyhedral cones, respectively given by constraints and generators:

Proposition 3. Let V I,τ a set of generators of P H I,τ . Then ρ(x) = λ • x + λ 0 is a quasi ranking function iff λ ∈ Cone constraints (I) ∩ Cone(V I,τ ).
Thanks to this proposition, we can restrict the search of a ranking function to vectors that are linear combinations of Constraints(I) and of V I,τ , which we will do in Definition 11.

Maximal "Termination Power" and Strict Ranking Functions

We are however interested in more than quasi ranking functions (otherwise, λ = 0 would do!). In the simplest cases, we would like

∀1 ≤ i ≤ m, λ • v i > 0: by appropriate scaling of λ, we can ensure that ∀1 ≤ i ≤ m, λ•v i ≥ 1 and thus λ is a ranking function, proving termination. Remark that this condition ∀i λ • v i > 0 is otherwise expressed by "λ lies in the interior V ⊥ • of V ⊥ ".
In case there is no strict ranking function, we will settle for what is the closest best:

Definition 10. λ is said to have maximal termination power if λ • v i > 0 for as many v i as possible.

In the framework of [START_REF] Alias | Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs[END_REF], this would be equivalent to maximizing the number of transitions where ρ decreases strictly.

The notations and results of this section are also adapted from Feautrier [1992a,b].

For λ ∈ V ⊥ , we define the set π V (λ) = {v ∈ V | λ • v > 0}; we would like ρ = λ • x + λ 0 of maximal |π V (λ)|.
Proposition 4. Given V = {v 1 , . . . , v N } a set of vectors and λ a vector, π V (λ) is maximal with respect to cardinality if and only if it is the maximum with respect to inclusion, i.e.

∀λ , |π V (λ )| ≤ |π V (λ)| ⇔ ∀λ , π V (λ ) ⊆ π V (λ) Proof. It is obvious that for all λ , if π V (λ ) ⊆ π V (λ) then |π V (λ )| ≤ |π V (λ)|.
Let us now prove the other implication. Let λ be a vector such that ∀λ , |π

V (λ )| ≤ |π V (λ)| and λ a vector. Let us suppose that π V (λ ) ⊆ π V (λ), then π V (λ )\π V (λ) is not empty. Since π V (λ) ∪ π V (λ ) ⊆ π V (λ + λ ), |π V (λ + λ )| ≥ |π V (λ) ∪ π V (λ )| = |π V (λ)| + |π V (λ )\π V (λ)| > |π V (λ)|, which is absurd since |π V (λ)| is assumed to be maximal. Thus, ∀λ , π V (λ ) ⊆ π V (λ).
From now, the problem of finding a ranking function of maximal termination power is thus reduced to maximising an affine objective function on a set of affine constraints. We thus define a family of Linear Programming instances: Definition 11. Given V = {v j |1 ≤ j ≤ N } a set of generators of (the convex hull of ) P I,τ and Constraints(I) = {a i |1 ≤ i ≤ m} a set of vectors (constraints of I), we denote by LP (V, Constraints(I)) the following linear programming instance where γ i and δ i are the unknowns:

       Maximize 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 maximizing the objective function. In the following, we denote as γ the vector with γ i components. Thanks to the previous section, we have the following result: Proposition 5. Let V = {v j |1 ≤ j ≤ N } be a set of generators of the convex hull of P I,τ and Constraints(I) = {a i |1 ≤ i ≤ m} the constraints of I. Then :

• LP (V, Constraints(I)) is always feasible. • 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 quasi ranking function of maximal π V .
Proof.

• Let us start by noticing that (γ, δ) = (0, 0) is a solution of the inequalities, and i δ i ≤ N , thus the set { i δ i |(γ, δ) is a solution of LP} has a least upper bound.

Moreover, in the optimum of LP (V, Constraints(I)), each δ j is either 0 or 1 : if 0 < δ j < 1, then by scaling up λ by a factor 1/δ j we obtain a solution ρ with δ j = 1. Therefore, the least upper bound is a maximum. It ensues that LP (V, Constraints(I)) is always feasible.

• All solutions of the inequalities are quasi ranking functions, thanks to Proposition 3.

• δ i = 1 iff v i ∈ π V (λ), thus |π V (λ)| = i δ i .
Note that δ j = 0 means that all solutions to the problem satisfy λ • v j = 0, a flatness condition that we shall discuss later.

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 Ben-Amram and Genaim [2014], compute their generators (x, x ) and collect all resulting xx ; 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

Let us propose a simple but somewhat wrong incremental algorithm, which will help understand the correct algorithm presented later. C is a set of vectors and ρ(x) = λ • x + λ 0 a candidate ranking function.

1. Initialize C := ∅, ρ(x) := 0, thus λ = 0. Example 2 (Example 1, cont.). We already computed the generators a i for I.

k 0 t1 x ≤ 10 ∧ 0 ≤ y x := x + 1 y := y -1 t2 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 the algorithm described subsection 3.3 step by step, repeated steps will be noted with '. 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)) =        Maximize δ 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)) =            Maximize δ 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 ∧ τ ∧ y -y ≤ 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 .

Termination Problems

Unfortunately, this simple algorithm suffers from two problems which may prevent its termination (see Example 3).

PLDI'15 Gonnord, Monniaux, Radanne -Author Version -8/20

The set of counterexamples is infinite 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). Depending on the implementation of the SMT-solver, it may be the case that all models u are vertices constructed by intersection of the linear atomic constraints in I ∧ τ , of which there are finitely (exponentially) many, which would ensure termination.

Note that, even in this favorable case, the algorithm will produce vertices that do not lie on the boundary of the convex hull P H I,τ , and thus accumulate unoptimally tight constraints, which may eventually become redundant. A better option is to impose that the model for the SMT-test should minimize λ•u, as in "optimization modulo theory" [START_REF] Nieuwenhuis | On SAT modulo theories and optimization problems[END_REF], [START_REF] Sebastiani | Optimization in SMT with LA(Q) cost functions[END_REF], which ensures that vertices are on the boundary of P H I,τ ; we shall explore this idea in section 4.

No Strict Ranking Function 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 (quasi) ranking function such that λ • u > 0. But what if the SMT-solver picks u such that all quasi ranking functions λ satisfy λ • u = 0? In this case, the algorithm may not terminate, always picking the same u.

Example 3. The algorithm does not terminate on this automaton:

k 0 t1 i 0 ∧ j 1 j := j -1 t2 i 0 ∧ j 0 i := i -1 j := N
Indeed, on the transition t 2 , j -j ≤ -N , and there is no constraint on N . Thus, if x = (i, j, N ) denoted the vector of variables, r = (0, -1, 0) is a ray of P H I,τ . As long as λ • r < 0, the SMT solver can return an infinite number of models as I ∧ τ ∧ λ • (x -x ) ≤ 0 is always satisfiable.

Corrected Mono-dimensional Algorithm

Let us now address the termination issues raised in subsection 3.4. We will first assume, as said then, that we use an optimizing SMT solver to minimize λ • u for u = xx in order to discover tight bounds of P H I,τ .

Non Termination due to the Absence of a Strict Ranking Function

The set {u | λ • u = 0 ∀ quasi ranking function ρ(x) = λ • x + λ 0 } is a linear subspace of Q n . To prevent elements from this subspace from being returned again and again by the SMT-solver, we maintain a linearly independent family {B 1 , . . . , B p } ⊆ Q n (initially empty), such that we search for solutions λ such that λ • B i = 0 for all 1 ≤ i ≤ p. Every time a new model u is found, it is added to C, and a new optimal solution (λ, λ 0 , δ) is computed, we check whether δ u (ie. δ i for i the index of u in C) is 0 or 1. If it is 0, which means that all quasi ranking functions will satisfy λ • u = 0, thus u is added to B. We then add to the SMT-query a subformula AvoidSpace(u, B) that forces u not to be a linear combination of elements of vectors of B (u / ∈ Span(B)). This constraint can be implemented by completing B into a basis (B, B ) of Q n , then:

AvoidSpace(u, B) ⇔ ∃(α i ) vi∈B ∃(β i ) vi∈B s.t. u = vi∈B α i v i + vi∈B β i v i ∧ i β i = 0

SMT Formulas with Unbounded Domain

In light of Example 3, the issue could be corrected by adding the constraints λ•r ≥ 0 for all ray generators r of P H (we will prove later that it does). However, computing all generators of P H may be expensive. Instead, we add generators on demand, as we do for vertices.

In addition to the vertices, we add to C the ray generators r incrementally, when the SMT-solver returns a model of the form u = • • • + βr such that λ • u unbounded, we compute r and add it to C.

Proposition 5 is still true, since m i=1 γ i (r.a i ) ≥ 0 for all r a ray of P H is a necessary condition for λ to be a quasi ranking function. PLDI'15 Gonnord, Monniaux, Radanne -Author Version -9/20

Final Algorithm and Proof

These remarks and solutions finally lead to Algorithm 1.

Algorithm 1 Monodim

Input: I and τ C ← ∅, B ← ∅ finished ← false λ ← 0, λ 0 ← 0 while ¬finished ∧ Sat(I ∧ τ ∧ AvoidSpace(u, B)) with minimization for λ • u(≤ 0) do (u, unbound) ← a model for u in the above SMT test C ← C ∪ {u} if unbound then Let r a ray generator of P H such that u = • • • + αr C ← C ∪ {r} (γ, δ) ← LP (C, Constraints(I)) if γ = 0 then finished ← true else λ ← m i=1 γ i a i , λ 0 ← m i=1 γ i b i if δ u = 0 then B ← B ∪ {u} return (λ, λ 0 , ( i δ i = 1) ∧ ¬Sat(I ∧ τ ∧ u = 0))
Adding "(I ∧ τ ∧ u = 0) unsatisfiable" is necessary in the case where there is a vector x such that (x, x ) ∈ τ . Indeed, the constraint AvoidSpace(u, B) prevents the SMT-solver from returning the model (x, x). Without this additional test, if B = ∅ at the end, the algorithm would return (λ, λ 0 , true) instead of (λ, λ 0 , false). Proposition 6. Algorithm 1 always terminates and returns a quasi ranking function of maximal termination power (Definition 10) Lemma 1. Algorithm 1 always terminates.

Proof. The number of vectors in B can only increase or stay the same, and it is bounded by n, thus B becomes stationary. Once it is stationary, so is the SMT formula (save for the optimization direction λ • u ≤ 0).

We argue that when B is stationary, then once δ i = 1 at one iteration, then it stays so at all future iterations. Suppose the opposite: we had a system C of constraints (that is, i λ • c i ≥ 0) such that δ i0 = 1 at the preceding iteration, and we are adding a new constraint C (λ • c ≥ 0). As LP (C ∪ {C }, Constraints(I)) yields δ i0 = 0 for some i 0 , this means, by Farkas' lemma [START_REF] Schrijver | Theory of linear and integer programming[END_REF], that -c i0 can be expressed as a combination of the other constraints in C and of C , otherwise said there exist nonnegative γ i , γ such that -c i0 = i =i0 γ i c i + γ c . If γ = 0, then C (without C ) already implies λ • c i0 ≤ 0 and thus δ i0 is already null at the preceding iteration; contradiction. Therefore, there exist nonnegative µ i such that -c = i µ i c i , otherwise said any solution of C satisfies λ • c ≤ 0; then this means, in our algorithm, that δ u = 0, and thus B is updated; but we have assumed B is stationary so this cannot occur.

Once B is stationary, all vectors u (or r) in C either belong to the vector space spanned by B (case δ u = 0), or satisfy δ u = 1. All λ obtained thus verify λ • u > 0 for all u in C but not in the span of B. A u or r that was already given as solution by the SMT solver cannot be given again.

Since we have assumed that the solutions of the form i α i v i returned by the SMT solver are taken from the finite set of generators of P H , then the algorithm terminates in at most as many iterations as the number of generators.

The algorithm returns (λ, λ 0 , b) where ρ(x) = λ • x + λ 0 is a quasi ranking function and b is a Boolean stating whether it is strict. Note that it is possible that λ is null, meaning that there is no linear ranking function that makes at least one transition (x, x ) decrease strictly. The following lemmas state that λ is of maximal termination power; recall that π(λ) is the set of vertices (x, x ) of I ∧ τ such that λ • u > 0.

Lemma 2. The algorithm returns λ with maximal π(λ).

Proof. If there is (x, x ) such that λ • u = 0, either u ultimately belongs to B in which case there is no λ such that λ • u > 0, either it does not in which case λ • u > 0.

Lemma 3. Let λ be the quasi ranking function produced by the algorithm and λ be another quasi ranking function. Then, for all (x, x

) ∈ I ∧ τ , if λ • u > 0 then λ • u > 0.
Proof. u can be expressed as a barycenter of a subset of vertices of

P H : u = v∈V α v v with v∈V α v = 1 and for all v ∈ V , α v > 0, where V ⊆ V . Thus λ • u = v α v λ • v (similarly for λ ). Thus if λ • u = 0, then for all v ∈ V , λ • v = 0.
Since λ has maximal π V (λ) by the preceding lemma, it follows that λ • v = 0 for any v ∈ V . But then λ • u = 0. We thus have proved the contrapose of the result.

Multidimensional Algorithm

Let us note ≺ (resp. ) the strict lexicographic ordering (resp. quasi lexicographic ordering) over vectors of integers. Our approach is similar to the one of [START_REF] Alias | Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs[END_REF]: for each dimension (d), generate a quasi ranking function of maximal termination power ρ d (x) = λ d • x + λ 0,d , after restricting the invariant on successive states to transitions that leave the previous components constant. The algorithm is described in Algorithm 2.

Algorithm 2 Multidim Input:

I and τ d ← 1, failed ← false repeat (λ, λ 0 , strict) ← Monodim I, τ ∧ d <d λ d • u = 0 if ¬strict then if λ is in the span of ρ then failed ← true else ρ d ← λ + λ 0 d ← d + 1 until strict ∨ failed return if failed then "None" else ρ Lemma 4.
At every iteration of Algorithm 2, ρ is a linearly independent family. Proof. By induction over the number of iterations (the size of ρ). If λ obtained from Monodim is a linear combination of ρ, then λ • u = 0 for all transitions specified in the call to Monodim; but then Monodim should have returned failed.

Corollary 1. Algorithm 2 always terminates in at most n iterations.

Proof. ρ is a linearly independent family in Q n , its size growing at each iteration.

The multidimensional ranking function produced by Algorithm 2 is at least as powerful for proving termination as any other: Lemma 5. Let ρ be the quasi multidimensional ranking function produced by Algorithm 2 at any iteration m and ρ be another quasi multidimensional ranking function of dimension at most m. Then, for all

(x, x ) ∈ I ∧ τ , if ρ (x) ρ (x ) then ρ(x) ρ(x ).
Proof. By induction over m. The base case m = 0 is obvious. Now for m > 0. Let ρ <m and ρ <m be the respective projections of ρ and ρ to their first m -1 coordinates. Let (x, x ) ∈ I ∧ τ such that ρ (x) ρ (x ). If ρ <m (x) ρ <m (x ), then the induction hypothesis concludes. Now assume ρ <m (x) = ρ <m (x ). Let ρ m and ρ m be the respective projections of ρ and ρ on their m-th coordinate; then ρ m (x) > ρ m (x ). Recall that ρ m and ρ m are quasi monodimensional ranking functions over {x | ρ <m (x) = ρ <m (x )}, and ρ m is the one returned by Monodim. By Lemma 3, ρ m (x) > ρ m (x ), which concludes.

Theorem 1. Algorithm 2 returns a multidimensional strict ranking function if and only if one exists relative to the invariant given; furthermore, the function returned is of minimum dimension.

Proof. (If ) Let ρ be a multidimensional strict ranking function and ρ is the quasi multidimensional ranking function returned by Algorithm 2 (or, if None, the last value of ρ). Let (x, x ) ∈ τ ∧ I; ρ (x) ρ (x ) because ρ is a strict ranking function; then by Lemma 5, ρ(x) ρ(x ); thus ρ is also a strict ranking function. (Only if ) From the termination condition, if Algorithm 2 does not return None, then it returns a strict ranking function.

(Minimality) Let ρ be a multidimensional strict ranking function and ρ the one returned by Algorithm 2. Assume also that the dimension m of ρ is less than that of ρ. By Lemma 5 applied to the m-th iteration, then ρ <m is a strict ranking function; but then the algorithm should have stopped at that iteration.

Multiple Control Points

Let us now consider a program with n variables, a set of control points W, an invariant I and a transition invariant Φ (the general case). We do not distinguish between a control point k and its integer index in W.

Once a cut-set W of program control points has been identified, the program can be rewritten with only W as control points, with "large block transitions" between the control points in W . To each control point k in W , one associates a lexicographic linear function f k . We want that, for any path k 1 → k 2 with initial values x and final values x , , f k1 (x) < f k2 (x 2 ). Then, searching for such rankings amounts to searching for a unique vector of size |w| × n, which is f = (f k1 , f k2 , . . .). All notations are adapted adequately.

Considering k in W, we remind the following notations:

1. We note the ranking function in

k: ρ(k, x) = λ k • x + λ k 0 .
2. We note the invariant in k:

I k = {x, m k i=1 a k i .x ≥ b k }.
Definition 12. e k (x) is a vector of size |W| × n null everywhere except in the coordinates k × n to (k + 1) × n -1, where it is x.

Definition 13. We note λ the vector of size |W| × n formed by the concatenation of the λ k .

e k (x) = 0 • • • 0 x 0 • • • 0 λ = λ 1 • • • λ k-1 λ k λ k+1 • • • λ |W| We have λ • e k (x) = λ k • x.
Definition 14. We note Constraints(I) = ∪ k {e k (a k i )|a k i ∈ Constraints(I k )} the set of vectors encoding the program invariants.

We will now modify the algorithm presented subsection 3.3 to work on multiple control points. The main modification is in the encoding of the SMT problem:

1. Two new additional variables, k and k , denotes the starting and ending control points.

2. We now have u = e k (x) -e k (x ).

We still minimize

λ • u = ρ(k, x) -ρ(k , x ).
Algorithm 1 is modified into Algorithm 3. The multidimensional Algorithm 2 is left unchanged, except that it calls Algorithm 3 instead of Algorithm 1.

Example 4 (Multi control points). The following example comes from a program with two nested loops [START_REF] Alias | Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs[END_REF]. We have W = {1, 2} and 2 variables i, j.

PLDI'15 Gonnord, Monniaux, Radanne -Author Version -12/20

Algorithm 3 Monodim-Multi for multiple control points Input:

(I k ) k∈W and τ C ← ∅, B ← ∅ f inished ← f alse λ k ← 0, λ k 0 ← 0 for all k ∈ W while ¬finished ∧ Sat(I ∧ τ ∧ AvoidSpace(u, B) ∧ u = e k (x) -e k (x )) with minimization for λ • u(≤ 0) do (u, unbound) ← a model for u in the above SMT test C ← C ∪ {u} if unbound then Let r a ray generator of P H such that u = • • • + αr C ← C ∪ {r} (γ, δ) ← LP (C, Constraints(I)) if γ = 0 then f inished ← true else λ k ← i γ k i a k i , λ k 0 ← i γ k i b k i for all k if δ u = 0 then B ← B ∪ {u} return (λ 1 , . . . , λ |W| , λ 1 0 , . . . , λ |W| 0 , ( i δ i = 1) ∧ ¬Sat(I ∧ τ ∧ u = 0)) 1 2 t1 j > 0 t2 i < 5 j := 0 t3 i > 2 ∧ j ≤ 9 j := j + 1 t4 i ≤ 2 ∨ j > 9 i := i + 1
We have the following invariant:

I : (k = 1 =⇒ i ≤ 5) ∧ (k = 2 =⇒ 0 ≤ j ≤ 10 ∧ i ≤ 4) 1.
Beginning with C = {} and ρ(x) = 0, that is: λ 1 = 0 and λ 2 = 0. We have x = i j and u = e k (x) -e k (x ). In the SMT-query, τ is now written as follows:

k = 1 ∧ k = 2 =⇒ i < 5 ∧ j = 0 ∧ u = (i, j, i , j ) ∧ . . . First iteration. 2. Sat(I ∧ τ ∧ AvoidSpace(u, B) ∧ 0 • u ≤ 0) ? Yes, with k = 2, k = 1, x = 1 10 and x = -2 10 (this corresponds to transition t 4 ) 3. C ← 1 10 -2 -10 4. Call LP (C, Constraints(I)). It gives us λ 1 = 0 0 and λ 2 = 1/2 0 . Second iteration. 2'. Sat(I ∧ τ ∧ AvoidSpace(u, B) ∧ λ • u ≤ 0) ? Yes, with k = 2, k = 2, x = 3 0 and x = 3 1 . 3'. C ← C ∪ 0 0 0 -1 4'. Call LP (C, Constraints(I)).
It gives us λ 1 = 0 0 and λ 2 = -11/2 -1 . Third iteration.

2". Sat(I ∧ τ ∧ y -y ≤ 0) ? No, we stop. Return. We obtain ρ 1 (x) = 0, ρ 2 (i, j) = -11/2i -j + 32, a strict ranking function for (τ, I).

Complexity

Ben-Amram and Genaim [2014, Sec. 3], which consider integer programs with the combined transition PLDI'15 Gonnord, Monniaux, Radanne -Author Version -13/20 relation and invariant Φ specified in disjunctive normal form, provide an exponential-time algorithm and prove that the problem of deciding the existence of a linear ranking function is coNP-complete. We now shall show that this decision problem is still coNP-complete if the Φ specified as input is given in general form (let us say, with a linear integer arithmetic formula with prefix existential quantifiers and disjunctions allowed) as opposed to disjunctive normal form.

Proposition 7. Deciding the existence of a linear ranking function given Φ (with ∃-prefix and ∨) is coNP-complete.

Proof. coNP-hardness directly follows from our class of input including that studied by Ben-Amram and Genaim [2014]; let us now show membership in coNP.

Our algorithms (section 4, section 6) stop when either they have a linear ranking function, either they reach an unsolvable system of constraints. If the number of program variables is n and the number of control points is |P |, then these constraints are over u = (n + 1) • |P | unknowns. By a combination of Farkas' lemma and Carathéodory's theorem [Schrijver, 1998, §7.7], if this system is unsatisfiable, there exists an unsatisfiable subset of u + 1 of these constraints.

Each of this constraints is given by a generator (vertex or ray) of the integer hull of one of the disjuncts of the disjunctive normal form of Φ. The bit-size of such a generator is polynomial in the size of the constraint representation of this disjunct [Schrijver, 1998, §17.1], and this constraint representation is an extract of Φ. Therefore, a witness of the unsatisfiability of the constraint system (i.e. of the absence of a linear affine ranking function) may be given by u + 1 elements of polynomial size, and thus is itself polynomial.

Proposition 8. Our algorithms have exponential complexity at most. Proof. Our algorithms enumerate at most once each generator of the integer hull of each disjunct of the disjunctive normal form of Φ, which (as in the previous proof) have polynomial size; thus there is an exponential number of them. Each of them may be obtained as the maximum solution of integer linear programming problems for all disjuncts, which can be done in exponential time. Finally, at each iteration the constraint system is solved by linear programming.

Thus, moving to a more succinct representation of transitions than in Ben-Amram and Genaim [2014] conserves coNP-membership and solving in exponential complexity.

Extensions

Coupling of Invariant and Transition Relation We supposed in subsection 3.1 that we have an invariant I expressed as the constraints of a convex closed polyhedron, and a transition related τ expressed as a formula of real linear arithmetic. In subsection 2.2, following Ben-Amram and Genaim [2014] we instead considered a single relation Φ incorporating both invariant and transition. This format can be handled by also using counterexamples for the nonnegativity constraint -i.e. counterexamples are not only extremal nondecreasing quadruples (k, x, k , x ) but also extremal points (k, x) where the ranking function candidate is negative.

Note a subtle difference between the two approaches, when instantiated on the multidimensional algorithm from section 5: in our original algorithm, as in [START_REF] Alias | Rank: a tool to check program termination and computational complexity[END_REF], we require that each component ρ j of the multidimensional ranking function should be nonnegative with respect to an invariant I (∀x ∈ I ρ j (x) ≥ 0) while in the modified version, we restrict at each step the invariant to the states over which the preceding components of the multidimensional ranking function do not decrease. This is a more powerful approach: there are programs that cannot be proved to terminate by using the same invariant for nonnegativity in all components of a lexicographic linear ranking function, but can be if the invariant is refined across components [Ben-Amram and Genaim, 2014, Ex. 2.12].

Richer Classes of Formulas For the transition relation τ and for the compound transition rela-tion+invariant Φ, we have so far assumed linear integer arithmetic. In fact, any decidable theory for which it is possible to perform optimization with respect to the integer components will do.

It is for instance possible to handle uninterpreted functions and arrays, since, by Ackermann's expansion, to a quantifier-free formula F with uninterpreted functions one can associate a formula F without uninterpreted functions, such that F has the same models with respect to the free variables of F [Kroening and Strichman, 2008, ch. 4]. Universally quantified properties (e.g. ∀0 ≤ k < n t[k] = 4) can be over-approximated by quantifier instantiation.

Rational Variables

The monodimensional algorithms are suitable for synthesizing what Ben-Amram and Genaim [2014] call weak ranking functions on programs using rational variables: in Definition 6, replace Z by Q.

Proposition 9. If ρ is a monodimensional weak ranking function, there exists α > 0 such that αρ decreases by at least 1 at each step. Thus, the program terminates.

Proof. Let β = inf{ρ k •x-ρ k •x | (k, x, k , x ) ∈ Φ}.
Since Φ is a finite union of closed convex polyhedra, this infimum is reached within the set. β ≤ 0 would contradict the weak ranking function hypothesis. Then β > 0 and one can take α = 1/β. This simple scaling approach does not always work for multidimensional ranking functions, and a somewhat more complicated procedure must be applied to obtain a multidimensional ranking function (strict decreasing steps of at least 1 unit) from a multidimensional weak ranking function [Ben-Amram and Genaim, 2014, §5.3]. We did not investigate the combination of that procedure with our counterexample-based approach, since all multidimensional problems that we tried (except for concocted examples) were solved by scaling.

Disjunctive Invariants In some cases, it is interesting to have multiple ranking functions for the same control point, depending on some kind of partitioning. For instance, in

k n > 0 d = 1; x = 0 x := x + d x = n x := x + d; d := -1
it is necessary to distinguish two phases of the loop (d = 1, d = -1) with two different ranking functions (n -x and x).

Certain static analyzers, including Pagai in certain modes of operation Henry et al. [2012b,a,b], return disjunctive invariants: to a given program point (possibly in a cut-set of program points) they associate a disjunction of abstract elements; for instance, here, a possible invariant is

(d = 1 ∧ 0 ≤ x ≤ n) ∨ (d = -1 ∧ 0 ≤ x ≤ n) It is possible to split the control point according to d = 1 ∨ d = -1: k pos k neg n > 0 d = 1; x = 0 x := x + d x = n d = -1 x := x + d
Then by taking {k pos ; k neg } as cut-set, one can construct the ranking function.

Implementation and Experimental Results

Implementation We implemented our prototype Termite in 3k lines of OCaml7 . Termite uses LLVM8 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 Henry et al. [2012b[START_REF] Henry | The Pagai static analyser[END_REF] is used to compute invariants from the LLVM IR. The transition relation is produced from these invariants and the LLVM IR. Then, the core analyzer implements the multidimensional, multiple control point algorithm described herein. Z39 answers (optimizing) SMT and LP queries.

Experiments We have compared Termite with Loopus [START_REF] Urban | An abstract domain to infer ordinal-valued ranking functions[END_REF]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 synthesize better invariants than Pagai.

Difficulties A termination analyser typically consists in 1) a front-end 2) an invariant generator 3) a termination analysis. One therefore compares whole toolchains 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. We had to leave out other tools from our experiments due to difficulties in running them successfully and lack of documentation. It is also possible that we used some of the listed tools improperly; if so we apologize to their respective authors.

Limitations Contrary to iRankFinder17 , Termite is unable to prove termination when the desired (multidimensional) ranking function has non positive components: we did not implement the CEGAR loop for nonnegativity suggested in section 8.

Contrary to T218 Termite is also unable to prove termination when the behavior of a loop is divided into phases (as we already discussed in section 6), unless some preprocessor divided the phases into different control points.

We unfortunately were unable to compare these two tools with ours, due to different input formats and unavailability of converters.

Conclusion and Future Work

We have proposed a new algorithm for the derivation of lexicographic linear ranking functions. There has been ample literature on this on related topics (see [Alias et al., 2010, §6] and [START_REF] Cook | Proving program termination[END_REF] for a large panel of proposed methods) ; let us therefore summarize salient points of difference.

Termination with Guaranteed Result Several existing approaches do not necessarily terminate. In contrast, our approach always terminates, and always outputs a lexicographic linear ranking function if one exists. Also, it is guaranteed to be of minimal dimension.

Use of Concrete Runs instead of Farkas' Lemma Like previous algorithms [START_REF] Alias | Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs[END_REF], we solve a sequence of problems of finding quasi monodimensional linear ranking functions; and each quasi monodimensional linear ranking function is obtained as the solution of a linear program. Where we differ, however, is how we build these linear programs; our method produces much smaller ones (e.g. by 1-2 orders of magnitude compared to Rank [START_REF] Alias | Rank: a tool to check program termination and computational complexity[END_REF], and thus is more scalable.

Most other approaches Bradley et al. [2005a,b], [START_REF] Alias | Rank: a tool to check program termination and computational complexity[END_REF], [START_REF] Podelski | A complete method for the synthesis of linear ranking functions[END_REF], [START_REF] Larraz | Proving termination of imperative programs using max-SMT[END_REF] create new unknowns (coefficients from Farkas' lemma) for each face of each transition polyhedron corresponding to a path between control nodes considered for the ranking function, along with relevant constraints. In contrast, with ours, constraints correspond to concrete (x, x ) transitions and the number of unknowns does not depend on the complexity of the transitions. Also, instead of creating constraints upfront, we create them on demand.

Furthermore, we can deal with integer variables both easily and precisely (by specifying them as integers in the SMT-solving call) while other approaches [START_REF] Larraz | Proving termination of imperative programs using max-SMT[END_REF] need to apply refinements based on Gomory-Chvátal cutting planes. We can similarly deal with existential quantification, uninterpreted functions, arrays, Booleans etc. in the transition relation.

Use of a Cut-set Our approach is able to solve for ranking functions only at a "cut set" of control nodes. In particular, we do not require that there is a lexicographic linear ranking function at points outside of the cut-set. This is useful for instance if a ranking function would need to be defined by case analysis at such points (e.g. according to the value of a Boolean variable, as at point B in the following example); it is difficult to synthesize such ranking functions, but in our case we do not need to do so, because we synthesize the ranking function only a cut-set points (e.g. A). 19Listing 1: A linear r.f. decreases on each path, not each step int x = p o s i t i v e ( ) ; while In previous approaches [START_REF] Gulwani | The reachability-bound problem[END_REF], one had to expand the control flow between these nodes, yielding (in general) an exponential number of transitions. In contrast, our algorithm "sees" transitions as needed, performing counterexample-guided refinement of the constraint system, which improves scalability.

Comparison with Other Approaches The difference with Rank and iRankFinder is not with respect to expressive power (we show that one variant of our algorithm is equivalent to Rank and another to iRankFinder) but with respect to complexity and efficiency. Rank and iRankFinder need transition relations in disjunctive normal form: in order to deal, as we do, with "big block" transitions between a cut-set of control locations, they would need to expand them at exponential cost -though one can argue that in many programs this unfolding is not so large.

Our system of constraints is constructed lazily, theirs are constructed eagerly. Heizmann, Hoenicke & Podelski's approach (Ultimate Büchi Automizer) is to cover 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. [START_REF] Cook | Ramsey vs. lexicographic termination proving[END_REF] give contrived examples where lexicographic linear arguments cannot prove termination, but linear Ramsey-based arguments can. They however conclude that in almost all cases where linear Ramsey-based arguments work, lexicographic linear ranking functions are sufficient and that the question is therefore how to find them efficiently. This is the question we address in this article.

The algorithm in Loopus [START_REF] Zuleger | Bound analysis of imperative programs with the sizechange 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 quicky conclude for termination in many cases since simple arguments are very often sufficient to prove that a given loop terminates [START_REF] Rodrigues | Real-world loops are easy to predict : a case study[END_REF].

Future Work A natural extension of our counterexample-guided refinement approach would be to use it to generate the supporting invariant: instead of generating constraints for each (x, x ) transition encountered where x lies within a precomputed invariant I, one would first try to prove x to be unreachable, using any approach capable of providing an inductive invariant J such that x / ∈ J ; if successful, one would replace I by I ∩ J and restart.

A further refinement of the method would be to look for a large set of initial states that guarantee that x is unreachable; the intersection of such sets would be a sufficient condition for termination to be proved by the ranking function output by the algorithm (conditional termination).

Our algorithm for finding linear ranking functions is a particular kind of partial quantifier elimination: conditions 2 and 3 in Definition 6, or condition 1 in Proposition 2, are formulas of the form ∀x F where F is quantifier free: we wish to obtain a satisfying assignment of their free variables. A full quantifier elimination would compute exactly the cone of solutions, but we stop once we have a point in the relative interior. It remains to be seen how our approach of extremal instantiation would generalize to a more general class of quantified formulas.

Figure 1 :

 1 Figure 1: Invariant polyhedron for Example 1

  PLDI'15 Gonnord, Monniaux, Radanne -Author Version -7/20 2. Find a transition with an u = xx in P H I,τ which contradicts that ρ is a strict ranking function. More precisely: (a) Ask an SMT-solver if ∃u s.t. I ∧ τ ∧ λ • u ≤ 0. (b) If U nsat, ρ is a strict ranking function. Return it. (c) If Sat, we get u from the SMT model. 3. Add u to C. 4. Call LP (C, Constraints(I)) (see Definition 11) to compute a new ranking function that maximises the number of v ∈ C such that ρ(v) > 0 and go back to step 2.

  ( x >= 0 ) { / * A * / b o o l c = c h o o s e ( ) ; i f ( c ) x=x -1; / * B * / i f ( ! c ) x=x -1; }

Table 1 :

 1 10 Zuleger et al. [2011], AProVE 11[START_REF] Giesl | Proving termination of programs automatically with aprove[END_REF], Ultimate Büchi Automizer 12 , Rank[START_REF] Alias | Rank: a tool to check program termination and computational complexity[END_REF] (with the c2fsm front-end and As-Comparison. 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.[START_REF] Gonnord | Abstract acceleration in linear relation analysis[END_REF] accelerating invariant generator), on examples from Polybench 14 , WTC (V2) 15 , the termination competition 16 and some sorting algorithms (Table9). Termite solves 33% more examples than Loopus, in twice the time. AProVE and Ultimate are considerably slower.Due to limitations in its front-end and invariant generator, Rank can 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

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

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

This also emulates the situation where one looks for the exact same linear function at all control points.

[START_REF] Ancourt | A modular static analysis approach to affine loop invariants detection[END_REF] use it to compute loop invariants.

If P I,τ is bounded, then its convex hull P H I,τ is a closed convex polyhedron, but it might not be closed if P I,τ is unbounded: e.g. the convex hull of {(0, 0)} and {(1, x) | x ∈ Q} is {(0, 0)} ∪ (0, 1] × Q, which is not closed.

http://termite-analyser.github.io/

http://llvm.org/

https://github.com/Z3Prover

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

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

http://ultimate.informatik.uni-freiburg.de/BuchiAutomizer/ PLDI'15Gonnord, Monniaux,

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

http://www.loopkiller.com/irankfinder/linrf.php

http://research.microsoft.com/en-us/projects/t2/

Our approach can also be applied to synthesize the same linear ranking function at all nodes in the cut-set. This linear ranking function is therefore allowed to locally increase at nodes outside of the cut-set, as long as this increase is compensated before the next node in the cut-set is reached, as in some other approaches[START_REF] Zankl | Increasing interpretations[END_REF].

PLDI'15 Gonnord, Monniaux,

Acknowledgments

We would like to show our gratitude to Paul Feautrier for sharing his comments and ideas during the course of this research, and Marc Vincenti who helped us a lot with the benchmarks. We also thank the anonymous reviewers for their insightful comments and feedback, which improved the quality of this paper.

The research leading to these results has received funding from the European Research Council under the European Union's Seventh Framework Programme (FP/2007-2013) / ERC Grant Agreement nr. 306595 "STATOR"

1 Between the 1999 and 2011 C standards an exception ( §6.8.5:6) was added to allow compilers to assume that every non trivially infinite computation loop always terminates -a brutal way to avoid termination analysis! 2 Tools such as Absint's aiT (http://www.absint.com/ait/) and OTAWA (http://otawa.fr/