Commit bd818011 authored by Léo Gourdin's avatar Léo Gourdin
Browse files

Allowing non-consec store, and cleaning

parent ec1a33e6
......@@ -16,6 +16,7 @@ open Asm
open Int64
open Printf
(* If true, the oracle will print a msg for each applied peephole *)
let debug = false
(* Functions to verify the immediate offset range for ldp/stp *)
......@@ -208,6 +209,8 @@ let update_pot_rep_basic inst insta pot_rep stype rev =
pot_rep := read_symb_mem rs2 insta !pot_rep stype rev
| Pfnmul (_, rd, rs1, rs2) -> ())
| PLoad i -> (
(* Here, we consider a different behavior for load and store potential candidates:
* a load does not obviously cancel the ldp candidates, but it does for any stp candidate. *)
match stype with
| "ldr" -> (
match i with
......@@ -221,7 +224,11 @@ let update_pot_rep_basic inst insta pot_rep stype rev =
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 := []
| PStore _ -> (
(* Here, we consider that a store cancel all ldp candidates, but it is far more complicated for stp ones :
* if we cancel stp candidates here, we would prevent ourselves to apply the non-consec store peephole.
* To solve this issue, the store candidates cleaning is managed directly in the peephole function below. *)
match stype with "ldr" -> pot_rep := [] | _ -> ())
| Pallocframe (_, _) -> pot_rep := []
| Pfreeframe (_, _) -> pot_rep := []
| Ploadsymbol (rd, _) ->
......@@ -297,6 +304,8 @@ let min_is_rev n1 n2 =
let z2 = to_int (camlint64_of_coqint n2) in
if z1 < z2 then true else false
(* Below functions were added to merge pattern matching cases in peephole,
* thanks to this, we can make the chunk difference (int/any) compatible. *)
let trans_ldi (ldi : load_rd_a) : load_rd1_rd2_a =
match ldi with
| Pldrw | Pldrw_a -> Pldpw
......@@ -409,8 +418,11 @@ let pair_rep_inv insta =
search_compat_rep_inv rd1 b1 n1 insta !pot_rep
(get_store_string sti)
with
(* If we can't find a candidate, add the current store as a potential future one *)
| None -> pot_rep := i :: !pot_rep
(* 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_rep := i :: !pot_rep
(* Else, perform the peephole *)
| Some (rep, c, r, b, n) ->
(* The two lines below are used to filter the elected candidate *)
......@@ -420,9 +432,16 @@ let pair_rep_inv insta =
if debug then eprintf "STP_BACK_SPACED_PEEP_IMM_INC\n";
insta.(i) <-
PStore
(Pstp (trans_sti sti, r, rd1, c, chunk_store sti, ADimm (b, n)))
(Pstp
(trans_sti sti, rd1, r, chunk_store sti, c, ADimm (b, n1)))
(* Any other inst *))
| _, _ -> ()
| i, _ -> (
(* Clear list of candidates if there is a non supported store *)
match i with
| PStore _ ->
pot_strw_rep := [];
pot_strx_rep := []
| _ -> ())
done
(* Main peephole function in forward style *)
......@@ -505,6 +524,11 @@ let pair_rep insta =
(* Consecutive str *)
| ( PStore (PSt_rs_a (sti1, IR (RR1 rd1), ADimm (b1, n1))),
PStore (PSt_rs_a (sti2, IR (RR1 rd2), ADimm (b2, n2))) ) ->
(* Regardless of whether we can perform the peephole or not,
* we have to clean the potential candidates for stp now as we are
* looking at two new store instructions. *)
pot_strw_rep := [];
pot_strx_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";
......@@ -528,8 +552,11 @@ let pair_rep insta =
match
search_compat_rep rd1 b1 n1 insta !pot_rep (get_store_string sti)
with
(* If we can't find a candidate, add the current store as a potential future one *)
| None -> pot_rep := i :: !pot_rep
(* 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_rep := i :: !pot_rep
(* Else, perform the peephole *)
| Some (rep, c, r, b, n) ->
(* The two lines below are used to filter the elected candidate *)
......@@ -542,7 +569,13 @@ let pair_rep insta =
(Pstp (trans_sti sti, r, rd1, c, chunk_store sti, ADimm (b, n)))
)
(* Any other inst *)
| _, _ -> ()
| i, _ -> (
(* Clear list of candidates if there is a non supported store *)
match i with
| PStore _ ->
pot_strw_rep := [];
pot_strx_rep := []
| _ -> ())
done
(* Calling peephole if flag is set *)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment