Use Coq strings instead of idents to name external and builtin functions.

The AST.ident type represents source-level identifiers as unique positive numbers.  However, the mapping identifiers <-> AST.ident differs between runs of CompCert on different source files.  This is problematic when we need to produce or recognize external functions and builtin functions with fixed names, for example:
* in $ARCH/Machregs.v to define the register conventions for builtin functions;
* in the VST program logic from Princeton to treat thread primitives specially.

So far, we used AST.ident_of_string to recover the ident associated with a string.  However, this function is defined in OCaml and doesn't execute within Coq.  This is a problem both for VST and for future executability of CompCert within Coq.

This commit replaces "ident" by "string" in the arguments of EF_external, EF_builtin, EF_inline_asm, EF_annot, and EF_annot_val.  This provides stable names for externals and builtins, as needed.  For inline asm and annotations, it's a matter of taste, but using strings feels more natural.  EF_debug keeps using idents, since some kinds of EF_debug annotations talk about program variables.

5 files changed, 347 insertions, 255 deletions

diff --git a/backend/CMparser.mly b/backend/CMparser.mly
index b48a486e..41bd35a1 100644
--- a/backend/CMparser.mly
+++ b/backend/CMparser.mly
@@ -35,9 +35,9 @@ type ef_token =
 let mkef sg toks =
   match toks with
   | [EFT_tok "extern"; EFT_string s] ->
-      EF_external(intern_string s, sg)
+      EF_external(coqstring_of_camlstring s, sg)
   | [EFT_tok "builtin"; EFT_string s] ->
-      EF_builtin(intern_string s, sg)
+      EF_builtin(coqstring_of_camlstring s, sg)
   | [EFT_tok "volatile"; EFT_tok "load"; EFT_chunk c] ->
       EF_vload c
   | [EFT_tok "volatile"; EFT_tok "store"; EFT_chunk c] ->
@@ -49,12 +49,12 @@ let mkef sg toks =
   | [EFT_tok "memcpy"; EFT_tok "size"; EFT_int sz; EFT_tok "align"; EFT_int al] ->
       EF_memcpy(Z.of_sint32 sz, Z.of_sint32 al)
   | [EFT_tok "annot"; EFT_string txt] ->
-      EF_annot(intern_string txt, sg.sig_args)
+      EF_annot(coqstring_of_camlstring txt, sg.sig_args)
   | [EFT_tok "annot_val"; EFT_string txt] ->
       if sg.sig_args = [] then raise Parsing.Parse_error;
-      EF_annot_val(intern_string txt, List.hd sg.sig_args)
+      EF_annot_val(coqstring_of_camlstring txt, List.hd sg.sig_args)
   | [EFT_tok "inline_asm"; EFT_string txt] ->
-      EF_inline_asm(intern_string txt, sg, [])
+      EF_inline_asm(coqstring_of_camlstring txt, sg, [])
   | _ ->
       raise Parsing.Parse_error
 
@@ -473,7 +473,7 @@ proc:
                         fn_stackspace = $8;
                         fn_body = $10 })) }
   | EXTERN STRINGLIT COLON signature 
-      { (intern_string $2, Gfun(External(EF_external(intern_string $2,$4)))) }
+      { (intern_string $2, Gfun(External(EF_external(coqstring_of_camlstring $2,$4)))) }
   | EXTERN STRINGLIT EQUAL eftoks COLON signature
       { (intern_string $2, Gfun(External(mkef $6 $4))) }
 ;
diff --git a/backend/SelectLong.vp b/backend/SelectLong.vp
index 970386a9..105b284c 100644
--- a/backend/SelectLong.vp
+++ b/backend/SelectLong.vp
@@ -12,6 +12,7 @@
 
 (** Instruction selection for 64-bit integer operations *)
 
+Require String.
 Require Import Coqlib.
 Require Import AST.
 Require Import Integers.
@@ -24,26 +25,24 @@ Local Open Scope cminorsel_scope.
 Local Open Scope string_scope.
 
 (** Some operations on 64-bit integers are transformed into calls to
-  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".
+  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_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) cc_default.
 Definition sig_l_f := mksignature (Tlong :: nil) (Some Tfloat) cc_default.
@@ -55,6 +54,8 @@ 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).
 
@@ -121,28 +122,28 @@ Definition longofintu (e: expr) :=
 Definition negl (e: expr) :=
   match is_longconst e with
   | Some n => longconst (Int64.neg n)
-  | None => Ebuiltin (EF_builtin i64_neg sig_l_l) (e ::: Enil)
+  | None => Ebuiltin (EF_builtin "__builtin_negl" 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 i64_dtos sig_f_l (arg ::: Enil).
+  Eexternal hf.(i64_dtos) sig_f_l (arg ::: Enil).
 Definition longuoffloat (arg: expr) :=
-  Eexternal i64_dtou sig_f_l (arg ::: Enil).
+  Eexternal hf.(i64_dtou) sig_f_l (arg ::: Enil).
 Definition floatoflong (arg: expr) :=
-  Eexternal i64_stod sig_l_f (arg ::: Enil).
+  Eexternal hf.(i64_stod) sig_l_f (arg ::: Enil).
 Definition floatoflongu (arg: expr) :=
-  Eexternal i64_utod sig_l_f (arg ::: Enil).
+  Eexternal hf.(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 i64_stof sig_l_s (arg ::: Enil).
+  Eexternal hf.(i64_stof) sig_l_s (arg ::: Enil).
 Definition singleoflongu (arg: expr) :=
-  Eexternal i64_utof sig_l_s (arg ::: Enil).
+  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)).
@@ -163,7 +164,7 @@ Definition shllimm (e1: expr) (n: int) :=
     makelong (shlimm (lowlong e1) (Int.sub n Int.iwordsize))
              (Eop (Ointconst Int.zero) Enil)
   else
