From 84c5408706feb748cf364efcbe6a67512d622f40 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 8 Apr 2020 09:49:24 +0200 Subject: added EF_profiling --- common/AST.v | 10 ++++++++- common/Events.v | 65 ++++++++++++++++++++++++++++++++++++++++++++---------- common/PrintAST.ml | 4 +++- 3 files changed, 65 insertions(+), 14 deletions(-) (limited to 'common') diff --git a/common/AST.v b/common/AST.v index eb34d675..595ace01 100644 --- a/common/AST.v +++ b/common/AST.v @@ -464,6 +464,9 @@ Qed. (** * External functions *) +(* Identifiers for profiling information *) +Definition profiling_id := Z.t. + (** For most languages, the functions composing the program are either internal functions, defined within the language, or external functions, defined outside. External functions include system calls but also @@ -514,10 +517,13 @@ Inductive external_function : Type := used with caution, as it can invalidate the semantic preservation theorem. Generated only if [-finline-asm] is given. *) - | EF_debug (kind: positive) (text: ident) (targs: list typ). + | EF_debug (kind: positive) (text: ident) (targs: list typ) (** Transport debugging information from the front-end to the generated assembly. Takes zero, one or several arguments like [EF_annot]. Unlike [EF_annot], produces no observable event. *) + | EF_profiling (id: profiling_id). + (** Count one profiling event for this identifier. + Takes no argument. Produces no observable event. *) (** The type signature of an external function. *) @@ -535,6 +541,7 @@ Definition ef_sig (ef: external_function): signature := | EF_annot_val kind text targ => mksignature (targ :: nil) targ cc_default | EF_inline_asm text sg clob => sg | EF_debug kind text targs => mksignature targs Tvoid cc_default + | EF_profiling id => mksignature nil Tvoid cc_default end. (** Whether an external function should be inlined by the compiler. *) @@ -553,6 +560,7 @@ Definition ef_inline (ef: external_function) : bool := | EF_annot_val kind Text rg => true | EF_inline_asm text sg clob => true | EF_debug kind text targs => true + | EF_profiling id => true end. (** Whether an external function must reload its arguments. *) diff --git a/common/Events.v b/common/Events.v index 28bb992a..16efd89c 100644 --- a/common/Events.v +++ b/common/Events.v @@ -1378,6 +1378,11 @@ Inductive extcall_debug_sem (ge: Senv.t): | extcall_debug_sem_intro: forall vargs m, extcall_debug_sem ge vargs m E0 Vundef m. +Inductive extcall_profiling_sem (ge: Senv.t): + list val -> mem -> trace -> val -> mem -> Prop := + | extcall_profiling_sem_intro: forall vargs m, + extcall_profiling_sem ge vargs m E0 Vundef m. + Lemma extcall_debug_ok: forall targs, extcall_properties extcall_debug_sem @@ -1412,6 +1417,40 @@ Proof. split. constructor. auto. Qed. +Lemma extcall_profiling_ok: + forall targs, + extcall_properties extcall_profiling_sem + (mksignature targs Tvoid cc_default). +Proof. + intros; constructor; intros. +(* well typed *) +- inv H. simpl. auto. +(* symbols *) +- inv H0. econstructor; eauto. +(* valid blocks *) +- inv H; auto. +(* perms *) +- inv H; auto. +(* readonly *) +- inv H; auto. +(* mem extends *) +- inv H. + exists Vundef; exists m1'; intuition. + econstructor; eauto. +(* mem injects *) +- inv H0. + exists f; exists Vundef; exists m1'; intuition. + econstructor; eauto. + red; intros; congruence. +(* trace length *) +- inv H; simpl; omega. +(* receptive *) +- inv H; inv H0. exists Vundef, m1; constructor. +(* determ *) +- inv H; inv H0. + split. constructor. auto. +Qed. + (** ** Semantics of known built-in functions. *) (** Some built-in functions and runtime support functions have known semantics @@ -1530,6 +1569,7 @@ Definition external_call (ef: external_function): extcall_sem := | EF_annot_val kind txt targ => extcall_annot_val_sem txt targ | EF_inline_asm txt sg clb => inline_assembly_sem txt sg | EF_debug kind txt targs => extcall_debug_sem + | EF_profiling id => extcall_profiling_sem end. Theorem external_call_spec: @@ -1537,18 +1577,19 @@ Theorem external_call_spec: extcall_properties (external_call ef) (ef_sig ef). Proof. intros. unfold external_call, ef_sig; destruct ef. - apply external_functions_properties. - apply builtin_or_external_sem_ok. - apply builtin_or_external_sem_ok. - apply volatile_load_ok. - apply volatile_store_ok. - apply extcall_malloc_ok. - apply extcall_free_ok. - apply extcall_memcpy_ok. - apply extcall_annot_ok. - apply extcall_annot_val_ok. - apply inline_assembly_properties. - apply extcall_debug_ok. +- apply external_functions_properties. +- apply builtin_or_external_sem_ok. +- apply builtin_or_external_sem_ok. +- apply volatile_load_ok. +- apply volatile_store_ok. +- apply extcall_malloc_ok. +- apply extcall_free_ok. +- apply extcall_memcpy_ok. +- apply extcall_annot_ok. +- apply extcall_annot_val_ok. +- apply inline_assembly_properties. +- apply extcall_debug_ok. +- apply extcall_profiling_ok. Qed. Definition external_call_well_typed_gen ef := ec_well_typed (external_call_spec ef). diff --git a/common/PrintAST.ml b/common/PrintAST.ml index 3f718428..7f15bc91 100644 --- a/common/PrintAST.ml +++ b/common/PrintAST.ml @@ -61,7 +61,9 @@ let name_of_external = function | EF_annot_val(kind,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) + sprintf "debug%d %S" (P.to_int kind) (extern_atom text) + | EF_profiling(id) -> + sprintf "profiling %LX" (Z.to_int64 id) let rec print_builtin_arg px oc = function | BA x -> px oc x -- cgit