Changeset 395 for Deliverables


Ignore:
Timestamp:
Dec 9, 2010, 3:33:55 PM (9 years ago)
Author:
mulligan
Message:

Lots added from this afternoon to report. Implemented nearly all improvements CSC suggested.

File:
1 edited

Legend:

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

    r394 r395  
    6262\textbf{
    6363Report n. D4.1\\
    64 Verified Compiler---Back End}
     64Executable Formal Semantics of Machine Code}
    6565\end{LARGE}
    6666\end{center}
     
    9898We 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.
    9999In particular, we focus on the decisions made during the design of both emulators, and how the design of the O'Caml emulator had to be modified in order to fit into the more stringent type system of Matita.
     100
     101Both emulators provide an `executable formal semantics of machine code' for our target processor, per the description of the Deliverable in the \textsf{CerCo} Grant Agreement.
    100102\newpage
    101103
     
    107109\label{sect.task}
    108110
    109 The Grant Agreement states the D4.1/D4.2 deliverables consist of the following tasks:
    110 
     111The Grant Agreement states that Task T4.1, entitled `Executable Formal Semantics of Machine Code' has associated deliverable D4.1 consisting of the following:
    111112\begin{quotation}
    112113\textbf{Executable Formal Semantics of Machine Code}: Formal definition of the semantics of the target language.
    113114The semantics will be given in a functional (and hence executable) form, useful for testing, validation and project assessment.
    114115\end{quotation}
    115 
    116 \begin{quotation}
    117 \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.
    118 This unit is meant to be composable with the front-end of deliverable D3.2, to obtain a full working compiler for Milestone M2.
    119 A 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.
    120 \end{quotation}
    121 We now report on our implementation of these deliverables.
     116This report details our implementation of this deliverable.
     117
     118\subsection{Connection with other deliverables}
     119\label{subsect.connection.other.deliverables}
     120
     121Deliverable D4.1 is an executable formal semantics of the machine code of our target processor (a brief overview of the processor architecture is provided in Section~\ref{sect.brief.overview.target.processor}).
     122We provide an executable semantics in both O'Caml and the internal language of the Matita proof assistant.
     123
     124The C compiler delivered by Work Package 3 will eventually produce machine code executable by our emulator, and we expect that the emulator will be useful as a debugging aid for the compiler writers.
     125Further, additional deliverables listed under Work Package 4 will later make use of the work reported in this document.
     126In particular, Deliverables D4.2 and D4.3 entail the implementation of a formalised version of the intermediate language of the compiler, along with an executable formal semantics of these languages.
     127We expect our emulator will be of great use in the implementation of both of these deliverables for debugging and testing purposes.
    122128
    123129\section{A brief overview of the target processor}
     
    507513
    508514The Matita emulator is executable from within Matita (naturally, the speed of execution is only a fraction of the speed of the O'Caml emulator).
     515In particular, we provide a function \texttt{execute\_trace} which executes a fixed number of steps of an 8051 assembly program, returning a trace of the instructions executed, in the form of a list.
     516This trace may then be compared with the trace produced by the O'Caml emulator when executing a program for validation purposes.
    509517
    510518\subsection{Future work}
     
    521529\newpage
    522530
    523 \section{Listing of O'Caml files}
    524 \label{sect.listing.ocaml.files}
    525 
    526 \begin{center}
    527 \begin{tabular*}{0.9\textwidth}{lp{10cm}}
     531\section{Listing of O'Caml files and functions}
     532\label{sect.listing.ocaml.files.functions}
     533
     534\subsection{Listing of O'Caml files}
     535\label{subsect.listing.ocaml.files}
     536
     537\begin{center}
     538\begin{tabular*}{0.9\textwidth}{p{3cm}p{9cm}}
    528539Title & Description \\
    529540\hline
     
    545556\label{subsect.selected.important.functions}
    546557
    547 \subsubsection{From \texttt{ASMInterpret.mli}}
    548 
    549 \begin{center}
    550 \begin{tabular*}{0.9\textwidth}{lp{10cm}}
     558\subsubsection{From \texttt{ASMInterpret.ml(i)}}
     559
     560\begin{center}
     561\begin{tabular*}{0.85\textwidth}{p{3cm}@{\quad}p{9cm}}
    551562Name & Description \\
    552563\hline
     
    559570\end{center}
    560571
     572\subsubsection{From \texttt{IntelHex.ml(i)}}
     573
     574\begin{center}
     575\begin{tabular*}{0.85\textwidth}{p{3cm}@{\quad}p{9cm}}
     576Name & Description \\
     577\hline
     578\texttt{intel\_hex\_of\_file} & Reads in a file and parses it if in Intel IHX format, otherwise raises an exception. \\
     579\texttt{process\_intel\_hex} & Accepts a parsed Intel IHX file and populates a hashmap (of the same type as code memory) with the contents.
     580\end{tabular*}
     581\end{center}
     582
     583\subsubsection{From \texttt{Physical.ml(i)}}
     584
     585\begin{center}
     586\begin{tabular*}{0.85\textwidth}{p{3cm}@{\quad}p{9cm}}
     587Name & Description \\
     588\hline
     589\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. \\
     590\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. \\
     591\texttt{dec} & Decrements an eight bit bitvector with underflow, if necessary. \\
     592\texttt{inc} & Increments an eight bit bitvector with overflow, if necessary.
     593\end{tabular*}
     594\end{center}
     595
    561596\newpage
    562597
    563 \section{Listing of Matita files}
    564 \label{sect.listing.matita.files}
    565 
    566 \begin{center}
    567 \begin{tabular}{ll}
    568 Title & Description \\
    569 \hline
    570 \end{tabular}
    571 \end{center}
    572 
     598\section{Listing of Matita files and functions}
     599\label{sect.listing.matita.files.functions}
     600
     601\subsection{Listing of Matita files}
     602\label{subsect.listing.files}
     603
     604\begin{center}
     605\begin{tabular*}{0.75\textwidth}{p{3cm}p{9cm}}
     606Title & Description \\
     607\hline
     608\texttt{Arithmetic.ma} & Contains functions implementing arithmetical operations on bitvectors. \\
     609\texttt{ASM.ma} & Contains inductive datatypes for representing abstract syntax trees of 8051 assembly language. \\
     610\texttt{Assembly.ma} & Contains functions related to the assembly of 8051 assembly programs into a list of bytes. \\
     611\texttt{BitVector.ma} & Contains functions specific to bitvectors. \\
     612\texttt{BitVectorTrie.ma} & Contains an implementation of a sparse bitvector trie, which we use for implementing memory in the processor. \\
     613\texttt{Bool.ma} & Implementation of Booleans, and related functions. \\
     614\texttt{Cartesian.ma} & Implementation of Cartesian products, and related functions. \\
     615\texttt{Char.ma} & Hypothesises a type of characters. \\
     616\texttt{Connectives.ma} & Implementation of logical connectives. \\
     617\texttt{DoTest.ma} & Contains experiments and debugging code for testing the emulator. \\
     618\texttt{Either.ma} & Implementation of disjoint union types. \\
     619\texttt{Exponential.ma} & Functions implementating the Natural exponential, and related lemmas. \\
     620\texttt{Fetch.ma} & Contains functions relating to the `fetch' function of the emulator, and related functions. \\
     621\texttt{Interpret.ma} & Contains the main emulator function, as well as ancillary definitions and functions. \\
     622\texttt{List.ma} & An implementation of polymorphic lists, and related functions. \\
     623\texttt{Maybe.ma} & Implementation of the `maybe' type. \\
     624\texttt{Nat.ma} & Implementation of Natural numbers, and related functions and lemmas. \\
     625\texttt{Status.ma} & Contains the definition of the `status' record, and related definitions. \\
     626\texttt{String.ma} & Contains a type for representing strings. \\
     627\texttt{Test.ma} & Contains definitions useful for debugging and testing the emulator. \\
     628\texttt{Universes.ma} & Infrastructure file related to Matita's universe hierarchy. \\
     629\texttt{Util.ma} & Contains miscellaneous utility functions that do not fit anywhere else. \\
     630\texttt{Vector.ma} & Contains an implementation of polymorphic vectors, and related definitions.
     631\end{tabular*}
     632\end{center}
     633
     634\subsection{Selected important functions}
     635\label{subsect.matita.selected.important.functions}
     636
     637\subsubsection{From \texttt{Arithmetic.ma}}
     638
     639\begin{center}
     640\begin{tabular*}{0.75\textwidth}{p{3cm}p{9cm}}
     641Title & Description \\
     642\hline
     643\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. \\
     644\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. \\
     645\texttt{half\_add} & Performs a standard half addition on bitvectors, returning the result and carry bit. \\
     646\texttt{full\_add} & Performs a standard full addition on bitvectors and a carry bit, returning the result and a carry bit.
     647\end{tabular*}
     648\end{center}
     649
     650\subsubsection{From \texttt{Assembly.ma}}
     651
     652\begin{center}
     653\begin{tabular*}{0.75\textwidth}{p{3cm}p{9cm}}
     654Title & Description \\
     655\hline
     656\texttt{assemble1} & Assembles a single 8051 assembly instruction into its encoded counterpart. \\
     657\texttt{assemble} & Assembles a list of 8051 assembly instructions into their encoded counterpart.
     658\end{tabular*}
     659\end{center}
     660
     661\subsubsection{From \texttt{BitVectorTrie.ma}}
     662
     663\begin{center}
     664\begin{tabular*}{0.75\textwidth}{p{3cm}p{9cm}}
     665Title & Description \\
     666\hline
     667\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. \\
     668\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.
     669\end{tabular*}
     670\end{center}
     671
     672\subsubsection{From \texttt{DoTest.ma}}
     673
     674\begin{center}
     675\begin{tabular*}{0.75\textwidth}{p{3cm}p{9cm}}
     676Title & Description \\
     677\hline
     678\texttt{execute\_trace} & Executes an assembly program for a fixed number of steps, recording in a trace which instructions were executed.
     679\end{tabular*}
     680\end{center}
     681
     682\subsubsection{From \texttt{Fetch.ma}}
     683
     684\begin{center}
     685\begin{tabular*}{0.75\textwidth}{p{3cm}p{9cm}}
     686Title & Description \\
     687\hline
     688\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. \\
     689\end{tabular*}
     690\end{center}
     691
     692\subsubsection{From \texttt{Interpret.ma}}
     693
     694\begin{center}
     695\begin{tabular*}{0.75\textwidth}{p{3cm}p{9cm}}
     696Title & Description \\
     697\hline
     698\texttt{execute\_1} & Executes a single step of an 8051 assembly program. \\
     699\texttt{execute} & Executes a fixed number of steps of an 8051 assembly program.
     700\end{tabular*}
     701\end{center}
     702
     703\subsubsection{From \texttt{Status.ma}}
     704
     705\begin{center}
     706\begin{tabular*}{0.75\textwidth}{p{3cm}p{9cm}}
     707Title & Description \\
     708\hline
     709\texttt{load} & Loads an assembled 8051 assembly program into code memory.
     710\end{tabular*}
     711\end{center}
    573712\end{document}
Note: See TracChangeset for help on using the changeset viewer.