Module ValueAnalysis

Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Globalenvs.
Require Import Op.
Require Import Registers.
Require Import RTL.
Require Import LatticeSignatures.
Require Import CfgIterator.
Require Export IntervalDomain.
Require Export VIntDomain.


Module Val.
  Definition t := (Interval.t * MustVInt.t)%type.
  Definition wlat : WLattice.t t val :=
    WProd.make Interval.wlat MustVInt.wlat.
  Definition bwlat : BWLattice.t (option t) val :=
    BWLattice.from_wlattice wlat.
End Val.


Definition t := option (PTree.t Val.t).

Definition bwlat : BWLattice.t t (PMap.t val) :=
  WPMap.make Val.wlat.

Definition swap {A} (xy:A*A) : A*A :=
  let (x,y) := xy in (y,x).

Definition backward_cmp (c:comparison) (i1 i2:Interval.t) :=
  match c with
    | Ceq => Interval.backward_eq i1 i2
    | Cne => Interval.backward_ne i1 i2
    | Clt => Interval.backward_lt i1 i2
    | Cle => Interval.backward_le i1 i2
    | Cgt => swap (Interval.backward_lt i2 i1)
    | Cge => swap (Interval.backward_le i2 i1)
  end.

Definition backward_cmpu (c:comparison) (i1 i2:Interval.t) :=
  match c with
    | Ceq => Interval.backward_eq i1 i2
    | Cne => Interval.backward_ne i1 i2
    | Clt => Interval.backward_ltu i1 i2
    | Cle => Interval.backward_leu i1 i2
    | Cgt => swap (Interval.backward_ltu i2 i1)
    | Cge => swap (Interval.backward_leu i2 i1)
  end.