-    Eexternal i64_shl sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil).
+    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
@@ -175,7 +176,7 @@ Definition shrluimm (e1: expr) (n: int) :=
     makelong (Eop (Ointconst Int.zero) Enil)
              (shruimm (highlong e1) (Int.sub n Int.iwordsize))
   else
-    Eexternal i64_shr sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil).
+    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
@@ -188,7 +189,7 @@ Definition shrlimm (e1: expr) (n: int) :=
       (makelong (shrimm (Eletvar 0) (Int.repr 31))
                 (shrimm (Eletvar 0) (Int.sub n Int.iwordsize)))
   else
-    Eexternal i64_sar sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil).
+    Eexternal hf.(i64_sar) sig_li_l (e1 ::: Eop (Ointconst n) Enil ::: Enil).
 
 Definition is_intconst (e: expr) :=
   match e with
@@ -199,23 +200,23 @@ Definition is_intconst (e: expr) :=
 Definition shll (e1 e2: expr) :=
   match is_intconst e2 with
   | Some n => shllimm e1 n
-  | None => Eexternal i64_shl sig_li_l (e1 ::: e2 ::: Enil)
+  | 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 i64_shr sig_li_l (e1 ::: e2 ::: Enil)
+  | 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 i64_sar sig_li_l (e1 ::: e2 ::: Enil)
+  | None => Eexternal hf.(i64_sar) sig_li_l (e1 ::: e2 ::: Enil)
   end.
 
 Definition addl (e1 e2: expr) :=
