Module PointsTo

Require Cells.
Import
  Utf8
  Coqlib
  Maps
  Globalenvs
  AST
  Integers
  Values
  Cminor
  Csharpminorannot
  Util
  ToString
  ShareTree
  AdomLib
  AssocList
  Sets
  PExpr
  Cells.

Set Implicit Arguments.
Unset Elimination Schemes.

Definition PTSet : Type := BlockSet.t +⊤.

Instance ptset_gamma ge stk : gamma_op BlockSet.t block :=
  λ s b,
  ∃ ab, BlockSet.mem ab s ∧ block_of_ablock ge stk ab = Some b.

Instance ptset_leb : leb_op BlockSet.t := BSO.Sleb.

Instance ptset_leb_correct (ge:genv) (stk:list (temp_env * env)) :
  leb_op_correct BlockSet.t block (G:=ptset_gamma ge stk).

Instance ptset_join : join_op BlockSet.t _ := BSO.Sjoin.

Instance ptset_join_correct (ge:genv) (stk:list (temp_env * env)) :
  join_op_correct BlockSet.t BlockSet.t block (GA:=ptset_gamma ge stk) (GB:=ptset_gamma ge stk).

Inductive type : Type :=
| TyFloat | TySingle | TyLong
| TyZero | TyInt
| TyPtr `(PTSet)
| TyZPtr `(PTSet)
| TyIntPtr.

Definition type_of_int (i: int) : type :=
  if Int.eq Int.zero i
  then TyZero
  else TyInt.

Section TO_STRING.
Context {F V} (ge: Genv.t F V).

Local Instance string_of_ablock : ToString ablock :=
  AblockToString ge.

Instance string_of_type : ToString type :=
  λ ty,
  match ty with
  | TyFloat => "float"
  | TySingle => "single"
  | TyLong => "long"
  | TyZero => "null"
  | TyInt => "int"
  | TyPtr bs => "ptr(" ++ to_string bs ++ ")"
  | TyZPtr bs => "null-ptr(" ++ to_string bs ++ ")"
  | TyIntPtr => "int-or-ptr"
  end.

End TO_STRING.

