Big merge of the newregalloc-int64 branch. Lots of changes in two directions:

1- new register allocator (+ live range splitting, spilling&reloading, etc)
   based on a posteriori validation using the Rideau-Leroy algorithm
2- support for 64-bit integer arithmetic (type "long long").


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

8 files changed, 741 insertions, 70 deletions

diff --git a/common/AST.v b/common/AST.v
index 8595b95..1f7f7d3 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -17,6 +17,7 @@
   the abstract syntax trees of many of the intermediate languages. *)
 
 Require Import Coqlib.
+Require String.
 Require Import Errors.
 Require Import Integers.
 Require Import Floats.
@@ -32,16 +33,19 @@ Definition ident := positive.
 
 Definition ident_eq := peq.
 
-(** The intermediate languages are weakly typed, using only two types:
-  [Tint] for integers and pointers, and [Tfloat] for floating-point
-  numbers. *)
+Parameter ident_of_string : String.string -> ident.
+
+(** The intermediate languages are weakly typed, using only three
+  types: [Tint] for 32-bit integers and pointers, [Tfloat] for 64-bit
+  floating-point numbers, [Tlong] for 64-bit integers. *)
 
 Inductive typ : Type :=
-  | Tint : typ
-  | Tfloat : typ.
+  | Tint
+  | Tfloat
+  | Tlong.
 
 Definition typesize (ty: typ) : Z :=
-  match ty with Tint => 4 | Tfloat => 8 end.
+  match ty with Tint => 4 | Tfloat => 8 | Tlong => 8 end.
 
 Lemma typesize_pos: forall ty, typesize ty > 0.
 Proof. destruct ty; simpl; omega. Qed.
@@ -54,6 +58,9 @@ Lemma opt_typ_eq: forall (t1 t2: option typ), {t1=t2} + {t1<>t2}.
 Proof. decide equality. apply typ_eq. Defined.
 Global Opaque opt_typ_eq.
 
+Definition list_typ_eq: forall (l1 l2: list typ), {l1=l2} + {l1<>l2}
+                     := list_eq_dec typ_eq.
+
 (** Additionally, function definitions and function calls are annotated
   by function signatures indicating the number and types of arguments,
   as well as the type of the returned value if any.  These signatures
@@ -76,14 +83,15 @@ Definition proj_sig_res (s: signature) : typ :=
   chunk of memory being accessed. *)
 
 Inductive memory_chunk : Type :=
-  | Mint8signed : memory_chunk     (**r 8-bit signed integer *)
-  | Mint8unsigned : memory_chunk   (**r 8-bit unsigned integer *)
-  | Mint16signed : memory_chunk    (**r 16-bit signed integer *)
-  | Mint16unsigned : memory_chunk  (**r 16-bit unsigned integer *)
-  | Mint32 : memory_chunk          (**r 32-bit integer, or pointer *)
-  | Mfloat32 : memory_chunk        (**r 32-bit single-precision float *)
-  | Mfloat64 : memory_chunk        (**r 64-bit double-precision float *)
-  | Mfloat64al32 : memory_chunk.   (**r 64-bit double-precision float, 4-aligned *)
+  | Mint8signed     (**r 8-bit signed integer *)
+  | Mint8unsigned   (**r 8-bit unsigned integer *)
+  | Mint16signed    (**r 16-bit signed integer *)
+  | Mint16unsigned  (**r 16-bit unsigned integer *)
+  | Mint32          (**r 32-bit integer, or pointer *)
+  | Mint64          (**r 64-bit integer *)
+  | Mfloat32        (**r 32-bit single-precision float *)
+  | Mfloat64        (**r 64-bit double-precision float *)
+  | Mfloat64al32.   (**r 64-bit double-precision float, 4-aligned *)
 
 (** The type (integer/pointer or float) of a chunk. *)
 
@@ -94,6 +102,7 @@ Definition type_of_chunk (c: memory_chunk) : typ :=
   | Mint16signed => Tint
   | Mint16unsigned => Tint
   | Mint32 => Tint
+  | Mint64 => Tlong
   | Mfloat32 => Tfloat
   | Mfloat64 => Tfloat
   | Mfloat64al32 => Tfloat
@@ -105,6 +114,7 @@ Inductive init_data: Type :=
   | Init_int8: int -> init_data
   | Init_int16: int -> init_data
   | Init_int32: int -> init_data
+  | Init_int64: int64 -> init_data
   | Init_float32: float -> init_data
   | Init_float64: float -> init_data
   | Init_space: Z -> init_data
@@ -549,4 +559,3 @@ Definition transf_partial_fundef (fd: fundef A): res (fundef B) :=
   end.
 
 End TRANSF_PARTIAL_FUNDEF.
-
diff --git a/common/Errors.v b/common/Errors.v
index 6b863a0..78e1199 100644
--- a/common/Errors.v
+++ b/common/Errors.v
@@ -96,30 +96,11 @@ Qed.
 
 (** Assertions *)
 
-Definition assertion (b: bool) : res unit :=
-  if b then OK tt else Error(msg "Assertion failed").
+Definition assertion_failed {A: Type} : res A := Error(msg "Assertion failed").
 
-Remark assertion_inversion:
-  forall b x, assertion b = OK x -> b = true.
-Proof.
-  unfold assertion; intros. destruct b; inv H; auto.
-Qed.
-
-Remark assertion_inversion_1:
-  forall (P Q: Prop) (a: {P}+{Q}) x,
-  assertion (proj_sumbool a) = OK x -> P.
-Proof.
-  intros. exploit assertion_inversion; eauto. 
-  unfold proj_sumbool. destruct a. auto. congruence.
-Qed.
-
-Remark assertion_inversion_2:
-  forall (P Q: Prop) (a: {P}+{Q}) x,
-  assertion (negb(proj_sumbool a)) = OK x -> Q.
-Proof.
-  intros. exploit assertion_inversion; eauto. 
-  unfold proj_sumbool. destruct a; simpl. congruence. auto.
-Qed.
+Notation "'assertion' A ; B" := (if A then B else assertion_failed)
+  (at level 200, A at level 100, B at level 200)
+  : error_monad_scope.
 
 (** This is the familiar monadic map iterator. *)
 
@@ -180,26 +161,19 @@ Ltac monadInv1 H :=
       destruct (bind2_inversion F G H) as [x1 [x2 [EQ1 EQ2]]];
       clear H;
       try (monadInv1 EQ2)))))
-  | (assertion (negb (proj_sumbool ?a)) = OK ?X) =>
-      let A := fresh "A" in (generalize (assertion_inversion_2 _ H); intro A);
-      clear H
-  | (assertion (proj_sumbool ?a) = OK ?X) =>
-      let A := fresh "A" in (generalize (assertion_inversion_1 _ H); intro A);
-      clear H
-  | (assertion ?b = OK ?X) =>
-      let A := fresh "A" in (generalize (assertion_inversion _ H); intro A);
-      clear H
+  | (match ?X with left _ => _ | right _ => assertion_failed end = OK _) =>
+      destruct X; [try (monadInv1 H) | discriminate]
+  | (match (negb ?X) with true => _ | false => assertion_failed end = OK _) =>
+      destruct X as [] eqn:?; [discriminate | try (monadInv1 H)]
+  | (match ?X with true => _ | false => assertion_failed end = OK _) =>
+      destruct X as [] eqn:?; [try (monadInv1 H) | discriminate]
   | (mmap ?F ?L = OK ?M) =>
       generalize (mmap_inversion F L H); intro
   end.
 
 Ltac monadInv H :=
