# Changeset 438 for Deliverables

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

Final version.

File:
1 edited

### Legend:

Unmodified
 r434 \begin{quote} \begin{lstlisting} let file := open_file "Filename" in let program := process_intel_hex file in let code_memory := load_mem program (initialize status) in let first_instr := fetch status code_memory (program_counter status) in execute callback status let hex = IntelHex.intel_hex_of_file filename in let mem = IntelHex.process_intel_hex hex in let status = ASMInterpret.load_mem mem ASMInterpret.initialize in ASMInterpret.execute callback status \end{lstlisting} \end{quote} \begin{quote} \begin{lstlisting} let program, label_map, cost_map := assembly labelled_program in let code_memory := load_mem program (initialize status) in let first_instr := fetch status code_memory (program_counter status) in execute callback status let mem, cost_map = ASMInterpret.assembly labelled_program in let status = ASMInterpret.load_mem mem ASMInterpret.initialize in ASMInterpret.execute callback status \end{lstlisting} \end{quote} We provide a high-level overview of the operation of the emulator. Two modes of operation exist: execution of an unlabelled program, and execution of a labelled program. Unlabelled execution proceeds as follows. Two modes of operation exist: execution of an unlabelled program -- like one obtained disassemblying an already assembled program -- and execution of a labelled program. Unlabelled execution proceeds as follows (see Fig.~\ref{fig.unlabelled.execution}). Program code is loaded onto the 8051 in a standard format, the Intel Hex (IHX) format. 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. Accordingly, our O'Caml emulator can parse IHX files and populate the emulator's code memory with their contents using \texttt{process\_intel\_hex}. Code memory is loaded into the processor status using \texttt{load\_mem}. 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. Thereafter, the emulator calls \texttt{execute}, which performs the standard fetch-decode-execute cycle indefinitely. Pseudocode is provided in Figure~\ref{fig.unlabelled.execution}. Labelled execution is similar. 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. As mentioned, these multisets may be used by the \texttt{callback} function, passed to execute, in order to implement label collecting semantics'. Pseudocode is provided in Figure~\ref{fig.labelled.execution}. All 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. Accordingly, 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}. Once code memory is loaded into the status, the emulator calls \texttt{execute}, which performs the standard fetch-decode-execute cycle indefinitely. The callback function passed to \texttt{execute} is called at the beginning of each cycle and takes in input the processor status. It can be used for debugging purposes, for instance to compute execution traces. The callback function can even stop execution by raising the \texttt{Halt} exception. This is the only way to stop the emulator, since the 8051 processors have no instruction to stop execution and program termination'' is usually compiled to a tight diverging loop. Labelled execution is similar (see Fig.~\ref{fig.labelled.execution}). 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 map from code addresses to cost annotations. The map can be used by the \texttt{callback} function, passed to execute, in order to implement the label collecting semantics' that the CerCo compiler will preserve. The (simplified) types of the functions mentioned in the pseudocode of Figures~\ref{fig.unlabelled.execution} and~\ref{fig.labelled.execution} are as follows: Title & Type \\ \hline \texttt{intel\_hex\_of\_file} & \texttt{string -> intel\_hex\_entry list} \\ \texttt{process\_intel\_hex} & \texttt{intel\_hex\_entry list -> byte map} \\ \texttt{load\_mem} & \texttt{byte map -> status -> status} \\ \texttt{initialize} & \texttt{status} \\ \texttt{fetch} & \texttt{status -> byte map -> byte map.key -> instruction} \\ \texttt{execute} & \texttt{(status -> unit) -> status -> status} \\ \texttt{assembly} & \texttt{labelled\_instruction list -> byte list * label map * cost map} \\ \texttt{assembly} & \texttt{assembly\_program -> byte list * cost map} \\ \texttt{callback} & \texttt{status -> unit} \end{tabular*} We plan, once the newer version is released, to port the Matita emulator to the most up-to-date version of the proof assistant. This will allow us to extract a verified O'Caml emulator from the Matita theory files. Another possible future work is to implement separate compilation by modifying the \texttt{assembly} function output to include a simble table and by adding a linking function. The assembly function will be changed to minimize (or at least reduce) the size of the assembled program by translating pseudo jumps to short jumps where possible. Finally, while the O'Caml emulator already implements I/O, timers and interrupt handling, the Matita version does not. Interrupt handling will 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, for the sake of completeness and future uses, we plan to eventually complete also the Matita version. \newpage Title & Description \\ \hline \texttt{assemble1} & Assembles a single 8051 assembly instruction into its encoded counterpart. \\ \texttt{assemble} & Assembles a list of 8051 assembly pseudo-instructions into their encoded counterpart. \texttt{assemble1} & Assembles a single 8051 assembly instruction into its memory representation. \\ \texttt{assemble} & Assembles an 8051 assembly program into its memory representation.\\ \texttt{assemble\_unlabelled\_program} &\\& Assembles a list of (unlabelled) 8051 assembly instructions into its memory representation. \end{tabular*} \end{center}