From 906a8553570ed17a8e90831c1d1df18d76e94154 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Mon, 6 May 2019 13:51:51 +0200 Subject: simplification semantique+preuve des load_q+load_o --- mppa_k1c/Asmblockdeps.v | 317 ++++++++----------------------------- mppa_k1c/Asmvliw.v | 14 +- mppa_k1c/PostpassSchedulingproof.v | 4 +- mppa_k1c/lib/Asmblockgenproof0.v | 6 +- 4 files changed, 74 insertions(+), 267 deletions(-) diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index a9f14f8e..7361ee81 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -653,21 +653,15 @@ Definition trans_basic (b: basic) : inst := | 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)] - 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))] + (#d1, Op (Load (OLoadRRO Pld_a (Ptrofs.add ofs (Ptrofs.repr 8)))) (Old(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))] + (#d1, Op (Load (OLoadRRO Pld_a (Ptrofs.add ofs (Ptrofs.repr 8)))) (Old(PReg (#a)) @ PReg pmem @ Enil)); + (#d2, Op (Load (OLoadRRO Pld_a (Ptrofs.add ofs (Ptrofs.repr 16)))) (Old(PReg (#a)) @ PReg pmem @ Enil)); + (#d3, Op (Load (OLoadRRO Pld_a (Ptrofs.add ofs (Ptrofs.repr 24)))) (Old(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))] @@ -869,13 +863,23 @@ 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 -> match_states (State rsw mw) sw -> match_outcome (parexec_basic_instr ge bi rsr rsw mr mw) (inst_prun Ge (trans_basic bi) sw sr sr). Proof. + +(* a little tactic to automate reasoning on preg_eq *) +Local Hint Resolve not_eq_sym ppos_pmem_discr ppos_discr. +Local Ltac preg_eq_discr r rd := + destruct (preg_eq r rd); try (subst r; rewrite assign_eq, Pregmap.gss; auto); + rewrite (assign_diff _ (#rd) (#r) _); auto; + rewrite Pregmap.gso; auto. + intros GENV MSR MSW; inversion MSR as (H & H0); inversion MSW as (H1 & H2). destruct bi; simpl. (* Arith *) @@ -903,156 +907,39 @@ 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 ]; simpl; auto. - 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 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 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 H. rewrite MEML0. trivial. - + destruct (gpreg_q_expand rd) as [rd0 rd1]; destruct Ge; simpl. + rewrite H0, H. + destruct (Mem.loadv Many64 mr _) as [load0 | ]; simpl; auto. + rewrite !(assign_diff _ _ pmem), H; auto. + destruct (Mem.loadv Many64 mr (_ _ (Ptrofs.add ofs (Ptrofs.repr 8)))) as [load1| ]; simpl; auto. + eexists; intuition eauto. + { rewrite !(assign_diff _ _ pmem); auto. } + { preg_eq_discr r rd1. + preg_eq_discr r rd0. } + (* 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. + + Local Hint Resolve not_eq_sym ppos_pmem_discr ppos_discr. + unfold parexec_load_o_offset. + destruct (gpreg_o_expand rd) as [[[rd0 rd1] rd2] rd3]; destruct Ge; simpl. + rewrite H0, H. + destruct (Mem.loadv Many64 mr (Val.offset_ptr (rsr ra) ofs)) as [load0 | ]; simpl; auto. + rewrite !(assign_diff _ _ pmem), !H; auto. + destruct (Mem.loadv Many64 mr (_ _ (Ptrofs.add ofs (Ptrofs.repr 8)))) as [load1| ]; simpl; auto. + rewrite !(assign_diff _ _ pmem), !H; auto. + destruct (Mem.loadv Many64 mr (_ _ (Ptrofs.add ofs (Ptrofs.repr 16)))) as [load2| ]; simpl; auto. + rewrite !(assign_diff _ _ pmem), !H; auto. + destruct (Mem.loadv Many64 mr (_ _ (Ptrofs.add ofs (Ptrofs.repr 24)))) as [load3| ]; simpl; auto. + eexists; intuition eauto. + { rewrite !(assign_diff _ _ pmem); auto. } + { preg_eq_discr r rd3. + preg_eq_discr r rd2. + preg_eq_discr r rd1. + preg_eq_discr r rd0. } + (* Store *) - destruct i. (* Store Offset *) @@ -1079,108 +966,28 @@ Proof. (* Store Quad Word *) + unfold parexec_store_q_offset. - destruct (gpreg_q_expand rs) as [s0 s1]. - simpl. - unfold exec_store_deps_offset. + destruct (gpreg_q_expand rs) as [s0 s1]; destruct Ge; simpl. rewrite !H0, !H. - destruct Ge. - destruct (Mem.storev _ _ _ (rsr s0)) as [mem0 | ] eqn:MEML0; simpl. - ++ rewrite MEML0. - destruct (Mem.storev _ _ _ (rsr s1)) as [mem1 | ] eqn:MEML1; simpl. - * rewrite (assign_diff sr _ (# s1)) by apply ppos_pmem_discr. - rewrite (assign_diff sr _ (# ra)) by apply ppos_pmem_discr. - repeat rewrite H0. - rewrite MEML1. - eexists; split. - reflexivity. - rewrite (assign_eq _ pmem). - split; trivial. - intro r. - rewrite (assign_diff _ _ (# r)) by apply ppos_pmem_discr. - rewrite (assign_diff _ _ (# r)) by apply ppos_pmem_discr. - congruence. - * rewrite (assign_diff sr pmem (# s1)) by apply ppos_pmem_discr. - rewrite (assign_diff sr pmem (# ra)) by apply ppos_pmem_discr. - repeat rewrite H0. - rewrite MEML1. - reflexivity. - ++ rewrite MEML0. - reflexivity. + destruct (Mem.storev _ _ _ (rsr s0)) as [mem0 | ]; simpl; auto. + rewrite !assign_diff, !H0; auto. + destruct (Mem.storev _ _ _ (rsr s1)) as [mem1 | ]; simpl; auto. + eexists; intuition eauto. + rewrite !assign_diff; auto. (* 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. - } - + destruct (gpreg_o_expand rs) as [[[s0 s1] s2] s3]; destruct Ge; simpl. + rewrite !H0, !H. + destruct (Mem.storev _ _ _ (rsr s0)) as [store0 | ]; simpl; auto. + rewrite !assign_diff, !H0; auto. + destruct (Mem.storev _ _ _ (rsr s1)) as [store1 | ]; simpl; auto. + rewrite !assign_diff, !H0; auto. + destruct (Mem.storev _ _ _ (rsr s2)) as [store2 | ]; simpl; auto. + rewrite !assign_diff, !H0; auto. + destruct (Mem.storev _ _ _ (rsr s3)) as [store3 | ]; simpl; auto. + eexists; intuition eauto. + rewrite !assign_diff; auto. + (* Allocframe *) - destruct (Mem.alloc _ _ _) eqn:MEMAL. destruct (Mem.store _ _ _ _) eqn:MEMS. * eexists; repeat split. diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index 3fbc048c..3bef1a5c 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -1186,9 +1186,9 @@ Definition parexec_load_offset (chunk: memory_chunk) (rsr rsw: regset) (mr mw: m Definition parexec_load_q_offset (rsr rsw: regset) (mr mw: mem) (d : gpreg_q) (a: ireg) (ofs: offset) := let (rd0, rd1) := gpreg_q_expand d in - if ireg_eq rd0 a - then Stuck - else +(* NB: By construction of [gpreg_q], register rd0 and rd1 are distinct, thus, the register writes cannot overlap. + But we do not need to express/prove this in the semantics. +*) match Mem.loadv Many64 mr (Val.offset_ptr (rsr a) ofs) with | None => Stuck | Some v0 => @@ -1201,10 +1201,10 @@ Definition parexec_load_q_offset (rsr rsw: regset) (mr mw: mem) (d : gpreg_q) (a Definition parexec_load_o_offset (rsr rsw: regset) (mr mw: mem) (d : gpreg_o) (a: ireg) (ofs: offset) := match gpreg_o_expand d with | (rd0, rd1, rd2, rd3) => - if (ireg_eq rd0 a) || (ireg_eq rd1 a) || (ireg_eq rd2 a) - then Stuck - else - match Mem.loadv Many64 mr (Val.offset_ptr (rsr a) ofs) with +(* NB: By construction of [gpreg_o], the four destination registers are pairwise distinct, thus, the register writes cannot overlap. + But we do not need to express/prove this in the semantics. +*) + match Mem.loadv Many64 mr (Val.offset_ptr (rsr a) ofs) with | None => Stuck | Some v0 => match Mem.loadv Many64 mr (Val.offset_ptr (rsr a) (Ptrofs.add ofs (Ptrofs.repr 8))) with diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 7ade517a..f470ef8a 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -135,7 +135,7 @@ Lemma exec_load_offset_q_pc_var: Proof. intros. unfold exec_load_q_offset in *. unfold parexec_load_q_offset in *. destruct (gpreg_q_expand rd) as [rd0 rd1]. - destruct (ireg_eq rd0 ra); try discriminate. + (* destruct (ireg_eq rd0 ra); try discriminate. *) rewrite Pregmap.gso; try discriminate. destruct (Mem.loadv _ _ _); try discriminate. inv H. @@ -153,9 +153,11 @@ Lemma exec_load_offset_o_pc_var: Proof. intros. unfold exec_load_o_offset in *. unfold parexec_load_o_offset in *. destruct (gpreg_o_expand rd) as [[[rd0 rd1] rd2] rd3]. +(* destruct (ireg_eq rd0 ra); try discriminate. destruct (ireg_eq rd1 ra); try discriminate. destruct (ireg_eq rd2 ra); try discriminate. +*) rewrite Pregmap.gso; try discriminate. simpl in *. destruct (Mem.loadv _ _ _); try discriminate. diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v index e8835a82..a8da1cf1 100644 --- a/mppa_k1c/lib/Asmblockgenproof0.v +++ b/mppa_k1c/lib/Asmblockgenproof0.v @@ -953,19 +953,17 @@ Proof. - (* PLoadQRRO *) unfold parexec_load_q_offset in H1. destruct (gpreg_q_expand _) as [r0 r1] in H1. - destruct (ireg_eq _ _) in H1; try discriminate. destruct (Mem.loadv _ _ _) in H1; try discriminate. destruct (Mem.loadv _ _ _) in H1; try discriminate. - inv H1. Simpl. + inv H1. Simpl. - (* PLoadORRO *) unfold parexec_load_o_offset in H1. destruct (gpreg_o_expand _) as [[[r0 r1] r2] r3] in H1. - destruct (orb _ _) in H1; try discriminate. destruct (Mem.loadv _ _ _) in H1; try discriminate. destruct (Mem.loadv _ _ _) in H1; try discriminate. destruct (Mem.loadv _ _ _) in H1; try discriminate. destruct (Mem.loadv _ _ _) in H1; try discriminate. - inv H1. Simpl. + inv H1. Simpl. - (* PStoreQRRO *) unfold parexec_store_q_offset in H1. destruct (gpreg_q_expand _) as [r0 r1] in H1. -- cgit