path: root/scheduling/BTL_Livecheck.v

Require Import Coqlib Maps.
Require Import AST Integers Values Events Memory Globalenvs Smallstep Op Registers OptionMonad.
Require Import Errors RTL BTL BTLmatchRTL.

(** TODO: adapt stuff RTLpathLivegen *)

Local Open Scope lazy_bool_scope.

Local Open Scope option_monad_scope.

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

Definition exit_checker {A} (btl: code) (alive: Regset.t) (s: node) (v: A): option A :=
  SOME next <- btl!s IN
  ASSERT Regset.subset next.(input_regs) alive IN
  Some v.

Fixpoint exit_list_checker (btl: code) (alive: Regset.t) (l: list node): bool :=
   match l with
   | nil => true
   | s :: l' => exit_checker btl alive s true &&& exit_list_checker btl alive l'
   end.

Definition final_inst_checker (btl: code) (alive: Regset.t) (fin: final): option unit :=
  match fin with
  | Bgoto s =>
      exit_checker btl alive s tt
  | Breturn oreg =>
      ASSERT reg_option_mem oreg alive IN Some tt
  | Bcall _ ros args res s =>
      ASSERT list_mem args alive IN
      ASSERT reg_sum_mem ros alive IN
      exit_checker btl (Regset.add res alive) s tt
  | Btailcall _ ros args =>
      ASSERT list_mem args alive IN
      ASSERT reg_sum_mem ros alive IN Some tt
  | Bbuiltin _ args res s =>
      ASSERT list_mem (params_of_builtin_args args) alive IN
      exit_checker btl (reg_builtin_res res alive) s tt
  | Bjumptable arg tbl =>
      ASSERT Regset.mem arg alive IN
      ASSERT exit_list_checker btl alive tbl IN Some tt
  end.

Definition is_none {A} (oa: option A): bool :=
  match oa with
  | Some _ => false
  | None => true
  end.

Fixpoint body_checker (btl: code) (ib: iblock) (alive: Regset.t): option (Regset.t*option final) :=
  match ib with
  | Bseq ib1 ib2 =>
      SOME res <- body_checker btl ib1 alive IN
      ASSERT is_none (snd res) IN
      body_checker btl ib2 (fst res)
  | Bnop _ => Some (alive, None)
  | Bop _ args dest _ =>
      ASSERT list_mem args alive IN
      Some (Regset.add dest alive, None)
  | Bload _ _ _ args dest _ =>
      ASSERT list_mem args alive IN
      Some (Regset.add dest alive, None)
  | Bstore _ _ args src _ =>
      ASSERT Regset.mem src alive IN
      ASSERT list_mem args alive IN
      Some (alive, None)
  | Bcond _ args (BF (Bgoto s) _) (Bnop None) _ =>
      ASSERT list_mem args alive IN
      exit_checker btl alive s (alive, None)
  | BF fin _ => Some (alive, Some fin)
  | _ => None
  end.

Definition iblock_checker (btl: code) (ib: iblock) (alive: Regset.t) : option unit :=
  SOME res <- body_checker btl ib alive IN
  SOME fin <- snd res IN
  final_inst_checker btl (fst res) fin.

Fixpoint list_iblock_checker (btl: code) (l: list (node*iblock_info)): bool :=
  match l with
  | nil => true
  | (_, ibf) :: l' => iblock_checker btl ibf.(entry) ibf.(input_regs) &&& list_iblock_checker btl 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 list_iblock_checker_correct btl l: 
  list_iblock_checker btl l = true -> forall e, List.In e l -> iblock_checker btl (snd e).(entry) (snd e).(input_regs) = Some tt.
Proof.
  intros CHECKER e H; induction l as [|(n & ibf) l]; intuition.
  simpl in * |- *. rewrite lazy_and_Some_tt_true in CHECKER. intuition (subst; auto).
Qed.


Definition liveness_checker_bool (f: BTL.function): bool :=
  f.(fn_code)!(f.(fn_entrypoint)) &&& list_iblock_checker f.(fn_code) (PTree.elements f.(fn_code)).

