From 86e108c7b95456e986605cb1861cb5128f348ec0 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 18 Jun 2021 11:08:52 +0200 Subject: End of main scheduling proof --- scheduling/BTL_Scheduler.v | 1 + scheduling/BTL_Schedulerproof.v | 139 ++++++++++++++++++++++++---------------- scheduling/RTLtoBTLproof.v | 9 ++- 3 files changed, 90 insertions(+), 59 deletions(-) (limited to 'scheduling') diff --git a/scheduling/BTL_Scheduler.v b/scheduling/BTL_Scheduler.v index 10f780e2..c50eb364 100644 --- a/scheduling/BTL_Scheduler.v +++ b/scheduling/BTL_Scheduler.v @@ -52,6 +52,7 @@ Definition check_symbolic_simu (f tf: BTL.function): res unit := OK tt. (* TODO: Lemma check_symbolic_simu_input_equiv x f1 f2: check_symbolic_simu f1 f2 = OK x -> equiv_input_regs f1 f2. +Proof. Admitted. Lemma check_symbolic_simu_correct x f1 f2: diff --git a/scheduling/BTL_Schedulerproof.v b/scheduling/BTL_Schedulerproof.v index 85b185c5..6963ee8b 100644 --- a/scheduling/BTL_Schedulerproof.v +++ b/scheduling/BTL_Schedulerproof.v @@ -105,6 +105,11 @@ Qed. Lemma transf_fundef_correct f f': transf_fundef f = OK f' -> match_fundef f f'. Proof. + intros TRANSF; destruct f; simpl. monadInv TRANSF. + + exploit transf_function_correct; eauto. + (*intros (dupmap & MATCH_F).*) + (*eapply match_Internal; eauto.*) + (*+ eapply match_External.*) Admitted. Lemma function_ptr_preserved: @@ -196,58 +201,79 @@ Theorem symbolic_simu_ssem stk1 stk2 st st' s t: /\ match_states s s'. Proof. intros SIMU SST1 STACKS MF. inversion MF. - (*destruct SST1.*) - (*- [> sem_Sfinal <]*) - (*admit.*) - (*- [> sem_Scond <]*) - exploit sem_sstate_run; eauto. intros (sis1 & sfv1 & rs' & m' & SOUT1 & SIS1 & SF). exploit sem_si_ok; eauto. intros SOK. - exploit SIMU; simpl; eauto. (* rewrite SEVAL; eauto. *) + exploit SIMU; simpl; eauto. intros (sis2 & sfv2 & SOUT2 & SSIMU & SFVSIM). remember SIS1 as EQSFV. clear HeqEQSFV. eapply SFVSIM in EQSFV. - - - exploit SSIMU; eauto. - intros SIS2. - - - + exploit SSIMU; eauto. intros SIS2. destruct SIS1 as (PRE1 & SMEM1 & SREGS1). try_simplify_someHyps; intros. - (*exploit sem_sfval_equiv; eauto.*) - (*intros (s' & SF' & EQUIV).*) set (EQSFV2:=sfv2). - inversion EQSFV; subst. - - - inversion SF; subst. - exploit (run_sem_sstate (bctx2 ctx) st' sis2 EQSFV2); eauto. - + erewrite <- str_regs_equiv; simpl; eauto. - + econstructor. - + intros SST2. eexists; split; eauto. - econstructor; simpl; eauto. - erewrite equiv_input_regs_tr_inputs; eauto. - - - - inversion SF; subst. - exploit sfind_function_preserved; eauto. intros (fd' & SFIND & FUND). - exploit (run_sem_sstate (bctx2 ctx) st' sis2 EQSFV2); eauto. - + erewrite <- str_regs_equiv; eauto. - + econstructor; eauto. - * apply function_sig_translated; auto. - * erewrite <- ARGS; eauto. - + intros SST2. eexists; split; eauto. - econstructor; simpl; eauto. - * erewrite equiv_input_regs_tr_inputs; eauto. - repeat (econstructor; eauto). - * apply transf_fundef_correct; auto. - - - - -admit. -Admitted. + inversion EQSFV; subst; inversion SF; subst. + - (* goto *) + exploit (run_sem_sstate (bctx2 ctx) st' sis2 EQSFV2); eauto. + + erewrite <- str_regs_equiv; simpl; eauto. + + econstructor. + + intros SST2. eexists; split; eauto. + econstructor; simpl; eauto. + erewrite equiv_input_regs_tr_inputs; eauto. + - (* call *) + exploit sfind_function_preserved; eauto. intros (fd' & SFIND & FUND). + exploit (run_sem_sstate (bctx2 ctx) st' sis2 EQSFV2); eauto. + + erewrite <- str_regs_equiv; eauto. + + econstructor; eauto. + * apply function_sig_translated; auto. + * erewrite <- ARGS; eauto. + + intros SST2. eexists; split; eauto. + econstructor; simpl; eauto. + * erewrite equiv_input_regs_tr_inputs; eauto. + repeat (econstructor; eauto). + * apply transf_fundef_correct; auto. + - (* tailcall *) + exploit sfind_function_preserved; eauto. intros (fd' & SFIND & FUND). + exploit (run_sem_sstate (bctx2 ctx) st' sis2 EQSFV2); eauto. + + econstructor; eauto. + * apply function_sig_translated; auto. + * simpl; erewrite <- preserv_fnstacksize; eauto. + * erewrite <- ARGS; eauto. + + intros SST2. eexists; split; eauto. + econstructor; simpl; eauto. + apply transf_fundef_correct; auto. + - (* builtin *) + exploit (run_sem_sstate (bctx2 ctx) st' sis2 EQSFV2); eauto. + + erewrite <- str_regs_equiv; simpl; eauto. + + econstructor. + * eapply eval_builtin_sargs_preserved. + eapply senv_preserved. + eapply eval_list_builtin_sval_correct; eauto. + inv BARGS. + erewrite <- eval_list_builtin_sval_preserved in H0; auto. + * simpl in *; eapply external_call_symbols_preserved; eauto. + eapply senv_preserved. + + intros SST2. eexists; split; eauto. + econstructor; simpl; eauto. + erewrite equiv_input_regs_tr_inputs; eauto. + - (* jumptable *) + exploit (run_sem_sstate (bctx2 ctx) st' sis2 EQSFV2); eauto. + + erewrite <- str_regs_equiv; simpl; eauto. + + econstructor; eauto. + rewrite <- VAL; auto. + + intros SST2. eexists; split; eauto. + econstructor; simpl; eauto. + erewrite equiv_input_regs_tr_inputs; eauto. + - (* return *) + exploit (run_sem_sstate (bctx2 ctx) st' sis2 EQSFV2); eauto. + + econstructor; eauto. + * simpl; erewrite <- preserv_fnstacksize; eauto. + * inv OPT; eauto. + rewrite <- SIMU0; auto. + + intros SST2. eexists; split; eauto. + econstructor; simpl; eauto. + Unshelve. all: auto. +Qed. Theorem symbolic_simu_correct stk1 stk2 ibf1 ibf2 s t: sstate_simu ctx (sexec f1 ibf1.(entry)) (sexec f2 ibf2.(entry)) -> @@ -269,17 +295,21 @@ Proof. eapply match_states_equiv; eauto. Qed. -Lemma iblock_step_eqregs tr ge stk f sp ib: - forall rs m rs' t s, - (forall r, rs # r = rs' # r) -> - iblock_step tr ge stk f sp rs m ib t s <-> - iblock_step tr ge stk f sp rs' m ib t s. +End SYMBOLIC_CTX. + +Lemma iblock_step_eqregs sp ib: + forall rs rs' + (EQREGS: forall r, rs # r = rs' # r) + fin m rs2 m2 (ISTEP: iblock_istep tpge sp rs m ib rs2 m2 (Some fin)), + iblock_istep tpge sp rs' m ib rs2 m2 (Some fin). Proof. - induction ib; try_simplify_someHyps. + induction ib; intros; inv ISTEP. + - + admit. + - econstructor; eauto. + - econstructor. eapply IHib1; eauto. Admitted. -End SYMBOLIC_CTX. - Lemma iblock_step_simulation stk1 stk2 f1 f2 sp rs rs' m ibf t s pc (STEP: iblock_step tr_inputs pge stk1 f1 sp rs m ibf.(entry) t s) (PC: (fn_code f1) ! pc = Some ibf) @@ -291,12 +321,13 @@ Lemma iblock_step_simulation stk1 stk2 f1 f2 sp rs rs' m ibf t s pc /\ iblock_step tr_inputs tpge stk2 f2 sp rs' m ibf'.(entry) t s' /\ match_states s s'. Proof. - (*destruct STEP as (rs1 & m1 & fin & ISTEP & FSTEP).*) exploit symbolic_simu_ok; eauto. intros (ib2 & PC' & SYMBS). exploit symbolic_simu_correct; repeat (eauto; simpl). intros (s' & STEP2 & MS). - exists ib2; exists s'; repeat split; auto. - erewrite iblock_step_eqregs; eauto. + exists ib2; exists s'. repeat split; auto. + destruct STEP2 as (rs2 & m2 & fin & ISTEP2 & FSTEP2). + unfold iblock_step. exists rs2; exists m2; exists fin. + split; auto. Admitted. Local Hint Constructors step: core. diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index f5c2f3db..4af5668c 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -252,11 +252,10 @@ Lemma transf_function_correct f f': transf_function f = OK f' -> exists dupmap, match_function dupmap f f'. Proof. unfold transf_function; unfold bind. repeat autodestruct. - intros H _ _ X. inversion X; subst; clear X. -(* - eexists; eapply verify_function_correct; simpl; eauto. -*) -Admitted. + intros LIVE VER _ _ X. inv X. eexists; econstructor. + - eapply verify_function_correct; simpl; eauto. + - unfold liveness_ok_function; destruct u0; auto. +Qed. Lemma transf_fundef_correct f f': transf_fundef f = OK f' -> match_fundef f f'. -- cgit