1 files changed, 67 insertions, 66 deletions
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: