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

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

assembly1 completed, but two cases commented out since they require infinite
time (why??)

File size: 26.4 KB
Line 
1include "ASM.ma".
2
3ndefinition assembly1 ≝
4 λi: instruction.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;r3]]) ]
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;r3]]) ]
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;r3]]) ]
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  | CLR addr ⇒
57     match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with
58      [ ACC_A ⇒ λ_.
59         [ ([[true; true; true; false; false; true; false; false]]) ]
60      | CARRY ⇒ λ_.
61         [ ([[true; true; false; false; false; false; true; true]]) ]
62      | BIT_ADDR b1 ⇒ λ_.
63         [ ([[true; true; false; false; false; false; true; false]]) ; b1 ]
64      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
65  | CPL addr ⇒
66     match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with
67      [ ACC_A ⇒ λ_.
68         [ ([[true; true; true; true; false; true; false; false]]) ]
69      | CARRY ⇒ λ_.
70         [ ([[true; false; true; true; false; false; true; true]]) ]
71      | BIT_ADDR b1 ⇒ λ_.
72         [ ([[true; false; true; true; false; false; true; false]]) ; b1 ]
73      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
74  | DA addr ⇒
75     [ ([[true; true; false; true; false; true; false; false]]) ]
76  | DEC addr ⇒
77     match addr return λx. bool_to_Prop (is_in ? [[acc_a;register;direct;indirect]] x) → ? with
78      [ ACC_A ⇒ λ_.
79         [ ([[false; false; false; true; false; true; false; false]]) ]
80      | REGISTER r1 r2 r3 ⇒ λ_.
81         [ ([[false; false; false; true; true; r1; r2; r3]]) ]
82      | DIRECT b1 ⇒ λ_.
83         [ ([[false; false; false; true; false; true; false; true]]); b1 ]
84      | INDIRECT i1 ⇒ λ_.
85         [ ([[false; false; false; true; false; true; true; i1]]) ]
86      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
87  | DIV addr1 addr2 ⇒
88     [ ([[true;false;false;false;false;true;false;false]]) ]
89  | Jump j ⇒
90     match j with
91      [ DJNZ addr1 addr2 ⇒
92         let b2 ≝
93          match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
94           [ RELATIVE b2 ⇒ λ_. b2
95           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
96         match addr1 return λx. bool_to_Prop (is_in ? [[register;direct]] x) → ? with
97          [ REGISTER r1 r2 r3 ⇒ λ_.
98             [ ([[true; true; false; true; true; r1; r2; r3]]) ; b2 ]
99          | DIRECT b1 ⇒ λ_.
100             [ ([[true; true; false; true; false; true; false; true]]); b1; b2 ]
101          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
102      | JC addr ⇒
103         match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
104          [ RELATIVE b1 ⇒ λ_.
105             [ ([[false; true; false; false; false; false; false; false]]); b1 ]
106          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
107      | JNC addr ⇒
108         match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
109          [ RELATIVE b1 ⇒ λ_.
110             [ ([[false; true; false; true; false; false; false; false]]); b1 ]
111          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
112      | JZ addr ⇒
113         match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
114          [ RELATIVE b1 ⇒ λ_.
115             [ ([[false; true; true; false; false; false; false; false]]); b1 ]
116          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
117      | JNZ addr ⇒
118         match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
119          [ RELATIVE b1 ⇒ λ_.
120             [ ([[false; true; true; true; false; false; false; false]]); b1 ]
121          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
122      | JB addr1 addr2 ⇒
123         let b2 ≝
124          match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
125           [ RELATIVE b2 ⇒ λ_. b2
126           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
127         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
128          [ BIT_ADDR b1 ⇒ λ_.
129             [ ([[false; false; true; false; false; false; false; false]]); b1; b2 ]
130          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
131      | JNB addr1 addr2 ⇒
132         let b2 ≝
133          match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
134           [ RELATIVE b2 ⇒ λ_. b2
135           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
136         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
137          [ BIT_ADDR b1 ⇒ λ_.
138             [ ([[false; false; true; true; false; false; false; false]]); b1; b2 ]
139          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
140      | JBC addr1 addr2 ⇒
141         let b2 ≝
142          match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
143           [ RELATIVE b2 ⇒ λ_. b2
144           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
145         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
146          [ BIT_ADDR b1 ⇒ λ_.
147             [ ([[false; false; false; true; false; false; false; false]]); b1; b2 ]
148          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
149      | CJNE addrs addr3 ⇒
150         let b3 ≝
151          match addr3 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
152           [ RELATIVE b3 ⇒ λ_. b3
153           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr3) in
154         match addrs with
155          [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
156             match addr2 return λx. bool_to_Prop (is_in ? [[direct;data]] x) → ? with
157              [ DIRECT b1 ⇒ λ_.
158                 [ ([[true; false; true; true; false; true; false; true]]); b1; b3 ]
159              | DATA b1 ⇒ λ_.
160                 [ ([[true; false; true; true; false; true; false; false]]); b1; b3 ]
161              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
162          | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
163             let b2 ≝
164              match addr2 return λx. bool_to_Prop (is_in ? [[data]] x) → ? with
165               [ DATA b2 ⇒ λ_. b2
166               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
167
168[ ] (*
169             match addr1 return λx. bool_to_Prop (is_in ? [[register;indirect]] x) → ? with
170              [ REGISTER r1 r2 r3 ⇒ λ_. [](*
171                 [ ([[true; false; true; true; true; r1; r2; r3]]); b2; b3 ]*)
172              | INDIRECT i1 ⇒ λ_. [] (*
173                 [ ([[true; false; true; true; false; true; true; i1]]); b2; b3 ] *)
174              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)*) ]]
175  | INC addr ⇒
176     match addr return λx. bool_to_Prop (is_in ? [[acc_a;register;direct;indirect;dptr]] x) → ? with
177      [ ACC_A ⇒ λ_.
178         [ ([[false;false;false;false;false;true;false;false]]) ]         
179      | REGISTER r1 r2 r3 ⇒ λ_.
180         [ ([[false;false;false;false;true;r1;r2;r3]]) ]
181      | DIRECT b1 ⇒ λ_.
182         [ ([[false; false; false; false; false; true; false; true]]); b1 ]
183      | INDIRECT i1 ⇒ λ_.
184        [ ([[false; false; false; false; false; true; true; i1]]) ]
185      | DPTR ⇒ λ_.
186        [ ([[true;false;true;false;false;false;true;true]]) ]
187      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
188  | JMP addr ⇒
189     [ ([[false;true;true;true;false;false;true;true]]) ]
190  | LCALL addr ⇒
191     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
192      [ ADDR16 w ⇒ λ_.
193         let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S (S (S (S (S (S Z)))))))) w in
194          [ ([[false;false;false;true;false;false;true;false]]); b1; b2 ]         
195      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
196  | LJMP addr ⇒
197     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
198      [ ADDR16 w ⇒ λ_.
199         let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S (S (S (S (S (S Z)))))))) w in
200          [ ([[false;false;false;false;false;false;true;false]]); b1; b2 ]         
201      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
202  | MOV addrs ⇒
203     match addrs with
204      [ Left addrs ⇒
205         match addrs with
206          [ Left addrs ⇒
207             match addrs with
208              [ Left addrs ⇒
209                 match addrs with
210                  [ Left addrs ⇒
211                     match addrs with
212                      [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
213                         match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
214                          [ REGISTER r1 r2 r3 ⇒ λ_.[ ([[true;true;true;false;true;r1;r2;r3]]) ]
215                          | DIRECT b1 ⇒ λ_.[ ([[true;true;true;false;false;true;false;true]]); b1 ]
216                          | INDIRECT i1 ⇒ λ_. [ ([[true;true;true;false;false;true;true;i1]]) ]
217                          | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;false;false]]) ; b1 ]
218                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
219                      | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
220                         match addr1 return λx. bool_to_Prop (is_in ? [[register;indirect]] x) → ? with
221                          [ REGISTER r1 r2 r3 ⇒ λ_.
222                             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with
223                              [ ACC_A ⇒ λ_.[ ([[true;true;true;true;true;r1;r2;r3]]) ]
224                              | DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;true;r1;r2;r3]]); b1 ]
225                              | DATA b1 ⇒ λ_. [ ([[false;true;true;true;true;r1;r2;r3]]) ; b1 ]
226                              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
227                          | INDIRECT i1 ⇒ λ_.
228                             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with
229                              [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;true;i1]]) ]
230                              | DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;false;true;true;i1]]); b1 ]
231                              | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;true;i1]]) ; b1 ]
232                              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
233                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
234                  | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in [] (*
235                     let b1 ≝
236                      match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
237                       [ DIRECT b1 ⇒ λ_. b1
238                       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
239                     match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;register;direct;indirect;data]] x) → ? with
240                      [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;false;true]]); b1]
241                      | REGISTER r1 r2 r3 ⇒ λ_.[ ([[true;false;false;false;true;r1;r2;r3]]); b1 ]
242                      | DIRECT b2 ⇒ λ_.[ ([[true;false;false;false;false;true;false;true]]); b1; b2 ]
243                      | INDIRECT i1 ⇒ λ_. [ ([[true;false;false;false;false;true;true;i1]]); b1 ]
244                      | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;false;true]]); b1; b2 ]
245                      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)*)]
246              | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
247                 match addr2 return λx. bool_to_Prop (is_in ? [[data16]] x) → ? with
248                  [ DATA16 w ⇒ λ_.
249                     let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S (S (S (S (S (S Z)))))))) w in
250                      [ ([[true;false;false;true;false;false;false;false]]); b1; b2]
251                  | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
252          | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
253             match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
254              [ BIT_ADDR b1 ⇒ λ_.
255                 [ ([[true;false;true;false;false;false;true;false]]); b1 ]
256              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
257      | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
258         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
259          [ BIT_ADDR b1 ⇒ λ_.
260             [ ([[true;false;false;true;false;false;true;false]]); b1 ]
261          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
262  | MOVC addr1 addr2 ⇒
263     match addr2 return λx. bool_to_Prop (is_in ? [[acc_dptr;acc_pc]] x) → ? with
264      [ ACC_DPTR ⇒ λ_.
265         [ ([[true;false;false;true;false;false;true;true]]) ]
266      | ACC_PC ⇒ λ_.
267         [ ([[true;false;false;false;false;false;true;true]]) ]
268      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
269  | MOVX addrs ⇒
270     match addrs with
271      [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
272         match addr2 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
273          [ EXT_INDIRECT i1 ⇒ λ_.
274             [ ([[true;true;true;false;false;false;true;i1]]) ]
275          | EXT_INDIRECT_DPTR ⇒ λ_.
276             [ ([[true;true;true;false;false;false;false;false]]) ]
277          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
278      | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
279         match addr1 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
280          [ EXT_INDIRECT i1 ⇒ λ_.
281             [ ([[true;true;true;true;false;false;true;i1]]) ]
282          | EXT_INDIRECT_DPTR ⇒ λ_.
283             [ ([[true;true;true;true;false;false;false;false]]) ]
284          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
285  | MUL addr1 addr2 ⇒
286     [ ([[true;false;true;false;false;true;false;false]]) ]
287  | NOP ⇒
288     [ ([[false;false;false;false;false;false;false;false]]) ]
289  | ORL addrs ⇒
290     match addrs with
291      [ Left addrs ⇒
292         match addrs with
293          [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
294             match addr2 return λx. bool_to_Prop (is_in ? [[register;data;direct;indirect]] x) → ? with
295             [ REGISTER r1 r2 r3 ⇒ λ_.[ ([[false;true;false;false;true;r1;r2;r3]]) ]
296             | DIRECT b1 ⇒ λ_.[ ([[false;true;false;false;false;true;false;true]]); b1 ]
297             | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;false;false;true;true;i1]]) ]
298             | DATA b1 ⇒ λ_. [ ([[false;true;false;false;false;true;false;false]]) ; b1 ]
299             | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
300          | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
301            let b1 ≝
302              match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
303               [ DIRECT b1 ⇒ λ_. b1
304               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
305             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
306              [ ACC_A ⇒ λ_.
307                 [ ([[false;true;false;false;false;false;true;false]]); b1 ]
308              | DATA b2 ⇒ λ_.
309                 [ ([[false;true;false;false;false;false;true;true]]); b1; b2 ]
310              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
311      | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in     
312         match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
313          [ BIT_ADDR b1 ⇒ λ_.
314             [ ([[false;true;true;true;false;false;true;false]]); b1 ]
315          | N_BIT_ADDR b1 ⇒ λ_.
316             [ ([[true;false;true;false;false;false;false;false]]); b1 ]
317          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
318  | POP addr ⇒
319     match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
320      [ DIRECT b1 ⇒ λ_.
321         [ ([[true;true;false;true;false;false;false;false]]) ; b1 ]
322      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
323  | PUSH addr ⇒
324     match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
325      [ DIRECT b1 ⇒ λ_.
326         [ ([[true;true;false;false;false;false;false;false]]) ; b1 ]
327      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
328  | RET ⇒
329     [ ([[false;false;true;false;false;false;true;false]]) ]
330  | RETI ⇒
331     [ ([[false;false;true;true;false;false;true;false]]) ]
332  | RL addr ⇒
333     [ ([[false;false;true;false;false;false;true;true]]) ]
334  | RLC addr ⇒
335     [ ([[false;false;true;true;false;false;true;true]]) ]
336  | RR addr ⇒
337     [ ([[false;false;false;false;false;false;true;true]]) ]
338  | RRC addr ⇒
339     [ ([[false;false;false;true;false;false;true;true]]) ]
340  | SETB addr ⇒     
341     match addr return λx. bool_to_Prop (is_in ? [[carry;bit_addr]] x) → ? with
342      [ CARRY ⇒ λ_.
343         [ ([[true;true;false;true;false;false;true;true]]) ]
344      | BIT_ADDR b1 ⇒ λ_.
345         [ ([[true;true;false;true;false;false;true;false]]); b1 ]
346      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
347  | SJMP addr ⇒
348     match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
349      [ RELATIVE b1 ⇒ λ_.
350         [ ([[true;false;false;false;false;false;false;false]]); b1 ]
351      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
352  | SUBB addr1 addr2 ⇒
353     match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
354      [ REGISTER r1 r2 r3 ⇒ λ_.
355         [ ([[true;false;false;true;true;r1;r2;r3]]) ]
356      | DIRECT b1 ⇒ λ_.
357         [ ([[true;false;false;true;false;true;false;true]]); b1]
358      | INDIRECT i1 ⇒ λ_.
359         [ ([[true;false;false;true;false;true;true;i1]]) ]
360      | DATA b1 ⇒ λ_.
361         [ ([[true;false;false;true;false;true;false;false]]); b1]
362      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
363  | SWAP addr ⇒
364     [ ([[true;true;false;false;false;true;false;false]]) ]
365  | XCH addr1 addr2 ⇒
366     match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect]] x) → ? with
367      [ REGISTER r1 r2 r3 ⇒ λ_.
368         [ ([[true;true;false;false;true;r1;r2;r3]]) ]
369      | DIRECT b1 ⇒ λ_.
370         [ ([[true;true;false;false;false;true;false;true]]); b1]
371      | INDIRECT i1 ⇒ λ_.
372         [ ([[true;true;false;false;false;true;true;i1]]) ]
373      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
374  | XCHD addr1 addr2 ⇒
375     match addr2 return λx. bool_to_Prop (is_in ? [[indirect]] x) → ? with
376      [ INDIRECT i1 ⇒ λ_.
377         [ ([[true;true;false;true;false;true;true;i1]]) ]
378      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
379  | XRL addrs ⇒
380     match addrs with
381      [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
382         match addr2 return λx. bool_to_Prop (is_in ? [[data;register;direct;indirect]] x) → ? with
383          [ REGISTER r1 r2 r3 ⇒ λ_.
384             [ ([[false;true;true;false;true;r1;r2;r3]]) ]
385          | DIRECT b1 ⇒ λ_.
386             [ ([[false;true;true;false;false;true;false;true]]); b1]
387          | INDIRECT i1 ⇒ λ_.
388             [ ([[false;true;true;false;false;true;true;i1]]) ]
389          | DATA b1 ⇒ λ_.
390             [ ([[false;true;true;false;false;true;false;false]]); b1]
391          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
392      | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
393         let b1 ≝
394          match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
395           [ DIRECT b1 ⇒ λ_. b1
396           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
397         match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
398          [ ACC_A ⇒ λ_.
399             [ ([[false;true;true;false;false;false;true;false]]); b1 ]         
400          | DATA b2 ⇒ λ_.
401             [ ([[false;true;true;false;false;false;true;true]]); b1; b2 ]
402          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]].
403
404(*
405let load_code_memory = fold_lefti (fun i mem v -> WordMap.add (vect_of_int i `Sixteen) v mem) WordMap.empty
406
407let load_mem mem status = { status with code_memory = mem }
408let load l = load_mem (load_code_memory l)
409
410module StringMap = Map.Make(String);;
411module IntMap = Map.Make(struct type t = int let compare = compare end);;
412
413
414let assembly_jump addr_of =
415 function
416    `JC a1 -> `JC (addr_of a1)
417  | `JNC a1 -> `JNC (addr_of a1)
418  | `JB (a1,a2) -> `JB (a1,addr_of a2)
419  | `JNB (a1,a2) -> `JNB (a1,addr_of a2)
420  | `JBC (a1,a2) -> `JBC (a1,addr_of a2)
421  | `JZ a1 -> `JZ (addr_of a1)
422  | `JNZ a1 -> `JNZ (addr_of a1)
423  | `CJNE (a1,a2) -> `CJNE (a1,addr_of a2)
424  | `DJNZ (a1,a2) -> `DJNZ (a1,addr_of a2)
425;;
426
427let assembly (preamble,l) =
428 let datalabels,_ =
429  List.fold_left
430   (fun (datalabels,addr) (name,size) ->
431     let addr16 = vect_of_int addr `Sixteen in
432      StringMap.add name addr16 datalabels, addr+size
433   ) (StringMap.empty,0) preamble
434 in
435 let pc,labels,costs =
436  List.fold_left
437   (fun (pc,labels,costs) i ->
438     match i with
439        `Label s -> pc, StringMap.add s pc labels, costs
440      | `Cost s -> pc, labels, IntMap.add pc s costs
441      | `Mov (_,_) -> pc, labels, costs
442      | `Jmp _
443      | `Call _ -> pc + 3, labels, costs  (*CSC: very stupid: always expand to worst opcode *)
444      | `WithLabel i ->
445          let fake_addr _ = `REL (zero `Eight) in
446          let fake_jump = assembly_jump fake_addr i in
447          let i',pc',_ = fetch (load_code_memory (assembly1 fake_jump)) (vect_of_int 0 `Sixteen) in
448           assert (fake_jump = i');
449           (pc + int_of_vect pc',labels, costs)
450      | #instruction as i ->
451        let i',pc',_ = fetch (load_code_memory (assembly1 i)) (vect_of_int 0 `Sixteen) in
452         assert (i = i');
453         (pc + int_of_vect pc',labels, costs)
454   ) (0,StringMap.empty,IntMap.empty) l
455 in
456  if pc >= 65536 then
457   raise CodeTooLarge
458  else
459      List.flatten (List.map
460         (function
461            `Label _
462          | `Cost _ -> []
463          | `WithLabel i ->
464              let addr_of (`Label s) =
465               let addr = StringMap.find s labels in
466               (* NOT IMPLEMENTED YET; NEEDS SMART ALGORITHM *)
467                assert (addr < 256);
468                `REL (vect_of_int addr `Eight)
469              in
470               assembly1 (assembly_jump addr_of i)
471          | `Mov (`DPTR,s) ->
472              let addrr16 = StringMap.find s datalabels in
473               assembly1 (`MOV (`U4 (`DPTR,`DATA16 addrr16)))
474          | `Jmp s ->
475              let pc_offset = StringMap.find s labels in
476                assembly1 (`LJMP (`ADDR16 (vect_of_int pc_offset `Sixteen)))
477          | `Call s ->
478              let pc_offset = StringMap.find s labels in
479                assembly1 (`LCALL (`ADDR16 (vect_of_int pc_offset `Sixteen)))
480          | #instruction as i -> assembly1 i) l), costs
481;;
482*)
Note: See TracBrowser for help on using the repository browser.