Support for 64-bit architectures: x86 in 64-bit mode

This commit enriches the IA32 port so that it supports x86 processors in 64-bit mode as well as in 32-bit mode, depending on the value of Archi.ptr64, which itself is set from the configuration model.

To activate x86-64 bit support, configure with "x86_64-linux".

Main steps:
- Enrich Op.v and Asm.v with 64-bit operations
- SelectLong: in 64-bit mode, use 64-bit operations directly; in 32-bit mode, fall back on the old implementation based on pairs of 32-bit integers
- Conventions1: support x86-64 ABI in addition to the 32-bit ABI.
- Add support for the new 64-bit operations everywhere.
- runtime/x86_64: implementation of the supporting library appropriate for x86 in 64-bit mode

To do:
- More optimizations are possible on 64-bit integer arithmetic operations.
- Could add new chunks to load, say, an unsigned byte into a 64-bit long
  (currently we load as a 32-bit int then zero-extend).
- Implements the wrong ABI for struct passing.

1 files changed, 631 insertions, 264 deletions

diff --git a/ia32/Op.v b/ia32/Op.v
index f21d7c6a..ed96c132 100644
--- a/ia32/Op.v
+++ b/ia32/Op.v
@@ -17,7 +17,7 @@
 - [operation]: arithmetic and logical operations;
 - [addressing]: addressing modes for load and store operations.
 
-  These types are IA32-specific and correspond roughly to what the
+  These types are X86-64-specific and correspond roughly to what the
   processor can compute in one instruction.  In other terms, these
   types reflect the state of the program after instruction selection.
   For a processor-independent set of operations, see the abstract
@@ -38,135 +38,179 @@ Set Implicit Arguments.
 (** Conditions (boolean-valued operators). *)
 
 Inductive condition : Type :=
-  | Ccomp: comparison -> condition      (**r signed integer comparison *)
-  | Ccompu: comparison -> condition     (**r unsigned integer comparison *)
-  | Ccompimm: comparison -> int -> condition (**r signed integer comparison with a constant *)
-  | Ccompuimm: comparison -> int -> condition  (**r unsigned integer comparison with a constant *)
-  | Ccompf: comparison -> condition     (**r 64-bit floating-point comparison *)
-  | Cnotcompf: comparison -> condition  (**r negation of a floating-point comparison *)
-  | Ccompfs: comparison -> condition    (**r 32-bit floating-point comparison *)
-  | Cnotcompfs: comparison -> condition (**r negation of a floating-point comparison *)
-  | Cmaskzero: int -> condition         (**r test [(arg & constant) == 0] *)
-  | Cmasknotzero: int -> condition.     (**r test [(arg & constant) != 0] *)
+  | Ccomp (c: comparison)      (**r signed integer comparison *)
+  | Ccompu (c: comparison)     (**r unsigned integer comparison *)
+  | Ccompimm (c: comparison) (n: int) (**r signed integer comparison with a constant *)
+  | Ccompuimm (c: comparison) (n: int)  (**r unsigned integer comparison with a constant *)
+  | Ccompl (c: comparison)      (**r signed 64-bit integer comparison *)
+  | Ccomplu (c: comparison)     (**r unsigned 64-bit integer comparison *)
+  | Ccomplimm (c: comparison) (n: int64) (**r signed 64-bit integer comparison with a constant *)
+  | Ccompluimm (c: comparison) (n: int64)  (**r unsigned 64-bit integer comparison with a constant *)
+  | Ccompf (c: comparison)     (**r 64-bit floating-point comparison *)
+  | Cnotcompf (c: comparison)  (**r negation of a floating-point comparison *)
+  | Ccompfs (c: comparison)    (**r 32-bit floating-point comparison *)
+  | Cnotcompfs (c: comparison) (**r negation of a floating-point comparison *)
+  | Cmaskzero (n: int)         (**r test [(arg & constant) == 0] *)
+  | Cmasknotzero (n: int).     (**r test [(arg & constant) != 0] *)
 
 (** Addressing modes.  [r1], [r2], etc, are the arguments to the
   addressing. *)
 
 Inductive addressing: Type :=
-  | Aindexed: int -> addressing         (**r Address is [r1 + offset] *)
-  | Aindexed2: int -> addressing        (**r Address is [r1 + r2 + offset] *)
-  | Ascaled: int -> int -> addressing   (**r Address is [r1 * scale + offset] *)
-  | Aindexed2scaled: int -> int -> addressing
-                                   (**r Address is [r1 + r2 * scale + offset] *)
-  | Aglobal: ident -> int -> addressing (**r Address is [symbol + offset] *)
-  | Abased: ident -> int -> addressing  (**r Address is [symbol + offset + r1] *)
-  | Abasedscaled: int -> ident -> int -> addressing  (**r Address is [symbol + offset + r1 * scale] *)
-  | Ainstack: int -> addressing.        (**r Address is [stack_pointer + offset] *)
+  | Aindexed: Z -> addressing       (**r Address is [r1 + offset] *)
+  | Aindexed2: Z -> addressing      (**r Address is [r1 + r2 + offset] *)
+  | Ascaled: Z -> Z -> addressing   (**r Address is [r1 * scale + offset] *)
+  | Aindexed2scaled: Z -> Z -> addressing
+                                    (**r Address is [r1 + r2 * scale + offset] *)
+  | Aglobal: ident -> ptrofs -> addressing (**r Address is [symbol + offset] *)
+  | Abased: ident -> ptrofs -> addressing  (**r Address is [symbol + offset + r1] *)
+  | Abasedscaled: Z -> ident -> ptrofs -> addressing  (**r Address is [symbol + offset + r1 * scale] *)
+  | Ainstack: ptrofs -> addressing. (**r Address is [stack_pointer + offset] *)
 
 (** Arithmetic and logical operations.  In the descriptions, [rd] is the
   result of the operation and [r1], [r2], etc, are the arguments. *)
 
 Inductive operation : Type :=
