source: Deliverables/D4.1/Report/report.tex @ 438

Last change on this file since 438 was 438, checked in by sacerdot, 9 years ago

Final version.

File size: 42.4 KB
Line 
1\documentclass[11pt, epsf, a4wide]{article}
2
3\usepackage{../../style/cerco}
4
5\usepackage{amsfonts}
6\usepackage{amsmath}
7\usepackage{amssymb} 
8\usepackage[english]{babel}
9\usepackage{graphicx}
10\usepackage[utf8x]{inputenc}
11\usepackage{listings}
12\usepackage{stmaryrd}
13\usepackage{url}
14
15\title{
16INFORMATION AND COMMUNICATION TECHNOLOGIES\\
17(ICT)\\
18PROGRAMME\\
19\vspace*{1cm}Project FP7-ICT-2009-C-243881 \cerco{}}
20
21\lstdefinelanguage{matita-ocaml}
22  {keywords={ndefinition,ncoercion,nlemma,ntheorem,nremark,ninductive,nrecord,nqed,nlet,let,in,rec,match,return,with,Type,try},
23   morekeywords={[2]nwhd,nnormalize,nelim,ncases,ndestruct},
24   morekeywords={[3]type,of},
25   mathescape=true,
26  }
27
28\lstset{language=matita-ocaml,basicstyle=\small\tt,columns=flexible,breaklines=false,
29        keywordstyle=\color{red}\bfseries,
30        keywordstyle=[2]\color{blue},
31        keywordstyle=[3]\color{blue}\bfseries,
32        commentstyle=\color{green},
33        stringstyle=\color{blue},
34        showspaces=false,showstringspaces=false}
35
36\lstset{extendedchars=false}
37\lstset{inputencoding=utf8x}
38\DeclareUnicodeCharacter{8797}{:=}
39\DeclareUnicodeCharacter{10746}{++}
40\DeclareUnicodeCharacter{9001}{\ensuremath{\langle}}
41\DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}}
42
43\date{}
44\author{}
45
46\begin{document}
47
48\thispagestyle{empty}
49
50\vspace*{-1cm}
51\begin{center}
52\includegraphics[width=0.6\textwidth]{../../style/cerco_logo.png}
53\end{center}
54
55\begin{minipage}{\textwidth}
56\maketitle
57\end{minipage}
58
59\vspace*{0.5cm}
60\begin{center}
61\begin{LARGE}
62\textbf{
63Report n. D4.1\\
64Executable Formal Semantics\\of Machine Code}
65\end{LARGE} 
66\end{center}
67
68\vspace*{2cm}
69\begin{center}
70\begin{large}
71Version 1.0
72\end{large}
73\end{center}
74
75\vspace*{0.5cm}
76\begin{center}
77\begin{large}
78Main Authors:\\
79Dominic P. Mulligan and Claudio Sacerdoti Coen
80\end{large}
81\end{center}
82
83\vspace*{\fill}
84
85\noindent
86Project Acronym: \cerco{}\\
87Project full title: Certified Complexity\\
88Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\
89
90\clearpage
91\pagestyle{myheadings}
92\markright{\cerco{}, FP7-ICT-2009-C-243881}
93
94\newpage
95
96\vspace*{7cm}
97\paragraph{Abstract}
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
101Both emulators provide an `executable formal semantics of machine code' for our target processor, per the description of the Deliverable in the \textsf{CerCo} Grant Agreement.
102\newpage
103
104\tableofcontents
105
106\newpage
107
108\section{Task}
109\label{sect.task}
110
111The Grant Agreement states that Task T4.1, entitled `Executable Formal Semantics of Machine Code' has associated deliverable D4.1 consisting of the following:
112\begin{quotation}
113\textbf{Executable Formal Semantics of Machine Code}: Formal definition of the semantics of the target language.
114The semantics will be given in a functional (and hence executable) form, useful for testing, validation and project assessment.
115\end{quotation}
116This report details our implementation of this deliverable.
117
118\subsection{Connection with other deliverables}
119\label{subsect.connection.other.deliverables}
120
121Deliverable D4.1 is an executable formal semantics of the machine code of our target processor (a brief overview of the processor architecture is provided in Section~\ref{sect.brief.overview.target.processor}).
122We provide an executable semantics in both O'Caml and the internal language of the Matita proof assistant.
123
124The C compiler delivered by Work Package 3 will eventually produce machine code executable by our emulator, and we expect that the emulator will be useful as a debugging aid for the compiler writers.
125Further, additional deliverables listed under Work Package 4 will later make use of the work reported in this document.
126Deliverables D4.2 and D4.3 entail the implementation of a formalised version of the intermediate language of the compiler, along with an executable formal semantics of these languages.
127In particular, Deliverable D4.3 requires a formalisation of the semantics of the intermediate languages of the compiler, and Deliverable D4.4 requires a formal proof of the correspondence between the semantics of these formalized languages, and the formal semantics of the target processor.
128The emulator(s) discussed in this report are the formalized semantics of our target processor made manifest.
129
130\section{A brief overview of the target processor}
131\label{sect.brief.overview.target.processor}
132
133The MCS-51 is an eight bit microprocessor introduced by Intel in the late 1970s.
134Commonly called the 8051, in the three decades since its introduction the processor has become a highly popular target for embedded systems engineers.
135Further, the processor and its immediate successor, the 8052, is still manufactured by a host of semiconductor suppliers---many of them European---including Atmel, Siemens Semiconductor, NXP (formerly Phillips Semiconductor), Texas Instruments, and Maxim (formerly Dallas Semiconductor).
136
137The 8051 is a well documented processor, and has the additional support of numerous open source and commercial tools, such as compilers for high-level languages and emulators.
138For instance, the open source Small Device C Compiler (SDCC) recognises a dialect of C, and other compilers targeting the 8051 for BASIC, Forth and Modula-2 are also extant.
139An open source emulator for the processor, MCU8051 IDE, is also available.
140
141\begin{figure}[t]
142\begin{center}
143\includegraphics[scale=0.5]{memorylayout.png}
144\end{center}
145\caption{High level overview of the 8051 memory layout}
146\label{fig.memory.layout}
147\end{figure}
148
149The 8051 has a relatively straightforward architecture, unencumbered by advanced features of modern processors, making it an ideal target for formalisation.
150A high-level overview of the processor's memory layout is provided in Figure~\ref{fig.memory.layout}.
151
152Processor RAM is divided into numerous segments, with the most prominent division being between internal and (optional) external memory.
153Internal memory, commonly provided on the die itself with fast access, is further divided into 128 bytes of internal RAM and numerous Special Function Registers (SFRs) which control the operation of the processor.
154Internal RAM (IRAM) is further divided into a eight general purpose bit-addressable registers (R0--R7).
155These sit in the first eight bytes of IRAM, though can be programmatically `shifted up' as needed.
156Bit memory, followed by a small amount of stack space resides in the memory space immediately after the register banks.
157What remains of the IRAM may be treated as general purpose memory.
158A schematic view of IRAM layout is provided in Figure~\ref{fig.iram.layout}.
159
160External RAM (XRAM), limited to 64 kilobytes, is optional, and may be provided on or off chip, depending on the manufacturer.
161XRAM is accessed using a dedicated instruction.
162External code memory (XCODE) is often stored in the form of an EPROM, and limited to 64 kilobytes in size.
163However, depending on the particular manufacturer and processor model, a dedicated on-die read-only memory area for program code (ICODE) may also be supplied.
164
165Memory may be addressed in numerous ways: immediate, direct, indirect, external direct and code indirect.
166As the latter two addressing modes hint, there are some restrictions enforced by the 8051 and its derivatives on which addressing modes may be used with specific types of memory.
167For instance, the 128 bytes of extra internal RAM that the 8052 features cannot be addressed using indirect addressing; rather, external (in)direct addressing must be used.
168
169The 8051 series possesses an eight bit Arithmetic and Logic Unit (ALU), with a wide variety of instructions for performing arithmetic and logical operations on bits and integers.
170Further, the processor possesses two eight bit general purpose accumulators, A and B.
171
172Communication with the device is facilitated by an onboard UART serial port, and associated serial controller, which can operate in numerous modes.
173Serial baud rate is determined by one of two sixteen bit timers included with the 8051, which can be set to multiple modes of operation.
174(The 8052 provides an additional sixteen bit timer.)
175As an additional method of communication, the 8051 also provides a four byte bit-addressable input-output port.
176
177The programmer may take advantage of the interrupt mechanism that the processor provides.
178This is especially useful when dealing with input or output involving the serial device, as an interrupt can be set when a whole character is sent or received via the serial port.
179
180Interrupts immediately halt the flow of execution of the processor, and cause the program counter to jump to a fixed address, where the requisite interrupt handler is stored.
181However, interrupts may be set to one of two priorities: low and high.
182The interrupt handler of an interrupt with high priority is executed ahead of the interrupt handler of an interrupt of lower priority, interrupting a currently executing handler of lower priority, if necessary.
183
184The 8051 has interrupts disabled by default.
185The programmer is free to handle serial input and output manually, by poking serial flags in the SFRs.
186Similarly, `exceptional circumstances' that would otherwise trigger an interrupt on more modern processors, for example, division by zero, are also signalled by setting flags.
187
188\begin{figure}[t]
189\begin{center}
190\includegraphics[scale=0.5]{iramlayout.png}
191\end{center}
192\caption{Schematic view of 8051 IRAM layout}
193\label{fig.iram.layout}
194\end{figure}
195
196\section{The emulator in O'Caml}
197\label{sect.emulator.in.ocaml}
198
199We discuss decisions made during the design of the prototype O'Caml emulator.
200
201\subsection{Lack of orthogonality in instruction set}
202\label{subsect.lack.orthogonality.instruction.set}
203
204The instruction set of 8051 assembly is highly irregular.
205For instance, consider the MOV instruction, which implements a data transfer between two memory locations, which takes eighteen possible combinations of addressing modes.
206
207We handle this problem by introducing `unions' of types, using O'Caml's polymorphic variants feature:
208\begin{quote}
209\begin{lstlisting}
210type ('a, 'b) union2 = [ `U1 of 'a | `U2 of 'b ]
211\end{lstlisting}
212\end{quote}
213(We also introduce \texttt{union3} and \texttt{union6}, which suffice for our purposes.)
214
215Using these union types, we can rationalise the inductive type encoding the assembly instruction set.
216For instance:
217\begin{quote}
218\begin{lstlisting}
219type 'addr preinstruction =
220...
221  | `XRL of (acc * [ data | reg | direct | indirect ],
222             direct * [ acc | data ]) union2
223...
224\end{lstlisting}
225\end{quote}
226That 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.
227
228Further, all functions that must pattern match against the \texttt{(pre)instruction} inductive type are also simplified using this technique.
229Using 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}.
230
231\subsection{Pseudo-instructions and labels}
232\label{subsect.pseudo-instructions.labels}
233
234Per 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.
235After consultation, it was found that the design of the compiler frontend could be simplified considerably with the introduction of \emph{pseudoinstructions} and labels.
236
237We introduce three new pseudoinstructions---\texttt{Jump}, \texttt{Call}, and \texttt{Mov}---corresponding to unconditional jumps, procedure calls and data transfers respectively.
238We 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.
239Further, we introduce labels for jumping to, and cost annotations, used by the Paris team.
240
241The 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.
242However, the emulator must perform an expansion stage, during which pseudoinstructions are translated to `real' 8051 assembly instructions.
243
244The introduction of labeled conditional jumps slightly complicates our type of abstract syntax for 8051 assembly.
245We define an inductive type representing conditional jumps in 8051 assembly code, parameterised by a type representing relative offsets:s
246\begin{quote}
247\begin{lstlisting}
248type 'addr jump =
249  [ `JC of 'addr
250  | `JNC of 'addr
251...
252\end{lstlisting}
253\end{quote}
254An 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:
255\begin{quote}
256\begin{lstlisting}
257type 'addr preinstruction =
258  [ `ADD of acc * [ reg | direct | indirect | data ]
259...
260  | 'addr jump
261...
262\end{lstlisting}
263\end{quote}
264A type representing instructions is defined, choosing a concrete type for relative offsets:
265\begin{quote}
266\begin{lstlisting}
267type instruction = rel preinstruction
268\end{lstlisting}
269\end{quote}
270Here, \texttt{rel} is a type which `wraps up' a byte.
271Finally, this type of instructions is incorporated into a type of labelled instructions:
272\begin{quote}
273\begin{lstlisting}
274type labelled_instruction =
275  [ instruction
276  | `Cost of string
277  | `Label of string
278  | `Jmp of string
279  | `Call of string
280  | `Mov of dptr * string
281  | `WithLabel of [`Label of string] jump
282]
283\end{lstlisting}
284\end{quote}
285Throughout, we make heavy use of polymorphic variants to deal with issues relating to subtyping.
286
287As mentioned, the emulator must now handle an additional expansion stage, removing pseudoinstructions in favour of real, 8051 assembly instructions.
288This is relatively straightforward, and is done in two stages.
289
290The first stage consists of iterating over an assembly program, building a multiset of all labels and their position in the program.
291This multiset is stored, and can later be used by the callback function passed to \texttt{execute}, the function that executes an 8051 assembly program, in order to produce a trace of labels.
292The callback function, a function from the processor state to unit, passed to \texttt{execute} implements our `label collecting semantics'.
293In pseudocode:
294\begin{quote}
295\begin{lstlisting}
296let f status :=
297  try
298    let labels := lookup (program_counter status) (costs_map $\cup$ label_map) in
299      ()
300  with NotFound $\rightarrow$ ()
301\end{lstlisting}
302\end{quote}
303Where \texttt{labels} is initialized to $\texttt{ref empty}$.
304That is, the callback attempts to make note of all the label that program execution `passes through'.
305
306In Deliverable D4.4, we will prove that this labelled trace is preserved by the compilation process.
307
308The 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.
309One subtletly persists, however.
310
311The 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}.
312The instructions \texttt{AJMP} and \texttt{JMP} are short jumps, whereas \texttt{LJMP} is a long jump, capable of reaching anywhere in the program.
313At the moment, the second pass of the expansion stage replaces all unconditional pseudojumps with a \texttt{LJMP} for simplicity.
314We do, however, plan to improve this process for efficiency reasons, expanding to shorter jumps where feasible.
315
316\subsection{Anatomy of the emulator}
317\label{subsect.anatomy.emulator}
318
319\begin{figure}[t]
320\begin{quote}
321\begin{lstlisting}
322  let hex = IntelHex.intel_hex_of_file filename in
323  let mem = IntelHex.process_intel_hex hex in
324  let status = ASMInterpret.load_mem mem ASMInterpret.initialize in
325    ASMInterpret.execute callback status
326\end{lstlisting}
327\end{quote}
328\caption{Pseudocode of unlabelled program execution}
329\label{fig.unlabelled.execution}
330\end{figure}
331
332\begin{figure}[t]
333\begin{quote}
334\begin{lstlisting}
335  let mem, cost_map = ASMInterpret.assembly labelled_program in
336  let status = ASMInterpret.load_mem mem ASMInterpret.initialize in
337    ASMInterpret.execute callback status
338\end{lstlisting}
339\end{quote}
340\caption{Pseudocode of labelled program execution}
341\label{fig.labelled.execution}
342\end{figure}
343
344We provide a high-level overview of the operation of the emulator.
345Two modes of operation exist: execution of an unlabelled program -- like one obtained disassemblying an already assembled program --
346and execution of a labelled program.
347
348Unlabelled execution proceeds as follows (see Fig.~\ref{fig.unlabelled.execution}).
349Program code is loaded onto the 8051 in a standard format, the Intel Hex (IHX) format.
350All compilers/assemblers producing machine code for the 8051, including the SDCC compiler which we use for debugging purposes, produce compiled programs in IHX format as standard.
351Accordingly, our O'Caml emulator can parse IHX files using \texttt{intel\_hex\_of\_file} and populate the emulator's code memory with their contents using \texttt{process\_intel\_hex}. Code memory is loaded into the initial processor status using \texttt{load\_mem}.
352
353Once code memory is loaded into the status, the emulator calls \texttt{execute}, which performs the standard fetch-decode-execute cycle
354indefinitely. The callback function passed to \texttt{execute} is called at the beginning of each cycle and takes in input the processor
355status. It can be used for debugging purposes, for instance to compute execution traces.
356
357The callback function can even stop execution by raising the \texttt{Halt} exception.
358This is the only way to stop the emulator, since the 8051 processors have no instruction to stop execution and program ``termination'' is
359usually compiled to a tight diverging loop.
360
361Labelled execution is similar (see Fig.~\ref{fig.labelled.execution}).
362However, instead of a program being loaded from an Intel Hex file, we process a labelled program with \texttt{assembly}, in order to obtain an unlabelled program, complete with a map from code addresses to cost annotations. The map can be used by the \texttt{callback} function,
363passed to execute, in order to implement the `label collecting semantics' that the CerCo compiler will preserve.
364
365The (simplified) types of the functions mentioned in the pseudocode of Figures~\ref{fig.unlabelled.execution} and~\ref{fig.labelled.execution} are as follows:
366\small{
367\begin{center}
368\begin{tabular*}{0.95\textwidth}{p{3cm}p{12cm}}
369Title & Type \\
370\hline
371\texttt{intel\_hex\_of\_file} & \texttt{string -> intel\_hex\_entry list} \\
372\texttt{process\_intel\_hex} & \texttt{intel\_hex\_entry list -> byte map} \\
373\texttt{load\_mem} & \texttt{byte map -> status -> status} \\
374\texttt{initialize} & \texttt{status} \\
375\texttt{execute} & \texttt{(status -> unit) -> status -> status} \\
376\texttt{assembly} & \texttt{assembly\_program -> byte list * cost map} \\
377\texttt{callback} & \texttt{status -> unit}
378\end{tabular*}
379\end{center}}
380
381\subsection{Validation}
382\label{subsect.validation}
383
384In validating the design and implementation of the O'Caml emulator we used two tactics:
385\begin{enumerate}
386\item
387Use of multiple manufacturer's data sheets (both the Siemens Semiconductor and Phillips Semiconductor specifications for the 8051, as well as online sources such as the Keil website).
388We found typographic errors in manufacturer's data sheets which were resolved by consulting an alternative sheet.
389\item
390Use of reference compilers and emulators.
391The operation of the emulator was manually tested by reference to \textsc{mcu 8051 ide}, an emulator for the 8051 series processor.
392A number of small C programs were compiled in SDCC\footnote{See the \texttt{GCC} directory for a selection of them.}.
393The resulting IHX files were disassembled by \textsc{mcu 8051 ide}.
394(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.)
395The status changes in both emulators were then compared.
396
397For further validation, the output of the compiled C programs from SDCC was compared with the output of the same programs in GCC, in order to pre-empt the introduction of bugs in the emulator inherited from a faulty C compiler.
398\end{enumerate}
399
400As 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}.
401
402\section{The emulator in Matita}
403\label{sect.emulator.in.matita}
404
405The O'Caml emulator served as a testbed and prototype for an emulator written in the internal language of the Matita proof assistant.
406We describe our work porting the emulator to Matita, especially where the design of the Matita emulator differs from that of the O'Caml version.
407
408\subsection{What we do not implement}
409\label{subsect.what.we.do.not.implement}
410
411Our O'Caml 8051 emulator provides functions for reading and parsing Intel IHX format files.
412We do not implement these functions in the Matita emulator, as Matita provides no means of input or output.
413
414\subsection{Auxilliary data structures and libraries}
415\label{subsect.auxilliary.data.structures.and.libraries}
416
417A small library of data structures was written, along with basic functions operating over them.
418Implemented data structures include: Booleans, option types, lists, Cartesian products, Natural numbers, fixed-length vectors, and sparse tries.
419
420Our type of vectors, in particular, makes heavy use of dependent types.
421Probing vectors is `type safe' for instance: we cannot index into a vector beyond the vector's length.
422
423We represent bits as Boolean values.
424Nibbles, bytes, words, and so on, are represented as fixed length (bit)vectors of the requisite length.
425
426\subsection{The emulator state}
427\label{subsect.emulator.state}
428
429We represent all processor memory in the Matita emulator as a sparse (bitvector)trie:
430
431\begin{quote}
432\begin{lstlisting}
433ninductive BitVectorTrie (A: Type[0]): Nat $\rightarrow$ Type[0] ≝
434  Leaf: A $\rightarrow$ BitVectorTrie A Z
435| Node: ∀n: Nat. BitVectorTrie A n $\rightarrow$ BitVectorTrie A n $\rightarrow$ BitVectorTrie A (S n)
436| Stub: ∀n: Nat. BitVectorTrie A n.
437\end{lstlisting}
438\end{quote}
439
440Nodes are addressed by a bitvector index, representing a path through the tree.
441At any point in the tree, a \texttt{Stub} may be inserted, representing a `hole' in the tree.
442All functions operating on tries use dependent types to enforce the invariant that the height of the tree and the length of the bitvector representing a path through the tree are the same.
443
444We probe a trie with the \texttt{lookup} function.
445This takes an additional argument representing the value to be returned should a stub, representing uninitialised data, be encountered during traversal.
446
447Like the O'Caml emulator, we use a record to represent processor state:
448
449\begin{quote}
450\begin{lstlisting}
451nrecord Status: Type[0] ≝
452{
453  code_memory: BitVectorTrie Byte sixteen;
454  low_internal_ram: BitVectorTrie Byte seven;
455  high_internal_ram: BitVectorTrie Byte seven;
456  external_ram: BitVectorTrie Byte sixteen;
457 
458  program_counter: Word;
459 
460  special_function_registers_8051: Vector Byte nineteen;
461  special_function_registers_8052: Vector Byte five;
462 
463  ...
464}.
465\end{lstlisting}
466\end{quote}
467
468However, we `squash' the \texttt{Status} record in the Matita emulator by grouping all 8051 SFRs (respectively, 8052 SFRs) into a single vector of bytes, as opposed to representing them as explicit fields in the record itself.
469We then provide functions that index into the respective vector to `get' and `set' the respective SFRs.
470This is due to record typechecking in Matita being slow for large records.
471
472\subsection{Dealing with partiality}
473\label{subsect.dealing.with.partiality}
474
475The O'Caml 8051 emulator makes use of a number of partial functions.
476These functions either \texttt{assert false}\footnote{O'Caml idiom: immediately halts execution of the running program.} or do not perform a comprehensive pattern analysis over their inputs.
477There are a number of possible reasons for this:
478\begin{enumerate}
479\item
480\textbf{Incomplete pattern analyses} are used where we are confident that the particular pattern match in question should never occur, for instance if the calling function performs a test beforehand, or where the emulator should fail anyway if a particular unchecked pattern is used as input.
481An example of a function which exhibits the latter behaviour is \texttt{set\_arg\_16} from \texttt{ASMInterpret.ml}, which fails with a pattern match exception if called on an input representing an eight bit argument.
482\item
483\textbf{Assert false} may be called if the emulator finds itself in an `impossible situation', such as encountering an empty list where a list containing one element is expected.
484In this respect, we used \texttt{assert false} in a similar way to the previously described use of incomplete pattern analysis.
485\item
486\textbf{Assert false} may be called is some feature of the physical 8051 processor is not implemented in the O'Caml emulator and an executing program is attempting to use it.
487\item
488\textbf{Assert false} may be called when the real, physical processor's behaviour is undefined in a particular context.
489An example of this is loading a program which is too large for the available amount of code memory that the processor provides.
490\end{enumerate}
491
492The four manifestations of partiality above can be split into two types: partiality that manifests itself due to O'Caml's type system not being strong enough to rule the cause out, and partiality that signals a `real' crash in the processor due to the user attempting to use an unimplemented feature.
493Items 1 and 2 belong to the former class, Items 3 and 4 to the latter.
494
495Clearly Items 1 and 2 above must be addressed in the Matita formalisation.
496Item 2 is solved through extensive use of dependent types.
497Indexing into lists and vectors, for instance, is always `type safe', as we provide probing functions with strong dependent types.
498
499Item 1 is perhaps the most problematic of the three problems, as we either have to provide an exhaustive case analysis, use pattern wildcards, or find a clever way of encoding the possible patterns that are expected as input in the type of a function.
500We employ a technique that implements the latter idea.
501This is discussed in Subsection~\ref{subsect.addressing.modes.use.of.dependent.types}.
502
503To solve Item 3 above in the Matita formalisation of the emulator, we introduce an axiom \texttt{not\_implemented} of type \texttt{False}.
504When the emulator attempts to use an unimplemented feature, we introduce a metavariable, corresponding to an open proof obligation.
505These obligations are closed by performing a case analysis over \texttt{not\_implemented}.
506
507In the rare case that Item 4 is encountered (only once in the implementation of the emulator, in the \texttt{assembly} function), we use the Maybe monad to signal failure or success.
508
509\subsection{Addressing modes: use of dependent types}
510\label{subsect.addressing.modes.use.of.dependent.types}
511
512We provide an inductive data type representing all possible addressing modes of 8051 assembly.
513This is the type that functions will pattern match against.
514
515\begin{quote}
516\begin{lstlisting}
517ninductive addressing_mode: Type[0] ≝
518  DIRECT: Byte $\rightarrow$ addressing_mode
519| INDIRECT: Bit $\rightarrow$ addressing_mode
520...
521\end{lstlisting}
522\end{quote}
523However, we also wish to express in the type of our functions the \emph{impossibility} of pattern matching against certain constructors.
524In order to do this, we introduce an inductive type of addressing mode `tags'.
525The constructors of \texttt{addressing\_mode\_tag} are in one-one correspondence with the constructors of \texttt{addressing\_mode}:
526\begin{quote}
527\begin{lstlisting}
528ninductive addressing_mode_tag : Type[0] ≝
529  direct: addressing_mode_tag
530| indirect: addressing_mode_tag
531...
532\end{lstlisting}
533\end{quote}
534We then provide a function that checks whether an \texttt{addressing\_mode} is `morally' an \texttt{addressing\_mode\_tag}, as follows:
535\begin{quote}
536\begin{lstlisting}
537nlet rec is_a (d:addressing_mode_tag) (A:addressing_mode) on d ≝
538  match d with
539   [ direct $\Rightarrow$ match A with [ DIRECT _ $\Rightarrow$ true | _ $\Rightarrow$ false ]
540   | indirect $\Rightarrow$ match A with [ INDIRECT _ $\Rightarrow$ true | _ $\Rightarrow$ false ]
541...
542\end{lstlisting}
543\end{quote}
544We also extend this check to vectors of \texttt{addressing\_mode\_tag}'s in the obvious manner:
545\begin{quote}
546\begin{lstlisting}
547nlet rec is_in (n: Nat) (l: Vector addressing_mode_tag n) (A:addressing_mode) on l ≝
548 match l return $\lambda$m.$\lambda$_ :Vector addressing_mode_tag m.Bool with
549  [ VEmpty $\Rightarrow$ false
550  | VCons m he (tl: Vector addressing_mode_tag m) $\Rightarrow$
551     is_a he A $\vee$ is_in ? tl A ].
552\end{lstlisting}
553\end{quote}
554Here \texttt{VEmpty} and \texttt{VCons} are the two constructors of the \texttt{Vector} data type, and $\mathtt{\vee}$ is inclusive disjunction on Booleans.
555\begin{quote}
556\begin{lstlisting}
557nrecord subaddressing_mode (n: Nat) (l: Vector addressing_mode_tag (S n)) : Type[0] ≝
558{
559  subaddressing_modeel :> addressing_mode;
560  subaddressing_modein: bool_to_Prop (is_in ? l subaddressing_modeel)
561}.
562\end{lstlisting}
563\end{quote}
564We can now provide an inductive type of preinstructions with precise typings:
565\begin{quote}
566\begin{lstlisting}
567ninductive preinstruction (A: Type[0]): Type[0] ≝
568   ADD: $\llbracket$ acc_a $\rrbracket$ $\rightarrow$ $\llbracket$ register; direct; indirect; data $\rrbracket$ $\rightarrow$ preinstruction A
569 | ADDC: $\llbracket$ acc_a $\rrbracket$ $\rightarrow$ $\llbracket$ register; direct; indirect; data $\rrbracket$ $\rightarrow$ preinstruction A
570...
571\end{lstlisting}
572\end{quote}
573Here $\llbracket - \rrbracket$ is syntax denoting a vector.
574We see that the constructor \texttt{ADD} expects two parameters, the first being the accumulator A (\texttt{acc\_a}), and the second being one of a register, direct, indirect or data addressing mode.
575
576The final, missing component is a pair of type coercions from \texttt{addressing\_mode} to \texttt{subaddressing\_mode} and from \texttt{subaddressing\_mode} to \texttt{Type$\lbrack0\rbrack$}, respectively.
577The previous machinery allows us to state in the type of a function what addressing modes that function expects.
578For instance, consider \texttt{set\_arg\_16}, which expects only a \texttt{DPTR}:
579\begin{quote}
580\begin{lstlisting}
581ndefinition set_arg_16: Status $\rightarrow$ Word $\rightarrow$ $\llbracket$ dptr $\rrbracket$ $\rightarrow$ Status ≝
582  $\lambda$s, v, a.
583   match a return $\lambda$x. bool_to_Prop (is_in ? $\llbracket$ dptr $\rrbracket$ x) $\rightarrow$ ? with
584     [ DPTR $\Rightarrow$ $\lambda$_: True.
585       let 〈 bu, bl 〉 := split $\ldots$ eight eight v in
586       let status := set_8051_sfr s SFR_DPH bu in
587       let status := set_8051_sfr status SFR_DPL bl in
588         status
589     | _ $\Rightarrow$ $\lambda$_: False.
590       match K in False with
591       [
592       ]
593     ] (subaddressing_modein $\ldots$ a).
594\end{lstlisting}
595\end{quote}
596All other cases are discharged by the catch-all at the bottom of the match expression.
597Attempting to match against another addressing mode not indicated in the type (for example, \texttt{REGISTER}) will produce a type-error.
598
599\subsection{Validation}
600\label{subsect.matita.validation}
601
602Two means of validating the Matita emulator exist.
603
604The emulator is executable from within Matita (naturally, the speed of execution is only a fraction of the speed of the O'Caml emulator).
605In particular, we provide a function \texttt{execute\_trace} which executes a fixed number of steps of an 8051 assembly program, returning a trace of the instructions executed, in the form of a list.
606This trace may then be compared with the trace produced by the O'Caml emulator when executing a program for validation purposes.
607
608Alternatively, once the Matita emulator is ported to the newest version of Matita (see Subsection~\ref{subsect.future.work}) an executable O'Caml emulator can be extracted from the Matita code, and execution traces of the extracted and prototype O'Caml emulators can be compared side-by-side.
609
610\subsection{Future work}
611\label{subsect.future.work}
612
613The Matita emulator is written in the latest public Subversion repository version of Matita.
614However, this version is in an intermediate stage between the `old' Matita, and a new, more streamlined version of the proof assistant.
615As a result, some key features of the system are currently missing in the repository version of Matita, most notably program code extraction from a Matita theory file.
616
617The new, rewritten version of Matita reinstates the missing functionality.
618We plan, once the newer version is released, to port the Matita emulator to the most up-to-date version of the proof assistant.
619This will allow us to extract a verified O'Caml emulator from the Matita theory files.
620
621Another possible future work is to implement separate compilation by modifying the \texttt{assembly} function output to include a simble
622table and by adding a linking function.
623
624The assembly function will be changed to minimize (or at least reduce) the size of the assembled program by translating pseudo jumps
625to short jumps where possible.
626
627Finally, while the O'Caml emulator already implements I/O, timers and interrupt handling, the Matita version does not. Interrupt handling
628will not be dealt with in CerCo and we are likely to handle I/O in a simplified way by means of external library functions. Nevertheless,
629for the sake of completeness and future uses, we plan to eventually complete also the Matita version.
630
631\newpage
632
633\section{Listing of O'Caml files and functions}
634\label{sect.listing.ocaml.files.functions}
635
636\subsection{Listing of O'Caml files}
637\label{subsect.listing.ocaml.files}
638
639\begin{center}
640\begin{tabular*}{0.9\textwidth}{p{3cm}p{9cm}}
641Title & Description \\
642\hline
643\texttt{ASM.mli} & Containts algebraic datatypes representing assembly code. \\
644\texttt{ASMInterpret.ml} & Contains the main emulation function, and auxiliary datatypes and functions necessary for emulation. \\
645\texttt{BitVectors.ml} & Contains an implementation of bitvectors, using polymorphic variants to emulate dependent types. \\
646\texttt{IntelHex.ml} & Contains functions for parsing the Intel IHX file format. \\
647\texttt{MatitaPretty.ml} & Functions for pretty printing an assembly abstract syntax tree in the O'Caml compiler into its equivalent form in the Matita compiler. \\
648\texttt{Parser.ml} & Generic functional parser combinators used for parsing the Intel IHX file format. \\
649\texttt{Physical.ml} & Functions implementing arithmetic (for instance, addition and subtraction with carry) on bitvectors. \\
650\texttt{Pretty.ml} & Functions for pretty printing assembly abstract syntax trees in the O'Caml compiler into a string form. \\
651\texttt{Test.ml} & Test harness for emulator.  Reads in and parses an Intel IHX file, and executes the resulting program. \\
652\texttt{ToMatita.ml} & Funtions for exporting an Intel IHX file to a form the Matita emulator can understand. \\
653\texttt{Util.ml} & Miscellaneous utility functions that do not fit elsewhere. \\
654\end{tabular*}
655\end{center}
656
657\subsection{Selected important functions}
658\label{subsect.selected.important.functions}
659
660\subsubsection{From \texttt{ASMInterpret.ml(i)}}
661
662\begin{center}
663\begin{tabular*}{0.85\textwidth}{p{3cm}@{\quad}p{9cm}}
664Name & Description \\
665\hline
666\texttt{assembly} & Assembles an abstract syntax tree representing an 8051 assembly program into a list of bytes, its compiled form. \\
667\texttt{initialize} & Initializes the emulator status. \\
668\texttt{load} & Loads an assembled program into the emulator's code memory. \\
669\texttt{fetch} & Fetches the next instruction, and automatically increments the program counter. \\
670\texttt{execute} & Emulates the processor.  Accepts as input a function that pretty prints the emulator status after every emulation loop. \\
671\end{tabular*}
672\end{center}
673
674\subsubsection{From \texttt{IntelHex.ml(i)}}
675
676\begin{center}
677\begin{tabular*}{0.85\textwidth}{p{3cm}@{\quad}p{9cm}}
678Name & Description \\
679\hline
680\texttt{intel\_hex\_of\_file} & Reads in a file and parses it if in Intel IHX format, otherwise raises an exception. \\
681\texttt{process\_intel\_hex} & Accepts a parsed Intel IHX file and populates a hashmap (of the same type as code memory) with the contents.
682\end{tabular*}
683\end{center}
684
685\subsubsection{From \texttt{Physical.ml(i)}}
686
687\begin{center}
688\begin{tabular*}{0.85\textwidth}{p{3cm}@{\quad}p{9cm}}
689Name & Description \\
690\hline
691\texttt{subb8\_with\_c} & Performs an eight bit subtraction on bitvectors.  The function also returns the most important PSW flags for the 8051: carry, auxiliary carry and overflow. \\
692\texttt{add8\_with\_c} & Performs an eight bit addition on bitvectors.  The function also returns the most important PSW flags for the 8051: carry, auxiliary carry and overflow. \\
693\texttt{dec} & Decrements an eight bit bitvector with underflow, if necessary. \\
694\texttt{inc} & Increments an eight bit bitvector with overflow, if necessary.
695\end{tabular*}
696\end{center}
697
698\newpage
699
700\section{Listing of Matita files and functions}
701\label{sect.listing.matita.files.functions}
702
703\subsection{Listing of Matita files}
704\label{subsect.listing.files}
705
706\begin{center}
707\begin{tabular*}{0.75\textwidth}{p{3cm}p{9cm}}
708Title & Description \\
709\hline
710\texttt{Arithmetic.ma} & Contains functions implementing arithmetical operations on bitvectors. \\
711\texttt{ASM.ma} & Contains inductive datatypes for representing abstract syntax trees of 8051 assembly language. \\
712\texttt{Assembly.ma} & Contains functions related to the assembly of 8051 assembly programs into a list of bytes. \\
713\texttt{BitVector.ma} & Contains functions specific to bitvectors. \\
714\texttt{BitVectorTrie.ma} & Contains an implementation of a sparse bitvector trie, which we use for implementing memory in the processor. \\
715\texttt{Bool.ma} & Implementation of Booleans, and related functions. \\
716\texttt{Cartesian.ma} & Implementation of Cartesian products, and related functions. \\
717\texttt{Char.ma} & Hypothesises a type of characters. \\
718\texttt{Connectives.ma} & Implementation of logical connectives. \\
719\texttt{DoTest.ma} & Contains experiments and debugging code for testing the emulator. \\
720\texttt{Either.ma} & Implementation of disjoint union types. \\
721\texttt{Exponential.ma} & Functions implementating the Natural exponential, and related lemmas. \\
722\texttt{Fetch.ma} & Contains functions relating to the `fetch' function of the emulator, and related functions. \\
723\texttt{Interpret.ma} & Contains the main emulator function, as well as ancillary definitions and functions. \\
724\texttt{List.ma} & An implementation of polymorphic lists, and related functions. \\
725\texttt{Maybe.ma} & Implementation of the `maybe' type. \\
726\texttt{Nat.ma} & Implementation of Natural numbers, and related functions and lemmas. \\
727\texttt{Status.ma} & Contains the definition of the `status' record, and related definitions. \\
728\texttt{String.ma} & Contains a type for representing strings. \\
729\texttt{Test.ma} & Contains definitions useful for debugging and testing the emulator. \\
730\texttt{Universes.ma} & Infrastructure file related to Matita's universe hierarchy. \\
731\texttt{Util.ma} & Contains miscellaneous utility functions that do not fit anywhere else. \\
732\texttt{Vector.ma} & Contains an implementation of polymorphic vectors, and related definitions.
733\end{tabular*}
734\end{center}
735
736\subsection{Selected important functions}
737\label{subsect.matita.selected.important.functions}
738
739\subsubsection{From \texttt{Arithmetic.ma}}
740
741\begin{center}
742\begin{tabular*}{0.75\textwidth}{p{3cm}p{9cm}}
743Title & Description \\
744\hline
745\texttt{add\_n\_with\_carry} & Performs an $n$ bit addition on bitvectors.  The function also returns the most important PSW flags for the 8051: carry, auxiliary carry and overflow. \\
746\texttt{sub\_8\_with\_carry} & Performs an eight bit subtraction on bitvectors. The function also returns the most important PSW flags for the 8051: carry, auxiliary carry and overflow. \\
747\texttt{half\_add} & Performs a standard half addition on bitvectors, returning the result and carry bit. \\
748\texttt{full\_add} & Performs a standard full addition on bitvectors and a carry bit, returning the result and a carry bit.
749\end{tabular*}
750\end{center}
751
752\subsubsection{From \texttt{Assembly.ma}}
753
754\begin{center}
755\begin{tabular*}{0.75\textwidth}{p{3cm}p{9cm}}
756Title & Description \\
757\hline
758\texttt{assemble1} & Assembles a single 8051 assembly instruction into its memory representation. \\
759\texttt{assemble} & Assembles an 8051 assembly program into its memory representation.\\
760\texttt{assemble\_unlabelled\_program} &\\& Assembles a list of (unlabelled) 8051 assembly instructions into its memory representation.
761\end{tabular*}
762\end{center}
763
764\subsubsection{From \texttt{BitVectorTrie.ma}}
765
766\begin{center}
767\begin{tabular*}{0.75\textwidth}{p{3cm}p{9cm}}
768Title & Description \\
769\hline
770\texttt{lookup} & Returns the data stored at the end of a particular path (a bitvector) from the trie.  If no data exists, returns a default value. \\
771\texttt{insert} & Inserts data into a tree at the end of the path (a bitvector) indicated.  Automatically expands the tree (by filling in stubs) if necessary.
772\end{tabular*}
773\end{center}
774
775\subsubsection{From \texttt{DoTest.ma}}
776
777\begin{center}
778\begin{tabular*}{0.75\textwidth}{p{3cm}p{9cm}}
779Title & Description \\
780\hline
781\texttt{execute\_trace} & Executes an assembly program for a fixed number of steps, recording in a trace which instructions were executed.
782\end{tabular*}
783\end{center}
784
785\subsubsection{From \texttt{Fetch.ma}}
786
787\begin{center}
788\begin{tabular*}{0.75\textwidth}{p{3cm}p{9cm}}
789Title & Description \\
790\hline
791\texttt{fetch} & Decodes and returns the instruction currently pointed to by the program counter and automatically increments the program counter the required amount to point to the next instruction. \\
792\end{tabular*}
793\end{center}
794
795\subsubsection{From \texttt{Interpret.ma}}
796
797\begin{center}
798\begin{tabular*}{0.75\textwidth}{p{3cm}p{9cm}}
799Title & Description \\
800\hline
801\texttt{execute\_1} & Executes a single step of an 8051 assembly program. \\
802\texttt{execute} & Executes a fixed number of steps of an 8051 assembly program.
803\end{tabular*}
804\end{center}
805
806\subsubsection{From \texttt{Status.ma}}
807
808\begin{center}
809\begin{tabular*}{0.75\textwidth}{p{3cm}p{9cm}}
810Title & Description \\
811\hline
812\texttt{load} & Loads an assembled 8051 assembly program into code memory.
813\end{tabular*}
814\end{center}
815\end{document}
Note: See TracBrowser for help on using the repository browser.