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

19 files changed, 1261 insertions, 1084 deletions

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 3bf459f..0ffbd66 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -160,10 +160,12 @@ let register_stub_function name tres targs =
   let rec letters_of_type = function
     | Tnil -> []
     | Tcons(Tfloat _, tl) -> "f" :: letters_of_type tl
+    | Tcons(Tlong _, tl) -> "l" :: letters_of_type tl
     | Tcons(_, tl) -> "i" :: letters_of_type tl in
   let rec types_of_types = function
     | Tnil -> Tnil
     | Tcons(Tfloat _, tl) -> Tcons(Tfloat(F64, noattr), types_of_types tl)
+    | Tcons(Tlong _, tl) -> Tcons(Tlong(Signed, noattr), types_of_types tl)
     | Tcons(_, tl) -> Tcons(Tpointer(Tvoid, noattr), types_of_types tl) in
   let stub_name =
     name ^ "$" ^ String.concat "" (letters_of_type targs) in
@@ -211,6 +213,7 @@ let mergeTypAttr ty a2 =
   | Tvoid -> ty
   | Tint(sz, sg, a1) -> Tint(sz, sg, mergeAttr a1 a2)
   | Tfloat(sz, a1) -> Tfloat(sz, mergeAttr a1 a2)
+  | Tlong(sg, a1) -> Tlong(sg, mergeAttr a1 a2)
   | Tpointer(ty', a1) -> Tpointer(ty', mergeAttr a1 a2)
   | Tarray(ty', sz, a1) -> Tarray(ty', sz, mergeAttr a1 a2)
   | Tfunction(targs, tres) -> ty
@@ -233,8 +236,7 @@ let convertIkind = function
   | C.ILong -> (Signed, I32)
   | C.IULong -> (Unsigned, I32)
   (* Special-cased in convertTyp below *)
-  | C.ILongLong -> unsupported "'long long' type"; (Signed, I32)
-  | C.IULongLong -> unsupported "'unsigned long long' type"; (Unsigned, I32)
+  | C.ILongLong | C.IULongLong -> assert false
 
 let convertFkind = function
   | C.FFloat -> F32
@@ -243,14 +245,6 @@ let convertFkind = function
       if not !Clflags.option_flongdouble then unsupported "'long double' type"; 
       F64
 
-let int64_struct a =
-  let ty = Tint(I32,Unsigned,noattr) in
-  Tstruct(intern_string "struct __int64",
-    (if Memdataaux.big_endian
-     then Fcons(intern_string "hi", ty, Fcons(intern_string "lo", ty, Fnil))
-     else Fcons(intern_string "lo", ty, Fcons(intern_string "hi", ty, Fnil))),
-    a)
-
 (** A cache for structs and unions already converted *)
 
 let compositeCache : (C.ident, coq_type) Hashtbl.t = Hashtbl.create 77
@@ -260,8 +254,10 @@ let convertTyp env t =
   let rec convertTyp seen t =
     match Cutil.unroll env t with
     | C.TVoid a -> Tvoid
-    | C.TInt((C.ILongLong|C.IULongLong), a) when !Clflags.option_flonglong ->
-        int64_struct (convertAttr a)
+    | C.TInt(C.ILongLong, a) ->
+        Tlong(Signed, convertAttr a)
+    | C.TInt(C.IULongLong, a) ->
+        Tlong(Unsigned, convertAttr a)
     | C.TInt(ik, a) ->
         let (sg, sz) = convertIkind ik in Tint(sz, sg, convertAttr a)
     | C.TFloat(fk, a) ->
@@ -360,14 +356,8 @@ let string_of_type ty =
   Format.pp_print_flush fb ();
   Buffer.contents b
 
-let first_class_value env ty =
-  match Cutil.unroll env ty with
-  | C.TInt((C.ILongLong|C.IULongLong), _) -> false
-  | _ -> true
-
 let supported_return_type env ty =
   match Cutil.unroll env ty with
-  | C.TInt((C.ILongLong|C.IULongLong), _) -> false
   | C.TStruct _  | C.TUnion _ -> false
   | _ -> true
 
@@ -419,10 +409,6 @@ let convertFloat f kind =
 
 let ezero = Eval(Vint(coqint_of_camlint 0l), type_int32s)
 
-let check_assignop msg env e =
-  if not (first_class_value env e.etyp) then
-    unsupported (msg ^ " on a l-value of type " ^ string_of_type e.etyp)
-
 let rec convertExpr env e =
   let ty = convertTyp env e.etyp in
   match e.edesc with
@@ -430,13 +416,11 @@ let rec convertExpr env e =
   | C.EUnop((C.Oderef|C.Odot _|C.Oarrow _), _)
   | C.EBinop(C.Oindex, _, _, _) ->
       let l = convertLvalue env e in
-      if not (first_class_value env e.etyp) then
-        unsupported ("r-value of type " ^ string_of_type e.etyp);
       Evalof(l, ty)
 
+  | C.EConst(C.CInt(i, (ILongLong|IULongLong), _)) ->
+      Eval(Vlong(coqint_of_camlint64 i), ty)
   | C.EConst(C.CInt(i, k, _)) ->
-      if k = C.ILongLong || k = C.IULongLong then
-        unsupported "'long long' integer literal";
       Eval(Vint(convertInt i), ty)
   | C.EConst(C.CFloat(f, k)) ->
       if k = C.FLongDouble && not !Clflags.option_flongdouble then
@@ -465,21 +449,17 @@ let rec convertExpr env e =
   | C.EUnop(C.Oaddrof, e1) ->
       Eaddrof(convertLvalue env e1, ty)
   | C.EUnop(C.Opreincr, e1) ->
-      check_assignop "pre-increment" env e1;
       coq_Epreincr Incr (convertLvalue env e1) ty
   | C.EUnop(C.Opredecr, e1) ->
-      check_assignop "pre-decrement" env e1;
       coq_Epreincr Decr (convertLvalue env e1) ty
   | C.EUnop(C.Opostincr, e1) ->
-      check_assignop "post-increment" env e1;
       Epostincr(Incr, convertLvalue env e1, ty)
   | C.EUnop(C.Opostdecr, e1) ->
-      check_assignop "post-decrement" env e1;
       Epostincr(Decr, convertLvalue env e1, ty)
 
   | C.EBinop((C.Oadd|C.Osub|C.Omul|C.Odiv|C.Omod|C.Oand|C.Oor|C.Oxor|
               C.Oshl|C.Oshr|C.Oeq|C.One|C.Olt|C.Ogt|C.Ole|C.Oge) as op,
-             e1, e2, _) ->
+             e1, e2, tyres) ->
       let op' =
         match op with
         | C.Oadd -> Oadd
@@ -503,7 +483,6 @@ let rec convertExpr env e =
   | C.EBinop(C.Oassign, e1, e2, _) ->
       let e1' = convertLvalue env e1 in
       let e2' = convertExpr env e2 in
