diff options
Diffstat (limited to 'driver')
| -rw-r--r-- | driver/Clflags.ml | 4 | ||||
| -rw-r--r-- | driver/Compiler.vexpand (renamed from driver/Compiler.v) | 194 | ||||
| -rw-r--r-- | driver/Compopts.v | 6 | ||||
| -rw-r--r-- | driver/Driver.ml | 16 |
4 files changed, 38 insertions, 182 deletions
diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 9d868de3..8f3b6605 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -82,10 +82,14 @@ let option_fglobaladdroffset = ref false let option_fxsaddr = ref true let option_faddx = ref false let option_fmadd = ref true +let option_div_i32 = ref "stsud" +let option_div_i64 = ref "stsud" let option_fcoalesce_mem = ref true let option_fforward_moves = ref true let option_fmove_loop_invariants = ref true let option_fnontrap_loads = ref true 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 let option_debug_compcert = ref 0 diff --git a/driver/Compiler.v b/driver/Compiler.vexpand index 17cb67af..0f59aab7 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.vexpand @@ -35,26 +35,7 @@ Require Cshmgen. Require Cminorgen. Require Selection. Require RTLgen. -Require Tailcall. -Require Inlining. -Require FirstNop. -Require Renumber. -Require Duplicate. -Require Constprop. -Require LICM. -Require CSE. -Require ForwardMoves. -Require CSE2. -Require CSE3. -Require Deadcode. -Require Unusedglob. -Require Allnontrap. -Require Allocation. -Require Tunneling. -Require Linearize. -Require CleanupLabels. -Require Debugvar. -Require Stacking. +EXPAND_RTL_REQUIRE Require Asmgen. (** Proofs of semantic preservation. *) Require SimplExprproof. @@ -63,26 +44,7 @@ Require Cshmgenproof. Require Cminorgenproof. Require Selectionproof. Require RTLgenproof. -Require Tailcallproof. -Require Inliningproof. -Require FirstNopproof. -Require Renumberproof. -Require Duplicateproof. -Require Constpropproof. -Require LICMproof. -Require CSEproof. -Require ForwardMovesproof. -Require CSE2proof. -Require CSE3proof. -Require Deadcodeproof. -Require Unusedglobproof. -Require Allnontrapproof. -Require Allocproof. -Require Tunnelingproof. -Require Linearizeproof. -Require CleanupLabelsproof. -Require Debugvarproof. -Require Stackingproof. +EXPAND_RTL_REQUIRE_PROOF Require Import Asmgenproof. (** Command-line flags. *) Require Import Compopts. @@ -134,48 +96,9 @@ Definition partial_if {A: Type} Definition transf_rtl_program (f: RTL.program) : res Asm.program := OK f @@ print (print_RTL 0) - @@ total_if Compopts.optim_tailcalls (time "Tail calls" Tailcall.transf_program) - @@ print (print_RTL 1) - @@@ time "Inlining" Inlining.transf_program - @@ print (print_RTL 2) - @@ total_if Compopts.optim_move_loop_invariants (time "Inserting initial nop" FirstNop.transf_program) - @@ print (print_RTL 3) - @@ time "Renumbering" Renumber.transf_program - @@ print (print_RTL 4) - @@@ partial_if Compopts.optim_duplicate (time "Tail-duplicating" Duplicate.transf_program) - @@ print (print_RTL 5) - @@ time "Renumbering pre constprop" Renumber.transf_program - @@ print (print_RTL 6) - @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) - @@ print (print_RTL 7) - @@@ partial_if Compopts.optim_move_loop_invariants (time "LICM" LICM.transf_program) - @@ print (print_RTL 8) - @@ total_if Compopts.optim_move_loop_invariants (time "Renumbering pre CSE" Renumber.transf_program) - @@ print (print_RTL 9) - @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program) - @@ print (print_RTL 10) - @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program) - @@ print (print_RTL 11) - @@@ partial_if Compopts.optim_CSE3 (time "CSE3" CSE3.transf_program) - @@ print (print_RTL 12) - @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program - @@ print (print_RTL 13) - @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program) - @@ print (print_RTL 14) - @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program - @@ print (print_RTL 15) - @@@ time "Unused globals" Unusedglob.transform_program - @@ print (print_RTL 16) - @@@ time "Register allocation" Allocation.transf_program - @@ print print_LTL - @@ time "Branch tunneling" Tunneling.tunnel_program - @@@ time "CFG linearization" Linearize.transf_program - @@ time "Label cleanup" CleanupLabels.transf_program - @@@ partial_if Compopts.debug (time "Debugging info for local variables" Debugvar.transf_program) - @@@ time "Mach generation" Stacking.transf_program - @@ print print_Mach +EXPAND_RTL_TRANSF_PROGRAM @@@ time "Total Mach->Asm generation" Asmgen.transf_program. - + Definition transf_cminor_program (p: Cminor.program) : res Asm.program := OK p @@ print print_Cminor @@ -265,28 +188,7 @@ Definition CompCert's_passes := ::: mkpass Cminorgenproof.match_prog ::: mkpass Selectionproof.match_prog ::: mkpass RTLgenproof.match_prog - ::: mkpass (match_if Compopts.optim_tailcalls Tailcallproof.match_prog) - ::: mkpass Inliningproof.match_prog - ::: mkpass (match_if Compopts.optim_move_loop_invariants FirstNopproof.match_prog) - ::: mkpass Renumberproof.match_prog - ::: mkpass (match_if Compopts.optim_duplicate Duplicateproof.match_prog) - ::: mkpass Renumberproof.match_prog - ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog) - ::: mkpass (match_if Compopts.optim_move_loop_invariants LICMproof.match_prog) - ::: mkpass (match_if Compopts.optim_move_loop_invariants Renumberproof.match_prog) - ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog) - ::: mkpass (match_if Compopts.optim_CSE2 CSE2proof.match_prog) - ::: mkpass (match_if Compopts.optim_CSE3 CSE3proof.match_prog) - ::: mkpass (match_if Compopts.optim_forward_moves ForwardMovesproof.match_prog) - ::: mkpass (match_if Compopts.optim_redundancy Deadcodeproof.match_prog) - ::: mkpass (match_if Compopts.all_loads_nontrap Allnontrapproof.match_prog) - ::: mkpass Unusedglobproof.match_prog - ::: mkpass Allocproof.match_prog - ::: mkpass Tunnelingproof.match_prog - ::: mkpass Linearizeproof.match_prog - ::: mkpass CleanupLabelsproof.match_prog - ::: mkpass (match_if Compopts.debug Debugvarproof.match_prog) - ::: mkpass Stackingproof.match_prog +EXPAND_RTL_MKPASS ::: mkpass Asmgenproof.match_prog ::: pass_nil _. @@ -315,29 +217,9 @@ Proof. unfold transf_cminor_program, time in T. rewrite ! compose_print_identity in T. cbn in T. destruct (Selection.sel_program p4) as [p5|e] eqn:P5; cbn in T; try discriminate. destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; cbn in T; try discriminate. - unfold transf_rtl_program, time in T. rewrite ! compose_print_identity in T. cbn in T. - set (p7 := total_if optim_tailcalls Tailcall.transf_program p6) in *. - destruct (Inlining.transf_program p7) as [p8|e] eqn:P8; cbn in T; try discriminate. - set (p9 := total_if Compopts.optim_move_loop_invariants FirstNop.transf_program p8) in *. - set (p9bis := Renumber.transf_program p9) in *. - destruct (partial_if optim_duplicate Duplicate.transf_program p9bis) as [p10|e] eqn:P10; cbn in T; try discriminate. - set (p11 := Renumber.transf_program p10) in *. - set (p12 := total_if optim_constprop Constprop.transf_program p11) in *. - destruct (partial_if optim_move_loop_invariants LICM.transf_program p12) as [p12bis|e] eqn:P12bis; cbn in T; try discriminate. - set (p12ter :=(total_if optim_move_loop_invariants Renumber.transf_program p12bis)) in *. - destruct (partial_if optim_CSE CSE.transf_program p12ter) as [p13|e] eqn:P13; cbn in T; try discriminate. - set (p13bis := total_if optim_CSE2 CSE2.transf_program p13) in *. - destruct (partial_if optim_CSE3 CSE3.transf_program p13bis) as [p13ter|e] eqn:P13ter; cbn in T; try discriminate. - set (p13quater := total_if optim_forward_moves ForwardMoves.transf_program p13ter) in *. - destruct (partial_if optim_redundancy Deadcode.transf_program p13quater) as [p14|e] eqn:P14; cbn in T; try discriminate. - set (p14bis := total_if all_loads_nontrap Allnontrap.transf_program p14) in *. - destruct (Unusedglob.transform_program p14bis) as [p15|e] eqn:P15; cbn in T; try discriminate. - destruct (Allocation.transf_program p15) as [p16|e] eqn:P16; cbn in T; try discriminate. - set (p17 := Tunneling.tunnel_program p16) in *. - destruct (Linearize.transf_program p17) as [p18|e] eqn:P18; cbn in T; try discriminate. - set (p19 := CleanupLabels.transf_program p18) in *. - destruct (partial_if debug Debugvar.transf_program p19) as [p20|e] eqn:P20; cbn in T; try discriminate. - destruct (Stacking.transf_program p20) as [p21|e] eqn:P21; cbn in T; try discriminate. + unfold transf_rtl_program, time in T. rewrite ! compose_print_identity in T. + cbn in T. +EXPAND_RTL_PROOF unfold match_prog; simpl. exists p1; split. apply SimplExprproof.transf_program_match; auto. exists p2; split. apply SimplLocalsproof.match_transf_program; auto. @@ -345,28 +227,7 @@ Proof. exists p4; split. apply Cminorgenproof.transf_program_match; auto. exists p5; split. apply Selectionproof.transf_program_match; auto. 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 p9; split. apply total_if_match. apply FirstNopproof.transf_program_match. - exists p9bis; split. apply Renumberproof.transf_program_match. - exists p10; split. eapply partial_if_match; eauto. apply Duplicateproof.transf_program_match; auto. - exists p11; split. apply Renumberproof.transf_program_match. - exists p12; split. apply total_if_match. apply Constpropproof.transf_program_match. - exists p12bis; split. eapply partial_if_match; eauto. apply LICMproof.transf_program_match. - exists p12ter; split. apply total_if_match; eauto. apply Renumberproof.transf_program_match. - exists p13; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. - exists p13bis; split. apply total_if_match. apply CSE2proof.transf_program_match. - exists p13ter; split. eapply partial_if_match; eauto. apply CSE3proof.transf_program_match. - exists p13quater; split. eapply total_if_match; eauto. apply ForwardMovesproof.transf_program_match. - exists p14; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match. - exists p14bis; split. eapply total_if_match; eauto. apply Allnontrapproof.transf_program_match. - exists p15; split. apply Unusedglobproof.transf_program_match; auto. - exists p16; split. apply Allocproof.transf_program_match; auto. - exists p17; split. apply Tunnelingproof.transf_program_match. - exists p18; split. apply Linearizeproof.transf_program_match; auto. - exists p19; split. apply CleanupLabelsproof.transf_program_match; auto. - exists p20; split. eapply partial_if_match; eauto. apply Debugvarproof.transf_program_match. - exists p21; split. apply Stackingproof.transf_program_match; auto. +EXPAND_RTL_PROOF2 exists tp; split. apply Asmgenproof.transf_program_match; auto. reflexivity. Qed. @@ -418,7 +279,9 @@ Ltac DestructM := destruct H as (p & M & MM); clear H end. repeat DestructM. subst tp. - assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p29)). + assert (F: forward_simulation (Cstrategy.semantics p) +EXPAND_ASM_SEMANTICS + ). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -432,38 +295,9 @@ Ltac DestructM := eapply Selectionproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply RTLgenproof.transf_program_correct; eassumption. +EXPAND_RTL_FORWARD_SIMULATIONS eapply compose_forward_simulations. - 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 FirstNopproof.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. - eapply compose_forward_simulations. - eapply compose_forward_simulations. eapply Renumberproof.transf_program_correct; eassumption. - eapply match_if_simulation. eassumption. exact Constpropproof.transf_program_correct. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact LICMproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact Renumberproof.transf_program_correct. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact CSEproof.transf_program_correct. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact CSE2proof.transf_program_correct. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact CSE3proof.transf_program_correct. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact ForwardMovesproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact Deadcodeproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply match_if_simulation. eassumption. exact Allnontrapproof.transf_program_correct. - eapply compose_forward_simulations. - eapply Unusedglobproof.transf_program_correct; eassumption. - eapply compose_forward_simulations. - eapply Allocproof.transf_program_correct; eassumption. + eapply Allocationproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply Tunnelingproof.transf_program_correct; eassumption. eapply compose_forward_simulations. diff --git a/driver/Compopts.v b/driver/Compopts.v index fb3481e2..3c5ccf36 100644 --- a/driver/Compopts.v +++ b/driver/Compopts.v @@ -90,6 +90,12 @@ 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. + +(** 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 ea9af62e..b9060ca7 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -226,7 +226,10 @@ Code generation options: (use -fno-<opt> to turn off -f<opt>) -falign-functions <n> Set alignment (in bytes) of function entry points -falign-branch-targets <n> Set alignment (in bytes) of branch targets -falign-cond-branches <n> 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 ^ @@ -293,6 +296,10 @@ let cmdline_actions = [Exact("-f" ^ name ^ "="), String (fun s -> (strref := (if s == "" then "list" else s)); ref := true) ] in + let f_str name strref default = + [Exact("-f" ^ name ^ "="), String + (fun s -> (strref := (if s == "" then default else s))) + ] in let check_align n = if n <= 0 || ((n land (n - 1)) <> 0) then error no_loc "requested alignment %d is not a power of 2" n @@ -331,6 +338,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 "-debug-compcert", Integer (fun n -> option_debug_compcert := n); Exact "-fsmall-data", Integer(fun n -> option_small_data := n); @@ -417,13 +425,17 @@ let cmdline_actions = @ f_opt "globaladdrtmp" option_fglobaladdrtmp @ f_opt "globaladdroffset" option_fglobaladdroffset @ f_opt "xsaddr" option_fxsaddr + @ f_str "div-i32" option_div_i32 "stsud" + @ f_str "div-i64" option_div_i64 "stsud" @ f_opt "addx" option_faddx @ f_opt "madd" option_fmadd @ f_opt "nontrap-loads" option_fnontrap_loads @ 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 "branch-probabilities" option_fbranch_probabilities @ f_opt "fpu" option_ffpu @ f_opt "sse" option_ffpu (* backward compatibility *) @ [ |