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

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

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