Changeset 1267


Ignore:
Timestamp:
Sep 26, 2011, 12:41:45 PM (8 years ago)
Author:
campbell
Message:

Other bits and pieces for D3.3.

File:
1 edited

Legend:

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

    r1265 r1267  
    113113% TODO: clear up any "front end" vs "front-end"
    114114% TODO: clear up any mentions of languages that aren't textsf'd.
    115 % TODO: mention the restricted form of types after Clight
    116115% TODO: fix unicode in listings
    117 % TODO: say something about what CIC is, and why we're doing this.
    118116
    119117\section{Introduction}
     
    131129minor changes to its semantics made to better align it with the whole
    132130development.
     131
     132The formalization of each language takes the form of definitions for abstract
     133syntax and functions providing a small-step executable semantics.  This is
     134done in the Calculus of Inductive Constructions (CIC), as implemented in the
     135\matita{} proof assistant.  These definitions will be essential for the
     136correctness proofs of the compiler in task 3.4.
    133137
    134138Finally, we will report on work to add several invariants to the
     
    231235The bit vectors in~\cite{d4.1} also came equipped with some basic arithmetic
    232236for the target semantics.  The front end required these operations to be
    233 generalized and extended.
    234 
    235 % TODO: expand, note need to sufficiently good performance for testing
     237generalized and extended.  In particular, we required operations such as zero
     238and sign extension and translation between bit vectors and full integers.  It
     239also became apparent that while the original definitions worked reasonably on
     2408-bit vectors, they did not scale up to 32-bit integers.  The definitions were
     241then reworked to make them efficient enough to animate programs in the
     242front-end semantics.
    236243
    237244\subsection{Front end operations}
     
    302309
    303310Otherwise, the syntax and semantics of \textsf{RTLabs} mirrors that of the
    304 prototype compiler.  The same common elements are used as for \textsf{Cminor},
     311prototype compiler.  Some of the syntax is shown below, including the type of
     312the control flow graphs.  The same common elements are used as for \textsf{Cminor},
    305313including the front end operations mentioned above.
    306314
    307 % TODO: give fragment of syntax, in particular the type of the graph
     315\begin{lstlisting}[language=matita]
     316inductive statement : Type[0] ≝
     317| St_skip : label → statement
     318| St_cost : costlabel → label → statement
     319| St_const : register → constant → label → statement
     320| St_op1 : unary_operation → register → register → label → statement
     321...
     322| St_return : statement
     323.
     324
     325definition graph : Type[0] → Type[0] ≝ identifier_map LabelTag.
     326
     327record internal_function : Type[0] ≝
     328{ f_labgen    : universe LabelTag
     329; f_reggen    : universe RegisterTag
     330; f_result    : option (register × typ)
     331; f_params    : list (register × typ)
     332; f_locals    : list (register × typ)
     333; f_stacksize : nat
     334; f_graph     : graph statement
     335}.
     336\end{lstlisting}
    308337
    309338\section{Testing}
     
    449478state and continuations.  It was convenient to split the continuations between
    450479the local continuation representing the rest of the code to be executed within
    451 the function, and the stack of function calls.
    452 % TODO: because???
     480the function, and the stack of function calls because it becomes easier to
     481state the property on the local continuation alone.
    453482  The invariant for variables is
    454483slightly different --- we require that every variable appear in the local
     
    472501\section{Conclusion}
    473502
     503We have developed executable semantics for each of the front-end languages of
     504the \cerco{} compiler.  These will form the basis of the correctness
     505statements for each stage of the compiler in task 3.4.  We have also shown
     506that useful invariants can be added as dependent types, and intend to use
     507these in subsequent work.
     508
    474509\bibliographystyle{plain}
    475510\bibliography{report}
Note: See TracChangeset for help on using the changeset viewer.