diff options
Diffstat (limited to 'scheduling/RTLpathSchedulerproof.v')
| -rw-r--r-- | scheduling/RTLpathSchedulerproof.v | 509 |
1 files changed, 0 insertions, 509 deletions
diff --git a/scheduling/RTLpathSchedulerproof.v b/scheduling/RTLpathSchedulerproof.v deleted file mode 100644 index a9c2fa76..00000000 --- a/scheduling/RTLpathSchedulerproof.v +++ /dev/null @@ -1,509 +0,0 @@ -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 RTLpathScheduler. - -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 (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. } - simpl. - destruct (Regset.subset (pre_output_regs path0) alive) eqn:SUB_ALIVE'; try congruence. - inversion_SOME p'. - destruct (Regset.subset (input_regs p') (pre_output_regs path0)) eqn:SUB_PATH; try congruence. - intros NPATH NPATH' _. econstructor; eauto. - instantiate (1:=p'). rewrite <- NPC; auto. - 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. -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. - + (* 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. |