Changeset 395
 Timestamp:
 Dec 9, 2010, 3:33:55 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Report/report.tex
r394 r395 62 62 \textbf{ 63 63 Report n. D4.1\\ 64 Verified CompilerBack End}64 Executable Formal Semantics of Machine Code} 65 65 \end{LARGE} 66 66 \end{center} … … 98 98 We 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. 99 99 In 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 101 Both 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. 100 102 \newpage 101 103 … … 107 109 \label{sect.task} 108 110 109 The Grant Agreement states the D4.1/D4.2 deliverables consist of the following tasks: 110 111 The Grant Agreement states that Task T4.1, entitled `Executable Formal Semantics of Machine Code' has associated deliverable D4.1 consisting of the following: 111 112 \begin{quotation} 112 113 \textbf{Executable Formal Semantics of Machine Code}: Formal definition of the semantics of the target language. 113 114 The semantics will be given in a functional (and hence executable) form, useful for testing, validation and project assessment. 114 115 \end{quotation} 115 116 \begin{quotation} 117 \textbf{CIC encoding: Backend}: 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 frontend 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 Costannotating OCaml Compiler D2.2 is achieved and reported in the deliverable, possibly triggering updates of the Untrusted Costannotating OCaml Compiler sources. 120 \end{quotation} 121 We now report on our implementation of these deliverables. 116 This report details our implementation of this deliverable. 117 118 \subsection{Connection with other deliverables} 119 \label{subsect.connection.other.deliverables} 120 121 Deliverable 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}). 122 We provide an executable semantics in both O'Caml and the internal language of the Matita proof assistant. 123 124 The 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. 125 Further, additional deliverables listed under Work Package 4 will later make use of the work reported in this document. 126 In 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. 127 We expect our emulator will be of great use in the implementation of both of these deliverables for debugging and testing purposes. 122 128 123 129 \section{A brief overview of the target processor} … … 507 513 508 514 The Matita emulator is executable from within Matita (naturally, the speed of execution is only a fraction of the speed of the O'Caml emulator). 515 In 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. 516 This trace may then be compared with the trace produced by the O'Caml emulator when executing a program for validation purposes. 509 517 510 518 \subsection{Future work} … … 521 529 \newpage 522 530 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}} 528 539 Title & Description \\ 529 540 \hline … … 545 556 \label{subsect.selected.important.functions} 546 557 547 \subsubsection{From \texttt{ASMInterpret.ml i}}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}} 551 562 Name & Description \\ 552 563 \hline … … 559 570 \end{center} 560 571 572 \subsubsection{From \texttt{IntelHex.ml(i)}} 573 574 \begin{center} 575 \begin{tabular*}{0.85\textwidth}{p{3cm}@{\quad}p{9cm}} 576 Name & 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}} 587 Name & 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 561 596 \newpage 562 597 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}} 606 Title & 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}} 641 Title & 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}} 654 Title & 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}} 665 Title & 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}} 676 Title & 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}} 686 Title & 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}} 696 Title & 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}} 707 Title & Description \\ 708 \hline 709 \texttt{load} & Loads an assembled 8051 assembly program into code memory. 710 \end{tabular*} 711 \end{center} 573 712 \end{document}
Note: See TracChangeset
for help on using the changeset viewer.