Ignore:
Timestamp:
Feb 27, 2012, 5:01:31 PM (8 years ago)
Author:
mulligan
Message:

...

File:
1 edited

Legend:

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

    r1776 r1777  
    632632\end{displaymath}
    633633
     634Translation from RTLabs to RTL states proceeds as follows.
     635Return states are translated as is:
     636\begin{displaymath}
     637\mathtt{Return} \longrightarrow \mathtt{Return}
     638\end{displaymath}
     639
     640\texttt{Call} states are translated to \texttt{Call\_ID} states:
     641\begin{displaymath}
     642\mathtt{Call(id,\ args,\ dst,\ pc)} \longrightarrow \mathtt{Call\_ID(id,\ \sigma'(args),\ \sigma(dst),\ pc)}
     643\end{displaymath}
     644Here, $\sigma$ and $\sigma'$ are two maps to be defined between pseudo-registers and lists of pseudo-registers, of the type:
     645
     646\begin{displaymath}
     647\sigma: \mathtt{register} \rightarrow \mathtt{list\ register}
     648\end{displaymath}
     649
     650and:
     651
     652\begin{displaymath}
     653\sigma': \mathtt{list\ register} \rightarrow \mathtt{list\ register}
     654\end{displaymath}
     655
     656where $\sigma'$ is implemented as:
     657
     658\begin{displaymath}
     659\sigma' = \mathtt{flatten} \circ \sigma
     660\end{displaymath}
     661
     662In the case of RTL, execution proceeds as follows.
     663Suppose we are executing a \texttt{CALL\_ID} instruction.
     664Then a case split occurs depending on whether we are executing an internal or an external function, as in the RTLabs case:
    634665\begin{displaymath}
    635666\begin{diagram}
     
    641672\end{diagram}
    642673\end{displaymath}
    643 
     674Here, 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.
     675The reason for this lack of implementation is as follows.
     676Though 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.
     677Whilst 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.
     678However, 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).
     679
     680In the case of an internal function being executed, we proceed as follows.
     681The 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.
     682Further, 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.
     683
     684Note, 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
     685\begin{displaymath}
     686\mathtt{PUSH(current\_frame[PC := after\_return])}
     687\end{displaymath}
     688
     689was executed.
     690
     691The 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:
    644692\begin{align*}
    645 \llbracket \mathtt{RETURN} \rrbracket \\
    646693\mathtt{return\_addr} & := \mathtt{top}(\mathtt{stack}) \\
    647 v*                    & := m(\mathtt{rv\_regs}) \\
     694v*                    & := M(\mathtt{rv\_regs}) \\
    648695\mathtt{dst}, \mathtt{sp}, \mathtt{carry}, \mathtt{regs} & := \mathtt{pop} \\
    649696\mathtt{regs}[v* / \mathtt{dst}] \\
Note: See TracChangeset for help on using the changeset viewer.