Changeset 1777 for Deliverables/D1.2

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


1 edited


  • Deliverables/D1.2/CompilerProofOutline/outline.tex

    r1776 r1777  
     634Translation from RTLabs to RTL states proceeds as follows.
     635Return states are translated as is:
     637\mathtt{Return} \longrightarrow \mathtt{Return}
     640\texttt{Call} states are translated to \texttt{Call\_ID} states:
     642\mathtt{Call(id,\ args,\ dst,\ pc)} \longrightarrow \mathtt{Call\_ID(id,\ \sigma'(args),\ \sigma(dst),\ pc)}
     644Here, $\sigma$ and $\sigma'$ are two maps to be defined between pseudo-registers and lists of pseudo-registers, of the type:
     647\sigma: \mathtt{register} \rightarrow \mathtt{list\ register}
     653\sigma': \mathtt{list\ register} \rightarrow \mathtt{list\ register}
     656where $\sigma'$ is implemented as:
     659\sigma' = \mathtt{flatten} \circ \sigma
     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:
     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).
     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.
     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
     686\mathtt{PUSH(current\_frame[PC := after\_return])}
     689was executed.
     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:
    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.