SSA Translation Is an Abstract Interpretation
summary
Claim: SSA translation is an abstract interpretation and can be implemented as a simple dataflow analysis that is sound and complete, avoids dominance-based algorithms, and names symbolic variables with control-location keys to terminate loops and produce cyclic term graphs. Implementation (under 1,000 LOC C) performs SSA translation plus optimistic GVN, sparse conditional constant propagation, and loop-invariant code motion in one pass, yields a correct SSA graph after fixpointing, runs practicably (about 7× slowdown unoptimized), and is used on C and machine code for verification.
AI-written summary · about
chapters (12)
- 0:00Intro
- 0:34SSA Translation Abstract Interpretation
- 1:45Why is this important?
- 5:37Symbolic execution (≈ single-path SSA translation)
- 10:43Meaning, soundness and completeness
- 12:46Where do we loose precision? Absence of control flow
- 14:11Computing the SSA graph: SSA translation by dataflow analysis
- 16:25Operational semantics of the SSA graph
- 17:22Bisimulation & homomorphism between transition systems
- 18:47Evaluation & Artifact
- 20:14Conclusions
- 23:47Example: Single-pass machine code decompilation to SSA
related talks
18mCompiling with Abstract Interpretation
18mSSA is Freyd Categories
22mMechanised Semantics for Gated Static Single Assignment
28mSSA CFG Yul A new viaIR backend
36mSound and Complete Refinement for SSA with Substructural Effects
29mA Flow-Insensitive-Complete Program Representation
09mRetargeting an Abstract Interpreter for a New Language by Partial Evaluation (Short Paper)
24mOptimism in Equality Saturation