diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-11 18:18:17 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-11 18:18:17 +0100 |
commit | af1b08974ff75966ec48b4d93d5da8b5a4beab43 (patch) | |
tree | 76405e7e720552ec89048bf4620550a3bd8bd3b6 /driver | |
parent | ca1536a5d9e850cf9c86a70f421412d2c7bdff38 (diff) | |
parent | 9e706de1eb25d6d6dbeb1eb2ced71e48523a499f (diff) | |
download | compcert-kvx-af1b08974ff75966ec48b4d93d5da8b5a4beab43.tar.gz compcert-kvx-af1b08974ff75966ec48b4d93d5da8b5a4beab43.zip |
Merge remote-tracking branch 'origin/mppa-work' into mppa-cse3
Diffstat (limited to 'driver')
-rw-r--r-- | driver/Clflags.ml | 4 | ||||
-rw-r--r-- | driver/Compiler.v | 10 | ||||
-rw-r--r-- | driver/Driver.ml | 6 |
3 files changed, 10 insertions, 10 deletions
diff --git a/driver/Clflags.ml b/driver/Clflags.ml index f4022941..7e3b23d8 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -29,8 +29,8 @@ let option_fcse = ref true let option_fcse2 = ref true let option_fcse3 = ref true let option_fredundancy = ref true -let option_fduplicate = ref false -let option_finvertcond = ref true (* only active if option_fduplicate is also true *) +let option_fduplicate = ref 0 +let option_finvertcond = ref true let option_ftracelinearize = ref false let option_fpostpass = ref true let option_fpostpass_sched = ref "list" diff --git a/driver/Compiler.v b/driver/Compiler.v index 22955160..c2428d94 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -136,7 +136,7 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@ print (print_RTL 2) @@ time "Renumbering" Renumber.transf_program @@ print (print_RTL 3) - @@@ partial_if Compopts.optim_duplicate (time "Tail-duplicating" Duplicate.transf_program) + @@@ time "Tail-duplicating" Duplicate.transf_program @@ print (print_RTL 4) @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program) @@ print (print_RTL 5) @@ -258,7 +258,7 @@ Definition CompCert's_passes := ::: mkpass (match_if Compopts.optim_tailcalls Tailcallproof.match_prog) ::: mkpass Inliningproof.match_prog ::: mkpass Renumberproof.match_prog - ::: mkpass (match_if Compopts.optim_duplicate Duplicateproof.match_prog) + ::: mkpass Duplicateproof.match_prog ::: mkpass (match_if Compopts.optim_constprop Constpropproof.match_prog) ::: mkpass (match_if Compopts.optim_constprop Renumberproof.match_prog) ::: mkpass (match_if Compopts.optim_CSE CSEproof.match_prog) @@ -306,7 +306,7 @@ 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 (p9 := Renumber.transf_program p8) in *. - destruct (partial_if optim_duplicate Duplicate.transf_program p9) as [p10|e] eqn:P10; simpl in T; try discriminate. + destruct (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 *. destruct (partial_if optim_CSE CSE.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate. @@ -332,7 +332,7 @@ Proof. 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 Renumberproof.transf_program_match; auto. - exists p10; split. eapply partial_if_match; eauto. apply Duplicateproof.transf_program_match; auto. + exists p10; split. apply Duplicateproof.transf_program_match; auto. exists p11; split. apply total_if_match. apply Constpropproof.transf_program_match. exists p12; split. apply total_if_match. apply Renumberproof.transf_program_match. exists p13; split. eapply partial_if_match; eauto. apply CSEproof.transf_program_match. @@ -419,7 +419,7 @@ Ltac DestructM := eapply Inliningproof.transf_program_correct; eassumption. 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 Duplicateproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Constpropproof.transf_program_correct. eapply compose_forward_simulations. diff --git a/driver/Driver.ml b/driver/Driver.ml index 6f32fc33..12b61d86 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -205,7 +205,7 @@ Processing options: -finvertcond Invert conditions based on predicted paths (to prefer fallthrough). Requires -fduplicate to be also activated [on] -ftracelinearize Linearizes based on the traces identified by duplicate phase - It is recommended to also activate -fduplicate with this pass [off] + It is heavily recommended to activate -finvertcond with this pass [off] -fforward-moves Forward moves after CSE -finline Perform inlining of functions [on] -finline-functions-called-once Integrate functions only required by their @@ -319,7 +319,7 @@ let cmdline_actions = [ Exact "-O0", Unit (unset_all optimization_options); Exact "-O", Unit (set_all optimization_options); - _Regexp "-O1", Self (fun _ -> set_all optimization_options (); option_fpostpass := false; option_fduplicate := false); + _Regexp "-O1", Self (fun _ -> set_all optimization_options (); option_fpostpass := false); _Regexp "-O[123]$", Unit (set_all optimization_options); Exact "-Os", Set option_Osize; Exact "-Obranchless", Set option_Obranchless; @@ -395,7 +395,7 @@ let cmdline_actions = @ f_opt "cse3" option_fcse3 @ f_opt "redundancy" option_fredundancy @ f_opt "postpass" option_fpostpass - @ f_opt "duplicate" option_fduplicate + @ [ Exact "-fduplicate", Integer (fun n -> option_fduplicate := n) ] @ f_opt "invertcond" option_finvertcond @ f_opt "tracelinearize" option_ftracelinearize @ f_opt_str "postpass" option_fpostpass option_fpostpass_sched |