open Value_domain
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_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 rand 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 a c && bound_leq d b
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) ->
Itv(
(if not (bound_leq a c) then
(if bound_leq (Int 0) c then Int 0 else MInf)
else a),
(if not (bound_leq d b) then
(if bound_leq d (Int 0) then Int 0 else PInf)
else b))
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
