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, 323 insertions, 142 deletions

diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index 8bc97b99..3a35b87e 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -245,6 +245,19 @@ Proof.
   intros. unfold make_floatconst. econstructor. reflexivity.
 Qed.
 
+Lemma make_ptrofsconst_correct:
+  forall n e le m,
+  eval_expr ge e le m (make_ptrofsconst n) (Vptrofs (Ptrofs.repr n)).
+Proof.
+  intros. unfold Vptrofs, make_ptrofsconst. destruct Archi.ptr64 eqn:SF.
+- replace (Ptrofs.to_int64 (Ptrofs.repr n)) with (Int64.repr n).
+  apply make_longconst_correct.
+  symmetry; auto with ptrofs.
+- replace (Ptrofs.to_int (Ptrofs.repr n)) with (Int.repr n).
+  apply make_intconst_correct.
+  symmetry; auto with ptrofs.
+Qed.
+
 Lemma make_singleoffloat_correct:
   forall a n e le m,
   eval_expr ge e le m a (Vfloat n) ->
@@ -276,38 +289,62 @@ Hint Resolve make_intconst_correct make_floatconst_correct make_longconst_correc
 Hint Constructors eval_expr eval_exprlist: cshm.
 Hint Extern 2 (@eq trace _ _) => traceEq: cshm.
 
-Lemma make_cmp_ne_zero_correct:
+Lemma make_cmpu_ne_zero_correct:
   forall e le m a n,
   eval_expr ge e le m a (Vint n) ->
-  eval_expr ge e le m (make_cmp_ne_zero a) (Vint (if Int.eq n Int.zero then Int.zero else Int.one)).
+  eval_expr ge e le m (make_cmpu_ne_zero a) (Vint (if Int.eq n Int.zero then Int.zero else Int.one)).
 Proof.
   intros.
