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.

3 files changed, 15 insertions, 14 deletions

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index bd281374..9b31dfdb 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -769,7 +769,7 @@ let rec convertExpr env e =
       | {edesc = C.EConst(CStr txt)} :: args1 ->
           let targs1 = convertTypArgs env [] args1 in
           Ebuiltin(
-            EF_annot(intern_string txt, typlist_of_typelist targs1),
+            EF_annot(coqstring_of_camlstring txt, typlist_of_typelist targs1),
             targs1, convertExprList env args1, convertTyp env e.etyp)
       | _ ->
           error "ill-formed __builtin_annot (first argument must be string literal)";
@@ -781,7 +781,7 @@ let rec convertExpr env e =
       | [ {edesc = C.EConst(CStr txt)}; arg ] ->
           let targ = convertTyp env
                          (Cutil.default_argument_conversion env arg.etyp) in
-          Ebuiltin(EF_annot_val(intern_string txt, typ_of_type targ),
+          Ebuiltin(EF_annot_val(coqstring_of_camlstring txt, typ_of_type targ),
                    Tcons(targ, Tnil), convertExprList env [arg], 
                    convertTyp env e.etyp)
       | _ ->
@@ -822,7 +822,7 @@ let rec convertExpr env e =
       let sg =
         signature_of_type targs tres
            {cc_vararg = true; cc_unproto = false; cc_structret = false} in
-      Ebuiltin(EF_external(intern_string "printf", sg), 
+      Ebuiltin(EF_external(coqstring_of_camlstring "printf", sg), 
                targs, convertExprList env args, tres)
  
   | C.ECall(fn, args) ->
@@ -877,7 +877,7 @@ let convertAsm loc env txt outputs inputs clobber =
   let e = 
     let tinputs = convertTypArgs env [] inputs' in
     let toutput = convertTyp env ty_res in
-    Ebuiltin(EF_inline_asm(intern_string txt', 
+    Ebuiltin(EF_inline_asm(coqstring_of_camlstring txt', 
                            signature_of_type tinputs toutput cc_default,
                            clobber'),
              tinputs,
@@ -1085,14 +1085,15 @@ let convertFundecl env (sto, id, ty, optinit) =
     | Tfunction(args, res, cconv) -> (args, res, cconv)
     | _ -> assert false in
   let id' = intern_string id.name in
+  let id'' = coqstring_of_camlstring id.name in
   let sg = signature_of_type args res cconv in
   let ef =
     if id.name = "malloc" then EF_malloc else
     if id.name = "free" then EF_free else
     if Str.string_match re_builtin id.name 0
     && List.mem_assoc id.name builtins.functions
-    then EF_builtin(id', sg)
-    else EF_external(id', sg) in
+    then EF_builtin(id'', sg)
+    else EF_external(id'', sg) in
   (id', Gfun(External(ef, args, res, cconv)))
 
 (** Initializers *)
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index 16d5823b..938454c5 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -391,7 +391,7 @@ Qed.
 (** External calls *)
 
 Variable do_external_function:
-  ident -> signature -> Senv.t -> world -> list val -> mem -> option (world * trace * val * mem).
+  string -> signature -> Senv.t -> world -> list val -> mem -> option (world * trace * val * mem).
 
 Hypothesis do_external_function_sound:
   forall id sg ge vargs m t vres m' w w',
@@ -405,7 +405,7 @@ Hypothesis do_external_function_complete:
   do_external_function id sg ge w vargs m = Some(w', t, vres, m').
 
 Variable do_inline_assembly:
-  ident -> signature -> Senv.t -> world -> list val -> mem -> option (world * trace * val * mem).
+  string -> signature -> Senv.t -> world -> list val -> mem -> option (world * trace * val * mem).
 
 Hypothesis do_inline_assembly_sound:
   forall txt sg ge vargs m t vres m' w w',
@@ -513,12 +513,12 @@ Definition do_ef_memcpy (sz al: Z)
   | _ => None
   end.
 
-Definition do_ef_annot (text: ident) (targs: list typ)
+Definition do_ef_annot (text: string) (targs: list typ)
        (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
   do args <- list_eventval_of_val vargs targs;
   Some(w, Event_annot text args :: E0, Vundef, m).
 
-Definition do_ef_annot_val (text: ident) (targ: typ)
+Definition do_ef_annot_val (text: string) (targ: typ)
        (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
   match vargs with
   | varg :: nil =>
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index d890c820..ce912a8c 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -258,12 +258,12 @@ let rec expr p (prec, e) =
                 exprlist (true, args)
   | Ebuiltin(EF_annot(txt, _), _, args, _) ->
       fprintf p "__builtin_annot@[<hov 1>(%S%a)@]"
-                (extern_atom txt) exprlist (false, args)
+                (camlstring_of_coqstring txt) exprlist (false, args)
   | Ebuiltin(EF_annot_val(txt, _), _, args, _) ->
       fprintf p "__builtin_annot_val@[<hov 1>(%S%a)@]"
-                (extern_atom txt) exprlist (false, args)
+                (camlstring_of_coqstring txt) exprlist (false, args)
   | Ebuiltin(EF_external(id, sg), _, args, _) ->
-      fprintf p "%s@[<hov 1>(%a)@]" (extern_atom id) exprlist (true, args)
+      fprintf p "%s@[<hov 1>(%a)@]" (camlstring_of_coqstring id) exprlist (true, args)
   | Ebuiltin(EF_inline_asm(txt, sg, clob), _, args, _) ->
       extended_asm p txt None args clob
   | Ebuiltin(_, _, args, _) ->
@@ -282,7 +282,7 @@ and exprlist p (first, rl) =
       exprlist p (false, rl)
 
 and extended_asm p txt res args clob =
-  fprintf p "asm volatile (@[<hv 0>%S" (extern_atom txt);
+  fprintf p "asm volatile (@[<hv 0>%S" (camlstring_of_coqstring txt);
   fprintf p "@ :";
   begin match res with
   | None -> ()