One of the benefits of SSA form is that it allows more efficient *sparse* static analyses [Choi et al. 1991] (see, e.g., Tavares et al. [2014] for partitioned per variable analyses, and Mirliaz and Pichardie [2022] for analyses using relational domains). *Combining our SSA domain with a sparse analysis allows performing sparse analyses simultaneously with the SSA translation, and integrating sparse analyses in a standard* [Blanchet et al. 2002; Blazy et al. 2017; Journault et al. 2019] *abstract interpretation framework*. Several work [Lerner et al. 2002; Ramsey et al. 2010; Rompf 2012] have shown that changing the program syntax is useful to communicate between abstract domains; our work allows seeing this as reduced products [Cousot and Cousot 1979] with the SSA abstract domain.

The need for static analyses and, in particular, memory, pointer or alias analyses to improve the precision of SSA is well-known. This requirement is very important, for instance, when the SSA form is used to generate logic formulas to an SMT solver [Clarke et al. 2004; Gurfinkel et al. 2015] to increase precision and decrease solving time. Static analyses are even indispensable for programs where the control-flow is not known in advance because usual SSA translations require a CFG (e.g., to compute dominance frontiers). In particular, this is the case when analyzing machine code, i.e. when doing decompilation [Brumley et al. 2013] to SSA, which is a popular target for decompilation [Van Emmerik 2007; Yadavalli and Smith 2019]. Precisely recovering control-flow in machine code requires doing control-flow and value analysis simultaneously [Bardin et al. 2011; Kinder et al. 2009]; and SSA is a good intermediate representation to do this value analysis. To deal with this phase ordering problem, Van Emmerik [2007] used a simple but inefficient method consisting in redoing the whole SSA decompilation every time an indirect jump target is discovered in a function. *Doing SSA translation as an abstract interpretation solves these phase ordering problems: we can use the incrementally built (Section 6) SSA representation to help the memory, numeric, or control-flow analyses that improve or are necessary to build the SSA representation.*

Outside SSA, is it well-known that symbolic domains can be used to improve the precision of abstract domains [Gange et al. 2016; Miné 2006], and our symbolic expression domain can be used for the same purpose (e.g., to detect equalities between variables that would be missed by numerical domains). Finally, Cousot and Cousot [2002] explains how abstract interpretation can help design and prove correct program transformations, and discusses the possibility of doing some transformations, like constant propagation and dead code elimination, using dataflow analysis.

# 9 CONCLUSION

SSA translation is not only a program transformation; it is the result of a static analysis based on abstract interpretation. This analysis has two parts: symbolic expression analysis, which maps program variables to symbolic expressions; and SSA graph creation, which expresses how the symbolic variables in the symbolic expressions change according to the control flow. The symbolic expression analysis (that also does a global value numbering) relates the SSA program graph to the original program graph by providing a strong homomorphism, a relation that implies bisimulation. Due to this bisimulation, the SSA-translation domain computes an abstraction of the original program which is both sound and complete. Furthermore, we can modify the analysis so that all intermediate abstractions are also complete. This static analysis can be done using relatively standard dataflow frameworks, which allows combination [Cousot and Cousot 1979] with other abstract domains. We explained, in this paper, how numerical abstract domains can strengthen the symbolic expression analysis and SSA abstractions, notably by detecting dead transitions or more equalities between symbolic expressions. Using a reduced product, we can build optimizing transformations from a source program to SSA in a single pass.

We have only sketched how the SSA abstraction can strengthen numerical abstract domains, and did not mention how the SSA abstraction can be combined with memory abstractions to do register promotion; these studies should be the target of future publications.
REFERENCES

Bowen Alpern, Mark N. Wegman, and F. Kenneth Zadeck. 1988. Detecting Equality of Variables in Programs. In *15th ACM Symposium on Principles of Programming Languages (POPL 1988)*. 1–11. https://doi.org/10.1145/73560.73561

Andrew W Appel. 1998a. *Modern compiler implementation in ML*. Cambridge University Press. https://doi.org/10.1017/CBO9780511811449

Andrew W. Appel. 1998b. SSA is Functional Programming. SIGPLAN Notices 33, 4 (apr 1998), 17–20. https://doi.org/10.1145/278283.278285

Zena M Ariola and Jan Willem Klop. 1996. Equational term graph rewriting. Fundamenta Informaticae 26, 3, 4 (1996), 207–240. https://doi.org/10.3233/FI-1996-263401

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

Sébastien Bardin, Philippe Herrmann, and Franck Védrine. 2011. Refinement-Based CFG Reconstruction from Unstructured Programs. In *12th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2011, Vol. 6538)*. Springer, 54–69. https://doi.org/10.1007/978-3-642-18275-4_6

Gilles Barthe, Delphine Demange, and David Pichardie. 2014. Formal Verification of an SSA-Based Middle-End for CompCert. ACM Trans. Program. Lang. Syst. 36, 1 (2014), 4:1–4:35. https://doi.org/10.1145/2579080

B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival. 2002. Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. *The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones* 2566 (Oct. 2002), 85–108. https://doi.org/10.1007/3-540-36377-7_5

Sandrine Blazy, David Bühler, and Boris Yakobowski. 2017. Structuring Abstract Interpreters Through State and Value Abstractions. In *18th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2017, Vol. 10145)*, Ahmed Bouajjani and David Monniaux (Eds.). Springer, 112–130. https://doi.org/10.1007/978-3-319-52234-0_7

François Bourdoncle. 1993. Efficient chaotic iteration strategies with widenings. In *Formal Methods in Programming and their Applications*. Springer, 128–141. https://doi.org/10.1007/BFb0039704

Martin Brain, Saurabh Joshi, Daniel Kroening, and Peter Schrammel. 2015. Safety Verification and Refutation by k-Invariants and k-Induction. In *Static Analysis (SAS 2015)*, Sandrine Blazy and Thomas Jensen (Eds.). Springer, 145–161. https://doi.org/10.1007/978-3-662-48288-9_9

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

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

David Brumley, JongHyup Lee, Edward J. Schwartz, and Maverick Woo. 2013. Native x86 Decompile Using Semantics-Preserving Structural Analysis and Iterative Control-Flow Structuring. In *22th USENIX Security Symposium. USENIX Association, 353–368*. https://www.usenix.org/conference/usenixsecurity13/technical-sessions/presentation/schwartz.

Sebastian Buchwald, Denis Lohner, and Sebastian Ullrich. 2016. Verified construction of static single assignment form. In *25th International Conference on Compiler Construction (CC 2016)*. ACM, 67–76. https://doi.org/10.1145/2892208.2892211

David Bühler, Pascal Cuoq, Boris Yakobowski, Matthieu Lemerre, André Maroneze, Valentin Perrelle, and Virgile Prevosto. 2017. *The EVA plug-in*. Technical Report. CEA LIST, Software Reliability Laboratory, Saclay, France, F-91191. https://frama-c.com/download/frama-c-eva-manual.pdf

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

Bor-Yuh Evan Chang and Xavier Rival. 2013. Modular Construction of Shape-Numeric Analyzers. In *Festschrift for Dave Schmidt (EPTCS, Vol. 129)*, Anindya Banerjee, Olivier Danvy, Kyung-Goo Doh, and John Hatcliff (Eds.). https://doi.org/10.48550/arXiv.1309.5138

Jong-Deok Choi, Ron Cytron, and Jeanne Ferrante. 1991. Automatic Construction of Sparse Data Flow Evaluation Graphs. In *18th ACM Symposium on Principles of Programming Languages (POPL 1991)*, David S. Wise (Ed.). 55–66. https://doi.org/10.1145/99583.99594

Edmund M. Clarke, Daniel Kroening, and Flavio Lerda. 2004. A Tool for Checking ANSI-C Programs. In *10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004)*, Kurt Jensen and Andreas Podelski (Eds.). Springer, 168–176. https://doi.org/10.1007/978-3-540-24730-2_15

Cliff Click. 1995. Global Code Motion / Global Value Mumbering. In *Conference on Programming Language Design and Implementation (PLDI 1995)*, David W. Wall (Ed.). ACM, 246–257. https://doi.org/10.1145/207110.207154

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

Bowen Alpern, Mark N. Wegman, and F. Kenneth Zadeck. 1988. Detecting Equality of Variables in Programs. In *15th ACM Symposium on Principles of Programming Languages (POPL 1988)*. 1–11. https://doi.org/10.1145/73560.73561

Andrew W Appel. 1998a. *Modern compiler implementation in ML*. Cambridge University Press. https://doi.org/10.1017/CBO9780511811449

Andrew W. Appel. 1998b. SSA is Functional Programming. SIGPLAN Notices 33, 4 (apr 1998), 17–20. https://doi.org/10.1145/278283.278285

Zena M Ariola and Jan Willem Klop. 1996. Equational term graph rewriting. Fundamenta Informaticae 26, 3, 4 (1996), 207–240. https://doi.org/10.3233/FI-1996-263401

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

Sébastien Bardin, Philippe Herrmann, and Franck Védrine. 2011. Refinement-Based CFG Reconstruction from Unstructured Programs. In *12th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2011, Vol. 6538)*. Springer, 54–69. https://doi.org/10.1007/978-3-642-18275-4_6

Gilles Barthe, Delphine Demange, and David Pichardie. 2014. Formal Verification of an SSA-Based Middle-End for CompCert. ACM Trans. Program. Lang. Syst. 36, 1 (2014), 4:1–4:35. https://doi.org/10.1145/2579080

B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival. 2002. Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. *The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones* 2566 (Oct. 2002), 85–108. https://doi.org/10.1007/3-540-36377-7_5

Sandrine Blazy, David Bühler, and Boris Yakobowski. 2017. Structuring Abstract Interpreters Through State and Value Abstractions. In *18th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2017, Vol. 10145)*, Ahmed Bouajjani and David Monniaux (Eds.). Springer, 112–130. https://doi.org/10.1007/978-3-319-52234-0_7

François Bourdoncle. 1993. Efficient chaotic iteration strategies with widenings. In *Formal Methods in Programming and their Applications*. Springer, 128–141. https://doi.org/10.1007/BFb0039704

Martin Brain, Saurabh Joshi, Daniel Kroening, and Peter Schrammel. 2015. Safety Verification and Refutation by k-Invariants and k-Induction. In *Static Analysis (SAS 2015)*, Sandrine Blazy and Thomas Jensen (Eds.). Springer, 145–161. https://doi.org/10.1007/978-3-662-48288-9_9

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

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

David Brumley, JongHyup Lee, Edward J. Schwartz, and Maverick Woo. 2013. Native x86 Decompile Using Semantics-Preserving Structural Analysis and Iterative Control-Flow Structuring. In *22th USENIX Security Symposium. USENIX Association, 353–368*. https://www.usenix.org/conference/usenixsecurity13/technical-sessions/presentation/schwartz.

Sebastian Buchwald, Denis Lohner, and Sebastian Ullrich. 2016. Verified construction of static single assignment form. In *25th International Conference on Compiler Construction (CC 2016)*. ACM, 67–76. https://doi.org/10.1145/2892208.2892211

David Bühler, Pascal Cuoq, Boris Yakobowski, Matthieu Lemerre, André Maroneze, Valentin Perrelle, and Virgile Prevosto. 2017. *The EVA plug-in*. Technical Report. CEA LIST, Software Reliability Laboratory, Saclay, France, F-91191. https://frama-c.com/download/frama-c-eva-manual.pdf

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

Bor-Yuh Evan Chang and Xavier Rival. 2013. Modular Construction of Shape-Numeric Analyzers. In *Festschrift for Dave Schmidt (EPTCS, Vol. 129)*, Anindya Banerjee, Olivier Danvy, Kyung-Goo Doh, and John Hatcliff (Eds.). https://doi.org/10.48550/arXiv.1309.5138

Jong-Deok Choi, Ron Cytron, and Jeanne Ferrante. 1991. Automatic Construction of Sparse Data Flow Evaluation Graphs. In *18th ACM Symposium on Principles of Programming Languages (POPL 1991)*, David S. Wise (Ed.). 55–66. https://doi.org/10.1145/99583.99594

Edmund M. Clarke, Daniel Kroening, and Flavio Lerda. 2004. A Tool for Checking ANSI-C Programs. In *10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004)*, Kurt Jensen and Andreas Podelski (Eds.). Springer, 168–176. https://doi.org/10.1007/978-3-540-24730-2_15

Cliff Click. 1995. Global Code Motion / Global Value Mumbering. In *Conference on Programming Language Design and Implementation (PLDI 1995)*, David W. Wall (Ed.). ACM, 246–257. https://doi.org/10.1145/207110.207154

Cliff Click and Keith D. Cooper. 1995. Combining Analyses, Combining Optimizations. ACM Trans. Program. Lang. Syst. 17, 2 (1995), 181–196. https://doi.org/10.1145/201059.201061
Cliff Click and Michael Paleczny. 1995. A simple graph-based intermediate representation. *ACM Sigplan Notices* 30, 3 (1995), 35-49. https://doi.org/10.1145/202530.202534

Keith D Cooper and Taylor Simpson. 1995. *SCC-Based Value Numbering*. Technical Report. Rice University.

Patrick Cousot. 1977. *Asynchronous iterative methods for solving a fixed point system of monotone equations in a complete lattice*. Technical Report. Laboratoire IMAG, Université scientifique et médicale de Grenoble, Grenoble, France. https://www.di.ens.fr/~cousot/publications.www/Cousot-IMAG-RR88-Sep-1977.pdf

Patrick Cousot. 1978. *Méthodes itératives de construction et d'approximation de points fixes d'opérateurs monotones sur un treillis, analyse sémantique de programmes (in French)*. Ph.D. Dissertation. Université Joseph Fourier, Grenoble, France. https://www.di.ens.fr/~cousot/publications.www/CousotTheseEsSciences1978.pdf

Patrick Cousot. 2002. Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. *Theor. Comput. Sci.* 277, 1-2 (2002), 47-103. https://doi.org/10.1016/S0304-3975(00)00313-3

Patrick Cousot and Radhia Cousot. 1977. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In *4th ACM Symposium on Principles of Programming Languages (POPL 1977)*. 238-252. https://doi.org/10.1145/512950.512973

Patrick Cousot and Radhia Cousot. 1979. Systematic design of program analysis frameworks. In *6th ACM Symposium on Principles of Programming Languages (POPL 1979)*. 269-282. https://doi.org/10.1145/567752.567778

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

Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. 2006. Combination of Abstractions in the ASTRÉE Static Analyzer. In *Revised Selected Papers from the 11th Asian Computing Science Conference on Advances in Computer Science - Secure Software and Related Issues - ASIAN 2006* (Lecture Notes in Computer Science, Vol. 4435). Springer, 272-300. https://doi.org/10.1007/978-3-540-77505-8_23

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

Jacobus Willem de Bakker and Lambert Meertens. 1975. On the Completeness of the Inductive Assertion Method. *J. Comput. Syst. Sci.* 11, 3 (1975), 323-357. https://doi.org/10.1016/S0022-0000(75)80056-0

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

Edsger W. Dijkstra. 1975. Guarded commands, nondeterminacy and formal derivation of programs. *Commun. ACM* 18, 8 (aug 1975), 453-457. https://doi.org/10.1145/360933.360975

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

Benjamin Farinier, Robin David, Sébastien Bardin, and Matthieu Lemerre. 2018. Arrays Made Simpler: An Efficient, Scalable and Thorough Preprocessing. In *22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-22, Vol. 57)*, Gilles Barthe, Geoff Sutcliffe, and Margus Veanes (Eds.). EasyChair, 363-380. https://doi.org/10.2900dc9b

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

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

Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, and Jorge A Navas. 2015. The SeaHorn verification framework. In *International Conference on Computer Aided Verification (CAV 2015)*. Springer, 343-361. https://doi.org/10.1007/978-3-319-21690-4_20

Sebastian Hack. 2016. SSA reconstruction (1st ed.), Chapter 5. In [Rastello 2016].

Julien Henry, David Monniaux, and Matthieu Moy. 2012. PAGAI: a path sensitive static analyzer. In *Tools for Automatic Program Analysis (TAPAS)*, Bertrand Jeannet (Ed.). https://doi.org/10.1016/j.entcs.2012.11.003

Hugo Illous, Matthieu Lemerre, and Xavier Rival. 2021. A relational shape abstract domain. *Formal Methods Syst. Des.* 57, 3 (2021), 343-400. https://doi.org/10.1007/s10703-021-00366-4

Matthieu Journault, Antoine Miné, Raphaël Monat, and Abdelraouf Ouadjaout. 2019. Combinations of Reusable Abstract Domains for a Multilingual Static Analyzer. In *11th International Conference on Verified Software Theories, Tools, and Experiments - Revised Selected Papers (VSTTE 2019, Vol. 12031)*, Supratik Chakraborty and Jorge A. Navas (Eds.). Springer, 1-18. https://doi.org/10.1007/978-3-030-41600-3_1
Cliff Click and Michael Paleczny. 1995. A simple graph-based intermediate representation. *ACM Sigplan Notices* 30, 3 (1995), 35-49. https://doi.org/10.1145/202530.202534

Keith D Cooper and Taylor Simpson. 1995. *SCC-Based Value Numbering*. Technical Report. Rice University.

Patrick Cousot. 1977. *Asynchronous iterative methods for solving a fixed point system of monotone equations in a complete lattice*. Technical Report. Laboratoire IMAG, Université scientifique et médicale de Grenoble, Grenoble, France. https://www.di.ens.fr/~cousot/publications.www/Cousot-IMAG-RR88-Sep-1977.pdf

Patrick Cousot. 1978. *Méthodes itératives de construction et d'approximation de points fixes d'opérateurs monotones sur un treillis, analyse sémantique de programmes (in French)*. Ph.D. Dissertation. Université Joseph Fourier, Grenoble, France. https://www.di.ens.fr/~cousot/publications.www/CousotTheseEsSciences1978.pdf

Patrick Cousot. 2002. Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. *Theor. Comput. Sci.* 277, 1-2 (2002), 47-103. https://doi.org/10.1016/S0304-3975(00)00313-3

Patrick Cousot and Radhia Cousot. 1977. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In *4th ACM Symposium on Principles of Programming Languages (POPL 1977)*. 238-252. https://doi.org/10.1145/512950.512973

