From e3613e0614ccc93c1013f7c39b58cffb6c21a76c Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 10 May 2021 17:49:29 +0200 Subject: new strong_state predicate and lemma --- scheduling/RTLtoBTLproof.v | 110 +++++++++++++++++++++++++++++---------------- 1 file changed, 72 insertions(+), 38 deletions(-) (limited to 'scheduling/RTLtoBTLproof.v') diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index 1fa13242..eb4734b8 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -102,8 +102,8 @@ The simulation diagram for match_states_intro is as follows: >> *) -Inductive match_states: (option iblock) -> RTL.state -> state -> Prop := - | match_states_intro (* TODO: LES DETAILS SONT SANS DOUTE A REVOIR !!! *) +Inductive match_strong_state: (option iblock) -> RTL.state -> state -> Prop := + | match_strong_state_intro ib dupmap st f sp rs m st' f' pcB0 pcR0 pcR1 rs0 m0 isfst ib0 (STACKS: list_forall2 match_stackframes st st') (TRANSF: match_function dupmap f f') @@ -113,6 +113,14 @@ Inductive match_states: (option iblock) -> RTL.state -> state -> Prop := (IS_EXPD: is_expand ib) (RTL_RUN: star RTL.step ge (RTL.State st f sp pcR0 rs0 m0) E0 (RTL.State st f sp pcR1 rs m)) (BTL_RUN: iblock_istep_run tge sp ib0.(entry) rs0 m0 = iblock_istep_run tge sp ib rs m) + : match_strong_state (Some ib) (RTL.State st f sp pcR1 rs m) (State st' f' sp pcB0 rs0 m0) + . + +Inductive match_states: (option iblock) -> RTL.state -> state -> Prop := + | match_states_intro (* TODO: LES DETAILS SONT SANS DOUTE A REVOIR !!! *) + ib st f sp rs m st' f' pcB0 pcR1 rs0 m0 + (MSTRONG: match_strong_state (Some ib) (RTL.State st f sp pcR1 rs m) (State st' f' sp pcB0 rs0 m0)) + (NGOTO: is_goto ib = false) : match_states (Some ib) (RTL.State st f sp pcR1 rs m) (State st' f' sp pcB0 rs0 m0) | match_states_call st st' f f' args m @@ -123,7 +131,24 @@ Inductive match_states: (option iblock) -> RTL.state -> state -> Prop := st st' v m (STACKS: list_forall2 match_stackframes st st') : match_states None (RTL.Returnstate st v m) (Returnstate st' v m) - . + . + +Lemma match_strong_state_equiv sp st st' ib f f' rs m rs0 m0 pcB0 pcR1: + match_strong_state (Some ib) (RTL.State st f sp pcR1 rs m) (State st' f' sp pcB0 rs0 m0) -> + match is_goto ib with + | true => + exists ib' succ, + iblock_istep tge sp rs0 m0 (entry ib') rs m (Some (Bgoto succ)) + | false => match_states (Some ib) (RTL.State st f sp pcR1 rs m) (State st' f' sp pcB0 rs0 m0) + end. +Proof. + destruct (is_goto ib) eqn:EQ. + - intros. destruct ib; try destruct fi; try discriminate. + inv H. simpl in BTL_RUN. + rewrite <- iblock_istep_run_equiv in BTL_RUN. + repeat eexists; eauto. + - intros. econstructor; eauto. +Qed. Lemma symbols_preserved s: Genv.find_symbol tge s = Genv.find_symbol ge s. Proof. @@ -227,24 +252,34 @@ Proof. induction ib; simpl; auto; lia. Qed. +Lemma list_nth_z_rev_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': node), + list_nth_z ln' val = Some pc' + /\ dupmap!pc' = Some pc. +Proof. + 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. + Lemma opt_simu_intro - sp f f' st st' dupmap isfst pcR0 pcR1 pcB0 ib ib0 rs m rs0 m0 t s1' + sp f f' st st' pcR1 pcB0 ib rs m rs0 m0 t s1' (STEP : RTL.step ge (RTL.State st f sp pcR1 rs m) t s1') - (STACKS : list_forall2 match_stackframes st st') - (TRANSF : match_function dupmap f f') - (ATpc0 : (fn_code f') ! pcB0 = Some ib0) - (DUPLIC : dupmap ! pcB0 = Some pcR0) - (MIB : match_iblock dupmap (RTL.fn_code f) isfst pcR1 ib None) - (IS_EXPD : is_expand ib) - (RTL_RUN : star RTL.step ge (RTL.State st f sp pcR0 rs0 m0) E0 - (RTL.State st f sp pcR1 rs m)) - (BTL_RUN : iblock_istep_run tge sp (entry ib0) rs0 m0 = - iblock_istep_run tge sp ib rs m) + (MSTRONG : match_strong_state (Some ib) (RTL.State st f sp pcR1 rs m) + (State st' f' sp pcB0 rs0 m0)) + (NGOTO : is_goto ib = false) : exists (oib' : option iblock), (exists s2', step tge (State st' f' sp pcB0 rs0 m0) t s2' /\ match_states oib' s1' s2') \/ (omeasure oib' < omeasure (Some ib) /\ t=E0 /\ match_states oib' s1' (State st' f' sp pcB0 rs0 m0)). Proof. - inv MIB. + inv MSTRONG. inv MIB. - (* mib_BF *) inv H0; inversion STEP; subst; try_simplify_someHyps; intros. @@ -293,32 +328,31 @@ Proof. pose symbols_preserved as SYMPRES. eapply eval_builtin_args_preserved; eauto. eapply external_call_symbols_preserved; eauto. eapply senv_preserved. - * econstructor; eauto. eapply code_expand; eauto. - apply star_refl. + * econstructor; eauto. + { econstructor; eauto. eapply code_expand; eauto. + apply star_refl. } + inversion MI; subst; try_simplify_someHyps. + inv H3; try_simplify_someHyps. + (* Bjumptable *) - admit. - (* eexists; left; eexists; split. + 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. + eexists; left; eexists; split. * econstructor; eauto. econstructor. eexists; eexists; split. eapply iblock_istep_run_equiv in BTL_RUN. eapply BTL_RUN. econstructor; eauto. - exploit (list_nth_z_dupmap dupmap ln' ln); eauto. - * econstructor; eauto.*) + * econstructor; eauto. + { econstructor; eauto. eapply code_expand; eauto. + apply star_refl. } + inversion MI; subst; try_simplify_someHyps. + inv H4; try_simplify_someHyps. - (* mib_exit *) - (* exists None; right; repeat (split; auto). - inversion STEP; subst; try_simplify_someHyps. - eexists; left. eexists; split. - econstructor; eauto. econstructor. - eexists; eexists; split. - eapply iblock_istep_run_equiv in BTL_RUN. - eapply BTL_RUN. econstructor. econstructor; eauto. - inv BTL_RUN. - + eapply exec_iblock; eauto. - econstructor; repeat eexists. - inv STEP. - eapply exec_Bgoto.*) admit. - - (* mib_seq *) - inv H. + discriminate. + - (* mib_seq *) admit. + (* inv H. + (* Bnop *) inversion STEP; subst; try_simplify_someHyps. exists (Some b2); right; repeat (split; auto). @@ -351,8 +385,8 @@ Proof. + (* Absurd case *) inv IS_EXPD. inv H4. inv H. + (* Absurd Bcond (Bcond are not allowed in the left part of a Bseq *) - inv IS_EXPD; discriminate. - - (* mib_cond *) + inv IS_EXPD; discriminate.*) + - (* mib_cond *) admit. (* inversion STEP; subst; try_simplify_someHyps. intros; rewrite H12 in BTL_RUN. destruct b. * (* Ifso *) @@ -366,7 +400,7 @@ Proof. simpl; assert (measure bso > 0) by apply measure_pos; lia. inv H2; econstructor; eauto. 1,3: inv IS_EXPD; auto; discriminate. - all: eapply star_right; eauto. + all: eapply star_right; eauto.*) Admitted. (** * Main RTL to BTL simulation theorem -- cgit