source: src/ASM/ASM.ma @ 2754

Last change on this file since 2754 was 2754, checked in by sacerdot, 7 years ago
  1. WARNING: I commented out one of James's function used in compiler.ma because it was undefined (partial commit). To be restored.
  2. The type of labelled_object_code programs now has a symbol table, used to generate the intensional events function call/return.
File size: 33.2 KB
Line 
1include "ASM/BitVector.ma".
2include "common/Identifiers.ma".
3include "common/CostLabel.ma".
4include "common/LabelledObjects.ma".
5include "joint/String.ma".
6
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
31definition eq_addressing_mode: addressing_mode → addressing_mode → bool ≝
32  λa, b: addressing_mode.
33  match a with
34  [ DIRECT d ⇒
35    match b with
36    [ DIRECT e ⇒ eq_bv ? d e
37    | _ ⇒ false
38    ]
39  | INDIRECT b' ⇒
40    match b with
41    [ INDIRECT e ⇒ eq_b b' e
42    | _ ⇒ false
43    ]
44  | EXT_INDIRECT b' ⇒
45    match b with
46    [ EXT_INDIRECT e ⇒ eq_b b' e
47    | _ ⇒ false
48    ]
49  | REGISTER bv ⇒
50    match b with
51    [ REGISTER bv' ⇒ eq_bv ? bv bv'
52    | _ ⇒ false
53    ]
54  | ACC_A ⇒ match b with [ ACC_A ⇒ true | _ ⇒ false ]
55  | ACC_B ⇒ match b with [ ACC_B ⇒ true | _ ⇒ false ]
56  | DPTR ⇒ match b with [ DPTR ⇒ true | _ ⇒ false ]
57  | DATA b' ⇒
58    match b with
59    [ DATA e ⇒ eq_bv ? b' e
60    | _ ⇒ false
61    ]
62  | DATA16 w ⇒
63    match b with
64    [ DATA16 e ⇒ eq_bv ? w e
65    | _ ⇒ false
66    ]
67  | ACC_DPTR ⇒ match b with [ ACC_DPTR ⇒ true | _ ⇒ false ]
68  | ACC_PC ⇒ match b with [ ACC_PC ⇒ true | _ ⇒ false ]
69  | EXT_INDIRECT_DPTR ⇒ match b with [ EXT_INDIRECT_DPTR ⇒ true | _ ⇒ false ]
70  | INDIRECT_DPTR ⇒ match b with [ INDIRECT_DPTR ⇒ true | _ ⇒ false ]
71  | CARRY ⇒ match b with [ CARRY ⇒ true | _ ⇒ false ]
72  | BIT_ADDR b' ⇒
73    match b with
74    [ BIT_ADDR e ⇒ eq_bv ? b' e
75    | _ ⇒ false
76    ]
77  | N_BIT_ADDR b' ⇒
78    match b with
79    [ N_BIT_ADDR e ⇒ eq_bv ? b' e
80    | _ ⇒ false
81    ]
82  | RELATIVE n ⇒
83    match b with
84    [ RELATIVE e ⇒ eq_bv ? n e
85    | _ ⇒ false
86    ]
87  | ADDR11 w ⇒
88    match b with
89    [ ADDR11 e ⇒ eq_bv ? w e
90    | _ ⇒ false
91    ]
92  | ADDR16 w ⇒
93    match b with
94    [ ADDR16 e ⇒ eq_bv ? w e
95    | _ ⇒ false
96    ]
97  ].
98
99lemma eq_addressing_mode_refl:
100  ∀a. eq_addressing_mode a a = true.
101  #a
102  cases a try #arg1 try #arg2
103  try @eq_bv_refl try @eq_b_refl
104  try normalize %
105qed.
106
107(* dpm: renamed register to registr to avoid clash with brian's types *)
108inductive addressing_mode_tag : Type[0] ≝
109  direct: addressing_mode_tag
110| indirect: addressing_mode_tag
111| ext_indirect: addressing_mode_tag
112| registr: addressing_mode_tag
113| acc_a: addressing_mode_tag
114| acc_b: addressing_mode_tag
115| dptr: addressing_mode_tag
116| data: addressing_mode_tag
117| data16: addressing_mode_tag
118| acc_dptr: addressing_mode_tag
119| acc_pc: addressing_mode_tag
120| ext_indirect_dptr: addressing_mode_tag
121| indirect_dptr: addressing_mode_tag
122| carry: addressing_mode_tag
123| bit_addr: addressing_mode_tag
124| n_bit_addr: addressing_mode_tag
125| relative: addressing_mode_tag
126| addr11: addressing_mode_tag
127| addr16: addressing_mode_tag.
128
129definition eq_a ≝
130  λa, b: addressing_mode_tag.
131    match a with
132      [ direct ⇒ match b with [ direct ⇒ true | _ ⇒ false ]
133      | indirect ⇒ match b with [ indirect ⇒ true | _ ⇒ false ]
134      | ext_indirect ⇒ match b with [ ext_indirect ⇒ true | _ ⇒ false ]
135      | registr ⇒ match b with [ registr ⇒ true | _ ⇒ false ]
136      | acc_a ⇒ match b with [ acc_a ⇒ true | _ ⇒ false ]
137      | acc_b ⇒ match b with [ acc_b ⇒ true | _ ⇒ false ]
138      | dptr ⇒ match b with [ dptr ⇒ true | _ ⇒ false ]
139      | data ⇒ match b with [ data ⇒ true | _ ⇒ false ]
140      | data16 ⇒ match b with [ data16 ⇒ true | _ ⇒ false ]
141      | acc_dptr ⇒ match b with [ acc_dptr ⇒ true | _ ⇒ false ]
142      | acc_pc ⇒ match b with [ acc_pc ⇒ true | _ ⇒ false ]
143      | ext_indirect_dptr ⇒ match b with [ ext_indirect_dptr ⇒ true | _ ⇒ false ]
144      | indirect_dptr ⇒ match b with [ indirect_dptr ⇒ true | _ ⇒ false ]
145      | carry ⇒ match b with [ carry ⇒ true | _ ⇒ false ]
146      | bit_addr ⇒ match b with [ bit_addr ⇒ true | _ ⇒ false ]
147      | n_bit_addr ⇒ match b with [ n_bit_addr ⇒ true | _ ⇒ false ]
148      | relative ⇒ match b with [ relative ⇒ true | _ ⇒ false ]
149      | addr11 ⇒ match b with [ addr11 ⇒ true | _ ⇒ false ]
150      | addr16 ⇒ match b with [ addr16 ⇒ true | _ ⇒ false ]
151      ].
152
153lemma eq_a_to_eq:
154  ∀a,b.
155    eq_a a b = true → a = b.
156 #a #b
157 cases a cases b
158 #K
159 try cases (eq_true_false K)
160 %
161qed.
162
163lemma eq_a_reflexive:
164  ∀a. eq_a a a = true.
165  #a cases a %
166qed.
167
168let rec member_addressing_mode_tag
169  (n: nat) (v: Vector addressing_mode_tag n) (a: addressing_mode_tag)
170    on v: Prop ≝
171  match v with
172  [ VEmpty ⇒ False
173  | VCons n' hd tl ⇒
174      bool_to_Prop (eq_a hd a) ∨ member_addressing_mode_tag n' tl a
175  ].
176
177lemma mem_decidable:
178  ∀n: nat.
179  ∀v: Vector addressing_mode_tag n.
180  ∀element: addressing_mode_tag.
181    mem … eq_a n v element = true ∨
182      mem … eq_a … v element = false.
183  #n #v #element //
184qed.
185
186lemma eq_a_elim:
187  ∀tag.
188  ∀hd.
189  ∀P: bool → Prop.
190    (tag = hd → P (true)) →
191      (tag ≠ hd → P (false)) →
192        P (eq_a tag hd).
193  #tag #hd #P
194  cases tag
195  cases hd
196  #true_hyp #false_hyp
197  try @false_hyp
198  try @true_hyp
199  try %
200  #absurd destruct(absurd)
201qed.
202
203(* to avoid expansion... *)
204let rec is_a (d:addressing_mode_tag) (A:addressing_mode) on d ≝
205  match d with
206   [ direct ⇒ match A with [ DIRECT _ ⇒ true | _ ⇒ false ]
207   | indirect ⇒ match A with [ INDIRECT _ ⇒ true | _ ⇒ false ]
208   | ext_indirect ⇒ match A with [ EXT_INDIRECT _ ⇒ true | _ ⇒ false ]
209   | registr ⇒ match A with [ REGISTER _ ⇒ true | _ ⇒ false ]
210   | acc_a ⇒ match A with [ ACC_A ⇒ true | _ ⇒ false ]
211   | acc_b ⇒ match A with [ ACC_B ⇒ true | _ ⇒ false ]
212   | dptr ⇒ match A with [ DPTR ⇒ true | _ ⇒ false ]
213   | data ⇒ match A with [ DATA _ ⇒ true | _ ⇒ false ]
214   | data16 ⇒ match A with [ DATA16 _ ⇒ true | _ ⇒ false ]
215   | acc_dptr ⇒ match A with [ ACC_DPTR ⇒ true | _ ⇒ false ]
216   | acc_pc ⇒ match A with [ ACC_PC ⇒ true | _ ⇒ false ]
217   | ext_indirect_dptr ⇒ match A with [ EXT_INDIRECT_DPTR ⇒ true | _ ⇒ false ]
218   | indirect_dptr ⇒ match A with [ INDIRECT_DPTR ⇒ true | _ ⇒ false ]
219   | carry ⇒ match A with [ CARRY ⇒ true | _ ⇒ false ]
220   | bit_addr ⇒ match A with [ BIT_ADDR _ ⇒ true | _ ⇒ false ]
221   | n_bit_addr ⇒ match A with [ N_BIT_ADDR _ ⇒ true | _ ⇒ false ]
222   | relative ⇒ match A with [ RELATIVE _ ⇒ true | _ ⇒ false ]
223   | addr11 ⇒ match A with [ ADDR11 _ ⇒ true | _ ⇒ false ]
224   | addr16 ⇒ match A with [ ADDR16 _ ⇒ true | _ ⇒ false ]
225   ].
226
227lemma is_a_decidable:
228  ∀hd.
229  ∀element.
230    is_a hd element = true ∨ is_a hd element = false.
231  #hd #element //
232qed.
233
234let rec is_in n (l: Vector addressing_mode_tag n) (A:addressing_mode) on l : bool ≝
235 match l return λm.λ_:Vector addressing_mode_tag m.bool with
236  [ VEmpty ⇒ false
237  | VCons m he (tl: Vector addressing_mode_tag m) ⇒
238     is_a he A ∨ is_in ? tl A ].
239
240definition is_in_cons_elim:
241 ∀len.∀hd,tl.∀m:addressing_mode
242  .is_in (S len) (hd:::tl) m →
243    (bool_to_Prop (is_a hd m)) ∨ (bool_to_Prop (is_in len tl m)).
244 #len #hd #tl #am #ISIN whd in match (is_in ???) in ISIN;
245 cases (is_a hd am) in ISIN; /2/
246qed.
247
248lemma is_in_monotonic_wrt_append:
249  ∀m, n: nat.
250  ∀p: Vector addressing_mode_tag m.
251  ∀q: Vector addressing_mode_tag n.
252  ∀to_search: addressing_mode.
253    bool_to_Prop (is_in ? p to_search) → bool_to_Prop (is_in ? (q @@ p) to_search).
254  #m #n #p #q #to_search #assm
255  elim q try assumption
256  #n' #hd #tl #inductive_hypothesis
257  normalize
258  cases (is_a ??) try @I
259  >inductive_hypothesis @I
260qed.
261
262corollary is_in_hd_tl:
263  ∀to_search: addressing_mode.
264  ∀hd: addressing_mode_tag.
265  ∀n: nat.
266  ∀v: Vector addressing_mode_tag n.
267    bool_to_Prop (is_in ? v to_search) → bool_to_Prop (is_in ? (hd:::v) to_search).
268  #to_search #hd #n #v
269  elim v
270  [1:
271    #absurd
272    normalize in absurd; cases absurd
273  |2:
274    #n' #hd' #tl #inductive_hypothesis #assm
275    >vector_cons_append >(vector_cons_append … hd' tl)
276    @(is_in_monotonic_wrt_append … ([[hd']]@@tl) [[hd]] to_search)
277    assumption
278  ]
279qed.
280
281lemma is_a_to_mem_to_is_in:
282 ∀he,a,m,q.
283   is_a he … a = true → mem … eq_a (S m) q he = true → is_in … q a = true.
284 #he #a #m #q
285 elim q
286 [1:
287   #_ #K assumption
288 |2:
289   #m' #t #q' #II #H1 #H2
290   normalize
291   change with (orb ??) in H2:(??%?);
292   cases (inclusive_disjunction_true … H2)
293   [1:
294     #K
295     <(eq_a_to_eq … K) >H1 %
296   |2:
297     #K
298     >II
299     try assumption
300     cases (is_a t a)
301     normalize
302     %
303   ]
304 ]
305qed.
306
307lemma is_a_true_to_is_in:
308  ∀n: nat.
309  ∀x: addressing_mode.
310  ∀tag: addressing_mode_tag.
311  ∀supervector: Vector addressing_mode_tag n.
312  mem addressing_mode_tag eq_a n supervector tag →
313    is_a tag x = true →
314      is_in … supervector x.
315  #n #x #tag #supervector
316  elim supervector
317  [1:
318    #absurd cases absurd
319  |2:
320    #n' #hd #tl #inductive_hypothesis
321    whd in match (mem … eq_a (S n') (hd:::tl) tag);
322    @eq_a_elim normalize nodelta
323    [1:
324      #tag_hd_eq #irrelevant
325      whd in match (is_in (S n') (hd:::tl) x);
326      <tag_hd_eq #is_a_hyp >is_a_hyp normalize nodelta
327      @I
328    |2:
329      #tag_hd_neq
330      whd in match (is_in (S n') (hd:::tl) x);
331      change with (
332        mem … eq_a n' tl tag)
333          in match (fold_right … n' ? false tl);
334      #mem_hyp #is_a_hyp
335      cases(is_a hd x)
336      [1:
337        normalize nodelta //
338      |2:
339        normalize nodelta
340        @inductive_hypothesis assumption
341      ]
342    ]
343  ]
344qed.
345
346record subaddressing_mode (n) (l: Vector addressing_mode_tag (S n)) : Type[0] ≝
347{
348  subaddressing_modeel:> addressing_mode;
349  subaddressing_modein: bool_to_Prop (is_in ? l subaddressing_modeel)
350}.
351
352coercion subaddressing_mode : ∀n.∀l:Vector addressing_mode_tag (S n).Type[0]
353 ≝ subaddressing_mode on _l: Vector addressing_mode_tag (S ?) to Type[0].
354
355coercion mk_subaddressing_mode :
356 ∀n.∀l:Vector addressing_mode_tag (S n).∀a:addressing_mode.
357  ∀p:bool_to_Prop (is_in ? l a).subaddressing_mode n l
358 ≝ mk_subaddressing_mode on a:addressing_mode to subaddressing_mode ? ?.
359
360lemma is_in_subvector_is_in_supervector:
361  ∀m, n: nat.
362  ∀subvector: Vector addressing_mode_tag m.
363  ∀supervector: Vector addressing_mode_tag n.
364  ∀element: addressing_mode.
365    subvector_with … eq_a subvector supervector →
366      is_in m subvector element → is_in n supervector element.
367  #m #n #subvector #supervector #element
368  elim subvector
369  [1:
370    #subvector_with_proof #is_in_proof
371    cases is_in_proof
372  |2:
373    #n' #hd' #tl' #inductive_hypothesis #subvector_with_proof
374    whd in match (is_in … (hd':::tl') element);
375    cases (is_a_decidable hd' element)
376    [1:
377      #is_a_true >is_a_true
378      #irrelevant
379      whd in match (subvector_with … eq_a (hd':::tl') supervector) in subvector_with_proof;
380      @(is_a_true_to_is_in … is_a_true)
381      lapply(subvector_with_proof)
382      cases(mem … eq_a n supervector hd') //
383    |2:
384      #is_a_false >is_a_false normalize nodelta
385      #assm
386      @inductive_hypothesis
387      [1:
388        generalize in match subvector_with_proof;
389        whd in match (subvector_with … eq_a (hd':::tl') supervector);
390        cases(mem_decidable n supervector hd')
391        [1:
392          #mem_true >mem_true normalize nodelta
393          #assm assumption
394        |2:
395          #mem_false >mem_false #absurd
396          cases absurd
397        ]
398      |2:
399        assumption
400      ]
401    ]
402  ]
403qed.
404
405(* XXX: move back into ASM.ma *)
406lemma subvector_with_to_subvector_with_tl:
407  ∀n: nat.
408  ∀m: nat.
409  ∀v.
410  ∀fixed_v.
411  ∀proof: (subvector_with addressing_mode_tag n (S m) eq_a v fixed_v).
412  ∀n': nat.
413  ∀hd: addressing_mode_tag.
414  ∀tl: Vector addressing_mode_tag n'.
415  ∀m_refl: S n'=n.
416  ∀v_refl: v≃hd:::tl.
417   subvector_with addressing_mode_tag n' (S m) eq_a tl fixed_v.
418  #n #m #v #fixed_v #proof #n' #hd #tl #m_refl #v_refl
419  generalize in match proof; destruct
420  whd in match (subvector_with … eq_a (hd:::tl) fixed_v);
421  cases (mem … eq_a ? fixed_v hd) normalize nodelta
422  [1:
423    whd in match (subvector_with … eq_a tl fixed_v);
424    #assm assumption
425  |2:
426    normalize in ⊢ (% → ?);
427    #absurd cases absurd
428  ]
429qed.
430
431let rec subaddressing_mode_elim_type
432  (m: nat) (fixed_v: Vector addressing_mode_tag (S m)) (origaddr: fixed_v)
433    (Q: fixed_v → Prop)
434     (n: nat) (v: Vector addressing_mode_tag n) (proof: subvector_with … eq_a v fixed_v)
435       on v: Prop ≝
436  match v return λo: nat. λv': Vector addressing_mode_tag o. o = n → v ≃ v' → ? with
437  [ VEmpty         ⇒ λm_refl. λv_refl. Q origaddr
438  | VCons n' hd tl ⇒ λm_refl. λv_refl.
439    let tail_call ≝ subaddressing_mode_elim_type m fixed_v origaddr Q n' tl ?
440    in
441    match hd return λa: addressing_mode_tag. a = hd → ? with
442    [ addr11            ⇒ λhd_refl. (∀w: Word11.      Q (ADDR11 w)) → tail_call
443    | addr16            ⇒ λhd_refl. (∀w: Word.        Q (ADDR16 w)) → tail_call
444    | direct            ⇒ λhd_refl. (∀w: Byte.        Q (DIRECT w)) → tail_call
445    | indirect          ⇒ λhd_refl. (∀w: Bit.         Q (INDIRECT w)) → tail_call
446    | ext_indirect      ⇒ λhd_refl. (∀w: Bit.         Q (EXT_INDIRECT w)) → tail_call
447    | acc_a             ⇒ λhd_refl.                  Q ACC_A → tail_call
448    | registr           ⇒ λhd_refl. (∀w: BitVector 3. Q (REGISTER w)) → tail_call
449    | acc_b             ⇒ λhd_refl.                  Q ACC_B → tail_call
450    | dptr              ⇒ λhd_refl.                  Q DPTR → tail_call
451    | data              ⇒ λhd_refl. (∀w: Byte.        Q (DATA w))  → tail_call
452    | data16            ⇒ λhd_refl. (∀w: Word.        Q (DATA16 w)) → tail_call
453    | acc_dptr          ⇒ λhd_refl.                  Q ACC_DPTR → tail_call
454    | acc_pc            ⇒ λhd_refl.                  Q ACC_PC → tail_call
455    | ext_indirect_dptr ⇒ λhd_refl.                  Q EXT_INDIRECT_DPTR → tail_call
456    | indirect_dptr     ⇒ λhd_refl.                  Q INDIRECT_DPTR → tail_call
457    | carry             ⇒ λhd_refl.                  Q CARRY → tail_call
458    | bit_addr          ⇒ λhd_refl. (∀w: Byte.        Q (BIT_ADDR w)) → tail_call
459    | n_bit_addr        ⇒ λhd_refl. (∀w: Byte.        Q (N_BIT_ADDR w)) → tail_call
460    | relative          ⇒ λhd_refl. (∀w: Byte.        Q (RELATIVE w)) → tail_call
461    ] (refl … hd)
462  ] (refl … n) (refl_jmeq … v).
463  [20:
464    @(subvector_with_to_subvector_with_tl … proof … m_refl v_refl)
465  ]
466  @(is_in_subvector_is_in_supervector … proof)
467  destruct @I
468qed.
469
470lemma subaddressing_mode_elim0:
471  ∀n: nat.
472  ∀v: Vector addressing_mode_tag (S n).
473  ∀addr: v.
474  ∀Q: v → Prop.
475  ∀m,w,H.
476  (∀xaddr: v. ¬ is_in … w xaddr → Q xaddr) →
477   subaddressing_mode_elim_type n v addr Q m w H.
478  #n #v #addr #Q #m #w elim w
479  [1:
480    /2/
481  |2:
482    #n' #hd #tl #IH cases hd #H
483    #INV whd #PO @IH #xaddr cases xaddr *
484    try (#b #IS_IN #ALREADYSEEN) try (#IS_IN #ALREADYSEEN) try @PO @INV
485    @ALREADYSEEN
486  ]
487qed.
488
489lemma subaddressing_mode_elim:
490  ∀n: nat.
491  ∀v: Vector addressing_mode_tag (S n).
492  ∀addr: v.
493  ∀Q: v → Prop.
494   subaddressing_mode_elim_type n v addr Q (S n) v ?.
495  [1:
496    #n #v #addr #Q @subaddressing_mode_elim0 * #el #H #NH @⊥ >H in NH; //
497  |2:
498    @subvector_with_refl @eq_a_reflexive
499  ]
500qed.
501 
502inductive preinstruction (A: Type[0]) : Type[0] ≝
503  ADD: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A
504| ADDC: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A
505| SUBB: [[acc_a]] → [[ registr ; direct ; indirect ; data ]] → preinstruction A
506| INC: [[ acc_a ; registr ; direct ; indirect ; dptr ]] → preinstruction A
507| DEC: [[ acc_a ; registr ; direct ; indirect ]] → preinstruction A
508| MUL: [[acc_a]] → [[acc_b]] → preinstruction A
509| DIV: [[acc_a]] → [[acc_b]] → preinstruction A
510| DA: [[acc_a]] → preinstruction A
511
512(* conditional jumps *)
513| JC: A → preinstruction A
514| JNC: A → preinstruction A
515| JB: [[bit_addr]] → A → preinstruction A
516| JNB: [[bit_addr]] → A → preinstruction A
517| JBC: [[bit_addr]] → A → preinstruction A
518| JZ: A → preinstruction A
519| JNZ: A → preinstruction A
520| CJNE:
521   [[acc_a]] × [[direct; data]] ⊎ [[registr; indirect]] × [[data]] → A → preinstruction A
522| DJNZ: [[registr ; direct]] → A → preinstruction A
523 (* logical operations *)
524| ANL:
525   [[acc_a]] × [[ registr ; direct ; indirect ; data ]] ⊎
526   [[direct]] × [[ acc_a ; data ]] ⊎
527   [[carry]] × [[ bit_addr ; n_bit_addr]] → preinstruction A
528| ORL:
529   [[acc_a]] × [[ registr ; data ; direct ; indirect ]] ⊎
530   [[direct]] × [[ acc_a ; data ]] ⊎
531   [[carry]] × [[ bit_addr ; n_bit_addr]] → preinstruction A
532| XRL:
533   [[acc_a]] × [[ data ; registr ; direct ; indirect ]] ⊎
534   [[direct]] × [[ acc_a ; data ]] → preinstruction A
535| CLR: [[ acc_a ; carry ; bit_addr ]] → preinstruction A
536| CPL: [[ acc_a ; carry ; bit_addr ]] → preinstruction A
537| RL: [[acc_a]] → preinstruction A
538| RLC: [[acc_a]] → preinstruction A
539| RR: [[acc_a]] → preinstruction A
540| RRC: [[acc_a]] → preinstruction A
541| SWAP: [[acc_a]] → preinstruction A
542
543 (* data transfer *)
544| MOV:
545    [[acc_a]] × [[ registr ; direct ; indirect ; data ]] ⊎
546    [[ registr ; indirect ]] × [[ acc_a ; direct ; data ]] ⊎
547    [[direct]] × [[ acc_a ; registr ; direct ; indirect ; data ]] ⊎
548    [[dptr]] × [[data16]] ⊎
549    [[carry]] × [[bit_addr]] ⊎
550    [[bit_addr]] × [[carry]] → preinstruction A
551| MOVX:
552    [[acc_a]] × [[ ext_indirect ; ext_indirect_dptr ]] ⊎
553    [[ ext_indirect ; ext_indirect_dptr ]] × [[acc_a]] → preinstruction A
554| SETB: [[ carry ; bit_addr ]] → preinstruction A
555| PUSH: [[direct]] → preinstruction A
556| POP: [[direct]] → preinstruction A
557| XCH: [[acc_a]] → [[ registr ; direct ; indirect ]] → preinstruction A
558| XCHD: [[acc_a]] → [[indirect]] → preinstruction A
559
560 (* program branching *)
561| RET: preinstruction A
562| RETI: preinstruction A
563| NOP: preinstruction A
564| JMP: [[indirect_dptr]] → preinstruction A.
565
566definition eq_preinstruction: preinstruction [[relative]] → preinstruction [[relative]] → bool ≝
567  λi, j.
568  match i with
569  [ ADD arg1 arg2 ⇒
570    match j with
571    [ ADD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
572    | _ ⇒ false
573    ]
574  | ADDC arg1 arg2 ⇒
575    match j with
576    [ ADDC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
577    | _ ⇒ false
578    ]
579  | SUBB arg1 arg2 ⇒
580    match j with
581    [ SUBB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
582    | _ ⇒ false
583    ]
584  | INC arg ⇒
585    match j with
586    [ INC arg' ⇒ eq_addressing_mode arg arg'
587    | _ ⇒ false
588    ]
589  | DEC arg ⇒
590    match j with
591    [ DEC arg' ⇒ eq_addressing_mode arg arg'
592    | _ ⇒ false
593    ]
594  | MUL arg1 arg2 ⇒
595    match j with
596    [ MUL arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
597    | _ ⇒ false
598    ]
599  | DIV arg1 arg2 ⇒
600    match j with
601    [ DIV arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
602    | _ ⇒ false
603    ]
604  | DA arg ⇒
605    match j with
606    [ DA arg' ⇒ eq_addressing_mode arg arg'
607    | _ ⇒ false
608    ]
609  | JC arg ⇒
610    match j with
611    [ JC arg' ⇒ eq_addressing_mode arg arg'
612    | _ ⇒ false
613    ]
614  | JNC arg ⇒
615    match j with
616    [ JNC arg' ⇒ eq_addressing_mode arg arg'
617    | _ ⇒ false
618    ]
619  | JB arg1 arg2 ⇒
620    match j with
621    [ JB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
622    | _ ⇒ false
623    ]
624  | JNB arg1 arg2 ⇒
625    match j with
626    [ JNB arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
627    | _ ⇒ false
628    ]
629  | JBC arg1 arg2 ⇒
630    match j with
631    [ JBC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
632    | _ ⇒ false
633    ]
634  | JZ arg ⇒
635    match j with
636    [ JZ arg' ⇒ eq_addressing_mode arg arg'
637    | _ ⇒ false
638    ]
639  | JNZ arg ⇒
640    match j with
641    [ JNZ arg' ⇒ eq_addressing_mode arg arg'
642    | _ ⇒ false
643    ]
644  | JMP arg ⇒
645    match j with
646    [ JMP arg' ⇒ eq_addressing_mode arg arg'
647    | _ ⇒ false
648    ]
649  | CJNE arg1 arg2 ⇒
650    match j with
651    [ CJNE arg1' arg2' ⇒
652      let prod_eq_left ≝ eq_prod [[acc_a]] [[direct; data]] eq_addressing_mode eq_addressing_mode in
653      let prod_eq_right ≝ eq_prod [[registr; indirect]] [[data]] eq_addressing_mode eq_addressing_mode in
654      let arg1_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
655        arg1_eq arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
656    | _ ⇒ false
657    ]
658  | DJNZ arg1 arg2 ⇒
659    match j with
660    [ DJNZ arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
661    | _ ⇒ false
662    ]
663  | CLR arg ⇒
664    match j with
665    [ CLR arg' ⇒ eq_addressing_mode arg arg'
666    | _ ⇒ false
667    ]
668  | CPL arg ⇒
669    match j with
670    [ CPL arg' ⇒ eq_addressing_mode arg arg'
671    | _ ⇒ false
672    ]
673  | RL arg ⇒
674    match j with
675    [ RL arg' ⇒ eq_addressing_mode arg arg'
676    | _ ⇒ false
677    ]
678  | RLC arg ⇒
679    match j with
680    [ RLC arg' ⇒ eq_addressing_mode arg arg'
681    | _ ⇒ false
682    ]
683  | RR arg ⇒
684    match j with
685    [ RR arg' ⇒ eq_addressing_mode arg arg'
686    | _ ⇒ false
687    ]
688  | RRC arg ⇒
689    match j with
690    [ RRC arg' ⇒ eq_addressing_mode arg arg'
691    | _ ⇒ false
692    ]
693  | SWAP arg ⇒
694    match j with
695    [ SWAP arg' ⇒ eq_addressing_mode arg arg'
696    | _ ⇒ false
697    ]
698  | SETB arg ⇒
699    match j with
700    [ SETB arg' ⇒ eq_addressing_mode arg arg'
701    | _ ⇒ false
702    ]
703  | PUSH arg ⇒
704    match j with
705    [ PUSH arg' ⇒ eq_addressing_mode arg arg'
706    | _ ⇒ false
707    ]
708  | POP arg ⇒
709    match j with
710    [ POP arg' ⇒ eq_addressing_mode arg arg'
711    | _ ⇒ false
712    ]
713  | XCH arg1 arg2 ⇒
714    match j with
715    [ XCH arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
716    | _ ⇒ false
717    ]
718  | XCHD arg1 arg2 ⇒
719    match j with
720    [ XCHD arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
721    | _ ⇒ false
722    ]
723  | RET ⇒ match j with [ RET ⇒ true | _ ⇒ false ]
724  | RETI ⇒ match j with [ RETI ⇒ true | _ ⇒ false ]
725  | NOP ⇒ match j with [ NOP ⇒ true | _ ⇒ false ]
726  | MOVX arg ⇒
727    match j with
728    [ MOVX arg' ⇒
729      let prod_eq_left ≝ eq_prod [[acc_a]] [[ext_indirect; ext_indirect_dptr]] eq_addressing_mode eq_addressing_mode in
730      let prod_eq_right ≝ eq_prod [[ext_indirect; ext_indirect_dptr]] [[acc_a]] eq_addressing_mode eq_addressing_mode in
731      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
732        sum_eq arg arg'
733    | _ ⇒ false
734    ]
735  | XRL arg ⇒
736    match j with
737    [ XRL arg' ⇒
738      let prod_eq_left ≝ eq_prod [[acc_a]] [[ data ; registr ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in
739      let prod_eq_right ≝ eq_prod [[direct]] [[ acc_a ; data ]] eq_addressing_mode eq_addressing_mode in
740      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
741        sum_eq arg arg'
742    | _ ⇒ false
743    ]
744  | ORL arg ⇒
745    match j with
746    [ ORL arg' ⇒
747      let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; data ; direct ; indirect ]] eq_addressing_mode eq_addressing_mode in
748      let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in
749      let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in
750      let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in
751      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
752        sum_eq arg arg'
753    | _ ⇒ false
754    ]
755  | ANL arg ⇒
756    match j with
757    [ ANL arg' ⇒
758      let prod_eq_left1 ≝ eq_prod [[acc_a]] [[ registr ; direct ; indirect ; data ]] eq_addressing_mode eq_addressing_mode in
759      let prod_eq_left2 ≝ eq_prod [[direct]] [[ acc_a; data ]] eq_addressing_mode eq_addressing_mode in
760      let prod_eq_left ≝ eq_sum ? ? prod_eq_left1 prod_eq_left2 in
761      let prod_eq_right ≝ eq_prod [[carry]] [[ bit_addr ; n_bit_addr]] eq_addressing_mode eq_addressing_mode in
762      let sum_eq ≝ eq_sum ? ? prod_eq_left prod_eq_right in
763        sum_eq arg arg'
764    | _ ⇒ false
765    ]
766  | MOV arg ⇒
767    match j with
768    [ MOV arg' ⇒
769      let prod_eq_6 ≝ eq_prod [[acc_a]] [[registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in
770      let prod_eq_5 ≝ eq_prod [[registr; indirect]] [[acc_a; direct; data]] eq_addressing_mode eq_addressing_mode in
771      let prod_eq_4 ≝ eq_prod [[direct]] [[acc_a; registr; direct; indirect; data]] eq_addressing_mode eq_addressing_mode in
772      let prod_eq_3 ≝ eq_prod [[dptr]] [[data16]] eq_addressing_mode eq_addressing_mode in
773      let prod_eq_2 ≝ eq_prod [[carry]] [[bit_addr]] eq_addressing_mode eq_addressing_mode in
774      let prod_eq_1 ≝ eq_prod [[bit_addr]] [[carry]] eq_addressing_mode eq_addressing_mode in
775      let sum_eq_1 ≝ eq_sum ? ? prod_eq_6 prod_eq_5 in
776      let sum_eq_2 ≝ eq_sum ? ? sum_eq_1 prod_eq_4 in
777      let sum_eq_3 ≝ eq_sum ? ? sum_eq_2 prod_eq_3 in
778      let sum_eq_4 ≝ eq_sum ? ? sum_eq_3 prod_eq_2 in
779      let sum_eq_5 ≝ eq_sum ? ? sum_eq_4 prod_eq_1 in
780        sum_eq_5 arg arg'
781    | _ ⇒ false
782    ]
783  ].
784
785lemma eq_preinstruction_refl:
786  ∀i.
787    eq_preinstruction i i = true.
788  #i cases i try #arg1 try #arg2
789  try @eq_addressing_mode_refl
790  [1,2,3,4,5,6,7,8,10,16,17,18,19,20:
791    whd in ⊢ (??%?); try %
792    >eq_addressing_mode_refl
793    >eq_addressing_mode_refl %
794  |13,15:
795    whd in ⊢ (??%?);
796    cases arg1
797    [*:
798      #arg1_left normalize nodelta
799      >eq_prod_refl [*: try % #argr @eq_addressing_mode_refl]
800    ]
801  |11,12:
802    whd in ⊢ (??%?);
803    cases arg1
804    [1:
805      #arg1_left normalize nodelta
806      >(eq_sum_refl …)
807      [1: % | 2,3: #arg @eq_prod_refl ]
808      @eq_addressing_mode_refl
809    |2:
810      #arg1_left normalize nodelta
811      @eq_prod_refl [*: @eq_addressing_mode_refl ]
812    |3:
813      #arg1_left normalize nodelta
814      >(eq_sum_refl …)
815      [1:
816        %
817      |2,3:
818        #arg @eq_prod_refl #arg @eq_addressing_mode_refl
819      ]
820    |4:
821      #arg1_left normalize nodelta
822      @eq_prod_refl [*: #arg @eq_addressing_mode_refl ]
823    ]
824  |14:
825    whd in ⊢ (??%?);
826    cases arg1
827    [1:
828      #arg1_left normalize nodelta
829      @eq_sum_refl
830      [1:
831        #arg @eq_sum_refl
832        [1:
833          #arg @eq_sum_refl
834          [1:
835            #arg @eq_sum_refl
836            [1:
837              #arg @eq_prod_refl
838              [*:
839                @eq_addressing_mode_refl
840              ]
841            |2:
842              #arg @eq_prod_refl
843              [*:
844                #arg @eq_addressing_mode_refl
845              ]
846            ]
847          |2:
848            #arg @eq_prod_refl
849            [*:
850              #arg @eq_addressing_mode_refl
851            ]
852          ]
853        |2:
854          #arg @eq_prod_refl
855          [*:
856            #arg @eq_addressing_mode_refl
857          ]
858        ]
859      |2:
860        #arg @eq_prod_refl
861        [*:
862          #arg @eq_addressing_mode_refl
863        ]
864      ]
865    |2:
866      #arg1_right normalize nodelta
867      @eq_prod_refl
868      [*:
869        #arg @eq_addressing_mode_refl
870      ]
871    ]
872  |*:
873    whd in ⊢ (??%?);
874    cases arg1
875    [*:
876      #arg1 >eq_sum_refl
877      [1,4:
878        @eq_addressing_mode_refl
879      |2,3,5,6:
880        #arg @eq_prod_refl
881        [*:
882          #arg @eq_addressing_mode_refl
883        ]
884      ]
885    ]
886  ]
887qed.
888
889inductive instruction: Type[0] ≝
890  | ACALL: [[addr11]] → instruction
891  | LCALL: [[addr16]] → instruction
892  | AJMP: [[addr11]] → instruction
893  | LJMP: [[addr16]] → instruction
894  | SJMP: [[relative]] → instruction
895  | MOVC: [[acc_a]] → [[ acc_dptr ; acc_pc ]] → instruction
896  | RealInstruction: preinstruction [[ relative ]] → instruction.
897 
898coercion RealInstruction: ∀p: preinstruction [[ relative ]]. instruction ≝
899  RealInstruction on _p: preinstruction ? to instruction.
900
901definition eq_instruction: instruction → instruction → bool ≝
902  λi, j.
903  match i with
904  [ ACALL arg ⇒
905    match j with
906    [ ACALL arg' ⇒ eq_addressing_mode arg arg'
907    | _ ⇒ false
908    ]
909  | LCALL arg ⇒
910    match j with
911    [ LCALL arg' ⇒ eq_addressing_mode arg arg'
912    | _ ⇒ false
913    ]
914  | AJMP arg ⇒
915    match j with
916    [ AJMP arg' ⇒ eq_addressing_mode arg arg'
917    | _ ⇒ false
918    ]
919  | LJMP arg ⇒
920    match j with
921    [ LJMP arg' ⇒ eq_addressing_mode arg arg'
922    | _ ⇒ false
923    ]
924  | SJMP arg ⇒
925    match j with
926    [ SJMP arg' ⇒ eq_addressing_mode arg arg'
927    | _ ⇒ false
928    ]
929  | MOVC arg1 arg2 ⇒
930    match j with
931    [ MOVC arg1' arg2' ⇒ eq_addressing_mode arg1 arg1' ∧ eq_addressing_mode arg2 arg2'
932    | _ ⇒ false
933    ]
934  | RealInstruction instr ⇒
935    match j with
936    [ RealInstruction instr' ⇒ eq_preinstruction instr instr'
937    | _ ⇒ false
938    ]
939  ].
940 
941lemma eq_instruction_refl:
942  ∀i. eq_instruction i i = true.
943  #i cases i [*: #arg1 ]
944  try @eq_addressing_mode_refl
945  try @eq_preinstruction_refl
946  #arg2 whd in ⊢ (??%?);
947  >eq_addressing_mode_refl >eq_addressing_mode_refl %
948qed.
949
950lemma eq_instruction_to_eq:
951  ∀i1, i2: instruction.
952    eq_instruction i1 i2 = true → i1 ≃ i2.
953  #i1 #i2
954  cases i1 cases i2 cases daemon (* easy but tedious
955  [1,10,19,28,37,46:
956    #arg1 #arg2
957    whd in match (eq_instruction ??);
958    cases arg1 #subaddressing_mode
959    cases subaddressing_mode
960    try (#arg1' #arg2' normalize in ⊢ (% → ?); #absurd cases absurd @I)
961    try (#arg1' normalize in ⊢ (% → ?); #absurd cases absurd @I)
962    try (normalize in ⊢ (% → ?); #absurd cases absurd @I)
963    #word11 #irrelevant
964    cases arg2 #subaddressing_mode
965    cases subaddressing_mode
966    try (#arg1' #arg2' normalize in ⊢ (% → ?); #absurd cases absurd @I)
967    try (#arg1' normalize in ⊢ (% → ?); #absurd cases absurd @I)
968    try (normalize in ⊢ (% → ?); #absurd cases absurd @I)
969    #word11' #irrelevant normalize nodelta
970    #eq_bv_assm cases (eq_bv_eq … eq_bv_assm) % *)
971qed.
972
973inductive word_side : Type[0] ≝ HIGH : word_side | LOW : word_side.
974
975inductive pseudo_instruction: Type[0] ≝
976  | Instruction: preinstruction Identifier → pseudo_instruction
977  | Comment: String → pseudo_instruction
978  | Cost: costlabel → pseudo_instruction
979  | Jmp: Identifier → pseudo_instruction
980  | Jnz : [[acc_a]] → Identifier → Identifier → pseudo_instruction
981  | MovSuccessor : [[ acc_a ; direct ; registr ]] → word_side → Identifier → pseudo_instruction
982  | Call: Identifier → pseudo_instruction
983  | Mov: [[dptr]] → Identifier → pseudo_instruction.
984
985definition labelled_instruction ≝ labelled_obj ASMTag pseudo_instruction.
986(* The first associative list assigns symbol names to addresses in data memory.
987   The second associative list assigns to Identifiers meant to be entry points
988   of functions the name of the function (that lives in a different namespace) *)
989definition preamble ≝ list (Identifier × Word) × (list (Identifier × ident)).
990definition assembly_program ≝ list instruction.
991definition pseudo_assembly_program ≝ preamble × (list labelled_instruction).
992
993definition object_code ≝ list Byte.
994definition costlabel_map ≝ BitVectorTrie costlabel 16.
995definition symboltable_type ≝ BitVectorTrie ident 16.
996definition labelled_object_code ≝ object_code × (costlabel_map × symboltable_type).
997
998(* labels & instructions *)
999definition instruction_has_label ≝
1000  λid: Identifier.
1001  λi.
1002  match i with
1003  [ Jmp j ⇒ j = id
1004  | Call j ⇒ j = id
1005  | Instruction instr ⇒
1006    match instr with
1007    [ JC j ⇒ j = id
1008    | JNC j ⇒ j = id
1009    | JZ j ⇒ j = id
1010    | JNZ j ⇒ j = id
1011    | JB _ j ⇒ j = id
1012    | JNB _ j ⇒ j = id
1013    | JBC _ j ⇒ j = id
1014    | DJNZ _ j ⇒ j = id
1015    | CJNE _ j ⇒ j = id
1016    | _ ⇒ False
1017    ]
1018  | _ ⇒ False
1019  ].
1020
1021
1022(* If instruction i is a jump, then there will be something in the policy at
1023 * position i *)
1024definition is_jump' ≝
1025  λx:preinstruction Identifier.
1026  match x with
1027  [ JC _ ⇒ true
1028  | JNC _ ⇒ true
1029  | JZ _ ⇒ true
1030  | JNZ _ ⇒ true
1031  | JB _ _ ⇒ true
1032  | JNB _ _ ⇒ true
1033  | JBC _ _ ⇒ true
1034  | CJNE _ _ ⇒ true
1035  | DJNZ _ _ ⇒ true
1036  | _ ⇒ false
1037  ].
1038
1039definition is_relative_jump ≝
1040  λinstr:pseudo_instruction.
1041  match instr with
1042  [ Instruction i ⇒ is_jump' i
1043  | _             ⇒ false
1044  ].
1045   
1046definition is_jump ≝
1047  λinstr:pseudo_instruction.
1048  match instr with
1049  [ Instruction i   ⇒ is_jump' i
1050  | Call _ ⇒ true
1051  | Jmp _ ⇒ true
1052  | _ ⇒ false
1053  ].
1054
1055definition is_call ≝
1056  λinstr:pseudo_instruction.
1057  match instr with
1058  [ Call _ ⇒ true
1059  | _ ⇒ false
1060  ].
1061 
1062definition is_jump_to ≝
1063  λx:pseudo_instruction.λd:Identifier.
1064  match x with
1065  [ Instruction i ⇒ match i with
1066    [ JC j ⇒ d = j
1067    | JNC j ⇒ d = j
1068    | JZ j ⇒ d = j
1069    | JNZ j ⇒ d = j
1070    | JB _ j ⇒ d = j
1071    | JNB _ j ⇒ d = j
1072    | JBC _ j ⇒ d = j
1073    | CJNE _ j ⇒ d = j
1074    | DJNZ _ j ⇒ d = j
1075    | _ ⇒ False
1076    ]
1077  | Call c ⇒ d = c
1078  | Jmp j ⇒ d = j
1079  | _ ⇒ False
1080  ].
Note: See TracBrowser for help on using the repository browser.