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 --- Makefile | 1 + backend/CSE.v | 2 +- backend/Profiling.v | 97 +++++++++++++++++++++++++++++------------------------ cfrontend/Cexec.v | 2 +- common/AST.v | 9 ++--- common/Events.v | 2 +- common/PrintAST.ml | 4 +-- driver/Clflags.ml | 3 ++ driver/Compopts.v | 3 ++ driver/Driver.ml | 4 ++- 10 files changed, 73 insertions(+), 54 deletions(-) diff --git a/Makefile b/Makefile index 2cd40800..cad61d9d 100644 --- a/Makefile +++ b/Makefile @@ -79,6 +79,7 @@ BACKEND=\ RTLgen.v RTLgenspec.v RTLgenproof.v \ Tailcall.v Tailcallproof.v \ Inlining.v Inliningspec.v Inliningproof.v \ + Profiling.v Profilingproof.v \ Renumber.v Renumberproof.v \ Duplicate.v Duplicateproof.v \ RTLtyping.v \ diff --git a/backend/CSE.v b/backend/CSE.v index 9ba50a34..838d96a6 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -493,7 +493,7 @@ Definition transfer (f: function) (approx: PMap.t VA.t) (pc: node) (before: numb | _ => empty_numbering end - | EF_vload _ | EF_annot _ _ _ | EF_annot_val _ _ _ | EF_debug _ _ _ | EF_profiling _ => + | EF_vload _ | EF_annot _ _ _ | EF_annot_val _ _ _ | EF_debug _ _ _ | EF_profiling _ _ => set_res_unknown before res end | Icond cond args ifso ifnot _ => diff --git a/backend/Profiling.v b/backend/Profiling.v index ce0e4e38..4995c507 100644 --- a/backend/Profiling.v +++ b/backend/Profiling.v @@ -4,54 +4,63 @@ Require Import Memory Registers Op RTL. Local Open Scope positive. -Definition inject_profiling_call (prog : code) - (pc extra_pc ifso ifnot : node) : node * code := - let extra_pc' := Pos.succ extra_pc in - let prog' := PTree.set extra_pc - (Ibuiltin (EF_profiling 0%Z) nil BR_none ifso) prog in - let prog'':= PTree.set extra_pc' - (Ibuiltin (EF_profiling 0%Z) nil BR_none ifnot) prog' in - (Pos.succ extra_pc', prog''). - -Definition inject_at (prog : code) (pc extra_pc : node) : node * code := - match PTree.get pc prog with - | Some (Icond cond args ifso ifnot expected) => - inject_profiling_call - (PTree.set pc - (Icond cond args extra_pc (Pos.succ extra_pc) expected) prog) +Parameter fundef_id : fundef -> Z. +Parameter branch_id : Z -> node -> Z. + +Section PER_FUNCTION_ID. + Variable function_id : Z. + + Definition inject_profiling_call (prog : code) + (pc extra_pc ifso ifnot : node) : node * code := + let id := branch_id function_id pc in + let extra_pc' := Pos.succ extra_pc in + let prog' := PTree.set extra_pc + (Ibuiltin (EF_profiling id 0%Z) nil BR_none ifso) prog in + let prog'':= PTree.set extra_pc' + (Ibuiltin (EF_profiling id 1%Z) nil BR_none ifnot) prog' in + (Pos.succ extra_pc', prog''). + + Definition inject_at (prog : code) (pc extra_pc : node) : node * code := + match PTree.get pc prog with + | Some (Icond cond args ifso ifnot expected) => + inject_profiling_call + (PTree.set pc + (Icond cond args extra_pc (Pos.succ extra_pc) expected) prog) pc extra_pc ifso ifnot - | _ => inject_profiling_call prog pc extra_pc 1 1 (* does not happen *) - end. - -Definition inject_at' (already : node * code) pc := - let (extra_pc, prog) := already in - inject_at prog pc extra_pc. - -Definition inject_l (prog : code) extra_pc injections := - List.fold_left (fun already (inject_pc : node) => - inject_at' already inject_pc) - injections - (extra_pc, prog). - -Definition gen_conditions (prog : code) := - List.map fst (PTree.elements (PTree.filter1 - (fun instr => - match instr with - | Icond cond args ifso ifnot expected => true - | _ => false - end) prog)). - -Definition transf_function (f : function) : function := - let max_pc := max_pc_function f in - let conditions := gen_conditions (fn_code f) in + | _ => inject_profiling_call prog pc extra_pc 1 1 (* does not happen *) + end. + + Definition inject_at' (already : node * code) pc := + let (extra_pc, prog) := already in + inject_at prog pc extra_pc. + + Definition inject_l (prog : code) extra_pc injections := + List.fold_left (fun already (inject_pc : node) => + inject_at' already inject_pc) + injections + (extra_pc, prog). + + Definition gen_conditions (prog : code) := + List.map fst (PTree.elements (PTree.filter1 + (fun instr => + match instr with + | Icond cond args ifso ifnot expected => true + | _ => false + end) prog)). + + Definition transf_function (f : function) : function := + let max_pc := max_pc_function f in + let conditions := gen_conditions (fn_code f) in {| fn_sig := f.(fn_sig); - fn_params := f.(fn_params); - fn_stacksize := f.(fn_stacksize); - fn_code := snd (inject_l (fn_code f) (Pos.succ max_pc) conditions); - fn_entrypoint := f.(fn_entrypoint) |}. + fn_params := f.(fn_params); + fn_stacksize := f.(fn_stacksize); + fn_code := snd (inject_l (fn_code f) (Pos.succ max_pc) conditions); + fn_entrypoint := f.(fn_entrypoint) |}. + +End PER_FUNCTION_ID. Definition transf_fundef (fd: fundef) : fundef := - AST.transf_fundef transf_function fd. + AST.transf_fundef (transf_function (fundef_id fd)) fd. Definition transf_program (p: program) : program := transform_program transf_fundef p. diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index 609689a7..fbf9bbeb 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -535,7 +535,7 @@ Definition do_external (ef: external_function): | EF_annot_val kind text targ => do_ef_annot_val text targ | EF_inline_asm text sg clob => do_inline_assembly text sg ge | EF_debug kind text targs => do_ef_debug kind text targs - | EF_profiling id => do_ef_profiling id + | EF_profiling id kind => do_ef_profiling id end. Lemma do_ef_external_sound: 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 diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 6986fb96..87c8d9c8 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -82,3 +82,6 @@ let option_fcoalesce_mem = ref true let option_fforward_moves = ref true let option_all_loads_nontrap = ref false let option_inline_auto_threshold = ref 0 + +let option_profile_arcs = ref false + diff --git a/driver/Compopts.v b/driver/Compopts.v index 848657e5..245322ef 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -75,6 +75,9 @@ Parameter all_loads_nontrap: unit -> bool. (** Flag -fforward-moves. Forward moves after CSE. *) Parameter optim_forward_moves: unit -> bool. +(** Flag -fprofile-arcs. Add profiling logger. *) +Parameter profile_arcs : unit -> bool. + (* TODO is there a more appropriate place? *) Require Import Coqlib. Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := f. diff --git a/driver/Driver.ml b/driver/Driver.ml index 388482a0..909ef0d5 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -223,6 +223,7 @@ Code generation options: (use -fno- to turn off -f) -falign-branch-targets Set alignment (in bytes) of branch targets -falign-cond-branches Set alignment (in bytes) of conditional branches -fcommon Put uninitialized globals in the common section [on]. + -fprofile-arcs Profile branches [off]. |} ^ target_help ^ toolchain_help ^ @@ -412,7 +413,8 @@ let cmdline_actions = @ f_opt "coalesce-mem" option_fcoalesce_mem @ f_opt "all-loads-nontrap" option_all_loads_nontrap @ f_opt "forward-moves" option_fforward_moves -(* Code generation options *) + (* Code generation options *) + @ f_opt "profile-arcs" option_profile_arcs @ f_opt "fpu" option_ffpu @ f_opt "sse" option_ffpu (* backward compatibility *) @ [ -- cgit