weblib/Cerco/ASM/ASM.ma

   1 include "ASM/BitVector.ma".
   2
   3 definition Identifier ≝ Word.
   4
   5 inductive addressing_mode: Type[0] ≝
   6   DIRECT: Byte → addressing_mode
   7 | INDIRECT: Bit → addressing_mode
   8 | EXT_INDIRECT: Bit → addressing_mode
   9 | REGISTER: BitVector 3 → addressing_mode
  10 | ACC_A: addressing_mode
  11 | ACC_B: addressing_mode
  12 | DPTR: addressing_mode
  13 | DATA: Byte → addressing_mode
  14 | DATA16: Word → addressing_mode
  15 | ACC_DPTR: addressing_mode
  16 | ACC_PC: addressing_mode
  17 | EXT_INDIRECT_DPTR: addressing_mode
  18 | INDIRECT_DPTR: addressing_mode
  19 | CARRY: addressing_mode
  20 | BIT_ADDR: Byte → addressing_mode
  21 | N_BIT_ADDR: Byte → addressing_mode
  22 | RELATIVE: Byte → addressing_mode
  23 | ADDR11: Word11 → addressing_mode
  24 | ADDR16: Word → addressing_mode.
  25
  26 (* dpm: renamed register to registr to avoid clash with brian's types *)
  27 inductive addressing_mode_tag : Type[0] ≝
  28   direct: addressing_mode_tag
  29 | indirect: addressing_mode_tag
  30 | ext_indirect: addressing_mode_tag
  31 | registr: addressing_mode_tag
  32 | acc_a: addressing_mode_tag
  33 | acc_b: addressing_mode_tag
  34 | dptr: addressing_mode_tag
  35 | data: addressing_mode_tag
  36 | data16: addressing_mode_tag
  37 | acc_dptr: addressing_mode_tag
  38 | acc_pc: addressing_mode_tag
  39 | ext_indirect_dptr: addressing_mode_tag
  40 | indirect_dptr: addressing_mode_tag
  41 | carry: addressing_mode_tag
  42 | bit_addr: addressing_mode_tag
  43 | n_bit_addr: addressing_mode_tag
  44 | relative: addressing_mode_tag
  45 | addr11: addressing_mode_tag
  46 | addr16: addressing_mode_tag.
  47
  48 definition eq_a ≝
  49   λa, b: addressing_mode_tag.
  50     match a with
  51       [ direct ⇒ match b with [ direct ⇒ true | _ ⇒ false ]
  52       | indirect ⇒ match b with [ indirect ⇒ true | _ ⇒ false ]
  53       | ext_indirect ⇒ match b with [ ext_indirect ⇒ true | _ ⇒ false ]
  54       | registr ⇒ match b with [ registr ⇒ true | _ ⇒ false ]
  55       | acc_a ⇒ match b with [ acc_a ⇒ true | _ ⇒ false ]
  56       | acc_b ⇒ match b with [ acc_b ⇒ true | _ ⇒ false ]
  57       | dptr ⇒ match b with [ dptr ⇒ true | _ ⇒ false ]
  58       | data ⇒ match b with [ data ⇒ true | _ ⇒ false ]
  59       | data16 ⇒ match b with [ data16 ⇒ true | _ ⇒ false ]
  60       | acc_dptr ⇒ match b with [ acc_dptr ⇒ true | _ ⇒ false ]
  61       | acc_pc ⇒ match b with [ acc_pc ⇒ true | _ ⇒ false ]
  62       | ext_indirect_dptr ⇒ match b with [ ext_indirect_dptr ⇒ true | _ ⇒ false ]
  63       | indirect_dptr ⇒ match b with [ indirect_dptr ⇒ true | _ ⇒ false ]
  64       | carry ⇒ match b with [ carry ⇒ true | _ ⇒ false ]
  65       | bit_addr ⇒ match b with [ bit_addr ⇒ true | _ ⇒ false ]
  66       | n_bit_addr ⇒ match b with [ n_bit_addr ⇒ true | _ ⇒ false ]
  67       | relative ⇒ match b with [ relative ⇒ true | _ ⇒ false ]
  68       | addr11 ⇒ match b with [ addr11 ⇒ true | _ ⇒ false ]
  69       | addr16 ⇒ match b with [ addr16 ⇒ true | _ ⇒ false ]
  70       ].
  71
  72 (* to avoid expansion... *)
  73 let rec is_a (d:addressing_mode_tag) (A:addressing_mode) on d ≝
  74   match d with
  75    [ direct ⇒ match A with [ DIRECT _ ⇒ true | _ ⇒ false ]
  76    | indirect ⇒ match A with [ INDIRECT _ ⇒ true | _ ⇒ false ]
  77    | ext_indirect ⇒ match A with [ EXT_INDIRECT _ ⇒ true | _ ⇒ false ]
  78    | registr ⇒ match A with [ REGISTER _ ⇒ true | _ ⇒ false ]
  79    | acc_a ⇒ match A with [ ACC_A ⇒ true | _ ⇒ false ]
  80    | acc_b ⇒ match A with [ ACC_B ⇒ true | _ ⇒ false ]
  81    | dptr ⇒ match A with [ DPTR ⇒ true | _ ⇒ false ]
  82    | data ⇒ match A with [ DATA _ ⇒ true | _ ⇒ false ]
  83    | data16 ⇒ match A with [ DATA16 _ ⇒ true | _ ⇒ false ]
  84    | acc_dptr ⇒ match A with [ ACC_DPTR ⇒ true | _ ⇒ false ]
  85    | acc_pc ⇒ match A with [ ACC_PC ⇒ true | _ ⇒ false ]
  86    | ext_indirect_dptr ⇒ match A with [ EXT_INDIRECT_DPTR ⇒ true | _ ⇒ false ]
  87    | indirect_dptr ⇒ match A with [ INDIRECT_DPTR ⇒ true | _ ⇒ false ]
  88    | carry ⇒ match A with [ CARRY ⇒ true | _ ⇒ false ]
  89    | bit_addr ⇒ match A with [ BIT_ADDR _ ⇒ true | _ ⇒ false ]
  90    | n_bit_addr ⇒ match A with [ N_BIT_ADDR _ ⇒ true | _ ⇒ false ]
  91    | relative ⇒ match A with [ RELATIVE _ ⇒ true | _ ⇒ false ]
  92    | addr11 ⇒ match A with [ ADDR11 _ ⇒ true | _ ⇒ false ]
  93    | addr16 ⇒ match A with [ ADDR16 _ ⇒ true | _ ⇒ false ]
  94    ].
  95
  96
  97 let rec is_in n (l: Vector addressing_mode_tag n) (A:addressing_mode) on l : bool ≝
  98  match l return λm.λ_:Vector addressing_mode_tag m.bool with
  99   [ VEmpty ⇒ false
 100   | VCons m he (tl: Vector addressing_mode_tag m) ⇒
 101      is_a he A ∨ is_in ? tl A ].
 102
 103 record subaddressing_mode (n) (l: Vector addressing_mode_tag (S n)) : Type[0] ≝
 104 {
 105   subaddressing_modeel:> addressing_mode;
 106   subaddressing_modein: bool_to_Prop (is_in ? l subaddressing_modeel)
 107 }.
 108
 109 coercion subaddressing_mode : ∀n.∀l:Vector addressing_mode_tag (S n).Type[0]
 110  ≝ subaddressing_mode on _l: Vector addressing_mode_tag (S ?) to Type[0].
 111
 112 coercion mk_subaddressing_mode :
 113  ∀n.∀l:Vector addressing_mode_tag (S n).∀a:addressing_mode.
 114   ∀p:bool_to_Prop (is_in ? l a).subaddressing_mode n l
 115  ≝ mk_subaddressing_mode on a:addressing_mode to subaddressing_mode ? ?.
 116
 117 inductive preinstruction (A: Type[0]) : Type[0] ≝
 118   ADD: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A
 119 | ADDC: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A
 120 | SUBB: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A
 121 | INC: [[ acc_a ; registr ; direct ; indirect ; dptr ]] → preinstruction A
 122 | DEC: [[ acc_a ; registr ; direct ; indirect ]] → preinstruction A
 123 | MUL: [[acc_a]] → [[acc_b]] → preinstruction A
 124 | DIV: [[acc_a]] → [[acc_b]] → preinstruction A
 125 | DA: [[acc_a]] → preinstruction A
 126
 127 (* conditional jumps *)
 128 | JC: A → preinstruction A
 129 | JNC: A → preinstruction A
 130 | JB: [[bit_addr]] → A → preinstruction A
 131 | JNB: [[bit_addr]] → A → preinstruction A
 132 | JBC: [[bit_addr]] → A → preinstruction A
 133 | JZ: A → preinstruction A
 134 | JNZ: A → preinstruction A
 135 | CJNE:
 136    [[acc_a]] × [[direct; data]] ⊎ [[registr; indirect]] × [[data]] → A → preinstruction A
 137 | DJNZ: [[registr ; direct]] → A → preinstruction A
 138  (* logical operations *)
 139 | ANL:
 140    [[acc_a]] × [[ registr ; direct ; indirect ; data ]] ⊎
 141    [[direct]] × [[ acc_a ; data ]] ⊎
 142    [[carry]] × [[ bit_addr ; n_bit_addr]] → preinstruction A
 143 | ORL:
 144    [[acc_a]] × [[ registr ; data ; direct ; indirect ]] ⊎
 145    [[direct]] × [[ acc_a ; data ]] ⊎
 146    [[carry]] × [[ bit_addr ; n_bit_addr]] → preinstruction A
 147 | XRL:
 148    [[acc_a]] × [[ data ; registr ; direct ; indirect ]] ⊎
 149    [[direct]] × [[ acc_a ; data ]] → preinstruction A
 150 | CLR: [[ acc_a ; carry ; bit_addr ]] → preinstruction A
 151 | CPL: [[ acc_a ; carry ; bit_addr ]] → preinstruction A
 152 | RL: [[acc_a]] → preinstruction A
 153 | RLC: [[acc_a]] → preinstruction A
 154 | RR: [[acc_a]] → preinstruction A
 155 | RRC: [[acc_a]] → preinstruction A
 156 | SWAP: [[acc_a]] → preinstruction A
 157
 158  (* data transfer *)
 159 | MOV:
 160     [[acc_a]] × [[ registr ; direct ; indirect ; data ]] ⊎
 161     [[ registr ; indirect ]] × [[ acc_a ; direct ; data ]] ⊎
 162     [[direct]] × [[ acc_a ; registr ; direct ; indirect ; data ]] ⊎
 163     [[dptr]] × [[data16]] ⊎
 164     [[carry]] × [[bit_addr]] ⊎
 165     [[bit_addr]] × [[carry]] → preinstruction A
 166 | MOVX:
 167     [[acc_a]] × [[ ext_indirect ; ext_indirect_dptr ]] ⊎
 168     [[ ext_indirect ; ext_indirect_dptr ]] × [[acc_a]] → preinstruction A
 169 | SETB: [[ carry ; bit_addr ]] → preinstruction A
 170 | PUSH: [[direct]] → preinstruction A
 171 | POP: [[direct]] → preinstruction A
 172 | XCH: [[acc_a]] → [[ registr ; direct ; indirect ]] → preinstruction A
 173 | XCHD: [[acc_a]] → [[indirect]] → preinstruction A
 174
 175  (* program branching *)
 176 | RET: preinstruction A
 177 | RETI: preinstruction A
 178 | NOP: preinstruction A.
 179
 180 inductive instruction: Type[0] ≝
 181   | ACALL: [[addr11]] → instruction
 182   | LCALL: [[addr16]] → instruction
 183   | AJMP: [[addr11]] → instruction
 184   | LJMP: [[addr16]] → instruction
 185   | SJMP: [[relative]] → instruction
 186   | JMP: [[indirect_dptr]] → instruction
 187   | MOVC: [[acc_a]] → [[ acc_dptr ; acc_pc ]] → instruction
 188   | RealInstruction: preinstruction [[ relative ]] → instruction.
 189
 190 coercion RealInstruction: ∀p: preinstruction [[ relative ]]. instruction ≝
 191   RealInstruction on _p: preinstruction ? to instruction.
 192
 193 inductive pseudo_instruction: Type[0] ≝
 194   | Instruction: preinstruction Identifier → pseudo_instruction
 195   | Comment: String → pseudo_instruction
 196   | Cost: Identifier → pseudo_instruction
 197   | Jmp: Identifier → pseudo_instruction
 198   | Call: Identifier → pseudo_instruction
 199   | Mov: [[dptr]] → Identifier → pseudo_instruction.
 200
 201 definition labelled_instruction ≝ option Identifier × pseudo_instruction.
 202 definition preamble ≝ list (Identifier × nat).
 203 definition assembly_program ≝ list instruction.
 204 definition pseudo_assembly_program ≝ preamble × (list labelled_instruction).