fixes for ARM

5 files changed, 74 insertions, 21 deletions

diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml
index a4ec0c5d..5d5779d4 100644
--- a/arm/Asmexpand.ml
+++ b/arm/Asmexpand.ml
@@ -18,7 +18,6 @@ open Asm
 open Asmexpandaux
 open AST
 open Camlcoq
-open Integers
 
 exception Error of string
 
@@ -104,7 +103,7 @@ let memcpy_small_arg sz arg tmp =
       (r, _0)
   | BA_addrstack ofs ->
       if offset_in_range ofs
-      && offset_in_range (Int.add ofs (Int.repr (Z.of_uint sz)))
+      && offset_in_range (Integers.Int.add ofs (Integers.Int.repr (Z.of_uint sz)))
       then (IR13, ofs)
       else begin expand_addimm tmp IR13 ofs; (tmp, _0) end
   | _ ->
@@ -119,19 +118,19 @@ let expand_builtin_memcpy_small sz al src dst =
     if sz >= 8 && al >= 4 && !Clflags.option_ffpu then begin
       emit (Pfldd (FR7,rsrc,osrc));
       emit (Pfstd (FR7,rdst,odst));
-      copy (Int.add osrc _8) (Int.add odst _8) (sz - 8)
+      copy (Integers.Int.add osrc _8) (Integers.Int.add odst _8) (sz - 8)
     end else if sz >= 4 && al >= 4 then begin
       emit (Pldr (IR14,rsrc,SOimm osrc));
       emit (Pstr (IR14,rdst,SOimm odst));
-      copy (Int.add osrc _4) (Int.add odst _4) (sz - 4)
+      copy (Integers.Int.add osrc _4) (Integers.Int.add odst _4) (sz - 4)
     end else if sz >= 2 && al >= 2 then begin
       emit (Pldrh (IR14,rsrc,SOimm osrc));
       emit (Pstrh (IR14,rdst,SOimm odst));
-      copy (Int.add osrc _2) (Int.add odst _2) (sz - 2)
+      copy (Integers.Int.add osrc _2) (Integers.Int.add odst _2) (sz - 2)
     end else if sz >= 1 then begin
       emit (Pldrb (IR14,rsrc,SOimm osrc));
       emit (Pstrb (IR14,rdst,SOimm odst));
-      copy (Int.add osrc _1) (Int.add odst _1) (sz - 1)
+      copy (Integers.Int.add osrc _1) (Integers.Int.add odst _1) (sz - 1)
     end in
   copy osrc odst sz
 
@@ -188,8 +187,8 @@ let expand_builtin_vload_common chunk base ofs res =
   | Mint32, BR(IR res) ->
      emit (Pldr (res, base, SOimm ofs))
   | Mint64, BR_splitlong(BR(IR res1), BR(IR res2)) ->
-     let ofs_hi = if Archi.big_endian then ofs else Int.add ofs _4 in
-     let ofs_lo = if Archi.big_endian then Int.add ofs _4 else ofs in
+     let ofs_hi = if Archi.big_endian then ofs else Integers.Int.add ofs _4 in
+     let ofs_lo = if Archi.big_endian then Integers.Int.add ofs _4 else ofs in
      if base <> res2 then begin
 	 emit (Pldr (res2, base, SOimm ofs_lo));
 	 emit (Pldr (res1, base, SOimm ofs_hi))
@@ -209,7 +208,7 @@ let expand_builtin_vload chunk args res =
   | [BA(IR addr)] ->
       expand_builtin_vload_common chunk addr _0 res
   | [BA_addrstack ofs] ->
-      if offset_in_range (Int.add ofs (Memdata.size_chunk chunk)) then
+      if offset_in_range (Integers.Int.add ofs (Memdata.size_chunk chunk)) then
         expand_builtin_vload_common chunk IR13 ofs res
       else begin
         expand_addimm IR14 IR13 ofs;
@@ -219,7 +218,7 @@ let expand_builtin_vload chunk args res =
       emit (Ploadsymbol (IR14,id,ofs));
       expand_builtin_vload_common chunk IR14 _0 res
   | [BA_addptr(BA(IR addr), BA_int ofs)] ->
-      if offset_in_range (Int.add ofs (Memdata.size_chunk chunk)) then
+      if offset_in_range (Integers.Int.add ofs (Memdata.size_chunk chunk)) then
         expand_builtin_vload_common chunk addr ofs res
       else begin
         expand_addimm IR14 addr ofs;
