Changeset 1461 for src/ASM/Erase.ma


Ignore:
Timestamp:
Oct 24, 2011, 5:56:55 PM (9 years ago)
Author:
mulligan
Message:

rewrote erasure for assembly programs

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/Erase.ma

    r1460 r1461  
    11include "ASM/ASM.ma".
    2 include "ASM/Arithmetic.ma".
     2include "ASM/BitVectorTrie.ma".
     3     
     4let 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
     33qed.
    334
    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     ]
     35definition 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
    8068  ].
    8169
    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 *)
     70definition 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
    25877  | 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
    27180  | 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
    28483  | 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
    35386  ].
    35487     
    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〉〉.
     88let 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  ].
    36098
    36199definition erase: pseudo_assembly_program → pseudo_assembly_program ≝
    362100  λ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.