Changeset 1727 for Deliverables/D1.2/CompilerProofOutline/outline.tex
 Timestamp:
 Feb 23, 2012, 1:47:03 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D1.2/CompilerProofOutline/outline.tex
r1726 r1727 209 209 & s \stackrel{1}{\rightarrow} s^{*} \Rightarrow \exists n. s' \stackrel{n}{\rightarrow} s'^{*} \wedge s'^{*} = s'\ \sigma 210 210 \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} 211 257 212 258 \section{The ERTL to LTL translation}
Note: See TracChangeset
for help on using the changeset viewer.