source: src/ERTL/liveness.ma @ 1249

include "ASM/Util.ma".
include "ERTL/ERTL.ma".
include "utilities/adt/set_adt.ma".

definition statement_successors ≝
  λglobals: list ident.
  λs: ertl_statement globals.
  match s with
  [ joint_st_sequential seq l ⇒
    match seq with
    [ joint_instr_cond acc_a_reg lbl_true ⇒
        set_insert … lbl_true (set_singleton … l)
    | _ ⇒ set_singleton … l
    ]
  | joint_st_extension ext ⇒
    match ext with
    [ ertl_st_ext_new_frame l ⇒ set_singleton … l
    | ertl_st_ext_del_frame l ⇒ set_singleton … l
    | ertl_st_ext_frame_size r l ⇒ set_singleton … l
    ]
  | joint_st_goto l ⇒ set_singleton … l
  | joint_st_return ⇒ set_empty …
  ].

definition register_lattice ≝ (set register) × (set Register).
definition lattice_property ≝ register_lattice.
definition lattice_bottom: register_lattice ≝ 〈set_empty register, set_empty Register〉.
definition lattice_psingleton: register → register_lattice ≝
  λr.
    〈set_singleton … r, set_empty …〉.
definition lattice_hsingleton: Register → register_lattice ≝
  λr.
    〈set_empty …, set_singleton … r〉.

definition lattice_join: register_lattice → register_lattice → register_lattice ≝
  λleft.
  λright.
  let 〈lp, lh〉 ≝ left in
  let 〈rp, rh〉 ≝ right in
    〈set_union … lp rp, set_union … lh rh〉.

definition lattice_diff: register_lattice → register_lattice → register_lattice ≝
  λleft.
  λright.
  let 〈lp, lh〉 ≝ left in
  let 〈rp, rh〉 ≝ right in
    〈set_diff … lp rp, set_diff … lh rh〉.

definition lattice_equal: register_lattice → register_lattice → bool ≝
  λleft.
  λright.
  let 〈lp, lh〉 ≝ left in
  let 〈rp, rh〉 ≝ right in
    andb (set_equal … (eq_identifier …) lp rp) (set_equal … eq_Register lh rh).

definition lattice_is_maximal: register_lattice → bool ≝ λl. false.

record lattice_property_sig: Type[1] ≝
{
  lp_type      : Type[0];
  lp_property  : Type[0];
  lp_bottom    : lp_type;
  lp_psingleton: register → lp_type;
  lp_hsingleton: Register → lp_type;
  lp_join      : lp_type → lp_type → lp_type;
  lp_diff      : lp_type → lp_type → lp_type;
  lp_equal     : lp_type → lp_type → bool;
  lp_is_maximal: lp_type → bool
}.

definition property ≝
  mk_lattice_property_sig
    ((set register) × (set Register))
    lattice_property
    lattice_bottom
    lattice_psingleton
    lattice_hsingleton
    lattice_join
    lattice_diff
    lattice_equal
    lattice_is_maximal.

definition defined ≝
  λglobals: list ident.
  λs: ertl_statement globals.
  match s with
  [ joint_st_sequential seq l ⇒
    match seq with
    [ joint_instr_op2 op2 r _ ⇒
      match op2 with
      [ Add ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
      | Addc ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
      | Sub ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r)
      | _ ⇒ lattice_psingleton r
      ]
    | joint_instr_clear_carry ⇒ lattice_hsingleton RegisterCarry
    | joint_instr_set_carry ⇒ lattice_hsingleton RegisterCarry
    | joint_instr_opaccs opaccs r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    | joint_instr_op1 op1 r ⇒ lattice_psingleton r
    | joint_instr_pop r ⇒ lattice_psingleton r
    | joint_instr_int r _ ⇒ lattice_psingleton r
    | joint_instr_address _ _ r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    | joint_instr_load r _ _ ⇒ lattice_psingleton r
    (* Potentially destroys all caller-save hardware registers. *)
    | joint_instr_call_id _ _ ⇒ 〈set_empty …, set_from_list … RegisterCallerSaved〉
    | joint_instr_comment c ⇒ lattice_bottom
    | joint_instr_cond r lbl_true ⇒ lattice_bottom
    | joint_instr_store acc_a dpl dph ⇒ lattice_bottom
    | joint_instr_cost_label clabel ⇒ lattice_bottom
    | joint_instr_push r ⇒ lattice_bottom
    | joint_instr_move pair_reg ⇒
      (* first register relevant only *)
      let r1 ≝ \fst pair_reg in
      match r1 with
      [ pseudo p ⇒ lattice_psingleton p
      | hardware h ⇒ lattice_hsingleton h
      ]
    ]
  | joint_st_return ⇒ lattice_bottom
  | joint_st_extension ext ⇒
    match ext with
    [ ertl_st_ext_new_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    | ertl_st_ext_del_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    | ertl_st_ext_frame_size r l ⇒ lattice_psingleton r
    ]
  | joint_st_goto l ⇒ lattice_bottom
  ].

