Add unknown thread ID

src/analyses/useAfterFree.ml

@@ -76,7 +76,7 @@ struct
           end
           else if HeapVars.mem heap_var (snd ctx.local) then begin
             if is_double_free then set_mem_safety_flag InvalidFree else set_mem_safety_flag InvalidDeref;
-            M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "%s might occur in current unique thread %a for heap variable %a" bug_name ThreadIdDomain.FlagConfiguredTID.pretty current CilType.Varinfo.pretty heap_var
+            M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "%s might occur in current unique thread %a for heap variable %a" bug_name ThreadIdDomain.Thread.pretty current CilType.Varinfo.pretty heap_var
           end
         end
       | `Top ->

src/cdomains/mHP.ml

@@ -4,7 +4,7 @@ include Printable.Std
 
 let name () = "mhp"
 
-module TID = ThreadIdDomain.FlagConfiguredTID
+module TID = ThreadIdDomain.Thread
 module Pretty = GoblintCil.Pretty
 
 type t = {

src/cdomains/threadIdDomain.ml

@@ -279,6 +279,77 @@ struct
   let name () = "FlagConfiguredTID: " ^ if history_enabled () then H.name () else P.name ()
 end
 
-module Thread = FlagConfiguredTID
+module Thread : Stateful =
+struct
+  include Printable.Std
+  type t =
+    | Thread of FlagConfiguredTID.t
+    | UnknownThread
+  [@@deriving eq, ord, hash]
+
+  let name () = "Thread id"
+  let pretty () t =
+    match t with
+    | Thread tid -> FlagConfiguredTID.pretty () tid
+    | UnknownThread -> Pretty.text "Unknown thread id"
+
+  let show t =
+    match t with
+    | Thread tid -> FlagConfiguredTID.show tid
+    | UnknownThread -> "Unknown thread id"
+
+  let printXml f t =
+    match t with
+    | Thread tid -> FlagConfiguredTID.printXml f tid
+    | UnknownThread -> BatPrintf.fprintf f "<value>\n<data>\nUnknown thread id\n</data>\n</value>\n"
+
+  let to_yojson t =
+    match t with
+    | Thread tid -> FlagConfiguredTID.to_yojson tid
+    | UnknownThread -> `String "Unknown thread id"
+
+  let relift t =
+    match t with
+    | Thread tid -> Thread (FlagConfiguredTID.relift tid)
+    | UnknownThread -> UnknownThread
+
+  let lift t = Thread t
+
+  let threadinit v ~multiple = Thread (FlagConfiguredTID.threadinit v ~multiple)
+
+  let is_main t =
+    match t with
+    | Thread tid -> FlagConfiguredTID.is_main tid
+    | UnknownThread -> false
+
+  let is_unique t =
+    match t with
+    | Thread tid -> FlagConfiguredTID.is_unique tid
+    | UnknownThread -> false
+
+  let may_create t1 t2 =
+    match t1, t2 with
+    | Thread tid1, Thread tid2 -> FlagConfiguredTID.may_create tid1 tid2
+    | _, _ -> true
+
+  let is_must_parent t1 t2 =
+    match t1, t2 with
+    | Thread tid1, Thread tid2 -> FlagConfiguredTID.is_must_parent tid1 tid2
+    | _, _ -> false
+
+  module D = FlagConfiguredTID.D
+
+  let threadenter (t, d) node i v =
+    match t with
+    | Thread tid -> List.map lift (FlagConfiguredTID.threadenter (tid, d) node i v)
+    | UnknownThread -> assert false
+
+  let threadspawn = FlagConfiguredTID.threadspawn
+
+  let created t d =
+    match t with
+    | Thread tid -> Option.map (List.map lift) (FlagConfiguredTID.created tid d)
+    | UnknownThread -> None
+end
 
 module ThreadLifted = Lift (Thread)