diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-08-16 11:52:56 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-08-16 11:52:56 +0000 |
| commit | 2ee7552c01a9e42754f9e3c99881b9399958cdda (patch) | |
| tree | e6f710b27fe556ef4d5ebbd2e60a2e23f831ab99 /driver | |
| parent | cfe40ae85583cabd33315c9432d1f60e98e0d132 (diff) | |
New backend pass "RRE": optimize (somewhat) redundant reloads introduced by the Reload pass.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1713 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'driver')
| -rw-r--r-- | driver/Compiler.v | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/driver/Compiler.v b/driver/Compiler.v index 37a187e..abd3867 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -52,6 +52,7 @@ Require Tunneling. Require Linearize. Require CleanupLabels. Require Reload. +Require RRE. Require Stacking. Require Asmgen. (** Type systems. *) @@ -80,6 +81,8 @@ Require CleanupLabelsproof. Require CleanupLabelstyping. Require Reloadproof. Require Reloadtyping. +Require RREproof. +Require RREtyping. Require Stackingproof. Require Stackingtyping. Require Asmgenproof. @@ -150,6 +153,7 @@ Definition transf_rtl_fundef (f: RTL.fundef) : res Asm.fundef := @@ CleanupLabels.transf_fundef @@ print print_LTLin @@ Reload.transf_fundef + @@ RRE.transf_fundef @@@ Stacking.transf_fundef @@ print print_Mach @@@ Asmgen.transf_fundef. @@ -327,13 +331,14 @@ Proof. unfold transf_rtl_program, transf_rtl_fundef in H. repeat TransfProgInv. repeat rewrite transform_program_print_identity in *. subst. - generalize (transform_partial_program_identity _ _ _ _ X0). intro EQ. subst. + generalize (transform_partial_program_identity _ _ _ _ X). intro EQ. subst. generalize Alloctyping.program_typing_preserved Tunnelingtyping.program_typing_preserved Linearizetyping.program_typing_preserved CleanupLabelstyping.program_typing_preserved Reloadtyping.program_typing_preserved + RREtyping.program_typing_preserved Stackingtyping.program_typing_preserved; intros. eapply compose_forward_simulation. apply Tailcallproof.transf_program_correct. @@ -345,6 +350,7 @@ Proof. eapply compose_forward_simulation. apply Linearizeproof.transf_program_correct. eassumption. eauto. eapply compose_forward_simulation. apply CleanupLabelsproof.transf_program_correct. eapply compose_forward_simulation. apply Reloadproof.transf_program_correct. eauto. + eapply compose_forward_simulation. apply RREproof.transf_program_correct. eauto. eapply compose_forward_simulation. apply Stackingproof.transf_program_correct. eassumption. eauto 8. apply Asmgenproof.transf_program_correct; eauto 10. split. auto. |