Support for 64-bit architectures: generic support

- Introduce Archi.ptr64 parameter.
- Define module Ptrofs of integers as wide as a pointer (64 if Archi.ptr64, 32 otherwise).
- Use Ptrofs.int as the offset type for Vptr values and anywhere pointer offsets are manipulated.
- Modify Val operations that handle pointers (e.g. Val.add, Val.sub, Val.cmpu) so that in 64-bit pointer mode it is the "long" operation (e.g. Val.addl, Val.subl, Val.cmplu) that handles pointers.
- Update the memory model accordingly.
- Modify C operations that handle pointers (e.g. addition, subtraction, comparisons) accordingly.
- Make it possible to turn off the splitting of 64-bit integers into pairs of 32-bit integers.
- Update the compiler front-end and back-end accordingly.

1 files changed, 95 insertions, 85 deletions

diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index 0e9c58b3..d8d916de 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -67,12 +67,14 @@ Lemma load_result_inject:
   forall j ty v v',
   Val.inject j v v' -> Val.has_type v ty -> Val.inject j v (Val.load_result (chunk_of_type ty) v').
 Proof.
-  destruct 1; intros; auto; destruct ty; simpl; try contradiction; econstructor; eauto.
+  intros until v'; unfold Val.has_type, Val.load_result; destruct Archi.ptr64;
+  destruct 1; intros; auto; destruct ty; simpl;
+  try contradiction; try discriminate; econstructor; eauto.
 Qed.
 
 Section PRESERVATION.
 
-Variable return_address_offset: Mach.function -> Mach.code -> int -> Prop.
+Variable return_address_offset: Mach.function -> Mach.code -> ptrofs -> Prop.
 
 Hypothesis return_address_offset_exists:
   forall f sg ros c,
@@ -100,12 +102,12 @@ Lemma unfold_transf_function:
          f.(Linear.fn_sig)
          (transl_body f fe)
          fe.(fe_size)
-         (Int.repr fe.(fe_ofs_link))
-         (Int.repr fe.(fe_ofs_retaddr)).
+         (Ptrofs.repr fe.(fe_ofs_link))
+         (Ptrofs.repr fe.(fe_ofs_retaddr)).
 Proof.
   generalize TRANSF_F. unfold transf_function.
   destruct (wt_function f); simpl negb.
-  destruct (zlt Int.max_unsigned (fe_size (make_env (function_bounds f)))).
+  destruct (zlt Ptrofs.max_unsigned (fe_size (make_env (function_bounds f)))).
   intros; discriminate.
   intros. unfold fe. unfold b. congruence.
   intros; discriminate.
@@ -118,11 +120,11 @@ Proof.
   destruct (wt_function f); simpl negb. auto. intros; discriminate.
 Qed.
 
-Lemma size_no_overflow: fe.(fe_size) <= Int.max_unsigned.
+Lemma size_no_overflow: fe.(fe_size) <= Ptrofs.max_unsigned.
 Proof.
   generalize TRANSF_F. unfold transf_function.
   destruct (wt_function f); simpl negb.
-  destruct (zlt Int.max_unsigned (fe_size (make_env (function_bounds f)))).
+  destruct (zlt Ptrofs.max_unsigned (fe_size (make_env (function_bounds f)))).
   intros; discriminate.
   intros. unfold fe. unfold b. omega.
   intros; discriminate.
@@ -143,18 +145,18 @@ Local Opaque Z.add Z.mul Z.divide.
 Lemma contains_get_stack:
   forall spec m ty sp ofs,
   m |= contains (chunk_of_type ty) sp ofs spec ->
-  exists v, load_stack m (Vptr sp Int.zero) ty (Int.repr ofs) = Some v /\ spec v.
+  exists v, load_stack m (Vptr sp Ptrofs.zero) ty (Ptrofs.repr ofs) = Some v /\ spec v.
 Proof.
   intros. unfold load_stack. 
-  replace (Val.add (Vptr sp Int.zero) (Vint (Int.repr ofs))) with (Vptr sp (Int.repr ofs)).
+  replace (Val.offset_ptr (Vptr sp Ptrofs.zero) (Ptrofs.repr ofs)) with (Vptr sp (Ptrofs.repr ofs)).
   eapply loadv_rule; eauto.
-  simpl. rewrite Int.add_zero_l; auto.
+  simpl. rewrite Ptrofs.add_zero_l; auto.
 Qed.
 
 Lemma hasvalue_get_stack:
   forall ty m sp ofs v,
   m |= hasvalue (chunk_of_type ty) sp ofs v ->
