Changeset 1011


Ignore:
Timestamp:
Jun 20, 2011, 6:39:10 PM (8 years ago)
Author:
mulligan
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CPP2011/cpp-2011.tex

    r1010 r1011  
    342342definition expand_pseudo_instruction:
    343343  ∀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 MCS-51'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
    351347\begin{lstlisting}
    352348axiom assembly_ok: ∀program,assembled,costs,labels.
     
    386382Lemma \texttt{fetch\_assembly\_pseudo} establishes a basic relationship between \texttt{expand\_pseudo\_instruction} and \texttt{assembly\_1\_pseudoinstruction}:
    387383\begin{lstlisting}
    388 lemma fetch_assembly_pseudo: $\forall$program, ppc, lk_labels, lk_dlabels.
     384lemma fetch_assembly_pseudo: $\forall$p. $\forall$pol: policy p. $\forall$ppc, lk_lbl, lk_dlbl.
    389385  $\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}
     394Here, \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.
    401395We assemble a single pseudoinstruction with \texttt{assembly\_1\_pseudoinstruction}, which internally calls \texttt{jump\_expansion} and \texttt{expand\_pseudo\_instruction}.
    402396The function \texttt{fetch\_many} fetches multiple machine code instructions from code memory and performs some routine checks.
     
    410404At first sight, Lemma \texttt{fetch\_assembly\_pseudo2} appears to nearly establish the correctness of the assembler:
    411405\begin{lstlisting}
    412 lemma fetch_assembly_pseudo2: $\forall$program, assembled, costs, labels.
     406lemma fetch_assembly_pseudo2: $\forall$p. $\forall$pol: policy p. $\forall$assembled, costs, labels.
    413407  Some $\ldots$ $\langle$labels, costs$\rangle$ = build_maps program $\rightarrow$
    414408  Some $\ldots$ $\langle$assembled, costs$\rangle$ = assembly program $\rightarrow$ $\forall$ppc.
Note: See TracChangeset for help on using the changeset viewer.