path: root/aarch64/PeepholeOracle.ml

(* *************************************************************)
(*                                                             *)
(*             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 = false

(* Functions to verify the immediate offset range for ldp/stp *)
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

(* Functions to check if a ldp/stp replacement is valid according to args *)
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) b2))
    && (z2 = z1 + 4 || 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) b2))
    && (z2 = z1 + 8 || 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)

(* Return true if an intermediate
 * affectation eliminates the potential
 * candidate *)
let verify_load_affect reg rd b rev =
  let b = (IR b) in
  let rd = dreg_of_ireg rd in
  if not rev then
    dreg_eq reg b
  else
    (dreg_eq reg b) || (dreg_eq reg rd)

(* Return true if an intermediate
 * read eliminates the potential
 * candidate *)
let verify_load_read reg rd b rev =
  let rd = dreg_of_ireg rd in
  dreg_eq reg rd

(* Return true if an intermediate
 * affectation eliminates the potential
 * candidate *)
let verify_store_affect reg rs b rev =
  let b = (IR b) in
  let rs = dreg_of_ireg rs in
  (dreg_eq reg b) || (dreg_eq reg rs)

(* Affect a symbolic memory list of potential replacements
 * for a given write in reg *)
let rec affect_symb_mem reg insta pot_rep stype rev =
  match pot_rep with
  | [] -> []
  | h0 :: t0 -> (
      match (insta.(h0), stype) with
      | PLoad (PLd_rd_a (Pldrw, IR (RR1 rd), ADimm (b, n))), "ldrw" ->
          if verify_load_affect reg rd b rev then affect_symb_mem reg insta t0 stype rev
          else h0 :: affect_symb_mem reg insta t0 stype rev
      | PLoad (PLd_rd_a (Pldrx, IR (RR1 rd), ADimm (b, n))), "ldrx" ->
          if verify_load_affect reg rd b rev then affect_symb_mem reg insta t0 stype rev
          else h0 :: affect_symb_mem reg insta t0 stype rev
      | PStore (PSt_rs_a (Pstrw, IR (RR1 rs), ADimm (b, n))), "strw" ->
          if verify_store_affect reg rs b rev then
            affect_symb_mem reg insta t0 stype rev
          else h0 :: affect_symb_mem reg insta t0 stype rev
      | PStore (PSt_rs_a (Pstrx, IR (RR1 rs), ADimm (b, n))), "strx" ->
          if verify_store_affect reg rs b rev then
            affect_symb_mem reg insta t0 stype rev
          else h0 :: affect_symb_mem reg insta t0 stype rev
      | _, _ ->
          failwith "affect_symb_mem: Found an inconsistent inst in pot_rep")

(* Affect a symbolic memory list of potential replacements
 * for a given read in reg *)
let rec read_symb_mem reg insta pot_rep stype rev =
  match pot_rep with
  | [] -> []
  | h0 :: t0 -> (
      match (insta.(h0), stype) with
      | PLoad (PLd_rd_a (Pldrw, IR (RR1 rd), ADimm (b, n))), "ldrw" ->
          if verify_load_read reg rd b rev then read_symb_mem reg insta t0 stype rev
          else h0 :: read_symb_mem reg insta t0 stype rev
      | PLoad (PLd_rd_a (Pldrx, IR (RR1 rd), ADimm (b, n))), "ldrx" ->
          if verify_load_read reg rd b rev then read_symb_mem reg insta t0 stype rev
          else h0 :: read_symb_mem reg insta t0 stype rev
      | PStore (PSt_rs_a (Pstrw, IR (RR1 rs), ADimm (b, n))), "strw" ->
          h0 :: affect_symb_mem reg insta t0 stype rev
      | PStore (PSt_rs_a (Pstrx, IR (RR1 rs), ADimm (b, n))), "strx" ->
          h0 :: affect_symb_mem reg insta t0 stype rev
      | _, _ -> failwith "read_symb_mem: Found an inconsistent inst in pot_rep")

(* Update a symbolic memory list of potential replacements
 * for any addressing *)
