From 8252a8b7678ca4b82191ce0159b93b976f8c58d9 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 14 Jun 2021 13:35:51 +0200 Subject: begin scheduler BTL proof --- scheduling/BTL_Schedulerproof.v | 146 ++++++++++++++++++++++++++++++++++++++-- 1 file changed, 141 insertions(+), 5 deletions(-) (limited to 'scheduling/BTL_Schedulerproof.v') diff --git a/scheduling/BTL_Schedulerproof.v b/scheduling/BTL_Schedulerproof.v index 3811b170..f186581f 100644 --- a/scheduling/BTL_Schedulerproof.v +++ b/scheduling/BTL_Schedulerproof.v @@ -1,7 +1,7 @@ Require Import AST Linking Values Maps Globalenvs Smallstep Registers. -Require Import Coqlib Maps Events Errors Op. +Require Import Coqlib Maps Events Errors Op OptionMonad. Require Import RTL BTL BTL_SEtheory. -Require Import BTL_Scheduler. +Require Import BTLmatchRTL BTL_Scheduler. Definition match_prog (p tp: program) := match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp. @@ -22,12 +22,148 @@ Hypothesis TRANSL: match_prog prog tprog. Let pge := Genv.globalenv prog. Let tpge := Genv.globalenv tprog. -Inductive match_states (s1 s2: BTL.state): Prop :=. (* STUB *) +Lemma symbols_preserved s: Genv.find_symbol tpge s = Genv.find_symbol pge s. +Proof. + rewrite <- (Genv.find_symbol_match TRANSL). reflexivity. +Qed. + +Lemma senv_preserved: + Senv.equiv pge tpge. +Proof. + eapply (Genv.senv_match TRANSL). +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') + | match_External ef: match_fundef (External ef) (External ef). + +Inductive match_stackframes: stackframe -> stackframe -> Prop := + | match_stackframe_intro + res f sp pc rs f' + (TRANSF: match_function f f') + : match_stackframes (BTL.Stackframe res f sp pc rs) (BTL.Stackframe res f' sp pc rs). + +Inductive match_states: state -> state -> Prop := + | match_states_intro + st f sp pc rs m st' f' + (*(ENTRY: (fn_code f) ! pc = Some ibf)*) + (STACKS: list_forall2 match_stackframes st st') + (TRANSF: match_function f f') + : match_states (State st f sp pc rs m) (State st' f' sp pc rs m) + | match_states_call + st st' f f' args m + (STACKS: list_forall2 match_stackframes st st') + (TRANSF: match_fundef f f') + : match_states (Callstate st f args m) (Callstate st' f' args m) + | match_states_return + st st' v m + (STACKS: list_forall2 match_stackframes st st') + : match_states (Returnstate st v m) (Returnstate st' v m) + . + +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. +Qed. + +Lemma transf_fundef_correct f f': + transf_fundef f = OK f' -> match_fundef f f'. +Proof. +Admitted. + +Lemma function_ptr_preserved: + forall v f, + Genv.find_funct_ptr pge v = Some f -> + exists tf, + Genv.find_funct_ptr tpge v = Some tf /\ transf_fundef f = OK tf. +Proof. + intros. + exploit (Genv.find_funct_ptr_transf_partial TRANSL); eauto. +Qed. + +Lemma function_sig_translated f tf: transf_fundef f = OK tf -> funsig tf = funsig f. +Proof. + intros H; apply transf_fundef_correct in H; destruct H; simpl; eauto. + symmetry; erewrite preserv_fnsig; eauto. +Qed. + +Theorem transf_initial_states: + forall s1, initial_state prog s1 -> + exists s2, initial_state tprog s2 /\ match_states s1 s2. +Proof. + intros. inv H. + exploit function_ptr_preserved; eauto. intros (tf & FIND & TRANSF). + eexists. split. + - econstructor; eauto. + + intros; apply (Genv.init_mem_match TRANSL); eauto. + + replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto. + symmetry. eapply match_program_main. eauto. + + erewrite function_sig_translated; eauto. + - constructor; eauto. + + constructor. + + apply transf_fundef_correct; auto. +Qed. + +Lemma transf_final_states s1 s2 r: + match_states s1 s2 -> final_state s1 r -> final_state s2 r. +Proof. + intros. inv H0. inv H. inv STACKS. constructor. +Qed. + +Lemma iblock_step_simulation stk1 stk2 f f' sp rs m ibf t s1 pc + (STEP : iblock_step tr_inputs pge stk1 f sp rs m ibf.(entry) t s1) + (ENTRY : (fn_code f) ! pc = Some ibf) + (STACKS : list_forall2 match_stackframes stk1 stk2) + (TRANSF : match_function f f') + :exists s2 : state, + (fn_code f') ! pc = Some ibf /\ + iblock_step tr_inputs tpge stk2 f' sp rs m ibf.(entry) t s2 /\ + match_states s1 s2. +Admitted. + +Local Hint Constructors step: core. + +Theorem step_simulation s1 s1' t s2 + (STEP: step tr_inputs pge s1 t s1') + (MS: match_states s1 s2) + :exists s2', + step tr_inputs tpge s2 t s2' + /\ match_states s1' s2'. +Proof. + destruct STEP as [stack ibf f sp n rs m t s ENTRY STEP | | | ]; inv MS. + - (* iblock *) + simplify_someHyps. intros ENTRY. + exploit iblock_step_simulation; eauto. + intros (s2 & ENTRY2 & STEP2 & MS2). + eexists; split; eauto. + - (* function internal *) + inversion TRANSF as [xf tf MF |]; subst. + eexists; split. + + econstructor. erewrite <- preserv_fnstacksize; eauto. + + erewrite preserv_fnparams; eauto. + erewrite preserv_entrypoint; eauto. + econstructor; eauto. + - (* function external *) + inv TRANSF. eexists; split; econstructor; eauto. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. + - (* return *) + inv STACKS. destruct b1 as [res' f' sp' pc' rs']. + eexists; split. + + econstructor. + + inv H1. econstructor; eauto. +Qed. Theorem transf_program_correct: forward_simulation (fsem prog) (fsem tprog). Proof. - eapply forward_simulation_step with match_states. (* lock-step with respect to match_states *) -Admitted. + eapply forward_simulation_step with match_states; simpl; eauto. (* lock-step with respect to match_states *) + - eapply senv_preserved. + - eapply transf_initial_states. + - eapply transf_final_states. + - intros; eapply step_simulation; eauto. +Qed. End PRESERVATION. -- cgit