finish merge

3 files changed, 32 insertions, 14 deletions

diff --git a/backend/Duplicate.v b/backend/Duplicate.v
index 3ad37c83..46f0855d 100644
--- a/backend/Duplicate.v
+++ b/backend/Duplicate.v
@@ -72,17 +72,19 @@ Definition verify_match_inst dupmap inst tinst :=
           else Error(msg "Different operations in Iop")
       | _ => Error(msg "verify_match_inst Inop") end
 
-  | Iload m a lr r n => match tinst with
-      | Iload m' a' lr' r' n' =>
+  | Iload tm m a lr r n => match tinst with
+      | Iload tm' m' a' lr' r' n' =>
           do u <- verify_is_copy dupmap n n';
-          if (chunk_eq m m') then
-            if (eq_addressing a a') then
-              if (list_eq_dec Pos.eq_dec lr lr') then
-                if (Pos.eq_dec r r') then OK tt
-                else Error (msg "Different r in Iload")
-              else Error (msg "Different lr in Iload")
-            else Error (msg "Different addressing in Iload")
-          else Error (msg "Different mchunk in Iload")
+          if (trapping_mode_eq tm tm') then
+            if (chunk_eq m m') then
+              if (eq_addressing a a') then
+                if (list_eq_dec Pos.eq_dec lr lr') then
+                  if (Pos.eq_dec r r') then OK tt
+                  else Error (msg "Different r in Iload")
+                else Error (msg "Different lr in Iload")
+              else Error (msg "Different addressing in Iload")
+            else Error (msg "Different mchunk in Iload")
+          else Error (msg "Different trapping_mode in Iload")
       | _ => Error (msg "verify_match_inst Iload") end
 
   | Istore m a lr r n => match tinst with
@@ -195,4 +197,4 @@ Definition transf_fundef (f: fundef) : res fundef :=
   transf_partial_fundef transf_function f.
 
 Definition transf_program (p: program) : res program :=
-  transform_partial_program transf_fundef p.
\ No newline at end of file
+  transform_partial_program transf_fundef p.
diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v
index 39b7a353..e66a1068 100644
--- a/backend/Duplicateproof.v
+++ b/backend/Duplicateproof.v
@@ -13,8 +13,8 @@ Inductive match_inst (dupmap: PTree.t node): instruction -> instruction -> Prop
       dupmap!n' = (Some n) -> match_inst dupmap (Inop n) (Inop n')
   | match_inst_op: forall n n' op lr r,
       dupmap!n' = (Some n) -> match_inst dupmap (Iop op lr r n) (Iop op lr r n')
-  | match_inst_load: forall n n' m a lr r,
-      dupmap!n' = (Some n) -> match_inst dupmap (Iload m a lr r n) (Iload m a lr r n')
+  | match_inst_load: forall n n' tm m a lr r,
+      dupmap!n' = (Some n) -> match_inst dupmap (Iload tm m a lr r n) (Iload tm m a lr r n')
   | match_inst_store: forall n n' m a lr r,
       dupmap!n' = (Some n) -> match_inst dupmap (Istore m a lr r n) (Istore m a lr r n')
   | match_inst_call: forall n n' s ri lr r,
@@ -137,6 +137,7 @@ Proof.
 (* Iload *)
   - destruct i'; try (inversion H; fail). monadInv H.
     destruct x. eapply verify_is_copy_correct in EQ.
+    destruct (trapping_mode_eq _ _); try discriminate.
     destruct (chunk_eq _ _); try discriminate.
     destruct (eq_addressing _ _); try discriminate.
     destruct (list_eq_dec _ _ _); try discriminate.
@@ -393,6 +394,21 @@ Proof.
     eexists. split.
     + eapply exec_Iload; eauto. 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.
+      
 (* Istore *)
   - eapply dupmap_correct in DUPLIC; eauto.
     destruct DUPLIC as (i' & H2 & H3). inv H3.
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index 994d2652..3fe61470 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -328,7 +328,7 @@ Local Opaque mreg_type.
     change ty_res with (snd (ty_args, ty_res)). rewrite <- TYOP. eapply type_of_operation_sound; eauto.
     red; intros; subst op. simpl in ISMOVE.
     destruct args; try discriminate. destruct args; discriminate.
-    apply wt_undef_regs; auto.
+    (* no longer needed apply wt_undef_regs; auto. *)
 - (* load *)
   simpl in *; InvBooleans.
   econstructor; eauto.