# Changeset 984

Ignore:
Timestamp:
Jun 16, 2011, 4:16:41 PM (9 years ago)
Message:

 r983 PseudoStatus $\rightarrow$ PseudoStatus := $\ldots$ \end{lstlisting} Notice, here, that the emulation function for pseudoprograms takes an additional argument. This is a function that maps program counters (for the pseudoprogram) to pairs of natural numbers representing the number of clock ticks that the pseudoinstruction needs to execute, post expansion. Notice, here, that the emulation function for assembly programs takes an additional argument. This is a function that maps program counters (at the assembly level) to pairs of natural numbers representing the number of clock ticks that the pseudoinstruction needs to execute, post expansion. We call this function a \emph{costing}, and note that the costing is induced by the particular strategy we use to expand pseudoinstructions. If we change how we expand conditional jumps to labels, for instance, then the costing needs to change, hence \texttt{execute\_1\_pseudo\_instruction}'s parametricity in the costing. However, this property is \emph{not} strong enough to establish that the semantics of an assembly program has been preserved by the assembly process. In particular, \texttt{fetch\_assembly\_pseudo2} says nothing about how An \texttt{internal\_pseudo\_address\_map} positions in the memory of a \texttt{PseudoStatus} with a physical memory address. In particular, \texttt{fetch\_assembly\_pseudo2} says nothing about how memory addresses evolve during assembly. Memory addresses in one memory space may be mapped to memory addresses in a completely different memory space during assembly. To handle this problem, we need some more machinery. We use an \texttt{internal\_pseudo\_address\_map} for this purpose. An \texttt{internal\_pseudo\_address\_map} associates positions in the memory of a \texttt{PseudoStatus} with a physical memory address: \begin{lstlisting} definition internal_pseudo_address_map := list (BitVector 8). \end{lstlisting} We use \texttt{internal\_pseudo\_address\_map}s to convert the lower internal RAM of a \texttt{PseudoStatus} into the lower internal RAM of a \texttt{Status}. The actual conversion process is performed by \texttt{low\_internal\_ram\_of\_pseudo\_low\_internal\_ram}:\footnote{An associated set of axioms describe how \texttt{low\_internal\_ram\_of\_pseudo\_low\_internal\_ram} behaves.  This is a form of parametricity.  We don't care about the particulars of the conversion functions, as long as they behave in accordance with our axioms.} \begin{lstlisting} axiom low_internal_ram_of_pseudo_low_internal_ram: internal_pseudo_address_map $\rightarrow$ BitVectorTrie Byte 7 $\rightarrow$ BitVectorTrie Byte 7. \end{lstlisting} A similar axiom exists for high internal RAM. Notice, the MCS-51's internal RAM is addressed with a 7-bit `byte'. % dpm: ugly English, fix The whole of the internal RAM space is addressed with bytes: the first bit is used to distinguish between the programmer addressing low and high internal memory. \begin{lstlisting} axiom low_internal_ram_of_pseudo_low_internal_ram: internal_pseudo_address_map $\rightarrow$ BitVectorTrie Byte 7 $\rightarrow$ BitVectorTrie Byte 7. \end{lstlisting} A similar axiom exists for high internal RAM. Next, we are able to translate \texttt{PseudoStatus} records into \texttt{Status} records using \texttt{status\_of\_pseudo\_status}.