-  assert (DEFAULT: eval_expr ge e le m (Ebinop (Ocmp Cne) a (make_intconst Int.zero))
+  assert (DEFAULT: eval_expr ge e le m (Ebinop (Ocmpu Cne) a (make_intconst Int.zero))
                                        (Vint (if Int.eq n Int.zero then Int.zero else Int.one))).
-    econstructor; eauto with cshm. simpl. unfold Val.cmp, Val.cmp_bool.
-    unfold Int.cmp. destruct (Int.eq n Int.zero); auto.
+  { econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool.
+    unfold Int.cmpu. destruct (Int.eq n Int.zero); auto. }
   assert (CMP: forall ob,
                Val.of_optbool ob = Vint n ->
                n = (if Int.eq n Int.zero then Int.zero else Int.one)).
-    intros. destruct ob; simpl in H0; inv H0. destruct b; inv H2.
+  { intros. destruct ob; simpl in H0; inv H0. destruct b; inv H2.
     rewrite Int.eq_false. auto. apply Int.one_not_zero.
-    rewrite Int.eq_true. auto.
+    rewrite Int.eq_true. auto. }
   destruct a; simpl; auto. destruct b; auto.
-  inv H. econstructor; eauto. rewrite H6. decEq. decEq.
-  simpl in H6. inv H6. unfold Val.cmp in H0. eauto.
-  inv H. econstructor; eauto. rewrite H6. decEq. decEq.
-  simpl in H6. inv H6. unfold Val.cmp in H0. eauto.
-  inv H. econstructor; eauto. rewrite H6. decEq. decEq.
-  simpl in H6. inv H6. unfold Val.cmp in H0. eauto.
-  inv H. econstructor; eauto. rewrite H6. decEq. decEq.
-  simpl in H6. unfold Val.cmpfs in H6.
-  destruct (Val.cmpfs_bool c v1 v2) as [[]|]; inv H6; reflexivity.
-  inv H. econstructor; eauto. rewrite H6. decEq. decEq.
+- inv H. econstructor; eauto. rewrite H6. decEq. decEq.
+  simpl in H6. inv H6. eauto.
+- inv H. econstructor; eauto. rewrite H6. decEq. decEq.
+  simpl in H6. inv H6. eauto.
+- inv H. econstructor; eauto. rewrite H6. decEq. decEq.
+  simpl in H6. inv H6. eauto.
+- inv H. econstructor; eauto. rewrite H6. decEq. decEq.
+  simpl in H6. inv H6. eauto.
+- inv H. econstructor; eauto. rewrite H6. decEq. decEq.
   simpl in H6. unfold Val.cmpl in H6.
   destruct (Val.cmpl_bool c v1 v2) as [[]|]; inv H6; reflexivity.
-  inv H. econstructor; eauto. rewrite H6. decEq. decEq.
+- inv H. econstructor; eauto. rewrite H6. decEq. decEq.
   simpl in H6. unfold Val.cmplu in H6.
-  destruct (Val.cmplu_bool c v1 v2) as [[]|]; inv H6; reflexivity.
+  destruct (Val.cmplu_bool (Mem.valid_pointer m) c v1 v2) as [[]|]; inv H6; reflexivity.
+Qed.
+
+Lemma make_cmpu_ne_zero_correct_ptr:
+  forall e le m a b i,
+  eval_expr ge e le m a (Vptr b i) ->
+  Archi.ptr64 = false ->
+  Mem.weak_valid_pointer m b (Ptrofs.unsigned i) = true ->
+  eval_expr ge e le m (make_cmpu_ne_zero a) Vone.
+Proof.
+  intros. 
+  assert (DEFAULT: eval_expr ge e le m (Ebinop (Ocmpu Cne) a (make_intconst Int.zero)) Vone).
+  { econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool.
+    unfold Mem.weak_valid_pointer in H1. rewrite H0, H1.
+    rewrite Int.eq_true; auto. }
+  assert (OF_OPTBOOL: forall ob, Some (Val.of_optbool ob) <> Some (Vptr b i)).
+  { intros. destruct ob as [[]|]; discriminate. }
+  assert (OF_BOOL: forall ob, option_map Val.of_bool ob <> Some (Vptr b i)).
+  { intros. destruct ob as [[]|]; discriminate. }
+  destruct a; simpl; auto. destruct b0; auto.
+- inv H; eelim OF_OPTBOOL; eauto.
+- inv H; eelim OF_OPTBOOL; eauto.
+- inv H; eelim OF_OPTBOOL; eauto.
+- inv H; eelim OF_OPTBOOL; eauto.
+- inv H; eelim OF_BOOL; eauto. 
+- inv H; eelim OF_BOOL; eauto. 
 Qed.
 
 Lemma make_cast_int_correct:
@@ -320,10 +357,27 @@ Proof.
   destruct si; eauto with cshm.
   destruct si; eauto with cshm.
   auto.
-  apply make_cmp_ne_zero_correct; auto.
+  apply make_cmpu_ne_zero_correct; auto.
 Qed.
 
-Hint Resolve make_cast_int_correct: cshm.
+Lemma make_longofint_correct:
+  forall e le m a n si,
+  eval_expr ge e le m a (Vint n) ->
+  eval_expr ge e le m (make_longofint a si) (Vlong (cast_int_long si n)).
+Proof.
+  intros. unfold make_longofint, cast_int_long. destruct si; eauto with cshm. 
+Qed.
+
+Hint Resolve make_cast_int_correct make_longofint_correct: cshm.
+
+Ltac InvEval :=
+  match goal with
+  | [ H: None = Some _ |- _ ] => discriminate
+  | [ H: Some _ = Some _ |- _ ] => inv H; InvEval
+  | [ H: match ?x with Some _ => _ | None => _ end = Some _ |- _ ] => destruct x eqn:?; InvEval
+  | [ H: match ?x with true => _ | false => _ end = Some _ |- _ ] => destruct x eqn:?; InvEval
+  | _ => idtac
+  end.
 
 Lemma make_cast_correct:
   forall e le m a b v ty1 ty2 v',
@@ -333,59 +387,51 @@ Lemma make_cast_correct:
   eval_expr ge e le m b v'.
 Proof.
   intros. unfold make_cast, sem_cast in *;
-  destruct (classify_cast ty1 ty2); inv H; destruct v; inv H1; eauto with cshm.
-  (* single -> int *)
+  destruct (classify_cast ty1 ty2); inv H; destruct v; InvEval; eauto with cshm.
+- (* single -> int *)
   unfold make_singleofint, cast_int_float. destruct si1; eauto with cshm.
-  (* float -> int *)
-  destruct (cast_float_int si2 f) as [i|] eqn:E; inv H2.
+- (* float -> int *)
   apply make_cast_int_correct.
-  unfold cast_float_int in E. unfold make_intoffloat.
-  destruct si2; econstructor; eauto; simpl; rewrite E; auto.
-  (* single -> int *)
-  destruct (cast_single_int si2 f) as [i|] eqn:E; inv H2.
+  unfold cast_float_int in Heqo. unfold make_intoffloat.
+  destruct si2; econstructor; eauto; simpl; rewrite Heqo; auto.
+- (* single -> int *)
   apply make_cast_int_correct.
-  unfold cast_single_int in E. unfold make_intofsingle.
-  destruct si2; econstructor; eauto with cshm; simpl; rewrite E; auto.
-  (* long -> int *)
-  unfold make_longofint, cast_int_long. destruct si1; eauto with cshm.
-  (* long -> float *)
+  unfold cast_single_int in Heqo. unfold make_intofsingle.
+  destruct si2; econstructor; eauto with cshm; simpl; rewrite Heqo; auto.
+- (* long -> float *)
   unfold make_floatoflong, cast_long_float. destruct si1; eauto with cshm.
-  (* long -> single *)
+- (* long -> single *)
   unfold make_singleoflong, cast_long_single. destruct si1; eauto with cshm.
-  (* float -> long *)
-  destruct (cast_float_long si2 f) as [i|] eqn:E; inv H2.
-  unfold cast_float_long in E. unfold make_longoffloat.
-  destruct si2; econstructor; eauto; simpl; rewrite E; auto.
-  (* single -> long *)
-  destruct (cast_single_long si2 f) as [i|] eqn:E; inv H2.
-  unfold cast_single_long in E. unfold make_longofsingle.
-  destruct si2; econstructor; eauto with cshm; simpl; rewrite E; auto.
-  (* float -> bool *)
+- (* float -> long *)
+  unfold cast_float_long in Heqo. unfold make_longoffloat.
+  destruct si2; econstructor; eauto; simpl; rewrite Heqo; auto.
+- (* single -> long *)
+  unfold cast_single_long in Heqo. unfold make_longofsingle.
+  destruct si2; econstructor; eauto with cshm; simpl; rewrite Heqo; auto.
+- (* int -> bool *)
+  apply make_cmpu_ne_zero_correct; auto.
+- (* pointer (32 bits) -> bool *)
+  eapply make_cmpu_ne_zero_correct_ptr; eauto.
+- (* long -> bool *)
+  econstructor; eauto with cshm.
+  simpl. unfold Val.cmplu, Val.cmplu_bool, Int64.cmpu.
+  destruct (Int64.eq i Int64.zero); auto.
+- (* pointer (64 bits) -> bool *)
+  econstructor; eauto with cshm.
+  simpl. unfold Val.cmplu, Val.cmplu_bool. unfold Mem.weak_valid_pointer in Heqb1.
+  rewrite Heqb0, Heqb1. rewrite Int64.eq_true. reflexivity.
+- (* float -> bool *)
   econstructor; eauto with cshm.
   simpl. unfold Val.cmpf, Val.cmpf_bool. rewrite Float.cmp_ne_eq.
   destruct (Float.cmp Ceq f Float.zero); auto.
-  (* single -> bool *)
+- (* single -> bool *)
   econstructor; eauto with cshm.
   simpl. unfold Val.cmpfs, Val.cmpfs_bool. rewrite Float32.cmp_ne_eq.
   destruct (Float32.cmp Ceq f Float32.zero); auto.
-  (* long -> bool *)
-  econstructor; eauto with cshm.
-  simpl. unfold Val.cmpl, Val.cmpl_bool, Int64.cmp.
-  destruct (Int64.eq i Int64.zero); auto.
-  (* int -> bool *)
-  econstructor; eauto with cshm.
-  simpl. unfold Val.cmpu, Val.cmpu_bool, Int.cmpu.
-  destruct (Int.eq i Int.zero); auto.
-  (* pointer -> bool *)
-  destruct (Mem.weak_valid_pointer m b (Int.unsigned i)) eqn:VALID; inv H2.
-  econstructor; eauto with cshm.
-  simpl. unfold Val.cmpu. simpl. rewrite Int.eq_true.
-  unfold Mem.weak_valid_pointer in VALID; rewrite VALID. 
-  auto.
-  (* struct *)
-  destruct (ident_eq id1 id2); inv H2; auto.
-  (* union *)
-  destruct (ident_eq id1 id2); inv H2; auto.
+- (* struct *)
+  destruct (ident_eq id1 id2); inv H1; auto.
+- (* union *)
+  destruct (ident_eq id1 id2); inv H1; auto.
 Qed.
 
 Lemma make_boolean_correct:
@@ -397,29 +443,28 @@ Lemma make_boolean_correct:
     /\ Val.bool_of_val vb b.
 Proof.
   intros. unfold make_boolean. unfold bool_val in H0.
-  destruct (classify_bool ty); destruct v; inv H0.
-(* int *)
-  econstructor; split. apply make_cmp_ne_zero_correct with (n := i); auto.
+  destruct (classify_bool ty); destruct v; InvEval.
+- (* int *)
+  econstructor; split. apply make_cmpu_ne_zero_correct with (n := i); auto.
   destruct (Int.eq i Int.zero); simpl; constructor.
-(* float *)
+- (* ptr 32 bits *)
+  exists Vone; split. eapply make_cmpu_ne_zero_correct_ptr; eauto. constructor. 
+- (* long *)
+  econstructor; split. econstructor; eauto with cshm. simpl. unfold Val.cmplu. simpl. eauto.
+  destruct (Int64.eq i Int64.zero); simpl; constructor.
+- (* ptr 64 bits *)
+  exists Vone; split. 
+  econstructor; eauto with cshm. simpl. unfold Val.cmplu, Val.cmplu_bool. 
+  unfold Mem.weak_valid_pointer in Heqb0. rewrite Heqb0, Heqb1, Int64.eq_true. reflexivity.
+  constructor.
+- (* float *)
   econstructor; split. econstructor; eauto with cshm. simpl. eauto.
   unfold Val.cmpf, Val.cmpf_bool. simpl. rewrite <- Float.cmp_ne_eq.
   destruct (Float.cmp Cne f Float.zero); constructor.
-(* single *)
+- (* single *)
   econstructor; split. econstructor; eauto with cshm. simpl. eauto.
   unfold Val.cmpfs, Val.cmpfs_bool. simpl. rewrite <- Float32.cmp_ne_eq.
   destruct (Float32.cmp Cne f Float32.zero); constructor.
-(* pointer *)
-  econstructor; split. econstructor; eauto with cshm. simpl. eauto.
-  unfold Val.cmpu, Val.cmpu_bool. simpl.
-  destruct (Int.eq i Int.zero); simpl; constructor.
-  econstructor; split. econstructor; eauto with cshm. simpl. eauto.
-  destruct (Mem.weak_valid_pointer m b0 (Int.unsigned i)) eqn:V; inv H2.
-  unfold Val.cmpu, Val.cmpu_bool. simpl.
-  unfold Mem.weak_valid_pointer in V; rewrite V. constructor.
-(* long *)
-  econstructor; split. econstructor; eauto with cshm. simpl. unfold Val.cmpl. simpl. eauto.
-  destruct (Int64.eq i Int64.zero); simpl; constructor.
 Qed.
 
 Lemma make_neg_correct:
@@ -454,11 +499,24 @@ Lemma make_notbool_correct:
   eval_expr ge e le m a va ->
   eval_expr ge e le m c v.
 Proof.
-  unfold sem_notbool, make_notbool; intros until m; intros SEM MAKE EV1;
-  destruct (classify_bool tya); inv MAKE; destruct va; inv SEM; eauto with cshm.
-  destruct (Mem.weak_valid_pointer m b (Int.unsigned i)) eqn:V; inv H0.
-  econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool.
-  unfold Mem.weak_valid_pointer in V; rewrite V. auto.
+  unfold sem_notbool, bool_val, make_notbool; intros until m; intros SEM MAKE EV1.
+  destruct (classify_bool tya); inv MAKE; destruct va; simpl in SEM; InvEval.
+- econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool, Int.cmpu. 
+  destruct (Int.eq i Int.zero); auto.
+- destruct Archi.ptr64 eqn:SF; inv SEM.
+  destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)) eqn:V; simpl in H0; inv H0.
+  econstructor; eauto with cshm. simpl. unfold Val.cmpu, Val.cmpu_bool. 
+  unfold Mem.weak_valid_pointer in V. rewrite SF, V, Int.eq_true. auto.
+- econstructor; eauto with cshm. simpl. unfold Val.cmplu, Val.cmplu_bool, Int64.cmpu. 
+  destruct (Int64.eq i Int64.zero); auto.
+- destruct Archi.ptr64 eqn:SF; inv SEM.
+  destruct (Mem.weak_valid_pointer m b (Ptrofs.unsigned i)) eqn:V; simpl in H0; inv H0.
+  econstructor; eauto with cshm. simpl. unfold Val.cmplu, Val.cmplu_bool. 
+  unfold Mem.weak_valid_pointer in V. rewrite SF, V, Int64.eq_true. auto.
+- econstructor; eauto with cshm. simpl. unfold Val.cmpf, Val.cmpf_bool. 
+  destruct (Float.cmp Ceq f Float.zero); auto.
+- econstructor; eauto with cshm. simpl. unfold Val.cmpfs, Val.cmpfs_bool. 
+  destruct (Float32.cmp Ceq f Float32.zero); auto.
 Qed.
 
 Lemma make_notint_correct:
