Changeset 1734


Ignore:
Timestamp:
Feb 24, 2012, 11:44:01 AM (7 years ago)
Author:
mulligan
Message:

followed brian's lead in explaining the backend translation steps with a handy diagram, some more changes, commit to avoid conflicts also

File:
1 edited

Legend:

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

    r1733 r1734  
    243243flattening result to show that it is correct.
    244244
    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
     248The 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 endo-transformation) \\
     258\> $\downarrow$ \> copy propagation (an endo-transformation) \\
     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 endo-transformation) \\
     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
     276Here, by `endo-transformation', we mean a mapping from language back to itself.
     277For 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}
    247281
    248282% dpm: type system and casting load (???)
     
    360394\end{displaymath}
    361395
    362 \section{The RTL to ERTL translation}
    363 \label{sect.rtl.ertl.translation}
     396\subsection{The RTL to ERTL translation}
     397\label{subsect.rtl.ertl.translation}
    364398
    365399\begin{displaymath}
     
    463497\end{displaymath}
    464498
    465 \section{The ERTL to LTL translation}
    466 \label{sect.ertl.ltl.translation}
    467 
    468 \section{The LTL to LIN translation}
    469 \label{sect.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}
    470504
    471505We 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:
     
    543577Each well-formed 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.
    544578
    545 \section{The LIN to ASM and ASM to MCS-51 machine code translations}
    546 \label{sect.lin.asm.translation}
     579\subsection{The LIN to ASM and ASM to MCS-51 machine code translations}
     580\label{subsect.lin.asm.translation}
    547581
    548582The LIN to ASM translation step is trivial, being almost the identity function.
Note: See TracChangeset for help on using the changeset viewer.