From 4527f1503e7e7c76d12cfac10e0e7e719b0578a6 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 4 Jun 2021 19:40:11 +0200 Subject: preparation and starting final lemma --- scheduling/BTL_Livecheck.v | 121 +++++++++++++++++++++++++++++++++++++-------- 1 file changed, 100 insertions(+), 21 deletions(-) (limited to 'scheduling') diff --git a/scheduling/BTL_Livecheck.v b/scheduling/BTL_Livecheck.v index 95b6a155..8d613ef8 100644 --- a/scheduling/BTL_Livecheck.v +++ b/scheduling/BTL_Livecheck.v @@ -26,33 +26,33 @@ Definition reg_builtin_res (res: builtin_res reg) (alive: Regset.t): Regset.t := | _ => alive end. -Definition exit_checker {A} (btl: code) (alive: Regset.t) (s: node) (v: A): option A := +Definition exit_checker (btl: code) (alive: Regset.t) (s: node): option unit := SOME next <- btl!s IN ASSERT Regset.subset next.(input_regs) alive IN - Some v. + Some tt. Fixpoint exit_list_checker (btl: code) (alive: Regset.t) (l: list node): bool := match l with | nil => true - | s :: l' => exit_checker btl alive s true &&& exit_list_checker btl alive l' + | s :: l' => exit_checker btl alive s &&& exit_list_checker btl alive l' end. Definition final_inst_checker (btl: code) (alive: Regset.t) (fin: final): option unit := match fin with | Bgoto s => - exit_checker btl alive s tt + exit_checker btl alive s | Breturn oreg => ASSERT reg_option_mem oreg alive IN Some tt | Bcall _ ros args res s => ASSERT list_mem args alive IN ASSERT reg_sum_mem ros alive IN - exit_checker btl (Regset.add res alive) s tt + exit_checker btl (Regset.add res alive) s | Btailcall _ ros args => ASSERT list_mem args alive IN ASSERT reg_sum_mem ros alive IN Some tt | Bbuiltin _ args res s => ASSERT list_mem (params_of_builtin_args args) alive IN - exit_checker btl (reg_builtin_res res alive) s tt + exit_checker btl (reg_builtin_res res alive) s | Bjumptable arg tbl => ASSERT Regset.mem arg alive IN ASSERT exit_list_checker btl alive tbl IN Some tt @@ -273,34 +273,110 @@ Variable prog: BTL.program. Let ge := Genv.globalenv prog. -Hypothesis all_liveness_checker: forall b f, Genv.find_funct_ptr ge b = Some f -> liveness_ok_fundef f. +Hypothesis all_fundef_liveness_ok: 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. - -(*Lemma tr_inputs_eqlive f rs1 rs2 tbl or r - (REGS: forall r, eqlive_reg (ext (input_regs ibf)) rs1 rs2) +(* +Lemma tr_inputs_eqlive f rs1 rs2 tbl or r + forall r, eqlive_reg (ext (input_regs ibf)) rs1 rs2) :eqlive_reg (tr_inputs f tbl or rs1) (tid f tbl or rs2). +REGS' : forall v : val, + eqlive_reg (ext (input_regs ibf)) rs1 # res <- v rs2 # res <- v +forall v : val, +eqlive_reg (ext (input_regs ibf)) + (tid f tbl or rs1) # res <- v + (tr_inputs f tbl or rs2) # res <- v + + Proof. unfold tid; rewrite tr_inputs_get. autodestruct. - Qed.*) +Qed. + *) +Lemma find_funct_liveness_ok v fd: + Genv.find_funct ge v = Some fd -> liveness_ok_fundef fd. +Proof. + unfold Genv.find_funct. + destruct v; try congruence. + destruct (Integers.Ptrofs.eq_dec _ _); try congruence. + eapply all_fundef_liveness_ok; eauto. +Qed. + +Lemma find_function_liveness_ok ros rs f: + find_function ge ros rs = Some f -> liveness_ok_fundef f. +Proof. + destruct ros as [r|i]; simpl. + - intros; eapply find_funct_liveness_ok; eauto. + - destruct (Genv.find_symbol ge i); try congruence. + eapply all_fundef_liveness_ok; eauto. +Qed. -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) +Lemma find_function_eqlive alive ros rs1 rs2: + eqlive_reg (ext alive) rs1 rs2 -> + reg_sum_mem ros alive = true -> + find_function ge ros rs1 = find_function ge ros rs2. +Proof. + intros EQLIVE. + destruct ros; simpl; auto. + intros H; erewrite (EQLIVE r); eauto. +Qed. + +Lemma exit_checker_eqlive_ext1 (btl: code) (alive: Regset.t) (pc: node) r rs1 rs2: + exit_checker btl (Regset.add r alive) pc = Some tt -> + eqlive_reg (ext alive) rs1 rs2 -> + exists ibf, btl!pc = Some ibf /\ (forall v, eqlive_reg (ext ibf.(input_regs)) (rs1 # r <- v) (rs2 # r <- v)). +Proof. + unfold exit_checker. + inversion_SOME next. + inversion_ASSERT. try_simplify_someHyps. + repeat (econstructor; eauto). + intros; eapply eqlive_reg_update; eauto. + eapply eqlive_reg_monotonic; eauto. + intros r0 [X1 X2]; exploit Regset.subset_2; eauto. + rewrite regset_add_spec. intuition subst. +Qed. + +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) (LIVE: liveness_ok_function f) + (REGS: eqlive_reg (ext alive) rs1 rs2) + (FCHK: final_inst_checker (fn_code f) alive fin = Some tt) (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. + :exists s', + final_step tr_inputs ge stk2 f sp rs2 m fin t s' + /\ eqlive_states s s'. Proof. - destruct FSTEP. + destruct FSTEP; try_simplify_someHyps; repeat inversion_ASSERT; intros. - (* Bgoto *) econstructor. econstructor. econstructor. econstructor. eauto. eauto. repeat econstructor; eauto. + all: admit. + - (* Breturn *) + eexists; split. econstructor; eauto. + destruct or; simpl in *; + try erewrite (REGS r); eauto. + - (* Bcall *) + exploit exit_checker_eqlive_ext1; eauto. + intros (ibf & PC & REGS'). + eexists; split. + + econstructor; eauto. + erewrite <- find_function_eqlive; eauto. + + erewrite eqlive_reg_listmem; eauto. + eapply eqlive_states_call; eauto. + eapply find_function_liveness_ok; eauto. + repeat (econstructor; eauto). + admit. + - (* Btailcall *) + eexists; split. + + econstructor; eauto. + erewrite <- find_function_eqlive; eauto. + + erewrite eqlive_reg_listmem; eauto. + eapply eqlive_states_call; eauto. + eapply find_function_liveness_ok; eauto. + - (* Bbuiltin *) + Admitted. Lemma cfgsem2fsem_ibistep_simu_None sp f ib: forall rs1 m rs1' m' @@ -363,6 +439,7 @@ Lemma cfgsem2fsem_ibistep_simu_Some sp f stk1 stk2 ib: forall s t rs1 m rs1' m' 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) + (*(PC : (fn_code f) ! pc = Some ibf)*) (STACKS: list_forall2 eqlive_stackframes stk1 stk2), exists rs2' s', iblock_istep_run ge sp ib rs2 m = Some (out rs2' m' (Some fin)) @@ -372,8 +449,10 @@ Proof. induction ib; simpl; try_simplify_someHyps; repeat inversion_ASSERT; intros; inv ISTEP. - (* BF *) - exploit cfgsem2fsem_finalstep_simu; eauto. - intros (s2 & FSTEP' & STATES). eauto. + generalize BDY; clear BDY. + inversion_SOME x; try_simplify_someHyps; intros FCHK. + destruct x; 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. -- cgit