Require Import SetoidList.

Require Import Coqlib.
Require Import Time.
Require Import Errors.
Require Import Maps.
Require Import Lattice.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Globalenvs.
Require Import Op.
Require Import Registers.
Require Import Utils.
Require Import SSA.
Require Import SSAutils.
Require Import Kildall.
Require Import KildallComp.
Require Import Kildall_v2.
Require Import DLib.
Require Import Classical.

Local Open Scope string_scope.

Liveness analysis over SSA

Notation reg_live := SSARegSet.add.
Notation reg_dead := SSARegSet.remove.

Definition reg_option_live (or: option reg)
    (lv: SSARegSet.t) :=
  match or with
  | None => lv
  | Some r => reg_live r lv
  end.

Definition reg_sum_live (ros: reg + ident)
    (lv: SSARegSet.t) :=
  match ros with
  | inl r => reg_live r lv
  | inr s => lv
  end.

Fixpoint reg_list_live
    (rl: list reg) (lv: SSARegSet.t) {struct rl}
      : SSARegSet.t :=
  match rl with
  | nil => lv
  | r1 :: rs => reg_list_live rs (reg_live r1 lv)
  end.

Fixpoint reg_list_dead
   (rl: list reg) (lv: SSARegSet.t) {struct rl}
     : SSARegSet.t :=
  match rl with
  | nil => lv
  | r1 :: rs => reg_list_dead rs (reg_dead r1 lv)
  end.

Definition transfer_phib k pb after :=
  List.fold_left (fun lv pi =>
    match pi with
    | Iphi args _ =>
      match nth_error args k with
      | None => lv
      | Some r => reg_live r lv
      end
    end) pb after.

Definition transfer_instruction preds (phicode:phicode)
    (i : instruction) pc
    (after: SSARegSet.t) : SSARegSet.t :=
  match i with
  | Inop s =>
    match phicode ! s with
    | None => after
    | Some pb =>
      match index_pred preds pc s with
      | None => after
      | Some k => transfer_phib k pb after
      end
    end
  | Iop op args res s =>
      reg_list_live args (reg_dead res after)
  | Iload chunk addr args dst s =>
      reg_list_live args (reg_dead dst after)
  | Istore chunk addr args src s =>
      reg_list_live args (reg_live src after)
  | Icall sig ros args res s =>
      reg_list_live args
       (reg_sum_live ros (reg_dead res after))
  | Itailcall sig ros args =>
      reg_list_live args
        (reg_sum_live ros after)
  | Ibuiltin ef args (BR res) s =>
      reg_list_live (params_of_builtin_args args) (reg_dead res after)
  | Ibuiltin ef args res s =>
      reg_list_live (params_of_builtin_args args) after
  | Icond cond args ifso ifnot =>
      reg_list_live args after
  | Ijumptable arg tbl =>
      reg_live arg after
  | Ireturn optarg =>
      reg_option_live optarg after
  end.

Definition transfer_phib' (phib : phiblock)
    (after: SSARegSet.t) : SSARegSet.t :=
  List.fold_left (fun lv pi =>
    match pi with
    | Iphi _ res => reg_dead res lv
    end) phib after.

Definition transfer
    (f: function) preds (pc: node)
    (after: SSARegSet.t) : SSARegSet.t :=
  match f.(fn_code)!pc with
  | None =>
      SSARegSet.empty
  | Some i =>
      let lv := transfer_instruction preds f.(fn_phicode) i pc after in
      if peq pc f.(fn_entrypoint) then reg_list_dead f.(fn_params) lv
      else
        match (fn_phicode f) ! pc with
        | None => lv
        | Some phib =>
          transfer_phib' phib lv
        end
  end.


Module RegsetLat := LFSet(SSARegSet).
Module DS := Backward_Dataflow_Solver(RegsetLat)(NodeSetBackward).

Definition analyze (f: function): option (PMap.t SSARegSet.t) :=
  let preds :=
    time (Some "analyze ") "predecessors " (fun _ =>
      (make_predecessors (fn_code f) successors_instr)) tt
  in
  time (Some "analyze ") "fixpoint " (fun _ =>
    DS.fixpoint f.(fn_code) successors_instr (transfer f preds)) tt.


Lemma use_phicode_is_inop : forall f x pc
  (wf : wf_ssa_function f),
  use_phicode f x pc -> exists s, f.(fn_code) ! pc = Some (Inop s).

Lemma wf_ssa_use_and_def_same_pc_precise : forall f x pc,
  wf_ssa_function f ->
  use f x pc ->
  def f x pc ->
  assigned_phi_spec f.(fn_phicode) pc x \/ ext_params f x /\ use_phicode f x pc.

Lemma prop_dec_exists_dec : forall (c : code) (P : node -> Prop)
  (P_finite : forall pc, P pc -> c ! pc <> None)
  (P_dec : forall pc, P pc \/ ~ P pc),
  (exists pc, P pc) \/ ~ exists pc, P pc.

Lemma assigned_code_spec_finite : forall c pc x,
  assigned_code_spec c pc x ->
  c ! pc <> None.

