From fa16ab84c204bdc9470c979c3a27fc45cfb012ba Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 4 May 2021 17:31:54 +0200 Subject: some advance and simplifications --- scheduling/BTLtoRTLproof.v | 138 +++++++++++++++++++++++---------------------- 1 file changed, 71 insertions(+), 67 deletions(-) (limited to 'scheduling/BTLtoRTLproof.v') diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v index 8dad43c7..f23bfcf8 100644 --- a/scheduling/BTLtoRTLproof.v +++ b/scheduling/BTLtoRTLproof.v @@ -106,6 +106,25 @@ Proof. intros. inv H0. inv H. inv STACKS. constructor. Qed. +(* TODO copied from Duplicateproof.v *) +(*Lemma list_nth_z_dupmap: + forall dupmap ln ln' (pc pc': node) val, + list_nth_z ln val = Some pc' -> + list_forall2 (fun n n' => dupmap!n' = Some n) ln ln' -> + exists pc', + list_nth_z ln' val = Some pc' + /\ dupmap!pc' = Some pc. +Proof. +Admitted. + induction ln; intros until val; intros LNZ LFA. + - inv LNZ. + - inv LNZ. destruct (zeq val 0) eqn:ZEQ. + + inv H0. destruct ln'; inv LFA. + simpl. exists p. split; auto. + + inv LFA. simpl. rewrite ZEQ. exploit IHln. 2: eapply H0. all: eauto. + intros (pc'1 & LNZ & REV). exists pc'1. split; auto. congruence. + Qed.*) + (* FIXME: unused ? Definition is_goto (i: final): option exit := match i with @@ -131,9 +150,8 @@ Proof. eapply plus_trans; eauto. Qed. - Local Hint Constructors RTL.step match_states: core. -Local Hint Resolve css_refl plus_one: 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): @@ -143,33 +161,37 @@ Lemma iblock_istep_simulation sp dupmap stack' f' rs0 m0 ib rs1 m1 ofin 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 => - (* A CHANGER ? *) + (* 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. - - assert (X: opc = None). { inv MIB; auto. } + - (* exec_final *) + assert (X: opc = None). { inv MIB; auto. } subst. repeat eexists; eauto. - (* eapply css_refl; auto. *) - - inv MIB. exists pc'; split; eauto. - (* apply plus_one; eauto. apply exec_Inop; trivial. *) - - inv MIB. exists pc'; split; auto. + - (* exec_nop *) + inv MIB. exists pc'; split; eauto. + - (* exec_op *) + inv MIB. exists pc'; split; auto. apply plus_one. eapply exec_Iop; eauto. erewrite <- eval_operation_preserved; eauto. intros; rewrite symbols_preserved; trivial. - - inv MIB. exists pc'; split; auto. + - (* exec_load *) + inv MIB. exists pc'; split; auto. apply plus_one. eapply exec_Iload; eauto. erewrite <- eval_addressing_preserved; eauto. intros; rewrite symbols_preserved; trivial. - - inv MIB. exists pc'; split; auto. + - (* exec_store *) + inv MIB. exists pc'; split; auto. apply plus_one. eapply exec_Istore; eauto. erewrite <- eval_addressing_preserved; eauto. intros; rewrite symbols_preserved; trivial. - - inv MIB; eauto. - (* exploit IHIBIS; eauto. *) - - inv MIB. + - (* exec_seq_stop *) + inv MIB; eauto. + - (* exec_seq_continue *) + inv MIB. exploit IHIBIS1; eauto. intros (pc1 & EQpc1 & STEP1); inv EQpc1. exploit IHIBIS2; eauto. @@ -180,7 +202,8 @@ Proof. + intros (pc2 & EQpc2 & STEP2); inv EQpc2. eexists; split; auto. eapply plus_trans; eauto. - - inv MIB. + - (* exec_cond *) + inv MIB. assert (JOIN: is_join_opt opc1 opc2 opc). { exact H10. } clear H10. destruct b; exploit IHIBIS; eauto. + (* taking ifso *) @@ -189,34 +212,25 @@ Proof. intros (isfst' & pc1 & MI & STAR). repeat eexists; eauto. eapply css_plus_trans; eauto. - (* eapply plus_one. eapply exec_Icond; eauto. - eauto. *) * (* ofin is None *) intros (pc1 & OPC & PLUS). inv OPC. inv JOIN; eexists; split; eauto. all: eapply plus_trans; eauto. - (* - [ eapply plus_one; eapply exec_Icond; eauto - | eauto | eauto ].*) + (* taking ifnot *) destruct ofin; simpl. * (* ofin is Some final *) intros (isfst' & pc1 & MI & STAR). repeat eexists; eauto. eapply css_plus_trans; eauto. - (* eapply plus_one. eapply exec_Icond; eauto. - eauto. *) * (* ofin is None *) intros (pc1 & OPC & PLUS). subst. inv JOIN; eexists; split; eauto. all: eapply plus_trans; eauto. -(* - [ eapply plus_one; eapply exec_Icond; eauto - | eauto | eauto ]. *) Qed. +(* TODO move above *) Lemma css_star P s0 s1 t: cond_star_step P s0 t s1 -> star RTL.step tge s0 t s1. @@ -226,19 +240,35 @@ Proof. - eapply plus_star; eauto. Qed. -Lemma final_simu_except_goto sp dupmap stack stack' f f' rs0 m0 rs1 m1 pc0 fin t s +Lemma final_simu_except_goto sp dupmap stack stack' f f' rs1 m1 pc1 fin t s (STACKS : list_forall2 match_stackframes stack stack') (TRANSF : match_function dupmap f f') (FS : final_step ge stack f sp rs1 m1 fin t s) - (pc1 : node) - (STAR : star RTL.step tge (RTL.State stack' f' sp pc0 rs0 m0) E0 - (RTL.State stack' f' sp pc1 rs1 m1)) (i : instruction) (ATpc1 : (RTL.fn_code f') ! pc1 = Some i) (MF : match_final_inst dupmap fin i) - : exists s', plus RTL.step tge (RTL.State stack' f' sp pc0 rs0 m0) t s' /\ match_states s s'. + : exists s', RTL.step tge (RTL.State stack' f' sp pc1 rs1 m1) t s' /\ match_states s s'. Proof. inv MF; inv FS. + - (* return *) + eexists; split. + eapply exec_Ireturn; eauto. + 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). Admitted. Lemma iblock_step_simulation sp dupmap stack stack' f f' ib rs0 m0 rs1 m1 pc0 fin t s @@ -254,7 +284,11 @@ Proof. inv MI. - (* final inst except goto *) exploit final_simu_except_goto; eauto. - eapply css_star; eauto. + intros (s' & STEP & MS). eexists; split. + + eapply plus_right. + eapply css_star; eauto. + eapply STEP. econstructor. + + eapply MS. - (* goto *) inv FS. inv STAR; try congruence. @@ -262,6 +296,8 @@ Proof. econstructor; eauto. Qed. +(* BROUILLON + Lemma iblock_step_simulation_draft 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') @@ -279,49 +315,17 @@ Proof. eexists; split. eauto. econstructor; eauto. - - inv MI. - inv STAR. - + inv H5. eexists; split. - eapply plus_one. eapply exec_Ireturn; eauto. - erewrite <- preserv_fnstacksize; eauto. - econstructor; eauto. - + inv H5. eexists; split. - eapply plus_trans. eauto. - eapply plus_one. eapply exec_Ireturn; eauto. - erewrite <- preserv_fnstacksize; eauto. eauto. - econstructor; eauto. - - inv MI. - inv STAR. - + inv H5. - pose symbols_preserved as SYMPRES. - destruct ros. - * simpl in H. apply functions_translated in H. - destruct H as (tf & cunit & TFUN & GFIND & LO). - eexists; split. - eapply plus_one. eapply exec_Icall; eauto. - apply function_sig_translated. assumption. - admit. - (* TODO ?? *) - * admit. - + admit. - - admit. - inv MI. pose symbols_preserved as SYMPRES. inv STAR. + inv H5. eexists; split. - eapply plus_one. eapply exec_Ibuiltin; eauto. - eapply eval_builtin_args_preserved; eauto. - eapply external_call_symbols_preserved; eauto. eapply senv_preserved. - econstructor; eauto. - + inv H5. eexists; split. - eapply plus_trans. eauto. - eapply plus_one. eapply exec_Ibuiltin; eauto. - eapply eval_builtin_args_preserved; eauto. - eapply external_call_symbols_preserved; eauto. eapply senv_preserved. - eauto. econstructor; eauto. + eapply plus_one. eapply exec_Ijumptable; eauto. + exploit list_nth_z_dupmap; eauto. intros (pc'1 & LNZ & REVM). + eexists. split. + + eapply exec_Ijumptable; eauto. + + econstructor; eauto. - admit. Admitted. -(* BROUILLON Inductive iblock_istep_gen sp dupmap stack f pc0 cfg ib: trace -> bool -> option final -> option node -> Prop := | ibis_synced opc pc1 -- cgit