Ignore:
Timestamp:
Oct 10, 2011, 6:18:10 PM (8 years ago)
Author:
campbell
Message:

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/Report/report.tex

    r1317 r1346  
    6868\bf
    6969Report n. D3.3\\
    70 Executable Formal Semantics of front end intermediate languages\\
     70Executable Formal Semantics of front-end intermediate languages\\
    7171\end{LARGE}
    7272\end{center}
     
    9999\vspace*{7cm}
    100100\paragraph{Abstract}
    101 We report on the formalization of the front end intermediate languages for the
     101We report on the formalization of the front-end intermediate languages for the
    102102\cerco{} project's compiler using executable semantics in the \matita{} proof
    103103assistant.  This includes common definitions for fresh identifier handling,
    104 $n$-bit arithmetic and operations and testing of the smeantics.  We also
     104$n$-bit arithmetic and operations and testing of the semantics.  We also
    105105consider embedding invariants into the semantics for showing correctness
    106106properties.
    107107
     108This work was Task~3.3 of the \cerco{} project and the languages that were
     109formalized were first described in Deliverable~2.1~\cite{d2.1}.  They are used
     110by the formalized front-end in Task~3.2 to provide the syntax for the
     111transformations, and to test them by animating programs in the executable
     112semantics.  It will also be a crucial part of the specifications for the
     113correctness results in Task~3.4.
     114
    108115\newpage
    109116
    110117\tableofcontents
    111118
    112 % TODO: clear up any -ize vs -ise
    113 % TODO: clear up any "front end" vs "front-end"
    114 % TODO: clear up any mentions of languages that aren't textsf'd.
    115 % TODO: fix unicode in listings
     119% CHECK: clear up any -ize vs -ise
     120% CHECK: clear up any "front end" vs "front-end"
     121% CHECK: clear up any mentions of languages that aren't textsf'd.
     122% CHECK: fix unicode in listings
    116123
    117124\section{Introduction}
    118125
    119 This work formalizes the front end intermediate languages from the \cerco{}
     126This work formalizes the front-end intermediate languages from the \cerco{}
    120127prototype compiler, described in previous deliverables~\cite{d2.1,d2.2}.  The
    121 front end of the compiler is summarized in Figure~\ref{fig:summary} including
     128front-end of the compiler is summarized in Figure~\ref{fig:summary} including
    122129the intermediate languages and the compiler passes described in the
    123 accompanying deliverable 3.2.  We have also refined parts of the formal
     130accompanying Deliverable 3.2.  We have also refined parts of the formal
    124131development that are used for several of the languages in the compiler.
    125132
    126 The input language to the formalized front end is the \textsf{Clight}
     133The input language to the formalized front-end is the \textsf{Clight}
    127134language.  The executable semantics for this language were presented in a
    128135previous deliverable~\cite{d3.1}.  Here we will report on some
     
    134141done in the Calculus of Inductive Constructions (CIC), as implemented in the
    135142\matita{} proof assistant.  These definitions will be essential for the
    136 correctness proofs of the compiler in task 3.4.
     143correctness proofs of the compiler in Task 3.4.
    137144
    138145Finally, we will report on work to add several invariants to the
    139 languages.  This activity overlaps with task 3.4 on the correctness of the
    140 compiler front end.  However, the use of dependent types mean that this work
     146languages.  This activity overlaps with Task 3.4 on the correctness of the
     147compiler front-end.  However, the use of dependent types mean that this work
    141148is tied closely to the definition of the languages and the transformations of
    142 the front end in task 3.2.  By considering it now we can experiment with and
     149the front-end in Task 3.2.  By considering it now we can experiment with and
    143150judge its impact on the formal semantics, and how feasible retrofitting such
    144151invariants is.
     
    158165 simplification\\
    159166\textsf{Cminor}\\
    160 \> $\downarrow$ \> generate global variable initialisation code\\
     167\> $\downarrow$ \> generate global variable initialization code\\
    161168\> $\downarrow$ \> transform to RTL graph\\
    162169\textsf{RTLabs}\\
    163 \> $\downarrow$ \> start of target specific backend\\
     170\> $\downarrow$ \> start of target specific back-end\\
    164171\>\quad \vdots
    165172\end{tabbing}
    166173\end{minipage}
    167174\end{center}
    168 \caption{Front end languages and transformations}
     175\caption{Front-end languages and transformations}
    169176\label{fig:summary}
    170177\end{figure}
     
    189196a monad for encapsulating failure and I/O (using resumptions).  The executable
    190197memory model was ported from CompCert as part of the work on \textsf{Clight}
    191 and was reused for the front end languages\footnote{However, it is likely that
     198and was reused for the front-end languages\footnote{However, it is likely that
    192199we will revise the memory model to make it better suited for describing the
    193200back-end of our compiler.}.  The failure and I/O monad was introduced in the
     
    234241
    235242The bit vectors in~\cite{d4.1} also came equipped with some basic arithmetic
    236 for the target semantics.  The front end required these operations to be
     243for the target semantics.  The front-end required these operations to be
    237244generalized and extended.  In particular, we required operations such as zero
    238245and sign extension and translation between bit vectors and full integers.  It
     
    242249front-end semantics.
    243250
    244 \subsection{Front end operations}
    245 
    246 The two front end intermediate languages, \textsf{Cminor} and \textsf{RTLabs},
     251\subsection{Front-end operations}
     252
     253The two front-end intermediate languages, \textsf{Cminor} and \textsf{RTLabs},
    247254share the same set of operations on values.  They differ from
    248255\textsf{Clight}'s operations by incorporating casts and by having a separate
     
    274281is similar to the prototype, except that the types attached to expressions are
    275282restricted so that some corner cases are ruled out in the \textsf{Cminor} to
    276 \textsf{RTLabs} stage (see the accompanying deliverable 3.2 for details):
     283\textsf{RTLabs} stage (see the accompanying Deliverable 3.2 for details):
    277284\begin{lstlisting}
    278285    inductive expr : typ $\rightarrow$ Type[0] ≝
     
    289296In principle we could extend this to statically ensure that only well-typed
    290297\textsf{Cminor} expressions are considered, and we will consider this as part
    291 of the work on correctness in task 3.4.
     298of the work on correctness in Task 3.4.
    292299
    293300We also provide a variant of the syntax where the only initialization data is
     
    311318prototype compiler.  Some of the syntax is shown below, including the type of
    312319the control flow graphs.  The same common elements are used as for \textsf{Cminor},
    313 including the front end operations mentioned above.
     320including the front-end operations mentioned above.
    314321
    315322\begin{lstlisting}[language=matita]
     
    339346
    340347To provide some assurance that the semantics were properly implemented, and to
    341 support the testing described in the accompanying deliverable 3.2, we have
     348support the testing described in the accompanying Deliverable 3.2, we have
    342349adapted the pretty printers in the prototype compiler to produce \matita{}
    343350terms for the syntax of each language described above.
    344351
    345352A few common definitions were added for animating the small step semantics
    346 definitions for any of the front end languages in \matita.  We then used a
     353definitions for any of the front-end languages in \matita.  We then used a
    347354small selection of test cases to ensure basic functionality.  However, this is
    348355still a time consuming process, so more testing will carried out once the
     
    362369involves manipulating the syntax and semantics of the intermediate languages
    363370(the present work), the encoding of the front-end compiler phases in \matita{}
    364 (task 3.2) and the correctness of the front-end (task 3.4).  Thus this work is
     371(Task 3.2) and the correctness of the front-end (Task 3.4).  Thus this work is
    365372rather experimental; it is being carried out on branches in our source code
    366 repository and the final form will be decided and merged in during task 3.4.
     373repository and the final form will be decided and merged in during Task 3.4.
    367374
    368375So far we have tried adding two forms of invariant --- one using dependent
     
    474481
    475482The \textsf{Clight} semantics can be amended to use these invariants, although
    476 the main benefit is for the compiler stages (see the accompanying deliverable
     483the main benefit is for the compiler stages (see the accompanying Deliverable
    4774843.2 for details).  The semantics require the invariants to be added to the
    478485state and continuations.  It was convenient to split the continuations between
     
    491498presence of proof terms and more dependent pattern matching in the semantics
    492499will have on the complexity of future correctness proofs.  We plan to examine
    493 this issue during task 3.4.
     500this issue during Task 3.4.
    494501
    495502We use a similar method to specify the invariant that the \textsf{RTLabs}
     
    503510We have developed executable semantics for each of the front-end languages of
    504511the \cerco{} compiler.  These will form the basis of the correctness
    505 statements for each stage of the compiler in task 3.4.  We have also shown
     512statements for each stage of the compiler in Task 3.4.  We have also shown
    506513that useful invariants can be added as dependent types, and intend to use
    507514these in subsequent work.
Note: See TracChangeset for help on using the changeset viewer.