Lemma assigned_code_spec_dec : forall c pc x,
  assigned_code_spec c pc x \/ ~ assigned_code_spec c pc x.

Lemma assigned_phi_spec_finite : forall c pc x,
  assigned_phi_spec c pc x -> c ! pc <> None.

Definition phi_eq (phi1 phi2 : phiinstruction) :=
  match phi1, phi2 with
  | Iphi _ r1, Iphi _ r2 => r1 = r2
  end.

Lemma phi_eq_dec : forall (phi1 phi2 : phiinstruction),
  { phi_eq phi1 phi2 } + { ~ phi_eq phi1 phi2 }.

Lemma assigned_phi_spec_dec : forall c pc x,
  assigned_phi_spec c pc x \/ ~ assigned_phi_spec c pc x.

Lemma make_predecessors_some : forall {A} (code:PTree.t A) successors s l,
  (make_predecessors code successors) ! s = Some l ->
  forall p, In p l -> exists i, code ! p = Some i.

Lemma fn_phicode_code : forall f,
  wf_ssa_function f ->
  forall pc block,
    (fn_phicode f) ! pc = Some block ->
    exists ins, (fn_code f) ! pc = Some ins.

Lemma ssa_use_exists_def : forall f,
  wf_ssa_function f ->
  forall x u,
  use f x u -> exists d, def f x d.



Inductive live_spec (f : function) (r : reg)
   (pc : node) : Prop :=
| live_spec_use :
    ~ def f r pc ->
    use f r pc ->
    live_spec f r pc
| live_spec_pred :
    forall pc',
    cfg f pc pc' ->
    ~ def f r pc ->
    live_spec f r pc' ->
    live_spec f r pc.

Inductive liveout_spec (f : function) (r : reg)
   (pc : node) : Prop :=
| liveout_spec_use :
    forall pc',
    cfg f pc pc' ->
    ~ def f r pc' ->
    use f r pc' ->
    liveout_spec f r pc
| liveout_spec_trans :
    forall pc',
    cfg f pc pc' ->
    ~ def f r pc' ->
    liveout_spec f r pc' ->
    liveout_spec f r pc.

Record wf_live1 f (live : reg -> node -> Prop) := MK_WF_LIVE1 {
    wf_live_incl1 : forall pc pc' x,
      cfg f pc pc' ->
      live x pc' ->
      live x pc \/ def f x pc;

    wf_live_use1 : forall pc x, use f x pc -> ~ def f x pc -> live x pc
  }.

Record wf_live2 f (live_in live_out : reg -> node -> Prop):= MK_WF_LIVE2 {
    wf_liveout_incl2 : forall pc pc' x,
      cfg f pc pc' ->
      live_in x pc' ->
      live_out x pc ;

    wf_livein_incl2 : forall pc x,
      ~ def f x pc ->
      live_out x pc ->
      live_in x pc ;

    wf_live_use2 : forall pc x,
      use f x pc ->
      ~ def f x pc ->
      live_in x pc
  }.

Definition wf_live3 f (live : reg -> node -> Prop) :=
  forall r pc,
  liveout_spec f r pc ->
  live r pc.

Definition wf_live4 f (live : reg -> node -> Prop) :=
  forall r pc,
  live_spec f r pc ->
  live r pc.

Lemma liveout_live : forall f (wf : wf_ssa_function f),
  forall r pc pc',
  cfg f pc pc' ->
  live_spec f r pc' ->
  liveout_spec f r pc.

Lemma live_liveout :
  forall f pc x,
  ~ def f x pc ->
  liveout_spec f x pc ->
  live_spec f x pc.

Lemma live_spec_exists_def : forall f (wf : wf_ssa_function f) r pc,
  live_spec f r pc ->
  exists pc', def f r pc'.

Lemma liveout_spec_exists_def : forall f (wf : wf_ssa_function f) r pc,
  liveout_spec f r pc ->
  exists pc', def f r pc'.

Lemma live_wf_live1 : forall f (wf : wf_ssa_function f),
  wf_live1 f (live_spec f).

Lemma live_wf_live2 : forall f (wf : wf_ssa_function f),
  wf_live2 f (live_spec f) (liveout_spec f).

Lemma wf_live2_wf_live1 : forall f (wf : wf_ssa_function f) live_in live_out,
  wf_live2 f live_in live_out ->
  wf_live1 f live_in.

Lemma wf_live2_wf_live3 : forall f (wf : wf_ssa_function f) live_in live_out,
  wf_live2 f live_in live_out ->
  wf_live3 f live_out.

Lemma wf_live2_wf_live4 : forall f (wf : wf_ssa_function f) live_in live_out,
  wf_live2 f live_in live_out ->
  wf_live4 f live_in.

Lemma wf_live1_wf_live4 : forall f (wf : wf_ssa_function f) live,
  wf_live1 f live ->
  wf_live4 f live.

Lemma live_spec_exists_path : forall f (wf : wf_ssa_function f) r pc,
  live_spec f r pc ->
  exists d u l,
  def f r d /\
  use f r u /\
  SSApath f (Dom.PState pc) l (Dom.PState u) /\
  ~ In d (l ++ cons u nil).

