[985] | 1 | include "ASM/BitVector.ma". |
---|
[1515] | 2 | include "common/Identifiers.ma". |
---|
| 3 | include "common/CostLabel.ma". |
---|
[1882] | 4 | include "common/LabelledObjects.ma". |
---|
[475] | 5 | |
---|
[1515] | 6 | axiom ASMTag : String. |
---|
| 7 | definition Identifier ≝ identifier ASMTag. |
---|
| 8 | definition toASM_ident : ∀tag. identifier tag → Identifier ≝ λt,i. match i with [ an_identifier id ⇒ an_identifier ASMTag id ]. |
---|
[985] | 9 | |
---|
[475] | 10 | inductive addressing_mode: Type[0] ≝ |
---|
| 11 | DIRECT: Byte → addressing_mode |
---|
| 12 | | INDIRECT: Bit → addressing_mode |
---|
| 13 | | EXT_INDIRECT: Bit → addressing_mode |
---|
[698] | 14 | | REGISTER: BitVector 3 → addressing_mode |
---|
[475] | 15 | | ACC_A: addressing_mode |
---|
| 16 | | ACC_B: addressing_mode |
---|
| 17 | | DPTR: addressing_mode |
---|
| 18 | | DATA: Byte → addressing_mode |
---|
| 19 | | DATA16: Word → addressing_mode |
---|
| 20 | | ACC_DPTR: addressing_mode |
---|
| 21 | | ACC_PC: addressing_mode |
---|
| 22 | | EXT_INDIRECT_DPTR: addressing_mode |
---|
| 23 | | INDIRECT_DPTR: addressing_mode |
---|
| 24 | | CARRY: addressing_mode |
---|
| 25 | | BIT_ADDR: Byte → addressing_mode |
---|
| 26 | | N_BIT_ADDR: Byte → addressing_mode |
---|
| 27 | | RELATIVE: Byte → addressing_mode |
---|
| 28 | | ADDR11: Word11 → addressing_mode |
---|
| 29 | | ADDR16: Word → addressing_mode. |
---|
| 30 | |
---|
[757] | 31 | (* dpm: renamed register to registr to avoid clash with brian's types *) |
---|
[475] | 32 | inductive addressing_mode_tag : Type[0] ≝ |
---|
| 33 | direct: addressing_mode_tag |
---|
| 34 | | indirect: addressing_mode_tag |
---|
| 35 | | ext_indirect: addressing_mode_tag |
---|
[757] | 36 | | registr: addressing_mode_tag |
---|
[475] | 37 | | acc_a: addressing_mode_tag |
---|
| 38 | | acc_b: addressing_mode_tag |
---|
| 39 | | dptr: addressing_mode_tag |
---|
| 40 | | data: addressing_mode_tag |
---|
| 41 | | data16: addressing_mode_tag |
---|
| 42 | | acc_dptr: addressing_mode_tag |
---|
| 43 | | acc_pc: addressing_mode_tag |
---|
| 44 | | ext_indirect_dptr: addressing_mode_tag |
---|
| 45 | | indirect_dptr: addressing_mode_tag |
---|
| 46 | | carry: addressing_mode_tag |
---|
| 47 | | bit_addr: addressing_mode_tag |
---|
| 48 | | n_bit_addr: addressing_mode_tag |
---|
| 49 | | relative: addressing_mode_tag |
---|
| 50 | | addr11: addressing_mode_tag |
---|
| 51 | | addr16: addressing_mode_tag. |
---|
| 52 | |
---|
| 53 | definition eq_a ≝ |
---|
| 54 | λa, b: addressing_mode_tag. |
---|
| 55 | match a with |
---|
| 56 | [ direct ⇒ match b with [ direct ⇒ true | _ ⇒ false ] |
---|
| 57 | | indirect ⇒ match b with [ indirect ⇒ true | _ ⇒ false ] |
---|
| 58 | | ext_indirect ⇒ match b with [ ext_indirect ⇒ true | _ ⇒ false ] |
---|
[757] | 59 | | registr ⇒ match b with [ registr ⇒ true | _ ⇒ false ] |
---|
[475] | 60 | | acc_a ⇒ match b with [ acc_a ⇒ true | _ ⇒ false ] |
---|
| 61 | | acc_b ⇒ match b with [ acc_b ⇒ true | _ ⇒ false ] |
---|
| 62 | | dptr ⇒ match b with [ dptr ⇒ true | _ ⇒ false ] |
---|
| 63 | | data ⇒ match b with [ data ⇒ true | _ ⇒ false ] |
---|
| 64 | | data16 ⇒ match b with [ data16 ⇒ true | _ ⇒ false ] |
---|
| 65 | | acc_dptr ⇒ match b with [ acc_dptr ⇒ true | _ ⇒ false ] |
---|
| 66 | | acc_pc ⇒ match b with [ acc_pc ⇒ true | _ ⇒ false ] |
---|
| 67 | | ext_indirect_dptr ⇒ match b with [ ext_indirect_dptr ⇒ true | _ ⇒ false ] |
---|
| 68 | | indirect_dptr ⇒ match b with [ indirect_dptr ⇒ true | _ ⇒ false ] |
---|
| 69 | | carry ⇒ match b with [ carry ⇒ true | _ ⇒ false ] |
---|
| 70 | | bit_addr ⇒ match b with [ bit_addr ⇒ true | _ ⇒ false ] |
---|
| 71 | | n_bit_addr ⇒ match b with [ n_bit_addr ⇒ true | _ ⇒ false ] |
---|
| 72 | | relative ⇒ match b with [ relative ⇒ true | _ ⇒ false ] |
---|
| 73 | | addr11 ⇒ match b with [ addr11 ⇒ true | _ ⇒ false ] |
---|
| 74 | | addr16 ⇒ match b with [ addr16 ⇒ true | _ ⇒ false ] |
---|
| 75 | ]. |
---|
| 76 | |
---|
[2032] | 77 | lemma eq_a_to_eq: |
---|
| 78 | ∀a,b. |
---|
| 79 | eq_a a b = true → a = b. |
---|
| 80 | #a #b |
---|
| 81 | cases a cases b |
---|
| 82 | #K |
---|
| 83 | try cases (eq_true_false K) |
---|
| 84 | % |
---|
| 85 | qed. |
---|
| 86 | |
---|
| 87 | lemma eq_a_reflexive: |
---|
| 88 | ∀a. eq_a a a = true. |
---|
| 89 | #a cases a % |
---|
| 90 | qed. |
---|
| 91 | |
---|
| 92 | let rec member_addressing_mode_tag |
---|
| 93 | (n: nat) (v: Vector addressing_mode_tag n) (a: addressing_mode_tag) |
---|
| 94 | on v: Prop ≝ |
---|
| 95 | match v with |
---|
| 96 | [ VEmpty ⇒ False |
---|
| 97 | | VCons n' hd tl ⇒ |
---|
| 98 | bool_to_Prop (eq_a hd a) ∨ member_addressing_mode_tag n' tl a |
---|
| 99 | ]. |
---|
| 100 | |
---|
| 101 | lemma mem_decidable: |
---|
| 102 | ∀n: nat. |
---|
| 103 | ∀v: Vector addressing_mode_tag n. |
---|
| 104 | ∀element: addressing_mode_tag. |
---|
| 105 | mem … eq_a n v element = true ∨ |
---|
| 106 | mem … eq_a … v element = false. |
---|
| 107 | #n #v #element // |
---|
| 108 | qed. |
---|
| 109 | |
---|
| 110 | lemma eq_a_elim: |
---|
| 111 | ∀tag. |
---|
| 112 | ∀hd. |
---|
| 113 | ∀P: bool → Prop. |
---|
| 114 | (tag = hd → P (true)) → |
---|
| 115 | (tag ≠ hd → P (false)) → |
---|
| 116 | P (eq_a tag hd). |
---|
| 117 | #tag #hd #P |
---|
| 118 | cases tag |
---|
| 119 | cases hd |
---|
| 120 | #true_hyp #false_hyp |
---|
| 121 | try @false_hyp |
---|
| 122 | try @true_hyp |
---|
| 123 | try % |
---|
| 124 | #absurd destruct(absurd) |
---|
| 125 | qed. |
---|
| 126 | |
---|
[475] | 127 | (* to avoid expansion... *) |
---|
| 128 | let rec is_a (d:addressing_mode_tag) (A:addressing_mode) on d ≝ |
---|
| 129 | match d with |
---|
| 130 | [ direct ⇒ match A with [ DIRECT _ ⇒ true | _ ⇒ false ] |
---|
| 131 | | indirect ⇒ match A with [ INDIRECT _ ⇒ true | _ ⇒ false ] |
---|
| 132 | | ext_indirect ⇒ match A with [ EXT_INDIRECT _ ⇒ true | _ ⇒ false ] |
---|
[757] | 133 | | registr ⇒ match A with [ REGISTER _ ⇒ true | _ ⇒ false ] |
---|
[475] | 134 | | acc_a ⇒ match A with [ ACC_A ⇒ true | _ ⇒ false ] |
---|
| 135 | | acc_b ⇒ match A with [ ACC_B ⇒ true | _ ⇒ false ] |
---|
| 136 | | dptr ⇒ match A with [ DPTR ⇒ true | _ ⇒ false ] |
---|
| 137 | | data ⇒ match A with [ DATA _ ⇒ true | _ ⇒ false ] |
---|
| 138 | | data16 ⇒ match A with [ DATA16 _ ⇒ true | _ ⇒ false ] |
---|
| 139 | | acc_dptr ⇒ match A with [ ACC_DPTR ⇒ true | _ ⇒ false ] |
---|
| 140 | | acc_pc ⇒ match A with [ ACC_PC ⇒ true | _ ⇒ false ] |
---|
| 141 | | ext_indirect_dptr ⇒ match A with [ EXT_INDIRECT_DPTR ⇒ true | _ ⇒ false ] |
---|
| 142 | | indirect_dptr ⇒ match A with [ INDIRECT_DPTR ⇒ true | _ ⇒ false ] |
---|
| 143 | | carry ⇒ match A with [ CARRY ⇒ true | _ ⇒ false ] |
---|
| 144 | | bit_addr ⇒ match A with [ BIT_ADDR _ ⇒ true | _ ⇒ false ] |
---|
| 145 | | n_bit_addr ⇒ match A with [ N_BIT_ADDR _ ⇒ true | _ ⇒ false ] |
---|
| 146 | | relative ⇒ match A with [ RELATIVE _ ⇒ true | _ ⇒ false ] |
---|
| 147 | | addr11 ⇒ match A with [ ADDR11 _ ⇒ true | _ ⇒ false ] |
---|
[1112] | 148 | | addr16 ⇒ match A with [ ADDR16 _ ⇒ true | _ ⇒ false ] |
---|
| 149 | ]. |
---|
[475] | 150 | |
---|
[2032] | 151 | lemma is_a_decidable: |
---|
| 152 | ∀hd. |
---|
| 153 | ∀element. |
---|
| 154 | is_a hd element = true ∨ is_a hd element = false. |
---|
| 155 | #hd #element // |
---|
| 156 | qed. |
---|
[475] | 157 | |
---|
| 158 | let rec is_in n (l: Vector addressing_mode_tag n) (A:addressing_mode) on l : bool ≝ |
---|
| 159 | match l return λm.λ_:Vector addressing_mode_tag m.bool with |
---|
| 160 | [ VEmpty ⇒ false |
---|
| 161 | | VCons m he (tl: Vector addressing_mode_tag m) ⇒ |
---|
| 162 | is_a he A ∨ is_in ? tl A ]. |
---|
| 163 | |
---|
[2032] | 164 | lemma is_a_to_mem_to_is_in: |
---|
| 165 | ∀he,a,m,q. |
---|
| 166 | is_a he … a = true → mem … eq_a (S m) q he = true → is_in … q a = true. |
---|
| 167 | #he #a #m #q |
---|
| 168 | elim q |
---|
| 169 | [1: |
---|
| 170 | #_ #K assumption |
---|
| 171 | |2: |
---|
| 172 | #m' #t #q' #II #H1 #H2 |
---|
| 173 | normalize |
---|
| 174 | change with (orb ??) in H2:(??%?); |
---|
| 175 | cases (inclusive_disjunction_true … H2) |
---|
| 176 | [1: |
---|
| 177 | #K |
---|
| 178 | <(eq_a_to_eq … K) >H1 % |
---|
| 179 | |2: |
---|
| 180 | #K |
---|
| 181 | >II |
---|
| 182 | try assumption |
---|
| 183 | cases (is_a t a) |
---|
| 184 | normalize |
---|
| 185 | % |
---|
| 186 | ] |
---|
| 187 | ] |
---|
| 188 | qed. |
---|
| 189 | |
---|
| 190 | lemma is_a_true_to_is_in: |
---|
| 191 | ∀n: nat. |
---|
| 192 | ∀x: addressing_mode. |
---|
| 193 | ∀tag: addressing_mode_tag. |
---|
| 194 | ∀supervector: Vector addressing_mode_tag n. |
---|
| 195 | mem addressing_mode_tag eq_a n supervector tag → |
---|
| 196 | is_a tag x = true → |
---|
| 197 | is_in … supervector x. |
---|
| 198 | #n #x #tag #supervector |
---|
| 199 | elim supervector |
---|
| 200 | [1: |
---|
| 201 | #absurd cases absurd |
---|
| 202 | |2: |
---|
| 203 | #n' #hd #tl #inductive_hypothesis |
---|
| 204 | whd in match (mem … eq_a (S n') (hd:::tl) tag); |
---|
| 205 | @eq_a_elim normalize nodelta |
---|
| 206 | [1: |
---|
| 207 | #tag_hd_eq #irrelevant |
---|
| 208 | whd in match (is_in (S n') (hd:::tl) x); |
---|
| 209 | <tag_hd_eq #is_a_hyp >is_a_hyp normalize nodelta |
---|
| 210 | @I |
---|
| 211 | |2: |
---|
| 212 | #tag_hd_neq |
---|
| 213 | whd in match (is_in (S n') (hd:::tl) x); |
---|
| 214 | change with ( |
---|
| 215 | mem … eq_a n' tl tag) |
---|
| 216 | in match (fold_right … n' ? false tl); |
---|
| 217 | #mem_hyp #is_a_hyp |
---|
| 218 | cases(is_a hd x) |
---|
| 219 | [1: |
---|
| 220 | normalize nodelta // |
---|
| 221 | |2: |
---|
| 222 | normalize nodelta |
---|
| 223 | @inductive_hypothesis assumption |
---|
| 224 | ] |
---|
| 225 | ] |
---|
| 226 | ] |
---|
| 227 | qed. |
---|
| 228 | |
---|
[475] | 229 | record subaddressing_mode (n) (l: Vector addressing_mode_tag (S n)) : Type[0] ≝ |
---|
| 230 | { |
---|
| 231 | subaddressing_modeel:> addressing_mode; |
---|
| 232 | subaddressing_modein: bool_to_Prop (is_in ? l subaddressing_modeel) |
---|
| 233 | }. |
---|
| 234 | |
---|
| 235 | coercion subaddressing_mode : ∀n.∀l:Vector addressing_mode_tag (S n).Type[0] |
---|
| 236 | ≝ subaddressing_mode on _l: Vector addressing_mode_tag (S ?) to Type[0]. |
---|
| 237 | |
---|
| 238 | coercion mk_subaddressing_mode : |
---|
| 239 | ∀n.∀l:Vector addressing_mode_tag (S n).∀a:addressing_mode. |
---|
| 240 | ∀p:bool_to_Prop (is_in ? l a).subaddressing_mode n l |
---|
| 241 | ≝ mk_subaddressing_mode on a:addressing_mode to subaddressing_mode ? ?. |
---|
[2032] | 242 | |
---|
| 243 | lemma is_in_subvector_is_in_supervector: |
---|
| 244 | ∀m, n: nat. |
---|
| 245 | ∀subvector: Vector addressing_mode_tag m. |
---|
| 246 | ∀supervector: Vector addressing_mode_tag n. |
---|
| 247 | ∀element: addressing_mode. |
---|
| 248 | subvector_with … eq_a subvector supervector → |
---|
| 249 | is_in m subvector element → is_in n supervector element. |
---|
| 250 | #m #n #subvector #supervector #element |
---|
| 251 | elim subvector |
---|
| 252 | [1: |
---|
| 253 | #subvector_with_proof #is_in_proof |
---|
| 254 | cases is_in_proof |
---|
| 255 | |2: |
---|
| 256 | #n' #hd' #tl' #inductive_hypothesis #subvector_with_proof |
---|
| 257 | whd in match (is_in … (hd':::tl') element); |
---|
| 258 | cases (is_a_decidable hd' element) |
---|
| 259 | [1: |
---|
| 260 | #is_a_true >is_a_true |
---|
| 261 | #irrelevant |
---|
| 262 | whd in match (subvector_with … eq_a (hd':::tl') supervector) in subvector_with_proof; |
---|
| 263 | @(is_a_true_to_is_in … is_a_true) |
---|
| 264 | lapply(subvector_with_proof) |
---|
| 265 | cases(mem … eq_a n supervector hd') // |
---|
| 266 | |2: |
---|
| 267 | #is_a_false >is_a_false normalize nodelta |
---|
| 268 | #assm |
---|
| 269 | @inductive_hypothesis |
---|
| 270 | [1: |
---|
| 271 | generalize in match subvector_with_proof; |
---|
| 272 | whd in match (subvector_with … eq_a (hd':::tl') supervector); |
---|
| 273 | cases(mem_decidable n supervector hd') |
---|
| 274 | [1: |
---|
| 275 | #mem_true >mem_true normalize nodelta |
---|
| 276 | #assm assumption |
---|
| 277 | |2: |
---|
| 278 | #mem_false >mem_false #absurd |
---|
| 279 | cases absurd |
---|
| 280 | ] |
---|
| 281 | |2: |
---|
| 282 | assumption |
---|
| 283 | ] |
---|
| 284 | ] |
---|
| 285 | ] |
---|
| 286 | qed. |
---|
| 287 | |
---|
| 288 | |
---|
| 289 | let rec subaddressing_mode_elim_type |
---|
| 290 | (m: nat) (fixed_v: Vector addressing_mode_tag (S m)) (origaddr: fixed_v) |
---|
| 291 | (Q: fixed_v → Prop) |
---|
| 292 | (n: nat) (v: Vector addressing_mode_tag n) (proof: subvector_with … eq_a v fixed_v) |
---|
| 293 | on v: Prop ≝ |
---|
| 294 | match v return λo: nat. λv': Vector addressing_mode_tag o. o = n → v ≃ v' → ? with |
---|
| 295 | [ VEmpty ⇒ λm_refl. λv_refl. Q origaddr |
---|
| 296 | | VCons n' hd tl ⇒ λm_refl. λv_refl. |
---|
| 297 | let tail_call ≝ subaddressing_mode_elim_type m fixed_v origaddr Q n' tl ? |
---|
| 298 | in |
---|
| 299 | match hd return λa: addressing_mode_tag. a = hd → ? with |
---|
| 300 | [ addr11 ⇒ λhd_refl. (∀w: Word11. Q (ADDR11 w)) → tail_call |
---|
| 301 | | addr16 ⇒ λhd_refl. (∀w: Word. Q (ADDR16 w)) → tail_call |
---|
| 302 | | direct ⇒ λhd_refl. (∀w: Byte. Q (DIRECT w)) → tail_call |
---|
| 303 | | indirect ⇒ λhd_refl. (∀w: Bit. Q (INDIRECT w)) → tail_call |
---|
| 304 | | ext_indirect ⇒ λhd_refl. (∀w: Bit. Q (EXT_INDIRECT w)) → tail_call |
---|
| 305 | | acc_a ⇒ λhd_refl. Q ACC_A → tail_call |
---|
| 306 | | registr ⇒ λhd_refl. (∀w: BitVector 3. Q (REGISTER w)) → tail_call |
---|
| 307 | | acc_b ⇒ λhd_refl. Q ACC_B → tail_call |
---|
| 308 | | dptr ⇒ λhd_refl. Q DPTR → tail_call |
---|
| 309 | | data ⇒ λhd_refl. (∀w: Byte. Q (DATA w)) → tail_call |
---|
| 310 | | data16 ⇒ λhd_refl. (∀w: Word. Q (DATA16 w)) → tail_call |
---|
| 311 | | acc_dptr ⇒ λhd_refl. Q ACC_DPTR → tail_call |
---|
| 312 | | acc_pc ⇒ λhd_refl. Q ACC_PC → tail_call |
---|
| 313 | | ext_indirect_dptr ⇒ λhd_refl. Q EXT_INDIRECT_DPTR → tail_call |
---|
| 314 | | indirect_dptr ⇒ λhd_refl. Q INDIRECT_DPTR → tail_call |
---|
| 315 | | carry ⇒ λhd_refl. Q CARRY → tail_call |
---|
| 316 | | bit_addr ⇒ λhd_refl. (∀w: Byte. Q (BIT_ADDR w)) → tail_call |
---|
| 317 | | n_bit_addr ⇒ λhd_refl. (∀w: Byte. Q (N_BIT_ADDR w)) → tail_call |
---|
| 318 | | relative ⇒ λhd_refl. (∀w: Byte. Q (RELATIVE w)) → tail_call |
---|
| 319 | ] (refl … hd) |
---|
| 320 | ] (refl … n) (refl_jmeq … v). |
---|
| 321 | [20: |
---|
| 322 | generalize in match proof; destruct |
---|
| 323 | whd in match (subvector_with … eq_a (hd:::tl) fixed_v); |
---|
| 324 | cases (mem … eq_a ? fixed_v hd) normalize nodelta |
---|
| 325 | [1: |
---|
| 326 | whd in match (subvector_with … eq_a tl fixed_v); |
---|
| 327 | #assm assumption |
---|
| 328 | |2: |
---|
| 329 | normalize in ⊢ (% → ?); |
---|
| 330 | #absurd cases absurd |
---|
| 331 | ] |
---|
| 332 | ] |
---|
| 333 | @(is_in_subvector_is_in_supervector … proof) |
---|
| 334 | destruct @I |
---|
| 335 | qed. |
---|
| 336 | |
---|
| 337 | lemma subaddressing_mode_elim0: |
---|
| 338 | ∀n: nat. |
---|
| 339 | ∀v: Vector addressing_mode_tag (S n). |
---|
| 340 | ∀addr: v. |
---|
| 341 | ∀Q: v → Prop. |
---|
| 342 | ∀m,w,H. |
---|
| 343 | (∀xaddr: v. ¬ is_in … w xaddr → Q xaddr) → |
---|
| 344 | subaddressing_mode_elim_type n v addr Q m w H. |
---|
| 345 | #n #v #addr #Q #m #w elim w |
---|
| 346 | [ /2/ |
---|
| 347 | | #n' #hd #tl #IH cases hd #H |
---|
| 348 | #INV whd #PO @IH #xaddr cases xaddr * |
---|
| 349 | try (#b #IS_IN #ALREADYSEEN) try (#IS_IN #ALREADYSEEN) try @PO @INV |
---|
| 350 | @ALREADYSEEN ] |
---|
| 351 | qed. |
---|
| 352 | |
---|
| 353 | lemma subaddressing_mode_elim: |
---|
| 354 | ∀n: nat. |
---|
| 355 | ∀v: Vector addressing_mode_tag (S n). |
---|
| 356 | ∀addr: v. |
---|
| 357 | ∀Q: v → Prop. |
---|
| 358 | subaddressing_mode_elim_type n v addr Q (S n) v ?. |
---|
| 359 | [ #n #v #addr #Q @subaddressing_mode_elim0 * #el #H #NH @⊥ >H in NH; // |
---|
| 360 | | @subvector_with_refl @eq_a_reflexive |
---|
| 361 | ] |
---|
| 362 | qed. |
---|
[832] | 363 | |
---|
[475] | 364 | inductive preinstruction (A: Type[0]) : Type[0] ≝ |
---|
[757] | 365 | ADD: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A |
---|
| 366 | | ADDC: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A |
---|
| 367 | | SUBB: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A |
---|
| 368 | | INC: [[ acc_a ; registr ; direct ; indirect ; dptr ]] → preinstruction A |
---|
| 369 | | DEC: [[ acc_a ; registr ; direct ; indirect ]] → preinstruction A |
---|
[475] | 370 | | MUL: [[acc_a]] → [[acc_b]] → preinstruction A |
---|
| 371 | | DIV: [[acc_a]] → [[acc_b]] → preinstruction A |
---|
| 372 | | DA: [[acc_a]] → preinstruction A |
---|
| 373 | |
---|
[820] | 374 | (* conditional jumps *) |
---|
| 375 | | JC: A → preinstruction A |
---|
| 376 | | JNC: A → preinstruction A |
---|
| 377 | | JB: [[bit_addr]] → A → preinstruction A |
---|
| 378 | | JNB: [[bit_addr]] → A → preinstruction A |
---|
| 379 | | JBC: [[bit_addr]] → A → preinstruction A |
---|
| 380 | | JZ: A → preinstruction A |
---|
| 381 | | JNZ: A → preinstruction A |
---|
| 382 | | CJNE: |
---|
| 383 | [[acc_a]] × [[direct; data]] ⊎ [[registr; indirect]] × [[data]] → A → preinstruction A |
---|
| 384 | | DJNZ: [[registr ; direct]] → A → preinstruction A |
---|
[475] | 385 | (* logical operations *) |
---|
| 386 | | ANL: |
---|
[757] | 387 | [[acc_a]] × [[ registr ; direct ; indirect ; data ]] ⊎ |
---|
[475] | 388 | [[direct]] × [[ acc_a ; data ]] ⊎ |
---|
| 389 | [[carry]] × [[ bit_addr ; n_bit_addr]] → preinstruction A |
---|
| 390 | | ORL: |
---|
[757] | 391 | [[acc_a]] × [[ registr ; data ; direct ; indirect ]] ⊎ |
---|
[475] | 392 | [[direct]] × [[ acc_a ; data ]] ⊎ |
---|
| 393 | [[carry]] × [[ bit_addr ; n_bit_addr]] → preinstruction A |
---|
| 394 | | XRL: |
---|
[757] | 395 | [[acc_a]] × [[ data ; registr ; direct ; indirect ]] ⊎ |
---|
[475] | 396 | [[direct]] × [[ acc_a ; data ]] → preinstruction A |
---|
| 397 | | CLR: [[ acc_a ; carry ; bit_addr ]] → preinstruction A |
---|
| 398 | | CPL: [[ acc_a ; carry ; bit_addr ]] → preinstruction A |
---|
| 399 | | RL: [[acc_a]] → preinstruction A |
---|
| 400 | | RLC: [[acc_a]] → preinstruction A |
---|
| 401 | | RR: [[acc_a]] → preinstruction A |
---|
| 402 | | RRC: [[acc_a]] → preinstruction A |
---|
| 403 | | SWAP: [[acc_a]] → preinstruction A |
---|
| 404 | |
---|
| 405 | (* data transfer *) |
---|
| 406 | | MOV: |
---|
[757] | 407 | [[acc_a]] × [[ registr ; direct ; indirect ; data ]] ⊎ |
---|
| 408 | [[ registr ; indirect ]] × [[ acc_a ; direct ; data ]] ⊎ |
---|
| 409 | [[direct]] × [[ acc_a ; registr ; direct ; indirect ; data ]] ⊎ |
---|
[475] | 410 | [[dptr]] × [[data16]] ⊎ |
---|
| 411 | [[carry]] × [[bit_addr]] ⊎ |
---|
| 412 | [[bit_addr]] × [[carry]] → preinstruction A |
---|
| 413 | | MOVX: |
---|
| 414 | [[acc_a]] × [[ ext_indirect ; ext_indirect_dptr ]] ⊎ |
---|
| 415 | [[ ext_indirect ; ext_indirect_dptr ]] × [[acc_a]] → preinstruction A |
---|
| 416 | | SETB: [[ carry ; bit_addr ]] → preinstruction A |
---|
| 417 | | PUSH: [[direct]] → preinstruction A |
---|
| 418 | | POP: [[direct]] → preinstruction A |
---|
[757] | 419 | | XCH: [[acc_a]] → [[ registr ; direct ; indirect ]] → preinstruction A |
---|
[475] | 420 | | XCHD: [[acc_a]] → [[indirect]] → preinstruction A |
---|
| 421 | |
---|
| 422 | (* program branching *) |
---|
| 423 | | RET: preinstruction A |
---|
| 424 | | RETI: preinstruction A |
---|
| 425 | | NOP: preinstruction A. |
---|
| 426 | |
---|
[820] | 427 | inductive instruction: Type[0] ≝ |
---|
| 428 | | ACALL: [[addr11]] → instruction |
---|
| 429 | | LCALL: [[addr16]] → instruction |
---|
| 430 | | AJMP: [[addr11]] → instruction |
---|
| 431 | | LJMP: [[addr16]] → instruction |
---|
| 432 | | SJMP: [[relative]] → instruction |
---|
| 433 | | JMP: [[indirect_dptr]] → instruction |
---|
| 434 | | MOVC: [[acc_a]] → [[ acc_dptr ; acc_pc ]] → instruction |
---|
| 435 | | RealInstruction: preinstruction [[ relative ]] → instruction. |
---|
| 436 | |
---|
| 437 | coercion RealInstruction: ∀p: preinstruction [[ relative ]]. instruction ≝ |
---|
| 438 | RealInstruction on _p: preinstruction ? to instruction. |
---|
[475] | 439 | |
---|
[722] | 440 | inductive pseudo_instruction: Type[0] ≝ |
---|
[820] | 441 | | Instruction: preinstruction Identifier → pseudo_instruction |
---|
| 442 | | Comment: String → pseudo_instruction |
---|
[1515] | 443 | | Cost: costlabel → pseudo_instruction |
---|
[820] | 444 | | Jmp: Identifier → pseudo_instruction |
---|
| 445 | | Call: Identifier → pseudo_instruction |
---|
| 446 | | Mov: [[dptr]] → Identifier → pseudo_instruction. |
---|
[475] | 447 | |
---|
[1882] | 448 | definition labelled_instruction ≝ labelled_obj ASMTag pseudo_instruction. |
---|
[1522] | 449 | definition preamble ≝ (identifier_map SymbolTag nat) × (list (Identifier × Word)). |
---|
[820] | 450 | definition assembly_program ≝ list instruction. |
---|
| 451 | definition pseudo_assembly_program ≝ preamble × (list labelled_instruction). |
---|