diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-06-08 11:40:59 +0200 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-06-08 11:40:59 +0200 |
commit | 7aefe9ee6df7632fd97fe61163a53d82a9725ac7 (patch) | |
tree | 08fcec657d77a306920f32199e1e6b17c369a254 /scheduling | |
parent | a7bb27d5125fd2232fa38fe9605c31766a96fa2e (diff) | |
parent | cb167a462bd4e26ae31694ecf48425ad257fb0f3 (diff) | |
download | compcert-kvx-7aefe9ee6df7632fd97fe61163a53d82a9725ac7.tar.gz compcert-kvx-7aefe9ee6df7632fd97fe61163a53d82a9725ac7.zip |
Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into BTL
Diffstat (limited to 'scheduling')
-rw-r--r-- | scheduling/BTL_Livecheck.v | 200 |
1 files changed, 172 insertions, 28 deletions
diff --git a/scheduling/BTL_Livecheck.v b/scheduling/BTL_Livecheck.v index 8d613ef8..25a1c545 100644 --- a/scheduling/BTL_Livecheck.v +++ b/scheduling/BTL_Livecheck.v @@ -276,23 +276,17 @@ 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 - - -Proof. - unfold tid; rewrite tr_inputs_get. - autodestruct. -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 find_funct_liveness_ok v fd: Genv.find_funct ge v = Some fd -> liveness_ok_fundef fd. Proof. @@ -321,7 +315,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 +357,115 @@ 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. + +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 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' & 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 (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. 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 +478,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 +496,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,8 +504,24 @@ Proof. eapply eqlive_states_call; eauto. eapply find_function_liveness_ok; eauto. - (* Bbuiltin *) - -Admitted. + 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). + 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' (ISTEP: iblock_istep ge sp rs1 m ib rs1' m' None) |