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.

4 files changed, 23 insertions, 25 deletions

diff --git a/common/AST.v b/common/AST.v
index 4e02b3d4..c62b0091 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -16,8 +16,8 @@
 (** This file defines a number of data types and operations used in
   the abstract syntax trees of many of the intermediate languages. *)
 
+Require Import String.
 Require Import Coqlib.
-Require String.
 Require Import Errors.
 Require Import Integers.
 Require Import Floats.
@@ -33,8 +33,6 @@ Definition ident := positive.
 
 Definition ident_eq := peq.
 
-Parameter ident_of_string : String.string -> ident.
-
 (** The intermediate languages are weakly typed, using the following types: *)
 
 Inductive typ : Type :=
@@ -305,8 +303,7 @@ End TRANSF_PROGRAM_IDENT.
   for the case the identifier of the function is passed as additional 
   argument *)
 
-Open Local Scope error_monad_scope.
-Open Local Scope string_scope.
+Local Open Scope error_monad_scope.
 
 Section TRANSF_PROGRAM_GEN.
 
@@ -760,10 +757,10 @@ Qed.
   and associated operations. *)
 
 Inductive external_function : Type :=
-  | EF_external (name: ident) (sg: signature)
+  | EF_external (name: string) (sg: signature)
      (** A system call or library function.  Produces an event
          in the trace. *)
-  | EF_builtin (name: ident) (sg: signature)
+  | EF_builtin (name: string) (sg: signature)
      (** A compiler built-in function.  Behaves like an external, but
          can be inlined by the compiler. *)
   | EF_vload (chunk: memory_chunk)
@@ -786,15 +783,15 @@ Inductive external_function : Type :=
          Produces no observable event. *)
   | EF_memcpy (sz: Z) (al: Z)
      (** Block copy, of [sz] bytes, between addresses that are [al]-aligned. *)
-  | EF_annot (text: ident) (targs: list typ)
+  | EF_annot (text: string) (targs: list typ)
      (** A programmer-supplied annotation.  Takes zero, one or several arguments,
          produces an event carrying the text and the values of these arguments,
          and returns no value. *)
-  | EF_annot_val (text: ident) (targ: typ)
+  | EF_annot_val (text: string) (targ: typ)
      (** Another form of annotation that takes one argument, produces
          an event carrying the text and the value of this argument,
          and returns the value of the argument. *)
-  | EF_inline_asm (text: ident) (sg: signature) (clobbers: list String.string)
+  | EF_inline_asm (text: string) (sg: signature) (clobbers: list string)
      (** Inline [asm] statements.  Semantically, treated like an
          annotation with no parameters ([EF_annot text nil]).  To be
          used with caution, as it can invalidate the semantic
@@ -852,9 +849,8 @@ Definition ef_reloads (ef: external_function) : bool :=
 
 Definition external_function_eq: forall (ef1 ef2: external_function), {ef1=ef2} + {ef1<>ef2}.
 Proof.
-  generalize ident_eq signature_eq chunk_eq typ_eq list_eq_dec zeq Int.eq_dec; intros.
+  generalize ident_eq string_dec signature_eq chunk_eq typ_eq list_eq_dec zeq Int.eq_dec; intros.
   decide equality.
-  apply list_eq_dec. apply String.string_dec. 
 Defined.
 Global Opaque external_function_eq.
 
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.
 
diff --git a/common/Events.v b/common/Events.v
index 7cd9155e..dc38b344 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -15,6 +15,7 @@
 
 (** Observable events, execution traces, and semantics of external calls. *)
 
+Require Import String.
 Require Import Coqlib.
 Require Intv.
 Require Import AST.
@@ -61,10 +62,10 @@ Inductive eventval: Type :=
   | EVptr_global: ident -> int -> eventval.
 
 Inductive event: Type :=
-  | Event_syscall: ident -> list eventval -> eventval -> event
+  | Event_syscall: string -> list eventval -> eventval -> event
   | Event_vload: memory_chunk -> ident -> int -> eventval -> event
   | Event_vstore: memory_chunk -> ident -> int -> eventval -> event
-  | Event_annot: ident -> list eventval -> event.
+  | Event_annot: string -> list eventval -> event.
 
 (** The dynamic semantics for programs collect traces of events.
   Traces are of two kinds: finite (type [trace]) or infinite (type [traceinf]). *)
@@ -1219,7 +1220,7 @@ Qed.
 
 (** ** Semantics of annotations. *)
 
-Inductive extcall_annot_sem (text: ident) (targs: list typ) (ge: Senv.t):
+Inductive extcall_annot_sem (text: string) (targs: list typ) (ge: Senv.t):
               list val -> mem -> trace -> val -> mem -> Prop :=
   | extcall_annot_sem_intro: forall vargs m args,
       eventval_list_match ge args targs vargs ->
@@ -1264,7 +1265,7 @@ Proof.
   split. constructor. auto.
 Qed.
 
-Inductive extcall_annot_val_sem (text: ident) (targ: typ) (ge: Senv.t):
+Inductive extcall_annot_val_sem (text: string) (targ: typ) (ge: Senv.t):
               list val -> mem -> trace -> val -> mem -> Prop :=
   | extcall_annot_val_sem_intro: forall varg m arg,
       eventval_match ge arg targ varg ->
@@ -1354,14 +1355,14 @@ Qed.
   we do not define their semantics, but only assume that it satisfies
   [extcall_properties]. *)
 
