Changeset 2068 for src/ASM

Ignore:
Timestamp:
Jun 13, 2012, 7:54:36 PM (7 years ago)
Message:

...

File:
1 edited

Legend:

Unmodified
 r2067 \label{subsect.total.correctness.of.the.assembler} Throughout the proof of correctness for assembly we assume that policies are bifurcated into two functions: \texttt{sigma} mapping \texttt{Word} to \texttt{Word} and \texttt{policy} mapping \texttt{Word} to \texttt{bool}. For our purposes, \texttt{sigma} is most interesting, as it maps pseudo program counters to program counters; \texttt{policy} is merely a technical device used in jump expansion. Using our policies, we now work toward proving the total correctness of the assembler. By total correctness', we mean that the assembly process never fails when provided with a good policy and that the process does not change the semantics of a certain class of well behaved assembly programs. By good policy' we mean We assume the correctness of the policies given to us using a function, \texttt{sigma\_policy\_specification} that we take in input, when needed. We expand pseudoinstructions using the function \texttt{expand\_pseudo\_instruction}. This takes an assembly program (consisting of a list of pseudoinstructions), a policy for the program, a map detailing the physical addresses of data labels from the pseudo program's preamble, and the pseudoinstruction to be expanded. It returns a list of instructions, corresponding to the expanded pseudoinstruction referenced by the pointer. Execution proceeds by case analysis on the pseudoinstruction given as input. The policy, \texttt{sigma}, is used to decide how to expand \texttt{Call}s, \texttt{Jmp}s and conditional jumps. \begin{lstlisting} definition expand_pseudo_instruction: $\forall$lookup_labels: Identifier $\rightarrow$ Word. $\forall$sigma: Word $\rightarrow$ Word. $\forall$policy: Word $\rightarrow$ bool. Word $\rightarrow$ (Identifier $\rightarrow$ Word) $\rightarrow$ pseudo_instruction $\rightarrow$ list instruction := ... \end{lstlisting} By `total correctness', we mean that the assembly process never fails when provided with a correct policy and that the process does not change the semantics of a certain class of well behaved assembly programs. We can express the following lemma, expressing the correctness of the assembly function (slightly simplified):