From 1972df30827022dcb39110cddf9032eaa3dc61b9 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 8 Apr 2020 11:35:17 +0200 Subject: begin installing profiling --- common/AST.v | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'common/AST.v') diff --git a/common/AST.v b/common/AST.v index 595ace01..846678c2 100644 --- a/common/AST.v +++ b/common/AST.v @@ -466,6 +466,7 @@ Qed. (* Identifiers for profiling information *) Definition profiling_id := Z.t. +Definition profiling_kind := Z.t. (** For most languages, the functions composing the program are either internal functions, defined within the language, or external functions, @@ -521,8 +522,8 @@ Inductive external_function : Type := (** 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. + | EF_profiling (id: profiling_id) (kind : profiling_kind). + (** Count one profiling event for this identifier and kind. Takes no argument. Produces no observable event. *) (** The type signature of an external function. *) @@ -541,7 +542,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 + | EF_profiling id kind => mksignature nil Tvoid cc_default end. (** Whether an external function should be inlined by the compiler. *) @@ -560,7 +561,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 + | EF_profiling id kind => true end. (** Whether an external function must reload its arguments. *) -- cgit