Merge branch 'RTL_has_loaded' into kvx-work

1 files changed, 41 insertions, 42 deletions

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: