Protect against redefinition of the __i64_xxx helper library functions.

This is achieved by declaring these functions in C2C.ml, then
re-checking their declarations in the global environment during
the Selection pass.

In passing, the "hf" parameter for SelectLong functions was removed
and replaced by fixed identifiers corresponding to the actual names
of the helper functions.

6 files changed, 306 insertions, 251 deletions

diff --git a/backend/SelectLong.vp b/backend/SelectLong.vp
index ab4ab8c4..970386a9 100644
--- a/backend/SelectLong.vp
+++ b/backend/SelectLong.vp
@@ -20,31 +20,30 @@ Require Import Op.
 Require Import CminorSel.
 Require Import SelectOp.
 
-Open Local Scope cminorsel_scope.
+Local Open Scope cminorsel_scope.
+Local Open Scope string_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 float64 -> signed long *)
-  i64_dtou: ident;                      (**r float64 -> unsigned long *)
-  i64_stod: ident;                      (**r signed long -> float64 *)
-  i64_utod: ident;                      (**r unsigned long -> float64 *)
-  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 *)
-}.
+  runtime library functions or built-in functions.
+  Here are the names and signatures of these functions. *)
+
+Definition i64_dtos := ident_of_string "__i64_dtos".
+Definition i64_dtou := ident_of_string "__i64_dtou".
+Definition i64_stod := ident_of_string "__i64_stod".
+Definition i64_utod := ident_of_string "__i64_utod".
+Definition i64_stof := ident_of_string "__i64_stof".
+Definition i64_utof := ident_of_string "__i64_utof".
+Definition i64_neg := ident_of_string "__builtin_negl".
+Definition i64_add := ident_of_string "__builtin_addl".
+Definition i64_sub := ident_of_string "__builtin_subl".
+Definition i64_mul := ident_of_string "__builtin_mull".
+Definition i64_sdiv := ident_of_string "__i64_sdiv".
+Definition i64_udiv := ident_of_string "__i64_udiv".
+Definition i64_smod := ident_of_string "__i64_smod".
+Definition i64_umod := ident_of_string "__i64_umod".
+Definition i64_shl := ident_of_string "__i64_shl".
+Definition i64_shr := ident_of_string "__i64_shr".
+Definition i64_sar := ident_of_string "__i64_sar".
 
 Definition sig_l_l := mksignature (Tlong :: nil) (Some Tlong) cc_default.
 Definition sig_l_f := mksignature (Tlong :: nil) (Some Tfloat) cc_default.
@@ -56,8 +55,6 @@ Definition sig_ii_l := mksignature (Tint :: Tint :: nil) (Some Tlong) cc_default
 
 Section SELECT.
 
-Variable hf: helper_functions.
-
 Definition makelong (h l: expr): expr :=
   Eop Omakelong (h ::: l ::: Enil).
 
@@ -124,28 +121,28 @@ Definition longofintu (e: expr) :=
 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)
+  | None => Ebuiltin (EF_builtin 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).
+  Eexternal i64_dtos sig_f_l (arg ::: Enil).
 Definition longuoffloat (arg: expr) :=
-  Eexternal hf.(i64_dtou) sig_f_l (arg ::: Enil).
+  Eexternal i64_dtou sig_f_l (arg ::: Enil).
 Definition floatoflong (arg: expr) :=
-  Eexternal hf.(i64_stod) sig_l_f (arg ::: Enil).
+  Eexternal i64_stod sig_l_f (arg ::: Enil).
 Definition floatoflongu (arg: expr) :=
-  Eexternal hf.(i64_utod) sig_l_f (arg ::: Enil).
+  Eexternal i64_utod sig_l_f (arg ::: Enil).
 Definition longofsingle (arg: expr) := 
   longoffloat (floatofsingle arg).
 Definition longuofsingle (arg: expr) :=
   longuoffloat (floatofsingle arg).
 Definition singleoflong (arg: expr) :=
-  Eexternal hf.(i64_stof) sig_l_s (arg ::: Enil).
+  Eexternal i64_stof sig_l_s (arg ::: Enil).
 Definition singleoflongu (arg: expr) :=
-  Eexternal hf.(i64_utof) sig_l_s (arg ::: Enil).
+  Eexternal 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)).
@@ -166,7 +163,7 @@ Definition shllimm (e1: expr) (n: int) :=
     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).
+    Eexternal 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
@@ -178,7 +175,7 @@ Definition shrluimm (e1: expr) (n: int) :=
     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).
+    Eexternal 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
@@ -191,7 +188,7 @@ Definition shrlimm (e1: expr) (n: int) :=
       (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).
+    Eexternal i64_sar sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil).
 
 Definition is_intconst (e: expr) :=
   match e with
@@ -202,23 +199,23 @@ Definition is_intconst (e: expr) :=
 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)
+  | None => Eexternal 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)
+  | None => Eexternal 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)
+  | None => Eexternal 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
+  let default := Ebuiltin (EF_builtin 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
@@ -227,7 +224,7 @@ Definition addl (e1 e2: expr) :=
   end.
 
 Definition subl (e1 e2: expr) :=
-  let default := Ebuiltin (EF_builtin hf.(i64_sub) sig_ll_l) (e1 ::: e2 ::: Enil) in
+  let default := Ebuiltin (EF_builtin 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
@@ -237,7 +234,7 @@ Definition subl (e1 e2: expr) :=
 
 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))
