source: src/ASM/Assembly.ma @ 833

Last change on this file since 833 was 833, checked in by sacerdot, 10 years ago

Bug fixed to make the file compile.
But the type of the assembly function is no more right.

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