Changeset 2368
 Timestamp:
 Sep 28, 2012, 11:41:39 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/cppasm2012/cpp2012asm.tex
r2367 r2368 490 490 gets you back to where you started. 491 491 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! 492 Remembering that \texttt{assembly\_1\_pseudo\_instruction} is the composition 493 of \texttt{assembly1} with \texttt{expand\_pseudo\_instruction}, we can 494 lift the previous result from instructions (already expanded) to 495 pseudoinstructions (to be expanded): 494 496 \begin{lstlisting} 495 497 lemma fetch_assembly_pseudo: 496 498 $\forall$program: pseudo_assembly_program. 497 $\forall$policy. 498 $\forall$ppc. 499 $\forall$code_memory. 499 $\forall$policy,ppc,code_memory. 500 500 let $\langle$preamble, instr_list$\rangle$ := program in 501 501 let pi := $\pi_1$ (fetch_pseudo_instruction instr_list ppc) in 502 502 let pc := policy ppc in 503 let instrs := expand_pseudo_instructio policy ppc pi in503 let instrs := expand_pseudo_instruction policy ppc pi in 504 504 let $\langle$l, a$\rangle$ := assembly_1_pseudoinstruction policy ppc pi in 505 505 let pc_plus_len := pc + l in … … 511 511 The function \texttt{fetch\_many} fetches multiple machine code instructions from code memory and performs some routine checks. 512 512 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: 513 Intuitively, Lemma \texttt{fetch\_assembly\_pseudo} says that 514 expanding a pseudoinstruction into $n$ instructions, encoding the instructions 515 and immediately fetching $n$ instructions back yield exactly the expansion. 516 517 Combining \texttt{assembly\_ok} with the previos lemma and a proof of 518 correctness of loading object code in memory, we finally get correctness 519 of the assembler w.r.t. fetching: 519 520 \begin{lstlisting} 520 521 lemma 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$ 525 524 $\forall$ppc. ppc < $\mid$snd program$\mid$ $\rightarrow$ 526 let $\langle$labels, costs$\rangle$ := create_label_cost_map program in527 525 let $\langle$assembled, costs'$\rangle$ := $\pi_1$ (assembly program policy) in 528 526 let cmem := load_code_memory assembled in … … 536 534 Suppose we are given an assembly program which can be addressed by a 16bit word and a policy that is correct for this program. 537 535 Suppose 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 pseudocode 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. 536 Then, fetching a pseudoinstruction from the pseudocode memory stored in 537 the interval $[ppc,newppc]$ corresponds to fetching a sequence of instructions from the real code memory, stored in the interval $[policy(ppc),policy(ppc+1)]$. 538 The correspondence is precise: the fetched instructions are exactly those 539 obtained expanding the pseudoinstruction according to policy. 540 541 In order to complete the proof of correctness of the assembler, we need 542 to prove that each pseudoinstruction is simulated by the execution of its 543 expansion (correctness w.r.t. execution). In general this is not the case 544 when the instruction freely manipulates program addresses. Characterizing 545 well behaved programs and proving correctness w.r.t. expansion is the topic 546 of the next Section. 543 547 544 548 %  % … … 548 552 \label{subsect.total.correctness.for.well.behaved.assembly.programs} 549 553 550 The traditional approach to verifying the correctness of an assembler is to treat memory addresses as opaque structures that cannot be modified. 554 The traditional approach to verifying the correctness of an assembler is to 555 restrict the semantics of assembly code to treat memory addresses as opaque 556 (symbolic) structures that cannot be modified. 551 557 Memory is represented as a map from opaque addresses to the disjoint union of data and opaque addressesaddresses are kept opaque to prevent their possible `semantics breaking' manipulation by assembly programs: 552 558 \begin{displaymath} 553 559 \mathtt{Mem} : \mathtt{Addr} \rightarrow \mathtt{Bytes} + \mathtt{Addr} \qquad \llbracket  \rrbracket : \mathtt{Instr} \rightarrow \mathtt{Mem} \rightarrow \mathtt{option\ Mem} 554 560 \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. 561 Similarly, registers may contain either data or opaque addresses. 562 563 The 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. 557 564 \begin{gather*} 558 \llbracket \mathtt{ ADD\ @A1\ @A2} \rrbracket^\mathtt{M} = \begin{cases}565 \llbracket \mathtt{MUL\ @A1\ @A2} \rrbracket^\mathtt{M} = \begin{cases} 559 566 \mathtt{Byte\ b1},\ \mathtt{Byte\ b2} & \rightarrow \mathtt{Some}(\mathtt{M}\ \text{with}\ \mathtt{b1} + \mathtt{b2}) \\ 560 567 ,\ \mathtt{Addr\ a} & \rightarrow \mathtt{None} \\
Note: See TracChangeset
for help on using the changeset viewer.