diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-12-10 23:06:17 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-12-10 23:06:17 +0100 |
| commit | ec1a33e664f3484772a06dcd7e3198aa80b5d993 (patch) | |
| tree | 12307fad767aa457d6b9a7391dac1ccc31523b77 /aarch64/Asmgenproof.v | |
| parent | 9d5f379cd9e36def513357363308f1e0b0f4e082 (diff) | |
| download | compcert-kvx-ec1a33e664f3484772a06dcd7e3198aa80b5d993.tar.gz compcert-kvx-ec1a33e664f3484772a06dcd7e3198aa80b5d993.zip | |
Big improvment in peephole, changing LDP/STP semantics
Diffstat (limited to 'aarch64/Asmgenproof.v')
| -rw-r--r-- | aarch64/Asmgenproof.v | 31 |
1 files changed, 16 insertions, 15 deletions
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. |