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

Adding fp stores pair

parent 8781c27a
......@@ -278,7 +278,8 @@ Inductive instruction: Type :=
| Pstrs (rs: freg) (a: addressing) (**r store float32 *)
| Pstrd (rs: freg) (a: addressing) (**r store float64 *)
| Pstrd_a (rs: freg) (a: addressing) (**r store float64 as any64 *)
(* TODO *)
| Pstps (rd1 rd2: freg) (chk1 chk2: memory_chunk) (a: addressing) (**r store two float32 *)
| Pstpd (rd1 rd2: freg) (chk1 chk2: memory_chunk) (a: addressing) (**r store two float64 *)
(** Floating-point move *)
| Pfmov (rd r1: freg)
| Pfmovimms (rd: freg) (f: float32) (**r load float32 constant *)
......@@ -1275,10 +1276,10 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
exec_load_double chk1 chk2 (fun v => v) a rd1 rd2 rs m
| Pldpd rd1 rd2 chk1 chk2 a =>
exec_load_double chk1 chk2 (fun v => v) a rd1 rd2 rs m
(* TODO | Pstps rs1 rs2 chk1 chk2 a =>
| Pstps rs1 rs2 chk1 chk2 a =>
exec_store_double chk1 chk2 a rs#rs1 rs#rs2 rs m
| Pstpd rs1 rs2 chk1 chk2 a =>
exec_store_double chk1 chk2 a rs#rs1 rs#rs2 rs m *)
exec_store_double chk1 chk2 a rs#rs1 rs#rs2 rs m
| Pnop => Next (nextinstr rs) m
(** The following instructions and directives are not generated directly
by Asmgen, so we do not model them. *)
......
......@@ -136,7 +136,8 @@ Inductive store_rs_a : Type :=
Inductive store_rs1_rs2_a : Type :=
| Pstpw
| Pstpx
(* TODO *)
| Pstps
| Pstpd
.
Inductive st_instruction : Type :=
......
......@@ -1164,12 +1164,18 @@ Definition trans_ldp_chunk (chunk: memory_chunk) (r: dreg): load_rd_a :=
end
end.
Definition trans_stp_chunk (chunk: memory_chunk): store_rs_a :=
Definition trans_stp_chunk (chunk: memory_chunk) (r: dreg): store_rs_a :=
match chunk with
| Many32 => Pstrw_a
| Mint32 => Pstrw
| Mint64 => Pstrx
| Many64 => Pstrx_a
| _ => Pstrw
| Mfloat32 => Pstrs
| Mfloat64 => Pstrd
| Many32 => Pstrw_a
| _ => (* This case should always correspond to Many64 *)
match r with
| IR _ => Pstrx_a
| FR _ => Pstrd_a
end
end.
Definition trans_load (ldi: ld_instruction) :=
......@@ -1196,8 +1202,8 @@ Definition trans_store (sti: st_instruction) :=
| PSt_rs_a st r a =>
let lr := eval_addressing_rlocs_st st (chunk_store st) r a in [(pmem, lr)]
| Pstp st r1 r2 chk1 chk2 a =>
let sti1 := trans_stp_chunk chk1 in
let sti2 := trans_stp_chunk chk2 in
let sti1 := trans_stp_chunk chk1 r1 in
let sti2 := trans_stp_chunk chk2 r1 in
let lr := eval_addressing_rlocs_st sti1 chk1 r1 a in
let ofs := match chk1 with | Mint32 | Mfloat32| Many32 => 4%Z | _ => 8%Z end in
match a with
......
......@@ -354,6 +354,12 @@ Definition basic_to_instruction (b: basic) : res Asm.instruction :=
| PStore (Pstp Pstpx rs1 rs2 chk1 chk2 a) => do rs1' <- ireg_of_preg rs1;
do rs2' <- ireg_of_preg rs2;
OK (Asm.Pstpx rs1' rs2' chk1 chk2 a)
| PStore (Pstp Pstps rs1 rs2 chk1 chk2 a) => do rs1' <- freg_of_preg rs1;
do rs2' <- freg_of_preg rs2;
OK (Asm.Pstps rs1' rs2' chk1 chk2 a)
| PStore (Pstp Pstpd rs1 rs2 chk1 chk2 a) => do rs1' <- freg_of_preg rs1;
do rs2' <- freg_of_preg rs2;
OK (Asm.Pstpd rs1' rs2' chk1 chk2 a)
| Pallocframe sz linkofs => OK (Asm.Pallocframe sz linkofs)
| Pfreeframe sz linkofs => OK (Asm.Pfreeframe sz linkofs)
......
......@@ -2226,8 +2226,7 @@ Proof.
- apply senv_preserved.
- eexact transf_initial_states.
- eexact transf_final_states.
- (* TODO step_simulation *)
unfold match_states.
- unfold match_states.
simpl; intros; subst; eexists; split; eauto.
eapply step_simulation; eauto.
Qed.
......
......@@ -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
......
......@@ -421,6 +421,10 @@ module Target (*: TARGET*) =
fprintf oc " ldp %a, %a, %a\n" sreg rd1 sreg rd2 addressing a
| Pldpd(rd1, rd2, _, _, a) ->
fprintf oc " ldp %a, %a, %a\n" dreg rd1 dreg rd2 addressing a
| Pstps(rd1, rd2, _, _, a) ->
fprintf oc " stp %a, %a, %a\n" sreg rd1 sreg rd2 addressing a
| Pstpd(rd1, rd2, _, _, a) ->
fprintf oc " stp %a, %a, %a\n" dreg rd1 dreg rd2 addressing a
(* Floating-point move *)
| Pfmov(rd, r1) ->
fprintf oc " fmov %a, %a\n" dreg rd dreg r1
......
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