-      check_assignop "assignment" env e1;
       Eassign(e1', e2', ty)
   | C.EBinop((C.Oadd_assign|C.Osub_assign|C.Omul_assign|C.Odiv_assign|
               C.Omod_assign|C.Oand_assign|C.Oor_assign|C.Oxor_assign|
@@ -525,7 +504,6 @@ let rec convertExpr env e =
         | _ -> assert false in
       let e1' = convertLvalue env e1 in
       let e2' = convertExpr env e2 in
-      check_assignop "assignment-operation" env e1;
       Eassignop(op', e1', e2', tyres, ty)
   | C.EBinop(C.Ocomma, e1, e2, _) ->
       Ecomma(convertExpr env e1, convertExpr env e2, ty)
@@ -537,8 +515,6 @@ let rec convertExpr env e =
   | C.EConditional(e1, e2, e3) ->
       Econdition(convertExpr env e1, convertExpr env e2, convertExpr env e3, ty)
   | C.ECast(ty1, e1) ->
-      if not (first_class_value env ty1) then
-        unsupported ("cast to type " ^ string_of_type ty1);
       Ecast(convertExpr env e1, convertTyp env ty1)
 
   | C.ECall({edesc = C.EVar {name = "__builtin_annot"}}, args) ->
diff --git a/cfrontend/CPragmas.ml b/cfrontend/CPragmas.ml
index 7bf80bb..5ae147e 100644
--- a/cfrontend/CPragmas.ml
+++ b/cfrontend/CPragmas.ml
@@ -49,8 +49,7 @@ let process_reserve_register_pragma name =
       C2C.error "unknown register in `reserve_register' pragma"
   | Some r ->
       if Machregsaux.can_reserve_register r then
-        Coloringaux.reserved_registers :=
-          r :: !Coloringaux.reserved_registers
+        IRC.reserved_registers := r :: !IRC.reserved_registers
       else
         C2C.error "cannot reserve this register (not a callee-save)"
 
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index ebc27ad..a19a0e2 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -104,6 +104,7 @@ Definition eventval_of_val (v: val) (t: typ) : option eventval :=
   match v, t with
   | Vint i, AST.Tint => Some (EVint i)
   | Vfloat f, AST.Tfloat => Some (EVfloat f)
+  | Vlong n, AST.Tlong => Some (EVlong n)
   | Vptr b ofs, AST.Tint => do id <- Genv.invert_symbol ge b; Some (EVptr_global id ofs)
   | _, _ => None
   end.
@@ -122,6 +123,7 @@ Definition val_of_eventval (ev: eventval) (t: typ) : option val :=
   match ev, t with
   | EVint i, AST.Tint => Some (Vint i)
   | EVfloat f, AST.Tfloat => Some (Vfloat f)
+  | EVlong n, AST.Tlong => Some (Vlong n)
   | EVptr_global id ofs, AST.Tint => do b <- Genv.find_symbol ge id; Some (Vptr b ofs)
   | _, _ => None
   end.
@@ -132,6 +134,7 @@ Proof.
   intros. destruct v; destruct t; simpl in H; inv H.
   constructor.
   constructor.
+  constructor.
   destruct (Genv.invert_symbol ge b) as [id|] eqn:?; inv H1. 
   constructor. apply Genv.invert_find_symbol; auto.
 Qed.
@@ -166,6 +169,7 @@ Proof.
   intros. destruct ev; destruct t; simpl in H; inv H.
   constructor.
   constructor.
+  constructor.
   destruct (Genv.find_symbol ge i) as [b|] eqn:?; inv H1.
   constructor. auto.
 Qed.
diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v
index e9ec7cc..3bd06df 100644
--- a/cfrontend/Clight.v
+++ b/cfrontend/Clight.v
@@ -48,6 +48,7 @@ Require Import Cop.
 Inductive expr : Type :=
   | Econst_int: int -> type -> expr       (**r integer literal *)
   | Econst_float: float -> type -> expr   (**r float literal *)
+  | Econst_long: int64 -> type -> expr    (**r long integer literal *)
   | Evar: ident -> type -> expr           (**r variable *)
   | Etempvar: ident -> type -> expr       (**r temporary variable *)
   | Ederef: expr -> type -> expr          (**r pointer dereference (unary [*]) *)
@@ -68,6 +69,7 @@ Definition typeof (e: expr) : type :=
   match e with
   | Econst_int _ ty => ty
   | Econst_float _ ty => ty
+  | Econst_long _ ty => ty
   | Evar _ ty => ty
   | Etempvar _ ty => ty
   | Ederef _ ty => ty
@@ -347,6 +349,8 @@ Inductive eval_expr: expr -> val -> Prop :=
       eval_expr (Econst_int i ty) (Vint i)
   | eval_Econst_float:   forall f ty,
       eval_expr (Econst_float f ty) (Vfloat f)
+  | eval_Econst_long:   forall i ty,
+      eval_expr (Econst_long i ty) (Vlong i)
   | eval_Etempvar:  forall id ty v,
       le!id = Some v ->
       eval_expr (Etempvar id ty) v
diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v
index af85971..419ffff 100644
--- a/cfrontend/Cminorgen.v
+++ b/cfrontend/Cminorgen.v
@@ -171,6 +171,7 @@ Definition of_chunk (chunk: memory_chunk) :=
   | Mint16signed => Int16s
   | Mint16unsigned => Int16u
   | Mint32 => Any
+  | Mint64 => Any
   | Mfloat32 => Float32
   | Mfloat64 => Any
   | Mfloat64al32 => Any
@@ -239,6 +240,8 @@ Definition transl_constant (cst: Csharpminor.constant): (constant * approx) :=
       (Ointconst n, Approx.of_int n)
   | Csharpminor.Ofloatconst n =>
       (Ofloatconst n, Approx.of_float n)
+  | Csharpminor.Olongconst n =>
+      (Olongconst n, Any)
   end.
 
 (** Translation of expressions.  Return both a Cminor expression and
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index a61808a..9d3d255 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -1495,6 +1495,8 @@ Ltac TrivialExists :=
       exists (Vint x); split; [eauto with evalexpr | constructor]
   | [ |- exists y, _ /\ val_inject _ (Vfloat ?x) _ ] =>
       exists (Vfloat x); split; [eauto with evalexpr | constructor]
+  | [ |- exists y, _ /\ val_inject _ (Vlong ?x) _ ] =>
+      exists (Vlong x); split; [eauto with evalexpr | constructor]
   | _ => idtac
   end.
 
@@ -1522,6 +1524,15 @@ Proof.
   inv H0; simpl in H; inv H. simpl. destruct (Float.intuoffloat f0); simpl in *; inv H1. TrivialExists.
   inv H0; simpl in H; inv H. simpl. TrivialExists.
   inv H0; simpl in H; inv H. simpl. TrivialExists.
+  inv H; inv H0; simpl; TrivialExists.
+  inv H; inv H0; simpl; TrivialExists.
+  inv H; inv H0; simpl; TrivialExists.
+  inv H; inv H0; simpl; TrivialExists.
+  inv H; inv H0; simpl; TrivialExists.
+  inv H0; simpl in H; inv H. simpl. destruct (Float.longoffloat f0); simpl in *; inv H1. TrivialExists.
+  inv H0; simpl in H; inv H. simpl. destruct (Float.longuoffloat f0); simpl in *; inv H1. TrivialExists.
+  inv H0; simpl in H; inv H. simpl. TrivialExists.
+  inv H0; simpl in H; inv H. simpl. TrivialExists.
 Qed.
 
 (** Compatibility of [eval_binop] with respect to [val_inject]. *)
@@ -1566,46 +1577,43 @@ Proof.
   inv H; inv H0; inv H1; TrivialExists.
   inv H; inv H0; inv H1; TrivialExists.
   inv H; inv H0; inv H1; TrivialExists.
+  inv H; inv H0; inv H1; TrivialExists.
+  inv H; inv H0; inv H1; TrivialExists.
+  inv H; inv H0; inv H1; TrivialExists.
+  inv H0; try discriminate; inv H1; try discriminate. simpl in *. 
+    destruct (Int64.eq i0 Int64.zero
+      || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H; TrivialExists.
+  inv H0; try discriminate; inv H1; try discriminate. simpl in *. 
+    destruct (Int64.eq i0 Int64.zero); inv H. TrivialExists.
+  inv H0; try discriminate; inv H1; try discriminate. simpl in *. 
+    destruct (Int64.eq i0 Int64.zero
+      || Int64.eq i (Int64.repr Int64.min_signed) && Int64.eq i0 Int64.mone); inv H; TrivialExists.
+  inv H0; try discriminate; inv H1; try discriminate. simpl in *. 
+    destruct (Int64.eq i0 Int64.zero); inv H. TrivialExists.
+  inv H; inv H0; inv H1; TrivialExists.
+  inv H; inv H0; inv H1; TrivialExists.
+  inv H; inv H0; inv H1; TrivialExists.
+  inv H; inv H0; inv H1; TrivialExists. simpl. destruct (Int.ltu i0 Int64.iwordsize'); auto.
+  inv H; inv H0; inv H1; TrivialExists. simpl. destruct (Int.ltu i0 Int64.iwordsize'); auto.
+  inv H; inv H0; inv H1; TrivialExists. simpl. destruct (Int.ltu i0 Int64.iwordsize'); auto.
   inv H; inv H0; inv H1; TrivialExists. apply val_inject_val_of_optbool.
 (* cmpu *)
-  inv H; inv H0; inv H1; TrivialExists.
-    apply val_inject_val_of_optbool.
-    apply val_inject_val_of_optbool.
-    apply val_inject_val_of_optbool.
-Opaque Int.add.
-    unfold Val.cmpu. simpl.
-    destruct (zeq b1 b0); subst.
-    (* same blocks *)
-    rewrite H0 in H. inv H. rewrite zeq_true.
-    fold (Mem.weak_valid_pointer m b0 (Int.unsigned ofs1)).
-    fold (Mem.weak_valid_pointer m b0 (Int.unsigned ofs0)).
-    fold (Mem.weak_valid_pointer tm b2 (Int.unsigned (Int.add ofs1 (Int.repr delta)))).
-    fold (Mem.weak_valid_pointer tm b2 (Int.unsigned (Int.add ofs0 (Int.repr delta)))).
-    destruct (Mem.weak_valid_pointer m b0 (Int.unsigned ofs1)) eqn:?; auto.
-    destruct (Mem.weak_valid_pointer m b0 (Int.unsigned ofs0)) eqn:?; auto.
-    rewrite (Mem.weak_valid_pointer_inject_val _ _ _ _ _ _ _ H2 Heqb) by eauto.
-    rewrite (Mem.weak_valid_pointer_inject_val _ _ _ _ _ _ _ H2 Heqb0) by eauto.
-    rewrite Int.translate_cmpu
-      by eauto using Mem.weak_valid_pointer_inject_no_overflow.
-    apply val_inject_val_of_optbool.
-    (* different source blocks *)
-    destruct (Mem.valid_pointer m b1 (Int.unsigned ofs1)) eqn:?; auto.
-    destruct (Mem.valid_pointer m b0 (Int.unsigned ofs0)) eqn:?; auto.
-    destruct (zeq b2 b3).
-    fold (Mem.weak_valid_pointer tm b2 (Int.unsigned (Int.add ofs1 (Int.repr delta)))).
-    fold (Mem.weak_valid_pointer tm b3 (Int.unsigned (Int.add ofs0 (Int.repr delta0)))).
-    rewrite Mem.valid_pointer_implies
-      by (eapply (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ H2 Heqb); eauto).
-    rewrite Mem.valid_pointer_implies
-      by (eapply (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ H2 Heqb0); eauto).
-    exploit Mem.different_pointers_inject; eauto. intros [A|A]; [congruence |].
-    destruct c; simpl; auto.
-    rewrite Int.eq_false. constructor. congruence.
-    rewrite Int.eq_false. constructor. congruence.
-    rewrite (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ H2 Heqb) by eauto.
-    rewrite (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ H2 Heqb0) by eauto.
-    apply val_inject_val_of_optbool.
-  (* cmpf *)
+  inv H. econstructor; split; eauto. 
+  unfold Val.cmpu. 
+  destruct (Val.cmpu_bool (Mem.valid_pointer m) c v1 v2) as [b|] eqn:E.
+  replace (Val.cmpu_bool (Mem.valid_pointer tm) c tv1 tv2) with (Some b).
+  destruct b; simpl; constructor.
+  symmetry. eapply val_cmpu_bool_inject; 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.
+  simpl; auto.
+(* cmpf *)
+  inv H; inv H0; inv H1; TrivialExists. apply val_inject_val_of_optbool.
+(* cmpl *)
+  inv H; inv H0; inv H1; TrivialExists. apply val_inject_val_of_optbool.
+(* cmplu *)
   inv H; inv H0; inv H1; TrivialExists. apply val_inject_val_of_optbool.
 Qed.
 
@@ -1843,6 +1851,8 @@ Proof.
   repeat rewrite Int.zero_ext_and; auto. omega. omega.
   (* int32 *)
   exists va; auto.
+  (* int64 *)
+  exists va; auto.
   (* float32 *)
   exploit eval_uncast_float32; eauto. intros [v' [A B]].
   exists v'; split; auto.
@@ -2036,6 +2046,7 @@ Proof.
   destruct cst; simpl; intros; inv H. 
   exists (Vint i); intuition. apply approx_of_int_sound.
   exists (Vfloat f0); intuition. apply approx_of_float_sound.
+  exists (Vlong i); intuition. 
 Qed.
 
 Lemma transl_expr_correct:
diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v
index af7aaa8..c6e07b7 100644
--- a/cfrontend/Cop.v
+++ b/cfrontend/Cop.v
@@ -76,23 +76,35 @@ Inductive classify_cast_cases : Type :=
   | cast_case_f2f (sz2:floatsize)                  (**r float -> float *)
   | cast_case_i2f (si1:signedness) (sz2:floatsize) (**r int -> float *)
   | cast_case_f2i (sz2:intsize) (si2:signedness)   (**r float -> int *)
+  | cast_case_l2l                       (**r long -> long *)
+  | cast_case_i2l (si1: signedness)     (**r int -> long *)
+  | cast_case_l2i (sz2: intsize) (si2: signedness) (**r long -> int *)
+  | cast_case_l2f (si1: signedness) (sz2: floatsize) (**r long -> float *)
+  | cast_case_f2l (si2: signedness)     (**r float -> long *)
   | cast_case_f2bool                    (**r float -> bool *)
+  | cast_case_l2bool                    (**r long -> bool *)
   | cast_case_p2bool                    (**r pointer -> bool *)
   | cast_case_struct (id1: ident) (fld1: fieldlist) (id2: ident) (fld2: fieldlist) (**r struct -> struct *)
   | cast_case_union (id1: ident) (fld1: fieldlist) (id2: ident) (fld2: fieldlist) (**r union -> union *)
   | cast_case_void                                 (**r any -> void *)
   | cast_case_default.
 
-Function classify_cast (tfrom tto: type) : classify_cast_cases :=
+Definition classify_cast (tfrom tto: type) : classify_cast_cases :=
   match tto, tfrom with
-  | Tint I32 si2 _, (Tint _ _ _ | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _) => cast_case_neutral
+  | Tint I32 si2 _, (Tint _ _ _ | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _) => cast_case_neutral
   | Tint IBool _ _, Tfloat _ _ => cast_case_f2bool
-  | Tint IBool _ _, (Tpointer _ _ | Tarray _ _ _ | Tfunction _ _) => cast_case_p2bool
+  | Tint IBool _ _, (Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _) => cast_case_p2bool
   | Tint sz2 si2 _, Tint sz1 si1 _ => cast_case_i2i sz2 si2
   | Tint sz2 si2 _, Tfloat sz1 _ => cast_case_f2i sz2 si2
   | Tfloat sz2 _, Tfloat sz1 _ => cast_case_f2f sz2
   | Tfloat sz2 _, Tint sz1 si1 _ => cast_case_i2f si1 sz2
-  | Tpointer _ _, (Tint _ _ _ | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _) => cast_case_neutral
+  | (Tpointer _ _ | Tcomp_ptr _ _), (Tint _ _ _ | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _) => cast_case_neutral
+  | Tlong _ _, Tlong _ _ => cast_case_l2l
+  | Tlong _ _, Tint sz1 si1 _ => cast_case_i2l si1
+  | Tint IBool _ _, Tlong _ _ => cast_case_l2bool
+  | Tint sz2 si2 _, Tlong _ _ => cast_case_l2i sz2 si2
+  | Tlong si2 _, Tfloat sz1 _ => cast_case_f2l si2
+  | Tfloat sz2 _, Tlong si1 _ => cast_case_l2f si1 sz2
   | Tstruct id2 fld2 _, Tstruct id1 fld1 _ => cast_case_struct id1 fld1 id2 fld2
   | Tunion id2 fld2 _, Tunion id1 fld1 _ => cast_case_union id1 fld1 id2 fld2
   | Tvoid, _ => cast_case_void
@@ -131,7 +143,25 @@ Definition cast_float_float (sz: floatsize) (f: float) : float :=
   | F64 => f
   end.
 
-Function sem_cast (v: val) (t1 t2: type) : option val :=
+Definition cast_int_long (si: signedness) (i: int) : int64 :=
+  match si with
+  | Signed => Int64.repr (Int.signed i)
+  | Unsigned => Int64.repr (Int.unsigned i)
+  end.
+
+Definition cast_long_float (si : signedness) (i: int64) : float :=
+  match si with
+  | Signed => Float.floatoflong i
+  | Unsigned => Float.floatoflongu i
+  end.
+
+Definition cast_float_long (si : signedness) (f: float) : option int64 :=
+  match si with
+  | Signed => Float.longoffloat f
+  | Unsigned => Float.longuoffloat f
+  end.
+
+Definition sem_cast (v: val) (t1 t2: type) : option val :=
   match classify_cast t1 t2 with
   | cast_case_neutral =>
       match v with
@@ -174,10 +204,53 @@ Function sem_cast (v: val) (t1 t2: type) : option val :=
       | Vptr _ _ => Some (Vint Int.one)
       | _ => None
       end
+  | cast_case_l2l =>
+      match v with
+      | Vlong n => Some (Vlong n)
+      | _ => None
+      end
+  | cast_case_i2l si =>
+      match v with
+      | Vint n => Some(Vlong (cast_int_long si n))
+      | _ => None
+      end
+  | cast_case_l2i sz si =>
+      match v with
+      | Vlong n => Some(Vint (cast_int_int sz si (Int.repr (Int64.unsigned n))))
+      | _ => None
+      end
+  | cast_case_l2bool =>
+      match v with
+      | Vlong n =>
+          Some(Vint(if Int64.eq n Int64.zero then Int.zero else Int.one))
+      | _ => None
+      end
+  | cast_case_l2f si1 sz2 =>
+      match v with
+      | Vlong i => Some (Vfloat (cast_float_float sz2 (cast_long_float si1 i)))
+      | _ => None
+      end
+  | cast_case_f2l si2 =>
+      match v with
+      | Vfloat f =>
+          match cast_float_long si2 f with
+          | Some i => Some (Vlong i)
+          | None => None
+          end
+      | _ => None
+      end
   | cast_case_struct id1 fld1 id2 fld2 =>
-      if ident_eq id1 id2 && fieldlist_eq fld1 fld2 then Some v else None
+      match v with
+      | Vptr b ofs =>
+          if ident_eq id1 id2 && fieldlist_eq fld1 fld2 then Some v else None
+      | _ => None
+      end
   | cast_case_union id1 fld1 id2 fld2 =>
-      if ident_eq id1 id2 && fieldlist_eq fld1 fld2 then Some v else None
+      match v with
+      | Vptr b ofs =>
+          if ident_eq id1 id2 && fieldlist_eq fld1 fld2 then Some v else None
+      | _ => None
+      end
   | cast_case_void =>
       Some v
   | cast_case_default =>
@@ -192,13 +265,15 @@ Inductive classify_bool_cases : Type :=
   | bool_case_i                           (**r integer *)
   | bool_case_f                           (**r float *)
   | bool_case_p                           (**r pointer *)
+  | bool_case_l                           (**r long *)
   | bool_default.
 
 Definition classify_bool (ty: type) : classify_bool_cases :=
   match typeconv ty with
   | Tint _ _ _ => bool_case_i
-  | Tpointer _ _ => bool_case_p
+  | Tpointer _ _ | Tcomp_ptr _ _ => bool_case_p
   | Tfloat _ _ => bool_case_f
+  | Tlong _ _ => bool_case_l
   | _ => bool_default
   end.
 
@@ -207,7 +282,7 @@ Definition classify_bool (ty: type) : classify_bool_cases :=
   considered as true.  The integer zero (which also represents
   the null pointer) and the float 0.0 are false. *)
 
-Function bool_val (v: val) (t: type) : option bool :=
+Definition bool_val (v: val) (t: type) : option bool :=
   match classify_bool t with
   | bool_case_i =>
       match v with
@@ -225,6 +300,11 @@ Function bool_val (v: val) (t: type) : option bool :=
       | Vptr b ofs => Some true
       | _ => None
       end
+  | bool_case_l =>
+      match v with
+      | Vlong n => Some (negb (Int64.eq n Int64.zero))
+      | _ => None
+      end
   | bool_default => None
   end.
 
@@ -239,25 +319,29 @@ Proof.
   assert (A: classify_bool t =
     match t with
     | Tint _ _ _ => bool_case_i
-    | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ => bool_case_p
+    | Tpointer _ _ | Tcomp_ptr _ _ | Tarray _ _ _ | Tfunction _ _ => bool_case_p
     | Tfloat _ _ => bool_case_f
+    | Tlong _ _ => bool_case_l
     | _ => bool_default
     end).
-  unfold classify_bool; destruct t; simpl; auto. destruct i; auto. destruct s; auto.
-
+  {
+    unfold classify_bool; destruct t; simpl; auto. destruct i; auto.
+  }
   unfold bool_val. rewrite A. unfold sem_cast. destruct t; simpl; auto; destruct v; auto.
-  destruct (Int.eq i0 Int.zero); auto. 
+  destruct (Int.eq i0 Int.zero); auto.
+  destruct (Int64.eq i Int64.zero); auto.
   destruct (Float.cmp Ceq f0 Float.zero); auto.
   destruct (Int.eq i Int.zero); auto. 
   destruct (Int.eq i Int.zero); auto. 
   destruct (Int.eq i Int.zero); auto. 
+  destruct (Int.eq i0 Int.zero); auto. 
 Qed.
 
 (** ** Unary operators *)
 
 (** *** Boolean negation *)
 
-Function sem_notbool (v: val) (ty: type) : option val :=
+Definition sem_notbool (v: val) (ty: type) : option val :=
   match classify_bool ty with
   | bool_case_i =>
       match v with
@@ -275,6 +359,11 @@ Function sem_notbool (v: val) (ty: type) : option val :=
       | Vptr _ _ => Some Vfalse
       | _ => None
       end
+  | bool_case_l =>
+      match v with
+      | Vlong n => Some (Val.of_bool (Int64.eq n Int64.zero))
+      | _ => None
+      end
   | bool_default => None
   end.
 
@@ -294,6 +383,7 @@ Qed.
 Inductive classify_neg_cases : Type :=
   | neg_case_i(s: signedness)              (**r int *)
   | neg_case_f                             (**r float *)
+  | neg_case_l(s: signedness)              (**r long *)
   | neg_default.
 
 Definition classify_neg (ty: type) : classify_neg_cases :=
@@ -301,10 +391,11 @@ Definition classify_neg (ty: type) : classify_neg_cases :=
   | Tint I32 Unsigned _ => neg_case_i Unsigned
   | Tint _ _ _ => neg_case_i Signed
   | Tfloat _ _ => neg_case_f
+  | Tlong si _ => neg_case_l si
   | _ => neg_default
   end.
 
-Function sem_neg (v: val) (ty: type) : option val :=
+Definition sem_neg (v: val) (ty: type) : option val :=
   match classify_neg ty with
   | neg_case_i sg =>
       match v with
@@ -316,6 +407,11 @@ Function sem_neg (v: val) (ty: type) : option val :=
       | Vfloat f => Some (Vfloat (Float.neg f))
       | _ => None
       end
+  | neg_case_l sg =>
+      match v with
+      | Vlong n => Some (Vlong (Int64.neg n))
+      | _ => None
+      end
   | neg_default => None
   end.
 
@@ -323,20 +419,27 @@ Function sem_neg (v: val) (ty: type) : option val :=
 
 Inductive classify_notint_cases : Type :=
   | notint_case_i(s: signedness)              (**r int *)
+  | notint_case_l(s: signedness)              (**r long *)
   | notint_default.
 
 Definition classify_notint (ty: type) : classify_notint_cases :=
   match ty with
   | Tint I32 Unsigned _ => notint_case_i Unsigned
   | Tint _ _ _ => notint_case_i Signed
+  | Tlong si _ => notint_case_l si
   | _ => notint_default
   end.
 
-Function sem_notint (v: val) (ty: type): option val :=
+Definition sem_notint (v: val) (ty: type): option val :=
   match classify_notint ty with
   | notint_case_i sg =>
       match v with
-      | Vint n => Some (Vint (Int.xor n Int.mone))
+      | Vint n => Some (Vint (Int.not n))
+      | _ => None
+      end
+  | notint_case_l sg =>
+      match v with
+      | Vlong n => Some (Vlong (Int64.not n))
       | _ => None
       end
   | notint_default => None
@@ -351,59 +454,119 @@ Function sem_notint (v: val) (ty: type): option val :=
   (e.g. division, modulus, comparisons), the unsigned operation is selected
   if at least one of the arguments is of type "unsigned int32", otherwise
   the signed operation is performed.
+- Likewise if both arguments are of long integer type.
 - If both arguments are of float type, a float operation is performed.
   We choose to perform all float arithmetic in double precision,
   even if both arguments are single-precision floats.
-- If one argument has integer type and the other has float type,
+- If one argument has integer/long type and the other has float type,
   we convert the integer argument to float, then perform the float operation.
+- If one argument has long integer type and the other integer type,
+  we convert the integer argument to long, then perform the long operation
 *)
 
-(** *** Addition *)
-
-Inductive classify_add_cases : Type :=
-  | add_case_ii(s: signedness)         (**r int, int *)
-  | add_case_ff                        (**r float, float *)
-  | add_case_if(s: signedness)         (**r int, float *)
-  | add_case_fi(s: signedness)         (**r float, int *)
-  | add_case_pi(ty: type)(a: attr)     (**r pointer, int *)
-  | add_case_ip(ty: type)(a: attr)     (**r int, pointer *)
-  | add_default.
-
-Definition classify_add (ty1: type) (ty2: type) :=
+Inductive binarith_cases: Type :=
+  | bin_case_ii(s: signedness)         (**r int, int *)
+  | bin_case_ff                        (**r float, float *)
+  | bin_case_if(s: signedness)         (**r int, float *)
+  | bin_case_fi(s: signedness)         (**r float, int *)
+  | bin_case_ll(s: signedness)         (**r long, long *)
+  | bin_case_il(s1 s2: signedness)     (**r int, long *)
+  | bin_case_li(s1 s2: signedness)     (**r long, int *)
+  | bin_case_lf(s: signedness)         (**r long, float *)
+  | bin_case_fl(s: signedness)         (**r float, long *)
+  | bin_default.
+
+Definition classify_binarith (ty1: type) (ty2: type) : binarith_cases :=
   match typeconv ty1, typeconv ty2 with
-  | Tint I32 Unsigned _, Tint _ _ _ => add_case_ii Unsigned
-  | Tint _ _ _, Tint I32 Unsigned _ => add_case_ii Unsigned
-  | Tint _ _ _, Tint _ _ _ => add_case_ii Signed
-  | Tfloat _ _, Tfloat _ _ => add_case_ff
-  | Tint _ sg _, Tfloat _ _ => add_case_if sg
-  | Tfloat _ _, Tint _ sg _ => add_case_fi sg
-  | Tpointer ty a, Tint _ _ _ => add_case_pi ty a
-  | Tint _ _ _, Tpointer ty a => add_case_ip ty a
-  | _, _ => add_default
+  | Tint I32 Unsigned _, Tint _ _ _ => bin_case_ii Unsigned
+  | Tint _ _ _, Tint I32 Unsigned _ => bin_case_ii Unsigned
+  | Tint _ _ _, Tint _ _ _ => bin_case_ii Signed
+  | Tfloat _ _, Tfloat _ _ => bin_case_ff
+  | Tint _ sg _, Tfloat _ _ => bin_case_if sg
+  | Tfloat _ _, Tint _ sg _ => bin_case_fi sg
+  | Tlong Signed _, Tlong Signed _ => bin_case_ll Signed
+  | Tlong _ _, Tlong _ _ => bin_case_ll Unsigned
+  | Tint _ s1 _, Tlong s2 _ => bin_case_il s1 s2
+  | Tlong s1 _, Tint _ s2 _ => bin_case_li s1 s2
+  | Tlong sg _, Tfloat _ _ => bin_case_lf sg
+  | Tfloat _ _, Tlong sg _ => bin_case_fl sg
+  | _, _ => bin_default
   end.
 
-Function sem_add (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
-  match classify_add t1 t2 with 
-  | add_case_ii sg =>                   (**r integer addition *)
+Definition sem_binarith
+    (sem_int: signedness -> int -> int -> option val)
+    (sem_long: signedness -> int64 -> int64 -> option val)
+    (sem_float: float -> float -> option val)
+    (v1: val) (t1: type) (v2: val) (t2: type) : option val :=
+  match classify_binarith t1 t2 with
+  | bin_case_ii sg =>
+      match v1, v2 with
+      | Vint n1, Vint n2 => sem_int sg n1 n2
+      | _,  _ => None
+      end
+  | bin_case_ff =>
+      match v1, v2 with
+      | Vfloat n1, Vfloat n2 => sem_float n1 n2
+      | _,  _ => None
+      end
+  | bin_case_if sg =>
+      match v1, v2 with
+      | Vint n1, Vfloat n2 => sem_float (cast_int_float sg n1) n2
+      | _, _ => None
+      end
+  | bin_case_fi sg =>
+      match v1, v2 with
+      | Vfloat n1, Vint n2 => sem_float n1 (cast_int_float sg n2)
+      | _, _ => None
+      end
+  | bin_case_ll sg =>
+      match v1, v2 with
+      | Vlong n1, Vlong n2 => sem_long sg n1 n2
+      | _,  _ => None
+      end
+  | bin_case_il sg1 sg2 =>
       match v1, v2 with
-      | Vint n1, Vint n2 => Some (Vint (Int.add n1 n2))
+      | Vint n1, Vlong n2 => sem_long sg2 (cast_int_long sg1 n1) n2
       | _,  _ => None
       end
-  | add_case_ff =>                      (**r float addition *)
+  | bin_case_li sg1 sg2 =>
       match v1, v2 with
-      | Vfloat n1, Vfloat n2 => Some (Vfloat (Float.add n1 n2))
+      | Vlong n1, Vint n2 => sem_long sg1 n1 (cast_int_long sg2 n2)
       | _,  _ => None
       end
-  | add_case_if sg =>                   (**r int plus float *)
+  | bin_case_lf sg =>
       match v1, v2 with
-      | Vint n1, Vfloat n2 => Some (Vfloat (Float.add (cast_int_float sg n1) n2))
+      | Vlong n1, Vfloat n2 => sem_float (cast_long_float sg n1) n2
       | _, _ => None
       end
-  | add_case_fi sg =>                   (**r float plus int *)
+  | bin_case_fl sg =>
       match v1, v2 with
-      | Vfloat n1, Vint n2 => Some (Vfloat (Float.add n1 (cast_int_float sg n2)))
+      | Vfloat n1, Vlong n2 => sem_float n1 (cast_long_float sg n2)
       | _, _ => None
       end
+  | bin_default => None
+  end.
+
+(** *** Addition *)
+
+Inductive classify_add_cases : Type :=
+  | add_case_pi(ty: type)(a: attr)     (**r pointer, int *)
+  | add_case_ip(ty: type)(a: attr)     (**r int, pointer *)
+  | add_case_pl(ty: type)(a: attr)     (**r pointer, long *)
+  | add_case_lp(ty: type)(a: attr)     (**r long, pointer *)
+  | add_default.                       (**r numerical type, numerical type *)
+
+Definition classify_add (ty1: type) (ty2: type) :=
+  match typeconv ty1, typeconv ty2 with
+  | Tpointer ty a, Tint _ _ _ => add_case_pi ty a
+  | Tint _ _ _, Tpointer ty a => add_case_ip ty a
+  | Tpointer ty a, Tlong _ _ => add_case_pl ty a
+  | Tlong _ _, Tpointer ty a => add_case_lp ty a
+  | _, _ => add_default
+  end.
+
+Definition sem_add (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
+  match classify_add t1 t2 with 
   | add_case_pi ty _ =>                 (**r pointer plus integer *)
       match v1,v2 with
       | Vptr b1 ofs1, Vint n2 => 
@@ -416,59 +579,57 @@ Function sem_add (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
         Some (Vptr b2 (Int.add ofs2 (Int.mul (Int.repr (sizeof ty)) n1)))
       | _,  _ => None
       end   
-  | add_default => None
-end.
+  | add_case_pl ty _ =>                 (**r pointer plus long *)
+      match v1,v2 with
+      | Vptr b1 ofs1, Vlong n2 => 
+        let n2 := Int.repr (Int64.unsigned n2) in
+        Some (Vptr b1 (Int.add ofs1 (Int.mul (Int.repr (sizeof ty)) n2)))
+      | _,  _ => None
+      end   
+  | add_case_lp ty _ =>                 (**r long plus pointer *)
+      match v1,v2 with
+      | Vlong n1, Vptr b2 ofs2 => 
+        let n1 := Int.repr (Int64.unsigned n1) in
+        Some (Vptr b2 (Int.add ofs2 (Int.mul (Int.repr (sizeof ty)) n1)))
+      | _,  _ => None
+      end   
+  | add_default =>
+      sem_binarith
+        (fun sg n1 n2 => Some(Vint(Int.add n1 n2)))
+        (fun sg n1 n2 => Some(Vlong(Int64.add n1 n2)))
+        (fun n1 n2 => Some(Vfloat(Float.add n1 n2)))
+        v1 t1 v2 t2
+  end.
 
 (** *** Subtraction *)
 
 Inductive classify_sub_cases : Type :=
-  | sub_case_ii(s: signedness)          (**r int , int *)
-  | sub_case_ff                         (**r float , float *)
-  | sub_case_if(s: signedness)          (**r int, float *)
-  | sub_case_fi(s: signedness)          (**r float, int *)
-  | sub_case_pi(ty: type)               (**r pointer, int *)
+  | sub_case_pi(ty: type)(a: attr)      (**r pointer, int *)
   | sub_case_pp(ty: type)               (**r pointer, pointer *)
-  | sub_default.
+  | sub_case_pl(ty: type)(a: attr)      (**r pointer, long *)
+  | sub_default.                        (**r numerical type, numerical type *)
 
 Definition classify_sub (ty1: type) (ty2: type) :=
   match typeconv ty1, typeconv ty2 with
-  | Tint I32 Unsigned _, Tint _ _ _ => sub_case_ii Unsigned
-  | Tint _ _ _, Tint I32 Unsigned _ => sub_case_ii Unsigned
-  | Tint _ _ _, Tint _ _ _ => sub_case_ii Signed
-  | Tfloat _ _ , Tfloat _ _ => sub_case_ff
-  | Tint _ sg _, Tfloat _ _ => sub_case_if sg
-  | Tfloat _ _, Tint _ sg _ => sub_case_fi sg
-  | Tpointer ty _, Tint _ _ _ => sub_case_pi ty
+  | Tpointer ty a, Tint _ _ _ => sub_case_pi ty a
   | Tpointer ty _ , Tpointer _ _ => sub_case_pp ty
-  | _ ,_ => sub_default
+  | Tpointer ty a, Tlong _ _ => sub_case_pl ty a
+  | _, _ => sub_default
   end.
 
-Function sem_sub (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
+Definition sem_sub (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
   match classify_sub t1 t2 with
-  | sub_case_ii sg =>            (**r integer subtraction *)
-      match v1,v2 with
-      | Vint n1, Vint n2 => Some (Vint (Int.sub n1 n2))
-      | _,  _ => None
-      end 
-  | sub_case_ff =>               (**r float subtraction *)
+  | sub_case_pi ty attr =>            (**r pointer minus integer *)
       match v1,v2 with
-      | Vfloat f1, Vfloat f2 => Some (Vfloat(Float.sub f1 f2))
+      | Vptr b1 ofs1, Vint n2 => 
+          Some (Vptr b1 (Int.sub ofs1 (Int.mul (Int.repr (sizeof ty)) n2)))
       | _,  _ => None
       end
-  | sub_case_if sg =>            (**r int minus float *)
-      match v1, v2 with
-      | Vint n1, Vfloat n2 => Some (Vfloat (Float.sub (cast_int_float sg n1) n2))
-      | _, _ => None
-      end
-  | sub_case_fi sg =>            (**r float minus int *)
-      match v1, v2 with
-      | Vfloat n1, Vint n2 => Some (Vfloat (Float.sub n1 (cast_int_float sg n2)))
-      | _, _ => None
-      end
-  | sub_case_pi ty =>            (**r pointer minus integer *)
+  | sub_case_pl ty attr =>            (**r pointer minus long *)
       match v1,v2 with
-      | Vptr b1 ofs1, Vint n2 => 
-            Some (Vptr b1 (Int.sub ofs1 (Int.mul (Int.repr (sizeof ty)) n2)))
+      | Vptr b1 ofs1, Vlong n2 => 
+          let n2 := Int.repr (Int64.unsigned n2) in
+          Some (Vptr b1 (Int.sub ofs1 (Int.mul (Int.repr (sizeof ty)) n2)))
       | _,  _ => None
       end
   | sub_case_pp ty =>          (**r pointer minus pointer *)
@@ -480,255 +641,187 @@ Function sem_sub (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
           else None
       | _, _ => None
       end
-  | sub_default => None
+  | sub_default =>
+      sem_binarith
+        (fun sg n1 n2 => Some(Vint(Int.sub n1 n2)))
+        (fun sg n1 n2 => Some(Vlong(Int64.sub n1 n2)))
+        (fun n1 n2 => Some(Vfloat(Float.sub n1 n2)))
+        v1 t1 v2 t2
   end.
  
-(** *** Multiplication *)
-
-Inductive classify_mul_cases : Type:=
-  | mul_case_ii(s: signedness) (**r int , int *)
-  | mul_case_ff                (**r float , float *)
-  | mul_case_if(s: signedness) (**r int, float *)
-  | mul_case_fi(s: signedness) (**r float, int *)
-  | mul_default.
-
-Definition classify_mul (ty1: type) (ty2: type) :=
-  match typeconv ty1, typeconv ty2 with
-  | Tint I32 Unsigned _, Tint _ _ _ => mul_case_ii Unsigned
-  | Tint _ _ _, Tint I32 Unsigned _ => mul_case_ii Unsigned
-  | Tint _ _ _, Tint _ _ _ => mul_case_ii Signed
-  | Tfloat _ _ , Tfloat _ _ => mul_case_ff
-  | Tint _ sg _, Tfloat _ _ => mul_case_if sg
-  | Tfloat _ _, Tint _ sg _ => mul_case_fi sg
-  | _,_  => mul_default
-end.
-
-Function sem_mul (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
- match classify_mul t1 t2 with
-  | mul_case_ii sg =>
-      match v1,v2 with
-      | Vint n1, Vint n2 => Some (Vint (Int.mul n1 n2))
-      | _,  _ => None
-      end
-  | mul_case_ff =>
-      match v1,v2 with
-      | Vfloat f1, Vfloat f2 => Some (Vfloat (Float.mul f1 f2))
-      | _,  _ => None
-      end
-  | mul_case_if sg =>
-      match v1, v2 with
-      | Vint n1, Vfloat n2 => Some (Vfloat (Float.mul (cast_int_float sg n1) n2))
-      | _, _ => None
-      end
-  | mul_case_fi sg =>
-      match v1, v2 with
-      | Vfloat n1, Vint n2 => Some (Vfloat (Float.mul n1 (cast_int_float sg n2)))
-      | _, _ => None
-      end
-  | mul_default =>
-      None
-end.
-
-(** *** Division *)
-
-Inductive classify_div_cases : Type:=
-  | div_case_ii(s: signedness) (**r int , int *)
-  | div_case_ff                (**r float , float *)
-  | div_case_if(s: signedness) (**r int, float *)
-  | div_case_fi(s: signedness) (**r float, int *)
-  | div_default.
-
-Definition classify_div (ty1: type) (ty2: type) :=
-  match typeconv ty1, typeconv ty2 with
-  | Tint I32 Unsigned _, Tint _ _ _ => div_case_ii Unsigned
-  | Tint _ _ _, Tint I32 Unsigned _ => div_case_ii Unsigned
-  | Tint _ _ _, Tint _ _ _ => div_case_ii Signed
-  | Tfloat _ _ , Tfloat _ _ => div_case_ff
-  | Tint _ sg _, Tfloat _ _ => div_case_if sg
-  | Tfloat _ _, Tint _ sg _ => div_case_fi sg
-  | _,_  => div_default
-end.
-
-Function sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
-   match classify_div t1 t2 with
-  | div_case_ii Unsigned =>
-      match v1,v2 with
-      | Vint n1, Vint n2 =>
-          if Int.eq n2 Int.zero then None else Some (Vint (Int.divu n1 n2))
-      | _,_ => None
-      end
-  | div_case_ii Signed =>
-      match v1,v2 with
-       | Vint n1, Vint n2 =>
+(** *** Multiplication, division, modulus *)
+
+Definition sem_mul (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
+  sem_binarith
+    (fun sg n1 n2 => Some(Vint(Int.mul n1 n2)))
+    (fun sg n1 n2 => Some(Vlong(Int64.mul n1 n2)))
+    (fun n1 n2 => Some(Vfloat(Float.mul n1 n2)))
+    v1 t1 v2 t2.
+
+Definition sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
+  sem_binarith
+    (fun sg n1 n2 =>
+      match sg with
+      | Signed =>
           if Int.eq n2 Int.zero
           || Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone
-          then None else Some (Vint(Int.divs n1 n2))
-      | _,_ => None
-      end
-  | div_case_ff =>
-      match v1,v2 with
-      | Vfloat f1, Vfloat f2 => Some (Vfloat(Float.div f1 f2))
-      | _,  _ => None
-      end 
-  | div_case_if sg =>
-      match v1, v2 with
-      | Vint n1, Vfloat n2 => Some (Vfloat (Float.div (cast_int_float sg n1) n2))
-      | _, _ => None
-      end
-  | div_case_fi sg =>
-      match v1, v2 with
-      | Vfloat n1, Vint n2 => Some (Vfloat (Float.div n1 (cast_int_float sg n2)))
-      | _, _ => None
-      end
-  | div_default =>
-      None
-end.
-
-(** *** Integer-only binary operations: modulus, bitwise "and", "or", and "xor" *)
-
-Inductive classify_binint_cases : Type:=
-  | binint_case_ii(s: signedness) (**r int , int *)
-  | binint_default.
-
-Definition classify_binint (ty1: type) (ty2: type) :=
-  match typeconv ty1, typeconv ty2 with
-  | Tint I32 Unsigned _, Tint _ _ _ => binint_case_ii Unsigned
-  | Tint _ _ _, Tint I32 Unsigned _ => binint_case_ii Unsigned
-  | Tint _ _ _, Tint _ _ _ => binint_case_ii Signed
-  | _,_  => binint_default
-end.
-
-Function sem_mod (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
-  match classify_binint t1 t2 with
-  | binint_case_ii Unsigned =>
-      match v1, v2 with
-      | Vint n1, Vint n2 =>
-          if Int.eq n2 Int.zero then None else Some (Vint (Int.modu n1 n2))
-      | _, _ => None
-      end
-  | binint_case_ii Signed =>
-      match v1,v2 with
-      | Vint n1, Vint n2 =>
+          then None else Some(Vint(Int.divs n1 n2))
+      | Unsigned =>
+          if Int.eq n2 Int.zero
+          then None else Some(Vint(Int.divu n1 n2))
+      end)
+    (fun sg n1 n2 =>
+      match sg with
+      | Signed =>
+          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))
+      | Unsigned =>
+          if Int64.eq n2 Int64.zero
+          then None else Some(Vlong(Int64.divu n1 n2))
+      end)
+    (fun n1 n2 => Some(Vfloat(Float.div n1 n2)))
+    v1 t1 v2 t2.
+
+Definition sem_mod (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
+  sem_binarith
+    (fun sg n1 n2 =>
+      match sg with
+      | Signed =>
           if Int.eq n2 Int.zero
           || Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone
-          then None else Some (Vint (Int.mods n1 n2))
-      | _, _ => None
-      end
-  | binint_default =>
-      None
-  end.
-
-Function sem_and (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
-  match classify_binint t1 t2 with
-  | binint_case_ii sg =>
-      match v1, v2 with
-      | Vint n1, Vint n2 => Some (Vint(Int.and n1 n2))
-      | _, _ => None
-      end
-  | binint_default => None
-  end.
-
-Function sem_or (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
-  match classify_binint t1 t2 with
-  | binint_case_ii sg =>
-      match v1, v2 with
-      | Vint n1, Vint n2 => Some (Vint(Int.or n1 n2))
-      | _, _ => None
-      end
-  | binint_default => None
-  end.
-
-Function sem_xor (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
-  match classify_binint t1 t2 with
-  | binint_case_ii sg =>
-      match v1, v2 with
-      | Vint n1, Vint n2 => Some (Vint(Int.xor n1 n2))
-      | _, _ => None
-      end
-  | binint_default => None
-  end.
+          then None else Some(Vint(Int.mods n1 n2))
+      | Unsigned =>
+          if Int.eq n2 Int.zero
+          then None else Some(Vint(Int.modu n1 n2))
+      end)
+    (fun sg n1 n2 =>
+      match sg with
+      | Signed =>
+          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))
+      | Unsigned =>
+          if Int64.eq n2 Int64.zero
+          then None else Some(Vlong(Int64.modu n1 n2))
+      end)
+    (fun n1 n2 => None)
+    v1 t1 v2 t2.
+
+Definition sem_and (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
+  sem_binarith
+    (fun sg n1 n2 => Some(Vint(Int.and n1 n2)))
+    (fun sg n1 n2 => Some(Vlong(Int64.and n1 n2)))
+    (fun n1 n2 => None)
+    v1 t1 v2 t2.
+
+Definition sem_or (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
+  sem_binarith
+    (fun sg n1 n2 => Some(Vint(Int.or n1 n2)))
+    (fun sg n1 n2 => Some(Vlong(Int64.or n1 n2)))
+    (fun n1 n2 => None)
+    v1 t1 v2 t2.
+
+Definition sem_xor (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
+  sem_binarith
+    (fun sg n1 n2 => Some(Vint(Int.xor n1 n2)))
+    (fun sg n1 n2 => Some(Vlong(Int64.xor n1 n2)))
+    (fun n1 n2 => None)
+    v1 t1 v2 t2.
 
 (** *** Shifts *)
 
+(** Shifts do not perform the usual binary conversions.  Instead,
+  each argument is converted independently, and the signedness
+  of the result is always that of the first argument. *)
+
 Inductive classify_shift_cases : Type:=
-  | shift_case_ii(s: signedness) (**r int , int *)
+  | shift_case_ii(s: signedness)         (**r int , int *)
+  | shift_case_ll(s: signedness)         (**r long, long *)
+  | shift_case_il(s: signedness)         (**r int, long *)
+  | shift_case_li(s: signedness)         (**r long, int *)
   | shift_default.
 
 Definition classify_shift (ty1: type) (ty2: type) :=
   match typeconv ty1, typeconv ty2 with
   | Tint I32 Unsigned _, Tint _ _ _ => shift_case_ii Unsigned
   | Tint _ _ _, Tint _ _ _ => shift_case_ii Signed
+  | Tint I32 Unsigned _, Tlong _ _ => shift_case_il Unsigned
+  | Tint _ _ _, Tlong _ _ => shift_case_il Signed
+  | Tlong s _, Tint _ _ _ => shift_case_li s
+  | Tlong s _, Tlong _ _ => shift_case_ll s
   | _,_  => shift_default
-end.
+  end.
 
-Function sem_shl (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
+Definition sem_shift
+    (sem_int: signedness -> int -> int -> int)
+    (sem_long: signedness -> int64 -> int64 -> int64)
+    (v1: val) (t1: type) (v2: val) (t2: type) : option val :=
   match classify_shift t1 t2 with
   | shift_case_ii sg =>
       match v1, v2 with
-      | Vint n1, Vint n2 =>
-         if Int.ltu n2 Int.iwordsize then Some (Vint(Int.shl n1 n2)) else None
+      | Vint n1, Vint n2 => 
+          if Int.ltu n2 Int.iwordsize
+          then Some(Vint(sem_int sg n1 n2)) else None
+      | _, _ => None
+      end
+  | shift_case_il sg =>
+      match v1, v2 with
+      | Vint n1, Vlong n2 => 
+          if Int64.ltu n2 (Int64.repr 32)
+          then Some(Vint(sem_int sg n1 (Int64.loword n2))) else None
+      | _, _ => None
+      end
+  | shift_case_li sg =>
+      match v1, v2 with
+      | Vlong n1, Vint n2 => 
+          if Int.ltu n2 Int64.iwordsize'
+          then Some(Vlong(sem_long sg n1 (Int64.repr (Int.unsigned n2)))) else None
+      | _, _ => None
+      end
+  | shift_case_ll sg =>
+      match v1, v2 with
+      | Vlong n1, Vlong n2 => 
+          if Int64.ltu n2 Int64.iwordsize
+          then Some(Vlong(sem_long sg n1 n2)) else None
       | _, _ => None
       end
   | shift_default => None
   end.
 
-Function sem_shr (v1: val) (t1: type) (v2: val) (t2: type): option val :=
-  match classify_shift t1 t2 with 
-  | shift_case_ii Unsigned =>
-      match v1,v2 with 
-      | Vint n1, Vint n2 =>
-          if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shru n1 n2)) else None
-      | _,_ => None
-      end
-   | shift_case_ii Signed =>
-      match v1,v2 with
-      | Vint n1,  Vint n2 =>
-          if Int.ltu n2 Int.iwordsize then Some (Vint (Int.shr n1 n2)) else None
-      | _,  _ => None
-      end
-   | shift_default =>
-      None
-   end.
+Definition sem_shl (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
+  sem_shift
+    (fun sg n1 n2 => Int.shl n1 n2)
+    (fun sg n1 n2 => Int64.shl n1 n2)
+    v1 t1 v2 t2.
+
+Definition sem_shr (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
+  sem_shift
+    (fun sg n1 n2 => match sg with Signed => Int.shr n1 n2 | Unsigned => Int.shru n1 n2 end)
+    (fun sg n1 n2 => match sg with Signed => Int64.shr n1 n2 | Unsigned => Int64.shru n1 n2 end)
+    v1 t1 v2 t2.
 
 (** *** Comparisons *)
 
-Inductive classify_cmp_cases : Type:=
-  | cmp_case_ii(s: signedness) (**r int, int *)
-  | cmp_case_pp                (**r pointer, pointer *)
-  | cmp_case_ff                (**r float , float *)
-  | cmp_case_if(s: signedness) (**r int, float *)
-  | cmp_case_fi(s: signedness) (**r float, int *)
-  | cmp_default.
+Inductive classify_cmp_cases : Type :=
+  | cmp_case_pp                       (**r pointer, pointer *)
+  | cmp_default.                      (**r numerical, numerical *)
 
 Definition classify_cmp (ty1: type) (ty2: type) :=
   match typeconv ty1, typeconv ty2 with 
-  | Tint I32 Unsigned _ , Tint _ _ _ => cmp_case_ii Unsigned
-  | Tint _ _ _ , Tint I32 Unsigned _ => cmp_case_ii Unsigned
-  | Tint _ _ _ , Tint _ _ _ => cmp_case_ii Signed
-  | Tfloat _ _ , Tfloat _ _ => cmp_case_ff
-  | Tint _ sg _, Tfloat _ _ => cmp_case_if sg
-  | Tfloat _ _, Tint _ sg _ => cmp_case_fi sg
   | Tpointer _ _ , Tpointer _ _ => cmp_case_pp
   | Tpointer _ _ , Tint _ _ _ => cmp_case_pp
   | Tint _ _ _, Tpointer _ _ => cmp_case_pp
-  | _ , _ => cmp_default
+  | _, _ => cmp_default
   end.
 
-Function sem_cmp (c:comparison)
+Definition sem_cmp (c:comparison)
                   (v1: val) (t1: type) (v2: val) (t2: type)
                   (m: mem): option val :=
   match classify_cmp t1 t2 with
-  | cmp_case_ii Signed =>
-      match v1,v2 with
-      | Vint n1, Vint n2 => Some (Val.of_bool (Int.cmp c n1 n2))
-      | _,  _ => None
-      end
-  | cmp_case_ii Unsigned =>
-      match v1,v2 with
-      | Vint n1, Vint n2 => Some (Val.of_bool (Int.cmpu c n1 n2))
-      | _,  _ => None
-      end
   | cmp_case_pp =>
+     option_map Val.of_bool (Val.cmpu_bool (Mem.valid_pointer m) c v1 v2)
+(*
       match v1,v2 with
       | Vint n1, Vint n2 => Some (Val.of_bool (Int.cmpu c n1 n2))
       | Vptr b1 ofs1,  Vptr b2 ofs2  =>
@@ -752,22 +845,16 @@ Function sem_cmp (c:comparison)
           else None
       | _,  _ => None
       end
-  | cmp_case_ff =>
-      match v1,v2 with
-      | Vfloat f1, Vfloat f2 => Some (Val.of_bool (Float.cmp c f1 f2))  
-      | _,  _ => None
-      end
-  | cmp_case_if sg =>
-      match v1, v2 with
-      | Vint n1, Vfloat n2 => Some (Val.of_bool (Float.cmp c (cast_int_float sg n1) n2))
-      | _, _ => None
-      end
-  | cmp_case_fi sg =>
-      match v1, v2 with
-      | Vfloat n1, Vint n2 => Some (Val.of_bool (Float.cmp c n1 (cast_int_float sg n2)))
-      | _, _ => None
-      end
-  | cmp_default => None
+*)
+  | cmp_default =>
+      sem_binarith
+        (fun sg n1 n2 =>
+            Some(Val.of_bool(match sg with Signed => Int.cmp c n1 n2 | Unsigned => Int.cmpu c n1 n2 end)))
+        (fun sg n1 n2 =>
+            Some(Val.of_bool(match sg with Signed => Int64.cmp c n1 n2 | Unsigned => Int64.cmpu c n1 n2 end)))
+        (fun n1 n2 =>
+            Some(Val.of_bool(Float.cmp c n1 n2)))
+        v1 t1 v2 t2
   end.
 
 (** ** Function applications *)
@@ -821,3 +908,249 @@ Definition sem_incrdecr (id: incr_or_decr) (v: val) (ty: type) :=
   | Incr => sem_add v ty (Vint Int.one) type_int32s
   | Decr => sem_sub v ty (Vint Int.one) type_int32s
   end.
+
+(** * Compatibility with extensions and injections *)
+
+Section GENERIC_INJECTION.
+
+Variable f: meminj.
+Variables m m': mem.
+
+Hypothesis valid_pointer_inj:
+  forall b1 ofs b2 delta,
+  f b1 = Some(b2, delta) ->
+  Mem.valid_pointer m b1 (Int.unsigned ofs) = true ->
+  Mem.valid_pointer m' b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
+
+Hypothesis weak_valid_pointer_inj:
+  forall b1 ofs b2 delta,
+  f b1 = Some(b2, delta) ->
+  Mem.weak_valid_pointer m b1 (Int.unsigned ofs) = true ->
+  Mem.weak_valid_pointer m' b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true.
+
+Hypothesis weak_valid_pointer_no_overflow:
+  forall b1 ofs b2 delta,
+  f b1 = Some(b2, delta) ->
+  Mem.weak_valid_pointer m b1 (Int.unsigned ofs) = true ->
+  0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned.
+
+Hypothesis valid_different_pointers_inj:
+  forall b1 ofs1 b2 ofs2 b1' delta1 b2' delta2,
+  b1 <> b2 ->
+  Mem.valid_pointer m b1 (Int.unsigned ofs1) = true ->
+  Mem.valid_pointer m b2 (Int.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)).
+
+Remark val_inject_vtrue: forall f, val_inject f Vtrue Vtrue.
+Proof. unfold Vtrue; auto. Qed.
+
+Remark val_inject_vfalse: forall f, val_inject f Vfalse Vfalse.
+Proof. unfold Vfalse; auto. Qed.
+
+Remark val_inject_of_bool: forall f b, val_inject f (Val.of_bool b) (Val.of_bool b).
+Proof. intros. unfold Val.of_bool. destruct b; [apply val_inject_vtrue|apply val_inject_vfalse]. 
+Qed.
+
+Hint Resolve val_inject_vtrue val_inject_vfalse val_inject_of_bool.
+
+Ltac TrivialInject :=
+  match goal with
+  | |- exists v', Some ?v = Some v' /\ _ => exists v; split; auto
+  | _ => idtac
+  end.
+
+Lemma sem_unary_operation_inject:
+  forall op v1 ty v tv1,
+  sem_unary_operation op v1 ty = Some v ->
+  val_inject f v1 tv1 ->
+  exists tv, sem_unary_operation op tv1 ty = Some tv /\ val_inject f v tv.
+Proof.
+  unfold sem_unary_operation; intros. destruct op.
+  (* notbool *)
+  unfold sem_notbool in *; destruct (classify_bool ty); inv H0; inv H; TrivialInject.
+  (* notint *)
+  unfold sem_notint in *; destruct (classify_notint ty); inv H0; inv H; TrivialInject.
+  (* neg *)
+  unfold sem_neg in *; destruct (classify_neg ty); inv H0; inv H; TrivialInject.
+Qed.
+
+Definition optval_self_injects (ov: option val) : Prop :=
+  match ov with
+  | Some (Vptr b ofs) => False
+  | _ => True
+  end.
+
+Remark sem_binarith_inject:
+  forall sem_int sem_long sem_float v1 t1 v2 t2 v v1' v2',
+  sem_binarith sem_int sem_long sem_float v1 t1 v2 t2 = Some v ->
+  val_inject f v1 v1' -> val_inject f v2 v2' ->
+  (forall sg n1 n2, optval_self_injects (sem_int sg n1 n2)) ->
+  (forall sg n1 n2, optval_self_injects (sem_long sg n1 n2)) ->
+  (forall n1 n2, optval_self_injects (sem_float n1 n2)) ->
+  exists v', sem_binarith sem_int sem_long sem_float v1' t1 v2' t2 = Some v' /\ val_inject f v v'.
+Proof.
+  intros. 
+  assert (SELF: forall ov v, ov = Some v -> optval_self_injects ov -> val_inject f v v).
+  {
+    intros. subst ov; simpl in H6. destruct v0; contradiction || constructor.
+  }
+  exists v.
+  unfold sem_binarith in *; destruct (classify_binarith t1 t2); inv H0; inv H1; discriminate || eauto.
+Qed.
+
+Remark sem_shift_inject:
+  forall sem_int sem_long v1 t1 v2 t2 v v1' v2',
+  sem_shift sem_int sem_long v1 t1 v2 t2 = Some v ->
+  val_inject f v1 v1' -> val_inject f v2 v2' ->
+  exists v', sem_shift sem_int sem_long v1' t1 v2' t2 = Some v' /\ val_inject f v v'.
+Proof.
+  intros. exists v.
+  unfold sem_shift in *; destruct (classify_shift t1 t2); inv H0; inv H1; try discriminate.
+  destruct (Int.ltu i0 Int.iwordsize); inv H; auto.
+  destruct (Int64.ltu i0 Int64.iwordsize); inv H; auto.
+  destruct (Int64.ltu i0 (Int64.repr 32)); inv H; auto.
+  destruct (Int.ltu i0 Int64.iwordsize'); inv H; auto.
+Qed.
+
+Remark sem_cmp_inj:
+  forall cmp v1 tv1 ty1 v2 tv2 ty2 v,
+  sem_cmp cmp v1 ty1 v2 ty2 m = Some v ->
+  val_inject f v1 tv1 ->
+  val_inject f v2 tv2 ->
+  exists tv, sem_cmp cmp tv1 ty1 tv2 ty2 m' = Some tv /\ val_inject f v tv.
+Proof.
+  intros.
+  unfold sem_cmp in *; destruct (classify_cmp ty1 ty2).
+- (* pointer - pointer *)
+  destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as [b|] eqn:E; simpl in H; inv H.
+  replace (Val.cmpu_bool (Mem.valid_pointer m') cmp tv1 tv2) with (Some b).
+  simpl. TrivialInject. 
+  symmetry. eapply val_cmpu_bool_inject; eauto. 
+- (* numerical - numerical *)
+  assert (SELF: forall b, optval_self_injects (Some (Val.of_bool b))).
+  {
+    destruct b; exact I.
+  }
+  eapply sem_binarith_inject; eauto.
+Qed.
+
+Lemma sem_binary_operation_inj:
+  forall op v1 ty1 v2 ty2 v tv1 tv2,
+  sem_binary_operation op v1 ty1 v2 ty2 m = Some v ->
+  val_inject f v1 tv1 -> val_inject f v2 tv2 ->
+  exists tv, sem_binary_operation op tv1 ty1 tv2 ty2 m' = Some tv /\ val_inject f v tv.
+Proof.
+  unfold sem_binary_operation; intros; destruct op.
+- (* add *)
+  unfold sem_add in *; destruct (classify_add ty1 ty2).
+  + inv H0; inv H1; inv H. TrivialInject. 
+    econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
+  + inv H0; inv H1; inv H. TrivialInject. 
+    econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
+  + inv H0; inv H1; inv H. TrivialInject. 
+    econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
+  + inv H0; inv H1; inv H. TrivialInject. 
+    econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
+  + eapply sem_binarith_inject; eauto; intros; exact I.
+- (* sub *)
+  unfold sem_sub in *; destruct (classify_sub ty1 ty2).
+  + inv H0; inv H1; inv H. TrivialInject.
+    econstructor. eauto. rewrite Int.sub_add_l. auto.
+  + inv H0; inv H1; inv H. TrivialInject.
+    destruct (zeq b1 b0); try discriminate. subst b1. 
+    rewrite H0 in H2; inv H2. rewrite zeq_true. 
+    destruct (Int.eq (Int.repr (sizeof ty)) Int.zero); inv H3.
+    rewrite Int.sub_shifted. TrivialInject.
+  + inv H0; inv H1; inv H. TrivialInject.
+    econstructor. eauto. rewrite Int.sub_add_l. auto.
+  + eapply sem_binarith_inject; eauto; intros; exact I.
+- (* mul *)
+  eapply sem_binarith_inject; eauto; intros; exact I.
+- (* div *)
+  eapply sem_binarith_inject; eauto; intros.
+  destruct sg.
+  destruct (Int.eq n2 Int.zero
+            || Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone); exact I.
+  destruct (Int.eq n2 Int.zero); exact I.
+  destruct sg.
+  destruct (Int64.eq n2 Int64.zero
+            || Int64.eq n1 (Int64.repr Int64.min_signed) && Int64.eq n2 Int64.mone); exact I.
+  destruct (Int64.eq n2 Int64.zero); exact I.
+  exact I.
+- (* mod *)
+  eapply sem_binarith_inject; eauto; intros.
+  destruct sg.
+  destruct (Int.eq n2 Int.zero
+            || Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone); exact I.
+  destruct (Int.eq n2 Int.zero); exact I.
+  destruct sg.
+  destruct (Int64.eq n2 Int64.zero
+            || Int64.eq n1 (Int64.repr Int64.min_signed) && Int64.eq n2 Int64.mone); exact I.
+  destruct (Int64.eq n2 Int64.zero); exact I.
+  exact I.
+- (* and *)
+  eapply sem_binarith_inject; eauto; intros; exact I.
+- (* or *)
+  eapply sem_binarith_inject; eauto; intros; exact I.
+- (* xor *)
+  eapply sem_binarith_inject; eauto; intros; exact I.
+- (* shl *)
+  eapply sem_shift_inject; eauto.
+- (* shr *)
+  eapply sem_shift_inject; eauto.
+  (* comparisons *)
+- eapply sem_cmp_inj; eauto.
+- eapply sem_cmp_inj; eauto.
+- eapply sem_cmp_inj; eauto.
+- eapply sem_cmp_inj; eauto.
+- eapply sem_cmp_inj; eauto.
+- eapply sem_cmp_inj; eauto.
+Qed.
+
+Lemma sem_cast_inject:
+  forall v1 ty1 ty v tv1,
+  sem_cast v1 ty1 ty = Some v ->
+  val_inject f v1 tv1 ->
+  exists tv, sem_cast tv1 ty1 ty = Some tv /\ val_inject f v tv.
+Proof.
+  unfold sem_cast; intros; destruct (classify_cast ty1 ty);
+  inv H0; inv H; TrivialInject.
+- econstructor; eauto. 
+- destruct (cast_float_int si2 f0); inv H1; TrivialInject.
+- destruct (cast_float_long si2 f0); inv H1; TrivialInject.
+- destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H2; TrivialInject. econstructor; eauto.
+- destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H2; TrivialInject. econstructor; eauto.
+- econstructor; eauto.
+Qed.
+
+Lemma bool_val_inject:
+  forall v ty b tv,
+  bool_val v ty = Some b ->
+  val_inject f v tv ->
+  bool_val tv ty = Some b.
+Proof.
+  unfold bool_val; intros. 
+  destruct (classify_bool ty); inv H0; congruence.
+Qed.
+
+End GENERIC_INJECTION.
+
+Lemma sem_binary_operation_inject:
+  forall f m m' op v1 ty1 v2 ty2 v tv1 tv2,
+  sem_binary_operation op v1 ty1 v2 ty2 m = Some v ->
+  val_inject f v1 tv1 -> val_inject f v2 tv2 ->
+  Mem.inject f m m' ->
+  exists tv, sem_binary_operation op tv1 ty1 tv2 ty2 m' = Some tv /\ val_inject f v tv.
+Proof.
+  intros. eapply sem_binary_operation_inj; 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.
+Qed.
+
+
+
diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v
index d0bd9f4..718daa1 100644
--- a/cfrontend/Csharpminor.v
+++ b/cfrontend/Csharpminor.v
@@ -33,7 +33,8 @@ Require Import Smallstep.
 
 Inductive constant : Type :=
   | Ointconst: int -> constant          (**r integer constant *)
-  | Ofloatconst: float -> constant.     (**r floating-point constant *)
+  | Ofloatconst: float -> constant      (**r floating-point constant *)
+  | Olongconst: int64 -> constant.      (**r long integer constant *)
 
 Definition unary_operation : Type := Cminor.unary_operation.
 Definition binary_operation : Type := Cminor.binary_operation.
@@ -238,6 +239,7 @@ Definition eval_constant (cst: constant) : option val :=
   match cst with
   | Ointconst n => Some (Vint n)
   | Ofloatconst n => Some (Vfloat n)
+  | Olongconst n => Some (Vlong n)
   end.
 
 Definition eval_unop := Cminor.eval_unop.
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index 51f89da..2a27852 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -44,7 +44,7 @@ Open Local Scope error_monad_scope.
 -  The C types of the arguments of the operation.  These types
      are used to insert the necessary numeric conversions and to
      resolve operation overloading.
-   Most of these functions return an [option expr], with [None] 
+   Most of these functions return a [res expr], with [Error]
    denoting a case where the operation is not defined at the given types.
 *)
 
@@ -52,6 +52,8 @@ Definition make_intconst (n: int) :=  Econst (Ointconst n).
 
 Definition make_floatconst (f: float) :=  Econst (Ofloatconst f).
 
+Definition make_longconst (f: int64) :=  Econst (Olongconst f).
+
 Definition make_floatofint (e: expr) (sg: signedness) :=
   match sg with
   | Signed => Eunop Ofloatofint e
@@ -64,6 +66,24 @@ Definition make_intoffloat (e: expr) (sg: signedness) :=
   | Unsigned => Eunop Ointuoffloat e
   end.
 
+Definition make_longofint (e: expr) (sg: signedness) :=
+  match sg with
+  | Signed => Eunop Olongofint e
+  | Unsigned => Eunop Olongofintu e
+  end.
+
+Definition make_floatoflong (e: expr) (sg: signedness) :=
+  match sg with
+  | Signed => Eunop Ofloatoflong e
+  | Unsigned => Eunop Ofloatoflongu e
+  end.
+
+Definition make_longoffloat (e: expr) (sg: signedness) :=
+  match sg with
+  | Signed => Eunop Olongoffloat e
+  | Unsigned => Eunop Olonguoffloat e
+  end.
+
 (** [make_boolean e ty] returns a Csharpminor expression that evaluates
    to the boolean value of [e].  *)
 
@@ -80,6 +100,7 @@ Definition make_boolean (e: expr) (ty: type) :=
   | bool_case_i => make_cmp_ne_zero e
   | bool_case_f => Ebinop (Ocmpf Cne) e (make_floatconst Float.zero)
   | bool_case_p => Ebinop (Ocmpu Cne) e (make_intconst Int.zero)
+  | bool_case_l => Ebinop (Ocmpl Cne) e (make_longconst Int64.zero)
   | bool_default => e   (**r should not happen *)
   end.
 
@@ -88,6 +109,7 @@ Definition make_notbool (e: expr) (ty: type) :=
   | bool_case_i => OK (Ebinop (Ocmp Ceq) e (make_intconst Int.zero))
   | bool_case_f => OK (Ebinop (Ocmpf Ceq) e (make_floatconst Float.zero))
   | bool_case_p => OK (Ebinop (Ocmpu Ceq) e (make_intconst Int.zero))
+  | bool_case_l => OK (Ebinop (Ocmpl Ceq) e (make_longconst Int64.zero))
   | _ => Error (msg "Cshmgen.make_notbool")
   end.
 
@@ -95,96 +117,144 @@ Definition make_neg (e: expr) (ty: type) :=
   match classify_neg ty with
   | neg_case_i _ => OK (Eunop Onegint e)
   | neg_case_f => OK (Eunop Onegf e)
+  | neg_case_l _ => OK (Eunop Onegl e)
   | _ => Error (msg "Cshmgen.make_neg")
   end.
 
 Definition make_notint (e: expr) (ty: type) :=
-  Eunop Onotint e.
+  match classify_notint ty with
+  | notint_case_i _ => OK (Eunop Onotint e)
+  | notint_case_l _ => OK (Eunop Onotl e)
+  | _ => Error (msg "Cshmgen.make_notint")
+  end.
+
+Definition make_binarith (iop iopu fop lop lopu: binary_operation)
+                         (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
+  match classify_binarith ty1 ty2 with
+  | bin_case_ii Signed => OK (Ebinop iop e1 e2)
+  | bin_case_ii Unsigned => OK (Ebinop iopu e1 e2)
+  | bin_case_ff => OK (Ebinop fop e1 e2)
+  | bin_case_if sg => OK (Ebinop fop (make_floatofint e1 sg) e2)
+  | bin_case_fi sg => OK (Ebinop fop e1 (make_floatofint e2 sg))
+  | bin_case_ll Signed => OK (Ebinop lop e1 e2)
+  | bin_case_ll Unsigned => OK (Ebinop lopu e1 e2)
+  | bin_case_il sg1 Signed => OK (Ebinop lop (make_longofint e1 sg1) e2)
+  | bin_case_il sg1 Unsigned => OK (Ebinop lopu (make_longofint e1 sg1) e2)
+  | bin_case_li Signed sg2 => OK (Ebinop lop e1 (make_longofint e2 sg2))
+  | bin_case_li Unsigned sg2 => OK (Ebinop lopu e1 (make_longofint e2 sg2))
+  | bin_case_lf sg => OK (Ebinop fop (make_floatoflong e1 sg) e2)
+  | bin_case_fl sg => OK (Ebinop fop e1 (make_floatoflong e2 sg))
+  | bin_default => Error (msg "Cshmgen.make_binarith")
+  end.
 
 Definition make_add (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
   match classify_add ty1 ty2 with
-  | add_case_ii _ => OK (Ebinop Oadd e1 e2)
-  | add_case_ff => OK (Ebinop Oaddf e1 e2)
-  | add_case_if sg => OK (Ebinop Oaddf (make_floatofint e1 sg) e2)
-  | add_case_fi sg => OK (Ebinop Oaddf e1 (make_floatofint e2 sg))
   | add_case_pi ty _ =>
       let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in
       OK (Ebinop Oadd e1 (Ebinop Omul n e2))
   | add_case_ip ty _ =>
       let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in
       OK (Ebinop Oadd e2 (Ebinop Omul n e1))
-  | add_default => Error (msg "Cshmgen.make_add")
+  | add_case_pl ty _ =>
+      let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in
+      OK (Ebinop Oadd e1 (Ebinop Omul n (Eunop Ointoflong e2)))
+  | add_case_lp ty _ =>
+      let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in
+      OK (Ebinop Oadd e2 (Ebinop Omul n (Eunop Ointoflong e1)))
+  | add_default =>
+      make_binarith Oadd Oadd Oaddf Oaddl Oaddl e1 ty1 e2 ty2
   end.
 
 Definition make_sub (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
   match classify_sub ty1 ty2 with
-  | sub_case_ii _ => OK (Ebinop Osub e1 e2)
-  | sub_case_ff => OK (Ebinop Osubf e1 e2)
-  | sub_case_if sg => OK (Ebinop Osubf (make_floatofint e1 sg) e2)
-  | sub_case_fi sg => OK (Ebinop Osubf e1 (make_floatofint e2 sg))
-  | sub_case_pi ty =>
+  | sub_case_pi ty _ =>
       let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in
       OK (Ebinop Osub e1 (Ebinop Omul n e2))
   | sub_case_pp ty =>
       let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in
       OK (Ebinop Odivu (Ebinop Osub e1 e2) n)
-  | sub_default => Error (msg "Cshmgen.make_sub")
+  | sub_case_pl ty _ =>
+      let n := make_intconst (Int.repr (Ctypes.sizeof ty)) in
+      OK (Ebinop Osub e1 (Ebinop Omul n (Eunop Ointoflong e2)))
+  | sub_default =>
+      make_binarith Osub Osub Osubf Osubl Osubl e1 ty1 e2 ty2
   end.
 
 Definition make_mul (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
-  match classify_mul ty1 ty2 with
-  | mul_case_ii _ => OK (Ebinop Omul e1 e2)
-  | mul_case_ff => OK (Ebinop Omulf e1 e2)
-  | mul_case_if sg => OK (Ebinop Omulf (make_floatofint e1 sg) e2)
-  | mul_case_fi sg => OK (Ebinop Omulf e1 (make_floatofint e2 sg))
-  | mul_default => Error (msg "Cshmgen.make_mul")
-  end.
+  make_binarith Omul Omul Omulf Omull Omull e1 ty1 e2 ty2.
 
 Definition make_div (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
-  match classify_div ty1 ty2 with
-  | div_case_ii Unsigned => OK (Ebinop Odivu e1 e2)
-  | div_case_ii Signed => OK (Ebinop Odiv e1 e2)
-  | div_case_ff => OK (Ebinop Odivf e1 e2)
-  | div_case_if sg => OK (Ebinop Odivf (make_floatofint e1 sg) e2)
-  | div_case_fi sg => OK (Ebinop Odivf e1 (make_floatofint e2 sg))
-  | div_default => Error (msg "Cshmgen.make_div")
+  make_binarith Odiv Odivu Odivf Odivl Odivlu e1 ty1 e2 ty2.
+
+Definition make_binarith_int (iop iopu lop lopu: binary_operation)
+                             (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
+  match classify_binarith ty1 ty2 with
+  | bin_case_ii Signed => OK (Ebinop iop e1 e2)
+  | bin_case_ii Unsigned => OK (Ebinop iopu e1 e2)
+  | bin_case_ll Signed => OK (Ebinop lop e1 e2)
+  | bin_case_ll Unsigned => OK (Ebinop lopu e1 e2)
+  | bin_case_il sg1 Signed => OK (Ebinop lop (make_longofint e1 sg1) e2)
+  | bin_case_il sg1 Unsigned => OK (Ebinop lopu (make_longofint e1 sg1) e2)
+  | bin_case_li Signed sg2 => OK (Ebinop lop e1 (make_longofint e2 sg2))
+  | bin_case_li Unsigned sg2 => OK (Ebinop lopu e1 (make_longofint e2 sg2))
+  | _ => Error (msg "Cshmgen.make_binarith_int")
   end.
 
 Definition make_mod (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
-  match classify_binint ty1 ty2 with
-  | binint_case_ii Unsigned => OK (Ebinop Omodu e1 e2)
-  | binint_case_ii Signed => OK (Ebinop Omod e1 e2)
-  | mod_default => Error (msg "Cshmgen.make_mod")
-  end.
+  make_binarith_int Omod Omodu Omodl Omodlu e1 ty1 e2 ty2.
 
 Definition make_and (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
-  OK(Ebinop Oand e1 e2).
+  make_binarith_int Oand Oand Oandl Oandl e1 ty1 e2 ty2.
 
 Definition make_or (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
-  OK(Ebinop Oor e1 e2).
+  make_binarith_int Oor Oor Oorl Oorl e1 ty1 e2 ty2.
 
 Definition make_xor (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
-  OK(Ebinop Oxor e1 e2).
+  make_binarith_int Oxor Oxor Oxorl Oxorl e1 ty1 e2 ty2.
+
+(*
+Definition make_shift (iop iopu lop lopu: binary_operation)
+                      (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
+  match classify_shift ty1 ty2 with
+  | shift_case_ii Signed => OK (Ebinop iop e1 e2)
+  | shift_case_ii Unsigned => OK (Ebinop iopu e1 e2)
+  | shift_case_li Signed => OK (Ebinop lop e1 e2)
+  | shift_case_li Unsigned => OK (Ebinop lopu e1 e2)
+  | shift_case_il Signed => OK (Ebinop iop e1 (Eunop Ointoflong e2))
+  | shift_case_il Unsigned => OK (Ebinop iopu e1 (Eunop Ointoflong e2))
+  | shift_case_ll Signed => OK (Ebinop lop e1 (Eunop Ointoflong e2))
+  | shift_case_ll Unsigned => OK (Ebinop lopu e1 (Eunop Ointoflong e2))
+  | shift_default => Error (msg "Cshmgen.make_shift")
+  end.
+*)
 
 Definition make_shl (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
-  OK(Ebinop Oshl e1 e2).
+  match classify_shift ty1 ty2 with
+  | shift_case_ii _ => OK (Ebinop Oshl e1 e2)
+  | shift_case_li _ => OK (Ebinop Oshll e1 e2)
+  | shift_case_il _ => OK (Ebinop Oshl e1 (Eunop Ointoflong e2))
+  | shift_case_ll _ => OK (Ebinop Oshll e1 (Eunop Ointoflong e2))
+  | shift_default => Error (msg "Cshmgen.make_shl")
+  end.
 
 Definition make_shr (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
   match classify_shift ty1 ty2 with
-  | shift_case_ii Unsigned => OK (Ebinop Oshru e1 e2)
   | shift_case_ii Signed => OK (Ebinop Oshr e1 e2)
-  | shr_default => Error (msg "Cshmgen.make_shr")
+  | shift_case_ii Unsigned => OK (Ebinop Oshru e1 e2)
+  | shift_case_li Signed => OK (Ebinop Oshrl e1 e2)
+  | shift_case_li Unsigned => OK (Ebinop Oshrlu e1 e2)
+  | shift_case_il Signed => OK (Ebinop Oshr e1 (Eunop Ointoflong e2))
+  | shift_case_il Unsigned => OK (Ebinop Oshru e1 (Eunop Ointoflong e2))
+  | shift_case_ll Signed => OK (Ebinop Oshrl e1 (Eunop Ointoflong e2))
+  | shift_case_ll Unsigned => OK (Ebinop Oshrlu e1 (Eunop Ointoflong e2))
+  | shift_default => Error (msg "Cshmgen.make_shr")
   end.
 
 Definition make_cmp (c: comparison) (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
   match classify_cmp ty1 ty2 with
-  | cmp_case_ii Signed => OK (Ebinop (Ocmp c) e1 e2)
-  | cmp_case_ii Unsigned => OK (Ebinop (Ocmpu c) e1 e2)
   | cmp_case_pp => OK (Ebinop (Ocmpu c) e1 e2)
-  | cmp_case_ff => OK (Ebinop (Ocmpf c) e1 e2)
-  | cmp_case_if sg => OK (Ebinop (Ocmpf c) (make_floatofint e1 sg) e2)
-  | cmp_case_fi sg => OK (Ebinop (Ocmpf c) e1 (make_floatofint e2 sg))
-  | cmp_default => Error (msg "Cshmgen.make_cmp")
+  | cmp_default =>
+      make_binarith (Ocmp c) (Ocmpu c) (Ocmpf c) (Ocmpl c) (Ocmplu c) e1 ty1 e2 ty2
   end.
 
 (** [make_cast from to e] applies to [e] the numeric conversions needed
@@ -208,17 +278,23 @@ Definition make_cast_float (e: expr) (sz: floatsize) :=
 
 Definition make_cast (from to: type) (e: expr) :=
   match classify_cast from to with
-  | cast_case_neutral => e
-  | cast_case_i2i sz2 si2 => make_cast_int e sz2 si2
-  | cast_case_f2f sz2 => make_cast_float e sz2
-  | cast_case_i2f si1 sz2 => make_cast_float (make_floatofint e si1) sz2
-  | cast_case_f2i sz2 si2 => make_cast_int (make_intoffloat e si2) sz2 si2
-  | cast_case_f2bool => Ebinop (Ocmpf Cne) e (make_floatconst Float.zero)
-  | cast_case_p2bool => Ebinop (Ocmpu Cne) e (make_intconst Int.zero)
-  | cast_case_struct id1 fld1 id2 fld2 => e
-  | cast_case_union id1 fld1 id2 fld2 => e
-  | cast_case_void => e
-  | cast_case_default => e
+  | cast_case_neutral => OK e
+  | cast_case_i2i sz2 si2 => OK (make_cast_int e sz2 si2)
+  | cast_case_f2f sz2 => OK (make_cast_float e sz2)
+  | cast_case_i2f si1 sz2 => OK (make_cast_float (make_floatofint e si1) sz2)
+  | cast_case_f2i sz2 si2 => OK (make_cast_int (make_intoffloat e si2) sz2 si2)
+  | cast_case_l2l => OK e
+  | cast_case_i2l si1 => OK (make_longofint e si1)
+  | cast_case_l2i sz2 si2 => OK (make_cast_int (Eunop Ointoflong e) sz2 si2)
+  | cast_case_l2f si1 sz2 => OK (make_cast_float (make_floatoflong e si1) sz2)
+  | cast_case_f2l si2 => OK (make_longoffloat e si2)
+  | cast_case_f2bool => OK (Ebinop (Ocmpf Cne) e (make_floatconst Float.zero))
+  | cast_case_l2bool => OK (Ebinop (Ocmpl Cne) e (make_longconst Int64.zero))
+  | cast_case_p2bool => OK (Ebinop (Ocmpu Cne) e (make_intconst Int.zero))
+  | cast_case_struct id1 fld1 id2 fld2 => OK e
+  | cast_case_union id1 fld1 id2 fld2 => OK e
+  | cast_case_void => OK e
+  | cast_case_default => Error (msg "Cshmgen.make_cast")
   end.
 
 (** [make_load addr ty_res] loads a value of type [ty_res] from
@@ -259,7 +335,7 @@ Definition make_store (addr: expr) (ty: type) (rhs: expr) :=
 Definition transl_unop (op: Cop.unary_operation) (a: expr) (ta: type) : res expr :=
   match op with
   | Cop.Onotbool => make_notbool a ta
-  | Cop.Onotint => OK(make_notint a ta)
+  | Cop.Onotint => make_notint a ta
   | Cop.Oneg => make_neg a ta
   end.
 
@@ -297,6 +373,8 @@ Fixpoint transl_expr (a: Clight.expr) {struct a} : res expr :=
       OK(make_intconst n)
   | Clight.Econst_float n _ =>
       OK(make_floatconst n)
+  | Clight.Econst_long n _ =>
+      OK(make_longconst n)
   | Clight.Evar id ty =>
       make_load (Eaddrof id) ty
   | Clight.Etempvar id ty =>
@@ -315,7 +393,7 @@ Fixpoint transl_expr (a: Clight.expr) {struct a} : res expr :=
       transl_binop op tb (typeof b) tc (typeof c)
   | Clight.Ecast b ty =>
       do tb <- transl_expr b;
-      OK (make_cast (typeof b) ty tb)
+      make_cast (typeof b) ty tb
   | Clight.Efield b i ty => 
       match typeof b with
       | Tstruct _ fld _ =>
@@ -369,8 +447,9 @@ Fixpoint transl_arglist (al: list Clight.expr) (tyl: typelist)
   | nil, Tnil => OK nil
   | a1 :: a2, Tcons ty1 ty2 =>
       do ta1 <- transl_expr a1;
-      do ta2 <- transl_arglist a2 ty2;
-      OK (make_cast (typeof a1) ty1 ta1 :: ta2)
+      do ta1' <- make_cast (typeof a1) ty1 ta1;
+      do ta2 <- transl_arglist a2 ty2;      
+      OK (ta1' :: ta2)
   | _, _ =>
       Error(msg "Cshmgen.transl_arglist: arity mismatch")
   end.
@@ -408,7 +487,8 @@ Fixpoint transl_statement (tyret: type) (nbrk ncnt: nat)
   | Clight.Sassign b c =>
       do tb <- transl_lvalue b;
       do tc <- transl_expr c;
-      make_store tb (typeof b) (make_cast (typeof c) (typeof b) tc)
+      do tc' <- make_cast (typeof c) (typeof b) tc;
+      make_store tb (typeof b) tc'
   | Clight.Sset x b =>
       do tb <- transl_expr b;
       OK(Sset x tb)
@@ -442,7 +522,8 @@ Fixpoint transl_statement (tyret: type) (nbrk ncnt: nat)
       OK (Sexit ncnt)
   | Clight.Sreturn (Some e) =>
       do te <- transl_expr e;
-      OK (Sreturn (Some (make_cast (typeof e) tyret te)))
+      do te' <- make_cast (typeof e) tyret te;
+      OK (Sreturn (Some te'))
   | Clight.Sreturn None =>
       OK (Sreturn None)
   | Clight.Sswitch a sl =>
@@ -486,9 +567,6 @@ Definition transl_function (f: Clight.function) : res function :=
        (map fst (Clight.fn_temps f))
        tbody).
 
-Definition list_typ_eq: forall (l1 l2: list typ), {l1=l2} + {l1<>l2}
-                     := list_eq_dec typ_eq.
-
 Definition transl_fundef (f: Clight.fundef) : res fundef :=
   match f with
   | Clight.Internal g => 
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index ad5ada6..7c24d0d 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -67,157 +67,10 @@ Proof.
   rewrite H0; reflexivity.
 Qed.
 
-(*
-Lemma var_kind_by_value:
-  forall ty chunk,
-  access_mode ty = By_value chunk ->
-  var_kind_of_type ty = OK(Vscalar chunk).
-Proof.
-  intros ty chunk; destruct ty; simpl; try congruence.
-  destruct i; try congruence; destruct s; congruence.
-  destruct f; congruence.
-Qed.
-
-Lemma var_kind_by_reference:
-  forall ty vk,
-  access_mode ty = By_reference \/ access_mode ty = By_copy ->
-  var_kind_of_type ty = OK vk ->
-  vk = Varray (Ctypes.sizeof ty) (Ctypes.alignof ty).
-Proof.
-  intros ty vk; destruct ty; simpl; try intuition congruence.
-  destruct i; try congruence; destruct s; intuition congruence.
-  destruct f; intuition congruence.
-Qed.
-
-Lemma sizeof_var_kind_of_type:
-  forall ty vk,
-  var_kind_of_type ty = OK vk ->
-  Csharpminor.sizeof vk = Ctypes.sizeof ty.
-Proof.
-  intros ty vk.
-  assert (sizeof (Varray (Ctypes.sizeof ty) (Ctypes.alignof ty)) = Ctypes.sizeof ty).
-    simpl. rewrite Zmax_spec. apply zlt_false. 
-    generalize (Ctypes.sizeof_pos ty). omega.
-  destruct ty; try (destruct i; try destruct s); try (destruct f); 
-  simpl; intro EQ; inversion EQ; subst vk; auto.
-Qed.
-*)
-(****
-Remark cast_int_int_normalized:
-  forall sz si a chunk n,
-  access_mode (Tint sz si a) = By_value chunk ->
-  val_normalized (Vint (cast_int_int sz si n)) chunk.
-Proof.
-  unfold access_mode, cast_int_int, val_normalized; intros. destruct sz.
-  destruct si; inv H; simpl.
-  rewrite Int.sign_ext_idem; auto. compute; auto.
-  rewrite Int.zero_ext_idem; auto. compute; auto.
-  destruct si; inv H; simpl.
-  rewrite Int.sign_ext_idem; auto. compute; auto.
-  rewrite Int.zero_ext_idem; auto. compute; auto.
-  inv H. auto.
-  inv H. destruct (Int.eq n Int.zero); auto.
-Qed.
-
-Remark cast_float_float_normalized:
-  forall sz a chunk n,
-  access_mode (Tfloat sz a) = By_value chunk ->
-  val_normalized (Vfloat (cast_float_float sz n)) chunk.
-Proof.
-  unfold access_mode, cast_float_float, val_normalized; intros. 
-  destruct sz; inv H; simpl.
-  rewrite Float.singleoffloat_idem. auto.
-  auto.
-Qed.
-
-Remark cast_neutral_normalized:
-  forall ty1 ty2 chunk,
-  classify_cast ty1 ty2 = cast_case_neutral ->
-  access_mode ty2 = By_value chunk ->
-  chunk = Mint32.
-Proof.
-  intros. functional inversion H; subst; simpl in H0; congruence.
-Qed.
-
-Remark cast_to_bool_normalized:
-  forall ty1 ty2 chunk,
-  classify_cast ty1 ty2 = cast_case_f2bool \/
-  classify_cast ty1 ty2 = cast_case_p2bool ->
-  access_mode ty2 = By_value chunk ->
-  chunk = Mint8unsigned.
-Proof.
-  intros. destruct ty2; simpl in *; try discriminate. 
-  destruct i; destruct ty1; intuition congruence. 
-  destruct ty1; intuition discriminate.
-  destruct ty1; intuition discriminate.
-Qed.
-
-Lemma cast_result_normalized:
-  forall chunk v1 ty1 ty2 v2,
-  sem_cast v1 ty1 ty2 = Some v2 ->
-  access_mode ty2 = By_value chunk ->
-  val_normalized v2 chunk.
-Proof.
-  intros. functional inversion H; subst.
-  rewrite (cast_neutral_normalized ty1 ty2 chunk); auto. red; auto.
-  rewrite (cast_neutral_normalized ty1 ty2 chunk); auto. red; auto.
-  functional inversion H2; subst. eapply cast_int_int_normalized; eauto.
-  functional inversion H2; subst. eapply cast_float_float_normalized; eauto.
-  functional inversion H2; subst. eapply cast_float_float_normalized; eauto.
-  functional inversion H2; subst. eapply cast_int_int_normalized; eauto.
-  rewrite (cast_to_bool_normalized ty1 ty2 chunk); auto. red; auto.
-  rewrite (cast_to_bool_normalized ty1 ty2 chunk); auto. red; auto.
-  rewrite (cast_to_bool_normalized ty1 ty2 chunk); auto. destruct (Int.eq i Int.zero); red; auto.
-  rewrite (cast_to_bool_normalized ty1 ty2 chunk); auto. red; auto.
-  functional inversion H2; subst. simpl in H0. congruence.
-  functional inversion H2; subst. simpl in H0. congruence.
-  functional inversion H5; subst. simpl in H0. congruence.
-Qed.
-
-Definition val_casted (v: val) (ty: type) : Prop :=
-  exists v0, exists ty0, sem_cast v0 ty0 ty = Some v.
-
-Lemma val_casted_normalized:
-  forall v ty chunk,
-  val_casted v ty -> access_mode ty = By_value chunk -> val_normalized v chunk.
-Proof.
-  intros. destruct H as [v0 [ty0 CAST]]. eapply cast_result_normalized; eauto.
-Qed.
-
-Fixpoint val_casted_list (vl: list val) (tyl: typelist) {struct vl}: Prop :=
-  match vl, tyl with
-  | nil, Tnil => True
-  | v1 :: vl', Tcons ty1 tyl' => val_casted v1 ty1 /\ val_casted_list vl' tyl'
-  | _, _ => False
-  end.
-
-Lemma eval_exprlist_casted:
-  forall ge e le m al tyl vl,
-  Clight.eval_exprlist ge e le m al tyl vl ->
-  val_casted_list vl tyl.
-Proof.
-  induction 1; simpl.
-  auto.
-  split. exists v1; exists (typeof a); auto. eauto.
-Qed.
-
-*******)
-
 (** * Properties of the translation functions *)
 
 (** Transformation of expressions and statements. *)
 
-(*
-Lemma is_variable_correct:
-  forall a id,
-  is_variable a = Some id ->
-  a = Clight.Evar id (typeof a).
-Proof.
-  intros until id. unfold is_variable; destruct a; intros; try discriminate.
-  simpl. congruence.
-Qed.
-*)
-
 Lemma transl_expr_lvalue:
   forall ge e le m a loc ofs ta,
   Clight.eval_lvalue ge e le m a loc ofs ->
@@ -283,6 +136,13 @@ Proof.
   intros. unfold make_floatconst. econstructor. reflexivity. 
 Qed.
 
+Lemma make_longconst_correct:
+  forall n e le m,
+  eval_expr ge e le m (make_longconst n) (Vlong n).
+Proof.
+  intros. unfold make_floatconst. econstructor. reflexivity. 
+Qed.
+
 Lemma make_floatofint_correct:
   forall a n sg e le m,
   eval_expr ge e le m a (Vint n) ->
@@ -302,8 +162,38 @@ Proof.
   destruct sg; econstructor; eauto; simpl; rewrite H0; auto.
 Qed.
 
-Hint Resolve make_intconst_correct make_floatconst_correct
+Lemma make_longofint_correct:
+  forall a n sg e le m,
+  eval_expr ge e le m a (Vint n) ->
+  eval_expr ge e le m (make_longofint a sg) (Vlong(cast_int_long sg n)).
+Proof.
+  intros. unfold make_longofint, cast_int_long. 
+  destruct sg; econstructor; eauto. 
+Qed.
+
+Lemma make_floatoflong_correct:
+  forall a n sg e le m,
+  eval_expr ge e le m a (Vlong n) ->
+  eval_expr ge e le m (make_floatoflong a sg) (Vfloat(cast_long_float sg n)).
+Proof.
+  intros. unfold make_floatoflong, cast_int_long. 
+  destruct sg; econstructor; eauto. 
+Qed.
+
+Lemma make_longoffloat_correct:
+  forall e le m a sg f i,
+  eval_expr ge e le m a (Vfloat f) ->
+  cast_float_long sg f = Some i ->
+  eval_expr ge e le m (make_longoffloat a sg) (Vlong i).
+Proof.
+  unfold cast_float_long, make_longoffloat; intros.
+  destruct sg; econstructor; eauto; simpl; rewrite H0; auto.
+Qed.
+
+Hint Resolve make_intconst_correct make_floatconst_correct make_longconst_correct
              make_floatofint_correct make_intoffloat_correct
+             make_longofint_correct
+             make_floatoflong_correct make_longoffloat_correct
              eval_Eunop eval_Ebinop: cshm.
 Hint Extern 2 (@eq trace _ _) => traceEq: cshm.
 
@@ -357,38 +247,34 @@ Qed.
 Hint Resolve make_cast_int_correct make_cast_float_correct: cshm.
 
 Lemma make_cast_correct:
-  forall e le m a v ty1 ty2 v',
+  forall e le m a b v ty1 ty2 v',
+  make_cast ty1 ty2 a = OK b ->
   eval_expr ge e le m a v ->
   sem_cast v ty1 ty2 = Some v' ->
-  eval_expr ge e le m (make_cast ty1 ty2 a) v'.
+  eval_expr ge e le m b v'.
 Proof.
-  intros. unfold make_cast. functional inversion H0; subst.
-  (* neutral *)
-  rewrite H2; auto.
-  rewrite H2; auto.
-  (* int -> int *)
-  rewrite H2. auto with cshm. 
-  (* float -> float *)
-  rewrite H2. auto with cshm.
-  (* int -> float *)
-  rewrite H2. auto with cshm. 
+  intros. unfold make_cast, sem_cast in *;
+  destruct (classify_cast ty1 ty2); inv H; destruct v; inv H1; eauto with cshm.
   (* float -> int *)
-  rewrite H2. eauto with cshm.
+  destruct (cast_float_int si2 f) as [i|] eqn:E; inv H2. eauto with cshm.
+  (* float -> long *)
+  destruct (cast_float_long si2 f) as [i|] eqn:E; inv H2. eauto with cshm.
   (* float -> bool *)
-  rewrite H2. econstructor; eauto with cshm.
-  simpl. unfold Val.cmpf, Val.cmpf_bool. rewrite Float.cmp_ne_eq. rewrite H7; auto.
-  rewrite H2. econstructor; eauto with cshm.
-  simpl. unfold Val.cmpf, Val.cmpf_bool. rewrite Float.cmp_ne_eq. rewrite H7; auto.
-  (* pointer -> bool *)
-  rewrite H2. econstructor; eauto with cshm.
-  simpl. unfold Val.cmpu, Val.cmpu_bool, Int.cmpu. destruct (Int.eq i Int.zero); reflexivity.
-  rewrite H2. econstructor; eauto with cshm.
-  (* struct -> struct *)
-  rewrite H2. auto.
-  (* union -> union *)
-  rewrite H2. auto.
-  (* any -> void *)
-  rewrite H5. auto.
+  econstructor; eauto with cshm.
+  simpl. unfold Val.cmpf, Val.cmpf_bool. rewrite Float.cmp_ne_eq.
+  destruct (Float.cmp Ceq f Float.zero); auto.
+  (* long -> bool *)
+  econstructor; eauto with cshm.
+  simpl. unfold Val.cmpl, Val.cmpl_bool, Int64.cmp.
+  destruct (Int64.eq i Int64.zero); auto.
+  (* int -> bool *)
+  econstructor; eauto with cshm.
+  simpl. unfold Val.cmpu, Val.cmpu_bool, Int.cmpu.
+  destruct (Int.eq i Int.zero); auto.
+  (* struct *)
+  destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H2; auto.
+  (* union *)
+  destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H2; auto.
 Qed.
 
 Lemma make_boolean_correct:
@@ -413,6 +299,10 @@ Proof.
   unfold Val.cmpu, Val.cmpu_bool. simpl.
   destruct (Int.eq i Int.zero); simpl; constructor.
   exists Vtrue; split. econstructor; eauto with cshm. constructor.
+(* long *)
+  econstructor; split. econstructor; eauto with cshm. simpl. eauto. 
+  unfold Val.cmpl, Val.cmpl_bool. simpl. 
+  destruct (Int64.eq i Int64.zero); simpl; constructor. 
 Qed.
 
 Lemma make_neg_correct:
@@ -422,10 +312,8 @@ Lemma make_neg_correct:
   eval_expr ge e le m a va ->
   eval_expr ge e le m c v.
 Proof.
-  intros until m; intro SEM. unfold make_neg. 
-  functional inversion SEM; intros.
-  rewrite H0 in H4. inv H4. eapply eval_Eunop; eauto with cshm.
-  rewrite H0 in H4. inv H4. eauto with cshm.
+  unfold sem_neg, make_neg; intros until m; intros SEM MAKE EV1;
+  destruct (classify_neg tya); inv MAKE; destruct va; inv SEM; eauto with cshm.
 Qed.
 
 Lemma make_notbool_correct:
@@ -435,20 +323,19 @@ Lemma make_notbool_correct:
   eval_expr ge e le m a va ->
   eval_expr ge e le m c v.
 Proof.
-  intros until m; intro SEM. unfold make_notbool. 
-  functional inversion SEM; intros; rewrite H0 in H4; inversion H4; simpl;
-  eauto with cshm.
+  unfold sem_notbool, make_notbool; intros until m; intros SEM MAKE EV1;
+  destruct (classify_bool tya); inv MAKE; destruct va; inv SEM; eauto with cshm.
 Qed.
 
 Lemma make_notint_correct:
   forall a tya c va v e le m,
   sem_notint va tya = Some v ->
-  make_notint a tya = c ->  
+  make_notint a tya = OK c ->  
   eval_expr ge e le m a va ->
   eval_expr ge e le m c v.
 Proof.
-  intros until m; intro SEM. unfold make_notint. 
-  functional inversion SEM; intros. subst. eauto with cshm. 
+  unfold sem_notint, make_notint; intros until m; intros SEM MAKE EV1;
+  destruct (classify_notint tya); inv MAKE; destruct va; inv SEM; eauto with cshm.
 Qed.
 
 Definition binary_constructor_correct
@@ -461,99 +348,206 @@ Definition binary_constructor_correct
   eval_expr ge e le m b vb ->
   eval_expr ge e le m c v.
 
+Section MAKE_BIN.
+
+Variable sem_int: signedness -> int -> int -> option val.
+Variable sem_long: signedness -> int64 -> int64 -> option val.
+Variable sem_float: float -> float -> option val.
+Variables iop iopu fop lop lopu: binary_operation.
+
+Hypothesis iop_ok:
+  forall x y m, eval_binop iop (Vint x) (Vint y) m = sem_int Signed x y.
+Hypothesis iopu_ok:
+  forall x y m, eval_binop iopu (Vint x) (Vint y) m = sem_int Unsigned x y.
+Hypothesis lop_ok:
+  forall x y m, eval_binop lop (Vlong x) (Vlong y) m = sem_long Signed x y.
+Hypothesis lopu_ok:
+  forall x y m, eval_binop lopu (Vlong x) (Vlong y) m = sem_long Unsigned x y.
+Hypothesis fop_ok:
+  forall x y m, eval_binop fop (Vfloat x) (Vfloat y) m = sem_float x y.
+
+Lemma make_binarith_correct:
+  binary_constructor_correct
+    (make_binarith iop iopu fop lop lopu)
+    (sem_binarith sem_int sem_long sem_float).
+Proof.
+  red; unfold make_binarith, sem_binarith;
+  intros until m; intros SEM MAKE EV1 EV2;
+  destruct (classify_binarith tya tyb); inv MAKE;
+  destruct va; try discriminate; destruct vb; try discriminate.
+- destruct s; inv H0; econstructor; eauto with cshm. 
+  rewrite iop_ok; auto. rewrite iopu_ok; auto.
+- erewrite <- fop_ok in SEM; eauto with cshm.
+- erewrite <- fop_ok in SEM; eauto with cshm.
+- erewrite <- fop_ok in SEM; eauto with cshm.
+- destruct s; inv H0; econstructor; eauto with cshm. 
+  rewrite lop_ok; auto. rewrite lopu_ok; auto.
+- destruct s2; inv H0; econstructor; eauto with cshm. 
+  rewrite lop_ok; auto. rewrite lopu_ok; auto.
+- destruct s1; inv H0; econstructor; eauto with cshm. 
+  rewrite lop_ok; auto. rewrite lopu_ok; auto.
+- erewrite <- fop_ok in SEM; eauto with cshm.
+- erewrite <- fop_ok in SEM; eauto with cshm.
+Qed.
+
+Lemma make_binarith_int_correct:
+  binary_constructor_correct
+    (make_binarith_int iop iopu lop lopu)
+    (sem_binarith sem_int sem_long (fun x y => None)).
+Proof.
+  red; unfold make_binarith_int, sem_binarith;
+  intros until m; intros SEM MAKE EV1 EV2;
+  destruct (classify_binarith tya tyb); inv MAKE;
+  destruct va; try discriminate; destruct vb; try discriminate.
+- destruct s; inv H0; econstructor; eauto with cshm. 
+  rewrite iop_ok; auto. rewrite iopu_ok; auto.
+- destruct s; inv H0; econstructor; eauto with cshm. 
+  rewrite lop_ok; auto. rewrite lopu_ok; auto.
+- destruct s2; inv H0; econstructor; eauto with cshm. 
+  rewrite lop_ok; auto. rewrite lopu_ok; auto.
+- destruct s1; inv H0; econstructor; eauto with cshm. 
+  rewrite lop_ok; auto. rewrite lopu_ok; auto.
+Qed.
+
+End MAKE_BIN.
+
+Hint Extern 2 (@eq (option val) _ _) => (simpl; reflexivity) : cshm.
+
 Lemma make_add_correct: binary_constructor_correct make_add sem_add.
 Proof.
-  red; intros until m. intro SEM. unfold make_add. 
-  functional inversion SEM; rewrite H0; intros;
-  inversion H7; eauto with cshm. 
-  eapply eval_Ebinop. eauto. 
-  eapply eval_Ebinop. eauto with cshm. eauto.
-  simpl. reflexivity. reflexivity. 
-  eapply eval_Ebinop. eauto. 
-  eapply eval_Ebinop. eauto with cshm. eauto. 
-  simpl. reflexivity. simpl. reflexivity.
+  red; unfold make_add, sem_add;
+  intros until m; intros SEM MAKE EV1 EV2;
+  destruct (classify_add tya tyb); inv MAKE.
+- destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
+- destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
+- destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
+- destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
+- eapply make_binarith_correct; eauto; intros; auto.
 Qed.
 
 Lemma make_sub_correct: binary_constructor_correct make_sub sem_sub.
 Proof.
-  red; intros until m. intro SEM. unfold make_sub. 
-  functional inversion SEM; rewrite H0; intros;
-  inversion H7; eauto with cshm. 
-  eapply eval_Ebinop. eauto. 
-  eapply eval_Ebinop. eauto with cshm. eauto.
-  simpl. reflexivity. reflexivity. 
-  inversion H9. eapply eval_Ebinop. 
-  eapply eval_Ebinop; eauto. 
-  simpl. unfold eq_block; rewrite H3. reflexivity.
-  eauto with cshm. simpl. rewrite H8. reflexivity.
+  red; unfold make_sub, sem_sub;
+  intros until m; intros SEM MAKE EV1 EV2;
+  destruct (classify_sub tya tyb); inv MAKE.
+- destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
+- destruct va; try discriminate; destruct vb; inv SEM.
+  destruct (zeq b0 b1); try discriminate. destruct (Int.eq (Int.repr (sizeof ty)) Int.zero) eqn:E; inv H0.
+  econstructor; eauto with cshm. rewrite zeq_true. simpl. rewrite E; auto. 
+- destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
+- eapply make_binarith_correct; eauto; intros; auto.
 Qed.
 
 Lemma make_mul_correct: binary_constructor_correct make_mul sem_mul.
 Proof.
-  red; intros until m. intro SEM. unfold make_mul. 
-  functional inversion SEM; rewrite H0; intros;
-  inversion H7; eauto with cshm. 
+  apply make_binarith_correct; intros; auto.
 Qed.
 
 Lemma make_div_correct: binary_constructor_correct make_div sem_div.
 Proof.
-  red; intros until m. intro SEM. unfold make_div. 
-  functional inversion SEM; rewrite H0; intros.
-  inversion H8. eapply eval_Ebinop; eauto with cshm. 
-  simpl. rewrite H7; auto.
-  inversion H8. eapply eval_Ebinop; eauto with cshm. 
-  simpl. rewrite H7; auto.
-  inversion H7; eauto with cshm. 
-  inversion H7; eauto with cshm. 
-  inversion H7; eauto with cshm. 
+  apply make_binarith_correct; intros; auto.
 Qed.
 
 Lemma make_mod_correct: binary_constructor_correct make_mod sem_mod.
-  red; intros until m. intro SEM. unfold make_mod. 
-  functional inversion SEM; rewrite H0; intros.
-  inversion H8. eapply eval_Ebinop; eauto with cshm. 
-  simpl. rewrite H7; auto.
-  inversion H8. eapply eval_Ebinop; eauto with cshm. 
-  simpl. rewrite H7; auto.
+Proof.
+  apply make_binarith_int_correct; intros; auto.
 Qed.
 
 Lemma make_and_correct: binary_constructor_correct make_and sem_and.
 Proof.
-  red; intros until m. intro SEM. unfold make_and. 
-  functional inversion SEM. intros. inversion H7. 
-  eauto with cshm. 
+  apply make_binarith_int_correct; intros; auto.
 Qed.
 
 Lemma make_or_correct: binary_constructor_correct make_or sem_or.
 Proof.
-  red; intros until m. intro SEM. unfold make_or. 
-  functional inversion SEM. intros. inversion H7. 
-  eauto with cshm. 
+  apply make_binarith_int_correct; intros; auto.
 Qed.
 
 Lemma make_xor_correct: binary_constructor_correct make_xor sem_xor.
 Proof.
-  red; intros until m. intro SEM. unfold make_xor. 
-  functional inversion SEM. intros. inversion H7. 
-  eauto with cshm. 
+  apply make_binarith_int_correct; intros; auto.
+Qed.
+
+Ltac comput val :=
+  let x := fresh in set val as x in *; vm_compute in x; subst x.
+
+Remark small_shift_amount_1:
+  forall i,
+  Int64.ltu i Int64.iwordsize = true ->
+  Int.ltu (Int64.loword i) Int64.iwordsize' = true
+  /\ Int64.unsigned i = Int.unsigned (Int64.loword i).
+Proof.
+  intros. apply Int64.ltu_inv in H. comput (Int64.unsigned Int64.iwordsize). 
+  assert (Int64.unsigned i = Int.unsigned (Int64.loword i)).
+  {
+    unfold Int64.loword. rewrite Int.unsigned_repr; auto. 
+    comput Int.max_unsigned; omega.
+  }
+  split; auto. unfold Int.ltu. apply zlt_true. rewrite <- H0. tauto.
+Qed.
+
+Remark small_shift_amount_2:
+  forall i,
+  Int64.ltu i (Int64.repr 32) = true ->
+  Int.ltu (Int64.loword i) Int.iwordsize = true.
+Proof.
+  intros. apply Int64.ltu_inv in H. comput (Int64.unsigned (Int64.repr 32)).
+  assert (Int64.unsigned i = Int.unsigned (Int64.loword i)).
+  {
+    unfold Int64.loword. rewrite Int.unsigned_repr; auto. 
+    comput Int.max_unsigned; omega.
+  }
+  unfold Int.ltu. apply zlt_true. rewrite <- H0. tauto.
+Qed.
+
+Lemma small_shift_amount_3:
+  forall i,
+  Int.ltu i Int64.iwordsize' = true ->
+  Int64.unsigned (Int64.repr (Int.unsigned i)) = Int.unsigned i.
+Proof.
+  intros. apply Int.ltu_inv in H. comput (Int.unsigned Int64.iwordsize'). 
+  apply Int64.unsigned_repr. comput Int64.max_unsigned; omega.
 Qed.
 
 Lemma make_shl_correct: binary_constructor_correct make_shl sem_shl.
 Proof.
-  red; intros until m. intro SEM. unfold make_shl. 
-  functional inversion SEM. intros. inversion H8. 
-  eapply eval_Ebinop; eauto with cshm. 
-  simpl. rewrite H7. auto.
+  red; unfold make_shl, sem_shl, sem_shift;
+  intros until m; intros SEM MAKE EV1 EV2;
+  destruct (classify_shift tya tyb); inv MAKE;
+  destruct va; try discriminate; destruct vb; try discriminate.
+- destruct (Int.ltu i0 Int.iwordsize) eqn:E; inv SEM.
+  econstructor; eauto. simpl; rewrite E; auto.
+- destruct (Int64.ltu i0 Int64.iwordsize) eqn:E; inv SEM.
+  exploit small_shift_amount_1; eauto. intros [A B].
+  econstructor; eauto with cshm. simpl. rewrite A. 
+  f_equal; f_equal. unfold Int64.shl', Int64.shl. rewrite B; auto.
+- destruct (Int64.ltu i0 (Int64.repr 32)) eqn:E; inv SEM.
+  econstructor; eauto with cshm. simpl. rewrite small_shift_amount_2; auto. 
+- destruct (Int.ltu i0 Int64.iwordsize') eqn:E; inv SEM. 
+  econstructor; eauto with cshm. simpl. rewrite E. 
+  unfold Int64.shl', Int64.shl. rewrite small_shift_amount_3; auto.
 Qed.
 
 Lemma make_shr_correct: binary_constructor_correct make_shr sem_shr.
 Proof.
-  red; intros until m. intro SEM. unfold make_shr. 
-  functional inversion SEM; intros; rewrite H0 in H8; inversion H8.
-  eapply eval_Ebinop; eauto with cshm.
-  simpl; rewrite H7; auto.
-  eapply eval_Ebinop; eauto with cshm.
-  simpl; rewrite H7; auto.
+  red; unfold make_shr, sem_shr, sem_shift;
+  intros until m; intros SEM MAKE EV1 EV2;
+  destruct (classify_shift tya tyb); inv MAKE;
+  destruct va; try discriminate; destruct vb; try discriminate.
+- destruct (Int.ltu i0 Int.iwordsize) eqn:E; inv SEM.
+  destruct s; inv H0; econstructor; eauto; simpl; rewrite E; auto.
+- destruct (Int64.ltu i0 Int64.iwordsize) eqn:E; inv SEM.
+  exploit small_shift_amount_1; eauto. intros [A B].
+  destruct s; inv H0; econstructor; eauto with cshm; simpl; rewrite A;
+  f_equal; f_equal.
+  unfold Int64.shr', Int64.shr; rewrite B; auto.
+  unfold Int64.shru', Int64.shru; rewrite B; auto.
+- destruct (Int64.ltu i0 (Int64.repr 32)) eqn:E; inv SEM.
+  destruct s; inv H0; econstructor; eauto with cshm; simpl; rewrite small_shift_amount_2; auto. 
+- destruct (Int.ltu i0 Int64.iwordsize') eqn:E; inv SEM.
+  destruct s; inv H0; econstructor; eauto with cshm; simpl; rewrite E. 
+  unfold Int64.shr', Int64.shr; rewrite small_shift_amount_3; auto.
+  unfold Int64.shru', Int64.shru; rewrite small_shift_amount_3; auto.
 Qed.
 
 Lemma make_cmp_correct:
@@ -564,35 +558,12 @@ Lemma make_cmp_correct:
   eval_expr ge e le m b vb ->
   eval_expr ge e le m c v.
 Proof.
-  intros until m. intro SEM. unfold make_cmp.
-  functional inversion SEM; rewrite H0; intros.
-  (** ii Signed *)
-  inversion H8; eauto with cshm.
-  (* ii Unsigned *) 
-  inversion H8. eauto with cshm.
-  (* pp int int *)
-  inversion H8. eauto with cshm.
-  (* pp ptr ptr *)
-  inversion H10. eapply eval_Ebinop; eauto with cshm.
-  simpl. unfold Val.cmpu. simpl. unfold Mem.weak_valid_pointer in *. 
-  rewrite H3. rewrite H9. auto.
-  inversion H10. eapply eval_Ebinop; eauto with cshm.
-  simpl. unfold Val.cmpu. simpl. rewrite H3. rewrite H9.
-  destruct cmp; simpl in *; inv H; auto.
-  (* pp ptr int *)
-  inversion H9. eapply eval_Ebinop; eauto with cshm.
-  simpl. unfold Val.cmpu. simpl. rewrite H8.
-  destruct cmp; simpl in *; inv H; auto.
-  (* pp int ptr *)
-  inversion H9. eapply eval_Ebinop; eauto with cshm.
-  simpl. unfold Val.cmpu. simpl. rewrite H8.
-  destruct cmp; simpl in *; inv H; auto.
-  (* ff *)
-  inversion H8. eauto with cshm.
-  (* if *)
-  inversion H8. eauto with cshm.
-  (* fi *)
-  inversion H8. eauto with cshm.
+  unfold sem_cmp, make_cmp; intros until m; intros SEM MAKE EV1 EV2;
+  destruct (classify_cmp tya tyb).
+- inv MAKE. destruct (Val.cmpu_bool (Mem.valid_pointer m) cmp va vb) as [bv|] eqn:E;
+  simpl in SEM; inv SEM.
+  econstructor; eauto. simpl. unfold Val.cmpu. rewrite E. auto.
+- eapply make_binarith_correct; eauto; intros; auto.
 Qed.
 
 Lemma transl_unop_correct:
@@ -604,7 +575,7 @@ Lemma transl_unop_correct:
 Proof.
   intros. destruct op; simpl in *.
   eapply make_notbool_correct; eauto. 
-  eapply make_notint_correct with (tya := tya); eauto. congruence.
+  eapply make_notint_correct; eauto. 
   eapply make_neg_correct; eauto.
 Qed.
 
@@ -903,6 +874,8 @@ Proof.
   apply make_intconst_correct.
 (* const float *)
   apply make_floatconst_correct.
+(* const long *)
+  apply make_longconst_correct.
 (* temp var *)
   constructor; auto.
 (* addrof *)
@@ -957,8 +930,7 @@ Proof.
   induction 1; intros.
   monadInv H. constructor.
   monadInv H2. constructor. 
-  eapply make_cast_correct. eapply transl_expr_correct; eauto. auto. 
-  eauto.
+  eapply make_cast_correct; eauto. eapply transl_expr_correct; eauto. auto. 
 Qed.
 
 End EXPR.
@@ -1103,8 +1075,8 @@ Proof.
 (* skip *)
   auto.
 (* assign *)
-  unfold make_store, make_memcpy in EQ2.
-  destruct (access_mode (typeof e)); inv EQ2; auto.
+  unfold make_store, make_memcpy in EQ3.
+  destruct (access_mode (typeof e)); inv EQ3; auto.
 (* set *)
   auto.
 (* call *)
@@ -1196,7 +1168,7 @@ Proof.
   monadInv TR.
   assert (SAME: ts' = ts /\ tk' = tk).
     inversion MTR. auto. 
-    subst ts. unfold make_store, make_memcpy in EQ2. destruct (access_mode (typeof a1)); congruence.
+    subst ts. unfold make_store, make_memcpy in EQ3. destruct (access_mode (typeof a1)); congruence.
   destruct SAME; subst ts' tk'.
   econstructor; split.
   apply plus_one. eapply make_store_correct; eauto.
@@ -1327,7 +1299,7 @@ Proof.
   monadInv TR. inv MTR. 
   econstructor; split.
   apply plus_one. constructor.
-  eapply make_cast_correct. eapply transl_expr_correct; eauto. eauto.
+  eapply make_cast_correct; eauto. eapply transl_expr_correct; eauto.
   eapply match_env_free_blocks; eauto.
   econstructor; eauto.
   eapply match_cont_call_cont. eauto. 
diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v
index c05f21a..bf483a0 100644
--- a/cfrontend/Ctypes.v
+++ b/cfrontend/Ctypes.v
@@ -26,7 +26,7 @@ Require Import Errors.
   union).  Numeric types (integers and floats) fully specify the
   bit size of the type.  An integer type is a pair of a signed/unsigned
   flag and a bit size: 8, 16, or 32 bits, or the special [IBool] size
-  standing for the C99 [_Bool] type. *)
+  standing for the C99 [_Bool] type.  64-bit integers are treated separately. *)
 
 Inductive signedness : Type :=
   | Signed: signedness
@@ -92,6 +92,7 @@ Definition noattr := {| attr_volatile := false |}.
 Inductive type : Type :=
   | Tvoid: type                                    (**r the [void] type *)
   | Tint: intsize -> signedness -> attr -> type    (**r integer types *)
+  | Tlong: signedness -> attr -> type              (**r 64-bit integer types *)
   | Tfloat: floatsize -> attr -> type              (**r floating-point types *)
   | Tpointer: type -> attr -> type                 (**r pointer types ([*ty]) *)
   | Tarray: type -> Z -> attr -> type              (**r array types ([ty[len]]) *)
@@ -131,6 +132,7 @@ Definition attr_of_type (ty: type) :=
   match ty with
   | Tvoid => noattr
   | Tint sz si a => a
+  | Tlong si a => a
   | Tfloat sz a => a
   | Tpointer elt a => a
   | Tarray elt sz a => a
@@ -148,8 +150,7 @@ Definition type_bool := Tint IBool Signed noattr.
 
 Definition typeconv (ty: type) : type :=
   match ty with
-  | Tint I32 Unsigned _ => ty
-  | Tint _ _ a          => Tint I32 Signed a
+  | Tint (I8 | I16 | IBool) _ a => Tint I32 Signed a
   | Tarray t sz a       => Tpointer t a
   | Tfunction _ _       => Tpointer ty noattr
   | _                   => ty
@@ -166,6 +167,7 @@ Fixpoint alignof (t: type) : Z :=
   | Tint I16 _ _ => 2
   | Tint I32 _ _ => 4
   | Tint IBool _ _ => 1
+  | Tlong _ _ => 8
   | Tfloat F32 _ => 4
   | Tfloat F64 _ => 8
   | Tpointer _ _ => 4
@@ -218,6 +220,7 @@ Fixpoint sizeof (t: type) : Z :=
   | Tint I16 _ _ => 2
   | Tint I32 _ _ => 4
   | Tint IBool _ _ => 1
+  | Tlong _ _ => 8
   | Tfloat F32 _ => 4
   | Tfloat F64 _ => 8
   | Tpointer _ _ => 4
@@ -425,6 +428,7 @@ Definition access_mode (ty: type) : mode :=
   | Tint I16 Unsigned _ => By_value Mint16unsigned
   | Tint I32 _ _ => By_value Mint32
   | Tint IBool _ _ => By_value Mint8unsigned
+  | Tlong _ _ => By_value Mint64
   | Tfloat F32 _ => By_value Mfloat32
   | Tfloat F64 _ => By_value Mfloat64
   | Tvoid => By_nothing
@@ -458,6 +462,7 @@ Fixpoint unroll_composite (ty: type) : type :=
   match ty with
   | Tvoid => ty
   | Tint _ _ _ => ty
+  | Tlong _ _ => ty
   | Tfloat _ _ => ty
   | Tpointer t1 a => Tpointer (unroll_composite t1) a
   | Tarray t1 sz a => Tarray (unroll_composite t1) sz a
@@ -526,6 +531,7 @@ Fixpoint type_of_params (params: list (ident * type)) : typelist :=
 Definition typ_of_type (t: type) : AST.typ :=
   match t with
   | Tfloat _ _ => AST.Tfloat
+  | Tlong _ _ => AST.Tlong
   | _ => AST.Tint
   end.
 
@@ -533,6 +539,7 @@ Definition opttyp_of_type (t: type) : option AST.typ :=
   match t with
   | Tvoid => None
   | Tfloat _ _ => Some AST.Tfloat
+  | Tlong _ _ => Some AST.Tlong
   | _ => Some AST.Tint
   end.
 
diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v
index 7711ade..657f607 100644
--- a/cfrontend/Initializers.v
+++ b/cfrontend/Initializers.v
@@ -54,7 +54,7 @@ Fixpoint constval (a: expr) : res val :=
   match a with
   | Eval v ty =>
       match v with
-      | Vint _ | Vfloat _ => OK v
+      | Vint _ | Vfloat _ | Vlong _ => OK v
       | Vptr _ _ | Vundef => Error(msg "illegal constant")
       end
   | Evalof l ty =>
@@ -152,6 +152,7 @@ Definition transl_init_single (ty: type) (a: expr) : res init_data :=
   | Vint n, Tint I32 sg _ => OK(Init_int32 n)
   | Vint n, Tpointer _ _ => OK(Init_int32 n)
   | Vint n, Tcomp_ptr _ _ => OK(Init_int32 n)
+  | Vlong n, Tlong _ _ => OK(Init_int64 n)
   | Vfloat f, Tfloat F32 _ => OK(Init_float32 f)
   | Vfloat f, Tfloat F64 _ => OK(Init_float64 f)
   | Vptr (Zpos id) ofs, Tint I32 sg _ => OK(Init_addrof id ofs)
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v
index 75b73ff..c2ca135 100644
--- a/cfrontend/Initializersproof.v
+++ b/cfrontend/Initializersproof.v
@@ -333,45 +333,19 @@ Qed.
 
 (** * Soundness of the compile-time evaluator *)
 
-(** [match_val v v'] holds if the compile-time value [v]
-  (with symbolic pointers) matches the run-time value [v']
-  (with concrete pointers). *)
-
-Inductive match_val: val -> val -> Prop :=
-  | match_vint: forall n,
-      match_val (Vint n) (Vint n)
-  | match_vfloat: forall f,
-      match_val (Vfloat f) (Vfloat f)
-  | match_vptr: forall id b ofs,
-      Genv.find_symbol ge id = Some b ->
-      match_val (Vptr (Zpos id) ofs) (Vptr b ofs)
-  | match_vundef:
-      match_val Vundef Vundef.
-
-Lemma match_val_of_bool:
-  forall b, match_val (Val.of_bool b) (Val.of_bool b).
-Proof.
-  destruct b; constructor.
-Qed.
-
-Hint Constructors match_val: mval.
-Hint Resolve match_val_of_bool: mval.
-
-(** The [match_val] relation commutes with the evaluation functions
-  from [Csem]. *)
-
-Lemma sem_unary_match:
-  forall op ty v1 v v1' v',
-  sem_unary_operation op v1 ty = Some v ->
-  sem_unary_operation op v1' ty = Some v' ->
-  match_val v1 v1' ->
-  match_val v v'.
-Proof.
-  intros. destruct op; simpl in *.
-  unfold sem_notbool in *. destruct (classify_bool ty); inv H1; inv H; inv H0; auto with mval. constructor.
-  unfold sem_notint in *. destruct (classify_notint ty); inv H1; inv H; inv H0; auto with mval.
-  unfold sem_neg in *. destruct (classify_neg ty); inv H1; inv H; inv H0; auto with mval.
-Qed.
+(** A global environment [ge] induces a memory injection mapping
+  our symbolic pointers [Vptr (Zpos id) ofs] to run-time pointers
+  [Vptr b ofs] where [Genv.find_symbol ge id = Some b]. *)
+
+Definition inj (b: block) :=
+  match b with
+  | Zpos id =>
+      match Genv.find_symbol ge id with
+      | Some b' => Some (b', 0)
+      | None => None
+      end
+  | _ => None
+  end.
 
 Lemma mem_empty_not_valid_pointer:
   forall b ofs, Mem.valid_pointer Mem.empty b ofs = false.
@@ -387,104 +361,18 @@ Proof.
   now rewrite !mem_empty_not_valid_pointer.
 Qed.
 
-Lemma sem_cmp_match:
-  forall c v1 ty1 v2 ty2 m v v1' v2' v',
-  sem_cmp c v1 ty1 v2 ty2 Mem.empty = Some v ->
-  sem_cmp c v1' ty1 v2' ty2 m = Some v' ->
-  match_val v1 v1' -> match_val v2 v2' ->
-  match_val v v'.
-Proof.
-Opaque zeq.
-  intros. unfold sem_cmp in *.
-  destruct (classify_cmp ty1 ty2); try (destruct s); inv H1; inv H2; inv H; inv H0; auto with mval.
-- destruct (Int.eq n Int.zero); try discriminate. 
-  unfold Val.cmp_different_blocks in *. destruct c; inv H3; inv H2; constructor.
-- destruct (Int.eq n Int.zero); try discriminate. 
-  unfold Val.cmp_different_blocks in *. destruct c; inv H2; inv H1; constructor.
-- destruct (zeq (Z.pos id) (Z.pos id0)); discriminate.
-Qed.
-
-Lemma sem_binary_match:
-  forall op v1 ty1 v2 ty2 m v v1' v2' v',
-  sem_binary_operation op v1 ty1 v2 ty2 Mem.empty = Some v ->
-  sem_binary_operation op v1' ty1 v2' ty2 m = Some v' ->
-  match_val v1 v1' -> match_val v2 v2' ->
-  match_val v v'.
-Proof.
-  intros. unfold sem_binary_operation in *; destruct op.
-(* add *)
-  unfold sem_add in *. destruct (classify_add ty1 ty2); inv H1; inv H2; inv H; inv H0; auto with mval.
-(* sub *)
-  unfold sem_sub in *. destruct (classify_sub ty1 ty2); inv H1; inv H2; try (inv H; inv H0; auto with mval; fail).
-  destruct (zeq (Zpos id) (Zpos id0)); try discriminate.
-  assert (b0 = b) by congruence. subst b0. rewrite zeq_true in H0. 
-  destruct (Int.eq (Int.repr (sizeof ty)) Int.zero); inv H; inv H0; auto with mval.
-(* mul *)
-  unfold sem_mul in *. destruct (classify_mul ty1 ty2); inv H1; inv H2; inv H; inv H0; auto with mval.
-(* div *)
-  unfold sem_div in H0. functional inversion H; rewrite H4 in H0; inv H1; inv H2; inv H0.
-  inv H12. rewrite H11 in H2. inv H2. constructor.
-  inv H12. rewrite H11 in H2. inv H2. constructor.
-  inv H11. constructor.
-  inv H11. constructor.
-  inv H11. constructor.
-(* mod *)
-  unfold sem_mod in H0. functional inversion H; rewrite H4 in H0; inv H1; inv H2; inv H0.
-  inv H12. rewrite H11 in H2. inv H2. constructor.
-  inv H12. rewrite H11 in H2. inv H2. constructor.
-(* and *)
-  unfold sem_and in *. destruct (classify_binint ty1 ty2); inv H1; inv H2; inv H; inv H0; auto with mval.
-(* or *)
-  unfold sem_or in *. destruct (classify_binint ty1 ty2); inv H1; inv H2; inv H; inv H0; auto with mval.
-(* xor *)
-  unfold sem_xor in *. destruct (classify_binint ty1 ty2); inv H1; inv H2; inv H; inv H0; auto with mval.
-(* shl *)
-  unfold sem_shl in *. destruct (classify_shift ty1 ty2); inv H1; inv H2; try discriminate.
-  destruct (Int.ltu n0 Int.iwordsize); inv H0; inv H; constructor.
-(* shr *)
-  unfold sem_shr in *. destruct (classify_shift ty1 ty2); try discriminate;
-  destruct s; inv H1; inv H2; try discriminate.
-  destruct (Int.ltu n0 Int.iwordsize); inv H0; inv H; constructor.
-  destruct (Int.ltu n0 Int.iwordsize); inv H0; inv H; constructor.
-(* comparisons *)
-  eapply sem_cmp_match; eauto.
-  eapply sem_cmp_match; eauto.
-  eapply sem_cmp_match; eauto.
-  eapply sem_cmp_match; eauto.
-  eapply sem_cmp_match; eauto.
-  eapply sem_cmp_match; eauto.
-Qed.
-
 Lemma sem_cast_match:
-  forall v1 ty1 ty2 v2, sem_cast v1 ty1 ty2 = Some v2 ->
-  forall v1' v2',  match_val v1' v1 -> do_cast v1' ty1 ty2 = OK v2' ->
-  match_val v2' v2.
+  forall v1 ty1 ty2 v2 v1' v2',
+  sem_cast v1 ty1 ty2 = Some v2 ->
+  do_cast v1' ty1 ty2 = OK v2' ->
+  val_inject inj v1' v1 ->
+  val_inject inj v2' v2.
 Proof.
-  intros. unfold do_cast in H1. destruct (sem_cast v1' ty1 ty2) as [v2''|] eqn:?; inv H1.
-  unfold sem_cast in H; functional inversion Heqo; subst. 
-  rewrite H2 in H. inv H0. inv H. constructor.
-  rewrite H2 in H. inv H0. inv H. constructor; auto.
-  rewrite H2 in H. inv H0. inv H. constructor.
-  rewrite H2 in H. inv H0. inv H. constructor.
-  rewrite H2 in H. inv H0. inv H. constructor.
-  rewrite H2 in H. inv H0. destruct (cast_float_int si2 f); inv H. inv H7. constructor.
-  rewrite H2 in H. inv H0. inv H. rewrite H7. constructor.
-  rewrite H2 in H. inv H0. inv H. rewrite H7. constructor.
-  rewrite H2 in H. inv H0. inv H. constructor.
-  rewrite H2 in H. inv H0. inv H. constructor.
-  rewrite H2 in H. destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H. auto.
-  rewrite H2 in H. destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H. auto.
-  rewrite H5 in H. inv H. auto.
+  intros. unfold do_cast in H0. destruct (sem_cast v1' ty1 ty2) as [v2''|] eqn:E; inv H0.
+  exploit sem_cast_inject. eexact E. eauto. 
+  intros [v' [A B]]. congruence.
 Qed.
 
-Lemma bool_val_match:
-  forall v v' ty,
-  match_val v v' ->
-  bool_val v ty = bool_val v' ty.
-Proof.
-  intros. inv H; auto.
-Qed.
-  
 (** Soundness of [constval] with respect to the big-step semantics *)
 
 Lemma constval_rvalue:
@@ -492,13 +380,13 @@ Lemma constval_rvalue:
   eval_simple_rvalue empty_env m a v ->
   forall v',
   constval a = OK v' ->
-  match_val v' v
+  val_inject inj v' v
 with constval_lvalue:
   forall m a b ofs,
   eval_simple_lvalue empty_env m a b ofs ->
   forall v',
   constval a = OK v' ->
-  match_val v' (Vptr b ofs).
+  val_inject inj v' (Vptr b ofs).
 Proof.
   (* rvalue *)
   induction 1; intros vres CV; simpl in CV; try (monadInv CV).
@@ -509,11 +397,18 @@ Proof.
   (* addrof *)
   eauto.
   (* unop *)
-  revert EQ0. caseEq (sem_unary_operation op x (typeof r1)); intros; inv EQ0.
-  eapply sem_unary_match; eauto. 
+  destruct (sem_unary_operation op x (typeof r1)) as [v1'|] eqn:E; inv EQ0.
+  exploit sem_unary_operation_inject. eexact E. eauto. 
+  intros [v' [A B]]. congruence.
   (* binop *)
-  revert EQ2. caseEq (sem_binary_operation op x (typeof r1) x0 (typeof r2) Mem.empty); intros; inv EQ2.
-  eapply sem_binary_match; eauto.
+  destruct (sem_binary_operation op x (typeof r1) x0 (typeof r2) Mem.empty) as [v1'|] eqn:E; inv EQ2.
+  exploit (sem_binary_operation_inj inj Mem.empty m).
+  intros. rewrite mem_empty_not_valid_pointer in H3; discriminate.
+  intros. rewrite mem_empty_not_weak_valid_pointer in H3; discriminate.
+  intros. rewrite mem_empty_not_weak_valid_pointer in H3; discriminate.
+  intros. rewrite mem_empty_not_valid_pointer in H3; discriminate.
+  eauto. eauto. eauto. 
+  intros [v' [A B]]. congruence.
   (* cast *)
   eapply sem_cast_match; eauto. 
   (* sizeof *)
@@ -521,18 +416,26 @@ Proof.
   (* alignof *)
   constructor.
   (* seqand *)
-  rewrite (bool_val_match x v1 (typeof r1)) in EQ2; auto. rewrite H0 in EQ2. 
-  monadInv EQ2. eapply sem_cast_match; eauto. eapply sem_cast_match; eauto.
-  rewrite (bool_val_match x v1 (typeof r1)) in EQ2; auto. rewrite H0 in EQ2. 
-  monadInv EQ2. constructor.
+  destruct (bool_val x (typeof r1)) as [b|] eqn:E; inv EQ2. 
+  exploit bool_val_inject. eexact E. eauto. intros E'.
+  assert (b = true) by congruence. subst b. monadInv H5. 
+  eapply sem_cast_match; eauto. eapply sem_cast_match; eauto.
+  destruct (bool_val x (typeof r1)) as [b|] eqn:E; inv EQ2. 
+  exploit bool_val_inject. eexact E. eauto. intros E'.
+  assert (b = false) by congruence. subst b. inv H2. auto.
   (* seqor *)
-  rewrite (bool_val_match x v1 (typeof r1)) in EQ2; auto. rewrite H0 in EQ2. 
-  monadInv EQ2. eapply sem_cast_match; eauto. eapply sem_cast_match; eauto.
-  rewrite (bool_val_match x v1 (typeof r1)) in EQ2; auto. rewrite H0 in EQ2. 
-  monadInv EQ2. constructor.
+  destruct (bool_val x (typeof r1)) as [b|] eqn:E; inv EQ2. 
+  exploit bool_val_inject. eexact E. eauto. intros E'.
+  assert (b = false) by congruence. subst b. monadInv H5. 
+  eapply sem_cast_match; eauto. eapply sem_cast_match; eauto.
+  destruct (bool_val x (typeof r1)) as [b|] eqn:E; inv EQ2. 
+  exploit bool_val_inject. eexact E. eauto. intros E'.
+  assert (b = true) by congruence. subst b. inv H2. auto.
   (* conditional *)
-  rewrite (bool_val_match x v1 (typeof r1)) in EQ3; auto.
-  rewrite H0 in EQ3. destruct b; eapply sem_cast_match; eauto.
+  destruct (bool_val x (typeof r1)) as [b'|] eqn:E; inv EQ3.
+  exploit bool_val_inject. eexact E. eauto. intros E'.
+  assert (b' = b) by congruence. subst b'. 
+  destruct b; eapply sem_cast_match; eauto.
   (* comma *)
   auto.
   (* paren *)
@@ -543,12 +446,14 @@ Proof.
   (* var local *)
   unfold empty_env in H. rewrite PTree.gempty in H. congruence.
   (* var_global *)
-  constructor; auto.
+  econstructor. unfold inj. rewrite H0. eauto. auto. 
   (* deref *)
   eauto.
   (* field struct *)
   rewrite H0 in CV. monadInv CV. exploit constval_rvalue; eauto. intro MV. inv MV.
-  simpl. replace x with delta by congruence. constructor. auto.
+  simpl. replace x with delta by congruence. econstructor; eauto. 
+  rewrite ! Int.add_assoc. f_equal. apply Int.add_commut. 
+  simpl. auto.
   (* field union *)
   rewrite H0 in CV. eauto.
 Qed.
@@ -569,7 +474,7 @@ Theorem constval_steps:
   forall f r m v v' ty m',
   star step ge (ExprState f r Kstop empty_env m) E0 (ExprState f (Eval v' ty) Kstop empty_env m') ->
   constval r = OK v ->
-  m' = m /\ ty = typeof r /\ match_val v v'.
+  m' = m /\ ty = typeof r /\ val_inject inj v v'.
 Proof.
   intros. exploit eval_simple_steps; eauto. eapply constval_simple; eauto. 
   intros [A [B C]]. intuition. eapply constval_rvalue; eauto.
@@ -595,19 +500,23 @@ Proof.
   inv D. 
   (* int *)
   destruct ty; try discriminate. 
-  destruct i; inv EQ2.
+  destruct i0; inv EQ2.
   destruct s; simpl in H2; inv H2. rewrite <- Mem.store_signed_unsigned_8; auto. auto.
   destruct s; simpl in H2; inv H2. rewrite <- Mem.store_signed_unsigned_16; auto. auto.
   simpl in H2; inv H2. assumption.
   inv EQ2. simpl in H2; inv H2. assumption.
+  (* long *)
+  destruct ty; inv EQ2. simpl in H2; inv H2. assumption.
   (* float *)
   destruct ty; try discriminate. 
   destruct f1; inv EQ2; simpl in H2; inv H2; assumption.
   (* pointer *)
-  assert (data = Init_addrof id ofs0 /\ chunk = Mint32).
+  unfold inj in H. destruct b1; try discriminate.
+  assert (data = Init_addrof p ofs1 /\ chunk = Mint32).
     destruct ty; inv EQ2; inv H2.
     destruct i; inv H5. intuition congruence. auto.
-  destruct H4; subst. rewrite H. assumption.
+  destruct H4; subst. destruct (Genv.find_symbol ge p); inv H. 
+  rewrite Int.add_zero in H3. auto.
   (* undef *)
   discriminate.
 Qed.
@@ -624,12 +533,15 @@ Proof.
   destruct ty; try discriminate. 
   destruct i0; inv EQ2; reflexivity.
   inv EQ2; reflexivity.
+  inv EQ2; reflexivity.
+  destruct ty; inv EQ2; reflexivity. 
   destruct ty; try discriminate.
   destruct f0; inv EQ2; reflexivity.
   destruct b; try discriminate.
   destruct ty; try discriminate.
   destruct i0; inv EQ2; reflexivity.
   inv EQ2; reflexivity.
+  inv EQ2; reflexivity.
 Qed.
 
 Notation idlsize := Genv.init_data_list_size.
diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml
index d61afa3..a8b2b98 100644
--- a/cfrontend/PrintClight.ml
+++ b/cfrontend/PrintClight.ml
@@ -43,6 +43,7 @@ let rec precedence = function
   | Efield _ -> (16, LtoR)
   | Econst_int _ -> (16, NA)
   | Econst_float _ -> (16, NA)
+  | Econst_long _ -> (16, NA)
   | Eunop _ -> (15, RtoL)
   | Eaddrof _ -> (15, RtoL)
   | Ecast _ -> (14, RtoL)
@@ -79,6 +80,8 @@ let rec expr p (prec, e) =
       fprintf p "%ld" (camlint_of_coqint n)
   | Econst_float(f, _) ->
       fprintf p "%F" (camlfloat_of_coqfloat f)
+  | Econst_long(n, _) ->
+      fprintf p "%LdLL" (camlint64_of_coqint n)
   | Eunop(op, a1, _) ->
       fprintf p "%s%a" (name_unop op) expr (prec', a1)
   | Eaddrof(a1, _) ->
@@ -258,6 +261,7 @@ let rec collect_expr e =
   match e with
   | Econst_int _ -> ()
   | Econst_float _ -> ()
+  | Econst_long _ -> ()
   | Evar _ -> ()
   | Etempvar _ -> ()
   | Ederef(r, _) -> collect_expr r
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index b1ee234..f91dca6 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -64,6 +64,11 @@ let name_floattype sz =
   | F32 -> "float"
   | F64 -> "double"
 
+let name_longtype sg =
+  match sg with
+  | Signed -> "long long"
+  | Unsigned -> "unsigned long long"
+
 (* Collecting the names and fields of structs and unions *)
 
 module StructUnion = Map.Make(String)
@@ -91,6 +96,8 @@ let rec name_cdecl id ty =
       name_inttype sz sg ^ attributes a ^ name_optid id
   | Tfloat(sz, a) ->
       name_floattype sz ^ attributes a ^ name_optid id
+  | Tlong(sg, a) ->
+      name_longtype sg ^ attributes a ^ name_optid id
   | Tpointer(t, a) ->
       let id' =
         match t with
@@ -174,6 +181,7 @@ let print_value p v =
   match v with
   | Vint n -> fprintf p "%ld" (camlint_of_coqint n)
   | Vfloat f -> fprintf p "%F" (camlfloat_of_coqfloat f)
+  | Vlong n -> fprintf p "%Ld" (camlint64_of_coqint n)
   | Vptr(b, ofs) -> fprintf p "<ptr%a>" !print_pointer_hook (b, ofs)
   | Vundef -> fprintf p "<undef>"
 
@@ -397,6 +405,7 @@ let print_init p = function
   | Init_int8 n -> fprintf p "%ld,@ " (camlint_of_coqint n)
   | Init_int16 n -> fprintf p "%ld,@ " (camlint_of_coqint n)
   | Init_int32 n -> fprintf p "%ld,@ " (camlint_of_coqint n)
+  | Init_int64 n -> fprintf p "%Ld,@ " (camlint64_of_coqint n)
   | Init_float32 n -> fprintf p "%F,@ " (camlfloat_of_coqfloat n)
   | Init_float64 n -> fprintf p "%F,@ " (camlfloat_of_coqfloat n)
   | Init_space n -> fprintf p "/* skip %ld, */@ " (camlint_of_coqint n)
@@ -444,6 +453,7 @@ let rec collect_type = function
   | Tvoid -> ()
   | Tint _ -> ()
   | Tfloat _ -> ()
+  | Tlong _ -> ()
   | Tpointer(t, _) -> collect_type t
   | Tarray(t, _, _) -> collect_type t
   | Tfunction(args, res) -> collect_type_list args; collect_type res
diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v
index 2dbd97e..98dad93 100644
--- a/cfrontend/SimplExpr.v
+++ b/cfrontend/SimplExpr.v
@@ -108,6 +108,7 @@ Function eval_simpl_expr (a: expr) : option val :=
   match a with
   | Econst_int n _ => Some(Vint n)
   | Econst_float n _ => Some(Vfloat n)
+  | Econst_long n _ => Some(Vlong n)
   | Ecast b ty => 
       match eval_simpl_expr b with
       | None => None
@@ -222,6 +223,8 @@ Fixpoint transl_expr (dst: destination) (a: Csyntax.expr) : mon (list statement
       ret (finish dst nil (Econst_int n ty))
   | Csyntax.Eval (Vfloat n) ty =>
       ret (finish dst nil (Econst_float n ty))
+  | Csyntax.Eval (Vlong n) ty =>
+      ret (finish dst nil (Econst_long n ty))
   | Csyntax.Eval _ ty =>
       error (msg "SimplExpr.transl_expr: Eval")
   | Csyntax.Esizeof ty' ty =>
diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v
index b31738b..1e7a84c 100644
--- a/cfrontend/SimplExprspec.v
+++ b/cfrontend/SimplExprspec.v
@@ -768,6 +768,10 @@ Opaque makeif.
     constructor. auto. intros; constructor.
     constructor.
     constructor. auto. intros; constructor.
+  intros. destruct dst; simpl in *; inv H2. 
+    constructor. auto. intros; constructor.
+    constructor.
+    constructor. auto. intros; constructor.
 (* var *)
   monadInv H; econstructor; split; auto with gensym. UseFinish. constructor.
 (* field *)
diff --git a/cfrontend/SimplLocals.v b/cfrontend/SimplLocals.v
index 18eeea2..edcd5fe 100644
--- a/cfrontend/SimplLocals.v
+++ b/cfrontend/SimplLocals.v
@@ -46,6 +46,7 @@ Definition make_cast (a: expr) (tto: type) : expr :=
   | cast_case_neutral => a
   | cast_case_i2i I32 _ => a
   | cast_case_f2f F64 => a
+  | cast_case_l2l => a
   | cast_case_struct _ _ _ _ => a
   | cast_case_union _ _ _ _ => a
   | cast_case_void => a
@@ -58,6 +59,7 @@ Fixpoint simpl_expr (cenv: compilenv) (a: expr) : expr :=
   match a with
   | Econst_int _ _ => a
   | Econst_float _ _ => a
+  | Econst_long _ _ => a
   | Evar id ty => if VSet.mem id cenv then Etempvar id ty else Evar id ty
   | Etempvar id ty => Etempvar id ty
   | Ederef a1 ty => Ederef (simpl_expr cenv a1) ty
@@ -156,6 +158,7 @@ Fixpoint addr_taken_expr (a: expr): VSet.t :=
   match a with
   | Econst_int _ _ => VSet.empty
   | Econst_float _ _ => VSet.empty
+  | Econst_long _ _ => VSet.empty
   | Evar id ty => VSet.empty
   | Etempvar id ty => VSet.empty
   | Ederef a1 ty => addr_taken_expr a1
@@ -224,8 +227,7 @@ Definition add_lifted (cenv: compilenv) (vars1 vars2: list (ident * type)) :=
 
 Definition transf_function (f: function) : res function :=
   let cenv := cenv_for f in
-  do x <- assertion (list_disjoint_dec ident_eq (var_names f.(fn_params))
-                                                (var_names f.(fn_temps)));
+  assertion (list_disjoint_dec ident_eq (var_names f.(fn_params)) (var_names f.(fn_temps)));
   do body' <- simpl_stmt cenv f.(fn_body);
   OK {| fn_return := f.(fn_return);
         fn_params := f.(fn_params);
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index e3aa4e2..1dcf630 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -202,16 +202,22 @@ Inductive val_casted: val -> type -> Prop :=
   | val_casted_float: forall sz attr n,
       cast_float_float sz n = n ->
       val_casted (Vfloat n) (Tfloat sz attr)
+  | val_casted_long: forall si attr n,
+      val_casted (Vlong n) (Tlong si attr)
   | val_casted_ptr_ptr: forall b ofs ty attr,
       val_casted (Vptr b ofs) (Tpointer ty attr)
   | val_casted_int_ptr: forall n ty attr,
       val_casted (Vint n) (Tpointer ty attr)
   | val_casted_ptr_int: forall b ofs si attr,
       val_casted (Vptr b ofs) (Tint I32 si attr)
-  | val_casted_struct: forall id fld attr v,
-      val_casted v (Tstruct id fld attr)
-  | val_casted_union: forall id fld attr v,
-      val_casted v (Tunion id fld attr)
+  | val_casted_ptr_cptr: forall b ofs id attr,
+      val_casted (Vptr b ofs) (Tcomp_ptr id attr)
+  | val_casted_int_cptr: forall n id attr,
+      val_casted (Vint n) (Tcomp_ptr id attr)
+  | val_casted_struct: forall id fld attr b ofs,
+      val_casted (Vptr b ofs) (Tstruct id fld attr)
+  | val_casted_union: forall id fld attr b ofs,
+      val_casted (Vptr b ofs) (Tunion id fld attr)
   | val_casted_void: forall v,
       val_casted v Tvoid.
 
@@ -240,12 +246,15 @@ Proof.
   constructor.
 (* int *)
   destruct i; destruct ty; simpl in H; try discriminate; destruct v; inv H.
-  constructor. apply (cast_int_int_idem I8 s). 
+  constructor. apply (cast_int_int_idem I8 s).
+  constructor. apply (cast_int_int_idem I8 s).
   destruct (cast_float_int s f0); inv H1.   constructor. apply (cast_int_int_idem I8 s). 
-  constructor. apply (cast_int_int_idem I16 s). 
+  constructor. apply (cast_int_int_idem I16 s).
+  constructor. apply (cast_int_int_idem I16 s).
   destruct (cast_float_int s f0); inv H1.   constructor. apply (cast_int_int_idem I16 s). 
   constructor. auto.
-  constructor. 
+  constructor.
+  constructor. auto. 
   destruct (cast_float_int s f0); inv H1. constructor. auto.
   constructor. auto.
   constructor.
@@ -253,7 +262,10 @@ Proof.
   constructor.
   constructor; auto.
   constructor; auto.
+  constructor; auto.
+  constructor; auto.
   constructor. simpl. destruct (Int.eq i0 Int.zero); auto.
+  constructor. simpl. destruct (Int64.eq i Int64.zero); auto.
   constructor. simpl. destruct (Float.cmp Ceq f0 Float.zero); auto.
   constructor. simpl. destruct (Int.eq i Int.zero); auto.
   constructor; auto.
@@ -261,20 +273,31 @@ Proof.
   constructor; auto.
   constructor. simpl. destruct (Int.eq i Int.zero); auto.
   constructor; auto.
+  constructor. simpl. destruct (Int.eq i0 Int.zero); auto.
+  constructor; auto.
+(* long *)
+  destruct ty; try discriminate.
+  destruct v; inv H. constructor.
+  destruct v; inv H. constructor.
+  destruct v; try discriminate. destruct (cast_float_long s f0); inv H. constructor.
 (* float *)
   destruct ty; simpl in H; try discriminate; destruct v; inv H.
   constructor. apply cast_float_float_idem.
   constructor. apply cast_float_float_idem.
+  constructor. apply cast_float_float_idem.
 (* pointer *)
   destruct ty; simpl in H; try discriminate; destruct v; inv H; try constructor.
 (* impossible cases *)
   discriminate.
   discriminate.
-(* structs,unions *)
-  constructor.
-  constructor.
-(* impossible cases *)
-  discriminate.
+(* structs *)
+  destruct ty; try discriminate; destruct v; try discriminate.
+  destruct (ident_eq i0 i && fieldlist_eq f0 f); inv H; constructor.
+(* unions *)
+  destruct ty; try discriminate; destruct v; try discriminate.
+  destruct (ident_eq i0 i && fieldlist_eq f0 f); inv H; constructor.
+(* comp_ptr *)
+  destruct ty; simpl in H; try discriminate; destruct v; inv H; constructor.
 Qed.
 
 Lemma val_casted_load_result:
@@ -293,6 +316,9 @@ Proof.
   inv H0; auto.
   inv H0; auto.
   inv H0; auto.
+  inv H0; auto.
+  discriminate.
+  discriminate.
   discriminate.
   discriminate.
   discriminate.
@@ -301,24 +327,18 @@ Qed.
 Lemma cast_val_casted:
   forall v ty, val_casted v ty -> sem_cast v ty ty = Some v.
 Proof.
-  intros. inversion H; clear H; subst v ty; unfold sem_cast; simpl.
+  intros. inversion H; clear H; subst v ty; unfold sem_cast; simpl; auto.
   destruct sz; congruence.
   congruence.
-  auto.
-  auto.
-  auto.
   unfold proj_sumbool; repeat rewrite dec_eq_true; auto.
   unfold proj_sumbool; repeat rewrite dec_eq_true; auto.
-  auto.
 Qed.
 
 Lemma val_casted_inject:
   forall f v v' ty,
   val_inject f v v' -> val_casted v ty -> val_casted v' ty.
 Proof.
-  intros. inv H.
-  auto.
-  auto.
+  intros. inv H; auto.
   inv H0; constructor.
   inv H0; constructor.
 Qed.
@@ -356,7 +376,10 @@ Proof.
   destruct v1; inv H0; auto.
   destruct sz2; auto. destruct v1; inv H0; auto.
   destruct sz2; auto. destruct v1; inv H0; auto.
+  destruct v1; inv H0; auto.
+  destruct v1; try discriminate.
   destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H0; auto.
+  destruct v1; try discriminate.
   destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H0; auto.
   inv H0; auto.
 Qed.
@@ -1324,176 +1347,6 @@ Proof.
   exists (Vptr loc' ofs'); split; auto. eapply deref_loc_copy; eauto.
 Qed.
 
-Remark val_inject_vtrue: forall f, val_inject f Vtrue Vtrue.
-Proof. unfold Vtrue; auto. Qed.
-
-Remark val_inject_vfalse: forall f, val_inject f Vfalse Vfalse.
-Proof. unfold Vfalse; auto. Qed.
-
-Remark val_inject_of_bool: forall f b, val_inject f (Val.of_bool b) (Val.of_bool b).
-Proof. intros. unfold Val.of_bool. destruct b; [apply val_inject_vtrue|apply val_inject_vfalse]. 
-Qed.
-
-Hint Resolve val_inject_vtrue val_inject_vfalse val_inject_of_bool.
-
-Ltac TrivialInject :=
-  match goal with
-  | |- exists v', Some ?v = Some v' /\ _ => exists v; split; auto
-(*
-  | |- exists v', _ /\ val_inject _ (Vint ?n) _ => exists (Vint n); split; auto
-  | |- exists v', _ /\ val_inject _ (Vfloat ?n) _ => exists (Vfloat n); split; auto
-  | |- exists v', _ /\ val_inject _ Vtrue _ => exists Vtrue; split; auto
-  | |- exists v', _ /\ val_inject _ Vfalse _ => exists Vfalse; split; auto
-  | |- exists v', _ /\ val_inject _ (Val.of_bool ?b) _ => exists (Val.of_bool b); split; auto
-*)
-  | _ => idtac
-  end.
-
-Lemma sem_unary_operation_inject:
-  forall op v1 ty v tv1,
-  sem_unary_operation op v1 ty = Some v ->
-  val_inject f v1 tv1 ->
-  exists tv, sem_unary_operation op tv1 ty = Some tv /\ val_inject f v tv.
-Proof.
-  unfold sem_unary_operation; intros. destruct op.
-  (* notbool *)
-  unfold sem_notbool in *; destruct (classify_bool ty); inv H0; inv H; TrivialInject.
-  (* notint *)
-  unfold sem_notint in *; destruct (classify_notint ty); inv H0; inv H; TrivialInject.
-  (* neg *)
-  unfold sem_neg in *; destruct (classify_neg ty); inv H0; inv H; TrivialInject.
-Qed.
-
-Lemma sem_cmp_inject:
-  forall cmp v1 tv1 ty1 v2 tv2 ty2 v,
-  sem_cmp cmp v1 ty1 v2 ty2 m = Some v ->
-  val_inject f v1 tv1 ->
-  val_inject f v2 tv2 ->
-  exists tv, sem_cmp cmp tv1 ty1 tv2 ty2 tm = Some tv /\ val_inject f v tv.
-Proof.
-  unfold sem_cmp; intros. 
-  assert (MM: option_map Val.of_bool (Val.cmp_different_blocks cmp) = Some v ->
-      exists tv, option_map Val.of_bool (Val.cmp_different_blocks cmp) = Some tv /\ val_inject f v tv).
-    intros. exists v; split; auto. 
-    destruct cmp; simpl in H2; inv H2; auto.
-
-  destruct (classify_cmp ty1 ty2); try destruct s; inv H0; try discriminate; inv H1; inv H; TrivialInject.
-  destruct (Int.eq i Int.zero); try discriminate; auto.
-  destruct (Int.eq i Int.zero); try discriminate; auto.
-
-  destruct (zeq b1 b0); subst.
-  rewrite H0 in H2. inv H2. rewrite zeq_true.
-  destruct (Mem.weak_valid_pointer m b0 (Int.unsigned ofs1)) eqn:?; try discriminate.
-  destruct (Mem.weak_valid_pointer m b0 (Int.unsigned ofs0)) eqn:?; try discriminate.
-  simpl H3.
-  rewrite (Mem.weak_valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb) by eauto.
-  rewrite (Mem.weak_valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb0) by eauto.
-  simpl. replace  (Int.cmpu cmp (Int.add ofs1 (Int.repr delta))
-                         (Int.add ofs0 (Int.repr delta)))
-     with  (Int.cmpu cmp ofs1 ofs0).
-  inv H3; TrivialInject.
-  symmetry. apply Int.translate_cmpu. 
-  eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
-  eapply Mem.weak_valid_pointer_inject_no_overflow; eauto.
-  destruct (Mem.valid_pointer m b1 (Int.unsigned ofs1)) eqn:?; try discriminate.
-  destruct (Mem.valid_pointer m b0 (Int.unsigned ofs0)) eqn:?; try discriminate.
-  destruct (zeq b2 b3); subst.
-  rewrite Mem.valid_pointer_implies
-    by (eapply (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb); eauto).
-  rewrite Mem.valid_pointer_implies
-    by (eapply (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb0); eauto).
-  simpl.
-  exploit Mem.different_pointers_inject; eauto. intros [[]|A]. easy.
-  destruct cmp; simpl in H3; inv H3.
-  simpl. unfold Int.eq. rewrite zeq_false; auto.
-  simpl. unfold Int.eq. rewrite zeq_false; auto.
-  rewrite (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb) by eauto.
-  rewrite (Mem.valid_pointer_inject_val _ _ _ _ _ _ _ MEMINJ Heqb0) by eauto.
-  simpl in H3 |- *. auto.
-Qed.
-
-Lemma sem_binary_operation_inject:
-  forall op v1 ty1 v2 ty2 v tv1 tv2,
-  sem_binary_operation op v1 ty1 v2 ty2 m = Some v ->
-  val_inject f v1 tv1 -> val_inject f v2 tv2 ->
-  exists tv, sem_binary_operation op tv1 ty1 tv2 ty2 tm = Some tv /\ val_inject f v tv.
-Proof.
-  unfold sem_binary_operation; intros. destruct op.
-(* add *)
-  unfold sem_add in *; destruct (classify_add ty1 ty2); inv H0; try discriminate; inv H1; inv H; TrivialInject.
-  econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
-  econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
-(* sub *)
-  unfold sem_sub in *; destruct (classify_sub ty1 ty2); inv H0; try discriminate; inv H1; inv H; TrivialInject.
-  econstructor. eauto. rewrite Int.sub_add_l. auto. 
-  destruct (zeq b1 b0); try discriminate. subst b1. rewrite H0 in H2; inv H2.
-  rewrite zeq_true. destruct (Int.eq (Int.repr (sizeof ty)) Int.zero); inv H3.
-  rewrite Int.sub_shifted. TrivialInject. 
-(* mul *)
-  unfold sem_mul in *; destruct (classify_mul ty1 ty2); inv H0; try discriminate; inv H1; inv H; TrivialInject.
-(* div *)
-  unfold sem_div in *; destruct (classify_div ty1 ty2); try destruct s; inv H0; try discriminate; inv H1; inv H; TrivialInject.
-  destruct ( Int.eq i0 Int.zero
-           || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H1; TrivialInject.
-  destruct (Int.eq i0 Int.zero); inv H1; TrivialInject.
-(* mod *)
-  unfold sem_mod in *; destruct (classify_binint ty1 ty2); try destruct s; inv H0; try discriminate; inv H1; inv H; TrivialInject.
-  destruct ( Int.eq i0 Int.zero
-           || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H1; TrivialInject.
-  destruct (Int.eq i0 Int.zero); inv H1; TrivialInject.
-(* and *)
-  unfold sem_and in *; destruct (classify_binint ty1 ty2); inv H0; try discriminate; inv H1; inv H; TrivialInject.
-(* or *)
-  unfold sem_or in *; destruct (classify_binint ty1 ty2); inv H0; try discriminate; inv H1; inv H; TrivialInject.
-(* xor *)
-  unfold sem_xor in *; destruct (classify_binint ty1 ty2); inv H0; try discriminate; inv H1; inv H; TrivialInject.
-(* shl *)
-  unfold sem_shl in *; destruct (classify_shift ty1 ty2); inv H0; try discriminate; inv H1; inv H; TrivialInject.
-  destruct (Int.ltu i0 Int.iwordsize); inv H1; TrivialInject.
-(* shr *)
-  unfold sem_shr in *; destruct (classify_shift ty1 ty2); try destruct s; inv H0; try discriminate; inv H1; inv H; TrivialInject.
-  destruct (Int.ltu i0 Int.iwordsize); inv H1; TrivialInject.
-  destruct (Int.ltu i0 Int.iwordsize); inv H1; TrivialInject.
-(* comparisons *)
-  eapply sem_cmp_inject; eauto.
-  eapply sem_cmp_inject; eauto.
-  eapply sem_cmp_inject; eauto.
-  eapply sem_cmp_inject; eauto.
-  eapply sem_cmp_inject; eauto.
-  eapply sem_cmp_inject; eauto.
-Qed.
-
-Lemma sem_cast_inject:
-  forall v1 ty1 ty v tv1,
-  sem_cast v1 ty1 ty = Some v ->
-  val_inject f v1 tv1 ->
-  exists tv, sem_cast tv1 ty1 ty = Some tv /\ val_inject f v tv.
-Proof.
-  unfold sem_cast; intros.
-  destruct (classify_cast ty1 ty); try discriminate.
-  inv H0; inv H; TrivialInject. econstructor; eauto.
-  inv H0; inv H; TrivialInject. 
-  inv H0; inv H; TrivialInject. 
-  inv H0; inv H; TrivialInject. 
-  inv H0; try discriminate. destruct (cast_float_int si2 f0); inv H. TrivialInject.
-  inv H0; inv H. TrivialInject.
-  inv H0; inv H. TrivialInject.
-  TrivialInject.
-  destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H. TrivialInject.
-  destruct (ident_eq id1 id2 && fieldlist_eq fld1 fld2); inv H. TrivialInject.
-  inv H; TrivialInject.
-Qed.
-
-Lemma bool_val_inject:
-  forall v ty b tv,
-  bool_val v ty = Some b ->
-  val_inject f v tv ->
-  bool_val tv ty = Some b.
-Proof.
-  unfold bool_val; intros. 
-  destruct (classify_bool ty); inv H0; congruence.
-Qed.
-
 Lemma eval_simpl_expr:
   forall a v,
   eval_expr ge e le m a v ->
@@ -1512,6 +1365,7 @@ Proof.
 (* const *)
   exists (Vint i); split; auto. constructor.
   exists (Vfloat f0); split; auto. constructor.
+  exists (Vlong i); split; auto. constructor.
 (* tempvar *)
   exploit me_temps; eauto. intros [[tv [A B]] C]. 
   exists tv; split; auto. constructor; auto.
@@ -2184,7 +2038,7 @@ Proof.
 
 (* goto *)
   generalize TRF; intros TRF'. monadInv TRF'. 
-  exploit (simpl_find_label j (cenv_for f) m lo tlo lbl (fn_body f) (call_cont k) x0 (call_cont tk)).
+  exploit (simpl_find_label j (cenv_for f) m lo tlo lbl (fn_body f) (call_cont k) x (call_cont tk)).
     eauto. eapply match_cont_call_cont. eauto.  
     apply compat_cenv_for.
   rewrite H. intros [ts' [tk' [A [B [C D]]]]]. 
@@ -2197,12 +2051,10 @@ Proof.
   generalize EQ; intro EQ'; monadInv EQ'.
   assert (list_norepet (var_names (fn_params f ++ fn_vars f))).
     unfold var_names. rewrite map_app. auto.
-  assert (list_disjoint (var_names (fn_params f)) (var_names (fn_temps f))).
-    monadInv EQ0. auto. 
   exploit match_envs_alloc_variables; eauto.
     instantiate (1 := cenv_for_gen (addr_taken_stmt f.(fn_body)) (fn_params f ++ fn_vars f)).
-    intros. eapply cenv_for_gen_by_value; eauto. rewrite VSF.mem_iff. eexact H5.
-    intros. eapply cenv_for_gen_domain. rewrite VSF.mem_iff. eexact H4.
+    intros. eapply cenv_for_gen_by_value; eauto. rewrite VSF.mem_iff. eexact H4.
+    intros. eapply cenv_for_gen_domain. rewrite VSF.mem_iff. eexact H3.
   intros [j' [te [tm0 [A [B [C [D [E F]]]]]]]].
   exploit store_params_correct.
     eauto. 
@@ -2212,7 +2064,7 @@ Proof.
     eexact B. eexact C.
     intros. apply (create_undef_temps_lifted id f). auto.
     intros. destruct (create_undef_temps (fn_temps f))!id as [v|] eqn:?; auto.
-    exploit create_undef_temps_inv; eauto. intros [P Q]. elim (H3 id id); auto.
+    exploit create_undef_temps_inv; eauto. intros [P Q]. elim (l id id); auto.
   intros [tel [tm1 [P [Q [R [S T]]]]]].
   change (cenv_for_gen (addr_taken_stmt (fn_body f)) (fn_params f ++ fn_vars f))
     with (cenv_for f) in *.