 Timestamp:
 Jun 15, 2011, 4:32:57 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CPP2011/cpp2011.tex
r960 r968 213 213 Notice, here, that the emulation function for pseudoprograms takes an additional argument. 214 214 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. 215 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. 215 We call this function a \emph{costing}, and note that the costing is induced by the particular strategy we use to expand pseudoinstructions. 216 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. 217 218 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. 216 219 This timing information is used inside \texttt{execute\_1\_pseudo\_instruction} to update the clock of the \texttt{PseudoStatus}. 217 220 During the proof of correctness of the assembler we relate the clocks of \texttt{Status}es and \texttt{PseudoStatus}es. … … 233 236 \label{subsect.policies} 234 237 235 \begin{lstlisting} 236 inductive jump_length: Type[0] ≝ 238 Policies exist to dictate how conditional and unconditional jumps at the assembly level should be expanded into machine code instructions. 239 Using policies, we are able to completely decouple the decision over how jumps are expanded with the act of expansion, simplifying our proofs. 240 As mentioned, the MCS51 instruction set includes three different jump instructions: \texttt{SJMP}, \texttt{AJMP} and \texttt{LJMP}; call these `short', `medium' and `long' jumps, respectively: 241 \begin{lstlisting} 242 inductive jump_length: Type[0] := 237 243  short_jump: jump_length 238 244  medium_jump: jump_length … … 240 246 \end{lstlisting} 241 247 242 \begin{lstlisting} 243 definition jump_expansion_policy ≝ BitVectorTrie jump_length 16. 244 \end{lstlisting} 245 246 \begin{lstlisting} 247 definition policy_ok := λpolicy.λp. sigma_safe policy p <> None .... 248 \end{lstlisting} 249 248 A \texttt{jump\_expansion\_policy} is a map from \texttt{Word}s to \texttt{jump\_length}s, implemented as a trie. 249 Intuitively, a policy maps positions in a program (indexed using program counters implemented as \texttt{Word}s) to a particular variety of jump. 250 \begin{lstlisting} 251 definition jump_expansion_policy := BitVectorTrie jump_length 16. 252 \end{lstlisting} 253 254 Next, we require a series of `sigma' functions. 255 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. 256 At the heart of this process is \texttt{sigma0} which traverses an assembly program building maps from program counter to program counter. 257 This function fails if and only if an internal call to \texttt{assembly\_1\_pseudoinstruction} fails: 258 \begin{lstlisting} 259 definition sigma0: pseudo_assembly_program 260 $\rightarrow$ option (nat $\times$ (nat $\times$ (BitVectorTrie Word 16))) := $\ldots$ 261 \end{lstlisting} 262 263 We eventually lift this to functions from program counters to program counters: 264 \begin{lstlisting} 265 definition sigma_safe: pseudo_assembly_program 266 $\rightarrow$ option (Word $\rightarrow$ Word) := $\ldots$ 267 \end{lstlisting} 268 269 Now, it's possible to define what a `good policy' is i.e. one that does not cause \texttt{sigma\_safe} to fail. 270 As mentioned, \texttt{sigma\_safe} can only fail if an assembly program fails to be assembled: 271 \begin{lstlisting} 272 definition policy_ok := $\lambda$policy. $\lambda$p. sigma_safe policy p $\neq$ None $\ldots$. 273 \end{lstlisting} 274 275 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'. 250 276 \begin{lstlisting} 251 277 definition sigma:
Note: See TracChangeset
for help on using the changeset viewer.