definition ret_regs ≝ set_from_list … RegisterRets.

definition used ≝
  λglobals: list ident.
  λs: ertl_statement globals.
  match s with
  [ joint_st_sequential seq l ⇒
    match seq with
    [ joint_instr_op2 op2 acc_a r ⇒
      match op2 with
      [ Addc ⇒
        lattice_join (lattice_join (lattice_psingleton acc_a) (lattice_psingleton r)) (lattice_hsingleton RegisterCarry)
      | _ ⇒ lattice_join (lattice_psingleton acc_a) (lattice_psingleton r)
      ]
    | joint_instr_clear_carry ⇒ lattice_bottom
    | joint_instr_set_carry ⇒ lattice_bottom
    (* acc_a and acc_b *)
    | joint_instr_opaccs opaccs r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2)
    | joint_instr_op1 op1 r ⇒ lattice_psingleton r
    | joint_instr_pop r ⇒ lattice_bottom
    | joint_instr_int r _ ⇒ lattice_bottom
    | joint_instr_address _ _ r1 r2 ⇒ lattice_bottom
    | joint_instr_load acc_a dpl dph ⇒ lattice_join (lattice_psingleton dpl) (lattice_psingleton dph)
    (* Reads the hardware registers that are used to pass parameters. *)
    | joint_instr_call_id _ nparams ⇒ 〈set_empty …, set_from_list … (prefix ? nparams RegisterParams)〉
    | joint_instr_comment c ⇒ lattice_bottom
    | joint_instr_cond r lbl_true ⇒ lattice_psingleton r
    | joint_instr_store acc_a dpl dph ⇒
      lattice_join (lattice_join (lattice_psingleton acc_a) (lattice_psingleton dpl)) (lattice_psingleton dph)
    | joint_instr_cost_label clabel ⇒ lattice_bottom
    | joint_instr_push r ⇒ lattice_psingleton r
    | joint_instr_move pair_reg ⇒
      (* only second reg in pair relevant *)
      let r2 ≝ \snd pair_reg in
      match r2 with
      [ pseudo p ⇒ lattice_psingleton p
      | hardware h ⇒ lattice_hsingleton h
      ]
    ]
  | joint_st_return ⇒ 〈set_empty …, set_union … (set_from_list … RegisterCalleeSaved) ret_regs〉
  | joint_st_goto l ⇒ lattice_bottom
  | joint_st_extension ext ⇒
    match ext with
    [ ertl_st_ext_new_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    | ertl_st_ext_del_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    | ertl_st_ext_frame_size r l ⇒ lattice_bottom
    ]
  ].

