Correct translation of imperative programs to single assignment form

Abstract

A common practice in compiler design is to have an intermediate representation of the source code in Static Single-Assignment (SSA) form in order to simplify the code optimization process and make it more efficient. Generally, one says that an imperative program is in SSA form if each variable is assigned exactly once. In this thesis we study the central ideas of SSA-programs in the context of a simple imperative language including jump instructions. The focus of this work is the proof of correctness of a translation from programs of the source imperative language into the SSA format. In particular, we formally introduce the syntax and the semantics of the source imperative language (GL) and the SSA language; we define and implement a function that translates from source imperative programs into SSA-programs; we develop an alternative operational semantics, in order to be able to relate the execution of a source program and of its SSA translation; we prove soundness and completeness results for the translation, relatively to the alternative operational semantics, and from these results we prove correctness of the translation relatively to the initial small-step semantics.

Uma prática comum no design de compiladores é ter uma representação intermédia do código fonte em formato Static Single Assigment (SSA), de modo a facilitar o processo subsequente de análise e optimização de código. Em termos gerais, diz-se que um programa imperativo está no formato SSA se cada variável do programa é atribuída exatamente uma vez. Nesta tese estudamos as ideias principais do SSA no contexto de uma linguagem imperativa simples com instruções de salto. O foco deste trabalho é a prova de correcção de uma tradução dos programas fonte para formato SSA. Concretamente, definimos formalmente a sintaxe e a semântica da linguagem fonte (GL) e da linguagem em formato SSA; definimos e implementamos a função de tradução; desenvolvemos semânticas operacionais alternativas de modo a permitir relacionar a execução do programa fonte com a sua tradução SSA; provamos a idoneidade e a completude do processo de tradução relativamente às semânticas alternativas definidas; e a partir destes resultados demonstramos a correção da tradução em ordem às semânticas operacionais estruturais definidas inicialmente.