source: src/ASM/Assembly.ma @ 907

Last change on this file since 907 was 907, checked in by boender, 9 years ago
  • added quadruples to Util
  • start of implementation of new jump expansion policy
File size: 35.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 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
426definition jump_expansion_policy ≝ BitVectorTrie jump_length 16.
427
428definition find_right_call: Word → Word → nat × (option jump_length) ≝
429 (* medium call: 11 bits, only in "current segment" *)
430 (* can this be done more efficiently with bit vector arithmetic? *)
431 λpc.λaddress.
432  let 〈p1, p2〉 ≝ split ? 5 11 address in
433  let 〈a1, a2〉 ≝ split ? 5 11 pc in
434   if eq_bv ? p1 a1 then (* we're in the same segment *)
435    〈2, Some ? medium_jump〉
436   else
437    〈3, Some ? long_jump〉.
438
439definition distance ≝
440 λx.λy.if gtb x y then x - y else y - x.
441 
442definition find_right_jump: Word → Word → nat × (option jump_length) ≝
443 (* short jump: 8 bits signed *)
444 (* medium jump: 11 bits, forward only *)
445 λpc.λaddress.
446  let pn ≝ nat_of_bitvector ? pc in
447  let pa ≝ nat_of_bitvector ? address in
448   if ltb (distance pn pa) 512 then
449    〈2, Some ? short_jump〉
450   else
451    find_right_call pc address.
452
453definition find_right_relative_jump: Word → (BitVectorTrie Word 16) →
454 Identifier → nat × (option jump_length) ≝
455 λpc.λlabels.λjmp.
456 match lookup_opt ? ? jmp labels with
457 [ None ⇒ 〈2, Some ? short_jump〉
458 | Some a ⇒ find_right_jump pc a ].
459 
460definition jep_relative: Word → (BitVectorTrie Word 16) → preinstruction Identifier → ? ≝
461 λpc.λlabels.λi.
462  match i with
463  [ JC jmp ⇒ find_right_relative_jump pc labels jmp
464  | JNC jmp ⇒ find_right_relative_jump pc labels jmp
465  | JB baddr jmp ⇒ find_right_relative_jump pc labels jmp
466  | JZ jmp ⇒ find_right_relative_jump pc labels jmp
467  | JNZ jmp ⇒ find_right_relative_jump pc labels jmp
468  | JBC baddr jmp ⇒ find_right_relative_jump pc labels jmp
469  | JNB baddr jmp ⇒ find_right_relative_jump pc labels jmp
470  | CJNE addr jmp ⇒ find_right_relative_jump pc labels jmp
471  | DJNZ addr jmp ⇒ find_right_relative_jump pc labels jmp
472  | _ ⇒ 〈length ? (assembly_preinstruction ? (λx.zero ?) i), None …〉 ].
473 
474definition jump_expansion_policy_internal: pseudo_assembly_program →
475 (BitVectorTrie Word 16) → jump_expansion_policy →
476 ((BitVectorTrie Word 16) × jump_expansion_policy × bool)≝
477 λprogram.λlabels.λpolicy.
478   let 〈pc, new_labels, new_policy, changed〉 ≝
479   foldl ? ? (λacc.λi:labelled_instruction.
480    let 〈label, instr〉 ≝ i in
481    let 〈pc,labels,policy,c0〉 ≝ acc in
482    let 〈c1,new_labels〉 ≝ match label with
483     [ None ⇒ 〈c0,labels〉
484     | Some l ⇒
485       match update ? ? pc l labels with
486       [ None ⇒ 〈c0,labels〉
487       | Some x ⇒ 〈true, x〉 ] ] in
488    let 〈pc_delta, jmp_len〉 ≝ match instr with
489     [ Call c ⇒
490       match lookup_opt ? ? c new_labels with
491        [ None        ⇒ 〈2, Some ? medium_jump〉
492        | Some c_addr ⇒ find_right_call pc c_addr ]
493     | Jmp j ⇒
494       match lookup_opt ? ? j new_labels with
495        [ None        ⇒ 〈2, Some ? short_jump〉
496        | Some j_addr ⇒ find_right_jump pc j_addr ]
497     | Instruction i ⇒ jep_relative pc new_labels i
498     | Mov _ _ ⇒ (* XXX is this correct? *) 〈2, None …〉
499     | Cost _ ⇒ 〈0, None …〉
500     | Comment _ ⇒ 〈0, None …〉 ] in
501    let 〈new_pc,ignore〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in
502    match jmp_len with
503    [ None   ⇒ 〈new_pc, new_labels, policy, c1〉
504    | Some j ⇒
505      match update ? ? pc j policy with
506      [ None ⇒ 〈new_pc, new_labels, policy, c1〉
507      | Some x ⇒ 〈new_pc, new_labels, x, true〉 ] ]
508   ) 〈zero ?, labels, policy, false〉 (\snd program) in
509   〈labels, policy, changed〉.
510
511(* let 〈new_labels, new_policy, ch〉 =
512 jump_expansion_policy_internal program old_labels old_policy in
513 if changed then recurse else stop *)
514 
515definition expand_relative_jump_internal:
516 (Identifier → Word) → jump_length → Identifier → Word → ([[relative]] → preinstruction [[relative]]) →
517 option (list instruction)
518 ≝
519  λlookup_labels,jmp_len.λjmp:Identifier.λpc,i.
520  match jmp_len with
521  [ short_jump ⇒
522     let lookup_address ≝ lookup_labels jmp in
523     let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in
524     let 〈upper, lower〉 ≝ split ? 8 8 result in
525     if eq_bv ? upper (zero 8) then
526      let address ≝ RELATIVE lower in
527       Some ? [ RealInstruction (i address) ]
528     else
529       None ?
530  | medium_jump ⇒ None …
531  | long_jump ⇒
532    Some ?
533    [ RealInstruction (i (RELATIVE (bitvector_of_nat ? 2)));
534      SJMP (RELATIVE (bitvector_of_nat ? 3)); (* LJMP size? *)
535      LJMP (ADDR16 (lookup_labels jmp))
536    ]
537  ].
538  @ I
539qed.
540
541definition expand_relative_jump: (Identifier → Word) → jump_length → Word → preinstruction Identifier → option (list instruction) ≝
542  λlookup_labels.
543  λjmp_len: jump_length.
544  λpc.
545  λi: preinstruction Identifier.
546  let rel_jmp ≝ RELATIVE (bitvector_of_nat ? 2) in
547  match i with
548  [ JC jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JC ?)
549  | JNC jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNC ?)
550  | JB baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JB ? baddr)
551  | JZ jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JZ ?)
552  | JNZ jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNZ ?)
553  | JBC baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JBC ? baddr)
554  | JNB baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNB ? baddr)
555  | CJNE addr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (CJNE ? addr)
556  | DJNZ addr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (DJNZ ? addr)
557  | ADD arg1 arg2 ⇒ Some ? [ ADD ? arg1 arg2 ]
558  | ADDC arg1 arg2 ⇒ Some ? [ ADDC ? arg1 arg2 ]
559  | SUBB arg1 arg2 ⇒ Some ? [ SUBB ? arg1 arg2 ]
560  | INC arg ⇒ Some ? [ INC ? arg ]
561  | DEC arg ⇒ Some ? [ DEC ? arg ]
562  | MUL arg1 arg2 ⇒ Some ? [ MUL ? arg1 arg2 ]
563  | DIV arg1 arg2 ⇒ Some ? [ DIV ? arg1 arg2 ]
564  | DA arg ⇒ Some ? [ DA ? arg ]
565  | ANL arg ⇒ Some ? [ ANL ? arg ]
566  | ORL arg ⇒ Some ? [ ORL ? arg ]
567  | XRL arg ⇒ Some ? [ XRL ? arg ]
568  | CLR arg ⇒ Some ? [ CLR ? arg ]
569  | CPL arg ⇒ Some ? [ CPL ? arg ]
570  | RL arg ⇒ Some ? [ RL ? arg ]
571  | RR arg ⇒ Some ? [ RR ? arg ]
572  | RLC arg ⇒ Some ? [ RLC ? arg ]
573  | RRC arg ⇒ Some ? [ RRC ? arg ]
574  | SWAP arg ⇒ Some ? [ SWAP ? arg ]
575  | MOV arg ⇒ Some ? [ MOV ? arg ]
576  | MOVX arg ⇒ Some ? [ MOVX ? arg ]
577  | SETB arg ⇒ Some ? [ SETB ? arg ]
578  | PUSH arg ⇒ Some ? [ PUSH ? arg ]
579  | POP arg ⇒ Some ? [ POP ? arg ]
580  | XCH arg1 arg2 ⇒ Some ? [ XCH ? arg1 arg2 ]
581  | XCHD arg1 arg2 ⇒ Some ? [ XCHD ? arg1 arg2 ]
582  | RET ⇒ Some ? [ RET ? ]
583  | RETI ⇒ Some ? [ RETI ? ]
584  | NOP ⇒ Some ? [ RealInstruction (NOP ?) ]
585  ].
586
587definition expand_pseudo_instruction: ? → ? → Word → jump_length → pseudo_instruction → option (list instruction) ≝
588  λlookup_labels.
589  λlookup_datalabels.
590  λpc.
591  λjmp_len.
592  λi.
593  match i with
594  [ Cost cost ⇒ Some ? [ ]
595  | Comment comment ⇒ Some ? [ ]
596  | Call call ⇒
597    match jmp_len with
598    [ short_jump ⇒ None ?
599    | medium_jump ⇒
600      let 〈ignore, address〉 ≝ split ? 5 11 (lookup_labels call) in
601      let 〈fst_5, rest〉 ≝ split ? 5 11 pc in
602      if eq_bv ? ignore fst_5 then
603        let address ≝ ADDR11 address in
604          Some ? ([ ACALL address ])
605      else
606        None ?
607    | long_jump ⇒
608      let address ≝ ADDR16 (lookup_labels call) in
609        Some ? [ LCALL address ]
610    ]
611  | Mov d trgt ⇒
612    let address ≝ DATA16 (lookup_datalabels trgt) in
613      Some ? [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))]
614  | Instruction instr ⇒ expand_relative_jump lookup_labels jmp_len pc instr
615  | Jmp jmp ⇒
616    match jmp_len with
617    [ short_jump ⇒
618      let lookup_address ≝ lookup_labels jmp in
619      let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in
620      let 〈upper, lower〉 ≝ split ? 8 8 result in
621      if eq_bv ? upper (zero 8) then
622        let address ≝ RELATIVE lower in
623          Some ? [ SJMP address ]
624      else
625        None ?
626    | medium_jump ⇒
627      let address ≝ lookup_labels jmp in
628      let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 address in
629      let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
630      if eq_bv ? fst_5_addr fst_5_pc then
631        let address ≝ ADDR11 rest_addr in
632          Some ? ([ AJMP address ])
633      else
634        None ?
635    | long_jump ⇒
636      let address ≝ ADDR16 (lookup_labels jmp) in
637        Some ? [ LJMP address ]
638    ]
639  ].
640  @ I
641qed.
642
643definition assembly_1_pseudoinstruction ≝
644  λprogram.
645  λpc.
646  λlookup_labels.
647  λlookup_datalabels.
648  λi.
649  let expansion ≝ jump_expansion_policy policy_zero program pc in
650    match expand_pseudo_instruction lookup_labels lookup_datalabels pc expansion i with
651    [ None ⇒ None ?
652    | Some pseudos ⇒
653      let mapped ≝ map ? ? assembly1 pseudos in
654      let flattened ≝ flatten ? mapped in
655      let len ≝ length ? flattened in
656        Some ? (〈len, flattened〉)
657    ].
658
659definition construct_datalabels ≝
660  λpreamble.
661    \fst (foldl ((BitVectorTrie Identifier 16) × nat) ? (
662    λt. λpreamble.
663      let 〈datalabels, addr〉 ≝ t in
664      let 〈name, size〉 ≝ preamble in
665      let addr_16 ≝ bitvector_of_nat 16 addr in
666        〈insert ? ? name addr_16 datalabels, addr + size〉)
667          〈(Stub ? ?), 0〉 preamble).
668
669definition construct_costs ≝
670  λprogram.
671  λprogram_counter: nat.
672  λlookup_labels.
673  λlookup_datalabels.
674  λcosts: BitVectorTrie Word 16.
675  λi.
676  match i with
677  [ Cost cost ⇒
678    let program_counter_bv ≝ bitvector_of_nat ? program_counter in
679      Some ? 〈program_counter, (insert ? ? program_counter_bv cost costs)〉
680  | _ ⇒
681    let pc_bv ≝ bitvector_of_nat ? program_counter in
682    let pc_delta_assembled ≝
683      assembly_1_pseudoinstruction program pc_bv
684        lookup_labels lookup_datalabels i
685    in
686    match pc_delta_assembled with
687    [ None ⇒ None ?
688    | Some pc_delta_assembled ⇒
689      let 〈pc_delta, assembled〉 ≝ pc_delta_assembled in
690        Some ? 〈pc_delta + program_counter, costs〉       
691    ]
692  ].
693
694definition build_maps ≝
695  λinstr_list.
696  let result ≝ foldl (option ((BitVectorTrie Word 16) × (nat × (BitVectorTrie Word 16)))) ?
697    (λt. λi.
698       let 〈label, i〉 ≝ i in
699       match t with
700       [ None ⇒ None ?
701       | Some t ⇒
702         let 〈labels, pc_costs〉 ≝ t in
703         let 〈program_counter, costs〉 ≝ pc_costs in
704         let labels ≝
705           match label with
706           [ None ⇒ labels
707           | Some label ⇒
708             let program_counter_bv ≝ bitvector_of_nat ? program_counter in
709               insert ? ? label program_counter_bv labels
710           ]
711         in
712           match construct_costs instr_list program_counter (λx. zero ?) (λx. zero ?) costs i with
713           [ None ⇒ None ?
714           | Some construct ⇒ Some ? 〈labels, construct〉
715           ]
716       ]) (Some ? 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉) (\snd instr_list) in
717  match result with
718  [ None ⇒ None ?
719  | Some result ⇒
720    let 〈labels, pc_costs〉 ≝ result in
721    let 〈pc, costs〉 ≝ pc_costs in
722      if gtb pc (2^16) then
723        None ?
724      else
725        Some ? 〈labels, costs〉
726  ].
727
728definition assembly: pseudo_assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
729  λp.
730    let 〈preamble, instr_list〉 ≝ p in
731      match build_maps p with
732      [ None ⇒ None ?
733      | Some labels_costs ⇒
734        let datalabels ≝ construct_datalabels preamble in
735        let 〈labels,costs〉 ≝ labels_costs in
736        let lookup_labels ≝ λx. lookup ? ? x labels (zero ?) in
737        let lookup_datalabels ≝ λx. lookup ? ? x datalabels (zero ?) in
738        let result ≝ foldr ? ? (λx. λy.
739            match y with
740            [ None ⇒ None ?
741            | Some lst ⇒
742              let 〈pc, y〉 ≝ lst in
743              let x ≝ assembly_1_pseudoinstruction p pc lookup_labels lookup_datalabels (\snd x) in
744              match x with
745              [ None ⇒ None ?
746              | Some x ⇒
747                let 〈pc_delta, program〉 ≝ x in
748                let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in
749                  Some ? 〈new_pc, (program @ y)〉
750              ]
751            ]) (Some ? 〈(zero ?), [ ]〉) instr_list
752        in
753          match result with
754          [ None ⇒ None ?
755          | Some result ⇒ Some ? (〈\snd result, costs〉)
756          ]
757      ].
758
759definition assembly_unlabelled_program: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
760 λp. Some ? (〈foldr ? ? (λi,l. assembly1 i @ l) [ ] p, Stub …〉).
Note: See TracBrowser for help on using the repository browser.