suggestions...

1 files changed, 70 insertions, 20 deletions

diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v
index 4595eb83..8dad43c7 100644
--- a/scheduling/BTLtoRTLproof.v
+++ b/scheduling/BTLtoRTLproof.v
@@ -131,6 +131,10 @@ Proof.
   eapply plus_trans; eauto.
 Qed.
 
+
+Local Hint Constructors RTL.step match_states: core.
+Local Hint Resolve css_refl plus_one: core.
+
 Lemma iblock_istep_simulation sp dupmap stack' f' rs0 m0 ib rs1 m1 ofin
  (IBIS: iblock_istep ge sp rs0 m0 ib rs1 m1 ofin):
  forall pc0 opc isfst
@@ -148,9 +152,9 @@ Proof.
   - assert (X: opc = None). { inv MIB; auto. }
     subst.
     repeat eexists; eauto.
-    eapply css_refl; auto.
-  - inv MIB. exists pc'; split; auto.
-    apply plus_one. apply exec_Inop; trivial.
+    (* eapply css_refl; auto. *)
+  - inv MIB. exists pc'; split; eauto.
+    (* apply plus_one; eauto. apply exec_Inop; trivial. *)
   - inv MIB. exists pc'; split; auto.
     apply plus_one. eapply exec_Iop; eauto.
     erewrite <- eval_operation_preserved; eauto.
@@ -163,8 +167,8 @@ Proof.
     apply plus_one. eapply exec_Istore; eauto.
     erewrite <- eval_addressing_preserved; eauto.
     intros; rewrite symbols_preserved; trivial.
-  - inv MIB.
-    exploit IHIBIS; eauto.
+  - inv MIB; eauto.
+    (* exploit IHIBIS; eauto. *)
   - inv MIB.
     exploit IHIBIS1; eauto.
     intros (pc1 & EQpc1 & STEP1); inv EQpc1.
@@ -177,39 +181,66 @@ Proof.
       eexists; split; auto.
       eapply plus_trans; eauto.
   - inv MIB.
+    assert (JOIN: is_join_opt opc1 opc2 opc). { exact H10. } clear H10. 
     destruct b; exploit IHIBIS; eauto.
     + (* taking ifso *)
       destruct ofin; simpl.
       * (* ofin is Some final *)
         intros (isfst' & pc1 & MI & STAR).
         repeat eexists; eauto.
-        eapply css_plus_trans.
-        eapply plus_one. eapply exec_Icond; eauto.
-        eauto.
+        eapply css_plus_trans; eauto.
+        (* eapply plus_one. eapply exec_Icond; eauto.
+        eauto. *)
       * (* ofin is None *)
         intros (pc1 & OPC & PLUS). inv OPC.
-        inv H10; eexists; split; eauto.
+        inv JOIN; eexists; split; eauto.
         all:
-          eapply plus_trans;
+          eapply plus_trans; eauto.
+        (*
           [ eapply plus_one; eapply exec_Icond; eauto
-          | eauto | eauto ].
+          | eauto | eauto ].*)
     + (* taking ifnot *)
       destruct ofin; simpl.
       * (* ofin is Some final *)
         intros (isfst' & pc1 & MI & STAR).
         repeat eexists; eauto.
-        eapply css_plus_trans.
-        eapply plus_one. eapply exec_Icond; eauto.
-        eauto.
+        eapply css_plus_trans; eauto.
+        (* eapply plus_one. eapply exec_Icond; eauto.
+           eauto. *)
       * (* ofin is None *)
-        intros (pc1 & OPC & PLUS). inv OPC.
-        inv H10; eexists; split; eauto.
+        intros (pc1 & OPC & PLUS). subst.
+        inv JOIN; eexists; split; eauto.
         all:
-          eapply plus_trans;
+          eapply plus_trans; eauto.
+(*
           [ eapply plus_one; eapply exec_Icond; eauto
-          | eauto | eauto ].
+          | eauto | eauto ]. *)
 Qed.
 
+Lemma css_star P s0 s1 t:
+  cond_star_step P s0 t s1 ->
+  star RTL.step tge s0 t s1.
+Proof.
+  destruct 1.
+  - eapply star_refl; eauto.
+  - eapply plus_star; eauto.
+Qed.
+
+Lemma final_simu_except_goto sp dupmap stack stack' f f' rs0 m0 rs1 m1 pc0 fin t s
+  (STACKS : list_forall2 match_stackframes stack stack')
+  (TRANSF : match_function dupmap f f')
+  (FS : final_step ge stack f sp rs1 m1 fin t s)
+  (pc1 : node)
+  (STAR : star RTL.step tge (RTL.State stack' f' sp pc0 rs0 m0) E0
+                            (RTL.State stack' f' sp pc1 rs1 m1))
+  (i : instruction)
+  (ATpc1 : (RTL.fn_code f') ! pc1 = Some i)
+  (MF : match_final_inst dupmap fin i)
+  : exists s', plus RTL.step tge (RTL.State stack' f' sp pc0 rs0 m0) t s' /\ match_states s s'.
+Proof.
+  inv MF; inv FS.
+Admitted.
+
 Lemma iblock_step_simulation sp dupmap stack stack' f f' ib rs0 m0 rs1 m1 pc0 fin t s
  (STACKS: list_forall2 match_stackframes stack stack')
  (TRANSF: match_function dupmap f f')
@@ -219,6 +250,27 @@ Lemma iblock_step_simulation sp dupmap stack stack' f f' ib rs0 m0 rs1 m1 pc0 fi
  :exists s', plus RTL.step tge (RTL.State stack' f' sp pc0 rs0 m0) t s' /\ match_states s s'.
 Proof.
   intros; exploit iblock_istep_simulation; eauto.
+  simpl. intros (isfst' & pc1 & MI & STAR). clear IBIS MIB.
+  inv MI.
+  - (* final inst except goto *)
+    exploit final_simu_except_goto; eauto.
+    eapply css_star; eauto.
+  - (* goto *)
+    inv FS.
+    inv STAR; try congruence.
+    eexists; split. eauto.
+    econstructor; eauto.
+Qed.
+
+Lemma iblock_step_simulation_draft sp dupmap stack stack' f f' ib rs0 m0 rs1 m1 pc0 fin t s
+ (STACKS: list_forall2 match_stackframes stack stack')
+ (TRANSF: match_function dupmap f f')
+ (IBIS: iblock_istep ge sp rs0 m0 ib rs1 m1 (Some fin))
+ (MIB : match_iblock dupmap (RTL.fn_code f') true pc0 ib None)
+ (FS : final_step ge stack f sp rs1 m1 fin t s)
+ :exists s', plus RTL.step tge (RTL.State stack' f' sp pc0 rs0 m0) t s' /\ match_states s s'.
+Proof.
+  intros; exploit iblock_istep_simulation; eauto.
   simpl. intros (isfst' & pc1 & MI & STAR).
   induction FS.
   - inv MI.
@@ -266,8 +318,6 @@ Proof.
       eapply eval_builtin_args_preserved; eauto.
       eapply external_call_symbols_preserved; eauto. eapply senv_preserved.
       eauto. econstructor; eauto.
-(* Icond *)
-  - admit.
   - admit.
 Admitted.