Merge branch 'RTL_has_loaded' into kvx-work

23 files changed, 1324 insertions, 1382 deletions

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).
diff --git a/backend/Allocationproof.v b/backend/Allocationproof.v
index 15cbdcdc..114a9a1d 100644
--- a/backend/Allocationproof.v
+++ b/backend/Allocationproof.v
@@ -2082,25 +2082,73 @@ Proof.
   econstructor; eauto.
   eapply wt_exec_Iop; eauto.
 
-(* load regular TRAP *)
-- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'.
-  exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]].
-  exploit transfer_use_def_satisf; eauto. intros [X Y].
-  exploit eval_addressing_lessdef; eauto. intros [a' [F G]].
-  exploit Mem.loadv_extends; eauto. intros [v' [P Q]].
-  exploit (exec_moves mv2); eauto. intros [ls2 [A2 B2]].
-  econstructor; split.
-  eapply plus_left. econstructor; eauto.
-  eapply star_trans. eexact A1.
-  eapply star_left. econstructor. instantiate (1 := a'). rewrite <- F.
-  apply eval_addressing_preserved. exact symbols_preserved. eauto. eauto.
-  eapply star_right. eexact A2. constructor.
-  eauto. eauto. eauto. traceEq.
-  exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]].
-  econstructor; eauto.
+(* load regular *)
+- inv H0.
+  + generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ _ WTI LOAD WTRS). intros WTRS'.
+    exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]].
+    exploit transfer_use_def_satisf; eauto. intros [X Y].
+    exploit eval_addressing_lessdef; eauto. intros [a' [F G]].
+    exploit Mem.loadv_extends; eauto. intros [v' [P Q]].
+    exploit (exec_moves mv2); eauto. intros [ls2 [A2 B2]].
+    econstructor; split.
+    eapply plus_left. econstructor; eauto.
+    eapply star_trans. eexact A1.
+    eapply star_left. econstructor. instantiate (1 := a'). rewrite <- F.
+    apply eval_addressing_preserved. exact symbols_preserved. eauto. eauto.
+    eapply star_right. eexact A2. constructor.
+    eauto. eauto. eauto. traceEq.
+    exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]].
+    econstructor; eauto.
+  + destruct (eval_addressing) eqn:EVAL in LOAD.
+    * specialize (LOAD v).
+      generalize (wt_exec_Iload_notrap _ _ _ _ _ _ _ _ WTI WTRS).
+      intro WTRS'.
+      exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]].
+      exploit transfer_use_def_satisf; eauto. intros [X Y].
+      exploit eval_addressing_lessdef; eauto. intros [a' [F G]].
+      destruct (Mem.loadv chunk m' a') as [v' |] eqn:Hload.
+      { exploit (exec_moves mv2 env (rs # dst <- Vundef)); eauto.  intros [ls2 [A2 B2]].
+          econstructor; split.
+      eapply plus_left. econstructor; eauto.
+      eapply star_trans. eexact A1.
+      eapply star_left. econstructor. instantiate (1 := a'). rewrite <- F.
+      apply eval_addressing_preserved. exact symbols_preserved. eauto. eauto.
+      eapply star_right. eexact A2. constructor.
+      eauto. eauto. eauto. traceEq.
+      exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]].
+      econstructor; eauto.
+      }
+      { exploit (exec_moves mv2 env (rs # dst <- Vundef)); eauto.  intros [ls2 [A2 B2]].
+      econstructor; split.
+      eapply plus_left. econstructor; eauto.
+      eapply star_trans. eexact A1.
+      eapply star_left. eapply exec_Lload_notrap2. rewrite <- F.
+      apply eval_addressing_preserved. exact symbols_preserved. assumption.
+      eauto.
+      eapply star_right. eexact A2. constructor.
+      eauto. eauto. eauto. traceEq.
+      exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]].
+      econstructor; eauto.
+      }
+    * generalize (wt_exec_Iload_notrap _ _ _ _ _ _ _ _ WTI WTRS).
+      intro WTRS'.
+      exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]].
+      exploit transfer_use_def_satisf; eauto. intros [X Y].
+      exploit eval_addressing_lessdef_none; eauto. intro Haddr.
+      exploit (exec_moves mv2); eauto.  intros [ls2 [A2 B2]].
+      econstructor; split.
+      eapply plus_left. econstructor; eauto.
+      eapply star_trans. eexact A1.
+      eapply star_left. eapply exec_Lload_notrap1. rewrite <- Haddr.
+      apply eval_addressing_preserved. exact symbols_preserved. eauto.
+      
+      eapply star_right. eexact A2. constructor.
+      eauto. eauto. eauto. traceEq.
+      exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]].
+      econstructor; eauto.
 
 (* load pair *)
-- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'.
+- inv H0. generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ _ WTI LOAD WTRS). intros WTRS'.
   exploit loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V1 & V2).
   set (v2' := if Archi.big_endian then v2 else v1) in *.
   set (v1' := if Archi.big_endian then v1 else v2) in *.
@@ -2155,7 +2203,7 @@ Proof.
   econstructor; eauto.
 
 (* load first word of a pair *)
-- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'.
+- inv H0. generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ _ WTI LOAD WTRS). intros WTRS'.
   exploit loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V1 & V2).
   set (v2' := if Archi.big_endian then v2 else v1) in *.
   set (v1' := if Archi.big_endian then v1 else v2) in *.
@@ -2185,7 +2233,7 @@ Proof.
   econstructor; eauto.
 
 (* load second word of a pair *)
-- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'.
+- inv H0. generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ _ WTI LOAD WTRS). intros WTRS'.
   exploit loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V1 & V2).
   set (v2' := if Archi.big_endian then v2 else v1) in *.
   set (v1' := if Archi.big_endian then v1 else v2) in *.
@@ -2226,82 +2274,10 @@ Proof.
   exploit satisf_successors. eauto. eauto. simpl; eauto. eauto.
   eapply reg_unconstrained_satisf; eauto.
   intros [enext [U V]].
-  econstructor; eauto.
-  eapply wt_exec_Iload; eauto.
-
-- (* load notrap1 *)
-  generalize (wt_exec_Iload_notrap _ _ _ _ _ _ _ _ WTI WTRS).
-  intro WTRS'.
-  exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]].
-  exploit transfer_use_def_satisf; eauto. intros [X Y].
-  exploit eval_addressing_lessdef_none; eauto. intro Haddr.
-  exploit (exec_moves mv2); eauto.  intros [ls2 [A2 B2]].
-  econstructor; split.
-  eapply plus_left. econstructor; eauto.
-  eapply star_trans. eexact A1.
-  eapply star_left. eapply exec_Lload_notrap1. rewrite <- Haddr.
-  apply eval_addressing_preserved. exact symbols_preserved. eauto.
-  
-  eapply star_right. eexact A2. constructor.
-  eauto. eauto. eauto. traceEq.
-  exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]].
-  econstructor; eauto.
-
-(* load notrap1 dead *)
-- exploit exec_moves; eauto. intros [ls1 [X Y]].
-  econstructor; split.
-  eapply plus_left. econstructor; eauto.
-  eapply star_right. eexact X. econstructor; eauto.
-  eauto. traceEq.
-  exploit satisf_successors. eauto. eauto. simpl; eauto. eauto.
-  eapply reg_unconstrained_satisf; eauto.
-  intros [enext [U V]].
-  econstructor; eauto.
-  eapply wt_exec_Iload_notrap; eauto.
+  econstructor; eauto. inv H0.
+  + eapply wt_exec_Iload; eauto.
+  + eapply wt_exec_Iload_notrap; eauto.
 
