may_overlap_sound

1 files changed, 38 insertions, 0 deletions

diff --git a/backend/CSE2proof.v b/backend/CSE2proof.v
index eeb9442f..206dbf30 100644
--- a/backend/CSE2proof.v
+++ b/backend/CSE2proof.v
@@ -735,6 +735,44 @@ Proof.
   }
 Qed.
 
+Lemma may_overlap_sound:
+  forall m m' : mem,
+  forall chunk addr args chunk' addr' args' v a a' vl rs,
+    (eval_addressing genv sp addr (rs ## args)) = Some a ->
+    (eval_addressing genv sp addr' (rs ## args')) = Some a' ->
+    (may_overlap chunk addr args chunk' addr' args') = false ->
+    (Mem.storev chunk m a v) = Some m' ->
+    (Mem.loadv chunk' m  a') = Some vl ->
+    (Mem.loadv chunk' m' a') = Some vl.
+Proof.
+  intros until rs.
+  intros ADDR ADDR' OVERLAP STORE LOAD.
+  destruct addr; destruct addr'; try discriminate.
+  { (* Aindexed / Aindexed *)
+  destruct args as [ | base [ | ]]. 1,3: discriminate.
+  destruct args' as [ | base' [ | ]]. 1,3: discriminate.
+  simpl in OVERLAP.
+  destruct (peq base base'). 2: discriminate.
+  subst base'.
+  destruct (can_swap_accesses_ofs z0 chunk' z chunk) eqn:SWAP.
+  2: discriminate.
+  simpl in *.
+  eapply load_store_away; eassumption.
+  }
+  { (* Aglobal / Aglobal *)
+    destruct args. 2: discriminate.
+    destruct args'. 2: discriminate.
+    simpl in *.
+    destruct (peq i i1).
+    {
+      subst i1.
+      rewrite negb_false_iff in OVERLAP.
+      eapply load_store_glob_away; eassumption.
+    }
+    eapply load_store_diff_globals; eassumption.
+  }
+Qed.
+  
 Lemma kill_store_sound :
   forall m m' : mem,
   forall rel : RELATION.t,