source: src/ASM/Assembly.ma @ 837

Last change on this file since 837 was 837, checked in by mulligan, 8 years ago

changes complete

File size: 31.2 KB
Line 
1include "ASM/ASM.ma".
2include "ASM/BitVectorTrie.ma".
3include "ASM/Arithmetic.ma".
4include "ASM/Fetch.ma".
5include "ASM/Status.ma".
6
7definition assembly_preinstruction ≝
8  λA: Type[0].
9  λaddr_of: A → Byte. (* relative *)
10  λpre: preinstruction A.
11  match pre with
12  [ ADD addr1 addr2 ⇒
13     match addr2 return λx. bool_to_Prop (is_in ? [[registr;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 ? [[registr;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  | ANL addrs ⇒
27     match addrs with
28      [ inl addrs ⇒ match addrs with
29         [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
30           match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
31            [ REGISTER r ⇒ λ_.[ ([[false;true;false;true;true]]) @@ r ]
32            | DIRECT b1 ⇒ λ_.[ ([[false;true;false;true;false;true;false;true]]); b1 ]
33            | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;true;false;true;true;i1]]) ]
34            | DATA b1 ⇒ λ_. [ ([[false;true;false;true;false;true;false;false]]) ; b1 ]
35            | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
36         | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
37            let b1 ≝
38             match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
39              [ DIRECT b1 ⇒ λ_.b1
40              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
41            match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
42             [ ACC_A ⇒ λ_.[ ([[false;true;false;true;false;false;true;false]]) ; b1 ]
43             | DATA b2 ⇒ λ_. [ ([[false;true;false;true;false;false;true;true]]) ; b1 ; b2 ]
44             | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
45         ]
46      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
47         match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
48          [ BIT_ADDR b1 ⇒ λ_.[ ([[true;false;false;false;false;false;true;false]]) ; b1 ]
49          | N_BIT_ADDR b1 ⇒ λ_. [ ([[true;false;true;true;false;false;false;false]]) ; b1 ]
50          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
51  | CLR addr ⇒
52     match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with
53      [ ACC_A ⇒ λ_.
54         [ ([[true; true; true; false; false; true; false; false]]) ]
55      | CARRY ⇒ λ_.
56         [ ([[true; true; false; false; false; false; true; true]]) ]
57      | BIT_ADDR b1 ⇒ λ_.
58         [ ([[true; true; false; false; false; false; true; false]]) ; b1 ]
59      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
60  | CPL 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; true; false; true; false; false]]) ]
64      | CARRY ⇒ λ_.
65         [ ([[true; false; true; true; false; false; true; true]]) ]
66      | BIT_ADDR b1 ⇒ λ_.
67         [ ([[true; false; true; true; false; false; true; false]]) ; b1 ]
68      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
69  | DA addr ⇒
70     [ ([[true; true; false; true; false; true; false; false]]) ]
71  | DEC addr ⇒
72     match addr return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect]] x) → ? with
73      [ ACC_A ⇒ λ_.
74         [ ([[false; false; false; true; false; true; false; false]]) ]
75      | REGISTER r ⇒ λ_.
76         [ ([[false; false; false; true; true]]) @@ r ]
77      | DIRECT b1 ⇒ λ_.
78         [ ([[false; false; false; true; false; true; false; true]]); b1 ]
79      | INDIRECT i1 ⇒ λ_.
80         [ ([[false; false; false; true; false; true; true; i1]]) ]
81      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
82      | DJNZ addr1 addr2 ⇒
83         let b2 ≝ addr_of addr2 in
84         match addr1 return λx. bool_to_Prop (is_in ? [[registr;direct]] x) → ? with
85          [ REGISTER r ⇒ λ_.
86             [ ([[true; true; false; true; true]]) @@ r ; b2 ]
87          | DIRECT b1 ⇒ λ_.
88             [ ([[true; true; false; true; false; true; false; true]]); b1; b2 ]
89          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
90      | JC addr ⇒
91        let b1 ≝ addr_of addr in
92          [ ([[false; true; false; false; false; false; false; false]]); b1 ]
93      | JNC addr ⇒
94         let b1 ≝ addr_of addr in
95           [ ([[false; true; false; true; false; false; false; false]]); b1 ]
96      | JZ addr ⇒
97         let b1 ≝ addr_of addr in
98           [ ([[false; true; true; false; false; false; false; false]]); b1 ]
99      | JNZ addr ⇒
100         let b1 ≝ addr_of addr in
101           [ ([[false; true; true; true; false; false; false; false]]); b1 ]
102      | JB addr1 addr2 ⇒
103         let b2 ≝ addr_of addr2 in
104         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
105          [ BIT_ADDR b1 ⇒ λ_.
106             [ ([[false; false; true; false; false; false; false; false]]); b1; b2 ]
107          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
108      | JNB addr1 addr2 ⇒
109         let b2 ≝ addr_of addr2 in
110         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
111          [ BIT_ADDR b1 ⇒ λ_.
112             [ ([[false; false; true; true; false; false; false; false]]); b1; b2 ]
113          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
114      | JBC addr1 addr2 ⇒
115         let b2 ≝ addr_of addr2 in
116         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
117          [ BIT_ADDR b1 ⇒ λ_.
118             [ ([[false; false; false; true; false; false; false; false]]); b1; b2 ]
119          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
120      | CJNE addrs addr3 ⇒
121         let b3 ≝ addr_of addr3 in
122         match addrs with
123          [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
124             match addr2 return λx. bool_to_Prop (is_in ? [[direct;data]] x) → ? with
125              [ DIRECT b1 ⇒ λ_.
126                 [ ([[true; false; true; true; false; true; false; true]]); b1; b3 ]
127              | DATA b1 ⇒ λ_.
128                 [ ([[true; false; true; true; false; true; false; false]]); b1; b3 ]
129              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
130          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
131             let b2 ≝
132              match addr2 return λx. bool_to_Prop (is_in ? [[data]] x) → ? with
133               [ DATA b2 ⇒ λ_. b2
134               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
135             match addr1 return λx. bool_to_Prop (is_in ? [[registr;indirect]] x) → list Byte with
136              [ REGISTER r ⇒ λ_.
137                 [ ([[true; false; true; true; true]]) @@ r; b2; b3 ]
138              | INDIRECT i1 ⇒ λ_.
139                 [ ([[true; false; true; true; false; true; true; i1]]); b2; b3 ]
140              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
141         ]
142  | DIV addr1 addr2 ⇒
143     [ ([[true;false;false;false;false;true;false;false]]) ]
144  | INC addr ⇒
145     match addr return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect;dptr]] x) → ? with
146      [ ACC_A ⇒ λ_.
147         [ ([[false;false;false;false;false;true;false;false]]) ]         
148      | REGISTER r ⇒ λ_.
149         [ ([[false;false;false;false;true]]) @@ r ]
150      | DIRECT b1 ⇒ λ_.
151         [ ([[false; false; false; false; false; true; false; true]]); b1 ]
152      | INDIRECT i1 ⇒ λ_.
153        [ ([[false; false; false; false; false; true; true; i1]]) ]
154      | DPTR ⇒ λ_.
155        [ ([[true;false;true;false;false;false;true;true]]) ]
156      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
157  | MOV addrs ⇒
158     match addrs with
159      [ inl addrs ⇒
160         match addrs with
161          [ inl addrs ⇒
162             match addrs with
163              [ inl addrs ⇒
164                 match addrs with
165                  [ inl addrs ⇒
166                     match addrs with
167                      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
168                         match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
169                          [ REGISTER r ⇒ λ_.[ ([[true;true;true;false;true]]) @@ r ]
170                          | DIRECT b1 ⇒ λ_.[ ([[true;true;true;false;false;true;false;true]]); b1 ]
171                          | INDIRECT i1 ⇒ λ_. [ ([[true;true;true;false;false;true;true;i1]]) ]
172                          | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;false;false]]) ; b1 ]
173                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
174                      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
175                         match addr1 return λx. bool_to_Prop (is_in ? [[registr;indirect]] x) → ? with
176                          [ REGISTER r ⇒ λ_.
177                             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with
178                              [ ACC_A ⇒ λ_.[ ([[true;true;true;true;true]]) @@ r ]
179                              | DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;true]]) @@ r; b1 ]
180                              | DATA b1 ⇒ λ_. [ ([[false;true;true;true;true]]) @@ r; b1 ]
181                              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
182                          | INDIRECT i1 ⇒ λ_.
183                             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with
184                              [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;true;i1]]) ]
185                              | DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;false;true;true;i1]]); b1 ]
186                              | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;true;i1]]) ; b1 ]
187                              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
188                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
189                  | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
190                     let b1 ≝
191                      match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
192                       [ DIRECT b1 ⇒ λ_. b1
193                       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
194                     match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect;data]] x) → ? with
195                      [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;false;true]]); b1]
196                      | REGISTER r ⇒ λ_.[ ([[true;false;false;false;true]]) @@ r; b1 ]
197                      | DIRECT b2 ⇒ λ_.[ ([[true;false;false;false;false;true;false;true]]); b1; b2 ]
198                      | INDIRECT i1 ⇒ λ_. [ ([[true;false;false;false;false;true;true;i1]]); b1 ]
199                      | DATA b2 ⇒ λ_. [ ([[false;true;true;true;false;true;false;true]]); b1; b2 ]
200                      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
201              | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
202                 match addr2 return λx. bool_to_Prop (is_in ? [[data16]] x) → ? with
203                  [ DATA16 w ⇒ λ_.
204                     let 〈b1,b2〉 ≝ split ? 8 8 w in
205                      [ ([[true;false;false;true;false;false;false;false]]); b1; b2]
206                  | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
207          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
208             match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
209              [ BIT_ADDR b1 ⇒ λ_.
210                 [ ([[true;false;true;false;false;false;true;false]]); b1 ]
211              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
212      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
213         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
214          [ BIT_ADDR b1 ⇒ λ_.
215             [ ([[true;false;false;true;false;false;true;false]]); b1 ]
216          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
217  | MOVX addrs ⇒
218     match addrs with
219      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
220         match addr2 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
221          [ EXT_INDIRECT i1 ⇒ λ_.
222             [ ([[true;true;true;false;false;false;true;i1]]) ]
223          | EXT_INDIRECT_DPTR ⇒ λ_.
224             [ ([[true;true;true;false;false;false;false;false]]) ]
225          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
226      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
227         match addr1 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
228          [ EXT_INDIRECT i1 ⇒ λ_.
229             [ ([[true;true;true;true;false;false;true;i1]]) ]
230          | EXT_INDIRECT_DPTR ⇒ λ_.
231             [ ([[true;true;true;true;false;false;false;false]]) ]
232          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
233  | MUL addr1 addr2 ⇒
234     [ ([[true;false;true;false;false;true;false;false]]) ]
235  | NOP ⇒
236     [ ([[false;false;false;false;false;false;false;false]]) ]
237  | ORL addrs ⇒
238     match addrs with
239      [ inl addrs ⇒
240         match addrs with
241          [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
242             match addr2 return λx. bool_to_Prop (is_in ? [[registr;data;direct;indirect]] x) → ? with
243             [ REGISTER r ⇒ λ_.[ ([[false;true;false;false;true]]) @@ r ]
244             | DIRECT b1 ⇒ λ_.[ ([[false;true;false;false;false;true;false;true]]); b1 ]
245             | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;false;false;true;true;i1]]) ]
246             | DATA b1 ⇒ λ_. [ ([[false;true;false;false;false;true;false;false]]) ; b1 ]
247             | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
248          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
249            let b1 ≝
250              match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
251               [ DIRECT b1 ⇒ λ_. b1
252               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
253             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
254              [ ACC_A ⇒ λ_.
255                 [ ([[false;true;false;false;false;false;true;false]]); b1 ]
256              | DATA b2 ⇒ λ_.
257                 [ ([[false;true;false;false;false;false;true;true]]); b1; b2 ]
258              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
259      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in     
260         match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
261          [ BIT_ADDR b1 ⇒ λ_.
262             [ ([[false;true;true;true;false;false;true;false]]); b1 ]
263          | N_BIT_ADDR b1 ⇒ λ_.
264             [ ([[true;false;true;false;false;false;false;false]]); b1 ]
265          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
266  | POP addr ⇒
267     match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
268      [ DIRECT b1 ⇒ λ_.
269         [ ([[true;true;false;true;false;false;false;false]]) ; b1 ]
270      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
271  | PUSH addr ⇒
272     match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
273      [ DIRECT b1 ⇒ λ_.
274         [ ([[true;true;false;false;false;false;false;false]]) ; b1 ]
275      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
276  | RET ⇒
277     [ ([[false;false;true;false;false;false;true;false]]) ]
278  | RETI ⇒
279     [ ([[false;false;true;true;false;false;true;false]]) ]
280  | RL addr ⇒
281     [ ([[false;false;true;false;false;false;true;true]]) ]
282  | RLC addr ⇒
283     [ ([[false;false;true;true;false;false;true;true]]) ]
284  | RR addr ⇒
285     [ ([[false;false;false;false;false;false;true;true]]) ]
286  | RRC addr ⇒
287     [ ([[false;false;false;true;false;false;true;true]]) ]
288  | SETB addr ⇒     
289     match addr return λx. bool_to_Prop (is_in ? [[carry;bit_addr]] x) → ? with
290      [ CARRY ⇒ λ_.
291         [ ([[true;true;false;true;false;false;true;true]]) ]
292      | BIT_ADDR b1 ⇒ λ_.
293         [ ([[true;true;false;true;false;false;true;false]]); b1 ]
294      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
295  | SUBB addr1 addr2 ⇒
296     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
297      [ REGISTER r ⇒ λ_.
298         [ ([[true;false;false;true;true]]) @@ r ]
299      | DIRECT b1 ⇒ λ_.
300         [ ([[true;false;false;true;false;true;false;true]]); b1]
301      | INDIRECT i1 ⇒ λ_.
302         [ ([[true;false;false;true;false;true;true;i1]]) ]
303      | DATA b1 ⇒ λ_.
304         [ ([[true;false;false;true;false;true;false;false]]); b1]
305      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
306  | SWAP addr ⇒
307     [ ([[true;true;false;false;false;true;false;false]]) ]
308  | XCH addr1 addr2 ⇒
309     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect]] x) → ? with
310      [ REGISTER r ⇒ λ_.
311         [ ([[true;true;false;false;true]]) @@ r ]
312      | DIRECT b1 ⇒ λ_.
313         [ ([[true;true;false;false;false;true;false;true]]); b1]
314      | INDIRECT i1 ⇒ λ_.
315         [ ([[true;true;false;false;false;true;true;i1]]) ]
316      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
317  | XCHD addr1 addr2 ⇒
318     match addr2 return λx. bool_to_Prop (is_in ? [[indirect]] x) → ? with
319      [ INDIRECT i1 ⇒ λ_.
320         [ ([[true;true;false;true;false;true;true;i1]]) ]
321      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
322  | XRL addrs ⇒
323     match addrs with
324      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
325         match addr2 return λx. bool_to_Prop (is_in ? [[data;registr;direct;indirect]] x) → ? with
326          [ REGISTER r ⇒ λ_.
327             [ ([[false;true;true;false;true]]) @@ r ]
328          | DIRECT b1 ⇒ λ_.
329             [ ([[false;true;true;false;false;true;false;true]]); b1]
330          | INDIRECT i1 ⇒ λ_.
331             [ ([[false;true;true;false;false;true;true;i1]]) ]
332          | DATA b1 ⇒ λ_.
333             [ ([[false;true;true;false;false;true;false;false]]); b1]
334          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
335      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
336         let b1 ≝
337          match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
338           [ DIRECT b1 ⇒ λ_. b1
339           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
340         match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
341          [ ACC_A ⇒ λ_.
342             [ ([[false;true;true;false;false;false;true;false]]); b1 ]         
343          | DATA b2 ⇒ λ_.
344             [ ([[false;true;true;false;false;false;true;true]]); b1; b2 ]
345          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
346       ].
347
348definition assembly1 ≝
349 λi: instruction.
350 match i with
351  [ ACALL addr ⇒
352     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
353      [ ADDR11 w ⇒ λ_.
354         let 〈v1,v2〉 ≝ split ? 3 8 w in
355          [ (v1 @@ [[true; false; false; false; true]]) ; v2 ]
356      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
357  | AJMP addr ⇒
358     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
359      [ ADDR11 w ⇒ λ_.
360         let 〈v1,v2〉 ≝ split ?  3 8 w in
361          [ (v1 @@ [[false; false; false; false; true]]) ; v2 ]
362      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
363  | JMP adptr ⇒
364     [ ([[false;true;true;true;false;false;true;true]]) ]
365  | LCALL addr ⇒
366     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
367      [ ADDR16 w ⇒ λ_.
368         let 〈b1,b2〉 ≝ split ? 8 8 w in
369          [ ([[false;false;false;true;false;false;true;false]]); b1; b2 ]         
370      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
371  | LJMP addr ⇒
372     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
373      [ ADDR16 w ⇒ λ_.
374         let 〈b1,b2〉 ≝ split ? 8 8 w in
375          [ ([[false;false;false;false;false;false;true;false]]); b1; b2 ]         
376      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
377  | MOVC addr1 addr2 ⇒
378     match addr2 return λx. bool_to_Prop (is_in ? [[acc_dptr;acc_pc]] x) → ? with
379      [ ACC_DPTR ⇒ λ_.
380         [ ([[true;false;false;true;false;false;true;true]]) ]
381      | ACC_PC ⇒ λ_.
382         [ ([[true;false;false;false;false;false;true;true]]) ]
383      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
384  | SJMP addr ⇒
385     match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
386      [ RELATIVE b1 ⇒ λ_.
387         [ ([[true;false;false;false;false;false;false;false]]); b1 ]
388      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
389  | RealInstruction instr ⇒
390    assembly_preinstruction [[ relative ]]
391      (λx.
392        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with
393        [ RELATIVE r ⇒ λ_. r
394        | _ ⇒ λabsd. ⊥
395        ] (subaddressing_modein … x)) instr
396  ].
397  cases absd
398qed.
399
400definition address_of: BitVectorTrie Word 16 → Identifier → Byte ≝
401    λmap.
402    λid: Identifier.
403      let address ≝ lookup … id map (zero ?) in
404      let 〈high, low〉 ≝ split ? 8 8 address in
405      if eq_bv ? high (zero ?) then
406        low
407      else
408        ?.
409      elim not_implemented.
410qed.
411
412inductive jump_length: Type[0] ≝
413  | short_jump: jump_length
414  | medium_jump: jump_length
415  | long_jump: jump_length.
416
417axiom jump_expansion_policy:
418  ∀program: pseudo_assembly_program.
419  ∀pc: Word.
420    jump_length.
421
422definition expand_relative_jump_internal ≝
423  λjmp_len.
424  λi.
425  match jmp_len with
426  [ short_jump ⇒ Some ? [ i ]
427  | medium_jump ⇒ None ?
428  | long_jump ⇒
429    Some ? [ RealInstruction i;
430      SJMP (RELATIVE (bitvector_of_nat ? 3)); (* LJMP size? *)
431      LJMP (ADDR16 (bitvector_of_nat ? 0)) (* fill in *)
432    ]
433  ].
434  @ I
435qed.
436
437definition expand_relative_jump: jump_length → preinstruction Identifier → option (list instruction) ≝
438  λjmp_len: jump_length.
439  λi: preinstruction Identifier.
440  let rel_jmp ≝ RELATIVE (bitvector_of_nat ? 2) in
441  match i with
442  [ JC jmp ⇒ expand_relative_jump_internal jmp_len (JC ? rel_jmp)
443  | JNC jmp ⇒ expand_relative_jump_internal jmp_len (JNC ? rel_jmp)
444  | JB baddr jmp ⇒ expand_relative_jump_internal jmp_len (JB ? baddr rel_jmp)
445  | JZ jmp ⇒ expand_relative_jump_internal jmp_len (JZ ? rel_jmp)
446  | JNZ jmp ⇒ expand_relative_jump_internal jmp_len (JNZ ? rel_jmp)
447  | JBC baddr jmp ⇒ expand_relative_jump_internal jmp_len (JBC ? baddr rel_jmp)
448  | JNB baddr jmp ⇒ expand_relative_jump_internal jmp_len (JNB ? baddr rel_jmp)
449  | CJNE addr jmp ⇒ expand_relative_jump_internal jmp_len (CJNE ? addr rel_jmp)
450  | DJNZ addr jmp ⇒ expand_relative_jump_internal jmp_len (DJNZ ? addr rel_jmp)
451  | ADD arg1 arg2 ⇒ Some ? [ ADD ? arg1 arg2 ]
452  | ADDC arg1 arg2 ⇒ Some ? [ ADDC ? arg1 arg2 ]
453  | SUBB arg1 arg2 ⇒ Some ? [ SUBB ? arg1 arg2 ]
454  | INC arg ⇒ Some ? [ INC ? arg ]
455  | DEC arg ⇒ Some ? [ DEC ? arg ]
456  | MUL arg1 arg2 ⇒ Some ? [ MUL ? arg1 arg2 ]
457  | DIV arg1 arg2 ⇒ Some ? [ DIV ? arg1 arg2 ]
458  | DA arg ⇒ Some ? [ DA ? arg ]
459  | ANL arg ⇒ Some ? [ ANL ? arg ]
460  | ORL arg ⇒ Some ? [ ORL ? arg ]
461  | XRL arg ⇒ Some ? [ XRL ? arg ]
462  | CLR arg ⇒ Some ? [ CLR ? arg ]
463  | CPL arg ⇒ Some ? [ CPL ? arg ]
464  | RL arg ⇒ Some ? [ RL ? arg ]
465  | RR arg ⇒ Some ? [ RR ? arg ]
466  | RLC arg ⇒ Some ? [ RLC ? arg ]
467  | RRC arg ⇒ Some ? [ RRC ? arg ]
468  | SWAP arg ⇒ Some ? [ SWAP ? arg ]
469  | MOV arg ⇒ Some ? [ MOV ? arg ]
470  | MOVX arg ⇒ Some ? [ MOVX ? arg ]
471  | SETB arg ⇒ Some ? [ SETB ? arg ]
472  | PUSH arg ⇒ Some ? [ PUSH ? arg ]
473  | POP arg ⇒ Some ? [ POP ? arg ]
474  | XCH arg1 arg2 ⇒ Some ? [ XCH ? arg1 arg2 ]
475  | XCHD arg1 arg2 ⇒ Some ? [ XCHD ? arg1 arg2 ]
476  | RET ⇒ Some ? [ RET ? ]
477  | RETI ⇒ Some ? [ RETI ? ]
478  | NOP ⇒ Some ? [ RealInstruction (NOP ?) ]
479  ].
480  @ I
481qed.
482
483definition expand_pseudo_instruction: ? → ? → Word → jump_length → pseudo_instruction → option (list instruction) ≝
484  λlookup_labels.
485  λlookup_datalabels.
486  λpc.
487  λjmp_len.
488  λi.
489  match i with
490  [ Cost cost ⇒ Some ? [ ]
491  | Comment comment ⇒ Some ? [ ]
492  | Call call ⇒
493    match jmp_len with
494    [ short_jump ⇒ None ?
495    | medium_jump ⇒
496      let 〈ignore, address〉 ≝ split ? 5 11 (lookup_labels call) in
497      let 〈fst_5, rest〉 ≝ split ? 5 11 pc in
498      if eq_bv ? ignore fst_5 then
499        let address ≝ ADDR11 address in
500          Some ? ([ ACALL address ])
501      else
502        None ?
503    | long_jump ⇒
504      let address ≝ ADDR16 (lookup_labels call) in
505        Some ? [ LCALL address ]
506    ]
507  | Mov d trgt ⇒
508    let address ≝ DATA16 (lookup_datalabels trgt) in
509      Some ? [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))]
510  | Instruction instr ⇒ expand_relative_jump jmp_len instr
511  | Jmp jmp ⇒
512    match jmp_len with
513    [ short_jump ⇒
514      let lookup_address ≝ lookup_labels jmp in
515      let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in
516      let 〈upper, lower〉 ≝ split ? 8 8 result in
517      if eq_bv ? upper (zero 8) then
518        let address ≝ RELATIVE lower in
519          Some ? [ SJMP address ]
520      else
521        None ?
522    | medium_jump ⇒
523      let address ≝ lookup_labels jmp in
524      let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 address in
525      let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
526      if eq_bv ? fst_5_addr fst_5_pc then
527        let address ≝ ADDR11 rest_addr in
528          Some ? ([ AJMP address ])
529      else
530        None ?
531    | long_jump ⇒
532      let address ≝ ADDR16 (lookup_labels jmp) in
533        Some ? [ LJMP address ]
534    ]
535  ].
536  @ I
537qed.
538
539definition assembly_1_pseudoinstruction ≝
540  λprogram.
541  λpc.
542  λlookup_labels.
543  λlookup_datalabels.
544  λi.
545  let expansion ≝ jump_expansion_policy program pc in
546    match expand_pseudo_instruction lookup_labels lookup_datalabels pc expansion i with
547    [ None ⇒ None ?
548    | Some pseudos ⇒
549      let mapped ≝ map ? ? assembly1 pseudos in
550      let flattened ≝ flatten ? mapped in
551      let len ≝ length ? flattened in
552        Some ? (〈len, flattened〉)
553    ].
554
555definition construct_datalabels ≝
556  λpreamble.
557    \fst (foldl ((BitVectorTrie Identifier 16) × nat) ? (
558    λt. λpreamble.
559      let 〈datalabels, addr〉 ≝ t in
560      let 〈name, size〉 ≝ preamble in
561      let addr_16 ≝ bitvector_of_nat 16 addr in
562        〈insert ? ? name addr_16 datalabels, addr + size〉)
563          〈(Stub ? ?), 0〉 preamble).
564
565definition is_jump ≝
566  λi: preinstruction Identifier.
567  match i with
568  [ JC _ ⇒ true
569  | JNC _ ⇒ true
570  | JB _ _ ⇒ true
571  | JNB _ _ ⇒ true
572  | JBC _ _ ⇒ true
573  | JZ _ ⇒ true
574  | JNZ _ ⇒ true
575  | CJNE _ _ ⇒ true
576  | DJNZ _ _ ⇒ true
577  | _ ⇒ false
578  ].
579
580definition construct_costs ≝
581  λprogram.
582  λprogram_counter: nat.
583  λlookup_labels.
584  λlookup_datalabels.
585  λcosts: BitVectorTrie Word 16.
586  λi.
587  match i with
588  [ Comment comment ⇒ Some ? 〈program_counter, costs〉
589  | Cost cost ⇒
590    let program_counter_bv ≝ bitvector_of_nat ? program_counter in
591      Some ? 〈program_counter, (insert ? ? program_counter_bv cost costs)〉
592  | _ ⇒
593    let pc_bv ≝ bitvector_of_nat ? program_counter in
594    let pc_delta_assembled ≝
595      assembly_1_pseudoinstruction program pc_bv
596        lookup_labels lookup_datalabels i
597    in
598    match pc_delta_assembled with
599    [ None ⇒ None ?
600    | Some pc_delta_assembled ⇒
601      let 〈pc_delta, assembled〉 ≝ pc_delta_assembled in
602        Some ? 〈pc_delta + program_counter, costs〉       
603    ]
604  ].
605
606definition build_maps ≝
607  λinstr_list.
608  let result ≝ foldl (option ((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16)))) ?
609    (λt. λi.
610       let 〈label, i〉 ≝ i in
611       match t with
612       [ None ⇒ None ?
613       | Some t ⇒
614         let 〈labels, pc_costs〉 ≝ t in
615         let 〈program_counter, costs〉 ≝ pc_costs in
616         let labels ≝
617           match label with
618           [ None ⇒ labels
619           | Some label ⇒
620             let program_counter_bv ≝ bitvector_of_nat ? program_counter in
621               insert ? ? label program_counter_bv labels
622           ]
623         in
624           match construct_costs instr_list program_counter (λx. zero ?) (λx. zero ?) costs i with
625           [ None ⇒ None ?
626           | Some construct ⇒ Some ? 〈labels, construct〉
627           ]
628       ]) (Some ? 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉) (\snd instr_list) in
629  match result with
630  [ None ⇒ None ?
631  | Some result ⇒
632    let 〈labels, pc_costs〉 ≝ result in
633    let 〈pc, costs〉 ≝ pc_costs in
634      if gtb pc (2^16) then
635        None ?
636      else
637        Some ? 〈labels, costs〉
638  ].
639
640definition assembly: pseudo_assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
641  λp.
642    let 〈preamble, instr_list〉 ≝ p in
643    match build_maps p with
644    [ None ⇒ None ?
645    | Some maps ⇒
646      let labels ≝ \fst maps in
647      let datalabels ≝ construct_datalabels preamble in
648      match build_maps p with
649      [ None ⇒ None ?
650      | Some labels_costs ⇒
651        let 〈labels,costs〉 ≝ labels_costs in
652        let lookup_labels ≝ λx. lookup ? ? x labels (zero ?) in
653        let lookup_datalabels ≝ λx. lookup ? ? x datalabels (zero ?) in
654        let result ≝ foldr ? ? (λx. λy.
655            match y with
656            [ None ⇒ None ?
657            | Some lst ⇒
658              let 〈pc, y〉 ≝ lst in
659              let x ≝ assembly_1_pseudoinstruction p pc lookup_labels lookup_datalabels (\snd x) in
660              match x with
661              [ None ⇒ None ?
662              | Some x ⇒
663                let 〈pc_delta, program〉 ≝ x in
664                let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in
665                  Some ? 〈new_pc, (program @ y)〉
666              ]
667            ]) (Some ? 〈(zero ?), [ ]〉) instr_list
668        in
669          match result with
670          [ None ⇒ None ?
671          | Some result ⇒ Some ? (〈\snd result, costs〉)
672          ]
673      ]
674    ].
675
676definition assembly_unlabelled_program: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
677 λp. Some ? (〈foldr ? ? (λi,l. assembly1 i @ l) [ ] p, Stub …〉).
678
Note: See TracBrowser for help on using the repository browser.