let update_pot_rep_addressing a insta pot_rep stype rev =
  match a with
  | ADimm (base, _) -> pot_rep := read_symb_mem (IR base) insta !pot_rep stype rev
  | ADreg (base, r) ->
      pot_rep := read_symb_mem (IR base) insta !pot_rep stype rev;
      pot_rep := read_symb_mem (dreg_of_ireg r) insta !pot_rep stype rev
  | ADlsl (base, r, _) ->
      pot_rep := read_symb_mem (IR base) insta !pot_rep stype rev;
      pot_rep := read_symb_mem (dreg_of_ireg r) insta !pot_rep stype rev
  | ADsxt (base, r, _) ->
      pot_rep := read_symb_mem (IR base) insta !pot_rep stype rev;
      pot_rep := read_symb_mem (dreg_of_ireg r) insta !pot_rep stype rev
  | ADuxt (base, r, _) ->
      pot_rep := read_symb_mem (IR base) insta !pot_rep stype rev;
      pot_rep := read_symb_mem (dreg_of_ireg r) insta !pot_rep stype rev
  | ADadr (base, _, _) ->
      pot_rep := read_symb_mem (IR base) insta !pot_rep stype rev
  | ADpostincr (base, _) ->
      pot_rep := read_symb_mem (IR base) insta !pot_rep stype rev

(* Update a symbolic memory list of potential replacements
 * for any basic instruction *)
let update_pot_rep_basic inst insta pot_rep stype rev =
  match inst with
  | PArith i -> (
      match i with
      | PArithP (_, rd) -> pot_rep := affect_symb_mem rd insta !pot_rep stype rev
      | PArithPP (_, rd, rs) ->
          pot_rep := affect_symb_mem rd insta !pot_rep stype rev;
          pot_rep := read_symb_mem rs insta !pot_rep stype rev
      | PArithPPP (_, rd, rs1, rs2) ->
          pot_rep := affect_symb_mem rd insta !pot_rep stype rev;
          pot_rep := read_symb_mem rs1 insta !pot_rep stype rev;
          pot_rep := read_symb_mem rs2 insta !pot_rep stype rev
      | PArithRR0R (_, rd, rs1, rs2) ->
          pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype rev;
          (match rs1 with
          | RR0 rs1 ->
              pot_rep := read_symb_mem (dreg_of_ireg rs1) insta !pot_rep stype rev
          | _ -> ());
          pot_rep := read_symb_mem (dreg_of_ireg rs2) insta !pot_rep stype rev
      | PArithRR0 (_, rd, rs) -> (
          pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype rev;
          match rs with
          | RR0 rs1 ->
              pot_rep := read_symb_mem (dreg_of_ireg rs1) insta !pot_rep stype rev
          | _ -> ())
      | PArithARRRR0 (_, rd, rs1, rs2, rs3) -> (
          pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype rev;
          pot_rep := read_symb_mem (dreg_of_ireg rs1) insta !pot_rep stype rev;
          pot_rep := read_symb_mem (dreg_of_ireg rs2) insta !pot_rep stype rev;
          match rs3 with
          | RR0 rs1 ->
              pot_rep := read_symb_mem (dreg_of_ireg rs1) insta !pot_rep stype rev
          | _ -> ())
      | PArithComparisonPP (_, rs1, rs2) ->
          pot_rep := read_symb_mem rs1 insta !pot_rep stype rev;
          pot_rep := read_symb_mem rs2 insta !pot_rep stype rev
      | PArithComparisonR0R (_, rs1, rs2) ->
          (match rs1 with
          | RR0 rs1 ->
              pot_rep := read_symb_mem (dreg_of_ireg rs1) insta !pot_rep stype rev
          | _ -> ());
          pot_rep := read_symb_mem (dreg_of_ireg rs2) insta !pot_rep stype rev
      | PArithComparisonP (_, rs1) ->
          pot_rep := read_symb_mem rs1 insta !pot_rep stype rev
      | Pcset (rd, _) ->
          pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype rev
      | Pfmovi (_, _, rs) -> (
          match rs with
          | RR0 rs ->
              pot_rep := read_symb_mem (dreg_of_ireg rs) insta !pot_rep stype rev
          | _ -> ())
      | Pcsel (rd, rs1, rs2, _) ->
          pot_rep := affect_symb_mem rd insta !pot_rep stype rev;
          pot_rep := read_symb_mem rs1 insta !pot_rep stype rev;
          pot_rep := read_symb_mem rs2 insta !pot_rep stype rev
      | Pfnmul (_, rd, rs1, rs2) -> ())
  | PLoad i -> (
      match stype with
      | "ldrw" | "ldrx" -> (
          match i with
          | PLd_rd_a (_, rd, a) ->
              pot_rep := affect_symb_mem rd insta !pot_rep stype rev;
              update_pot_rep_addressing a insta pot_rep stype rev
          | Pldp (_, rd1, rd2, a) ->
              pot_rep := affect_symb_mem (dreg_of_ireg rd1) insta !pot_rep stype rev;
              pot_rep := affect_symb_mem (dreg_of_ireg rd2) insta !pot_rep stype rev;
              update_pot_rep_addressing a insta pot_rep stype rev)
      | _ -> pot_rep := [])
  | PStore _ -> pot_rep := []
  | Pallocframe (_, _) -> pot_rep := []
  | Pfreeframe (_, _) -> pot_rep := []
  | Ploadsymbol (rd, _) ->
      pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype rev
  | Pcvtsw2x (rd, rs) ->
      pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype rev;
      pot_rep := read_symb_mem (dreg_of_ireg rs) insta !pot_rep stype rev
  | Pcvtuw2x (rd, rs) ->
      pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype rev;
      pot_rep := read_symb_mem (dreg_of_ireg rs) insta !pot_rep stype rev
  | Pcvtx2w rd ->
      pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype rev;
      pot_rep := read_symb_mem (dreg_of_ireg rd) insta !pot_rep stype rev
  | Pnop -> ()

