Some advance in Liveness lemmas

1 files changed, 138 insertions, 71 deletions

diff --git a/scheduling/BTL_Livecheck.v b/scheduling/BTL_Livecheck.v
index d5aad8b8..95b6a155 100644
--- a/scheduling/BTL_Livecheck.v
+++ b/scheduling/BTL_Livecheck.v
@@ -2,7 +2,6 @@ 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.
 
@@ -59,32 +58,44 @@ Definition final_inst_checker (btl: code) (alive: Regset.t) (fin: final): option
       ASSERT exit_list_checker btl alive tbl IN Some tt
   end.
 
-Fixpoint body_checker (btl: code) (ib: iblock) (alive: Regset.t): option Regset.t :=
+(* This definition is the meet (infimum) subset of alive registers,
+   used for conditions by the below checker.
+   A None argument represents the neutral element for intersection. *)
+Definition meet (o1 o2: option Regset.t): option Regset.t :=
+  match o1, o2 with
+  | None, _ => o2
+  | _, None => o1
+  | Some alive1, Some alive2 => Some (Regset.inter alive1 alive2)
+  end.
+
+Fixpoint body_checker (btl: code) (ib: iblock) (alive: Regset.t): option (option Regset.t) :=
   match ib with
   | Bseq ib1 ib2 =>
-      SOME alive1 <- body_checker btl ib1 alive IN
+      SOME oalive1 <- body_checker btl ib1 alive IN
+      SOME alive1 <- oalive1 IN
       body_checker btl ib2 alive1
-  | Bnop _ => Some alive
+  | Bnop _ => Some (Some alive)
   | Bop _ args dest _ =>
       ASSERT list_mem args alive IN
-      Some (Regset.add dest alive)
+      Some (Some (Regset.add dest alive))
   | Bload _ _ _ args dest _ =>
       ASSERT list_mem args alive IN
-      Some (Regset.add dest alive)
+      Some (Some (Regset.add dest alive))
   | Bstore _ _ args src _ =>
       ASSERT Regset.mem src alive IN
       ASSERT list_mem args alive IN
-      Some alive
+      Some (Some alive)
   | Bcond _ args ib1 ib2 _ =>
       ASSERT list_mem args alive IN
-      SOME alive1 <- body_checker btl ib1 alive IN
-      SOME alive2 <- body_checker btl ib2 alive IN
-      Some (Regset.union alive1 alive2)
+      SOME oalive1 <- body_checker btl ib1 alive IN
+      SOME oalive2 <- body_checker btl ib2 alive IN
+      Some (meet oalive1 oalive2)
   | BF fin _ =>
       SOME _ <- final_inst_checker btl alive fin IN
-      Some Regset.empty
+      Some None
   end.
 
+(* This definition simply convert the result in an option unit *)
 Definition iblock_checker (btl: code) (ib: iblock) (alive: Regset.t): option unit :=
   SOME _ <- body_checker btl ib alive IN Some tt.
 
@@ -115,7 +126,6 @@ Proof.
   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)).
 
@@ -163,10 +173,25 @@ 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).
 
+Definition ext_opt (oalive: option Regset.t): Regset.elt -> Prop :=
+  match oalive with
+  | Some alive => ext alive
+  | None => fun _ => True
+  end.
+
+Lemma ext_opt_meet: forall r oalive1 oalive2,
+  ext_opt (meet oalive1 oalive2) r ->
+  ext_opt oalive1 r /\ ext_opt oalive2 r.
+Proof.
+  intros. destruct oalive1, oalive2;
+  simpl in *; intuition.
+  eapply Regset.inter_1; eauto.
+  eapply Regset.inter_2; eauto.
+Qed.
+
 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).
@@ -177,6 +202,7 @@ Proof.
 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.
@@ -191,11 +217,6 @@ 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.
@@ -246,8 +267,6 @@ Inductive eqlive_states: state -> state -> Prop :=
       (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.
@@ -257,7 +276,6 @@ 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)
@@ -267,22 +285,39 @@ Proof.
   autodestruct.
    Qed.*)
 
