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, 11 insertions, 18 deletions

diff --git a/ia32/Asmexpand.ml b/ia32/Asmexpand.ml
index 4f02e633..99babeb4 100644
--- a/ia32/Asmexpand.ml
+++ b/ia32/Asmexpand.ml
@@ -368,7 +368,7 @@ let expand_instruction instr =
      begin
        match ef with
        | EF_builtin(name, sg) ->
-	  expand_builtin_inline (extern_atom name) args res
+	  expand_builtin_inline (camlstring_of_coqstring name) args res
        | EF_vload chunk ->
           expand_builtin_vload chunk args res
        | EF_vstore chunk ->
diff --git a/ia32/Machregs.v b/ia32/Machregs.v
index ace193b7..f3801900 100644
--- a/ia32/Machregs.v
+++ b/ia32/Machregs.v
@@ -129,17 +129,14 @@ Fixpoint destroyed_by_clobber (cl: list string): list mreg :=
       end
   end.
 
-Definition builtin_write16_reversed := ident_of_string "__builtin_write16_reversed".
-Definition builtin_write32_reversed := ident_of_string "__builtin_write32_reversed".
-
 Definition destroyed_by_builtin (ef: external_function): list mreg :=
   match ef with
   | EF_memcpy sz al =>
       if zle sz 32 then CX :: X7 :: nil else CX :: SI :: DI :: nil
   | EF_vstore (Mint8unsigned|Mint8signed) => AX :: CX :: nil
-  | EF_builtin id sg =>
-      if ident_eq id builtin_write16_reversed
-      || ident_eq id builtin_write32_reversed
+  | EF_builtin name sg =>
+      if string_dec name "__builtin_write16_reversed"
+      || string_dec name "__builtin_write32_reversed"
       then CX :: DX :: nil else nil
   | EF_inline_asm txt sg clob => destroyed_by_clobber clob
   | _ => nil
@@ -173,21 +170,17 @@ Definition mregs_for_operation (op: operation): list (option mreg) * option mreg
   | _ => (nil, None)
   end.
 
-Definition builtin_negl := ident_of_string "__builtin_negl".
-Definition builtin_addl := ident_of_string "__builtin_addl".
-Definition builtin_subl := ident_of_string "__builtin_subl".
-Definition builtin_mull := ident_of_string "__builtin_mull".
-
 Definition mregs_for_builtin (ef: external_function): list (option mreg) * list (option mreg) :=
   match ef with
   | EF_memcpy sz al =>
      if zle sz 32 then (Some AX :: Some DX :: nil, nil) else (Some DI :: Some SI :: nil, nil)
-  | EF_builtin id sg =>
-     if ident_eq id builtin_negl then
+  | EF_builtin name sg =>
+     if string_dec name "__builtin_negl" then
        (Some DX :: Some AX :: nil, Some DX :: Some AX :: nil)
-     else if ident_eq id builtin_addl || ident_eq id builtin_subl then
+     else if string_dec name "__builtin_addl"
+          || string_dec name "__builtin_subl" then
        (Some DX :: Some AX :: Some CX :: Some BX :: nil, Some DX :: Some AX :: nil)
-     else if ident_eq id builtin_mull then
+     else if string_dec name "__builtin_mull" then
        (Some AX :: Some DX :: nil, Some DX :: Some AX :: nil)
      else
        (nil, nil)
diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml
index 95de40ca..3f5e6cfe 100644
--- a/ia32/TargetPrinter.ml
+++ b/ia32/TargetPrinter.ml
@@ -656,13 +656,13 @@ module Target(System: SYSTEM):TARGET =
           begin match ef with
           | EF_annot(txt, targs) ->
               fprintf oc "%s annotation: " comment;
-              print_annot_text preg "%esp" oc (extern_atom txt) args
+              print_annot_text preg "%esp" oc (camlstring_of_coqstring txt) args
           | EF_debug(kind, txt, targs) ->
               print_debug_info comment print_file_line preg "%esp" oc
                                (P.to_int kind) (extern_atom txt) args
           | EF_inline_asm(txt, sg, clob) ->
               fprintf oc "%s begin inline assembly\n\t" comment;
-              print_inline_asm preg oc (extern_atom txt) sg args res;
+              print_inline_asm preg oc (camlstring_of_coqstring txt) sg args res;
               fprintf oc "%s end inline assembly\n" comment
           | _ ->
               assert false