(* Try to find the index of the first previous compatible
 * replacement in a given symbolic memory *)
let rec search_compat_rep r2 b2 n2 insta pot_rep stype =
  match pot_rep with
  | [] -> None
  | h0 :: t0 -> (
      match (insta.(h0), stype) with
      | PLoad (PLd_rd_a (Pldrw, IR (RR1 rd1), ADimm (b1, n1))), "ldrw" ->
          if is_valid_ldrw rd1 r2 b1 b2 n1 n2 then Some (h0, rd1, b1, n1)
          else search_compat_rep r2 b2 n2 insta t0 stype
      | PLoad (PLd_rd_a (Pldrx, IR (RR1 rd1), ADimm (b1, n1))), "ldrx" ->
          if is_valid_ldrx rd1 r2 b1 b2 n1 n2 then Some (h0, rd1, b1, n1)
          else search_compat_rep r2 b2 n2 insta t0 stype
      | PStore (PSt_rs_a (Pstrw, IR (RR1 rs1), ADimm (b1, n1))), "strw" ->
          if is_valid_strw b1 b2 n1 n2 then Some (h0, rs1, b1, n1)
          else search_compat_rep r2 b2 n2 insta t0 stype
      | PStore (PSt_rs_a (Pstrx, IR (RR1 rs1), ADimm (b1, n1))), "strx" ->
          if is_valid_strx b1 b2 n1 n2 then Some (h0, rs1, b1, n1)
          else search_compat_rep r2 b2 n2 insta t0 stype
      | _, _ ->
          failwith "search_compat_rep: Found an inconsistent inst in pot_rep")

(* Try to find the index of the first previous compatible
 * replacement in a given symbolic memory (when iterating in the reversed list) *)
