aboutsummaryrefslogtreecommitdiffstats
path: root/mppa_k1c/lib/RTLpathScheduler.v
diff options
context:
space:
mode:
Diffstat (limited to 'mppa_k1c/lib/RTLpathScheduler.v')
-rw-r--r--mppa_k1c/lib/RTLpathScheduler.v70
1 files changed, 35 insertions, 35 deletions
diff --git a/mppa_k1c/lib/RTLpathScheduler.v b/mppa_k1c/lib/RTLpathScheduler.v
index fb2be412..4478ee72 100644
--- a/mppa_k1c/lib/RTLpathScheduler.v
+++ b/mppa_k1c/lib/RTLpathScheduler.v
@@ -33,7 +33,7 @@ Record match_function (dupmap: PTree.t node) (f1 f2: RTLpath.function): Prop :=
preserv_entrypoint: dupmap!(f2.(fn_entrypoint)) = Some f1.(fn_entrypoint);
dupmap_path_entry1: forall pc1 pc2, dupmap!pc2 = Some pc1 -> path_entry (fn_path f1) pc1;
dupmap_path_entry2: forall pc1 pc2, dupmap!pc2 = Some pc1 -> path_entry (fn_path f2) pc2;
- dupmap_correct: forall pc1 pc2, dupmap!pc2 = Some pc1 -> symb_step_simu dupmap f1 f2 pc1 pc2
+ dupmap_correct: forall pc1 pc2, dupmap!pc2 = Some pc1 -> sstep_simu dupmap f1 f2 pc1 pc2
}.
(* TODO: remove these two stub parameters *)
@@ -110,13 +110,13 @@ Lemma match_stack_equiv stk1 stk2:
forall stk3, list_forall2 equiv_stackframe stk2 stk3 ->
list_forall2 match_stackframes stk1 stk3.
Proof.
- Local Hint Resolve match_stackframes_equiv.
+ Local Hint Resolve match_stackframes_equiv: core.
induction 1; intros stk3 EQ; inv EQ; econstructor; eauto.
Qed.
Lemma match_states_equiv s1 s2 s3: match_states s1 s2 -> equiv_state s2 s3 -> match_states s1 s3.
Proof.
- Local Hint Resolve match_stack_equiv.
+ Local Hint Resolve match_stack_equiv: core.
destruct 1; intros EQ; inv EQ; econstructor; eauto.
intros; eapply eqlive_reg_triv_trans; eauto.
Qed.
@@ -139,7 +139,7 @@ Qed.
Lemma eqlive_match_states s1 s2 s3: eqlive_states s1 s2 -> match_states s2 s3 -> match_states s1 s3.
Proof.
- Local Hint Resolve eqlive_match_stack.
+ Local Hint Resolve eqlive_match_stack: core.
destruct 1; intros MS; inv MS; try_simplify_someHyps; econstructor; eauto.
eapply eqlive_reg_trans; eauto.
Qed.
@@ -293,15 +293,15 @@ Proof.
Qed.
Lemma s_find_function_preserved sp svos rs0 m0 fd:
- s_find_function pge ge sp svos rs0 m0 = Some fd ->
- exists fd', s_find_function tpge tge sp svos rs0 m0 = Some fd'
+ sfind_function pge ge sp svos rs0 m0 = Some fd ->
+ exists fd', sfind_function tpge tge sp svos rs0 m0 = Some fd'
/\ transf_fundef fd = OK fd'
/\ liveness_ok_fundef fd.
Proof.
- Local Hint Resolve symbols_preserved_RTL.
- unfold s_find_function. destruct svos; simpl.
- + rewrite (sval_eval_preserved ge tge); auto.
- destruct (sval_eval _ _ _ _); try congruence.
+ Local Hint Resolve symbols_preserved_RTL: core.
+ unfold sfind_function. destruct svos; simpl.
+ + rewrite (seval_preserved ge tge); auto.
+ destruct (seval_sval _ _ _ _); try congruence.
intros; exploit functions_preserved; eauto.
intros (fd' & cunit & X). eexists. intuition eauto.
eapply find_funct_liveness_ok; eauto.
@@ -310,27 +310,27 @@ Proof.
intros (fd' & X). eexists. intuition eauto.
Qed.
-Lemma sem_istate_simu f dupmap sp st st' rs m is:
- sem_istate ge sp st rs m is ->
+Lemma sistate_simu f dupmap sp st st' rs m is:
+ simatch ge sp st rs m is ->
liveness_ok_function f ->
- s_istate_simu f dupmap st st' ->
+ sistate_simu f dupmap st st' ->
exists is',
- sem_istate tge sp st' rs m is' /\ istate_simu f dupmap is is'.
+ simatch tge sp st' rs m is' /\ istate_simu f dupmap is is'.
Proof.
intros SEM LIVE X; eapply X; eauto.
Qed.
-Lemma sem_sfval_simu dupmap f f' stk stk' sp st st' rs0 m0 sv sv' rs m t s:
+Lemma sfmatch_simu dupmap f f' stk stk' sp st st' rs0 m0 sv sv' rs m t s:
match_function dupmap f f' ->
liveness_ok_function f ->
list_forall2 match_stackframes stk stk' ->
(* s_istate_simu f dupmap st st' -> *)
- sfval_simu f dupmap st.(the_pc) st'.(the_pc) sv sv' ->
- sfval_sem pge ge sp st stk f rs0 m0 sv rs m t s ->
- exists s', sfval_sem tpge tge sp st' stk' f' rs0 m0 sv' rs m t s' /\ match_states s s'.
+ sfval_simu f dupmap st.(si_pc) st'.(si_pc) sv sv' ->
+ sfmatch pge ge sp st stk f rs0 m0 sv rs m t s ->
+ exists s', sfmatch tpge tge sp st' stk' f' rs0 m0 sv' rs m t s' /\ match_states s s'.
Proof.
- Local Hint Resolve transf_fundef_correct.
+ Local Hint Resolve transf_fundef_correct: core.
intros FUN LIVE STK (* SIS *) SFV. destruct SFV; intros SEM; inv SEM; simpl.
- (* Snone *)
exploit initialize_path. { eapply dupmap_path_entry1; eauto. }
@@ -350,38 +350,38 @@ Proof.
eexists; split; econstructor; eauto.
+ erewrite <- preserv_fnstacksize; eauto.
+ destruct os; auto.
- erewrite <- sval_eval_preserved; eauto.
+ erewrite <- seval_preserved; eauto.
Qed.
(* The main theorem on simulation of symbolic states ! *)
-Theorem sem_symb_state_simu dupmap f f' stk stk' sp st st' rs m t s:
+Theorem smatch_sstate_simu dupmap f f' stk stk' sp st st' rs m t s:
match_function dupmap f f' ->
liveness_ok_function f ->
list_forall2 match_stackframes stk stk' ->
- sem_state pge ge sp st stk f rs m t s ->
- s_state_simu f dupmap st st' ->
- exists s', sem_state tpge tge sp st' stk' f' rs m t s' /\ match_states s s'.
+ smatch pge ge sp st stk f rs m t s ->
+ sstate_simu f dupmap st st' ->
+ exists s', smatch tpge tge sp st' stk' f' rs m t s' /\ match_states s s'.
Proof.
intros MFUNC LIVE STACKS SEM (SIMU1 & SIMU2). destruct SEM as [is CONT SEM|is t s' CONT SEM1 SEM2]; simpl.
- (* sem_early *)
- exploit sem_istate_simu; eauto.
+ exploit sistate_simu; eauto.
unfold istate_simu; rewrite CONT.
intros (is' & SEM' & (path & PATH & (CONT' & RS' & M') & PC')).
- exists (State stk' f' sp (RTLpath.the_pc is') (the_rs is') (the_mem is')).
+ exists (State stk' f' sp (ipc is') (irs is') (imem is')).
split.
- + eapply sem_early; auto. congruence.
+ + eapply smatch_early; auto. congruence.
+ rewrite M'. econstructor; eauto.
- (* sem_normal *)
- exploit sem_istate_simu; eauto.
+ exploit sistate_simu; eauto.
unfold istate_simu; rewrite CONT.
intros (is' & SEM' & (CONT' & RS' & M')).
rewrite <- eqlive_reg_triv in RS'.
- exploit sem_sfval_simu; eauto.
+ exploit sfmatch_simu; eauto.
clear SEM2; intros (s0 & SEM2 & MATCH0).
- exploit sfval_sem_equiv; eauto.
+ exploit sfmatch_equiv; eauto.
clear SEM2; rewrite M'; rewrite CONT' in CONT; intros (s1 & EQ & SEM2).
exists s1; split.
- + eapply sem_normal; eauto.
+ + eapply smatch_normal; eauto.
+ eapply match_states_equiv; eauto.
Qed.
@@ -398,13 +398,13 @@ Proof.
exploit initialize_path. { eapply dupmap_path_entry2; eauto. }
intros (path' & PATH').
exists path'.
- exploit (symb_step_correct f pc pge ge sp path stk rs m t s); eauto.
+ exploit (sstep_correct f pc pge ge sp path stk rs m t s); eauto.
intros (st & SYMB & SEM); clear STEP.
exploit dupmap_correct; eauto.
clear SYMB; intros (st' & SYMB & SIMU).
- exploit sem_symb_state_simu; eauto.
+ exploit smatch_sstate_simu; eauto.
intros (s0 & SEM0 & MATCH).
- exploit symb_step_exact; eauto.
+ exploit sstep_exact; eauto.
intros (s' & STEP' & EQ).
exists s'; intuition.
eapply match_states_equiv; eauto.
@@ -417,7 +417,7 @@ Lemma step_simulation s1 t s1' s2:
step tge tpge s2 t s2'
/\ match_states s1' s2'.
Proof.
- Local Hint Resolve eqlive_stacks_refl transf_fundef_correct.
+ 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.
generated by cgit (git 2.34.1) at 2024-07-12 01:33:23 +0000