(* This file is developed by Qinxiang Cao, Aquinas Hobor and Shengyi Wang in 2015. *)

Require Import VST.veric.base.
Require Import VST.veric.val_lemmas.
Require Import VST.veric.Memory.

Lemma range_overlap_spec: forall l1 n1 l2 n2,
  n1 > 0 ->
  n2 > 0 ->
  (range_overlap l1 n1 l2 n2 <-> adr_range l1 n1 l2 \/ adr_range l2 n2 l1).
Proof.
(* Goal: forall (p1 : val) (n1 : Z) (p2 : val) (n2 : Z) (_ : pointer_range_overlap p1 n1 p2 n2), and (isptr p1) (isptr p2) *)
  intros.
(* Goal: iff (range_overlap l1 n1 l2 n2) (or (adr_range l1 n1 l2) (adr_range l2 n2 l1)) *)
  unfold range_overlap, adr_range.
(* Goal: iff (@ex address (fun loc : address => and (let (b, ofs) := l1 in let (b', ofs') := loc in and (@eq block b b') (and (Z.le ofs ofs') (Z.lt ofs' (Z.add ofs n1)))) (let (b, ofs) := l2 in let (b', ofs') := loc in and (@eq block b b') (and (Z.le ofs ofs') (Z.lt ofs' (Z.add ofs n2)))))) (or (let (b, ofs) := l1 in let (b', ofs') := l2 in and (@eq block b b') (and (Z.le ofs ofs') (Z.lt ofs' (Z.add ofs n1)))) (let (b, ofs) := l2 in let (b', ofs') := l1 in and (@eq block b b') (and (Z.le ofs ofs') (Z.lt ofs' (Z.add ofs n2))))) *)
  destruct l1, l2.
(* Goal: forall (p1 : val) (n1 : Z) (p2 : val) (n2 : Z) (_ : pointer_range_overlap p1 n1 p2 n2), and (isptr p1) (isptr p2) *)
  split; intros.
  + destruct H1 as [[? ?] [[? ?] [? ?]]].
(* Goal: or (and (@eq block b b0) (and (Z.le z z0) (Z.lt z0 (Z.add z n1)))) (and (@eq block b0 b) (and (Z.le z0 z) (Z.lt z (Z.add z0 n2)))) *)
    subst.
(* Goal: or (and (@eq block b1 b1) (and (Z.le z z0) (Z.lt z0 (Z.add z n1)))) (and (@eq block b1 b1) (and (Z.le z0 z) (Z.lt z (Z.add z0 n2)))) *)
    destruct (zle z z0); [left | right].
    - split; auto.
(* Goal: and (Z.le z0 z) (Z.lt z (Z.add z0 n2)) *)
      omega.
    - split; auto.
(* Goal: and (Z.le z0 z) (Z.lt z (Z.add z0 n2)) *)
      omega.
  + destruct H1 as [[? ?] | [? ?]].
    - exists (b0, z0). repeat split; auto; omega.
    - exists (b, z). repeat split; auto; omega.
Qed.

Lemma range_overlap_comm: forall l1 n1 l2 n2, range_overlap l1 n1 l2 n2 -> range_overlap l2 n2 l1 n1.
Proof.
(* Goal: forall (l1 : address) (n1 : Z) (l2 : address) (n2 : Z) (_ : range_overlap l1 n1 l2 n2), and (Z.gt n1 Z0) (Z.gt n2 Z0) *)
  unfold range_overlap.
(* Goal: forall (p1 : val) (n1 : Z) (p2 : val) (n2 : Z) (_ : pointer_range_overlap p1 n1 p2 n2), and (isptr p1) (isptr p2) *)
  intros.
(* Goal: @ex address (fun loc : address => and (adr_range l2 n2 loc) (adr_range l1 n1 loc)) *)
  destruct H as [l ?].
(* Goal: @ex address (fun loc : address => and (adr_range l2 n2 loc) (adr_range l1 n1 loc)) *)
  exists l.
(* Goal: iff (pointer_range_overlap p1 n1 p2 n2) (pointer_range_overlap p2 n2 p1 n1) *)
  tauto.
Qed.

Lemma range_overlap_non_zero: forall l1 n1 l2 n2, range_overlap l1 n1 l2 n2 -> n1 > 0 /\ n2 > 0.
Proof.
(* Goal: forall (l1 : address) (n1 : Z) (l2 : address) (n2 : Z) (_ : range_overlap l1 n1 l2 n2), and (Z.gt n1 Z0) (Z.gt n2 Z0) *)
  unfold range_overlap.
