diff options
Diffstat (limited to 'aarch64/Peephole.v')
| -rw-r--r-- | aarch64/Peephole.v | 100 |
1 files changed, 35 insertions, 65 deletions
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 |