source: src/ASM/Erase.ma @ 1460

include "ASM/ASM.ma".
include "ASM/Arithmetic.ma".

let rec find_largest_identifier
  (default: Identifier) (the_list: list Identifier)
    on the_list: Identifier ≝
  match the_list with
  [ nil        ⇒ default
  | cons hd tl ⇒
    match lt_u … hd default with
    [ true  ⇒ find_largest_identifier default tl
    | false ⇒ find_largest_identifier hd tl
    ]
  ].
  
(* -------------------------------------------------------------------------- *)
(* Supplies for generating fresh identifiers, in order to effect the global   *)
(* renaming.                                                                  *)
(* -------------------------------------------------------------------------- *)

record identifier_supply: Type[0] ≝
{
  next: Identifier
}.

definition create_identifier_supply: list Identifier → identifier_supply ≝
  λthe_list.
  let maximum ≝ find_largest_identifier (zero …) the_list in
  let incremented ≝ increment … maximum in
    mk_identifier_supply incremented.

definition fresh_identifier: identifier_supply → (identifier_supply × Identifier) ≝
  λsupply.
    let fresh ≝ next supply in
    let new_supply ≝ mk_identifier_supply (increment … fresh) in
      〈new_supply, fresh〉.

(* -------------------------------------------------------------------------- *)
(* Identify all identifiers in a labelled program.                            *)
(* -------------------------------------------------------------------------- *)

definition identifiers_of_labelled_program: list (labelled_instruction) → list Identifier ≝
  λprogram.
    foldr … (λlabel_instruction. λaccum.
      let 〈label, instruction〉 ≝ label_instruction in
        match label with
        [ None       ⇒ accum
        | Some label ⇒ label :: accum
        ]
    ) [ ] program.

