Skip to content

Commit

Permalink
Use set instead of toppedSet for ThreadSet
Browse files Browse the repository at this point in the history
  • Loading branch information
karoliineh committed Oct 26, 2023
1 parent 0e31b8d commit 192108b
Show file tree
Hide file tree
Showing 2 changed files with 27 additions and 6 deletions.
21 changes: 20 additions & 1 deletion src/cdomains/concDomain.ml
Original file line number Diff line number Diff line change
@@ -1,6 +1,25 @@
(** Domains for thread sets and their uniqueness. *)

module ThreadSet = SetDomain.ToppedSet (ThreadIdDomain.Thread) (struct let topname = "All Threads" end)
module ThreadSet =
struct
include SetDomain.Make (ThreadIdDomain.Thread)

let is_top = mem UnknownThread

let top () = singleton UnknownThread

let merge uop cop x y =
match is_top x, is_top y with
| true, true -> uop x y
| false, true -> x
| true, false -> y
| false, false -> cop x y

let meet x y = merge join meet x y

let narrow x y = merge (fun x y -> widen x (join x y)) narrow x y

end
module MustThreadSet = SetDomain.Reverse(ThreadSet)

module CreatedThreadSet = ThreadSet
Expand Down
12 changes: 7 additions & 5 deletions src/cdomains/threadIdDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -279,13 +279,15 @@ struct
let name () = "FlagConfiguredTID: " ^ if history_enabled () then H.name () else P.name ()
end

module Thread : Stateful =
type thread =
| Thread of FlagConfiguredTID.t
| UnknownThread
[@@deriving eq, ord, hash]

module Thread : Stateful with type t = thread =
struct
include Printable.Std
type t =
| Thread of FlagConfiguredTID.t
| UnknownThread
[@@deriving eq, ord, hash]
type t = thread [@@deriving eq, ord, hash]

let name () = "Thread id"
let pretty () t =
Expand Down

0 comments on commit 192108b

Please sign in to comment.