diff options
Diffstat (limited to 'scheduling/RTLpathSchedulerproof.v')
| -rw-r--r-- | scheduling/RTLpathSchedulerproof.v | 215 |
1 files changed, 189 insertions, 26 deletions
diff --git a/scheduling/RTLpathSchedulerproof.v b/scheduling/RTLpathSchedulerproof.v index 4ba197b0..72a4ee01 100644 --- a/scheduling/RTLpathSchedulerproof.v +++ b/scheduling/RTLpathSchedulerproof.v @@ -143,13 +143,25 @@ 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' - /\ liveness_ok_fundef fd. + /\ transf_fundef fd = OK fd'. Proof. Local Hint Resolve symbols_preserved_RTL: core. unfold sfind_function. intros [sv1 sv2 SIMU|]; simpl in *. @@ -159,20 +171,16 @@ Proof. intros; exploit functions_preserved; eauto. intros (fd' & cunit & (X1 & X2 & X3)). eexists. repeat split; eauto. - eapply find_funct_liveness_ok; eauto. -(* intros. eapply all_fundef_liveness_ok; eauto. *) + subst. rewrite symbols_preserved. destruct (Genv.find_symbol _ _); try congruence. intros; exploit function_ptr_preserved; eauto. - intros (fd' & X). eexists. intuition eauto. -(* intros. eapply all_fundef_liveness_ok; eauto. *) Qed. -Lemma sistate_simu f dupmap sp st st' rs m is +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 st st' (mkctx sp rs m LIVE)-> + 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 is is'. + ssem_internal tge sp st' rs m is' /\ istate_simu f dupmap outframe is is'. Proof. intros SEM X; eapply X; eauto. Qed. @@ -198,13 +206,12 @@ 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' -> - (* s_istate_simu f dupmap st st' -> *) 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 (* SIS *) SFV. destruct SFV; intros SEM; inv SEM; simpl in *. + intros FUN STK SFV. destruct SFV; intros SEM; inv SEM; simpl in *. - (* Snone *) exploit initialize_path. { eapply dupmap_path_entry1; eauto. } intros (path & PATH). @@ -212,7 +219,7 @@ Proof. eapply eqlive_reg_refl. - (* Scall *) exploit s_find_function_preserved; eauto. - intros (fd' & FIND & TRANSF & LIVE'). + intros (fd' & FIND & TRANSF). erewrite <- function_sig_preserved; eauto. exploit initialize_path. { eapply dupmap_path_entry1; eauto. } intros (path & PATH). @@ -221,7 +228,7 @@ Proof. + simpl. repeat (econstructor; eauto). - (* Stailcall *) exploit s_find_function_preserved; eauto. - intros (fd' & FIND & TRANSF & LIVE'). + intros (fd' & FIND & TRANSF). erewrite <- function_sig_preserved; eauto. eexists; split; econstructor; eauto. + erewrite <- preserv_fnstacksize; eauto. @@ -253,18 +260,171 @@ Proof. + rewrite <- H. erewrite <- seval_preserved; eauto. Qed. +Lemma ipath_checker_default_succ (f: RTLpath.function) path: forall alive pc res, + ipath_checker path f (fn_path f) alive pc = Some res + -> nth_default_succ (fn_code f) path pc = Some (snd res). +Proof. + induction path; simpl. + + try_simplify_someHyps. + + intros alive pc res. + inversion_SOME i; intros INST. + inversion_SOME res0; intros ICHK IPCHK. + rewrite INST. + erewrite iinst_checker_default_succ; 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 -> + (* path_step ge pge path0.(psize) stk f sp rs0 m0 pc0 t s -> *) (* NB: should be useless *) + sexec f pc0 = Some st -> + (* icontinue is = true -> *) + list_forall2 match_stackframes stk stk' -> + (* ssem_internal ge sp st rs0 m0 is -> *) + 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 (*PSTEP*) SEXEC (*CONT*) STK (*SSEM1*) 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' stk stk' sp st st' rs m t s: +Theorem ssem_sstate_simu dm f f' pc0 path0 stk stk' sp st st' rs m t s: + (fn_path f) ! pc0 = Some path0 -> + (* path_step ge pge (psize path0) stk f sp rs m pc0 t s -> *) + 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 st st' ctx) -> + (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 MFUNC LIVE STACKS SEM SIMU. + intros PATH0 (*STEP*) 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. + 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. @@ -276,15 +436,17 @@ Proof. - (* sem_normal *) exploit sistate_simu; eauto. unfold istate_simu; rewrite CONT. - intros (is' & SEM' & (CONT' & RS' & M')(* & DMEQ *)). - rewrite <- eqlive_reg_triv in RS'. + 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 (s0 & SEM2 & MATCH0). + clear SEM2; intros (s1 & SEM2 & MATCH0). exploit ssem_final_equiv; eauto. - clear SEM2; rewrite M'; rewrite CONT' in CONT; intros (s1 & EQ & SEM2). - exists s1; split. + clear SEM2; rewrite M'; rewrite CONT' in CONT; intros (s2 & EQ & SEM2). + exists s2; split. + eapply ssem_normal; eauto. - + eapply match_states_equiv; 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: @@ -301,12 +463,13 @@ Proof. intros (path' & PATH'). exists path'. exploit (sexec_correct f pc pge ge sp path stk rs m t s); eauto. - intros (st & SYMB & SEM); clear STEP. + intros (st & SYMB & SEM). exploit dupmap_correct; eauto. - clear SYMB; intros (st' & SYMB & SIMU). + 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; eauto. + exploit (sexec_exact f'); eauto. intros (s' & STEP' & EQ). exists s'; intuition. eapply match_states_equiv; eauto. |