Changeset 1727


Ignore:
Timestamp:
Feb 23, 2012, 1:47:03 PM (7 years ago)
Author:
boender
Message:
  • added last RTL - ERTL diagrams
File:
1 edited

Legend:

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

    r1726 r1727  
    209209&       s \stackrel{1}{\rightarrow} s^{*} \Rightarrow \exists n. s' \stackrel{n}{\rightarrow} s'^{*} \wedge s'^{*} = s'\ \sigma
    210210\end{align*}
     211
     212\begin{align*}
     213\mathrm{RTL\ status} & \ \ \mathrm{ERTL\ status} \\
     214\mathtt{sp} & = \mathtt{spl} / \mathtt{sph} \\
     215\mathtt{graph} & \mapsto \mathtt{graph} + \mathtt{prologue}(s) + \mathtt{epilogue}(s) \\
     216& \mathrm{where}\ s = \mathrm{callee\ saved} + \nu \mathrm{RA} \\
     217\end{align*}
     218
     219\begin{displaymath}
     220\begin{diagram}
     221\mathtt{CALL} & \rTo^1 & \mathtt{inside\ function} \\
     222\dTo & & \dTo \\
     223\underbrace{\ldots}_{\llbracket \mathtt{CALL} \rrbracket} & \rTo &
     224\underbrace{\ldots}_{\mathtt{prologue}} \\
     225\end{diagram}
     226\end{displaymath}
     227
     228\begin{displaymath}
     229\begin{diagram}
     230\mathtt{RETURN} & \rTo^1 & \mathtt{.} \\
     231\dTo & & \dTo \\
     232\underbrace{\ldots}_{\mathtt{epilogue}} & \rTo &
     233\underbrace{\ldots} \\
     234\end{diagram}
     235\end{displaymath}
     236
     237\begin{align*}
     238\mathtt{prologue}(s) = & \mathtt{create\_new\_frame}; \\
     239                       & \mathtt{pop\ ra}; \\
     240                       & \mathtt{save\ callee\_saved}; \\
     241                                                                                         & \mathtt{get\_params} \\
     242                                                                                         & \ \ \mathtt{reg\_params}: \mathtt{move} \\
     243                                                                                         & \ \ \mathtt{stack\_params}: \mathtt{push}/\mathtt{pop}/\mathtt{move} \\
     244\end{align*}
     245
     246\begin{align*}
     247\mathtt{epilogue}(s) = & \mathtt{save\ return\ to\ tmp\ real\ regs}; \\
     248                                                                                         & \mathtt{restore\_registers}; \\
     249                       & \mathtt{push\ ra}; \\
     250                       & \mathtt{delete\_frame}; \\
     251                       & \mathtt{save return} \\
     252\end{align*}
     253
     254\begin{displaymath}
     255\mathtt{CALL} id \mapsto \mathtt{set\_params}; \mathtt{CALL} id; \mathtt{fetch\_result}
     256\end{displaymath}
    211257
    212258\section{The ERTL to LTL translation}
Note: See TracChangeset for help on using the changeset viewer.