source: Deliverables/D4.1/Matita/Assembly.ma @ 358

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

A simple version of assembly (no labels) implemented.
File size: 26.3 KB
Line 
1include "ASM.ma".
2
3ndefinition assembly1 ≝
4 λi: instruction.match i with
5  [ ACALL addr ⇒
6     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
7      [ ADDR11 w ⇒ λ_.
8         let 〈v1,v2〉 ≝ split ? (S (S (S Z))) (S (S (S (S (S (S (S (S Z)))))))) w in
9          [ (v1 @@ [[true; false; false; false; true]]) ; v2 ]
10      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
11  | ADD addr1 addr2 ⇒
12     match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
13      [ REGISTER r ⇒ λ_.[ ([[false;false;true;false;true]]) @@ r ]
14      | DIRECT b1 ⇒ λ_.[ ([[false;false;true;false;false;true;false;true]]); b1 ]
15      | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;false;false;true;true;i1]]) ]
16      | DATA b1 ⇒ λ_. [ ([[false;false;true;false;false;true;false;false]]) ; b1 ]
17      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
18  | ADDC addr1 addr2 ⇒
19     match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
20      [ REGISTER r ⇒ λ_.[ ([[false;false;true;true;true]]) @@ r ]
21      | DIRECT b1 ⇒ λ_.[ ([[false;false;true;true;false;true;false;true]]); b1 ]
22      | INDIRECT i1 ⇒ λ_. [ ([[false;false;true;true;false;true;true;i1]]) ]
23      | DATA b1 ⇒ λ_. [ ([[false;false;true;true;false;true;false;false]]) ; b1 ]
24      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
25  | AJMP addr ⇒
26     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
27      [ ADDR11 w ⇒ λ_.
28         let 〈v1,v2〉 ≝ split ?  (S (S (S Z))) (S (S (S (S (S (S (S (S Z)))))))) w in
29          [ (v1 @@ [[false; false; false; false; true]]) ; v2 ]
30      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
31  | ANL addrs ⇒
32     match addrs with
33      [ Left addrs ⇒ match addrs with
34         [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
35           match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
36            [ REGISTER r ⇒ λ_.[ ([[false;true;false;true;true]]) @@ r ]
37            | DIRECT b1 ⇒ λ_.[ ([[false;true;false;true;false;true;false;true]]); b1 ]
38            | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;true;false;true;true;i1]]) ]
39            | DATA b1 ⇒ λ_. [ ([[false;true;false;true;false;true;false;false]]) ; b1 ]
40            | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
41         | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
42            let b1 ≝
43             match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
44              [ DIRECT b1 ⇒ λ_.b1
45              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
46            match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
47             [ ACC_A ⇒ λ_.[ ([[false;true;false;true;false;false;true;false]]) ; b1 ]
48             | DATA b2 ⇒ λ_. [ ([[false;true;false;true;false;false;true;true]]) ; b1 ; b2 ]
49             | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
50         ]
51      | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
52         match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
53          [ BIT_ADDR b1 ⇒ λ_.[ ([[true;false;false;false;false;false;true;false]]) ; b1 ]
54          | N_BIT_ADDR b1 ⇒ λ_. [ ([[true;false;true;true;false;false;false;false]]) ; b1 ]
55          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
56  | CLR addr ⇒
57     match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with
58      [ ACC_A ⇒ λ_.
59         [ ([[true; true; true; false; false; true; false; false]]) ]
60      | CARRY ⇒ λ_.
61         [ ([[true; true; false; false; false; false; true; true]]) ]
62      | BIT_ADDR b1 ⇒ λ_.
63         [ ([[true; true; false; false; false; false; true; false]]) ; b1 ]
64      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
65  | CPL addr ⇒
66     match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with
67      [ ACC_A ⇒ λ_.
68         [ ([[true; true; true; true; false; true; false; false]]) ]
69      | CARRY ⇒ λ_.
70         [ ([[true; false; true; true; false; false; true; true]]) ]
71      | BIT_ADDR b1 ⇒ λ_.
72         [ ([[true; false; true; true; false; false; true; false]]) ; b1 ]
73      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
74  | DA addr ⇒
75     [ ([[true; true; false; true; false; true; false; false]]) ]
76  | DEC addr ⇒
77     match addr return λx. bool_to_Prop (is_in ? [[acc_a;register;direct;indirect]] x) → ? with
78      [ ACC_A ⇒ λ_.
79         [ ([[false; false; false; true; false; true; false; false]]) ]
80      | REGISTER r ⇒ λ_.
81         [ ([[false; false; false; true; true]]) @@ r ]
82      | DIRECT b1 ⇒ λ_.
83         [ ([[false; false; false; true; false; true; false; true]]); b1 ]
84      | INDIRECT i1 ⇒ λ_.
85         [ ([[false; false; false; true; false; true; true; i1]]) ]
86      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
87  | DIV addr1 addr2 ⇒
88     [ ([[true;false;false;false;false;true;false;false]]) ]
89  | Jump j ⇒
90     match j with
91      [ DJNZ addr1 addr2 ⇒
92         let b2 ≝
93          match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
94           [ RELATIVE b2 ⇒ λ_. b2
95           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
96         match addr1 return λx. bool_to_Prop (is_in ? [[register;direct]] x) → ? with
97          [ REGISTER r ⇒ λ_.
98             [ ([[true; true; false; true; true]]) @@ r ; b2 ]
99          | DIRECT b1 ⇒ λ_.
100             [ ([[true; true; false; true; false; true; false; true]]); b1; b2 ]
101          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
102      | JC addr ⇒
103         match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
104          [ RELATIVE b1 ⇒ λ_.
105             [ ([[false; true; false; false; false; false; false; false]]); b1 ]
106          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
107      | JNC addr ⇒
108         match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
109          [ RELATIVE b1 ⇒ λ_.
110             [ ([[false; true; false; true; false; false; false; false]]); b1 ]
111          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
112      | JZ addr ⇒
113         match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
114          [ RELATIVE b1 ⇒ λ_.
115             [ ([[false; true; true; false; false; false; false; false]]); b1 ]
116          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
117      | JNZ addr ⇒
118         match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
119          [ RELATIVE b1 ⇒ λ_.
120             [ ([[false; true; true; true; false; false; false; false]]); b1 ]
121          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
122      | JB addr1 addr2 ⇒
123         let b2 ≝
124          match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
125           [ RELATIVE b2 ⇒ λ_. b2
126           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
127         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
128          [ BIT_ADDR b1 ⇒ λ_.
129             [ ([[false; false; true; false; false; false; false; false]]); b1; b2 ]
130          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
131      | JNB addr1 addr2 ⇒
132         let b2 ≝
133          match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
134           [ RELATIVE b2 ⇒ λ_. b2
135           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
136         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
137          [ BIT_ADDR b1 ⇒ λ_.
138             [ ([[false; false; true; true; false; false; false; false]]); b1; b2 ]
139          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
140      | JBC addr1 addr2 ⇒
141         let b2 ≝
142          match addr2 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
143           [ RELATIVE b2 ⇒ λ_. b2
144           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
145         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
146          [ BIT_ADDR b1 ⇒ λ_.
147             [ ([[false; false; false; true; false; false; false; false]]); b1; b2 ]
148          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)
149      | CJNE addrs addr3 ⇒
150         let b3 ≝
151          match addr3 return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
152           [ RELATIVE b3 ⇒ λ_. b3
153           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr3) in
154         match addrs with
155          [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
156             match addr2 return λx. bool_to_Prop (is_in ? [[direct;data]] x) → ? with
157              [ DIRECT b1 ⇒ λ_.
158                 [ ([[true; false; true; true; false; true; false; true]]); b1; b3 ]
159              | DATA b1 ⇒ λ_.
160                 [ ([[true; false; true; true; false; true; false; false]]); b1; b3 ]
161              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
162          | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
163             let b2 ≝
164              match addr2 return λx. bool_to_Prop (is_in ? [[data]] x) → ? with
165               [ DATA b2 ⇒ λ_. b2
166               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
167             match addr1 return λx. bool_to_Prop (is_in ? [[register;indirect]] x) → List Byte with
168              [ REGISTER r⇒ λ_.
169                 [ ([[true; false; true; true; true]]) @@ r; b2; b3 ]
170              | INDIRECT i1 ⇒ λ_.
171                 [ ([[true; false; true; true; false; true; true; i1]]); b2; b3 ]
172              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) ]]
173  | INC addr ⇒
174     match addr return λx. bool_to_Prop (is_in ? [[acc_a;register;direct;indirect;dptr]] x) → ? with
175      [ ACC_A ⇒ λ_.
176         [ ([[false;false;false;false;false;true;false;false]]) ]         
177      | REGISTER r ⇒ λ_.
178         [ ([[false;false;false;false;true]]) @@ r ]
179      | DIRECT b1 ⇒ λ_.
180         [ ([[false; false; false; false; false; true; false; true]]); b1 ]
181      | INDIRECT i1 ⇒ λ_.
182        [ ([[false; false; false; false; false; true; true; i1]]) ]
183      | DPTR ⇒ λ_.
184        [ ([[true;false;true;false;false;false;true;true]]) ]
185      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
186  | JMP addr ⇒
187     [ ([[false;true;true;true;false;false;true;true]]) ]
188  | LCALL addr ⇒
189     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
190      [ ADDR16 w ⇒ λ_.
191         let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S (S (S (S (S (S Z)))))))) w in
192          [ ([[false;false;false;true;false;false;true;false]]); b1; b2 ]         
193      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
194  | LJMP addr ⇒
195     match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with
196      [ ADDR16 w ⇒ λ_.
197         let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S (S (S (S (S (S Z)))))))) w in
198          [ ([[false;false;false;false;false;false;true;false]]); b1; b2 ]         
199      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
200  | MOV addrs ⇒
201     match addrs with
202      [ Left addrs ⇒
203         match addrs with
204          [ Left addrs ⇒
205             match addrs with
206              [ Left addrs ⇒
207                 match addrs with
208                  [ Left addrs ⇒
209                     match addrs with
210                      [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
211                         match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
212                          [ REGISTER r ⇒ λ_.[ ([[true;true;true;false;true]]) @@ r ]
213                          | DIRECT b1 ⇒ λ_.[ ([[true;true;true;false;false;true;false;true]]); b1 ]
214                          | INDIRECT i1 ⇒ λ_. [ ([[true;true;true;false;false;true;true;i1]]) ]
215                          | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;false;false]]) ; b1 ]
216                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
217                      | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
218                         match addr1 return λx. bool_to_Prop (is_in ? [[register;indirect]] x) → ? with
219                          [ REGISTER r ⇒ λ_.
220                             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with
221                              [ ACC_A ⇒ λ_.[ ([[true;true;true;true;true]]) @@ r ]
222                              | DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;true]]) @@ r; b1 ]
223                              | DATA b1 ⇒ λ_. [ ([[false;true;true;true;true]]) @@ r; b1 ]
224                              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
225                          | INDIRECT i1 ⇒ λ_.
226                             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;direct;data]] x) → ? with
227                              [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;true;i1]]) ]
228                              | DIRECT b1 ⇒ λ_.[ ([[true;false;true;false;false;true;true;i1]]); b1 ]
229                              | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;true;i1]]) ; b1 ]
230                              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
231                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
232                  | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
233                     let b1 ≝
234                      match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
235                       [ DIRECT b1 ⇒ λ_. b1
236                       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
237                     match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;register;direct;indirect;data]] x) → ? with
238                      [ ACC_A ⇒ λ_.[ ([[true;true;true;true;false;true;false;true]]); b1]
239                      | REGISTER r ⇒ λ_.[ ([[true;false;false;false;true]]) @@ r; b1 ]
240                      | DIRECT b2 ⇒ λ_.[ ([[true;false;false;false;false;true;false;true]]); b1; b2 ]
241                      | INDIRECT i1 ⇒ λ_. [ ([[true;false;false;false;false;true;true;i1]]); b1 ]
242                      | DATA b2 ⇒ λ_. [ ([[false;true;true;true;false;true;false;true]]); b1; b2 ]
243                      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
244              | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
245                 match addr2 return λx. bool_to_Prop (is_in ? [[data16]] x) → ? with
246                  [ DATA16 w ⇒ λ_.
247                     let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S (S (S (S (S (S Z)))))))) w in
248                      [ ([[true;false;false;true;false;false;false;false]]); b1; b2]
249                  | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
250          | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
251             match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
252              [ BIT_ADDR b1 ⇒ λ_.
253                 [ ([[true;false;true;false;false;false;true;false]]); b1 ]
254              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
255      | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
256         match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with
257          [ BIT_ADDR b1 ⇒ λ_.
258             [ ([[true;false;false;true;false;false;true;false]]); b1 ]
259          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
260  | MOVC addr1 addr2 ⇒
261     match addr2 return λx. bool_to_Prop (is_in ? [[acc_dptr;acc_pc]] x) → ? with
262      [ ACC_DPTR ⇒ λ_.
263         [ ([[true;false;false;true;false;false;true;true]]) ]
264      | ACC_PC ⇒ λ_.
265         [ ([[true;false;false;false;false;false;true;true]]) ]
266      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
267  | MOVX addrs ⇒
268     match addrs with
269      [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
270         match addr2 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
271          [ EXT_INDIRECT i1 ⇒ λ_.
272             [ ([[true;true;true;false;false;false;true;i1]]) ]
273          | EXT_INDIRECT_DPTR ⇒ λ_.
274             [ ([[true;true;true;false;false;false;false;false]]) ]
275          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
276      | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
277         match addr1 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with
278          [ EXT_INDIRECT i1 ⇒ λ_.
279             [ ([[true;true;true;true;false;false;true;i1]]) ]
280          | EXT_INDIRECT_DPTR ⇒ λ_.
281             [ ([[true;true;true;true;false;false;false;false]]) ]
282          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
283  | MUL addr1 addr2 ⇒
284     [ ([[true;false;true;false;false;true;false;false]]) ]
285  | NOP ⇒
286     [ ([[false;false;false;false;false;false;false;false]]) ]
287  | ORL addrs ⇒
288     match addrs with
289      [ Left addrs ⇒
290         match addrs with
291          [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
292             match addr2 return λx. bool_to_Prop (is_in ? [[register;data;direct;indirect]] x) → ? with
293             [ REGISTER r ⇒ λ_.[ ([[false;true;false;false;true]]) @@ r ]
294             | DIRECT b1 ⇒ λ_.[ ([[false;true;false;false;false;true;false;true]]); b1 ]
295             | INDIRECT i1 ⇒ λ_. [ ([[false;true;false;false;false;true;true;i1]]) ]
296             | DATA b1 ⇒ λ_. [ ([[false;true;false;false;false;true;false;false]]) ; b1 ]
297             | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
298          | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
299            let b1 ≝
300              match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
301               [ DIRECT b1 ⇒ λ_. b1
302               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
303             match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
304              [ ACC_A ⇒ λ_.
305                 [ ([[false;true;false;false;false;false;true;false]]); b1 ]
306              | DATA b2 ⇒ λ_.
307                 [ ([[false;true;false;false;false;false;true;true]]); b1; b2 ]
308              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
309      | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in     
310         match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
311          [ BIT_ADDR b1 ⇒ λ_.
312             [ ([[false;true;true;true;false;false;true;false]]); b1 ]
313          | N_BIT_ADDR b1 ⇒ λ_.
314             [ ([[true;false;true;false;false;false;false;false]]); b1 ]
315          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
316  | POP addr ⇒
317     match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
318      [ DIRECT b1 ⇒ λ_.
319         [ ([[true;true;false;true;false;false;false;false]]) ; b1 ]
320      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
321  | PUSH addr ⇒
322     match addr return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
323      [ DIRECT b1 ⇒ λ_.
324         [ ([[true;true;false;false;false;false;false;false]]) ; b1 ]
325      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
326  | RET ⇒
327     [ ([[false;false;true;false;false;false;true;false]]) ]
328  | RETI ⇒
329     [ ([[false;false;true;true;false;false;true;false]]) ]
330  | RL addr ⇒
331     [ ([[false;false;true;false;false;false;true;true]]) ]
332  | RLC addr ⇒
333     [ ([[false;false;true;true;false;false;true;true]]) ]
334  | RR addr ⇒
335     [ ([[false;false;false;false;false;false;true;true]]) ]
336  | RRC addr ⇒
337     [ ([[false;false;false;true;false;false;true;true]]) ]
338  | SETB addr ⇒     
339     match addr return λx. bool_to_Prop (is_in ? [[carry;bit_addr]] x) → ? with
340      [ CARRY ⇒ λ_.
341         [ ([[true;true;false;true;false;false;true;true]]) ]
342      | BIT_ADDR b1 ⇒ λ_.
343         [ ([[true;true;false;true;false;false;true;false]]); b1 ]
344      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
345  | SJMP addr ⇒
346     match addr return λx. bool_to_Prop (is_in ? [[relative]] x) → ? with
347      [ RELATIVE b1 ⇒ λ_.
348         [ ([[true;false;false;false;false;false;false;false]]); b1 ]
349      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
350  | SUBB addr1 addr2 ⇒
351     match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with
352      [ REGISTER r ⇒ λ_.
353         [ ([[true;false;false;true;true]]) @@ r ]
354      | DIRECT b1 ⇒ λ_.
355         [ ([[true;false;false;true;false;true;false;true]]); b1]
356      | INDIRECT i1 ⇒ λ_.
357         [ ([[true;false;false;true;false;true;true;i1]]) ]
358      | DATA b1 ⇒ λ_.
359         [ ([[true;false;false;true;false;true;false;false]]); b1]
360      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
361  | SWAP addr ⇒
362     [ ([[true;true;false;false;false;true;false;false]]) ]
363  | XCH addr1 addr2 ⇒
364     match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect]] x) → ? with
365      [ REGISTER r ⇒ λ_.
366         [ ([[true;true;false;false;true]]) @@ r ]
367      | DIRECT b1 ⇒ λ_.
368         [ ([[true;true;false;false;false;true;false;true]]); b1]
369      | INDIRECT i1 ⇒ λ_.
370         [ ([[true;true;false;false;false;true;true;i1]]) ]
371      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
372  | XCHD addr1 addr2 ⇒
373     match addr2 return λx. bool_to_Prop (is_in ? [[indirect]] x) → ? with
374      [ INDIRECT i1 ⇒ λ_.
375         [ ([[true;true;false;true;false;true;true;i1]]) ]
376      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
377  | XRL addrs ⇒
378     match addrs with
379      [ Left addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
380         match addr2 return λx. bool_to_Prop (is_in ? [[data;register;direct;indirect]] x) → ? with
381          [ REGISTER r ⇒ λ_.
382             [ ([[false;true;true;false;true]]) @@ r ]
383          | DIRECT b1 ⇒ λ_.
384             [ ([[false;true;true;false;false;true;false;true]]); b1]
385          | INDIRECT i1 ⇒ λ_.
386             [ ([[false;true;true;false;false;true;true;i1]]) ]
387          | DATA b1 ⇒ λ_.
388             [ ([[false;true;true;false;false;true;false;false]]); b1]
389          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
390      | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
391         let b1 ≝
392          match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
393           [ DIRECT b1 ⇒ λ_. b1
394           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) in
395         match addr2 return λx. bool_to_Prop (is_in ? [[acc_a;data]] x) → ? with
396          [ ACC_A ⇒ λ_.
397             [ ([[false;true;true;false;false;false;true;false]]); b1 ]         
398          | DATA b2 ⇒ λ_.
399             [ ([[false;true;true;false;false;false;true;true]]); b1; b2 ]
400          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]].
401
402(*
403let load_code_memory = fold_lefti (fun i mem v -> WordMap.add (vect_of_int i `Sixteen) v mem) WordMap.empty
404
405let load_mem mem status = { status with code_memory = mem }
406let load l = load_mem (load_code_memory l)
407
408module StringMap = Map.Make(String);;
409module IntMap = Map.Make(struct type t = int let compare = compare end);;
410
411
412let assembly_jump addr_of =
413 function
414    `JC a1 -> `JC (addr_of a1)
415  | `JNC a1 -> `JNC (addr_of a1)
416  | `JB (a1,a2) -> `JB (a1,addr_of a2)
417  | `JNB (a1,a2) -> `JNB (a1,addr_of a2)
418  | `JBC (a1,a2) -> `JBC (a1,addr_of a2)
419  | `JZ a1 -> `JZ (addr_of a1)
420  | `JNZ a1 -> `JNZ (addr_of a1)
421  | `CJNE (a1,a2) -> `CJNE (a1,addr_of a2)
422  | `DJNZ (a1,a2) -> `DJNZ (a1,addr_of a2)
423;;
424
425let assembly (preamble,l) =
426 let datalabels,_ =
427  List.fold_left
428   (fun (datalabels,addr) (name,size) ->
429     let addr16 = vect_of_int addr `Sixteen in
430      StringMap.add name addr16 datalabels, addr+size
431   ) (StringMap.empty,0) preamble
432 in
433 let pc,labels,costs =
434  List.fold_left
435   (fun (pc,labels,costs) i ->
436     match i with
437        `Label s -> pc, StringMap.add s pc labels, costs
438      | `Cost s -> pc, labels, IntMap.add pc s costs
439      | `Mov (_,_) -> pc, labels, costs
440      | `Jmp _
441      | `Call _ -> pc + 3, labels, costs  (*CSC: very stupid: always expand to worst opcode *)
442      | `WithLabel i ->
443          let fake_addr _ = `REL (zero `Eight) in
444          let fake_jump = assembly_jump fake_addr i in
445          let i',pc',_ = fetch (load_code_memory (assembly1 fake_jump)) (vect_of_int 0 `Sixteen) in
446           assert (fake_jump = i');
447           (pc + int_of_vect pc',labels, costs)
448      | #instruction as i ->
449        let i',pc',_ = fetch (load_code_memory (assembly1 i)) (vect_of_int 0 `Sixteen) in
450         assert (i = i');
451         (pc + int_of_vect pc',labels, costs)
452   ) (0,StringMap.empty,IntMap.empty) l
453 in
454  if pc >= 65536 then
455   raise CodeTooLarge
456  else
457      List.flatten (List.map
458         (function
459            `Label _
460          | `Cost _ -> []
461          | `WithLabel i ->
462              let addr_of (`Label s) =
463               let addr = StringMap.find s labels in
464               (* NOT IMPLEMENTED YET; NEEDS SMART ALGORITHM *)
465                assert (addr < 256);
466                `REL (vect_of_int addr `Eight)
467              in
468               assembly1 (assembly_jump addr_of i)
469          | `Mov (`DPTR,s) ->
470              let addrr16 = StringMap.find s datalabels in
471               assembly1 (`MOV (`U4 (`DPTR,`DATA16 addrr16)))
472          | `Jmp s ->
473              let pc_offset = StringMap.find s labels in
474                assembly1 (`LJMP (`ADDR16 (vect_of_int pc_offset `Sixteen)))
475          | `Call s ->
476              let pc_offset = StringMap.find s labels in
477                assembly1 (`LCALL (`ADDR16 (vect_of_int pc_offset `Sixteen)))
478          | #instruction as i -> assembly1 i) l), costs
479;;
480*)
481
482ndefinition assembly: List instruction → List Byte ≝
483 fold_right … (λi,l. assembly1 i @ l) [].
Note: See TracBrowser for help on using the repository browser.