Refactor

Author: michael-schwarz

src/analyses/useAfterFree.ml

@@ -46,11 +46,7 @@ struct
           let not_started = MHP.definitely_not_started (current, created_threads) tid in
           let possibly_started = not not_started in
           (* If [current] is possibly running together with [tid], but is also joined before the free() in [tid], then no need to WARN *)
-          let current_joined_before_free = match current with
-            | ThreadIdDomain.Thread ft -> ConcDomain.FiniteMustThreadSet.mem ft joined_threads
-            | ThreadIdDomain.UnknownThread -> false
-          in
-          possibly_started && not current_joined_before_free
+          possibly_started && not (ConcDomain.FiniteMustThreadSet.mem_lifted current joined_threads)
         | `Top -> true
         | `Bot -> false
       in

src/cdomain/value/cdomains/concDomain.ml

@@ -1,6 +1,13 @@
 (** Domains for thread sets and their uniqueness. *)
 
-module FiniteMustThreadSet = SetDomain.Reverse (SetDomain.Make (ThreadIdDomain.FlagConfiguredTID))
+module FiniteMustThreadSet = struct
+  include SetDomain.Reverse (SetDomain.Make (ThreadIdDomain.FlagConfiguredTID))
+
+  let mem_lifted lifted_tid set =
+    match lifted_tid with
+    | ThreadIdDomain.Thread ft -> mem ft set
+    | ThreadIdDomain.UnknownThread -> false
+end
 
 module ThreadSet =
 struct
@@ -22,11 +29,7 @@ struct
   let narrow x y = merge (fun x y -> widen x (join x y)) narrow x y
 
   let diff_mustset x (y: FiniteMustThreadSet.t) =
-    filter (fun t ->
-        match t with
-        | ThreadIdDomain.Thread ft -> not (FiniteMustThreadSet.mem ft y)
-        | ThreadIdDomain.UnknownThread -> true
-      ) x
+    FiniteMustThreadSet.fold (fun t -> remove (ThreadIdDomain.Thread t)) y x
 end
 
 module CreatedThreadSet = ThreadSet

src/cdomains/mHP.ml

@@ -65,11 +65,8 @@ let definitely_not_started (current, created) other =
 let exists_definitely_not_started_in_joined (current,created) other_joined =
   ConcDomain.FiniteMustThreadSet.exists (fun ft -> definitely_not_started (current, created) (ThreadIdDomain.Thread ft)) other_joined
 
-(** Must the thread with thread id other be already joined  *)
-let must_be_joined other joined =
-  match other with
-  | ThreadIdDomain.Thread ft -> ConcDomain.FiniteMustThreadSet.mem ft joined
-  | ThreadIdDomain.UnknownThread -> false
+(** Must the thread be already joined  *)
+let must_be_joined = ConcDomain.FiniteMustThreadSet.mem_lifted
 
 (** May two program points with respective MHP information happen in parallel *)
 let may_happen_in_parallel one two =