@@ -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 ()
0 commit comments