Changeset 1771 for Deliverables/D1.2/CompilerProofOutline

Timestamp:

Feb 27, 2012, 3:44:43 PM (9 years ago)

Author:

mulligan

Message:

some typos fixed, commit mostly to avoid conflicts

File:

• Deliverables/D1.2/CompilerProofOutline/outline.tex (modified) (4 diffs)

Deliverables/D1.2/CompilerProofOutline/outline.tex

@@ -490 +490 @@
 \end{figure}
 
-The forward simulation proof for all steps that do not involve function
-calls are lengthy, but unsurprising. They consists in 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. The properties of $\sigma$ presented before that relate
-values and memories needs to be heavily exploited.
-
-The simulation of invocation of functions and returns from functions is
-less obvious. We sketch here what happens on the source code and on its
-translation.
+The forward simulation proof for all steps that do not involve function calls are lengthy, but routine.
+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.
+The properties of $\sigma$ presented before that relate values and memories will need to be heavily exploited.
+
+The simulation of invocation of functions and returns from functions is less obvious.
+We sketch here what happens on the source code and on its translation.
 
 \begin{displaymath}
@@ -509 +505 @@
 Suppose we are given a \texttt{State} with a list of stack frames, with the top frame being \texttt{Frame}.
 Suppose also that the program counter in \texttt{Frame} points to a \texttt{Call} instruction, complete with arguments and destination address.
-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.
+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.
 
 Now, what happens next depends on whether we are executing an internal or an external function.
@@ -551 +547 @@
 \end{array}
 \end{displaymath}
-
-\subsection{The RTL to ERTL translation}
-\label{subsect.rtl.ertl.translation}
 
 \begin{displaymath}
@@ -590 +583 @@
 \end{diagram}
 \end{displaymath}
+
+\subsection{The RTL to ERTL translation}
+\label{subsect.rtl.ertl.translation}
 
 \begin{displaymath}