research-article

Open access

SSA Translation Is an Abstract Interpretation

Author:

Matthieu LemerreAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 7, Issue POPL

Article No.: 65, Pages 1895 - 1924

https://doi.org/10.1145/3571258

Published: 11 January 2023 Publication History

Abstract

Static single assignment (SSA) form is a popular intermediate representation that helps implement useful static analyses, including global value numbering (GVN), sparse dataflow analyses, or SMT-based abstract interpretation or model checking. However, the precision of the SSA translation itself depends on static analyses, and a priori static analysis is even indispensable in the case of low-level input languages like machine code.

To solve this chicken-and-egg problem, we propose to turn the SSA translation into a standard static analysis based on abstract interpretation. This allows the SSA translation to be combined with other static analyses in a single pass, taking advantage of the fact that it is more precise to combine analyses than applying passes in sequence.

We illustrate the practicality of these results by writing a simple dataflow analysis that performs SSA translation, optimistic global value numbering, sparse conditional constant propagation, and loop-invariant code motion in a single small pass; and by presenting a multi-language static analyzer for both C and machine code that uses the SSA abstract domain as its main intermediate representation.

References

[1]

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

Digital Library

[2]

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

[3]

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

Digital Library

[4]

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

[5]

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

[6]

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

[7]

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

Digital Library

[8]

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 (2002), Oct., 85–108. https://doi.org/10.1007/3-540-36377-7_5

[9]

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, Ahmed Bouajjani and David Monniaux (Eds.) (VMCAI 2017, Vol. 10145). Springer, 112–130. https://doi.org/10.1007/978-3-319-52234-0_7

[10]

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

[11]

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

[12]

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

Digital Library

[13]

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

Digital Library

[14]

David Brumley, JongHyup Lee, Edward J. Schwartz, and Maverick Woo. 2013. Native x86 Decompilation 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

[15]

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

Digital Library

[16]

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

Digital Library

[17]

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

[18]

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, David S. Wise (Ed.) (POPL 1991). 55–66. https://doi.org/10.1145/99583.99594

Digital Library

[19]

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, Kurt Jensen and Andreas Podelski (Eds.) (TACAS 2004). Springer, 168–176. https://doi.org/10.1007/978-3-540-24730-2_15

[20]

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

Digital Library

[21]

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

Digital Library

[22]

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

[23]

Patrick Cousot. 1977. Asynchronous iterative methods for solving a fixed point system of monotone equations in a complete lattice. 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

[24]

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

[25]

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

Digital Library

[26]

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

Digital Library

[27]

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

Digital Library

[28]

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

Digital Library

[29]

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

[30]

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 (1991), oct, 451–490. https://doi.org/10.1145/115372.115320

Digital Library

[31]

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

Digital Library

[32]

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, Christophe Dubach and Jingling Xue (Eds.) (CC 2018). ACM, 163–173. https://doi.org/10.1145/3178372.3179503

Digital Library

[33]

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

Digital Library

[34]

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

[35]

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, Gilles Barthe, Geoff Sutcliffe, and Margus Veanes (Eds.) (EPiC Series in Computing, Vol. 57). EasyChair, 363–380. https://doi.org/10.29007/dc9b

[36]

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, Barbara Jobstmann and K. Rustan M. Leino (Eds.) (VMCAI 2016). Springer, 85–103. https://doi.org/10.1007/978-3-662-49122-5_4

Digital Library

[37]

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

[38]

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

[39]

Sebastian Hack. 2016. SSA reconstruction (1st ed.).

[40]

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

Digital Library

[41]

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

Digital Library

[42]

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, Supratik Chakraborty and Jorge A. Navas (Eds.) (Lecture Notes in Computer Science, Vol. 12031). Springer, 1–18. https://doi.org/10.1007/978-3-030-41600-3_1

[43]

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

Digital Library

[44]

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

Digital Library

[45]

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, Neil D. Jones and Markus Müller-Olm (Eds.) (VMCAI 2009). Springer, 214–228. https://doi.org/10.1007/978-3-540-93900-9_19

Digital Library

[46]

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

Digital Library

[47]

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

Digital Library

[48]

Matthieu Lemerre. 2023. SSA Translation is an Abstract Interpretation (full version with appendices). CEA, LIST. https://binsec.github.io/assets/publications/papers/2023-popl-full-with-appendices.pdf

[49]

Matthieu Lemerre. 2023. SSA Translation is an Abstract Interpretation (artifact). CEA, LIST. https://doi.org/10.1145/3554341

Digital Library

[50]

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

Digital Library

[51]

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, Matt Kaufmann and Lawrence C. Paulson (Eds.) (Lecture Notes in Computer Science, Vol. 6172). Springer, 371–386. https://doi.org/10.1007/978-3-642-14052-5_26

Digital Library

[52]

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). 348–363. https://doi.org/10.1007/11609773_23

Digital Library

[53]

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

Digital Library

[54]

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

[55]

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

[56]

Olivier Nicole, Matthieu Lemerre, and Xavier Rival. 2021. Binsec/Codex, an abstract interpreter to verify safety and security properties of systems code. https://binsec.github.io/assets/publications/papers/2021-rtas-technical-report-analysis.pdf

