Now supporting Bnop insertion in conditions

1 files changed, 59 insertions, 92 deletions

diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v
index 7ad1472b..f3e258ae 100644
--- a/scheduling/RTLtoBTLproof.v
+++ b/scheduling/RTLtoBTLproof.v
@@ -242,11 +242,20 @@ Proof.
 Qed.
 
 Lemma expand_entry_isnt_goto dupmap f pc ib:
-  match_iblock dupmap (RTL.fn_code f) true pc (expand (entry ib) None) None ->
-  is_goto (expand (entry ib) None) = false.
+  match_iblock dupmap (RTL.fn_code f) true pc (expand (entry ib) (Bnop None)) None ->
+  is_goto (expand (entry ib) (Bnop None)) = false.
 Proof.
-  destruct (is_goto (expand (entry ib) None))eqn:EQG;
-  destruct (expand (entry ib) None);
+  destruct (is_goto (expand (entry ib) (Bnop None))) eqn:EQG;
+  destruct (expand (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.
+Proof.
+  destruct (expand (entry ib) (Bnop None)) eqn:EQG;
   try destruct fi; try discriminate; trivial.
   intros; inv H; inv H5.
 Qed.
@@ -268,38 +277,23 @@ Proof.
       intros (pc'1 & LNZ & REV). exists pc'1. split; auto. congruence.
 Qed.
 
+Local Hint Constructors iblock_istep: core.
 Lemma expand_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 =>
-             (k = None /\ rs2=rs1 /\ m2=m1 /\ ofin2 = None)
-             \/ (exists rem, k = Some rem
-                /\ iblock_istep tge sp rs1 m1 rem rs2 m2 ofin2)
+         | 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.
 Proof.
-  induction 1; simpl.
-  { (* BF *)
-    intros ? ? ? ? (HRS & HM & HOF); subst.
-    constructor. }
-    (*destruct k; intros. try inv CONT.*)
-  1-4: (* Bnop, Bop, Bload, Bstore *)
-    destruct k; intros; destruct CONT as [[HK [HRS [HM HO]]]|[rem [HR ISTEP]]];
-    subst; try (inv HK; fail); try (inv HR; fail); try (econstructor; eauto; fail);
-    inversion HR; subst; clear HR;
-    eapply exec_seq_continue; [ econstructor; eauto | assumption].
-  - (* Bseq_stop *)
-    destruct k; intros; apply IHISTEP; eauto.
-  - (* Bseq_continue *)
-    destruct ofin; intros.
-    + destruct CONT as [HRS [HM HOF]]; subst.
-      eapply IHISTEP1; right. eexists; repeat split; eauto.
-    + destruct CONT as [[HK [HRS [HM HO]]]|[rem [HR ISTEP]]]; subst.
-      * eapply IHISTEP1; right. eexists; repeat split; eauto.
-        eapply IHISTEP2; left; simpl; auto.
-      * eapply IHISTEP1; right. eexists; repeat split; eauto.
+  induction 1; simpl; intros; intuition subst; eauto.
+  { (* Bnop *)
+    autodestruct; intros OI; inv OI; destruct (Bnop_dec k); subst;
+    try (inv CONT; constructor; fail); repeat econstructor; eauto. }
+  1-3: (* Bop, Bload, Bstore *)
+    intros; destruct (Bnop_dec k); subst; repeat econstructor; eauto;
+    inv CONT; econstructor; eauto.
   - (* Bcond *)
     destruct ofin; intros;
     econstructor; eauto;
@@ -308,47 +302,19 @@ Qed.
 
 Lemma expand_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 None) rs1 m1 ofin.
+  iblock_istep tge sp rs0 m0 (expand ib (Bnop None)) rs1 m1 ofin.
 Proof.
   intros; eapply expand_iblock_istep_rec_correct; eauto.
   destruct ofin; simpl; auto.
 Qed.
 
-(* TODO gourdinl useless? *)
-Lemma expand_iblock_istep_run_Some_rec sp ib rs0 m0 rs1 m1 ofin1:
-  forall (ISTEP: iblock_istep_run tge sp ib rs0 m0 =
-  Some {| _rs := rs1; _m := m1; _fin := ofin1 |})
-  k ofin2 rs2 m2
-  (CONT: match ofin1 with
-         | None =>
-             (k = None /\ rs2=rs1 /\ m2=m1 /\ ofin2 = None)
-             \/ (exists rem, k = Some rem
-                /\ iblock_istep_run tge sp rem rs1 m1 =
-                Some {| _rs := rs2; _m := m2; _fin := ofin2 |})
-         | Some fin1 => rs2=rs1 /\ m2=m1 /\ ofin2=Some fin1
-         end),
-  iblock_istep_run tge sp (expand ib k) rs0 m0 =
-  Some {| _rs := rs2; _m := m2; _fin := ofin2 |}.
-Proof.
-  intros. destruct ofin1;
-  rewrite <- iblock_istep_run_equiv in *.
-  - destruct CONT as [HRS [HM HO]]; subst.
-    eapply expand_iblock_istep_rec_correct; eauto.
-    simpl; auto.
-  - eapply expand_iblock_istep_rec_correct; eauto.
-    simpl. destruct CONT as [HL | [rem [HR ISTEP']]].
-    left; auto. rewrite <- iblock_istep_run_equiv in ISTEP'.
-    right; eexists; split; eauto.
-Qed.
-
 Lemma expand_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
          | Some (out rs1 m1 ofin) =>
-             exists rem,
-             k = Some rem /\ ofin = None /\
-             iblock_istep_run tge sp rem rs1 m1 = None
+             ofin = None /\
+             iblock_istep_run tge sp k rs1 m1 = None
          | _ => True
      end),
   iblock_istep_run tge sp (expand ib k) rs0 m0 = None.
@@ -357,35 +323,34 @@ Proof.
   try discriminate.
   - (* BF *)
     intros; destruct o; try discriminate; simpl in *.
-    inv ISTEP. destruct CONT as [rem [HR [HO ISTEP]]]; inv HR; inv HO.
+    inv ISTEP. destruct CONT as [HO ISTEP]; inv HO.
   - (* Bnop *)
-    intros; destruct o; inv ISTEP; destruct k;
-    destruct CONT as [rem [HR [HO ISTEP]]]; inv HR; inv HO; trivial.
+    intros; destruct o; inv ISTEP; destruct oiinfo, CONT; auto.
+    destruct (Bnop_dec k); subst; repeat econstructor; eauto.
   - (* Bop *)
-    intros; destruct o;
-    destruct (eval_operation _ _ _ _ _) eqn:EVAL; inv ISTEP; destruct k;
-    simpl; rewrite EVAL; auto; destruct CONT as [rem [HR [HO ISTEP]]];
-    inv HR; inv HO; trivial.
+    intros; destruct o; destruct (Bnop_dec k);
+    destruct (eval_operation _ _ _ _ _) eqn:EVAL; inv ISTEP;
+    simpl; rewrite EVAL; auto; destruct CONT as [HO ISTEP];
+    trivial.
   - (* Bload *)
-    intros; destruct o;
+    intros; destruct o; destruct (Bnop_dec k);
     destruct (trap) eqn:TRAP;
     try destruct (eval_addressing _ _ _ _) eqn:EVAL;
-    try destruct (Mem.loadv _ _ _) eqn:MEM; inv ISTEP; destruct k;
+    try destruct (Mem.loadv _ _ _) eqn:MEM; inv ISTEP;
     simpl; try rewrite EVAL; try rewrite MEM; simpl; auto;
-    destruct CONT as [rem [HR [HO ISTEP]]]; inv HR; inv HO; trivial.
+    destruct CONT as [HO ISTEP]; trivial.
   - (* Bstore *)
-    intros; destruct o;
+    intros; destruct o; destruct (Bnop_dec k);
     destruct (eval_addressing _ _ _ _) eqn:EVAL;
-    try destruct (Mem.storev _ _ _) eqn:MEM; inv ISTEP; destruct k;
+    try destruct (Mem.storev _ _ _) eqn:MEM; inv ISTEP;
     simpl; try rewrite EVAL; try rewrite MEM; simpl; auto;
-    destruct CONT as [rem [HR [HO ISTEP]]]; inv HR; inv HO; trivial.
+    destruct CONT as [HO ISTEP]; inv HO; trivial.
   - (* Bseq *)
     intros.
     eapply IHib1; eauto.
     destruct (iblock_istep_run tge sp ib1 rs0 m0) eqn:EQib1; try auto.
-    destruct o0. eexists; split; eauto. simpl in *.
-    destruct _fin; inv ISTEP.
-    + destruct CONT as [rem [_ [CONTRA _]]]; inv CONTRA.
+    destruct o0; simpl in *. destruct _fin; inv ISTEP.
+    + destruct CONT as [CONTRA _]; inv CONTRA.
     + split; auto. eapply IHib2; eauto.
   - (* Bcond *)
     intros; destruct (eval_condition _ _ _); trivial.
@@ -396,7 +361,7 @@ Qed.
 
 Lemma expand_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 None) rs m = None.
+  -> iblock_istep_run tge sp (expand ib (Bnop None)) rs m = None.
 Proof.
   intros; eapply expand_iblock_istep_run_None_rec; eauto.
   simpl; auto.
@@ -404,7 +369,7 @@ Qed.
 
 Lemma expand_preserves_iblock_istep_run sp ib:
   forall rs m, iblock_istep_run tge sp ib rs m =
-  iblock_istep_run tge sp (expand ib None) rs m.
+  iblock_istep_run tge sp (expand ib (Bnop None)) rs m.
 Proof.
   intros.
   destruct (iblock_istep_run tge sp ib rs m) eqn:ISTEP.
@@ -415,28 +380,24 @@ Proof.
     apply expand_preserves_iblock_istep_run_None; auto.
 Qed.
 
+Local Hint Constructors match_iblock: core.
 Lemma expand_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
          | Some pc' =>
-             k = None /\ opc2 = opc1 \/
-             (exists rem, k = Some rem
-             /\ match_iblock dupmap cfg false pc' rem opc2)
+             match_iblock dupmap cfg false pc' k opc2
          | None => opc2=opc1
          end),
   match_iblock dupmap cfg isfst pc (expand ib k) opc2.
 Proof.
-  induction 1; simpl.
+  induction 1; simpl; intros; eauto.
   { (* BF *)
-    intros; inv CONT; econstructor; eauto. }
-  1-4: (* Bnop *)
-    destruct k; intros; destruct CONT as [[HK HO] | [rem [HR MIB]]];
-    try inv HK; try inv HO; try inv HR; repeat econstructor; eauto.
+    inv CONT; econstructor; eauto. }
+  1-4: (* Bnop, Bop, Bload, Bstore *)
+    destruct (Bnop_dec k); subst; eauto; inv CONT; econstructor; eauto.
   { (* Bgoto *)
     intros; inv CONT; apply mib_exit; auto. }
-  { (* Bseq *)
-    intros. eapply IHMIB1. right. eexists; split; eauto. }
   { (* Bcond *)
     intros. inv H0;
     econstructor; eauto; try econstructor.
@@ -445,7 +406,7 @@ Qed.
 
 Lemma expand_matchiblock_correct dupmap cfg ib pc isfst opc:
   match_iblock dupmap cfg isfst pc ib opc ->
-  match_iblock dupmap cfg isfst pc (expand ib None) opc.
+  match_iblock dupmap cfg isfst pc (expand ib (Bnop None)) opc.
 Proof.
   intros.
   eapply expand_matchiblock_rec_correct; eauto.
@@ -508,6 +469,7 @@ Proof.
       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.
   - (* Others *)
@@ -575,7 +537,8 @@ Proof.
         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.  
+        { 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.
     + (* Bjumptable *)
@@ -591,6 +554,7 @@ Proof.
         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.
   - (* mib_exit *)
@@ -599,7 +563,7 @@ Proof.
     inversion H; subst;
     try (inv IS_EXPD; try inv H5; discriminate; fail);
     inversion STEP; subst; try_simplify_someHyps; intros.
-    + (* Bnop *)
+    + (* Bnop is_rtl *)
       eapply match_strong_state_simu.
       1,2: do 2 (econstructor; eauto).
       econstructor; eauto.
@@ -637,7 +601,8 @@ Proof.
     intros; rewrite H12 in BTL_RUN. destruct b;
     eapply match_strong_state_simu; eauto.
     1,3: inv H2; econstructor; eauto.
-    1,3,5,7: inv IS_EXPD; auto; discriminate.
+    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-4: eapply star_right; eauto.
     assert (measure bnot > 0) by apply measure_pos; lia.
     assert (measure bso > 0) by apply measure_pos; lia.
@@ -698,6 +663,7 @@ Proof.
       * apply expand_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.
         all: erewrite preserv_fnparams; eauto.
         constructor.
@@ -719,7 +685,8 @@ Proof.
     + apply expand_matchiblock_correct in MI.
       econstructor. econstructor; eauto.
       apply expand_correct; trivial.
-      constructor. apply expand_preserves_iblock_istep_run.
+      constructor. congruence. eapply expand_entry_isnt_bnop; eauto.
+      econstructor. apply expand_preserves_iblock_istep_run.
       eapply expand_entry_isnt_goto; eauto.
 Qed.