# The Arithmetic-Geometric Progression Abstract Domain

Jérôme Feret

► To cite this version:

Jérôme Feret. The Arithmetic-Geometric Progression Abstract Domain. the 6th International Conference on Verification, Model Checking and Abstract Interpretation - VMCAI 2005, Radhia Cousot, Jan 2005, Paris, France. pp.42-58, 10.1007/978-3-540-30579-8_3. inria-00528450

HAL Id: inria-00528450

https://inria.hal.science/inria-00528450v1

Submitted on 15 Feb 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# The Arithmetic-Geometric Progression Abstract Domain*

Jérôme Feret

DI, École Normale Supérieure, Paris, FRANCE
jerome.feret@ens.fr

**Abstract** We present a new numerical abstract domain. This domain automatically detects and proves bounds on the values of program variables. For that purpose, it relates variable values to a clock counter. More precisely, it bounds these values with the *i*-th iterate of the function $[X \mapsto \alpha \times X + \beta]$ applied on *M*, where *i* denotes the clock counter and the floating-point numbers *α*, *β*, and *M* are discovered by the analysis. Such properties are especially useful to analyze loops in which a variable is iteratively assigned with a barycentric mean of the values that were associated with the same variable at some previous iterations. Because of rounding errors, the computation of this barycenter may diverge when the loop is iterated forever. Our domain provides a bound that depends on the execution time of the program.

**Keywords:** Abstract Interpretation, static analysis, numerical domains.

## 1 Introduction

A critical synchronous real-time system (as found in automotive, aeronautic, and aerospace applications) usually consists in iterating a huge loop. Because practical systems do not run forever, a bound on the maximum iteration number of this loop can be provided by the end-user or discovered automatically. The full certification of such a software may require relating variable values to the number of iterations of the main loop. It is especially true when using floating-point numbers. Some computations that are stable when carried out in the real field, may diverge because of the rounding errors. Rounding errors are accumulated at each iteration of the loop. When expressions are linear and when the evaluation of expressions does not overflow, the rounding errors at each loop iteration are usually proportional to the value of the variables. Thus the overall contribution of rounding errors can be obtained by iterating a function of the form $[X \mapsto \alpha \times X + \beta]$. Then by using the maximum number of iterations we can infer bounds on the values that would normally have diverged in the case of an infinite computation.

We propose a new numerical abstract domain that associates with each variable the corresponding coefficients *α* and *β* and the starting value *M*. This

<footnote>* This work was partially supported by the ASTRÉE RNTL project.</footnote>
$$
\begin{align*}
& V \in \mathcal{V}, I \in \mathcal{I} \\
& E := I \mid V \mid I \times V + E \\
& P := V = E \mid \mathbf{skip} \mid \mathbf{tick} \mid \mathbf{if} (V \ge 0) \{P\} \mathbf{else} \{P\} \mid \mathbf{while} (V \ge 0) \{P\} \mid P; P
\end{align*}
$$

<caption>Figure 1. Syntax.</caption>

framework was fully implemented in OCAML [7] and plugged into an existing
analyzer [1,2]. We use this analyzer for certifying a family of critical embedded
softwares, programs ranging from 70,000 to 379,000 lines of C.

**Outline.** In Sect. 2, we present the syntax and semantics of our language. In Sect. 3, we describe a generic abstraction for this language. In Sect. 4, we define a numerical abstract predomain that relates arithmetic-geometric constraints with sets of real numbers. In Sect. 5, we enrich an existing analysis so that it can deal with arithmetic-geometric constraints. In Sect. 6, we refine our analysis to deal with more complex examples. In Sect. 7, we report the impact of the arithmetic-geometric progression domain on the analysis results.

## 2 Language

We analyze a subset of C without dynamic memory allocation nor side-effect. Moreover, the use of pointer operations is restricted to call-by reference. For the sake of simplicity, we introduce an intermediate language to describe programs that are interpreted between the concrete and an abstract level. Data structures have been translated by using a finite set of abstract cells (see [2, Sect. 6.1]). Non-deterministic branching over-approximates all the memory accesses (array accesses, pointer dereferencing) that are not fully statically resolved. Furthermore, floating-point expressions have been conservatively approximated by linear forms with real interval coefficients. These linear forms include both the rounding errors and some expression approximations (see [9]). We also suppose that the occurrence of runtime errors (such as floating-point overflows) can be described by interval constraints on the memory state.

Let $\mathcal{V}$ be a finite set of variables. Let clock $\notin \mathcal{V}$ be an extra variable which is associated with the clock counter. The clock counter is explicitly incremented when a command **tick** is executed. The system stops when the clock counter overflows a maximum value which is defined by the end-user. We denote by $\mathcal{I}$ the set of all real number intervals (including $\mathbb{R}$ itself). We define inductively the syntax of programs in Fig. 1. We denote by $\mathcal{E}$ the set of expressions $E$. We describe the semantics of these programs in a denotational way. An *environment* ($\rho \in \mathcal{V} \cup \{\mathbf{clock}\} \to \mathbb{R}$) denotes a memory state. It maps each variable, including the clock variable, to a real number. We denote by *Env* the set of all environments. The semantics of an expression *E* is a function $\langle E \rangle \in \mathit{Env} \to I$ mapping each environment to an interval. Given a maximum value *mc* for the clock, the semantics of a program *P* is a function $\llbracket P \rrbracket_{\mathit{mc}} \in \mathit{Env} \to \wp(\mathit{Env})$ mapping each environment $\rho$ to the set of the environments that can be reached when applying the program *P* starting from the environment $\rho$. Returning a set of environments allows the description of both non-determinism and program halting (when the
<figure><img src="image_2.png" /><figcaption>**Figure 2.** Concrete semantics.</figcaption></figure>

clock has reached its maximum value). The functions ($|-|$) and $[-]$$_{mc}$ are defined by induction on the syntax of programs in Fig. 2. Loop semantics requires the computation of a loop invariant, which is the set of all environments that can be reached just before the guard of this loop is tested. This invariant is well-defined as the least fixpoint of a $\cup$-complete endomorphism<fnref n="1" /> $f \in \wp(Env) \to \wp(Env)$. Nevertheless, such a fixpoint is usually not computable, so we give a decidable approximate semantics in the next section.

We describe two toy examples.

**Example 1.** The first example iterates the computation of a barycentric mean: at each loop iteration, a variable is updated with a barycentric mean among its current value and two previous values.

<figure><img src="image_3.png" /></figure>

where $I \in \mathcal{I}$, $\varepsilon_i > 0$ for any $i \in \{X; Y; Z; 0\}$, $0 < \alpha < 0.5$, $I_X = [1 - 2 \times \alpha - \varepsilon_X; 1 - 2 \times \alpha + \varepsilon_X]$, $I_Y = [\alpha - \varepsilon_Y; \alpha + \varepsilon_Y]$, $I_Z = [\alpha - \varepsilon_Z; \alpha + \varepsilon_Z]$, and $I_\varepsilon = [-\varepsilon_0; \varepsilon_0]$.

More precisely, initialization values range in the interval $I$. The parameter $\alpha$ is a coefficient of the barycentric mean. The parameters $\varepsilon_X$, $\varepsilon_Y$, and $\varepsilon_Z$ encode the rounding errors relative respectively to the variables $X$, $Y$, and $Z$ in the computation of the barycentric mean. The parameter $\varepsilon_0$ encodes the absolute rounding error. The three variables $X$, $Y$, and $Z$ allow the recursion ($X$ is associated with

<footnote n="1">¹ In fact, we only use the monotonicity of $f$.</footnote>
the current value, $Y$ is associated with the last selected value and $Z$ is associated with the previous selected value) and the three variables $V$, $B_1$, and $B_2$ allow non-deterministic boolean control. The variable $V$ allows stopping the loop iteration. The variable $B_1$ allows the selection of a recursive value which consists in shifting the variables $X$, $Y$, and $Z$. The variable $B_2$ allows the choice between a reinitialization or an iteration step: a reinitialization step consists in assigning the variables $X$, $Y$, and $Z$ with some random values in the interval $I$, whereas an iteration step consists in updating the variable $X$ with the barycentric mean between its current value and the last two selected values. Because of rounding errors, the value associated with the variable $X$ cannot be bounded without considering the clock. Therefore, we can prove that this value is bounded by $[X \mapsto ((1+\epsilon_X+\epsilon_Y+\epsilon_Z) \times X)+\epsilon_0]^{(\text{mc})}(M_I)$, where $M_I$ is the least upper bound of the set $\{|x| \mid x \in I\}$. This bound can be discovered using the arithmetic-geometric domain presented in this paper. It is worth noting that the domains that deal with digital stream processing [6] do not help because the value of the variable $Y$ is not necessarily the previous value of the variable $X$: such domains can only approximate relations of the form $o_n = f(o_{n-1}, \dots, o_{n-p}, i_{n-1}, \dots, i_{n-q})$ where $(i_n)$ is the input stream and $(o_n)$ is the output stream.

