(** Building a RTLpath program with liveness annotation.
*)


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.
Proof.
  unfold exit_checker, path_entry.
  inversion_SOME path; simpl; congruence.
Qed.

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.
Proof.
  unfold exit_checker, path_entry.
  inversion_SOME path; try_simplify_someHyps.
  inversion_ASSERT; try_simplify_someHyps.
Qed.

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.
Proof.
  destruct i; simpl; try_simplify_someHyps; subst.
  inversion_ASSERT; try_simplify_someHyps.
Qed.

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.
Proof.
  destruct i; simpl; try_simplify_someHyps; subst;
  repeat (inversion_ASSERT); try_simplify_someHyps.
  intros; exploit exit_checker_res; eauto.
  intros; subst. simpl; auto.
Qed.

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.
Proof.
  induction ps; simpl; try_simplify_someHyps.
  inversion_SOME i; inversion_SOME res'.
  intros. eapply wf_internal_node; eauto.
  * eapply iinst_checker_default_succ; eauto.
  * intros; eapply iinst_checker_path_entry; eauto.
Qed.


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).
Proof.
  induction path; simpl.
  + try_simplify_someHyps.
  + intros alive pc res.
    inversion_SOME i; intros INST.
    inversion_SOME res0; intros ICHK IPCHK.
    rewrite INST.
    erewrite iinst_checker_default_succ; eauto.
Qed.

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.

(* NB: definition following [regmap_setres] in [RTL.step] semantics *)
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.
Proof.
  destruct o; simpl; intuition. 
  - eauto.
  - firstorder. try_simplify_someHyps.
Qed.

Lemma lazy_and_Some_tt_true (o: option unit) (b: bool): o &&& b = true <-> o = Some tt /\ b = true.
Proof.
   intros; rewrite lazy_and_Some_true; firstorder.
   destruct x; auto.
Qed.


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.
Proof.
  intros EXIT PC; induction l; intuition.
  simpl in * |-. rewrite lazy_and_Some_tt_true in EXIT.
  firstorder (subst; eauto).
Qed.

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.
Proof.
  intros CHECK PC. eapply wf_last_node; eauto.
  clear c pc PC. intros pc PC.
  destruct i; simpl in * |- *; intuition (subst; eauto);
  try (generalize CHECK; clear CHECK; try (inversion_SOME path); repeat inversion_ASSERT; try_simplify_someHyps).
Qed.

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.
Proof.
  unfold inst_checker.
  destruct (iinst_checker pm alive i) as [[alive0 pc0]|] eqn: CHECK1; simpl.
  - simpl; intros CHECK2 PC. eapply wf_last_node; eauto.
    destruct i; simpl in * |- *; intuition (subst; eauto);
    try (generalize CHECK2 CHECK1; clear CHECK1 CHECK2; try (inversion_SOME path); repeat inversion_ASSERT; try_simplify_someHyps).
    intros PC CHECK1 CHECK2. 
    intros; exploit exit_checker_res; eauto.
    intros X; inversion X. intros; subst; eauto.
  - simpl; intros CHECK2 PC. eapply final_inst_checker_wellformed; eauto.
    generalize CHECK2. clear CHECK2. inversion_ASSERT. try_simplify_someHyps.
Qed.

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.
Proof.
  unfold path_checker.
  inversion_SOME res.
  inversion_SOME i.
  intros; eapply ipath_checker_wellformed; eauto.
  eapply inst_checker_wellformed; eauto.
Qed.

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.
Proof.
  intros CHECKER e H; induction l as [|(pc & path) l]; intuition.
  simpl in * |- *. rewrite lazy_and_Some_tt_true in CHECKER. intuition (subst; auto).
Qed.

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.
Proof.
  unfold function_checker; rewrite lazy_and_Some_true.
  intros (ENTRY & PATH) PC.
  exploit list_path_checker_correct; eauto.
  - eapply PTree.elements_correct; eauto.
  - simpl; auto.
Qed.

Lemma function_checker_wellformed_path_map f pm:
  function_checker f pm = true -> wellformed_path_map f.(fn_code) pm.
Proof.
  unfold wellformed_path_map.
  intros; eapply path_checker_wellformed; eauto.
  intros; eapply function_checker_correct; eauto.
Qed.

Lemma function_checker_path_entry f pm:
  function_checker f pm = true -> path_entry pm (f.(fn_entrypoint)).
Proof.
  unfold function_checker; rewrite lazy_and_Some_true;
  unfold path_entry. firstorder congruence.
Qed.

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.
Obligation 2.
  apply function_checker_wellformed_path_map; auto.
Qed.
Obligation 3.
  unfold liveness_ok_function; simpl; intros; intuition.
  apply function_checker_correct; auto.
Qed.

Definition transf_fundef (f: RTL.fundef) : res fundef :=
  transf_partial_fundef (fun f => ` (transf_function f)) f.

Inductive liveness_ok_fundef: fundef -> Prop :=
  | liveness_ok_Internal f: liveness_ok_function f -> liveness_ok_fundef (Internal f)
  | liveness_ok_External ef: liveness_ok_fundef (External ef).

Lemma transf_fundef_correct f f':
  transf_fundef f = OK f' -> (liveness_ok_fundef f') /\ fundef_RTL f' = f.
Proof.
  intros TRANSF; destruct f; simpl; monadInv TRANSF.
  - destruct (transf_function f) as [res H]; simpl in * |- *; auto.
    destruct (H _ EQ).
    intuition subst; auto. apply liveness_ok_Internal; auto.
  - intuition. apply liveness_ok_External; auto.
Qed.

Definition transf_program (p: RTL.program) : res program :=
  transform_partial_program transf_fundef p.