Require Import Coqlib.
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 RTL.
Require Import Kildall.
Require Import Locations.
Require Import Conventions.
Require Import DLib.



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

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

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

Fixpoint reg_list_live
             (rl: list reg) (lv: Regset.t) {struct rl} : Regset.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: Regset.t) {struct rl} : Regset.t :=
  match rl with
  | nil => lv
  | r1 :: rs => reg_list_dead rs (reg_dead r1 lv)
  end.

Definition transfer
            (f: RTL.function) (pc: node) (after: Regset.t) : Regset.t :=
  match f.(fn_code)!pc with
  | None =>
      Regset.empty
  | Some i =>
      match i with
      | Inop s =>
          after
      | 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 Regset.empty)
      | Ibuiltin ef args res s =>
          reg_list_live args (reg_dead res after)
      | Icond cond args ifso ifnot =>
          reg_list_live args after
      | Ijumptable arg tbl =>
          reg_live arg after
      | Ireturn optarg =>
          reg_option_live optarg Regset.empty
      end
  end.


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

Definition analyze (f: RTL.function): option (PMap.t Regset.t) :=
  DS.fixpoint (successors f) (transfer f) nil.

Well-formedness condition for a liveness analysis

Section WF_LIVE.

  Variable f: RTL.function.
  
  Definition Lin := (fun pc live_out => (transfer f pc (live_out pc))).
  
  Definition Lout {A: Type} := (fun (live: PMap.t A) pc => live # pc).

Auxiliary lemmas about analyze

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

  Lemma reg_list_live_cases : forall x l s,
    Regset.In x (reg_list_live l s) ->
    (Regset.In x s) \/ In x l.
    
  Inductive def (pc:node) : reg -> Prop :=
  | AIop: forall op args dst succ,
    (fn_code f)!pc = Some (Iop op args dst succ) ->
    def pc dst
  | AIload: forall chunk addr args dst succ,
    (fn_code f)!pc = Some (Iload chunk addr args dst succ) ->
    def pc dst
  | AIcall: forall sig fn args dst succ,
    (fn_code f)!pc = Some (Icall sig fn args dst succ) ->
    def pc dst
  | AIbuiltin: forall fn args dst succ,
    (fn_code f)!pc = Some (Ibuiltin fn args dst succ) ->
    def pc dst.

  Inductive use (pc:node): reg -> Prop :=
  | UIop: forall arg op args dst s,
    (fn_code f) !pc = Some (Iop op args dst s) -> In arg args -> use pc arg
  | UIload: forall arg chk adr args dst s,
    (fn_code f) !pc = Some (Iload chk adr args dst s) -> In arg args -> use pc arg
  | UIcond: forall arg cond args s s',
    (fn_code f) !pc = Some (Icond cond args s s') -> In arg args -> use pc arg
  | UIbuiltin: forall arg ef args dst s,
    (fn_code f) !pc = Some (Ibuiltin ef args dst s) -> In arg args -> use pc arg
  | UIstore1: forall arg chk adr args src s,
    (fn_code f) !pc = Some (Istore chk adr args src s) -> In arg args -> use pc arg
  | UIstore2: forall chk adr args src s,
    (fn_code f) !pc = Some (Istore chk adr args src s) -> use pc src
  | UIcall: forall arg sig r args dst s,
    (fn_code f) !pc = Some (Icall sig (inl ident r) args dst s) -> In arg (r::args) -> use pc arg
  | UItailcall: forall arg sig r args,
    (fn_code f) !pc = Some (Itailcall sig (inl ident r) args) -> In arg (r::args) -> use pc arg
  | UIcall2: forall arg sig id args dst s,
    (fn_code f) !pc = Some (Icall sig (inr reg id) args dst s) -> In arg args -> use pc arg
  | UItailcall2: forall arg sig id args,
    (fn_code f) !pc = Some (Itailcall sig (inr reg id) args) -> In arg args -> use pc arg
  | UIjump: forall arg tbl,
    (fn_code f) !pc = Some (Ijumptable arg tbl) -> use pc arg
  | UIret: forall arg,
    (fn_code f) !pc = Some (Ireturn (Some arg)) -> use pc arg.

  Inductive Live (pc:node) (v:reg) : Prop :=
    | Live_Inop : forall pc',
      (fn_code f) ! pc = Some (Inop pc') ->
      Live pc' v -> Live pc v
    | Live_Iop : forall op args res pc',
      (fn_code f) ! pc = Some (Iop op args res pc') ->
      Live pc' v -> v<> res -> Live pc v
    | Live_Iload : forall chunk addr args dst pc',
      (fn_code f) ! pc = Some (Iload chunk addr args dst pc') ->
      Live pc' v -> v<> dst -> Live pc v
    | Live_Icond1 : forall cond args ifso ifnot,
      (fn_code f) ! pc = Some (Icond cond args ifso ifnot) ->
      Live ifso v -> Live pc v
    | Live_Icond2 : forall cond args ifso ifnot,
      (fn_code f) ! pc = Some (Icond cond args ifso ifnot) ->
      Live ifnot v -> Live pc v
    | Live_Ibuiltin : forall ef args res pc',
      (fn_code f) ! pc = Some (Ibuiltin ef args res pc') ->
      Live pc' v -> v<> res -> Live pc v
    | Live_Ijumptable : forall arg tbl pc',
      (fn_code f) ! pc = Some (Ijumptable arg tbl) ->
      In pc' tbl ->
      Live pc' v -> Live pc v
    | Live_use : use pc v -> Live pc v.

  Lemma build_live_correct: forall live,
    analyze f = Some live ->
    forall n v,
      Live n v -> Regset.In v (Lin n (Lout live)).

End WF_LIVE.