-  | Omove: operation                    (**r [rd = r1] *)
-  | Ointconst: int -> operation         (**r [rd] is set to the given integer constant *)
-  | Ofloatconst: float -> operation     (**r [rd] is set to the given float constant *)
-  | Osingleconst: float32 -> operation  (**r [rd] is set to the given float constant *)
-  | Oindirectsymbol: ident -> operation (**r [rd] is set to the address of the symbol *)
-(*c Integer arithmetic: *)
-  | Ocast8signed: operation             (**r [rd] is 8-bit sign extension of [r1] *)
-  | Ocast8unsigned: operation           (**r [rd] is 8-bit zero extension of [r1] *)
-  | Ocast16signed: operation            (**r [rd] is 16-bit sign extension of [r1] *)
-  | Ocast16unsigned: operation          (**r [rd] is 16-bit zero extension of [r1] *)
-  | Oneg: operation                     (**r [rd = - r1] *)
-  | Osub: operation                     (**r [rd = r1 - r2] *)
-  | Omul: operation                     (**r [rd = r1 * r2] *)
-  | Omulimm: int -> operation           (**r [rd = r1 * n] *)
-  | Omulhs: operation                   (**r [rd = high part of r1 * r2, signed] *)
-  | Omulhu: operation                   (**r [rd = high part of r1 * r2, unsigned] *)
-  | Odiv: operation                     (**r [rd = r1 / r2] (signed) *)
-  | Odivu: operation                    (**r [rd = r1 / r2] (unsigned) *)
-  | Omod: operation                     (**r [rd = r1 % r2] (signed) *)
-  | Omodu: operation                    (**r [rd = r1 % r2] (unsigned) *)
-  | Oand: operation                     (**r [rd = r1 & r2] *)
-  | Oandimm: int -> operation           (**r [rd = r1 & n] *)
-  | Oor: operation                      (**r [rd = r1 | r2] *)
-  | Oorimm: int -> operation            (**r [rd = r1 | n] *)
-  | Oxor: operation                     (**r [rd = r1 ^ r2] *)
-  | Oxorimm: int -> operation           (**r [rd = r1 ^ n] *)
-  | Onot: operation                     (**r [rd = ~r1] *)
-  | Oshl: operation                     (**r [rd = r1 << r2] *)
-  | Oshlimm: int -> operation           (**r [rd = r1 << n] *)
-  | Oshr: operation                     (**r [rd = r1 >> r2] (signed) *)
-  | Oshrimm: int -> operation           (**r [rd = r1 >> n] (signed) *)
-  | Oshrximm: int -> operation          (**r [rd = r1 / 2^n] (signed) *)
-  | Oshru: operation                    (**r [rd = r1 >> r2] (unsigned) *)
-  | Oshruimm: int -> operation          (**r [rd = r1 >> n] (unsigned) *)
-  | Ororimm: int -> operation           (**r rotate right immediate *)
-  | Oshldimm: int -> operation          (**r [rd = r1 << n | r2 >> (32-n)] *)
-  | Olea: addressing -> operation       (**r effective address *)
+  | Omove                    (**r [rd = r1] *)
+  | Ointconst (n: int)       (**r [rd] is set to the given integer constant *)
+  | Olongconst (n: int64)    (**r [rd] is set to the given integer constant *)
+  | Ofloatconst (n: float)   (**r [rd] is set to the given float constant *)
+  | Osingleconst (n: float32)(**r [rd] is set to the given float constant *)
+  | Oindirectsymbol (id: ident) (**r [rd] is set to the address of the symbol *)
+(*c 32-bit integer arithmetic: *)
+  | Ocast8signed             (**r [rd] is 8-bit sign extension of [r1] *)
+  | Ocast8unsigned           (**r [rd] is 8-bit zero extension of [r1] *)
+  | Ocast16signed            (**r [rd] is 16-bit sign extension of [r1] *)
+  | Ocast16unsigned          (**r [rd] is 16-bit zero extension of [r1] *)
+  | Oneg                     (**r [rd = - r1] *)
+  | Osub                     (**r [rd = r1 - r2] *)
+  | Omul                     (**r [rd = r1 * r2] *)
+  | Omulimm (n: int)         (**r [rd = r1 * n] *)
+  | Omulhs                   (**r [rd = high part of r1 * r2, signed] *)
+  | Omulhu                   (**r [rd = high part of r1 * r2, unsigned] *)
+  | Odiv                     (**r [rd = r1 / r2] (signed) *)
+  | Odivu                    (**r [rd = r1 / r2] (unsigned) *)
+  | Omod                     (**r [rd = r1 % r2] (signed) *)
+  | Omodu                    (**r [rd = r1 % r2] (unsigned) *)
+  | Oand                     (**r [rd = r1 & r2] *)
+  | Oandimm (n: int)         (**r [rd = r1 & n] *)
+  | Oor                      (**r [rd = r1 | r2] *)
+  | Oorimm (n: int)          (**r [rd = r1 | n] *)
+  | Oxor                     (**r [rd = r1 ^ r2] *)
+  | Oxorimm (n: int)         (**r [rd = r1 ^ n] *)
+  | Onot                     (**r [rd = ~r1] *)
+  | Oshl                     (**r [rd = r1 << r2] *)
+  | Oshlimm (n: int)         (**r [rd = r1 << n] *)
+  | Oshr                     (**r [rd = r1 >> r2] (signed) *)
+  | Oshrimm (n: int)         (**r [rd = r1 >> n] (signed) *)
+  | Oshrximm (n: int)        (**r [rd = r1 / 2^n] (signed) *)
+  | Oshru                    (**r [rd = r1 >> r2] (unsigned) *)
+  | Oshruimm (n: int)        (**r [rd = r1 >> n] (unsigned) *)
+  | Ororimm (n: int)         (**r rotate right immediate *)
+  | Oshldimm (n: int)        (**r [rd = r1 << n | r2 >> (32-n)] *)
+  | Olea (a: addressing)     (**r effective address *)
+(*c 64-bit integer arithmetic: *)
+  | Omakelong                (**r [rd = r1 << 32 | r2] *)
+  | Olowlong                 (**r [rd = low-word(r1)] *)
+  | Ohighlong                (**r [rd = high-word(r1)] *)
+  | Ocast32signed            (**r [rd] is 32-bit sign extension of [r1] *)
+  | Ocast32unsigned          (**r [rd] is 32-bit zero extension of [r1] *)
+  | Onegl                    (**r [rd = - r1] *)
+  | Oaddlimm (n: int64)      (**r [rd = r1 + n] *)
+  | Osubl                    (**r [rd = r1 - r2] *)
+  | Omull                    (**r [rd = r1 * r2] *)
+  | Omullimm (n: int64)      (**r [rd = r1 * n] *)
+  | Odivl                    (**r [rd = r1 / r2] (signed) *)
+  | Odivlu                   (**r [rd = r1 / r2] (unsigned) *)
+  | Omodl                    (**r [rd = r1 % r2] (signed) *)
+  | Omodlu                   (**r [rd = r1 % r2] (unsigned) *)
+  | Oandl                    (**r [rd = r1 & r2] *)
+  | Oandlimm (n: int64)      (**r [rd = r1 & n] *)
+  | Oorl                     (**r [rd = r1 | r2] *)
+  | Oorlimm (n: int64)       (**r [rd = r1 | n] *)
+  | Oxorl                    (**r [rd = r1 ^ r2] *)
+  | Oxorlimm (n: int64)      (**r [rd = r1 ^ n] *)
+  | Onotl                    (**r [rd = ~r1] *)
+  | Oshll                    (**r [rd = r1 << r2] *)
+  | Oshllimm (n: int)        (**r [rd = r1 << n] *)
+  | Oshrl                    (**r [rd = r1 >> r2] (signed) *)
+  | Oshrlimm (n: int)        (**r [rd = r1 >> n] (signed) *)
+  | Oshrlu                   (**r [rd = r1 >> r2] (unsigned) *)
+  | Oshrluimm (n: int)       (**r [rd = r1 >> n] (unsigned) *)
+  | Ororlimm (n: int)        (**r rotate right immediate *)
+  | Oleal (a: addressing)    (**r effective address *)
 (*c Floating-point arithmetic: *)
-  | Onegf: operation                    (**r [rd = - r1] *)
-  | Oabsf: operation                    (**r [rd = abs(r1)] *)
-  | Oaddf: operation                    (**r [rd = r1 + r2] *)
-  | Osubf: operation                    (**r [rd = r1 - r2] *)
-  | Omulf: operation                    (**r [rd = r1 * r2] *)
-  | Odivf: operation                    (**r [rd = r1 / r2] *)
-  | Onegfs: operation                   (**r [rd = - r1] *)
-  | Oabsfs: operation                   (**r [rd = abs(r1)] *)
-  | Oaddfs: operation                   (**r [rd = r1 + r2] *)
-  | Osubfs: operation                   (**r [rd = r1 - r2] *)
-  | Omulfs: operation                   (**r [rd = r1 * r2] *)
-  | Odivfs: operation                   (**r [rd = r1 / r2] *)
-  | Osingleoffloat: operation           (**r [rd] is [r1] truncated to single-precision float *)
-  | Ofloatofsingle: operation           (**r [rd] is [r1] extended to double-precision float *)
+  | Onegf                    (**r [rd = - r1] *)
+  | Oabsf                    (**r [rd = abs(r1)] *)
+  | Oaddf                    (**r [rd = r1 + r2] *)
+  | Osubf                    (**r [rd = r1 - r2] *)
+  | Omulf                    (**r [rd = r1 * r2] *)
+  | Odivf                    (**r [rd = r1 / r2] *)
+  | Onegfs                   (**r [rd = - r1] *)
+  | Oabsfs                   (**r [rd = abs(r1)] *)
+  | Oaddfs                   (**r [rd = r1 + r2] *)
+  | Osubfs                   (**r [rd = r1 - r2] *)
+  | Omulfs                   (**r [rd = r1 * r2] *)
+  | Odivfs                   (**r [rd = r1 / r2] *)
+  | Osingleoffloat           (**r [rd] is [r1] truncated to single-precision float *)
+  | Ofloatofsingle           (**r [rd] is [r1] extended to double-precision float *)
 (*c Conversions between int and float: *)
-  | Ointoffloat: operation              (**r [rd = signed_int_of_float64(r1)] *)
-  | Ofloatofint: operation              (**r [rd = float64_of_signed_int(r1)] *)
-  | Ointofsingle: operation             (**r [rd = signed_int_of_float32(r1)] *)
-  | Osingleofint: operation             (**r [rd = float32_of_signed_int(r1)] *)
-(*c Manipulating 64-bit integers: *)
-  | Omakelong: operation                (**r [rd = r1 << 32 | r2] *)
-  | Olowlong: operation                 (**r [rd = low-word(r1)] *)
-  | Ohighlong: operation                (**r [rd = high-word(r1)] *)
+  | Ointoffloat              (**r [rd = signed_int_of_float64(r1)] *)
+  | Ofloatofint              (**r [rd = float64_of_signed_int(r1)] *)
+  | Ointofsingle             (**r [rd = signed_int_of_float32(r1)] *)
+  | Osingleofint             (**r [rd = float32_of_signed_int(r1)] *)
+  | Olongoffloat             (**r [rd = signed_long_of_float64(r1)] *)
+  | Ofloatoflong             (**r [rd = float64_of_signed_long(r1)] *)
+  | Olongofsingle            (**r [rd = signed_long_of_float32(r1)] *)
+  | Osingleoflong            (**r [rd = float32_of_signed_long(r1)] *)
 (*c Boolean tests: *)
