Simplify descendantLockset access output, fix ambiguous history TID printing

src/analyses/descendantLockset.ml

@@ -96,10 +96,62 @@ module Spec = struct
     | _ -> man.local
 
   module A = struct
-    module DlLhProd = Printable.Prod3 (D) (G) (Queries.LH)
+    module D =
+    struct
+      include D
+      let name () = "local"
+      let should_print dl =
+        let ls_not_empty _ ls = not @@ Lockset.is_empty ls in
+        exists ls_not_empty dl
+    end
+    module G =
+    struct
+      include G
+      let name () = "global"
+      let should_print dlg =
+        exists (fun _ -> D.should_print) dlg
+    end
+    module LH =
+    struct
+      include Queries.LH
+      let should_print lh =
+        exists (fun l tids -> not @@ TIDs.is_empty tids) lh
+    end
+    module DlLhProd =
+    struct
+      include Printable.Prod3 (D) (G) (LH)
+      let should_print (dl, dlg, lh) =
+        D.should_print dl || G.should_print dlg || LH.should_print lh
+
+      let pretty () (dl, dlg, lh) =
+        let open GoblintCil in
+        let dl_doc =
+          if D.should_print dl then
+            Some (Pretty.dprintf "%s:%a" (D.name ()) D.pretty dl)
+          else
+            None
+        in
+        let dlg_doc =
+          if G.should_print dlg then
+            Some (Pretty.dprintf "%s:%a" (G.name ()) G.pretty dlg)
+          else
+            None
+        in
+        let lh_doc =
+          if LH.should_print lh then
+            Some (Pretty.dprintf "%s:%a" (LH.name ()) LH.pretty lh)
+          else
+            None
+        in
+        let docs = List.filter_map Fun.id [dl_doc; dlg_doc; lh_doc] in
+        Pretty.dprintf "(%a)" (Pretty.d_list ", " Pretty.insert) docs
+
+      let show x = GobPretty.sprint pretty x
+    end
 
     (** ego tid * (local descendant lockset * global descendant lockset * lock history) *)
     include Printable.Prod (TID) (DlLhProd)
