diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-12-16 16:45:14 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-12-16 16:45:14 +0100 |
| commit | dc7ba7bf86828da813e60d60dc9627cbd6ddcf0e (patch) | |
| tree | a4fafd3becda28ca3d42e2b72067bb1785dd21ae /mppa_k1c | |
| parent | 34518ae5db9ca7c04d9ce5d90261ede3c9d0e550 (diff) | |
| download | compcert-kvx-dc7ba7bf86828da813e60d60dc9627cbd6ddcf0e.tar.gz compcert-kvx-dc7ba7bf86828da813e60d60dc9627cbd6ddcf0e.zip | |
swap load and store at disjoint offsets
Diffstat (limited to 'mppa_k1c')
| -rw-r--r-- | mppa_k1c/Asmblockdeps.v | 54 |
1 files changed, 53 insertions, 1 deletions
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 759b4396..2cdf9499 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -234,7 +234,8 @@ Definition disjoint_chunks Definition small_offset_threshold := 18446744073709551608. -Lemma store_swap : forall n1 n2 ofs1 ofs2 vs1 vs2 va m0 m1 m2 m1' m2', +Lemma store_store_disjoint_offsets : + 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 -> @@ -288,6 +289,57 @@ Proof. lia. Qed. +Lemma load_store_disjoint_offsets : + forall n1 n2 tm ofs1 ofs2 vs va m0 m1, + (disjoint_chunks ofs1 (store_chunk n1) ofs2 (load_chunk n2)) -> + (Ptrofs.unsigned ofs1) < small_offset_threshold -> + (Ptrofs.unsigned ofs2) < small_offset_threshold -> + store_eval (OStoreRRO n1 ofs1) [vs; va; Memstate m0] = Some (Memstate m1) -> + load_eval (OLoadRRO n2 tm ofs2) [va; Memstate m1] = + load_eval (OLoadRRO n2 tm ofs2) [va; Memstate m0]. +Proof. + intros until m1. + intros DISJOINT SMALL1 SMALL2 STORE0. + destruct vs as [v | ]; simpl in STORE0; try congruence. + destruct va as [base | ]; try congruence. + unfold exec_store_deps_offset in *. + unfold eval_offset in *; simpl in *. + unfold exec_load_deps_offset. + unfold Mem.storev, Mem.loadv in *. + destruct Ge in *. + unfold eval_offset in *. + unfold Val.offset_ptr in *. + destruct base as [ | | | | | wblock wpofs] in * ; try congruence. + destruct (Mem.store _ _ _ _) eqn:E0 in STORE0; try congruence. + inv STORE0. + assert ( + (Mem.load (load_chunk n2) m1 wblock + (Ptrofs.unsigned (Ptrofs.add wpofs ofs2))) = + (Mem.load (load_chunk n2) m0 wblock + (Ptrofs.unsigned (Ptrofs.add wpofs ofs2))) ) as LOADS. + { + eapply Mem.load_store_other. + eassumption. + right. + pose proof (size_chunk_positive (store_chunk n1)). + pose proof (size_chunk_positive (load_chunk n2)). + pose proof (size_chunk_small (store_chunk n1)). + pose proof (size_chunk_small (load_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; + change Ptrofs.modulus with 18446744073709551616 in *; + lia. + } + destruct (Mem.load _ m1 _ _) in *; destruct (Mem.load _ m0 _ _) in *; congruence. +Qed. + Definition goto_label_deps (f: function) (lbl: label) (vpc: val) := match label_pos lbl 0 (fn_blocks f) with | None => None |