(* -------------------------------------------------------------------------- *)
(* Rename the labels in a single pseudo instruction (and preinstructions.  We *)
(* take a list of lists of identifiers, the inner list of identifiers must    *)
(* all be renamed to the same fresh label.  We also take an identifier supply *)
(* for generating fresh identifiers.                                          *)
(* We give back a list of pairs of lists of identifiers with optional         *)
(* identifiers.  If any identifier in the inner list of identifiers given to  *)
(* this function is renamed to something fresh, we return that fresh          *)
(* identifier wrapped in an option type paired with the list input to the     *)
(* function.  This information is used when renaming the second part of the   *)
(* labelled instruction, to ensure consistency amongst renamings.             *)
(* -------------------------------------------------------------------------- *)

definition lift_renamings_to_empty_initial_mappings:
  list (list Identifier) → list (list Identifier × (option Identifier)) ≝
  λrenamings.
    map … (λeq_class. 〈eq_class, None …〉) renamings.

let rec should_be_renamed
  (ident: Identifier) (the_list: (list (list Identifier × (option Identifier))))
    on the_list: bool ≝
  match the_list with
  [ nil        ⇒ false
  | cons hd tl ⇒
    match member … (eq_bv …) ident (\fst hd) with
    [ true  ⇒ true
    | false ⇒ should_be_renamed ident tl
    ]
  ].

let rec get_previous_renaming
  (label: Identifier) (initial_mapping: (list (list Identifier × (option Identifier))))
    on initial_mapping: option Identifier ≝
  match initial_mapping with
  [ nil        ⇒ None …
  | cons hd tl ⇒
    let 〈class, renaming〉 ≝ hd in
      match member … (eq_bv …) label class with
      [ true  ⇒ renaming
      | false ⇒ get_previous_renaming label tl
      ]
  ].

let rec add_mapping_to_initial_mapping
  (initial_mapping: list (list Identifier × (option Identifier))) (belongs: Identifier) (fresh: Identifier)
    on initial_mapping: list (list Identifier × (option Identifier)) ≝
  match initial_mapping with
  [ nil        ⇒ nil …
  | cons hd tl ⇒
    match member … (eq_bv …) belongs (\fst hd) with
    [ true  ⇒ 〈\fst hd, Some … fresh〉 :: tl
    | false ⇒ 〈\fst hd, None …〉 :: add_mapping_to_initial_mapping tl belongs fresh
    ]
  ].

definition rename_preinstruction:
  list (list Identifier × (option Identifier)) → preinstruction Identifier → identifier_supply →
    ((list (list Identifier × (option Identifier))) × (preinstruction Identifier) × identifier_supply) ≝
  λinitial_mapping.
  λpreinstruction.
  λsupply.
  match preinstruction with
  [ JC ident ⇒
    match should_be_renamed ident initial_mapping with
    [ false ⇒ (* XXX: does not need renaming *)
      〈initial_mapping, JC … ident, supply〉
    | true ⇒
      match get_previous_renaming ident initial_mapping with
      [ None ⇒
        let 〈supply, fresh_ident〉 ≝ fresh_identifier supply in
        let initial_mapping ≝ add_mapping_to_initial_mapping initial_mapping ident fresh_ident in
          〈initial_mapping, JC … fresh_ident, supply〉
      | Some renaming ⇒ (* XXX: no action necessary, just reuse *)
          〈initial_mapping, JC … renaming, supply〉
      ]
    ]
  | JNC ident ⇒
    match should_be_renamed ident initial_mapping with
    [ false ⇒ (* XXX: does not need renaming *)
      〈initial_mapping, JNC … ident, supply〉
    | true ⇒
      match get_previous_renaming ident initial_mapping with
      [ None ⇒
        let 〈supply, fresh_ident〉 ≝ fresh_identifier supply in
        let initial_mapping ≝ add_mapping_to_initial_mapping initial_mapping ident fresh_ident in
          〈initial_mapping, JNC … fresh_ident, supply〉
      | Some renaming ⇒ (* XXX: no action necessary, just reuse *)
          〈initial_mapping, JNC … renaming, supply〉
      ]
    ]
  | JB bit ident ⇒
    match should_be_renamed ident initial_mapping with
    [ false ⇒ (* XXX: does not need renaming *)
      〈initial_mapping, JB … bit ident, supply〉
    | true ⇒
      match get_previous_renaming ident initial_mapping with
      [ None ⇒
        let 〈supply, fresh_ident〉 ≝ fresh_identifier supply in
        let initial_mapping ≝ add_mapping_to_initial_mapping initial_mapping ident fresh_ident in
          〈initial_mapping, JB … bit fresh_ident, supply〉
      | Some renaming ⇒ (* XXX: no action necessary *)
          〈initial_mapping, JB … bit renaming, supply〉
      ]
    ]
  | JNB bit ident ⇒
    match should_be_renamed ident initial_mapping with
    [ false ⇒ (* XXX: does not need renaming *)
      〈initial_mapping, JNB … bit ident, supply〉
    | true ⇒
      match get_previous_renaming ident initial_mapping with
      [ None ⇒
        let 〈supply, fresh_ident〉 ≝ fresh_identifier supply in
        let initial_mapping ≝ add_mapping_to_initial_mapping initial_mapping ident fresh_ident in
          〈initial_mapping, JNB … bit fresh_ident, supply〉
      | Some renaming ⇒ (* XXX: no action necessary *)
          〈initial_mapping, JNB … bit renaming, supply〉
      ]
    ]
  | JBC bit ident ⇒
    match should_be_renamed ident initial_mapping with
    [ false ⇒ (* XXX: does not need renaming *)
      〈initial_mapping, JBC … bit ident, supply〉
    | true ⇒
      match get_previous_renaming ident initial_mapping with
      [ None ⇒
        let 〈supply, fresh_ident〉 ≝ fresh_identifier supply in
        let initial_mapping ≝ add_mapping_to_initial_mapping initial_mapping ident fresh_ident in
          〈initial_mapping, JBC … bit fresh_ident, supply〉
      | Some renaming ⇒ (* XXX: no action necessary *)
          〈initial_mapping, JBC … bit renaming, supply〉
      ]
    ]
  | JZ ident ⇒
    match should_be_renamed ident initial_mapping with
    [ false ⇒ (* XXX: does not need renaming *)
      〈initial_mapping, JZ … ident, supply〉
    | true ⇒
      match get_previous_renaming ident initial_mapping with
      [ None ⇒
        let 〈supply, fresh_ident〉 ≝ fresh_identifier supply in
        let initial_mapping ≝ add_mapping_to_initial_mapping initial_mapping ident fresh_ident in
          〈initial_mapping, JZ … fresh_ident, supply〉
      | Some renaming ⇒ (* XXX: no action necessary *)
          〈initial_mapping, JZ … renaming, supply〉
      ]
    ]
  | JNZ ident ⇒
    match should_be_renamed ident initial_mapping with
    [ false ⇒ (* XXX: does not need renaming *)
      〈initial_mapping, JNZ … ident, supply〉
    | true ⇒
      match get_previous_renaming ident initial_mapping with
      [ None ⇒
        let 〈supply, fresh_ident〉 ≝ fresh_identifier supply in
        let initial_mapping ≝ add_mapping_to_initial_mapping initial_mapping ident fresh_ident in
          〈initial_mapping, JNZ … fresh_ident, supply〉
      | Some renaming ⇒ (* XXX: no action necessary *)
          〈initial_mapping, JNZ … renaming, supply〉
      ]
    ]
  | CJNE src ident ⇒
    match should_be_renamed ident initial_mapping with
    [ false ⇒ (* XXX: does not need renaming *)
      〈initial_mapping, CJNE … src ident, supply〉
    | true ⇒
      match get_previous_renaming ident initial_mapping with
      [ None ⇒
        let 〈supply, fresh_ident〉 ≝ fresh_identifier supply in
        let initial_mapping ≝ add_mapping_to_initial_mapping initial_mapping ident fresh_ident in
          〈initial_mapping, CJNE … src fresh_ident, supply〉
      | Some renaming ⇒ (* XXX: no action necessary *)
          〈initial_mapping, CJNE … src renaming, supply〉
      ]
    ]
  | DJNZ src ident ⇒
    match should_be_renamed ident initial_mapping with
    [ false ⇒ (* XXX: does not need renaming *)
      〈initial_mapping, DJNZ … src ident, supply〉
    | true ⇒
      match get_previous_renaming ident initial_mapping with
      [ None ⇒
        let 〈supply, fresh_ident〉 ≝ fresh_identifier supply in
        let initial_mapping ≝ add_mapping_to_initial_mapping initial_mapping ident fresh_ident in
          〈initial_mapping, DJNZ … src fresh_ident, supply〉
      | Some renaming ⇒ (* XXX: no action necessary *)
          〈initial_mapping, DJNZ … src renaming, supply〉
      ]
    ]
  (* XXX: no identifiers in rest of instructions *)
  | _ ⇒ 〈initial_mapping, preinstruction, supply〉
  ].
    
definition rename_pseudo_instruction:
  (list (list Identifier × (option Identifier))) → pseudo_instruction → identifier_supply →
  ((list (list Identifier × (option Identifier))) × pseudo_instruction × identifier_supply) ≝
  λinitial_mapping.
  λpseudo_instruction.
  λsupply.
  match pseudo_instruction with
  [ Instruction instr ⇒
    let 〈initial_mapping, instruction, supply〉 ≝ rename_preinstruction initial_mapping instr supply in
      〈initial_mapping, Instruction instruction, supply〉
  | Comment comment ⇒
      〈initial_mapping, Comment comment, supply〉
  | Cost cost ⇒
      〈initial_mapping, Cost cost, supply〉 (* XXX: cost labels are not renamed *)
  | Jmp ident ⇒
    match should_be_renamed ident initial_mapping with
    [ false ⇒ 〈initial_mapping, Jmp ident, supply〉
    | true ⇒
      match get_previous_renaming ident initial_mapping with
      [ None ⇒ (* XXX: no previous renaming *)
        let 〈supply, fresh_ident〉 ≝ fresh_identifier supply in
        let initial_mapping ≝ add_mapping_to_initial_mapping initial_mapping ident fresh_ident in
          〈initial_mapping, Jmp fresh_ident, supply〉
      | Some previous ⇒
          〈initial_mapping, Jmp previous, supply〉
      ]
    ]
  | Call ident ⇒
    match should_be_renamed ident initial_mapping with
    [ false ⇒ 〈initial_mapping, Call ident, supply〉
    | true ⇒ 
      match get_previous_renaming ident initial_mapping with
      [ None ⇒ (* XXX: no previous renaming *)
        let 〈supply, fresh_ident〉 ≝ fresh_identifier supply in
        let initial_mapping ≝ add_mapping_to_initial_mapping initial_mapping ident fresh_ident in
          〈initial_mapping, Call fresh_ident, supply〉
      | Some previous ⇒
          〈initial_mapping, Call previous, supply〉
      ]
    ]
  | Mov dptr ident ⇒
    match should_be_renamed ident initial_mapping with
    [ false ⇒ 〈initial_mapping, Mov dptr ident, supply〉
    | true ⇒
      match get_previous_renaming ident initial_mapping with
      [ None ⇒ (* XXX: no previous renaming *)
        let 〈supply, fresh_ident〉 ≝ fresh_identifier supply in
        let initial_mapping ≝ add_mapping_to_initial_mapping initial_mapping ident fresh_ident in
          〈initial_mapping, Mov dptr fresh_ident, supply〉
      | Some previous ⇒
          〈initial_mapping, Mov dptr previous, supply〉
      ]
    ]
  ].
  
(* -------------------------------------------------------------------------- *)
(* Perform a global renaming.  Here, we take a list of lists of identifiers.  *)
(* The inner lists contain identifiers that must be renamed to the same fresh *)
(* identifier throughout.                                                     *)
(* -------------------------------------------------------------------------- *)

let rec map_prod
  (a: Type[0]) (b: Type[0]) (c: Type[0]) (f: a → c → b × c) (seed: c)
    (the_list: list a)
      on the_list: list b ≝
  match the_list with
  [ nil        ⇒ nil …
  | cons hd tl ⇒
    let 〈hd, seed〉 ≝ f hd seed in
      hd :: map_prod … f seed tl
  ].

definition global_renaming: list (list Identifier) → pseudo_assembly_program → pseudo_assembly_program ≝
  λrenamings.
  λpseudo_program.
    let 〈preamble, program〉 ≝ pseudo_program in
    let labels ≝ identifiers_of_labelled_program program in
    (* XXX: create a supply starting from S (max label in program) *)
    let supply ≝ create_identifier_supply labels in
    let renamed ≝ map_prod … (λlabel_instruction. λinitial_mapping_supply.
      let 〈label, instruction〉 ≝ label_instruction in
      let 〈initial_mapping, supply〉 ≝ initial_mapping_supply in
      let 〈initial_mapping, renamed_instruction, supply〉 ≝ rename_pseudo_instruction initial_mapping instruction supply in
      match label with
      [ None       ⇒ 〈〈None …, renamed_instruction〉, 〈initial_mapping, supply〉〉
      | Some label ⇒
        (* XXX: does this label need renaming? *)
        match should_be_renamed label initial_mapping with
        [ false ⇒ 〈〈Some … label, renamed_instruction〉, 〈initial_mapping, supply〉〉
        | true ⇒
          (* XXX: has this label's class been renamed before? *)
          match get_previous_renaming label initial_mapping with
          [ None           ⇒ (* XXX: we are free to rename *)
            let 〈supply, fresh_ident〉 ≝ fresh_identifier supply in
            let initial_mapping ≝ add_mapping_to_initial_mapping initial_mapping label fresh_ident in
              〈〈Some … fresh_ident, renamed_instruction〉, 〈initial_mapping, supply〉〉
          | Some new_label ⇒ 〈〈Some … new_label, renamed_instruction〉, 〈initial_mapping, supply〉〉
          ]
        ]
      ]
    ) (〈lift_renamings_to_empty_initial_mappings renamings, supply〉) program in
      〈preamble, renamed〉.
      
let rec pre_erase'
  (the_program: list labelled_instruction)
    on the_program: (list (list Identifier) × (list labelled_instruction)) ≝
  match the_program with
  [ nil        ⇒ ?
  | cons hd tl ⇒ ?
  ].
      
definition pre_erase: pseudo_assembly_program → (list (list Identifier) × pseudo_assembly_program) ≝
  λpseudo_program.
  let 〈preamble, pseudos〉 ≝ pseudo_program in
  let 〈renamings, pseudos〉 ≝ pre_erase' pseudos in
    〈renamings, 〈preamble, pseudos〉〉.

definition erase: pseudo_assembly_program → pseudo_assembly_program ≝
  λprogram.
  let 〈renamings, pseudo_program〉 ≝ pre_erase program in
    global_renaming renamings pseudo_program.