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. --- common/PrintAST.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'common/PrintAST.ml') 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) -- cgit From 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 20 Oct 2015 13:32:18 +0200 Subject: Updated PR by removing whitespaces. Bug 17450. --- common/PrintAST.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'common/PrintAST.ml') diff --git a/common/PrintAST.ml b/common/PrintAST.ml index 67b5eb9d..39481bfb 100644 --- a/common/PrintAST.ml +++ b/common/PrintAST.ml @@ -57,17 +57,17 @@ let rec print_builtin_arg px oc = function | BA_long n -> fprintf oc "long %Ld" (camlint64_of_coqint n) | BA_float n -> fprintf oc "float %F" (camlfloat_of_coqfloat n) | BA_single n -> fprintf oc "single %F" (camlfloat_of_coqfloat32 n) - | BA_loadstack(chunk, ofs) -> + | BA_loadstack(chunk, ofs) -> fprintf oc "%s[sp + %ld]" (name_of_chunk chunk) (camlint_of_coqint ofs) | BA_addrstack(ofs) -> fprintf oc "sp + %ld" (camlint_of_coqint ofs) - | BA_loadglobal(chunk, id, ofs) -> + | BA_loadglobal(chunk, id, ofs) -> fprintf oc "%s[&%s + %ld]" (name_of_chunk chunk) (extern_atom id) (camlint_of_coqint ofs) | BA_addrglobal(id, ofs) -> fprintf oc "&%s + %ld" (extern_atom id) (camlint_of_coqint ofs) | BA_splitlong(hi, lo) -> - fprintf oc "splitlong(%a, %a)" + fprintf oc "splitlong(%a, %a)" (print_builtin_arg px) hi (print_builtin_arg px) lo let rec print_builtin_args px oc = function @@ -80,6 +80,6 @@ let rec print_builtin_res px oc = function | BR x -> px oc x | BR_none -> fprintf oc "_" | BR_splitlong(hi, lo) -> - fprintf oc "splitlong(%a, %a)" + fprintf oc "splitlong(%a, %a)" (print_builtin_res px) hi (print_builtin_res px) lo -- cgit