splitting is_expand property with a weak version for conditions

1 files changed, 58 insertions, 56 deletions

diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v
index f3e258ae..cd6c4dae 100644
--- a/scheduling/RTLtoBTLproof.v
+++ b/scheduling/RTLtoBTLproof.v
@@ -241,25 +241,34 @@ Proof.
   destruct fi; trivial. inv H. inv H5.
 Qed.
 
-Lemma expand_entry_isnt_goto dupmap f pc ib:
-  match_iblock dupmap (RTL.fn_code f) true pc (expand (entry ib) (Bnop None)) None ->
-  is_goto (expand (entry ib) (Bnop None)) = false.
+Lemma normRTL_entry_isnt_goto dupmap f pc ib:
+  match_iblock dupmap (RTL.fn_code f) true pc (normRTL (entry ib) (Bnop None)) None ->
+  is_goto (normRTL (entry ib) (Bnop None)) = false.
 Proof.
-  destruct (is_goto (expand (entry ib) (Bnop None))) eqn:EQG;
-  destruct (expand (entry ib) (Bnop None));
+  destruct (is_goto (normRTL (entry ib) (Bnop None))) eqn:EQG;
+  destruct (normRTL (entry ib) (Bnop None));
   try destruct fi; try discriminate; trivial.
   intros; inv H; inv H5.
 Qed.
 
-Lemma expand_entry_isnt_bnop dupmap f pc ib:
-  match_iblock dupmap (RTL.fn_code f) true pc (expand (entry ib) (Bnop None)) None ->
-  expand (entry ib) (Bnop None) <> Bnop None.
+Lemma normRTL_entry_isnt_bnop dupmap f pc ib:
+  match_iblock dupmap (RTL.fn_code f) true pc (normRTL (entry ib) (Bnop None)) None ->
+  normRTL (entry ib) (Bnop None) <> Bnop None.
 Proof.
-  destruct (expand (entry ib) (Bnop None)) eqn:EQG;
+  destruct (normRTL (entry ib) (Bnop None)) eqn:EQG;
   try destruct fi; try discriminate; trivial.
   intros; inv H; inv H5.
 Qed.
 
+Lemma is_expand_normRTL_entry dupmap f ib pc
+  (MI : match_iblock dupmap (RTL.fn_code f) true pc (normRTL (entry ib) (Bnop None)) None):
+  is_expand (normRTL (entry ib) (Bnop None)).
+Proof.
+  eapply is_wexpand_expand; eauto.
+  apply normRTL_correct; try congruence.
+  eapply normRTL_entry_isnt_bnop; eauto.
+Qed.
+
 Lemma list_nth_z_rev_dupmap:
   forall dupmap ln ln' (pc pc': node) val,
   list_nth_z ln val = Some pc ->
@@ -278,14 +287,14 @@ Proof.
 Qed.
 
 Local Hint Constructors iblock_istep: core.
-Lemma expand_iblock_istep_rec_correct sp ib rs0 m0 rs1 m1 ofin1:
+Lemma normRTL_iblock_istep_rec_correct sp ib rs0 m0 rs1 m1 ofin1:
   forall (ISTEP: iblock_istep tge sp rs0 m0 ib rs1 m1 ofin1)
   k ofin2 rs2 m2
   (CONT: match ofin1 with
          | None => iblock_istep tge sp rs1 m1 k rs2 m2 ofin2
          | Some fin1 => rs2=rs1 /\ m2=m1 /\ ofin2=Some fin1
          end),
