Please use this identifier to cite or link to this item: http://hdl.handle.net/1822/47725

TitleCorrect translation of imperative programs to single assignment form
Other titlesTradução correta de programas imperativos para a forma single assignment
Author(s)Azevedo, Marta Vasconcelos Castro
Advisor(s)Frade, M. J.
Pinto, Luís F.
Issue date2017
Abstract(s)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.
TypeMaster thesis
DescriptionDissertação de mestrado em Computer Science
URIhttp://hdl.handle.net/1822/47725
AccessOpen access
Appears in Collections:BUM - Dissertações de Mestrado
DI - Dissertações de Mestrado

Files in This Item:
File Description SizeFormat 
Marta Vasconcelos Castro Azevedo.pdf533,44 kBAdobe PDFView/Open

Partilhe no FacebookPartilhe no TwitterPartilhe no DeliciousPartilhe no LinkedInPartilhe no DiggAdicionar ao Google BookmarksPartilhe no MySpacePartilhe no Orkut
Exporte no formato BibTex mendeley Exporte no formato Endnote Adicione ao seu ORCID