Require Import Coqlib.
Require Import Maps.
Require Import IntvSets.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Globalenvs.
Require Import Events.
Require Import Lattice.
Require Import Registers.
Require Import ValueDomain.
Require Import Op.
Require Import RTL.

Neededness for values

Inductive nval : Type :=
  | Nothing (* value is entirely unused *)
  | I (m: int) (* only need the bits that are 1 in m *)
  | All. (* every bit of the value is used *)

Definition eq_nval (x y: nval) : {x=y} + {x<>y}.

Agreement between two values relative to a need.

Definition iagree (p q mask: int) : Prop :=
  forall i, 0 <= i < Int.zwordsize -> Int.testbit mask i = true ->
            Int.testbit p i = Int.testbit q i.

Fixpoint vagree (v w: val) (x: nval) {struct x}: Prop :=
  match x with
  | Nothing => True
  | I m =>
      match v, w with
      | Vint p, Vint q => iagree p q m
      | Vint p, _ => False
      | _, _ => True
      end
  | All => Val.lessdef v w
  end.

Lemma vagree_same: forall v x, vagree v v x.

Lemma vagree_lessdef: forall v w x, Val.lessdef v w -> vagree v w x.

Lemma lessdef_vagree: forall v w, vagree v w All -> Val.lessdef v w.

Hint Resolve vagree_same vagree_lessdef lessdef_vagree: na.

Inductive vagree_list: list val -> list val -> list nval -> Prop :=
  | vagree_list_nil: forall nvl,
      vagree_list nil nil nvl
  | vagree_list_default: forall v1 vl1 v2 vl2,
      vagree v1 v2 All -> vagree_list vl1 vl2 nil ->
      vagree_list (v1 :: vl1) (v2 :: vl2) nil
  | vagree_list_cons: forall v1 vl1 v2 vl2 nv1 nvl,
      vagree v1 v2 nv1 -> vagree_list vl1 vl2 nvl ->
      vagree_list (v1 :: vl1) (v2 :: vl2) (nv1 :: nvl).

Lemma lessdef_vagree_list:
  forall vl1 vl2, vagree_list vl1 vl2 nil -> Val.lessdef_list vl1 vl2.

Lemma vagree_lessdef_list:
  forall vl1 vl2, Val.lessdef_list vl1 vl2 -> forall nvl, vagree_list vl1 vl2 nvl.

Hint Resolve lessdef_vagree_list vagree_lessdef_list: na.

Ordering and least upper bound between value needs

Inductive nge: nval -> nval -> Prop :=
  | nge_nothing: forall x, nge All x
  | nge_all: forall x, nge x Nothing
  | nge_int: forall m1 m2,
      (forall i, 0 <= i < Int.zwordsize -> Int.testbit m2 i = true -> Int.testbit m1 i = true) ->
      nge (I m1) (I m2).

Lemma nge_refl: forall x, nge x x.

Hint Constructors nge: na.
Hint Resolve nge_refl: na.

Lemma nge_trans: forall x y, nge x y -> forall z, nge y z -> nge x z.

Lemma nge_agree:
  forall v w x y, nge x y -> vagree v w x -> vagree v w y.

Definition nlub (x y: nval) : nval :=
  match x, y with
  | Nothing, _ => y
  | _, Nothing => x
  | I m1, I m2 => I (Int.or m1 m2)
  | _, _ => All
  end.

Lemma nge_lub_l:
  forall x y, nge (nlub x y) x.

Lemma nge_lub_r:
  forall x y, nge (nlub x y) y.

Properties of agreement between integers

Lemma iagree_refl:
  forall p m, iagree p p m.

Remark eq_same_bits:
  forall i x y, x = y -> Int.testbit x i = Int.testbit y i.

Lemma iagree_and_eq:
  forall x y mask,
  iagree x y mask <-> Int.and x mask = Int.and y mask.

Lemma iagree_mone:
  forall p q, iagree p q Int.mone -> p = q.

Lemma iagree_zero:
  forall p q, iagree p q Int.zero.

Lemma iagree_and:
  forall x y n m,
  iagree x y (Int.and m n) -> iagree (Int.and x n) (Int.and y n) m.

