Changeset 1770


Ignore:
Timestamp:
Feb 27, 2012, 2:57:26 PM (8 years ago)
Author:
mulligan
Message:

...

File:
1 edited

Legend:

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

    r1769 r1770  
    537537Here, execution of the \texttt{Call} state first pushes the current frame with the program counter set to the address following the function call.
    538538The 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.
    539 Then:
     539After this, the stack pointer is freed and a \texttt{Return} state is entered:
    540540\begin{displaymath}
    541541\begin{array}{rcl}
    542542\mathtt{sp = alloc}, regs = \emptyset[- := PARAMS] & \longrightarrow & \mathtt{free(sp)} \\
    543 \mathtt{State}(regs,\ sp,\ pc_\emptyset,\ dst)     &                 & \mathtt{Return(M(ret\_val), dst, frames)}
     543\mathtt{State}(regs,\ sp,\ pc_\emptyset,\ dst)     &                 & \mathtt{Return(M(ret\_val), dst, Frames)}
    544544\end{array}
    545545\end{displaymath}
    546 
    547 and finally:
    548 
     546Then 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:
    549547\begin{displaymath}
    550548\begin{array}{rcl}
    551549\mathtt{free(sp)}                         & \longrightarrow & \mathtt{pc = POP\_STACK(regs[dst := M(ret\_val)],\ pc)} \\
    552 \mathtt{Return(M(ret\_val), dst, frames)} &                 &
     550\mathtt{Return(M(ret\_val), dst, frames)} &                 & \mathtt{State(regs[dst := M(ret\_val),\ pc)}
    553551\end{array}
    554552\end{displaymath}
Note: See TracChangeset for help on using the changeset viewer.