From b65a646a9ff0d16e65923d225b75942cc766bc02 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Thu, 3 Jun 2021 13:41:59 +0200 Subject: update a more general version of the liveness checker --- scheduling/BTL_Livecheck.v | 211 +++++++++++++++++++++++++-------------------- 1 file changed, 118 insertions(+), 93 deletions(-) (limited to 'scheduling/BTL_Livecheck.v') diff --git a/scheduling/BTL_Livecheck.v b/scheduling/BTL_Livecheck.v index 82efff44..d5aad8b8 100644 --- a/scheduling/BTL_Livecheck.v +++ b/scheduling/BTL_Livecheck.v @@ -59,40 +59,34 @@ Definition final_inst_checker (btl: code) (alive: Regset.t) (fin: final): option ASSERT exit_list_checker btl alive tbl IN Some tt end. -Definition is_none {A} (oa: option A): bool := - match oa with - | Some _ => false - | None => true - end. - -Fixpoint body_checker (btl: code) (ib: iblock) (alive: Regset.t): option (Regset.t*option final) := +Fixpoint body_checker (btl: code) (ib: iblock) (alive: Regset.t): option Regset.t := match ib with | Bseq ib1 ib2 => - SOME res <- body_checker btl ib1 alive IN - ASSERT is_none (snd res) IN - body_checker btl ib2 (fst res) - | Bnop _ => Some (alive, None) + SOME alive1 <- body_checker btl ib1 alive IN + body_checker btl ib2 alive1 + | Bnop _ => Some alive | Bop _ args dest _ => ASSERT list_mem args alive IN - Some (Regset.add dest alive, None) + Some (Regset.add dest alive) | Bload _ _ _ args dest _ => ASSERT list_mem args alive IN - Some (Regset.add dest alive, None) + Some (Regset.add dest alive) | Bstore _ _ args src _ => ASSERT Regset.mem src alive IN ASSERT list_mem args alive IN - Some (alive, None) - | Bcond _ args (BF (Bgoto s) _) (Bnop None) _ => + Some alive + | Bcond _ args ib1 ib2 _ => ASSERT list_mem args alive IN - exit_checker btl alive s (alive, None) - | BF fin _ => Some (alive, Some fin) - | _ => None + SOME alive1 <- body_checker btl ib1 alive IN + SOME alive2 <- body_checker btl ib2 alive IN + Some (Regset.union alive1 alive2) + | BF fin _ => + SOME _ <- final_inst_checker btl alive fin IN + Some Regset.empty end. -Definition iblock_checker (btl: code) (ib: iblock) (alive: Regset.t) : option unit := - SOME res <- body_checker btl ib alive IN - SOME fin <- snd res IN - final_inst_checker btl (fst res) fin. +Definition iblock_checker (btl: code) (ib: iblock) (alive: Regset.t): option unit := + SOME _ <- body_checker btl ib alive IN Some tt. Fixpoint list_iblock_checker (btl: code) (l: list (node*iblock_info)): bool := match l with @@ -113,8 +107,9 @@ Proof. destruct x; auto. Qed. -Lemma list_iblock_checker_correct btl l: - list_iblock_checker btl l = true -> forall e, List.In e l -> iblock_checker btl (snd e).(entry) (snd e).(input_regs) = Some tt. +Lemma list_iblock_checker_correct btl l: + list_iblock_checker btl l = true -> + forall e, List.In e l -> iblock_checker btl (snd e).(entry) (snd e).(input_regs) = Some tt. Proof. intros CHECKER e H; induction l as [|(n & ibf) l]; intuition. simpl in * |- *. rewrite lazy_and_Some_tt_true in CHECKER. intuition (subst; auto). @@ -181,9 +176,53 @@ Proof. * eapply Regset.add_2; auto. 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. + Definition eqlive_reg (alive: Regset.elt -> Prop) (rs1 rs2: regset): Prop := forall r, (alive r) -> rs1#r = rs2#r. +Lemma eqlive_reg_empty rs1 rs2: eqlive_reg (ext Regset.empty) rs1 rs2. +Proof. + unfold eqlive_reg; intros. inv H. +Qed. + +Lemma eqlive_reg_update (alive: Regset.elt -> Prop) rs1 rs2 r v: eqlive_reg (fun r1 => r1 <> r /\ alive r1) rs1 rs2 -> eqlive_reg alive (rs1 # r <- v) (rs2 # r <- v). +Proof. + unfold eqlive_reg; intros EQLIVE r0 ALIVE. + destruct (Pos.eq_dec r r0) as [H|H]. + - subst. rewrite! Regmap.gss. auto. + - rewrite! Regmap.gso; auto. +Qed. + +Lemma eqlive_reg_monotonic (alive1 alive2: Regset.elt -> Prop) rs1 rs2: eqlive_reg alive2 rs1 rs2 -> (forall r, alive1 r -> alive2 r) -> eqlive_reg alive1 rs1 rs2. +Proof. + unfold eqlive_reg; intuition. +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. + intros; eapply eqlive_reg_list; eauto. + intros; eapply list_mem_correct; eauto. +Qed. + Inductive eqlive_stackframes: stackframe -> stackframe -> Prop := | eqlive_stackframes_intro ibf res f sp pc rs1 rs2 (LIVE: liveness_ok_function f) @@ -218,6 +257,7 @@ Let ge := Genv.globalenv prog. Hypothesis all_liveness_checker: forall b f, Genv.find_funct_ptr ge b = Some f -> liveness_ok_fundef f. Local Hint Constructors eqlive_stackframes eqlive_states final_step list_forall2 step: core. +Local Hint Resolve eqlive_reg_empty: core. (*Lemma tr_inputs_eqlive f rs1 rs2 tbl or r (REGS: forall r, eqlive_reg (ext (input_regs ibf)) rs1 rs2) @@ -227,82 +267,67 @@ Proof. 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. - 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 -> +Lemma cfgsem2fsem_ibistep_simu sp f: forall rs1 m rs1' m' of ib, + iblock_istep ge sp rs1 m ib 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 -> + forall alive1 alive2 rs2, eqlive_reg (ext alive1) rs1 rs2 -> + body_checker (fn_code f) ib alive1 = Some alive2 -> (*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). + exists rs2', iblock_istep_run ge sp ib rs2 m = Some (out rs2' m' of) + /\ eqlive_reg (ext alive2) rs1' rs2'. Proof. - induction 1; simpl; repeat inversion_ASSERT; intros; try_simplify_someHyps. + induction 1; simpl; try_simplify_someHyps; + repeat inversion_ASSERT; intros. + - (* BF *) + generalize H0; clear H0; inversion_SOME x; try_simplify_someHyps. - (* Bop *) - intros. erewrite <- eqlive_reg_listmem; eauto. try_simplify_someHyps. - (* - (*- [> BF <]*) - (*intros. inv H1; eexists; reflexivity.*) + repeat econstructor. + apply eqlive_reg_update. + eapply eqlive_reg_monotonic; eauto. + intros r0; rewrite regset_add_spec. + intuition. + - (* Bload *) + erewrite <- eqlive_reg_listmem; eauto. + try_simplify_someHyps; intros. + rewrite LOAD; eauto. + repeat econstructor. + apply eqlive_reg_update. + eapply eqlive_reg_monotonic; eauto. + intros r0; rewrite regset_add_spec. + intuition. + - (* Bstore *) + erewrite <- eqlive_reg_listmem; eauto. + rewrite <- (H src); auto. + try_simplify_someHyps; intros. + rewrite STORE; eauto. - (* 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. *) + generalize H1; clear H1. + inversion_SOME aliveMid. intros BDY1 BDY2. + (*rewrite iblock_istep_run_equiv in H.*) + exploit IHiblock_istep; eauto. + intros (rs2' & ISTEP1 & REGS). rewrite ISTEP1; simpl. + repeat econstructor. admit. + - (* Bseq continue *) + generalize H2; clear H2. + inversion_SOME aliveMid; intros BDY1 BDY2. + exploit IHiblock_istep1; eauto. + intros (rs2' & ISTEP1 & REGS1). rewrite ISTEP1; simpl. + eapply IHiblock_istep2; eauto. - (* Bcond *) - admit.*) + generalize H2; clear H2. + inversion_SOME aliveSo; inversion_SOME aliveNot; intros BDY1 BDY2 UNION. + inv UNION. erewrite <- eqlive_reg_listmem; eauto. + admit. Admitted. -Lemma cfgsem2fsem_finalstep_simu stk1 f sp rs1 m1 fin t s1 stk2 rs2 m2 - (FSTEP: final_step tid ge stk1 f sp rs1 m1 fin t s1) - (STACKS: list_forall2 eqlive_stackframes stk1 stk2) - : exists s2, final_step tr_inputs ge stk2 f sp rs2 m2 fin t s2 - /\ eqlive_states s1 s2. +Lemma cfgsem2fsem_finalstep_simu stk1 f sp rs1 m1 fin t s1 stk2 rs2 m2: + final_step tid ge stk1 f sp rs1 m1 fin t s1 -> + list_forall2 eqlive_stackframes stk1 stk2 -> + exists s2, final_step tr_inputs ge stk2 f sp rs2 m2 fin t s2 + /\ eqlive_states s1 s2. Proof. - destruct FSTEP. - - (* Bgoto *) - eexists; split; simpl. econstructor; eauto. Admitted. Lemma cfgsem2fsem_ibstep_simu stk1 stk2 f sp rs1 m rs2 ibf pc s1 t: @@ -321,11 +346,11 @@ Proof. 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). + inversion_SOME x; intros BODY _. + destruct STEP as (rs1' & m1' & fin' & ISTEP1 & FSTEP). exploit cfgsem2fsem_ibistep_simu; eauto. - intros (rs2' & ISTEP2). - rewrite <- iblock_istep_run_equiv in ISTEP2. clear ISTEP. + intros (rs2' & ISTEP2 & REGS). + rewrite <- iblock_istep_run_equiv in ISTEP2. clear ISTEP1. exploit cfgsem2fsem_finalstep_simu; eauto. intros (s2 & FSTEP2 & STATES). clear FSTEP. unfold iblock_step. repeat eexists; eauto. -- cgit