source: Deliverables/D4.1/ITP-Paper/itp-2011.tex @ 555

Last change on this file since 555 was 555, checked in by mulligan, 9 years ago

Resolved conflict, updated bibtex, finished bibliography, and llncs.cls updated to latest version.

File size: 53.7 KB
Line 
1\documentclass{llncs}
2
3\usepackage{amsfonts}
4\usepackage{amsmath}
5\usepackage{amssymb} 
6\usepackage[english]{babel}
7\usepackage{color}
8\usepackage{fancybox}
9\usepackage{graphicx}
10\usepackage[colorlinks]{hyperref}
11\usepackage[utf8x]{inputenc}
12\usepackage{listings}
13\usepackage{mdwlist}
14\usepackage{microtype}
15\usepackage{stmaryrd}
16\usepackage{url}
17
18\newlength{\mylength} 
19\newenvironment{frametxt}%
20        {\setlength{\fboxsep}{5pt}
21                \setlength{\mylength}{\linewidth}%
22                \addtolength{\mylength}{-2\fboxsep}%
23                \addtolength{\mylength}{-2\fboxrule}%
24                \Sbox
25                \minipage{\mylength}%
26                        \setlength{\abovedisplayskip}{0pt}%
27                        \setlength{\belowdisplayskip}{0pt}%
28                }%
29                {\endminipage\endSbox
30                        \[\fbox{\TheSbox}\]}
31
32\lstdefinelanguage{matita-ocaml}
33  {keywords={definition,coercion,lemma,theorem,remark,inductive,record,qed,let,in,rec,match,return,with,Type,try,on,to},
34   morekeywords={[2]whd,normalize,elim,cases,destruct},
35   morekeywords={[3]type,of,val,assert,let,function},
36   mathescape=true,
37  }
38\lstset{language=matita-ocaml,basicstyle=\small\tt,columns=flexible,breaklines=false,
39        keywordstyle=\color{red}\bfseries,
40        keywordstyle=[2]\color{blue},
41        keywordstyle=[3]\color{blue}\bfseries,
42        commentstyle=\color{green},
43        stringstyle=\color{blue},
44        showspaces=false,showstringspaces=false}
45\lstset{extendedchars=false}
46\lstset{inputencoding=utf8x}
47\DeclareUnicodeCharacter{8797}{:=}
48\DeclareUnicodeCharacter{10746}{++}
49\DeclareUnicodeCharacter{9001}{\ensuremath{\langle}}
50\DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}}
51
52\author{Dominic P. Mulligan\thanks{The project CerCo acknowledges the financial support of the Future and
53Emerging Technologies (FET) programme within the Seventh Framework
54Programme for Research of the European Commission, under FET-Open grant
55number: 243881} \and Claudio Sacerdoti Coen$^\star$}
56\authorrunning{D. P. Mulligan and C. Sacerdoti Coen}
57\title{An executable formalisation of the MCS-51 microprocessor in Matita}
58\titlerunning{An executable formalisation of the MCS-51}
59\institute{Dipartimento di Scienze dell'Informazione, Universit\`a di Bologna}
60
61\bibliographystyle{plain}
62
63\begin{document}
64
65\maketitle
66
67\begin{abstract}
68We summarise our formalisation of an emulator for the MCS-51 microprocessor in the Matita proof assistant.
69The MCS-51 is a widely used 8-bit microprocessor, especially popular in embedded devices.
70
71We proceeded in two stages, first implementing in O'Caml a prototype emulator, where bugs could be `ironed out' quickly.
72We then ported our O'Caml emulator to Matita's internal language.
73Though mostly straight-forward, this porting presented multiple problems.
74Of particular interest is how we handle the extreme non-orthoganality of the MSC-51's instruction set.
75In O'Caml, this was handled through heavy use of polymorphic variants.
76In Matita, we achieve the same effect through a non-standard use of dependent types.
77
78Both the O'Caml and Matita emulators are `executable'.
79Assembly programs may be animated within Matita, producing a trace of instructions executed.
80
81Our formalisation is a major component of the ongoing EU-funded CerCo project.
82\end{abstract}
83
84%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
85% SECTION                                                                      %
86%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
87\section{Background}
88\label{sect.introduction}
89
90Formal methods are designed to increase our confidence in the design and implementation of software (and hardware).
91Ideally, we would like all software to come equipped with a formal specification, along with a proof of correctness that the software meets this specification.
92Today the majority of programs are written in high level languages and then compiled into low level ones.
93Specifications are therefore also given at a high level and correctness can be proved by reasoning automatically or interactively on the program's source code.
94The code that is actually run, however, is not the high level source code that we reason on, but the object code that is generated by the compiler.
95A few simple questions now arise:
96\begin{itemize*}
97\item
98What properties are preserved during compilation?
99\item
100What properties are affected by the compilation strategy?
101\item
102To what extent can you trust your compiler in preserving those properties?
103\end{itemize*}
104These questions, and others like them, motivate a current `hot topic' in computer science research: \emph{compiler verification} (for instance~\cite{leroy:formal:2009,chlipala:verified:2010}, and many others).
105So far, the field has been focused on the first and last questions only.
106In particular, much attention has been placed on verifying compiler correctness with respect to extensional properties of programs, which are easily preserved during compilation; it is sufficient to completely preserve the denotational semantics of the input program.
107
108However, if we consider intensional properties of programs---such as space, time or energy spent into computation and transmission of data---the situation is more complex.
109To even be able to express these properties, and to be able to reason about them, we are forced to adopt a cost model that assigns a cost to single, or blocks, of instructions.
110Ideally, we would like to have a compositional cost model that assigns the same cost to all occurrences of one instruction.
111However, compiler optimisations are inherently non-compositional: each occurrence of a high level instruction is usually compiled in a different way according to the context it finds itself in.
112Therefore both the cost model and intensional specifications are affected by the compilation process.
113
114In the current EU project CerCo (`Certified Complexity')~\cite{cerco:2011} we approach the problem of reasoning about intensional properties of programs as follows.
115We are currently developing a compiler that induces a cost model on the high level source code.
116Costs are assigned to each block of high level instructions by considering the costs of the corresponding blocks of compiled object code.
117The cost model is therefore inherently non-compositional.
118However, the model has the potential to be extremely \emph{precise}, capturing a program's \emph{realistic} cost, by taking into account, not ignoring, the compilation process.
119A prototype compiler, where no approximation of the cost is provided, has been developed.
120(The full technical details of the CerCo cost model is explained in~\cite{amadio:certifying:2010}.)
121
122We believe that our approach is especially applicable to certifying real time programs.
123Here, a user can certify that all `deadlines' are met whilst wringing as many clock cycles from the processor---using a cost model that does not over-estimate---as possible.
124
125Further, we see our approach as being relevant to the field of compiler verification (and construction) itself.
126For instance, an optimisation specified only extensionally is only half specified; though the optimisation may preserve the denotational semantics of a program, there is no guarantee that any intensional properties of the program, such as space or time usage, will be improved.
127Another potential application is toward completeness and correctness of the compilation process in the presence of space constraints.
128Here, a compiler could potentially reject a source program targetting an embedded system when the size of the compiled code exceeds the available ROM size.
129Moreover, preservation of a program's semantics may only be required for those programs that do not exhaust the stack or heap.
130Hence the statement of completeness of the compiler must take in to account a realistic cost model.
131
132In the methodology proposed in CerCo we assume we are able to compute on the object code exact and realistic costs for sequential blocks of instructions.
133With modern processors, though possible (see~\cite{bate:wcet:2011,yan:wcet:2008} for instance), it is difficult to compute exact costs or to reasonably approximate them.
134This is because the execution of a program itself has an influence on the speed of processing.
135For instance, caching, memory effects and other advanced features such as branch prediction all have a profound effect on execution speeds.
136For this reason CerCo decided to focus on 8-bit microprocessors.
137These are still widely used in embedded systems, and have the advantage of an easily predictable cost model due to the relative sparcity of features that they possess.
138
139In particular, we have fully formalised an executable formal semantics of a family of 8 bit Freescale Microprocessors~\cite{oliboni:matita:2008}, and provided a similar executable formal semantics for the MCS-51 microprocessor.
140The latter work is what we describe in this paper.
141The main focus of the formalisation has been on capturing the intensional behaviour of the processor.
142However, the design of the MCS-51 itself has caused problems in our formalisation.
143For example, the MCS-51 has a highly unorthogonal instruction set.
144To cope with this unorthogonality, and to produce an executable specification, we have exploited the dependent type system of Matita, an interactive proof assistant.
145
146\subsection{The 8051/8052}
147\label{subsect.8051-8052}
148
149The MCS-51 is an eight bit microprocessor introduced by Intel in the late 1970s.
150Commonly called the 8051, in the three decades since its introduction the processor has become a highly popular target for embedded systems engineers.
151Further, the processor, its immediate successor the 8052, and many derivatives are still manufactured \emph{en masse} by a host of semiconductor suppliers.
152
153The 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.
154For instance, the open source Small Device C Compiler (SDCC) recognises a dialect of C~\cite{sdcc:2010}, and other compilers targeting the 8051 for BASIC, Forth and Modula-2 are also extant.
155An open source emulator for the processor, MCU-8051 IDE, is also available~\cite{mcu8051ide:2010}.
156Both MCU-8051 IDE and SDCC were used profitably in the implementation of our formalisation.
157
158\begin{figure}[t]
159\begin{center}
160\includegraphics[scale=0.5]{memorylayout.png}
161\end{center}
162\caption{High level overview of the 8051 memory layout}
163\label{fig.memory.layout}
164\end{figure}
165
166The 8051 has a relatively straightforward architecture, unencumbered by advanced features of modern processors, making it an ideal target for formalisation.
167A high-level overview of the processor's memory layout is provided in Figure~\ref{fig.memory.layout}.
168
169Processor RAM is divided into numerous segments, with the most prominent division being between internal and (optional) external memory.
170Internal memory, commonly provided on the die itself with fast access, is composed of 256 bytes, but, in direct addressing mode, half of them are overloaded with 128 bytes of memory mapped Special Function Registers (SFRs) which control the operation of the processor.
171Internal RAM (IRAM) is further divided into eight general purpose bit-addressable registers (R0--R7).
172These sit in the first eight bytes of IRAM, though can be programmatically `shifted up' as needed.
173Bit memory, followed by a small amount of stack space, resides in the memory space immediately after the register banks.
174What remains of the IRAM may be treated as general purpose memory.
175A schematic view of IRAM layout is provided in Figure~\ref{fig.iram.layout}.
176
177External RAM (XRAM), limited to a maximum size of 64 kilobytes, is optional, and may be provided on or off chip, depending on the manufacturer.
178XRAM is accessed using a dedicated instruction, and requires sixteen bits to address fully.
179External code memory (XCODE) is often stored in the form of an EPROM, and limited to 64 kilobytes in size.
180However, depending on the particular manufacturer and processor model, a dedicated on-die read-only memory area for program code (ICODE) may also be supplied.
181
182Memory may be addressed in numerous ways: immediate, direct, indirect, external direct and code indirect.
183As 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.
184For 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. Moreover, some memory segments are addressed using 8 bits pointers while others require 16 bits.
185
186The 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.
187Further, the processor possesses two eight bit general purpose accumulators, A and B.
188
189Communication with the device is facilitated by an onboard UART serial port, and associated serial controller, which can operate in numerous modes.
190Serial baud rate is determined by one of two sixteen bit timers included with the 8051, which can be set to multiple modes of operation.
191(The 8052 provides an additional sixteen bit timer.)
192As an additional method of communication, the 8051 also provides a four byte bit-addressable input-output port.
193
194The programmer may take advantage of the interrupt mechanism that the processor provides.
195This 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.
196
197Interrupts 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.
198However, interrupts may be set to one of two priorities: low and high.
199The 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.
200
201The 8051 has interrupts disabled by default.
202The programmer is free to handle serial input and output manually, by poking serial flags in the SFRs.
203Similarly, `exceptional circumstances' that would otherwise trigger an interrupt on more modern processors, for example, division by zero, are also signalled by setting flags.
204
205\begin{figure}[t]
206\begin{center}
207\includegraphics[scale=0.5]{iramlayout.png}
208\end{center}
209\caption{Schematic view of 8051 IRAM layout}
210\label{fig.iram.layout}
211\end{figure}
212
213%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
214% SECTION                                                                      %
215%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
216\subsection{Overview of paper}
217\label{subsect.overview.paper}
218
219In Section~\ref{sect.design.issues.formalisation} we discuss design issues in the development of the formalisation.
220In Section~\ref{sect.validation} we discuss how we validated the design and implementation of our emulator to ensure that what we formalised was an accurate model of an MCS-51 series microprocessor.
221In Section~\ref{sect.related.work} we describe previous work, with an eye toward describing its relation with the work described herein.
222In Section~\ref{sect.conclusions} we conclude the paper.
223
224In Appendices~\ref{sect.listing.main.ocaml.functions} and~\ref{sect.listing.main.matita.functions} we provide a brief overview of the main functions in our implementation, and describe at a high level what they do.
225
226%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
227% SECTION                                                                      %
228%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
229\section{Design issues in the formalisation}
230\label{sect.design.issues.formalisation}
231
232From hereonin, we typeset O'Caml source with \texttt{\color{blue}{blue}} and Matita source with \texttt{\color{red}{red}} to distinguish the two syntaxes.
233Matita's syntax is largely straightforward to those familiar with Coq or O'Caml.
234The only subtlety is the use of `\texttt{?}' in an argument position denoting an argument that should be inferred automatically.
235
236\subsection{Development strategy}
237\label{subsect.development.strategy}
238
239Our implementation progressed in two stages.
240We began with an emulator written in O'Caml.
241We used this to `iron out' any bugs in our design and implementation within O'Caml's more permissive type system.
242O'Caml's ability to perform file input-output also eased debugging and validation.
243Once we were happy with the performance and design of the O'Caml emulator, we moved to the Matita formalisation.
244
245Matita's syntax is lexically similar to O'Caml's.
246This eased the translation, as large swathes of code were merely copy-pasted with minor modifications.
247However, several major issues had to be addresses when moving from O'Caml to Matita.
248These are now discussed.
249
250%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
251% SECTION                                                                      %
252%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
253\subsection{Representation of bytes, words, etc.}
254\label{subsect.representation.integers}
255
256\begin{figure}[t]
257\begin{minipage}[t]{0.45\textwidth}
258\vspace{0pt}
259\begin{lstlisting}
260type 'a vect = bit list
261type nibble = [`Sixteen] vect
262type byte = [`Eight] vect
263$\color{blue}{\mathtt{let}}$ split_word w = split_nth 4 w
264$\color{blue}{\mathtt{let}}$ split_byte b = split_nth 2 b
265\end{lstlisting}
266\end{minipage}
267%
268\begin{minipage}[t]{0.55\textwidth}
269\vspace{0pt}
270\begin{lstlisting}
271type 'a vect
272type word = [`Sixteen] vect
273type byte = [`Eight] vect
274val split_word: word -> byte * word
275val split_byte: byte -> nibble * nibble
276\end{lstlisting}
277\end{minipage}
278\caption{Sample of O'Caml implementation and interface for bitvectors module}
279\label{fig.ocaml.implementation.bitvectors}
280\end{figure}
281
282The formalization of MCS-51 must deal with bytes (8 bits), words (16 bits) but also with more exoteric quantities (7 bits, 3 bits, 9 bits).
283To avoid size mismatch bugs difficult to spot, we represent all of these quantities using bitvectors, i.e. fixed length vectors of booleans.
284In our O'Caml emulator, we `faked' bitvectors using phantom types implemented with polymorphic variants\cite{phantom_types_ocaml}, as in Figure~\ref{fig.ocaml.implementation.bitvectors}.
285From within the bitvector module (left column) bitvectors are just lists of bits and no guarantee is provided on sizes.
286However, the module's interface (right column) enforces the size invariants in the rest of the code.
287
288In Matita, we are able to use the full power of dependent types to always work with vectors of a known size:
289\begin{lstlisting}
290inductive Vector (A: Type[0]): nat → Type[0] ≝
291  VEmpty: Vector A O
292| VCons: ∀n: nat. A → Vector A n → Vector A (S n).
293\end{lstlisting}
294We define \texttt{BitVector} as a specialization of \texttt{Vector} to \texttt{bool}.
295We may use Matita's type system to provide precise typing for functions that are
296polymorphic in the size without having to duplicate the code as we did in O'Caml:
297\begin{lstlisting}
298let rec split (A: Type[0]) (m,n: nat) on m:
299   Vector A (plus m n) $\rightarrow$ (Vector A m) $\times$ (Vector A n) := ...
300\end{lstlisting}
301
302%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
303% SECTION                                                                      %
304%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
305\subsection{Representing memory}
306\label{subsect.representing.memory}
307
308The MCS-51 has numerous different types of memory.
309In our prototype implementation, we simply used a map datastructure from the O'Caml standard library.
310Matita's standard library is relatively small, and does not contain a generic map datastructure.
311Therefore, we had the opportunity of crafting a special-purpose datastructure for the job.
312
313We worked under the assumption that large swathes of memory would often be uninitialized.
314Na\"ively, using a complete binary tree, for instance, would be extremely memory inefficient.
315Instead, we chose to use a modified form of trie, where paths are represented by bitvectors.
316As bitvectors were widely used in our implementation already for representing integers, this worked well:
317\begin{lstlisting}
318inductive BitVectorTrie (A: Type[0]): nat $\rightarrow$ Type[0] ≝
319  Leaf: A $\rightarrow$ BitVectorTrie A 0
320| Node: ∀n. BitVectorTrie A n $\rightarrow$ BitVectorTrie A n $\rightarrow$ BitVectorTrie A (S n)
321| Stub: ∀n. BitVectorTrie A n.
322\end{lstlisting}
323Here, \texttt{Stub} is a constructor that can appear at any point in our tries.
324It internalises the notion of `uninitialized data'.
325Performing a lookup in memory is now straight-forward.
326We merely traverse a path, and if at any point we encounter a \texttt{Stub}, we return a default value\footnote{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 do not believe that this is an outrageous decision, as SDCC for instance generates code which first `zeroes out' all 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.}.
327As we are using bitvectors, we may make full use of dependent types and ensure that our bitvector paths are of the same length as the height of the tree.
328
329%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
330% SECTION                                                                      %
331%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
332\subsection{Labels and pseudoinstructions}
333\label{subsect.labels.pseudoinstructions}
334
335Aside from implementing the core MCS-51 instruction set, we also provided \emph{pseudoinstructions}, \emph{labels} and \emph{cost labels}.
336The purpose of \emph{cost labels} will be explained in Subsection~\ref{subsect.computation.cost.traces}.
337
338Introducing pseudoinstructions had the effect of simplifying a C compiler---another component of the CerCo project---that was being implemented in parallel with our implementation.
339To understand why this is so, consider the fact that the MCS-51's instruction set has numerous instructions for unconditional and conditional jumps to memory locations.
340For instance, the instructions \texttt{AJMP}, \texttt{JMP} and \texttt{LJMP} all perform unconditional jumps.
341However, these instructions differ in how large the maximum size of the offset of the jump to be performed can be.
342Further, all jump instructions require a concrete memory address---to jump to---to be specified.
343Requiring the compiler to compute these offsets, and select appropriate jump instructions, was seen as needleslly burdensome.
344
345Introducing labels also had a simplifying effect on the design of the compiler.
346Instead of jumping to a concrete address, the compiler could `just' jump to a label.
347In this vein, we introduced pseudoinstructions for both unconditional and conditional jumps to a label.
348
349Further, we also introduced labels for storing global data in a preamble before the program.
350A pseudoinstruction \texttt{Mov} moves (16-bit) data stored at a label into the (16-bit) register \texttt{DPTR}.
351We believe this facility, of storing global data in a preamble referenced by a label, will also make any future extension considering separate compilation much simpler.
352
353Our pseudoinstructions and labels induce an assembly language similar to that of SDCC.
354All pseudoinstructions and labels are `assembled away', prior to program execution, using a preprocessing stage.
355Jumps are computed in two stages.
356The first stage builds a map associating memory addresses to labels, with the second stage removing pseudojumps with concrete jumps to the correct address.
357
358%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
359% SECTION                                                                      %
360%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
361\subsection{Anatomy of the (Matita) emulator}
362\label{subsect.anatomy.matita.emulator}
363
364The internal state of our Matita emulator is represented as a record:
365\begin{lstlisting}
366record Status: Type[0] ≝
367{
368  code_memory: BitVectorTrie Byte 16;
369  low_internal_ram: BitVectorTrie Byte 7;
370  high_internal_ram: BitVectorTrie Byte 7;
371  external_ram: BitVectorTrie Byte 16;
372  program_counter: Word;
373  special_function_registers_8051: Vector Byte 19;
374  special_function_registers_8052: Vector Byte 5;
375  ...
376}.
377\end{lstlisting}
378This record neatly encapsulates the current memory contents, the program counter, the state of the current SFRs, and so on.
379One peculiarity is the packing of the 24 combined SFRs into fixed length vectors.
380This was due to a bug in Matita when we were constructing the emulator, since fixed, where the time needed to typecheck a record grew exponentially with the number of fields.
381
382Here, it appears that the MCS-51's memory spaces are completely disjoint.
383This is not so; many of them overlap with each other, and there's a many-many relationship between addressing modes and memory spaces.
384For instance, \texttt{DIRECT} addressing can be used to address low internal RAM and the SFRs, but not high internal RAM.
385
386For simplicity, we merely treat memory spaces as if they are completely disjoint in the \texttt{Status} record.
387Overlapping, and checking which addressing modes can be used to address particular memory spaces, is handled through numerous \texttt{get\_arg\_XX} and \texttt{set\_arg\_XX} (for 1, 8 and 16 bits) functions.
388
389Both the Matita and O'Caml emulators follows the classic `fetch-decode-execute' model of processor operation.
390The next instruction to be processed, indexed by the program counter, is fetched from code memory with \texttt{fetch}.
391An updated program counter, along with the concrete cost, in processor cycles for executing this instruction, is also returned.
392These costs are taken from a Siemens Semiconductor Group data sheet for the MCS-51~\cite{siemens:2011}, and will likely vary across manufacturers and particular derivatives of the processor.
393\begin{lstlisting}
394definition fetch:
395  BitVectorTrie Byte 16 $\rightarrow$ Word $\rightarrow$ instruction $\times$ Word $\times$ nat := ...
396\end{lstlisting}
397A single instruction is assembled into its corresponding bit encoding with \texttt{assembly1}:
398\begin{lstlisting}
399definition assembly1: instruction $\rightarrow$ list Byte := ...
400\end{lstlisting}
401An assembly program, consisting of a preamble containing global data, and a list of (pseudo)instructions, is assembled using \texttt{assembly}.
402Pseudoinstructions and labels are eliminated in favour of concrete instructions from the MCS-51 instruction set.
403A map associating memory locations and cost labels (see Subsection~\ref{subsect.computation.cost.traces}) is also produced.
404\begin{lstlisting}
405definition assembly:
406  assembly_program $\rightarrow$ option (list Byte $\times$ (BitVectorTrie String 16)) := ...
407\end{lstlisting}
408A single execution step of the processor is evaluated using \texttt{execute\_1}, mapping a \texttt{Status} to a \texttt{Status}:
409\begin{lstlisting}
410definition execute_1: Status $\rightarrow$ Status := ...
411\end{lstlisting}
412Multiple steps of processor execution are implemented in \texttt{execute}, which wraps \texttt{execute\_1}:
413\begin{lstlisting}
414let rec execute (n: nat) (s: Status) on n: Status := ...
415\end{lstlisting}
416This differs slightly from the design of the O'Caml emulator, which executed a program indefinitely, and also accepted a callback function as an argument, which could `witness' the execution as it happened, and providing a print-out of the processor state, and other debugging information.
417Due to Matita's requirement that all functions be strongly normalizing, \texttt{execute} cannot execute a program indefinitely, and must execute a fixed number of steps.
418
419%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
420% SECTION                                                                      %
421%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
422\subsection{Instruction set unorthogonality}
423\label{subsect.instruction.set.unorthogonality}
424
425A peculiarity of the MCS-51 is the non-orthogonality of its instruction set.
426For instance, the \texttt{MOV} instruction, can be invoked using one of sixteen combinations of addressing modes.
427
428% Show example of pattern matching with polymorphic variants
429
430Such non-orthogonality in the instruction set was handled with the use of polymorphic variants in the O'Caml emulator.
431For instance, we introduced types corresponding to each addressing mode:
432\begin{lstlisting}
433type direct = [ `DIRECT of byte ]
434type indirect = [ `INDIRECT of bit ]
435...
436\end{lstlisting}
437Which were then used in our inductive datatype for assembly instructions, as follows:
438\begin{lstlisting}
439type 'addr preinstruction =
440 [ `ADD of acc * [ reg | direct | indirect | data ]
441...
442 | `MOV of
443    (acc * [ reg | direct | indirect | data ],
444     [ reg | indirect ] * [ acc | direct | data ],
445     direct * [ acc | reg | direct | indirect | data ],
446     dptr * data16,
447     carry * bit,
448     bit * carry
449     ) union6
450...
451\end{lstlisting}
452Here, \texttt{union6} is a disjoint union type, defined as follows:
453\begin{lstlisting}
454type ('a,'b,'c,'d,'e,'f) union6 = [ `U1 of 'a | ... | `U6 of 'f ]
455\end{lstlisting}
456For our purposes, the types \texttt{union2}, \texttt{union3} and \texttt{union6} sufficed.
457
458This polymorphic variant machinery worked well: it introduced a certain level of type safety (for instance, the type of our \texttt{MOV} instruction 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.
459However, this polymorphic variant machinery is \emph{not} present in Matita.
460We needed some way to produce the same effect, which Matita supported.
461For this task, we used dependent types.
462
463We first provided an inductive data type representing all possible addressing modes, a type that functions will pattern match against:
464\begin{lstlisting}
465inductive addressing_mode: Type[0] ≝
466  DIRECT: Byte $\rightarrow$ addressing_mode
467| INDIRECT: Bit $\rightarrow$ addressing_mode
468...
469\end{lstlisting}
470We also wished to express in the type of functions the \emph{impossibility} of pattern matching against certain constructors.
471In order to do this, we introduced an inductive type of addressing mode `tags'.
472The constructors of \texttt{addressing\_mode\_tag} are in one-to-one correspondence with the constructors of \texttt{addressing\_mode}:
473\begin{lstlisting}
474inductive addressing_mode_tag : Type[0] ≝
475  direct: addressing_mode_tag
476| indirect: addressing_mode_tag
477...
478\end{lstlisting}
479A function that checks whether an \texttt{addressing\_mode} is `morally' an \texttt{addressing\_mode\_tag} is provided, as follows:
480\begin{lstlisting}
481let rec is_a (d: addressing_mode_tag) (A: addressing_mode) on d :=
482  match d with
483   [ direct $\Rightarrow$ match A with [ DIRECT _ $\Rightarrow$ true | _ $\Rightarrow$ false ]
484   | indirect $\Rightarrow$ match A with [ INDIRECT _ $\Rightarrow$ true | _ $\Rightarrow$ false ]
485...
486\end{lstlisting}
487We also extend this check to vectors of \texttt{addressing\_mode\_tag}'s in the obvious manner:
488\begin{lstlisting}
489let rec is_in (n: nat) (l: Vector addressing_mode_tag n) (A: addressing_mode) on l :=
490 match l return $\lambda$m.$\lambda$_: Vector addressing_mode_tag m. bool with
491  [ VEmpty $\Rightarrow$ false
492  | VCons m he (tl: Vector addressing_mode_tag m) $\Rightarrow$
493     is_a he A $\vee$ is_in ? tl A ].
494\end{lstlisting}
495Here $\mathtt{\vee}$ is inclusive disjunction on the \texttt{bool} datatype.
496\begin{lstlisting}
497record subaddressing_mode (n: nat) (l: Vector addressing_mode_tag (S n)): Type[0] :=
498{
499  subaddressing_modeel :> addressing_mode;
500  subaddressing_modein: bool_to_Prop (is_in ? l subaddressing_modeel)
501}.
502\end{lstlisting}
503We can now provide an inductive type of preinstructions with precise typings:
504\begin{lstlisting}
505inductive preinstruction (A: Type[0]): Type[0] ≝
506   ADD: $\llbracket$ acc_a $\rrbracket$ $\rightarrow$ $\llbracket$ register; direct; indirect; data $\rrbracket$ $\rightarrow$ preinstruction A
507 | ADDC: $\llbracket$ acc_a $\rrbracket$ $\rightarrow$ $\llbracket$ register; direct; indirect; data $\rrbracket$ $\rightarrow$ preinstruction A
508...
509\end{lstlisting}
510Here $\llbracket - \rrbracket$ is syntax denoting a vector.
511We 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.
512
513% One of these coercions opens up a proof obligation which needs discussing
514% Have lemmas proving that if an element is a member of a sub, then it is a member of a superlist, and so on
515The 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.
516The latter coercion is largely straightforward, however the former is not:
517\begin{lstlisting}
518coercion mk_subaddressing_mode:
519  $\forall$n.  $\forall$l: Vector addressing_mode_tag (S n).
520  $\forall$a: addressing_mode.
521  $\forall$p: bool_to_Prop (is_in ? l a). subaddressing_mode n l :=
522    mk_subaddressing_mode on a: addressing_mode to subaddressing_mode ? ?.
523\end{lstlisting}
524Using this coercion opens a proof obligation wherein we must prove that the \texttt{addressing\_mode\_tag} in correspondence with the \texttt{addressing\_mode} is a member of the \texttt{Vector} of permissible \texttt{addressing\_mode\_tag}s.
525This impels us to state and prove a number of auxilliary lemmas.
526For instance, we prove that if an \texttt{addressing\_mode\_tag} is a member of a \texttt{Vector}, and we possess another vector with additional elements, then the same \texttt{addressing\_mode\_tag} is a member of this vector.
527Using these lemmas, and Matita's automation, all proof obligations are solved easily.
528(Type checking the main \texttt{execute\_1} function, for instance, opens up over 200 proof obligations.)
529
530The machinery just described allows us to state in the type of a function what addressing modes that function expects.
531For instance, consider \texttt{set\_arg\_16}, which expects only a \texttt{DPTR}:
532\begin{lstlisting}
533definition set_arg_16: Status $\rightarrow$ Word $\rightarrow$ $\llbracket$ dptr $\rrbracket$ $\rightarrow$ Status ≝
534  $\lambda$s, v, a.
535   match a return $\lambda$x. bool_to_Prop (is_in ? $\llbracket$ dptr $\rrbracket$ x) $\rightarrow$ ? with
536     [ DPTR $\Rightarrow$ $\lambda$_: True.
537       let 〈 bu, bl 〉 := split $\ldots$ eight eight v in
538       let status := set_8051_sfr s SFR_DPH bu in
539       let status := set_8051_sfr status SFR_DPL bl in
540         status
541     | _ $\Rightarrow$ $\lambda$_: False.
542       match K in False with
543       [
544       ]
545     ] (subaddressing_modein $\ldots$ a).
546\end{lstlisting}
547All other cases are discharged by the catch-all at the bottom of the match expression.
548Attempting to match against another addressing mode not indicated in the type (for example, \texttt{REGISTER}) will produce a type-error.
549
550% Talk about extraction to O'Caml code, which hopefully will allow us to extract back to using polymorphic variants, or when extracting vectors we could extract using phantom types
551% Discuss alternative approaches, i.e. Sigma types to piece together smaller types into larger ones, as opposed to using a predicate to `cut out' pieces of a larger type, which is what we did
552
553%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
554% SECTION                                                                      %
555%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
556\subsection{I/O and timers}
557\label{subsect.i/o.timers}
558
559% `Real clock' for I/O and timers
560The O'Caml emulator has code for handling timers, asynchronous I/O and interrupts (these are not yet ported to the Matita emulator).
561All three of these features interact with each other in subtle ways.
562For instance, interrupts can `fire' when an input is detected on the processor's UART port, and, in certain modes, timers reset when a high signal is detected on one of the MCS-51's communication pins.
563
564To accurately model timers and I/O, we add an unbounded integral field \texttt{clock} to the central \texttt{status} record.
565This field is only logical, since it does not represent any quantity stored in the actual processor, and is used to keep track of the current processor time.
566Before every execution step, \texttt{clock} is incremented by the number of processor cycles that the instruction just fetched will take to execute.
567The processor then executes the instruction, followed by the code implementing the timers and I/O\footnote{Though it isn't fully specified by the manufacturer's data sheets if I/O is handled at the beginning or the end of each cycle.}. In order to model I/O, we also store in the status a
568We use \emph{continuation} as a description of the behaviour of the environment:
569\begin{lstlisting}
570type line =
571  [ `P1 of byte | `P3 of byte
572  | `SerialBuff of [ `Eight of byte | `Nine of BitVectors.bit * byte ]]
573type continuation =
574  [`In of time * line * epsilon * continuation] option *
575  [`Out of (time -> line -> time * continuation)]
576\end{lstlisting}
577At each moment, the second projection of the continuation $k$ describes how the environment will react to an output event performed in the future by the processor.
578If the processor at time $\tau$ starts an asynchronous output $o$ either on the P1 or P3 output lines, or on the UART, then the environment will receive the output at time $\tau'$.
579Moreover the status is immediately updated with the continuation $k'$ where $\pi_2(k)(\tau,o) = \langle \tau',k' \rangle$.
580
581Further, if $\pi_1(k) = \mathtt{Some}~\langle \tau',i,\epsilon,k'\rangle$, then at time $\tau'$ the environment will send the asynchronous input $i$ to the processor and the status will be updated with the continuation $k'$.
582This input will become visible to the processor only at time $\tau' + \epsilon$.
583
584The time required to perform an I/O operation is partially specified in the data sheets of the UART module.
585However, this computation is complex so we prefer to abstract over it.
586We therefore leave the computation of the delay time to the environment.
587
588We use only the P1 and P3 lines despite the MCS-51 having four output lines, P0--P3.
589This is because P0 and P2 become inoperable if the processor is equipped with XRAM (which we assume it is).
590
591The UART port can work in several modes, depending on the how the SFRs are set.
592In an asyncrhonous mode, the UART transmits eight bits at a time, using a ninth line for syncrhonization.
593In a syncrhonous mode the ninth line is used to transmit an additional bit.
594
595%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
596% SECTION                                                                      %
597%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
598\subsection{Computation of cost traces}
599\label{subsect.computation.cost.traces}
600
601As mentioned in Subsection~\ref{subsect.labels.pseudoinstructions} we introduced a notion of \emph{cost label}.
602Cost labels are inserted by the prototype C compiler in specific locations in the object code.
603Roughly, for those familiar with control flow graphs, they are inserted at the start of every basic block.
604
605Cost labels are used to calculate a precise costing for a program by marking the location of basic blocks.
606During the assembly phase, where labels and pseudoinstructions are eliminated, a map is generated associating cost labels with memory locations.
607This map is later used in a separate analysis which computes the cost of a program by traversing through a program, fetching one instruction at a time, and computing the cost of blocks.
608These block costings are stored in another map, and will later be passed back to the prototype compiler.
609
610%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
611% SECTION                                                                      %
612%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
613\section{Validation}
614\label{sect.validation}
615
616We spent considerable effort attempting to ensure that our formalisation is correct, that is, what we have formalised really is an accurate model of the MCS-51 microprocessor.
617
618First, we made use of multiple data sheets, each from a different semiconductor manufacturer.
619This helped us spot errors in the specification of the processor's instruction set, and its behaviour.
620
621The O'Caml prototype was especially useful for validation purposes.
622This is because we wrote a module for parsing and loading the Intel HEX file format.
623HEX is a standard format that all compilers targetting the MCS-51, and similar processors, produce.
624It is essentially a snapshot of the processor's code memory in compressed form.
625Using this, we were able to compile C programs with SDCC, an open source compiler, and load the resulting program directly into our emulator's code memory, ready for execution.
626Further, we are able to produce a HEX file from our emulator's code memory, for loading into third party tools.
627After each step of execution, we can print out both the instruction that had been executed, along with its arguments, and a snapshot of the processor's state, including all flags and register contents.
628For example:
629\begin{frametxt}
630\begin{verbatim}
631...
632
63308: mov 81 #07
634
635 Processor status:                               
636
637   ACC : 0 (00000000) B   : 0 (00000000) PSW : 0 (00000000)
638    with flags set as:
639     CY  : false   AC  : false FO  : false
640     RS1 : false   RS0 : false OV  : false
641     UD  : false   P   : false
642   SP  : 7 (00000111) IP  : 0 (00000000)
643   PC  : 8 (0000000000001000)
644   DPL : 0 (00000000) DPH : 0 (00000000) SCON: 0 (00000000)
645   SBUF: 0 (00000000) TMOD: 0 (00000000) TCON: 0 (00000000)
646   Registers:                                   
647    R0 : 0 (00000000) R1 : 0 (00000000) R2 : 0 (00000000)
648    R3 : 0 (00000000) R4 : 0 (00000000) R5 : 0 (00000000)
649    R6 : 0 (00000000) R7 : 0 (00000000)
650
651...
652\end{verbatim}
653\end{frametxt}
654Here, the traces indicates that the instruction \texttt{mov 81 \#07} has just been executed by the processor, which is now in the state indicated.
655These traces were useful in spotting anything that was `obviously' wrong with the execution of the program.
656
657Further, we used MCU 8051 IDE as a reference.
658Using our execution traces, we were able to step through a compiled program, one instruction at a time, in MCU 8051 IDE, and compare the resulting execution trace with the trace produced by our emulator.
659
660Our Matita formalisation was largely copied from the O'Caml source code, apart from changes related to addressing modes already mentioned.
661However, as the Matita emulator is executable, we could perform further validation by comparing the trace of a program's execution in the Matita emulator with the trace of the same program in the O'Caml emulator.
662
663%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
664% SECTION                                                                      %
665%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
666\section{Related work}
667\label{sect.related.work}
668There exists a large body of literature on the formalisation of microprocessors.
669The majority of it aims to prove correctness of the implementation of the microprocessor at the microcode or gate level.
670However, we are interested in providing a precise specification of the behaviour of the microprocessor in order to prove the correctness of a compiler which will target the processor.
671In particular, we are interested in intensional properties of the processor; precise timings of instruction execution in clock cycles.
672Moreover, in addition to formalising the interface of an MCS-51 processor, we have also built a complete MCS-51 ecosystem: the UART, the I/O lines, and hardware timers, along with an assembler.
673
674Similar work to ours can be found in~\cite{fox:trustworthy:2010}.
675Here, the authors describe the formalisation, in HOL4, of the ARMv7 instruction set architecture, and point to a good list of references to related work in the literature.
676This formalisation also considers the machine code level, as opposed to only considering an abstract assembly language.
677In particular, instruction decoding is explicitly modelled inside HOL4's logic.
678However, we go further in also providing an assembly language, complete with assembler, to translate instructions and pseudoinstruction to machine code.
679
680Further, in~\cite{fox:trustworthy:2010} the authors validated their formalisation by using development boards and random testing.
681However, we currently rely on non-exhaustive testing against a third party emulator.
682We leave similar exhaustive testing for future work.
683
684Executability is another key difference between our work and~\cite{fox:trustworthy:2010}.
685Our formalisation is executable: applying the emulation function to an input state eventually reduces to an output state that already satisfies the appropriate conditions.
686This is because Matita is based on a logic that internalizes conversion.
687In~\cite{fox:trustworthy:2010} the authors provide an automation layer to derive single step theorems: if the processor is in a particular state that satisfies some preconditions, then after execution of an instruction it will reside in another state satisfying some postconditions.
688We do not need single step theorems of this form.
689
690Our main difficulties resided in the non-uniformity of an old 8-bit architecture, in terms of the instruction set, addressing modes and memory models.
691In contrast, the ARM instruction set and memory model is relatively uniform, simplifying any formalisation considerably.
692
693Perhaps the closest project to CerCo is CompCert~\cite{leroy:formal:2009,leroy:formally:2009,blazy:formal:2006}.
694CompCert concerns the certification of an ARM compiler and includes a formalisation in Coq of a subset of ARM.
695Coq and Matita essentially share the same logic.
696
697Despite this similarity, the two formalisations do not have much in common.
698First, CompCert provides a formalisation at the assembly level (no instruction decoding), and this impels them to trust an unformalised assembler and linker, whereas we provide our own.
699I/O is also not considered at all in CompCert.
700Moreover an idealized abstract and uniform memory model is assumed, while we take into account the complicated overlapping memory model of the MCS-51 architecture.
701Finally, around 90 instructions of the 200+ offered by the processor are formalised in CompCert, and the assembly language is augmented with macro instructions that are turned into `real' instructions only during communication with the external assembler.
702Even from a technical level the two formalisations differ: while we tried to exploit dependent types as often as possible, CompCert largely sticks to the non-dependent fragment of Coq.
703
704In~\cite{atkey:coqjvm:2007} Atkey presents an executable specification of the Java virtual machine which uses dependent types.
705As we do, dependent types are used to remove spurious partiality from the model, and to lower the need for over-specifying the behaviour of the processor in impossible cases.
706Our use of dependent types will also help to maintain invariants when we prove the correctness of the CerCo prototype compiler.
707
708Finally, in~\cite{sarkar:semantics:2009} Sarkar et al provide an executable semantics for x86-CC multiprocessor machine code.
709This machine code exhibits a high degree of non-uniformity similar to the MCS-51.
710However, only a very small subset of the instruction set is considered, and they over-approximate the possibilities of unorthogonality of the instruction set, largely dodging the problems we had to face.
711
712Further, it seems that the definition of the decode function is potentially error prone.
713A small domain specific language of patterns is formalised in HOL4.
714This is similar to the specification language of the x86 instruction set found in manufacturer's data sheets.
715A decode function is implemented by copying lines from data sheets into the proof script.
716
717We are currently considering implementing a similar domain specific language in Matita.
718However, we would prefer to certify in Matita the compiler for this language.
719Data sheets could then be compiled down to the efficient code that we currently provide, instead of inefficiently interpreting the data sheets every time an instruction is executed.
720
721%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
722% SECTION                                                                      %
723%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
724\section{Conclusions}
725\label{sect.conclusions}
726
727\CSC{Tell what is NOT formalized/formalizable: the HEX parser/pretty printer
728 and/or the I/O procedure}
729\CSC{Decode: two implementations}
730\CSC{Discuss over-specification}
731
732- WE FORMALIZE ALSO I/O ETC. NOT ONLY THE INSTRUCTION SELECTION (??)
733  How to test it? Specify it?
734
735\bibliography{itp-2011.bib}
736
737\newpage
738
739\appendix
740
741\section{Listing of main O'Caml functions}
742\label{sect.listing.main.ocaml.functions}
743
744\subsubsection{From \texttt{ASMInterpret.ml(i)}}
745
746\begin{center}
747\begin{tabular*}{\textwidth}{p{3cm}@{\quad}p{9cm}}
748Name & Description \\
749\hline
750\texttt{assembly} & Assembles an abstract syntax tree representing an 8051 assembly program into a list of bytes, its compiled form. \\
751\texttt{initialize} & Initializes the emulator status. \\
752\texttt{load} & Loads an assembled program into the emulator's code memory. \\
753\texttt{fetch} & Fetches the next instruction, and automatically increments the program counter. \\
754\texttt{execute} & Emulates the processor.  Accepts as input a function that pretty prints the emulator status after every emulation loop. \\
755\end{tabular*}
756\end{center}
757
758\subsubsection{From \texttt{ASMCosts.ml(i)}}
759
760\begin{center}
761\begin{tabular*}{\textwidth}{p{3cm}@{\quad}p{9cm}}
762Name & Description \\
763\hline
764\texttt{compute} & Computes a map associating costings to basic blocks in the program.
765\end{tabular*}
766\end{center}
767
768\subsubsection{From \texttt{IntelHex.ml(i)}}
769
770\begin{center}
771\begin{tabular*}{\textwidth}{p{3cm}@{\quad}p{9cm}}
772Name & Description \\
773\hline
774\texttt{intel\_hex\_of\_file} & Reads in a file and parses it if in Intel IHX format, otherwise raises an exception. \\
775\texttt{process\_intel\_hex} & Accepts a parsed Intel IHX file and populates a hashmap (of the same type as code memory) with the contents.
776\end{tabular*}
777\end{center}
778
779\subsubsection{From \texttt{Physical.ml(i)}}
780
781\begin{center}
782\begin{tabular*}{\textwidth}{p{3cm}@{\quad}p{9cm}}
783Name & Description \\
784\hline
785\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. \\
786\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. \\
787\texttt{dec} & Decrements an eight bit bitvector with underflow, if necessary. \\
788\texttt{inc} & Increments an eight bit bitvector with overflow, if necessary.
789\end{tabular*}
790\end{center}
791
792\newpage
793
794\section{Listing of main Matita functions}
795\label{sect.listing.main.matita.functions}
796
797\subsubsection{From \texttt{Arithmetic.ma}}
798
799\begin{center}
800\begin{tabular*}{\textwidth}{p{3cm}p{9cm}}
801Title & Description \\
802\hline
803\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. \\
804\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. \\
805\texttt{half\_add} & Performs a standard half addition on bitvectors, returning the result and carry bit. \\
806\texttt{full\_add} & Performs a standard full addition on bitvectors and a carry bit, returning the result and a carry bit.
807\end{tabular*}
808\end{center}
809
810\subsubsection{From \texttt{Assembly.ma}}
811
812\begin{center}
813\begin{tabular*}{\textwidth}{p{3cm}p{9cm}}
814Title & Description \\
815\hline
816\texttt{assemble1} & Assembles a single 8051 assembly instruction into its memory representation. \\
817\texttt{assemble} & Assembles an 8051 assembly program into its memory representation.\\
818\texttt{assemble\_unlabelled\_program} &\\& Assembles a list of (unlabelled) 8051 assembly instructions into its memory representation.
819\end{tabular*}
820\end{center}
821
822\subsubsection{From \texttt{BitVectorTrie.ma}}
823
824\begin{center}
825\begin{tabular*}{\textwidth}{p{3cm}p{9cm}}
826Title & Description \\
827\hline
828\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. \\
829\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.
830\end{tabular*}
831\end{center}
832
833\subsubsection{From \texttt{DoTest.ma}}
834
835\begin{center}
836\begin{tabular*}{\textwidth}{p{3cm}p{9cm}}
837Title & Description \\
838\hline
839\texttt{execute\_trace} & Executes an assembly program for a fixed number of steps, recording in a trace which instructions were executed.
840\end{tabular*}
841\end{center}
842
843\subsubsection{From \texttt{Fetch.ma}}
844
845\begin{center}
846\begin{tabular*}{\textwidth}{p{3cm}p{9cm}}
847Title & Description \\
848\hline
849\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. \\
850\end{tabular*}
851\end{center}
852
853\subsubsection{From \texttt{Interpret.ma}}
854
855\begin{center}
856\begin{tabular*}{\textwidth}{p{3cm}p{9cm}}
857Title & Description \\
858\hline
859\texttt{execute\_1} & Executes a single step of an 8051 assembly program. \\
860\texttt{execute} & Executes a fixed number of steps of an 8051 assembly program.
861\end{tabular*}
862\end{center}
863
864\subsubsection{From \texttt{Status.ma}}
865
866\begin{center}
867\begin{tabular*}{\textwidth}{p{3cm}p{9cm}}
868Title & Description \\
869\hline
870\texttt{load} & Loads an assembled 8051 assembly program into code memory.
871\end{tabular*}
872\end{center}
873\end{document}
Note: See TracBrowser for help on using the repository browser.