From a44c77d4f36894f11958f29a738e791c069cd2e0 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 7 Dec 2020 23:26:20 +0100 Subject: Simplifications in Peephole and size proof. --- aarch64/Peephole.v | 100 +++++++++++++++---------------------------- aarch64/PostpassScheduling.v | 64 ++++++--------------------- 2 files changed, 48 insertions(+), 116 deletions(-) (limited to 'aarch64') diff --git a/aarch64/Peephole.v b/aarch64/Peephole.v index 6cd2e110..a1bb6c6c 100644 --- a/aarch64/Peephole.v +++ b/aarch64/Peephole.v @@ -48,26 +48,43 @@ Definition is_valid_strx (b1 b2: iregsp) (n1 n2: int64) : bool := then true else false. (* Try to find arguments of the next compatible ldrw to replace. *) -Fixpoint get_next_comp_ldpw_args (ldb: basic) (rd1: ireg) (b1: iregsp) (n1: int64) (t1: list basic) : option (ireg * iregsp * int64) := +Fixpoint get_next_comp_ldpw_args (rd1: ireg) (b1: iregsp) (n1: int64) (t1: list basic) : option (ireg * iregsp * int64) := match t1 with | nil => None | (PLd_rd_a Pldrw (IR (RR1 rd2)) (ADimm b2 n2)) :: t2 => if (is_valid_ldrw rd1 rd2 b1 b2 n1 n2) then Some (rd2, b2, n2) else None - | _ :: t2 => get_next_comp_ldpw_args ldb rd1 b1 n1 t2 + | _ :: t2 => get_next_comp_ldpw_args rd1 b1 n1 t2 end. -(*Fixpoint ldpw_follow (ldb h1: basic) (rd1: ireg) (b1: iregsp) (n1: int64) (t1: list basic) : list basic := - match (get_next_comp_ldpw_args ldb rd1 b1 n1 t1) with - | None => ldb :: h1 :: t1 +(* Try to delete the next compatible ldrw to replace. *) +Fixpoint del_next_comp_ldpw_args (rd1: ireg) (b1: iregsp) (n1: int64) (t1: list basic) : list basic := + match t1 with + | nil => nil + | (PLd_rd_a Pldrw (IR (RR1 rd2)) (ADimm b2 n2)) :: t2 => + if (is_valid_ldrw rd1 rd2 b1 b2 n1 n2) then t2 + else t1 + | h2 :: t2 => h2 :: del_next_comp_ldpw_args rd1 b1 n1 t2 + end. + +Fixpoint ldpw_follow (rd1: ireg) (b1: iregsp) (n1: int64) (t1: list basic) : option (basic * list basic) := + match (get_next_comp_ldpw_args rd1 b1 n1 t1) with + | None => None | Some (rd2, b2, n2) => match t1 with - | nil => ldb :: h1 :: nil + | nil => None | h2 :: t2 => match h2 with - | (PLd_rd_a Pldrw (IR (RR1 rd2)) (ADimm b2 n2)) => - | - *) + | (PStore _) => None + | (PLd_rd_a Pldrw (IR (RR1 rd')) (ADimm b' n')) => + if (ireg_eq rd' rd2) && (iregsp_eq b' b2) && (Int64.eq n' n2) then + Some ((PLoad (Pldp Pldpw rd1 rd2 (ADimm b1 n1))), + (del_next_comp_ldpw_args rd1 b1 n1 t1)) + else ldpw_follow rd1 b1 n1 t2 + | _ => ldpw_follow rd1 b1 n1 t2 + end + end + end. Fixpoint pair_rep (insns : list basic) : list basic := match insns with @@ -81,32 +98,30 @@ Fixpoint pair_rep (insns : list basic) : list basic := | (PLd_rd_a Pldrw (IR (RR1 rd1)) (ADimm b1 n1)), (PLd_rd_a Pldrw (IR (RR1 rd2)) (ADimm b2 n2)) => - (* TODO This could be insteresting to add if compatible with the checker - When both load the same dest, and with no reuse of ld1 in ld2. *) - (* if (ireg_eq rd1 rd2) && (negb (iregsp_eq b2 (RR1 rd1))) then + (* When both load the same dest, and with no reuse of ld1 in ld2. *) + if (ireg_eq rd1 rd2) && (negb (iregsp_eq b2 (RR1 rd1))) then Pnop :: (pair_rep t0) (* When two consec mem addr are loading two different dest. *) - else*) - - if (is_valid_ldrw rd1 rd2 b1 b2 n1 n2) then + else if (is_valid_ldrw rd1 rd2 b1 b2 n1 n2) then (PLoad (Pldp Pldpw rd1 rd2 (ADimm b1 n1))) :: Pnop :: (pair_rep t1) (* When nothing can be optimized. *) else h0 :: (pair_rep t0) | (PLd_rd_a Pldrx (IR (RR1 rd1)) (ADimm b1 n1)), (PLd_rd_a Pldrx (IR (RR1 rd2)) (ADimm b2 n2)) => - (*if (ireg_eq rd1 rd2) && (negb (iregsp_eq b2 (RR1 rd1))) then + if (ireg_eq rd1 rd2) && (negb (iregsp_eq b2 (RR1 rd1))) then Pnop :: (pair_rep t0) - else*) - - if (is_valid_ldrx rd1 rd2 b1 b2 n1 n2) then + else if (is_valid_ldrx rd1 rd2 b1 b2 n1 n2) then (PLoad (Pldp Pldpx rd1 rd2 (ADimm b1 n1))) :: Pnop :: (pair_rep t1) else h0 :: (pair_rep t0) (* When there are some insts between loads/stores *) (*| (PLd_rd_a Pldrw (IR (RR1 rd1)) (ADimm b1 n1)), h1 =>*) - (*pair_rep (ldpw_follow h0 h1 rd1 b1 n1 t1)*) + (*match ldpw_follow rd1 b1 n1 t1 with*) + (*| None => h0 :: (pair_rep t0)*) + (*| Some (ldpw, l) => ldpw :: Pnop :: (pair_rep l)*) + (*end*) (*| (PLd_rd_a Pldrx rd1 (ADimm b1 n1)), h1 => ldpx_follow rd1 b1 n1*) @@ -144,51 +159,6 @@ Fixpoint pair_rep (insns : list basic) : list basic := end end. -(*Fixpoint stp_rep (insns : list basic) : list basic := - match insns with - | nil => nil - | h0 :: t0 => - match t0 with - | h1 :: t1 => - match h0, h1 with - | (PSt_rs_a Pstrw (IR (RR1 rs1)) (ADimm b1 n1)), - (PSt_rs_a Pstrw (IR (RR1 rs2)) (ADimm b2 n2)) => - let z1 := Int64.signed n1 in - let z2 := Int64.signed n2 in - - (* When both store at the same addr, same ofs. *) - (*if (iregsp_eq b1 b2) && (z2 =? z1) then - Pnop :: (stp_rep t0) - (* When two consec mem addr are targeted by two store. *) - else*) - - if (iregsp_eq b1 b2) && (z2 =? z1 + 4) && (is_valid_immofs_32 z1) then - (PStore (Pstp Pstpw rs1 rs2 (ADimm b1 n1))) :: Pnop :: (stp_rep t1) - (* When nothing can be optimized. *) - else - h0 :: (stp_rep t0) - | (PSt_rs_a Pstrx (IR (RR1 rs1)) (ADimm b1 n1)), - (PSt_rs_a Pstrx (IR (RR1 rs2)) (ADimm b2 n2)) => - let z1 := Int64.signed n1 in - let z2 := Int64.signed n2 in - - (*if (iregsp_eq b1 b2) && (z2 =? z1) then - Pnop :: (stp_rep t0) - else*) - - if (iregsp_eq b1 b2) && (z2 =? z1 + 8) && (is_valid_immofs_64 z1) then - (PStore (Pstp Pstpx rs1 rs2 (ADimm b1 n1))) :: Pnop :: (stp_rep t1) - else - h0 :: (stp_rep t0) - (*| (PLd_rd_a Pldrw rd1 (ADimm b1 n1)), h1 => ldpw_follow rd1 b1 n1*) - (*| (PLd_rd_a Pldrx rd1 (ADimm b1 n1)), h1 => ldpx_follow rd1 b1 n1*) - | _, _ => h0 :: (stp_rep t0) - end - | nil => h0 :: nil - end - end. - *) - Definition optimize_body (insns : list basic) := (* TODO ADD A FLAG TO ENABLE PEEPHOLE *) if Compopts.optim_coalesce_mem tt diff --git a/aarch64/PostpassScheduling.v b/aarch64/PostpassScheduling.v index 19bed77b..b8c16131 100644 --- a/aarch64/PostpassScheduling.v +++ b/aarch64/PostpassScheduling.v @@ -68,66 +68,28 @@ Definition do_schedule (bb: bblock) : res bblock := if (Z.eqb (size bb) 1) then OK (bb) else match (schedule bb) with (lb, oc) => schedule_to_bblock lb oc end. +Definition do_peephole (bb: bblock) : bblock := + let res := Peephole.optimize_bblock bb in + if (size res =? size bb) then res else bb. + Definition verified_schedule (bb : bblock) : res bblock := let nhbb := no_header bb in - let nhbb' := Peephole.optimize_bblock nhbb in - do nhbb'' <- do_schedule nhbb'; - let bb' := stick_header (header bb) nhbb'' in + let phbb := do_peephole nhbb in + do schbb <- do_schedule phbb; + let bb' := stick_header (header bb) schbb in do sizecheck <- verify_size bb bb'; do schedcheck <- verify_schedule bb bb'; OK (bb'). -(*Lemma size_peephole_unchanged: forall bb,*) - (*size (Peephole.optimize_bblock (no_header bb)) = size (no_header bb).*) -(*Proof.*) - (*intros.*) - (*unfold Peephole.optimize_bblock, size in *. simpl in *.*) - (*destruct non_empty_bblockb eqn:NEMPTY; auto.*) - (*apply inj_eq. rewrite Nat.add_cancel_r.*) - (*unfold Peephole.optimize_body.*) - (*remember (body bb) as l.*) - (*generalize dependent l.*) - (*induction l.*) - (*- simpl. reflexivity.*) - (*- intros.*) - (*simpl.*) - (*unfold Peephole.stp_rep, Peephole.ldp_rep.*) - Lemma verified_schedule_size: forall bb bb', verified_schedule bb = OK bb' -> size bb = size bb'. Proof. -Admitted. - (*intros. unfold verified_schedule in H.*) - (*monadInv H.*) - (*unfold do_schedule in EQ.*) - (*destruct schedule in EQ.*) - (*destruct Peephole.optimize_bblock eqn:PEEP.*) - (*destruct (size (_) =? 1) eqn:TRIVB in EQ.*) - (*[>destruct (size (Peephole.optimize_bblock (no_header bb)) =? 1) eqn:TRIVB.<]*) - (*-*) - (*inv EQ. *) - (*unfold Peephole.optimize_bblock in PEEP. simpl in *.*) - - (*unfold size. *) - (*simpl in *.*) - - (*simpl. unfold non_empty_bblockb, non_empty_exit, non_empty_body.*) - (*reflexivity.*) - (*- unfold schedule_to_bblock in EQ.*) - (*destruct o in EQ.*) - (*+ inv EQ. unfold verify_size in EQ1. unfold size in *. simpl in *.*) - (*rewrite Z.eqb_neq in TRIVB.*) - (*destruct (Z.of_nat (Datatypes.length (header bb) + Datatypes.length (body bb) + length_opt (exit bb)) =?*) - (*Z.of_nat (Datatypes.length (header bb) + Datatypes.length l + 1)) eqn:ESIZE; try discriminate.*) - (*rewrite Z.eqb_eq in ESIZE; repeat rewrite Nat2Z.inj_add in *;*) - (*rewrite ESIZE. reflexivity.*) - (*+ unfold make_bblock_from_basics in EQ. destruct l in EQ; try discriminate.*) - (*inv EQ. unfold verify_size in EQ1; unfold size in *; simpl in *.*) - (*destruct (Z.of_nat (Datatypes.length (header bb) + Datatypes.length (body bb) + length_opt (exit bb)) =?*) - (*Z.of_nat (Datatypes.length (header bb) + Datatypes.S (Datatypes.length l) + 0)) eqn:ESIZE; try discriminate.*) - (*rewrite Z.eqb_eq in ESIZE. repeat rewrite Nat2Z.inj_add in *.*) - (*rewrite ESIZE. reflexivity.*) -(*Qed.*) + intros. unfold verified_schedule in H. + monadInv H. + unfold verify_size in EQ1. + destruct (size _ =? size _) eqn:ESIZE_H in EQ1; try discriminate. + rewrite Z.eqb_eq in ESIZE_H; rewrite ESIZE_H; reflexivity. +Qed. Theorem verified_schedule_correct: forall ge f bb bb', -- cgit