Module IntOrPtrDomain

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.

  Lemma gamma_monotone : forall ab1 ab2,
    leb ab1 ab2 = true -> forall v, gamma ab1 v -> gamma ab2 v.

  Lemma join_sound' (x y: t) : gamma x ∪ gamma y ⊆ gamma (join x y).

  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.

  Lemma eval_unop_correct : forall op arg x v,
    Cminor.eval_unop op arg = Some v ->
    γ x arg ->
    γ (eval_unop op x) v.

  Lemma gamma_Vundef: forall x, gamma x Vundef.
  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.

  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.

  Definition eval_cond (b: t) (l r: t+⊥) : t+⊥ :=
    match b with
      | VI => l ⊔ r
      | VP => l
      | Top => l ⊔ r
    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
    _) .

End IOP.