+  monadInv1 H ||
   match type of H with
-  | (OK _ = OK _) => monadInv1 H
-  | (Error _ = OK _) => monadInv1 H
-  | (bind ?F ?G = OK ?X) => monadInv1 H
-  | (bind2 ?F ?G = OK ?X) => monadInv1 H
-  | (assertion _ = OK _) => monadInv1 H
   | (?F _ _ _ _ _ _ _ _ = OK _) => 
       ((progress simpl in H) || unfold F in H); monadInv1 H
   | (?F _ _ _ _ _ _ _ = OK _) => 
diff --git a/common/Events.v b/common/Events.v
index e310bfe..f342799 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -55,6 +55,7 @@ Require Import Globalenvs.
 
 Inductive eventval: Type :=
   | EVint: int -> eventval
+  | EVlong: int64 -> eventval
   | EVfloat: float -> eventval
   | EVptr_global: ident -> int -> eventval.
 
@@ -267,6 +268,8 @@ Variable ge: Genv.t F V.
 Inductive eventval_match: eventval -> typ -> val -> Prop :=
   | ev_match_int: forall i,
       eventval_match (EVint i) Tint (Vint i)
+  | ev_match_long: forall i,
+      eventval_match (EVlong i) Tlong (Vlong i)
   | ev_match_float: forall f,
       eventval_match (EVfloat f) Tfloat (Vfloat f)
   | ev_match_ptr: forall id b ofs,
@@ -327,7 +330,7 @@ Lemma eventval_match_inject:
   forall ev ty v1 v2,
   eventval_match ev ty v1 -> val_inject f v1 v2 -> eventval_match ev ty v2.
 Proof.
-  intros. inv H; inv H0. constructor. constructor.
+  intros. inv H; inv H0; try constructor.
   destruct glob_pres as [A [B C]].
   exploit A; eauto. intro EQ; rewrite H3 in EQ; inv EQ.
   rewrite Int.add_zero. econstructor; eauto. 
@@ -337,7 +340,7 @@ Lemma eventval_match_inject_2:
   forall ev ty v,
   eventval_match ev ty v -> val_inject f v v.
 Proof.
-  induction 1. constructor. constructor.
+  induction 1; auto.
   destruct glob_pres as [A [B C]].
   exploit A; eauto. intro EQ.
   econstructor; eauto. rewrite Int.add_zero; auto.
@@ -379,6 +382,7 @@ Qed.
 Definition eventval_valid (ev: eventval) : Prop :=
   match ev with
   | EVint _ => True
+  | EVlong _ => True
   | EVfloat _ => True
   | EVptr_global id ofs => exists b, Genv.find_symbol ge id = Some b
   end.
@@ -386,6 +390,7 @@ Definition eventval_valid (ev: eventval) : Prop :=
 Definition eventval_type (ev: eventval) : typ :=
   match ev with
   | EVint _ => Tint
+  | EVlong _ => Tlong
   | EVfloat _ => Tfloat
   | EVptr_global id ofs => Tint
   end.
@@ -396,6 +401,7 @@ Lemma eventval_valid_match:
 Proof.
   intros. subst ty. destruct ev; simpl in *.
   exists (Vint i); constructor.
+  exists (Vlong i); constructor.
   exists (Vfloat f0); constructor.
   destruct H as [b A]. exists (Vptr b i0); constructor; auto.
 Qed.
@@ -1693,3 +1699,190 @@ Proof.
   intros. exploit external_call_determ. eexact H. eexact H0. intuition.
 Qed.
 