Definition backward1 (x:reg) (f:Interval.t->(Interval.itvbot*Interval.itvbot)) (ab: t) : t :=
  match WPMap.get Val.wlat ab x with
    | None => None
    | Some (vx,MustVInt.VI) =>
      match f vx with
        | (None,_)
        | (_,None) => None
        | (Some vx', Some _) =>
          WPMap.set ab x (Some (vx',MustVInt.VI))
      end
    | _ => ab
  end.

Definition backward2 (x y:reg) (f:Interval.t->Interval.t->(Interval.itvbot*Interval.itvbot)) (ab: t) : t :=
  match WPMap.get Val.wlat ab x, WPMap.get Val.wlat ab y with
    | None, _
    | _, None => None
    | Some (vx,MustVInt.VI), Some (vy,MustVInt.VI) =>
      match f vx vy with
        | (None,_)
        | (_,None) => None
        | (Some vx', Some vy') =>
          WPMap.set
            (WPMap.set ab x (Some (vx',MustVInt.VI)))
            y (Some (vy',MustVInt.VI))
      end
    | _, _ => ab
  end.

Definition backward_cmp_var_var (c:comparison) (x y:reg) : t -> t :=
  backward2 x y (backward_cmp c).

Definition backward_cmp_var_cst (c:comparison) (x:reg) (n:int) : t -> t :=
  backward1 x (fun v_x => backward_cmp c v_x (Interval.signed n)).

Definition backward_cmpu_var_var (c:comparison) (x y:reg) : t -> t :=
  backward2 x y (backward_cmpu c).

Definition backward_cmpu_var_cst (c:comparison) (x:reg) (n:int) : t -> t :=
  backward1 x (fun v_x => backward_cmpu c v_x (Interval.signed n)).


Definition assume (c:condition) (args:list reg) (app:t) : t :=
  match c, args with
    | Ccomp c , x1 :: x2 :: nil => backward_cmp_var_var c x1 x2 app
    | Ccompimm c n, x :: nil => backward_cmp_var_cst c x n app
    | Ccompu c , x1 :: x2 :: nil => backward_cmpu_var_var c x1 x2 app
    | Ccompuimm c n, x :: nil => backward_cmpu_var_cst c x n app
    | _, _ => app
  end.

Definition neg_cmp (c:comparison) : comparison :=
  match c with
    | Ceq => Cne
    | Cne => Ceq
    | Clt => Cge
    | Cle => Cgt
    | Cgt => Cle
    | Cge => Clt
  end.

Definition neg_cond (c:condition) : condition :=
  match c with
    | Ccomp c => Ccomp (neg_cmp c)
    | Ccompimm c n => Ccompimm (neg_cmp c) n
    | Ccompu c => Ccompu (neg_cmp c)
    | Ccompuimm c n => Ccompuimm (neg_cmp c) n
    | _ => c
  end.

Definition cast_int7 : Interval.t-> bool := Interval.is_in_interval 0 127.
Definition cast_int8s : Interval.t-> bool := Interval.is_in_interval (-128) 127.
Definition cast_int8u : Interval.t-> bool := Interval.is_in_interval 0 255.
Definition cast_int15 : Interval.t-> bool := Interval.is_in_interval 0 32767.
Definition cast_int16s : Interval.t-> bool := Interval.is_in_interval (-32768) 32767.
Definition cast_int16u : Interval.t-> bool := Interval.is_in_interval 0 65535.

Inductive get_list_return_type := GL_Bot | GL_Top | GL_Some (l:list Interval.t).

Fixpoint get_list (ab: t) (rl: list reg) : get_list_return_type :=
  match rl with
    | nil => GL_Some nil
    | r::q =>
      match WPMap.get Val.wlat ab r with
        | None => GL_Bot
        | Some (i,MustVInt.Top) => GL_Top
        | Some (i,_) =>
          match get_list ab q with
            | GL_Top => GL_Top
            | GL_Bot => GL_Bot
            | GL_Some q' => GL_Some (i::q')
          end
      end
  end.

Definition ab_operation (op: operation) (vl: list Interval.t) : Interval.t :=
  match op, vl with
    | Omove, v :: nil => v
    | Ointconst n, _ => Interval.signed n
    | Oneg, v :: nil => Interval.neg v
    | Ocast8signed, v :: nil => if cast_int8s v then v else Interval.top
    | Ocast8unsigned, v :: nil => if cast_int8u v then v else Interval.top
    | Ocast16signed, v :: nil => if cast_int16s v then v else Interval.top
    | Ocast16unsigned, v :: nil => if cast_int16u v then v else Interval.top
    | Ocmp _, _ => Interval.booleans
    | Osub, v1 :: v2 :: nil => Interval.sub v1 v2
    | Omul, v1 :: v2 :: nil => Interval.mult v1 v2
    | Omulimm n, v :: nil => Interval.mult v (Interval.signed n)
    | Olea (Aindexed n), v :: nil => Interval.add v (Interval.signed n)
    | Olea (Aindexed2 n), v1 :: v2 :: nil =>
      Interval.add (Interval.add v1 v2) (Interval.signed n)
    | Olea (Ascaled sc n), v :: nil =>
      Interval.add (Interval.mult v (Interval.signed sc)) (Interval.signed n)
    | Olea (Aindexed2scaled sc n), v1 :: v2 :: nil =>
      Interval.add v1
      (Interval.add (Interval.mult v2 (Interval.signed sc)) (Interval.signed n))
    | _, _ => Interval.top
  end.

Definition eval_op_gives_VInt (op:operation) (nb_args:nat) : bool :=
  match op with
    | Ofloatconst _
    | Olea (Aglobal _ _)
    | Olea (Abased _ _)
    | Olea (Abasedscaled _ _ _)
    | Olea (Ainstack _)
    | Osingleoffloat
    | Ofloatofint
    | Onegf
    | Oabsf
    | Oaddf
    | Osubf
    | Omulf
    | Odivf => false
    | Oshl
    | Oshr
    | Oshru => false
    | Oshlimm n
    | Oshrimm n
    | Oshruimm n
    | Ororimm n => Int.ltu n Int.iwordsize
    | Ocmp c =>
      match c, nb_args with
        | Ccomp _, 2%nat
        | Ccompu _, 2%nat
        | Ccompimm _ _, 1%nat
        | Ccompuimm _ _, 1%nat
        | Cmaskzero _, 1%nat
        | Cmasknotzero _, 1%nat => true
        | _, _ => false
      end
    | _ => true
  end.

Definition ab_op (op:operation) (args:list reg) (dst:reg) (ab:t) : t :=
  match get_list ab args with
    | GL_Bot => BWLattice.bot bwlat
    | GL_Top => WPMap.set ab dst (BWLattice.top Val.bwlat)
    | GL_Some args =>
      match ab with
        | None => None
        | Some _ =>
          if eval_op_gives_VInt op (length args) then
            let i := ab_operation op args in
            WPMap.set ab dst (Some (i,MustVInt.VI))
          else WPMap.set ab dst (BWLattice.top Val.bwlat)
      end
  end.

Definition transfer (ins: instruction) : list (node*(t->t)) :=
  match ins with
    | Inop s
    | Istore _ _ _ _ s => (s,fun ab => ab) :: nil
    | Iop op args dst s => (s,ab_op op args dst) :: nil
    | Iload _ _ _ dst s
    | Icall _ _ _ dst s
    | Ibuiltin _ _ dst s => (s, fun ab =>
                                  match ab with
                                    | None => None
                                    | _ => WPMap.set ab dst (BWLattice.top Val.bwlat) end) :: nil
    | Icond c args s1 s2 =>
      (s1,assume c args) ::
      (s2,assume (neg_cond c) args) :: nil
    | Ijumptable _ tbl =>
      List.map (fun j => (j,fun ab => ab)) tbl
    | Itailcall _ _ _
    | Ireturn _ => nil
  end.

Definition analyze (f:function) : node -> t :=
  BourdoncleIterator.analyze bwlat f transfer (BWLattice.top bwlat).


Record interval := Make_interval {
  itv_min: Z;
  itv_max: Z;
  itv_wf: (itv_max >= itv_min)%Z
}.

Require Import Errors.
Require Import VarsUseDef.

Definition make_interval (itv:Interval.t) : res interval :=
  let min := Interval.min itv in
  let max := Interval.max itv in
  match Z_ge_dec max min with
    | left h => OK (Make_interval min max h)
    |_ => Error (MSG ("empty interval") :: nil)
  end.

Definition value (f:function) : node -> var -> res interval :=
  let dom_regs := analyze f in
  fun pc x =>
  match dom_regs pc with
    | None => Error (MSG "empty interval (None)" :: nil)
    | Some t =>
      match t ! x with
        | None => Error (MSG "dom x: got None" :: nil)
        | Some (itv, res) =>
          match res with
            | MustVInt.Top => Error (MSG ("dom: got Top") :: nil)
            | MustVInt.VI => make_interval itv
          end
      end
  end.