# Changeset 1016 for src/ASM/CPP2011

Ignore:
Timestamp:
Jun 21, 2011, 10:20:20 AM (8 years ago)
Message:

Many fixes to the code snippets.

File:
1 edited

### Legend:

Unmodified
 r1013 | long_jump: jump_length. \end{lstlisting} A \texttt{jump\_expansion\_policy} is a map from pseudo program counters (implemented as \texttt{Word}s) to \texttt{jump\_length}s, implemented as a trie. A \texttt{jump\_expansion\_policy} is a map from pseudo program counters (implemented as \texttt{Word}s) to \texttt{jump\_length}s. Efficient implementations of policies are based on tries. 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. definition policy_type ≝ Word → jump_length. \end{lstlisting} Next, we require a series of sigma' functions. 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: \begin{lstlisting} definition sigma0: pseudo_assembly_program definition sigma0: pseudo_assembly_program $\rightarrow$ policy_type $\rightarrow$ option (nat $\times$ (nat $\times$ (BitVectorTrie Word 16))) := $\ldots$ \end{lstlisting} \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. A policy is deemed good when it prevents \texttt{sigma\_safe} from ever failing. As mentioned, \texttt{sigma\_safe} can only fail if an assembly program fails to be assembled: \begin{lstlisting} definition policy_ok := $\lambda$p. sigma_safe p $\neq$ None $\ldots$. \end{lstlisting} Finally, we obtain \texttt{sigma}, a mapping from pseudo program counters to program counters which incorporates, depending also on a policy. 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: pseudo_assembly_program $\rightarrow$ policy_type $\rightarrow$ option (Word $\rightarrow$ Word) := $\ldots$ \end{lstlisting} Now, it's possible to define what a `good policy' is for a program \texttt{p}. A policy \texttt{pol} is deemed good when it prevents \texttt{sigma\_safe} from failing on \texttt{p}. Failure is only possible when the policy prescribes short/middle jumps to too far locations or when the prouced object code does not fit in code memory. A \texttt{policy} for a program \texttt{p} is a policy that is good for \texttt{p}. \begin{lstlisting} definition policy_ok := $\lambda$pol.$\lambda$p. sigma_safe p $\neq$ None $\ldots$. definition policy ≝ λp. $\Sigma$jump_expansion:policy_type. policy_ok jump_expansion p. \end{lstlisting} Finally, we obtain \texttt{sigma}, a mapping from pseudo program counters to program counters that takes in input a good policy and thus never fails. Note how we avoid failure here and in most of the remaining functions by restricting the domain using the dependent type \texttt{policy}. \begin{lstlisting} definition sigma: $\forall$p. policy p $\rightarrow$ Word $\rightarrow$ Word := $\ldots$