source: src/ASM/Assembly.ma @ 842

Last change on this file since 842 was 842, checked in by sacerdot, 9 years ago

Bug fixed.

File size: 31.7 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 is_relative_jump ≝
401  λi: preinstruction Identifier.
402  match i with
403  [ JC _ ⇒ True
404  | JNC _ ⇒ True
405  | JB _ _ ⇒ True
406  | JNB _ _ ⇒ True
407  | JBC _ _ ⇒ True
408  | JZ _ ⇒ True
409  | JNZ _ ⇒ True
410  | CJNE _ _ ⇒ True
411  | DJNZ _ _ ⇒ True
412  | _ ⇒ False
413  ].
414
415definition pseudo_instruction_is_relative_jump: pseudo_instruction → Prop ≝
416 λi.
417  match i with
418   [ Instruction j ⇒ is_relative_jump j
419   | _ ⇒ False ].
420
421inductive jump_length: Type[0] ≝
422  | short_jump: jump_length
423  | medium_jump: jump_length
424  | long_jump: jump_length.
425
426axiom jump_expansion_policy:
427  ∀program: pseudo_assembly_program.
428  ∀pc: Word.
429   jump_length.
430
431definition expand_relative_jump_internal:
432 (Identifier → Word) → jump_length → Identifier → Word → ([[relative]] → preinstruction [[relative]]) →
433 option (list instruction)
434 ≝
435  λlookup_labels,jmp_len.λjmp:Identifier.λpc,i.
436  match jmp_len with
437  [ short_jump ⇒
438     let lookup_address ≝ lookup_labels jmp in
439     let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in
440     let 〈upper, lower〉 ≝ split ? 8 8 result in
441     if eq_bv ? upper (zero 8) then
442      let address ≝ RELATIVE lower in
443       Some ? [ RealInstruction (i address) ]
444     else
445       None ?
446  | medium_jump ⇒ None …
447  | long_jump ⇒
448    Some ?
449    [ RealInstruction (i (RELATIVE (bitvector_of_nat ? 2)));
450      SJMP (RELATIVE (bitvector_of_nat ? 3)); (* LJMP size? *)
451      LJMP (ADDR16 (lookup_labels jmp))
452    ]
453  ].
454  @ I
455qed.
456
457definition expand_relative_jump: (Identifier → Word) → jump_length → Word → preinstruction Identifier → option (list instruction) ≝
458  λlookup_labels.
459  λjmp_len: jump_length.
460  λpc.
461  λi: preinstruction Identifier.
462  let rel_jmp ≝ RELATIVE (bitvector_of_nat ? 2) in
463  match i with
464  [ JC jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JC ?)
465  | JNC jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNC ?)
466  | JB baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JB ? baddr)
467  | JZ jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JZ ?)
468  | JNZ jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNZ ?)
469  | JBC baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JBC ? baddr)
470  | JNB baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNB ? baddr)
471  | CJNE addr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (CJNE ? addr)
472  | DJNZ addr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (DJNZ ? addr)
473  | ADD arg1 arg2 ⇒ Some ? [ ADD ? arg1 arg2 ]
474  | ADDC arg1 arg2 ⇒ Some ? [ ADDC ? arg1 arg2 ]
475  | SUBB arg1 arg2 ⇒ Some ? [ SUBB ? arg1 arg2 ]
476  | INC arg ⇒ Some ? [ INC ? arg ]
477  | DEC arg ⇒ Some ? [ DEC ? arg ]
478  | MUL arg1 arg2 ⇒ Some ? [ MUL ? arg1 arg2 ]
479  | DIV arg1 arg2 ⇒ Some ? [ DIV ? arg1 arg2 ]
480  | DA arg ⇒ Some ? [ DA ? arg ]
481  | ANL arg ⇒ Some ? [ ANL ? arg ]
482  | ORL arg ⇒ Some ? [ ORL ? arg ]
483  | XRL arg ⇒ Some ? [ XRL ? arg ]
484  | CLR arg ⇒ Some ? [ CLR ? arg ]
485  | CPL arg ⇒ Some ? [ CPL ? arg ]
486  | RL arg ⇒ Some ? [ RL ? arg ]
487  | RR arg ⇒ Some ? [ RR ? arg ]
488  | RLC arg ⇒ Some ? [ RLC ? arg ]
489  | RRC arg ⇒ Some ? [ RRC ? arg ]
490  | SWAP arg ⇒ Some ? [ SWAP ? arg ]
491  | MOV arg ⇒ Some ? [ MOV ? arg ]
492  | MOVX arg ⇒ Some ? [ MOVX ? arg ]
493  | SETB arg ⇒ Some ? [ SETB ? arg ]
494  | PUSH arg ⇒ Some ? [ PUSH ? arg ]
495  | POP arg ⇒ Some ? [ POP ? arg ]
496  | XCH arg1 arg2 ⇒ Some ? [ XCH ? arg1 arg2 ]
497  | XCHD arg1 arg2 ⇒ Some ? [ XCHD ? arg1 arg2 ]
498  | RET ⇒ Some ? [ RET ? ]
499  | RETI ⇒ Some ? [ RETI ? ]
500  | NOP ⇒ Some ? [ RealInstruction (NOP ?) ]
501  ].
502
503definition expand_pseudo_instruction: ? → ? → Word → jump_length → pseudo_instruction → option (list instruction) ≝
504  λlookup_labels.
505  λlookup_datalabels.
506  λpc.
507  λjmp_len.
508  λi.
509  match i with
510  [ Cost cost ⇒ Some ? [ ]
511  | Comment comment ⇒ Some ? [ ]
512  | Call call ⇒
513    match jmp_len with
514    [ short_jump ⇒ None ?
515    | medium_jump ⇒
516      let 〈ignore, address〉 ≝ split ? 5 11 (lookup_labels call) in
517      let 〈fst_5, rest〉 ≝ split ? 5 11 pc in
518      if eq_bv ? ignore fst_5 then
519        let address ≝ ADDR11 address in
520          Some ? ([ ACALL address ])
521      else
522        None ?
523    | long_jump ⇒
524      let address ≝ ADDR16 (lookup_labels call) in
525        Some ? [ LCALL address ]
526    ]
527  | Mov d trgt ⇒
528    let address ≝ DATA16 (lookup_datalabels trgt) in
529      Some ? [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))]
530  | Instruction instr ⇒ expand_relative_jump lookup_labels jmp_len pc instr
531  | Jmp jmp ⇒
532    match jmp_len with
533    [ short_jump ⇒
534      let lookup_address ≝ lookup_labels jmp in
535      let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in
536      let 〈upper, lower〉 ≝ split ? 8 8 result in
537      if eq_bv ? upper (zero 8) then
538        let address ≝ RELATIVE lower in
539          Some ? [ SJMP address ]
540      else
541        None ?
542    | medium_jump ⇒
543      let address ≝ lookup_labels jmp in
544      let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 address in
545      let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
546      if eq_bv ? fst_5_addr fst_5_pc then
547        let address ≝ ADDR11 rest_addr in
548          Some ? ([ AJMP address ])
549      else
550        None ?
551    | long_jump ⇒
552      let address ≝ ADDR16 (lookup_labels jmp) in
553        Some ? [ LJMP address ]
554    ]
555  ].
556  @ I
557qed.
558
559definition assembly_1_pseudoinstruction ≝
560  λprogram.
561  λpc.
562  λlookup_labels.
563  λlookup_datalabels.
564  λi.
565  let expansion ≝ jump_expansion_policy program pc in
566    match expand_pseudo_instruction lookup_labels lookup_datalabels pc expansion i with
567    [ None ⇒ None ?
568    | Some pseudos ⇒
569      let mapped ≝ map ? ? assembly1 pseudos in
570      let flattened ≝ flatten ? mapped in
571      let len ≝ length ? flattened in
572        Some ? (〈len, flattened〉)
573    ].
574
575definition construct_datalabels ≝
576  λpreamble.
577    \fst (foldl ((BitVectorTrie Identifier 16) × nat) ? (
578    λt. λpreamble.
579      let 〈datalabels, addr〉 ≝ t in
580      let 〈name, size〉 ≝ preamble in
581      let addr_16 ≝ bitvector_of_nat 16 addr in
582        〈insert ? ? name addr_16 datalabels, addr + size〉)
583          〈(Stub ? ?), 0〉 preamble).
584
585definition construct_costs ≝
586  λprogram.
587  λprogram_counter: nat.
588  λlookup_labels.
589  λlookup_datalabels.
590  λcosts: BitVectorTrie Word 16.
591  λi.
592  match i with
593  [ Cost cost ⇒
594    let program_counter_bv ≝ bitvector_of_nat ? program_counter in
595      Some ? 〈program_counter, (insert ? ? program_counter_bv cost costs)〉
596  | _ ⇒
597    let pc_bv ≝ bitvector_of_nat ? program_counter in
598    let pc_delta_assembled ≝
599      assembly_1_pseudoinstruction program pc_bv
600        lookup_labels lookup_datalabels i
601    in
602    match pc_delta_assembled with
603    [ None ⇒ None ?
604    | Some pc_delta_assembled ⇒
605      let 〈pc_delta, assembled〉 ≝ pc_delta_assembled in
606        Some ? 〈pc_delta + program_counter, costs〉       
607    ]
608  ].
609
610definition build_maps ≝
611  λinstr_list.
612  let result ≝ foldl (option ((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16)))) ?
613    (λt. λi.
614       let 〈label, i〉 ≝ i in
615       match t with
616       [ None ⇒ None ?
617       | Some t ⇒
618         let 〈labels, pc_costs〉 ≝ t in
619         let 〈program_counter, costs〉 ≝ pc_costs in
620         let labels ≝
621           match label with
622           [ None ⇒ labels
623           | Some label ⇒
624             let program_counter_bv ≝ bitvector_of_nat ? program_counter in
625               insert ? ? label program_counter_bv labels
626           ]
627         in
628           match construct_costs instr_list program_counter (λx. zero ?) (λx. zero ?) costs i with
629           [ None ⇒ None ?
630           | Some construct ⇒ Some ? 〈labels, construct〉
631           ]
632       ]) (Some ? 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉) (\snd instr_list) in
633  match result with
634  [ None ⇒ None ?
635  | Some result ⇒
636    let 〈labels, pc_costs〉 ≝ result in
637    let 〈pc, costs〉 ≝ pc_costs in
638      if gtb pc (2^16) then
639        None ?
640      else
641        Some ? 〈labels, costs〉
642  ].
643
644definition assembly: pseudo_assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
645  λp.
646    let 〈preamble, instr_list〉 ≝ p in
647    match build_maps p with
648    [ None ⇒ None ?
649    | Some maps ⇒
650      let labels ≝ \fst maps in
651      let datalabels ≝ construct_datalabels preamble in
652      match build_maps p with
653      [ None ⇒ None ?
654      | Some labels_costs ⇒
655        let 〈labels,costs〉 ≝ labels_costs in
656        let lookup_labels ≝ λx. lookup ? ? x labels (zero ?) in
657        let lookup_datalabels ≝ λx. lookup ? ? x datalabels (zero ?) in
658        let result ≝ foldr ? ? (λx. λy.
659            match y with
660            [ None ⇒ None ?
661            | Some lst ⇒
662              let 〈pc, y〉 ≝ lst in
663              let x ≝ assembly_1_pseudoinstruction p pc lookup_labels lookup_datalabels (\snd x) in
664              match x with
665              [ None ⇒ None ?
666              | Some x ⇒
667                let 〈pc_delta, program〉 ≝ x in
668                let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in
669                  Some ? 〈new_pc, (program @ y)〉
670              ]
671            ]) (Some ? 〈(zero ?), [ ]〉) instr_list
672        in
673          match result with
674          [ None ⇒ None ?
675          | Some result ⇒ Some ? (〈\snd result, costs〉)
676          ]
677      ]
678    ].
679
680definition assembly_unlabelled_program: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
681 λp. Some ? (〈foldr ? ? (λi,l. assembly1 i @ l) [ ] p, Stub …〉).
682
Note: See TracBrowser for help on using the repository browser.