@@ -561,19 +619,66 @@ End MAKE_BIN.
 
 Hint Extern 2 (@eq (option val) _ _) => (simpl; reflexivity) : cshm.
 
+(*
+Lemma eqm_ptrofs_of_int:
+  forall si i,
+  Ptrofs.eqm (Ptrofs.unsigned (ptrofs_of_int si i))
+             (match si with Signed => Int.signed i | Unsigned => Int.unsigned i end).
+Proof.
+  intros. unfold ptrofs_of_int. destruct si; apply Ptrofs.eqm_sym; apply Ptrofs.eqm_unsigned_repr.
+Qed.
+
+Lemma ptrofs_mul_32:
+  forall si n i,
+  Archi.ptr64 = false ->
+  Ptrofs.of_int (Int.mul (Int.repr n) i) = Ptrofs.mul (Ptrofs.repr n) (ptrofs_of_int si i).
+Proof.
+  intros. apply Ptrofs.eqm_samerepr. 
+  eapply Ptrofs.eqm_trans; [ | apply Ptrofs.eqm_mult ].
+  apply -> Val.ptrofs_eqm_32; auto. apply Int.eqm_sym; apply Int.eqm_unsigned_repr.
+  apply Ptrofs.eqm_unsigned_repr_r. apply -> Val.ptrofs_eqm_32; auto. apply Int.eqm_sym; apply Int.eqm_unsigned_repr.
+  apply Ptrofs.eqm_sym. eapply Ptrofs.eqm_trans. apply eqm_ptrofs_of_int.
+  apply -> Val.ptrofs_eqm_32; auto. destruct si. apply Int.eqm_signed_unsigned. apply Int.eqm_refl.
+Qed.
+
+Lemma ptrofs_mul_32_64:
+  forall n i,
+  Archi.ptr64 = false ->
+  Ptrofs.of_int (Int.mul (Int.repr n) (Int64.loword i)) = Ptrofs.mul (Ptrofs.repr n) (Ptrofs.of_int64 i).
+Proof.
+  intros. apply Ptrofs.eqm_samerepr. 
+  eapply Ptrofs.eqm_trans; [ | apply Ptrofs.eqm_mult ].
+  apply -> Val.ptrofs_eqm_32; auto. apply Int.eqm_sym; apply Int.eqm_unsigned_repr.
+  apply Ptrofs.eqm_unsigned_repr_r. apply -> Val.ptrofs_eqm_32; auto. apply Int.eqm_sym; apply Int.eqm_unsigned_repr.
+  unfold Ptrofs.of_int64. apply Ptrofs.eqm_unsigned_repr_r. 
+  unfold Int64.loword. apply -> Val.ptrofs_eqm_32; auto. apply Int.eqm_sym; apply Int.eqm_unsigned_repr.
+Qed.
+*)
+
 Lemma make_add_correct: binary_constructor_correct (make_add cunit.(prog_comp_env)) (sem_add prog.(prog_comp_env)).
 Proof.
   red; unfold make_add, sem_add;
   intros until m; intros SEM MAKE EV1 EV2;
   destruct (classify_add tya tyb); try (monadInv MAKE).
