diff options
| author | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2021-08-16 09:10:38 +0200 |
|---|---|---|
| committer | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2021-08-16 09:10:38 +0200 |
| commit | 6c90b08a1451e212d48f96d2fdd23c0c85f40bab (patch) | |
| tree | 4521af8c16d6269263f7e447fa9fa140ec47bd3e | |
| parent | b807e528c9fe45c15ddb4c87b44099a1aac6b768 (diff) | |
| download | compcert-kvx-6c90b08a1451e212d48f96d2fdd23c0c85f40bab.tar.gz compcert-kvx-6c90b08a1451e212d48f96d2fdd23c0c85f40bab.zip | |
Experimenting with compiler passes
| -rw-r--r-- | driver/Compiler.vexpand | 11 | ||||
| -rw-r--r-- | tools/compiler_expand.ml | 8 |
2 files changed, 19 insertions, 0 deletions
diff --git a/driver/Compiler.vexpand b/driver/Compiler.vexpand index 3b2f269c..a32900b5 100644 --- a/driver/Compiler.vexpand +++ b/driver/Compiler.vexpand @@ -332,6 +332,17 @@ EXPAND_RTL_FORWARD_SIMULATIONS eapply RTLpathSchedulerproof.transf_program_correct; eassumption. eapply compose_forward_simulations. eapply RTLpathproof.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 KillUselessMovesproof.transf_program_correct; eassumption. + eapply compose_forward_simulations. + eapply match_if_simulation. eassumption. eapply ForwardMovesproof.transf_program_correct; eassumption. + + eapply compose_forward_simulations. eapply Allocationproof.transf_program_correct; eassumption. eapply compose_forward_simulations. diff --git a/tools/compiler_expand.ml b/tools/compiler_expand.ml index bd711a0b..4c33aa8a 100644 --- a/tools/compiler_expand.ml +++ b/tools/compiler_expand.ml @@ -64,6 +64,7 @@ let post_rtl_passes = 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; + (* Actual CSE3 pass *) TOTAL, Always, NoRequire, (Some "Renumbering pre CSE"), "Renumber", Noprint; PARTIAL, (Option "optim_CSE3"), Require, (Some "CSE3"), "CSE3", Noprint; @@ -74,6 +75,13 @@ let post_rtl_passes = 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))); + + TOTAL, Always, NoRequire, (Some "Renumbering pre CSE"), "Renumber", Noprint; + PARTIAL, (Option "optim_CSE3"), Require, (Some "CSE3"), "CSE3", Noprint; + TOTAL, (Option "optim_CSE3"), Require, (Some "Kill useless moves after CSE3"), "KillUselessMoves", Noprint; + TOTAL, (Option "optim_forward_moves"), Require, (Some "Forwarding moves"), "ForwardMoves", Noprint; + (* PARTIAL, (Option "optim_redundancy"), Require, (Some "Redundancy elimination"), "Deadcode", Noprint; *) + PARTIAL, Always, Require, (Some "Register allocation"), "Allocation", (Print "LTL 1"); PARTIAL, Always, Require, (Some "Branch tunneling"), "Tunneling", (Print "LTL 2"); PARTIAL, Always, Require, (Some "CFG linearization"), "Linearize", Noprint; |