Skip to content

Commit 71b1ec4

Browse files
committed
use man.ask instead of ask.f
1 parent 9ff2446 commit 71b1ec4

File tree

2 files changed

+19
-26
lines changed

2 files changed

+19
-26
lines changed

src/analyses/creationLockset.ml

Lines changed: 16 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -35,44 +35,42 @@ module Spec = struct
3535

3636
(** reflexive-transitive closure of child relation applied to [tid]
3737
and filtered to only include threads, where [tid] is a must-ancestor
38-
@param ask any ask
38+
@param man any man
3939
@param tid
4040
*)
41-
let must_ancestor_descendants_closure (ask : Queries.ask) tid =
42-
let descendants = ask.f @@ Queries.DescendantThreads tid in
41+
let must_ancestor_descendants_closure man tid =
42+
let descendants = man.ask @@ Queries.DescendantThreads tid in
4343
let must_ancestors_descendants = TIDs.filter (TID.must_be_ancestor tid) descendants in
4444
TIDs.add tid must_ancestors_descendants
4545

4646
let threadspawn man ~multiple lval f args fman =
47-
let ask = ask_of_man man in
48-
let tid_lifted = ask.f Queries.CurrentThreadId in
49-
let child_ask = ask_of_man fman in
50-
let child_tid_lifted = child_ask.f Queries.CurrentThreadId in
47+
let tid_lifted = man.ask Queries.CurrentThreadId in
48+
let child_tid_lifted = fman.ask Queries.CurrentThreadId in
5149
match tid_lifted, child_tid_lifted with
5250
| `Lifted tid, `Lifted child_tid when TID.must_be_ancestor tid child_tid ->
53-
let must_ancestor_descendants = must_ancestor_descendants_closure child_ask child_tid in
54-
let lockset = ask.f Queries.MustLockset in
51+
let must_ancestor_descendants = must_ancestor_descendants_closure fman child_tid in
52+
let lockset = man.ask Queries.MustLockset in
5553
let to_contribute = G.singleton tid lockset in
5654
TIDs.iter (contribute_locks man to_contribute) must_ancestor_descendants
5755
| _ -> ()
5856

5957
(** compute all descendant threads that may run along with the ego thread at a program point.
6058
for all of them, tid must be an ancestor
59+
@param man man of ego thread at the program point
6160
@param tid ego thread id
62-
@param ask ask of ego thread at the program point
6361
*)
64-
let get_must_ancestor_running_descendants tid (ask : Queries.ask) =
65-
let may_created_tids = ask.f Queries.CreatedThreads in
62+
let get_must_ancestor_running_descendants man tid =
63+
let may_created_tids = man.ask Queries.CreatedThreads in
6664
let may_must_ancestor_created_tids =
6765
TIDs.filter (TID.must_be_ancestor tid) may_created_tids
6866
in
6967
let may_transitively_created_tids =
7068
TIDs.fold
71-
(fun child_tid acc -> TIDs.union acc (must_ancestor_descendants_closure ask child_tid))
69+
(fun child_tid acc -> TIDs.union acc (must_ancestor_descendants_closure man child_tid))
7270
may_must_ancestor_created_tids
7371
(TIDs.empty ())
7472
in
75-
let must_joined_tids = ask.f Queries.MustJoinedThreads in
73+
let must_joined_tids = man.ask Queries.MustJoinedThreads in
7674
TIDs.diff may_transitively_created_tids must_joined_tids
7775

7876
(** handle unlock of mutex [lock] *)
@@ -97,11 +95,10 @@ module Spec = struct
9795
let event man e _ =
9896
match e with
9997
| Events.Unlock addr ->
100-
let ask = ask_of_man man in
101-
let tid_lifted = ask.f Queries.CurrentThreadId in
98+
let tid_lifted = man.ask Queries.CurrentThreadId in
10299
(match tid_lifted with
103100
| `Lifted tid ->
104-
let possibly_running_tids = get_must_ancestor_running_descendants tid ask in
101+
let possibly_running_tids = get_must_ancestor_running_descendants man tid in
105102
let lock_opt = LockDomain.MustLock.of_addr addr in
106103
(match lock_opt with
107104
| Some lock -> unlock man tid possibly_running_tids lock
@@ -147,11 +144,10 @@ module Spec = struct
147144
end
148145

149146
let access man _ =
150-
let ask = ask_of_man man in
151-
let tid_lifted = ask.f Queries.CurrentThreadId in
147+
let tid_lifted = man.ask Queries.CurrentThreadId in
152148
match tid_lifted with
153149
| `Lifted tid ->
154-
let lockset = ask.f Queries.MustLockset in
150+
let lockset = man.ask Queries.MustLockset in
155151
let creation_lockset = man.global tid in
156152
tid, lockset, creation_lockset
157153
| _ -> ThreadIdDomain.UnknownThread, Lockset.empty (), G.empty ()

src/analyses/threadDescendants.ml

Lines changed: 3 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -24,19 +24,16 @@ module Spec = struct
2424
match x with
2525
| Queries.DescendantThreads t ->
2626
let children = man.global t in
27-
let ask = ask_of_man man in
2827
(G.fold
29-
(fun e acc -> G.union (ask.f @@ Queries.DescendantThreads e) acc)
28+
(fun e acc -> G.union (man.ask @@ Queries.DescendantThreads e) acc)
3029
children
3130
children
3231
: G.t)
3332
| _ -> Queries.Result.top x
3433

3534
let threadspawn man ~multiple lval f args fman =
36-
let ask = ask_of_man man in
37-
let tid_lifted = ask.f Queries.CurrentThreadId in
38-
let child_ask = ask_of_man fman in
39-
let child_tid_lifted = child_ask.f Queries.CurrentThreadId in
35+
let tid_lifted = man.ask Queries.CurrentThreadId in
36+
let child_tid_lifted = fman.ask Queries.CurrentThreadId in
4037
match tid_lifted, child_tid_lifted with
4138
| `Lifted tid, `Lifted child_tid -> man.sideg tid (G.singleton child_tid)
4239
| _ -> ()

0 commit comments

Comments
 (0)