Module Cells

Require Import
  Coqlib AST Values Maps ShareTree Globalenvs Csharpminor Memory Hash Integers.

Require Import
  Utf8 String ToString DebugLib DebugCminor FastArith
  AdomLib Util TreeAl AssocList MemChunkTree Sets.

Require Import AbMemSignatureCsharpminor.

Notation fname := ident (only parsing).

Set Implicit Arguments.
Unset Elimination Schemes.

Inductive ablock :=
| ABlocal (f: fname) (l: ident)
| ABglobal (b: block)
.

Instance AblockToString (ge: genv) : ToString ablock :=
  (λ b, match b with
       | ABlocal f l => "Local(" ++ to_string f ++ ", " ++ string_of_ident l ++ ")"
       | ABglobal b => "Global(" ++ match Genv.invert_symbol ge b with Some s => string_of_ident s | None => "?" end ++ ")"
       end)%string.

Definition ablock_beq (x y: ablock) : bool :=
  match x, y with
  | ABlocal a b, ABlocal c d => match Pos.eqb a c with true => Pos.eqb b d | f => f end
  | ABglobal a, ABglobal b => Pos.eqb a b
  | _, _ => false
  end.

Lemma ablock_beq_correct :
  ∀ x y, ablock_beq x y = true <-> x = y.

Definition ablock_dec (x y: ablock) : { x = y } + { x ≠ y } :=
  eq_dec_of_beq ablock_beq ablock_beq_correct x y.
Instance AblockDec : EqDec ablock := ablock_dec.

Module Ablock : TYPE_EQ
with Definition s := ablock
with Definition t := (fname * ident + block)%type.

  Definition s := ablock.
  Definition t := (fname * ident + block)%type.
  Definition t_of_s (b: s) : t :=
    match b with
    | ABlocal f l => inl (f, l)
    | ABglobal b => inr b
    end.
  Definition s_of_t (x: t) : s :=
    match x with
    | inl (f, l) => ABlocal f l
    | inr b => ABglobal b
    end.
  Lemma s_of_t_of_s : forall x : s, s_of_t (t_of_s x) = x.
  Lemma t_of_s_of_t: forall x : t, t_of_s (s_of_t x) = x.
  Definition eq: forall (x y: s), {x = y} + {x <> y} := ablock_dec.
End Ablock.

Module _MTFI : SHARETREE with Definition elt := (fname * ident)%type
  := ProdShareTree(PShareTree)(PShareTree).
Module _MTFIB : SHARETREE with Definition elt := (fname * ident + block)%type
  := SumShareTree(_MTFI)(PShareTree).
Module ABTree : SHARETREE with Definition elt := ablock := BijShareTree(Ablock)(_MTFIB).
Module ABTreeDom := WPFun ABTree.
Existing Instance ABTreeDom.toString.
Module BlockSet := Tree2Set ABTree.
Module BSO := SetOp BlockSet.

Definition get_stk (f: fname) (stk: list (temp_env * env)) : option (temp_env * env) :=
  nth (rev stk) f.

Lemma get_stk_in {f stk r} : get_stk f stk = Some r → In r stk.

Lemma get_stk_length' pre a stk :
  get_stk (plength stk) (pre ++ a :: stk) = Some a.

Lemma get_stk_length a stk :
  get_stk (plength stk) (a :: stk) = Some a.

Lemma get_stk_cons n a b :
  get_stk n (a :: b) = if Pos.eqb n (plength b) then Some a else get_stk n b.

Lemma get_stk_lt n m a :
  get_stk n m = Some a →
  (n < plength m)%positive.

Definition get_stk_dep n m :
  { r |
    get_stk n m = Some (snd (fst r)) ∧
    (rev m = rev (fst (fst r) ++ snd (fst r) :: snd r) ∧
     Pos.eqb n (plength (snd r)))%list
  } +
  { (plength m <=? n ∧ get_stk n m = None )%positive }.

