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/Allnontrapproof.v | 38 +++++++++++++++++++++-----------------
 1 file changed, 21 insertions(+), 17 deletions(-)

(limited to 'backend/Allnontrapproof.v')

diff --git a/backend/Allnontrapproof.v b/backend/Allnontrapproof.v
index 157c5de2..f3b10600 100644
--- a/backend/Allnontrapproof.v
+++ b/backend/Allnontrapproof.v
@@ -111,6 +111,8 @@ Inductive match_states: RTL.state -> RTL.state -> Prop :=
       match_states (Returnstate stk v m)
                    (Returnstate stk' v m).
 
+(*Lemma load_notrap_simu_correct:*)
+
 Lemma step_simulation:
   forall S1 t S2, RTL.step ge S1 t S2 ->
   forall S1', match_states S1 S1' ->
@@ -126,23 +128,25 @@ Proof.
   rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved.
   constructor; auto.
 (* load *)
-- econstructor; split.
-  assert (eval_addressing tge sp addr rs ## args = Some a).
-  rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
-  eapply exec_Iload; eauto.
-  constructor; auto.
-- (* load notrap1 *)
-  econstructor; split.
-  assert (eval_addressing tge sp addr rs ## args = None).
-  rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
-  eapply exec_Iload_notrap1; eauto.
-  constructor; auto.
-- (* load notrap2 *)
-  econstructor; split.
-  assert (eval_addressing tge sp addr rs ## args = Some a).
-  rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
-  eapply exec_Iload_notrap2; eauto.
-  constructor; auto. 
+- inv H0.
+  + econstructor; split.
+    assert (eval_addressing tge sp addr rs ## args = Some a).
+    rewrite <- EVAL. apply eval_addressing_preserved. exact symbols_preserved.
+    eapply exec_Iload; eauto. eapply has_loaded_normal; eauto.
+    constructor; auto.
+  + destruct (eval_addressing) eqn:EVAL in LOAD.
+    * specialize (LOAD v). econstructor; split.
+      assert (eval_addressing tge sp addr rs ## args = Some v).
+      rewrite <- EVAL. apply eval_addressing_preserved. exact symbols_preserved.
+      eapply exec_Iload; eauto. eapply has_loaded_default; eauto.
+      intros a EVAL'; rewrite H0 in EVAL'; inv EVAL'. apply LOAD; auto.
+      constructor; auto.
+    * econstructor; split.
+      assert (eval_addressing tge sp addr rs ## args = None).
+      rewrite <- EVAL. apply eval_addressing_preserved. exact symbols_preserved.
+      eapply exec_Iload; eauto. eapply has_loaded_default; eauto.
+      intros a EVAL'; rewrite H0 in EVAL'; inv EVAL'.
+      constructor; auto. 
 - (* store *)
   econstructor; split.
   assert (eval_addressing tge sp addr rs ## args = Some a).
-- 
cgit