diff options
Diffstat (limited to 'abstract/intervals_domain.ml')
| -rw-r--r-- | abstract/intervals_domain.ml | 158 |
1 files changed, 158 insertions, 0 deletions
diff --git a/abstract/intervals_domain.ml b/abstract/intervals_domain.ml new file mode 100644 index 0000000..848f634 --- /dev/null +++ b/abstract/intervals_domain.ml @@ -0,0 +1,158 @@ +open Value_domain + +module VD : VALUE_DOMAIN = struct + type bound = Int of int | 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 -> 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 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 bound_str = function + | MInf -> "-oo" + | PInf -> "+oo" + | Int i -> string_of_int i + let to_string = function + | Bot -> "bot" + | Itv(a, b) -> "[" ^ (bound_str a) ^ ";" ^ (bound_str b) ^ "]" + +end |