Porting the BTL non-trap loads approach to RTL

3 files changed, 23 insertions, 25 deletions

diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index f832085c..c10b8ac2 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -205,22 +205,8 @@ Definition find_function (ros: reg + ident) (rs: regset) : option fundef :=
 
 Local Open Scope option_monad_scope.
 
-(* TODO: a new (hopefully simpler) scheme to support "NOTRAP" wrt current scheme of RTL *)
-
-Inductive has_loaded sp rs m chunk addr args v: trapping_mode -> Prop :=
-  | has_loaded_normal a trap
-      (EVAL: eval_addressing ge sp addr rs##args = Some a)
-      (LOAD: Mem.loadv chunk m a = Some v)
-      : has_loaded sp rs m chunk addr args v trap
-  | has_loaded_default
-      (LOAD: forall a, eval_addressing ge sp addr rs##args = Some a -> Mem.loadv chunk m a = None)
-      (DEFAULT: v = Vundef)
-      : has_loaded sp rs m chunk addr args v NOTRAP 
-  .
 Local Hint Constructors has_loaded: core.
 
-(* TODO: move this scheme in "Memory" module if this scheme is useful ! *)
-
 (** 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)
@@ -229,7 +215,7 @@ Inductive iblock_istep sp: regset -> mem -> iblock -> regset -> mem -> option fi
      (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
   | exec_load rs m trap chunk addr args dst v iinfo
-      (LOAD: has_loaded sp rs m chunk addr args v trap)
+      (LOAD: has_loaded ge sp rs m chunk addr args v trap)
      : iblock_istep sp rs m (Bload trap chunk addr args dst iinfo) (rs#dst <- v) m None
   | exec_store rs m chunk addr args src a m' iinfo
      (EVAL: eval_addressing ge sp addr rs##args = Some a)
@@ -296,7 +282,7 @@ Fixpoint iblock_istep_run sp ib rs m: option outcome :=
 Lemma iblock_istep_run_equiv_load sp ib v rs rs' m trap chunk addr args dst iinfo ofin:
   ib = (Bload trap chunk addr args dst iinfo) ->
   rs' = rs # dst <- v ->
-  has_loaded sp rs m chunk addr args v trap ->
+  has_loaded ge sp rs m chunk addr args v trap ->
   iblock_istep sp rs m ib rs' m ofin <->
   iblock_istep_run sp ib rs m = Some {| _rs := rs'; _m := m; _fin := ofin |}.
 Proof.
diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v
index cbdc81bd..2e3c5cd8 100644
--- a/scheduling/BTLtoRTLproof.v
+++ b/scheduling/BTLtoRTLproof.v
@@ -230,12 +230,20 @@ Proof.
     intros; rewrite symbols_preserved; trivial.
   - (* exec_load *)
     inv MIB. exists pc'; split; auto; constructor.
-    apply plus_one. inv LOAD.
-    eapply exec_Iload; eauto.
-    all: try (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.
+    apply plus_one. inversion LOAD; subst.
+    + eapply exec_Iload; eauto. eapply has_loaded_normal; eauto.
+      rewrite <- EVAL. erewrite <- eval_addressing_preserved; eauto.
+      intros; rewrite symbols_preserved; trivial.
+    + destruct (eval_addressing) eqn:EVAL in LOAD0.
+      * specialize (LOAD0 v).
+        eapply exec_Iload; eauto. eapply has_loaded_default; eauto.
+        rewrite eval_addressing_preserved with (ge1:=ge).
+        intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'. apply LOAD0; auto.
+        intros; rewrite symbols_preserved; trivial.
+      * eapply exec_Iload; eauto. eapply has_loaded_default; eauto.
+        rewrite eval_addressing_preserved with (ge1:=ge).
+        intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'.
+        intros; rewrite symbols_preserved; trivial.
   - (* exec_store *)
     inv MIB. exists pc'; split; auto; constructor.
     apply plus_one. eapply exec_Istore; eauto.
diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v
index 0ca93bce..6ec32ffc 100644
--- a/scheduling/RTLtoBTLproof.v
+++ b/scheduling/RTLtoBTLproof.v
@@ -631,9 +631,13 @@ Proof.
       erewrite eval_operation_preserved in H12.
       erewrite H12 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;
+    (* Bload/Bstore *)
+    inv H12; [ idtac | destruct (eval_addressing) eqn:EVAL in LOAD;[ specialize (LOAD v) |] ];
+    rename LOAD into MEMT.
+    4: rename H12 into EVAL; rename H13 into MEMT.
+    all:
+      erewrite eval_addressing_preserved in EVAL;
+      try erewrite EVAL in BTL_RUN; try erewrite MEMT in BTL_RUN;
       simpl in BTL_RUN; try destruct trap; auto;
       intros; rewrite <- symbols_preserved; trivial.
   - (* mib_cond *)