Dec 9, 2010, 3:33:55 PM (11 years ago)

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

1 edited


  • Deliverables/D4.1/Report/report.tex

    r394 r395  
    6363Report n. D4.1\\
    64 Verified Compiler---Back End}
     64Executable Formal Semantics of Machine Code}
    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.
     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.
    109 The Grant Agreement states the D4.1/D4.2 deliverables consist of the following tasks:
     111The Grant Agreement states that Task T4.1, entitled `Executable Formal Semantics of Machine Code' has associated deliverable D4.1 consisting of the following:
    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.
    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.
     118\subsection{Connection with other deliverables}
     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.
     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.
    123129\section{A brief overview of the target processor}
    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.
    510518\subsection{Future work}
    523 \section{Listing of O'Caml files}
    524 \label{sect.listing.ocaml.files}
    526 \begin{center}
    527 \begin{tabular*}{0.9\textwidth}{lp{10cm}}
     531\section{Listing of O'Caml files and functions}
     534\subsection{Listing of O'Caml files}
    528539Title & Description \\
    547 \subsubsection{From \texttt{ASMInterpret.mli}}
    549 \begin{center}
    550 \begin{tabular*}{0.9\textwidth}{lp{10cm}}
     558\subsubsection{From \texttt{ASMInterpret.ml(i)}}
    551562Name & Description \\
     572\subsubsection{From \texttt{IntelHex.ml(i)}}
     576Name & Description \\
     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.
     583\subsubsection{From \texttt{Physical.ml(i)}}
     587Name & Description \\
     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.
    563 \section{Listing of Matita files}
    564 \label{sect.listing.matita.files}
    566 \begin{center}
    567 \begin{tabular}{ll}
    568 Title & Description \\
    569 \hline
    570 \end{tabular}
    571 \end{center}
     598\section{Listing of Matita files and functions}
     601\subsection{Listing of Matita files}
     606Title & Description \\
     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.
     634\subsection{Selected important functions}
     637\subsubsection{From \texttt{Arithmetic.ma}}
     641Title & Description \\
     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.
     650\subsubsection{From \texttt{Assembly.ma}}
     654Title & Description \\
     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.
     661\subsubsection{From \texttt{BitVectorTrie.ma}}
     665Title & Description \\
     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.
     672\subsubsection{From \texttt{DoTest.ma}}
     676Title & Description \\
     678\texttt{execute\_trace} & Executes an assembly program for a fixed number of steps, recording in a trace which instructions were executed.
     682\subsubsection{From \texttt{Fetch.ma}}
     686Title & Description \\
     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. \\
     692\subsubsection{From \texttt{Interpret.ma}}
     696Title & Description \\
     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.
     703\subsubsection{From \texttt{Status.ma}}
     707Title & Description \\
     709\texttt{load} & Loads an assembled 8051 assembly program into code memory.
Note: See TracChangeset for help on using the changeset viewer.