Skip to Main content Skip to Navigation
New interface
Journal articles

SSA translation is an abstract interpretation

Matthieu Lemerre 1 
1 LSL - Laboratoire Sûreté des Logiciels
DILS - Département Ingénierie Logiciels et Systèmes : DRT/LIST/DILS
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.
Document type :
Journal articles
Complete list of metadata
Contributor : Matthieu Lemerre Connect in order to contact the contributor
Submitted on : Saturday, November 12, 2022 - 4:52:55 AM
Last modification on : Thursday, November 17, 2022 - 3:37:30 AM


Publisher files allowed on an open archive



Matthieu Lemerre. SSA translation is an abstract interpretation. Proceedings of the ACM on Programming Languages, 2023, POPL 2023 - the 50th ACM SIGPLAN Symposium on Principles of Programming Languages, 7, pp.65. ⟨10.1145/3571258⟩. ⟨cea-03849637⟩



Record views


Files downloads