Definition liveness_checker (f: BTL.function): res unit :=
  match liveness_checker_bool f with
  | true => OK tt
  | false => Error (msg "BTL_Livecheck: liveness_checker failed")
  end.

Lemma decomp_liveness_checker f:
  liveness_checker f = OK tt ->
  exists ibf, f.(fn_code)!(f.(fn_entrypoint)) = Some ibf /\
  list_iblock_checker f.(fn_code) (PTree.elements f.(fn_code)) = true.
Proof.
  intros LIVE; unfold liveness_checker in LIVE.
  destruct liveness_checker_bool eqn:EQL; try congruence.
  clear LIVE. unfold liveness_checker_bool in EQL.
  rewrite lazy_and_Some_true in EQL; destruct EQL as [[ibf ENTRY] LIST].
  eexists; split; eauto.
Qed.

Lemma liveness_checker_correct f n ibf:
  liveness_checker f = OK tt ->
  f.(fn_code)!n = Some ibf ->
  iblock_checker f.(fn_code) ibf.(entry) ibf.(input_regs) = Some tt.
Proof.
  intros LIVE PC.
  apply decomp_liveness_checker in LIVE; destruct LIVE as [ibf' [ENTRY LIST]].
  exploit list_iblock_checker_correct; eauto.
  - eapply PTree.elements_correct; eauto.
  - simpl; auto.
Qed.

Lemma liveness_checker_entrypoint f:
  liveness_checker f = OK tt ->
  f.(fn_code)!(f.(fn_entrypoint)) <> None.
Proof.
  intros LIVE; apply decomp_liveness_checker in LIVE; destruct LIVE as [ibf' [ENTRY LIST]].
  unfold not; intros CONTRA. congruence.
Qed.

Definition liveness_ok_function (f: BTL.function): Prop := liveness_checker f = OK tt.

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).

(** TODO: adapt stuff RTLpathLivegenproof *)

Local Notation ext alive := (fun r => Regset.In r alive).

Lemma regset_add_spec live r1 r2: Regset.In r1 (Regset.add r2 live) <-> (r1 = r2 \/ Regset.In r1 live).
Proof.
  destruct (Pos.eq_dec r1 r2).
  - subst. intuition; eapply Regset.add_1; auto.
  - intuition. 
    * right. eapply Regset.add_3; eauto.
    * eapply Regset.add_2; auto.
Qed.

Definition eqlive_reg (alive: Regset.elt -> Prop) (rs1 rs2: regset): Prop :=
 forall r, (alive r) -> rs1#r = rs2#r.

Inductive eqlive_stackframes: stackframe -> stackframe -> Prop :=
  | eqlive_stackframes_intro ibf res f sp pc rs1 rs2
      (LIVE: liveness_ok_function f)
      (ENTRY: f.(fn_code)!pc = Some ibf)
      (EQUIV: forall v, eqlive_reg (ext ibf.(input_regs)) (rs1 # res <- v) (rs2 # res <- v)):
       eqlive_stackframes (Stackframe res f sp pc rs1) (Stackframe res f sp pc rs2). 

Inductive eqlive_states: state -> state -> Prop :=
  | eqlive_states_intro 
      ibf st1 st2 f sp pc rs1 rs2 m
      (STACKS: list_forall2 eqlive_stackframes st1 st2)
      (LIVE: liveness_ok_function f)
      (PATH: f.(fn_code)!pc = Some ibf)
      (EQUIV: eqlive_reg (ext ibf.(input_regs)) rs1 rs2):
      eqlive_states (State st1 f sp pc rs1 m) (State st2 f sp pc rs2 m)
  | eqlive_states_call st1 st2 f args m
      (LIVE: liveness_ok_fundef f)
      (STACKS: list_forall2 eqlive_stackframes st1 st2):
      eqlive_states (Callstate st1 f args m) (Callstate st2 f args m)
  | eqlive_states_return st1 st2 v m
      (STACKS: list_forall2 eqlive_stackframes st1 st2):
      eqlive_states (Returnstate st1 v m) (Returnstate st2 v m).

(* continue to adapt stuff RTLpathLivegenproof *)

Section FSEM_SIMULATES_CFGSEM.

Variable prog: BTL.program.

Let ge := Genv.globalenv prog.

Hypothesis all_liveness_checker: forall b f, Genv.find_funct_ptr ge b = Some f -> liveness_ok_fundef f.

Local Hint Constructors eqlive_stackframes eqlive_states final_step list_forall2 step: core.

(*Lemma tr_inputs_eqlive f rs1 rs2 tbl or r
  (REGS: forall r, eqlive_reg (ext (input_regs ibf)) rs1 rs2)
  :eqlive_reg (tr_inputs f tbl or rs1) (tid f tbl or rs2).
Proof.
  unfold tid; rewrite tr_inputs_get.
  autodestruct.
   Qed.*)

Remark is_none_true {A} (fin: option A):
  is_none fin = true ->
  fin = None.
Proof.
  unfold is_none; destruct fin; congruence.
Qed.

Local Hint Resolve Regset.mem_2 Regset.subset_2: core.
Lemma lazy_and_true (b1 b2: bool): b1 &&& b2 = true <-> b1 = true /\ b2 = true.
Proof.
  destruct b1; simpl; intuition.
Qed.

Lemma list_mem_correct (rl: list reg) (alive: Regset.t):
  list_mem rl alive = true -> forall r, List.In r rl -> ext alive r.
Proof.
  induction rl; simpl; try rewrite lazy_and_true; intuition subst; auto.
Qed.

Lemma eqlive_reg_list (alive: Regset.elt -> Prop) args rs1 rs2: eqlive_reg alive rs1 rs2 -> (forall r, List.In r args -> (alive r)) -> rs1##args = rs2##args.
Proof.
  induction args; simpl; auto.
  intros EQLIVE ALIVE; rewrite IHargs; auto.
  unfold eqlive_reg in EQLIVE.
  rewrite EQLIVE; auto.
Qed.

Lemma eqlive_reg_listmem (alive: Regset.t) args rs1 rs2: eqlive_reg (ext alive) rs1 rs2 -> list_mem args alive = true -> rs1##args = rs2##args.
Proof.
  intros; eapply eqlive_reg_list; eauto.
  intros; eapply list_mem_correct; eauto.
Qed.

Lemma cfgsem2fsem_ibistep_simu sp f: forall rs1 m rs1' m' rs2 of ibf res,
  iblock_istep ge sp rs1 m ibf.(entry) rs1' m' of ->
  (*iblock_checker (fn_code f) ibf.(entry) ibf.(input_regs) = Some tt ->*)
  eqlive_reg (ext (input_regs ibf)) rs1 rs2 ->
  body_checker (fn_code f) ibf.(entry) ibf.(input_regs) = Some res ->
(*LIST : list_iblock_checker (fn_code f) (PTree.elements (fn_code f)) = true*)
  exists rs2', iblock_istep_run ge sp ibf.(entry) rs2 m = Some (out rs2' m' of).
Proof.
  induction 1; simpl; repeat inversion_ASSERT; intros; try_simplify_someHyps.
  - (* Bop *)
    intros.
    erewrite <- eqlive_reg_listmem; eauto.
    try_simplify_someHyps.
    (*
  (*- [> BF <]*)
    (*intros. inv H1; eexists; reflexivity.*)
  - (* Bseq stop *)
    admit. (*
    inversion_SOME res0.
    inversion_ASSERT; intros.
    exploit IHiblock_istep. unfold iblock_checker.
    rewrite H1. inv H0.
    inversion_SOME out1.
              try_simplify_someHyps.*)
  - inversion_SOME res0.
    inversion_ASSERT; intros.
    admit.
    (* TODO The first induction hyp should not be based on iblock_checker *)
    (* exploit IHiblock_istep1. unfold iblock_checker.
       rewrite H2. apply is_none_true in H1. rewrite H1. *)
  - (* Bcond *)
       admit.*)
Admitted.

Lemma cfgsem2fsem_finalstep_simu stk1 f sp rs1 m1 fin t s1 stk2 rs2 m2
  (FSTEP: final_step tid ge stk1 f sp rs1 m1 fin t s1)
  (STACKS: list_forall2 eqlive_stackframes stk1 stk2)
  : exists s2, final_step tr_inputs ge stk2 f sp rs2 m2 fin t s2
    /\ eqlive_states s1 s2.
Proof.
  destruct FSTEP.
  - (* Bgoto *)
    eexists; split; simpl. econstructor; eauto.
Admitted.

Lemma cfgsem2fsem_ibstep_simu stk1 stk2 f sp rs1 m rs2 ibf pc s1 t:
  iblock_step tid (Genv.globalenv prog) stk1 f sp rs1 m ibf.(entry) t s1 ->
  list_forall2 eqlive_stackframes stk1 stk2 ->
  eqlive_reg (ext (input_regs ibf)) rs1 rs2 ->
  liveness_ok_function f ->
  (fn_code f) ! pc = Some ibf ->
  exists s2 : state,
    iblock_step tr_inputs (Genv.globalenv prog) stk2 f sp rs2 m ibf.(entry) t s2 /\
    eqlive_states s1 s2.
Proof.
  intros STEP STACKS EQLIVE LIVE PC.
  unfold liveness_ok_function in LIVE.
  apply decomp_liveness_checker in LIVE; destruct LIVE as [ibf' [ENTRY LIST]].
  eapply PTree.elements_correct in PC as PCIN.
  eapply list_iblock_checker_correct in LIST as IBC; eauto.
  unfold iblock_checker in IBC. generalize IBC; clear IBC.
  inversion_SOME res; inversion_SOME fin; intros RES BODY FINAL.
  destruct STEP as (rs1' & m1' & fin' & ISTEP & FSTEP).
  exploit cfgsem2fsem_ibistep_simu; eauto.
  intros (rs2' & ISTEP2).
  rewrite <- iblock_istep_run_equiv in ISTEP2. clear ISTEP.
  exploit cfgsem2fsem_finalstep_simu; eauto.
  intros (s2 & FSTEP2 & STATES). clear FSTEP.
  unfold iblock_step. repeat eexists; eauto.
Qed.

Local Hint Constructors step: core.

Lemma cfgsem2fsem_step_simu s1 s1' t s2:
  step tid (Genv.globalenv prog) s1 t s1' ->
  eqlive_states s1 s2 ->
  exists s2' : state,
    step tr_inputs (Genv.globalenv prog) s2 t s2' /\
    eqlive_states s1' s2'.
Proof.
  destruct 1 as [stack ibf f sp n rs m t s ENTRY STEP | | | ]; intros STATES;
  try (inv STATES; inv LIVE; eexists; split; econstructor; eauto; fail).
  - inv STATES; simplify_someHyps.
    intros.
    exploit cfgsem2fsem_ibstep_simu; eauto.
    intros (s2 & STEP2 & EQUIV2). 
    eexists; split; eauto.
  - inv STATES; inv LIVE.
    apply liveness_checker_entrypoint in H0 as ENTRY.
    destruct ((fn_code f) ! (fn_entrypoint f)) eqn:EQENTRY; try congruence; eauto.
    eexists; split; repeat econstructor; eauto.
  - inv STATES.
    inversion STACKS as [|s1 st1 s' s2 STACK STACKS']; subst; clear STACKS.
    inv STACK.
    exists (State s2 f sp pc (rs2 # res <- vres) m); split.
    * apply exec_return.
    * eapply eqlive_states_intro; eauto.
Qed.

Theorem cfgsem2fsem: forward_simulation (cfgsem prog) (fsem prog).
Proof.
  eapply forward_simulation_step with eqlive_states; simpl; eauto.
  - destruct 1, f; intros; eexists; intuition eauto;
    repeat (econstructor; eauto).
  - intros s1 s2 r STATES FINAL; destruct FINAL.
    inv STATES; inv STACKS; constructor.
  - intros. eapply cfgsem2fsem_step_simu; eauto.
Qed.

End FSEM_SIMULATES_CFGSEM.