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.