Ignore:
Timestamp:
Dec 16, 2010, 3:05:31 AM (9 years ago)
Author:
sacerdot
Message:

Final version.

File:
1 edited

Legend:

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

    r434 r438  
    320320\begin{quote}
    321321\begin{lstlisting}
    322   let file := open_file "Filename" in
    323   let program := process_intel_hex file in
    324   let code_memory := load_mem program (initialize status) in
    325   let first_instr := fetch status code_memory (program_counter status) in
    326     execute callback status
     322  let hex = IntelHex.intel_hex_of_file filename in
     323  let mem = IntelHex.process_intel_hex hex in
     324  let status = ASMInterpret.load_mem mem ASMInterpret.initialize in
     325    ASMInterpret.execute callback status
    327326\end{lstlisting}
    328327\end{quote}
     
    334333\begin{quote}
    335334\begin{lstlisting}
    336   let program, label_map, cost_map := assembly labelled_program in
    337   let code_memory := load_mem program (initialize status) in
    338   let first_instr := fetch status code_memory (program_counter status) in
    339     execute callback status
     335  let mem, cost_map = ASMInterpret.assembly labelled_program in
     336  let status = ASMInterpret.load_mem mem ASMInterpret.initialize in
     337    ASMInterpret.execute callback status
    340338\end{lstlisting}
    341339\end{quote}
     
    345343
    346344We provide a high-level overview of the operation of the emulator.
    347 Two modes of operation exist: execution of an unlabelled program, and execution of a labelled program.
    348 
    349 Unlabelled execution proceeds as follows.
    350 
     345Two modes of operation exist: execution of an unlabelled program -- like one obtained disassemblying an already assembled program --
     346and execution of a labelled program.
     347
     348Unlabelled execution proceeds as follows (see Fig.~\ref{fig.unlabelled.execution}).
    351349Program code is loaded onto the 8051 in a standard format, the Intel Hex (IHX) format.
    352 All compilers producing machine code for the 8051, including the SDCC compiler which we use for debugging purposes, produce compiled programs in IHX format as standard.
    353 Accordingly, our O'Caml emulator can parse IHX files and populate the emulator's code memory with their contents using \texttt{process\_intel\_hex}.
    354 Code memory is loaded into the processor status using \texttt{load\_mem}.
    355 
    356 Once code memory is populated, and the rest of the emulator state has been initialized (using a call to \texttt{initialize}), the O'Caml emulator performs an initial \texttt{fetch} of the first instruction pointed to by the program counter.
    357 Thereafter, the emulator calls \texttt{execute}, which performs the standard fetch-decode-execute cycle indefinitely.
    358 Pseudocode is provided in Figure~\ref{fig.unlabelled.execution}.
    359 
    360 Labelled execution is similar.
    361 However, instead of a program being loaded from an Intel Hex file, we process a labelled program with \texttt{assembly}, in order to obtain an unlabelled program, complete with a multiset of all labels and cost annotations, and their positions in the program, in the form of a map datastructure.
    362 As mentioned, these multisets may be used by the \texttt{callback} function, passed to execute, in order to implement `label collecting semantics'.
    363 Pseudocode is provided in Figure~\ref{fig.labelled.execution}.
     350All compilers/assemblers producing machine code for the 8051, including the SDCC compiler which we use for debugging purposes, produce compiled programs in IHX format as standard.
     351Accordingly, our O'Caml emulator can parse IHX files using \texttt{intel\_hex\_of\_file} and populate the emulator's code memory with their contents using \texttt{process\_intel\_hex}. Code memory is loaded into the initial processor status using \texttt{load\_mem}.
     352
     353Once code memory is loaded into the status, the emulator calls \texttt{execute}, which performs the standard fetch-decode-execute cycle
     354indefinitely. The callback function passed to \texttt{execute} is called at the beginning of each cycle and takes in input the processor
     355status. It can be used for debugging purposes, for instance to compute execution traces.
     356
     357The callback function can even stop execution by raising the \texttt{Halt} exception.
     358This is the only way to stop the emulator, since the 8051 processors have no instruction to stop execution and program ``termination'' is
     359usually compiled to a tight diverging loop.
     360
     361Labelled execution is similar (see Fig.~\ref{fig.labelled.execution}).
     362However, instead of a program being loaded from an Intel Hex file, we process a labelled program with \texttt{assembly}, in order to obtain an unlabelled program, complete with a map from code addresses to cost annotations. The map can be used by the \texttt{callback} function,
     363passed to execute, in order to implement the `label collecting semantics' that the CerCo compiler will preserve.
    364364
    365365The (simplified) types of the functions mentioned in the pseudocode of Figures~\ref{fig.unlabelled.execution} and~\ref{fig.labelled.execution} are as follows:
     
    369369Title & Type \\
    370370\hline
     371\texttt{intel\_hex\_of\_file} & \texttt{string -> intel\_hex\_entry list} \\
    371372\texttt{process\_intel\_hex} & \texttt{intel\_hex\_entry list -> byte map} \\
    372373\texttt{load\_mem} & \texttt{byte map -> status -> status} \\
    373374\texttt{initialize} & \texttt{status} \\
    374 \texttt{fetch} & \texttt{status -> byte map -> byte map.key -> instruction} \\
    375375\texttt{execute} & \texttt{(status -> unit) -> status -> status} \\
    376 \texttt{assembly} & \texttt{labelled\_instruction list -> byte list * label map * cost map} \\
     376\texttt{assembly} & \texttt{assembly\_program -> byte list * cost map} \\
    377377\texttt{callback} & \texttt{status -> unit}
    378378\end{tabular*}
     
    618618We plan, once the newer version is released, to port the Matita emulator to the most up-to-date version of the proof assistant.
    619619This will allow us to extract a verified O'Caml emulator from the Matita theory files.
     620
     621Another possible future work is to implement separate compilation by modifying the \texttt{assembly} function output to include a simble
     622table and by adding a linking function.
     623
     624The assembly function will be changed to minimize (or at least reduce) the size of the assembled program by translating pseudo jumps
     625to short jumps where possible.
     626
     627Finally, while the O'Caml emulator already implements I/O, timers and interrupt handling, the Matita version does not. Interrupt handling
     628will not be dealt with in CerCo and we are likely to handle I/O in a simplified way by means of external library functions. Nevertheless,
     629for the sake of completeness and future uses, we plan to eventually complete also the Matita version.
    620630
    621631\newpage
     
    746756Title & Description \\
    747757\hline
    748 \texttt{assemble1} & Assembles a single 8051 assembly instruction into its encoded counterpart. \\
    749 \texttt{assemble} & Assembles a list of 8051 assembly pseudo-instructions into their encoded counterpart.
     758\texttt{assemble1} & Assembles a single 8051 assembly instruction into its memory representation. \\
     759\texttt{assemble} & Assembles an 8051 assembly program into its memory representation.\\
     760\texttt{assemble\_unlabelled\_program} &\\& Assembles a list of (unlabelled) 8051 assembly instructions into its memory representation.
    750761\end{tabular*}
    751762\end{center}
Note: See TracChangeset for help on using the changeset viewer.