Module RTLpathLivegen

Require Import Coqlib.
Require Import Maps.
Require Import Lattice.
Require Import AST.
Require Import Op.
Require Import Registers.
Require Import Globalenvs Smallstep RTL RTLpath.
Require Import Bool Errors.
Require Import Program.

Local Open Scope lazy_bool_scope.

Local Open Scope option_monad_scope.

Axiom build_path_map: RTL.function -> path_map.

Extract Constant build_path_map => "RTLpathLivegenaux.build_path_map".

Fixpoint list_mem (rl: list reg) (alive: Regset.t) {struct rl}: bool :=
  match rl with
  | nil => true
  | r1 :: rs => Regset.mem r1 alive &&& list_mem rs alive
  end.

Definition exit_checker {A} (pm: path_map) (alive: Regset.t) (pc: node) (v:A): option A :=
   SOME path <- pm!pc IN
   ASSERT Regset.subset path.(input_regs) alive IN
   Some v.

Lemma exit_checker_path_entry A (pm: path_map) (alive: Regset.t) (pc: node) (v:A) res:
  exit_checker pm alive pc v = Some res -> path_entry pm pc.

Lemma exit_checker_res A (pm: path_map) (alive: Regset.t) (pc: node) (v:A) res:
  exit_checker pm alive pc v = Some res -> v=res.

