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

Last change on this file since 425 was 425, checked in by mulligan, 10 years ago

Removed Map.ma as no longer needed. Everything else seems to build apart from DoTest?.ma (are we including this in final distr?)

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