@@ -237,8 +236,8 @@ let expand_builtin_vstore_common chunk base ofs src =
   | Mint32, BA(IR src) ->
      emit (Pstr (src, base, SOimm ofs))
   | Mint64, BA_splitlong(BA(IR src1), BA(IR src2)) ->
-     let ofs_hi = if Archi.big_endian then ofs else Int.add ofs _4 in
-     let ofs_lo = if Archi.big_endian then Int.add ofs _4 else ofs in
+     let ofs_hi = if Archi.big_endian then ofs else Integers.Int.add ofs _4 in
+     let ofs_lo = if Archi.big_endian then Integers.Int.add ofs _4 else ofs in
      emit (Pstr (src2, base, SOimm ofs_lo));
      emit (Pstr (src1, base, SOimm ofs_hi))
   | Mfloat32, BA(FR src) ->
@@ -253,7 +252,7 @@ let expand_builtin_vstore chunk args =
   | [BA(IR addr); src] ->
       expand_builtin_vstore_common chunk addr _0 src
   | [BA_addrstack ofs; src] ->
-      if offset_in_range (Int.add ofs (Memdata.size_chunk chunk)) then
+      if offset_in_range (Integers.Int.add ofs (Memdata.size_chunk chunk)) then
         expand_builtin_vstore_common chunk IR13 ofs src
       else begin
         expand_addimm IR14 IR13 ofs;
@@ -263,7 +262,7 @@ let expand_builtin_vstore chunk args =
       emit (Ploadsymbol (IR14,id,ofs));
       expand_builtin_vstore_common chunk IR14 _0 src
   | [BA_addptr(BA(IR addr), BA_int ofs); src] ->
-      if offset_in_range (Int.add ofs (Memdata.size_chunk chunk)) then
+      if offset_in_range (Integers.Int.add ofs (Memdata.size_chunk chunk)) then
         expand_builtin_vstore_common chunk addr ofs src
       else begin
         expand_addimm IR14 addr ofs;
diff --git a/arm/Asmgen.v b/arm/Asmgen.v
index 1a1e7f2f..016a1c5a 100644
--- a/arm/Asmgen.v
+++ b/arm/Asmgen.v
@@ -689,8 +689,12 @@ Definition transl_memory_access_float
     None
     mk_immed addr args k.
 
-Definition transl_load (chunk: memory_chunk) (addr: addressing)
-                       (args: list mreg) (dst: mreg) (k: code) :=
+Definition transl_load (trap : trapping_mode)
+           (chunk: memory_chunk) (addr: addressing)
+           (args: list mreg) (dst: mreg) (k: code) :=
+  match trap with
+  | NOTRAP => Error (msg "Asmgen.transl_load non-trapping loads unsupported on Arm")
+  | TRAP =>
   match chunk with
   | Mint8signed =>
       transl_memory_access_int Pldrsb mk_immed_mem_small dst addr args k
@@ -708,6 +712,7 @@ Definition transl_load (chunk: memory_chunk) (addr: addressing)
       transl_memory_access_float Pfldd mk_immed_mem_float dst addr args k
   | _ =>
       Error (msg "Asmgen.transl_load")
+  end
   end.
 
 Definition transl_store (chunk: memory_chunk) (addr: addressing)
@@ -747,8 +752,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction)
           else loadind_int IR13 f.(fn_link_ofs) IR12 c)
   | Mop op args res =>
       transl_op op args res k
-  | Mload chunk addr args dst =>
-      transl_load chunk addr args dst k
+  | Mload trap chunk addr args dst =>
+      transl_load trap chunk addr args dst k
   | Mstore chunk addr args src =>
       transl_store chunk addr args src k
   | Mcall sig (inl arg) =>
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v
index 25f91d23..92ae524f 100644
--- a/arm/Asmgenproof.v
+++ b/arm/Asmgenproof.v
@@ -303,6 +303,7 @@ Proof.
     eapply tail_nolabel_trans. 2: eapply loadind_label; eauto. unfold loadind_int; TailNoLabel.
   eapply transl_op_label; eauto.
   unfold transl_load, transl_memory_access_int, transl_memory_access_float in H.
+  destruct t; try discriminate.
   destruct m; monadInv H; eapply transl_memory_access_label; eauto; simpl; auto.
   unfold transl_store, transl_memory_access_int, transl_memory_access_float in H.
   destruct m; monadInv H; eapply transl_memory_access_label; eauto; simpl; auto.
@@ -618,6 +619,12 @@ Opaque loadind.
   split. eapply agree_set_undef_mreg; eauto. congruence.
   simpl; congruence.
 