-  let default := Ebuiltin (EF_builtin i64_add sig_ll_l) (e1 ::: e2 ::: Enil) in
+  let default := Ebuiltin (EF_builtin "__builtin_addl" 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
@@ -224,7 +225,7 @@ Definition addl (e1 e2: expr) :=
   end.
 
 Definition subl (e1 e2: expr) :=
-  let default := Ebuiltin (EF_builtin i64_sub sig_ll_l) (e1 ::: e2 ::: Enil) in
+  let default := Ebuiltin (EF_builtin "__builtin_subl" 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
@@ -234,7 +235,7 @@ Definition subl (e1 e2: expr) :=
 
 Definition mull_base (e1 e2: expr) :=
   splitlong2 e1 e2 (fun h1 l1 h2 l2 =>
-    Elet (Ebuiltin (EF_builtin i64_mul sig_ii_l) (l1 ::: l2 ::: Enil))
+    Elet (Ebuiltin (EF_builtin "__builtin_mull" sig_ii_l) (l1 ::: l2 ::: Enil))
       (makelong
         (add (add (Eop Ohighlong (Eletvar O ::: Enil))
                   (mul (lift l1) (lift h2)))
@@ -263,11 +264,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 i64_sdiv Int64.divs.
-Definition modl := binop_long i64_smod Int64.mods.
+Definition divl e1 e2 := binop_long hf.(i64_sdiv) Int64.divs e1 e2.
+Definition modl e1 e2 := binop_long hf.(i64_smod) Int64.mods e1 e2.
 
 Definition divlu (e1 e2: expr) :=
-  let default := Eexternal i64_udiv sig_ll_l (e1 ::: e2 ::: Enil) in
+  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 =>
@@ -279,7 +280,7 @@ Definition divlu (e1 e2: expr) :=
   end.
 
 Definition modlu (e1 e2: expr) :=
-  let default := Eexternal i64_umod sig_ll_l (e1 ::: e2 ::: Enil) in
+  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 =>
@@ -359,45 +360,3 @@ Definition cmpl (c: comparison) (e1 e2: expr) :=
   end.
 
 End SELECT.
-
-(** Checking that the helper functions are available. *)
-
-Require Import Errors.
-Require Import Globalenvs.
-Local Open Scope error_monad_scope.
-
-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 40c11dd8..cdfb1107 100644
--- a/backend/SelectLongproof.v
+++ b/backend/SelectLongproof.v
@@ -12,6 +12,7 @@
 
 (** Correctness of instruction selection for integer division *)
 
+Require Import String.
 Require Import Coqlib.
 Require Import AST.
 Require Import Errors.
@@ -29,81 +30,96 @@ Require Import SelectOpproof.
 Require Import SelectLong.
 
 Open Local Scope cminorsel_scope.
+Open Local Scope string_scope.
 
 (** * Axiomatization of the helper functions *)
 
-Definition external_implements (id: ident) (sg: signature) (vargs: list val) (vres: val) : Prop :=
+Definition external_implements (name: string) (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.
+  external_call (EF_external name sg) ge vargs m E0 vres m.
 
-Definition builtin_implements (id: ident) (sg: signature) (vargs: list val) (vres: val) : Prop :=
+Definition builtin_implements (name: string) (sg: signature) (vargs: list val) (vres: val) : Prop :=
   forall F V (ge: Genv.t F V) m,
-  external_call (EF_builtin id sg) ge vargs m E0 vres m.
+  external_call (EF_builtin name 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
+    (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 "__builtin_negl" sig_l_l (x::nil) (Val.negl x))
+ /\ (forall x y, builtin_implements "__builtin_addl" sig_ll_l (x::y::nil) (Val.addl x y))
+ /\ (forall x y, builtin_implements "__builtin_subl" sig_ll_l (x::y::nil) (Val.subl x y))
+ /\ (forall x y, builtin_implements "__builtin_mull" 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) (id: ident) (name: string) (sg: signature) : Prop :=
+  exists b, Genv.find_symbol ge id = Some b
          /\ Genv.find_funct_ptr ge b = Some (External (EF_external name sg)).
 
+Definition helper_functions_declared {F V: Type} (ge: Genv.t (AST.fundef F) V) (hf: helper_functions) : Prop :=
+     helper_declared ge hf.(i64_dtos) "__i64_dtos" sig_f_l
+  /\ helper_declared ge hf.(i64_dtou) "__i64_dtou" sig_f_l
+  /\ helper_declared ge hf.(i64_stod) "__i64_stod" sig_l_f
+  /\ helper_declared ge hf.(i64_utod) "__i64_utod" sig_l_f
+  /\ helper_declared ge hf.(i64_stof) "__i64_stof" sig_l_s
+  /\ helper_declared ge hf.(i64_utof) "__i64_utof" sig_l_s
+  /\ helper_declared ge hf.(i64_sdiv) "__i64_sdiv" sig_ll_l
+  /\ helper_declared ge hf.(i64_udiv) "__i64_udiv" sig_ll_l
+  /\ helper_declared ge hf.(i64_smod) "__i64_smod" sig_ll_l
+  /\ helper_declared ge hf.(i64_umod) "__i64_umod" sig_ll_l
+  /\ helper_declared ge hf.(i64_shl) "__i64_shl" sig_li_l
+  /\ helper_declared ge hf.(i64_shr) "__i64_shr" sig_li_l
+  /\ helper_declared ge hf.(i64_sar) "__i64_sar" sig_li_l.
+
 (** * Correctness of the instruction selection functions for 64-bit operators *)
 
 Section CMCONSTR.
 
 Variable ge: genv.
-Hypothesis HELPERS:
-  forall name sg, In (name, sg) i64_helpers -> helper_declared ge name sg.
+Variable hf: helper_functions.
+Hypothesis HELPERS: helper_functions_declared ge hf.
 Variable sp: val.
 Variable e: env.
 Variable m: mem.
 
-Ltac UseHelper :=
-  generalize i64_helpers_correct; intros;
-  repeat (eauto; match goal with | [ H: _ /\ _ |- _ ] => destruct H end).
+Ltac UseHelper := decompose [Logic.and] i64_helpers_correct; eauto.
+Ltac DeclHelper := red in HELPERS; decompose [Logic.and] HELPERS; eauto.
 
 Lemma eval_helper:
-  forall le id sg args vargs vres,
+  forall le id name sg args vargs vres,
   eval_exprlist ge sp e m le args vargs ->
-  In (id, sg) i64_helpers ->
-  external_implements id sg vargs vres ->
+  helper_declared ge id name sg  ->
+  external_implements name sg vargs vres ->
   eval_expr ge sp e m le (Eexternal id sg args) vres.
 Proof.
-  intros. exploit HELPERS; eauto. intros (b & A & B). econstructor; eauto.
+  intros. destruct H0 as (b & P & Q). econstructor; eauto.
 Qed.
 
 Corollary eval_helper_1:
-  forall le id sg arg1 varg1 vres,
+  forall le id name sg arg1 varg1 vres,
   eval_expr ge sp e m le arg1 varg1 ->
-  In (id, sg) i64_helpers ->
-  external_implements id sg (varg1::nil) vres ->
+  helper_declared ge id name sg  ->
+  external_implements name 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.
 Qed.
 
 Corollary eval_helper_2:
-  forall le id sg arg1 arg2 varg1 varg2 vres,
+  forall le id name sg arg1 arg2 varg1 varg2 vres,
   eval_expr ge sp e m le arg1 varg1 ->
   eval_expr ge sp e m le arg2 varg2 ->
-  In (id, sg) i64_helpers ->
-  external_implements id sg (varg1::varg2::nil) vres ->
+  helper_declared ge id name sg  ->
+  external_implements name 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.
@@ -394,51 +410,47 @@ 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 a) v /\ Val.lessdef y v.
+  exists v, eval_expr ge sp e m le (longoffloat hf a) v /\ Val.lessdef y v.
 Proof.
   intros; unfold longoffloat. econstructor; split. 
-  eapply eval_helper_1; eauto. simpl; auto. UseHelper.
-  auto.
+  eapply eval_helper_1; eauto. DeclHelper. UseHelper. auto.
 Qed.
 
 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 a) v /\ Val.lessdef y v.
+  exists v, eval_expr ge sp e m le (longuoffloat hf a) v /\ Val.lessdef y v.
 Proof.
   intros; unfold longuoffloat. econstructor; split. 
-  eapply eval_helper_1; eauto. simpl; auto. UseHelper. 
-  auto.
+  eapply eval_helper_1; eauto. DeclHelper. UseHelper. auto.
 Qed.
 
 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 a) v /\ Val.lessdef y v.
+  exists v, eval_expr ge sp e m le (floatoflong hf a) v /\ Val.lessdef y v.
 Proof.
   intros; unfold floatoflong. econstructor; split. 
-  eapply eval_helper_1; eauto. simpl; auto. UseHelper. 
-  auto.
+  eapply eval_helper_1; eauto. DeclHelper. UseHelper. auto.
 Qed.
 
 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 a) v /\ Val.lessdef y v.
+  exists v, eval_expr ge sp e m le (floatoflongu hf a) v /\ Val.lessdef y v.
 Proof.
   intros; unfold floatoflongu. econstructor; split. 
-  eapply eval_helper_1; eauto. simpl; auto. UseHelper. 
-  auto.
+  eapply eval_helper_1; eauto. DeclHelper. UseHelper. auto.
 Qed.
 
 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 a) v /\ Val.lessdef y v.
+  exists v, eval_expr ge sp e m le (longofsingle hf 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.
@@ -452,7 +464,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 a) v /\ Val.lessdef y v.
+  exists v, eval_expr ge sp e m le (longuofsingle hf 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.
@@ -466,22 +478,20 @@ 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 a) v /\ Val.lessdef y v.
+  exists v, eval_expr ge sp e m le (singleoflong hf a) v /\ Val.lessdef y v.
 Proof.
   intros; unfold singleoflong. econstructor; split. 
-  eapply eval_helper_1; eauto. simpl; auto 20. UseHelper. 
-  auto.
+  eapply eval_helper_1; eauto. DeclHelper. UseHelper. auto.
 Qed.
 
 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 a) v /\ Val.lessdef y v.
+  exists v, eval_expr ge sp e m le (singleoflongu hf a) v /\ Val.lessdef y v.
 Proof.
   intros; unfold singleoflongu. econstructor; split. 
-  eapply eval_helper_1; eauto. simpl; auto 20. UseHelper. 
-  auto.
+  eapply eval_helper_1; eauto. DeclHelper. UseHelper. auto.
 Qed.
 
 Theorem eval_andl: binary_constructor_sound andl Val.andl.
@@ -578,7 +588,7 @@ Qed.
 
 Lemma eval_shllimm:
   forall n,
-  unary_constructor_sound (fun e => shllimm e n) (fun v => Val.shll v (Vint n)).
+  unary_constructor_sound (fun e => shllimm hf e n) (fun v => Val.shll v (Vint n)).
 Proof.
   unfold shllimm; red; intros.
   apply eval_shift_imm; intros.
@@ -608,11 +618,10 @@ 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. 
-    simpl; auto 20. UseHelper. auto.
+    econstructor; split. eapply eval_helper_2; eauto. EvalOp. DeclHelper. UseHelper. auto.
 Qed.
 
-Theorem eval_shll: binary_constructor_sound shll Val.shll.
+Theorem eval_shll: binary_constructor_sound (shll hf) Val.shll.
 Proof.
   unfold shll; red; intros.
   destruct (is_intconst b) as [n|] eqn:IC.
@@ -620,12 +629,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. simpl; auto 20. UseHelper. auto.
+  econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto.
 Qed.
 
 Lemma eval_shrluimm:
   forall n,
-  unary_constructor_sound (fun e => shrluimm e n) (fun v => Val.shrlu v (Vint n)).
+  unary_constructor_sound (fun e => shrluimm hf e n) (fun v => Val.shrlu v (Vint n)).
 Proof.
   unfold shrluimm; red; intros. apply eval_shift_imm; intros.
   + (* n = 0 *)
@@ -654,10 +663,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. simpl; auto 20. UseHelper. auto.
+    econstructor; split. eapply eval_helper_2; eauto. EvalOp. DeclHelper. UseHelper. auto.
 Qed.
 
-Theorem eval_shrlu: binary_constructor_sound shrlu Val.shrlu.
+Theorem eval_shrlu: binary_constructor_sound (shrlu hf) Val.shrlu.
 Proof.
   unfold shrlu; red; intros.
   destruct (is_intconst b) as [n|] eqn:IC.
@@ -665,12 +674,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. simpl; auto 20. UseHelper. auto.
+  econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto.
 Qed.
 
 Lemma eval_shrlimm:
   forall n,
-  unary_constructor_sound (fun e => shrlimm e n) (fun v => Val.shrl v (Vint n)).
+  unary_constructor_sound (fun e => shrlimm hf e n) (fun v => Val.shrl v (Vint n)).
 Proof.
   unfold shrlimm; red; intros. apply eval_shift_imm; intros.
   + (* n = 0 *)
@@ -703,10 +712,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. simpl; auto 20. UseHelper. auto.
+    econstructor; split. eapply eval_helper_2; eauto. EvalOp. DeclHelper. UseHelper. auto.
 Qed.
 
-Theorem eval_shrl: binary_constructor_sound shrl Val.shrl.
+Theorem eval_shrl: binary_constructor_sound (shrl hf) Val.shrl.
 Proof.
   unfold shrl; red; intros.
   destruct (is_intconst b) as [n|] eqn:IC.
@@ -714,17 +723,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. simpl; auto 20. UseHelper. auto.
+  econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto.
 Qed.
 
 Theorem eval_addl: binary_constructor_sound addl Val.addl.
 Proof.
   unfold addl; red; intros.
-  set (default := Ebuiltin (EF_builtin i64_add sig_ll_l) (a ::: b ::: Enil)).
+  set (default := Ebuiltin (EF_builtin "__builtin_addl" 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. simpl; auto 20. UseHelper. auto. 
+    econstructor; split. eapply eval_builtin_2; eauto. UseHelper. auto. 
   }
   destruct (is_longconst a) as [p|] eqn:LC1;
   destruct (is_longconst b) as [q|] eqn:LC2.
@@ -743,11 +752,11 @@ Qed.
 Theorem eval_subl: binary_constructor_sound subl Val.subl.
 Proof.
   unfold subl; red; intros.
-  set (default := Ebuiltin (EF_builtin i64_sub sig_ll_l) (a ::: b ::: Enil)).
+  set (default := Ebuiltin (EF_builtin "__builtin_subl" 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. simpl; auto 20. UseHelper. auto. 
+    econstructor; split. eapply eval_builtin_2; eauto. UseHelper. auto. 
   }
   destruct (is_longconst a) as [p|] eqn:LC1;
   destruct (is_longconst b) as [q|] eqn:LC2.
@@ -778,7 +787,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. simpl; auto 20. UseHelper. 
+  EvalOp. eapply eval_builtin_2; eauto. 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 +795,7 @@ Proof.
 Qed.
 
 Lemma eval_mullimm:
-  forall n, unary_constructor_sound (fun a => mullimm a n) (fun v => Val.mull v (Vlong n)).
+  forall n, unary_constructor_sound (fun a => mullimm hf 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 +825,7 @@ Proof.
   apply eval_mull_base; auto. apply eval_longconst. 
 Qed.
 
-Theorem eval_mull: binary_constructor_sound mull Val.mull.
+Theorem eval_mull: binary_constructor_sound (mull hf) Val.mull.
 Proof.
   unfold mull; red; intros.
   destruct (is_longconst a) as [p|] eqn:LC1;
@@ -834,10 +843,10 @@ Proof.
 Qed.
 
 Lemma eval_binop_long:
-  forall id sem le a b x y z,
+  forall id name sem le a b x y z,
   (forall p q, x = Vlong p -> y = Vlong q -> z = Vlong (sem p q)) ->
-  external_implements id sig_ll_l (x::y::nil) z ->
-  In (id, sig_ll_l) i64_helpers ->
+  helper_declared ge id name sig_ll_l ->
+  external_implements name sig_ll_l (x::y::nil) z ->
   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.
@@ -857,15 +866,14 @@ 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 a b) v /\ Val.lessdef z v.
+  exists v, eval_expr ge sp e m le (divl hf a b) v /\ Val.lessdef z v.
 Proof.
   intros. eapply eval_binop_long; eauto. 
   intros; subst; simpl in H1.
   destruct (Int64.eq q Int64.zero
          || Int64.eq p (Int64.repr Int64.min_signed) && Int64.eq q Int64.mone); inv H1. 
   auto.
-  UseHelper. 
-  simpl; auto 20.
+  DeclHelper. UseHelper. 
 Qed.
 
 Theorem eval_modl:
@@ -873,15 +881,14 @@ 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 a b) v /\ Val.lessdef z v.
+  exists v, eval_expr ge sp e m le (modl hf a b) v /\ Val.lessdef z v.
 Proof.
   intros. eapply eval_binop_long; eauto. 
   intros; subst; simpl in H1.
   destruct (Int64.eq q Int64.zero
          || Int64.eq p (Int64.repr Int64.min_signed) && Int64.eq q Int64.mone); inv H1. 
   auto.
-  UseHelper. 
-  simpl; auto 20.
+  DeclHelper. UseHelper.
 Qed.
 
 Theorem eval_divlu:
@@ -889,14 +896,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 a b) v /\ Val.lessdef z v.
+  exists v, eval_expr ge sp e m le (divlu hf a b) v /\ Val.lessdef z v.
 Proof.
   intros. unfold divlu. 
-  set (default := Eexternal i64_udiv sig_ll_l (a ::: b ::: Enil)).
+  set (default := Eexternal hf.(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. simpl; auto 20. UseHelper. auto. 
+    econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto. 
   }
   destruct (is_longconst a) as [p|] eqn:LC1;
   destruct (is_longconst b) as [q|] eqn:LC2.
@@ -932,14 +939,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 a b) v /\ Val.lessdef z v.
+  exists v, eval_expr ge sp e m le (modlu hf a b) v /\ Val.lessdef z v.
 Proof.
   intros. unfold modlu. 
-  set (default := Eexternal i64_umod sig_ll_l (a ::: b ::: Enil)).
+  set (default := Eexternal hf.(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. simpl; auto 20. UseHelper. auto. 
+    econstructor; split. eapply eval_helper_2; eauto. DeclHelper. 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 2e631ad2..dea8a008 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -22,7 +22,9 @@
   Instruction selection proceeds by bottom-up rewriting over expressions.
   The source language is Cminor and the target language is CminorSel. *)
 
+Require String.
 Require Import Coqlib.
+Require Import Maps.
 Require Import AST.
 Require Import Errors.
 Require Import Integers.
@@ -67,6 +69,8 @@ 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
@@ -104,14 +108,14 @@ Definition sel_unop (op: Cminor.unary_operation) (arg: expr) : expr :=
   | Cminor.Ointoflong => intoflong arg
   | Cminor.Olongofint => longofint arg
   | Cminor.Olongofintu => longofintu 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
+  | 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
   end.
 
 Definition sel_binop (op: Cminor.binary_operation) (arg1 arg2: expr) : expr :=
@@ -139,17 +143,17 @@ Definition sel_binop (op: Cminor.binary_operation) (arg1 arg2: expr) : expr :=
   | Cminor.Odivfs => divfs 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.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.Oandl => andl arg1 arg2
   | Cminor.Oorl => orl arg1 arg2
   | Cminor.Oxorl => xorl arg1 arg2
-  | Cminor.Oshll => shll arg1 arg2
-  | Cminor.Oshrl => shrl arg1 arg2
-  | Cminor.Oshrlu => shrlu arg1 arg2
+  | Cminor.Oshll => shll hf arg1 arg2
+  | Cminor.Oshrl => shrl hf arg1 arg2
+  | Cminor.Oshrlu => shrlu hf arg1 arg2
   | Cminor.Ocmp c => comp c arg1 arg2
   | Cminor.Ocmpu c => compu c arg1 arg2
   | Cminor.Ocmpf c => compf c arg1 arg2
@@ -324,8 +328,6 @@ Fixpoint sel_stmt (ge: Cminor.genv) (s: Cminor.stmt) : res stmt :=
   | Cminor.Sgoto lbl => OK (Sgoto lbl)
   end.
 
-End SELECTION.
-
 (** Conversion of functions. *)
 
 Definition sel_function (ge: Cminor.genv) (f: Cminor.function) : res function :=
@@ -340,10 +342,76 @@ Definition sel_function (ge: Cminor.genv) (f: Cminor.function) : res function :=
 Definition sel_fundef (ge: Cminor.genv) (f: Cminor.fundef) : res fundef :=
   transf_partial_fundef (sel_function ge) f.
 
+End SELECTION.
+
+(** Setting up the helper functions. *)
+
+Definition globdef := AST.globdef Cminor.fundef unit.
+
+(** We build a partial mapping from global identifiers to their definitions,
+  restricting ourselves to the globals we are interested in, namely
+  the external function declarations whose name starts with "__i64_".
+  This ensures that the mapping remains small and that [lookup_helper]
+  below is efficient. *)
+
+Definition globdef_of_interest (gd: globdef) : bool :=
+  match gd with
+  | Gfun (External (EF_external name sg)) => String.prefix "__i64_" name
+  | _ => false
+  end.
+
+Definition record_globdef (globs: PTree.t globdef) (id_gd: ident * globdef) :=
+  let (id, gd) := id_gd in
+  if globdef_of_interest gd 
+  then PTree.set id gd globs
+  else PTree.remove id globs.
+
+Definition record_globdefs (p: Cminor.program) : PTree.t globdef :=
+  List.fold_left record_globdef p.(prog_defs) (PTree.empty _).
+
+Definition lookup_helper_aux
+     (name: String.string) (sg: signature) (res: option ident)
+     (id: ident) (gd: globdef) :=
+  match gd with
+  | Gfun (External (EF_external name' sg')) =>
+      if String.string_dec name name' && signature_eq sg sg'
+      then Some id
+      else res
+  | _ => res
+  end.
+
+Definition lookup_helper (globs: PTree.t globdef)
+                         (name: String.string) (sg: signature) : res ident :=
+  match PTree.fold (lookup_helper_aux name sg) globs None with
+  | Some id => OK id
+  | None    => Error (MSG name :: MSG ": missing or incorrect declaration" :: nil)
+  end.
+
+Local Open Scope string_scope.
+
+Definition get_helpers (p: Cminor.program) : res helper_functions :=
+  let globs := record_globdefs p in
+  do i64_dtos <- lookup_helper globs "__i64_dtos" sig_f_l ;
+  do i64_dtou <- lookup_helper globs "__i64_dtou" sig_f_l ;
+  do i64_stod <- lookup_helper globs "__i64_stod" sig_l_f ;
+  do i64_utod <- lookup_helper globs "__i64_utod" sig_l_f ;
+  do i64_stof <- lookup_helper globs "__i64_stof" sig_l_s ;
+  do i64_utof <- lookup_helper globs "__i64_utof" sig_l_s ;
+  do i64_sdiv <- lookup_helper globs "__i64_sdiv" sig_ll_l ;
+  do i64_udiv <- lookup_helper globs "__i64_udiv" sig_ll_l ;
+  do i64_smod <- lookup_helper globs "__i64_smod" sig_ll_l ;
+  do i64_umod <- lookup_helper globs "__i64_umod" sig_ll_l ;
+  do i64_shl <- lookup_helper globs "__i64_shl" sig_li_l ;
+  do i64_shr <- lookup_helper globs "__i64_shr" sig_li_l ;
+  do i64_sar <- lookup_helper globs "__i64_sar" sig_li_l ;
+  OK (mk_helper_functions
+     i64_dtos i64_dtou i64_stod i64_utod i64_stof i64_utof
+     i64_sdiv i64_udiv i64_smod i64_umod
+     i64_shl i64_shr i64_sar).
+
 (** Conversion of programs. *)
 
 Definition sel_program (p: Cminor.program) : res program :=
-  let ge := Genv.globalenv p in
-  do x <- check_helpers ge;
-  transform_partial_program (sel_fundef ge) p.
+  do hf <- get_helpers p;
+  transform_partial_program (sel_fundef hf (Genv.globalenv p)) p.
 
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index 1d2f2b3a..8ea4c56e 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.
-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.
+Variable hf: helper_functions.
+Hypothesis HELPERS: helper_functions_declared ge hf.
+Hypothesis TRANSFPROG: transform_partial_program (sel_fundef hf 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 ge f = OK tf.
+  exists tf, Genv.find_funct_ptr tge b = Some tf /\ sel_fundef hf 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 ge f = OK tf.
+  exists tf, Genv.find_funct tge v' = Some tf /\ sel_fundef hf 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 ge f = OK tf -> funsig tf = Cminor.funsig f.
+  forall f tf, sel_fundef hf 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 ge f = OK tf -> fn_stackspace tf = Cminor.fn_stackspace f.
+  forall f tf, sel_function hf ge f = OK tf -> fn_stackspace tf = Cminor.fn_stackspace f.
 Proof.
   intros. monadInv H. auto. 
 Qed.
@@ -100,17 +100,17 @@ Proof.
 Qed.
 
 Lemma helper_declared_preserved:
-  forall id sg, helper_declared ge id sg -> helper_declared tge id sg.
+  forall id name sg, helper_declared ge id name sg -> helper_declared tge id name sg.
 Proof.
-  intros id sg (b & A & B).
+  intros id name sg (b & A & B).
   exploit function_ptr_translated; eauto. simpl. intros (tf & P & Q). inv Q. 
   exists b; split; auto. rewrite symbols_preserved. auto.
 Qed.
 
-Let HELPERS':
-  forall name sg, In (name, sg) i64_helpers -> helper_declared tge name sg.
+Let HELPERS': helper_functions_declared tge hf.
 Proof.
-  intros. apply helper_declared_preserved. auto.
+  red in HELPERS; decompose [Logic.and] HELPERS.
+  red. auto 20 using helper_declared_preserved. 
 Qed.
 
 Section CMCONSTR.
@@ -172,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 op a1) v' /\ Val.lessdef v v'.
+  exists v', eval_expr tge sp e m le (sel_unop hf op a1) v' /\ Val.lessdef v v'.
 Proof.
   destruct op; simpl; intros; FuncInv; try subst v.
   apply eval_cast8unsigned; auto.
@@ -215,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 op a1 a2) v' /\ Val.lessdef v v'.
+  exists v', eval_expr tge sp e m le (sel_binop hf op a1 a2) v' /\ Val.lessdef v v'.
 Proof.
   destruct op; simpl; intros; FuncInv; try subst v.
   apply eval_add; auto.
@@ -552,7 +552,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 a) v' /\ Val.lessdef v v'.
+  exists v', eval_expr tge sp e' m' le (sel_expr hf a) v' /\ Val.lessdef v v'.
 Proof.
   induction 1; intros; simpl.
   (* Evar *)
