aboutsummaryrefslogtreecommitdiffstats
path: root/driver
diff options
context:
space:
mode:
authorCyril SIX <cyril.six@kalray.eu>2020-05-20 17:57:54 +0200
committerCyril SIX <cyril.six@kalray.eu>2020-05-20 17:57:54 +0200
commit9e1268915a43c9668b0e6dda5426ba47d6b4870b (patch)
tree50e2fe14bf543af0369a58013d61b4b474927961 /driver
parenta0db2354c891c6f27015bd7b05054b33223b41c1 (diff)
downloadcompcert-kvx-9e1268915a43c9668b0e6dda5426ba47d6b4870b.tar.gz
compcert-kvx-9e1268915a43c9668b0e6dda5426ba47d6b4870b.zip
RTL -> RTLpath -> RTL
Diffstat (limited to 'driver')
-rw-r--r--driver/Compiler.v18
1 files changed, 16 insertions, 2 deletions
diff --git a/driver/Compiler.v b/driver/Compiler.v
index 499feff2..37bb54f7 100644
--- a/driver/Compiler.v
+++ b/driver/Compiler.v
@@ -39,6 +39,7 @@ Require Tailcall.
Require Inlining.
Require Renumber.
Require Duplicate.
+Require RTLpath RTLpathLivegen.
Require Constprop.
Require CSE.
Require ForwardMoves.
@@ -152,6 +153,9 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program :=
@@ print (print_RTL 11)
@@@ time "Unused globals" Unusedglob.transform_program
@@ print (print_RTL 12)
+ @@@ time "RTLpath generation" RTLpathLivegen.transf_program
+ @@ time "RTL projection" RTLpath.program_RTL
+ @@ print (print_RTL 13)
@@@ time "Register allocation" Allocation.transf_program
@@ print print_LTL
@@ time "Branch tunneling" Tunneling.tunnel_program
@@ -263,6 +267,8 @@ Definition CompCert's_passes :=
::: mkpass (match_if Compopts.optim_redundancy Deadcodeproof.match_prog)
::: mkpass (match_if Compopts.all_loads_nontrap Allnontrapproof.match_prog)
::: mkpass Unusedglobproof.match_prog
+ ::: mkpass RTLpathLivegen.match_prog
+ ::: mkpass RTLpath.match_program_RTL
::: mkpass Allocproof.match_prog
::: mkpass Tunnelingproof.match_prog
::: mkpass Linearizeproof.match_prog
@@ -310,7 +316,9 @@ Proof.
destruct (partial_if optim_redundancy Deadcode.transf_program p13ter) as [p14|e] eqn:P14; simpl 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; simpl in T; try discriminate.
- destruct (Allocation.transf_program p15) as [p16|e] eqn:P16; simpl in T; try discriminate.
+ destruct (RTLpathLivegen.transf_program p15) as [p15_1|e] eqn:P15_1; simpl in T; try discriminate.
+ set (p15_2 := RTLpath.program_RTL p15_1) in *.
+ destruct (Allocation.transf_program p15_2) as [p16|e] eqn:P16; simpl in T; try discriminate.
set (p17 := Tunneling.tunnel_program p16) in *.
destruct (Linearize.transf_program p17) as [p18|e] eqn:P18; simpl in T; try discriminate.
set (p19 := CleanupLabels.transf_program p18) in *.
@@ -335,6 +343,8 @@ Proof.
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 p15_1; split. apply RTLpathLivegen.transf_program_match; auto.
+ exists p15_2; split. apply RTLpath.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.
@@ -392,7 +402,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 p27)).
{
eapply compose_forward_simulations.
eapply SimplExprproof.transl_program_correct; eassumption.
@@ -430,6 +440,10 @@ Ltac DestructM :=
eapply compose_forward_simulations.
eapply Unusedglobproof.transf_program_correct; eassumption.
eapply compose_forward_simulations.
+ eapply RTLpathLivegen.transf_program_correct; eassumption.
+ eapply compose_forward_simulations.
+ eapply RTLpath.transf_program_correct; eassumption.
+ eapply compose_forward_simulations.
eapply Allocproof.transf_program_correct; eassumption.
eapply compose_forward_simulations.
eapply Tunnelingproof.transf_program_correct; eassumption.