Retab

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