source: src/ASM/Erase.ma @ 1460

Last change on this file since 1460 was 1460, checked in by mulligan, 8 years ago

most of cost label erasure for assembly language complete, with one axiom remaining

File size: 15.8 KB
Line 
1include "ASM/ASM.ma".
2include "ASM/Arithmetic.ma".
3
4let 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
21record identifier_supply: Type[0] ≝
22{
23  next: Identifier
24}.
25
26definition 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
32definition 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
42definition 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
65definition 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
70let 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
82let 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
95let 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
107definition 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   
244definition 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
305let 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
316definition 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     
347let 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     
355definition 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
361definition erase: pseudo_assembly_program → pseudo_assembly_program ≝
362  λprogram.
363  let 〈renamings, pseudo_program〉 ≝ pre_erase program in
364    global_renaming renamings pseudo_program.
Note: See TracBrowser for help on using the repository browser.