Changeset 508


Ignore:
Timestamp:
Feb 14, 2011, 3:24:55 PM (6 years ago)
Author:
mulligan
Message:

Changes

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/ITP-Paper/itp-2011.tex

    r507 r508  
    198198\label{subsect.labels.pseudoinstructions}
    199199
    200 The MCS-51's instruction set has numerous instructions for jumping to memory locations, calling procedures and moving data between memory spaces.
    201 For instance, the instructions \texttt{AJMP}, \texttt{JMP} and \texttt{LJMP} all perform jumps.
    202 However, these instructions differ in how large the maximum size of the offset in memory of the jump performed can be.
    203 Selecting a jump instruction therefore requires the compiler to compute the size of the offset and select the most suitable instruction.
    204 
    205 In parallel with the implementation of the emulator was the implementation of a prototype compiler.
    206 It was recognised that it would simplify the design of the compiler if the emulator introduced a notion of \emph{pseudoinstruction}.
    207 That is, instead of requiring that the compiler select the most appropriate jump instruction, for instance, we introduce a single pseudoinstruction \texttt{Jump}.
    208 Similarly, we introduce pseudoinstructions for generic calls,
     200As part of the CerCo project, a prototype compiler was being developed in parallel with the emulator.
     201Easing the design of the compiler was a key objective in implementing the emulator.
     202For this reason, we introduced notion of \emph{pseudoinstruction} and \emph{label}.
     203
     204The MCS-51's instruction set has numerous instructions for unconditional and conditional jumps to memory locations, calling procedures and moving data between memory spaces.
     205For instance, the instructions \texttt{AJMP}, \texttt{JMP} and \texttt{LJMP} all perform unconditional jumps.
     206However, these instructions differ in how large the maximum size of the offset of the jump to be performed can be.
     207Further, all jump instructions require a concrete memory address, to jump to, to be specified.
     208Requiring the compiler to compute these offsets, and select appropriate jump instructions, was seen as needleslly burdensome.
     209
     210Instead, we introduced generic \texttt{Jump}, \texttt{Call} and \texttt{Move} instructions.
     211These are expanded into MCS-51 assembly instructions with an assembly phase, prior to program execution.
     212Further, we introduced a notion of label (represented by strings), and introduced pseudoinstructions that allow conditional jumps to jump to labels.
     213These are also removed during the assembly phase, and replaced by concrete memory addresses and offsets.
    209214
    210215%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     
    213218\subsection{Putting dependent types to work}
    214219\label{subsect.putting.dependent.types.to.work}
     220
     221A peculiarity of the MCS-51 is the non-orthogonality of its instruction set.
     222For instance, the \texttt{MOV} instruction, can be invoked using one of sixteen combinations of addressing modes.
     223
     224Such non-orthogonality in the instruction set was handled with the use of polymorphic variants in the O'Caml emulator.
     225For instance, we introduced types corresponding to each addressing mode:
     226\begin{quote}
     227\begin{lstlisting}
     228type direct = [ `DIRECT of byte ]
     229type indirect = [ `INDIRECT of bit ]
     230...
     231\end{lstlisting}
     232\end{quote}
     233Which were then used in our inductive datatype for assembly instructions, as follows:
     234\begin{quote}
     235\begin{lstlisting}
     236type 'addr preinstruction =
     237 [ `ADD of acc * [ reg | direct | indirect | data ]
     238...
     239 | `MOV of
     240    (acc * [ reg | direct | indirect | data ],
     241     [ reg | indirect ] * [ acc | direct | data ],
     242     direct * [ acc | reg | direct | indirect | data ],
     243     dptr * data16,
     244     carry * bit,
     245     bit * carry
     246     ) union6
     247...
     248\end{lstlisting}
     249\end{quote}
     250Here, \texttt{union6} is a disjoint union type, defined as follows:
     251\begin{quote}
     252\begin{lstlisting}
     253type ('a,'b,'c,'d,'e,'f) union6 = [ `U1 of 'a | ... | `U6 of 'f ]
     254\end{lstlisting}
     255\end{quote}
     256For our purposes, the types \texttt{union2} and \texttt{union3} were also necessary.
     257
     258This polymorphic variant machinery worked well: it allowed us to pattern match
    215259
    216260We provide an inductive data type representing all possible addressing modes of 8051 assembly.
Note: See TracChangeset for help on using the changeset viewer.