From 1586662d37caefd065f54bd693c0594109b3db36 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 2 Jun 2021 17:21:17 +0200 Subject: lemmas on entrypoint, tr_inputs, eqlive_regs, ... --- scheduling/BTL_Livecheck.v | 133 ++++++++++++++++++++++++++++++++++++++------- 1 file changed, 112 insertions(+), 21 deletions(-) (limited to 'scheduling') diff --git a/scheduling/BTL_Livecheck.v b/scheduling/BTL_Livecheck.v index 50719f67..82efff44 100644 --- a/scheduling/BTL_Livecheck.v +++ b/scheduling/BTL_Livecheck.v @@ -120,24 +120,48 @@ Proof. simpl in * |- *. rewrite lazy_and_Some_tt_true in CHECKER. intuition (subst; auto). Qed. + +Definition liveness_checker_bool (f: BTL.function): bool := + f.(fn_code)!(f.(fn_entrypoint)) &&& list_iblock_checker f.(fn_code) (PTree.elements f.(fn_code)). + Definition liveness_checker (f: BTL.function): res unit := - match list_iblock_checker f.(fn_code) (PTree.elements f.(fn_code)) with + match liveness_checker_bool f with | true => OK tt | false => Error (msg "BTL_Livecheck: liveness_checker failed") end. +Lemma decomp_liveness_checker f: + liveness_checker f = OK tt -> + exists ibf, f.(fn_code)!(f.(fn_entrypoint)) = Some ibf /\ + list_iblock_checker f.(fn_code) (PTree.elements f.(fn_code)) = true. +Proof. + intros LIVE; unfold liveness_checker in LIVE. + destruct liveness_checker_bool eqn:EQL; try congruence. + clear LIVE. unfold liveness_checker_bool in EQL. + rewrite lazy_and_Some_true in EQL; destruct EQL as [[ibf ENTRY] LIST]. + eexists; split; eauto. +Qed. + Lemma liveness_checker_correct f n ibf: liveness_checker f = OK tt -> f.(fn_code)!n = Some ibf -> iblock_checker f.(fn_code) ibf.(entry) ibf.(input_regs) = Some tt. Proof. - unfold liveness_checker. - destruct list_iblock_checker eqn:EQL; try congruence. - intros _ P. exploit list_iblock_checker_correct; eauto. + intros LIVE PC. + apply decomp_liveness_checker in LIVE; destruct LIVE as [ibf' [ENTRY LIST]]. + exploit list_iblock_checker_correct; eauto. - eapply PTree.elements_correct; eauto. - simpl; auto. Qed. +Lemma liveness_checker_entrypoint f: + liveness_checker f = OK tt -> + f.(fn_code)!(f.(fn_entrypoint)) <> None. +Proof. + intros LIVE; apply decomp_liveness_checker in LIVE; destruct LIVE as [ibf' [ENTRY LIST]]. + unfold not; intros CONTRA. congruence. +Qed. + Definition liveness_ok_function (f: BTL.function): Prop := liveness_checker f = OK tt. Inductive liveness_ok_fundef: fundef -> Prop := @@ -195,16 +219,79 @@ Hypothesis all_liveness_checker: forall b f, Genv.find_funct_ptr ge b = Some f - Local Hint Constructors eqlive_stackframes eqlive_states final_step list_forall2 step: core. -Lemma cfgsem2fsem_ibistep_simu sp rs1 m1 rs1' m1' of ib - (ISTEP: iblock_istep ge sp rs1 m1 ib rs1' m1' of): forall - rs2 m2, - exists rs2' m2', iblock_istep_run ge sp ib rs2 m2 = Some (out rs2' m2' of). +(*Lemma tr_inputs_eqlive f rs1 rs2 tbl or r + (REGS: forall r, eqlive_reg (ext (input_regs ibf)) rs1 rs2) + :eqlive_reg (tr_inputs f tbl or rs1) (tid f tbl or rs2). +Proof. + unfold tid; rewrite tr_inputs_get. + autodestruct. + Qed.*) + +Remark is_none_true {A} (fin: option A): + is_none fin = true -> + fin = None. +Proof. + unfold is_none; destruct fin; congruence. +Qed. + +Local Hint Resolve Regset.mem_2 Regset.subset_2: core. +Lemma lazy_and_true (b1 b2: bool): b1 &&& b2 = true <-> b1 = true /\ b2 = true. +Proof. + destruct b1; simpl; intuition. +Qed. + +Lemma list_mem_correct (rl: list reg) (alive: Regset.t): + list_mem rl alive = true -> forall r, List.In r rl -> ext alive r. +Proof. + induction rl; simpl; try rewrite lazy_and_true; intuition subst; auto. +Qed. + +Lemma eqlive_reg_list (alive: Regset.elt -> Prop) args rs1 rs2: eqlive_reg alive rs1 rs2 -> (forall r, List.In r args -> (alive r)) -> rs1##args = rs2##args. +Proof. + induction args; simpl; auto. + intros EQLIVE ALIVE; rewrite IHargs; auto. + unfold eqlive_reg in EQLIVE. + rewrite EQLIVE; auto. +Qed. + +Lemma eqlive_reg_listmem (alive: Regset.t) args rs1 rs2: eqlive_reg (ext alive) rs1 rs2 -> list_mem args alive = true -> rs1##args = rs2##args. Proof. - induction ISTEP; simpl; try_simplify_someHyps; intros. + intros; eapply eqlive_reg_list; eauto. + intros; eapply list_mem_correct; eauto. +Qed. + +Lemma cfgsem2fsem_ibistep_simu sp f: forall rs1 m rs1' m' rs2 of ibf res, + iblock_istep ge sp rs1 m ibf.(entry) rs1' m' of -> + (*iblock_checker (fn_code f) ibf.(entry) ibf.(input_regs) = Some tt ->*) + eqlive_reg (ext (input_regs ibf)) rs1 rs2 -> + body_checker (fn_code f) ibf.(entry) ibf.(input_regs) = Some res -> +(*LIST : list_iblock_checker (fn_code f) (PTree.elements (fn_code f)) = true*) + exists rs2', iblock_istep_run ge sp ibf.(entry) rs2 m = Some (out rs2' m' of). +Proof. + induction 1; simpl; repeat inversion_ASSERT; intros; try_simplify_someHyps. - (* Bop *) - inversion_SOME v0; intros EVAL'; - repeat eexists. - inv EVAL'. + intros. + erewrite <- eqlive_reg_listmem; eauto. + try_simplify_someHyps. + (* + (*- [> BF <]*) + (*intros. inv H1; eexists; reflexivity.*) + - (* Bseq stop *) + admit. (* + inversion_SOME res0. + inversion_ASSERT; intros. + exploit IHiblock_istep. unfold iblock_checker. + rewrite H1. inv H0. + inversion_SOME out1. + try_simplify_someHyps.*) + - inversion_SOME res0. + inversion_ASSERT; intros. + admit. + (* TODO The first induction hyp should not be based on iblock_checker *) + (* exploit IHiblock_istep1. unfold iblock_checker. + rewrite H2. apply is_none_true in H1. rewrite H1. *) + - (* Bcond *) + admit.*) Admitted. Lemma cfgsem2fsem_finalstep_simu stk1 f sp rs1 m1 fin t s1 stk2 rs2 m2 @@ -215,7 +302,7 @@ Lemma cfgsem2fsem_finalstep_simu stk1 f sp rs1 m1 fin t s1 stk2 rs2 m2 Proof. destruct FSTEP. - (* Bgoto *) - (*eexists; split; simpl ; econstructor; eauto.*) + eexists; split; simpl. econstructor; eauto. Admitted. Lemma cfgsem2fsem_ibstep_simu stk1 stk2 f sp rs1 m rs2 ibf pc s1 t: @@ -229,19 +316,21 @@ Lemma cfgsem2fsem_ibstep_simu stk1 stk2 f sp rs1 m rs2 ibf pc s1 t: eqlive_states s1 s2. Proof. intros STEP STACKS EQLIVE LIVE PC. - unfold liveness_ok_function, liveness_checker in LIVE. - destruct list_iblock_checker eqn:LIBC in LIVE; try discriminate. - clear LIVE. - destruct STEP as (rs1' & m1' & fin & ISTEP & FSTEP). + unfold liveness_ok_function in LIVE. + apply decomp_liveness_checker in LIVE; destruct LIVE as [ibf' [ENTRY LIST]]. + eapply PTree.elements_correct in PC as PCIN. + eapply list_iblock_checker_correct in LIST as IBC; eauto. + unfold iblock_checker in IBC. generalize IBC; clear IBC. + inversion_SOME res; inversion_SOME fin; intros RES BODY FINAL. + destruct STEP as (rs1' & m1' & fin' & ISTEP & FSTEP). exploit cfgsem2fsem_ibistep_simu; eauto. - intros (rs2' & m2' & ISTEP2). + intros (rs2' & ISTEP2). rewrite <- iblock_istep_run_equiv in ISTEP2. clear ISTEP. exploit cfgsem2fsem_finalstep_simu; eauto. intros (s2 & FSTEP2 & STATES). clear FSTEP. unfold iblock_step. repeat eexists; eauto. Qed. - Local Hint Constructors step: core. Lemma cfgsem2fsem_step_simu s1 s1' t s2: @@ -259,14 +348,16 @@ Proof. intros (s2 & STEP2 & EQUIV2). eexists; split; eauto. - inv STATES; inv LIVE. - eexists; split; econstructor; eauto. all : admit. (* TODO gourdinl *) + apply liveness_checker_entrypoint in H0 as ENTRY. + destruct ((fn_code f) ! (fn_entrypoint f)) eqn:EQENTRY; try congruence; eauto. + eexists; split; repeat econstructor; eauto. - inv STATES. inversion STACKS as [|s1 st1 s' s2 STACK STACKS']; subst; clear STACKS. inv STACK. exists (State s2 f sp pc (rs2 # res <- vres) m); split. * apply exec_return. * eapply eqlive_states_intro; eauto. -Admitted. +Qed. Theorem cfgsem2fsem: forward_simulation (cfgsem prog) (fsem prog). Proof. -- cgit