open Value_domain
module Intervals : VALUE_DOMAIN = struct
type bound = Int of Z.t | PInf | MInf
type t = Itv of bound * bound | Bot
(* utilities *)
let bound_leq a b = (* a <= b ? *)
match a, b with
| MInf, _ | _, PInf -> true
| Int a, Int b -> Z.leq 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 (Z.add a b)
| _ -> assert false
let bound_mul a b =
match a, b with
| PInf, Int(x) | Int(x), PInf ->
if x > Z.zero then PInf
else if x < Z.zero then MInf
else Int Z.zero
| MInf, Int(x) | Int(x), MInf ->
if x < Z.zero then PInf
else if x > Z.zero then MInf
else Int Z.zero
| Int(x), Int(y) -> Int(Z.mul x y)
| MInf, PInf | PInf, MInf -> MInf
| MInf, MInf | PInf, PInf -> PInf
let bound_div a b =
match a, b with
| _, PInf | _, MInf -> Int Z.zero
| PInf, Int i ->
if i < Z.zero then MInf
else PInf
| MInf, Int i ->
if i < Z.zero then PInf
else MInf
| Int i, Int j ->
if j = Z.zero then
if i < Z.zero then MInf
else PInf
else Int (Z.div 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 (Z.neg 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 Z.leq i j then Itv(Int i, Int j) else Bot
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 MInf else a),
(if not (bound_leq d b) then 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 (Z.of_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 (Z.of_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 Z.zero,
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 bound_str = function
| MInf -> "-oo"
| PInf -> "+oo"
| Int i -> Z.to_string i
let to_string = function
| Bot -> "bot"
| Itv(a, b) -> "[" ^ (bound_str a) ^ ";" ^ (bound_str b) ^ "]"
end
