Update ARM port. Not tested yet.

15 files changed, 388 insertions, 271 deletions

diff --git a/arm/Archi.v b/arm/Archi.v
index fedc55f5..64afb3ec 100644
--- a/arm/Archi.v
+++ b/arm/Archi.v
@@ -20,10 +20,19 @@ Require Import ZArith.
 Require Import Fappli_IEEE.
 Require Import Fappli_IEEE_bits.
 
+Definition ptr64 := false.
+
 Parameter big_endian: bool.
 
-Notation align_int64 := 8%Z (only parsing).
-Notation align_float64 := 8%Z (only parsing).
+Definition align_int64 := 8%Z.
+Definition align_float64 := 8%Z.
+
+Definition splitlong := true.
+
+Lemma splitlong_ptr32: splitlong = true -> ptr64 = false.
+Proof.
+  unfold splitlong, ptr64; congruence.
+Qed.
 
 Program Definition default_pl_64 : bool * nan_pl 53 :=
   (false, iter_nat 51 _ xO xH).
@@ -45,7 +54,8 @@ Definition choose_binop_pl_32 (s1: bool) (pl1: nan_pl 24) (s2: bool) (pl2: nan_p
 
 Definition float_of_single_preserves_sNaN := false.
 
-Global Opaque default_pl_64 choose_binop_pl_64
+Global Opaque ptr64 big_endian splitlong
+              default_pl_64 choose_binop_pl_64
               default_pl_32 choose_binop_pl_32
               float_of_single_preserves_sNaN.
 
diff --git a/arm/Asm.v b/arm/Asm.v
index 010d5d7b..d211ead0 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -199,10 +199,10 @@ Inductive instruction : Type :=
   | Pfsts: freg -> ireg -> int -> instruction       (**r float32 store *)
 
   (* Pseudo-instructions *)
-  | Pallocframe: Z -> int -> instruction      (**r allocate new stack frame *)
-  | Pfreeframe: Z -> int -> instruction       (**r deallocate stack frame and restore previous frame *)
+  | Pallocframe: Z -> ptrofs -> instruction      (**r allocate new stack frame *)
+  | Pfreeframe: Z -> ptrofs -> instruction       (**r deallocate stack frame and restore previous frame *)
   | Plabel: label -> instruction                   (**r define a code label *)
-  | Ploadsymbol: ireg -> ident -> int -> instruction (**r load the address of a symbol *)
+  | Ploadsymbol: ireg -> ident -> ptrofs -> instruction (**r load the address of a symbol *)
   | Pmovite: testcond -> ireg -> shift_op -> shift_op -> instruction (**r integer conditional move *)
   | Pbtbl: ireg -> list label -> instruction       (**r N-way branch through a jump table *)
   | Pbuiltin: external_function -> list (builtin_arg preg) -> builtin_res preg -> instruction (**r built-in function (pseudo) *)
@@ -376,7 +376,7 @@ Inductive outcome: Type :=
   instruction ([nextinstr]) or branching to a label ([goto_label]). *)
 
 Definition nextinstr (rs: regset) :=
-  rs#PC <- (Val.add rs#PC Vone).
+  rs#PC <- (Val.offset_ptr rs#PC Ptrofs.one).
 
 Definition nextinstr_nf (rs: regset) :=
   nextinstr (undef_flags rs).
@@ -386,7 +386,7 @@ Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) :=
   | None => Stuck
   | Some pos =>
       match rs#PC with
