1 files changed, 41 insertions, 49 deletions
diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v
index be20af0b..52332a82 100644
--- a/backend/Deadcodeproof.v
+++ b/backend/Deadcodeproof.v
@@ -797,113 +797,105 @@ Ltac UseTransfer :=
   apply eagree_update; eauto 2 with na.
 
 - (* load *)
-  TransfInstr; UseTransfer.
-  destruct (is_dead (nreg ne dst)) eqn:DEAD;
+  TransfInstr; UseTransfer. inv H0.
++ destruct (is_dead (nreg ne dst)) eqn:DEAD;
   [idtac|destruct (is_int_zero (nreg ne dst)) eqn:INTZERO];
   simpl in *.
-+ (* dead instruction, turned into a nop *)
+* (* dead instruction, turned into a nop *)
   econstructor; split.
   eapply exec_Inop; eauto.
   eapply match_succ_states; eauto. simpl; auto.
   apply eagree_update_dead; auto with na.
-+ (* instruction with needs = [I Int.zero], turned into a load immediate of zero. *)
+* (* instruction with needs = [I Int.zero], turned into a load immediate of zero. *)
   econstructor; split.
   eapply exec_Iop with (v := Vint Int.zero); eauto.
   eapply match_succ_states; eauto. simpl; auto.
   apply eagree_update; auto.
   rewrite is_int_zero_sound by auto.
   destruct v; simpl; auto. apply iagree_zero.
-+ (* preserved *)
+* (* preserved *)
   exploit eval_addressing_lessdef. eapply add_needs_all_lessdef; eauto. eauto.
   intros (ta & U & V). inv V; try discriminate.
-  destruct ta; simpl in H1; try discriminate.
+  destruct ta; simpl in EVAL; try discriminate.
   exploit magree_load; eauto.
   exploit aaddressing_sound; eauto. intros (bc & A & B & C).
   intros. apply nlive_add with bc i; assumption.
   intros (tv & P & Q).
   econstructor; split.
-  eapply exec_Iload with (a := Vptr b i). eauto.
-  rewrite <- U. apply eval_addressing_preserved. exact symbols_preserved.
-  eauto.
+  try (eapply exec_Iload; eauto; eapply has_loaded_normal; eauto;
+  try (rewrite <- U; apply eval_addressing_preserved; exact symbols_preserved; fail); eauto).
   eapply match_succ_states; eauto. simpl; auto.
   apply eagree_update; eauto 2 with na.
   eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto.
-
-- (* load notrap1 *)
-  TransfInstr; UseTransfer.
++ destruct (eval_addressing) eqn:EVAL in LOAD.
+* specialize (LOAD v).
   destruct (is_dead (nreg ne dst)) eqn:DEAD;
   [idtac|destruct (is_int_zero (nreg ne dst)) eqn:INTZERO];
   simpl in *.
-+ (* dead instruction, turned into a nop *)
+** (* dead instruction, turned into a nop *)
   econstructor; split.
   eapply exec_Inop; eauto.
   eapply match_succ_states; eauto. simpl; auto.
   apply eagree_update_dead; auto with na.
-+ (* instruction with needs = [I Int.zero], turned into a load immediate of zero. *)
+** (* instruction with needs = [I Int.zero], turned into a load immediate of zero. *)
   econstructor; split.
   eapply exec_Iop with (v := Vint Int.zero); eauto.
   eapply match_succ_states; eauto. simpl; auto.
   apply eagree_update; auto.
   rewrite is_int_zero_sound by auto.
   constructor.
-+ (* preserved *)
-  exploit eval_addressing_lessdef_none. eapply add_needs_all_lessdef; eauto. eassumption.
-  intro Hnone'.
-  assert (eval_addressing tge (Vptr sp0 Ptrofs.zero) addr te ## args = None) as Hnone2'.
+** (* preserved *)
+  exploit eval_addressing_lessdef. eapply add_needs_all_lessdef; eauto. eauto.
+  intros (ta & U & V).
+  destruct (Mem.loadv chunk tm ta) eqn:Hchunk2.
+  {
+  econstructor; split.
+  try (eapply exec_Iload; eauto; eapply has_loaded_normal; eauto;
+  try (rewrite <- U; apply eval_addressing_preserved; exact symbols_preserved; fail); eauto).
+  eapply match_succ_states; eauto. simpl; auto.
+  apply eagree_update; eauto 2 with na.
+  eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto.
+  }
+  {
+  econstructor; split.
+  eapply exec_Iload. eauto. eapply has_loaded_default; eauto.
   erewrite eval_addressing_preserved with (ge1 := ge).
-  assumption.
+  intros a EVAL'; rewrite U in EVAL'; inv EVAL'. auto.
   exact symbols_preserved.
-  
-  econstructor; split.
-  eapply exec_Iload_notrap1; eauto.
   eapply match_succ_states; eauto. simpl; auto.
   apply eagree_update; eauto 2 with na.
   eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto.
-
-- (* load notrap2 *)
-  TransfInstr; UseTransfer.
-  
-  destruct (is_dead (nreg ne dst)) eqn:DEAD;
+  }
+* destruct (is_dead (nreg ne dst)) eqn:DEAD;
   [idtac|destruct (is_int_zero (nreg ne dst)) eqn:INTZERO];
   simpl in *.
-+ (* dead instruction, turned into a nop *)
+** (* dead instruction, turned into a nop *)
   econstructor; split.
   eapply exec_Inop; eauto.
   eapply match_succ_states; eauto. simpl; auto.
   apply eagree_update_dead; auto with na.
-+ (* instruction with needs = [I Int.zero], turned into a load immediate of zero. *)
+** (* instruction with needs = [I Int.zero], turned into a load immediate of zero. *)
   econstructor; split.
   eapply exec_Iop with (v := Vint Int.zero); eauto.
   eapply match_succ_states; eauto. simpl; auto.
   apply eagree_update; auto.
   rewrite is_int_zero_sound by auto.
   constructor.
-+ (* preserved *)
-  exploit eval_addressing_lessdef. eapply add_needs_all_lessdef; eauto. eauto.
-  intros (ta & U & V).
-  destruct (Mem.loadv chunk tm ta) eqn:Hchunk2.
-  {
-  econstructor; split.
-  eapply exec_Iload. eauto.
+** exploit eval_addressing_lessdef_none. eapply add_needs_all_lessdef; eauto. eassumption.
+  intro Hnone'.
+  assert (eval_addressing tge (Vptr sp0 Ptrofs.zero) addr te ## args = None) as Hnone2'.
   erewrite eval_addressing_preserved with (ge1 := ge).
-  eassumption.
+  assumption.
   exact symbols_preserved.
-  eassumption.
-  eapply match_succ_states; eauto. simpl; auto.
-  apply eagree_update; eauto 2 with na.
-  eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto.
-  }
-  {
+  
   econstructor; split.
-  eapply exec_Iload_notrap2. eauto.
-  erewrite eval_addressing_preserved with (ge1 := ge).
-  eassumption.
-  exact symbols_preserved.
-  eassumption.
+  eapply exec_Iload; eauto. eapply has_loaded_default; eauto.
+  intros a EVAL'; rewrite Hnone2' in EVAL'; inv EVAL'.
+
   eapply match_succ_states; eauto. simpl; auto.
   apply eagree_update; eauto 2 with na.
   eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto.
-  }
+
 - (* store *)
   TransfInstr; UseTransfer.
   destruct (nmem_contains nm (aaddressing (vanalyze cu f) # pc addr args)