ci fix?

3 files changed, 17 insertions, 25 deletions

diff --git a/scheduling/BTLmatchRTL.v b/scheduling/BTLmatchRTL.v
index c271ae02..07131893 100644
--- a/scheduling/BTLmatchRTL.v
+++ b/scheduling/BTLmatchRTL.v
@@ -214,9 +214,9 @@ Inductive match_iblock (dupmap: PTree.t node) (cfg: RTL.code): bool -> node -> i
   | 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')
-  | mib_load isfst pc pc' m a lr r iinfo:
-      cfg!pc = Some (Iload TRAP m a lr r pc') -> 
-      match_iblock dupmap cfg isfst pc (Bload TRAP m a lr r iinfo) (Some pc')
+  | mib_load isfst pc pc' trap m a lr r iinfo:
+      cfg!pc = Some (Iload trap m a lr r pc') -> 
+      match_iblock dupmap cfg isfst pc (Bload trap m a lr r iinfo) (Some pc')
   | mib_store isfst pc pc' m a lr r iinfo:
       cfg!pc = Some (Istore m a lr r pc') -> 
       match_iblock dupmap cfg isfst pc (Bstore m a lr r iinfo) (Some pc')
@@ -407,7 +407,7 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node)
   | Bload tm m a lr r _ =>
       match cfg!pc with
       | Some (Iload tm' m' a' lr' r' pc') =>
-          if (trapping_mode_eq tm TRAP && trapping_mode_eq tm' TRAP) then
+          if (trapping_mode_eq tm tm') then
             if (chunk_eq m m') then
               if (eq_addressing a a') then
                 if (list_eq_dec Pos.eq_dec lr lr') then
@@ -417,7 +417,7 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node)
                 else Error (msg "BTL.verify_block: different lr in Bload")
               else Error (msg "BTL.verify_block: different addressing in Bload")
             else Error (msg "BTL.verify_block: different chunk in Bload")
-          else Error (msg "BTL.verify_block: NOTRAP trapping_mode unsupported in Bload")
+          else Error (msg "BTL.verify_block: different trapping_mode in Bload")
       | _ => Error (msg "BTL.verify_block: incorrect cfg Bload")
       end
   | Bstore m a lr r _ =>
@@ -520,8 +520,7 @@ Proof.
     constructor; assumption.
   - (* Bload *)
     destruct i; try discriminate.
-    do 2 (destruct (trapping_mode_eq _ _); try discriminate).
-    simpl in H.
+    destruct (trapping_mode_eq _ _); try discriminate.
     destruct (chunk_eq _ _); try discriminate.
     destruct (eq_addressing _ _); try discriminate.
     destruct (list_eq_dec _ _ _); try discriminate.
diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v
index 324f1d14..4ef55928 100644
--- a/scheduling/BTLtoRTLproof.v
+++ b/scheduling/BTLtoRTLproof.v
@@ -232,6 +232,8 @@ Proof.
     inv MIB. exists pc'; split; auto; constructor.
     apply plus_one. inv LOAD.
     eapply exec_Iload; eauto.
+    2: destruct (eval_addressing _ _ _ _) eqn:EVAL;
+    [ eapply exec_Iload_notrap2 | eapply exec_Iload_notrap1]; eauto.
     all: erewrite <- eval_addressing_preserved; eauto;
          intros; rewrite symbols_preserved; trivial.
   - (* exec_store *)
diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v
index 13ba5a29..0ca93bce 100644
--- a/scheduling/RTLtoBTLproof.v
+++ b/scheduling/RTLtoBTLproof.v
@@ -624,26 +624,17 @@ Proof.
   - (* mib_seq *)
     inv IS_EXPD; try discriminate.
     inv H; simpl in *; try congruence;
-    inv STEP; try_simplify_someHyps; eauto.
-    + (* Bnop is_rtl *)
-      intros; eapply match_strong_state_simu; eauto.
-    + (* Bop *)
-      intros; eapply match_strong_state_simu; eauto.
-      econstructor; eauto.
+    inv STEP; try_simplify_someHyps;
+    intros; eapply match_strong_state_simu; eauto;
+    econstructor; eauto.
+    { (* Bop *)
       erewrite eval_operation_preserved in H12.
       erewrite H12 in BTL_RUN; simpl in BTL_RUN; auto.
-      intros; rewrite <- symbols_preserved; trivial.
-    + (* Bload *)
-      intros; eapply match_strong_state_simu; eauto.
-      econstructor; eauto.
-      erewrite eval_addressing_preserved in H12.
-      erewrite H12, H13 in BTL_RUN; simpl in BTL_RUN; auto.
-      intros; rewrite <- symbols_preserved; trivial.
-    + (* Bstore *)
-      intros; eapply match_strong_state_simu; eauto.
-      econstructor; eauto.
-      erewrite eval_addressing_preserved in H12.
-      erewrite H12, H13 in BTL_RUN; simpl in BTL_RUN; auto.
+      intros; rewrite <- symbols_preserved; trivial. }
+    all: (* Bload / Bstore *)
+      erewrite eval_addressing_preserved in H12;
+      try erewrite H12 in BTL_RUN; try erewrite H13 in BTL_RUN;
+      simpl in BTL_RUN; try destruct trap; auto;
       intros; rewrite <- symbols_preserved; trivial.
   - (* mib_cond *)
     inv IS_EXPD; try discriminate.