Branching stub scheduler

1 files changed, 11 insertions, 5 deletions

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.
@@ -442,6 +446,8 @@ Ltac DestructM :=
   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.
     eapply Allocproof.transf_program_correct; eassumption.