From b063fb03af84483671833d40491f4fa8d2c8b4c9 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Fri, 23 Jul 2021 18:25:00 +0200
Subject: non trapping loads

---
 scheduling/BTL.v | 51 ++++++++++++++++++++++++++++++++++++++-------------
 1 file changed, 38 insertions(+), 13 deletions(-)

(limited to 'scheduling/BTL.v')

diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index 6536addb..96377943 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -205,7 +205,7 @@ 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 *)
+(* 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
@@ -217,11 +217,10 @@ Inductive has_loaded sp rs m chunk addr args v: trapping_mode -> Prop :=
       (DEFAULT: v = default_notrap_load_value chunk)
       : 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,15 +228,9 @@ Inductive iblock_istep sp: regset -> mem -> iblock -> regset -> mem -> option fi
   | 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
-  | exec_load_TRAP rs m chunk addr args dst a v iinfo
-     (EVAL: eval_addressing ge sp addr rs##args = Some a)
-     (LOAD: Mem.loadv chunk m a = Some v)
-     : iblock_istep sp rs m (Bload TRAP chunk addr args dst iinfo) (rs#dst <- v) m None
-(* TODO: replace [exec_load_TRAP] above by this one. See "new scheme" for "NOTRAP" above
-  | exec_load rs m trap chunk addr args dst v
+  | exec_load rs m trap chunk addr args dst v iinfo
       (LOAD: has_loaded sp rs m chunk addr args v trap)
-     : iblock_istep sp rs m (Bload trap chunk addr args dst) (rs#dst <- v) m None
-*)
+     : 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)
      (STORE: Mem.storev chunk m a rs#src = Some m')
@@ -274,7 +267,18 @@ Fixpoint iblock_istep_run sp ib rs m: option outcome :=
       SOME v <- Mem.loadv chunk m a IN
       Some {| _rs := rs#dst <- v; _m:= m; _fin := None |}
   | Bload NOTRAP chunk addr args dst _ =>
-      None (* TODO *)
+      match eval_addressing ge sp addr rs##args with
+      | Some a =>
+          match Mem.loadv chunk m a with
+          | Some v => Some {| _rs := rs#dst <- v; _m:= m; _fin := None |}
+          | None =>
+              let v := default_notrap_load_value chunk in
+              Some {| _rs := rs#dst <- v; _m:= m; _fin := None |}
+          end
+      | None =>
+          let v := default_notrap_load_value chunk in
+          Some {| _rs := rs#dst <- v; _m:= m; _fin := None |}
+      end
   | Bstore chunk addr args src _ =>
       SOME a <- eval_addressing ge sp addr rs##args IN
       SOME m' <- Mem.storev chunk m a rs#src IN
@@ -291,13 +295,34 @@ Fixpoint iblock_istep_run sp ib rs m: option outcome :=
       iblock_istep_run sp (if b then ifso else ifnot) rs m
   end.
 
+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 ->
+  iblock_istep sp rs m ib rs' m ofin <->
+  iblock_istep_run sp ib rs m = Some {| _rs := rs'; _m := m; _fin := ofin |}.
+Proof.
+  split; subst; inv H1; simpl in *; intros.
+  - destruct trap; inv H; simpl in *; repeat autodestruct.
+  - inv H; autodestruct; rewrite LOAD; auto.
+  - destruct trap; inv H; simpl in *;
+    rewrite EVAL, LOAD in H1; inv H1; repeat econstructor; eauto.
+  - generalize H; autodestruct.
+    + rewrite LOAD in *; inv H; auto; constructor.
+      eapply has_loaded_default; eauto; try_simplify_someHyps.
+    + inv H; constructor. eapply has_loaded_default; eauto; try_simplify_someHyps.
+Qed.
+Local Hint Resolve iblock_istep_run_equiv_load: core.
+
 Lemma iblock_istep_run_equiv sp rs m ib rs' m' ofin:
   iblock_istep sp rs m ib rs' m' ofin <-> iblock_istep_run sp ib rs m = Some {| _rs := rs'; _m:= m'; _fin := ofin |}.
 Proof.
   constructor.
-  - induction 1; simpl; try autodestruct; try_simplify_someHyps.
+  - induction 1; try (eapply iblock_istep_run_equiv_load; eauto; fail);
+    simpl; try autodestruct; try_simplify_someHyps.
   - generalize rs m rs' m' ofin; clear rs m rs' m' ofin.
     induction ib; simpl; repeat (try autodestruct; try_simplify_someHyps).
+    1,2: constructor; eapply has_loaded_default; try_simplify_someHyps.
     destruct o; try_simplify_someHyps; subst; eauto.
 Qed.
 
-- 
cgit