From 80ae2a92d6c3215beec912d30b60ae6343222706 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 12 Feb 2021 16:45:18 +0100 Subject: [Broken version] Intermediate local commit: proof of inst_checker_eqlive OK --- scheduling/RTLpathLivegen.v | 84 ++++++++++++++++++++++----------------------- 1 file changed, 41 insertions(+), 43 deletions(-) (limited to 'scheduling/RTLpathLivegen.v') diff --git a/scheduling/RTLpathLivegen.v b/scheduling/RTLpathLivegen.v index 7449dcc6..91c8e790 100644 --- a/scheduling/RTLpathLivegen.v +++ b/scheduling/RTLpathLivegen.v @@ -152,7 +152,7 @@ Qed. Local Hint Resolve exit_list_checker_correct: core. -Definition final_inst_checker (pm: path_map) (alive: Regset.t) (i: instruction): option unit := +(* TODO REMOVE (REPLACED) 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 @@ -173,47 +173,7 @@ Definition final_inst_checker (pm: path_map) (alive: Regset.t) (i: instruction): ASSERT (reg_option_mem optarg) alive IN Some tt | _ => None - end. - -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). -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 := - 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) i. - -(* TODO: replace the implementation of [path_checker] above by this one in order to check [path.(pre_output_regs)] + end.*) Definition final_inst_checker (pm: path_map) (alive por: Regset.t) (i: instruction): option unit := match i with @@ -238,6 +198,24 @@ Definition final_inst_checker (pm: path_map) (alive por: Regset.t) (i: instructi | _ => None end. +Lemma final_inst_checker_wellformed (c:code) pc (pm: path_map) (alive por: Regset.t) (i: instruction): + final_inst_checker pm alive por 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). +Qed. + +(* TODO (REPLACED) 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.*) + Definition inst_checker (pm: path_map) (alive por: Regset.t) (i: instruction): option unit := match iinst_checker pm alive i with | Some res => @@ -248,11 +226,31 @@ Definition inst_checker (pm: path_map) (alive por: Regset.t) (i: instruction): o final_inst_checker pm alive por i end. +Lemma inst_checker_wellformed (c:code) pc (pm: path_map) (alive por: Regset.t) (i: instruction): + inst_checker pm alive por 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. + - simpl; intros CHECK2 PC. eapply final_inst_checker_wellformed; eauto. + generalize CHECK2. clear CHECK2. inversion_ASSERT. try_simplify_someHyps. +Qed. + +(* TODO (REPLACED) 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) i. *) + 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. -- cgit