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

definition register_lattice : property_lattice ≝
mk_property_lattice
 ((set register) × (set Register))
 〈set_empty …, set_empty …〉
 (λleft.
  λright.
  set_equal … (eq_identifier ?) (\fst left) (\fst right) ∧
  set_equal … eq_Register (\snd left) (\snd right))
 (λleft.
  λright.
  set_subset … (eq_identifier ?) (\fst left) (\fst right) ∧
  set_subset … eq_Register (\snd left) (\snd right))
 (λ_.false).

definition rl_bottom ≝ l_bottom register_lattice.
definition rl_psingleton: register → register_lattice ≝
  λr.
    〈set_singleton … r, set_empty …〉.
definition rl_hsingleton: Register → register_lattice ≝
  λr.
    〈set_empty …, set_singleton … r〉.

definition rl_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 rl_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 defined ≝
  λglobals: list ident.
  λs: joint_statement ERTL globals.
  match s with
  [ sequential seq l ⇒
    match seq with
    [ step_seq s ⇒
      match s with
      [ OP2 op2 r1 r2 _ ⇒
        match op2 with
        [ Add ⇒ rl_join (rl_hsingleton RegisterCarry) (rl_psingleton r1)
        | Addc ⇒ rl_join (rl_hsingleton RegisterCarry) (rl_psingleton r1)
        | Sub ⇒ rl_join (rl_hsingleton RegisterCarry)  (rl_psingleton r1)
        | _ ⇒ rl_psingleton r1
        ]
      | CLEAR_CARRY ⇒ rl_hsingleton RegisterCarry
      | SET_CARRY ⇒ rl_hsingleton RegisterCarry
      | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
        rl_join (rl_join (rl_psingleton dr1)
                                    (rl_psingleton dr2))
                      (rl_hsingleton RegisterCarry)
      | OP1 op1 r1 r2 ⇒ rl_join (rl_psingleton r1) (rl_psingleton r2)
      | POP r ⇒ rl_psingleton r
      | ADDRESS _ _ r1 r2 ⇒ rl_join (rl_psingleton r1) (rl_psingleton r2)
      | LOAD r _ _ ⇒ rl_psingleton r
      | COMMENT c ⇒ rl_bottom
      | STORE acc_a dpl dph ⇒ rl_bottom
      | COST_LABEL clabel ⇒ rl_bottom
      | PUSH r ⇒ rl_bottom
      | MOVE pair_reg ⇒
        (* first register relevant only *)
        match \fst pair_reg with
        [ PSD p ⇒ rl_psingleton p
        | HDW h ⇒ rl_hsingleton h
        ]
      | extension_seq ext ⇒
        match ext with
        [ ertl_new_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
        | ertl_del_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
        | ertl_frame_size r ⇒ rl_psingleton r
        ]
      (* Potentially destroys all caller-save hardware registers. *)
      | CALL_ID id _ _ ⇒ 〈set_empty …, set_from_list … RegisterCallerSaved〉
      | extension_call abs ⇒ match abs in void with [ ]
      ]
    | COND r lbl_true ⇒ rl_bottom
    ]
  | final _ ⇒ rl_bottom
  ].

definition ret_regs ≝ set_from_list … RegisterRets.

definition rl_arg : psd_argument → register_lattice ≝
  λarg.match arg with
  [ Imm _ ⇒ rl_bottom
  | Reg r ⇒ rl_psingleton r
  ].

definition used ≝
  λglobals: list ident.
  λs: joint_statement ERTL globals.
  match s with
  [ sequential seq l ⇒
    match seq with
    [ step_seq s ⇒
      match s with
      [ OP2 op2 acc_a r1 r2 ⇒
        rl_join (rl_join (rl_arg r1) (rl_arg r2))
          (match op2 with
            [ Addc ⇒ rl_hsingleton RegisterCarry
            | Sub ⇒ rl_hsingleton RegisterCarry
            | _ ⇒ rl_bottom
            ])
      (* acc_a and acc_b *)
      | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
        rl_join (rl_arg sr1) (rl_arg sr2)
      | OP1 op1 r1 r2 ⇒ rl_psingleton r2
      | LOAD acc_a dpl dph ⇒ rl_join (rl_arg dpl) (rl_arg dph)
      | STORE acc_a dpl dph ⇒
        rl_join (rl_join (rl_arg acc_a) (rl_arg dpl)) (rl_arg dph)
      | PUSH r ⇒ rl_arg r
      | MOVE pair_reg ⇒
        let r2 ≝ \snd pair_reg in
        match r2 with
        [ Reg p ⇒
          match p with
          [ PSD r ⇒ rl_psingleton r
          | HDW r ⇒ rl_hsingleton r
          ]
        | Imm _ ⇒ rl_bottom
        ]
      | extension_seq ext ⇒
        match ext with
        [ ertl_new_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
        | ertl_del_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
        | ertl_frame_size r ⇒ rl_bottom
        ]
      (* Reads the hardware registers that are used to pass parameters. *)
      | CALL_ID _ nparams _ ⇒ 〈set_empty …, set_from_list … (prefix ? nparams RegisterParams)〉
      | extension_call abs ⇒ match abs in void with [ ]
      | _ ⇒ rl_bottom
      ]
    | COND r lbl_true ⇒ rl_psingleton r
    ]
  | final fin ⇒
    match fin with
    [ RETURN ⇒ 〈set_empty …, set_union … (set_from_list … RegisterCalleeSaved) ret_regs〉
    | GOTO l ⇒ rl_bottom
    | tailcall abs ⇒ match abs in void with [ ]
    ]
  ].

