From 173e6c25b2937d6e6941973aa7b116e1d6405513 Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@lilo.org>
Date: Tue, 2 Nov 2021 10:10:34 +0100
Subject: Porting the BTL non-trap loads approach to RTL

---
 backend/RTL.v | 30 ++++++++++++++----------------
 1 file changed, 14 insertions(+), 16 deletions(-)

(limited to 'backend/RTL.v')

diff --git a/backend/RTL.v b/backend/RTL.v
index fe350adf..b43fd377 100644
--- a/backend/RTL.v
+++ b/backend/RTL.v
@@ -181,6 +181,18 @@ Inductive state : Type :=
              (m: mem),                (**r memory state *)
       state.
 
+Inductive has_loaded {F V: Type} (genv: Genv.t F V) sp rs m chunk addr args v: trapping_mode -> Prop :=
+  | has_loaded_normal a trap
+      (EVAL: eval_addressing genv sp addr rs##args = Some a)
+      (LOAD: Mem.loadv chunk m a = Some v)
+      : has_loaded genv sp rs m chunk addr args v trap
+  | has_loaded_default
+      (LOAD: forall a, eval_addressing genv sp addr rs##args = Some a -> Mem.loadv chunk m a = None)
+      (DEFAULT: v = Vundef)
+      : has_loaded genv sp rs m chunk addr args v NOTRAP 
+  .
+Local Hint Constructors has_loaded: core.
+
 Section RELSEM.
 
 Variable ge: genv.
@@ -214,25 +226,11 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State s f sp pc rs m)
         E0 (State s f sp pc' (rs#res <- v) m)
   | exec_Iload:
-      forall s f sp pc rs m trap chunk addr args dst pc' a v,
+      forall s f sp pc rs m trap chunk addr args dst pc' v,
       (fn_code f)!pc = Some(Iload trap chunk addr args dst pc') ->
-      eval_addressing ge sp addr rs##args = Some a ->
-      Mem.loadv chunk m a = Some v ->
+      has_loaded ge sp rs m chunk addr args v trap ->
       step (State s f sp pc rs m)
         E0 (State s f sp pc' (rs#dst <- v) m)
-  | exec_Iload_notrap1:
-      forall s f sp pc rs m chunk addr args dst pc',
-      (fn_code f)!pc = Some(Iload NOTRAP chunk addr args dst pc') ->
-      eval_addressing ge sp addr rs##args = None ->
-      step (State s f sp pc rs m)
-        E0 (State s f sp pc' (rs#dst <- Vundef) m)
-  | exec_Iload_notrap2:
-      forall s f sp pc rs m chunk addr args dst pc' a,
-      (fn_code f)!pc = Some(Iload NOTRAP chunk addr args dst pc') ->
-      eval_addressing ge sp addr rs##args = Some a ->
-      Mem.loadv chunk m a = None->
-      step (State s f sp pc rs m)
-        E0 (State s f sp pc' (rs#dst <- Vundef) m)
   | exec_Istore:
       forall s f sp pc rs m chunk addr args src pc' a m',
       (fn_code f)!pc = Some(Istore chunk addr args src pc') ->
-- 
cgit