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 --- driver/Clflags.ml | 3 +++ driver/Compopts.v | 3 +++ driver/Driver.ml | 4 +++- 3 files changed, 9 insertions(+), 1 deletion(-) (limited to 'driver') 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 From 3c30567c452f030267d0fb09465adf8d7b44a90d Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 8 Apr 2020 12:36:24 +0200 Subject: installed Profiling (not finished) --- driver/Compiler.v | 33 +++++++++++++++++++++------------ 1 file changed, 21 insertions(+), 12 deletions(-) (limited to 'driver') diff --git a/driver/Compiler.v b/driver/Compiler.v index 499feff2..dc32cd3f 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -37,6 +37,7 @@ Require Selection. Require RTLgen. Require Tailcall. Require Inlining. +Require Profiling. Require Renumber. Require Duplicate. Require Constprop. @@ -62,6 +63,7 @@ Require Selectionproof. Require RTLgenproof. Require Tailcallproof. Require Inliningproof. +Require Profilingproof. Require Renumberproof. Require Duplicateproof. Require Constpropproof. @@ -132,26 +134,28 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 1) @@@ time "Inlining" Inlining.transf_program @@ print (print_RTL 2) - @@ time "Renumbering" Renumber.transf_program + @@ total_if Compopts.profile_arcs (time "Profiling insertion" Profiling.transf_program) @@ print (print_RTL 3) - @@@ partial_if Compopts.optim_duplicate (time "Tail-duplicating" Duplicate.transf_program) + @@ time "Renumbering" Renumber.transf_program @@ print (print_RTL 4) - @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) + @@@ partial_if Compopts.optim_duplicate (time "Tail-duplicating" Duplicate.transf_program) @@ print (print_RTL 5) - @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program) + @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) @@ print (print_RTL 6) - @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) + @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program) @@ print (print_RTL 7) - @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program) + @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) @@ print (print_RTL 8) - @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program + @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program) @@ print (print_RTL 9) - @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) + @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program @@ print (print_RTL 10) - @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program + @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) @@ print (print_RTL 11) - @@@ time "Unused globals" Unusedglob.transform_program + @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program @@ print (print_RTL 12) + @@@ time "Unused globals" Unusedglob.transform_program + @@ print (print_RTL 13) @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL @@ time "Branch tunneling" Tunneling.tunnel_program @@ -253,6 +257,7 @@ Definition CompCert's_passes := ::: mkpass RTLgenproof.match_prog ::: mkpass (match_if Compopts.optim_tailcalls Tailcallproof.match_prog) ::: mkpass Inliningproof.match_prog + ::: mkpass (match_if Compopts.profile_arcs Profilingproof.match_prog) ::: mkpass Renumberproof.match_prog ::: mkpass (match_if Compopts.optim_duplicate Duplicateproof.match_prog) ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog) @@ -300,7 +305,8 @@ Proof. unfold transf_rtl_program, time in T. rewrite ! compose_print_identity in T. simpl in T. set (p7 := total_if optim_tailcalls Tailcall.transf_program p6) in *. destruct (Inlining.transf_program p7) as [p8|e] eqn:P8; simpl in T; try discriminate. - set (p9 := Renumber.transf_program p8) in *. + set (p8bis := total_if profile_arcs Profiling.transf_program p8) in *. + set (p9 := Renumber.transf_program p8bis) in *. destruct (partial_if optim_duplicate Duplicate.transf_program p9) as [p10|e] eqn:P10; simpl in T; try discriminate. set (p11 := total_if optim_constprop Constprop.transf_program p10) in *. set (p12 := total_if optim_constprop Renumber.transf_program p11) in *. @@ -325,6 +331,7 @@ Proof. exists p6; split. apply RTLgenproof.transf_program_match; auto. exists p7; split. apply total_if_match. apply Tailcallproof.transf_program_match. exists p8; split. apply Inliningproof.transf_program_match; auto. + exists p8bis; split. apply total_if_match. apply Profilingproof.transf_program_match; auto. exists p9; split. apply Renumberproof.transf_program_match; auto. exists p10; split. eapply partial_if_match; eauto. apply Duplicateproof.transf_program_match; auto. exists p11; split. apply total_if_match. apply Constpropproof.transf_program_match. @@ -392,7 +399,7 @@ Ltac DestructM := destruct H as (p & M & MM); clear H end. repeat DestructM. subst tp. - assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p25)). + assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p26)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -410,6 +417,8 @@ Ltac DestructM := eapply match_if_simulation. eassumption. exact Tailcallproof.transf_program_correct. eapply compose_forward_simulations. eapply Inliningproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact Profilingproof.transf_program_correct. eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Duplicateproof.transf_program_correct. -- cgit From 96165dbec88ab4c951d99e64e51f5c55a1244137 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 8 Apr 2020 16:28:00 +0200 Subject: fixed a bug in support libraries; reload profiling info --- driver/Clflags.ml | 1 - driver/Driver.ml | 1 + 2 files changed, 1 insertion(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 87c8d9c8..600c3371 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -84,4 +84,3 @@ let option_all_loads_nontrap = ref false let option_inline_auto_threshold = ref 0 let option_profile_arcs = ref false - diff --git a/driver/Driver.ml b/driver/Driver.ml index 909ef0d5..7fbcb025 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -328,6 +328,7 @@ let cmdline_actions = _Regexp "-O[123]$", Unit (set_all optimization_options); Exact "-Os", Set option_Osize; Exact "-Obranchless", Set option_Obranchless; + Exact "-fprofile-use=", String (fun s -> Profilingaux.load_profiling_info s); Exact "-finline-auto-threshold", Integer (fun n -> option_inline_auto_threshold := n); Exact "-fsmall-data", Integer(fun n -> option_small_data := n); Exact "-fsmall-const", Integer(fun n -> option_small_const := n); -- cgit From c3f5f3dbd088091e3fab9f357b01693932d148f8 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 8 Apr 2020 17:02:45 +0200 Subject: reloading and exploiting seems to work --- driver/Clflags.ml | 1 + driver/Compiler.v | 33 +++++++++++++++++++++------------ driver/Compopts.v | 3 +++ driver/Driver.ml | 4 +++- 4 files changed, 28 insertions(+), 13 deletions(-) (limited to 'driver') diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 600c3371..e8f7cef2 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -84,3 +84,4 @@ let option_all_loads_nontrap = ref false let option_inline_auto_threshold = ref 0 let option_profile_arcs = ref false +let option_fbranch_probabilities = ref true diff --git a/driver/Compiler.v b/driver/Compiler.v index dc32cd3f..3f0ac3e5 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -38,6 +38,7 @@ Require RTLgen. Require Tailcall. Require Inlining. Require Profiling. +Require ProfilingExploit. Require Renumber. Require Duplicate. Require Constprop. @@ -64,6 +65,7 @@ Require RTLgenproof. Require Tailcallproof. Require Inliningproof. Require Profilingproof. +Require ProfilingExploitproof. Require Renumberproof. Require Duplicateproof. Require Constpropproof. @@ -136,26 +138,28 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 2) @@ total_if Compopts.profile_arcs (time "Profiling insertion" Profiling.transf_program) @@ print (print_RTL 3) - @@ time "Renumbering" Renumber.transf_program + @@ total_if Compopts.branch_probabilities (time "Profiling use" ProfilingExploit.transf_program) @@ print (print_RTL 4) - @@@ partial_if Compopts.optim_duplicate (time "Tail-duplicating" Duplicate.transf_program) + @@ time "Renumbering" Renumber.transf_program @@ print (print_RTL 5) - @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) + @@@ partial_if Compopts.optim_duplicate (time "Tail-duplicating" Duplicate.transf_program) @@ print (print_RTL 6) - @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program) + @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) @@ print (print_RTL 7) - @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) + @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program) @@ print (print_RTL 8) - @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program) + @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) @@ print (print_RTL 9) - @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program + @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program) @@ print (print_RTL 10) - @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) + @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program @@ print (print_RTL 11) - @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program + @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) @@ print (print_RTL 12) - @@@ time "Unused globals" Unusedglob.transform_program + @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program @@ print (print_RTL 13) + @@@ time "Unused globals" Unusedglob.transform_program + @@ print (print_RTL 14) @@@ time "Register allocation" Allocation.transf_program @@ print print_LTL @@ time "Branch tunneling" Tunneling.tunnel_program @@ -258,6 +262,7 @@ Definition CompCert's_passes := ::: mkpass (match_if Compopts.optim_tailcalls Tailcallproof.match_prog) ::: mkpass Inliningproof.match_prog ::: mkpass (match_if Compopts.profile_arcs Profilingproof.match_prog) + ::: mkpass (match_if Compopts.branch_probabilities ProfilingExploitproof.match_prog) ::: mkpass Renumberproof.match_prog ::: mkpass (match_if Compopts.optim_duplicate Duplicateproof.match_prog) ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog) @@ -306,7 +311,8 @@ Proof. set (p7 := total_if optim_tailcalls Tailcall.transf_program p6) in *. destruct (Inlining.transf_program p7) as [p8|e] eqn:P8; simpl in T; try discriminate. set (p8bis := total_if profile_arcs Profiling.transf_program p8) in *. - set (p9 := Renumber.transf_program p8bis) in *. + set (p8ter := total_if branch_probabilities ProfilingExploit.transf_program p8bis) in *. + set (p9 := Renumber.transf_program p8ter) in *. destruct (partial_if optim_duplicate Duplicate.transf_program p9) as [p10|e] eqn:P10; simpl in T; try discriminate. set (p11 := total_if optim_constprop Constprop.transf_program p10) in *. set (p12 := total_if optim_constprop Renumber.transf_program p11) in *. @@ -332,6 +338,7 @@ Proof. exists p7; split. apply total_if_match. apply Tailcallproof.transf_program_match. exists p8; split. apply Inliningproof.transf_program_match; auto. exists p8bis; split. apply total_if_match. apply Profilingproof.transf_program_match; auto. + exists p8ter; split. apply total_if_match. apply ProfilingExploitproof.transf_program_match; auto. exists p9; split. apply Renumberproof.transf_program_match; auto. exists p10; split. eapply partial_if_match; eauto. apply Duplicateproof.transf_program_match; auto. exists p11; split. apply total_if_match. apply Constpropproof.transf_program_match. @@ -399,7 +406,7 @@ Ltac DestructM := destruct H as (p & M & MM); clear H end. repeat DestructM. subst tp. - assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p26)). + assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p27)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -419,6 +426,8 @@ Ltac DestructM := eapply Inliningproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Profilingproof.transf_program_correct. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. exact ProfilingExploitproof.transf_program_correct. eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Duplicateproof.transf_program_correct. diff --git a/driver/Compopts.v b/driver/Compopts.v index 245322ef..98cbcc37 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -78,6 +78,9 @@ Parameter optim_forward_moves: unit -> bool. (** Flag -fprofile-arcs. Add profiling logger. *) Parameter profile_arcs : unit -> bool. +(** Flag -fbranch_probabilities. Use profiling information if available *) +Parameter branch_probabilities : 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 7fbcb025..29fbaa7c 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -222,8 +222,10 @@ Code generation options: (use -fno- to turn off -f) -falign-functions Set alignment (in bytes) of function entry points -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]. + -fcommon Put uninitialized globals in the common section [on] -fprofile-arcs Profile branches [off]. + -fprofile-use= filename Use profiling information in filename + -fbranch-probabilities Use profiling information (if available) for branches [on] |} ^ target_help ^ toolchain_help ^ -- cgit From 7aca3fcf600365b416865a6b6bc6ecc9852b08df Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 8 Apr 2020 17:24:09 +0200 Subject: -fbranch-probabilities --- driver/Driver.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'driver') diff --git a/driver/Driver.ml b/driver/Driver.ml index 29fbaa7c..0f716168 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -417,7 +417,8 @@ let cmdline_actions = @ f_opt "all-loads-nontrap" option_all_loads_nontrap @ f_opt "forward-moves" option_fforward_moves (* Code generation options *) - @ f_opt "profile-arcs" option_profile_arcs + @ f_opt "profile-arcs" option_profile_arcs + @ f_opt "branch-probabilities" option_fbranch_probabilities @ f_opt "fpu" option_ffpu @ f_opt "sse" option_ffpu (* backward compatibility *) @ [ -- cgit