From 8781c27a16463fd8f83a9c6eaba7b76846bd296c Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 20 Jan 2021 16:46:52 +0100 Subject: Adding fp loads pair --- aarch64/Asmblockdeps.v | 43 ++++++++++++++++++++++++++++++------------- 1 file changed, 30 insertions(+), 13 deletions(-) (limited to 'aarch64/Asmblockdeps.v') diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v index e1d591df..8a2061de 100644 --- a/aarch64/Asmblockdeps.v +++ b/aarch64/Asmblockdeps.v @@ -1150,12 +1150,18 @@ Definition eval_addressing_rlocs_ld (ld: load_rd_a) (chunk: memory_chunk) (a: ad | ADpostincr base n => Op (Load (Oload1 ld chunk a)) (PReg (#base) @ PReg (pmem) @ Enil) end. -Definition trans_ldp_chunk (chunk: memory_chunk): load_rd_a := +Definition trans_ldp_chunk (chunk: memory_chunk) (r: dreg): load_rd_a := match chunk with - | Many32 => Pldrw_a + | Mint32 => Pldrw | Mint64 => Pldrx - | Many64 => Pldrx_a - | _ => Pldrw + | Mfloat32 => Pldrs + | Mfloat64 => Pldrd + | Many32 => Pldrw_a + | _ => (* This case should always correspond to Many64 *) + match r with + | IR _ => Pldrx_a + | FR _ => Pldrd_a + end end. Definition trans_stp_chunk (chunk: memory_chunk): store_rs_a := @@ -1171,10 +1177,10 @@ Definition trans_load (ldi: ld_instruction) := | PLd_rd_a ld r a => let lr := eval_addressing_rlocs_ld ld (chunk_load ld) a in [(#r, lr)] | Pldp ld r1 r2 chk1 chk2 a => - let ldi1 := trans_ldp_chunk chk1 in - let ldi2 := trans_ldp_chunk chk2 in + let ldi1 := trans_ldp_chunk chk1 r1 in + let ldi2 := trans_ldp_chunk chk2 r1 in let lr := eval_addressing_rlocs_ld ldi1 chk1 a in - let ofs := match chk1 with | Mint32 | Many32 => 4%Z | _ => 8%Z end in + let ofs := match chk1 with | Mint32 | Mfloat32 | Many32 => 4%Z | _ => 8%Z end in match a with | ADimm base n => let a' := (get_offset_addr a ofs) in @@ -1193,7 +1199,7 @@ Definition trans_store (sti: st_instruction) := let sti1 := trans_stp_chunk chk1 in let sti2 := trans_stp_chunk chk2 in let lr := eval_addressing_rlocs_st sti1 chk1 r1 a in - let ofs := match chk1 with | Mint32 | Many32 => 4%Z | _ => 8%Z end in + let ofs := match chk1 with | Mint32 | Mfloat32| Many32 => 4%Z | _ => 8%Z end in match a with | ADimm base n => let a' := (get_offset_addr a ofs) in @@ -1356,6 +1362,14 @@ Proof. intros; destruct r; discriminate. Qed. +Lemma dreg_not_pmem: forall (r: dreg), + (# r) <> pmem. +Proof. + intros; destruct r as [i|f]. + - destruct i. apply ireg_not_pmem. discriminate. + - apply freg_not_pmem. +Qed. + Ltac DPRM pr := destruct pr as [drDPRF|crDPRF|]; [destruct drDPRF as [irDPRF|frDPRF]; [destruct irDPRF |] @@ -1463,6 +1477,7 @@ Ltac discriminate_ppos := try apply ireg_not_pmem; try apply ireg_not_pc; try apply freg_not_pmem; + try apply dreg_not_pmem; try apply ireg_not_CN; try apply ireg_not_CZ; try apply ireg_not_CC; @@ -1706,10 +1721,10 @@ Proof. econstructor. Qed. -Lemma load_chunk_neutral: forall chk v, - interp_load (trans_ldp_chunk chk) v = v. +Lemma load_chunk_neutral: forall chk v r, + interp_load (trans_ldp_chunk chk r) v = v. Proof. - intros; destruct chk; simpl; reflexivity. + intros; destruct chk; destruct r; simpl; reflexivity. Qed. Theorem bisimu_basic rsr mr sr bi: @@ -1749,8 +1764,10 @@ Local Ltac preg_eq_discr r rd := try destruct (Mem.loadv _ _ _); simpl; auto; Simpl_exists sr; rewrite !load_chunk_neutral; try (rewrite !assign_diff; discriminate_ppos; reflexivity); - try (destruct base; discriminate_ppos); - repeat (try fold (ppos r); intros; Simpl_update). + try (destruct rd1 as [ir1|fr1]; try destruct ir1; destruct rd2 as [ir2|fr2]; try destruct ir2; + destruct base; discriminate_ppos); + repeat (try fold (ppos r); try fold (ppos r0); + try fold (ppos fr1); try fold (ppos fr2); intros; Simpl_update). - (* Store *) destruct st. + unfold exec_store, exec_store_rs_a, eval_addressing_rlocs_st, exp_eval; -- cgit