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. --- exportclight/Clightdefs.v | 1 + exportclight/Clightgen.ml | 2 +- exportclight/ExportClight.ml | 26 +++++++++++++------------- 3 files changed, 15 insertions(+), 14 deletions(-) (limited to 'exportclight') diff --git a/exportclight/Clightdefs.v b/exportclight/Clightdefs.v index a75c95a5..fda5bb55 100644 --- a/exportclight/Clightdefs.v +++ b/exportclight/Clightdefs.v @@ -15,6 +15,7 @@ (** All imports and definitions used by .v Clight files generated by clightgen *) +Require Export String. Require Export List. Require Export ZArith. Require Export Integers. diff --git a/exportclight/Clightgen.ml b/exportclight/Clightgen.ml index a1dba2d9..c1009b4f 100644 --- a/exportclight/Clightgen.ml +++ b/exportclight/Clightgen.ml @@ -112,7 +112,7 @@ let parse_c_file sourcename ifile = in (* Parsing and production of a simplified C AST *) let ast = - match fst (Parse.preprocessed_file simplifs sourcename ifile) with + match Parse.preprocessed_file simplifs sourcename ifile with | None -> exit 2 | Some p -> p in (* Save C AST if requested *) 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 "@[(EF_external %a@ %a)@]" ident name signatur sg + fprintf p "@[(EF_external %a@ %a)@]" coqstring name signatur sg | EF_builtin(name, sg) -> - fprintf p "@[(EF_builtin %a@ %a)@]" ident name signatur sg + fprintf p "@[(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 "@[(EF_inline_asm %ld%%positive@ %a@ %a)@]" - (P.to_int32 text) + fprintf p "@[(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.@ @ " -- cgit