From ee558407e59c6794daad70aab2e1e7794535367e Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 17 May 2021 19:12:46 +0200 Subject: finishing RTLtoBTL --- scheduling/RTLtoBTLproof.v | 57 +++++++++++++++++++++++++++------------------- 1 file changed, 34 insertions(+), 23 deletions(-) (limited to 'scheduling/RTLtoBTLproof.v') diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index faf0b76c..633e1b8e 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -9,7 +9,6 @@ Require Import Linking. Record match_function dupmap (f:RTL.function) (tf: BTL.function): Prop := { dupmap_correct: match_cfg dupmap (fn_code tf) (RTL.fn_code f); dupmap_entrypoint: dupmap!(fn_entrypoint tf) = Some (RTL.fn_entrypoint f); - code_expand: forall pc ib, (fn_code tf)!pc=Some ib -> is_expand ib.(entry); preserv_fnsig: fn_sig tf = RTL.fn_sig f; preserv_fnparams: fn_params tf = RTL.fn_params f; preserv_fnstacksize: fn_stacksize tf = RTL.fn_stacksize f @@ -31,7 +30,6 @@ Lemma verify_function_correct dupmap f f' tt: fn_sig f' = RTL.fn_sig f -> fn_params f' = RTL.fn_params f -> fn_stacksize f' = RTL.fn_stacksize f -> - (forall pc ib, (fn_code f')!pc=Some ib -> is_expand ib.(entry)) -> match_function dupmap f f'. Proof. unfold verify_function; intro VERIF. monadInv VERIF. @@ -46,7 +44,6 @@ Proof. unfold transf_function; unfold bind. repeat autodestruct. intros H _ _ X. inversion X; subst; clear X. eexists; eapply verify_function_correct; simpl; eauto. - eapply expand_code_correct; eauto. Qed. Lemma transf_fundef_correct f f': @@ -243,6 +240,18 @@ Proof. destruct fi; trivial. inv H. inv H4. Qed. +Lemma expand_entry_isnt_goto dupmap f pc ib: + match_iblock dupmap (RTL.fn_code f) true pc (expand (entry ib) None) None -> + is_goto (expand (entry ib) None) = false. +Proof. + destruct (is_goto (expand (entry ib) None))eqn:EQG. + - destruct (expand (entry ib) None); + try destruct fi; try discriminate; trivial. + intros; inv H; inv H4. + - destruct (expand (entry ib) None); + try destruct fi; try discriminate; trivial. +Qed. + Lemma list_nth_z_rev_dupmap: forall dupmap ln ln' (pc pc': node) val, list_nth_z ln val = Some pc -> @@ -498,10 +507,10 @@ Proof. eexists; left; eexists; split. + repeat econstructor; eauto. apply iblock_istep_run_equiv in BTL_RUN; eauto. - + econstructor. econstructor; eauto. - eapply code_expand; eauto. - econstructor. - eapply entry_isnt_goto; eauto. + + econstructor; apply expand_matchiblock_correct in MI. + econstructor; eauto. apply expand_correct; trivial. + econstructor. apply expand_preserves_iblock_istep_run. + eapply expand_entry_isnt_goto; eauto. - (* Others *) exists (Some ib2); right; split. simpl; auto. @@ -566,11 +575,10 @@ Proof. pose symbols_preserved as SYMPRES. eapply eval_builtin_args_preserved; eauto. eapply external_call_symbols_preserved; eauto. eapply senv_preserved. - * econstructor; eauto. - { econstructor; eauto. eapply code_expand; eauto. - apply star_refl. } - inversion MI; subst; try_simplify_someHyps. - inv H3; try_simplify_someHyps. + * econstructor; eauto; apply expand_matchiblock_correct in MI. + { econstructor; eauto. apply expand_correct; trivial. + apply star_refl. apply expand_preserves_iblock_istep_run. } + eapply expand_entry_isnt_goto; eauto. + (* Bjumptable *) exploit list_nth_z_rev_dupmap; eauto. intros (pc'0 & LNZ & DM). @@ -582,11 +590,10 @@ Proof. eexists; eexists; split. eapply iblock_istep_run_equiv in BTL_RUN. eapply BTL_RUN. econstructor; eauto. - * econstructor; eauto. - { econstructor; eauto. eapply code_expand; eauto. - apply star_refl. } - inversion MI; subst; try_simplify_someHyps. - inv H4; try_simplify_someHyps. + * econstructor; eauto; apply expand_matchiblock_correct in MI. + { econstructor; eauto. apply expand_correct; trivial. + apply star_refl. apply expand_preserves_iblock_istep_run. } + eapply expand_entry_isnt_goto; eauto. - (* mib_exit *) discriminate. - (* mib_seq *) @@ -689,11 +696,13 @@ Proof. eexists; left; eexists; split. * eapply exec_function_internal. erewrite preserv_fnstacksize; eauto. - * econstructor. econstructor; eauto. - eapply code_expand; eauto. - 3: eapply entry_isnt_goto; eauto. + * apply expand_matchiblock_correct in MI. + econstructor. econstructor; eauto. + apply expand_correct; trivial. + 3: eapply expand_entry_isnt_goto; eauto. all: erewrite preserv_fnparams; eauto. constructor. + apply expand_preserves_iblock_istep_run. + (* External function *) inv TRANSF. eexists; left; eexists; split. @@ -708,9 +717,11 @@ Proof. apply DMC in DUPLIC as [ib [FNC MI]]; clear DMC. eexists; left; eexists; split. + eapply exec_return. - + econstructor. econstructor; eauto. - eapply code_expand; eauto. - constructor. eapply entry_isnt_goto; eauto. + + apply expand_matchiblock_correct in MI. + econstructor. econstructor; eauto. + apply expand_correct; trivial. + constructor. apply expand_preserves_iblock_istep_run. + eapply expand_entry_isnt_goto; eauto. Qed. Local Hint Resolve plus_one star_refl: core. -- cgit