diff options
Diffstat (limited to 'mppa_k1c/Asmblockdeps.v')
| -rw-r--r-- | mppa_k1c/Asmblockdeps.v | 60 |
1 files changed, 58 insertions, 2 deletions
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 52af8cdf..ee4a9b51 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -650,6 +650,14 @@ Definition trans_basic (b: basic) : inst := | PLoadRRR n d a ro => [(#d, Op (Load (OLoadRRR n)) (PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))] | PLoadRRRXS n d a ro => [(#d, Op (Load (OLoadRRRXS n)) (PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))] | PStoreRRO n s a ofs => [(pmem, Op (Store (OStoreRRO n ofs)) (PReg (#s) @ PReg (#a) @ PReg pmem @ Enil))] + | PLoadQRRO qd a ofs => + let (d0, d1) := gpreg_q_expand qd in + if ireg_eq d0 a + then [(#d0, Op Fail Enil); + (#d1, Op Fail Enil)] + else + [(#d0, Op (Load (OLoadRRO Pld_a ofs)) (PReg (#a) @ PReg pmem @ Enil)); + (#d1, Op (Load (OLoadRRO Pld_a (Ptrofs.add ofs (Ptrofs.repr 8)))) (PReg (#a) @ PReg pmem @ Enil))] | PStoreRRR n s a ro => [(pmem, Op (Store (OStoreRRR n)) (PReg (#s) @ PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))] | PStoreRRRXS n s a ro => [(pmem, Op (Store (OStoreRRRXS n)) (PReg (#s) @ PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))] | PStoreQRRO qs a ofs => @@ -842,7 +850,7 @@ Proof. * intros rr; destruct rr; Simpl. destruct (ireg_eq g rd); subst; Simpl. Qed. - + Theorem forward_simu_par_wio_basic ge fn rsr rsw mr mw sr sw bi: Ge = Genv ge fn -> match_states (State rsr mr) sr -> @@ -877,7 +885,55 @@ Proof. destruct (Mem.loadv _ _ _) eqn:MEML; simpl; auto; eexists; split; try split; Simpl; intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl. - + + unfold parexec_load_q_offset. + destruct (gpreg_q_expand rd) as [rd0 rd1]. + destruct (ireg_eq rd0 ra) as [ OVERLAP0 | NOOVERLAP0 ]. + simpl. trivial. + unfold exec_load_deps_offset. + destruct Ge. + unfold eval_offset. + repeat rewrite H0. + destruct (Mem.loadv Many64 mr (Val.offset_ptr (rsr ra) ofs)) as [load0 | ] eqn:MEML0; simpl. + ++ destruct (Mem.loadv Many64 mr + (Val.offset_ptr (rsr ra) (Ptrofs.add ofs (Ptrofs.repr 8)))) as [load1| ] eqn:MEML1. + +++ rewrite H0. + rewrite H. + rewrite MEML0. + rewrite (assign_diff _ _ (# ra)) by (apply ppos_discr; congruence). + rewrite H0. + rewrite (assign_diff _ _ pmem) by (apply not_eq_sym; apply ppos_pmem_discr). + rewrite H. + rewrite MEML1. + eexists; split. + * f_equal. + * constructor. + ** repeat rewrite (assign_diff _ _ pmem) by (apply not_eq_sym; apply ppos_pmem_discr). + assumption. + ** intro. + destruct (preg_eq r rd1). + *** subst r. + rewrite (assign_eq _ (# rd1)). + rewrite Pregmap.gss. + reflexivity. + *** rewrite (assign_diff _ (#rd1) (#r) _) by (apply ppos_discr; apply not_eq_sym; assumption). + rewrite Pregmap.gso by assumption. + destruct (preg_eq r rd0). + **** subst r. + rewrite (assign_eq _ (# rd0)). + rewrite Pregmap.gss. + reflexivity. + **** rewrite (assign_diff _ (#rd0) (#r) _) by (apply ppos_discr; apply not_eq_sym; assumption). + rewrite Pregmap.gso by assumption. + trivial. + +++ rewrite H0. rewrite H. rewrite MEML0. + rewrite (assign_diff _ _ (# ra)) by (apply ppos_discr; congruence). + rewrite H0. + rewrite (assign_diff _ _ pmem) by (apply not_eq_sym; apply ppos_pmem_discr). + rewrite H. + rewrite MEML1. + constructor. + ++ rewrite H0. rewrite H. rewrite MEML0. trivial. + (* Store *) - destruct i. (* Store Offset *) |