Feb 23, 2012, 7:07:13 PM (9 years ago)

More on front-end.

1 edited


  • Deliverables/D1.2/CompilerProofOutline/outline.tex

    r1731 r1732  
    126126\subsection{Clight to Cminor translation}
     128This translation is the first to introduce some invariants, with the
     129proofs closely tied to the implementation by dependent typing.  These
     130are largely complete and show that the generated code enjoys:
     132\item some minimal type safety shown by explicit checks on the
     133  Cminor types during the transformation (a little more work remains
     134  to be done here, but follows the same form);
     135\item that variables named in the parameter and local variable
     136  environments are distinct from one another, again by an explicit
     137  check;
     138\item that variables used in the generated code are present in the
     139  resulting environment (either by checking their presence in the
     140  source environment, or from a list of freshly temporary variables);
     141  and
     142\item that all \lstinline[language=C]'goto' labels are present (by
     143  checking them against a list of source labels and proving that all
     144  source labels are preserved).
     147The simulation will be similar to the relevant stages of CompCert
     148(Clight to Csharpminor and Csharpminor to Cminor --- in the event that
     149the direct proof is unwieldy we could introduce a corresponding
     150intermediate language).  During early experimentation with porting
     151CompCert definitions to the Matita proof assistant we found little
     152difficulty reproving the results for the memory model, so we plan to
     153port the memory injection properties and use them to relate Clight
     154in-memory variables with either a local variable valuation or a stack
     155slot, depending on how it was classified.
     157This should be sufficient to show the equivalence of (big-step)
     158expression evaluation.  The simulation can then be shown by relating
     159corresponding blocks of statement and continuations with their Cminor
     160counterparts and proving that a few steps reaches the next matching
     163The syntactic properties required for cost labels remain similar and a
     164structural induction on the function bodies should be sufficient to
     165show that they are preserved.
    128167\subsection{Cminor global initialisation code}
     169This short phase replaces the global variable initialisation data with
     170code that executes when the program starts.  Each piece of
     171initialisation data in the source is matched by a new statement
     172storing that data.  As each global variable is allocated a distinct
     173memory block, the program state after the initialisation statements
     174will be the same as the original program's state at the start of
     175execution, and will proceed in the same manner afterwards.
     177% Actually, the above is wrong...
     178% ... this ought to be in a fresh main function with a fresh cost label
    130180\subsection{Cminor to RTLabs translation}
Note: See TracChangeset for help on using the changeset viewer.