Adding fp stores pair

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