1 files changed, 28 insertions, 45 deletions
diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v
index 39fc10fb..4eb0ba23 100644
--- a/backend/Tailcallproof.v
+++ b/backend/Tailcallproof.v
@@ -427,51 +427,34 @@ Proof.
 - (* load *)
   TransfInstr.
   assert (Val.lessdef_list (rs##args) (rs'##args)). apply regs_lessdef_regs; auto.
-  exploit eval_addressing_lessdef; eauto.
-  intros [a' [ADDR' ALD]].
-  exploit Mem.loadv_extends; eauto.
-  intros [v' [LOAD' VLD]].
-  left. exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- v') m'); split.
-  eapply exec_Iload with (a := a'). eauto.  rewrite <- ADDR'.
-  apply eval_addressing_preserved. exact symbols_preserved. eauto.
-  econstructor; eauto. apply set_reg_lessdef; auto.
-
-- (* load notrap1 *)
-  TransfInstr.
-  assert (Val.lessdef_list (rs##args) (rs'##args)). apply regs_lessdef_regs; auto.
-  left.
-  exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- Vundef) m'); split.
-  eapply exec_Iload_notrap1.
-  eassumption.
-  eapply eval_addressing_lessdef_none. eassumption.
-  erewrite eval_addressing_preserved.
-  eassumption. exact symbols_preserved.
-
-  econstructor; eauto. apply set_reg_lessdef; auto.
-
-- (* load notrap2 *)
-  TransfInstr.
-  assert (Val.lessdef_list (rs##args) (rs'##args)). apply regs_lessdef_regs; auto.
-  left.
-
-  exploit eval_addressing_lessdef; eauto.
-  intros [a' [ADDR' ALD]].
-  
-  destruct (Mem.loadv chunk m' a') eqn:Echunk2.
-  + exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- v) m'); split.
-    eapply exec_Iload with (a:=a'). eassumption.
-    erewrite eval_addressing_preserved.
-    eassumption.
-    exact symbols_preserved.
-    assumption.
-    econstructor; eauto. apply set_reg_lessdef; auto.
-  + exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- Vundef) m'); split.
-    eapply exec_Iload_notrap2. eassumption.
-    erewrite eval_addressing_preserved.
-    eassumption.
-    exact symbols_preserved.
-    assumption.
-    econstructor; eauto. apply set_reg_lessdef; auto.
+  inv H0.
+  + exploit eval_addressing_lessdef; eauto.
+    intros [a' [EVAL' ALD]].
+    exploit Mem.loadv_extends; eauto.
+    intros [v' [LOAD' VLD]].
+    left. exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- v') m'); split.
+    * try (eapply exec_Iload; eauto; eapply has_loaded_normal; eauto;
+      rewrite <- EVAL'; apply eval_addressing_preserved; exact symbols_preserved).
+    * econstructor; eauto. apply set_reg_lessdef; auto.
+  + destruct (eval_addressing) eqn:EVAL in LOAD.
+    * left. exploit eval_addressing_lessdef; eauto.
+      intros [a' [EVAL' ALD]]. specialize (LOAD v).
+      destruct (Mem.loadv chunk m' a') eqn:Echunk2.
+      -- exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- v0) m'); split.
+         ++ try (eapply exec_Iload; eauto; eapply has_loaded_normal; eauto;
+            erewrite eval_addressing_preserved; eauto; exact symbols_preserved).
+         ++ econstructor; eauto. apply set_reg_lessdef; auto.
+      -- exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- Vundef) m'); split.
+         ++ eapply exec_Iload; eauto. eapply has_loaded_default; intuition.
+            erewrite (eval_addressing_preserved ge tge) in H2; [ idtac | exact symbols_preserved].
+            rewrite EVAL' in H2; inv H2. assumption.
+         ++ econstructor; eauto. apply set_reg_lessdef; auto.
+    * left. exists (State s' (transf_function f) (Vptr sp0 Ptrofs.zero) pc' (rs'#dst <- Vundef) m'); split.
+      -- eapply exec_Iload; eauto. apply has_loaded_default; auto; intros.
+         eapply eval_addressing_lessdef_none in EVAL; eauto.
+         erewrite (eval_addressing_preserved ge tge) in H0; [ idtac | exact symbols_preserved].
+         congruence.
+      -- econstructor; eauto. apply set_reg_lessdef; auto.
     
 - (* store *)
   TransfInstr.