From 65a1029a0e2c1b1678e522f485b1e914b6e6d52a Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 7 May 2021 10:31:29 +0200 Subject: proof OK for Call and Return states --- scheduling/RTLtoBTLproof.v | 27 +++++++++++++++++++++------ 1 file changed, 21 insertions(+), 6 deletions(-) (limited to 'scheduling') diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index aac7772c..79b7ca1a 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -252,10 +252,11 @@ Proof. inv H. + (* Internal function *) inv TRANSF. - rename H0 into MF. - eapply dupmap_entrypoint in MF as ENTRY. - eapply dupmap_correct in MF as DMC. unfold match_cfg in DMC. - apply DMC in ENTRY as DMC'. destruct DMC' as [ib [CENTRY MI]]. + rename H0 into TRANSF. + eapply dupmap_entrypoint in TRANSF as ENTRY. + eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC. + apply DMC in ENTRY as DMC'. + destruct DMC' as [ib [CENTRY MI]]; clear DMC. eexists; left; eexists; split. * eapply exec_function_internal. erewrite preserv_fnstacksize; eauto. @@ -264,8 +265,22 @@ Proof. all: erewrite preserv_fnparams; eauto. constructor. + (* External function *) - admit. - - admit. + inv TRANSF. + eexists; left; eexists; split. + * eapply exec_function_external. + eapply external_call_symbols_preserved. + eapply senv_preserved. eauto. + * econstructor; eauto. + - (* Returnstate *) + inv H. inv STACKS. inv H1. + eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC. + remember DUPLIC as ODUPLIC; clear HeqODUPLIC. + apply DMC in DUPLIC as [ib [FNC MI]]; clear DMC. + eexists; left; eexists; split. + + eapply exec_return. + + econstructor; eauto. + eapply code_right_assoc; eauto. + constructor. Admitted. Local Hint Resolve plus_one star_refl: core. -- cgit