source: src/ASM/Assembly.ma @ 762

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

Lots more fixing to get both front and backends using same conventions and types.

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 ? [[registr;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 ? [[registr;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 ? [[registr;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;registr;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 ? [[registr;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 ? [[registr;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;registr;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 ? [[registr;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 ? [[registr;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;registr;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 ? [[registr;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 ? [[registr;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 ? [[registr;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;registr;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.