# Changeset 433

Ignore:
Timestamp:
Dec 15, 2010, 7:42:04 PM (9 years ago)
Message:

Most things added, just need to fill in types in table.

File:
1 edited

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

 r424 \lstdefinelanguage{matita-ocaml} {keywords={ndefinition,ncoercion,nlemma,ntheorem,nremark,ninductive,nrecord,nqed,nlet,let,in,rec,match,return,with,Type}, {keywords={ndefinition,ncoercion,nlemma,ntheorem,nremark,ninductive,nrecord,nqed,nlet,let,in,rec,match,return,with,Type,try}, morekeywords={[2]nwhd,nnormalize,nelim,ncases,ndestruct}, morekeywords={[3]type,of}, This is relatively straightforward, and is done in two stages. The first stage consists of iterating over an assembly program, building a dictionary of all labels and their position in the program. This dictionary is stored, and can later be used by the callback function passed to \texttt{execute}, the function that executes an 8051 assembly program, in order to produce a trace of labels. The first stage consists of iterating over an assembly program, building a multiset of all labels and their position in the program. This multiset is stored, and can later be used by the callback function passed to \texttt{execute}, the function that executes an 8051 assembly program, in order to produce a trace of labels. The callback function, a function from the processor state to unit, passed to \texttt{execute} implements our label collecting semantics'. In pseudocode: \begin{quote} \begin{lstlisting} let f status := try let labels := lookup (program_counter status) (costs_map $\cup$ label_map) in () with NotFound $\rightarrow$ () \end{lstlisting} \end{quote} Where \texttt{labels} is initialized to $\texttt{ref empty}$. That is, the callback attempts to make note of all the label that program execution passes through'. In Deliverable D4.4, we will prove that this labelled trace is preserved by the compilation process. The second stage consists of iterating over the same program and replacing all pseudojumps (both conditional and unconditional) with an 8051 jump to the requisite computed offset. At the moment, the second pass of the expansion stage replaces all unconditional pseudojumps with a \texttt{LJMP} for simplicity. We do, however, plan to improve this process for efficiency reasons, expanding to shorter jumps where feasible. \subsection{Anatomy of the emulator} \label{subsect.anatomy.emulator} \begin{figure}[t] \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 \end{lstlisting} \end{quote} \caption{Pseudocode of unlabelled program execution} \label{fig.unlabelled.execution} \end{figure} \begin{figure}[t] \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 \end{lstlisting} \end{quote} \caption{Pseudocode of labelled program execution} \label{fig.labelled.execution} \end{figure} 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. 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}. The types of the functions mentioned in the pseudocode of Figures~\ref{fig.unlabelled.execution} and~\ref{fig.labelled.execution} are as follows: \begin{center} \begin{tabular*}{0.9\textwidth}{p{4cm}p{5cm}} Title & Type \\ \hline \texttt{process\_intel\_hex} & \\ \texttt{load\_mem} & \\ \texttt{initialize} & \texttt{status} \\ \texttt{fetch} & \\ \texttt{execute} & \\ \texttt{assembly} & \\ \texttt{callback} & \texttt{status -> unit} \end{tabular*} \end{center} \subsection{Validation}
Note: See TracChangeset for help on using the changeset viewer.