blob: c0deacf042ff68ab4be13fe5b0b79ffca00b3184 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
|
(* *************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* David Monniaux CNRS, VERIMAG *)
(* *)
(* Copyright VERIMAG. All rights reserved. *)
(* This file is distributed under the terms of the INRIA *)
(* Non-Commercial License Agreement. *)
(* *)
(* *************************************************************)
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 (Ptrofs.unsigned ofs') chunk' (Ptrofs.unsigned ofs) chunk)
else true
| (Ainstack ofs), (Ainstack ofs'), _, _ =>
negb (can_swap_accesses_ofs (Ptrofs.unsigned ofs') chunk' (Ptrofs.unsigned ofs) chunk)
| _, _, _, _ => true
end.
|
