source: src/ASM/Assembly.ma @ 833

Last change on this file since 833 was 833, checked in by sacerdot, 8 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.