finishing RTLtoBTL

1 files changed, 34 insertions, 23 deletions

diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v
index faf0b76c..633e1b8e 100644
--- a/scheduling/RTLtoBTLproof.v
+++ b/scheduling/RTLtoBTLproof.v
@@ -9,7 +9,6 @@ Require Import Linking.
 Record match_function dupmap (f:RTL.function) (tf: BTL.function): Prop := {
   dupmap_correct: match_cfg dupmap (fn_code tf) (RTL.fn_code f);
   dupmap_entrypoint: dupmap!(fn_entrypoint tf) = Some (RTL.fn_entrypoint f);
-  code_expand: forall pc ib, (fn_code tf)!pc=Some ib -> is_expand ib.(entry);
   preserv_fnsig: fn_sig tf = RTL.fn_sig f;
   preserv_fnparams: fn_params tf = RTL.fn_params f;
   preserv_fnstacksize: fn_stacksize tf = RTL.fn_stacksize f
@@ -31,7 +30,6 @@ Lemma verify_function_correct dupmap f f' tt:
   fn_sig f' = RTL.fn_sig f ->
   fn_params f' = RTL.fn_params f ->
   fn_stacksize f' = RTL.fn_stacksize f ->
-  (forall pc ib, (fn_code f')!pc=Some ib -> is_expand ib.(entry)) ->
   match_function dupmap f f'.
 Proof.
   unfold verify_function; intro VERIF. monadInv VERIF.
@@ -46,7 +44,6 @@ Proof.
   unfold transf_function; unfold bind. repeat autodestruct.
   intros H _ _ X. inversion X; subst; clear X.
   eexists; eapply verify_function_correct; simpl; eauto.
-  eapply expand_code_correct; eauto.
 Qed.
 
 Lemma transf_fundef_correct f f':
@@ -243,6 +240,18 @@ Proof.
   destruct fi; trivial. inv H. inv H4.
 Qed.
 
+Lemma expand_entry_isnt_goto dupmap f pc ib:
+  match_iblock dupmap (RTL.fn_code f) true pc (expand (entry ib) None) None ->
+  is_goto (expand (entry ib) None) = false.
+Proof.
+  destruct (is_goto (expand (entry ib) None))eqn:EQG.
+  - destruct (expand (entry ib) None);
+    try destruct fi; try discriminate; trivial.
+    intros; inv H; inv H4.
+  - destruct (expand (entry ib) None);
+    try destruct fi; try discriminate; trivial.
+Qed.
+
 Lemma list_nth_z_rev_dupmap:
   forall dupmap ln ln' (pc pc': node) val,
   list_nth_z ln val = Some pc ->
@@ -498,10 +507,10 @@ Proof.
     eexists; left; eexists; split.
     + repeat econstructor; eauto.
       apply iblock_istep_run_equiv in BTL_RUN; eauto.
-    + econstructor. econstructor; eauto.
-      eapply code_expand; eauto.
-      econstructor.
-      eapply entry_isnt_goto; eauto.
+    + econstructor; apply expand_matchiblock_correct in MI.
+      econstructor; eauto. apply expand_correct; trivial.
+      econstructor. apply expand_preserves_iblock_istep_run.
+      eapply expand_entry_isnt_goto; eauto.
   - (* Others *)
     exists (Some ib2); right; split.
     simpl; auto.
@@ -566,11 +575,10 @@ Proof.
         pose symbols_preserved as SYMPRES.
         eapply eval_builtin_args_preserved; eauto.
         eapply external_call_symbols_preserved; eauto. eapply senv_preserved.
-      * econstructor; eauto.
-        { econstructor; eauto. eapply code_expand; eauto.  
-          apply star_refl. }
-        inversion MI; subst; try_simplify_someHyps.
-        inv H3; try_simplify_someHyps.
+      * econstructor; eauto; apply expand_matchiblock_correct in MI.
+        { econstructor; eauto. apply expand_correct; trivial.  
+          apply star_refl. apply expand_preserves_iblock_istep_run. }
+        eapply expand_entry_isnt_goto; eauto.
     + (* Bjumptable *)
       exploit list_nth_z_rev_dupmap; eauto.
       intros (pc'0 & LNZ & DM).
@@ -582,11 +590,10 @@ Proof.
         eexists; eexists; split.
         eapply iblock_istep_run_equiv in BTL_RUN.
         eapply BTL_RUN. econstructor; eauto.
-      * econstructor; eauto.
-        { econstructor; eauto. eapply code_expand; eauto.  
-          apply star_refl. }
-        inversion MI; subst; try_simplify_someHyps.
-        inv H4; try_simplify_someHyps.
+      * econstructor; eauto; apply expand_matchiblock_correct in MI.
+        { econstructor; eauto. apply expand_correct; trivial.  
+          apply star_refl. apply expand_preserves_iblock_istep_run. }
+        eapply expand_entry_isnt_goto; eauto.
   - (* mib_exit *)
     discriminate.
   - (* mib_seq *)
@@ -689,11 +696,13 @@ Proof.
       eexists; left; eexists; split.
       * eapply exec_function_internal.
         erewrite preserv_fnstacksize; eauto.
-      * econstructor. econstructor; eauto.
-        eapply code_expand; eauto.
-        3: eapply entry_isnt_goto; eauto.
+      * apply expand_matchiblock_correct in MI.
+        econstructor. econstructor; eauto.
+        apply expand_correct; trivial.
+        3: eapply expand_entry_isnt_goto; eauto.
         all: erewrite preserv_fnparams; eauto.
         constructor.
+        apply expand_preserves_iblock_istep_run.
     + (* External function *)
       inv TRANSF.
       eexists; left; eexists; split.
@@ -708,9 +717,11 @@ Proof.
     apply DMC in DUPLIC as [ib [FNC MI]]; clear DMC.
     eexists; left; eexists; split.
     + eapply exec_return.
-    + econstructor. econstructor; eauto.
-      eapply code_expand; eauto.
-      constructor. eapply entry_isnt_goto; eauto.
+    + apply expand_matchiblock_correct in MI.
+      econstructor. econstructor; eauto.
+      apply expand_correct; trivial.
+      constructor. apply expand_preserves_iblock_istep_run.
+      eapply expand_entry_isnt_goto; eauto.
 Qed.
 
 Local Hint Resolve plus_one star_refl: core.