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

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

Moved over to standard library.

File size: 28.9 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 O))) (S (S (S (S (S (S (S (S O)))))))) 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 O))) (S (S (S (S (S (S (S (S O)))))))) 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      [ inl addrs ⇒ match addrs with
38         [ inl 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         | inr 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      | inr 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          [ inl 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          | inr 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 O)))))))) (S (S (S (S (S (S (S (S O)))))))) 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 O)))))))) (S (S (S (S (S (S (S (S O)))))))) 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      [ inl addrs ⇒
207         match addrs with
208          [ inl addrs ⇒
209             match addrs with
210              [ inl addrs ⇒
211                 match addrs with
212                  [ inl addrs ⇒
213                     match addrs with
214                      [ inl 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                      | inr 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                  | inr 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              | inr 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 O)))))))) (S (S (S (S (S (S (S (S O)))))))) w in
252                      [ ([[true;false;false;true;false;false;false;false]]); b1; b2]
253                  | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
254          | inr 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      | inr 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      [ inl 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      | inr 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      [ inl addrs ⇒
294         match addrs with
295          [ inl 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          | inr 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      | inr 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      [ inl 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      | inr 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 8) 8 → String → addressing_mode ≝
422    λmap: BitVectorTrie (BitVector 8) 8.
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 leb address_bv 256 then
427          RELATIVE address
428        else
429          ?.
430      nelim not_implemented.
431nqed.
432
433ndefinition assembly: assembly_program → option (list Byte × (BitVectorTrie String 16)) ≝
434  λp.
435    let 〈preamble, instr_list〉 ≝ p in
436    let 〈datalabels, ignore〉 ≝
437      foldl ((BitVectorTrie (BitVector 16) 16) × nat) ? (
438        λt. λpreamble.
439          let 〈datalabels, addr〉 ≝ t in
440          let 〈name, size〉 ≝ preamble in
441          let addr_sixteen ≝ bitvector_of_nat 16 addr in
442            〈insert ? ? (bitvector_of_string ? name) addr_sixteen datalabels, addr + size〉)
443              〈(Stub ? ?), O〉 preamble in
444    let 〈pc_labels, costs〉 ≝
445      foldl ((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 16) 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 8 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 + 3, labels〉, costs〉
464              | Call call ⇒
465                  〈〈program_counter + 3, labels〉, costs〉
466              | Mov dptr trgt ⇒ t
467              | WithLabel jmp ⇒
468                let fake_addr ≝ RELATIVE (zero 8) 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 16) in
472                let 〈instr', program_counter'〉 ≝ instr_pc' in
473                let program_counter_n' ≝ nat_of_bitvector 16 program_counter' in
474                  〈〈program_counter + program_counter_n', labels〉, costs〉
475              ]
476          ) 〈〈O, (Stub ? ?)〉, (Stub ? ?)〉 instr_list in
477    let 〈program_counter, labels〉 ≝ pc_labels in
478      if gtb program_counter (2^16) then
479        None ?
480      else
481        let flat_list ≝
482          flatten ? (
483            map ? ? (
484              λi: labelled_instruction.
485                match i with
486                  [ Cost cost ⇒ [ ]
487                  | Label label ⇒ [ ]
488                  | Call call ⇒
489                    let pc_offset ≝ lookup ? ? (bitvector_of_string ? call) labels (zero ?) in
490                    let pc_offset_pad ≝ (zero 8) @@ pc_offset in
491                    let address ≝ ADDR16 pc_offset_pad in
492                      assembly1 (LCALL ? address)
493                  | Mov d trgt ⇒
494                    let pc_offset ≝ lookup ? ? (bitvector_of_string ? trgt) datalabels (zero ?) in
495                    let address ≝ DATA16 pc_offset in
496                      assembly1 (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))
497                  | Instruction instr ⇒ assembly1 instr
498                  | Jmp jmp ⇒
499                    let pc_offset ≝ lookup ? ? (bitvector_of_string ? jmp) labels (zero ?) in
500                    let pc_offset_pad ≝ (zero 8) @@ pc_offset in
501                    let address ≝ ADDR16 pc_offset_pad in
502                      assembly1 (LJMP ? address)
503                  | WithLabel jmp ⇒
504                    assembly1 (assembly_jump jmp (address_of labels))
505                  ]
506            ) instr_list
507          ) in
508        Some (list ? × (BitVectorTrie ? ?)) 〈flat_list, costs〉.
509  ##[##2,3,4,5,6: nnormalize; @;
510  ##| nwhd in ⊢ (? (? ? ? %));
511      ncases (leb (nat_of_bitvector 8 ?) 256)
512        [ nnormalize; @;
513      ##| nnormalize;
514          nelim not_implemented;
515      ##]
516  ##]
517nqed.
518
519ndefinition assembly_unlabelled_program: list instruction → option (list Byte × (BitVectorTrie String 16)) ≝
520 λp.Some ? (〈foldr ?? (λi,l. assembly1 i @ l) [ ] p, Stub …〉).
Note: See TracBrowser for help on using the repository browser.