Now supporting Bnop insertion in conditions

5 files changed, 135 insertions, 139 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.
diff --git a/scheduling/BTLtoRTLaux.ml b/scheduling/BTLtoRTLaux.ml
index b4833b2c..36d3e6a4 100644
--- a/scheduling/BTLtoRTLaux.ml
+++ b/scheduling/BTLtoRTLaux.ml
@@ -6,15 +6,11 @@ open AuxTools
 open DebugPrint
 open BTLaux
 
-let is_atom = function
-  | Bseq (_, _) | Bcond (_, _, _, _, _) -> false
-  | _ -> true
-
 let get_inumb iinfo = P.of_int iinfo.inumb
 
 let rec get_ib_num = function
   | BF (Bgoto s, _) -> s
-  | Bnop iinfo
+  | Bnop Some iinfo
   | Bop (_, _, _, iinfo)
   | Bload (_, _, _, _, _, iinfo)
   | Bstore (_, _, _, _, iinfo)
@@ -22,6 +18,7 @@ let rec get_ib_num = function
   | BF (_, iinfo) ->
       get_inumb iinfo
   | Bseq (ib1, _) -> get_ib_num ib1
+  | Bnop None -> failwith "get_ib_num: Bnop None found"
 
 let translate_function code entry =
   let rtl_code = ref PTree.empty in
@@ -45,23 +42,21 @@ let translate_function code entry =
           | Bcond (cond, lr, BF (Bgoto s1, _), BF (Bgoto s2, _), iinfo) ->
               next_nodes := s1 :: s2 :: !next_nodes;
               Some (Icond (cond, lr, s1, s2, iinfo.pcond), get_inumb iinfo)
-          | Bcond (cond, lr, BF (Bgoto s1, _), ib2, iinfo) ->
+          | Bcond (cond, lr, BF (Bgoto s1, _), Bnop None, iinfo) ->
               assert (iinfo.pcond = Some false);
               next_nodes := s1 :: !next_nodes;
-              translate_btl_block ib2 None;
               Some
