An ASM Semantics for SSA Intermediate Representations

Abstract. Static single assignment (SSA) form is the intermediate representation of choice in modern optimizing compilers for which no formal semantics has been stated yet. To prove such compilers correct, a formal semantics of SSA representations is necessary. In this paper, we show tract state machines (ASMs) are able to capture the imperative as well as the data flow-driven and therefore non-deterministic aspects of SSA representations in a simple and elegant way. Furthermore, we demonstrate that correctness of code generation can be verified based on this ASM semantics by proving the correctness of a simple code generation algorithm. on, to appear in the Proceedings of the International Workshop on Abstract State Machines ASM 2004, to be published by Springer, LNCS, 2004.

• Type: Conference
• Year: 2004
• Where: ASM
• Authors: Sabine Glesner
• Keywords: ASM 2004, Formal Semantics, Microbiology, Modern Optimizing Compilers, SSA Representations