Merge pull request #1573 from goblint/issue-1572

Improve use of `Lattice.BotValue` and `Lattice.TopValue`

src/cdomain/value/cdomains/stringDomain.ml

@@ -71,7 +71,7 @@ let to_string_length x =
 
 let to_exp = function
   | Some x -> GoblintCil.mkString x
-  | None -> raise (Lattice.Unsupported "Cannot express unknown string pointer as expression.")
+  | None -> failwith "Cannot express unknown string pointer as expression."
 
 let semantic_equal x y =
   match x, y with

src/cdomains/stackDomain.ml

@@ -13,14 +13,14 @@ struct
   let n = 3
   let rec times x = function 0 -> [] | n -> x::times x (n-1)
   let rec map2 f xs ys =
-    match xs, ys with x::xs, y::ys -> (try f x y :: map2 f xs ys with Lattice.Unsupported _ -> []) | _ -> []
+    match xs, ys with x::xs, y::ys -> (try f x y :: map2 f xs ys with Lattice.BotValue | Lattice.TopValue -> []) | _ -> []
 
   let rec fold_left2 f a b xs ys =
     match xs, ys with
     | [], _ | _, [] -> a
     | x::xs, y::ys ->
       try fold_left2 f (f a x y) b xs ys with
-      | Lattice.Unsupported _ -> b
+      | Lattice.BotValue | Lattice.TopValue -> b
 
   let rec take n xs =
     match n, xs with

src/domain/lattice.ml

@@ -45,9 +45,6 @@ exception BotValue
 (** Exception raised by a bottomless lattice in place of a bottom value.
     Surrounding lattice functors may handle this on their own. *)
 
-exception Unsupported of string
-let unsupported x = raise (Unsupported x)
-
 exception Invalid_widen of Pretty.doc
 
 let () = Printexc.register_printer (function
@@ -93,10 +90,10 @@ struct
   include Base
   let leq = equal
   let join x y =
-    if equal x y then x else raise (Unsupported "fake join")
+    if equal x y then x else raise TopValue
   let widen = join
   let meet x y =
-    if equal x y then x else raise (Unsupported "fake meet")
+    if equal x y then x else raise BotValue
   let narrow = meet
   include NoBotTop
 
@@ -259,24 +256,36 @@ struct
     | (_, `Top) -> `Top
     | (`Bot, x) -> x
     | (x, `Bot) -> x
-    | (`Lifted x, `Lifted y) -> `Lifted (Base.join x y)
+    | (`Lifted x, `Lifted y) ->
+      try `Lifted (Base.join x y)
+      with TopValue -> `Top
 
   let meet x y =
     match (x,y) with
     | (`Bot, _) -> `Bot
     | (_, `Bot) -> `Bot
     | (`Top, x) -> x
     | (x, `Top) -> x
-    | (`Lifted x, `Lifted y) -> `Lifted (Base.meet x y)
+    | (`Lifted x, `Lifted y) ->
+      try `Lifted (Base.meet x y)
+      with BotValue -> `Bot
 
   let widen x y =
     match (x,y) with
-    | (`Lifted x, `Lifted y) -> `Lifted (Base.widen x y)
+    | (`Lifted x, `Lifted y) ->
+      begin
+        try `Lifted (Base.widen x y)
+        with TopValue -> `Top
+      end
     | _ -> y
 
   let narrow x y =
     match (x,y) with
-    | (`Lifted x, `Lifted y) -> `Lifted (Base.narrow x y)
+    | (`Lifted x, `Lifted y) ->
+      begin
+        try `Lifted (Base.narrow x y)
+        with BotValue -> `Bot
+      end
     | (_, `Bot) -> `Bot
     | (`Top, y) -> y
     | _ -> x
@@ -315,7 +324,7 @@ struct
     | (x, `Bot) -> x
     | (`Lifted x, `Lifted y) ->
       try `Lifted (Base.join x y)
-      with Uncomparable -> `Top
+      with Uncomparable | TopValue -> `Top
 
   let meet x y =
     match (x,y) with
@@ -325,20 +334,24 @@ struct
     | (x, `Top) -> x
     | (`Lifted x, `Lifted y) ->
       try `Lifted (Base.meet x y)
-      with Uncomparable -> `Bot
+      with Uncomparable | BotValue -> `Bot
 
   let widen x y =
     match (x,y) with
     | (`Lifted x, `Lifted y) ->
-      (try `Lifted (Base.widen x y)
-       with Uncomparable -> `Top)
+      begin
+        try `Lifted (Base.widen x y)
+        with Uncomparable | TopValue -> `Top
+      end
     | _ -> y
 
   let narrow x y =
     match (x,y) with
     | (`Lifted x, `Lifted y) ->
-      (try `Lifted (Base.narrow x y)
-       with Uncomparable -> `Bot)
+      begin
+        try `Lifted (Base.narrow x y)
+        with Uncomparable | BotValue -> `Bot
+      end
     | (_, `Bot) -> `Bot
     | (`Top, y) -> y
     | _ -> x
