From ec1a33e664f3484772a06dcd7e3198aa80b5d993 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Thu, 10 Dec 2020 23:06:17 +0100 Subject: Big improvment in peephole, changing LDP/STP semantics --- aarch64/Asmgenproof.v | 31 ++++++++++++++++--------------- 1 file changed, 16 insertions(+), 15 deletions(-) (limited to 'aarch64/Asmgenproof.v') diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index 793d94f9..a91ec285 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -1092,11 +1092,11 @@ Proof. + next_stuck_cong. Qed. -Lemma load_double_preserved n rs1 m1 rs1' m1' rs2 m2 rd1 rd2 chk f a: forall +Lemma load_double_preserved n rs1 m1 rs1' m1' rs2 m2 rd1 rd2 chk1 chk2 f a: forall (BOUNDED: 0 <= n <= Ptrofs.max_unsigned) (MATCHI: match_internal n (State rs1 m1) (State rs2 m2)) - (HLOAD: exec_load_double lk chk f a rd1 rd2 rs1 m1 = Next rs1' m1'), - exists (rs2' : regset) (m2' : mem), Asm.exec_load_double tge chk f a rd1 rd2 rs2 m2 = Next rs2' m2' + (HLOAD: exec_load_double lk chk1 chk2 f a rd1 rd2 rs1 m1 = Next rs1' m1'), + exists (rs2' : regset) (m2' : mem), Asm.exec_load_double tge chk1 chk2 f a rd1 rd2 rs2 m2 = Next rs2' m2' /\ match_internal (n + 1) (State rs1' m1') (State rs2' m2'). Proof. intros. @@ -1105,10 +1105,10 @@ Proof. erewrite <- !eval_addressing_preserved; eauto. destruct (is_pair_addressing_mode_correct a); try discriminate. destruct (Mem.loadv _ _ _); - destruct (Mem.loadv chk m2 + destruct (Mem.loadv chk2 m2 (eval_addressing lk - (get_offset_addr a match chk with - | Mint32 => 4 + (get_offset_addr a match chk1 with + | Mint32 | Many32 => 4 | _ => 8 end) rs1)); inversion HLOAD; auto. @@ -1141,11 +1141,11 @@ Proof. + next_stuck_cong. Qed. -Lemma store_double_preserved n rs1 m1 rs1' m1' rs2 m2 v1 v2 chk a: forall +Lemma store_double_preserved n rs1 m1 rs1' m1' rs2 m2 v1 v2 chk1 chk2 a: forall (BOUNDED: 0 <= n <= Ptrofs.max_unsigned) (MATCHI: match_internal n (State rs1 m1) (State rs2 m2)) - (HSTORE: exec_store_double lk chk a v1 v2 rs1 m1 = Next rs1' m1'), - exists (rs2' : regset) (m2' : mem), Asm.exec_store_double tge chk a v1 v2 rs2 m2 = Next rs2' m2' + (HSTORE: exec_store_double lk chk1 chk2 a v1 v2 rs1 m1 = Next rs1' m1'), + exists (rs2' : regset) (m2' : mem), Asm.exec_store_double tge chk1 chk2 a v1 v2 rs2 m2 = Next rs2' m2' /\ match_internal (n + 1) (State rs1' m1') (State rs2' m2'). Proof. intros. @@ -1154,12 +1154,13 @@ Proof. erewrite <- !eval_addressing_preserved; eauto. destruct (is_pair_addressing_mode_correct a); try discriminate. destruct (Mem.storev _ _ _ _); - try destruct (Mem.storev chk m - (eval_addressing lk - (get_offset_addr a match chk with - | Mint32 => 4 - | _ => 8 - end) rs1) v2); + try destruct (Mem.storev chk2 m + (eval_addressing lk + (get_offset_addr a + match chk1 with + | Mint32 | Many32 => 4 + | _ => 8 + end) rs1) v2); inversion HSTORE; auto. repeat (econstructor; eauto). * eapply nextinstr_agree_but_pc; intros. -- cgit