Changeset 1770 for Deliverables/D1.2/CompilerProofOutline/outline.tex

Timestamp:

Feb 27, 2012, 2:57:26 PM (9 years ago)

Author:

mulligan

Message:

...

File:

• Deliverables/D1.2/CompilerProofOutline/outline.tex (modified) (1 diff)

Deliverables/D1.2/CompilerProofOutline/outline.tex

@@ -537 +537 @@
 Here, execution of the \texttt{Call} state first pushes the current frame with the program counter set to the address following the function call.
 The stack pointer allocates more space, the register map is initialized first to the empty map, assigning an undefined value to all register, before the value of the parameters is inserted into the map into the argument registers, and a new \texttt{State} follows.
-Then:
+After this, the stack pointer is freed and a \texttt{Return} state is entered:
 \begin{displaymath}
 \begin{array}{rcl}
 \mathtt{sp = alloc}, regs = \emptyset[- := PARAMS] & \longrightarrow & \mathtt{free(sp)} \\
-\mathtt{State}(regs,\ sp,\ pc_\emptyset,\ dst)     &                 & \mathtt{Return(M(ret\_val), dst, frames)}
+\mathtt{State}(regs,\ sp,\ pc_\emptyset,\ dst)     &                 & \mathtt{Return(M(ret\_val), dst, Frames)}
 \end{array}
 \end{displaymath}
-
-and finally:
-
+Then the return state restores the program counter by popping the stack, and execution proceeds in a new \texttt{State}, like the case for external functions:
 \begin{displaymath}
 \begin{array}{rcl}
 \mathtt{free(sp)}                         & \longrightarrow & \mathtt{pc = POP\_STACK(regs[dst := M(ret\_val)],\ pc)} \\
-\mathtt{Return(M(ret\_val), dst, frames)} &                 & 
+\mathtt{Return(M(ret\_val), dst, frames)} &                 & \mathtt{State(regs[dst := M(ret\_val),\ pc)}
 \end{array}
 \end{displaymath}