# Compiling with Abstract Interpretation (with appendices)

Dorian Lesbre, Matthieu Lemerre

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

## To cite this version:

Dorian Lesbre, Matthieu Lemerre. Compiling with Abstract Interpretation (with appendices). CEA LIST. 2024. hal-04535159v3

HAL Id: hal-04535159

https://hal.science/hal-04535159v3

Submitted on 2 May 2024

HAL is a multi-disciplinary open access archive for the deposit and dissemination of scientific research documents, whether they are published 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_2.png" /></figure>
Compiling with Abstract Interpretation (with appendices)

DORIAN LESBRE, Université Paris-Saclay, CEA, List, France

MATTHIEU LEMERRE, Université Paris-Saclay, CEA, List, France

Rewriting and static analyses are mutually beneficial techniques: program transformations change the inten-
sional aspects of the program, and can thus improve analysis precision, while some efficient transformations
are enabled by specific knowledge of some program invariants. Despite the strong interaction between these
techniques, they are usually considered distinct. In this paper, we demonstrate that we can turn abstract
interpreters into compilers, using a simple free algebra over the standard signature of abstract domains.
Functor domains correspond to compiler passes, for which soundness is translated to a proof of forward
simulation, and completeness to backward simulation. We achieve translation to SSA using an abstract do-
main with a non-standard SSA signature. Incorporating such an SSA translation to an abstract interpreter
improves its precision; in particular we show that an SSA-based non-relational domain is always more precise
than a standard non-relational domain for similar time and memory complexity. Moreover, such a domain
allows recovering from precision losses that occur when analyzing low-level machine code instead of source
code. These results help implement analyses or compilation passes where symbolic and semantic methods
simultaneously refine each other, and improves precision when compared to doing the passes in sequence.

CCS Concepts: • Software and its engineering → Compilers; Formal software verification; • Theory of computation → Program analysis; Program verification; Abstraction; Equational logic and rewriting.

Additional Key Words and Phrases: Compilers, Abstract Interpretation, Static Single Assignment (SSA).

# 1 INTRODUCTION

Syntactic transformations, also called symbolic methods [Miné 2006], are an essential tool to improve
the precision of abstract domains. For instance, compiled code usually executes sequences of small
instructions over temporary variables. Analyzing such code one instruction at a time leads to
precision losses compared to source analysis because the analysis lacks context. Logozzo and
Fähndrich [2008] call this the limited code window problem, and show that solving it requires
the use of syntactic term manipulation. Moreover, when the compilation target is machine code,
a precise analysis can only be obtained if it reconstructs simple conditions from the machine
semantics (e.g. it is more precise to analyze x > y than an instruction sequence involving a xor
between the overflow and signed flag) [Balakrishnan and Reps 2010; Djoudi et al. 2016]. Outside
of compiled code, many authors have used syntactic transformations to improve the precision of
abstract domains at a low cost [Boillot and Feret 2023; Gange et al. 2016; Lemerre 2023; Miné 2006].

However, many such syntactic transformations benefit from a prior semantic analysis. For
example, rewriting x | 4 into x + 4 (where | means bitwise or, as in C) holds only if the second bit of
x always has value 0. Common examples include dead code elimination or constant propagation,
which requires a static analysis to identify constant boolean conditions or expressions. In general, the
essence of compiler optimization is to symbolically rewrite the program using semantic invariants
computed in a prior analysis pass [Cousot and Cousot 2002].

Thus, syntactic transformations both benefit from, and help improve, semantic analyses. There-
fore, applying each in different passes raises the phase ordering issue, and the best precision is
obtained by performing both simultaneously [Click and Cooper 1995; Cousot and Cousot 1979]. A
notable application of such a simultaneous analysis is machine code analysis, which often fails to
terminate due to excessive imprecision. Here, syntactic rewrites enabled by found invariants are
useful to undo compiler transformations and recover a representation which is easier to analyze.

Authors' addresses: Dorian Lesbre, Université Paris-Saclay, CEA, List, F-91120, Palaiseau, France, dorian.lesbre@cea.fr;
Matthieu Lemerre, Université Paris-Saclay, CEA, List, F-91120, Palaiseau, France, matthieu.lemerre@cea.fr;
Compiling with Abstract Interpretation (with appendices)

DORIAN LESBRE, Université Paris-Saclay, CEA, List, France

MATTHIEU LEMERRE, Université Paris-Saclay, CEA, List, France

Rewriting and static analyses are mutually beneficial techniques: program transformations change the inten-
sional aspects of the program, and can thus improve analysis precision, while some efficient transformations
are enabled by specific knowledge of some program invariants. Despite the strong interaction between these
techniques, they are usually considered distinct. In this paper, we demonstrate that we can turn abstract
interpreters into compilers, using a simple free algebra over the standard signature of abstract domains.
Functor domains correspond to compiler passes, for which soundness is translated to a proof of forward
simulation, and completeness to backward simulation. We achieve translation to SSA using an abstract do-
main with a non-standard SSA signature. Incorporating such an SSA translation to an abstract interpreter
improves its precision; in particular we show that an SSA-based non-relational domain is always more precise
than a standard non-relational domain for similar time and memory complexity. Moreover, such a domain
allows recovering from precision losses that occur when analyzing low-level machine code instead of source
code. These results help implement analyses or compilation passes where symbolic and semantic methods
simultaneously refine each other, and improves precision when compared to doing the passes in sequence.

CCS Concepts: • Software and its engineering → Compilers; Formal software verification; • Theory of computation → Program analysis; Program verification; Abstraction; Equational logic and rewriting.

Additional Key Words and Phrases: Compilers, Abstract Interpretation, Static Single Assignment (SSA).

# 1 INTRODUCTION

Syntactic transformations, also called symbolic methods [Miné 2006], are an essential tool to improve the precision of abstract domains. For instance, compiled code usually executes sequences of small instructions over temporary variables. Analyzing such code one instruction at a time leads to precision losses compared to source analysis because the analysis lacks context. Logozzo and Fähndrich [2008] call this the limited code window problem, and show that solving it requires the use of syntactic term manipulation. Moreover, when the compilation target is machine code, a precise analysis can only be obtained if it reconstructs simple conditions from the machine semantics (e.g. it is more precise to analyze $x > y$ than an instruction sequence involving a xor between the overflow and signed flag) [Balakrishnan and Reps 2010; Djoudi et al. 2016]. Outside of compiled code, many authors have used syntactic transformations to improve the precision of abstract domains at a low cost [Boillot and Feret 2023; Gange et al. 2016; Lemerre 2023; Miné 2006].

However, many such syntactic transformations benefit from a prior semantic analysis. For
example, rewriting $x | 4$ into $x + 4$ (where | means bitwise or, as in C) holds only if the second bit of
$x$ always has value 0. Common examples include dead code elimination or constant propagation,
which requires a static analysis to identify constant boolean conditions or expressions. In general, the
essence of compiler optimization is to symbolically rewrite the program using semantic invariants
computed in a prior analysis pass [Cousot and Cousot 2002].

Thus, syntactic transformations both benefit from, and help improve, semantic analyses. Therefore, applying each in different passes raises the phase ordering issue, and the best precision is obtained by performing both simultaneously [Click and Cooper 1995; Cousot and Cousot 1979]. A notable application of such a simultaneous analysis is machine code analysis, which often fails to terminate due to excessive imprecision. Here, syntactic rewrites enabled by found invariants are useful to undo compiler transformations and recover a representation which is easier to analyze.

Authors’ addresses: Dorian Lesbre, Université Paris-Saclay, CEA, List, F-91120, Palaiseau, France, dorian.lesbre@cea.fr;
Matthieu Lemerre, Université Paris-Saclay, CEA, List, F-91120, Palaiseau, France, matthieu.lemerre@cea.fr.
<figure><img src="image_1.png" /><figcaption>Fig. 1. Functor chain of our analysis: with the final domain on the left and base domains on the right. Arrows point from arguments to the functor that uses them. Square purple nodes are IMP domains, and circular blue nodes are SSA domains.</figcaption></figure>

*Abstract interpretation* [Cousot and Cousot 1977] provides a generic method for combining analysis passes [Cousot and Cousot 1979] by encoding them as operations over an abstract domain with a common interface. The classical interface requires a join, inclusion, widening, and analysis of statements. Some syntactic transformations have been implemented as abstract domains under this interface (e.g. [Boillot and Feret 2023; Chang and Leino 2005; Gange et al. 2016; Gulwani and Necula 2004; Kildall 1973; Miné 2006]), but until recently, such domains could not produce recursive terms. This limited the syntactic transformations that an abstract interpreter could perform to local transformations, unlike the usual syntactic translation method used in compilation. This restriction was lifted in *Lemerre* [2023], where an abstract interpreter was used to perform a complex syntactic transformation, SSA translation, using simple abstract domains. The resulting algorithm is arguably simpler than the standard methods [Aycock and Horspool 2000; Brandis and Mössenböck 1994; Braun et al. 2013; Cytron et al. 1991; Sreedhar and Gao 1995].

*Problem*. While the work of *Lemerre* [2023] hinted that some compilation techniques could be performed by abstract interpretation, it left many questions unanswered, such as:

* Can compilation-by-abstract-interpretation generalize to transformations other than SSA translation, i.e. to other input or output languages? In particular, *Lemerre* [2023] does not perform any control-flow transformation other than dead-code elimination, and maintains a 1-to-1 correspondence between source and target locations.

* How can compilation-by-abstract-interpretation interact with semantic analyses in practice? *Lemerre* [2023] proposed using a regular reduced product [Cousot and Cousot 1979]. However, one might prefer other generic domain combinations [Cousot and Cousot 1979; Venet 1996], or a more specialized combination. This is especially true if one wants to perform the analysis on the SSA translation instead of the source program.

* What are the cost and precision advantages of compilation-by-abstract-interpretation (and in particular, SSA translation) when used to improve the precision of a static analysis? Do standard compilation techniques apply to this framework, such as rewriting terms to improve global value numbering? How would they impact precision? *Lemerre* [2023] only stated that his symbolic expression abstract domain has a low computational complexity.

*Contributions*. Our overall contribution is to provide answers to the above questions by presenting an abstract interpreter design. In this design, syntactic transformations, seen semantically as abstract domains, can be combined with semantic analyses so that both run simultaneously and help each other. We summarize this as “compiling with abstract interpretation”, which not only means performing the compilation using abstract interpretation, but also to simultaneously use the program transformations as a means to improve the abstract interpretation.

Figure 1 presents the overall design of our abstract interpreter as a collection of abstract domains that are all executed simultaneously. More specifically:
<figure><img src="image_3.png" /><figcaption>Fig. 1. Contractor chain of our analysis: with the final domain on the left and base domains on the right. Arrows point from arguments to the contractor that uses them. Square purple nodes are IMP domains, and circular blue nodes are SSA domains.</figcaption></figure>

*Abstract interpretation* [Cousot and Cousot 1977] provides a generic method for combining analysis passes [Cousot and Cousot 1979] by encoding them as operations over an abstract domain with a common interface. The classical interface requires a join, inclusion, widening, and analysis of statements. Some syntactic transformations have been implemented as abstract domains under this interface (e.g. [Boillot and Feret 2023; Chang and Leino 2005; Gange et al. 2016; Gulwani and Necula 2004; Kildall 1973; Miné 2006]), but until recently, such domains could not produce recursive terms. This limited the syntactic transformations that an abstract interpreter could perform to local transformations, unlike the usual syntactic translation method used in compilation. This restriction was lifted in Lemerre [2023], where an abstract interpreter was used to perform a complex syntactic transformation, SSA translation, using simple abstract domains. The resulting algorithm is arguably simpler than the standard methods [Aycock and Horspool 2000; Brandis and Mössenböck 1994; Braun et al. 2013; Cytron et al. 1991; Sreedhar and Gao 1995].

**Problem.** While the work of Lemerre [2023] hinted that some compilation techniques could be
performed by abstract interpretation, it left many questions unanswered, such as:

* Can compilation-by-abstract-interpretation generalize to transformations other than SSA translation, i.e. to other input or output languages? In particular, Lemerre [2023] does not perform any control-flow transformation other than dead-code elimination, and maintains a 1-to-1 correspondence between source and target locations.

* How can compilation-by-abstract-interpretation interact with semantic analyses in practice? Lemerre [2023] proposed using a regular reduced product [Cousot and Cousot 1979]. However, one might prefer other generic domain combinations [Cousot and Cousot 1979; Venet 1996], or a more specialized combination. This is especially true if one wants to perform the analysis on the SSA translation instead of the source program.

* What are the cost and precision advantages of compilation-by-abstract-interpretation (and in particular, SSA translation) when used to improve the precision of a static analysis? Do standard compilation techniques apply to this framework, such as rewriting terms to improve global value numbering? How would they impact precision? Lemerre [2023] only stated that his symbolic expression abstract domain has a low computational complexity.

*Contributions.* Our overall contribution is to provide answers to the above questions by presenting an abstract interpreter design. In this design, syntactic transformations, seen semantically as abstract domains, can be combined with semantic analyses so that both run simultaneously and help each other. We summarize this as “compiling with abstract interpretation”, which not only means performing the compilation using abstract interpretation, but also to simultaneously use the program transformations as a means to improve the abstract interpretation.

Figure 1 presents the overall design of our abstract interpreter as a collection of abstract domains that are all executed simultaneously. More specifically:
* Section 4 (FA domain) explains how we can generate imperative programs by abstract interpretation. We use a domain of free algebras over the classical abstract domain signature, dually interpreted as a set of states and as a transition system. The result of this free-algebra analysis is a program graph which is isomorphic to the source program graph;

* Section 5 (Q, DG, T, and × functors) shows that functor domains<fnref n="1" />, commonly used in abstract interpretation to transform analyses, can be viewed as compiler transformation passes. The setting is related to the tagless-final staged interpreters of Carette et al. [2009]. We show in particular that these passes preserve semantics: functor soundness implies a forward simulation and completeness implies a backward simulation with the same relation;

* Section 6 (circular hatted blue nodes) shows why static analysis of SSA programs requires an abstract domain with a different signature (and free algebra $\hat{\mathrm{FA}}$) than the usual signature for imperative programs;

* Section 7 (Lift functor) implements an SSA-translation compiler pass. This is achieved by a functor that lifts an abstract domain with SSA domain signature to an abstract domain with an imperative domain signature;

* Section 8 (N domain), presents a “non-relational” analysis for the SSA signature, based on the combination of symbolic expressions [Lemerre 2023] with single-value abstractions<fnref n="2" />, such as intervals. We prove that lifting this non-relational SSA domain to an imperative domain is always more precise than the usual imperative analysis while incurring only a constant overhead. Moreover, it is the first known domain we know to have the strong relative completeness [Logozzo and Fähndrich 2008] property: it allows analyzing a compiled program with the same precision as the original (solving the limited code window problem);

* Section 9 evaluates our approach by describing CODEX, a static analyzer, based on this technique. It can handle both C and machine code and has been successfully used on industrial code bases [Nicole et al. 2021, 2022]. The multiple simultaneous translations (both at the source and SSA level) improve the precision and simplify the design of the analyzer in practice. We also present a simplified analyzer, TAI, that closely corresponds to Figure 1. Using it, we compare SSA numerical analysis to a standard non-relational analysis in terms of performance and precision. Both appear in the open source software artifact accompanying this article [Lesbre and Lemerre 2024a].

This is the full version (with appendices) of Lesbre and Lemerre [2024b].

## 2 A SMALL EXAMPLE

The top of Figure 2 presents a small example program, both in C code and in IMP (the simple input language of our analysis, Section 3). It consists of a simple loop, with a branching path testing whether the loop invariant holds. Here, the F macro stands for any complex numeric operation, changing it to another expression should work just as well. The graph distinguishes between conditional edges and assignment edges.

Proving the invariant, and optimizing the dead code of the else branch away is fairly involved. It is not optimized by modern compilers like GCC or LLVM. Doing so requires simultaneously performing numerical analysis (to learn that z is even), some syntactic transformations (to learn that $F(j + z\%2)$ is $F(j)$), optimistic global value numbering (to learn that $i = j$), and dead code elimination so that no analysis takes the else branch (which breaks all those properties). Performing all analyses in one pass is crucial, as no analysis is strong enough to prove the full invariant alone.

The rest of the figure displays the result of analyzing this program with various domains presented in this paper. Using the free algebra domain from Section 4 yields a renaming of the initial graph by

<footnote n="1">¹also called cofibered domains [Venet 1996]</footnote>

<footnote n="2">²called basis in Miné [2004] or partitioned lattice per variable in Rastello and Bouchez Tichadou [2022]</footnote>
* Section 4 (FA domain) explains how we can generate imperative programs by abstract interpretation. We use a domain of free algebras over the classical abstract domain signature, dually interpreted as a set of states and as a transition system. The result of this free-algebra analysis is a program graph which is isomorphic to the source program graph;

* Section 5 (Q, DG, T, and × functors) shows that functor domains<fnref n="1" />, commonly used in abstract interpretation to transform analyses, can be viewed as compiler transformation passes. The setting is related to the tagless-final staged interpreters of Carette et al. [2009]. We show in particular that these passes preserve semantics: functor soundness implies a forward simulation and completeness implies a backward simulation with the same relation;

* Section 6 (circular hatted blue nodes) shows why static analysis of SSA programs requires an abstract domain with a different signature (and free algebra $\overline{\text{FA}}$) than the usual signature for imperative programs;

* Section 7 (Lift functor) implements an SSA-translation compiler pass. This is achieved by a functor that lifts an abstract domain with SSA domain signature to an abstract domain with an imperative domain signature;

* Section 8 (N domain), presents a “non-relational” analysis for the SSA signature, based on the combination of symbolic expressions [Lemerre 2023] with single-value abstractions<fnref n="2" />, such as intervals. We prove that lifting this non-relational SSA domain to an imperative domain is always more precise than the usual imperative analysis while incurring only a constant overhead. Moreover, it is the first known domain we know to have the strong relative completeness [Logozzo and Fähndrich 2008] property: it allows analyzing a compiled program with the same precision as the original (solving the limited code window problem);

* Section 9 evaluates our approach by describing CODEX, a static analyzer, based on this technique. It can handle both C and machine code and has been successfully used on industrial code bases [Nicole et al. 2021, 2022]. The multiple simultaneous translations (both at the source and SSA level) improve the precision and simplify the design of the analyzer in practice. We also present a simplified analyzer, TAI, that closely corresponds to Figure 1. Using it, we compare SSA numerical analysis to a standard non-relational analysis in terms of performance and precision. Both appear in the open source software artifact accompanying this article [Lesbre and Lemerre 2024a].

This is the full version (with appendices) of Lesbre and Lemerre [2024b].

## 2 A SMALL EXAMPLE

The top of Figure 2 presents a small example program, both in C code and in IMP (the simple input language of our analysis, Section 3). It consists of a simple loop, with a branching path testing whether the loop invariant holds. Here, the F macro stands for any complex numeric operation, changing it to another expression should work just as well. The graph distinguishes between conditional edges and assignment edges.

Proving the invariant, and optimizing the dead code of the else branch away is fairly involved. It is not optimized by modern compilers like GCC or LLVM. Doing so requires simultaneously performing numerical analysis (to learn that z is even), some syntactic transformations (to learn that $F(j + z\%2)$ is $F(j)$), optimistic global value numbering (to learn that $i = j$), and dead code elimination so that no analysis takes the else branch (which breaks all those properties). Performing all analyses in one pass is crucial, as no analysis is strong enough to prove the full invariant alone.

The rest of the figure displays the result of analyzing this program with various domains presented in this paper. Using the free algebra domain from Section 4 yields a renaming of the initial graph by

<footnote n="1">¹also called cofibered domains [Venet 1996]</footnote>

<footnote n="2">²called basis in Miné [2004] or partitioned lattice per variable in Rastello and Bouchez Tichadou [2022]</footnote>
```c
#define F(x) ((x) * (x) + 1)
void example(int rand) { // l0
    int i = 0;          // l1
    int j = 0;          // l2
    int z = 4;          // l3
    while(z < 125){      // l4
        // Invariant: i = j ^ z%2 = 0
        j = F(j + z % 2); // l5
        if(F(i) == j && z%2 == 0){ // l6
            z += 2;
        } else { // Dead code // l7
            i = rand;       // l8
            z += 7;
        }
        // l9
        i = F(i);
    }
    // l10
}
```

<figure><img src="image_2.png" /><figcaption>(a) Example input program in C (left) and translated to IMP representation (right).</figcaption></figure>

```
p#(l0) = Entry             p#(l1) = Apply(i := 0, Entry)
p#(l2) = Apply(j := 0, Apply(i := 0, Entry)) p#(l4) = Apply(If z < 125, Loc(l3))
p#(l3) = Loc(l3)          Fg(p#)(l3) = Join{Apply(z := 4, p#(l2)); Apply(i := F(i), p#(l9))}
p#(l9) = Join{Apply(z := z + 7, p#(l8)); Apply(z := z + 2, p#(l6))}
```