-                ( Icond (cond, lr, s1, get_ib_num ib2, iinfo.pcond),
+                ( Icond (cond, lr, s1, get_ib_num (get_some k), iinfo.pcond),
                   get_inumb iinfo )
           (* TODO gourdinl remove dynamic check *)
           | Bcond (_, _, _, _, _) ->
               failwith "translate_function: invalid Bcond"
           | Bseq (ib1, ib2) ->
-              (* TODO gourdinl remove dynamic check *)
-              assert (is_atom ib1);
               translate_btl_block ib1 (Some ib2);
               translate_btl_block ib2 None;
               None
-          | Bnop iinfo -> Some (Inop (get_ib_num (get_some k)), get_inumb iinfo)
+          | Bnop Some iinfo -> Some (Inop (get_ib_num (get_some k)), get_inumb iinfo)
+          | Bnop None -> failwith "translate_function: invalid Bnop"
           | Bop (op, lr, rd, iinfo) ->
               Some (Iop (op, lr, rd, get_ib_num (get_some k)), get_inumb iinfo)
           | Bload (trap, chk, addr, lr, rd, iinfo) ->
diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v
index 9b37d8fa..2e8d960c 100644
--- a/scheduling/BTLtoRTLproof.v
+++ b/scheduling/BTLtoRTLproof.v
@@ -202,6 +202,17 @@ Proof.
   eapply plus_trans; eauto.
 Qed.
 
+Lemma css_E0_trans isfst isfst' s0 s1 s2:
+  cond_star_step (isfst=false) s0 E0 s1 ->
+  cond_star_step (false=isfst') s1 E0 s2 ->
+  cond_star_step (isfst=isfst') s0 E0 s2.
+Proof.
+  intros S1 S2.
+  inversion S1; subst; eauto.
+  inversion S2; subst; eauto.
+  eapply css_plus_trans; eauto.
+Qed.
+
 Lemma css_star P s0 s1 t:
   cond_star_step P s0 t s1 ->
   star RTL.step tge s0 t s1.
@@ -219,7 +230,7 @@ Lemma iblock_istep_simulation sp dupmap stack' f' rs0 m0 ib rs1 m1 ofin
   forall pc0 opc isfst
   (MIB: match_iblock dupmap (RTL.fn_code f') isfst pc0 ib opc),
    match ofin with 
-   | None => exists pc1,(opc = Some pc1) /\ plus RTL.step tge (RTL.State stack' f' sp pc0 rs0 m0) E0 (RTL.State stack' f' sp pc1 rs1 m1)
+   | None => exists pc1,(opc = Some pc1) /\ cond_star_step (isfst = false) (RTL.State stack' f' sp pc0 rs0 m0) E0 (RTL.State stack' f' sp pc1 rs1 m1)
    | Some fin =>
       exists isfst' pc1 iinfo, match_iblock dupmap (RTL.fn_code f') isfst' pc1 (BF fin iinfo) None
                  /\ cond_star_step (isfst = isfst') (RTL.State stack' f' sp pc0 rs0 m0) E0 (RTL.State stack' f' sp pc1 rs1 m1)
@@ -231,19 +242,19 @@ Proof.
     subst.
     repeat eexists; eauto.
   - (* exec_nop *)
-    inv MIB. exists pc'; split; eauto.
+    inv MIB; eexists; split; econstructor; eauto.
   - (* exec_op *)
-    inv MIB. exists pc'; split; auto.
+    inv MIB. exists pc'; split; auto; constructor.
     apply plus_one. eapply exec_Iop; eauto.
     erewrite <- eval_operation_preserved; eauto.
     intros; rewrite symbols_preserved; trivial.
   - (* exec_load *)
-    inv MIB. exists pc'; split; auto.
+    inv MIB. exists pc'; split; auto; constructor.
     apply plus_one. eapply exec_Iload; eauto.
     erewrite <- eval_addressing_preserved; eauto.
     intros; rewrite symbols_preserved; trivial.
   - (* exec_store *)
-    inv MIB. exists pc'; split; auto.
+    inv MIB. exists pc'; split; auto; constructor.
     apply plus_one. eapply exec_Istore; eauto.
     erewrite <- eval_addressing_preserved; eauto.
     intros; rewrite symbols_preserved; trivial.
@@ -257,10 +268,10 @@ Proof.
     destruct ofin; simpl.
     + intros (ifst2 & pc2 & iinfo & M2 & STEP2).
       repeat eexists; eauto.
-      eapply css_plus_trans; eauto.
+      eapply css_E0_trans; eauto. 
     + intros (pc2 & EQpc2 & STEP2); inv EQpc2.
       eexists; split; auto.
-      eapply plus_trans; eauto.
+      eapply css_E0_trans; eauto.
   - (* exec_cond *)
     inv MIB.
     rename H10 into JOIN. (* is_join_opt opc1 opc2 opc *)
@@ -275,7 +286,7 @@ Proof.
         intros (pc1 & OPC & PLUS). inv OPC.
         inv JOIN; eexists; split; eauto.
         all:
-          eapply plus_trans; eauto.
+          eapply css_plus_trans; eauto.
     + (* taking ifnot *)
       destruct ofin; simpl.
       * (* ofin is Some final *)
@@ -286,7 +297,7 @@ Proof.
         intros (pc1 & OPC & PLUS). subst.
         inv JOIN; eexists; split; eauto.
         all:
-          eapply plus_trans; eauto.
+          eapply css_plus_trans; eauto.
 Qed.
 
 Lemma final_simu_except_goto sp dupmap stack stack' f f' rs1 m1 pc1 fin t s
diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml
index 43556150..4be2b180 100644
--- a/scheduling/RTLtoBTLaux.ml
+++ b/scheduling/RTLtoBTLaux.ml
@@ -2,9 +2,9 @@ open Maps
 open RTL
 open BTL
 open Registers
-open DebugPrint
 open PrintBTL
 open AuxTools
+open DebugPrint
 open BTLaux
 
 let undef_node = -1
@@ -20,13 +20,13 @@ let encaps_final inst osucc =
   | BF _ | Bcond _ -> inst
   | _ -> Bseq (inst, BF (Bgoto (get_some @@ osucc), def_iinfo))
 
-let translate_inst iinfo inst is_final =
+let translate_inst (iinfo: BTL.inst_info) inst is_final =
   let osucc = ref None in
   let btli =
     match inst with
     | Inop s ->
         osucc := Some s;
-        Bnop iinfo
+        Bnop (Some iinfo)
     | Iop (op, lr, rd, s) ->
         osucc := Some s;
         Bop (op, lr, rd, iinfo)
@@ -80,12 +80,13 @@ let translate_function code entry join_points =
                 assert (s = ifnot);
                 next_nodes := !next_nodes @ non_predicted_successors inst psucc;
                 iinfo.pcond <- info;
+                Bseq (
                 Bcond
                   ( cond,
                     lr,
                     BF (Bgoto ifso, def_iinfo),
-                    build_btl_block s,
-                    iinfo )
+                    Bnop None,
+                    iinfo ), build_btl_block s)
             | _ -> Bseq (translate_inst iinfo inst false, build_btl_block s))
         | None ->
             debug "BLOCK END.\n";
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.