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/Asmblockdeps.v | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) (limited to 'aarch64/Asmblockdeps.v') 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 -- cgit