(* Goal: forall (p1 : val) (n1 : Z) (p2 : val) (n2 : Z) (_ : pointer_range_overlap p1 n1 p2 n2), and (isptr p1) (isptr p2) *)
  intros.
(* Goal: and (Z.gt n1 Z0) (Z.gt n2 Z0) *)
  destruct H as [l [? ?]].
(* Goal: and (Z.gt n1 Z0) (Z.gt n2 Z0) *)
  apply adr_range_non_zero in H.
(* Goal: and (Z.gt n1 Z0) (Z.gt n2 Z0) *)
  apply adr_range_non_zero in H0.
(* Goal: range_overlap l n1 l' n2 *)
  auto.
Qed.

Definition pointer_range_overlap p n p' n' :=
  exists l l', val2adr p l /\ val2adr p' l' /\ range_overlap l n l' n'.

Lemma pointer_range_overlap_dec: forall p1 n1 p2 n2, {pointer_range_overlap p1 n1 p2 n2} + {~ pointer_range_overlap p1 n1 p2 n2}.
Proof.
(* Goal: forall (p1 : val) (n1 : Z) (p2 : val) (n2 : Z) (_ : pointer_range_overlap p1 n1 p2 n2), pointer_range_overlap p2 n2 p1 n1 *)
  unfold pointer_range_overlap.
(* Goal: forall (p1 : val) (n1 : Z) (p2 : val) (n2 : Z) (_ : pointer_range_overlap p1 n1 p2 n2), and (isptr p1) (isptr p2) *)
  intros.
  destruct p1;
  try solve
   [right;
    intros [[? ?] [[? ?] [HH [_ _]]]];
    inversion HH].
  destruct p2;
  try solve
   [right;
    intros [[? ?] [[? ?] [_ [HH _]]]];
    inversion HH].
(* Goal: sumbool (@ex address (fun l : address => @ex address (fun l' : address => and (val2adr (Vptr b i) l) (and (val2adr (Vptr b0 i0) l') (range_overlap l n1 l' n2))))) (not (@ex address (fun l : address => @ex address (fun l' : address => and (val2adr (Vptr b i) l) (and (val2adr (Vptr b0 i0) l') (range_overlap l n1 l' n2)))))) *)
  destruct (zlt 0 n1); [| right; intros [[? ?] [[? ?] [_ [_ HH]]]]; apply range_overlap_non_zero in HH; omega].
(* Goal: sumbool (@ex address (fun l : address => @ex address (fun l' : address => and (val2adr (Vptr b i) l) (and (val2adr (Vptr b0 i0) l') (range_overlap l n1 l' n2))))) (not (@ex address (fun l : address => @ex address (fun l' : address => and (val2adr (Vptr b i) l) (and (val2adr (Vptr b0 i0) l') (range_overlap l n1 l' n2)))))) *)
  destruct (zlt 0 n2); [| right; intros [[? ?] [[? ?] [_ [_ HH]]]]; apply range_overlap_non_zero in HH; omega].
(* Goal: sumbool (@ex address (fun l : address => @ex address (fun l' : address => and (val2adr (Vptr b i) l) (and (val2adr (Vptr b0 i0) l') (range_overlap l n1 l' n2))))) (not (@ex address (fun l : address => @ex address (fun l' : address => and (val2adr (Vptr b i) l) (and (val2adr (Vptr b0 i0) l') (range_overlap l n1 l' n2)))))) *)
  destruct (eq_block b b0).
  (*destruct (Clight_lemmas.block_eq_dec b b0).*)
  + subst b0.
(* Goal: sumbool (@ex address (fun l : address => @ex address (fun l' : address => and (val2adr (Vptr b i) l) (and (val2adr (Vptr b i0) l') (range_overlap l n1 l' n2))))) (not (@ex address (fun l : address => @ex address (fun l' : address => and (val2adr (Vptr b i) l) (and (val2adr (Vptr b i0) l') (range_overlap l n1 l' n2)))))) *)
    unfold val2adr.
    forget (Ptrofs.unsigned i) as i1;
    forget (Ptrofs.unsigned i0) as i2;
    clear i i0.
    destruct (range_dec i1 i2 (i1 + n1)); [| destruct (range_dec i2 i1 (i2 + n2))].
    - left.
