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

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