# Changeset 2339 for Papers/cpp-asm-2012

Ignore:
Timestamp:
Sep 26, 2012, 12:24:53 PM (8 years ago)
Message:

Got to page 8/9.

File:
1 edited

Unmodified
Removed
• ## Papers/cpp-asm-2012/cpp-2012-asm.tex

 r2329 definition execute_1: $\forall$cm. Status cm $\rightarrow$ Status cm := $\ldots$ \end{lstlisting} Here \texttt{Status} is parameterised by \texttt{cm}, a code memory represented as a trie. %The function \texttt{execute} allows one to execute an arbitrary, but fixed (due to Matita's normalisation requirement) number of steps of a program. The function \texttt{execute\_1} closely matches the operation of the MCS-51 hardware, as described by a Siemen's manufacturer's data sheet (specifically, this one~\cite{siemens:2011}). inductive preinstruction (A: Type[0]): Type[0] := | ADD: $\llbracket$acc_a$\rrbracket$ → $\llbracket$registr; direct; indirect; data$\rrbracket$ $\rightarrow$ preinstruction A | INC: $\llbracket$ acc_a; registr; direct; indirect; dptr$\rrbracket$ $\rightarrow$ preinstruction A | DEC: $\llbracket$acc_a; registr; direct; indirect$\rrbracket$ $\rightarrow$ preinstruction A | JB: $\llbracket$bit_addr$\rrbracket$ $\rightarrow$ A $\rightarrow$ preinstruction A | ... Once decoded, execution proceeds by a case analysis on the decoded instruction, following the operation of the hardware. For example, the \texttt{DEC} instruction (decrement') is implemented as follows: \begin{lstlisting} | DEC addr $\Rightarrow$ \begin{lstlisting} definition execute_1_pseudo_instruction: (Word $\rightarrow$ nat $\times$ nat) $\rightarrow$ $\forall$cm. PseudoStatus cm $\rightarrow$ PseudoStatus cm := $\ldots$ \end{lstlisting} Notice, here, that the emulation function for assembly programs takes an additional argument over \texttt{execute\_1}. This is a function that maps program counters (at the assembly level) to pairs of natural numbers representing the number of clock ticks that the pseudoinstruction needs to execute, post expansion. $\forall$cm. ($\forall$ppc: Word. ppc < $\mid$snd cm$\mid$ $\rightarrow$ nat $\times$ nat) $\rightarrow$ $\forall$s:PseudoStatus cm. program_counter $\ldots$ s < $\mid$snd cm$\mid$ $\rightarrow$ PseudoStatus cm := $\ldots$ \end{lstlisting} The type of \texttt{execute\_1\_pseudo\_instruction} is interesting. Note here that our representation of code memory \texttt{cm} is no longer a bitvector trie of bytes, but a list of pseudoinstructions. Further, we take in a function that maps program counters (at the assembly level) to pairs of natural numbers representing the number of clock ticks that the pseudoinstructions needs to execute, post expansion. We call this function a \emph{costing}, and note that the costing is induced by the particular strategy we use to expand pseudoinstructions. If we change how we expand conditional jumps to labels, for instance, then the costing needs to change, hence \texttt{execute\_1\_pseudo\_instruction}'s parametricity in the costing. This costing function expects a proof, at its second argument, stating that the program counter falls within the bounds of the pseudoprogram. A similar invariant holds of the pseudoprogram counter passed to the \texttt{execute\_1\_pseudo\_instruction} function. The costing returns \emph{pairs} of natural numbers because, in the case of expanding conditional jumps to labels, the expansion of the true branch' and `false branch' may differ in execution time. Execution proceeds by first fetching from pseudo-code memory using the program counter---treated as an index into the pseudoinstruction list. This index is always guaranteed to be within the bounds of the pseudoinstruction list due to the dependent type placed on the function. No decoding is required. We then proceed by case analysis over the pseudoinstruction, reusing the code for object code for all instructions present in the MCS-51's instruction set. \begin{lstlisting} definition assembly: $\forall$p: pseudo_assembly_program. $\forall$sigma: Word $\rightarrow$ Word. $\forall$policy: Word $\rightarrow$ bool. $\Sigma$res:list Byte $\times$ (BitVectorTrie costlabel 16). sigma_meets_specification p sigma policy $\rightarrow$ let $\langle$preamble, instr_list$\rangle$ := p in |instr_list| < 2^16 $\rightarrow$ let $\langle$assembled,costs$\rangle$ := res in $\forall$ppc. $\forall$ppc_ok:nat_of_bitvector $\ldots$ ppc < |instr_list|. let $\langle$pi,newppc$\rangle$ := fetch_pseudo_instruction instr_list ppc ppc_ok in let $\langle$l,a$\rangle$ := assembly_1_pseudoinstruction $\ldots$ sigma policy ppc $\ldots$ pi in $\forall$j:nat. j < |a| nth j a = nth (add $\ldots$ (sigma ppc) (bitvector_of_nat ? j))) assembled $\forall$program: pseudo_assembly_program. $\forall$policy. $\Sigma$assembled: list Byte $\times$ (BitVectorTrie costlabel 16). policy is correct for program $\rightarrow$ $\mid$program$\mid$ < $2^{16}$ $\rightarrow$ $\mid$fst assembled$\mid$ < $2^{16}$ $\wedge$ policy ($\mid$program$\mid$) = $\mid$fst assembled$\mid$ $\vee$ policy ($\mid$program$\mid$) = 0 $\wedge$ $\mid$fst assembled$\mid$ = $2^{16}$ $\wedge$ $\forall$ppc: pseudo\_program\_counter such that ppc < $2^{16}$. let pseudo_instr := fetch from program at ppc in let assembled_i := assemble pseudo_instr in $\mid$assembled_i$\mid$ $\leq$ $2^{16}$ $\wedge$ $\forall$n: nat such that n < $\mid$assembled_i$\mid$. $\exists$k: nat. nth assembled_i n = nth assembled (policy ppc + k). \end{lstlisting} In plain words, the type of \texttt{assembly} states the following.
Note: See TracChangeset for help on using the changeset viewer.