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 +++++++++++++++++++++++++++++++++++++-------- 1 file changed, 47 insertions(+), 9 deletions(-) (limited to 'scheduling/RTLpathLivegen.v') 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. -- cgit