From d46e96ef6c0287d6892bfc7d2272b7473f5e4979 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Thu, 28 May 2020 16:36:11 +0200 Subject: Branching stub scheduler --- driver/Compiler.v | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) (limited to 'driver') diff --git a/driver/Compiler.v b/driver/Compiler.v index 37bb54f7..07889ae5 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -39,7 +39,7 @@ Require Tailcall. Require Inlining. Require Renumber. Require Duplicate. -Require RTLpath RTLpathLivegen. +Require RTLpath RTLpathLivegen RTLpathScheduler. Require Constprop. Require CSE. Require ForwardMoves. @@ -154,6 +154,7 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program := @@@ time "Unused globals" Unusedglob.transform_program @@ print (print_RTL 12) @@@ time "RTLpath generation" RTLpathLivegen.transf_program + @@@ time "RTLpath scheduling" RTLpathScheduler.transf_program @@ time "RTL projection" RTLpath.program_RTL @@ print (print_RTL 13) @@@ time "Register allocation" Allocation.transf_program @@ -268,6 +269,7 @@ Definition CompCert's_passes := ::: mkpass (match_if Compopts.all_loads_nontrap Allnontrapproof.match_prog) ::: mkpass Unusedglobproof.match_prog ::: mkpass RTLpathLivegen.match_prog + ::: mkpass RTLpathScheduler.match_prog ::: mkpass RTLpath.match_program_RTL ::: mkpass Allocproof.match_prog ::: mkpass Tunnelingproof.match_prog @@ -317,8 +319,9 @@ Proof. 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 (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. + destruct (RTLpathScheduler.transf_program p15_1) as [p15_2|e] eqn:P15_2; simpl in T; try discriminate. + set (p15_3 := RTLpath.program_RTL p15_2) in *. + destruct (Allocation.transf_program p15_3) 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 *. @@ -344,7 +347,8 @@ Proof. 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 p15_2; split. apply RTLpathScheduler.transf_program_match; auto. + exists p15_3; 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. @@ -402,7 +406,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 p27)). + assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p28)). { eapply compose_forward_simulations. eapply SimplExprproof.transl_program_correct; eassumption. @@ -441,6 +445,8 @@ Ltac DestructM := eapply Unusedglobproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply RTLpathLivegen.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply RTLpathScheduler.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply RTLpath.transf_program_correct; eassumption. eapply compose_forward_simulations. -- cgit