Changeset 1734
 Timestamp:
 Feb 24, 2012, 11:44:01 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D1.2/CompilerProofOutline/outline.tex
r1733 r1734 243 243 flattening result to show that it is correct. 244 244 245 \section{The RTLabs to RTL translation} 246 \label{sect.rtlabs.rtl.translation} 245 \section{Backend: RTLabs to machine code} 246 \label{sect.backend.rtlabs.machine.code} 247 248 The compiler backend consists of the following intermediate languages, and stages of translation: 249 250 \begin{center} 251 \begin{minipage}{.8\linewidth} 252 \begin{tabbing} 253 \quad \= $\downarrow$ \quad \= \kill 254 \textsf{RTLabs}\\ 255 \> $\downarrow$ \> instruction selection\\ 256 \textsf{RTL}\\ 257 \> $\downarrow$ \> constant propagation (an endotransformation) \\ 258 \> $\downarrow$ \> copy propagation (an endotransformation) \\ 259 \> $\downarrow$ \> calling convention made explicit \\ 260 \> $\downarrow$ \> stack frame generation \\ 261 \textsf{ERTL}\\ 262 \> $\downarrow$ \> register allocation and spilling\\ 263 \> $\downarrow$ \> dead code elimination\\ 264 \textsf{LTL}\\ 265 \> $\downarrow$ \> function linearisation\\ 266 \> $\downarrow$ \> branch compression (an endotransformation) \\ 267 \textsf{LIN}\\ 268 \> $\downarrow$ \> relabeling\\ 269 \textsf{ASM}\\ 270 \> $\downarrow$ \> pseudoinstruction expansion\\ 271 \textsf{Machine code}\\ 272 \end{tabbing} 273 \end{minipage} 274 \end{center} 275 276 Here, by `endotransformation', we mean a mapping from language back to itself. 277 For example, the constant propagation step maps the RTL language to the RTL language. 278 279 \subsection{The RTLabs to RTL translation} 280 \label{subsect.rtlabs.rtl.translation} 247 281 248 282 % dpm: type system and casting load (???) … … 360 394 \end{displaymath} 361 395 362 \s ection{The RTL to ERTL translation}363 \label{s ect.rtl.ertl.translation}396 \subsection{The RTL to ERTL translation} 397 \label{subsect.rtl.ertl.translation} 364 398 365 399 \begin{displaymath} … … 463 497 \end{displaymath} 464 498 465 \s ection{The ERTL to LTL translation}466 \label{s ect.ertl.ltl.translation}467 468 \s ection{The LTL to LIN translation}469 \label{s ect.ltl.lin.translation}499 \subsection{The ERTL to LTL translation} 500 \label{subsect.ertl.ltl.translation} 501 502 \subsection{The LTL to LIN translation} 503 \label{subsect.ltl.lin.translation} 470 504 471 505 We require a map, $\sigma$, from LTL statuses, where program counters are represented as labels in a graph data structure, to LIN statuses, where program counters are natural numbers: … … 543 577 Each wellformed function must end with a call to \texttt{RET}, and therefore the only correct instruction that can terminate a LIN program is a \texttt{RET} instruction. 544 578 545 \s ection{The LIN to ASM and ASM to MCS51 machine code translations}546 \label{s ect.lin.asm.translation}579 \subsection{The LIN to ASM and ASM to MCS51 machine code translations} 580 \label{subsect.lin.asm.translation} 547 581 548 582 The LIN to ASM translation step is trivial, being almost the identity function.
Note: See TracChangeset
for help on using the changeset viewer.