definition eliminable ≝
  λglobals: list ident.
  λl: register_lattice.
  λs: ertl_statement globals.
  let 〈pliveafter, hliveafter〉 ≝ l in
  match s with
  [ joint_st_sequential seq l ⇒
    match seq with
    [ joint_instr_op2 op2 acc_a r ⇒
      if set_member … (eq_identifier …) acc_a pliveafter ∨
         set_member … eq_Register RegisterCarry hliveafter then
        None ?
      else
        Some ? l
    | joint_instr_clear_carry ⇒ None ?
    | joint_instr_set_carry ⇒ None ?
    | joint_instr_opaccs opaccs r1 r2 ⇒
      if set_member … (eq_identifier …) r1 pliveafter ∨
         set_member … (eq_identifier …) r2 pliveafter ∨
         set_member … eq_Register RegisterCarry hliveafter then
        None ?
      else
        Some ? l
    | joint_instr_op1 op1 r ⇒
      if set_member … (eq_identifier …) r pliveafter ∨
         set_member … eq_Register RegisterCarry hliveafter then
        None ?
      else
        Some ? l
    | joint_instr_pop r ⇒ None ?
    | joint_instr_int r _ ⇒
      if set_member … (eq_identifier …) r pliveafter ∨
         set_member … eq_Register RegisterCarry hliveafter then
        None ?
      else
        Some ? l
    | joint_instr_address _ _ r1 r2 ⇒
      if set_member … (eq_identifier …) r1 pliveafter ∨
         set_member … (eq_identifier …) r2 pliveafter ∨
         set_member … eq_Register RegisterCarry hliveafter then
        None ?
      else
        Some ? l
    | joint_instr_load acc_a dpl dph ⇒
      if set_member ? (eq_identifier …) acc_a pliveafter ∨
         set_member … eq_Register RegisterCarry hliveafter then
        None ?
      else
        Some ? l
    | joint_instr_call_id _ nparams ⇒ None ?
    | joint_instr_comment c ⇒ None ?
    | joint_instr_cond r lbl_true ⇒ None ?
    | joint_instr_store acc_a dpl dph ⇒ None ?
    | joint_instr_cost_label clabel ⇒ None ?
    | joint_instr_push r ⇒ None ?
    | joint_instr_move pair_reg ⇒
      let r1 ≝ \fst pair_reg in
      let r2 ≝ \snd pair_reg in
      match r1 with
      [ pseudo p1 ⇒
        if set_member … (eq_identifier …) p1 pliveafter ∨
           set_member … eq_Register RegisterCarry hliveafter then
          None ?
        else
          Some ? l
      | hardware h1 ⇒
        if set_member … eq_Register h1 hliveafter then
          None ?
        else
          Some ? l
      ]
    ]
  | joint_st_goto l ⇒ None ?
  | joint_st_return ⇒ None ?
  | joint_st_extension ext ⇒
    match ext with
    [ ertl_st_ext_new_frame l ⇒ None ?
    | ertl_st_ext_del_frame l ⇒ None ?
    | ertl_st_ext_frame_size r l ⇒
      if set_member ? (eq_identifier RegisterTag) r pliveafter ∨
         set_member ? eq_Register RegisterCarry hliveafter then
        None ?
      else
        Some ? l
    ]
  ].

definition statement_semantics: ∀globals: list ident. ertl_statement globals → register_lattice → register_lattice ≝
  λglobals.
  λstmt.
  λliveafter.
  match eliminable globals liveafter stmt with
  [ None ⇒ lattice_join (lattice_diff liveafter (defined globals stmt)) (used globals stmt)
  | Some l ⇒ liveafter
  ].

definition valuation ≝ label → register_lattice.
definition rhs ≝ valuation → lattice_property.
definition equations ≝ label → rhs.

axiom fix_lfp: equations → valuation.

definition livebefore ≝
  λglobals: list ident.
  λint_fun: ertl_internal_function globals.
  λlabel.
  λliveafter: valuation.
  match lookup … (joint_if_code … int_fun) label with
  [ None      ⇒ ?
  | Some stmt ⇒ statement_semantics globals stmt (liveafter label)
  ].
  cases not_implemented (* XXX *)
qed.

definition liveafter ≝
  λglobals: list ident.
  λint_fun: ertl_internal_function globals.
  λlivebefore: label → ?.
  λlabel.
  λliveafter: valuation.
  match lookup … (joint_if_code … int_fun) label with
  [ None      ⇒ ?
  | Some stmt ⇒ set_fold ? ? (λsuccessor. λaccu: register_lattice.
      lattice_join (livebefore successor liveafter) accu)
      (statement_successors globals stmt) lattice_bottom
  ].
  cases not_implemented (* XXX *)
qed.

definition analyse ≝
  λglobals.
  λint_fun.
    fix_lfp (liveafter globals int_fun (livebefore globals int_fun)).