Module PointsTo


Require Cells TypesDomain.
Import
  Utf8
  Coqlib
  Maps
  Globalenvs
  AST
  Values
  Csharpminor
  Util
  ShareTree
  AdomLib
  AssocList
  Sets
  PExpr
  TypesDomain
  Cells.

Set Implicit Arguments.

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

Instance ptset_gamma ge stk : gamma_op BlockSet.t val :=
  λ s i,
  match i with
         | Vptr b _ =>
           ∃ ab, BlockSet.mem ab s ∧ block_of_ablock ge stk ab = Some b
         | _ => True
         end.

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 val (G:=ptset_gamma ge stk).
Proof.
  intros x y H [| | | | |b i] X; auto.
  destruct X as (ab & IN & AB). exists ab. intuition.
  eapply BlockSet.le_spec; eauto.
Qed.

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 val (GA:=ptset_gamma ge stk) (GB:=ptset_gamma ge stk).
Proof.
  intros x y [|?|?|?|?|b ?] H; try now intuition.
  destruct H as [(ab & IN & AB)|(ab & IN & AB)]; exists ab; intuition;
  rewrite BlockSet.mem_union; apply orb_true_intro; rewrite IN; auto.
Qed.

Module PT ( T : SHARETREE ).

Module ACTreeDom := WPFun T.

Definition points_to : Type := ACTreeDom.t BlockSet.t.

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

Instance points_to_leb : leb_op points_to :=
  ACTreeDom.leb_tree _ _.
Proof.
  abstract now
  unfold leb, ptset_leb, BSO.Sleb, BlockSet.le;
  intros x;
  rewrite ABTree.shforall2_correct;
  intros x'; destruct ABTree.get.
Defined.

Instance points_to_join : join_op points_to points_to :=
  ACTreeDom.join_tree _ _.
Proof.
  abstract now
  intros x;
  unfold join, ptset_join, join_top_res, join, BSO.Sjoin, BlockSet.union;
  rewrite ABTree.shcombine_eq.
Defined.

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 (ptset_gamma ge stk).

Section PT_EVAL.

Context (ge: genv) (μ: fname) (pt: points_to).
Fixpoint pt_eval_pexpr (pe: pexpr T.elt) : PTSet :=
  match pe with
  | PEvar x _ => ACTreeDom.get x pt
  | PElocal s => Just (BSO.singleton (ABlocal μ s))
  | PEconst None _ => All
  | PEconst (Some (Oaddrsymbol s _)) _ =>
    match Genv.find_symbol ge s with
    | Some b => Just (BSO.singleton (ABglobal b))
    | None => Just BlockSet.empty
    end
  | PEconst (Some _) _ => Just BlockSet.empty
  | PEunop _ pe' _ => pt_eval_pexpr pe'
  | PEbinop _ x y _ =>
    do p <- pt_eval_pexpr x;
    do q <- pt_eval_pexpr y;
    ret (BlockSet.union p q)
  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 pt_eval_pexpr_correct m stk ρ ε tmp
      (Hstk: μ = plength stk)
      (PT: ρ ∈ points_to_gamma ge ((tmp, ε):: stk) pt) :
  ∀ pe,
  eval_pexpr ge m ρ ε pe ⊆ toplift_gamma (ptset_gamma ge ((tmp, ε) :: stk)) (pt_eval_pexpr pe).
Proof.
  induction pe; intros w W; eval_pexpr_inv; hsplit.
  - generalize (PT v). rewrite W. exact id.
  - subst w.
    eexists. split. apply BSO.mem_singleton. eauto. simpl.
    rewrite Hstk, get_stk_length. assumption.
  - destruct o as [()|]; eval_pexpr_inv; hsplit; try subst w; try exact I.
    simpl. destruct (Genv.find_symbol ge i) eqn:?. 2: exact I.
    eexists. split. apply BSO.mem_singleton. eauto. simpl. erewrite Genv.find_invert_symbol; eauto.
  - simpl.
    destruct w; try (destruct (pt_eval_pexpr pe); exact I).
    eelim (eval_pexpr_unop_ptr). eapply eval_PEunop with (ty:=VP); simpl; eauto.
  - repeat match goal with H : (∀ _ _, _), K : _ |- _ => specialize (H _ K) end.
    simpl. destruct (pt_eval_pexpr pe1) as [|p]. exact I.
    simpl. destruct (pt_eval_pexpr pe2) as [|q]. exact I.
    simpl in *.
    destruct b; eq_some_inv; subst;
    destruct v₁; simpl in *; eq_some_inv; try exact I; destruct v₂; eq_some_inv; try exact I;
    subst;
    try (unfold Val.cmp, Val.cmpu, Val.cmpf, Val.cmpfs; simpl; bif; exact I);
    try (revert H0; bif; intro; simpl in *; eq_some_inv; subst; exact I);
    try (
        unfold Val.cmpl, Val.cmplu, Val.cmpl_bool, Val.cmplu_bool in *;
        try (apply AbTy.if_opt in H0; hsplit; subst);
        simpl in *; eq_some_inv; subst;
        match goal with |- appcontext[ Val.of_bool ?b ] => destruct b; exact I end
      );
    try (unfold Val.cmpu; repeat (simpl; bif; try exact I); destruct c; exact I);
    hnf in *; hsplit; vauto.
    eexists. split. rewrite BlockSet.mem_union. bright. eauto. auto.
    eexists. split. rewrite BlockSet.mem_union. bleft. eauto. auto.
    eexists. split. rewrite BlockSet.mem_union. bleft. eauto. auto.
Qed.

End PT_EVAL.

End PT.

Generated by coq2html