From 7a6bb90048db7a254e959b1e3c308bac5fe6c418 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 11 Oct 2015 17:43:59 +0200 Subject: 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. --- cfrontend/PrintCsyntax.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'cfrontend/PrintCsyntax.ml') diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index d890c820..ce912a8c 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -258,12 +258,12 @@ let rec expr p (prec, e) = exprlist (true, args) | Ebuiltin(EF_annot(txt, _), _, args, _) -> fprintf p "__builtin_annot@[(%S%a)@]" - (extern_atom txt) exprlist (false, args) + (camlstring_of_coqstring txt) exprlist (false, args) | Ebuiltin(EF_annot_val(txt, _), _, args, _) -> fprintf p "__builtin_annot_val@[(%S%a)@]" - (extern_atom txt) exprlist (false, args) + (camlstring_of_coqstring txt) exprlist (false, args) | Ebuiltin(EF_external(id, sg), _, args, _) -> - fprintf p "%s@[(%a)@]" (extern_atom id) exprlist (true, args) + fprintf p "%s@[(%a)@]" (camlstring_of_coqstring id) exprlist (true, args) | Ebuiltin(EF_inline_asm(txt, sg, clob), _, args, _) -> extended_asm p txt None args clob | Ebuiltin(_, _, args, _) -> @@ -282,7 +282,7 @@ and exprlist p (first, rl) = exprlist p (false, rl) and extended_asm p txt res args clob = - fprintf p "asm volatile (@[%S" (extern_atom txt); + fprintf p "asm volatile (@[%S" (camlstring_of_coqstring txt); fprintf p "@ :"; begin match res with | None -> () -- cgit