source: src/ASM/ASM.ma @ 2123

Last change on this file since 2123 was 2123, checked in by boender, 9 years ago
File size: 16.5 KB
Line 
1include "ASM/BitVector.ma".
2include "common/Identifiers.ma".
3include "common/CostLabel.ma".
4include "common/LabelledObjects.ma".
5
6axiom ASMTag : String.
7definition Identifier ≝ identifier ASMTag.
8definition toASM_ident : ∀tag. identifier tag → Identifier ≝ λt,i. match i with [ an_identifier id ⇒ an_identifier ASMTag id ].
9
10inductive addressing_mode: Type[0] ≝
11  DIRECT: Byte → addressing_mode
12| INDIRECT: Bit → addressing_mode
13| EXT_INDIRECT: Bit → addressing_mode
14| REGISTER: BitVector 3 → addressing_mode
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
31(* dpm: renamed register to registr to avoid clash with brian's types *)
32inductive addressing_mode_tag : Type[0] ≝
33  direct: addressing_mode_tag
34| indirect: addressing_mode_tag
35| ext_indirect: addressing_mode_tag
36| registr: addressing_mode_tag
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
53definition 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 ]
59      | registr ⇒ match b with [ registr ⇒ true | _ ⇒ false ]
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
77lemma 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 %
85qed.
86
87lemma eq_a_reflexive:
88  ∀a. eq_a a a = true.
89  #a cases a %
90qed.
91
92let 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
101lemma 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 //
108qed.
109
110lemma 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)
125qed.
126
127(* to avoid expansion... *)
128let 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 ]
133   | registr ⇒ match A with [ REGISTER _ ⇒ true | _ ⇒ false ]
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 ]
148   | addr16 ⇒ match A with [ ADDR16 _ ⇒ true | _ ⇒ false ]
149   ].
150
151lemma is_a_decidable:
152  ∀hd.
153  ∀element.
154    is_a hd element = true ∨ is_a hd element = false.
155  #hd #element //
156qed.
157
158let 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
164lemma 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 ]
188qed.
189
190lemma 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  ]
227qed.
228
229record 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
235coercion 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
238coercion 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 ? ?.
242
243lemma 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  ]
286qed.
287
288
289let 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
335qed.
336
337lemma 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 ]
351qed.
352
353lemma 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]
362qed.
363 
364inductive preinstruction (A: Type[0]) : Type[0] ≝
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
370| MUL: [[acc_a]] → [[acc_b]] → preinstruction A
371| DIV: [[acc_a]] → [[acc_b]] → preinstruction A
372| DA: [[acc_a]] → preinstruction A
373
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
385 (* logical operations *)
386| ANL:
387   [[acc_a]] × [[ registr ; direct ; indirect ; data ]] ⊎
388   [[direct]] × [[ acc_a ; data ]] ⊎
389   [[carry]] × [[ bit_addr ; n_bit_addr]] → preinstruction A
390| ORL:
391   [[acc_a]] × [[ registr ; data ; direct ; indirect ]] ⊎
392   [[direct]] × [[ acc_a ; data ]] ⊎
393   [[carry]] × [[ bit_addr ; n_bit_addr]] → preinstruction A
394| XRL:
395   [[acc_a]] × [[ data ; registr ; direct ; indirect ]] ⊎
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:
407    [[acc_a]] × [[ registr ; direct ; indirect ; data ]] ⊎
408    [[ registr ; indirect ]] × [[ acc_a ; direct ; data ]] ⊎
409    [[direct]] × [[ acc_a ; registr ; direct ; indirect ; data ]] ⊎
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
419| XCH: [[acc_a]] → [[ registr ; direct ; indirect ]] → preinstruction A
420| XCHD: [[acc_a]] → [[indirect]] → preinstruction A
421
422 (* program branching *)
423| RET: preinstruction A
424| RETI: preinstruction A
425| NOP: preinstruction A.
426
427inductive 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 
437coercion RealInstruction: ∀p: preinstruction [[ relative ]]. instruction ≝
438  RealInstruction on _p: preinstruction ? to instruction.
439
440inductive pseudo_instruction: Type[0] ≝
441  | Instruction: preinstruction Identifier → pseudo_instruction
442  | Comment: String → pseudo_instruction
443  | Cost: costlabel → pseudo_instruction
444  | Jmp: Identifier → pseudo_instruction
445  | Call: Identifier → pseudo_instruction
446  | Mov: [[dptr]] → Identifier → pseudo_instruction.
447
448definition labelled_instruction ≝ labelled_obj ASMTag pseudo_instruction.
449definition preamble ≝ (identifier_map SymbolTag nat) × (list (Identifier × Word)).
450definition assembly_program ≝ list instruction.
451definition pseudo_assembly_program ≝ preamble × (list labelled_instruction).
452
453(* labels & instructions *)
454definition instruction_has_label ≝
455  λid: Identifier.
456  λi.
457  match i with
458  [ Jmp j ⇒ j = id
459  | Call j ⇒ j = id
460  | Instruction instr ⇒
461    match instr with
462    [ JC j ⇒ j = id
463    | JNC j ⇒ j = id
464    | JZ j ⇒ j = id
465    | JNZ j ⇒ j = id
466    | JB _ j ⇒ j = id
467    | JBC _ j ⇒ j = id
468    | DJNZ _ j ⇒ j = id
469    | CJNE _ j ⇒ j = id
470    | _ ⇒ False
471    ]
472  | _ ⇒ False
473  ].
Note: See TracBrowser for help on using the repository browser.