Lemma get_stk_app {x n y} :
  get_stk n (y ++ x) = if (n <? plength x)%positive then get_stk n x else get_stk (Pos.succ n - plength x)%positive y.

Lemma get_stk_tail e n m a :
  get_stk n m = Some a →
  get_stk n (e :: m) = Some a.

Lemma get_stk_nil n : get_stk n nil = None.

Lemma in_get_stk x y :
  In x y → ∃ n, get_stk n y = Some x.

Definition block_of_ablock (ge: genv) (stk: list (temp_env * env))
           (ab: ablock) : option block :=
  match ab with
  | ABlocal f l =>
    do (_, e) <- get_stk f stk;
    do (b, _) <- PTree.get l e;
    ret b
  | ABglobal b =>
    do s <- Genv.invert_symbol ge b;
    ret b
  end.

Definition size_ty_chunk (κ:typed_memory_chunk) := size_chunk (proj1_sig κ).

Inductive cell : Type :=
| AClocal (f: fname) (l: ident) (ofs: Z) (κ: typed_memory_chunk)
| ACtemp (f: fname) (r: ident)
| ACglobal (b: block) (ofs: Z) (κ: typed_memory_chunk)
.

Definition ablock_of_cell (c: cell) : ablock :=
  match c with
  | AClocal f l _ _ => ABlocal f l
  | ACglobal b _ _ => ABglobal b
  | ACtemp f r => ABglobal xH
  end.

Definition range : Type := (Z * typed_memory_chunk)%type.

Definition range_of_cell (c: cell) : range :=
  match c with
  | AClocal _ _ o κ
  | ACglobal _ o κ => (o, κ)
  | ACtemp _ _ => (0, exist _ Mint32 I)
  end.

Definition cell_from (b: ablock) (r: range) : cell :=
  match b with
  | ABlocal f l => AClocal f l (fst r) (snd r)
  | ABglobal b => ACglobal b (fst r) (snd r)
  end.

Lemma ablock_of_cell_from b r :
  ablock_of_cell (cell_from b r) = b.

Definition cell_beq (x y: cell) : bool :=
  match x, y return _ with
  | AClocal f l o κ, AClocal f' l' o' κ' =>
    Pos.eqb f f' && Pos.eqb l l' &&
    Z.eqb o o' && chunk_beq κ κ'
  | ACtemp f r, ACtemp f' r' =>
    Pos.eqb f f' && Pos.eqb r r'
  | ACglobal b o κ, ACglobal b' o' κ' =>
    Pos.eqb b b' && Z.eqb o o' && chunk_beq κ κ'
  | _, _ => false
  end.

Lemma cell_beq_correct x y :
  cell_beq x y ↔ x = y.

Instance CellToString (ge: genv): ToString cell :=
  λ c,
  match c with
  | ACtemp f r => ("Temp(" ++ to_string f ++ ", " ++ string_of_ident r ++")")%string
  | AClocal _ _ o κ
  | ACglobal _ o κ =>
    ("[" ++ to_string (ToString := AblockToString ge) (ablock_of_cell c) ++
               (if Z_zerop o then "" else ", " ++ to_string o) ++
               "]%" ++ to_string (proj1_sig κ))%string
  end.

Definition read_cell (ge: genv) (m: concrete_state) (c: cell) : option val :=
  match c with
  | AClocal f l ofs κ =>
    do (_, e) <- get_stk f (fst m);
    do (b, sz) <- PTree.get l e;
    Mem.load (proj1_sig κ) (snd m) b ofs
  | ACtemp f r =>
    do (t, _) <- get_stk f (fst m);
    PTree.get r t
  | ACglobal b ofs κ =>
    do s <- Genv.invert_symbol ge b;
    Mem.load (proj1_sig κ) (snd m) b ofs
  end.

Definition extend {A} (f: A → option val) : A → val :=
  λ a, match f a with Some v => v | None => Vundef end.
Arguments extend [A] f _ /.

