diff options
Diffstat (limited to 'mppa_k1c/Asmblockdeps.v')
| -rw-r--r-- | mppa_k1c/Asmblockdeps.v | 202 |
1 files changed, 199 insertions, 3 deletions
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 225c3e98..baaff273 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -654,17 +654,35 @@ Definition trans_basic (b: basic) : inst := | 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)] + then [(#d0, 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))] + | PLoadORRO od a ofs => + match gpreg_o_expand od with + | (d0, d1, d2, d3) => + if (ireg_eq d0 a) || (ireg_eq d1 a) || (ireg_eq d2 a) + then [(#d0, 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)); + (#d2, Op (Load (OLoadRRO Pld_a (Ptrofs.add ofs (Ptrofs.repr 16)))) (PReg (#a) @ PReg pmem @ Enil)); + (#d3, Op (Load (OLoadRRO Pld_a (Ptrofs.add ofs (Ptrofs.repr 24)))) (PReg (#a) @ PReg pmem @ Enil))] + end | 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 => let (s0, s1) := gpreg_q_expand qs in [(pmem, Op (Store (OStoreRRO Psd_a ofs)) (PReg (#s0) @ PReg (#a) @ PReg pmem @ Enil)); (pmem, Op (Store (OStoreRRO Psd_a (Ptrofs.add ofs (Ptrofs.repr 8)))) (PReg (#s1) @ PReg (#a) @ PReg pmem @ Enil))] + | PStoreORRO os a ofs => + match gpreg_o_expand os with + | (s0, s1, s2, s3) => + [(pmem, Op (Store (OStoreRRO Psd_a ofs)) (PReg (#s0) @ PReg (#a) @ PReg pmem @ Enil)); + (pmem, Op (Store (OStoreRRO Psd_a (Ptrofs.add ofs (Ptrofs.repr 8)))) (PReg (#s1) @ PReg (#a) @ PReg pmem @ Enil)); + (pmem, Op (Store (OStoreRRO Psd_a (Ptrofs.add ofs (Ptrofs.repr 16)))) (PReg (#s2) @ PReg (#a) @ PReg pmem @ Enil)); + (pmem, Op (Store (OStoreRRO Psd_a (Ptrofs.add ofs (Ptrofs.repr 24)))) (PReg (#s3) @ PReg (#a) @ PReg pmem @ Enil))] + end | Pallocframe sz pos => [(#FP, PReg (#SP)); (#SP, Op (Allocframe2 sz pos) (PReg (#SP) @ PReg pmem @ Enil)); (#RTMP, Op (Constant Vundef) Enil); (pmem, Op (Allocframe sz pos) (Old (PReg (#SP)) @ PReg pmem @ Enil))] | Pfreeframe sz pos => [(pmem, Op (Freeframe sz pos) (PReg (#SP) @ PReg pmem @ Enil)); @@ -885,7 +903,9 @@ Proof. unfold parexec_load_regxs; simpl; unfold exec_load_deps_regxs; rewrite H, H0; rewrite (H0 rofs); destruct (Mem.loadv _ _ _) eqn:MEML; simpl; auto; eexists; split; try split; Simpl; - intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl. + intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl. + + (* Load Quad word *) + unfold parexec_load_q_offset. destruct (gpreg_q_expand rd) as [rd0 rd1]. destruct (ireg_eq rd0 ra) as [ OVERLAP0 | NOOVERLAP0 ]. @@ -935,6 +955,106 @@ Proof. constructor. ++ rewrite H0. rewrite H. rewrite MEML0. trivial. + (* Load Octuple word *) + + unfold parexec_load_o_offset. + destruct (gpreg_o_expand rd) as [[[rd0 rd1] rd2] rd3]. + destruct (ireg_eq rd0 ra); simpl; trivial. + destruct (ireg_eq rd1 ra); simpl; trivial. + destruct (ireg_eq rd2 ra); simpl; trivial. + destruct Ge. + 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. + { destruct (Mem.loadv Many64 mr + (Val.offset_ptr (rsr ra) (Ptrofs.add ofs (Ptrofs.repr 16)))) as [load2| ] eqn:MEML2. + { destruct (Mem.loadv Many64 mr + (Val.offset_ptr (rsr ra) (Ptrofs.add ofs (Ptrofs.repr 24)))) as [load3| ] eqn:MEML3. + { 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. + repeat rewrite (assign_diff _ _ (# ra)) by (apply ppos_discr; congruence). + rewrite H0. + repeat rewrite (assign_diff _ _ pmem) by (apply not_eq_sym; apply ppos_pmem_discr). + rewrite H. + rewrite MEML2. + repeat rewrite (assign_diff _ _ (# ra)) by (apply ppos_discr; congruence). + rewrite H0. + repeat rewrite (assign_diff _ _ pmem) by (apply not_eq_sym; apply ppos_pmem_discr). + rewrite H. + rewrite MEML3. + repeat rewrite (assign_diff _ _ (# ra)) by (apply ppos_discr; congruence). + econstructor; split; trivial. + constructor. + { repeat rewrite (assign_diff _ _ pmem) by (apply not_eq_sym; apply ppos_pmem_discr). assumption. } + { intro. + destruct (preg_eq r rd3). + { subst r. rewrite assign_eq. rewrite Pregmap.gss. trivial. + } + rewrite assign_diff by (apply ppos_discr; congruence). + rewrite Pregmap.gso by assumption. + destruct (preg_eq r rd2). + { subst r. rewrite assign_eq. + rewrite Pregmap.gss. trivial. + } + rewrite assign_diff by (apply ppos_discr; congruence). + rewrite Pregmap.gso by assumption. + destruct (preg_eq r rd1). + { subst r. rewrite assign_eq. + rewrite Pregmap.gss. trivial. + } + rewrite assign_diff by (apply ppos_discr; congruence). + rewrite Pregmap.gso by assumption. + destruct (preg_eq r rd0). + { subst r. rewrite assign_eq. + rewrite Pregmap.gss. trivial. + } + rewrite assign_diff by (apply ppos_discr; congruence). + rewrite Pregmap.gso by assumption. + auto. + } + } + rewrite H. rewrite MEML0. + rewrite assign_diff by (apply ppos_discr; congruence). + rewrite H0. + rewrite (assign_diff _ _ pmem) by (apply not_eq_sym; apply ppos_pmem_discr). + rewrite H. rewrite MEML1. + repeat rewrite assign_diff by (apply ppos_discr; congruence). + rewrite H0. + repeat rewrite (assign_diff _ _ pmem) by (apply not_eq_sym; apply ppos_pmem_discr). + rewrite H. rewrite MEML2. + repeat rewrite assign_diff by (apply ppos_discr; congruence). + rewrite H0. + repeat rewrite (assign_diff _ _ pmem) by (apply not_eq_sym; apply ppos_pmem_discr). + rewrite H. rewrite MEML3. + constructor. + } + rewrite H. rewrite MEML0. + rewrite assign_diff by (apply ppos_discr; congruence). + rewrite H0. + rewrite (assign_diff _ _ pmem) by (apply not_eq_sym; apply ppos_pmem_discr). + rewrite H. rewrite MEML1. + repeat rewrite assign_diff by (apply ppos_discr; congruence). + rewrite H0. + repeat rewrite (assign_diff _ _ pmem) by (apply not_eq_sym; apply ppos_pmem_discr). + rewrite H. rewrite MEML2. + repeat rewrite assign_diff by (apply ppos_discr; congruence). + constructor. + } + rewrite H. rewrite MEML0. + rewrite assign_diff by (apply ppos_discr; congruence). + rewrite H0. + rewrite (assign_diff _ _ pmem) by (apply not_eq_sym; apply ppos_pmem_discr). + rewrite H. rewrite MEML1. + repeat rewrite assign_diff by (apply ppos_discr; congruence). + constructor. + } + rewrite H. rewrite MEML0. + constructor. (* Store *) - destruct i. (* Store Offset *) @@ -959,6 +1079,7 @@ Proof. eexists; split; try split; Simpl; intros rr; destruct rr; Simpl. + (* Store Quad Word *) + unfold parexec_store_q_offset. simpl. destruct (gpreg_q_expand rs) as [s0 s1]. @@ -989,6 +1110,81 @@ Proof. reflexivity. ++ rewrite MEML0. reflexivity. + + (* Store Ocuple Word *) + + unfold parexec_store_o_offset. + simpl. + destruct (gpreg_o_expand rs) as [[[s0 s1] s2] s3]. + simpl. + destruct Ge. + destruct (Mem.storev _ _ _ (rsr s0)) as [store0 | ] eqn:MEML0. + { destruct (Mem.storev _ _ _ (rsr s1)) as [store1 | ] eqn:MEML1. + { destruct (Mem.storev _ _ _ (rsr s2)) as [store2 | ] eqn:MEML2. + { destruct (Mem.storev _ _ _ (rsr s3)) as [store3 | ] eqn:MEML3. + { repeat (try rewrite H0; try rewrite H). + simpl. + rewrite MEML0. + repeat rewrite (assign_diff _ _ _) by apply ppos_pmem_discr. + repeat (try rewrite H0; try rewrite H). + rewrite assign_eq. + rewrite MEML1. + repeat rewrite (assign_diff _ _ _) by apply ppos_pmem_discr. + repeat (try rewrite H0; try rewrite H). + rewrite assign_eq. + rewrite MEML2. + repeat rewrite (assign_diff _ _ _) by apply ppos_pmem_discr. + repeat (try rewrite H0; try rewrite H). + rewrite assign_eq. + rewrite MEML3. + econstructor; split; trivial. + split. + { repeat rewrite assign_eq. trivial. } + { intro. + repeat rewrite (assign_diff _ _ _) by apply ppos_pmem_discr. + trivial. } + } + { + repeat (try rewrite H0; try rewrite H; simpl). + rewrite MEML0. + repeat rewrite (assign_diff _ _ _) by apply ppos_pmem_discr. + repeat (try rewrite H0; try rewrite H; simpl). + rewrite MEML1. + repeat rewrite (assign_diff _ _ _) by apply ppos_pmem_discr. + repeat (try rewrite H0; try rewrite H; simpl). + rewrite MEML2. + repeat rewrite (assign_diff _ _ _) by apply ppos_pmem_discr. + repeat (try rewrite H0; try rewrite H; simpl). + rewrite MEML3. + trivial. + } + } + { + repeat (try rewrite H0; try rewrite H; simpl). + rewrite MEML0. + repeat rewrite (assign_diff _ _ _) by apply ppos_pmem_discr. + repeat (try rewrite H0; try rewrite H; simpl). + rewrite MEML1. + repeat rewrite (assign_diff _ _ _) by apply ppos_pmem_discr. + repeat (try rewrite H0; try rewrite H; simpl). + rewrite MEML2. + trivial. + } + } + { + repeat (try rewrite H0; try rewrite H; simpl). + rewrite MEML0. + repeat rewrite (assign_diff _ _ _) by apply ppos_pmem_discr. + repeat (try rewrite H0; try rewrite H; simpl). + rewrite MEML1. + trivial. + } + } + { + repeat (try rewrite H0; try rewrite H; simpl). + rewrite MEML0. + trivial. + } + (* Allocframe *) - destruct (Mem.alloc _ _ _) eqn:MEMAL. destruct (Mem.store _ _ _ _) eqn:MEMS. * eexists; repeat split. |