let rec search_compat_rep_inv r2 b2 n2 insta pot_rep stype =
  match pot_rep with
  | [] -> None
  | h0 :: t0 -> (
      match (insta.(h0), stype) with
      | PLoad (PLd_rd_a (Pldrw, IR (RR1 rd1), ADimm (b1, n1))), "ldrw" ->
          if is_valid_ldrw r2 rd1 b2 b1 n2 n1 then Some (h0, rd1, b1, n1)
          else search_compat_rep_inv r2 b2 n2 insta t0 stype
      | PLoad (PLd_rd_a (Pldrx, IR (RR1 rd1), ADimm (b1, n1))), "ldrx" ->
          if is_valid_ldrx r2 rd1 b2 b1 n2 n1 then Some (h0, rd1, b1, n1)
          else search_compat_rep_inv r2 b2 n2 insta t0 stype
      | PStore (PSt_rs_a (Pstrw, IR (RR1 rs1), ADimm (b1, n1))), "strw" ->
          if is_valid_strw b2 b1 n2 n1 then Some (h0, rs1, b1, n1)
          else search_compat_rep_inv r2 b2 n2 insta t0 stype
      | PStore (PSt_rs_a (Pstrx, IR (RR1 rs1), ADimm (b1, n1))), "strx" ->
          if is_valid_strx b2 b1 n2 n1 then Some (h0, rs1, b1, n1)
          else search_compat_rep_inv r2 b2 n2 insta t0 stype
      | _, _ ->
          failwith "search_compat_rep_inv: Found an inconsistent inst in pot_rep")

(* This is useful to manage the case were the immofs
 * of the first ldr/str is greater than the second one *)
let min_is_rev n1 n2 =
  let z1 = to_int (camlint64_of_coqint n1) in
  let z2 = to_int (camlint64_of_coqint n2) in
  if z1 < z2 then true else false

