Changeset 1010
- Timestamp:
- Jun 20, 2011, 6:18:39 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/CPP2011/cpp-2011.tex
r1009 r1010 300 300 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. 301 301 At the heart of this process is \texttt{sigma0} which traverses an assembly program building maps from pseudo program counters to program counters. 302 This function fails if and only if an internal call to \texttt{assembly\_1\_pseudoinstruction } fails:302 This function fails if and only if an internal call to \texttt{assembly\_1\_pseudoinstruction\_safe} fails, which happens if a jump pseudoinstruction is expanded incorrectly: 303 303 \begin{lstlisting} 304 304 definition sigma0: pseudo_assembly_program 305 305 $\rightarrow$ option (nat $\times$ (nat $\times$ (BitVectorTrie Word 16))) := $\ldots$ 306 306 \end{lstlisting} 307 We eventually lift this to functions from program counters to program counters: 307 Here, the returned \texttt{BitVectorTrie} is a map between pseudo program counters and program counters, and is constructed by successively expanding pseudoinstructions and incrementing the two program counters the requisite amount to keep them in correct correspondence. 308 The two natural numbers returned are the maximum values that the two program counters attained. 309 310 We eventually lift this to functions from pseudo program counters to program counters, implemented as \texttt{Word}s: 308 311 \begin{lstlisting} 309 312 definition sigma_safe: 310 313 pseudo_assembly_program $\rightarrow$ option (Word $\rightarrow$ Word) := $\ldots$ 311 314 \end{lstlisting} 312 Now, it's possible to define what a `good policy' is i.e. one that does not cause \texttt{sigma\_safe} to fail. 315 Now, it's possible to define what a `good policy' is. 316 A policy is deemed good when it prevents \texttt{sigma\_safe} from ever failing. 313 317 As mentioned, \texttt{sigma\_safe} can only fail if an assembly program fails to be assembled: 314 318 \begin{lstlisting} 315 319 definition policy_ok := $\lambda$p. sigma_safe p $\neq$ None $\ldots$. 316 320 \end{lstlisting} 317 Finally, we obtain \texttt{sigma}, a map from program counters to program counters, which is guranteed not to fail as we internally provide a that 318 \begin{lstlisting} 319 definition sigma: pseudo_assembly_program $\rightarrow$ Word $\rightarrow$ Word := $\ldots$ 321 Finally, we obtain \texttt{sigma}, a mapping from pseudo program counters to program counters which incorporates, depending also on a policy. 322 This is a thin shell around \texttt{sigma\_safe}, and dispenses with the option type via a proof that \texttt{sigma\_safe} never fails under the assumption that a supplied policy is correct: 323 \begin{lstlisting} 324 definition sigma: $\forall$p. policy p $\rightarrow$ Word $\rightarrow$ Word := $\ldots$ 320 325 \end{lstlisting} 321 326 … … 328 333 Using our policies, we now work toward proving the total correctness of the assembler. 329 334 By total correctness, we mean that the assembly process does not change the semantics of an assembly program. 330 Naturally, this necessitates keeping some sort of correspondence between program counters at the assembly level, and program counters at the machine code level.335 Naturally, this necessitates keeping some sort of correspondence between addresses at the assembly level and addresses at the machine code level. 331 336 For this, we use the \texttt{sigma} machinery defined at the end of Subsection~\ref{subsect.policies}. 332 337
Note: See TracChangeset
for help on using the changeset viewer.