aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64/Peephole.v
diff options
context:
space:
mode:
Diffstat (limited to 'aarch64/Peephole.v')
-rw-r--r--aarch64/Peephole.v177
1 files changed, 0 insertions, 177 deletions
diff --git a/aarch64/Peephole.v b/aarch64/Peephole.v
deleted file mode 100644
index 54670708..00000000
--- a/aarch64/Peephole.v
+++ /dev/null
@@ -1,177 +0,0 @@
-(* *************************************************************)
-(* *)
-(* 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.
-
-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.
-
-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 (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 rd1 b1 n1 t2
- end.
-
-(* 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 => None
- | h2 :: t2 =>
- match h2 with
- | (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
- | 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)) =>
- (* 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
- (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
- Pnop :: (pair_rep t0)
- 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 =>*)
- (*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*)
-
-
-(* ########################## 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.
-
-Definition optimize_body (insns : list basic) :=
- if Compopts.optim_coalesce_mem tt
- then (pair_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.
generated by cgit (git 2.34.1) at 2024-06-13 11:41:39 +0000