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

Last change on this file since 410 was 410, checked in by mulligan, 9 years ago

Using bitvectortries for a dictionary doesn't work even if we hypothesise conversion functions from bitvectors to string, and back again. Many changes, including most of the assembly function implemented.

File size: 30.1 KB
Line 
1include "ASM.ma".
2include "BitVectorTrie.ma".
3
4ndefinition assembly1 ≝
5 λi: instruction.match i with
6  [ ACALL addr ⇒
7     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
8      [ ADDR11 w ⇒ λ_.
9         let 〈v1,v2〉 ≝ split ? (S (S (S Z))) (S (S (S (S (S (S (S (S Z)))))))) w in
10          [ (v1 @@ [[true; false; false; false; true]]) ; v2 ]
11      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
12  | ADD addr1 addr2 ⇒
13     match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
14      [ REGISTER r ⇒ λ_.[ ([[false;false;true;false;true]]) @@ r ]
15      | DIRECT b1 ⇒ λ_.[ ([[false;false;true;false;false;true;false;true]]); b1 ]
16      | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;false;false;true;true;i1]]) ]
17      | DATA b1 ⇒ λ_. [ ([[false;false;true;false;false;true;false;false]]) ; b1 ]
18      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
19  | ADDC addr1 addr2 ⇒
20     match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
21      [ REGISTER r ⇒ λ_.[ ([[false;false;true;true;true]]) @@ r ]
22      | DIRECT b1 ⇒ λ_.[ ([[false;false;true;true;false;true;false;true]]); b1 ]
23      | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;true;false;true;true;i1]]) ]
24      | DATA b1 ⇒ λ_. [ ([[false;false;true;true;false;true;false;false]]) ; b1 ]
25      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
26  | AJMP addr ⇒
27     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
28      [ ADDR11 w ⇒ λ_.
29         let 〈v1,v2〉 ≝ split ?  (S (S (S Z))) (S (S (S (S (S (S (S (S Z)))))))) w in
30          [ (v1 @@ [[false; false; false; false; true]]) ; v2 ]
31      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
32  | ANL addrs ⇒
33     match addrs with
34      [ Left addrs ⇒ match addrs with
35         [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
36           match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
37            [ REGISTER r ⇒ λ_.[ ([[false;true;false;true;true]]) @@ r ]
38            | DIRECT b1 ⇒ λ_.[ ([[false;true;false;true;false;true;false;true]]); b1 ]
39            | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;true;false;true;true;i1]]) ]
40            | DATA b1 ⇒ λ_. [ ([[false;true;false;true;false;true;false;false]]) ; b1 ]
41            | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
42         | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
43            let b1 ≝
44             match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
45              [ DIRECT b1 ⇒ λ_.b1
46              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
47            match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
48             [ ACC_A ⇒ λ_.[ ([[false;true;false;true;false;false;true;false]]) ; b1 ]
49             | DATA b2 ⇒ λ_. [ ([[false;true;false;true;false;false;true;true]]) ; b1 ; b2 ]
50             | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
51         ]
52      | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
53         match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
54          [ BIT_ADDR b1 ⇒ λ_.[ ([[true;false;false;false;false;false;true;false]]) ; b1 ]
55          | N_BIT_ADDR b1 ⇒ λ_. [ ([[true;false;true;true;false;false;false;false]]) ; b1 ]
56          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
57  | CLR addr ⇒
58     match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with
59      [ ACC_A ⇒ λ_.
60         [ ([[true; true; true; false; false; true; false; false]]) ]
61      | CARRY ⇒ λ_.
62         [ ([[true; true; false; false; false; false; true; true]]) ]
63      | BIT_ADDR b1 ⇒ λ_.
64         [ ([[true; true; false; false; false; false; true; false]]) ; b1 ]
65      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
66  | CPL 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; true; false; true; false; false]]) ]
70      | CARRY ⇒ λ_.
71         [ ([[true; false; true; true; false; false; true; true]]) ]
72      | BIT_ADDR b1 ⇒ λ_.
73         [ ([[true; false; true; true; false; false; true; false]]) ; b1 ]
74      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
75  | DA addr ⇒
76     [ ([[true; true; false; true; false; true; false; false]]) ]
77  | DEC addr ⇒
78     match addr return λx. bool_to_Prop (is_in ? [[acc_a;register;direct;indirect]] x) → ? with
79      [ ACC_A ⇒ λ_.
80         [ ([[false; false; false; true; false; true; false; false]]) ]
81      | REGISTER r ⇒ λ_.
82         [ ([[false; false; false; true; true]]) @@ r ]
83      | DIRECT b1 ⇒ λ_.
84         [ ([[false; false; false; true; false; true; false; true]]); b1 ]
85      | INDIRECT i1 ⇒ λ_.
86         [ ([[false; false; false; true; false; true; true; i1]]) ]
87      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
88  | DIV addr1 addr2 ⇒
89     [ ([[true;false;false;false;false;true;false;false]]) ]
90  | Jump j ⇒
91     match j with
92      [ DJNZ addr1 addr2 ⇒
93         let b2 ≝
94          match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
95           [ RELATIVE b2 ⇒ λ_. b2
96           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
97         match addr1 return λx. bool_to_Prop (is_in ? [[register;direct]] x) → ? with
98          [ REGISTER r ⇒ λ_.
99             [ ([[true; true; false; true; true]]) @@ r ; b2 ]
100          | DIRECT b1 ⇒ λ_.
101             [ ([[true; true; false; true; false; true; false; true]]); b1; b2 ]
102          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
103      | JC addr ⇒
104         match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
105          [ RELATIVE b1 ⇒ λ_.
106             [ ([[false; true; false; false; false; false; false; false]]); b1 ]
107          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
108      | JNC addr ⇒
109         match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
110          [ RELATIVE b1 ⇒ λ_.
111             [ ([[false; true; false; true; false; false; false; false]]); b1 ]
112          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
113      | JZ addr ⇒
114         match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
115          [ RELATIVE b1 ⇒ λ_.
116             [ ([[false; true; true; false; false; false; false; false]]); b1 ]
117          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
118      | JNZ addr ⇒
119         match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
120          [ RELATIVE b1 ⇒ λ_.
121             [ ([[false; true; true; true; false; false; false; false]]); b1 ]
122          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
123      | JB addr1 addr2 ⇒
124         let b2 ≝
125          match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
126           [ RELATIVE b2 ⇒ λ_. b2
127           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
128         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
129          [ BIT_ADDR b1 ⇒ λ_.
130             [ ([[false; false; true; false; false; false; false; false]]); b1; b2 ]
131          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
132      | JNB addr1 addr2 ⇒
133         let b2 ≝
134          match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
135           [ RELATIVE b2 ⇒ λ_. b2
136           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
137         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
138          [ BIT_ADDR b1 ⇒ λ_.
139             [ ([[false; false; true; true; false; false; false; false]]); b1; b2 ]
140          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
141      | JBC addr1 addr2 ⇒
142         let b2 ≝
143          match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
144           [ RELATIVE b2 ⇒ λ_. b2
145           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
146         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
147          [ BIT_ADDR b1 ⇒ λ_.
148             [ ([[false; false; false; true; false; false; false; false]]); b1; b2 ]
149          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
150      | CJNE addrs addr3 ⇒
151         let b3 ≝
152          match addr3 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
153           [ RELATIVE b3 ⇒ λ_. b3
154           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr3) in
155         match addrs with
156          [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
157             match addr2 return λx. bool_to_Prop (is_in ? [[direct;data]] x) → ? with
158              [ DIRECT b1 ⇒ λ_.
159                 [ ([[true; false; true; true; false; true; false; true]]); b1; b3 ]
160              | DATA b1 ⇒ λ_.
161                 [ ([[true; false; true; true; false; true; false; false]]); b1; b3 ]
162              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
163          | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
164             let b2 ≝
165              match addr2 return λx. bool_to_Prop (is_in ? [[data]] x) → ? with
166               [ DATA b2 ⇒ λ_. b2
167               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
168             match addr1 return λx. bool_to_Prop (is_in ? [[register;indirect]] x) → List Byte with
169              [ REGISTER r⇒ λ_.
170                 [ ([[true; false; true; true; true]]) @@ r; b2; b3 ]
171              | INDIRECT i1 ⇒ λ_.
172                 [ ([[true; false; true; true; false; true; true; i1]]); b2; b3 ]
173              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) ]]
174  | INC addr ⇒
175     match addr return λx. bool_to_Prop (is_in ? [[acc_a;register;direct;indirect;dptr]] x) → ? with
176      [ ACC_A ⇒ λ_.
177         [ ([[false;false;false;false;false;true;false;false]]) ]         
178      | REGISTER r ⇒ λ_.
179         [ ([[false;false;false;false;true]]) @@ r ]
180      | DIRECT b1 ⇒ λ_.
181         [ ([[false; false; false; false; false; true; false; true]]); b1 ]
182      | INDIRECT i1 ⇒ λ_.
183        [ ([[false; false; false; false; false; true; true; i1]]) ]
184      | DPTR ⇒ λ_.
185        [ ([[true;false;true;false;false;false;true;true]]) ]
186      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
187  | JMP addr ⇒
188     [ ([[false;true;true;true;false;false;true;true]]) ]
189  | LCALL addr ⇒
190     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
191      [ ADDR16 w ⇒ λ_.
192         let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S (S (S (S (S (S Z)))))))) w in
193          [ ([[false;false;false;true;false;false;true;false]]); b1; b2 ]         
194      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
195  | LJMP addr ⇒
196     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
197      [ ADDR16 w ⇒ λ_.
198         let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S (S (S (S (S (S Z)))))))) w in
199          [ ([[false;false;false;false;false;false;true;false]]); b1; b2 ]         
200      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
201  | MOV addrs ⇒
202     match addrs with
203      [ Left addrs ⇒
204         match addrs with
205          [ Left addrs ⇒
206             match addrs with
207              [ Left addrs ⇒
208                 match addrs with
209                  [ Left addrs ⇒
210                     match addrs with
211                      [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
212                         match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
213                          [ REGISTER r ⇒ λ_.[ ([[true;true;true;false;true]]) @@ r ]
214                          | DIRECT b1 ⇒ λ_.[ ([[true;true;true;false;false;true;false;true]]); b1 ]
215                          | INDIRECT i1 ⇒ λ_. [ ([[true;true;true;false;false;true;true;i1]]) ]
216                          | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;false;false]]) ; b1 ]
217                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
218                      | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
219                         match addr1 return λx. bool_to_Prop (is_in ? [[register;indirect]] x) → ? with
220                          [ REGISTER r ⇒ λ_.
221                             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with
222                              [ ACC_A ⇒ λ_.[ ([[true;true;true;true;true]]) @@ r ]
223                              | DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;true]]) @@ r; b1 ]
224                              | DATA b1 ⇒ λ_. [ ([[false;true;true;true;true]]) @@ r; b1 ]
225                              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
226                          | INDIRECT i1 ⇒ λ_.
227                             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with
228                              [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;true;i1]]) ]
229                              | DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;false;true;true;i1]]); b1 ]
230                              | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;true;i1]]) ; b1 ]
231                              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
232                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
233                  | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
234                     let b1 ≝
235                      match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
236                       [ DIRECT b1 ⇒ λ_. b1
237                       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
238                     match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;register;direct;indirect;data]] x) → ? with
239                      [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;false;true]]); b1]
240                      | REGISTER r ⇒ λ_.[ ([[true;false;false;false;true]]) @@ r; b1 ]
241                      | DIRECT b2 ⇒ λ_.[ ([[true;false;false;false;false;true;false;true]]); b1; b2 ]
242                      | INDIRECT i1 ⇒ λ_. [ ([[true;false;false;false;false;true;true;i1]]); b1 ]
243                      | DATA b2 ⇒ λ_. [ ([[false;true;true;true;false;true;false;true]]); b1; b2 ]
244                      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
245              | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
246                 match addr2 return λx. bool_to_Prop (is_in ? [[data16]] x) → ? with
247                  [ DATA16 w ⇒ λ_.
248                     let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S (S (S (S (S (S Z)))))))) w in
249                      [ ([[true;false;false;true;false;false;false;false]]); b1; b2]
250                  | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
251          | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
252             match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
253              [ BIT_ADDR b1 ⇒ λ_.
254                 [ ([[true;false;true;false;false;false;true;false]]); b1 ]
255              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
256      | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
257         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
258          [ BIT_ADDR b1 ⇒ λ_.
259             [ ([[true;false;false;true;false;false;true;false]]); b1 ]
260          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
261  | MOVC addr1 addr2 ⇒
262     match addr2 return λx. bool_to_Prop (is_in ? [[acc_dptr;acc_pc]] x) → ? with
263      [ ACC_DPTR ⇒ λ_.
264         [ ([[true;false;false;true;false;false;true;true]]) ]
265      | ACC_PC ⇒ λ_.
266         [ ([[true;false;false;false;false;false;true;true]]) ]
267      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
268  | MOVX addrs ⇒
269     match addrs with
270      [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
271         match addr2 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
272          [ EXT_INDIRECT i1 ⇒ λ_.
273             [ ([[true;true;true;false;false;false;true;i1]]) ]
274          | EXT_INDIRECT_DPTR ⇒ λ_.
275             [ ([[true;true;true;false;false;false;false;false]]) ]
276          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
277      | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
278         match addr1 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
279          [ EXT_INDIRECT i1 ⇒ λ_.
280             [ ([[true;true;true;true;false;false;true;i1]]) ]
281          | EXT_INDIRECT_DPTR ⇒ λ_.
282             [ ([[true;true;true;true;false;false;false;false]]) ]
283          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
284  | MUL addr1 addr2 ⇒
285     [ ([[true;false;true;false;false;true;false;false]]) ]
286  | NOP ⇒
287     [ ([[false;false;false;false;false;false;false;false]]) ]
288  | ORL addrs ⇒
289     match addrs with
290      [ Left addrs ⇒
291         match addrs with
292          [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
293             match addr2 return λx. bool_to_Prop (is_in ? [[register;data;direct;indirect]] x) → ? with
294             [ REGISTER r ⇒ λ_.[ ([[false;true;false;false;true]]) @@ r ]
295             | DIRECT b1 ⇒ λ_.[ ([[false;true;false;false;false;true;false;true]]); b1 ]
296             | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;false;false;true;true;i1]]) ]
297             | DATA b1 ⇒ λ_. [ ([[false;true;false;false;false;true;false;false]]) ; b1 ]
298             | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
299          | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
300            let b1 ≝
301              match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
302               [ DIRECT b1 ⇒ λ_. b1
303               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
304             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
305              [ ACC_A ⇒ λ_.
306                 [ ([[false;true;false;false;false;false;true;false]]); b1 ]
307              | DATA b2 ⇒ λ_.
308                 [ ([[false;true;false;false;false;false;true;true]]); b1; b2 ]
309              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
310      | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in     
311         match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
312          [ BIT_ADDR b1 ⇒ λ_.
313             [ ([[false;true;true;true;false;false;true;false]]); b1 ]
314          | N_BIT_ADDR b1 ⇒ λ_.
315             [ ([[true;false;true;false;false;false;false;false]]); b1 ]
316          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
317  | POP addr ⇒
318     match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
319      [ DIRECT b1 ⇒ λ_.
320         [ ([[true;true;false;true;false;false;false;false]]) ; b1 ]
321      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
322  | PUSH addr ⇒
323     match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
324      [ DIRECT b1 ⇒ λ_.
325         [ ([[true;true;false;false;false;false;false;false]]) ; b1 ]
326      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
327  | RET ⇒
328     [ ([[false;false;true;false;false;false;true;false]]) ]
329  | RETI ⇒
330     [ ([[false;false;true;true;false;false;true;false]]) ]
331  | RL addr ⇒
332     [ ([[false;false;true;false;false;false;true;true]]) ]
333  | RLC addr ⇒
334     [ ([[false;false;true;true;false;false;true;true]]) ]
335  | RR addr ⇒
336     [ ([[false;false;false;false;false;false;true;true]]) ]
337  | RRC addr ⇒
338     [ ([[false;false;false;true;false;false;true;true]]) ]
339  | SETB addr ⇒     
340     match addr return λx. bool_to_Prop (is_in ? [[carry;bit_addr]] x) → ? with
341      [ CARRY ⇒ λ_.
342         [ ([[true;true;false;true;false;false;true;true]]) ]
343      | BIT_ADDR b1 ⇒ λ_.
344         [ ([[true;true;false;true;false;false;true;false]]); b1 ]
345      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
346  | SJMP addr ⇒
347     match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
348      [ RELATIVE b1 ⇒ λ_.
349         [ ([[true;false;false;false;false;false;false;false]]); b1 ]
350      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
351  | SUBB addr1 addr2 ⇒
352     match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
353      [ REGISTER r ⇒ λ_.
354         [ ([[true;false;false;true;true]]) @@ r ]
355      | DIRECT b1 ⇒ λ_.
356         [ ([[true;false;false;true;false;true;false;true]]); b1]
357      | INDIRECT i1 ⇒ λ_.
358         [ ([[true;false;false;true;false;true;true;i1]]) ]
359      | DATA b1 ⇒ λ_.
360         [ ([[true;false;false;true;false;true;false;false]]); b1]
361      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
362  | SWAP addr ⇒
363     [ ([[true;true;false;false;false;true;false;false]]) ]
364  | XCH addr1 addr2 ⇒
365     match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect]] x) → ? with
366      [ REGISTER r ⇒ λ_.
367         [ ([[true;true;false;false;true]]) @@ r ]
368      | DIRECT b1 ⇒ λ_.
369         [ ([[true;true;false;false;false;true;false;true]]); b1]
370      | INDIRECT i1 ⇒ λ_.
371         [ ([[true;true;false;false;false;true;true;i1]]) ]
372      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
373  | XCHD addr1 addr2 ⇒
374     match addr2 return λx. bool_to_Prop (is_in ? [[indirect]] x) → ? with
375      [ INDIRECT i1 ⇒ λ_.
376         [ ([[true;true;false;true;false;true;true;i1]]) ]
377      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
378  | XRL addrs ⇒
379     match addrs with
380      [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
381         match addr2 return λx. bool_to_Prop (is_in ? [[data;register;direct;indirect]] x) → ? with
382          [ REGISTER r ⇒ λ_.
383             [ ([[false;true;true;false;true]]) @@ r ]
384          | DIRECT b1 ⇒ λ_.
385             [ ([[false;true;true;false;false;true;false;true]]); b1]
386          | INDIRECT i1 ⇒ λ_.
387             [ ([[false;true;true;false;false;true;true;i1]]) ]
388          | DATA b1 ⇒ λ_.
389             [ ([[false;true;true;false;false;true;false;false]]); b1]
390          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
391      | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
392         let b1 ≝
393          match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
394           [ DIRECT b1 ⇒ λ_. b1
395           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
396         match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
397          [ ACC_A ⇒ λ_.
398             [ ([[false;true;true;false;false;false;true;false]]); b1 ]         
399          | DATA b2 ⇒ λ_.
400             [ ([[false;true;true;false;false;false;true;true]]); b1; b2 ]
401          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]].
402
403include "Arithmetic.ma".
404include "Fetch.ma".
405include "Status.ma".
406
407ndefinition assembly_jump ≝
408  λA, B: Type[0].
409  λj.
410  λaddr_of: A → B.
411    match j with
412      [ JC jmp ⇒ JC ? (addr_of jmp)
413      | JNC jmp ⇒ JNC ? (addr_of jmp)
414      | JZ jmp ⇒ JZ ? (addr_of jmp)
415      | JNZ jmp ⇒ JNZ ? (addr_of jmp)
416      | JB jmp jmp' ⇒ JB ? jmp (addr_of jmp')
417      | JNB jmp jmp' ⇒ JNB ? jmp (addr_of jmp')
418      | JBC jmp jmp' ⇒ JBC ? jmp (addr_of jmp')
419      | CJNE jmp jmp' ⇒ CJNE ? jmp (addr_of jmp')
420      | DJNZ jmp jmp' ⇒ DJNZ ? jmp (addr_of jmp')
421      ].
422
423ndefinition assembly: assembly_program → Maybe (List Byte × (BitVectorTrie ? sixteen)) ≝
424  λp.
425    let 〈preamble, instr_list〉 ≝ p in
426    let 〈datalabels, ignore〉 ≝
427      fold_left ? ? (
428        λt. λpreamble.
429          let 〈datalabels, addr〉 ≝ t in
430          let 〈name, size〉 ≝ preamble in
431          let addr_sixteen ≝ bitvector_of_nat sixteen addr in
432            〈insert ? ? addr_sixteen name datalabels, addr + size〉)
433              〈(Stub ? ?), Z〉 preamble in
434    let 〈pc_labels, costs〉 ≝
435      fold_left ? ? (
436        λt. λi.
437          let 〈pc_labels, costs〉 ≝ t in
438          let 〈program_counter, labels〉 ≝ pc_labels in
439            match i with
440              [ Instruction instr ⇒
441                let code_memory ≝ load_code_memory (assembly1 instr) in
442                let 〈instr_pc', ignore〉  ≝ fetch code_memory (zero sixteen) in
443                let 〈instr', program_counter'〉 ≝ instr_pc' in
444                let program_counter_n' ≝ nat_of_bitvector ? program_counter' in
445                  〈〈program_counter + program_counter_n', labels〉, costs〉
446              | Label label ⇒
447                let program_counter_bv ≝ bitvector_of_nat sixteen program_counter in
448                  〈〈program_counter, (insert ? ? program_counter_bv label labels)〉, costs〉
449              | Cost cost ⇒
450                let program_counter_bv ≝ bitvector_of_nat sixteen program_counter in
451                  〈pc_labels, (insert ? ? program_counter_bv cost costs)〉
452              | Jmp jmp ⇒
453                  〈〈program_counter + three, labels〉, costs〉
454              | Call call ⇒
455                  〈〈program_counter + three, labels〉, costs〉
456              | Mov dptr trgt ⇒ t
457              | WithLabel jmp ⇒ ? (*
458                let fake_addr ≝ RELATIVE (zero eight) in
459                let fake_jump ≝ assembly_jump ? ? jmp (λx. fake_addr) in
460                let code_memory ≝ load_code_memory (assembly1 (Jump relative fake_jump)) in
461                let 〈instr_pc', ignore〉  ≝ fetch code_memory (zero sixteen) in
462                let 〈instr', program_counter'〉 ≝ instr_pc' in
463                let program_counter_n' ≝ nat_of_bitvector ? program_counter' in
464                  〈〈program_counter + program_counter_n', labels〉, costs〉 *)
465              ]
466          ) 〈〈Z, (Stub ? ?)〉, (Stub ? ?)〉 instr_list in
467    let 〈program_counter, labels〉 ≝ pc_labels in
468      if greater_than_b program_counter
469                        sixty_five_thousand_five_hundred_and_thirty_six then
470        Nothing ?
471      else
472        let flat_list ≝
473          flatten ? (
474            map ? ? (
475              λi: labelled_instruction.
476                match i with
477                  [ Cost cost ⇒ [ ]
478                  | Label label ⇒ [ ]
479                  | Call call ⇒
480                    let pc_offset ≝ lookup ? ? (bitvector_of_string ? call) labels (zero ?) in
481                    let address ≝ ADDR16 (bitvector_of_nat sixteen pc_offset) in
482                      assembly1 (LCALL address)
483                  | _ ⇒ ?
484                  ]
485            ) instr_list
486          ) in
487        Just ? 〈flat_list, costs〉.
488
489(*
490let load_code_memory = fold_lefti (fun i mem v -> WordMap.add (vect_of_int i `Sixteen) v mem) WordMap.empty
491
492let load_mem mem status = { status with code_memory = mem }
493let load l = load_mem (load_code_memory l)
494
495module StringMap = Map.Make(String);;
496module IntMap = Map.Make(struct type t = int let compare = compare end);;
497
498
499let assembly_jump addr_of =
500 function
501    `JC a1 -> `JC (addr_of a1)
502  | `JNC a1 -> `JNC (addr_of a1)
503  | `JB (a1,a2) -> `JB (a1,addr_of a2)
504  | `JNB (a1,a2) -> `JNB (a1,addr_of a2)
505  | `JBC (a1,a2) -> `JBC (a1,addr_of a2)
506  | `JZ a1 -> `JZ (addr_of a1)
507  | `JNZ a1 -> `JNZ (addr_of a1)
508  | `CJNE (a1,a2) -> `CJNE (a1,addr_of a2)
509  | `DJNZ (a1,a2) -> `DJNZ (a1,addr_of a2)
510;;
511
512let assembly (preamble,l) =
513 let datalabels,_ =
514  List.fold_left
515   (fun (datalabels,addr) (name,size) ->
516     let addr16 = vect_of_int addr `Sixteen in
517      StringMap.add name addr16 datalabels, addr+size
518   ) (StringMap.empty,0) preamble
519 in
520 let pc,labels,costs =
521  List.fold_left
522   (fun (pc,labels,costs) i ->
523     match i with
524        `Label s -> pc, StringMap.add s pc labels, costs
525      | `Cost s -> pc, labels, IntMap.add pc s costs
526      | `Mov (_,_) -> pc, labels, costs
527      | `Jmp _
528      | `Call _ -> pc + 3, labels, costs  (*CSC: very stupid: always expand to worst opcode *)
529      | `WithLabel i ->
530          let fake_addr _ = `REL (zero `Eight) in
531          let fake_jump = assembly_jump fake_addr i in
532          let i',pc',_ = fetch (load_code_memory (assembly1 fake_jump)) (vect_of_int 0 `Sixteen) in
533           assert (fake_jump = i');
534           (pc + int_of_vect pc',labels, costs)
535      | #instruction as i ->
536        let i',pc',_ = fetch (load_code_memory (assembly1 i)) (vect_of_int 0 `Sixteen) in
537         assert (i = i');
538         (pc + int_of_vect pc',labels, costs)
539   ) (0,StringMap.empty,IntMap.empty) l
540 in
541  if pc >= 65536 then
542   raise CodeTooLarge
543  else
544      List.flatten (List.map
545         (function
546            `Label _
547          | `Cost _ -> []
548          | `WithLabel i ->
549              let addr_of (`Label s) =
550               let addr = StringMap.find s labels in
551               (* NOT IMPLEMENTED YET; NEEDS SMART ALGORITHM *)
552                assert (addr < 256);
553                `REL (vect_of_int addr `Eight)
554              in
555               assembly1 (assembly_jump addr_of i)
556          | `Mov (`DPTR,s) ->
557              let addrr16 = StringMap.find s datalabels in
558               assembly1 (`MOV (`U4 (`DPTR,`DATA16 addrr16)))
559          | `Jmp s ->
560              let pc_offset = StringMap.find s labels in
561                assembly1 (`LJMP (`ADDR16 (vect_of_int pc_offset `Sixteen)))
562          | `Call s ->
563              let pc_offset = StringMap.find s labels in
564                assembly1 (`LCALL (`ADDR16 (vect_of_int pc_offset `Sixteen)))
565          | #instruction as i -> assembly1 i) l), costs
566;;
567*)
568
569ndefinition assembly: List instruction → List Byte ≝
570 fold_right … (λi,l. assembly1 i @ l) [].
Note: See TracBrowser for help on using the repository browser.