starting to extend RTLtoBTL with Liveness checking (on BTL side)

1 files changed, 40 insertions, 23 deletions

diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v
index ef336de5..18ff8d5f 100644
--- a/scheduling/RTLtoBTLproof.v
+++ b/scheduling/RTLtoBTLproof.v
@@ -230,20 +230,33 @@ Qed.
 (** * Matching relation on functions *)
 
 (* we simply switch [f] and [tf] in the usual way *)
-Definition match_function dupmap (f:RTL.function) (tf: BTL.function): Prop := 
-  BTLmatchRTL.match_function dupmap tf f.
+Record match_function dupmap (f:RTL.function) (tf: BTL.function): Prop := {
+  matchRTL:> BTLmatchRTL.match_function dupmap tf f;
+  liveness_ok: liveness_ok_function tf;
+}.
 
-Definition match_fundef f tf := BTLmatchRTL.match_fundef tf f.
+Local Hint Resolve matchRTL: core.
 
-Definition match_stackframes stk stk' := BTLmatchRTL.match_stackframes stk' stk.
+Inductive match_fundef: RTL.fundef -> BTL.fundef -> Prop :=
+  | match_Internal dupmap f f': match_function dupmap f f' -> match_fundef (Internal f) (Internal f')
+  | match_External ef: match_fundef (External ef) (External ef).
+
+Inductive match_stackframes: RTL.stackframe -> BTL.stackframe -> Prop :=
+  | match_stackframe_intro 
+      dupmap res f sp pc rs f' pc'
+      (TRANSF: match_function dupmap f f')
+      (DUPLIC: dupmap!pc' = Some pc)
+      : match_stackframes (RTL.Stackframe res f sp pc rs) (BTL.Stackframe res f' sp pc' rs).
 
 Lemma transf_function_correct f f':
   transf_function f = OK f' -> exists dupmap, match_function dupmap f f'.
 Proof.
   unfold transf_function; unfold bind. repeat autodestruct.
   intros H _ _ X. inversion X; subst; clear X.
+(*
   eexists; eapply verify_function_correct; simpl; eauto.
-Qed.
+*)
+Admitted.
 
 Lemma transf_fundef_correct f f':
   transf_fundef f = OK f' -> match_fundef f f'.
@@ -362,7 +375,7 @@ Lemma function_sig_translated f tf: transf_fundef f = OK tf -> funsig tf = RTL.f
 Proof.
   intros H; apply transf_fundef_correct in H; destruct H; simpl; eauto.
   erewrite preserv_fnsig; eauto.
-Qed.
+Admitted.
 
 Lemma transf_initial_states s1:
   RTL.initial_state prog s1 ->
@@ -525,8 +538,8 @@ Proof.
   - (* Bgoto *)
     inv MSS2. inversion MIB; subst; try inv H4.
     remember H2 as ODUPLIC; clear HeqODUPLIC.
-    eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC.
-    apply DMC in H2 as [ib [FNC MI]]; clear DMC.
+    exploit dupmap_correct; eauto.
+    intros [ib [FNC MI]].
     eexists; left; eexists; split; eauto.
     repeat econstructor; eauto.
     apply iblock_istep_run_equiv in BTL_RUN; eauto.
@@ -584,9 +597,8 @@ Proof.
       * repeat (econstructor; eauto).
         eapply transf_fundef_correct; eauto.
     + (* Bbuiltin *)
-      eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC.
-      remember H1 as ODUPLIC; clear HeqODUPLIC.
-      apply DMC in H1 as [ib [FNC MI]]; clear DMC.
+      exploit dupmap_correct; eauto.
+      intros [ib [FNC MI]].
       exists (Some (normRTL (entry ib))); left; eexists; split; eauto.
       econstructor; eauto. econstructor.
       eexists; eexists; split.
@@ -598,9 +610,8 @@ Proof.
     + (* Bjumptable *)
       exploit list_nth_z_rev_dupmap; eauto.
       intros (pc'0 & LNZ & DM).
-      eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC.
-      remember DM as ODUPLIC; clear HeqODUPLIC.
-      apply DMC in DM as [ib [FNC MI]]; clear DMC.
+      exploit dupmap_correct; eauto.
+      intros [ib [FNC MI]].
       exists (Some (normRTL (entry ib))); left; eexists; split; eauto.
       econstructor; eauto. econstructor.
       eexists; eexists; split.
@@ -687,11 +698,10 @@ Proof.
     inv H.
     + (* Internal function *)
       inv TRANSF.
-      rename H1 into TRANSF.
-      eapply dupmap_entrypoint in TRANSF as ENTRY.
-      eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC.
-      apply DMC in ENTRY as DMC'.
-      destruct DMC' as [ib [CENTRY MI]]; clear DMC.
+      rename H0 into TRANSF.
+      exploit dupmap_entrypoint; eauto. intros ENTRY.
+      exploit dupmap_correct; eauto.
+      intros [ib [CENTRY MI]].
       exists (Some (normRTL (entry ib))); left; eexists; split.
       * eapply exec_function_internal.
         erewrite preserv_fnstacksize; eauto.
@@ -705,16 +715,15 @@ Proof.
       * econstructor; eauto.
   - (* Returnstate *)
     inv H. inv STACKS. inv H1.
-    eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC.
-    remember DUPLIC as ODUPLIC; clear HeqODUPLIC.
-    apply DMC in DUPLIC as [ib [FNC MI]]; clear DMC.
+    exploit dupmap_correct; eauto.
+    intros [ib [FNC MI]].
     eexists; left; eexists; split; eauto.
     eapply exec_return.
 Qed.
 
 Local Hint Resolve plus_one star_refl: core.
 
-Theorem transf_program_correct:
+Theorem transf_program_correct_cfg:
   forward_simulation (RTL.semantics prog) (BTLmatchRTL.cfgsem tprog).
 Proof.
   eapply (Forward_simulation (L1:=RTL.semantics prog) (L2:=cfgsem tprog) (ltof _ omeasure) match_states).
@@ -729,4 +738,12 @@ Proof.
   - eapply senv_preserved.
 Qed.
 
+Theorem transf_program_correct:
+  forward_simulation (RTL.semantics prog) (BTL.fsem tprog).
+Proof.
+  eapply compose_forward_simulations.
+  - eapply transf_program_correct_cfg.
+  - eapply cfgsem2fsem.
+Admitted.
+
 End BTL_SIMULATES_RTL.