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

finished rtl to ertl

File:
1 edited

Legend:

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

    r1779 r1780  
    745745\end{displaymath}
    746746
     747\subsection{The RTL to ERTL translation}
     748\label{subsect.rtl.ertl.translation}
     749
     750We map RTL statuses to ERTL statuses as follows:
    747751\begin{align*}
    748 \mathrm{RTL\ status} & \ \ \mathrm{ERTL\ status} \\
    749 \mathtt{sp} & = \mathtt{spl} / \mathtt{sph} \\
     752\mathtt{sp} & = \mathtt{RegisterSPH} / \mathtt{RegisterSPL} \\
    750753\mathtt{graph} &  \mathtt{graph} + \mathtt{prologue}(s) + \mathtt{epilogue}(s) \\
    751754& \mathrm{where}\ s = \mathrm{callee\ saved} + \nu \mathrm{RA} \\
    752755\end{align*}
    753 
    754 \begin{displaymath}
    755 \begin{diagram}
    756 \mathtt{CALL} & \rTo^1 & \mathtt{inside\ function} \\
    757 \dTo & & \dTo \\
    758 \underbrace{\ldots}_{\llbracket \mathtt{CALL} \rrbracket} & \rTo &
    759 \underbrace{\ldots}_{\mathtt{prologue}} \\
    760 \end{diagram}
    761 \end{displaymath}
    762 
    763 \begin{displaymath}
    764 \begin{diagram}
    765 \mathtt{RETURN} & \rTo^1 & \mathtt{.} \\
    766 \dTo & & \dTo \\
    767 \underbrace{\ldots}_{\mathtt{epilogue}} & \rTo &
    768 \underbrace{\ldots} \\
    769 \end{diagram}
    770 \end{displaymath}
    771 
     756The 16-bit RTL stack pointer \texttt{SP} is mapped to a pair of 8-bit hardware registers \texttt{RegisterSPH} and \texttt{RegisterSPL}.
     757The 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.
     758
     759The prologue and epilogue that are added to the function graph do the following:
    772760\begin{align*}
    773761\mathtt{prologue}(s) = & \mathtt{create\_new\_frame}; \\
     
    778766                                                                                         & \ \ \mathtt{stack\_params}: \mathtt{push}/\mathtt{pop}/\mathtt{move} \\
    779767\end{align*}
    780 
     768That 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.
     769In other words, the prologue of a function correctly sets up the calling convention used in the compiler when calling a function.
     770On the other hand, the epilogue undoes the action of the prologue:
    781771\begin{align*}
    782772\mathtt{epilogue}(s) = & \mathtt{save\ return\ to\ tmp\ real\ regs}; \\
     
    786776                       & \mathtt{save return} \\
    787777\end{align*}
    788 
     778That 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.
     779
     780The \texttt{CALL} instruction is translated as follows:
    789781\begin{displaymath}
    790782\mathtt{CALL}\ id \mapsto \mathtt{set\_params};\ \mathtt{CALL}\ id;\ \mathtt{fetch\_result}
     783\end{displaymath}
     784Here, \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.
     785
     786The translation from RTL to ERTL and execution functions must satisfy the following properties for \texttt{CALL} and \texttt{RETURN} instructions appropriately:
     787\begin{displaymath}
     788\begin{diagram}
     789\mathtt{CALL} & \rTo^1 & \mathtt{inside\ function} \\
     790\dTo & & \dTo \\
     791\underbrace{\ldots}_{\llbracket \mathtt{CALL} \rrbracket} & \rTo &
     792\underbrace{\ldots}_{\mathtt{prologue}} \\
     793\end{diagram}
     794\end{displaymath}
     795That 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.
     796A similar property for \texttt{RETURN} should also hold, substituting the prologue for the epilogue of the function being translated:
     797\begin{displaymath}
     798\begin{diagram}
     799\mathtt{RETURN} & \rTo^1 & \mathtt{.} \\
     800\dTo & & \dTo \\
     801\underbrace{\ldots}_{\mathtt{epilogue}} & \rTo &
     802\underbrace{\ldots} \\
     803\end{diagram}
    791804\end{displaymath}
    792805
Note: See TracChangeset for help on using the changeset viewer.