Changeset 1461 for src/ASM/Erase.ma
- Timestamp:
- Oct 24, 2011, 5:56:55 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Erase.ma
r1460 r1461 1 1 include "ASM/ASM.ma". 2 include "ASM/Arithmetic.ma". 2 include "ASM/BitVectorTrie.ma". 3 4 let rec pre_erase 5 (the_program: list labelled_instruction) (labels: list Identifier) 6 on the_program: ((BitVectorTrie Identifier 16) × (list labelled_instruction)) ≝ 7 match the_program with 8 [ nil ⇒ 9 match labels with 10 [ nil ⇒ 〈Stub Identifier 16, [ ]〉 (* XXX: labels should be empty *) 11 | _ ⇒ ⊥ 12 ] 13 | cons hd tl ⇒ 14 let 〈label, instruction〉 ≝ hd in 15 match label with 16 [ None ⇒ 17 let 〈maps, the_program〉 ≝ pre_erase tl labels in 18 match instruction with 19 [ Cost cost ⇒ 〈maps, the_program〉 20 | _ ⇒ 〈maps, 〈None …, instruction〉 :: the_program〉 21 ] 22 | Some label ⇒ 23 match instruction with 24 [ Cost cost ⇒ pre_erase tl (label :: labels) 25 | _ ⇒ 26 let 〈maps, the_program〉 ≝ pre_erase tl [ ] in 27 let maps ≝ foldr … (λl. λmap. insert … l label map) maps (label::labels) in 28 〈maps, the_program〉 29 ] 30 ] 31 ]. 32 @daemon 33 qed. 3 34 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 ] 35 definition relabel_instruction: preinstruction Identifier → BitVectorTrie Identifier 16 → preinstruction Identifier ≝ 36 λpre. 37 λmap. 38 match pre with 39 [ JC ident ⇒ 40 let located ≝ lookup … ident map ident in 41 JC … located 42 | JNC ident ⇒ 43 let located ≝ lookup … ident map ident in 44 JNC … located 45 | JB bit ident ⇒ 46 let located ≝ lookup … ident map ident in 47 JB … bit located 48 | JNB bit ident ⇒ 49 let located ≝ lookup … ident map ident in 50 JNB … bit located 51 | JBC bit ident ⇒ 52 let located ≝ lookup … ident map ident in 53 JBC … bit located 54 | JZ ident ⇒ 55 let located ≝ lookup … ident map ident in 56 JZ … located 57 | JNZ ident ⇒ 58 let located ≝ lookup … ident map ident in 59 JNZ … located 60 | CJNE src ident ⇒ 61 let located ≝ lookup … ident map ident in 62 CJNE … src located 63 | DJNZ src ident ⇒ 64 let located ≝ lookup … ident map ident in 65 DJNZ … src located 66 (* XXX: no identifiers in rest of instructions *) 67 | _ ⇒ pre 80 68 ]. 81 69 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 *) 70 definition relabel_pseudo_instruction: pseudo_instruction → BitVectorTrie Identifier 16 → pseudo_instruction ≝ 71 λpseudo. 72 λmap. 73 match pseudo with 74 [ Instruction instr ⇒ Instruction (relabel_instruction instr map) 75 | Cost cost ⇒ Cost cost 76 | Comment comment ⇒ Comment comment 258 77 | 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 ] 78 let located ≝ lookup … ident map ident in 79 Jmp located 271 80 | 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 ] 81 let located ≝ lookup … ident map ident in 82 Call located 284 83 | 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 ⇒ ? 84 let located ≝ lookup … ident map ident in 85 Mov dptr located 353 86 ]. 354 87 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〉〉. 88 let rec relabel 89 (the_program: list labelled_instruction) (map: BitVectorTrie Identifier 16) 90 on the_program: list labelled_instruction ≝ 91 match the_program with 92 [ nil ⇒ [ ] 93 | cons hd tl ⇒ 94 let 〈label, instruction〉 ≝ hd in 95 let relabelled ≝ relabel_pseudo_instruction instruction map in 96 〈label, relabelled〉 :: relabel tl map 97 ]. 360 98 361 99 definition erase: pseudo_assembly_program → pseudo_assembly_program ≝ 362 100 λprogram. 363 let 〈renamings, pseudo_program〉 ≝ pre_erase program in 364 global_renaming renamings pseudo_program. 101 let 〈preamble, instructions〉 ≝ program in 102 let 〈maps, instructions〉 ≝ pre_erase instructions [ ] in 103 let relabelled ≝ relabel instructions maps in 104 〈preamble, relabelled〉.
Note: See TracChangeset
for help on using the changeset viewer.