diff options
| -rw-r--r-- | driver/Compiler.vexpand | 21 | ||||
| -rw-r--r-- | tools/compiler_expand.ml | 16 |
2 files changed, 37 insertions, 0 deletions
diff --git a/driver/Compiler.vexpand b/driver/Compiler.vexpand index 952bed22..74f3a97b 100644 --- a/driver/Compiler.vexpand +++ b/driver/Compiler.vexpand @@ -302,6 +302,27 @@ EXPAND_RTL_FORWARD_SIMULATIONS pose proof RTLpathLivegenproof.all_fundef_liveness_ok as X. refine (modusponens _ _ (X _ _ _) _); eauto. intro. eapply compose_forward_simulations. + eapply MyRTLpathSchedulerproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply RTLpathproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply Liftifproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply Renumberproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. eapply CSE3proof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. eapply Deadcodeproof.transf_program_correct; eassumption. + + eapply compose_forward_simulations. + eapply RTLTunnelingproof.transf_program_correct; eassumption. + + eapply compose_forward_simulations. + eapply RTLpathLivegenproof.transf_program_correct; eassumption. + pose proof RTLpathLivegenproof.all_fundef_liveness_ok as X'. + refine (modusponens _ _ (X' _ _ _) _); eauto. intro. + + eapply compose_forward_simulations. eapply RTLpathSchedulerproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply RTLpathproof.transf_program_correct; eassumption. diff --git a/tools/compiler_expand.ml b/tools/compiler_expand.ml index e45f0617..9fbc2924 100644 --- a/tools/compiler_expand.ml +++ b/tools/compiler_expand.ml @@ -55,6 +55,22 @@ PARTIAL, Always, Require, (Some "Unused globals"), "Unusedglob"; let post_rtl_passes = [| PARTIAL, Always, Require, (Some "RTLpath generation"), "RTLpathLivegen", Noprint; + PARTIAL, Always, Require, (Some "Limited register renaming and/or preparing code motion past side exits."), "MyRTLpathScheduler", Noprint; + TOTAL, Always, Require, (Some "Projection to RTL"), "RTLpath", (Print (Printf.sprintf "RTL %d" ((Array.length rtl_passes) + 1))); + (* Is renumbering necessary and/or helpful here? *) + (* TOTAL, Always, NoRequire, (Some "Renumbering pre tail duplication"), "Renumber"; *) + PARTIAL, Always, NoRequire, (Some "TODO lift if"), "Liftif", Noprint; + + TOTAL, Always, NoRequire, (Some "Renumbering pre CSE"), "Renumber", Noprint; + (* Due to hackery this pass of CSE3 only removes redundant conditions *) + PARTIAL, (Option "optim_CSE3"), Require, (Some "CSE3"), "CSE3", Noprint; + (* This is meant to clean up dead code afer "if-lifting" + removing of redundant condition *) + PARTIAL, (Option "optim_redundancy"), Require, (Some "Redundancy elimination"), "Deadcode", Noprint; + + PARTIAL, Always, Require, (Some "RTL Branch Tunneling"), "RTLTunneling", Noprint; + + + PARTIAL, Always, Require, (Some "RTLpath generation"), "RTLpathLivegen", Noprint; PARTIAL, Always, Require, (Some "Prepass scheduling"), "RTLpathScheduler", Noprint; TOTAL, Always, Require, (Some "Projection to RTL"), "RTLpath", (Print (Printf.sprintf "RTL %d" ((Array.length rtl_passes) + 1))); PARTIAL, Always, Require, (Some "Register allocation"), "Allocation", (Print "LTL 1"); |