Changeset 375


Ignore:
Timestamp:
Dec 6, 2010, 10:03:03 AM (9 years ago)
Author:
mulligan
Message:

More work on report.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Report/report.tex

    r371 r375  
    77\usepackage{amssymb}
    88\usepackage[english]{babel}
     9\usepackage[utf8x]{inputenc}
     10\usepackage{listings}
    911\usepackage{url}
    1012
     
    1416PROGRAMME\\
    1517\vspace*{1cm}Project FP7-ICT-2009-C-243881 \cerco{}}
     18
     19\lstdefinelanguage{matita}
     20  {keywords={ndefinition,nlemma,ntheorem,nremark,ninductive,nrecord,nqed,nlet,rec,match,with,Type},
     21   morekeywords={[2]nwhd,nnormalize,nelim,ncases,ndestruct},
     22   mathescape=true,
     23  }
     24
     25\lstset{language=matita,basicstyle=\small\tt,columns=flexible,breaklines=false,
     26        keywordstyle=\color{red}\bfseries,
     27        keywordstyle=[2]\color{blue},
     28        commentstyle=\color{green},
     29        stringstyle=\color{blue},
     30        showspaces=false,showstringspaces=false}
     31
     32\lstset{extendedchars=false}
     33\lstset{inputencoding=utf8x}
     34\DeclareUnicodeCharacter{8797}{:=}
     35\DeclareUnicodeCharacter{10746}{++}
     36\DeclareUnicodeCharacter{9001}{\ensuremath{\langle}}
     37\DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}}
    1638
    1739\date{}
     
    158180\label{sect.emulator.in.matita}
    159181
     182\subsection{What we implement}
     183\label{subsect.what.we.implement}
     184
     185Our O'Caml 8051 emulator provides functions for reading and parsing Intel IHX format files.
     186We do not implement these functions in the Matita emulator, as Matita provides no means of input or output.
     187Instead, the Matita emulator is initialised with a call to \texttt{load}, which takes as input a list of bytes representing the compiled IHX file.
     188The use must manually
     189
     190\subsection{Auxilliary data structures and libraries}
     191\label{subsect.auxilliary.data.structures.and.libraries}
     192
     193A small library of data structures was written, along with basic functions operating over them.
     194Implemented data structures include: Booleans, option types, lists, Cartesian products, Natural numbers, fixed-length vectors, and sparse tries.
     195
     196We represent bits as Boolean values.
     197Nibbles, bytes, words, and so on, are represented as fixed length (bit)vectors of the requisite length.
     198
     199\subsection{The emulator state}
     200\label{subsect.emulator.state}
     201
     202\begin{quote}
     203\begin{lstlisting}
     204nrecord Status: Type[0] ≝
     205{
     206  code_memory: BitVectorTrie Byte sixteen;
     207  low_internal_ram: BitVectorTrie Byte seven;
     208  high_internal_ram: BitVectorTrie Byte seven;
     209  external_ram: BitVectorTrie Byte sixteen;
     210 
     211  program_counter: Word;
     212 
     213  special_function_registers_8051: Vector Byte nineteen;
     214  special_function_registers_8052: Vector Byte five;
     215 
     216  p1_latch: Byte;
     217  p3_latch: Byte;
     218 
     219  clock: Time
     220}.
     221\end{lstlisting}
     222\end{quote}
     223
     224% Polymorphic variants
     225
     226% Parsing
     227
     228% Bitvectors: dependent types
     229
     230% Dependent types subtyping
     231
     232\subsection{Dealing with partiality}
     233\label{subsect.dealing.with.partiality}
     234
     235The O'Caml 8051 emulator makes use of a number of partial functions.
     236These 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.
     237There are a number of possible reasons for this:
     238\begin{enumerate}
     239\item
     240\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.
     241An 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.
     242\item
     243\textbf{Assert false} may be called if the emulator finds itself in an `impossible situation'.
     244In this respect, we used \texttt{assert false} in a similar way to the previously described use of incomplete pattern analysis.
     245\item
     246\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.
     247\end{enumerate}
    160248\end{document}
Note: See TracChangeset for help on using the changeset viewer.