Changeset 1777 for Deliverables/D1.2/CompilerProofOutline/outline.tex
- Timestamp:
- Feb 27, 2012, 5:01:31 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D1.2/CompilerProofOutline/outline.tex
r1776 r1777 632 632 \end{displaymath} 633 633 634 Translation from RTLabs to RTL states proceeds as follows. 635 Return 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} 644 Here, $\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 650 and: 651 652 \begin{displaymath} 653 \sigma': \mathtt{list\ register} \rightarrow \mathtt{list\ register} 654 \end{displaymath} 655 656 where $\sigma'$ is implemented as: 657 658 \begin{displaymath} 659 \sigma' = \mathtt{flatten} \circ \sigma 660 \end{displaymath} 661 662 In the case of RTL, execution proceeds as follows. 663 Suppose we are executing a \texttt{CALL\_ID} instruction. 664 Then a case split occurs depending on whether we are executing an internal or an external function, as in the RTLabs case: 634 665 \begin{displaymath} 635 666 \begin{diagram} … … 641 672 \end{diagram} 642 673 \end{displaymath} 643 674 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. 675 The reason for this lack of implementation is as follows. 676 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. 677 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. 678 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). 679 680 In the case of an internal function being executed, we proceed as follows. 681 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. 682 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. 683 684 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 685 \begin{displaymath} 686 \mathtt{PUSH(current\_frame[PC := after\_return])} 687 \end{displaymath} 688 689 was executed. 690 691 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: 644 692 \begin{align*} 645 \llbracket \mathtt{RETURN} \rrbracket \\646 693 \mathtt{return\_addr} & := \mathtt{top}(\mathtt{stack}) \\ 647 v* & := m(\mathtt{rv\_regs}) \\694 v* & := M(\mathtt{rv\_regs}) \\ 648 695 \mathtt{dst}, \mathtt{sp}, \mathtt{carry}, \mathtt{regs} & := \mathtt{pop} \\ 649 696 \mathtt{regs}[v* / \mathtt{dst}] \\
Note: See TracChangeset
for help on using the changeset viewer.