From c918205205fd0883850308c9598ab2e221bdff7b Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 7 Jun 2021 10:48:54 +0200 Subject: advance for tr_input proof --- scheduling/BTL_Livecheck.v | 195 +++++++++++++++++++++++++++++++++++++++------ 1 file changed, 171 insertions(+), 24 deletions(-) (limited to 'scheduling/BTL_Livecheck.v') diff --git a/scheduling/BTL_Livecheck.v b/scheduling/BTL_Livecheck.v index 8d613ef8..3882639c 100644 --- a/scheduling/BTL_Livecheck.v +++ b/scheduling/BTL_Livecheck.v @@ -276,23 +276,50 @@ Let ge := Genv.globalenv prog. 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 - 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 - +Lemma tr_inputs_eqlive_None f pc 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). +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 -> + rs1 # r = rs2 # r. +Proof. + intros v REGS NRES INR. unfold eqlive_reg in REGS. + specialize REGS with r. apply REGS in INR. + 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. - unfold tid; rewrite tr_inputs_get. - autodestruct. + 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. @@ -321,7 +348,34 @@ Proof. intros H; erewrite (EQLIVE r); eauto. Qed. -Lemma exit_checker_eqlive_ext1 (btl: code) (alive: Regset.t) (pc: node) r rs1 rs2: +Lemma exit_checker_eqlive (btl: code) (alive: Regset.t) (pc: node) rs1 rs2: + exit_checker btl alive pc = Some tt -> + eqlive_reg (ext alive) rs1 rs2 -> + exists ibf, btl!pc = Some ibf /\ eqlive_reg (ext ibf.(input_regs)) rs1 rs2. +Proof. + unfold exit_checker. + inversion_SOME next. + inversion_ASSERT. try_simplify_someHyps. + repeat (econstructor; eauto). + intros; eapply eqlive_reg_monotonic; eauto. + intros; exploit Regset.subset_2; eauto. +Qed. + +Lemma exit_list_checker_eqlive (btl: code) (alive: Regset.t) (tbl: list node) rs1 rs2 pc: forall n, + exit_list_checker btl alive tbl = true -> + eqlive_reg (ext alive) rs1 rs2 -> + list_nth_z tbl n = Some pc -> + exists ibf, btl!pc = Some ibf /\ eqlive_reg (ext ibf.(input_regs)) rs1 rs2. +Proof. + induction tbl; simpl. + - intros; try congruence. + - intros n; rewrite lazy_and_Some_tt_true; destruct (zeq n 0) eqn: Hn. + * try_simplify_someHyps; intuition. + exploit exit_checker_eqlive; eauto. + * intuition. eapply IHtbl; eauto. +Qed. + +Lemma exit_checker_eqlive_update (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)). @@ -336,6 +390,56 @@ Proof. rewrite regset_add_spec. intuition subst. Qed. +Lemma exit_checker_eqlive_builtin_res (btl: code) (alive: Regset.t) (pc: node) rs1 rs2 (res:builtin_res reg): + exit_checker btl (reg_builtin_res res alive) pc = Some tt -> + eqlive_reg (ext alive) rs1 rs2 -> + exists ibf, btl!pc = Some ibf /\ (forall vres, eqlive_reg (ext ibf.(input_regs)) (regmap_setres res vres rs1) (regmap_setres res vres rs2)). +Proof. + destruct res; simpl. + - intros; exploit exit_checker_eqlive_update; eauto. + - intros; exploit exit_checker_eqlive; eauto. + intros (ibf & PC & REGS). + eexists; intuition eauto. + - intros; exploit exit_checker_eqlive; eauto. + intros (ibf & PC & REGS). + eexists; intuition eauto. +Qed. + +Local Hint Resolve in_or_app: local. +Lemma eqlive_eval_builtin_args alive rs1 rs2 sp m args vargs: + eqlive_reg alive rs1 rs2 -> + Events.eval_builtin_args ge (fun r => rs1 # r) sp m args vargs -> + (forall r, List.In r (params_of_builtin_args args) -> alive r) -> + Events.eval_builtin_args ge (fun r => rs2 # r) sp m args vargs. +Proof. + unfold Events.eval_builtin_args. + intros EQLIVE; induction 1 as [|a1 al b1 bl EVAL1 EVALL]; simpl. + { econstructor; eauto. } + intro X. + assert (X1: eqlive_reg (fun r => In r (params_of_builtin_arg a1)) rs1 rs2). + { eapply eqlive_reg_monotonic; eauto with local. } + lapply IHEVALL; eauto with local. + clear X IHEVALL; intro X. econstructor; eauto. + generalize X1; clear EVALL X1 X. + induction EVAL1; simpl; try (econstructor; eauto; fail). + - intros X1; erewrite X1; [ econstructor; eauto | eauto ]. + - intros; econstructor. + + eapply IHEVAL1_1; eauto. + eapply eqlive_reg_monotonic; eauto. + simpl; intros; eauto with local. + + eapply IHEVAL1_2; eauto. + eapply eqlive_reg_monotonic; eauto. + simpl; intros; eauto with local. + - intros; econstructor. + + eapply IHEVAL1_1; eauto. + eapply eqlive_reg_monotonic; eauto. + simpl; intros; eauto with local. + + eapply IHEVAL1_2; eauto. + eapply eqlive_reg_monotonic; eauto. + simpl; intros; eauto with local. +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) (LIVE: liveness_ok_function f) @@ -348,17 +452,17 @@ Lemma cfgsem2fsem_finalstep_simu sp f stk1 stk2 s t fin alive rs1 m rs2 Proof. destruct FSTEP; try_simplify_someHyps; repeat inversion_ASSERT; intros. - (* Bgoto *) - econstructor. econstructor. - econstructor. econstructor. - eauto. eauto. - repeat econstructor; eauto. - all: admit. + eexists; split. + + econstructor; eauto. + + exploit exit_checker_eqlive; eauto. + intros (ibf & PC & REGS'). + econstructor; eauto. - (* Breturn *) eexists; split. econstructor; eauto. destruct or; simpl in *; try erewrite (REGS r); eauto. - (* Bcall *) - exploit exit_checker_eqlive_ext1; eauto. + exploit exit_checker_eqlive_update; eauto. intros (ibf & PC & REGS'). eexists; split. + econstructor; eauto. @@ -366,8 +470,6 @@ Proof. + 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. @@ -376,7 +478,52 @@ Proof. eapply eqlive_states_call; eauto. eapply find_function_liveness_ok; eauto. - (* Bbuiltin *) - + exploit exit_checker_eqlive_builtin_res; eauto. + intros (ibf & PC & REGS'). + eexists; split. + + econstructor; eauto. + eapply eqlive_eval_builtin_args; eauto. + intros; eapply list_mem_correct; eauto. + + repeat (econstructor; simpl; eauto). + unfold regmap_setres. destruct res; simpl in *; eauto. + - (* Bjumptable *) + exploit exit_list_checker_eqlive; eauto. + intros (ibf & PC & REGS'). + eexists; split. + + econstructor; eauto. + 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. Lemma cfgsem2fsem_ibistep_simu_None sp f ib: forall rs1 m rs1' m' -- cgit