Changeset 2349
 Timestamp:
 Sep 26, 2012, 5:44:31 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/cppasm2012/cpp2012asm.tex
r2348 r2349 172 172 In this way, Matita supports the `Russell' proof methodology developed by Sozeau in~\cite{sozeau:subset:2006}, with an implementation that is lighter and more tightly integrated with the system than that of Coq. 173 173 174 Throughout this paper we simplify the statements of lemmas and types of definitions in order to emphasise readability. 175 174 176 %  % 175 177 % SECTION % … … 349 351 definition expand_pseudo_instruction: 350 352 $\forall$lookup_labels: Identifier $\rightarrow$ Word. 351 $\forall$sigma: Word $\rightarrow$ Word. 352 $\forall$policy: Word $\rightarrow$ bool. 353 $\forall$policy. 353 354 $\forall$ppc: Word. 354 355 $\forall$lookup_datalabels: Identifier $\rightarrow$ Word. … … 358 359 Here, the functions \texttt{lookup\_labels} and \texttt{lookup\_datalabels} are the functions that map labels and datalabels to program counters respectively, both of them used in the semantics of assembly. 359 360 The input \texttt{pi} is the pseudoinstruction to be expanded and is found at address \texttt{ppc} in the assembly program. 360 The policy is defined using the two functions \texttt{sigma} and \texttt{policy}, of which \texttt{sigma} is the most interesting. 361 The function \texttt{sigma} maps pseudoprogram counters to program counters: the encoding of the expansion of the pseudoinstruction found at address \texttt{a} in the assembly code should be placed into code memory at address \texttt{sigma(a)}. 361 The function takes \texttt{policy} as an input. 362 In reality, this is a pair of functions, but for the purposes of this paper we simplify. 363 The \texttt{policy} maps pseudoprogram counters to program counters: the encoding of the expansion of the pseudoinstruction found at address \texttt{a} in the assembly code should be placed into code memory at address \texttt{policy(a)}. 362 364 Of course this is possible only if the policy is correct, which means that the encoding of consecutive assembly instructions must be consecutive in code memory. 363 365 \begin{displaymath} 364 \texttt{ sigma}(\texttt{ppc} + 1) = \texttt{pc} + \texttt{current\_instruction\_size}366 \texttt{policy}(\texttt{ppc} + 1) = \texttt{pc} + \texttt{current\_instruction\_size} 365 367 \end{displaymath} 366 368 Here, \texttt{current\_instruction\_size} is the size in bytes of the encoding of the expanded pseudoinstruction found at \texttt{ppc}. … … 369 371 A companion submission to this one~\cite{boender:correctness:2012} certifies an algorithm that finds branch displacement policies for the assembler described in this paper. 370 372 371 The \texttt{expand\_pseudo\_instruction} function uses the \texttt{ sigma} map to determine the size of jump required when expanding pseudojumps, computing the jump size by examining the size of the differences between program counters.372 For instance, if at address \texttt{ppc} in the assembly program we found \texttt{Jmp l} such that \texttt{lookup\_labels l = a}, if the offset \texttt{d = sigma(a)  sigma(ppc + 1)} is such that \texttt{d} $< 128$ then \texttt{Jmp l} is normally translated to the best local solution, the short jump \texttt{SJMP d}.373 The \texttt{expand\_pseudo\_instruction} function uses the \texttt{policy} map to determine the size of jump required when expanding pseudojumps, computing the jump size by examining the size of the differences between program counters. 374 For instance, if at address \texttt{ppc} in the assembly program we found \texttt{Jmp l} such that \texttt{lookup\_labels l = a}, if the offset \texttt{d = policy(a)  policy(ppc + 1)} is such that \texttt{d} $< 128$ then \texttt{Jmp l} is normally translated to the best local solution, the short jump \texttt{SJMP d}. 373 375 A global best solution to the branch displacement problem, however, is not always made of locally best solutions. 374 376 Therefore, in some circumstances, it is necessary to force the assembler to expand jumps into larger ones. 375 This is achieved by the \texttt{policy} function: if \texttt{policy ppc = true}then a \texttt{Jmp l} at address \texttt{ppc} is always translated to a long jump.377 This is achieved by another booleanvalued function such that if the function applied to \texttt{ppc} returns true then a \texttt{Jmp l} at address \texttt{ppc} is always translated to a long jump. 376 378 An essentially identical mechanism exists for call instructions. 377 379 … … 404 406 nth assembled_i n = nth assembled (policy ppc + k). 405 407 \end{lstlisting} 406 [dpm: update]407 408 In plain words, the type of \texttt{assembly} states the following. 408 Suppose we are given a policy that is correct for the program we are assembling, and suppose the program to be assembled is fully addressable by a 16bit word. 409 Then if we fetch from the pseudoprogram counter \texttt{ppc} we get a pseudoinstruction \texttt{pi} and a new pseudoprogram counter \texttt{ppc}. 410 Further, assembling the pseudoinstruction \texttt{pi} results in a list of bytes, \texttt{a}. 411 Then, indexing into this list with any natural number \texttt{j} less than the length of \texttt{a} gives the same result as indexing into \texttt{assembled} with \texttt{sigma(ppc)} (the program counter pointing to the start of the expansion in \texttt{assembled}) plus \texttt{j}. 409 Suppose we are given a policy that is correct for the program we are assembling. 410 Then we return a list of assembled bytes, complete with a map from program counters to cost labels, such that the following properties hold for the list of bytes. 411 Under the condition that the policy is `correct' for the program and the program is fully addressable by a 16bit word, the assembled list is also fully addressable by a 16bit word, the policy maps the last program counter that can address the program to the last instruction of the assemble pseudoinstruction or overflows, and if we fetch from the pseudoprogram counter \texttt{ppc} we get a pseudoinstruction \texttt{pi} and a new pseudoprogram counter \texttt{ppc}. 412 Further, assembling the pseudoinstruction \texttt{pseudo\_instr} results in a list of bytes, \texttt{assembled\_i}. 413 Then, indexing into this list with any natural number \texttt{n} less than the length of \texttt{assembled\_i} gives the same result as indexing into \texttt{assembled} with \texttt{policy ppc} (the program counter pointing to the start of the expansion in \texttt{assembled}) plus \texttt{k}. 412 414 413 415 Essentially the lemma above states that the \texttt{assembly} function correctly expands pseudoinstructions, and that the expanded instruction reside consecutively in memory. … … 435 437 Or, in plainer words, assembling and then immediately fetching again gets you back to where you started. 436 438 437 Lemma \texttt{fetch\_assembly\_pseudo} (slightly simplified, here)is obtained by composition of \texttt{expand\_pseudo\_instruction} and \texttt{assembly\_1\_pseudoinstruction}:439 Lemma \texttt{fetch\_assembly\_pseudo} is obtained by composition of \texttt{expand\_pseudo\_instruction} and \texttt{assembly\_1\_pseudoinstruction}: 438 440 \begin{lstlisting} 439 441 lemma fetch_assembly_pseudo: … … 445 447 let pi := $\pi_1$ (fetch_pseudo_instruction instr_list ppc) in 446 448 let pc := policy ppc in 447 let instrs := expand_pseudo_instructio sigmapolicy ppc pi in448 let $\langle$l, a$\rangle$ := assembly_1_pseudoinstruction sigmapolicy ppc pi in449 let instrs := expand_pseudo_instructio policy ppc pi in 450 let $\langle$l, a$\rangle$ := assembly_1_pseudoinstruction policy ppc pi in 449 451 let pc_plus_len := pc + l in 450 452 encoding_check code_memory pc pc_plus_len a $\rightarrow$ … … 456 458 457 459 Intuitively, Lemma \texttt{fetch\_assembly\_pseudo} can be read as follows. 458 Suppose we expand the pseudoinstruction at \texttt{ppc} with the policy decision \texttt{sigma}, obtaining the list of machine code instructions \texttt{instrs}.460 Suppose we expand the pseudoinstruction at \texttt{ppc} with the policy, obtaining the list of machine code instructions \texttt{instrs}. 459 461 Suppose we also assemble the pseudoinstruction at \texttt{ppc} to obtain \texttt{a}, a list of bytes. 460 462 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. 461 463 462 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. 463 Again, we slightly simplify: 464 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: 464 465 \begin{lstlisting} 465 466 lemma fetch_assembly_pseudo2: … … 469 470 policy is correct for program $\rightarrow$ 470 471 $\forall$ppc. ppc < $\mid$snd program$\mid$ $\rightarrow$ 471 let $\langle$preamble, instr_list$\rangle$ := program in 472 let $\langle$labels, costs$\rangle$ := create_label_cost_map instr_list in 472 let $\langle$labels, costs$\rangle$ := create_label_cost_map program in 473 473 let $\langle$assembled, costs'$\rangle$ := $\pi_1$ (assembly program sigma policy) in 474 474 let cmem := load_code_memory assembled in 475 let $\langle$pi, newppc$\rangle$ := fetch_pseudo_instruction instr_listppc in475 let $\langle$pi, newppc$\rangle$ := fetch_pseudo_instruction program ppc in 476 476 let instructions := expand_pseudo_instruction policy ppc pi in 477 477 fetch_many cmem (policy newppc) (policy ppc) instructions. … … 481 481 482 482 We read \texttt{fetch\_assembly\_pseudo2} as follows. 483 Suppose we are given an assembly program which can be addressed by a 16bit word and a policy that is correct for this program. 483 484 Suppose we are able to successfully assemble an assembly program using \texttt{assembly} and produce a code memory, \texttt{cmem}. 484 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{ sigma} to expand pseudoinstructions.485 The fetched sequence corresponds to the expansion, according to \texttt{sigma}, of the pseudoinstruction.485 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. 486 The fetched sequence corresponds to the expansion, according to the policy, of the pseudoinstruction. 486 487 487 488 At first, the lemma appears to immediately imply the correctness of the assembler.
Note: See TracChangeset
for help on using the changeset viewer.