diff options
| author | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2021-09-16 20:16:24 +0200 |
|---|---|---|
| committer | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2021-09-16 20:16:24 +0200 |
| commit | 5a277ea92e49270d15bfd202098873d09c8b2546 (patch) | |
| tree | 9aca81b9a6722fecb03d02d8e460f94c9a7ab325 | |
| parent | e47c08eca32ae156c86dbf8c4801fadd9ca8ec31 (diff) | |
| download | compcert-kvx-5a277ea92e49270d15bfd202098873d09c8b2546.tar.gz compcert-kvx-5a277ea92e49270d15bfd202098873d09c8b2546.zip | |
Add RTLtunneling pass before actual prepass scheduling
This should avoid cases where scheduling turns a side-exit into a
"useless Icond" which changes the number of exits and is ruled illegal.
| -rw-r--r-- | driver/Compiler.vexpand | 3 | ||||
| -rw-r--r-- | tools/compiler_expand.ml | 3 |
2 files changed, 6 insertions, 0 deletions
diff --git a/driver/Compiler.vexpand b/driver/Compiler.vexpand index 34e85b6b..81aaf2a9 100644 --- a/driver/Compiler.vexpand +++ b/driver/Compiler.vexpand @@ -317,6 +317,9 @@ EXPAND_RTL_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. diff --git a/tools/compiler_expand.ml b/tools/compiler_expand.ml index dfadca3b..c6bb88a5 100644 --- a/tools/compiler_expand.ml +++ b/tools/compiler_expand.ml @@ -67,6 +67,9 @@ let post_rtl_passes = (* 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))); |