WG211/M21Blazy

Static Single Assignment (SSA) has proven useful for implementing many static-analysis and optimisation passes, thanks to its structural and semantic properties. However, SSA phi-instructions depend on control-flow, whereas many advanced analysis passes are data-flow dependent, limiting these inherently. One solution is to use a richer intermediate representation, namely Gated-SSA, which partially transforms control-flow dependencies into data-dependencies, and encode enough information to make the semantics of phi-instructions independent of control-flow. Gated-SSA has been successfully applied in various practical contexts of optimising compilation, and yet, no reference implementation or semantics have been described in the literature.

In this talk, we formulate an operational semantics for Gated-SSA. We also provide a formal specification of a translation from SSA to Gated-SSA, and we prove it is semantics preserving. To demonstrate the practicality of our approach, we implement this specification as a translation pass within the CompCertSSA compiler, which is formally verified in Coq.