RTL -> RTLpath -> RTL

2 files changed, 86 insertions, 3 deletions

diff --git a/driver/Compiler.v b/driver/Compiler.v
index 499feff2..37bb54f7 100644
--- a/driver/Compiler.v
+++ b/driver/Compiler.v
@@ -39,6 +39,7 @@ Require Tailcall.
 Require Inlining.
 Require Renumber.
 Require Duplicate.
+Require RTLpath RTLpathLivegen.
 Require Constprop.
 Require CSE.
 Require ForwardMoves.
@@ -152,6 +153,9 @@ Definition transf_rtl_program (f: RTL.program) : res Asm.program :=
    @@ print (print_RTL 11)
   @@@ time "Unused globals" Unusedglob.transform_program
    @@ print (print_RTL 12)
+  @@@ time "RTLpath generation" RTLpathLivegen.transf_program
+   @@ time "RTL projection" RTLpath.program_RTL
+   @@ print (print_RTL 13)
   @@@ time "Register allocation" Allocation.transf_program
    @@ print print_LTL
    @@ time "Branch tunneling" Tunneling.tunnel_program
@@ -263,6 +267,8 @@ Definition CompCert's_passes :=
   ::: mkpass (match_if Compopts.optim_redundancy Deadcodeproof.match_prog)
   ::: mkpass (match_if Compopts.all_loads_nontrap Allnontrapproof.match_prog)
   ::: mkpass Unusedglobproof.match_prog
+  ::: mkpass RTLpathLivegen.match_prog
+  ::: mkpass RTLpath.match_program_RTL
   ::: mkpass Allocproof.match_prog
   ::: mkpass Tunnelingproof.match_prog
   ::: mkpass Linearizeproof.match_prog
@@ -310,7 +316,9 @@ Proof.
   destruct (partial_if optim_redundancy Deadcode.transf_program p13ter) as [p14|e] eqn:P14; simpl in T; try discriminate.
   set (p14bis := total_if all_loads_nontrap Allnontrap.transf_program p14) in *.
   destruct (Unusedglob.transform_program p14bis) as [p15|e] eqn:P15; simpl in T; try discriminate.
-  destruct (Allocation.transf_program p15) as [p16|e] eqn:P16; simpl in T; try discriminate.
+  destruct (RTLpathLivegen.transf_program p15) as [p15_1|e] eqn:P15_1; simpl in T; try discriminate.
+  set (p15_2 := RTLpath.program_RTL p15_1) in *.
+  destruct (Allocation.transf_program p15_2) as [p16|e] eqn:P16; simpl in T; try discriminate.
   set (p17 := Tunneling.tunnel_program p16) in *.
   destruct (Linearize.transf_program p17) as [p18|e] eqn:P18; simpl in T; try discriminate.
   set (p19 := CleanupLabels.transf_program p18) in *.
@@ -335,6 +343,8 @@ Proof.
   exists p14; split. eapply partial_if_match; eauto. apply Deadcodeproof.transf_program_match.
   exists p14bis; split. eapply total_if_match; eauto. apply Allnontrapproof.transf_program_match.
   exists p15; split. apply Unusedglobproof.transf_program_match; auto.
+  exists p15_1; split. apply RTLpathLivegen.transf_program_match; auto.
+  exists p15_2; split. apply RTLpath.transf_program_match; auto.
   exists p16; split. apply Allocproof.transf_program_match; auto.
   exists p17; split. apply Tunnelingproof.transf_program_match.
   exists p18; split. apply Linearizeproof.transf_program_match; auto.
@@ -392,7 +402,7 @@ Ltac DestructM :=
       destruct H as (p & M & MM); clear H
   end.
   repeat DestructM. subst tp.
