From 4622f49fd089ae47d0c853343cb0a05f986c962a Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 27 Mar 2015 08:55:05 +0100 Subject: Extend annotations so that they can keep track of global variables and local variables whose address is taken. - CminorSel, RTL: add "annot" instructions. - CminorSel to Asm: use type "annot_arg" for arguments of "annot" instructions. - AST, Events: simplify EF_annot because constants are now part of the arguments. Implementation is not complete yet. --- common/AST.v | 73 +++++++++++++++++++++++++++++++++++++++++++++++------------- 1 file changed, 57 insertions(+), 16 deletions(-) (limited to 'common/AST.v') diff --git a/common/AST.v b/common/AST.v index 9c29a374..d2926178 100644 --- a/common/AST.v +++ b/common/AST.v @@ -576,7 +576,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 annot_arg) + | EF_annot (text: ident) (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. *) @@ -584,27 +584,15 @@ 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 @@ -616,7 +604,7 @@ Definition ef_sig (ef: external_function): signature := | EF_malloc => mksignature (Tint :: nil) (Some Tint) cc_default | EF_free => mksignature (Tint :: nil) None cc_default | EF_memcpy sz al => mksignature (Tint :: Tint :: nil) None cc_default - | EF_annot text targs => mksignature (annot_args_typ targs) None cc_default + | EF_annot text targs => mksignature targs None cc_default | EF_annot_val text targ => mksignature (targ :: nil) (Some targ) cc_default | EF_inline_asm text => mksignature nil None cc_default end. @@ -653,7 +641,7 @@ Definition external_function_eq: forall (ef1 ef2: external_function), {ef1=ef2} Proof. generalize ident_eq signature_eq chunk_eq typ_eq zeq Int.eq_dec; intros. decide equality. - apply list_eq_dec. decide equality. apply Float.eq_dec. + apply list_eq_dec. auto. Defined. Global Opaque external_function_eq. @@ -699,3 +687,56 @@ Definition transf_partial_fundef (fd: fundef A): res (fundef B) := end. End TRANSF_PARTIAL_FUNDEF. + +(** * Arguments to annotations *) + +Set Contextual Implicit. + +Inductive annot_arg (A: Type) : Type := + | AA_base (x: A) + | AA_int (n: int) + | AA_long (n: int64) + | AA_float (f: float) + | AA_single (f: float32) + | AA_loadstack (chunk: memory_chunk) (ofs: int) + | AA_addrstack (ofs: int) + | AA_loadglobal (chunk: memory_chunk) (id: ident) (ofs: int) + | AA_addrglobal (id: ident) (ofs: int) + | AA_longofwords (hi lo: annot_arg A). + +Fixpoint globals_of_annot_arg (A: Type) (a: annot_arg A) : list ident := + match a with + | AA_loadglobal chunk id ofs => id :: nil + | AA_addrglobal id ofs => id :: nil + | AA_longofwords hi lo => globals_of_annot_arg hi ++ globals_of_annot_arg lo + | _ => nil + end. + +Definition globals_of_annot_args (A: Type) (al: list (annot_arg A)) : list ident := + List.fold_right (fun a l => globals_of_annot_arg a ++ l) nil al. + +Fixpoint params_of_annot_arg (A: Type) (a: annot_arg A) : list A := + match a with + | AA_base x => x :: nil + | AA_longofwords hi lo => params_of_annot_arg hi ++ params_of_annot_arg lo + | _ => nil + end. + +Definition params_of_annot_args (A: Type) (al: list (annot_arg A)) : list A := + List.fold_right (fun a l => params_of_annot_arg a ++ l) nil al. + +Fixpoint map_annot_arg (A B: Type) (f: A -> B) (a: annot_arg A) : annot_arg B := + match a with + | AA_base x => AA_base (f x) + | AA_int n => AA_int n + | AA_long n => AA_long n + | AA_float n => AA_float n + | AA_single n => AA_single n + | AA_loadstack chunk ofs => AA_loadstack chunk ofs + | AA_addrstack ofs => AA_addrstack ofs + | AA_loadglobal chunk id ofs => AA_loadglobal chunk id ofs + | AA_addrglobal id ofs => AA_addrglobal id ofs + | AA_longofwords hi lo => + AA_longofwords (map_annot_arg f hi) (map_annot_arg f lo) + end. + -- cgit