definition eliminable ≝
  λglobals: list ident.
  λl: register_lattice.
  λs: joint_statement ERTL globals.
  let pliveafter ≝ \fst l in
  let hliveafter ≝ \snd l in
  match s with
  [ sequential seq l ⇒
    match seq with
    [ step_seq s ⇒
      match s with
      [ OP2 op2 r1 r2 r3 ⇒
        if match op2 with
          [ Add ⇒ set_member … eq_Register RegisterCarry hliveafter
          | Addc ⇒ set_member … eq_Register RegisterCarry hliveafter
          | Sub ⇒ set_member … eq_Register RegisterCarry hliveafter
          | _ ⇒ false
          ] ∨ set_member … (eq_identifier …) r1 pliveafter
        then
          None ?
        else
          Some ? l
      | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
        if set_member … (eq_identifier …) dr1 pliveafter ∨
           set_member … (eq_identifier …) dr2 pliveafter ∨
           set_member … eq_Register RegisterCarry hliveafter then
          None ?
        else
          Some ? l
      | OP1 op1 r1 r2 ⇒
        if set_member … (eq_identifier …) r1 pliveafter then
          None ?
        else
          Some ? l
      | ADDRESS _ _ r1 r2 ⇒
        if set_member … (eq_identifier …) r1 pliveafter ∨
           set_member … (eq_identifier …) r2 pliveafter then
          None ?
        else
          Some ? l
      | LOAD acc_a dpl dph ⇒
        if set_member ? (eq_identifier …) acc_a pliveafter then
          None ?
        else
          Some ? l
      | MOVE pair_reg ⇒
        if match \fst pair_reg with
          [ PSD p1 ⇒
            set_member … (eq_identifier …) p1 pliveafter
          | HDW h1 ⇒
            set_member … eq_Register h1 hliveafter
          ] then
            None ?
          else
            Some ? l
      | extension_seq ext ⇒
        match ext with
        [ ertl_new_frame ⇒ None ?
        | ertl_del_frame ⇒ None ?
        | ertl_frame_size r ⇒
          if set_member ? (eq_identifier RegisterTag) r pliveafter then
            None ?
          else
            Some ? l
        ]
      | _ ⇒ None ?
      ]
    | COND _ _ ⇒ None ?
    ]
  | _ ⇒ None ?
  ].

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

definition livebefore ≝
  λglobals: list ident.
  λint_fun: joint_internal_function ERTL globals.
  λlabel.
  λliveafter: valuation register_lattice.
  match lookup ?? (joint_if_code … int_fun) label with
  [ None      ⇒ rl_bottom
  | Some stmt ⇒ statement_semantics globals stmt (liveafter label)
  ].

definition liveafter ≝
   λglobals: list ident.
  λint_fun: joint_internal_function ERTL globals.
  λlabel.
  λliveafter: valuation register_lattice.
 match lookup ?? (joint_if_code … int_fun) label with
  [ None      ⇒ rl_bottom
  | Some stmt ⇒
    \fold[rl_join,rl_bottom]_{successor ∈ stmt_labels … stmt}
      (livebefore globals int_fun successor liveafter)
  ].

definition analyse_liveness ≝
  λglobals.
  λint_fun.
    the_fixpoint ? (liveafter globals int_fun).

definition vertex ≝ register + Register.

definition plives : register → register_lattice → bool ≝
  λvertex.λprop.set_member ? (eq_identifier RegisterTag) vertex (\fst prop).
definition hlives : Register → register_lattice → bool ≝
  λvertex.λprop.set_member ? eq_Register vertex (\snd prop).

definition lives : vertex → register_lattice → bool ≝
  λvertex.
  match vertex with
  [ inl v ⇒ plives v
  | inr v ⇒ hlives v
  ].