blob: 9db51bbb0e9d12a747715c64232de1992408b613 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
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.
|
