From f0a5038b4e4220300637d3e9e918d9ec31623108 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 8 Oct 2015 15:33:47 +0200 Subject: Added versions of the tranform_* functions in AST to work with functions taking the ident as argument. This functions are currently not used inside the proven part but it is nice to have them already there, when they are used by some future pass. They also come equiped with the corresponding proofs. --- extraction/extraction.v | 1 + 1 file changed, 1 insertion(+) (limited to 'extraction/extraction.v') diff --git a/extraction/extraction.v b/extraction/extraction.v index 6327f871..dc7522b8 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -168,4 +168,5 @@ Separate Extraction Machregs.mregs_for_operation Machregs.mregs_for_builtin Machregs.two_address_op Machregs.is_stack_reg AST.signature_main + AST.transform_partial_ident_program Parser.translation_unit_file. -- cgit 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. --- extraction/extraction.v | 4 ---- 1 file changed, 4 deletions(-) (limited to 'extraction/extraction.v') diff --git a/extraction/extraction.v b/extraction/extraction.v index dc7522b8..aca7102d 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -42,10 +42,6 @@ Extract Inlined Constant Coqlib.proj_sumbool => "(fun x -> x)". (* Wfsimpl *) Extraction Inline Wfsimpl.Fix Wfsimpl.Fixm. -(* AST *) -Extract Constant AST.ident_of_string => - "fun s -> Camlcoq.intern_string (Camlcoq.camlstring_of_coqstring s)". - (* Memory - work around an extraction bug. *) Extraction NoInline Memory.Mem.valid_pointer. -- 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. --- extraction/extraction.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'extraction/extraction.v') diff --git a/extraction/extraction.v b/extraction/extraction.v index aca7102d..0f0a8637 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -111,7 +111,7 @@ Extract Constant Compiler.time => "Timing.time_coq". (*Extraction Inline Compiler.apply_total Compiler.apply_partial.*) (* Cabs *) -Extract Constant Cabs.cabsloc => +Extract Constant Cabs.cabsloc => "{ lineno : int; filename: string; byteno: int; -- cgit