Skip to content

Commit

Permalink
Remove Lattice.Unsupported
Browse files Browse the repository at this point in the history
All cases can be replaced with BotValue or TopValue.
  • Loading branch information
sim642 committed Sep 23, 2024
1 parent 39686d5 commit 372a838
Show file tree
Hide file tree
Showing 6 changed files with 15 additions and 21 deletions.
2 changes: 1 addition & 1 deletion src/cdomain/value/cdomains/stringDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,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
Expand Down
4 changes: 2 additions & 2 deletions src/cdomains/stackDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
20 changes: 7 additions & 13 deletions src/domain/lattice.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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") (* TODO: TopValue? *)
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") (* TODO: BotValue? *)
if equal x y then x else raise BotValue
let narrow = meet
include NoBotTop

Expand Down Expand Up @@ -394,11 +391,11 @@ struct
| (x, `Bot) -> x
| (`Lifted1 x, `Lifted1 y) -> begin
try `Lifted1 (Base1.join x y)
with Unsupported _ | TopValue -> `Top
with TopValue -> `Top
end
| (`Lifted2 x, `Lifted2 y) -> begin
try `Lifted2 (Base2.join x y)
with Unsupported _ | TopValue -> `Top
with TopValue -> `Top
end
| _ -> `Top

Expand All @@ -410,11 +407,11 @@ struct
| (x, `Top) -> x
| (`Lifted1 x, `Lifted1 y) -> begin
try `Lifted1 (Base1.meet x y)
with Unsupported _ | BotValue -> `Bot
with BotValue -> `Bot
end
| (`Lifted2 x, `Lifted2 y) -> begin
try `Lifted2 (Base2.meet x y)
with Unsupported _ | BotValue -> `Bot
with BotValue -> `Bot
end
| _ -> `Bot

Expand Down Expand Up @@ -581,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
Expand Down
4 changes: 2 additions & 2 deletions src/domain/mapDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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

Expand Down
2 changes: 1 addition & 1 deletion src/domains/domainProperties.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 ->
Expand Down
4 changes: 2 additions & 2 deletions tests/unit/domains/mapDomainTest.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand All @@ -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
Expand Down

0 comments on commit 372a838

Please sign in to comment.