diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-12-16 14:45:56 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-12-16 14:45:56 +0100 |
| commit | 34518ae5db9ca7c04d9ce5d90261ede3c9d0e550 (patch) | |
| tree | 55ff51a36cceab452cef2f8fae43a359639ea37b /mppa_k1c | |
| parent | afa881c19f2dcc4494e0a0eb5cab92575f9c7aec (diff) | |
| download | compcert-kvx-34518ae5db9ca7c04d9ce5d90261ede3c9d0e550.tar.gz compcert-kvx-34518ae5db9ca7c04d9ce5d90261ede3c9d0e550.zip | |
swap stores at disjoint offsets
Diffstat (limited to 'mppa_k1c')
| -rw-r--r-- | mppa_k1c/Asmblockdeps.v | 46 |
1 files changed, 30 insertions, 16 deletions
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 4d53763c..759b4396 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -218,6 +218,12 @@ Proof. destruct chunk; simpl; lia. Qed. +Remark size_chunk_small: forall chunk, + (size_chunk chunk) <= 8. +Proof. + destruct chunk; simpl; lia. +Qed. + Definition disjoint_chunks (ofs1 : offset) (chunk1 : memory_chunk) (ofs2 : offset) (chunk2 : memory_chunk) := @@ -226,18 +232,20 @@ Definition disjoint_chunks ((Ptrofs.unsigned ofs2), ((Ptrofs.unsigned ofs2) + (size_chunk chunk2))). -(* THIS CANNOT BE PROVED DUE TO OVERFLOW WRAPPING -(* use something like load_store_other *) -Lemma store_swap : forall n1 n2 ofs1 ofs2 vs1 vs2 va m0 m0' m1 m2 m1' m2', +Definition small_offset_threshold := 18446744073709551608. + +Lemma store_swap : forall n1 n2 ofs1 ofs2 vs1 vs2 va m0 m1 m2 m1' m2', (disjoint_chunks ofs1 (store_chunk n1) ofs2 (store_chunk n2)) -> + (Ptrofs.unsigned ofs1) < small_offset_threshold -> + (Ptrofs.unsigned ofs2) < small_offset_threshold -> store_eval (OStoreRRO n1 ofs1) [vs1; va; Memstate m0] = Some (Memstate m1) -> store_eval (OStoreRRO n2 ofs2) [vs2; va; Memstate m1] = Some (Memstate m2) -> - store_eval (OStoreRRO n2 ofs2) [vs2; va; Memstate m0'] = Some (Memstate m1') -> + store_eval (OStoreRRO n2 ofs2) [vs2; va; Memstate m0] = Some (Memstate m1') -> store_eval (OStoreRRO n1 ofs1) [vs1; va; Memstate m1'] = Some (Memstate m2') -> m2 = m2'. Proof. intros until m2'. - intros DISJOINT STORE0 STORE1 STORE0' STORE1'. + intros DISJOINT SMALL1 SMALL2 STORE0 STORE1 STORE0' STORE1'. unfold disjoint_chunks in DISJOINT. destruct vs1 as [v1 | ]; simpl in STORE0, STORE1'; try congruence. destruct vs2 as [v2 | ]; simpl in STORE1, STORE0'; try congruence. @@ -261,18 +269,24 @@ Proof. rewrite <- E1. rewrite <- E1'. eapply Mem.store_store_other. - { - right. - pose proof (size_chunk_positive (store_chunk n1)). - pose proof (size_chunk_positive (store_chunk n2)). - destruct (Intv.range_disjoint _ _ DISJOINT) as [DIS | [DIS | DIS]]; - unfold Intv.empty in DIS; simpl in DIS. - 1, 2: lia. - destruct (Ptrofs.unsigned_add_either wpofs ofs1) as [R1 | R1]; rewrite R1; + 2, 3: eassumption. + + right. + pose proof (size_chunk_positive (store_chunk n1)). + pose proof (size_chunk_positive (store_chunk n2)). + pose proof (size_chunk_small (store_chunk n1)). + pose proof (size_chunk_small (store_chunk n2)). + destruct (Intv.range_disjoint _ _ DISJOINT) as [DIS | [DIS | DIS]]; + unfold Intv.empty in DIS; simpl in DIS. + 1, 2: lia. + pose proof (Ptrofs.unsigned_range ofs1). + pose proof (Ptrofs.unsigned_range ofs2). + unfold small_offset_threshold in *. + destruct (Ptrofs.unsigned_add_either wpofs ofs1) as [R1 | R1]; rewrite R1; destruct (Ptrofs.unsigned_add_either wpofs ofs2) as [R2 | R2]; rewrite R2; - try lia. - } -*) + change Ptrofs.modulus with 18446744073709551616 in *; + lia. +Qed. Definition goto_label_deps (f: function) (lbl: label) (vpc: val) := match label_pos lbl 0 (fn_blocks f) with |