From 2ee7552c01a9e42754f9e3c99881b9399958cdda Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Tue, 16 Aug 2011 11:52:56 +0000
Subject: 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
---
 driver/Compiler.v | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'driver/Compiler.v')

diff --git a/driver/Compiler.v b/driver/Compiler.v
index 37a187ee..abd38678 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. 
-- 
cgit