ACM, 270-282. https://doi.org/10.1145/503272.503298

Xavier Leroy. 2009. A formally verified compiler back-end. *Journal of Automated Reasoning* 43 (2009), 363-446. https://doi.org/10.1007/s10817-009-9155-4

Dorian Lesbre and Matthieu Lemerre. 2024a. Compiling with Abstract Interpretation: Artifact. https://doi.org/10.5281/zenodo.10895582

Dorian Lesbre and Matthieu Lemerre. 2024b. Compiling with Abstract Interpretation (PLDI 2024). Article 162. https://doi.org/10.1145/3656392

Francesco Logozzo and Manuel Fähndrich. 2008. *On the Relative Completeness of Bytecode Analysis Versus Source Code Analysis*. Springer, Berlin, Heidelberg, 197-212. https://doi.org/10.1007/978-3-540-78791-4_14

Laurent D. Michel and Pascal Van Hentenryck. 2012. Constraint Satisfaction over Bit-Vectors. In *Principles and Practice of Constraint Programming - 18th International Conference, CP 2012, Québec City, QC, Canada, October 8-12, 2012. Proceedings (Lecture Notes in Computer Science, Vol. 7514)*, Michela Milano (Ed.). Springer, 527-543. https://doi.org/10.1007/978-3-642-33558-7_39

A. Miné. 2004. *Weakly relational numerical abstract domains*. Ph. D. Dissertation. École Polytechnique. http://www.di.ens.fr/~mine/these/these-color.pdf.

Antoine Miné. 2006. Symbolic methods to enhance the precision of numerical abstract domains. In *International Workshop on Verification, Model Checking, and Abstract Interpretation (VMCAI 2006)*. Springer, 348-363. https://doi.org/10.1007/11609773_23

Antoine Miné. 2012. Abstract domains for bit-level machine integer and floating-point operations. In *WING'12 - 4th International Workshop on invariant Generation*. Manchester, United Kingdom, 16. https://doi.org/10.29007/b63g

Antoine Miné. 2017. Tutorial on static inference of numeric invariants by abstract interpretation. *Foundations and Trends® in Programming Languages 4*, 3-4 (2 2017), 120-372. https://doi.org/10.1561/2500000034

Olivier Nicole, Matthieu Lemerre, Sébastien Bardin, and Xavier Rival. 2021. No Crash, No Exploit: Automated Verification of Embedded Kernels. In *27th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS 2021)*. 27-39. https://doi.org/10.1109/RTAS52030.2021.00011

Olivier Nicole, Matthieu Lemerre, and Xavier Rival. 2022. Lightweight Shape Analysis Based on Physical Types. In *23rd International Conference on Verification, Model Checking, and Abstract Interpretation – VMCAI 2022 (Lecture Notes in Computer Science, Vol. 13182)*, Bernd Finkbeiner and Thomas Wies (Eds.). Springer, 219-241. https://doi.org/10.1007/978-3-030-94583-1_11

Fabrice Rastello and Florent Bouchez Tichadou (Eds.). 2022. *SSA-based Compiler Design*. Springer.

Tiark Rompf. 2012. *Lightweight modular staging and embedded compilers: Abstraction without regret for high-level high-performance programming*. Ph. D. Dissertation. École Polytechnique Fédérale de Lausanne.

Barry K Rosen, Mark N Wegman, and F Kenneth Zadeck. 1988. Global value numbers and redundant computations, In *Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. ACM-SIGACT Symposium on Principles of Programming Languages*, 12-27. https://doi.org/10.1145/73560.73562

Grigore Roşu and Traian-Florin Serbanuta. 2010. An overview of the K semantic framework. *J. Log. Algebraic Methods Program.* 79 (2010), 397-434. https://apisemanticscholar.org/CorpusID:13756844

Sigurd Schneider. 2013. Semantics of an intermediate language for program transformation. *preparation. Master's Thesis. Universität des Saarlandes* (2013).

Ilya Sergey, Dominique Devriese, Matthew Might, Jan Midtgaard, David Darais, Dave Clarke, and Frank Piessens. 2013. Monadic abstract interpreters. In *ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '13, Seattle, WA, USA, June 16-19, 2013*, Hans-Juergen Boehm and Cormac Flanagan (Eds.). ACM, 399-410. https://doi.org/10.1145/2491956.2491979

Vugranam C. Sreedhar and Guang R. Gao. 1995. A Linear Time Algorithm for Placing phi-nodes. In *22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1995)*, Ron K. Cytron and Peter Lee (Eds.). 62-73. https://doi.org/10.1145/199448.199464

Arnaud Venet. 1996. Abstract Cofibered Domains: Application to the Alias Analysis of Untyped Programs. In *Proceedings of the Third International Symposium on Static Analysis (SAS '96)*. Springer-Verlag, London, UK, 366-382. https://doi.org/10.1007/3-540-61739-6_53

Harishankar Vishwanathan, Matan Shachnai, Srinivas Narayana, and Santosh Nagarakatte. 2022. Sound, Precise, and Fast Abstract Interpretation with Tristate Numbers. In *IEEE/ACM International Symposium on Code Generation and Optimization, CGO 2022, Seoul, Korea, Republic of, April 2-6, 2022*, Jae W. Lee, Sebastian Hack, and Tatiana Shpeisman (Eds.). IEEE, 254-265. https://doi.org/10.1109/CGO53902.2022.9741267

Mark N Wegman and F Kenneth Zadeck. 1991. Constant propagation with conditional branches. *ACM Transactions on Programming Languages and Systems (TOPLAS)* 13, 2 (4 1991), 181-210. https://doi.org/10.1145/103135.103136

Mark D. Weiser. 1984. Program Slicing. *IEEE Trans. Software Eng.* 10, 4 (1984), 352-357. https://doi.org/10.1109/TSE.1984.5010248
ACM, 270-282. https://doi.org/10.1145/503272.503298

Xavier Leroy. 2009. A formally verified compiler back-end. *Journal of Automated Reasoning* 43 (2009), 363-446. https://doi.org/10.1007/s10817-009-9155-4

Dorian Lesbre and Matthieu Lemerre. 2024a. Compiling with Abstract Interpretation: Artifact. https://doi.org/10.5281/zenodo.10895582

Dorian Lesbre and Matthieu Lemerre. 2024b. Compiling with Abstract Interpretation (PLDI 2024). Article 162. https://doi.org/10.1145/3656392

Francesco Logozzo and Manuel Fähndrich. 2008. *On the Relative Completeness of Bytecode Analysis Versus Source Code Analysis*. Springer, Berlin, Heidelberg, 197-212. https://doi.org/10.1007/978-3-540-78791-4_14

Laurent D. Michel and Pascal Van Hentenryck. 2012. Constraint Satisfaction over Bit-Vectors. In *Principles and Practice of Constraint Programming - 18th International Conference, CP 2012, Québec City, QC, Canada, October 8-12, 2012. Proceedings (Lecture Notes in Computer Science, Vol. 7514)*, Michela Milano (Ed.). Springer, 527-543. https://doi.org/10.1007/978-3-642-33558-7_39

A. Miné. 2004. *Weakly relational numerical abstract domains*. Ph. D. Dissertation. École Polytechnique. http://www.di.ens.fr/~mine/these/these-color.pdf.

Antoine Miné. 2006. Symbolic methods to enhance the precision of numerical abstract domains. In *International Workshop on Verification, Model Checking, and Abstract Interpretation (VMCAI 2006)*. Springer, 348-363. https://doi.org/10.1007/11609773_23

Antoine Miné. 2012. Abstract domains for bit-level machine integer and floating-point operations. In *WING'12 - 4th International Workshop on invariant Generation*. Manchester, United Kingdom, 16. https://doi.org/10.29007/b63g

Antoine Miné. 2017. Tutorial on static inference of numeric invariants by abstract interpretation. *Foundations and Trends® in Programming Languages 4*, 3-4 (2 2017), 120-372. https://doi.org/10.1561/2500000034

Olivier Nicole, Matthieu Lemerre, Sébastien Bardin, and Xavier Rival. 2021. No Crash, No Exploit: Automated Verification of Embedded Kernels. In *27th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS 2021)*. 27-39. https://doi.org/10.1109/RTAS52030.2021.00011

Olivier Nicole, Matthieu Lemerre, and Xavier Rival. 2022. Lightweight Shape Analysis Based on Physical Types. In *23rd International Conference on Verification, Model Checking, and Abstract Interpretation - VMCAI 2022 (Lecture Notes in Computer Science, Vol. 13182)*, Bernd Finkbeiner and Thomas Wies (Eds.). Springer, 219-241. https://doi.org/10.1007/978-3-030-94583-1_11

Fabrice Rastello and Florent Bouchez Tichadou (Eds.). 2022. *SSA-based Compiler Design*. Springer.

Tiark Rompf. 2012. *Lightweight modular staging and embedded compilers: Abstraction without regret for high-level high-performance programming*. Ph. D. Dissertation. École Polytechnique Fédérale de Lausanne.

Barry K Rosen, Mark N Wegman, and F Kenneth Zadeck. 1988. Global value numbers and redundant computations, In *Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. ACM-SIGACT Symposium on Principles of Programming Languages*, 12-27. https://doi.org/10.1145/73560.73562

Grigore Roșu and Traian-Florin Serbanuta. 2010. An overview of the K semantic framework. *J. Log. Algebraic Methods Program.* 79 (2010), 397-434. https://apisemanticscholar.org/CorpusID:13756844

Sigurd Schneider. 2013. Semantics of an intermediate language for program transformation. *preparation. Master's Thesis. Universität des Saarlandes* (2013).

Ilya Sergey, Dominique Devriese, Matthew Might, Jan Midtgaard, David Darais, Dave Clarke, and Frank Piessens. 2013. Monadic abstract interpreters. In *ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '13, Seattle, WA, USA, June 16-19, 2013*, Hans-Juergen Boehm and Cormac Flanagan (Eds.). ACM, 399-410. https://doi.org/10.1145/2491956.2491979

Vugranam C. Sreedhar and Guang R. Gao. 1995. A Linear Time Algorithm for Placing phi-nodes. In *22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1995)*, Ron K. Cytron and Peter Lee (Eds.). 62-73. https://doi.org/10.1145/199448.199464