-- rewrite (transl_sizeof _ _ _ _ LINK EQ).
-  destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
-- rewrite (transl_sizeof _ _ _ _ LINK EQ).
-  destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
-- rewrite (transl_sizeof _ _ _ _ LINK EQ).
-  destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
-- rewrite (transl_sizeof _ _ _ _ LINK EQ).
-  destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
+- destruct Archi.ptr64 eqn:SF; inv EQ0; rewrite (transl_sizeof _ _ _ _ LINK EQ).
++ destruct va; InvEval; destruct vb; inv SEM; eauto with cshm.
+  econstructor; eauto with cshm.
+  simpl. rewrite SF. do 3 f_equal. 
+  assert (Ptrofs.agree64 (ptrofs_of_int si i0) (cast_int_long si i0)).
+  { destruct si; simpl; apply Ptrofs.agree64_repr; auto. }
+  auto with ptrofs.
++ destruct va; InvEval; destruct vb; inv SEM; eauto with cshm.
+  econstructor; eauto with cshm. simpl. rewrite SF. do 3 f_equal.
+  assert (Ptrofs.agree32 (ptrofs_of_int si i0) i0) by (destruct si; simpl; auto with ptrofs).
+  auto with ptrofs.
+- destruct Archi.ptr64 eqn:SF; inv EQ0; rewrite (transl_sizeof _ _ _ _ LINK EQ).
++ destruct va; InvEval; destruct vb; inv SEM; eauto with cshm.
+  econstructor; eauto with cshm.
+  simpl. rewrite SF. do 3 f_equal. auto with ptrofs.
++ destruct va; InvEval; destruct vb; inv SEM; eauto with cshm.
+  econstructor; eauto with cshm. simpl. rewrite SF. do 3 f_equal.
+  assert (Ptrofs.agree32 (Ptrofs.of_int64 i0) (Int64.loword i0)) by (apply Ptrofs.agree32_repr; auto).
+  auto with ptrofs.
 - eapply make_binarith_correct; eauto; intros; auto.
 Qed.
 