**Example 2.** The second example iterates a loop where a floating point is first divided by a coefficient $\alpha > 0$ and then multiplied by the coefficient $\alpha$.

$$ 
\begin{array}{l}
V = \mathbb{R}; B_1 = \mathbb{R}; B_2 = \mathbb{R}; X = 0; \\
\textbf{while } (V \ge 0) \{ \\
\quad V = \mathbb{R}; B_1 = \mathbb{R}; B_2 = \mathbb{R}; \\
\quad \textbf{if } (B_1 \ge 0) \{X = I_1\} \textbf{ else } \textbf{skip}; \\
\quad X = \left[\frac{1}{\alpha} - \epsilon_1; \frac{1}{\alpha} + \epsilon_1\right] \times X + [-\epsilon_2; \epsilon_2]; \\
\quad \textbf{if } (B_2 \ge 0) \{X = I_2\} \textbf{ else } \textbf{skip}; \\
\quad X = [\alpha - \epsilon_3; \alpha + \epsilon_3] \times X + [-\epsilon_4; \epsilon_4]; \\
\quad \textbf{tick} \}
\end{array}
$$

where $\epsilon_i > 0$, for any $i \in \{1; 2; 3; 4\}$, $\alpha > 0$, and $I_1, I_2 \in \mathcal{I}$.

More precisely, initialization values range in the intervals $I_1$ and $I_2$. The parameter $\alpha$ is a coefficient of the example. The parameters $\epsilon_1$ and $\epsilon_3$ encode relative rounding errors and the parameters $\epsilon_2$ and $\epsilon_4$ encode absolute rounding errors. The variable $X$ contains the value that is divided and multiplied. The three variables $V$, $B_1$, and $B_2$ allow boolean control. The variable $V$ allows stopping the loop iteration. The variable $B_1$ allows the reinitialization of the variable $X$ before the division, the variable $B_2$ allows its reinitialization before the multiplication. Because of rounding errors, the value associated with the variable $X$ cannot be bounded without considering the clock. Therefore, we can prove that this value is bounded by $[X \mapsto (1+a) \times X + b]^{(\text{mc})}(M_I)$ where $a = \alpha \times \epsilon_1 + \frac{1}{\alpha} \times \epsilon_3 + \epsilon_1 \times \epsilon_3$ and $b = \epsilon_2 \times (\alpha + \epsilon_3) + \epsilon_4$, and $M_I$ is the least upper bound of the set $\{|x| \mid x \in I_1 \cup A\}$ with $A = \{\frac{y}{\epsilon_1+\frac{1}{\alpha}} \mid y \in I_2\}$. This bound can be discovered using the arithmetic-geometric domain.
### 3 Underlying Domain

We use the Abstract Interpretation framework [3,4,5] to derive a generic approximate semantics. An abstract domain $Env^\#$ is a set of properties about memory states. Each abstract property is related to the set of the environments which satisfy it via a concretization map $\gamma$. An operator $\sqcup$ allows the gathering of information about different control flow paths. The primitives ASSIGN, GUARD, and TICK are sound counterparts to concrete assignments, guards, and clock ticks. To effectively compute an approximation of concrete fixpoints, we introduce an iteration basis $\perp$, a widening operator $\triangleright$, and a narrowing operator $\triangle$. Several abstract domains collaborate and use simple constraints to refine each other. We introduce two domains of simple constraints. The domain of interval $V \cup \{\mathbf{clock}\} \to \mathcal{I}$ and the domain of absolute value ordering $\wp(V^2)$. The interval constraints encoded by a map $\rho^\# \in V \cup \{\mathbf{clock}\} \to \mathcal{I}$ are satisfied by the environment set $\gamma_\mathcal{I}(\rho^\#) = \{\rho \in Env \mid \rho(X) \in \rho^\#(X), \forall X \in V \cup \{\mathbf{clock}\}\}$. The constraints encoded by a subset $\mathcal{R} \subseteq V^2$ are satisfied by the environment set $\gamma_{\text{ABS}}(\mathcal{R}) = \bigcap_{(X,Y) \in \mathcal{R}} \{\rho \in Env \mid |\rho(X)| \le |\rho(Y)|\}$. The primitives RANGE and ABS capture simple constraints about the values that are associated with variables by weakening the abstract elements of $Env^\#$. These constraints are useful in refining the arithmetic-geometric progression domain. Conversely, a primitive REDUCE uses the range constraints that have been computed by the other domains in order to refine the underlying domain.