Definition mem_as_fun ge (m: concrete_state) : cell → val :=
  extend (read_cell ge m).
Arguments mem_as_fun ge m _ /.

Lemma block_of_ablock_None ge m ab :
  block_of_ablock ge (fst m) ab = None →
  ∀ r, read_cell ge m (cell_from ab r) = None.

Lemma block_of_ablock_Some ge m ab b :
  block_of_ablock ge (fst m) ab = Some b →
  ∀ r, read_cell ge m (cell_from ab r) = Mem.load (proj1_sig (snd r)) (snd m) b (fst r).

Section OVERLAP.

Definition ranges_disjoint (a b: range) : Prop :=
  let '(i,c) := a in
  let '(j,d) := b in
  i + size_ty_chunk c <= j ∨ j + size_ty_chunk d <= i.

Definition ranges_overlap (a b: range) : Prop :=
  let '(i,c) := a in
  let '(j,d) := b in
  j < i + size_ty_chunk c ∧ i < j + size_ty_chunk d.

Remark ranges_disjoint_overlap a b :
  ranges_disjoint a b →
  ranges_overlap a b →
  ∀ P : Prop, P.

Lemma ranges_disjoint_dec a b :
  { ranges_disjoint a b } + { ranges_overlap a b }.
Global Opaque ranges_disjoint_dec.

Lemma ranges_disjoint_not_eq r r' :
  ranges_disjoint r r' → r ≠ r'.

Definition is_temp (c: cell) : bool :=
  match c with
  | ACtemp _ _ => true
  | _ => false
  end.

Definition cells_disjoint (a b: cell) : Prop :=
  is_temp a || is_temp b ∧ a ≠ b ∨
  ablock_of_cell a ≠ ablock_of_cell b ∨
  ranges_disjoint (range_of_cell a) (range_of_cell b).

Definition cells_overlap (a b: cell) : Prop :=
  (is_temp a || is_temp b = false ∨ a = b) ∧
  ablock_of_cell a = ablock_of_cell b ∧
  ranges_overlap (range_of_cell a) (range_of_cell b).

Remark cells_disjoint_overlap a b :
  cells_disjoint a b →
  cells_overlap a b →
  ∀ P : Prop, P.

Lemma cells_disjoint_not_eq c c' :
  cells_disjoint c c' → c ≠ c'.

Definition cells_disjoint_dec a b :
  { cells_disjoint a b } + { cells_overlap a b }.
  refine (
      (if (is_temp a || is_temp b) && negb (cell_beq a b) as q return _ = q → _
      then λ K, left (or_introl _)
      else
        λ K,
        match ablock_dec (ablock_of_cell a) (ablock_of_cell b) with
        | left EQ =>
          match ranges_disjoint_dec (range_of_cell a) (range_of_cell b) with
          | left D => left (or_intror (or_intror D))
          | right H => right (conj _ (conj EQ H))
          end
        | right NE => left (or_intror (or_introl NE))
        end) eq_refl).

Program Definition memory_chunk_fold {A} (f: A → typed_memory_chunk → A) (a: A) : A :=
  (f (f (f (f (f (f (f (f a Mint8signed) Mint8unsigned) Mint16signed) Mint16unsigned) Mint32) Mint64) Mfloat32) Mfloat64).