@@ -582,25 +687,61 @@ Proof.
   red; unfold make_sub, sem_sub;
   intros until m; intros SEM MAKE EV1 EV2;
   destruct (classify_sub tya tyb); try (monadInv MAKE).
-- rewrite (transl_sizeof _ _ _ _ LINK EQ).
-  destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
-- rewrite (transl_sizeof _ _ _ _ LINK EQ).
-  destruct va; try discriminate; destruct vb; inv SEM.
-  destruct (eq_block b0 b1); try discriminate.
+- destruct Archi.ptr64 eqn:SF; inv EQ0; rewrite (transl_sizeof _ _ _ _ LINK EQ).
++ destruct va; InvEval; destruct vb; inv SEM; eauto with cshm.
+  econstructor; eauto with cshm.
+  simpl. rewrite SF. do 3 f_equal. 
+  assert (Ptrofs.agree64 (ptrofs_of_int si i0) (cast_int_long si i0)).
+  { destruct si; simpl; apply Ptrofs.agree64_repr; auto. }
+  auto with ptrofs.
++ destruct va; InvEval; destruct vb; inv SEM; eauto with cshm.
+  econstructor; eauto with cshm. simpl. rewrite SF. do 3 f_equal.
+  assert (Ptrofs.agree32 (ptrofs_of_int si i0) i0) by (destruct si; simpl; auto with ptrofs).
+  auto with ptrofs.
+- rewrite (transl_sizeof _ _ _ _ LINK EQ) in EQ0. clear EQ. 
   set (sz := Ctypes.sizeof (prog_comp_env prog) ty) in *.
