source: src/ASM/Assembly.ma @ 719

Last change on this file since 719 was 719, checked in by mulligan, 10 years ago

Added missing assembly file ported to matita.
File size: 28.5 KB
Line 
1include "ASM/ASM.ma".
2include "ASM/BitVectorTrie.ma".
3include "ASM/Arithmetic.ma".
4include "ASM/Fetch.ma".
5include "ASM/Status.ma".
6
7definition assembly1 ≝
8 λi: instruction.
9 match i with
10  [ ACALL addr ⇒
11     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
12      [ ADDR11 w ⇒ λ_.
13         let 〈v1,v2〉 ≝ split ? 3 8 w in
14          [ (v1 @@ [[true; false; false; false; true]]) ; v2 ]
15      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
16  | ADD addr1 addr2 ⇒
17     match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
18      [ REGISTER r ⇒ λ_.[ ([[false;false;true;false;true]]) @@ r ]
19      | DIRECT b1 ⇒ λ_.[ ([[false;false;true;false;false;true;false;true]]); b1 ]
20      | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;false;false;true;true;i1]]) ]
21      | DATA b1 ⇒ λ_. [ ([[false;false;true;false;false;true;false;false]]) ; b1 ]
22      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
23  | ADDC addr1 addr2 ⇒
24     match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
25      [ REGISTER r ⇒ λ_.[ ([[false;false;true;true;true]]) @@ r ]
26      | DIRECT b1 ⇒ λ_.[ ([[false;false;true;true;false;true;false;true]]); b1 ]
27      | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;true;false;true;true;i1]]) ]
28      | DATA b1 ⇒ λ_. [ ([[false;false;true;true;false;true;false;false]]) ; b1 ]
29      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
30  | AJMP addr ⇒
31     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
32      [ ADDR11 w ⇒ λ_.
33         let 〈v1,v2〉 ≝ split ?  3 8 w in
34          [ (v1 @@ [[false; false; false; false; true]]) ; v2 ]
35      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
36  | ANL addrs ⇒
37     match addrs with
38      [ inl addrs ⇒ match addrs with
39         [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
40           match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
41            [ REGISTER r ⇒ λ_.[ ([[false;true;false;true;true]]) @@ r ]
42            | DIRECT b1 ⇒ λ_.[ ([[false;true;false;true;false;true;false;true]]); b1 ]
43            | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;true;false;true;true;i1]]) ]
44            | DATA b1 ⇒ λ_. [ ([[false;true;false;true;false;true;false;false]]) ; b1 ]
45            | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
46         | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
47            let b1 ≝
48             match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
49              [ DIRECT b1 ⇒ λ_.b1
50              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
51            match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
52             [ ACC_A ⇒ λ_.[ ([[false;true;false;true;false;false;true;false]]) ; b1 ]
53             | DATA b2 ⇒ λ_. [ ([[false;true;false;true;false;false;true;true]]) ; b1 ; b2 ]
54             | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
55         ]
56      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
57         match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
58          [ BIT_ADDR b1 ⇒ λ_.[ ([[true;false;false;false;false;false;true;false]]) ; b1 ]
59          | N_BIT_ADDR b1 ⇒ λ_. [ ([[true;false;true;true;false;false;false;false]]) ; b1 ]
60          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
61  | CLR 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; false; false; true; false; false]]) ]
65      | CARRY ⇒ λ_.
66         [ ([[true; true; false; false; false; false; true; true]]) ]
67      | BIT_ADDR b1 ⇒ λ_.
68         [ ([[true; true; false; false; false; false; true; false]]) ; b1 ]
69      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
70  | CPL addr ⇒
71     match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with
72      [ ACC_A ⇒ λ_.
73         [ ([[true; true; true; true; false; true; false; false]]) ]
74      | CARRY ⇒ λ_.
75         [ ([[true; false; true; true; false; false; true; true]]) ]
76      | BIT_ADDR b1 ⇒ λ_.
77         [ ([[true; false; true; true; false; false; true; false]]) ; b1 ]
78      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
79  | DA addr ⇒
80     [ ([[true; true; false; true; false; true; false; false]]) ]
81  | DEC addr ⇒
82     match addr return λx. bool_to_Prop (is_in ? [[acc_a;register;direct;indirect]] x) → ? with
83      [ ACC_A ⇒ λ_.
84         [ ([[false; false; false; true; false; true; false; false]]) ]
85      | REGISTER r ⇒ λ_.
86         [ ([[false; false; false; true; true]]) @@ r ]
87      | DIRECT b1 ⇒ λ_.
88         [ ([[false; false; false; true; false; true; false; true]]); b1 ]
89      | INDIRECT i1 ⇒ λ_.
90         [ ([[false; false; false; true; false; true; true; i1]]) ]
91      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
92  | DIV addr1 addr2 ⇒
93     [ ([[true;false;false;false;false;true;false;false]]) ]
94  | Jump j ⇒
95     match j with
96      [ DJNZ addr1 addr2 ⇒
97         let b2 ≝
98          match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
99           [ RELATIVE b2 ⇒ λ_. b2
100           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
101         match addr1 return λx. bool_to_Prop (is_in ? [[register;direct]] x) → ? with
102          [ REGISTER r ⇒ λ_.
103             [ ([[true; true; false; true; true]]) @@ r ; b2 ]
104          | DIRECT b1 ⇒ λ_.
105             [ ([[true; true; false; true; false; true; false; true]]); b1; b2 ]
106          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
107      | JC addr ⇒
108         match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
109          [ RELATIVE b1 ⇒ λ_.
110             [ ([[false; true; false; false; false; false; false; false]]); b1 ]
111          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
112      | JNC addr ⇒
113         match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
114          [ RELATIVE b1 ⇒ λ_.
115             [ ([[false; true; false; true; false; false; false; false]]); b1 ]
116          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
117      | JZ addr ⇒
118         match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
119          [ RELATIVE b1 ⇒ λ_.
120             [ ([[false; true; true; false; false; false; false; false]]); b1 ]
121          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
122      | JNZ addr ⇒
123         match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
124          [ RELATIVE b1 ⇒ λ_.
125             [ ([[false; true; true; true; false; false; false; false]]); b1 ]
126          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
127      | JB addr1 addr2 ⇒
128         let b2 ≝
129          match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
130           [ RELATIVE b2 ⇒ λ_. b2
131           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
132         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
133          [ BIT_ADDR b1 ⇒ λ_.
134             [ ([[false; false; true; false; false; false; false; false]]); b1; b2 ]
135          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
136      | JNB addr1 addr2 ⇒
137         let b2 ≝
138          match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
139           [ RELATIVE b2 ⇒ λ_. b2
140           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
141         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
142          [ BIT_ADDR b1 ⇒ λ_.
143             [ ([[false; false; true; true; false; false; false; false]]); b1; b2 ]
144          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
145      | JBC addr1 addr2 ⇒
146         let b2 ≝
147          match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
148           [ RELATIVE b2 ⇒ λ_. b2
149           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
150         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
151          [ BIT_ADDR b1 ⇒ λ_.
152             [ ([[false; false; false; true; false; false; false; false]]); b1; b2 ]
153          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
154      | CJNE addrs addr3 ⇒
155         let b3 ≝
156          match addr3 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
157           [ RELATIVE b3 ⇒ λ_. b3
158           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr3) in
159         match addrs with
160          [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
161             match addr2 return λx. bool_to_Prop (is_in ? [[direct;data]] x) → ? with
162              [ DIRECT b1 ⇒ λ_.
163                 [ ([[true; false; true; true; false; true; false; true]]); b1; b3 ]
164              | DATA b1 ⇒ λ_.
165                 [ ([[true; false; true; true; false; true; false; false]]); b1; b3 ]
166              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
167          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
168             let b2 ≝
169              match addr2 return λx. bool_to_Prop (is_in ? [[data]] x) → ? with
170               [ DATA b2 ⇒ λ_. b2
171               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
172             match addr1 return λx. bool_to_Prop (is_in ? [[register;indirect]] x) → list Byte with
173              [ REGISTER r⇒ λ_.
174                 [ ([[true; false; true; true; true]]) @@ r; b2; b3 ]
175              | INDIRECT i1 ⇒ λ_.
176                 [ ([[true; false; true; true; false; true; true; i1]]); b2; b3 ]
177              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) ]]
178  | INC addr ⇒
179     match addr return λx. bool_to_Prop (is_in ? [[acc_a;register;direct;indirect;dptr]] x) → ? with
180      [ ACC_A ⇒ λ_.
181         [ ([[false;false;false;false;false;true;false;false]]) ]         
182      | REGISTER r ⇒ λ_.
183         [ ([[false;false;false;false;true]]) @@ r ]
184      | DIRECT b1 ⇒ λ_.
185         [ ([[false; false; false; false; false; true; false; true]]); b1 ]
186      | INDIRECT i1 ⇒ λ_.
187        [ ([[false; false; false; false; false; true; true; i1]]) ]
188      | DPTR ⇒ λ_.
189        [ ([[true;false;true;false;false;false;true;true]]) ]
190      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
191  | JMP addr ⇒
192     [ ([[false;true;true;true;false;false;true;true]]) ]
193  | LCALL addr ⇒
194     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
195      [ ADDR16 w ⇒ λ_.
196         let 〈b1,b2〉 ≝ split ? 8 8 w in
197          [ ([[false;false;false;true;false;false;true;false]]); b1; b2 ]         
198      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
199  | LJMP addr ⇒
200     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
201      [ ADDR16 w ⇒ λ_.
202         let 〈b1,b2〉 ≝ split ? 8 8 w in
203          [ ([[false;false;false;false;false;false;true;false]]); b1; b2 ]         
204      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
205  | MOV addrs ⇒
206     match addrs with
207      [ inl addrs ⇒
208         match addrs with
209          [ inl addrs ⇒
210             match addrs with
211              [ inl addrs ⇒
212                 match addrs with
213                  [ inl addrs ⇒
214                     match addrs with
215                      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
216                         match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
217                          [ REGISTER r ⇒ λ_.[ ([[true;true;true;false;true]]) @@ r ]
218                          | DIRECT b1 ⇒ λ_.[ ([[true;true;true;false;false;true;false;true]]); b1 ]
219                          | INDIRECT i1 ⇒ λ_. [ ([[true;true;true;false;false;true;true;i1]]) ]
220                          | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;false;false]]) ; b1 ]
221                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
222                      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
223                         match addr1 return λx. bool_to_Prop (is_in ? [[register;indirect]] x) → ? with
224                          [ REGISTER r ⇒ λ_.
225                             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with
226                              [ ACC_A ⇒ λ_.[ ([[true;true;true;true;true]]) @@ r ]
227                              | DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;true]]) @@ r; b1 ]
228                              | DATA b1 ⇒ λ_. [ ([[false;true;true;true;true]]) @@ r; b1 ]
229                              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
230                          | INDIRECT i1 ⇒ λ_.
231                             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with
232                              [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;true;i1]]) ]
233                              | DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;false;true;true;i1]]); b1 ]
234                              | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;true;i1]]) ; b1 ]
235                              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
236                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
237                  | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
238                     let b1 ≝
239                      match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
240                       [ DIRECT b1 ⇒ λ_. b1
241                       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
242                     match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;register;direct;indirect;data]] x) → ? with
243                      [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;false;true]]); b1]
244                      | REGISTER r ⇒ λ_.[ ([[true;false;false;false;true]]) @@ r; b1 ]
245                      | DIRECT b2 ⇒ λ_.[ ([[true;false;false;false;false;true;false;true]]); b1; b2 ]
246                      | INDIRECT i1 ⇒ λ_. [ ([[true;false;false;false;false;true;true;i1]]); b1 ]
247                      | DATA b2 ⇒ λ_. [ ([[false;true;true;true;false;true;false;true]]); b1; b2 ]
248                      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
249              | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
250                 match addr2 return λx. bool_to_Prop (is_in ? [[data16]] x) → ? with
251                  [ DATA16 w ⇒ λ_.
252                     let 〈b1,b2〉 ≝ split ? 8 8 w in
253                      [ ([[true;false;false;true;false;false;false;false]]); b1; b2]
254                  | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
255          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
256             match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
257              [ BIT_ADDR b1 ⇒ λ_.
258                 [ ([[true;false;true;false;false;false;true;false]]); b1 ]
259              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
260      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
261         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
262          [ BIT_ADDR b1 ⇒ λ_.
263             [ ([[true;false;false;true;false;false;true;false]]); b1 ]
264          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
265  | MOVC addr1 addr2 ⇒
266     match addr2 return λx. bool_to_Prop (is_in ? [[acc_dptr;acc_pc]] x) → ? with
267      [ ACC_DPTR ⇒ λ_.
268         [ ([[true;false;false;true;false;false;true;true]]) ]
269      | ACC_PC ⇒ λ_.
270         [ ([[true;false;false;false;false;false;true;true]]) ]
271      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
272  | MOVX addrs ⇒
273     match addrs with
274      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
275         match addr2 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
276          [ EXT_INDIRECT i1 ⇒ λ_.
277             [ ([[true;true;true;false;false;false;true;i1]]) ]
278          | EXT_INDIRECT_DPTR ⇒ λ_.
279             [ ([[true;true;true;false;false;false;false;false]]) ]
280          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
281      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
282         match addr1 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
283          [ EXT_INDIRECT i1 ⇒ λ_.
284             [ ([[true;true;true;true;false;false;true;i1]]) ]
285          | EXT_INDIRECT_DPTR ⇒ λ_.
286             [ ([[true;true;true;true;false;false;false;false]]) ]
287          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
288  | MUL addr1 addr2 ⇒
289     [ ([[true;false;true;false;false;true;false;false]]) ]
290  | NOP ⇒
291     [ ([[false;false;false;false;false;false;false;false]]) ]
292  | ORL addrs ⇒
293     match addrs with
294      [ inl addrs ⇒
295         match addrs with
296          [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
297             match addr2 return λx. bool_to_Prop (is_in ? [[register;data;direct;indirect]] x) → ? with
298             [ REGISTER r ⇒ λ_.[ ([[false;true;false;false;true]]) @@ r ]
299             | DIRECT b1 ⇒ λ_.[ ([[false;true;false;false;false;true;false;true]]); b1 ]
300             | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;false;false;true;true;i1]]) ]
301             | DATA b1 ⇒ λ_. [ ([[false;true;false;false;false;true;false;false]]) ; b1 ]
302             | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
303          | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
304            let b1 ≝
305              match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
306               [ DIRECT b1 ⇒ λ_. b1
307               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
308             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
309              [ ACC_A ⇒ λ_.
310                 [ ([[false;true;false;false;false;false;true;false]]); b1 ]
311              | DATA b2 ⇒ λ_.
312                 [ ([[false;true;false;false;false;false;true;true]]); b1; b2 ]
313              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
314      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in     
315         match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
316          [ BIT_ADDR b1 ⇒ λ_.
317             [ ([[false;true;true;true;false;false;true;false]]); b1 ]
318          | N_BIT_ADDR b1 ⇒ λ_.
319             [ ([[true;false;true;false;false;false;false;false]]); b1 ]
320          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
321  | POP addr ⇒
322     match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
323      [ DIRECT b1 ⇒ λ_.
324         [ ([[true;true;false;true;false;false;false;false]]) ; b1 ]
325      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
326  | PUSH addr ⇒
327     match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
328      [ DIRECT b1 ⇒ λ_.
329         [ ([[true;true;false;false;false;false;false;false]]) ; b1 ]
330      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
331  | RET ⇒
332     [ ([[false;false;true;false;false;false;true;false]]) ]
333  | RETI ⇒
334     [ ([[false;false;true;true;false;false;true;false]]) ]
335  | RL addr ⇒
336     [ ([[false;false;true;false;false;false;true;true]]) ]
337  | RLC addr ⇒
338     [ ([[false;false;true;true;false;false;true;true]]) ]
339  | RR addr ⇒
340     [ ([[false;false;false;false;false;false;true;true]]) ]
341  | RRC addr ⇒
342     [ ([[false;false;false;true;false;false;true;true]]) ]
343  | SETB addr ⇒     
344     match addr return λx. bool_to_Prop (is_in ? [[carry;bit_addr]] x) → ? with
345      [ CARRY ⇒ λ_.
346         [ ([[true;true;false;true;false;false;true;true]]) ]
347      | BIT_ADDR b1 ⇒ λ_.
348         [ ([[true;true;false;true;false;false;true;false]]); b1 ]
349      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
350  | SJMP addr ⇒
351     match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
352      [ RELATIVE b1 ⇒ λ_.
353         [ ([[true;false;false;false;false;false;false;false]]); b1 ]
354      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
355  | SUBB addr1 addr2 ⇒
356     match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
357      [ REGISTER r ⇒ λ_.
358         [ ([[true;false;false;true;true]]) @@ r ]
359      | DIRECT b1 ⇒ λ_.
360         [ ([[true;false;false;true;false;true;false;true]]); b1]
361      | INDIRECT i1 ⇒ λ_.
362         [ ([[true;false;false;true;false;true;true;i1]]) ]
363      | DATA b1 ⇒ λ_.
364         [ ([[true;false;false;true;false;true;false;false]]); b1]
365      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
366  | SWAP addr ⇒
367     [ ([[true;true;false;false;false;true;false;false]]) ]
368  | XCH addr1 addr2 ⇒
369     match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect]] x) → ? with
370      [ REGISTER r ⇒ λ_.
371         [ ([[true;true;false;false;true]]) @@ r ]
372      | DIRECT b1 ⇒ λ_.
373         [ ([[true;true;false;false;false;true;false;true]]); b1]
374      | INDIRECT i1 ⇒ λ_.
375         [ ([[true;true;false;false;false;true;true;i1]]) ]
376      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
377  | XCHD addr1 addr2 ⇒
378     match addr2 return λx. bool_to_Prop (is_in ? [[indirect]] x) → ? with
379      [ INDIRECT i1 ⇒ λ_.
380         [ ([[true;true;false;true;false;true;true;i1]]) ]
381      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
382  | XRL addrs ⇒
383     match addrs with
384      [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
385         match addr2 return λx. bool_to_Prop (is_in ? [[data;register;direct;indirect]] x) → ? with
386          [ REGISTER r ⇒ λ_.
387             [ ([[false;true;true;false;true]]) @@ r ]
388          | DIRECT b1 ⇒ λ_.
389             [ ([[false;true;true;false;false;true;false;true]]); b1]
390          | INDIRECT i1 ⇒ λ_.
391             [ ([[false;true;true;false;false;true;true;i1]]) ]
392          | DATA b1 ⇒ λ_.
393             [ ([[false;true;true;false;false;true;false;false]]); b1]
394          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
395      | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
396         let b1 ≝
397          match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
398           [ DIRECT b1 ⇒ λ_. b1
399           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
400         match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
401          [ ACC_A ⇒ λ_.
402             [ ([[false;true;true;false;false;false;true;false]]); b1 ]         
403          | DATA b2 ⇒ λ_.
404             [ ([[false;true;true;false;false;false;true;true]]); b1; b2 ]
405          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]].
406         
407definition assembly_jump: (jump Identifier) → (Identifier → [[relative]]) → instruction ≝
408  λj: jump Identifier.
409  λaddr_of: Identifier → [[relative]].
410    match j with
411      [ JC jmp ⇒ Jump ? (JC ? (addr_of jmp))
412      | JNC jmp ⇒ Jump ? (JNC ? (addr_of jmp))
413      | JZ jmp ⇒ Jump ? (JZ ? (addr_of jmp))
414      | JNZ jmp ⇒ Jump ? (JNZ ? (addr_of jmp))
415      | JB jmp jmp' ⇒ Jump ? (JB ? jmp (addr_of jmp'))
416      | JNB jmp jmp' ⇒ Jump ? (JNB ? jmp (addr_of jmp'))
417      | JBC jmp jmp' ⇒ Jump ? (JBC ? jmp (addr_of jmp'))
418      | CJNE jmp jmp' ⇒ Jump ? (CJNE ? jmp (addr_of jmp'))
419      | DJNZ jmp jmp' ⇒ Jump ? (DJNZ ? jmp (addr_of jmp'))
420      ].
421
422definition address_of: BitVectorTrie Word 16 → Identifier → addressing_mode ≝
423    λmap.
424    λid: Identifier.
425      let address ≝ lookup … id map (zero ?) in
426      let 〈high, low〉 ≝ split ? 8 8 address in
427      if eq_bv ? high (zero ?) then
428        RELATIVE low
429      else
430        ?.
431      elim not_implemented.
432qed.
433
434definition assembly: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
435  λp.
436    let 〈preamble, instr_list〉 ≝ p in
437    let 〈datalabels, ignore〉 ≝
438      foldl ((BitVectorTrie Identifier 16) × nat) ? (
439        λt. λpreamble.
440          let 〈datalabels, addr〉 ≝ t in
441          let 〈name, size〉 ≝ preamble in
442          let addr_16 ≝ bitvector_of_nat 16 addr in
443            〈insert ? ? name addr_16 datalabels, addr + size〉)
444              〈(Stub ? ?), 0〉 preamble in
445    let 〈labels,pc_costs〉 ≝
446      foldl ((BitVectorTrie ? ?) × (nat  × (BitVectorTrie ? ?))) ? (
447        λt. λi.
448          let 〈label, i〉 ≝ i in
449          let 〈labels, pc_costs〉 ≝ t in
450          let 〈program_counter, costs〉 ≝ pc_costs in
451          let labels ≝ match label with
452          [ None ⇒ labels
453          | Some label ⇒
454            let program_counter_bv ≝ bitvector_of_nat ? program_counter in
455              insert ? ? label program_counter_bv labels
456          ] in
457          〈labels,
458            match i with
459              [ Instruction instr ⇒
460                let code_memory ≝ load_code_memory (assembly1 instr) in
461                let 〈instr_pc', ignore〉 ≝ fetch code_memory (zero 16) in
462                let 〈instr', program_counter'〉 ≝ instr_pc' in
463                let program_counter_n' ≝ nat_of_bitvector ? program_counter' in
464                  〈program_counter + program_counter_n', costs〉
465              | Comment comment ⇒ 〈program_counter, costs〉
466              | Cost cost ⇒
467                let program_counter_bv ≝ bitvector_of_nat ? program_counter in
468                  〈program_counter, (insert ? ? program_counter_bv cost costs)〉
469              | Jmp jmp ⇒
470                  〈program_counter + 3, costs〉
471              | Call call ⇒
472                  〈program_counter + 3, costs〉
473              | Mov dptr trgt ⇒ pc_costs
474              | WithLabel jmp ⇒
475                let fake_addr ≝ RELATIVE (zero 8) in
476                let fake_jump ≝ assembly_jump jmp (λx: Identifier. fake_addr) in
477                let code_memory ≝ load_code_memory (assembly1 fake_jump) in
478                let 〈instr_pc', ignore〉 ≝ fetch code_memory (zero 16) in
479                let 〈instr', program_counter'〉 ≝ instr_pc' in
480                let program_counter_n' ≝ nat_of_bitvector 16 program_counter' in
481                  〈program_counter + program_counter_n', costs〉
482              ]〉
483          ) 〈(Stub ? ?), 〈0,(Stub ? ?)〉〉 instr_list in
484    let 〈program_counter, costs〉 ≝ pc_costs in
485      if gtb program_counter (2^16) then (* 65536 *)
486        None ?
487      else
488        let flat_list ≝
489          flatten ? (
490            map ? ? (
491              λi: labelled_instruction.
492                match \snd i with
493                  [ Cost cost ⇒ [ ]
494                  | Comment comment ⇒ [ ]
495                  | Call call ⇒
496                    let pc_offset ≝ lookup ? ? call labels (zero ?) in
497                    let address ≝ ADDR16 pc_offset in
498                      assembly1 (LCALL ? address)
499                  | Mov d trgt ⇒
500                    let pc_offset ≝ lookup ? ? trgt datalabels (zero ?) in
501                    let address ≝ DATA16 pc_offset in
502                      assembly1 (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉))))
503                  | Instruction instr ⇒ assembly1 instr
504                  | Jmp jmp ⇒
505                    let pc_offset ≝ lookup ? ? jmp labels (zero ?) in
506                    let address ≝ ADDR16 pc_offset in
507                      assembly1 (LJMP ? address)
508                  | WithLabel jmp ⇒ assembly1 (assembly_jump jmp (address_of labels))
509                  ]
510            ) instr_list
511          ) in
512        Some (list ? × (BitVectorTrie ? ?)) 〈flat_list, costs〉.
513  [2,3,4,5,6:
514    normalize; %;
515  | whd in ⊢ (? (? ? ? %));
516      cases (split bool 8 8 (lookup Word 16 c0 labels (zero 16)))
517      # high
518      # low
519      whd in ⊢ (? (? ? ? %))
520      cases (eq_bv 8 high (zero 8))
521      [ normalize
522        %
523      | elim not_implemented;
524      ]
525  ]
526qed.
527
528definition assembly_unlabelled_program: list instruction → option (list Byte × (BitVectorTrie Identifier 16)) ≝
529 λp. Some ? (〈foldr ? ? (λi,l. assembly1 i @ l) [ ] p, Stub …〉).
530
Note: See TracBrowser for help on using the repository browser.