-(* load regular notrap2 *)
-- generalize (wt_exec_Iload_notrap _ _ _ _ _ _ _ _ WTI WTRS).
-  intro WTRS'.
-  exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]].
-  exploit transfer_use_def_satisf; eauto. intros [X Y].
-  exploit eval_addressing_lessdef; eauto. intros [a' [F G]].
-  destruct (Mem.loadv chunk m' a') as [v' |] eqn:Hload.
-  { exploit (exec_moves mv2 env (rs # dst <- Vundef)); eauto.  intros [ls2 [A2 B2]].
-      econstructor; split.
-  eapply plus_left. econstructor; eauto.
-  eapply star_trans. eexact A1.
-  eapply star_left. econstructor. instantiate (1 := a'). rewrite <- F.
-  apply eval_addressing_preserved. exact symbols_preserved. eauto. eauto.
-  eapply star_right. eexact A2. constructor.
-  eauto. eauto. eauto. traceEq.
-  exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]].
-  econstructor; eauto.
-  }
-  { exploit (exec_moves mv2 env (rs # dst <- Vundef)); eauto.  intros [ls2 [A2 B2]].
-  econstructor; split.
-  eapply plus_left. econstructor; eauto.
-  eapply star_trans. eexact A1.
-  eapply star_left. eapply exec_Lload_notrap2. rewrite <- F.
-  apply eval_addressing_preserved. exact symbols_preserved. assumption.
-  eauto.
-  eapply star_right. eexact A2. constructor.
-  eauto. eauto. eauto. traceEq.
-  exploit satisf_successors; eauto. simpl; eauto. intros [enext [U V]].
-  econstructor; eauto.
-  }
-  
-- (* load notrap2 dead *)
-  exploit exec_moves; eauto. intros [ls1 [X Y]].
-  econstructor; split.
-  eapply plus_left. econstructor; eauto.
-  eapply star_right. eexact X. econstructor; eauto.
-  eauto. traceEq.
-  exploit satisf_successors. eauto. eauto. simpl; eauto. eauto.
-  eapply reg_unconstrained_satisf; eauto.
-  intros [enext [U V]].
-  econstructor; eauto.
-  eapply wt_exec_Iload_notrap; eauto.
-  
 (* store *)
 - exploit exec_moves; eauto. intros [ls1 [X Y]].
   exploit add_equations_lessdef; eauto. intros LD. simpl in LD. inv LD.
diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
index 252240c9..08891e1d 100644
--- a/backend/CSE2proof.v
+++ b/backend/CSE2proof.v
@@ -1314,105 +1314,62 @@ Proof.
   }
     
 (* load *)
-- unfold transf_instr in *.
-  destruct find_load_in_fmap eqn:FIND_LOAD.
-  {
-    unfold find_load_in_fmap, fmap_sem', fmap_sem in *.
-    destruct (forward_map f) as [map |] eqn:MAP.
-    2: discriminate.
-    change (@PMap.get (option RELATION.t) pc map) with (map # pc) in *. 
-    destruct (map # pc) as [mpc | ] eqn:MPC.
-    2: discriminate.
-    econstructor; split.
+- unfold transf_instr in *. inv H0.
+  + destruct find_load_in_fmap eqn:FIND_LOAD.
     {
-      eapply exec_Iop with (v := v); eauto.
-      simpl.
-      rewrite <- subst_args_ok with (genv := ge) (f := f) (pc := pc) (sp := sp) (m := m) in H0.
+      unfold find_load_in_fmap, fmap_sem', fmap_sem in *.
+      destruct (forward_map f) as [map |] eqn:MAP.
+      2: discriminate.
+      change (@PMap.get (option RELATION.t) pc map) with (map # pc) in *. 
+      destruct (map # pc) as [mpc | ] eqn:MPC.
+      2: discriminate.
+      econstructor; split.
       {
-        f_equal.
-        symmetry.
-        rewrite MAP in H0.
-        eapply find_load_sound' with (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs).
-        all: eassumption.
+        eapply exec_Iop with (v := v); eauto.
+        simpl.
+        rewrite <- subst_args_ok with (genv := ge) (f := f) (pc := pc) (sp := sp) (m := m) in EVAL.
+        {
+          f_equal.
+          symmetry.
+          rewrite MAP in EVAL.
+          eapply find_load_sound' with (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs).
+          all: eassumption.
+        }
+        unfold fmap_sem. rewrite MAP. rewrite MPC. assumption.
       }
-      unfold fmap_sem. rewrite MAP. rewrite MPC. assumption.
-    }
-    constructor; eauto.
-    unfold fmap_sem', fmap_sem in *.
-    rewrite MAP.
-    apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)).
-    {
-      replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
+      constructor; eauto.
+      unfold fmap_sem', fmap_sem in *.
+      rewrite MAP.
+      apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)).
       {
-        eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
-        2: apply apply_instr'_bot.
-        simpl. tauto.
+        replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
+        {
+          eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
+          2: apply apply_instr'_bot.
+          simpl. tauto.
+        }
+        unfold apply_instr'.
+        rewrite H.
+        rewrite MPC.
+        simpl.
+        reflexivity.
       }
-      unfold apply_instr'.
-      rewrite H.
-      rewrite MPC.
-      simpl.
-      reflexivity.
-    }
-    unfold sem_rel_b', sem_rel_b.
-    apply load_sound with (a := a); auto.
-  }
-  {  
-  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.
-  rewrite (subst_args_ok' sp m); assumption.
-  constructor; auto.
-
-  simpl in *.
-  unfold fmap_sem', fmap_sem in *.
-  destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
-  destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
-  apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)).
-  {
-    replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
-    {
-      eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
-      2: apply apply_instr'_bot.
-      simpl. tauto.
+      unfold sem_rel_b', sem_rel_b.
+      apply load_sound with (a := a); auto.
     }
-    unfold apply_instr'.
-    rewrite H.
-    rewrite MPC.
-    simpl.
-    reflexivity.
-  }
-  apply load_sound with (a := a); assumption.
-  }
-  
-- (* load notrap1 *)
-  unfold transf_instr in *.
-  destruct find_load_in_fmap eqn:FIND_LOAD.
-  {
-    unfold find_load_in_fmap, fmap_sem', fmap_sem in *.
-    destruct (forward_map f) as [map |] eqn:MAP.
-    2: discriminate.
-    change (@PMap.get (option RELATION.t) pc map) with (map # pc) in *. 
-    destruct (map # pc) as [mpc | ] eqn:MPC.
-    2: discriminate.
+    {  
     econstructor; split.
-    {
-      eapply exec_Iop with (v := Vundef); eauto.
-      simpl.
-      rewrite <- subst_args_ok with (genv := ge) (f := f) (pc := pc) (sp := sp) (m := m) in H0.
-      {
-        f_equal.
-        rewrite MAP in H0.
-        eapply find_load_notrap1_sound' with (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs).
-        all: eassumption.
-      }
-      unfold fmap_sem. rewrite MAP. rewrite MPC. assumption.
-    }
-    constructor; eauto.
+    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.
+    rewrite (subst_args_ok' sp m); assumption.
+    constructor; auto.
+
+    simpl in *.
     unfold fmap_sem', fmap_sem in *.
-    rewrite MAP.
+    destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
+    destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
     apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)).
     {
       replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
@@ -1427,111 +1384,154 @@ Proof.
       simpl.
       reflexivity.
     }
-    unfold sem_rel_b', sem_rel_b.
-    apply load_notrap1_sound; auto.
-  }
-  {  
-  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.
-  rewrite (subst_args_ok' sp m); assumption.
-  constructor; auto.
-
-  simpl in *.
-  unfold fmap_sem', fmap_sem in *.
-  destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
-  destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
-  apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)).
-  {
-    replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
-    {
-      eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
-      2: apply apply_instr'_bot.
-      simpl. tauto.
+    apply load_sound with (a := a); assumption.
     }
-    unfold apply_instr'.
-    rewrite H.
-    rewrite MPC.
-    simpl.
-    reflexivity.
-  }
-  apply load_notrap1_sound; assumption.
-  }
-  
-(* load notrap2 *)
-- unfold transf_instr in *.
-  destruct find_load_in_fmap eqn:FIND_LOAD.
-  {
-    unfold find_load_in_fmap, fmap_sem', fmap_sem in *.
-    destruct (forward_map f) as [map |] eqn:MAP.
-    2: discriminate.
-    change (@PMap.get (option RELATION.t) pc map) with (map # pc) in *. 
-    destruct (map # pc) as [mpc | ] eqn:MPC.
-    2: discriminate.
-    econstructor; split.
-    {
-      eapply exec_Iop with (v := Vundef); eauto.
-      simpl.
-      rewrite <- subst_args_ok with (genv := ge) (f := f) (pc := pc) (sp := sp) (m := m) in H0.
+    
+  + destruct (eval_addressing) eqn:EVAL in LOAD.
+    * specialize (LOAD v).
+      destruct find_load_in_fmap eqn:FIND_LOAD.
+        {
+          unfold find_load_in_fmap, fmap_sem', fmap_sem in *.
+          destruct (forward_map f) as [map |] eqn:MAP.
+          2: discriminate.
+          change (@PMap.get (option RELATION.t) pc map) with (map # pc) in *. 
+          destruct (map # pc) as [mpc | ] eqn:MPC.
+          2: discriminate.
+          econstructor; split.
+          {
+            eapply exec_Iop with (v := Vundef); eauto.
+            simpl.
+            rewrite <- subst_args_ok with (genv := ge) (f := f) (pc := pc) (sp := sp) (m := m) in EVAL.
+            {
+              f_equal.
+              rewrite MAP in EVAL.
+              eapply find_load_notrap2_sound' with (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs).
+              all: try eassumption. apply LOAD; auto.
+            }
+            unfold fmap_sem. rewrite MAP. rewrite MPC. assumption.
+          }
+          constructor; eauto.
+          unfold fmap_sem', fmap_sem in *.
+          rewrite MAP.
+          apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)).
+          {
+            replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
+            {
+              eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
+              2: apply apply_instr'_bot.
+              simpl. tauto.
+            }
+            unfold apply_instr'.
+            rewrite H.
+            rewrite MPC.
+            simpl.
+            reflexivity.
+          }
+          unfold sem_rel_b', sem_rel_b.
+          apply load_notrap2_sound with (a := v); auto.
+        }
+        {  
+        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.
+        rewrite (subst_args_ok' sp m).
+        intros a EVAL'; rewrite H0 in EVAL'; inv EVAL'; auto.
+        assumption.
+        constructor; auto.
+
+        simpl in *.
+        unfold fmap_sem', fmap_sem in *.
+        destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
+        destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
+        apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)).
+        {
+          replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
+          {
+            eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
+            2: apply apply_instr'_bot.
+            simpl. tauto.
+          }
+          unfold apply_instr'.
+          rewrite H.
+          rewrite MPC.
+          simpl.
+          reflexivity.
+        }
+        apply load_notrap2_sound with (a := v); auto.
+        }
+        
+    * destruct find_load_in_fmap eqn:FIND_LOAD.
       {
-        f_equal.
-        rewrite MAP in H0.
-        eapply find_load_notrap2_sound' with (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs).
-        all: try eassumption.
+        unfold find_load_in_fmap, fmap_sem', fmap_sem in *.
+        destruct (forward_map f) as [map |] eqn:MAP.
+        2: discriminate.
+        change (@PMap.get (option RELATION.t) pc map) with (map # pc) in *. 
+        destruct (map # pc) as [mpc | ] eqn:MPC.
+        2: discriminate.
+        econstructor; split.
+        {
+          eapply exec_Iop with (v := Vundef); eauto.
+          simpl.
+          rewrite <- subst_args_ok with (genv := ge) (f := f) (pc := pc) (sp := sp) (m := m) in EVAL.
+          {
+            f_equal.
+            rewrite MAP in EVAL.
+            eapply find_load_notrap1_sound' with (genv := ge) (sp := sp) (addr := addr) (args := subst_args (Some map) pc args) (rel := mpc) (src := r) (rs := rs).
+            all: eassumption.
+          }
+          unfold fmap_sem. rewrite MAP. rewrite MPC. assumption.
+        }
+        constructor; eauto.
+        unfold fmap_sem', fmap_sem in *.
+        rewrite MAP.
+        apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)).
+        {
+          replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
+          {
+            eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
+            2: apply apply_instr'_bot.
+            simpl. tauto.
+          }
+          unfold apply_instr'.
+          rewrite H.
+          rewrite MPC.
+          simpl.
+          reflexivity.
+        }
+        unfold sem_rel_b', sem_rel_b.
+        apply load_notrap1_sound; auto.
       }
-      unfold fmap_sem. rewrite MAP. rewrite MPC. assumption.
-    }
-    constructor; eauto.
-    unfold fmap_sem', fmap_sem in *.
-    rewrite MAP.
-    apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)).
-    {
-      replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
+      {  
+      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.
+      rewrite (subst_args_ok' sp m); eauto. congruence.
+      constructor; auto.
+
+      simpl in *.
+      unfold fmap_sem', fmap_sem in *.
+      destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
+      destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
+      apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)).
       {
-        eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
-        2: apply apply_instr'_bot.
-        simpl. tauto.
+        replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
+        {
+          eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
+          2: apply apply_instr'_bot.
+          simpl. tauto.
+        }
+        unfold apply_instr'.
+        rewrite H.
+        rewrite MPC.
+        simpl.
+        reflexivity.
+      }
+      apply load_notrap1_sound; assumption.
       }
-      unfold apply_instr'.
-      rewrite H.
-      rewrite MPC.
-      simpl.
-      reflexivity.
-    }
-    unfold sem_rel_b', sem_rel_b.
-    apply load_notrap2_sound with (a := a); auto.
-  }
-  {  
-  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.
-  rewrite (subst_args_ok' sp m); assumption.
-  constructor; auto.
-
-  simpl in *.
-  unfold fmap_sem', fmap_sem in *.
-  destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
-  destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
-  apply sem_rel_b_ge with (rb2 := Some (load chunk addr dst args mpc)).
-  {
-    replace (Some (load chunk addr dst args mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
-    {
-      eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
-      2: apply apply_instr'_bot.
-      simpl. tauto.
-    }
-    unfold apply_instr'.
-    rewrite H.
-    rewrite MPC.
-    simpl.
-    reflexivity.
-  }
-  apply load_notrap2_sound with (a := a); assumption.
-  }
   
 - (* store *)
   econstructor. split.
diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v
index a601d5d5..86c2c8a7 100644
--- a/backend/CSE3proof.v
+++ b/backend/CSE3proof.v
@@ -582,48 +582,51 @@ Proof.
       apply oper_sound; unfold ctx; eauto with cse3.
       (* END INVARIANT *)
   - (* Iload *)
-    exists (State ts tf sp pc' (rs # dst <- v) m). split.
-    + pose (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload trap chunk addr args dst pc')) as instr'.
-      assert (instr' = (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload trap chunk addr args dst pc'))) by reflexivity.
-      unfold param_transf_instr, find_load_in_fmap in instr'.
-      destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC.
-      pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SLoad chunk addr)
-                (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND.
-      * destruct rhs_find eqn:FIND.
-        ** apply exec_Iop with (op := Omove) (args := r :: nil).
-           TR_AT.
-           subst instr'.
-           congruence.
-           simpl.
-           specialize FIND_SOUND with (src := r) (rs := rs) (m := m).
-           simpl in FIND_SOUND.
-           rewrite subst_args_ok with (sp:=sp) (m:=m) in FIND_SOUND.
-           rewrite H0 in FIND_SOUND. (* ADDR *)
-           rewrite H1 in FIND_SOUND. (* LOAD *)
-           rewrite FIND_SOUND; auto.
-           unfold fmap_sem.
-           change ((fst (preanalysis tenv f)) # pc)
-                  with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))).
-           rewrite INV_PC.
-           assumption.
-        ** apply exec_Iload with (trap := trap) (chunk := chunk) (a := a) (addr := addr) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial.
-           TR_AT.
-           { subst instr'.
-           congruence. }
-           rewrite subst_args_ok with (sp:=sp) (m:=m).
-           {
-           rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved.
-           assumption.
-           }
-           unfold fmap_sem.
-           change ((fst (preanalysis tenv f)) # pc)
-                  with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))).
-           rewrite INV_PC.
-           assumption.
-      * apply exec_Iload with (chunk := chunk) (trap := trap) (addr := addr) (a := a) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial.
+    inv H0.
+    + exists (State ts tf sp pc' (rs # dst <- v) m). split.
+      * pose (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload trap chunk addr args dst pc')) as instr'.
+        assert (instr' = (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload trap chunk addr args dst pc'))) by reflexivity.
+        unfold param_transf_instr, find_load_in_fmap in instr'.
+        destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC.
+        pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SLoad chunk addr)
+        (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND.
+        -- destruct rhs_find eqn:FIND.
+           ** apply exec_Iop with (op := Omove) (args := r :: nil).
+              TR_AT.
+              subst instr'.
+              congruence.
+              simpl.
+              specialize FIND_SOUND with (src := r) (rs := rs) (m := m).
+              simpl in FIND_SOUND.
+              rewrite subst_args_ok with (sp:=sp) (m:=m) in FIND_SOUND.
+              rewrite EVAL in FIND_SOUND. (* ADDR *)
+              rewrite LOAD in FIND_SOUND. (* LOAD *)
+              rewrite FIND_SOUND; auto.
+              unfold fmap_sem.
+              change ((fst (preanalysis tenv f)) # pc)
+                     with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))).
+              rewrite INV_PC.
+              assumption.
+           ** apply exec_Iload with (trap := trap) (chunk := chunk) (addr := addr) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial.
+              TR_AT.
+              { subst instr'.
+              congruence. }
+              eapply has_loaded_normal; eauto.
+              rewrite subst_args_ok with (sp:=sp) (m:=m).
+              {
+              rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved.
+              assumption.
+              }
+              unfold fmap_sem.
+              change ((fst (preanalysis tenv f)) # pc)
+                     with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))).
+              rewrite INV_PC.
+              assumption.
+        -- apply exec_Iload with (chunk := chunk) (trap := trap) (addr := addr) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial.
            TR_AT.
            { subst instr'.
            congruence. }
+           eapply has_loaded_normal; eauto.
            rewrite subst_args_ok with (sp:=sp) (m:=m).
            {
            rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved.
@@ -634,183 +637,187 @@ Proof.
                   with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))).
            rewrite INV_PC.
            assumption.
-    + econstructor; eauto.
-      * eapply wt_exec_Iload with (f:=f); try eassumption.
+      * econstructor; eauto.
+        -- eapply wt_exec_Iload with (f:=f); try eassumption.
         eauto with wt.