-  | Ocmp: condition -> operation.       (**r [rd = 1] if condition holds, [rd = 0] otherwise. *)
-
-(** Derived operators. *)
-
-Definition Oaddrsymbol (id: ident) (ofs: int) : operation := Olea (Aglobal id ofs).
-Definition Oaddrstack (ofs: int) : operation := Olea (Ainstack ofs).
-Definition Oaddimm (n: int) : operation := Olea (Aindexed n).
+  | Ocmp (cond: condition).  (**r [rd = 1] if condition holds, [rd = 0] otherwise. *)
 
 (** Comparison functions (used in modules [CSE] and [Allocation]). *)
 
 Definition eq_condition (x y: condition) : {x=y} + {x<>y}.
 Proof.
-  generalize Int.eq_dec; intro.
+  generalize Int.eq_dec Int64.eq_dec; intro.
   assert (forall (x y: comparison), {x=y}+{x<>y}). decide equality.
   decide equality.
 Defined.
 
 Definition eq_addressing (x y: addressing) : {x=y} + {x<>y}.
 Proof.
-  generalize Int.eq_dec; intro.
-  assert (forall (x y: ident), {x=y}+{x<>y}). exact peq.
+  generalize ident_eq Ptrofs.eq_dec zeq; intros.
   decide equality.
 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.
-  generalize Int64.eq_dec; intro.
+  generalize Int.eq_dec Int64.eq_dec Float.eq_dec Float32.eq_dec; intros.
   decide equality.
-  apply peq.
+  apply ident_eq.
+  apply eq_addressing.
   apply eq_addressing.
   apply eq_condition.
 Defined.
 
 Global Opaque eq_condition eq_addressing eq_operation.
 
