Changeset 1028 for src/ASM/CPP2011


Ignore:
Timestamp:
Jun 21, 2011, 2:08:45 PM (8 years ago)
Author:
sacerdot
Message:

One more sentence restored and fitted in.

File:
1 edited

Legend:

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

    r1027 r1028  
    278278This process is iterated for each pseudoinstruction, before the lists are flattened into a single bit list representation of the original assembly program.
    279279
    280 %By inspecting the above diagram, it would appear that the best way to proceed with a proof that the assembly process does not change the semantics of an assembly program is via a decomposition of the problem into two subproblems.
     280By inspecting the above diagram, it would appear that the best way to proceed with a proof that the assembly process does not change the semantics of an assembly program is by proving the same independently for
     281\texttt{expand\_pseudo\_instruction} and for \texttt{assembly1}.
    281282%Namely, we first expand any and all pseudoinstructions into lists of machine instructions, and provide a proof that this process does not change our program's semantics.
    282283%Finally, we assemble all machine code instructions into machine code---lists of bytes---and prove once more that this process does not have an adverse effect on a program's semantics.
    283284%By composition, we then have that the whole assembly process is semantics preserving.
    284 
    285285This is a tempting approach to the proof, but ultimately the wrong approach.
    286 In particular, to expand a pseudoinstruction we need to know the address at which the expanded instructions will be located, for instance to determine if a short jump is possible.
     286In particular, to expand a pseudoinstruction we need to know the address at which the expanded instructions will be located, for instance to know if a short jump is possible.
    287287That address is a function of the \emph{machine code} generated for the pseudoinstructions already expanded.
    288 Thus, we must assemble each psedutoinstruction into machine code before moving on, and this must be eventually reflected in the proof of correctness.
    289 Therefore we will have lemmas proving correctness for \texttt{assembly1}, and for the composition of \texttt{expand\_pseudo\_instruction} and \texttt{assembly1}, but not for \texttt{expand\_pseudo\_instruction} alone.
     288Thus, we must assemble each pseudoinstruction into machine code before moving on, and this must be eventually reflected in the proof too.
     289Therefore we will have lemmas proving correctness for \texttt{assembly1}, and for the composition of \texttt{assembly1} and
     290\texttt{expand\_pseudo\_instruction}, but not for \texttt{expand\_pseudo\_instruction} alone.
    290291
    291292% ---------------------------------------------------------------------------- %
Note: See TracChangeset for help on using the changeset viewer.