+    Elet (Ebuiltin (EF_builtin i64_mul sig_ii_l) (l1 ::: l2 ::: Enil))
       (makelong
         (add (add (Eop Ohighlong (Eletvar O ::: Enil))
                   (mul (lift l1) (lift h2)))
@@ -266,11 +263,11 @@ Definition binop_long (id: ident) (sem: int64 -> int64 -> int64) (e1 e2: expr) :
   | _, _ => 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 divl := binop_long i64_sdiv Int64.divs.
+Definition modl := binop_long i64_smod Int64.mods.
 
 Definition divlu (e1 e2: expr) :=
-  let default := Eexternal hf.(i64_udiv) sig_ll_l (e1 ::: e2 ::: Enil) in
+  let default := Eexternal 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 =>
@@ -282,7 +279,7 @@ Definition divlu (e1 e2: expr) :=
   end.
 
 Definition modlu (e1 e2: expr) :=
-  let default := Eexternal hf.(i64_umod) sig_ll_l (e1 ::: e2 ::: Enil) in
+  let default := Eexternal 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 =>
@@ -363,35 +360,44 @@ Definition cmpl (c: comparison) (e1 e2: expr) :=
 
 End SELECT.
 
-(** Setting up the helper functions *)
+(** Checking that the helper functions are available. *)
 
 Require Import Errors.
-
-Local Open Scope string_scope.
+Require Import Globalenvs.
 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).
+Definition check_helper (ge: Cminor.genv) (name_sg: ident * signature) : res unit :=
+  let (name, sg) := name_sg in
+  match Genv.find_symbol ge name with
+  | None => 
+      Error (CTX name :: MSG ": not declared" :: nil)
+  | Some b =>
+      match Genv.find_funct_ptr ge b with
+      | Some (External (EF_external name' sg')) =>
+          if ident_eq name' name && signature_eq sg' sg
+          then OK tt
+          else Error (CTX name :: MSG ": wrong declaration" :: nil)
+      | _ =>
+          Error (CTX name :: MSG ": wrong declaration" :: nil)
+      end
+  end.
+
+Definition i64_helpers :=
+    (i64_dtos, sig_f_l) ::
+    (i64_dtou, sig_f_l) ::
+    (i64_stod, sig_l_f) ::
+    (i64_utod, sig_l_f) ::
+    (i64_stof, sig_l_s) ::
+    (i64_utof, sig_l_s) ::
+    (i64_sdiv, sig_ll_l) ::
+    (i64_udiv, sig_ll_l) ::
+    (i64_smod, sig_ll_l) ::
+    (i64_umod, sig_ll_l) ::
+    (i64_shl, sig_li_l) ::
+    (i64_shr, sig_li_l) ::
+    (i64_sar, sig_li_l) ::
+    nil.
+
+Definition check_helpers (ge: Cminor.genv): res unit :=
+  do x <- mmap (check_helper ge) i64_helpers;
+  OK tt.
diff --git a/backend/SelectLongproof.v b/backend/SelectLongproof.v
index c7c7ab2d..40c11dd8 100644
--- a/backend/SelectLongproof.v
+++ b/backend/SelectLongproof.v
@@ -32,69 +32,67 @@ Open Local Scope cminorsel_scope.
 
 (** * Axiomatization of the helper functions *)
 
-Section HELPERS.
-
-Context {F V: Type} (ge: Genv.t (AST.fundef F) V).
-
-Definition helper_implements (id: ident) (sg: signature) (vargs: list val) (vres: val) : Prop :=
-  exists b, exists ef,
-     Genv.find_symbol ge id = Some b
-  /\ Genv.find_funct_ptr ge b = Some (External ef)
-  /\ ef_sig ef = sg
-  /\ forall m, external_call ef ge vargs m E0 vres m.
+Definition external_implements (id: ident) (sg: signature) (vargs: list val) (vres: val) : Prop :=
+  forall F V (ge: Genv.t F V) m,
+  external_call (EF_external id sg) ge vargs m E0 vres m.
 
 Definition builtin_implements (id: ident) (sg: signature) (vargs: list val) (vres: val) : Prop :=
-  forall m, external_call (EF_builtin id sg) ge vargs m E0 vres m.
-
-Definition i64_helpers_correct (hf: helper_functions) : Prop :=
-    (forall x z, Val.longoffloat x = Some z -> helper_implements hf.(i64_dtos) sig_f_l (x::nil) z)
-  /\(forall x z, Val.longuoffloat x = Some z -> helper_implements hf.(i64_dtou) sig_f_l (x::nil) z)
-  /\(forall x z, Val.floatoflong x = Some z -> helper_implements hf.(i64_stod) sig_l_f (x::nil) z)
-  /\(forall x z, Val.floatoflongu x = Some z -> helper_implements hf.(i64_utod) sig_l_f (x::nil) z)
-  /\(forall x z, Val.singleoflong x = Some z -> helper_implements hf.(i64_stof) sig_l_s (x::nil) z)
-  /\(forall x z, Val.singleoflongu x = Some z -> helper_implements hf.(i64_utof) sig_l_s (x::nil) z)
-  /\(forall x, builtin_implements hf.(i64_neg) sig_l_l (x::nil) (Val.negl x))
-  /\(forall x y, builtin_implements hf.(i64_add) sig_ll_l (x::y::nil) (Val.addl x y))
-  /\(forall x y, builtin_implements hf.(i64_sub) sig_ll_l (x::y::nil) (Val.subl x y))
-  /\(forall x y, builtin_implements hf.(i64_mul) sig_ii_l (x::y::nil) (Val.mull' x y))
-  /\(forall x y z, Val.divls x y = Some z -> helper_implements hf.(i64_sdiv) sig_ll_l (x::y::nil) z)
-  /\(forall x y z, Val.divlu x y = Some z -> helper_implements hf.(i64_udiv) sig_ll_l (x::y::nil) z)
-  /\(forall x y z, Val.modls x y = Some z -> helper_implements hf.(i64_smod) sig_ll_l (x::y::nil) z)
-  /\(forall x y z, Val.modlu x y = Some z -> helper_implements hf.(i64_umod) sig_ll_l (x::y::nil) z)
-  /\(forall x y, helper_implements hf.(i64_shl) sig_li_l (x::y::nil) (Val.shll x y))
-  /\(forall x y, helper_implements hf.(i64_shr) sig_li_l (x::y::nil) (Val.shrlu x y))
-  /\(forall x y, helper_implements hf.(i64_sar) sig_li_l (x::y::nil) (Val.shrl x y)).
-
-End HELPERS.
+  forall F V (ge: Genv.t F V) m,
+  external_call (EF_builtin id sg) ge vargs m E0 vres m.
+
+Axiom i64_helpers_correct :
+    (forall x z, Val.longoffloat x = Some z -> external_implements i64_dtos sig_f_l (x::nil) z)
+ /\ (forall x z, Val.longuoffloat x = Some z -> external_implements i64_dtou sig_f_l (x::nil) z)
+ /\ (forall x z, Val.floatoflong x = Some z -> external_implements i64_stod sig_l_f (x::nil) z)
+ /\ (forall x z, Val.floatoflongu x = Some z -> external_implements i64_utod sig_l_f (x::nil) z)
+ /\ (forall x z, Val.singleoflong x = Some z -> external_implements i64_stof sig_l_s (x::nil) z)
+ /\ (forall x z, Val.singleoflongu x = Some z -> external_implements i64_utof sig_l_s (x::nil) z)
+ /\ (forall x, builtin_implements i64_neg sig_l_l (x::nil) (Val.negl x))
+ /\ (forall x y, builtin_implements i64_add sig_ll_l (x::y::nil) (Val.addl x y))
+ /\ (forall x y, builtin_implements i64_sub sig_ll_l (x::y::nil) (Val.subl x y))
+ /\ (forall x y, builtin_implements i64_mul sig_ii_l (x::y::nil) (Val.mull' x y))
+ /\ (forall x y z, Val.divls x y = Some z -> external_implements i64_sdiv sig_ll_l (x::y::nil) z)
+ /\ (forall x y z, Val.divlu x y = Some z -> external_implements i64_udiv sig_ll_l (x::y::nil) z)
+ /\ (forall x y z, Val.modls x y = Some z -> external_implements i64_smod sig_ll_l (x::y::nil) z)
+ /\ (forall x y z, Val.modlu x y = Some z -> external_implements i64_umod sig_ll_l (x::y::nil) z)
+ /\ (forall x y, external_implements i64_shl sig_li_l (x::y::nil) (Val.shll x y))
+ /\ (forall x y, external_implements i64_shr sig_li_l (x::y::nil) (Val.shrlu x y))
+ /\ (forall x y, external_implements i64_sar sig_li_l (x::y::nil) (Val.shrl x y)).
+
+Definition helper_declared {F V: Type} (ge: Genv.t (AST.fundef F) V) (name: ident) (sg: signature) : Prop :=
+  exists b, Genv.find_symbol ge name = Some b
+         /\ Genv.find_funct_ptr ge b = Some (External (EF_external name sg)).
 
 (** * Correctness of the instruction selection functions for 64-bit operators *)
 
 Section CMCONSTR.
 
-Variable hf: helper_functions.
 Variable ge: genv.
-Hypothesis HELPERS: i64_helpers_correct ge hf.
+Hypothesis HELPERS:
+  forall name sg, In (name, sg) i64_helpers -> helper_declared ge name sg.
 Variable sp: val.
 Variable e: env.
 Variable m: mem.
 
 Ltac UseHelper :=
-  red in HELPERS;
+  generalize i64_helpers_correct; intros;
   repeat (eauto; match goal with | [ H: _ /\ _ |- _ ] => destruct H end).
 
 Lemma eval_helper:
   forall le id sg args vargs vres,
   eval_exprlist ge sp e m le args vargs ->
-  helper_implements ge id sg vargs vres ->
+  In (id, sg) i64_helpers ->
+  external_implements id sg vargs vres ->
   eval_expr ge sp e m le (Eexternal id sg args) vres.
 Proof.
-  intros. destruct H0 as (b & ef & A & B & C & D). econstructor; eauto.
+  intros. exploit HELPERS; eauto. intros (b & A & B). econstructor; eauto.
 Qed.
 
 Corollary eval_helper_1:
   forall le id sg arg1 varg1 vres,
   eval_expr ge sp e m le arg1 varg1 ->
-  helper_implements ge id sg (varg1::nil) vres ->
+  In (id, sg) i64_helpers ->
+  external_implements id sg (varg1::nil) vres ->
   eval_expr ge sp e m le (Eexternal id sg (arg1 ::: Enil)) vres.
 Proof.
   intros. eapply eval_helper; eauto. constructor; auto. constructor.
@@ -104,7 +102,8 @@ Corollary eval_helper_2:
   forall le id sg arg1 arg2 varg1 varg2 vres,
   eval_expr ge sp e m le arg1 varg1 ->
   eval_expr ge sp e m le arg2 varg2 ->
-  helper_implements ge id sg (varg1::varg2::nil) vres ->
+  In (id, sg) i64_helpers ->
+  external_implements id sg (varg1::varg2::nil) vres ->
   eval_expr ge sp e m le (Eexternal id sg (arg1 ::: arg2 ::: Enil)) vres.
 Proof.
   intros. eapply eval_helper; eauto. constructor; auto. constructor; auto. constructor.
@@ -113,7 +112,7 @@ Qed.
 Remark eval_builtin_1:
   forall le id sg arg1 varg1 vres,
   eval_expr ge sp e m le arg1 varg1 ->
-  builtin_implements ge id sg (varg1::nil) vres ->
+  builtin_implements id sg (varg1::nil) vres ->
   eval_expr ge sp e m le (Ebuiltin (EF_builtin id sg) (arg1 ::: Enil)) vres.
 Proof.
   intros. econstructor. econstructor. eauto. constructor. apply H0. 
@@ -123,7 +122,7 @@ Remark eval_builtin_2:
   forall le id sg arg1 arg2 varg1 varg2 vres,
   eval_expr ge sp e m le arg1 varg1 ->
   eval_expr ge sp e m le arg2 varg2 ->
-  builtin_implements ge id sg (varg1::varg2::nil) vres ->
+  builtin_implements id sg (varg1::varg2::nil) vres ->
   eval_expr ge sp e m le (Ebuiltin (EF_builtin id sg) (arg1 ::: arg2 ::: Enil)) vres.
 Proof.
   intros. econstructor. constructor; eauto. constructor; eauto. constructor. apply H1.
@@ -371,7 +370,7 @@ Proof.
   f_equal. destruct (zlt (i0 - Int.zwordsize + (Int.zwordsize - 1)) Int.zwordsize); omega.
 Qed.
 
-Theorem eval_negl: unary_constructor_sound (negl hf) Val.negl.
+Theorem eval_negl: unary_constructor_sound negl Val.negl.
 Proof.
   unfold negl; red; intros. destruct (is_longconst a) eqn:E.
   econstructor; split. apply eval_longconst.  
@@ -395,10 +394,10 @@ Theorem eval_longoffloat:
   forall le a x y,
   eval_expr ge sp e m le a x ->
   Val.longoffloat x = Some y ->
-  exists v, eval_expr ge sp e m le (longoffloat hf a) v /\ Val.lessdef y v.
+  exists v, eval_expr ge sp e m le (longoffloat a) v /\ Val.lessdef y v.
 Proof.
   intros; unfold longoffloat. econstructor; split. 
-  eapply eval_helper_1; eauto. UseHelper. 
+  eapply eval_helper_1; eauto. simpl; auto. UseHelper.
   auto.
 Qed.
 
@@ -406,10 +405,10 @@ Theorem eval_longuoffloat:
   forall le a x y,
   eval_expr ge sp e m le a x ->
   Val.longuoffloat x = Some y ->
-  exists v, eval_expr ge sp e m le (longuoffloat hf a) v /\ Val.lessdef y v.
+  exists v, eval_expr ge sp e m le (longuoffloat a) v /\ Val.lessdef y v.
 Proof.
   intros; unfold longuoffloat. econstructor; split. 
-  eapply eval_helper_1; eauto. UseHelper. 
+  eapply eval_helper_1; eauto. simpl; auto. UseHelper. 
   auto.
 Qed.
 
@@ -417,10 +416,10 @@ Theorem eval_floatoflong:
   forall le a x y,
   eval_expr ge sp e m le a x ->
   Val.floatoflong x = Some y ->
-  exists v, eval_expr ge sp e m le (floatoflong hf a) v /\ Val.lessdef y v.
+  exists v, eval_expr ge sp e m le (floatoflong a) v /\ Val.lessdef y v.
 Proof.
   intros; unfold floatoflong. econstructor; split. 
-  eapply eval_helper_1; eauto. UseHelper. 
+  eapply eval_helper_1; eauto. simpl; auto. UseHelper. 
   auto.
 Qed.
 
@@ -428,10 +427,10 @@ Theorem eval_floatoflongu:
   forall le a x y,
   eval_expr ge sp e m le a x ->
   Val.floatoflongu x = Some y ->
-  exists v, eval_expr ge sp e m le (floatoflongu hf a) v /\ Val.lessdef y v.
+  exists v, eval_expr ge sp e m le (floatoflongu a) v /\ Val.lessdef y v.
 Proof.
   intros; unfold floatoflongu. econstructor; split. 
-  eapply eval_helper_1; eauto. UseHelper. 
+  eapply eval_helper_1; eauto. simpl; auto. UseHelper. 
   auto.
 Qed.
 
@@ -439,7 +438,7 @@ Theorem eval_longofsingle:
   forall le a x y,
   eval_expr ge sp e m le a x ->
   Val.longofsingle x = Some y ->
-  exists v, eval_expr ge sp e m le (longofsingle hf a) v /\ Val.lessdef y v.
+  exists v, eval_expr ge sp e m le (longofsingle a) v /\ Val.lessdef y v.
 Proof.
   intros; unfold longofsingle.
   destruct x; simpl in H0; inv H0. destruct (Float32.to_long f) as [n|] eqn:EQ; simpl in H2; inv H2.
@@ -453,7 +452,7 @@ Theorem eval_longuofsingle:
   forall le a x y,
   eval_expr ge sp e m le a x ->
   Val.longuofsingle x = Some y ->
-  exists v, eval_expr ge sp e m le (longuofsingle hf a) v /\ Val.lessdef y v.
+  exists v, eval_expr ge sp e m le (longuofsingle a) v /\ Val.lessdef y v.
 Proof.
   intros; unfold longuofsingle.
   destruct x; simpl in H0; inv H0. destruct (Float32.to_longu f) as [n|] eqn:EQ; simpl in H2; inv H2.
@@ -467,10 +466,10 @@ Theorem eval_singleoflong:
   forall le a x y,
   eval_expr ge sp e m le a x ->
   Val.singleoflong x = Some y ->
-  exists v, eval_expr ge sp e m le (singleoflong hf a) v /\ Val.lessdef y v.
+  exists v, eval_expr ge sp e m le (singleoflong a) v /\ Val.lessdef y v.
 Proof.
   intros; unfold singleoflong. econstructor; split. 
-  eapply eval_helper_1; eauto. UseHelper. 
+  eapply eval_helper_1; eauto. simpl; auto 20. UseHelper. 
   auto.
 Qed.
 
@@ -478,10 +477,10 @@ Theorem eval_singleoflongu:
   forall le a x y,
   eval_expr ge sp e m le a x ->
   Val.singleoflongu x = Some y ->
-  exists v, eval_expr ge sp e m le (singleoflongu hf a) v /\ Val.lessdef y v.
+  exists v, eval_expr ge sp e m le (singleoflongu a) v /\ Val.lessdef y v.
 Proof.
   intros; unfold singleoflongu. econstructor; split. 
-  eapply eval_helper_1; eauto. UseHelper. 
+  eapply eval_helper_1; eauto. simpl; auto 20. UseHelper. 
   auto.
 Qed.
 
@@ -579,7 +578,7 @@ Qed.
 
 Lemma eval_shllimm:
   forall n,
-  unary_constructor_sound (fun e => shllimm hf e n) (fun v => Val.shll v (Vint n)).
+  unary_constructor_sound (fun e => shllimm e n) (fun v => Val.shll v (Vint n)).
 Proof.
   unfold shllimm; red; intros.
   apply eval_shift_imm; intros.
@@ -609,10 +608,11 @@ Proof.
     simpl. erewrite <- Int64.decompose_shl_2. instantiate (1 := Int64.hiword i). 
     rewrite Int64.ofwords_recompose. auto. auto.
   + (* n >= 64 *)
-    econstructor; split. eapply eval_helper_2; eauto. EvalOp. UseHelper. auto.
+    econstructor; split. eapply eval_helper_2; eauto. EvalOp. 
+    simpl; auto 20. UseHelper. auto.
 Qed.
 
-Theorem eval_shll: binary_constructor_sound (shll hf) Val.shll.
+Theorem eval_shll: binary_constructor_sound shll Val.shll.
 Proof.
   unfold shll; red; intros.
   destruct (is_intconst b) as [n|] eqn:IC.
@@ -620,12 +620,12 @@ Proof.
   exploit is_intconst_sound; eauto. intros EQ; subst y; clear H0.
   eapply eval_shllimm; eauto.
 - (* General case *)
-  econstructor; split. eapply eval_helper_2; eauto. UseHelper. auto.
+  econstructor; split. eapply eval_helper_2; eauto. simpl; auto 20. UseHelper. auto.
 Qed.
 
 Lemma eval_shrluimm:
   forall n,
-  unary_constructor_sound (fun e => shrluimm hf e n) (fun v => Val.shrlu v (Vint n)).
+  unary_constructor_sound (fun e => shrluimm e n) (fun v => Val.shrlu v (Vint n)).
 Proof.
   unfold shrluimm; red; intros. apply eval_shift_imm; intros.
   + (* n = 0 *)
@@ -654,10 +654,10 @@ Proof.
     simpl. erewrite <- Int64.decompose_shru_2. instantiate (1 := Int64.loword i). 
     rewrite Int64.ofwords_recompose. auto. auto.
   + (* n >= 64 *)
-    econstructor; split. eapply eval_helper_2; eauto. EvalOp. UseHelper. auto.
+    econstructor; split. eapply eval_helper_2; eauto. EvalOp. simpl; auto 20. UseHelper. auto.
 Qed.
 
-Theorem eval_shrlu: binary_constructor_sound (shrlu hf) Val.shrlu.
+Theorem eval_shrlu: binary_constructor_sound shrlu Val.shrlu.
 Proof.
   unfold shrlu; red; intros.
   destruct (is_intconst b) as [n|] eqn:IC.
@@ -665,12 +665,12 @@ Proof.
   exploit is_intconst_sound; eauto. intros EQ; subst y; clear H0.
   eapply eval_shrluimm; eauto.
 - (* General case *)
-  econstructor; split. eapply eval_helper_2; eauto. UseHelper. auto.
+  econstructor; split. eapply eval_helper_2; eauto. simpl; auto 20. UseHelper. auto.
 Qed.
 
 Lemma eval_shrlimm:
   forall n,
-  unary_constructor_sound (fun e => shrlimm hf e n) (fun v => Val.shrl v (Vint n)).
+  unary_constructor_sound (fun e => shrlimm e n) (fun v => Val.shrl v (Vint n)).
 Proof.
   unfold shrlimm; red; intros. apply eval_shift_imm; intros.
   + (* n = 0 *)
@@ -703,10 +703,10 @@ Proof.
     erewrite <- Int64.decompose_shr_2. instantiate (1 := Int64.loword i). 
     rewrite Int64.ofwords_recompose. auto. auto.
   + (* n >= 64 *)
-    econstructor; split. eapply eval_helper_2; eauto. EvalOp. UseHelper. auto.
+    econstructor; split. eapply eval_helper_2; eauto. EvalOp. simpl; auto 20. UseHelper. auto.
 Qed.
 
-Theorem eval_shrl: binary_constructor_sound (shrl hf) Val.shrl.
+Theorem eval_shrl: binary_constructor_sound shrl Val.shrl.
 Proof.
   unfold shrl; red; intros.
   destruct (is_intconst b) as [n|] eqn:IC.
@@ -714,17 +714,17 @@ Proof.
   exploit is_intconst_sound; eauto. intros EQ; subst y; clear H0.
   eapply eval_shrlimm; eauto.
 - (* General case *)
-  econstructor; split. eapply eval_helper_2; eauto. UseHelper. auto.
+  econstructor; split. eapply eval_helper_2; eauto. simpl; auto 20. UseHelper. auto.
 Qed.
 
-Theorem eval_addl: binary_constructor_sound (addl hf) Val.addl.
+Theorem eval_addl: binary_constructor_sound addl Val.addl.
 Proof.
   unfold addl; red; intros.
-  set (default := Ebuiltin (EF_builtin (i64_add hf) sig_ll_l) (a ::: b ::: Enil)).
+  set (default := Ebuiltin (EF_builtin i64_add sig_ll_l) (a ::: b ::: Enil)).
   assert (DEFAULT:
     exists v, eval_expr ge sp e m le default v /\ Val.lessdef (Val.addl x y) v).
   {
-    econstructor; split. eapply eval_builtin_2; eauto. UseHelper. auto. 
+    econstructor; split. eapply eval_builtin_2; eauto. simpl; auto 20. UseHelper. auto. 
   }
   destruct (is_longconst a) as [p|] eqn:LC1;
   destruct (is_longconst b) as [q|] eqn:LC2.
@@ -740,14 +740,14 @@ Proof.
 - auto.
 Qed.
 
-Theorem eval_subl: binary_constructor_sound (subl hf) Val.subl.
+Theorem eval_subl: binary_constructor_sound subl Val.subl.
 Proof.
   unfold subl; red; intros.
-  set (default := Ebuiltin (EF_builtin (i64_sub hf) sig_ll_l) (a ::: b ::: Enil)).
+  set (default := Ebuiltin (EF_builtin i64_sub sig_ll_l) (a ::: b ::: Enil)).
   assert (DEFAULT:
     exists v, eval_expr ge sp e m le default v /\ Val.lessdef (Val.subl x y) v).
   {
-    econstructor; split. eapply eval_builtin_2; eauto. UseHelper. auto. 
+    econstructor; split. eapply eval_builtin_2; eauto. simpl; auto 20. UseHelper. auto. 
   }
   destruct (is_longconst a) as [p|] eqn:LC1;
   destruct (is_longconst b) as [q|] eqn:LC2.
@@ -764,7 +764,7 @@ Proof.
 - auto.
 Qed.
 
-Lemma eval_mull_base: binary_constructor_sound (mull_base hf) Val.mull.
+Lemma eval_mull_base: binary_constructor_sound mull_base Val.mull.
 Proof.
   unfold mull_base; red; intros. apply eval_splitlong2; auto.
 - intros. 
@@ -778,7 +778,7 @@ Proof.
   exploit eval_add. eexact E2. eexact E3. intros [v5 [E5 L5]].
   exploit eval_add. eexact E5. eexact E4. intros [v6 [E6 L6]].
   exists (Val.longofwords v6 (Val.loword p)); split.
-  EvalOp. eapply eval_builtin_2; eauto. UseHelper. 
+  EvalOp. eapply eval_builtin_2; eauto. simpl; auto 20. UseHelper. 
   intros. unfold le1, p in *; subst; simpl in *.
   inv L3. inv L4. inv L5. simpl in L6. inv L6. 
   simpl. f_equal. symmetry. apply Int64.decompose_mul. 
@@ -786,7 +786,7 @@ Proof.
 Qed.
 
 Lemma eval_mullimm:
-  forall n, unary_constructor_sound (fun a => mullimm hf a n) (fun v => Val.mull v (Vlong n)).
+  forall n, unary_constructor_sound (fun a => mullimm a n) (fun v => Val.mull v (Vlong n)).
 Proof.
   unfold mullimm; red; intros.
   predSpec Int64.eq Int64.eq_spec n Int64.zero.
@@ -816,7 +816,7 @@ Proof.
   apply eval_mull_base; auto. apply eval_longconst. 
 Qed.
 
-Theorem eval_mull: binary_constructor_sound (mull hf) Val.mull.
+Theorem eval_mull: binary_constructor_sound mull Val.mull.
 Proof.
   unfold mull; red; intros.
   destruct (is_longconst a) as [p|] eqn:LC1;
@@ -836,7 +836,8 @@ Qed.
 Lemma eval_binop_long:
   forall id sem le a b x y z,
   (forall p q, x = Vlong p -> y = Vlong q -> z = Vlong (sem p q)) ->
-  helper_implements ge id sig_ll_l (x::y::nil) z ->
+  external_implements id sig_ll_l (x::y::nil) z ->
+  In (id, sig_ll_l) i64_helpers ->
   eval_expr ge sp e m le a x ->
   eval_expr ge sp e m le b y ->
   exists v, eval_expr ge sp e m le (binop_long id sem a b) v /\ Val.lessdef z v.
@@ -856,7 +857,7 @@ Theorem eval_divl:
   eval_expr ge sp e m le a x ->
   eval_expr ge sp e m le b y ->
   Val.divls x y = Some z ->
-  exists v, eval_expr ge sp e m le (divl hf a b) v /\ Val.lessdef z v.
+  exists v, eval_expr ge sp e m le (divl a b) v /\ Val.lessdef z v.
 Proof.
   intros. eapply eval_binop_long; eauto. 
   intros; subst; simpl in H1.
@@ -864,6 +865,7 @@ Proof.
          || Int64.eq p (Int64.repr Int64.min_signed) && Int64.eq q Int64.mone); inv H1. 
   auto.
   UseHelper. 
+  simpl; auto 20.
 Qed.
 
 Theorem eval_modl:
@@ -871,7 +873,7 @@ Theorem eval_modl:
   eval_expr ge sp e m le a x ->
   eval_expr ge sp e m le b y ->
   Val.modls x y = Some z ->
-  exists v, eval_expr ge sp e m le (modl hf a b) v /\ Val.lessdef z v.
+  exists v, eval_expr ge sp e m le (modl a b) v /\ Val.lessdef z v.
 Proof.
   intros. eapply eval_binop_long; eauto. 
   intros; subst; simpl in H1.
@@ -879,6 +881,7 @@ Proof.
          || Int64.eq p (Int64.repr Int64.min_signed) && Int64.eq q Int64.mone); inv H1. 
   auto.
   UseHelper. 
+  simpl; auto 20.
 Qed.
 
 Theorem eval_divlu:
@@ -886,14 +889,14 @@ Theorem eval_divlu:
   eval_expr ge sp e m le a x ->
   eval_expr ge sp e m le b y ->
   Val.divlu x y = Some z ->
-  exists v, eval_expr ge sp e m le (divlu hf a b) v /\ Val.lessdef z v.
+  exists v, eval_expr ge sp e m le (divlu a b) v /\ Val.lessdef z v.
 Proof.
   intros. unfold divlu. 
-  set (default := Eexternal (i64_udiv hf) sig_ll_l (a ::: b ::: Enil)).
+  set (default := Eexternal i64_udiv sig_ll_l (a ::: b ::: Enil)).
   assert (DEFAULT:
     exists v, eval_expr ge sp e m le default v /\ Val.lessdef z v).
   {
-    econstructor; split. eapply eval_helper_2; eauto. UseHelper. auto. 
+    econstructor; split. eapply eval_helper_2; eauto. simpl; auto 20. UseHelper. auto. 
   }
   destruct (is_longconst a) as [p|] eqn:LC1;
   destruct (is_longconst b) as [q|] eqn:LC2.
@@ -929,14 +932,14 @@ Theorem eval_modlu:
   eval_expr ge sp e m le a x ->
   eval_expr ge sp e m le b y ->
   Val.modlu x y = Some z ->
-  exists v, eval_expr ge sp e m le (modlu hf a b) v /\ Val.lessdef z v.
+  exists v, eval_expr ge sp e m le (modlu a b) v /\ Val.lessdef z v.
 Proof.
   intros. unfold modlu. 
-  set (default := Eexternal (i64_umod hf) sig_ll_l (a ::: b ::: Enil)).
+  set (default := Eexternal i64_umod sig_ll_l (a ::: b ::: Enil)).
   assert (DEFAULT:
     exists v, eval_expr ge sp e m le default v /\ Val.lessdef z v).
   {
-    econstructor; split. eapply eval_helper_2; eauto. UseHelper. auto. 
+    econstructor; split. eapply eval_helper_2; eauto. simpl; auto 20. UseHelper. auto. 
   }
   destruct (is_longconst a) as [p|] eqn:LC1;
   destruct (is_longconst b) as [q|] eqn:LC2.
diff --git a/backend/Selection.v b/backend/Selection.v
index cd17b9fd..11125856 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -66,8 +66,6 @@ Definition store (chunk: memory_chunk) (e1 e2: expr) :=
 
 Section SELECTION.
 
-Variable hf: helper_functions.
-
 Definition sel_constant (cst: Cminor.constant) : expr :=
   match cst with
   | Cminor.Ointconst n => Eop (Ointconst n) Enil
@@ -100,19 +98,19 @@ Definition sel_unop (op: Cminor.unary_operation) (arg: expr) : expr :=
   | Cminor.Ointuofsingle => intuofsingle arg
   | Cminor.Osingleofint => singleofint arg
   | Cminor.Osingleofintu => singleofintu arg
-  | Cminor.Onegl => negl hf arg
+  | Cminor.Onegl => negl arg
   | Cminor.Onotl => notl arg
   | Cminor.Ointoflong => intoflong arg
   | Cminor.Olongofint => longofint arg
   | Cminor.Olongofintu => longofintu arg
-  | Cminor.Olongoffloat => longoffloat hf arg
-  | Cminor.Olonguoffloat => longuoffloat hf arg
-  | Cminor.Ofloatoflong => floatoflong hf arg
-  | Cminor.Ofloatoflongu => floatoflongu hf arg
-  | Cminor.Olongofsingle => longofsingle hf arg
-  | Cminor.Olonguofsingle => longuofsingle hf arg
-  | Cminor.Osingleoflong => singleoflong hf arg
-  | Cminor.Osingleoflongu => singleoflongu hf arg
+  | Cminor.Olongoffloat => longoffloat arg
+  | Cminor.Olonguoffloat => longuoffloat arg
+  | Cminor.Ofloatoflong => floatoflong arg
+  | Cminor.Ofloatoflongu => floatoflongu arg
+  | Cminor.Olongofsingle => longofsingle arg
+  | Cminor.Olonguofsingle => longuofsingle arg
+  | Cminor.Osingleoflong => singleoflong arg
+  | Cminor.Osingleoflongu => singleoflongu arg
   end.
 
 Definition sel_binop (op: Cminor.binary_operation) (arg1 arg2: expr) : expr :=
@@ -138,19 +136,19 @@ Definition sel_binop (op: Cminor.binary_operation) (arg1 arg2: expr) : expr :=
   | Cminor.Osubfs => subfs arg1 arg2
   | Cminor.Omulfs => mulfs arg1 arg2
   | Cminor.Odivfs => divfs arg1 arg2
-  | Cminor.Oaddl => addl hf arg1 arg2
-  | Cminor.Osubl => subl hf arg1 arg2
-  | Cminor.Omull => mull hf arg1 arg2
-  | Cminor.Odivl => divl hf arg1 arg2
-  | Cminor.Odivlu => divlu hf arg1 arg2
-  | Cminor.Omodl => modl hf arg1 arg2
-  | Cminor.Omodlu => modlu hf arg1 arg2
+  | Cminor.Oaddl => addl arg1 arg2
+  | Cminor.Osubl => subl arg1 arg2
+  | Cminor.Omull => mull arg1 arg2
+  | Cminor.Odivl => divl arg1 arg2
+  | Cminor.Odivlu => divlu arg1 arg2
+  | Cminor.Omodl => modl arg1 arg2
+  | Cminor.Omodlu => modlu arg1 arg2
   | Cminor.Oandl => andl arg1 arg2
   | Cminor.Oorl => orl arg1 arg2
   | Cminor.Oxorl => xorl arg1 arg2
-  | Cminor.Oshll => shll hf arg1 arg2
-  | Cminor.Oshrl => shrl hf arg1 arg2
-  | Cminor.Oshrlu => shrlu hf arg1 arg2
+  | Cminor.Oshll => shll arg1 arg2
+  | Cminor.Oshrl => shrl arg1 arg2
+  | Cminor.Oshrlu => shrlu arg1 arg2
   | Cminor.Ocmp c => comp c arg1 arg2
   | Cminor.Ocmpu c => compu c arg1 arg2
   | Cminor.Ocmpf c => compf c arg1 arg2
@@ -248,7 +246,7 @@ Definition sel_switch_long :=
   sel_switch
     (fun arg n => cmpl Ceq arg (longconst (Int64.repr n)))
     (fun arg n => cmplu Clt arg (longconst (Int64.repr n)))
-    (fun arg ofs => subl hf arg (longconst (Int64.repr ofs)))
+    (fun arg ofs => subl arg (longconst (Int64.repr ofs)))
     lowlong.
 
 (** Conversion from Cminor statements to Cminorsel statements. *)
@@ -303,8 +301,8 @@ End SELECTION.
 
 (** Conversion of functions. *)
 
-Definition sel_function (hf: helper_functions) (ge: Cminor.genv) (f: Cminor.function) : res function :=
-  do body' <- sel_stmt hf ge f.(Cminor.fn_body);
+Definition sel_function (ge: Cminor.genv) (f: Cminor.function) : res function :=
+  do body' <- sel_stmt ge f.(Cminor.fn_body);
   OK (mkfunction
         f.(Cminor.fn_sig)
         f.(Cminor.fn_params)
@@ -312,12 +310,13 @@ Definition sel_function (hf: helper_functions) (ge: Cminor.genv) (f: Cminor.func
         f.(Cminor.fn_stackspace)
         body').
 
-Definition sel_fundef (hf: helper_functions) (ge: Cminor.genv) (f: Cminor.fundef) : res fundef :=
-  transf_partial_fundef (sel_function hf ge) f.
+Definition sel_fundef (ge: Cminor.genv) (f: Cminor.fundef) : res fundef :=
+  transf_partial_fundef (sel_function ge) f.
 
 (** Conversion of programs. *)
 
 Definition sel_program (p: Cminor.program) : res program :=
   let ge := Genv.globalenv p in
-  do hf <- get_helpers ge; transform_partial_program (sel_fundef hf ge) p.
+  do x <- check_helpers ge;
+  transform_partial_program (sel_fundef ge) p.
 
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index 672853e3..bb9bd592 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -46,9 +46,9 @@ Variable prog: Cminor.program.
 Variable tprog: CminorSel.program.
 Let ge := Genv.globalenv prog.
 Let tge := Genv.globalenv tprog.
-Variable hf: helper_functions.
-Hypothesis HELPERS: i64_helpers_correct tge hf.
-Hypothesis TRANSFPROG: transform_partial_program (sel_fundef hf ge) prog = OK tprog.
+Hypothesis HELPERS:
+  forall name sg, In (name, sg) i64_helpers -> helper_declared ge name sg.
+Hypothesis TRANSFPROG: transform_partial_program (sel_fundef ge) prog = OK tprog.
 
 Lemma symbols_preserved:
   forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
@@ -65,7 +65,7 @@ Qed.
 Lemma function_ptr_translated:
   forall (b: block) (f: Cminor.fundef),
   Genv.find_funct_ptr ge b = Some f ->
-  exists tf, Genv.find_funct_ptr tge b = Some tf /\ sel_fundef hf ge f = OK tf.
+  exists tf, Genv.find_funct_ptr tge b = Some tf /\ sel_fundef ge f = OK tf.
 Proof.  
   intros. eapply Genv.find_funct_ptr_transf_partial; eauto.
 Qed.
@@ -74,7 +74,7 @@ Lemma functions_translated:
   forall (v v': val) (f: Cminor.fundef),
   Genv.find_funct ge v = Some f ->
   Val.lessdef v v' ->
-  exists tf, Genv.find_funct tge v' = Some tf /\ sel_fundef hf ge f = OK tf.
+  exists tf, Genv.find_funct tge v' = Some tf /\ sel_fundef ge f = OK tf.
 Proof.  
   intros. inv H0.
   eapply Genv.find_funct_transf_partial; eauto.
@@ -82,13 +82,13 @@ Proof.
 Qed.
 
 Lemma sig_function_translated:
-  forall f tf, sel_fundef hf ge f = OK tf -> funsig tf = Cminor.funsig f.
+  forall f tf, sel_fundef ge f = OK tf -> funsig tf = Cminor.funsig f.
 Proof.
   intros. destruct f; monadInv H; auto. monadInv EQ. auto. 
 Qed.
 
 Lemma stackspace_function_translated:
-  forall f tf, sel_function hf ge f = OK tf -> fn_stackspace tf = Cminor.fn_stackspace f.
+  forall f tf, sel_function ge f = OK tf -> fn_stackspace tf = Cminor.fn_stackspace f.
 Proof.
   intros. monadInv H. auto. 
 Qed.
@@ -99,38 +99,18 @@ Proof.
   intros; eapply Genv.find_var_info_transf_partial; eauto.
 Qed.
 
-Lemma helper_implements_preserved:
-  forall id sg vargs vres,
-  helper_implements ge id sg vargs vres ->
-  helper_implements tge id sg vargs vres.
+Lemma helper_declared_preserved:
+  forall id sg, helper_declared ge id sg -> helper_declared tge id sg.
 Proof.
-  intros. destruct H as (b & ef & A & B & C & D).
+  intros id sg (b & A & B).
   exploit function_ptr_translated; eauto. simpl. intros (tf & P & Q). inv Q. 
-  exists b; exists ef. 
-  split. rewrite symbols_preserved. auto.
-  split. auto.
-  split. auto.
-  intros. eapply external_call_symbols_preserved; eauto. 
-  exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
-Qed.
-
-Lemma builtin_implements_preserved:
-  forall id sg vargs vres,
-  builtin_implements ge id sg vargs vres ->
-  builtin_implements tge id sg vargs vres.
-Proof.
-  unfold builtin_implements; intros.
-  eapply external_call_symbols_preserved; eauto. 
-  exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
+  exists b; split; auto. rewrite symbols_preserved. auto.
 Qed.
 
-Lemma helpers_correct_preserved:
-  forall h, i64_helpers_correct ge h -> i64_helpers_correct tge h.
+Let HELPERS':
+  forall name sg, In (name, sg) i64_helpers -> helper_declared tge name sg.
 Proof.
-  unfold i64_helpers_correct; intros.
-  repeat (match goal with [ H: _ /\ _ |- _ /\ _ ] => destruct H; split end);
-  intros; try (eapply helper_implements_preserved; eauto);
-  try (eapply builtin_implements_preserved; eauto).
+  intros. apply helper_declared_preserved. auto.
 Qed.
 
 Section CMCONSTR.
@@ -192,7 +172,7 @@ Lemma eval_sel_unop:
   forall le op a1 v1 v,
   eval_expr tge sp e m le a1 v1 ->
   eval_unop op v1 = Some v ->
-  exists v', eval_expr tge sp e m le (sel_unop hf op a1) v' /\ Val.lessdef v v'.
+  exists v', eval_expr tge sp e m le (sel_unop op a1) v' /\ Val.lessdef v v'.
 Proof.
   destruct op; simpl; intros; FuncInv; try subst v.
   apply eval_cast8unsigned; auto.
@@ -235,7 +215,7 @@ Lemma eval_sel_binop:
   eval_expr tge sp e m le a1 v1 ->
   eval_expr tge sp e m le a2 v2 ->
   eval_binop op v1 v2 m = Some v ->
-  exists v', eval_expr tge sp e m le (sel_binop hf op a1 a2) v' /\ Val.lessdef v v'.
+  exists v', eval_expr tge sp e m le (sel_binop op a1 a2) v' /\ Val.lessdef v v'.
 Proof.
   destruct op; simpl; intros; FuncInv; try subst v.
   apply eval_add; auto.
@@ -456,7 +436,7 @@ Lemma sel_switch_long_correct:
   forall dfl cases arg sp e m i t le,
   validate_switch Int64.modulus dfl cases t = true ->
   eval_expr tge sp e m le arg (Vlong i) ->
-  eval_exitexpr tge sp e m le (XElet arg (sel_switch_long hf O t)) (switch_target (Int64.unsigned i) dfl cases).
+  eval_exitexpr tge sp e m le (XElet arg (sel_switch_long O t)) (switch_target (Int64.unsigned i) dfl cases).
 Proof.
   intros. eapply sel_switch_correct with (R := Rlong); eauto.
 - intros until n; intros EVAL R RANGE.
@@ -470,7 +450,7 @@ Proof.
   rewrite Int64.unsigned_repr. destruct (zlt (Int64.unsigned n0) n); auto. 
   unfold Int64.max_unsigned; omega.
 - intros until n; intros EVAL R RANGE.
-  exploit eval_subl. eexact HELPERS. eexact EVAL. apply eval_longconst with (n := Int64.repr n).
+  exploit eval_subl.  eexact EVAL. apply eval_longconst with (n := Int64.repr n).
   intros (vb & A & B).
   inv R. simpl in B. inv B. econstructor; split; eauto. 
   replace ((Int64.unsigned n0 - n) mod Int64.modulus)
@@ -564,7 +544,7 @@ Lemma sel_expr_correct:
   Cminor.eval_expr ge sp e m a v ->
   forall e' le m',
   env_lessdef e e' -> Mem.extends m m' ->
-  exists v', eval_expr tge sp e' m' le (sel_expr hf a) v' /\ Val.lessdef v v'.
+  exists v', eval_expr tge sp e' m' le (sel_expr a) v' /\ Val.lessdef v v'.
 Proof.
   induction 1; intros; simpl.
   (* Evar *)
@@ -601,7 +581,7 @@ Lemma sel_exprlist_correct:
   Cminor.eval_exprlist ge sp e m a v ->
   forall e' le m',
   env_lessdef e e' -> Mem.extends m m' ->
-  exists v', eval_exprlist tge sp e' m' le (sel_exprlist hf a) v' /\ Val.lessdef_list v v'.
+  exists v', eval_exprlist tge sp e' m' le (sel_exprlist a) v' /\ Val.lessdef_list v v'.
 Proof.
   induction 1; intros; simpl. 
   exists (@nil val); split; auto. constructor.
@@ -616,21 +596,21 @@ Inductive match_cont: Cminor.cont -> CminorSel.cont -> Prop :=
   | match_cont_stop:
       match_cont Cminor.Kstop Kstop
   | match_cont_seq: forall s s' k k',
-      sel_stmt hf ge s = OK s' ->
+      sel_stmt ge s = OK s' ->
       match_cont k k' ->
       match_cont (Cminor.Kseq s k) (Kseq s' k')
   | match_cont_block: forall k k',
       match_cont k k' ->
       match_cont (Cminor.Kblock k) (Kblock k')
   | match_cont_call: forall id f sp e k f' e' k',
-      sel_function hf ge f = OK f' ->
+      sel_function ge f = OK f' ->
       match_cont k k' -> env_lessdef e e' ->
       match_cont (Cminor.Kcall id f sp e k) (Kcall id f' sp e' k').
 
 Inductive match_states: Cminor.state -> CminorSel.state -> Prop :=
   | match_state: forall f f' s k s' k' sp e m e' m'
-        (TF: sel_function hf ge f = OK f')
-        (TS: sel_stmt hf ge s = OK s')
+        (TF: sel_function ge f = OK f')
+        (TS: sel_stmt ge s = OK s')
         (MC: match_cont k k')
         (LD: env_lessdef e e')
         (ME: Mem.extends m m'),
@@ -638,7 +618,7 @@ Inductive match_states: Cminor.state -> CminorSel.state -> Prop :=
         (Cminor.State f s k sp e m)
         (State f' s' k' sp e' m')
   | match_callstate: forall f f' args args' k k' m m'
-        (TF: sel_fundef hf ge f = OK f')
+        (TF: sel_fundef ge f = OK f')
         (MC: match_cont k k')
         (LD: Val.lessdef_list args args')
         (ME: Mem.extends m m'),
@@ -653,7 +633,7 @@ Inductive match_states: Cminor.state -> CminorSel.state -> Prop :=
         (Cminor.Returnstate v k m)
         (Returnstate v' k' m')
   | match_builtin_1: forall ef args args' optid f sp e k m al f' e' k' m'
-        (TF: sel_function hf ge f = OK f')
+        (TF: sel_function ge f = OK f')
         (MC: match_cont k k')
         (LDA: Val.lessdef_list args args')
         (LDE: env_lessdef e e')
@@ -663,7 +643,7 @@ Inductive match_states: Cminor.state -> CminorSel.state -> Prop :=
         (Cminor.Callstate (External ef) args (Cminor.Kcall optid f sp e k) m)
         (State f' (Sbuiltin optid ef al) k' sp e' m')
   | match_builtin_2: forall v v' optid f sp e k m f' e' m' k'
-        (TF: sel_function hf ge f = OK f')
+        (TF: sel_function ge f = OK f')
         (MC: match_cont k k')
         (LDV: Val.lessdef v v')
         (LDE: env_lessdef e e')
@@ -681,16 +661,16 @@ Qed.
 Remark find_label_commut:
   forall lbl s k s' k',
   match_cont k k' ->
-  sel_stmt hf ge s = OK s' ->
+  sel_stmt ge s = OK s' ->
   match Cminor.find_label lbl s k, find_label lbl s' k' with
   | None, None => True
-  | Some(s1, k1), Some(s1', k1') => sel_stmt hf ge s1 = OK s1' /\ match_cont k1 k1'
+  | Some(s1, k1), Some(s1', k1') => sel_stmt ge s1 = OK s1' /\ match_cont k1 k1'
   | _, _ => False
   end.
 Proof.
   induction s; intros until k'; simpl; intros MC SE; try (monadInv SE); simpl; auto.
 (* store *)
-  unfold store. destruct (addressing m (sel_expr hf e)); simpl; auto.
+  unfold store. destruct (addressing m (sel_expr e)); simpl; auto.
 (* call *)
   destruct (classify_call ge e); simpl; auto.
 (* tailcall *)
@@ -854,7 +834,7 @@ Proof.
 - (* Slabel *)
   left; econstructor; split. constructor. constructor; auto.
 - (* Sgoto *)
-  assert (sel_stmt hf ge (Cminor.fn_body f) = OK (fn_body f')).
+  assert (sel_stmt ge (Cminor.fn_body f) = OK (fn_body f')).
   { monadInv TF; simpl; auto. }
   exploit (find_label_commut lbl (Cminor.fn_body f) (Cminor.call_cont k)).
     apply call_cont_commut; eauto. eauto.
@@ -922,19 +902,39 @@ Qed.
 
 End PRESERVATION.
 
-Axiom get_helpers_correct:
-  forall ge hf, get_helpers ge = OK hf -> i64_helpers_correct ge hf.
+Lemma check_helper_correct:
+  forall ge name sg res,
+  check_helper ge (name, sg) = OK res -> helper_declared ge name sg.
+Proof with (try discriminate).
+  unfold check_helper; intros. 
+  destruct (Genv.find_symbol ge name) as [b|] eqn:FS...
+  destruct (Genv.find_funct_ptr ge b) as [fd|] eqn:FP...
+  destruct fd... destruct e... destruct (ident_eq name0 name)... 
+  destruct (signature_eq sg0 sg)... 
+  subst. exists b; auto.
+Qed.
+
+Lemma check_helpers_correct:
+  forall ge res, check_helpers ge = OK res ->
+  forall name sg, In (name, sg) i64_helpers -> helper_declared ge name sg.
+Proof.
+  unfold check_helpers; intros ge res CH name sg. 
+  monadInv CH. generalize (mmap_inversion _ _ EQ). 
+  generalize i64_helpers x. induction 1; simpl; intros.
+  contradiction.
+  destruct H1. subst a1. eapply check_helper_correct; eauto. eauto. 
+Qed.
 
 Theorem transf_program_correct:
   forall prog tprog,
   sel_program prog = OK tprog ->
   forward_simulation (Cminor.semantics prog) (CminorSel.semantics tprog).
 Proof.
-  intros. unfold sel_program in H. 
-  destruct (get_helpers (Genv.globalenv prog)) as [hf|] eqn:E; simpl in H; try discriminate.
-  apply forward_simulation_opt with (match_states := match_states prog tprog hf) (measure := measure). 
+  intros. unfold sel_program in H. set (ge := Genv.globalenv prog) in *.
+  destruct (check_helpers ge) eqn:CH; simpl in H; try discriminate.
+  apply forward_simulation_opt with (match_states := match_states prog tprog) (measure := measure). 
   eapply public_preserved; eauto.
   apply sel_initial_states; auto.
   apply sel_final_states; auto.
-  apply sel_step_correct; auto. eapply helpers_correct_preserved; eauto. apply get_helpers_correct. auto.
+  apply sel_step_correct; auto. eapply check_helpers_correct; eauto.
 Qed.
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 118b6d2d..584c265a 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -188,7 +188,60 @@ let builtins_generic = {
     "__compcert_va_float64",
         (TFloat(FDouble, []),
           [TPtr(TVoid [], [])],
-          false)
+          false);
+  (* Helper functions for int64 arithmetic *)
+    "__i64_dtos",
+        (TInt(ILongLong, []),
+         [TFloat(FDouble, [])],
+         false);
+    "__i64_dtou",
+        (TInt(IULongLong, []),
+         [TFloat(FDouble, [])],
+         false);
+    "__i64_stod",
+        (TFloat(FDouble, []),
+         [TInt(ILongLong, [])],
+         false);
+    "__i64_utod",
+        (TFloat(FDouble, []),
+         [TInt(IULongLong, [])],
+         false);
+    "__i64_stof",
+        (TFloat(FFloat, []),
+         [TInt(ILongLong, [])],
+         false);
+    "__i64_utof",
+        (TFloat(FFloat, []),
+         [TInt(IULongLong, [])],
+         false);
+    "__i64_sdiv",
+        (TInt(ILongLong, []),
+         [TInt(ILongLong, []); TInt(ILongLong, [])],
+         false);
+    "__i64_udiv",
+        (TInt(IULongLong, []),
+         [TInt(IULongLong, []); TInt(IULongLong, [])],
+         false);
+    "__i64_smod",
+        (TInt(ILongLong, []),
+         [TInt(ILongLong, []); TInt(ILongLong, [])],
+         false);
+    "__i64_umod",
+        (TInt(IULongLong, []),
+         [TInt(IULongLong, []); TInt(IULongLong, [])],
+         false);
+    "__i64_shl",
+        (TInt(ILongLong, []),
+         [TInt(ILongLong, []); TInt(IInt, [])],
+         false);
+    "__i64_shr",
+        (TInt(IULongLong, []),
+         [TInt(IULongLong, []); TInt(IInt, [])],
+         false);
+    "__i64_sar",
+        (TInt(ILongLong, []),
+         [TInt(ILongLong, []); TInt(IInt, [])],
+         false)
   ]
 }
 
diff --git a/extraction/extraction.v b/extraction/extraction.v
index ee496ffa..94ac6f52 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -57,12 +57,6 @@ Extract Constant Iteration.GenIter.iterate =>
 
 (* Selection *)
 
-Extract Constant SelectLong.get_helper =>
-  "fun ge s sg ->
-     Errors.OK (Camlcoq.intern_string (Camlcoq.camlstring_of_coqstring s))".
-Extract Constant SelectLong.get_builtin =>
-  "fun s sg ->
-     Errors.OK (Camlcoq.intern_string (Camlcoq.camlstring_of_coqstring s))".
 Extract Constant Selection.compile_switch => "Switchaux.compile_switch".
 
 (* RTLgen *)