# Changeset 1200 for Deliverables

Ignore:
Timestamp:
Sep 9, 2011, 11:03:20 AM (9 years ago)
Message:

small changes and rewordings to decrease length

File:
1 edited

### Legend:

Unmodified
 r1199 \begin{abstract} We summarise the formalisation of two emulators for the MCS-51 microprocessor in O'Caml and the Matita proof assistant. The MCS-51 is a widely used 8-bit microprocessor, especially popular in embedded devices. We summarise the formalisation of emulators for the MCS-51 microprocessor in O'Caml and the Matita proof assistant. The MCS-51 is a widely used microprocessor, especially popular in embedded devices. The O'Caml emulator is intended to be feature complete' with respect to the MCS-51 device. \emph{An optimisation specified only extensionally is only half specified}; the optimisation may preserve the denotational semantics of a program, but there is no guarantee that intentional properties of the program improve. Another potential application is toward completeness and correctness of the compilation process in the presence of space constraints. A compiler could reject a source program targetting an embedded system when the size of the compiled code exceeds the available ROM size. Preservation of a program's semantics may only be required for those programs that do not exhaust the stack or heap. Another potential application is the completeness and correctness of the compilation process in the presence of space constraints. A compiler could reject a source program targetting an embedded system when the size of the compiled code exceeds available ROM size. Preservation of semantics may only be required for those programs that do not exhaust the stack or heap. The statement of completeness of the compiler must take into account a realistic cost model. \paragraph*{The MCS-51}\quad The MCS-51 is an 8-bit microprocessor introduced by Intel in the late 1970s. Commonly called the 8051, in the decades since its introduction the processor has become a popular component of embedded systems. The processor and derivatives are still manufactured \emph{en masse} by a host of vendors. Surprisingly, however, there is not yet a formal model of the MCS-51. The MCS-51 is an 8-bit microprocessor. Commonly called the 8051, since its introduction by Intel the processor has become a popular component of embedded systems. Despite being manufactured \emph{en masse}, there is not yet a formal model of the MCS-51. The 8051 is a well documented processor, with very few underspecified behaviours (almost all of these correspond to erroneous usage of the processor). \centering \setlength{\unitlength}{0.87pt} \small{ \begin{picture}(410,250)(-50,200) %\put(-50,200){\framebox(410,250){}} \put(264,324){\makebox(80,0){Direct}} \put(264,310){\makebox(80,0){PC relative}} \end{picture} \end{picture}} \caption{The 8051 memory model} \label{fig.memory.layout} We may use Matita's type system to provide precise typings for functions that are polymorphic in the size without code duplication: \begin{lstlisting}[frame=single] let rec split (A: Type[0]) (m,n: nat) on m: Vector A (m+n) $\rightarrow$ (Vector A m)$\times$(Vector A n) := ... let rec split (A: Type[0]) (m,n: nat) on m: Vector A (m+n) $\rightarrow$ (Vector A m)$\times$(Vector A n) := ... \end{lstlisting} Further, we assumed that large swathes of memory would often be uninitialized (an assumption on the behaviour of the programmer, not the processor!) We picked a modified form of trie of fixed height $h$. Paths are represented by bitvectors (already used in the implementation for addresses and registers) of length $h$: We use a modified form of trie of fixed height $h$. Paths are represented by bitvectors (used also for addresses and registers) of length $h$: \begin{lstlisting}[frame=single] inductive BitVectorTrie(A: Type[0]):nat $\rightarrow$ Type[0] := All manufacturer data sheets that we consulted were silent on the subject of what should be returned if we attempt to access uninitialized memory. We defaulted to simply returning zero, though our \texttt{lookup} function is parametric in this choice. We believe that this is reasonable, as SDCC for instance generates code which first zeroes' memory in a preamble before executing the program proper. This is reasonable, as SDCC for instance generates code which first `zeroes' memory in a preamble before executing the program proper. This is in line with the C standard, which guarantees that all global variables will be zero initialized piecewise. The types \texttt{union2}, \texttt{union3} and \texttt{union6} sufficed. This polymorphic variant machinery worked well: it introduced a certain level of type safety (for instance, the type of \texttt{MOV} above guarantees it cannot be invoked with arguments in the \texttt{carry} and \texttt{data16} addressing modes, respectively), and also allowed us to pattern match against instructions, when necessary. This polymorphic variant machinery worked well: it introduced a certain level of type safety (the type of \texttt{MOV} above guarantees it cannot be invoked with arguments in the \texttt{carry} and \texttt{data16} addressing modes), and also allowed us to pattern match against instructions, when necessary. However, this polymorphic variant machinery is \emph{not} present in Matita. We needed some way to produce the same effect, which Matita supported. For instance, consider \texttt{set\_arg\_16}, which expects only a \texttt{DPTR}: \begin{lstlisting}[frame=single] definition set_arg_16: Status $\rightarrow$ Word $\rightarrow$ $\llbracket$dptr$\rrbracket$ $\rightarrow$ Status := $~\lambda$s, v, a. match a return $\lambda$x. bool_to_Prop (is_in ? $\llbracket$dptr$\rrbracket$ x) $\rightarrow$ ? with definition set_arg_16: Status $\rightarrow$ Word $\rightarrow$ $\llbracket$dptr$\rrbracket$ $\rightarrow$ Status := $~\lambda$s, v, a. match a return $\lambda$x. bool_to_Prop (is_in ? $\llbracket$dptr$\rrbracket$ x) $\rightarrow$ ? with [ DPTR $\Rightarrow$ $\lambda$_: True. let $\langle$bu, bl$\rangle$ := split $\ldots$ eight eight v in