(b) Result of analyzing using the free algebra domain ($p^# \triangleq$ analyse(FA), Section 4) for a selection of points ($l_0, l_1, l_2, l_3, l_4$ and $l_9$). The value of $F_g(p^#)$ is also shown when different from that of $p^#$.

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

(c) Analysis with bare SSA translation (left: Lift($\hat{\mathrm{FA}}$), Sections 6 and 7), and translation combined with numerical analysis and simple rewrites (right: Lift($\hat{\mathrm{Q}}(\hat{\mathrm{FA}}\times\hat{\mathrm{N}})$)). For legibility, we use $T, U, V, W, X$ as short names for terms and $\alpha, \beta, \gamma$ as short names for edges

<caption>Fig. 2. Example input program and results of different analysis.</caption>
```c
#define F(x) ((x) * (x) + 1)
void example(int rand) { // l0
    int i = 0;          // l1
    int j = 0;          // l2
    int z = 4;          // l3
    while(z < 125){      // l4
        // Invariant: i = j ^ z%2 = 0
        j = F(j + z % 2); // l5
        if(F(i) == j && z%2 == 0){ // l6
            z += 2;
        } else { // Dead code // l7
            i = rand;       // l8
            z += 7;
        }
        // l9
        i = F(i);
    }
    // l10
}
```

<figure><img src="image_4.png" /><figcaption>(a) Example input program in C (left) and translated to IMP representation (right).</figcaption></figure>

```
p#(l0) = Entry              p#(l1) = Apply(i := 0, Entry)
p#(l2) = Apply(j := 0, Apply(i := 0, Entry)) p#(l4) = Apply(If z < 125, Loc(l3))
p#(l3) = Loc(l3)           Fg(p#)(l3) = Join{Apply(z := 4, p#(l2)); Apply(i := F(i), p#(l9))}
p#(l9) = Join{Apply(z := z + 7, p#(l8)); Apply(z := z + 2, p#(l6))}
```

(b) Result of analyzing using the free algebra domain ($p^# \triangleq$ analyse(FA), Section 4) for a selection of points ($l_0, l_1, l_2, l_3, l_4$ and $l_9$). The value of $F_g(p^#)$ is also shown when different from that of $p^#$.

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

(c) Analysis with bare SSA translation (left: Lift($\hat{FA}$), Sections 6 and 7), and translation combined with numerical analysis and simple rewrites (right: Lift($\hat{Q}(\hat{FA} \times \hat{N})$)). For legibility, we use $T, U, V, W, X$ as short names for terms and $\alpha, \beta, \gamma$ as short names for edges

<caption>Fig. 2. Example input program and results of different analysis.</caption>
z ∈ Z (Integers)      x ∈ X (Variables)      σ ∈ Σ ≜ X → Z (Stores)      ℓ ∈ L (Locations)
S ≜ L × Σ    ◦ ∈ {+; −; ×; /; %; =; ≠; <; ≤; ∧; ∨}    e ∈ E ≜ z | x | e ◦ e | e ? e : e (Expressions)
R ∈ R ≜ If e | x := e (Syntactic relations)      G ∈ G ≜ L × R × L → {0; 1} (Program graph)

$$
\mathcal{E}[\llbracket \cdot \rrbracket] \in \mathbb{E} \to \Sigma \to \mathbb{Z}_{\perp} \qquad \mathcal{R}[\llbracket \cdot \rrbracket] \in \mathbb{R} \to (\Sigma \times \Sigma \to \{0; 1\}) \quad \to_G \in \mathcal{S} \times \mathcal{S} \to \{0; 1\}
$$

$$
\mathcal{E}[\llbracket z \rrbracket](\sigma) \triangleq z
$$

$$
\mathcal{E}[\llbracket x \rrbracket](\sigma) \triangleq \sigma(x)
$$

$$
\mathcal{E}[\llbracket e_{\text{cond}} ? e_{\text{true}} : e_{\text{false}} \rrbracket](\sigma) \triangleq \begin{cases} \perp & \text{if } \mathcal{E}[\llbracket e_{\text{cond}} \rrbracket](\sigma) = \perp \\ \mathcal{E}[\llbracket e_{\text{true}} \rrbracket](\sigma) & \text{if } \mathcal{E}[\llbracket e_{\text{cond}} \rrbracket](\sigma) \neq 0 \\ \mathcal{E}[\llbracket e_{\text{false}} \rrbracket](\sigma) & \text{if } \mathcal{E}[\llbracket e_{\text{cond}} \rrbracket](\sigma) = 0 \end{cases}
$$

$$
\mathcal{E}[\llbracket e_l \diamond e_r \rrbracket](\sigma) \triangleq \begin{cases} \perp & \text{if } (\diamond \in \{/; \%\} \land \mathcal{E}[\llbracket e_r \rrbracket](\sigma) = 0) \lor (\perp \in \{\mathcal{E}[\llbracket e_l \rrbracket](\sigma); \mathcal{E}[\llbracket e_r \rrbracket](\sigma)\}) \\ \mathcal{E}[\llbracket e_l \rrbracket](\sigma) \diamond \mathcal{E}[\llbracket e_r \rrbracket](\sigma) & \text{otherwise} \end{cases}
$$

$$
\mathcal{R}[\llbracket \text{If } e \rrbracket(\sigma, \sigma') \triangleq \sigma = \sigma' \land \mathcal{E}[\llbracket e \rrbracket](\sigma) \notin \{0; \perp\} \quad \mathcal{R}[\llbracket x := e \rrbracket(\sigma, \sigma') \triangleq \mathcal{E}[\llbracket e \rrbracket](\sigma) \neq \perp \land \sigma' = \sigma[x \mapsto \mathcal{E}[\llbracket e \rrbracket](\sigma)] \\
(\ell, \sigma) \to_G (\ell', \sigma') \triangleq \exists R \in \mathbb{R}, \mathcal{G}(\ell, R, \ell') \land \mathcal{R}[\llbracket R \rrbracket](\sigma, \sigma')
$$

<caption>Fig. 3. IMP syntax (top) and semantics (bottom).</caption>

Theorem 4.1, so we only show how a few select points are renamed in Figure 2b. Finally, Figure 2c shows the result of our SSA translations, both as a standalone analysis (left), and combined with other analysis that prove the invariant (right). The first one closely resembles the intermediate representation that a compiler would generate, although our SSA variant deviates slightly from typical SSA ($\phi$ functions replaced by join nodes). Note how binding edges only appear before joins.

3 NOTATIONS AND BACKGROUND

This section presents the background notions used in this paper, with their associated notations.
Specifically, it describes common notations; introduces a small example language: *IMP*; and presents
the signature of our abstract domains along with an example numeric domain.

3.1 Notations

We write $X_{\perp} \triangleq X \cup \{\perp\}$ for the set $X$ with an extra element $\perp \notin X$. We use $\mathcal{P}(X) \triangleq \{Y \mid Y \subseteq X\}$ for the set of subsets of $X$ and $\mathcal{P}_f(X) \triangleq \{Y \in \mathcal{P}(X) \mid Y \text{ finite}\}$ for the set of finite subsets of $X$.

Let $X \to Y$ be the set of partial functions from $X$ to $Y$ and $X \to Y$ the set of total functions from $X$ to $Y$ (their domain is exactly $X$). Functions are seen as sets of bindings $x \mapsto y$, replacing curly braces {} with brackets []. So $[z \mapsto z+1 \mid z \in \mathbb{Z}]$ is the successor function, and $[0 \mapsto 1; 1 \mapsto 2]$ is a function defined only on 0 and 1. We use the short notation $[x \in X \mapsto f(x)]$ for $[x \mapsto f(x) \mid x \in X]$.

For a function *f*, we denote its domain by *dom* *f* and its image by *img* *f*. We denote the image of *x* under *f* by *f*(*x*). We use *f*[*g*] ≜ [*v* ↦ *f*(*v*) | *v* ∈ *dom* *f* \ *dom* *g*] ∪ *g* for the function *f* updated with all bindings of *g*. Often *g* will be a single binding [*x* ↦ *y*] which leads to the notation: *f* [*x* ↦ *y*].

We view relations *R* as multi-variable predicates *R* ∈ *X* × *Y* → {0; 1} (also called indicative functions). We often write then as logic formulas using the usual logical operators (=, ∧, ∨).

3.2 IMP syntax and semantics

We use a small imperative programming language named IMP, defined in Figure 3. Program expressions e ∈ E are composed of integers (Z), variables (X), binary operators (◦), and a ternary if-then-else operator. A program G ∈ G is a directed graph, with location identifiers ℓ ∈ L as vertices. Its edges are labelled by syntactic relations R ∈ R, which are either guard conditions or single variable assignments. L is finite. This language supports loops (looping path in the graph), arbitrary gotos, but not function calls, as it has no memory and thus no call stack.
z ∈ Z (Integers)      x ∈ X (Variables)      σ ∈ Σ ≜ X → Z (Stores)      ℓ ∈ L (Locations)
S ≜ L × Σ    ◦ ∈ {+; −; ×; /; %; =; ≠; <; ≤; ∧; ∨}    e ∈ E ≜ z | x | e ◦ e | e ? e : e (Expressions)
R ∈ R ≜ If e | x := e (Syntactic relations)      G ∈ G ≜ L × R × L → {0; 1} (Program graph)

$$
\mathcal{E}[\cdot] \in E \to \Sigma \to Z_{\perp} \qquad \mathcal{R}[\cdot] \in R \to (\Sigma \times \Sigma \to \{0; 1\}) \quad \to_G \mathcal{S} \times \mathcal{S} \to \{0; 1\}
$$

$$
\mathcal{E}[z](\sigma) \triangleq z
$$

$$
\mathcal{E}[x](\sigma) \triangleq \sigma(x)
$$

$$
\mathcal{E}[e_{\text{cond}} ? e_{\text{true}} : e_{\text{false}}](\sigma) \triangleq \begin{cases} \perp & \text{if } \mathcal{E}[e_{\text{cond}}](\sigma) = \perp \\ \mathcal{E}[e_{\text{true}}](\sigma) & \text{if } \mathcal{E}[e_{\text{cond}}](\sigma) \neq 0 \\ \mathcal{E}[e_{\text{false}}](\sigma) & \text{if } \mathcal{E}[e_{\text{cond}}](\sigma) = 0 \end{cases}
$$

$$
\mathcal{E}[e_l \diamond e_r](\sigma) \triangleq \begin{cases} \perp & \text{if } (\diamond \in \{\;/\;\%\} \land \mathcal{E}[e_r](\sigma) = 0) \lor (\perp \in \{\mathcal{E}[e_l](\sigma); \mathcal{E}[e_r](\sigma)\}) \\ \mathcal{E}[e_l](\sigma) \diamond \mathcal{E}[e_r](\sigma) & \text{otherwise} \end{cases}
$$

$$
\mathcal{R}[\text{If } e](\sigma, \sigma') \triangleq \sigma = \sigma' \land \mathcal{E}[e](\sigma) \notin \{0; \perp\} \quad \mathcal{R}[x := e](\sigma, \sigma') \triangleq \mathcal{E}[e](\sigma) \neq \perp \land \sigma' = \sigma[x \mapsto \mathcal{E}[e](\sigma)] \\
(\ell, \sigma) \to_G (\ell', \sigma') \triangleq \exists R \in \mathcal{R}, \mathcal{G}(\ell, R, \ell') \land \mathcal{R}[R](\sigma, \sigma')
$$

<caption>Fig. 3. IMP syntax (top) and semantics (bottom).</caption>

Theorem 4.1, so we only show how a few select points are renamed in Figure 2b. Finally, Figure 2c shows the result of our SSA translations, both as a standalone analysis (left), and combined with other analysis that prove the invariant (right). The first one closely resembles the intermediate representation that a compiler would generate, although our SSA variant deviates slightly from typical SSA (φ functions replaced by join nodes). Note how binding edges only appear before joins.

3 NOTATIONS AND BACKGROUND

This section presents the background notions used in this paper, with their associated notations.
Specifically, it describes common notations; introduces a small example language: **IMP**; and presents
the signature of our abstract domains along with an example numeric domain.

**3.1 Notations**

We write $X_{\perp} \triangleq X \cup \{\perp\}$ for the set $X$ with an extra element $\perp \notin X$. We use $\mathcal{P}(X) \triangleq \{Y \mid Y \subseteq X\}$ for the set of subsets of $X$ and $\mathcal{P}_f(X) \triangleq \{Y \in \mathcal{P}(X) \mid Y \text{ finite}\}$ for the set of finite subsets of $X$.

Let $X \to Y$ be the set of partial functions from $X$ to $Y$ and $X \to Y$ the set of total functions from $X$ to $Y$ (their domain is exactly $X$). Functions are seen as sets of bindings $x \mapsto y$, replacing curly braces {} with brackets []. So $[z \mapsto z + 1 \mid z \in \mathbb{Z}]$ is the successor function, and $[0 \mapsto 1; 1 \mapsto 2]$ is a function defined only on 0 and 1. We use the short notation $[x \in X \mapsto f(x)]$ for $[x \mapsto f(x) \mid x \in X]$.

For a function *f*, we denote its domain by *dom* *f* and its image by *img* *f*. We denote the image of *x* under *f* by *f*(*x*). We use *f*[*g*] ≜ [*v* ↦ *f*(*v*) | *v* ∈ *dom* *f* \ *dom* *g*] ∪ *g* for the function *f* updated with all bindings of *g*. Often *g* will be a single binding [*x* ↦ *y*] which leads to the notation: *f* [*x* ↦ *y*].

We view relations *R* as multi-variable predicates *R* ∈ *X* × *Y* → {0; 1} (also called indicative functions). We often write then as logic formulas using the usual logical operators (=, ∧, ∨).

## 3.2 IMP syntax and semantics

We use a small imperative programming language named **IMP**, defined in Figure 3. Program expressions `e ∈ E` are composed of integers (`Z`), variables (`X`), binary operators (`diamond`), and a ternary if-then-else operator. A program `G ∈ G` is a directed graph, with *location* identifiers `ℓ ∈ L` as vertices. Its edges are labelled by syntactic relations `R ∈ R`, which are either guard conditions or single variable assignments. `L` is finite. This language supports loops (looping path in the graph), arbitrary gotos, but not function calls, as it has no memory and thus no call stack.
$$
\begin{array}{l@{\qquad}l}
\Sigma^{\#}(\text{set of abstract states}) & \gamma \in \Sigma_{\perp}^{\#} \to \mathcal{P}(\Sigma) \\
\text{entry} \in \Sigma^{\#} & \Sigma \subseteq \gamma(\text{entry}) \qquad (\text{ENTRY SOUND}) \\
\text{apply} \in \mathbb{R} \times \Sigma^{\#} \to \Sigma_{\perp}^{\#} & \{\sigma' \in \Sigma \mid \exists \sigma \in \gamma(s^{\#}), \mathcal{R}[\mathbb{R}](\sigma, \sigma')\} \subseteq \gamma(\text{apply}(R, s^{\#})) \qquad (\text{APPLY SOUND}) \\
\text{join} \in \mathcal{P}_{\gamma}(\Sigma^{\#}) \to \Sigma^{\#} & \cup_{s^{\#} \in S^{\#}} \gamma(s^{\#}) \subseteq \gamma(\text{join}(S^{\#})) \qquad (\text{JOIN SOUND}) \\
\text{widen} \in \mathbb{W} \times \Sigma^{\#} \times \Sigma^{\#} \to \Sigma^{\#} & \gamma(s^{\#}) \cup \gamma(t^{\#}) \subseteq \gamma(\text{widen}(\ell, s^{\#}, t^{\#})) \qquad (\text{WSOUND})
\end{array}
$$

$$
\begin{array}{l@{\qquad}l}
\mathcal{F}_g \in (\mathbb{L} \to \text{D.}\Sigma^\#) \to (\mathbb{L} \to \text{D.}\Sigma^\#) & \text{(D is an IMP domain)} \\
\mathcal{F}_g(p^\#) \triangleq \ell_0 \mapsto \text{D.entry} \\
\quad | \quad \ell \mapsto \text{D.join} \left\{ \begin{array}{@{}l@{}}
\text{D.apply}(R, p^\#(\ell')) \quad \text{for } \ell' \in \mathbb{L}, R \in \mathbb{R} : \begin{array}{@{}l@{}}
\mathcal{G}(\ell', R, \ell) \wedge \ell' \in \text{dom } p^\# \\
\wedge \text{D.apply}(R, p^\#(\ell')) \neq \perp
\end{array}
\end{array} \right\} & \\
\nabla_W \in (\mathbb{L} \to \text{D.}\Sigma^\#) \to (\mathbb{L} \to \text{D.}\Sigma^\#) \to (\mathbb{L} \to \text{D.}\Sigma^\#) & \\
p^\# \nabla_W q^\# \triangleq \ell \mapsto \text{D.widen}(\ell, p^\#(\ell), q^\#(\ell)) & \text{if } \ell \in \mathbb{W} \text{ (set of widening points)} \\
\quad | \quad \ell \mapsto q^\#(\ell) & \text{otherwise} \\
\text{analyse}(\text{D}) \in \mathbb{L} \to \text{D.}\Sigma^\# & \\
\text{analyse}(\text{D}) \triangleq \text{Ifp} \left[ p^\# \in (\mathbb{L} \to \text{D.}\Sigma^\#) \mapsto p^\# \nabla_W \mathcal{F}_g(p^\#) \right]
\end{array}
$$

<caption>Fig. 4. IMP abstract domain signature (top left) properties (top right) and analysis (bottom).</caption>

Semantics. $\mathcal{E}[\llbracket e \rrbracket](\sigma)$ evaluates the expression $e$ to an integer, using the store $\sigma$ for variable values. Arithmetic operators are standard, using euclidean division and modulo. Divisions by 0 interrupt the program (i.e., return $\perp$). Comparison operators are defined to return 1 when true and 0 otherwise. Boolean operators are non-lazy, and consider any non-zero value as true.

$\mathbb{R}[\cdot] \llbracket \cdot \rrbracket$ transforms a syntactic relation $\mathbb{R}$ into a mathematical relation on *program states* (pairs of locations and stores). Guards do not change the store but block execution when the condition evaluates to 0 or $\perp$; assignments $x := e$ change the value of $x$ to the evaluation of $e$ in the input state, leaving the other variables unchanged.

The semantics of a program $G \in \mathcal{G}$ is given as a transition relation $(\ell, \sigma) \to_G \ell'$ ($\sigma'$) between states. There is a transition between two states if there exists an edge between their locations in $G$ such that the edge's relation is verified by the stores. This is not necessarily deterministic, as a state might have multiple valid successors. We write $\to_G^*$ for the reflexive transitive closure of $\to_G$. We assume that all outgoing edges from a location are labelled by different relations.<fnref n="3" />

Finally, programs have an initial location $\ell_0 \in \mathbb{L}$, which has no predecessors. We say that a state $(\ell, \sigma) \in \mathcal{S}$ is *reachable* when there is a $\sigma_0 \in \Sigma$ such that $(\ell_0, \sigma_0) \to_G^* (\ell, \sigma)$.

## 3.3 Abstract interpretation of IMP

Abstract domains [Cousot and Cousot 1977] are algebraic structures whose signature is given at the top of Figure 4. They contain a set of abstract states $\Sigma^\#$ whose meaning is given by a concretization function $\gamma$, mapping an abstract state to a set of states. This function is only used in proofs and needs not to be computable. To lighten notations, we lift this concretization to $\Sigma_{\perp}^\#$ and assume that $\gamma(\perp) = \emptyset$ for all domains.

The domain operations (top left of Figure 4) must be computable. entry is the program entry point. apply($R, s^\#$) represents all the states that can be obtained from $s^\#$ after applying a relation $R$. join computes an over-approximation of finite union, and is used at merge points in the control flow. widen is a widening operation, used to ensure termination of the analysis. For the sake of

<footnote n="3">³This allows uniquely identifying a program path from the trace of applied relations. It is true on deterministic programs, but can also be enforced on non-deterministic ones (using rewrites $e \mapsto e \times 1$ if needed). This simplifies Theorem 4.1.</footnote>
$$
\begin{array}{l@{\qquad}l}
\Sigma^{\#}(\text{set of abstract states}) & \gamma \in \Sigma_{\perp}^{\#} \to \mathcal{P}(\Sigma) \\
\text{entry} \in \Sigma^{\#} & \Sigma \subseteq \gamma(\text{entry}) \qquad (\text{ENTRY SOUND}) \\
\text{apply} \in \mathbb{R} \times \Sigma^{\#} \to \Sigma_{\perp}^{\#} & \{\sigma' \in \Sigma \mid \exists \sigma \in \gamma(s^{\#}), \mathcal{R}[\mathbb{R}](\sigma, \sigma')\} \subseteq \gamma(\text{apply}(R, s^{\#})) \qquad (\text{APPLY SOUND}) \\
\text{join} \in \mathcal{P}_{\gamma}(\Sigma^{\#}) \to \Sigma^{\#} & \cup_{s^{\#} \in S^{\#}} \gamma(s^{\#}) \subseteq \gamma(\text{join}(S^{\#})) \qquad (\text{JOIN SOUND}) \\
\text{widen} \in \mathbb{W} \times \Sigma^{\#} \times \Sigma^{\#} \to \Sigma^{\#} & \gamma(s^{\#}) \cup \gamma(t^{\#}) \subseteq \gamma(\text{widen}(\ell, s^{\#}, t^{\#})) \qquad (\text{WSOUND})
\end{array}
$$

$$
\begin{array}{l@{\qquad}l}
\mathcal{F}_g \in (\mathbb{L} \to \mathrm{D.}\Sigma^\#) \to (\mathbb{L} \to \mathrm{D.}\Sigma^\#) & \text{(D is an IMP domain)} \\
\mathcal{F}_g(p^\#) \triangleq \ell_0 \mapsto \mathrm{D.}\mathrm{entry} \\
\quad | \quad \ell \mapsto \mathrm{D.join} \left\{ \mathrm{D.apply}(R, p^\#(\ell')) \middle| \begin{array}{@{}l@{}} \text{for } \ell' \in \mathbb{L}, R \in \mathbb{R} : \mathcal{G}(\ell', R, \ell) \wedge \ell' \in \mathrm{dom} \, p^\# \\ \qquad \wedge \mathrm{D.apply}(R, p^\#(\ell')) \neq \perp \end{array} \right\} & \\
\nabla_W \in (\mathbb{L} \to \mathrm{D.}\Sigma^\#) \to (\mathbb{L} \to \mathrm{D.}\Sigma^\#) \to (\mathbb{L} \to \mathrm{D.}\Sigma^\#) & \\
p^\# \nabla_W q^\# \triangleq \ell \mapsto \mathrm{D.widen}(\ell, p^\#(\ell), q^\#(\ell)) & \text{if } \ell \in \mathbb{W} \text{ (set of widening points)} \\
\quad | \quad \ell \mapsto q^\#(\ell) & \text{otherwise} \\
\text{analyse}(\mathrm{D}) \in \mathbb{L} \to \mathrm{D.}\Sigma^\# & \\
\text{analyse}(\mathrm{D}) \triangleq \text{Ifp } [p^\# \in (\mathbb{L} \to \mathrm{D.}\Sigma^\#) \mapsto p^\# \nabla_W \mathcal{F}_g(p^\#)] &
\end{array}
$$

<caption>Fig. 4. IMP abstract domain signature (top left) properties (top right) and analysis (bottom).</caption>

Semantics. $\mathcal{E}[[e]](\sigma)$ evaluates the expression $e$ to an integer, using the store $\sigma$ for variable values. Arithmetic operators are standard, using euclidean division and modulo. Divisions by 0 interrupt the program (i.e., return $\perp$). Comparison operators are defined to return 1 when true and 0 otherwise. Boolean operators are non-lazy, and consider any non-zero value as true.

$\mathbb{R}[[\cdot]]$ transforms a syntactic relation $\mathbb{R}$ into a mathematical relation on *program states* (pairs of locations and stores). Guards do not change the store but block execution when the condition evaluates to 0 or $\perp$; assignments $x := e$ change the value of $x$ to the evaluation of $e$ in the input state, leaving the other variables unchanged.

The semantics of a program $G \in \mathcal{G}$ is given as a transition relation $(\ell, \sigma) \to_G \mathcal{G}(\ell', \sigma')$ between states. There is a transition between two states if there exists an edge between their locations in $G$ such that the edge's relation is verified by the stores. This is not necessarily deterministic, as a state might have multiple valid successors. We write $\to_G^*$ for the reflexive transitive closure of $\to_G$. We assume that all outgoing edges from a location are labelled by different relations.<fnref n="3" />

Finally, programs have an initial location $\ell_0 \in \mathbb{L}$, which has no predecessors. We say that a state $(\ell, \sigma) \in \mathcal{S}$ is *reachable* when there is a $\sigma_0 \in \Sigma$ such that $(\ell_0, \sigma_0) \to_G^*(\ell, \sigma)$.

## 3.3 Abstract interpretation of IMP

Abstract domains [Cousot and Cousot 1977] are algebraic structures whose signature is given at the top of Figure 4. They contain a set of abstract states $\Sigma^\#$ whose meaning is given by a concretization function $\gamma$, mapping an abstract state to a set of states. This function is only used in proofs and needs not to be computable. To lighten notations, we lift this concretization to $\Sigma_{\perp}^\#$ and assume that $\gamma(\perp) = \emptyset$ for all domains.

The domain operations (top left of Figure 4) must be computable. entry is the program entry point. apply($R, s^\#$) represents all the states that can be obtained from $s^\#$ after applying a relation $R$. join computes an over-approximation of finite union, and is used at merge points in the control flow. widen is a widening operation, used to ensure termination of the analysis. For the sake of

<footnote n="3">³This allows uniquely identifying a program path from the trace of applied relations. It is true on deterministic programs, but can also be enforced on non-deterministic ones (using rewrites $e \mapsto e \times 1$ if needed). This simplifies Theorem 4.1.</footnote>
<figure><img src="image_4.png" /><figcaption>Fig. 5. The numeric IMP abstract domain (N).</figcaption></figure>

simplicity, we do not discuss much about termination here. We only require that widening chains, i.e. repeated applications of widening operations, eventually stabilize. Thus, we do not need an order relation in our domain signature, as we can use equality directly.<fnref n="4" /> Another non-standard point is the need to pass a location (the widening point) as an argument to *widen*. This is required to ensure the convergence of abstract domains consisting in recursive terms [Lemerre 2023] by giving unique names to those terms. One can view domains implementing this signature as records whose fields are functions. We use the notation *D.**apply** to denote the *apply* function of the domain *D*.

A domain is *sound* when its operations meet the soundness hypotheses given at the top right of Figure 4. It is *complete* when its operations meet the converse hypotheses, with set inclusion reversed.

Abstract interpretation of an IMP domain *D* is done via a standard dataflow analysis [Cousot and Cousot 1977], presented in the bottom of Figure 4. *F*<sub>*g*</sub> joins at each point the *applies* of the predecessors. It is undefined at points where the set in *D*.**join** is empty. We write *W* the set of *widening points*, i.e. points where widenings are performed. Any subset of *L* with at least one point on every cycle in the control-flow graph is a valid choice for *W*. Bourdoncle [1993] gives a method to compute a reasonably small *W* (set of loop heads). The final result of our analysis is given by analyse(*D*)<sup>5</sup>. It is a partial function mapping locations *L* to our domain state *D*.Σ<sup>#</sup>. It is undefined on locations determined unreachable. It is computed as least fixed-point (lfp) of the widening of *F*<sub>*g*</sub>.

The most precise domain we can define in this setting is the *collecting semantics* domain, denoted *CS*. The concretization *γ* of *CS* is the identity. It is not computable, but helps quantify the abstraction loss suffered by other domains.

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

## 3.4 Example: non-relational numeric domain

A classical example domain is built on top of a single-value abstraction like intervals. They represent set of integers by pairs [*m*: *M*] ∈ Z<sup>#</sup> ≜ Z ∪ {−∞} × Z ∪ {+∞} with m ≤ M, concretized by γ<sub>Z<sup>#</sup></sub>([*m*: *M*]) ≜ {z ∈ Z | m ≤ z ≤ M}. We denote ⋃<sub>Z<sup>#</sup></sub>, ⋂<sub>Z<sup>#</sup></sub>, ⊆<sub>Z<sup>#</sup></sub> and ∇<sub>Z<sup>#</sup></sub> the usual join, meet, subset and widening operators on intervals [Cousot and Cousot 1977].

For each expression construct *f* of arity *n* we let $\tilde{f} \in \mathbb{Z}^{#n} \rightarrow \mathbb{Z}^#$ be the associated *forward transfer function* (which yields an abstraction of *f* given abstractions of its arguments) and $\tilde{f} \in \mathbb{Z}^{#n} \times \mathbb{Z}^# \rightarrow \mathbb{Z}^{#n}$ the *backward transfer function* (which refines the abstractions of the arguments given an abstraction of the result of *f*).

Using these, we can define our first IMP domain: the numeric domain, denoted *N*. It is presented in Figure 5, where $\tilde{\mathcal{E}}[\cdot] \in \mathbb{E} \rightarrow (\mathcal{X} \rightarrow \mathbb{Z}^#) \rightarrow \mathbb{Z}^#$ evaluates the expression (similarly to $\mathcal{E}[\cdot]$) in $\mathbb{Z}^#$ using the forward transfer functions; and $\sigma^# \leftarrow e \neq 0$ symbolizes refining $\sigma^#$ using the backward transfer functions and the information that $e \neq 0$ (using an algorithm similar to the HC4 constraint propagation [Benhamou et al. 1999]). This numerical domain is sound.

<footnote n="4">⁴For more details on this, see Appendix B.</footnote>

<footnote n="5">⁵The domain *D* is implicit in *F*<sub>*g*</sub> and ∇<sub>*W*</sub>, as it can be deduced from the analysis being considered, but explicit in analyse.</footnote>
<figure><img src="image_6.png" /><figcaption>Fig. 5. The numeric IMP abstract domain (N).</figcaption></figure>

simplicity, we do not discuss much about termination here. We only require that widening chains, i.e. repeated applications of widening operations, eventually stabilize. Thus, we do not need an order relation in our domain signature, as we can use equality directly.<fnref n="4" /> Another non-standard point is the need to pass a location (the widening point) as an argument to *widen*. This is required to ensure the convergence of abstract domains consisting in recursive terms [Lemerre 2023] by giving unique names to those terms. One can view domains implementing this signature as records whose fields are functions. We use the notation *D.**apply** to denote the *apply* function of the domain *D*.

A domain is *sound* when its operations meet the soundness hypotheses given at the top right of Figure 4. It is *complete* when its operations meet the converse hypotheses, with set inclusion reversed.

Abstract interpretation of an IMP domain *D* is done via a standard dataflow analysis [Cousot and Cousot 1977], presented in the bottom of Figure 4. *F*<sub>*g*</sub> joins at each point the *applies* of the predecessors. It is undefined at points where the set in *D*.**join** is empty. We write *W* the set of *widening points*, i.e. points where widenings are performed. Any subset of *L* with at least one point on every cycle in the control-flow graph is a valid choice for *W*. Bourdoncle [1993] gives a method to compute a reasonably small *W* (set of loop heads). The final result of our analysis is given by analyse(*D*)<sup>5</sup>. It is a partial function mapping locations *L* to our domain state *D*.Σ<sup>#</sup>. It is undefined on locations determined unreachable. It is computed as least fixed-point (lfp) of the widening of *F*<sub>*g*</sub>.

The most precise domain we can define in this setting is the *collecting semantics* domain, denoted *CS*. The concretization *γ* of *CS* is the identity. It is not computable, but helps quantify the abstraction loss suffered by other domains.

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

## 3.4 Example: non-relational numeric domain

A classical example domain is built on top of a single-value abstraction like intervals. They represent set of integers by pairs [*m*: *M*] ∈ Z<sup>#</sup> ≜ Z ∪ {−∞} × Z ∪ {+∞} with m ≤ M, concretized by γ<sub>Z<sup>#</sup></sub>([*m*: *M*]) ≜ {z ∈ Z | m ≤ z ≤ M}. We denote ⋃<sub>Z<sup>#</sup></sub>, ⋂<sub>Z<sup>#</sup></sub>, ⊆<sub>Z<sup>#</sup></sub> and ∇<sub>Z<sup>#</sup></sub> the usual join, meet, subset and widening operators on intervals [Cousot and Cousot 1977].

For each expression construct *f* of arity *n* we let $\tilde{f} \in \mathbb{Z}^{#n} \to \mathbb{Z}^#$ be the associated *forward transfer function* (which yields an abstraction of *f* given abstractions of its arguments) and $\tilde{f} \in \mathbb{Z}^{#n} \times \mathbb{Z}^# \to \mathbb{Z}^{#n}$ the *backward transfer function* (which refines the abstractions of the arguments given an abstraction of the result of *f*).

Using these, we can define our first IMP domain: the *numeric domain*, denoted *N*. It is presented in Figure 5, where $\tilde{\mathcal{E}}[\cdot] \in \mathbb{E} \to (\mathcal{X} \to \mathbb{Z}^#) \to \mathbb{Z}^#$ evaluates the expression (similarly to $\mathcal{E}[\cdot]$) in $\mathbb{Z}^#$ using the forward transfer functions; and $\sigma^# \leftarrow e \neq 0$ symbolizes refining $\sigma^#$ using the backward transfer functions and the information that $e \neq 0$ (using an algorithm similar to the HC4 constraint propagation [Benhamou et al. 1999]). This numerical domain is *sound*.

<footnote n="4">⁴For more details on this, see Appendix B.</footnote>

<footnote n="5">⁵The domain *D* is implicit in *F*<sub>*g*</sub> and ∇<sub>*W*</sub>, as it can be deduced from the analysis being considered, but explicit in analyse.</footnote>
$$ s^{\#} \in \mathrm{FA.}\Sigma^{\#} \triangleq \underset{\text{Entry} \mid \text{Apply}(R, s^{\#}) \mid \text{Join}(S^{\#}) \mid \text{Loc}(\ell)}{\text{Entry}} \quad \text{(Algebraic locations)} \\ \text{(where } R \in \mathbb{R} \text{ is a syntactic program relation, and } S^{\#} \in \mathcal{P}_{f}(\mathrm{FA.}\Sigma^{\#}) \text{)} $$

$$ \begin{array}{rcl@{\hspace{2em}}rcl} \mathrm{FA.entry} & \triangleq & \mathrm{Entry} & & \mathrm{FA.join}(S^{\#}) & \triangleq & \begin{cases} \perp & \text{if } S^{\#} \text{ is empty} \\ S^{\#} & \text{if } S^{\#} \text{ is a singleton } \{S^{\#}\} \\ \mathrm{Join}(S^{\#}) & \text{otherwise} \end{cases} \\ \mathrm{FA.apply}(R, s^{\#}) & \triangleq & \mathrm{Apply}(R, s^{\#}) & & \mathrm{FA.loc}(\ell) & \triangleq & \mathrm{Loc}(\ell) \\ \mathrm{FA.widen}(\ell, \llap{\text{\textit{, \_}}}, \llap{\text{\textit{\_}}}) & \triangleq & \mathrm{Loc}(\ell) & & & & \\ \mathrm{FA.}\gamma(\mathrm{Entry}) & \triangleq & \Sigma & & \mathrm{FA.}\gamma(\mathrm{Apply}(R, s^{\#})) & \triangleq & \{\sigma \in \Sigma \mid \exists \sigma' \in \mathrm{FA.}\gamma(s^{\#}), \mathcal{R}[\llap{\text{\textit{[}}R\text{\textit{]}}}] (\sigma', \sigma)\} \\ \mathrm{FA.}\gamma(\mathrm{Join}(S^{\#})) & \triangleq & \bigcup_{s^{\#} \in S^{\#}} \mathrm{FA.}\gamma(s^{\#}) & & \mathrm{FA.}\gamma(\mathrm{Loc}(\ell)) & \triangleq & \Sigma \end{array} $$

$$ \begin{array}{c@{\hspace{2em}}c@{\hspace{2em}}c} \begin{array}{c} \mathrm{TAPPLY} \\ s^{\#} \overset{R}{\mapsto} \underset{\text{Apply}(R, s^{\#})}{\text{\textit{\#}}} \end{array} & \begin{array}{c} \mathrm{TJOIN} \\ s^{\#} \overset{R}{\mapsto} \underset{\text{Join}(S^{\#})}{\text{\textit{\#}}} \end{array} & \begin{array}{c} \mathrm{TSELF} \\ \mathcal{F}_g(p^{\#})(\ell) = \text{Join}(S^{\#}) \qquad \mathrm{Loc}(\ell) \in S^{\#} \\ \mathrm{Loc}(\ell) \overset{\text{If } 1}{\mapsto} \underset{\text{Loc}(\ell)}{\text{\textit{\#}}} \end{array} \\ \begin{array}{c} \mathrm{TLoc} \\ s^{\#} \overset{R}{\mapsto} \underset{\text{Loc}(\ell)}{\text{\textit{\#}}} \end{array} & \begin{array}{c} \mathrm{VBASE} \\ s^{\#} \in \text{img } p^{\#} \\ V(s^{\#}) \end{array} & \begin{array}{c} \mathrm{VREC} \\ s^{\#} \overset{R}{\mapsto} \underset{\text{Loc}(\ell)}{\text{\textit{\#}}} \end{array} \qquad \begin{array}{c} \mathrm{GRAPHGEN} \\ s^{\#} \overset{R}{\mapsto} \underset{\text{Loc}(\ell)}{\text{\textit{\#}}} \end{array} \\ \begin{array}{c} s^{\#} \overset{R}{\mapsto} \underset{\text{Loc}(\ell)}{\text{\textit{\#}}} \end{array} & \begin{array}{c} V(s^{\#}) \\ V(s^{\#}) \end{array} & \begin{array}{c} V(t^{\#}) \\ \mathcal{G}_{p^{\#}}(s^{\#}, R, t^{\#}) \end{array} \end{array} $$

<caption>Fig. 6. The free algebra IMP abstract domain (FA) (top) and rules for generating IMP programs (bottom).</caption>

We use intervals here as they are well-known and easy to define, but this abstraction can very easily be switched to other single-value abstractions, such as congruence [Miné 2017], bitwise/tristate [Michel and Hentenryck 2012; Miné 2012; Vishwanathan et al. 2022], or any product of these abstractions. For our running example (Figure 2), intervals alone cannot prove that z is even, thus we need another abstraction (bitwise or congruence).

# 4 FREE ALGEBRA OF THE DOMAIN SIGNATURE

We now explain how a free algebra over the domain signature of Figure 4 can be used to exactly recover the source program as a standard abstract interpretation. This is achieved thanks to the dual interpretation of this abstract domain: the classical interpretation as a set of states, and the other as a new program graph whose vertices are elements of the free algebra, and whose edges are given by the Apply terms. In this section, the generated program is isomorphic to the source. We will add transformations in Section 5.

## 4.1 Definition

The free algebra IMP domain, denoted FA, is presented in Figure 6. Its elements, called algebraic locations are cyclic terms in the free algebra of the abstract domain signature (Figure 4). Thus, the domain operations: FA.entry, FA.apply and FA.join just create terms using the Entry<fnref n="6" />, Apply and Join function symbols. The other constructor, Loc, represents widening points, which also corresponds to recursion variables in the control-flow graph viewed as a cyclic term graph [Ariola and Klop 1996], as they are both used to break cycles. Thus, the widening operation FA.widen simply returns the relevant Loc, using the original program location name as a way to give a deterministic name to recursion variables and allow the analysis to terminate [Lemerre 2023]. Figure 2b shows the value of p# obtained from performing an analysis using this domain on a few select points.

<footnote n="6">⁶We denote the IMP domain interface in lowercase purple italics, its implementations in the same style but prefixed with the domain short name, and the terms of its free algebra in Capitalized Orange Typewriter Font.</footnote>
## 4.2 Concretization as a set of states

These algebraic locations can be interpreted in different ways. The first, more usual one, is as sets of states in the collecting semantics. It is given by the concretization $\mathbf{FA.}\gamma$ (which matches with the definition of the collecting semantics domain). Notice how the definition of the concretization simply maps our free algebra constructors to the corresponding operation in the collecting semantics. For instance, for the apply operation we have $\mathbf{FA.}\gamma(\mathbf{Apply}(R, s^*)) = \mathbf{CS.}\mathbf{apply}(R, \mathbf{FA.}\gamma(s^*))$.

All FA domain operations are sound. $\mathbf{FA.join}$, $\mathbf{FA.apply}$ and $\mathbf{FA.entry}$ transfer functions are also complete: only $\mathbf{FA.widen}$ loses precision as $\mathbf{Loc}$ concretizes into the entire set of stores $\Sigma$. This concretization can be refined by unfolding the fixed point (replacing $\mathbf{Loc}(\ell)$ with $\mathcal{F}_g(p^*)(\ell)$). The new term will still contain $\mathbf{Loc}(\ell)$ as subterm, which can once again be unfolded, and so on. For the most precise version, unfold until a fixed point is reached here.

## 4.3 Concretization as a program graph

We can also construct a new IMP program graph $G_{p^*} \in \mathbf{FA.}\Sigma^* \times \mathbb{R} \times \mathbf{FA.}\Sigma^* \to \{0; 1\}$ from an abstract element $p^* \in \mathbb{L} \to \mathbf{FA.}\Sigma^*$, or any analysis that uses the free algebra domain as a subdomain. To do so, we define an edge predicate $\mapsto_\# \in (\mathbf{FA.}\Sigma^* \times \mathbb{R} \times \mathbf{FA.}\Sigma^*) \to \{0; 1\}$, and a vertex predicate $V \in \mathbf{FA.}\Sigma^* \to \{0; 1\}$ by the rules at the bottom of Figure 6. Both depend on $p^*$, not included it in their notation to keep them light. See Figure 7 for a small example graph built using these rules.

An $\mathbf{Apply}(R, s^*)$ term represents a vertex (i.e., program location in the new graph) obtained by following an edge labelled by $R$ coming from $s^*$ (rule $\mathbf{TAPPLY}$). $\mathbf{TJOIN}$ ensures that all the terms appearing in a $\mathbf{Join}(S^*)$ term correspond to the same program location in the generated program graph, thus, for any edge going to $t^* \in S^*$, it adds an edge going to $\mathbf{Join}(S^*)$. For the $\mathbf{Loc}(\ell)$ case, we need to use the main transfer function $\mathcal{F}_g$ of our abstract interpretation to obtain the pre-state before widening (join of the applys of the predecessors of $\ell$). The rule $\mathbf{TLoc}$ then simply states that the transitions to $\mathbf{Loc}$ are the same as those to that pre-state ($\mathbf{Loc}$ is only introduced at a widening point as a renaming to avoid having recursive terms). Finally, $\mathbf{TSELF}$ ensures that immediate loops ($\ell$ being its own predecessor through a trivial relation) are preserved. Note that $\mathbf{Entry}$ has no predecessor, which corresponds to the assumption that $\ell_0$ also has no predecessor.

The $V$ predicate is used to limit our graph $G_{p^*}$ to terms that appear in the result of our analysis ($\mathbf{img}(p^*)$ by $\mathbf{VBASE}$) or their predecessors through $\mapsto_\#$ ($\mathbf{VREC}$). It notably excludes the intermediate terms that appear in $\mathbf{TJOIN}$ and $\mathbf{TLOC}$. In practice, it means we are defining an equivalence relation on our states $\mathbf{FA.}\Sigma^*$, that relates $\mathbf{Join}$ and its contents, as well as $\mathbf{Loc}$ and its value before renaming; and choosing the $\mathbf{Join}$ and $\mathbf{Loc}$ terms as canonical representatives of their classes.

Finally, $\mathbf{GRAPHGEN}$ defines our new graph $G_{p^*}$: its edges are elements of $\mapsto_\#$ that end in $V$. Using the free algebra domain on its own, this newly generated graph is isomorphic to the input (restricted to reachable locations). It is the same graph, whose vertices have been renamed by $p^*$, as mentioned in the following theorem. This implies there is no abstraction loss when using this domain.

**THEOREM 4.1.** When $p^* = \mathbf{analyse}(\mathbf{FA})$, $G_{p^*}$ is isomorphic to $\mathcal{G}$ (restricted to reachable locations, i.e. locations $\ell$ such that there is a path from $\ell_0$ to $\ell$ in $\mathcal{G}$) via $p^*$:

* $p^*$ is injective (restricted to reachable locations)

* $G_{p^*} = \{(p^*(\ell), R, p^*(\ell')) \mid \mathcal{G}(\ell, R, \ell') \wedge \ell \text{ reachable}\}$

Note that the proof (in Appendix A.2) uses the assumption that outgoing edges of each node are uniquely labelled. Without it, we lose injectivity of $p^*$ as we merge identical children in $G_{p^*}$. $\mathcal{G}$ and $G_{p^*}$ would still be linked via a bisimulation between entry and widening points (where injectivity still holds), similar to that of Theorems 5.5 and 5.6.
## 4.2 Concretization as a set of states

These algebraic locations can be interpreted in different ways. The first, more usual one, is as sets of states in the collecting semantics. It is given by the concretization $\mathbf{FA.}\gamma$ (which matches with the definition of the collecting semantics domain). Notice how the definition of the concretization simply maps our free algebra constructors to the corresponding operation in the collecting semantics. For instance, for the apply operation we have $\mathbf{FA.}\gamma(\mathbf{Apply}(R, s^*)) = \mathbf{CS.}\mathbf{apply}(R, \mathbf{FA.}\gamma(s^*))$.

All FA domain operations are sound. $\mathbf{FA.join}$, $\mathbf{FA.apply}$ and $\mathbf{FA.entry}$ transfer functions are also complete: only $\mathbf{FA.widen}$ loses precision as $\mathbf{Loc}$ concretizes into the entire set of stores $\Sigma$. This concretization can be refined by unfolding the fixed point (replacing $\mathbf{Loc}(\ell)$ with $\mathcal{F}_g(p^*)(\ell)$). The new term will still contain $\mathbf{Loc}(\ell)$ as subterm, which can once again be unfolded, and so on. For the most precise version, unfold until a fixed point is reached here.

## 4.3 Concretization as a program graph

We can also construct a new IMP program graph $G_{p^*} \in \mathbf{FA.}\Sigma^* \times \mathbb{R} \times \mathbf{FA.}\Sigma^* \to \{0; 1\}$ from an abstract element $p^* \in \mathbb{L} \to \mathbf{FA.}\Sigma^*$, or any analysis that uses the free algebra domain as a subdomain. To do so, we define an edge predicate $\mapsto_\# \in (\mathbf{FA.}\Sigma^* \times \mathbb{R} \times \mathbf{FA.}\Sigma^*) \to \{0; 1\}$, and a vertex predicate $V \in \mathbf{FA.}\Sigma^* \to \{0; 1\}$ by the rules at the bottom of Figure 6. Both depend on $p^*$, not included it in their notation to keep them light. See Figure 7 for a small example graph built using these rules.

An $\mathbf{Apply}(R, s^*)$ term represents a vertex (i.e., program location in the new graph) obtained by following an edge labelled by $R$ coming from $s^*$ (rule $TAPPLY$). $\mathbf{TJOIN}$ ensures that all the terms appearing in a $\mathbf{Join}(S^*)$ term correspond to the same program location in the generated program graph, thus, for any edge going to $t^* \in S^*$, it adds an edge going to $\mathbf{Join}(S^*)$. For the $\mathbf{Loc}(\ell)$ case, we need to use the main transfer function $\mathcal{F}_g$ of our abstract interpretation to obtain the pre-state before widening (join of the applys of the predecessors of $\ell$). The rule $\mathbf{TLoc}$ then simply states that the transitions to $\mathbf{Loc}$ are the same as those to that pre-state ($\mathbf{Loc}$ is only introduced at a widening point as a renaming to avoid having recursive terms). Finally, $\mathbf{TSELF}$ ensures that immediate loops ($\ell$ being its own predecessor through a trivial relation) are preserved. Note that $\mathbf{Entry}$ has no predecessor, which corresponds to the assumption that $\ell_0$ also has no predecessor.

The $V$ predicate is used to limit our graph $G_{p^*}$ to terms that appear in the result of our analysis ($\mathbf{img}(p^*)$ by $\mathbf{VBASE}$) or their predecessors through $\mapsto_\#$ ($\mathbf{VREC}$). It notably excludes the intermediate terms that appear in $\mathbf{TJOIN}$ and $\mathbf{TLOC}$. In practice, it means we are defining an equivalence relation on our states $\mathbf{FA.}\Sigma^*$, that relates $\mathbf{Join}$ and its contents, as well as $\mathbf{Loc}$ and its value before renaming; and choosing the $\mathbf{Join}$ and $\mathbf{Loc}$ terms as canonical representatives of their classes.

Finally, $\mathbf{GRAPHGEN}$ defines our new graph $G_{p^*}$: its edges are elements of $\mapsto_\#$ that end in $V$. Using the free algebra domain on its own, this newly generated graph is isomorphic to the input (restricted to reachable locations). It is the same graph, whose vertices have been renamed by $p^*$, as mentioned in the following theorem. This implies there is no abstraction loss when using this domain.

**THEOREM 4.1.** When $p^* = \mathbf{analyse}(\mathbf{FA})$, $G_{p^*}$ is isomorphic to $\mathcal{G}$ (restricted to reachable locations, i.e. locations $\ell$ such that there is a path from $\ell_0$ to $\ell$ in $\mathcal{G}$) via $p^*$:

* $p^*$ is injective (restricted to reachable locations)

* $G_{p^*} = \{(p^*(\ell), R, p^*(\ell')) \mid \mathcal{G}(\ell, R, \ell') \wedge \ell \text{ reachable}\}$

Note that the proof (in Appendix A.2) uses the assumption that outgoing edges of each node are uniquely labelled. Without it, we lose injectivity of $p^*$ as we merge identical children in $G_{p^*}$. $\mathcal{G}$ and $\mathcal{G}_{p^*}$ would still be linked via a bisimulation between entry and widening points (where injectivity still holds), similar to that of Theorems 5.5 and 5.6.
# 5 TRANSFORMATION FUNCTORS AS COMPILER PASSES

A functor F is a function that creates a new IMP domain F(D₁, ..., Dₙ) from a number of IMP domains D₁, ..., Dₙ passed as arguments. Here we are interested in two specific kinds of functors: transformation functors, which only change the apply operation, and product functors which combine domains. We exhibit a criteria for soundness and completeness of such functors, and show how applying sound (resp. complete) functors to the free algebra domain lead to a forward (resp. backward) simulation between the widening points in the input and generated programs.

We say that an n-ary functor F is sound when for all sound domains D₁, ..., Dₙ, the domain F(D₁, ..., Dₙ) is also sound. Similarly, we say that F is complete when for all complete domains D₁, ..., Dₙ, the domain F(D₁, ..., Dₙ) is also complete. Note that functor soundness and completeness are compositional: if F and G are sound (or complete), then so is D ↦ F(G(D)).

## 5.1 Transformation functors

Transformation functors are used to perform small, statement level transformations of our programs. Formally, a transformation functor F is any functor that (1) only modifies the apply operation of its argument D and (2) can only create values of type D.Σ# through the domain operations of D: specifically only D.**apply** and D.**join**. This means that all domain components other than apply are equal to those of D; notably, F(D).Σ# = D.Σ#. Furthermore, F(D).**apply**(R, s#) returns a combination of D.**apply**, D.**join**, and s#. The specific combination depends on R and s#. Using an opaque type, it is quite easy to enforce this constraint in code.

The state s# can only be inspected through sound queries. We write s# ⊢ P when all elements abstracted by s# ∈ D.Σ# satisfy predicate P ∈ Σ → {0; 1}, i.e. s# ⊢ P implies ∀σ ∈ D.γ(s#), P(σ). For instance s# ⊢ [σ ∈ Σ ↦ σ(x) = 0] means variable x is zero in all elements abstracted by s#. As the full function definition of P is a bit heavy, we abbreviate it as s# ⊢ σ(x) = 0. Note that not having s# ⊢ P does not mean the property is false on D.γ(s#).

**Example 5.1 (Division guard functor).** A simple example of a transformation is the division guard functor (DG), which adds an assertion “divisor is not 0” before every division:

$$
\begin{align*}
\mathit{safe}(\{e_1; \dots; e_n\}, s^#) &\triangleq \mathit{D.apply}(\mathit{If } e_1 \neq 0, \dots \mathit{D.apply}(\mathit{If } e_n \neq 0, s^#) \dots) \\
\mathit{DG}(\mathit{D}).\mathit{apply}(\mathit{If } e, s^#) &\triangleq \mathit{D.apply}(\mathit{If } e, \mathit{safe}(\mathit{divisors}(e), s^#)) \\
\mathit{DG}(\mathit{D}).\mathit{apply}(x := e, s^#) &\triangleq \mathit{D.apply}(x := e, \mathit{safe}(\mathit{divisors}(e), s^#))
\end{align*}
$$

where divisors ∈ E → ℙ(E) is the set of sub-expressions that appear to the right of a division or modulo operation in e. Furthermore, we extend apply so that apply(⊥, ⊥) ≜ ⊥. This way, safe ∈ ℙ(E) × D.Σ# → D.Σ# ⊥ adds a guard for each expression in its argument set<fnref n="7" />.

**Example 5.2 (Ternary expression rewrite functor).** A more complex example is the ternary rewrite functor (T), which replaces the ternary if-then-else in expressions by explicit jumps. The full definition is a bit technical, but for a single ternary expression, it can be defined as:

$$
T(D).\mathit{apply}(\mathit{If } (e_c ? e_t : e_e), s^#) \triangleq D.\mathit{apply}\left(\mathit{If } t, D.\mathit{join}\left(\begin{array}{@{}l@{}} D.\mathit{apply}(t := e_t, D.\mathit{apply}(\mathit{If } e_c, s^#)); \\ D.\mathit{apply}(t := e_e, D.\mathit{apply}(\mathit{If } e_c = 0, s^#)) \end{array}\right)\right)
$$

where t /∈ ℥ is a new, fresh variable. This example shows that transformation functors can change the type of program relations (in this case, we remove a construct and add a variable). The new variable requires changing the concretization as well: T(D).γ(s#) is the same as D.γ(s#) but removes t from the store.

<footnote n="7">⁷To avoid issues with nested divisions, the set passed to safe should be sorted in increasing size of terms.</footnote>
# 5 TRANSFORMATION FUNCTORS AS COMPILER PASSES

A functor F is a function that creates a new IMP domain F(D₁, ..., Dₙ) from a number of IMP domains D₁, ..., Dₙ passed as arguments. Here we are interested in two specific kinds of functors: transformation functors, which only change the apply operation, and product functors which combine domains. We exhibit a criteria for soundness and completeness of such functors, and show how applying sound (resp. complete) functors to the free algebra domain lead to a forward (resp. backward) simulation between the widening points in the input and generated programs.

We say that an n-ary functor F is sound when for all sound domains D₁, ..., Dₙ, the domain F(D₁, ..., Dₙ) is also sound. Similarly, we say that F is complete when for all complete domains D₁, ..., Dₙ, the domain F(D₁, ..., Dₙ) is also complete. Note that functor soundness and completeness are compositional: if F and G are sound (or complete), then so is D ↦ F(G(D)).

## 5.1 Transformation functors

Transformation functors are used to perform small, statement level transformations of our programs. Formally, a transformation functor F is any functor that (1) only modifies the apply operation of its argument D and (2) can only create values of type D.Σ# through the domain operations of D: specifically only D.**apply** and D.**join**. This means that all domain components other than apply are equal to those of D; notably, F(D).Σ# = D.Σ#. Furthermore, F(D).**apply**(R, s#) returns a combination of D.**apply**, D.**join**, and s#. The specific combination depends on R and s#. Using an opaque type, it is quite easy to enforce this constraint in code.

The state s# can only be inspected through sound queries. We write s# ⊢ P when all elements abstracted by s# ∈ D.Σ# satisfy predicate P ∈ Σ → {0; 1}, i.e. s# ⊢ P implies ∀σ ∈ D.γ(s#), P(σ). For instance s# ⊢ [σ ∈ Σ ↦ σ(x) = 0] means variable x is zero in all elements abstracted by s#. As the full function definition of P is a bit heavy, we abbreviate it as s# ⊢ σ(x) = 0. Note that not having s# ⊢ P does not mean the property is false on D.γ(s#).

**Example 5.1 (Division guard functor).** A simple example of a transformation is the division guard functor (DG), which adds an assertion “divisor is not 0” before every division:

$$ 
\begin{align*}
\mathit{safe}(\{e_1; \dots; e_n\}, s^#) &\triangleq \mathit{D.apply}(\mathit{If } e_1 \neq 0, \dots \mathit{D.apply}(\mathit{If } e_n \neq 0, s^#) \dots) \\
\mathit{DG}(\mathit{D}).\mathit{apply}(\mathit{If } e, s^#) &\triangleq \mathit{D.apply}(\mathit{If } e, \mathit{safe}(\mathit{divisors}(e), s^#)) \\
\mathit{DG}(\mathit{D}).\mathit{apply}(x := e, s^#) &\triangleq \mathit{D.apply}(x := e, \mathit{safe}(\mathit{divisors}(e), s^#))
\end{align*}
$$

where divisors ∈ E → ℙ(E) is the set of sub-expressions that appear to the right of a division or modulo operation in e. Furthermore, we extend apply so that apply(⊥, ⊥) ≜ ⊥. This way, safe ∈ ℙ(E) × D.Σ# → D.Σ# ⊥ adds a guard for each expression in its argument set<fnref n="7" />.

**Example 5.2 (Ternary expression rewrite functor).** A more complex example is the ternary rewrite functor (T), which replaces the ternary if-then-else in expressions by explicit jumps. The full definition is a bit technical, but for a single ternary expression, it can be defined as:

$$ T(D).\mathit{apply}(\mathit{If } (e_c ? e_t : e_e), s^#) \triangleq \mathit{D.} \mathit{apply} \left( \mathit{If } t, \mathit{D.} \mathit{join} \left( \begin{array}{@{}l@{}} \mathit{D.} \mathit{apply}(t := e_t, \mathit{D.} \mathit{apply}(\mathit{If } e_c, s^#)); \\ \mathit{D.} \mathit{apply}(t := e_e, \mathit{D.} \mathit{apply}(\mathit{If } e_c = 0, s^#)); \end{array} \right) \right) $$

where t /∈ ℥ is a new, fresh variable. This example shows that transformation functors can change the type of program relations (in this case, we remove a construct and add a variable). The new variable requires changing the concretization as well: T(D).γ(s#) is the same as D.γ(s#) but removes t from the store.

<footnote n="7">⁷To avoid issues with nested divisions, the set passed to safe should be sorted in increasing size of terms.</footnote>
<figure><img src="image_6.png" /><figcaption>Fig. 7. Example compilation of the small program “r := b%2 ? r × a : r” through the division guard and ternary functors (analyse(DG(T(FA)))). We use T, U, V and W as short names for legibility.</figcaption></figure>

Figure 7 shows the result of compiling a simple program (a single assignment) through the ternary rewrite (T) and division guard (DG) functors, applied to the free algebra (FA) domain of Section 4.

*Example 5.3 (Query simplification functor)*. Both previous examples only perform syntactic transformations: their *apply* does not inspect the program state. A simple functor that does this is the *query simplification functor*:

$$
\begin{align*}
Q(D).\text{apply}(x := e, s^#) \triangleq \begin{cases}
\perp & \text{if } s^# \models \hat{\mathcal{E}}[e](\sigma) = \perp \\
s^# & \text{if } s^# \models \sigma(x) = \hat{\mathcal{E}}[e](\sigma) \\
\text{D. apply}(x := z, s^#) & \text{if } \exists z, s^# \models \hat{\mathcal{E}}[e](\sigma) = z \\
\text{D. apply}(x := e, s^#) & \text{otherwise}
\end{cases} \\
Q(D).\text{apply}(\text{If } e, (s^#, \sigma^#)) \triangleq \begin{cases}
\perp & \text{if } s^# \models \hat{\mathcal{E}}[e](\sigma) \subseteq \{0; \perp\} \\
s^# & \text{if } s^# \models \hat{\mathcal{E}}[e](\sigma) \neq 0 \\
\text{D. apply}(\text{If } e, s^#) & \text{otherwise}
\end{cases}
\end{align*}
$$

This simplifies an assignment to $\perp$ if one of the variables has no valid values; removes it if it doesn't change the value of $x$; simplifies it if the expression $e$ has a constant value (thus performing constant propagation); and leaves it unchanged otherwise. For guards, it checks if the condition is false, in which case it returns $\perp$; or true, in which case it removes the guard. Q works well with the numerical domain, since queries using $\hat{\mathcal{E}}[\cdot]$ can be computed using the forward evaluation function $\vec{\mathcal{E}}[\cdot]$ (for example $\sigma^# \models \hat{\mathcal{E}}[e](\sigma) = 0$ is simply $\vec{\mathcal{E}}[e](\sigma^#) = [0:0]$)

This definition for transformation functors is quite restrictive. They only act on a single relation, and not on multiple statements. For example, they cannot simplify double assignments ($x := 0$ followed by $x := 1$) or change order of assignments. However, our SSA translation will perform these automatically by grouping assignments in blocks of bindings.

On the other hand, their simplicity allows proving some strong results. The following lemma shows that it suffices to prove soundness (respectively, completeness) of the functor applied to the collecting semantics domain (CS) to prove soundness (respectively, completeness) for any domain given as an argument.

**LEMMA 5.4 (FUNCTOR SOUNDNESS AND COMPLETENESS).** *A transformation functor $F$ is sound if and only if $F(CS)$ is sound. Similarly, $F$ is complete if and only if $F(CS)$ is complete.*

See proof in Appendix A.3. All three examples above are both sound and complete functors.

When proving soundness (or completeness) of a $F(CS)$, one must take care to only use query soundness results ($s^# \models P \Rightarrow P(s^#)$), and not completeness, as queries may be false even when $P$ is always true. For instance, to prove soundness of a functor that looks like

$$
F(CS).\text{apply}(R, s^#) \triangleq \begin{cases} \dots & \text{if } s^# \models \text{true} \\ \dots & \text{otherwise} \end{cases}
$$
<figure><img src="image_8.png" /><figcaption>Fig. 7. Example compilation of the small program “r := b%2 ? r × a : r” through the division guard and ternary functors (analyse(DG(T(FA)))). We use T, U, V and W as short names for legibility.</figcaption></figure>

Figure 7 shows the result of compiling a simple program (a single assignment) through the ternary rewrite (T) and division guard (DG) functors, applied to the free algebra (FA) domain of Section 4.

*Example 5.3 (Query simplification functor)*. Both previous examples only perform syntactic transformations: their *apply* does not inspect the program state. A simple functor that does this is the *query simplification functor*:

$$ \begin{array}{r@{\quad}l} \mathcal{Q}(\mathcal{D}).\mathit{apply}(x := e, s^#) \triangleq & \left\{ \begin{array}{ll} \perp & \text{if } s^# \models \hat{\mathcal{E}}[e](\sigma) = \perp \\ s^# & \text{if } s^# \models \sigma(x) = \hat{\mathcal{E}}[e](\sigma) \\ \mathcal{D}.\mathit{apply}(x := z, s^#) & \text{if } \exists z, s^# \models \hat{\mathcal{E}}[e](\sigma) = z \\ \mathcal{D}.\mathit{apply}(x := e, s^#) & \text{otherwise} \end{array} \right. \\ \\ \mathcal{Q}(\mathcal{D}).\mathit{apply}(\mathit{If } e, (s^#, s^#)) \triangleq & \left\{ \begin{array}{ll} \perp & \text{if } s^# \models \hat{\mathcal{E}}[e](\sigma) \subseteq \{0; \perp\} \\ s^# & \text{if } s^# \models \hat{\mathcal{E}}[e](\sigma) \neq 0 \\ \mathcal{D}.\mathit{apply}(\mathit{If } e, s^#) & \text{otherwise} \end{array} \right. \end{array} $$

This simplifies an assignment to $\perp$ if one of the variables has no valid values; removes it if it doesn't change the value of $x$; simplifies it if the expression $e$ has a constant value (thus performing constant propagation); and leaves it unchanged otherwise. For guards, it checks if the condition is false, in which case it returns $\perp$; or true, in which case it removes the guard. $\mathcal{Q}$ works well with the numerical domain, since queries using $\hat{\mathcal{E}}[\cdot]$ can be computed using the forward evaluation function $\vec{\mathcal{E}}[\cdot]$ (for example $\sigma^# \models \hat{\mathcal{E}}[e](\sigma) = 0$ is simply $\vec{\mathcal{E}}[e](\sigma^#) = [0:0]$)

This definition for transformation functors is quite restrictive. They only act on a single relation, and not on multiple statements. For example, they cannot simplify double assignments ($x := 0$ followed by $x := 1$) or change order of assignments. However, our SSA translation will perform these automatically by grouping assignments in blocks of bindings.

On the other hand, their simplicity allows proving some strong results. The following lemma shows that it suffices to prove soundness (respectively, completeness) of the functor applied to the collecting semantics domain (CS) to prove soundness (respectively, completeness) for any domain given as an argument.

**LEMMA 5.4 (FUNCTOR SOUNDNESS AND COMPLETENESS).** *A transformation functor $\mathcal{F}$ is sound if and only if $\mathcal{F}(\mathcal{CS})$ is sound. Similarly, $\mathcal{F}$ is complete if and only if $\mathcal{F}(\mathcal{CS})$ is complete.*

See proof in Appendix A.3. All three examples above are both sound and complete functors.

When proving soundness (or completeness) of a $\mathcal{F}(\mathcal{CS})$, one must take care to only use query soundness results ($s^# \models P \Rightarrow P(s^#)$), and not completeness, as queries may be false even when $P$ is always true. For instance, to prove soundness of a functor that looks like

$$ \mathcal{F}(\mathcal{CS}).\mathit{apply}(R, s^#) \triangleq \left\{ \begin{array}{ll} \dots & \text{if } s^# \models \text{true} \\ \dots & \text{otherwise} \end{array} \right. $$
we must prove soundness in the first branch (restricted to elements that satisfy P) and in the second branch. We cannot use the information “true is true on all elements of $s^*$” to skip the proof of the second branch, as the query may return false.

## 5.2 Simulation theorems

Applying a transformation functor can be seen as a statement-level compiler pass. These passes can perform syntactic transformations (by inspecting the relation), semantic ones (through queries on the input states), or combine both. Since functor soundness and completeness are compositional, we can easily define each small transformation we want to perform as a functor, prove that these functors are sound (or complete) individually, and obtain the result for the whole chain.

Let us take a transformation functor F, we are interested the program generated by the free algebra domain under F. We write $p^\# = \text{analyse}(F(\text{FA}))$ the analysis result, and $\rightarrow_{G_{p^\#}}$ the transition system associated with the new IMP program $G_{p^\#}$ generated by the free algebra domain.

**THEOREM 5.5 (SOUND FUNCTOR FORWARD SIMULATION).** If F is a sound transformation functor, then for all reachable pairs $(\ell, \sigma)$ and $(\ell', \sigma')$ such that $\ell$ and $\ell'$ are the entrypoint or widening points:

$$ (\ell, \sigma) \rightarrow_G^+ (\ell', \sigma') \Rightarrow (p^\#(\ell), \sigma) \rightarrow_{G_{p^\#}}^+ (p^\#(\ell'), \sigma') $$

**THEOREM 5.6 (COMPLETE FUNCTOR BACKWARD SIMULATION).** If F is a complete transformation functor, then for all entry or widening points $\ell, \ell'$, and for all $\sigma, \sigma'$:

$$ (p^\#(\ell), \sigma) \rightarrow_{G_{p^\#}}^+ (p^\#(\ell'), \sigma') \Rightarrow (\ell, \sigma) \rightarrow_G^+ (\ell', \sigma') $$

See proofs in Appendix A.3.

## 5.3 Product functors

Reduced domain products [Cousot and Cousot 1979] are a classical tool to combine domains. The basic product is a two argument functor. It returns a domain whose state is a pair of the states of its arguments; whose operations are the pairwise lifting the argument operation; and whose concretization is the intersection of their concretizations. We denote it with the infix $\times$.

Simply using this is equivalent to running the two analysis independently. For added benefit, add a query simplification functor Q on top of the product. Queries can then use information from both states to simplify the terms, and thus prove results that each individual domain could not.

A product between the free algebra domain and another domain can still generate a program graph. The rules TLOC and TSELF just need to be adapted a little as $F_g(p^\#)(\ell)$ is no longer a free algebra state, but a pair containing such a state, so we need to add a simple projection.

# 6 SSA SIGNATURE AND SSA FREE ALGEBRA

This section presents our SSA language, highlighting the differences to IMP. It then presents an abstract domain signature adapted to this language (similarly to the IMP signature in Figure 4) and a free algebra implementation of this signature (similar to the one from Section 4).

## 6.1 SSA syntax and semantics

We use the syntax and semantics of SSA (Figure 8) defined by Lemerre [2023] (corresponding to a high-level representation of the sea-of-nodes representation [Click and Paleczny 1995; Demange et al. 2018]), with small variations.

**Syntax.** An SSA expression $\hat{e} \in \hat{\mathbb{E}}^8$ is similar to a program expression $e \in \mathbb{E}$ but without the ternary if-then-else. SSA variables are composed of an identifier $i \in \mathbb{I}$ and a location $\hat{i} \in \hat{\mathbb{I}}$, which

<footnote n="8">⁸We use a hat $^\hat{}$ notation to differentiate SSA-specific objects from their IMP counterparts.</footnote>
we must prove soundness in the first branch (restricted to elements that satisfy P) and in the second branch. We cannot use the information “true is true on all elements of $s^*$” to skip the proof of the second branch, as the query may return false.

## 5.2 Simulation theorems

Applying a transformation functor can be seen as a statement-level compiler pass. These passes can perform syntactic transformations (by inspecting the relation), semantic ones (through queries on the input states), or combine both. Since functor soundness and completeness are compositional, we can easily define each small transformation we want to perform as a functor, prove that these functors are sound (or complete) individually, and obtain the result for the whole chain.

Let us take a transformation functor F, we are interested the program generated by the free algebra domain under F. We write $p^\# = \text{analyse}(F(\text{FA}))$ the analysis result, and $\rightarrow_{G_{p^\#}}$ the transition system associated with the new IMP program $G_{p^\#}$ generated by the free algebra domain.

**THEOREM 5.5 (SOUND FUNCTOR FORWARD SIMULATION).** If F is a sound transformation functor, then for all reachable pairs $(\ell, \sigma)$ and $(\ell', \sigma')$ such that $\ell$ and $\ell'$ are the entrypoint or widening points:

$$ (\ell, \sigma) \rightarrow_{G}^{+} (\ell', \sigma') \Rightarrow (p^{\#}(\ell), \sigma) \rightarrow_{G_{p^{\#}}}^{+} (p^{\#}(\ell'), \sigma') $$

**THEOREM 5.6 (COMPLETE FUNCTOR BACKWARD SIMULATION).** If F is a complete transformation functor, then for all entry or widening points $\ell, \ell'$, and for all $\sigma, \sigma'$:

$$ (p^{\#}(\ell), \sigma) \rightarrow_{G_{p^{\#}}}^{+} (p^{\#}(\ell'), \sigma') \Rightarrow (\ell, \sigma) \rightarrow_{G}^{+} (\ell', \sigma') $$

See proofs in Appendix A.3.

## 5.3 Product functors

Reduced domain products [Cousot and Cousot 1979] are a classical tool to combine domains. The basic product is a two argument functor. It returns a domain whose state is a pair of the states of its arguments; whose operations are the pairwise lifting the argument operation; and whose concretization is the intersection of their concretizations. We denote it with the infix $\times$.

Simply using this is equivalent to running the two analysis independently. For added benefit, add a query simplification functor Q on top of the product. Queries can then use information from both states to simplify the terms, and thus prove results that each individual domain could not.

A product between the free algebra domain and another domain can still generate a program graph. The rules TLOC and TSELF just need to be adapted a little as $\mathcal{F}_g(p^\#)(\ell)$ is no longer a free algebra state, but a pair containing such a state, so we need to add a simple projection.

# 6 SSA SIGNATURE AND SSA FREE ALGEBRA

This section presents our SSA language, highlighting the differences to IMP. It then presents an abstract domain signature adapted to this language (similarly to the IMP signature in Figure 4) and a free algebra implementation of this signature (similar to the one from Section 4).

## 6.1 SSA syntax and semantics

We use the syntax and semantics of SSA (Figure 8) defined by Lemerre [2023] (corresponding to a high-level representation of the sea-of-nodes representation [Click and Paleczny 1995; Demange et al. 2018]), with small variations.

**Syntax.** An SSA expression $\hat{e} \in \hat{\mathbb{E}}^8$ is similar to a program expression $e \in \mathbb{E}$ but without the ternary if-then-else. SSA variables are composed of an identifier $i \in \mathbb{I}$ and a location $\hat{i} \in \hat{\mathbb{I}}$, which

<footnote n="8">⁸We use a hat $\hat{}$ notation to differentiate SSA-specific objects from their IMP counterparts.</footnote>
<table><tr><td>i &isin; &#8468; (Identifiers)</td><td>&ell;&#770; &isin; &#8468; (Locations)</td><td>i<sub>&ell;</sub> &isin; &#8475; &asymp; &#8468; &times; &#8468; (Variables)</td><td>&Gamma; &asymp; &#8475; &rarr; &#8469; (Valuation)</td></tr><tr><td>&epsilon; &isin; &#8469; &asymp; z | i<sub>&ell;</sub> | &epsilon; &diamond; &epsilon; (SSA expression)</td><td>B &asymp; B &asymp; &#8475; &rarr; &epsilon; (Bindings)</td><td>R&#770; &asymp; R&#770; &asymp; &Imacr;f &epsilon; | Bind(B)</td><td></td></tr><tr><td>G&#770; &asymp; (&#8469; &times; R&#770; &times; &#8469;) &rarr; {0; 1} (SSA graph)</td><td>S&#770; &asymp; &#8469; &times; &#8468; (SSA state)</td><td></td><td></td></tr></table>

<table><caption>Fig. 8. SSA language syntax (top) and semantics (bottom).</caption><tr><td>scope<sub>G&#770;</sub> &isin; &#8469; &rarr; P(<span style="text-decoration: overline;">&#8469;</span>)</td><td>scope<sub>G&#770;</sub>(i<sub>&ell;</sub>) &asymp; {<sub>&ell;&#770;</sub> &isin; <span style="text-decoration: overline;">&#8469;</span> | <sub>&ell;</sub> dominates <sub>&ell;&#770;</sub> in <span style="text-decoration: overline;">G&#770;</span>}</td></tr><tr><td>unbind<sub>G&#770;</sub> &isin; <span style="text-decoration: overline;">&#8469;</span> &times; &#8468; &rarr; &#8468;</td><td>unbind<sub>G&#770;</sub>(<span style="text-decoration: overline;">&ell;</span>, &Gamma;) &asymp; [<span style="text-decoration: overline;">&x;&#770;</span> &isin; dom &Gamma; &mapsto; &Gamma;(v) | <sub>&ell;</sub> &isin; scope<sub>G&#770;</sub>(<span style="text-decoration: overline;">x;&#770;</span>)]</td></tr><tr><td>bind &isin; B &times; &#8468; &rarr; &#8468;</td><td>bind(B, &Gamma;) &asymp; [<span style="text-decoration: overline;">&x;&#770;</span> &isin; &#8475; &mapsto; [<span style="text-decoration: overline;">&xi;&#770;</span>[[B(<span style="text-decoration: overline;">x;&#770;</span>)]](&Gamma;) if <span style="text-decoration: overline;">x;&#770;</span> &isin; dom B<br>&Gamma;(<span style="text-decoration: overline;">x;&#770;</span>) otherwise]</td></tr><tr><td>~&rarr;<sub>G&#770;</sub> &isin; S&#770; &times; S&#770;</td><td>(<span style="text-decoration: overline;">&ell;</span>, &Gamma;) ~&rarr;<sub>G&#770;</sub> (<sub>&ell;&#770;</sub>, &Gamma;') &asymp; &exist; &epsilon;, <span style="text-decoration: overline;">G&#770;</span>(<span style="text-decoration: overline;">&ell;</span>, &Imacr;f &epsilon;, <sub>&ell;&#770;</sub>) &wedge; &Gamma;' = &Gamma; &wedge; <span style="text-decoration: overline;">&xi;&#770;</span>[[&epsilon;]](Gamma) &notin; {0; &#8469;}<br>&ve; &exist; B, <span style="text-decoration: overline;">G&#770;</span>(<span style="text-decoration: overline;">&ell;</span>, Bind(B), <sub>&ell;&#770;</sub>) &wedge; &Gamma;' = unbind<sub>G&#770;</sub>(<span style="text-decoration: overline;">&ell;&#770;</span>, bind(B, &Gamma;))</td></tr></table>

determines its *scope*, i.e., the set of locations where the variable can appear. For simplicity in this paper, we choose $\mathcal{I} = \mathcal{X}$, i.e., the SSA variable $x_{\ell}$ can be understood as the value of IMP variable $x$ at location $\ell$.

In an SSA graph $\hat{G} \in \hat{G}$, edges are either annotated by expressions $(\hat{I}f \hat{e})$, representing a condition, or bindings $(\text{Bind}(B))$ mapping multiple variables to expressions. We denote by $\ell_0$ the initial location where SSA programs start. We require that bindings edges are exactly those leading into a join node (node with multiple predecessors). Furthermore, an SSA variable $x_{\ell}$ should only appear in the bindings leading into the join node at location $\ell$ (location where it is bound), and it should appear in all the bindings leading into $\ell$ (all bindings leading into a join node have the same domain). Thus, join nodes represent both program joins and what traditional SSA denotes by $\phi$ functions. If $\ell$ has two predecessors $\hat{G}(\ell', \text{Bind}([\hat{x} \mapsto \hat{e}]), \ell)$ and $\hat{G}(\ell'', \text{Bind}([\hat{x} \mapsto \hat{e'}]), \ell)$, then the scope of $\hat{x}$ is $\ell$. In traditional SSA, $\hat{x}$ would be bound here to $\phi(\hat{e}, \hat{e}')$. Two example SSA graphs are given in Figure 2c (where $\hat{I}f$ and $\text{Bind}$ constructors have been left implicit).

**Semantics.** The interpretation of SSA expressions $\hat{E}[[\cdot]]$ is similar to that of IMP expressions $\mathcal{E}[[\cdot]]$. The semantics of SSA is given as a transition system $(\hat{S}, \rightsquigarrow)$ between SSA states. Given an SSA graph $\hat{G}$, there is a transition $(\hat{I}, \Gamma) \rightsquigarrow \hat{G}$ ($\hat{I}', \Gamma'$) if there is an edge $\hat{G}(\hat{I}, \hat{R}, \hat{I}')$ and the edge $\hat{R}$ is either a condition that evaluates to non-zero, or a binding, which is then evaluated and added to the environment.

We also have an unbinding operation that removes variables that are no longer in scope from the environment (where scope is defined using domination between locations). It is not necessary (SSA variables can be seen as assigned rather than bound [Schneider 2013]) but will help analyses, as it avoids maintaining information about useless variables. Unbinding only occurs at join nodes (whose incoming edges are annotated by bindings), since non-join nodes only have a single predecessor and thus only grow in scope.

## 6.2 SSA domain signature

The signature of SSA domains is given in Figure 9. It is similar to the previous signature of Figure 4 with a few key variations. The only relations applied on SSA are guards. To emphasize this, we rename *apply* to *assûme*. Since bindings only occur before joins, we place them directly in the signature of *join*. It no longer takes a set of states as argument, but a set of states paired with their respective bindings. Once again, all bindings given to a join should have the same domain (define the same variables). For example, *join* {([x&#770; &mapsto; 3], &Gamma;#); ([x&#770; &mapsto; 5], &Gamma;#)} is the merging of two branches
$\Gamma^{\#} \in \Gamma^{\#} \quad (\text{set of abstract states})$

$\mathit{entry} \in \Gamma^{\#}$

$\mathit{assûme} \in \hat{\mathbb{E}} \times \Gamma^{\#} \to \Gamma_{\perp}^{\#}$

$\mathit{join} \in \mathcal{P}_f(\mathbb{B} \times \Gamma^{\#}) \to \Gamma_{\perp}^{\#}$

$\mathit{widen} \in W \times \Gamma^{\#} \times \Gamma^{\#} \to \Gamma^{\#}$

$\hat{\gamma} \in \Gamma^{\#} \to \mathcal{P}(\Gamma)$

$$
\begin{array}{l}
\hat{\mathcal{F}}_{\hat{g}} \in (\hat{\mathbb{L}} \to \mathit{D.}\Gamma^{\#}) \to (\hat{\mathbb{L}} \to \mathit{D.}\Gamma^{\#}) \\
\hat{\mathcal{F}}_{\hat{g}}(\hat{p}^{\#}) \triangleq \hat{\ell}_{0} \mapsto \mathit{D.}\mathit{entry} \\
\quad \hat{\ell} \mapsto \mathit{D.}\mathit{assûme}(\hat{e}, \hat{p}^{\#}(\hat{\ell}')) \quad \text{if } \hat{\mathcal{G}}(\hat{\ell}', \hat{\mathbb{L}}\hat{e}, \hat{\ell}) \wedge \hat{\ell}' \in \mathit{dom} \hat{p}^{\#} \\
\quad \hat{\ell} \mapsto \mathit{D.}\mathit{join} \{(B_k, \hat{p}^{\#}(\hat{k})) \mid (\hat{k}, B_k) \text{ such that } \hat{\mathcal{G}}(\hat{k}, \mathit{Bind}(B_k), \hat{\ell}) \wedge \hat{k} \in \mathit{dom} \hat{p}^{\#}\}
\end{array}
$$

<caption>Fig. 9. SSA abstract domain signature (top) and abstract interpretation (bottom)</caption>

$$
\begin{array}{l}
\Gamma^{\#} \in \widehat{\mathbb{A}}.\Gamma^{\#} \triangleq \mathit{En\acute{t}ry} | \mathit{Ass\acute{u}me}(\hat{e}, \Gamma^{\#}) | \mathit{Jo\^in}(C^{\#}) | \mathit{L\^oc}(\ell) \quad (\text{SSA algebraic locations}) \\
\text{where } \hat{e} \in \hat{\mathbb{E}} \text{ and } C^{\#} \in \mathcal{P}_f(\mathbb{B} \times \widehat{\mathbb{A}}.\Gamma^{\#})
\end{array}
$$

$$
\begin{align*}
\widehat{\mathbb{A}}.\mathit{entry} &\triangleq \mathit{En\acute{t}ry} \\
\widehat{\mathbb{A}}.\mathit{assûme}(\hat{e}, \Gamma^{\#}) &\triangleq \mathit{Assûme}(\hat{e}, \Gamma^{\#}) \\
\widehat{\mathbb{A}}.\mathit{widen}(\ell, \_, \_) &\triangleq \mathit{L\^oc}(\ell) \\
\widehat{\mathbb{A}}.\hat{\mathcal{Y}}(\mathit{En\acute{t}ry}) &\triangleq \Gamma \\
\widehat{\mathbb{A}}.\hat{\mathcal{Y}}(\mathit{Assûme}(\hat{e}, \Gamma^{\#})) &\triangleq \{\Gamma \in \widehat{\mathbb{A}}.\hat{\mathcal{Y}}(\Gamma^{\#}) \mid \hat{\mathcal{E}}[\hat{e}](\Gamma) \neq 0\} \\
\widehat{\mathbb{A}}.\hat{\mathcal{Y}}(\mathit{Jo\^in}(C^{\#})) &\triangleq \bigcup_{B, \Gamma^{\#} \in C^{\#}} \{\mathit{bind}(B, \Gamma) \mid \Gamma \in \widehat{\mathbb{A}}.\hat{\mathcal{Y}}(C^{\#})\} \\
\widehat{\mathbb{A}}.\hat{\mathcal{Y}}(\mathit{L\^oc}(\ell)) &\triangleq \Gamma
\end{align*}
$$

$$
\begin{array}{c}
\text{TASSUMESSA} \\
\Gamma^{\#} \stackrel{\hat{\ell} \frown \hat{e}}{\rightleftharpoons} \# \text{Assûme}(\hat{e}, \Gamma^{\#})
\end{array}
$$

$$
\begin{array}{l}
\text{TJOINSSA} \\
(B, \Gamma^{\#}) \in C^{\#} \\
\Gamma^{\#} \stackrel{\text{Bind}(B)}{\rightleftharpoons} \# \text{Join}(C^{\#})
\end{array}
$$

$$
\begin{array}{l}
\text{TLocSSA} \\
\Gamma^{\#} \stackrel{\hat{R}}{\rightleftharpoons} \# \hat{\mathcal{F}}_{\hat{g}}(\hat{p}^{\#})(\hat{\ell}) \\
\Gamma^{\#} \stackrel{\hat{R}}{\rightleftharpoons} \# \text{L\^oc}(\hat{\ell})
\end{array}
$$

<caption>Fig. 10. The free algebra SSA abstract domain ($\widehat{\mathbb{A}}$) (top) and rules for generating SSA programs (bottom).</caption>

$\Gamma^{\#}$ and $\Gamma'^{\#}$ with the additional information that $\hat{x}$ is 3 when coming from $\Gamma^{\#}$ and 5 when coming from $\Gamma'^{\#}$. This is how we represent what traditional SSA would denote with a $\phi$ function: $\hat{x} \mapsto \phi(3, 5)$. Note that this signature makes some constraints placed on our SSA programs explicit: it is clear that assume nodes have a single predecessor labelled by a guard, and join nodes have multiple predecessors labelled by bindings.

$\hat{\mathcal{F}}_{\hat{g}}$ is the transfer function used for the direct analysis of SSA programs. It is similar to $\mathcal{F}_g$, but explicitly separates treatment of guard edges (with *assûme*) and bindings before a join (with *join*), whereas $\mathcal{F}_g$ performed both simultaneously using a *join* of *applies*. The other components of our analysis ($\nabla_W$ and *analyse*) are the same as in Figure 4.

The SSA domain also has soundness and correction hypothesis similar to those of the IMP domain in Figure 4, omitted here for the sake of brevity.

6.3 Free algebra of the SSA domain signature

Figure 10 presents the *free algebra* SSA domain, denoted $\widehat{\mathbb{A}}$. Just like in IMP free algebra (Section 4), the domain operation simply create terms using the relevant function symbols.

This domain also presents a dual interpretation as sets of valuations (given by the concretization
$\widehat{\mathbb{A}}.\hat{\mathcal{Y}}$) and as a program graph (given by the edge predicate $\coeur{\#} \in (\widehat{\mathbb{A}}.\Gamma^{\#} \times \hat{\mathbb{R}} \times \widehat{\mathbb{A}}.\Gamma^{\#}) \to \{0; 1\}$).
The rules for generating this graph are similar to those of the IMP free algebra. Note that contrary
to TJOIN, where a Join had the same predecessors as its elements, here the Join's predecessors are
$\Gamma^{\#} \in \Gamma^{\#} \quad (\text{set of abstract states})$

$\text{entr}'y \in \Gamma^{\#}$

$\text{ass}'ume \in \hat{\mathbb{E}} \times \Gamma^{\#} \to \Gamma_{\perp}^{\#}$

$\text{join} \in \mathcal{P}_f(\mathbb{B} \times \Gamma^{\#}) \to \Gamma_{\perp}^{\#}$

$\text{widen} \in W \times \Gamma^{\#} \times \Gamma^{\#} \to \Gamma^{\#}$

$\hat{\gamma} \in \Gamma^{\#} \to \mathcal{P}(\Gamma)$

$$
\begin{array}{l}
\hat{\mathcal{F}}_{\hat{g}} \in (\hat{\mathbb{L}} \to \mathrm{D.}\Gamma^{\#}) \to (\hat{\mathbb{L}} \to \mathrm{D.}\Gamma^{\#}) \\
\hat{\mathcal{F}}_{\hat{g}}(\hat{p}^{\#}) \triangleq \hat{\ell}_{0} \mapsto \mathrm{D.entr}'y \\
\quad \hat{\ell} \mapsto \mathrm{D.ass}'ume(\hat{e}, \hat{p}^{\#}(\hat{\ell}')) \quad \text{if } \hat{\mathcal{G}}(\hat{\ell}', \hat{\mathrm{If}} \hat{e}, \hat{\ell}) \wedge \hat{\ell}' \in \mathrm{dom} \hat{p}^{\#} \\
\quad \hat{\ell} \mapsto \mathrm{D.}join \{(B_k, \hat{p}^{\#}(\hat{k})) \mid (\hat{k}, B_k) \text{ such that } \hat{\mathcal{G}}(\hat{k}, \mathrm{Bind}(B_k), \hat{\ell}) \wedge \hat{k} \in \mathrm{dom} \hat{p}^{\#}\}
\end{array}
$$

<caption>Fig. 9. SSA abstract domain signature (top) and abstract interpretation (bottom)</caption>

$$
\begin{array}{l}
\Gamma^{\#} \in \widehat{\mathbb{A}}.\Gamma^{\#} \triangleq \text{Entry} | \text{Assûme}(\hat{e}, \Gamma^{\#}) | \text{Joîn}(C^{\#}) | \text{Lôc}(\ell) \quad (\text{SSA algebraic locations}) \\
\text{where } \hat{e} \in \hat{\mathbb{E}} \text{ and } C^{\#} \in \mathcal{P}_f(\mathbb{B} \times \widehat{\mathbb{A}}.\Gamma^{\#})
\end{array}
$$

$$
\begin{align*}
\widehat{\mathbb{A}}.\text{entr}'y &\triangleq \text{Entry} \\
\widehat{\mathbb{A}}.\text{ass}'ume(\hat{e}, \Gamma^{\#}) &\triangleq \text{Assûme}(\hat{e}, \Gamma^{\#}) \\
\widehat{\mathbb{A}}.\text{widen}(\ell, \_, \_) &\triangleq \text{Lôc}(\ell) \\
\widehat{\mathbb{A}}.\hat{y}(\text{Entry}) &\triangleq \Gamma \\
\widehat{\mathbb{A}}.\hat{y}(\text{Assûme}(\hat{e}, \Gamma^{\#})) &\triangleq \{\Gamma \in \widehat{\mathbb{A}}.\hat{y}(\Gamma^{\#}) \mid \hat{e} \llbracket \hat{e} \rrbracket(\Gamma) \neq 0\} \\
\widehat{\mathbb{A}}.\hat{y}(\text{Joîn}(C^{\#})) &\triangleq \bigcup_{B, \Gamma^{\#} \in C^{\#}} \{\text{bind}(B, \Gamma) \mid \Gamma \in \widehat{\mathbb{A}}.\hat{y}(C^{\#})\} \\
\widehat{\mathbb{A}}.\hat{y}(\text{Lôc}(\ell)) &\triangleq \Gamma
\end{align*}
$$

$$
\begin{array}{c}
\text{TASSUMESSA} \\
\Gamma^{\#} \stackrel{\hat{\mathrm{If}}}{\rightleftharpoons} \hat{e} \xrightarrow{\#} \text{Assûme}(\hat{e}, \Gamma^{\#})
\end{array}
$$

$$
\begin{array}{c}
\text{TJOINSSA} \\
(B, \Gamma^{\#}) \in C^{\#} \\
\Gamma^{\#} \stackrel{\text{Bind}(B)}{\rightleftharpoons} \# \text{Join}(C^{\#})
\end{array}
$$

$$
\begin{array}{c}
\text{TLocSSA} \\
\Gamma^{\#} \stackrel{\hat{R}}{\rightleftharpoons} \# \hat{\mathcal{F}}_{\hat{g}}(\hat{p}^{\#})(\hat{\ell}) \\
\Gamma^{\#} \stackrel{\hat{R}}{\rightleftharpoons} \# \text{Lôc}(\hat{\ell})
\end{array}
$$

<caption>Fig. 10. The free algebra SSA abstract domain ($\widehat{\mathbb{A}}$) (top) and rules for generating SSA programs (bottom).</caption>

$\Gamma^{\#}$ and $\Gamma'^{\#}$ with the additional information that $\hat{x}$ is 3 when coming from $\Gamma^{\#}$ and 5 when coming from $\Gamma'^{\#}$. This is how we represent what traditional SSA would denote with a $\phi$ function: $\hat{x} \mapsto \phi(3, 5)$. Note that this signature makes some constraints placed on our SSA programs explicit: it is clear that assume nodes have a single predecessor labelled by a guard, and join nodes have multiple predecessors labelled by bindings.

$\hat{\mathcal{F}}_{\hat{g}}$ is the transfer function used for the direct analysis of SSA programs. It is similar to $\mathcal{F}_g$, but explicitly separates treatment of guard edges (with *assûme*) and bindings before a join (with *joîn*), whereas $\mathcal{F}_g$ performed both simultaneously using a *join* of *applies*. The other components of our analysis ($\nabla_W$ and *analyse*) are the same as in Figure 4.

The SSA domain also has soundness and correction hypothesis similar to those of the IMP domain
in Figure 4, omitted here for the sake of brevity.

6.3 Free algebra of the SSA domain signature

Figure 10 presents the *free algebra SSA domain*, denoted $\widehat{\mathbb{A}}$. Just like in IMP free algebra (Section 4), the domain operation simply create terms using the relevant function symbols.

This domain also presents a dual interpretation as sets of valuations (given by the concretization
$\widehat{\mathbb{A}}.\hat{y}$) and as a program graph (given by the edge predicate $\stackrel{\wedge}{\mapsto} \# \in (\widehat{\mathbb{A}}.\Gamma^{\#} \times \hat{\mathbb{R}} \times \widehat{\mathbb{A}}.\Gamma^{\#}) \to \{0; 1\}$).
The rules for generating this graph are similar to those of the IMP free algebra. Note that contrary
to $\text{TJOIN}$, where a $\text{Join}$ had the same predecessors as its elements, here the $\text{Joîn}$'s predecessors are
<figure><img src="image_7.png" /><figcaption>Fig. 11. The lift functor, lifting an SSA Domain $\hat{D}$ into an IMP domain Lift($\hat{D}$).</figcaption></figure>

its elements. Instead of identifying each term in the joined set with the whole join, each term is the predecessor of the join, with the edge labelled by its bindings. This also means we no longer need a TSELF rule, as we can no longer collapse loops completely.

Like in Figure 6, generating the graph also requires a vertex predicate $\hat{V} \in \widehat{FA}.\Gamma^# \to \{0; 1\}$ to filter the relevant nodes. It has the same rules as those of V, so they were omitted here. Figure 2c presents two example graphs generated from such free algebra terms.

*Going further.* We could easily show a version of Theorem 4.1 for direct analysis of the SSA free algebra domain, and define functors on SSA similarly to Section 5. However, apart from the product functor $\hat{\mathcal{X}}$, we do not really need them as we are mostly interested in analyzing IMP programs, which can use IMP functors before reaching SSA domains through the SSA Lift functor (Section 7).

# 7 LIFTING SSA DOMAINS TO IMP DOMAINS

In this section, we present the *SSA Lift domain*, denoted Lift, a functor that lifts an SSA domain into an IMP domain. We then show that, when applied to the SSA free algebra domain, this functor is akin to compilation from IMP to SSA.

## 7.1 The SSA lift functor

The lift functor is detailed in Figure 11. Lift states are pairs of an abstract store, mapping from program variables to the SSA expressions they currently hold, and an SSA state $\hat{D}.\Gamma^#$. The functor reuses the SSA states of the argument $\hat{D}$ as SSA locations ($\hat{L} = \hat{D}.\Gamma^#$). The entrypoint Lift($\hat{D}$).entry contains a map from all program variables to initial SSA variables, paired with the SSA domain's entrypoint $\hat{D}.enîry$.

Applying an assignment updates the store of the corresponding variable; and applying a guard updates the SSA state using $\hat{D}.assûme$. Here the $subst \in E \times (\mathcal{X} \to \hat{E}) \to \hat{E}$ function substitutes all variables from a program expression $e \in E$ by their value in $\sigma^#$, which is an SSA expression. This only works if the constructs that appear in $E$ are translatable to SSA expression constructs. Use transformation functors (Section 5) to simplify the language of program expressions if needed.
<figure><img src="image_9.png" /><figcaption>Fig. 11. The lift functor, lifting an SSA Domain $\hat{D}$ into an IMP domain Lift($\hat{D}$).</figcaption></figure>

its elements. Instead of identifying each term in the joined set with the whole join, each term is the predecessor of the join, with the edge labelled by its bindings. This also means we no longer need a TSELF rule, as we can no longer collapse loops completely.

Like in Figure 6, generating the graph also requires a vertex predicate $\hat{V} \in \widehat{FA}.\Gamma^# \to \{0; 1\}$ to filter the relevant nodes. It has the same rules as those of V, so they were omitted here. Figure 2c presents two example graphs generated from such free algebra terms.

*Going further.* We could easily show a version of Theorem 4.1 for direct analysis of the SSA free algebra domain, and define functors on SSA similarly to Section 5. However, apart from the product functor $\hat{\mathcal{X}}$, we do not really need them as we are mostly interested in analyzing IMP programs, which can use IMP functors before reaching SSA domains through the SSA Lift functor (Section 7).

# 7 LIFTING SSA DOMAINS TO IMP DOMAINS

In this section, we present the *SSA Lift domain*, denoted Lift, a functor that lifts an SSA domain into an IMP domain. We then show that, when applied to the SSA free algebra domain, this functor is akin to compilation from IMP to SSA.

## 7.1 The SSA lift functor

The lift functor is detailed in Figure 11. Lift states are pairs of an abstract store, mapping from program variables to the SSA expressions they currently hold, and an SSA state $\hat{D}.\Gamma^#$. The functor reuses the SSA states of the argument $\hat{D}$ as SSA locations ($\hat{L} = \hat{D}.\Gamma^#$). The entrypoint Lift($\hat{D}$).entry contains a map from all program variables to initial SSA variables, paired with the SSA domain's entrypoint $\hat{D}.enîry$.

Applying an assignment updates the store of the corresponding variable; and applying a guard updates the SSA state using $\hat{D}.assûme$. Here the $subst \in E \times (X \to \hat{E}) \to \hat{E}$ function substitutes all variables from a program expression $e \in E$ by their value in $\sigma^#$, which is an SSA expression. This only works if the constructs that appear in $E$ are translatable to SSA expression constructs. Use transformation functors (Section 5) to simplify the language of program expressions if needed.
The $\hat{\mathbb{D}}.join\{(\sigma_i^#, \Gamma_i^#) | i = 1..n\}$ function is a bit more complex. The new store $\sigma^#$ maps $x$ to the unique value if all argument stores evaluate $x$ the same value, and to a new SSA variable otherwise (introducing a $\phi$ function). The new SSA state $\Gamma^#$ is the $\hat{\mathbb{D}}.join$ of all locations $\Gamma_i^#$ with the corresponding bindings for renamed variables. Note that this is a recursive definition, as SSA variables in the bindings are named $x_{\Gamma^*}$ where $\Gamma^#$ is the SSA state being defined. In practice, we break this mutual recursion through hash-consing [Filliâtre and Conchon 2006], each SSA state is given a unique numeric identifier and SSA variables only reference that identifier. Although not presented here, this join operation can easily be adapted to perform global value numbering [Lemerre 2023] by merging SSA variables which are equal in all branches. Performing GVN is required to optimize the dead code in Figure 2. Notice that by definition, the calls to $\hat{\mathbb{D}}.join$ respect the assumptions we made on our SSA form. All set elements bind the same variables, and, since those variables are named after the current location, they are bound nowhere else.

The widening simply calls $\hat{\mathbb{D}}.widen$ to determine the new SSA state, and renames any introduced variables in the store to match the new state. Note that this assumes both stores are fairly similar.

Finally, Lift($\hat{\mathbb{D}}$).$\gamma$($\sigma^#, \Gamma^#$) generates the set of represented stores, by using $\sigma^#$ to map variable to SSA expressions, and then evaluating these expressions in a context given by $\hat{\mathbb{D}}$. $\hat{\gamma}(\Gamma^#)$.

## 7.2 Compiling to SSA

We now consider running the analysis on the lift functor to the SSA free algebra domain $\hat{\mathbb{F}}A$. We write $p^# \triangleq \text{analyse}(\text{Lift}(\hat{\mathbb{F}}A))$ the analysis result. Using it, we generate an SSA program $\hat{G}_{p^*}$ from the SSA free algebra. Just like for the functor products, this requires adapting the TLocSSA rule by adding a projection, since our states are not SSA free algebra states, but a pair (which includes an SSA free algebra state). With this setup, our analysis effectively compiles an IMP program to SSA form. We write $\rightsquigarrow \hat{G}_{p^*}$ the transition system associated with this new SSA program.

The following theorems show simulation results between the source and compiled programs. Since the source and target language are different, our simulation relation is no longer just equality:

$$ \begin{array}{l} C \in \mathbb{S} \times \hat{\mathbb{S}} \to \{0; 1\} \\ C((\ell, \sigma), (\Gamma^#, \Gamma)) \triangleq \exists \sigma^# \in \mathbb{F} \to \hat{\mathbb{F}}, (\sigma^#, \Gamma^#) = p^#(\ell) \wedge \sigma = [x \in \mathbb{F} \mapsto \hat{\mathbb{E}}[\sigma_0^#(x)](\Gamma)] \end{array} $$

The first part is compatibility between the IMP location $\ell$ and the SSA location $\Gamma^#$ via $p^#$, and the second part is compatibility between the IMP store $\sigma$ and the SSA valuation $\Gamma$. Notice that with this relation, $\Gamma^#$ is uniquely determined by $\ell$, and $\sigma$ is uniquely determined by $\Gamma$.

**THEOREM 7.1 (SSA COMPILATION FORWARD SIMULATION).** For all reachable pairs $(\ell, \sigma)$ and $(\ell', \sigma')$ such that $\ell$ and $\ell'$ are entry or widening points, for all $\hat{s} \in \hat{\mathbb{S}}$ we have:

$$ (\ell, \sigma) \to_G^+ (\ell', \sigma') \wedge C((\ell, \sigma), \hat{s}) \Rightarrow \exists \hat{s}' \in \hat{\mathbb{S}}, C((\ell', \sigma'), \hat{s}') \wedge \hat{s} \rightsquigarrow^* \hat{G}_{p^*} \hat{s}' $$

Furthermore, there exists an $\hat{s} \in \hat{\mathbb{S}}$ such that $C((\ell, \sigma), \hat{s})$ holds.

Finally, if $\hat{s} \rightsquigarrow^* \hat{G}_{p^*} \hat{s}'$ has length 0, then $\ell'$ is not a true loop head (it has a single reachable predecessor).

**THEOREM 7.2 (SSA COMPILATION BACKWARD SIMULATION).** For all SSA states $(\Gamma^#, \Gamma)$ and $(\Gamma'^#, \Gamma')$ where $\Gamma^#$ and $\Gamma'^#$ appear in $\text{img } p^*$ as images of widening or entry points, and for all $s' \in \mathbb{S}$ we have:

$$ (\Gamma^#, \Gamma) \rightsquigarrow^* \hat{G}_{p^*} (\Gamma'^#, \Gamma') \wedge C(s', (\Gamma'^#, \Gamma')) \Rightarrow \exists s \in \mathbb{S}, C(s, (\Gamma^#, \Gamma)) \wedge s \to_G^+ s' $$

Furthermore, there exists an $s' \in \mathbb{S}$ such that $C(s', (\Gamma'^#, \Gamma'))$ holds.

See proofs in Appendix A.4.
The $\hat{\mathbb{D}}.join\{(\sigma_i^#, \Gamma_i^#) | i = 1..n\}$ function is a bit more complex. The new store $\sigma^#$ maps $x$ to the unique value if all argument stores evaluate $x$ the same value, and to a new SSA variable otherwise (introducing a $\phi$ function). The new SSA state $\Gamma^#$ is the $\hat{\mathbb{D}}.join$ of all locations $\Gamma_i^#$ with the corresponding bindings for renamed variables. Note that this is a recursive definition, as SSA variables in the bindings are named $x_{\Gamma^*}$ where $\Gamma^#$ is the SSA state being defined. In practice, we break this mutual recursion through hash-consing [Filliâtre and Conchon 2006], each SSA state is given a unique numeric identifier and SSA variables only reference that identifier. Although not presented here, this join operation can easily be adapted to perform global value numbering [Lemerre 2023] by merging SSA variables which are equal in all branches. Performing GVN is required to optimize the dead code in Figure 2. Notice that by definition, the calls to $\hat{\mathbb{D}}.join$ respect the assumptions we made on our SSA form. All set elements bind the same variables, and, since those variables are named after the current location, they are bound nowhere else.

The widening simply calls $\hat{\mathbb{D}}.widen$ to determine the new SSA state, and renames any introduced variables in the store to match the new state. Note that this assumes both stores are fairly similar.

Finally, Lift($\hat{\mathbb{D}}$).$\gamma$($\sigma^$, $\Gamma^$)) generates the set of represented stores, by using $\sigma^$ to map variable to SSA expressions, and then evaluating these expressions in a context given by $\hat{\mathbb{D}}$. $\gamma(\Gamma^)$.

## 7.2 Compiling to SSA

We now consider running the analysis on the lift functor to the SSA free algebra domain $\hat{\mathbb{F}}A$. We write $p^# \triangleq \text{analyse}(\text{Lift}(\hat{\mathbb{F}}A))$ the analysis result. Using it, we generate an SSA program $\hat{G}_{p^*}$ from the SSA free algebra. Just like for the functor products, this requires adapting the TLocSSA rule by adding a projection, since our states are not SSA free algebra states, but a pair (which includes an SSA free algebra state). With this setup, our analysis effectively compiles an IMP program to SSA form. We write $\rightsquigarrow \hat{G}_{p^*}$ the transition system associated with this new SSA program.

The following theorems show simulation results between the source and compiled programs. Since the source and target language are different, our simulation relation is no longer just equality:

$$ C \in \mathbb{S} \times \hat{\mathbb{S}} \to \{0; 1\} \\ C((\ell, \sigma), (\Gamma^#, \Gamma)) \triangleq \exists \sigma^# \in \mathbb{X} \to \hat{\mathbb{E}}, (\sigma^#, \Gamma^#) = p^#(\ell) \wedge \sigma = [x \in \mathbb{X} \mapsto \hat{\mathbb{E}}[\sigma_0^#(x)]](\Gamma)] $$

The first part is compatibility between the IMP location $\ell$ and the SSA location $\Gamma^#$ via $p^#$, and the second part is compatibility between the IMP store $\sigma$ and the SSA valuation $\Gamma$. Notice that with this relation, $\Gamma^#$ is uniquely determined by $\ell$, and $\sigma$ is uniquely determined by $\Gamma$.

**THEOREM 7.1 (SSA COMPILATION FORWARD SIMULATION).** For all reachable pairs $(\ell, \sigma)$ and $(\ell', \sigma')$ such that $\ell$ and $\ell'$ are entry or widening points, for all $\hat{s} \in \hat{\mathbb{S}}$ we have:

$$ (\ell, \sigma) \to_G^+ (\ell', \sigma') \wedge C((\ell, \sigma), \hat{s}) \Rightarrow \exists \hat{s}' \in \hat{\mathbb{S}}, C((\ell', \sigma'), \hat{s}') \wedge \hat{s} \rightsquigarrow^* \hat{G}_{p^*} \hat{s}' $$

Furthermore, there exists an $\hat{s} \in \hat{\mathbb{S}}$ such that $C((\ell, \sigma), \hat{s})$ holds.

Finally, if $\hat{s} \rightsquigarrow^* \hat{G}_{p^*} \hat{s}'$ has length 0, then $\ell'$ is not a true loop head (it has a single reachable predecessor).

**THEOREM 7.2 (SSA COMPILATION BACKWARD SIMULATION).** For all SSA states $(\Gamma^#, \Gamma)$ and $(\Gamma'^#, \Gamma')$ where $\Gamma^#$ and $\Gamma'^#$ appear in $\text{img } p^*$ as images of widening or entry points, and for all $s' \in \mathbb{S}$ we have:

$$ (\Gamma^#, \Gamma) \rightsquigarrow^* \hat{G}_{p^*} (\Gamma'^#, \Gamma') \wedge C(s', (\Gamma'^#, \Gamma')) \Rightarrow \exists s \in \mathbb{S}, C(s, (\Gamma^#, \Gamma)) \wedge s \to_G^+ s' $$

Furthermore, there exists an $s' \in \mathbb{S}$ such that $C(s', (\Gamma'^#, \Gamma'))$ holds.

See proofs in Appendix A.4.
<table><caption>Fig. 12. Evaluation rules for ⇝ (top), constraint propagation/reduction rules (middle), SSA numeric domain $\tilde{N}$ (bottom).</caption><thead><tr><th>EVALREUSE</th><th>EVALCST</th><th>EVALBINOP</th><th>EVALVAR</th></tr></thead><tbody><tr><td>ê ∈ dom(Γ<sup>#</sup>)<br>Γ<sup>#</sup> = ê ⇝ Γ<sup>#</sup>(ê)</td><td>Γ<sup>#</sup> = z ⇝ [z : z]</td><td>ê<sub>1</sub> ◦ ê<sub>2</sub> /∈ dom(Γ<sup>#</sup>)<br>Γ<sup>#</sup> = ê<sub>1</sub> ⇝ z<sup>#</sup><sub>1</sub> &nbsp;&nbsp;&nbsp;&nbsp; Γ<sup>#</sup> = ê<sub>2</sub> ⇝ z<sup>#</sup><sub>1</sub><br>Γ<sup>#</sup> = ê<sub>1</sub> ◦ ê<sub>2</sub> ⇝ ⃗(z<sup>#</sup><sub>1</sub>, z<sup>#</sup><sub>2</sub>)</td><td>ê ∈ dom(Γ<sup>#</sup>)<br>Γ<sup>#</sup> = ê /∈ dom(Γ<sup>#</sup>)<br>Γ<sup>#</sup> = ê ⇝ [-∞ : +∞]</td></tr><tr><td colspan="4"><b>REDUCEBWD</b></td></tr><tr><td>Γ<sup>#</sup> = ê<sub>1</sub> ◦ ê<sub>2</sub> ⇝ z<sup>#</sup><br>(z'<sub>1</sub><sup>#</sup>, z'<sub>2</sub><sup>#</sup>) = ⃗(z<sub>1</sub><sup>#</sup>, z<sub>2</sub><sup>#</sup>, z<sup>#</sup>) &nbsp;&nbsp;&nbsp;&nbsp; (z'<sub>i</sub><sup>#</sup> ∩ Z<sup>#</sup> &nbsp;&nbsp;&nbsp;&nbsp; z<sub>i</sub><sup>#</sup>) ⊂ Z<sup>#</sup><br>Γ<sup>#</sup> ⇒ Γ<sup>#</sup>[ê<sub>i</sub> ↦ z<sub>i</sub><sup>#</sup> ∩ Z<sup>#</sup> &nbsp;&nbsp;&nbsp;&nbsp; z'<sub>i</sub><sup>#</sup>]</td><td>Γ<sup>#</sup> = ê<sub>1</sub> ⇝ z<sup>#</sup><sub>1</sub> &nbsp;&nbsp;&nbsp;&nbsp; Γ<sup>#</sup> = ê<sub>2</sub> ⇝ z<sup>#</sup><sub>2</sub><br>Γ<sup>#</sup> = ê<sub>2</sub> ⇝ z<sup>#</sup><sub>2</sub><br>Γ<sup>#</sup> = ê<sub>1</sub> ◦ ê<sub>2</sub> ⇝ ⃗(z'<sub>1</sub><sup>#</sup>, z'<sub>2</sub><sup>#</sup>)</td><td>Γ<sup>#</sup> = ê ⇝ z<sup>#</sup><br>Γ<sup>#</sup> = ê<sub>1</sub> ◦ ê<sub>2</sub> ⇝ z<sup>#</sup><sub>1</sub><br>Γ<sup>#</sup> = ê<sub>2</sub> ⇝ z<sup>#</sup><sub>1</sub><br>Γ<sup>#</sup> = ê<sub>1</sub> ◦ ê<sub>2</sub> ⇝ ⃗(z'<sub>1</sub><sup>#</sup>, z'<sub>2</sub><sup>#</sup>)</td><td>Γ<sup>#</sup> = ê ⇝ ⊥<sub>⊥N</sub><br>Γ<sup>#</sup> = ê<sub>1</sub> ◦ ê<sub>2</sub> ⇝ ⊥<sub>Z<sup>#</sup></sub><br>Γ<sup>#</sup> = ê<sub>1</sub> ◦ ê<sub>2</sub> ⇝ ⊥<sub>Z<sup>#</sup></sub><br>Γ<sup>#</sup> = ê<sub>1</sub> ◦ ê<sub>2</sub> ⇝ ⊥<sub>Z<sup>#</sup></sub></td></tr><tr><td>Γ<sup>#</sup> ∈ N̄.Γ<sup>#</sup> ≜ Ê → Z<sup>#</sup></td><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td></tr><tr><td colspan="4"><b>REDUCEFWD</b></td></tr><tr><td>Γ<sup>#</sup> = Ê ⇝ z<sup>#</sup></td><td>Γ<sup>#</sup> = Ê ⇝ z<sup>#</sup></td><td>Γ<sup>#</sup> = Ê ⇝ z<sup>#</sup></td><td>Γ<sup>#</sup> = Ê ⇝ z<sup>#</sup></td></tr><tr><td colspan="4"><b>REDUCEBOT</b></td></tr><tr><td>Γ<sup>#</sup> = Ê ⇝ ⊥<sub>Z<sup>#</sup></sub></td><td>Γ<sup>#</sup> = Ê ⇝ ⊥<sub>Z<sup>#</sup></sub></td><td>Γ<sup>#</sup> = Ê ⇝ ⊥<sub>Z<sup>#</sup></sub></td><td>Γ<sup>#</sup> = Ê ⇝ ⊥<sub>Z<sup>#</sup></sub></td></tr><tr><td colspan="4"><b>REDUCEBWD</b></td></tr><tr><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td></tr><tr><td colspan="4"><b>REDUCEFWD</b></td></tr><tr><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td></tr><tr><td colspan="4"><b>REDUCEBOT</b></td></tr><tr><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td></tr><tr><td colspan="4"><b>REDUCEBWD</b></td></tr><tr><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td></tr><tr><td colspan="4"><b>REDUCEFWD</b></td></tr><tr><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td></tr><tr><td colspan="4"><b>REDUCEBOT</b></td></tr><tr><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td></tr><tr><td colspan="4"><b>REDUCEBWD</b></td></tr><tr><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td></tr><tr><td colspan="4"><b>REDUCEFWD</b></td></tr><tr><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td></tr><tr><td colspan="4"><b>REDUCEBOT</b></td></tr><tr><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td></tr></tbody></table>

These theorems statements are designed to be easily composable: if we have three widening point $(\ell, \sigma) \to_G^+(\ell', \sigma') \to_G^+(\ell'', \sigma'')$, we can use Theorem 7.1 twice and compose the results.

# 8 SSA BASED NUMERICAL ANALYSIS

In this section, we implement a numerical abstract domain $\tilde{N}$ (similar to that of Section 3.4), but using the SSA domain signature. Using SSA form here allows storing information about expressions, and not just about variables, which improves precision. This is possible because variables are bound and not assigned, and thus their values, and the values of expressions that use them, never change. We illustrate the precision improvement through various examples, and prove that using Lift($\tilde{N}$) is always more precise than N.

## 8.1 The SSA numeric domain

The SSA numeric domain is presented at the bottom Figure 12. Its states are mappings from SSA symbolic expressions to a numerical single-value abstraction. The concretization of such an element $\Gamma^#$ is the set of valuations which, when used to evaluate an expression $\hat{e}$ of $\Gamma^#$, yield an integer in $\Gamma^#(\hat{e})$. The entry point is the empty mapping. The domain operations require defining a forward evaluation judgement $\Gamma^# = \hat{e} \llcorner z^# \in (\tilde{N}.\Gamma^# \times \hat{E} \times Z^#) \to \{0; 1\}$ and a reduction operator $\Rightarrow \in (\Gamma^# \times \Gamma^#) \to \{0; 1\}$.

The judgement $\Gamma^# = \hat{e} \llcorner z^#$ intuitively means that we can deduce $\hat{e} \in \gamma_{Z^*}(z^#)$ from $\Gamma^#$. Formally, it is defined through the induction rules given at the top of Figure 12. They proceed by recursively evaluating the expression $\hat{e}$ (rule EVALBINOP) until a constant (EVALCST), variable (EVALVAR), or remembered expression (EVALREUSE) is found in $\Gamma^#$. Binary expressions are evaluated through
<table><caption>Fig. 12. Evaluation rules for ⇝ (top), constraint propagation/reduction rules (middle), SSA numeric domain $\tilde{N}$ (bottom).</caption><thead><tr><th>EVALREUSE</th><th>EVALCST</th><th>EVALBINOP</th><th>EVALVAR</th></tr></thead><tbody><tr><td>ê ∈ dom(Γ<sup>#</sup>)<br>Γ<sup>#</sup> = ê ⇝ Γ<sup>#</sup>(ê)</td><td>Γ<sup>#</sup> = z ⇝ [z : z]</td><td>ê<sub>1</sub> ◦ ê<sub>2</sub> ∉ dom(Γ<sup>#</sup>)<br>Γ<sup>#</sup> = ê<sub>1</sub> ⇝ z<sub>1</sub><sup>#</sup> &nbsp;&nbsp;&nbsp;&nbsp; Γ<sup>#</sup> = ê<sub>2</sub> ⇝ z<sub>1</sub><sup>#</sup><br>Γ<sup>#</sup> = ê<sub>1</sub> ◦ ê<sub>2</sub> ⇝ ⃗(z<sub>1</sub><sup>#</sup>, z<sub>2</sub><sup>#</sup>)</td><td>ê ∈ dom(Γ<sup>#</sup>)<br>Γ<sup>#</sup> = x̂ ∉ dom(Γ<sup>#</sup>)<br>Γ<sup>#</sup> = x̂ ⇝ [-∞ : +∞]</td></tr><tr><td colspan="4"><b>REDUCEBWD</b></td></tr><tr><td>Γ<sup>#</sup> = ê<sub>1</sub> ◦ ê<sub>2</sub> ⇝ z<sup>#</sup><br>(z'<sub>1</sub><sup>#</sup>, z'<sub>2</sub><sup>#</sup>) = ⃗(z<sub>1</sub><sup>#</sup>, z<sub>2</sub><sup>#</sup>, z<sup>#</sup>)<br>Γ<sup>#</sup> ⇒ Γ<sup>#</sup>[ê<sub>i</sub> ↦ z<sub>i</sub><sup>#</sup> ∩ Z<sup>#</sup> z'<sub>i</sub><sup>#</sup>]</td><td>Γ<sup>#</sup> = ê<sub>1</sub> ⇝ z<sub>1</sub><sup>#</sup> &nbsp;&nbsp;&nbsp;&nbsp; Γ<sup>#</sup> = ê<sub>2</sub> ⇝ z<sub>2</sub><sup>#</sup><br>(z'<sub>i</sub><sup>#</sup> ∩ Z<sup>#</sup> z<sub>i</sub><sup>#</sup>) ⊂ Z<sup>#</sup> z<sub>i</sub><sup>#</sup></td><td>Γ<sup>#</sup> = ê ⇝ z<sup>#</sup><br>Γ<sup>#</sup> ⇒ Γ<sup>#</sup>[ê ↦ z<sup>#</sup>]</td><td>Γ<sup>#</sup> = ê ⇝ ⊥Z<sup>#</sup><br>Γ<sup>#</sup> ⇒ ⊥N̂</td></tr><tr><td colspan="4"><b>REDUCEFWD</b></td></tr><tr><td>Γ<sup>#</sup> ∈ N̂.Γ<sup>#</sup> ≜ Ê → Z<sup>#</sup></td><td>Γ<sup>#</sup> = ê ⇝ z<sup>#</sup></td><td>Γ<sup>#</sup> = ê ⇝ z<sup>#</sup></td><td>Γ<sup>#</sup> = ê ⇝ ⊥Z<sup>#</sup></td></tr><tr><td colspan="4"><b>REDUCEBOT</b></td></tr><tr><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td></tr><tr><td colspan="4"><b>REDUCECST</b></td></tr><tr><td>Nbind(B, Γ<sup>#</sup>) ≜ Γ<sup>#</sup> ♦ [x̂ ↦ z<sup>#</sup> | x̂ ↦ê ∈ B ∧ Γ<sup>#</sup> = ê ⇝ z<sup>#</sup>]</td><td>Γ<sup>#</sup> = Nbind(B<sub>i</sub>, Γ<sub>i</sub><sup>#</sup>) ⇒ Γ'<sub>i</sub><sup>#</sup> &nbsp;&nbsp;&nbsp;&nbsp; i ∈ 1..n</td><td>Γ<sup>#</sup> = Nbind(B<sub>i</sub>, Γ<sub>i</sub><sup>#</sup>) ⇒ Γ'<sub>i</sub><sup>#</sup> &nbsp;&nbsp;&nbsp;&nbsp; i ∈ 1..n</td><td>Γ<sup>#</sup> = Nbind(B<sub>i</sub>, Γ<sub>i</sub><sup>#</sup>) ⇒ Γ'<sub>i</sub><sup>#</sup> &nbsp;&nbsp;&nbsp;&nbsp; i ∈ 1..n</td></tr><tr><td colspan="4"><b>REDUCEBWD</b></td></tr><tr><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td></tr><tr><td colspan="4"><b>REDUCEFWD</b></td></tr><tr><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td></tr><tr><td colspan="4"><b>REDUCEVAR</b></td></tr><tr><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td></tr><tr><td colspan="4"><b>REDUCECST</b></td></tr><tr><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td></tr><tr><td colspan="4"><b>REDUCEVAR</b></td></tr><tr><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td></tr><tr><td colspan="4"><b>REDUCEBWD</b></td></tr><tr><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td></tr><tr><td colspan="4"><b>REDUCEFWD</b></td></tr><tr><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td></tr><tr><td colspan="4"><b>REDUCEVAR</b></td></tr><tr><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td><td>Γ<sup>#</sup> = Ê</td></tr></tbody></table>

These theorems statements are designed to be easily composable: if we have three widening point $(\ell, \sigma) \to_G^+(\ell', \sigma') \to_G^+(\ell'', \sigma'')$, we can use Theorem 7.1 twice and compose the results.

# 8 SSA BASED NUMERICAL ANALYSIS

In this section, we implement a numerical abstract domain $\tilde{N}$ (similar to that of Section 3.4), but using the SSA domain signature. Using SSA form here allows storing information about expressions, and not just about variables, which improves precision. This is possible because variables are bound and not assigned, and thus their values, and the values of expressions that use them, never change. We illustrate the precision improvement through various examples, and prove that using Lift($\tilde{N}$) is always more precise than N.

## 8.1 The SSA numeric domain

The SSA numeric domain is presented at the bottom Figure 12. Its states are mappings from SSA symbolic expressions to a numerical single-value abstraction. The concretization of such an element $Γ^#$ is the set of valuations which, when used to evaluate an expression $ê$ of $Γ^#$, yield an integer in $Γ^#(ê)$. The entry point is the empty mapping. The domain operations require defining a forward evaluation judgement $Γ^# = ê ⇝ z^# \in (\tilde{N}.Γ^# \times Ê \times Z^#) \to \{0; 1\}$ and a reduction operator $\Rightarrow \in (Γ^# \times Γ^#) \to \{0; 1\}$.

The judgement $Γ^# = ê ⇝ z^#$ intuitively means that we can deduce $ê \in \gamma_{Z^*}(z^#)$ from $Γ^#$. Formally, it is defined through the induction rules given at the top of Figure 12. They proceed by recursively evaluating the expression $ê$ (rule EVALBINOP) until a constant (EVALCST), variable (EVALVAR), or remembered expression (EVALREUSE) is found in $Γ^#$. Binary expressions are evaluated through
forward transfer functions, remembered expression return their values and unremembered variables return the top element. The following lemma proves our judgement captures the intended meaning:

LEMMA 8.1. If $\Gamma^{\#} \models \hat{e} \llcorner z^{\#}$, then $\forall \Gamma \in \tilde{N}.\hat{y}(\Gamma^{\#})$, $\hat{E} \llcorner \hat{e}](\Gamma) \in \gamma_{Z^{\#}}(z^{\#})$.

PROOF. By induction on expressions, and soundness of $\tilde{\omega}$.

□

The judgement $\Gamma^{\#} \Rightarrow \Gamma'^{\#}$ is a reduction operator [Granger 1992], it implies that $\Gamma^{\#}$ and $\Gamma'^{\#}$ represent the same abstraction $(\tilde{N}.\hat{y}(\Gamma^{\#}) = \tilde{N}.\hat{y}(\Gamma'^{\#}))$ but $\Gamma'^{\#}$ is smaller. Its induction rules are given in the middle of Figure 12. REDUCEBWD propagates constraints [Benhamou et al. 1999] of the form $\hat{e} \in \gamma_{Z^{\#}}(z^{\#})$ between the symbolic expressions. Thus, it learns from conditions [Granger 1992] (appearing e.g. in if statements). The result is saved when the precision has improved, which allows further evaluations with $\Rightarrow$ to also improve. REDUCEFWD saves the result of evaluation. This will make the result of future joins more precise. Finally, REDUCEBOT quickly propagates the information that the current state is bottom (some constraint is unsatisfiable).

The domain operations are given as rules instead of functions as they depend on how many reductions ($\Rightarrow$) we wish to perform before returning the result. Performing more reductions will be more precise but also reduce performance.

$\tilde{N}.assûme(\hat{e}, \Gamma^{\#})$ propagates constraints, adding the information that the guard must be true (denoted as $\neg 0^9$). Nbind($B$, $\Gamma^{\#}$) updates the abstract SSA state $\Gamma^{\#}$ by mapping $\hat{x}$ to the result of the evaluation of $\hat{e}$ for all bindings $\hat{x} \mapsto \hat{e}$ that appear in the bindings $B$. The last operation, $\tilde{N}.joîn$, applies the bindings, and then performs an intersection of the maps (only keeping expressions that are present in all branches, including freshly bound variables). We can perform an intersection because we know nothing important about a symbolic expression that is not present in every branch (in many cases, they will go out of scope and be unbounded).

## 8.2 Combination of SSA-based analysis and online SSA translation

We can use this SSA state abstraction with the translation of Section 7 to analyze an SSA program while it is being computed from the source program. This analysis combines our SSA abstract state $\Gamma^{\#}$ with an abstract store $\sigma^{\#} \in \mathcal{X} \to \hat{E}$.

This combination is more precise than the standard non-relational numerical analysis performed by N (that constrains program variables instead of program values), i.e. we can abstract our combination to a standard numerical analysis.

$$ \alpha \in \text{Lift}(\tilde{N}), \Sigma^{\#} \to N, \Sigma^{\#} \\ \alpha(\sigma^{\#}, \Gamma^{\#}) \triangleq [x \in \mathcal{X} \mapsto z^{\#} \mid \Gamma^{\#} \models \sigma^{\#}(x) \llcorner z^{\#}] $$

Intuitively, this abstraction forgets the relations between the variables that are given by the symbolic expressions, and just sees them as opaque identifiers. In particular, we can prove that our analysis operations are monotonic (provided a suitable strategy for applying $\Rightarrow$, such as maximally applying $\Rightarrow$ when evaluation is limited to the symbolic expressions that appear in the abstract store), and thus that our combination is always more precise than the non-relational abstract domain for any succession of operations.

We can also provide specific examples where our analysis improves over a non-relational domain:

* **Reduction on related variables:** in $y := x+1$; $z := y*y$; if ($2 \le y \le 5$) ... , the Lift($\tilde{N}$) domain can prove that $4 \le z \le 25$ and $1 \le x \le 4$ while N cannot. This is very useful when analyzing machine code, which often places related variables in separate registers (and flags).

<footnote n="9">⁹Interval or congruence cannot represent this accurately, but a specialized 0/≠ 0 domain could be used here, or we could use a specific rule for when $\hat{e}$ is a comparison operator, since its value is either 0 or 1.</footnote>
forward transfer functions, remembered expression return their values and unremembered variables return the top element. The following lemma proves our judgement captures the intended meaning:

LEMMA 8.1. If $\Gamma^{\#} \models \hat{e} \llcorner z^{\#}$, then $\forall \Gamma \in \tilde{N}.\hat{y}(\Gamma^{\#})$, $\hat{E} \llcorner \hat{e}](\Gamma) \in \gamma_{Z^{\#}}(z^{\#})$.

PROOF. By induction on expressions, and soundness of $\tilde{\omega}$.

□

The judgement $\Gamma^{\#} \Rightarrow \Gamma'^{\#}$ is a reduction operator [Granger 1992], it implies that $\Gamma^{\#}$ and $\Gamma'^{\#}$ represent the same abstraction $(\tilde{N}.\hat{y}(\Gamma^{\#}) = \tilde{N}.\hat{y}(\Gamma'^{\#}))$ but $\Gamma'^{\#}$ is smaller. Its induction rules are given in the middle of Figure 12. REDUCEBWD propagates constraints [Benhamou et al. 1999] of the form $\hat{e} \in \gamma_{Z^{\#}}(z^{\#})$ between the symbolic expressions. Thus, it learns from conditions [Granger 1992] (appearing e.g. in if statements). The result is saved when the precision has improved, which allows further evaluations with $\Rightarrow$ to also improve. REDUCEFWD saves the result of evaluation. This will make the result of future joins more precise. Finally, REDUCEBOT quickly propagates the information that the current state is bottom (some constraint is unsatisfiable).

The domain operations are given as rules instead of functions as they depend on how many reductions ($\Rightarrow$) we wish to perform before returning the result. Performing more reductions will be more precise but also reduce performance.

$\tilde{N}.assûme(\hat{e}, \Gamma^{\#})$ propagates constraints, adding the information that the guard must be true (denoted as $\neg 0^9$). Nbind($B$, $\Gamma^{\#}$) updates the abstract SSA state $\Gamma^{\#}$ by mapping $\hat{x}$ to the result of the evaluation of $\hat{e}$ for all bindings $\hat{x} \mapsto \hat{e}$ that appear in the bindings $B$. The last operation, $\tilde{N}.joîn$, applies the bindings, and then performs an intersection of the maps (only keeping expressions that are present in all branches, including freshly bound variables). We can perform an intersection because we know nothing important about a symbolic expression that is not present in every branch (in many cases, they will go out of scope and be unbounded).

## 8.2 Combination of SSA-based analysis and online SSA translation

We can use this SSA state abstraction with the translation of Section 7 to analyze an SSA program while it is being computed from the source program. This analysis combines our SSA abstract state $\Gamma^{\#}$ with an abstract store $\sigma^{\#} \in \mathcal{X} \to \hat{E}$.

This combination is more precise than the standard non-relational numerical analysis performed by N (that constrains program variables instead of program values), i.e. we can abstract our combination to a standard numerical analysis.

$$ \alpha \in \text{Lift}(\tilde{N}), \Sigma^{\#} \to N, \Sigma^{\#} \\ \alpha(\sigma^{\#}, \Gamma^{\#}) \triangleq [x \in \mathcal{X} \mapsto z^{\#} \mid \Gamma^{\#} \models \sigma^{\#}(x) \llcorner z^{\#}] $$

Intuitively, this abstraction forgets the relations between the variables that are given by the symbolic expressions, and just sees them as opaque identifiers. In particular, we can prove that our analysis operations are monotonic (provided a suitable strategy for applying $\Rightarrow$, such as maximally applying $\Rightarrow$ when evaluation is limited to the symbolic expressions that appear in the abstract store), and thus that our combination is always more precise than the non-relational abstract domain for any succession of operations.

We can also provide specific examples where our analysis improves over a non-relational domain:

* **Reduction on related variables:** in $y := x+1$; $z := y*y$; if ($2 \le y \le 5$) ... , the Lift($\tilde{N}$) domain can prove that $4 \le z \le 25$ and $1 \le x \le 4$ while N cannot. This is very useful when analyzing machine code, which often places related variables in separate registers (and flags).

<footnote n="9">⁹Interval or congruence cannot represent this accurately, but a specialized 0/≠ 0 domain could be used here, or we could use a specific rule for when $\hat{e}$ is a comparison operator, since its value is either 0 or 1.</footnote>
* **Propagation across statements:** in $c := x < 7$; if(c) ..., the SSA-based domain can prove $x < 7$ after the if, while the IMP numeric domain cannot. Our domain thus avoids the limitation that reduction over a condition [Granger 1992] is limited to the current statement.

* **Remembering previously known facts:** the Lift($\hat{N}$) domain can store information that the interval single-value abstraction cannot remember. For instance, it can prove both if($x!=0$) assert($x!=0$) and if($x*x == 4$) assert($x*x==4$), both of which cannot be proven from a simple interval abstraction of $x$.

* **Benefiting from global value numbering:** We could improve precision further by adding global value numbering [Alpern et al. 1988; Rosen et al. 1988] in our Lift domain [Lemerre 2023]. We could then prove that both i and j are equal to 7 after running: i := j := 0; while(i < 7) {i++; j++}.

In general, the domain Lift($\hat{N}$) does not lose precision when analyzing a source which has computations split across multiple statements and variables, as is often the case with machine code. This is the strong relative completeness property, defined by Logozzo and Fähndrich [2008].

LEMMA 8.2 (STRONG RELATIVE COMPLETENESS). Let $C \in \mathcal{G} \to \mathcal{G}$ be the transformation that flattens IMP program expression by writing all sub-expressions to new temporary variables, and $\pi$ a projection that strips those newly introduced variables, then

$$ \text{analyse}_G(\text{Lift}(\hat{N})) = \pi(\text{analyse}_{C(G)}(\text{Lift}(\hat{N}))) $$

See proof in Appendix A.5.

# 9 EVALUATION

## 9.1 Evaluating using TAI

While our study is mostly theoretical, some of our claims can be validated through a practical implementation. We are interested in the following research questions: how does SSA-based numerical analysis (Lift($\hat{N}$)) compare to standard numerical analysis (N), both in terms of precision and complexity? What overhead is introduced by using free algebra domains and the SSA lift domain?

To answer these, we have written a small abstract interpreter named TAI in OCaml, following the definitions of this paper. It implements all domains and functors presented in this paper, and allows combining them freely. We have run TAI on some C programs generated using CSMITH [Yang et al. 2011] (limited to the constructs that IMP can represent: integer variables and non-recursive function calls only). We then recorded the average analysis time over 100 passes. This is only the time of the fixed-point calculation in analyse, it does not include parsing time or computation of the set W.

To validate precision, we run the analysis using N and Lift($\hat{N}$) in parallel. We compare the precision using two metrics: the first compares the abstractions of all variables in all locations, the second compares the abstractions of expressions that appear on outgoing edges in all locations.

Our results are presented in Table 1. We found that adding FA domains barely increases cost. It even improves it in some case as we used hash-consing to have fast equality on the free-algebra, thus skipping the slower numerical equality in our fixed-point computation. The SSA numeric domain increases cost by a reasonable factor. The free algebra alone is quite fast, the SSA free algebra is very slow mostly because of the Lift functor. Lift($\hat{N} \times \hat{F} \hat{A}$) is faster than Lift($\hat{F} \hat{A}$) since queries on the numerical domain greatly reduce the number of nodes being considered.

In terms of precision, the SSA numeric abstraction is always equal or more precise than the standard one. The first metric's specific counts mean little, as variables often have the same value in multiple locations, so a single improvement can be counted multiple times. The second metric does not have this issue and shows that 5 to 10% of outgoing edges have a strict precision improvement in most programs. Note that these metrics say nothing of how big that improvement is.
* **Propagation across statements:** in $c := x < 7$; if(c) ..., the SSA-based domain can prove $x < 7$ after the if, while the IMP numeric domain cannot. Our domain thus avoids the limitation that reduction over a condition [Granger 1992] is limited to the current statement.

* **Remembering previously known facts:** the Lift($\hat{N}$) domain can store information that the interval single-value abstraction cannot remember. For instance, it can prove both if($x!=0$) assert($x!=0$) and if($x*x == 4$) assert($x*x==4$), both of which cannot be proven from a simple interval abstraction of $x$.

* **Benefiting from global value numbering:** We could improve precision further by adding global value numbering [Alpern et al. 1988; Rosen et al. 1988] in our Lift domain [Lemerre 2023]. We could then prove that both i and j are equal to 7 after running: i := j := 0; while(i < 7) {i++; j++}.

In general, the domain Lift($\hat{N}$) does not lose precision when analyzing a source which has computations split across multiple statements and variables, as is often the case with machine code. This is the strong relative completeness property, defined by Logozzo and Fähndrich [2008].

LEMMA 8.2 (STRONG RELATIVE COMPLETENESS). Let $C \in \mathcal{G} \to \mathcal{G}$ be the transformation that flattens IMP program expression by writing all sub-expressions to new temporary variables, and $\pi$ a projection that strips those newly introduced variables, then

$$ \text{analyse}_G(\text{Lift}(\hat{N})) = \pi(\text{analyse}_{C(G)}(\text{Lift}(\hat{N}))) $$

See proof in Appendix A.5.

# 9 EVALUATION

## 9.1 Evaluating using TAI

While our study is mostly theoretical, some of our claims can be validated through a practical implementation. We are interested in the following research questions: how does SSA-based numerical analysis (Lift($\hat{N}$)) compare to standard numerical analysis (N), both in terms of precision and complexity? What overhead is introduced by using free algebra domains and the SSA lift domain?

To answer these, we have written a small abstract interpreter named TAI in OCaml, following the definitions of this paper. It implements all domains and functors presented in this paper, and allows combining them freely. We have run TAI on some C programs generated using CSMITH [Yang et al. 2011] (limited to the constructs that IMP can represent: integer variables and non-recursive function calls only). We then recorded the average analysis time over 100 passes. This is only the time of the fixed-point calculation in analyse, it does not include parsing time or computation of the set W.

To validate precision, we run the analysis using N and Lift($\hat{N}$) in parallel. We compare the precision using two metrics: the first compares the abstractions of all variables in all locations, the second compares the abstractions of expressions that appear on outgoing edges in all locations.

Our results are presented in Table 1. We found that adding FA domains barely increases cost. It even improves it in some case as we used hash-consing to have fast equality on the free-algebra, thus skipping the slower numerical equality in our fixed-point computation. The SSA numeric domain increases cost by a reasonable factor. The free algebra alone is quite fast, the SSA free algebra is very slow mostly because of the Lift functor. Lift($\hat{N} \times \hat{F} \hat{A}$) is faster than Lift($\hat{F} \hat{A}$) since queries on the numerical domain greatly reduce the number of nodes being considered.

In terms of precision, the SSA numeric abstraction is always equal or more precise than the standard one. The first metric's specific counts mean little, as variables often have the same value in multiple locations, so a single improvement can be counted multiple times. The second metric does not have this issue and shows that 5 to 10% of outgoing edges have a strict precision improvement in most programs. Note that these metrics say nothing of how big that improvement is.
<table><caption>Table 1. Execution time (in milliseconds) of our analysis of each domain, along with the ratio (time for this domain/time for N). All domains were passed through the query simplification functor Q, which not mentioned in the header. LOC indicates lines of code in each file, as counted by cloc.</caption><thead><tr><th>File</th><th>LOC</th><th>N</th><th>Lift(Î)</th><th>N×FA</th><th>Lift(Î)×FA</th><th>FA</th><th>Lift(FA)</th><th>Lift(Î×FA)</th></tr></thead><tbody><tr><td>c00.c</td><td>237</td><td>57</td><td>130 (2.3)</td><td>66 (1.16)</td><td>125 (2.2)</td><td>6 (0.11)</td><td>130 (2.3)</td><td>136 (2.39)</td></tr><tr><td>c02.c</td><td>393</td><td>87</td><td>86 (0.99)</td><td>103 (1.18)</td><td>100 (1.14)</td><td>17 (0.2)</td><td>334 (3.82)</td><td>81 (0.93)</td></tr><tr><td>c04.c</td><td>304</td><td>13</td><td>39 (3.09)</td><td>11 (0.9)</td><td>41 (3.25)</td><td>3 (0.25)</td><td>45 (3.54)</td><td>40 (3.15)</td></tr><tr><td>c07.c</td><td>397</td><td>12</td><td>25 (2.09)</td><td>12 (1.05)</td><td>27 (2.27)</td><td>9 (0.8)</td><td>131 (11.1)</td><td>27 (2.28)</td></tr><tr><td>c18.c</td><td>292</td><td>84</td><td>193 (2.3)</td><td>93 (1.11)</td><td>207 (2.47)</td><td>8 (0.1)</td><td>234 (2.79)</td><td>180 (2.15)</td></tr><tr><td>c23.c</td><td>3174</td><td>50</td><td>348 (7.02)</td><td>52 (1.05)</td><td>357 (7.2)</td><td>90 (1.82)</td><td>20.7s (418)</td><td>346 (6.98)</td></tr><tr><td>c24.c</td><td>11076</td><td>6.2s</td><td>20.4s (3.3)</td><td>5.3s (0.86)</td><td>19.4s (3.14)</td><td>2s (0.33)</td><td>>10min</td><td>18.6s (3.01)</td></tr><tr><td>c29.c</td><td>2347</td><td>140</td><td>276 (1.98)</td><td>119 (0.85)</td><td>262 (1.88)</td><td>99 (0.71)</td><td>15.1s (108)</td><td>588 (4.21)</td></tr><tr><td>c30.c</td><td>1178</td><td>200</td><td>355 (1.77)</td><td>189 (0.95)</td><td>396 (1.98)</td><td>70 (0.35)</td><td>8.8s (44.2)</td><td>1361 (6.8)</td></tr></tbody></table>

## 9.2 Practical experience

The compiling-with-abstract-interpretation method presented in this paper has also been implemented as part of a generic static analysis library named CODEX. It is an abstract interpreter that supports not only the whole of C, but also a number of machine code formats (x86, ARM, AMD, RISC-V), notably used in [Nicole et al. 2021, 2022]. This library is a collection of abstract domains which lifts SSA-based numerical abstractions to standard analysis abstractions, whose interface correspond to either the C or machine code language. Most of the code is generic (and related to the memory abstractions, that are not covered in the present paper); the C-specific frontend requires only 3KLOC, and the binary-specific one 4KLOC (excluding the parsers that come from external components).

We have proved that the Lift(Î) domain is always more precise than the direct numerical analysis, and that it solves the small-code window problem. In practice, this domain is key to the precision of machine code analysis, but is also very often useful when analyzing C. An important feature of the SSA lift is that it is very easy to rewrite SSA expressions to improve precision, which is often needed when analyzing machine code [Djoudi et al. 2016].

One of the main applications of the free algebra domain is that we can automatically produce a simplified program that corresponds to all the traces leading to a remaining alarm or unproved assertion. This SSA program can easily be converted to Constrained Horn Clauses for verification by a goal-oriented software model checker like Spacer [Gurfinkel 2022] to remove these remaining alarms. We found that the simplifications performed by the abstract interpreter are key to help Spacer solve the formula (especially memory reasoning, which is a weak point of SMT solvers). Note, for instance that the nature of the terms in our SSA free algebra domain implies that the generated program is automatically sliced [Weiser 1984] for free.

## 10 RELATED WORK

*Abstract interpretation for compilation, and compiling for abstract interpretation.* Using static analyses to perform program transformations is the quintessential job of a compiler; we refer to Cousot and Cousot [2002] for a formal treatment of this subject. Studying how program transformations can affect the precision of an analysis has been comparatively less studied. It is known that functionally equivalent but intensionally different programs may yield different results when analyzed, and thus that program transformation may affect the precision of an analysis [Bruni et al. 2020; Giacobazzi et al. 2015].
<table><caption>Table 1. Execution time (in milliseconds) of our analysis of each domain, along with the ratio (time for this domain/time for N). All domains were passed through the query simplification functor Q, which not mentioned in the header. LOC indicates lines of code in each file, as counted by cloc.</caption><thead><tr><th>File</th><th>LOC</th><th>N</th><th>Lift(Î)</th><th>N×FA</th><th>Lift(Î)×FA</th><th>FA</th><th>Lift(FA)</th><th>Lift(Î×FA)</th></tr></thead><tbody><tr><td>c00.c</td><td>237</td><td>57</td><td>130 (2.3)</td><td>66 (1.16)</td><td>125 (2.2)</td><td>6 (0.11)</td><td>130 (2.3)</td><td>136 (2.39)</td></tr><tr><td>c02.c</td><td>393</td><td>87</td><td>86 (0.99)</td><td>103 (1.18)</td><td>100 (1.14)</td><td>17 (0.2)</td><td>334 (3.82)</td><td>81 (0.93)</td></tr><tr><td>c04.c</td><td>304</td><td>13</td><td>39 (3.09)</td><td>11 (0.9)</td><td>41 (3.25)</td><td>3 (0.25)</td><td>45 (3.54)</td><td>40 (3.15)</td></tr><tr><td>c07.c</td><td>397</td><td>12</td><td>25 (2.09)</td><td>12 (1.05)</td><td>27 (2.27)</td><td>9 (0.8)</td><td>131 (11.1)</td><td>27 (2.28)</td></tr><tr><td>c18.c</td><td>292</td><td>84</td><td>193 (2.3)</td><td>93 (1.11)</td><td>207 (2.47)</td><td>8 (0.1)</td><td>234 (2.79)</td><td>180 (2.15)</td></tr><tr><td>c23.c</td><td>3174</td><td>50</td><td>348 (7.02)</td><td>52 (1.05)</td><td>357 (7.2)</td><td>90 (1.82)</td><td>20.7s (418)</td><td>346 (6.98)</td></tr><tr><td>c24.c</td><td>11076</td><td>6.2s</td><td>20.4s (3.3)</td><td>5.3s (0.86)</td><td>19.4s (3.14)</td><td>2s (0.33)</td><td>>10min</td><td>18.6s (3.01)</td></tr><tr><td>c29.c</td><td>2347</td><td>140</td><td>276 (1.98)</td><td>119 (0.85)</td><td>262 (1.88)</td><td>99 (0.71)</td><td>15.1s (108)</td><td>588 (4.21)</td></tr><tr><td>c30.c</td><td>1178</td><td>200</td><td>355 (1.77)</td><td>189 (0.95)</td><td>396 (1.98)</td><td>70 (0.35)</td><td>8.8s (44.2)</td><td>1361 (6.8)</td></tr></tbody></table>

## 9.2 Practical experience

The compiling-with-abstract-interpretation method presented in this paper has also been implemented as part of a generic static analysis library named CODEX. It is an abstract interpreter that supports not only the whole of C, but also a number of machine code formats (x86, ARM, AMD, RISC-V), notably used in [Nicole et al. 2021, 2022]. This library is a collection of abstract domains which lifts SSA-based numerical abstractions to standard analysis abstractions, whose interface correspond to either the C or machine code language. Most of the code is generic (and related to the memory abstractions, that are not covered in the present paper); the C-specific frontend requires only 3KLOC, and the binary-specific one 4KLOC (excluding the parsers that come from external components).

We have proved that the Lift(Î) domain is always more precise than the direct numerical analysis, and that it solves the small-code window problem. In practice, this domain is key to the precision of machine code analysis, but is also very often useful when analyzing C. An important feature of the SSA lift is that it is very easy to rewrite SSA expressions to improve precision, which is often needed when analyzing machine code [Djoudi et al. 2016].

One of the main applications of the free algebra domain is that we can automatically produce a simplified program that corresponds to all the traces leading to a remaining alarm or unproved assertion. This SSA program can easily be converted to Constrained Horn Clauses for verification by a goal-oriented software model checker like Spacer [Gurfinkel 2022] to remove these remaining alarms. We found that the simplifications performed by the abstract interpreter are key to help Spacer solve the formula (especially memory reasoning, which is a weak point of SMT solvers). Note, for instance that the nature of the terms in our SSA free algebra domain implies that the generated program is automatically sliced [Weiser 1984] for free.

## 10 RELATED WORK

*Abstract interpretation for compilation, and compiling for abstract interpretation.* Using static analyses to perform program transformations is the quintessential job of a compiler; we refer to Cousot and Cousot [2002] for a formal treatment of this subject. Studying how program transformations can affect the precision of an analysis has been comparatively less studied. It is known that functionally equivalent but intensionally different programs may yield different results when analyzed, and thus that program transformation may affect the precision of an analysis [Bruni et al. 2020; Giacobazzi et al. 2015].
One particular instance is the loss of precision induced when analyzing a compiled code compared to its source version. Logozzo and Fähndrich [2008] explains that compiled code analysis is less precise because instructions have a smaller code window: typical low-level instructions are three-address code "$r_i \leftarrow r_j \oplus r_k$" or conditional jumps on the value of a flag register "if(z) goto l", while instructions in source programs can view arbitrary large expressions with statements of the form "$x := e$" or "if(e)". They then establish notions of strong completeness, asking whether an analysis can be as precise on the source and binary executable. We prove that our SSA translation and SSA-based non-relational domain is always more precise than the standard non-relational abstract domain, and furthermore fulfills the strong relative completeness property, thus allowing byte-compiled code to be analyzed as precisely as source programs using this domain.

It is common to perform a preprocessing transformation to enhance the precision of static analyses. For instance, Djoudi et al. [2016] undoes compiler transformations to recover high-level conditions from sequences of machine code instructions to help their static analyzer. But often, these program transformations are performed online, during the analysis, so that the transformation can benefit from the invariants computed by the analysis. For instance, Miné [2006] linearizes expression and substitutes variables with their assigned expression; Boillot and Feret [2023] transform modular arithmetic to standard arithmetic when possible. In particular, the dynamic expression rewriting domains in MOPSA [Journault et al. 2019], used to simplify the language handled by the lower layers of the analysis, are very similar to the transformation functors of Section 5. Symbolic domains have also been used for the numerical properties that they can infer (e.g. to detect equalities [Chang and Leino 2005; Kildall 1973; Lemerre 2023]), or as part of an abstract domain (for instance, Gange et al. [2016] propagate non-relational values on terms instead of variables, similarly to our SSA-lift on SSA non-relational domain combination Lift($\hat{N}$)).

*Intertwining transformation and analysis.* The traditional compiler design as a sequence of passes allows transformations and analyses to help each other. For instance, analyses may help perform register promotion, which will help analyses with a basic representation of memory. These improvements can be done in a fixed-point until maximum precision is reached. However, this will not be as precise as doing all the analyses and transformations simultaneously [Click and Cooper 1995], and transformations are often grouped to gain precision; sparse conditional constant propagation [Wegman and Zadeck 1991] is a prime example of this. Abstract interpretation provides systematic methods to combine analyses [Cousot and Cousot 1979], such as reduced products, which allows implementing these combinations while maintaining a modular code base. In practice, reduced products are implemented by having each analysis communicate through common abstractions (called communication channels in Astrée [Cousot et al. 2006]). Another method for combining analyses is the exchange of program transformations [Lerner et al. 2002]; a consequence of our work is that this can be viewed as using the free algebra abstract domain (FA) as a communication channel between domains. When the shared program fragment is sea-of-node SSA [Click and Paleczny 1995], as in Rompf [2012], then the communication channel is the free SSA algebra abstract domain.

*Interpreters and compiler as (co)algebras on the program expressions.* The idea of using an algebra signature over program expressions that can correspond to concrete or abstract semantics has been proposed in the context of structured programs. Our main contribution in this area is to use the standard abstract domain signature to generate programs.

A very inspiring work in this area are the *tagless-final interpreters* of Carette et al. [2009] and Kiselyov [2010]. In this work, the same language signature (for the PCF functional programming language) is used to implement both a concrete interpreter, a compiler, partial evaluation/constant
One particular instance is the loss of precision induced when analyzing a compiled code compared to its source version. Logozzo and Fähndrich [2008] explains that compiled code analysis is less precise because instructions have a smaller code window: typical low-level instructions are three-address code "$r_i \leftarrow r_j \oplus r_k$" or conditional jumps on the value of a flag register "if(z) goto l", while instructions in source programs can view arbitrary large expressions with statements of the form "$x := e$" or "if(e)". They then establish notions of strong completeness, asking whether an analysis can be as precise on the source and binary executable. We prove that our SSA translation and SSA-based non-relational domain is always more precise than the standard non-relational abstract domain, and furthermore fulfills the strong relative completeness property, thus allowing byte-compiled code to be analyzed as precisely as source programs using this domain.

It is common to perform a preprocessing transformation to enhance the precision of static analyses. For instance, Djoudi et al. [2016] undoes compiler transformations to recover high-level conditions from sequences of machine code instructions to help their static analyzer. But often, these program transformations are performed online, during the analysis, so that the transformation can benefit from the invariants computed by the analysis. For instance, Miné [2006] linearizes expression and substitutes variables with their assigned expression; Boillot and Feret [2023] transform modular arithmetic to standard arithmetic when possible. In particular, the dynamic expression rewriting domains in MOPSA [Journault et al. 2019], used to simplify the language handled by the lower layers of the analysis, are very similar to the transformation functors of Section 5. Symbolic domains have also been used for the numerical properties that they can infer (e.g. to detect equalities [Chang and Leino 2005; Kildall 1973; Lemerre 2023]), or as part of an abstract domain (for instance, Gange et al. [2016] propagate non-relational values on terms instead of variables, similarly to our SSA-lift on SSA non-relational domain combination Lift($\hat{N}$)).

*Intertwining transformation and analysis.* The traditional compiler design as a sequence of passes allows transformations and analyses to help each other. For instance, analyses may help perform register promotion, which will help analyses with a basic representation of memory. These improvements can be done in a fixed-point until maximum precision is reached. However, this will not be as precise as doing all the analyses and transformations simultaneously [Click and Cooper 1995], and transformations are often grouped to gain precision; sparse conditional constant propagation [Wegman and Zadeck 1991] is a prime example of this. Abstract interpretation provides systematic methods to combine analyses [Cousot and Cousot 1979], such as reduced products, which allows implementing these combinations while maintaining a modular code base. In practice, reduced products are implemented by having each analysis communicate through common abstractions (called communication channels in Astrée [Cousot et al. 2006]). Another method for combining analyses is the exchange of program transformations [Lerner et al. 2002]; a consequence of our work is that this can be viewed as using the free algebra abstract domain (FA) as a communication channel between domains. When the shared program fragment is sea-of-node SSA [Click and Paleczny 1995], as in Rompf [2012], then the communication channel is the free SSA algebra abstract domain.

*Interpreters and compiler as (co)algebras on the program expressions.* The idea of using an algebra signature over program expressions that can correspond to concrete or abstract semantics has been proposed in the context of structured programs. Our main contribution in this area is to use the standard abstract domain signature to generate programs.

A very inspiring work in this area are the *tagless-final interpreters* of Carette et al. [2009] and Kiselyov [2010]. In this work, the same language signature (for the PCF functional programming language) is used to implement both a concrete interpreter, a compiler, partial evaluation/constant
propagation and transformation-passes functors that transform the program to compilation-passing style, a form which is equivalent to SSA [Kelsey 1995]. Our work differs in that our analysis signature corresponds to the abstract semantics rather than the concrete one (i.e. our work could be described as tagless-final abstract interpretation), and targets unstructured imperative programs rather than higher-order functional programs.

It is generally desirable that the structure of an abstract interpreter or compiler mimics (or is derived from) the structure of the concrete interpreter (see e.g. [Bodin et al. 2019; Roșu and Serbanuta 2010]). This enables building the abstract interpreter by composing abstractions of the different concepts of the concrete language [Darais et al. 2017, 2015; Keidel and Erdweg 2019; Sergey et al. 2013]. While in this paper we have composed abstraction using product and functor domains, it would be interesting to combine compiling-with-abstract interpretation with other compositional design of abstract interpreters to produce modular single-pass compilers.

*Formal verification of compiler passes.* The correctness theorem on our functor domains used as compiler passes is stuttering bisimulation between widening points of the program, which is unusual in the field of semantic-preserving compilers [Appel 2014; Leroy 2009]. There seems to be some benefits to these theorems. Firstly, as you cannot perform, neither in the source nor target language, an infinite number of steps without encountering a widening point, this ensures that the bisimulation between both traces remains synchronized. Secondly, it also allows including infinite traces in the correctness argument. Finally, bisimulation proofs handle non-deterministic program semantics (like the ones used in the paper), unlike the common technique of proving only forward simulation assuming that the target language is deterministic [Leroy 2009].

# 11 CONCLUSION

Our contributions can be summarized using the following key messages: abstract interpreters can be transformed into compilers by using a free algebra computing terms over the abstract domain signature. Different languages have different abstract signatures, that can be non-standard, like the SSA abstract domain.Functor domains can be seen as compiler passes that all run simultaneously, rather than sequentially. Combining symbolic and semantic analyses can significantly improve precision, both in theory and in practice, as exemplified by our SSA-based non-relational abstract domain.

In future work, it would be interesting to see if lifting functor domains to compiler passes can be an effective method to design compilers, as our practical experience with this method is limited to the compilation of a program to horn clauses and SMT formulas. Note that even if our source and target languages encodes conditional jumps as non-determinism and guards, it is possible to re-encode the result using standard target languages like LLVM [Lemerre 2023]. An important issue is that abstract domains are usually sound but incomplete, which in the case of a functor used as a compiler pass, means that the pass adds behaviors that are not present in the source program. We believe however that many program transformations and corresponding functors are both sound and complete. It is also possible that behavioral refinement [Dockins 2012], which translates program that go wrong to executable traces, could also fit our framework; however, passes performing choice refinement, i.e. removing determinism from the source language, does not seem to be expressible as abstract interpretation functors. Another interesting direction would be to see if lifting semantic soundness and completeness proofs on functor domains (as done by Jourdan et al. [2015]) to compiler passes could be an effective method to formally implement and verify these passes. Finally, the current analysis is limited to forward analysis. Performing any backwards analysis (like liveness) must be done in a separate stage. It would be interesting to see if this restriction can be lifted.
propagation and transformation-passes functors that transform the program to compilation-passing style, a form which is equivalent to SSA [Kelsey 1995]. Our work differs in that our analysis signature corresponds to the abstract semantics rather than the concrete one (i.e. our work could be described as tagless-final abstract interpretation), and targets unstructured imperative programs rather than higher-order functional programs.

It is generally desirable that the structure of an abstract interpreter or compiler mimics (or is derived from) the structure of the concrete interpreter (see e.g. [Bodin et al. 2019; Roșu and Serbanuta 2010]). This enables building the abstract interpreter by composing abstractions of the different concepts of the concrete language [Darais et al. 2017, 2015; Keidel and Erdweg 2019; Sergey et al. 2013]. While in this paper we have composed abstraction using product and functor domains, it would be interesting to combine compiling-with-abstract interpretation with other compositional design of abstract interpreters to produce modular single-pass compilers.

*Formal verification of compiler passes.* The correctness theorem on our functor domains used as compiler passes is stuttering bisimulation between widening points of the program, which is unusual in the field of semantic-preserving compilers [Appel 2014; Leroy 2009]. There seems to be some benefits to these theorems. Firstly, as you cannot perform, neither in the source nor target language, an infinite number of steps without encountering a widening point, this ensures that the bisimulation between both traces remains synchronized. Secondly, it also allows including infinite traces in the correctness argument. Finally, bisimulation proofs handle non-deterministic program semantics (like the ones used in the paper), unlike the common technique of proving only forward simulation assuming that the target language is deterministic [Leroy 2009].

# 11 CONCLUSION

Our contributions can be summarized using the following key messages: abstract interpreters can be transformed into compilers by using a free algebra computing terms over the abstract domain signature. Different languages have different abstract signatures, that can be non-standard, like the SSA abstract domain.Functor domains can be seen as compiler passes that all run simultaneously, rather than sequentially. Combining symbolic and semantic analyses can significantly improve precision, both in theory and in practice, as exemplified by our SSA-based non-relational abstract domain.

In future work, it would be interesting to see if lifting functor domains to compiler passes can be an effective method to design compilers, as our practical experience with this method is limited to the compilation of a program to horn clauses and SMT formulas. Note that even if our source and target languages encodes conditional jumps as non-determinism and guards, it is possible to re-encode the result using standard target languages like LLVM [Lemerre 2023]. An important issue is that abstract domains are usually sound but incomplete, which in the case of a functor used as a compiler pass, means that the pass adds behaviors that are not present in the source program. We believe however that many program transformations and corresponding functors are both sound and complete. It is also possible that behavioral refinement [Dockins 2012], which translates program that go wrong to executable traces, could also fit our framework; however, passes performing choice refinement, i.e. removing determinism from the source language, does not seem to be expressible as abstract interpretation functors. Another interesting direction would be to see if lifting semantic soundness and completeness proofs on functor domains (as done by Jourdan et al. [2015]) to compiler passes could be an effective method to formally implement and verify these passes. Finally, the current analysis is limited to forward analysis. Performing any backwards analysis (like liveness) must be done in a separate stage. It would be interesting to see if this restriction can be lifted.
# ACKNOWLEDGEMENTS

This research was supported in part by the Agence Nationale de la Recherche (ANR) grant agreement ANR-22-CE39-0014-03 (EMASS project).

# DATA-AVAILABILITY STATEMENT

The software that supports Section 9 is available on Zenodo DOI 10.5281/zenodo.10895582 [Lesbre and Lemerre 2024a]. The Codex analyzer is available on www.codex.top [Lemerre et al. 2024].

# REFERENCES

* Bowen Alpern, Mark N Wegman, and F Kenneth Zadeck. 1988. Detecting equality of variables in programs, In Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. ACM-SIGACT Symposium on Principles of Programming Languages, 1-11. https://doi.org/10.1145/73560.73561

* Andrew W. Appel. 2014. *Program Logics - for Certified Compilers*. Cambridge University Press.

* Zena M. Ariola and Jan Willem Klop. 1996. Equational Term Graph Rewriting. *Fundamenta Informaticae* 26 (12 1996), 207-240. https://doi.org/10.3233/fi-1996-263401

* John Aycock and R. Nigel Horspool. 2000. Simple Generation of Static Single-Assignment Form. In *9th International Conference on Compiler Construction - CC 2000 (LNCS, Vol. 1781)*. Springer, 110-124. https://doi.org/10.1007/3-540-46423-9_8

* Gogul Balakrishnan and Thomas W. Reps. 2010. WYSINWYX: What you see is not what you eXecute. *ACM Trans. Program. Lang. Syst.* 32, 6 (2010), 23:1-23:84. https://doi.org/10.1145/1749608.1749612

* Frédéric Benhamou, Frédéric Goualard, Laurent Granvilliers, and Jean-François Puget. 1999. Revising hull and box consistency, In Logic Programming: Proceedings of the 1999 International Conference on Logic Programming. *International Conference on Logic Programming*, 230. https://doi.org/10.7551/mitpress/4304.003.0024

* Martin Bodin, Philippa Gardner, Thomas P. Jensen, and Alan Schmitt. 2019. Skeletal semantics and their interpretations. *Proc. ACM Program. Lang.* 3, POPL (2019), 44:1-44:31. https://doi.org/10.1145/3290357

* Jérôme Boillot and Jérôme Feret. 2023. Symbolic Transformation of Expressions in Modular Arithmetic. (10 2023), 84-113. https://doi.org/10.1007/978-3-031-44245-2_6

* François Bourdoncle. 1993. Efficient chaotic iteration strategies with widenings, In Formal Methods in Programming and Their Applications, Dines Bjørner, Manfred Broy, and Igor V. Pottosin (Eds.). *Formal Methods in Programming and Their Applications*, 128-141. https://doi.org/10.1007/bfb0039704

* Marc M. Brandis and Hanspeter Mössenböck. 1994. Single-Pass Generation of Static Single-Assignment Form for Structured Languages. *ACM Trans. Program. Lang. Syst.* 16, 6 (1994), 1684-1698. https://doi.org/10.1145/197320.197331

* Matthias Braun, Sebastian Buchwald, Sebastian Hack, Roland Leißa, Christoph Mallon, and Andreas Zwinkau. 2013. Simple and Efficient Construction of Static Single Assignment Form. In *22nd International Conference on Compiler Construction (CC 2013)*. https://doi.org/10.1007/978-3-642-37051-9_6

* Roberto Bruni, Roberto Giacobazzi, Roberta Gori, Isabel Garcia-Contreras, and Dusko Pavlovic. 2020. Abstract extensionality: on the properties of incomplete abstract interpretations. *Proc. ACM Program. Lang.* 4, POPL (2020), 28:1-28:28. https://doi.org/10.1145/3371096

* Jacques Carette, Oleg Kiselyov, and Chung-chieh Shan. 2009. Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages. *Journal of Functional Programming* 19, 05 (2009), 509-543.

* Bor-Yuh Evan Chang and K. Rustan M. Leino. 2005. *Abstract Interpretation with Alien Expressions and Heap Structures*. Springer, 147-163. https://doi.org/10.1007/978-3-540-30579-8_11

* Cliff Click and Keith D. Cooper. 1995. Combining Analyses, Combining Optimizations. *ACM Trans. Program. Lang. Syst.* 17, 2 (1995), 181-196. https://doi.org/10.1145/201059.201061

* Cliff Click and Michael Paleczny. 1995. A simple graph-based intermediate representation. *ACM Sigplan Notices* 30, 3 (3 (1995), 35-49. https://doi.org/10.1145/202529.202534

* Patrick Cousot and Radhia Cousot. 1977. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints (*POPL* 1977). Association for Computing Machinery, New York, NY, USA, 238-252. https://doi.org/10.1145/512950.512973

* Patrick Cousot and Radhia Cousot. 1979. Systematic Design of Program Analysis Frameworks. In *6th ACM Symposium on Principles of Programming Languages (San Antonio, Texas) (POPL 1979)*. Association for Computing Machinery, New York, NY, USA, 269-282. https://doi.org/10.1145/567752.567778

* Patrick Cousot and Radhia Cousot. 2002. Systematic design of program transformation frameworks by abstract interpretation. In *29th Symposium on Principles of Programming Languages (POPL 2002)*, John Launchbury and John C. Mitchell (Eds.). ACM, 178-190. https://doi.org/10.1145/503272.503290
# ACKNOWLEDGEMENTS

This research was supported in part by the Agence Nationale de la Recherche (ANR) grant agreement ANR-22-CE39-0014-03 (EMASS project).

# DATA-AVAILABILITY STATEMENT

The software that supports Section 9 is available on Zenodo DOI 10.5281/zenodo.10895582 [Lesbre and Lemerre 2024a]. The Codex analyzer is available on www.codex.top [Lemerre et al. 2024].

# REFERENCES

- Bowen Alpern, Mark N Wegman, and F Kenneth Zadeck. 1988. Detecting equality of variables in programs, In Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. ACM-SIGACT Symposium on Principles of Programming Languages, 1-11. https://doi.org/10.1145/73560.73561

- Andrew W. Appel. 2014. *Program Logics - for Certified Compilers*. Cambridge University Press.

- Zena M. Ariola and Jan Willem Klop. 1996. Equational Term Graph Rewriting. *Fundamenta Informaticae* 26 (12 1996), 207-240. https://doi.org/10.3233/fi-1996-263401

- John Aycock and R. Nigel Horspool. 2000. Simple Generation of Static Single-Assignment Form. In *9th International Conference on Compiler Construction - CC 2000 (LNCS, Vol. 1781)*. Springer, 110-124. https://doi.org/10.1007/3-540-46423-9_8

- Gogul Balakrishnan and Thomas W. Reps. 2010. WYSINWYX: What you see is not what you eXecute. *ACM Trans. Program. Lang. Syst.* 32, 6 (2010), 23:1-23:84. https://doi.org/10.1145/1749608.1749612

- Frédéric Benhamou, Frédéric Goualard, Laurent Granvilliers, and Jean-François Puget. 1999. Revising hull and box consistency, In Logic Programming: Proceedings of the 1999 International Conference on Logic Programming. *International Conference on Logic Programming*, 230. https://doi.org/10.7551/mitpress/4304.003.0024

- Martin Bodin, Philippa Gardner, Thomas P. Jensen, and Alan Schmitt. 2019. Skeletal semantics and their interpretations. *Proc. ACM Program. Lang.* 3, POPL (2019), 44:1-44:31. https://doi.org/10.1145/3290357

- Jérôme Boillot and Jérôme Feret. 2023. Symbolic Transformation of Expressions in Modular Arithmetic. (10 2023), 84-113. https://doi.org/10.1007/978-3-031-44245-2_6

- François Bourdoncle. 1993. Efficient chaotic iteration strategies with widenings, In Formal Methods in Programming and Their Applications, Dines Bjørner, Manfred Broy, and Igor V. Pottosin (Eds.). *Formal Methods in Programming and Their Applications*, 128-141. https://doi.org/10.1007/bfb0039704

- Marc M. Brandis and Hanspeter Mössenböck. 1994. Single-Pass Generation of Static Single-Assignment Form for Structured Languages. *ACM Trans. Program. Lang. Syst.* 16, 6 (1994), 1684-1698. https://doi.org/10.1145/197320.197331

- Matthias Braun, Sebastian Buchwald, Sebastian Hack, Roland Leißa, Christoph Mallon, and Andreas Zwinkau. 2013. Simple and Efficient Construction of Static Single Assignment Form. In *22nd International Conference on Compiler Construction (CC 2013)*. https://doi.org/10.1007/978-3-642-37051-9_6

- Roberto Bruni, Roberto Giacobazzi, Roberta Gori, Isabel Garcia-Contreras, and Dusko Pavlovic. 2020. Abstract extensionality: on the properties of incomplete abstract interpretations. *Proc. ACM Program. Lang.* 4, POPL (2020), 28:1-28:28. https://doi.org/10.1145/3371096

- Jacques Carette, Oleg Kiselyov, and Chung-chieh Shan. 2009. Finally tagless, partially evaluated: Tagless staged interpreters for simpler typed languages. *Journal of Functional Programming* 19, 05 (2009), 509-543.

- Bor-Yuh Evan Chang and K. Rustan M. Leino. 2005. *Abstract Interpretation with Alien Expressions and Heap Structures*. Springer, 147-163. https://doi.org/10.1007/978-3-540-30579-8_11

- Cliff Click and Keith D. Cooper. 1995. Combining Analyses, Combining Optimizations. *ACM Trans. Program. Lang. Syst.* 17, 2 (1995), 181-196. https://doi.org/10.1145/201059.201061

- Cliff Click and Michael Paleczny. 1995. A simple graph-based intermediate representation. *ACM Sigplan Notices* 30, 3 (3 (1995), 35-49. https://doi.org/10.1145/202529.202534

- Patrick Cousot and Radhia Cousot. 1977. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints (*POPL 1977*). Association for Computing Machinery, New York, NY, USA, 238-252. https://doi.org/10.1145/512950.512973

- Patrick Cousot and Radhia Cousot. 1979. Systematic Design of Program Analysis Frameworks. In *6th ACM Symposium on Principles of Programming Languages (San Antonio, Texas) (POPL 1979)*. Association for Computing Machinery, New York, NY, USA, 269-282. https://doi.org/10.1145/567752.567778

- Patrick Cousot and Radhia Cousot. 2002. Systematic design of program transformation frameworks by abstract interpretation. In *29th Symposium on Principles of Programming Languages (POPL 2002)*, John Launchbury and John C. Mitchell (Eds.). ACM, 178-190. https://doi.org/10.1145/503272.503290
Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. 2006. Combination of Abstractions in the ASTRÈE Static Analyzer. In *Revised Selected Papers from the 11th Asian Computing Science Conference on Advances in Computer Science - Secure Software and Related Issues - ASIAN 2006* (Lecture Notes in Computer Science, Vol. 4435). Springer, 272–300. https://doi.org/10.1007/978-3-540-77505-8_23

Ron Cytron, Jeanne Ferrante, Barry K. Rosen, Mark N. Wegman, and F. Kenneth Zadeck. 1991. Efficiently Computing Static Single Assignment Form and the Control Dependence Graph. *ACM Trans. Program. Lang. Syst.* 13, 4 (oct 1991), 451–490. https://doi.org/10.1145/115372.115320

David Darais, Nicholas Labich, Phuc C. Nguyen, and David Van Horn. 2017. Abstracting definitional interpreters (functional pearl). *Proc. ACM Program. Lang.* 1, ICFP (2017), 12:1–12:25. https://doi.org/10.1145/3110256

David Darais, Matthew Might, and David Van Horn. 2015. Galois transformers and modular abstract interpreters: reusable metatheory for program analysis. In *Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2015, part of SPLASH 2015, Pittsburgh, PA, USA, October 25-30, 2015*, Jonathan Aldrich and Patrick Eugster (Eds.). ACM, 552–571. https://doi.org/10.1145/2814270.2814308

Delphine Demange, Yon Fernández de Retana, and David Pichardie. 2018. Semantic reasoning about the sea of nodes, In *Proceedings of the 27th International Conference on Compiler Construction, Christophe Dubach and Jingling Xue (Eds.). International Conference on Compiler Construction*, 163–173. https://doi.org/10.1145/3178372.3179503

Adel Djoudi, Sébastien Bardin, and Éric Goubault. 2016. Recovering High-Level Conditions from Binary Programs. In *21st International Symposium on Formal Methods (FM 2016)*. 235–253. https://doi.org/10.1007/978-3-319-48989-6_15

Robert W Dockins. 2012. *Operational refinement for compiler correctness*. Ph. D. Dissertation, Princeton University.

Jean-Christophe Filliâtre and Sylvain Conchon. 2006. Type-Safe Modular Hash-Consing. *ML Workshop* (9 2006), 12–19. https://doi.org/10.1145/1159876.1159880

Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard, and Peter J. Stuckey. 2016. An Abstract Domain of Uninterpreted Functions. In *Verification, Model Checking, and Abstract Interpretation (VMCAI 2016)*, Barbara Jobstmann and K. Rustan M. Leino (Eds.). Springer, 85–103. https://doi.org/10.1007/978-3-662-49122-5_4

Roberto Giacobazzi, Francesco Logozzo, and Francesco Ranzato. 2015. Analyzing Program Analyses. In *Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015*, Sriram K. Rajamani and David Walker (Eds.). ACM, 261–273. https://doi.org/10.1145/2676726.2676987

Philippe Granger. 1992. Improving the results of static analyses of programs by local decreasing iterations. In *International Conference on Foundations of Software Technology and Theoretical Computer Science*. Springer, Springer Berlin Heidelberg, 68–79. https://doi.org/10.1007/3-540-56287-7_95

Sumit Gulwani and George C. Necula. 2004. A Polynomial-Time Algorithm for Global Value Numbering. In *Static Analysis Symposium (SAS 2004)*, Roberto Giacobazzi (Ed.). Springer, 212–227. https://doi.org/10.1007/978-3-540-27864-1_17

Arie Gurfinkel. 2022. Program Verification with Constrained Horn Clauses (Invited Paper). In *Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I (Lecture Notes in Computer Science, Vol. 13371)*, Sharon Shoham and Yakir Vizel (Eds.). Springer, 19–29. https://doi.org/10.1007/978-3-031-13185-1_2

Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, and David Pichardie. 2015. A formally-verified C static analyzer. *ACM SIGPLAN Notices* 50, 1 (2015), 247–259. https://doi.org/10.1145/2676726.2676966

Matthieu Journault, Antoine Miné, Raphaël Monat, and Abdelraouf Ouadjaout. 2019. Combinations of Reusable Abstract Domains for a Multilingual Static Analyzer. In *11th International Conference on Verified Software Theories, Tools, and Experiments - Revised Selected Papers (Lecture Notes in Computer Science, Vol. 12031)*, Supratik Chakraborty and Jorge A. Navas (Eds.). Springer, 1–18. https://doi.org/10.1007/978-3-030-41600-3_1

Sven Keidel and Sebastian Erdweg. 2019. Sound and reusable components for abstract interpretation. *Proc. ACM Program. Lang.* 3, OOPSLA (2019), 176:1–176:28. https://doi.org/10.1145/3360602

Richard Kelsey. 1995. A Correspondence between Continuation Passing Style and Static Single Assignment Form. In *Proceedings ACM SIGPLAN Workshop on Intermediate Representations (IR’95)*, Michael D. Ernst (Ed.). ACM, 13–23. https://doi.org/10.1145/202529.202532

Gary A Kildall. 1973. A unified approach to global program optimization. In *1st annual ACM SIGACT-SIGPLAN Symposium on Principles of programming languages (POPL 1973)*. https://doi.org/10.1145/512927.512945

Oleg Kiselyov. 2010. Typed Tagless Final Interpreters. In *Generic and Indexed Programming - International Spring School, SSGIP 2010, Oxford, UK, March 22-26, 2010, Revised Lectures (Lecture Notes in Computer Science, Vol. 7470)*, Jeremy Gibbons (Ed.). Springer, 130–174. https://doi.org/10.1007/978-3-642-32202-0_3

Matthieu Lemerre. 2023. SSA Translation Is an Abstract Interpretation. *Proceedings of the ACM on Programming Languages* 7, Article 65 (1 2023), 30 pages. https://doi.org/10.1145/3571258

Matthieu Lemerre, Julien Simonnet, Olivier Nicole, Dorian Lesbre, Iker Canut, Corentin Gendreau, and Guillaume Girol. 2024. The Codex semantic library. https://github.com/codex-semantics-library/codex. Version 1.0-beta.

Sorin Lerner, David Grove, and Craig Chambers. 2002. Composing dataflow analyses and transformations. In *29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2002)*, John Launchbury and John C. Mitchell (Eds.).
Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. 2006. Combination of Abstractions in the ASTRÈE Static Analyzer. In *Revised Selected Papers from the 11th Asian Computing Science Conference on Advances in Computer Science - Secure Software and Related Issues - ASIAN 2006* (Lecture Notes in Computer Science, Vol. 4435). Springer, 272–300. https://doi.org/10.1007/978-3-540-77505-8_23

Ron Cytron, Jeanne Ferrante, Barry K. Rosen, Mark N. Wegman, and F. Kenneth Zadeck. 1991. Efficiently Computing Static Single Assignment Form and the Control Dependence Graph. *ACM Trans. Program. Lang. Syst.* 13, 4 (oct 1991), 451–490. https://doi.org/10.1145/115372.115320

David Darais, Nicholas Labich, Phuc C. Nguyen, and David Van Horn. 2017. Abstracting definitional interpreters (functional pearl). *Proc. ACM Program. Lang.* 1, ICFP (2017), 12:1–12:25. https://doi.org/10.1145/3110256

David Darais, Matthew Might, and David Van Horn. 2015. Galois transformers and modular abstract interpreters: reusable metatheory for program analysis. In *Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2015, part of SPLASH 2015, Pittsburgh, PA, USA, October 25-30, 2015*, Jonathan Aldrich and Patrick Eugster (Eds.). ACM, 552–571. https://doi.org/10.1145/2814270.2814308

Delphine Demange, Yon Fernández de Retana, and David Pichardie. 2018. Semantic reasoning about the sea of nodes, In *Proceedings of the 27th International Conference on Compiler Construction, Christophe Dubach and Jingling Xue (Eds.). International Conference on Compiler Construction*, 163–173. https://doi.org/10.1145/3178372.3179503

Adel Djoudi, Sébastien Bardin, and Éric Goubault. 2016. Recovering High-Level Conditions from Binary Programs. In *21st International Symposium on Formal Methods (FM 2016)*. 235–253. https://doi.org/10.1007/978-3-319-48989-6_15

Robert W Dockins. 2012. *Operational refinement for compiler correctness*. Ph. D. Dissertation, Princeton University.

Jean-Christophe Filliâtre and Sylvain Conchon. 2006. Type-Safe Modular Hash-Consing. *ML Workshop* (9 2006), 12–19. https://doi.org/10.1145/1159876.1159880

Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard, and Peter J. Stuckey. 2016. An Abstract Domain of Uninterpreted Functions. In *Verification, Model Checking, and Abstract Interpretation (VMCAI 2016)*, Barbara Jobstmann and K. Rustan M. Leino (Eds.). Springer, 85–103. https://doi.org/10.1007/978-3-662-49122-5_4

Roberto Giacobazzi, Francesco Logozzo, and Francesco Ranzato. 2015. Analyzing Program Analyses. In *Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015*, Sriram K. Rajamani and David Walker (Eds.). ACM, 261–273. https://doi.org/10.1145/2676726.2676987

Philippe Granger. 1992. Improving the results of static analyses of programs by local decreasing iterations. In *International Conference on Foundations of Software Technology and Theoretical Computer Science*. Springer, Springer Berlin Heidelberg, 68–79. https://doi.org/10.1007/3-540-56287-7_95

Sumit Gulwani and George C. Necula. 2004. A Polynomial-Time Algorithm for Global Value Numbering. In *Static Analysis Symposium (SAS 2004)*, Roberto Giacobazzi (Ed.). Springer, 212–227. https://doi.org/10.1007/978-3-540-27864-1_17

Arie Gurfinkel. 2022. Program Verification with Constrained Horn Clauses (Invited Paper). In *Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I (Lecture Notes in Computer Science, Vol. 13371)*, Sharon Shoham and Yakir Vizel (Eds.). Springer, 19–29. https://doi.org/10.1007/978-3-031-13185-1_2

Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, and David Pichardie. 2015. A formally-verified C static analyzer. *ACM SIGPLAN Notices* 50, 1 (2015), 247–259. https://doi.org/10.1145/2676726.2676966

Matthieu Journault, Antoine Miné, Raphaël Monat, and Abdelraouf Ouadjaout. 2019. Combinations of Reusable Abstract Domains for a Multilingual Static Analyzer. In *11th International Conference on Verified Software Theories, Tools, and Experiments - Revised Selected Papers (Lecture Notes in Computer Science, Vol. 12031)*, Supratik Chakraborty and Jorge A. Navas (Eds.). Springer, 1–18. https://doi.org/10.1007/978-3-030-41600-3_1

Sven Keidel and Sebastian Erdweg. 2019. Sound and reusable components for abstract interpretation. *Proc. ACM Program. Lang.* 3, OOPSLA (2019), 176:1–176:28. https://doi.org/10.1145/3360602

Richard Kelsey. 1995. A Correspondence between Continuation Passing Style and Static Single Assignment Form. In *Proceedings ACM SIGPLAN Workshop on Intermediate Representations (IR'95)*, Michael D. Ernst (Ed.). ACM, 13–23. https://doi.org/10.1145/202529.202532

Gary A Kildall. 1973. A unified approach to global program optimization. In *1st annual ACM SIGACT-SIGPLAN Symposium on Principles of programming languages (POPL 1973)*. https://doi.org/10.1145/512927.512945

Oleg Kiselyov. 2010. Typed Tagless Final Interpreters. In *Generic and Indexed Programming - International Spring School, SSGIP 2010, Oxford, UK, March 22-26, 2010, Revised Lectures (Lecture Notes in Computer Science, Vol. 7470)*, Jeremy Gibbons (Ed.). Springer, 130–174. https://doi.org/10.1007/978-3-642-32202-0_3

Matthieu Lemerre. 2023. SSA Translation Is an Abstract Interpretation. *Proceedings of the ACM on Programming Languages* 7, Article 65 (1 2023), 30 pages. https://doi.org/10.1145/3571258

Matthieu Lemerre, Julien Simonnet, Olivier Nicole, Dorian Lesbre, Iker Canut, Corentin Gendreau, and Guillaume Girol. 2024. The Codex semantic library. https://github.com/codex-semantics-library/codex. Version 1.0-beta.

Sorin Lerner, David Grove, and Craig Chambers. 2002. Composing dataflow analyses and transformations. In *29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2002)*, John Launchbury and John C. Mitchell (Eds.).