From bf2ed66aa8c87b95c1d57cdd7f22dc131c7728cf Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 4 May 2021 23:08:53 +0200 Subject: Factorize as suggested for call/tailcall --- scheduling/BTLtoRTLproof.v | 86 +++++++++++++++++++++++----------------------- 1 file changed, 43 insertions(+), 43 deletions(-) (limited to 'scheduling/BTLtoRTLproof.v') 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. -- cgit