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

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

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