diff options
Diffstat (limited to 'aarch64/Asmblockdeps.v')
| -rw-r--r-- | aarch64/Asmblockdeps.v | 61 |
1 files changed, 42 insertions, 19 deletions
diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v index e1d591df..5cd049c5 100644 --- a/aarch64/Asmblockdeps.v +++ b/aarch64/Asmblockdeps.v @@ -1150,20 +1150,32 @@ 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 := +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) := @@ -1171,10 +1183,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 @@ -1190,10 +1202,10 @@ 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 | 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 +1368,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 +1483,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 +1727,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 +1770,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; |