diff options
Diffstat (limited to 'scheduling/MyRTLpathSchedulerproof.v')
| -rw-r--r-- | scheduling/MyRTLpathSchedulerproof.v | 526 |
1 files changed, 526 insertions, 0 deletions
diff --git a/scheduling/MyRTLpathSchedulerproof.v b/scheduling/MyRTLpathSchedulerproof.v new file mode 100644 index 00000000..4f14903e --- /dev/null +++ b/scheduling/MyRTLpathSchedulerproof.v @@ -0,0 +1,526 @@ +Require Import AST Linking Values Maps Globalenvs Smallstep Registers. +Require Import Coqlib Maps Events Errors Op. +Require Import RTL RTLpath RTLpathLivegen RTLpathLivegenproof RTLpathSE_theory. +Require Import MyRTLpathScheduler. + +Definition match_prog (p tp: program) := + match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp. + +Lemma transf_program_match: + forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog. +Proof. + intros. eapply match_transform_partial_program_contextual; eauto. +Qed. + +Section PRESERVATION. + +Variable prog: program. +Variable tprog: program. + +Hypothesis TRANSL: match_prog prog tprog. + +Let pge := Genv.globalenv prog. +Let tpge := Genv.globalenv tprog. + +Hypothesis all_fundef_liveness_ok: forall b fd, Genv.find_funct_ptr pge b = Some fd -> liveness_ok_fundef fd. + +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. + +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. + +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_preserved: + forall f tf, transf_fundef f = OK tf -> funsig tf = funsig f. +Proof. + intros. destruct f. + - simpl in H. monadInv H. + destruct (transf_function f) as [res H]; simpl in * |- *; auto. + destruct (H _ EQ). + intuition subst; auto. + symmetry. + eapply match_function_preserves. + eassumption. + - simpl in H. monadInv H. reflexivity. +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). + exists (Callstate nil tf nil m0). + split. + - econstructor; eauto. + + intros; apply (Genv.init_mem_match TRANSL); assumption. + + replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto. + symmetry. eapply match_program_main. eauto. + + destruct f. + * monadInv TRANSF. rewrite <- H3. + destruct (transf_function f) as [res H]; simpl in * |- *; auto. + destruct (H _ EQ). + intuition subst; auto. + symmetry; eapply match_function_preserves. eassumption. + * monadInv TRANSF. assumption. + - constructor; eauto. + + constructor. + + apply transf_fundef_correct; auto. +(* + eapply all_fundef_liveness_ok; eauto. *) +Qed. + +Theorem transf_final_states s1 s2 r: + final_state s1 r -> match_states s1 s2 -> final_state s2 r. +Proof. + unfold final_state. + intros H; inv H. + intros H; inv H; simpl in * |- *; try congruence. + inv H1. + destruct st; simpl in * |- *; try congruence. + inv STACKS. constructor. +Qed. + + +Let ge := Genv.globalenv (RTLpath.transf_program prog). +Let tge := Genv.globalenv (RTLpath.transf_program tprog). + +Lemma senv_sym x y: Senv.equiv x y -> Senv.equiv y x. +Proof. + unfold Senv.equiv. intuition congruence. +Qed. + +Lemma senv_transitivity x y z: Senv.equiv x y -> Senv.equiv y z -> Senv.equiv x z. +Proof. + unfold Senv.equiv. intuition congruence. +Qed. + +Lemma senv_preserved_RTL: + Senv.equiv ge tge. +Proof. + eapply senv_transitivity. { eapply senv_sym; eapply RTLpath.senv_preserved. } + eapply senv_transitivity. { eapply senv_preserved. } + eapply RTLpath.senv_preserved. +Qed. + +Lemma symbols_preserved_RTL s: Genv.find_symbol tge s = Genv.find_symbol ge s. +Proof. + unfold tge, ge. erewrite RTLpath.symbols_preserved; eauto. + rewrite symbols_preserved. + erewrite RTLpath.symbols_preserved; eauto. +Qed. + +Program Definition mkctx sp rs0 m0 {f1: RTLpath.function} (hyp: liveness_ok_function f1) + : simu_proof_context f1 + := {| the_ge1:= ge; the_ge2 := tge; the_sp:=sp; the_rs0:=rs0; the_m0:=m0 |}. +Obligation 2. + erewrite symbols_preserved_RTL. eauto. +Qed. + +Lemma s_find_function_fundef f sp svos rs0 m0 fd + (LIVE: liveness_ok_function f): + sfind_function pge ge sp svos rs0 m0 = Some fd -> + liveness_ok_fundef fd. +Proof. + unfold sfind_function. destruct svos; simpl. + + destruct (seval_sval _ _ _ _); try congruence. + eapply find_funct_liveness_ok; eauto. + + destruct (Genv.find_symbol _ _); try congruence. + intros. eapply all_fundef_liveness_ok; eauto. +Qed. +Local Hint Resolve s_find_function_fundef: core. + +Lemma s_find_function_preserved f sp svos1 svos2 rs0 m0 fd + (LIVE: liveness_ok_function f): + (svident_simu f (mkctx sp rs0 m0 LIVE) svos1 svos2) -> + sfind_function pge ge sp svos1 rs0 m0 = Some fd -> + exists fd', sfind_function tpge tge sp svos2 rs0 m0 = Some fd' + /\ transf_fundef fd = OK fd'. +Proof. + Local Hint Resolve symbols_preserved_RTL: core. + unfold sfind_function. intros [sv1 sv2 SIMU|]; simpl in *. + + rewrite !(seval_preserved ge tge) in *; eauto. + destruct (seval_sval _ _ _ _); try congruence. + erewrite <- SIMU; try congruence. clear SIMU. + intros; exploit functions_preserved; eauto. + intros (fd' & cunit & (X1 & X2 & X3)). eexists. + repeat split; eauto. + + subst. rewrite symbols_preserved. destruct (Genv.find_symbol _ _); try congruence. + intros; exploit function_ptr_preserved; eauto. +Qed. + +Lemma sistate_simu f dupmap outframe sp st st' rs m is + (LIVE: liveness_ok_function f): + ssem_internal ge sp st rs m is -> + sistate_simu dupmap f outframe st st' (mkctx sp rs m LIVE)-> + exists is', + ssem_internal tge sp st' rs m is' /\ istate_simu f dupmap outframe is is'. +Proof. + intros SEM X; eapply X; eauto. +Qed. + +Lemma seval_builtin_sval_preserved sp rs m: + forall bs, seval_builtin_sval ge sp bs rs m = seval_builtin_sval tge sp bs rs m. +Proof. + induction bs. + all: try (simpl; try reflexivity; erewrite seval_preserved by eapply symbols_preserved_RTL; reflexivity). + all: simpl; rewrite IHbs1; rewrite IHbs2; reflexivity. +Qed. + +Lemma seval_list_builtin_sval_preserved sp rs m: + forall lbs, + seval_list_builtin_sval ge sp lbs rs m = seval_list_builtin_sval tge sp lbs rs m. +Proof. + induction lbs; [simpl; reflexivity|]. + simpl. rewrite seval_builtin_sval_preserved. rewrite IHlbs. + reflexivity. +Qed. + +Lemma ssem_final_simu dm f f' stk stk' sp st st' rs0 m0 sv sv' rs m t s + (LIVE: liveness_ok_function f): + match_function dm f f' -> + list_forall2 match_stackframes stk stk' -> + sfval_simu dm f st.(si_pc) st'.(si_pc) (mkctx sp rs0 m0 LIVE) sv sv' -> + ssem_final pge ge sp st.(si_pc) stk f rs0 m0 sv rs m t s -> + exists s', ssem_final tpge tge sp st'.(si_pc) stk' f' rs0 m0 sv' rs m t s' /\ match_states s s'. +Proof. + Local Hint Resolve transf_fundef_correct: core. + intros FUN STK SFV. destruct SFV; intros SEM; inv SEM; simpl in *. + - (* Snone *) + exploit initialize_path. { eapply dupmap_path_entry1; eauto. } + intros (path & PATH). + eexists; split; econstructor; eauto. + eapply eqlive_reg_refl. + - (* Scall *) + exploit s_find_function_preserved; eauto. + intros (fd' & FIND & TRANSF). + erewrite <- function_sig_preserved; eauto. + exploit initialize_path. { eapply dupmap_path_entry1; eauto. } + intros (path & PATH). + eexists; split; econstructor; eauto. + + eapply eq_trans; try eassumption; auto. + + simpl. repeat (econstructor; eauto). + - (* Stailcall *) + exploit s_find_function_preserved; eauto. + intros (fd' & FIND & TRANSF). + erewrite <- function_sig_preserved; eauto. + eexists; split; econstructor; eauto. + + erewrite <- preserv_fnstacksize; eauto. + + eapply eq_trans; try eassumption; auto. + - (* Sbuiltin *) + pose senv_preserved_RTL as SRTL. + exploit initialize_path. { eapply dupmap_path_entry1; eauto. } + intros (path & PATH). + eexists; split; econstructor; eauto. + + eapply seval_builtin_args_preserved; eauto. + eapply seval_list_builtin_sval_correct; eauto. + rewrite H0. + erewrite seval_list_builtin_sval_preserved; eauto. + + eapply external_call_symbols_preserved; eauto. + + eapply eqlive_reg_refl. + - (* Sjumptable *) + exploit ptree_get_list_nth_rev; eauto. intros (p2 & LNZ & DM). + exploit initialize_path. { eapply dupmap_path_entry1; eauto. } + intros (path & PATH). + eexists; split; econstructor; eauto. + + eapply eq_trans; try eassumption; auto. + + eapply eqlive_reg_refl. + - (* Sreturn *) + eexists; split; econstructor; eauto. + erewrite <- preserv_fnstacksize; eauto. + - (* Sreturn bis *) + eexists; split; econstructor; eauto. + + erewrite <- preserv_fnstacksize; eauto. + + rewrite <- H. erewrite <- seval_preserved; eauto. +Qed. + +Lemma siexec_snone_por_correct rs' is t s alive path0 i sp s0 st0 stk stk' f rs0 m0: forall + (SSEM2 : ssem_final pge ge sp (si_pc s0) stk f rs0 m0 Snone + (irs is) (imem is) t s) + (SIEXEC : siexec_inst i st0 = Some s0) + (ICHK : inst_checker (fn_path f) alive (pre_output_regs path0) i = Some tt), + (liveness_ok_function f) -> + list_forall2 match_stackframes stk stk' -> + eqlive_reg (fun r : Regset.elt => Regset.In r (pre_output_regs path0)) (irs is) rs' -> + exists s' : state, + ssem_final pge ge sp (si_pc s0) stk f rs0 m0 Snone rs' (imem is) t s' /\ + eqlive_states s s'. +Proof. + Local Hint Resolve eqlive_stacks_refl: core. + intros ? ? ? LIVE STK EQLIVE. + inversion SSEM2; subst; clear SSEM2. + eexists; split. + * econstructor. + * generalize ICHK. + unfold inst_checker. destruct i; simpl in *; + unfold exit_checker; try discriminate. + all: + try destruct Pos.eq_dec; simpl; + try destruct (list_mem _ _); simpl; + try (destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence; fail). + 4,5: + destruct (Regset.mem _ _); destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence. + 1,2,3,4: assert (NPC: n=(si_pc s0)). + all: try (inv SIEXEC; simpl; auto; fail). + 1,2,3,4: + try (destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence); + simpl; inversion_SOME p; + destruct (Regset.subset (input_regs p) (pre_output_regs path0)) eqn:SUB_PATH; try congruence; + intros NPATH _; econstructor; eauto; + try (instantiate (1:=p); rewrite <- NPC; auto; fail). + 1,2,3,4: + eapply eqlive_reg_monotonic; eauto; simpl; + intros; apply Regset.subset_2 in SUB_PATH; + unfold Regset.Subset in SUB_PATH; + apply SUB_PATH in H; auto. + assert (NPC: n0=(si_pc s0)). { inv SIEXEC; simpl; auto. } + inversion_SOME p. + 2: { destruct (Regset.subset _ _) eqn:?; try congruence. } + destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence. + 2: { + destruct (Regset.subset (pre_output_regs path0) alive) eqn:?; try congruence; + destruct ((fn_path f) ! n); intros; try discriminate. + all: inversion SIEXEC; simpl; auto. + all: destruct Regset.subset in ICHK0; try discriminate; + destruct Regset.subset in ICHK0; try discriminate; + simpl in ICHK0. + all: destruct PTree.get eqn:GET in ICHK0; try discriminate. + all: destruct Regset.subset eqn:SUBS_PATH0 in ICHK0; try discriminate. + all: econstructor; eauto. + all: eapply eqlive_reg_monotonic; eauto. + all: destruct (Regset.subset (input_regs p0) (pre_output_regs path0)) eqn:SUB_PATH; try congruence. + all: intros; apply Regset.subset_2 in SUB_PATH. + all: unfold Regset.Subset in SUB_PATH; apply SUB_PATH in H; auto. } + intros; simpl. + destruct (Regset.subset (pre_output_regs path0) alive) eqn:SUB_ALIVE'; try congruence. + destruct (Regset.subset (input_regs p) (pre_output_regs path0)) eqn:SUB_PATH; try congruence. + apply Regset.subset_2 in SUB_PATH. + unfold Regset.Subset in SUB_PATH. + econstructor; eauto. { rewrite <- NPC; eauto. } + eapply eqlive_reg_monotonic; eauto. +Qed. + +Lemma pre_output_regs_correct f pc0 path0 stk stk' sp (st:sstate) rs0 m0 t s is rs': + (liveness_ok_function f) -> + (fn_path f) ! pc0 = Some path0 -> + sexec f pc0 = Some st -> + list_forall2 match_stackframes stk stk' -> + ssem_final pge ge sp (si_pc st) stk f rs0 m0 (final st) (irs is) (imem is) t s -> + eqlive_reg (fun r : Regset.elt => Regset.In r (pre_output_regs path0)) (irs is) rs' -> + exists s', ssem_final pge ge sp (si_pc st) stk f rs0 m0 (final st) rs' (imem is) t s' /\ eqlive_states s s'. +Proof. + Local Hint Resolve eqlive_stacks_refl: core. + intros LIVE PATH0 SEXEC STK SSEM2 EQLIVE. + (* start decomposing path_checker *) + generalize (LIVE pc0 path0 PATH0). + unfold path_checker. + inversion_SOME res; intros IPCHK. + inversion_SOME i; intros INST ICHK. + exploit ipath_checker_default_succ; eauto. intros DEFSUCC. + (* start decomposing SEXEC *) + generalize SEXEC; clear SEXEC. + unfold sexec; rewrite PATH0. + inversion_SOME st0; intros SEXEC_PATH. + exploit siexec_path_default_succ; eauto. + simpl. rewrite DEFSUCC. + clear DEFSUCC. destruct res as [alive pc1]. simpl in *. + try_simplify_someHyps. + destruct (siexec_inst i st0) eqn: SIEXEC; try_simplify_someHyps; intros. + (* Snone *) + eapply siexec_snone_por_correct; eauto. + destruct i; try_simplify_someHyps; try congruence; + inversion SSEM2; subst; clear SSEM2; simpl in *. + + (* Scall *) + eexists; split. + * econstructor; eauto. + * econstructor; eauto. + econstructor; eauto. + (* wf *) + generalize ICHK. + unfold inst_checker; simpl in *. + destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence. + destruct (list_mem _ _); try congruence. + destruct (reg_sum_mem _ _); try congruence. + intros EXIT. + exploit exit_checker_eqlive_ext1; eauto. + intros. destruct H as [p [PATH EQLIVE']]. + econstructor; eauto. + + (* Stailcall *) + eexists; split. + * econstructor; eauto. + * econstructor; eauto. + + (* Sbuiltin *) + eexists; split. + * econstructor; eauto. + * (* wf *) + generalize ICHK. + unfold inst_checker; simpl in *. + destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence. + destruct (list_mem _ _); try congruence. + intros EXIT. + exploit exit_checker_eqlive_builtin_res; eauto. + intros. destruct H as [p [PATH EQLIVE']]. + econstructor; eauto. + + (* Icond *) + eexists; split. + * econstructor. + * generalize ICHK. + unfold inst_checker; simpl in *. + destruct Pos.eq_dec; destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence. + + (* Sjumptable *) + eexists; split. + * econstructor; eauto. + * (* wf *) + generalize ICHK. + unfold inst_checker; simpl in *. + destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence. + destruct (Regset.mem _ _); try congruence. + destruct (exit_list_checker _ _ _) eqn:EQL; try congruence. + exploit exit_list_checker_eqlive; eauto. + intros. destruct H as [p [PATH EQLIVE']]. + econstructor; eauto. + + (* Sreturn *) + eexists; split. + * econstructor; eauto. + * econstructor; eauto. +Qed. + +(* The main theorem on simulation of symbolic states ! *) +Theorem ssem_sstate_simu dm f f' pc0 path0 stk stk' sp st st' rs m t s: + (fn_path f) ! pc0 = Some path0 -> + sexec f pc0 = Some st -> + match_function dm f f' -> + liveness_ok_function f -> + list_forall2 match_stackframes stk stk' -> + ssem pge ge sp st stk f rs m t s -> + (forall ctx: simu_proof_context f, sstate_simu dm f (pre_output_regs path0) st st' ctx) -> + exists s', ssem tpge tge sp st' stk' f' rs m t s' /\ match_states s s'. +Proof. + intros PATH0 SEXEC MFUNC LIVE STACKS SEM SIMU. + destruct (SIMU (mkctx sp rs m LIVE)) as (SIMU1 & SIMU2); clear SIMU. + destruct SEM as [is CONT SEM|is t s' CONT SEM1 SEM2]; simpl in *. + - (* sem_early *) + exploit sistate_simu; eauto. + unfold istate_simu; rewrite CONT. + intros (is' & SEM' & (path & PATH & (CONT' & RS' & M') & PC')). + exists (State stk' f' sp (ipc is') (irs is') (imem is')). + split. + + eapply ssem_early; auto. congruence. + + rewrite M'. econstructor; eauto. + - (* sem_normal *) + exploit sistate_simu; eauto. + unfold istate_simu; rewrite CONT. + intros (is' & SEM' & (CONT' & RS' & M')). + exploit pre_output_regs_correct; eauto. + clear SEM2; intros (s0 & SEM2 & EQLIVE). + exploit ssem_final_simu; eauto. + clear SEM2; intros (s1 & SEM2 & MATCH0). + exploit ssem_final_equiv; eauto. + clear SEM2; rewrite M'; rewrite CONT' in CONT; intros (s2 & EQ & SEM2). + exists s2; split. + + eapply ssem_normal; eauto. + + eapply eqlive_match_states; eauto. + eapply match_states_equiv; eauto. +Qed. + +Lemma exec_path_simulation dupmap path stk stk' f f' sp rs m pc pc' t s: + (fn_path f)!pc = Some path -> + path_step ge pge path.(psize) stk f sp rs m pc t s -> + list_forall2 match_stackframes stk stk' -> + dupmap ! pc' = Some pc -> + match_function dupmap f f' -> + liveness_ok_function f -> + exists path' s', (fn_path f')!pc' = Some path' /\ path_step tge tpge path'.(psize) stk' f' sp rs m pc' t s' /\ match_states s s'. +Proof. + intros PATH STEP STACKS DUPPC MATCHF LIVE. + exploit initialize_path. { eapply dupmap_path_entry2; eauto. } + intros (path' & PATH'). + exists path'. + exploit (sexec_correct f pc pge ge sp path stk rs m t s); eauto. + intros (st & SYMB & SEM). + exploit dupmap_correct; eauto. + intros (path0 & st' & PATH0 & SYMB' & SIMU). + rewrite PATH0 in PATH; inversion PATH; subst. + exploit ssem_sstate_simu; eauto. + intros (s0 & SEM0 & MATCH). + exploit (sexec_exact f'); eauto. + intros (s' & STEP' & EQ). + exists s'; intuition. + eapply match_states_equiv; eauto. +Qed. + +Lemma step_simulation s1 t s1' s2: + step ge pge s1 t s1' -> + match_states s1 s2 -> + exists s2', + step tge tpge s2 t s2' + /\ match_states s1' s2'. +Proof. + Local Hint Resolve eqlive_stacks_refl transf_fundef_correct: core. + destruct 1 as [path stack f sp rs m pc t s PATH STEP | | | ]; intros MS; inv MS. +(* exec_path *) + - try_simplify_someHyps. intros. + exploit path_step_eqlive; eauto. (* { intros. eapply all_fundef_liveness_ok; eauto. } *) + clear STEP EQUIV rs; intros (s2 & STEP & EQLIVE). + exploit exec_path_simulation; eauto. + clear STEP; intros (path' & s' & PATH' & STEP' & MATCH'). + exists s'; split. + + eapply exec_path; eauto. + + eapply eqlive_match_states; eauto. +(* exec_function_internal *) + - inv LIVE. + exploit initialize_path. { eapply (fn_entry_point_wf f). } + destruct 1 as (path & PATH). + inversion TRANSF as [f0 xf tf MATCHF|]; subst. eexists. split. + + eapply exec_function_internal. erewrite <- preserv_fnstacksize; eauto. + + erewrite preserv_fnparams; eauto. + econstructor; eauto. + { apply preserv_entrypoint; auto. } + { apply eqlive_reg_refl. } +(* exec_function_external *) + - inversion TRANSF as [|]; subst. eexists. split. + + econstructor. eapply external_call_symbols_preserved; eauto. apply senv_preserved_RTL. + + constructor. assumption. +(* exec_return *) + - inv STACKS. destruct b1 as [res' f' sp' pc' rs']. eexists. split. + + constructor. + + inv H1. econstructor; eauto. +Qed. + +Theorem transf_program_correct: + forward_simulation (semantics prog) (semantics tprog). +Proof. + eapply forward_simulation_step with match_states. + - eapply senv_preserved. + - eapply transf_initial_states. + - intros; eapply transf_final_states; eauto. + - intros; eapply step_simulation; eauto. +Qed. + +End PRESERVATION. |