aboutsummaryrefslogtreecommitdiffstats
path: root/driver
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-03-11 18:18:17 +0100
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-03-11 18:18:17 +0100
commitaf1b08974ff75966ec48b4d93d5da8b5a4beab43 (patch)
tree76405e7e720552ec89048bf4620550a3bd8bd3b6 /driver
parentca1536a5d9e850cf9c86a70f421412d2c7bdff38 (diff)
parent9e706de1eb25d6d6dbeb1eb2ced71e48523a499f (diff)
downloadcompcert-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.ml4
-rw-r--r--driver/Compiler.v10
-rw-r--r--driver/Driver.ml6
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