From 402c91019a333461b6ae5d06bb62f4879b2145d4 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 7 Dec 2020 11:30:15 +0100 Subject: Simplification by merging fixpoints --- aarch64/Peephole.v | 117 +++++++++++++++++++++++++++++++++++++++++++---------- 1 file changed, 96 insertions(+), 21 deletions(-) (limited to 'aarch64') diff --git a/aarch64/Peephole.v b/aarch64/Peephole.v index ba78b29f..6cd2e110 100644 --- a/aarch64/Peephole.v +++ b/aarch64/Peephole.v @@ -23,54 +23,128 @@ Definition is_valid_immofs_32 (z: Z) : bool := Definition is_valid_immofs_64 (z: Z) : bool := if (zle z 504) && (zle (-512) z) && ((Z.modulo z 8) =? 0) then true else false. -Fixpoint ldp_rep (insns : list basic) : list basic := +Definition is_valid_ldrw (rd1 rd2: ireg) (b1 b2: iregsp) (n1 n2: int64) : bool := + let z1 := Int64.signed n1 in + let z2 := Int64.signed n2 in + if (negb (ireg_eq rd1 rd2)) && (iregsp_eq b1 b2) && (negb (iregsp_eq (RR1 rd1) b1)) + && (z2 =? z1 + 4) && (is_valid_immofs_32 z1) then true else false. + +Definition is_valid_ldrx (rd1 rd2: ireg) (b1 b2: iregsp) (n1 n2: int64) : bool := + let z1 := Int64.signed n1 in + let z2 := Int64.signed n2 in + if (negb (ireg_eq rd1 rd2)) && (iregsp_eq b1 b2) && (negb (iregsp_eq (RR1 rd1) b1)) + && (z2 =? z1 + 8) && (is_valid_immofs_64 z1) then true else false. + +Definition is_valid_strw (b1 b2: iregsp) (n1 n2: int64) : bool := + let z1 := Int64.signed n1 in + let z2 := Int64.signed n2 in + if (iregsp_eq b1 b2) && (z2 =? z1 + 4) && (is_valid_immofs_32 z1) + then true else false. + +Definition is_valid_strx (b1 b2: iregsp) (n1 n2: int64) : bool := + let z1 := Int64.signed n1 in + let z2 := Int64.signed n2 in + if (iregsp_eq b1 b2) && (z2 =? z1 + 8) && (is_valid_immofs_64 z1) + 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) := + 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 + 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 + | Some (rd2, b2, n2) => + match t1 with + | nil => ldb :: h1 :: nil + | h2 :: t2 => + match h2 with + | (PLd_rd_a Pldrw (IR (RR1 rd2)) (ADimm b2 n2)) => + | + *) + +Fixpoint pair_rep (insns : list basic) : list basic := match insns with | nil => nil | h0 :: t0 => match t0 with | h1 :: t1 => match h0, h1 with + +(* ########################## LDP *) + | (PLd_rd_a Pldrw (IR (RR1 rd1)) (ADimm b1 n1)), (PLd_rd_a Pldrw (IR (RR1 rd2)) (ADimm b2 n2)) => - let z1 := Int64.signed n1 in - let z2 := Int64.signed n2 in - (* 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 - Pnop :: (ldp_rep t0) + Pnop :: (pair_rep t0) (* When two consec mem addr are loading two different dest. *) else*) - if (negb (ireg_eq rd1 rd2)) && (iregsp_eq b1 b2) && (negb (iregsp_eq (RR1 rd1) b1)) - && (z2 =? z1 + 4) && (is_valid_immofs_32 z1) then - (PLoad (Pldp Pldpw rd1 rd2 (ADimm b1 n1))) :: Pnop :: (ldp_rep t1) + 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 :: (ldp_rep t0) + h0 :: (pair_rep t0) | (PLd_rd_a Pldrx (IR (RR1 rd1)) (ADimm b1 n1)), (PLd_rd_a Pldrx (IR (RR1 rd2)) (ADimm b2 n2)) => - let z1 := Int64.signed n1 in - let z2 := Int64.signed n2 in - (*if (ireg_eq rd1 rd2) && (negb (iregsp_eq b2 (RR1 rd1))) then - Pnop :: (ldp_rep t0) + Pnop :: (pair_rep t0) else*) - if (negb (ireg_eq rd1 rd2)) && (iregsp_eq b1 b2) && (negb (iregsp_eq (RR1 rd1) b1)) - && (z2 =? z1 + 8) && (is_valid_immofs_64 z1) then - (PLoad (Pldp Pldpx rd1 rd2 (ADimm b1 n1))) :: Pnop :: (ldp_rep t1) + 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 :: (ldp_rep t0) - (*| (PLd_rd_a Pldrw rd1 (ADimm b1 n1)), h1 => ldpw_follow rd1 b1 n1*) + 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)*) (*| (PLd_rd_a Pldrx rd1 (ADimm b1 n1)), h1 => ldpx_follow rd1 b1 n1*) - | _, _ => h0 :: (ldp_rep t0) + + +(* ########################## STP *) + + | (PSt_rs_a Pstrw (IR (RR1 rs1)) (ADimm b1 n1)), + (PSt_rs_a Pstrw (IR (RR1 rs2)) (ADimm b2 n2)) => + (* When both store at the same addr, same ofs. *) + (*if (iregsp_eq b1 b2) && (z2 =? z1) then + Pnop :: (pair_rep t0) + (* When two consec mem addr are targeted by two store. *) + else*) + + if (is_valid_strw b1 b2 n1 n2) then + (PStore (Pstp Pstpw rs1 rs2 (ADimm b1 n1))) :: Pnop :: (pair_rep t1) + (* When nothing can be optimized. *) + else + h0 :: (pair_rep t0) + | (PSt_rs_a Pstrx (IR (RR1 rs1)) (ADimm b1 n1)), + (PSt_rs_a Pstrx (IR (RR1 rs2)) (ADimm b2 n2)) => + (*if (iregsp_eq b1 b2) && (z2 =? z1) then + Pnop :: (pair_rep t0) + else*) + + if (is_valid_strx b1 b2 n1 n2) then + (PStore (Pstp Pstpx rs1 rs2 (ADimm b1 n1))) :: Pnop :: (pair_rep t1) + else + h0 :: (pair_rep t0) + + + + | _, _ => h0 :: (pair_rep t0) end | nil => h0 :: nil end end. -Fixpoint stp_rep (insns : list basic) : list basic := +(*Fixpoint stp_rep (insns : list basic) : list basic := match insns with | nil => nil | h0 :: t0 => @@ -113,11 +187,12 @@ Fixpoint stp_rep (insns : list basic) : list basic := | nil => h0 :: nil end end. + *) Definition optimize_body (insns : list basic) := (* TODO ADD A FLAG TO ENABLE PEEPHOLE *) if Compopts.optim_coalesce_mem tt - then stp_rep (ldp_rep insns) + then (pair_rep insns) else insns. Program Definition optimize_bblock (bb : bblock) := -- cgit