Module IntOrPtrDomain

Abstract domain for simple type reconstruction in CFG.

Require Import Coqlib.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Op.
Require Import LatticeSignatures.
Require Import Cminor.
Require Import DLib.
Require Import Cells.

Module IOP.

Inductive t := VI | VP | Top.


Definition leb (x y:t) : bool :=
    match x,y with
      | VI, VI
      | VP, VP
      | _, Top => true
      | _,_ => false
    end.

Definition gamma (ab:t) (v:val) : Prop :=
  match ab, v with
    | VI, Vint i => True
    | VP, Vptr _ _ => True
    | Top, _ => True
    | _, Vundef => True
    | _, _ => False
  end.

Definition join (i1 i2: t) : t :=
  match i1, i2 with
    | VI, VI => VI
    | VP, VP => VP
    | _, _ => Top
  end.

Definition widen := join.

Definition top := Top.

  Lemma gamma_top : forall v,
    gamma top v.
Proof.
    destruct v; simpl; auto.
  Qed.

  Lemma gamma_monotone : forall ab1 ab2,
    leb ab1 ab2 = true -> forall v, gamma ab1 v -> gamma ab2 v.
Proof.
    destruct ab1; destruct ab2; simpl in *; try congruence;
    try destruct v; simpl in *; auto.
  Qed.

  Lemma join_sound' (x y: t) : gamma xgamma ygamma (join x y).
Proof.
    intros [| | |]; destruct x; destruct y; intuition.
  Qed.

  Instance wlat : adom t val :=
   { leb := leb;
     top := top;
     join := join;
     widen := widen;
     gamma := gamma;
     gamma_monotone := gamma_monotone;
     gamma_top := gamma_top
   ; join_sound := join_sound'
   }.

  Definition eval_constant (cst: constant) : t:=
    match cst with
      | Ointconst n => VI
      | Ofloatconst n => Top
      | Oaddrsymbol s ofs => VP
      | Oaddrstack ofs => VP
  end.

  Definition eval_unop (op: unary_operation) (arg: t) : t :=
    match op with
      | Ocast8unsigned
      | Ocast8signed
      | Ocast16unsigned
      | Ocast16signed
      | Oboolval
      | Onegint
      | Onotbool
      | Onotint
      | Ointoffloat
      | Ointuoffloat => VI
      | Onegf
      | Oabsf
      | Osingleoffloat
      | Ofloatofint
      | Ofloatofintu => Top
  end.

  Definition eval_binop (op: binary_operation) (arg1 arg2: t): t :=
    match op with
      | Oadd =>
        match arg1, arg2 with
          | VP, VI | VI, VP => VP
          | VI, VI => VI
          | _, _ => Top
        end
      | Osub =>
        match arg1, arg2 with
          | VP, VI => VP
          | VP, VP | VI, VI => VI
          | _, _ => Top
        end
      | Omul
      | Odiv
      | Odivu
      | Omod
      | Omodu
      | Oand
      | Oor
      | Oxor
      | Oshl
      | Oshr
      | Oshru
      | Ocmp _
      | Ocmpu _
      | Ocmpf _ => VI
      | Oaddf
      | Osubf
      | Omulf
      | Odivf => Top
    end.

  Lemma eval_constant_correct : forall (ge:CFG.genv) sp c v,
    Cminor.eval_constant ge (Vptr sp Int.zero) c = Some v ->
    γ (eval_constant c) v.
Proof.
    destruct c; simpl; intros v Hv; inv Hv; auto.
    destruct_option_in_goal; auto.
  Qed.

  Lemma eval_unop_correct : forall op arg x v,
    Cminor.eval_unop op arg = Some v ->
    γ x arg ->
    γ (eval_unop op x) v.
Proof.
    destruct op; destruct arg; simpl; intros x v Hv; inv Hv;
      simpl; auto.
    destruct Int.eq; simpl; auto.
    destruct Int.eq; simpl; auto.
    destruct Float.intoffloat; inv H0; simpl; auto.
    destruct Float.intuoffloat; inv H0; simpl; auto.
  Qed.

  Lemma gamma_Vundef: forall x, gamma x Vundef.
Proof.
    destruct x; simpl; auto.
  Qed.
  Hint Resolve gamma_Vundef.

  Lemma of_optbool_lemma: forall v,
   match Val.of_optbool v with
   | Vundef => True
   | Vint _ => True
   | Vfloat _ => False
   | Vptr _ _ => False
   end.
Proof.
    destruct v; simpl; auto.
    destruct b; simpl; auto.
  Qed.

  Lemma eval_binop_correct : forall op arg1 arg2 x1 x2 m v,
    Cminor.eval_binop op arg1 arg2 m = Some v ->
    γ x1 arg1 ->
    γ x2 arg2 ->
    γ (eval_binop op x1 x2) v.
Proof.
    intros op; set (op':=op).
    destruct op; destruct arg1; destruct arg2; simpl;
    intros x1 x2 m v Hv; inv Hv; simpl; auto;
    intros H1 H2; destruct x1; destruct x2; inv H1; inv H2; simpl; auto;
    try (destruct_bool; try simpl_option; auto);
    apply of_optbool_lemma.
  Qed.

  Definition eval_cond (b: t) (l r: t+⊥) : t+⊥ :=
    match b with
      | VI => lr
      | VP => l
      | Top => lr
    end.

  Definition adom : @Cell2Val.adom t.
    refine (
    Cell2Val.Build_adom
    wlat
    eval_constant
    eval_unop
    eval_binop
    eval_cond
    eval_constant_correct
    eval_unop_correct
    eval_binop_correct
    _) .
Proof.
    unfold eval_cond.
    intros [| |] l r B bv H H0 K H1.
    apply join_sound. destruct bv; auto.
    destruct B; inv H; inv H0. auto.
    apply join_sound. destruct bv; auto.
  Defined.

End IOP.