**Definition 1 (Generic abstraction).** An abstraction is defined by a tuple $(Env^\#, \gamma, \sqcup, \text{ASSIGN}, \text{GUARD}, \text{TICK}, \perp, \triangleright, \triangle, \text{RANGE}, \text{ABS}, \text{REDUCE})$ such that:

1. $Env^\#$ is a set of properties;

2. $\gamma \in Env^\# \to \wp(Env)$ is a concretization map;

3. $\forall a, b \in Env^\#$, $\gamma(a) \cup \gamma(b) \subseteq \gamma(a \sqcup b)$;

4. $\forall a \in Env^\#$, $X \in V, E \in \mathcal{E}, \rho \in \gamma(a), [[X = E]]_{\text{mc}}(\rho) \subseteq \gamma(\text{ASSIGN}(X = E, a));$

5. $\forall a \in Env^\#$, $X \in V \cup \{\mathbf{clock}\}, I \in \mathcal{I}, \{\rho \in \gamma(a) \mid \rho(X) \in I\} \subseteq \gamma(\text{GUARD}(X, I, a));$

6. $\forall a \in Env^\#$, $\{\rho[\mathbf{clock} \mapsto \rho(\mathbf{clock}) + 1] \mid \rho \in \gamma(a)\} \subseteq \gamma(\text{TICK}(a));$

7. $\forall a \in Env^\#$, $\rho^\# \in (V \cup \{\mathbf{clock}\} \to \mathcal{I}), \gamma(a) \cap \gamma_\mathcal{I}(\rho^\#) \subseteq \gamma(\text{REDUCE}(\rho^\#, a));$

8. $\triangleright$ is a widening operator such that: $\forall a, b \in Env^\#$, $\gamma(a) \cup \gamma(b) \subseteq \gamma(a \triangleright b)$; and $\forall k \in \mathbb{N}, \rho_1, \dots, \rho_k \in (V \cup \{\mathbf{clock}\} \to \mathcal{I}), (a_i) \in (Env^\#)^{\mathbb{N}},$ the sequence $(a_i^\triangleright)$ defined by $a_0^\triangleright = r(a_0)$ and $a_{n+1}^\triangleright = r(a_n^\triangleright \triangleright a_{n+1})$ with $r = [X \mapsto \text{REDUCE}(\rho_k, X)] \circ \dots \circ [X \mapsto \text{REDUCE}(\rho_1, X)]$, is ultimately stationary;

9. $\triangle$ is a narrowing operator such that: $\forall a, b \in Env^\#$, $\gamma(a) \cap \gamma(b) \subseteq \gamma(a \triangle b)$; and $\forall k \in \mathbb{N}, \rho_1, \dots, \rho_k \in (V \cup \{\mathbf{clock}\} \to \mathcal{I}), (a_i) \in (Env^\#)^{\mathbb{N}},$ the sequence $(a_i^\triangle)$ defined by $a_0^\triangle = r(a_0)$ and $a_{n+1}^\triangle = r(a_n^\triangle \triangle a_{n+1})$, with $r = [X \mapsto \text{REDUCE}(\rho_k, X)] \circ \dots \circ [X \mapsto \text{REDUCE}(\rho_1, X)]$, is ultimately stationary;

10. $\forall a \in Env^\#$, $\gamma(a) \subseteq \gamma_\mathcal{I}(\text{RANGE}(a))$ and $\gamma(a) \subseteq \gamma_{\text{ABS}}(\text{ABS}(a))$.

Least fixpoint approximation is performed in two steps [4]: we first compute an approximation using the widening operator; then we refine it using the narrowing operator. More formally, let $f$ be a monotonic map in $\wp(Env) \to$
ρ(Env) and (f# ∈ Env# → Env#) be an abstract counterpart of f satisfying
∀a ∈ Env#, (f ◦ γ)(a) ⊑ (γ ◦ f#)(a). It is worth noting that the abstract counterpart f# is usually not monotonic with respect to the partial order ⊑# that is defined by a ⊑# b ⇐⇒ γ(a) ⊑ γ(b). The abstract upward iteration (C_n^v) of f# is defined by C_0^v = ⊥ and C_{n+1}^v = C_n^v ∨ f^#(C_n^v). The sequence (C_n^v) is ultimately stationary and we denote its limit by C_ω^v. Then the abstract downward iteration (D_n^Δ) of f# is defined by D_0^Δ = C_ω^v and D_{n+1}^Δ = D_n^Δ ∩ f^#(D_n^Δ). The sequence (D_n^Δ) is ultimately stationary and we denote its limit by D_ω^Δ. We define<fnref n="2" /> lfp#(f#) by the limit D_ω^Δ of the abstract downward iteration of f#. We introduce some lemmas in order to prove that lfp(f) ⊑ γ(D_ω^Δ):

**Lemma 1.** We have $f(\gamma(C_{\omega}^{\nabla})) \subseteq \gamma(C_{\omega}^{\nabla})$.

*Proof.* Since $C_{\omega}^{\nabla}$ is the limit of the upward-iteration, we have $C_{\omega}^{\nabla} = C_{\omega}^{\nabla} \bigtriangledown f^{\#}(C_{\omega}^{\nabla})$. By Def. 1.(8) of the widening, we obtain that $\gamma(f^{\#}(C_{\omega}^{\nabla})) \subseteq \gamma(C_{\omega}^{\nabla})$. By soundness of $f^{\#}$, we also have $f(\gamma(C_{\omega}^{\nabla})) \subseteq \gamma(f^{\#}(C_{\omega}^{\nabla}))$. So $f(\gamma(C_{\omega}^{\nabla})) \subseteq \gamma(C_{\omega}^{\nabla})$. $\square$

**Lemma 2.** For all $a \in \wp(Env)$ and $x \in Env^{\#}$, we have:

$$a \subseteq \gamma(x) \implies a \cap f(a) \subseteq \gamma(x \Delta f^{\#}(x)).$$

*Proof.* Let $a \in \wp(Env)$ and $x \in Env^{\#}$ such that $a \subseteq \gamma(x)$. Since $f$ is monotonic, we have $f(a) \subseteq f(\gamma(x))$. Then by soundness of $f^{\#}$, we have $f(\gamma(x)) \subseteq \gamma(f^{\#}(x))$. Thus $f(a) \subseteq \gamma(f^{\#}(x))$. So $a \cap f(a) \subseteq \gamma(x) \cap \gamma(f^{\#}(x))$. By Def. 1.(9), we have $\gamma(x) \cap \gamma(f^{\#}(x)) \subseteq \gamma(x \Delta f^{\#}(x))$. We conclude that $a \cap f(a) \subseteq \gamma(x \Delta f^{\#}(x))$. $\square$

**Lemma 3.** For all $a \in \wp(Env)$, we have:

$$f(a) \subseteq a \implies f(f(a) \cap a) \subseteq f(a) \cap a.$$

*Proof.* Let $a \in \wp(Env)$ such that $f(a) \subseteq a$. We have $f(a) \cap a = f(a)$. Since $f$ is monotonic, we have $f(f(a)) \subseteq f(a)$. We conclude that $f(f(a) \cap a) \subseteq f(a) \cap a$. $\square$

**Lemma 4 (transfinite kleenean iteration).** For all $a \in \wp(Env)$, we have:

$$f(a) \subseteq a \implies lfp(f) \subseteq a.$$

**Theorem 1.** We have $lfp(f) \subseteq \gamma(D_{\omega}^{\Delta})$.

*Proof.* We introduce the sequence $(u_n)$ that is defined by $u_0 = \gamma(C_{\omega}^{\nabla})$ and $u_{n+1} = u_n \cap f(u_n)$ for any $n \in \mathbb{N}$. We can prove by induction that $\forall n \in \mathbb{N}$, we have:

1. $u_n \subseteq \gamma(D_n^\Delta)$;

2. $f(u_n) \subseteq u_n$.

<footnote n="2">² lfp#(f#) is an approximation of the concrete least fixpoint; it may not be a least fixpoint of the abstract counterpart f# which is not supposed to be monotonic.</footnote>
$$[V = E]^\sharp_{\text{mc}}(a) = \text{ASSIGN}(V = E, a)$$

$$[\text{skip}]^\sharp_{\text{mc}}(a) = a$$

$$[\text{tick}]^\sharp_{\text{mc}}(a) = \text{GUARD}(\text{clock}, [0; \text{mc}], \text{TICK}(a))$$

$$[\text{if } (V \ge 0) \{P_1\} \text{ else } \{P_2\}]^\sharp_{\text{mc}}(a) = a_1 \sqcup a_2,$$

where $$ \begin{cases} a_1 = [[P_1]]^\sharp_{\text{mc}}(\text{GUARD}(V, [0; +\infty[, a])) \\ a_2 = [[P_2]]^\sharp_{\text{mc}}(\text{GUARD}(V, ]-\infty; 0[, a)) \end{cases} $$

$$[\text{while } (V \ge 0) \{P\}]^\sharp_{\text{mc}}(a) = \text{GUARD}(V, ]-\infty; 0[, \text{Inv}^\sharp),$$

where $\text{Inv}^\sharp = \text{lfp}^\sharp(X \mapsto a \sqcup [[P]]^\sharp_{\text{mc}}(\text{GUARD}(V, [0; +\infty[, X)))$

$$[P_1; P_2]^\sharp_{\text{mc}}(a) = [[P_2]]^\sharp_{\text{mc}}([P_1]^\sharp_{\text{mc}}(a))$$

<caption>**Figure 3.** Abstract semantics.</caption>

- When $n = 0$: by definition, we have $u_0 = \gamma(C_\omega^\nabla) = \gamma(D_0^\Delta)$ and thanks to Lemma 1, we have $f(u_0) \subseteq u_0$.

- We now suppose there exists $n \in \mathbb{N}$ such that $u_n \subseteq D_n^\Delta$ and $f(u_n) \subseteq u_n$.

1. We have $u_{n+1} = u_n \cap f(u_n)$ and $u_n \subseteq \gamma(D_n^\Delta)$. By Lemma 2, we have $u_{n+1} \subseteq \gamma(D_n^\Delta \triangle f^\sharp(D_n^\Delta))$. By definition of $D_{n+1}^\Delta$, we obtain that $u_{n+1} \subseteq \gamma(D_{n+1}^\Delta)$.

2. We have $f(u_{n+1}) = f(u_n \cap f(u_n))$ and $f(u_n) \subseteq u_n$. By Lemma 3, we obtain that $f(u_{n+1}) \subseteq u_{n+1}$.

Then let $n \in \mathbb{N}$ be a natural such that $D_\omega^\Delta = D_n^\Delta$. We have $u_n \subseteq \gamma(D_\omega^\Delta)$ and $f(u_n) \subseteq u_n$. By lemma 4, we have $\text{lfp}(f) \subseteq \gamma(D_\omega^\Delta)$. $\square$

The abstract semantics of a program is given by a function $([\text{ ]}]^\sharp_{\text{mc}} \in \text{Env}^\sharp \to \text{Env}^\sharp)$ in Fig. 3. Its soundness can be proved by induction on the syntax:

**Theorem 2.** For any program *P*, environment $\rho$, abstract element *a*, and maximum clock value *mc*, we have:

$$\rho \in \gamma(a) \implies [[P]]_{\text{mc}}(\rho) \subseteq \gamma(\llbracket P \rrbracket_{\text{mc}}^\sharp(a)).$$

# 4 Arithmetic-geometric progressions

## 4.1 Affine transformations

We introduce, as follows, the family of the affine transformations ($f[a, b]$) that is indexed by two non-negative real parameters $a$ and $b$:

$$f[a, b] : \begin{cases} \mathbb{R}^+ \to \mathbb{R}^+ \\ X \mapsto a \times X + b \end{cases}$$

**Lemma 5.** Let $a_1, a_2, b_1, b_2, X_1, X_2$ be non-negative real numbers in $\mathbb{R}^+$. If $a_1 \le a_2, b_1 \le b_2$, and $X_1 \le X_2$, then $f[a_1, b_1](X_1) \le f[a_2, b_2](X_2)$.
## 4.2 Arithmetic-geometric progression in the real field

We introduce the predomain $D_R$ of all the 5-tuples of non-negative real numbers. The predomain $D_R$ is ordered by the product order $\subseteq_{D_R}$. Intuitively,<fnref n="3" /> an element $(M, a, b, a', b')$ of this predomain encodes an arithmetic-geometric progression. The real $M$ is a bound on the initial value of the progression. The affine transformation $f[a', b']$ over-approximates the composition of all the affine transformations that can be applied to a value between two consecutive clock ticks. Finally, the affine transformation $f[a, b]$ over-approximates the composition of all the affine transformations that have been applied to a value since the last clock tick.

Thus, given a clock value $vc \in \mathbb{N}$, we can define the concretization $\gamma_{D_R}^{vc}(d)$ of such a tuple $d = (M, a, b, a', b') \in D_R$ by the set of all the elements $X \in \mathbb{R}$ such that $|X| \le f[a, b] ((f[a', b'])^{(vc)}(M))$. We now define some primitives to handle the elements of $D_R$:

1. The join operator $\sqcup_{D_R}$ applies the maximum function component-wise. The soundness of the operator $\sqcup_{D_R}$ is established by Thm. 3, as follows:

**Theorem 3.** For any $vc \in \mathbb{N}$,

$$ \gamma_{D_R}^{vc}(d_1) \cup \gamma_{D_R}^{vc}(d_2) \subseteq \gamma_{D_R}^{vc}(d_1 \sqcup_{D_R} d_2). $$

*Proof.* By Lem. 5. □

<figure><img src="image_4.png" /></figure>

2. The primitive affine$_{D_R}$ computes a linear combination among some elements of $D_R$. Let $n \in \mathbb{N}^*$ be a positive natural,<fnref n="4" /> let $(d_i) = (M_i, a_i, b_i, a'_i, b'_i) \in D_R^n$ be a family of elements in $D_R$, let $(\alpha_i) \in (\mathbb{R} \setminus \{0\})^n$ be a family of real coefficients that are all distinct from 0, and let $\beta \in \mathbb{R}$ be a real coefficient. We define the element affine$_{D_R}$((αᵢ, dᵢ), β) ∈ $D_R$ by $(g(M_i), a_\infty \times \alpha', |\beta| + g(b_i), a'_\infty, g(b'_i))$ where:

$$ - a_{\infty} = \max\{|a_i| \mid 1 \le i \le n\}, a'_{\infty} = \max\{|a'_i| \mid 1 \le i \le n\}, $$

$$ - \alpha' = \sum_{1 \le i \le n} |\alpha_i| \text{ and} $$

$$ - \text{the function } g : \mathbb{R}^n \to \mathbb{R} \text{ maps each family } (x_i) \text{ of } n \text{ real numbers into} \\ \text{the real number defined by } \sum_{1 \le i \le n} \frac{|\alpha_i \times x_i|}{\alpha'}. $$

The soundness of the primitive affine$_{D_R}$ is established by Thm. 4, as follows:

**Theorem 4.** Let $vc \in \mathbb{N}$ be a natural and $(X_i) \in \mathbb{R}^n$ be a non-empty family of reals such that for any $i$ such that $1 \le i \le n$, we have $X_i \in \gamma_{D_R}^{vc}(d_i)$. Then we have:

$$ \left( \sum_{1 \le i \le n} \alpha_i \times X_i + \beta \right) \in \gamma_{D_R}^{vc} (\text{affine}_{D_R}((\alpha_i, d_i), \beta)). $$

<footnote n="3">³ In Sect. 6 we forget this intuition to get a more expressive domain.</footnote>

<footnote n="4">⁴ The approximation of affine constants has an ad-hoc handling (Cf. Sect. 5.3).</footnote>
*Proof.* By Lemma 5, by replacing $\alpha_i$ with $\frac{\alpha' \times \alpha_i}{\alpha'}$, by expanding $f[a, b]^{(vc)}$, and by applying the triangular inequality. $\square$

3. The primitive $\text{TICK}_{D_R} \in D_R \to D_R$ simulates clock ticks. It maps any element $d = (M, a, b, a', b') \in D_R$ into the element $(M, 1, 0, \max(a, a'), \max(b, b')) \in D_R$. Thus, just after the clock tick, the arithmetic-geometric progression that has been applied since the last clock tick is the identity. The progression between two clock ticks is chosen by applying the worst case among the progression between the last two clock ticks, and the progression between any other two consecutive clock ticks. The soundness of this operator is established by Thm. 5 as follows:

**Theorem 5 (clock tick).** Let $vc \in \mathbb{N}$ be a natural. Then we have:

$$ \gamma_{D_R}^{vc}(d) \subseteq \gamma_{D_R}^{vc+1}(\text{TICK}_{D_R}(d)) $$

*Proof.* By Lemma 5. $\square$

For the sake of accuracy, we get a more precise definition of the primitive $\text{TICK}_{D_R}$ in Sect. 6, by forgetting the intuitive meaning of the elements of $D_R$.

4. The primitive $range_{D_R} \in (D_R \times \{[a; b] | a, b \in \mathbb{N}, a \le b\}) \to \mathcal{I}$ associates an element of $D_R$ and an interval for the clock counter with an interval range: we define $range_{D_R}((M, a, b, a', b'), [m_{vc}; M_{vc}])$ by $[-l; l]$ where $l = \max(u_{m_{clock}}, u_{M_{clock}})$ and for any $vc \in \mathbb{N}$,

$$ u_{vc} = \begin{cases} a \times (M + vc \times b') + b & \text{if } a' = 1, \\ a \times (a'^{vc} \times (M - \frac{b'}{1-a'}) + \frac{b'}{1-a'}) + b & \text{otherwise.} \end{cases} $$

The soundness of the primitive $range_{D_R}$ is established in Thm. 6 as follows:

**Theorem 6.** For any $vc \in \mathbb{N}$ such that $m_{vc} \le vc \le M_{vc}$, we have:

$$ \gamma_{D_R}^{vc}(d) \subseteq range_{D_R}(d, [m_{vc}; M_{vc}]). $$

*Proof.* By studying the sign of $(u_{n+1} - u_n)$, for any $n \in \mathbb{N}$. $\square$

## 4.3 Representable real numbers

Until now, we have only used real numbers. In order to implement numerical abstract domains, we use a finite subset $\mathbb{F}$ of real numbers (such as the floating-point numbers) that contains the set of numbers $\{0, 1\}$ and that is closed under negation. The set $\overline{\mathbb{F}}$ is obtained by enriching the set $\mathbb{F}$ with two extra elements $+\infty$ and $-\infty$ that respectively describe the reals that are greater (resp. smaller) than the greatest (resp. smallest) element of $\mathbb{F}$. We denote the set $\{x \in \mathbb{F} | x \ge 0\}$ by $\mathbb{F}^+$ and the set $\mathbb{F}^+ \cup \{+\infty\}$ by $\overline{\mathbb{F}}^+$. The result of a computation on elements of $\overline{\mathbb{F}}$ may be not in $\overline{\mathbb{F}}$. So we suppose that we are given a function $[-] \in \mathbb{R} \to \overline{\mathbb{F}}$ such that $[x] \ge x$, for any $x \in \mathbb{R}$ and such that $[x] \le 0$, for any $x \le 0$. The domain $\overline{\mathbb{F}}$ is related to $\wp(\mathbb{R})$ via the concretization $\gamma_{\overline{\mathbb{F}}}$ that maps any representable number $e$ into the set of the reals $r \in \mathbb{R}$ such that $|r| < e$, moreover we set $\gamma_{\overline{\mathbb{F}}}(+\infty) = \mathbb{R}$ and $\gamma_{\overline{\mathbb{F}}}(-\infty) = \emptyset$.
## 4.4 Representable arithmetic-geometric constraints

We introduce the predomain $D_F$ as the set of the 5-tuples $(M, a, b, a', b') \in (\bar{\mathbb{F}}^+)^5$. The order $\sqsubseteq_{D_F}$, the concretizations $\gamma_{D_F}^{\text{vc}}$ (for any $\text{vc} \in \mathbb{N}$), the join operator $\sqcup_{D_F}$, and the clock tick primitive $\text{TICK}_{D_F}$ are respectively defined as restrictions of the order $\sqsubseteq_{D_R}$, the concretizations $\gamma_{D_R}^{\text{vc}}$, the join operator $\sqcup_{D_R}$, and the primitive $\text{TICK}_{D_R}$.

We now update the definition of the linear combination primitive $\text{affine}_{D_F}$ and of the reduction primitive $\text{range}_{D_F}$:

1. The primitive $\text{affine}_{D_F}$ maps each pair $((\alpha_i, d_i), \beta)$ where $(\alpha_i) \in \mathbb{R}^n$ (where $n \in \mathbb{N}^*$ is a positive natural), $(d_i) = ((M_i, a_i, b_i, a'_i, b'_i)) \in D_F^n$, and $\beta \in \mathbb{R}$ to the element:

$$ (g(M_i), \lceil a_{\infty} \times \alpha'_{M} \rceil, |\beta| + g(b_i), a'_{\infty}, g(b'_i)) $$

where:

$$ - a_{\infty} = \max\{|a_i| \mid 1 \le i \le n\}, a'_{\infty} = \max\{|a'_i| \mid 1 \le i \le n\}, $$

$$ - s_n : \mathbb{R}^n \to \bar{\mathbb{F}}^+ \text{ is defined by } s_0(()) = 0 \text{ and } s_{n+1}((a_i)_{1 \le i \le n+1}) = \lceil s_n((a_i)_{1 \le i \le n}) + \lceil a_{n+1} \rceil \rceil. $$

$$ - \alpha'_m = -s_n((-|\alpha_i|)_{1 \le i \le n}), \alpha'_M = s_n((|\alpha_i|)_{1 \le i \le n}), $$

$$ - g : \mathbb{R}^n \to \bar{\mathbb{F}}^+ \text{ maps each family } (x_i) \text{ of real numbers into the real number that is defined by} $$

$$ \min \left( \max(\{|x_i| \mid 1 \le i \le n\}), s_n \left( \frac{\lceil |\alpha_i| \times |x_i| \rceil}{\alpha'_m} \right) \right). $$

**Theorem 7.** For any clock value $\text{vc} \in \mathbb{N}$, we have:

$$ \left\{ \sum_{1 \le i \le n} \alpha_i \times X_i + \beta \mid X_i \in \gamma_{D_F}^{\text{vc}}(d_i) \right\} \subseteq \gamma_{D_F}^{\text{vc}}(\text{affine}_{D_F}((\alpha_i, d_i), \beta)). $$

*Proof.* By Lemma 5 and Thm. 4. $\square$

<figure><img src="image_5.png" /></figure>

**Remark 1.** We define $g$ as the minimum of two sound results. In the real field, the second one is more precise. However, it may become less precise when computing with rounding errors.

2. The interval $\text{range}_{D_F}((M, a, b, a', b'), [m_{\text{vc}}, M_{\text{vc}}])$ is given by $[-l; l]$ where:

$$ - l = \max(u_{m_{\text{vc}}}, u_{M_{\text{vc}}}); $$

$$ - u_{\text{vc}} = \lceil [a \times v_{\text{vc}}] + b \rceil; $$

$$ - v_{\text{vc}} = \begin{cases} \lceil M + \text{vc} \times b' \rceil & \text{if } a' = 1, \\ [c_1^+ + c_2^+] & \text{otherwise;} \end{cases} $$

$$ - \begin{cases} \exp_0^- = 1, \exp_{2 \times n}^- = -\lceil \exp_n^- \times (-\exp_n^-) \rceil, \\ \exp_{2 \times n+1}^- = -\lceil \exp_n^- \times (-\exp_n^-) \rceil \times a' \end{cases}; $$

$$ - \begin{cases} \exp_0^+ = 1, \exp_{2 \times n}^+ = \lceil \exp_n^+ \times \exp_n^+ \rceil, \\ \exp_{2 \times n+1}^+ = \lceil \exp_n^+ \times \exp_n^+ \rceil \times a' \end{cases}; $$
$$ -c_1^+ = \begin{cases} \lceil \exp_{vc}^+ \times [M - c_2^-] \rceil & \text{if } M \ge c_2^- \\ \lceil \exp_{vc}^- \times [M - c_2^-] \rceil & \text{otherwise;} \end{cases} \\ -c_2^- = - \left\lceil \frac{-b'}{|1-a'|} \right\rceil \text{ and } c_2^+ = \left\lceil \frac{-b'}{|a'-1|} \right\rceil. $$

**Theorem 8.** For any clock value vc ∈ [m<sub>vc</sub>; M<sub>vc</sub>], we have:

$$ \gamma_{\mathcal{D}_F}^{vc}(d) \subseteq \text{range}_{\mathcal{D}_F}(d, vc). $$

*Proof.* Because $\forall vc \in \mathbb{N}$, $\exp_{vc}^- \le a'^{vc} \le \exp_{vc}^+$, $c_1^+ \ge a'^{vc} \times (M - \frac{b'}{1-a'})$ and $c_2^- \le \frac{b'}{1-a'} \le c_2^+$, and by applying Thm. 6. $\square$

*Remark 2.* In the implementation, we use memoization to avoid computing the same exponential twice.

## 4.5 Tuning the extrapolation strategy

Although $\overline{\mathbb{F}}$ is height-bounded, we introduce some extrapolation operators in order to accelerate the convergence of abstract iterations. A widening step consists in applying an extensive map to each unstable components of the 5-tuples. In order to let constraints stabilize, we only widen a component when it has been unstable a given number of times since its last widening. For that purpose, we associate each representable number in $\overline{\mathbb{F}}$ with a natural that denotes the number of times it has been unstable without being widened. We suppose that we are given a natural parameter $n$ and an extensive function $f$ over $\overline{\mathbb{F}}$. We first define the widening $\nabla_f^n$ of two annotated representable numbers $(x_1, n_1)$, $(x_2, n_2) \in \overline{\mathbb{F}} \times \mathbb{N}$ by:

$$ (x_1, n_1) \nabla_f^n (x_2, n_2) = \begin{cases} (x_1, n_1) & \text{if } x_1 \ge x_2 \\ (x_2, n_1 + 1) & \text{if } x_1 < x_2 \text{ and } n_1 < n \\ (f(x_2), 0) & \text{otherwise.} \end{cases} $$

A narrowing step refines an arithmetic-geometric constraint with another one if the last one is smaller component-wise (so that we are sure that this refinement does not locally lose accuracy). To avoid too long decreasing sequences, we count the number of times such a refinement has been applied with each constraint. Thus we associate each constraint with an extra counter.

We then introduce the predomain $D_{\overline{\mathbb{F}}}^{\mathcal{L}} = (\overline{\mathbb{F}}^+ \times \mathbb{N})^5 \times \mathbb{N}$ of annotated constraints. The function *Annotate* maps each element $d = (M, a, b, a', b') \in D_{\overline{\mathbb{F}}}$ to the annotated element that is defined by (((*M*, 0), (*a*, 0), (*b*, 0), (*a'*, 0), (*b'*, 0)), 0) ∈ $D_{\overline{\mathbb{F}}}^{\mathcal{L}}$, where all counters are initialized with the value 0. Conversely the function *remove* maps each element (((*M*, *n*<sub>*M*</sub>), (*a*, *n*<sub>*a*</sub>), (*b*, *n*<sub>*b*</sub>), (*a'*, *n*<sub>*a*</sub>'), (*b'*, *n*<sub>*b*</sub>)), *n*) ∈ $D_{\overline{\mathbb{F}}}^{\mathcal{L}}$ to the annotation-free element (*M*, *a*, *b*, *a'*, *b*') ∈ $D_{\overline{\mathbb{F}}}$. We can define the preorder $\sqsubseteq_{D_{\overline{\mathbb{F}}}^{\mathcal{L}}}$ by $a \sqsubseteq_{D_{\overline{\mathbb{F}}}^{\mathcal{L}}} b \iff \text{remove}(a) \sqsubseteq_{D_{\overline{\mathbb{F}}}} \text{remove}(b)$. The monotonic concretization $\gamma_{D_{\overline{\mathbb{F}}}^{\mathcal{L}}}$ is defined as the composition $\gamma_{D_{\overline{\mathbb{F}}}} \circ \text{remove}$.

Extrapolation operators store information about the history of the extrapolation process into the counters of their left argument, whereas the other primitives
reset these counters: we define the union $a \sqcup_{D_F^c} b$ by ` annotate((remove(a)) \sqcup_{D_F} (remove(b)))`, the affine combination `affine_{D_F^c}((\alpha_i, d_i), \beta)` by the abstract element ` annotate(affine_{D_F}((\alpha_i, remove(d_i)), \beta))`, the abstract clock tick primitive `TICK_{D_F^c}` by the map ` annotate \circ TICK_{D_F} \circ remove`, and the interval constraints `range_{D_F^c}(d, I)` by the interval map `range_{D_F}(remove(d), I)`.

We define extrapolation operators. Let $f_a, f_b$, and $f_M$ be extensive functions over the set $\overline{\mathbb{F}}$; let $n_a, n_b, n_M$, and $n$ be some naturals. The functions $f_a, f_b$, and $f_M$ and the naturals $n_a, n_b, n_M$, and $n$ are left as parameters of our extrapolation strategy. The widening $((M_1, a_1, b_1, a'_1, b'_1), n_1) \triangledown_{D_F^c} ((M_2, a_2, b_2, a'_2, b'_2), n_2)$ is defined by $((M_1 \triangledown_{f_M}^{n_M} M_2, a_1 \triangledown_{f_a}^{n_a} a_2, b_1 \triangledown_{f_b}^{n_b} b_2, a'_1 \triangledown_{f_a}^{n_a} a'_2, b'_1 \triangledown_{f_b}^{n_b} b'_2), 0)$. The narrowing $(t_1, n_1) \triangleq_{D_F^c} (t_2, n_2)$ is then defined by $(t_2, n_1 + 1)$ in the case when $n_1 < n$ and $(t_2, n_2) \sqsubseteq_{D_F^c} (t_1, n_1)$, and by $(t_1, n_1)$ otherwise.

# 5 Refining an existing abstraction

We now show how we can extend an existing abstraction defined as in Def. 1 so that it can also deal with arithmetic-geometric constraints.

## 5.1 Domain extension

Let $(Env_0^\sharp, \gamma_0, \sqcup_0, ASSIGN_0, GUARD_0, TICK_0, \perp_0, \triangledown_0, \Delta_0, RANGE_0, ABS_0, REDUCE_0)$ be an abstraction which is called the underlying domain. We build the abstraction $Env^\sharp$ as the Cartesian product $Env_0^\sharp \times (\mathcal{V} \to D_F^c \cup \{\top\})$. The element $\top \notin D_F^c$ denotes the absence of constraint. The concretization $\gamma: Env^\sharp \to \wp(Env)$ maps each pair $(e, f)$ to the following set of environments:

$$ \gamma_0(e) \cap \{ \rho \in Env \mid \forall X \in \mathcal{V} \text{ such that } f(X) \neq \top, \rho(X) \in \gamma_{D_F^c}^{\rho(\text{clock})}(f(X)) \}. $$

Moreover, abstract iterations start with the element $\perp = (\perp_0, [X \mapsto \top])$.

## 5.2 Refinement operators

The underlying domain and the arithmetic-geometric domain refine each other when the computation of an abstract primitive requires it. We introduce here some operators that describe these refinement steps.

The operator $r^- \llcorner$ uses the arithmetic-geometric constraints to refine the underlying domain. Given an abstract element $(e, f) \in Env^\sharp$ and a subset $V \subseteq \mathcal{V}$ of variables, we define $r^-((e, f), V)$ by $(REDUCE_0(g, e), f)$ where $g(X)$ is given by:

$$ \begin{cases} \text{range}_{D_F^c}(f(X), \text{RANGE}_0(e)(\text{clock})) & \text{if } X \in V \text{ and } f(X) \neq \top, \\ \mathbb{R} & \text{otherwise.} \end{cases} $$

Conversely, we use the underlying domain to build new arithmetic-geometric constraints or to refine existing arithmetic-geometric constraints. Let $X \in \mathcal{V}$
be a variable, let $a, b \in \mathbb{F}^+$ be two non negative real parameters, and let $e \in \text{Env}_0^\sharp$ be an abstract element of the underlying domain. The variable $X$ can soundly be associated with the arithmetic-geometric constraint $g_e(X, (a, b))$, where $g_e(X, (a, b))$ is given by:

$$ \left\{ \begin{array}{ll} \text{ annotate} \left( \left( \left\lfloor \frac{\max(0, \lfloor l-b \rfloor)}{a} \right\rfloor, a, b, 1, 0 \right) \right) & \text{if } a \neq 0, \\ \text{ annotate}((a, b, 1, 0, l)) & \text{otherwise,} \end{array} \right. $$

where $l \in \bar{\mathbb{F}}$ is the least upper bound (in $\bar{\mathbb{F}}$) of the set $\{|x| \mid x \in \text{RANGE}_0(e)(X)\}$.

We now define the operator $r^-$ which refines arithmetic-geometric constraints over a set of variables by weakening the range constraints that can be extracted from the underlying domain. Given an abstract element $(e, f) \in \text{Env}^\sharp$, a subset $A \subseteq \mathcal{V}$, and a map $\Gamma \in A \to \mathbb{F}^+ \times \mathbb{F}^+$, we define $r^→((e, f), A, \Gamma)$ by $(e, f')$ where $f'(X)$ is defined by:

$$ \left\{ \begin{array}{ll} g_e(X, \Gamma(X)) & \text{if } X \in A \text{ and either } f(X) = \top, \text{ or } g_e(X, \Gamma(X)) \subseteq_{\mathcal{D}_F^\mathcal{L}} f(X), \\ f(X) & \text{otherwise.} \end{array} \right. $$

## 5.3 Primitives

Binary operators are all defined in the same way. Let $\otimes$ be an operator in $\{\sqcup, \Delta, \nabla\}$ and let $(e_1, f_1), (e_2, f_2)$ be two abstract elements of $\text{Env}^\sharp$. Before applying a binary operator, we refine arithmetic-geometric constraints so that both arguments constrain the same set of variables: we set for any $i \in \{1, 2\}$, $(e'_i, f'_i) = (r^→((e_i, f_i), V_{3-i} \setminus V_i, \Gamma_{3-i}))$, where for any $i \in \{1; 2\}$, $V_i = \{X \mid f_i(X) \neq \top\}$ and $\Gamma_i(X) = (a, b)$ when $f_i(X)$ matches $(M, a, b, a', b')$. We then apply $\otimes$ component-wise: we set $e'' = e'_1 \otimes_0 e'_2$; we set $f''(X) = f'_1(X) \otimes_{\mathcal{D}_F^\mathcal{L}} f'_2(X)$ for any $X \in V_1 \cup V_2$; we set $f''(X) = \top$ for any $X \in \mathcal{V} \setminus (V_1 \cup V_2)$. After applying a binary operator, we use the arithmetic-geometric constraints to refine the underlying domain: we define $(e_1, f_1) \otimes (e_2, f_2)$ by $r^→((e'', f''), \mathcal{V})$.

We use a heuristics to drive the abstraction of assignments. This heuristics weakens the precondition to simplify the assigned expression: it takes some variable ranges, some arithmetic-geometric constraints and an expression; it replaces in the expression some variables with their range. The choice of the variables that are replaced is left as a parameter of the abstraction. Thus, the heuristics $\text{heu} \in ((\mathcal{V} \cup \{\text{clock}\} \to \mathcal{I}) \times (\mathcal{V} \to \mathcal{D}_F^\mathcal{L} \cup \{\top\})) \times \mathcal{E} \to ((\mathbb{R} \setminus \{0\} \times \mathcal{V})^* \times \mathbb{R})$ maps each pair $((\rho^\sharp, f), E)$ to a pair $((\alpha_i, V_i)_{1 \le i \le n}, \beta)$ that satisfies:

$$ \gamma(\lfloor E \rfloor) \subseteq \left\{ \beta + \sum_{1 \le i \le n} \alpha_i \times \rho(V_i) \;\middle|\; \begin{array}{l} \forall \rho \in \text{Env} \text{ such that:} \\ \forall X \in \mathcal{V}, \rho(X) \in \rho^\sharp(X) \cap \gamma_{\mathcal{D}_F^\mathcal{L}}^{\rho(\text{clock})}(f(X)) \\ \text{and } \rho(\text{clock}) \in \rho^\sharp(\text{clock}) \end{array} \right\}. $$

Let $(e, f) \in \text{Env}^\sharp$ be an abstract element. We consider several cases when abstracting an assignment $X = E$:
1. When computing an assignment $X = Y$ with $Y \in \mathcal{V}$, we associate the variable $X$ with any constraint about $Y$. Thus we set:

$$ \text{ASSIGN}(X = Y, (e, f)) = (\text{ASSIGN}_0(X = Y, e), f[X \mapsto f(Y)]); $$

2. When computing an assignment $X = E$ where $E \notin \mathcal{V}$ such that the pair $heu((\text{RANGE}_0(e), f), E)$ matches $((), \beta)$, we remove any arithmetic-geometric constraints about $X$. Thus we set:

$$ \text{ASSIGN}(X = E, (e, f)) = (\text{ASSIGN}_0(X = E, e), f[X \mapsto \top]); $$

3. Otherwise, we denote by $((\alpha_i, V_i)_{1 \le i \le n}, \beta) = heu((\text{RANGE}_0(e), f), E)$ the approximation of $E$ by the heuristics. Before the assignment, we use the underlying domain to refine information about the variables $(V_i)$ that occur in the simplified expression. When such a variable is tied with no arithmetic-geometric constraint, we build one with arbitrary coefficients for the affine transformations. We also refine existing constraints without modifying the coefficients of the affine transformations. Thus we define the element $(e', f')$ by $r^-(((e, f), \{V_i \mid 1 \le i \le n\}, \Gamma))$ where for any $i \in \mathbb{N}$ such that $1 \le i \le n$, we have $\Gamma(V_i) = (1, 0)$ if $f(V_i) = \top$ (missing constraints) and $\Gamma(V_i) = (a, b)$ if $f(V_i) = (M, a, b, a', b')$ (existing constraints). Then we apply the assignment component-wise: we define $(e'', f'')$ by $(\text{ASSIGN}_0(X = E, e'), f[X \mapsto \text{affine}_{D_F^\mathcal{L}}((\alpha_i, f'(V_i)), \beta)])$. At last, we refine the underlying domain by the new computed constraint: we set $\text{ASSIGN}(X = E, (e, f)) = r^-((e'', f''), \{X\})$.

The abstraction of a clock tick $\text{TICK}(e, f)$ is defined component-wise by $(\text{TICK}_0(e), f')$ where $f'(X) = \text{TICK}_{D_F^\mathcal{L}}(f(X))$ if $f(X) \neq \top$ and $f'(X) = \top$ otherwise. We do not deal directly with guards in the arithmetic-geometric domain. Nevertheless, if after applying a guard, we can prove in the underlying domain that the absolute value that is associated with a variable is less than the absolute value that is associated with another variable, we use this information to refine arithmetic-geometric constraints. So we define the primitive $r^{\text{ABS}}$ that refines arithmetic-geometric constraints, according to absolute value constraints. Given a relation $\mathcal{R} \subseteq \mathcal{V}^2$ and a map $f \in \mathcal{V} \to \mathcal{D}_F^\mathcal{L} \cup \{\top\}$, the map $r^{\text{ABS}}(\mathcal{R}, f) \in \mathcal{V} \to \mathcal{D}_F^\mathcal{L} \cup \{\top\}$ associates any variable $X$ with a minimal element (for $\subseteq_{\mathcal{D}_F^\mathcal{L}}$) of the set $(\{f(X)\} \cup \{f(Y) \mid (X, Y) \in \mathcal{R}\} \setminus \{\top\})$ if this set is not empty, or with the element $\top$ otherwise. Then the abstract element $\text{GUARD}(X, I, (a, f))$ is defined by $(\text{GUARD}_0(X, I, a), r^{\text{ABS}}(\text{ABS}_0(\text{GUARD}_0(X, I, a)), f))$.

In order not to break the extrapolation process, we never refine arithmetic-geometric constraints after applying an extrapolation operator. Thus we define $\text{REDUCE}(\rho^\#(e, f))$ by $(\text{REDUCE}_0(\rho^\#(e), f))$. Moreover, the domain $\mathcal{D}_F^\mathcal{L}$ cannot help in comparing the absolute value of variables, so we set $\text{ABS}(e, f) = \text{ABS}_0(e)$. Nevertheless, the domain $\mathcal{D}_F^\mathcal{L}$ can refine variable range: we set $\text{RANGE}(e, f)(X)$ by $\text{RANGE}_0(e)(X) \cap \text{range}_{\mathcal{D}_F^\mathcal{L}}(f(X), \text{RANGE}_0(e)(\text{clock}))$.

**Theorem 9.** $(\text{Env}^\#(e), \gamma, \square, \text{ASSIGN}, \text{GUARD}, \text{TICK}, \perp, \nabla, \Delta, \text{RANGE}, \text{ABS}, \text{REDUCE})$ is an abstraction.
*Proof.* We sketch the proof of Th. 9: all soundness requirements come from the soundness of both the underlying domain and the arithmetic-geometric pre-domain. During an extrapolation iteration (ascending or descending), the set of arithmetic-geometric constraints (i.e., the set of the variables that are not mapped into $\top$) is ultimately stationary (since the number of constraints is increasing, whereas $\mathcal{V}$ is finite); then each arithmetic-geometric constraint sequence is ultimately stationary; once the information that refines the underlying domain is fixed, the underlying domain termination criteria in Def. 1.(8-9) apply. □

# 6 Dealing with buffers

The definition of the primitive $TICK_{D_F}$ in Sect. 4.4 implicitly supposes that the affine transformations that must be captured are fully computed between two clock ticks. For instance, Ex. 2 can be analyzed accurately because the multiplication and the division are computed in the same loop iteration. We first slightly modify Ex. 2 so that this atomicity assumption is not satisfied. Then we refine the primitive $TICK_{D_F}$ to handle more complex cases precisely.

## 6.1 Motivating example

*Example 3.* This example iterates a loop where a floating point is first divided by a coefficient $\alpha > 2$ and then multiplied by the coefficient $\alpha$. Unlike Ex. 2, the division and the multiplication are not computed in the same iteration of the loop. At each iteration, the current value of $X$ is multiplied by $\alpha$ and the result is stored in a buffer (denoted by the variable `BUFFER`). The next value for $X$ is obtained by dividing the value that was in the buffer at the beginning of the iteration (while the current value of $X$ is stored in a temporary variable `TMP`). For the sake of simplicity, we have removed reinitialization branches.

$$ 
\begin{array}{l}
V = \mathbb{R}; X = I; \text{TMP} = 0; \text{BUFFER} = I; \\
\textbf{while } (V \ge 0) \{ \\
\quad V = \mathbb{R}; \\
\quad \text{TMP} = X; \\
\quad X = \left[ \frac{1}{\alpha} - \varepsilon_1; \frac{1}{\alpha} + \varepsilon_1 \right] \times \text{BUFFER} + [-\varepsilon_2; \varepsilon_2]; \\
\quad \text{BUFFER} = [\alpha - \varepsilon_3; \alpha + \varepsilon_3] \times \text{TMP} + [-\varepsilon_4; \varepsilon_4]; \\
\quad \text{tick} \}
\end{array}
$$

where $0 < \varepsilon_i < 1$, for any $i \in \{1; 2; 3; 4\}$, $\alpha > 2$, and $I \in \mathcal{I}$.

Moreover, initialization values range in the intervals $I$. The parameter $\alpha$ is a coefficient in the example. The parameters $\varepsilon_1$ and $\varepsilon_3$ encode relative rounding errors, and the parameters $\varepsilon_2$ and $\varepsilon_4$ encode absolute rounding errors. The variable $V$ allows stopping the loop iteration.

At the first abstract iteration, before the first clock tick, the variable `BUFFER` is associated with the 5-tuple $(M_1, a_1, b_1, 1, 0)$ where $M_I$ is the least upper bound of the set $\{|x| \mid x \in I\}$, $a_1 = \lceil \alpha + \varepsilon_3 \rceil$ and $b_1 = \lceil \varepsilon_4 \rceil$. After the first clock tick, it is associated with $(M_1, 1, 0, a_1, b_1)$. At the second abstract iteration, before
the clock tick, the variable *X* is associated with the 5-tuple (*M*₁, *a*₂, *b*₂, *a*₁, *b*₁) where *a*₂ = [1/α + ε₁] and *b*₂ = [ε₂]. After the second clock tick, the variable *X* is associated with the 5-tuple (*M*₁, 1, 0, *a*₁, max(*b*₁, *b*₂)). We notice that the arithmetic-geometric domain cannot help in bounding the range of the variable *X* because of the computation of the exponential (since we have *a*₁ > 2). All information has been lost when computing the first clock tick in the abstract.

## 6.2 Refining the domain

To refine the domain, we have to decide at each clock tick which affine computations are finished. For that purpose, we introduce two parameters $\beta_m, \beta_M \in \mathbb{F}^+$ very close to 1 and such that $\beta_m < 1 < \beta_M$. We then consider that an affine transformation $[X \mapsto a \times X + b]$ denotes a finished computation if and only if $\beta_m < a < \beta_M$. In fact, in the case when $a > \beta_M$ the arithmetic-geometric progression domain will provide useless range and in the case when $a < \beta_m$ the interval domain can provide accurate range by using widening and narrowing. Thus, we redefine the element $\text{TICK}_{\mathbb{D}_F}(M, a, b, a', b')$ by $(M, a, 0, a', \max\{b, b'\})$ in the case when both $a \notin [\beta_m; \beta_M]$ and $a' \ge 1$, and by $(M, 1, 0, \max\{a, a'\}, \max\{b, b'\})$ otherwise. This definition still satisfies Thm. 5.

In Ex. 3, after the first clock tick and provided that $a_1 < \beta_m$, the variable BUFFER is now associated with $(M_1, a_1, 0, 1, b_1)$. At the second abstract iteration, before the clock tick the variable *X* is associated with the 5-tuple $(M_1, a_3, b_3, 1, b_1)$ where $a_3 = [[\alpha + \varepsilon_3] \times a_1]$ and $b_3 = \varepsilon_3$. Then after the second clock tick and provided that $a_3 < \beta_M$, the variable *X* is associated with $(M_1, 1, 0, a_3, \max(b_1, b_3))$. This constraint is stable and allows the computation of an accurate range for the variable *X*.

# 7 Benchmarks

We tested our framework with three programs of a same family of critical embedded software written in C. For each program we tested the ASTRÉE [2] analyzer with the classical domains (intervals [4], octagons [8], decision trees, and expanded digital filter domains [6]) and without/with the new arithmetic-geometric domain. For each of these analyses, we report in Fig. 4 the analyzed program size, the number of global variables, the number of arithmetic-geometric constraints that are captured by the analysis, the analysis time, the number of iterations for the main loop, and the number of warnings (in polyvariant function calls). These results have been obtained on a AMD Opteron 248, with 8 Gb of RAM. In two of the three programs, the arithmetic-geometric progression domain solve all the remaining false alarms which gives a proof of absence of run-time errors.

# 8 Conclusion

We have proposed a new numerical domain which relates the value of each variable to a clock counter. It approximates each value by an expression of the form
<table><caption>**Figure 4.** Some statistics.</caption><thead><tr><th></th><th>70,000</th><th>216,000</th><th>379,000</th></tr></thead><tbody><tr><td>lines of C</td><td></td><td></td><td></td></tr><tr><td>global variables</td><td>13,400</td><td>7,500</td><td>9,000</td></tr><tr><td>ari-geo progressions</td><td>disabled</td><td>enabled</td><td>disabled</td></tr><tr><td>ari-geo constraints</td><td></td><td>257</td><td>458</td></tr><tr><td>iterations</td><td>53</td><td>47</td><td>228</td></tr><tr><td>average time per iteration</td><td>1mn30s</td><td>1mn47s</td><td>5mn40s</td></tr><tr><td>analysis time</td><td>1h20mn</td><td>1h24mn</td><td>21h32mn</td></tr><tr><td>warnings</td><td>24</td><td>0</td><td>80</td></tr></tbody></table>

$[X \mapsto \alpha \times X + \beta]^{(n)}(M)$, where $(M, \alpha, \beta)$ are discovered automatically and $n$ is the maximum value of the clock counter. This approximation is proved correct and allows us to bound the value of some floating-point variables by using the program execution time. These bounds cannot be discovered either by ignoring the clock counter or by just bounding the difference between variable values and the clock value (c.f. [1]). Our framework allows the full certification of huge critical embedded softwares. The accuracy gain significantly reduces the exploration space which leads to an analysis speed-up in some of our examples.

**Acknowledgments.** We deeply thank the anonymous referees. We also thank Francesco Logozzo, Enea Zaffanella, and each member of the magic team: Bruno Blanchet, Patrick Cousot, Radhia Cousot, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival.

## References

1. B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival. Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In *The Essence of Computation: Complexity, Analysis, Transformation.*, LNCS 2566. Springer-Verlag, 2002.

2. B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival. A static analyzer for large safety-critical software. In *Proc. PLDI'03.* ACM Press, 2003.

3. P. 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.* PhD thesis, Université Scientifique et Médicale de Grenoble, 1978.

4. P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In *Proc. POPL'77.* ACM Press, 1977.

5. P. Cousot and R. Cousot. Abstract interpretation frameworks. *Journal of logic and computation*, 2(4), August 1992.

6. J. Feret. Static analysis of digital filters. In *European Symposium on Programming (ESOP'04)*, number 2986 in LNCS. Springer-Verlag, 2004.

7. X. Leroy, D. Doligez, J. Garrigue, D. Rémy, and J. Vouillon. The Objective Caml system, documentation and user's manual. Technical report, INRIA, 2002.

8. A. Miné. The octagon abstract domain. In *Proc. WCRE'01(AST'01)*, IEEE, 2001.

9. A. Miné. Relational abstract domains for the detection of floating-point run-time errors. In *Proc. ESOP'04*, LNCS. Springer, 2004.