source: src/ASM/Assembly.ma @ 982

Last change on this file since 982 was 982, checked in by boender, 9 years ago
  • this should work (see previous commit)
File size: 36.4 KB
Line 
1include "ASM/ASM.ma".
2include "ASM/BitVectorTrie.ma".
3include "ASM/Arithmetic.ma".
4include "ASM/Fetch.ma".
5include "ASM/Status.ma".
6include "ASM/FoldStuff.ma".
7
8definition assembly_preinstruction ≝
9  λA: Type[0].
10  λaddr_of: A → Byte. (* relative *)
11  λpre: preinstruction A.
12  match pre with
13  [ ADD addr1 addr2 ⇒
14     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
15      [ REGISTER r ⇒ λ_.[ ([[false;false;true;false;true]]) @@ r ]
16      | DIRECT b1 ⇒ λ_.[ ([[false;false;true;false;false;true;false;true]]); b1 ]
17      | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;false;false;true;true;i1]]) ]
18      | DATA b1 ⇒ λ_. [ ([[false;false;true;false;false;true;false;false]]) ; b1 ]
19      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
20  | ADDC addr1 addr2 ⇒
21     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
22      [ REGISTER r ⇒ λ_.[ ([[false;false;true;true;true]]) @@ r ]
23      | DIRECT b1 ⇒ λ_.[ ([[false;false;true;true;false;true;false;true]]); b1 ]
24      | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;true;false;true;true;i1]]) ]
25      | DATA b1 ⇒ λ_. [ ([[false;false;true;true;false;true;false;false]]) ; b1 ]
26      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
27  | ANL addrs ⇒
28     match addrs with
29      [ inl addrs ⇒ match addrs with
30         [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
31           match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
32            [ REGISTER r ⇒ λ_.[ ([[false;true;false;true;true]]) @@ r ]
33            | DIRECT b1 ⇒ λ_.[ ([[false;true;false;true;false;true;false;true]]); b1 ]
34            | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;true;false;true;true;i1]]) ]
35            | DATA b1 ⇒ λ_. [ ([[false;true;false;true;false;true;false;false]]) ; b1 ]
36            | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
37         | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
38            let b1 ≝
39             match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
40              [ DIRECT b1 ⇒ λ_.b1
41              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
42            match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
43             [ ACC_A ⇒ λ_.[ ([[false;true;false;true;false;false;true;false]]) ; b1 ]
44             | DATA b2 ⇒ λ_. [ ([[false;true;false;true;false;false;true;true]]) ; b1 ; b2 ]
45             | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
46         ]
47      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
48         match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
49          [ BIT_ADDR b1 ⇒ λ_.[ ([[true;false;false;false;false;false;true;false]]) ; b1 ]
50          | N_BIT_ADDR b1 ⇒ λ_. [ ([[true;false;true;true;false;false;false;false]]) ; b1 ]
51          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
52  | CLR addr ⇒
53     match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with
54      [ ACC_A ⇒ λ_.
55         [ ([[true; true; true; false; false; true; false; false]]) ]
56      | CARRY ⇒ λ_.
57         [ ([[true; true; false; false; false; false; true; true]]) ]
58      | BIT_ADDR b1 ⇒ λ_.
59         [ ([[true; true; false; false; false; false; true; false]]) ; b1 ]
60      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
61  | CPL addr ⇒
62     match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with
63      [ ACC_A ⇒ λ_.
64         [ ([[true; true; true; true; false; true; false; false]]) ]
65      | CARRY ⇒ λ_.
66         [ ([[true; false; true; true; false; false; true; true]]) ]
67      | BIT_ADDR b1 ⇒ λ_.
68         [ ([[true; false; true; true; false; false; true; false]]) ; b1 ]
69      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
70  | DA addr ⇒
71     [ ([[true; true; false; true; false; true; false; false]]) ]
72  | DEC addr ⇒
73     match addr return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect]] x) → ? with
74      [ ACC_A ⇒ λ_.
75         [ ([[false; false; false; true; false; true; false; false]]) ]
76      | REGISTER r ⇒ λ_.
77         [ ([[false; false; false; true; true]]) @@ r ]
78      | DIRECT b1 ⇒ λ_.
79         [ ([[false; false; false; true; false; true; false; true]]); b1 ]
80      | INDIRECT i1 ⇒ λ_.
81         [ ([[false; false; false; true; false; true; true; i1]]) ]
82      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
83      | DJNZ addr1 addr2 ⇒
84         let b2 ≝ addr_of addr2 in
85         match addr1 return λx. bool_to_Prop (is_in ? [[registr;direct]] x) → ? with
86          [ REGISTER r ⇒ λ_.
87             [ ([[true; true; false; true; true]]) @@ r ; b2 ]
88          | DIRECT b1 ⇒ λ_.
89             [ ([[true; true; false; true; false; true; false; true]]); b1; b2 ]
90          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
91      | JC addr ⇒
92        let b1 ≝ addr_of addr in
93          [ ([[false; true; false; false; false; false; false; false]]); b1 ]
94      | JNC addr ⇒
95         let b1 ≝ addr_of addr in
96           [ ([[false; true; false; true; false; false; false; false]]); b1 ]
97      | JZ addr ⇒
98         let b1 ≝ addr_of addr in
99           [ ([[false; true; true; false; false; false; false; false]]); b1 ]
100      | JNZ addr ⇒
101         let b1 ≝ addr_of addr in
102           [ ([[false; true; true; true; false; false; false; false]]); b1 ]
103      | JB addr1 addr2 ⇒
104         let b2 ≝ addr_of addr2 in
105         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
106          [ BIT_ADDR b1 ⇒ λ_.
107             [ ([[false; false; true; false; false; false; false; false]]); b1; b2 ]
108          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
109      | JNB addr1 addr2 ⇒
110         let b2 ≝ addr_of addr2 in
111         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
112          [ BIT_ADDR b1 ⇒ λ_.
113             [ ([[false; false; true; true; false; false; false; false]]); b1; b2 ]
114          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
115      | JBC addr1 addr2 ⇒
116         let b2 ≝ addr_of addr2 in
117         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
118          [ BIT_ADDR b1 ⇒ λ_.
119             [ ([[false; false; false; true; false; false; false; false]]); b1; b2 ]
120          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
121      | CJNE addrs addr3 ⇒
122         let b3 ≝ addr_of addr3 in
123         match addrs with
124          [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
125             match addr2 return λx. bool_to_Prop (is_in ? [[direct;data]] x) → ? with
126              [ DIRECT b1 ⇒ λ_.
127                 [ ([[true; false; true; true; false; true; false; true]]); b1; b3 ]
128              | DATA b1 ⇒ λ_.
129                 [ ([[true; false; true; true; false; true; false; false]]); b1; b3 ]
130              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
131          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
132             let b2 ≝
133              match addr2 return λx. bool_to_Prop (is_in ? [[data]] x) → ? with
134               [ DATA b2 ⇒ λ_. b2
135               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
136             match addr1 return λx. bool_to_Prop (is_in ? [[registr;indirect]] x) → list Byte with
137              [ REGISTER r ⇒ λ_.
138                 [ ([[true; false; true; true; true]]) @@ r; b2; b3 ]
139              | INDIRECT i1 ⇒ λ_.
140                 [ ([[true; false; true; true; false; true; true; i1]]); b2; b3 ]
141              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
142         ]
143  | DIV addr1 addr2 ⇒
144     [ ([[true;false;false;false;false;true;false;false]]) ]
145  | INC addr ⇒
146     match addr return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect;dptr]] x) → ? with
147      [ ACC_A ⇒ λ_.
148         [ ([[false;false;false;false;false;true;false;false]]) ]         
149      | REGISTER r ⇒ λ_.
150         [ ([[false;false;false;false;true]]) @@ r ]
151      | DIRECT b1 ⇒ λ_.
152         [ ([[false; false; false; false; false; true; false; true]]); b1 ]
153      | INDIRECT i1 ⇒ λ_.
154        [ ([[false; false; false; false; false; true; true; i1]]) ]
155      | DPTR ⇒ λ_.
156        [ ([[true;false;true;false;false;false;true;true]]) ]
157      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
158  | MOV addrs ⇒
159     match addrs with
160      [ inl addrs ⇒
161         match addrs with
162          [ inl addrs ⇒
163             match addrs with
164              [ inl addrs ⇒
165                 match addrs with
166                  [ inl addrs ⇒
167                     match addrs with
168                      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
169                         match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
170                          [ REGISTER r ⇒ λ_.[ ([[true;true;true;false;true]]) @@ r ]
171                          | DIRECT b1 ⇒ λ_.[ ([[true;true;true;false;false;true;false;true]]); b1 ]
172                          | INDIRECT i1 ⇒ λ_. [ ([[true;true;true;false;false;true;true;i1]]) ]
173                          | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;false;false]]) ; b1 ]
174                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
175                      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
176                         match addr1 return λx. bool_to_Prop (is_in ? [[registr;indirect]] x) → ? with
177                          [ REGISTER r ⇒ λ_.
178                             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with
179                              [ ACC_A ⇒ λ_.[ ([[true;true;true;true;true]]) @@ r ]
180                              | DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;true]]) @@ r; b1 ]
181                              | DATA b1 ⇒ λ_. [ ([[false;true;true;true;true]]) @@ r; b1 ]
182                              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
183                          | INDIRECT i1 ⇒ λ_.
184                             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with
185                              [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;true;i1]]) ]
186                              | DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;false;true;true;i1]]); b1 ]
187                              | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;true;i1]]) ; b1 ]
188                              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
189                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
190                  | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
191                     let b1 ≝
192                      match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
193                       [ DIRECT b1 ⇒ λ_. b1
194                       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
195                     match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;registr;direct;indirect;data]] x) → ? with
196                      [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;false;true]]); b1]
197                      | REGISTER r ⇒ λ_.[ ([[true;false;false;false;true]]) @@ r; b1 ]
198                      | DIRECT b2 ⇒ λ_.[ ([[true;false;false;false;false;true;false;true]]); b1; b2 ]
199                      | INDIRECT i1 ⇒ λ_. [ ([[true;false;false;false;false;true;true;i1]]); b1 ]
200                      | DATA b2 ⇒ λ_. [ ([[false;true;true;true;false;true;false;true]]); b1; b2 ]
201                      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
202              | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
203                 match addr2 return λx. bool_to_Prop (is_in ? [[data16]] x) → ? with
204                  [ DATA16 w ⇒ λ_.
205                     let b1_b2 ≝ split ? 8 8 w in
206                     let b1 ≝ \fst b1_b2 in
207                     let b2 ≝ \fst b1_b2 in
208                      [ ([[true;false;false;true;false;false;false;false]]); b1; b2]
209                  | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
210          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
211             match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
212              [ BIT_ADDR b1 ⇒ λ_.
213                 [ ([[true;false;true;false;false;false;true;false]]); b1 ]
214              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
215      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
216         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
217          [ BIT_ADDR b1 ⇒ λ_.
218             [ ([[true;false;false;true;false;false;true;false]]); b1 ]
219          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
220  | MOVX addrs ⇒
221     match addrs with
222      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
223         match addr2 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
224          [ EXT_INDIRECT i1 ⇒ λ_.
225             [ ([[true;true;true;false;false;false;true;i1]]) ]
226          | EXT_INDIRECT_DPTR ⇒ λ_.
227             [ ([[true;true;true;false;false;false;false;false]]) ]
228          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
229      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
230         match addr1 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
231          [ EXT_INDIRECT i1 ⇒ λ_.
232             [ ([[true;true;true;true;false;false;true;i1]]) ]
233          | EXT_INDIRECT_DPTR ⇒ λ_.
234             [ ([[true;true;true;true;false;false;false;false]]) ]
235          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
236  | MUL addr1 addr2 ⇒
237     [ ([[true;false;true;false;false;true;false;false]]) ]
238  | NOP ⇒
239     [ ([[false;false;false;false;false;false;false;false]]) ]
240  | ORL addrs ⇒
241     match addrs with
242      [ inl addrs ⇒
243         match addrs with
244          [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
245             match addr2 return λx. bool_to_Prop (is_in ? [[registr;data;direct;indirect]] x) → ? with
246             [ REGISTER r ⇒ λ_.[ ([[false;true;false;false;true]]) @@ r ]
247             | DIRECT b1 ⇒ λ_.[ ([[false;true;false;false;false;true;false;true]]); b1 ]
248             | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;false;false;true;true;i1]]) ]
249             | DATA b1 ⇒ λ_. [ ([[false;true;false;false;false;true;false;false]]) ; b1 ]
250             | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
251          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
252            let b1 ≝
253              match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
254               [ DIRECT b1 ⇒ λ_. b1
255               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
256             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
257              [ ACC_A ⇒ λ_.
258                 [ ([[false;true;false;false;false;false;true;false]]); b1 ]
259              | DATA b2 ⇒ λ_.
260                 [ ([[false;true;false;false;false;false;true;true]]); b1; b2 ]
261              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
262      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in     
263         match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
264          [ BIT_ADDR b1 ⇒ λ_.
265             [ ([[false;true;true;true;false;false;true;false]]); b1 ]
266          | N_BIT_ADDR b1 ⇒ λ_.
267             [ ([[true;false;true;false;false;false;false;false]]); b1 ]
268          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
269  | POP addr ⇒
270     match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
271      [ DIRECT b1 ⇒ λ_.
272         [ ([[true;true;false;true;false;false;false;false]]) ; b1 ]
273      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
274  | PUSH addr ⇒
275     match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
276      [ DIRECT b1 ⇒ λ_.
277         [ ([[true;true;false;false;false;false;false;false]]) ; b1 ]
278      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
279  | RET ⇒
280     [ ([[false;false;true;false;false;false;true;false]]) ]
281  | RETI ⇒
282     [ ([[false;false;true;true;false;false;true;false]]) ]
283  | RL addr ⇒
284     [ ([[false;false;true;false;false;false;true;true]]) ]
285  | RLC addr ⇒
286     [ ([[false;false;true;true;false;false;true;true]]) ]
287  | RR addr ⇒
288     [ ([[false;false;false;false;false;false;true;true]]) ]
289  | RRC addr ⇒
290     [ ([[false;false;false;true;false;false;true;true]]) ]
291  | SETB addr ⇒     
292     match addr return λx. bool_to_Prop (is_in ? [[carry;bit_addr]] x) → ? with
293      [ CARRY ⇒ λ_.
294         [ ([[true;true;false;true;false;false;true;true]]) ]
295      | BIT_ADDR b1 ⇒ λ_.
296         [ ([[true;true;false;true;false;false;true;false]]); b1 ]
297      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
298  | SUBB addr1 addr2 ⇒
299     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect;data]] x) → ? with
300      [ REGISTER r ⇒ λ_.
301         [ ([[true;false;false;true;true]]) @@ r ]
302      | DIRECT b1 ⇒ λ_.
303         [ ([[true;false;false;true;false;true;false;true]]); b1]
304      | INDIRECT i1 ⇒ λ_.
305         [ ([[true;false;false;true;false;true;true;i1]]) ]
306      | DATA b1 ⇒ λ_.
307         [ ([[true;false;false;true;false;true;false;false]]); b1]
308      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
309  | SWAP addr ⇒
310     [ ([[true;true;false;false;false;true;false;false]]) ]
311  | XCH addr1 addr2 ⇒
312     match addr2 return λx. bool_to_Prop (is_in ? [[registr;direct;indirect]] x) → ? with
313      [ REGISTER r ⇒ λ_.
314         [ ([[true;true;false;false;true]]) @@ r ]
315      | DIRECT b1 ⇒ λ_.
316         [ ([[true;true;false;false;false;true;false;true]]); b1]
317      | INDIRECT i1 ⇒ λ_.
318         [ ([[true;true;false;false;false;true;true;i1]]) ]
319      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
320  | XCHD addr1 addr2 ⇒
321     match addr2 return λx. bool_to_Prop (is_in ? [[indirect]] x) → ? with
322      [ INDIRECT i1 ⇒ λ_.
323         [ ([[true;true;false;true;false;true;true;i1]]) ]
324      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
325  | XRL addrs ⇒
326     match addrs with
327      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
328         match addr2 return λx. bool_to_Prop (is_in ? [[data;registr;direct;indirect]] x) → ? with
329          [ REGISTER r ⇒ λ_.
330             [ ([[false;true;true;false;true]]) @@ r ]
331          | DIRECT b1 ⇒ λ_.
332             [ ([[false;true;true;false;false;true;false;true]]); b1]
333          | INDIRECT i1 ⇒ λ_.
334             [ ([[false;true;true;false;false;true;true;i1]]) ]
335          | DATA b1 ⇒ λ_.
336             [ ([[false;true;true;false;false;true;false;false]]); b1]
337          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
338      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
339         let b1 ≝
340          match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
341           [ DIRECT b1 ⇒ λ_. b1
342           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
343         match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
344          [ ACC_A ⇒ λ_.
345             [ ([[false;true;true;false;false;false;true;false]]); b1 ]         
346          | DATA b2 ⇒ λ_.
347             [ ([[false;true;true;false;false;false;true;true]]); b1; b2 ]
348          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
349       ].
350
351definition assembly1 ≝
352 λi: instruction.
353 match i with
354  [ ACALL addr ⇒
355     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
356      [ ADDR11 w ⇒ λ_.
357         let v1_v2 ≝ split ? 3 8 w in
358         let v1 ≝ \fst v1_v2 in
359         let v2 ≝ \snd v1_v2 in
360          [ (v1 @@ [[true; false; false; false; true]]) ; v2 ]
361      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
362  | AJMP addr ⇒
363     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
364      [ ADDR11 w ⇒ λ_.
365         let v1_v2 ≝ split ? 3 8 w in
366         let v1 ≝ \fst v1_v2 in
367         let v2 ≝ \snd v1_v2 in
368          [ (v1 @@ [[false; false; false; false; true]]) ; v2 ]
369      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
370  | JMP adptr ⇒
371     [ ([[false;true;true;true;false;false;true;true]]) ]
372  | LCALL addr ⇒
373     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
374      [ ADDR16 w ⇒ λ_.
375         let b1_b2 ≝ split ? 8 8 w in
376         let b1 ≝ \fst b1_b2 in
377         let b2 ≝ \snd b1_b2 in
378          [ ([[false;false;false;true;false;false;true;false]]); b1; b2 ]         
379      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
380  | LJMP addr ⇒
381     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
382      [ ADDR16 w ⇒ λ_.
383         let b1_b2 ≝ split ? 8 8 w in
384         let b1 ≝ \fst b1_b2 in
385         let b2 ≝ \snd b1_b2 in
386          [ ([[false;false;false;false;false;false;true;false]]); b1; b2 ]         
387      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
388  | MOVC addr1 addr2 ⇒
389     match addr2 return λx. bool_to_Prop (is_in ? [[acc_dptr;acc_pc]] x) → ? with
390      [ ACC_DPTR ⇒ λ_.
391         [ ([[true;false;false;true;false;false;true;true]]) ]
392      | ACC_PC ⇒ λ_.
393         [ ([[true;false;false;false;false;false;true;true]]) ]
394      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
395  | SJMP addr ⇒
396     match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
397      [ RELATIVE b1 ⇒ λ_.
398         [ ([[true;false;false;false;false;false;false;false]]); b1 ]
399      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
400  | RealInstruction instr ⇒
401    assembly_preinstruction [[ relative ]]
402      (λx.
403        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → ? with
404        [ RELATIVE r ⇒ λ_. r
405        | _ ⇒ λabsd. ⊥
406        ] (subaddressing_modein … x)) instr
407  ].
408  cases absd
409qed.
410
411definition is_relative_jump ≝
412  λi: preinstruction Identifier.
413  match i with
414  [ JC _ ⇒ True
415  | JNC _ ⇒ True
416  | JB _ _ ⇒ True
417  | JNB _ _ ⇒ True
418  | JBC _ _ ⇒ True
419  | JZ _ ⇒ True
420  | JNZ _ ⇒ True
421  | CJNE _ _ ⇒ True
422  | DJNZ _ _ ⇒ True
423  | _ ⇒ False
424  ].
425
426definition pseudo_instruction_is_relative_jump: pseudo_instruction → Prop ≝
427 λi.
428  match i with
429   [ Instruction j ⇒ is_relative_jump j
430   | _ ⇒ False ].
431
432inductive jump_length: Type[0] ≝
433  | short_jump: jump_length
434  | medium_jump: jump_length
435  | long_jump: jump_length.
436
437definition jump_expansion_policy ≝ BitVectorTrie jump_length 16.
438
439definition find_right_call: Word → Word → nat × (option jump_length) ≝
440 (* medium call: 11 bits, only in "current segment" *)
441 (* can this be done more efficiently with bit vector arithmetic? *)
442 λpc.λaddress.
443  let 〈p1, p2〉 ≝ split ? 5 11 address in
444  let 〈a1, a2〉 ≝ split ? 5 11 pc in
445   if eq_bv ? p1 a1 then (* we're in the same segment *)
446    〈2, Some ? medium_jump〉
447   else
448    〈3, Some ? long_jump〉.
449
450definition distance ≝
451 λx.λy.if gtb x y then x - y else y - x.
452 
453definition find_right_jump: Word → Word → nat × (option jump_length) ≝
454 (* short jump: 8 bits signed *)
455 (* medium jump: 11 bits, forward only *)
456 λpc.λaddress.
457  let pn ≝ nat_of_bitvector ? pc in
458  let pa ≝ nat_of_bitvector ? address in
459   if ltb (distance pn pa) 127 then
460    〈2, Some ? short_jump〉
461   else
462    find_right_call pc address.
463
464definition find_right_relative_jump: Word → (BitVectorTrie Word 16) →
465 Identifier → nat × (option jump_length) ≝
466 λpc.λlabels.λjmp.
467 match lookup_opt ? ? jmp labels with
468 [ None ⇒ 〈2, Some ? short_jump〉
469 | Some a ⇒ find_right_jump pc a ].
470 
471definition jep_relative: Word → (BitVectorTrie Word 16) → preinstruction Identifier → ? ≝
472 λpc.λlabels.λi.
473  match i with
474  [ JC jmp ⇒ find_right_relative_jump pc labels jmp
475  | JNC jmp ⇒ find_right_relative_jump pc labels jmp
476  | JB baddr jmp ⇒ find_right_relative_jump pc labels jmp
477  | JZ jmp ⇒ find_right_relative_jump pc labels jmp
478  | JNZ jmp ⇒ find_right_relative_jump pc labels jmp
479  | JBC baddr jmp ⇒ find_right_relative_jump pc labels jmp
480  | JNB baddr jmp ⇒ find_right_relative_jump pc labels jmp
481  | CJNE addr jmp ⇒ find_right_relative_jump pc labels jmp
482  | DJNZ addr jmp ⇒ find_right_relative_jump pc labels jmp
483  | _ ⇒ 〈length ? (assembly_preinstruction ? (λx.zero ?) i), None …〉 ].
484 
485definition jump_expansion_policy_internal: pseudo_assembly_program →
486 (BitVectorTrie Word 16) → jump_expansion_policy →
487 ((BitVectorTrie Word 16) × jump_expansion_policy × bool)≝
488 λprogram.λlabels.λpolicy.
489   let 〈pc, new_labels, new_policy, changed〉 ≝
490   foldl ? ? (λacc.λi:labelled_instruction.
491    let 〈label, instr〉 ≝ i in
492    let 〈pc,labels,policy,c0〉 ≝ acc in
493    let 〈c1,new_labels〉 ≝ match label with
494     [ None ⇒ 〈c0,labels〉
495     | Some l ⇒
496       match update ? ? pc l labels with
497       [ None ⇒ 〈c0,labels〉
498       | Some x ⇒ 〈true, x〉 ] ] in
499    let 〈pc_delta, jmp_len〉 ≝ match instr with
500     [ Call c ⇒
501       match lookup_opt ? ? c new_labels with
502        [ None        ⇒ 〈2, Some ? medium_jump〉
503        | Some c_addr ⇒ find_right_call pc c_addr ]
504     | Jmp j ⇒
505       match lookup_opt ? ? j new_labels with
506        [ None        ⇒ 〈2, Some ? short_jump〉
507        | Some j_addr ⇒ find_right_jump pc j_addr ]
508     | Instruction i ⇒ jep_relative pc new_labels i
509     | Mov _ _ ⇒ 〈3, None …〉
510     | Cost _ ⇒ 〈0, None …〉
511     | Comment _ ⇒ 〈0, None …〉 ] in
512    let 〈new_pc,ignore〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in
513    match jmp_len with
514    [ None   ⇒ 〈new_pc, new_labels, policy, c1〉
515    | Some j ⇒
516      match update ? ? pc j policy with
517      [ None ⇒ 〈new_pc, new_labels, policy, c1〉
518      | Some x ⇒ 〈new_pc, new_labels, x, true〉 ] ]
519   ) 〈zero ?, labels, policy, false〉 (\snd program) in
520   〈labels, policy, changed〉.
521
522definition expand_relative_jump_internal:
523 (Identifier → Word) → jump_length → Identifier → Word → ([[relative]] → preinstruction [[relative]]) →
524 option (list instruction)
525 ≝
526  λlookup_labels,jmp_len.λjmp:Identifier.λpc,i.
527  match jmp_len with
528  [ short_jump ⇒
529     let lookup_address ≝ lookup_labels jmp in
530     let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in
531     let 〈upper, lower〉 ≝ split ? 8 8 result in
532     if eq_bv ? upper (zero 8) then
533      let address ≝ RELATIVE lower in
534       Some ? [ RealInstruction (i address) ]
535     else
536       None ?
537  | medium_jump ⇒ None …
538  | long_jump ⇒
539    Some ?
540    [ RealInstruction (i (RELATIVE (bitvector_of_nat ? 2)));
541      SJMP (RELATIVE (bitvector_of_nat ? 3)); (* LJMP size? *)
542      LJMP (ADDR16 (lookup_labels jmp))
543    ]
544  ].
545  @ I
546qed.
547
548definition expand_relative_jump: (Identifier → Word) → jump_length → Word → preinstruction Identifier → option (list instruction) ≝
549  λlookup_labels.
550  λjmp_len: jump_length.
551  λpc.
552  λi: preinstruction Identifier.
553  let rel_jmp ≝ RELATIVE (bitvector_of_nat ? 2) in
554  match i with
555  [ JC jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JC ?)
556  | JNC jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNC ?)
557  | JB baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JB ? baddr)
558  | JZ jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JZ ?)
559  | JNZ jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNZ ?)
560  | JBC baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JBC ? baddr)
561  | JNB baddr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (JNB ? baddr)
562  | CJNE addr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (CJNE ? addr)
563  | DJNZ addr jmp ⇒ expand_relative_jump_internal lookup_labels jmp_len jmp pc (DJNZ ? addr)
564  | ADD arg1 arg2 ⇒ Some ? [ ADD ? arg1 arg2 ]
565  | ADDC arg1 arg2 ⇒ Some ? [ ADDC ? arg1 arg2 ]
566  | SUBB arg1 arg2 ⇒ Some ? [ SUBB ? arg1 arg2 ]
567  | INC arg ⇒ Some ? [ INC ? arg ]
568  | DEC arg ⇒ Some ? [ DEC ? arg ]
569  | MUL arg1 arg2 ⇒ Some ? [ MUL ? arg1 arg2 ]
570  | DIV arg1 arg2 ⇒ Some ? [ DIV ? arg1 arg2 ]
571  | DA arg ⇒ Some ? [ DA ? arg ]
572  | ANL arg ⇒ Some ? [ ANL ? arg ]
573  | ORL arg ⇒ Some ? [ ORL ? arg ]
574  | XRL arg ⇒ Some ? [ XRL ? arg ]
575  | CLR arg ⇒ Some ? [ CLR ? arg ]
576  | CPL arg ⇒ Some ? [ CPL ? arg ]
577  | RL arg ⇒ Some ? [ RL ? arg ]
578  | RR arg ⇒ Some ? [ RR ? arg ]
579  | RLC arg ⇒ Some ? [ RLC ? arg ]
580  | RRC arg ⇒ Some ? [ RRC ? arg ]
581  | SWAP arg ⇒ Some ? [ SWAP ? arg ]
582  | MOV arg ⇒ Some ? [ MOV ? arg ]
583  | MOVX arg ⇒ Some ? [ MOVX ? arg ]
584  | SETB arg ⇒ Some ? [ SETB ? arg ]
585  | PUSH arg ⇒ Some ? [ PUSH ? arg ]
586  | POP arg ⇒ Some ? [ POP ? arg ]
587  | XCH arg1 arg2 ⇒ Some ? [ XCH ? arg1 arg2 ]
588  | XCHD arg1 arg2 ⇒ Some ? [ XCHD ? arg1 arg2 ]
589  | RET ⇒ Some ? [ RET ? ]
590  | RETI ⇒ Some ? [ RETI ? ]
591  | NOP ⇒ Some ? [ RealInstruction (NOP ?) ]
592  ].
593
594definition expand_pseudo_instruction: ? → ? → Word → jump_length → pseudo_instruction → option (list instruction) ≝
595  λlookup_labels.
596  λlookup_datalabels.
597  λpc.
598  λjmp_len.
599  λi.
600  match i with
601  [ Cost cost ⇒ Some ? [ ]
602  | Comment comment ⇒ Some ? [ ]
603  | Call call ⇒
604    match jmp_len with
605    [ short_jump ⇒ None ?
606    | medium_jump ⇒
607      let 〈ignore, address〉 ≝ split ? 5 11 (lookup_labels call) in
608      let 〈fst_5, rest〉 ≝ split ? 5 11 pc in
609      if eq_bv ? ignore fst_5 then
610        let address ≝ ADDR11 address in
611          Some ? ([ ACALL address ])
612      else
613        None ?
614    | long_jump ⇒
615      let address ≝ ADDR16 (lookup_labels call) in
616        Some ? [ LCALL address ]
617    ]
618  | Mov d trgt ⇒
619    let address ≝ DATA16 (lookup_datalabels trgt) in
620      Some ? [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))]
621  | Instruction instr ⇒ expand_relative_jump lookup_labels jmp_len pc instr
622  | Jmp jmp ⇒
623    match jmp_len with
624    [ short_jump ⇒
625      let lookup_address ≝ lookup_labels jmp in
626      let 〈result, flags〉 ≝ sub_16_with_carry pc lookup_address false in
627      let 〈upper, lower〉 ≝ split ? 8 8 result in
628      if eq_bv ? upper (zero 8) then
629        let address ≝ RELATIVE lower in
630          Some ? [ SJMP address ]
631      else
632        None ?
633    | medium_jump ⇒
634      let address ≝ lookup_labels jmp in
635      let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 address in
636      let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in
637      if eq_bv ? fst_5_addr fst_5_pc then
638        let address ≝ ADDR11 rest_addr in
639          Some ? ([ AJMP address ])
640      else
641        None ?
642    | long_jump ⇒
643      let address ≝ ADDR16 (lookup_labels jmp) in
644        Some ? [ LJMP address ]
645    ]
646  ].
647  @ I
648qed.
649
650let rec jump_expansion_internal (n: nat) (program: pseudo_assembly_program)
651 (old_labels: BitVectorTrie Word 16) (old_policy: BitVectorTrie jump_length 16)
652 on n: jump_expansion_policy ≝
653 match n with
654 [ O ⇒ old_policy
655 | S n' ⇒
656   let 〈new_labels, new_policy, ch〉 ≝
657    jump_expansion_policy_internal program old_labels old_policy in
658    jump_expansion_internal n' program new_labels new_policy ].
659         
660definition jump_expansion ≝
661 λpc.λprogram.
662  let policy ≝ jump_expansion_internal (length ? (\snd program)) program (Stub ? ?) (Stub ? ?) in
663  lookup ? ? pc policy long_jump.
664 
665definition assembly_1_pseudoinstruction ≝
666  λprogram: pseudo_assembly_program.
667  λppc: Word.
668  λpc: Word.
669  λlookup_labels.
670  λlookup_datalabels.
671  λi.
672  let expansion ≝ jump_expansion ppc program in
673    match expand_pseudo_instruction lookup_labels lookup_datalabels pc expansion i with
674    [ None ⇒ None ?
675    | Some pseudos ⇒
676      let mapped ≝ map ? ? assembly1 pseudos in
677      let flattened ≝ flatten ? mapped in
678      let pc_len ≝ length ? flattened in
679        Some ? (〈pc_len, flattened〉)
680    ].
681 
682definition construct_datalabels ≝
683  λpreamble.
684    \fst (foldl ((BitVectorTrie Identifier 16) × nat) ? (
685    λt. λpreamble.
686      let 〈datalabels, addr〉 ≝ t in
687      let 〈name, size〉 ≝ preamble in
688      let addr_16 ≝ bitvector_of_nat 16 addr in
689        〈insert ? ? name addr_16 datalabels, addr + size〉)
690          〈(Stub ? ?), 0〉 preamble).
691
692definition construct_costs ≝
693  λprogram.
694  λpseudo_program_counter: nat.
695  λprogram_counter: nat.
696  λlookup_labels.
697  λlookup_datalabels.
698  λcosts: BitVectorTrie Word 16.
699  λi.
700  match i with
701  [ Cost cost ⇒
702    let program_counter_bv ≝ bitvector_of_nat ? program_counter in
703      Some ? 〈program_counter, (insert ? ? program_counter_bv cost costs)〉
704  | _ ⇒
705    let pc_bv ≝ bitvector_of_nat ? program_counter in
706    let ppc_bv ≝ bitvector_of_nat ? pseudo_program_counter in
707    let pc_delta_assembled ≝
708      assembly_1_pseudoinstruction program ppc_bv pc_bv
709        lookup_labels lookup_datalabels i
710    in
711    match pc_delta_assembled with
712    [ None ⇒ None ?
713    | Some pc_delta_assembled ⇒
714      let 〈pc_delta, assembled〉 ≝ pc_delta_assembled in
715        Some ? 〈pc_delta + program_counter, costs〉       
716    ]
717  ].
718
719definition build_maps ≝
720  λinstr_list.
721  let result ≝ foldl (option ((BitVectorTrie Word 16) × (nat × (nat × (BitVectorTrie Word 16))))) ?
722    (λt. λi.
723       let 〈label, i〉 ≝ i in
724       match t with
725       [ None ⇒ None ?
726       | Some t ⇒
727         let 〈labels, pc_ppc_costs〉 ≝ t in
728         let 〈program_counter, ppc_costs〉 ≝ pc_ppc_costs in
729         let 〈pseudo_program_counter, costs〉 ≝ ppc_costs in
730         let labels ≝
731           match label with
732           [ None ⇒ labels
733           | Some label ⇒
734             let program_counter_bv ≝ bitvector_of_nat ? program_counter in
735               insert ? ? label program_counter_bv labels
736           ]
737         in
738           match construct_costs instr_list pseudo_program_counter program_counter (λx. zero ?) (λx. zero ?) costs i with
739           [ None ⇒ None ?
740           | Some construct ⇒ Some ? 〈labels, 〈pseudo_program_counter + 1, construct〉〉
741           ]
742       ]) (Some ? 〈(Stub ? ?), 〈0, 〈0, (Stub ? ?)〉〉〉) (\snd instr_list) in
743  match result with
744  [ None ⇒ None ?
745  | Some result ⇒
746    let 〈labels, pc_ppc_costs〉 ≝ result in
747    let 〈pc, ppc_costs〉 ≝ pc_ppc_costs in
748    let 〈ppc, costs〉 ≝ ppc_costs in
749      if gtb pc (2^16) then
750        None ?
751      else
752        Some ? 〈labels, costs〉
753  ].
754
755definition assembly: pseudo_assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
756  λp.
757    let 〈preamble, instr_list〉 ≝ p in
758      match build_maps p with
759      [ None ⇒ None ?
760      | Some labels_costs ⇒
761        let datalabels ≝ construct_datalabels preamble in
762        let 〈labels,costs〉 ≝ labels_costs in
763        let lookup_labels ≝ λx. lookup ? ? x labels (zero ?) in
764        let lookup_datalabels ≝ λx. lookup ? ? x datalabels (zero ?) in
765        let result ≝ foldr ? ? (λx. λy.
766            match y with
767            [ None ⇒ None ?
768            | Some lst ⇒
769              let 〈pc, ppc_y〉 ≝ lst in
770              let 〈ppc, y〉 ≝ ppc_y in
771              let x ≝ assembly_1_pseudoinstruction p ppc pc lookup_labels lookup_datalabels (\snd x) in
772              match x with
773              [ None ⇒ None ?
774              | Some x ⇒
775                let 〈pc_delta, program〉 ≝ x in
776                let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in
777                let new_ppc ≝ \snd (half_add ? ppc (bitvector_of_nat ? 1)) in
778                  Some ? 〈new_pc, 〈new_ppc, (program @ y)〉〉
779              ]
780            ]) (Some ? 〈(zero ?), 〈(zero ?), [ ]〉〉) instr_list
781        in
782          match result with
783          [ None ⇒ None ?
784          | Some result ⇒ Some ? (〈\snd (\snd result), costs〉)
785          ]
786      ].
787
788definition assembly_unlabelled_program: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
789 λp. Some ? (〈foldr ? ? (λi,l. assembly1 i @ l) [ ] p, Stub …〉).
Note: See TracBrowser for help on using the repository browser.