# Changeset 1780 for Deliverables

Ignore:
Timestamp:
Feb 27, 2012, 5:45:00 PM (8 years ago)
Message:

finished rtl to ertl

File:
1 edited

Unmodified
Added
Removed
• ## Deliverables/D1.2/CompilerProofOutline/outline.tex

 r1779 \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}; \\ & \ \ \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}; \\ & \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}
Note: See TracChangeset for help on using the changeset viewer.