-  iblock_istep tge sp rs0 m0 (expand ib k) rs2 m2 ofin2.
+  iblock_istep tge sp rs0 m0 (normRTL ib k) rs2 m2 ofin2.
 Proof.
   induction 1; simpl; intros; intuition subst; eauto.
   { (* Bnop *)
@@ -300,15 +309,15 @@ Proof.
     destruct b; eapply IHISTEP; eauto.
 Qed.
 
-Lemma expand_iblock_istep_correct sp ib rs0 m0 rs1 m1 ofin:
+Lemma normRTL_iblock_istep_correct sp ib rs0 m0 rs1 m1 ofin:
   iblock_istep tge sp rs0 m0 ib rs1 m1 ofin ->
-  iblock_istep tge sp rs0 m0 (expand ib (Bnop None)) rs1 m1 ofin.
+  iblock_istep tge sp rs0 m0 (normRTL ib (Bnop None)) rs1 m1 ofin.
 Proof.
-  intros; eapply expand_iblock_istep_rec_correct; eauto.
+  intros; eapply normRTL_iblock_istep_rec_correct; eauto.
   destruct ofin; simpl; auto.
 Qed.
 
-Lemma expand_iblock_istep_run_None_rec sp ib:
+Lemma normRTL_iblock_istep_run_None_rec sp ib:
   forall rs0 m0 o k
   (ISTEP: iblock_istep_run tge sp ib rs0 m0 = o)
   (CONT: match o with
@@ -317,7 +326,7 @@ Lemma expand_iblock_istep_run_None_rec sp ib:
              iblock_istep_run tge sp k rs1 m1 = None
          | _ => True
      end),
-  iblock_istep_run tge sp (expand ib k) rs0 m0 = None.
+  iblock_istep_run tge sp (normRTL ib k) rs0 m0 = None.
 Proof.
   induction ib; simpl;
   try discriminate.
@@ -359,29 +368,29 @@ Proof.
     + eapply IHib2; eauto.
 Qed.
 
-Lemma expand_preserves_iblock_istep_run_None sp ib:
+Lemma normRTL_preserves_iblock_istep_run_None sp ib:
   forall rs m, iblock_istep_run tge sp ib rs m = None
-  -> iblock_istep_run tge sp (expand ib (Bnop None)) rs m = None.
+  -> iblock_istep_run tge sp (normRTL ib (Bnop None)) rs m = None.
 Proof.
-  intros; eapply expand_iblock_istep_run_None_rec; eauto.
+  intros; eapply normRTL_iblock_istep_run_None_rec; eauto.
   simpl; auto.
 Qed.
 
-Lemma expand_preserves_iblock_istep_run sp ib:
+Lemma normRTL_preserves_iblock_istep_run sp ib:
   forall rs m, iblock_istep_run tge sp ib rs m =
-  iblock_istep_run tge sp (expand ib (Bnop None)) rs m.
+  iblock_istep_run tge sp (normRTL ib (Bnop None)) rs m.
 Proof.
   intros.
   destruct (iblock_istep_run tge sp ib rs m) eqn:ISTEP.
   - destruct o. symmetry.
     rewrite <- iblock_istep_run_equiv in *.
-    apply expand_iblock_istep_correct; auto.
+    apply normRTL_iblock_istep_correct; auto.
   - symmetry.
-    apply expand_preserves_iblock_istep_run_None; auto.
+    apply normRTL_preserves_iblock_istep_run_None; auto.
 Qed.
 
 Local Hint Constructors match_iblock: core.
-Lemma expand_matchiblock_rec_correct dupmap cfg ib pc isfst:
+Lemma normRTL_matchiblock_rec_correct dupmap cfg ib pc isfst:
   forall opc1
   (MIB: match_iblock dupmap cfg isfst pc ib opc1) k opc2
   (CONT: match opc1 with
@@ -389,7 +398,7 @@ Lemma expand_matchiblock_rec_correct dupmap cfg ib pc isfst:
              match_iblock dupmap cfg false pc' k opc2
          | None => opc2=opc1
          end),
-  match_iblock dupmap cfg isfst pc (expand ib k) opc2.
+  match_iblock dupmap cfg isfst pc (normRTL ib k) opc2.
 Proof.
   induction 1; simpl; intros; eauto.
   { (* BF *)
@@ -404,12 +413,12 @@ Proof.
     destruct opc0; econstructor. }
 Qed.
 
-Lemma expand_matchiblock_correct dupmap cfg ib pc isfst opc:
+Lemma normRTL_matchiblock_correct dupmap cfg ib pc isfst opc:
   match_iblock dupmap cfg isfst pc ib opc ->
-  match_iblock dupmap cfg isfst pc (expand ib (Bnop None)) opc.
+  match_iblock dupmap cfg isfst pc (normRTL ib (Bnop None)) opc.
 Proof.
   intros.
-  eapply expand_matchiblock_rec_correct; eauto.
+  eapply normRTL_matchiblock_rec_correct; eauto.
   destruct opc; simpl; auto.
 Qed.
 
@@ -467,11 +476,10 @@ Proof.
     eexists; left; eexists; split.
     + repeat econstructor; eauto.
       apply iblock_istep_run_equiv in BTL_RUN; eauto.
-    + econstructor; apply expand_matchiblock_correct in MI.
-      econstructor; eauto. apply expand_correct; trivial.
-      intros CONTRA; congruence. eapply expand_entry_isnt_bnop; eauto.
-      econstructor. apply expand_preserves_iblock_istep_run.
-      eapply expand_entry_isnt_goto; eauto.
+    + econstructor; apply normRTL_matchiblock_correct in MI.
+      econstructor; eauto. eapply is_expand_normRTL_entry; eauto.
+      econstructor. apply normRTL_preserves_iblock_istep_run.
+      eapply normRTL_entry_isnt_goto; eauto.
   - (* Others *)
     exists (Some ib2); right; split.
     simpl; auto.
@@ -536,11 +544,10 @@ Proof.
         pose symbols_preserved as SYMPRES.
         eapply eval_builtin_args_preserved; eauto.
         eapply external_call_symbols_preserved; eauto. eapply senv_preserved.
-      * econstructor; eauto; apply expand_matchiblock_correct in MI.
-        { econstructor; eauto. apply expand_correct; trivial.
-          intros CONTRA; congruence. eapply expand_entry_isnt_bnop; eauto.
-          apply star_refl. apply expand_preserves_iblock_istep_run. }
-        eapply expand_entry_isnt_goto; eauto.
+      * econstructor; eauto; apply normRTL_matchiblock_correct in MI.
+        { econstructor; eauto. eapply is_expand_normRTL_entry; eauto.
+          apply star_refl. apply normRTL_preserves_iblock_istep_run. }
+        eapply normRTL_entry_isnt_goto; eauto.
     + (* Bjumptable *)
       exploit list_nth_z_rev_dupmap; eauto.
       intros (pc'0 & LNZ & DM).
@@ -552,11 +559,10 @@ Proof.
         eexists; eexists; split.
         eapply iblock_istep_run_equiv in BTL_RUN.
         eapply BTL_RUN. econstructor; eauto.
-      * econstructor; eauto; apply expand_matchiblock_correct in MI.
-        { econstructor; eauto. apply expand_correct; trivial.  
-          intros CONTRA; congruence. eapply expand_entry_isnt_bnop; eauto.
-          apply star_refl. apply expand_preserves_iblock_istep_run. }
-        eapply expand_entry_isnt_goto; eauto.
+      * econstructor; eauto; apply normRTL_matchiblock_correct in MI.
+        { econstructor; eauto. eapply is_expand_normRTL_entry; eauto.
+          apply star_refl. apply normRTL_preserves_iblock_istep_run. }
+        eapply normRTL_entry_isnt_goto; eauto.
   - (* mib_exit *)
     discriminate.
   - (* mib_seq *)
@@ -601,8 +607,7 @@ Proof.
     intros; rewrite H12 in BTL_RUN. destruct b;
     eapply match_strong_state_simu; eauto.
     1,3: inv H2; econstructor; eauto.
-    1,3: inv IS_EXPD; [ inv H3; auto; inv H0 | inv H ].
-    3,5: inv IS_EXPD; [ inv H7; auto; inv H1 | inv H ].
+    1,3,5,7: inv IS_EXPD; auto; try discriminate.
     1-4: eapply star_right; eauto.
     assert (measure bnot > 0) by apply measure_pos; lia.
     assert (measure bso > 0) by apply measure_pos; lia.
@@ -660,14 +665,12 @@ Proof.
       eexists; left; eexists; split.
       * eapply exec_function_internal.
         erewrite preserv_fnstacksize; eauto.
-      * apply expand_matchiblock_correct in MI.
+      * apply normRTL_matchiblock_correct in MI.
         econstructor. econstructor; eauto.
-        apply expand_correct; trivial.
-        intros CONTRA; congruence. eapply expand_entry_isnt_bnop; eauto.
-        3: eapply expand_entry_isnt_goto; eauto.
+        eapply is_expand_normRTL_entry; eauto.
+        3: eapply normRTL_entry_isnt_goto; eauto.
         all: erewrite preserv_fnparams; eauto.
-        constructor.
-        apply expand_preserves_iblock_istep_run.
+        constructor. apply normRTL_preserves_iblock_istep_run.
     + (* External function *)
       inv TRANSF.
       eexists; left; eexists; split.
@@ -682,12 +685,11 @@ Proof.
     apply DMC in DUPLIC as [ib [FNC MI]]; clear DMC.
     eexists; left; eexists; split.
     + eapply exec_return.
-    + apply expand_matchiblock_correct in MI.
+    + apply normRTL_matchiblock_correct in MI.
       econstructor. econstructor; eauto.
-      apply expand_correct; trivial.
-      constructor. congruence. eapply expand_entry_isnt_bnop; eauto.
-      econstructor. apply expand_preserves_iblock_istep_run.
-      eapply expand_entry_isnt_goto; eauto.
+      eapply is_expand_normRTL_entry; eauto.
+      econstructor. apply normRTL_preserves_iblock_istep_run.
+      eapply normRTL_entry_isnt_goto; eauto.
 Qed.
 
 Local Hint Resolve plus_one star_refl: core.