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.

1 files changed, 0 insertions, 4 deletions

diff --git a/extraction/extraction.v b/extraction/extraction.v
index dc7522b8..aca7102d 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -42,10 +42,6 @@ Extract Inlined Constant Coqlib.proj_sumbool => "(fun x -> x)".
 (* Wfsimpl *)
 Extraction Inline Wfsimpl.Fix Wfsimpl.Fixm.
 
-(* AST *)
-Extract Constant AST.ident_of_string =>
-  "fun s -> Camlcoq.intern_string (Camlcoq.camlstring_of_coqstring s)".
-
 (* Memory - work around an extraction bug. *)
 Extraction NoInline Memory.Mem.valid_pointer.