update a more general version of the liveness checker

1 files changed, 118 insertions, 93 deletions

diff --git a/scheduling/BTL_Livecheck.v b/scheduling/BTL_Livecheck.v
index 82efff44..d5aad8b8 100644
--- a/scheduling/BTL_Livecheck.v
+++ b/scheduling/BTL_Livecheck.v
@@ -59,40 +59,34 @@ Definition final_inst_checker (btl: code) (alive: Regset.t) (fin: final): option
       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) :=
+Fixpoint body_checker (btl: code) (ib: iblock) (alive: Regset.t): option Regset.t :=
   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)
+      SOME alive1 <- body_checker btl ib1 alive IN
+      body_checker btl ib2 alive1
+  | Bnop _ => Some alive
   | Bop _ args dest _ =>
       ASSERT list_mem args alive IN
-      Some (Regset.add dest alive, None)
+      Some (Regset.add dest alive)
   | Bload _ _ _ args dest _ =>
       ASSERT list_mem args alive IN
-      Some (Regset.add dest alive, None)
+      Some (Regset.add dest alive)
   | 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) _ =>
+      Some alive
+  | Bcond _ args ib1 ib2 _ =>
       ASSERT list_mem args alive IN
-      exit_checker btl alive s (alive, None)
-  | BF fin _ => Some (alive, Some fin)
-  | _ => None
+      SOME alive1 <- body_checker btl ib1 alive IN
+      SOME alive2 <- body_checker btl ib2 alive IN
+      Some (Regset.union alive1 alive2)
+  | BF fin _ =>
+      SOME _ <- final_inst_checker btl alive fin IN
+      Some Regset.empty
   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.
+Definition iblock_checker (btl: code) (ib: iblock) (alive: Regset.t): option unit :=
+  SOME _ <- body_checker btl ib alive IN Some tt.
 
 Fixpoint list_iblock_checker (btl: code) (l: list (node*iblock_info)): bool :=
   match l with
@@ -113,8 +107,9 @@ Proof.
    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.
+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).
@@ -181,9 +176,53 @@ Proof.
     * eapply Regset.add_2; auto.
 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.
+
 Definition eqlive_reg (alive: Regset.elt -> Prop) (rs1 rs2: regset): Prop :=
  forall r, (alive r) -> rs1#r = rs2#r.
 
