# Changeset 1731 for Deliverables

Ignore:
Timestamp:
Feb 23, 2012, 5:25:43 PM (9 years ago)
Message:

A bit of front-end proof outline.

File:
1 edited

### Legend:

Unmodified
 r1728 This document provides a very high-level, pen-and-paper sketch of what we view as the best path to completing the correctness proof for the compiler. In particular, for every translation between two intermediate languages, in both the front- and back-ends, we identify the key translation steps, and identify some invariants that we view as being important for the correctness proof. \section{Front-end: Clight to RTLabs} The front-end of the CerCo compiler consists of several stages: \begin{center} \begin{minipage}{.8\linewidth} \begin{tabbing} \quad \= $\downarrow$ \quad \= \kill \textsf{Clight}\\ \> $\downarrow$ \> cast removal\\ \> $\downarrow$ \> add runtime functions\footnote{Following the last project meeting we intend to move this transformation to the back-end}\\ \> $\downarrow$ \> cost labelling\\ \> $\downarrow$ \> stack variable allocation and control structure simplification\\ \textsf{Cminor}\\ \> $\downarrow$ \> generate global variable initialisation code\\ \> $\downarrow$ \> transform to RTL graph\\ \textsf{RTLabs}\\ \> $\downarrow$ \> start of target specific back-end\\ \>\quad \vdots \end{tabbing} \end{minipage} \end{center} %Our overall statements of correctness with respect to costs will %require a correctly labelled program There are three layers in most of the proofs proposed: \begin{enumerate} \item invariants closely tied to the syntax and transformations using dependent types, \item a forward simulation proof, and \item syntactic proofs about the cost labelling. \end{enumerate} The first will support both function correctness and allow us to show the totality of some of the compiler stages (that is, these stages of the compiler cannot fail).  The second provides the main functional correctness result, and the last will be crucial for applying correctness results about the costings from the back-end. We will also prove that a suitably labelled RTLabs trace can be turned into a \emph{structured trace} which splits the execution trace into cost-label-to-cost-label chunks with nested function calls.  This structure was identified during work on the correctness of the back-end cost analysis as retaining important information about the structure of the execution that is difficult to reconstruct later in the compiler. \subsection{Clight Cast removal} This removes some casts inserted by the parser to make arithmetic promotion explicit when they are superfluous (such as \lstinline[language=C]'c = (short)((int)a + (int)b);'). The transformation only affects Clight expressions, recursively detecting casts that can be safely eliminated.  The semantics provides a big-step definition for expression, so we should be able to show a lock-step forward simulation using a lemma showing that cast elimination does not change the evaluation of expressions.  This lemma will follow from a structural induction on the source expression.  We have already proved a few of the underlying arithmetic results necessary to validate the approach. \subsection{Clight cost labelling} This adds cost labels before and after selected statements and expressions, and the execution traces ought to be equivalent modulo cost labels.  Hence it requires a simple forward simulation with a limited amount of stuttering whereever a new cost label is introduced. A bound can be given for the amount of stuttering allowed can be given based on the statement or continuation to be evaluated next. We also intend to show three syntactic properties about the cost labelling: \begin{itemize} \item every function starts with a cost label, \item every branching instruction is followed by a label (note that exiting a loop is treated as a branch), and \item the head of every loop (and any \lstinline'goto' destination) is a cost label. \end{itemize} These can be shown by structural induction on the source term. \subsection{Clight to Cminor translation} \subsection{Cminor global initialisation code} \subsection{Cminor to RTLabs translation} \subsection{RTLabs structured trace generation} \section{The RTLabs to RTL translation}