Changeset 1767
 Timestamp:
 Feb 27, 2012, 2:45:53 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D1.2/CompilerProofOutline/outline.tex
r1766 r1767 498 498 \end{displaymath} 499 499 That is, the call to the external function enters a return state after first computing the return value by executing the external function on the arguments. 500 Then the return state 500 Then the return state restores the program counter by popping the stack, and execution proceeds in a new \texttt{State}: 501 501 \begin{displaymath} 502 502 \begin{array}{rcl} 503 \mathtt{Return(ret\_val,\ dst,\ PUSH(...))} & \longrightarrow & \mathtt{pc = POP\_STACK(regs[dst := M(ret\_val)],\ pc)} 503 \mathtt{Return(ret\_val,\ dst,\ PUSH(...))} & \longrightarrow & \mathtt{pc = POP\_STACK(regs[dst := M(ret\_val)],\ pc)} \\ 504 & & \mathtt{State(regs[dst := M(ret\_val),\ pc)} 504 505 \end{array} 505 506 \end{displaymath} 506 507 507 In the case where the call is to an internal function, we have: 508 508 Suppose we are executing an internal function, however: 509 509 \begin{displaymath} 510 510 \begin{array}{rcl} 511 \mathtt{CALL}(\mathtt{id}, \mathtt{args}, \mathtt{dst}, \mathtt{pc}) & \longrightarrow & \mathtt{CALL\_ID}(\mathtt{id}, \sigma'(\mathtt{args}), \sigma(\mathtt{dst}), \mathtt{pc}) \\ 512 \mathtt{RETURN} & \longrightarrow & \mathtt{RETURN} \\ 513 \end{array} 514 \end{displaymath} 515 516 \begin{displaymath} 517 \begin{array}{rcl} 518 \mathtt{Call(M(args), dst)} & \longrightarrow & \mathtt{sp = alloc}, regs = \emptyset[ := PARAMS] \\ 511 \mathtt{Call(M(args), dst)} & \longrightarrow & \mathtt{SP = alloc}, regs = \emptyset[ := params] \\ 519 512 \mathtt{PUSH(current\_frame[PC := after\_return])} & & \mathtt{State}(regs,\ sp,\ pc_\emptyset,\ dst) 520 513 \end{array} 521 514 \end{displaymath} 522 523 then: 524 515 Here, execution of the \texttt{Call} state first pushes the current frame with the program counter set to the address following the function call. 516 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. 517 Then: 525 518 \begin{displaymath} 526 519 \begin{array}{rcl}
Note: See TracChangeset
for help on using the changeset viewer.