Lemma iagree_not:
  forall x y m, iagree x y m -> iagree (Int.not x) (Int.not y) m.

Lemma iagree_not':
  forall x y m, iagree (Int.not x) (Int.not y) m -> iagree x y m.

Lemma iagree_or:
  forall x y n m,
  iagree x y (Int.and m (Int.not n)) -> iagree (Int.or x n) (Int.or y n) m.

Lemma iagree_bitwise_binop:
  forall sem f,
  (forall x y i, 0 <= i < Int.zwordsize ->
       Int.testbit (f x y) i = sem (Int.testbit x i) (Int.testbit y i)) ->
  forall x1 x2 y1 y2 m,
  iagree x1 y1 m -> iagree x2 y2 m -> iagree (f x1 x2) (f y1 y2) m.

Lemma iagree_shl:
  forall x y m n,
  iagree x y (Int.shru m n) -> iagree (Int.shl x n) (Int.shl y n) m.

Lemma iagree_shru:
  forall x y m n,
  iagree x y (Int.shl m n) -> iagree (Int.shru x n) (Int.shru y n) m.

Lemma iagree_shr_1:
  forall x y m n,
  Int.shru (Int.shl m n) n = m ->
  iagree x y (Int.shl m n) -> iagree (Int.shr x n) (Int.shr y n) m.

Lemma iagree_shr:
  forall x y m n,
  iagree x y (Int.or (Int.shl m n) (Int.repr Int.min_signed)) ->
  iagree (Int.shr x n) (Int.shr y n) m.

Lemma iagree_rol:
  forall p q m amount,
  iagree p q (Int.ror m amount) ->
  iagree (Int.rol p amount) (Int.rol q amount) m.

Lemma iagree_ror:
  forall p q m amount,
  iagree p q (Int.rol m amount) ->
  iagree (Int.ror p amount) (Int.ror q amount) m.

Lemma eqmod_iagree:
  forall m x y,
  Int.eqmod (two_p (Int.size m)) x y ->
  iagree (Int.repr x) (Int.repr y) m.

Definition complete_mask (m: int) := Int.zero_ext (Int.size m) Int.mone.

Lemma iagree_eqmod:
  forall x y m,
  iagree x y (complete_mask m) ->
  Int.eqmod (two_p (Int.size m)) (Int.unsigned x) (Int.unsigned y).

Lemma complete_mask_idem:
  forall m, complete_mask (complete_mask m) = complete_mask m.

Abstract operations over value needs.

Ltac InvAgree :=
  simpl vagree in *;
  repeat (
  auto || exact Logic.I ||
  match goal with
  | [ H: False |- _ ] => contradiction
  | [ H: match ?v with Vundef => _ | Vint _ => _ | Vlong _ => _ | Vfloat _ => _ | Vsingle _ => _ | Vptr _ _ => _ end |- _ ] => destruct v
  | [ |- context [if Archi.ptr64 then _ else _] ] => destruct Archi.ptr64 eqn:?
  end).


Definition andimm (x: nval) (n: int) :=
  match x with
  | Nothing => Nothing
  | I m => I (Int.and m n)
  | All => I n
  end.

Lemma andimm_sound:
  forall v w x n,
  vagree v w (andimm x n) ->
  vagree (Val.and v (Vint n)) (Val.and w (Vint n)) x.

Definition orimm (x: nval) (n: int) :=
  match x with
  | Nothing => Nothing
  | I m => I (Int.and m (Int.not n))
  | _ => I (Int.not n)
  end.

Lemma orimm_sound:
  forall v w x n,
  vagree v w (orimm x n) ->
  vagree (Val.or v (Vint n)) (Val.or w (Vint n)) x.


Definition bitwise (x: nval) := x.

Remark bitwise_idem: forall nv, bitwise (bitwise nv) = bitwise nv.

