aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64/PeepholeOracle.ml
diff options
context:
space:
mode:
authorLéo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>2021-01-20 19:31:49 +0100
committerLéo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>2021-01-20 19:31:49 +0100
commit05c77498f8f6b6f47a4669e0da79ec6f685e6722 (patch)
tree58f3e1dd65110db080d102ded8867308d807412f /aarch64/PeepholeOracle.ml
parent8781c27a16463fd8f83a9c6eaba7b76846bd296c (diff)
downloadcompcert-kvx-05c77498f8f6b6f47a4669e0da79ec6f685e6722.tar.gz
compcert-kvx-05c77498f8f6b6f47a4669e0da79ec6f685e6722.zip
Adding fp stores pair
Diffstat (limited to 'aarch64/PeepholeOracle.ml')
-rw-r--r--aarch64/PeepholeOracle.ml63
1 files changed, 48 insertions, 15 deletions
diff --git a/aarch64/PeepholeOracle.ml b/aarch64/PeepholeOracle.ml
index ecb529d0..9e37b3c6 100644
--- a/aarch64/PeepholeOracle.ml
+++ b/aarch64/PeepholeOracle.ml
@@ -262,6 +262,8 @@ let trans_sti (sti : store_rs_a) : store_rs1_rs2_a =
match sti with
| Pstrw | Pstrw_a -> Pstpw
| Pstrx | Pstrx_a -> Pstpx
+ | Pstrs -> Pstps
+ | Pstrd | Pstrd_a -> Pstpd
| _ -> failwith "trans_sti: Found a non compatible store to translate"
let is_compat_load (ldi : load_rd_a) =
@@ -276,12 +278,14 @@ let are_compat_load (ldi1 : load_rd_a) (ldi2 : load_rd_a) =
| _ -> false
let is_compat_store (sti : store_rs_a) =
- match sti with Pstrw | Pstrw_a | Pstrx | Pstrx_a -> true | _ -> false
+ match sti with Pstrw | Pstrw_a | Pstrx | Pstrx_a | Pstrs | Pstrd | Pstrd_a -> true | _ -> false
let are_compat_store (sti1 : store_rs_a) (sti2 : store_rs_a) =
match sti1 with
| Pstrw | Pstrw_a -> ( match sti2 with Pstrw | Pstrw_a -> true | _ -> false)
| Pstrx | Pstrx_a -> ( match sti2 with Pstrx | Pstrx_a -> true | _ -> false)
+ | Pstrs -> (match sti2 with Pstrs -> true | _ -> false)
+ | Pstrd | Pstrd_a -> ( match sti2 with Pstrd | Pstrd_a -> true | _ -> false)
| _ -> false
let get_load_string (ldi : load_rd_a) =
@@ -295,7 +299,9 @@ let get_load_string (ldi : load_rd_a) =
let get_store_string (sti : store_rs_a) =
match sti with
| Pstrw | Pstrw_a -> "str32"
+ | Pstrs -> "str32f"
| Pstrx | Pstrx_a -> "str64"
+ | Pstrd | Pstrd_a -> "str64f"
| _ -> failwith "get_store_string: Found a non compatible store to translate"
let is_valid_ldr rd1 rd2 b1 b2 n1 n2 stype =
@@ -356,6 +362,8 @@ let pair_rep_inv insta =
let pot_ldrd_rep = ref [] in
let pot_strw_rep = ref [] in
let pot_strx_rep = ref [] in
+ let pot_strs_rep = ref [] in
+ let pot_strd_rep = ref [] in
for i = Array.length insta - 1 downto 1 do
let h0 = insta.(i) in
let h1 = insta.(i - 1) in
@@ -366,6 +374,8 @@ let pair_rep_inv insta =
update_pot_rep_basic h0 insta pot_ldrd_rep "ldr" true;
update_pot_rep_basic h0 insta pot_strw_rep "str" true;
update_pot_rep_basic h0 insta pot_strx_rep "str" true;
+ update_pot_rep_basic h0 insta pot_strs_rep "str" true;
+ update_pot_rep_basic h0 insta pot_strd_rep "str" true;
match (h0, h1) with
(* Non-consecutive ldr *)
| PLoad (PLd_rd_a (ldi, rd1, ADimm (b1, n1))), _ -> (
@@ -407,17 +417,23 @@ let pair_rep_inv insta =
| PStore (PSt_rs_a (sti, rd1, ADimm (b1, n1))), _ -> (
if is_compat_store sti then
let pot_rep =
- match sti with Pstrw | Pstrw_a -> pot_strw_rep | _ -> pot_strx_rep
+ match sti with
+ | Pstrw | Pstrw_a -> pot_strw_rep
+ | Pstrx | Pstrx_a -> pot_strx_rep
+ | Pstrs -> pot_strs_rep
+ | _ -> pot_strd_rep
in
(* Search a previous compatible store *)
+ let st_string = get_store_string sti in
match
- search_compat_rep_inv rd1 b1 n1 insta !pot_rep
- (get_store_string sti)
+ search_compat_rep_inv rd1 b1 n1 insta !pot_rep st_string
with
(* If we can't find a candidate, clean and add the current store as a potential future one *)
| None ->
pot_strw_rep := [];
pot_strx_rep := [];
+ pot_strs_rep := [];
+ pot_strd_rep := [];
pot_rep := i :: !pot_rep
(* Else, perform the peephole *)
| Some (rep, c, r, b, n) ->
@@ -425,7 +441,7 @@ let pair_rep_inv insta =
let filt x = x != rep in
pot_rep := List.filter filt !pot_rep;
insta.(rep) <- Pnop;
- if debug then eprintf "STP_BACK_SPACED_PEEP_IMM_INC\n";
+ if debug then eprintf "STP_BACK_SPACED_PEEP_IMM_INC_%s\n" st_string;
insta.(i) <-
PStore
(Pstp
@@ -436,7 +452,9 @@ let pair_rep_inv insta =
match i with
| PStore _ ->
pot_strw_rep := [];
- pot_strx_rep := []
+ pot_strx_rep := [];
+ pot_strs_rep := [];
+ pot_strd_rep := []
| _ -> ())
done
@@ -451,17 +469,20 @@ let pair_rep insta =
let pot_ldrd_rep = ref [] in
let pot_strw_rep = ref [] in
let pot_strx_rep = ref [] in
+ let pot_strs_rep = ref [] in
+ let pot_strd_rep = ref [] in
for i = 0 to Array.length insta - 2 do
- eprintf "DEBUG %d" (Array.length insta);
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 "ldr" false;
update_pot_rep_basic h0 insta pot_ldrx_rep "ldr" false;
- update_pot_rep_basic h0 insta pot_ldrs_rep "ldr" true;
- update_pot_rep_basic h0 insta pot_ldrd_rep "ldr" true;
+ update_pot_rep_basic h0 insta pot_ldrs_rep "ldr" false;
+ update_pot_rep_basic h0 insta pot_ldrd_rep "ldr" false;
update_pot_rep_basic h0 insta pot_strw_rep "str" false;
update_pot_rep_basic h0 insta pot_strx_rep "str" false;
+ update_pot_rep_basic h0 insta pot_strs_rep "str" false;
+ update_pot_rep_basic h0 insta pot_strd_rep "str" false;
match (h0, h1) with
(* Consecutive ldr *)
| ( PLoad (PLd_rd_a (ldi1, rd1, ADimm (b1, n1))),
@@ -536,9 +557,12 @@ let pair_rep insta =
* looking at two new store instructions. *)
pot_strw_rep := [];
pot_strx_rep := [];
+ pot_strs_rep := [];
+ pot_strd_rep := [];
if are_compat_store sti1 sti2 then
- if is_valid_str b1 b2 n1 n2 (get_store_string sti1) then (
- if debug then eprintf "STP_CONSEC_PEEP_IMM_INC\n";
+ let st_string = get_store_string sti1 in
+ if is_valid_str b1 b2 n1 n2 st_string then (
+ if debug then eprintf "STP_CONSEC_PEEP_IMM_INC_%s\n" st_string;
insta.(i) <-
PStore
(Pstp
@@ -553,16 +577,23 @@ let pair_rep insta =
| PStore (PSt_rs_a (sti, rd1, ADimm (b1, n1))), _ -> (
if is_compat_store sti then
let pot_rep =
- match sti with Pstrw | Pstrw_a -> pot_strw_rep | _ -> pot_strx_rep
+ match sti with
+ | Pstrw | Pstrw_a -> pot_strw_rep
+ | Pstrx | Pstrx_a -> pot_strx_rep
+ | Pstrs -> pot_strs_rep
+ | _ -> pot_strd_rep
in
(* Search a previous compatible store *)
+ let st_string = get_store_string sti in
match
- search_compat_rep rd1 b1 n1 insta !pot_rep (get_store_string sti)
+ search_compat_rep rd1 b1 n1 insta !pot_rep st_string
with
(* If we can't find a candidate, clean and add the current store as a potential future one *)
| None ->
pot_strw_rep := [];
pot_strx_rep := [];
+ pot_strs_rep := [];
+ pot_strd_rep := [];
pot_rep := i :: !pot_rep
(* Else, perform the peephole *)
| Some (rep, c, r, b, n) ->
@@ -570,7 +601,7 @@ let pair_rep insta =
let filt x = x != rep in
pot_rep := List.filter filt !pot_rep;
insta.(rep) <- Pnop;
- if debug then eprintf "STP_FORW_SPACED_PEEP_IMM_INC\n";
+ if debug then eprintf "STP_FORW_SPACED_PEEP_IMM_INC_%s\n" st_string;
insta.(i) <-
PStore
(Pstp (trans_sti sti, r, rd1, c, chunk_store sti, ADimm (b, n)))
@@ -581,7 +612,9 @@ let pair_rep insta =
match i with
| PStore _ ->
pot_strw_rep := [];
- pot_strx_rep := []
+ pot_strx_rep := [];
+ pot_strs_rep := [];
+ pot_strd_rep := []
| _ -> ())
done