Merge pull request #1977 from goblint/copilot/fix-invalid-widen-issue

Refactor `bot` of threadJoins analysis to mean uncomputed

Author: sim642

src/analyses/apron/relationPriv.apron.ml

@@ -1242,7 +1242,7 @@ struct
       )
       else (
         (* fold throws if the thread set is top *)
-        let tids' = ConcDomain.ThreadSet.diff tids (ask.f Q.MustJoinedThreads) in (* avoid unnecessary imprecision by force joining already must-joined threads, e.g. 46-apron2/04-other-assume-inprec *)
+        let tids' = ConcDomain.ThreadSet.diff_mustset tids (ask.f Q.MustJoinedThreads) in (* avoid unnecessary imprecision by force joining already must-joined threads, e.g. 46-apron2/04-other-assume-inprec *)
         let (lmust', l') = ConcDomain.ThreadSet.fold (fun tid (lmust, l) ->
             let lmust',l' = G.thread (getg (V.thread tid)) in
             (LMust.union lmust' lmust, L.join l l')

src/analyses/basePriv.ml

@@ -636,7 +636,7 @@ struct
       )
       else (
         (* fold throws if the thread set is top *)
-        let tids' = ConcDomain.ThreadSet.diff tids (ask.f Q.MustJoinedThreads) in (* avoid unnecessary imprecision by force joining already must-joined threads, e.g. 46-apron2/04-other-assume-inprec *)
+        let tids' = ConcDomain.ThreadSet.diff_mustset tids (ask.f Q.MustJoinedThreads) in (* avoid unnecessary imprecision by force joining already must-joined threads, e.g. 46-apron2/04-other-assume-inprec *)
         let (lmust', l') = ConcDomain.ThreadSet.fold (fun tid (lmust, l) ->
             let lmust',l' = G.thread (getg (V.thread tid)) in
             (LMust.union lmust' lmust, L.join l l')

src/analyses/creationLockset.ml

@@ -71,7 +71,7 @@ module Spec = struct
         (TIDs.empty ())
     in
     let must_joined_tids = man.ask Queries.MustJoinedThreads in
-    TIDs.diff may_transitively_created_tids must_joined_tids
+    TIDs.diff_mustset may_transitively_created_tids must_joined_tids
 
   (** handle unlock of mutex [lock] *)
   let unlock man tid possibly_running_tids lock =

src/analyses/mHPAnalysis.ml

@@ -15,7 +15,7 @@ struct
     let should_print {tid; created; must_joined} =
       GobConfig.get_bool "dbg.full-output" ||
       (not (ConcDomain.ThreadSet.is_empty created) ||
-       not (ConcDomain.ThreadSet.is_empty must_joined))
+       not (ConcDomain.FiniteMustThreadSet.is_empty must_joined))
   end
 
   let access man _: MHP.t = MHP.current (Analyses.ask_of_man man)

src/analyses/threadId.ml

@@ -121,7 +121,7 @@ struct
             ConcDomain.ThreadSet.is_empty created
           else if man.ask Queries.ThreadsJoinedCleanly then
             let joined = man.ask Queries.MustJoinedThreads in
-            ConcDomain.ThreadSet.is_empty (ConcDomain.ThreadSet.diff created joined)
+            ConcDomain.ThreadSet.is_empty (ConcDomain.ThreadSet.diff_mustset created joined)
           else
             false
         | _ -> false

src/analyses/threadJoins.ml

@@ -7,7 +7,6 @@ open Analyses
 
 module TID  = ThreadIdDomain.Thread
 module TIDs = ConcDomain.ThreadSet
-module MustTIDs = ConcDomain.MustThreadSet
 module CleanExit = Queries.MustBool
 
 module Spec =
@@ -16,9 +15,13 @@ struct
 
   let name () = "threadJoins"
 
+
+  (* Must thread set, join is intersection, meet is union. Bottom denotes unreachability. Put here to not expose weirdness to the outsside *)
+  module MustTIDsWithBot = SetDomain.Reverse (SetDomain.ToppedSet (ThreadIdDomain.FlagConfiguredTID) (struct let topname = "All Threads" end))
+
   (* The first component is the set of must-joined TIDs, the second component tracks whether all TIDs recorded in MustTIDs have been exited cleanly, *)
   (* i.e., all created subthreads have also been joined. This is helpful as there is no set of all transitively created threads available. *)
-  module D = Lattice.Prod(MustTIDs)(CleanExit)
+  module D = Lattice.Prod(MustTIDsWithBot)(CleanExit)
   include Analyses.ValueContexts(D)
   module G = D
   module V =
@@ -34,7 +37,15 @@ struct
       let (j,joined_clean) = man.local in
       (* the current thread has been exited cleanly if all joined threads where exited cleanly, and all created threads are joined *)
       let created = man.ask Queries.CreatedThreads in
-      let clean = TIDs.subset created j in
+      let clean =
+        if MustTIDsWithBot.is_bot j then
+          raise Deadcode
+        else
+          TIDs.for_all (function
+              | ThreadIdDomain.Thread ft -> MustTIDsWithBot.mem ft j
+              | ThreadIdDomain.UnknownThread -> false
+            ) created
+      in
       man.sideg tid (j, joined_clean && clean)
     | _ -> () (* correct? *)
 
@@ -55,59 +66,63 @@ struct
         (* all elements are known *)
         let threads = TIDs.elements threads in
         match threads with
-        | [tid] when TID.is_unique tid->
+        | [(ThreadIdDomain.Thread tid_ft) as tid] when TID.is_unique tid->
           let (local_joined, local_clean) = man.local in
           let (other_joined, other_clean) = man.global tid in
-          (MustTIDs.union (MustTIDs.add tid local_joined) other_joined, local_clean && other_clean)
+          (MustTIDsWithBot.union (MustTIDsWithBot.add tid_ft local_joined) other_joined, local_clean && other_clean)
         | _ -> man.local (* if multiple possible thread ids are joined, none of them is must joined *)
         (* Possible improvement: Do the intersection first, things that are must joined in all possibly joined threads are must-joined *)
       )
     | Unknown, "__goblint_assume_join" ->
       let id = List.hd arglist in
       let threads = man.ask (Queries.EvalThread id) in
       if TIDs.is_top threads then (
-        M.info ~category:Unsound "Unknown thread ID assume-joined, assuming ALL threads must-joined.";
-        (MustTIDs.bot(), true) (* consider everything joined, MustTIDs is reversed so bot is All threads *)
-      )
-      else (
-        (* all elements are known *)
-        let threads = TIDs.elements threads in
-        if List.compare_length_with threads 1 > 0 then
-          M.info ~category:Unsound "Ambiguous thread ID assume-joined, assuming all of those threads must-joined.";
-        List.fold_left (fun (joined, clean) tid ->
+        M.info ~category:Unsound "Unknown thread ID assume-joined, continuing with known thread ids.";
+      );
+      let threads = TIDs.remove (ThreadIdDomain.UnknownThread) threads in
+      (* all elements are known *)
+      let threads = TIDs.elements threads in
+      if List.compare_length_with threads 1 > 0 then
+        M.info ~category:Unsound "Ambiguous thread ID assume-joined, assuming all of those threads must-joined.";
+      List.fold_left (fun (joined, clean) tid ->
+          match tid with
+          | ThreadIdDomain.Thread tid_ft ->
             let (other_joined, other_clean) = man.global tid in
-            (MustTIDs.union (MustTIDs.add tid joined) other_joined, clean && other_clean)
-          ) (man.local) threads
-      )
+            (MustTIDsWithBot.union (MustTIDsWithBot.add tid_ft joined) other_joined, clean && other_clean)
+          | ThreadIdDomain.UnknownThread -> assert false (* unreachable *)
+        ) (man.local) threads
     | _, _ -> man.local
 
   let threadspawn man ~multiple lval f args fman =
