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/AST.v | 20 ++++++++------------ common/Determinism.v | 5 +++-- common/Events.v | 13 +++++++------ common/PrintAST.ml | 10 +++++----- 4 files changed, 23 insertions(+), 25 deletions(-) (limited to 'common') 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. diff --git a/common/Determinism.v b/common/Determinism.v index 7ea19663..2445398c 100644 --- a/common/Determinism.v +++ b/common/Determinism.v @@ -13,6 +13,7 @@ (** Characterization and properties of deterministic external worlds and deterministic semantics *) +Require Import String. Require Import Coqlib. Require Import AST. Require Import Integers. @@ -37,11 +38,11 @@ Require Import Behaviors. the world to [w]. *) CoInductive world: Type := - World (io: ident -> list eventval -> option (eventval * world)) + World (io: string -> list eventval -> option (eventval * world)) (vload: memory_chunk -> ident -> int -> option (eventval * world)) (vstore: memory_chunk -> ident -> int -> eventval -> option world). -Definition nextworld_io (w: world) (evname: ident) (evargs: list eventval) : +Definition nextworld_io (w: world) (evname: string) (evargs: list eventval) : option (eventval * world) := match w with World io vl vs => io evname evargs end. diff --git a/common/Events.v b/common/Events.v index 7cd9155e..dc38b344 100644 --- a/common/Events.v +++ b/common/Events.v @@ -15,6 +15,7 @@ (** Observable events, execution traces, and semantics of external calls. *) +Require Import String. Require Import Coqlib. Require Intv. Require Import AST. @@ -61,10 +62,10 @@ Inductive eventval: Type := | EVptr_global: ident -> int -> eventval. Inductive event: Type := - | Event_syscall: ident -> list eventval -> eventval -> event + | Event_syscall: string -> list eventval -> eventval -> event | Event_vload: memory_chunk -> ident -> int -> eventval -> event | Event_vstore: memory_chunk -> ident -> int -> eventval -> event - | Event_annot: ident -> list eventval -> event. + | Event_annot: string -> list eventval -> event. (** The dynamic semantics for programs collect traces of events. Traces are of two kinds: finite (type [trace]) or infinite (type [traceinf]). *) @@ -1219,7 +1220,7 @@ Qed. (** ** Semantics of annotations. *) -Inductive extcall_annot_sem (text: ident) (targs: list typ) (ge: Senv.t): +Inductive extcall_annot_sem (text: string) (targs: list typ) (ge: Senv.t): list val -> mem -> trace -> val -> mem -> Prop := | extcall_annot_sem_intro: forall vargs m args, eventval_list_match ge args targs vargs -> @@ -1264,7 +1265,7 @@ Proof. split. constructor. auto. Qed. -Inductive extcall_annot_val_sem (text: ident) (targ: typ) (ge: Senv.t): +Inductive extcall_annot_val_sem (text: string) (targ: typ) (ge: Senv.t): list val -> mem -> trace -> val -> mem -> Prop := | extcall_annot_val_sem_intro: forall varg m arg, eventval_match ge arg targ varg -> @@ -1354,14 +1355,14 @@ Qed. we do not define their semantics, but only assume that it satisfies [extcall_properties]. *) -Parameter external_functions_sem: ident -> signature -> extcall_sem. +Parameter external_functions_sem: String.string -> signature -> extcall_sem. Axiom external_functions_properties: forall id sg, extcall_properties (external_functions_sem id sg) sg. (** We treat inline assembly similarly. *) -Parameter inline_assembly_sem: ident -> signature -> extcall_sem. +Parameter inline_assembly_sem: String.string -> signature -> extcall_sem. Axiom inline_assembly_properties: forall id sg, extcall_properties (inline_assembly_sem id sg) sg. 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