From 202bc495442a1a8fa184b73ac0063bdbbbcdf846 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 24 Feb 2013 09:01:28 +0000 Subject: Constant propagation within __builtin_annot. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2126 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/AST.v | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) (limited to 'common/AST.v') diff --git a/common/AST.v b/common/AST.v index d2065d6..44811b2 100644 --- a/common/AST.v +++ b/common/AST.v @@ -443,7 +443,7 @@ 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: ident) (targs: list annot_arg) (** 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. *) @@ -451,15 +451,27 @@ Inductive external_function : Type := (** 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). + | EF_inline_asm (text: ident) (** 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 preservation theorem. Generated only if [-finline-asm] is given. *) +with annot_arg : Type := + | AA_arg (ty: typ) + | AA_int (n: int) + | AA_float (n: float). + (** The type signature of an external function. *) +Fixpoint annot_args_typ (targs: list annot_arg) : list typ := + match targs with + | nil => nil + | AA_arg ty :: targs' => ty :: annot_args_typ targs' + | _ :: targs' => annot_args_typ targs' + end. + Definition ef_sig (ef: external_function): signature := match ef with | EF_external name sg => sg @@ -471,7 +483,7 @@ Definition ef_sig (ef: external_function): signature := | EF_malloc => mksignature (Tint :: nil) (Some Tint) | EF_free => mksignature (Tint :: nil) None | EF_memcpy sz al => mksignature (Tint :: Tint :: nil) None - | EF_annot text targs => mksignature targs None + | EF_annot text targs => mksignature (annot_args_typ targs) None | EF_annot_val text targ => mksignature (targ :: nil) (Some targ) | EF_inline_asm text => mksignature nil None end. -- cgit v1.2.3