splitting is_expand property with a weak version for conditions

2 files changed, 117 insertions, 78 deletions

diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index 05391c58..0f9ef44f 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -812,7 +812,7 @@ Definition is_goto (ib: iblock): bool :=
   | _ => false
   end.
 
-Definition is_atom (ib: iblock): bool :=
+Definition is_RTLatom (ib: iblock): bool :=
  match ib with
  | Bseq _ _ | Bcond _ _ _ _ _ | Bnop None => false 
  | _ => true
@@ -824,43 +824,80 @@ Proof.
   intuition congruence.
 Defined.
 
-(** Is expand property to only support atomic instructions on the left part of a Bseq *)
+(** Is expand property to only support atomic instructions on the left part of a Bseq:
+   The tree is right-expanded, and block are normalized to simplify RTL simulation *)
 Inductive is_expand: iblock -> Prop :=
   | exp_Bseq ib1 ib2:
-     is_atom ib1 = true ->
+     is_RTLatom ib1 = true ->
      is_expand ib2 -> 
      is_expand (Bseq ib1 ib2)
-  | exp_Bcond cond args ib1 ib2 iinfo:
-     is_expand ib1 \/ ib1 = Bnop None ->
-     is_expand ib2 \/ ib2 = Bnop None -> 
-     is_expand (Bcond cond args ib1 ib2 iinfo)
+  | exp_Bcond cond args ib1 ib2 i:
+     is_expand ib1 ->
+     is_expand ib2 -> 
+     is_expand (Bcond cond args ib1 ib2 i)
   | exp_others ib:
-     is_atom ib = true ->
+     is_RTLatom ib = true ->
      is_expand ib
      .
 Local Hint Constructors is_expand: core.
 
-Fixpoint expand (ib: iblock) (k: iblock): iblock :=
+(** The weak version with more specific hypothesis for conditions *)
+Inductive is_wexpand: iblock -> Prop :=
+  | wexp_Bseq ib1 ib2:
+     is_RTLatom ib1 = true ->
+     is_wexpand ib2 -> 
+     is_wexpand (Bseq ib1 ib2)
+  | wexp_Bcond cond args ib1 ib2 iinfo:
+     (ib1 <> Bnop None -> is_wexpand ib1) ->
+     (ib2 <> Bnop None -> is_wexpand ib2) ->
+     is_wexpand (Bcond cond args ib1 ib2 iinfo)
+  | wexp_others ib:
+     is_RTLatom ib = true ->
+     is_wexpand ib
+     .
+Local Hint Constructors is_wexpand: core.
+
+Fixpoint normRTL (ib: iblock) (k: iblock): iblock :=
   match ib with
-  | Bseq ib1 ib2 => expand ib1 (expand ib2 k)
+  | Bseq ib1 ib2 => normRTL ib1 (normRTL ib2 k)
   | Bcond cond args ib1 ib2 iinfo => 
-     Bcond cond args (expand ib1 k) (expand ib2 k) iinfo
+     Bcond cond args (normRTL ib1 k) (normRTL ib2 k) iinfo
   | BF fin iinfo => BF fin iinfo
   | Bnop None => k
   | ib =>
       if Bnop_dec k then ib else Bseq ib k
   end.
 
-Lemma expand_correct ib: forall k,
-  (k <> (Bnop None) -> is_expand k)
-  -> (expand ib k) <> (Bnop None)
-  -> is_expand (expand ib k).
+Lemma normRTL_correct ib: forall k,
+  (k <> (Bnop None) -> is_wexpand k) ->
+  (normRTL ib k) <> Bnop None ->
+  is_wexpand (normRTL ib k).
 Proof.
-  induction ib; simpl; intros; auto.
-  1-4:
-    try destruct oiinfo;
-    destruct (Bnop_dec k); auto.
-  constructor.
-  - destruct (Bnop_dec (expand ib1 k)); auto.
-  - destruct (Bnop_dec (expand ib2 k)); auto.
+  induction ib; simpl; intros; try autodestruct; auto.
+  intros; destruct (Bnop_dec k); auto.
+Qed.
+
+Lemma is_join_opt_None {A} (opc1 opc2: option A): 
+  is_join_opt opc1 opc2 None -> opc1 = None /\ opc2 = None.
+Proof.
+  intros X. inv X; auto.
+Qed.
+
+Lemma match_iblock_None_not_Bnop dupmap cfg isfst pc ib: 
+  match_iblock dupmap cfg isfst pc ib None -> ib <> Bnop None.
+Proof.
+  intros X; inv X; try congruence.
+Qed.
+Local Hint Resolve match_iblock_None_not_Bnop: core.
+
+Lemma is_wexpand_expand dupmap cfg ib:
+  is_wexpand ib ->
+  forall isfst pc
+  (MIB: match_iblock dupmap cfg isfst pc ib None),
+  is_expand ib.
+Proof.
+  induction 1; simpl; intros; auto; try (inv MIB); eauto.
+  (* Bcond *)
+  destruct (is_join_opt_None opc1 opc2); subst; eauto.
+  econstructor; eauto.
 Qed.
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.