idea of a new scheme to define the semantics of LOAD NOTRAP

1 files changed, 22 insertions, 0 deletions

diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index fb67d150..8ccab024 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -175,6 +175,23 @@ 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 = default_notrap_load_value chunk)
+      : has_loaded sp rs m chunk addr args v NOTRAP 
+  .
+
+(* 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: iblock_istep sp rs m (BF fin) rs m (Some fin)
@@ -186,6 +203,11 @@ Inductive iblock_istep sp: regset -> mem -> iblock -> regset -> mem -> option fi
      (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) (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
+      (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
+*)
   | exec_store rs m chunk addr args src a m' 
      (EVAL: eval_addressing ge sp addr rs##args = Some a)
      (STORE: Mem.storev chunk m a rs#src = Some m')