Definition iinst_checker (pm: path_map) (alive: Regset.t) (i: instruction): option (Regset.t * node) :=
  match i with
  | Inop pc' => Some (alive, pc')
  | Iop op args dst pc' =>
      ASSERT list_mem args alive IN
      Some (Regset.add dst alive, pc')
  | Iload _ chunk addr args dst pc' =>
      ASSERT list_mem args alive IN
      Some (Regset.add dst alive, pc')
  | Istore chunk addr args src pc' =>
      ASSERT Regset.mem src alive IN
      ASSERT list_mem args alive IN
      Some (alive, pc')
  | Icond cond args ifso ifnot _ =>
      ASSERT list_mem args alive IN
      exit_checker pm alive ifso (alive, ifnot)
  | _ => None
  end.


Local Hint Resolve exit_checker_path_entry: core.

Lemma iinst_checker_path_entry (pm: path_map) (alive: Regset.t) (i: instruction) res pc:
  iinst_checker pm alive i = Some res ->
  early_exit i = Some pc -> path_entry pm pc.

Lemma iinst_checker_default_succ (pm: path_map) (alive: Regset.t) (i: instruction) res pc:
  iinst_checker pm alive i = Some res ->
  pc = snd res ->
  default_succ i = Some pc.

Fixpoint ipath_checker (ps:nat) (f: RTL.function) (pm: path_map) (alive: Regset.t) (pc:node): option (Regset.t * node) :=
  match ps with
  | O => Some (alive, pc)
  | S p =>
    SOME i <- f.(fn_code)!pc IN
    SOME res <- iinst_checker pm alive i IN
    ipath_checker p f pm (fst res) (snd res)
  end.

Lemma ipath_checker_wellformed f pm ps: forall alive pc res,
   ipath_checker ps f pm alive pc = Some res ->
   wellformed_path f.(fn_code) pm 0 (snd res) ->
   wellformed_path f.(fn_code) pm ps pc.


Lemma ipath_checker_default_succ (f: RTLpath.function) path: forall alive pc res,
  ipath_checker path f (fn_path f) alive pc = Some res
  -> nth_default_succ (fn_code f) path pc = Some (snd res).

Definition reg_option_mem (or: option reg) (alive: Regset.t) :=
  match or with None => true | Some r => Regset.mem r alive end.

Definition reg_sum_mem (ros: reg + ident) (alive: Regset.t) :=
  match ros with inl r => Regset.mem r alive | inr s => true end.

Definition reg_builtin_res (res: builtin_res reg) (alive: Regset.t): Regset.t :=
  match res with
  | BR r => Regset.add r alive
  | _ => alive
  end.

Fixpoint exit_list_checker (pm: path_map) (alive: Regset.t) (l: list node): bool :=
   match l with
   | nil => true
   | pc::l' => exit_checker pm alive pc tt &&& exit_list_checker pm alive l'
   end.

Lemma lazy_and_Some_true A (o: option A) (b: bool): o &&& b = true <-> (exists v, o = Some v) /\ b = true.

Lemma lazy_and_Some_tt_true (o: option unit) (b: bool): o &&& b = true <-> o = Some tt /\ b = true.


Lemma exit_list_checker_correct pm alive l pc:
  exit_list_checker pm alive l = true -> List.In pc l -> exit_checker pm alive pc tt = Some tt.

Local Hint Resolve exit_list_checker_correct: core.

Definition final_inst_checker (pm: path_map) (alive por: Regset.t) (i: instruction): option unit :=
   match i with
   | Icall sig ros args res pc' =>
      ASSERT list_mem args alive IN
      ASSERT reg_sum_mem ros alive IN
      exit_checker pm (Regset.add res por) pc' tt
   | Itailcall sig ros args =>
      ASSERT list_mem args alive IN
      ASSERT reg_sum_mem ros alive IN
      Some tt
   | Ibuiltin ef args res pc' =>
      ASSERT list_mem (params_of_builtin_args args) alive IN
      exit_checker pm (reg_builtin_res res por) pc' tt
   | Ijumptable arg tbl =>
      ASSERT Regset.mem arg alive IN
      ASSERT exit_list_checker pm por tbl IN
      Some tt
   | Ireturn optarg =>
      ASSERT (reg_option_mem optarg) alive IN
      Some tt
   | _ => None
   end.

Lemma final_inst_checker_wellformed (c:code) pc (pm: path_map) (alive por: Regset.t) (i: instruction):
  final_inst_checker pm alive por i = Some tt ->
  c!pc = Some i -> wellformed_path c pm 0 pc.

Definition inst_checker (pm: path_map) (alive por: Regset.t) (i: instruction): option unit :=
   match iinst_checker pm alive i with
   | Some res =>
      ASSERT Regset.subset por (fst res) IN
      exit_checker pm por (snd res) tt
   | _ =>
      ASSERT Regset.subset por alive IN
      final_inst_checker pm alive por i
   end.

Lemma inst_checker_wellformed (c:code) pc (pm: path_map) (alive por: Regset.t) (i: instruction):
  inst_checker pm alive por i = Some tt ->
  c!pc = Some i -> wellformed_path c pm 0 pc.

Definition path_checker (f: RTL.function) pm (pc: node) (path:path_info): option unit :=
   SOME res <- ipath_checker (path.(psize)) f pm (path.(input_regs)) pc IN
   SOME i <- f.(fn_code)!(snd res) IN
   inst_checker pm (fst res) (path.(pre_output_regs)) i.

Lemma path_checker_wellformed f pm pc path:
   path_checker f pm pc path = Some tt -> wellformed_path (f.(fn_code)) pm (path.(psize)) pc.

Fixpoint list_path_checker f pm (l:list (node*path_info)): bool :=
  match l with
  | nil => true
  | (pc, path)::l' =>
      path_checker f pm pc path &&& list_path_checker f pm l'
  end.

Lemma list_path_checker_correct f pm l:
  list_path_checker f pm l = true -> forall e, List.In e l -> path_checker f pm (fst e) (snd e) = Some tt.

Definition function_checker (f: RTL.function) pm: bool :=
  pm!(f.(fn_entrypoint)) &&& list_path_checker f pm (PTree.elements pm).

Lemma function_checker_correct f pm pc path:
  function_checker f pm = true ->
  pm!pc = Some path ->
  path_checker f pm pc path = Some tt.

Lemma function_checker_wellformed_path_map f pm:
  function_checker f pm = true -> wellformed_path_map f.(fn_code) pm.

Lemma function_checker_path_entry f pm:
  function_checker f pm = true -> path_entry pm (f.(fn_entrypoint)).

Definition liveness_ok_function (f: function): Prop :=
  forall pc path, f.(fn_path)!pc = Some path -> path_checker f f.(fn_path) pc path = Some tt.

Program Definition transf_function (f: RTL.function): { r: res function | forall f', r = OK f' -> liveness_ok_function f' /\ f'.(fn_RTL) = f } :=
  let pm := build_path_map f in
  match function_checker f pm with
  | true => OK {| fn_RTL := f; fn_path := pm |}
  | false => Error(msg "RTLpathGen: function_checker failed")
  end.
Obligation 1.
  apply function_checker_path_entry; auto.
Qed.