diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-08 11:35:17 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-08 11:35:17 +0200 |
| commit | 1972df30827022dcb39110cddf9032eaa3dc61b9 (patch) | |
| tree | 37a7e62cbe08675ca56d2f734104bd2d164f74e0 /common | |
| parent | 66f700d36891a90983bb97d245e04a2e97913c7d (diff) | |
| download | compcert-kvx-1972df30827022dcb39110cddf9032eaa3dc61b9.tar.gz compcert-kvx-1972df30827022dcb39110cddf9032eaa3dc61b9.zip | |
begin installing profiling
Diffstat (limited to 'common')
| -rw-r--r-- | common/AST.v | 9 | ||||
| -rw-r--r-- | common/Events.v | 2 | ||||
| -rw-r--r-- | common/PrintAST.ml | 4 |
3 files changed, 8 insertions, 7 deletions
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. *) diff --git a/common/Events.v b/common/Events.v index 16efd89c..033e2e03 100644 --- a/common/Events.v +++ b/common/Events.v @@ -1569,7 +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 + | EF_profiling id kind => extcall_profiling_sem end. Theorem external_call_spec: diff --git a/common/PrintAST.ml b/common/PrintAST.ml index 7f15bc91..69939428 100644 --- a/common/PrintAST.ml +++ b/common/PrintAST.ml @@ -62,8 +62,8 @@ let name_of_external = function | 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) - | EF_profiling(id) -> - sprintf "profiling %LX" (Z.to_int64 id) + | EF_profiling(id, kind) -> + sprintf "profiling %LX %d" (Z.to_int64 id) (Z.to_int kind) let rec print_builtin_arg px oc = function | BA x -> px oc x |