+    let name () = "descendantLockset"
 
     (** checks if program point 1 must happen before program point 2
         @param (t1,dl1) thread id and descendant lockset of program point 1
@@ -113,7 +165,7 @@ module Spec = struct
       else
         let relevant_lh2_threads =
           Lockset.fold
-            (fun lock -> TIDs.union (Queries.LH.find lock lh2))
+            (fun lock -> TIDs.union (LH.find lock lh2))
             locks_held_creating_t2
             (TIDs.empty ())
         in
@@ -143,11 +195,7 @@ module Spec = struct
     let to_yojson (_, dl_dlg_lh) = DlLhProd.to_yojson dl_dlg_lh
     let printXml f (_, dl_dlg_lh) = DlLhProd.printXml f dl_dlg_lh
 
-    let should_print (_, (dl, dlg, lh)) =
-      let ls_not_empty _ ls = not @@ Lockset.is_empty ls in
-      D.exists ls_not_empty dl
-      || G.exists (fun _ -> D.exists ls_not_empty) dlg
-      || Queries.LH.exists (fun l tids -> not @@ TIDs.is_empty tids) lh
+    let should_print (_, dl_dlg_lh) = DlLhProd.should_print dl_dlg_lh
   end
 
   let access man _ =

src/cdomain/value/cdomains/threadIdDomain.ml

@@ -111,6 +111,7 @@ struct
     include Printable.Liszt (Base)
     (* Prefix is stored in reversed order (main is last) since prepending is more efficient. *)
     let name () = "prefix"
+    let pretty = Pretty.d_list ", " Base.pretty (* without surrounding [] (added below) *)
   end
   module S =
   struct
@@ -122,9 +123,9 @@ struct
   let pretty () (p, s) =
     let p = List.rev p in (* show in "unreversed" order *)
     if S.is_empty s then
-      P.pretty () p (* hide empty set *)
+      Pretty.dprintf "[%a]" P.pretty p (* hide empty set *)
     else
-      Pretty.dprintf "%a, %a" P.pretty p S.pretty s
+      Pretty.dprintf "[%a, %a]" P.pretty p S.pretty s
 
   let show x = GobPretty.sprint pretty x
 

src/domains/queries.ml

@@ -79,7 +79,11 @@ module YS = SetDomain.ToppedSet (YamlWitnessType.Entry) (struct let topname = "T
 
 module CL = MapDomain.MapBot_LiftTop (ThreadIdDomain.Thread) (LockDomain.MustLockset)
 
-module LH = MapDomain.MapTop (LockDomain.MustLock) (SetDomain.Reverse (ConcDomain.ThreadSet))
+module LH =
+struct
+  include MapDomain.MapTop (LockDomain.MustLock) (SetDomain.Reverse (ConcDomain.ThreadSet))
+  let name () = "lock history"
+end
 
 
 (** GADT for queries with specific result type. *)

tests/regression/53-races-mhp/56-dl_multiple_creates_sequential_racing.t

@@ -0,0 +1,41 @@
+  $ goblint --set ana.activated[+] threadJoins --set ana.activated[+] threadDescendants --set ana.activated[+] mustlockHistory --set ana.activated[+] descendantLockset --disable ana.thread.include-node 56-dl_multiple_creates_sequential_racing.c
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 13
+    dead: 0
+    total lines: 13
+  [Warning][Race] Memory location global (race with conf. 110): (56-dl_multiple_creates_sequential_racing.c:4:5-4:15)
+    write with descendantLockset:(lock history:{
+                                               mutex -> {[main], [main, {t1}]}
+                                             }) (conf. 110)  (exp: & global) (56-dl_multiple_creates_sequential_racing.c:11:3-11:11)
+    write with descendantLockset:(lock history:{
+                                               mutex -> {[main, {t1}]}
+                                             }) (conf. 110)  (exp: & global) (56-dl_multiple_creates_sequential_racing.c:11:3-11:11)
+    write with [descendantLockset:(lock history:{
+                                                mutex -> {[main, t1]}
+                                              }), thread:[main, t1]] (conf. 110)  (exp: & global) (56-dl_multiple_creates_sequential_racing.c:11:3-11:11)
+    write with [descendantLockset:(lock history:{
+                                                mutex -> {[main, t1], [main]}
+                                              }), thread:[main, t1]] (conf. 110)  (exp: & global) (56-dl_multiple_creates_sequential_racing.c:11:3-11:11)
+    write with [descendantLockset:(lock history:{
+                                                mutex -> {[main]}
+                                              }), mhp:{created={[main, t1], [main, {t1}]}}, lock:{mutex}, thread:[main]] (conf. 110)  (exp: & global) (56-dl_multiple_creates_sequential_racing.c:20:3-20:11)
+    read with descendantLockset:(lock history:{
+                                              mutex -> {[main], [main, {t1}]}
+                                            }) (conf. 110)  (exp: & global) (56-dl_multiple_creates_sequential_racing.c:11:3-11:11)
+    read with descendantLockset:(lock history:{
+                                              mutex -> {[main, {t1}]}
+                                            }) (conf. 110)  (exp: & global) (56-dl_multiple_creates_sequential_racing.c:11:3-11:11)
+    read with [descendantLockset:(lock history:{
+                                               mutex -> {[main, t1]}
+                                             }), thread:[main, t1]] (conf. 110)  (exp: & global) (56-dl_multiple_creates_sequential_racing.c:11:3-11:11)
+    read with [descendantLockset:(lock history:{
+                                               mutex -> {[main, t1], [main]}
+                                             }), thread:[main, t1]] (conf. 110)  (exp: & global) (56-dl_multiple_creates_sequential_racing.c:11:3-11:11)
+    read with [descendantLockset:(lock history:{
+                                               mutex -> {[main]}
+                                             }), mhp:{created={[main, t1], [main, {t1}]}}, lock:{mutex}, thread:[main]] (conf. 110)  (exp: & global) (56-dl_multiple_creates_sequential_racing.c:20:3-20:11)
+  [Info][Race] Memory locations race summary:
+    safe: 3
+    vulnerable: 0
+    unsafe: 1
+    total memory locations: 4

tests/regression/53-races-mhp/dune

@@ -0,0 +1,2 @@
+(cram
+ (deps (glob_files *.c)))