From ef95bd7f4afe159bcedc3ec5732579bfc6ba08c6 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Thu, 17 Jun 2021 17:36:42 +0200 Subject: some advance, new section to simplify context from symbolic exec --- scheduling/BTL_Scheduler.v | 12 ++- scheduling/BTL_Schedulerproof.v | 203 ++++++++++++++++++++++++++++------------ scheduling/RTLtoBTLproof.v | 2 +- 3 files changed, 151 insertions(+), 66 deletions(-) (limited to 'scheduling') diff --git a/scheduling/BTL_Scheduler.v b/scheduling/BTL_Scheduler.v index ec83b3c1..10f780e2 100644 --- a/scheduling/BTL_Scheduler.v +++ b/scheduling/BTL_Scheduler.v @@ -9,7 +9,6 @@ Axiom scheduler: BTL.function -> BTL.code. Extract Constant scheduler => "BTLScheduleraux.btl_scheduler". -(* TODO: could be useful ? Definition equiv_input_regs (f1 f2: BTL.function): Prop := (forall pc, (fn_code f1)!pc = None <-> (fn_code f2)!pc = None) /\ (forall pc ib1 ib2, (fn_code f1)!pc = Some ib1 -> (fn_code f2)!pc = Some ib2 -> ib1.(input_regs) = ib2.(input_regs)). @@ -28,8 +27,13 @@ Lemma equiv_input_regs_pre f1 f2 tbl or: Proof. intros; unfold pre_inputs; erewrite equiv_input_regs_union; auto. Qed. -*) +Lemma equiv_input_regs_tr_inputs f1 f2 l oreg rs: + equiv_input_regs f1 f2 -> + tr_inputs f1 l oreg rs = tr_inputs f2 l oreg rs. +Proof. + intros; unfold tr_inputs; erewrite equiv_input_regs_pre; eauto. +Qed. (* a specification of the verification to do on each function *) Record match_function (f1 f2: BTL.function): Prop := { @@ -37,7 +41,7 @@ Record match_function (f1 f2: BTL.function): Prop := { preserv_fnparams: fn_params f1 = fn_params f2; preserv_fnstacksize: fn_stacksize f1 = fn_stacksize f2; preserv_entrypoint: fn_entrypoint f1 = fn_entrypoint f2; - (* preserv_inputs: equiv_input_regs f1 f2; TODO: a-t-on besoin de ça ? *) + preserv_inputs: equiv_input_regs f1 f2; (* TODO: a-t-on besoin de ça ? *) symbolic_simu_ok: forall pc ib1, (fn_code f1)!pc = Some ib1 -> exists ib2, (fn_code f2)!pc = Some ib2 /\ symbolic_simu f1 f2 (entry ib1) (entry ib2); }. @@ -46,11 +50,9 @@ Local Open Scope error_monad_scope. Definition check_symbolic_simu (f tf: BTL.function): res unit := OK tt. (* TODO: fixme *) -(* TODO: a-t-on besoin de ça ? Lemma check_symbolic_simu_input_equiv x f1 f2: check_symbolic_simu f1 f2 = OK x -> equiv_input_regs f1 f2. Admitted. -*) Lemma check_symbolic_simu_correct x f1 f2: check_symbolic_simu f1 f2 = OK x -> diff --git a/scheduling/BTL_Schedulerproof.v b/scheduling/BTL_Schedulerproof.v index c7ecb0dc..85b185c5 100644 --- a/scheduling/BTL_Schedulerproof.v +++ b/scheduling/BTL_Schedulerproof.v @@ -33,6 +33,18 @@ Proof. eapply (Genv.senv_match TRANSL). Qed. +Lemma functions_preserved: + forall (v: val) (f: fundef), + Genv.find_funct pge v = Some f -> + exists tf cunit, transf_fundef f = OK tf /\ Genv.find_funct tpge v = Some tf /\ linkorder cunit prog. +Proof. + intros. exploit (Genv.find_funct_match TRANSL); eauto. + intros (cu & tf & A & B & C). + repeat eexists; intuition eauto. + + unfold incl; auto. + + eapply linkorder_refl. +Qed. + (* TODO gourdinl move this to BTL_Scheduler.v? *) Inductive match_fundef: fundef -> fundef -> Prop := | match_Internal f f': match_function f f' -> match_fundef (Internal f) (Internal f') @@ -85,7 +97,9 @@ Lemma transf_function_correct f f': transf_function f = OK f' -> match_function f f'. Proof. unfold transf_function. intros H. monadInv H. - econstructor; eauto. eapply check_symbolic_simu_correct; eauto. + econstructor; eauto. + eapply check_symbolic_simu_input_equiv; eauto. + eapply check_symbolic_simu_correct; eauto. Qed. Lemma transf_fundef_correct f f': @@ -132,30 +146,122 @@ Proof. intros. inv H0. inv H. inv STACKS. constructor. Qed. -Theorem symbolic_simu_ssem stk1 stk2 f1 f2 ib1 ib2: - forall (ctx: simu_proof_context f1 f2) t s, - sem_sstate (bctx1 ctx) stk1 t s (sexec f1 ib1) -> +Section SYMBOLIC_CTX. + +Variables f1 f2: function. +Variable sp0: val. +Variable rs0: regset. +Variable m0: Memory.Mem.mem. + +Lemma symbols_preserved_rev s: Genv.find_symbol pge s = Genv.find_symbol tpge s. +Proof. + symmetry; apply symbols_preserved. +Qed. + +Let ctx := Sctx f1 f2 pge tpge symbols_preserved_rev sp0 rs0 m0. + +Lemma str_regs_equiv sfv1 sfv2 rs: + sfv_simu ctx sfv1 sfv2 -> + match_function f1 f2 -> + str_regs (cf (bctx1 ctx)) sfv1 rs = str_regs (cf (bctx2 ctx)) sfv2 rs. +Proof. + intros SFV MF; inv MF. + inv SFV; simpl; + erewrite equiv_input_regs_tr_inputs; auto. +Qed. + +Lemma sfind_function_preserved ros1 ros2 fd: + svident_simu ctx ros1 ros2 -> + sfind_function (bctx1 ctx) ros1 = Some fd -> + exists fd', + sfind_function (bctx2 ctx) ros2 = Some fd' + /\ transf_fundef fd = OK fd'. +Proof. + unfold sfind_function. intros [sv1 sv2 SIMU|]; simpl in *. + + rewrite !SIMU. clear SIMU. + destruct (eval_sval _ _); try congruence. + intros; exploit functions_preserved; eauto. + intros (fd' & cunit & (X1 & X2 & X3)). eexists; eauto. + + subst. rewrite symbols_preserved. destruct (Genv.find_symbol _ _); try congruence. + intros; exploit function_ptr_preserved; eauto. +Qed. + +Theorem symbolic_simu_ssem stk1 stk2 st st' s t: + sstate_simu ctx st st' -> + sem_sstate (bctx1 ctx) stk1 t s st -> + list_forall2 match_stackframes stk1 stk2 -> + match_function f1 f2 -> exists s', - sem_sstate (bctx2 ctx) stk2 t s' (sexec f2 ib2) + sem_sstate (bctx2 ctx) stk2 t s' st' /\ 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. *) + intros (sis2 & sfv2 & SOUT2 & SSIMU & SFVSIM). + remember SIS1 as EQSFV. clear HeqEQSFV. + eapply SFVSIM in EQSFV. + + + 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. -Theorem symbolic_simu_correct stk1 stk2 f1 f2 ib1 ib2: - symbolic_simu f1 f2 ib1 ib2 -> - forall (ctx: simu_proof_context f1 f2) t s, iblock_step tr_inputs (sge1 ctx) stk1 f1 (ssp ctx) (srs0 ctx) (sm0 ctx) ib1 t s -> +Theorem symbolic_simu_correct stk1 stk2 ibf1 ibf2 s t: + sstate_simu ctx (sexec f1 ibf1.(entry)) (sexec f2 ibf2.(entry)) -> + iblock_step tr_inputs (sge1 ctx) stk1 f1 (ssp ctx) (srs0 ctx) (sm0 ctx) ibf1.(entry) t s -> + list_forall2 match_stackframes stk1 stk2 -> + match_function f1 f2 -> exists s', - iblock_step tr_inputs (sge2 ctx) stk2 f2 (ssp ctx) (srs0 ctx) (sm0 ctx) ib2 t s' + iblock_step tr_inputs (sge2 ctx) stk2 f2 (ssp ctx) (srs0 ctx) (sm0 ctx) ibf2.(entry) t s' /\ match_states s s'. Proof. - unfold symbolic_simu, sstate_simu. - intros SIMU ctx t s1 STEP1. + unfold sstate_simu. + intros SIMU STEP1 STACKS MF. exploit (sexec_correct (bctx1 ctx)); simpl; eauto. - intros SST1. exploit sem_sstate_run; eauto. - intros (sis1 & sfv1 & rs & m & OUTC1 & SIS1 & SV1). - exploit sem_si_ok; eauto. intros SOK. - intros; exploit SIMU; eauto. - intros (sis2 & sfv2 & OUTC2 & SSIMU & SEM). - exploit symbolic_simu_ssem; eauto. + intros SST1. exploit symbolic_simu_ssem; eauto. intros (s2 & SST2 & MS). exploit (sexec_exact (bctx2 ctx)); simpl; eauto. intros (s3 & STEP & EQUIV). @@ -163,57 +269,34 @@ Proof. eapply match_states_equiv; eauto. Qed. -(* -Lemma iblock_istep_simulation_None stk1 stk2 f f' sp pc rs1 m rs1' m' rs2 ib1 ibf2 s - (ISTEP: iblock_istep pge sp rs1 m ib1 rs1' m' None) - (PC: (fn_code f') ! pc = Some ibf2) - (EQREGS: forall r : positive, rs1 # r = rs2 # r) - (STACKS: list_forall2 match_stackframes stk1 stk2) - (TRANSF: match_function f f') - :exists rs2' s', - iblock_istep_run tpge sp ibf2.(entry) rs2 m = Some (out rs2' m' None) - /\ match_states s s'. +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. Proof. - induction ib1; inv ISTEP; eauto. + induction ib; try_simplify_someHyps. Admitted. -Lemma iblock_istep_simulation_Some stk1 stk2 f f' sp ib1: forall fin ibf2 rs1 m rs1' m' rs2 pc t s - (ISTEP: iblock_istep pge sp rs1 m ib1 rs1' m' (Some fin)) - (FSTEP: final_step tr_inputs pge stk1 f sp rs1' m' fin t s) - (PC: (fn_code f') ! pc = Some ibf2) - (EQREGS: forall r : positive, rs1 # r = rs2 # r) - (STACKS: list_forall2 match_stackframes stk1 stk2) - (TRANSF: match_function f f'), - exists rs2' s', - iblock_istep_run tpge sp ibf2.(entry) rs2 m = Some (out rs2' m' (Some fin)) - /\ final_step tr_inputs tpge stk2 f' sp rs2' m' fin t s' - /\ match_states s s'. -Proof. - induction ib1; simpl; try_simplify_someHyps; inv ISTEP; eauto; intros. - - (* BF *) - admit. - - (* Bseq continue *) - exploit iblock_istep_simulation_None; eauto. - intros (rs2' & s' & ISTEP & MS). - admit. - - -Admitted. - *) -Lemma iblock_step_simulation stk1 stk2 f f' sp rs rs' m ibf t s pc - (STEP: iblock_step tr_inputs pge stk1 f sp rs m ibf.(entry) t s) - (PC: (fn_code f) ! pc = Some ibf) +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) (EQREGS: forall r : positive, rs # r = rs' # r) (STACKS: list_forall2 match_stackframes stk1 stk2) - (TRANSF: match_function f f') + (TRANSF: match_function f1 f2) :exists ibf' s', - (fn_code f') ! pc = Some ibf' - /\ iblock_step tr_inputs tpge stk2 f' sp rs' m ibf'.(entry) t s' + (fn_code f2) ! pc = Some ibf' + /\ 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). - inversion TRANSF. apply symbolic_simu_ok in PC as SYMB. - destruct SYMB as (ibf2 & PC' & SYMBS). clear symbolic_simu_ok. - unfold symbolic_simu, sstate_simu in SYMBS. + (*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. Admitted. Local Hint Constructors step: core. diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index 513ed40a..f5c2f3db 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -743,7 +743,7 @@ Theorem transf_program_correct: Proof. eapply compose_forward_simulations. - eapply transf_program_correct_cfg. - - eapply cfgsem2fsem. + - eapply cfgsem2fsem. eauto. Admitted. End BTL_SIMULATES_RTL. -- cgit