1 files changed, 51 insertions, 22 deletions

diff --git a/scheduling/RTLpathLivegenproof.v b/scheduling/RTLpathLivegenproof.v
index c6125985..26a1a50a 100644
--- a/scheduling/RTLpathLivegenproof.v
+++ b/scheduling/RTLpathLivegenproof.v
@@ -501,12 +501,23 @@ Proof.
   intros H; erewrite (EQLIVE r); eauto.
 Qed.
 
+Lemma final_inst_checker_from_iinst_checker i sp rs m st pm alive:
+  istep ge i sp rs m = Some st -> 
+  final_inst_checker pm alive i = None.
+Proof.
+  destruct i; simpl; try congruence.
+Qed.
+
+(* is it useful ?
 Lemma inst_checker_from_iinst_checker i sp rs m st pm alive:
   istep ge i sp rs m = Some st -> 
   inst_checker pm alive i = (SOME res <- iinst_checker pm alive i IN exit_checker pm (fst res) (snd res) tt).
 Proof.
-  destruct i; simpl; try congruence. 
+  unfold inst_checker.
+  destruct (iinst_checker pm alive i); simpl; auto.
+  destruct i; simpl; try congruence.
 Qed.
+*)
 
 Lemma exit_checker_eqlive_ext1 (pm: path_map) (alive: Regset.t) (pc: node) r rs1 rs2:
   exit_checker pm (Regset.add r alive) pc tt = Some tt ->  
@@ -586,13 +597,13 @@ Proof.
     * intuition. eapply IHtbl; eauto.
 Qed.
 
-Lemma inst_checker_eqlive (f: function) sp alive pc i rs1 rs2 m stk1 stk2 t s1:
+Lemma final_inst_checker_eqlive (f: function) sp alive pc i rs1 rs2 m stk1 stk2 t s1:
   list_forall2 eqlive_stackframes stk1 stk2 ->
   eqlive_reg (ext alive) rs1 rs2 -> 
   liveness_ok_function f ->
   (fn_code f) ! pc = Some i ->
   path_last_step ge pge stk1 f sp pc rs1 m t s1 ->
-  inst_checker (fn_path f) alive i = Some tt -> 
+  final_inst_checker (fn_path f) alive i = Some tt -> 
   exists s2, path_last_step ge pge stk2 f sp pc rs2 m t s2 /\ eqlive_states s1 s2.
 Proof.
   intros STACKS EQLIVE LIVENESS PC; 
@@ -604,25 +615,8 @@ Proof.
                  st1 pc rs1 m optr m']; 
   try_simplify_someHyps.
   + (* istate *)
-    intros PC ISTEP. erewrite inst_checker_from_iinst_checker; eauto.
-    inversion_SOME res.
-    intros.
-    destruct (icontinue st1) eqn: CONT.
-    - (* CONT => true *)
-      exploit iinst_checker_eqlive; eauto.
-      destruct 1 as (st2 & ISTEP2 & [CONT' PC2 RS MEM]).
-      repeat (econstructor; simpl; eauto).
-      rewrite <- MEM, <- PC2.
-      exploit exit_checker_eqlive; eauto.
-      intros (path & PATH & EQLIVE2).
-      eapply eqlive_states_intro; eauto.
-      erewrite <- iinst_checker_istep_continue; eauto.
-    - (* CONT => false *)
-      intros; exploit iinst_checker_eqlive_stopped; eauto.
-      destruct 1 as (path & st2 & PATH & ISTEP2 & [CONT2 PC2 RS MEM]).
-      repeat (econstructor; simpl; eauto).
-      rewrite <- MEM, <- PC2.
-      eapply eqlive_states_intro; eauto.
+    intros PC ISTEP. erewrite final_inst_checker_from_iinst_checker; eauto.
+    congruence.
   + (* Icall *)
     repeat inversion_ASSERT. intros.
     exploit exit_checker_eqlive_ext1; eauto.
@@ -669,6 +663,41 @@ Proof.
       * eapply eqlive_states_return; eauto.
 Qed.
 
+Lemma inst_checker_eqlive (f: function) sp alive pc i rs1 rs2 m stk1 stk2 t s1:
+  list_forall2 eqlive_stackframes stk1 stk2 ->
+  eqlive_reg (ext alive) rs1 rs2 -> 
+  liveness_ok_function f ->
+  (fn_code f) ! pc = Some i ->
+  path_last_step ge pge stk1 f sp pc rs1 m t s1 ->
+  inst_checker (fn_path f) alive i = Some tt -> 
+  exists s2, path_last_step ge pge stk2 f sp pc rs2 m t s2 /\ eqlive_states s1 s2.
+Proof.
+  unfold inst_checker;
+  intros STACKS EQLIVE LIVENESS PC.
+  destruct (iinst_checker (fn_path f) alive i) as [res|] eqn: IICHECKER.
+  + destruct 1 as [i' sp pc rs1 m st1| | | | | ];
+    try_simplify_someHyps.
+    intros PC ISTEP.
+    intros.
+    destruct (icontinue st1) eqn: CONT.
+    - (* CONT => true *)
+      exploit iinst_checker_eqlive; eauto.
+      destruct 1 as (st2 & ISTEP2 & [CONT' PC2 RS MEM]).
+      repeat (econstructor; simpl; eauto).
+      rewrite <- MEM, <- PC2.
+      exploit exit_checker_eqlive; eauto.
+      intros (path & PATH & EQLIVE2).
+      eapply eqlive_states_intro; eauto.
+      erewrite <- iinst_checker_istep_continue; eauto.
+    - (* CONT => false *)
+      intros; exploit iinst_checker_eqlive_stopped; eauto.
+      destruct 1 as (path & st2 & PATH & ISTEP2 & [CONT2 PC2 RS MEM]).
+      repeat (econstructor; simpl; eauto).
+      rewrite <- MEM, <- PC2.
+      eapply eqlive_states_intro; eauto.
+  + intros; exploit final_inst_checker_eqlive; eauto.
+Qed.
+
 Lemma path_step_eqlive path stk1 f sp rs1 m pc t s1 stk2 rs2:
   path_step ge pge (psize path) stk1 f sp rs1 m pc t s1 ->
   list_forall2 eqlive_stackframes stk1 stk2 ->