diff --git a/infer/src/concurrency/RacerDConfig.ml b/infer/src/concurrency/RacerDConfig.ml index 2a126cce9..32029348b 100644 --- a/infer/src/concurrency/RacerDConfig.ml +++ b/infer/src/concurrency/RacerDConfig.ml @@ -702,7 +702,7 @@ module Models = struct (* at most one function is allowed to be true *) let may_block = - let open StarvationDomain.LockEvent in + let open StarvationDomain.Event in let matchers = [ (is_blocking_java_io, Low) ; (is_countdownlatch_await, Medium) diff --git a/infer/src/concurrency/RacerDConfig.mli b/infer/src/concurrency/RacerDConfig.mli index 109d63f98..e4d9d0f0d 100644 --- a/infer/src/concurrency/RacerDConfig.mli +++ b/infer/src/concurrency/RacerDConfig.mli @@ -82,7 +82,7 @@ module Models : sig requested via @ThreadSafe *) val may_block : - Tenv.t -> Typ.Procname.t -> HilExp.t list -> StarvationDomain.LockEvent.severity_t option + Tenv.t -> Typ.Procname.t -> HilExp.t list -> StarvationDomain.Event.severity_t option (** is the method call potentially blocking, given the actuals passed? *) val is_synchronized_library_call : Tenv.t -> Typ.Procname.t -> bool diff --git a/infer/src/concurrency/starvation.ml b/infer/src/concurrency/starvation.ml index 4bf2c560b..6fbe41a1e 100644 --- a/infer/src/concurrency/starvation.ml +++ b/infer/src/concurrency/starvation.ml @@ -137,7 +137,7 @@ let analyze_procedure {Callbacks.proc_desc; tenv; summary} = let make_trace_with_header ?(header= "") elem pname = - let trace = StarvationDomain.LockOrder.make_loc_trace elem in + let trace = StarvationDomain.Order.make_loc_trace elem in let trace_descr = Format.asprintf "%s %a" header (MF.wrap_monospaced Typ.Procname.pp) pname in let start_loc = List.hd trace |> Option.value_map ~default:Location.dummy ~f:(fun lt -> lt.Errlog.lt_loc) @@ -163,8 +163,7 @@ let get_summaries_of_methods_in_class tenv clazz = (** per-procedure report map, which takes care of deduplication *) module ReportMap = struct - type issue_t = Starvation of StarvationDomain.LockEvent.severity_t | Deadlock - [@@deriving compare] + type issue_t = Starvation of StarvationDomain.Event.severity_t | Deadlock [@@deriving compare] type report_t = { issue: issue_t @@ -222,31 +221,29 @@ end let should_report_deadlock_on_current_proc current_elem endpoint_elem = let open StarvationDomain in - match (current_elem.LockOrder.first, current_elem.LockOrder.eventually) with - | None, _ | Some {LockEvent.event= MayBlock _}, _ | _, {LockEvent.event= MayBlock _} -> + match (current_elem.Order.first, current_elem.Order.eventually) with + | None, _ | Some {Event.event= MayBlock _}, _ | _, {Event.event= MayBlock _} -> (* should never happen *) - L.die InternalError "Deadlock cannot occur without two lock events: %a" LockOrder.pp - current_elem - | Some {LockEvent.event= LockAcquire ((Var.LogicalVar _, _), [])}, _ -> + L.die InternalError "Deadlock cannot occur without two lock events: %a" Order.pp current_elem + | Some {Event.event= LockAcquire ((Var.LogicalVar _, _), [])}, _ -> (* first event is a class object (see [lock_of_class]), so always report because the reverse ordering on the events will not occur *) true - | Some {LockEvent.event= LockAcquire ((Var.LogicalVar _, _), _ :: _)}, _ - | _, {LockEvent.event= LockAcquire ((Var.LogicalVar _, _), _)} -> + | Some {Event.event= LockAcquire ((Var.LogicalVar _, _), _ :: _)}, _ + | _, {Event.event= LockAcquire ((Var.LogicalVar _, _), _)} -> (* first event has an ident root, but has a non-empty access path, which means we are not filtering out local variables (see [exec_instr]), or, second event has an ident root, which should not happen if we are filtering locals *) - L.die InternalError "Deadlock cannot occur on these logical variables: %a @." LockOrder.pp + L.die InternalError "Deadlock cannot occur on these logical variables: %a @." Order.pp current_elem - | ( Some {LockEvent.event= LockAcquire ((_, typ1), _)} - , {LockEvent.event= LockAcquire ((_, typ2), _)} ) -> + | Some {Event.event= LockAcquire ((_, typ1), _)}, {Event.event= LockAcquire ((_, typ2), _)} -> (* use string comparison on types as a stable order to decide whether to report a deadlock *) let c = String.compare (Typ.to_string typ1) (Typ.to_string typ2) in c < 0 || Int.equal 0 c && (* same class, so choose depending on location *) - Location.compare current_elem.LockOrder.eventually.LockEvent.loc - endpoint_elem.LockOrder.eventually.LockEvent.loc + Location.compare current_elem.Order.eventually.Event.loc + endpoint_elem.Order.eventually.Event.loc < 0 @@ -263,35 +260,35 @@ let report_deadlocks tenv current_pdesc (summary, current_main) report_map' = let report_endpoint_elem current_elem endpoint_pname elem report_map = if not - ( LockOrder.may_deadlock current_elem elem + ( Order.may_deadlock current_elem elem && should_report_deadlock_on_current_proc current_elem elem ) then report_map else - let () = debug "Possible deadlock:@.%a@.%a@." LockOrder.pp current_elem LockOrder.pp elem in - match (current_elem.LockOrder.eventually, elem.LockOrder.eventually) with - | {LockEvent.event= LockAcquire _}, {LockEvent.event= LockAcquire _} -> + let () = debug "Possible deadlock:@.%a@.%a@." Order.pp current_elem Order.pp elem in + match (current_elem.Order.eventually, elem.Order.eventually) with + | {Event.event= LockAcquire _}, {Event.event= LockAcquire _} -> let error_message = Format.asprintf "Potential deadlock.@.Trace 1 (starts at %a), %a.@.Trace 2 (starts at %a), %a." (MF.wrap_monospaced Typ.Procname.pp) - current_pname LockOrder.pp current_elem + current_pname Order.pp current_elem (MF.wrap_monospaced Typ.Procname.pp) - endpoint_pname LockOrder.pp elem + endpoint_pname Order.pp elem in let first_trace = List.rev (make_loc_trace current_pname 1 current_elem) in let second_trace = make_loc_trace endpoint_pname 2 elem in let ltr = List.rev_append first_trace second_trace in - let loc = LockOrder.get_loc current_elem in + let loc = Order.get_loc current_elem in ReportMap.add_deadlock current_pname loc ltr error_message report_map | _, _ -> report_map in let report_on_current_elem elem report_map = match elem with - | {LockOrder.first= None} | {LockOrder.eventually= {LockEvent.event= LockEvent.MayBlock _}} -> + | {Order.first= None} | {Order.eventually= {Event.event= Event.MayBlock _}} -> report_map - | {LockOrder.eventually= {LockEvent.event= LockEvent.LockAcquire endpoint_lock}} -> - LockIdentity.owner_class endpoint_lock + | {Order.eventually= {Event.event= Event.LockAcquire endpoint_lock}} -> + Lock.owner_class endpoint_lock |> Option.value_map ~default:report_map ~f:(fun endpoint_class -> (* get the class of the root variable of the lock in the endpoint event and retrieve all the summaries of the methods of that class *) @@ -300,10 +297,10 @@ let report_deadlocks tenv current_pdesc (summary, current_main) report_map' = List.fold endpoint_summaries ~init:report_map ~f: (fun acc (endp_pname, (endp_summary, endp_ui)) -> if UIThreadDomain.is_empty current_main || UIThreadDomain.is_empty endp_ui then - LockOrderDomain.fold (report_endpoint_elem elem endp_pname) endp_summary acc + OrderDomain.fold (report_endpoint_elem elem endp_pname) endp_summary acc else acc ) ) in - LockOrderDomain.fold report_on_current_elem summary report_map' + OrderDomain.fold report_on_current_elem summary report_map' let report_blocks_on_main_thread tenv current_pdesc (order, ui) report_map' = @@ -312,37 +309,37 @@ let report_blocks_on_main_thread tenv current_pdesc (order, ui) report_map' = let report_remote_block ui_explain current_elem current_lock endpoint_pname endpoint_elem report_map = match endpoint_elem with - | { LockOrder.first= Some {LockEvent.event= LockEvent.LockAcquire lock} - ; eventually= {LockEvent.event= LockEvent.MayBlock (block_descr, sev)} } - when LockIdentity.equal current_lock lock -> + | { Order.first= Some {Event.event= Event.LockAcquire lock} + ; eventually= {Event.event= Event.MayBlock (block_descr, sev)} } + when Lock.equal current_lock lock -> let error_message = Format.asprintf "Method %a runs on UI thread (because %s) and %a, which may be held by another thread \ which %s." (MF.wrap_monospaced Typ.Procname.pp) - current_pname ui_explain LockIdentity.pp lock block_descr + current_pname ui_explain Lock.pp lock block_descr in let first_trace = List.rev (make_loc_trace current_pname 1 current_elem) in let second_trace = make_loc_trace endpoint_pname 2 endpoint_elem in let ltr = List.rev_append first_trace second_trace in - let loc = LockOrder.get_loc current_elem in + let loc = Order.get_loc current_elem in ReportMap.add_starvation sev current_pname loc ltr error_message report_map | _ -> report_map in - let report_on_current_elem ui_explain ({LockOrder.eventually} as elem) report_map = + let report_on_current_elem ui_explain ({Order.eventually} as elem) report_map = match eventually with - | {LockEvent.event= LockEvent.MayBlock (_, sev)} -> + | {Event.event= Event.MayBlock (_, sev)} -> let error_message = Format.asprintf "Method %a runs on UI thread (because %s), and may block; %a." (MF.wrap_monospaced Typ.Procname.pp) - current_pname ui_explain LockEvent.pp_event eventually.LockEvent.event + current_pname ui_explain Event.pp_event eventually.Event.event in - let loc = LockOrder.get_loc elem in + let loc = Order.get_loc elem in let ltr = make_trace_with_header elem current_pname in ReportMap.add_starvation sev current_pname loc ltr error_message report_map - | {LockEvent.event= LockEvent.LockAcquire endpoint_lock} -> - LockIdentity.owner_class endpoint_lock + | {Event.event= Event.LockAcquire endpoint_lock} -> + Lock.owner_class endpoint_lock |> Option.value_map ~default:report_map ~f:(fun endpoint_class -> (* get the class of the root variable of the lock in the endpoint event and retrieve all the summaries of the methods of that class *) @@ -352,7 +349,7 @@ let report_blocks_on_main_thread tenv current_pdesc (order, ui) report_map' = (fun acc (endpoint_pname, (order, ui)) -> (* skip methods known to run on ui thread, as they cannot run in parallel to us *) if UIThreadDomain.is_empty ui then - LockOrderDomain.fold + OrderDomain.fold (report_remote_block ui_explain elem endpoint_lock endpoint_pname) order acc else acc ) ) @@ -361,7 +358,7 @@ let report_blocks_on_main_thread tenv current_pdesc (order, ui) report_map' = | AbstractDomain.Types.Bottom -> report_map' | AbstractDomain.Types.NonBottom ui_explain -> - LockOrderDomain.fold (report_on_current_elem ui_explain) order report_map' + OrderDomain.fold (report_on_current_elem ui_explain) order report_map' let reporting {Callbacks.procedures; exe_env} = diff --git a/infer/src/concurrency/starvationDomain.ml b/infer/src/concurrency/starvationDomain.ml index a72ef51a0..d5907230a 100644 --- a/infer/src/concurrency/starvationDomain.ml +++ b/infer/src/concurrency/starvationDomain.ml @@ -11,7 +11,7 @@ module F = Format module L = Logging module MF = MarkupFormatter -module LockIdentity = struct +module Lock = struct type t = AccessPath.t (* compare type, base variable modulo this and access list *) @@ -52,15 +52,14 @@ module LockIdentity = struct let owner_class ((_, typ), _) = Typ.inner_name typ end -module LockEvent = struct +module Event = struct type severity_t = Low | Medium | High [@@deriving compare] - type event_t = LockAcquire of LockIdentity.t | MayBlock of (string * severity_t) - [@@deriving compare] + type event_t = LockAcquire of Lock.t | MayBlock of (string * severity_t) [@@deriving compare] let pp_event fmt = function | LockAcquire lock -> - LockIdentity.pp fmt lock + Lock.pp fmt lock | MayBlock (msg, _) -> F.pp_print_string fmt msg @@ -80,7 +79,7 @@ module LockEvent = struct let locks_equal e e' = match (e.event, e'.event) with | LockAcquire lock, LockAcquire lock' -> - LockIdentity.equal lock lock' + Lock.equal lock lock' | _, _ -> false @@ -88,7 +87,7 @@ module LockEvent = struct let locks_equal_modulo_base e e' = match (e.event, e'.event) with | LockAcquire lock, LockAcquire lock' -> - LockIdentity.equal_modulo_base lock lock' + Lock.equal_modulo_base lock lock' | _, _ -> false @@ -137,23 +136,22 @@ module LockEvent = struct if reverse then res else List.rev res end -module LockOrder = struct - type t = {first: LockEvent.t option; eventually: LockEvent.t} [@@deriving compare] +module Order = struct + type t = {first: Event.t option; eventually: Event.t} [@@deriving compare] let pp fmt o = match o.first with | None -> - F.fprintf fmt "eventually %a" LockEvent.pp o.eventually + F.fprintf fmt "eventually %a" Event.pp o.eventually | Some lock -> - F.fprintf fmt "first %a, and before releasing it, %a" LockEvent.pp lock LockEvent.pp - o.eventually + F.fprintf fmt "first %a, and before releasing it, %a" Event.pp lock Event.pp o.eventually let may_deadlock elem elem' = match (elem.first, elem'.first) with | Some b, Some b' -> - LockEvent.locks_equal_modulo_base b elem'.eventually - && LockEvent.locks_equal_modulo_base b' elem.eventually + Event.locks_equal_modulo_base b elem'.eventually + && Event.locks_equal_modulo_base b' elem.eventually | _, _ -> false @@ -161,47 +159,46 @@ module LockOrder = struct let make_eventually eventually = {first= None; eventually} let make_first_and_eventually b eventually = - if not (LockEvent.is_lock_event b) then L.(die InternalError) "Expected a lock event first." ; + if not (Event.is_lock_event b) then L.(die InternalError) "Expected a lock event first." ; {first= Some b; eventually} let with_callsite callsite o = - { o with - eventually= {o.eventually with LockEvent.trace= callsite :: o.eventually.LockEvent.trace} } + {o with eventually= {o.eventually with Event.trace= callsite :: o.eventually.Event.trace}} let get_loc {first; eventually} = - match first with Some event -> LockEvent.get_loc event | None -> LockEvent.get_loc eventually + match first with Some event -> Event.get_loc event | None -> Event.get_loc eventually let make_loc_trace o = let first_trace = - Option.value_map o.first ~default:[] ~f:(LockEvent.make_loc_trace ~reverse:true) + Option.value_map o.first ~default:[] ~f:(Event.make_loc_trace ~reverse:true) in - let eventually_trace = LockEvent.make_loc_trace o.eventually in + let eventually_trace = Event.make_loc_trace o.eventually in List.rev_append first_trace eventually_trace end -module LockOrderDomain = struct - include AbstractDomain.FiniteSet (LockOrder) +module OrderDomain = struct + include AbstractDomain.FiniteSet (Order) let with_callsite callsite lo = - fold (fun o acc -> add (LockOrder.with_callsite callsite o) acc) lo empty + fold (fun o acc -> add (Order.with_callsite callsite o) acc) lo empty let is_eventually_locked lock lo = - LockEvent.is_lock_event lock - && exists (fun pair -> LockEvent.locks_equal pair.LockOrder.eventually lock) lo + Event.is_lock_event lock + && exists (fun pair -> Event.locks_equal pair.Order.eventually lock) lo end -module LockStack = AbstractDomain.StackDomain (LockEvent) +module LockStack = AbstractDomain.StackDomain (Event) module LockState = struct - include AbstractDomain.InvertedMap (LockIdentity) (LockStack) + include AbstractDomain.InvertedMap (Lock) (LockStack) let is_taken lock_event map = - match lock_event.LockEvent.event with - | LockEvent.LockAcquire lock -> ( + match lock_event.Event.event with + | Event.LockAcquire lock -> ( try not (find lock map |> LockStack.is_empty) with Caml.Not_found -> false ) | _ -> false @@ -239,72 +236,90 @@ module UIThreadExplanationDomain = struct end module UIThreadDomain = AbstractDomain.BottomLifted (UIThreadExplanationDomain) -include AbstractDomain.Pair (AbstractDomain.Pair (LockState) (LockOrderDomain)) (UIThreadDomain) -let empty = ((LockState.empty, LockOrderDomain.empty), UIThreadDomain.empty) +type astate = {lock_state: LockState.astate; order: OrderDomain.astate; ui: UIThreadDomain.astate} -let is_empty ((ls, lo), main) = - LockState.is_empty ls && LockOrderDomain.is_empty lo && UIThreadDomain.is_empty main +let empty = {lock_state= LockState.empty; order= OrderDomain.empty; ui= UIThreadDomain.empty} + +let is_empty {lock_state; order; ui} = + LockState.is_empty lock_state && OrderDomain.is_empty order && UIThreadDomain.is_empty ui + + +let pp fmt {lock_state; order; ui} = + F.fprintf fmt "{lock_state= %a; order= %a; ui= %a}" LockState.pp lock_state OrderDomain.pp order + UIThreadDomain.pp ui + + +let join lhs rhs = + { lock_state= LockState.join lhs.lock_state rhs.lock_state + ; order= OrderDomain.join lhs.order rhs.order + ; ui= UIThreadDomain.join lhs.ui rhs.ui } + + +let widen ~prev ~next ~num_iters:_ = join prev next + +let ( <= ) ~lhs ~rhs = + UIThreadDomain.( <= ) ~lhs:lhs.ui ~rhs:rhs.ui && OrderDomain.( <= ) ~lhs:lhs.order ~rhs:rhs.order + && LockState.( <= ) ~lhs:lhs.lock_state ~rhs:rhs.lock_state (* for every lock b held locally, add a pair (b, lock_event), plus (None, lock_event) *) -let add_order_pairs ls lock_event acc = +let add_order_pairs order lock_event acc = (* add no pairs whatsoever if we already hold that lock *) - if LockState.is_taken lock_event ls then acc + if LockState.is_taken lock_event order then acc else let add_eventually acc = (* don't add an eventually-locks pair if there is already another with same endpoint*) - if LockOrderDomain.is_eventually_locked lock_event acc then acc + if OrderDomain.is_eventually_locked lock_event acc then acc else - let elem = LockOrder.make_eventually lock_event in - LockOrderDomain.add elem acc + let elem = Order.make_eventually lock_event in + OrderDomain.add elem acc in let add_first_and_eventually acc first = (* never add a pair of the form (a,a) -- should never happen due to the check above *) - let elem = LockOrder.make_first_and_eventually first lock_event in - LockOrderDomain.add elem acc + let elem = Order.make_first_and_eventually first lock_event in + OrderDomain.add elem acc in - LockState.fold_over_events add_first_and_eventually ls acc |> add_eventually + LockState.fold_over_events add_first_and_eventually order acc |> add_eventually + +let acquire ({lock_state; order} as astate) loc lockid = + let newlock_event = Event.make_acquire lockid loc in + { astate with + lock_state= LockState.acquire lockid newlock_event lock_state + ; order= add_order_pairs lock_state newlock_event order } -let acquire ((ls, lo), main) loc lockid = - let newlock_event = LockEvent.make_acquire lockid loc in - let lo' = add_order_pairs ls newlock_event lo in - let ls' = LockState.acquire lockid newlock_event ls in - ((ls', lo'), main) +let blocking_call ~caller ~callee sev loc ({lock_state; order} as astate) = + let newlock_event = Event.make_blocking_call ~caller ~callee sev loc in + {astate with order= add_order_pairs lock_state newlock_event order} -let blocking_call ~caller ~callee sev loc ((ls, lo), main) = - let newlock_event = LockEvent.make_blocking_call ~caller ~callee sev loc in - let lo' = add_order_pairs ls newlock_event lo in - ((ls, lo'), main) +let release ({lock_state} as astate) lockid = + {astate with lock_state= LockState.release lockid lock_state} -let release ((ls, lo), main) lockid = ((LockState.release lockid ls, lo), main) -let integrate_summary ((ls, lo), main) callee_pname loc callee_summary = - let callee_lo, callee_main = callee_summary in +let integrate_summary ({lock_state; order; ui} as astate) callee_pname loc callee_summary = + let callee_order, callee_ui = callee_summary in (* for each pair (b,a) in the callee, add (l,b) and (l,a) to the current state, where l is held locally *) let do_elem elem acc = - Option.value_map elem.LockOrder.first ~default:acc ~f:(fun b -> add_order_pairs ls b acc) - |> add_order_pairs ls elem.LockOrder.eventually + Option.value_map elem.Order.first ~default:acc ~f:(fun b -> add_order_pairs lock_state b acc) + |> add_order_pairs lock_state elem.Order.eventually in let callsite = CallSite.make callee_pname loc in (* add callsite to the "eventually" trace *) - let elems = LockOrderDomain.with_callsite callsite callee_lo in - let lo' = LockOrderDomain.fold do_elem elems lo in - let main' = UIThreadDomain.join main callee_main in - ((ls, lo'), main') + let elems = OrderDomain.with_callsite callsite callee_order in + {astate with order= OrderDomain.fold do_elem elems order; ui= UIThreadDomain.join ui callee_ui} -let set_on_ui_thread (sum, explain_opt) explain = - (sum, UIThreadDomain.join explain_opt (AbstractDomain.Types.NonBottom explain)) +let set_on_ui_thread ({ui} as astate) explain = + {astate with ui= UIThreadDomain.join ui (AbstractDomain.Types.NonBottom explain)} -let to_summary ((_, lo), main) = (lo, main) +let to_summary {order; ui} = (order, ui) -type summary = LockOrderDomain.astate * UIThreadDomain.astate +type summary = OrderDomain.astate * UIThreadDomain.astate -let pp_summary fmt (lo, main) = - F.fprintf fmt "LockOrder: %a, UIThread: %a" LockOrderDomain.pp lo UIThreadDomain.pp main +let pp_summary fmt (order, ui) = + F.fprintf fmt "Order: %a, UIThread: %a" OrderDomain.pp order UIThreadDomain.pp ui diff --git a/infer/src/concurrency/starvationDomain.mli b/infer/src/concurrency/starvationDomain.mli index f92923cdb..e9feaf9fa 100644 --- a/infer/src/concurrency/starvationDomain.mli +++ b/infer/src/concurrency/starvationDomain.mli @@ -12,7 +12,7 @@ module F = Format (** Abstraction of a path that represents a lock, special-casing equality and comparisons to work over type, base variable modulo this and access list *) -module LockIdentity : sig +module Lock : sig include PrettyPrintable.PrintableOrderedType with type t = AccessPath.t val owner_class : t -> Typ.name option @@ -21,12 +21,11 @@ module LockIdentity : sig val equal : t -> t -> bool end -(** A lock event. Equality/comparison disregards the call trace but includes location. *) -module LockEvent : sig +(** Event type. Equality/comparison disregards the call trace but includes location. *) +module Event : sig type severity_t = Low | Medium | High [@@deriving compare] - type event_t = LockAcquire of LockIdentity.t | MayBlock of (string * severity_t) - [@@deriving compare] + type event_t = LockAcquire of Lock.t | MayBlock of (string * severity_t) [@@deriving compare] val pp_event : F.formatter -> event_t -> unit @@ -40,8 +39,8 @@ end ("eventually"), or, - the "first" lock being taken *in the current method* and, before its release, the eventual acquisition of "eventually" *) -module LockOrder : sig - type t = private {first: LockEvent.t option; eventually: LockEvent.t} +module Order : sig + type t = private {first: Event.t option; eventually: Event.t} include PrettyPrintable.PrintableOrderedType with type t := t @@ -54,8 +53,8 @@ module LockOrder : sig val get_loc : t -> Location.t end -module LockOrderDomain : sig - include PrettyPrintable.PPSet with type elt = LockOrder.t +module OrderDomain : sig + include PrettyPrintable.PPSet with type elt = Order.t include AbstractDomain.WithBottom with type astate = t end @@ -65,19 +64,19 @@ module UIThreadDomain : include AbstractDomain.WithBottom -val acquire : astate -> Location.t -> LockIdentity.t -> astate +val acquire : astate -> Location.t -> Lock.t -> astate -val release : astate -> LockIdentity.t -> astate +val release : astate -> Lock.t -> astate val blocking_call : - caller:Typ.Procname.t -> callee:Typ.Procname.t -> LockEvent.severity_t -> Location.t -> astate + caller:Typ.Procname.t -> callee:Typ.Procname.t -> Event.severity_t -> Location.t -> astate -> astate val set_on_ui_thread : astate -> string -> astate (** set the property "runs on UI thread" to true by attaching the given explanation string as to why this method is thought to do so *) -type summary = LockOrderDomain.astate * UIThreadDomain.astate +type summary = OrderDomain.astate * UIThreadDomain.astate val pp_summary : F.formatter -> summary -> unit