# Changeset 2380

Ignore:
Timestamp:
Sep 28, 2012, 6:35:12 PM (7 years ago)
Message:

Some spelling changes to Britishi*S*e the text.

File:
1 edited

### Legend:

Unmodified
 r2379 % SECTION                                                                      % % ---------------------------------------------------------------------------- % \section{Certification of an optimizing assembler} \section{Certification of an optimising assembler} \label{sect.the.proof} The MCS-51 has many operand modes, but an unorthogonal instruction set: every opcode is only enable for a finite subset of the possible operand modes. Here we exploit dependent types and an implicit coercion to synthesize Here we exploit dependent types and an implicit coercion to synthesise the type of arguments of opcodes from a vector of names of operand modes. For example, \texttt{ACC} has two operands, the first one constrained to be The function that implements the tracking map update, previously denoted by $\llbracket - \rrbracket$, is called \texttt{next\_internal\_pseudo\_address\_map} in the formalisation. For the time being, we accept as good behaviours address copying amongst memory cells and the accumulator (\texttt{MOV} pseudoinstruction) and the use of the \texttt{CJNE} conditional jump that compares two addresses and jumps to a given label if the two labels are equal. Moreover, \texttt{RET} to return from a function call is well behaved iff the lower and upper parts of the return address, fetched from the stack, are both marked as complementary parts of the same address (i.e. \texttt{h} is tracked as \texttt{$\langle$Upper,l$\rangle$} and \texttt{l} is tracked as \texttt{$\langle$Lower,h$\rangle$}. Moreover, \texttt{RET} to return from a function call is well-behaved iff the lower and upper parts of the return address, fetched from the stack, are both marked as complementary parts of the same address (i.e. \texttt{h} is tracked as \texttt{$\langle$Upper,l$\rangle$} and \texttt{l} is tracked as \texttt{$\langle$Lower,h$\rangle$}. These three operations are sufficient to implement the backend of the CerCo compiler. Other good behaviours could be recognised in the future, for instance in order to implement the C branch statement efficiently. The statement is standard for forward simulation, but restricted to \texttt{PseudoStatuses} \texttt{ps} whose tracking map is \texttt{M} and who are well-behaved according to \texttt{internal\_pseudo\_address\_map} \texttt{M}. The \texttt{ticks\_of program policy} function returns the costing computed by assembling the \texttt{program} using the given \texttt{policy}. An obvious corollary of \texttt{main\_thm} is the correct simulation of $n$ well behaved steps by some number of steps $m$, where each step must be well-behaved with respect to the tracking map returned by the previous step. An obvious corollary of \texttt{main\_thm} is the correct simulation of $n$ well-behaved steps by some number of steps $m$, where each step must be well-behaved with respect to the tracking map returned by the previous step. % ---------------------------------------------------------------------------- % We may compare our work to an `industrial grade' assembler for the MCS-51: SDCC~\cite{sdcc:2011}, the only open source C compiler that targets the MCS-51 instruction set. It appears that all pseudojumps in SDCC assembly are expanded to \texttt{LJMP} instructions, the worst possible jump expansion policy from an efficiency point of view. Note that this policy is the only possible policy \emph{in theory} that makes every assembly program well behaved, preserving its the semantics during the assembly process. This comes at the expense of assembler completeness as the generated program may be too large for code memory, there being a trade-off between the completeness of the assembler and the efficiency of the assembled program. Note that this policy is the only possible policy \emph{in theory} that makes every assembly program well-behaved, preserving its the semantics during the assembly process. This comes at the expense of assembler completeness as the generated program may be too large for code memory, there being a trade-off between the completeness of the assembler and the efficiency of the assembled program. The definition and proof of a terminating, correct jump expansion policy is described elsewhere~\cite{boender:correctness:2012}.