Lemma liveout_spec_exists_path : forall f (wf : wf_ssa_function f) r pc,
  liveout_spec f r pc ->
  exists d u l,
  def f r d /\
  use f r u /\
  SSApath f (Dom.PState pc) (pc::l) (Dom.PState u) /\
  ~ In d (l ++ u :: nil).

Lemma exists_path_live_spec : forall f (wf : wf_ssa_function f) r d u pc l,
  def f r d ->
  use f r u ->
  SSApath f (Dom.PState pc) l (Dom.PState u) ->
  ~ In d (l ++ u :: nil) ->
  live_spec f r pc.

Lemma exists_path_liveout_spec : forall f (wf : wf_ssa_function f) r d u pc l,
  def f r d ->
  use f r u ->
  SSApath f (Dom.PState pc) (pc::l) (Dom.PState u) ->
  ~ In d (l ++ u :: nil) ->
  liveout_spec f r pc.

Lemma live_spec_not_def : forall f r d pc,
  def f r d ->
  live_spec f r pc ->
  d <> pc.

Lemma live_spec_reached : forall f (wf : wf_ssa_function f) r pc,
  live_spec f r pc ->
  reached f pc.

Lemma liveout_spec_reached : forall f (wf : wf_ssa_function f) r pc,
  liveout_spec f r pc ->
  reached f pc.

Lemma live_spec_strict : forall f (wf : wf_ssa_function f) r d pc,
  def f r d ->
  live_spec f r pc ->
  sdom f d pc.

Lemma liveout_spec_strict : forall f (wf : wf_ssa_function f) r d pc,
  def f r d ->
  liveout_spec f r pc ->
  dom f d pc.

Corollary live_spec_no_entry : forall f (wf : wf_ssa_function f) r,
  ~ live_spec f r f.(fn_entrypoint).

Section WF_LIVE.

Variable f : function.
Variable wf : wf_ssa_function f.

Notation preds := (make_predecessors (fn_code f) successors_instr).

Definition Lin := (fun pc live_out => (transfer f preds pc (live_out pc))).

Definition Lout {A: Type} := (fun (live: PMap.t A) pc => live # pc).

Lemma reg_list_live_incl : forall x l s,
    SSARegSet.In x s ->
    SSARegSet.In x (reg_list_live l s).

Lemma reg_list_live_incl_2 : forall x l s,
    In x l ->
    SSARegSet.In x (reg_list_live l s).

Lemma reg_list_dead_not_in : forall l r s,
  SSARegSet.In r s ->
  ~ In r l ->
  SSARegSet.In r (reg_list_dead l s).

Lemma reg_sum_live_incl : forall x ros s,
  SSARegSet.In x s ->
  SSARegSet.In x (reg_sum_live ros s).

Lemma reg_option_live_incl : forall x or s,
  SSARegSet.In x s ->
  SSARegSet.In x (reg_option_live or s).

Lemma OP2_eq : forall r1 r2, OP2.eq r1 r2 <-> r1 = r2.

Lemma liveout_incl : forall live, analyze f = Some live ->
    forall pc pc',
    cfg f pc pc' ->
    SSARegSet.Subset (Lin pc' (Lout live)) (Lout live pc).

Lemma transfer_phib_livein_incl : forall live k phib,
    SSARegSet.Subset live (transfer_phib k phib live).

Lemma transfer_phib'_livein_incl : forall live pc phib x,
    f.(fn_phicode) ! pc = Some phib ->
    SSARegSet.In x live ->
    ~ def f x pc ->
    SSARegSet.In x (transfer_phib' phib live).

Lemma transfer_instruction_livein_incl : forall live i pc x,
    f.(fn_code) ! pc = Some i ->
    SSARegSet.In x live ->
    ~ def f x pc ->
    SSARegSet.In x (transfer_instruction preds (fn_phicode f) i pc live).

Lemma livein_incl : forall live pc x
    (Hincl : forall x, SSARegSet.In x (Lout live pc) -> f.(fn_code) ! pc <> None),
    SSARegSet.In x (Lout live pc) ->
    ~ def f x pc ->
    SSARegSet.In x (Lin pc (Lout live)).

Lemma analyze_some : forall live, analyze f = Some live ->
  forall pc x,
  SSARegSet.In x (Lout live pc) ->
  f.(fn_code) ! pc <> None.

Lemma transfer_phib_live_use : forall live k phib args dst x,
  In (Iphi args dst) phib ->
  nth_error args k = Some x ->
  SSARegSet.In x (transfer_phib k phib live).

Lemma transfer_instruction_live_use : forall live i pc x,
    f.(fn_code) ! pc = Some i ->
    use f x pc ->
    SSARegSet.In x (transfer_instruction preds (fn_phicode f) i pc live).

Lemma live_use : forall live pc x,
    ~ def f x pc ->
    use f x pc ->
    SSARegSet.In x (Lin pc (Lout live)).

Lemma live_wf_live : forall live, analyze f = Some live ->
  wf_live2 f
    (fun x pc => SSARegSet.In x (Lin pc (Lout live)))
    (fun x pc => SSARegSet.In x (Lout live pc)).

End WF_LIVE.