aboutsummaryrefslogtreecommitdiffstats
path: root/driver
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-04-20 18:27:36 +0200
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-04-20 18:27:36 +0200
commitc0449b50b6d461dbc431ee881ba3a35604961a42 (patch)
tree961d5419bbe90260e42970df44257f4b019e3a67 /driver
parent0c9cc34f2306b3ea073684806118f1ab36cfc993 (diff)
parenteead578fde08a1555086ed75714bca3ca1f9b1dc (diff)
downloadcompcert-kvx-c0449b50b6d461dbc431ee881ba3a35604961a42.tar.gz
compcert-kvx-c0449b50b6d461dbc431ee881ba3a35604961a42.zip
Merge remote-tracking branch 'origin/mppa-licm' into mppa-features
Diffstat (limited to 'driver')
-rw-r--r--driver/Clflags.ml5
-rw-r--r--driver/Compiler.v68
-rw-r--r--driver/Compopts.v6
-rw-r--r--driver/Driver.ml4
4 files changed, 60 insertions, 23 deletions
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 558e1d09..fd9603ee 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -79,9 +79,12 @@ let use_standard_headers = ref Configuration.has_standard_headers
let option_fglobaladdrtmp = ref false
let option_fglobaladdroffset = ref false
let option_fxsaddr = ref true
-let option_faddx = ref false
+let option_faddx = ref false
+let option_fmadd = ref true
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
diff --git a/driver/Compiler.v b/driver/Compiler.v
index ee091c37..69041ab0 100644
--- a/driver/Compiler.v
+++ b/driver/Compiler.v
@@ -39,9 +39,11 @@ Require Tailcall.
Require Inlining.
Require Profiling.
Require ProfilingExploit.
+Require FirstNop.
Require Renumber.
Require Duplicate.
Require Constprop.
+Require LICM.
Require CSE.
Require ForwardMoves.
Require CSE2.
@@ -67,9 +69,11 @@ Require Tailcallproof.
Require Inliningproof.
Require Profilingproof.
Require ProfilingExploitproof.
+Require FirstNopproof.
Require Renumberproof.
Require Duplicateproof.
Require Constpropproof.
+Require LICMproof.
Require CSEproof.
Require ForwardMovesproof.
Require CSE2proof.
@@ -142,28 +146,34 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program :=
@@ print (print_RTL 3)
@@ total_if Compopts.branch_probabilities (time "Profiling use" ProfilingExploit.transf_program)
@@ print (print_RTL 4)
- @@ time "Renumbering" Renumber.transf_program
+ @@ total_if Compopts.optim_move_loop_invariants (time "Inserting initial nop" FirstNop.transf_program)
@@ print (print_RTL 5)
- @@@ partial_if Compopts.optim_duplicate (time "Tail-duplicating" Duplicate.transf_program)
+ @@ time "Renumbering" Renumber.transf_program
@@ print (print_RTL 6)
- @@ 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 7)
- @@ total_if Compopts.optim_constprop (time "Renumbering" Renumber.transf_program)
+ @@ time "Renumbering pre constprop" Renumber.transf_program
@@ print (print_RTL 8)
- @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program)
+ @@ total_if Compopts.optim_constprop (time "Constant propagation" Constprop.transf_program)
@@ print (print_RTL 9)
- @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program)
+ @@@ partial_if Compopts.optim_move_loop_invariants (time "LICM" LICM.transf_program)
@@ print (print_RTL 10)
- @@@ partial_if Compopts.optim_CSE3 (time "CSE3" CSE3.transf_program)
+ @@ total_if Compopts.optim_move_loop_invariants (time "Renumbering pre CSE" Renumber.transf_program)
@@ print (print_RTL 11)
- @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program
+ @@@ partial_if Compopts.optim_CSE (time "CSE" CSE.transf_program)
@@ print (print_RTL 12)
- @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program)
+ @@ total_if Compopts.optim_CSE2 (time "CSE2" CSE2.transf_program)
@@ print (print_RTL 13)
- @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program
+ @@@ partial_if Compopts.optim_CSE3 (time "CSE3" CSE3.transf_program)
@@ print (print_RTL 14)
- @@@ time "Unused globals" Unusedglob.transform_program
+ @@ total_if Compopts.optim_forward_moves ForwardMoves.transf_program
@@ print (print_RTL 15)
+ @@@ partial_if Compopts.optim_redundancy (time "Redundancy elimination" Deadcode.transf_program)
+ @@ print (print_RTL 16)
+ @@ total_if Compopts.all_loads_nontrap Allnontrap.transf_program
+ @@ print (print_RTL 17)
+ @@@ time "Unused globals" Unusedglob.transform_program
+ @@ print (print_RTL 18)
@@@ time "Register allocation" Allocation.transf_program
@@ print print_LTL
@@ time "Branch tunneling" Tunneling.tunnel_program
@@ -267,10 +277,13 @@ Definition CompCert's_passes :=
::: mkpass Inliningproof.match_prog
::: mkpass (match_if Compopts.profile_arcs Profilingproof.match_prog)
::: mkpass (match_if Compopts.branch_probabilities ProfilingExploitproof.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_constprop Renumberproof.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)
@@ -317,11 +330,14 @@ Proof.
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 (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 *.
- destruct (partial_if optim_CSE CSE.transf_program p12) as [p13|e] eqn:P13; simpl in T; try discriminate.
+ set (p9 := total_if Compopts.optim_move_loop_invariants FirstNop.transf_program p8ter) in *.
+ set (p9bis := Renumber.transf_program p9) in *.
+ destruct (partial_if optim_duplicate Duplicate.transf_program p9bis) as [p10|e] eqn:P10; simpl 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; simpl 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; simpl 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; simpl in T; try discriminate.
set (p13quater := total_if optim_forward_moves ForwardMoves.transf_program p13ter) in *.
@@ -345,10 +361,13 @@ Proof.
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 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 total_if_match. apply Constpropproof.transf_program_match.
- exists p12; split. apply total_if_match. apply Renumberproof.transf_program_match.
+ 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.
@@ -413,7 +432,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 p28)).
+ assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p31)).
{
eapply compose_forward_simulations.
eapply SimplExprproof.transl_program_correct; eassumption.
@@ -435,11 +454,16 @@ Ltac DestructM :=
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 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 match_if_simulation. eassumption. exact Constpropproof.transf_program_correct.
+ 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.
diff --git a/driver/Compopts.v b/driver/Compopts.v
index 1e10009d..58ac62b7 100644
--- a/driver/Compopts.v
+++ b/driver/Compopts.v
@@ -48,6 +48,9 @@ Parameter optim_CSE3: unit -> bool.
(** Flag -fcse3-alias-analysis. For DMonniaux's common subexpression elimination. *)
Parameter optim_CSE3_alias_analysis: unit -> bool.
+(** Flag -fmove-loop-invariants. *)
+Parameter optim_move_loop_invariants: unit -> bool.
+
(** Flag -fredundancy. For dead code elimination. *)
Parameter optim_redundancy: unit -> bool.
@@ -66,6 +69,9 @@ Parameter optim_xsaddr: unit -> bool.
(** FIXME TEMPORARY Flag -fcoaelesce-mem. Fuse (default true) *)
Parameter optim_coalesce_mem: unit -> bool.
+(* FIXME TEMPORARY Flag -faddx. Fuse (default true) *)
+Parameter optim_madd: unit -> bool.
+
(** FIXME TEMPORARY Flag -faddx. Fuse (default false) *)
Parameter optim_addx: unit -> bool.
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 72715e65..3fae2a7d 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -199,6 +199,7 @@ Processing options:
-fcse2 Perform inter-loop common subexpression elimination [off]
-fcse3 Perform inter-loop common subexpression elimination [on]
-fcse3-alias-analysis Perform inter-loop common subexpression elimination with alias analysis [on]
+ -fmove-loop-invariants Perform loop-invariant code motion [off]
-fredundancy Perform redundancy elimination [on]
-fpostpass Perform postpass scheduling (only for K1 architecture) [on]
-fpostpass= <optim> Perform postpass scheduling with the specified optimization [list]
@@ -405,6 +406,7 @@ let cmdline_actions =
@ f_opt "cse2" option_fcse2
@ f_opt "cse3" option_fcse3
@ f_opt "cse3-alias-analysis" option_fcse3_alias_analysis
+ @ f_opt "move-loop-invariants" option_fmove_loop_invariants
@ f_opt "redundancy" option_fredundancy
@ f_opt "postpass" option_fpostpass
@ [ Exact "-fduplicate", Integer (fun n -> option_fduplicate := n) ]
@@ -417,6 +419,8 @@ let cmdline_actions =
@ f_opt "globaladdroffset" option_fglobaladdroffset
@ f_opt "xsaddr" option_fxsaddr
@ 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