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

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