-Parameter external_functions_sem: ident -> signature -> extcall_sem.
+Parameter external_functions_sem: String.string -> signature -> extcall_sem.
 
 Axiom external_functions_properties:
   forall id sg, extcall_properties (external_functions_sem id sg) sg.
 
 (** We treat inline assembly similarly. *)
 
-Parameter inline_assembly_sem: ident -> signature -> extcall_sem.
+Parameter inline_assembly_sem: String.string -> signature -> extcall_sem.
 
 Axiom inline_assembly_properties:
   forall id sg, extcall_properties (inline_assembly_sem id sg) sg.
diff --git a/common/PrintAST.ml b/common/PrintAST.ml
index aea8ff0f..67b5eb9d 100644
--- a/common/PrintAST.ml
+++ b/common/PrintAST.ml
@@ -37,17 +37,17 @@ let name_of_chunk = function
   | Many64 -> "any64"
 
 let name_of_external = function
-  | EF_external(name, sg) -> sprintf "extern %S" (extern_atom name)
-  | EF_builtin(name, sg) -> sprintf "builtin %S" (extern_atom name)
+  | EF_external(name, sg) -> sprintf "extern %S" (camlstring_of_coqstring name)
+  | EF_builtin(name, sg) -> sprintf "builtin %S" (camlstring_of_coqstring name)
   | EF_vload chunk -> sprintf "volatile load %s" (name_of_chunk chunk)
   | EF_vstore chunk -> sprintf "volatile store %s" (name_of_chunk chunk)
   | EF_malloc -> "malloc"
   | EF_free -> "free"
   | EF_memcpy(sz, al) ->
       sprintf "memcpy size %s align %s " (Z.to_string sz) (Z.to_string al)
-  | EF_annot(text, targs) -> sprintf "annot %S" (extern_atom text)
-  | EF_annot_val(text, targ) ->  sprintf "annot_val %S" (extern_atom text)
-  | EF_inline_asm(text, sg, clob) -> sprintf "inline_asm %S" (extern_atom text)
+  | EF_annot(text, targs) -> sprintf "annot %S" (camlstring_of_coqstring text)
+  | EF_annot_val(text, targ) ->  sprintf "annot_val %S" (camlstring_of_coqstring text)
+  | EF_inline_asm(text, sg, clob) -> sprintf "inline_asm %S" (camlstring_of_coqstring text)
   | EF_debug(kind, text, targs) ->
       sprintf "debug%d %S" (P.to_int kind) (extern_atom text)