# Changeset 1763 for Deliverables/D1.2

Ignore:
Timestamp:
Feb 27, 2012, 1:52:30 PM (9 years ago)
Message:

to avoid conflicts

File:
1 edited

### Legend:

Unmodified
 r1762 This will entail more proof obligations, demonstrating that the $\sigma$-map between memory spaces respects memory regions. RTLabs states come in three flavours: \begin{displaymath} \begin{array}{rll} \end{array} \end{displaymath} \texttt{State} is the default state in which RTLabs programs are almost always in. The \texttt{Call} state is only entered when a call instruction is being executed, and then we immediately return to being in \texttt{State}. Similarly, \texttt{Return} is only entered when a return instruction is being executed, before returning immediately to \texttt{State}. All RTLabs states are accompanied by a memory, \texttt{Mem}, with \texttt{Call} and \texttt{Return} keeping track of arguments, return addresses and the results of functions. \texttt{State} keeps track of a list of stack frames. RTL states differ from their RTLabs counterparts, in including a program counter \texttt{PC}, stack-pointer \texttt{SP}, internal stack pointer \texttt{ISP}, a carry flag \texttt{CARRY} and a set of registers \texttt{REGS}: \begin{displaymath} \mathtt{State} ::= \mathtt{Frame}^* \times \mathtt{PC} \times \mathtt{SP} \times \mathtt{ISP} \times \mathtt{CARRY} \times \mathtt{REGS} \end{displaymath} The internal stack pointer \texttt{ISP}, and its relationship with the stack pointer \texttt{SP}, needs some comment. Due to the design of the MCS-51, and its minuscule stack, it was decided that the compiler would implement an emulated stack in external memory. As a result, we have two stack pointers in our state: \texttt{ISP}, which is the real, hardware stack, and \texttt{SP}, which is the stack pointer of the emulated stack in memory. The emulated stack is used for pushing and popping stack frames when calling or returning from function calls, however this is done using the hardware stack, indexed by \texttt{ISP} as an intermediary. Instructions like \texttt{LCALL} and \texttt{ACALL} are hardwired by the processor's design to push on to the hardware stack, therefore after a call has been made, and after a call returns, the compiler emits code to move parameters and return addresses to-and-from the hardware stack. As a result, for most of the execution of the processor, the hardware stack is empty, or contains a single item ready to be moved into external memory. Once more, we require a map from RTLabs states to RTL states. Call it $\sigma$: \begin{displaymath} \mathtt{State} \stackrel{\sigma}{\longrightarrow} \mathtt{State} \end{displaymath} \begin{displaymath} \sigma(\mathtt{State} (\mathtt{Frame}^* \times \mathtt{Frame})) \longrightarrow ((\sigma(\mathtt{Frame}^*), \sigma(\mathtt{PC}), \sigma(\mathtt{SP}), 0, 0, \sigma(\mathtt{REGS})), \sigma(\mathtt{Mem})) \end{displaymath} Translating an RTLabs state to an RTL state proceeds by cases on the particular type of state we are trying to translate, either a \texttt{State}, \texttt{Call} or a \texttt{Return}. For \texttt{State} we perform a further case analysis of the top stack frame, which decomposes into a tuple holding the current program counter value, the current stack pointer and the value of the registers: \begin{displaymath} \sigma(\mathtt{State} (\mathtt{Frame}^* \times \mathtt{\langle PC, REGS, SP \rangle})) \longrightarrow ((\sigma(\mathtt{Frame}^*), \sigma(\mathtt{PC}), \sigma(\mathtt{SP}), 0, 0, \sigma(\mathtt{REGS})), \sigma(\mathtt{Mem})) \end{displaymath} Translation then proceeds by translating the remaining stack frames, as well as the contents of the top stack frame, and setting all untranslated values to zero, their default value. Translating \texttt{Call} and \texttt{Return} states is more involved, as a commutation between a single step of execution and the translation process must hold: \begin{displaymath} \sigma(\mathtt{Return}(-)) \longrightarrow \sigma \circ \text{return one step} \end{displaymath} Return one step commuting diagram: Here \emph{return one step} and \emph{call one step} refer to a pair of commuting diagrams relating the one-step execution of a call and return state and translation of both. We provide the one step commuting diagrams in Figure~\ref{fig.commuting.diagrams}. \begin{figure} \begin{displaymath} \begin{diagram} \end{displaymath} Call one step commuting diagram: \begin{displaymath} \begin{diagram} \end{diagram} \end{displaymath} \caption{The one-step commuting diagrams for \texttt{Call} and \texttt{Return} state translations} \label{fig.commuting.diagrams} \end{figure} We outline how states are executed: \begin{displaymath} \begin{array}{rcl} \mathtt{Call(id,\ args,\ dst,\ pc),\ State(FRAME, FRAMES)} & \longrightarrow & \mathtt{Call(M(args), dst)}, \\ &                 & \mathtt{PUSH(current\_frame[PC := after\_return])} \mathtt{Call(id,\ args,\ dst,\ pc),\ State(Frame^*, Frame)} & \longrightarrow & \mathtt{Call(M(args), dst)}, \\ &                 & \mathtt{PUSH(Frame[PC := after\_return])} \end{array} \end{displaymath} Suppose we are given a \texttt{State} with a list of stack frames, with the top frame being \texttt{Frame}. Suppose also that the program counter in \texttt{Frame} points to a \texttt{Call} instruction, complete with arguments and destination address. Then this is executed by entering into a \texttt{Call} state were the arguments are looked up in memory, and the destination address is filled in, with the current stack frame being pushed on top of the stack with the return address substituted for the program counter. Now, what happens next depends on whether we are executing an internal or an external function. In the case where the call is to an external function, we have: \begin{displaymath} \begin{array}{rcl} \end{displaymath} then: \mathtt{free(sp)}                         & \longrightarrow & \mathtt{pc = POP\_STACK(regs[dst := M(ret\_val)],\ pc)} \\ \mathtt{Return(M(ret\_val), dst, frames)} &                 & \end{array} \end{displaymath} \begin{displaymath} \begin{array}{rcl} \sigma & : & \mathtt{register} \rightarrow \mathtt{list\ register} \\ \sigma' & : & \mathtt{list\ register} \rightarrow \mathtt{list\ register} \end{array} \end{displaymath}