-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 ->*)
-  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 ib rs2 m = Some (out rs2' m' of)
-  /\ eqlive_reg (ext alive2) rs1' rs2'.
+Lemma cfgsem2fsem_finalstep_simu stk1 f sp rs1 m fin t s1 stk2 rs2
+  (FSTEP: final_step tid ge stk1 f sp rs1 m fin t s1)
+  (LIVE: liveness_ok_function f)
+  (STACKS: list_forall2 eqlive_stackframes stk1 stk2)
+  (*body_checker (fn_code f) (entry ibf) (input_regs ibf) = Some x ->*)
+  (*eqlive_reg (ext x) rs1' rs2' ->*)
+  :exists s2,
+    final_step tr_inputs ge stk2 f sp rs2 m fin t s2
+    /\ eqlive_states s1 s2.
 Proof.
-  induction 1; simpl; try_simplify_someHyps;
-  repeat inversion_ASSERT; intros.
-  - (* BF *)
-    generalize H0; clear H0; inversion_SOME x; try_simplify_someHyps.
+  destruct FSTEP.
+  - (* Bgoto *)
+    econstructor. econstructor.
+    econstructor. econstructor.
+    eauto. eauto.
+    repeat econstructor; eauto.
+Admitted.
+
+Lemma cfgsem2fsem_ibistep_simu_None sp f ib: forall rs1 m rs1' m'
+  (ISTEP: iblock_istep ge sp rs1 m ib rs1' m' None)
+  alive1 oalive2 rs2 (REGS: eqlive_reg (ext alive1) rs1 rs2)
+  (BDY: body_checker (fn_code f) ib alive1 = Some (oalive2)),
+  exists rs2',
+    iblock_istep_run ge sp ib rs2 m = Some (out rs2' m' None)
+    /\ eqlive_reg (ext_opt oalive2) rs1' rs2'.
+Proof.
+  induction ib; intros; try_simplify_someHyps;
+  repeat inversion_ASSERT; intros; inv ISTEP.
+  - (* Bnop *)
+    inv BDY; eauto.
   - (* Bop *)
     erewrite <- eqlive_reg_listmem; eauto.
-    try_simplify_someHyps.
+    try_simplify_someHyps; intros.
     repeat econstructor.
     apply eqlive_reg_update.
     eapply eqlive_reg_monotonic; eauto.
@@ -299,36 +334,65 @@ Proof.
     intuition.
   - (* Bstore *)
     erewrite <- eqlive_reg_listmem; eauto.
-    rewrite <- (H src); auto.
+    rewrite <- (REGS src); auto.
     try_simplify_someHyps; intros.
     rewrite STORE; eauto.