@@ -589,7 +589,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 a) v' /\ Val.lessdef_list v v'.
+  exists v', eval_exprlist tge sp e' m' le (sel_exprlist hf a) v' /\ Val.lessdef_list v v'.
 Proof.
   induction 1; intros; simpl. 
   exists (@nil val); split; auto. constructor.
@@ -603,13 +603,13 @@ Lemma sel_builtin_arg_correct:
   env_lessdef e e' -> Mem.extends m m' ->
   Cminor.eval_expr ge sp e m a v ->
   exists v',
-     CminorSel.eval_builtin_arg tge sp e' m' (sel_builtin_arg a c) v'
+     CminorSel.eval_builtin_arg tge sp e' m' (sel_builtin_arg hf a c) v'
   /\ Val.lessdef v v'.
 Proof.
   intros. unfold sel_builtin_arg. 
   exploit sel_expr_correct; eauto. intros (v1 & A & B).
   exists v1; split; auto.
-  destruct (builtin_arg_ok (builtin_arg (sel_expr a)) c).
+  destruct (builtin_arg_ok (builtin_arg (sel_expr hf a)) c).
   apply eval_builtin_arg; eauto.
   constructor; auto.
 Qed.
@@ -622,7 +622,7 @@ Lemma sel_builtin_args_correct:
   forall cl,
   exists vl',
      list_forall2 (CminorSel.eval_builtin_arg tge sp e' m')
