include "ASM/Util.ma".
include "ERTLptr/ERTLptr.ma".
include "utilities/adt/set_adt.ma".
include "utilities/fixpoints.ma".

definition rl_included ≝
 λleft,right.
  set_subset … (eq_identifier RegisterTag) (\fst left) (\fst right) ∧
  set_subset … eq_Register (\snd left) (\snd right).

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))
 rl_included
 (λ_.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 pairwise : ∀A,B : Type[0]. ∀f : A → A → A. ∀g: B → B → B.
A × B → A × B → A × B≝
λA,B,f,g,c1,c2.〈f (\fst c1) (\fst c2) , g (\snd c1) (\snd c2)〉.

definition rl_join: register_lattice → register_lattice → register_lattice ≝ 
pairwise ?? (set_union …) (set_union …).

definition rl_diff: register_lattice → register_lattice → register_lattice ≝
pairwise ?? (set_diff …) (set_diff …).

definition defined ≝
  λglobals: list ident.
  λs: joint_statement ERTLptr 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_psingleton r1
      | 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
      | 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
        [ ertlptr_ertl 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
           ]
        | LOW_ADDRESS r1 l ⇒ rl_psingleton r1
        | HIGH_ADDRESS r1 l ⇒ rl_psingleton r1
        ]
      (* Potentially destroys all caller-save hardware registers. *)
      ]
    | CALL _ _ _ ⇒ 〈set_empty …, set_from_list … RegisterCallerSaved〉
    | COND r lbl_true ⇒ rl_bottom
    | COST_LABEL clabel ⇒ rl_bottom
    ]
  | final _ ⇒ rl_bottom
  | FCOND abs _ _ _ ⇒ Ⓧabs
  ].

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 ERTLptr 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
        [ ertlptr_ertl 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 ]
        | LOW_ADDRESS r1 l ⇒ rl_bottom
        | HIGH_ADDRESS r1 l ⇒ rl_bottom
        ]        
      (* Reads the hardware registers that are used to pass parameters. *)
      | _ ⇒ rl_bottom
      ]
    | COST_LABEL clabel ⇒ rl_bottom
    | CALL _ nparams _ ⇒ 〈set_empty …, set_from_list … (prefix ? nparams RegisterParams)〉
    | 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 False with [ ]
    ]
  | FCOND abs _ _ _ ⇒ Ⓧabs
  ].

definition eliminable_step ≝
λglobals: list ident.
λl: register_lattice.
λs: joint_step ERTLptr globals.
let pliveafter ≝ \fst l in
let hliveafter ≝ \snd l in
match s with
[ step_seq s ⇒
  match s with
  [ OP2 op2 r1 r2 r3 ⇒
    ¬(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)
  | OPACCS opaccs dr1 dr2 sr1 sr2 ⇒
    ¬(set_member … (eq_identifier …) dr1 pliveafter ∨
      set_member … (eq_identifier …) dr2 pliveafter ∨
      set_member … eq_Register RegisterCarry hliveafter)
  | OP1 op1 r1 r2 ⇒
    ¬set_member … (eq_identifier …) r1 pliveafter
  | ADDRESS _ _ r1 r2 ⇒
    ¬(set_member … (eq_identifier …) r1 pliveafter ∨
      set_member … (eq_identifier …) r2 pliveafter)
  | LOAD acc_a dpl dph ⇒
    ¬set_member ? (eq_identifier …) acc_a pliveafter
  | MOVE pair_reg ⇒
    ¬match \fst pair_reg with
      [ PSD p1 ⇒
        set_member … (eq_identifier …) p1 pliveafter
      | HDW h1 ⇒
        set_member … eq_Register h1 hliveafter
      ]
  | extension_seq ext ⇒
    match ext with
    [ ertlptr_ertl ext' ⇒
       match ext' with
       [ ertl_new_frame ⇒ false
       | ertl_del_frame ⇒ false
       | ertl_frame_size r ⇒
         ¬set_member ? (eq_identifier RegisterTag) r pliveafter
       ]
    | LOW_ADDRESS r1 l' ⇒
       ¬set_member ? (eq_identifier RegisterTag) r1 pliveafter
    | HIGH_ADDRESS r1 l' ⇒
       ¬set_member ? (eq_identifier RegisterTag) r1 pliveafter
    ]        
  | _ ⇒ false
  ]
| _ ⇒ false
].

definition eliminable ≝
  λglobals: list ident.
  λl: register_lattice.
  λs: joint_statement ERTLptr globals.
  let pliveafter ≝ \fst l in
  let hliveafter ≝ \snd l in
  match s with
  [ sequential seq _ ⇒ eliminable_step … l seq
  | _ ⇒ false
  ].

definition statement_semantics: ∀globals: list ident.
  joint_statement ERTLptr globals → register_lattice → register_lattice ≝
  λglobals.
  λstmt.
  λliveafter.
  if eliminable globals liveafter stmt then
    liveafter
  else
    rl_join (rl_diff liveafter (defined globals stmt)) (used globals stmt).

definition livebefore:
  ∀globals: list ident.
   joint_internal_function ERTLptr globals →
     valuation register_lattice → valuation register_lattice
≝
  λglobals: list ident.
  λint_fun: joint_internal_function ERTLptr globals.
  λliveafter: valuation register_lattice.
  λlabel.
  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 ERTLptr 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 liveafter successor)
  ].

definition analyse_liveness ≝
  λthe_fixpoint: fixpoint_computer. λ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
  ].