# Changeset 3218

Ignore:
Timestamp:
Apr 30, 2013, 12:01:03 AM (5 years ago)
Message:

File:
1 edited

Unmodified
Removed
• ## Deliverables/D3.4/Report/report.tex

 r3216 \todo{Make this a particular case of the more general statement on baking more invariants in the Clight language} \subsection{Clight to Cminor} \subsubsection{Clight to Cminor} This pass is the last one operating on the \textsf{Clight} language. discuss our implementation of memory injections, and then the simulation proof. \subparagraph{Memory injections.} \paragraph{Memory injections.} Our memory injections are modelled after the work of Blazy \& Leroy. loads after writes were axiomatised, due to a lack of time. \subparagraph{Simulation proof.} \paragraph{Simulation proof.} The correctness proof for this transformation was not completed. We proved the \todo{list cases, explain while loop, explain labeling problem} \subsubsection{Cminor to RTLabs} The translation from \textsf{Cminor} to \textsf{RTLabs} is a fairly routine control flow graph (CFG) construction.  As such, we chose to axiomatise its simulation results.  However, we did prove several properties of the generated programs: \begin{itemize} \item All statements are type correct with respect to the declared pseudo-register type environment. \item The CFG is closed, and has a distinguished entry node and a unique exit node. \end{itemize} These properties rely on similar properties about type safety and the presence of \lstinline[language=C]'goto'-labels for Cminor programs which are checked at the preceding stage.  As a result, this transformation is total and any compilation failures must occur when the corresponding \textsf{Clight} source is available and a better error message can be generated. The proof obligations for these properties include many instances of graph inclusion.  We automated these proofs using a small amount of reflection, making the obligations much easier to handle.  One drawback to enforcing invariants thoroughly is that temporarily breaking them can be awkward.  For example, \lstinline'return' statements were originally used as placeholders for \lstinline[language=C]'goto' destinations that had not yet been translated.  However, this made establishing the single exit node property rather difficult, and a different placeholder was chosen instead.  In other circumstances it is possible to prove a more complex invariant then simplify it at the end of the transformation. \section{Checking cost labelling properties}
Note: See TracChangeset for help on using the changeset viewer.