Changeset 1771 for Deliverables/D1.2/CompilerProofOutline
- Timestamp:
- Feb 27, 2012, 3:44:43 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D1.2/CompilerProofOutline/outline.tex
r1770 r1771 490 490 \end{figure} 491 491 492 The forward simulation proof for all steps that do not involve function 493 calls are lengthy, but unsurprising. They consists in simulating a 494 front-end operation on front-end pseudo-registers and the front-end memory 495 with sequences of back-end operations on the back-end pseudo-registers 496 and back-end memory. The properties of $\sigma$ presented before that relate 497 values and memories needs to be heavily exploited. 498 499 The simulation of invocation of functions and returns from functions is 500 less obvious. We sketch here what happens on the source code and on its 501 translation. 492 The forward simulation proof for all steps that do not involve function calls are lengthy, but routine. 493 They consist of simulating a front-end operation on front-end pseudo-registers and the front-end memory with sequences of back-end operations on the back-end pseudo-registers and back-end memory. 494 The properties of $\sigma$ presented before that relate values and memories will need to be heavily exploited. 495 496 The simulation of invocation of functions and returns from functions is less obvious. 497 We sketch here what happens on the source code and on its translation. 502 498 503 499 \begin{displaymath} … … 509 505 Suppose we are given a \texttt{State} with a list of stack frames, with the top frame being \texttt{Frame}. 510 506 Suppose also that the program counter in \texttt{Frame} points to a \texttt{Call} instruction, complete with arguments and destination address. 511 Then this is executed by entering into a \texttt{Call} state w ere the arguments are looked up in memory, and the destination addressis filled in, with the current stack frame being pushed on top of the stack with the return address substituted for the program counter.507 Then this is executed by entering into a \texttt{Call} state where the arguments are loaded from memory, and the address pointing to the instruction immediately following the \texttt{Call} instruction is filled in, with the current stack frame being pushed on top of the stack with the return address substituted for the program counter. 512 508 513 509 Now, what happens next depends on whether we are executing an internal or an external function. … … 551 547 \end{array} 552 548 \end{displaymath} 553 554 \subsection{The RTL to ERTL translation}555 \label{subsect.rtl.ertl.translation}556 549 557 550 \begin{displaymath} … … 590 583 \end{diagram} 591 584 \end{displaymath} 585 586 \subsection{The RTL to ERTL translation} 587 \label{subsect.rtl.ertl.translation} 592 588 593 589 \begin{displaymath}
Note: See TracChangeset
for help on using the changeset viewer.