+  destruct va; InvEval; destruct vb; InvEval. 
+  destruct (eq_block b0 b1); try discriminate.
   destruct (zlt 0 sz); try discriminate.
-  destruct (zle sz Int.max_signed); simpl in H0; inv H0.
+  destruct (zle sz Ptrofs.max_signed); simpl in SEM; inv SEM.
+  assert (E1: Ptrofs.signed (Ptrofs.repr sz) = sz).
+  { apply Ptrofs.signed_repr. generalize Ptrofs.min_signed_neg; omega. }
+  destruct Archi.ptr64 eqn:SF; inversion EQ0; clear EQ0; subst c.
++ assert (E: Int64.signed (Int64.repr sz) = sz).
+  { apply Int64.signed_repr.
+    replace Int64.max_signed with Ptrofs.max_signed. 
+    generalize Int64.min_signed_neg; omega.
+    unfold Ptrofs.max_signed, Ptrofs.half_modulus; rewrite Ptrofs.modulus_eq64 by auto. reflexivity. }
   econstructor; eauto with cshm.
-  rewrite dec_eq_true; simpl.
-  assert (E: Int.signed (Int.repr sz) = sz).
-  { apply Int.signed_repr. generalize Int.min_signed_neg; omega. }
+  rewrite SF, dec_eq_true. simpl. 
+  predSpec Int64.eq Int64.eq_spec (Int64.repr sz) Int64.zero.
+  rewrite H in E; rewrite Int64.signed_zero in E; omegaContradiction.
+  predSpec Int64.eq Int64.eq_spec (Int64.repr sz) Int64.mone.
+  rewrite H0 in E; rewrite Int64.signed_mone in E; omegaContradiction.
+  rewrite andb_false_r; simpl. unfold Vptrofs; rewrite SF. do 2 f_equal.
+  symmetry. auto with ptrofs.
++ assert (E: Int.signed (Int.repr sz) = sz).
+  { apply Int.signed_repr.
+    replace Int.max_signed with Ptrofs.max_signed. 
+    generalize Int.min_signed_neg; omega.
+    unfold Ptrofs.max_signed, Ptrofs.half_modulus, Ptrofs.modulus, Ptrofs.wordsize, Wordsize_Ptrofs.wordsize. rewrite SF. reflexivity. 
+  }
+  econstructor; eauto with cshm. rewrite SF, dec_eq_true. simpl. 
   predSpec Int.eq Int.eq_spec (Int.repr sz) Int.zero.
   rewrite H in E; rewrite Int.signed_zero in E; omegaContradiction.
   predSpec Int.eq Int.eq_spec (Int.repr sz) Int.mone.
   rewrite H0 in E; rewrite Int.signed_mone in E; omegaContradiction.
