End of liveness proof

1 files changed, 45 insertions, 54 deletions

diff --git a/scheduling/BTL_Livecheck.v b/scheduling/BTL_Livecheck.v
index a92f24c3..25a1c545 100644
--- a/scheduling/BTL_Livecheck.v
+++ b/scheduling/BTL_Livecheck.v
@@ -277,21 +277,6 @@ Hypothesis all_fundef_liveness_ok: forall b f, Genv.find_funct_ptr ge b = Some f
 
 Local Hint Constructors eqlive_stackframes eqlive_states final_step list_forall2 step: core.
 
-Lemma tr_inputs_eqlive_None f pc tbl ibf rs1 rs2:
-  (fn_code f) ! pc = Some ibf ->
-  eqlive_reg (ext (input_regs ibf)) rs1 rs2 ->
-  eqlive_reg (ext (input_regs ibf)) (tid f (pc :: tbl) None rs1)
-    (tr_inputs f (pc :: tbl) None rs2).
-Proof.
-  intros PC REGS.
-  unfold eqlive_reg. intros r INR.
-  unfold tid. rewrite tr_inputs_get.
-  simpl. rewrite PC.
-  exploit Regset.union_3. eapply INR.
-  intros INRU. eapply Regset.mem_1 in INRU.
-  erewrite INRU; eauto.
-Qed.
-
 Lemma eqlive_reg_update_gso alive rs1 rs2 res r: forall v : val,
   eqlive_reg (ext alive) rs1 # res <- v rs2 # res <- v ->
   res <> r -> Regset.In r alive ->
@@ -302,24 +287,6 @@ Proof.
   rewrite !Regmap.gso in INR; auto.
 Qed.
 
