path: root/abstract/intervals_domain.ml

open Value_domain

(*
  Value domain for representing one interval, doing operations on
  such representations, etc.

  Restricted implementation, only support integers.
*)

module VD : VALUE_DOMAIN = struct
    type t = itv

    (* utilities *)
    let bound_leq a b =   (* a <= b ? *)
        match a, b with
        | MInf, _ | _, PInf -> true
        | Int a, Int b -> a <= b
        | x, y -> x = y

    let bound_lt a b = not (bound_leq b a)    (* a < b *)

    let bound_add a b =
        match a, b with
        | MInf, Int a | Int a, MInf -> MInf
        | PInf, Int a | Int a, PInf -> PInf
        | MInf, MInf -> MInf
        | PInf, PInf -> PInf
        | Int a, Int b -> Int (a + b)
        | _ -> assert false
    let bound_mul a b =
        match a, b with
        | PInf, Int(x) | Int(x), PInf ->
            if x > 0 then PInf
            else if x < 0 then MInf
            else Int 0
        | MInf, Int(x) | Int(x), MInf ->
            if x < 0 then PInf
            else if x > 0 then MInf
            else Int 0
        | Int(x), Int(y) -> Int(x * y)
        | MInf, PInf | PInf, MInf -> MInf
        | MInf, MInf | PInf, PInf -> PInf
    let bound_div a b =
        match a, b with
        | _, PInf | _, MInf -> Int 0
        | PInf, Int i ->
          if i < 0 then MInf
          else PInf
        | MInf, Int i ->
          if i < 0 then PInf
          else MInf
        | Int i, Int j ->
          assert (j != 0);
          Int (i / j)

    let bound_min a b = match a, b with
        | MInf, _ | _, MInf -> MInf
        | Int a, Int b -> Int (min a b)
        | Int a, PInf -> Int a
        | PInf, Int a -> Int a
        | PInf, PInf -> PInf
    let bound_max a b = match a, b with
        | PInf, _ | _, PInf -> PInf
        | Int a, Int b -> Int (max a b)
        | Int a, MInf | MInf, Int a -> Int a
        | MInf, MInf -> MInf

    let bound_neg = function
        | PInf -> MInf
        | MInf -> PInf
        | Int i -> Int (- i)
  
    let bound_abs a = bound_max a (bound_neg a)

    (* implementation *)
    let top = Itv(MInf, PInf)
    let bottom = Bot
    let const i = Itv(Int i, Int i)
    let itv i j =
        if i <= j then Itv(Int i, Int j) else Bot
    let to_itv x = x
    let as_const = function
      | Itv(Int i, Int j) when i = j -> Some i
      | _ -> None

    let subset a b = match a, b with
        | Bot, _ -> true
        | _, Bot -> false
        | Itv(a, b), Itv(c, d) -> bound_leq c a && bound_leq b d

    let join a b = match a, b with
        | Bot, x | x, Bot -> x
        | Itv(a, b), Itv(c, d) ->
            Itv(bound_min a c, bound_max b d)

    let meet a b = match a, b with
        | Bot, x | x, Bot -> Bot
        | Itv(a, b), Itv(c, d) ->
          let u, v = bound_max a c, bound_min b d in
          if bound_leq u v
            then Itv(u, v)
            else Bot

    let widen a b = match a, b with
        | x, Bot | Bot, x -> x
        | Itv(a, b), Itv(c, d) ->
          let lb =
            if bound_lt c a then
                (if bound_leq (Int 0) c then Int 0 else MInf)
              else a
          in
          let ub = 
            if bound_lt b d then
                (if bound_leq d (Int 0) then Int 0 else PInf)
              else b
          in
          Itv(lb, ub)

    let neg = function
        | Bot -> Bot
        | Itv(a, b) -> Itv(bound_neg b, bound_neg a)
    let add a b = match a, b with
        | Bot, _ | _, Bot -> Bot
        | Itv(a, b), Itv(c, d) ->
            Itv(bound_add a c, bound_add b d)
    let sub a b = match a, b with
        | Bot, _ | _, Bot -> Bot
        | Itv(a, b), Itv(c, d) ->
            Itv(bound_add a (bound_neg d), bound_add b (bound_neg c))
    let mul a b = match a, b with
        | Bot, _ | _, Bot -> Bot
        | Itv(a, b), Itv(c, d) ->
            Itv(
                (bound_min (bound_min (bound_mul a c) (bound_mul a d))
                            (bound_min (bound_mul b c) (bound_mul b d))),
                (bound_max (bound_max (bound_mul a c) (bound_mul a d))
                            (bound_max (bound_mul b c) (bound_mul b d))))
    let div a b = match a, b with
        | Bot, _ -> Bot
        | Itv(a, b), q ->
          let p1 = match meet q (Itv(Int 1, PInf)) with
            | Bot -> Bot
            | Itv(c, d) ->
              Itv(min (bound_div a c) (bound_div a d),
                  max (bound_div b c) (bound_div b d))
          in
          let p2 = match meet q (Itv(MInf, Int (-1))) with
            | Bot -> Bot
            | Itv(c, d) ->
              Itv(min (bound_div b c) (bound_div b d),
                  max (bound_div a c) (bound_div a d))
          in
          join p1 p2
    let rem a b = match a, b with
        | Bot, _ | _, Bot -> Bot
        | Itv(a, b), Itv(c, d) ->
          Itv(Int 0, bound_max (bound_abs c) (bound_abs d))

    let leq a b = match a, b with
        | Bot, _ | _, Bot -> Bot, Bot
        | Itv(a, b), Itv(c, d) ->
          if not (bound_leq a d)
            then Bot, Bot
            else Itv(a, bound_min b d), Itv(bound_max a c, d)

    let to_string = string_of_itv

end