# Changeset 968 for src/ASM/CPP2011

Ignore:
Timestamp:
Jun 15, 2011, 4:32:57 PM (8 years ago)
Message:

work on paper

File:
1 edited

### Legend:

Unmodified
 r960 Notice, here, that the emulation function for pseudoprograms takes an additional argument. This is a function that maps program counters (for the pseudoprogram) to pairs of natural numbers representing the number of clock ticks that the pseudoinstruction needs to execute, post expansion. We require \emph{pairs} of natural numbers because, in the case of expanding conditional jumps to labels, the expansion of the true branch' and false branch' may differ in the number of clock ticks needed for execution. We call this function a \emph{costing}, and note that the costing is induced by the particular strategy we use to expand pseudoinstructions. If we change how we expand conditional jumps to labels, for instance, then the costing needs to change, hence \texttt{execute\_1\_pseudo\_instruction}'s parametricity in the costing. The costing returns \emph{pairs} of natural numbers because, in the case of expanding conditional jumps to labels, the expansion of the true branch' and false branch' may differ in the number of clock ticks needed for execution. This timing information is used inside \texttt{execute\_1\_pseudo\_instruction} to update the clock of the \texttt{PseudoStatus}. During the proof of correctness of the assembler we relate the clocks of \texttt{Status}es and \texttt{PseudoStatus}es. \label{subsect.policies} \begin{lstlisting} inductive jump_length: Type[0] ≝ Policies exist to dictate how conditional and unconditional jumps at the assembly level should be expanded into machine code instructions. Using policies, we are able to completely decouple the decision over how jumps are expanded with the act of expansion, simplifying our proofs. As mentioned, the MCS-51 instruction set includes three different jump instructions: \texttt{SJMP}, \texttt{AJMP} and \texttt{LJMP}; call these short', medium' and long' jumps, respectively: \begin{lstlisting} inductive jump_length: Type[0] := | short_jump: jump_length | medium_jump: jump_length \end{lstlisting} \begin{lstlisting} definition jump_expansion_policy ≝ BitVectorTrie jump_length 16. \end{lstlisting} \begin{lstlisting} definition policy_ok := λpolicy.λp. sigma_safe policy p <> None .... \end{lstlisting} A \texttt{jump\_expansion\_policy} is a map from \texttt{Word}s to \texttt{jump\_length}s, implemented as a trie. Intuitively, a policy maps positions in a program (indexed using program counters implemented as \texttt{Word}s) to a particular variety of jump. \begin{lstlisting} definition jump_expansion_policy := BitVectorTrie jump_length 16. \end{lstlisting} Next, we require a series of sigma' functions. These functions map assembly program counters to their machine code counterparts, establishing the correspondence between positions' in an assembly program and positions' in a machine code program. At the heart of this process is \texttt{sigma0} which traverses an assembly program building maps from program counter to program counter. This function fails if and only if an internal call to \texttt{assembly\_1\_pseudoinstruction} fails: \begin{lstlisting} definition sigma0: pseudo_assembly_program $\rightarrow$ option (nat $\times$ (nat $\times$ (BitVectorTrie Word 16))) := $\ldots$ \end{lstlisting} We eventually lift this to functions from program counters to program counters: \begin{lstlisting} definition sigma_safe: pseudo_assembly_program $\rightarrow$ option (Word $\rightarrow$ Word) := $\ldots$ \end{lstlisting} Now, it's possible to define what a good policy' is i.e. one that does not cause \texttt{sigma\_safe} to fail. As mentioned, \texttt{sigma\_safe} can only fail if an assembly program fails to be assembled: \begin{lstlisting} definition policy_ok := $\lambda$policy. $\lambda$p. sigma_safe policy p $\neq$ None $\ldots$. \end{lstlisting} Finally, we obtain \texttt{sigma}, a map from program counters to program counters, which is guranteed not to fail, as we must provide a proof that our policy at hand is a good policy'. \begin{lstlisting} definition sigma: