Changeset 383


Ignore:
Timestamp:
Dec 7, 2010, 4:12:16 PM (9 years ago)
Author:
mulligan
Message:

First draft of report finished.

Location:
Deliverables/D4.1/Report
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Report/iramlayout.svg

    r382 r383  
    1515   version="1.1"
    1616   inkscape:version="0.48.0 r9654"
    17    sodipodi:docname="New document 15">
     17   sodipodi:docname="iramlayout.svg">
    1818  <defs
    1919     id="defs3339" />
     
    5959       x="99.125"
    6060       y="39.75"
    61        rx="0.875" />
     61       rx="0.875"
     62       inkscape:export-filename="/home/dpm/Projects/Cerco/Deliverables/D4.1/Report/iramlayout.png"
     63       inkscape:export-xdpi="79.209999"
     64       inkscape:export-ydpi="79.209999" />
    6265    <rect
    6366       style="fill:#ffffff;stroke:#000000;stroke-width:3.75;stroke-linecap:round;stroke-linejoin:round;stroke-miterlimit:4;stroke-opacity:1;stroke-dasharray:none"
     
    6770       x="99.375"
    6871       y="72.25"
    69        rx="0.875" />
     72       rx="0.875"
     73       inkscape:export-filename="/home/dpm/Projects/Cerco/Deliverables/D4.1/Report/iramlayout.png"
     74       inkscape:export-xdpi="79.209999"
     75       inkscape:export-ydpi="79.209999" />
    7076    <rect
    7177       style="fill:#ffffff;stroke:#000000;stroke-width:2.875;stroke-linecap:round;stroke-linejoin:round;stroke-miterlimit:4;stroke-opacity:1;stroke-dasharray:none"
     
    7581       x="99.375"
    7682       y="104.75"
    77        rx="0.875" />
     83       rx="0.875"
     84       inkscape:export-filename="/home/dpm/Projects/Cerco/Deliverables/D4.1/Report/iramlayout.png"
     85       inkscape:export-xdpi="79.209999"
     86       inkscape:export-ydpi="79.209999" />
    7887    <rect
    7988       style="fill:#ffffff;stroke:#000000;stroke-width:3.75;stroke-linecap:round;stroke-linejoin:round;stroke-miterlimit:4;stroke-opacity:1;stroke-dasharray:none"
     
    8392       x="99.375"
    8493       y="134.75"
    85        rx="0.875" />
     94       rx="0.875"
     95       inkscape:export-filename="/home/dpm/Projects/Cerco/Deliverables/D4.1/Report/iramlayout.png"
     96       inkscape:export-xdpi="79.209999"
     97       inkscape:export-ydpi="79.209999" />
    8698    <rect
    8799       style="fill:#e6e6e6;stroke:#000000;stroke-width:3.75;stroke-linecap:round;stroke-linejoin:round;stroke-miterlimit:4;stroke-opacity:1;stroke-dasharray:none"
     
    91103       x="99.375"
    92104       y="166"
    93        rx="0.875" />
     105       rx="0.875"
     106       inkscape:export-filename="/home/dpm/Projects/Cerco/Deliverables/D4.1/Report/iramlayout.png"
     107       inkscape:export-xdpi="79.209999"
     108       inkscape:export-ydpi="79.209999" />
    94109    <rect
    95110       style="fill:#e6e6e6;stroke:#000000;stroke-width:2.875;stroke-linecap:round;stroke-linejoin:round;stroke-miterlimit:4;stroke-opacity:1;stroke-dasharray:none"
     
    99114       x="99.375"
    100115       y="196"
    101        rx="0.875" />
     116       rx="0.875"
     117       inkscape:export-filename="/home/dpm/Projects/Cerco/Deliverables/D4.1/Report/iramlayout.png"
     118       inkscape:export-xdpi="79.209999"
     119       inkscape:export-ydpi="79.209999" />
    102120    <rect
    103121       style="fill:#808080;stroke:#000000;stroke-width:3.55477333;stroke-linecap:round;stroke-linejoin:round;stroke-miterlimit:4;stroke-opacity:1;stroke-dasharray:none"
     
    107125       x="99.375"
    108126       y="227.25"
    109        rx="0.875" />
     127       rx="0.875"
     128       inkscape:export-filename="/home/dpm/Projects/Cerco/Deliverables/D4.1/Report/iramlayout.png"
     129       inkscape:export-xdpi="79.209999"
     130       inkscape:export-ydpi="79.209999" />
    110131    <rect
    111132       style="fill:#333333;stroke:#000000;stroke-width:3.31642604;stroke-linecap:round;stroke-linejoin:round;stroke-miterlimit:4;stroke-opacity:1;stroke-dasharray:none"
     
    115136       x="99.375"
    116137       y="332.92642"
    117        rx="0.875" />
     138       rx="0.875"
     139       inkscape:export-filename="/home/dpm/Projects/Cerco/Deliverables/D4.1/Report/iramlayout.png"
     140       inkscape:export-xdpi="79.209999"
     141       inkscape:export-ydpi="79.209999" />
    118142    <text
    119143       xml:space="preserve"
     
    122146       y="59.582031"
    123147       id="text4209-3"
    124        sodipodi:linespacing="125%"><tspan
     148       sodipodi:linespacing="125%"
     149       inkscape:export-filename="/home/dpm/Projects/Cerco/Deliverables/D4.1/Report/iramlayout.png"
     150       inkscape:export-xdpi="79.209999"
     151       inkscape:export-ydpi="79.209999"><tspan
    125152         sodipodi:role="line"
    126153         id="tspan4211-0"
     
    134161       y="93.050781"
    135162       id="text4209-3-2"
    136        sodipodi:linespacing="125%"><tspan
     163       sodipodi:linespacing="125%"
     164       inkscape:export-filename="/home/dpm/Projects/Cerco/Deliverables/D4.1/Report/iramlayout.png"
     165       inkscape:export-xdpi="79.209999"
     166       inkscape:export-ydpi="79.209999"><tspan
    137167         sodipodi:role="line"
    138168         id="tspan4211-0-3"
     
    146176       y="124.30078"
    147177       id="text4209-3-5"
    148        sodipodi:linespacing="125%"><tspan
     178       sodipodi:linespacing="125%"
     179       inkscape:export-filename="/home/dpm/Projects/Cerco/Deliverables/D4.1/Report/iramlayout.png"
     180       inkscape:export-xdpi="79.209999"
     181       inkscape:export-ydpi="79.209999"><tspan
    149182         sodipodi:role="line"
    150183         id="tspan4211-0-4"
     
    158191       y="155.55078"
    159192       id="text4209-3-9"
    160        sodipodi:linespacing="125%"><tspan
     193       sodipodi:linespacing="125%"
     194       inkscape:export-filename="/home/dpm/Projects/Cerco/Deliverables/D4.1/Report/iramlayout.png"
     195       inkscape:export-xdpi="79.209999"
     196       inkscape:export-ydpi="79.209999"><tspan
    161197         sodipodi:role="line"
    162198         id="tspan4211-0-6"
     
    170206       y="185.55078"
    171207       id="text4209-3-7"
    172        sodipodi:linespacing="125%"><tspan
     208       sodipodi:linespacing="125%"
     209       inkscape:export-filename="/home/dpm/Projects/Cerco/Deliverables/D4.1/Report/iramlayout.png"
     210       inkscape:export-xdpi="79.209999"
     211       inkscape:export-ydpi="79.209999"><tspan
    173212         sodipodi:role="line"
    174213         id="tspan4211-0-47"
     
    182221       y="216.80078"
    183222       id="text4209-3-7-0"
    184        sodipodi:linespacing="125%"><tspan
     223       sodipodi:linespacing="125%"
     224       inkscape:export-filename="/home/dpm/Projects/Cerco/Deliverables/D4.1/Report/iramlayout.png"
     225       inkscape:export-xdpi="79.209999"
     226       inkscape:export-ydpi="79.209999"><tspan
    185227         sodipodi:role="line"
    186228         id="tspan4211-0-47-4"
     
    194236       y="263.05078"
    195237       id="text4209-3-7-7"
    196        sodipodi:linespacing="125%"><tspan
     238       sodipodi:linespacing="125%"
     239       inkscape:export-filename="/home/dpm/Projects/Cerco/Deliverables/D4.1/Report/iramlayout.png"
     240       inkscape:export-xdpi="79.209999"
     241       inkscape:export-ydpi="79.209999"><tspan
    197242         sodipodi:role="line"
    198243         id="tspan4211-0-47-0"
     
    211256       y="360.66406"
    212257       id="text4209-3-7-7-7"
    213        sodipodi:linespacing="125%"><tspan
     258       sodipodi:linespacing="125%"
     259       inkscape:export-filename="/home/dpm/Projects/Cerco/Deliverables/D4.1/Report/iramlayout.png"
     260       inkscape:export-xdpi="79.209999"
     261       inkscape:export-ydpi="79.209999"><tspan
    214262         sodipodi:role="line"
    215263         x="255.28711"
     
    228276       y="49.75"
    229277       id="text4209-0"
    230        sodipodi:linespacing="125%"><tspan
     278       sodipodi:linespacing="125%"
     279       inkscape:export-filename="/home/dpm/Projects/Cerco/Deliverables/D4.1/Report/iramlayout.png"
     280       inkscape:export-xdpi="79.209999"
     281       inkscape:export-ydpi="79.209999"><tspan
    231282         sodipodi:role="line"
    232283         x="67.832031"
     
    240291       y="82.25"
    241292       id="text4209-9"
    242        sodipodi:linespacing="125%"><tspan
     293       sodipodi:linespacing="125%"
     294       inkscape:export-filename="/home/dpm/Projects/Cerco/Deliverables/D4.1/Report/iramlayout.png"
     295       inkscape:export-xdpi="79.209999"
     296       inkscape:export-ydpi="79.209999"><tspan
    243297         sodipodi:role="line"
    244298         x="67.886719"
     
    252306       y="115.1875"
    253307       id="text4209-32"
    254        sodipodi:linespacing="125%"><tspan
     308       sodipodi:linespacing="125%"
     309       inkscape:export-filename="/home/dpm/Projects/Cerco/Deliverables/D4.1/Report/iramlayout.png"
     310       inkscape:export-xdpi="79.209999"
     311       inkscape:export-ydpi="79.209999"><tspan
    255312         sodipodi:role="line"
    256313         x="67.832031"
     
    269326       y="144.75"
    270327       id="text4209"
    271        sodipodi:linespacing="125%"><tspan
     328       sodipodi:linespacing="125%"
     329       inkscape:export-filename="/home/dpm/Projects/Cerco/Deliverables/D4.1/Report/iramlayout.png"
     330       inkscape:export-xdpi="79.209999"
     331       inkscape:export-ydpi="79.209999"><tspan
    272332         sodipodi:role="line"
    273333         x="67.886719"
     
    286346       y="176"
    287347       id="text4209-05"
    288        sodipodi:linespacing="125%"><tspan
     348       sodipodi:linespacing="125%"
     349       inkscape:export-filename="/home/dpm/Projects/Cerco/Deliverables/D4.1/Report/iramlayout.png"
     350       inkscape:export-xdpi="79.209999"
     351       inkscape:export-ydpi="79.209999"><tspan
    289352         sodipodi:role="line"
    290353         x="67.832031"
     
    303366       y="206.4375"
    304367       id="text4209-4"
    305        sodipodi:linespacing="125%"><tspan
     368       sodipodi:linespacing="125%"
     369       inkscape:export-filename="/home/dpm/Projects/Cerco/Deliverables/D4.1/Report/iramlayout.png"
     370       inkscape:export-xdpi="79.209999"
     371       inkscape:export-ydpi="79.209999"><tspan
    306372         sodipodi:role="line"
    307373         x="67.886719"
     
    329395       y="237.34761"
    330396       id="text4209-1"
    331        sodipodi:linespacing="125%"><tspan
     397       sodipodi:linespacing="125%"
     398       inkscape:export-filename="/home/dpm/Projects/Cerco/Deliverables/D4.1/Report/iramlayout.png"
     399       inkscape:export-xdpi="79.209999"
     400       inkscape:export-ydpi="79.209999"><tspan
    332401         sodipodi:role="line"
    333402         x="67.832031"
     
    346415       y="317.07422"
    347416       id="text4209-13"
    348        sodipodi:linespacing="125%"><tspan
     417       sodipodi:linespacing="125%"
     418       inkscape:export-filename="/home/dpm/Projects/Cerco/Deliverables/D4.1/Report/iramlayout.png"
     419       inkscape:export-xdpi="79.209999"
     420       inkscape:export-ydpi="79.209999"><tspan
    349421         sodipodi:role="line"
    350422         x="67.574219"
     
    363435       y="343.14322"
    364436       id="text4209-10"
    365        sodipodi:linespacing="125%"><tspan
     437       sodipodi:linespacing="125%"
     438       inkscape:export-filename="/home/dpm/Projects/Cerco/Deliverables/D4.1/Report/iramlayout.png"
     439       inkscape:export-xdpi="79.209999"
     440       inkscape:export-ydpi="79.209999"><tspan
    366441         sodipodi:role="line"
    367442         x="67.832031"
     
    381456       id="text4209-35"
    382457       sodipodi:linespacing="125%"
    383        transform="matrix(0,1,-1,0,0,0)"><tspan
     458       transform="matrix(0,1,-1,0,0,0)"
     459       inkscape:export-filename="/home/dpm/Projects/Cerco/Deliverables/D4.1/Report/iramlayout.png"
     460       inkscape:export-xdpi="79.209999"
     461       inkscape:export-ydpi="79.209999"><tspan
    384462         sodipodi:role="line"
    385463         x="264.55859"
     
    399477       id="text4209-35-4"
    400478       sodipodi:linespacing="125%"
    401        transform="matrix(0,1,-1,0,0,0)"><tspan
     479       transform="matrix(0,1,-1,0,0,0)"
     480       inkscape:export-filename="/home/dpm/Projects/Cerco/Deliverables/D4.1/Report/iramlayout.png"
     481       inkscape:export-xdpi="79.209999"
     482       inkscape:export-ydpi="79.209999"><tspan
    402483         sodipodi:role="line"
    403484         x="367.49609"
  • Deliverables/D4.1/Report/report.tex

    r382 r383  
    1919\vspace*{1cm}Project FP7-ICT-2009-C-243881 \cerco{}}
    2020
    21 \lstdefinelanguage{matita}
     21\lstdefinelanguage{matita-ocaml}
    2222  {keywords={ndefinition,ncoercion,nlemma,ntheorem,nremark,ninductive,nrecord,nqed,nlet,let,in,rec,match,return,with,Type},
    2323   morekeywords={[2]nwhd,nnormalize,nelim,ncases,ndestruct},
     24   morekeywords={[3]type,of},
    2425   mathescape=true,
    2526  }
    2627
    27 \lstset{language=matita,basicstyle=\small\tt,columns=flexible,breaklines=false,
     28\lstset{language=matita-ocaml,basicstyle=\small\tt,columns=flexible,breaklines=false,
    2829        keywordstyle=\color{red}\bfseries,
    2930        keywordstyle=[2]\color{blue},
     31        keywordstyle=[3]\color{blue}\bfseries,
    3032        commentstyle=\color{green},
    3133        stringstyle=\color{blue},
     
    9496\vspace*{7cm}
    9597\paragraph{Abstract}
    96 We discuss the design and implementation of an O'Caml emulator for the Intel 8051/8052 eight bit processor, and its subsequent formalisation in the dependently typed proof assistant Matita.
    97 
     98We discuss the implementation of a prototype O'Caml emulator for the Intel 8051/8052 eight bit processor, and its subsequent formalisation in the dependently typed proof assistant Matita.
     99In particular, we focus on the decisions made during the design of both emulators, and how the design of the O'Caml emulator had to be modified in order to fit into the more stringent type system of Matita.
     100
     101We also briefly summarise the Intel 8051/8052 processor architecture, our target processor model for the \textsf{CerCo} project.
    98102\newpage
    99103
     
    102106\newpage
    103107
    104 \section{Introduction}
    105 \label{sect.introduction}
    106 
    107 \subsection{Task}
    108 \label{subsect.task}
     108\section{Task}
     109\label{sect.task}
    109110
    110111The Grant Agreement states the D4.1/D4.2 deliverables consist of the following tasks:
     
    122123We now report on our implementation of these deliverables.
    123124
    124 \subsection{A brief overview of the target processor}
    125 \label{subsect.brief.overview.target.processor}
     125\section{A brief overview of the target processor}
     126\label{sect.brief.overview.target.processor}
    126127
    127128The MCS-51 is an eight bit microprocessor introduced by Intel in the late 1970s.
     
    191192\label{sect.emulator.in.ocaml}
    192193
    193 \subsection{Anatomy of the emulator}
    194 \label{subsect.anatomy.emulator}
     194We discuss decisions made during the design of the prototype O'Caml emulator.
    195195
    196196\subsection{Lack of orthogonality in instruction set}
     
    200200For instance, consider the MOV instruction, which implements a data transfer between two memory locations, which takes eighteen possible combinations of addressing modes.
    201201
    202 \subsection{Pseudo-instructions}
    203 \label{subsect.pseudo-instructions}
     202We handle this problem by introducing `unions' of types, using O'Caml's polymorphic variants feature:
     203\begin{quote}
     204\begin{lstlisting}
     205type ('a, 'b) union2 = [ `U1 of 'a | `U2 of 'b ]
     206\end{lstlisting}
     207\end{quote}
     208(We also introduce \texttt{union3} and \texttt{union6}, which suffice for our purposes.)
     209
     210Using these union types, we can rationalise the inductive type encoding the assembly instruction set.
     211For instance:
     212\begin{quote}
     213\begin{lstlisting}
     214type 'addr preinstruction =
     215...
     216  | `XRL of (acc * [ data | reg | direct | indirect ],
     217             direct * [ acc | data ]) union2
     218...
     219\end{lstlisting}
     220\end{quote}
     221That is, the \texttt{XRL} instruction\footnote{Exclusive disjunction.} take either the accumulator A as its first argument, followed by data with one of data, register, direct or indirect addressing modes, or takes data with a direct addressing mode as its first argument, with either the accumulator A or data with the data addressing mode as its second argument.
     222
     223Further, all functions that must pattern match against the \texttt{(pre)instruction} inductive type are also simplified using this technique.
     224Using O'Caml's ability to perform `deep pattern' matches, we may pattern match against \texttt{`XRL(`U1(arg1, arg2))} and have the guarantee that \texttt{arg1} takes the form \texttt{`ACC\_A}.
     225
     226\subsection{Pseudo-instructions and labels}
     227\label{subsect.pseudo-instructions.labels}
     228
     229Per the description of Deliverable D4.1 in the Grant Agreement above, the 8051 emulator must eventually interface with the C compiler frontend of Deliverable D3.2, produced in Paris.
     230After consultation, it was found that the design of the compiler frontend could be simplified considerably with the introduction of \emph{pseudoinstructions} and labels.
     231
     232We introduce three new pseudoinstructions---\texttt{Jump}, \texttt{Call}, and \texttt{Mov}---corresponding to unconditional jumps, procedure calls and data transfers respectively.
     233We also `promote' all unlabeled conditional jumps in 8051 assembly to labeled pseudojumps; one can now jump to a label conditionally, as opposed to jumping to a fixed relative offset.
     234Further, we introduce labels for jumping to, and cost annotations, used by the Paris team.
     235
     236The three new pseudoinstructions, along with the promoted conditional jumps, allow the Paris team to abstract away from the differences between different types of unconditional jump (the 8051 has three different sorts, depending on the length of the jump), as well as abstract away the differences between memory transfers and calls.
     237However, the emulator must perform an expansion stage, during which pseudoinstructions are translated to `real' 8051 assembly instructions.
     238
     239The introduction of labeled conditional jumps slightly complicates our type of abstract syntax for 8051 assembly.
     240We define an inductive type representing conditional jumps in 8051 assembly code, parameterised by a type representing relative offsets:s
     241\begin{quote}
     242\begin{lstlisting}
     243type 'addr jump =
     244  [ `JC of 'addr
     245  | `JNC of 'addr
     246...
     247\end{lstlisting}
     248\end{quote}
     249An inductive type of preinstructions is defined, which is also parameterised by a type representing relative offsets in assembly code, and incorporates the inductive type of conditional jumps:
     250\begin{quote}
     251\begin{lstlisting}
     252type 'addr preinstruction =
     253  [ `ADD of acc * [ reg | direct | indirect | data ]
     254...
     255  | 'addr jump
     256...
     257\end{lstlisting}
     258\end{quote}
     259A type representing instructions is defined, choosing a concrete type for relative offsets:
     260\begin{quote}
     261\begin{lstlisting}
     262type instruction = rel preinstruction
     263\end{lstlisting}
     264\end{quote}
     265Here, \texttt{rel} is a type which `wraps up' a byte.
     266Finally, this type of instructions is incorporated into a type of labelled instructions:
     267\begin{quote}
     268\begin{lstlisting}
     269type labelled_instruction =
     270  [ instruction
     271  | `Cost of string
     272  | `Label of string
     273  | `Jmp of string
     274  | `Call of string
     275  | `Mov of dptr * string
     276  | `WithLabel of [`Label of string] jump
     277]
     278\end{lstlisting}
     279\end{quote}
     280Throughout, we make heavy use of polymorphic variants to deal with issues relating to subtyping.
     281
     282As mentioned, the emulator must now handle an additional expansion stage, removing pseudoinstructions in favour of real, 8051 assembly instructions.
     283This is relatively straightforward, and is done in two stages.
     284
     285The first stage consists of iterating over an assembly program, building a dictionary of all labels and their position in the program.
     286The second stage consists of iterating over the same program and replacing all pseudojumps (both conditional and unconditional) with an 8051 jump to the requisite computed offset.
     287One subtletly persists, however.
     288
     289The 8051 has three different types of unconditional jump, depending on the length of the jump to be used: \texttt{AJMP}, \texttt{JMP} and \texttt{LJMP}.
     290The instructions \texttt{AJMP} and \texttt{JMP} are short jumps, whereas \texttt{LJMP} is a long jump, capable of reaching anywhere in the program.
     291At the moment, the second pass of the expansion stage replaces all unconditional pseudojumps with a \texttt{LJMP} for simplicity.
     292We do, however, plan to improve this process for efficiency reasons, expanding to shorter jumps where feasible.
     293
     294\subsection{Validation}
     295\label{subsect.validation}
    204296
    205297In validating the design and implementation of the O'Caml emulator we used two tactics:
     
    211303Use of reference compilers and emulators.
    212304The operation of the emulator was manually tested by reference to \textsc{mcu 8051 ide}, an emulator for the 8051 series processor.
    213 A number of small C programs were compiled in SDCC\footnote{See the \texttt{GCC} directory for a selection of them.}, and the resulting IHX files were disassembled by \textsc{mcu 8051 ide}.
     305A number of small C programs were compiled in SDCC\footnote{See the \texttt{GCC} directory for a selection of them.}.
     306The resulting IHX files were disassembled by \textsc{mcu 8051 ide}.
     307(IHX files are a standard format for transferring compiled assembly code onto an 8051 series processor, produced by SDCC and all other compilers that target that 8051.)
    214308The status changes in both emulators were then compared.
    215309
     
    219313As a further check, the design and operation of the emulator was compared with the textual description of online tutorials on 8051 programming, such as those found at \url{http://www.8052.com}.
    220314
    221 \subsection{Validation}
    222 \label{subsect.validation}
    223 
    224315\section{The emulator in Matita}
    225316\label{sect.emulator.in.matita}
     317
     318The O'Caml emulator served as a testbed and prototype for an emulator written in the internal language of the Matita proof assistant.
     319We describe our work porting the emulator to Matita, especially where the design of the Matita emulator differs from that of the O'Caml version.
    226320
    227321\subsection{What we do not implement}
Note: See TracChangeset for help on using the changeset viewer.