diff options
Diffstat (limited to 'aarch64/Peephole.v')
| -rw-r--r-- | aarch64/Peephole.v | 167 |
1 files changed, 167 insertions, 0 deletions
diff --git a/aarch64/Peephole.v b/aarch64/Peephole.v new file mode 100644 index 00000000..2282326a --- /dev/null +++ b/aarch64/Peephole.v @@ -0,0 +1,167 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Léo Gourdin UGA, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + +Require Import Coqlib. +Require Import Asmblock. +Require Import Values. +Require Import Integers. +Require Import AST. +Require Compopts. + +(*Fixpoint gpreg_q_search_rec r0 r1 l := + match l with + | h :: t => + let (s0, s1) := gpreg_q_expand h in + if (gpreg_eq r0 s0) && (gpreg_eq r1 s1) + then Some h + else gpreg_q_search_rec r0 r1 t + | nil => None + end. + +Fixpoint gpreg_o_search_rec r0 r1 r2 r3 l := + match l with + | h :: t => + match gpreg_o_expand h with + | (((s0, s1), s2), s3) => + if (gpreg_eq r0 s0) && (gpreg_eq r1 s1) && + (gpreg_eq r2 s2) && (gpreg_eq r3 s3) + then Some h + else gpreg_o_search_rec r0 r1 r2 r3 t + end + | nil => None + end. + +Definition gpreg_q_search (r0 : gpreg) (r1 : gpreg) : option gpreg_q := + gpreg_q_search_rec r0 r1 gpreg_q_list. + +Definition gpreg_o_search r0 r1 r2 r3 : option gpreg_o := + gpreg_o_search_rec r0 r1 r2 r3 gpreg_o_list. + +Parameter print_found_store: forall A, Z -> A -> A. + + Definition coalesce_octuples := true.*) + +Definition is_valid_immofs_32 (z: Z) : bool := + if (zle z 252) && (zle (-256) z) && ((Z.modulo z 4) =? 0) then true else false. + +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 := + match insns with + | nil => nil + | h0 :: t0 => + match t0 with + | h1 :: t1 => + match h0, h1 with + | (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) + (* 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) + (* When nothing can be optimized. *) + else + h0 :: (ldp_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) + 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) + else + h0 :: (ldp_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 :: (ldp_rep t0) + end + | nil => h0 :: nil + 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) := + stp_rep (ldp_rep insns). + (* TODO ADD A FLAG TO ENABLE PEEPHOLE *) + (*if Compopts.optim_coalesce_mem tt*) + (*then ldp_rep insns*) + (*else insns.*) + +Program Definition optimize_bblock (bb : bblock) := + let optimized := optimize_body (body bb) in + let wf_ok := non_empty_bblockb optimized (exit bb) in + {| header := header bb; + body := if wf_ok then optimized else (body bb); + exit := exit bb |}. +Next Obligation. + destruct (non_empty_bblockb (optimize_body (body bb))) eqn:Rwf. + - rewrite Rwf. cbn. trivial. + - exact (correct bb). +Qed. |