@@ -378,11 +391,11 @@ struct
     | (x, `Bot) -> x
     | (`Lifted1 x, `Lifted1 y) -> begin
         try `Lifted1 (Base1.join x y)
-        with Unsupported _ -> `Top
+        with TopValue -> `Top
       end
     | (`Lifted2 x, `Lifted2 y) -> begin
         try `Lifted2 (Base2.join x y)
-        with Unsupported _ -> `Top
+        with TopValue -> `Top
       end
     | _ -> `Top
 
@@ -394,11 +407,11 @@ struct
     | (x, `Top) -> x
     | (`Lifted1 x, `Lifted1 y) -> begin
         try `Lifted1 (Base1.meet x y)
-        with Unsupported _ -> `Bot
+        with BotValue -> `Bot
       end
     | (`Lifted2 x, `Lifted2 y) -> begin
         try `Lifted2 (Base2.meet x y)
-        with Unsupported _ -> `Bot
+        with BotValue -> `Bot
       end
     | _ -> `Bot
 
@@ -489,7 +502,9 @@ struct
     match (x,y) with
     | (`Bot, _) -> `Bot
     | (_, `Bot) -> `Bot
-    | (`Lifted x, `Lifted y) -> `Lifted (Base.meet x y)
+    | (`Lifted x, `Lifted y) ->
+      try `Lifted (Base.meet x y)
+      with BotValue -> `Bot
 
   let widen x y =
     match (x,y) with
@@ -498,7 +513,11 @@ struct
 
   let narrow x y =
     match (x,y) with
-    | (`Lifted x, `Lifted y) -> `Lifted (Base.narrow x y)
+    | (`Lifted x, `Lifted y) ->
+      begin
+        try `Lifted (Base.narrow x y)
+        with BotValue -> `Bot
+      end
     | (_, `Bot) -> `Bot
     | _ -> x
 end
@@ -525,7 +544,9 @@ struct
     match (x,y) with
     | (`Top, x) -> `Top
     | (x, `Top) -> `Top
-    | (`Lifted x, `Lifted y) -> `Lifted (Base.join x y)
+    | (`Lifted x, `Lifted y) ->
+      try `Lifted (Base.join x y)
+      with TopValue -> `Top
 
   let meet x y =
     match (x,y) with
@@ -535,7 +556,11 @@ struct
 
   let widen x y =
     match (x,y) with
-    | (`Lifted x, `Lifted y) -> `Lifted (Base.widen x y)
+    | (`Lifted x, `Lifted y) ->
+      begin
+        try `Lifted (Base.widen x y)
+        with TopValue -> `Top
+      end
     | _ -> y
 
   let narrow x y =
@@ -553,10 +578,7 @@ end
 module Liszt (Base: S) =
 struct
   include Printable.Liszt (Base)
-  let bot () = raise (Unsupported "bot?")
-  let is_top _ = false
-  let top () = raise (Unsupported "top?")
-  let is_bot _ = false
+  include NoBotTop
 
   let leq =
     let f acc x y = Base.leq x y && acc in

src/domain/mapDomain.ml

@@ -398,7 +398,7 @@ struct
   let leq = leq_with_fct Range.leq
 
   let find x m = try find x m with | Not_found -> Range.bot ()
-  let top () = Lattice.unsupported "partial map top"
+  let top () = raise Lattice.TopValue
   let bot () = empty ()
   let is_top _ = false
   let is_bot = is_empty
@@ -448,7 +448,7 @@ struct
 
   let find x m = try find x m with | Not_found -> Range.top ()
   let top () = empty ()
-  let bot () = Lattice.unsupported "partial map bot"
+  let bot () = raise Lattice.BotValue
   let is_top = is_empty
   let is_bot _ = false
 

src/domains/domainProperties.ml

@@ -126,7 +126,7 @@ struct
     with
       | Failure _ (* raised by IntDomain *)
       | SetDomain.Unsupported _ (* raised by SetDomain *)
-      | Lattice.Unsupported _ (* raised by MapDomain *) ->
+      | Lattice.TopValue (* raised by MapDomain *) ->
         false
 
   let top_leq = make ~name:"top leq" (arb) (fun a ->

tests/unit/domains/mapDomainTest.ml

@@ -18,7 +18,7 @@ struct
   let get_empty () =
     try
       (is_empty_top := true;  M.top ())
-    with Lattice.Unsupported _ | Lattice.BotValue | Lattice.TopValue ->
+    with Lattice.TopValue ->
       (is_empty_top := false; M.bot ())
 
   let is_empty x =
@@ -44,7 +44,7 @@ struct
       map := M.remove "key1" !map;
       begin
         try ignore (M.find "key1" !map); assert_failure "problem removeing key1"
-        with Lattice.Unsupported _ | Lattice.BotValue | Lattice.TopValue -> ()
+        with Lattice.BotValue | Lattice.TopValue -> ()
       end ;
 
     end