+(** In addressing modes, offsets are 32-bit signed integers, even in 64-bit mode.
+    The following function checks that an addressing mode is valid, i.e. that
+    the offsets are in range. *)
+
+Definition offset_in_range (n: Z) : bool := zle Int.min_signed n && zle n Int.max_signed.
+
+Definition addressing_valid (a: addressing) : bool :=
+  match a with
+  | Aindexed n => offset_in_range n
+  | Aindexed2 n => offset_in_range n
+  | Ascaled sc ofs => offset_in_range ofs
+  | Aindexed2scaled sc ofs => offset_in_range ofs
+  | Aglobal s ofs => true
+  | Abased s ofs => true
+  | Abasedscaled sc s ofs => true
+  | Ainstack ofs => offset_in_range (Ptrofs.signed ofs)
+  end.
+
 (** * Evaluation functions *)
 
 (** Evaluation of conditions, operators and addressing modes applied
@@ -180,6 +224,10 @@ Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool
   | Ccompu c, v1 :: v2 :: nil => Val.cmpu_bool (Mem.valid_pointer m) c v1 v2
   | Ccompimm c n, v1 :: nil => Val.cmp_bool c v1 (Vint n)
   | Ccompuimm c n, v1 :: nil => Val.cmpu_bool (Mem.valid_pointer m) c v1 (Vint n)
+  | Ccompl c, v1 :: v2 :: nil => Val.cmpl_bool c v1 v2
+  | Ccomplu c, v1 :: v2 :: nil => Val.cmplu_bool (Mem.valid_pointer m) c v1 v2
+  | Ccomplimm c n, v1 :: nil => Val.cmpl_bool c v1 (Vlong n)
+  | Ccompluimm c n, v1 :: nil => Val.cmplu_bool (Mem.valid_pointer m) c v1 (Vlong n)
   | Ccompf c, v1 :: v2 :: nil => Val.cmpf_bool c v1 v2
   | Cnotcompf c, v1 :: v2 :: nil => option_map negb (Val.cmpf_bool c v1 v2)
   | Ccompfs c, v1 :: v2 :: nil => Val.cmpfs_bool c v1 v2
@@ -189,38 +237,65 @@ Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool
   | _, _ => None
   end.
 
-Definition eval_addressing
+Definition eval_addressing32
     (F V: Type) (genv: Genv.t F V) (sp: val)
     (addr: addressing) (vl: list val) : option val :=
   match addr, vl with
   | Aindexed n, v1::nil =>
-      Some (Val.add v1 (Vint n))
+      Some (Val.add v1 (Vint (Int.repr n)))
   | Aindexed2 n, v1::v2::nil =>
-      Some (Val.add (Val.add v1 v2) (Vint n))
+      Some (Val.add (Val.add v1 v2) (Vint (Int.repr n)))
   | Ascaled sc ofs, v1::nil =>
-      Some (Val.add (Val.mul v1 (Vint sc)) (Vint ofs))
+      Some (Val.add (Val.mul v1 (Vint (Int.repr sc))) (Vint (Int.repr ofs)))
   | Aindexed2scaled sc ofs, v1::v2::nil =>
-      Some(Val.add v1 (Val.add (Val.mul v2 (Vint sc)) (Vint ofs)))
+      Some(Val.add v1 (Val.add (Val.mul v2 (Vint (Int.repr sc))) (Vint (Int.repr ofs))))
   | Aglobal s ofs, nil =>
-      Some (Genv.symbol_address genv s ofs)
+      if Archi.ptr64 then None else Some (Genv.symbol_address genv s ofs)
   | Abased s ofs, v1::nil =>
-      Some (Val.add (Genv.symbol_address genv s ofs) v1)
+      if Archi.ptr64 then None else Some (Val.add (Genv.symbol_address genv s ofs) v1)
   | Abasedscaled sc s ofs, v1::nil =>
-      Some (Val.add (Genv.symbol_address genv s ofs) (Val.mul v1 (Vint sc)))
+      if Archi.ptr64 then None else Some (Val.add (Genv.symbol_address genv s ofs) (Val.mul v1 (Vint (Int.repr sc))))
   | Ainstack ofs, nil =>
-      Some(Val.add sp (Vint ofs))
+      if Archi.ptr64 then None else Some(Val.offset_ptr sp ofs)
   | _, _ => None
   end.
 
+Definition eval_addressing64
+    (F V: Type) (genv: Genv.t F V) (sp: val)
+    (addr: addressing) (vl: list val) : option val :=
+  match addr, vl with
+  | Aindexed n, v1::nil =>
+      Some (Val.addl v1 (Vlong (Int64.repr n)))
+  | Aindexed2 n, v1::v2::nil =>
+      Some (Val.addl (Val.addl v1 v2) (Vlong (Int64.repr n)))
+  | Ascaled sc ofs, v1::nil =>
+      Some (Val.addl (Val.mull v1 (Vlong (Int64.repr sc))) (Vlong (Int64.repr ofs)))
+  | Aindexed2scaled sc ofs, v1::v2::nil =>
+      Some(Val.addl v1 (Val.addl (Val.mull v2 (Vlong (Int64.repr sc))) (Vlong (Int64.repr ofs))))
+  | Aglobal s ofs, nil =>
+      if Archi.ptr64 then Some (Genv.symbol_address genv s ofs) else None
+  | Ainstack ofs, nil =>
+      if Archi.ptr64 then Some(Val.offset_ptr sp ofs) else None
+  | _, _ => None
+  end.
+
+Definition eval_addressing
+    (F V: Type) (genv: Genv.t F V) (sp: val)
+    (addr: addressing) (vl: list val) : option val :=
+  if Archi.ptr64
+  then eval_addressing64 genv sp addr vl
+  else eval_addressing32 genv sp addr vl.
+
 Definition eval_operation
     (F V: Type) (genv: Genv.t F V) (sp: val)
     (op: operation) (vl: list val) (m: mem): option val :=
   match op, vl with
   | Omove, v1::nil => Some v1
   | Ointconst n, nil => Some (Vint n)
+  | Olongconst n, nil => Some (Vlong n)
   | Ofloatconst n, nil => Some (Vfloat n)
   | Osingleconst n, nil => Some (Vsingle n)
-  | Oindirectsymbol id, nil => Some (Genv.symbol_address genv id Int.zero)
+  | Oindirectsymbol id, nil => Some (Genv.symbol_address genv id Ptrofs.zero)
   | Ocast8signed, v1 :: nil => Some (Val.sign_ext 8 v1)
   | Ocast8unsigned, v1 :: nil => Some (Val.zero_ext 8 v1)
   | Ocast16signed, v1 :: nil => Some (Val.sign_ext 16 v1)
@@ -252,7 +327,36 @@ Definition eval_operation
   | Ororimm n, v1::nil => Some (Val.ror v1 (Vint n))
   | Oshldimm n, v1::v2::nil => Some (Val.or (Val.shl v1 (Vint n))
                                             (Val.shru v2 (Vint (Int.sub Int.iwordsize n))))
-  | Olea addr, _ => eval_addressing genv sp addr vl
+  | Olea addr, _ => eval_addressing32 genv sp addr vl
+  | Omakelong, v1::v2::nil => Some(Val.longofwords v1 v2)
+  | Olowlong, v1::nil => Some(Val.loword v1)
+  | Ohighlong, v1::nil => Some(Val.hiword v1)
+  | Ocast32signed, v1 :: nil => Some (Val.longofint v1)
+  | Ocast32unsigned, v1 :: nil => Some (Val.longofintu v1)
+  | Onegl, v1::nil => Some (Val.negl v1)
+  | Oaddlimm n, v1::nil => Some (Val.addl v1 (Vlong n))
+  | Osubl, v1::v2::nil => Some (Val.subl v1 v2)
+  | Omull, v1::v2::nil => Some (Val.mull v1 v2)
+  | Omullimm n, v1::nil => Some (Val.mull v1 (Vlong n))
+  | Odivl, v1::v2::nil => Val.divls v1 v2
+  | Odivlu, v1::v2::nil => Val.divlu v1 v2
+  | Omodl, v1::v2::nil => Val.modls v1 v2
+  | Omodlu, v1::v2::nil => Val.modlu v1 v2
+  | Oandl, v1::v2::nil => Some(Val.andl v1 v2)
+  | Oandlimm n, v1::nil => Some (Val.andl v1 (Vlong n))
+  | Oorl, v1::v2::nil => Some(Val.orl v1 v2)
+  | Oorlimm n, v1::nil => Some (Val.orl v1 (Vlong n))
+  | Oxorl, v1::v2::nil => Some(Val.xorl v1 v2)
+  | Oxorlimm n, v1::nil => Some (Val.xorl v1 (Vlong n))
+  | Onotl, v1::nil => Some(Val.notl v1)
+  | Oshll, v1::v2::nil => Some (Val.shll v1 v2)
+  | Oshllimm n, v1::nil => Some (Val.shll v1 (Vint n))
+  | Oshrl, v1::v2::nil => Some (Val.shrl v1 v2)
+  | Oshrlimm n, v1::nil => Some (Val.shrl v1 (Vint n))
+  | Oshrlu, v1::v2::nil => Some (Val.shrlu v1 v2)
+  | Oshrluimm n, v1::nil => Some (Val.shrlu v1 (Vint n))
+  | Ororlimm n, v1::nil => Some (Val.rorl v1 (Vint n))
+  | Oleal addr, _ => eval_addressing64 genv sp addr vl
   | Onegf, v1::nil => Some(Val.negf v1)
   | Oabsf, v1::nil => Some(Val.absf v1)
   | Oaddf, v1::v2::nil => Some(Val.addf v1 v2)
@@ -271,21 +375,48 @@ Definition eval_operation
   | Ofloatofint, v1::nil => Val.floatofint v1
   | Ointofsingle, v1::nil => Val.intofsingle v1
   | Osingleofint, v1::nil => Val.singleofint v1
-  | Omakelong, v1::v2::nil => Some(Val.longofwords v1 v2)
-  | Olowlong, v1::nil => Some(Val.loword v1)
-  | Ohighlong, v1::nil => Some(Val.hiword v1)
+  | Olongoffloat, v1::nil => Val.longoffloat v1
+  | Ofloatoflong, v1::nil => Val.floatoflong v1
+  | Olongofsingle, v1::nil => Val.longofsingle v1
+  | Osingleoflong, v1::nil => Val.singleoflong v1
   | Ocmp c, _ => Some(Val.of_optbool (eval_condition c vl m))
   | _, _ => None
   end.
 
+Remark eval_addressing_Aglobal:
+  forall (F V: Type) (genv: Genv.t F V) sp id ofs,
+  eval_addressing genv sp (Aglobal id ofs) nil = Some (Genv.symbol_address genv id ofs).
+Proof.
+  intros. unfold eval_addressing, eval_addressing32, eval_addressing64; destruct Archi.ptr64; auto. 
+Qed.
+
+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. unfold eval_addressing, eval_addressing32, eval_addressing64; destruct Archi.ptr64; auto. 
+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, eval_addressing32, eval_addressing64;
+  intros; destruct Archi.ptr64; destruct vl; inv H; auto.
+Qed.
+
 Ltac FuncInv :=
   match goal with
   | H: (match ?x with nil => _ | _ :: _ => _ end = Some _) |- _ =>
-      destruct x; simpl in H; try discriminate; FuncInv
+      destruct x; simpl in H; try discriminate H; FuncInv
   | H: (match ?v with Vundef => _ | Vint _ => _ | Vfloat _ => _ | Vptr _ _ => _ end = Some _) |- _ =>
-      destruct v; simpl in H; try discriminate; FuncInv
+      destruct v; simpl in H; try discriminate H; FuncInv
+  | H: (if Archi.ptr64 then _ else _) = Some _ |- _ =>
+      destruct Archi.ptr64 eqn:?; try discriminate H; FuncInv
   | H: (Some _ = Some _) |- _ =>
       injection H; intros; clear H; FuncInv
+  | H: (None = Some _) |- _ =>
+      discriminate H
   | _ =>
       idtac
   end.
@@ -298,6 +429,10 @@ Definition type_of_condition (c: condition) : list typ :=
   | Ccompu _ => Tint :: Tint :: nil
   | Ccompimm _ _ => Tint :: nil
   | Ccompuimm _ _ => Tint :: nil
+  | Ccompl _ => Tlong :: Tlong :: nil
+  | Ccomplu _ => Tlong :: Tlong :: nil
+  | Ccomplimm _ _ => Tlong :: nil
+  | Ccompluimm _ _ => Tlong :: nil
   | Ccompf _ => Tfloat :: Tfloat :: nil
   | Cnotcompf _ => Tfloat :: Tfloat :: nil
   | Ccompfs _ => Tsingle :: Tsingle :: nil
@@ -306,25 +441,30 @@ Definition type_of_condition (c: condition) : list typ :=
   | Cmasknotzero _ => Tint :: nil
   end.
 
-Definition type_of_addressing (addr: addressing) : list typ :=
+Definition type_of_addressing_gen (tyA: typ) (addr: addressing): list typ :=
   match addr with
-  | Aindexed _ => Tint :: nil
-  | Aindexed2 _ => Tint :: Tint :: nil
-  | Ascaled _ _ => Tint :: nil
-  | Aindexed2scaled _ _ => Tint :: Tint :: nil
+  | Aindexed _ => tyA :: nil
+  | Aindexed2 _ => tyA :: tyA :: nil
+  | Ascaled _ _ => tyA :: nil
+  | Aindexed2scaled _ _ => tyA :: tyA :: nil
   | Aglobal _ _ => nil
-  | Abased _ _ => Tint :: nil
-  | Abasedscaled _ _ _ => Tint :: nil
+  | Abased _ _ => tyA :: nil
+  | Abasedscaled _ _ _ => tyA :: nil
   | Ainstack _ => nil
   end.
 
+Definition type_of_addressing := type_of_addressing_gen Tptr.
+Definition type_of_addressing32 := type_of_addressing_gen Tint.
+Definition type_of_addressing64 := type_of_addressing_gen Tlong.
+
 Definition type_of_operation (op: operation) : list typ * typ :=
   match op with
   | Omove => (nil, Tint)   (* treated specially *)
   | Ointconst _ => (nil, Tint)
+  | Olongconst _ => (nil, Tlong)
   | Ofloatconst f => (nil, Tfloat)
   | Osingleconst f => (nil, Tsingle)
-  | Oindirectsymbol _ => (nil, Tint)
+  | Oindirectsymbol _ => (nil, Tptr)
   | Ocast8signed => (Tint :: nil, Tint)
   | Ocast8unsigned => (Tint :: nil, Tint)
   | Ocast16signed => (Tint :: nil, Tint)
@@ -355,7 +495,36 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Oshruimm _ => (Tint :: nil, Tint)
   | Ororimm _ => (Tint :: nil, Tint)
   | Oshldimm _ => (Tint :: Tint :: nil, Tint)
-  | Olea addr => (type_of_addressing addr, Tint)
+  | Olea addr => (type_of_addressing32 addr, Tint)
+  | Omakelong => (Tint :: Tint :: nil, Tlong)
+  | Olowlong => (Tlong :: nil, Tint)
+  | Ohighlong => (Tlong :: nil, Tint)
+  | Ocast32signed => (Tint :: nil, Tlong)
+  | Ocast32unsigned => (Tint :: nil, Tlong)
+  | Onegl => (Tlong :: nil, Tlong)
+  | Oaddlimm _ => (Tlong :: nil, Tlong)
+  | Osubl => (Tlong :: Tlong :: nil, Tlong)
+  | Omull => (Tlong :: Tlong :: nil, Tlong)
+  | Omullimm _ => (Tlong :: nil, Tlong)
+  | Odivl => (Tlong :: Tlong :: nil, Tlong)
+  | Odivlu => (Tlong :: Tlong :: nil, Tlong)
+  | Omodl => (Tlong :: Tlong :: nil, Tlong)
+  | Omodlu => (Tlong :: Tlong :: nil, Tlong)
+  | Oandl => (Tlong :: Tlong :: nil, Tlong)
+  | Oandlimm _ => (Tlong :: nil, Tlong)
+  | Oorl => (Tlong :: Tlong :: nil, Tlong)
+  | Oorlimm _ => (Tlong :: nil, Tlong)
+  | Oxorl => (Tlong :: Tlong :: nil, Tlong)
+  | Oxorlimm _ => (Tlong :: nil, Tlong)
+  | Onotl => (Tlong :: nil, Tlong)
+  | Oshll => (Tlong :: Tint :: nil, Tlong)
+  | Oshllimm _ => (Tlong :: nil, Tlong)
+  | Oshrl => (Tlong :: Tint :: nil, Tlong)
+  | Oshrlimm _ => (Tlong :: nil, Tlong)
+  | Oshrlu => (Tlong :: Tint :: nil, Tlong)
+  | Oshrluimm _ => (Tlong :: nil, Tlong)
+  | Ororlimm _ => (Tlong :: nil, Tlong)
+  | Oleal addr => (type_of_addressing64 addr, Tlong)
   | Onegf => (Tfloat :: nil, Tfloat)
   | Oabsf => (Tfloat :: nil, Tfloat)
   | Oaddf => (Tfloat :: Tfloat :: nil, Tfloat)
@@ -374,9 +543,10 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Ofloatofint => (Tint :: nil, Tfloat)
   | Ointofsingle => (Tsingle :: nil, Tint)
   | Osingleofint => (Tint :: nil, Tsingle)
-  | Omakelong => (Tint :: Tint :: nil, Tlong)
-  | Olowlong => (Tlong :: nil, Tint)
-  | Ohighlong => (Tlong :: nil, Tint)
+  | Olongoffloat => (Tfloat :: nil, Tlong)
+  | Ofloatoflong => (Tlong :: nil, Tfloat)
+  | Olongofsingle => (Tsingle :: nil, Tlong)
+  | Osingleoflong => (Tlong :: nil, Tsingle)
   | Ocmp c => (type_of_condition c, Tint)
   end.
 
@@ -389,22 +559,45 @@ Section SOUNDNESS.
 Variable A V: Type.
 Variable genv: Genv.t A V.
 
-Lemma type_of_addressing_sound:
+Remark type_add:
+  forall v1 v2, Val.has_type (Val.add v1 v2) Tint.
+Proof.
+  intros. unfold Val.has_type, Val.add. destruct Archi.ptr64, v1, v2; auto.
+Qed.
+
+Remark type_addl:
+  forall v1 v2, Val.has_type (Val.addl v1 v2) Tlong.
+Proof.
+  intros. unfold Val.has_type, Val.addl. destruct Archi.ptr64, v1, v2; auto.
+Qed.
+
+Lemma type_of_addressing64_sound:
   forall addr vl sp v,
-  eval_addressing genv sp addr vl = Some v ->
+  eval_addressing64 genv sp addr vl = Some v ->
+  Val.has_type v Tlong.
+Proof.
+  intros. destruct addr; simpl in H; FuncInv; subst; simpl; auto using type_addl.
+- unfold Genv.symbol_address; destruct (Genv.find_symbol genv i); simpl; auto.
+- destruct sp; simpl; auto.
+Qed.
+
+Lemma type_of_addressing32_sound:
+  forall addr vl sp v,
+  eval_addressing32 genv sp addr vl = Some v ->
   Val.has_type v Tint.
-Proof with (try exact I).
-  intros. destruct addr; simpl in H; FuncInv; subst; simpl.
-  destruct v0...
-  destruct v0... destruct v1... destruct v1...
-  destruct v0...
-  destruct v0... destruct v1... destruct v1...
-  unfold Genv.symbol_address; destruct (Genv.find_symbol genv i)...
-  unfold Genv.symbol_address; destruct (Genv.find_symbol genv i)...
-  unfold Genv.symbol_address; destruct (Genv.find_symbol genv i)... destruct v0...
-  destruct v0...
-  unfold Genv.symbol_address; destruct (Genv.find_symbol genv i0)... destruct v0...
-  destruct sp...
+Proof.
+  intros. destruct addr; simpl in H; FuncInv; subst; simpl; auto using type_add.
+- unfold Genv.symbol_address; destruct (Genv.find_symbol genv i); simpl; auto.
+- destruct sp; simpl; auto.
+Qed.
+
+Corollary type_of_addressing_sound:
+  forall addr vl sp v,
+  eval_addressing genv sp addr vl = Some v ->
+  Val.has_type v Tptr.
+Proof.
+  unfold eval_addressing, Tptr; intros. 
+  destruct Archi.ptr64; eauto using type_of_addressing64_sound, type_of_addressing32_sound.
 Qed.
 
 Lemma type_of_operation_sound:
@@ -419,13 +612,17 @@ Proof with (try exact I).
   exact I.
   exact I.
   exact I.
-  unfold Genv.symbol_address; destruct (Genv.find_symbol genv i)...
+  exact I.
+  unfold Genv.symbol_address; destruct (Genv.find_symbol genv id)...
+    unfold Val.has_type, Tptr; destruct Archi.ptr64; auto.
   destruct v0...
   destruct v0...
   destruct v0...
   destruct v0...
   destruct v0...
-  destruct v0; destruct v1... simpl. destruct (eq_block b b0)...
+  destruct v0; destruct v1; simpl...
+    unfold Val.has_type; destruct Archi.ptr64; auto.
+    unfold Val.has_type; destruct Archi.ptr64; auto. destruct (eq_block b b0); auto.
   destruct v0; destruct v1...
   destruct v0...
   destruct v0; destruct v1...
@@ -444,16 +641,49 @@ Proof with (try exact I).
   destruct v0...
   destruct v0...
   destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int.iwordsize)...