+Lemma eqlive_reg_empty rs1 rs2: eqlive_reg (ext Regset.empty) rs1 rs2.
+Proof.
+  unfold eqlive_reg; intros. inv H.
+Qed.
+
+Lemma eqlive_reg_update (alive: Regset.elt -> Prop) rs1 rs2 r v: eqlive_reg (fun r1 => r1 <> r /\ alive r1) rs1 rs2 -> eqlive_reg alive (rs1 # r <- v) (rs2 # r <- v).
+Proof.
+  unfold eqlive_reg; intros EQLIVE r0 ALIVE.
+  destruct (Pos.eq_dec r r0) as [H|H].
+  - subst. rewrite! Regmap.gss. auto.
+  - rewrite! Regmap.gso; auto.
+Qed.
+
+Lemma eqlive_reg_monotonic (alive1 alive2: Regset.elt -> Prop) rs1 rs2: eqlive_reg alive2 rs1 rs2 -> (forall r, alive1 r -> alive2 r) ->  eqlive_reg alive1 rs1 rs2.
+Proof.
+  unfold eqlive_reg; intuition.
+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.
+
 Inductive eqlive_stackframes: stackframe -> stackframe -> Prop :=
   | eqlive_stackframes_intro ibf res f sp pc rs1 rs2
       (LIVE: liveness_ok_function f)
@@ -218,6 +257,7 @@ 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.
+Local Hint Resolve eqlive_reg_empty: core.
 
 (*Lemma tr_inputs_eqlive f rs1 rs2 tbl or r
   (REGS: forall r, eqlive_reg (ext (input_regs ibf)) rs1 rs2)
@@ -227,82 +267,67 @@ Proof.
   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 ->
+Lemma cfgsem2fsem_ibistep_simu sp f: forall rs1 m rs1' m' of ib,
+  iblock_istep ge sp rs1 m ib 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 ->
+  forall alive1 alive2 rs2, eqlive_reg (ext alive1) rs1 rs2 ->
+  body_checker (fn_code f) ib alive1 = Some alive2 ->
 (*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).
+  exists rs2', iblock_istep_run ge sp ib rs2 m = Some (out rs2' m' of)
+  /\ eqlive_reg (ext alive2) rs1' rs2'.
 Proof.
-  induction 1; simpl; repeat inversion_ASSERT; intros; try_simplify_someHyps.
+  induction 1; simpl; try_simplify_someHyps;
+  repeat inversion_ASSERT; intros.
+  - (* BF *)
+    generalize H0; clear H0; inversion_SOME x; try_simplify_someHyps.
   - (* Bop *)
-    intros.
     erewrite <- eqlive_reg_listmem; eauto.
     try_simplify_someHyps.
-    (*
-  (*- [> BF <]*)
-    (*intros. inv H1; eexists; reflexivity.*)
+    repeat econstructor.
+    apply eqlive_reg_update.
+    eapply eqlive_reg_monotonic; eauto.
+    intros r0; rewrite regset_add_spec. 
+    intuition.
+  - (* Bload *)
+    erewrite <- eqlive_reg_listmem; eauto.
+    try_simplify_someHyps; intros.
+    rewrite LOAD; eauto.
+    repeat econstructor.
+    apply eqlive_reg_update.
+    eapply eqlive_reg_monotonic; eauto.
+    intros r0; rewrite regset_add_spec. 
+    intuition.
+  - (* Bstore *)
+    erewrite <- eqlive_reg_listmem; eauto.
+    rewrite <- (H src); auto.
+    try_simplify_someHyps; intros.
+    rewrite STORE; eauto.
   - (* 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. *)
+    generalize H1; clear H1.
+    inversion_SOME aliveMid. intros BDY1 BDY2.
+    (*rewrite iblock_istep_run_equiv in H.*)
+      exploit IHiblock_istep; eauto.
+      intros (rs2' & ISTEP1 & REGS). rewrite ISTEP1; simpl.
+              repeat econstructor. admit.
+  - (* Bseq continue *)
+    generalize H2; clear H2.
+    inversion_SOME aliveMid; intros BDY1 BDY2.
+    exploit IHiblock_istep1; eauto.
+    intros (rs2' & ISTEP1 & REGS1). rewrite ISTEP1; simpl.
+    eapply IHiblock_istep2; eauto.
   - (* Bcond *)
-       admit.*)
+    generalize H2; clear H2.
+    inversion_SOME aliveSo; inversion_SOME aliveNot; intros BDY1 BDY2 UNION.
+    inv UNION. erewrite <- eqlive_reg_listmem; eauto.
+    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.
+Lemma cfgsem2fsem_finalstep_simu stk1 f sp rs1 m1 fin t s1 stk2 rs2 m2:
+  final_step tid ge stk1 f sp rs1 m1 fin t s1 ->
+  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:
@@ -321,11 +346,11 @@ Proof.
   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).
+  inversion_SOME x; intros BODY _.
+  destruct STEP as (rs1' & m1' & fin' & ISTEP1 & FSTEP).
   exploit cfgsem2fsem_ibistep_simu; eauto.
-  intros (rs2' & ISTEP2).
-  rewrite <- iblock_istep_run_equiv in ISTEP2. clear ISTEP.
+  intros (rs2' & ISTEP2 & REGS).
+  rewrite <- iblock_istep_run_equiv in ISTEP2. clear ISTEP1.
   exploit cfgsem2fsem_finalstep_simu; eauto.
   intros (s2 & FSTEP2 & STATES). clear FSTEP.
   unfold iblock_step. repeat eexists; eauto.