Changeset 1734 for Deliverables/D1.2/CompilerProofOutline

Timestamp:

Feb 24, 2012, 11:44:01 AM (9 years ago)

Author:

mulligan

Message:

followed brian's lead in explaining the backend translation steps with a handy diagram, some more changes, commit to avoid conflicts also

File:

• Deliverables/D1.2/CompilerProofOutline/outline.tex (modified) (4 diffs)

Deliverables/D1.2/CompilerProofOutline/outline.tex

@@ -243 +243 @@
 flattening result to show that it is correct.
 
-\section{The RTLabs to RTL translation}
-\label{sect.rtlabs.rtl.translation}
+\section{Backend: RTLabs to machine code}
+\label{sect.backend.rtlabs.machine.code}
+
+The compiler backend consists of the following intermediate languages, and stages of translation:
+
+\begin{center}
+\begin{minipage}{.8\linewidth}
+\begin{tabbing}
+\quad \= $\downarrow$ \quad \= \kill
+\textsf{RTLabs}\\
+\> $\downarrow$ \> instruction selection\\
+\textsf{RTL}\\
+\> $\downarrow$ \> constant propagation (an endo-transformation) \\
+\> $\downarrow$ \> copy propagation (an endo-transformation) \\
+\> $\downarrow$ \> calling convention made explicit \\
+\> $\downarrow$ \> stack frame generation \\
+\textsf{ERTL}\\
+\> $\downarrow$ \> register allocation and spilling\\
+\> $\downarrow$ \> dead code elimination\\
+\textsf{LTL}\\
+\> $\downarrow$ \> function linearisation\\
+\> $\downarrow$ \> branch compression (an endo-transformation) \\
+\textsf{LIN}\\
+\> $\downarrow$ \> relabeling\\
+\textsf{ASM}\\
+\> $\downarrow$ \> pseudoinstruction expansion\\
+\textsf{Machine code}\\
+\end{tabbing}
+\end{minipage}
+\end{center}
+
+Here, by `endo-transformation', we mean a mapping from language back to itself.
+For example, the constant propagation step maps the RTL language to the RTL language.
+
+\subsection{The RTLabs to RTL translation}
+\label{subsect.rtlabs.rtl.translation}
 
 % dpm: type system and casting load (???)
@@ -360 +394 @@
 \end{displaymath}
 
-\section{The RTL to ERTL translation}
-\label{sect.rtl.ertl.translation}
+\subsection{The RTL to ERTL translation}
+\label{subsect.rtl.ertl.translation}
 
 \begin{displaymath}
@@ -463 +497 @@
 \end{displaymath}
 
-\section{The ERTL to LTL translation}
-\label{sect.ertl.ltl.translation}
-
-\section{The LTL to LIN translation}
-\label{sect.ltl.lin.translation}
+\subsection{The ERTL to LTL translation}
+\label{subsect.ertl.ltl.translation}
+
+\subsection{The LTL to LIN translation}
+\label{subsect.ltl.lin.translation}
 
 We require a map, $\sigma$, from LTL statuses, where program counters are represented as labels in a graph data structure, to LIN statuses, where program counters are natural numbers:
@@ -543 +577 @@
 Each well-formed function must end with a call to \texttt{RET}, and therefore the only correct instruction that can terminate a LIN program is a \texttt{RET} instruction.
 
-\section{The LIN to ASM and ASM to MCS-51 machine code translations}
-\label{sect.lin.asm.translation}
+\subsection{The LIN to ASM and ASM to MCS-51 machine code translations}
+\label{subsect.lin.asm.translation}
 
 The LIN to ASM translation step is trivial, being almost the identity function.