-  destruct v0; simpl... destruct (Int.ltu i Int.iwordsize)...
+  destruct v0; simpl... destruct (Int.ltu n Int.iwordsize)...
   destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int.iwordsize)...
-  destruct v0; simpl... destruct (Int.ltu i Int.iwordsize)...
-  destruct v0; simpl in H0; try discriminate. destruct (Int.ltu i (Int.repr 31)); inv H0...
+  destruct v0; simpl... destruct (Int.ltu n Int.iwordsize)...
+  destruct v0; simpl in H0; try discriminate. destruct (Int.ltu n (Int.repr 31)); inv H0...
   destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int.iwordsize)...
-  destruct v0; simpl... destruct (Int.ltu i Int.iwordsize)...
+  destruct v0; simpl... destruct (Int.ltu n Int.iwordsize)...
+  destruct v0...
+  destruct v0; simpl... destruct (Int.ltu n Int.iwordsize)...
+  destruct v1; simpl... destruct (Int.ltu (Int.sub Int.iwordsize n) Int.iwordsize)...
+  eapply type_of_addressing32_sound; eauto.
+  destruct v0; destruct v1...
+  destruct v0...
+  destruct v0...
+  destruct v0...
+  destruct v0...
+  destruct v0...
+  destruct v0; simpl... unfold Val.has_type; destruct Archi.ptr64; auto. 
+  destruct v0; destruct v1; simpl...
+    unfold Val.has_type; destruct Archi.ptr64; auto.
+    unfold Val.has_type; destruct Archi.ptr64; simpl; auto. destruct (eq_block b b0); auto.
+  destruct v0; destruct v1...
+  destruct v0...
+  destruct v0; destruct v1; simpl in *; inv H0.
+    destruct (Int64.eq i0 Int64.zero || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H2...
+  destruct v0; destruct v1; simpl in *; inv H0. destruct (Int64.eq i0 Int64.zero); inv H2...
+  destruct v0; destruct v1; simpl in *; inv H0.
+    destruct (Int64.eq i0 Int64.zero || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H2...
+  destruct v0; destruct v1; simpl in *; inv H0. destruct (Int64.eq i0 Int64.zero); inv H2...
+  destruct v0; destruct v1...
+  destruct v0...
+  destruct v0; destruct v1...
+  destruct v0...
+  destruct v0; destruct v1...
+  destruct v0...
+  destruct v0...
+  destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int64.iwordsize')...
+  destruct v0; simpl... destruct (Int.ltu n Int64.iwordsize')...
+  destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int64.iwordsize')...
+  destruct v0; simpl... destruct (Int.ltu n Int64.iwordsize')...
+  destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int64.iwordsize')...
+  destruct v0; simpl... destruct (Int.ltu n Int64.iwordsize')...
   destruct v0...
-  destruct v0; simpl... destruct (Int.ltu i Int.iwordsize)...
-  destruct v1; simpl... destruct (Int.ltu (Int.sub Int.iwordsize i) Int.iwordsize)...
-  eapply type_of_addressing_sound; eauto.
+  eapply type_of_addressing64_sound; eauto.
   destruct v0...
   destruct v0...
   destruct v0; destruct v1...
@@ -472,10 +702,11 @@ Proof with (try exact I).
   destruct v0; simpl in H0; inv H0...
   destruct v0; simpl in H0; inv H0. destruct (Float32.to_int f); inv H2...
   destruct v0; simpl in H0; inv H0...
-  destruct v0; destruct v1...
-  destruct v0...
-  destruct v0...
-  destruct (eval_condition c vl m); simpl... destruct b...
+  destruct v0; simpl in H0; inv H0. destruct (Float.to_long f); inv H2...
+  destruct v0; simpl in H0; inv H0...
+  destruct v0; simpl in H0; inv H0. destruct (Float32.to_long f); inv H2...
+  destruct v0; simpl in H0; inv H0...
+  destruct (eval_condition cond vl m); simpl... destruct b...
 Qed.
 
 End SOUNDNESS.
@@ -512,6 +743,10 @@ Definition negate_condition (cond: condition): condition :=
   | Ccompu c => Ccompu(negate_comparison c)
   | Ccompimm c n => Ccompimm (negate_comparison c) n
   | Ccompuimm c n => Ccompuimm (negate_comparison c) n
+  | Ccompl c => Ccompl(negate_comparison c)
+  | Ccomplu c => Ccomplu(negate_comparison c)
+  | Ccomplimm c n => Ccomplimm (negate_comparison c) n
+  | Ccompluimm c n => Ccompluimm (negate_comparison c) n
   | Ccompf c => Cnotcompf c
   | Cnotcompf c => Ccompf c
   | Ccompfs c => Cnotcompfs c
@@ -529,25 +764,30 @@ Proof.
   repeat (destruct vl; auto). apply Val.negate_cmpu_bool.
   repeat (destruct vl; auto). apply Val.negate_cmp_bool.
   repeat (destruct vl; auto). apply Val.negate_cmpu_bool.
+  repeat (destruct vl; auto). apply Val.negate_cmpl_bool.
+  repeat (destruct vl; auto). apply Val.negate_cmplu_bool.
+  repeat (destruct vl; auto). apply Val.negate_cmpl_bool.
+  repeat (destruct vl; auto). apply Val.negate_cmplu_bool.
   repeat (destruct vl; auto).
   repeat (destruct vl; auto). destruct (Val.cmpf_bool c v v0) as [[]|]; auto.
   repeat (destruct vl; auto).
   repeat (destruct vl; auto). destruct (Val.cmpfs_bool c v v0) as [[]|]; auto.
   destruct vl; auto. destruct vl; auto.
-  destruct vl; auto. destruct vl; auto. destruct (Val.maskzero_bool v i) as [[]|]; auto.
+  destruct vl; auto. destruct vl; auto. destruct (Val.maskzero_bool v n) as [[]|]; auto.
 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 ofs (Ptrofs.repr delta))
   | _ => addr
   end.
 
-Definition shift_stack_operation (delta: int) (op: operation) :=
+Definition shift_stack_operation (delta: Z) (op: operation) :=
   match op with
-  | Olea addr => Olea (shift_stack_addressing delta addr)
+  | Olea  addr => Olea  (shift_stack_addressing delta addr)
+  | Oleal addr => Oleal (shift_stack_addressing delta addr)
   | _ => op
   end.
 
@@ -560,75 +800,116 @@ Qed.
 Lemma type_shift_stack_operation:
   forall delta op, type_of_operation (shift_stack_operation delta op) = type_of_operation op.
 Proof.
-  intros. destruct op; auto. simpl. decEq. apply type_shift_stack_addressing.
+  intros. destruct op; auto; simpl; decEq; destruct a; auto.
 Qed.
 
-Lemma eval_shift_stack_addressing:
+Lemma eval_shift_stack_addressing32:
   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_addressing32 ge (Vptr sp Ptrofs.zero) (shift_stack_addressing delta addr) vl =
+  eval_addressing32 ge (Vptr sp (Ptrofs.repr delta)) addr vl.
 Proof.
   intros. destruct addr; simpl; auto.
-  rewrite Val.add_assoc. simpl. auto.
+  destruct vl; auto. destruct Archi.ptr64 eqn:SF; auto.
+  do 2 f_equal. rewrite Ptrofs.add_zero_l. apply Ptrofs.add_commut.
+Qed.
+
+Lemma eval_shift_stack_addressing64:
+  forall F V (ge: Genv.t F V) sp addr vl delta,
+  eval_addressing64 ge (Vptr sp Ptrofs.zero) (shift_stack_addressing delta addr) vl =
+  eval_addressing64 ge (Vptr sp (Ptrofs.repr delta)) addr vl.
+Proof.
+  intros. destruct addr; simpl; auto.
+  destruct vl; auto. destruct Archi.ptr64 eqn:SF; auto.
+  do 2 f_equal. rewrite Ptrofs.add_zero_l. apply Ptrofs.add_commut.
+Qed.
+
+Lemma eval_shift_stack_addressing:
+  forall F V (ge: Genv.t F V) sp addr vl delta,
+  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. unfold eval_addressing. 
+  destruct Archi.ptr64; auto using eval_shift_stack_addressing32, eval_shift_stack_addressing64.
 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.
-  apply eval_shift_stack_addressing.
+  intros. destruct op; simpl; auto using eval_shift_stack_addressing32, eval_shift_stack_addressing64.
 Qed.
 
 (** Offset an addressing mode [addr] by a quantity [delta], so that
   it designates the pointer [delta] bytes past the pointer designated
-  by [addr].  On PowerPC and ARM, this may be undefined, in which case
-  [None] is returned.  On IA32, it is always defined, but we keep the
-  same interface. *)
+  by [addr].  This may be undefined if an offset overflows, in which case
+  [None] is returned.  *)
 
-Definition offset_addressing_total (addr: addressing) (delta: int) : addressing :=
+Definition offset_addressing_total (addr: addressing) (delta: Z) : addressing :=
   match addr with
-  | Aindexed n => Aindexed (Int.add n delta)
-  | Aindexed2 n => Aindexed2 (Int.add n delta)
-  | Ascaled sc n => Ascaled sc (Int.add n delta)
-  | Aindexed2scaled sc n => Aindexed2scaled sc (Int.add n delta)
-  | Aglobal s n => Aglobal s (Int.add n delta)
-  | Abased s n => Abased s (Int.add n delta)
-  | Abasedscaled sc s n => Abasedscaled sc s (Int.add n delta)
-  | Ainstack n => Ainstack (Int.add n delta)
+  | Aindexed n => Aindexed (n + delta)
+  | Aindexed2 n => Aindexed2 (n + delta)
+  | Ascaled sc n => Ascaled sc (n + delta)
+  | Aindexed2scaled sc n => Aindexed2scaled sc (n + delta)
+  | Aglobal s n => Aglobal s (Ptrofs.add n (Ptrofs.repr delta))
+  | Abased s n => Abased s (Ptrofs.add n (Ptrofs.repr delta))
+  | Abasedscaled sc s n => Abasedscaled sc s (Ptrofs.add n (Ptrofs.repr delta))
+  | Ainstack n => Ainstack (Ptrofs.add n (Ptrofs.repr delta))
   end.
 
-Definition offset_addressing (addr: addressing) (delta: int) : option addressing :=
-  Some(offset_addressing_total addr delta).
+Definition offset_addressing (addr: addressing) (delta: Z) : option addressing :=
+  let addr' := offset_addressing_total addr delta in
+  if addressing_valid addr' then Some addr' else None.
 
-Lemma eval_offset_addressing_total:
+Lemma eval_offset_addressing_total_32:
   forall (F V: Type) (ge: Genv.t F V) sp addr args delta v,
-  eval_addressing ge sp addr args = Some v ->
-  eval_addressing ge sp (offset_addressing_total addr delta) args =
-    Some(Val.add v (Vint delta)).
+  eval_addressing32 ge sp addr args = Some v ->
+  eval_addressing32 ge sp (offset_addressing_total addr delta) args = Some(Val.add v (Vint (Int.repr delta))).
 Proof.
-  intros. destruct addr; simpl in *; FuncInv; subst.
-  rewrite Val.add_assoc; auto.
-  rewrite !Val.add_assoc; auto.
-  rewrite !Val.add_assoc; auto.
-  rewrite !Val.add_assoc; auto.
-  unfold Genv.symbol_address. destruct (Genv.find_symbol ge i); auto.
-  unfold Genv.symbol_address. destruct (Genv.find_symbol ge i); auto.
-  rewrite Val.add_assoc. rewrite Val.add_permut. rewrite Val.add_commut. auto.
-  unfold Genv.symbol_address. destruct (Genv.find_symbol ge i0); auto.
-  rewrite Val.add_assoc. rewrite Val.add_permut. rewrite Val.add_commut. auto.
-  rewrite Val.add_assoc. auto.
+  assert (A: forall x y, Int.add (Int.repr x) (Int.repr y) = Int.repr (x + y)).
+  { intros. apply Int.eqm_samerepr; auto with ints. }
+  assert (B: forall delta, Archi.ptr64 = false -> Ptrofs.repr delta = Ptrofs.of_int (Int.repr delta)).
+  { intros; symmetry; auto with ptrofs. }
+  intros. destruct addr; simpl in *; FuncInv; subst; simpl.
+- rewrite <- A, ! Val.add_assoc; auto.
+- rewrite <- A, ! Val.add_assoc; auto.
+- rewrite <- A, ! Val.add_assoc; auto.
+- rewrite <- A, ! Val.add_assoc; auto.
+- rewrite B, Genv.shift_symbol_address_32 by auto. auto.
+- rewrite B, Genv.shift_symbol_address_32 by auto. rewrite ! Val.add_assoc. do 2 f_equal. apply Val.add_commut.
+- rewrite B, Genv.shift_symbol_address_32 by auto. rewrite ! Val.add_assoc. do 2 f_equal. apply Val.add_commut.
+- destruct sp; simpl; auto. rewrite Heqb. rewrite Ptrofs.add_assoc. do 4 f_equal. symmetry; auto with ptrofs.
 Qed.
 
+Lemma eval_offset_addressing_total_64:
+  forall (F V: Type) (ge: Genv.t F V) sp addr args delta v,
+  eval_addressing64 ge sp addr args = Some v ->
+  eval_addressing64 ge sp (offset_addressing_total addr delta) args = Some(Val.addl v (Vlong (Int64.repr delta))).
+Proof.
+  assert (A: forall x y, Int64.add (Int64.repr x) (Int64.repr y) = Int64.repr (x + y)).
+  { intros. apply Int64.eqm_samerepr; auto with ints. }
+  assert (B: forall delta, Archi.ptr64 = true -> Ptrofs.repr delta = Ptrofs.of_int64 (Int64.repr delta)).
+  { intros; symmetry; auto with ptrofs. }
+  intros. destruct addr; simpl in *; FuncInv; subst; simpl.
+- rewrite <- A, ! Val.addl_assoc; auto.
+- rewrite <- A, ! Val.addl_assoc; auto.
+- rewrite <- A, ! Val.addl_assoc; auto.
+- rewrite <- A, ! Val.addl_assoc; auto.
+- rewrite B, Genv.shift_symbol_address_64 by auto. auto.
+- destruct sp; simpl; auto. rewrite Heqb. rewrite Ptrofs.add_assoc. do 4 f_equal. symmetry; auto with ptrofs.
+Qed.
+
+(** The following lemma is used only in [Allocproof] in cases where [Archi.ptr64 = false]. *)
+
 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)).
+  Archi.ptr64 = false ->
+  eval_addressing ge sp addr' args = Some(Val.add v (Vint (Int.repr delta))).
 Proof.
-  intros. unfold offset_addressing in H; inv H.
-  eapply eval_offset_addressing_total; eauto.
+  intros. unfold offset_addressing in H. destruct (addressing_valid (offset_addressing_total addr delta)); inv H.
+  unfold eval_addressing in *; rewrite H1 in *. apply eval_offset_addressing_total_32; auto.
 Qed.
 
 (** Operations that are so cheap to recompute that CSE should not factor them out. *)
@@ -637,8 +918,11 @@ Definition is_trivial_op (op: operation) : bool :=
   match op with
   | Omove => true
   | Ointconst _ => true
+  | Olongconst _ => true
   | Olea (Aglobal _ _) => true
   | Olea (Ainstack _) => true
+  | Oleal (Aglobal _ _) => true
+  | Oleal (Ainstack _) => true
   | _ => false
   end.
 
@@ -646,8 +930,10 @@ Definition is_trivial_op (op: operation) : bool :=
 
 Definition op_depends_on_memory (op: operation) : bool :=
   match op with
-  | Ocmp (Ccompu _) => true
-  | Ocmp (Ccompuimm _ _) => true
+  | Ocmp (Ccompu _) => negb Archi.ptr64
+  | Ocmp (Ccompuimm _ _) => negb Archi.ptr64
+  | Ocmp (Ccomplu _) => Archi.ptr64
+  | Ocmp (Ccompluimm _ _) => Archi.ptr64
   | _ => false
   end.
 
@@ -657,7 +943,8 @@ Lemma op_depends_on_memory_correct:
   eval_operation ge sp op args m1 = eval_operation ge sp op args m2.
 Proof.
   intros until m2. destruct op; simpl; try congruence.
-  destruct c; simpl; auto; congruence.
+  destruct cond; simpl; intros SF; auto; rewrite ? negb_false_iff in SF;
+  unfold Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity.
 Qed.
 
 (** Global variables mentioned in an operation or addressing mode *)
@@ -674,6 +961,7 @@ Definition globals_operation (op: operation) : list ident :=
   match op with
   | Oindirectsymbol s => s :: nil
   | Olea addr => globals_addressing addr
+  | Oleal addr => globals_addressing addr
   | _ => nil
   end.
 
@@ -692,13 +980,30 @@ Variable ge2: Genv.t F2 V2.
 Hypothesis agree_on_symbols:
   forall (s: ident), Genv.find_symbol ge2 s = Genv.find_symbol ge1 s.
 
+Lemma eval_addressing32_preserved:
+  forall sp addr vl,
+  eval_addressing32 ge2 sp addr vl = eval_addressing32 ge1 sp addr vl.
+Proof.
+  intros.
+  unfold eval_addressing32, Genv.symbol_address; destruct addr; try rewrite agree_on_symbols;
+  reflexivity.
+Qed.
+
+Lemma eval_addressing64_preserved:
+  forall sp addr vl,
+  eval_addressing64 ge2 sp addr vl = eval_addressing64 ge1 sp addr vl.
+Proof.
+  intros.
+  unfold eval_addressing64, Genv.symbol_address; destruct addr; try rewrite agree_on_symbols;
+  reflexivity.
+Qed.
+
 Lemma eval_addressing_preserved:
   forall sp addr vl,
   eval_addressing ge2 sp addr vl = eval_addressing ge1 sp addr vl.
 Proof.
   intros.
-  unfold eval_addressing, Genv.symbol_address; destruct addr; try rewrite agree_on_symbols;
-  reflexivity.
+  unfold eval_addressing; destruct Archi.ptr64; auto using eval_addressing32_preserved, eval_addressing64_preserved.
 Qed.
 
 Lemma eval_operation_preserved:
@@ -708,7 +1013,8 @@ Proof.
   intros.
   unfold eval_operation; destruct op; auto.
   unfold Genv.symbol_address. rewrite agree_on_symbols. auto.
-  apply eval_addressing_preserved.
+  apply eval_addressing32_preserved.
+  apply eval_addressing64_preserved.
 Qed.
 
 End GENV_TRANSF.
@@ -728,30 +1034,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
@@ -775,16 +1081,20 @@ Lemma eval_condition_inj:
   eval_condition cond vl2 m2 = Some b.
 Proof.
   intros. destruct cond; simpl in H0; FuncInv; InvInject; simpl; auto.
-  inv H3; inv H2; simpl in H0; inv H0; auto.
-  eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies.
-  inv H3; simpl in H0; inv H0; auto.
-  eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies.
-  inv H3; inv H2; simpl in H0; inv H0; auto.
-  inv H3; inv H2; simpl in H0; inv H0; auto.
-  inv H3; inv H2; simpl in H0; inv H0; auto.
-  inv H3; inv H2; simpl in H0; inv H0; auto.
-  inv H3; try discriminate; auto.
-  inv H3; try discriminate; auto.
+- inv H3; inv H2; simpl in H0; inv H0; auto.
+- eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies.
+- inv H3; simpl in H0; inv H0; auto.
+- eauto 3 using Val.cmpu_bool_inject, Mem.valid_pointer_implies.
+- inv H3; inv H2; simpl in H0; inv H0; auto.
+- eauto 3 using Val.cmplu_bool_inject, Mem.valid_pointer_implies.
+- inv H3; simpl in H0; inv H0; auto.
+- eauto 3 using Val.cmplu_bool_inject, Mem.valid_pointer_implies.
+- inv H3; inv H2; simpl in H0; inv H0; auto.
+- inv H3; inv H2; simpl in H0; inv H0; auto.
+- inv H3; inv H2; simpl in H0; inv H0; auto.
+- inv H3; inv H2; simpl in H0; inv H0; auto.
+- inv H3; try discriminate; auto.
+- inv H3; try discriminate; auto.
 Qed.
 
 Ltac TrivialExists :=
@@ -794,6 +1104,36 @@ Ltac TrivialExists :=
   | _ => idtac
   end.
 
+Lemma eval_addressing32_inj:
+  forall addr sp1 vl1 sp2 vl2 v1,
+  (forall id ofs,
+      In id (globals_addressing addr) ->
+      Val.inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) ->
+  Val.inject f sp1 sp2 ->
+  Val.inject_list f vl1 vl2 ->
+  eval_addressing32 ge1 sp1 addr vl1 = Some v1 ->
+  exists v2, eval_addressing32 ge2 sp2 addr vl2 = Some v2 /\ Val.inject f v1 v2.
+Proof.
+  assert (A: forall v1 v2 v1' v2', Val.inject f v1 v1' -> Val.inject f v2 v2' -> Val.inject f (Val.mul v1 v2) (Val.mul v1' v2')).
+  { intros. inv H; simpl; auto. inv H0; auto. }
+  intros. destruct addr; simpl in *; FuncInv; InvInject; TrivialExists; eauto using Val.add_inject, Val.offset_ptr_inject with coqlib.
+Qed.
+
+Lemma eval_addressing64_inj:
+  forall addr sp1 vl1 sp2 vl2 v1,
+  (forall id ofs,
+      In id (globals_addressing addr) ->
+      Val.inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) ->
+  Val.inject f sp1 sp2 ->
+  Val.inject_list f vl1 vl2 ->
+  eval_addressing64 ge1 sp1 addr vl1 = Some v1 ->
+  exists v2, eval_addressing64 ge2 sp2 addr vl2 = Some v2 /\ Val.inject f v1 v2.
+Proof.
+  assert (A: forall v1 v2 v1' v2', Val.inject f v1 v1' -> Val.inject f v2 v2' -> Val.inject f (Val.mull v1 v2) (Val.mull v1' v2')).
+  { intros. inv H; simpl; auto. inv H0; auto. }
+  intros. destruct addr; simpl in *; FuncInv; InvInject; TrivialExists; eauto using Val.addl_inject, Val.offset_ptr_inject with coqlib.
+Qed.
+
 Lemma eval_addressing_inj:
   forall addr sp1 vl1 sp2 vl2 v1,
   (forall id ofs,
@@ -804,15 +1144,7 @@ Lemma eval_addressing_inj:
   eval_addressing ge1 sp1 addr vl1 = Some v1 ->
   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 Values.Val.add_inject; auto. inv H5; simpl; auto.
-  apply Values.Val.add_inject; auto. apply Values.Val.add_inject; auto. inv H3; simpl; auto.
-  apply H; simpl; auto.
-  apply Values.Val.add_inject; auto. apply H; simpl; auto.
-  apply Values.Val.add_inject; auto. apply H; simpl; auto. inv H5; simpl; auto.
-  apply Values.Val.add_inject; auto.
+  unfold eval_addressing; intros. destruct Archi.ptr64; eauto using eval_addressing32_inj, eval_addressing64_inj.
 Qed.
 
 Lemma eval_operation_inj:
@@ -832,10 +1164,7 @@ Proof.
   inv H4; simpl; auto.
   inv H4; simpl; auto.
   inv H4; simpl; auto.
-  inv H4; inv H2; simpl; auto. econstructor; eauto.
-    rewrite Int.sub_add_l. auto.
-    destruct (eq_block b1 b0); auto. subst. rewrite H1 in H0. inv H0. rewrite dec_eq_true.
-    rewrite Int.sub_shifted. auto.
+  apply Val.sub_inject; auto.
   inv H4; inv H2; simpl; auto.
   inv H4; simpl; auto.
   inv H4; inv H2; simpl; auto.
@@ -856,17 +1185,50 @@ Proof.
   inv H4; simpl; auto.
   inv H4; simpl; auto.
   inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int.iwordsize); auto.
-  inv H4; simpl; auto. destruct (Int.ltu i Int.iwordsize); auto.
+  inv H4; simpl; auto. destruct (Int.ltu n Int.iwordsize); auto.
   inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int.iwordsize); auto.
