Simplification by merging fixpoints

1 files changed, 96 insertions, 21 deletions

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) :=