Changeset 1777 for Deliverables/D1.2/CompilerProofOutline/outline.tex

Timestamp:

Feb 27, 2012, 5:01:31 PM (8 years ago)

Author:

mulligan

Message:

...

File:

• Deliverables/D1.2/CompilerProofOutline/outline.tex (modified) (2 diffs)

Deliverables/D1.2/CompilerProofOutline/outline.tex

@@ -632 +632 @@
 \end{displaymath}
 
+Translation from RTLabs to RTL states proceeds as follows.
+Return states are translated as is:
+\begin{displaymath}
+\mathtt{Return} \longrightarrow \mathtt{Return}
+\end{displaymath}
+
+\texttt{Call} states are translated to \texttt{Call\_ID} states:
+\begin{displaymath}
+\mathtt{Call(id,\ args,\ dst,\ pc)} \longrightarrow \mathtt{Call\_ID(id,\ \sigma'(args),\ \sigma(dst),\ pc)}
+\end{displaymath}
+Here, $\sigma$ and $\sigma'$ are two maps to be defined between pseudo-registers and lists of pseudo-registers, of the type:
+
+\begin{displaymath}
+\sigma: \mathtt{register} \rightarrow \mathtt{list\ register}
+\end{displaymath}
+
+and:
+
+\begin{displaymath}
+\sigma': \mathtt{list\ register} \rightarrow \mathtt{list\ register}
+\end{displaymath}
+
+where $\sigma'$ is implemented as:
+
+\begin{displaymath}
+\sigma' = \mathtt{flatten} \circ \sigma
+\end{displaymath}
+
+In the case of RTL, execution proceeds as follows.
+Suppose we are executing a \texttt{CALL\_ID} instruction.
+Then a case split occurs depending on whether we are executing an internal or an external function, as in the RTLabs case:
 \begin{displaymath}
 \begin{diagram}
@@ -641 +672 @@
 \end{diagram}
 \end{displaymath}
-
+Here, however, we differ from RTLabs when we attempt to execute an external function, in that we use a daemon (i.e. an axiom that can close any goal) to artificially close the case, as we have not yet implemented external functions in the backend.
+The reason for this lack of implementation is as follows.
+Though we have implemented an optimising assembler as the target of the compiler's backend, we have not yet implemented a linker for that assembler, so external functions can not yet be called.
+Whilst external functions are carried forth throughout the entirety of the compiler's frontend, we choose not to do the same for the backend, instead eliminating them in RTL.
+However, it is plausible that we could have carried external functions forth, in order to eliminate them at a later stage (i.e. when translating from LIN to assembly).
+
+In the case of an internal function being executed, we proceed as follows.
+The register map is initialized to the empty map, where all registers are assigned the undefined value, and then the registers corresponding to the function parameters are assigned the value of the parameters.
+Further, the stack pointer is reallocated to make room for an extra stack frame, then a frame is pushed onto the stack with the correct address to jump back to in place of the program counter.
+
+Note, in particular, that this final act of pushing a frame on the stack leaves us in an identical state to the RTLabs case, where the instruction
+\begin{displaymath}
+\mathtt{PUSH(current\_frame[PC := after\_return])}
+\end{displaymath}
+
+was executed.
+
+The execution of \texttt{Return} in RTL is similarly straightforward, with the return address, stack pointer, and so on, being computed by popping off the top of the stack, and the return value computed by the function being retrieved from memory:
 \begin{align*}
-\llbracket \mathtt{RETURN} \rrbracket \\
 \mathtt{return\_addr} & := \mathtt{top}(\mathtt{stack}) \\
-v*                    & := m(\mathtt{rv\_regs}) \\
+v*                    & := M(\mathtt{rv\_regs}) \\
 \mathtt{dst}, \mathtt{sp}, \mathtt{carry}, \mathtt{regs} & := \mathtt{pop} \\
 \mathtt{regs}[v* / \mathtt{dst}] \\