# Changeset 2345 for Papers/cpp-asm-2012/cpp-2012-asm.tex

Ignore:
Timestamp:
Sep 26, 2012, 2:57:50 PM (8 years ago)
Message:

...

File:
1 edited

### Legend:

Unmodified
 r2344 \label{sect.the.proof} The aim of the section is to explain the main ideas and steps of the certified proof of correctness for an optimizing assembler for the MCS-8051. The formalization is available at~\url{http://cerco.cs.unibo.it}. In Section~\ref{subsect.machine.code.semantics} we sketch an operational semantics (a realistic and efficient emulator) for the MCS-8051. We also introduce a syntax for decoded instructions that will be reused for the assembly language. In Section~\ref{subsect.assembly.code.semantics} we describe the assembly code language and operational semantics. The latter is parametric in the cost model that will be induced by the assembler. It fully reuses the semantics of the machine code on all real'' (i.e. non pseudo) instructions. Branch displacement policies are introduced in Section~\ref{subsect.the.assembler} where we also describe the assembler as a function over policies as previously described. The proof of correctness of the assembler consists in showing that the object code given in output together with a cost model for the source program simulates the source program executed using that cost model. The proof can be divided into two main lemmas. The first is correctness with respect to fetching, described in Section~\ref{subsect.total.correctness.of.the.assembler}. It roughly states that one step of fetching at the assembly level that returns the decoded instruction $I$ is simulated by $n$ steps of fetching at object level that return instructions $J_1,\ldots,J_n$, where $J_1,\ldots,J_n$ is, among the possible expansions of $I$, the one picked by the policy. The second lemma shows that $J_1,\ldots,J_n$ simulates $I$ but only if the $I$ is well-behaved, i.e. it manipulates addresses in ways that are anticipated in the correctness proof. To keep track of the well-behaved ways, we couple the assembly status with a map that records where addresses are currently stored in memory or in the registers. Then we introduce a dynamic checking function that inspects the assembly status and the map to determine if the operation is well behaved. A positive answer is the pre-condition of the lemma. The second lemma is part of Section~\ref{subsect.total.correctness.for.well.behaved.assembly.programs} where we also establish \emph{total correctness} of our assembler as a composition of the two lemmas: programs that are well behaved when executed under the cost model induced by the compiler are correctly simulated by the compiled code. % ---------------------------------------------------------------------------- % % SECTION                                                                      %