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

...

File:
1 edited

Legend:

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

    r1766 r1767  
    498498\end{displaymath}
    499499That 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
     500Then the return state restores the program counter by popping the stack, and execution proceeds in a new \texttt{State}:
    501501\begin{displaymath}
    502502\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)}
    504505\end{array}
    505506\end{displaymath}
    506507
    507 In the case where the call is to an internal function, we have:
    508 
     508Suppose we are executing an internal function, however:
    509509\begin{displaymath}
    510510\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] \\
    519512\mathtt{PUSH(current\_frame[PC := after\_return])} &                 & \mathtt{State}(regs,\ sp,\ pc_\emptyset,\ dst)
    520513\end{array}
    521514\end{displaymath}
    522 
    523 then:
    524 
     515Here, execution of the \texttt{Call} state first pushes the current frame with the program counter set to the address following the function call.
     516The 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.
     517Then:
    525518\begin{displaymath}
    526519\begin{array}{rcl}
Note: See TracChangeset for help on using the changeset viewer.