# Changeset 2350

Ignore:
Timestamp:
Sep 26, 2012, 5:53:31 PM (7 years ago)
Message:

Got to the conclusions.

File:
1 edited

### Legend:

Unmodified
 r2349 $\times$ (option address_entry). \end{lstlisting} [dpm update] Here, \texttt{upper\_lower} is a type isomorphic to the booleans denoting whether a byte value is the upper or lower byte of some 16-bit address. The implementation of \texttt{internal\_pseudo\_address\_map} is complicated by some peculiarities of the MCS-51's instruction set. Note here that all addresses are 16 bit words, but are stored (and manipulated) as 8 bit bytes. All \texttt{MOV} instructions in the MCS-51 must use the accumulator \texttt{A} as an intermediary, moving a byte at a time. The second component of \texttt{internal\_pseudo\_address\_map} therefore states whether the accumulator currently holds a piece of an address, and if so, whether it is the upper or lower byte of the address (using the boolean flag) complete with the corresponding source address in full. The first component, on the other hand, performs a similar task for the rest of external RAM. Again, we use a boolean flag to describe whether a byte is the upper or lower component of a 16-bit address. The third component of \texttt{internal\_pseudo\_address\_map} therefore states whether the accumulator currently holds a piece of an address, and if so, whether it is the upper or lower byte of the address (using the \texttt{upper\_lower} flag) complete with the corresponding source address in full. The first and second components, on the other hand, performs a similar task for the higher and lower external RAM. Again, we use our \texttt{upper\_lower} flag to describe whether a byte is the upper or lower component of a 16-bit address. The \texttt{low\_internal\_ram\_of\_pseudo\_low\_internal\_ram} function converts the lower internal RAM of a \texttt{PseudoStatus} into the lower internal RAM of a \texttt{Status}. A similar function exists for high internal RAM. Note that both RAM segments are indexed using addresses 7-bits long. The function is currently axiomatised, and an associated set of axioms prescribe the behaviour of the function: Note that both RAM segments are indexed using addresses 7-bits long: \begin{lstlisting} definition low_internal_ram_of_pseudo_low_internal_ram: program_counter s < $2^{16}$ $\rightarrow$ option internal_pseudo_address_map \end{lstlisting} [dpm change] Note, if we wished to allow benign manipulations' of addresses, it would be this function that needs to be changed. If we wished to allow benign manipulations' of addresses, it would be this function that needs to be changed. Note we once again use dependent types to ensure that program counters are properly within bounds. The third argument is a function that resolves the concrete address of a label. The function \texttt{ticks\_of0} computes how long---in clock cycles---a pseudoinstruction will take to execute when expanded in accordance with a given policy. (ticks_of program ($\lambda$id. addr_of id ps) policy) ps) policy. \end{lstlisting} [dpm change] The statement is standard for forward simulation, but restricted to \texttt{PseudoStatuses} \texttt{ps} whose next instruction to be executed is well-behaved with respect to the \texttt{internal\_pseudo\_address\_map} \texttt{M}. Further, we explicitly require proof that our policy is correct and the pseudo-program counter lies within the bounds of the program. Further, we explicitly require proof that our policy is correct, our program is well-labelled (i.e. no repeated labels, and so on) and the pseudo-program counter lies within the bounds of the program. Theorem \texttt{main\_thm} establishes the total correctness of the assembly process and can simply be lifted to the forward simulation of an arbitrary number of well behaved steps on the assembly program.