source: Deliverables/D4.1/Matita/Assembly.ma @ 271

Last change on this file since 271 was 271, checked in by sacerdot, 10 years ago

assembly1 defined on ACALL and ADD: it seems it will become too slow...

File size: 17.0 KB
Line 
1include "ASM.ma".
2
3(*
4ndefinition from_addressing_mode_tag ≝
5 λT:Type[0].λt:addressing_mode_tag.
6  match t with
7   [ direct ⇒ Byte → T
8   | indirect ⇒ Bit → T
9   | ext_indirect ⇒ Bit → T
10   | register ⇒ Bit → Bit → Bit → T
11   | acc_a ⇒ T
12   | acc_b ⇒ T
13   | dptr ⇒ T
14   | data ⇒ Byte → T
15   | data16 ⇒ Word → T
16   | acc_dptr ⇒ T
17   | acc_pc ⇒ T
18   | ext_indirect_dptr ⇒ T
19   | indirect_dptr ⇒ T
20   | carry ⇒ T
21   | bit_addr ⇒ Bit → T
22   | n_bit_addr ⇒ Bit → T
23   | relative ⇒ Byte → T
24   | addr11 ⇒ Word11 → T
25   | addr16 ⇒ Word → T ].
26*)
27(*
28nlet rec elim_addr (T:addressing_mode → Type[0]) n l on l
29: subaddressing_mode n l → Type[0] ≝
30 match l
31  return λm.λl:Vector addressing_mode_tag m.
32   ∀proof:m = S n.
33    subaddressing_mode n (match proof with [refl ⇒ l]) → Type[0] with
34  [ Empty ⇒ λK.λ_.Nat
35  | Cons o he tl ⇒ λK.λv.Nat(*
36     match o
37      return λy.∀p:S y = S n.
38       subaddressing_mode y
39        (v⌈Vector addressing_mode_tag (S y) ↦ Vector addressing_mode_tag (S n)⌉)
40        → Type[0]
41     with
42      [ Z ⇒ λK.λv.(? : Type[0])
43      | S p ⇒ λK.λv.(? : Type[0])
44      ]*)
45  ] (?: S n = S n).
46##[##1: @
47  | ndestruct
48  |##7: //
49  | normalize;
50
51nlet rec elim_addr n (v: Vector addressing_mode_tag (S n)) on v
52: subaddressing_mode n v Type[0]
53
54 match v return λx.λ_.x = S n. Type[0] with
55  [ Empty ⇒ λK.⊥
56  | Cons o he tl ⇒ λK.
57     match o with
58      [ Z ⇒
59      | S m ⇒
60      ]
61  ] (? : S n = S n).
62*)
63
64notation "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
65 with precedence 10
66for @{ match $t with [ mk_Cartesian ${ident x} ${ident y} ⇒ $s ] }.
67
68ncheck (let 〈x,z〉 ≝ 〈Z,Z〉 in 〈x,z〉).
69
70ndefinition assembly1 ≝
71 λA.λi: preinstruction A.match i with
72  [ ACALL addr ⇒
73     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
74      [ ADDR11 w ⇒ λ_.
75         let 〈v1,v2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S Z))) w in
76          [ (v1 @ [[true; false; false; false; true]]) ; v2 ]
77      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
78  | ADD addr1 addr2 ⇒
79     match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
80      [ REGISTER r1 r2 r3 ⇒ λ_.[ ([[false;false;true;false;true;r1;r2;r2]]) ]
81      | DIRECT b1 ⇒ λ_.[ ([[false;false;true;false;false;true;false;true]]); b1 ]
82      | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;false;false;true;true;i1]]) ]
83      | DATA b1 ⇒ λ_. [ ([[false;false;true;false;false;true;false;false]]) ; b1 ]
84      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
85  | _ ⇒ [ ([[false;false;false;false;false;false;false;false]]) ]].
86
87
88  | `ADDC (`A, `REG(r1,r2,r3)) ->
89     [mk_byte_from_bits ((false,false,true,true),(true,r1,r2,r3))]
90  | `ADDC (`A, `DIRECT b1) ->
91     [mk_byte_from_bits ((false,false,true,true),(false,true,false,true)); b1]
92  | `ADDC (`A,`INDIRECT i1) ->
93     [mk_byte_from_bits ((false,false,true,true),(false,true,true,i1))]
94  | `ADDC (`A,`DATA b1) ->
95     [mk_byte_from_bits ((false,false,true,true),(false,true,false,false)); b1]
96  | `AJMP (`ADDR11 w) ->
97     let (a10,a9,a8,b1) = from_word11 w in
98       [mk_byte_from_bits ((a10,a9,a8,false),(false,false,false,true))]
99  | `ANL (`U1 (`A, `REG (r1,r2,r3))) ->
100     [mk_byte_from_bits ((false,true,false,true),(true,r1,r2,r3))]
101  | `ANL (`U1 (`A, `DIRECT b1)) ->
102     [mk_byte_from_bits ((false,true,false,true),(false,true,false,true)); b1]
103  | `ANL (`U1 (`A, `INDIRECT i1)) ->
104     [mk_byte_from_bits ((false,true,false,true),(false,true,true,i1))]
105  | `ANL (`U1 (`A, `DATA b1)) ->
106     [mk_byte_from_bits ((false,true,false,true),(false,true,false,false)); b1]
107  | `ANL (`U2 (`DIRECT b1,`A)) ->
108     [mk_byte_from_bits ((false,true,false,true),(false,false,true,false)); b1]
109  | `ANL (`U2 (`DIRECT b1,`DATA b2)) ->
110     [mk_byte_from_bits ((false,true,false,true),(false,false,true,true)); b1; b2]
111  | `ANL (`U3 (`C,`BIT b1)) ->
112     [mk_byte_from_bits ((true,false,false,false),(false,false,true,false)); b1]
113  | `ANL (`U3 (`C,`NBIT b1)) ->
114    [mk_byte_from_bits ((true,false,true,true),(false,false,false,false)); b1]
115  | `CJNE (`U1 (`A, `DIRECT b1), `REL b2) ->
116    [mk_byte_from_bits ((true,false,true,true),(false,true,false,true)); b1; b2]
117  | `CJNE (`U1 (`A, `DATA b1), `REL b2) ->
118    [mk_byte_from_bits ((true,false,true,true),(false,true,false,false)); b1; b2]
119  | `CJNE (`U2 (`REG(r1,r2,r3), `DATA b1), `REL b2) ->
120    [mk_byte_from_bits ((true,false,true,true),(true,r1,r2,r3)); b1; b2]
121  | `CJNE (`U2 (`INDIRECT i1, `DATA b1), `REL b2) ->
122    [mk_byte_from_bits ((true,false,true,true),(false,true,true,i1)); b1; b2]
123  | `CLR `A ->
124    [mk_byte_from_bits ((true,true,true,false),(false,true,false,false))]
125  | `CLR `C ->
126    [mk_byte_from_bits ((true,true,false,false),(false,false,true,true))]
127  | `CLR (`BIT b1) ->
128    [mk_byte_from_bits ((true,true,false,false),(false,false,true,false)); b1]
129  | `CPL `A ->
130    [mk_byte_from_bits ((true,true,true,true),(false,true,false,false))]
131  | `CPL `C ->
132    [mk_byte_from_bits ((true,false,true,true),(false,false,true,true))]
133  | `CPL (`BIT b1) ->
134    [mk_byte_from_bits ((true,false,true,true),(false,false,true,false)); b1]
135  | `DA `A ->
136    [mk_byte_from_bits ((true,true,false,true),(false,true,false,false))]
137  | `DEC `A ->
138    [mk_byte_from_bits ((false,false,false,true),(false,true,false,false))]
139  | `DEC (`REG(r1,r2,r3)) ->
140    [mk_byte_from_bits ((false,false,false,true),(true,r1,r2,r3))]
141  | `DEC (`DIRECT b1) ->
142    [mk_byte_from_bits ((false,false,false,true),(false,true,false,true)); b1]
143  | `DEC (`INDIRECT i1) ->
144    [mk_byte_from_bits ((false,false,false,true),(false,true,true,i1))]
145  | `DIV (`A, `B) ->
146    [mk_byte_from_bits ((true,false,false,false),(false,true,false,false))]
147  | `DJNZ (`REG(r1,r2,r3), `REL b1) ->
148    [mk_byte_from_bits ((true,true,false,true),(true,r1,r2,r3)); b1]
149  | `DJNZ (`DIRECT b1, `REL b2) ->
150    [mk_byte_from_bits ((true,true,false,true),(false,true,false,true)); b1; b2]
151  | `INC `A ->
152    [mk_byte_from_bits ((false,false,false,false),(false,true,false,false))]
153  | `INC (`REG(r1,r2,r3)) ->
154    [mk_byte_from_bits ((false,false,false,false),(true,r1,r2,r3))]
155  | `INC (`DIRECT b1) ->
156    [mk_byte_from_bits ((false,false,false,false),(false,true,false,true)); b1]
157  | `INC (`INDIRECT i1) ->
158    [mk_byte_from_bits ((false,false,false,false),(false,true,true,i1))]
159  | `INC `DPTR ->
160    [mk_byte_from_bits ((true,false,true,false),(false,false,true,true))]
161  | `JB (`BIT b1, `REL b2) ->
162    [mk_byte_from_bits ((false,false,true,false),(false,false,false,false)); b1; b2]
163  | `JBC (`BIT b1, `REL b2) ->
164    [mk_byte_from_bits ((false,false,false,true),(false,false,false,false)); b1; b2]
165  | `JC (`REL b1) ->
166    [mk_byte_from_bits ((false,true,false,false),(false,false,false,false)); b1]
167  | `JMP `IND_DPTR ->
168    [mk_byte_from_bits ((false,true,true,true),(false,false,true,true))]
169  | `JNB (`BIT b1, `REL b2) ->
170    [mk_byte_from_bits ((false,false,true,true),(false,false,false,false)); b1; b2]
171  | `JNC (`REL b1) ->
172    [mk_byte_from_bits ((false,true,false,true),(false,false,false,false)); b1]
173  | `JNZ (`REL b1) ->
174    [mk_byte_from_bits ((false,true,true,true),(false,false,false,false)); b1]
175  | `JZ (`REL b1) ->
176    [mk_byte_from_bits ((false,true,true,false),(false,false,false,false)); b1]
177  | `LCALL (`ADDR16 w) ->
178      let (b1,b2) = from_word w in
179        [mk_byte_from_bits ((false,false,false,true),(false,false,true,false)); b1; b2]
180  | `LJMP (`ADDR16 w) ->
181      let (b1,b2) = from_word w in
182        [mk_byte_from_bits ((false,false,false,false),(false,false,true,false)); b1; b2]
183  | `MOV (`U1 (`A, `REG(r1,r2,r3))) ->
184    [mk_byte_from_bits ((true,true,true,false),(true,r1,r2,r3))]
185  | `MOV (`U1 (`A, `DIRECT b1)) ->
186    [mk_byte_from_bits ((true,true,true,false),(false,true,false,true)); b1]
187  | `MOV (`U1 (`A, `INDIRECT i1)) ->
188    [mk_byte_from_bits ((true,true,true,false),(false,true,true,i1))]
189  | `MOV (`U1 (`A, `DATA b1)) ->
190    [mk_byte_from_bits ((false,true,true,true),(false,true,false,false)); b1]
191  | `MOV (`U2 (`REG(r1,r2,r3), `A)) ->
192    [mk_byte_from_bits ((true,true,true,true),(true,r1,r2,r3))]
193  | `MOV (`U2 (`REG(r1,r2,r3), (`DIRECT b1))) ->
194    [mk_byte_from_bits ((true,false,true,false),(true,r1,r2,r3)); b1]
195  | `MOV (`U2 (`REG(r1,r2,r3), (`DATA b1))) ->
196    [mk_byte_from_bits ((false,true,true,true),(true,r1,r2,r3)); b1]
197  | `MOV (`U3 (`DIRECT b1, `A)) ->
198    [mk_byte_from_bits ((true,true,true,true),(false,true,false,true)); b1]
199  | `MOV (`U3 (`DIRECT b1, `REG(r1,r2,r3))) ->
200    [mk_byte_from_bits ((true,false,false,false),(true,r1,r2,r3)); b1]
201  | `MOV (`U3 (`DIRECT b1, `DIRECT b2)) ->
202    [mk_byte_from_bits ((true,false,false,false),(false,true,false,true)); b1; b2]
203  | `MOV (`U3 (`DIRECT b1, `INDIRECT i1)) ->
204    [mk_byte_from_bits ((true,false,false,false),(false,true,true,i1)); b1]
205  | `MOV (`U3 (`DIRECT b1, `DATA b2)) ->
206    [mk_byte_from_bits ((false,true,true,true),(false,true,false,true)); b1; b2]
207  | `MOV (`U2 (`INDIRECT i1, `A)) ->
208    [mk_byte_from_bits ((true,true,true,true),(false,true,true,i1))]
209  | `MOV (`U2 (`INDIRECT i1, `DIRECT b1)) ->
210    [mk_byte_from_bits ((true,false,true,false),(false,true,true,i1)); b1]
211  | `MOV (`U2 (`INDIRECT i1, `DATA b1)) ->
212    [mk_byte_from_bits ((false,true,true,true),(false,true,true,i1)); b1]
213  | `MOV (`U5 (`C, `BIT b1)) ->
214    [mk_byte_from_bits ((true,false,true,false),(false,false,true,false)); b1]
215  | `MOV (`U6 (`BIT b1, `C)) ->
216    [mk_byte_from_bits ((true,false,false,true),(false,false,true,false)); b1]
217  | `MOV (`U4 (`DPTR, `DATA16 w)) ->
218    let (b1,b2) = from_word w in
219      [mk_byte_from_bits ((true,false,false,true),(false,false,false,false)); b1; b2]
220  | `MOVC (`A, `A_DPTR) ->
221    [mk_byte_from_bits ((true,false,false,true),(false,false,true,true))]
222  | `MOVC (`A, `A_PC) ->
223    [mk_byte_from_bits ((true,false,false,false),(false,false,true,true))]
224  | `MOVX (`U1 (`A, `EXT_INDIRECT i1)) ->
225    [mk_byte_from_bits ((true,true,true,false),(false,false,true,i1))]
226  | `MOVX (`U1 (`A, `EXT_IND_DPTR)) ->
227    [mk_byte_from_bits ((true,true,true,false),(false,false,false,false))]
228  | `MOVX (`U2 (`EXT_INDIRECT i1, `A)) ->
229    [mk_byte_from_bits ((true,true,true,true),(false,false,true,i1))]
230  | `MOVX (`U2 (`EXT_IND_DPTR, `A)) ->
231    [mk_byte_from_bits ((true,true,true,true),(false,false,false,false))]
232  | `MUL(`A, `B) ->
233    [mk_byte_from_bits ((true,false,true,false),(false,true,false,false))]
234  | `NOP ->
235    [mk_byte_from_bits ((false,false,false,false),(false,false,false,false))]
236  | `ORL (`U1(`A, `REG(r1,r2,r3))) ->
237    [mk_byte_from_bits ((false,true,false,false),(true,r1,r2,r3))]
238  | `ORL (`U1(`A, `DIRECT b1)) ->
239    [mk_byte_from_bits ((false,true,false,false),(false,true,false,true)); b1]
240  | `ORL (`U1(`A, `INDIRECT i1)) ->
241    [mk_byte_from_bits ((false,true,false,false),(false,true,true,i1))]
242  | `ORL (`U1(`A, `DATA b1)) ->
243    [mk_byte_from_bits ((false,true,false,false),(false,true,false,false)); b1]
244  | `ORL (`U2(`DIRECT b1, `A)) ->
245    [mk_byte_from_bits ((false,true,false,false),(false,false,true,false)); b1]
246  | `ORL (`U2 (`DIRECT b1, `DATA b2)) ->
247    [mk_byte_from_bits ((false,true,false,false),(false,false,true,true)); b1; b2]
248  | `ORL (`U3 (`C, `BIT b1)) ->
249    [mk_byte_from_bits ((false,true,true,true),(false,false,true,false)); b1]
250  | `ORL (`U3 (`C, `NBIT b1)) ->
251    [mk_byte_from_bits ((true,false,true,false),(false,false,false,false)); b1]
252  | `POP (`DIRECT b1) ->
253    [mk_byte_from_bits ((true,true,false,true),(false,false,false,false)); b1]
254  | `PUSH (`DIRECT b1) ->
255    [mk_byte_from_bits ((true,true,false,false),(false,false,false,false)); b1]
256  | `RET ->
257    [mk_byte_from_bits ((false,false,true,false),(false,false,true,false))]
258  | `RETI ->
259    [mk_byte_from_bits ((false,false,true,true),(false,false,true,false))]
260  | `RL `A ->
261    [mk_byte_from_bits ((false,false,true,false),(false,false,true,true))]
262  | `RLC `A ->
263    [mk_byte_from_bits ((false,false,true,true),(false,false,true,true))]
264  | `RR `A ->
265    [mk_byte_from_bits ((false,false,false,false),(false,false,true,true))]
266  | `RRC `A ->
267    [mk_byte_from_bits ((false,false,false,true),(false,false,true,true))]
268  | `SETB `C ->
269    [mk_byte_from_bits ((true,true,false,true),(false,false,true,true))]
270  | `SETB (`BIT b1) ->
271    [mk_byte_from_bits ((true,true,false,true),(false,false,true,false)); b1]
272  | `SJMP (`REL b1) ->
273    [mk_byte_from_bits ((true,false,false,false),(false,false,false,false)); b1]
274  | `SUBB (`A, `REG(r1,r2,r3)) ->
275    [mk_byte_from_bits ((true,false,false,true),(true,r1,r2,r3))]
276  | `SUBB (`A, `DIRECT b1) ->
277    [mk_byte_from_bits ((true,false,false,true),(false,true,false,true)); b1]
278  | `SUBB (`A, `INDIRECT i1) ->
279    [mk_byte_from_bits ((true,false,false,true),(false,true,true,i1))]
280  | `SUBB (`A, `DATA b1) ->
281    [mk_byte_from_bits ((true,false,false,true),(false,true,false,false)); b1]
282  | `SWAP `A ->
283    [mk_byte_from_bits ((true,true,false,false),(false,true,false,false))]
284  | `XCH (`A, `REG(r1,r2,r3)) ->
285    [mk_byte_from_bits ((true,true,false,false),(true,r1,r2,r3))]
286  | `XCH (`A, `DIRECT b1) ->
287    [mk_byte_from_bits ((true,true,false,false),(false,true,false,true)); b1]
288  | `XCH (`A, `INDIRECT i1) ->
289    [mk_byte_from_bits ((true,true,false,false),(false,true,true,i1))]
290  | `XCHD(`A, `INDIRECT i1) ->
291    [mk_byte_from_bits ((true,true,false,true),(false,true,true,i1))]
292  | `XRL(`U1(`A, `REG(r1,r2,r3))) ->
293    [mk_byte_from_bits ((false,true,true,false),(true,r1,r2,r3))]
294  | `XRL(`U1(`A, `DIRECT b1)) ->
295    [mk_byte_from_bits ((false,true,true,false),(false,true,false,true)); b1]
296  | `XRL(`U1(`A, `INDIRECT i1)) ->
297    [mk_byte_from_bits ((false,true,true,false),(false,true,true,i1))]
298  | `XRL(`U1(`A, `DATA b1)) ->
299    [mk_byte_from_bits ((false,true,true,false),(false,true,false,false)); b1]
300  | `XRL(`U2(`DIRECT b1, `A)) ->
301    [mk_byte_from_bits ((false,true,true,false),(false,false,true,false)); b1]
302  | `XRL(`U2(`DIRECT b1, `DATA b2)) ->
303    [mk_byte_from_bits ((false,true,true,false),(false,false,true,true)); b1; b2]
304;;
305
306
307
308nrecord Sigma (A: Type[0]) (T: A → Type[0]) : Type[0] ≝ {
309   elem:> A;
310   witness: T elem
311}.
312
313interpretation "Sigma" 'sigma T = (Sigma ? T).
314
315naxiom daemon: False.
316
317naxiom decode_register: Vector Bool (S (S (S Z))) → [reg].
318naxiom decode_direct:   Vector Bool (S (S (S Z))) → [direct].
319
320ndefinition decode_tbl0: List ((Σn.Vector Bool n) × (Vector Bool (S (S (S Z))) → Instruction))
321 ≝
322 [mk_Cartesian ??
323   (mk_Sigma ? (λn.Vector Bool n) ? [ false; false; true; false; true])
324     (λl.
325       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
326             (mk_subaddressing_mode ? ?    (decode_register l) ?));
327  mk_Cartesian ??
328   (mk_Sigma ? (λn.Vector Bool n) ? [ false; false; true; false; true])
329     (λl.
330       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
331             (mk_subaddressing_mode ? ? (decode_direct l) ?)) ].
332ncases daemon.
333nqed.
334
335
336naxiom decode_register: List Bool → [reg].
337naxiom decode_direct: List Bool → [direct].
338
339ndefinition decode_tbl0: List (List Bool × (List Bool → Instruction))
340 ≝
341 [mk_Cartesian ??
342   [ false; false; true; false; true]
343     (λl.
344       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
345             (mk_subaddressing_mode ? ?    (decode_register l) ?));
346  mk_Cartesian ??
347   [ false; false; true; false; true]
348     (λl.
349       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
350             (mk_subaddressing_mode ? ? (decode_direct l) ?)) ].
351ncases daemon.
352nqed.
353
354
355ndefinition decode_tbl1:
356 List (List Bool × Σaddr:all_types. [addr] → Instruction)
357 ≝
358 [mk_Cartesian ??
359   [ false; false; true; false; true]
360   (mk_Sigma ? (λaddr:all_types. [addr] → Instruction)
361     reg
362     (λa.
363       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
364             (mk_subaddressing_mode ? ? a ?))) ].
365ncases daemon.
366nqed.
367             
368ndefinition decode_tbl2:
369 List (List Bool × Σaddr:all_types. [addr] → Instruction)
370 ≝
371 [mk_Cartesian ??
372   [ false; false; true; false; false; true; false; true]
373   (mk_Sigma ? (λaddr:all_types. [addr] → Instruction)
374     direct
375     (λa.
376       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
377             (mk_subaddressing_mode ? ?     a ?))) ].
378ncases daemon.
379nqed.
380
381ndefinition decode_tbl ≝ decode_tbl1 @ decode_tbl2.
382
383decode_addr_mode; ∀addr:all_types. List Bool → [addr].
384
385decode ≝
386 λl:List Bit.
387  List.iter
388   (fun l0 addr mk_f →
389     match split_prefix l l0 with
390      [ None ⇒ ...
391      | Some r ⇒ mk_f (decode_addr_mode r) ]
392     
393   ) decode_tbl
394
395encode ≝
396
397ndefinition decode_tbl:
398 List (List Bool × Σaddr:all_types. [addr] → Instruction)
399 ≝
400 [mk_Cartesian ??
401   [ False; False; True; False; True]
402   (mk_Sigma all_types (λaddr:all_types. [addr] → Instruction)
403     reg
404     (λa:subaddressing_mode ? [reg].
405       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
406             (mk_subaddressing_mode ? ?     a ?)));
407  mk_Cartesian ??
408   [ False; False; True; False; False; True; False; True]
409   (mk_Sigma all_types (λaddr:all_types. [addr] → Instruction)
410     direct
411     (λa:subaddressing_mode ? [direct].
412       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
413             (mk_subaddressing_mode ? ?     a ?)))
414 ].
415nnormalize;
416 
417 ].
418
Note: See TracBrowser for help on using the repository browser.