-  rewrite andb_false_r; auto.
-- rewrite (transl_sizeof _ _ _ _ LINK EQ).
-  destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
+  rewrite andb_false_r; simpl. unfold Vptrofs; rewrite SF. do 2 f_equal.
+  symmetry. auto with ptrofs.
+- destruct Archi.ptr64 eqn:SF; inv EQ0; rewrite (transl_sizeof _ _ _ _ LINK EQ).
++ destruct va; InvEval; destruct vb; inv SEM; eauto with cshm.
+  econstructor; eauto with cshm.
+  simpl. rewrite SF. do 3 f_equal. 
+  auto with ptrofs.
++ destruct va; InvEval; destruct vb; inv SEM; eauto with cshm.
+  econstructor; eauto with cshm. simpl. rewrite SF. do 3 f_equal.
+  assert (Ptrofs.agree32 (Ptrofs.of_int64 i0) (Int64.loword i0)) by (apply Ptrofs.agree32_repr; auto).
+  auto with ptrofs.
 - eapply make_binarith_correct; eauto; intros; auto.
 Qed.
 
@@ -716,25 +857,61 @@ Proof.
   unfold Int64.shru', Int64.shru; rewrite small_shift_amount_3; auto.
 Qed.
 
+Lemma make_cmp_ptr_correct:
+  forall cmp e le m a va b vb v,
+  cmp_ptr m cmp va vb = Some v ->
+  eval_expr ge e le m a va ->
+  eval_expr ge e le m b vb ->
+  eval_expr ge e le m (make_cmp_ptr cmp a b) v.
+Proof.
+  unfold cmp_ptr, make_cmp_ptr; intros.
+  destruct Archi.ptr64.
+- econstructor; eauto.
+- econstructor; eauto. simpl. unfold Val.cmpu. 
+  destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp va vb) as [bo|]; inv H. auto.
+Qed.
+
+Remark make_ptrofs_of_int_correct:
+  forall e le m a i si,
+  eval_expr ge e le m a (Vint i) ->
+  eval_expr ge e le m (if Archi.ptr64 then make_longofint a si else a) (Vptrofs (ptrofs_of_int si i)).
+Proof.
+  intros. unfold Vptrofs, ptrofs_of_int. destruct Archi.ptr64 eqn:SF.
+- unfold make_longofint. destruct si.
++ replace (Ptrofs.to_int64 (Ptrofs.of_ints i)) with (Int64.repr (Int.signed i)).
+  eauto with cshm.
+  apply Int64.eqm_samerepr. rewrite Ptrofs.eqm64 by auto. apply Ptrofs.eqm_unsigned_repr. 
++ replace (Ptrofs.to_int64 (Ptrofs.of_intu i)) with (Int64.repr (Int.unsigned i)).
+  eauto with cshm.
+  apply Int64.eqm_samerepr. rewrite Ptrofs.eqm64 by auto. apply Ptrofs.eqm_unsigned_repr. 
+- destruct si.
++ replace (Ptrofs.to_int (Ptrofs.of_ints i)) with i. auto.
+  symmetry. auto with ptrofs. 
++ replace (Ptrofs.to_int (Ptrofs.of_intu i)) with i. auto.
+  symmetry. auto with ptrofs. 
+Qed.
+
+Remark make_ptrofs_of_int64_correct:
+  forall e le m a i,
+  eval_expr ge e le m a (Vlong i) ->
+  eval_expr ge e le m (if Archi.ptr64 then a else Eunop Ointoflong a) (Vptrofs (Ptrofs.of_int64 i)).
+Proof.
+  intros. unfold Vptrofs. destruct Archi.ptr64 eqn:SF.
+- replace (Ptrofs.to_int64 (Ptrofs.of_int64 i)) with i. auto.
+  symmetry. auto with ptrofs.
+- econstructor; eauto. simpl. do 2 f_equal.
+  apply Int.eqm_samerepr. rewrite Ptrofs.eqm32 by auto. apply Ptrofs.eqm_unsigned_repr.
+Qed.
+
 Lemma make_cmp_correct: forall cmp, binary_constructor_correct (make_cmp cmp) (sem_cmp cmp).
 Proof.
   red; unfold sem_cmp, make_cmp; intros until m; intros SEM MAKE EV1 EV2;
   destruct (classify_cmp tya tyb).