-  inv H4; simpl; auto. destruct (Int.ltu i Int.iwordsize); auto.
+  inv H4; simpl; auto. destruct (Int.ltu n Int.iwordsize); auto.
   inv H4; simpl in H1; try discriminate. simpl.
-  destruct (Int.ltu i (Int.repr 31)); inv H1. TrivialExists.
+  destruct (Int.ltu n (Int.repr 31)); inv H1. TrivialExists.
   inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int.iwordsize); auto.
-  inv H4; simpl; auto. destruct (Int.ltu i Int.iwordsize); auto.
+  inv H4; simpl; auto. destruct (Int.ltu n Int.iwordsize); auto.
+  inv H4; simpl; auto.
+  inv H4; simpl; auto. destruct (Int.ltu n Int.iwordsize); auto.
+  inv H2; simpl; auto. destruct (Int.ltu (Int.sub Int.iwordsize n) Int.iwordsize); auto.
+  eapply eval_addressing32_inj; eauto.
+  inv H4; inv H2; simpl; auto.
+  inv H4; simpl; auto.
+  inv H4; simpl; auto.
+  inv H4; simpl; auto.
   inv H4; simpl; auto.
-  inv H4; simpl; auto. destruct (Int.ltu i Int.iwordsize); auto.
-  inv H2; simpl; auto. destruct (Int.ltu (Int.sub Int.iwordsize i) Int.iwordsize); auto.
-  eapply eval_addressing_inj; eauto.
+  inv H4; simpl; auto.
+  apply Val.addl_inject; auto.
+  apply Val.subl_inject; auto.
+  inv H4; inv H2; simpl; auto.
+  inv H4; simpl; auto.
+  inv H4; inv H3; simpl in H1; inv H1. simpl.
+    destruct (Int64.eq i0 Int64.zero || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H2. TrivialExists.
+  inv H4; inv H3; simpl in H1; inv H1. simpl.
+    destruct (Int64.eq i0 Int64.zero); inv H2. TrivialExists.
+  inv H4; inv H3; simpl in H1; inv H1. simpl.
+    destruct (Int64.eq i0 Int64.zero || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H2. TrivialExists.
+  inv H4; inv H3; simpl in H1; inv H1. simpl.
+    destruct (Int64.eq i0 Int64.zero); inv H2. TrivialExists.
+  inv H4; inv H2; simpl; auto.
+  inv H4; simpl; auto.
+  inv H4; inv H2; simpl; auto.
+  inv H4; simpl; auto.
+  inv H4; inv H2; simpl; auto.
+  inv H4; simpl; auto.
+  inv H4; simpl; auto.
+  inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto.
+  inv H4; simpl; auto. destruct (Int.ltu n Int64.iwordsize'); auto.
+  inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto.
+  inv H4; simpl; auto. destruct (Int.ltu n Int64.iwordsize'); auto.
+  inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto.
+  inv H4; simpl; auto. destruct (Int.ltu n Int64.iwordsize'); auto.
+  inv H4; simpl; auto.
+  eapply eval_addressing64_inj; eauto.
   inv H4; simpl; auto.
   inv H4; simpl; auto.
   inv H4; inv H2; simpl; auto.
@@ -887,10 +1249,13 @@ Proof.
   inv H4; simpl in H1; inv H1. simpl. destruct (Float32.to_int f0); simpl in H2; inv H2.
   exists (Vint i); auto.
   inv H4; simpl in H1; inv H1. simpl. TrivialExists.
-  inv H4; inv H2; simpl; auto.
-  inv H4; simpl; auto.
-  inv H4; simpl; auto.
-  subst v1. destruct (eval_condition c vl1 m1) eqn:?.
+  inv H4; simpl in H1; inv H1. simpl. destruct (Float.to_long f0); simpl in H2; inv H2.
+  exists (Vlong i); auto.
+  inv H4; simpl in H1; inv H1. simpl. TrivialExists.
+  inv H4; simpl in H1; inv H1. simpl. destruct (Float32.to_long f0); simpl in H2; inv H2.
+  exists (Vlong i); auto.
+  inv H4; simpl in H1; inv H1. simpl. TrivialExists.
+  subst v1. destruct (eval_condition cond vl1 m1) eqn:?.
   exploit eval_condition_inj; eauto. intros EQ; rewrite EQ.
   destruct b; simpl; constructor.
   simpl; constructor.
@@ -909,40 +1274,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.
@@ -1022,7 +1387,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:
@@ -1042,34 +1407,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.
+  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.