-Lemma tr_inputs_eqlive_update f pc ibf rs1 rs2 res:
-  (fn_code f) ! pc = Some ibf ->
-  forall v : val,
-    eqlive_reg (ext (input_regs ibf)) rs1 # res <- v rs2 # res <- v ->
-  eqlive_reg (ext (input_regs ibf))
-    (tid f (pc :: nil) (Some res) rs1) # res <- v
-    (tr_inputs f (pc :: nil) (Some res) rs2) # res <- v.
-Proof.
-  intros PC v REGS. apply eqlive_reg_update.
-  unfold eqlive_reg. intros r (NRES & INR).
-  unfold tid. rewrite tr_inputs_get.
-  simpl. rewrite PC. assert (NRES': res <> r) by auto.
-  clear NRES. exploit Regset.union_3. eapply INR.
-  intros INRU. exploit Regset.remove_2; eauto.
-  intros INRU_RES. eapply Regset.mem_1 in INRU_RES.
-  erewrite INRU_RES. eapply eqlive_reg_update_gso; eauto.
-Qed.
-
 Lemma find_funct_liveness_ok v fd:
   Genv.find_funct ge v = Some fd -> liveness_ok_fundef fd.
 Proof.
@@ -439,34 +406,63 @@ Proof.
       simpl; intros; eauto with local.
 Qed.
 
-Lemma tr_inputs_eqlive_list_None tbl: forall f pc n alive ibf rs1 rs2,
-  (*rs1 # arg = Vint n ->*)
-  eqlive_reg (ext alive) rs1 rs2 ->
-  exit_list_checker (fn_code f) alive tbl = true ->
-(*H1 : Regset.mem arg alive = true*)
-  list_nth_z tbl n = Some pc ->
-  (fn_code f) ! pc = Some ibf ->
-  eqlive_reg (ext (input_regs ibf)) rs1 rs2 ->
+Lemma tr_inputs_eqlive_None f pc tbl ibf rs1 rs2
+  (PC: (fn_code f) ! pc = Some ibf)
+  (REGS: eqlive_reg (ext (input_regs ibf)) rs1 rs2)
+  :eqlive_reg (ext (input_regs ibf)) (tid f (pc :: tbl) None rs1)
+    (tr_inputs f (pc :: tbl) None rs2).
+Proof.
+  unfold eqlive_reg. intros r INR.
+  unfold tid. rewrite tr_inputs_get.
+  simpl. rewrite PC.
+  exploit Regset.union_3. eapply INR.
+  intros INRU. eapply Regset.mem_1 in INRU.
+  erewrite INRU; eauto.
+Qed.
+
+Lemma tr_inputs_eqlive_list_None tbl: forall f pc n alive ibf rs1 rs2
+  (REGS1: eqlive_reg (ext alive) rs1 rs2)
+  (EXIT_LIST: exit_list_checker (fn_code f) alive tbl = true)
+  (LIST: list_nth_z tbl n = Some pc)
+  (PC: (fn_code f) ! pc = Some ibf)
+  (REGS2: eqlive_reg (ext (input_regs ibf)) rs1 rs2),
   eqlive_reg (ext (input_regs ibf)) (tid f tbl None rs1)
     (tr_inputs f tbl None rs2).
 Proof.
   induction tbl as [| pc' tbl IHtbl]; try_simplify_someHyps.
   autodestruct; try_simplify_someHyps.
   - intros; eapply tr_inputs_eqlive_None; eauto.
-  - rewrite lazy_and_Some_tt_true in H0.
-    destruct H0 as [EXIT EXIT_REM].
-    intros LIST PC. unfold eqlive_reg.
-    intros r INR.
+  - rewrite lazy_and_Some_tt_true in EXIT_LIST.
+    destruct EXIT_LIST as [EXIT EXIT_REM].
+    intros. unfold eqlive_reg. intros r INR.
     exploit (IHtbl f pc (Z.pred n) alive ibf rs1 rs2); eauto.
     unfold tid. rewrite !tr_inputs_get.
     exploit exit_checker_eqlive; eauto.
-    intros (ibf' & PC' & REGS).
+    intros (ibf' & PC' & REGS3).
     simpl; rewrite PC'. autodestruct.
     + intro INRU. apply Regset.mem_2 in INRU.
       intros EQR. eapply Regset.union_2 in INRU.
       eapply Regset.mem_1 in INRU. erewrite INRU; auto.
     + intros. autodestruct.
-      rewrite (H3 r); auto.
+      rewrite (REGS2 r); auto.
+Qed.
+
+Lemma tr_inputs_eqlive_update f pc ibf rs1 rs2 res
+  (PC: (fn_code f) ! pc = Some ibf)
+  :forall (v: val)
+    (REGS: eqlive_reg (ext (input_regs ibf)) rs1 # res <- v rs2 # res <- v),
+  eqlive_reg (ext (input_regs ibf))
+    (tid f (pc :: nil) (Some res) rs1) # res <- v
+    (tr_inputs f (pc :: nil) (Some res) rs2) # res <- v.
+Proof.
+  intros. apply eqlive_reg_update.
+  unfold eqlive_reg. intros r (NRES & INR).
+  unfold tid. rewrite tr_inputs_get.
+  simpl. rewrite PC. assert (NRES': res <> r) by auto.
+  clear NRES. exploit Regset.union_3. eapply INR.
+  intros INRU. exploit Regset.remove_2; eauto.
+  intros INRU_RES. eapply Regset.mem_1 in INRU_RES.
+  erewrite INRU_RES. eapply eqlive_reg_update_gso; eauto.
 Qed.
 
 Local Hint Resolve tr_inputs_eqlive_None tr_inputs_eqlive_update: core.
@@ -523,13 +519,8 @@ Proof.
     + econstructor; eauto.
       erewrite <- REGS; eauto.
     + repeat (econstructor; simpl; eauto).
-
-      eapply tr_inputs_eqlive_list_None.
-      eapply REGS.
-      eauto.
-      eauto.
-      eauto.
-      eauto.
+      apply (tr_inputs_eqlive_list_None tbl f pc' (Int.unsigned n) alive ibf rs1 rs2);
+      auto.
 Qed.
 
 Lemma cfgsem2fsem_ibistep_simu_None sp f ib: forall rs1 m rs1' m'