From 05c77498f8f6b6f47a4669e0da79ec6f685e6722 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 20 Jan 2021 19:31:49 +0100 Subject: Adding fp stores pair --- aarch64/Asm.v | 7 +++--- aarch64/Asmblock.v | 3 ++- aarch64/Asmblockdeps.v | 18 +++++++++----- aarch64/Asmgen.v | 6 +++++ aarch64/Asmgenproof.v | 3 +-- aarch64/PeepholeOracle.ml | 63 ++++++++++++++++++++++++++++++++++++----------- aarch64/TargetPrinter.ml | 4 +++ 7 files changed, 77 insertions(+), 27 deletions(-) diff --git a/aarch64/Asm.v b/aarch64/Asm.v index 85e5ed3a..5f109224 100644 --- a/aarch64/Asm.v +++ b/aarch64/Asm.v @@ -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. *) diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v index f5d2abbe..c606002a 100644 --- a/aarch64/Asmblock.v +++ b/aarch64/Asmblock.v @@ -136,7 +136,8 @@ Inductive store_rs_a : Type := Inductive store_rs1_rs2_a : Type := | Pstpw | Pstpx - (* TODO *) + | Pstps + | Pstpd . Inductive st_instruction : Type := diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v index 8a2061de..5cd049c5 100644 --- a/aarch64/Asmblockdeps.v +++ b/aarch64/Asmblockdeps.v @@ -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 diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v index b6aa4c70..45205158 100644 --- a/aarch64/Asmgen.v +++ b/aarch64/Asmgen.v @@ -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) diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index 23db2e92..d27b3f8c 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -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. 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 diff --git a/aarch64/TargetPrinter.ml b/aarch64/TargetPrinter.ml index 93cfa99c..9ec1d563 100644 --- a/aarch64/TargetPrinter.ml +++ b/aarch64/TargetPrinter.ml @@ -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 -- cgit