Changeset 1267

Sep 26, 2011, 12:41:45 PM (8 years ago)

Other bits and pieces for D3.3.

1 edited


  • 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.
    131129minor changes to its semantics made to better align it with the whole
     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.
    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.
    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.
    237244\subsection{Front end operations}
    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.
    307 % TODO: give fragment of syntax, in particular the type of the graph
     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
     322| St_return : statement
     325definition graph : Type[0] → Type[0] ≝ identifier_map LabelTag.
     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
    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
     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.
Note: See TracChangeset for help on using the changeset viewer.