Skip to content

Commit ee18c9a

Browse files
committed
improve printing of descendantLockset analysis
1 parent 717b52f commit ee18c9a

File tree

1 file changed

+13
-2
lines changed

1 file changed

+13
-2
lines changed

src/analyses/descendantLockset.ml

Lines changed: 13 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -128,8 +128,10 @@ module Spec = struct
128128
| _ -> man.local
129129

130130
module A = struct
131+
module DlProd = Printable.Prod (D) (G)
132+
131133
(** ego tid * lock history * (local descendant lockset * global descendant lockset) *)
132-
include Printable.Prod3 (TID) (Queries.LH) (Printable.Prod (D) (G))
134+
include Printable.Prod3 (TID) (Queries.LH) (DlProd)
133135

134136
let happens_before (t1, dl1) (t2, lh2) =
135137
let locks_held_creating_t2 = D.find t2 dl1 in
@@ -162,7 +164,16 @@ module Spec = struct
162164
|| happens_before_global dlg1 (t2, lh2)
163165
|| happens_before_global dlg2 (t1, lh1))
164166

165-
let should_print _ = false
167+
(* only descendant locksets need to be printed *)
168+
let pretty () (_, _, dl) = DlProd.pretty () dl
169+
let show (_, _, dl) = DlProd.show dl
170+
let to_yojson (_, _, dl) = DlProd.to_yojson dl
171+
let printXml f (_, _, dl) = DlProd.printXml f dl
172+
173+
let should_print (_, _, (dl, dlg)) =
174+
let ls_not_empty _ ls = not @@ Lockset.is_empty ls in
175+
D.exists (ls_not_empty) dl
176+
|| G.exists (fun _ -> TidToLocksetMapTop.exists (ls_not_empty)) dlg
166177
end
167178

168179
let access man _ =

0 commit comments

Comments
 (0)