-                  (sel_builtin_args al cl)
+                  (sel_builtin_args hf al cl)
                   vl'
   /\ Val.lessdef_list vl vl'.
 Proof.
@@ -647,21 +647,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 ge s = OK s' ->
+      sel_stmt hf 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 ge f = OK f' ->
+      sel_function hf 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 ge f = OK f')
-        (TS: sel_stmt ge s = OK s')
+        (TF: sel_function hf ge f = OK f')
+        (TS: sel_stmt hf ge s = OK s')
         (MC: match_cont k k')
         (LD: env_lessdef e e')
         (ME: Mem.extends m m'),
@@ -669,7 +669,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 ge f = OK f')
+        (TF: sel_fundef hf ge f = OK f')
         (MC: match_cont k k')
         (LD: Val.lessdef_list args args')
         (ME: Mem.extends m m'),
@@ -684,7 +684,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 ge f = OK f')
+        (TF: sel_function hf ge f = OK f')
         (MC: match_cont k k')
         (LDA: Val.lessdef_list args args')
         (LDE: env_lessdef e e')
@@ -694,7 +694,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 (sel_builtin_res 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 ge f = OK f')
+        (TF: sel_function hf ge f = OK f')
         (MC: match_cont k k')
         (LDV: Val.lessdef v v')
         (LDE: env_lessdef e e')
@@ -712,16 +712,16 @@ Qed.
 Remark find_label_commut:
   forall lbl s k s' k',
   match_cont k k' ->
-  sel_stmt ge s = OK s' ->
+  sel_stmt hf 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 ge s1 = OK s1' /\ match_cont k1 k1'
+  | Some(s1, k1), Some(s1', k1') => sel_stmt hf 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 e)); simpl; auto.
+  unfold store. destruct (addressing m (sel_expr hf e)); simpl; auto.
 (* call *)
   destruct (classify_call ge e); simpl; auto.
 (* tailcall *)
@@ -886,7 +886,7 @@ Proof.
 - (* Slabel *)
   left; econstructor; split. constructor. constructor; auto.
 - (* Sgoto *)
-  assert (sel_stmt ge (Cminor.fn_body f) = OK (fn_body f')).
+  assert (sel_stmt hf 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.
@@ -954,39 +954,97 @@ Qed.
 
 End PRESERVATION.
 
-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.
+(** Processing of helper functions *)
+
+Lemma record_globdefs_sound:
+  forall p id fd,
+  (record_globdefs p)!id = Some (Gfun fd) ->
+  exists b, Genv.find_symbol (Genv.globalenv p) id = Some b
+         /\ Genv.find_funct_ptr (Genv.globalenv p) b = Some fd.
+Proof.
+  intros until fd.
+  set (P := fun (m: PTree.t globdef) (ge: Genv.t Cminor.fundef unit) =>
+               m!id = Some (Gfun fd) ->
+               exists b, Genv.find_symbol ge id = Some b
+                      /\ Genv.find_funct_ptr ge b = Some fd).
+  assert (REC: forall gl m ge,
+             P m ge ->
+             P (fold_left record_globdef gl m) (Genv.add_globals ge gl)).
+  {
+    induction gl; simpl; intros.
+  - auto.
+  - apply IHgl. red. destruct a as [id1 gd1]; simpl; intros.
+    unfold Genv.find_symbol; simpl. rewrite PTree.gsspec. destruct (peq id id1).
+    + subst id1. exists (Genv.genv_next ge); split; auto. 
+      replace gd1 with (@Gfun Cminor.fundef unit fd).
+      unfold Genv.find_funct_ptr; simpl. apply PTree.gss. 
+      destruct (globdef_of_interest gd1).
+      rewrite PTree.gss in H0; congruence.
+      rewrite PTree.grs in H0; congruence.
+    + assert (m!id = Some (Gfun fd)).
+      { destruct (globdef_of_interest gd1). 
+        rewrite PTree.gso in H0; auto.
+        rewrite PTree.gro in H0; auto. }
+      exploit H; eauto. intros (b & A & B).
+      exists b; split; auto. unfold Genv.find_funct_ptr; simpl.
+      destruct gd1; auto. rewrite PTree.gso; auto. 
+      apply Plt_ne. eapply Genv.genv_symb_range; eauto. 
+  }
+  eapply REC. red; intros. rewrite PTree.gempty in H; discriminate.
+Qed.
+
+Lemma lookup_helper_correct_1:
+  forall globs name sg id,
+  lookup_helper globs name sg = OK id ->
+  globs!id = Some (Gfun (External (EF_external name sg))).
+Proof.
+  intros.
+  set (P := fun (m: PTree.t globdef) res => res = Some id -> m!id = Some(Gfun(External (EF_external name sg)))).
+  assert (P globs (PTree.fold (lookup_helper_aux name sg) globs None)).
+  { apply PTree_Properties.fold_rec; red; intros.
+  - rewrite <- H0. apply H1; auto. 
+  - discriminate.
+  - assert (EITHER: k = id /\ v = Gfun (External (EF_external name sg))
+                \/  a = Some id).
+    { unfold lookup_helper_aux in H3. destruct v; auto. destruct f; auto. destruct e; auto. 
+      destruct (String.string_dec name name0); auto.
+      destruct (signature_eq sg sg0); auto.
+      inversion H3. left; split; auto. repeat f_equal; auto. }
+    destruct EITHER as [[X Y] | X].
+    subst k v. apply PTree.gss. 
+    apply H2 in X. rewrite PTree.gso by congruence. auto.
+  }
+  red in H0. unfold lookup_helper in H. 
+  destruct (PTree.fold (lookup_helper_aux name sg) globs None); inv H. 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.
+Lemma lookup_helper_correct:
+  forall p name sg id,
+  lookup_helper (record_globdefs p) name sg = OK id ->
+  helper_declared (Genv.globalenv p) id 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. 
+  intros. apply lookup_helper_correct_1 in H. apply record_globdefs_sound in H. auto.
 Qed.
 
+Theorem get_helpers_correct:
+  forall p hf,
+  get_helpers p = OK hf -> helper_functions_declared (Genv.globalenv p) hf.
+Proof.
+  intros. monadInv H. red; simpl. auto 20 using lookup_helper_correct.
+Qed.
+
+(** All together *)
+
 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. 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). 
+  intros. unfold sel_program in H. 
+  destruct (get_helpers prog) as [hf|] eqn:G; simpl in H; try discriminate.
+  apply forward_simulation_opt with (match_states := match_states prog tprog hf) (measure := measure). 
   eapply public_preserved; eauto.
   apply sel_initial_states; auto.
   apply sel_final_states; auto.
-  apply sel_step_correct; auto. eapply check_helpers_correct; eauto.
+  apply sel_step_correct; auto. eapply get_helpers_correct; eauto. 
 Qed.