From a918b4e3b646aa24e413863455301d498f1742a3 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Thu, 11 Feb 2021 09:47:46 +0100 Subject: refactorize inst_checker for checking pre_output_regs --- scheduling/RTLpathLivegen.v | 56 +++++++++++++++++++++++++----- scheduling/RTLpathLivegenproof.v | 73 ++++++++++++++++++++++++++++------------ 2 files changed, 98 insertions(+), 31 deletions(-) diff --git a/scheduling/RTLpathLivegen.v b/scheduling/RTLpathLivegen.v index 1f0ebe3c..f3ae29cf 100644 --- a/scheduling/RTLpathLivegen.v +++ b/scheduling/RTLpathLivegen.v @@ -152,7 +152,7 @@ Qed. Local Hint Resolve exit_list_checker_correct: core. -Definition inst_checker (pm: path_map) (alive: Regset.t) (i: instruction): option unit := +Definition final_inst_checker (pm: path_map) (alive: Regset.t) (i: instruction): option unit := match i with | Icall sig ros args res pc' => ASSERT list_mem args alive IN @@ -170,23 +170,43 @@ Definition inst_checker (pm: path_map) (alive: Regset.t) (i: instruction): optio ASSERT exit_list_checker pm alive tbl IN Some tt | Ireturn optarg => - ASSERT (reg_option_mem optarg) alive IN + ASSERT (reg_option_mem optarg) alive IN Some tt - | _ => - SOME res <- iinst_checker pm alive i IN - exit_checker pm (fst res) (snd res) tt + | _ => None end. -Lemma inst_checker_wellformed (c:code) pc (pm: path_map) (alive: Regset.t) (i: instruction): - inst_checker pm alive i = Some tt -> +Lemma final_inst_checker_wellformed (c:code) pc (pm: path_map) (alive: Regset.t) (i: instruction): + final_inst_checker pm alive i = Some tt -> c!pc = Some i -> wellformed_path c pm 0 pc. Proof. intros CHECK PC. eapply wf_last_node; eauto. clear c pc PC. intros pc PC. destruct i; simpl in * |- *; intuition (subst; eauto); try (generalize CHECK; clear CHECK; try (inversion_SOME path); repeat inversion_ASSERT; try_simplify_someHyps). - intros X; exploit exit_checker_res; eauto. - clear X. intros; subst; eauto. +Qed. + + +Definition inst_checker (pm: path_map) (alive: Regset.t) (i: instruction): option unit := + match iinst_checker pm alive i with + | Some res => + exit_checker pm (fst res) (snd res) tt + | _ => + final_inst_checker pm alive i + end. + +Lemma inst_checker_wellformed (c:code) pc (pm: path_map) (alive: Regset.t) (i: instruction): + inst_checker pm alive i = Some tt -> + c!pc = Some i -> wellformed_path c pm 0 pc. +Proof. + unfold inst_checker. + destruct (iinst_checker pm alive i) as [[alive0 pc0]|] eqn: CHECK1; simpl. + - simpl; intros CHECK2 PC. eapply wf_last_node; eauto. + destruct i; simpl in * |- *; intuition (subst; eauto); + try (generalize CHECK2 CHECK1; clear CHECK1 CHECK2; try (inversion_SOME path); repeat inversion_ASSERT; try_simplify_someHyps). + intros PC CHECK1 CHECK2. + intros; exploit exit_checker_res; eauto. + intros X; inversion X. intros; subst; eauto. + - eapply final_inst_checker_wellformed. Qed. Definition path_checker (f: RTL.function) pm (pc: node) (path:path_info): option unit := @@ -194,6 +214,24 @@ Definition path_checker (f: RTL.function) pm (pc: node) (path:path_info): option SOME i <- f.(fn_code)!(snd res) IN inst_checker pm (fst res) i. +(* TODO: replace the implementation of [path_checker] above by this one in order to check [path.(pre_output_regs)] + +Definition inst_checker (pm: path_map) (alive por: Regset.t) (i: instruction): option unit := + match iinst_checker pm alive i with + | Some res => + ASSERT Regset.subset por (fst res) IN + exit_checker pm por (snd res) tt + | _ => + ASSERT Regset.subset por alive IN + final_inst_checker pm por i + end. + +Definition path_checker (f: RTL.function) pm (pc: node) (path:path_info): option unit := + SOME res <- ipath_checker (path.(psize)) f pm (path.(input_regs)) pc IN + SOME i <- f.(fn_code)!(snd res) IN + inst_checker pm (fst res) (path.(pre_output_regs)) i. +*) + Lemma path_checker_wellformed f pm pc path: path_checker f pm pc path = Some tt -> wellformed_path (f.(fn_code)) pm (path.(psize)) pc. Proof. diff --git a/scheduling/RTLpathLivegenproof.v b/scheduling/RTLpathLivegenproof.v index c6125985..26a1a50a 100644 --- a/scheduling/RTLpathLivegenproof.v +++ b/scheduling/RTLpathLivegenproof.v @@ -501,12 +501,23 @@ Proof. intros H; erewrite (EQLIVE r); eauto. Qed. +Lemma final_inst_checker_from_iinst_checker i sp rs m st pm alive: + istep ge i sp rs m = Some st -> + final_inst_checker pm alive i = None. +Proof. + destruct i; simpl; try congruence. +Qed. + +(* is it useful ? Lemma inst_checker_from_iinst_checker i sp rs m st pm alive: istep ge i sp rs m = Some st -> inst_checker pm alive i = (SOME res <- iinst_checker pm alive i IN exit_checker pm (fst res) (snd res) tt). Proof. - destruct i; simpl; try congruence. + unfold inst_checker. + destruct (iinst_checker pm alive i); simpl; auto. + destruct i; simpl; try congruence. Qed. +*) Lemma exit_checker_eqlive_ext1 (pm: path_map) (alive: Regset.t) (pc: node) r rs1 rs2: exit_checker pm (Regset.add r alive) pc tt = Some tt -> @@ -586,13 +597,13 @@ Proof. * intuition. eapply IHtbl; eauto. Qed. -Lemma inst_checker_eqlive (f: function) sp alive pc i rs1 rs2 m stk1 stk2 t s1: +Lemma final_inst_checker_eqlive (f: function) sp alive pc i rs1 rs2 m stk1 stk2 t s1: list_forall2 eqlive_stackframes stk1 stk2 -> eqlive_reg (ext alive) rs1 rs2 -> liveness_ok_function f -> (fn_code f) ! pc = Some i -> path_last_step ge pge stk1 f sp pc rs1 m t s1 -> - inst_checker (fn_path f) alive i = Some tt -> + final_inst_checker (fn_path f) alive i = Some tt -> exists s2, path_last_step ge pge stk2 f sp pc rs2 m t s2 /\ eqlive_states s1 s2. Proof. intros STACKS EQLIVE LIVENESS PC; @@ -604,25 +615,8 @@ Proof. st1 pc rs1 m optr m']; try_simplify_someHyps. + (* istate *) - intros PC ISTEP. erewrite inst_checker_from_iinst_checker; eauto. - inversion_SOME res. - intros. - destruct (icontinue st1) eqn: CONT. - - (* CONT => true *) - exploit iinst_checker_eqlive; eauto. - destruct 1 as (st2 & ISTEP2 & [CONT' PC2 RS MEM]). - repeat (econstructor; simpl; eauto). - rewrite <- MEM, <- PC2. - exploit exit_checker_eqlive; eauto. - intros (path & PATH & EQLIVE2). - eapply eqlive_states_intro; eauto. - erewrite <- iinst_checker_istep_continue; eauto. - - (* CONT => false *) - intros; exploit iinst_checker_eqlive_stopped; eauto. - destruct 1 as (path & st2 & PATH & ISTEP2 & [CONT2 PC2 RS MEM]). - repeat (econstructor; simpl; eauto). - rewrite <- MEM, <- PC2. - eapply eqlive_states_intro; eauto. + intros PC ISTEP. erewrite final_inst_checker_from_iinst_checker; eauto. + congruence. + (* Icall *) repeat inversion_ASSERT. intros. exploit exit_checker_eqlive_ext1; eauto. @@ -669,6 +663,41 @@ Proof. * eapply eqlive_states_return; eauto. Qed. +Lemma inst_checker_eqlive (f: function) sp alive pc i rs1 rs2 m stk1 stk2 t s1: + list_forall2 eqlive_stackframes stk1 stk2 -> + eqlive_reg (ext alive) rs1 rs2 -> + liveness_ok_function f -> + (fn_code f) ! pc = Some i -> + path_last_step ge pge stk1 f sp pc rs1 m t s1 -> + inst_checker (fn_path f) alive i = Some tt -> + exists s2, path_last_step ge pge stk2 f sp pc rs2 m t s2 /\ eqlive_states s1 s2. +Proof. + unfold inst_checker; + intros STACKS EQLIVE LIVENESS PC. + destruct (iinst_checker (fn_path f) alive i) as [res|] eqn: IICHECKER. + + destruct 1 as [i' sp pc rs1 m st1| | | | | ]; + try_simplify_someHyps. + intros PC ISTEP. + intros. + destruct (icontinue st1) eqn: CONT. + - (* CONT => true *) + exploit iinst_checker_eqlive; eauto. + destruct 1 as (st2 & ISTEP2 & [CONT' PC2 RS MEM]). + repeat (econstructor; simpl; eauto). + rewrite <- MEM, <- PC2. + exploit exit_checker_eqlive; eauto. + intros (path & PATH & EQLIVE2). + eapply eqlive_states_intro; eauto. + erewrite <- iinst_checker_istep_continue; eauto. + - (* CONT => false *) + intros; exploit iinst_checker_eqlive_stopped; eauto. + destruct 1 as (path & st2 & PATH & ISTEP2 & [CONT2 PC2 RS MEM]). + repeat (econstructor; simpl; eauto). + rewrite <- MEM, <- PC2. + eapply eqlive_states_intro; eauto. + + intros; exploit final_inst_checker_eqlive; eauto. +Qed. + Lemma path_step_eqlive path stk1 f sp rs1 m pc t s1 stk2 rs2: path_step ge pge (psize path) stk1 f sp rs1 m pc t s1 -> list_forall2 eqlive_stackframes stk1 stk2 -> -- cgit