+- (* Mload notrap1 *)
+  inv AT. simpl in *. unfold bind in *. destruct (transl_code _ _ _) in *; discriminate.
+
+- (* Mload notrap *)
+  inv AT. simpl in *. unfold bind in *. destruct (transl_code _ _ _) in *; discriminate.
+
 - (* Mstore *)
   assert (eval_addressing tge sp addr rs##args = Some a).
     rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved.
diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v
index 807e069d..7ef7b776 100644
--- a/arm/Asmgenproof1.v
+++ b/arm/Asmgenproof1.v
@@ -1540,8 +1540,8 @@ Proof.
 Qed.
 
 Lemma transl_load_correct:
-  forall chunk addr args dst k c (rs: regset) a m v,
-  transl_load chunk addr args dst k = OK c ->
+  forall trap chunk addr args dst k c (rs: regset) a m v,
+  transl_load trap chunk addr args dst k = OK c ->
   eval_addressing ge (rs#SP) addr (map rs (map preg_of args)) = Some a ->
   Mem.loadv chunk m a = Some v ->
   exists rs',
@@ -1549,7 +1549,9 @@ Lemma transl_load_correct:
    /\ rs'#(preg_of dst) = v
    /\ forall r, data_preg r = true -> r <> preg_of dst -> rs'#r = rs#r.
 Proof.
-  intros. destruct chunk; simpl in H.
+  intros.
+  destruct trap; try (simpl in *; discriminate).
+  destruct chunk; simpl in H.
   eapply transl_load_int_correct; eauto.
   eapply transl_load_int_correct; eauto.
   eapply transl_load_int_correct; eauto.
diff --git a/arm/Op.v b/arm/Op.v
index cc90e043..9de365e9 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -975,6 +975,20 @@ Proof.
   apply Val.offset_ptr_inject; auto.
 Qed.
 
+Lemma eval_addressing_inj_none:
+  forall addr sp1 vl1 sp2 vl2,
+  (forall id ofs,
+      In id (globals_addressing addr) ->
+      Val.inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) ->
+  Val.inject f sp1 sp2 ->
+  Val.inject_list f vl1 vl2 ->
+  eval_addressing ge1 sp1 addr vl1 = None ->
+  eval_addressing ge2 sp2 addr vl2 = None.
+Proof.
+  intros until vl2. intros Hglobal Hinjsp Hinjvl.
+  destruct addr; simpl in *;
+  inv Hinjvl; trivial; try discriminate; inv H0; trivial; try discriminate; inv H2; trivial; try discriminate.
+Qed.
 End EVAL_COMPAT.
 
 (** Compatibility of the evaluation functions with the ``is less defined'' relation over values. *)
@@ -1080,6 +1094,19 @@ Proof.
   destruct H1 as [v2 [A B]]. exists v2; split; auto. rewrite val_inject_lessdef; auto.
 Qed.
 
+Lemma eval_addressing_lessdef_none:
+  forall sp addr vl1 vl2,
+  Val.lessdef_list vl1 vl2 ->
+  eval_addressing genv sp addr vl1 = None ->
+  eval_addressing genv sp addr vl2 = None.
+Proof.
+  intros. rewrite val_inject_list_lessdef in H.
+  eapply eval_addressing_inj_none with (sp1 := sp).
+  intros. rewrite <- val_inject_lessdef; auto.
+  rewrite <- val_inject_lessdef; auto.
+  eauto. auto.
+Qed.
+
 End EVAL_LESSDEF.
 
 (** Compatibility of the evaluation functions with memory injections. *)
@@ -1132,6 +1159,19 @@ Proof.
   econstructor; eauto. rewrite Ptrofs.add_zero_l; auto.
 Qed.
 
+Lemma eval_addressing_inject_none:
+  forall addr vl1 vl2,
+  Val.inject_list f vl1 vl2 ->
+  eval_addressing genv (Vptr sp1 Ptrofs.zero) addr vl1 = None ->
+  eval_addressing genv (Vptr sp2 Ptrofs.zero) (shift_stack_addressing delta addr) vl2 = None.
+Proof.
+  intros.
+  rewrite eval_shift_stack_addressing.
+  eapply eval_addressing_inj_none with (sp1 := Vptr sp1 Ptrofs.zero); eauto.
+  intros. apply symbol_address_inject.
+  econstructor; eauto. rewrite Ptrofs.add_zero_l; auto. 
+Qed.
+
 Lemma eval_operation_inject:
   forall op vl1 vl2 v1 m1 m2,
   Val.inject_list f vl1 vl2 ->