-  assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p25)).
+  assert (F: forward_simulation (Cstrategy.semantics p) (Asm.semantics p27)).
   {
   eapply compose_forward_simulations.
     eapply SimplExprproof.transl_program_correct; eassumption.
@@ -430,6 +440,10 @@ Ltac DestructM :=
   eapply compose_forward_simulations.
     eapply Unusedglobproof.transf_program_correct; eassumption.
   eapply compose_forward_simulations.
+    eapply RTLpathLivegen.transf_program_correct; eassumption.
+  eapply compose_forward_simulations.
+    eapply RTLpath.transf_program_correct; eassumption.
+  eapply compose_forward_simulations.
     eapply Allocproof.transf_program_correct; eassumption.
   eapply compose_forward_simulations.
     eapply Tunnelingproof.transf_program_correct; eassumption.
diff --git a/mppa_k1c/lib/RTLpath.v b/mppa_k1c/lib/RTLpath.v
index 228bc95b..f170e0c3 100644
--- a/mppa_k1c/lib/RTLpath.v
+++ b/mppa_k1c/lib/RTLpath.v
@@ -135,6 +135,15 @@ Coercion fundef_RTL: fundef >-> RTL.fundef.
 Definition program_RTL (p: program) : RTL.program := transform_program fundef_RTL p.
 Coercion program_RTL: program >-> RTL.program.
 
+Definition match_program_RTL (p: RTLpath.program) (tp: RTL.program) :=
+  match_program (fun ctx f tf => tf = fundef_RTL f) eq p tp.
+
+Lemma transf_program_match:
+  forall p, match_program_RTL p (program_RTL p).
+Proof.
+  intros. eapply match_transform_program; eauto.
+Qed.
+
 (** * Path-step semantics of RTLpath programs *)
 
 (* Semantics of internal instructions (mimicking RTL semantics) *)
@@ -330,7 +339,6 @@ Definition final_state (st: state) (i:int): Prop
 Definition semantics (p: program) :=
   Semantics (step (Genv.globalenv (program_RTL p))) (initial_state p) final_state (Genv.globalenv p).
 
-
 (** * Proving the bisimulation between (semantics p) and (RTL.semantics p). *)
 
 (** ** Preliminaries: simple tactics for option-monad *)
@@ -516,6 +524,67 @@ Qed.
 
 End CORRECTNESS.
 
+Lemma program_equals {A B: Type} : forall (p1 p2: AST.program A B),
+  prog_defs p1 = prog_defs p2 ->
+  prog_public p1 = prog_public p2 ->
+  prog_main p1 = prog_main p2 ->
+  p1 = p2.
+Proof.
+  intros. destruct p1. destruct p2. simpl in *. subst. auto.
+Qed.
+
+Lemma cons_extract {A: Type} : forall (l: list A) a b, a = b -> a::l = b::l.
+Proof.
+  intros. congruence.
+Qed.
+
+(* Definition transf_program : RTLpath.program -> RTL.program := transform_program fundef_RTL.
+
+Lemma transf_program_proj: forall p, program_RTL (transf_program p) = p.
+Proof.
+  intros p. destruct p as [defs pub main]. unfold program_proj. simpl.
+  apply program_equals; simpl; auto.
+  induction defs.
+  - simpl; auto.
+  - simpl. rewrite IHdefs. 
+    destruct a as [id gd]; simpl.
+    destruct gd as [f|v]; simpl; auto.
+    rewrite transf_fundef_proj. auto.
+Qed. *)
+
+Lemma match_program_transf:
+  forall p tp, match_program_RTL p tp -> program_RTL p = tp.
+Proof.
+  intros p tp H. inversion_clear H. inv H1.
+  destruct p as [defs pub main]. destruct tp as [tdefs tpub tmain]. simpl in *.
+  subst. unfold program_RTL. unfold transform_program. simpl.
+  apply program_equals; simpl; auto.
+  induction H0; simpl; auto.
+  rewrite IHlist_forall2. apply cons_extract.
+  destruct a1 as [ida gda]. destruct b1 as [idb gdb].
+  simpl in *.
+  inv H. inv H2.
+  - simpl in *. subst. auto.
+  - simpl in *. subst. inv H. auto.
+Qed.
+
+
+Section PRESERVATION.
+
+Variable prog: RTLpath.program.
+Variable tprog: RTL.program.
+Hypothesis TRANSF: match_program_RTL prog tprog.
+Let ge := Genv.globalenv prog.
+Let tge := Genv.globalenv tprog.
+
+Theorem transf_program_correct:
+  forward_simulation (RTLpath.semantics prog) (RTL.semantics tprog).
+Proof.
+  pose proof (match_program_transf prog tprog TRANSF) as TR. subst.
+  eapply RTLpath_correct.
+Qed.
+
+End PRESERVATION.