From 640cdb752b812f2e5301acbfc63c2d4fa798de06 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 4 Jun 2021 18:47:40 +0200 Subject: Some advance in Liveness lemmas --- scheduling/BTL_Livecheck.v | 209 ++++++++++++++++++++++++++++++--------------- 1 file changed, 138 insertions(+), 71 deletions(-) (limited to 'scheduling') diff --git a/scheduling/BTL_Livecheck.v b/scheduling/BTL_Livecheck.v index d5aad8b8..95b6a155 100644 --- a/scheduling/BTL_Livecheck.v +++ b/scheduling/BTL_Livecheck.v @@ -2,7 +2,6 @@ Require Import Coqlib Maps. Require Import AST Integers Values Events Memory Globalenvs Smallstep Op Registers OptionMonad. Require Import Errors RTL BTL BTLmatchRTL. -(** TODO: adapt stuff RTLpathLivegen *) Local Open Scope lazy_bool_scope. @@ -59,32 +58,44 @@ Definition final_inst_checker (btl: code) (alive: Regset.t) (fin: final): option ASSERT exit_list_checker btl alive tbl IN Some tt end. -Fixpoint body_checker (btl: code) (ib: iblock) (alive: Regset.t): option Regset.t := +(* This definition is the meet (infimum) subset of alive registers, + used for conditions by the below checker. + A None argument represents the neutral element for intersection. *) +Definition meet (o1 o2: option Regset.t): option Regset.t := + match o1, o2 with + | None, _ => o2 + | _, None => o1 + | Some alive1, Some alive2 => Some (Regset.inter alive1 alive2) + end. + +Fixpoint body_checker (btl: code) (ib: iblock) (alive: Regset.t): option (option Regset.t) := match ib with | Bseq ib1 ib2 => - SOME alive1 <- body_checker btl ib1 alive IN + SOME oalive1 <- body_checker btl ib1 alive IN + SOME alive1 <- oalive1 IN body_checker btl ib2 alive1 - | Bnop _ => Some alive + | Bnop _ => Some (Some alive) | Bop _ args dest _ => ASSERT list_mem args alive IN - Some (Regset.add dest alive) + Some (Some (Regset.add dest alive)) | Bload _ _ _ args dest _ => ASSERT list_mem args alive IN - Some (Regset.add dest alive) + Some (Some (Regset.add dest alive)) | Bstore _ _ args src _ => ASSERT Regset.mem src alive IN ASSERT list_mem args alive IN - Some alive + Some (Some alive) | Bcond _ args ib1 ib2 _ => ASSERT list_mem args alive IN - SOME alive1 <- body_checker btl ib1 alive IN - SOME alive2 <- body_checker btl ib2 alive IN - Some (Regset.union alive1 alive2) + SOME oalive1 <- body_checker btl ib1 alive IN + SOME oalive2 <- body_checker btl ib2 alive IN + Some (meet oalive1 oalive2) | BF fin _ => SOME _ <- final_inst_checker btl alive fin IN - Some Regset.empty + Some None end. +(* This definition simply convert the result in an option unit *) Definition iblock_checker (btl: code) (ib: iblock) (alive: Regset.t): option unit := SOME _ <- body_checker btl ib alive IN Some tt. @@ -115,7 +126,6 @@ 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)). @@ -163,10 +173,25 @@ Inductive liveness_ok_fundef: fundef -> Prop := | liveness_ok_Internal f: liveness_ok_function f -> liveness_ok_fundef (Internal f) | liveness_ok_External ef: liveness_ok_fundef (External ef). -(** TODO: adapt stuff RTLpathLivegenproof *) Local Notation ext alive := (fun r => Regset.In r alive). +Definition ext_opt (oalive: option Regset.t): Regset.elt -> Prop := + match oalive with + | Some alive => ext alive + | None => fun _ => True + end. + +Lemma ext_opt_meet: forall r oalive1 oalive2, + ext_opt (meet oalive1 oalive2) r -> + ext_opt oalive1 r /\ ext_opt oalive2 r. +Proof. + intros. destruct oalive1, oalive2; + simpl in *; intuition. + eapply Regset.inter_1; eauto. + eapply Regset.inter_2; eauto. +Qed. + Lemma regset_add_spec live r1 r2: Regset.In r1 (Regset.add r2 live) <-> (r1 = r2 \/ Regset.In r1 live). Proof. destruct (Pos.eq_dec r1 r2). @@ -177,6 +202,7 @@ Proof. 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. @@ -191,11 +217,6 @@ 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. @@ -246,8 +267,6 @@ Inductive eqlive_states: state -> state -> Prop := (STACKS: list_forall2 eqlive_stackframes st1 st2): eqlive_states (Returnstate st1 v m) (Returnstate st2 v m). -(* continue to adapt stuff RTLpathLivegenproof *) - Section FSEM_SIMULATES_CFGSEM. Variable prog: BTL.program. @@ -257,7 +276,6 @@ 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) @@ -267,22 +285,39 @@ Proof. autodestruct. Qed.*) -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 ->*) - 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 ib rs2 m = Some (out rs2' m' of) - /\ eqlive_reg (ext alive2) rs1' rs2'. +Lemma cfgsem2fsem_finalstep_simu stk1 f sp rs1 m fin t s1 stk2 rs2 + (FSTEP: final_step tid ge stk1 f sp rs1 m fin t s1) + (LIVE: liveness_ok_function f) + (STACKS: list_forall2 eqlive_stackframes stk1 stk2) + (*body_checker (fn_code f) (entry ibf) (input_regs ibf) = Some x ->*) + (*eqlive_reg (ext x) rs1' rs2' ->*) + :exists s2, + final_step tr_inputs ge stk2 f sp rs2 m fin t s2 + /\ eqlive_states s1 s2. Proof. - induction 1; simpl; try_simplify_someHyps; - repeat inversion_ASSERT; intros. - - (* BF *) - generalize H0; clear H0; inversion_SOME x; try_simplify_someHyps. + destruct FSTEP. + - (* Bgoto *) + econstructor. econstructor. + econstructor. econstructor. + eauto. eauto. + repeat econstructor; eauto. +Admitted. + +Lemma cfgsem2fsem_ibistep_simu_None sp f ib: forall rs1 m rs1' m' + (ISTEP: iblock_istep ge sp rs1 m ib rs1' m' None) + alive1 oalive2 rs2 (REGS: eqlive_reg (ext alive1) rs1 rs2) + (BDY: body_checker (fn_code f) ib alive1 = Some (oalive2)), + exists rs2', + iblock_istep_run ge sp ib rs2 m = Some (out rs2' m' None) + /\ eqlive_reg (ext_opt oalive2) rs1' rs2'. +Proof. + induction ib; intros; try_simplify_someHyps; + repeat inversion_ASSERT; intros; inv ISTEP. + - (* Bnop *) + inv BDY; eauto. - (* Bop *) erewrite <- eqlive_reg_listmem; eauto. - try_simplify_someHyps. + try_simplify_someHyps; intros. repeat econstructor. apply eqlive_reg_update. eapply eqlive_reg_monotonic; eauto. @@ -299,36 +334,65 @@ Proof. intuition. - (* Bstore *) erewrite <- eqlive_reg_listmem; eauto. - rewrite <- (H src); auto. + rewrite <- (REGS src); auto. try_simplify_someHyps; intros. rewrite STORE; eauto. - - (* Bseq stop *) - 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. + destruct (body_checker _ _ _) eqn:BDY1 in BDY; try discriminate. + generalize BDY; clear BDY. + inversion_SOME aliveMid; intros OALIVE BDY2. inv OALIVE. + exploit IHib1; eauto. intros (rs2' & ISTEP1 & REGS1). rewrite ISTEP1; simpl. - eapply IHiblock_istep2; eauto. + eapply IHib2; eauto. - (* Bcond *) - generalize H2; clear H2. - inversion_SOME aliveSo; inversion_SOME aliveNot; intros BDY1 BDY2 UNION. - inv UNION. erewrite <- eqlive_reg_listmem; eauto. - admit. -Admitted. + generalize BDY; clear BDY. + inversion_SOME oaliveSo; inversion_SOME oaliveNot; intros BDY1 BDY2 JOIN. + erewrite <- eqlive_reg_listmem; eauto. + rewrite EVAL. + destruct b; [ exploit IHib1; eauto | exploit IHib2; eauto]. + all: + intros (rs2' & ISTEP1 & REGS1); + econstructor; split; eauto; inv JOIN; + eapply eqlive_reg_monotonic; eauto; + intros r EXTM; apply ext_opt_meet in EXTM; intuition. +Qed. -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. +Lemma cfgsem2fsem_ibistep_simu_Some sp f stk1 stk2 ib: forall s t rs1 m rs1' m' fin + (ISTEP: iblock_istep ge sp rs1 m ib rs1' m' (Some fin)) + (FSTEP: final_step tid ge stk1 f sp rs1' m' fin t s) + alive1 oalive2 rs2 (REGS: eqlive_reg (ext alive1) rs1 rs2) + (BDY: body_checker (fn_code f) ib alive1 = Some (oalive2)) + (LIVE: liveness_ok_function f) + (STACKS: list_forall2 eqlive_stackframes stk1 stk2), + exists rs2' s', + iblock_istep_run ge sp ib rs2 m = Some (out rs2' m' (Some fin)) + /\ final_step tr_inputs ge stk2 f sp rs2' m' fin t s' + /\ eqlive_states s s'. Proof. -Admitted. + induction ib; simpl; try_simplify_someHyps; + repeat inversion_ASSERT; intros; inv ISTEP. + - (* BF *) + exploit cfgsem2fsem_finalstep_simu; eauto. + intros (s2 & FSTEP' & STATES). eauto. + - (* Bseq stop *) + destruct (body_checker _ _ _) eqn:BDY1 in BDY; try discriminate. + generalize BDY; clear BDY. + inversion_SOME aliveMid. intros OALIVE BDY2. inv OALIVE. + exploit IHib1; eauto. intros (rs2' & s' & ISTEP1 & FSTEP1 & STATES). + rewrite ISTEP1; simpl. + do 2 eexists; intuition eauto. + - (* Bseq continue *) + destruct (body_checker _ _ _) eqn:BDY1 in BDY; try discriminate. + generalize BDY; clear BDY. + inversion_SOME aliveMid; intros OALIVE BDY2. inv OALIVE. + exploit cfgsem2fsem_ibistep_simu_None; eauto. + intros (rs2' & ISTEP1 & REGS'). rewrite ISTEP1; simpl; eauto. + - (* Bcond *) + generalize BDY; clear BDY. + inversion_SOME oaliveSo; inversion_SOME oaliveNot; intros BDY1 BDY2 JOIN. + erewrite <- eqlive_reg_listmem; eauto. rewrite EVAL. + destruct b; eauto. +Qed. Lemma cfgsem2fsem_ibstep_simu stk1 stk2 f sp rs1 m rs2 ibf pc s1 t: iblock_step tid (Genv.globalenv prog) stk1 f sp rs1 m ibf.(entry) t s1 -> @@ -341,18 +405,17 @@ 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 in LIVE. - apply decomp_liveness_checker in LIVE; destruct LIVE as [ibf' [ENTRY LIST]]. + assert (CHECKER: liveness_ok_function f) by auto. + unfold liveness_ok_function in CHECKER. + apply decomp_liveness_checker in CHECKER; destruct CHECKER 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 x; intros BODY _. - destruct STEP as (rs1' & m1' & fin' & ISTEP1 & FSTEP). - exploit cfgsem2fsem_ibistep_simu; eauto. - intros (rs2' & ISTEP2 & REGS). - rewrite <- iblock_istep_run_equiv in ISTEP2. clear ISTEP1. - exploit cfgsem2fsem_finalstep_simu; eauto. - intros (s2 & FSTEP2 & STATES). clear FSTEP. + inversion_SOME alive; intros BODY _. + destruct STEP as (rs1' & m1' & fin' & ISTEP & FSTEP). + exploit cfgsem2fsem_ibistep_simu_Some; eauto. + intros (rs2' & s' & ISTEP' & FSTEP' & REGS). + rewrite <- iblock_istep_run_equiv in ISTEP'. clear ISTEP. unfold iblock_step. repeat eexists; eauto. Qed. @@ -365,18 +428,22 @@ Lemma cfgsem2fsem_step_simu s1 s1' t s2: step tr_inputs (Genv.globalenv prog) s2 t s2' /\ eqlive_states s1' s2'. Proof. - destruct 1 as [stack ibf f sp n rs m t s ENTRY STEP | | | ]; intros STATES; - try (inv STATES; inv LIVE; eexists; split; econstructor; eauto; fail). - - inv STATES; simplify_someHyps. + destruct 1 as [stack ibf f sp n rs m t s ENTRY STEP | | | ]; intros STATES. + - (* iblock *) + inv STATES; simplify_someHyps. intros. exploit cfgsem2fsem_ibstep_simu; eauto. intros (s2 & STEP2 & EQUIV2). eexists; split; eauto. - - inv STATES; inv LIVE. + - (* function internal *) + inv STATES; inv LIVE. 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. + - (* function external *) + inv STATES; inv LIVE; eexists; split; econstructor; eauto. + - (* return *) + 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. -- cgit