diff --git a/src/analyses/descendantLockset.ml b/src/analyses/descendantLockset.ml index 53e5f2c98b..4cd6fa4114 100644 --- a/src/analyses/descendantLockset.ml +++ b/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 _ = diff --git a/src/cdomain/value/cdomains/threadIdDomain.ml b/src/cdomain/value/cdomains/threadIdDomain.ml index 5ac8f02d9c..61b9099ce8 100644 --- a/src/cdomain/value/cdomains/threadIdDomain.ml +++ b/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 diff --git a/src/domains/queries.ml b/src/domains/queries.ml index 318ff3c270..1e209c1572 100644 --- a/src/domains/queries.ml +++ b/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. *) diff --git a/tests/regression/53-races-mhp/56-dl_multiple_creates_sequential_racing.t b/tests/regression/53-races-mhp/56-dl_multiple_creates_sequential_racing.t new file mode 100644 index 0000000000..0c42f7b562 --- /dev/null +++ b/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 diff --git a/tests/regression/53-races-mhp/dune b/tests/regression/53-races-mhp/dune new file mode 100644 index 0000000000..23c0dd3290 --- /dev/null +++ b/tests/regression/53-races-mhp/dune @@ -0,0 +1,2 @@ +(cram + (deps (glob_files *.c)))