Changeset 1028 for src/ASM/CPP2011
 Timestamp:
 Jun 21, 2011, 2:08:45 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CPP2011/cpp2011.tex
r1027 r1028 278 278 This process is iterated for each pseudoinstruction, before the lists are flattened into a single bit list representation of the original assembly program. 279 279 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. 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 by proving the same independently for 281 \texttt{expand\_pseudo\_instruction} and for \texttt{assembly1}. 281 282 %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. 282 283 %Finally, we assemble all machine code instructions into machine codelists of bytesand prove once more that this process does not have an adverse effect on a program's semantics. 283 284 %By composition, we then have that the whole assembly process is semantics preserving. 284 285 285 This 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 determineif a short jump is possible.286 In 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. 287 287 That 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. 288 Thus, we must assemble each pseudoinstruction into machine code before moving on, and this must be eventually reflected in the proof too. 289 Therefore 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. 290 291 291 292 %  %
Note: See TracChangeset
for help on using the changeset viewer.