From 644f1a3208f9a4e013928e042257763313ac2b0d Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 7 Jun 2021 12:17:53 +0200 Subject: ugly complete version of liveness proof (I will clean in next commits) --- scheduling/BTL_Livecheck.v | 74 +++++++++++++++++++++++++--------------------- 1 file changed, 40 insertions(+), 34 deletions(-) (limited to 'scheduling/BTL_Livecheck.v') diff --git a/scheduling/BTL_Livecheck.v b/scheduling/BTL_Livecheck.v index 3882639c..a92f24c3 100644 --- a/scheduling/BTL_Livecheck.v +++ b/scheduling/BTL_Livecheck.v @@ -277,11 +277,11 @@ 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 ibf rs1 rs2: +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 :: nil) None rs1) - (tr_inputs f (pc :: nil) None 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. @@ -439,6 +439,36 @@ 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 -> + 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. + 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). + 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. +Qed. + Local Hint Resolve tr_inputs_eqlive_None tr_inputs_eqlive_update: core. Lemma cfgsem2fsem_finalstep_simu sp f stk1 stk2 s t fin alive rs1 m rs2 (FSTEP: final_step tid ge stk1 f sp rs1 m fin t s) @@ -494,37 +524,13 @@ Proof. erewrite <- REGS; eauto. + repeat (econstructor; simpl; eauto). -(* - generalize dependent ibf. - generalize dependent n. - generalize dependent alive. - generalize dependent tbl. - induction tbl; simpl; try congruence. - intros alive REGS. rewrite lazy_and_Some_tt_true. - intros (EXIT & EXIT_REM) INARG n ARG. autodestruct. - * try_simplify_someHyps; intros. - - 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. - - - * try_simplify_someHyps; intros. - exploit IHtbl. eapply REGS. - eauto. eauto. eauto. eauto. - exploit exit_checker_eqlive; eauto. - intros (ibf' & 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. - admit.*) -Admitted. + eapply tr_inputs_eqlive_list_None. + eapply REGS. + eauto. + eauto. + eauto. + eauto. +Qed. Lemma cfgsem2fsem_ibistep_simu_None sp f ib: forall rs1 m rs1' m' (ISTEP: iblock_istep ge sp rs1 m ib rs1' m' None) -- cgit