(* Goal: and (@eq block b1 b1) (and (Z.le z0 z) (Z.lt z (Z.add z0 n2))) *)
      exists (b, i1), (b, i2); repeat split; auto.
(* Goal: and (Z.le z0 z) (Z.lt z (Z.add z0 n2)) *)
      apply range_overlap_spec; try omega.
(* Goal: range_overlap l n1 l' n2 *)
      left; simpl; auto.
    - left.
(* Goal: and (@eq block b1 b1) (and (Z.le z0 z) (Z.lt z (Z.add z0 n2))) *)
      exists (b, i1), (b, i2); repeat split; auto.
(* Goal: and (Z.le z0 z) (Z.lt z (Z.add z0 n2)) *)
      apply range_overlap_spec; try omega.
(* Goal: range_overlap l n1 l' n2 *)
      right; simpl; auto.
    - right.
(* Goal: not (@ex address (fun l : address => @ex address (fun l' : address => and (val2adr (Vptr b i) l) (and (val2adr (Vptr b0 i0) l') (range_overlap l n1 l' n2))))) *)
      intros [[? ?] [[? ?] [? [? HH]]]].
(* Goal: or (and (@eq block b b0) (and (Z.le z z0) (Z.lt z0 (Z.add z n1)))) (and (@eq block b0 b) (and (Z.le z0 z) (Z.lt z (Z.add z0 n2)))) *)
      inversion H; inversion H0; subst.
(* Goal: False *)
      apply range_overlap_spec in HH; [| omega | omega].
(* Goal: and (Z.le z0 z) (Z.lt z (Z.add z0 n2)) *)
      simpl in HH; omega.
  + right.
(* Goal: not (@ex address (fun l : address => @ex address (fun l' : address => and (val2adr (Vptr b i) l) (and (val2adr (Vptr b0 i0) l') (range_overlap l n1 l' n2))))) *)
    intros [[? ?] [[? ?] [? [? HH]]]].
(* Goal: False *)
    simpl in H, H0.
(* Goal: or (and (@eq block b b0) (and (Z.le z z0) (Z.lt z0 (Z.add z n1)))) (and (@eq block b0 b) (and (Z.le z0 z) (Z.lt z (Z.add z0 n2)))) *)
    inversion H; inversion H0; subst.
(* Goal: False *)
    apply range_overlap_spec in HH; [| omega | omega].
(* Goal: False *)
    simpl in HH.
(* Goal: False *)
    pose proof @eq_sym _ b0 b.
(* Goal: iff (pointer_range_overlap p1 n1 p2 n2) (pointer_range_overlap p2 n2 p1 n1) *)
    tauto.
Qed.

Lemma pointer_range_overlap_refl: forall p n1 n2,
  isptr p ->
  n1 > 0 ->
  n2 > 0 ->
  pointer_range_overlap p n1 p n2.
Proof.
(* Goal: forall (p1 : val) (n1 : Z) (p2 : val) (n2 : Z) (_ : pointer_range_overlap p1 n1 p2 n2), and (isptr p1) (isptr p2) *)
  intros.
(* Goal: pointer_range_overlap p n1 p n2 *)
  destruct p; try inversion H.
(* Goal: pointer_range_overlap (Vptr b i) n1 (Vptr b i) n2 *)
  exists (b, Ptrofs.unsigned i), (b, Ptrofs.unsigned i).
(* Goal: and (@eq block b1 b1) (and (Z.le z0 z) (Z.lt z (Z.add z0 n2))) *)
  repeat split; auto.
(* Goal: range_overlap l n1 l' n2 *)
  apply range_overlap_spec; auto.
(* Goal: or (adr_range (@pair block Z b (Ptrofs.unsigned i)) n1 (@pair block Z b (Ptrofs.unsigned i))) (adr_range (@pair block Z b (Ptrofs.unsigned i)) n2 (@pair block Z b (Ptrofs.unsigned i))) *)
  left.
(* Goal: adr_range (@pair block Z b (Ptrofs.unsigned i)) n1 (@pair block Z b (Ptrofs.unsigned i)) *)
  simpl.
(* Goal: and (Z.le z0 z) (Z.lt z (Z.add z0 n2)) *)
  split; auto; omega.
Qed.

Lemma pointer_range_overlap_comm: forall p1 n1 p2 n2,
  pointer_range_overlap p1 n1 p2 n2 <->
  pointer_range_overlap p2 n2 p1 n1.
Proof.
  cut (forall p1 n1 p2 n2,
         pointer_range_overlap p1 n1 p2 n2 ->
(* Goal: forall (_ : forall (p1 : val) (n1 : Z) (p2 : val) (n2 : Z) (_ : pointer_range_overlap p1 n1 p2 n2), pointer_range_overlap p2 n2 p1 n1) (p1 : val) (n1 : Z) (p2 : val) (n2 : Z), iff (pointer_range_overlap p1 n1 p2 n2) (pointer_range_overlap p2 n2 p1 n1) *)
(* Goal: forall (p1 : val) (n1 : Z) (p2 : val) (n2 : Z) (_ : pointer_range_overlap p1 n1 p2 n2), pointer_range_overlap p2 n2 p1 n1 *)
         pointer_range_overlap p2 n2 p1 n1). {
(* Goal: forall (p1 : val) (n1 : Z) (p2 : val) (n2 : Z) (_ : pointer_range_overlap p1 n1 p2 n2), and (isptr p1) (isptr p2) *)
    intros.
(* Goal: iff (pointer_range_overlap p1 n1 p2 n2) (pointer_range_overlap p2 n2 p1 n1) *)
    pose proof H p1 n1 p2 n2.
(* Goal: iff (pointer_range_overlap p1 n1 p2 n2) (pointer_range_overlap p2 n2 p1 n1) *)
    pose proof H p2 n2 p1 n1.
(* Goal: iff (pointer_range_overlap p1 n1 p2 n2) (pointer_range_overlap p2 n2 p1 n1) *)
    tauto.
  }
(* Goal: forall (p1 : val) (n1 : Z) (p2 : val) (n2 : Z) (_ : pointer_range_overlap p1 n1 p2 n2), pointer_range_overlap p2 n2 p1 n1 *)
  unfold pointer_range_overlap.
(* Goal: forall (p1 : val) (n1 : Z) (p2 : val) (n2 : Z) (_ : pointer_range_overlap p1 n1 p2 n2), and (isptr p1) (isptr p2) *)
  intros.
(* Goal: @ex address (fun l : address => @ex address (fun l' : address => and (val2adr p2 l) (and (val2adr p1 l') (range_overlap l n2 l' n1)))) *)
  destruct H as [l [l' [? [? ?]]]].
(* Goal: @ex address (fun l : address => @ex address (fun l' : address => and (val2adr p2 l) (and (val2adr p1 l') (range_overlap l n2 l' n1)))) *)
  exists l', l.
(* Goal: and (@eq block b1 b1) (and (Z.le z0 z) (Z.lt z (Z.add z0 n2))) *)
  repeat split; auto.
(* Goal: range_overlap l' n2 l n1 *)
  apply range_overlap_comm.
(* Goal: range_overlap l n1 l' n2 *)
  auto.
Qed.

Lemma pointer_range_overlap_non_zero: forall p1 n1 p2 n2,
  pointer_range_overlap p1 n1 p2 n2 -> n1 > 0 /\ n2 > 0.
Proof.
(* Goal: forall (p1 : val) (n1 : Z) (p2 : val) (n2 : Z) (_ : pointer_range_overlap p1 n1 p2 n2), and (isptr p1) (isptr p2) *)
  intros.
(* Goal: and (isptr p1) (isptr p2) *)
  destruct H as [? [? [? [? ?]]]].
(* Goal: range_overlap l n1 l' n2 *)
  eapply range_overlap_non_zero; eauto.
Qed.

Lemma pointer_range_overlap_isptr: forall p1 n1 p2 n2,
  pointer_range_overlap p1 n1 p2 n2 -> isptr p1 /\ isptr p2.
Proof.
(* Goal: forall (p1 : val) (n1 : Z) (p2 : val) (n2 : Z) (_ : pointer_range_overlap p1 n1 p2 n2), and (isptr p1) (isptr p2) *)
  intros.
(* Goal: and (isptr p1) (isptr p2) *)
  destruct H as [? [? [? [? ?]]]].
(* Goal: and (isptr p1) (isptr p2) *)
  destruct p1, p2; try solve [inversion H | inversion H0].
(* Goal: range_overlap l n1 l' n2 *)
  simpl; auto.
Qed.