Definition overlap_aux (b: ablock) (ofs: Z) (κ': typed_memory_chunk) (n: N) (acc: list cell): list cell :=
  let base := ofs - size_ty_chunk κ' + 1 in
  N.peano_rect (λ _, list cell)
               acc
               (λ n,
                let ofs' := base + Z.of_N n in
                cons (cell_from b (ofs', κ'))
                )
               n.

Lemma overlap_aux_correct b ofs κ' c:
  ∀ n acc,
    In c (overlap_aux b ofs κ' n acc)
       ↔
    In c acc ∨
    ∃ ofs', c = cell_from b (ofs', κ') ∧ ofs' < ofs - size_ty_chunk κ' + Z.of_N n + 1 ∧ ofs < ofs' + size_ty_chunk κ'.

Definition overlap (c: cell) : list cell :=
  match c with
  | ACtemp _ _ => nil
  | AClocal _ _ ofs κ
  | ACglobal _ ofs κ =>
    let b := ablock_of_cell c in
    memory_chunk_fold
      (λ l κ',
       if eq_dec (proj1_sig κ) (proj1_sig κ')
       then
         overlap_aux b ofs κ (Z.to_N (size_ty_chunk κ - 1))
        (overlap_aux b (ofs + size_ty_chunk κ) κ (Z.to_N (size_ty_chunk κ - 1)) l)
       else overlap_aux b ofs κ' (Z.to_N (size_ty_chunk κ + size_ty_chunk κ' - 1)) l)
      nil
  end.

Lemma memory_chunk_fold_rec {A} (f: A -> typed_memory_chunk -> A) :
  ∀ (P:A -> Prop), (∀ x c, P x -> P (f x c)) ->
  ∀ x, P x -> P (memory_chunk_fold f x).

Lemma in_memory_chunk_fold {A} (f: list A → typed_memory_chunk → list A) :
  (∀ x c l, In x l → In x (f l c)) →
  ∀ x c, (∀ l, In x (f l c)) →
         ∀ l, In x (memory_chunk_fold f l).

Lemma overlap_correct' : ∀ c c', cells_overlap c c' → c ≠ c' → In c' (overlap c).

Lemma overlap_correct r r' : ¬ In r' (overlap r) → cells_disjoint r r' ∨ r = r'.

Global Opaque overlap.

End OVERLAP.

Module Cell : TYPE_EQ
with Definition s := cell
with Definition t := (fname * ident * Z * typed_memory_chunk + fname * ident + block * Z * typed_memory_chunk)%type.

  Definition s := cell.
  Definition t := (fname * ident * Z * typed_memory_chunk + fname * ident + block * Z * typed_memory_chunk)%type.
  Definition t_of_s (b: s) : t :=
    match b with
    | AClocal f l o κ => inl (inl (f, l, o, κ))
    | ACtemp f r => inl (inr (f, r))
    | ACglobal b o κ => inr (b, o, κ)
    end.
  Definition s_of_t (x: t) : s :=
    match x with
    | inl (inl (f, l, o, κ)) => AClocal f l o κ
    | inl (inr (f, r)) => ACtemp f r
    | inr (b, o, κ) => ACglobal b o κ
    end.
  Lemma s_of_t_of_s : forall x : s, s_of_t (t_of_s x) = x.
  Lemma t_of_s_of_t: forall x : t, t_of_s (s_of_t x) = x.
  Definition eq: forall (x y: s), {x = y} + {x <> y} :=
    eq_dec_of_beq cell_beq cell_beq_correct.
End Cell.

Module _MTFIZ : SHARETREE with Definition elt := (fname * ident * Z)%type
  := ProdShareTree(_MTFI)(ZShareTree).
Module _MTFIZC : SHARETREE with Definition elt := (fname * ident * Z * typed_memory_chunk)%type
  := ProdShareTree(_MTFIZ)(MemChunkTree).
Module _MTFIZCFI : SHARETREE with Definition elt := (fname * ident * Z * typed_memory_chunk + fname * ident)%type
  := SumShareTree(_MTFIZC)(_MTFI).
Module _MTBZ : SHARETREE with Definition elt := (block * Z)%type
  := ProdShareTree(PShareTree)(ZShareTree).
Module _MTBZC : SHARETREE with Definition elt := (block * Z * typed_memory_chunk)%type
  := ProdShareTree(_MTBZ)(MemChunkTree).
Module _MTFIZCFIBZC : SHARETREE with Definition elt := (fname * ident * Z * typed_memory_chunk + fname * ident + block * Z * typed_memory_chunk)%type
  := SumShareTree(_MTFIZCFI)(_MTBZC).

Module ACTree : SHARETREE with Definition elt := cell := BijShareTree(Cell)(_MTFIZCFIBZC).
Module CellSet : SET with Definition elt := cell := Tree2Set ACTree.
Module CSO := SetOp CellSet.

Instance ACellDec : EqDec cell := ACTree.elt_eq.

Definition set_product (bs: BlockSet.t) κ (offs: ZSet.t+⊤+⊥) : CellSet.t +⊤ :=
  match offs with
  | Bot => Just CellSet.empty
  | NotBot offs =>
    do offs <- offs;
    Just (BlockSet.fold
            (λ b cs, ZSet.fold (λ ofs cs, CellSet.add (cell_from b (ofs, κ)) cs) offs cs)
            bs
            CellSet.empty)
  end.

Lemma ztree_fold_union_In f acc x (is: ZSet.t) :
  ((∃i, In i (ZSet.elements is) ∧ x = f i) ∨ CellSet.mem x acc)
  ↔
  CellSet.mem x (ZSet.fold (λ i cs, CellSet.add (f i) cs) is acc).

Lemma set_product_correct :
  forall bs κ offs b i,
    BlockSet.mem b bs ->
    i ∈ γ offs ->
    match set_product bs κ offs with
    | All => True
    | Just res => CellSet.mem (cell_from b (Int.unsigned i, κ)) res
    end.

Instance hash_cell : hashable cell := fun (h:Nfast) (c:cell) =>
  match c with
  | AClocal x y z t =>
    hash (hash (hash (hash (MIX h F0) x) y) (z:Zfast)) t
  | ACtemp x y =>
    hash (hash (MIX h F1) x) y
  | ACglobal x y z =>
    hash (hash (hash (MIX h F2) (Npos x:Nfast)) (y:Zfast)) z
  end.


Inductive cmp_blockset_t := Equal (b: ablock) | Disjoint | DontKnow | Contradiction.

Definition cmp_blockset (x y: BlockSet.t) : cmp_blockset_t :=
  match BSO.classify x, BSO.classify y with
  | BSO.Empty, _ | _, BSO.Empty => Contradiction
  | BSO.Singleton v, BSO.Singleton w => if eq_dec v w then Equal v else Disjoint
  | _, _ => if BlockSet.le (BlockSet.inter x y) BlockSet.empty then Disjoint else DontKnow
  end.

Lemma cmp_blockset_correct x y v w :
  BlockSet.mem v x → BlockSet.mem w y →
  match cmp_blockset x y with
  | Equal b => v = b ∧ w = b
  | Disjoint => v ≠ w
  | DontKnow => True
  | Contradiction => False
  end.

Inductive min_size_t := MinSize | Size (z: Z) | MaxSize.
Definition size_of_option {A} (a: option (Z * A)) := match a with Some (a, _) => Size a | None => MinSize end.

Definition omin {A} (x: option (Z * A)) (y: min_size_t) : min_size_t :=
  match x, y with
  | None, _ => MinSize
  | _, MinSize => y
  | Some (x, _), Size y => Size (Z.min x y)
  | Some (x, _), MaxSize => Size x
  end.

Definition ozle (x y: min_size_t) : Prop :=
  match x, y with
  | MinSize, _ | _, MaxSize => True
  | MaxSize, _ | _, MinSize => False
  | Size x, Size y => Z.le x y
  end.

Remark ozle_refl : ∀ a, ozle a a.

Remark ozle_min_2 : ∀ A (a: option (Z * A)) b c,
  ozle (size_of_option a) c ∨ ozle b c →
  ozle (omin a b) c.

Definition min_size A (sz: ABTree.t (Z * A)) := BlockSet.fold (λ b, omin (ABTree.get b sz)).

Lemma min_size_min A (sz: ABTree.t (Z * A)) bs z:
  let m := min_size sz bs z in
  (∀ b, BlockSet.mem b bs → ozle m (size_of_option (ABTree.get b sz))) ∧ ozle m z.