# Changeset 1346 for Deliverables/D3.2

Ignore:
Timestamp:
Oct 10, 2011, 6:18:10 PM (9 years ago)
Message:

Minor corrections and a paragraph of context in the abstract to deliverables 3.2 and 3.3.

File:
1 edited

Unmodified
Removed
• ## Deliverables/D3.2/Report/report.tex

 r1317 \vspace*{7cm} \paragraph{Abstract} We describe the translation of the front end of the \cerco{} compiler from the We describe the translation of the front-end of the \cerco{} compiler from the \ocaml{} prototype to the Calculus of Inductive Constructions (CIC) in the \matita{} proof assistant.  This transforms programs in the C-like will assist in future work proving correctness properties. This work was Task~3.2 of the \cerco{} project, translating the prototype described in Deliverable~2.2~\cite{d2.2} into CIC using the intermediate languages formalized in Deliverables~3.1~\cite{d3.1} and~3.3.  It will feed into the front-end correctness proofs in Task~3.4 and is a counterpart to the back-end formalization in Task~4.2. \newpage % TODO: clear up any -ize vs -ise % TODO: clear up any "front end" vs "front-end" % TODO: clear up any mentions of languages that aren't textsf'd. % TODO: fix unicode in listings % TODO: make it clear that our correctness is intended to go beyond compcert's % TODO: capitalise deliverable/task? % CHECK: clear up any "front end" vs "front-end" % CHECK: clear up any mentions of languages that aren't textsf'd. % CHECK: fix unicode in listings % CHEKC: capitalise deliverable/task when referring to a particular one \section{Introduction} \> $\downarrow$ \> transform to RTL graph\\ \textsf{RTLabs}\\ \> $\downarrow$ \> start of target specific backend\\ \> $\downarrow$ \> start of target specific back-end\\ \>\quad \vdots \end{tabbing} \item[\textsf{RTLabs}] --- a language in the form of a control flow graph which retains the values and front end operations from \textsf{Cminor} which retains the values and front-end operations from \textsf{Cminor} \end{description} More details on the formalisation of the syntax and semantics of these languages can be found in the accompanying deliverable 3.4. languages can be found in the accompanying Deliverable 3.4. Development of the formalized front-end was conducted in concert with the development of these intermediate languages to facilitate testing. \end{itemize} This document describes the formalized front end after these changes. This document describes the formalized front-end after these changes. \section{\textsf{Clight} phases} This has been implemented in \matita.  We have also performed a few proofs that the arithmetic behind these changes is correct to gain confidence in the technique.  During task 3.4 we will extend these proofs to cover more technique.  During Task 3.4 we will extend these proofs to cover more operations and show that the semantics of the expressions are equivalent, not just the underlying arithmetic. simple recursive definition, and was straightforward to port to \matita.  The generation of cost labels was handled by our generic identifiers code, described in the accompanying deliverable 3.3 on intermediate languages. described in the accompanying Deliverable 3.3 on intermediate languages. \subsection{Runtime functions} \textsf{Clight} abstract syntax trees directly. \subsection{Conversion to Cminor} \subsection{Conversion to \textsf{Cminor}} The conversion to \textsf{Cminor} performs two essential tasks.  First, it formed early in the compilation process. This work overlaps with deliverable 3.3 (where more details of the additions This work overlaps with Deliverable 3.3 (where more details of the additions to the syntax and semantics of the intermediate languages can be found) and task 3.4 on the correctness of the compiler.  Thus this work is experimental in nature, and will evolve during task 3.4. Task 3.4 on the correctness of the compiler.  Thus this work is experimental in nature, and will evolve during Task 3.4. The use of the invariants follows a common pattern.  Each language embeds To provide some early testing and bug fixing of this code we constructed it in concert with the executable semantics described in deliverable 3.3, and concert with the executable semantics described in Deliverable 3.3, and \matita{} term pretty printers in the prototype compiler.  Using these, we were able to test the phases individually and together by running programs proof assistant, and shown that invariants can be added to the intermediate languages to help show properties of it.  This work provides a solid basis for the compiler correctness proofs in task 3.4. the compiler correctness proofs in Task 3.4. \bibliographystyle{plain}
Note: See TracChangeset for help on using the changeset viewer.