+(** Late in the back-end, calling conventions for external calls change:
+  arguments and results of type [Tlong] are passed as two integers.
+  We now wrap [external_call] to adapt to this convention. *)
+
+Fixpoint decode_longs (tyl: list typ) (vl: list val) : list val :=
+  match tyl with
+  | nil => nil
+  | Tlong :: tys =>
+      match vl with
+      | v1 :: v2 :: vs => Val.longofwords v1 v2 :: decode_longs tys vs
+      | _ => nil
+      end
+  | ty :: tys =>
+      match vl with
+      | v1 :: vs => v1 :: decode_longs tys vs
+      | _ => nil
+      end
+  end.
+
+Definition encode_long (oty: option typ) (v: val) : list val :=
+  match oty with
+  | Some Tlong => Val.hiword v :: Val.loword v :: nil
+  | _ => v :: nil
+  end.
+
+Definition proj_sig_res' (s: signature) : list typ :=
+  match s.(sig_res) with
+  | Some Tlong => Tint :: Tint :: nil
+  | Some ty => ty :: nil
+  | None => Tint :: nil
+  end.
+
+Inductive external_call'
+      (ef: external_function) (F V: Type) (ge: Genv.t F V)
+      (vargs: list val) (m1: mem) (t: trace) (vres: list val) (m2: mem) : Prop :=
+  external_call'_intro: forall v,
+    external_call ef ge (decode_longs (sig_args (ef_sig ef)) vargs) m1 t v m2 ->
+    vres = encode_long (sig_res (ef_sig ef)) v ->
+    external_call' ef ge vargs m1 t vres m2.
+
+Lemma decode_longs_lessdef:
+  forall tyl vl1 vl2, Val.lessdef_list vl1 vl2 -> Val.lessdef_list (decode_longs tyl vl1) (decode_longs tyl vl2).
+Proof.
+  induction tyl; simpl; intros. 
+  auto.
+  destruct a; inv H; auto. inv H1; auto. constructor; auto. apply Val.longofwords_lessdef; auto. 
+Qed.
+
+Lemma decode_longs_inject:
+  forall f tyl vl1 vl2, val_list_inject f vl1 vl2 -> val_list_inject f (decode_longs tyl vl1) (decode_longs tyl vl2).
+Proof.
+  induction tyl; simpl; intros. 
+  auto.
+  destruct a; inv H; auto. inv H1; auto. constructor; auto. apply val_longofwords_inject; auto. 
+Qed.
+
+Lemma encode_long_lessdef:
+  forall oty v1 v2, Val.lessdef v1 v2 -> Val.lessdef_list (encode_long oty v1) (encode_long oty v2).
+Proof.
+  intros. destruct oty as [[]|]; simpl; auto. 
+  constructor. apply Val.hiword_lessdef; auto. constructor. apply Val.loword_lessdef; auto. auto.
+Qed.
+
+Lemma encode_long_inject:
+  forall f oty v1 v2, val_inject f v1 v2 -> val_list_inject f (encode_long oty v1) (encode_long oty v2).
+Proof.
+  intros. destruct oty as [[]|]; simpl; auto. 
+  constructor. apply val_hiword_inject; auto. constructor. apply val_loword_inject; auto. auto.
+Qed.
+
+Lemma encode_long_has_type:
+  forall v sg,
+  Val.has_type v (proj_sig_res sg) ->
+  Val.has_type_list (encode_long (sig_res sg) v) (proj_sig_res' sg).
+Proof.
+  unfold proj_sig_res, proj_sig_res', encode_long; intros.
+  destruct (sig_res sg) as [[] | ]; simpl; auto.
+  destruct v; simpl; auto.
+Qed.
+
+Lemma external_call_well_typed':
+  forall ef (F V : Type) (ge : Genv.t F V) vargs m1 t vres m2,
+  external_call' ef ge vargs m1 t vres m2 ->
+  Val.has_type_list vres (proj_sig_res' (ef_sig ef)).
+Proof.
+  intros. inv H. apply encode_long_has_type. 
+  eapply external_call_well_typed; eauto. 
+Qed.
+
+Lemma external_call_symbols_preserved':
+  forall ef F1 F2 V (ge1: Genv.t F1 V) (ge2: Genv.t F2 V) vargs m1 t vres m2,
+  external_call' ef ge1 vargs m1 t vres m2 ->
+  (forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id) ->
+  (forall b, Genv.find_var_info ge2 b = Genv.find_var_info ge1 b) ->
+  external_call' ef ge2 vargs m1 t vres m2.
+Proof.
+  intros. inv H. exists v; auto. eapply external_call_symbols_preserved; eauto.
+Qed.
+
+Lemma external_call_valid_block':
+  forall ef (F V : Type) (ge : Genv.t F V) vargs m1 t vres m2 b,
+  external_call' ef ge vargs m1 t vres m2 ->
+  Mem.valid_block m1 b -> Mem.valid_block m2 b.
+Proof.
+  intros. inv H. eapply external_call_valid_block; eauto.
+Qed.
+
+Lemma external_call_mem_extends':
+  forall ef (F V : Type) (ge : Genv.t F V) vargs m1 t vres m2 m1' vargs',
+  external_call' ef ge vargs m1 t vres m2 ->
+  Mem.extends m1 m1' ->
+  Val.lessdef_list vargs vargs' ->
+  exists vres' m2',
+     external_call' ef ge vargs' m1' t vres' m2'
+  /\ Val.lessdef_list vres vres'
+  /\ Mem.extends m2 m2'
+  /\ mem_unchanged_on (loc_out_of_bounds m1) m1' m2'.
+Proof.
+  intros. inv H. 
+  exploit external_call_mem_extends; eauto.
+  eapply decode_longs_lessdef; eauto. 
+  intros (v' & m2' & A & B & C & D).
+  exists (encode_long (sig_res (ef_sig ef)) v'); exists m2'; intuition.
+  econstructor; eauto.
+  eapply encode_long_lessdef; eauto.
+Qed.
+
+Lemma external_call_mem_inject':
+  forall ef F V (ge: Genv.t F V) vargs m1 t vres m2 f m1' vargs',
+  meminj_preserves_globals ge f ->
+  external_call' ef ge vargs m1 t vres m2 ->
+  Mem.inject f m1 m1' ->
+  val_list_inject f vargs vargs' ->
+  exists f' vres' m2',
+     external_call' ef ge vargs' m1' t vres' m2'
+  /\ val_list_inject f' vres vres'
+  /\ Mem.inject f' m2 m2'
+  /\ mem_unchanged_on (loc_unmapped f) m1 m2
+  /\ mem_unchanged_on (loc_out_of_reach f m1) m1' m2'
+  /\ inject_incr f f'
+  /\ inject_separated f f' m1 m1'.
+Proof.
+  intros. inv H0. 
+  exploit external_call_mem_inject; eauto.
+  eapply decode_longs_inject; eauto.
+  intros (f' & v' & m2' & A & B & C & D & E & P & Q).
+  exists f'; exists (encode_long (sig_res (ef_sig ef)) v'); exists m2'; intuition.
+  econstructor; eauto.
+  apply encode_long_inject; auto.
+Qed.
+
+Lemma external_call_determ':
+  forall ef (F V : Type) (ge : Genv.t F V) vargs m t1 vres1 m1 t2 vres2 m2,
+  external_call' ef ge vargs m t1 vres1 m1 ->
+  external_call' ef ge vargs m t2 vres2 m2 ->
+  match_traces ge t1 t2 /\ (t1 = t2 -> vres1 = vres2 /\ m1 = m2).
+Proof.
+  intros. inv H; inv H0. exploit external_call_determ. eexact H1. eexact H. 
+  intros [A B]. split. auto. intros. destruct B as [C D]; auto. subst. auto. 
+Qed.
+
+Lemma external_call_match_traces':
+  forall ef (F V : Type) (ge : Genv.t F V) vargs m t1 vres1 m1 t2 vres2 m2,
+  external_call' ef ge vargs m t1 vres1 m1 ->
+  external_call' ef ge vargs m t2 vres2 m2 ->
+  match_traces ge t1 t2.
+Proof.
+  intros. inv H; inv H0. eapply external_call_match_traces; eauto.
+Qed.
+
+Lemma external_call_deterministic':
+  forall ef (F V : Type) (ge : Genv.t F V) vargs m t vres1 m1 vres2 m2,
+  external_call' ef ge vargs m t vres1 m1 ->
+  external_call' ef ge vargs m t vres2 m2 ->
+  vres1 = vres2 /\ m1 = m2.
+Proof.
+  intros. inv H; inv H0. 
+  exploit external_call_deterministic. eexact H1. eexact H. intros [A B].
+  split; congruence.
+Qed.
+
+
+
+
+
+
+
diff --git a/common/Globalenvs.v b/common/Globalenvs.v
index 3d9f499..a082819 100644
--- a/common/Globalenvs.v
+++ b/common/Globalenvs.v
@@ -491,6 +491,7 @@ Definition init_data_size (i: init_data) : Z :=
   | Init_int8 _ => 1
   | Init_int16 _ => 2
   | Init_int32 _ => 4
+  | Init_int64 _ => 8
   | Init_float32 _ => 4
   | Init_float64 _ => 8
   | Init_addrof _ _ => 4
@@ -508,6 +509,7 @@ Definition store_init_data (m: mem) (b: block) (p: Z) (id: init_data) : option m
   | Init_int8 n => Mem.store Mint8unsigned m b p (Vint n)
   | Init_int16 n => Mem.store Mint16unsigned m b p (Vint n)
   | Init_int32 n => Mem.store Mint32 m b p (Vint n)
+  | Init_int64 n => Mem.store Mint64 m b p (Vlong n)
   | Init_float32 n => Mem.store Mfloat32 m b p (Vfloat n)
   | Init_float64 n => Mem.store Mfloat64 m b p (Vfloat n)
   | Init_addrof symb ofs =>
@@ -761,6 +763,9 @@ Fixpoint load_store_init_data (m: mem) (b: block) (p: Z) (il: list init_data) {s
   | Init_int32 n :: il' =>
       Mem.load Mint32 m b p = Some(Vint n)
       /\ load_store_init_data m b (p + 4) il'
+  | Init_int64 n :: il' =>
+      Mem.load Mint64 m b p = Some(Vlong n)
+      /\ load_store_init_data m b (p + 8) il'
   | Init_float32 n :: il' =>
       Mem.load Mfloat32 m b p = Some(Vfloat(Float.singleoffloat n))
       /\ load_store_init_data m b (p + 4) il'
@@ -795,6 +800,7 @@ Proof.
   eapply (A Mint8unsigned (Vint i)); eauto.
   eapply (A Mint16unsigned (Vint i)); eauto.
   eapply (A Mint32 (Vint i)); eauto.
+  eapply (A Mint64 (Vlong i)); eauto.
   eapply (A Mfloat32 (Vfloat f)); eauto.
   eapply (A Mfloat64 (Vfloat f)); eauto.
   destruct (find_symbol ge i); try congruence. exists b0; split; auto. 
diff --git a/common/Memdata.v b/common/Memdata.v
index 3de5f39..c62ba99 100644
--- a/common/Memdata.v
+++ b/common/Memdata.v
@@ -35,6 +35,7 @@ Definition size_chunk (chunk: memory_chunk) : Z :=
   | Mint16signed => 2
   | Mint16unsigned => 2
   | Mint32 => 4
+  | Mint64 => 8
   | Mfloat32 => 4
   | Mfloat64 => 8
   | Mfloat64al32 => 8
@@ -82,6 +83,7 @@ Definition align_chunk (chunk: memory_chunk) : Z :=
   | Mint16signed => 2
   | Mint16unsigned => 2
   | Mint32 => 4
+  | Mint64 => 8
   | Mfloat32 => 4
   | Mfloat64 => 8
   | Mfloat64al32 => 4
@@ -96,7 +98,7 @@ Qed.
 Lemma align_size_chunk_divides:
   forall chunk, (align_chunk chunk | size_chunk chunk).
 Proof.
-  intros. destruct chunk; simpl; try apply Zdivide_refl. exists 2; auto. 
+  intros. destruct chunk; simpl; try apply Zdivide_refl; exists 2; auto. 
 Qed.
 
 Lemma align_le_divides:
@@ -340,6 +342,7 @@ Definition encode_val (chunk: memory_chunk) (v: val) : list memval :=
   | Vint n, (Mint16signed | Mint16unsigned) => inj_bytes (encode_int 2%nat (Int.unsigned n))
   | Vint n, Mint32 => inj_bytes (encode_int 4%nat (Int.unsigned n))
   | Vptr b ofs, Mint32 => inj_pointer 4%nat b ofs
+  | Vlong n, Mint64 => inj_bytes (encode_int 8%nat (Int64.unsigned n))
   | Vfloat n, Mfloat32 => inj_bytes (encode_int 4%nat (Int.unsigned (Float.bits_of_single n)))
   | Vfloat n, (Mfloat64 | Mfloat64al32) => inj_bytes (encode_int 8%nat (Int64.unsigned (Float.bits_of_double n)))
   | _, _ => list_repeat (size_chunk_nat chunk) Undef
@@ -354,6 +357,7 @@ Definition decode_val (chunk: memory_chunk) (vl: list memval) : val :=
       | Mint16signed => Vint(Int.sign_ext 16 (Int.repr (decode_int bl)))
       | Mint16unsigned => Vint(Int.zero_ext 16 (Int.repr (decode_int bl)))
       | Mint32 => Vint(Int.repr(decode_int bl))
+      | Mint64 => Vlong(Int64.repr(decode_int bl))
       | Mfloat32 => Vfloat(Float.single_of_bits (Int.repr (decode_int bl)))
       | Mfloat64 | Mfloat64al32 => Vfloat(Float.double_of_bits (Int64.repr (decode_int bl)))
       end
@@ -394,14 +398,19 @@ Definition decode_encode_val (v1: val) (chunk1 chunk2: memory_chunk) (v2: val) :
   | Vint n, Mint16unsigned, Mint16unsigned => v2 = Vint(Int.zero_ext 16 n)
   | Vint n, Mint32, Mint32 => v2 = Vint n
   | Vint n, Mint32, Mfloat32 => v2 = Vfloat(Float.single_of_bits n)
-  | Vint n, (Mfloat32 | Mfloat64 | Mfloat64al32), _ => v2 = Vundef
+  | Vint n, (Mint64 | Mfloat32 | Mfloat64 | Mfloat64al32), _ => v2 = Vundef
   | Vint n, _, _ => True (**r nothing meaningful to say about v2 *)
   | Vptr b ofs, Mint32, Mint32 => v2 = Vptr b ofs
   | Vptr b ofs, _, _ => v2 = Vundef
+  | Vlong n, Mint64, Mint64 => v2 = Vlong n
+  | Vlong n, Mint64, (Mfloat64 | Mfloat64al32) => v2 = Vfloat(Float.double_of_bits n)
+  | Vlong n, (Mint8signed|Mint8unsigned|Mint16signed|Mint16unsigned|Mint32|Mfloat32|Mfloat64|Mfloat64al32), _ => v2 = Vundef
+  | Vlong n, _, _ => True (**r nothing meaningful to say about v2 *)
   | Vfloat f, Mfloat32, Mfloat32 => v2 = Vfloat(Float.singleoffloat f)
   | Vfloat f, Mfloat32, Mint32 => v2 = Vint(Float.bits_of_single f)
   | Vfloat f, (Mfloat64 | Mfloat64al32), (Mfloat64 | Mfloat64al32) => v2 = Vfloat f
-  | Vfloat f, (Mint8signed|Mint8unsigned|Mint16signed|Mint16unsigned|Mint32), _ => v2 = Vundef
+  | Vfloat f, (Mint8signed|Mint8unsigned|Mint16signed|Mint16unsigned|Mint32|Mint64), _ => v2 = Vundef
+  | Vfloat f, (Mfloat64 | Mfloat64al32), Mint64 => v2 = Vlong(Float.bits_of_double f)
   | Vfloat f, _, _ => True   (* nothing interesting to say about v2 *)
   end.
 
@@ -419,7 +428,6 @@ Opaque inj_pointer.
   intros.
   destruct v; destruct chunk1; simpl; try (apply decode_val_undef);
   destruct chunk2; unfold decode_val; auto; try (rewrite proj_inj_bytes).
-  (* int-int *)
   rewrite decode_encode_int_1. decEq. apply Int.sign_ext_zero_ext. omega.
   rewrite decode_encode_int_1. decEq. apply Int.zero_ext_idem. omega.
   rewrite decode_encode_int_1. decEq. apply Int.sign_ext_zero_ext. omega.
@@ -430,10 +438,15 @@ Opaque inj_pointer.
   rewrite decode_encode_int_2. decEq. apply Int.zero_ext_idem. omega.
   rewrite decode_encode_int_4. auto.
   rewrite decode_encode_int_4. auto.
+  rewrite decode_encode_int_8. auto.
+  rewrite decode_encode_int_8. auto.
+  rewrite decode_encode_int_8. auto.
   rewrite decode_encode_int_4. auto.
-  rewrite decode_encode_int_4. decEq. apply Float.single_of_bits_of_single. 
+  rewrite decode_encode_int_4. decEq. apply Float.single_of_bits_of_single.
+  rewrite decode_encode_int_8. auto.
   rewrite decode_encode_int_8. decEq. apply Float.double_of_bits_of_double.
   rewrite decode_encode_int_8. decEq. apply Float.double_of_bits_of_double.
+  rewrite decode_encode_int_8. auto.
   rewrite decode_encode_int_8. decEq. apply Float.double_of_bits_of_double.
   rewrite decode_encode_int_8. decEq. apply Float.double_of_bits_of_double.
   change (proj_bytes (inj_pointer 4 b i)) with (@None (list byte)). simpl. 
@@ -815,6 +828,7 @@ Proof.
   intros. inv H; simpl.
   destruct chunk; apply inj_bytes_inject || apply repeat_Undef_inject_self.
   destruct chunk; apply inj_bytes_inject || apply repeat_Undef_inject_self.
+  destruct chunk; apply inj_bytes_inject || apply repeat_Undef_inject_self.
   destruct chunk; try (apply repeat_Undef_inject_self). 
   repeat econstructor; eauto. 
   replace (size_chunk_nat chunk) with (length (encode_val chunk v2)).
@@ -845,3 +859,143 @@ Proof.
   constructor.
 Qed. 
 
+(** * Breaking 64-bit memory accesses into two 32-bit accesses *)
+
+Lemma int_of_bytes_append:
+  forall l2 l1, 
+  int_of_bytes (l1 ++ l2) = int_of_bytes l1 + int_of_bytes l2 * two_p (Z_of_nat (length l1) * 8).
+Proof.
+  induction l1; simpl int_of_bytes; intros.
+  simpl. ring.
+  simpl length. rewrite inj_S. 
+  replace (Z.succ (Z.of_nat (length l1)) * 8) with (Z_of_nat (length l1) * 8 + 8) by omega.
+  rewrite two_p_is_exp. change (two_p 8) with 256. rewrite IHl1. ring.
+  omega. omega.
+Qed.
+
+Lemma int_of_bytes_range:
+  forall l, 0 <= int_of_bytes l < two_p (Z_of_nat (length l) * 8).
+Proof.
+  induction l; intros. 
+  simpl. omega.
+  simpl length. rewrite inj_S. 
+  replace (Z.succ (Z.of_nat (length l)) * 8) with (Z.of_nat (length l) * 8 + 8) by omega.
+  rewrite two_p_is_exp. change (two_p 8) with 256. 
+  simpl int_of_bytes. generalize (Byte.unsigned_range a). 
+  change Byte.modulus with 256. omega. 
+  omega. omega. 
+Qed.
+
+Lemma length_proj_bytes:
+  forall l b, proj_bytes l = Some b -> length b = length l.
+Proof.
+  induction l; simpl; intros. 
+  inv H; auto.
+  destruct a; try discriminate. 
+  destruct (proj_bytes l) eqn:E; inv H. 
+  simpl. f_equal. auto.
+Qed.
+
+Lemma proj_bytes_append:
+  forall l2 l1,
+  proj_bytes (l1 ++ l2) =
+  match proj_bytes l1, proj_bytes l2 with
+  | Some b1, Some b2 => Some (b1 ++ b2)
+  | _, _ => None
+  end.
+Proof.
+  induction l1; simpl.
+  destruct (proj_bytes l2); auto.
+  destruct a; auto. rewrite IHl1. 
+  destruct (proj_bytes l1); auto. destruct (proj_bytes l2); auto. 
+Qed.
+
+Lemma decode_val_int64:
+  forall l1 l2,
+  length l1 = 4%nat -> length l2 = 4%nat ->
+  decode_val Mint64 (l1 ++ l2) =
+  Val.longofwords (decode_val Mint32 (if big_endian then l1 else l2))
+                  (decode_val Mint32 (if big_endian then l2 else l1)).
+Proof.
+  intros. unfold decode_val.
+  assert (PP: forall vl, match proj_pointer vl with Vundef => True | Vptr _ _ => True | _ => False end).
+    intros. unfold proj_pointer. destruct vl; auto. destruct m; auto. 
+    destruct (check_pointer 4 b i (Pointer b i n :: vl)); auto. 
+  assert (PP1: forall vl v2, Val.longofwords (proj_pointer vl) v2 = Vundef).
+    intros. generalize (PP vl). destruct (proj_pointer vl); reflexivity || contradiction.
+  assert (PP2: forall v1 vl, Val.longofwords v1 (proj_pointer vl) = Vundef).
+    intros. destruct v1; simpl; auto. 
+    generalize (PP vl). destruct (proj_pointer vl); reflexivity || contradiction.
+  rewrite proj_bytes_append. 
+  destruct (proj_bytes l1) as [b1|] eqn:B1; destruct (proj_bytes l2) as [b2|] eqn:B2.
+- exploit length_proj_bytes. eexact B1. rewrite H; intro L1.
+  exploit length_proj_bytes. eexact B2. rewrite H0; intro L2.
+  assert (UR: forall l, length l = 4%nat -> Int.unsigned (Int.repr (int_of_bytes l)) = int_of_bytes l).
+    intros. apply Int.unsigned_repr. 
+    generalize (int_of_bytes_range l). rewrite H1. 
+    change (two_p (Z.of_nat 4 * 8)) with (Int.max_unsigned + 1). 
+    omega.
+  unfold decode_int, rev_if_be. destruct big_endian; rewrite B1; rewrite B2.
+  + rewrite <- (rev_length b1) in L1. 
+    rewrite <- (rev_length b2) in L2.
+    rewrite rev_app_distr.
+    set (b1' := rev b1) in *; set (b2' := rev b2) in *.
+    unfold Val.longofwords. f_equal. rewrite Int64.ofwords_add. f_equal.
+    rewrite !UR by auto. rewrite int_of_bytes_append. 
+    rewrite L2. change (Z.of_nat 4 * 8) with 32. ring.
+  + unfold Val.longofwords. f_equal. rewrite Int64.ofwords_add. f_equal.
+    rewrite !UR by auto. rewrite int_of_bytes_append. 
+    rewrite L1. change (Z.of_nat 4 * 8) with 32. ring.
+- destruct big_endian; rewrite B1; rewrite B2; auto.
+- destruct big_endian; rewrite B1; rewrite B2; auto.
+- destruct big_endian; rewrite B1; rewrite B2; auto.
+Qed.
+
+Lemma bytes_of_int_append:
+  forall n2 x2 n1 x1,
+  0 <= x1 < two_p (Z_of_nat n1 * 8) ->
+  bytes_of_int (n1 + n2) (x1 + x2 * two_p (Z_of_nat n1 * 8)) =
+  bytes_of_int n1 x1 ++ bytes_of_int n2 x2.
+Proof.
+  induction n1; intros.
+- simpl in *. f_equal. omega. 
+- assert (E: two_p (Z.of_nat (S n1) * 8) = two_p (Z.of_nat n1 * 8) * 256).
+  {
+    rewrite inj_S. change 256 with (two_p 8). rewrite <- two_p_is_exp. 
+    f_equal. omega. omega. omega. 
+  }
+  rewrite E in *. simpl. f_equal.
+  apply Byte.eqm_samerepr. exists (x2 * two_p (Z.of_nat n1 * 8)). 
+  change Byte.modulus with 256. ring.
+  rewrite Zmult_assoc. rewrite Z_div_plus. apply IHn1.
+  apply Zdiv_interval_1. omega. apply two_p_gt_ZERO; omega. omega. 
+  assumption. omega.
+Qed.
+
+Lemma bytes_of_int64:
+  forall i,
+  bytes_of_int 8 (Int64.unsigned i) =
+  bytes_of_int 4 (Int.unsigned (Int64.loword i)) ++ bytes_of_int 4 (Int.unsigned (Int64.hiword i)).
+Proof.
+  intros. transitivity (bytes_of_int (4 + 4) (Int64.unsigned (Int64.ofwords (Int64.hiword i) (Int64.loword i)))).
+  f_equal. f_equal. rewrite Int64.ofwords_recompose. auto.
+  rewrite Int64.ofwords_add'.
+  change 32 with (Z_of_nat 4 * 8). 
+  rewrite Zplus_comm. apply bytes_of_int_append. apply Int.unsigned_range. 
+Qed.
+
+Lemma encode_val_int64:
+  forall v,
+  encode_val Mint64 v =
+     encode_val Mint32 (if big_endian then Val.hiword v else Val.loword v)
+  ++ encode_val Mint32 (if big_endian then Val.loword v else Val.hiword v).
+Proof.
+  intros. destruct v; destruct big_endian eqn:BI; try reflexivity;
+  unfold Val.loword, Val.hiword, encode_val.
+  unfold inj_bytes. rewrite <- map_app. f_equal. 
+  unfold encode_int, rev_if_be. rewrite BI. rewrite <- rev_app_distr. f_equal.
+  apply bytes_of_int64. 
+  unfold inj_bytes. rewrite <- map_app. f_equal. 
+  unfold encode_int, rev_if_be. rewrite BI.
+  apply bytes_of_int64.
+Qed.
diff --git a/common/Memory.v b/common/Memory.v
index 12a0f45..54d50f7 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -862,6 +862,60 @@ Proof.
   rewrite inj_S. omega.
 Qed.
 
+Theorem load_int64_split:
+  forall m b ofs v,
+  load Mint64 m b ofs = Some v ->
+  exists v1 v2,
+     load Mint32 m b ofs = Some (if big_endian then v1 else v2)
+  /\ load Mint32 m b (ofs + 4) = Some (if big_endian then v2 else v1)
+  /\ v = Val.longofwords v1 v2.
+Proof.
+  intros. 
+  exploit load_valid_access; eauto. intros [A B]. simpl in *.
+  exploit load_loadbytes. eexact H. simpl. intros [bytes [LB EQ]].
+  change 8 with (4 + 4) in LB. 
+  exploit loadbytes_split. eexact LB. omega. omega. 
+  intros (bytes1 & bytes2 & LB1 & LB2 & APP).
+  change 4 with (size_chunk Mint32) in LB1.
+  exploit loadbytes_load. eexact LB1.
+  simpl. apply Zdivides_trans with 8; auto. exists 2; auto.
+  intros L1.
+  change 4 with (size_chunk Mint32) in LB2.
+  exploit loadbytes_load. eexact LB2.
+  simpl. apply Zdivide_plus_r. apply Zdivides_trans with 8; auto. exists 2; auto. exists 1; auto.
+  intros L2.
+  exists (decode_val Mint32 (if big_endian then bytes1 else bytes2));
+  exists (decode_val Mint32 (if big_endian then bytes2 else bytes1)).
+  split. destruct big_endian; auto.
+  split. destruct big_endian; auto.
+  rewrite EQ. rewrite APP. apply decode_val_int64.
+  erewrite loadbytes_length; eauto. reflexivity. 
+  erewrite loadbytes_length; eauto. reflexivity. 
+Qed.
+
+Theorem loadv_int64_split:
+  forall m a v,
+  loadv Mint64 m a = Some v ->
+  exists v1 v2,
+     loadv Mint32 m a = Some (if big_endian then v1 else v2)
+  /\ loadv  Mint32 m (Val.add a (Vint (Int.repr 4))) = Some (if big_endian then v2 else v1)
+  /\ v = Val.longofwords v1 v2.
+Proof.
+  intros. destruct a; simpl in H; try discriminate.
+  exploit load_int64_split; eauto. intros (v1 & v2 & L1 & L2 & EQ).
+  assert (NV: Int.unsigned (Int.add i (Int.repr 4)) = Int.unsigned i + 4).
+    rewrite Int.add_unsigned. apply Int.unsigned_repr.
+    exploit load_valid_access. eexact H. intros [P Q]. simpl in Q.
+    exploit (Zdivide_interval (Int.unsigned i) Int.modulus 8).
+    omega. apply Int.unsigned_range. auto. exists (two_p (32-3)); reflexivity. 
+    unfold Int.max_unsigned. omega.
+  exists v1; exists v2.
+Opaque Int.repr.
+  split. auto.
+  split. simpl. rewrite NV. auto. 
+  auto.
+Qed.
+
 (** ** Properties related to [store] *)
 
 Theorem valid_access_store:
@@ -1581,6 +1635,44 @@ Proof.
   exists m1; split; auto. 
 Qed.
 
+Theorem store_int64_split:
+  forall m b ofs v m',
+  store Mint64 m b ofs v = Some m' ->
+  exists m1,
+     store Mint32 m b ofs (if big_endian then Val.hiword v else Val.loword v) = Some m1
+  /\ store Mint32 m1 b (ofs + 4) (if big_endian then Val.loword v else Val.hiword v) = Some m'.
+Proof.
+  intros. 
+  exploit store_valid_access_3; eauto. intros [A B]. simpl in *.
+  exploit store_storebytes. eexact H. intros SB.
+  rewrite encode_val_int64 in SB. 
+  exploit storebytes_split. eexact SB. intros [m1 [SB1 SB2]]. 
+  rewrite encode_val_length in SB2. simpl in SB2. 
+  exists m1; split. 
+  apply storebytes_store. exact SB1.
+  simpl. apply Zdivides_trans with 8; auto. exists 2; auto.
+  apply storebytes_store. exact SB2. 
+  simpl. apply Zdivide_plus_r. apply Zdivides_trans with 8; auto. exists 2; auto. exists 1; auto.
+Qed.
+
+Theorem storev_int64_split:
+  forall m a v m',
+  storev Mint64 m a v = Some m' ->
+  exists m1,
+     storev Mint32 m a (if big_endian then Val.hiword v else Val.loword v) = Some m1
+  /\ storev Mint32 m1 (Val.add a (Vint (Int.repr 4))) (if big_endian then Val.loword v else Val.hiword v) = Some m'.
+Proof.
+  intros. destruct a; simpl in H; try discriminate.
+  exploit store_int64_split; eauto. intros [m1 [A B]].
+  exists m1; split.
+  exact A.
+  unfold storev, Val.add. rewrite Int.add_unsigned. rewrite Int.unsigned_repr. exact B.
+  exploit store_valid_access_3. eexact H. intros [P Q]. simpl in Q.
+  exploit (Zdivide_interval (Int.unsigned i) Int.modulus 8).
+    omega. apply Int.unsigned_range. auto. exists (two_p (32-3)); reflexivity. 
+  change (Int.unsigned (Int.repr 4)) with 4. unfold Int.max_unsigned. omega. 
+Qed.
+
 (** ** Properties related to [alloc]. *)
 
 Section ALLOC.
diff --git a/common/PrintAST.ml b/common/PrintAST.ml
index 7f2ed3f..c18b09d 100644
--- a/common/PrintAST.ml
+++ b/common/PrintAST.ml
@@ -16,7 +16,7 @@ open Printf
 open Camlcoq
 open AST
 
-let name_of_type = function Tint -> "int" | Tfloat -> "float"
+let name_of_type = function Tint -> "int" | Tfloat -> "float" | Tlong -> "long"
 
 let name_of_chunk = function
   | Mint8signed -> "int8signed"
@@ -24,6 +24,7 @@ let name_of_chunk = function
   | Mint16signed -> "int16signed"
   | Mint16unsigned -> "int16unsigned"
   | Mint32 -> "int32"
+  | Mint64 -> "int64"
   | Mfloat32 -> "float32"
   | Mfloat64 -> "float64"
   | Mfloat64al32 -> "float64al32"
diff --git a/common/Values.v b/common/Values.v
index f629628..f917e0b 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -36,6 +36,7 @@ Definition eq_block := zeq.
 Inductive val: Type :=
   | Vundef: val
   | Vint: int -> val
+  | Vlong: int64 -> val
   | Vfloat: float -> val
   | Vptr: block -> int -> val.
 
@@ -58,6 +59,7 @@ Definition has_type (v: val) (t: typ) : Prop :=
   match v, t with
   | Vundef, _ => True
   | Vint _, Tint => True
+  | Vlong _, Tlong => True
   | Vfloat _, Tfloat => True
   | Vptr _ _, Tint => True
   | _, _ => False
@@ -70,6 +72,12 @@ Fixpoint has_type_list (vl: list val) (tl: list typ) {struct vl} : Prop :=
   | _, _ => False
   end.
 
+Definition has_opttype (v: val) (ot: option typ) : Prop :=
+  match ot with
+  | None => v = Vundef
+  | Some t => has_type v t
+  end.
+
 (** Truth values.  Pointers and non-zero integers are treated as [True].
   The integer 0 (also used to represent the null pointer) is [False].
   [Vundef] and floats are neither true nor false. *)
@@ -127,12 +135,6 @@ Definition floatofintu (v: val) : option val :=
   | _ => None
   end.
 
-Definition floatofwords (v1 v2: val) : val :=
-  match v1, v2 with
-  | Vint n1, Vint n2 => Vfloat (Float.from_words n1 n2)
-  | _, _ => Vundef
-  end.
-
 Definition negint (v: val) : val :=
   match v with
   | Vint n => Vint (Int.neg n)
@@ -344,6 +346,183 @@ Definition divf (v1 v2: val): val :=
   | _, _ => Vundef
   end.
 
+Definition floatofwords (v1 v2: val) : val :=
+  match v1, v2 with
+  | Vint n1, Vint n2 => Vfloat (Float.from_words n1 n2)
+  | _, _ => Vundef
+  end.
+
+(** Operations on 64-bit integers *)
+
+Definition longofwords (v1 v2: val) : val :=
+  match v1, v2 with
+  | Vint n1, Vint n2 => Vlong (Int64.ofwords n1 n2)
+  | _, _ => Vundef
+  end.
+
+Definition loword (v: val) : val :=
+  match v with
+  | Vlong n  => Vint (Int64.loword n)
+  | _ => Vundef
+  end.
+
+Definition hiword (v: val) : val :=
+  match v with
+  | Vlong n  => Vint (Int64.hiword n)
+  | _ => Vundef
+  end.
+
+Definition negl (v: val) : val :=
+  match v with
+  | Vlong n => Vlong (Int64.neg n)
+  | _ => Vundef
+  end.
+
+Definition notl (v: val) : val :=
+  match v with
+  | Vlong n => Vlong (Int64.not n)
+  | _ => Vundef
+  end.
+
+Definition longofint (v: val) : val :=
+  match v with
+  | Vint n => Vlong (Int64.repr (Int.signed n))
+  | _ => Vundef
+  end.
+
+Definition longofintu (v: val) : val :=
+  match v with
+  | Vint n => Vlong (Int64.repr (Int.unsigned n))
+  | _ => Vundef
+  end.
+
+Definition longoffloat (v: val) : option val :=
+  match v with
+  | Vfloat f => option_map Vlong (Float.longoffloat f)
+  | _ => None
+  end.
+
+Definition longuoffloat (v: val) : option val :=
+  match v with
+  | Vfloat f => option_map Vlong (Float.longuoffloat f)
+  | _ => None
+  end.
+
+Definition floatoflong (v: val) : option val :=
+  match v with
+  | Vlong n => Some (Vfloat (Float.floatoflong n))
+  | _ => None
+  end.
+
+Definition floatoflongu (v: val) : option val :=
+  match v with
+  | Vlong n => Some (Vfloat (Float.floatoflongu n))
+  | _ => None
+  end.
+
+Definition addl (v1 v2: val): val :=
+  match v1, v2 with
+  | Vlong n1, Vlong n2 => Vlong(Int64.add n1 n2)
+  | _, _ => Vundef
+  end.
+
+Definition subl (v1 v2: val): val :=
+  match v1, v2 with
+  | Vlong n1, Vlong n2 => Vlong(Int64.sub n1 n2)
+  | _, _ => Vundef
+  end.
+
+Definition mull (v1 v2: val): val :=
+  match v1, v2 with
+  | Vlong n1, Vlong n2 => Vlong(Int64.mul n1 n2)
+  | _, _ => Vundef
+  end.
+
+Definition mull' (v1 v2: val): val :=
+  match v1, v2 with
+  | Vint n1, Vint n2 => Vlong(Int64.mul' n1 n2)
+  | _, _ => Vundef
+  end.
+
+Definition divls (v1 v2: val): option val :=
+  match v1, v2 with
+  | Vlong n1, Vlong n2 =>
+      if Int64.eq n2 Int64.zero
+      || Int64.eq n1 (Int64.repr Int64.min_signed) && Int64.eq n2 Int64.mone
+      then None
+      else Some(Vlong(Int64.divs n1 n2))
+  | _, _ => None
+  end.
+
+Definition modls (v1 v2: val): option val :=
+  match v1, v2 with
+  | Vlong n1, Vlong n2 =>
+      if Int64.eq n2 Int64.zero
+      || Int64.eq n1 (Int64.repr Int64.min_signed) && Int64.eq n2 Int64.mone
+      then None
+      else Some(Vlong(Int64.mods n1 n2))
+  | _, _ => None
+  end.
+
+Definition divlu (v1 v2: val): option val :=
+  match v1, v2 with
+  | Vlong n1, Vlong n2 =>
+      if Int64.eq n2 Int64.zero then None else Some(Vlong(Int64.divu n1 n2))
+  | _, _ => None
+  end.
+
+Definition modlu (v1 v2: val): option val :=
+  match v1, v2 with
+  | Vlong n1, Vlong n2 =>
+      if Int64.eq n2 Int64.zero then None else Some(Vlong(Int64.modu n1 n2))
+  | _, _ => None
+  end.
+
+Definition andl (v1 v2: val): val :=
+  match v1, v2 with
+  | Vlong n1, Vlong n2 => Vlong(Int64.and n1 n2)
+  | _, _ => Vundef
+  end.
+
+Definition orl (v1 v2: val): val :=
+  match v1, v2 with
+  | Vlong n1, Vlong n2 => Vlong(Int64.or n1 n2)
+  | _, _ => Vundef
+  end.
+
+Definition xorl (v1 v2: val): val :=
+  match v1, v2 with
+  | Vlong n1, Vlong n2 => Vlong(Int64.xor n1 n2)
+  | _, _ => Vundef
+  end.
+
+Definition shll (v1 v2: val): val :=
+  match v1, v2 with
+  | Vlong n1, Vint n2 =>
+     if Int.ltu n2 Int64.iwordsize'
+     then Vlong(Int64.shl' n1 n2)
+     else Vundef
+  | _, _ => Vundef
+  end.
+
+Definition shrl (v1 v2: val): val :=
+  match v1, v2 with
+  | Vlong n1, Vint n2 =>
+     if Int.ltu n2 Int64.iwordsize'
+     then Vlong(Int64.shr' n1 n2)
+     else Vundef
+  | _, _ => Vundef
+  end.
+
+Definition shrlu (v1 v2: val): val :=
+  match v1, v2 with
+  | Vlong n1, Vint n2 =>
+     if Int.ltu n2 Int64.iwordsize'
+     then Vlong(Int64.shru' n1 n2)
+     else Vundef
+  | _, _ => Vundef
+  end.
+
 (** Comparisons *)
 
 Section COMPARISONS.
@@ -392,6 +571,18 @@ Definition cmpf_bool (c: comparison) (v1 v2: val): option bool :=
   | _, _ => None
   end.
 
+Definition cmpl_bool (c: comparison) (v1 v2: val): option bool :=
+  match v1, v2 with
+  | Vlong n1, Vlong n2 => Some (Int64.cmp c n1 n2)
+  | _, _ => None
+  end.
+
+Definition cmplu_bool (c: comparison) (v1 v2: val): option bool :=
+  match v1, v2 with
+  | Vlong n1, Vlong n2 => Some (Int64.cmpu c n1 n2)
+  | _, _ => None
+  end.
+
 Definition of_optbool (ob: option bool): val :=
   match ob with Some true => Vtrue | Some false => Vfalse | None => Vundef end.
 
@@ -404,6 +595,12 @@ Definition cmpu (c: comparison) (v1 v2: val): val :=
 Definition cmpf (c: comparison) (v1 v2: val): val :=
   of_optbool (cmpf_bool c v1 v2).
 
+Definition cmpl (c: comparison) (v1 v2: val): val :=
+  of_optbool (cmpl_bool c v1 v2).
+
+Definition cmplu (c: comparison) (v1 v2: val): val :=
+  of_optbool (cmplu_bool c v1 v2).
+
 End COMPARISONS.
 
 (** [load_result] is used in the memory model (library [Mem])
@@ -423,6 +620,7 @@ Definition load_result (chunk: memory_chunk) (v: val) :=
   | Mint16unsigned, Vint n => Vint (Int.zero_ext 16 n)
   | Mint32, Vint n => Vint n
   | Mint32, Vptr b ofs => Vptr b ofs
+  | Mint64, Vlong n => Vlong n
   | Mfloat32, Vfloat f => Vfloat(Float.singleoffloat f)
   | (Mfloat64 | Mfloat64al32), Vfloat f => Vfloat f
   | _, _ => Vundef
@@ -981,6 +1179,12 @@ Inductive lessdef: val -> val -> Prop :=
   | lessdef_refl: forall v, lessdef v v
   | lessdef_undef: forall v, lessdef Vundef v.
 
+Lemma lessdef_same:
+  forall v1 v2, v1 = v2 -> lessdef v1 v2.
+Proof.
+  intros. subst v2. constructor.
+Qed.
+
 Lemma lessdef_trans:
   forall v1 v2 v3, lessdef v1 v2 -> lessdef v2 v3 -> lessdef v1 v3.
 Proof.
@@ -1071,6 +1275,25 @@ Proof.
   intros. destruct ob; simpl; auto. rewrite (H b); auto. 
 Qed.
 
+Lemma longofwords_lessdef:
+  forall v1 v2 v1' v2',
+  lessdef v1 v1' -> lessdef v2 v2' -> lessdef (longofwords v1 v2) (longofwords v1' v2').
+Proof.
+  intros. unfold longofwords. inv H; auto. inv H0; auto. destruct v1'; auto.
+Qed.
+
+Lemma loword_lessdef:
+  forall v v', lessdef v v' -> lessdef (loword v) (loword v').
+Proof.
+  intros. inv H; auto. 
+Qed.
+
+Lemma hiword_lessdef:
+  forall v v', lessdef v v' -> lessdef (hiword v) (hiword v').
+Proof.
+  intros. inv H; auto. 
+Qed.
+
 End Val.
 
 (** * Values and memory injections *)
@@ -1093,6 +1316,8 @@ Definition meminj : Type := block -> option (block * Z).
 Inductive val_inject (mi: meminj): val -> val -> Prop :=
   | val_inject_int:
       forall i, val_inject mi (Vint i) (Vint i)
+  | val_inject_long:
+      forall i, val_inject mi (Vlong i) (Vlong i)
   | val_inject_float:
       forall f, val_inject mi (Vfloat f) (Vfloat f)
   | val_inject_ptr:
@@ -1103,8 +1328,7 @@ Inductive val_inject (mi: meminj): val -> val -> Prop :=
   | val_inject_undef: forall v,
       val_inject mi Vundef v.
 
-Hint Resolve val_inject_int val_inject_float val_inject_ptr 
-             val_inject_undef.
+Hint Constructors val_inject.
 
 Inductive val_list_inject (mi: meminj): list val -> list val-> Prop:= 
   | val_nil_inject :
@@ -1225,6 +1449,25 @@ Proof.
   now erewrite !valid_ptr_inj by eauto.
 Qed.
 
+Lemma val_longofwords_inject:
+  forall v1 v2 v1' v2',
+  val_inject f v1 v1' -> val_inject f v2 v2' -> val_inject f (Val.longofwords v1 v2) (Val.longofwords v1' v2').
+Proof.
+  intros. unfold Val.longofwords. inv H; auto. inv H0; auto.
+Qed.
+
+Lemma val_loword_inject:
+  forall v v', val_inject f v v' -> val_inject f (Val.loword v) (Val.loword v').
+Proof.
+  intros. unfold Val.loword; inv H; auto. 
+Qed.
+
+Lemma val_hiword_inject:
+  forall v v', val_inject f v v' -> val_inject f (Val.hiword v) (Val.hiword v').
+Proof.
+  intros. unfold Val.hiword; inv H; auto. 
+Qed.
+
 End VAL_INJ_OPS.
 
 (** Monotone evolution of a memory injection. *)
@@ -1288,9 +1531,8 @@ Lemma val_inject_id:
   val_inject inject_id v1 v2 <-> Val.lessdef v1 v2.
 Proof.
   intros; split; intros.
-  inv H. constructor. constructor.
+  inv H; auto. 
   unfold inject_id in H0. inv H0. rewrite Int.add_zero. constructor.
-  constructor.
   inv H. destruct v2; econstructor. unfold inject_id; reflexivity. rewrite Int.add_zero; auto.
   constructor.
 Qed.