Instance type_leb : leb_op type :=
  λ x x',
  match x, x' with
  | TyFloat, TyFloat
  | TySingle, TySingle
  | TyLong, TyLong
    => true
  | TyFloat, _ | _, TyFloat
  | TySingle, _ | _, TySingle
  | TyLong, _ | _, TyLong
    => false
  | TyZero, (TyZero | TyInt | TyZPtr _ | TyIntPtr) => true
  | TyZero, TyPtr _ => false
  | TyInt, (TyInt | TyIntPtr) => true
  | TyInt, (TyZero | TyPtr _ | TyZPtr _) => false
  | TyPtr b, (TyPtr b' | TyZPtr b')
  | TyZPtr b, (TyZPtr b') => b ⊑ b'
  | (TyPtr _ | TyZPtr _), TyIntPtr => true
  | TyPtr _, (TyZero | TyInt) => false
  | TyZPtr _, (TyZero | TyInt | TyPtr _) => false
  | TyIntPtr, TyIntPtr => true
  | TyIntPtr, (TyZero | TyInt | TyPtr _ | TyZPtr _) => false
  end.

Instance type_join : join_op type (type+⊤) :=
  λ x x',
  match x, x' with
  | TyFloat, TyFloat
  | TySingle, TySingle
  | TyLong, TyLong
  | TyZero, TyZero
  | TyInt, TyInt
  | TyIntPtr, TyIntPtr
    => ret x
  | TyFloat, _ | _, TyFloat
  | TySingle, _ | _, TySingle
  | TyLong, _ | _, TyLong
    => ⊤
  | (TyZero | TyInt), TyIntPtr
  | TyZero, TyInt
    => ret x'
  | (TyInt | TyIntPtr), TyZero
  | TyIntPtr, TyInt
    => ret x
  | (TyPtr b | TyZPtr b), TyZero
  | TyZero, (TyPtr b | TyZPtr b) => ret (TyZPtr b)
  | (TyPtr _ | TyZPtr _), (TyInt | TyIntPtr)
  | (TyInt | TyIntPtr), (TyPtr _ | TyZPtr _) => ret TyIntPtr
  | TyPtr b, TyPtr b' => ret (TyPtr (b ⊔ b'))
  | TyZPtr b, TyPtr b'
  | TyPtr b, TyZPtr b'
  | TyZPtr b, TyZPtr b'
    => ret (TyZPtr (b ⊔ b'))
  end.

Instance type_gamma (G: gamma_op BlockSet.t block) : gamma_op type val :=
  λ x v,
  match x, v with
  | TyFloat, Vfloat _
  | TySingle, Vsingle _
  | TyLong, Vlong _
  | TyInt, Vint _
  | TyIntPtr, (Vint _ | Vptr _ _)
    => True

  | TyZero, Vint n => Int.eq Int.zero n
  | TyPtr bs, Vptr b _
  | TyZPtr bs, Vptr b _
    => b ∈ γ bs
  | TyZPtr _, Vint n => Int.eq Int.zero n

  | TyFloat, _
  | TySingle, _
  | TyLong, _
  | TyZero, _
  | TyInt, _
  | TyPtr _, _
  | TyZPtr _, _
  | TyIntPtr, _
    => False
  end.

Lemma type_gamma_inv G x v :
  type_gamma G x v →
  match x with
  | TyFloat => ∃ f, v = Vfloat f
  | TySingle => ∃ s, v = Vsingle s
  | TyLong => ∃ i, v = Vlong i
  | TyZero => v = Vint Int.zero
  | TyInt => ∃ i, v = Vint i
  | TyPtr bs => ∃ b i, v = Vptr b i ∧ b ∈ γ bs
  | TyZPtr bs => (v = Vint Int.zero) ∨ (∃ b i, v = Vptr b i ∧ b ∈ γ bs)
  | TyIntPtr => (∃ i, v = Vint i) ∨ (∃ b i, v = Vptr b i)
  end.

Lemma type_gamma_inv' G x v :
  type_gamma G x v →
  match v with
  | Vfloat _ => x = TyFloat
  | Vsingle _ => x = TySingle
  | Vlong _ => x = TyLong
  | Vptr b _ => (∃ bs, b ∈ γ bs ∧ (x = TyPtr bs ∨ x = TyZPtr bs)) ∨ (x = TyIntPtr)
  | Vint n => (n = Int.zero ∧ (x = TyZero ∨ ∃ bs, x = TyZPtr bs)) ∨ (x = TyInt) ∨ (x = TyIntPtr)
  | Vundef => False
  end.

Lemma toplift_gamma_def G x v :
  toplift_gamma (type_gamma G) x v →
  x = All ∨
  match v with Vundef => True | _ => ∃ ty, x = Just ty ∧ v ∈ type_gamma G ty end.

Instance type_leb_correct (G: gamma_op BlockSet.t block) (BS: leb_op_correct BlockSet.t block) :
  @leb_op_correct _ _ type_leb (type_gamma G).

Instance type_join_correct (G: gamma_op BlockSet.t block) (BS: join_op_correct BlockSet.t _ block) :
  @join_op_correct _ _ _ type_join (type_gamma G) _.

Module PT ( T : SHARETREE ).

Module ACTreeDom := WPFun T.

Definition points_to : Type := ACTreeDom.t type.

Definition points_to_get (pt: points_to) (c: T.elt) : type+⊤ :=
  ACTreeDom.get c pt.
Coercion points_to_get : points_to >-> Funclass.

Instance points_to_leb : leb_op points_to :=
  ACTreeDom.leb_tree _ _.

Instance points_to_join : join_op points_to points_to :=
  ACTreeDom.join_tree _ _.

Definition points_to_widen : points_to → points_to → points_to := join.

Instance points_to_gamma ge stk : gamma_op points_to (T.elt → val) :=
  ACTreeDom.gamma_tree (type_gamma (ptset_gamma ge stk)).

Instance points_to_leb_correct ge stk :
  @leb_op_correct _ _ points_to_leb (points_to_gamma ge stk).

Instance points_to_join_correct ge stk :
  @join_op_correct _ _ _ points_to_join (points_to_gamma ge stk) (points_to_gamma ge stk).

Section PT_EVAL.

Context (ge: genv) (μ: fname) (pt: points_to).
Fixpoint pt_eval_pexpr (pe: pexpr T.elt) : type+⊤ :=
  match pe with
  | PEvar x _ => ACTreeDom.get x pt
  | PElocal s => Just (TyPtr (Just (BSO.singleton (ABlocal μ s))))
  | PEconst (Ointconst i) _ _ => Just (type_of_int i)
  | PEconst (Ofloatconst _) _ _ => Just TyFloat
  | PEconst (Osingleconst _) _ _ => Just TySingle
  | PEconst (Olongconst _) _ _ => Just TyLong
  | PEconst (Oaddrsymbol s _) _ _ =>
    Just (TyPtr
    match Genv.find_symbol ge s with
    | Some b => Just (BSO.singleton (ABglobal b))
    | None => All
    end)

  | PEunop op pe' _ _ =>
    Just
    match op with
    | Ocast8unsigned
    | Ocast8signed
    | Ocast16unsigned
    | Ocast16signed
      =>
      match pt_eval_pexpr pe' with
      | Just TyZero => TyZero
      | _ => TyInt
      end
    | Onegint | Onotint | Ointoffloat | Ointuoffloat | Ointofsingle | Ointuofsingle | Ointoflong => TyInt
    | Onegf | Oabsf | Ofloatofsingle | Ofloatofint | Ofloatofintu | Ofloatoflong | Ofloatoflongu => TyFloat
    | Onegfs | Oabsfs | Osingleoffloat | Osingleofint | Osingleofintu | Osingleoflong | Osingleoflongu => TySingle
    | Onegl | Onotl | Olongofint | Olongofintu | Olongoffloat | Olonguoffloat | Olongofsingle | Olonguofsingle => TyLong
    end

  | PEbinop op x y _ _ =>
    match op with
    | Oadd =>
      do p <- pt_eval_pexpr x;
      do q <- pt_eval_pexpr y;
      Just
      match p, q with
      | TyFloat, _ | _, TyFloat
      | TySingle, _ | _, TySingle
      | TyLong, _ | _, TyLong
        => TyZero
      | TyZero, k | k, TyZero => k
      | TyInt, TyZPtr _ | TyZPtr _, TyInt => TyIntPtr
      | TyInt, k | k, TyInt => k
      | TyPtr _, TyPtr _ => TyZero
      | TyPtr _ as k, (TyZPtr _ | TyIntPtr) | (TyZPtr _ | TyIntPtr), TyPtr _ as k => k
      | TyZPtr bs, TyZPtr bs' => TyZPtr (bs ⊔ bs')
      | TyIntPtr, TyIntPtr
      | TyIntPtr, TyZPtr _
      | TyZPtr _, TyIntPtr => TyIntPtr
      end

    | Osub =>
      do p <- pt_eval_pexpr x;
      do q <- pt_eval_pexpr y;
      Just
      match p, q with
      | TyFloat, _ | _, TyFloat
      | TySingle, _ | _, TySingle
      | TyLong, _ | _, TyLong
        => TyZero
      | TyZero, k | k, TyZero => k
      | TyInt, _
      | TyPtr _, TyPtr _
      | TyZPtr _, TyPtr _ => TyInt
      | (TyPtr _ | TyIntPtr), TyInt => p
      | TyPtr _, (TyZPtr _ | TyIntPtr)
      | TyZPtr _, (TyInt | TyZPtr _ | TyIntPtr)
      | TyIntPtr, _
        => TyIntPtr
      end

    | Omul
    | Odiv | Odivu | Omod | Omodu
    | Oand | Oor | Oxor | Oshl | Oshr | Oshru
    | Ocmp _
    | Ocmpu _
      => Just TyInt
    | Oaddf | Osubf | Omulf | Odivf => Just TyFloat
    | Oaddfs | Osubfs | Omulfs | Odivfs => Just TySingle
    | Oaddl | Osubl | Omull | Odivl | Odivlu | Omodl | Omodlu
    | Oandl | Oorl | Oxorl | Oshll | Oshrl | Oshrlu => Just TyLong
    | Ocmpf _ | Ocmpfs _ | Ocmpl _ | Ocmplu _ => Just TyInt
    end
  end.

Definition env_as_fun : env → ident → option block :=
  λ e i, match e ! i with Some (b, _) => Some b | _ => None end.
Coercion env_as_fun : env >-> Funclass.

Lemma int_eq_intro (P: bool → Prop) :
  ∀ x y,
    (x = y → P true) →
    (x ≠ y → P false) →
    P (Int.eq x y).

Context (m: Memory.mem) (stk: list (temp_env * env)) (ρ: T.elt → val) (ε: env) (tmp: temp_env).
Local Instance __ptset_gamma : gamma_op BlockSet.t block := ptset_gamma ge ((tmp, ε) :: stk).
Local Instance __ptset_join_correct : join_op_correct BlockSet.t BlockSet.t block := @ptset_join_correct ge ((tmp, ε) :: stk).

Lemma pt_eval_pexpr_correct
      (Hstk: μ = plength stk)
      (PT: ρ ∈ points_to_gamma ge ((tmp, ε) :: stk) pt) :
  ∀ pe v,
    v ∈ eval_pexpr ge m ρ ε pe →
    match v with Vundef => False | _ => True end →
    v ∈ toplift_gamma (type_gamma __ptset_gamma) (pt_eval_pexpr pe).

End PT_EVAL.

End PT.