Lemma vagree_bitwise_binop:
  forall f,
  (forall p1 p2 q1 q2 m,
     iagree p1 q1 m -> iagree p2 q2 m -> iagree (f p1 p2) (f q1 q2) m) ->
  forall v1 w1 v2 w2 x,
  vagree v1 w1 (bitwise x) -> vagree v2 w2 (bitwise x) ->
  vagree (match v1, v2 with Vint i1, Vint i2 => Vint(f i1 i2) | _, _ => Vundef end)
         (match w1, w2 with Vint i1, Vint i2 => Vint(f i1 i2) | _, _ => Vundef end)
         x.

Lemma and_sound:
  forall v1 w1 v2 w2 x,
  vagree v1 w1 (bitwise x) -> vagree v2 w2 (bitwise x) ->
  vagree (Val.and v1 v2) (Val.and w1 w2) x.
Proof (vagree_bitwise_binop Int.and (iagree_bitwise_binop andb Int.and Int.bits_and)).

Lemma or_sound:
  forall v1 w1 v2 w2 x,
  vagree v1 w1 (bitwise x) -> vagree v2 w2 (bitwise x) ->
  vagree (Val.or v1 v2) (Val.or w1 w2) x.
Proof (vagree_bitwise_binop Int.or (iagree_bitwise_binop orb Int.or Int.bits_or)).

Lemma xor_sound:
  forall v1 w1 v2 w2 x,
  vagree v1 w1 (bitwise x) -> vagree v2 w2 (bitwise x) ->
  vagree (Val.xor v1 v2) (Val.xor w1 w2) x.
Proof (vagree_bitwise_binop Int.xor (iagree_bitwise_binop xorb Int.xor Int.bits_xor)).

Lemma notint_sound:
  forall v w x,
  vagree v w (bitwise x) -> vagree (Val.notint v) (Val.notint w) x.


Definition shlimm (x: nval) (n: int) :=
  match x with
  | Nothing => Nothing
  | I m => I (Int.shru m n)
  | All => I (Int.shru Int.mone n)
  end.

Lemma shlimm_sound:
  forall v w x n,
  vagree v w (shlimm x n) ->
  vagree (Val.shl v (Vint n)) (Val.shl w (Vint n)) x.

Definition shruimm (x: nval) (n: int) :=
  match x with
  | Nothing => Nothing
  | I m => I (Int.shl m n)
  | All => I (Int.shl Int.mone n)
  end.

Lemma shruimm_sound:
  forall v w x n,
  vagree v w (shruimm x n) ->
  vagree (Val.shru v (Vint n)) (Val.shru w (Vint n)) x.

