Many things work!

1 files changed, 122 insertions, 0 deletions

diff --git a/abstract/intervals_domain.ml b/abstract/intervals_domain.ml
new file mode 100644
index 0000000..98f4daf
--- /dev/null
+++ b/abstract/intervals_domain.ml
@@ -0,0 +1,122 @@
+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_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)
+
+  (* 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 = top (* TODO *)
+  let rem a b = top (* TODO *)
+
+  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