diff options
Diffstat (limited to 'abstract')
| -rw-r--r-- | abstract/interpret.ml | 1 | ||||
| -rw-r--r-- | abstract/intervals_domain.ml | 41 | ||||
| -rw-r--r-- | abstract/nonrelational.ml | 2 |
3 files changed, 40 insertions, 4 deletions
diff --git a/abstract/interpret.ml b/abstract/interpret.ml index cb32e22..f6a6cb4 100644 --- a/abstract/interpret.ml +++ b/abstract/interpret.ml @@ -73,7 +73,6 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct (binop AST_OR (binop AST_LESS e1 e2) (binop AST_LESS e2 e1)) env - | _ -> env end diff --git a/abstract/intervals_domain.ml b/abstract/intervals_domain.ml index b63f8a9..d95a938 100644 --- a/abstract/intervals_domain.ml +++ b/abstract/intervals_domain.ml @@ -33,6 +33,21 @@ module Intervals : VALUE_DOMAIN = struct | 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 @@ -50,6 +65,8 @@ module Intervals : VALUE_DOMAIN = struct | 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) @@ -101,8 +118,28 @@ module Intervals : VALUE_DOMAIN = struct (bound_max (bound_mul b c) (bound_mul b d)))) - let div a b = top (* TODO *) - let rem a b = top (* TODO *) + 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 diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml index aa34d14..188c8bc 100644 --- a/abstract/nonrelational.ml +++ b/abstract/nonrelational.ml @@ -110,7 +110,7 @@ module NonRelational (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct | Env m, Env n -> VarMap.for_all2o (fun _ _ -> true) - (fun _ _ -> true) + (fun _ v -> v = V.top) (fun _ a b -> V.subset a b) m n |