Oops, wrong commit of generated files.

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

2 files changed, 0 insertions, 758 deletions

diff --git a/backend/SelectDiv.v b/backend/SelectDiv.v
deleted file mode 100644
index e61a088..0000000
--- a/backend/SelectDiv.v
+++ /dev/null
@@ -1,248 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              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
deleted file mode 100644
index 5ba892d..0000000
--- a/backend/SelectLong.v
+++ /dev/null
@@ -1,510 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              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).