1 files changed, 20 insertions, 0 deletions
diff --git a/arm/CSE2deps.v b/arm/CSE2deps.v
new file mode 100644
index 00000000..9db51bbb
--- /dev/null
+++ b/arm/CSE2deps.v
@@ -0,0 +1,20 @@
+Require Import BoolEqual Coqlib.
+Require Import AST Integers Floats.
+Require Import Values Memory Globalenvs Events.
+Require Import Op.
+
+
+Definition can_swap_accesses_ofs ofsr chunkr ofsw chunkw :=
+     (0 <=? ofsw) && (ofsw <=? (Ptrofs.modulus - largest_size_chunk))
+  && (0 <=? ofsr) && (ofsr <=? (Ptrofs.modulus - largest_size_chunk))
+  && ((ofsw + size_chunk chunkw <=? ofsr) ||
+      (ofsr + size_chunk chunkr <=? ofsw)).
+
+Definition may_overlap chunk addr args chunk' addr' args' :=
+  match addr, addr', args, args' with
+  | (Aindexed ofs), (Aindexed ofs'),
+    (base :: nil), (base' :: nil) =>
+    if peq base base'
+    then negb (can_swap_accesses_ofs (Int.unsigned ofs') chunk' (Int.unsigned ofs) chunk)
+    else true  | _, _, _, _ => true
+  end.