 Timestamp:
 Jun 20, 2011, 6:39:10 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CPP2011/cpp2011.tex
r1010 r1011 342 342 definition expand_pseudo_instruction: 343 343 ∀lookup_labels, lookup_datalabels, pc, policy_decision. 344 pseudo_instruction $\rightarrow$ option list instruction := $\ldots$ 345 \end{lstlisting} 346 Under the assumption that a correct policy exists, \texttt{expand\_pseudo\_instruction} should never fail, and therefore the option type may be dispensed with. 347 This is because the only failure conditions for \texttt{expand\_pseudo\_instruction} result from trying to expand a pseudoinstruction into an `impossible' combination of machine code instructions. 348 For instance, if the policy decision dictates that we should expand a \texttt{Call} pseudoinstruction into a `short jump', then we fail, as the MCS51's instruction set only features instructions \texttt{ACALL} and \texttt{LCALL}. 349 350 % dpm todo 344 pseudo_instruction $\rightarrow$ list instruction := $\ldots$ 345 \end{lstlisting} 346 351 347 \begin{lstlisting} 352 348 axiom assembly_ok: ∀program,assembled,costs,labels. … … 386 382 Lemma \texttt{fetch\_assembly\_pseudo} establishes a basic relationship between \texttt{expand\_pseudo\_instruction} and \texttt{assembly\_1\_pseudoinstruction}: 387 383 \begin{lstlisting} 388 lemma fetch_assembly_pseudo: $\forall$p rogram, ppc, lk_labels, lk_dlabels.384 lemma fetch_assembly_pseudo: $\forall$p. $\forall$pol: policy p. $\forall$ppc, lk_lbl, lk_dlbl. 389 385 $\forall$pi, code_memory, len, assembled, instructions, pc. 390 let jexp := jump_expansion ppc program in 391 let exp := 392 expand_pseudo_instruction lk_labels lk_dlabels pc jexp pi 393 let ass := 394 assembly_1_pseudoinstruction program ppc pc lk_labels lk_dlabels pi in 395 Some ? instructions = exp $\rightarrow$ 396 Some $\ldots$ $\langle$len, assembled$\rangle$ = ass $\rightarrow$ 397 encoding_check code_memory pc (pc + len) assembled $\rightarrow$ 398 fetch_many code_memory (pc + len) pc instructions. 399 \end{lstlisting} 400 Here, \texttt{len} is the number of machine code instructions the pseudoinstruction at hand has been expanded into, \texttt{encoding\_check} is a recursive function that checks for any possible corruption of the code memory, resulting from expanding the pseudoinstruction. 386 let exp := pol ppc in 387 let expand := expand_pseudo_instruction lk_lbls lk_dlbl pc exp pi in 388 let ass := assembly_1_pseudoinstruction p pol ppc pc lk_lbl lk_dlbl pi in 389 Some ? instructions = expand $\rightarrow$ 390 Some $\ldots$ $\langle$len, assembled$\rangle$ = ass $\rightarrow$ 391 encoding_check code_memory pc (pc + len) assembled $\rightarrow$ 392 fetch_many code_memory (pc + len) pc instructions. 393 \end{lstlisting} 394 Here, \texttt{len} is the number of machine code instructions the pseudoinstruction at hand has been expanded into, and \texttt{encoding\_check} is a recursive function that checks that assembled machine code is correctly stored in code memory. 401 395 We assemble a single pseudoinstruction with \texttt{assembly\_1\_pseudoinstruction}, which internally calls \texttt{jump\_expansion} and \texttt{expand\_pseudo\_instruction}. 402 396 The function \texttt{fetch\_many} fetches multiple machine code instructions from code memory and performs some routine checks. … … 410 404 At first sight, Lemma \texttt{fetch\_assembly\_pseudo2} appears to nearly establish the correctness of the assembler: 411 405 \begin{lstlisting} 412 lemma fetch_assembly_pseudo2: $\forall$p rogram,assembled, costs, labels.406 lemma fetch_assembly_pseudo2: $\forall$p. $\forall$pol: policy p. $\forall$assembled, costs, labels. 413 407 Some $\ldots$ $\langle$labels, costs$\rangle$ = build_maps program $\rightarrow$ 414 408 Some $\ldots$ $\langle$assembled, costs$\rangle$ = assembly program $\rightarrow$ $\forall$ppc.
Note: See TracChangeset
for help on using the changeset viewer.