-  load_stack m (Vptr sp Int.zero) ty (Int.repr ofs) = Some v.
+  load_stack m (Vptr sp Ptrofs.zero) ty (Ptrofs.repr ofs) = Some v.
 Proof.
   intros. exploit contains_get_stack; eauto. intros (v' & A & B). congruence.
 Qed.
@@ -164,13 +166,13 @@ Lemma contains_set_stack:
   m |= contains (chunk_of_type ty) sp ofs spec1 ** P ->
   spec (Val.load_result (chunk_of_type ty) v) ->
   exists m',
-      store_stack m (Vptr sp Int.zero) ty (Int.repr ofs) v = Some m'
+      store_stack m (Vptr sp Ptrofs.zero) ty (Ptrofs.repr ofs) v = Some m'
   /\ m' |= contains (chunk_of_type ty) sp ofs spec ** P.
 Proof.
   intros. unfold store_stack. 
-  replace (Val.add (Vptr sp Int.zero) (Vint (Int.repr ofs))) with (Vptr sp (Int.repr ofs)).
+  replace (Val.offset_ptr (Vptr sp Ptrofs.zero) (Ptrofs.repr ofs)) with (Vptr sp (Ptrofs.repr ofs)).
   eapply storev_rule; eauto.
-  simpl. rewrite Int.add_zero_l; auto.
+  simpl. rewrite Ptrofs.add_zero_l; auto.
 Qed.
 
 (** [contains_locations j sp pos bound sl ls] is a separation logic assertion
@@ -184,7 +186,7 @@ Qed.
 
 Program Definition contains_locations (j: meminj) (sp: block) (pos bound: Z) (sl: slot) (ls: locset) : massert := {|
   m_pred := fun m =>
-    (8 | pos) /\ 0 <= pos /\ pos + 4 * bound <= Int.modulus /\
+    (8 | pos) /\ 0 <= pos /\ pos + 4 * bound <= Ptrofs.modulus /\
     Mem.range_perm m sp pos (pos + 4 * bound) Cur Freeable /\
     forall ofs ty, 0 <= ofs -> ofs + typesize ty <= bound -> (typealign ty | ofs) ->
     exists v, Mem.load (chunk_of_type ty) m sp (pos + 4 * ofs) = Some v
@@ -225,13 +227,13 @@ Lemma get_location:
   m |= contains_locations j sp pos bound sl ls ->
   0 <= ofs -> ofs + typesize ty <= bound -> (typealign ty | ofs) ->
   exists v,
-     load_stack m (Vptr sp Int.zero) ty (Int.repr (pos + 4 * ofs)) = Some v
+     load_stack m (Vptr sp Ptrofs.zero) ty (Ptrofs.repr (pos + 4 * ofs)) = Some v
   /\ Val.inject j (ls (S sl ofs ty)) v.
 Proof.
   intros. destruct H as (D & E & F & G & H).
   exploit H; eauto. intros (v & U & V). exists v; split; auto.
-  unfold load_stack; simpl. rewrite Int.add_zero_l, Int.unsigned_repr; auto.
-  unfold Int.max_unsigned. generalize (typesize_pos ty). omega.
+  unfold load_stack; simpl. rewrite Ptrofs.add_zero_l, Ptrofs.unsigned_repr; auto.
+  unfold Ptrofs.max_unsigned. generalize (typesize_pos ty). omega.
 Qed.
 
 Lemma set_location:
@@ -240,7 +242,7 @@ Lemma set_location:
   0 <= ofs -> ofs + typesize ty <= bound -> (typealign ty | ofs) ->
   Val.inject j v v' ->
   exists m',
-     store_stack m (Vptr sp Int.zero) ty (Int.repr (pos + 4 * ofs)) v' = Some m'
+     store_stack m (Vptr sp Ptrofs.zero) ty (Ptrofs.repr (pos + 4 * ofs)) v' = Some m'
   /\ m' |= contains_locations j sp pos bound sl (Locmap.set (S sl ofs ty) v ls) ** P.
 Proof.
   intros. destruct H as (A & B & C). destruct A as (D & E & F & G & H).
@@ -249,8 +251,8 @@ Proof.
   assert (PERM: Mem.range_perm m' sp pos (pos + 4 * bound) Cur Freeable).
   { red; intros; eauto with mem. }
   exists m'; split.
-- unfold store_stack; simpl. rewrite Int.add_zero_l, Int.unsigned_repr; eauto.
-  unfold Int.max_unsigned. generalize (typesize_pos ty). omega.
+- unfold store_stack; simpl. rewrite Ptrofs.add_zero_l, Ptrofs.unsigned_repr; eauto.
+  unfold Ptrofs.max_unsigned. generalize (typesize_pos ty). omega.
 - simpl. intuition auto.
 + unfold Locmap.set. 
   destruct (Loc.eq (S sl ofs ty) (S sl ofs0 ty0)); [|destruct (Loc.diff_dec (S sl ofs ty) (S sl ofs0 ty0))].
@@ -258,7 +260,7 @@ Proof.
   inv e. rename ofs0 into ofs. rename ty0 into ty.
   exists (Val.load_result (chunk_of_type ty) v'); split.
   eapply Mem.load_store_similar_2; eauto. omega. 
-  inv H3; destruct (chunk_of_type ty); simpl; econstructor; eauto.
+  apply Val.load_result_inject; auto.
 * (* different locations *)
   exploit H; eauto. intros (v0 & X & Y). exists v0; split; auto.
   rewrite <- X; eapply Mem.load_store_other; eauto.
@@ -366,8 +368,8 @@ represents the Linear stack data. *)
 Definition frame_contents_1 (j: meminj) (sp: block) (ls ls0: locset) (parent retaddr: val) :=
     contains_locations j sp fe.(fe_ofs_local) b.(bound_local) Local ls
  ** contains_locations j sp fe_ofs_arg b.(bound_outgoing) Outgoing ls
- ** hasvalue Mint32 sp fe.(fe_ofs_link) parent
- ** hasvalue Mint32 sp fe.(fe_ofs_retaddr) retaddr
+ ** hasvalue Mptr sp fe.(fe_ofs_link) parent
+ ** hasvalue Mptr sp fe.(fe_ofs_retaddr) retaddr
  ** contains_callee_saves j sp fe.(fe_ofs_callee_save) b.(used_callee_save) ls0.
 
 Definition frame_contents (j: meminj) (sp: block) (ls ls0: locset) (parent retaddr: val) :=
@@ -382,7 +384,7 @@ Lemma frame_get_local:
   m |= frame_contents j sp ls ls0 parent retaddr ** P ->
   slot_within_bounds b Local ofs ty -> slot_valid f Local ofs ty = true ->
   exists v,
-     load_stack m (Vptr sp Int.zero) ty (Int.repr (offset_local fe ofs)) = Some v
+     load_stack m (Vptr sp Ptrofs.zero) ty (Ptrofs.repr (offset_local fe ofs)) = Some v
   /\ Val.inject j (ls (S Local ofs ty)) v.
 Proof.
   unfold frame_contents, frame_contents_1; intros. unfold slot_valid in H1; InvBooleans.
@@ -395,7 +397,7 @@ Lemma frame_get_outgoing:
   m |= frame_contents j sp ls ls0 parent retaddr ** P ->
   slot_within_bounds b Outgoing ofs ty -> slot_valid f Outgoing ofs ty = true ->
   exists v,
-     load_stack m (Vptr sp Int.zero) ty (Int.repr (offset_arg ofs)) = Some v
+     load_stack m (Vptr sp Ptrofs.zero) ty (Ptrofs.repr (offset_arg ofs)) = Some v
   /\ Val.inject j (ls (S Outgoing ofs ty)) v.
 Proof.
   unfold frame_contents, frame_contents_1; intros. unfold slot_valid in H1; InvBooleans.
@@ -406,20 +408,20 @@ Qed.
 Lemma frame_get_parent:
   forall j sp ls ls0 parent retaddr m P,
   m |= frame_contents j sp ls ls0 parent retaddr ** P ->
-  load_stack m (Vptr sp Int.zero) Tint (Int.repr fe.(fe_ofs_link)) = Some parent.
+  load_stack m (Vptr sp Ptrofs.zero) Tptr (Ptrofs.repr fe.(fe_ofs_link)) = Some parent.
 Proof.
   unfold frame_contents, frame_contents_1; intros.
-  apply mconj_proj1 in H. apply sep_proj1 in H. apply sep_pick3 in H. 
+  apply mconj_proj1 in H. apply sep_proj1 in H. apply sep_pick3 in H. rewrite <- chunk_of_Tptr in H.
   eapply hasvalue_get_stack; eauto.
 Qed.
 
 Lemma frame_get_retaddr:
   forall j sp ls ls0 parent retaddr m P,
   m |= frame_contents j sp ls ls0 parent retaddr ** P ->
-  load_stack m (Vptr sp Int.zero) Tint (Int.repr fe.(fe_ofs_retaddr)) = Some retaddr.
+  load_stack m (Vptr sp Ptrofs.zero) Tptr (Ptrofs.repr fe.(fe_ofs_retaddr)) = Some retaddr.
 Proof.
   unfold frame_contents, frame_contents_1; intros.
-  apply mconj_proj1 in H. apply sep_proj1 in H. apply sep_pick4 in H. 
+  apply mconj_proj1 in H. apply sep_proj1 in H. apply sep_pick4 in H. rewrite <- chunk_of_Tptr in H.
   eapply hasvalue_get_stack; eauto.
 Qed.
 
@@ -431,7 +433,7 @@ Lemma frame_set_local:
   slot_within_bounds b Local ofs ty -> slot_valid f Local ofs ty = true ->
   Val.inject j v v' ->
   exists m',
-     store_stack m (Vptr sp Int.zero) ty (Int.repr (offset_local fe ofs)) v' = Some m'
+     store_stack m (Vptr sp Ptrofs.zero) ty (Ptrofs.repr (offset_local fe ofs)) v' = Some m'
   /\ m' |= frame_contents j sp (Locmap.set (S Local ofs ty) v ls) ls0 parent retaddr ** P.
 Proof.
   intros. unfold frame_contents in H.
@@ -456,7 +458,7 @@ Lemma frame_set_outgoing:
   slot_within_bounds b Outgoing ofs ty -> slot_valid f Outgoing ofs ty = true ->
   Val.inject j v v' ->
   exists m',
-     store_stack m (Vptr sp Int.zero) ty (Int.repr (offset_arg ofs)) v' = Some m'
+     store_stack m (Vptr sp Ptrofs.zero) ty (Ptrofs.repr (offset_arg ofs)) v' = Some m'
   /\ m' |= frame_contents j sp (Locmap.set (S Outgoing ofs ty) v ls) ls0 parent retaddr ** P.
 Proof.
   intros. unfold frame_contents in H.
@@ -855,7 +857,8 @@ Qed.
 Remark destroyed_by_store_caller_save:
   forall chunk addr, no_callee_saves (destroyed_by_store chunk addr).
 Proof.
-  unfold no_callee_saves; destruct chunk; reflexivity.
+Local Transparent destroyed_by_store.
+  unfold no_callee_saves, destroyed_by_store; intros; destruct chunk; try reflexivity; destruct Archi.ptr64; reflexivity.
 Qed.
 
 Remark destroyed_by_cond_caller_save:
@@ -939,12 +942,13 @@ Lemma save_callee_save_rec_correct:
   agree_regs j ls rs ->
   exists rs', exists m',
      star step tge
-        (State cs fb (Vptr sp Int.zero) (save_callee_save_rec l pos k) rs m)
-     E0 (State cs fb (Vptr sp Int.zero) k rs' m')
+        (State cs fb (Vptr sp Ptrofs.zero) (save_callee_save_rec l pos k) rs m)
+     E0 (State cs fb (Vptr sp Ptrofs.zero) k rs' m')
   /\ m' |= contains_callee_saves j sp pos l ls ** P
   /\ (forall ofs k p, Mem.perm m sp ofs k p -> Mem.perm m' sp ofs k p)
   /\ agree_regs j ls rs'.
 Proof.
+Local Opaque mreg_type.
   induction l as [ | r l]; simpl; intros until P; intros CS SEP AG.
 - exists rs, m. 
   split. apply star_refl.
@@ -1029,8 +1033,8 @@ Lemma save_callee_save_correct:
   let rs1 := undef_regs destroyed_at_function_entry rs in
   exists rs', exists m',
      star step tge
-        (State cs fb (Vptr sp Int.zero) (save_callee_save fe k) rs1 m)
-     E0 (State cs fb (Vptr sp Int.zero) k rs' m')
+        (State cs fb (Vptr sp Ptrofs.zero) (save_callee_save fe k) rs1 m)
+     E0 (State cs fb (Vptr sp Ptrofs.zero) k rs' m')
   /\ m' |= contains_callee_saves j sp fe.(fe_ofs_callee_save) b.(used_callee_save) ls0 ** P
   /\ (forall ofs k p, Mem.perm m sp ofs k p -> Mem.perm m' sp ofs k p)
   /\ agree_regs j ls1 rs'.
@@ -1071,15 +1075,15 @@ Lemma function_prologue_correct:
   ls1 = LTL.undef_regs destroyed_at_function_entry (LTL.call_regs ls) ->
   rs1 = undef_regs destroyed_at_function_entry rs ->
   Mem.alloc m1 0 f.(Linear.fn_stacksize) = (m2, sp) ->
-  Val.has_type parent Tint -> Val.has_type ra Tint ->
+  Val.has_type parent Tptr -> Val.has_type ra Tptr ->
   m1' |= minjection j m1 ** globalenv_inject ge j ** P ->
   exists j', exists rs', exists m2', exists sp', exists m3', exists m4', exists m5',
      Mem.alloc m1' 0 tf.(fn_stacksize) = (m2', sp')
-  /\ store_stack m2' (Vptr sp' Int.zero) Tint tf.(fn_link_ofs) parent = Some m3'
-  /\ store_stack m3' (Vptr sp' Int.zero) Tint tf.(fn_retaddr_ofs) ra = Some m4'
+  /\ store_stack m2' (Vptr sp' Ptrofs.zero) Tptr tf.(fn_link_ofs) parent = Some m3'
+  /\ store_stack m3' (Vptr sp' Ptrofs.zero) Tptr tf.(fn_retaddr_ofs) ra = Some m4'
   /\ star step tge
-         (State cs fb (Vptr sp' Int.zero) (save_callee_save fe k) rs1 m4')
-      E0 (State cs fb (Vptr sp' Int.zero) k rs' m5')
+         (State cs fb (Vptr sp' Ptrofs.zero) (save_callee_save fe k) rs1 m4')
+      E0 (State cs fb (Vptr sp' Ptrofs.zero) k rs' m5')
   /\ agree_regs j' ls1 rs'
   /\ agree_locs ls1 ls0
   /\ m5' |= frame_contents j' sp' ls1 ls0 parent ra ** minjection j' m2 ** globalenv_inject ge j' ** P
@@ -1113,17 +1117,17 @@ Local Opaque b fe.
   (* Dividing up the frame *)
   apply (frame_env_separated b) in SEP. replace (make_env b) with fe in SEP by auto.
   (* Store of parent *)
-  rewrite sep_swap3 in SEP. 
-  apply (range_contains Mint32) in SEP; [|tauto].
-  exploit (contains_set_stack (fun v' => v' = parent) parent (fun _ => True) m2' Tint).
-  eexact SEP. apply Val.load_result_same; auto.
+  rewrite sep_swap3 in SEP.
+  apply (range_contains Mptr) in SEP; [|tauto].
+  exploit (contains_set_stack (fun v' => v' = parent) parent (fun _ => True) m2' Tptr).
+  rewrite chunk_of_Tptr; eexact SEP. apply Val.load_result_same; auto.
   clear SEP; intros (m3' & STORE_PARENT & SEP).
   rewrite sep_swap3 in SEP.
   (* Store of return address *)
   rewrite sep_swap4 in SEP.
-  apply (range_contains Mint32) in SEP; [|tauto].
-  exploit (contains_set_stack (fun v' => v' = ra) ra (fun _ => True) m3' Tint).
-  eexact SEP. apply Val.load_result_same; auto.
+  apply (range_contains Mptr) in SEP; [|tauto].
+  exploit (contains_set_stack (fun v' => v' = ra) ra (fun _ => True) m3' Tptr).
+  rewrite chunk_of_Tptr; eexact SEP. apply Val.load_result_same; auto.
   clear SEP; intros (m4' & STORE_RETADDR & SEP).
   rewrite sep_swap4 in SEP.
   (* Saving callee-save registers *)
@@ -1147,7 +1151,8 @@ Local Opaque b fe.
   rewrite sep_swap in SEP.
   (* Now we frame this *)
   assert (SEPFINAL: m5' |= frame_contents j' sp' ls1 ls0 parent ra ** minjection j' m2 ** globalenv_inject ge j' ** P).
-  { eapply frame_mconj. eexact SEPCONJ. 
+  { eapply frame_mconj. eexact SEPCONJ.
+    rewrite chunk_of_Tptr in SEP.  
     unfold frame_contents_1; rewrite ! sep_assoc. exact SEP.
     assert (forall ofs k p, Mem.perm m2' sp' ofs k p -> Mem.perm m5' sp' ofs k p).
     { intros. apply PERMS. 
@@ -1198,12 +1203,13 @@ Lemma restore_callee_save_rec_correct:
   (forall r, In r l -> mreg_within_bounds b r) ->
   exists rs',
     star step tge
-      (State cs fb (Vptr sp Int.zero) (restore_callee_save_rec l ofs k) rs m)
-   E0 (State cs fb (Vptr sp Int.zero) k rs' m)
+      (State cs fb (Vptr sp Ptrofs.zero) (restore_callee_save_rec l ofs k) rs m)
+   E0 (State cs fb (Vptr sp Ptrofs.zero) k rs' m)
   /\ (forall r, In r l -> Val.inject j (ls0 (R r)) (rs' r))
   /\ (forall r, ~(In r l) -> rs' r = rs r)
   /\ agree_unused ls0 rs'.
 Proof.
+Local Opaque mreg_type.
   induction l as [ | r l]; simpl; intros.
 - (* base case *)
   exists rs. intuition auto. apply star_refl.
@@ -1242,8 +1248,8 @@ Lemma restore_callee_save_correct:
   agree_unused j ls0 rs ->
   exists rs',
     star step tge
-       (State cs fb (Vptr sp Int.zero) (restore_callee_save fe k) rs m)
-    E0 (State cs fb (Vptr sp Int.zero) k rs' m)
+       (State cs fb (Vptr sp Ptrofs.zero) (restore_callee_save fe k) rs m)
+    E0 (State cs fb (Vptr sp Ptrofs.zero) k rs' m)
   /\ (forall r,
         is_callee_save r = true -> Val.inject j (ls0 (R r)) (rs' r))
   /\ (forall r,
@@ -1277,12 +1283,12 @@ Lemma function_epilogue_correct:
   j sp = Some(sp', fe.(fe_stack_data)) ->
   Mem.free m sp 0 f.(Linear.fn_stacksize) = Some m1 ->
   exists rs1, exists m1',
-     load_stack m' (Vptr sp' Int.zero) Tint tf.(fn_link_ofs) = Some pa
-  /\ load_stack m' (Vptr sp' Int.zero) Tint tf.(fn_retaddr_ofs) = Some ra
+     load_stack m' (Vptr sp' Ptrofs.zero) Tptr tf.(fn_link_ofs) = Some pa
+  /\ load_stack m' (Vptr sp' Ptrofs.zero) Tptr tf.(fn_retaddr_ofs) = Some ra
   /\ Mem.free m' sp' 0 tf.(fn_stacksize) = Some m1'
   /\ star step tge
-       (State cs fb (Vptr sp' Int.zero) (restore_callee_save fe k) rs m')
-    E0 (State cs fb (Vptr sp' Int.zero) k rs1 m')
+       (State cs fb (Vptr sp' Ptrofs.zero) (restore_callee_save fe k) rs m')
+    E0 (State cs fb (Vptr sp' Ptrofs.zero) k rs1 m')
   /\ agree_regs j (return_regs ls0 ls) rs1
   /\ agree_callee_save (return_regs ls0 ls) ls0
   /\ m1' |= minjection j m1 ** P.
@@ -1304,8 +1310,8 @@ Proof.
   (* Reloading the back link and return address *)
   unfold frame_contents in SEP; apply mconj_proj1 in SEP.
   unfold frame_contents_1 in SEP; rewrite ! sep_assoc in SEP.
-  exploit (hasvalue_get_stack Tint). eapply sep_pick3; eexact SEP. intros LOAD_LINK.
-  exploit (hasvalue_get_stack Tint). eapply sep_pick4; eexact SEP. intros LOAD_RETADDR.
+  exploit (hasvalue_get_stack Tptr). rewrite chunk_of_Tptr. eapply sep_pick3; eexact SEP. intros LOAD_LINK.
+  exploit (hasvalue_get_stack Tptr). rewrite chunk_of_Tptr. eapply sep_pick4; eexact SEP. intros LOAD_RETADDR.
   clear SEP.
   (* Conclusions *)
   rewrite unfold_transf_function; simpl.
@@ -1353,15 +1359,15 @@ Inductive match_stacks (j: meminj):
         (TRF: transf_function f = OK trf)
         (TRC: transl_code (make_env (function_bounds f)) c = c')
         (INJ: j sp = Some(sp', (fe_stack_data (make_env (function_bounds f)))))
-        (TY_RA: Val.has_type ra Tint)
+        (TY_RA: Val.has_type ra Tptr)
         (AGL: agree_locs f ls (parent_locset cs))
         (ARGS: forall ofs ty,
            In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments sg)) ->
            slot_within_bounds (function_bounds f) Outgoing ofs ty)
         (STK: match_stacks j cs cs' (Linear.fn_sig f)),
       match_stacks j
-                   (Linear.Stackframe f (Vptr sp Int.zero) ls c :: cs)
-                   (Stackframe fb (Vptr sp' Int.zero) ra c' :: cs')
+                   (Linear.Stackframe f (Vptr sp Ptrofs.zero) ls c :: cs)
+                   (Stackframe fb (Vptr sp' Ptrofs.zero) ra c' :: cs')
                    sg.
 
 (** Invariance with respect to change of memory injection. *)
@@ -1409,17 +1415,17 @@ Qed.
 Lemma match_stacks_type_sp:
   forall j cs cs' sg,
   match_stacks j cs cs' sg ->
-  Val.has_type (parent_sp cs') Tint.
+  Val.has_type (parent_sp cs') Tptr.
 Proof.
-  induction 1; simpl; auto.
-Qed.
+  induction 1; unfold parent_sp. apply Val.Vnullptr_has_type. apply Val.Vptr_has_type.
+Qed. 
 
 Lemma match_stacks_type_retaddr:
   forall j cs cs' sg,
   match_stacks j cs cs' sg ->
-  Val.has_type (parent_ra cs') Tint.
+  Val.has_type (parent_ra cs') Tptr.
 Proof.
-  induction 1; simpl; auto.
+  induction 1; unfold parent_ra. apply Val.Vnullptr_has_type. auto.
 Qed.
 
 (** * Syntactic properties of the translation *)
@@ -1700,11 +1706,11 @@ Hypothesis SEP: m' |= frame_contents f j sp' ls ls0 parent retaddr ** minjection
 
 Lemma transl_builtin_arg_correct:
   forall a v,
-  eval_builtin_arg ge ls (Vptr sp Int.zero) m a v ->
+  eval_builtin_arg ge ls (Vptr sp Ptrofs.zero) m a v ->
   (forall l, In l (params_of_builtin_arg a) -> loc_valid f l = true) ->
   (forall sl ofs ty, In (S sl ofs ty) (params_of_builtin_arg a) -> slot_within_bounds b sl ofs ty) ->
   exists v',
-     eval_builtin_arg ge rs (Vptr sp' Int.zero) m' (transl_builtin_arg fe a) v'
+     eval_builtin_arg ge rs (Vptr sp' Ptrofs.zero) m' (transl_builtin_arg fe a) v'
   /\ Val.inject j v v'.
 Proof.
   assert (SYMB: forall id ofs, Val.inject j (Senv.symbol_address ge id ofs) (Senv.symbol_address ge id ofs)).
@@ -1712,7 +1718,7 @@ Proof.
     { eapply globalenv_inject_preserves_globals. eapply sep_proj2. eapply sep_proj2. eexact SEP. }
     intros; unfold Senv.symbol_address; simpl; unfold Genv.symbol_address.
     destruct (Genv.find_symbol ge id) eqn:FS; auto.
-    destruct G. econstructor. eauto. rewrite Int.add_zero; auto. }
+    destruct G. econstructor. eauto. rewrite Ptrofs.add_zero; auto. }
 Local Opaque fe.
   induction 1; simpl; intros VALID BOUNDS.
 - assert (loc_valid f x = true) by auto.
@@ -1724,13 +1730,13 @@ Local Opaque fe.
 - econstructor; eauto with barg.
 - econstructor; eauto with barg.
 - econstructor; eauto with barg.
-- set (ofs' := Int.add ofs (Int.repr (fe_stack_data fe))).
+- set (ofs' := Ptrofs.add ofs (Ptrofs.repr (fe_stack_data fe))).
   apply sep_proj2 in SEP. apply sep_proj1 in SEP. exploit loadv_parallel_rule; eauto.
-  instantiate (1 := Val.add (Vptr sp' Int.zero) (Vint ofs')). 
-  simpl. rewrite ! Int.add_zero_l. econstructor; eauto.
+  instantiate (1 := Val.offset_ptr (Vptr sp' Ptrofs.zero) ofs').
+  simpl. rewrite ! Ptrofs.add_zero_l. econstructor; eauto.
   intros (v' & A & B). exists v'; split; auto. constructor; auto. 
 - econstructor; split; eauto with barg.
-  unfold Val.add. rewrite ! Int.add_zero_l. econstructor; eauto.
+  unfold Val.offset_ptr. rewrite ! Ptrofs.add_zero_l. econstructor; eauto.
 - apply sep_proj2 in SEP. apply sep_proj1 in SEP. exploit loadv_parallel_rule; eauto.
   intros (v' & A & B). exists v'; auto with barg.
 - econstructor; split; eauto with barg. 
@@ -1742,11 +1748,11 @@ Qed.
 
 Lemma transl_builtin_args_correct:
   forall al vl,
-  eval_builtin_args ge ls (Vptr sp Int.zero) m al vl ->
+  eval_builtin_args ge ls (Vptr sp Ptrofs.zero) m al vl ->
   (forall l, In l (params_of_builtin_args al) -> loc_valid f l = true) ->
   (forall sl ofs ty, In (S sl ofs ty) (params_of_builtin_args al) -> slot_within_bounds b sl ofs ty) ->
   exists vl',
-     eval_builtin_args ge rs (Vptr sp' Int.zero) m' (List.map (transl_builtin_arg fe) al) vl'
+     eval_builtin_args ge rs (Vptr sp' Ptrofs.zero) m' (List.map (transl_builtin_arg fe) al) vl'
   /\ Val.inject_list j vl vl'.
 Proof.
   induction 1; simpl; intros VALID BOUNDS.
@@ -1798,8 +1804,8 @@ Inductive match_states: Linear.state -> Mach.state -> Prop :=
                  ** stack_contents j cs cs'
                  ** minjection j m
                  ** globalenv_inject ge j),
-      match_states (Linear.State cs f (Vptr sp Int.zero) c ls m)
-                   (Mach.State cs' fb (Vptr sp' Int.zero) (transl_code (make_env (function_bounds f)) c) rs m')
+      match_states (Linear.State cs f (Vptr sp Ptrofs.zero) c ls m)
+                   (Mach.State cs' fb (Vptr sp' Ptrofs.zero) (transl_code (make_env (function_bounds f)) c) rs m')
   | match_states_call:
       forall cs f ls m cs' fb rs m' j tf
         (STACKS: match_stacks j cs cs' (Linear.funsig f))
@@ -1882,7 +1888,7 @@ Proof.
                end).
   eapply frame_undef_regs with (rl := destroyed_by_setstack ty) in SEP.
   assert (A: exists m'',
-              store_stack m' (Vptr sp' Int.zero) ty (Int.repr ofs') (rs0 src) = Some m''
+              store_stack m' (Vptr sp' Ptrofs.zero) ty (Ptrofs.repr ofs') (rs0 src) = Some m''
            /\ m'' |= frame_contents f j sp' (Locmap.set (S sl ofs ty) (rs (R src))
                                                (LTL.undef_regs (destroyed_by_setstack ty) rs))
                                             (parent_locset s) (parent_sp cs') (parent_ra cs')
@@ -1902,7 +1908,7 @@ Proof.
 
 - (* Lop *)
   assert (exists v',
-          eval_operation ge (Vptr sp' Int.zero) (transl_op (make_env (function_bounds f)) op) rs0##args m' = Some v'
+          eval_operation ge (Vptr sp' Ptrofs.zero) (transl_op (make_env (function_bounds f)) op) rs0##args m' = Some v'
        /\ Val.inject j v v').
   eapply eval_operation_inject; eauto.
   eapply globalenv_inject_preserves_globals. eapply sep_proj2. eapply sep_proj2. eapply sep_proj2. eexact SEP.
@@ -1921,7 +1927,7 @@ Proof.
 
 - (* Lload *)
   assert (exists a',
-          eval_addressing ge (Vptr sp' Int.zero) (transl_addr (make_env (function_bounds f)) addr) rs0##args = Some a'
+          eval_addressing ge (Vptr sp' Ptrofs.zero) (transl_addr (make_env (function_bounds f)) addr) rs0##args = Some a'
        /\ Val.inject j a a').
   eapply eval_addressing_inject; eauto.
   eapply globalenv_inject_preserves_globals. eapply sep_proj2. eapply sep_proj2. eapply sep_proj2. eexact SEP.
@@ -1941,7 +1947,7 @@ Proof.
 
 - (* Lstore *)
   assert (exists a',
-          eval_addressing ge (Vptr sp' Int.zero) (transl_addr (make_env (function_bounds f)) addr) rs0##args = Some a'
+          eval_addressing ge (Vptr sp' Ptrofs.zero) (transl_addr (make_env (function_bounds f)) addr) rs0##args = Some a'
        /\ Val.inject j a a').
   eapply eval_addressing_inject; eauto.
   eapply globalenv_inject_preserves_globals. eapply sep_proj2. eapply sep_proj2. eapply sep_proj2. eexact SEP.
@@ -1972,7 +1978,7 @@ Proof.
   apply plus_one. econstructor; eauto.
   econstructor; eauto.
   econstructor; eauto with coqlib.
-  simpl; auto.
+  apply Val.Vptr_has_type.
   intros; red.
     apply Zle_trans with (size_arguments (Linear.funsig f')); auto.
     apply loc_arguments_bounded; auto.
@@ -2150,7 +2156,11 @@ Lemma transf_final_states:
   match_states st1 st2 -> Linear.final_state st1 r -> Mach.final_state st2 r.
 Proof.
   intros. inv H0. inv H. inv STACKS.
-  assert (R: exists r, loc_result signature_main = One r) by (econstructor; reflexivity). 
+  assert (R: exists r, loc_result signature_main = One r).
+  { destruct (loc_result signature_main) as [r1 | r1 r2] eqn:LR.
+  - exists r1; auto.
+  - generalize (loc_result_type signature_main). rewrite LR. discriminate.
+  }
   destruct R as [rres EQ]. rewrite EQ in H1. simpl in H1.
   generalize (AGREGS rres). rewrite H1. intros A; inv A.
   econstructor; eauto.