Now supporting Bnop insertion in conditions

1 files changed, 44 insertions, 22 deletions

diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index ca727f82..05391c58 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -58,7 +58,7 @@ Inductive iblock: Type :=
 (* final instructions that stops block execution *)
   | BF (fi: final) (iinfo: inst_info)
 (* basic instructions that continues block execution, except when aborting *)
-  | Bnop (iinfo: inst_info) (* nop instruction *)
+  | Bnop (oiinfo: option inst_info) (* nop instruction *)
   | Bop (op:operation) (args:list reg) (dest:reg) (iinfo: inst_info)
       (** performs the arithmetic operation [op] over the values of registers [args], stores the result in [dest] *)
   | Bload (trap:trapping_mode) (chunk:memory_chunk) (addr:addressing) (args:list reg) (dest:reg) (iinfo: inst_info)
@@ -204,7 +204,7 @@ Inductive has_loaded sp rs m chunk addr args v: trapping_mode -> Prop :=
 (** internal big-step execution of one iblock *)
 Inductive iblock_istep sp: regset -> mem -> iblock -> regset -> mem -> option final -> Prop :=
   | exec_final rs m fin iinfo: iblock_istep sp rs m (BF fin iinfo) rs m (Some fin)
-  | exec_nop rs m iinfo: iblock_istep sp rs m (Bnop iinfo) rs m None
+| exec_nop rs m oiinfo: iblock_istep sp rs m (Bnop oiinfo) rs m None
   | exec_op rs m op args res v iinfo
      (EVAL: eval_operation ge sp op rs##args m = Some v)
      : iblock_istep sp rs m (Bop op args res iinfo) (rs#res <- v) m None
@@ -425,9 +425,11 @@ Inductive match_iblock (dupmap: PTree.t node) (cfg: RTL.code): bool -> node -> i
       cfg!pc = Some i ->
       match_final_inst dupmap fi i ->
       match_iblock dupmap cfg isfst pc (BF fi iinfo) None
-  | mib_nop isfst pc pc' iinfo:
+  | mib_nop_on_rtl isfst pc pc' iinfo:
       cfg!pc = Some (Inop pc') ->
-      match_iblock dupmap cfg isfst pc (Bnop iinfo) (Some pc')
+      match_iblock dupmap cfg isfst pc (Bnop (Some iinfo)) (Some pc')
+  | mib_nop_skip pc:
+      match_iblock dupmap cfg false pc (Bnop None) (Some pc)
   | mib_op isfst pc pc' op lr r iinfo:
       cfg!pc = Some (Iop op lr r pc') ->
       match_iblock dupmap cfg isfst pc (Bop op lr r iinfo) (Some pc')
@@ -592,10 +594,16 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node)
           | _ => Error (msg "BTL.verify_block: incorrect cfg Bjumptable")
           end
       end
-  | Bnop _ =>
-      match cfg!pc with
-      | Some (Inop pc') => OK (Some pc')
-      | _ => Error (msg "BTL.verify_block: incorrect cfg Bnop")
+  | Bnop oiinfo =>
+      match oiinfo with
+      | Some _ =>
+          match cfg!pc with
+          | Some (Inop pc') => OK (Some pc')
+          | _ => Error (msg "BTL.verify_block: incorrect cfg Bnop")
+          end
+      | None =>
+          if negb isfst then OK (Some pc)
+          else Error (msg "BTL.verify_block: isfst is true Bnop (on_rtl is false)")
       end
   | Bop op lr r _ =>
       match cfg!pc with
@@ -712,8 +720,11 @@ Proof.
       destruct (Pos.eq_dec _ _); try discriminate. subst.
       inv EQ0. eapply mib_BF; eauto. constructor; assumption.
   - (* Bnop *)
-    destruct i; inv H.
-    constructor; assumption.
+    destruct oiinfo; simpl in *.
+    + destruct (cfg!pc) eqn:EQCFG; try discriminate.
+      destruct i0; inv H. constructor; assumption.
+    + destruct isfst; try discriminate. inv H.
+      constructor; assumption.
   - (* Bop *)
     destruct i; try discriminate.
     destruct (eq_operation _ _); try discriminate.
@@ -803,10 +814,16 @@ Definition is_goto (ib: iblock): bool :=
 
 Definition is_atom (ib: iblock): bool :=
  match ib with
- | Bseq _ _ | Bcond _ _ _ _ _ => false 
+ | Bseq _ _ | Bcond _ _ _ _ _ | Bnop None => false 
  | _ => true
  end.
 
+Definition Bnop_dec k: { k=Bnop None} + { k<>(Bnop None) }.
+Proof.
+  destruct k; simpl; try destruct oiinfo;
+  intuition congruence.
+Defined.
+
 (** Is expand property to only support atomic instructions on the left part of a Bseq *)
 Inductive is_expand: iblock -> Prop :=
   | exp_Bseq ib1 ib2:
@@ -814,8 +831,8 @@ Inductive is_expand: iblock -> Prop :=
      is_expand ib2 -> 
      is_expand (Bseq ib1 ib2)
   | exp_Bcond cond args ib1 ib2 iinfo:
-     is_expand ib1 ->
-     is_expand ib2 -> 
+     is_expand ib1 \/ ib1 = Bnop None ->
+     is_expand ib2 \/ ib2 = Bnop None -> 
      is_expand (Bcond cond args ib1 ib2 iinfo)
   | exp_others ib:
      is_atom ib = true ->
@@ -823,22 +840,27 @@ Inductive is_expand: iblock -> Prop :=
      .
 Local Hint Constructors is_expand: core.
 
-Fixpoint expand (ib: iblock) (k: option iblock): iblock :=
+Fixpoint expand (ib: iblock) (k: iblock): iblock :=
   match ib with
-  | Bseq ib1 ib2 => expand ib1 (Some (expand ib2 k))
+  | Bseq ib1 ib2 => expand ib1 (expand ib2 k)
   | Bcond cond args ib1 ib2 iinfo => 
      Bcond cond args (expand ib1 k) (expand ib2 k) iinfo
   | BF fin iinfo => BF fin iinfo
-  | ib => 
-    match k with 
-    | None => ib
-    | Some rem => Bseq ib rem
-    end
+  | Bnop None => k
+  | ib =>
+      if Bnop_dec k then ib else Bseq ib k
   end.
 
 Lemma expand_correct ib: forall k,
-  (match k with Some rem => is_expand rem | None => True end)
+  (k <> (Bnop None) -> is_expand k)
+  -> (expand ib k) <> (Bnop None)
   -> is_expand (expand ib k).
 Proof.
-  induction ib; simpl; intros; try autodestruct; auto.
+  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.
 Qed.