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, 3 insertions, 2 deletions

diff --git a/common/Determinism.v b/common/Determinism.v
index 7ea19663..2445398c 100644
--- a/common/Determinism.v
+++ b/common/Determinism.v
@@ -13,6 +13,7 @@
 (** Characterization and properties of deterministic external worlds
   and deterministic semantics *)
 
+Require Import String.
 Require Import Coqlib.
 Require Import AST.
 Require Import Integers.
@@ -37,11 +38,11 @@ Require Import Behaviors.
   the world to [w]. *)
 
 CoInductive world: Type :=
-  World (io: ident -> list eventval -> option (eventval * world))
+  World (io: string -> list eventval -> option (eventval * world))
         (vload: memory_chunk -> ident -> int -> option (eventval * world))
         (vstore: memory_chunk -> ident -> int -> eventval -> option world).
 
-Definition nextworld_io (w: world) (evname: ident) (evargs: list eventval) :
+Definition nextworld_io (w: world) (evname: string) (evargs: list eventval) :
                      option (eventval * world) :=
   match w with World io vl vs => io evname evargs end.