Patrick Cousot and Radhia Cousot. 1979. Systematic design of program analysis frameworks. In *6th ACM Symposium on Principles of Programming Languages (POPL 1979)*. 269-282. https://doi.org/10.1145/567752.567778

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

Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. 2006. Combination of Abstractions in the ASTRÉE Static Analyzer. In *Revised Selected Papers from the 11th Asian Computing Science Conference on Advances in Computer Science - Secure Software and Related Issues - ASIAN 2006* (Lecture Notes in Computer Science, Vol. 4435). Springer, 272-300. https://doi.org/10.1007/978-3-540-77505-8_23

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

Jacobus Willem de Bakker and Lambert Meertens. 1975. On the Completeness of the Inductive Assertion Method. *J. Comput. Syst. Sci.* 11, 3 (1975), 323-357. https://doi.org/10.1016/S0022-0000(75)80056-0

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

Edsger W. Dijkstra. 1975. Guarded commands, nondeterminacy and formal derivation of programs. *Commun. ACM* 18, 8 (aug 1975), 453-457. https://doi.org/10.1145/360933.360975

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

Benjamin Farinier, Robin David, Sébastien Bardin, and Matthieu Lemerre. 2018. Arrays Made Simpler: An Efficient, Scalable and Thorough Preprocessing. In *22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-22, Vol. 57)*, Gilles Barthe, Geoff Sutcliffe, and Margus Veanes (Eds.). EasyChair, 363-380. https://doi.org/10.2900dc9b

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

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

Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, and Jorge A Navas. 2015. The SeaHorn verification framework. In *International Conference on Computer Aided Verification (CAV 2015)*. Springer, 343-361. https://doi.org/10.1007/978-3-319-21690-4_20

Sebastian Hack. 2016. SSA reconstruction (1st ed.), Chapter 5. In [*Rastello* 2016].

Julien Henry, David Monniaux, and Matthieu Moy. 2012. PAGAI: a path sensitive static analyzer. In *Tools for Automatic Program Analysis (TAPAS)*, Bertrand Jeannet (Ed.). https://doi.org/10.1016/j.entcs.2012.11.003

Hugo Illous, Matthieu Lemerre, and Xavier Rival. 2021. A relational shape abstract domain. *Formal Methods Syst. Des.* 57, 3 (2021), 343-400. https://doi.org/10.1007/s10703-021-00366-4

Matthieu Journault, Antoine Miné, Raphaël Monat, and Abdelraouf Ouadjaout. 2019. Combinations of Reusable Abstract Domains for a Multilingual Static Analyzer. In *11th International Conference on Verified Software Theories, Tools, and Experiments - Revised Selected Papers (VSTTE 2019, Vol. 12031)*, Supratik Chakraborty and Jorge A. Navas (Eds.). Springer, 1-18. https://doi.org/10.1007/978-3-030-41600-3_1
Richard Kelsey. 1995. A Correspondence between Continuation Passing Style and Static Single Assignment Form. In *Proceedings ACM SIGPLAN Workshop on Intermediate Representations (IR'95)*, Michael D. Ernst (Ed.). ACM, 13-23.
https://doi.org/10.1145/202529.202532

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

Johannes Kinder, Florian Zuleger, and Helmut Veith. 2009. An Abstract Interpretation-Based Framework for Control Flow Reconstruction from Binaries. In *Verification, Model Checking, and Abstract Interpretation (VMCAI 2009)*, Neil D. Jones and Markus Müller-Olm (Eds.). Springer, 214-228. https://doi.org/10.1007/978-3-540-93900-9_19

James C. King. 1976. Symbolic Execution and Program Testing. *Commun. ACM* 19, 7 (1976), 385-394. https://doi.org/10.1145/360248.360252

K.R.M. Leino. 2005. Efficient weakest preconditions. *Inform. Process. Lett.* 93, 6 (2005), 281-288. https://doi.org/10.1016/j.ipl.2004.10.015

Sorin Lerner, David Grove, and Craig Chambers. 2002. Composing dataflow analyses and transformations. In *29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2002)*, John Launchbury and John C. Mitchell (Eds.). ACM, 270-282. https://doi.org/10.1145/503272.503298

William Mansky and Elsa L. Gunter. 2010. A Framework for Formal Verification of Compiler Optimizations. In *1st International Conference on Interactive Theorem Proving - ITP 2010 (Lecture Notes in Computer Science, Vol. 6172)*, Matt Kaufmann and Lawrence C. Paulson (Eds.). Springer, 371-386. https://doi.org/10.1007/978-3-642-14052-5_26

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

Solène Mirliaz and David Pichardie. 2022. A Flow-Insensitive-Complete Program Representation. In *23rd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2022)*. https://doi.org/10.1007/978-3-030-94583-1_10

Greg Nelson. 1980. *Techniques for program verification*. Ph.D. Dissertation. Stanford University, CA, USA.

Olivier Nicole, Matthieu Lemerre, Sébastien Bardin, and Xavier Rival. 2021b. 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. 2021a. *Binsec/Codex, an abstract interpreter to verify safety and security properties of systems code*. Technical Report. https://binsec.github.io/assets/publications/papers/2021-rtas-technical-report-analysis.pdf

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

Chris Okasaki and Andrew Gill. 1998. Fast Mergeable Integer Maps. In *Workshop on ML*. 77-86.

Norman Ramsey, João Dias, and Simon L. Peyton Jones. 2010. Hoopl: a modular, reusable library for dataflow analysis and transformation. In *Proceedings of the 3rd ACM SIGPLAN Symposium on Haskell (Haskell 2010)*, Jeremy Gibbons (Ed.). ACM, 121-134. https://doi.org/10.1145/1863523.1863539

Fabrice Rastello. 2016. *SSA-based Compiler Design* (1st ed.). Springer Publishing Company, Incorporated.

John H. Reif and Harry R. Lewis. 1986. Efficient Symbolic Analysis of Programs. *J. Comput. Syst. Sci.* 32, 3 (1986), 280-314.
https://doi.org/10.1016/0022-0000(86)90031-0

John H. Reif and Robert Endre Tarjan. 1982. Symbolic Program Analysis in Almost-Linear Time. *SIAM J. Comput.* 11, 1 (1982), 81-93. https://doi.org/10.1137/0211007

Thomas Reinbacher and Jörg Brauer. 2011. Precise control flow reconstruction using boolean logic. In *11th International Conference on Embedded Software (EMSOFT 2011)*, Samarjit Chakraborty, Ahmed Jerraya, Sanjoy K. Baruah, and Sebastian Fischmeister (Eds.). ACM, 117-126. https://doi.org/10.1145/2038642.2038662

Thomas W. Reps, Shmuel Sagiv, and Greta Yorsh. 2004. Symbolic Implementation of the Best Transformer. In *5th International Conference on Verification, Model Checking, and Abstract Interpretation - VMCAI 2004 (Lecture Notes in Computer Science, Vol. 2937)*, Bernhard Steffen and Giorgio Levi (Eds.). Springer, 252-266. https://doi.org/10.1007/978-3-540-24622-0_21

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 *15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL 1988)*. 12-27. https://doi.org/10.1145/73560.73562

Oliver Rüthing, Jens Knoop, and Bernhard Steffen. 1999. Detecting Equalities of Variables: Combining Efficiency with Precision. In *6th Static Analysis Symposium – SAS ’99 (Lecture Notes in Computer Science, Vol. 1694)*, Agostino Cortesi and
Richard Kelsey. 1995. A Correspondence between Continuation Passing Style and Static Single Assignment Form. In *Proceedings ACM SIGPLAN Workshop on Intermediate Representations (IR'95)*, Michael D. Ernst (Ed.). ACM, 13-23.
https://doi.org/10.1145/202529.202532

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

Johannes Kinder, Florian Zuleger, and Helmut Veith. 2009. An Abstract Interpretation-Based Framework for Control Flow Reconstruction from Binaries. In *Verification, Model Checking, and Abstract Interpretation (VMCAI 2009)*, Neil D. Jones and Markus Müller-Olm (Eds.). Springer, 214-228. https://doi.org/10.1007/978-3-540-93900-9_19

James C. King. 1976. Symbolic Execution and Program Testing. *Commun. ACM* 19, 7 (1976), 385-394. https://doi.org/10.1145/360248.360252

K.R.M. Leino. 2005. Efficient weakest preconditions. *Inform. Process. Lett.* 93, 6 (2005), 281-288. https://doi.org/10.1016/j.ipl.2004.10.015

Sorin Lerner, David Grove, and Craig Chambers. 2002. Composing dataflow analyses and transformations. In *29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2002)*, John Launchbury and John C. Mitchell (Eds.). ACM, 270-282. https://doi.org/10.1145/503272.503298

William Mansky and Elsa L. Gunter. 2010. A Framework for Formal Verification of Compiler Optimizations. In *1st International Conference on Interactive Theorem Proving - ITP 2010 (Lecture Notes in Computer Science, Vol. 6172)*, Matt Kaufmann and Lawrence C. Paulson (Eds.). Springer, 371-386. https://doi.org/10.1007/978-3-642-14052-5_26

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

Solène Mirliaz and David Pichardie. 2022. A Flow-Insensitive-Complete Program Representation. In *23rd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2022)*. https://doi.org/10.1007/978-3-030-94583-1_10

Greg Nelson. 1980. *Techniques for program verification*. Ph.D. Dissertation. Stanford University, CA, USA.

Olivier Nicole, Matthieu Lemerre, Sébastien Bardin, and Xavier Rival. 2021b. 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. 2021a. *Binsec/Codex, an abstract interpreter to verify safety and security properties of systems code*. Technical Report. https://binsec.github.io/assets/publications/papers/2021-rtas-technical-report-analysis.pdf

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

Chris Okasaki and Andrew Gill. 1998. Fast Mergeable Integer Maps. In *Workshop on ML*. 77-86.

Norman Ramsey, João Dias, and Simon L. Peyton Jones. 2010. Hoopl: a modular, reusable library for dataflow analysis and transformation. In *Proceedings of the 3rd ACM SIGPLAN Symposium on Haskell (Haskell 2010)*, Jeremy Gibbons (Ed.). ACM, 121-134. https://doi.org/10.1145/1863523.1863539

Fabrice Rastello. 2016. *SSA-based Compiler Design* (1st ed.). Springer Publishing Company, Incorporated.

John H. Reif and Harry R. Lewis. 1986. Efficient Symbolic Analysis of Programs. *J. Comput. Syst. Sci.* 32, 3 (1986), 280-314.
https://doi.org/10.1016/0022-0000(86)90031-0

John H. Reif and Robert Endre Tarjan. 1982. Symbolic Program Analysis in Almost-Linear Time. *SIAM J. Comput.* 11, 1 (1982), 81-93. https://doi.org/10.1137/0211007

Thomas Reinbacher and Jörg Brauer. 2011. Precise control flow reconstruction using boolean logic. In *11th International Conference on Embedded Software (EMSOFT 2011)*, Samarjit Chakraborty, Ahmed Jerraya, Sanjoy K. Baruah, and Sebastian Fischmeister (Eds.). ACM, 117-126. https://doi.org/10.1145/2038642.2038662

Thomas W. Reps, Shmuel Sagiv, and Greta Yorsh. 2004. Symbolic Implementation of the Best Transformer. In *5th International Conference on Verification, Model Checking, and Abstract Interpretation - VMCAI 2004 (Lecture Notes in Computer Science, Vol. 2937)*, Bernhard Steffen and Giorgio Levi (Eds.). Springer, 252-266. https://doi.org/10.1007/978-3-540-24622-0_21

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 *15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL 1988)*. 12-27. https://doi.org/10.1145/73560.73562

Oliver Rüthing, Jens Knoop, and Bernhard Steffen. 1999. Detecting Equalities of Variables: Combining Efficiency with Precision. In *6th Static Analysis Symposium – SAS ’99 (Lecture Notes in Computer Science, Vol. 1694)*, Agostino Cortesi and
Gilberto Filé (Eds.). Springer, 232–247. https://doi.org/10.1007/3-540-48294-6_15

Davide Sangiorgi. 2009. On the origins of bisimulation and coinduction. *ACM Trans. Program. Lang. Syst.* 31, 4 (2009), 15:1–15:41. https://doi.org/10.1145/1516507.1516510

Sigurd Schneider. 2013. *Semantics of an Intermediate Language for Program Transformation*. Master’s thesis. Saarland University. https://www.ps.uni-saarland.de/~sdschn/msc.pdf

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

James Stanier. 2016. *Graphs and Gating Functions* (1st ed.), Chapter 14. In [Rastello 2016].

André Luiz Camargos Tavares, Benoit Boissinot, Fernando Magno Quintão Pereira, and Fabrice Rastello. 2014. Parameterized Construction of Program Representations for Sparse Dataflow Analyses. In *23rd International Conference on Compiler Construction – CC 2014 (Lecture Notes in Computer Science, Vol. 8409)*, Albert Cohen (Ed.). Springer, 18–39. https://doi.org/10.1007/978-3-642-54807-9_2

Michael James Van Emmerik. 2007. *Static single assignment for decompilation*. Ph.D. Dissertation. University of Queensland.

Mark N. Wegman and F. Kenneth Zadeck. 1991. *Constant Propagation with Conditional Branches*. *ACM Trans. Program. Lang. Syst.* 13, 2 (1991), 181–210. https://doi.org/10.1145/103135.103136

Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, and Pavel Panchekha. 2021. *egg: Fast and extensible equality saturation*. *Proc. ACM Program. Lang.* 5, POPL (2021), 1–29. https://doi.org/10.1145/3434304

S. Bharadwaj Yadavalli and Aaron Smith. 2019. Raising binaries to LLVM IR with MCTOLL (WIP paper). In *20th ACM SIGPLAN/SIGBED International Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES 2019)*, Jian-Jia Chen and Aviral Shrivastava (Eds.). 213–218. https://doi.org/10.1145/3316482.3326354

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

Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic. 2012. Formalizing the LLVM intermediate representation for verified program transformations. In *39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2012)*, John Field and Michael Hicks (Eds.). 427–440. https://doi.org/10.1145/2103656.2103709

# A SOUNDNESS OF THE SYMBOLIC EXPRESSION ANALYSIS

While the description of the symbolic expression analysis (performing global value numbering) is sufficiently simple that its complete description fits in Figure 4, the soundness proof is more complex. This soundness proof is interesting in that it shows that the interpretation of instruction is very precise, and that approximations only come from the join operation (for which the soundness is more involved).

## A.1 Soundness and completeness of abstract evaluation of instructions

For the analysis of instructions we prove a stronger version of the usual soundness theorem, where the argument and result of transfer functions are related using the same valuation $\Gamma$.

