Factorize as suggested for call/tailcall

1 files changed, 43 insertions, 43 deletions

diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v
index da65d6ac..67a01c20 100644
--- a/scheduling/BTLtoRTLproof.v
+++ b/scheduling/BTLtoRTLproof.v
@@ -106,6 +106,22 @@ Proof.
   intros. inv H0. inv H. inv STACKS. constructor.
 Qed.
 
+Lemma find_function_preserved ri rs0 fd
+  (FIND : find_function ge ri rs0 = Some fd)
+  : exists fd', RTL.find_function tge ri rs0 = Some fd'
+                /\ transf_fundef fd = OK fd'.
+Proof.
+  pose symbols_preserved as SYMPRES.
+  destruct ri.
+  + simpl in FIND; apply functions_translated in FIND.
+    destruct FIND as (tf & cunit & TFUN & GFIND & LO).
+    eexists; split. eauto. assumption.
+  + simpl in FIND. destruct (Genv.find_symbol _ _) eqn:GFS; try discriminate.
+    apply function_ptr_translated in FIND. destruct FIND as (tf & GFF & TF).
+    eexists; split. simpl. rewrite symbols_preserved.
+    rewrite GFS. eassumption. assumption.
+Qed.
+
 (* Inspired from Duplicateproof.v *)
 Lemma list_nth_z_dupmap:
   forall dupmap ln ln' (pc pc': node) val,
@@ -153,17 +169,16 @@ Local Hint Constructors RTL.step match_states: core.
 Local Hint Resolve css_refl plus_one transf_fundef_correct: core.
 
 Lemma iblock_istep_simulation sp dupmap stack' f' rs0 m0 ib rs1 m1 ofin
- (IBIS: iblock_istep ge sp rs0 m0 ib rs1 m1 ofin):
- forall pc0 opc isfst
- (MIB: match_iblock dupmap (RTL.fn_code f') isfst pc0 ib opc)
- ,
-  match ofin with 
-  | None => exists pc1,(opc = Some pc1) /\ plus RTL.step tge (RTL.State stack' f' sp pc0 rs0 m0) E0 (RTL.State stack' f' sp pc1 rs1 m1)
-  | Some fin =>
-     (* XXX A CHANGER ? *)
-     exists isfst' pc1, match_iblock dupmap (RTL.fn_code f') isfst' pc1 fin None
-                /\ cond_star_step (isfst = isfst') (RTL.State stack' f' sp pc0 rs0 m0) E0 (RTL.State stack' f' sp pc1 rs1 m1)
-  end.
+  (IBIS: iblock_istep ge sp rs0 m0 ib rs1 m1 ofin):
+  forall pc0 opc isfst
+  (MIB: match_iblock dupmap (RTL.fn_code f') isfst pc0 ib opc),
+   match ofin with 
+   | None => exists pc1,(opc = Some pc1) /\ plus RTL.step tge (RTL.State stack' f' sp pc0 rs0 m0) E0 (RTL.State stack' f' sp pc1 rs1 m1)
+   | Some fin =>
+      (* XXX A CHANGER ? *)
+      exists isfst' pc1, match_iblock dupmap (RTL.fn_code f') isfst' pc1 fin None
+                 /\ cond_star_step (isfst = isfst') (RTL.State stack' f' sp pc0 rs0 m0) E0 (RTL.State stack' f' sp pc1 rs1 m1)
+   end.
 Proof.
   induction IBIS; simpl; intros.
   - (* exec_final *)
@@ -245,35 +260,20 @@ Proof.
     erewrite <- preserv_fnstacksize; eauto.
     econstructor; eauto.
   - (* call *)
-    pose symbols_preserved as SYMPRES.
     rename H7 into FIND.
-    destruct ri.
-    + simpl in FIND; apply functions_translated in FIND.
-      destruct FIND as (tf & cunit & TFUN & GFIND & LO).
-      eexists; split. eapply exec_Icall; eauto.
-      apply function_sig_translated. assumption.
-      repeat (econstructor; eauto).
-    + simpl in FIND. destruct (Genv.find_symbol _ _) eqn:GFS; try discriminate.
-      apply function_ptr_translated in FIND. destruct FIND as (tf & GFF & TF).
-      eexists; split. eapply exec_Icall; eauto. simpl. rewrite symbols_preserved.
-      rewrite GFS. eassumption. apply function_sig_translated. assumption.
-      repeat (econstructor; eauto).
+    exploit find_function_preserved; eauto.
+    intros (fd' & FIND' & TRANSFU).
+    eexists; split. eapply exec_Icall; eauto.
+    apply function_sig_translated. assumption.
+    repeat (econstructor; eauto).
   - (* tailcall *)
-    pose symbols_preserved as SYMPRES.
     rename H2 into FIND.
-    destruct ri.
-    + simpl in FIND; apply functions_translated in FIND.
-      destruct FIND as (tf & cunit & TFUN & GFIND & LO).
-      eexists; split. eapply exec_Itailcall; eauto.
-      apply function_sig_translated. assumption.
-      erewrite <- preserv_fnstacksize; eauto.
-      repeat (econstructor; eauto).
-    + simpl in FIND. destruct (Genv.find_symbol _ _) eqn:GFS; try discriminate.
-      apply function_ptr_translated in FIND. destruct FIND as (tf & GFF & TF).
-      eexists; split. eapply exec_Itailcall; eauto. simpl. rewrite symbols_preserved.
-      rewrite GFS. eassumption. apply function_sig_translated. assumption.
-      erewrite <- preserv_fnstacksize; eauto.
-      repeat (econstructor; eauto).
+    exploit find_function_preserved; eauto.
+    intros (fd' & FIND' & TRANSFU).
+    eexists; split. eapply exec_Itailcall; eauto.
+    apply function_sig_translated. assumption.
+    erewrite <- preserv_fnstacksize; eauto.
+    repeat (econstructor; eauto).
   - (* builtin *)
     pose symbols_preserved as SYMPRES.
     eexists. split.
@@ -289,12 +289,12 @@ Proof.
 Qed.
 
 Lemma iblock_step_simulation sp dupmap stack stack' f f' ib rs0 m0 rs1 m1 pc0 fin t s
- (STACKS: list_forall2 match_stackframes stack stack')
- (TRANSF: match_function dupmap f f')
- (IBIS: iblock_istep ge sp rs0 m0 ib rs1 m1 (Some fin))
- (MIB : match_iblock dupmap (RTL.fn_code f') true pc0 ib None)
- (FS : final_step ge stack f sp rs1 m1 fin t s)
- :exists s', plus RTL.step tge (RTL.State stack' f' sp pc0 rs0 m0) t s' /\ match_states s s'.
+  (STACKS: list_forall2 match_stackframes stack stack')
+  (TRANSF: match_function dupmap f f')
+  (IBIS: iblock_istep ge sp rs0 m0 ib rs1 m1 (Some fin))
+  (MIB : match_iblock dupmap (RTL.fn_code f') true pc0 ib None)
+  (FS : final_step ge stack f sp rs1 m1 fin t s)
+  : exists s', plus RTL.step tge (RTL.State stack' f' sp pc0 rs0 m0) t s' /\ match_states s s'.
 Proof.
   intros; exploit iblock_istep_simulation; eauto.
   simpl. intros (isfst' & pc1 & MI & STAR). clear IBIS MIB.