-      | Vptr b ofs => Next (rs#PC <- (Vptr b (Int.repr pos))) m
+      | Vptr b ofs => Next (rs#PC <- (Vptr b (Ptrofs.repr pos))) m
       | _ => Stuck
     end
   end.
@@ -564,11 +564,11 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       | None => Stuck
       end
   | Pbsymb id sg =>
-      Next (rs#PC <- (Genv.symbol_address ge id Int.zero)) m
+      Next (rs#PC <- (Genv.symbol_address ge id Ptrofs.zero)) m
   | Pbreg r sg =>
       Next (rs#PC <- (rs#r)) m
   | Pblsymb id sg =>
-      Next (rs#IR14 <- (Val.add rs#PC Vone) #PC <- (Genv.symbol_address ge id Int.zero)) m
+      Next (rs#IR14 <- (Val.add rs#PC Vone) #PC <- (Genv.symbol_address ge id Ptrofs.zero)) m
   | Pblreg r sg =>
       Next (rs#IR14 <- (Val.add rs#PC Vone) #PC <- (rs#r)) m
   | Pbic r1 r2 so =>
@@ -716,13 +716,13 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   (* Pseudo-instructions *)
   | Pallocframe sz pos =>
       let (m1, stk) := Mem.alloc m 0 sz in
-      let sp := (Vptr stk Int.zero) in
-      match Mem.storev Mint32 m1 (Val.add sp (Vint pos)) rs#IR13 with
+      let sp := (Vptr stk Ptrofs.zero) in
+      match Mem.storev Mint32 m1 (Val.offset_ptr sp pos) rs#IR13 with
       | None => Stuck
       | Some m2 => Next (nextinstr (rs #IR12 <- (rs#IR13) #IR13 <- sp)) m2
       end
   | Pfreeframe sz pos =>
-      match Mem.loadv Mint32 m (Val.add rs#IR13 (Vint pos)) with
+      match Mem.loadv Mint32 m (Val.offset_ptr rs#IR13 pos) with
       | None => Stuck
       | Some v =>
           match rs#IR13 with
@@ -810,7 +810,7 @@ Inductive extcall_arg (rs: regset) (m: mem): loc -> val -> Prop :=
   | extcall_arg_stack: forall ofs ty bofs v,
       bofs = Stacklayout.fe_ofs_arg + 4 * ofs ->
       Mem.loadv (chunk_of_type ty) m
-                (Val.add (rs (IR IR13)) (Vint (Int.repr bofs))) = Some v ->
+                (Val.offset_ptr (rs (IR IR13)) (Ptrofs.repr bofs)) = Some v ->
       extcall_arg rs m (S Outgoing ofs ty) v.
 
 Inductive extcall_arg_pair (rs: regset) (m: mem): rpair loc -> val -> Prop :=
@@ -839,14 +839,14 @@ Inductive step: state -> trace -> state -> Prop :=
       forall b ofs f i rs m rs' m',
       rs PC = Vptr b ofs ->
       Genv.find_funct_ptr ge b = Some (Internal f) ->
-      find_instr (Int.unsigned ofs) (fn_code f) = Some i ->
+      find_instr (Ptrofs.unsigned ofs) (fn_code f) = Some i ->
       exec_instr f i rs m = Next rs' m' ->
       step (State rs m) E0 (State rs' m')
   | exec_step_builtin:
       forall b ofs f ef args res rs m vargs t vres rs' m',
       rs PC = Vptr b ofs ->
       Genv.find_funct_ptr ge b = Some (Internal f) ->
-      find_instr (Int.unsigned ofs) f.(fn_code) = Some (Pbuiltin ef args res) ->
+      find_instr (Ptrofs.unsigned ofs) f.(fn_code) = Some (Pbuiltin ef args res) ->
       eval_builtin_args ge rs (rs SP) m args vargs ->
       external_call ef ge vargs m t vres m' ->
       rs' = nextinstr
@@ -855,7 +855,7 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State rs m) t (State rs' m')
   | exec_step_external:
       forall b ef args res rs m t rs' m',
-      rs PC = Vptr b Int.zero ->
+      rs PC = Vptr b Ptrofs.zero ->
       Genv.find_funct_ptr ge b = Some (External ef) ->
       external_call ef ge args m t res m' ->
       extcall_arguments rs m (ef_sig ef) args ->
@@ -871,7 +871,7 @@ Inductive initial_state (p: program): state -> Prop :=
       let ge := Genv.globalenv p in
       let rs0 :=
         (Pregmap.init Vundef)
-        # PC <- (Genv.symbol_address ge p.(prog_main) Int.zero)
+        # PC <- (Genv.symbol_address ge p.(prog_main) Ptrofs.zero)
         # IR14 <- Vzero
         # IR13 <- Vzero in
       Genv.init_mem p = Some m0 ->
diff --git a/arm/Asmgen.v b/arm/Asmgen.v
index 90d3b189..bbfad3c9 100644
--- a/arm/Asmgen.v
+++ b/arm/Asmgen.v
@@ -362,7 +362,7 @@ Definition transl_op
       OK (Ploadsymbol r s ofs :: k)
   | Oaddrstack n, nil =>
       do r <- ireg_of res;
-      OK (addimm r IR13 n k)
+      OK (addimm r IR13 (Ptrofs.to_int n) k)
   | Ocast8signed, a1 :: nil =>
       do r <- ireg_of res; do r1 <- ireg_of a1;
       OK (if thumb tt then
@@ -565,10 +565,11 @@ Definition indexed_memory_access
   then mk_instr base n :: k
   else addimm IR14 base (Int.sub n n1) (mk_instr IR14 n1 :: k).
 
-Definition loadind_int (base: ireg) (ofs: int) (dst: ireg) (k: code) :=
-  indexed_memory_access (fun base n => Pldr dst base (SOimm n)) mk_immed_mem_word base ofs k.
+Definition loadind_int (base: ireg) (ofs: ptrofs) (dst: ireg) (k: code) :=
+  indexed_memory_access (fun base n => Pldr dst base (SOimm n)) mk_immed_mem_word base (Ptrofs.to_int ofs) k.
 
-Definition loadind (base: ireg) (ofs: int) (ty: typ) (dst: mreg) (k: code) :=
+Definition loadind (base: ireg) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: code) :=
+  let ofs := Ptrofs.to_int ofs in
   match ty, preg_of dst with
   | Tint, IR r =>
       OK (indexed_memory_access (fun base n => Pldr r base (SOimm n)) mk_immed_mem_word base ofs k)
@@ -584,7 +585,8 @@ Definition loadind (base: ireg) (ofs: int) (ty: typ) (dst: mreg) (k: code) :=
       Error (msg "Asmgen.loadind")
   end.
 
-Definition storeind (src: mreg) (base: ireg) (ofs: int) (ty: typ) (k: code) :=
+Definition storeind (src: mreg) (base: ireg) (ofs: ptrofs) (ty: typ) (k: code) :=
+  let ofs := Ptrofs.to_int ofs in
   match ty, preg_of src with
   | Tint, IR r =>
       OK (indexed_memory_access (fun base n => Pstr r base (SOimm n)) mk_immed_mem_word base ofs k)
@@ -628,7 +630,7 @@ Definition transl_memory_access
           Error (msg "Asmgen.Aindexed2shift")
       end
   | Ainstack n, nil =>
-      OK (indexed_memory_access mk_instr_imm mk_immed IR13 n k)
+      OK (indexed_memory_access mk_instr_imm mk_immed IR13 (Ptrofs.to_int n) k)
   | _, _ =>
       Error(msg "Asmgen.transl_memory_access")
   end.
@@ -788,11 +790,11 @@ Definition transl_function (f: Mach.function) :=
   do c <- transl_code f f.(Mach.fn_code) true;
   OK (mkfunction f.(Mach.fn_sig)
         (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::
-         Pstr IR14 IR13 (SOimm f.(fn_retaddr_ofs)) :: c)).
+         Pstr IR14 IR13 (SOimm (Ptrofs.to_int f.(fn_retaddr_ofs))) :: c)).
 
 Definition transf_function (f: Mach.function) : res Asm.function :=
   do tf <- transl_function f;
-  if zlt Int.max_unsigned (list_length_z tf.(fn_code))
+  if zlt Ptrofs.max_unsigned (list_length_z tf.(fn_code))
   then Error (msg "code size exceeded")
   else OK tf.
 
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v
index 431743c6..ade121c5 100644
--- a/arm/Asmgenproof.v
+++ b/arm/Asmgenproof.v
@@ -18,6 +18,8 @@ Require Import Values Memory Events Globalenvs Smallstep.
 Require Import Op Locations Mach Conventions Asm.
 Require Import Asmgen Asmgenproof0 Asmgenproof1.
 
+Local Transparent Archi.ptr64.
+
 Definition match_prog (p: Mach.program) (tp: Asm.program) :=
   match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp.
 
@@ -64,9 +66,9 @@ Qed.
 
 Lemma transf_function_no_overflow:
   forall f tf,
-  transf_function f = OK tf -> list_length_z (fn_code tf) <= Int.max_unsigned.
+  transf_function f = OK tf -> list_length_z (fn_code tf) <= Ptrofs.max_unsigned.
 Proof.
-  intros. monadInv H. destruct (zlt Int.max_unsigned (list_length_z (fn_code x))); inv EQ0. omega.
+  intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (list_length_z (fn_code x))); inv EQ0. omega.
 Qed.
 
 Lemma exec_straight_exec:
@@ -335,7 +337,7 @@ Lemma transl_find_label:
   | Some c => exists tc, find_label lbl (fn_code tf) = Some tc /\ transl_code f c false = OK tc
   end.
 Proof.
-  intros. monadInv H. destruct (zlt Int.max_unsigned (list_length_z (fn_code x))); inv EQ0.
+  intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (list_length_z (fn_code x))); inv EQ0.
   monadInv EQ. simpl.
   eapply transl_code_label; eauto.
 Qed.
@@ -360,10 +362,10 @@ Proof.
   intros [tc [A B]].
   exploit label_pos_code_tail; eauto. instantiate (1 := 0).
   intros [pos' [P [Q R]]].
-  exists tc; exists (rs#PC <- (Vptr b (Int.repr pos'))).
+  exists tc; exists (rs#PC <- (Vptr b (Ptrofs.repr pos'))).
   split. unfold goto_label. rewrite P. rewrite H1. auto.
   split. rewrite Pregmap.gss. constructor; auto.
-  rewrite Int.unsigned_repr. replace (pos' - 0) with pos' in Q.
+  rewrite Ptrofs.unsigned_repr. replace (pos' - 0) with pos' in Q.
   auto. omega.
   generalize (transf_function_no_overflow _ _ H0). omega.
   intros. apply Pregmap.gso; auto.
@@ -379,7 +381,7 @@ Proof.
 - intros. exploit transl_instr_label; eauto.
   destruct i; try (intros [A B]; apply A). intros. subst c0. repeat constructor.
 - intros. monadInv H0.
-  destruct (zlt Int.max_unsigned (list_length_z (fn_code x))); inv EQ0. monadInv EQ.
+  destruct (zlt Ptrofs.max_unsigned (list_length_z (fn_code x))); inv EQ0. monadInv EQ.
   exists x; exists true; split; auto. repeat constructor.
 - exact transf_function_no_overflow.
 Qed.
@@ -418,7 +420,7 @@ Inductive match_states: Mach.state -> Asm.state -> Prop :=
         (STACKS: match_stack ge s)
         (MEXT: Mem.extends m m')
         (AG: agree ms (parent_sp s) rs)
-        (ATPC: rs PC = Vptr fb Int.zero)
+        (ATPC: rs PC = Vptr fb Ptrofs.zero)
         (ATLR: rs RA = parent_ra s),
       match_states (Mach.Callstate s fb ms m)
                    (Asm.State rs m')
@@ -624,13 +626,13 @@ Opaque loadind.
     eapply transf_function_no_overflow; eauto.
   destruct ros as [rf|fid]; simpl in H; monadInv H5.
 + (* Indirect call *)
-  assert (rs rf = Vptr f' Int.zero).
+  assert (rs rf = Vptr f' Ptrofs.zero).
     destruct (rs rf); try discriminate.
-    revert H; predSpec Int.eq Int.eq_spec i Int.zero; intros; congruence.
-  assert (rs0 x0 = Vptr f' Int.zero).
+    revert H; predSpec Ptrofs.eq Ptrofs.eq_spec i Ptrofs.zero; intros; congruence.
+  assert (rs0 x0 = Vptr f' Ptrofs.zero).
     exploit ireg_val; eauto. rewrite H5; intros LD; inv LD; auto.
   generalize (code_tail_next_int _ _ _ _ NOOV H6). intro CT1.
-  assert (TCA: transl_code_at_pc ge (Vptr fb (Int.add ofs Int.one)) fb f c false tf x).
+  assert (TCA: transl_code_at_pc ge (Vptr fb (Ptrofs.add ofs Ptrofs.one)) fb f c false tf x).
     econstructor; eauto.
   exploit return_address_offset_correct; eauto. intros; subst ra.
   left; econstructor; split.
@@ -644,7 +646,7 @@ Opaque loadind.
   Simpl. rewrite <- H2. auto.
 + (* Direct call *)
   generalize (code_tail_next_int _ _ _ _ NOOV H6). intro CT1.
-  assert (TCA: transl_code_at_pc ge (Vptr fb (Int.add ofs Int.one)) fb f c false tf x).
+  assert (TCA: transl_code_at_pc ge (Vptr fb (Ptrofs.add ofs Ptrofs.one)) fb f c false tf x).
     econstructor; eauto.
   exploit return_address_offset_correct; eauto. intros; subst ra.
   left; econstructor; split.
@@ -660,7 +662,7 @@ Opaque loadind.
 - (* Mtailcall *)
   assert (f0 = f) by congruence.  subst f0.
   inversion AT; subst.
-  assert (NOOV: list_length_z (fn_code tf) <= Int.max_unsigned).
+  assert (NOOV: list_length_z (fn_code tf) <= Ptrofs.max_unsigned).
     eapply transf_function_no_overflow; eauto.
   exploit Mem.loadv_extends. eauto. eexact H1. auto.
   unfold chunk_of_type. rewrite (sp_val _ _ _ AG). intros [parent' [A B]].
@@ -682,16 +684,16 @@ Opaque loadind.
     exploit loadind_int_correct. eexact C. intros [rs1 [P [Q R]]].
     econstructor; split.
     eapply exec_straight_trans. eexact P. apply exec_straight_one.
-    simpl. rewrite R; auto with asmgen. unfold chunk_of_type in A. rewrite A.
+    simpl. rewrite R; auto with asmgen. unfold chunk_of_type in A; simpl in A. rewrite A.
     rewrite <- (sp_val _ _ _ AG). rewrite E. eauto. auto.
     split. Simpl. split. Simpl. intros. Simpl.
   }
   destruct ros as [rf|fid]; simpl in H; monadInv H7.
 + (* Indirect call *)
-  assert (rs rf = Vptr f' Int.zero).
+  assert (rs rf = Vptr f' Ptrofs.zero).
     destruct (rs rf); try discriminate.
-    revert H; predSpec Int.eq Int.eq_spec i Int.zero; intros; congruence.
-  assert (rs0 x0 = Vptr f' Int.zero).
+    revert H; predSpec Ptrofs.eq Ptrofs.eq_spec i Ptrofs.zero; intros; congruence.
+  assert (rs0 x0 = Vptr f' Ptrofs.zero).
     exploit ireg_val; eauto. rewrite H7; intros LD; inv LD; auto.
   destruct (X (Pbreg x0 sig :: x)) as [rs2 [P [Q [R S]]]].
   exploit exec_straight_steps_2. eexact P. eauto. eauto. eapply functions_transl; eauto. eauto.
@@ -850,7 +852,7 @@ Opaque loadind.
 - (* internal function *)
   exploit functions_translated; eauto. intros [tf [A B]]. monadInv B.
   generalize EQ; intros EQ'. monadInv EQ'.
-  destruct (zlt Int.max_unsigned (list_length_z (fn_code x0))); inversion EQ1. clear EQ1.
+  destruct (zlt Ptrofs.max_unsigned (list_length_z (fn_code x0))); inversion EQ1. clear EQ1.
   monadInv EQ0.
   unfold store_stack in *.
   exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl.
@@ -860,24 +862,27 @@ Opaque loadind.
   exploit Mem.storev_extends. eexact G. eexact H2. eauto. eauto.
   intros [m3' [P Q]].
   (* Execution of function prologue *)
-  set (rs2 := nextinstr (rs0#IR12 <- (parent_sp s) #IR13 <- (Vptr stk Int.zero))).
+  set (rs2 := nextinstr (rs0#IR12 <- (parent_sp s) #IR13 <- (Vptr stk Ptrofs.zero))).
   set (rs3 := nextinstr rs2).
   assert (EXEC_PROLOGUE:
             exec_straight tge x
               (fn_code x) rs0 m'
               x1 rs3 m3').
-  rewrite <- H5 at 2; unfold fn_code.
+  replace (fn_code x)
+  with (Pallocframe (fn_stacksize f) (fn_link_ofs f) :: Pstr IR14 IR13 (SOimm (Ptrofs.to_int (fn_retaddr_ofs f))) :: x1)
+  by (rewrite <- H5; auto).
   apply exec_straight_two with rs2 m2'.
   unfold exec_instr. rewrite C. fold sp.
-  rewrite <- (sp_val _ _ _ AG). unfold chunk_of_type in F. rewrite F. auto.
+  rewrite <- (sp_val _ _ _ AG). unfold Tptr, chunk_of_type, Archi.ptr64 in F. rewrite F. auto.
   simpl. auto.
   simpl. unfold exec_store. change (rs2 IR14) with (rs0 IR14).
-  rewrite Int.add_zero_l. simpl. unfold chunk_of_type in P. simpl in P.
-  rewrite Int.add_zero_l in P. rewrite ATLR. rewrite P. auto. auto. auto.
+  rewrite Ptrofs.add_zero_l. simpl. unfold Tptr, chunk_of_type, Archi.ptr64 in P. simpl in P.
+  rewrite Ptrofs.add_zero_l in P. rewrite ATLR. rewrite Ptrofs.of_int_to_int by auto.
+  rewrite P. auto. auto. auto.
   left; exists (State rs3 m3'); split.
   eapply exec_straight_steps_1; eauto. omega. constructor.
   econstructor; eauto.
-  change (rs3 PC) with (Val.add (Val.add (rs0 PC) Vone) Vone).
+  change (rs3 PC) with (Val.offset_ptr (Val.offset_ptr (rs0 PC) Ptrofs.one) Ptrofs.one).
   rewrite ATPC. simpl. constructor; eauto.
   subst x. eapply code_tail_next_int. omega.
   eapply code_tail_next_int. omega. constructor.
@@ -915,12 +920,12 @@ Proof.
   econstructor; split.
   econstructor.
   eapply (Genv.init_mem_transf_partial TRANSF); eauto.
-  replace (Genv.symbol_address (Genv.globalenv tprog) (prog_main tprog) Int.zero)
-     with (Vptr fb Int.zero).
+  replace (Genv.symbol_address (Genv.globalenv tprog) (prog_main tprog) Ptrofs.zero)
+     with (Vptr fb Ptrofs.zero).
   econstructor; eauto.
   constructor.
   apply Mem.extends_refl.
-  split. auto. simpl. unfold Vzero; congruence. intros. rewrite Regmap.gi. auto.
+  split. auto. simpl. unfold Vnullptr; simpl; congruence. intros. rewrite Regmap.gi. auto.
   unfold Genv.symbol_address.
   rewrite (match_program_main TRANSF).
   rewrite symbols_preserved.
diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v
index 76a7b080..252a294a 100644
--- a/arm/Asmgenproof1.v
+++ b/arm/Asmgenproof1.v
@@ -30,6 +30,8 @@ Require Import Asmgen.
 Require Import Conventions.
 Require Import Asmgenproof0.
 
+Local Transparent Archi.ptr64. 
+
 (** Useful properties of the R14 registers. *)
 
 Lemma ireg_of_not_R14:
@@ -49,7 +51,7 @@ Hint Resolve ireg_of_not_R14': asmgen.
 (** [undef_flags] and [nextinstr_nf] *)
 
 Lemma nextinstr_nf_pc:
-  forall rs, (nextinstr_nf rs)#PC = Val.add rs#PC Vone.
+  forall rs, (nextinstr_nf rs)#PC = Val.offset_ptr rs#PC Ptrofs.one.
 Proof.
   intros. reflexivity.
 Qed.
@@ -520,49 +522,55 @@ Qed.
 
 Lemma loadind_int_correct:
   forall (base: ireg) ofs dst (rs: regset) m v k,
-  Mem.loadv Mint32 m (Val.add rs#base (Vint ofs)) = Some v ->
+  Mem.loadv Mint32 m (Val.offset_ptr rs#base ofs) = Some v ->
   exists rs',
      exec_straight ge fn (loadind_int base ofs dst k) rs m k rs' m
   /\ rs'#dst = v
   /\ forall r, if_preg r = true -> r <> IR14 -> r <> dst -> rs'#r = rs#r.
 Proof.
-  intros; unfold loadind_int. apply indexed_memory_access_correct; intros.
+  intros; unfold loadind_int.
+  assert (Val.offset_ptr (rs base) ofs = Val.add (rs base) (Vint (Ptrofs.to_int ofs))).
+  { destruct (rs base); try discriminate. simpl. f_equal; f_equal. symmetry; auto with ptrofs. }   
+  apply indexed_memory_access_correct; intros.
   econstructor; split.
-  apply exec_straight_one. simpl. unfold exec_load. rewrite H0; rewrite H; eauto. auto.
+  apply exec_straight_one. simpl. unfold exec_load. rewrite H1, <- H0, H. eauto. auto.
   split; intros; Simpl.
 Qed.
 
 Lemma loadind_correct:
   forall (base: ireg) ofs ty dst k c (rs: regset) m v,
   loadind base ofs ty dst k = OK c ->
-  Mem.loadv (chunk_of_type ty) m (Val.add rs#base (Vint ofs)) = Some v ->
+  Mem.loadv (chunk_of_type ty) m (Val.offset_ptr rs#base ofs) = Some v ->
   exists rs',
      exec_straight ge fn c rs m k rs' m
   /\ rs'#(preg_of dst) = v
   /\ forall r, if_preg r = true -> r <> IR14 -> r <> preg_of dst -> rs'#r = rs#r.
 Proof.
-  unfold loadind; intros. destruct ty; destruct (preg_of dst); inv H; simpl in H0.
+  unfold loadind; intros. 
+  assert (Val.offset_ptr (rs base) ofs = Val.add (rs base) (Vint (Ptrofs.to_int ofs))).
+  { destruct (rs base); try discriminate. simpl. f_equal; f_equal. symmetry; auto with ptrofs. }   
+  destruct ty; destruct (preg_of dst); inv H; simpl in H0.
 - (* int *)
   apply loadind_int_correct; auto.
 - (* float *)
   apply indexed_memory_access_correct; intros.
   econstructor; split.
-  apply exec_straight_one. simpl. unfold exec_load. rewrite H. rewrite H0. eauto. auto.
+  apply exec_straight_one. simpl. unfold exec_load. rewrite H, <- H1, H0. eauto. auto.
   split; intros; Simpl.
 - (* single *)
   apply indexed_memory_access_correct; intros.
   econstructor; split.
-  apply exec_straight_one. simpl. unfold exec_load. rewrite H. rewrite H0. eauto. auto.
+  apply exec_straight_one. simpl. unfold exec_load. rewrite H, <- H1, H0. eauto. auto.
   split; intros; Simpl.
 - (* any32 *)
   apply indexed_memory_access_correct; intros.
   econstructor; split.
-  apply exec_straight_one. simpl. unfold exec_load. rewrite H. rewrite H0. eauto. auto.
+  apply exec_straight_one. simpl. unfold exec_load. rewrite H, <- H1, H0. eauto. auto.
   split; intros; Simpl.
 - (* any64 *)
   apply indexed_memory_access_correct; intros.
   econstructor; split.
-  apply exec_straight_one. simpl. unfold exec_load. rewrite H. rewrite H0. eauto. auto.
+  apply exec_straight_one. simpl. unfold exec_load. rewrite H, <- H1, H0. eauto. auto.
   split; intros; Simpl.
 Qed.
 
@@ -571,43 +579,40 @@ Qed.
 Lemma storeind_correct:
   forall (base: ireg) ofs ty src k c (rs: regset) m m',
   storeind src base ofs ty k = OK c ->
-  Mem.storev (chunk_of_type ty) m (Val.add rs#base (Vint ofs)) (rs#(preg_of src)) = Some m' ->
+  Mem.storev (chunk_of_type ty) m (Val.offset_ptr rs#base ofs) (rs#(preg_of src)) = Some m' ->
   exists rs',
      exec_straight ge fn c rs m k rs' m'
   /\ forall r, if_preg r = true -> r <> IR14 -> rs'#r = rs#r.
 Proof.
   unfold storeind; intros.
   assert (DATA: data_preg (preg_of src) = true) by eauto with asmgen.
+  assert (Val.offset_ptr (rs base) ofs = Val.add (rs base) (Vint (Ptrofs.to_int ofs))).
+  { destruct (rs base); try discriminate. simpl. f_equal; f_equal. symmetry; auto with ptrofs. }   
   destruct ty; destruct (preg_of src); inv H; simpl in H0.
 - (* int *)
   apply indexed_memory_access_correct; intros.
   econstructor; split.
-  apply exec_straight_one. simpl. unfold exec_store.
-  rewrite H. rewrite H1; auto with asmgen. rewrite H0; eauto. auto.
+  apply exec_straight_one. simpl. unfold exec_store. rewrite H, <- H1, H2, H0 by auto with asmgen; eauto. auto. 
   intros; Simpl.
 - (* float *)
   apply indexed_memory_access_correct; intros.
   econstructor; split.
-  apply exec_straight_one. simpl. unfold exec_store.
-  rewrite H. rewrite H1; auto with asmgen. rewrite H0; eauto. auto.
+  apply exec_straight_one. simpl. unfold exec_store. rewrite H, <- H1, H2, H0 by auto with asmgen; eauto. auto. 
   intros; Simpl.
 - (* single *)
   apply indexed_memory_access_correct; intros.
   econstructor; split.
-  apply exec_straight_one. simpl. unfold exec_store.
-  rewrite H. rewrite H1; auto with asmgen. rewrite H0; eauto. auto.
+  apply exec_straight_one. simpl. unfold exec_store. rewrite H, <- H1, H2, H0 by auto with asmgen; eauto. auto. 
   intros; Simpl.
 - (* any32 *)
   apply indexed_memory_access_correct; intros.
   econstructor; split.
-  apply exec_straight_one. simpl. unfold exec_store.
-  rewrite H. rewrite H1; auto with asmgen. rewrite H0; eauto. auto.
+  apply exec_straight_one. simpl. unfold exec_store. rewrite H, <- H1, H2, H0 by auto with asmgen; eauto. auto. 
   intros; Simpl.
 - (* any64 *)
   apply indexed_memory_access_correct; intros.
   econstructor; split.
-  apply exec_straight_one. simpl. unfold exec_store.
-  rewrite H. rewrite H1; auto with asmgen. rewrite H0; eauto. auto.
+  apply exec_straight_one. simpl. unfold exec_store. rewrite H, <- H1, H2, H0 by auto with asmgen; eauto. auto. 
   intros; Simpl.
 Qed.
 
@@ -731,32 +736,32 @@ Proof.
   destruct (Int.ltu i i0); reflexivity.
 (* int ptr *)
   destruct (Int.eq i Int.zero &&
-    (Mem.valid_pointer m b0 (Int.unsigned i0) || Mem.valid_pointer m b0 (Int.unsigned i0 - 1))) eqn:?; try discriminate.
+    (Mem.valid_pointer m b0 (Ptrofs.unsigned i0) || Mem.valid_pointer m b0 (Ptrofs.unsigned i0 - 1))) eqn:?; try discriminate.
   destruct c; simpl in *; inv H1.
   rewrite Heqb1; reflexivity.
   rewrite Heqb1; reflexivity.
 (* ptr int *)
   destruct (Int.eq i0 Int.zero &&
-    (Mem.valid_pointer m b0 (Int.unsigned i) || Mem.valid_pointer m b0 (Int.unsigned i - 1))) eqn:?; try discriminate.
+    (Mem.valid_pointer m b0 (Ptrofs.unsigned i) || Mem.valid_pointer m b0 (Ptrofs.unsigned i - 1))) eqn:?; try discriminate.
   destruct c; simpl in *; inv H1.
   rewrite Heqb1; reflexivity.
   rewrite Heqb1; reflexivity.
 (* ptr ptr *)
   simpl.
-  fold (Mem.weak_valid_pointer m b0 (Int.unsigned i)) in *.
-  fold (Mem.weak_valid_pointer m b1 (Int.unsigned i0)) in *.
+  fold (Mem.weak_valid_pointer m b0 (Ptrofs.unsigned i)) in *.
+  fold (Mem.weak_valid_pointer m b1 (Ptrofs.unsigned i0)) in *.
   destruct (eq_block b0 b1).
-  destruct (Mem.weak_valid_pointer m b0 (Int.unsigned i) &&
-            Mem.weak_valid_pointer m b1 (Int.unsigned i0)); inversion H1.
+  destruct (Mem.weak_valid_pointer m b0 (Ptrofs.unsigned i) &&
+            Mem.weak_valid_pointer m b1 (Ptrofs.unsigned i0)); inversion H1.
   destruct c; simpl; auto.
-  destruct (Int.eq i i0); reflexivity.
-  destruct (Int.eq i i0); auto.
-  destruct (Int.ltu i i0); auto.
-  rewrite (int_not_ltu i i0). destruct (Int.ltu i i0); simpl; destruct (Int.eq i i0); auto.
-  rewrite (int_ltu_not i i0). destruct (Int.ltu i i0); destruct (Int.eq i i0); reflexivity.
-  destruct (Int.ltu i i0); reflexivity.
-  destruct (Mem.valid_pointer m b0 (Int.unsigned i) &&
-            Mem.valid_pointer m b1 (Int.unsigned i0)); try discriminate.
+  destruct (Ptrofs.eq i i0); reflexivity.
+  destruct (Ptrofs.eq i i0); auto.
+  destruct (Ptrofs.ltu i i0); auto.
+  rewrite (Ptrofs.not_ltu i i0). destruct (Ptrofs.ltu i i0); simpl; destruct (Ptrofs.eq i i0); auto.
+  rewrite (Ptrofs.ltu_not i i0). destruct (Ptrofs.ltu i i0); destruct (Ptrofs.eq i i0); reflexivity.
+  destruct (Ptrofs.ltu i i0); reflexivity.
+  destruct (Mem.valid_pointer m b0 (Ptrofs.unsigned i) &&
+            Mem.valid_pointer m b1 (Ptrofs.unsigned i0)); try discriminate.
   destruct c; simpl in *; inv H1; reflexivity.
 Qed.
 
@@ -785,7 +790,7 @@ Qed.
 
 Lemma compare_float_nextpc:
   forall rs v1 v2,
-  nextinstr (compare_float rs v1 v2) PC = Val.add (rs PC) Vone.
+  nextinstr (compare_float rs v1 v2) PC = Val.offset_ptr (rs PC) Ptrofs.one.
 Proof.
   intros. unfold compare_float. destruct v1; destruct v2; reflexivity.
 Qed.
@@ -891,7 +896,7 @@ Qed.
 
 Lemma compare_float32_nextpc:
   forall rs v1 v2,
-  nextinstr (compare_float32 rs v1 v2) PC = Val.add (rs PC) Vone.
+  nextinstr (compare_float32 rs v1 v2) PC = Val.offset_ptr (rs PC) Ptrofs.one.
 Proof.
   intros. unfold compare_float32. destruct v1; destruct v2; reflexivity.
 Qed.
@@ -1138,7 +1143,7 @@ Lemma transl_op_correct_same:
   forall op args res k c (rs: regset) m v,
   transl_op op args res k = OK c ->
   eval_operation ge rs#IR13 op (map rs (map preg_of args)) m = Some v ->
-  match op with Ocmp _ => False | _ => True end ->
+  match op with Ocmp _ => False | Oaddrstack _ => False | _ => True end ->
   exists rs',
      exec_straight ge fn c rs m k rs' m
   /\ rs'#(preg_of res) = v
@@ -1155,9 +1160,7 @@ Proof.
   generalize (loadimm_correct x i k rs m). intros [rs' [A [B C]]].
   exists rs'; auto with asmgen.
   (* Oaddrstack *)
-  generalize (addimm_correct x IR13 i k rs m).
-  intros [rs' [EX [RES OTH]]].
-  exists rs'; auto with asmgen.
+  contradiction.
   (* Ocast8signed *)
   destruct (thumb tt).
   econstructor; split. apply exec_straight_one; simpl; eauto. intuition Simpl.
@@ -1296,19 +1299,29 @@ Lemma transl_op_correct:
   /\ forall r, data_preg r = true -> r <> preg_of res -> preg_notin r (destroyed_by_op op) -> rs'#r = rs#r.
 Proof.
   intros.
-  assert (EITHER: match op with Ocmp _ => False | _ => True end \/ exists cmp, op = Ocmp cmp).
-    destruct op; auto. right; exists c0; auto.
-  destruct EITHER as [A | [cmp A]].
-  exploit transl_op_correct_same; eauto. intros [rs' [P [Q R]]].
-  subst v. exists rs'; eauto.
-  (* Ocmp *)
-  subst op. simpl in H. monadInv H. simpl in H0. inv H0.
+  assert (SAME:
+      (exists rs', exec_straight ge fn c rs m k rs' m
+           /\ rs'#(preg_of res) = v
+           /\ forall r, data_preg r = true -> r <> preg_of res -> preg_notin r (destroyed_by_op op) -> rs'#r = rs#r) ->
+       exists rs', exec_straight ge fn c rs m k rs' m
+           /\ Val.lessdef v rs'#(preg_of res)
+           /\ forall r, data_preg r = true -> r <> preg_of res -> preg_notin r (destroyed_by_op op) -> rs'#r = rs#r).
+  { intros (rs' & A & B & C). subst v; exists rs'; auto. } 
+  destruct op; try (apply SAME; eapply transl_op_correct_same; eauto; fail).
+- (* Oaddrstack *)
+  clear SAME; simpl in *; ArgsInv.
+  destruct (addimm_correct x IR13 (Ptrofs.to_int i) k rs m) as [rs' [EX [RES OTH]]].
+  exists rs'; split. auto. split.
+  rewrite RES; inv H0. destruct (rs IR13); simpl; auto. rewrite Ptrofs.of_int_to_int; auto.
+  intros; apply OTH; eauto with asmgen.
+- (* Ocmp *)
+  clear SAME. simpl in H. monadInv H. simpl in H0. inv H0.
   rewrite (ireg_of_eq _ _ EQ).
   exploit transl_cond_correct; eauto. instantiate (1 := rs). instantiate (1 := m). intros [rs1 [A [B C]]].
   econstructor; split.
   eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. auto.
   split; intros; Simpl.
-  destruct (eval_condition cmp rs ## (preg_of ## args) m) as [b|]; simpl; auto.
+  destruct (eval_condition c0 rs ## (preg_of ## args) m) as [b|]; simpl; auto.
   destruct B as [B1 B2]; rewrite B1. destruct b; auto.
 Qed.
 
@@ -1317,7 +1330,10 @@ Qed.
 Remark val_add_add_zero:
   forall v1 v2, Val.add v1 v2 = Val.add (Val.add v1 v2) (Vint Int.zero).
 Proof.
-  intros. destruct v1; destruct v2; simpl; auto; rewrite Int.add_zero; auto.
+  intros. destruct v1; destruct v2; simpl; auto.
+  rewrite Int.add_zero; auto.
+  rewrite Ptrofs.add_zero; auto.
+  rewrite Ptrofs.add_zero; auto.
 Qed.
 
 Lemma transl_memory_access_correct:
@@ -1327,6 +1343,7 @@ Lemma transl_memory_access_correct:
          addr args k c (rs: regset) a m m',
   transl_memory_access mk_instr_imm mk_instr_gen mk_immed addr args k = OK c ->
   eval_addressing ge (rs#SP) addr (map rs (map preg_of args)) = Some a ->
+  match a with Vptr _ _ => True | _ => False end ->
   (forall (r1: ireg) (rs1: regset) n k,
     Val.add rs1#r1 (Vint n) = a ->
     (forall (r: preg), if_preg r = true -> r <> IR14 -> rs1 r = rs r) ->
@@ -1343,7 +1360,7 @@ Lemma transl_memory_access_correct:
   exists rs',
     exec_straight ge fn c rs m k rs' m' /\ P rs'.
 Proof.
-  intros until m'; intros TR EA MK1 MK2.
+  intros until m'; intros TR EA ADDR MK1 MK2.
   unfold transl_memory_access in TR; destruct addr; ArgsInv; simpl in EA; inv EA.
   (* Aindexed *)
   apply indexed_memory_access_correct. exact MK1.
@@ -1354,7 +1371,8 @@ Proof.
   destruct mk_instr_gen as [mk | ]; monadInv TR. apply MK2.
   erewrite ! ireg_of_eq; eauto. rewrite transl_shift_correct. auto.
   (* Ainstack *)
-  inv TR. apply indexed_memory_access_correct. exact MK1.
+  inv TR. apply indexed_memory_access_correct. intros. eapply MK1; eauto.
+  rewrite H. destruct (rs IR13); try contradiction. simpl. f_equal; f_equal. auto with ptrofs.     
 Qed.
 
 Lemma transl_load_int_correct:
@@ -1372,6 +1390,7 @@ Lemma transl_load_int_correct:
 Proof.
   intros. monadInv H. erewrite ireg_of_eq by eauto.
   eapply transl_memory_access_correct; eauto.
+  destruct a; discriminate || trivial.
   intros; simpl. econstructor; split. apply exec_straight_one.
   rewrite H2. unfold exec_load. simpl eval_shift_op. rewrite H. rewrite H1. eauto. auto.
   split. Simpl. intros; Simpl.
@@ -1396,6 +1415,7 @@ Lemma transl_load_float_correct:
 Proof.
   intros. monadInv H. erewrite freg_of_eq by eauto.
   eapply transl_memory_access_correct; eauto.
+  destruct a; discriminate || trivial.
   intros; simpl. econstructor; split. apply exec_straight_one.
   rewrite H2. unfold exec_load. rewrite H. rewrite H1. eauto. auto.
   split. Simpl. intros; Simpl.
@@ -1417,6 +1437,7 @@ Proof.
   intros. assert (DR: data_preg (preg_of src) = true) by eauto with asmgen.
   monadInv H. erewrite ireg_of_eq in * by eauto.
   eapply transl_memory_access_correct; eauto.
+  destruct a; discriminate || trivial.
   intros; simpl. econstructor; split. apply exec_straight_one.
   rewrite H2. unfold exec_store. simpl eval_shift_op. rewrite H. rewrite H3; eauto with asmgen.
   rewrite H1. eauto. auto.
@@ -1442,6 +1463,7 @@ Proof.
   intros. assert (DR: data_preg (preg_of src) = true) by eauto with asmgen.
   monadInv H. erewrite freg_of_eq in * by eauto.
   eapply transl_memory_access_correct; eauto.
+  destruct a; discriminate || trivial.
   intros; simpl. econstructor; split. apply exec_straight_one.
   rewrite H2. unfold exec_store. rewrite H. rewrite H3; auto with asmgen. rewrite H1. eauto. auto.
   intros; Simpl.
diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp
index 872493a6..e0f0889f 100644
--- a/arm/ConstpropOp.vp
+++ b/arm/ConstpropOp.vp
@@ -22,6 +22,18 @@ Require Import Op.
 Require Import Registers.
 Require Import ValueDomain.
 
+(** * Converting known values to constants *)
+
+Definition const_for_result (a: aval) : option operation :=
+  match a with
+  | I n => Some(Ointconst n)
+  | F n => if Compopts.generate_float_constants tt then Some(Ofloatconst n) else None
+  | FS n => if Compopts.generate_float_constants tt then Some(Osingleconst n) else None
+  | Ptr(Gl id ofs) => Some (Oaddrsymbol id ofs)
+  | Ptr(Stk ofs) => Some(Oaddrstack ofs)
+  | _ => None
+  end.
+
 (** * Operator strength reduction *)
 
 (** We now define auxiliary functions for strength reduction of
@@ -237,19 +249,19 @@ Nondetfunction addr_strength_reduction
                 (addr: addressing) (args: list reg) (vl: list aval) :=
   match addr, args, vl with
   | Aindexed2, r1 :: r2 :: nil, Ptr(Stk n1) :: I n2 :: nil =>
-      (Ainstack (Int.add n1 n2), nil)
+      (Ainstack (Ptrofs.add n1 (Ptrofs.of_int n2)), nil)
   | Aindexed2, r1 :: r2 :: nil, I n1 :: Ptr(Stk n2) :: nil =>
-      (Ainstack (Int.add n1 n2), nil)
+      (Ainstack (Ptrofs.add (Ptrofs.of_int n1) n2), nil)
   | Aindexed2, r1 :: r2 :: nil, I n1 :: v2 :: nil =>
       (Aindexed n1, r2 :: nil)
   | Aindexed2, r1 :: r2 :: nil, v1 :: I n2 :: nil =>
       (Aindexed n2, r1 :: nil)
   | Aindexed2shift s, r1 :: r2 :: nil, Ptr(Stk n1) :: I n2 :: nil =>
-      (Ainstack (Int.add n1 (eval_static_shift s n2)), nil)
+      (Ainstack (Ptrofs.add n1 (Ptrofs.of_int (eval_static_shift s n2))), nil)
   | Aindexed2shift s, r1 :: r2 :: nil, v1 :: I n2 :: nil =>
       (Aindexed (eval_static_shift s n2), r1 :: nil)
   | Aindexed n, r1 :: nil, Ptr(Stk n1) :: nil =>
-      (Ainstack (Int.add n1 n), nil)
+      (Ainstack (Ptrofs.add n1 (Ptrofs.of_int n)), nil)
   | _, _, _ =>
       (addr, args)
   end.
diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v
index 0b7643c6..e1ae80a2 100644
--- a/arm/ConstpropOpproof.v
+++ b/arm/ConstpropOpproof.v
@@ -27,6 +27,8 @@ Require Import RTL.
 Require Import ValueDomain.
 Require Import ConstpropOp.
 
+Local Transparent Archi.ptr64.
+
 (** * Correctness of strength reduction *)
 
 (** We now show that strength reduction over operators and addressing
@@ -95,6 +97,28 @@ Ltac SimplVM :=
   | _ => idtac
   end.
 
+Lemma const_for_result_correct:
+  forall a op v,
+  const_for_result a = Some op ->
+  vmatch bc v a ->
+  exists v', eval_operation ge (Vptr sp Ptrofs.zero) op nil m = Some v' /\ Val.lessdef v v'.
+Proof.
+  unfold const_for_result; intros.
+  destruct a; inv H; SimplVM.
+- (* integer *)
+  exists (Vint n); auto.
+- (* float *)
+  destruct (generate_float_constants tt); inv H2. exists (Vfloat f); auto.
+- (* single *)
+  destruct (generate_float_constants tt); inv H2. exists (Vsingle f); auto.
+- (* pointer *)
+  destruct p; try discriminate; SimplVM.
+  + (* global *)
+    inv H2. exists (Genv.symbol_address ge id ofs); auto.
+  + (* stack *)
+    inv H2. exists (Vptr sp ofs); split; auto. simpl. rewrite Ptrofs.add_zero_l; auto.  
+Qed.
+
 Lemma eval_static_shift_correct:
   forall s n, eval_shift s (Vint n) = Vint (eval_static_shift s n).
 Proof.
@@ -146,7 +170,7 @@ Lemma make_cmp_base_correct:
   forall c args vl,
   vl = map (fun r => AE.get r ae) args ->
   let (op', args') := make_cmp_base c args vl in
-  exists v, eval_operation ge (Vptr sp Int.zero) op' rs##args' m = Some v
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op' rs##args' m = Some v
          /\ Val.lessdef (Val.of_optbool (eval_condition c rs##args m)) v.
 Proof.
   intros. unfold make_cmp_base.
@@ -159,7 +183,7 @@ Lemma make_cmp_correct:
   forall c args vl,
   vl = map (fun r => AE.get r ae) args ->
   let (op', args') := make_cmp c args vl in
-  exists v, eval_operation ge (Vptr sp Int.zero) op' rs##args' m = Some v
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op' rs##args' m = Some v
          /\ Val.lessdef (Val.of_optbool (eval_condition c rs##args m)) v.
 Proof.
   intros c args vl.
@@ -191,11 +215,12 @@ Qed.
 Lemma make_addimm_correct:
   forall n r,
   let (op, args) := make_addimm n r in
-  exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.add rs#r (Vint n)) v.
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.add rs#r (Vint n)) v.
 Proof.
   intros. unfold make_addimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros.
-  subst. exists (rs#r); split; auto. destruct (rs#r); simpl; auto; rewrite Int.add_zero; auto.
+  subst. exists (rs#r); split; auto.
+  destruct (rs#r); simpl; auto. rewrite Int.add_zero; auto. rewrite Ptrofs.add_zero; auto.
   exists (Val.add rs#r (Vint n)); auto.
 Qed.
 
@@ -203,7 +228,7 @@ Lemma make_shlimm_correct:
   forall n r1 r2,
   rs#r2 = Vint n ->
   let (op, args) := make_shlimm n r1 r2 in
-  exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.shl rs#r1 (Vint n)) v.
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.shl rs#r1 (Vint n)) v.
 Proof.
   Opaque mk_shift_amount.
   intros; unfold make_shlimm.
@@ -218,7 +243,7 @@ Lemma make_shrimm_correct:
   forall n r1 r2,
   rs#r2 = Vint n ->
   let (op, args) := make_shrimm n r1 r2 in
-  exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.shr rs#r1 (Vint n)) v.
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.shr rs#r1 (Vint n)) v.
 Proof.
   intros; unfold make_shrimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
@@ -232,7 +257,7 @@ Lemma make_shruimm_correct:
   forall n r1 r2,
   rs#r2 = Vint n ->
   let (op, args) := make_shruimm n r1 r2 in
-  exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.shru rs#r1 (Vint n)) v.
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.shru rs#r1 (Vint n)) v.
 Proof.
   intros; unfold make_shruimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
@@ -246,7 +271,7 @@ Lemma make_mulimm_correct:
   forall n r1 r2,
   rs#r2 = Vint n ->
   let (op, args) := make_mulimm n r1 r2 in
-  exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mul rs#r1 (Vint n)) v.
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.mul rs#r1 (Vint n)) v.
 Proof.
   intros; unfold make_mulimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros. subst.
@@ -265,7 +290,7 @@ Lemma make_divimm_correct:
   Val.divs rs#r1 rs#r2 = Some v ->
   rs#r2 = Vint n ->
   let (op, args) := make_divimm n r1 r2 in
-  exists w, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some w /\ Val.lessdef v w.
+  exists w, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some w /\ Val.lessdef v w.
 Proof.
   intros; unfold make_divimm.
   destruct (Int.is_power2 n) eqn:?.
@@ -280,7 +305,7 @@ Lemma make_divuimm_correct:
   Val.divu rs#r1 rs#r2 = Some v ->
   rs#r2 = Vint n ->
   let (op, args) := make_divuimm n r1 r2 in
-  exists w, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some w /\ Val.lessdef v w.
+  exists w, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some w /\ Val.lessdef v w.
 Proof.
   intros; unfold make_divuimm.
   destruct (Int.is_power2 n) eqn:?.
@@ -295,7 +320,7 @@ Lemma make_andimm_correct:
   forall n r x,
   vmatch bc rs#r x ->
   let (op, args) := make_andimm n r x in
-  exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.and rs#r (Vint n)) v.
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.and rs#r (Vint n)) v.
 Proof.
   intros; unfold make_andimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros.
@@ -320,7 +345,7 @@ Qed.
 Lemma make_orimm_correct:
   forall n r,
   let (op, args) := make_orimm n r in
-  exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.or rs#r (Vint n)) v.
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.or rs#r (Vint n)) v.
 Proof.
   intros; unfold make_orimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros.
@@ -333,7 +358,7 @@ Qed.
 Lemma make_xorimm_correct:
   forall n r,
   let (op, args) := make_xorimm n r in
-  exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.xor rs#r (Vint n)) v.
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.xor rs#r (Vint n)) v.
 Proof.
   intros; unfold make_xorimm.
   predSpec Int.eq Int.eq_spec n Int.zero; intros.
@@ -348,7 +373,7 @@ Lemma make_mulfimm_correct:
   forall n r1 r2,
   rs#r2 = Vfloat n ->
   let (op, args) := make_mulfimm n r1 r1 r2 in
-  exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulf rs#r1 rs#r2) v.
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulf rs#r1 rs#r2) v.
 Proof.
   intros; unfold make_mulfimm.
   destruct (Float.eq_dec n (Float.of_int (Int.repr 2))); intros.
@@ -361,7 +386,7 @@ Lemma make_mulfimm_correct_2:
   forall n r1 r2,
   rs#r1 = Vfloat n ->
   let (op, args) := make_mulfimm n r2 r1 r2 in
-  exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulf rs#r1 rs#r2) v.
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulf rs#r1 rs#r2) v.
 Proof.
   intros; unfold make_mulfimm.
   destruct (Float.eq_dec n (Float.of_int (Int.repr 2))); intros.
@@ -375,7 +400,7 @@ Lemma make_mulfsimm_correct:
   forall n r1 r2,
   rs#r2 = Vsingle n ->
   let (op, args) := make_mulfsimm n r1 r1 r2 in
-  exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulfs rs#r1 rs#r2) v.
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulfs rs#r1 rs#r2) v.
 Proof.
   intros; unfold make_mulfsimm.
   destruct (Float32.eq_dec n (Float32.of_int (Int.repr 2))); intros.
@@ -388,7 +413,7 @@ Lemma make_mulfsimm_correct_2:
   forall n r1 r2,
   rs#r1 = Vsingle n ->
   let (op, args) := make_mulfsimm n r2 r1 r2 in
-  exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulfs rs#r1 rs#r2) v.
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulfs rs#r1 rs#r2) v.
 Proof.
   intros; unfold make_mulfsimm.
   destruct (Float32.eq_dec n (Float32.of_int (Int.repr 2))); intros.
@@ -402,7 +427,7 @@ Lemma make_cast8signed_correct:
   forall r x,
   vmatch bc rs#r x ->
   let (op, args) := make_cast8signed r x in
-  exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.sign_ext 8 rs#r) v.
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.sign_ext 8 rs#r) v.
 Proof.
   intros; unfold make_cast8signed. destruct (vincl x (Sgn Ptop 8)) eqn:INCL.
   exists rs#r; split; auto.
@@ -416,7 +441,7 @@ Lemma make_cast16signed_correct:
   forall r x,
   vmatch bc rs#r x ->
   let (op, args) := make_cast16signed r x in
-  exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.sign_ext 16 rs#r) v.
+  exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.sign_ext 16 rs#r) v.
 Proof.
   intros; unfold make_cast16signed. destruct (vincl x (Sgn Ptop 16)) eqn:INCL.
   exists rs#r; split; auto.
@@ -429,9 +454,9 @@ Qed.
 Lemma op_strength_reduction_correct:
   forall op args vl v,
   vl = map (fun r => AE.get r ae) args ->
-  eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v ->
+  eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v ->
   let (op', args') := op_strength_reduction op args vl in
-  exists w, eval_operation ge (Vptr sp Int.zero) op' rs##args' m = Some w /\ Val.lessdef v w.
+  exists w, eval_operation ge (Vptr sp Ptrofs.zero) op' rs##args' m = Some w /\ Val.lessdef v w.
 Proof.
   intros until v; unfold op_strength_reduction;
   case (op_strength_reduction_match op args vl); simpl; intros.
@@ -440,8 +465,7 @@ Proof.
 (* cast8signed *)
   InvApproxRegs; SimplVM; inv H0. apply make_cast16signed_correct; auto.
 (* add *)
-  InvApproxRegs; SimplVM. inv H0.
-  fold (Val.add (Vint n1) rs#r2). rewrite Val.add_commut. apply make_addimm_correct.
+  InvApproxRegs; SimplVM. rewrite Val.add_commut in H0. inv H0. apply make_addimm_correct.
   InvApproxRegs; SimplVM. inv H0. apply make_addimm_correct.
 (* addshift *)
   InvApproxRegs; SimplVM. inv H0. rewrite eval_static_shift_correct. apply make_addimm_correct.
@@ -504,28 +528,30 @@ Qed.
 Lemma addr_strength_reduction_correct:
   forall addr args vl res,
   vl = map (fun r => AE.get r ae) args ->
-  eval_addressing ge (Vptr sp Int.zero) addr rs##args = Some res ->
+  eval_addressing ge (Vptr sp Ptrofs.zero) addr rs##args = Some res ->
   let (addr', args') := addr_strength_reduction addr args vl in
-  exists res', eval_addressing ge (Vptr sp Int.zero) addr' rs##args' = Some res' /\ Val.lessdef res res'.
+  exists res', eval_addressing ge (Vptr sp Ptrofs.zero) addr' rs##args' = Some res' /\ Val.lessdef res res'.
 Proof.
   intros until res. unfold addr_strength_reduction.
   destruct (addr_strength_reduction_match addr args vl); simpl;
   intros VL EA; InvApproxRegs; SimplVM; try (inv EA).
-- rewrite Int.add_zero_l.
-  change (Vptr sp (Int.add n1 n2)) with (Val.add (Vptr sp n1) (Vint n2)).
+- rewrite Ptrofs.add_zero_l.
+  change (Vptr sp (Ptrofs.add n1 (Ptrofs.of_int n2))) with (Val.add (Vptr sp n1) (Vint n2)).
   econstructor; split; eauto. apply Val.add_lessdef; auto.
-- fold (Val.add (Vint n1) rs#r2).  rewrite Int.add_zero_l. rewrite Int.add_commut.
-  change (Vptr sp (Int.add n2 n1)) with (Val.add (Vptr sp n2) (Vint n1)).
-  rewrite Val.add_commut. econstructor; split; eauto. apply Val.add_lessdef; auto.
-- fold (Val.add (Vint n1) rs#r2).
-  rewrite Val.add_commut. econstructor; split; eauto.
+- rewrite Ptrofs.add_zero_l. econstructor; split; eauto. rewrite Ptrofs.add_commut.
+  change (Val.lessdef (Val.add (Vint n1) rs#r2) (Val.add (Vptr sp n2) (Vint n1))).
+  rewrite Val.add_commut; apply Val.add_lessdef; auto.
+- econstructor; split; eauto.
+  change (Val.lessdef (Val.add (Vint n1) rs#r2) (Val.add rs#r2 (Vint n1))).
+  rewrite Val.add_commut; apply Val.add_lessdef; auto.
 - econstructor; split; eauto.
-- rewrite eval_static_shift_correct. rewrite Int.add_zero_l.
-  change (Vptr sp (Int.add n1 (eval_static_shift s n2)))
+- rewrite eval_static_shift_correct. rewrite Ptrofs.add_zero_l. econstructor; split; eauto.
+  change (Vptr sp (Ptrofs.add n1 (Ptrofs.of_int (eval_static_shift s n2))))
     with (Val.add (Vptr sp n1) (Vint (eval_static_shift s n2))).
-  econstructor; split; eauto. apply Val.add_lessdef; auto.
+  apply Val.add_lessdef; auto.
 - rewrite eval_static_shift_correct. econstructor; split; eauto.
-- rewrite Int.add_zero_l. change (Vptr sp (Int.add n1 n)) with (Val.add (Vptr sp n1) (Vint n)).
+- rewrite Ptrofs.add_zero_l.
+  change (Vptr sp (Ptrofs.add n1 (Ptrofs.of_int n))) with (Val.add (Vptr sp n1) (Vint n)).
   econstructor; split; eauto. apply Val.add_lessdef; auto.
 - exists res; auto.
 Qed.
diff --git a/arm/Conventions1.v b/arm/Conventions1.v
index 888861a5..ecf03e1d 100644
--- a/arm/Conventions1.v
+++ b/arm/Conventions1.v
@@ -60,6 +60,15 @@ Definition destroyed_at_call :=
 Definition dummy_int_reg := R0.     (**r Used in [Coloring]. *)
 Definition dummy_float_reg := F0.   (**r Used in [Coloring]. *)
 
+Definition is_float_reg (r: mreg): bool :=
+  match r with
+  | R0  | R1  | R2  | R3
+  | R4  | R5  | R6  | R7
+  | R8  | R9  | R10 | R11  | R12 => false
+  | F0  | F1  | F2  | F3  | F4  | F5  | F6  | F7
+  | F8  | F9  | F10  | F11 | F12  | F13  | F14  | F15 => true
+  end.
+
 (** * Function calling conventions *)
 
 (** The functions in this section determine the locations (machine registers
@@ -127,7 +136,7 @@ Lemma loc_result_pair:
   forall sg,
   match loc_result sg with
   | One _ => True
-  | Twolong r1 r2 => r1 <> r2 /\ sg.(sig_res) = Some Tlong /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true
+  | Twolong r1 r2 => r1 <> r2 /\ sg.(sig_res) = Some Tlong /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true /\ Archi.splitlong = true
   end.
 Proof.
   intros; unfold loc_result; destruct (sig_res sg) as [[]|]; destruct Archi.big_endian; auto.
@@ -135,6 +144,14 @@ Proof.
   intuition congruence.
 Qed.
 
+(** The location of the result depends only on the result part of the signature *)
+
+Lemma loc_result_exten:
+  forall s1 s2, s1.(sig_res) = s2.(sig_res) -> loc_result s1 = loc_result s2.
+Proof.
+  intros. unfold loc_result. rewrite H; auto.
+Qed.
+
 (** ** Location of function arguments *)
 
 (** For the "hardfloat" configuration, we use the following calling conventions,
diff --git a/arm/NeedOp.v b/arm/NeedOp.v
index 41b80941..dee7cae1 100644
--- a/arm/NeedOp.v
+++ b/arm/NeedOp.v
@@ -145,11 +145,11 @@ Qed.
 
 Lemma needs_of_operation_sound:
   forall op args v nv args',
-  eval_operation ge (Vptr sp Int.zero) op args m = Some v ->
+  eval_operation ge (Vptr sp Ptrofs.zero) op args m = Some v ->
   vagree_list args args' (needs_of_operation op nv) ->
   nv <> Nothing ->
   exists v',
-     eval_operation ge (Vptr sp Int.zero) op args' m' = Some v'
+     eval_operation ge (Vptr sp Ptrofs.zero) op args' m' = Some v'
   /\ vagree v v' nv.
 Proof.
   unfold needs_of_operation; intros; destruct op; try (eapply default_needs_of_operation_sound; eauto; fail);
@@ -188,7 +188,7 @@ Qed.
 Lemma operation_is_redundant_sound:
   forall op nv arg1 args v arg1' args',
   operation_is_redundant op nv = true ->
-  eval_operation ge (Vptr sp Int.zero) op (arg1 :: args) m = Some v ->
+  eval_operation ge (Vptr sp Ptrofs.zero) op (arg1 :: args) m = Some v ->
   vagree_list (arg1 :: args) (arg1' :: args') (needs_of_operation op nv) ->
   vagree v arg1' nv.
 Proof.
diff --git a/arm/Op.v b/arm/Op.v
index bc717d7b..0d31c2ac 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -35,6 +35,7 @@ Require Import Globalenvs.
 Require Import Events.
 
 Set Implicit Arguments.
+Local Transparent Archi.ptr64.
 
 Record shift_amount: Type :=
   { s_amount: int;
@@ -74,8 +75,8 @@ Inductive operation : Type :=
   | Ointconst: int -> operation         (**r [rd] is set to the given integer constant *)
   | Ofloatconst: float -> operation     (**r [rd] is set to the given 64-bit float constant *)
   | Osingleconst: float32 -> operation  (**r [rd] is set to the given 32-bit float constant *)
-  | Oaddrsymbol: ident -> int -> operation (**r [rd] is set to the the address of the symbol plus the offset *)
-  | Oaddrstack: int -> operation        (**r [rd] is set to the stack pointer plus the given offset *)
+  | Oaddrsymbol: ident -> ptrofs -> operation (**r [rd] is set to the the address of the symbol plus the offset *)
+  | Oaddrstack: ptrofs -> operation        (**r [rd] is set to the stack pointer plus the given offset *)
 (*c Integer arithmetic: *)
   | Ocast8signed: operation             (**r [rd] is 8-bit sign extension of [r1] *)
   | Ocast16signed: operation            (**r [rd] is 16-bit sign extension of [r1] *)
@@ -148,7 +149,7 @@ Inductive addressing: Type :=
   | Aindexed: int -> addressing         (**r Address is [r1 + offset] *)
   | Aindexed2: addressing               (**r Address is [r1 + r2] *)
   | Aindexed2shift: shift -> addressing (**r Address is [r1 + shifted r2] *)
-  | Ainstack: int -> addressing.        (**r Address is [stack_pointer + offset] *)
+  | Ainstack: ptrofs -> addressing.        (**r Address is [stack_pointer + offset] *)
 
 (** Comparison functions (used in module [CSE]). *)
 
@@ -173,10 +174,8 @@ Defined.
 
 Definition eq_operation (x y: operation): {x=y} + {x<>y}.
 Proof.
-  generalize Int.eq_dec; intro.
-  generalize Float.eq_dec; intro.
-  generalize Float32.eq_dec; intro.
-  assert (forall (x y: ident), {x=y}+{x<>y}). exact peq.
+  generalize Int.eq_dec Ptrofs.eq_dec ident_eq; intros.
+  generalize Float.eq_dec Float32.eq_dec; intros.
   generalize eq_shift; intro.
   generalize eq_condition; intro.
   decide equality.
@@ -184,7 +183,7 @@ Defined.
 
 Definition eq_addressing (x y: addressing) : {x=y} + {x<>y}.
 Proof.
-  generalize Int.eq_dec; intro.
+  generalize Int.eq_dec Ptrofs.eq_dec; intro.
   generalize eq_shift; intro.
   decide equality.
 Defined.
@@ -235,7 +234,7 @@ Definition eval_operation
   | Ofloatconst n, nil => Some (Vfloat n)
   | Osingleconst n, nil => Some (Vsingle n)
   | Oaddrsymbol s ofs, nil => Some (Genv.symbol_address genv s ofs)
-  | Oaddrstack ofs, nil => Some (Val.add sp (Vint ofs))
+  | Oaddrstack ofs, nil => Some (Val.offset_ptr sp ofs)
   | Ocast8signed, v1::nil => Some (Val.sign_ext 8 v1)
   | Ocast16signed, v1::nil => Some (Val.sign_ext 16 v1)
   | Oadd, v1 :: v2 :: nil => Some (Val.add v1 v2)
@@ -305,10 +304,24 @@ Definition eval_addressing
   | Aindexed n, v1 :: nil => Some (Val.add v1 (Vint n))
   | Aindexed2, v1 :: v2 :: nil => Some (Val.add v1 v2)
   | Aindexed2shift s, v1 :: v2 :: nil => Some (Val.add v1 (eval_shift s v2))
-  | Ainstack ofs, nil => Some (Val.add sp (Vint ofs))
+  | Ainstack ofs, nil => Some (Val.offset_ptr sp ofs)
   | _, _ => None
   end.
 
+Remark eval_addressing_Ainstack:
+  forall (F V: Type) (genv: Genv.t F V) sp ofs,
+  eval_addressing genv sp (Ainstack ofs) nil = Some (Val.offset_ptr sp ofs).
+Proof.
+  intros. reflexivity.
+Qed.
+
+Remark eval_addressing_Ainstack_inv:
+  forall (F V: Type) (genv: Genv.t F V) sp ofs vl v,
+  eval_addressing genv sp (Ainstack ofs) vl = Some v -> vl = nil /\ v = Val.offset_ptr sp ofs.
+Proof.
+  unfold eval_addressing; intros; destruct vl; inv H; auto.
+Qed.
+
 Ltac FuncInv :=
   match goal with
   | H: (match ?x with nil => _ | _ :: _ => _ end = Some _) |- _ =>
@@ -430,7 +443,7 @@ Lemma type_of_operation_sound:
   op <> Omove ->
   eval_operation genv sp op vl m = Some v ->
   Val.has_type v (snd (type_of_operation op)).
-Proof with (try exact I).
+Proof with (try exact I; try reflexivity).
   assert (S: forall s v, Val.has_type (eval_shift s v) Tint).
     intros. unfold eval_shift. destruct s; destruct v; simpl; auto; rewrite s_range; exact I.
   intros.
@@ -588,15 +601,15 @@ Qed.
 
 (** Shifting stack-relative references.  This is used in [Stacking]. *)
 
-Definition shift_stack_addressing (delta: int) (addr: addressing) :=
+Definition shift_stack_addressing (delta: Z) (addr: addressing) :=
   match addr with
-  | Ainstack ofs => Ainstack (Int.add delta ofs)
+  | Ainstack ofs => Ainstack (Ptrofs.add (Ptrofs.repr delta) ofs)
   | _ => addr
   end.
 
-Definition shift_stack_operation (delta: int) (op: operation) :=
+Definition shift_stack_operation (delta: Z) (op: operation) :=
   match op with
-  | Oaddrstack ofs => Oaddrstack (Int.add delta ofs)
+  | Oaddrstack ofs => Oaddrstack (Ptrofs.add (Ptrofs.repr delta) ofs)
   | _ => op
   end.
 
@@ -614,79 +627,43 @@ Qed.
 
 Lemma eval_shift_stack_addressing:
   forall F V (ge: Genv.t F V) sp addr vl delta,
-  eval_addressing ge sp (shift_stack_addressing delta addr) vl =
-  eval_addressing ge (Val.add sp (Vint delta)) addr vl.
+  eval_addressing ge (Vptr sp Ptrofs.zero) (shift_stack_addressing delta addr) vl =
+  eval_addressing ge (Vptr sp (Ptrofs.repr delta)) addr vl.
 Proof.
   intros. destruct addr; simpl; auto.
-  rewrite Val.add_assoc. simpl. auto.
+  rewrite Ptrofs.add_zero_l; auto.
 Qed.
 
 Lemma eval_shift_stack_operation:
   forall F V (ge: Genv.t F V) sp op vl m delta,
-  eval_operation ge sp (shift_stack_operation delta op) vl m =
-  eval_operation ge (Val.add sp (Vint delta)) op vl m.
+  eval_operation ge (Vptr sp Ptrofs.zero) (shift_stack_operation delta op) vl m =
+  eval_operation ge (Vptr sp (Ptrofs.repr delta)) op vl m.
 Proof.
   intros. destruct op; simpl; auto.
-  rewrite Val.add_assoc. simpl. auto.
+  rewrite Ptrofs.add_zero_l; auto.
 Qed.
 
 (** Offset an addressing mode [addr] by a quantity [delta], so that
   it designates the pointer [delta] bytes past the pointer designated
   by [addr].  May be undefined, in which case [None] is returned. *)
 
-Definition offset_addressing (addr: addressing) (delta: int) : option addressing :=
+Definition offset_addressing (addr: addressing) (delta: Z) : option addressing :=
   match addr with
-  | Aindexed n => Some(Aindexed (Int.add n delta))
+  | Aindexed n => Some(Aindexed (Int.add n (Int.repr delta)))
   | Aindexed2 => None
   | Aindexed2shift s => None
-  | Ainstack n => Some(Ainstack (Int.add n delta))
+  | Ainstack n => Some(Ainstack (Ptrofs.add n (Ptrofs.repr delta)))
   end.
 
 Lemma eval_offset_addressing:
   forall (F V: Type) (ge: Genv.t F V) sp addr args delta addr' v,
   offset_addressing addr delta = Some addr' ->
   eval_addressing ge sp addr args = Some v ->
-  eval_addressing ge sp addr' args = Some(Val.add v (Vint delta)).
+  eval_addressing ge sp addr' args = Some(Val.add v (Vint (Int.repr delta))).
 Proof.
   intros. destruct addr; simpl in H; inv H; simpl in *; FuncInv; subst.
   rewrite Val.add_assoc; auto.
-  rewrite Val.add_assoc. auto.
-Qed.
-
-(** Transformation of addressing modes with two operands or more
-  into an equivalent arithmetic operation.  This is used in the [Reload]
-  pass when a store instruction cannot be reloaded directly because
-  it runs out of temporary registers. *)
-
-(** For the ARM, there are only two binary addressing mode: [Aindexed2]
-  and [Aindexed2shift].  The corresponding operations are [Oadd]
-  and [Oaddshift]. *)
-
-Definition op_for_binary_addressing (addr: addressing) : operation :=
-  match addr with
-  | Aindexed2 => Oadd
-  | Aindexed2shift s => Oaddshift s
-  | _ => Ointconst Int.zero (* never happens *)
-  end.
-
-Lemma eval_op_for_binary_addressing:
-  forall (F V: Type) (ge: Genv.t F V) sp addr args v m,
-  (length args >= 2)%nat ->
-  eval_addressing ge sp addr args = Some v ->
-  eval_operation ge sp (op_for_binary_addressing addr) args m = Some v.
-Proof.
-  intros.
-  unfold eval_addressing in H0; destruct addr; FuncInv; simpl in H; try omegaContradiction; simpl.
-  congruence.
-  congruence.
-Qed.
-
-Lemma type_op_for_binary_addressing:
-  forall addr,
-  (length (type_of_addressing addr) >= 2)%nat ->
-  type_of_operation (op_for_binary_addressing addr) = (type_of_addressing addr, Tint).
-Proof.
-  intros. destruct addr; simpl in H; reflexivity || omegaContradiction.
+  destruct sp; simpl; auto. rewrite Ptrofs.add_assoc. do 4 f_equal. symmetry; auto with ptrofs.
 Qed.
 
 (** Two-address operations.  There are none in the ARM architecture. *)
@@ -781,30 +758,30 @@ Variable m2: mem.
 Hypothesis valid_pointer_inj:
   forall b1 ofs b2 delta,
   f b1 = Some(b2, delta) ->
-  Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true ->
-  Mem.valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
+  Mem.valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true ->
+  Mem.valid_pointer m2 b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true.
 
 Hypothesis weak_valid_pointer_inj:
   forall b1 ofs b2 delta,
   f b1 = Some(b2, delta) ->
-  Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true ->
-  Mem.weak_valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
+  Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true ->
+  Mem.weak_valid_pointer m2 b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true.
 
 Hypothesis weak_valid_pointer_no_overflow:
   forall b1 ofs b2 delta,
   f b1 = Some(b2, delta) ->
-  Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true ->
-  0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned.
+  Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true ->
+  0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned.
 
 Hypothesis valid_different_pointers_inj:
   forall b1 ofs1 b2 ofs2 b1' delta1 b2' delta2,
   b1 <> b2 ->
-  Mem.valid_pointer m1 b1 (Int.unsigned ofs1) = true ->
-  Mem.valid_pointer m1 b2 (Int.unsigned ofs2) = true ->
+  Mem.valid_pointer m1 b1 (Ptrofs.unsigned ofs1) = true ->
+  Mem.valid_pointer m1 b2 (Ptrofs.unsigned ofs2) = true ->
   f b1 = Some (b1', delta1) ->
   f b2 = Some (b2', delta2) ->
   b1' <> b2' \/
-  Int.unsigned (Int.add ofs1 (Int.repr delta1)) <> Int.unsigned (Int.add ofs2 (Int.repr delta2)).
+  Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta1)) <> Ptrofs.unsigned (Ptrofs.add ofs2 (Ptrofs.repr delta2)).
 
 Ltac InvInject :=
   match goal with
@@ -871,20 +848,20 @@ Lemma eval_operation_inj:
 Proof.
   intros until v1; intros GL; intros. destruct op; simpl in H1; simpl; FuncInv; InvInject; TrivialExists.
   apply GL; simpl; auto.
-  apply Values.Val.add_inject; auto.
+  apply Val.offset_ptr_inject; auto.
   inv H4; simpl; auto.
   inv H4; simpl; auto.
-  apply Values.Val.add_inject; auto.
-  apply Values.Val.add_inject; auto. apply eval_shift_inj; auto.
-  apply Values.Val.add_inject; auto.
+  apply Val.add_inject; auto.
+  apply Val.add_inject; auto. apply eval_shift_inj; auto.
+  apply Val.add_inject; auto.
 
-  apply Values.Val.sub_inject; auto.
-  apply Values.Val.sub_inject; auto. apply eval_shift_inj; auto.
-  apply Values.Val.sub_inject; auto. apply eval_shift_inj; auto.
-  apply (@Values.Val.sub_inject f (Vint i) (Vint i) v v'); auto.
+  apply Val.sub_inject; auto.
+  apply Val.sub_inject; auto. apply eval_shift_inj; auto.
+  apply Val.sub_inject; auto. apply eval_shift_inj; auto.
+  apply (@Val.sub_inject f (Vint i) (Vint i) v v'); auto.
 
   inv H4; inv H2; simpl; auto.
-  apply Values.Val.add_inject; auto. inv H4; inv H2; simpl; auto.
+  apply Val.add_inject; auto. inv H4; inv H2; simpl; auto.
   inv H4; inv H2; simpl; auto.
   inv H4; inv H2; simpl; auto.
   inv H4; inv H3; simpl in H1; inv H1. simpl.
@@ -965,10 +942,10 @@ Lemma eval_addressing_inj:
   exists v2, eval_addressing ge2 sp2 addr vl2 = Some v2 /\ Val.inject f v1 v2.
 Proof.
   intros. destruct addr; simpl in H2; simpl; FuncInv; InvInject; TrivialExists.
-  apply Values.Val.add_inject; auto.
-  apply Values.Val.add_inject; auto.
-  apply Values.Val.add_inject; auto. apply eval_shift_inj; auto.
-  apply Values.Val.add_inject; auto.
+  apply Val.add_inject; auto.
+  apply Val.add_inject; auto.
+  apply Val.add_inject; auto. apply eval_shift_inj; auto.
+  apply Val.offset_ptr_inject; auto.
 Qed.
 
 End EVAL_COMPAT.
@@ -984,40 +961,40 @@ Remark valid_pointer_extends:
   forall m1 m2, Mem.extends m1 m2 ->
   forall b1 ofs b2 delta,
   Some(b1, 0) = Some(b2, delta) ->
-  Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true ->
-  Mem.valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
+  Mem.valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true ->
+  Mem.valid_pointer m2 b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true.
 Proof.
-  intros. inv H0. rewrite Int.add_zero. eapply Mem.valid_pointer_extends; eauto.
+  intros. inv H0. rewrite Ptrofs.add_zero. eapply Mem.valid_pointer_extends; eauto.
 Qed.
 
 Remark weak_valid_pointer_extends:
   forall m1 m2, Mem.extends m1 m2 ->
   forall b1 ofs b2 delta,
   Some(b1, 0) = Some(b2, delta) ->
-  Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true ->
-  Mem.weak_valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
+  Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true ->
+  Mem.weak_valid_pointer m2 b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true.
 Proof.
-  intros. inv H0. rewrite Int.add_zero. eapply Mem.weak_valid_pointer_extends; eauto.
+  intros. inv H0. rewrite Ptrofs.add_zero. eapply Mem.weak_valid_pointer_extends; eauto.
 Qed.
 
 Remark weak_valid_pointer_no_overflow_extends:
   forall m1 b1 ofs b2 delta,
   Some(b1, 0) = Some(b2, delta) ->
-  Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true ->
-  0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned.
+  Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true ->
+  0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned.
 Proof.
-  intros. inv H. rewrite Zplus_0_r. apply Int.unsigned_range_2.
+  intros. inv H. rewrite Zplus_0_r. apply Ptrofs.unsigned_range_2.
 Qed.
 
 Remark valid_different_pointers_extends:
   forall m1 b1 ofs1 b2 ofs2 b1' delta1 b2' delta2,
   b1 <> b2 ->
-  Mem.valid_pointer m1 b1 (Int.unsigned ofs1) = true ->
-  Mem.valid_pointer m1 b2 (Int.unsigned ofs2) = true ->
+  Mem.valid_pointer m1 b1 (Ptrofs.unsigned ofs1) = true ->
+  Mem.valid_pointer m1 b2 (Ptrofs.unsigned ofs2) = true ->
   Some(b1, 0) = Some (b1', delta1) ->
   Some(b2, 0) = Some (b2', delta2) ->
   b1' <> b2' \/
-  Int.unsigned(Int.add ofs1 (Int.repr delta1)) <> Int.unsigned(Int.add ofs2 (Int.repr delta2)).
+  Ptrofs.unsigned(Ptrofs.add ofs1 (Ptrofs.repr delta1)) <> Ptrofs.unsigned(Ptrofs.add ofs2 (Ptrofs.repr delta2)).
 Proof.
   intros. inv H2; inv H3. auto.
 Qed.
@@ -1096,7 +1073,7 @@ Remark symbol_address_inject:
 Proof.
   intros. unfold Genv.symbol_address. destruct (Genv.find_symbol genv id) eqn:?; auto.
   exploit (proj1 globals); eauto. intros.
-  econstructor; eauto. rewrite Int.add_zero; auto.
+  econstructor; eauto. rewrite Ptrofs.add_zero; auto.
 Qed.
 
 Lemma eval_condition_inject:
@@ -1116,34 +1093,36 @@ Qed.
 Lemma eval_addressing_inject:
   forall addr vl1 vl2 v1,
   Val.inject_list f vl1 vl2 ->
-  eval_addressing genv (Vptr sp1 Int.zero) addr vl1 = Some v1 ->
+  eval_addressing genv (Vptr sp1 Ptrofs.zero) addr vl1 = Some v1 ->
   exists v2,
-     eval_addressing genv (Vptr sp2 Int.zero) (shift_stack_addressing (Int.repr delta) addr) vl2 = Some v2
+     eval_addressing genv (Vptr sp2 Ptrofs.zero) (shift_stack_addressing delta addr) vl2 = Some v2
   /\ Val.inject f v1 v2.
 Proof.
   intros.
-  rewrite eval_shift_stack_addressing. simpl.
-  eapply eval_addressing_inj with (sp1 := Vptr sp1 Int.zero); eauto.
-  intros; apply symbol_address_inject.
+  rewrite eval_shift_stack_addressing.
+  eapply eval_addressing_inj 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 ->
   Mem.inject f m1 m2 ->
-  eval_operation genv (Vptr sp1 Int.zero) op vl1 m1 = Some v1 ->
+  eval_operation genv (Vptr sp1 Ptrofs.zero) op vl1 m1 = Some v1 ->
   exists v2,
-     eval_operation genv (Vptr sp2 Int.zero) (shift_stack_operation (Int.repr delta) op) vl2 m2 = Some v2
+     eval_operation genv (Vptr sp2 Ptrofs.zero) (shift_stack_operation delta op) vl2 m2 = Some v2
   /\ Val.inject f v1 v2.
 Proof.
   intros.
   rewrite eval_shift_stack_operation. simpl.
-  eapply eval_operation_inj with (sp1 := Vptr sp1 Int.zero) (m1 := m1); eauto.
+  eapply eval_operation_inj with (sp1 := Vptr sp1 Ptrofs.zero) (m1 := m1); eauto.
   intros; eapply Mem.valid_pointer_inject_val; eauto.
   intros; eapply Mem.weak_valid_pointer_inject_val; eauto.
   intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
   intros; eapply Mem.different_pointers_inject; eauto.
   intros; apply symbol_address_inject.
+  econstructor; eauto. rewrite Ptrofs.add_zero_l; auto. 
 Qed.
 
 End EVAL_INJECT.
diff --git a/arm/SelectLong.vp b/arm/SelectLong.vp
new file mode 100644
index 00000000..cc7a38f6
--- /dev/null
+++ b/arm/SelectLong.vp
@@ -0,0 +1,21 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*                 Xavier Leroy, INRIA Paris                           *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Instruction selection for 64-bit integer operations *)
+
+Require Import Coqlib.
+Require Import Compopts.
+Require Import AST Integers Floats.
+Require Import Op CminorSel.
+Require Import SelectOp SplitLong.
+
+(** This file is empty because we use the default implementation provided in [SplitLong]. *)
diff --git a/arm/SelectLongproof.v b/arm/SelectLongproof.v
new file mode 100644
index 00000000..a82c082c
--- /dev/null
+++ b/arm/SelectLongproof.v
@@ -0,0 +1,22 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*                 Xavier Leroy, INRIA Paris                           *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Instruction selection for 64-bit integer operations *)
+
+Require Import String Coqlib Maps Integers Floats Errors.
+Require Archi.
+Require Import AST Values Memory Globalenvs Events.
+Require Import Cminor Op CminorSel.
+Require Import SelectOp SelectOpproof SplitLong SplitLongproof.
+Require Import SelectLong.
+
+(** This file is empty because we use the default implementation provided in [SplitLong]. *)
diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp
index aec737ad..80a5d753 100644
--- a/arm/SelectOp.vp
+++ b/arm/SelectOp.vp
@@ -48,10 +48,10 @@ Open Local Scope cminorsel_scope.
 
 (** ** Constants **)
 
-Definition addrsymbol (id: ident) (ofs: int) :=
+Definition addrsymbol (id: ident) (ofs: ptrofs) :=
   Eop (Oaddrsymbol id ofs) Enil.
 
-Definition addrstack (ofs: int) :=
+Definition addrstack (ofs: ptrofs) :=
   Eop (Oaddrstack ofs) Enil.
 
 (** ** Integer logical negation *)
@@ -72,8 +72,8 @@ Nondetfunction addimm (n: int) (e: expr) :=
   if Int.eq n Int.zero then e else
   match e with
   | Eop (Ointconst m) Enil       => Eop (Ointconst(Int.add n m)) Enil
-  | Eop (Oaddrsymbol s m) Enil   => Eop (Oaddrsymbol s (Int.add n m)) Enil
-  | Eop (Oaddrstack m) Enil      => Eop (Oaddrstack (Int.add n m)) Enil
+  | Eop (Oaddrsymbol s m) Enil   => Eop (Oaddrsymbol s (Ptrofs.add (Ptrofs.of_int n) m)) Enil
+  | Eop (Oaddrstack m) Enil      => Eop (Oaddrstack (Ptrofs.add (Ptrofs.of_int n) m)) Enil
   | Eop (Oaddimm m) (t ::: Enil) => Eop (Oaddimm(Int.add n m)) (t ::: Enil)
   | _                            => Eop (Oaddimm n) (e ::: Enil)
   end.
@@ -501,6 +501,6 @@ Nondetfunction builtin_arg (e: expr) :=
   | Eop Omakelong (h ::: l ::: Enil) => BA_splitlong (BA h) (BA l)
   | Eload chunk (Ainstack ofs) Enil => BA_loadstack chunk ofs
   | Eload chunk (Aindexed ofs1) (Eop (Oaddrsymbol id ofs) Enil ::: Enil) =>
-       BA_loadglobal chunk id (Int.add ofs ofs1)
+       BA_loadglobal chunk id (Ptrofs.add ofs (Ptrofs.of_int ofs1))
   | _ => BA e
   end.
diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v
index 297e1f64..e520b3cf 100644
--- a/arm/SelectOpproof.v
+++ b/arm/SelectOpproof.v
@@ -26,6 +26,7 @@ Require Import CminorSel.
 Require Import SelectOp.
 
 Open Local Scope cminorsel_scope.
+Local Transparent Archi.ptr64.
 
 (** * Useful lemmas and tactics *)
 
@@ -123,7 +124,7 @@ Qed.
 
 Theorem eval_addrstack:
   forall le ofs,
-  exists v, eval_expr ge sp e m le (addrstack ofs) v /\ Val.lessdef (Val.add sp (Vint ofs)) v.
+  exists v, eval_expr ge sp e m le (addrstack ofs) v /\ Val.lessdef (Val.offset_ptr sp ofs) v.
 Proof.
   intros. unfold addrstack. econstructor; split.
   EvalOp. simpl; eauto.
@@ -147,11 +148,11 @@ Proof.
   red; unfold addimm; intros until x.
   predSpec Int.eq Int.eq_spec n Int.zero.
   subst n. intros. exists x; split; auto.
-  destruct x; simpl; auto. rewrite Int.add_zero. auto. rewrite Int.add_zero. auto.
+  destruct x; simpl; auto. rewrite Int.add_zero. auto. rewrite Ptrofs.add_zero. auto.
   case (addimm_match a); intros; InvEval; simpl; TrivialExists; simpl.
   rewrite Int.add_commut. auto.
-  unfold Genv.symbol_address. destruct (Genv.find_symbol ge s); simpl; auto. rewrite Int.add_commut; auto.
-  rewrite Val.add_assoc. rewrite Int.add_commut. auto.
+  unfold Genv.symbol_address. destruct (Genv.find_symbol ge s); simpl; auto. rewrite Ptrofs.add_commut; auto.
+  destruct sp; simpl; auto. rewrite Ptrofs.add_assoc. do 3 f_equal. apply Ptrofs.add_commut.
   subst x. rewrite Val.add_assoc. rewrite Int.add_commut. auto.
 Qed.
 
@@ -856,12 +857,12 @@ Proof.
   destruct (can_use_Aindexed2shift chunk); simpl.
   exists (v1 :: v0 :: nil); split. eauto with evalexpr. congruence.
   exists (Vptr b ofs :: nil); split. constructor. EvalOp. simpl. congruence. constructor.
-  simpl. rewrite Int.add_zero; auto.
+  simpl. rewrite Ptrofs.add_zero; auto.
   destruct (can_use_Aindexed2 chunk); simpl.
   exists (v1 :: v0 :: nil); split. eauto with evalexpr. congruence.
   exists (Vptr b ofs :: nil); split. constructor. EvalOp. simpl. congruence. constructor.
-  simpl. rewrite Int.add_zero; auto.
-  exists (v :: nil); split. eauto with evalexpr. subst. simpl. rewrite Int.add_zero; auto.
+  simpl. rewrite Ptrofs.add_zero; auto.
+  exists (v :: nil); split. eauto with evalexpr. subst. simpl. rewrite Ptrofs.add_zero; auto.
 Qed.
 
 Theorem eval_builtin_arg:
@@ -876,7 +877,7 @@ Proof.
 - simpl in H5. inv H5. constructor.
 - subst v. constructor; auto.
 - inv H. InvEval. simpl in H6; inv H6. constructor; auto.
-- inv H. InvEval. simpl in H6. rewrite <- Genv.shift_symbol_address in H6.
+- inv H. InvEval. simpl in H6. rewrite <- Genv.shift_symbol_address_32 in H6 by auto.
   inv H6. constructor; auto.
 - constructor; auto.
 Qed.
diff --git a/arm/ValueAOp.v b/arm/ValueAOp.v
index 64a34329..e19ddd6d 100644
--- a/arm/ValueAOp.v
+++ b/arm/ValueAOp.v
@@ -183,18 +183,18 @@ Ltac InvHyps :=
 
 Theorem eval_static_addressing_sound:
   forall addr vargs vres aargs,
-  eval_addressing ge (Vptr sp Int.zero) addr vargs = Some vres ->
+  eval_addressing ge (Vptr sp Ptrofs.zero) addr vargs = Some vres ->
   list_forall2 (vmatch bc) vargs aargs ->
   vmatch bc vres (eval_static_addressing addr aargs).
 Proof.
   unfold eval_addressing, eval_static_addressing; intros;
   destruct addr; InvHyps; eauto with va.
-  rewrite Int.add_zero_l; auto with va.
+  rewrite Ptrofs.add_zero_l; auto with va.
 Qed.
 
 Theorem eval_static_operation_sound:
   forall op vargs m vres aargs,
-  eval_operation ge (Vptr sp Int.zero) op vargs m = Some vres ->
+  eval_operation ge (Vptr sp Ptrofs.zero) op vargs m = Some vres ->
   list_forall2 (vmatch bc) vargs aargs ->
   vmatch bc vres (eval_static_operation op aargs).
 Proof.
@@ -202,7 +202,7 @@ Proof.
   destruct op; InvHyps; eauto with va.
   destruct (propagate_float_constants tt); constructor.
   destruct (propagate_float_constants tt); constructor.
-  rewrite Int.add_zero_l; eauto with va.
+  rewrite Ptrofs.add_zero_l; eauto with va.
   fold (Val.sub (Vint i) a1). auto with va.
   apply of_optbool_sound. eapply eval_static_condition_sound; eauto.
 Qed.