being more archi-independant

8 files changed, 19 insertions, 22 deletions

diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v
index 305e8eeb..be64a1a7 100644
--- a/backend/Deadcodeproof.v
+++ b/backend/Deadcodeproof.v
@@ -822,9 +822,8 @@ Ltac UseTransfer :=
   intros. apply nlive_add with bc i; assumption.
   intros (tv & P & Q).
   econstructor; split.
-  eapply exec_Iload; eauto. eapply has_loaded_normal; eauto.
-  rewrite <- U. apply eval_addressing_preserved. exact symbols_preserved.
-  eauto.
+  try (eapply exec_Iload; eauto; eapply has_loaded_normal; eauto;
+  [ rewrite <- U; apply eval_addressing_preserved; exact symbols_preserved | 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.
@@ -851,10 +850,8 @@ Ltac UseTransfer :=
   destruct (Mem.loadv chunk tm ta) eqn:Hchunk2.
   {
   econstructor; split.
-  eapply exec_Iload. eauto. eapply has_loaded_normal; eauto.
-  erewrite eval_addressing_preserved with (ge1 := ge).
-  assumption.
-  exact symbols_preserved.
+  try (eapply exec_Iload; eauto; eapply has_loaded_normal; eauto;
+  erewrite eval_addressing_preserved with (ge1 := ge); [ assumption | exact symbols_preserved]).
   eapply match_succ_states; eauto. simpl; auto.
   apply eagree_update; eauto 2 with na.
   eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto.
diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v
index c4270e46..5752f5d2 100644
--- a/backend/Duplicateproof.v
+++ b/backend/Duplicateproof.v
@@ -416,7 +416,7 @@ Proof.
     destruct DUPLIC as (i' & H2 & H3). inv H3.
     pose symbols_preserved as SYMPRES. inv H0.
     + eexists; split.
-      * eapply exec_Iload; eauto. eapply has_loaded_normal; eauto. erewrite eval_addressing_preserved; eauto.
+      * 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.
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v
index a4bf838e..647938f3 100644
--- a/backend/Inliningproof.v
+++ b/backend/Inliningproof.v
@@ -992,8 +992,8 @@ Proof.
       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. eapply has_loaded_normal; eauto.
-            try (rewrite <- P; apply eval_addressing_preserved; exact symbols_preserved).
+         ++ 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.
diff --git a/backend/ProfilingExploitproof.v b/backend/ProfilingExploitproof.v
index 292acc2a..4308b670 100644
--- a/backend/ProfilingExploitproof.v
+++ b/backend/ProfilingExploitproof.v
@@ -128,8 +128,8 @@ Proof.
 (* load *)
 - inv H0.
   + econstructor; split.
-    * eapply exec_Iload; eauto. eapply has_loaded_normal; eauto.
-      rewrite <- EVAL. apply eval_addressing_preserved. exact symbols_preserved.
+    * 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.
diff --git a/backend/RTLTunnelingproof.v b/backend/RTLTunnelingproof.v
index 2cef08e2..aa21fc06 100644
--- a/backend/RTLTunnelingproof.v
+++ b/backend/RTLTunnelingproof.v
@@ -461,7 +461,7 @@ Proof.
       left. eexists. split.
       * eapply exec_Iload.
         -- exploit instruction_type_preserved; (simpl; eauto)||congruence.
-        -- eapply has_loaded_normal; eauto. rewrite <- EVAL'. apply eval_addressing_preserved. apply symbols_preserved.
+        -- 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).
@@ -473,7 +473,7 @@ Proof.
         -- left; eexists; split.
            eapply exec_Iload.
            ++ exploit instruction_type_preserved; (simpl; eauto)||congruence.
-           ++ eapply has_loaded_normal; eauto. rewrite <- ADDR. apply eval_addressing_preserved. apply symbols_preserved.
+           ++ 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.
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index 59d0a451..2b1349d2 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -586,8 +586,8 @@ Proof.
   exists (rs1#rd <- v'); exists tm1.
 (* Exec *)
   split. eapply star_right. eexact EX1. eapply exec_Iload. eauto.
-  econstructor; eauto. rewrite <- H3.
-  apply eval_addressing_preserved. exact symbols_preserved.
+  econstructor; eauto. try (rewrite <- H3;
+  apply eval_addressing_preserved; exact symbols_preserved).
   auto.
 (* Match-env *)
   split. eauto with rtlg.
diff --git a/backend/Renumberproof.v b/backend/Renumberproof.v
index 7c7bc7e3..cd3efe73 100644
--- a/backend/Renumberproof.v
+++ b/backend/Renumberproof.v
@@ -172,8 +172,8 @@ Proof.
 (* load *)
   - inv H0.
     + econstructor; split.
-      * eapply exec_Iload; eauto. eapply has_loaded_normal; eauto.
-        rewrite <- EVAL. apply eval_addressing_preserved. exact symbols_preserved.
+      * 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.
diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v
index c8107ad6..4eb0ba23 100644
--- a/backend/Tailcallproof.v
+++ b/backend/Tailcallproof.v
@@ -433,16 +433,16 @@ Proof.
     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; eauto. eapply has_loaded_normal; eauto.
-      rewrite <- EVAL'. apply eval_addressing_preserved. exact symbols_preserved.
+    * 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.
-         ++ eapply exec_Iload; eauto. eapply has_loaded_normal; eauto.
-            erewrite eval_addressing_preserved; eauto. exact symbols_preserved.
+         ++ 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.