-      *         (* BEGIN INVARIANT *)
-        fold ctx. fold invs.
-      assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto).
-      unfold check_inductiveness in IND.
-      rewrite andb_true_iff in IND.
-      destruct IND as [IND_entry IND_step].
-      rewrite PTree_Properties.for_all_correct in IND_step.
-      pose proof (IND_step pc _ H) as IND_step_me.
-      clear IND_entry IND_step.
-      destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL.
-      2: contradiction.
-      cbn in IND_step_me.
-      destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *.
-      2: discriminate.
-      rewrite andb_true_iff in IND_step_me.
-      destruct IND_step_me.
-      rewrite rel_leb_correct in *.
-      eapply rel_ge.
-      eassumption.
-      apply oper_sound; unfold ctx; eauto with cse3.
-      (* END INVARIANT *)
-        
-  - (* Iload notrap1 *)
-    exists (State ts tf sp pc' (rs # dst <- Vundef) m). split.
-    + pose (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc')) as instr'.
-      assert (instr' = (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc'))) by reflexivity.
-      unfold param_transf_instr, find_load_in_fmap in instr'.
-      destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC.
-      pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SLoad chunk addr)
-                (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND.
-      * destruct rhs_find eqn:FIND.
-        ** apply exec_Iop with (op := Omove) (args := r :: nil).
-           TR_AT.
-           subst instr'.
-           congruence.
-           simpl.
-           specialize FIND_SOUND with (src := r) (rs := rs) (m := m).
-           simpl in FIND_SOUND.
-           rewrite subst_args_ok with (sp:=sp) (m:=m) in FIND_SOUND.
-           rewrite H0 in FIND_SOUND. (* ADDR *)
-           rewrite FIND_SOUND; auto.
-           unfold fmap_sem.
-           change ((fst (preanalysis tenv f)) # pc)
-                  with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))).
-           rewrite INV_PC.
-           assumption.
-        ** apply exec_Iload_notrap1 with (chunk := chunk) (addr := addr) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial.
-           TR_AT.
-           { subst instr'.
-           congruence. }
-           rewrite subst_args_ok with (sp:=sp) (m:=m).
-           {
-           rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved.
-           assumption.
-           }
-           unfold fmap_sem.
-           change ((fst (preanalysis tenv f)) # pc)
-                  with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))).
-           rewrite INV_PC.
-           assumption.
-      * apply exec_Iload_notrap1 with (chunk := chunk) (addr := addr) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial.
-           TR_AT.
-           { subst instr'.
-           congruence. }
-           rewrite subst_args_ok with (sp:=sp) (m:=m).
-           {
-           rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved.
-           assumption.
-           }
-           unfold fmap_sem.
-           change ((fst (preanalysis tenv f)) # pc)
-                  with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))).
-           rewrite INV_PC.
-           assumption.
-    + econstructor; eauto.
-      * apply wt_undef; assumption.
-      *          (* BEGIN INVARIANT *)
-        fold ctx. fold invs.
-      assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto).
-      unfold check_inductiveness in IND.
-      rewrite andb_true_iff in IND.
-      destruct IND as [IND_entry IND_step].
-      rewrite PTree_Properties.for_all_correct in IND_step.
-      pose proof (IND_step pc _ H) as IND_step_me.
-      clear IND_entry IND_step.
-      destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL.
-      2: contradiction.
-      cbn in IND_step_me.
-      destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *.
-      2: discriminate.
-      rewrite andb_true_iff in IND_step_me.
-      destruct IND_step_me.
-      rewrite rel_leb_correct in *.
-      eapply rel_ge.
-      eassumption.
-      apply oper_sound; unfold ctx; eauto with cse3.
-      (* END INVARIANT *)
+        -- (* BEGIN INVARIANT *)
+           fold ctx. fold invs.
+           assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto).
+           unfold check_inductiveness in IND.
+           rewrite andb_true_iff in IND.
+           destruct IND as [IND_entry IND_step].
+           rewrite PTree_Properties.for_all_correct in IND_step.
+           pose proof (IND_step pc _ H) as IND_step_me.
+           clear IND_entry IND_step.
+           destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL.
+           2: contradiction.
+           cbn in IND_step_me.
+           destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *.
+           2: discriminate.
+           rewrite andb_true_iff in IND_step_me.
+           destruct IND_step_me.
+           rewrite rel_leb_correct in *.
+           eapply rel_ge.
+           eassumption.
+           apply oper_sound; unfold ctx; eauto with cse3.
+           (* END INVARIANT *)
+              
+    + destruct (eval_addressing) eqn:EVAL in LOAD.
+      * specialize (LOAD v).
+        exists (State ts tf sp pc' (rs # dst <- Vundef) m). split.
+        -- pose (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc')) as instr'.
+           assert (instr' = (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc'))) by reflexivity.
+           unfold param_transf_instr, find_load_in_fmap in instr'.
+           destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC.
+           pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SLoad chunk addr)
+           (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND.
+           ++ destruct rhs_find eqn:FIND.
+              ** apply exec_Iop with (op := Omove) (args := r :: nil).
+                 TR_AT.
+                 subst instr'.
+                 congruence.
+                 simpl.
+                 specialize FIND_SOUND with (src := r) (rs := rs) (m := m).
+                 simpl in FIND_SOUND.
+                 rewrite subst_args_ok with (sp:=sp) (m:=m) in FIND_SOUND.
+                 rewrite EVAL in FIND_SOUND. (* ADDR *)
+                 rewrite LOAD in FIND_SOUND; auto. (* LOAD *)
+                 rewrite FIND_SOUND; auto.
+                 unfold fmap_sem.
+                 change ((fst (preanalysis tenv f)) # pc)
+                        with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))).
+                 rewrite INV_PC.
+                 assumption.
+              ** apply exec_Iload with (trap := NOTRAP) (chunk := chunk) (addr := addr) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial.
+                 TR_AT.
+                 { subst instr'.
+                 congruence. }
+                 eapply has_loaded_default; eauto.
+                 rewrite subst_args_ok with (sp:=sp) (m:=m).
+                 {
+                 rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved.
+                 intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'. apply LOAD; auto.
+                 }
+                 unfold fmap_sem.
+                 change ((fst (preanalysis tenv f)) # pc)
+                        with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))).
+                 rewrite INV_PC.
+                 assumption.
+           ++ apply exec_Iload with (trap := NOTRAP) (chunk := chunk) (addr := addr) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial.
+                 TR_AT.
+              { subst instr'.
+              congruence. }
+              eapply has_loaded_default; eauto.
+              rewrite subst_args_ok with (sp:=sp) (m:=m).
+              {
+              rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved.
+              intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'. apply LOAD; auto.
+              }
+              unfold fmap_sem.
+              change ((fst (preanalysis tenv f)) # pc)
+                     with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))).
+              rewrite INV_PC.
+              assumption.
+        -- econstructor; eauto.
+           ++ apply wt_undef; assumption.
+           ++ (* BEGIN INVARIANT *)
+              fold ctx. fold invs.
+              assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto).
+              unfold check_inductiveness in IND.
+              rewrite andb_true_iff in IND.
+              destruct IND as [IND_entry IND_step].
+              rewrite PTree_Properties.for_all_correct in IND_step.
+              pose proof (IND_step pc _ H) as IND_step_me.
+              clear IND_entry IND_step.
+              destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL.
+              2: contradiction.
+              cbn in IND_step_me.
+              destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *.
+              2: discriminate.
+              rewrite andb_true_iff in IND_step_me.
+              destruct IND_step_me.
+              rewrite rel_leb_correct in *.
+              eapply rel_ge.
+              eassumption.
+              apply oper_sound; unfold ctx; eauto with cse3.
+              (* END INVARIANT *)
         
-  - (* Iload notrap2 *)
-    exists (State ts tf sp pc' (rs # dst <- Vundef) m). split.
-    + pose (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc')) as instr'.
-      assert (instr' = (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc'))) by reflexivity.
-      unfold param_transf_instr, find_load_in_fmap in instr'.
-      destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC.
-      pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SLoad chunk addr)
-                (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND.
-      * destruct rhs_find eqn:FIND.
-        ** apply exec_Iop with (op := Omove) (args := r :: nil).
-           TR_AT.
-           subst instr'.
-           congruence.
-           simpl.
-           specialize FIND_SOUND with (src := r) (rs := rs) (m := m).
-           simpl in FIND_SOUND.
-           rewrite subst_args_ok with (sp:=sp) (m:=m) in FIND_SOUND.
-           rewrite H0 in FIND_SOUND. (* ADDR *)
-           rewrite H1 in FIND_SOUND. (* LOAD *)
-           rewrite FIND_SOUND; auto.
-           unfold fmap_sem.
-           change ((fst (preanalysis tenv f)) # pc)
-                  with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))).
-           rewrite INV_PC.
-           assumption.
-        ** apply exec_Iload_notrap2 with (chunk := chunk) (a := a) (addr := addr) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial.
-           TR_AT.
-           { subst instr'.
-           congruence. }
-           rewrite subst_args_ok with (sp:=sp) (m:=m).
-           {
-           rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved.
-           assumption.
-           }
-           unfold fmap_sem.
-           change ((fst (preanalysis tenv f)) # pc)
-                  with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))).
-           rewrite INV_PC.
-           assumption.
-      * apply exec_Iload_notrap2 with (chunk := chunk) (addr := addr) (a := a) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial.
-           TR_AT.
-           { subst instr'.
-           congruence. }
-           rewrite subst_args_ok with (sp:=sp) (m:=m).
-           {
-           rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved.
-           assumption.
-           }
-           unfold fmap_sem.
-           change ((fst (preanalysis tenv f)) # pc)
-                  with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))).
-           rewrite INV_PC.
-           assumption.
-    + econstructor; eauto.
-      * apply wt_undef; assumption.
-      *  (* BEGIN INVARIANT *)
-        fold ctx. fold invs.
-      assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto).
-      unfold check_inductiveness in IND.
-      rewrite andb_true_iff in IND.
-      destruct IND as [IND_entry IND_step].
-      rewrite PTree_Properties.for_all_correct in IND_step.
-      pose proof (IND_step pc _ H) as IND_step_me.
-      clear IND_entry IND_step.
-      destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL.
-      2: contradiction.
-      cbn in IND_step_me.
-      destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *.
-      2: discriminate.
-      rewrite andb_true_iff in IND_step_me.
-      destruct IND_step_me.
-      rewrite rel_leb_correct in *.
-      eapply rel_ge.
-      eassumption.
-      apply oper_sound; unfold ctx; eauto with cse3.
-      (* END INVARIANT *)
+      * exists (State ts tf sp pc' (rs # dst <- Vundef) m). split.
+        -- pose (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc')) as instr'.
+           assert (instr' = (param_transf_instr (ctx:=(context_from_hints (snd (preanalysis tenv f)))) params (fst (preanalysis tenv f)) pc (Iload NOTRAP chunk addr args dst pc'))) by reflexivity.
+           unfold param_transf_instr, find_load_in_fmap in instr'.
+           destruct (@PMap.get (option RELATION.t) pc) eqn:INV_PC.
+           pose proof (rhs_find_sound (sp:=sp) (genv:=ge) (ctx:=(context_from_hints (snd (preanalysis tenv f)))) pc (SLoad chunk addr)
+           (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args) t) as FIND_SOUND.
+           ++ destruct rhs_find eqn:FIND.
+              ** apply exec_Iop with (op := Omove) (args := r :: nil).
+                 TR_AT.
+                 subst instr'.
+                 congruence.
+                 simpl.
+                 specialize FIND_SOUND with (src := r) (rs := rs) (m := m).
+                 simpl in FIND_SOUND.
+                 rewrite subst_args_ok with (sp:=sp) (m:=m) in FIND_SOUND.
+                 rewrite EVAL in FIND_SOUND. (* ADDR *)
+                 rewrite FIND_SOUND; auto.
+                 unfold fmap_sem.
+                 change ((fst (preanalysis tenv f)) # pc)
+                        with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))).
+                 rewrite INV_PC.
+                 assumption.
+              ** apply exec_Iload with (trap := NOTRAP) (chunk := chunk) (addr := addr) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial.
+                 TR_AT.
+                 { subst instr'.
+                 congruence. }
+                 eapply has_loaded_default; eauto.
+                 rewrite subst_args_ok with (sp:=sp) (m:=m).
+                 {
+                 rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved.
+                 intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'.
+                 }
+                 unfold fmap_sem.
+                 change ((fst (preanalysis tenv f)) # pc)
+                        with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))).
+                 rewrite INV_PC.
+                 assumption.
+           ++ apply exec_Iload with (trap := NOTRAP) (chunk := chunk) (addr := addr) (args := (subst_args (ctx:=(context_from_hints (snd (preanalysis tenv f)))) (fst (preanalysis tenv f)) pc args)); trivial.
+              TR_AT.
+              { subst instr'.
+              congruence. }
+              eapply has_loaded_default; eauto.
+              rewrite subst_args_ok with (sp:=sp) (m:=m).
+              {
+              rewrite eval_addressing_preserved with (ge1:=ge) by exact symbols_preserved.
+              intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'.
+              }
+              unfold fmap_sem.
+              change ((fst (preanalysis tenv f)) # pc)
+                     with (@PMap.get (option RELATION.t) pc (@fst invariants analysis_hints (preanalysis tenv f))).
+              rewrite INV_PC.
+              assumption.
+        -- econstructor; eauto.
+           ++ apply wt_undef; assumption.
+           ++ (* BEGIN INVARIANT *)
+              fold ctx. fold invs.
+              assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto).
+              unfold check_inductiveness in IND.
+              rewrite andb_true_iff in IND.
+              destruct IND as [IND_entry IND_step].
+              rewrite PTree_Properties.for_all_correct in IND_step.
+              pose proof (IND_step pc _ H) as IND_step_me.
+              clear IND_entry IND_step.
+              destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL.
+              2: contradiction.
+              cbn in IND_step_me.
+              destruct (invs # pc') as [inv_pc' | ] eqn:INV_pc'; cbn in *.
+              2: discriminate.
+              rewrite andb_true_iff in IND_step_me.
+              destruct IND_step_me.
+              rewrite rel_leb_correct in *.
+              eapply rel_ge.
+              eassumption.
+              apply oper_sound; unfold ctx; eauto with cse3.
+              (* END INVARIANT *)
 
   - (* Istore *)
     exists (State ts tf sp pc' rs m'). split.
diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index 556b44b3..72b52375 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -1098,135 +1098,126 @@ Proof.
   destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?.
   destruct SAT as [valu1 NH1].
   exploit valnum_regs_holds; eauto. intros (valu2 & NH2 & EQ & AG & P & Q).
-  destruct trap.
-
-  (* TRAP *)
-  {
-  destruct (find_rhs n1 (Load chunk addr vl)) as [r|] eqn:?.
-+ (* replaced by move *)
-  exploit find_rhs_sound; eauto. intros (v' & EV & LD).
-  assert (v' = v) by (inv EV; congruence). subst v'.
-  econstructor; split.
-  eapply exec_Iop; eauto. simpl; eauto.
-  econstructor; eauto.
-  eapply analysis_correct_1; eauto. simpl; auto.
-  unfold transfer; rewrite H.
-  eapply add_load_holds; eauto.
-  apply set_reg_lessdef; auto. eapply Val.lessdef_trans; eauto.
-+ (* load is preserved, but addressing is possibly simplified *)
-  destruct (reduce addressing combine_addr n1 addr args vl) as [addr' args'] eqn:?.
-  assert (ADDR: eval_addressing ge sp addr' rs##args' = Some a).
-  { eapply reduce_sound with (sem := fun addr vl => eval_addressing ge sp addr vl); eauto.
-    intros; eapply combine_addr_sound; eauto. }
-  exploit eval_addressing_lessdef. apply regs_lessdef_regs; eauto. eexact ADDR.
-  intros [a' [A B]].
-  assert (ADDR': eval_addressing tge sp addr' rs'##args' = Some a').
-  { rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved. }
-  exploit Mem.loadv_extends; eauto.
-  intros [v' [X Y]].
-  econstructor; split.
-  eapply exec_Iload; eauto.
-  econstructor; eauto.
-  eapply analysis_correct_1; eauto. simpl; auto.
-  unfold transfer; rewrite H.
-  eapply add_load_holds; eauto.
-  apply set_reg_lessdef; auto.
-  }
-
-  (* NOTRAP *)
-  {
-    assert (exists a' : val,
-       eval_addressing ge sp addr rs' ## args = Some a' /\ Val.lessdef a a')
-       as Haa'.    
-    apply eval_addressing_lessdef with (vl1 := rs ## args).
-    apply regs_lessdef_regs; assumption.
-    assumption.
-    destruct Haa' as [a' [Ha'1 Ha'2]].
-
-    assert (
-    exists v' : val,
-        Mem.loadv chunk m' a' = Some v' /\ Val.lessdef v v') as Hload' by
-    (apply Mem.loadv_extends with (m1 := m) (addr1 := a); assumption).
-    destruct Hload' as [v' [Hv'1 Hv'2]].
-
-    econstructor. split.
-    eapply exec_Iload; eauto.
-    try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved).
-
-    econstructor; eauto.
-    eapply analysis_correct_1; eauto. simpl; eauto.
-    unfold transfer. rewrite H.
-    exists valu1.
-    apply set_unknown_holds.
-    assumption.
-    apply set_reg_lessdef; assumption.
-  }
-
-- (* Iload notrap 1*)
-  destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?.
-  destruct SAT as [valu1 NH1].
-  exploit valnum_regs_holds; eauto. intros (valu2 & NH2 & EQ & AG & P & Q).
-
-    econstructor. split.
-    eapply exec_Iload_notrap1; eauto.
-    rewrite eval_addressing_preserved with (ge1 := ge).
-    apply eval_addressing_lessdef_none with (vl1 := rs ## args).
-    apply regs_lessdef_regs; assumption.
-    assumption.
-    exact symbols_preserved.
-
-    econstructor; eauto.
-    eapply analysis_correct_1; eauto. simpl; eauto.
-    unfold transfer. rewrite H.
-    exists valu1.
-    apply set_unknown_holds.
-    assumption.
-    apply set_reg_lessdef.
-    constructor. assumption.
-  
-- (* Iload notrap 2*)
-  destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?.
-  destruct SAT as [valu1 NH1].
-  exploit valnum_regs_holds; eauto. intros (valu2 & NH2 & EQ & AG & P & Q).
-
-    assert (exists a' : val,
-       eval_addressing ge sp addr rs' ## args = Some a' /\ Val.lessdef a a')
-       as Haa'.    
-    apply eval_addressing_lessdef with (vl1 := rs ## args).
-    apply regs_lessdef_regs; assumption.
-    assumption.
-    destruct Haa' as [a' [Ha'1 Ha'2]].
+  destruct trap; inv H0.
+
+  + (* TRAP *)
+    { destruct (find_rhs n1 (Load chunk addr vl)) as [r|] eqn:?.
+      * (* replaced by move *)
+        exploit find_rhs_sound; eauto. intros (v' & EV & LD).
+        assert (v' = v) by (inv EV; congruence). subst v'.
+        econstructor; split.
+        eapply exec_Iop; eauto. simpl; eauto.
+        econstructor; eauto.
+        eapply analysis_correct_1; eauto. simpl; auto.
+        unfold transfer; rewrite H.
+        eapply add_load_holds; eauto.
+        apply set_reg_lessdef; auto. eapply Val.lessdef_trans; eauto.
+      * (* load is preserved, but addressing is possibly simplified *)
+        destruct (reduce addressing combine_addr n1 addr args vl) as [addr' args'] eqn:?.
+        assert (ADDR: eval_addressing ge sp addr' rs##args' = Some a).
+        { eapply reduce_sound with (sem := fun addr vl => eval_addressing ge sp addr vl); eauto.
+          intros; eapply combine_addr_sound; eauto. }
+        exploit eval_addressing_lessdef. apply regs_lessdef_regs; eauto. eexact ADDR.
+        intros [a' [A B]].
+        assert (ADDR': eval_addressing tge sp addr' rs'##args' = Some a').
+        { rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved. }
+        exploit Mem.loadv_extends; eauto.
+        intros [v' [X Y]].
+        econstructor; split.
+        eapply exec_Iload; eauto. eapply has_loaded_normal; eauto.
+        econstructor; eauto.
+        eapply analysis_correct_1; eauto. simpl; auto.
+        unfold transfer; rewrite H.
+        eapply add_load_holds; eauto.
+        apply set_reg_lessdef; auto. }
+
+  + (* NOTRAP1 *)
+    { assert (exists a' : val,
+         eval_addressing ge sp addr rs' ## args = Some a' /\ Val.lessdef a a')
+         as Haa'.    
+      apply eval_addressing_lessdef with (vl1 := rs ## args).
+      apply regs_lessdef_regs; assumption.
+      assumption.
+      destruct Haa' as [a' [Ha'1 Ha'2]].
 
-    destruct (Mem.loadv chunk m' a') eqn:Hload'.
+      assert (
+      exists v' : val,
+          Mem.loadv chunk m' a' = Some v' /\ Val.lessdef v v') as Hload' by
+      (apply Mem.loadv_extends with (m1 := m) (addr1 := a); assumption).
+      destruct Hload' as [v' [Hv'1 Hv'2]].
 
-    {
       econstructor. split.
-      eapply exec_Iload; eauto.
+      eapply exec_Iload; eauto. eapply has_loaded_normal; eauto.
       try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved).
-      
+
       econstructor; eauto.
       eapply analysis_correct_1; eauto. simpl; eauto.
       unfold transfer. rewrite H.
       exists valu1.
       apply set_unknown_holds.
       assumption.
-      apply set_reg_lessdef; eauto.
+      apply set_reg_lessdef; assumption.
     }
-    {
-      econstructor. split.
-      eapply exec_Iload_notrap2; eauto.
-      try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved).
-      
-      econstructor; eauto.
-      eapply analysis_correct_1; eauto. simpl; eauto.
-      unfold transfer. rewrite H.
-      exists valu1.
-      apply set_unknown_holds.
+
+  + (* NOTRAP2 *)
+    destruct (eval_addressing) eqn:EVAL in LOAD.
+    * specialize (LOAD v).
+      assert (exists a' : val,
+         eval_addressing ge sp addr rs' ## args = Some a' /\ Val.lessdef v a')
+         as Haa'.    
+      apply eval_addressing_lessdef with (vl1 := rs ## args).
+      apply regs_lessdef_regs; assumption.
       assumption.
-      apply set_reg_lessdef.
-      constructor. assumption.
-    }
-    
+      destruct Haa' as [a' [Ha'1 Ha'2]].
+
+      destruct (Mem.loadv chunk m' a') eqn:Hload'.
+
+      {
+        econstructor. split.
+        eapply exec_Iload; eauto. eapply has_loaded_normal; eauto.
+        try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved).
+        
+        econstructor; eauto.
+        eapply analysis_correct_1; eauto. simpl; eauto.
+        unfold transfer. rewrite H.
+        exists valu1.
+        apply set_unknown_holds.
+        assumption.
+        apply set_reg_lessdef; eauto.
+      }
+      {
+        econstructor. split.
+        eapply exec_Iload; eauto. eapply has_loaded_default; eauto.
+        try (intros a EVAL';
+          rewrite eval_addressing_preserved with (ge1 := ge) in EVAL'; [| exact symbols_preserved];
+          inv Ha'2; rewrite Ha'1 in EVAL'; inv EVAL'; auto).
+        
+        econstructor; eauto.
+        eapply analysis_correct_1; eauto. simpl; eauto.
+        unfold transfer. rewrite H.
+        exists valu1.
+        apply set_unknown_holds.
+        assumption.
+        apply set_reg_lessdef.
+        constructor. assumption.
+      }
+    * econstructor. split.
+      -- eapply exec_Iload; eauto. eapply has_loaded_default; eauto.
+         rewrite eval_addressing_preserved with (ge1 := ge).
+         intros a EVAL'. eapply eval_addressing_lessdef_none with (vl1 := rs ## args) in EVAL.
+         erewrite EVAL in EVAL'. congruence.
+         apply regs_lessdef_regs; assumption.
+         exact symbols_preserved.
+
+      -- econstructor; eauto.
+         eapply analysis_correct_1; eauto. simpl; eauto.
+         unfold transfer. rewrite H.
+         exists valu1.
+         apply set_unknown_holds.
+         assumption.
+         apply set_reg_lessdef.
+         constructor. assumption.
+  
 - (* Istore *)
   destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?.
   destruct SAT as [valu1 NH1].
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index b59ee8b4..749add67 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -402,90 +402,89 @@ Proof.
 
 - (* Iload *)
   rename pc'0 into pc. TransfInstr.
-  set (aa := eval_static_addressing addr (aregs ae args)).
-  assert (VM1: vmatch bc a aa) by (eapply eval_static_addressing_sound; eauto with va).
-  set (av := loadv chunk (romem_for cu) am aa).
-  assert (VM2: vmatch bc v av) by (eapply loadv_sound; eauto).
-  destruct trap.
-  {
-  destruct (const_for_result av) as [cop|] eqn:?; intros.
-+ (* constant-propagated *)
-  exploit const_for_result_correct; eauto. intros (v' & A & B).
-  left; econstructor; econstructor; split.
-  eapply exec_Iop; eauto.
-  eapply match_states_succ; eauto.
-  apply set_reg_lessdef; auto.
-+ (* strength-reduced *)
-  assert (ADDR:
-     let (addr', args') := addr_strength_reduction addr args (aregs ae args) in
-     exists a',
-        eval_addressing ge (Vptr sp0 Ptrofs.zero) addr' rs ## args' = Some a' /\
-        Val.lessdef a a').
-  { eapply addr_strength_reduction_correct with (ae := ae); eauto with va. }
-  destruct (addr_strength_reduction addr args (aregs ae args)) as [addr' args'].
-  destruct ADDR as (a' & P & Q).
-  exploit eval_addressing_lessdef. eapply regs_lessdef_regs; eauto. eexact P.
-  intros (a'' & U & V).
-  assert (W: eval_addressing tge (Vptr sp0 Ptrofs.zero) addr' rs'##args' = Some a'').
-  { rewrite <- U. apply eval_addressing_preserved. exact symbols_preserved. }
-  exploit Mem.loadv_extends. eauto. eauto. apply Val.lessdef_trans with a'; eauto.
-  intros (v' & X & Y).
-  left; econstructor; econstructor; split.
-  eapply exec_Iload; eauto.
-  eapply match_states_succ; eauto. apply set_reg_lessdef; auto.
-  }
-  {
-    assert (exists v2 : val,
-         eval_addressing ge (Vptr sp0 Ptrofs.zero) addr (rs' ## args) = Some v2 /\ Val.lessdef a v2) as Hexist2.
-    apply eval_addressing_lessdef with (vl1 := rs ## args).
-    apply regs_lessdef_regs; assumption.
-    assumption.
-    destruct Hexist2 as [v2 [Heval2 Hlessdef2]].
-    destruct (Mem.loadv_extends chunk m m' a v2 v MEM H1 Hlessdef2) as [vX [Hvx1 Hvx2]].
-    left; econstructor; econstructor; split.
-    eapply exec_Iload with (a := v2); eauto.
-    try (erewrite eval_addressing_preserved with (ge1:=ge); auto;
-    exact symbols_preserved).
-  eapply match_states_succ; eauto. apply set_reg_lessdef; auto.
-    
-  }
-
-- (* Iload notrap1 *)
-  rename pc'0 into pc. TransfInstr.
-  assert (eval_addressing tge (Vptr sp0 Ptrofs.zero) addr (rs' ## args) =  None).
-  rewrite eval_addressing_preserved with (ge1 := ge); eauto.
-  apply eval_addressing_lessdef_none with (vl1 := rs ## args).
-  apply regs_lessdef_regs; assumption.
-  assumption.
-  exact symbols_preserved.
-  
-  left; econstructor; econstructor; split.
-  eapply exec_Iload_notrap1; eauto.
-  eapply match_states_succ; eauto. apply set_reg_lessdef; auto.
-
-- (* Iload notrap2 *)
-  rename pc'0 into pc. TransfInstr.
-    assert (exists v2 : val,
-         eval_addressing ge (Vptr sp0 Ptrofs.zero) addr (rs' ## args) = Some v2 /\ Val.lessdef a v2) as Hexist2.
-    apply eval_addressing_lessdef with (vl1 := rs ## args).
-    apply regs_lessdef_regs; assumption.
-    assumption.
-    destruct Hexist2 as [a' [Heval' Hlessdef']].
-    destruct (Mem.loadv chunk m' a') eqn:Hload'.
+  inv H0.
+  + set (aa := eval_static_addressing addr (aregs ae args)).
+    assert (VM1: vmatch bc a aa) by (eapply eval_static_addressing_sound; eauto with va).
+    set (av := loadv chunk (romem_for cu) am aa).
+    assert (VM2: vmatch bc v av) by (eapply loadv_sound; eauto).
+    destruct trap.
     {
+    destruct (const_for_result av) as [cop|] eqn:?; intros.
+  * (* constant-propagated *)
+    exploit const_for_result_correct; eauto. intros (v' & A & B).
+    left; econstructor; econstructor; split.
+    eapply exec_Iop; eauto.
+    eapply match_states_succ; eauto.
+    apply set_reg_lessdef; auto.
+  * (* strength-reduced *)
+    assert (ADDR:
+       let (addr', args') := addr_strength_reduction addr args (aregs ae args) in
+       exists a',
+          eval_addressing ge (Vptr sp0 Ptrofs.zero) addr' rs ## args' = Some a' /\
+          Val.lessdef a a').
+    { eapply addr_strength_reduction_correct with (ae := ae); eauto with va. }
+    destruct (addr_strength_reduction addr args (aregs ae args)) as [addr' args'].
+    destruct ADDR as (a' & P & Q).
+    exploit eval_addressing_lessdef. eapply regs_lessdef_regs; eauto. eexact P.
+    intros (a'' & U & V).
+    assert (W: eval_addressing tge (Vptr sp0 Ptrofs.zero) addr' rs'##args' = Some a'').
+    { rewrite <- U. apply eval_addressing_preserved. exact symbols_preserved. }
+    exploit Mem.loadv_extends. eauto. eauto. apply Val.lessdef_trans with a'; eauto.
+    intros (v' & X & Y).
     left; econstructor; econstructor; split.
-    eapply exec_Iload; eauto.
-   
-    try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved).
+    eapply exec_Iload; eauto. eapply has_loaded_normal; eauto.
     eapply match_states_succ; eauto. apply set_reg_lessdef; auto.
     }
     {
+      assert (exists v2 : val,
+           eval_addressing ge (Vptr sp0 Ptrofs.zero) addr (rs' ## args) = Some v2 /\ Val.lessdef a v2) as Hexist2.
+      apply eval_addressing_lessdef with (vl1 := rs ## args).
+      apply regs_lessdef_regs; assumption.
+      assumption.
+      destruct Hexist2 as [v2 [Heval2 Hlessdef2]].
+      destruct (Mem.loadv_extends chunk m m' a v2 v MEM LOAD Hlessdef2) as [vX [Hvx1 Hvx2]].
       left; econstructor; econstructor; split.
-      eapply exec_Iload_notrap2; eauto.
-   
-    try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved).
+      eapply exec_Iload; eauto. eapply has_loaded_normal; eauto.
+      try (erewrite eval_addressing_preserved with (ge1:=ge); auto;
+      exact symbols_preserved).
     eapply match_states_succ; eauto. apply set_reg_lessdef; auto.
+      
     }
+  + destruct (eval_addressing) eqn:EVAL in LOAD.
+    * specialize (LOAD v). 
+      assert (exists v2 : val,
+           eval_addressing ge (Vptr sp0 Ptrofs.zero) addr (rs' ## args) = Some v2 /\ Val.lessdef v v2) as Hexist2.
+      apply eval_addressing_lessdef with (vl1 := rs ## args).
+      apply regs_lessdef_regs; assumption.
+      assumption.
+      destruct Hexist2 as [a' [Heval' Hlessdef']].
+      destruct (Mem.loadv chunk m' a') eqn:Hload'.
+      {
+      left; econstructor; econstructor; split.
+      eapply exec_Iload; eauto.
+     
+      try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved).
+      eapply has_loaded_normal; eauto.
+      try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved).
+      eapply match_states_succ; eauto. apply set_reg_lessdef; auto.
+      }
+      {
+      left; econstructor; econstructor; split.
+      eapply exec_Iload; eauto. eapply has_loaded_default; eauto.
+      try (intros a; rewrite eval_addressing_preserved with (ge1 := ge); [ intros CONTRA; try congruence | exact symbols_preserved ]).
+      eapply match_states_succ; eauto. apply set_reg_lessdef; auto.
+      }
+    * assert (eval_addressing tge (Vptr sp0 Ptrofs.zero) addr (rs' ## args) =  None).
+      rewrite eval_addressing_preserved with (ge1 := ge); eauto.
+      apply eval_addressing_lessdef_none with (vl1 := rs ## args).
+      apply regs_lessdef_regs; assumption.
+      assumption.
+      exact symbols_preserved.
+      
+      left; econstructor; econstructor; split.
+      eapply exec_Iload; eauto. eapply has_loaded_default; eauto.
+      intros; congruence.
+      eapply match_states_succ; eauto. apply set_reg_lessdef; auto.
 
 - (* Istore *)
   rename pc'0 into pc. TransfInstr.
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)
diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v
index 2f3bad2f..5752f5d2 100644
--- a/backend/Duplicateproof.v
+++ b/backend/Duplicateproof.v
@@ -414,25 +414,19 @@ Proof.
 (* Iload *)
   - eapply dupmap_correct in DUPLIC; eauto.
     destruct DUPLIC as (i' & H2 & H3). inv H3.
-    pose symbols_preserved as SYMPRES.
-    eexists. split.
-    + eapply exec_Iload; eauto; (* is the follow still needed?*) erewrite eval_addressing_preserved; eauto.
-    + econstructor; eauto.
-(* Iload notrap1 *)
-  - eapply dupmap_correct in DUPLIC; eauto.
-    destruct DUPLIC as (i' & H2 & H3). inv H3.
-    pose symbols_preserved as SYMPRES.
-    eexists. split.
-    + eapply exec_Iload_notrap1; eauto; erewrite eval_addressing_preserved; eauto. 
-    + econstructor; eauto.
-(* Iload notrap2 *)
-  - eapply dupmap_correct in DUPLIC; eauto.
-    destruct DUPLIC as (i' & H2 & H3). inv H3.
-    pose symbols_preserved as SYMPRES.
-    eexists. split.
-    + eapply exec_Iload_notrap2; eauto; erewrite eval_addressing_preserved; eauto.
-    + econstructor; eauto.
-      
+    pose symbols_preserved as SYMPRES. inv H0.
+    + eexists; split.
+      * try (eapply exec_Iload; eauto; eapply has_loaded_normal; eauto; erewrite eval_addressing_preserved; eauto).
+      * econstructor; eauto.
+    + destruct (eval_addressing) eqn:EVAL in LOAD.
+      * specialize (LOAD v). eexists; split.
+        -- eapply exec_Iload; eauto. eapply has_loaded_default; eauto. erewrite eval_addressing_preserved; eauto.
+           intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'. apply LOAD; auto.
+        -- econstructor; eauto.
+      * eexists; split.
+        -- eapply exec_Iload; eauto. eapply has_loaded_default; eauto. erewrite eval_addressing_preserved; eauto.
+           intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'.
+        -- econstructor; eauto.
 (* Istore *)
   - eapply dupmap_correct in DUPLIC; eauto.
     destruct DUPLIC as (i' & H2 & H3). inv H3.
diff --git a/backend/FirstNopproof.v b/backend/FirstNopproof.v
index 5a1c5acf..b0cf0879 100644
--- a/backend/FirstNopproof.v
+++ b/backend/FirstNopproof.v
@@ -178,23 +178,28 @@ Proof.
       apply eval_operation_preserved.
       apply symbols_preserved.
     + constructor; auto with firstnop.
-  - left. econstructor. split.
-    + eapply plus_one. eapply exec_Iload with (v:=v); eauto with firstnop.
-      all: rewrite <- H0.
-      all: auto using eval_addressing_preserved, symbols_preserved.
-    + constructor; auto with firstnop.
-  - left. econstructor. split.
-    + eapply plus_one. eapply exec_Iload_notrap1; eauto with firstnop.
-      all: rewrite <- H0;
-      apply eval_addressing_preserved;
-      apply symbols_preserved.
-    + constructor; auto with firstnop.
-  - left. econstructor. split.
-    + eapply plus_one. eapply exec_Iload_notrap2; eauto with firstnop.
-      all: rewrite <- H0;
-      apply eval_addressing_preserved;
-      apply symbols_preserved.
-    + constructor; auto with firstnop.
+  - left. inv H0.
+    + econstructor. split.
+      * eapply plus_one. eapply exec_Iload with (v:=v); eauto with firstnop.
+        eapply has_loaded_normal; eauto.
+        all: rewrite <- EVAL.
+        all: auto using eval_addressing_preserved, symbols_preserved.
+      * constructor; auto with firstnop.
+    + destruct (eval_addressing) eqn:EVAL in LOAD.
+      * specialize (LOAD v). econstructor; split.
+        -- eapply plus_one. eapply exec_Iload; eauto with firstnop.
+           eapply has_loaded_default; eauto.
+           all:
+           rewrite eval_addressing_preserved with (ge1:=ge); [| apply symbols_preserved];
+           intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'; apply LOAD; auto.
+        -- constructor; auto with firstnop.
+      * econstructor; split.
+        -- eapply plus_one. eapply exec_Iload; eauto with firstnop.
+           eapply has_loaded_default; eauto.
+           all:
+           rewrite eval_addressing_preserved with (ge1:=ge); [| apply symbols_preserved];
+           intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'; apply LOAD; auto.
+        -- constructor; auto with firstnop.
   - left. econstructor. split.
     + eapply plus_one. eapply exec_Istore; eauto with firstnop.
       all: rewrite <- H0;
diff --git a/backend/ForwardMovesproof.v b/backend/ForwardMovesproof.v
index f3e572e0..27137206 100644
--- a/backend/ForwardMovesproof.v
+++ b/backend/ForwardMovesproof.v
@@ -494,89 +494,89 @@ Proof.
   assumption.
   
 (* 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.
-  rewrite subst_args_ok; assumption.
-  constructor; auto.
-
-  simpl in *.
-  unfold fmap_sem in *.
-  destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
-  destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
-  apply get_rb_sem_ge with (rb2 := Some (kill dst mpc)).
-  {
-    replace (Some (kill dst mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
-    {
-      eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
-      2: apply apply_instr'_bot.
-      simpl. tauto.
-    }
-    unfold apply_instr'.
-    rewrite H.
-    rewrite MPC.
-    reflexivity.
-  }
-  apply kill_ok.
-  assumption.
-  
-- (* 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.
-  rewrite subst_args_ok; assumption.
-  constructor; auto.
-
-  simpl in *.
-  unfold fmap_sem in *.
-  destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
-  destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
-  apply get_rb_sem_ge with (rb2 := Some (kill dst mpc)).
-  {
-    replace (Some (kill dst mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
-    {
-      eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
-      2: apply apply_instr'_bot.
-      simpl. tauto.
-    }
-    unfold apply_instr'.
-    rewrite H.
-    rewrite MPC.
-    reflexivity.
-  }
-  apply kill_ok.
-  assumption.
-  
-- (* 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.
-  rewrite subst_args_ok; assumption.
-  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.
+    rewrite subst_args_ok; assumption.
+    constructor; auto.
 
-  simpl in *.
-  unfold fmap_sem in *.
-  destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
-  destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
-  apply get_rb_sem_ge with (rb2 := Some (kill dst mpc)).
-  {
-    replace (Some (kill dst mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
+    simpl in *.
+    unfold fmap_sem in *.
+    destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
+    destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
+    apply get_rb_sem_ge with (rb2 := Some (kill dst mpc)).
     {
-      eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
-      2: apply apply_instr'_bot.
-      simpl. tauto.
+      replace (Some (kill dst mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
+      {
+        eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
+        2: apply apply_instr'_bot.
+        simpl. tauto.
+      }
+      unfold apply_instr'.
+      rewrite H.
+      rewrite MPC.
+      reflexivity.
     }
-    unfold apply_instr'.
-    rewrite H.
-    rewrite MPC.
-    reflexivity.
-  }
-  apply kill_ok.
-  assumption.
+    apply kill_ok.
+    assumption.
+  + 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.
+      rewrite subst_args_ok; eauto.
+      intros a EVAL'; rewrite H0 in EVAL'; inv EVAL'. apply LOAD; auto.
+      constructor; auto.
+
+      simpl in *.
+      unfold fmap_sem in *.
+      destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
+      destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
+      apply get_rb_sem_ge with (rb2 := Some (kill dst mpc)).
+      {
+        replace (Some (kill dst mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
+        {
+          eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
+          2: apply apply_instr'_bot.
+          simpl. tauto.
+        }
+        unfold apply_instr'.
+        rewrite H.
+        rewrite MPC.
+        reflexivity.
+      }
+      apply kill_ok.
+      assumption.
+    * 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.
+      rewrite subst_args_ok; eauto.
+      intros a EVAL'; rewrite H0 in EVAL'; inv EVAL'.
+      constructor; auto.
+
+      simpl in *.
+      unfold fmap_sem in *.
+      destruct (forward_map _) as [map |] eqn:MAP in *; trivial.
+      destruct (map # pc) as [mpc |] eqn:MPC in *; try contradiction.
+      apply get_rb_sem_ge with (rb2 := Some (kill dst mpc)).
+      {
+        replace (Some (kill dst mpc)) with (apply_instr' (fn_code f) pc (map # pc)).
+        {
+          eapply DS.fixpoint_solution with (code := fn_code f) (successors := successors_instr); try eassumption.
+          2: apply apply_instr'_bot.
+          simpl. tauto.
+        }
+        unfold apply_instr'.
+        rewrite H.
+        rewrite MPC.
+        reflexivity.
+      }
+      apply kill_ok.
+      assumption.
   
 - (* store *)
   econstructor; split.
diff --git a/backend/Injectproof.v b/backend/Injectproof.v
index dd5e72f8..13154850 100644
--- a/backend/Injectproof.v
+++ b/backend/Injectproof.v
@@ -785,24 +785,29 @@ Section INJECTOR.
           rewrite map_length.
           assumption.
       - rewrite Pos.ltb_lt in VALID.
-        destruct (eval_addressing ge sp addr trs ## args) as [a | ] eqn:ADDR.
+        destruct (eval_addressing ge sp addr trs ## args) as [a | ] eqn:EVAL.
         + destruct (Mem.loadv chunk m a) as [v | ] eqn:LOAD.
           * exists (trs # res <- v).
             split.
-            ** apply exec_Iload with (trap := NOTRAP) (chunk := chunk) (addr := addr) (args := args) (dst := res) (a := a); trivial.
+            ** apply exec_Iload with (trap := NOTRAP) (chunk := chunk) (addr := addr) (args := args) (dst := res); trivial.
+               eapply has_loaded_normal; eauto.
                all: try rewrite eval_addressing_preserved with (ge1 := ge).
                all: auto using symbols_preserved.
             ** apply assign_above; auto.
           * exists (trs # res <- Vundef).
             split.
-            ** apply exec_Iload_notrap2 with (chunk := chunk) (addr := addr) (args := args) (dst := res) (a := a); trivial.
+            ** apply exec_Iload with (trap := NOTRAP) (chunk := chunk) (addr := addr) (args := args) (dst := res); trivial.
+               eapply has_loaded_default; eauto.
                all: rewrite eval_addressing_preserved with (ge1 := ge).
+               intros a0 EVAL'; rewrite EVAL in EVAL'; inv EVAL'. assumption.
                all: auto using symbols_preserved.
             ** apply assign_above; auto.
         + exists (trs # res <- Vundef).
           split.
-          * apply exec_Iload_notrap1 with (chunk := chunk) (addr := addr) (args := args) (dst := res); trivial.
+          * apply exec_Iload with (trap := NOTRAP) (chunk := chunk) (addr := addr) (args := args) (dst := res); trivial.
+            eapply has_loaded_default; eauto.
             all: rewrite eval_addressing_preserved with (ge1 := ge).
+            intros a0 EVAL'; rewrite EVAL in EVAL'; inv EVAL'.
             all: auto using symbols_preserved.
           * apply assign_above; auto.
     Qed.
@@ -1351,128 +1356,127 @@ Section INJECTOR.
             assumption.
 
       - (* load *)
-        destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION.
-        + exploit transf_function_redirects; eauto.
-          { eapply max_pc_function_sound; eauto. }
-          intros [pc_inj [ALTER SKIP]].
-          specialize SKIP with (ts := ts) (sp := sp) (m := m)
-             (trs := trs # dst <- v).
-          destruct SKIP as [trs' [MATCH PLUS]].
-          econstructor; split.
-          * eapply Smallstep.plus_left.
-            ** apply exec_Iload with (trap := trap) (chunk := chunk) (addr := addr) (args := args) (a := a).
-               exact ALTER.
-               rewrite eval_addressing_preserved with (ge1 := ge).
-               {
-                 replace args with (instr_uses (Iload trap chunk addr args dst pc')) by reflexivity.
-                 rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
-               }
-               exact symbols_preserved.
-               eassumption.
-            ** apply Smallstep.plus_star.
-               exact PLUS.
-            ** reflexivity.
-          * constructor; trivial.
-            apply match_regs_trans with (rs2 := trs # dst <- v); trivial.
-            apply match_regs_write.
-            assumption.
-        + econstructor; split.
-          * apply Smallstep.plus_one.
-            apply exec_Iload with (trap := trap) (chunk := chunk) (addr := addr) (args := args) (a := a).
-            ** rewrite transf_function_preserves with (f:=f); eauto.
-               eapply max_pc_function_sound; eauto.
-            ** rewrite eval_addressing_preserved with (ge1 := ge).
-               {
-                 replace args with (instr_uses (Iload trap chunk addr args dst pc')) by reflexivity.
-                 rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
-               }
-               exact symbols_preserved.
-            ** eassumption.
-          * constructor; trivial.
-            apply match_regs_write.
-            assumption.
-        
-      - (* load notrap1 *)
-        destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION.
-        + exploit transf_function_redirects; eauto.
+        inv H0.
+        + destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION.
+          * exploit transf_function_redirects; eauto.
           { eapply max_pc_function_sound; eauto. }
-          intros [pc_inj [ALTER SKIP]].
-          specialize SKIP with (ts := ts) (sp := sp) (m := m)
-             (trs := trs # dst <- Vundef).
-          destruct SKIP as [trs' [MATCH PLUS]].
-          econstructor; split.
-          * eapply Smallstep.plus_left.
-            ** apply exec_Iload_notrap1 with (chunk := chunk) (addr := addr) (args := args).
-               exact ALTER.
-               rewrite eval_addressing_preserved with (ge1 := ge).
-               {
-                 replace args with (instr_uses (Iload NOTRAP chunk addr args dst pc')) by reflexivity.
-                 rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
-               }
-               exact symbols_preserved.
-            ** apply Smallstep.plus_star.
-               exact PLUS.
-            ** reflexivity.
-          * constructor; trivial.
-            apply match_regs_trans with (rs2 := trs # dst <- Vundef); trivial.
-            apply match_regs_write.
-            assumption.
-        + econstructor; split.
-          * apply Smallstep.plus_one.
-            apply exec_Iload_notrap1 with (chunk := chunk) (addr := addr) (args := args).
-            ** rewrite transf_function_preserves with (f:=f); eauto.
-               eapply max_pc_function_sound; eauto.
-            ** rewrite eval_addressing_preserved with (ge1 := ge).
-               {
-                 replace args with (instr_uses (Iload NOTRAP chunk addr args dst pc')) by reflexivity.
-                 rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
-               }
-               exact symbols_preserved.
-          * constructor; trivial.
-            apply match_regs_write.
-            assumption.
-
-      - (* load notrap2 *)
-        destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION.
-        + exploit transf_function_redirects; eauto.
-          { eapply max_pc_function_sound; eauto. }
-          intros [pc_inj [ALTER SKIP]].
-          specialize SKIP with (ts := ts) (sp := sp) (m := m)
-             (trs := trs # dst <- Vundef).
-          destruct SKIP as [trs' [MATCH PLUS]].
-          econstructor; split.
-          * eapply Smallstep.plus_left.
-            ** apply exec_Iload_notrap2 with (chunk := chunk) (addr := addr) (args := args) (a := a).
-               exact ALTER.
-               rewrite eval_addressing_preserved with (ge1 := ge).
-               {
-                 replace args with (instr_uses (Iload NOTRAP chunk addr args dst pc')) by reflexivity.
-                 rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
-               }
-               exact symbols_preserved.
-               eassumption.
-            ** apply Smallstep.plus_star.
-               exact PLUS.
-            ** reflexivity.
-          * constructor; trivial.
-            apply match_regs_trans with (rs2 := trs # dst <- Vundef); trivial.
-            apply match_regs_write.
-            assumption.
-        + econstructor; split.
-          * apply Smallstep.plus_one.
-            apply exec_Iload_notrap2 with (chunk := chunk) (addr := addr) (args := args) (a := a).
-            ** rewrite transf_function_preserves with (f:=f); eauto.
-               eapply max_pc_function_sound; eauto.
-            ** rewrite eval_addressing_preserved with (ge1 := ge).
-               {
-                 replace args with (instr_uses (Iload NOTRAP chunk addr args dst pc')) by reflexivity.
-                 rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
-               }
-               exact symbols_preserved.
-            ** eassumption.
-          * constructor; trivial.
-            apply match_regs_write.
-            assumption.
+            intros [pc_inj [ALTER SKIP]].
+            specialize SKIP with (ts := ts) (sp := sp) (m := m)
+               (trs := trs # dst <- v).
+            destruct SKIP as [trs' [MATCH PLUS]].
+            econstructor; split.
+            -- eapply Smallstep.plus_left.
+               ** apply exec_Iload with (trap := trap) (chunk := chunk) (addr := addr) (args := args).
+                  exact ALTER.
+                  eapply has_loaded_normal; eauto. rewrite eval_addressing_preserved with (ge1 := ge).
+                  {
+                    replace args with (instr_uses (Iload trap chunk addr args dst pc')) by reflexivity.
+                    rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
+                  }
+                  exact symbols_preserved.
+               ** apply Smallstep.plus_star.
+                  exact PLUS.
+               ** reflexivity.
+            -- constructor; trivial.
+               apply match_regs_trans with (rs2 := trs # dst <- v); trivial.
+               apply match_regs_write.
+               assumption.
+          * econstructor; split.
+            -- apply Smallstep.plus_one.
+               apply exec_Iload with (trap := trap) (chunk := chunk) (addr := addr) (args := args).
+               ** rewrite transf_function_preserves with (f:=f); eauto.
+                  eapply max_pc_function_sound; eauto.
+               ** eapply has_loaded_normal; eauto. rewrite eval_addressing_preserved with (ge1 := ge).
+                  {
+                    replace args with (instr_uses (Iload trap chunk addr args dst pc')) by reflexivity.
+                    rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
+                  }
+                  exact symbols_preserved.
+            -- constructor; trivial.
+               apply match_regs_write.
+               assumption.
+        + destruct (eval_addressing) eqn:EVAL in LOAD.
+          * specialize (LOAD v).
+            destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION.
+            -- exploit transf_function_redirects; eauto.
+               { eapply max_pc_function_sound; eauto. }
+               intros [pc_inj [ALTER SKIP]].
+               specialize SKIP with (ts := ts) (sp := sp) (m := m)
+                  (trs := trs # dst <- Vundef).
+               destruct SKIP as [trs' [MATCH PLUS]].
+               econstructor; split.
+               ++ eapply Smallstep.plus_left.
+                  ** apply exec_Iload with (trap := NOTRAP) (chunk := chunk) (addr := addr) (args := args).
+                     exact ALTER.
+                     eapply has_loaded_default; eauto. rewrite eval_addressing_preserved with (ge1 := ge).
+                     {
+                       replace args with (instr_uses (Iload NOTRAP chunk addr args dst pc')) by reflexivity.
+                       rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
+                       simpl. intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'. apply LOAD; auto.
+                     }
+                     exact symbols_preserved.
+                  ** apply Smallstep.plus_star.
+                     exact PLUS.
+                  ** reflexivity.
+               ++ constructor; trivial.
+                  apply match_regs_trans with (rs2 := trs # dst <- Vundef); trivial.
+                  apply match_regs_write.
+                  assumption.
+            -- econstructor; split.
+               ++ apply Smallstep.plus_one.
+                  apply exec_Iload with (trap := NOTRAP) (chunk := chunk) (addr := addr) (args := args).
+                  ** rewrite transf_function_preserves with (f:=f); eauto.
+                     eapply max_pc_function_sound; eauto.
+                  ** eapply has_loaded_default; eauto. rewrite eval_addressing_preserved with (ge1 := ge).
+                     {
+                       replace args with (instr_uses (Iload NOTRAP chunk addr args dst pc')) by reflexivity.
+                       rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
+                       simpl. intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'. apply LOAD; auto.
+                     }
+                     exact symbols_preserved.
+               ++ constructor; trivial.
+                  apply match_regs_write.
+                  assumption.
+          * destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION.
+            -- exploit transf_function_redirects; eauto.
+               { eapply max_pc_function_sound; eauto. }
+               intros [pc_inj [ALTER SKIP]].
+               specialize SKIP with (ts := ts) (sp := sp) (m := m)
+                  (trs := trs # dst <- Vundef).
+               destruct SKIP as [trs' [MATCH PLUS]].
+               econstructor; split.
+               ++ eapply Smallstep.plus_left.
+                  ** apply exec_Iload with (trap := NOTRAP) (chunk := chunk) (addr := addr) (args := args).
+                     exact ALTER.
+                     eapply has_loaded_default; eauto. rewrite eval_addressing_preserved with (ge1 := ge).
+                     {
+                       replace args with (instr_uses (Iload NOTRAP chunk addr args dst pc')) by reflexivity.
+                       rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
+                       simpl. intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'.
+                     }
+                     exact symbols_preserved.
+                  ** apply Smallstep.plus_star.
+                     exact PLUS.
+                  ** reflexivity.
+               ++ constructor; trivial.
+                  apply match_regs_trans with (rs2 := trs # dst <- Vundef); trivial.
+                  apply match_regs_write.
+                  assumption.
+            -- econstructor; split.
+               ++ apply Smallstep.plus_one.
+                  apply exec_Iload with (trap := NOTRAP) (chunk := chunk) (addr := addr) (args := args).
+                  ** rewrite transf_function_preserves with (f:=f); eauto.
+                     eapply max_pc_function_sound; eauto.
+                  ** eapply has_loaded_default; eauto. rewrite eval_addressing_preserved with (ge1 := ge).
+                     {
+                       replace args with (instr_uses (Iload NOTRAP chunk addr args dst pc')) by reflexivity.
+                       rewrite transf_function_preserves_uses with (f := f) (tf := tf) (pc := pc) (rs := rs); trivial.
+                       simpl. intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'.
+                     }
+                     exact symbols_preserved.
+               ++ constructor; trivial.
+                  apply match_regs_write.
+                  assumption.
         
       - (* store *)
         destruct ((gen_injections f (max_pc_function f) (max_reg_function f)) ! pc) eqn:INJECTION.
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v
index eb30732b..647938f3 100644
--- a/backend/Inliningproof.v
+++ b/backend/Inliningproof.v
@@ -969,66 +969,53 @@ Proof.
   apply agree_set_reg; auto.
 
 - (* load *)
-  exploit tr_funbody_inv; eauto. intros TR; inv TR.
-  exploit eval_addressing_inject.
-    eapply match_stacks_inside_globals; eauto.
-    eexact SP.
-    instantiate (2 := rs##args). instantiate (1 := rs'##(sregs ctx args)). eapply agree_val_regs; eauto.
-    eauto.
-  fold (saddr ctx addr). intros [a' [P Q]].
-  exploit Mem.loadv_inject; eauto. intros [v' [U V]].
-  assert (eval_addressing tge (Vptr sp' Ptrofs.zero) (saddr ctx addr) rs' ## (sregs ctx args) = Some a').
-  rewrite <- P. apply eval_addressing_preserved. exact symbols_preserved.
-  left; econstructor; split.
-  eapply plus_one. eapply exec_Iload; eauto.
-  econstructor; eauto.
-  apply match_stacks_inside_set_reg; auto.
-  apply agree_set_reg; auto.
-
-- (* load notrap1 *)
-  exploit tr_funbody_inv; eauto. intros TR; inv TR.
-  left; econstructor; split.
-  eapply plus_one. eapply exec_Iload_notrap1. eassumption.
-  rewrite eval_addressing_preserved with (ge1:=ge) (ge2:=tge).
-  exploit eval_addressing_inj_none.
-  4: eassumption.
-  intros. eapply symbol_address_inject.
-  eapply match_stacks_inside_globals; eauto.
-  eauto.
-  instantiate (1 := rs'##(sregs ctx args)). eapply agree_val_regs; eauto.
-  rewrite Ptrofs.add_zero_l.
-  apply eval_addressing_none.
-  exact symbols_preserved.
-  econstructor; eauto.
-  apply match_stacks_inside_set_reg; auto.
-  apply agree_set_reg; auto.
-
-- (* load notrap2 *)
-  exploit tr_funbody_inv; eauto. intros TR; inv TR.
-
-  exploit eval_addressing_inject.
+  exploit tr_funbody_inv; eauto. intros TR; inv TR. inv H0.
+  + exploit eval_addressing_inject.
     eapply match_stacks_inside_globals; eauto.
     eexact SP.
     instantiate (2 := rs##args). instantiate (1 := rs'##(sregs ctx args)). eapply agree_val_regs; eauto.
     eauto.
-  fold (saddr ctx addr). intros [a' [P Q]].
-
-  destruct (Mem.loadv chunk m' a') eqn:Hload'.
-  + left; econstructor; split.
-    eapply plus_one.
-    eapply exec_Iload; eauto.
-    try (rewrite <- P; apply eval_addressing_preserved; exact symbols_preserved).
-    econstructor; eauto.
-  apply match_stacks_inside_set_reg; auto.
-  apply agree_set_reg; auto.
-    
-  + left; econstructor; split.
-    eapply plus_one.
-    eapply exec_Iload_notrap2; eauto.
-    try (rewrite <- P; apply eval_addressing_preserved; exact symbols_preserved).
-    econstructor; eauto.
-  apply match_stacks_inside_set_reg; auto.
-  apply agree_set_reg; auto.
+    fold (saddr ctx addr). intros [a' [P Q]].
+    exploit Mem.loadv_inject; eauto. intros [v' [U V]].
+    assert (eval_addressing tge (Vptr sp' Ptrofs.zero) (saddr ctx addr) rs' ## (sregs ctx args) = Some a').
+    { rewrite <- P. apply eval_addressing_preserved. exact symbols_preserved. }
+    left; econstructor; split.
+    * eapply plus_one. eapply exec_Iload; eauto. eapply has_loaded_normal; eauto.
+    * econstructor; eauto. apply match_stacks_inside_set_reg; auto.
+      apply agree_set_reg; auto.
+  + destruct (eval_addressing) eqn:ADDR in LOAD.
+    * exploit eval_addressing_inject.
+      eapply match_stacks_inside_globals; eauto.
+      eexact SP.
+      instantiate (2 := rs##args). instantiate (1 := rs'##(sregs ctx args)). eapply agree_val_regs; eauto.
+      eauto.
+      fold (saddr ctx addr). intros [a' [P Q]].
+      destruct (Mem.loadv chunk m' a') eqn:Hload'.
+      -- left; econstructor; split.
+         ++ eapply plus_one. try (eapply exec_Iload; eauto; eapply has_loaded_normal; eauto;
+            rewrite <- P; apply eval_addressing_preserved; exact symbols_preserved).
+         ++ econstructor; eauto. apply match_stacks_inside_set_reg; auto.
+            apply agree_set_reg; auto.
+      -- left; econstructor; split.
+         ++ eapply plus_one. eapply exec_Iload; eauto. eapply has_loaded_default; eauto.
+            try (intros a ADDR'; erewrite eval_addressing_preserved in ADDR'; [ rewrite P in ADDR' |
+              exact symbols_preserved ]; inv ADDR'; assumption).
+         ++ econstructor; eauto. apply match_stacks_inside_set_reg; auto.
+            apply agree_set_reg; auto.
+    * left; econstructor; split.
+      -- eapply plus_one. eapply exec_Iload; eauto. eapply has_loaded_default; eauto.
+         intros. rewrite eval_addressing_preserved with (ge1:=ge) (ge2:=tge) in H0.
+         exploit eval_addressing_inj_none.
+         4: eassumption.
+         intros. eapply symbol_address_inject.
+         eapply match_stacks_inside_globals; eauto.
+         eauto.
+         instantiate (1 := rs'##(sregs ctx args)). eapply agree_val_regs; eauto.
+         rewrite Ptrofs.add_zero_l.
+         intros. apply eval_addressing_none in H1. congruence.
+         exact symbols_preserved.
+      -- econstructor; eauto. apply match_stacks_inside_set_reg; auto.
+         apply agree_set_reg; auto.
   
 - (* store *)
   exploit tr_funbody_inv; eauto. intros TR; inv TR.
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).
diff --git a/backend/ProfilingExploitproof.v b/backend/ProfilingExploitproof.v
index 78de09af..4308b670 100644
--- a/backend/ProfilingExploitproof.v
+++ b/backend/ProfilingExploitproof.v
@@ -126,23 +126,24 @@ 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.
+    * try (eapply exec_Iload; eauto; eapply has_loaded_normal; eauto;
+      rewrite <- EVAL; apply eval_addressing_preserved; exact symbols_preserved).
+    * econstructor; eauto.
+  + destruct (eval_addressing) eqn:EVAL in LOAD.
+    * specialize (LOAD v). econstructor; split.
+      -- eapply exec_Iload; eauto. eapply has_loaded_default; eauto.
+         rewrite eval_addressing_preserved with (ge1:=ge).
+         intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'. apply LOAD; auto.
+         exact symbols_preserved.
+      -- econstructor; eauto.
+    * econstructor; split.
+      -- eapply exec_Iload; eauto. eapply has_loaded_default; eauto.
+         rewrite eval_addressing_preserved with (ge1:=ge).
+         intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'.
+         exact symbols_preserved.
+      -- econstructor; eauto.
 - (* store *)
   econstructor; split.
   assert (eval_addressing tge sp addr rs ## args = Some a).
diff --git a/backend/Profilingproof.v b/backend/Profilingproof.v
index 0cebc601..e39e7f80 100644
--- a/backend/Profilingproof.v
+++ b/backend/Profilingproof.v
@@ -458,27 +458,27 @@ Proof.
       * rewrite eval_operation_preserved with (ge1:=ge);
           eauto with profiling.
     + constructor; auto.
-  - econstructor; split.
-    + apply plus_one. apply exec_Iload with (trap:=trap) (chunk:=chunk)
-                                            (addr:=addr) (args:=args) (a:=a).
-      erewrite transf_function_at; eauto. apply I.
-      rewrite eval_addressing_preserved with (ge1:=ge).
-      all: eauto with profiling.
-    + constructor; auto.
-  - econstructor; split.
-    + apply plus_one. apply exec_Iload_notrap1 with (chunk:=chunk)
-                                            (addr:=addr) (args:=args).
-      erewrite transf_function_at; eauto. apply I.
-      rewrite eval_addressing_preserved with (ge1:=ge).
-      all: eauto with profiling.
-    + constructor; auto.
-  -  econstructor; split.
-    + apply plus_one. apply exec_Iload_notrap2 with (chunk:=chunk)
-                                            (addr:=addr) (args:=args) (a:=a).
-      erewrite transf_function_at; eauto. apply I.
-      rewrite eval_addressing_preserved with (ge1:=ge).
-      all: eauto with profiling.
-    + constructor; auto.
+  - inv H0.
+    + econstructor; split.
+      * apply plus_one. eapply exec_Iload; eauto.
+        -- erewrite transf_function_at; eauto. apply I.
+        -- eapply has_loaded_normal. rewrite eval_addressing_preserved with (ge1:=ge).
+           all: eauto with profiling.
+      * constructor; auto.
+    + destruct (eval_addressing) eqn:EVAL in LOAD.
+      * econstructor; split.
+        -- specialize (LOAD v). apply plus_one. eapply exec_Iload; eauto.
+           ++ erewrite transf_function_at; eauto. apply I.
+           ++ eapply has_loaded_default; eauto. rewrite eval_addressing_preserved with (ge1:=ge).
+              intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'. apply LOAD; auto.
+              eauto with profiling.
+        -- constructor; auto.
+      * econstructor; split.
+        -- apply plus_one. eapply exec_Iload; eauto.
+           ++ erewrite transf_function_at; eauto. apply I.
+           ++ eapply has_loaded_default; eauto. rewrite eval_addressing_preserved with (ge1:=ge).
+              intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'. eauto with profiling.
+        -- constructor; auto.
   -  econstructor; split.
     + apply plus_one. apply exec_Istore with (chunk:=chunk) (src := src)
                                             (addr:=addr) (args:=args) (a:=a).
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') ->
diff --git a/backend/RTLTunnelingproof.v b/backend/RTLTunnelingproof.v
index 0861143b..aa21fc06 100644
--- a/backend/RTLTunnelingproof.v
+++ b/backend/RTLTunnelingproof.v
@@ -452,43 +452,47 @@ Proof.
       rewrite <- EVAL. apply eval_operation_preserved. apply symbols_preserved.
     + apply match_states_intro; eauto. apply set_reg_lessdef. apply LD. apply RS.
   - (* Iload *)
-    exploit eval_addressing_lessdef; try eassumption.
-    apply reglist_lessdef. apply RS.
-    intros (ta & EVAL & LD).
-    exploit Mem.loadv_extends; try eassumption.
-    intros (tv & LOAD & LD').
-    left. eexists. split.
-    + eapply exec_Iload.
-      * exploit instruction_type_preserved; (simpl; eauto)||congruence.
-      * rewrite <- EVAL. apply eval_addressing_preserved. apply symbols_preserved.
-      * apply LOAD.
-    + apply match_states_intro; try assumption. apply set_reg_lessdef. apply LD'. apply RS.
-  - (* Iload NOTRAP1 *)
-    exploit eval_addressing_lessdef_none; try eassumption.
-    apply reglist_lessdef; apply RS.
-    left. eexists. split.
-    + eapply exec_Iload_notrap1.
-      * exploit instruction_type_preserved; (simpl; eauto)||congruence.
-      * rewrite <- H1. apply eval_addressing_preserved. apply symbols_preserved.
-    + apply match_states_intro; try assumption. apply set_reg_lessdef. apply Val.lessdef_undef. apply RS.
-  - (* Iload NOTRAP2 *)
-    exploit eval_addressing_lessdef; try eassumption.
-    apply reglist_lessdef; apply RS.
-    intros (ta & EVAL & LD).
-    (* TODO: on peut sans doute factoriser ça *)
-    destruct (Mem.loadv chunk tm ta) eqn:Htload.
-    + left; eexists; split.
-      eapply exec_Iload.
-      * exploit instruction_type_preserved; (simpl; eauto)||congruence.
-      * rewrite <- EVAL. apply eval_addressing_preserved. apply symbols_preserved.
-      * apply Htload.
-      * apply match_states_intro; try assumption. apply set_reg_lessdef; eauto.
-    + left; eexists; split.
-      eapply exec_Iload_notrap2.
-      * exploit instruction_type_preserved; (simpl; eauto)||congruence.
-      * rewrite <- EVAL. apply eval_addressing_preserved. apply symbols_preserved.
-      * apply Htload.
-      * apply match_states_intro; try assumption. apply set_reg_lessdef; eauto.
+    inv H0.
+    + exploit eval_addressing_lessdef; try eassumption.
+      apply reglist_lessdef. apply RS.
+      intros (ta & EVAL' & LD).
+      exploit Mem.loadv_extends; try eassumption.
+      intros (tv & LOAD' & LD').
+      left. eexists. split.
+      * eapply exec_Iload.
+        -- exploit instruction_type_preserved; (simpl; eauto)||congruence.
+        -- try (eapply has_loaded_normal; eauto; rewrite <- EVAL'; apply eval_addressing_preserved; apply symbols_preserved).
+      * apply match_states_intro; try assumption. apply set_reg_lessdef. apply LD'. apply RS.
+    + destruct (eval_addressing) eqn:EVAL in LOAD.
+      * specialize (LOAD v).
+        exploit eval_addressing_lessdef; try eassumption.
+        apply reglist_lessdef; apply RS.
+        intros (ta & ADDR & LD).
+        (* TODO: on peut sans doute factoriser ça *)
+        destruct (Mem.loadv chunk tm ta) eqn:Htload.
+        -- left; eexists; split.
+           eapply exec_Iload.
+           ++ exploit instruction_type_preserved; (simpl; eauto)||congruence.
+           ++ try (eapply has_loaded_normal; eauto; rewrite <- ADDR; apply eval_addressing_preserved; apply symbols_preserved).
+           ++ apply match_states_intro; try assumption. apply set_reg_lessdef; eauto.
+        -- left; eexists; split.
+           eapply exec_Iload.
+           ++ exploit instruction_type_preserved; (simpl; eauto)||congruence.
+           ++ eapply has_loaded_default; eauto.
+              rewrite eval_addressing_preserved with (ge1:=ge).
+              intros a EVAL'; rewrite ADDR in EVAL'; inv EVAL'. auto.
+              apply symbols_preserved.
+           ++ apply match_states_intro; try assumption. apply set_reg_lessdef; eauto.
+      * exploit eval_addressing_lessdef_none; try eassumption.
+        apply reglist_lessdef; apply RS.
+        left. eexists. split.
+        -- eapply exec_Iload.
+           ++ exploit instruction_type_preserved; (simpl; eauto)||congruence.
+           ++ eapply has_loaded_default; eauto.
+              rewrite eval_addressing_preserved with (ge1:=ge).
+              intros a EVAL'; rewrite H0 in EVAL'; inv EVAL'.
+              apply symbols_preserved.
+        -- apply match_states_intro; try assumption. apply set_reg_lessdef. apply Val.lessdef_undef. apply RS.
   - (* Lstore *)
     exploit eval_addressing_lessdef; try eassumption.
     apply reglist_lessdef; apply RS.
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index d07dc968..2b1349d2 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -586,9 +586,9 @@ Proof.
   exists (rs1#rd <- v'); exists tm1.
 (* Exec *)
   split. eapply star_right. eexact EX1. eapply exec_Iload. eauto.
-  instantiate (1 := vaddr'). rewrite <- H3.
-  apply eval_addressing_preserved. exact symbols_preserved.
-  auto. traceEq.
+  econstructor; eauto. try (rewrite <- H3;
+  apply eval_addressing_preserved; exact symbols_preserved).
+  auto.
 (* Match-env *)
   split. eauto with rtlg.
 (* Result *)
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index 6048f895..85d3c439 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -938,60 +938,59 @@ Proof.
   induction 1; intros; inv WT;
   try (generalize (wt_instrs _ _ WT_FN pc _ H); intros WTI).
   (* Inop *)
-  econstructor; eauto.
+  - econstructor; eauto.
   (* Iop *)
-  econstructor; eauto. eapply wt_exec_Iop; eauto.
+  - econstructor; eauto. eapply wt_exec_Iop; eauto.
   (* Iload *)
-  econstructor; eauto. eapply wt_exec_Iload; eauto.
-  (* Iload notrap1*)
-  econstructor; eauto. eapply wt_exec_Iload_notrap; eauto.
-  (* Iload notrap2*)
-  econstructor; eauto. eapply wt_exec_Iload_notrap; eauto.
+  - econstructor; eauto. inv H0.
+    + eapply wt_exec_Iload; eauto.
+    + destruct (eval_addressing) eqn:EVAL in LOAD;
+      eapply wt_exec_Iload_notrap; eauto.
   (* Istore *)
-  econstructor; eauto.
+  - econstructor; eauto.
   (* Icall *)
-  assert (wt_fundef fd).
-    destruct ros; simpl in H0.
-    pattern fd. apply Genv.find_funct_prop with fundef unit p (rs#r).
-    exact wt_p. exact H0.
-    caseEq (Genv.find_symbol ge i); intros; rewrite H1 in H0.
-    pattern fd. apply Genv.find_funct_ptr_prop with fundef unit p b.
-    exact wt_p. exact H0.
-    discriminate.
-  econstructor; eauto.
-  econstructor; eauto. inv WTI; auto.
-  inv WTI. rewrite <- H8. apply wt_regset_list. auto.
+  - assert (wt_fundef fd).
+      destruct ros; simpl in H0.
+      pattern fd. apply Genv.find_funct_prop with fundef unit p (rs#r).
+      exact wt_p. exact H0.
+      caseEq (Genv.find_symbol ge i); intros; rewrite H1 in H0.
+      pattern fd. apply Genv.find_funct_ptr_prop with fundef unit p b.
+      exact wt_p. exact H0.
+      discriminate.
+    econstructor; eauto.
+    econstructor; eauto. inv WTI; auto.
+    inv WTI. rewrite <- H8. apply wt_regset_list. auto.
   (* Itailcall *)
-  assert (wt_fundef fd).
-    destruct ros; simpl in H0.
-    pattern fd. apply Genv.find_funct_prop with fundef unit p (rs#r).
-    exact wt_p. exact H0.
-    caseEq (Genv.find_symbol ge i); intros; rewrite H1 in H0.
-    pattern fd. apply Genv.find_funct_ptr_prop with fundef unit p b.
-    exact wt_p. exact H0.
-    discriminate.
-  econstructor; eauto.
-  inv WTI. apply wt_stackframes_change_sig with (fn_sig f); auto.
-  inv WTI. rewrite <- H7. apply wt_regset_list. auto.
+  - assert (wt_fundef fd).
+      destruct ros; simpl in H0.
+      pattern fd. apply Genv.find_funct_prop with fundef unit p (rs#r).
+      exact wt_p. exact H0.
+      caseEq (Genv.find_symbol ge i); intros; rewrite H1 in H0.
+      pattern fd. apply Genv.find_funct_ptr_prop with fundef unit p b.
+      exact wt_p. exact H0.
+      discriminate.
+    econstructor; eauto.
+    inv WTI. apply wt_stackframes_change_sig with (fn_sig f); auto.
+    inv WTI. rewrite <- H7. apply wt_regset_list. auto.
   (* Ibuiltin *)
-  econstructor; eauto. eapply wt_exec_Ibuiltin; eauto.
+  - econstructor; eauto. eapply wt_exec_Ibuiltin; eauto.
   (* Icond *)
-  econstructor; eauto.
+  - econstructor; eauto.
   (* Ijumptable *)
-  econstructor; eauto.
+  - econstructor; eauto.
   (* Ireturn *)
-  econstructor; eauto.
-  inv WTI; simpl. auto. rewrite <- H3. auto.
+  - econstructor; eauto.
+    inv WTI; simpl. auto. rewrite <- H3. auto.
   (* internal function *)
-  simpl in *. inv H5.
-  econstructor; eauto.
-  inv H1. apply wt_init_regs; auto. rewrite wt_params0. auto.
+  - simpl in *. inv H5.
+    econstructor; eauto.
+    inv H1. apply wt_init_regs; auto. rewrite wt_params0. auto.
   (* external function *)
-  econstructor; eauto.
-  eapply external_call_well_typed; eauto.
+  - econstructor; eauto.
+    eapply external_call_well_typed; eauto.
   (* return *)
-  inv H1. econstructor; eauto.
-  apply wt_regset_assign; auto. rewrite H10; auto.
+  - inv H1. econstructor; eauto.
+    apply wt_regset_assign; auto. rewrite H10; auto.
 Qed.
 
 Lemma wt_initial_state:
diff --git a/backend/Renumberproof.v b/backend/Renumberproof.v
index 2e161965..cd3efe73 100644
--- a/backend/Renumberproof.v
+++ b/backend/Renumberproof.v
@@ -162,84 +162,85 @@ Lemma step_simulation:
 Proof.
   induction 1; intros S1' MS; inv MS; try TR_AT.
 (* nop *)
-  econstructor; split. eapply exec_Inop; eauto.
-  constructor; auto. eapply reach_succ; eauto. simpl; auto.
+  - econstructor; split. eapply exec_Inop; eauto.
+    constructor; auto. eapply reach_succ; eauto. simpl; auto.
 (* op *)
-  econstructor; split.
-  eapply exec_Iop; eauto.
-  instantiate (1 := v). rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved.
-  constructor; auto. eapply reach_succ; eauto. simpl; auto.
+  - econstructor; split.
+    eapply exec_Iop; eauto.
+    instantiate (1 := v). rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved.
+    constructor; auto. eapply reach_succ; eauto. simpl; 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. eapply reach_succ; eauto. simpl; 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. eapply reach_succ; eauto. simpl; 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. eapply reach_succ; eauto. simpl; auto.
+  - inv H0.
+    + econstructor; split.
+      * try (eapply exec_Iload; eauto; eapply has_loaded_normal; eauto;
+        rewrite <- EVAL; apply eval_addressing_preserved; exact symbols_preserved).
+      * econstructor; eauto. eapply reach_succ; eauto. simpl; auto.
+    + destruct (eval_addressing) eqn:EVAL in LOAD.
+      * specialize (LOAD v). econstructor; split.
+        -- eapply exec_Iload; eauto. eapply has_loaded_default; eauto.
+           rewrite eval_addressing_preserved with (ge1:=ge).
+           intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'. apply LOAD; auto.
+           exact symbols_preserved.
+        -- econstructor; eauto. eapply reach_succ; eauto. simpl; auto.
+      * econstructor; split.
+        -- eapply exec_Iload; eauto. eapply has_loaded_default; eauto.
+           rewrite eval_addressing_preserved with (ge1:=ge).
+           intros a EVAL'; rewrite EVAL in EVAL'; inv EVAL'.
+           exact symbols_preserved.
+        -- econstructor; eauto. eapply reach_succ; eauto. simpl; auto.
 (* store *)
-  econstructor; split.
-  assert (eval_addressing tge sp addr rs ## args = Some a).
-  rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
-  eapply exec_Istore; eauto.
-  constructor; auto. eapply reach_succ; eauto. simpl; auto.
+  - econstructor; split.
+    assert (eval_addressing tge sp addr rs ## args = Some a).
+    rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
+    eapply exec_Istore; eauto.
+    constructor; auto. eapply reach_succ; eauto. simpl; auto.
 (* call *)
-  econstructor; split.
-  eapply exec_Icall with (fd := transf_fundef fd); eauto.
-    eapply find_function_translated; eauto.
-    apply sig_preserved.
-  constructor. constructor; auto. constructor. eapply reach_succ; eauto. simpl; auto.
+  - econstructor; split.
+    eapply exec_Icall with (fd := transf_fundef fd); eauto.
+      eapply find_function_translated; eauto.
+      apply sig_preserved.
+    constructor. constructor; auto. constructor. eapply reach_succ; eauto. simpl; auto.
 (* tailcall *)
-  econstructor; split.
-  eapply exec_Itailcall with (fd := transf_fundef fd); eauto.
-    eapply find_function_translated; eauto.
-    apply sig_preserved.
-  constructor. auto.
+  - econstructor; split.
+    eapply exec_Itailcall with (fd := transf_fundef fd); eauto.
+      eapply find_function_translated; eauto.
+      apply sig_preserved.
+    constructor. auto.
 (* builtin *)
-  econstructor; split.
-  eapply exec_Ibuiltin; eauto.
-    eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
-    eapply external_call_symbols_preserved; eauto. apply senv_preserved.
-  constructor; auto. eapply reach_succ; eauto. simpl; auto.
+  - econstructor; split.
+    eapply exec_Ibuiltin; eauto.
+      eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
+      eapply external_call_symbols_preserved; eauto. apply senv_preserved.
+    constructor; auto. eapply reach_succ; eauto. simpl; auto.
 (* cond *)
-  econstructor; split.
-  eapply exec_Icond; eauto.
-  replace (if b then renum_pc (pnum f) ifso else renum_pc (pnum f) ifnot)
-     with (renum_pc (pnum f) (if b then ifso else ifnot)).
-  constructor; auto. eapply reach_succ; eauto. simpl. destruct b; auto.
-  destruct b; auto.
+  - econstructor; split.
+    eapply exec_Icond; eauto.
+    replace (if b then renum_pc (pnum f) ifso else renum_pc (pnum f) ifnot)
+       with (renum_pc (pnum f) (if b then ifso else ifnot)).
+    constructor; auto. eapply reach_succ; eauto. simpl. destruct b; auto.
+    destruct b; auto.
 (* jumptbl *)
-  econstructor; split.
-  eapply exec_Ijumptable; eauto. rewrite list_nth_z_map. rewrite H1. simpl; eauto.
-  constructor; auto. eapply reach_succ; eauto. simpl. eapply list_nth_z_in; eauto.
+  - econstructor; split.
+    eapply exec_Ijumptable; eauto. rewrite list_nth_z_map. rewrite H1. simpl; eauto.
+    constructor; auto. eapply reach_succ; eauto. simpl. eapply list_nth_z_in; eauto.
 (* return *)
-  econstructor; split.
-  eapply exec_Ireturn; eauto.
-  constructor; auto.
+  - econstructor; split.
+    eapply exec_Ireturn; eauto.
+    constructor; auto.
 (* internal function *)
-  simpl. econstructor; split.
-  eapply exec_function_internal; eauto.
-  constructor; auto. unfold reach. constructor.
+  - simpl. econstructor; split.
+    eapply exec_function_internal; eauto.
+    constructor; auto. unfold reach. constructor.
 (* external function *)
-  econstructor; split.
-  eapply exec_function_external; eauto.
-    eapply external_call_symbols_preserved; eauto. apply senv_preserved.
-  constructor; auto.
+  - econstructor; split.
+    eapply exec_function_external; eauto.
+      eapply external_call_symbols_preserved; eauto. apply senv_preserved.
+    constructor; auto.
 (* return *)
-  inv STACKS. inv H1.
-  econstructor; split.
-  eapply exec_return; eauto.
-  constructor; auto.
+  - inv STACKS. inv H1.
+    econstructor; split.
+    eapply exec_return; eauto.
+    constructor; auto.
 Qed.
 
 Lemma transf_initial_states:
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.
diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v
index 476208b0..ce9c7a86 100644
--- a/backend/Unusedglobproof.v
+++ b/backend/Unusedglobproof.v
@@ -910,50 +910,52 @@ Proof.
   econstructor; eauto. apply set_reg_inject; auto.
 
 - (* load *)
-  assert (A: exists ta,
-               eval_addressing tge (Vptr tsp Ptrofs.zero) addr trs##args = Some ta
-            /\ Val.inject j a ta).
-  { apply eval_addressing_inj with (ge1 := ge) (sp1 := Vptr sp0 Ptrofs.zero) (vl1 := rs##args).
-    intros. apply symbol_address_inject. eapply match_stacks_preserves_globals; eauto.
-    apply KEPT. red. exists pc, (Iload trap chunk addr args dst pc'); auto.
-    econstructor; eauto.
-    apply regs_inject; auto.
-    assumption. }
-  destruct A as (ta & B & C).
-  exploit Mem.loadv_inject; eauto. intros (tv & D & E).
-  econstructor; split. eapply exec_Iload; eauto.
-  econstructor; eauto. apply set_reg_inject; auto.
-
-- (* load notrap1 *)
-  assert (eval_addressing tge (Vptr tsp Ptrofs.zero) addr trs##args = None).
-  { eapply eval_addressing_inj_none.
-    intros. apply symbol_address_inject. eapply match_stacks_preserves_globals; eauto.
-    apply KEPT. red. exists pc, (Iload NOTRAP chunk addr args dst pc'); auto.
-    econstructor; eauto.
-    rewrite Ptrofs.add_zero; reflexivity.
-    apply regs_inject; auto.
-    eassumption.
-    assumption. }
- 
-  econstructor; split. eapply exec_Iload_notrap1; eauto.
-  econstructor; eauto. apply set_reg_inject; auto.
-
-- (* load notrap2 *)
-  assert (A: exists ta,
-               eval_addressing tge (Vptr tsp Ptrofs.zero) addr trs##args = Some ta
-            /\ Val.inject j a ta).
-  { apply eval_addressing_inj with (ge1 := ge) (sp1 := Vptr sp0 Ptrofs.zero) (vl1 := rs##args).
-    intros. apply symbol_address_inject. eapply match_stacks_preserves_globals; eauto.
-    apply KEPT. red. exists pc, (Iload NOTRAP chunk addr args dst pc'); auto.
-    econstructor; eauto.
-    apply regs_inject; auto.
-    assumption. }
-  destruct A as (ta & B & C).
-  destruct (Mem.loadv chunk tm ta) eqn:Echunk2.
-  + econstructor; split. eapply exec_Iload; eauto.
-    econstructor; eauto. apply set_reg_inject; auto.
-  + econstructor; split. eapply exec_Iload_notrap2; eauto.
+  inv H0.
+  + assert (A: exists ta,
+                 eval_addressing tge (Vptr tsp Ptrofs.zero) addr trs##args = Some ta
+              /\ Val.inject j a ta).
+    { apply eval_addressing_inj with (ge1 := ge) (sp1 := Vptr sp0 Ptrofs.zero) (vl1 := rs##args).
+      intros. apply symbol_address_inject. eapply match_stacks_preserves_globals; eauto.
+      apply KEPT. red. exists pc, (Iload trap chunk addr args dst pc'); auto.
+      econstructor; eauto.
+      apply regs_inject; auto.
+      assumption. }
+    destruct A as (ta & B & C).
+    exploit Mem.loadv_inject; eauto. intros (tv & D & E).
+    econstructor; split. eapply exec_Iload; eauto. eapply has_loaded_normal; eauto.
     econstructor; eauto. apply set_reg_inject; auto.
+  + destruct (eval_addressing) eqn:EVAL in LOAD.
+    * specialize (LOAD v).
+      assert (A: exists ta,
+                   eval_addressing tge (Vptr tsp Ptrofs.zero) addr trs##args = Some ta
+                /\ Val.inject j v ta).
+      { apply eval_addressing_inj with (ge1 := ge) (sp1 := Vptr sp0 Ptrofs.zero) (vl1 := rs##args).
+        intros. apply symbol_address_inject. eapply match_stacks_preserves_globals; eauto.
+        apply KEPT. red. exists pc, (Iload NOTRAP chunk addr args dst pc'); auto.
+        econstructor; eauto.
+        apply regs_inject; auto.
+        assumption. }
+      destruct A as (ta & B & C).
+      destruct (Mem.loadv chunk tm ta) eqn:Echunk2.
+      ** econstructor; split. eapply exec_Iload; eauto. eapply has_loaded_normal; eauto.
+         econstructor; eauto. apply set_reg_inject; auto.
+      ** econstructor; split. eapply exec_Iload; eauto. eapply has_loaded_default; eauto.
+         intros a EVAL'; rewrite B in EVAL'; inv EVAL'. auto.
+         econstructor; eauto. apply set_reg_inject; auto.
+    * assert (eval_addressing tge (Vptr tsp Ptrofs.zero) addr trs##args = None).
+      { eapply eval_addressing_inj_none.
+        intros. apply symbol_address_inject. eapply match_stacks_preserves_globals; eauto.
+        apply KEPT. red. exists pc, (Iload NOTRAP chunk addr args dst pc'); auto.
+        econstructor; eauto.
+        rewrite Ptrofs.add_zero; reflexivity.
+        apply regs_inject; auto.
+        eassumption.
+        assumption. }
+     
+      econstructor; split. eapply exec_Iload; eauto. eapply has_loaded_default; eauto.
+      intros a EVAL'; rewrite H0 in EVAL'; inv EVAL'.
+      econstructor; eauto. apply set_reg_inject; auto.
+
 - (* store *)
   assert (A: exists ta,
                eval_addressing tge (Vptr tsp Ptrofs.zero) addr trs##args = Some ta
diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v
index e20edff7..c112d69e 100644
--- a/backend/ValueAnalysis.v
+++ b/backend/ValueAnalysis.v
@@ -1272,7 +1272,7 @@ Proof.
   apply ematch_update; auto. eapply eval_static_operation_sound; eauto with va.
 
 - (* load *)
-  destruct trap.
+  destruct trap; inv H0.
   + eapply sound_succ_state; eauto. simpl; auto.
     unfold transfer; rewrite H. eauto.
     apply ematch_update; auto. eapply loadv_sound; eauto with va.
@@ -1283,16 +1283,9 @@ Proof.
     eapply vmatch_top.
     eapply loadv_sound; try eassumption.
     eapply eval_static_addressing_sound; eauto with va.
-- (* load notrap1 *)
-  eapply sound_succ_state; eauto. simpl; auto.
-  unfold transfer; rewrite H. eauto.
-  apply ematch_update; auto.
-  constructor.
-- (* load notrap2 *)
-  eapply sound_succ_state; eauto. simpl; auto.
-  unfold transfer; rewrite H. eauto.
-  apply ematch_update; auto.
-  constructor.
+  + eapply sound_succ_state; eauto. simpl; auto.
+    unfold transfer; rewrite H. eauto.
+    apply ematch_update; auto. econstructor.
 - (* store *)
   exploit eval_static_addressing_sound; eauto with va. intros VMADDR.
   eapply sound_succ_state; eauto. simpl; auto.