Changeset 495


Ignore:
Timestamp:
Feb 11, 2011, 3:16:15 PM (6 years ago)
Author:
mulligan
Message:

more added

File:
1 edited

Legend:

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

    r494 r495  
    11\documentclass{llncs}
    22
     3\usepackage{amsfonts}
     4\usepackage{amsmath}
     5\usepackage{amssymb}
    36\usepackage[english]{babel}
     7\usepackage{color}
    48\usepackage{graphicx}
     9\usepackage[utf8x]{inputenc}
     10\usepackage{listings}
     11\usepackage{stmaryrd}
     12\usepackage{url}
     13
     14\lstdefinelanguage{matita-ocaml}
     15  {keywords={ndefinition,ncoercion,nlemma,ntheorem,nremark,ninductive,nrecord,nqed,nlet,let,in,rec,match,return,with,Type,try},
     16   morekeywords={[2]nwhd,nnormalize,nelim,ncases,ndestruct},
     17   morekeywords={[3]type,of},
     18   mathescape=true,
     19  }
     20\lstset{language=matita-ocaml,basicstyle=\small\tt,columns=flexible,breaklines=false,
     21        keywordstyle=\color{red}\bfseries,
     22        keywordstyle=[2]\color{blue},
     23        keywordstyle=[3]\color{blue}\bfseries,
     24        commentstyle=\color{green},
     25        stringstyle=\color{blue},
     26        showspaces=false,showstringspaces=false}
     27\lstset{extendedchars=false}
     28\lstset{inputencoding=utf8x}
     29\DeclareUnicodeCharacter{8797}{:=}
     30\DeclareUnicodeCharacter{10746}{++}
     31\DeclareUnicodeCharacter{9001}{\ensuremath{\langle}}
     32\DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}}
    533
    634\author{Claudio Sacerdoti Coen \and Dominic P. Mulligan}
     
    1543
    1644\begin{abstract}
    17 We summary the recent encoding of an executable formal model of the 8051/8052 microprocessor within Matita's internal logic.
     45We summarise our formalisation of an emulator for the MCS-51 microprocessor in the Matita proof assistant.
     46The MCS-51 is a widely used 8-bit microprocessor, especially popular in embedded devices.
     47
     48We proceeded in two stages, first implementing in O'Caml a prototype emulator, where bugs could be `ironed out' quickly.
     49We then ported our O'Caml emulator to Matita's internal language.
     50Though mostly straight-forward, this porting presented multiple problems.
     51Of particular interest is how we handle the extreme non-orthoganality of the MSC-51's instruction set.
     52In O'Caml, this was handled through heavy use of polymorphic variants.
     53In Matita, we achieve the same effect through a novel use of dependent types.
     54
     55Both the O'Caml and Matita emulators are `executable'.
     56Assembly programs may be animated within Matita, producing a trace of instructions executed.
     57
     58Our formalisation is a major component of the ongoing EU-funded CerCo project.
    1859\end{abstract}
    1960
     
    125166% SECTION                                                                      %
    126167%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    127 \section{Development strategy}
    128 \label{sect.development.strategy}
     168\section{From O'Caml prototype to Matita formalisation}
     169\label{sect.from.o'caml.prototype.matita.formalisation}
     170
     171Our implementation followed a two-layered approach.
     172
     173\paragraph{O'Caml prototype}
     174Our implementation began with an emulator written in O'Caml.
     175This served the purpose of allowing us to `iron out' any bugs in the design of the emulator within a more permissive language.
     176Further,
     177
     178\paragraph{Matita formalisation}
    129179
    130180%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     
    146196\label{subsect.putting.dependent.types.to.work}
    147197
     198We provide an inductive data type representing all possible addressing modes of 8051 assembly.
     199This is the type that functions will pattern match against.
     200
     201\begin{quote}
     202\begin{lstlisting}
     203ninductive addressing_mode: Type[0] ≝
     204  DIRECT: Byte $\rightarrow$ addressing_mode
     205| INDIRECT: Bit $\rightarrow$ addressing_mode
     206...
     207\end{lstlisting}
     208\end{quote}
     209However, we also wish to express in the type of our functions the \emph{impossibility} of pattern matching against certain constructors.
     210In order to do this, we introduce an inductive type of addressing mode `tags'.
     211The constructors of \texttt{addressing\_mode\_tag} are in one-one correspondence with the constructors of \texttt{addressing\_mode}:
     212\begin{quote}
     213\begin{lstlisting}
     214ninductive addressing_mode_tag : Type[0] ≝
     215  direct: addressing_mode_tag
     216| indirect: addressing_mode_tag
     217...
     218\end{lstlisting}
     219\end{quote}
     220We then provide a function that checks whether an \texttt{addressing\_mode} is `morally' an \texttt{addressing\_mode\_tag}, as follows:
     221\begin{quote}
     222\begin{lstlisting}
     223nlet rec is_a (d:addressing_mode_tag) (A:addressing_mode) on d ≝
     224  match d with
     225   [ direct $\Rightarrow$ match A with [ DIRECT _ $\Rightarrow$ true | _ $\Rightarrow$ false ]
     226   | indirect $\Rightarrow$ match A with [ INDIRECT _ $\Rightarrow$ true | _ $\Rightarrow$ false ]
     227...
     228\end{lstlisting}
     229\end{quote}
     230We also extend this check to vectors of \texttt{addressing\_mode\_tag}'s in the obvious manner:
     231\begin{quote}
     232\begin{lstlisting}
     233nlet rec is_in (n: Nat) (l: Vector addressing_mode_tag n) (A:addressing_mode) on l ≝
     234 match l return $\lambda$m.$\lambda$_ :Vector addressing_mode_tag m.Bool with
     235  [ VEmpty $\Rightarrow$ false
     236  | VCons m he (tl: Vector addressing_mode_tag m) $\Rightarrow$
     237     is_a he A $\vee$ is_in ? tl A ].
     238\end{lstlisting}
     239\end{quote}
     240Here \texttt{VEmpty} and \texttt{VCons} are the two constructors of the \texttt{Vector} data type, and $\mathtt{\vee}$ is inclusive disjunction on Booleans.
     241\begin{quote}
     242\begin{lstlisting}
     243nrecord subaddressing_mode (n: Nat) (l: Vector addressing_mode_tag (S n)) : Type[0] ≝
     244{
     245  subaddressing_modeel :> addressing_mode;
     246  subaddressing_modein: bool_to_Prop (is_in ? l subaddressing_modeel)
     247}.
     248\end{lstlisting}
     249\end{quote}
     250We can now provide an inductive type of preinstructions with precise typings:
     251\begin{quote}
     252\begin{lstlisting}
     253ninductive preinstruction (A: Type[0]): Type[0] ≝
     254   ADD: $\llbracket$ acc_a $\rrbracket$ $\rightarrow$ $\llbracket$ register; direct; indirect; data $\rrbracket$ $\rightarrow$ preinstruction A
     255 | ADDC: $\llbracket$ acc_a $\rrbracket$ $\rightarrow$ $\llbracket$ register; direct; indirect; data $\rrbracket$ $\rightarrow$ preinstruction A
     256...
     257\end{lstlisting}
     258\end{quote}
     259Here $\llbracket - \rrbracket$ is syntax denoting a vector.
     260We 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.
     261
     262The 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.
     263The previous machinery allows us to state in the type of a function what addressing modes that function expects.
     264For instance, consider \texttt{set\_arg\_16}, which expects only a \texttt{DPTR}:
     265\begin{quote}
     266\begin{lstlisting}
     267ndefinition set_arg_16: Status $\rightarrow$ Word $\rightarrow$ $\llbracket$ dptr $\rrbracket$ $\rightarrow$ Status ≝
     268  $\lambda$s, v, a.
     269   match a return $\lambda$x. bool_to_Prop (is_in ? $\llbracket$ dptr $\rrbracket$ x) $\rightarrow$ ? with
     270     [ DPTR $\Rightarrow$ $\lambda$_: True.
     271       let 〈 bu, bl 〉 := split $\ldots$ eight eight v in
     272       let status := set_8051_sfr s SFR_DPH bu in
     273       let status := set_8051_sfr status SFR_DPL bl in
     274         status
     275     | _ $\Rightarrow$ $\lambda$_: False.
     276       match K in False with
     277       [
     278       ]
     279     ] (subaddressing_modein $\ldots$ a).
     280\end{lstlisting}
     281\end{quote}
     282All other cases are discharged by the catch-all at the bottom of the match expression.
     283Attempting to match against another addressing mode not indicated in the type (for example, \texttt{REGISTER}) will produce a type-error.
     284
    148285%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    149286% SECTION                                                                      %
Note: See TracChangeset for help on using the changeset viewer.