(* Main peephole function in backward style *)
let pair_rep_inv insta =
  (* Each list below is a symbolic mem representation
   * for one type of inst. Lists contains integers which
   * are the indices of insts in the main array "insta". *)
  let pot_ldrw_rep = ref [] in
  let pot_ldrx_rep = ref [] in
  let pot_strw_rep = ref [] in
  let pot_strx_rep = ref [] in
  for i = Array.length insta - 1 downto 1 do
    let h0 = insta.(i) in
    let h1 = insta.(i - 1) in
    (* Here we need to update every symbolic memory according to the matched inst *)
    update_pot_rep_basic h0 insta pot_ldrw_rep "ldrw" true;
    update_pot_rep_basic h0 insta pot_ldrx_rep "ldrx" true;
    update_pot_rep_basic h0 insta pot_strw_rep "strw" true;
    update_pot_rep_basic h0 insta pot_strx_rep "strx" true;
    match (h0, h1) with
    (* Non-consecutive ldrw *)
    | PLoad (PLd_rd_a (Pldrw, IR (RR1 rd1), ADimm (b1, n1))), _ -> (
        (* Search a previous compatible load *)
        match search_compat_rep_inv rd1 b1 n1 insta !pot_ldrw_rep "ldrw" with
        (* If we can't find a candidate, add the current load as a potential future one *)
        | None -> pot_ldrw_rep := i :: !pot_ldrw_rep
        (* Else, perform the peephole *)
        | Some (rep, r, b, n) ->
            (* The two lines below are used to filter the elected candidate *)
            let filt x = x != rep in
            pot_ldrw_rep := List.filter filt !pot_ldrw_rep;
            insta.(rep) <- Pnop;
            if min_is_rev n n1 then (
              if debug then eprintf "LDP_W_BACK_SPACED_PEEP_IMM_INC\n";
              insta.(i) <- PLoad (Pldp (Pldpw, r, rd1, ADimm (b, n))))
            else (
              if debug then eprintf "LDP_W_BACK_SPACED_PEEP_IMM_DEC\n";
              insta.(i) <- PLoad (Pldp (Pldpw, rd1, r, ADimm (b, n1)))))
    (* Non-consecutive ldrx *)
    | PLoad (PLd_rd_a (Pldrx, IR (RR1 rd1), ADimm (b1, n1))), _ -> (
        match search_compat_rep_inv rd1 b1 n1 insta !pot_ldrx_rep "ldrx" with
        | None -> pot_ldrx_rep := i :: !pot_ldrx_rep
        | Some (rep, r, b, n) ->
            let filt x = x != rep in
            pot_ldrx_rep := List.filter filt !pot_ldrx_rep;
            insta.(rep) <- Pnop;
            if min_is_rev n n1 then (
              if debug then eprintf "LDP_X_BACK_SPACED_PEEP_IMM_INC\n";
              insta.(i) <- PLoad (Pldp (Pldpx, r, rd1, ADimm (b, n))))
            else (
              if debug then eprintf "LDP_X_BACK_SPACED_PEEP_IMM_DEC\n";
              insta.(i) <- PLoad (Pldp (Pldpx, rd1, r, ADimm (b, n1)))))
    (* Non-consecutive stpw *)
    | PStore (PSt_rs_a (Pstrw, IR (RR1 rs1), ADimm (b1, n1))), _ -> (
        match search_compat_rep_inv rs1 b1 n1 insta !pot_strw_rep "strw" with
        | None -> pot_strw_rep := i :: !pot_strw_rep
        | Some (rep, r, b, n) ->
            let filt x = x != rep in
            pot_strw_rep := List.filter filt !pot_strw_rep;
            insta.(rep) <- Pnop;
            if debug then eprintf "STP_W_BACK_SPACED_PEEP_IMM_INC\n";
            insta.(i) <- PStore (Pstp (Pstpw, r, rs1, ADimm (b, n))))
    (* Non-consecutive stpx *)
    | PStore (PSt_rs_a (Pstrx, IR (RR1 rs1), ADimm (b1, n1))), _ -> (
        match search_compat_rep_inv rs1 b1 n1 insta !pot_strx_rep "strx" with
        | None -> pot_strx_rep := i :: !pot_strx_rep
        | Some (rep, r, b, n) ->
            let filt x = x != rep in
            pot_strx_rep := List.filter filt !pot_strx_rep;
            insta.(rep) <- Pnop;
            if debug then eprintf "STP_X_BACK_SPACED_PEEP_IMM_INC\n";
            insta.(i) <- PStore (Pstp (Pstpx, r, rs1, ADimm (b, n))))
    (* Any other inst *)
    | _, _ -> ()
  done

(* Main peephole function in forward style *)
let pair_rep insta =
  (* Each list below is a symbolic mem representation
   * for one type of inst. Lists contains integers which
   * are the indices of insts in the main array "insta". *)
  let pot_ldrw_rep = ref [] in
  let pot_ldrx_rep = ref [] in
  let pot_strw_rep = ref [] in
  let pot_strx_rep = ref [] in
  for i = 0 to Array.length insta - 2 do
    let h0 = insta.(i) in
    let h1 = insta.(i + 1) in
    (* Here we need to update every symbolic memory according to the matched inst *)
    update_pot_rep_basic h0 insta pot_ldrw_rep "ldrw" false;
    update_pot_rep_basic h0 insta pot_ldrx_rep "ldrx" false;
    update_pot_rep_basic h0 insta pot_strw_rep "strw" false;
    update_pot_rep_basic h0 insta pot_strx_rep "strx" false;
    match (h0, h1) with
    (* Consecutive ldrw *)
    | ( 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 min_is_rev n1 n2 then (
            if debug then eprintf "LDP_W_CONSEC_PEEP_IMM_INC\n";
            insta.(i) <- PLoad (Pldp (Pldpw, rd1, rd2, ADimm (b1, n1))))
          else (
            if debug then eprintf "LDP_W_CONSEC_PEEP_IMM_DEC\n";
            insta.(i) <- PLoad (Pldp (Pldpw, rd2, rd1, ADimm (b1, n2))));
          insta.(i + 1) <- Pnop)
    (* Consecutive ldrx *)
    | ( 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 min_is_rev n1 n2 then (
            if debug then eprintf "LDP_X_CONSEC_PEEP_IMM_INC\n";
            insta.(i) <- PLoad (Pldp (Pldpx, rd1, rd2, ADimm (b1, n1))))
          else (
            if debug then eprintf "LDP_X_CONSEC_PEEP_IMM_DEC\n";
            insta.(i) <- PLoad (Pldp (Pldpx, rd2, rd1, ADimm (b1, n2))));
          insta.(i + 1) <- Pnop)
    (* Non-consecutive ldrw *)
    | PLoad (PLd_rd_a (Pldrw, IR (RR1 rd1), ADimm (b1, n1))), _ -> (
        (* Search a previous compatible load *)
        match search_compat_rep rd1 b1 n1 insta !pot_ldrw_rep "ldrw" with
        (* If we can't find a candidate, add the current load as a potential future one *)
        | None -> pot_ldrw_rep := i :: !pot_ldrw_rep
        (* Else, perform the peephole *)
        | Some (rep, r, b, n) ->
            (* The two lines below are used to filter the elected candidate *)
            let filt x = x != rep in
            pot_ldrw_rep := List.filter filt !pot_ldrw_rep;
            insta.(rep) <- Pnop;
            if min_is_rev n n1 then (
              if debug then eprintf "LDP_W_FORW_SPACED_PEEP_IMM_INC\n";
              insta.(i) <- PLoad (Pldp (Pldpw, r, rd1, ADimm (b, n))))
            else (
              if debug then eprintf "LDP_W_FORW_SPACED_PEEP_IMM_DEC\n";
              insta.(i) <- PLoad (Pldp (Pldpw, rd1, r, ADimm (b, n1)))))
    (* Non-consecutive ldrx *)
    | PLoad (PLd_rd_a (Pldrx, IR (RR1 rd1), ADimm (b1, n1))), _ -> (
        match search_compat_rep rd1 b1 n1 insta !pot_ldrx_rep "ldrx" with
        | None -> pot_ldrx_rep := i :: !pot_ldrx_rep
        | Some (rep, r, b, n) ->
            let filt x = x != rep in
            pot_ldrx_rep := List.filter filt !pot_ldrx_rep;
            insta.(rep) <- Pnop;
            if min_is_rev n n1 then (
              if debug then eprintf "LDP_X_FORW_SPACED_PEEP_IMM_INC\n";
              insta.(i) <- PLoad (Pldp (Pldpx, r, rd1, ADimm (b, n))))
            else (
              if debug then eprintf "LDP_X_FORW_SPACED_PEEP_IMM_DEC\n";
              insta.(i) <- PLoad (Pldp (Pldpx, rd1, r, ADimm (b, n1)))))
    (* Consecutive strw *)
    | ( 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_W_CONSEC_PEEP_IMM_INC\n";
          insta.(i) <- PStore (Pstp (Pstpw, rs1, rs2, ADimm (b1, n1)));
          insta.(i + 1) <- Pnop (* When nothing can be optimized. *))
    (* Consecutive strx *)
    | ( 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_X_CONSEC_PEEP_IMM_INC\n";
          insta.(i) <- PStore (Pstp (Pstpx, rs1, rs2, ADimm (b1, n1)));
          insta.(i + 1) <- Pnop)
    (* Non-consecutive stpw *)
    | PStore (PSt_rs_a (Pstrw, IR (RR1 rs1), ADimm (b1, n1))), _ -> (
        match search_compat_rep rs1 b1 n1 insta !pot_strw_rep "strw" with
        | None -> pot_strw_rep := i :: !pot_strw_rep
        | Some (rep, r, b, n) ->
            let filt x = x != rep in
            pot_strw_rep := List.filter filt !pot_strw_rep;
            insta.(rep) <- Pnop;
            if debug then eprintf "STP_W_FORW_SPACED_PEEP_IMM_INC\n";
            insta.(i) <- PStore (Pstp (Pstpw, r, rs1, ADimm (b, n))))
    (* Non-consecutive stpx *)
    | PStore (PSt_rs_a (Pstrx, IR (RR1 rs1), ADimm (b1, n1))), _ -> (
        match search_compat_rep rs1 b1 n1 insta !pot_strx_rep "strx" with
        | None -> pot_strx_rep := i :: !pot_strx_rep
        | Some (rep, r, b, n) ->
            let filt x = x != rep in
            pot_strx_rep := List.filter filt !pot_strx_rep;
            insta.(rep) <- Pnop;
            if debug then eprintf "STP_X_FORW_SPACED_PEEP_IMM_INC\n";
            insta.(i) <- PStore (Pstp (Pstpx, r, rs1, ADimm (b, n))))
    (* Any other inst *)
    | _, _ -> ()
  done

(* Calling peephole if flag is set *)
let optimize_bdy (bdy : basic list) : basic list =
  if !Clflags.option_fcoalesce_mem then (
    let insta = Array.of_list bdy in
    pair_rep insta;
    pair_rep_inv 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