path: root/scheduling/RTLpathLivegen.v

(** 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.

(* FIXME - what about trap? *)
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 (* TODO jumptable ? *)
  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.

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 inst_checker (pm: path_map) (alive: 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 alive) 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 alive) pc' tt
   | Ijumptable arg tbl =>
      ASSERT Regset.mem arg alive IN
      ASSERT exit_list_checker pm alive tbl IN
      Some tt
   | Ireturn optarg =>
      ASSERT (reg_option_mem optarg) alive IN 
      Some tt
   | _ => 
      SOME res <- iinst_checker pm alive i IN
      exit_checker pm (fst res) (snd res) tt
   end.

Lemma inst_checker_wellformed (c:code) pc (pm: path_map) (alive: Regset.t) (i: instruction):
  inst_checker pm alive 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).
  intros X; exploit exit_checker_res; eauto.
  clear X. intros; subst; eauto.
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) 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.