Changeset 1770 for Deliverables/D1.2/CompilerProofOutline/outline.tex
- Timestamp:
- Feb 27, 2012, 2:57:26 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D1.2/CompilerProofOutline/outline.tex
r1769 r1770 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. 538 538 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. 539 Then:539 After this, the stack pointer is freed and a \texttt{Return} state is entered: 540 540 \begin{displaymath} 541 541 \begin{array}{rcl} 542 542 \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)} 544 544 \end{array} 545 545 \end{displaymath} 546 547 and finally: 548 546 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: 549 547 \begin{displaymath} 550 548 \begin{array}{rcl} 551 549 \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)} 553 551 \end{array} 554 552 \end{displaymath}
Note: See TracChangeset
for help on using the changeset viewer.