Arnaud Venet. 1996. Abstract Cofibered Domains: Application to the Alias Analysis of Untyped Programs. In *Proceedings of the Third International Symposium on Static Analysis (SAS '96)*. Springer-Verlag, London, UK, 366-382. https://doi.org/10.1007/3-540-61739-6_53

Harishankar Vishwanathan, Matan Shachnai, Srinivas Narayana, and Santosh Nagarakatte. 2022. Sound, Precise, and Fast Abstract Interpretation with Tristate Numbers. In *IEEE/ACM International Symposium on Code Generation and Optimization, CGO 2022, Seoul, Korea, Republic of, April 2-6, 2022*, Jae W. Lee, Sebastian Hack, and Tatiana Shpeisman (Eds.). IEEE, 254-265. https://doi.org/10.1109/CGO53902.2022.9741267

Mark N Wegman and F Kenneth Zadeck. 1991. Constant propagation with conditional branches. *ACM Transactions on Programming Languages and Systems (TOPLAS)* 13, 2 (4 1991), 181-210. https://doi.org/10.1145/103135.103136

Mark D. Weiser. 1984. Program Slicing. *IEEE Trans. Software Eng.* 10, 4 (1984), 352-357. https://doi.org/10.1109/TSE.1984.5010248
Xuejun Yang, Yang Chen, Eric Eide, and John Regehr. 2011. Finding and understanding bugs in C compilers. In *32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, SERIES: PLDI 2011*, Mary W. Hall and David A. Padua (Eds.). ACM, 283–294. https://doi.org/10.1145/1993498.1993532
Xuejun Yang, Yang Chen, Eric Eide, and John Regehr. 2011. Finding and understanding bugs in C compilers. In *32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, SERIES: PLDI 2011*, Mary W. Hall and David A. Padua (Eds.). ACM, 283–294. https://doi.org/10.1145/1993498.1993532
<figure><img src="image_8.png" /><figcaption>Fig. 13. Extra hypotheses on an abstract domain D</figcaption></figure>

# A PROOFS

## A.1 Proofs: notations and background

Figure 13 formally presents hypotheses on a domain D that were only described in the paper. Widening should always lead to convergence: we say a sequence $(s_n^#)$ stabilizes when it is constant after a certain time: $\exists m, \forall n, n \ge m \Rightarrow s_m^# = s_n^{#10}$. A domain’s soundness hypotheses were presented in the top right of Figure 4, here we also state their complementary completeness hypotheses.

For abstract interpretation, we want domains to be sound (so that our analysis says something meaningful about all program behaviors). For compilation, we want domains to be complete (so that the compiled program behaviors are included in the source behaviors).

Let us take a domain D.

**LEMMA A.1 (TERMINATION).** *Assuming D satisfies *WSOUND* and *WIDENVALID*, analyse(D) reaches a fixed point in a finite number of steps.*

**PROOF.** There are a finite number of widening points in W, which each stabilize in finite time. By *WIDENVALID*. Thus, they are all constant after the maximum of their stabilization times. After that, there are no loops in the program, so the remaining points also stabilize in finite time (bounded by longest path). □

In the rest of this section, we write $p_{\infty}^{#} \triangleq \text{analyse}(D)$, and $p_{n}^{#}$ the $n$-th iteration of the fixed point computation in analyse. These verify $p_{\infty}^{#} = p_{\infty}^{#} \nabla_{W} \mathcal{F}_{g}(p_{\infty}^{#})$ and $p_{0}^{#} = [\ell_{0} \mapsto \text{D.entry}]$ and $p_{n+1}^{#} = p_{n}^{#} \nabla_{W} \mathcal{F}_{g}(p_{n}^{#})$.

**LEMMA A.2 (SOUNDNESS).** *If D is sound, then for all reachable pairs $(\sigma, \ell)$, we have $\sigma \in D.\gamma(p_{\infty}^{#}(\ell))$.*

**PROOF.** By induction on the shortest path $(\sigma_0, \ell_0) \to_G^* (\sigma, \ell)$ that makes $(\sigma, \ell)$ reachable.

If that path is empty then $\sigma = \sigma_0$ and $\ell = \ell_0$. Therefore, we have $p_{\infty}^{#}(\ell) = \text{D.entry}$ and, by *ENTRY SOUND*, $\Sigma \subseteq D.\gamma(p_{\infty}^{#}(\ell))$.

For the recursive case we have $(\sigma_0, \ell_0) \to_G^* (\sigma_n, \ell_n) \to_G (\sigma, \ell)$ and $\sigma_n \in D.\gamma(p_{\infty}^{#}(\ell_n))$. We write $R_0, \dots, R_n$ the respective edge relations on this path. We can show that $\sigma \in D.\gamma(\mathcal{F}_g(p_{\infty}^{#})(\ell))$. Consider $\mathcal{F}_g(p_{\infty}^{#})(\ell)$, it is the D.join of a set. That set contains $\text{D.apply}(R_0, p_{\infty}^{#}(\ell_n))$ since

* $D.\gamma(p_{\infty}^{#}(\ell_n))$ is non-empty by induction, so $p_{\infty}^{#}(\ell_n) \neq \bot$

* $\mathcal{G}(\ell_n, R_n, \ell)$ holds by $(\sigma_n, \ell_n) \to_G (\sigma, \ell)$.

<footnote n="10">¹⁰Often in abstract interpretation, we only want to reach a post fixed point instead of a true fixed point. See Appendix B for details on how to do so with this framework.</footnote>
<figure><img src="image_10.png" /><figcaption>Fig. 13. Extra hypotheses on an abstract domain D</figcaption></figure>

# A PROOFS

## A.1 Proofs: notations and background

Figure 13 formally presents hypotheses on a domain D that were only described in the paper. Widening should always lead to convergence: we say a sequence $(s_n^#)$ stabilizes when it is constant after a certain time: $\exists m, \forall n, n \ge m \Rightarrow s_m^# = s_n^{\#10}$. A domain's soundness hypotheses were presented in the top right of Figure 4, here we also state their complementary completeness hypotheses.

For abstract interpretation, we want domains to be sound (so that our analysis says something meaningful about all program behaviors). For compilation, we want domains to be complete (so that the compiled program behaviors are included in the source behaviors).

Let us take a domain D.

**LEMMA A.1 (TERMINATION).** *Assuming D satisfies W SOUND and W IDENVALID , analyse (D) reaches a fixed point in a finite number of steps.*

**PROOF.** There are a finite number of widening points in W, which each stabilize in finite time. By WIDENVALID . Thus, they are all constant after the maximum of their stabilization times. After that, there are no loops in the program, so the remaining points also stabilize in finite time (bounded by longest path). $\square$

In the rest of this section, we write $p_{\infty}^{\#} \triangleq \text{analyse}(D)$, and $p_{n}^{\#}$ the $n$-th iteration of the fixed point computation in analyse. These verify $p_{\infty}^{\#} = p_{\infty}^{\#} \nabla_{W} \mathcal{F}_{g}(p_{\infty}^{\#})$ and $p_{0}^{\#} = [\ell_{0} \mapsto \text{D.entry}]$ and $p_{n+1}^{\#} = p_{n}^{\#} \nabla_{W} \mathcal{F}_{g}(p_{n}^{\#})$.

**LEMMA A.2 (SOUNDNESS).** *If D is sound, then for all reachable pairs $(\sigma, \ell)$, we have $\sigma \in D.\gamma(p_{\infty}^{\#}(\ell))$.*

**PROOF.** By induction on the shortest path $(\sigma_0, \ell_0) \to_G^* (\sigma, \ell)$ that makes $(\sigma, \ell)$ reachable.

If that path is empty then $\sigma = \sigma_0$ and $\ell = \ell_0$. Therefore, we have $p_{\infty}^{\#}(\ell) = \text{D.entry}$ and, by ENTRY SOUND , $\Sigma \subseteq D.\gamma(p_{\infty}^{\#}(\ell))$.

For the recursive case we have $(\sigma_0, \ell_0) \to_G^* (\sigma_n, \ell_n) \to_G (\sigma, \ell)$ and $\sigma_n \in D.\gamma(p_{\infty}^{\#}(\ell_n))$. We write $R_0, \dots, R_n$ the respective edge relations on this path. We can show that $\sigma \in D.\gamma(\mathcal{F}_g(p_{\infty}^{\#})(\ell))$. Consider $\mathcal{F}_g(p_{\infty}^{\#})(\ell)$, it is the D.join of a set. That set contains $\text{D.apply}(R_0, p_{\infty}^{\#}(\ell_n))$ since

* $D.\gamma(p_{\infty}^{\#}(\ell_n))$ is non-empty by induction, so $p_{\infty}^{\#}(\ell_n) \neq \bot$

* $\mathcal{G}(\ell_n, R_n, \ell)$ holds by $(\sigma_n, \ell_n) \to_G (\sigma, \ell)$.

<footnote n="10">¹⁰Often in abstract interpretation, we only want to reach a post fixed point instead of a true fixed point. See Appendix B for details on how to do so with this framework.</footnote>
* the D. apply is also not $\perp$ else this would contradict the soundness of D. apply, (we know D.γ(D. apply($R_n$, $p_\infty^\#(\ell_n)$)) should contain $\sigma$ as $(\sigma_n, \ell_n) \to \mathcal{G}$ ($\sigma, \ell$) implies $\mathcal{R}[[R_n]]$ ($\sigma_n, \sigma$), then use APPLY SOUND).

The join set thus contains D. apply($R_n$, $p_\infty^\#(\ell_n)$), and the soundness of D. join and D. apply suffice to show $\sigma \in D.\gamma(\mathcal{F}_g(p_\infty^\#)(\ell))$.

If $\ell$ is not a widening point, then we have $p_\infty^\#(\ell) = \mathcal{F}_g(p_\infty^\#)(\ell)$ and the result is shown. In the other case, $p_\infty^\#(\ell) = \text{D. widen}(\ell, p_\infty^\#(\ell), \mathcal{F}_g(p_\infty^\#)(\ell))$ so the soundness of D. widen is sufficient to conclude. $\square$

**LEMMA A.3 (COMPLETENESS).** If D is complete, then for all pairs $(\sigma, \ell)$, we have $\sigma \in D.\gamma(p_\infty^\#(\ell)) \Rightarrow (\sigma, \ell)$ reachable.

*PROOF.* We show the property holds for all $p_n^\#$ by induction on $n$.

It is true at $n=0$ since $p_0^\# = [\ell_0 \mapsto \text{D. entry}]$ (by ENTRYCOMPLETE).

Suppose it is true of $p_n^\#$, then since $p_{n+1}^\# = p_n^\# \nabla_W \mathcal{F}_g(p_n^\#)$ and since $\nabla_W$ and $\mathcal{F}_g$ only use complete operations, it remains true. $\square$

## A.2 Proofs: Free algebra of the domain signature

### Proof of Theorem 4.1:

**THEOREM 4.1.** When $p^\# = \text{analyse}(\text{FA})$, $\mathcal{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)

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

*PROOF.* For the injectivity of $p^\#$, we reason by structural induction on $s^\#$, showing the following property: “for all $\ell$ and $\ell'$ such that $p^\#(\ell) = p^\#(\ell') = s^\#$, we have $\ell = \ell'$”. This is shown largely by inspecting the fixpoint equality $p^\# = p^\# \nabla_W \mathcal{F}_g(p^\#)$ and unfolding $\mathcal{F}_g$ and $\nabla_W$.

* Case $s^\# = \text{Entry}$, the only operation that introduces such a term is the FA. entry in $\mathcal{F}_g$, which is only ever applied at $\ell_0$, so $\ell = \ell' = \ell_0$.

* Case $s^\# = \text{Loc}(\ell'')$, the only operation that introduces a Loc is FA. widen(,, w)hich is only ever applied at the point it is called, so $\ell = \ell' = \ell''$.

* Case $s^\# = \text{Apply}(R, t^\#)$: by unfolding $\mathcal{F}_g$, we know $t^\#$ must be in img $p^\#$, so we can apply the induction hypothesis there. Conclude using the requirement that outgoing edges of IMP nodes are uniquely labelled.

* The Join case is similar to the Apply case, just pick any element of the non-empty set: it must be an Apply by inversion of $\mathcal{F}_g$, so we can reuse the same reasoning.

Now for the second point.

Consider an edge $\mathcal{G}(\ell, R, \ell')$, assuming $\ell$ is reachable. Since the analysis is sound, this implies $\text{FA.}\gamma(p^\#(\ell)) \neq \emptyset$ and therefore $p^\#(\ell) \neq \perp$.

We can show that $p^\#(\ell) \stackrel{R}{\mapsto} \# \mathcal{F}_g(p^\#)(\ell')$ holds. By definition of $\mathcal{F}_g$, the right-hand side is a FA. join of FA. apply of the predecessors of $\ell'$, and $\ell$ is such a predecessor. The join is thus not empty, so it is either the single element Apply($R$, $p^\#(\ell)$) or the Join of a set containing it. Conclude by TAPPLY and TJOIN.

Since $p^\# = p^\# \nabla_W \mathcal{F}_g(p^\#)$, we have two cases, either we didn't widen at $\ell'$ ($p^\#(\ell') = \mathcal{F}_g(p^\#)(\ell')$), and thus $p^\#(\ell) \stackrel{R}{\mapsto} \# p^\#(\ell')$ holds directly, or we performed a widening, and the same holds via TLOC. This result is sufficient to show that $\mathcal{G}_{p^\#}(p^\#(\ell), R, p^\#(\ell'))$ holds using VBASE and GRAPHGEN.

Consider now an edge $\mathcal{G}_{p^\#}(s^\#, R, t^\#)$. By definition of $\mathcal{G}_{p^\#}$, $V(t^\#)$ holds, so by case disjunction:
* the D. apply is also not $\perp$ else this would contradict the soundness of D. apply, (we know D.γ(D. apply($R_n$, $p_\infty^\#(\ell_n)$)) should contain $\sigma$ as $(\sigma_n, \ell_n) \to \mathcal{G}$ ($\sigma, \ell$) implies $\mathcal{R}[[R_n]]$ ($\sigma_n, \sigma$), then use APPLY SOUND).

The join set thus contains D. apply($R_n$, $p_\infty^\#(\ell_n)$), and the soundness of D. join and D. apply suffice to show $\sigma \in D.\gamma(\mathcal{F}_g(p_\infty^\#)(\ell))$.

If $\ell$ is not a widening point, then we have $p_\infty^\#(\ell) = \mathcal{F}_g(p_\infty^\#)(\ell)$ and the result is shown. In the other case, $p_\infty^\#(\ell) = \text{D. widen}(\ell, p_\infty^\#(\ell), \mathcal{F}_g(p_\infty^\#)(\ell))$ so the soundness of D. widen is sufficient to conclude. $\square$

**LEMMA A.3 (COMPLETENESS).** If D is complete, then for all pairs $(\sigma, \ell)$, we have $\sigma \in D.\gamma(p_\infty^\#(\ell)) \Rightarrow (\sigma, \ell)$ reachable.

*PROOF.* We show the property holds for all $p_n^\#$ by induction on $n$.

It is true at $n=0$ since $p_0^\# = [\ell_0 \mapsto \text{D. entry}]$ (by ENTRYCOMPLETE).

Suppose it is true of $p_n^\#$, then since $p_{n+1}^\# = p_n^\# \nabla_W \mathcal{F}_g(p_n^\#)$ and since $\nabla_W$ and $\mathcal{F}_g$ only use complete operations, it remains true. $\square$

## A.2 Proofs: Free algebra of the domain signature

### Proof of Theorem 4.1:

**THEOREM 4.1.** When $p^\# = \text{analyse}(\text{FA})$, $\mathcal{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)

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

*PROOF.* For the injectivity of $p^\#$, we reason by structural induction on $s^\#$, showing the following property: “for all $\ell$ and $\ell'$ such that $p^\#(\ell) = p^\#(\ell') = s^\#$, we have $\ell = \ell'$”. This is shown largely by inspecting the fixpoint equality $p^\# = p^\# \nabla_W \mathcal{F}_g(p^\#)$ and unfolding $\mathcal{F}_g$ and $\nabla_W$.

* Case $s^\# = \text{Entry}$, the only operation that introduces such a term is the FA. entry in $\mathcal{F}_g$, which is only ever applied at $\ell_0$, so $\ell = \ell' = \ell_0$.

* Case $s^\# = \text{Loc}(\ell'')$, the only operation that introduces a Loc is FA. widen(,, w)hich is only ever applied at the point it is called, so $\ell = \ell' = \ell''$.

* Case $s^\# = \text{Apply}(R, t^\#)$: by unfolding $\mathcal{F}_g$, we know $t^\#$ must be in img $p^\#$, so we can apply the induction hypothesis there. Conclude using the requirement that outgoing edges of IMP nodes are uniquely labelled.

* The Join case is similar to the Apply case, just pick any element of the non-empty set: it must be an Apply by inversion of $\mathcal{F}_g$, so we can reuse the same reasoning.

Now for the second point.

Consider an edge $\mathcal{G}(\ell, R, \ell')$, assuming $\ell$ is reachable. Since the analysis is sound, this implies $\text{FA.}\gamma(p^\#(\ell)) \neq \emptyset$ and therefore $p^\#(\ell) \neq \perp$.

We can show that $p^\#(\ell) \stackrel{R}{\mapsto}_\# \mathcal{F}_g(p^\#)(\ell')$ holds. By definition of $\mathcal{F}_g$, the right-hand side is a FA. join of FA. apply of the predecessors of $\ell'$, and $\ell$ is such a predecessor. The join is thus not empty, so it is either the single element Apply($R$, $p^\#(\ell)$) or the Join of a set containing it. Conclude by TAPPLY and TJOIN.

Since $p^\# = p^\# \nabla_W \mathcal{F}_g(p^\#)$, we have two cases, either we didn't widen at $\ell'$ ($p^\#(\ell') = \mathcal{F}_g(p^\#)(\ell')$), and thus $p^\#(\ell) \stackrel{R}{\mapsto}_\# p^\#(\ell')$ holds directly, or we performed a widening, and the same holds via TLOC. This result is sufficient to show that $\mathcal{G}_{p^\#}(p^\#(\ell), R, p^\#(\ell'))$ holds using VBASE and GRAPHGEN.

Consider now an edge $\mathcal{G}_{p^\#}(s^\#, R, t^\#)$. By definition of $\mathcal{G}_{p^\#}$, $V(t^\#)$ holds, so by case disjunction:
* VBASE case: there is some $\ell'$ such that $t^\# = p^\#(\ell')$. We have $s^\# \stackrel{R}{\mapsto} \# \mathcal{F}_g(p^\#)(\ell')$ since either $\ell'$ isn't a widening point (and so $p^\#(\ell') = \mathcal{F}_g(p^\#)(\ell')$) or it is, in which case we use TLOC. $\mathcal{F}_g(p^\#)(\ell')$ isn't empty since it has an incoming transition. So it is either a Join of Apply of predecessors of $\ell'$ or a single such Apply. Either way (optionally using TJOIN), we can show that there exists a predecessor $\ell$ such that $s^\# \stackrel{R}{\mapsto} \# \text{Apply}(R, p^\#(\ell))$. Inverting TAPPLY allows us to conclude $s^\# = p^\#(\ell)$ and that $\mathcal{G}(\ell, R, \ell')$.

* VREC case: in the previous case, we have shown that if $s^\# \stackrel{R}{\mapsto} \# p^\#(\ell')$ then there exists $\ell$ such that $s^\# = p^\#(\ell)$. Thus by immediate recursion, $V(t^\#)$ implies $t^\# \in \text{img } p^\#$, so we can always use the base case. □

Notice that in this proof, TSELF cannot occur since we never simplify edges, and VREC is unused as all points that would be added by it are already true by VBASE. These extra constructs are only useful when dealing with transformation functors (Section 5) which can add extra intermediate states (which require VREC to be included) or remove no-op relations (which may require TSELF to avoid deleting loops).

## A.3 Proofs: Transformation functors as compiler passes

### Proof of Lemma 5.4:

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.

PROOF. We start by the soundness proof.

The direct implication is trivial, since CS is sound.

For the reciprocal: $F(CS)$ sound $\Rightarrow (\forall D, D \text{ sound} \Rightarrow F(D) \text{ sound})$, let us take a sound domain $D$. We only have to show APPLYSOUND in $F(D)$, since all other operations are equal to those of $D$.

Let us take $R \in \mathbb{R}$ and $s^\# \in D.\Sigma^\#$. We know $F(D).apply(R, s^\#)$ is a composition of $D$.apply, $D.join$, and $s^\#$. (That composition may depend on $R$, or on $s^\#$ through queries). We write it as $D.Composition(s^\#)$.

* By soundness of $D$ (and immediate induction on Composition): $\text{CS.Composition}(D.\gamma(s^\#)) \subseteq D.\gamma(\text{D.Composition}(s^\#))$.

* We can show $\{\sigma' \in \Sigma \mid \exists \sigma \in \gamma(s^\#), \mathcal{R}[R](\sigma, \sigma')\} \subseteq \text{CS.Composition}(D.\gamma(s^\#))$ This is trivial if there are no queries (Composition only depends on $R$). Since any query that holds on $s^\#$ will also hold on $\gamma(s^\#)$, (as the collecting semantics domain is the most precise domain).

* Thus: $F(CS).apply(R, D.\gamma(s^\#)) \subseteq F(D).apply(R, s^\#)$

* Conclude by soundness of $F(CS)$.

The completeness proof is similar: it only inverts the set inclusions. □

**Proof of Theorem 5.5:** The proof requires modifying the graph generation rules a bit. Specifically, we need to replace TJOIN by two new rules:

$$ \begin{array}{ccc} \text{TJOINELIDE} & & \text{TJOINNOELIDE} \\ \begin{array}{rcl} s^\# & \stackrel{R}{\mapsto} & t^\# \\ \hline s^\# & \stackrel{R}{\mapsto} & \text{Join}(S^\#) \end{array} & & \begin{array}{rcl} t^\# & \in & S^\# \\ \hline t^\# & \stackrel{\text{If } 1}{\mapsto} & \text{Join}(S^\#) \end{array} \end{array} $$

$$ \begin{array}{ccc} \text{TJOINNOELIDE} & & \text{TJOINELIDE} \\ \begin{array}{rcl} t^\# & \in & S^\# \\ \hline t^\# & \stackrel{\text{If } 1}{\mapsto} & \text{Join}(S^\#) \end{array} & & \begin{array}{rcl} t^\# & \in & \text{img } p^\# \\ \hline t^\# & \stackrel{\text{If } 1}{\mapsto} & \text{Join}(S^\#) \end{array} \end{array} $$

The problem with TJOIN is that, when using transformation functors, an element $t^\#$ that is both in $\text{img } p^\#$ and in a join, since we can now remove trivial applies. This would break our graph generation, duplicating all edges to $t^\#$ (they will also go into the join), and making $t^\#$ a local sink.
* **VBASE case:** there is some $\ell'$ such that $t^\# = p^\#(\ell')$. We have $s^\# \stackrel{R}{\mapsto} \# \mathcal{F}_g(p^\#)(\ell')$ since either $\ell'$ isn't a widening point (and so $p^\#(\ell') = \mathcal{F}_g(p^\#)(\ell')$) or it is, in which case we use **TLOC**. $\mathcal{F}_g(p^\#)(\ell')$ isn't empty since it has an incoming transition. So it is either a **Join** of **Apply** of predecessors of $\ell'$ or a single such **Apply**. Either way (optionally using **TJOIN**), we can show that there exists a predecessor $\ell$ such that $s^\# \stackrel{R}{\mapsto} \# \text{Apply}(R, p^\#(\ell))$. Inverting **TAPPLY** allows us to conclude $s^\# = p^\#(\ell)$ and that $\mathcal{G}(\ell, R, \ell')$.

* **VREC case:** in the previous case, we have shown that if $s^\# \stackrel{R}{\mapsto} \# p^\#(\ell')$ then there exists $\ell$ such that $s^\# = p^\#(\ell)$. Thus by immediate recursion, $V(t^\#)$ implies $t^\# \in \text{img } p^\#$, so we can always use the base case. □

Notice that in this proof, $\mathbf{TSELF}$ cannot occur since we never simplify edges, and $\mathbf{VREC}$ is unused as all points that would be added by it are already true by $\mathbf{VBASE}$. These extra constructs are only useful when dealing with transformation functors (Section 5) which can add extra intermediate states (which require $\mathbf{VREC}$ to be included) or remove no-op relations (which may require $\mathbf{TSELF}$ to avoid deleting loops).

## A.3 Proofs: Transformation functors as compiler passes

### Proof of Lemma 5.4:

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

**PROOF.** We start by the soundness proof.

The direct implication is trivial, since CS is sound.

For the reciprocal: $F(\mathbf{CS})$ sound $\Rightarrow$ ($\forall D, D$ sound $\Rightarrow$ $F(D)$ sound), let us take a sound domain $D$. We only have to show **APPLY SOUND** in $F(D)$, since all other operations are equal to those of $D$.

Let us take $R \in \mathbb{R}$ and $s^\# \in D.\Sigma^\#$. We know $F(D).\text{apply}(R, s^\#)$ is a composition of $D.\text{apply}$, $D.\text{join}$, and $s^\#$. (That composition may depend on $R$, or on $s^\#$ through queries). We write it as $D.\text{Composition}(s^\#)$.

* By soundness of $D$ (and immediate induction on Composition): $\text{CS.Composition}(D.\gamma(s^\#)) \subseteq D.\gamma(\text{D.Composition}(s^\#))$.

* We can show $\{\sigma' \in \Sigma \mid \exists \sigma \in \gamma(s^\#), \mathcal{R}[R](\sigma, \sigma')\} \subseteq \text{CS.Composition}(D.\gamma(s^\#))$ This is trivial if there are no queries (Composition only depends on $R$). Since any query that holds on $s^\#$ will also hold on $\gamma(s^\#)$, (as the collecting semantics domain is the most precise domain).

* Thus: $F(\mathbf{CS}).\text{apply}(R, D.\gamma(s^\#)) \subseteq F(D).\text{apply}(R, s^\#)$

* Conclude by soundness of $F(\mathbf{CS})$.

The completeness proof is similar: it only inverts the set inclusions. □

**Proof of Theorem 5.5:** The proof requires modifying the graph generation rules a bit. Specifically, we need to replace $\mathbf{TJOIN}$ by two new rules:

$$ \begin{array}{ccc} \text{TJOINELIDE} & & \text{TJOINNOELIDE} \\ \begin{array}{rcl} s^\# & \stackrel{R}{\mapsto} & t^\# \\ \hline s^\# & \stackrel{R}{\mapsto} & \text{Join}(S^\#) \end{array} & & \begin{array}{rcl} t^\# & \in & S^\# \\ \hline t^\# & \stackrel{\text{If } 1}{\mapsto} & \text{Join}(S^\#) \end{array} \end{array} $$

$$ \begin{array}{ccc} \text{TJOINNOELIDE} & & \text{TJOINELIDE} \\ \begin{array}{rcl} t^\# & \in & S^\# \\ \hline t^\# & \stackrel{\text{If } 1}{\mapsto} & \text{Join}(S^\#) \end{array} & & \begin{array}{rcl} t^\# & \in & \text{img } p^\# \\ \hline t^\# & \stackrel{\text{If } 1}{\mapsto} & \text{Join}(S^\#) \end{array} \end{array} $$

The problem with $\mathbf{TJOIN}$ is that, when using transformation functors, an element $t^\#$ that is both in $\text{img } p^\#$ and in a join, since we can now remove trivial applies. This would break our graph generation, duplicating all edges to $t^\#$ (they will also go into the join), and making $t^\#$ a local sink.
One solution to this is to remove $t^#$ from the new graph, but then we may lose the simulation (as no point equivalent to $t^#$ exists in the new graph, there is only the join, which has more parents).

The solution chosen here is to only carry over to the join the edges that don't lead into the image $p^#(TJOINELIDE)$, and add an explicit edge for the others (TJOINNOELIDE). Note that with these rules, Theorem 4.1 still holds (as TJOINNOELIDE is never used when all applys introduce terms). We chose to only present TJOIN in the main paper in an attempt at keeping the presentation simple.

In order to prove Theorem 5.5, we start by proving a stronger, more technical simulation result:

**LEMMA A.4.** If $F$ is a sound transformation functor, then for all reachable pairs $(\ell, \sigma)$ and $(\ell', \sigma')$ such that $(\ell, \sigma) \to_G (\ell', \sigma')$, we have $(p^#(\ell), \sigma) \to_{G_{p^#}} (p^#(\ell'), \sigma')$.

**PROOF.** Consider a transition $(\ell, \sigma) \to_G (\ell', \sigma')$. Let $R$ be the associated transition. By definition of $\to_G$, we know that $\mathcal{R}[[R]](\sigma, \sigma')$ holds.

Since FA is sound, $F(FA)$ is also sound. Thus, by Lemma A.2, $\sigma \in F(FA) \cdot \gamma(p^#(\ell))$.

Since $F$ is a transformation functor, $F(FA) \cdot \text{apply}(R, p^#(\ell))$ is a combination of $FA \cdot \text{apply}$, $FA \cdot \text{join}$ and $p^#(\ell)$, That is to say, it is a free algebra term made of Apply, Join and $p^#(\ell)$. Looking at the rules for our edge predicate, we can show that such a term represents a DAG between a unique source ($p^#(\ell)$) and a unique sink (the full term).

By soundness of $F$, $FA \cdot \gamma(F(FA) \cdot \text{apply}(R, p^#(\ell)))$ must contain $\sigma'$. Thus, looking at the concretization of the DAG term, we can show by induction on the DAG term, that there must exist a path with intermediate states $s_1^#..s_{n-1}^#$ and relations $R_1..R_n$ such that $p^#(\ell) \stackrel{R_1}{\longrightarrow} \# s_1^# \stackrel{\cdots}{\longrightarrow} \# \cdots \stackrel{\cdots}{\longrightarrow} \# s_{n-1}^# \stackrel{R_n}{\longrightarrow} \# F(FA) \cdot \text{apply}(R, p^#(\ell))$. and $(\mathcal{R}[[R_1]];..;\mathcal{R}[[R_n]])(\sigma, \sigma')$ (where $R_1;R_2$ is relation composition: $(R_1;R_2)(a,b) \triangleq \exists c, R_1(a,c) \wedge R_2(c,b)$)

* if that term is just $p^#(\ell)$, then our path is a single vertex. Since the apply was removed, we know by soundness that $R$ is no-op on $p^#(\ell)$, thus $\sigma = \sigma'$ (the empty relation composition is equality).

* if that term is $\text{Apply}(R_1, s_1^#)$ we know there exists $\sigma'' \in FA \cdot \gamma(s_1^#)$ such that $\mathcal{R}[[R_1]](\sigma'', \sigma')$ (by unfolding of $\sigma' \in FA \cdot \gamma(\text{Apply}(R_1, s_1^#))$).

Apply the induction hypothesis on $\sigma''$ to get a path from $p^#(\ell)$ to $s_1^#$, then extend that path by one step using TAPPLY.

* if that term is a join, we know the concretization of a join is the union of the concretization of its elements, so we can apply the induction hypothesis directly on the relevant element, then use TJOINELIDE or TJOINNOELIDE to turn the last path step into a step which leads into the full join instead of the single element.

Notice that we can only use TJOINELIDE if the path yielded by the induction hypothesis has non-zero length. However, if the path has length 0 then the element is $p^#(\ell)$, so TJOINNOELIDE. This is the proof step that fails when only using TJOIN, as it also needs a non-zero length path.

That last step can be turned into $s_{n-1}^# \stackrel{R_n}{\longrightarrow} \# p^#(\ell')$ via TJOINELIDE or TJOINNOELIDE (if $\mathcal{F}_g(p^#)(\ell')$ is a join) and TLOC (if $\ell'$ is a widening point).

All elements of the path satisfy $V$: the last point by VBASE and all previous ones by VREC.

This is enough to show $(p^#(\ell), \sigma) \to_{G_{p^#}}^* (p^#(\ell'), \sigma')$ since $G_{p^#}$ we have shown the edge and vertex predicates hold along the given path. $\square$

**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) \to_G^+ (\ell', \sigma') \Rightarrow (p^#(\ell), \sigma) \to_{G_{p^#}}^+ (p^#(\ell'), \sigma') $$
One solution to this is to remove $t^#$ from the new graph, but then we may lose the simulation (as no point equivalent to $t^#$ exists in the new graph, there is only the join, which has more parents).

The solution chosen here is to only carry over to the join the edges that don't lead into the image $p^#(TJOINELIDE)$, and add an explicit edge for the others (TJOINNOELIDE). Note that with these rules, Theorem 4.1 still holds (as TJOINNOELIDE is never used when all applys introduce terms). We chose to only present TJOIN in the main paper in an attempt at keeping the presentation simple.

In order to prove Theorem 5.5, we start by proving a stronger, more technical simulation result:

**LEMMA A.4.** If $F$ is a sound transformation functor, then for all reachable pairs $(\ell, \sigma)$ and $(\ell', \sigma')$ such that $(\ell, \sigma) \to_G (\ell', \sigma')$, we have $(p^#(\ell), \sigma) \to_{G_{p^#}} (p^#(\ell'), \sigma')$.

**PROOF.** Consider a transition $(\ell, \sigma) \to_G (\ell', \sigma')$. Let $R$ be the associated transition. By definition of $\to_G$, we know that $\mathcal{R}[[R]](\sigma, \sigma')$ holds.

Since FA is sound, $F(FA)$ is also sound. Thus, by Lemma A.2, $\sigma \in F(FA) \cdot \gamma(p^#(\ell))$.

Since $F$ is a transformation functor, $F(FA) \cdot \text{apply}(R, p^#(\ell))$ is a combination of $FA \cdot \text{apply}$, $FA \cdot \text{join}$ and $p^#(\ell)$, That is to say, it is a free algebra term made of Apply, Join and $p^#(\ell)$. Looking at the rules for our edge predicate, we can show that such a term represents a DAG between a unique source $(p^#(\ell))$ and a unique sink (the full term).

By soundness of $F$, $FA \cdot \gamma(F(FA) \cdot \text{apply}(R, p^#(\ell)))$ must contain $\sigma'$. Thus, looking at the concretization of the DAG term, we can show by induction on the DAG term, that there must exist a path with intermediate states $s_1^#..s_{n-1}^#$ and relations $R_1..R_n$ such that $p^#(\ell) \stackrel{R_1}{\longrightarrow} \dots \stackrel{s_1^#}{\longrightarrow} \dots \stackrel{\dots}{\longrightarrow} \dots \stackrel{R_n}{\longrightarrow} \dots \stackrel{p^#(\ell)}{\longrightarrow} \sigma'$ and $(\mathcal{R}[[R_1]]; \dots; \mathcal{R}[[R_n]])(\sigma, \sigma')$ (where $R_1; R_2$ is relation composition: $(R_1; R_2)(a, b) \triangleq \exists c, R_1(a, c) \wedge R_2(c, b)$)

* if that term is just $p^#(\ell)$, then our path is a single vertex. Since the apply was removed, we know by soundness that $R$ is no-op on $p^#(\ell)$, thus $\sigma = \sigma'$ (the empty relation composition is equality).

* if that term is $\text{Apply}(R_1, s_1^#)$ we know there exists $\sigma'' \in FA \cdot \gamma(s_1^#)$ such that $\mathcal{R}[[R_1]](\sigma'', \sigma')$ (by unfolding of $\sigma' \in FA \cdot \gamma(\text{Apply}(R_1, s_1^#))$).

Apply the induction hypothesis on $\sigma''$ to get a path from $p^#(\ell)$ to $s_1^#$, then extend that path by one step using TAPPLY.

* if that term is a join, we know the concretization of a join is the union of the concretization of its elements, so we can apply the induction hypothesis directly on the relevant element, then use TJOINELIDE or TJOINNOELIDE to turn the last path step into a step which leads into the full join instead of the single element.

Notice that we can only use TJOINELIDE if the path yielded by the induction hypothesis has non-zero length. However, if the path has length 0 then the element is $p^#(\ell)$, so TJOINNOELIDE. This is the proof step that fails when only using TJOIN, as it also needs a non-zero length path.

That last step can be turned into $s_{n-1}^# \stackrel{R_n}{\longrightarrow} \dots \stackrel{p^#(\ell')}{\longrightarrow} \sigma'$ via TJOINELIDE or TJOINNOELIDE (if $\mathcal{F}_g(p^#)(\ell')$ is a join) and TLOC (if $\ell'$ is a widening point).

All elements of the path satisfy $V$: the last point by VBASE and all previous ones by VREC.

This is enough to show $(p^#(\ell), \sigma) \to_{G_{p^#}}^* (p^#(\ell'), \sigma')$ since $G_{p^#}$ we have shown the edge and vertex predicates hold along the given path. $\square$

**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) \to_G^+ (\ell', \sigma') \Rightarrow (p^#(\ell), \sigma) \to_{G_{p^#}}^+ (p^#(\ell'), \sigma') $$
**PROOF.** Apply Lemma A.4 as many times as the initial path is long to get a path ($p^#(\ell)$, $\sigma \to_{G_{p^#}}^*$ ($p^#(\ell')$, $\sigma'$)). If the obtained path has non-zero length, then the result is shown. If its length is 0, then $p^#(\ell) = p^#(\ell')$ and $\sigma = \sigma'$. It is easy to show $p^#$ is injective when limited to entry or widening points as such terms are constructed with either Entry or Loc. Thus $\ell = \ell'$. This case is why we have the TSELF rule, it gives us a special edge to capture the fact that $\ell$ is a direct predecessor of itself. $\square$

**Proof of Theorem 5.6:** In order to prove Theorem 5.6, we start by proving a stronger, more technical simulation result:

**LEMMA A.5.** If F is complete, then for all pairs $(\ell, \sigma)$ and $(\ell', \sigma')$ such that $\ell$ is $\ell_0$ or a widening point and $(p^#(\ell), \sigma) \to_{G_{p^#}}^*$ $(p^#(\ell'), \sigma')$, then we have $(\ell, \sigma) \to_{\mathcal{G}}^*$ $(\ell', \sigma')$.

Furthermore, the right path has length 0 only if the left path also has length 0.

**PROOF SKETCH.** Proceed by strong induction on the path $(p^#(\ell), \sigma) \to_{G_{p^#}}^* (p^#(\ell'), \sigma')$. Using $p^# = p^# \nabla_W \mathcal{F}_g(p^#)$, and unfolding $\mathcal{F}_g$, we can obtain a direct predecessor $\ell''$ of $\ell$ that must be on this path. We can use the induction hypothesis to get from $\ell$ to $\ell''$, followed by completeness to get from $\ell''$ to $\ell'$.

There are some subtle cases when $p^#(\ell'')$ is equal to $p^#(\ell)$ (or $p^#(\ell')$), but $\ell'' \neq \ell$ or $\ell'' \neq \ell'$ (i.e. when successive nodes of $\mathcal{G}$ have been merged into one). We have still made progress in those cases since we cannot go through a location twice (as that would imply a loop in the source program, which would lead to a new widening point). $\square$

**PROOF.** Consider a transition path $(p^#(\ell), \sigma) \to_{G_{p^#}}^* (p^#(\ell'), \sigma')$, with $(\ell, \sigma)$ reachable and $\ell$ the entrypoint or a widening point. Unfolding $\to_{G_{p^#}}$, we obtain a path $p^#(\ell) \xrightarrow{R_1} \mathbf{s}^#_1 \xrightarrow{\vdots} \mathbf{s}^#_n \xrightarrow{R_n} \mathbf{s}^#_{n-1} \xrightarrow{\#} p^#(\ell')$. We show the result for when no widening point appears on this path. If one does, split the path where it appears, and apply the result to each segment, then compose the resulting paths.

We proceed by strong induction on this path.

If the path is empty we have $p^#(\ell) = p^#(\ell')$ and $\sigma = \sigma'$. We distinguish two cases:

* If $\ell = \ell'$ the result is immediate (empty path)

* Else $\ell \neq \ell'$.

$\ell'$ is not a widening point. This is because otherwise $p^#(\ell') = \text{Loc}(\ell')$ and since $\ell$ is either the entrypoint (Entry) or a widening ($\text{Loc}(\ell)$), we would get $\ell = \ell'$ from $p^#(\ell) = p^#(\ell')$.

Since $\ell'$ is not a widening point, we know that $p^#(\ell') = \mathcal{F}_g(p^#)(\ell')$. We also know $p^#(\ell')$ is either Entry or Loc($\ell$) since it is equal to $p^#(\ell)$.

Unfolding $\mathcal{F}_g$, we can see that $\ell'$ must have a unique (non $\perp$) predecessor $\ell''$ through a relation $R$ (since it isn't a Join) and F(FA). $\text{apply}(R, p^#(\ell'')) = \text{Loc}(\ell)$.

As a transformation functor, F(FA). $\text{apply}$ can't introduce the Loc, so it must be its argument: $p^#(\ell'') = p^#(\ell)$. Thus, we have an empty path, between argument and F(FA). $\text{apply}$. Completeness therefore implies that $\mathbb{R}[\mathbb{R}]$ contains the empty relation composition, equality. Therefore, for all $\sigma'$ we have $(\ell'', \sigma') \to_{\mathcal{G}} (\ell', \sigma')$, meaning it is sufficient to show we have a path ending in $(\ell'', \sigma')$ since that path can then be prolonged to reach $\ell'$.

We can then repeat the disjunction on $\ell'' = \ell$ using the same reasoning. This terminates because (1) there are a finite number of program locations (2) we cannot go through the same location twice (else there would be a loop, which would lead to a widening point). So at some point, we will get to $\ell$.
**PROOF.** Apply Lemma A.4 as many times as the initial path is long to get a path ($p^{#}(\ell)$, $\sigma \to_{G_{p^{#}}}^{*} (p^{#}(\ell'), \sigma')$). If the obtained path has non-zero length, then the result is shown. If its length is 0, then $p^{#}(\ell) = p^{#}(\ell')$ and $\sigma = \sigma'$. It is easy to show $p^{#}$ is injective when limited to entry or widening points as such terms are constructed with either Entry or Loc. Thus $\ell = \ell'$. This case is why we have the TSELF rule, it gives us a special edge to capture the fact that $\ell$ is a direct predecessor of itself. $\square$

**Proof of Theorem 5.6:** In order to prove Theorem 5.6, we start by proving a stronger, more technical simulation result:

**LEMMA A.5.** If F is complete, then for all pairs $(\ell, \sigma)$ and $(\ell', \sigma')$ such that $\ell$ is $\ell_0$ or a widening point and $(p^{#}(\ell), \sigma) \to_{G_{p^{#}}}^{*} (p^{#}(\ell'), \sigma')$, then we have $(\ell, \sigma) \to_{G}^{*} (\ell', \sigma')$.

Furthermore, the right path has length 0 only if the left path also has length 0.

**PROOF SKETCH.** Proceed by strong induction on the path $(p^{#}(\ell), \sigma) \to_{G_{p^{#}}}^{*} (p^{#}(\ell'), \sigma')$. Using $p^{#} = p^{#} \nabla_{W} \mathcal{F}_{g}(p^{#})$, and unfolding $\mathcal{F}_{g}$, we can obtain a direct predecessor $\ell''$ of $\ell$ that must be on this path. We can use the induction hypothesis to get from $\ell$ to $\ell''$, followed by completeness to get from $\ell''$ to $\ell'$.

There are some subtle cases when $p^{#}(\ell'')$ is equal to $p^{#}(\ell)$ (or $p^{#}(\ell')$), but $\ell'' \neq \ell$ or $\ell'' \neq \ell'$ (i.e. when successive nodes of $G$ have been merged into one). We have still made progress in those cases since we cannot go through a location twice (as that would imply a loop in the source program, which would lead to a new widening point). $\square$

**PROOF.** Consider a transition path $(p^{#}(\ell), \sigma) \to_{G_{p^{#}}}^{*} (p^{#}(\ell'), \sigma')$, with $(\ell, \sigma)$ reachable and $\ell$ the entrypoint or a widening point. Unfolding $\to_{G_{p^{#}}}^{*}$, we obtain a path $p^{#}(\ell) \xrightarrow{R_1} s_1^{#} \xrightarrow{\vdots} \vdots \xrightarrow{\vdots} s_{n-1}^{#} \xrightarrow{R_n} p^{#}(\ell')$. We show the result for when no widening point appears on this path. If one does, split the path where it appears, and apply the result to each segment, then compose the resulting paths.

We proceed by strong induction on this path.

If the path is empty we have $p^{#}(\ell) = p^{#}(\ell')$ and $\sigma = \sigma'$. We distinguish two cases:

* If $\ell = \ell'$ the result is immediate (empty path)

* Else $\ell \neq \ell'$.

$\ell'$ is not a widening point. This is because otherwise $p^{#}(\ell') = \text{Loc}(\ell')$ and since $\ell$ is either the entrypoint (Entry) or a widening ($\text{Loc}(\ell)$), we would get $\ell = \ell'$ from $p^{#}(\ell) = p^{#}(\ell')$.

Since $\ell'$ is not a widening point, we know that $p^{#}(\ell') = \mathcal{F}_{g}(p^{#})(\ell')$. We also know $p^{#}(\ell')$ is either Entry or Loc($\ell$) since it is equal to $p^{#}(\ell)$.

Unfolding $\mathcal{F}_{g}$, we can see that $\ell'$ must have a unique (non $\perp$) predecessor $\ell''$ through a relation $R$ (since it isn't a Join) and F(FA). $\text{apply}(R, p^{#}(\ell'')) = \text{Loc}(\ell)$.

As a transformation functor, F(FA). $\text{apply}$ can't introduce the Loc, so it must be its argument: $p^{#}(\ell'') = p^{#}(\ell)$. Thus, we have an empty path, between argument and F(FA). $\text{apply}$. Completeness therefore implies that $\mathbb{R}[\llcorner R\rrcorner]$ contains the empty relation composition, equality. Therefore, for all $\sigma'$ we have $(\ell'', \sigma') \to_{G} (\ell', \sigma')$, meaning it is sufficient to show we have a path ending in $(\ell'', \sigma')$ since that path can then be prolonged to reach $\ell'$.

We can then repeat the disjunction on $\ell'' = \ell$ using the same reasoning. This terminates because (1) there are a finite number of program locations (2) we cannot go through the same location twice (else there would be a loop, which would lead to a widening point). So at some point, we will get to $\ell$.
For the recursive case, consider the last step $s_{n-1}^{\#} \xrightarrow{R_n} \# p^{\#}(\ell')$. We would like to show $s_{n-1}^{\#} \xrightarrow{R_n} \# \mathcal{F}_g(p^{\#})(\ell')$, as this allows reasoning about the pre-state.

* This is immediate if $\ell'$ is not a widening.

* If $p^{\#}(\ell')$ is $\text{Loc}(\ell')$ and the last edge predicate comes from $\text{TLoc}$, the result is true since it is the premise of $\text{TLoc}$.

* Else $p^{\#}(\ell')$ is $\text{Loc}(\ell')$ and the last edge predicate comes from $\text{TSELF}$. This implies the path has length one; its relation is If 1 (so $\sigma = \sigma'$); the start and end match $\ell = \ell'$; and $\mathcal{F}_g(p^{\#})(\ell)$ is a $\text{Join}(\mathcal{S}^{\#})$ with $p^{\#}(\ell) \in \mathcal{S}^{\#}$.

In that case, since $\mathcal{F}_g(p^{\#})$ is a join that contains $p^{\#}(\ell)$, there is a looping path from $\ell$ to itself in $\mathcal{G}$. Furthermore, since the relation on this path have been erased by the functor, completeness implies they are all trivial. Thus, this circular path in $\mathcal{G}$ proves the lemma in this case.

For all remaining cases, we have $s_{n-1}^{\#} \xrightarrow{R_n} \# \mathcal{F}_g(p^{\#})(\ell')$. The right term is not $\perp$ or $\text{Entry}$ (as it has an incoming edge), thus by unfolding $\mathcal{F}_g$ and F(FA). $\text{join}$, it is either a $\text{Join}$ of an F(FA). $\text{apply}$ of the predecessors, or directly an F(FA). $\text{apply}$ of the unique predecessor. Either way (use $\text{TJOINELIDE}$ or $\text{TJOINNOELIDE}$ in the first case), we know there exists a $\ell''$, predecessor of $\ell'$ through a relation $R$ such that $s_{n-1}^{\#} \xrightarrow{R_n} \# \text{F}(\text{FA}).\text{apply}(R, p^{\#}(\ell''))$

Since the path contains no $\text{Locs}$ (as there are no widening points on it), it implies that $p^{\#}(\ell)$ is a subterm of F(FA). $\text{apply}(R, p^{\#}(\ell''))$ (It is easy to show that, when only using $\text{TAPPLY}$, $\text{TJOINELIDE}$ and $\text{TJOINNOELIDE}$, we have $s^{\#} \xrightarrow{R} \# t^{\#} \Rightarrow s^{\#}$ subterm of $t^{\#}$). Furthermore, by definition of transformation functors, $p^{\#}(\ell'')$ is a source subterm of F(FA). $\text{apply}(R, p^{\#}(\ell''))$.

$p^{\#}(\ell)$ cannot be a strict super-term of $p^{\#}(\ell'')$ since it is the entrypoint or a widening point (it has no subterms and cannot be introduced by F(FA). $\text{apply}$), thus it is either $p^{\#}(\ell'')$ or a subterm of it.

* Case $p^{\#}(\ell) = p^{\#}(\ell'')$

- If $\ell = \ell''$, then the chain simplifies to

$$p^{\#}(\ell) \xrightarrow{R_1} s_1^{\#} \cdots \xrightarrow{\cdots} s_{n-1}^{\#} \xrightarrow{R_n} \# \text{F}(\text{FA}).\text{apply}(R, p^{\#}(\ell))$$

Using the completeness yields $\mathcal{R}[R](\sigma, \sigma')$.

- The case $\ell'' \neq \ell$ is handled similarly to the initialization: $\ell''$ isn't a widening, so it has a single parent $\ell'''$ through a relation $R'$, and $\mathcal{R}[R']$ contains equality, so showing the result ending in $\ell'''$ is sufficient. Repeat the disjunction on $\ell'''$. This terminates because there is a finite number of locations, and we cannot loop.

* If $p^{\#}(\ell)$ is a strict subterm of $p^{\#}(\ell'')$ then either $p^{\#}(\ell'')$ appears on the path, or it is equal to the path's last term $p^{\#}(\ell')$. In the first case, use the recursion hypothesis on the first segment to obtain a path from $\ell$ to $\ell''$, followed by completeness for the (non-empty) path from $\ell''$ to $\ell'$.

The second case is the third time we run into the 0-step problem: $p^{\#}(\ell'') = p^{\#}(\ell')$ and $\ell'' \neq \ell'$. It is solved in the same way as the first two occurrences: we can show that $(\ell'', \sigma') \to_{\mathcal{G}} (\ell', \sigma')$ by completion; and that $\ell''$ has a parent that satisfies the same hypotheses, and that we will eventually take a non-zero step along our path since there are a finite number of locations, and we cannot loop.

In all cases, we have taken a step in $\mathcal{G}$, so we know the new path will not have length 0. □

**THEOREM 5.6 (COMPLETE FUNCTIONAL 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) \to_{\mathcal{G}_{p^{\#}}} (p^{\#}(\ell'), \sigma') \Rightarrow (\ell, \sigma) \to_{\mathcal{G}} (\ell', \sigma')$$
For the recursive case, consider the last step $s_{n-1}^{\#} \xrightarrow{R_n} \# p^{\#}(\ell')$. We would like to show $s_{n-1}^{\#} \xrightarrow{R_n} \# \mathcal{F}_g(p^{\#})(\ell')$, as this allows reasoning about the pre-state.

* This is immediate if $\ell'$ is not a widening.

* If $p^{\#}(\ell')$ is $\text{Loc}(\ell')$ and the last edge predicate comes from $\text{TLoc}$, the result is true since it is the premise of $\text{TLoc}$.

* Else $p^{\#}(\ell')$ is $\text{Loc}(\ell')$ and the last edge predicate comes from $\text{TSELF}$. This implies the path has length one; its relation is If 1 (so $\sigma = \sigma'$); the start and end match $\ell = \ell'$; and $\mathcal{F}_g(p^{\#})(\ell)$ is a $\text{Join}(\mathcal{S}^{\#})$ with $p^{\#}(\ell) \in \mathcal{S}^{\#}$.

In that case, since $\mathcal{F}_g(p^{\#})$ is a join that contains $p^{\#}(\ell)$, there is a looping path from $\ell$ to itself in $\mathcal{G}$. Furthermore, since the relation on this path have been erased by the functor, completeness implies they are all trivial. Thus, this circular path in $\mathcal{G}$ proves the lemma in this case.

For all remaining cases, we have $s_{n-1}^{\#} \xrightarrow{R_n} \# \mathcal{F}_g(p^{\#})(\ell')$. The right term is not $\perp$ or $\text{Entry}$ (as it has an incoming edge), thus by unfolding $\mathcal{F}_g$ and F(FA). $\text{join}$, it is either a $\text{Join}$ of an F(FA). $\text{apply}$ of the predecessors, or directly an F(FA). $\text{apply}$ of the unique predecessor. Either way (use $\text{TJOINELIDE}$ or $\text{TJOINNOELIDE}$ in the first case), we know there exists a $\ell''$, predecessor of $\ell'$ through a relation $R$ such that $s_{n-1}^{\#} \xrightarrow{R_n} \# \text{F}(\text{FA}).\text{apply}(R, p^{\#}(\ell''))$

Since the path contains no $\text{Locs}$ (as there are no widening points on it), it implies that $p^{\#}(\ell)$ is a subterm of F(FA). $\text{apply}(R, p^{\#}(\ell''))$ (It is easy to show that, when only using $\text{TAPPLY}$, $\text{TJOINELIDE}$ and $\text{TJOINNOELIDE}$, we have $s^{\#} \xrightarrow{R} \# t^{\#} \Rightarrow s^{\#}$ subterm of $t^{\#}$). Furthermore, by definition of transformation functors, $p^{\#}(\ell'')$ is a source subterm of F(FA). $\text{apply}(R, p^{\#}(\ell''))$.

$p^{\#}(\ell)$ cannot be a strict super-term of $p^{\#}(\ell'')$ since it is the entrypoint or a widening point (it has no subterms and cannot be introduced by F(FA). $\text{apply}$), thus it is either $p^{\#}(\ell'')$ or a subterm of it.

* Case $p^{\#}(\ell) = p^{\#}(\ell'')$

- If $\ell = \ell''$, then the chain simplifies to

$$p^{\#}(\ell) \xrightarrow{R_1} s_1^{\#} \cdots \xrightarrow{\cdots} s_{n-1}^{\#} \xrightarrow{R_n} \# \text{F}(\text{FA}).\text{apply}(R, p^{\#}(\ell))$$

Using the completeness yields $\mathcal{R}[R] (\sigma, \sigma')$.

- The case $\ell'' \neq \ell$ is handled similarly to the initialization: $\ell''$ isn't a widening, so it has a single parent $\ell'''$ through a relation $R'$, and $\mathcal{R}[R']$ contains equality, so showing the result ending in $\ell'''$ is sufficient. Repeat the disjunction on $\ell'''$. This terminates because there is a finite number of locations, and we cannot loop.

* If $p^{\#}(\ell)$ is a strict subterm of $p^{\#}(\ell'')$ then either $p^{\#}(\ell'')$ appears on the path, or it is equal to the path's last term $p^{\#}(\ell')$. In the first case, use the recursion hypothesis on the first segment to obtain a path from $\ell$ to $\ell''$, followed by completeness for the (non-empty) path from $\ell''$ to $\ell'$.

The second case is the third time we run into the 0-step problem: $p^{\#}(\ell'') = p^{\#}(\ell')$ and $\ell'' \neq \ell'$. It is solved in the same way as the first two occurrences: we can show that $(\ell'', \sigma') \to_{\mathcal{G}} (\ell', \sigma')$ by completion; and that $\ell''$ has a parent that satisfies the same hypotheses, and that we will eventually take a non-zero step along our path since there are a finite number of locations, and we cannot loop.

In all cases, we have taken a step in $\mathcal{G}$, so we know the new path will not have length 0. □

**THEOREM 5.6 (COMPLETE FUNCTIONAL 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) \to_{\mathcal{G}_{p^{\#}}} (p^{\#}(\ell'), \sigma') \Rightarrow (\ell, \sigma) \to_{\mathcal{G}} (\ell', \sigma')$$
PROOF. Apply Lemma A.5 as many times as the initial path is long to get a path $(\ell, \sigma) \to_G^* (\ell', \sigma')$. Since the initial path is not empty, we also know this new path is not empty. □

## A.4 Proofs: Lifting SSA domains to Imp domains

**Proof of Theorem 7.1:** we start by proving the following technical lemma.

LEMMA A.6 (SSA FORWARD SIMULATION). For all reachable pairs $(\ell, \sigma)$ and $(\ell', \sigma')$ such that $(\ell, \sigma) \to_G (\ell', \sigma')$:

* For all $(\Gamma^#, \Gamma)$ such that $C((\ell, \sigma), (\Gamma^#, \Gamma))$, there exists $(\Gamma'^#, \Gamma')$ such that we have both $C((\ell', \sigma'), (\Gamma'^#, \Gamma'))$ and $(\Gamma^#, \Gamma) \rightsquigarrow^{\hat{G}_{p^#}} (\Gamma'^#, \Gamma')$.

* There exists $(\Gamma^#, \Gamma)$ such that $C((\ell, \sigma), (\Gamma^#, \Gamma))$

* The $(\Gamma^#, \Gamma) \rightsquigarrow^{\hat{G}_{p^#}} (\Gamma'^#, \Gamma')$ is of length 0 only when $\ell'$ has a single predecessor.

PROOF SKETCH. For existence, $\Gamma^#$ is uniquely determined by $p^#(\ell)$ and $\Gamma$ exists by soundness and definition of Lift($\overline{\Gamma A}$). $\gamma$. For the other point, proceed by disjunction on $\mathcal{F}_g(p^#)(\ell')$, which is either the same SSA term $\Gamma^#$ as in $p^#(\ell)$, an Assûme($e, \Gamma^#$), or Join containing either $\Gamma^#$ or Assûme($e, \Gamma^#$). These case yield paths of lengths 0, 1, 1 and 2 respectively. □

PROOF. Take $(\ell, \sigma)$ and $(\ell', \sigma')$ reachable such that $(\ell, \sigma) \to_G (\ell', \sigma')$ via a relation $R$. Since both are reachable, their values through $p^#$ are not $\perp$ by soundness. Let us denote $(\sigma_0^#, \Gamma^#) \triangleq p^#(\ell)$ and $(\sigma_1^#, \Gamma'^#) \triangleq p^#(\ell')$. Soundness also implies $\sigma \in \text{Lift}(\overline{\Gamma A})$. $\gamma((\sigma_0^#, \Gamma^#))$ so, by unfolding Lift($\overline{\Gamma A}$). $\gamma$, we know there exists $\Gamma$ such that $\forall x, \hat{\mathcal{E}}[\sigma_0^#(x)](\Gamma) = \sigma(x)$. This proves the second point. For the first, take any $\Gamma$ that satisfies this property.

We know $\ell' \neq \ell_0$ since it has a predecessor $\ell$. Furthermore, if $\ell'$ is a widening point, we can use TLocSSA to obtain a new $\Gamma'^#$ with the same transitions which is equal to the one in $\mathcal{F}_g(p^#)(\ell')$. In the remaining cases, we have $\Gamma'^#$ equal to the one in $\mathcal{F}_g(p^#)(\ell')$.

The term built by $\mathcal{F}_g$ is a Lift($\overline{\Gamma A}$). join of Lift($\overline{\Gamma A}$). apply of the predecessors (which include $\ell$). Looking how these map to our SSA operations, we notice four cases: join may or may not introduce a Join, and apply may or may not introduce an Assûme.

* If $R$ is a guard "If $e$", then an Assûme is introduced; since the guard holds on $(\sigma, \sigma')$, we also know $\sigma = \sigma'$ and $\mathcal{E}[e](\sigma) \neq 0$. Therefore, we also have $\hat{\mathcal{E}}[\text{subst}(e, \sigma_0^#)](\Gamma) \neq 0$, which implies that $(\Gamma^#, \Gamma) \rightsquigarrow^{\hat{G}_{p^#}} (\text{Assûme}(\text{subst}(e, \sigma_0^#), \Gamma^#), \Gamma)$.

If no join is introduced, then we know Assûme($\text{subst}(e, \sigma_0^#), \Gamma^#$) = $\Gamma'^#$ and $\sigma_0^# = \sigma_1^#$. We set $\Gamma' \triangleq \Gamma$. We have a path of length 1, and the property on $\Gamma'$ is immediate given the one on $\Gamma$. If a join is introduced, let $B$ be the set of bindings for the $\Gamma^#$ branch. We define $\Gamma' \triangleq \text{unbind}_{\hat{G}_{p^#}}(\Gamma'^#, \text{bind}(B, \Gamma))$ and we have $(\Gamma^#, \Gamma) \rightsquigarrow^{\hat{G}_{p^#}} (\text{Assûme}(e, \Gamma^#), \Gamma) \rightsquigarrow^{\hat{G}_{p^#}} (\Gamma'^#, \Gamma')$. This is a path of length 2.

To show the condition on $\Gamma'$, take a variable $x$:

- If $x$ isn't in $\text{dom } B$, then its values are equal in all join branches. This means $\sigma_1^#(x) = \sigma_0^#(x)$. It also implies that that expression was in scope in all branches and therefore is still in scope at the join. So its evaluation is neither modified by $\text{unbind}_{\hat{G}_{p^#}}$ (in scope), nor by $\text{bind}(B, \Gamma)$ (not in $\text{dom } B$).

Thus, $\hat{\mathcal{E}}[\sigma_1^#(x)](\Gamma') = \hat{\mathcal{E}}[\sigma_0^#(x)](\text{unbind}_{\hat{G}_{p^#}}(\Gamma'^#, \text{bind}(B, \Gamma))) = \hat{\mathcal{E}}[\sigma_0^#(x)](\Gamma) = \sigma(x) = \sigma'(x)$
PROOF. Apply Lemma A.5 as many times as the initial path is long to get a path $(\ell, \sigma) \to_G^* (\ell', \sigma')$. Since the initial path is not empty, we also know this new path is not empty. □

## A.4 Proofs: Lifting SSA domains to Imp domains

**Proof of Theorem 7.1:** we start by proving the following technical lemma.

LEMMA A.6 (SSA FORWARD SIMULATION). For all reachable pairs $(\ell, \sigma)$ and $(\ell', \sigma')$ such that $(\ell, \sigma) \to_G (\ell', \sigma')$:

* For all $(\Gamma^#, \Gamma)$ such that $C((\ell, \sigma), (\Gamma^#, \Gamma))$, there exists $(\Gamma'^#, \Gamma')$ such that we have both $C((\ell', \sigma'), (\Gamma'^#, \Gamma'))$ and $(\Gamma^#, \Gamma) \rightsquigarrow^{\hat{G}_{p^#}} (\Gamma'^#, \Gamma')$.

* There exists $(\Gamma^#, \Gamma)$ such that $C((\ell, \sigma), (\Gamma^#, \Gamma))$

* The $(\Gamma^#, \Gamma) \rightsquigarrow^{\hat{G}_{p^#}} (\Gamma'^#, \Gamma')$ is of length 0 only when $\ell'$ has a single predecessor.

PROOF SKETCH. For existence, $\Gamma^#$ is uniquely determined by $p^#(\ell)$ and $\Gamma$ exists by soundness and definition of Lift($\overline{\Gamma A}$). $\gamma$. For the other point, proceed by disjunction on $\mathcal{F}_g(p^#)(\ell')$, which is either the same SSA term $\Gamma^#$ as in $p^#(\ell)$, an Assûme($e, \Gamma^#$), or Join containing either $\Gamma^#$ or Assûme($e, \Gamma^#$). These case yield paths of lengths 0, 1, 1 and 2 respectively. □

PROOF. Take $(\ell, \sigma)$ and $(\ell', \sigma')$ reachable such that $(\ell, \sigma) \to_G (\ell', \sigma')$ via a relation $R$. Since both are reachable, their values through $p^#$ are not $\perp$ by soundness. Let us denote $(\sigma_0^#, \Gamma^#) \triangleq p^#(\ell)$ and $(\sigma_1^#, \Gamma'^#) \triangleq p^#(\ell')$. Soundness also implies $\sigma \in \text{Lift}(\overline{\Gamma A})$. $\gamma((\sigma_0^#, \Gamma^#))$ so, by unfolding Lift($\overline{\Gamma A}$). $\gamma$, we know there exists $\Gamma$ such that $\forall x, \hat{\mathcal{E}}[\sigma_0^#(x)](\Gamma) = \sigma(x)$. This proves the second point. For the first, take any $\Gamma$ that satisfies this property.

We know $\ell' \neq \ell_0$ since it has a predecessor $\ell$. Furthermore, if $\ell'$ is a widening point, we can use TLocSSA to obtain a new $\Gamma'^#$ with the same transitions which is equal to the one in $\mathcal{F}_g(p^#)(\ell')$. In the remaining cases, we have $\Gamma'^#$ equal to the one in $\mathcal{F}_g(p^#)(\ell')$.

The term built by $\mathcal{F}_g$ is a Lift($\overline{\Gamma A}$). join of Lift($\overline{\Gamma A}$). apply of the predecessors (which include $\ell$). Looking how these map to our SSA operations, we notice four cases: join may or may not introduce a Join, and apply may or may not introduce an Assûme.

* If $R$ is a guard "If $e$", then an Assûme is introduced; since the guard holds on $(\sigma, \sigma')$, we also know $\sigma = \sigma'$ and $\mathcal{E}[e](\sigma) \neq 0$. Therefore, we also have $\hat{\mathcal{E}}[\text{subst}(e, \sigma_0^#)](\Gamma) \neq 0$, which implies that $(\Gamma^#, \Gamma) \rightsquigarrow^{\hat{G}_{p^#}} (\text{Assûme}(\text{subst}(e, \sigma_0^#), \Gamma^#), \Gamma)$.

If no join is introduced, then we know Assûme($\text{subst}(e, \sigma_0^#), \Gamma^#$) = $\Gamma'^#$ and $\sigma_0^# = \sigma_1^#$. We set $\Gamma' \triangleq \Gamma$. We have a path of length 1, and the property on $\Gamma'$ is immediate given the one on $\Gamma$. If a join is introduced, let $B$ be the set of bindings for the $\Gamma^#$ branch. We define $\Gamma' \triangleq \text{unbind}_{\hat{G}_{p^#}}(\Gamma'^#, \text{bind}(B, \Gamma))$ and we have $(\Gamma^#, \Gamma) \rightsquigarrow^{\hat{G}_{p^#}} (\text{Assûme}(e, \Gamma^#), \Gamma) \rightsquigarrow^{\hat{G}_{p^#}} (\Gamma'^#, \Gamma')$. This is a path of length 2.

To show the condition on $\Gamma'$, take a variable $x$:

- If $x$ isn't in $\text{dom } B$, then its values are equal in all join branches. This means $\sigma_1^#(x) = \sigma_0^#(x)$. It also implies that that expression was in scope in all branches and therefore is still in scope at the join. So its evaluation is neither modified by $\text{unbind}_{\hat{G}_{p^#}}$ (in scope), nor by $\text{bind}(B, \Gamma)$ (not in $\text{dom } B$).

Thus, $\hat{\mathcal{E}}[\sigma_1^#(x)](\Gamma') = \hat{\mathcal{E}}[\sigma_0^#(x)](\text{unbind}_{\hat{G}_{p^#}}(\Gamma'^#, \text{bind}(B, \Gamma))) = \hat{\mathcal{E}}[\sigma_0^#(x)](\Gamma) = \sigma(x) = \sigma'(x)$
- Otherwise, it is bound to a new variable $x_{\Gamma'^{\#}}$. Thus, it is in scope of $\Gamma'^{\#}$ and not removed by unbind $\hat{G}_{p^{\#}}$. Furthermore, B must bind $x_{\Gamma'^{\#}}$ to $\sigma_0^{\#}(x)$, so evaluating it also yields the same value.

* If $R$ is an assignment "$x := e$", no Assûme is introduced; and $\sigma' = \sigma [x \mapsto \mathcal{E}[e]](\sigma)$.
  If no join is introduced then we know that $\Gamma'^{\#} = \Gamma^{\#}$ and $\sigma_1^{\#} = \sigma_0^{\#} [x \mapsto \text{subst}(e, \sigma_0^{\#})]$ hold.
  We set $\Gamma' \triangleq \Gamma$. We have a path of length 0. All that needs to be shown is the property on $\Gamma'$, which is true for all variables except $x$ trivially, and true on $x$ by compatibility between $\text{subst}$ and $\mathcal{E}[\cdot]$. This is the only case where the path has length 0, and it implies $\ell'$ only has a single predecessor (no join). Thus, it proves the third point.
  If we introduce a join, let $B$ be the set of bindings for the $\Gamma^{\#}$ branch. We define $\Gamma' \triangleq \text{unbind}_{\hat{G}_{p^{\#}}} (\Gamma'^{\#}, \text{bind}(B, \Gamma))$ and we have $(\Gamma^{\#}, \Gamma) \rightsquigarrow \hat{G}_{p^{\#}} (\Gamma'^{\#}, \Gamma')$. This is a length 1 path.
  Showing the condition on $\Gamma'$ is the same as in the previous case with a join. $\square$

**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{S}$ we have:

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

Furthermore, there exists an $\hat{s} \in \hat{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).

The condition on $\ell'$ when paths have length 0 means it is either an extra point added to $W$ (not a loop head in the initial program), or it is the head of a loop that is syntactically never taken (e.g. while (...) {...; break; }). When combining SSA translation with transformation functors, it can also be the head of a loop that our analysis proves to be broken before completing the first iteration (e.g. while (c) when $c = 0$, or while (...) {... if (c) break; } when $c \neq 0$).

**PROOF.** We apply Lemma A.6 as many times as the input path is long, and then compose the resulting paths. $\square$

**Proof of Theorem 7.2:** we start by proving the following technical lemma.

**LEMMA A.7 (SSA BACKWARD SIMULATION).** For all paths $(\Gamma^{\#}, \Gamma) \rightsquigarrow_{\hat{G}_{p^{\#}}}^{*} (\Gamma'^{\#}, \Gamma')$ such that $\Gamma^{\#}$ and $\Gamma'^{\#}$ appear in $\text{img } p^{\#}$:

* For all $(\ell', \sigma')$ such that $C((\ell', \sigma'), (\Gamma'^{\#}, \Gamma'))$, there exists $(\ell, \sigma)$ such that $(\ell, \sigma) \to_{\hat{G}} (\ell', \sigma')$ and $C((\ell, \sigma), (\Gamma^{\#}, \Gamma))$.

* There exists $(\ell, \sigma)$ such that $C((\ell, \sigma), (\Gamma^{\#}, \Gamma))$

**PROOF SKETCH.** We show the result on paths that don't go through $\text{img } p^{\#}$, composing them if needed. $\Gamma'^{\#}$ is in the image of $p^{\#}$, so it has the same transitions as those to a $\mathcal{F}_g(p^{\#})(\ell')$ term. Thus, we have the same cases four cases as in Lemma A.6. We can use the no $p^{\#}$ on the path hypothesis to ensure the start $p^{\#}(\ell)$ of our path must match $\Gamma^{\#}$. This requires a bit of work for the length 0 case though. $\square$

**PROOF.** Take $(\Gamma^{\#}, \Gamma) \rightsquigarrow_{\hat{G}_{p^{\#}}}^{*} (\Gamma'^{\#}, \Gamma')$ such that $\Gamma^{\#}$ and $\Gamma'^{\#}$ appear in $\text{img } p^{\#}$. We show the result for when the path does not go through the image of $p^{\#}$, since the general case can be established by splitting the path around nodes that are in the image of $p^{\#}$ and applying the result to each segment. $\Gamma'^{\#}$ is in the image of $p^{\#}$, so there exists $\ell'$ and $\sigma_1^{\#}$ such that $(\sigma_1^{\#}, \Gamma'^{\#}) = p^{\#}(\ell')$. We can then define $\sigma' \triangleq [x \in \mathbb{L} \mapsto \hat{\mathcal{E}}[\sigma_1^{\#}(x)](\Gamma)]$ which shows existence.

For the rest of this proof, take $\ell'$ and $\sigma'$ such that $C((\ell', \sigma'), (\Gamma'^{\#}, \Gamma'))$.
- Otherwise, it is bound to a new variable $x_{\Gamma'^{\#}}$. Thus, it is in scope of $\Gamma'^{\#}$ and not removed by unbind $\hat{G}_{p^{\#}}$. Furthermore, B must bind $x_{\Gamma'^{\#}}$ to $\sigma_0^{\#}(x)$, so evaluating it also yields the same value.

* If $R$ is an assignment $x := e$", no Assûme is introduced; and $\sigma' = \sigma [x \mapsto \mathcal{E}[e]](\sigma)$.
If no join is introduced then we know that $\Gamma'^{\#} = \Gamma^{\#}$ and $\sigma_1^{\#} = \sigma_0^{\#} [x \mapsto \text{subst}(e, \sigma_0^{\#})]$ hold.
We set $\Gamma' \triangleq \Gamma$. We have a path of length 0. All that needs to be shown is the property on $\Gamma'$, which is true for all variables except $x$ trivially, and true on $x$ by compatibility between $\text{subst}$ and $\mathcal{E}[\cdot]$. This is the only case where the path has length 0, and it implies $\ell'$ only has a single predecessor (no join). Thus, it proves the third point.
If we introduce a join, let $B$ be the set of bindings for the $\Gamma^{\#}$ branch. We define $\Gamma' \triangleq \text{unbind}_{\hat{G}_{p^{\#}}} (\Gamma'^{\#}, \text{bind}(B, \Gamma))$ and we have $(\Gamma^{\#}, \Gamma) \rightsquigarrow \hat{G}_{p^{\#}} (\Gamma'^{\#}, \Gamma')$. This is a length 1 path.
Showing the condition on $\Gamma'$ is the same as in the previous case with a join. $\square$

**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{S}$ we have:

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

Furthermore, there exists an $\hat{s} \in \hat{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).

The condition on $\ell'$ when paths have length 0 means it is either an extra point added to $W$ (not a loop head in the initial program), or it is the head of a loop that is syntactically never taken (e.g. while (...) {...; break; }). When combining SSA translation with transformation functors, it can also be the head of a loop that our analysis proves to be broken before completing the first iteration (e.g. while (c) when $c = 0$, or while (...) {... if (c) break; } when $c \neq 0$).

**PROOF.** We apply Lemma A.6 as many times as the input path is long, and then compose the resulting paths. $\square$

**Proof of Theorem 7.2:** we start by proving the following technical lemma.

**LEMMA A.7 (SSA BACKWARD SIMULATION).** For all paths $(\Gamma^{\#}, \Gamma) \rightsquigarrow_{\hat{G}_{p^{\#}}}^{*} (\Gamma'^{\#}, \Gamma')$ such that $\Gamma^{\#}$ and $\Gamma'^{\#}$ appear in $\text{img } p^{\#}$:

* For all $(\ell', \sigma')$ such that $C((\ell', \sigma'), (\Gamma'^{\#}, \Gamma'))$, there exists $(\ell, \sigma)$ such that $(\ell, \sigma) \to_{\hat{G}} (\ell', \sigma')$ and $C((\ell, \sigma), (\Gamma^{\#}, \Gamma))$.

* There exists $(\ell, \sigma)$ such that $C((\ell, \sigma), (\Gamma^{\#}, \Gamma))$

**PROOF SKETCH.** We show the result on paths that don't go through $\text{img } p^{\#}$, composing them if needed. $\Gamma'^{\#}$ is in the image of $p^{\#}$, so it has the same transitions as those to a $\mathcal{F}_g(p^{\#})(\ell')$ term. Thus, we have the same cases four cases as in Lemma A.6. We can use the no $p^{\#}$ on the path hypothesis to ensure the start $p^{\#}(\ell)$ of our path must match $\Gamma^{\#}$. This requires a bit of work for the length 0 case though. $\square$

**PROOF.** Take $(\Gamma^{\#}, \Gamma) \rightsquigarrow_{\hat{G}_{p^{\#}}}^{*} (\Gamma'^{\#}, \Gamma')$ such that $\Gamma^{\#}$ and $\Gamma'^{\#}$ appear in $\text{img } p^{\#}$. We show the result for when the path does not go through the image of $p^{\#}$, since the general case can be established by splitting the path around nodes that are in the image of $p^{\#}$ and applying the result to each segment. $\Gamma'^{\#}$ is in the image of $p^{\#}$, so there exists $\ell'$ and $\sigma_1^{\#}$ such that $(\sigma_1^{\#}, \Gamma'^{\#}) = p^{\#}(\ell')$. We can then define $\sigma' \triangleq [x \in \mathbb{L} \mapsto \hat{\mathcal{E}}[\sigma_1^{\#}(x)](\Gamma)]$ which shows existence.

For the rest of this proof, take $\ell'$ and $\sigma'$ such that $C((\ell', \sigma'), (\Gamma'^{\#}, \Gamma'))$.
The same reasoning as in the previous theorem shows we can take $\Gamma'^{\#}$ to be the same as $\mathcal{F}_g(p^{\#})(\ell')$ without changing the path. The term built by $\mathcal{F}_g$ is a join of apply of the predecessors of $\ell'$. These predecessors are in the image of $p^{\#}$.

Looking how these map to our SSA operations, we notice the same four cases as before in the previous lemma (Lemma A.6). They imply that a path from a predecessor not going through the image of $p^{\#}$ is either empty, an Assûme, a Join, or a Join of an Assûme. Furthermore, these are the only paths that reach $\Gamma'^{\#}$, so one of these predecessors must correspond to the path coming from $\Gamma^{\#}$. Let us denote it $\ell$ and its associated relation $R$.

If the path from $p^{\#}(\ell)$ is non-empty, it must correspond to $\Gamma^{\#}$ (Otherwise, the path from $\Gamma^{\#}$ would go through a point in $\text{img } p^{\#}$). If the path is empty, then either $p^{\#}(\ell) \neq (\llcorner, \Gamma^{\#})$, then we can choose a $\ell \neq \ell'$ (else $\Gamma'^{\#}$ has only one parent, itself, and so $\Gamma^{\#} = \Gamma'^{\#}$). We can repeat this process until we find a $\ell$ that matches $\Gamma^{\#}$. This terminates because there is a finite number of program locations.

There must then exist $\sigma_0^{\#}$ such that $(\sigma_0^{\#}, \Gamma^{\#}) = p^{\#}(\ell)$.

* If there is no Assûme, then by inverting apply, we know that $R$ is an assignment “$x := e$”. If there is also no Join, the path is empty. $\Gamma^{\#} = \Gamma'^{\#}, \Gamma = \Gamma'$ and $\sigma_1^{\#} = \sigma_0^{\#} [x \mapsto \text{subst}(e, \sigma_0^{\#})]$. Choosing $\sigma \triangleq [x \in \mathbb{L} \mapsto \hat{\mathcal{E}}[\sigma_0^{\#}(x)](\Gamma)]$ is then sufficient. It indeed verifies the compatibility with $\Gamma$, which, combined with the compatibility between $\Gamma'$ and $\sigma'$, implies $\sigma' = \sigma [x \mapsto \mathcal{E}[e](\sigma)]$ by compatibility between $\text{subst}$ and $\mathcal{E}[\cdot]$.

If there is a Join, the path is a single transition labelled by bindings: $\Gamma^{\#} \stackrel{B}{\rightleftharpoons} \Gamma'^{\#}$. We therefore have $\Gamma' \triangleq \text{unbind}_{\hat{\mathcal{E}}_{p^{\#}}}(\Gamma'^{\#}, \text{bind}(B, \Gamma))$. Furthermore, if we denote $\sigma_2^{\#} \triangleq \sigma_0^{\#} [x \mapsto \text{subst}(e, \sigma_0^{\#})]$ $\sigma_1^{\#}$ is equal to $\sigma_2^{\#}$ on the variables not in $\text{dom } B$ and renames those in $\text{dom } B$ to $x_{\Gamma'^{\#}}$. Note that $B$ maps these variables to their value in $\sigma_2^{\#}$. Therefore, for all $x$, $\hat{\mathcal{E}}[\sigma_1^{\#}(x)](\Gamma') = \hat{\mathcal{E}}[\sigma_2^{\#}(x)](\Gamma')$. So again, it is sufficient to choose $\sigma \triangleq [x \in \mathbb{L} \mapsto \hat{\mathcal{E}}[\sigma_0^{\#}(x)](\Gamma)]$ and $\sigma' \triangleq [x \in \mathbb{L} \mapsto \hat{\mathcal{E}}[\sigma_1^{\#}(x)](\Gamma)]$ to show the results.

* If there is an Assûme, then by inverting apply, we know that $R$ is a guard “If $e$”. If there is also no Join, the path is a single transition $\Gamma^{\#} \stackrel{e}{\rightleftharpoons} \Gamma'^{\#}$. This transition implies that $\Gamma = \Gamma'$, $\sigma_1^{\#} = \sigma_0^{\#}$ and $\hat{\mathcal{E}}[e](\Gamma) \neq 0$. Choosing $\sigma \triangleq [x \in \mathbb{L} \mapsto \hat{\mathcal{E}}[\sigma_0^{\#}(x)](\Gamma)]$ is then sufficient. It indeed verifies $\sigma = \sigma' \wedge \mathcal{E}[e](\sigma) \neq 0$ and the compatibility with $\Gamma$ by definition. If there is a Join, the path is made of two transitions:

$$ \Gamma^{\#} \stackrel{e}{\rightleftharpoons}_{\#} \text{Assûme}(e, \Gamma^{\#}) \stackrel{B}{\rightleftharpoons}_{\#} \Gamma'^{\#} $$

We therefore have $\Gamma' \triangleq \text{unbind}_{\hat{\mathcal{E}}_{p^{\#}}}(\Gamma'^{\#}, \text{bind}(B, \Gamma))$. Furthermore, $\sigma_1^{\#}$ is equal to $\sigma_0^{\#}$ on the variables not in $\text{dom } B$ and renames those in $\text{dom } B$ to $x_{\Gamma'^{\#}}$. Note that $B$ maps these variables to their value in $\sigma_0^{\#}$. Therefore, for all $x$, $\hat{\mathcal{E}}[\sigma_1^{\#}(x)](\Gamma') = \hat{\mathcal{E}}[\sigma_0^{\#}(x)](\Gamma)$. So again, it is sufficient to choose $\sigma \triangleq [x \in \mathbb{L} \mapsto \hat{\mathcal{E}}[\sigma_0^{\#}(x)](\Gamma)]$ to show the results. $\square$

**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 \mathcal{S}$ we have:

$$ (\Gamma^{\#}, \Gamma) \rightsquigarrow_{\hat{\mathcal{G}}_{p^{\#}}} (\Gamma'^{\#}, \Gamma') \wedge C(s', (\Gamma'^{\#}, \Gamma')) \Rightarrow \exists s \in \mathcal{S}, C(s, (\Gamma^{\#}, \Gamma)) \wedge s \to^{+}_{\mathcal{G}} s' $$

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

**PROOF.** Apply Lemma A.7 as many times as the input path is long, and compose the results. $\square$

## A.5 Proofs: SSA based numerical analysis

### Proof of Lemma 8.2:
The same reasoning as in the previous theorem shows we can take $\Gamma'^{\#}$ to be the same as $\mathcal{F}_g(p^{\#})(\ell')$ without changing the path. The term built by $\mathcal{F}_g$ is a join of apply of the predecessors of $\ell'$. These predecessors are in the image of $p^{\#}$.

Looking how these map to our SSA operations, we notice the same four cases as before in the previous lemma (Lemma A.6). They imply that a path from a predecessor not going through the image of $p^{\#}$ is either empty, an Assûme, a Join, or a Join of an Assûme. Furthermore, these are the only paths that reach $\Gamma'^{\#}$, so one of these predecessors must correspond to the path coming from $\Gamma^{\#}$. Let us denote it $\ell$ and its associated relation $R$.

If the path from $p^{\#}(\ell)$ is non-empty, it must correspond to $\Gamma^{\#}$ (Otherwise, the path from $\Gamma^{\#}$ would go through a point in $\text{img } p^{\#}$). If the path is empty, then either $p^{\#}(\ell) \neq (\llcorner, \Gamma^{\#})$, then we can choose a $\ell \neq \ell'$ (else $\Gamma'^{\#}$ has only one parent, itself, and so $\Gamma^{\#} = \Gamma'^{\#}$). We can repeat this process until we find a $\ell$ that matches $\Gamma^{\#}$. This terminates because there is a finite number of program locations.

There must then exist $\sigma_0^{\#}$ such that $(\sigma_0^{\#}, \Gamma^{\#}) = p^{\#}(\ell)$.

* If there is no Assûme, then by inverting apply, we know that $R$ is an assignment “$x := e$”. If there is also no Join, the path is empty. $\Gamma^{\#} = \Gamma'^{\#}, \Gamma = \Gamma'$ and $\sigma_1^{\#} = \sigma_0^{\#} [x \mapsto \text{subst}(e, \sigma_0^{\#})]$. Choosing $\sigma \triangleq [x \in \mathbb{L} \mapsto \hat{\mathcal{E}}[\sigma_0^{\#}(x)](\Gamma)]$ is then sufficient. It indeed verifies the compatibility with $\Gamma$, which, combined with the compatibility between $\Gamma'$ and $\sigma'$, implies $\sigma' = \sigma [x \mapsto \mathcal{E}[e](\sigma)]$ by compatibility between $\text{subst}$ and $\mathcal{E}[\cdot]$.

If there is a Join, the path is a single transition labelled by bindings: $\Gamma^{\#} \stackrel{B}{\rightleftharpoons} \Gamma'^{\#}$. We therefore have $\Gamma' \triangleq \text{unbind}_{\hat{\mathcal{E}}_{p^{\#}}}(\Gamma'^{\#}, \text{bind}(B, \Gamma))$. Furthermore, if we denote $\sigma_2^{\#} \triangleq \sigma_0^{\#} [x \mapsto \text{subst}(e, \sigma_0^{\#})]$ $\sigma_1^{\#}$ is equal to $\sigma_2^{\#}$ on the variables not in $\text{dom } B$ and renames those in $\text{dom } B$ to $x_{\Gamma'^{\#}}$. Note that $B$ maps these variables to their value in $\sigma_2^{\#}$. Therefore, for all $x$, $\hat{\mathcal{E}}[\sigma_1^{\#}(x)](\Gamma') = \hat{\mathcal{E}}[\sigma_2^{\#}(x)](\Gamma')$. So again, it is sufficient to choose $\sigma \triangleq [x \in \mathbb{L} \mapsto \hat{\mathcal{E}}[\sigma_0^{\#}(x)](\Gamma)]$ and $\sigma' \triangleq [x \in \mathbb{L} \mapsto \hat{\mathcal{E}}[\sigma_1^{\#}(x)](\Gamma)]$ to show the results.

* If there is an Assûme, then by inverting apply, we know that $R$ is a guard “If $e$”. If there is also no Join, the path is a single transition $\Gamma^{\#} \stackrel{e}{\rightleftharpoons} \Gamma'^{\#}$. This transition implies that $\Gamma = \Gamma'$, $\sigma_1^{\#} = \sigma_0^{\#}$ and $\hat{\mathcal{E}}[e](\Gamma) \neq 0$. Choosing $\sigma \triangleq [x \in \mathbb{L} \mapsto \hat{\mathcal{E}}[\sigma_0^{\#}(x)](\Gamma)]$ is then sufficient. It indeed verifies $\sigma = \sigma' \wedge \mathcal{E}[e](\sigma) \neq 0$ and the compatibility with $\Gamma$ by definition. If there is a Join, the path is made of two transitions:

$$ \Gamma^{\#} \stackrel{e}{\rightleftharpoons}_{\#} \text{Assûme}(e, \Gamma^{\#}) \stackrel{B}{\rightleftharpoons}_{\#} \Gamma'^{\#} $$

We therefore have $\Gamma' \triangleq \text{unbind}_{\hat{\mathcal{E}}_{p^{\#}}}(\Gamma'^{\#}, \text{bind}(B, \Gamma))$. Furthermore, $\sigma_1^{\#}$ is equal to $\sigma_0^{\#}$ on the variables not in $\text{dom } B$ and renames those in $\text{dom } B$ to $x_{\Gamma'^{\#}}$. Note that $B$ maps these variables to their value in $\sigma_0^{\#}$. Therefore, for all $x$, $\hat{\mathcal{E}}[\sigma_1^{\#}(x)](\Gamma') = \hat{\mathcal{E}}[\sigma_0^{\#}(x)](\Gamma)$. So again, it is sufficient to choose $\sigma \triangleq [x \in \mathbb{L} \mapsto \hat{\mathcal{E}}[\sigma_0^{\#}(x)](\Gamma)]$ to show the results. $\square$

**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 \mathcal{S}$ we have:

$$ (\Gamma^{\#}, \Gamma) \rightsquigarrow_{\hat{\mathcal{G}}_{p^{\#}}} (\Gamma'^{\#}, \Gamma') \wedge C(s', (\Gamma'^{\#}, \Gamma')) \Rightarrow \exists s \in \mathcal{S}, C(s, (\Gamma^{\#}, \Gamma)) \wedge s \to^{+}_{\mathcal{G}} s' $$

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

**PROOF.** Apply Lemma A.7 as many times as the input path is long, and compose the results. $\square$

## A.5 Proofs: SSA based numerical analysis

### Proof of Lemma 8.2:
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}_{\mathcal{G}}(\text{Lift}(\tilde{N})) = \pi(\text{analyse}_{C(\mathcal{G})}(\text{Lift}(\tilde{N}))) $$

First, let us define the $C$ transformation a bit more formally. We define $C_e$ a transformation that transforms an expression into a list of assignments and a simple expression (either a constant or a variable) as follows:

$$
\begin{array}{l@{\qquad}l}
C_e \in \mathcal{E} \to (L(\mathcal{X} \times \mathcal{E}) \times \mathcal{E}) & (L(X) \triangleq X^* \text{ is the set of finite lists of } X) \\
C_e(z) \triangleq ([], z) & \\
C_e(x) \triangleq ([], x) & \\
C_e(e_l \diamond e_r) \triangleq (a_l \mathrel{++} a_r \mathrel{++} [(y, x_l \diamond x_r)], y) & (++ \text{ is list concatenation}) \\
\phantom{C_e(e_l \diamond e_r) \triangleq} y \text{ is fresh, } (a_i, x_i) \triangleq C_e(e_i) & \\
C_e(e_c \ ? \ e_t : e_f) \triangleq (a_c \mathrel{++} a_t \mathrel{++} a_f \mathrel{++} [(y, x_c \ ? \ x_t : x_f)], y) & \\
\phantom{C_e(e_c \ ? \ e_t : e_f) \triangleq} y \text{ is fresh, } (a_i, x_i) \triangleq C_e(e_i) &
\end{array}
$$

From this compilation of expression, $C$ transforms full IMP programs by replacing every edge with a chain of edges, as generated $C_e$. All but the last edge of the chain are assignments, given by the list, and the last edge is the same as the original edge, but whose expression was replaced by the simple expression returned by $C_e$.

These definitions are meant to be close to those of Logozzo and Fähndrich [2008]. They are slightly adapted to better fit our model. We do not have two distinct language for source and target: our source is IMP and our target IMP but only using simple expressions (whose depth is at most 1).

PROOF. The gist of the proof is to show that all domain operations verify the property, assuming their argument do. The result is then obtained by structural induction.

We first show that applying a single relation, or applying the chain of relation from the compiled version will lead to the same state (after removing the new temporary variables).

All but the last relation in the state are assignments. By definition of Lift. apply, these do not modify the SSA state, only the mapping of IMP variables to program expressions. For the last operation, the expression is first transformed to an SSA expression via subst. This function will unfold the definition of all variables until it reaches a constant or an SSA expression, thus undoing the compilation transformation.

We know that subst will remove all introduced variables since the only variables it cannot simplify are those mapped to SSA variables. As it stands, SSA variables are only introduced if a variable is used before it is defined ($x_{entry}$ variable), or if a variable has different values in different branches of a join ($\phi$-variable, $x_{join}(\dots)$). Both cases cannot occur for the newly introduced variables since, by definition of $C_e$, it is clear that new variables are always defined before being used. Furthermore, new variables are only defined once, so they cannot appear in multiple branches of a join.

Thus evaluating (with subst) the full relation directly, or evaluating each assignment, then the compiled (simplified) expression will yield the same result. Furthermore, the SSA state in unchanged by evaluating the assignments, and only new variables in the variable store are changed. Hence, after removing the new temporary variables, both abstract states are the same.

To generalize this result, all we need is to show that the other domain operations (entry, join, widen) also verify this property. Lift($\tilde{N}$). entry doesn't depend on the input program graph, so it is always true. For the Lift($\tilde{N}$). join, notice that the SSA state is again unchanged in both versions, since it only depends on the parent SSA states, and the variables that differ in each branch. For the
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}_{\mathcal{G}}(\text{Lift}(\tilde{N})) = \pi(\text{analyse}_{C(\mathcal{G})}(\text{Lift}(\tilde{N}))) $$

First, let us define the $C$ transformation a bit more formally. We define $C_e$ a transformation that transforms an expression into a list of assignments and a simple expression (either a constant or a variable) as follows:

$$
\begin{array}{l@{\qquad}l}
C_e \in \mathcal{E} \to (L(\mathcal{X} \times \mathcal{E}) \times \mathcal{E}) & (L(X) \triangleq X^* \text{ is the set of finite lists of } X) \\
C_e(z) \triangleq ([], z) & \\
C_e(x) \triangleq ([], x) & \\
C_e(e_l \diamond e_r) \triangleq (a_l \mathrel{++} a_r \mathrel{++} [(y, x_l \diamond x_r)], y) & (++ \text{ is list concatenation}) \\
\qquad y \text{ is fresh, } (a_i, x_i) \triangleq C_e(e_i) & \\
C_e(e_c ? e_t : e_f) \triangleq (a_c \mathrel{++} a_t \mathrel{++} a_f \mathrel{++} [(y, x_c ? x_t : x_f)], y) \\
\qquad y \text{ is fresh, } (a_i, x_i) \triangleq C_e(e_i)
\end{array}
$$

From this compilation of expression, $C$ transforms full IMP programs by replacing every edge with a chain of edges, as generated $C_e$. All but the last edge of the chain are assignments, given by the list, and the last edge is the same as the original edge, but whose expression was replaced by the simple expression returned by $C_e$.

These definitions are meant to be close to those of Logozzo and Fähndrich [2008]. They are slightly adapted to better fit our model. We do not have two distinct language for source and target: our source is IMP and our target IMP but only using simple expressions (whose depth is at most 1).

PROOF. The gist of the proof is to show that all domain operations verify the property, assuming their argument do. The result is then obtained by structural induction.

We first show that applying a single relation, or applying the chain of relation from the compiled version will lead to the same state (after removing the new temporary variables).

All but the last relation in the state are assignments. By definition of Lift. apply, these do not modify the SSA state, only the mapping of IMP variables to program expressions. For the last operation, the expression is first transformed to an SSA expression via subst. This function will unfold the definition of all variables until it reaches a constant or an SSA expression, thus undoing the compilation transformation.

We know that subst will remove all introduced variables since the only variables it cannot simplify are those mapped to SSA variables. As it stands, SSA variables are only introduced if a variable is used before it is defined ($x_{entry}$ variable), or if a variable has different values in different branches of a join ($\phi$-variable, $x_{join}(\dots)$). Both cases cannot occur for the newly introduced variables since, by definition of $C_e$, it is clear that new variables are always defined before being used. Furthermore, new variables are only defined once, so they cannot appear in multiple branches of a join.

Thus evaluating (with subst) the full relation directly, or evaluating each assignment, then the compiled (simplified) expression will yield the same result. Furthermore, the SSA state in unchanged by evaluating the assignments, and only new variables in the variable store are changed. Hence, after removing the new temporary variables, both abstract states are the same.

To generalize this result, all we need is to show that the other domain operations (entry, join, widen) also verify this property. Lift($\tilde{N}$). entry doesn't depend on the input program graph, so it is always true. For the Lift($\tilde{N}$). join, notice that the SSA state is again unchanged in both versions, since it only depends on the parent SSA states, and the variables that differ in each branch. For the
variable store, the join only keeps common variables, leaving them unchanged if they are equal in all branches, and introducing a new variable if not. As argued above, new variables are only introduced for original program variables. Thus removing the extra variables doesn't affect them and maintains the property.

Finally, the Lift($\tilde{N}$). widen is called at the same places on both graphs. It only affects the SSA state (which is the same in both graph), and only renames the newly introduced variables in the store (which are all variables from the original IMP program). Therefore, it also verifies the property.

Since all domain operations yield the same state (after stripping extra variables) when run directly or run on the compiled version, it stands to reason that the full analysis (result of a finite number of applications of such domain operations) also has this property. □

## B USING AN ORDER RELATION TO REACH A POST FIXED POINT

For our analysis in Section 3.3, the hypothesis WIDENVALID requires our domains widening to converge to a true fixed-point. Often in abstract interpretation, we relax that hypothesis to a post fixed-point. To do so, we need a new domain function, a pre-order relation on $\Sigma^#$:

$$ \sqsubseteq \in \mathcal{P}(\Sigma^# \times \Sigma^#) $$

It should be compatible with the domain order: $\forall s^# t^#, s^# \sqsubseteq t^# \Rightarrow \gamma(s^#) \sqsubseteq \gamma(t^#)$. We extend $\sqsubseteq$ to a relation on $\Sigma^# \perp$ by having $\perp$ be a minimal element.

With this, we can weaken WIDENVALID to simply say the sequence $t_{n+1}^# \triangleq \text{widen}(\ell, t_n^#, s_n^#)$ reaches a post-fixed point in finite time: $\exists n, t_{n+1}^# \sqsubseteq t_n^#$. However, to prove convergence we now need monotony hypotheses for two reasons:

* To ensure that once we will keep decreasing after we reach a post fixed point ($p_{n+1}^# \sqsubseteq p_n^#$), and so can stop at any time after that.

* To ensure that non widening points converge, since otherwise it is possible that although $p_n^#$ decreases on the widening points, it does not do so on non-widening points.

Overall, this leads to a weaker hypothesis on widen, but requires stronger hypotheses on apply and join:

$$ \forall s^# t^# R, \quad s^# \sqsubseteq t^# \Rightarrow \text{apply}(R, s^#) \sqsubseteq \text{apply}(R, t^#) \qquad (\text{APPLYMONOTONE}) $$

$$ \forall S^# T^#, \quad (\forall s^# \in S^#, \exists t^# \in T^#, s^# \sqsubseteq t^#) \Rightarrow \text{join}(S^#) \sqsubseteq \text{join}(T^#) \qquad (\text{JOINMONOTONE}) $$

## C PERFORMING FEWER WIDENINGS USING WIDENING EDGES

### C.1 Definition of widening edges

Since widening (calling widen) can lead to loss of precision, we want to do so as little as possible. As defined the analysis (Section 3.3) calls widen on all loop heads. This notably includes heads of unreachable loops. To avoid this, a simple improvement is to only widen at $\ell \in W$ if one of its predecessors is not $\perp$.

While we are considering predecessors, we can do even better by limiting widening to predecessors coming from inside the loop. Indeed, it is possible that the analysis detects that one edge of the loop is not taken. This is especially possible with transformation functors (Section 5) and numerical analysis (Section 5.3). This is expresses by having the corresponding apply evaluate to $\perp$. In that case, the loop is already broken: we have no need to widen at the head.

To take advantage of this fact, we replace our set of widening points W with a set of widening edges $U \in \mathcal{P}(\mathbb{L} \times \mathbb{R} \times \mathbb{L})$. Formally, this is a subset of the program graph $\mathcal{G}$ that should contain at least one edge in every looping path. In practice, we use the weak topological order [Bourdoncle 1993] and define U as the set of edges returning to a component head from inside said component.
variable store, the join only keeps common variables, leaving them unchanged if they are equal in all branches, and introducing a new variable if not. As argued above, new variables are only introduced for original program variables. Thus removing the extra variables doesn't affect them and maintains the property.

Finally, the Lift($\tilde{N}$). widen is called at the same places on both graphs. It only affects the SSA state (which is the same in both graph), and only renames the newly introduced variables in the store (which are all variables from the original IMP program). Therefore, it also verifies the property.

Since all domain operations yield the same state (after stripping extra variables) when run directly or run on the compiled version, it stands to reason that the full analysis (result of a finite number of applications of such domain operations) also has this property. □

## B USING AN ORDER RELATION TO REACH A POST FIXED POINT

For our analysis in Section 3.3, the hypothesis WIDENVALID requires our domains widening to converge to a true fixed-point. Often in abstract interpretation, we relax that hypothesis to a post fixed-point. To do so, we need a new domain function, a pre-order relation on $\Sigma^#$:

$$ \sqsubseteq \in \mathcal{P}(\Sigma^# \times \Sigma^#) $$

It should be compatible with the domain order: $\forall s^# t^#, s^# \sqsubseteq t^# \Rightarrow \gamma(s^#) \sqsubseteq \gamma(t^#)$. We extend $\sqsubseteq$ to a relation on $\Sigma^# \perp$ by having $\perp$ be a minimal element.

With this, we can weaken WIDENVALID to simply say the sequence $t_{n+1}^# \triangleq widen(\ell, t_n^#, s_n^#)$ reaches a post-fixed point in finite time: $\exists n, t_{n+1}^# \sqsubseteq t_n^#$. However, to prove convergence we now need monotony hypotheses for two reasons:

* To ensure that once we will keep decreasing after we reach a post fixed point ($p_{n+1}^# \sqsubseteq p_n^#$), and so can stop at any time after that.

* To ensure that non widening points converge, since otherwise it is possible that although $p_n^#$ decreases on the widening points, it does not do so on non-widening points.

Overall, this leads to a weaker hypothesis on widen, but requires stronger hypotheses on apply and join:

$$ \forall s^# t^# R, \quad s^# \sqsubseteq t^# \Rightarrow \mathit{apply}(R, s^#) \sqsubseteq \mathit{apply}(R, t^#) \qquad (\mathit{APPLY} \mathit{MONOTONE}) $$

$$ \forall S^# T^#, \quad (\forall s^# \in S^#, \exists t^# \in T^#, s^# \sqsubseteq t^#) \Rightarrow \mathit{join}(S^#) \sqsubseteq \mathit{join}(T^#) \qquad (\mathit{JOIN} \mathit{MONOTONE}) $$

## C PERFORMING FEWER WIDENINGS USING WIDENING EDGES

### C.1 Definition of widening edges

Since widening (calling widen) can lead to loss of precision, we want to do so as little as possible. As defined the analysis (Section 3.3) calls widen on all loop heads. This notably includes heads of unreachable loops. To avoid this, a simple improvement is to only widen at $\ell \in W$ if one of its predecessors is not $\perp$.

While we are considering predecessors, we can do even better by limiting widening to predecessors coming from inside the loop. Indeed, it is possible that the analysis detects that one edge of the loop is not taken. This is especially possible with transformation functors (Section 5) and numerical analysis (Section 5.3). This is expresses by having the corresponding apply evaluate to $\perp$. In that case, the loop is already broken: we have no need to widen at the head.

To take advantage of this fact, we replace our set of widening points W with a set of widening edges $U \in \mathcal{P}(\mathbb{L} \times \mathbb{R} \times \mathbb{L})$. Formally, this is a subset of the program graph $\mathcal{G}$ that should contain at least one edge in every looping path. In practice, we use the weak topological order [Bourdoncle 1993] and define U as the set of edges returning to a component head from inside said component.
This choice is not only practical, it is also optimal. Indeed, if the analysis detects a false edge, all subsequent loop locations will be unreachable (⊥). So, if any edge of the loop is eliminated, then the last edge will also be eliminated.

With this new set, we can define a new widening operator:

$$ p^{\#} \nabla_U q^{\#} \triangleq \begin{array}{l} \ell \mapsto \textit{widen}(\ell, p^{\#}(\ell), q^{\#}(\ell)) \quad \text{if } \exists \ell', (\ell', R, \ell) \in U \land \textit{apply}(R, p^{\#}(\ell')) \neq \bot \\ \mid \ell \mapsto q^{\#}(\ell) \quad \text{otherwise} \end{array} $$

Here, the condition for widening is more complex than that of $\nabla_W$. We only widen if we are at the end point of a widening edge (($\ell'$, R, $\ell$) ∈ U) and that edge is taken (apply(R, $p^{\#}(\ell')$) ≠ ⊥).

## C.2 Ensuring convergence

With this definition, we can still prove soundness (Lemma A.3) and completeness (Lemma A.3) fairly easily, but termination (Lemma A.1) is harder. Indeed, the set of widening points is no longer fixed. It might vary across iterations.

Increasing it is fine: if we can prove that once we start widening at a given point we always will, we can still show convergence. This is because in that case, the set of widening points is increasing across iterations, and bounded by the finite set of points that appear in U. Thus, it converges and the proof from Lemma A.1 still works.

**LEMMA C.1 (MONOTONE CASE).** If our transfer functions *apply* and *join* are monotone (verify *APPLYMONOTONE* and *JOINMONOTONE*), then the set of widening points is monotone.

**PROOF.** Start by proving that for all $n$, we have $\forall \ell, p_n^\#(\ell) \sqsubseteq p_{n+1}^\#(\ell)$. This can be done by strong induction on $n$.

* For $n = 0$, consider the case $\ell \neq \ell_0$. Then $p_0^\#(\ell) = \bot$, which is a minimal element. For the $\ell_0$ case, we have $p_1^\#(\ell_0) = \textit{entry} = p_0^\#(\ell_0)$.

* For the induction case, we can have $p_{n-1}^\#(\ell) \sqsubseteq p_n^\#(\ell)$ by induction hypothesis.

- If we widen at $\ell$ at $n+1$, the result is given by *WSOUND*.

- If there is no widening the result is shown by monotonicity of $\mathcal{F}_g$, immediate given *APPLYMONOTONE* and *JOINMONOTONE*.

- We cannot widen at step $n$ but not $n+1$. Otherwise, there exists $\ell'$ such that $(\ell', R, \ell) \in U$ (does not depend on $n$); $p_{n-1}^\#(\ell') \neq \bot$ (also true at $n$ since $p_{n-1}^\#(\ell') \sqsubseteq p_n^\#(\ell')$ by induction and $\bot$ is minimal); and *apply*($R$, $p_n^\#(\ell')$) $\neq \bot$ (also true at $n$ since *apply* is monotone and the same reasoning as the previous point). Thus, we will also widen at step $n+1$.

Repeat the reasoning of the last point to show that $\forall n \ell, p_n^\#(\ell) \sqsubseteq p_{n+1}^\#(\ell)$ implies the lemma. □

**Non-monotone non-convergence.** For the non-monotone case, we can find examples of non-convergence. For instance, consider the interval domain of Section 3.4. We could define non-monotone transfer functions. Consider this function for the + operator:

$$ \begin{aligned} [1:1] \bar{\mp} [1:1] &= [1:4] \\ [1:+\infty] \bar{\mp} [1:1] &= [2:+\infty] \not\sqsubseteq [1:4] \end{aligned} $$

Combine with edge elimination for false guards, this can lead to non-convergence. An example of such a program is given in Figure 14. The analysis will not converge since will alternate between widening at point 1, which leads to a more precise value at point 2, which leads to not considering the widening-edge 2 → 1, so no longer widening at 1, which leads to imprecision at point 2 which fails to eliminate the back edges...
This choice is not only practical, it is also optimal. Indeed, if the analysis detects a false edge, all subsequent loop locations will be unreachable (⊥). So, if any edge of the loop is eliminated, then the last edge will also be eliminated.

With this new set, we can define a new widening operator:

$$p^{\#} \nabla_U q^{\#} \triangleq \begin{array}{l} \ell \mapsto \textit{widen}(\ell, p^{\#}(\ell), q^{\#}(\ell)) \quad \text{if } \exists \ell', (\ell', R, \ell) \in U \land \textit{apply}(R, p^{\#}(\ell')) \neq \bot \\ \mid \ell \mapsto q^{\#}(\ell) \quad \text{otherwise} \end{array}$$

Here, the condition for widening is more complex than that of $\nabla_W$. We only widen if we are at the end point of a widening edge (($\ell'$, R, $\ell$) ∈ U) and that edge is taken (apply(R, $p^{\#}(\ell')$) ≠ ⊥).

## C.2 Ensuring convergence

With this definition, we can still prove soundness (Lemma A.3) and completeness (Lemma A.3) fairly easily, but termination (Lemma A.1) is harder. Indeed, the set of widening points is no longer fixed. It might vary across iterations.

Increasing it is fine: if we can prove that once we start widening at a given point we always will, we can still show convergence. This is because in that case, the set of widening points is increasing across iterations, and bounded by the finite set of points that appear in U. Thus, it converges and the proof from Lemma A.1 still works.

**LEMMA C.1 (MONOTONE CASE).** If our transfer functions *apply* and *join* are monotone (verify *APPLYMONOTONE* and *JOINMONOTONE*), then the set of widening points is monotone.

**PROOF.** Start by proving that for all $n$, we have $\forall \ell, p_n^\#(\ell) \sqsubseteq p_{n+1}^\#(\ell)$. This can be done by strong induction on $n$.

* For $n = 0$, consider the case $\ell \neq \ell_0$. Then $p_0^\#(\ell) = \bot$, which is a minimal element. For the $\ell_0$ case, we have $p_1^\#(\ell_0) = \textit{entry} = p_0^\#(\ell_0)$.

* For the induction case, we can have $p_{n-1}^\#(\ell) \sqsubseteq p_n^\#(\ell)$ by induction hypothesis.

- If we widen at $\ell$ at $n+1$, the result is given by *WSOUND*.

- If there is no widening the result is shown by monotonicity of $\mathcal{F}_g$, immediate given *APPLYMONOTONE* and *JOINMONOTONE*.

- We cannot widen at step $n$ but not $n+1$. Otherwise, there exists $\ell'$ such that $(\ell', R, \ell) \in U$ (does not depend on $n$); $p_{n-1}^\#(\ell') \neq \bot$ (also true at $n$ since $p_{n-1}^\#(\ell') \sqsubseteq p_n^\#(\ell')$ by induction and $\bot$ is minimal); and *apply*($R$, $p_n^\#(\ell')$) $\neq \bot$ (also true at $n$ since *apply* is monotone and the same reasoning as the previous point). Thus, we will also widen at step $n+1$.

Repeat the reasoning of the last point to show that $\forall n \ell, p_n^\#(\ell) \sqsubseteq p_{n+1}^\#(\ell)$ implies the lemma. □

**Non-monotone non-convergence.** For the non-monotone case, we can find examples of non-convergence. For instance, consider the interval domain of Section 3.4. We could define non-monotone transfer functions. Consider this function for the $+$ operator:

$$ \begin{aligned} [1:1] \bar{\vee} [1:1] &= [1:4] \\ [1:+\infty] \bar{\vee} [1:1] &= [2:+\infty] \bar{\vee} [1:4] \end{aligned} $$

Combine with edge elimination for false guards, this can lead to non-convergence. An example of such a program is given in Figure 14. The analysis will not converge since will alternate between widening at point 1, which leads to a more precise value at point 2, which leads to not considering the widening-edge 2 → 1, so no longer widening at 1, which leads to imprecision at point 2 which fails to eliminate the back edges...
<figure><img src="image_9.png" /><figcaption>Fig. 14. Example of non-convergence for non-monotone programs</figcaption></figure>

*Forcing monotony.* One workaround is to force the monotony of the set of widening points. We remember the points where we widened in previous iteration and keep widening there. Formally, we define the analysis no longer just on a function $p^\#$, but on a pair $(p^\#, L)$ where $L \in \mathcal{P}(\mathsf{L})$, starting at $(p_0^\#, \emptyset)$. The transfer function just applies $\mathcal{F}_g$ to the first component. For the widening change the condition in $\nabla_U$ to “... $\lor \ell \in L$”, and change $L$ to the set of points where we widened.

### C.3 Performance cost of widening edges

The new widening operator $\nabla_U$ can be computed with almost the same complexity as $\nabla_W$. Indeed, the *apply*($R, p^\#(\ell')$) $\neq \perp$ part of the condition is already computed in $\mathcal{F}_g$. By memorizing the points for which this is true, we can evaluate the widening condition by simply testing, for each of these predecessors, if they correspond to a widening edge. This means we have replaced one set lookup per point $\ell$ (check if $\ell \in W$) to multiple set lookups (for all predecessors $\ell'$, check if $(\ell', R, \ell) \in U$). Thus added complexity comes from points which have lots of predecessors, or loops with many paths returning to the head (e.g. loops with *continue* statements, which can lead to $U$ being much larger than $W$). In most programs, both of these will be bounded by reasonable constants.

Another performance lost comes from slower convergence. Since we only widen when we find a loop, we need to propagate through each loop at least twice to ensure convergence. Once before widening, and once more after (since widening likely changes the loop head). This wasn't a problem with widening points since we always widened at the head, and thus avoided the first pre-widening pass.

Received 2023-11-16; accepted 2024-03-31
<figure><img src="image_11.png" /><figcaption>Fig. 14. Example of non-convergence for non-monotone programs</figcaption></figure>

*Forcing monotony.* One workaround is to force the monotony of the set of widening points. We remember the points where we widened in previous iteration and keep widening there. Formally, we define the analysis no longer just on a function $p^\#$, but on a pair $(p^\#, L)$ where $L \in \mathcal{P}(\mathcal{L})$, starting at $(p_0^\#, \emptyset)$. The transfer function just applies $\mathcal{F}_g$ to the first component. For the widening change the condition in $\nabla_U$ to “... $\lor \ell \in L$”, and change $L$ to the set of points where we widened.

### C.3 Performance cost of widening edges

The new widening operator $\nabla_U$ can be computed with almost the same complexity as $\nabla_W$. Indeed, the *apply*($R, p^\#(\ell')$) $\neq \perp$ part of the condition is already computed in $\mathcal{F}_g$. By memorizing the points for which this is true, we can evaluate the widening condition by simply testing, for each of these predecessors, if they correspond to a widening edge. This means we have replaced one set lookup per point $\ell$ (check if $\ell \in W$) to multiple set lookups (for all predecessors $\ell'$, check if $(\ell', R, \ell) \in U$). Thus added complexity comes from points which have lots of predecessors, or loops with many paths returning to the head (e.g. loops with *continue* statements, which can lead to *U* being much larger than *W*). In most programs, both of these will be bounded by reasonable constants.

Another performance lost comes from slower convergence. Since we only widen when we find a loop, we need to propagate through each loop at least twice to ensure convergence. Once before widening, and once more after (since widening likely changes the loop head). This wasn't a problem with widening points since we always widened at the head, and thus avoided the first pre-widening pass.

Received 2023-11-16; accepted 2024-03-31