Ignore:
Timestamp:
Sep 28, 2012, 11:41:39 AM (7 years ago)
Author:
sacerdot
Message:

3.4 patched.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/cpp-asm-2012/cpp-2012-asm.tex

    r2367 r2368  
    490490gets you back to where you started.
    491491
    492 Lemma \texttt{fetch\_assembly\_pseudo} is obtained by composition of \texttt{expand\_pseudo\_instruction} and \texttt{assembly\_1\_pseudoinstruction}:
    493 \XXX they do not exist any longer!
     492Remembering that \texttt{assembly\_1\_pseudo\_instruction} is the composition
     493of \texttt{assembly1} with \texttt{expand\_pseudo\_instruction}, we can
     494lift the previous result from instructions (already expanded) to
     495pseudoinstructions (to be expanded):
    494496\begin{lstlisting}
    495497lemma fetch_assembly_pseudo:
    496498 $\forall$program: pseudo_assembly_program.
    497  $\forall$policy.
    498  $\forall$ppc.
    499  $\forall$code_memory.
     499 $\forall$policy,ppc,code_memory.
    500500 let $\langle$preamble, instr_list$\rangle$ := program in
    501501 let pi := $\pi_1$ (fetch_pseudo_instruction instr_list ppc) in
    502502 let pc := policy ppc in
    503  let instrs := expand_pseudo_instructio policy ppc pi in
     503 let instrs := expand_pseudo_instruction policy ppc pi in
    504504 let $\langle$l, a$\rangle$ := assembly_1_pseudoinstruction policy ppc pi in
    505505 let pc_plus_len := pc + l in
     
    511511The function \texttt{fetch\_many} fetches multiple machine code instructions from code memory and performs some routine checks.
    512512
    513 Intuitively, Lemma \texttt{fetch\_assembly\_pseudo} can be read as follows.
    514 Suppose we expand the pseudoinstruction at \texttt{ppc} with the policy, obtaining the list of machine code instructions \texttt{instrs}.
    515 Suppose we also assemble the pseudoinstruction at \texttt{ppc} to obtain \texttt{a}, a list of bytes.
    516 Then, we check with \texttt{fetch\_many} that the number of machine instructions that were fetched matches the number of instruction that \texttt{expand\_pseudo\_instruction} expanded.
    517 
    518 The final lemma in this series is \texttt{fetch\_assembly\_pseudo2} that combines the Lemma \texttt{fetch\_assembly\_pseudo} with the correctness of the functions that load object code into the processor's memory:
     513Intuitively, Lemma \texttt{fetch\_assembly\_pseudo} says that
     514expanding a pseudoinstruction into $n$ instructions, encoding the instructions
     515and immediately fetching $n$ instructions back yield exactly the expansion.
     516
     517Combining \texttt{assembly\_ok} with the previos lemma and a proof of
     518correctness of loading object code in memory, we finally get correctness
     519of the assembler w.r.t. fetching:
    519520\begin{lstlisting}
    520521lemma fetch_assembly_pseudo2:
    521  $\forall$program.
    522  $\mid$snd program$\mid$ $\leq$ $2^{16}$ $\rightarrow$
    523  $\forall$policy.
    524  policy is correct for program $\rightarrow$
     522 $\forall$program.  $\mid$snd program$\mid$ $\leq$ $2^{16}$ $\rightarrow$
     523 $\forall$policy.  policy is correct for program $\rightarrow$
    525524 $\forall$ppc. ppc < $\mid$snd program$\mid$ $\rightarrow$
    526   let $\langle$labels, costs$\rangle$ := create_label_cost_map program in
    527525  let $\langle$assembled, costs'$\rangle$ := $\pi_1$ (assembly program policy) in
    528526  let cmem := load_code_memory assembled in
     
    536534Suppose we are given an assembly program which can be addressed by a 16-bit word and a policy that is correct for this program.
    537535Suppose we are able to successfully assemble an assembly program using \texttt{assembly} and produce a code memory, \texttt{cmem}.
    538 Then, fetching a pseudoinstruction from the pseudo-code memory at address \texttt{ppc} corresponds to fetching a sequence of instructions from the real code memory using \texttt{policy} to expand pseudoinstructions.
    539 The fetched sequence corresponds to the expansion, according to the policy, of the pseudoinstruction.
    540 
    541 At first, the lemma appears to immediately imply the correctness of the assembler, but this property is \emph{not} strong enough to establish that the semantics of an assembly program has been preserved by the assembly process since it does not establish the correspondence between the semantics of a pseudoinstruction and that of its expansion.
    542 In particular, the two semantics differ on instructions that \emph{could} directly manipulate program addresses.
     536Then, fetching a pseudoinstruction from the pseudo-code memory stored in
     537the interval $[ppc,newppc]$ corresponds to fetching a sequence of instructions from the real code memory, stored in the interval $[policy(ppc),policy(ppc+1)]$.
     538The correspondence is precise: the fetched instructions are exactly those
     539obtained expanding the pseudoinstruction according to policy.
     540
     541In order to complete the proof of correctness of the assembler, we need
     542to prove that each pseudoinstruction is simulated by the execution of its
     543expansion (correctness w.r.t. execution). In general this is not the case
     544when the instruction freely manipulates program addresses. Characterizing
     545well behaved programs and proving correctness w.r.t. expansion is the topic
     546of the next Section.
    543547
    544548% ---------------------------------------------------------------------------- %
     
    548552\label{subsect.total.correctness.for.well.behaved.assembly.programs}
    549553
    550 The traditional approach to verifying the correctness of an assembler is to treat memory addresses as opaque structures that cannot be modified.
     554The traditional approach to verifying the correctness of an assembler is to
     555restrict the semantics of assembly code to treat memory addresses as opaque
     556(symbolic) structures that cannot be modified.
    551557Memory is represented as a map from opaque addresses to the disjoint union of data and opaque addresses---addresses are kept opaque to prevent their possible `semantics breaking' manipulation by assembly programs:
    552558\begin{displaymath}
    553559\mathtt{Mem} : \mathtt{Addr} \rightarrow \mathtt{Bytes} + \mathtt{Addr} \qquad \llbracket - \rrbracket : \mathtt{Instr} \rightarrow \mathtt{Mem} \rightarrow \mathtt{option\ Mem}
    554560\end{displaymath}
    555 The semantics of a pseudoinstruction, $\llbracket - \rrbracket$, is given as a possibly failing function from pseudoinstructions and memory spaces to new memory spaces.
    556 The semantic function proceeds by case analysis over the operands of a given instruction, failing if either operand is an opaque address, or otherwise succeeding, updating memory.
     561Similarly, registers may contain either data or opaque addresses.
     562
     563The semantics of a pseudoinstruction, $\llbracket - \rrbracket$, is given as a possibly failing function from pseudoinstructions and memory spaces (pseudostatuses to be more precise) to new memory spaces. The semantic function proceeds by case analysis over the operands of a given instruction, failing if either operand is an opaque address and the operation is meaningless on it.
    557564\begin{gather*}
    558 \llbracket \mathtt{ADD\ @A1\ @A2} \rrbracket^\mathtt{M} = \begin{cases}
     565\llbracket \mathtt{MUL\ @A1\ @A2} \rrbracket^\mathtt{M} = \begin{cases}
    559566                                                              \mathtt{Byte\ b1},\ \mathtt{Byte\ b2} & \rightarrow \mathtt{Some}(\mathtt{M}\ \text{with}\ \mathtt{b1} + \mathtt{b2}) \\
    560567                                                              -,\ \mathtt{Addr\ a} & \rightarrow \mathtt{None} \\
Note: See TracChangeset for help on using the changeset viewer.