**LEMMA A.1 (STRONG SOUNDNESS AND COMPLETENESS OF $\mathcal{E}^{\#}[\llbracket \cdot \rrbracket]$).** Let $\sigma^{\#} \in \Sigma^{\#}$, $e$ an expression. Let $\Gamma \mapsto \sigma \in \gamma_{\Sigma^{\#}}(\sigma^{\#})$, i.e. $\Gamma$ and $\sigma$ are such that $\sigma = \gamma_{\Sigma^{\#}}(\sigma^{\#})[\Gamma]$. Then:

$$ \mathcal{E}[\llbracket e \rrbracket](\sigma) = \mathcal{E}[\mathcal{E}^{\#}[\llbracket e \rrbracket](\sigma^{\#})](\Gamma) $$

**PROOF.** By structural induction on $e$, using the hypothesis that $\forall x, \sigma[x] = \mathcal{E}[\sigma^{\#}[x]](\Gamma)$ for the base variable case. $\square$

**Example A.2.** Let $\sigma^{\#} = [x \mapsto (2+x_{\ell_0})]$, $\Gamma = [x_{\ell_0} \mapsto 7]$, and $\sigma = [x \mapsto 9]$. We have $\sigma = \gamma_{\Sigma^{\#}}(\sigma^{\#})[\Gamma]$.

* $\mathcal{E}^{\#}[1+x](\sigma^{\#}) = \text{subst}(1+x, \sigma^{\#}) = 1+(2+x_{\ell_0})$. We have $\mathcal{E}[1+(2+x_{\ell_0})](\Gamma) = 10$.

* $\mathcal{E}^{\#}[1+x](\sigma) = 1+9=10$.

**LEMMA A.3 (STRONG SOUNDNESS OF $\mathcal{I}^{\#}[\llbracket \cdot \rrbracket]$).** Let $\sigma^{\#} \in \Sigma^{\#}$, $i$ an instruction. Let $\Gamma \mapsto \sigma \in \gamma_{\Sigma^{\#}}(\sigma^{\#})$, i.e. $\Gamma$ and $\sigma$ are such that $\sigma = \gamma_{\Sigma^{\#}}(\sigma^{\#})[\Gamma]$. Then:
Gilberto Filé (Eds.). Springer, 232–247. https://doi.org/10.1007/3-540-48294-6_15

Davide Sangiorgi. 2009. On the origins of bisimulation and coinduction. *ACM Trans. Program. Lang. Syst.* 31, 4 (2009), 15:1–15:41. https://doi.org/10.1145/1516507.1516510

Sigurd Schneider. 2013. *Semantics of an Intermediate Language for Program Transformation*. Master’s thesis. Saarland University. https://www.ps.uni-saarland.de/~sdschn/msc.pdf

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

James Stanier. 2016. *Graphs and Gating Functions* (1st ed.), Chapter 14. In [Rastello 2016].

André Luiz Camargos Tavares, Benoit Boissinot, Fernando Magno Quintão Pereira, and Fabrice Rastello. 2014. Parameterized Construction of Program Representations for Sparse Dataflow Analyses. In *23rd International Conference on Compiler Construction – CC 2014 (Lecture Notes in Computer Science, Vol. 8409)*, Albert Cohen (Ed.). Springer, 18–39. https://doi.org/10.1007/978-3-642-54807-9_2

Michael James Van Emmerik. 2007. *Static single assignment for decompilation*. Ph.D. Dissertation. University of Queensland.

Mark N. Wegman and F. Kenneth Zadeck. 1991. *Constant Propagation with Conditional Branches*. *ACM Trans. Program. Lang. Syst.* 13, 2 (1991), 181–210. https://doi.org/10.1145/103135.103136

Max Willsey, Chandrakana Nandi, Yisu Remy Wang, Oliver Flatt, Zachary Tatlock, and Pavel Panchekha. 2021. *egg: Fast and extensible equality saturation*. *Proc. ACM Program. Lang.* 5, POPL (2021), 1–29. https://doi.org/10.1145/3434304

S. Bharadwaj Yadavalli and Aaron Smith. 2019. Raising binaries to LLVM IR with MCTOLL (WIP paper). In *20th ACM SIGPLAN/SIGBED International Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES 2019)*, Jian-Jia Chen and Aviral Shrivastava (Eds.). 213–218. https://doi.org/10.1145/3316482.3326354

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

Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic. 2012. Formalizing the LLVM intermediate representation for verified program transformations. In *39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2012)*, John Field and Michael Hicks (Eds.). 427–440. https://doi.org/10.1145/2103656.2103709

# A SOUNDNESS OF THE SYMBOLIC EXPRESSION ANALYSIS

While the description of the symbolic expression analysis (performing global value numbering) is sufficiently simple that its complete description fits in Figure 4, the soundness proof is more complex. This soundness proof is interesting in that it shows that the interpretation of instruction is very precise, and that approximations only come from the join operation (for which the soundness is more involved).

## A.1 Soundness and completeness of abstract evaluation of instructions

For the analysis of instructions we prove a stronger version of the usual soundness theorem, where the argument and result of transfer functions are related using the same valuation $\Gamma$.

**LEMMA A.1 (STRONG SOUNDNESS AND COMPLETENESS OF $\mathcal{E}^{\#}[\llbracket \cdot \rrbracket]$).** Let $\sigma^{\#} \in \Sigma^{\#}$, $e$ an expression. Let $\Gamma \mapsto \sigma \in \gamma_{\Sigma^{\#}}(\sigma^{\#})$, i.e. $\Gamma$ and $\sigma$ are such that $\sigma = \gamma_{\Sigma^{\#}}(\sigma^{\#})[\Gamma]$. Then:

$$ \mathcal{E}[\llbracket e \rrbracket](\sigma) = \mathcal{E}[\mathcal{E}^{\#}[\llbracket e \rrbracket](\sigma^{\#})](\Gamma) $$

**PROOF.** By structural induction on $e$, using the hypothesis that $\forall x, \sigma[x] = \mathcal{E}[\sigma^{\#}[x]](\Gamma)$ for the base variable case. $\square$

*Example A.2.* Let $\sigma^{\#} = [x \mapsto (2+x_{\ell_0})]$, $\Gamma = [x_{\ell_0} \mapsto 7]$, and $\sigma = [x \mapsto 9]$. We have $\sigma = \gamma_{\Sigma^{\#}}(\sigma^{\#})[\Gamma]$.

* $\mathcal{E}^{\#}[1+x](\sigma^{\#}) = \text{subst}(1+x, \sigma^{\#}) = 1+(2+x_{\ell_0})$. We have $\mathcal{E}[1+(2+x_{\ell_0})](\Gamma) = 10$.

* $\mathcal{E}^{\#}[1+x](\sigma) = 1+9=10$.

**LEMMA A.3 (STRONG SOUNDNESS OF $\mathcal{I}^{\#}[\llbracket \cdot \rrbracket]$).** Let $\sigma^{\#} \in \Sigma^{\#}$, $i$ an instruction. Let $\Gamma \mapsto \sigma \in \gamma_{\Sigma^{\#}}(\sigma^{\#})$, i.e. $\Gamma$ and $\sigma$ are such that $\sigma = \gamma_{\Sigma^{\#}}(\sigma^{\#})[\Gamma]$. Then:
$$I[[i]](\sigma) = I^{\#}[[i]](\sigma^{\#})[\Gamma]$$

PROOF. Both $I[[i]]()$ and $I^{\#}[[[i]]]$ define sequence of instructions as function composition, so we only need to consider the case where $i$ is an assignment. We have $I[[x := e]](\sigma) = \sigma[x \leftarrow \mathcal{E}[e](\sigma)]$ and $I^{\#}[[x := e]](\sigma^{\#}) = \sigma[x \leftarrow \mathcal{E}^{\#}[e](\sigma^{\#})]$, so we can conclude the proof using Lemma A.1. $\square$

COROLLARY A.4 (SOUNDNESS AND COMPLETENESS OF $I^{\#}[[[i]]]$). Let $i$ an instruction and $\sigma^{\#} \in \Sigma^{\#}$.

$$\gamma_{\Xi^{\#}} \circ I^{\#}[[[i]]](\sigma^{\#}) = \{ \Gamma \mapsto I[[i]](\sigma) \mid \Gamma \mapsto \sigma \in \gamma_{\Xi^{\#}}(\sigma^{\#}) \}$$

PROOF. Immediate consequence of Lemma A.3. $\square$

## A.2 Soundness of $\sqcup^\ell$

The $\sqcup^\ell$ operator is not sound when applied to any pair of elements in $\Sigma^{\#}$. The problem comes from the fact that we reuse variable identifiers, which could thus create spurious relations between terms (this problem does not happen in analyses which create fresh variables instead). Consider for instance:

$$[x \mapsto 1 + y_{\ell_6}, y \mapsto 2] \sqcup^{\ell_6} [x \mapsto 1 + y_{\ell_6}, y \mapsto 3] = [x \mapsto 1 + y_{\ell_6}, y \mapsto y_{\ell_6}]$$

which contains a relation between $x$ and $y$ through the shared use of $y_{\ell_6}$, while this relation does not hold in the concrete. We can thus only prove a weaker soundness theorem:

*Definition A.5 (Occurs).* Let $p^{\#} \in \mathbb{L} \to \Sigma^{\#}$. Given two locations $\ell$ and $\ell_D$, we say that $\ell_D$ occurs in $p^{\#}[\ell]$ if a variable $v$ exists, with $\mathrm{loc}(v) = \ell_D$ and $v$ occurs in $p^{\#}[\ell]$ (i.e. $v$ is a subterm of $p^{\#}[\ell][x]$ for some $x \in \mathcal{X}$). For instance, if $p^{\#} = [\ell_8 \mapsto [x \mapsto 1 + x_{\ell_3}]]$, then $\ell_3$ occurs in $p^{\#}[\ell_8]$.

LEMMA A.6 (SOUNDNESS OF $\sqcup^\ell$). Let $\sigma_1^{\#}$ and $\sigma_2^{\#} \in \Sigma^{\#}$. If $\ell$ does not occur inside one of $\sigma_1^{\#}$ or $\sigma_2^{\#}$, then

$$\gamma_{\Xi^{\#}}(\sigma_1^{\#} \sqcup^{\ell} \sigma_2^{\#}) \supseteq \gamma_{\Xi^{\#}}(\sigma_1^{\#}) \cup \gamma_{\Xi^{\#}}(\sigma_2^{\#})$$

PROOF. Let $\sigma^{\#} = \sigma_1^{\#} \sqcup^{\ell} \sigma_2^{\#}$. Let $\Gamma_1 \in \Gamma$ and $\sigma_1 = \gamma_{\Xi^{\#}}(\sigma_1^{\#})[\Gamma_1]$. We show that $\Gamma$ exits, such that $\sigma_1 = \gamma_{\Xi^{\#}}(\sigma^{\#})[\Gamma]$. For this we take $\Gamma = \left[ v \in \mathcal{V} \mapsto \begin{cases} \sigma_1[x] & \text{if } \exists x \in \mathcal{X}: v = x_{\ell} \\ \Gamma_1[v] & \text{otherwise} \end{cases} \right]$.

* For variables $x$ such that $\sigma_1^{\#}[x] \neq \sigma_2^{\#}[x]$, i.e. such that $\sigma^{\#}[x] = x_{\ell}$, it is clear that $\gamma_{\Xi^{\#}}(\sigma^{\#})[\Gamma][x] = \mathcal{E}[[x_{\ell}]](\Gamma) = \sigma_1[x]$.

* For variables $x$ such that $\sigma^{\#}[x] = \sigma_1^{\#}[x] = \sigma_2^{\#}[x]$, we note that $\ell$ does not appear in any subterm of $\sigma^{\#}[x]$ by hypothesis. Thus, $\gamma_{\Xi^{\#}}(\sigma^{\#})[\Gamma][x] = \gamma_{\Xi^{\#}}(\sigma_1^{\#})[\Gamma_1][x]$ (as $\Gamma$ and $\Gamma_1$ have the same values for variables whose location is not $\ell$). And because $\gamma_{\Xi^{\#}}(\sigma_1^{\#})[\Gamma_1][x] = \sigma_1[x]$, this allows to conclude that $\gamma_{\Xi^{\#}}(\sigma^{\#})[\Gamma][x] = \sigma_1[x]$.

## A.3 Soundness of $\mathcal{F}_{\mathbb{L} \to \Sigma^{\#}}$

Fortunately, $\mathcal{F}_{\mathbb{L} \to \Sigma^{\#}}$ will always use $\sqcup^\ell$ in the context where it is sound. This is formally established using the following definition and theorem:

*Definition A.7 (Location of a variable).* Let $x_{\ell} \in \mathcal{V}$. We call $\ell$ the location of the variable $x_{\ell}$, and we define the function $\mathrm{loc}(\cdot) : \mathcal{V} \to \mathbb{L}$ the function that returns the location of its argument (i.e. $\mathrm{loc}(x_{\ell}) = \ell$).
$$I[[i]](\sigma) = I^{\#}[[i]](\sigma^{\#})[\Gamma]$$

PROOF. Both $I[[i]]()$ and $I^{\#}[[[i]]]$ define sequence of instructions as function composition, so we only need to consider the case where $i$ is an assignment. We have $I[[x := e]](\sigma) = \sigma[x \leftarrow \mathcal{E}[e](\sigma)]$ and $I^{\#}[[x := e]](\sigma^{\#}) = \sigma[x \leftarrow \mathcal{E}^{\#}[e](\sigma^{\#})]$, so we can conclude the proof using Lemma A.1. $\square$

COROLLARY A.4 (SOUNDNESS AND COMPLETENESS OF $I^{\#}[[[i]]]$). Let $i$ an instruction and $\sigma^{\#} \in \Sigma^{\#}$.

$$\gamma_{\Xi^{\#}} \circ I^{\#}[[[i]]](\sigma^{\#}) = \{ \Gamma \mapsto I[[i]](\sigma) \mid \Gamma \mapsto \sigma \in \gamma_{\Xi^{\#}}(\sigma^{\#}) \}$$

PROOF. Immediate consequence of Lemma A.3. $\square$

## A.2 Soundness of $\sqcup^\ell$

The $\sqcup^\ell$ operator is not sound when applied to any pair of elements in $\Sigma^{\#}$. The problem comes from the fact that we reuse variable identifiers, which could thus create spurious relations between terms (this problem does not happen in analyses which create fresh variables instead). Consider for instance:

$$[x \mapsto 1 + y_{\ell_6}, y \mapsto 2] \sqcup^{\ell_6} [x \mapsto 1 + y_{\ell_6}, y \mapsto 3] = [x \mapsto 1 + y_{\ell_6}, y \mapsto y_{\ell_6}]$$

which contains a relation between $x$ and $y$ through the shared use of $y_{\ell_6}$, while this relation does not hold in the concrete. We can thus only prove a weaker soundness theorem:

*Definition A.5 (Occurs).* Let $p^{\#} \in \mathbb{L} \to \Sigma^{\#}$. Given two locations $\ell$ and $\ell_D$, we say that $\ell_D$ occurs in $p^{\#}[\ell]$ if a variable $v$ exists, with $\mathrm{loc}(v) = \ell_D$ and $v$ occurs in $p^{\#}[\ell]$ (i.e. $v$ is a subterm of $p^{\#}[\ell][x]$ for some $x \in \mathcal{X}$). For instance, if $p^{\#} = [\ell_8 \mapsto [x \mapsto 1 + x_{\ell_3}]]$, then $\ell_3$ occurs in $p^{\#}[\ell_8]$.

LEMMA A.6 (SOUNDNESS OF $\sqcup^\ell$). Let $\sigma_1^{\#}$ and $\sigma_2^{\#} \in \Sigma^{\#}$. If $\ell$ does not occur inside one of $\sigma_1^{\#}$ or $\sigma_2^{\#}$, then

$$\gamma_{\Xi^{\#}}(\sigma_1^{\#} \sqcup^{\ell} \sigma_2^{\#}) \supseteq \gamma_{\Xi^{\#}}(\sigma_1^{\#}) \cup \gamma_{\Xi^{\#}}(\sigma_2^{\#})$$

PROOF. Let $\sigma^{\#} = \sigma_1^{\#} \sqcup^{\ell} \sigma_2^{\#}$. Let $\Gamma_1 \in \Gamma$ and $\sigma_1 = \gamma_{\Xi^{\#}}(\sigma_1^{\#})[\Gamma_1]$. We show that $\Gamma$ exits, such that $\sigma_1 = \gamma_{\Xi^{\#}}(\sigma^{\#})[\Gamma]$. For this we take $\Gamma = \left[ v \in \mathcal{V} \mapsto \begin{cases} \sigma_1[x] & \text{if } \exists x \in \mathcal{X} : v = x_{\ell} \\ \Gamma_1[v] & \text{otherwise} \end{cases} \right]$.

* For variables $x$ such that $\sigma_1^{\#}[x] \neq \sigma_2^{\#}[x]$, i.e. such that $\sigma^{\#}[x] = x_{\ell}$, it is clear that $\gamma_{\Xi^{\#}}(\sigma^{\#})[\Gamma][x] = \mathcal{E}[[x_{\ell}]](\Gamma) = \sigma_1[x]$.

* For variables $x$ such that $\sigma^{\#}[x] = \sigma_1^{\#}[x] = \sigma_2^{\#}[x]$, we note that $\ell$ does not appear in any subterm of $\sigma^{\#}[x]$ by hypothesis. Thus, $\gamma_{\Xi^{\#}}(\sigma^{\#})[\Gamma][x] = \gamma_{\Xi^{\#}}(\sigma_1^{\#})[\Gamma_1][x]$ (as $\Gamma$ and $\Gamma_1$ have the same values for variables whose location is not $\ell$). And because $\gamma_{\Xi^{\#}}(\sigma_1^{\#})[\Gamma_1][x] = \sigma_1[x]$, this allows to conclude that $\gamma_{\Xi^{\#}}(\sigma^{\#})[\Gamma][x] = \sigma_1[x]$.

## A.3 Soundness of $\mathcal{F}_{\mathbb{L} \to \Sigma^{\#}}$

Fortunately, $\mathcal{F}_{\mathbb{L} \to \Sigma^{\#}}$ will always use $\sqcup^\ell$ in the context where it is sound. This is formally established using the following definition and theorem:

*Definition A.7 (Location of a variable).* Let $x_{\ell} \in \mathcal{V}$. We call $\ell$ the location of the variable $x_{\ell}$, and we define the function $\mathrm{loc}(\cdot) : \mathcal{V} \to \mathbb{L}$ the function that returns the location of its argument (i.e. $\mathrm{loc}(x_{\ell}) = \ell$).
**LEMMA A.8.** Let $n \in \mathbb{N}$ and $p_n^\# = \mathcal{F}_{\mathbb{L} \to \Sigma_\perp}^{(n)}(\emptyset)$. Then, for all $\ell \in \mathbb{L}$, for any location $\ell'$ on any simple (acyclic) path from $\ell_0$ to $\ell$, $\ell$ does not occur in $\ell'$.

**PROOF.** The proof relies on the property (P) that if $n > 0$ and $p_n^\#[\ell] \neq \perp$, then there exists a simple path from $\ell_0$ to a predecessor of $\ell$ such that every element $\ell'$ in that path is such that $p_{n-1}^\#[\ell'] \neq \perp$, which is easily proved by induction.

The main proof is then done by induction of the property of the Lemma on $n$.

* the property is obviously true for $n = 0$, as $\mathcal{F}_{\mathbb{L} \to \Sigma_\perp}^{(0)}(\emptyset) = [\emptyset]$, whose domain is empty.

* when $n > 0$, we note $p_{n-1}^\# = \mathcal{F}_{\mathbb{L} \to \Sigma_\perp}^{(n-1)}(\emptyset)$ and $p_n^\# = \mathcal{F}_{\mathbb{L} \to \Sigma_\perp}^\#(p_{n-1}^\#)$.

- the property is true for $\ell_0$ by definition (there is no other location in the path from $\ell_0$ to $\ell_0$).

- we consider $\ell \in \mathbb{L}$ and $\ell'$ on a simple path from $\ell_0$ to $\ell$. By definition of $\mathcal{F}_{\mathbb{L} \to \Sigma_\perp}^\#$, we see that $\ell$ occurs in $p_n^\#[\ell']$ only if for all the predecessors $\ell''$ of $\ell'$, $\ell$ occurs in $p_{n-1}^\#[\ell'']$. But either $p_n^\#[\ell'] = \perp$, and then trivially $\ell$ does not occur in $p_n^\#[\ell']$. Or $p_n^\#[\ell'] \neq \perp$, and then by (P) there is a predecessor $\ell''$ of $\ell'$ such that $p_{n-1}^\#[\ell''] \neq \perp$, and further $\ell''$ is on a simple path from $\ell_0$ to $\ell'$. Using the induction hypothesis, we know that $\ell$ does not occur in $p_{n-1}^\#[\ell'']$. This concludes that $\ell$ does not occur in $p_n^\#[\ell']$.

□

With this lemma, we can now proceed to prove the soundness of the analysis:

**THEOREM A.9 (SOUNDNESS OF $\mathcal{F}_{\mathbb{L} \to \Sigma_\perp}^\#$).**

$$ \forall p^\# \in \mathbb{L} \to \Sigma_\perp^\# : (\mathcal{F}_{\mathbb{P}(\mathbb{S})} \circ \gamma_{\mathbb{L} \to \Sigma_\perp^\#}) (p^\#) \subseteq (\gamma_{\mathbb{L} \to \Sigma_\perp^\#} \circ \mathcal{F}_{\mathbb{L} \to \Sigma_\perp^\#}) (p^\#) $$

**PROOF.** We focus on the computation of $p'^\# = \mathcal{F}_{\mathbb{L} \to \Sigma_\perp^\#}(p^\#)$ at location $\ell$. Thanks to Lemma A.8, we know that for at least one of the predecessors $\ell'$ of $\ell$, the location $\ell$ will not occur in $p^\#[\ell']$. This will still be the case of $\mathcal{I}^\#[\mathrm{instr}[\ell']][p^\#[\ell']])$, by definition. Thus, the usage of $\mathbb{L}^\ell$ will be sound in this case. By combination with the soundness of $\mathcal{I}^\#[\cdot:\cdot](\cdot)$, we can conclude on the soundness of $\mathcal{F}_{\mathbb{L} \to \Sigma_\perp^\#}$.
□

**Note.** This analysis is sound, but it is not exact: notably, tests are not taken into account, nor is the semantic of the binary operation (we do as if they were uninterpreted functions); finally, the creation of simultaneous variables loose any relations that may exist between these variables. It is obviously usual for abstract domains to lose information; but it is still interesting to note that despite the fact that global value numbering is not exact, the SSA abstraction that builds on it will be exact.

## A.4 Soundness of the symbolic expression analysis

Our main soundness theorem for the global value numbering states that the analysis computes a sound overapproximation of all the reachable states of the program.

**THEOREM A.10 (SOUNDNESS OF GLOBAL VALUE NUMBERING).** Let $p^\#$ be a fixpoint of $\mathcal{F}_{\mathbb{L} \to \Sigma_\perp^\#}$, i.e. $p^\# = \mathcal{F}_{\mathbb{L} \to \Sigma_\perp^\#}(p^\#)$. Then $p^\#$ is a sound overapproximation of the reachable states of the $(\mathbb{S}, \to)$ transition system:

$$ \gamma_{\mathbb{L} \to \Sigma_\perp^\#}(p^\#) \supseteq \mathbb{S}_0^* $$
LEMMA A.8. Let $n \in \mathbb{N}$ and $p_n^\# = \mathcal{F}_{\mathbb{L} \to \Sigma_\perp}^{(n)}(\emptyset)$. Then, for all $\ell \in \mathbb{L}$, for any location $\ell'$ on any simple (acyclic) path from $\ell_0$ to $\ell$, $\ell$ does not occur in $\ell'$.

PROOF. The proof relies on the property (P) that if $n > 0$ and $p_n^\#[\ell] \neq \perp$, then there exists a simple path from $\ell_0$ to a predecessor of $\ell$ such that every element $\ell'$ in that path is such that $p_{n-1}^\#[\ell'] \neq \perp$, which is easily proved by induction.

The main proof is then done by induction of the property of the Lemma on $n$.

* the property is obviously true for $n = 0$, as $\mathcal{F}_{\mathbb{L} \to \Sigma_\perp}^{(0)}(\emptyset) = [\emptyset]$, whose domain is empty.

* when $n > 0$, we note $p_{n-1}^\# = \mathcal{F}_{\mathbb{L} \to \Sigma_\perp}^{(n-1)}(\emptyset)$ and $p_n^\# = \mathcal{F}_{\mathbb{L} \to \Sigma_\perp}^\#(p_{n-1}^\#)$.

- the property is true for $\ell_0$ by definition (there is no other location in the path from $\ell_0$ to $\ell_0$).

- we consider $\ell \in \mathbb{L}$ and $\ell'$ on a simple path from $\ell_0$ to $\ell$. By definition of $\mathcal{F}_{\mathbb{L} \to \Sigma_\perp}^\#$, we see that $\ell$ occurs in $p_n^\#[\ell']$ only if for all the predecessors $\ell''$ of $\ell'$, $\ell$ occurs in $p_{n-1}^\#[\ell'']$. But either $p_n^\#[\ell'] = \perp$, and then trivially $\ell$ does not occur in $p_n^\#[\ell']$. Or $p_n^\#[\ell'] \neq \perp$, and then by (P) there is a predecessor $\ell''$ of $\ell'$ such that $p_{n-1}^\#[\ell''] \neq \perp$, and further $\ell''$ is on a simple path from $\ell_0$ to $\ell'$. Using the induction hypothesis, we know that $\ell$ does not occur in $p_{n-1}^\#[\ell'']$. This concludes that $\ell$ does not occur in $p_n^\#[\ell']$.

□

With this lemma, we can now proceed to prove the soundness of the analysis:

THEOREM A.9 (SOUNDNESS OF $\mathcal{F}_{\mathbb{L} \to \Sigma_\perp}$).

$$ \forall p^\# \in \mathbb{L} \to \Sigma_\perp^\# : (\mathcal{F}_{\mathbb{P}(\mathbb{S})} \circ \gamma_{\mathbb{L} \to \Sigma_\perp^\#})(p^\#) \subseteq (\gamma_{\mathbb{L} \to \Sigma_\perp^\#} \circ \mathcal{F}_{\mathbb{L} \to \Sigma_\perp^\#})(p^\#) $$

PROOF. We focus on the computation of $p'^\# = \mathcal{F}_{\mathbb{L} \to \Sigma_\perp^\#}(p^\#)$ at location $\ell$. Thanks to Lemma A.8, we know that for at least one of the predecessors $\ell'$ of $\ell$, the location $\ell$ will not occur in $p^\#[\ell']$. This will still be the case of $\mathcal{I}^\#[\mathrm{instr}[\ell']][\mathcal{P}^\#[\ell']])$, by definition. Thus, the usage of $\mathbb{L}^\ell$ will be sound in this case. By combination with the soundness of $\mathcal{I}^\#[\cdot; \cdot](\cdot)$, we can conclude on the soundness of $\mathcal{F}_{\mathbb{L} \to \Sigma_\perp^\#}$.
□

Note. This analysis is sound, but it is not exact: notably, tests are not taken into account, nor is the semantic of the binary operation (we do as if they were uninterpreted functions); finally, the creation of simultaneous variables loose any relations that may exist between these variables. It is obviously usual for abstract domains to lose information; but it is still interesting to note that despite the fact that global value numbering is not exact, the SSA abstraction that builds on it will be exact.

## A.4 Soundness of the symbolic expression analysis

Our main soundness theorem for the global value numbering states that the analysis computes a sound overapproximation of all the reachable states of the program.

THEOREM A.10 (SOUNDNESS OF GLOBAL VALUE NUMBERING). Let $p^\#$ be a fixpoint of $\mathcal{F}_{\mathbb{L} \to \Sigma_\perp^\#}$, i.e. $p^\# = \mathcal{F}_{\mathbb{L} \to \Sigma_\perp^\#}(p^\#)$. Then $p^\#$ is a sound overapproximation of the reachable states of the $(\mathbb{S}, \to)$ transition system:

$$ \gamma_{\mathbb{L} \to \Sigma_\perp^\#}(p^\#) \supseteq \mathbb{S}_0^* $$
PROOF. By Theorem A.9 and the Tarski fixpoint transfer theorem. □

*Note.* The soundness of the algorithm works independently of the iteration strategy being used; we are thus free to use chaotic iteration methods [Cousot 1977] instead of the naive method presented in this formalization, to compute the global value numbering.

# B PROOFS OF SCOPE AND DOMINANCE PROPERTIES

In this section, let $p^{\#}$ be a fixpoint of $\mathcal{F}_{\mathbb{L} \to \mathbb{X}}^{\#}$ in a program whose graph is $\mathcal{G}$. We note by freevars($e$) the set of all the variables $v \in \mathbb{V}$ that occur in $e$.

THEOREM 5.1 (STRICTNESS). $\forall \ell \in \mathbb{L}, x \in \mathbb{X}, v \in \mathbb{V}: v \text{ occurs in } p^{\#}[\ell][x] \Rightarrow \text{loc}(v) \text{ dominates } \ell$.

PROOF OF THEOREM 5.1. We can prove the following property:

$$ \forall \ell_D, \ell \in \mathbb{L}: \ell_D \text{ occurs in } p^{\#}[\ell] \Rightarrow \ell = \ell_D \text{ or } \forall \ell' \in \text{preds}(\ell): \ell_D \text{ occurs in } p^{\#}[\ell'] \quad (2) $$

This is proved from the definition of $\mathcal{F}_{\mathbb{L} \to \mathbb{X}}^{\#}$: when analyzing location $\ell$, if $\ell = \ell_D$, a new symbolic variable $v$ with $\text{loc}(v) = \ell_D$ can be created. If $\ell \neq \ell_D$, assume there is $v$ with $\text{loc}(v) = \ell_D$ that occurs in $p^{\#}[\ell]$. Then $v$ must be present in all the predecessors: the $\sqcup^\ell$ operation replaces the term with a new symbolic variable (with a location $\ell$) when the abstract stores differ, so $v$ must occur in all arguments to $\sqcup^\ell$. Because $\mathcal{I}^{\#}[\mathbb{L} \cdot \mathbb{L}](\cdot)$ cannot introduce new variables, $v$ must occur in $p^{\#}[\ell']$ for all the predecessors $\ell'$ or $\ell$.

Now, iterating (2) implies that every path arriving at $\ell$ must either come from $\ell_D$, or from a location with no predecessor. The only location with no predecessor is $\ell_0$, and $\ell_D$ does not occur in the abstract store at $\ell_0$. Hence, $\ell_D$ dominates $\ell$. □

THEOREM B.1. If both $\ell_1$ and $\ell_2$ dominate $\ell$, then either $\ell_1$ dominate $\ell_2$ or $\ell_2$ dominate $\ell_1$.

PROOF OF THEOREM B.1. The proof can be found in [Appel 1998a, p.408]. □

THEOREM 5.6. $\text{scope}_G(e) = \{\ell \mid \overline{\text{scope}}_G(e) \text{ dominates } \ell\}$

PROOF OF THEOREM 5.6. We prove this property by induction on $e$:

* Case $e = v$: $\text{scope}_G(v) = \{\ell \mid \overline{\text{scope}}_G(v) \text{ dominates } \ell\}$ (by definition)

* Case $e = z$: $\text{scope}_G(z) = \mathbb{L} = \{\ell \mid \ell_0 \text{ dominates } \ell\}$ (because $\mathcal{G}$ only contains reachable locations and execution starts at $\ell_0$)

* Case $e = e_1 \diamond e_2$: Note that our induction property can be equivalently formulated as $\forall \ell \in \mathbb{L}: \ell \in \text{scope}_G(e) \Leftrightarrow \ell \text{ dominated by } \overline{\text{scope}}_G(e)$. And:

$$ \ell \in \text{scope}_G(e_1 \diamond e_2) \Leftrightarrow \ell \in \text{scope}_G(e_1) \wedge \ell \in \text{scope}_G(e_2) \quad \text{(by definition)} $$

$$ \Leftrightarrow \ell \text{ dominated by } \overline{\text{scope}}_G(e_1) \wedge \ell \text{ dominated by } \overline{\text{scope}}_G(e_2) \quad \text{(recursion hypothesis)} $$

$$ \Leftrightarrow \ell \text{ dominated by } \min(\overline{\text{scope}}_G(e_1), \overline{\text{scope}}_G(e_2)) \quad \text{(using Theorem B.1)} $$

$$ \Leftrightarrow \ell \text{ dominated by } \overline{\text{scope}}_G(e_1 \diamond e_2) \quad \text{(by definition)} $$

□

# C SOUNDNESS AND COMPLETENESS OF THE SSA ABSTRACTION

## C.1 $\mathcal{H}_{p^{\#}}$ is a strong homomorphism

We now prove that when $p^{\#}, \hat{g}$ is a fixpoint, $\mathcal{H}_{p^{\#}}$ is a strong homomorphism from $\rightsquigarrow \hat{g}$ to $\mapsto$.

This result is linked to the soundness (and completeness) of the $\mathcal{F}_{\text{SSA}^{\#}}$ transfer function, that we prove in the case where we reached a fixpoint $p^{\#}, \hat{g}$:
PROOF. By Theorem A.9 and the Tarski fixpoint transfer theorem. □

*Note.* The soundness of the algorithm works independently of the iteration strategy being used; we are thus free to use chaotic iteration methods [Cousot 1977] instead of the naive method presented in this formalization, to compute the global value numbering.

# B PROOFS OF SCOPE AND DOMINANCE PROPERTIES

In this section, let $p^{\#}$ be a fixpoint of $\mathcal{F}_{\mathbb{L} \to \mathbb{X}}^{\#}$ in a program whose graph is $\mathcal{G}$. We note by freevars($e$) the set of all the variables $v \in \mathbb{V}$ that occur in $e$.

THEOREM 5.1 (STRICTNESS). $\forall \ell \in \mathbb{L}, x \in \mathbb{X}, v \in \mathbb{V}: v \text{ occurs in } p^{\#}[\ell][x] \Rightarrow \text{loc}(v) \text{ dominates } \ell$.

PROOF OF THEOREM 5.1. We can prove the following property:

$$ \forall \ell_D, \ell \in \mathbb{L}: \ell_D \text{ occurs in } p^{\#}[\ell] \Rightarrow \ell = \ell_D \text{ or } \forall \ell' \in \text{preds}(\ell): \ell_D \text{ occurs in } p^{\#}[\ell'] \quad (2) $$

This is proved from the definition of $\mathcal{F}_{\mathbb{L} \to \mathbb{X}}^{\#}$: when analyzing location $\ell$, if $\ell = \ell_D$, a new symbolic variable $v$ with $\text{loc}(v) = \ell_D$ can be created. If $\ell \neq \ell_D$, assume there is $v$ with $\text{loc}(v) = \ell_D$ that occurs in $p^{\#}[\ell]$. Then $v$ must be present in all the predecessors: the $\sqcup^\ell$ operation replaces the term with a new symbolic variable (with a location $\ell$) when the abstract stores differ, so $v$ must occur in all arguments to $\sqcup^\ell$. Because $\mathcal{I}^{\#}[\mathbb{L} \cdot \mathbb{L}](\cdot)$ cannot introduce new variables, $v$ must occur in $p^{\#}[\ell']$ for all the predecessors $\ell'$ or $\ell$.

Now, iterating (2) implies that every path arriving at $\ell$ must either come from $\ell_D$, or from a location with no predecessor. The only location with no predecessor is $\ell_0$, and $\ell_D$ does not occur in the abstract store at $\ell_0$. Hence, $\ell_D$ dominates $\ell$. □

THEOREM B.1. If both $\ell_1$ and $\ell_2$ dominate $\ell$, then either $\ell_1$ dominate $\ell_2$ or $\ell_2$ dominate $\ell_1$.

PROOF OF THEOREM B.1. The proof can be found in [Appel 1998a, p.408]. □

THEOREM 5.6. $\text{scope}_G(e) = \{\ell \mid \overline{\text{scope}}_G(e) \text{ dominates } \ell\}$

PROOF OF THEOREM 5.6. We prove this property by induction on $e$:

* Case $e = v$: $\text{scope}_G(v) = \{\ell \mid \overline{\text{scope}}_G(v) \text{ dominates } \ell\}$ (by definition)

* Case $e = z$: $\text{scope}_G(z) = \mathbb{L} = \{\ell \mid \ell_0 \text{ dominates } \ell\}$ (because $\mathcal{G}$ only contains reachable locations and execution starts at $\ell_0$)

* Case $e = e_1 \diamond e_2$: Note that our induction property can be equivalently formulated as $\forall \ell \in \mathbb{L}: \ell \in \text{scope}_G(e) \Leftrightarrow \ell \text{ dominated by } \overline{\text{scope}}_G(e)$. And:

$$ \begin{align*} \ell \in \text{scope}_G(e_1 \diamond e_2) &\Leftrightarrow \ell \in \text{scope}_G(e_1) \wedge \ell \in \text{scope}_G(e_2) \tag{by definition} \\ &\Leftrightarrow \ell \text{ dominated by } \overline{\text{scope}}_G(e_1) \wedge \ell \text{ dominated by } \overline{\text{scope}}_G(e_2) \tag{recursion hypothesis} \\ &\Leftrightarrow \ell \text{ dominated by } \min(\overline{\text{scope}}_G(e_1), \overline{\text{scope}}_G(e_2)) \tag{using Theorem B.1} \\ &\Leftrightarrow \ell \text{ dominated by } \overline{\text{scope}}_G(e_1 \diamond e_2) \tag{by definition} \end{align*} $$

□

# C SOUNDNESS AND COMPLETENESS OF THE SSA ABSTRACTION

## C.1 $\mathcal{H}_{p^{\#}}$ is a strong homomorphism

We now prove that when $p^{\#}, \hat{g}$ is a fixpoint, $\mathcal{H}_{p^{\#}}$ is a strong homomorphism from $\rightsquigarrow_{\hat{g}}$ to $\mapsto$.

This result is linked to the soundness (and completeness) of the $\mathcal{F}_{\text{SSA}^{\#}}$ transfer function, that we prove in the case where we reached a fixpoint $p^{\#}, \hat{g}$:
LEMMA C.1 (SOUNDNESS AND COMPLETENESS OF $\mathcal{F}_{SSA^#}$). Let $(p^\#; \hat{g})$ such that $\mathcal{F}_{SSA^#}(p^\#; \hat{g}) = (p^\#; \hat{g})$. Let $\ell' \in \mathbb{L}$ and $\ell \in \text{preds}(\ell')$. Let $\sigma^\# = p^\#[\ell]$ and $\sigma'^\# = p^\#[\ell']$. Let $\Gamma \mapsto \sigma \in \gamma_{\Xi^\#}(\sigma^\#)$, i.e. $\sigma = \gamma_{\Xi^\#}(\sigma^\#)[\Gamma]$.

Then:

$$ \{\sigma' : (\ell, \sigma) \to (\ell', \sigma')\} = \{\gamma_{\Xi^\#}(\sigma'^\#)[\Gamma'] : (\ell, \Gamma) \rightsquigarrow \hat{g} (\ell', \Gamma')\} \quad (3) $$

$$ \{(\ell', \sigma') : (\ell, \sigma) \to (\ell', \sigma')\} = \{\mathcal{H}_{p^\#} (\ell', \Gamma') : (\ell, \Gamma) \rightsquigarrow \hat{g} (\ell', \Gamma')\} \quad (4) $$

PROOF. Equation (4) is obtained from (3) by expanding the definition of $\mathcal{H}_{p^\#}$, so we can concentrate on the proof of (3). The proof is simplified by the fact that both transitions $\rightsquigarrow g'^\#$ and $\to$ are deterministic when the next location is fixed. More precisely, let $\hat{e}, B$ be such that $(\ell, \ell') \mapsto (\hat{e}, B) \in \hat{g}$, then

$$ \exists \sigma' : (\ell, \sigma) \to (\ell', \sigma') \Rightarrow \sigma' = \mathcal{I}[\text{instr}[\ell]](\sigma) $$

$$ \exists \Gamma' : (\ell, \Gamma) \rightsquigarrow \hat{g} (\ell', \Gamma') \Rightarrow \Gamma' = \text{unbind}_{\hat{g}}(\ell', \text{bind}(B, \Gamma)) $$

Thus the set $\{\sigma' : (\ell, \sigma) \to (\ell', \sigma')\}$ is either a singleton or the empty set, and the same is true for $\{\gamma_{\Xi^\#}(\sigma'^\#)[\Gamma'] : (\ell, \Gamma) \rightsquigarrow \hat{g} (\ell', \Gamma')\}$.

The condition for the former set to be non-empty is that if $e$ is the condition guarding the transition from $\ell$ to $\ell'$ (i.e. $\mathcal{G}[\ell, \ell'] = e$), then $\mathcal{E}[e](\sigma') \neq 0$. Similarly, $(\ell, \Gamma) \rightsquigarrow g'^\# (\ell', \Gamma')$ if, and only if, $\mathcal{E}[\hat{e}](\Gamma) \neq 0$. Using Lemma A.1 (which says that the abstract evaluation of expression $\mathcal{E}^\#[]()$ is exact) and the definition of “edge”, we know that both conditions are equivalent. In the case where there is no edge from $\ell$ to $\ell'$ in $\hat{g}$, by definition of edge it means that either there is no edge from $\ell$ to $\ell'$ in $\mathcal{G}$, or that this edge has 0 for guard, or that $p^\#[\ell] = \perp$ and there is no state that reaches $\ell$: in every case the left and right sets are empty.

It remains to show that $\sigma' = \gamma_{\Xi^\#}(\sigma'^\#)[\Gamma']$. The main idea is that the binding $B$ produced by the edge function binds all the variables that are introduced at $\ell'$. Combined with Lemma A.3 (saying that the abstract evaluation of instructions $\mathcal{I}^\#[]()$ is exact), this allows to prove that $\sigma' = \gamma_{\Xi^\#}(\sigma'^\#)[\text{bind}(B, \Gamma)]$.

However, $\Gamma'$ is not just $\text{bind}(B, \Gamma)$, but $\text{unbind}_{\hat{g}}(\ell', \text{bind}(B, \Gamma))$. It remains to prove that this unbind operation has no effect. This is achieved using Theorem 5.3 (and the fact that $\text{scope}_B = \text{scope}_{\hat{g}}$, that says that because $p^\#$ is a fixed point, only symbolic variables that are scoped in $\ell'$ will occur in $\sigma'^\#$, thus unbind has no effect on the evaluation. Thus:

$$ \gamma_{\Xi^\#}(\sigma'^\#)(\Gamma') = \gamma_{\Xi^\#}(\sigma'^\#)[\text{unbind}_{\hat{g}}(\ell', \text{bind}(B, \Gamma))] = \gamma_{\Xi^\#}(\sigma'^\#)[\text{bind}(B, \Gamma)] = \sigma' $$

□

One consequence of this Lemma is the following theorem.

THEOREM C.2 (SAME SUCCESSOR STATES). Let $(p^\#; \hat{g})$ such that $\mathcal{F}_{SSA^#}(p^\#; \hat{g}) = (p^\#; \hat{g})$. Let $s \in \mathcal{S}, \hat{s} \in \hat{\mathcal{S}}$ such that $s = \mathcal{H}_{p^\#}(\hat{s})$. Then:

$$ \{s' \in \mathcal{S} \mid s \to s'\} = \{\mathcal{H}_{p^\#}(s') \mid s' \rightsquigarrow \hat{s} s'\} \quad (5) $$

PROOF. Obtained from Lemma C.1 (equation (4)) by union over all the successors of the location of $s$. □

COROLLARY C.3. $\mathcal{H}_{p^\#}$ is a strong homomorphism.

PROOF. Equation (5) is equivalent to Equation (1). □
LEMMA C.1 (SOUNDNESS AND COMPLETENESS OF $\mathcal{F}_{SSA\#}$). Let $(p^{\#}, \hat{g})$ such that $\mathcal{F}_{SSA\#}(p^{\#}, \hat{g}) = (p^{\#}, \hat{g})$. Let $\ell' \in \mathbb{L}$ and $\ell \in \text{preds}(\ell')$. Let $\sigma^{\#} = p^{\#}[\ell]$ and $\sigma'^{\#} = p^{\#}[\ell']$. Let $\Gamma \mapsto \sigma \in \gamma_{\Xi\#}(\sigma^{\#})$, i.e. $\sigma = \gamma_{\Xi\#}(\sigma^{\#})[\Gamma]$.

Then:

$$ \{\sigma' : (\ell, \sigma) \to (\ell', \sigma')\} = \{\gamma_{\Xi\#}(\sigma'^{\#})[\Gamma'] : (\ell, \Gamma) \rightsquigarrow \hat{g} (\ell', \Gamma')\} \quad (3) $$

$$ \{(\ell', \sigma') : (\ell, \sigma) \to (\ell', \sigma')\} = \{\mathcal{H}_{p^{\#}}(\ell', \Gamma') : (\ell, \Gamma) \rightsquigarrow \hat{g} (\ell', \Gamma')\} \quad (4) $$

PROOF. Equation (4) is obtained from (3) by expanding the definition of $\mathcal{H}_{p^{\#}}$, so we can concentrate on the proof of (3). The proof is simplified by the fact that both transitions $\rightsquigarrow g'^{\#}$ and $\to$ are deterministic when the next location is fixed. More precisely, let $\hat{e}, B$ be such that $(\ell, \ell') \mapsto (\hat{e}, B) \in \hat{g}$, then

$$ \exists \sigma' : (\ell, \sigma) \to (\ell', \sigma') \Rightarrow \sigma' = \mathcal{I}[\text{instr}[\ell]](\sigma) $$

$$ \exists \Gamma' : (\ell, \Gamma) \rightsquigarrow \hat{g} (\ell', \Gamma') \Rightarrow \Gamma' = \text{unbind}_{\hat{g}}(\ell', \text{bind}(B, \Gamma)) $$

Thus the set $\{\sigma' : (\ell, \sigma) \to (\ell', \sigma')\}$ is either a singleton or the empty set, and the same is true for $\{\gamma_{\Xi\#}(\sigma'^{\#})[\Gamma'] : (\ell, \Gamma) \rightsquigarrow \hat{g} (\ell', \Gamma')\}$.

The condition for the former set to be non-empty is that if $e$ is the condition guarding the transition from $\ell$ to $\ell'$ (i.e. $\mathcal{G}[\ell, \ell'] = e$), then $\mathcal{E}[e](\sigma') \neq 0$. Similarly, $(\ell, \Gamma) \rightsquigarrow g'^{\#} (\ell', \Gamma')$ if, and only if, $\mathcal{E}[\hat{e}](\Gamma) \neq 0$. Using Lemma A.1 (which says that the abstract evaluation of expression $\mathcal{E}^{\#}[]()$ is exact) and the definition of “edge”, we know that both conditions are equivalent. In the case where there is no edge from $\ell$ to $\ell'$ in $\hat{g}$, by definition of edge it means that either there is no edge from $\ell$ to $\ell'$ in $\mathcal{G}$, or that this edge has 0 for guard, or that $p^{\#}[\ell] = \perp$ and there is no state that reaches $\ell$: in every case the left and right sets are empty.

It remains to show that $\sigma' = \gamma_{\Xi\#}(\sigma'^{\#})[\Gamma']$. The main idea is that the binding $B$ produced by the edge function binds all the variables that are introduced at $\ell'$. Combined with Lemma A.3 (saying that the abstract evaluation of instructions $\mathcal{I}^{\#}[]()$ is exact), this allows to prove that $\sigma' = \gamma_{\Xi\#}(\sigma'^{\#})[\text{bind}(B, \Gamma)]$.

However, $\Gamma'$ is not just $\text{bind}(B, \Gamma)$, but $\text{unbind}_{\hat{g}}(\ell', \text{bind}(B, \Gamma))$. It remains to prove that this unbind operation has no effect. This is achieved using Theorem 5.3 (and the fact that $\text{scope}_{\mathcal{G}} = \text{scope}_{\hat{g}}$), that says that because $p^{\#}$ is a fixed point, only symbolic variables that are scoped in $\ell'$ will occur in $\sigma'^{\#}$, thus unbind has no effect on the evaluation. Thus:

$$ \gamma_{\Xi\#}(\sigma'^{\#})(\Gamma') = \gamma_{\Xi\#}(\sigma'^{\#})[\text{unbind}_{\hat{g}}(\ell', \text{bind}(B, \Gamma))] = \gamma_{\Xi\#}(\sigma'^{\#})[\text{bind}(B, \Gamma)] = \sigma' \quad \square $$

One consequence of this Lemma is the following theorem.

THEOREM C.2 (SAME SUCCESSOR STATES). Let $(p^{\#}, \hat{g})$ such that $\mathcal{F}_{SSA\#}(p^{\#}, \hat{g}) = (p^{\#}, \hat{g})$. Let $s \in \mathcal{S}, \hat{s} \in \hat{\mathcal{S}}$ such that $s = \mathcal{H}_{p^{\#}}(\hat{s})$. Then:

$$ \{s' \in \mathcal{S} \mid s \mapsto s'\} = \{\mathcal{H}_{p^{\#}}(s') \mid s' \rightsquigarrow \hat{s} s'\} \quad (5) $$

PROOF. Obtained from Lemma C.1 (equation (4)) by union over all the successors of the location of $s$. $\square$

COROLLARY C.3. $\mathcal{H}_{p^{\#}}$ is a strong homomorphism.

PROOF. Equation (5) is equivalent to Equation (1). $\square$
A consequence of $\mathcal{H}_{p^{\#}}$ being a strong homomorphism is that it is a homomorphism, and thus a simulation, which implies that the traces of $(\hat{\mathcal{S}}, \rightsquigarrow_{\hat{g}})$ are included in the traces of the $(\mathcal{S}, \rightarrow)$ transition system. Thus, we can conclude that $(p^{\#}, \hat{g})$ represents a subset of all the traces of $(\mathcal{S}, \rightarrow)$ (and is thus complete). In the next section, we also prove the soundness.

## C.2 $\mathcal{H}_{p^{\#}}$ is a surjective strong homomorphism between the reachable states

Up to now we could conclude that $\mathcal{H}_{p^{\#}}$ is a simulation from SSA to the original program, but we did not prove that it is a simulation from the original program to SSA. And indeed it is not: there are transitions in the original transition system that cannot be simulated in the SSA transition system.

*Example C.4.* Taking the transition system stemming from the program of Figure 1b, we have for instance:

$$ \text{let } s = \left( \ell_3, \left[ \begin{array}{l} \text{inc} \mapsto -4 \\ \text{time} \mapsto 35 \\ \text{i} \mapsto 10 \\ \text{hours} \mapsto 0 \end{array} \right] \right) \quad \text{and } s' = \left( \ell_4, \left[ \begin{array}{l} \text{inc} \mapsto -4 \\ \text{time} \mapsto 31 \\ \text{i} \mapsto 11 \\ \text{hours} \mapsto 0 \end{array} \right] \right). \quad \text{Then: } s \rightsquigarrow s'. $$

This $s \rightsquigarrow s'$ transition cannot be simulated by the SSA program, because the states where inc $\neq$ 1 and time $\neq$ i cannot be represented in the SSA version (i.e. : $\forall \hat{s} \in \hat{\mathcal{S}} : \mathcal{H}_{p^{\#}}(\hat{s}) \neq s$).

However, the reason why states like $s$ or $s'$ cannot be represented by $p^{\#}$ is that they are not reachable: $p^{\#}$ is a sound abstraction of the reachable states $S_0^*$ (Theorem A.10), but nothing requires that $p^{\#}$ represent non-reachable states.

We thus want to restrict the transition relation $\rightarrow$ to the reachable states:

$$ \rightarrow_{|S^*} \triangleq \{(s, s') \in S^* \mid s \rightarrow s'\} \qquad (6) $$

However, $\mathcal{H}_{p^{\#}}$ is no longer a homomorphism from $\rightsquigarrow_{\hat{g}}$ to $\rightarrow_{|S^*}$, because unreachable SSA transitions cannot be matched in $\rightarrow_{|S^*}$.

*Example C.5.* Indeed, if we take again Figure 1 as an example:

$$ \text{let } \hat{s} = \left( \ell_1, \left[ \begin{array}{l} \text{inc}_{\ell_0} \mapsto 11 \\ \text{time}_{\ell_0} \mapsto 22 \\ \text{i}_{\ell_0} \mapsto 33 \\ \text{hours}_{\ell_0} \mapsto 44 \\ \text{time}_{i_{\ell_1}} \mapsto -1 \\ \text{hours}_{i_{\ell_1}} \mapsto 27 \end{array} \right] \right) \quad \text{and } \hat{s}' = \left( \ell_2, \left[ \begin{array}{l} \text{inc}_{\ell_0} \mapsto 11 \\ \text{time}_{\ell_0} \mapsto 22 \\ \text{i}_{\ell_0} \mapsto 33 \\ \text{hours}_{\ell_0} \mapsto 44 \\ \text{time}_{i_{\ell_1}} \mapsto -1 \\ \text{hours}_{i_{\ell_1}} \mapsto 27 \end{array} \right] \right) $$

Then we have $\hat{s} \rightsquigarrow_{\hat{g}} \hat{s}'$ but we do not have $\mathcal{H}_{p^{\#}}(\hat{s}) \rightarrow_{|S^*} \mathcal{H}_{p^{\#}}(\hat{s}')$, because $\mathcal{H}_{p^{\#}}(\hat{s})$ is not a reachable state.

We thus also need to restrict SSA transitions to the reachable SSA states.

*Definition C.6 (Reachable SSA state).* Given $\hat{g}$, we define $\hat{\mathcal{S}}^*$ to be the reachable set of SSA states:

$$ \hat{\mathcal{S}}^* \triangleq \{ \hat{s} \in \hat{\mathcal{S}} : \exists \hat{s}_0 \in \hat{\mathcal{S}}_0, \hat{s}_0 \rightsquigarrow_{\hat{g}}^* \hat{s} \} $$

where $\rightsquigarrow_{\hat{g}}^*$ represent the reflexive and transitive closure of $\rightsquigarrow_{\hat{g}}$.

*Definition C.7 (Restricted SSA transition).*

$$ \rightsquigarrow_{\hat{g}}^{\triangleq} \{(\hat{s}, \hat{s}') \in \hat{\mathcal{S}}^* \mid \hat{s} \rightsquigarrow_{\hat{g}} \hat{s}'\} \qquad (7) $$
A consequence of $\mathcal{H}_{p^{\#}}$ being a strong homomorphism is that it is a homomorphism, and thus a simulation, which implies that the traces of $(\hat{\mathcal{S}}, \rightsquigarrow_{\hat{g}})$ are included in the traces of the $(\mathcal{S}, \rightarrow)$ transition system. Thus, we can conclude that $(p^{\#}, \hat{g})$ represents a subset of all the traces of $(\mathcal{S}, \rightarrow)$ (and is thus complete). In the next section, we also prove the soundness.

## C.2 $\mathcal{H}_{p^{\#}}$ is a surjective strong homomorphism between the reachable states

Up to now we could conclude that $\mathcal{H}_{p^{\#}}$ is a simulation from SSA to the original program, but we did not prove that it is a simulation from the original program to SSA. And indeed it is not: there are transitions in the original transition system that cannot be simulated in the SSA transition system.

*Example C.4.* Taking the transition system stemming from the program of Figure 1b, we have for instance:

$$ \text{let } s = \left( \ell_3, \left[ \begin{array}{l} \text{inc} \mapsto -4 \\ \text{time} \mapsto 35 \\ \text{i} \mapsto 10 \\ \text{hours} \mapsto 0 \end{array} \right] \right) \quad \text{and } s' = \left( \ell_4, \left[ \begin{array}{l} \text{inc} \mapsto -4 \\ \text{time} \mapsto 31 \\ \text{i} \mapsto 11 \\ \text{hours} \mapsto 0 \end{array} \right] \right). \quad \text{Then: } s \rightsquigarrow s'. $$

This $s \rightsquigarrow s'$ transition cannot be simulated by the SSA program, because the states where inc $\neq$ 1 and time $\neq$ i cannot be represented in the SSA version (i.e. : $\forall \hat{s} \in \hat{\mathcal{S}} : \mathcal{H}_{p^{\#}}(\hat{s}) \neq s$).

However, the reason why states like $s$ or $s'$ cannot be represented by $p^{\#}$ is that they are not reachable: $p^{\#}$ is a sound abstraction of the reachable states $S_0^*$ (Theorem A.10), but nothing requires that $p^{\#}$ represent non-reachable states.

We thus want to restrict the transition relation $\rightsquigarrow$ to the reachable states:

$$ \rightsquigarrow_{S^*} \triangleq \{(s, s') \in S^* \mid s \rightsquigarrow s'\} \quad (6) $$

However, $\mathcal{H}_{p^{\#}}$ is no longer a homomorphism from $\rightsquigarrow_{\hat{g}}$ to $\rightsquigarrow_{|S^*}$, because unreachable SSA transitions cannot be matched in $\rightsquigarrow_{|S^*}$.

*Example C.5.* Indeed, if we take again Figure 1 as an example:

$$ \text{let } \hat{s} = \left( \ell_1, \left[ \begin{array}{l} \text{inc}_{\ell_0} \mapsto 11 \\ \text{time}_{\ell_0} \mapsto 22 \\ \text{i}_{\ell_0} \mapsto 33 \\ \text{hours}_{\ell_0} \mapsto 44 \\ \text{time}_{i_{\ell_1}} \mapsto -1 \\ \text{hours}_{i_{\ell_1}} \mapsto 27 \end{array} \right] \right) \quad \text{and } \hat{s}' = \left( \ell_2, \left[ \begin{array}{l} \text{inc}_{\ell_0} \mapsto 11 \\ \text{time}_{\ell_0} \mapsto 22 \\ \text{i}_{\ell_0} \mapsto 33 \\ \text{hours}_{\ell_0} \mapsto 44 \\ \text{time}_{i_{\ell_1}} \mapsto -1 \\ \text{hours}_{i_{\ell_1}} \mapsto 27 \end{array} \right] \right) $$

Then we have $\hat{s} \rightsquigarrow_{\hat{g}} \hat{s}'$ but we do not have $\mathcal{H}_{p^{\#}}(\hat{s}) \rightsquigarrow_{|S^*} \mathcal{H}_{p^{\#}}(\hat{s}')$, because $\mathcal{H}_{p^{\#}}(\hat{s})$ is not a reachable state.

We thus also need to restrict SSA transitions to the reachable SSA states.

*Definition C.6 (Reachable SSA state).* Given $\hat{g}$, we define $\hat{S}^*$ to be the reachable set of SSA states:

$$ \hat{S}^* \triangleq \{\hat{s} \in \hat{\mathcal{S}} : \exists \hat{s}_0 \in \hat{S}_0, \hat{s}_0 \rightsquigarrow_{\hat{g}}^* \hat{s}'\} $$

where $\rightsquigarrow_{\hat{g}}^*$ represent the reflexive and transitive closure of $\rightsquigarrow_{\hat{g}}$.

*Definition C.7 (Restricted SSA transition).*

$$ \rightsquigarrow_{\hat{g}|\hat{S}^*} \triangleq \{(\hat{s}, \hat{s}') \in \hat{S}^* \mid \hat{s} \rightsquigarrow_{\hat{g}} \hat{s}'\} \quad (7) $$
We can now prove that $\mathcal{H}_{p^{\#}}$ is a surjective strong homomorphism on these restricted relations:

THEOREM C.8 ($\mathcal{H}_{p^{\#}}$ IS A SURJECTIVE STRONG HOMOMORPHISM). $\mathcal{H}_{p^{\#}}$ is a strong homomorphism from $\rightsquigarrow_{\hat{g}|\hat{s}^*} to \to_{|S^*}$:

$$ \forall \hat{s}, \hat{s}' \in \hat{S} : \hat{s} \rightsquigarrow_{\hat{g}|\hat{s}^*} \hat{s}' \Leftrightarrow \mathcal{H}(\hat{s}) \to_{|S^*} \mathcal{H}(\hat{s}') \quad (8) $$

$\mathcal{H}_{p^{\#}}$ is surjective on the field of $\to_{|S^*}$:

$$ \forall s, s' \in S : \mathcal{H}(\hat{s}) \to_{|S^*} \mathcal{H}(\hat{s}') \Rightarrow \exists \hat{s}, \hat{s}' \in \hat{S} : s = \mathcal{H}(\hat{s}) \wedge s' = \mathcal{H}(\hat{s}') \quad (9) $$

PROOF. We note by $S^n$ and $\hat{S}^n$ respectively the original program states and SSA states reachable after $n$ transitions, and we show by induction on $n$ that

$$ \forall \hat{s}, \hat{s}' \in \hat{S}^n : \hat{s} \rightsquigarrow_{\hat{g}|\hat{s}^*} \hat{s}' \Leftrightarrow \mathcal{H}(\hat{s}) \to_{|S^*} \mathcal{H}(\hat{s}') $$

using Theorem C.2. □

Note that it is quite clear that a surjective strong homomorphism is also a bisimulation.

### C.3 Meaning, soundness and completeness of the SSA abstraction

Up to now we discussed how an SSA abstraction can be constructed using transfer functions, and the strong relation between the SSA abstraction and the original program. What is missing is to define the concretization for the SSA abstraction.

Definition C.9 (Concretization of the SSA abstraction). We define the concretization of the $SSA^\#$ domain as follows:

$$ \gamma_{SSA^\#} : S^\#A^\# \to \mathcal{P}(\mathcal{P}(S \times S)) $$

$$ \gamma_{SSA^\#}(p^{\#}, \hat{g}) = \{(\mathcal{H}_{p^{\#}}(\hat{s}), \mathcal{H}_{p^{\#}}(\hat{s}')) | \hat{s} \rightsquigarrow_{\hat{g}|\hat{s}^*} \hat{s}'\} $$

(note that the definition of $\hat{S}^*$ depends on $\rightsquigarrow_{\hat{g}}$).

Using this concretization, we can say that what our SSA-transformation analysis computes a lossless (but non-trivial) abstraction of the transition system of the original program.

THEOREM C.10 (SOUNDNESS AND COMPLETENESS OF THE SSA ABSTRACTION COMPUTATION).

Let $(p^{\#}, \hat{g})$ be a fixpoint of $\mathcal{F}_{SSA^\#}$. Then: $\gamma_{SSA^\#}(p^{\#}, \hat{g}) = \to_{|S^*}$

PROOF. By definition of $\gamma_{SSA^\#}(p^{\#}, \hat{g})$ and Theorem C.8. □

Following the hierarchy of semantics [Cousot 2002], we can derive from this result that our analysis also computes weaker abstractions of the original program in a lossless way. For instance, the result of our analysis also exactly represents the set of reachable states:

THEOREM C.11 (SOUNDNESS AND COMPLETENESS OF THE SSA ABSTRACTION COMPUTATION VIEWED AS REACHABLE STATES). Let $\gamma$ be defined as

$$ \gamma : S^\#A^\# \to \mathcal{P}(S) $$

$$ \gamma(p^{\#}, \hat{g}) = \{s \in S : \exists s_0 \in S_0, s_0 \mathcal{R}^* s\} \text{ where } \mathcal{R} \triangleq \gamma_{SSA^\#}(p^{\#}, \hat{g}) $$

Let $(p^{\#}, \hat{g})$ be a fixpoint of $\mathcal{F}_{SSA^\#}$. Then:

$$ \gamma(p^{\#}, \hat{g}) = S^* $$
We can now prove that $\mathcal{H}_{p^{\#}}$ is a surjective strong homomorphism on these restricted relations:

**THEOREM C.8** ($\mathcal{H}_{p^{\#}}$ IS A SURJECTIVE STRONG HOMOMORPHISM). $\mathcal{H}_{p^{\#}}$ is a strong homomorphism from $\rightsquigarrow_{\hat{g}|\hat{s}^*} to \to_{|S^*}$:

$$ \forall \hat{s}, \hat{s}' \in \hat{S} : \hat{s} \rightsquigarrow_{\hat{g}|\hat{s}^*} \hat{s}' \Leftrightarrow \mathcal{H}(\hat{s}) \to_{|S^*} \mathcal{H}(\hat{s}') \quad (8) $$

$\mathcal{H}_{p^{\#}}$ is surjective on the field of $\to_{|S^*}$:

$$ \forall s, s' \in S : \mathcal{H}(\hat{s}) \to_{|S^*} \mathcal{H}(\hat{s}') \Rightarrow \exists \hat{s}, \hat{s}' \in \hat{S} : s = \mathcal{H}(\hat{s}) \wedge s' = \mathcal{H}(\hat{s}') \quad (9) $$

**PROOF.** We note by $S^n$ and $\hat{S}^n$ respectively the original program states and SSA states reachable after $n$ transitions, and we show by induction on $n$ that

$$ \forall \hat{s}, \hat{s}' \in \hat{S}^n : \hat{s} \rightsquigarrow_{\hat{g}|\hat{s}^*} \hat{s}' \Leftrightarrow \mathcal{H}(\hat{s}) \to_{|S^*} \mathcal{H}(\hat{s}') $$

using Theorem C.2.

□

Note that it is quite clear that a surjective strong homomorphism is also a bisimulation.

### C.3 Meaning, soundness and completeness of the SSA abstraction

Up to now we discussed how an SSA abstraction can be constructed using transfer functions, and the strong relation between the SSA abstraction and the original program. What is missing is to define the concretization for the SSA abstraction.

**Definition C.9** (Concretization of the SSA abstraction). We define the concretization of the $SSA^\#$ domain as follows:

$$ \gamma_{SSA^\#} : S^\#A^\# \to \mathcal{P}(\mathcal{P}(S \times S)) $$

$$ \gamma_{SSA^\#}(p^{\#}, \hat{g}) = \{(\mathcal{H}_{p^{\#}}(\hat{s}), \mathcal{H}_{p^{\#}}(\hat{s}')) \mid \hat{s} \rightsquigarrow_{\hat{g}|\hat{s}^*} \hat{s}'\} $$

(note that the definition of $\hat{S}^*$ depends on $\rightsquigarrow_{\hat{g}}$).

Using this concretization, we can say that what our SSA-transformation analysis computes a lossless (but non-trivial) abstraction of the transition system of the original program.

**THEOREM C.10** (SOUNDNESS AND COMPLETENESS OF THE SSA ABSTRACTION COMPUTATION).

$$ \text{Let } (p^{\#}, \hat{g}) \text{ be a fixpoint of } \mathcal{F}_{SSA^{\#}}. \text{ Then: } \quad \gamma_{SSA^{\#}}(p^{\#}, \hat{g}) = \to_{|S^{*}} $$

**PROOF.** By definition of $\gamma_{SSA^\#}(p^{\#}, \hat{g})$ and Theorem C.8.

□

Following the hierarchy of semantics [Cousot 2002], we can derive from this result that our analysis also computes weaker abstractions of the original program in a lossless way. For instance, the result of our analysis also exactly represents the set of reachable states:

**THEOREM C.11** (SOUNDNESS AND COMPLETENESS OF THE SSA ABSTRACTION COMPUTATION VIEWED AS REACHABLE STATES). Let $\gamma$ be defined as

$$ \gamma : S^\#A^\# \to \mathcal{P}(S) $$

$$ \gamma(p^{\#}, \hat{g}) = \{s \in S : \exists s_0 \in S_0, s_0 \mathcal{R}^* s\} \text{ where } \mathcal{R} \triangleq \gamma_{SSA^\#}(p^{\#}, \hat{g}) $$

Let $(p^{\#}, \hat{g})$ be a fixpoint of $\mathcal{F}_{SSA^\#}$. Then:

$$ \gamma(p^{\#}, \hat{g}) = S^{*} $$
PROOF. Consequence of Theorem C.10 □

The same could be done for the set of program traces, or the set of pairs of input/output states of the program. When viewed as a program transformation, this result also proved that the SSA translation preserved the semantics of the original program.

# D PROOFS FOR INCREMENTALLY COMPLETE CONSTRUCTION OF SSA

## D.1 Soundness and completeness of the analysis when a post-fixpoint is reached

LEMMA D.1. The following conditions are equivalent:

$$ \sigma_1^{\#} \sqsubseteq^{\ell} \sigma_2^{\#} = \sigma_2^{\#} = (\sigma_1^{\#} \sqcup^{\ell} \sigma_2^{\#}) \quad (10) $$

$$ \sigma_1^{\#} \sqsubseteq^{\ell} \sigma_2^{\#} = \exists \sigma_3^{\#} : \sigma_2^{\#} = \sigma_1^{\#} \sqcup^{\ell} \sigma_3^{\#} \quad (11) $$

PROOF. • (10) ⇒ (11): it suffices to pick $\sigma_3^{\#} = \sigma_2^{\#}$.

• (11) ⇒ (10):

$$ (\sigma_1^{\#} \sqcup^{\ell} \sigma_2^{\#}) = \sigma_1^{\#} \sqcup^{\ell} (\sigma_1^{\#} \sqcup^{\ell} \sigma_3^{\#}) \quad \text{(by definition of } \sigma_2^{\#}) $$

$$ = (\sigma_1^{\#} \sqcup^{\ell} \sigma_1^{\#}) \sqcup^{\ell} \sigma_3^{\#} \quad \text{(associativity of } \sqcup^{\ell}) $$

$$ = \sigma_1^{\#} \sqcup^{\ell} \sigma_3^{\#} \quad \text{(idempotence of } \sqcup^{\ell}) $$

$$ = \sigma_2^{\#} \quad \text{(by definition of } \sigma_2^{\#}) $$

□

Definition D.2 (Order relation on $\mathbb{L} \to \Sigma_{\perp}^{\#}$). Let $p_1^{\#}, p_2^{\#} \in \mathbb{L} \to \Sigma_{\perp}^{\#}$. We define:

$$ p_1^{\#} \sqsubseteq p_2^{\#} \triangleq \forall \ell \in \mathbb{L} : p_1^{\#}[\ell] \sqsubseteq p_2^{\#}[\ell] $$

Definition D.3 (Post-fixpoint). $p^{\#} \in \mathbb{L} \to \Sigma_{\perp}^{\#}$ is a post-fixpoint of $\mathcal{F}_{\mathbb{L} \to \Sigma_{\perp}^{\#}}$ if: $\mathcal{F}_{\mathbb{L} \to \Sigma_{\perp}^{\#}}(p^{\#}) \sqsubseteq p^{\#}.$

This is the classic definition of a post-fixpoint in abstract interpretation.

Now, many of the previous theorems that applied when $p^{\#}$ was a fixpoint of the program can be generalized to the case where $p^{\#}$ is only a post-fixpoint (see Theorems D.4, D.5 and Lemma D.6 in the appendix). In particular, we can generalize our soundness theorem to the post-fixpoint case:

THEOREM D.4 (THEOREM 5.1 IN THE POST-FIXPOINT CASE). Let $p^{\#}$ be a post-fixpoint of $\mathcal{F}_{\mathbb{L} \to \Sigma_{\perp}^{\#}}$.

Then

$$ \forall \ell \in \mathbb{L}, \forall x \in \mathcal{X} : \forall v \text{ free variable of } p^{\#}[\ell][x] : \text{loc}(v) \text{ dominates } \ell $$

PROOF. Equation (2) remains true, and we can iterate it again. □

THEOREM D.5 (THEOREM 5.3 IN THE POST-FIXPOINT CASE). Let $p^{\#}$ be a post-fixpoint of $\mathcal{F}_{\mathbb{L} \to \Sigma_{\perp}^{\#}}$ for a program whose graph is $\mathcal{G}$. Then:

$$ \forall \ell \in \mathbb{L} : \forall x \in \mathcal{X} : \ell \in \text{scope}_{\mathcal{G}}(p^{\#}[\ell][x]) $$

PROOF. Direct consequence of Theorem D.4 and definition of scope. □
PROOF. Consequence of Theorem C.10 □

The same could be done for the set of program traces, or the set of pairs of input/output states of the program. When viewed as a program transformation, this result also proved that the SSA translation preserved the semantics of the original program.

# D PROOFS FOR INCREMENTALLY COMPLETE CONSTRUCTION OF SSA

## D.1 Soundness and completeness of the analysis when a post-fixpoint is reached

LEMMA D.1. The following conditions are equivalent:

$$ \sigma_1^{\#} \sqsubseteq^{\ell} \sigma_2^{\#} = \sigma_2^{\#} = (\sigma_1^{\#} \sqcup^{\ell} \sigma_2^{\#}) \quad (10) $$

$$ \sigma_1^{\#} \sqsubseteq^{\ell} \sigma_2^{\#} = \exists \sigma_3^{\#} : \sigma_2^{\#} = \sigma_1^{\#} \sqcup^{\ell} \sigma_3^{\#} \quad (11) $$

PROOF. • (10) ⇒ (11): it suffices to pick $\sigma_3^{\#} = \sigma_2^{\#}$.

• (11) ⇒ (10):

$$ (\sigma_1^{\#} \sqcup^{\ell} \sigma_2^{\#}) = \sigma_1^{\#} \sqcup^{\ell} (\sigma_1^{\#} \sqcup^{\ell} \sigma_3^{\#}) \quad (\text{by definition of } \sigma_2^{\#}) $$

$$ = (\sigma_1^{\#} \sqcup^{\ell} \sigma_1^{\#}) \sqcup^{\ell} \sigma_3^{\#} \quad (\text{associativity of } \sqcup^{\ell}) $$

$$ = \sigma_1^{\#} \sqcup^{\ell} \sigma_3^{\#} \quad (\text{idempotence of } \sqcup^{\ell}) $$

$$ = \sigma_2^{\#} \quad (\text{by definition of } \sigma_2^{\#}) $$

□

Definition D.2 (Order relation on $\mathbb{L} \to \Sigma_{\perp}^{\#}$). Let $p_1^{\#}, p_2^{\#} \in \mathbb{L} \to \Sigma_{\perp}^{\#}$. We define:

$$ p_1^{\#} \sqsubseteq p_2^{\#} \triangleq \forall \ell \in \mathbb{L} : p_1^{\#}[\ell] \sqsubseteq p_2^{\#}[\ell] $$

Definition D.3 (Post-fixpoint). $p^{\#} \in \mathbb{L} \to \Sigma_{\perp}^{\#}$ is a post-fixpoint of $\mathcal{F}_{\mathbb{L} \to \Sigma_{\perp}^{\#}}$ if: $\mathcal{F}_{\mathbb{L} \to \Sigma_{\perp}^{\#}}(p^{\#}) \sqsubseteq p^{\#}.$

This is the classic definition of a post-fixpoint in abstract interpretation.

Now, many of the previous theorems that applied when $p^{\#}$ was a fixpoint of the program can be generalized to the case where $p^{\#}$ is only a post-fixpoint (see Theorems D.4, D.5 and Lemma D.6 in the appendix). In particular, we can generalize our soundness theorem to the post-fixpoint case:

THEOREM D.4 (THEOREM 5.1 IN THE POST-FIXPOINT CASE). Let $p^{\#}$ be a post-fixpoint of $\mathcal{F}_{\mathbb{L} \to \Sigma_{\perp}^{\#}}$.

Then

$$ \forall \ell \in \mathbb{L}, \forall x \in \mathcal{X} : \forall v \text{ free variable of } p^{\#}[\ell][x] : \text{loc}(v) \text{ dominates } \ell $$

PROOF. Equation (2) remains true, and we can iterate it again. □

THEOREM D.5 (THEOREM 5.3 IN THE POST-FIXPOINT CASE). Let $p^{\#}$ be a post-fixpoint of $\mathcal{F}_{\mathbb{L} \to \Sigma_{\perp}^{\#}}$ for a program whose graph is $\mathcal{G}$. Then:

$$ \forall \ell \in \mathbb{L} : \forall x \in \mathcal{X} : \ell \in \text{scope}_{\mathcal{G}}(p^{\#}[\ell][x]) $$

PROOF. Direct consequence of Theorem D.4 and definition of scope. □
LEMMA D.6 (LEMMA C.1 IN THE POST-FIXPOINT CASE). Let $p^{\#}$ be a post-fixpoint of $\mathcal{F}_{\mathbb{L} \to \Sigma_{\perp}^{\#}}$ and $\hat{g} = \text{graph}(p^{\#})$. Let $\ell' \in \mathbb{L}$ and $\ell \in \text{preds}(\ell')$. Let $\sigma^{\#} = p^{\#}[\ell]$ and $\sigma'^{\#} = p^{\#}[\ell']$. Let $\Gamma \mapsto \sigma \in \gamma_{\Sigma^{\#}}(\sigma^{\#})$, i.e. $\sigma = \gamma_{\Sigma^{\#}}(\sigma^{\#})[\Gamma]$.

Then:

$$ \{\sigma' : (\ell, \sigma) \to (\ell', \sigma')\} = \{\gamma_{\Sigma^{\#}}(\sigma'^{\#})[\Gamma'] : (\ell, \Gamma) \rightsquigarrow \hat{g} (\ell', \Gamma')\} \quad (12) $$

$$ \{(\ell', \sigma') : (\ell, \sigma) \to (\ell', \sigma')\} = \{\mathcal{H}_{p^{\#}}(\ell', \Gamma') : (\ell, \Gamma) \rightsquigarrow \hat{g}(\ell', \Gamma')\} \quad (13) $$

PROOF. The proof is similar to the one of Lemma C.1. Because we are a post-fixpoint instead of a fixpoint, there may be more "$\phi$" variables created than necessary, but they are still compensated by a corresponding binding in the graph.

Moreover, Theorem 5.3 still holds when $p^{\#}$ is a post-fixpoint instead of a fixpoint (see Theorem D.5). Thus, the Lemma is still true when $p^{\#}$ is a post-fixpoint. $\square$

THEOREM D.7 (SOUNDNESS AND COMPLETENESS OF THE SSA ABSTRACTION COMPUTATION (THEOREM C.10) WHEN $p^{\#}$ IS A POST-FIXPOINT). Let $p^{\#}$ be a post-fixpoint of $\mathcal{F}_{\mathbb{L} \to \Sigma_{\perp}^{\#}}$ and $\hat{g} = \text{graph}(p^{\#})$.

Then:

$$ \gamma_{\text{SSA}^{\#}}(p^{\#}, \hat{g}) = \to_{|\mathcal{S}^{*}} $$

PROOF. It suffices to redo all the proofs of Theorem C.10 starting from Lemma D.6. $\square$

## D.2 Fully-propagated subgraph

In this section, we provide and prove equivalent two characterizations of a fully-propagated subgraph $G$:

* In one, $G$ is the set of edges $(\ell, \ell')$ which are stable when $\mathcal{F}_{\mathbb{L} \to \Sigma_{\perp}^{\#}}$ is applied, i.e. the edges for which $p^{\#}[\ell']$ represents the successors of the states represented by $p^{\#}[\ell]$;

* In the other, $G$ is the part of the original program graph $\mathcal{G}$ for which $p^{\#}$ is a post-fixpoint.

The first characterization provides a computable definition of a fully-propagated subgraph, while the second will allow reusing the Theorems of the previous section.

First we introduce some notations. A subgraph $G \in \mathcal{P}(\mathbb{L} \times \mathbb{L})$ is a set of edges. We denote by:

* $\mathbb{L}_{|G} \triangleq \{\ell \mid \exists \ell' : (\ell, \ell') \in G \lor (\ell', \ell) \in G\}$ the set of locations that appear in $G$;

* $p^{\#}_{|G} \triangleq \{\ell \mapsto p^{\#}[\ell] \mid \ell \in \mathbb{L}_{|G}\}$ the restriction of $p^{\#} \in \mathbb{L} \to \Sigma_{\perp}^{\#}$ to the locations of $G$;

* $\mathcal{G}_{|G} \triangleq \{(\ell, \ell') \mapsto e \mid (\ell, \ell') \mapsto e \in \mathcal{G} \land (\ell, \ell') \in G\}$ the restriction of the original program graph $\mathcal{G}$ to the edges of the subgraph $G$;

* $\mathcal{F}_{\mathbb{L} \to \Sigma_{\perp}^{\#}}^{|G}(p^{\#}) \triangleq \left[ \begin{array}{l} \{x \in \mathcal{X} \mapsto x_{\ell_0}\} \quad \text{if } \ell' = \ell_0 \\ \sqcup_{\ell'} \{\mathcal{I}^{\#}[\text{instr}[\ell]](p^{\#}[\ell]) \mid \ell \in \text{preds}_{\mathcal{G}}(\ell')\} \quad \text{if } \ell' \neq \ell_0 \end{array} \right]$

where $\text{preds}_{\mathcal{G}}(\ell') \triangleq \{\ell \in \mathbb{L} \mid (\ell, \ell') \in \mathcal{G} \land \mathcal{G}[\ell, \ell'] \neq 0 \land p^{\#}[\ell] \neq \perp\}$ the restriction of the transfer function $\mathcal{F}_{\mathbb{L} \to \Sigma_{\perp}^{\#}}$ to $\mathcal{G}_{|G}$.

THEOREM D.8. Let $p^{\#} \in \mathbb{L} \to \Sigma_{\perp}^{\#}$ and $G \subseteq \text{dom} \mathcal{G}$. The following conditions are equivalent:

- The edges of $G$ are propagated in $p^{\#}$:

$$ \forall (\ell, \ell') \in G : \mathcal{G}[\ell, \ell'] \neq 0 \land p^{\#}[\ell] \neq \perp \Rightarrow \mathcal{I}^{\#}[\text{instr}[\ell]](p^{\#}[\ell]) \sqsubseteq^{\ell'} p^{\#}[\ell'] \quad (14) $$

- $p^{\#}_{|G}$ is a post-fixpoint of $\mathcal{F}_{\mathbb{L} \to \Sigma_{\perp}^{\#}}^{|G}$:

$$ p^{\#}_{|G} \sqsubseteq \mathcal{F}_{\mathbb{L} \to \Sigma_{\perp}^{\#}}^{|G}(p^{\#}_{|G}) \quad (15) $$

When either holds, we say that $G$ is a fully-propagated subgraph of $p^{\#}$.
LEMMA D.6 (LEMMA C.1 IN THE POST-FIXPOINT CASE). Let $p^{\#}$ be a post-fixpoint of $\mathcal{F}_{\mathbb{L} \to \Sigma_{\perp}^{\#}}$ and $\hat{g} = \text{graph}(p^{\#})$. Let $\ell' \in \mathbb{L}$ and $\ell \in \text{preds}(\ell')$. Let $\sigma^{\#} = p^{\#}[\ell]$ and $\sigma'^{\#} = p^{\#}[\ell']$. Let $\Gamma \mapsto \sigma \in \gamma_{\Sigma^{\#}}(\sigma^{\#})$, i.e. $\sigma = \gamma_{\Sigma^{\#}}(\sigma^{\#})[\Gamma]$.

Then:

$$ \{\sigma' : (\ell, \sigma) \to (\ell', \sigma')\} = \{\gamma_{\Sigma^{\#}}(\sigma'^{\#})[\Gamma'] : (\ell, \Gamma) \rightsquigarrow \hat{g} (\ell', \Gamma')\} \quad (12) $$

$$ \{(\ell', \sigma') : (\ell, \sigma) \to (\ell', \sigma')\} = \{\mathcal{H}_{p^{\#}}(\ell', \Gamma') : (\ell, \Gamma) \rightsquigarrow \hat{g}(\ell', \Gamma')\} \quad (13) $$

PROOF. The proof is similar to the one of Lemma C.1. Because we are a post-fixpoint instead of a fixpoint, there may be more "$\phi$" variables created than necessary, but they are still compensated by a corresponding binding in the graph.

Moreover, Theorem 5.3 still holds when $p^{\#}$ is a post-fixpoint instead of a fixpoint (see Theorem D.5). Thus, the Lemma is still true when $p^{\#}$ is a post-fixpoint. $\square$

THEOREM D.7 (SOUNDNESS AND COMPLETENESS OF THE SSA ABSTRACTION COMPUTATION (THEOREM C.10) WHEN $p^{\#}$ IS A POST-FIXPOINT). Let $p^{\#}$ be a post-fixpoint of $\mathcal{F}_{\mathbb{L} \to \Sigma_{\perp}^{\#}}$ and $\hat{g} = \text{graph}(p^{\#})$.

Then:

$$ \gamma_{\text{SSA}^{\#}}(p^{\#}, \hat{g}) = \to_{|\mathcal{S}^{*}} $$

PROOF. It suffices to redo all the proofs of Theorem C.10 starting from Lemma D.6. $\square$

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

## D.2 Fully-propagated subgraph

In this section, we provide and prove equivalent two characterizations of a fully-propagated subgraph $G$:

* In one, $G$ is the set of edges $(\ell, \ell')$ which are stable when $\mathcal{F}_{\mathbb{L} \to \Sigma_{\perp}^{\#}}$ is applied, i.e. the edges for which $p^{\#}[\ell']$ represents the successors of the states represented by $p^{\#}[\ell]$;

* In the other, $G$ is the part of the original program graph $\mathcal{G}$ for which $p^{\#}$ is a post-fixpoint.

The first characterization provides a computable definition of a fully-propagated subgraph, while the second will allow reusing the Theorems of the previous section.

First we introduce some notations. A subgraph $G \in \mathcal{P}(\mathbb{L} \times \mathbb{L})$ is a set of edges. We denote by:

* $\mathbb{L}|_G \triangleq \{\ell \mid \exists \ell' : (\ell, \ell') \in G \lor (\ell', \ell) \in G\}$ the set of locations that appear in $G$;

* $p^{\#}|_G \triangleq \{\ell \mapsto p^{\#}[\ell] \mid \ell \in \mathbb{L}|_G\}$ the restriction of $p^{\#} \in \mathbb{L} \to \Sigma_{\perp}^{\#}$ to the locations of $G$;

* $\mathcal{G}|_G \triangleq \{(\ell, \ell') \mapsto e \mid (\ell, \ell') \mapsto e \in \mathcal{G} \land (\ell, \ell') \in G\}$ the restriction of the original program graph $\mathcal{G}$ to the edges of the subgraph $G$;

* $\mathcal{F}|_{\mathbb{L} \to \Sigma_{\perp}^{\#}}^{[G]}(p^{\#}) \triangleq \left[ \begin{array}{ll} \{x \in \mathcal{X} \mapsto x_{\ell_0}\} & \text{if } \ell' = \ell_0 \\ \sqcup^{\ell'} \{\mathcal{I}^{\#}[\text{instr}[\ell]](p^{\#}[\ell]) \mid \ell \in \text{preds}_G(\ell')\} & \text{if } \ell' \neq \ell_0 \end{array} \right]$

where $\text{preds}_G(\ell') \triangleq \{\ell \in \mathbb{L} \mid (\ell, \ell') \in G \land \mathcal{G}[\ell, \ell'] \neq 0 \land p^{\#}[\ell] \neq \perp\}$ the restriction of the transfer function $\mathcal{F}_{\mathbb{L} \to \Sigma_{\perp}^{\#}}$ to $\mathcal{G}|_G$.

THEOREM D.8. Let $p^{\#} \in \mathbb{L} \to \Sigma_{\perp}^{\#}$ and $G \subseteq \text{dom} \mathcal{G}$. The following conditions are equivalent:

- The edges of $G$ are propagated in $p^{\#}$:

$$ \forall (\ell, \ell') \in G : \mathcal{G}[\ell, \ell'] \neq 0 \land p^{\#}[\ell] \neq \perp \Rightarrow \mathcal{I}^{\#}[\text{instr}[\ell]](p^{\#}[\ell]) \sqsubseteq^{\ell'} p^{\#}[\ell'] \quad (14) $$

- $p^{\#}|_G$ is a post-fixpoint of $\mathcal{F}|_{\mathbb{L} \to \Sigma_{\perp}^{\#}}^{[G]}$:

$$ p^{\#}|_G \sqsubseteq \mathcal{F}|_{\mathbb{L} \to \Sigma_{\perp}^{\#}}^{[G]}(p^{\#}|_G) \quad (15) $$

When either holds, we say that $G$ is a fully-propagated subgraph of $p^{\#}$.
PROOF.

• (15) ⇒ (14): If $(\ell, \ell') \in G$ then, by definition of $\mathcal{F}_{\mathbb{L} \to \Sigma_{\perp}}^{|G}$, $\exists \sigma^{\#} : p^{\#}[\ell'] = \mathcal{I}^{\#}[\mathrm{instr}[\ell]](p^{\#}[\ell]) \sqcup \ell'$
$\sigma^{\#}$. This means that $\mathcal{I}^{\#}[\mathrm{instr}[\ell]](p^{\#}[\ell]) \sqsubseteq \ell' p^{\#}[\ell']$ per Definition 6.1.

• (14) ⇒ (15): A standard property of semi-lattices is $\forall a, b, c : a \sqsubseteq b \wedge a \sqsubseteq c \Leftrightarrow a \sqsubseteq (b \sqcup c)$. Using the definition of $\mathcal{F}_{\mathbb{L} \to \Sigma_{\perp}}^{|G}$, this allows to conclude. □

The following theorem provides a computable definition of a suitable fully-propagated subgraph G:

COROLLARY D.9. Let $p^{\#} \in \mathbb{L} \to \Sigma_{\perp}^{\#}$. The set

$$ \max G(p^{\#}) \triangleq \{(\ell, \ell') \in \mathrm{dom} \, \mathcal{G} \mid \mathcal{G}[\ell, \ell'] = 0 \lor p^{\#}[\ell] = \perp \lor \mathcal{I}^{\#}[\mathrm{instr}[\ell]](p^{\#}[\ell]) \sqsubseteq \ell' p^{\#}[\ell']\} $$

is the maximal fully-propagated subgraph of $p^{\#}$.

Note that the theorems in this section are not restricted to $p^{\#} \in \mathbb{L} \to \Sigma_{\perp}^{\#}$ and works for any flow-sensitive abstraction; in particular it can be readily extended in the case where $p^{\#}$ is combined with other abstract domains (e.g., to have a more precise discovery of dead locations and branches).

## D.3 An incrementally complete transfer function

We can now complete the proof:

THEOREM D.10 (INCREMENTAL SSA GRAPHS ARE COMPLETE).

Let $p^{\#} \in \mathbb{L} \to \Sigma_{\perp}^{\#}$, $G = \max G(p^{\#})$, and $\hat{g} = \mathrm{graph}(\mathcal{F}_{\mathbb{L} \to \Sigma_{\perp}^{\#}}(p^{\#}))$. Then: $\gamma_{SSA^{\#}}(p^{\#}, \hat{g}|_G) \subseteq \rightarrow_{|S^{*}}$.

PROOF. We define $S|_G = \{(\ell, \sigma) \in S \mid \ell \in \mathbb{L}|_G\}$.

$$
\begin{align*}
\gamma_{SSA^{\#}}(p^{\#}, \hat{g}|_G) &= \gamma_{SSA^{\#}}(p^{\#}|_G, \hat{g}|_G) && \text{(by definition of } \gamma_{SSA^{\#}}) \\
&= \gamma_{SSA^{\#}}(p^{\#}|_G, \mathrm{graph}(p^{\#}|_G)) && \text{(by definition of the graph operator)} \\
&= \rightarrow_{|(S|_G \cap S^*)} && \text{(by Theorem D.7 and Theorem D.8)} \\
&\subseteq \rightarrow_{|S^*} && \text{(by definition of restriction)}
\end{align*}
$$

□

Note that if the intermediate versions of the SSA graph produced by $\mathcal{F}'_{SSA^{\#}}$ are now complete, $\mathcal{F}'_{SSA^{\#}}$ is not monotonic, because $\max G$ is not monotone: if $\mathcal{F}_{\mathbb{L} \to \Sigma_{\perp}^{\#}}(p^{\#})$ always represents more states than $p^{\#}$, there may be fewer fully-propagated locations in $(\mathcal{F}_{\mathbb{L} \to \Sigma_{\perp}^{\#}}(p^{\#}))$ than in $p^{\#}$.

## E USE CASE : SINGLE-PASS OPTIMIZED TRANSLATIONS TO SSA

This section describes our experiments to use SSA translation based on abstract interpretation to compile (a subset of) C to the LLVM IR (which is in SSA form).

*Implementation.* Our goal is to demonstrate the feasibility of using dataflow analysis as a basis for SSA translation. We have implemented the algorithms described in the paper as a small plugin for the FRAMA-C platform, and used the LLVM intermediate representation as the target of our translation. In particular, we have implemented the symbolic expression analysis of Section 4, followed by one call to the graph operator, modified to directly produce LLVM code instead of SSA graphs. This second, linear, pass consists on traversing all the subterms in the global value
PROOF.

• (15) ⇒ (14): If $(\ell, \ell') \in G$ then, by definition of $\mathcal{F}_{\mathcal{L} \to \Sigma_{\perp}}^{|G}$, $\exists \sigma^{\#} : p^{\#}[\ell'] = \mathcal{I}^{\#}[\mathrm{instr}[\ell]](p^{\#}[\ell]) \sqcup \ell'$
$\sigma^{\#}$. This means that $\mathcal{I}^{\#}[\mathrm{instr}[\ell]](p^{\#}[\ell]) \sqsubseteq \ell' p^{\#}[\ell']$ per Definition 6.1.

• (14) ⇒ (15): A standard property of semi-lattices is $\forall a, b, c : a \sqsubseteq b \wedge a \sqsubseteq c \Leftrightarrow a \sqsubseteq (b \sqcup c)$. Using the definition of $\mathcal{F}_{\mathcal{L} \to \Sigma_{\perp}}^{|G}$, this allows to conclude. □

The following theorem provides a computable definition of a suitable fully-propagated subgraph G:

COROLLARY D.9. Let $p^{\#} \in \mathcal{L} \to \Sigma_{\perp}^{\#}$. The set

$$ \max G(p^{\#}) \triangleq \{(\ell, \ell') \in \mathrm{dom} \ \mathcal{G} \mid \mathcal{G}[\ell, \ell'] = 0 \lor p^{\#}[\ell] = \perp \lor \mathcal{I}^{\#}[\mathrm{instr}[\ell]](p^{\#}[\ell]) \sqsubseteq \ell' p^{\#}[\ell']\} $$

is the maximal fully-propagated subgraph of $p^{\#}$.

Note that the theorems in this section are not restricted to $p^{\#} \in \mathcal{L} \to \Sigma_{\perp}^{\#}$ and works for any flow-sensitive abstraction; in particular it can be readily extended in the case where $p^{\#}$ is combined with other abstract domains (e.g., to have a more precise discovery of dead locations and branches).

## D.3 An incrementally complete transfer function

We can now complete the proof:

THEOREM D.10 (INCREMENTAL SSA GRAPHS ARE COMPLETE).

Let $p^{\#} \in \mathcal{L} \to \Sigma_{\perp}^{\#}$, $G = \max G(p^{\#})$, and $\hat{g} = \mathrm{graph}(\mathcal{F}_{\mathcal{L} \to \Sigma_{\perp}^{\#}}(p^{\#}))$. Then: $\gamma_{SSA^{\#}}(p^{\#}, \hat{g}|_G) \subseteq \rightarrow_{|S^{*}}$.

PROOF. We define $S|_G = \{(\ell, \sigma) \in S \mid \ell \in \mathcal{L}|_G\}$.

$$
\begin{align*}
\gamma_{SSA^{\#}}(p^{\#}, \hat{g}|_G) &= \gamma_{SSA^{\#}}(p^{\#}|_G, \hat{g}|_G) && (\text{by definition of } \gamma_{SSA^{\#}}) \\
&= \gamma_{SSA^{\#}}(p^{\#}|_G, \mathrm{graph}(p^{\#}|_G)) && (\text{by definition of the graph operator}) \\
&\rightarrow_{|S|_G \cap S^*} && (\text{by Theorem D.7 and Theorem D.8}) \\
&\subseteq \rightarrow_{|S^*} && (\text{by definition of restriction})
\end{align*}
$$

□

Note that if the intermediate versions of the SSA graph produced by $\mathcal{F}'_{SSA^{\#}}$ are now complete, $\mathcal{F}'_{SSA^{\#}}$ is not monotonic, because $\max G$ is not monotone: if $\mathcal{F}_{\mathcal{L} \to \Sigma_{\perp}^{\#}}(p^{\#})$ always represents more states than $p^{\#}$, there may be fewer fully-propagated locations in $(\mathcal{F}_{\mathcal{L} \to \Sigma_{\perp}^{\#}}(p^{\#}))$ than in $p^{\#}$.

## E USE CASE : SINGLE-PASS OPTIMIZED TRANSLATIONS TO SSA

This section describes our experiments to use SSA translation based on abstract interpretation to compile (a subset of) C to the LLVM IR (which is in SSA form).

*Implementation.* Our goal is to demonstrate the feasibility of using dataflow analysis as a basis for SSA translation. We have implemented the algorithms described in the paper as a small plugin for the FRAMA-C platform, and used the LLVM intermediate representation as the target of our translation. In particular, we have implemented the symbolic expression analysis of Section 4, followed by one call to the graph operator, modified to directly produce LLVM code instead of SSA graphs. This second, linear, pass consists on traversing all the subterms in the global value
graph, determining for each the location where to place the instruction, and then inserting the
corresponding instruction in the LLVM IR.

We have experimented with several possibilities for finding where to insert instructions. The first is to use our scope function. This corresponds to the "schedule early" strategy of Click [1995]. An alternative is change our symbolic expressions so that scope becomes explicit; i.e. the language of symbolic expression becomes $e \in E \triangleq L \times (z | v | e \diamond e)$. It is easy to change the analysis to register the current location in the newly created expressions. The benefit of this technique is that the SSA translation is closer to original program and to what a usual SSA translation would perform; the drawback is that the global value numbering detects fewer equalities between symbolic variables. The time below is given for this alternative version.

A necessary change is to insert terminator instructions (branches and conditional branches) instead of using guards and non-determinism. Formally, we define terminators as term $\in$ Terminator $\triangleq$ Exit $|$ Jmp($\ell$) $|$ JmpIf($e, \ell, \ell$), we replace the graph of the original program by a mapping $L \rightarrow$ Terminator (using a program expression for the condition), and we replace the guards on the SSA graphs by a mapping $L \rightarrow$ Terminator (using symbolic expression for the condition). The semantics is the standard one.

The implementation of this plugin, that does SSA translation, Global value numbering, global code motion, and sparse conditional constant propagation, required only 970 lines of OCaml code (measured by Sloccount), excluding a 316 lines implementation of Okasaki's Patricia tries [Okasaki and Gill 1998], and code implementing the iterative and recursive iteration strategy on Bourdoncle's [Bourdoncle 1993] WTO (183 lines). The parser and WTO calculation is provided by FRAMA-C, and the LLVM translation by the standard LLVM OCaml bindings.

*Evaluation.* We have used this implementation to evaluate both the soundness and performance of our algorithm. In languages like C, the variables are addressable, in which case they cannot be directly translated to SSA (Clang, for instance, does not translate C variables to SSA variables and delegates this process to later passes). To evaluate our algorithm on large programs containing only non-addressable variables, we have used the CSMITH [Yang et al. 2011] C generator, using options to generate only non-addressable integer variables (but complex unstructured control flow), to generate 100 large random programs (in particular, we increased CSMITH option -max-block-size to 10 to generate larger files). The median size of the files is 144kb, the largest is weighting 692kb. These are very large C file, and the FRAMA-C parser (whose performance are usually acceptable) took more than 5 minutes just to parse some of these files.

We used the FRAMA-C parser on this program, our dataflow analysis to generate an SSA graph followed by a linear pass to translate it to the LLVM Intermediate Representation; finally we used LLVM (version 13) to compile the result to native x86 code, that we executed. We then compared the result to a native LLVM compilation. All tests were executed on a standard laptop (Intel i7-8850H CPU @ 2.60GHz). The code for the experiment and its results can be retrieved at https://doi.org/10.5281/zenodo.7152678.

*Soundness.* We obtained the following results: all the 100 files provided the same result as the execution of the LLVM version. In another run we generated 100 other files without the safe-math option of CSMITH (that add guards before undefined behaviors, like overflowing shifts or division by zero), in which case we found a difference for 18 files, all of them explainable by an actual undefined behavior in the code (this was checked using the FRAMA-C/EVA [Bühler et al. 2017] abstract interpreter).

*Performance.* We measured the time needed for the dataflow analysis pass (Table 1) in 4 configurations: by choosing a fixpoint iteration strategy [Bourdoncle 1993] (Recursive or Iterative), or by
graph, determining for each the location where to place the instruction, and then inserting the
corresponding instruction in the LLVM IR.

We have experimented with several possibilities for finding where to insert instructions. The first is to use our scope function. This corresponds to the "schedule early" strategy of Click [1995]. An alternative is change our symbolic expressions so that scope becomes explicit; i.e. the language of symbolic expression becomes $e \in E \triangleq L \times (z | v | e \diamond e)$. It is easy to change the analysis to register the current location in the newly created expressions. The benefit of this technique is that the SSA translation is closer to original program and to what a usual SSA translation would perform; the drawback is that the global value numbering detects fewer equalities between symbolic variables. The time below is given for this alternative version.

A necessary change is to insert terminator instructions (branches and conditional branches) instead of using guards and non-determinism. Formally, we define terminators as term ∈ Terminator ≜ Exit | Jmp(t) | JmpIf(e, t, t), we replace the graph of the original program by a mapping $L \rightarrow Terminator$ (using a program expression for the condition), and we replace the guards on the SSA graphs by a mapping $L \rightarrow Terminator$ (using symbolic expression for the condition). The semantics is the standard one.

The implementation of this plugin, that does SSA translation, Global value numbering, global code motion, and sparse conditional constant propagation, required only 970 lines of OCaml code (measured by Sloccount), excluding a 316 lines implementation of Okasaki's Patricia tries [Okasaki and Gill 1998], and code implementing the iterative and recursive iteration strategy on Bourdoncle's [Bourdoncle 1993] WTO (183 lines). The parser and WTO calculation is provided by FRAMA-C, and the LLVM translation by the standard LLVM OCaml bindings.

*Evaluation.* We have used this implementation to evaluate both the soundness and performance of our algorithm. In languages like C, the variables are addressable, in which case they cannot be directly translated to SSA (Clang, for instance, does not translate C variables to SSA variables and delegates this process to later passes). To evaluate our algorithm on large programs containing only non-addressable variables, we have used the CSMITH [Yang et al. 2011] C generator, using options to generate only non-addressable integer variables (but complex unstructured control flow), to generate 100 large random programs (in particular, we increased CSMITH option -max-block-size to 10 to generate larger files). The median size of the files is 144kb, the largest is weighting 692kb. These are very large C file, and the FRAMA-C parser (whose performance are usually acceptable) took more than 5 minutes just to parse some of these files.

We used the FRAMA-C parser on this program, our dataflow analysis to generate an SSA graph followed by a linear pass to translate it to the LLVM Intermediate Representation; finally we used LLVM (version 13) to compile the result to native x86 code, that we executed. We then compared the result to a native LLVM compilation. All tests were executed on a standard laptop (Intel i7-8850H CPU @ 2.60GHz). The code for the experiment and its results can be retrieved at https://doi.org/10.5281/zenodo.7152678.

*Soundness.* We obtained the following results: all the 100 files provided the same result as the execution of the LLVM version. In another run we generated 100 other files without the safe-math option of CSMITH (that add guards before undefined behaviors, like overflowing shifts or division by zero), in which case we found a difference for 18 files, all of them explainable by an actual undefined behavior in the code (this was checked using the FRAMA-C/EVA [Bühler et al. 2017] abstract interpreter).

*Performance.* We measured the time needed for the dataflow analysis pass (Table 1) in 4 configurations: by choosing a fixpoint iteration strategy [Bourdoncle 1993] (Recursive or Iterative), or by
<table><caption>Table 1. Time spent in SSA translation in the generated programs (and compared to a standard compiler run).</caption><thead><tr><th rowspan="2"></th><th rowspan="2">Clang</th><th colspan="3">With Constant Propagation</th><th colspan="3">Without Constant Propagation</th></tr><tr><th>Iterative (/Clang)</th><th>Recursive (/Clang)</th><th>Clang →LLVM</th><th>Iterative (/Clang)</th><th>Recursive (/Clang)</th><th>Clang →LLVM</th></tr></thead><tbody><tr><th>Min</th><td>0.06s</td><td>0.207s (×1.70)</td><td>0.205s (×1.66)</td><td>0s</td><td>0.205s (×2.36)</td><td>0.204s (×2.34)</td><td>0s</td></tr><tr><th>Median</th><td>0.29s</td><td>0.601s (×2.19)</td><td>0.612s (×2.19)</td><td>0.027s</td><td>0.814s (×3.30)</td><td>0.791s (×3.27)</td><td>0.284s</td></tr><tr><th>Average</th><td>0.359s</td><td>0.754s (×2.48)</td><td>0.759s (×2.48)</td><td>0.365s</td><td>1.230s (×3.32)</td><td>1.220s (×3.30)</td><td>1.084s</td></tr><tr><th>Max</th><td>1.2s</td><td>2.270s (×3.70)</td><td>2.343s (×3.73)</td><td>0.127s</td><td>4.572s (×5.57)</td><td>5.756s (×5.33)</td><td>7.947s</td></tr></tbody></table>

enabling or disabling the combination of the SSA domain with constant propagation and dead code elimination. We provide this time in seconds, but also as a ratio compared to the performance of a standard compiler (using `clang` to compile the file). For instance, at worst the iterative strategy with constant propagation took 2.270s, and at worst it took 3.70 times the time spent by `clang` to compile the file. We can observe that the choice between different iteration strategies does not significantly impact the performance of the analysis, contrary to the use of constant propagation and dead code elimination. Furthermore, in a previous version of the program, we used the standard Map of OCaml instead of Okasaki maps to implement our abstract stores (as done in Astrée [Blanchet et al. 2002]), in which case the performance was noticeably slower (e.g. the analysis could take up to one minute).

We also measured the time for the linear compilation pass translating our SSA graphs to `LLVM IR` (with and without constant propagation, as the choice of an iteration strategy does not impact the result of the dataflow analysis). Again, the use of constant propagation and dead code elimination allows spending less time in this phase. The time spent in this phase is generally low except in some cases; a large part of this is due to a naive translation generating one `LLVM` basic block per C instruction. The majority of the work in this phase is spent in `LLVM`, and it is probable that the exported OCaml bindings do not provide the most efficient way of building the program in the intermediate representation.

Finally, we also measured the maximum number of iterations required to attain the fixpoint when analyzing a strongly connected component, which was 6 in the case of an iterative strategy and 3 for the iterative strategy. This contrasts with the theoretical maximum, which corresponds to the number of program variables (usually several thousands in our tests).

*Conclusions.* Doing SSA translation using a dataflow analysis is a sound and simple way to perform SSA translation. The soundness is not a surprise since we provided the proof for all of our algorithms, but the experimental evaluation confirms that it works in practice.

Furthermore, the time spent doing so is in the order of magnitude compatible for incorporation in a compiler: if we add incorporated our SSA translation pass inside a compiler, the maximum observed slowdown would have been ×6.57 (i.e. 5.57 + 1), which is slower but acceptable. This is a maximum, as such an incorporation would lead to removing existing passes in `clang`; furthermore, additional engineering (such as switching from OCaml to C) could further improve the performance. One of the reasons for this efficiency is that fixpoint iteration with the symbolic expression domain is usually obtained using few iterations, even in large programs. The other part is explained by the use of functional maps for low-complexity operations on abstract stores. One crucial engineering decision in our analysis performance was the use of Okasaki maps [Okasaki and Gill 1998] to implement the abstract stores, instead of the more common binary search trees [Blanchet et al. 2002], as otherwise the time spent in the `⊤f` operation dominates the time spent in the analysis. Okasaki maps allow more efficient handling of the parts of the abstract store that have not changed between when the different states that are joined with `⊤f`. Finally, combining SSA translation with other analyses such as constant propagation and dead code elimination can significantly improve the time spent in the
<table><caption>Table 1. Time spent in SSA translation in the generated programs (and compared to a standard compiler run).</caption><thead><tr><th rowspan="2"></th><th rowspan="2">Clang</th><th colspan="3">With Constant Propagation</th><th colspan="3">Without Constant Propagation</th></tr><tr><th>Iterative (/Clang)</th><th>Recursive (/Clang)</th><th>Clang →LLVM</th><th>Iterative (/Clang)</th><th>Recursive (/Clang)</th><th>Clang →LLVM</th></tr></thead><tbody><tr><th>Min</th><td>0.06s</td><td>0.207s (×1.70)</td><td>0.205s (×1.66)</td><td>0s</td><td>0.205s (×2.36)</td><td>0.204s (×2.34)</td><td>0s</td></tr><tr><th>Median</th><td>0.29s</td><td>0.601s (×2.19)</td><td>0.612s (×2.19)</td><td>0.027s</td><td>0.814s (×3.30)</td><td>0.791s (×3.27)</td><td>0.284s</td></tr><tr><th>Average</th><td>0.359s</td><td>0.754s (×2.48)</td><td>0.759s (×2.48)</td><td>0.365s</td><td>1.230s (×3.32)</td><td>1.220s (×3.30)</td><td>1.084s</td></tr><tr><th>Max</th><td>1.2s</td><td>2.270s (×3.70)</td><td>2.343s (×3.73)</td><td>0.127s</td><td>4.572s (×5.57)</td><td>5.756s (×5.33)</td><td>7.947s</td></tr></tbody></table>

enabling or disabling the combination of the SSA domain with constant propagation and dead code elimination. We provide this time in seconds, but also as a ratio compared to the performance of a standard compiler (using `clang` to compile the file). For instance, at worst the iterative strategy with constant propagation took 2.270s, and at worst it took 3.70 times the time spent by `clang` to compile the file. We can observe that the choice between different iteration strategies does not significantly impact the performance of the analysis, contrary to the use of constant propagation and dead code elimination. Furthermore, in a previous version of the program, we used the standard Map of OCaml instead of Okasaki maps to implement our abstract stores (as done in Astrée [Blanchet et al. 2002]), in which case the performance was noticeably slower (e.g. the analysis could take up to one minute).

We also measured the time for the linear compilation pass translating our SSA graphs to `LLVM IR` (with and without constant propagation, as the choice of an iteration strategy does not impact the result of the dataflow analysis). Again, the use of constant propagation and dead code elimination allows spending less time in this phase. The time spent in this phase is generally low except in some cases; a large part of this is due to a naive translation generating one `LLVM` basic block per C instruction. The majority of the work in this phase is spent in `LLVM`, and it is probable that the exported OCaml bindings do not provide the most efficient way of building the program in the intermediate representation.

Finally, we also measured the maximum number of iterations required to attain the fixpoint when analyzing a strongly connected component, which was 6 in the case of an iterative strategy and 3 for the iterative strategy. This contrasts with the theoretical maximum, which corresponds to the number of program variables (usually several thousands in our tests).

*Conclusions.* Doing SSA translation using a dataflow analysis is a sound and simple way to perform SSA translation. The soundness is not a surprise since we provided the proof for all of our algorithms, but the experimental evaluation confirms that it works in practice.

Furthermore, the time spent doing so is in the order of magnitude compatible for incorporation in a compiler: if we add incorporated our SSA translation pass inside a compiler, the maximum observed slowdown would have been ×6.57 (i.e. 5.57 + 1), which is slower but acceptable. This is a maximum, as such an incorporation would lead to removing existing passes in `clang`; furthermore, additional engineering (such as switching from OCaml to C) could further improve the performance. One of the reason for this efficiency is that fixpoint iteration with the symbolic expression domain is usually obtained using few iterations, even in large programs. The other part is explained by the use of functional maps for low-complexity operations on abstract stores. One crucial engineering decision in our analysis performance was the use of Okasaki maps [Okasaki and Gill 1998] to implement the abstract stores, instead of the more common binary search trees [Blanchet et al. 2002], as otherwise the time spent in the `⊤f` operation dominates the time spent in the analysis. Okasaki maps allow more efficient handling of the parts of the abstract store that have not changed between when the different states that are joined with `⊤f`. Finally, combining SSA translation with other analyses such as constant propagation and dead code elimination can significantly improve the time spent in the
*analysis*: in this case, incorporating our pass in LLVM would make it only 4.73 time slower (instead of 6.57 times), at worst.

Whether, with careful engineering, implementing compilers as a single-pass combination of modular abstract domains, can outperform the existing designs as a sequence of passes, is an open question, but our initial results indicate that the single-pass design could be competitive in terms of speed of compilation.

Received 2022-07-07; accepted 2022-11-07
*analysis:* in this case, incorporating our pass in LLVM would make it only 4.73 time slower (instead of 6.57 times), at worst.

Whether, with careful engineering, implementing compilers as a single-pass combination of modular
abstract domains, can outperform the existing designs as a sequence of passes, is an open question, but
our initial results indicate that the single-pass design could be competitive in terms of speed of
compilation.

Received 2022-07-07; accepted 2022-11-07