Ocaml peephole oracle and array datastruct instead of lists

1 files changed, 227 insertions, 0 deletions

diff --git a/aarch64/PeepholeOracle.ml b/aarch64/PeepholeOracle.ml
new file mode 100644
index 00000000..c9a1f8f4
--- /dev/null
+++ b/aarch64/PeepholeOracle.ml
@@ -0,0 +1,227 @@
+(* *************************************************************)
+(*                                                             *)
+(*             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.                          *)
+(*                                                             *)
+(* *************************************************************)
+
+open Camlcoq
+open Asmblock
+open Asm
+open Int64
+open Printf
+
+let debug = true
+
+let is_valid_immofs_32 z =
+  if z <= 252 && z >= -256 && z mod 4 == 0 then true else false
+
+let is_valid_immofs_64 z =
+  if z <= 504 && z >= -512 && z mod 8 == 0 then true else false
+
+let is_valid_ldrw rd1 rd2 b1 b2 n1 n2 =
+  let z1 = to_int (camlint64_of_coqint n1) in
+  let z2 = to_int (camlint64_of_coqint n2) in
+  if
+    (not (ireg_eq rd1 rd2))
+    && iregsp_eq b1 b2
+    && (not (iregsp_eq (RR1 rd1) b1))
+    && z2 == z1 + 4
+    && is_valid_immofs_32 z1
+  then true
+  else false
+
+let is_valid_ldrx rd1 rd2 b1 b2 n1 n2 =
+  let z1 = to_int (camlint64_of_coqint n1) in
+  let z2 = to_int (camlint64_of_coqint n2) in
+  if
+    (not (ireg_eq rd1 rd2))
+    && iregsp_eq b1 b2
+    && (not (iregsp_eq (RR1 rd1) b1))
+    && z2 == z1 + 8
+    && is_valid_immofs_64 z1
+  then true
+  else false
+
+let is_valid_strw b1 b2 n1 n2 =
+  let z1 = to_int (camlint64_of_coqint n1) in
+  let z2 = to_int (camlint64_of_coqint n2) in
+  if iregsp_eq b1 b2 && z2 == z1 + 4 && is_valid_immofs_32 z1 then true
+  else false
+
+let is_valid_strx b1 b2 n1 n2 =
+  let z1 = to_int (camlint64_of_coqint n1) in
+  let z2 = to_int (camlint64_of_coqint n2) in
+  if iregsp_eq b1 b2 && z2 == z1 + 8 && is_valid_immofs_64 z1 then true
+  else false
+
+let dreg_of_ireg r = IR (RR1 r)
+
+(*let pot_ldrw_rep = ref []*)
+
+let rec affect_symb_mem reg pot_rep stype =
+  match (pot_rep, stype) with
+  | [], _ -> []
+  | ( ((PLoad (PLd_rd_a (Pldrw, IR (RR1 rd), ADimm (b, n))), _) as h0) :: t0,
+      "ldrw" ) ->
+      if dreg_eq reg (IR b) then affect_symb_mem reg t0 stype
+      else h0 :: affect_symb_mem reg t0 stype
+  | _, _ -> failwith "Found an inconsistent inst in pot_rep"
+
+let rec read_symb_mem reg pot_rep stype =
+  match (pot_rep, stype) with
+  | [], _ -> []
+  | ( ((PLoad (PLd_rd_a (Pldrw, IR (RR1 rd), ADimm (b, n))), _) as h0) :: t0,
+      "ldrw" ) ->
+      if dreg_eq reg (IR (RR1 rd)) then read_symb_mem reg t0 stype
+      else h0 :: read_symb_mem reg t0 stype
+  | _, _ -> failwith "Found an inconsistent inst in pot_rep"
+
+let update_pot_rep inst pot_rep stype =
+  match inst with
+  | PArith i -> (
+      match i with
+      | PArithP (_, rd) -> pot_rep := affect_symb_mem rd !pot_rep stype
+      | PArithPP (_, rd, rs) ->
+          pot_rep := affect_symb_mem rd !pot_rep stype;
+          pot_rep := read_symb_mem rs !pot_rep stype
+      | PArithPPP (_, rd, rs1, rs2) ->
+          pot_rep := affect_symb_mem rd !pot_rep stype;
+          pot_rep := read_symb_mem rs1 !pot_rep stype;
+          pot_rep := read_symb_mem rs2 !pot_rep stype
+      | PArithRR0R (_, rd, rs1, rs2) ->
+          pot_rep := affect_symb_mem (dreg_of_ireg rd) !pot_rep stype;
+          (match rs1 with
+          | RR0 rs1 ->
+              pot_rep := read_symb_mem (dreg_of_ireg rs1) !pot_rep stype
+          | _ -> ());
+          pot_rep := read_symb_mem (dreg_of_ireg rs2) !pot_rep stype
+      | PArithRR0 (_, rd, rs) -> (
+          pot_rep := affect_symb_mem (dreg_of_ireg rd) !pot_rep stype;
+          match rs with
+          | RR0 rs1 ->
+              pot_rep := read_symb_mem (dreg_of_ireg rs1) !pot_rep stype
+          | _ -> ())
+      | PArithARRRR0 (_, rd, rs1, rs2, rs3) -> (
+          pot_rep := affect_symb_mem (dreg_of_ireg rd) !pot_rep stype;
+          pot_rep := read_symb_mem (dreg_of_ireg rs1) !pot_rep stype;
+          pot_rep := read_symb_mem (dreg_of_ireg rs2) !pot_rep stype;
+          match rs3 with
+          | RR0 rs1 ->
+              pot_rep := read_symb_mem (dreg_of_ireg rs1) !pot_rep stype
+          | _ -> ())
+      | PArithComparisonPP (_, rs1, rs2) ->
+          pot_rep := read_symb_mem rs1 !pot_rep stype;
+          pot_rep := read_symb_mem rs2 !pot_rep stype
+      | PArithComparisonR0R (_, rs1, rs2) ->
+          (match rs1 with
+          | RR0 rs1 ->
+              pot_rep := read_symb_mem (dreg_of_ireg rs1) !pot_rep stype
+          | _ -> ());
+          pot_rep := read_symb_mem (dreg_of_ireg rs2) !pot_rep stype
+      | PArithComparisonP (_, rs1) ->
+          pot_rep := read_symb_mem rs1 !pot_rep stype
+      | Pcset (rd, _) ->
+          pot_rep := affect_symb_mem (dreg_of_ireg rd) !pot_rep stype
+      | Pfmovi (_, _, rs) -> (
+          match rs with
+          | RR0 rs -> pot_rep := read_symb_mem (dreg_of_ireg rs) !pot_rep stype
+          | _ -> ())
+      | Pcsel (rd, rs1, rs2, _) ->
+          pot_rep := affect_symb_mem rd !pot_rep stype;
+          pot_rep := read_symb_mem rs1 !pot_rep stype;
+          pot_rep := read_symb_mem rs2 !pot_rep stype
+      | Pfnmul (_, rd, rs1, rs2) -> ())
+  | PLoad i -> (
+      match i with
+      | PLd_rd_a (_, rd, _) -> pot_rep := affect_symb_mem rd !pot_rep stype
+      | Pldp (_, rd1, rd2, _) ->
+          pot_rep := affect_symb_mem (dreg_of_ireg rd1) !pot_rep stype;
+          pot_rep := affect_symb_mem (dreg_of_ireg rd2) !pot_rep stype)
+  | PStore _ -> pot_rep := []
+  (* TODO *)
+  | _ -> ()
+
+(*let update_symb_mem inst = update_pot_rep inst pot_ldrw_rep "ldrw"*)
+
+let rec search_compat_rep rd b n pot_rep stype =
+  match (pot_rep, stype) with
+  | [], _ -> None
+  | ( ((PLoad (PLd_rd_a (Pldrx, IR (RR1 rd'), ADimm (b', n'))), c) as h0) :: t0,
+      "ldrw" ) ->
+      if is_valid_ldrw rd rd' b b' n n' then Some h0
+      else search_compat_rep rd b n t0 stype
+  | _, _ -> None
+
+let pair_rep insta =
+  for i = 0 to Array.length insta - 2 do
+    let h0 = insta.(i) in
+    let h1 = insta.(i + 1) in
+    match (h0, h1) with
+    | ( PLoad (PLd_rd_a (Pldrw, IR (RR1 rd1), ADimm (b1, n1))),
+        PLoad (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 && not (iregsp_eq b2 (RR1 rd1)) then (
+          if debug then eprintf "LDP_WOPT\n";
+          insta.(i) <- Pnop
+          (* When two consec mem addr are loading two different dest. *))
+        else if is_valid_ldrw rd1 rd2 b1 b2 n1 n2 then (
+          if debug then eprintf "LDP_WPEEP\n";
+          insta.(i) <- PLoad (Pldp (Pldpw, rd1, rd2, ADimm (b1, n1)));
+          insta.(i + 1) <- Pnop)
+    | ( PLoad (PLd_rd_a (Pldrx, IR (RR1 rd1), ADimm (b1, n1))),
+        PLoad (PLd_rd_a (Pldrx, IR (RR1 rd2), ADimm (b2, n2))) ) ->
+        if ireg_eq rd1 rd2 && not (iregsp_eq b2 (RR1 rd1)) then (
+          if debug then eprintf "LDP_XOPT\n";
+          insta.(i) <- Pnop)
+        else if is_valid_ldrx rd1 rd2 b1 b2 n1 n2 then (
+          if debug then eprintf "LDP_XPEEP\n";
+          insta.(i) <- PLoad (Pldp (Pldpx, rd1, rd2, ADimm (b1, n1)));
+          insta.(i + 1) <- Pnop
+          (* When there are some insts between loads/stores *)
+          (*| PLoad (PLd_rd_a (Pldrw, IR (RR1 rd1), ADimm (b1, n1))), _ ->*)
+          (*(match search_compat_rep h0 pot_ldrw_rep with*)
+          (*| None -> (pot_ldrw_rep := (h0, count) :: !pot_ldrw_rep; h0 :: pair_rep insta t0)*)
+          (*| Some (l, c) -> *))
+    | ( PStore (PSt_rs_a (Pstrw, IR (RR1 rs1), ADimm (b1, n1))),
+        PStore (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 insta t0)
+          (* When two consec mem addr are targeted by two store. *)
+             else*)
+        if is_valid_strw b1 b2 n1 n2 then (
+          if debug then eprintf "STP_WPEEP\n";
+          insta.(i) <- PStore (Pstp (Pstpw, rs1, rs2, ADimm (b1, n1)));
+          insta.(i + 1) <- Pnop (* When nothing can be optimized. *))
+    | ( PStore (PSt_rs_a (Pstrx, IR (RR1 rs1), ADimm (b1, n1))),
+        PStore (PSt_rs_a (Pstrx, IR (RR1 rs2), ADimm (b2, n2))) ) ->
+        (*if (iregsp_eq b1 b2) && (z2 =? z1) then
+          Pnop :: (pair_rep insta t0)
+           else*)
+        if is_valid_strx b1 b2 n1 n2 then (
+          if debug then eprintf "STP_XPEEP\n";
+          insta.(i) <- PStore (Pstp (Pstpx, rs1, rs2, ADimm (b1, n1)));
+          insta.(i + 1) <- Pnop)
+    | h0, _ -> () (*update_symb_mem h0*)
+  done
+
+let optimize_bdy (bdy : basic list) : basic list =
+  if !Clflags.option_fcoalesce_mem then
+    let insta = Array.of_list bdy in
+    (pair_rep insta; Array.to_list insta)
+  else bdy
+
+(** Called peephole function from Coq *)
+
+let peephole_opt bdy =
+  Timing.time_coq
+    [
+      'P'; 'e'; 'e'; 'p'; 'h'; 'o'; 'l'; 'e'; ' '; 'o'; 'r'; 'a'; 'c'; 'l'; 'e';
+    ]
+    optimize_bdy bdy