From 54d0ce9246ed1be12f150eb3745626a7576bf20b Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 10 May 2021 10:28:55 +0200 Subject: is_exp and bcond proof --- scheduling/RTLtoBTLproof.v | 53 ++++++++++++++++++++++++++++++---------------- 1 file changed, 35 insertions(+), 18 deletions(-) (limited to 'scheduling/RTLtoBTLproof.v') diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index efc22eb6..ac9cb8d8 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -1,4 +1,4 @@ -Require Import Coqlib Maps. +Require Import Coqlib Maps Lia. Require Import AST Integers Values Events Memory Globalenvs Smallstep. Require Import RTL Op Registers OptionMonad BTL. @@ -6,12 +6,10 @@ Require Import Errors Linking RTLtoBTL. Require Import Linking. -(* TODO: remplacer "right_assoc" par "expand" ci-dessous *) - 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_right_assoc: forall pc ib, (fn_code tf)!pc=Some ib -> is_right_assoc ib.(entry); + 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 @@ -33,7 +31,7 @@ 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_right_assoc ib.(entry)) -> + (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. @@ -48,7 +46,7 @@ Proof. unfold transf_function; unfold bind. repeat autodestruct. intros H _ _ X. inversion X; subst; clear X. eexists; eapply verify_function_correct; simpl; eauto. - eapply right_assoc_code_correct; eauto. + eapply expand_code_correct; eauto. Qed. Lemma transf_fundef_correct f f': @@ -112,7 +110,7 @@ Inductive match_states: (option iblock) -> RTL.state -> state -> Prop := (ATpc0: (fn_code f')!pcB0 = Some ib0) (DUPLIC: dupmap!pcB0 = Some pcR0) (MIB: match_iblock dupmap (RTL.fn_code f) isfst pcR1 ib None) - (RIGHTA: is_right_assoc ib) + (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_states (Some ib) (RTL.State st f sp pcR1 rs m) (State st' f' sp pcB0 rs0 m0) @@ -245,6 +243,12 @@ Definition omeasure (oib: option iblock): nat := | Some ib => measure ib end. +Lemma measure_pos: forall ib, + measure ib > 0. +Proof. + induction ib; simpl; auto; lia. +Qed. + Lemma opt_simu_intro sp f f' st st' dupmap isfst pcR0 pcR1 pcB0 ib ib0 rs m rs0 m0 t s1' (STEP : RTL.step ge (RTL.State st f sp pcR1 rs m) t s1') @@ -253,7 +257,7 @@ Lemma opt_simu_intro (ATpc0 : (fn_code f') ! pcB0 = Some ib0) (DUPLIC : dupmap ! pcB0 = Some pcR0) (MIB : match_iblock dupmap (RTL.fn_code f) isfst pcR1 ib None) - (RIGHTA : is_right_assoc ib) + (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 = @@ -280,12 +284,12 @@ Proof. + (* Bnop *) inversion STEP; subst; try_simplify_someHyps. (* TODO maybe move that for each subcase *) exists (Some b2); right; repeat (split; auto). - econstructor; eauto. inv RIGHTA; auto; discriminate. + econstructor; eauto. inv IS_EXPD; auto; discriminate. eapply star_right; eauto. + (* Bop *) inversion STEP; subst; try_simplify_someHyps. exists (Some b2); right; repeat (split; auto). - econstructor; eauto. inv RIGHTA; auto; discriminate. + econstructor; eauto. inv IS_EXPD; auto; discriminate. eapply star_right; eauto. erewrite eval_operation_preserved in H10. erewrite H10 in BTL_RUN; simpl in BTL_RUN; auto. @@ -293,7 +297,7 @@ Proof. + (* Bload *) inversion STEP; subst; try_simplify_someHyps. exists (Some (b2)); right; repeat (split; auto). - econstructor; eauto. inv RIGHTA; auto; discriminate. + econstructor; eauto. inv IS_EXPD; auto; discriminate. eapply star_right; eauto. erewrite eval_addressing_preserved in H10. erewrite H10, H11 in BTL_RUN; simpl in BTL_RUN; auto. @@ -301,17 +305,30 @@ Proof. + (* Bstore *) inversion STEP; subst; try_simplify_someHyps. exists (Some b2); right; repeat (split; auto). - econstructor; eauto. inv RIGHTA; auto; discriminate. + econstructor; eauto. inv IS_EXPD; auto; discriminate. eapply star_right; eauto. erewrite eval_addressing_preserved in H10. erewrite H10, H11 in BTL_RUN; simpl in BTL_RUN; auto. intros; rewrite <- symbols_preserved; trivial. + (* Absurd case *) - inv RIGHTA. inv H4. inv H. - + (* Bcond *) - admit. + 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 *) - admit. + inversion STEP; subst; try_simplify_someHyps. + intros; rewrite H12 in BTL_RUN. destruct b. + * (* Ifso *) + exists (Some bso); right; repeat (split; eauto). + simpl; assert (measure bnot > 0) by apply measure_pos; lia. + inv H2; econstructor; eauto. + 1,3: inv IS_EXPD; auto; discriminate. + all: eapply star_right; eauto. + * (* Ifnot *) + exists (Some bnot); right; repeat (split; eauto). + 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. Admitted. Theorem opt_simu s1 t s1' oib s2: @@ -338,7 +355,7 @@ Proof. * eapply exec_function_internal. erewrite preserv_fnstacksize; eauto. * econstructor; eauto. - eapply code_right_assoc; eauto. + eapply code_expand; eauto. all: erewrite preserv_fnparams; eauto. constructor. + (* External function *) @@ -356,7 +373,7 @@ Proof. eexists; left; eexists; split. + eapply exec_return. + econstructor; eauto. - eapply code_right_assoc; eauto. + eapply code_expand; eauto. constructor. Qed. -- cgit