1 | include "ASM/ASM.ma". |
---|
2 | include "ASM/Arithmetic.ma". |
---|
3 | |
---|
4 | let rec find_largest_identifier |
---|
5 | (default: Identifier) (the_list: list Identifier) |
---|
6 | on the_list: Identifier ≝ |
---|
7 | match the_list with |
---|
8 | [ nil ⇒ default |
---|
9 | | cons hd tl ⇒ |
---|
10 | match lt_u … hd default with |
---|
11 | [ true ⇒ find_largest_identifier default tl |
---|
12 | | false ⇒ find_largest_identifier hd tl |
---|
13 | ] |
---|
14 | ]. |
---|
15 | |
---|
16 | (* -------------------------------------------------------------------------- *) |
---|
17 | (* Supplies for generating fresh identifiers, in order to effect the global *) |
---|
18 | (* renaming. *) |
---|
19 | (* -------------------------------------------------------------------------- *) |
---|
20 | |
---|
21 | record identifier_supply: Type[0] ≝ |
---|
22 | { |
---|
23 | next: Identifier |
---|
24 | }. |
---|
25 | |
---|
26 | definition create_identifier_supply: list Identifier → identifier_supply ≝ |
---|
27 | λthe_list. |
---|
28 | let maximum ≝ find_largest_identifier (zero …) the_list in |
---|
29 | let incremented ≝ increment … maximum in |
---|
30 | mk_identifier_supply incremented. |
---|
31 | |
---|
32 | definition fresh_identifier: identifier_supply → (identifier_supply × Identifier) ≝ |
---|
33 | λsupply. |
---|
34 | let fresh ≝ next supply in |
---|
35 | let new_supply ≝ mk_identifier_supply (increment … fresh) in |
---|
36 | 〈new_supply, fresh〉. |
---|
37 | |
---|
38 | (* -------------------------------------------------------------------------- *) |
---|
39 | (* Identify all identifiers in a labelled program. *) |
---|
40 | (* -------------------------------------------------------------------------- *) |
---|
41 | |
---|
42 | definition identifiers_of_labelled_program: list (labelled_instruction) → list Identifier ≝ |
---|
43 | λprogram. |
---|
44 | foldr … (λlabel_instruction. λaccum. |
---|
45 | let 〈label, instruction〉 ≝ label_instruction in |
---|
46 | match label with |
---|
47 | [ None ⇒ accum |
---|
48 | | Some label ⇒ label :: accum |
---|
49 | ] |
---|
50 | ) [ ] program. |
---|
51 | |
---|
52 | (* -------------------------------------------------------------------------- *) |
---|
53 | (* Rename the labels in a single pseudo instruction (and preinstructions. We *) |
---|
54 | (* take a list of lists of identifiers, the inner list of identifiers must *) |
---|
55 | (* all be renamed to the same fresh label. We also take an identifier supply *) |
---|
56 | (* for generating fresh identifiers. *) |
---|
57 | (* We give back a list of pairs of lists of identifiers with optional *) |
---|
58 | (* identifiers. If any identifier in the inner list of identifiers given to *) |
---|
59 | (* this function is renamed to something fresh, we return that fresh *) |
---|
60 | (* identifier wrapped in an option type paired with the list input to the *) |
---|
61 | (* function. This information is used when renaming the second part of the *) |
---|
62 | (* labelled instruction, to ensure consistency amongst renamings. *) |
---|
63 | (* -------------------------------------------------------------------------- *) |
---|
64 | |
---|
65 | definition lift_renamings_to_empty_initial_mappings: |
---|
66 | list (list Identifier) → list (list Identifier × (option Identifier)) ≝ |
---|
67 | λrenamings. |
---|
68 | map … (λeq_class. 〈eq_class, None …〉) renamings. |
---|
69 | |
---|
70 | let rec should_be_renamed |
---|
71 | (ident: Identifier) (the_list: (list (list Identifier × (option Identifier)))) |
---|
72 | on the_list: bool ≝ |
---|
73 | match the_list with |
---|
74 | [ nil ⇒ false |
---|
75 | | cons hd tl ⇒ |
---|
76 | match member … (eq_bv …) ident (\fst hd) with |
---|
77 | [ true ⇒ true |
---|
78 | | false ⇒ should_be_renamed ident tl |
---|
79 | ] |
---|
80 | ]. |
---|
81 | |
---|
82 | let rec get_previous_renaming |
---|
83 | (label: Identifier) (initial_mapping: (list (list Identifier × (option Identifier)))) |
---|
84 | on initial_mapping: option Identifier ≝ |
---|
85 | match initial_mapping with |
---|
86 | [ nil ⇒ None … |
---|
87 | | cons hd tl ⇒ |
---|
88 | let 〈class, renaming〉 ≝ hd in |
---|
89 | match member … (eq_bv …) label class with |
---|
90 | [ true ⇒ renaming |
---|
91 | | false ⇒ get_previous_renaming label tl |
---|
92 | ] |
---|
93 | ]. |
---|
94 | |
---|
95 | let rec add_mapping_to_initial_mapping |
---|
96 | (initial_mapping: list (list Identifier × (option Identifier))) (belongs: Identifier) (fresh: Identifier) |
---|
97 | on initial_mapping: list (list Identifier × (option Identifier)) ≝ |
---|
98 | match initial_mapping with |
---|
99 | [ nil ⇒ nil … |
---|
100 | | cons hd tl ⇒ |
---|
101 | match member … (eq_bv …) belongs (\fst hd) with |
---|
102 | [ true ⇒ 〈\fst hd, Some … fresh〉 :: tl |
---|
103 | | false ⇒ 〈\fst hd, None …〉 :: add_mapping_to_initial_mapping tl belongs fresh |
---|
104 | ] |
---|
105 | ]. |
---|
106 | |
---|
107 | definition rename_preinstruction: |
---|
108 | list (list Identifier × (option Identifier)) → preinstruction Identifier → identifier_supply → |
---|
109 | ((list (list Identifier × (option Identifier))) × (preinstruction Identifier) × identifier_supply) ≝ |
---|
110 | λinitial_mapping. |
---|
111 | λpreinstruction. |
---|
112 | λsupply. |
---|
113 | match preinstruction with |
---|
114 | [ JC ident ⇒ |
---|
115 | match should_be_renamed ident initial_mapping with |
---|
116 | [ false ⇒ (* XXX: does not need renaming *) |
---|
117 | 〈initial_mapping, JC … ident, supply〉 |
---|
118 | | true ⇒ |
---|
119 | match get_previous_renaming ident initial_mapping with |
---|
120 | [ None ⇒ |
---|
121 | let 〈supply, fresh_ident〉 ≝ fresh_identifier supply in |
---|
122 | let initial_mapping ≝ add_mapping_to_initial_mapping initial_mapping ident fresh_ident in |
---|
123 | 〈initial_mapping, JC … fresh_ident, supply〉 |
---|
124 | | Some renaming ⇒ (* XXX: no action necessary, just reuse *) |
---|
125 | 〈initial_mapping, JC … renaming, supply〉 |
---|
126 | ] |
---|
127 | ] |
---|
128 | | JNC ident ⇒ |
---|
129 | match should_be_renamed ident initial_mapping with |
---|
130 | [ false ⇒ (* XXX: does not need renaming *) |
---|
131 | 〈initial_mapping, JNC … ident, supply〉 |
---|
132 | | true ⇒ |
---|
133 | match get_previous_renaming ident initial_mapping with |
---|
134 | [ None ⇒ |
---|
135 | let 〈supply, fresh_ident〉 ≝ fresh_identifier supply in |
---|
136 | let initial_mapping ≝ add_mapping_to_initial_mapping initial_mapping ident fresh_ident in |
---|
137 | 〈initial_mapping, JNC … fresh_ident, supply〉 |
---|
138 | | Some renaming ⇒ (* XXX: no action necessary, just reuse *) |
---|
139 | 〈initial_mapping, JNC … renaming, supply〉 |
---|
140 | ] |
---|
141 | ] |
---|
142 | | JB bit ident ⇒ |
---|
143 | match should_be_renamed ident initial_mapping with |
---|
144 | [ false ⇒ (* XXX: does not need renaming *) |
---|
145 | 〈initial_mapping, JB … bit ident, supply〉 |
---|
146 | | true ⇒ |
---|
147 | match get_previous_renaming ident initial_mapping with |
---|
148 | [ None ⇒ |
---|
149 | let 〈supply, fresh_ident〉 ≝ fresh_identifier supply in |
---|
150 | let initial_mapping ≝ add_mapping_to_initial_mapping initial_mapping ident fresh_ident in |
---|
151 | 〈initial_mapping, JB … bit fresh_ident, supply〉 |
---|
152 | | Some renaming ⇒ (* XXX: no action necessary *) |
---|
153 | 〈initial_mapping, JB … bit renaming, supply〉 |
---|
154 | ] |
---|
155 | ] |
---|
156 | | JNB bit ident ⇒ |
---|
157 | match should_be_renamed ident initial_mapping with |
---|
158 | [ false ⇒ (* XXX: does not need renaming *) |
---|
159 | 〈initial_mapping, JNB … bit ident, supply〉 |
---|
160 | | true ⇒ |
---|
161 | match get_previous_renaming ident initial_mapping with |
---|
162 | [ None ⇒ |
---|
163 | let 〈supply, fresh_ident〉 ≝ fresh_identifier supply in |
---|
164 | let initial_mapping ≝ add_mapping_to_initial_mapping initial_mapping ident fresh_ident in |
---|
165 | 〈initial_mapping, JNB … bit fresh_ident, supply〉 |
---|
166 | | Some renaming ⇒ (* XXX: no action necessary *) |
---|
167 | 〈initial_mapping, JNB … bit renaming, supply〉 |
---|
168 | ] |
---|
169 | ] |
---|
170 | | JBC bit ident ⇒ |
---|
171 | match should_be_renamed ident initial_mapping with |
---|
172 | [ false ⇒ (* XXX: does not need renaming *) |
---|
173 | 〈initial_mapping, JBC … bit ident, supply〉 |
---|
174 | | true ⇒ |
---|
175 | match get_previous_renaming ident initial_mapping with |
---|
176 | [ None ⇒ |
---|
177 | let 〈supply, fresh_ident〉 ≝ fresh_identifier supply in |
---|
178 | let initial_mapping ≝ add_mapping_to_initial_mapping initial_mapping ident fresh_ident in |
---|
179 | 〈initial_mapping, JBC … bit fresh_ident, supply〉 |
---|
180 | | Some renaming ⇒ (* XXX: no action necessary *) |
---|
181 | 〈initial_mapping, JBC … bit renaming, supply〉 |
---|
182 | ] |
---|
183 | ] |
---|
184 | | JZ ident ⇒ |
---|
185 | match should_be_renamed ident initial_mapping with |
---|
186 | [ false ⇒ (* XXX: does not need renaming *) |
---|
187 | 〈initial_mapping, JZ … ident, supply〉 |
---|
188 | | true ⇒ |
---|
189 | match get_previous_renaming ident initial_mapping with |
---|
190 | [ None ⇒ |
---|
191 | let 〈supply, fresh_ident〉 ≝ fresh_identifier supply in |
---|
192 | let initial_mapping ≝ add_mapping_to_initial_mapping initial_mapping ident fresh_ident in |
---|
193 | 〈initial_mapping, JZ … fresh_ident, supply〉 |
---|
194 | | Some renaming ⇒ (* XXX: no action necessary *) |
---|
195 | 〈initial_mapping, JZ … renaming, supply〉 |
---|
196 | ] |
---|
197 | ] |
---|
198 | | JNZ ident ⇒ |
---|
199 | match should_be_renamed ident initial_mapping with |
---|
200 | [ false ⇒ (* XXX: does not need renaming *) |
---|
201 | 〈initial_mapping, JNZ … ident, supply〉 |
---|
202 | | true ⇒ |
---|
203 | match get_previous_renaming ident initial_mapping with |
---|
204 | [ None ⇒ |
---|
205 | let 〈supply, fresh_ident〉 ≝ fresh_identifier supply in |
---|
206 | let initial_mapping ≝ add_mapping_to_initial_mapping initial_mapping ident fresh_ident in |
---|
207 | 〈initial_mapping, JNZ … fresh_ident, supply〉 |
---|
208 | | Some renaming ⇒ (* XXX: no action necessary *) |
---|
209 | 〈initial_mapping, JNZ … renaming, supply〉 |
---|
210 | ] |
---|
211 | ] |
---|
212 | | CJNE src ident ⇒ |
---|
213 | match should_be_renamed ident initial_mapping with |
---|
214 | [ false ⇒ (* XXX: does not need renaming *) |
---|
215 | 〈initial_mapping, CJNE … src ident, supply〉 |
---|
216 | | true ⇒ |
---|
217 | match get_previous_renaming ident initial_mapping with |
---|
218 | [ None ⇒ |
---|
219 | let 〈supply, fresh_ident〉 ≝ fresh_identifier supply in |
---|
220 | let initial_mapping ≝ add_mapping_to_initial_mapping initial_mapping ident fresh_ident in |
---|
221 | 〈initial_mapping, CJNE … src fresh_ident, supply〉 |
---|
222 | | Some renaming ⇒ (* XXX: no action necessary *) |
---|
223 | 〈initial_mapping, CJNE … src renaming, supply〉 |
---|
224 | ] |
---|
225 | ] |
---|
226 | | DJNZ src ident ⇒ |
---|
227 | match should_be_renamed ident initial_mapping with |
---|
228 | [ false ⇒ (* XXX: does not need renaming *) |
---|
229 | 〈initial_mapping, DJNZ … src ident, supply〉 |
---|
230 | | true ⇒ |
---|
231 | match get_previous_renaming ident initial_mapping with |
---|
232 | [ None ⇒ |
---|
233 | let 〈supply, fresh_ident〉 ≝ fresh_identifier supply in |
---|
234 | let initial_mapping ≝ add_mapping_to_initial_mapping initial_mapping ident fresh_ident in |
---|
235 | 〈initial_mapping, DJNZ … src fresh_ident, supply〉 |
---|
236 | | Some renaming ⇒ (* XXX: no action necessary *) |
---|
237 | 〈initial_mapping, DJNZ … src renaming, supply〉 |
---|
238 | ] |
---|
239 | ] |
---|
240 | (* XXX: no identifiers in rest of instructions *) |
---|
241 | | _ ⇒ 〈initial_mapping, preinstruction, supply〉 |
---|
242 | ]. |
---|
243 | |
---|
244 | definition rename_pseudo_instruction: |
---|
245 | (list (list Identifier × (option Identifier))) → pseudo_instruction → identifier_supply → |
---|
246 | ((list (list Identifier × (option Identifier))) × pseudo_instruction × identifier_supply) ≝ |
---|
247 | λinitial_mapping. |
---|
248 | λpseudo_instruction. |
---|
249 | λsupply. |
---|
250 | match pseudo_instruction with |
---|
251 | [ Instruction instr ⇒ |
---|
252 | let 〈initial_mapping, instruction, supply〉 ≝ rename_preinstruction initial_mapping instr supply in |
---|
253 | 〈initial_mapping, Instruction instruction, supply〉 |
---|
254 | | Comment comment ⇒ |
---|
255 | 〈initial_mapping, Comment comment, supply〉 |
---|
256 | | Cost cost ⇒ |
---|
257 | 〈initial_mapping, Cost cost, supply〉 (* XXX: cost labels are not renamed *) |
---|
258 | | Jmp ident ⇒ |
---|
259 | match should_be_renamed ident initial_mapping with |
---|
260 | [ false ⇒ 〈initial_mapping, Jmp ident, supply〉 |
---|
261 | | true ⇒ |
---|
262 | match get_previous_renaming ident initial_mapping with |
---|
263 | [ None ⇒ (* XXX: no previous renaming *) |
---|
264 | let 〈supply, fresh_ident〉 ≝ fresh_identifier supply in |
---|
265 | let initial_mapping ≝ add_mapping_to_initial_mapping initial_mapping ident fresh_ident in |
---|
266 | 〈initial_mapping, Jmp fresh_ident, supply〉 |
---|
267 | | Some previous ⇒ |
---|
268 | 〈initial_mapping, Jmp previous, supply〉 |
---|
269 | ] |
---|
270 | ] |
---|
271 | | Call ident ⇒ |
---|
272 | match should_be_renamed ident initial_mapping with |
---|
273 | [ false ⇒ 〈initial_mapping, Call ident, supply〉 |
---|
274 | | true ⇒ |
---|
275 | match get_previous_renaming ident initial_mapping with |
---|
276 | [ None ⇒ (* XXX: no previous renaming *) |
---|
277 | let 〈supply, fresh_ident〉 ≝ fresh_identifier supply in |
---|
278 | let initial_mapping ≝ add_mapping_to_initial_mapping initial_mapping ident fresh_ident in |
---|
279 | 〈initial_mapping, Call fresh_ident, supply〉 |
---|
280 | | Some previous ⇒ |
---|
281 | 〈initial_mapping, Call previous, supply〉 |
---|
282 | ] |
---|
283 | ] |
---|
284 | | Mov dptr ident ⇒ |
---|
285 | match should_be_renamed ident initial_mapping with |
---|
286 | [ false ⇒ 〈initial_mapping, Mov dptr ident, supply〉 |
---|
287 | | true ⇒ |
---|
288 | match get_previous_renaming ident initial_mapping with |
---|
289 | [ None ⇒ (* XXX: no previous renaming *) |
---|
290 | let 〈supply, fresh_ident〉 ≝ fresh_identifier supply in |
---|
291 | let initial_mapping ≝ add_mapping_to_initial_mapping initial_mapping ident fresh_ident in |
---|
292 | 〈initial_mapping, Mov dptr fresh_ident, supply〉 |
---|
293 | | Some previous ⇒ |
---|
294 | 〈initial_mapping, Mov dptr previous, supply〉 |
---|
295 | ] |
---|
296 | ] |
---|
297 | ]. |
---|
298 | |
---|
299 | (* -------------------------------------------------------------------------- *) |
---|
300 | (* Perform a global renaming. Here, we take a list of lists of identifiers. *) |
---|
301 | (* The inner lists contain identifiers that must be renamed to the same fresh *) |
---|
302 | (* identifier throughout. *) |
---|
303 | (* -------------------------------------------------------------------------- *) |
---|
304 | |
---|
305 | let rec map_prod |
---|
306 | (a: Type[0]) (b: Type[0]) (c: Type[0]) (f: a → c → b × c) (seed: c) |
---|
307 | (the_list: list a) |
---|
308 | on the_list: list b ≝ |
---|
309 | match the_list with |
---|
310 | [ nil ⇒ nil … |
---|
311 | | cons hd tl ⇒ |
---|
312 | let 〈hd, seed〉 ≝ f hd seed in |
---|
313 | hd :: map_prod … f seed tl |
---|
314 | ]. |
---|
315 | |
---|
316 | definition global_renaming: list (list Identifier) → pseudo_assembly_program → pseudo_assembly_program ≝ |
---|
317 | λrenamings. |
---|
318 | λpseudo_program. |
---|
319 | let 〈preamble, program〉 ≝ pseudo_program in |
---|
320 | let labels ≝ identifiers_of_labelled_program program in |
---|
321 | (* XXX: create a supply starting from S (max label in program) *) |
---|
322 | let supply ≝ create_identifier_supply labels in |
---|
323 | let renamed ≝ map_prod … (λlabel_instruction. λinitial_mapping_supply. |
---|
324 | let 〈label, instruction〉 ≝ label_instruction in |
---|
325 | let 〈initial_mapping, supply〉 ≝ initial_mapping_supply in |
---|
326 | let 〈initial_mapping, renamed_instruction, supply〉 ≝ rename_pseudo_instruction initial_mapping instruction supply in |
---|
327 | match label with |
---|
328 | [ None ⇒ 〈〈None …, renamed_instruction〉, 〈initial_mapping, supply〉〉 |
---|
329 | | Some label ⇒ |
---|
330 | (* XXX: does this label need renaming? *) |
---|
331 | match should_be_renamed label initial_mapping with |
---|
332 | [ false ⇒ 〈〈Some … label, renamed_instruction〉, 〈initial_mapping, supply〉〉 |
---|
333 | | true ⇒ |
---|
334 | (* XXX: has this label's class been renamed before? *) |
---|
335 | match get_previous_renaming label initial_mapping with |
---|
336 | [ None ⇒ (* XXX: we are free to rename *) |
---|
337 | let 〈supply, fresh_ident〉 ≝ fresh_identifier supply in |
---|
338 | let initial_mapping ≝ add_mapping_to_initial_mapping initial_mapping label fresh_ident in |
---|
339 | 〈〈Some … fresh_ident, renamed_instruction〉, 〈initial_mapping, supply〉〉 |
---|
340 | | Some new_label ⇒ 〈〈Some … new_label, renamed_instruction〉, 〈initial_mapping, supply〉〉 |
---|
341 | ] |
---|
342 | ] |
---|
343 | ] |
---|
344 | ) (〈lift_renamings_to_empty_initial_mappings renamings, supply〉) program in |
---|
345 | 〈preamble, renamed〉. |
---|
346 | |
---|
347 | let rec pre_erase' |
---|
348 | (the_program: list labelled_instruction) |
---|
349 | on the_program: (list (list Identifier) × (list labelled_instruction)) ≝ |
---|
350 | match the_program with |
---|
351 | [ nil ⇒ ? |
---|
352 | | cons hd tl ⇒ ? |
---|
353 | ]. |
---|
354 | |
---|
355 | definition pre_erase: pseudo_assembly_program → (list (list Identifier) × pseudo_assembly_program) ≝ |
---|
356 | λpseudo_program. |
---|
357 | let 〈preamble, pseudos〉 ≝ pseudo_program in |
---|
358 | let 〈renamings, pseudos〉 ≝ pre_erase' pseudos in |
---|
359 | 〈renamings, 〈preamble, pseudos〉〉. |
---|
360 | |
---|
361 | definition erase: pseudo_assembly_program → pseudo_assembly_program ≝ |
---|
362 | λprogram. |
---|
363 | let 〈renamings, pseudo_program〉 ≝ pre_erase program in |
---|
364 | global_renaming renamings pseudo_program. |
---|