1 | include "ASM/BitVector.ma". |
---|
2 | include "common/Identifiers.ma". |
---|
3 | include "common/CostLabel.ma". |
---|
4 | include "common/LabelledObjects.ma". |
---|
5 | |
---|
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 ]. |
---|
9 | |
---|
10 | inductive 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 *) |
---|
32 | inductive 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 | |
---|
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 ] |
---|
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 | |
---|
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 | |
---|
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 ] |
---|
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 | |
---|
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. |
---|
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 | |
---|
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 | |
---|
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 ? ?. |
---|
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. |
---|
363 | |
---|
364 | inductive 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 | |
---|
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. |
---|
439 | |
---|
440 | inductive 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 | |
---|
448 | definition labelled_instruction ≝ labelled_obj ASMTag pseudo_instruction. |
---|
449 | definition preamble ≝ (identifier_map SymbolTag nat) × (list (Identifier × Word)). |
---|
450 | definition assembly_program ≝ list instruction. |
---|
451 | definition pseudo_assembly_program ≝ preamble × (list labelled_instruction). |
---|
452 | |
---|
453 | (* labels & instructions *) |
---|
454 | definition 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 | ]. |
---|