-- inv MAKE. destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp va vb) as [bv|] eqn:E;
-  simpl in SEM; inv SEM.
-  econstructor; eauto. simpl. unfold Val.cmpu. rewrite E. auto.
-- inv MAKE. destruct vb; try discriminate.
-  set (vb := Vint (Int.repr (Int64.unsigned i))) in *.
-  destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp va vb) as [bv|] eqn:E;
-  simpl in SEM; inv SEM.
-  econstructor; eauto with cshm. simpl. change (Vint (Int64.loword i)) with vb.
-  unfold Val.cmpu. rewrite E. auto.
-- inv MAKE. destruct va; try discriminate.
-  set (va := Vint (Int.repr (Int64.unsigned i))) in *.
-  destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp va vb) as [bv|] eqn:E;
-  simpl in SEM; inv SEM.
-  econstructor; eauto with cshm. simpl. change (Vint (Int64.loword i)) with va.
-  unfold Val.cmpu. rewrite E. auto.
+- inv MAKE. eapply make_cmp_ptr_correct; eauto.
+- inv MAKE. destruct vb; InvEval; eauto using make_cmp_ptr_correct, make_ptrofs_of_int_correct.
+- inv MAKE. destruct va; InvEval; eauto using make_cmp_ptr_correct, make_ptrofs_of_int_correct.
+- inv MAKE. destruct vb; InvEval; eauto using make_cmp_ptr_correct, make_ptrofs_of_int64_correct.
+- inv MAKE. destruct va; InvEval; eauto using make_cmp_ptr_correct, make_ptrofs_of_int64_correct.
 - eapply make_binarith_correct; eauto; intros; auto.
 Qed.
 
@@ -1042,49 +1219,53 @@ Lemma transl_expr_lvalue_correct:
    Csharpminor.eval_expr tge te le m ta (Vptr b ofs)).
 Proof.
   apply eval_expr_lvalue_ind; intros; try (monadInv TR).
-(* const int *)
+- (* const int *)
   apply make_intconst_correct.
-(* const float *)
+- (* const float *)
   apply make_floatconst_correct.
-(* const single *)
+- (* const single *)
   apply make_singleconst_correct.
-(* const long *)
+- (* const long *)
   apply make_longconst_correct.
-(* temp var *)
+- (* temp var *)
   constructor; auto.
-(* addrof *)
+- (* addrof *)
   simpl in TR. auto.
-(* unop *)
+- (* unop *)
   eapply transl_unop_correct; eauto.
-(* binop *)
+- (* binop *)
   eapply transl_binop_correct; eauto.
-(* cast *)
+- (* cast *)
   eapply make_cast_correct; eauto.
-(* sizeof *)
-  rewrite (transl_sizeof _ _ _ _ LINK EQ). apply make_intconst_correct.
-(* alignof *)
-  rewrite (transl_alignof _ _ _ _ LINK EQ). apply make_intconst_correct.
-(* rvalue out of lvalue *)
+- (* sizeof *)
+  rewrite (transl_sizeof _ _ _ _ LINK EQ). apply make_ptrofsconst_correct.
+- (* alignof *)
+  rewrite (transl_alignof _ _ _ _ LINK EQ). apply make_ptrofsconst_correct.
+- (* rvalue out of lvalue *)
   exploit transl_expr_lvalue; eauto. intros [tb [TRLVAL MKLOAD]].
   eapply make_load_correct; eauto.
-(* var local *)
+- (* var local *)
   exploit (me_local _ _ MENV); eauto. intros EQ.
   econstructor. eapply eval_var_addr_local. eauto.
-(* var global *)
+- (* var global *)
   econstructor. eapply eval_var_addr_global.
   eapply match_env_globals; eauto.
   rewrite symbols_preserved. auto.
-(* deref *)
+- (* deref *)
   simpl in TR. eauto.
-(* field struct *)
+- (* field struct *)
   unfold make_field_access in EQ0. rewrite H1 in EQ0. 
   destruct (prog_comp_env cunit)!id as [co'|] eqn:CO; monadInv EQ0.
   exploit field_offset_stable. eexact LINK. eauto. instantiate (1 := i). intros [A B].
-  rewrite <- B in EQ1. 
-  eapply eval_Ebinop; eauto.
-  apply make_intconst_correct.
-  simpl. unfold ge in *; simpl in *. congruence.
-(* field union *)
+  rewrite <- B in EQ1.
+  assert (x0 = delta) by (unfold ge in *; simpl in *; congruence).
+  subst x0.
+  destruct Archi.ptr64 eqn:SF.
++ eapply eval_Ebinop; eauto using make_longconst_correct.
+  simpl. rewrite SF. do 3 f_equal. auto with ptrofs. 
++ eapply eval_Ebinop; eauto using make_intconst_correct.
+  simpl. rewrite SF. do 3 f_equal. auto with ptrofs.
+- (* field union *)
   unfold make_field_access in EQ0; rewrite H1 in EQ0; monadInv EQ0.
   auto.
 Qed.