From cb167a462bd4e26ae31694ecf48425ad257fb0f3 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 7 Jun 2021 12:33:49 +0200 Subject: End of liveness proof --- scheduling/BTL_Livecheck.v | 99 +++++++++++++++++++++------------------------- 1 file changed, 45 insertions(+), 54 deletions(-) (limited to 'scheduling/BTL_Livecheck.v') diff --git a/scheduling/BTL_Livecheck.v b/scheduling/BTL_Livecheck.v index a92f24c3..25a1c545 100644 --- a/scheduling/BTL_Livecheck.v +++ b/scheduling/BTL_Livecheck.v @@ -277,21 +277,6 @@ Hypothesis all_fundef_liveness_ok: 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 tr_inputs_eqlive_None f pc tbl ibf rs1 rs2: - (fn_code f) ! pc = Some ibf -> - eqlive_reg (ext (input_regs ibf)) rs1 rs2 -> - eqlive_reg (ext (input_regs ibf)) (tid f (pc :: tbl) None rs1) - (tr_inputs f (pc :: tbl) None rs2). -Proof. - intros PC REGS. - unfold eqlive_reg. intros r INR. - unfold tid. rewrite tr_inputs_get. - simpl. rewrite PC. - exploit Regset.union_3. eapply INR. - intros INRU. eapply Regset.mem_1 in INRU. - erewrite INRU; eauto. -Qed. - Lemma eqlive_reg_update_gso alive rs1 rs2 res r: forall v : val, eqlive_reg (ext alive) rs1 # res <- v rs2 # res <- v -> res <> r -> Regset.In r alive -> @@ -302,24 +287,6 @@ Proof. rewrite !Regmap.gso in INR; auto. Qed. -Lemma tr_inputs_eqlive_update f pc ibf rs1 rs2 res: - (fn_code f) ! pc = Some ibf -> - forall v : val, - eqlive_reg (ext (input_regs ibf)) rs1 # res <- v rs2 # res <- v -> - eqlive_reg (ext (input_regs ibf)) - (tid f (pc :: nil) (Some res) rs1) # res <- v - (tr_inputs f (pc :: nil) (Some res) rs2) # res <- v. -Proof. - intros PC v REGS. apply eqlive_reg_update. - unfold eqlive_reg. intros r (NRES & INR). - unfold tid. rewrite tr_inputs_get. - simpl. rewrite PC. assert (NRES': res <> r) by auto. - clear NRES. exploit Regset.union_3. eapply INR. - intros INRU. exploit Regset.remove_2; eauto. - intros INRU_RES. eapply Regset.mem_1 in INRU_RES. - erewrite INRU_RES. eapply eqlive_reg_update_gso; eauto. -Qed. - Lemma find_funct_liveness_ok v fd: Genv.find_funct ge v = Some fd -> liveness_ok_fundef fd. Proof. @@ -439,34 +406,63 @@ Proof. simpl; intros; eauto with local. Qed. -Lemma tr_inputs_eqlive_list_None tbl: forall f pc n alive ibf rs1 rs2, - (*rs1 # arg = Vint n ->*) - eqlive_reg (ext alive) rs1 rs2 -> - exit_list_checker (fn_code f) alive tbl = true -> -(*H1 : Regset.mem arg alive = true*) - list_nth_z tbl n = Some pc -> - (fn_code f) ! pc = Some ibf -> - eqlive_reg (ext (input_regs ibf)) rs1 rs2 -> +Lemma tr_inputs_eqlive_None f pc tbl ibf rs1 rs2 + (PC: (fn_code f) ! pc = Some ibf) + (REGS: eqlive_reg (ext (input_regs ibf)) rs1 rs2) + :eqlive_reg (ext (input_regs ibf)) (tid f (pc :: tbl) None rs1) + (tr_inputs f (pc :: tbl) None rs2). +Proof. + unfold eqlive_reg. intros r INR. + unfold tid. rewrite tr_inputs_get. + simpl. rewrite PC. + exploit Regset.union_3. eapply INR. + intros INRU. eapply Regset.mem_1 in INRU. + erewrite INRU; eauto. +Qed. + +Lemma tr_inputs_eqlive_list_None tbl: forall f pc n alive ibf rs1 rs2 + (REGS1: eqlive_reg (ext alive) rs1 rs2) + (EXIT_LIST: exit_list_checker (fn_code f) alive tbl = true) + (LIST: list_nth_z tbl n = Some pc) + (PC: (fn_code f) ! pc = Some ibf) + (REGS2: eqlive_reg (ext (input_regs ibf)) rs1 rs2), eqlive_reg (ext (input_regs ibf)) (tid f tbl None rs1) (tr_inputs f tbl None rs2). Proof. induction tbl as [| pc' tbl IHtbl]; try_simplify_someHyps. autodestruct; try_simplify_someHyps. - intros; eapply tr_inputs_eqlive_None; eauto. - - rewrite lazy_and_Some_tt_true in H0. - destruct H0 as [EXIT EXIT_REM]. - intros LIST PC. unfold eqlive_reg. - intros r INR. + - rewrite lazy_and_Some_tt_true in EXIT_LIST. + destruct EXIT_LIST as [EXIT EXIT_REM]. + intros. unfold eqlive_reg. intros r INR. exploit (IHtbl f pc (Z.pred n) alive ibf rs1 rs2); eauto. unfold tid. rewrite !tr_inputs_get. exploit exit_checker_eqlive; eauto. - intros (ibf' & PC' & REGS). + intros (ibf' & PC' & REGS3). simpl; rewrite PC'. autodestruct. + intro INRU. apply Regset.mem_2 in INRU. intros EQR. eapply Regset.union_2 in INRU. eapply Regset.mem_1 in INRU. erewrite INRU; auto. + intros. autodestruct. - rewrite (H3 r); auto. + rewrite (REGS2 r); auto. +Qed. + +Lemma tr_inputs_eqlive_update f pc ibf rs1 rs2 res + (PC: (fn_code f) ! pc = Some ibf) + :forall (v: val) + (REGS: eqlive_reg (ext (input_regs ibf)) rs1 # res <- v rs2 # res <- v), + eqlive_reg (ext (input_regs ibf)) + (tid f (pc :: nil) (Some res) rs1) # res <- v + (tr_inputs f (pc :: nil) (Some res) rs2) # res <- v. +Proof. + intros. apply eqlive_reg_update. + unfold eqlive_reg. intros r (NRES & INR). + unfold tid. rewrite tr_inputs_get. + simpl. rewrite PC. assert (NRES': res <> r) by auto. + clear NRES. exploit Regset.union_3. eapply INR. + intros INRU. exploit Regset.remove_2; eauto. + intros INRU_RES. eapply Regset.mem_1 in INRU_RES. + erewrite INRU_RES. eapply eqlive_reg_update_gso; eauto. Qed. Local Hint Resolve tr_inputs_eqlive_None tr_inputs_eqlive_update: core. @@ -523,13 +519,8 @@ Proof. + econstructor; eauto. erewrite <- REGS; eauto. + repeat (econstructor; simpl; eauto). - - eapply tr_inputs_eqlive_list_None. - eapply REGS. - eauto. - eauto. - eauto. - eauto. + apply (tr_inputs_eqlive_list_None tbl f pc' (Int.unsigned n) alive ibf rs1 rs2); + auto. Qed. Lemma cfgsem2fsem_ibistep_simu_None sp f ib: forall rs1 m rs1' m' -- cgit