Definition shrimm (x: nval) (n: int) :=
  match x with
  | Nothing => Nothing
  | I m => I (let m' := Int.shl m n in
              if Int.eq_dec (Int.shru m' n) m
              then m'
              else Int.or m' (Int.repr Int.min_signed))
  | All => I (Int.or (Int.shl Int.mone n) (Int.repr Int.min_signed))
  end.

Lemma shrimm_sound:
  forall v w x n,
  vagree v w (shrimm x n) ->
  vagree (Val.shr v (Vint n)) (Val.shr w (Vint n)) x.

Definition rol (x: nval) (amount: int) :=
  match x with
  | Nothing => Nothing
  | I m => I (Int.ror m amount)
  | All => All
  end.

Lemma rol_sound:
  forall v w x n,
  vagree v w (rol x n) ->
  vagree (Val.rol v (Vint n)) (Val.rol w (Vint n)) x.

Definition ror (x: nval) (amount: int) :=
  match x with
  | Nothing => Nothing
  | I m => I (Int.rol m amount)
  | All => All
  end.

Lemma ror_sound:
  forall v w x n,
  vagree v w (ror x n) ->
  vagree (Val.ror v (Vint n)) (Val.ror w (Vint n)) x.

Definition rolm (x: nval) (amount mask: int) := rol (andimm x mask) amount.

Lemma rolm_sound:
  forall v w x amount mask,
  vagree v w (rolm x amount mask) ->
  vagree (Val.rolm v amount mask) (Val.rolm w amount mask) x.


Definition modarith (x: nval) :=
  match x with
  | Nothing => Nothing
  | I m => I (complete_mask m)
  | All => All
  end.

Lemma add_sound:
  forall v1 w1 v2 w2 x,
  vagree v1 w1 (modarith x) -> vagree v2 w2 (modarith x) ->
  vagree (Val.add v1 v2) (Val.add w1 w2) x.

Remark modarith_idem: forall nv, modarith (modarith nv) = modarith nv.

Lemma mul_sound:
  forall v1 w1 v2 w2 x,
  vagree v1 w1 (modarith x) -> vagree v2 w2 (modarith x) ->
  vagree (Val.mul v1 v2) (Val.mul w1 w2) x.

Lemma neg_sound:
  forall v w x,
  vagree v w (modarith x) ->
  vagree (Val.neg v) (Val.neg w) x.


Definition zero_ext (n: Z) (x: nval) :=
  match x with
  | Nothing => Nothing
  | I m => I (Int.zero_ext n m)
  | All => I (Int.zero_ext n Int.mone)
  end.

Lemma zero_ext_sound:
  forall v w x n,
  vagree v w (zero_ext n x) ->
  0 <= n ->
  vagree (Val.zero_ext n v) (Val.zero_ext n w) x.

Definition sign_ext (n: Z) (x: nval) :=
  match x with
  | Nothing => Nothing
  | I m => I (Int.or (Int.zero_ext n m) (Int.shl Int.one (Int.repr (n - 1))))
  | All => I (Int.zero_ext n Int.mone)
  end.

Lemma sign_ext_sound:
  forall v w x n,
  vagree v w (sign_ext n x) ->
  0 < n < Int.zwordsize ->
  vagree (Val.sign_ext n v) (Val.sign_ext n w) x.


Definition store_argument (chunk: memory_chunk) :=
  match chunk with
  | Mint8signed | Mint8unsigned => I (Int.repr 255)
  | Mint16signed | Mint16unsigned => I (Int.repr 65535)
  | _ => All
  end.

Lemma store_argument_sound:
  forall chunk v w,
  vagree v w (store_argument chunk) ->
  list_forall2 memval_lessdef (encode_val chunk v) (encode_val chunk w).

Lemma store_argument_load_result:
  forall chunk v w,
  vagree v w (store_argument chunk) ->
  Val.lessdef (Val.load_result chunk v) (Val.load_result chunk w).


Definition maskzero (n: int) := I n.

Lemma maskzero_sound:
  forall v w n b,
  vagree v w (maskzero n) ->
  Val.maskzero_bool v n = Some b ->
  Val.maskzero_bool w n = Some b.


Definition default (x: nval) :=
  match x with
  | Nothing => Nothing
  | _ => All
  end.

Section DEFAULT.
Context `{memory_model_prf: Mem.MemoryModel}.

Variable ge: genv.
Variable sp: block.
Variables m1 m2: mem.
Hypothesis PERM: forall b ofs k p, Mem.perm m1 b ofs k p -> Mem.perm m2 b ofs k p.

Let valid_pointer_inj:
  forall b1 ofs b2 delta,
  inject_id b1 = Some(b2, delta) ->
  Mem.valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true ->
  Mem.valid_pointer m2 b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true.

Let weak_valid_pointer_inj:
  forall b1 ofs b2 delta,
  inject_id b1 = Some(b2, delta) ->
  Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true ->
  Mem.weak_valid_pointer m2 b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true.

Let weak_valid_pointer_no_overflow:
  forall b1 ofs b2 delta,
  inject_id b1 = Some(b2, delta) ->
  Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true ->
  0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned.

Let valid_different_pointers_inj:
  forall b1 ofs1 b2 ofs2 b1' delta1 b2' delta2,
  b1 <> b2 ->
  Mem.valid_pointer m1 b1 (Ptrofs.unsigned ofs1) = true ->
  Mem.valid_pointer m1 b2 (Ptrofs.unsigned ofs2) = true ->
  inject_id b1 = Some (b1', delta1) ->
  inject_id b2 = Some (b2', delta2) ->
  b1' <> b2' \/
  Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta1)) <> Ptrofs.unsigned (Ptrofs.add ofs2 (Ptrofs.repr delta2)).

Lemma default_needs_of_condition_sound:
  forall cond args1 b args2,
  eval_condition cond args1 m1 = Some b ->
  vagree_list args1 args2 nil ->
  eval_condition cond args2 m2 = Some b.

Lemma default_needs_of_operation_sound:
  forall op args1 v1 args2 nv,
  eval_operation ge (Vptr sp Ptrofs.zero) op args1 m1 = Some v1 ->
  vagree_list args1 args2 nil
  \/ vagree_list args1 args2 (default nv :: nil)
  \/ vagree_list args1 args2 (default nv :: default nv :: nil) ->
  nv <> Nothing ->
  exists v2,
     eval_operation ge (Vptr sp Ptrofs.zero) op args2 m2 = Some v2
  /\ vagree v1 v2 nv.

End DEFAULT.

Detecting operations that are redundant and can be turned into a move

Definition andimm_redundant (x: nval) (n: int) :=
  match x with
  | Nothing => true
  | I m => Int.eq_dec (Int.and m (Int.not n)) Int.zero
  | _ => false
  end.

Lemma andimm_redundant_sound:
  forall v w x n,
  andimm_redundant x n = true ->
  vagree v w (andimm x n) ->
  vagree (Val.and v (Vint n)) w x.

Definition orimm_redundant (x: nval) (n: int) :=
  match x with
  | Nothing => true
  | I m => Int.eq_dec (Int.and m n) Int.zero
  | _ => false
  end.

Lemma orimm_redundant_sound:
  forall v w x n,
  orimm_redundant x n = true ->
  vagree v w (orimm x n) ->
  vagree (Val.or v (Vint n)) w x.

Definition rolm_redundant (x: nval) (amount mask: int) :=
  Int.eq_dec amount Int.zero && andimm_redundant x mask.

Lemma rolm_redundant_sound:
  forall v w x amount mask,
  rolm_redundant x amount mask = true ->
  vagree v w (rolm x amount mask) ->
  vagree (Val.rolm v amount mask) w x.

Definition zero_ext_redundant (n: Z) (x: nval) :=
  match x with
  | Nothing => true
  | I m => Int.eq_dec (Int.zero_ext n m) m
  | _ => false
  end.

Lemma zero_ext_redundant_sound:
  forall v w x n,
  zero_ext_redundant n x = true ->
  vagree v w (zero_ext n x) ->
  0 <= n ->
  vagree (Val.zero_ext n v) w x.

Definition sign_ext_redundant (n: Z) (x: nval) :=
  match x with
  | Nothing => true
  | I m => Int.eq_dec (Int.zero_ext n m) m
  | _ => false
  end.

Lemma sign_ext_redundant_sound:
  forall v w x n,
  sign_ext_redundant n x = true ->
  vagree v w (sign_ext n x) ->
  0 < n ->
  vagree (Val.sign_ext n v) w x.

Neededness for register environments

Module NVal <: SEMILATTICE.

  Definition t := nval.
  Definition eq (x y: t) := (x = y).
  Definition eq_refl: forall x, eq x x := (@refl_equal t).
  Definition eq_sym: forall x y, eq x y -> eq y x := (@sym_equal t).
  Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := (@trans_equal t).
  Definition beq (x y: t) : bool := proj_sumbool (eq_nval x y).
  Lemma beq_correct: forall x y, beq x y = true -> eq x y.
  Definition ge := nge.
  Lemma ge_refl: forall x y, eq x y -> ge x y.
  Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z.
  Definition bot : t := Nothing.
  Lemma ge_bot: forall x, ge x bot.
  Definition lub := nlub.
  Lemma ge_lub_left: forall x y, ge (lub x y) x.
  Proof nge_lub_l.
  Lemma ge_lub_right: forall x y, ge (lub x y) y.
  Proof nge_lub_r.
End NVal.

Module NE := LPMap1(NVal).

Definition nenv := NE.t.

Definition nreg (ne: nenv) (r: reg) := NE.get r ne.

Definition eagree (e1 e2: regset) (ne: nenv) : Prop :=
  forall r, vagree e1#r e2#r (NE.get r ne).

Lemma nreg_agree:
  forall rs1 rs2 ne r, eagree rs1 rs2 ne -> vagree rs1#r rs2#r (nreg ne r).

Hint Resolve nreg_agree: na.

Lemma eagree_ge:
  forall e1 e2 ne ne',
  eagree e1 e2 ne -> NE.ge ne ne' -> eagree e1 e2 ne'.

Lemma eagree_bot:
  forall e1 e2, eagree e1 e2 NE.bot.

Lemma eagree_same:
  forall e ne, eagree e e ne.

Lemma eagree_update_1:
  forall e1 e2 ne v1 v2 nv r,
  eagree e1 e2 ne -> vagree v1 v2 nv -> eagree (e1#r <- v1) (e2#r <- v2) (NE.set r nv ne).

Lemma eagree_update:
  forall e1 e2 ne v1 v2 r,
  vagree v1 v2 (nreg ne r) ->
  eagree e1 e2 (NE.set r Nothing ne) ->
  eagree (e1#r <- v1) (e2#r <- v2) ne.

Lemma eagree_update_dead:
  forall e1 e2 ne v1 r,
  nreg ne r = Nothing ->
  eagree e1 e2 ne -> eagree (e1#r <- v1) e2 ne.

Neededness for memory locations

Inductive nmem : Type :=
  | NMemDead
  | NMem (stk: ISet.t) (gl: PTree.t ISet.t).


Section LOCATIONS.

Variable ge: genv.
Variable sp: block.

Inductive nlive: nmem -> block -> Z -> Prop :=
  | nlive_intro: forall stk gl b ofs
      (STK: b = sp -> ~ISet.In ofs stk)
      (GL: forall id iv,
           Genv.find_symbol ge id = Some b ->
           gl!id = Some iv ->
           ~ISet.In ofs iv),
      nlive (NMem stk gl) b ofs.


Definition nmem_all := NMem ISet.empty (PTree.empty _).

Lemma nlive_all: forall b ofs, nlive nmem_all b ofs.


Definition nmem_add (nm: nmem) (p: aptr) (sz: Z) : nmem :=
  match nm with
  | NMemDead => nmem_all (* very conservative, should never happen *)
  | NMem stk gl =>
      match p with
      | Gl id ofs =>
          match gl!id with
          | Some iv => NMem stk (PTree.set id (ISet.remove (Ptrofs.unsigned ofs) (Ptrofs.unsigned ofs + sz) iv) gl)
          | None => nm
          end
      | Glo id =>
          NMem stk (PTree.remove id gl)
      | Stk ofs =>
          NMem (ISet.remove (Ptrofs.unsigned ofs) (Ptrofs.unsigned ofs + sz) stk) gl
      | Stack =>
          NMem ISet.empty gl
      | _ => nmem_all
      end
  end.

Lemma nlive_add:
  forall bc b ofs p nm sz i,
  genv_match bc ge ->
  bc sp = BCstack ->
  pmatch bc b ofs p ->
  Ptrofs.unsigned ofs <= i < Ptrofs.unsigned ofs + sz ->
  nlive (nmem_add nm p sz) b i.

Lemma incl_nmem_add:
  forall nm b i p sz,
  nlive nm b i -> nlive (nmem_add nm p sz) b i.


Definition nmem_remove (nm: nmem) (p: aptr) (sz: Z) : nmem :=
  match nm with
  | NMemDead => NMemDead
  | NMem stk gl =>
    match p with
    | Gl id ofs =>
        let iv' :=
        match gl!id with
        | Some iv => ISet.add (Ptrofs.unsigned ofs) (Ptrofs.unsigned ofs + sz) iv
        | None => ISet.interval (Ptrofs.unsigned ofs) (Ptrofs.unsigned ofs + sz)
        end in
        NMem stk (PTree.set id iv' gl)
    | Stk ofs =>
        NMem (ISet.add (Ptrofs.unsigned ofs) (Ptrofs.unsigned ofs + sz) stk) gl
    | _ => nm
    end
  end.

Lemma nlive_remove:
  forall bc b ofs p nm sz b' i,
  genv_match bc ge ->
  bc sp = BCstack ->
  pmatch bc b ofs p ->
  nlive nm b' i ->
  b' <> b \/ i < Ptrofs.unsigned ofs \/ Ptrofs.unsigned ofs + sz <= i ->
  nlive (nmem_remove nm p sz) b' i.


Definition nmem_contains (nm: nmem) (p: aptr) (sz: Z) :=
  match nm with
  | NMemDead => false
  | NMem stk gl =>
      match p with
      | Gl id ofs =>
          match gl!id with
          | Some iv => negb (ISet.contains (Ptrofs.unsigned ofs) (Ptrofs.unsigned ofs + sz) iv)
          | None => true
          end
      | Stk ofs =>
          negb (ISet.contains (Ptrofs.unsigned ofs) (Ptrofs.unsigned ofs + sz) stk)
      | _ => true (* conservative answer *)
      end
  end.

Lemma nlive_contains:
  forall bc b ofs p nm sz i,
  genv_match bc ge ->
  bc sp = BCstack ->
  pmatch bc b ofs p ->
  nmem_contains nm p sz = false ->
  Ptrofs.unsigned ofs <= i < Ptrofs.unsigned ofs + sz ->
  ~(nlive nm b i).


Definition nmem_dead_stack (sz: Z) :=
  NMem (ISet.interval 0 sz) (PTree.empty _).

Lemma nlive_dead_stack:
  forall sz b' i, b' <> sp \/ ~(0 <= i < sz) -> nlive (nmem_dead_stack sz) b' i.


Definition nmem_lub (nm1 nm2: nmem) : nmem :=
  match nm1, nm2 with
  | NMemDead, _ => nm2
  | _, NMemDead => nm1
  | NMem stk1 gl1, NMem stk2 gl2 =>
      NMem (ISet.inter stk1 stk2)
           (PTree.combine
                (fun o1 o2 =>
                  match o1, o2 with
                  | Some iv1, Some iv2 => Some(ISet.inter iv1 iv2)
                  | _, _ => None
                  end)
                gl1 gl2)
  end.

Lemma nlive_lub_l:
  forall nm1 nm2 b i, nlive nm1 b i -> nlive (nmem_lub nm1 nm2) b i.

Lemma nlive_lub_r:
  forall nm1 nm2 b i, nlive nm2 b i -> nlive (nmem_lub nm1 nm2) b i.


Definition nmem_beq (nm1 nm2: nmem) : bool :=
  match nm1, nm2 with
  | NMemDead, NMemDead => true
  | NMem stk1 gl1, NMem stk2 gl2 => ISet.beq stk1 stk2 && PTree.beq ISet.beq gl1 gl2
  | _, _ => false
  end.

Lemma nmem_beq_sound:
  forall nm1 nm2 b ofs,
  nmem_beq nm1 nm2 = true ->
  (nlive nm1 b ofs <-> nlive nm2 b ofs).

End LOCATIONS.

The lattice for dataflow analysis

Module NA <: SEMILATTICE.

  Definition t := (nenv * nmem)%type.

  Definition eq (x y: t) :=
    NE.eq (fst x) (fst y) /\
    (forall ge sp b ofs, nlive ge sp (snd x) b ofs <-> nlive ge sp (snd y) b ofs).

  Lemma eq_refl: forall x, eq x x.
  Lemma eq_sym: forall x y, eq x y -> eq y x.
  Lemma eq_trans: forall x y z, eq x y -> eq y z -> eq x z.

  Definition beq (x y: t) : bool :=
    NE.beq (fst x) (fst y) && nmem_beq (snd x) (snd y).

  Lemma beq_correct: forall x y, beq x y = true -> eq x y.

  Definition ge (x y: t) : Prop :=
    NE.ge (fst x) (fst y) /\
    (forall ge sp b ofs, nlive ge sp (snd y) b ofs -> nlive ge sp (snd x) b ofs).

  Lemma ge_refl: forall x y, eq x y -> ge x y.
  Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z.

  Definition bot : t := (NE.bot, NMemDead).

  Lemma ge_bot: forall x, ge x bot.

  Definition lub (x y: t) : t :=
    (NE.lub (fst x) (fst y), nmem_lub (snd x) (snd y)).

  Lemma ge_lub_left: forall x y, ge (lub x y) x.
  Lemma ge_lub_right: forall x y, ge (lub x y) y.

End NA.