# Changeset 974

Ignore:
Timestamp:
Jun 16, 2011, 11:24:27 AM (8 years ago)
Message:

Location:
src/ASM/CPP2011
Files:
2 edited

### Legend:

Unmodified
 r973 To a degree of approximation, the assembler on an assembly program, consisting of $n$ pseudoinstructions $\mathtt{P_i}$ for $1 \leq i \leq n$, works as in the following diagram: \begin{displaymath} [\mathtt{P_1}, \ldots \mathtt{P_n}] \xrightarrow{\left(\mathtt{P_i} \xrightarrow{\mbox{\fontsize{7}{9}\selectfont$\mathtt{expand}$}} \mathtt{[I_1^i, \ldots I^q_i]} \xrightarrow{\mbox{\fontsize{7}{9}\selectfont$\mathtt{assembly1}^*$}} \mathtt{}\right)^{*}} \mathtt{} [\mathtt{P_1}, \ldots \mathtt{P_n}] \xrightarrow{\mathtt{flatten}\left(\mathtt{P_i} \xrightarrow{\mbox{\fontsize{7}{9}\selectfont$\mathtt{expand}$}} \mathtt{[I_1^i, \ldots I^q_i]} \xrightarrow{\mbox{\fontsize{7}{9}\selectfont$\mathtt{assembly1}^*$}} \mathtt{}\right)^{*}} \mathtt{} \end{displaymath} Here $\mathtt{I^i_j}$ for $1 \leq j \leq q$ are the $q$ machine code instructions obtained by expanding, with \texttt{expand\_pseudo\_instruction}, a single pseudoinstruction. Each machine code instruction $\mathtt{I^i_j}$ is then assembled, using the \texttt{assembly1} function, into a list of bytes. This process is iterated for each pseudoinstruction, before the lists are flattened into a single bit list representation of the original assembly program. By inspecting the above diagram, it would appear that the best way to proceed with a proof that the assembly process does not change the semantics of an assembly program is via a decomposition of the problem into two subproblems. Namely, we first expand any and all pseudoinstructions into lists of machine instructions, and provide a proof that this process does not change our program's semantics. Finally, we assemble all machine code instructions into machine code---lists of bytes---and prove once more that this process does not have an adverse effect on a program's semantics. By composition, we then have that the whole assembly process is semantics preserving. This is a tempting approach to the proof, but ultimately the wrong approach. In particular, it is important that we track how the program counter indexing into the assembly program, and the machine's program counter evolve, so that we can relate them. Expanding pseudoinstructions requires that the machine's program counter be incremented by $n$ steps, for $1 \leq n$, for every increment of the assembly program's program counter. Keeping track of the correspondence between the two program counters quickly becomes unfeasible using a compositional approach, and hence the proof must be monolithic. % ---------------------------------------------------------------------------- % 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$ 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: definition sigma: pseudo_assembly_program $\rightarrow$ Word $\rightarrow$ Word := $\ldots$ \end{lstlisting} % ---------------------------------------------------------------------------- % % SECTION                                                                      % % ---------------------------------------------------------------------------- % \subsection{Total correctness of the assembler} \label{subsect.total.correctness.of.the.assembler} CSC: no options using policy \begin{lstlisting} lemma fetch_assembly_pseudo2: $\forall$program, assembled, costs, labels. Some $\ldots$ $\langle$labels,costs$\rangle$ = build_maps program $\rightarrow$ Some $\ldots$ $\langle$assembled,costs$\rangle$ = assembly program $\rightarrow$ $\forall$ppc. let code_memory := load_code_memory assembled in let preamble := $\pi_1$ program in let data_labels := construct_datalabels preamble in let lk_labels := λx. sigma program (address_of_word_labels_code_mem ($\pi_2$ program) x) in let lk_dlabels := λx. lookup ? ? x data_labels (zero ?) in let expansion := jump_expansion ppc program in let $\langle$pi,newppc$\rangle$ := fetch_pseudo_instruction ($\pi_2$ program) ppc in let ppc' := sigma program ppc in let newppc' := sigma program newppc in let instructions' := expand_pseudo_instruction lk_labels lk_dlabels ppc' expansion pi in let fetched := fetch_many code_memory newppc' ppc' instructions in $\exists$instructions. Some ? instructions = instructions' $\wedge$ fetched. \end{lstlisting} \begin{lstlisting} definition expand_pseudo_instruction: ∀lookup_labels, lookup_datalabels, pc, policy_decision. pseudo_instruciton $\rightarrow$ option list instruction := $\ldots$ \end{lstlisting} \begin{lstlisting} axiom assembly_ok: ∀program,assembled,costs,labels. Some $\ldots$ $\langle$labels, costs$\rangle$ = build_maps program $\rightarrow$ Some $\ldots$ $\langle$assembled, costs$\rangle$ = assembly program $\rightarrow$ let code_memory := load_code_memory assembled in let preamble := $\pi_1$ program in let datalabels := construct_datalabels preamble in let lk_labels := $\lambda$x. sigma program (address_of_word_labels_code_mem ($\pi_2$ program) x) in let lk_dlabels := $\lambda$x. lookup ? ? x datalabels (zero ?) in ∀ppc,len,assembledi. let $\langle$pi, newppc$\rangle$ := fetch_pseudo_instruction ($\pi_2$ program) ppc in let assembly' := assembly_1_pseudoinstruction program ppc (sigma program ppc) lk_labels lk_dlabels pi in let newpc := (sigma program ppc) + len in let echeck := encoding_check code_memory (sigma program ppc) slen assembledi in Some $\ldots$ $\langle$len, assembledi$\rangle$ = assembly' $\rightarrow$ echeck $\wedge$ sigma program newppc = newpc. \end{lstlisting} \begin{lstlisting} lemma fetch_assembly_pseudo: $\forall$program, ppc, lk_labels, lk_dlabels. $\forall$pi, code_memory, len, assembled, instructions, pc. let jexp := jump_expansion ppc program in let exp := expand_pseudo_instruction lookup_labels lookup_datalabels pc jexp pi let ass := assembly_1_pseudoinstruction program ppc pc lk_labels lk_dlabels pi in Some ? instructions = exp $\rightarrow$ Some $\ldots$ $\langle$len, assembled$\rangle$ = ass $\rightarrow$ encoding_check code_memory pc (pc + len) assembled $\rightarrow$ fetch_many code_memory (pc + len) pc instructions. \end{lstlisting} \begin{lstlisting} theorem fetch_assembly: $\forall$pc, i, cmem, assembled. assembled = assembly1 i $\rightarrow$ let len := length ... assembled in encoding_check cmem pc (pc + len) assembled $\rightarrow$ let fetched := fetch code_memory (bitvector_of_nat $\ldots$ pc) in let $\langle$instr_pc, ticks$\rangle$ := fetched in let $\langle$instr,pc'$\rangle$ := instr_pc in (eq_instruction instr i $\wedge$ eqb ticks (ticks_of_instruction instr) $\wedge$ eq_bv $\ldots$ pc' (pc + len)) = true. \end{lstlisting} An \texttt{internal\_pseudo\_address\_map} positions in the memory of a \texttt{PseudoStatus} with a physical memory address. \begin{lstlisting} This is done with the following function: \begin{lstlisting} definition next_internal_pseudo_address_map: internal_pseudo_address_map $\rightarrow$ PseudoStatus $\rightarrow$ option internal_pseudo_address_map \end{lstlisting} Finally, we are able to state and prove our main theorem relating the execution of a single assembly instruction and the execution of (possibly) many machine code instructions: \begin{lstlisting} lemma main_thm: definition next_internal_pseudo_address_map: internal_pseudo_address_map $\rightarrow$ PseudoStatus $\rightarrow$ option internal_pseudo_address_map \end{lstlisting} Finally, we are able to state and prove our main theorem. This relates the execution of a single assembly instruction and the execution of (possibly) many machine code instructions. That is, the assembly process preserves the semantics of an assembly program, as it is translated into machine code: \begin{lstlisting} theorem main_thm: ∀M,M',ps,s,s''. next_internal_pseudo_address_map M ps = Some ... M' $\rightarrow$ Suppose further that, after executing a single assembly instruction and converting the resulting \texttt{PseudoStatus} into a \texttt{Status}, we obtain $s''$, being careful to track the number of ticks executed. Then, there exists some number $n$, so that executing $n$ machine code instructions in \texttt{Status} $s$ gives us \texttt{Status} $s''$. % ---------------------------------------------------------------------------- % % SECTION                                                                      % % ---------------------------------------------------------------------------- % \subsection{Proof of correctness} \label{subsect.proof.of.correctness} CSC: no options using policy \begin{lstlisting} lemma fetch_assembly_pseudo2: ∀program,assembled,costs,labels. Some ... LANGLElabels,costsRANGLE = build_maps program → Some ... LANGLEassembled,costsRANGLE = assembly program → ∀ppc. let code_memory ≝ load_code_memory assembled in let preamble ≝ \fst program in let data_labels ≝ construct_datalabels preamble in let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in let expansion ≝ jump_expansion ppc program in let LANGLEpi,newppcRANGLE ≝ fetch_pseudo_instruction (\snd program) ppc in ∃instructions. Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program ppc) expansion pi ∧ fetch_many code_memory (sigma program newppc) (sigma program ppc) instructions. \end{lstlisting} \begin{lstlisting} definition expand_pseudo_instruction: ∀lookup_labels.∀lookup_datalabels.∀pc.∀policy_decision. (sigma program ppc) expansion. pseudo_instruciton -> list instruction. \end{lstlisting} \begin{lstlisting} axiom assembly_ok: ∀program,assembled,costs,labels. Some ... LANGLElabels,costsRANGLE = build_maps program → Some ... LANGLEassembled,costsRANGLE = assembly program → let code_memory ≝ load_code_memory assembled in let preamble ≝ \fst program in let datalabels ≝ construct_datalabels preamble in let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in let lookup_datalabels ≝ λx. lookup ?? x datalabels (zero ?) in ∀ppc,len,assembledi. let LANGLEpi,newppcRANGLE ≝ fetch_pseudo_instruction (\snd program) ppc in Some ... LANGLElen,assemblediRANGLE = assembly_1_pseudoinstruction program ppc (sigma program ppc) lookup_labels lookup_datalabels pi → encoding_check code_memory (sigma program ppc) (bitvector_of_nat ... (nat_of_bitvector ... (sigma program ppc) + len)) assembledi ∧ sigma program newppc = bitvector_of_nat ... (nat_of_bitvector ... (sigma program ppc) + len). \end{lstlisting} \begin{lstlisting} lemma fetch_assembly_pseudo: ∀program,ppc,lookup_labels,lookup_datalabels. ∀pi,code_memory,len,assembled,instructions,pc. let expansion ≝ jump_expansion ppc program in Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (bitvector_of_nat ? pc) expansion pi → Some ... LANGLElen,assembledRANGLE = assembly_1_pseudoinstruction program ppc (bitvector_of_nat ? pc) lookup_labels lookup_datalabels pi → encoding_check code_memory (bitvector_of_nat ... pc) (bitvector_of_nat ... (pc + len)) assembled → fetch_many code_memory (bitvector_of_nat ... (pc + len)) (bitvector_of_nat ... pc) instructions. \end{lstlisting} \begin{lstlisting} theorem fetch_assembly: ∀pc,i,code_memory,assembled. assembled = assembly1 i → let len ≝ length ... assembled in encoding_check code_memory (bitvector_of_nat ... pc) (bitvector_of_nat ... (pc + len)) assembled → let fetched ≝ fetch code_memory (bitvector_of_nat ... pc) in let LANGLEinstr_pc, ticksRANGLE ≝ fetched in let LANGLEinstr,pc'RANGLE ≝ instr_pc in (eq_instruction instr i ∧ eqb ticks (ticks_of_instruction instr) ∧ eq_bv ... pc' (bitvector_of_nat ... (pc + len))) = true. \end{lstlisting} Theorem \texttt{main\_thm} establishes the correctness of the assembly process. % ---------------------------------------------------------------------------- %
 r960 mathescape=true, texcl=false, keywords={include}, morekeywords={record, with, match, let, rec, corec, inductive, definition, axiom, keywords={record, with, match, let, rec, corec, inductive, definition, axiom, qed, intro, intros, symmetry, simplify, rewrite, apply, elim, assumption, left, cut, cases, auto, right, coercion, split, lemma, theorem, skip, constructor, copy, from, letin, by, done, we, conclude, assume, need, to, prove, unfold, return, and, check, notation, interpretation, lapply, repeat, try, as, clear, in, change, whd, exists}, morekeywords={include}, %emph={Type, Prop, nat, real}, emphstyle={\textit}, literate= {...}{{$\ldots$}}1 , tabsize=1, comment=[s]{(*}{*)}, showstringspaces=true, captionpos=b, mathescape=true, keywordstyle=\bfseries, keywordstyle=\bfseries, keywordstyle=\bfseries, %backgroundcolor=\color{gray}, frame=tblr,