Forgot to add these two files.

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

2 files changed, 758 insertions, 0 deletions

diff --git a/backend/SelectDiv.v b/backend/SelectDiv.v
new file mode 100644
index 0000000..e61a088
--- /dev/null
+++ b/backend/SelectDiv.v
@@ -0,0 +1,248 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Instruction selection for integer division and modulus *)
+
+Require Import Coqlib.
+Require Import AST.
+Require Import Integers.
+Require Import Floats.
+Require Import Op.
+Require Import CminorSel.
+Require Import SelectOp.
+
+Open Local Scope cminorsel_scope.
+
+(** We try to turn divisions by a constant into a multiplication by
+  a pseudo-inverse of the divisor.  The approach is described in
+- Torbjörn Granlund, Peter L. Montgomery: "Division by Invariant
+  Integers using Multiplication". PLDI 1994.
+- Henry S. Warren, Jr: "Hacker's Delight". Addison-Wesley.  Chapter 10.
+*)
+
+Fixpoint find_div_mul_params (fuel: nat) (nc: Z) (d: Z) (p: Z) : option (Z * Z) :=
+  match fuel with
+  | O => None
+  | S fuel' =>
+      let twp := two_p p in
+      if zlt (nc * (d - twp mod d)) twp
+      then Some(p - 32, (twp + d - twp mod d) / d)
+      else find_div_mul_params fuel' nc d (p + 1)
+  end.
+
+Definition divs_mul_params (d: Z) : option (Z * Z) :=
+  match find_div_mul_params
+          Int.wordsize
+          (Int.half_modulus - Int.half_modulus mod d - 1)
+          d 32 with
+  | None => None
+  | Some(p, m) =>
+      if zlt 0 d
+      && zlt (two_p (32 + p)) (m * d)
+      && zle (m * d) (two_p (32 + p) + two_p (p + 1))
+      && zle 0 m && zlt m Int.modulus
+      && zle 0 p && zlt p 32
+      then Some(p, m) else None
+  end.
+
+Definition divu_mul_params (d: Z) : option (Z * Z) :=
+  match find_div_mul_params
+          Int.wordsize
+          (Int.modulus - Int.modulus mod d - 1)
+          d 32 with
+  | None => None
+  | Some(p, m) =>
+      if zlt 0 d
+      && zle (two_p (32 + p)) (m * d)
+      && zle (m * d) (two_p (32 + p) + two_p p)
+      && zle 0 m && zlt m Int.modulus
+      && zle 0 p && zlt p 32
+      then Some(p, m) else None
+  end.
+
+Definition divu_mul (p: Z) (m: Z) :=
+  shruimm (Eop Omulhu (Eletvar O ::: Eop (Ointconst (Int.repr m)) Enil ::: Enil))
+          (Int.repr p).
+
+Definition divuimm (e1: expr) (n2: int) :=
+  match Int.is_power2 n2 with
+  | Some l => shruimm e1 l
+  | None =>
+      match divu_mul_params (Int.unsigned n2) with
+      | None => divu_base e1 (Eop (Ointconst n2) Enil)
+      | Some(p, m) => Elet e1 (divu_mul p m)
+      end
+  end.
+
+(** Original definition:
+<<
+Nondetfunction divu (e1: expr) (e2: expr) := 
+  match e2 with
+  | Eop (Ointconst n2) Enil => divuimm e1 n2
+  | _ => divu_base e1 e2
+  end.
+>>
+*)
+
+Inductive divu_cases: forall (e2: expr), Type :=
+  | divu_case1: forall n2, divu_cases (Eop (Ointconst n2) Enil)
+  | divu_default: forall (e2: expr), divu_cases e2.
+
+Definition divu_match (e2: expr) :=
+  match e2 as zz1 return divu_cases zz1 with
+  | Eop (Ointconst n2) Enil => divu_case1 n2
+  | e2 => divu_default e2
+  end.
+
+Definition divu (e1: expr) (e2: expr) :=
+  match divu_match e2 with
+  | divu_case1 n2 => (* Eop (Ointconst n2) Enil *) 
+      divuimm e1 n2
+  | divu_default e2 =>
+      divu_base e1 e2
+  end.
+
+
+Definition mod_from_div (equo: expr) (n: int) :=
+  Eop Osub (Eletvar O ::: mulimm n equo ::: Enil).
+
+Definition moduimm (e1: expr) (n2: int) :=
+  match Int.is_power2 n2 with
+  | Some l => andimm (Int.sub n2 Int.one) e1
+  | None =>
+      match divu_mul_params (Int.unsigned n2) with
+      | None => modu_base e1 (Eop (Ointconst n2) Enil)
+      | Some(p, m) => Elet e1 (mod_from_div (divu_mul p m) n2)
+      end
+  end.
+
+(** Original definition:
+<<
+Nondetfunction modu (e1: expr) (e2: expr) := 
+  match e2 with
+  | Eop (Ointconst n2) Enil => moduimm e1 n2
+  | _ => modu_base e1 e2
+  end.
+>>
+*)
+
+Inductive modu_cases: forall (e2: expr), Type :=
+  | modu_case1: forall n2, modu_cases (Eop (Ointconst n2) Enil)
+  | modu_default: forall (e2: expr), modu_cases e2.
+
+Definition modu_match (e2: expr) :=
+  match e2 as zz1 return modu_cases zz1 with
+  | Eop (Ointconst n2) Enil => modu_case1 n2
+  | e2 => modu_default e2
+  end.
+
+Definition modu (e1: expr) (e2: expr) :=
+  match modu_match e2 with
+  | modu_case1 n2 => (* Eop (Ointconst n2) Enil *) 
+      moduimm e1 n2
+  | modu_default e2 =>
+      modu_base e1 e2
+  end.
+
+
+Definition divs_mul (p: Z) (m: Z) :=
+  let e2 :=
+    Eop Omulhs (Eletvar O ::: Eop (Ointconst (Int.repr m)) Enil ::: Enil) in
+  let e3 :=
+    if zlt m Int.half_modulus then e2 else add e2 (Eletvar O) in
+  add (shrimm e3 (Int.repr p))
+      (shruimm (Eletvar O) (Int.repr (Int.zwordsize - 1))).
+
+Definition divsimm (e1: expr) (n2: int) :=
+  match Int.is_power2 n2 with
+  | Some l => 
+      if Int.ltu l (Int.repr 31)
+      then shrximm e1 l
+      else divs_base e1 (Eop (Ointconst n2) Enil)
+  | None =>
+      match divs_mul_params (Int.signed n2) with
+      | None => divs_base e1 (Eop (Ointconst n2) Enil)
+      | Some(p, m) => Elet e1 (divs_mul p m)
+      end
+  end.
+
+(** Original definition:
+<<
+Nondetfunction divs (e1: expr) (e2: expr) := 
+  match e2 with
+  | Eop (Ointconst n2) Enil => divsimm e1 n2
+  | _ => divs_base e1 e2
+  end.
+>>
+*)
+
+Inductive divs_cases: forall (e2: expr), Type :=
+  | divs_case1: forall n2, divs_cases (Eop (Ointconst n2) Enil)
+  | divs_default: forall (e2: expr), divs_cases e2.
+
+Definition divs_match (e2: expr) :=
+  match e2 as zz1 return divs_cases zz1 with
+  | Eop (Ointconst n2) Enil => divs_case1 n2
+  | e2 => divs_default e2
+  end.
+
+Definition divs (e1: expr) (e2: expr) :=
+  match divs_match e2 with
+  | divs_case1 n2 => (* Eop (Ointconst n2) Enil *) 
+      divsimm e1 n2
+  | divs_default e2 =>
+      divs_base e1 e2
+  end.
+
+
+Definition modsimm (e1: expr) (n2: int) :=
+  match Int.is_power2 n2 with
+  | Some l =>
+      if Int.ltu l (Int.repr 31)
+      then Elet e1 (mod_from_div (shrximm (Eletvar O) l) n2)
+      else mods_base e1 (Eop (Ointconst n2) Enil)
+  | None =>
+      match divs_mul_params (Int.signed n2) with
+      | None => mods_base e1 (Eop (Ointconst n2) Enil)
+      | Some(p, m) => Elet e1 (mod_from_div (divs_mul p m) n2)
+      end
+  end.
+
+(** Original definition:
+<<
+Nondetfunction mods (e1: expr) (e2: expr) := 
+  match e2 with
+  | Eop (Ointconst n2) Enil => modsimm e1 n2
+  | _ => mods_base e1 e2
+  end.
+>>
+*)
+
+Inductive mods_cases: forall (e2: expr), Type :=
+  | mods_case1: forall n2, mods_cases (Eop (Ointconst n2) Enil)
+  | mods_default: forall (e2: expr), mods_cases e2.
+
+Definition mods_match (e2: expr) :=
+  match e2 as zz1 return mods_cases zz1 with
+  | Eop (Ointconst n2) Enil => mods_case1 n2
+  | e2 => mods_default e2
+  end.
+
+Definition mods (e1: expr) (e2: expr) :=
+  match mods_match e2 with
+  | mods_case1 n2 => (* Eop (Ointconst n2) Enil *) 
+      modsimm e1 n2
+  | mods_default e2 =>
+      mods_base e1 e2
+  end.
+
+
diff --git a/backend/SelectLong.v b/backend/SelectLong.v
new file mode 100644
index 0000000..5ba892d
--- /dev/null
+++ b/backend/SelectLong.v
@@ -0,0 +1,510 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Instruction selection for 64-bit integer operations *)
+
+Require Import Coqlib.
+Require Import AST.
+Require Import Integers.
+Require Import Floats.
+Require Import Op.
+Require Import CminorSel.
+Require Import SelectOp.
+
+Open Local Scope cminorsel_scope.
+
+(** Some operations on 64-bit integers are transformed into calls to
+  runtime library functions.  The following record type collects
+  the names of these functions. *)
+
+Record helper_functions : Type := mk_helper_functions {
+  i64_dtos: ident;                      (**r float -> signed long *)
+  i64_dtou: ident;                      (**r float -> unsigned long *)
+  i64_stod: ident;                      (**r signed long -> float *)
+  i64_utod: ident;                      (**r unsigned long -> float *)
+  i64_stof: ident;                      (**r signed long -> float32 *)
+  i64_utof: ident;                      (**r unsigned long -> float32 *)
+  i64_neg: ident;                       (**r opposite *)
+  i64_add: ident;                       (**r addition *)
+  i64_sub: ident;                       (**r subtraction *)
+  i64_mul: ident;                       (**r multiplication 32x32->64 *)
+  i64_sdiv: ident;                      (**r signed division *)
+  i64_udiv: ident;                      (**r unsigned division *)
+  i64_smod: ident;                      (**r signed remainder *)
+  i64_umod: ident;                      (**r unsigned remainder *)
+  i64_shl: ident;                       (**r shift left *)
+  i64_shr: ident;                       (**r shift right unsigned *)
+  i64_sar: ident                        (**r shift right signed *)
+}.
+
+Definition sig_l_l := mksignature (Tlong :: nil) (Some Tlong).
+Definition sig_l_f := mksignature (Tlong :: nil) (Some Tfloat).
+Definition sig_l_s := mksignature (Tlong :: nil) (Some Tsingle).
+Definition sig_f_l := mksignature (Tfloat :: nil) (Some Tlong).
+Definition sig_ll_l := mksignature (Tlong :: Tlong :: nil) (Some Tlong).
+Definition sig_li_l := mksignature (Tlong :: Tint :: nil) (Some Tlong).
+Definition sig_ii_l := mksignature (Tint :: Tint :: nil) (Some Tlong).
+
+Section SELECT.
+
+Variable hf: helper_functions.
+
+Definition makelong (h l: expr): expr :=
+  Eop Omakelong (h ::: l ::: Enil).
+
+(** Original definition:
+<<
+Nondetfunction splitlong (e: expr) (f: expr -> expr -> expr) :=
+  match e with
+  | Eop Omakelong (h ::: l ::: Enil) => f h l
+  | _ => Elet e (f (Eop Ohighlong (Eletvar O ::: Enil)) (Eop Olowlong (Eletvar O ::: Enil)))
+  end.
+>>
+*)
+
+Inductive splitlong_cases: forall (e: expr) , Type :=
+  | splitlong_case1: forall h l, splitlong_cases (Eop Omakelong (h ::: l ::: Enil))
+  | splitlong_default: forall (e: expr) , splitlong_cases e.
+
+Definition splitlong_match (e: expr)  :=
+  match e as zz1 return splitlong_cases zz1 with
+  | Eop Omakelong (h ::: l ::: Enil) => splitlong_case1 h l
+  | e => splitlong_default e
+  end.
+
+Definition splitlong (e: expr) (f: expr -> expr -> expr) :=
+  match splitlong_match e with
+  | splitlong_case1 h l => (* Eop Omakelong (h ::: l ::: Enil) *) 
+      f h l
+  | splitlong_default e =>
+      Elet e (f (Eop Ohighlong (Eletvar O ::: Enil)) (Eop Olowlong (Eletvar O ::: Enil)))
+  end.
+
+
+(** Original definition:
+<<
+Nondetfunction splitlong2 (e1 e2: expr) (f: expr -> expr -> expr -> expr -> expr) :=
+  match e1, e2 with
+  | Eop Omakelong (h1 ::: l1 ::: Enil), Eop Omakelong (h2 ::: l2 ::: Enil) =>
+      f h1 l1 h2 l2
+  | Eop Omakelong (h1 ::: l1 ::: Enil), t2 =>
+      Elet t2 (f (lift h1) (lift l1)
+                 (Eop Ohighlong (Eletvar O ::: Enil)) (Eop Olowlong (Eletvar O ::: Enil)))
+  | t1, Eop Omakelong (h2 ::: l2 ::: Enil) =>
+      Elet t1 (f (Eop Ohighlong (Eletvar O ::: Enil)) (Eop Olowlong (Eletvar O ::: Enil))
+                 (lift h2) (lift l2))
+  | _, _ =>
+      Elet e1 (Elet (lift e2)
+        (f (Eop Ohighlong (Eletvar 1 ::: Enil)) (Eop Olowlong (Eletvar 1 ::: Enil))
+           (Eop Ohighlong (Eletvar O ::: Enil)) (Eop Olowlong (Eletvar O ::: Enil))))
+  end.
+>>
+*)
+
+Inductive splitlong2_cases: forall (e1 e2: expr) , Type :=
+  | splitlong2_case1: forall h1 l1 h2 l2, splitlong2_cases (Eop Omakelong (h1 ::: l1 ::: Enil)) (Eop Omakelong (h2 ::: l2 ::: Enil))
+  | splitlong2_case2: forall h1 l1 t2, splitlong2_cases (Eop Omakelong (h1 ::: l1 ::: Enil)) (t2)
+  | splitlong2_case3: forall t1 h2 l2, splitlong2_cases (t1) (Eop Omakelong (h2 ::: l2 ::: Enil))
+  | splitlong2_default: forall (e1 e2: expr) , splitlong2_cases e1 e2.
+
+Definition splitlong2_match (e1 e2: expr)  :=
+  match e1 as zz1, e2 as zz2 return splitlong2_cases zz1 zz2 with
+  | Eop Omakelong (h1 ::: l1 ::: Enil), Eop Omakelong (h2 ::: l2 ::: Enil) => splitlong2_case1 h1 l1 h2 l2
+  | Eop Omakelong (h1 ::: l1 ::: Enil), t2 => splitlong2_case2 h1 l1 t2
+  | t1, Eop Omakelong (h2 ::: l2 ::: Enil) => splitlong2_case3 t1 h2 l2
+  | e1, e2 => splitlong2_default e1 e2
+  end.
+
+Definition splitlong2 (e1 e2: expr) (f: expr -> expr -> expr -> expr -> expr) :=
+  match splitlong2_match e1 e2 with
+  | splitlong2_case1 h1 l1 h2 l2 => (* Eop Omakelong (h1 ::: l1 ::: Enil), Eop Omakelong (h2 ::: l2 ::: Enil) *) 
+      f h1 l1 h2 l2
+  | splitlong2_case2 h1 l1 t2 => (* Eop Omakelong (h1 ::: l1 ::: Enil), t2 *) 
+      Elet t2 (f (lift h1) (lift l1) (Eop Ohighlong (Eletvar O ::: Enil)) (Eop Olowlong (Eletvar O ::: Enil)))
+  | splitlong2_case3 t1 h2 l2 => (* t1, Eop Omakelong (h2 ::: l2 ::: Enil) *) 
+      Elet t1 (f (Eop Ohighlong (Eletvar O ::: Enil)) (Eop Olowlong (Eletvar O ::: Enil)) (lift h2) (lift l2))
+  | splitlong2_default e1 e2 =>
+      Elet e1 (Elet (lift e2) (f (Eop Ohighlong (Eletvar 1 ::: Enil)) (Eop Olowlong (Eletvar 1 ::: Enil)) (Eop Ohighlong (Eletvar O ::: Enil)) (Eop Olowlong (Eletvar O ::: Enil))))
+  end.
+
+
+(** Original definition:
+<<
+Nondetfunction lowlong (e: expr) :=
+  match e with
+  | Eop Omakelong (e1 ::: e2 ::: Enil) => e2
+  | _ => Eop Olowlong (e ::: Enil)
+  end.
+>>
+*)
+
+Inductive lowlong_cases: forall (e: expr), Type :=
+  | lowlong_case1: forall e1 e2, lowlong_cases (Eop Omakelong (e1 ::: e2 ::: Enil))
+  | lowlong_default: forall (e: expr), lowlong_cases e.
+
+Definition lowlong_match (e: expr) :=
+  match e as zz1 return lowlong_cases zz1 with
+  | Eop Omakelong (e1 ::: e2 ::: Enil) => lowlong_case1 e1 e2
+  | e => lowlong_default e
+  end.
+
+Definition lowlong (e: expr) :=
+  match lowlong_match e with
+  | lowlong_case1 e1 e2 => (* Eop Omakelong (e1 ::: e2 ::: Enil) *) 
+      e2
+  | lowlong_default e =>
+      Eop Olowlong (e ::: Enil)
+  end.
+
+
+(** Original definition:
+<<
+Nondetfunction highlong (e: expr) :=
+  match e with
+  | Eop Omakelong (e1 ::: e2 ::: Enil) => e1
+  | _ => Eop Ohighlong (e ::: Enil)
+  end.
+>>
+*)
+
+Inductive highlong_cases: forall (e: expr), Type :=
+  | highlong_case1: forall e1 e2, highlong_cases (Eop Omakelong (e1 ::: e2 ::: Enil))
+  | highlong_default: forall (e: expr), highlong_cases e.
+
+Definition highlong_match (e: expr) :=
+  match e as zz1 return highlong_cases zz1 with
+  | Eop Omakelong (e1 ::: e2 ::: Enil) => highlong_case1 e1 e2
+  | e => highlong_default e
+  end.
+
+Definition highlong (e: expr) :=
+  match highlong_match e with
+  | highlong_case1 e1 e2 => (* Eop Omakelong (e1 ::: e2 ::: Enil) *) 
+      e1
+  | highlong_default e =>
+      Eop Ohighlong (e ::: Enil)
+  end.
+
+
+Definition longconst (n: int64) : expr :=
+  makelong (Eop (Ointconst (Int64.hiword n)) Enil)
+           (Eop (Ointconst (Int64.loword n)) Enil).
+
+(** Original definition:
+<<
+Nondetfunction is_longconst (e: expr) :=
+  match e with
+  | Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) =>
+      Some(Int64.ofwords h l)
+  | _ =>
+      None
+  end.
+>>
+*)
+
+Inductive is_longconst_cases: forall (e: expr), Type :=
+  | is_longconst_case1: forall h l, is_longconst_cases (Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil))
+  | is_longconst_default: forall (e: expr), is_longconst_cases e.
+
+Definition is_longconst_match (e: expr) :=
+  match e as zz1 return is_longconst_cases zz1 with
+  | Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) => is_longconst_case1 h l
+  | e => is_longconst_default e
+  end.
+
+Definition is_longconst (e: expr) :=
+  match is_longconst_match e with
+  | is_longconst_case1 h l => (* Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) *) 
+      Some(Int64.ofwords h l)
+  | is_longconst_default e =>
+      None
+  end.
+
+
+Definition is_longconst_zero (e: expr) :=
+  match is_longconst e with
+  | Some n => Int64.eq n Int64.zero
+  | None => false
+  end.
+
+Definition intoflong (e: expr) := lowlong e.
+
+Definition longofint (e: expr) :=
+  Elet e (makelong (shrimm (Eletvar O) (Int.repr 31)) (Eletvar O)).
+
+Definition longofintu (e: expr) :=
+  makelong (Eop (Ointconst Int.zero) Enil) e.
+
+Definition negl (e: expr) :=
+  match is_longconst e with
+  | Some n => longconst (Int64.neg n)
+  | None => Ebuiltin (EF_builtin hf.(i64_neg) sig_l_l) (e ::: Enil)
+  end.
+
+Definition notl (e: expr) :=
+  splitlong e (fun h l => makelong (notint h) (notint l)).
+
+Definition longoffloat (arg: expr) := 
+  Eexternal hf.(i64_dtos) sig_f_l (arg ::: Enil).
+Definition longuoffloat (arg: expr) :=
+  Eexternal hf.(i64_dtou) sig_f_l (arg ::: Enil).
+Definition floatoflong (arg: expr) :=
+  Eexternal hf.(i64_stod) sig_l_f (arg ::: Enil).
+Definition floatoflongu (arg: expr) :=
+  Eexternal hf.(i64_utod) sig_l_f (arg ::: Enil).
+Definition singleoflong (arg: expr) :=
+  Eexternal hf.(i64_stof) sig_l_s (arg ::: Enil).
+Definition singleoflongu (arg: expr) :=
+  Eexternal hf.(i64_utof) sig_l_s (arg ::: Enil).
+
+Definition andl (e1 e2: expr) :=
+  splitlong2 e1 e2 (fun h1 l1 h2 l2 => makelong (and h1 h2) (and l1 l2)).
+
+Definition orl (e1 e2: expr) :=
+  splitlong2 e1 e2 (fun h1 l1 h2 l2 => makelong (or h1 h2) (or l1 l2)).
+
+Definition xorl (e1 e2: expr) :=
+  splitlong2 e1 e2 (fun h1 l1 h2 l2 => makelong (xor h1 h2) (xor l1 l2)).
+
+Definition shllimm (e1: expr) (n: int) :=
+  if Int.eq n Int.zero then e1 else
+  if Int.ltu n Int.iwordsize then
+   splitlong e1 (fun h l =>
+     makelong (or (shlimm h n) (shruimm l (Int.sub Int.iwordsize n)))
+              (shlimm l n))
+  else if Int.ltu n Int64.iwordsize' then
+    makelong (shlimm (lowlong e1) (Int.sub n Int.iwordsize))
+             (Eop (Ointconst Int.zero) Enil)
+  else
+    Eexternal hf.(i64_shl) sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil).
+
+Definition shrluimm (e1: expr) (n: int) :=
+  if Int.eq n Int.zero then e1 else
+  if Int.ltu n Int.iwordsize then
+    splitlong e1 (fun h l =>
+      makelong (shruimm h n)
+               (or (shruimm l n) (shlimm h (Int.sub Int.iwordsize n))))
+  else if Int.ltu n Int64.iwordsize' then
+    makelong (Eop (Ointconst Int.zero) Enil)
+             (shruimm (highlong e1) (Int.sub n Int.iwordsize))
+  else
+    Eexternal hf.(i64_shr) sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil).
+
+Definition shrlimm (e1: expr) (n: int) :=
+  if Int.eq n Int.zero then e1 else
+  if Int.ltu n Int.iwordsize then
+    splitlong e1 (fun h l =>
+      makelong (shrimm h n)
+               (or (shruimm l n) (shlimm h (Int.sub Int.iwordsize n))))
+  else if Int.ltu n Int64.iwordsize' then
+    Elet (highlong e1)
+      (makelong (shrimm (Eletvar 0) (Int.repr 31))
+                (shrimm (Eletvar 0) (Int.sub n Int.iwordsize)))
+  else
+    Eexternal hf.(i64_sar) sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil).
+
+Definition is_intconst (e: expr) :=
+  match e with
+  | Eop (Ointconst n) Enil => Some n
+  | _ => None
+  end.
+
+Definition shll (e1 e2: expr) :=
+  match is_intconst e2 with
+  | Some n => shllimm e1 n
+  | None => Eexternal hf.(i64_shl) sig_li_l (e1 ::: e2 ::: Enil)
+  end.
+
+Definition shrlu (e1 e2: expr) :=
+  match is_intconst e2 with
+  | Some n => shrluimm e1 n
+  | None => Eexternal hf.(i64_shr) sig_li_l (e1 ::: e2 ::: Enil)
+  end.
+
+Definition shrl (e1 e2: expr) :=
+  match is_intconst e2 with
+  | Some n => shrlimm e1 n
+  | None => Eexternal hf.(i64_sar) sig_li_l (e1 ::: e2 ::: Enil)
+  end.
+
+Definition addl (e1 e2: expr) :=
+  let default := Ebuiltin (EF_builtin hf.(i64_add) sig_ll_l) (e1 ::: e2 ::: Enil) in
+  match is_longconst e1, is_longconst e2 with
+  | Some n1, Some n2 => longconst (Int64.add n1 n2)
+  | Some n1, _ => if Int64.eq n1 Int64.zero then e2 else default
+  | _, Some n2 => if Int64.eq n2 Int64.zero then e1 else default
+  | _, _ => default
+  end.
+
+Definition subl (e1 e2: expr) :=
+  let default := Ebuiltin (EF_builtin hf.(i64_sub) sig_ll_l) (e1 ::: e2 ::: Enil) in
+  match is_longconst e1, is_longconst e2 with
+  | Some n1, Some n2 => longconst (Int64.sub n1 n2)
+  | Some n1, _ => if Int64.eq n1 Int64.zero then negl e2 else default
+  | _, Some n2 => if Int64.eq n2 Int64.zero then e1 else default
+  | _, _ => default
+  end.
+
+Definition mull_base (e1 e2: expr) :=
+  splitlong2 e1 e2 (fun h1 l1 h2 l2 =>
+    Elet (Ebuiltin (EF_builtin hf.(i64_mul) sig_ii_l) (l1 ::: l2 ::: Enil))
+      (makelong
+        (add (add (Eop Ohighlong (Eletvar O ::: Enil))
+                  (mul (lift l1) (lift h2)))
+             (mul (lift h1) (lift l2)))
+        (Eop Olowlong (Eletvar O ::: Enil)))).
+
+Definition mullimm (e: expr) (n: int64) :=
+  if Int64.eq n Int64.zero then longconst Int64.zero else
+  if Int64.eq n Int64.one then e else
+  match Int64.is_power2 n with
+  | Some l => shllimm e (Int.repr (Int64.unsigned l))
+  | None   => mull_base e (longconst n)
+  end.
+
+Definition mull (e1 e2: expr) :=
+  match is_longconst e1, is_longconst e2 with
+  | Some n1, Some n2 => longconst (Int64.mul n1 n2)
+  | Some n1, _ => mullimm e2 n1
+  | _, Some n2 => mullimm e1 n2
+  | _, _ => mull_base e1 e2
+  end.
+
+Definition binop_long (id: ident) (sem: int64 -> int64 -> int64) (e1 e2: expr) :=
+  match is_longconst e1, is_longconst e2 with
+  | Some n1, Some n2 => longconst (sem n1 n2)
+  | _, _ => Eexternal id sig_ll_l (e1 ::: e2 ::: Enil)
+  end.
+
+Definition divl := binop_long hf.(i64_sdiv) Int64.divs.
+Definition modl := binop_long hf.(i64_smod) Int64.mods.
+
+Definition divlu (e1 e2: expr) :=
+  let default := Eexternal hf.(i64_udiv) sig_ll_l (e1 ::: e2 ::: Enil) in
+  match is_longconst e1, is_longconst e2 with
+  | Some n1, Some n2 => longconst (Int64.divu n1 n2)
+  | _, Some n2 =>
+      match Int64.is_power2 n2 with
+      | Some l => shrluimm e1 (Int.repr (Int64.unsigned l))
+      | None   => default
+      end
+  | _, _ => default
+  end.
+
+Definition modlu (e1 e2: expr) :=
+  let default := Eexternal hf.(i64_umod) sig_ll_l (e1 ::: e2 ::: Enil) in
+  match is_longconst e1, is_longconst e2 with
+  | Some n1, Some n2 => longconst (Int64.modu n1 n2)
+  | _, Some n2 =>
+      match Int64.is_power2 n2 with
+      | Some l => andl e1 (longconst (Int64.sub n2 Int64.one))
+      | None   => default
+      end
+  | _, _ => default
+  end.
+
+Definition cmpl_eq_zero (e: expr) :=
+  splitlong e (fun h l => comp Ceq (or h l) (Eop (Ointconst Int.zero) Enil)).
+
+Definition cmpl_ne_zero (e: expr) :=
+  splitlong e (fun h l => comp Cne (or h l) (Eop (Ointconst Int.zero) Enil)).
+
+Definition cmplu_gen (ch cl: comparison) (e1 e2: expr) :=
+  splitlong2 e1 e2 (fun h1 l1 h2 l2 =>
+    Econdition (CEcond (Ccomp Ceq) (h1:::h2:::Enil))
+               (Eop (Ocmp (Ccompu cl)) (l1:::l2:::Enil))
+               (Eop (Ocmp (Ccompu ch)) (h1:::h2:::Enil))).
+
+Definition cmplu (c: comparison) (e1 e2: expr) :=
+  match c with
+  | Ceq =>
+      if is_longconst_zero e2
+      then cmpl_eq_zero e1
+      else cmpl_eq_zero (xorl e1 e2)
+  | Cne =>
+      if is_longconst_zero e2
+      then cmpl_ne_zero e1
+      else cmpl_ne_zero (xorl e1 e2)
+  | Clt =>
+      cmplu_gen Clt Clt e1 e2
+  | Cle =>
+      cmplu_gen Clt Cle e1 e2
+  | Cgt =>
+      cmplu_gen Cgt Cgt e1 e2
+  | Cge =>
+      cmplu_gen Cgt Cge e1 e2
+  end.
+
+Definition cmpl_gen (ch cl: comparison) (e1 e2: expr) :=
+  splitlong2 e1 e2 (fun h1 l1 h2 l2 =>
+    Econdition (CEcond (Ccomp Ceq) (h1:::h2:::Enil))
+               (Eop (Ocmp (Ccompu cl)) (l1:::l2:::Enil))
+               (Eop (Ocmp (Ccomp ch)) (h1:::h2:::Enil))).
+
+Definition cmpl (c: comparison) (e1 e2: expr) :=
+  match c with
+  | Ceq =>
+      if is_longconst_zero e2
+      then cmpl_eq_zero e1
+      else cmpl_eq_zero (xorl e1 e2)
+  | Cne =>
+      if is_longconst_zero e2
+      then cmpl_ne_zero e1
+      else cmpl_ne_zero (xorl e1 e2)
+  | Clt =>
+      if is_longconst_zero e2
+      then comp Clt (highlong e1) (Eop (Ointconst Int.zero) Enil)
+      else cmpl_gen Clt Clt e1 e2
+  | Cle =>
+      cmpl_gen Clt Cle e1 e2
+  | Cgt =>
+      cmpl_gen Cgt Cgt e1 e2
+  | Cge =>
+      if is_longconst_zero e2
+      then comp Cge (highlong e1) (Eop (Ointconst Int.zero) Enil)
+      else cmpl_gen Cgt Cge e1 e2
+  end.
+
+End SELECT.
+
+(** Setting up the helper functions *)
+
+Require Import Errors.
+
+Local Open Scope string_scope.
+Local Open Scope error_monad_scope.
+
+Parameter get_helper: Cminor.genv -> String.string -> signature -> res ident.
+Parameter get_builtin: String.string -> signature -> res ident.
+
+Definition get_helpers (ge: Cminor.genv): res helper_functions :=
+  do i64_dtos <- get_helper ge "__i64_dtos" sig_f_l ;
+  do i64_dtou <- get_helper ge "__i64_dtou" sig_f_l ;
+  do i64_stod <- get_helper ge "__i64_stod" sig_l_f ;
+  do i64_utod <- get_helper ge "__i64_utod" sig_l_f ;
+  do i64_stof <- get_helper ge "__i64_stof" sig_l_s ;
+  do i64_utof <- get_helper ge "__i64_utof" sig_l_s ;
+  do i64_neg <- get_builtin "__builtin_negl" sig_l_l ;
+  do i64_add <- get_builtin "__builtin_addl" sig_ll_l ;
+  do i64_sub <- get_builtin "__builtin_subl" sig_ll_l ;
+  do i64_mul <- get_builtin "__builtin_mull" sig_ll_l ;
+  do i64_sdiv <- get_helper ge "__i64_sdiv" sig_ll_l ;
+  do i64_udiv <- get_helper ge "__i64_udiv" sig_ll_l ;
+  do i64_smod <- get_helper ge "__i64_smod" sig_ll_l ;
+  do i64_umod <- get_helper ge "__i64_umod" sig_ll_l ;
+  do i64_shl <- get_helper ge "__i64_shl" sig_li_l ;
+  do i64_shr <- get_helper ge "__i64_shr" sig_li_l ;
+  do i64_sar <- get_helper ge "__i64_sar" sig_li_l ;
+  OK (mk_helper_functions
+     i64_dtos i64_dtou i64_stod i64_utod i64_stof i64_utof
+     i64_neg i64_add i64_sub i64_mul i64_sdiv i64_udiv i64_smod i64_umod
+     i64_shl i64_shr i64_sar).