-    if D.is_bot man.local then ( (* bot is All threads *)
-      M.info ~category:Imprecise "Thread created while ALL threads must-joined, continuing with no threads joined.";
-      D.top () (* top is no threads *)
+    let (j, clean) = man.local in
+    if MustTIDsWithBot.is_bot j then ( (* bot is All threads *)
+      raise Deadcode
     )
     else
       match ThreadId.get_current (Analyses.ask_of_man fman) with
-      | `Lifted tid ->
-        let (j, clean) = man.local in
-        (MustTIDs.remove tid j, clean)
+      | `Lifted (ThreadIdDomain.Thread tid) ->
+        (MustTIDsWithBot.remove tid j, clean)
       | _ ->
         man.local
 
   let query man (type a) (q: a Queries.t): a Queries.result =
     match q with
-    | Queries.MustJoinedThreads -> (fst man.local:ConcDomain.MustThreadSet.t) (* type annotation needed to avoid "would escape the scope of its equation" *)
+    | Queries.MustJoinedThreads ->
+      (match ((fst man.local):MustTIDsWithBot.t) with
+       | `Lifted set -> set
+       | `Top -> Queries.Result.top q (* This is the lifted top of the reversed lattice, i.e., bottom, needed because of https://github.com/goblint/analyzer/issues/1978 *)
+      )
     | Queries.ThreadsJoinedCleanly -> (snd man.local:bool)
     | _ ->  Queries.Result.top q
 
   let combine_env man lval fexp f args fc au f_ask =
     let (caller_joined, local_clean) = man.local in
     let (callee_joined, callee_clean) = au in
-    (MustTIDs.union caller_joined callee_joined, local_clean && callee_clean)
-
+    if (MustTIDsWithBot.is_bot callee_joined) then raise Deadcode;
+    (MustTIDsWithBot.union caller_joined callee_joined, local_clean && callee_clean)
 
-  let startstate v = (MustTIDs.empty (), true)
-  let exitstate  v = (MustTIDs.empty (), true)
+  let startstate v = (MustTIDsWithBot.empty (), true)
+  let exitstate  v = (MustTIDsWithBot.empty (), true)
 end
 
 let _ = MCP.register_analysis ~dep:["threadid"] (module Spec : MCPSpec)

src/analyses/useAfterFree.ml

@@ -11,7 +11,7 @@ module HeapVars = SetDomain.ToppedSet(CilType.Varinfo)(struct let topname = "All
 (* Heap vars created by alloca() and deallocated at function exit * Heap vars deallocated by free() *)
 module StackAndHeapVars = Lattice.Prod(AllocaVars)(HeapVars)
 
-module ThreadIdToJoinedThreadsMap = MapDomain.MapBot(ThreadIdDomain.ThreadLifted)(ConcDomain.MustThreadSet)
+module ThreadIdToJoinedThreadsMap = MapDomain.MapBot(ThreadIdDomain.ThreadLifted)(ConcDomain.FiniteMustThreadSet)
 
 module Spec : Analyses.MCPSpec =
 struct
@@ -46,8 +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 = ConcDomain.MustThreadSet.mem current joined_threads 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,5 +1,14 @@
 (** Domains for thread sets and their uniqueness. *)
 
+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
   include SetDomain.Make (ThreadIdDomain.Thread)
@@ -19,8 +28,9 @@ struct
 
   let narrow x y = merge (fun x y -> widen x (join x y)) narrow x y
 
+  let diff_mustset x (y: FiniteMustThreadSet.t) =
+    FiniteMustThreadSet.fold (fun t -> remove (ThreadIdDomain.Thread t)) y x
 end
-module MustThreadSet = SetDomain.Reverse(ThreadSet)
 
 module CreatedThreadSet = ThreadSet
 

src/cdomains/mHP.ml

@@ -10,7 +10,7 @@ module Pretty = GoblintCil.Pretty
 type t = {
   tid: ThreadIdDomain.ThreadLifted.t;
   created: ConcDomain.ThreadSet.t;
-  must_joined: ConcDomain.ThreadSet.t;
+  must_joined: ConcDomain.FiniteMustThreadSet.t;
 } [@@deriving eq, ord, hash, relift]
 
 let current (ask:Queries.ask) =
@@ -35,10 +35,10 @@ let pretty () {tid; created; must_joined} =
       Some (Pretty.dprintf "created=%a" ConcDomain.ThreadSet.pretty created)
   in
   let must_joined_doc =
-    if ConcDomain.ThreadSet.is_empty must_joined then
+    if ConcDomain.FiniteMustThreadSet.is_empty must_joined then
       None
     else
-      Some (Pretty.dprintf "must_joined=%a" ConcDomain.ThreadSet.pretty must_joined)
+      Some (Pretty.dprintf "must_joined=%a" ConcDomain.FiniteMustThreadSet.pretty must_joined)
   in
   let docs = List.filter_map Fun.id [tid_doc; created_doc; must_joined_doc] in
   Pretty.dprintf "{%a}" (Pretty.d_list "; " Pretty.insert) docs
@@ -63,17 +63,10 @@ let definitely_not_started (current, created) other =
       not @@ ConcDomain.ThreadSet.exists (ident_or_may_be_created) created
 
 let exists_definitely_not_started_in_joined (current,created) other_joined =
-  if ConcDomain.ThreadSet.is_top other_joined then
-    false
-  else
-    ConcDomain.ThreadSet.exists (definitely_not_started (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 =
-  if ConcDomain.ThreadSet.is_top joined then
-    true (* top means all threads are joined, so [other] must be as well *)
-  else
-    ConcDomain.ThreadSet.mem other joined
+(** 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 =

src/domains/queries.ml

@@ -126,7 +126,7 @@ type _ t =
   | ActiveJumpBuf: JmpBufDomain.ActiveLongjmps.t t
   | ValidLongJmp: JmpBufDomain.JmpBufSet.t t
   | CreatedThreads: ConcDomain.ThreadSet.t t
-  | MustJoinedThreads: ConcDomain.MustThreadSet.t t
+  | MustJoinedThreads: ConcDomain.FiniteMustThreadSet.t t
   | ThreadsJoinedCleanly: MustBool.t t
   | MustProtectedVars: mustprotectedvars -> VS.t t
   | MustProtectingLocks: mustprotectinglocks -> LockDomain.MustLockset.t t
@@ -202,7 +202,7 @@ struct
     | ActiveJumpBuf -> (module JmpBufDomain.ActiveLongjmps)
     | ValidLongJmp ->  (module JmpBufDomain.JmpBufSet)
     | CreatedThreads ->  (module ConcDomain.ThreadSet)
-    | MustJoinedThreads -> (module ConcDomain.MustThreadSet)
+    | MustJoinedThreads -> (module ConcDomain.FiniteMustThreadSet)
     | ThreadsJoinedCleanly -> (module MustBool)
     | MustProtectedVars _ -> (module VS)
     | MustProtectingLocks _ -> (module LockDomain.MustLockset)
@@ -277,7 +277,7 @@ struct
     | ActiveJumpBuf -> JmpBufDomain.ActiveLongjmps.top ()
     | ValidLongJmp -> JmpBufDomain.JmpBufSet.top ()
     | CreatedThreads -> ConcDomain.ThreadSet.top ()
-    | MustJoinedThreads -> ConcDomain.MustThreadSet.top ()
+    | MustJoinedThreads -> ConcDomain.FiniteMustThreadSet.top ()
     | ThreadsJoinedCleanly -> MustBool.top ()
     | MustProtectedVars _ -> VS.top ()
     | MustProtectingLocks _ -> LockDomain.MustLockset.top ()