-  - (* Bseq stop *)
-    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.
+    destruct (body_checker _ _ _) eqn:BDY1 in BDY; try discriminate.
+    generalize BDY; clear BDY.
+    inversion_SOME aliveMid; intros OALIVE BDY2. inv OALIVE.
+    exploit IHib1; eauto.
     intros (rs2' & ISTEP1 & REGS1). rewrite ISTEP1; simpl.
-    eapply IHiblock_istep2; eauto.
+    eapply IHib2; eauto.
   - (* Bcond *)
-    generalize H2; clear H2.
-    inversion_SOME aliveSo; inversion_SOME aliveNot; intros BDY1 BDY2 UNION.
-    inv UNION. erewrite <- eqlive_reg_listmem; eauto.
-    admit.
-Admitted.
+    generalize BDY; clear BDY.
+    inversion_SOME oaliveSo; inversion_SOME oaliveNot; intros BDY1 BDY2 JOIN.
+    erewrite <- eqlive_reg_listmem; eauto.
+    rewrite EVAL.
+    destruct b; [ exploit IHib1; eauto | exploit IHib2; eauto].
+    all:
+      intros (rs2' & ISTEP1 & REGS1);
+      econstructor; split; eauto; inv JOIN;
+      eapply eqlive_reg_monotonic; eauto;
+      intros r EXTM; apply ext_opt_meet in EXTM; intuition.
+Qed.
 
-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.
+Lemma cfgsem2fsem_ibistep_simu_Some sp f stk1 stk2 ib: forall s t rs1 m rs1' m' fin
+  (ISTEP: iblock_istep ge sp rs1 m ib rs1' m' (Some fin))
+  (FSTEP: final_step tid ge stk1 f sp rs1' m' fin t s)
+  alive1 oalive2 rs2 (REGS: eqlive_reg (ext alive1) rs1 rs2)
+  (BDY: body_checker (fn_code f) ib alive1 = Some (oalive2))
+  (LIVE: liveness_ok_function f)
+  (STACKS: list_forall2 eqlive_stackframes stk1 stk2),
+  exists rs2' s',
+    iblock_istep_run ge sp ib rs2 m = Some (out rs2' m' (Some fin))
+    /\ final_step tr_inputs ge stk2 f sp rs2' m' fin t s'
+    /\ eqlive_states s s'.
 Proof.
-Admitted.
+  induction ib; simpl; try_simplify_someHyps;
+  repeat inversion_ASSERT; intros; inv ISTEP.
+  - (* BF *)
+    exploit cfgsem2fsem_finalstep_simu; eauto.
+    intros (s2 & FSTEP' & STATES). eauto.
+  - (* Bseq stop *)
+    destruct (body_checker _ _ _) eqn:BDY1 in BDY; try discriminate.
+    generalize BDY; clear BDY.
+    inversion_SOME aliveMid. intros OALIVE BDY2. inv OALIVE.
+    exploit IHib1; eauto. intros (rs2' & s' & ISTEP1 & FSTEP1 & STATES).
+    rewrite ISTEP1; simpl.
+    do 2 eexists; intuition eauto.
+  - (* Bseq continue *)
+    destruct (body_checker _ _ _) eqn:BDY1 in BDY; try discriminate.
+    generalize BDY; clear BDY.
+    inversion_SOME aliveMid; intros OALIVE BDY2. inv OALIVE.
+    exploit cfgsem2fsem_ibistep_simu_None; eauto.
+    intros (rs2' & ISTEP1 & REGS'). rewrite ISTEP1; simpl; eauto.
+  - (* Bcond *)
+    generalize BDY; clear BDY.
+    inversion_SOME oaliveSo; inversion_SOME oaliveNot; intros BDY1 BDY2 JOIN.
+    erewrite <- eqlive_reg_listmem; eauto. rewrite EVAL.
+    destruct b; eauto.
+Qed.
 
 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 ->
@@ -341,18 +405,17 @@ Lemma cfgsem2fsem_ibstep_simu stk1 stk2 f sp rs1 m rs2 ibf pc s1 t:
     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]].
+  assert (CHECKER: liveness_ok_function f) by auto.
+  unfold liveness_ok_function in CHECKER.
+  apply decomp_liveness_checker in CHECKER; destruct CHECKER 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 x; intros BODY _.
-  destruct STEP as (rs1' & m1' & fin' & ISTEP1 & FSTEP).
-  exploit cfgsem2fsem_ibistep_simu; eauto.
-  intros (rs2' & ISTEP2 & REGS).
-  rewrite <- iblock_istep_run_equiv in ISTEP2. clear ISTEP1.
-  exploit cfgsem2fsem_finalstep_simu; eauto.
-  intros (s2 & FSTEP2 & STATES). clear FSTEP.
+  inversion_SOME alive; intros BODY _.
+  destruct STEP as (rs1' & m1' & fin' & ISTEP & FSTEP).
+  exploit cfgsem2fsem_ibistep_simu_Some; eauto.
+  intros (rs2' & s' & ISTEP' & FSTEP' & REGS).
+  rewrite <- iblock_istep_run_equiv in ISTEP'. clear ISTEP.
   unfold iblock_step. repeat eexists; eauto.
 Qed.
 
@@ -365,18 +428,22 @@ Lemma cfgsem2fsem_step_simu s1 s1' t s2:
     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.
+  destruct 1 as [stack ibf f sp n rs m t s ENTRY STEP | | | ]; intros STATES.
+  - (* iblock *)
+    inv STATES; simplify_someHyps.
     intros.
     exploit cfgsem2fsem_ibstep_simu; eauto.
     intros (s2 & STEP2 & EQUIV2). 
     eexists; split; eauto.
-  - inv STATES; inv LIVE.
+  - (* function internal *)
+    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.
+  - (* function external *)
+    inv STATES; inv LIVE; eexists; split; econstructor; eauto.
+  - (* return *)
+    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.