splitting is_expand property with a weak version for conditions

1 files changed, 59 insertions, 22 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.