# Changeset 1346 for Deliverables/D3.3

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.3/Report/report.tex

 r1317 \bf Report n. D3.3\\ Executable Formal Semantics of front end intermediate languages\\ Executable Formal Semantics of front-end intermediate languages\\ \end{LARGE} \end{center} \vspace*{7cm} \paragraph{Abstract} We report on the formalization of the front end intermediate languages for the We report on the formalization of the front-end intermediate languages for the \cerco{} project's compiler using executable semantics in the \matita{} proof assistant.  This includes common definitions for fresh identifier handling, $n$-bit arithmetic and operations and testing of the smeantics.  We also $n$-bit arithmetic and operations and testing of the semantics.  We also consider embedding invariants into the semantics for showing correctness properties. This work was Task~3.3 of the \cerco{} project and the languages that were formalized were first described in Deliverable~2.1~\cite{d2.1}.  They are used by the formalized front-end in Task~3.2 to provide the syntax for the transformations, and to test them by animating programs in the executable semantics.  It will also be a crucial part of the specifications for the correctness results in Task~3.4. \newpage \tableofcontents % 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 % CHECK: clear up any -ize vs -ise % 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 \section{Introduction} This work formalizes the front end intermediate languages from the \cerco{} This work formalizes the front-end intermediate languages from the \cerco{} prototype compiler, described in previous deliverables~\cite{d2.1,d2.2}.  The front end of the compiler is summarized in Figure~\ref{fig:summary} including front-end of the compiler is summarized in Figure~\ref{fig:summary} including the intermediate languages and the compiler passes described in the accompanying deliverable 3.2.  We have also refined parts of the formal accompanying Deliverable 3.2.  We have also refined parts of the formal development that are used for several of the languages in the compiler. The input language to the formalized front end is the \textsf{Clight} The input language to the formalized front-end is the \textsf{Clight} language.  The executable semantics for this language were presented in a previous deliverable~\cite{d3.1}.  Here we will report on some done in the Calculus of Inductive Constructions (CIC), as implemented in the \matita{} proof assistant.  These definitions will be essential for the correctness proofs of the compiler in task 3.4. correctness proofs of the compiler in Task 3.4. Finally, we will report on work to add several invariants to the languages.  This activity overlaps with task 3.4 on the correctness of the compiler front end.  However, the use of dependent types mean that this work languages.  This activity overlaps with Task 3.4 on the correctness of the compiler front-end.  However, the use of dependent types mean that this work is tied closely to the definition of the languages and the transformations of the front end in task 3.2.  By considering it now we can experiment with and the front-end in Task 3.2.  By considering it now we can experiment with and judge its impact on the formal semantics, and how feasible retrofitting such invariants is. simplification\\ \textsf{Cminor}\\ \> $\downarrow$ \> generate global variable initialisation code\\ \> $\downarrow$ \> generate global variable initialization code\\ \> $\downarrow$ \> transform to RTL graph\\ \textsf{RTLabs}\\ \> $\downarrow$ \> start of target specific backend\\ \> $\downarrow$ \> start of target specific back-end\\ \>\quad \vdots \end{tabbing} \end{minipage} \end{center} \caption{Front end languages and transformations} \caption{Front-end languages and transformations} \label{fig:summary} \end{figure} a monad for encapsulating failure and I/O (using resumptions).  The executable memory model was ported from CompCert as part of the work on \textsf{Clight} and was reused for the front end languages\footnote{However, it is likely that and was reused for the front-end languages\footnote{However, it is likely that we will revise the memory model to make it better suited for describing the back-end of our compiler.}.  The failure and I/O monad was introduced in the The bit vectors in~\cite{d4.1} also came equipped with some basic arithmetic for the target semantics.  The front end required these operations to be for the target semantics.  The front-end required these operations to be generalized and extended.  In particular, we required operations such as zero and sign extension and translation between bit vectors and full integers.  It front-end semantics. \subsection{Front end operations} The two front end intermediate languages, \textsf{Cminor} and \textsf{RTLabs}, \subsection{Front-end operations} The two front-end intermediate languages, \textsf{Cminor} and \textsf{RTLabs}, share the same set of operations on values.  They differ from \textsf{Clight}'s operations by incorporating casts and by having a separate is similar to the prototype, except that the types attached to expressions are restricted so that some corner cases are ruled out in the \textsf{Cminor} to \textsf{RTLabs} stage (see the accompanying deliverable 3.2 for details): \textsf{RTLabs} stage (see the accompanying Deliverable 3.2 for details): \begin{lstlisting} inductive expr : typ $\rightarrow$ Type[0] ≝ In principle we could extend this to statically ensure that only well-typed \textsf{Cminor} expressions are considered, and we will consider this as part of the work on correctness in task 3.4. of the work on correctness in Task 3.4. We also provide a variant of the syntax where the only initialization data is prototype compiler.  Some of the syntax is shown below, including the type of the control flow graphs.  The same common elements are used as for \textsf{Cminor}, including the front end operations mentioned above. including the front-end operations mentioned above. \begin{lstlisting}[language=matita] To provide some assurance that the semantics were properly implemented, and to support the testing described in the accompanying deliverable 3.2, we have support the testing described in the accompanying Deliverable 3.2, we have adapted the pretty printers in the prototype compiler to produce \matita{} terms for the syntax of each language described above. A few common definitions were added for animating the small step semantics definitions for any of the front end languages in \matita.  We then used a definitions for any of the front-end languages in \matita.  We then used a small selection of test cases to ensure basic functionality.  However, this is still a time consuming process, so more testing will carried out once the involves manipulating the syntax and semantics of the intermediate languages (the present work), the encoding of the front-end compiler phases in \matita{} (task 3.2) and the correctness of the front-end (task 3.4).  Thus this work is (Task 3.2) and the correctness of the front-end (Task 3.4).  Thus this work is rather experimental; it is being carried out on branches in our source code repository and the final form will be decided and merged in during task 3.4. repository and the final form will be decided and merged in during Task 3.4. So far we have tried adding two forms of invariant --- one using dependent The \textsf{Clight} semantics can be amended to use these invariants, although the main benefit is for the compiler stages (see the accompanying deliverable the main benefit is for the compiler stages (see the accompanying Deliverable 3.2 for details).  The semantics require the invariants to be added to the state and continuations.  It was convenient to split the continuations between presence of proof terms and more dependent pattern matching in the semantics will have on the complexity of future correctness proofs.  We plan to examine this issue during task 3.4. this issue during Task 3.4. We use a similar method to specify the invariant that the \textsf{RTLabs} We have developed executable semantics for each of the front-end languages of the \cerco{} compiler.  These will form the basis of the correctness statements for each stage of the compiler in task 3.4.  We have also shown statements for each stage of the compiler in Task 3.4.  We have also shown that useful invariants can be added as dependent types, and intend to use these in subsequent work.
Note: See TracChangeset for help on using the changeset viewer.