Adding fp stores pair

1 files changed, 12 insertions, 6 deletions

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