Merge branch 'RTL_has_loaded' into kvx-work

1 files changed, 28 insertions, 26 deletions

diff --git a/backend/KillUselessMovesproof.v b/backend/KillUselessMovesproof.v
index 629aa6aa..7309c28e 100644
--- a/backend/KillUselessMovesproof.v
+++ b/backend/KillUselessMovesproof.v
@@ -227,32 +227,34 @@ Proof.
   apply eval_operation_preserved. exact symbols_preserved.
   constructor; auto using same_rs_write.
 (* load *)
-- econstructor; split.
-  assert (eval_addressing tge sp addr rs' ## args = Some a).
-  { rewrite <- H0.
-    rewrite (same_rs_subst rs rs' args SAME).
-    apply eval_addressing_preserved. exact symbols_preserved.
-  }
-  eapply exec_Iload; eauto.
-  constructor; auto using same_rs_write.
-- (* load notrap1 *)
-  econstructor; split.
-  assert (eval_addressing tge sp addr rs' ## args = None).
-  { rewrite <- H0.
-    rewrite (same_rs_subst rs rs' args SAME).
-    apply eval_addressing_preserved. exact symbols_preserved.
-  }
-  eapply exec_Iload_notrap1; eauto.
-  constructor; auto using same_rs_write.
-- (* load notrap2 *)
-  econstructor; split.
-  assert (eval_addressing tge sp addr rs' ## args = Some a).
-  { rewrite <- H0.
-    rewrite (same_rs_subst rs rs' args SAME).
-    apply eval_addressing_preserved. exact symbols_preserved.
-  }
-  eapply exec_Iload_notrap2; eauto.
-  constructor; auto using same_rs_write. 
+- inv H0.
+  + econstructor; split.
+    assert (eval_addressing tge sp addr rs' ## args = Some a).
+    { rewrite <- EVAL.
+      rewrite (same_rs_subst rs rs' args SAME).
+      apply eval_addressing_preserved. exact symbols_preserved.
+    }
+    eapply exec_Iload; eauto. eapply has_loaded_normal; eauto.
+    constructor; auto using same_rs_write.
+  + destruct (eval_addressing) eqn:EVAL in LOAD.
+    * specialize (LOAD v). econstructor; split.
+      assert (eval_addressing tge sp addr rs' ## args = Some v).
+      { rewrite <- EVAL.
+        rewrite (same_rs_subst rs rs' args SAME).
+        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 using same_rs_write. 
+    * econstructor; split.
+      assert (eval_addressing tge sp addr rs' ## args = None).
+      { rewrite <- EVAL.
+        rewrite (same_rs_subst rs rs' args SAME).
+        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 using same_rs_write.
 - (* store *)
   econstructor; split.
   assert (eval_addressing tge sp addr rs' ## args = Some a).