Changeset 1771 for Deliverables


Ignore:
Timestamp:
Feb 27, 2012, 3:44:43 PM (8 years ago)
Author:
mulligan
Message:

some typos fixed, commit mostly to avoid conflicts

File:
1 edited

Legend:

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

    r1770 r1771  
    490490\end{figure}
    491491
    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.
     492The forward simulation proof for all steps that do not involve function calls are lengthy, but routine.
     493They 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.
     494The properties of $\sigma$ presented before that relate values and memories will need to be heavily exploited.
     495
     496The simulation of invocation of functions and returns from functions is less obvious.
     497We sketch here what happens on the source code and on its translation.
    502498
    503499\begin{displaymath}
     
    509505Suppose we are given a \texttt{State} with a list of stack frames, with the top frame being \texttt{Frame}.
    510506Suppose 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 were the arguments are looked up in memory, and the destination address is filled in, with the current stack frame being pushed on top of the stack with the return address substituted for the program counter.
     507Then 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.
    512508
    513509Now, what happens next depends on whether we are executing an internal or an external function.
     
    551547\end{array}
    552548\end{displaymath}
    553 
    554 \subsection{The RTL to ERTL translation}
    555 \label{subsect.rtl.ertl.translation}
    556549
    557550\begin{displaymath}
     
    590583\end{diagram}
    591584\end{displaymath}
     585
     586\subsection{The RTL to ERTL translation}
     587\label{subsect.rtl.ertl.translation}
    592588
    593589\begin{displaymath}
Note: See TracChangeset for help on using the changeset viewer.