Changeset 1780 for Deliverables/D1.2/CompilerProofOutline

Timestamp:

Feb 27, 2012, 5:45:00 PM (9 years ago)

Author:

mulligan

Message:

finished rtl to ertl

File:

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

Deliverables/D1.2/CompilerProofOutline/outline.tex

@@ -745 +745 @@
 \end{displaymath}
 
+\subsection{The RTL to ERTL translation}
+\label{subsect.rtl.ertl.translation}
+
+We map RTL statuses to ERTL statuses as follows:
 \begin{align*}
-\mathrm{RTL\ status} & \ \ \mathrm{ERTL\ status} \\
-\mathtt{sp} & = \mathtt{spl} / \mathtt{sph} \\
+\mathtt{sp} & = \mathtt{RegisterSPH} / \mathtt{RegisterSPL} \\
 \mathtt{graph} &  \mathtt{graph} + \mathtt{prologue}(s) + \mathtt{epilogue}(s) \\
 & \mathrm{where}\ s = \mathrm{callee\ saved} + \nu \mathrm{RA} \\
 \end{align*}
-
-\begin{displaymath}
-\begin{diagram}
-\mathtt{CALL} & \rTo^1 & \mathtt{inside\ function} \\
-\dTo & & \dTo \\
-\underbrace{\ldots}_{\llbracket \mathtt{CALL} \rrbracket} & \rTo &
-\underbrace{\ldots}_{\mathtt{prologue}} \\
-\end{diagram}
-\end{displaymath}
-
-\begin{displaymath}
-\begin{diagram}
-\mathtt{RETURN} & \rTo^1 & \mathtt{.} \\
-\dTo & & \dTo \\
-\underbrace{\ldots}_{\mathtt{epilogue}} & \rTo &
-\underbrace{\ldots} \\
-\end{diagram}
-\end{displaymath}
-
+The 16-bit RTL stack pointer \texttt{SP} is mapped to a pair of 8-bit hardware registers \texttt{RegisterSPH} and \texttt{RegisterSPL}.
+The internal function graphs of RTL are augmented with an epilogue and a prologue, indexed by a set of registers, consisting of a fresh pair of registers \texttt{RA} and the set of registers that must be saved by the callee of a function.
+
+The prologue and epilogue that are added to the function graph do the following:
 \begin{align*}
 \mathtt{prologue}(s) = & \mathtt{create\_new\_frame}; \\
@@ -778 +766 @@
                                                                                          & \ \ \mathtt{stack\_params}: \mathtt{push}/\mathtt{pop}/\mathtt{move} \\
 \end{align*}
-
+That is, the prologue first creates a new stack frame, pops the return address from the stack, saves all the callee saved registers (i.e. the set \texttt{s}), fetches the parameters that are passed via registers and the stack and moves them into the correct registers.
+In other words, the prologue of a function correctly sets up the calling convention used in the compiler when calling a function.
+On the other hand, the epilogue undoes the action of the prologue:
 \begin{align*}
 \mathtt{epilogue}(s) = & \mathtt{save\ return\ to\ tmp\ real\ regs}; \\
@@ -786 +776 @@
                        & \mathtt{save return} \\
 \end{align*}
-
+That is, the epilogue first saves the return value to a temporary register, restores all the registers, pushes the return address on to the stack, deletes the stack frame that the prologue created, and saves the return value.
+
+The \texttt{CALL} instruction is translated as follows:
 \begin{displaymath}
 \mathtt{CALL}\ id \mapsto \mathtt{set\_params};\ \mathtt{CALL}\ id;\ \mathtt{fetch\_result}
+\end{displaymath}
+Here, \texttt{set\_params} and \texttt{fetch\_result} are functions that implement what the caller of the function needs to do when calling a function, as opposed to the epilogue and prologue which implement what the callee must do.
+
+The translation from RTL to ERTL and execution functions must satisfy the following properties for \texttt{CALL} and \texttt{RETURN} instructions appropriately:
+\begin{displaymath}
+\begin{diagram}
+\mathtt{CALL} & \rTo^1 & \mathtt{inside\ function} \\
+\dTo & & \dTo \\
+\underbrace{\ldots}_{\llbracket \mathtt{CALL} \rrbracket} & \rTo &
+\underbrace{\ldots}_{\mathtt{prologue}} \\
+\end{diagram}
+\end{displaymath}
+That is, if we start in a RTL \texttt{CALL} instruction, and translate this to an ERTL \texttt{CALL} instruction, then executing the RTL \texttt{CALL} instruction for one step and translating should land us in the prologue of the translated function.
+A similar property for \texttt{RETURN} should also hold, substituting the prologue for the epilogue of the function being translated:
+\begin{displaymath}
+\begin{diagram}
+\mathtt{RETURN} & \rTo^1 & \mathtt{.} \\
+\dTo & & \dTo \\
+\underbrace{\ldots}_{\mathtt{epilogue}} & \rTo &
+\underbrace{\ldots} \\
+\end{diagram}
 \end{displaymath}