diff options
Diffstat (limited to 'abstract')
| -rw-r--r-- | abstract/intervals_domain.ml | 87 | ||||
| -rw-r--r-- | abstract/value_domain.ml | 7 |
2 files changed, 50 insertions, 44 deletions
diff --git a/abstract/intervals_domain.ml b/abstract/intervals_domain.ml index 181266b..92d00a2 100644 --- a/abstract/intervals_domain.ml +++ b/abstract/intervals_domain.ml @@ -31,19 +31,18 @@ module VD : VALUE_DOMAIN = struct | 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_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 @@ -61,14 +60,14 @@ module VD : VALUE_DOMAIN = struct | 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 = + let itv i j = if i <= j then Itv(Int i, Int j) else Bot let to_itv x = x let as_const = function @@ -82,36 +81,43 @@ module VD : VALUE_DOMAIN = struct 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) + | 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 + 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 + let lb = + 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 + else a + in + let ub = + if not (bound_leq d b) then (if bound_leq d (Int 0) then Int 0 else PInf) - else b)) + 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) + | 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)) + | 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) -> @@ -123,29 +129,28 @@ module VD : VALUE_DOMAIN = struct 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 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) - ) + 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) + if not (bound_leq a d) then Bot, Bot else Itv(a, bound_min b d), Itv(bound_max a c, d) diff --git a/abstract/value_domain.ml b/abstract/value_domain.ml index bb27126..0a421f7 100644 --- a/abstract/value_domain.ml +++ b/abstract/value_domain.ml @@ -10,6 +10,7 @@ let string_of_itv = function | Bot -> "⊥" | Itv(a, b) -> "[" ^ (string_of_bound a) ^ "; " ^ (string_of_bound b) ^ "]" + module type VALUE_DOMAIN = sig type t @@ -17,7 +18,7 @@ module type VALUE_DOMAIN = sig val top : t val bottom : t val const : int -> t - val rand : int -> int -> t + val itv : int -> int -> t val to_itv : t -> itv val as_const : t -> int option @@ -37,8 +38,8 @@ module type VALUE_DOMAIN = sig val div : t -> t -> t val rem : t -> t -> t - (* boolean test *) - val leq : t -> t -> t * t (* For intervals : [a, b] -> [c, d] -> ([a, min b d], [max a c, d]) *) + (* restrict two values considering that the first is smaller than the second *) + val leq : t -> t -> t * t (* pretty-printing *) val to_string : t -> string |