Changeset 1780 for Deliverables/D1.2/CompilerProofOutline
 Timestamp:
 Feb 27, 2012, 5:45:00 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D1.2/CompilerProofOutline/outline.tex
r1779 r1780 745 745 \end{displaymath} 746 746 747 \subsection{The RTL to ERTL translation} 748 \label{subsect.rtl.ertl.translation} 749 750 We map RTL statuses to ERTL statuses as follows: 747 751 \begin{align*} 748 \mathrm{RTL\ status} & \ \ \mathrm{ERTL\ status} \\ 749 \mathtt{sp} & = \mathtt{spl} / \mathtt{sph} \\ 752 \mathtt{sp} & = \mathtt{RegisterSPH} / \mathtt{RegisterSPL} \\ 750 753 \mathtt{graph} & \mathtt{graph} + \mathtt{prologue}(s) + \mathtt{epilogue}(s) \\ 751 754 & \mathrm{where}\ s = \mathrm{callee\ saved} + \nu \mathrm{RA} \\ 752 755 \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 756 The 16bit RTL stack pointer \texttt{SP} is mapped to a pair of 8bit hardware registers \texttt{RegisterSPH} and \texttt{RegisterSPL}. 757 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. 758 759 The prologue and epilogue that are added to the function graph do the following: 772 760 \begin{align*} 773 761 \mathtt{prologue}(s) = & \mathtt{create\_new\_frame}; \\ … … 778 766 & \ \ \mathtt{stack\_params}: \mathtt{push}/\mathtt{pop}/\mathtt{move} \\ 779 767 \end{align*} 780 768 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. 769 In other words, the prologue of a function correctly sets up the calling convention used in the compiler when calling a function. 770 On the other hand, the epilogue undoes the action of the prologue: 781 771 \begin{align*} 782 772 \mathtt{epilogue}(s) = & \mathtt{save\ return\ to\ tmp\ real\ regs}; \\ … … 786 776 & \mathtt{save return} \\ 787 777 \end{align*} 788 778 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. 779 780 The \texttt{CALL} instruction is translated as follows: 789 781 \begin{displaymath} 790 782 \mathtt{CALL}\ id \mapsto \mathtt{set\_params};\ \mathtt{CALL}\ id;\ \mathtt{fetch\_result} 783 \end{displaymath} 784 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. 785 786 The 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} 795 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. 796 A 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} 791 804 \end{displaymath} 792 805
Note: See TracChangeset
for help on using the changeset viewer.