# Changeset 809

Ignore:
Timestamp:
May 16, 2011, 4:32:36 PM (9 years ago)
Message:

more changes to get everything to fit correctly. gone past 8 pg limit

File:
1 edited

### Legend:

Unmodified
 r808 mathescape=true, } \lstset{language=matita-ocaml,basicstyle=\small\tt,columns=flexible,breaklines=false, \lstset{language=matita-ocaml,basicstyle=\footnotesize\tt,columns=flexible,breaklines=false, keywordstyle=\bfseries, %\color{red}\bfseries, keywordstyle=[2]\bfseries, %\color{blue}, type nibble = [Sixteen] vect type byte = [Eight] vect $\color{blue}{\mathtt{let}}$ split_word w = split_nth 4 w $\color{blue}{\mathtt{let}}$ split_byte b = split_nth 2 b let split_word w = split_nth 4 w let split_byte b = split_nth 2 b \end{lstlisting}} \end{minipage} \begin{lstlisting} let rec split (A: Type[0]) (m,n: nat) on m: Vector A (plus m n) $\rightarrow$ (Vector A m) $\times$ (Vector A n) := ... Vector A (m + n) $\rightarrow$ (Vector A m)$\times$(Vector A n) := ... \end{lstlisting} inductive BitVectorTrie (A: Type[0]): nat $\rightarrow$ Type[0] ≝ Leaf: A $\rightarrow$ BitVectorTrie A 0 | Node: ∀n. BitVectorTrie A n $\rightarrow$ BitVectorTrie A n $\rightarrow$ BitVectorTrie A (S n) | Node: ∀n. BitVectorTrie A n $\rightarrow$ BitVectorTrie A n $\rightarrow$ BitVectorTrie A (S n) | Stub: ∀n. BitVectorTrie A n. \end{lstlisting} The internal state of the Matita emulator is represented as a record: \begin{lstlisting} record Status: Type[0] ≝ { record Status: Type[0] := { code_memory: BitVectorTrie Byte 16; low_internal_ram: BitVectorTrie Byte 7; program_counter: Word; special_function_registers_8051: Vector Byte 19; special_function_registers_8052: Vector Byte 5; ...  }. ... }. \end{lstlisting} This record encapsulates the current memory contents, the program counter, the state of the current SFRs, and so on. These costs are taken from a Siemens Semiconductor Group data sheet for the MCS-51~\cite{siemens:2011}, and will likely vary between particular implementations. \begin{lstlisting} definition fetch: BitVectorTrie Byte 16 $\rightarrow$ Word $\rightarrow$ instruction $\times$ Word $\times$ nat definition fetch: BitVectorTrie Byte 16 $\rightarrow$ Word $\rightarrow$ instruction $\times$ Word $\times$ nat \end{lstlisting} Instruction are assembled to bit encodings by \texttt{assembly1}: A map associating memory locations and cost labels (see Subsection~\ref{subsect.computation.cost.traces}) is produced. \begin{lstlisting} definition assembly: assembly_program $\rightarrow$ option (list Byte $\times$ (BitVectorTrie String 16)) definition assembly: assembly_program $\rightarrow$ option (list Byte $\times$ (BitVectorTrie String 16)) \end{lstlisting} A single fetch-decode-execute cycle is performed by \texttt{execute\_1}: \texttt{execute\_1}: \begin{lstlisting} let rec execute (n: nat) (s: Status) on n: Status := ... let rec execute (n: nat) (s: Status): Status := ... \end{lstlisting} This differs from the O'Caml emulator, which executed a program indefinitely. \begin{lstlisting} type 'addr preinstruction = [ ADD of acc * [ reg | direct | indirect | data ] [ ADD of acc * [ reg | direct | indirect | data ] ... | MOV of (acc * [ reg | direct | indirect | data ], [ reg | indirect ] * [ acc | direct | data ], direct * [ acc | reg | direct | indirect | data ], dptr * data16, carry * bit, bit * carry ) union6 | MOV of (acc * [ reg| direct | indirect | data ], [ reg | indirect ] * [ acc | direct | data ], direct * [ acc | reg | direct | indirect | data ], dptr * data16, carry * bit, bit * carry ) union6 ... \end{lstlisting} We first provided an inductive data type representing all possible addressing modes, a type that functions will pattern match against: \begin{lstlisting} inductive addressing_mode: Type[0] ≝ inductive addressing_mode: Type[0] := DIRECT: Byte $\rightarrow$ addressing_mode | INDIRECT: Bit $\rightarrow$ addressing_mode The constructors of \texttt{addressing\_mode\_tag} are in one-to-one correspondence with the constructors of \texttt{addressing\_mode}: \begin{lstlisting} inductive addressing_mode_tag : Type[0] ≝ inductive addressing_mode_tag : Type[0] := direct: addressing_mode_tag | indirect: addressing_mode_tag The \texttt{is\_a} function checks if an \texttt{addressing\_mode} matches an \texttt{addressing\_mode\_tag}: \begin{lstlisting} let rec is_a (d: addressing_mode_tag) (A: addressing_mode) on d := match d with [ direct $\Rightarrow$ match A with [ DIRECT _ $\Rightarrow$ true | _ $\Rightarrow$ false ] | indirect $\Rightarrow$ match A with [ INDIRECT _ $\Rightarrow$ true | _ $\Rightarrow$ false ] let rec is_a (d: addressing_mode_tag) (A: addressing_mode) on d := match d with [ direct $\Rightarrow$ match A with [ DIRECT _ $\Rightarrow$ true | _ $\Rightarrow$ false ] | indirect $\Rightarrow$ match A with [ INDIRECT _ $\Rightarrow$ true | _ $\Rightarrow$ false ] ... \end{lstlisting} A \texttt{subaddressing\_mode} is an \emph{ad hoc} non-empty $\Sigma$-type of \texttt{addressing\_mode}s constrained to be in a set of tags: \begin{lstlisting} record subaddressing_mode n (l: Vector addressing_mode_tag (S n)): Type[0] := { subaddressing_modeel :> addressing_mode; subaddressing_modein: bool_to_Prop (is_in ? l subaddressing_modeel) }. record subaddressing_mode (n: nat) (l: Vector addressing_mode_tag (S n)): Type[0] := { subaddressing_modeel :> addressing_mode; subaddressing_modein: bool_to_Prop (is_in ? l subaddressing_modeel) }. \end{lstlisting} An implicit coercion is provided to promote vectors of tags (denoted with $\llbracket - \rrbracket$) to the corresponding \texttt{subaddressing\_mode} so that we can use a syntax close to that of O'Caml to specify \texttt{preinstruction}s: \begin{lstlisting} inductive preinstruction (A: Type[0]): Type[0] ≝ ADD: $\llbracket$ acc_a $\rrbracket$ $\rightarrow$ $\llbracket$ register; direct; indirect; data $\rrbracket$ $\rightarrow$ preinstruction A | ADDC: $\llbracket$ acc_a $\rrbracket$ $\rightarrow$ $\llbracket$ register; direct; indirect; data $\rrbracket$ $\rightarrow$ preinstruction A ADD: $\llbracket$acc_a$\rrbracket$ $\rightarrow$ $\llbracket$register;direct;indirect;data$\rrbracket$ $\rightarrow$ preinstruction A | ADDC: $\llbracket$acc_a$\rrbracket$ $\rightarrow$ $\llbracket$register;direct;indirect;data$\rrbracket$ $\rightarrow$ preinstruction A ... \end{lstlisting} For instance, consider \texttt{set\_arg\_16}, which expects only a \texttt{DPTR}: \begin{lstlisting} definition set_arg_16: Status $\rightarrow$ Word $\rightarrow$ $\llbracket$ dptr $\rrbracket$ $\rightarrow$ Status ≝ $~\lambda$s, v, a. match a return $\lambda$x. bool_to_Prop (is_in ? $\llbracket$ dptr $\rrbracket$ x) $\rightarrow$ ? with [ DPTR $\Rightarrow$ $\lambda$_: True. let 〈 bu, bl 〉 := split $\ldots$ eight eight v in let status := set_8051_sfr s SFR_DPH bu in let status := set_8051_sfr status SFR_DPL bl in status | _ $\Rightarrow$ $\lambda$_: False. $\bot$ ] $~$(subaddressing_modein $\ldots$ a). definition set_arg_16: Status $\rightarrow$ Word $\rightarrow$ $\llbracket$dptr$\rrbracket$ $\rightarrow$ Status := $~\lambda$s, v, a. match a return $\lambda$x. bool_to_Prop (is_in ? $\llbracket$dptr$\rrbracket$ x) $\rightarrow$ ? with [ DPTR $\Rightarrow$ $\lambda$_: True. let $\langle$bu, bl$\rangle$ := split $\ldots$ eight eight v in let status := set_8051_sfr s SFR_DPH bu in let status := set_8051_sfr status SFR_DPL bl in status | _ $\Rightarrow$ $\lambda$_: False. $\bot$ ] $~$(subaddressing_modein $\ldots$ a). \end{lstlisting} We give a proof (the expression \texttt{(subaddressing\_modein} $\ldots$ \texttt{a)}) that the argument $a$ is in the set $\llbracket$ \texttt{dptr} $\rrbracket$ to the \texttt{match} expression. \begin{lstlisting} type line = [ P1 of byte | P3 of byte | SerialBuff of [ Eight of byte | Nine of BitVectors.bit * byte ] ] [ P1 of byte | P3 of byte | SerialBuff of [ Eight of byte | Nine of BitVectors.bit * byte ] ] type continuation = [In of time * line * epsilon * continuation] option * [Out of (time -> line -> time * continuation)] [In of time * line * epsilon * continuation] option * [Out of (time -> line -> time * continuation)] \end{lstlisting} At each moment, the second projection of the continuation $k$ describes how the environment will react to an output event performed in the future by the processor.