From 7a6bb90048db7a254e959b1e3c308bac5fe6c418 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
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/AST.v | 20 ++++++++------------
 1 file changed, 8 insertions(+), 12 deletions(-)

(limited to 'common/AST.v')

diff --git a/common/AST.v b/common/AST.v
index 4e02b3d4..c62b0091 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -16,8 +16,8 @@
 (** This file defines a number of data types and operations used in
   the abstract syntax trees of many of the intermediate languages. *)
 
+Require Import String.
 Require Import Coqlib.
-Require String.
 Require Import Errors.
 Require Import Integers.
 Require Import Floats.
@@ -33,8 +33,6 @@ Definition ident := positive.
 
 Definition ident_eq := peq.
 
-Parameter ident_of_string : String.string -> ident.
-
 (** The intermediate languages are weakly typed, using the following types: *)
 
 Inductive typ : Type :=
@@ -305,8 +303,7 @@ End TRANSF_PROGRAM_IDENT.
   for the case the identifier of the function is passed as additional 
   argument *)
 
-Open Local Scope error_monad_scope.
-Open Local Scope string_scope.
+Local Open Scope error_monad_scope.
 
 Section TRANSF_PROGRAM_GEN.
 
@@ -760,10 +757,10 @@ Qed.
   and associated operations. *)
 
 Inductive external_function : Type :=
-  | EF_external (name: ident) (sg: signature)
+  | EF_external (name: string) (sg: signature)
      (** A system call or library function.  Produces an event
          in the trace. *)
-  | EF_builtin (name: ident) (sg: signature)
+  | EF_builtin (name: string) (sg: signature)
      (** A compiler built-in function.  Behaves like an external, but
          can be inlined by the compiler. *)
   | EF_vload (chunk: memory_chunk)
@@ -786,15 +783,15 @@ Inductive external_function : Type :=
          Produces no observable event. *)
   | EF_memcpy (sz: Z) (al: Z)
      (** Block copy, of [sz] bytes, between addresses that are [al]-aligned. *)
-  | EF_annot (text: ident) (targs: list typ)
+  | EF_annot (text: string) (targs: list typ)
      (** A programmer-supplied annotation.  Takes zero, one or several arguments,
          produces an event carrying the text and the values of these arguments,
          and returns no value. *)
-  | EF_annot_val (text: ident) (targ: typ)
+  | EF_annot_val (text: string) (targ: typ)
      (** Another form of annotation that takes one argument, produces
          an event carrying the text and the value of this argument,
          and returns the value of the argument. *)
-  | EF_inline_asm (text: ident) (sg: signature) (clobbers: list String.string)
+  | EF_inline_asm (text: string) (sg: signature) (clobbers: list string)
      (** Inline [asm] statements.  Semantically, treated like an
          annotation with no parameters ([EF_annot text nil]).  To be
          used with caution, as it can invalidate the semantic
@@ -852,9 +849,8 @@ Definition ef_reloads (ef: external_function) : bool :=
 
 Definition external_function_eq: forall (ef1 ef2: external_function), {ef1=ef2} + {ef1<>ef2}.
 Proof.
-  generalize ident_eq signature_eq chunk_eq typ_eq list_eq_dec zeq Int.eq_dec; intros.
+  generalize ident_eq string_dec signature_eq chunk_eq typ_eq list_eq_dec zeq Int.eq_dec; intros.
   decide equality.
-  apply list_eq_dec. apply String.string_dec. 
 Defined.
 Global Opaque external_function_eq.
 
-- 
cgit