Module CSE2deps

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.

Definition is_condition_reflexive (cond: condition) : bool :=
  match cond with
  | Ccomp (Ceq | Cle | Cge)
  | Ccompu (Ceq | Cle | Cge) => true
  | Ccompl (Ceq | Cle | Cge)
  | Ccomplu (Ceq | Cle | Cge) => true
  | _ => false
  end.
           
Lemma is_condition_reflexive_sound:
  forall (cond: condition) (REFL : is_condition_reflexive cond = true)
         (v: val) (m: mem),
    eval_condition cond (v :: v :: nil) m <> Some false.