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

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

First draft of report finished.

File size: 25.9 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},
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\\
64Intel 8051/8052 emulator prototype, and formalisation in Matita}
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:\\
79Claudio Sacerdoti Coen and Dominic P. Mulligan
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
101We also briefly summarise the Intel 8051/8052 processor architecture, our target processor model for the \textsf{CerCo} project.
102\newpage
103
104\tableofcontents
105
106\newpage
107
108\section{Task}
109\label{sect.task}
110
111The Grant Agreement states the D4.1/D4.2 deliverables consist of the following tasks:
112
113\begin{quotation}
114\textbf{Executable Formal Semantics of Machine Code}: Formal definition of the semantics of the target language.
115The semantics will be given in a functional (and hence executable) form, useful for testing, validation and project assessment.
116\end{quotation}
117
118\begin{quotation}
119\textbf{CIC encoding: Back-end}: Functional Specification in the internal language of the Proof Assistant (the Calculus of Inductive Construction) of the back end of the compiler.
120This unit is meant to be composable with the front-end of deliverable D3.2, to obtain a full working compiler for Milestone M2.
121A first validation of the design principles and implementation choices for the Untrusted Cost-annotating OCaml Compiler D2.2 is achieved and reported in the deliverable, possibly triggering updates of the Untrusted Cost-annotating OCaml Compiler sources.
122\end{quotation}
123We now report on our implementation of these deliverables.
124
125\section{A brief overview of the target processor}
126\label{sect.brief.overview.target.processor}
127
128The MCS-51 is an eight bit microprocessor introduced by Intel in the late 1970s.
129Commonly called the 8051, in the three decades since its introduction the processor has become a highly popular target for embedded systems engineers.
130Further, 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).
131
132The 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.
133For 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.
134An open source emulator for the processor, MCU8051 IDE, is also available.
135
136The 8051 has a relatively straightforward architecture, unencumbered by advanced features of modern processors, making it an ideal target for formalisation.
137A high-level overview of the processor's memory layout is provided in Figure~\ref{fig.memory.layout}.
138
139Processor RAM is divided into numerous segments, with the most prominent division being between internal and (optional) external memory.
140Internal 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.
141Internal RAM (IRAM) is further divided into a eight general purpose bit-addressable registers (R0--R7).
142These sit in the first eight bytes of IRAM, though can be programmatically `shifted up' as needed.
143Bit memory, followed by a small amount of stack space resides in the memory space immediately after the register banks.
144What remains of the IRAM may be treated as general purpose memory.
145A schematic view of IRAM layout is provided in Figure~\ref{fig.iram.layout}.
146
147External RAM (XRAM), limited to 64 kilobytes, is optional, and may be provided on or off chip, depending on the manufacturer.
148XRAM is accessed using a dedicated instruction.
149External code memory (XCODE) is often stored in the form of an EPROM, and limited to 64 kilobytes in size.
150However, depending on the particular manufacturer and processor model, a dedicated on-die read-only memory area for program code (ICODE) may also be supplied.
151
152Memory may be addressed in numerous ways: immediate, direct, indirect, external direct and code indirect.
153As 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.
154For 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.
155
156The 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.
157Further, the processor possesses two eight bit general purpose accumulators, A and B.
158
159Communication with the device is facilitated by an onboard UART serial port, and associated serial controller, which can operate in numerous modes.
160Serial baud rate is determined by one of two sixteen bit timers included with the 8051, which can be set to multiple modes of operation.
161(The 8052 provides an additional sixteen bit timer.)
162As an additional method of communication, the 8051 also provides a four byte bit-addressable input-output port.
163
164The programmer may take advantage of the interrupt mechanism that the processor provides.
165This 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.
166
167Interrupts 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.
168However, interrupts may be set to one of two priorities: low and high.
169The 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.
170
171The 8051 has interrupts disabled by default.
172The programmer is free to handle serial input and output manually, by poking serial flags in the SFRs.
173Similarly, `exceptional circumstances' that would otherwise trigger an interrupt on more modern processors, for example, division by zero, are also signalled by setting flags.
174
175\begin{figure}[t]
176\begin{center}
177\includegraphics[scale=0.5]{memorylayout.png}
178\end{center}
179\caption{High level overview of the 8051 memory layout}
180\label{fig.memory.layout}
181\end{figure}
182
183\begin{figure}[t]
184\begin{center}
185\includegraphics[scale=0.5]{iramlayout.png}
186\end{center}
187\caption{Schematic view of 8051 IRAM layout}
188\label{fig.iram.layout}
189\end{figure}
190
191\section{The emulator in O'Caml}
192\label{sect.emulator.in.ocaml}
193
194We discuss decisions made during the design of the prototype O'Caml emulator.
195
196\subsection{Lack of orthogonality in instruction set}
197\label{subsect.lack.orthogonality.instruction.set}
198
199The instruction set of 8051 assembly is highly irregular.
200For instance, consider the MOV instruction, which implements a data transfer between two memory locations, which takes eighteen possible combinations of addressing modes.
201
202We handle this problem by introducing `unions' of types, using O'Caml's polymorphic variants feature:
203\begin{quote}
204\begin{lstlisting}
205type ('a, 'b) union2 = [ `U1 of 'a | `U2 of 'b ]
206\end{lstlisting}
207\end{quote}
208(We also introduce \texttt{union3} and \texttt{union6}, which suffice for our purposes.)
209
210Using these union types, we can rationalise the inductive type encoding the assembly instruction set.
211For instance:
212\begin{quote}
213\begin{lstlisting}
214type 'addr preinstruction =
215...
216  | `XRL of (acc * [ data | reg | direct | indirect ],
217             direct * [ acc | data ]) union2
218...
219\end{lstlisting}
220\end{quote}
221That is, the \texttt{XRL} instruction\footnote{Exclusive disjunction.} take either the accumulator A as its first argument, followed by data with one of data, register, direct or indirect addressing modes, or takes data with a direct addressing mode as its first argument, with either the accumulator A or data with the data addressing mode as its second argument.
222
223Further, all functions that must pattern match against the \texttt{(pre)instruction} inductive type are also simplified using this technique.
224Using O'Caml's ability to perform `deep pattern' matches, we may pattern match against \texttt{`XRL(`U1(arg1, arg2))} and have the guarantee that \texttt{arg1} takes the form \texttt{`ACC\_A}.
225
226\subsection{Pseudo-instructions and labels}
227\label{subsect.pseudo-instructions.labels}
228
229Per the description of Deliverable D4.1 in the Grant Agreement above, the 8051 emulator must eventually interface with the C compiler frontend of Deliverable D3.2, produced in Paris.
230After consultation, it was found that the design of the compiler frontend could be simplified considerably with the introduction of \emph{pseudoinstructions} and labels.
231
232We introduce three new pseudoinstructions---\texttt{Jump}, \texttt{Call}, and \texttt{Mov}---corresponding to unconditional jumps, procedure calls and data transfers respectively.
233We also `promote' all unlabeled conditional jumps in 8051 assembly to labeled pseudojumps; one can now jump to a label conditionally, as opposed to jumping to a fixed relative offset.
234Further, we introduce labels for jumping to, and cost annotations, used by the Paris team.
235
236The three new pseudoinstructions, along with the promoted conditional jumps, allow the Paris team to abstract away from the differences between different types of unconditional jump (the 8051 has three different sorts, depending on the length of the jump), as well as abstract away the differences between memory transfers and calls.
237However, the emulator must perform an expansion stage, during which pseudoinstructions are translated to `real' 8051 assembly instructions.
238
239The introduction of labeled conditional jumps slightly complicates our type of abstract syntax for 8051 assembly.
240We define an inductive type representing conditional jumps in 8051 assembly code, parameterised by a type representing relative offsets:s
241\begin{quote}
242\begin{lstlisting}
243type 'addr jump =
244  [ `JC of 'addr
245  | `JNC of 'addr
246...
247\end{lstlisting}
248\end{quote}
249An inductive type of preinstructions is defined, which is also parameterised by a type representing relative offsets in assembly code, and incorporates the inductive type of conditional jumps:
250\begin{quote}
251\begin{lstlisting}
252type 'addr preinstruction =
253  [ `ADD of acc * [ reg | direct | indirect | data ]
254...
255  | 'addr jump
256...
257\end{lstlisting}
258\end{quote}
259A type representing instructions is defined, choosing a concrete type for relative offsets:
260\begin{quote}
261\begin{lstlisting}
262type instruction = rel preinstruction
263\end{lstlisting}
264\end{quote}
265Here, \texttt{rel} is a type which `wraps up' a byte.
266Finally, this type of instructions is incorporated into a type of labelled instructions:
267\begin{quote}
268\begin{lstlisting}
269type labelled_instruction =
270  [ instruction
271  | `Cost of string
272  | `Label of string
273  | `Jmp of string
274  | `Call of string
275  | `Mov of dptr * string
276  | `WithLabel of [`Label of string] jump
277]
278\end{lstlisting}
279\end{quote}
280Throughout, we make heavy use of polymorphic variants to deal with issues relating to subtyping.
281
282As mentioned, the emulator must now handle an additional expansion stage, removing pseudoinstructions in favour of real, 8051 assembly instructions.
283This is relatively straightforward, and is done in two stages.
284
285The first stage consists of iterating over an assembly program, building a dictionary of all labels and their position in the program.
286The second stage consists of iterating over the same program and replacing all pseudojumps (both conditional and unconditional) with an 8051 jump to the requisite computed offset.
287One subtletly persists, however.
288
289The 8051 has three different types of unconditional jump, depending on the length of the jump to be used: \texttt{AJMP}, \texttt{JMP} and \texttt{LJMP}.
290The instructions \texttt{AJMP} and \texttt{JMP} are short jumps, whereas \texttt{LJMP} is a long jump, capable of reaching anywhere in the program.
291At the moment, the second pass of the expansion stage replaces all unconditional pseudojumps with a \texttt{LJMP} for simplicity.
292We do, however, plan to improve this process for efficiency reasons, expanding to shorter jumps where feasible.
293
294\subsection{Validation}
295\label{subsect.validation}
296
297In validating the design and implementation of the O'Caml emulator we used two tactics:
298\begin{enumerate}
299\item
300Use 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).
301We found typographic errors in manufacturer's data sheets which were resolved by consulting an alternative sheet.
302\item
303Use of reference compilers and emulators.
304The operation of the emulator was manually tested by reference to \textsc{mcu 8051 ide}, an emulator for the 8051 series processor.
305A number of small C programs were compiled in SDCC\footnote{See the \texttt{GCC} directory for a selection of them.}.
306The resulting IHX files were disassembled by \textsc{mcu 8051 ide}.
307(IHX files are a standard format for transferring compiled assembly code onto an 8051 series processor, produced by SDCC and all other compilers that target that 8051.)
308The status changes in both emulators were then compared.
309
310For 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.
311\end{enumerate}
312
313As 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}.
314
315\section{The emulator in Matita}
316\label{sect.emulator.in.matita}
317
318The O'Caml emulator served as a testbed and prototype for an emulator written in the internal language of the Matita proof assistant.
319We describe our work porting the emulator to Matita, especially where the design of the Matita emulator differs from that of the O'Caml version.
320
321\subsection{What we do not implement}
322\label{subsect.what.we.do.not.implement}
323
324Our O'Caml 8051 emulator provides functions for reading and parsing Intel IHX format files.
325We do not implement these functions in the Matita emulator, as Matita provides no means of input or output.
326
327\subsection{Auxilliary data structures and libraries}
328\label{subsect.auxilliary.data.structures.and.libraries}
329
330A small library of data structures was written, along with basic functions operating over them.
331Implemented data structures include: Booleans, option types, lists, Cartesian products, Natural numbers, fixed-length vectors, and sparse tries.
332
333Our type of vectors, in particular, makes heavy use of dependent types.
334Probing vectors is `type safe' for instance: we cannot index into a vector beyond the vector's length.
335
336We represent bits as Boolean values.
337Nibbles, bytes, words, and so on, are represented as fixed length (bit)vectors of the requisite length.
338
339\subsection{The emulator state}
340\label{subsect.emulator.state}
341
342We represent all processor memory in the Matita emulator as a sparse (bitvector)trie:
343
344\begin{quote}
345\begin{lstlisting}
346ninductive BitVectorTrie (A: Type[0]): Nat $\rightarrow$ Type[0] ≝
347  Leaf: A $\rightarrow$ BitVectorTrie A Z
348| Node: ∀n: Nat. BitVectorTrie A n $\rightarrow$ BitVectorTrie A n $\rightarrow$ BitVectorTrie A (S n)
349| Stub: ∀n: Nat. BitVectorTrie A n.
350\end{lstlisting}
351\end{quote}
352
353Nodes are addressed by a bitvector index, representing a path through the tree.
354At any point in the tree, a \texttt{Stub} may be inserted, representing a `hole' in the tree.
355All 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.
356
357We probe a trie with the \texttt{lookup} function.
358This takes an additional argument representing the value to be returned should a stub, representing uninitialised data, be encountered during traversal.
359
360Like the O'Caml emulator, we use a record to represent processor state:
361
362\begin{quote}
363\begin{lstlisting}
364nrecord Status: Type[0] ≝
365{
366  code_memory: BitVectorTrie Byte sixteen;
367  low_internal_ram: BitVectorTrie Byte seven;
368  high_internal_ram: BitVectorTrie Byte seven;
369  external_ram: BitVectorTrie Byte sixteen;
370 
371  program_counter: Word;
372 
373  special_function_registers_8051: Vector Byte nineteen;
374  special_function_registers_8052: Vector Byte five;
375 
376  ...
377}.
378\end{lstlisting}
379\end{quote}
380
381However, 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.
382We then provide functions that index into the respective vector to `get' and `set' the respective SFRs.
383This is due to record typechecking in Matita being slow for large records.
384
385\subsection{Dealing with partiality}
386\label{subsect.dealing.with.partiality}
387
388The O'Caml 8051 emulator makes use of a number of partial functions.
389These 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.
390There are a number of possible reasons for this:
391\begin{enumerate}
392\item
393\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.
394An 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.
395\item
396\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.
397In this respect, we used \texttt{assert false} in a similar way to the previously described use of incomplete pattern analysis.
398\item
399\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.
400\end{enumerate}
401
402The three 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.
403Items 1 and 2 belong to the former class, Item 3 to the latter.
404
405Clearly Items 1 and 2 above must be addressed in the Matita formalisation.
406Item 2 is solved through extensive use of dependent types.
407Indexing into lists and vectors, for instance, is always `type safe', as we provide probing functions with strong dependent types.
408
409Item 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.
410We employ a technique that implements the latter idea.
411This is discussed in Subsection~\ref{subsect.addressing.modes.use.of.dependent.types}.
412
413To solve Item 3 above in the Matita formalisation of the emulator, we introduce an axiom \texttt{not\_implemented} of type \texttt{False}.
414When the emulator attempts to use an unimplemented feature, we introduce a metavariable, corresponding to an open proof obligation.
415These obligations are closed by performing a case analysis over \texttt{not\_implemented}.
416
417\subsection{Addressing modes: use of dependent types}
418\label{subsect.addressing.modes.use.of.dependent.types}
419
420We provide an inductive data type representing all possible addressing modes of 8051 assembly.
421This is the type that functions will pattern match against.
422
423\begin{quote}
424\begin{lstlisting}
425ninductive addressing_mode: Type[0] ≝
426  DIRECT: Byte $\rightarrow$ addressing_mode
427| INDIRECT: Bit $\rightarrow$ addressing_mode
428...
429\end{lstlisting}
430\end{quote}
431However, we also wish to express in the type of our functions the \emph{impossibility} of pattern matching against certain constructors.
432In order to do this, we introduce an inductive type of addressing mode `tags'.
433The constructors of \texttt{addressing\_mode\_tag} are in one-one correspondence with the constructors of \texttt{addressing\_mode}:
434\begin{quote}
435\begin{lstlisting}
436ninductive addressing_mode_tag : Type[0] ≝
437  direct: addressing_mode_tag
438| indirect: addressing_mode_tag
439...
440\end{lstlisting}
441\end{quote}
442We then provide a function that checks whether an \texttt{addressing\_mode} is `morally' an \texttt{addressing\_mode\_tag}, as follows:
443\begin{quote}
444\begin{lstlisting}
445nlet rec is_a (d:addressing_mode_tag) (A:addressing_mode) on d ≝
446  match d with
447   [ direct $\Rightarrow$ match A with [ DIRECT _ $\Rightarrow$ true | _ $\Rightarrow$ false ]
448   | indirect $\Rightarrow$ match A with [ INDIRECT _ $\Rightarrow$ true | _ $\Rightarrow$ false ]
449...
450\end{lstlisting}
451\end{quote}
452We also extend this check to vectors of \texttt{addressing\_mode\_tag}'s in the obvious manner:
453\begin{quote}
454\begin{lstlisting}
455nlet rec is_in (n: Nat) (l: Vector addressing_mode_tag n) (A:addressing_mode) on l ≝
456 match l return $\lambda$m.$\lambda$_ :Vector addressing_mode_tag m.Bool with
457  [ VEmpty $\Rightarrow$ false
458  | VCons m he (tl: Vector addressing_mode_tag m) $\Rightarrow$
459     is_a he A $\vee$ is_in ? tl A ].
460\end{lstlisting}
461\end{quote}
462Here \texttt{VEmpty} and \texttt{VCons} are the two constructors of the \texttt{Vector} data type, and $\mathtt{\vee}$ is inclusive disjunction on Booleans.
463\begin{quote}
464\begin{lstlisting}
465nrecord subaddressing_mode (n: Nat) (l: Vector addressing_mode_tag (S n)) : Type[0] ≝
466{
467  subaddressing_modeel :> addressing_mode;
468  subaddressing_modein: bool_to_Prop (is_in ? l subaddressing_modeel)
469}.
470\end{lstlisting}
471\end{quote}
472We can now provide an inductive type of preinstructions with precise typings:
473\begin{quote}
474\begin{lstlisting}
475ninductive preinstruction (A: Type[0]): Type[0] ≝
476   ADD: $\llbracket$ acc_a $\rrbracket$ $\rightarrow$ $\llbracket$ register; direct; indirect; data $\rrbracket$ $\rightarrow$ preinstruction A
477 | ADDC: $\llbracket$ acc_a $\rrbracket$ $\rightarrow$ $\llbracket$ register; direct; indirect; data $\rrbracket$ $\rightarrow$ preinstruction A
478...
479\end{lstlisting}
480\end{quote}
481Here $\llbracket - \rrbracket$ is syntax denoting a vector.
482We 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.
483
484The 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.
485The previous machinery allows us to state in the type of a function what addressing modes that function expects.
486For instance, consider \texttt{set\_arg\_16}, which expects only a \texttt{DPTR}:
487\begin{quote}
488\begin{lstlisting}
489ndefinition set_arg_16: Status $\rightarrow$ Word $\rightarrow$ $\llbracket$ dptr $\rrbracket$ $\rightarrow$ Status ≝
490  $\lambda$s, v, a.
491   match a return $\lambda$x. bool_to_Prop (is_in ? $\llbracket$ dptr $\rrbracket$ x) $\rightarrow$ ? with
492     [ DPTR $\Rightarrow$ $\lambda$_: True.
493       let 〈 bu, bl 〉 := split $\ldots$ eight eight v in
494       let status := set_8051_sfr s SFR_DPH bu in
495       let status := set_8051_sfr status SFR_DPL bl in
496         status
497     | _ $\Rightarrow$ $\lambda$_: False.
498       match K in False with
499       [
500       ]
501     ] (subaddressing_modein $\ldots$ a).
502\end{lstlisting}
503\end{quote}
504All other cases are discharged by the catch-all at the bottom of the match expression.
505Attempting to match against another addressing mode not indicated in the type (for example, \texttt{REGISTER}) will produce a type-error.
506
507\end{document}
Note: See TracBrowser for help on using the repository browser.