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 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 +++++---- common/Events.v | 2 +- common/PrintAST.ml | 4 ++-- 3 files changed, 8 insertions(+), 7 deletions(-) (limited to 'common') 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 -- cgit From d3a8a8870050810a7bc3fb5e004059197ec364f8 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 8 Apr 2020 13:06:00 +0200 Subject: print hashes --- common/AST.v | 5 +++-- common/PrintAST.ml | 2 +- 2 files changed, 4 insertions(+), 3 deletions(-) (limited to 'common') diff --git a/common/AST.v b/common/AST.v index 846678c2..268e13d5 100644 --- a/common/AST.v +++ b/common/AST.v @@ -465,7 +465,8 @@ Qed. (** * External functions *) (* Identifiers for profiling information *) -Definition profiling_id := Z.t. +Parameter profiling_id : Type. +Axiom profiling_id_eq : forall (x y : profiling_id), {x=y} + {x<>y}. Definition profiling_kind := Z.t. (** For most languages, the functions composing the program are either @@ -577,7 +578,7 @@ Definition ef_reloads (ef: external_function) : bool := Definition external_function_eq: forall (ef1 ef2: external_function), {ef1=ef2} + {ef1<>ef2}. Proof. - generalize ident_eq string_dec signature_eq chunk_eq typ_eq list_eq_dec zeq Int.eq_dec; intros. + generalize profiling_id_eq ident_eq string_dec signature_eq chunk_eq typ_eq list_eq_dec zeq Int.eq_dec; intros. decide equality. Defined. Global Opaque external_function_eq. diff --git a/common/PrintAST.ml b/common/PrintAST.ml index 69939428..e24607ee 100644 --- a/common/PrintAST.ml +++ b/common/PrintAST.ml @@ -63,7 +63,7 @@ let name_of_external = function | EF_debug(kind, text, targs) -> sprintf "debug%d %S" (P.to_int kind) (extern_atom text) | EF_profiling(id, kind) -> - sprintf "profiling %LX %d" (Z.to_int64 id) (Z.to_int kind) + sprintf "profiling %a %d" Profilingaux.spp_id id (Z.to_int kind) let rec print_builtin_arg px oc = function | BA x -> px oc x -- cgit From 7299996cac6c4747b6611b17f0af15fb08c6ee80 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 11 Apr 2020 22:02:46 +0200 Subject: fix reverse printing problem for hashes --- common/PrintAST.ml | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) (limited to 'common') diff --git a/common/PrintAST.ml b/common/PrintAST.ml index e24607ee..38bbfa47 100644 --- a/common/PrintAST.ml +++ b/common/PrintAST.ml @@ -47,6 +47,13 @@ let name_of_chunk = function | Many32 -> "any32" | Many64 -> "any64" +let spp_profiling_id () (x : Digest.t) : string = + let s = Buffer.create 32 in + for i=0 to 15 do + Printf.bprintf s "%02x" (Char.code (String.get x i)) + done; + Buffer.contents s;; + let name_of_external = function | EF_external(name, sg) -> sprintf "extern %S" (camlstring_of_coqstring name) | EF_builtin(name, sg) -> sprintf "builtin %S" (camlstring_of_coqstring name) @@ -63,7 +70,7 @@ let name_of_external = function | EF_debug(kind, text, targs) -> sprintf "debug%d %S" (P.to_int kind) (extern_atom text) | EF_profiling(id, kind) -> - sprintf "profiling %a %d" Profilingaux.spp_id id (Z.to_int kind) + sprintf "profiling %a %d" spp_profiling_id id (Z.to_int kind) let rec print_builtin_arg px oc = function | BA x -> px oc x -- cgit