[57]

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, Bernd Finkbeiner and Thomas Wies (Eds.) (Lecture Notes in Computer Science, Vol. 13182). Springer, 219–241. https://doi.org/10.1007/978-3-030-94583-1_11

Digital Library

[58]

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

[59]

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, Jeremy Gibbons (Ed.) (Haskell 2010). ACM, 121–134. https://doi.org/10.1145/1863523.1863539

Digital Library

[60]

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

[61]

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

Digital Library

[62]

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

Digital Library

[63]

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

Digital Library

[64]

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, Bernhard Steffen and Giorgio Levi (Eds.) (Lecture Notes in Computer Science, Vol. 2937). Springer, 252–266. https://doi.org/10.1007/978-3-540-24622-0_21

[65]

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.

[66]

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

Digital Library

[67]

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

[68]

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

Digital Library

[69]

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

[70]

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, Ron K. Cytron and Peter Lee (Eds.) (POPL 1995). 62–73. https://doi.org/10.1145/199448.199464

Digital Library

[71]

James Stanier. 2016. Graphs and Gating Functions (1st ed.).

[72]

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, Albert Cohen (Ed.) (Lecture Notes in Computer Science, Vol. 8409). Springer, 18–39. https://doi.org/10.1007/978-3-642-54807-9_2

[73]

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

[74]

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

Digital Library

[75]

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

Digital Library

[76]

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, Jian-Jia Chen and Aviral Shrivastava (Eds.) (LCTES 2019). 213–218. https://doi.org/10.1145/3316482.3326354

Digital Library

[77]

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

Digital Library

[78]

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, John Field and Michael Hicks (Eds.) (POPL 2012). 427–440. https://doi.org/10.1145/2103656.2103709

Digital Library

Cited By

Simonnet JLemerre MSighireanu M(2024)A Dependent Nominal Physical Type System for Static Analysis of Memory in Low Level CodeProceedings of the ACM on Programming Languages10.1145/36897128:OOPSLA2(30-59)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689712
Negrini LPresotto SFerrara PZaffanella ECortesi AArceri VPasqua M(2024)Stability: An Abstract Domain for the Trend of Variation of Numerical VariablesProceedings of the 10th ACM SIGPLAN International Workshop on Numerical and Symbolic Abstract Domains10.1145/3689609.3689995(10-17)Online publication date: 17-Oct-2024
https://dl.acm.org/doi/10.1145/3689609.3689995
Lesbre DLemerre M(2024)Compiling with Abstract InterpretationProceedings of the ACM on Programming Languages10.1145/36563928:PLDI(368-393)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656392

Index Terms

SSA Translation Is an Abstract Interpretation
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification
  2. Software notations and tools
    1. Compilers
2. Theory of computation
  1. Logic
    1. Abstraction
    2. Equational logic and rewriting
  2. Semantics and reasoning
    1. Program reasoning
      1. Program analysis
      2. Program verification

Recommendations

Control-flow analysis of function calls and returns by abstract interpretation

Abstract interpretation techniques are used to derive a control-flow analysis for a simple higher-order functional language. The analysis approximates the interprocedural control-flow of both function calls and returns in the presence of first-class ...
A²I: abstract² interpretation

The fundamental idea of Abstract² Interpretation (A²I), also called meta-abstract interpretation, is to apply abstract interpretation to abstract interpretation-based static program analyses. A²I is generally meant to use abstract interpretation to ...
Deriving escape analysis by abstract interpretation

Escape analysis of object-oriented languages approximates the set of objects which do not escape from a given context. If we take a method as context, the non-escaping objects can be allocated on its activation stack; if we take a thread, Java ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 7, Issue POPL

January 2023

2196 pages

EISSN:2475-1421

DOI:10.1145/3554308

Editor:

Issue’s Table of Contents

Copyright © 2023 Owner/Author.

This work is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 January 2023

Published in PACMPL Volume 7, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
1,970
Total Downloads

Downloads (Last 12 months)764
Downloads (Last 6 weeks)67

Reflects downloads up to 14 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Simonnet JLemerre MSighireanu M(2024)A Dependent Nominal Physical Type System for Static Analysis of Memory in Low Level CodeProceedings of the ACM on Programming Languages10.1145/36897128:OOPSLA2(30-59)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689712
Negrini LPresotto SFerrara PZaffanella ECortesi AArceri VPasqua M(2024)Stability: An Abstract Domain for the Trend of Variation of Numerical VariablesProceedings of the 10th ACM SIGPLAN International Workshop on Numerical and Symbolic Abstract Domains10.1145/3689609.3689995(10-17)Online publication date: 17-Oct-2024
https://dl.acm.org/doi/10.1145/3689609.3689995
Lesbre DLemerre M(2024)Compiling with Abstract InterpretationProceedings of the ACM on Programming Languages10.1145/36563928:PLDI(368-393)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656392
Bautista SJensen TMontagu B(2024)An input–output relational domain for algebraic data types and functional arraysFormal Methods in System Design10.1007/s10703-024-00456-zOnline publication date: 13-Jun-2024
https://doi.org/10.1007/s10703-024-00456-z

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents