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, 13 insertions, 13 deletions

diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml
index 82066cc9..01e9037f 100644
--- a/exportclight/ExportClight.ml
+++ b/exportclight/ExportClight.ml
@@ -239,13 +239,13 @@ let signatur p sg =
      (print_option asttype) sg.sig_res 
      callconv sg.sig_cc
 
-let assertions = ref ([]: (ident * typ list) list)
+let assertions = ref ([]: (string * typ list) list)
 
 let external_function p = function
   | EF_external(name, sg) ->
-      fprintf p "@[<hov 2>(EF_external %a@ %a)@]" ident name signatur sg
+      fprintf p "@[<hov 2>(EF_external %a@ %a)@]" coqstring name signatur sg
   | EF_builtin(name, sg) ->
-      fprintf p "@[<hov 2>(EF_builtin %a@ %a)@]" ident name signatur sg
+      fprintf p "@[<hov 2>(EF_builtin %a@ %a)@]" coqstring name signatur sg
   | EF_vload chunk ->
       fprintf p "(EF_vload %s)" (name_of_chunk chunk)
   | EF_vstore chunk ->
@@ -255,16 +255,16 @@ let external_function p = function
   | EF_memcpy(sz, al) ->
       fprintf p "(EF_memcpy %ld %ld)" (Z.to_int32 sz) (Z.to_int32 al)
   | EF_annot(text, targs) -> 
-      assertions := (text, targs) :: !assertions;
-      fprintf p "(EF_annot %ld%%positive %a)" (P.to_int32 text) (print_list asttype) targs
+      assertions := (camlstring_of_coqstring text, targs) :: !assertions;
+      fprintf p "(EF_annot %a %a)" coqstring text (print_list asttype) targs
   | EF_annot_val(text, targ) ->
-      assertions := (text, [targ]) :: !assertions;
-      fprintf p "(EF_annot_val %ld%%positive %a)" (P.to_int32 text) asttype targ
+      assertions := (camlstring_of_coqstring text, [targ]) :: !assertions;
+      fprintf p "(EF_annot_val %a %a)" coqstring text asttype targ
   | EF_debug(kind, text, targs) -> 
       fprintf p "(EF_debug %ld%%positive %ld%%positive %a)" (P.to_int32 kind) (P.to_int32 text) (print_list asttype) targs
   | EF_inline_asm(text, sg, clob) ->
-      fprintf p "@[<hov 2>(EF_inline_asm %ld%%positive@ %a@ %a)@]"
-              (P.to_int32 text)
+      fprintf p "@[<hov 2>(EF_inline_asm %a@ %a@ %a)@]"
+              coqstring text
               signatur sg
               (print_list coqstring) clob
 
@@ -451,14 +451,14 @@ let print_assertion p (txt, targs) =
        | Str.Text s -> Text s
        | Str.Delim "%%" -> Text "%"
        | Str.Delim s -> Param(int_of_string(String.sub s 1 (String.length s - 1))))
-      (Str.full_split re_annot_param (extern_atom txt)) in
+      (Str.full_split re_annot_param txt) in
   let max_param = ref 0 in
   List.iter
     (function
      | Text _ -> ()
      | Param n -> max_param := max n !max_param)
     frags;
-  fprintf p "  | %ld%%positive, " (P.to_int32 txt);
+  fprintf p "  | \"%s\"%%string, " txt;
   list_iteri
     (fun i targ -> fprintf p "_x%d :: " (i + 1))
     targs;
@@ -473,8 +473,8 @@ let print_assertion p (txt, targs) =
 
 let print_assertions p =
   if !assertions <> [] then begin
-    fprintf p "Definition assertions (id: ident) args : Prop :=@ ";
-    fprintf p "  match id, args with@ ";
+    fprintf p "Definition assertions (txt: string) args : Prop :=@ ";
+    fprintf p "  match txt, args with@ ";
     List.iter (print_assertion p) !assertions;
     fprintf p "  | _, _ => False@ ";
     fprintf p "  end.@ @ "