diff --git a/infer/src/concurrency/starvation.ml b/infer/src/concurrency/starvation.ml index 7e39cd93c..a1f425ff9 100644 --- a/infer/src/concurrency/starvation.ml +++ b/infer/src/concurrency/starvation.ml @@ -220,21 +220,21 @@ end let should_report_deadlock_on_current_proc current_elem endpoint_elem = let open StarvationDomain in match (current_elem.Order.first, current_elem.Order.eventually) with - | None, _ | Some {Event.event= MayBlock _}, _ | _, {Event.event= MayBlock _} -> + | None, _ | Some {Event.elem= MayBlock _}, _ | _, {Event.elem= MayBlock _} -> (* should never happen *) 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 + | Some {Event.elem= LockAcquire ((Var.LogicalVar _, _), [])}, _ -> + (* first elem is a class object (see [lock_of_class]), so always report because the reverse ordering on the events will not occur *) true - | 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 + | Some {Event.elem= LockAcquire ((Var.LogicalVar _, _), _ :: _)}, _ + | _, {Event.elem= LockAcquire ((Var.LogicalVar _, _), _)} -> + (* first elem 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 *) + second elem has an ident root, which should not happen if we are filtering locals *) L.die InternalError "Deadlock cannot occur on these logical variables: %a @." Order.pp current_elem - | Some {Event.event= LockAcquire ((_, typ1), _)}, {Event.event= LockAcquire ((_, typ2), _)} -> + | Some {Event.elem= LockAcquire ((_, typ1), _)}, {Event.elem= 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 @@ -264,7 +264,7 @@ let report_deadlocks tenv current_pdesc {StarvationDomain.order; ui} report_map' else 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 _} -> + | {Event.elem= LockAcquire _}, {Event.elem= LockAcquire _} -> let error_message = Format.asprintf "Potential deadlock.@.Trace 1 (starts at %a), %a.@.Trace 2 (starts at %a), %a." @@ -283,12 +283,12 @@ let report_deadlocks tenv current_pdesc {StarvationDomain.order; ui} report_map' in let report_on_current_elem elem report_map = match elem with - | {Order.first= None} | {Order.eventually= {Event.event= Event.MayBlock _}} -> + | {Order.first= None} | {Order.eventually= {Event.elem= Event.MayBlock _}} -> report_map - | {Order.eventually= {Event.event= Event.LockAcquire endpoint_lock}} -> + | {Order.eventually= {Event.elem= 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 + (* get the class of the root variable of the lock in the endpoint elem and retrieve all the summaries of the methods of that class *) let endpoint_summaries = get_summaries_of_methods_in_class tenv endpoint_class in (* for each summary related to the endpoint, analyse and report on its pairs *) @@ -303,14 +303,14 @@ let report_deadlocks tenv current_pdesc {StarvationDomain.order; ui} report_map' OrderDomain.fold report_on_current_elem order report_map' -let report_blocks_on_main_thread tenv current_pdesc {StarvationDomain.order; ui} report_map' = +let report_starvation tenv current_pdesc {StarvationDomain.order; ui} report_map' = let open StarvationDomain in let current_pname = Procdesc.get_proc_name current_pdesc in let report_remote_block ui_explain current_elem current_lock endpoint_pname endpoint_elem report_map = match endpoint_elem with - | { Order.first= Some {Event.event= Event.LockAcquire lock} - ; eventually= {Event.event= Event.MayBlock (block_descr, sev)} } + | { Order.first= Some {Event.elem= Event.LockAcquire lock} + ; eventually= {Event.elem= Event.MayBlock (block_descr, sev)} } when Lock.equal current_lock lock -> let error_message = Format.asprintf @@ -329,19 +329,19 @@ let report_blocks_on_main_thread tenv current_pdesc {StarvationDomain.order; ui} in let report_on_current_elem ui_explain ({Order.eventually} as elem) report_map = match eventually with - | {Event.event= Event.MayBlock (_, sev)} -> + | {Event.elem= 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 Event.pp_event eventually.Event.event + current_pname ui_explain Event.pp_event eventually.Event.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 - | {Event.event= Event.LockAcquire endpoint_lock} -> + | {Event.elem= 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 + (* get the class of the root variable of the lock in the endpoint elem and retrieve all the summaries of the methods of that class *) let endpoint_summaries = get_summaries_of_methods_in_class tenv endpoint_class in (* for each summary related to the endpoint, analyse and report on its pairs *) @@ -367,7 +367,7 @@ let reporting {Callbacks.procedures; exe_env} = Payload.read proc_desc (Procdesc.get_proc_name proc_desc) |> Option.iter ~f:(fun summary -> report_deadlocks tenv proc_desc summary ReportMap.empty - |> report_blocks_on_main_thread tenv proc_desc summary |> ReportMap.log ) + |> report_starvation tenv proc_desc summary |> ReportMap.log ) in List.iter procedures ~f:report_procedure ; let sourcefile = exe_env.Exe_env.source_file in diff --git a/infer/src/concurrency/starvationDomain.ml b/infer/src/concurrency/starvationDomain.ml index a5ee90702..976998aec 100644 --- a/infer/src/concurrency/starvationDomain.ml +++ b/infer/src/concurrency/starvationDomain.ml @@ -52,6 +52,64 @@ module Lock = struct let owner_class ((_, typ), _) = Typ.inner_name typ end +module type TraceElem = sig + type elem_t + + type t = private {elem: elem_t; loc: Location.t; trace: CallSite.t list} + + include PrettyPrintable.PrintableOrderedType with type t := t + + val make : elem_t -> Location.t -> t + + val get_loc : t -> Location.t + + val make_loc_trace : ?reverse:bool -> t -> Errlog.loc_trace + + val with_callsite : t -> CallSite.t -> t +end + +module MakeTraceElem (Elem : PrettyPrintable.PrintableOrderedType) : + TraceElem with type elem_t = Elem.t = +struct + type elem_t = Elem.t + + type t = {elem: Elem.t; loc: Location.t; trace: CallSite.t list [@compare.ignore]} + [@@deriving compare] + + let pp fmt e = + let pp_trace fmt = function + | [] -> + () + | trace -> + F.fprintf fmt " (trace: %a)" (Pp.semicolon_seq CallSite.pp) trace + in + F.fprintf fmt "%a at %a%a" Elem.pp e.elem Location.pp e.loc pp_trace e.trace + + + let make elem loc = {elem; loc; trace= []} + + let get_loc {loc; trace} = List.hd trace |> Option.value_map ~default:loc ~f:CallSite.loc + + let make_loc_trace ?(reverse= false) e = + let call_trace, nesting = + List.fold e.trace ~init:([], 0) ~f:(fun (tr, ns) callsite -> + let elem_descr = + F.asprintf "Method call: %a" + (MF.wrap_monospaced Typ.Procname.pp) + (CallSite.pname callsite) + in + let elem = Errlog.make_trace_element ns (CallSite.loc callsite) elem_descr [] in + (elem :: tr, ns + 1) ) + in + let endpoint_descr = F.asprintf "%a" Elem.pp e.elem in + let endpoint = Errlog.make_trace_element nesting e.loc endpoint_descr [] in + let res = endpoint :: call_trace in + if reverse then res else List.rev res + + + let with_callsite elem callsite = {elem with trace= callsite :: elem.trace} +end + module Event = struct type severity_t = Low | Medium | High [@@deriving compare] @@ -64,20 +122,16 @@ module Event = struct F.pp_print_string fmt msg - type t = {event: event_t; loc: Location.t; trace: CallSite.t list} + include MakeTraceElem (struct + type t = event_t [@@deriving compare] - let is_lock_event e = match e.event with LockAcquire _ -> true | _ -> false - - (* ignore trace when comparing *) - let compare e e' = - if phys_equal e e' then 0 - else - let res = compare_event_t e.event e'.event in - if not (Int.equal res 0) then res else Location.compare e.loc e'.loc + let pp = pp_event + end) + let is_lock_event e = match e.elem with LockAcquire _ -> true | _ -> false let locks_equal e e' = - match (e.event, e'.event) with + match (e.elem, e'.elem) with | LockAcquire lock, LockAcquire lock' -> Lock.equal lock lock' | _, _ -> @@ -85,26 +139,14 @@ module Event = struct let locks_equal_modulo_base e e' = - match (e.event, e'.event) with + match (e.elem, e'.elem) with | LockAcquire lock, LockAcquire lock' -> Lock.equal_modulo_base lock lock' | _, _ -> false - let pp fmt e = - let pp_trace fmt = function - | [] -> - () - | trace -> - F.fprintf fmt " (trace: %a)" (Pp.semicolon_seq CallSite.pp) trace - in - F.fprintf fmt "%a at %a%a" pp_event e.event Location.pp e.loc pp_trace e.trace - - - let make_acquire lock loc = {event= LockAcquire lock; loc; trace= []} - - let make_blocks msg sev loc = {event= MayBlock (msg, sev); loc; trace= []} + let make_acquire lock loc = make (LockAcquire lock) loc let make_blocking_call ~caller ~callee sev loc = let descr = @@ -114,26 +156,14 @@ module Event = struct (MF.wrap_monospaced Typ.Procname.pp) caller in - make_blocks descr sev loc - + make (MayBlock (descr, sev)) loc +end - let get_loc {loc; trace} = List.hd trace |> Option.value_map ~default:loc ~f:CallSite.loc +module EventDomain = struct + include AbstractDomain.FiniteSet (Event) - let make_loc_trace ?(reverse= false) e = - let call_trace, nesting = - List.fold e.trace ~init:([], 0) ~f:(fun (tr, ns) callsite -> - let elem_descr = - F.asprintf "Method call: %a" - (MF.wrap_monospaced Typ.Procname.pp) - (CallSite.pname callsite) - in - let elem = Errlog.make_trace_element ns (CallSite.loc callsite) elem_descr [] in - (elem :: tr, ns + 1) ) - in - let endpoint_descr = F.asprintf "%a" pp_event e.event in - let endpoint = Errlog.make_trace_element nesting e.loc endpoint_descr [] in - let res = endpoint :: call_trace in - if reverse then res else List.rev res + let with_callsite astate callsite = + fold (fun e acc -> add (Event.with_callsite e callsite) acc) astate empty end module Order = struct @@ -159,16 +189,14 @@ module Order = struct let make_eventually eventually = {first= None; eventually} let make_first_and_eventually b eventually = - if not (Event.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 elem first." ; {first= Some b; eventually} - let with_callsite callsite o = - {o with eventually= {o.eventually with Event.trace= callsite :: o.eventually.Event.trace}} - + let with_callsite callsite o = {o with eventually= Event.with_callsite o.eventually callsite} let get_loc {first; eventually} = - match first with Some event -> Event.get_loc event | None -> Event.get_loc eventually + match first with Some elem -> Event.get_loc elem | None -> Event.get_loc eventually let make_loc_trace o = @@ -197,7 +225,7 @@ module LockState = struct include AbstractDomain.InvertedMap (Lock) (LockStack) let is_taken lock_event map = - match lock_event.Event.event with + match lock_event.Event.elem with | Event.LockAcquire lock -> ( try not (find lock map |> LockStack.is_empty) with Caml.Not_found -> false ) | _ -> @@ -237,21 +265,32 @@ end module UIThreadDomain = AbstractDomain.BottomLifted (UIThreadExplanationDomain) -type astate = {lock_state: LockState.astate; order: OrderDomain.astate; ui: UIThreadDomain.astate} +type astate = + { lock_state: LockState.astate + ; events: EventDomain.astate + ; order: OrderDomain.astate + ; ui: UIThreadDomain.astate } + +let empty = + { lock_state= LockState.empty + ; events= EventDomain.empty + ; order= OrderDomain.empty + ; ui= UIThreadDomain.empty } -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 is_empty {lock_state; events; order; ui} = + UIThreadDomain.is_empty ui && EventDomain.is_empty events && OrderDomain.is_empty order + && LockState.is_empty lock_state -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 pp fmt {lock_state; events; order; ui} = + F.fprintf fmt "{lock_state= %a; events= %a; order= %a; ui= %a}" LockState.pp lock_state + EventDomain.pp events OrderDomain.pp order UIThreadDomain.pp ui let join lhs rhs = { lock_state= LockState.join lhs.lock_state rhs.lock_state + ; events= EventDomain.join lhs.events rhs.events ; order= OrderDomain.join lhs.order rhs.order ; ui= UIThreadDomain.join lhs.ui rhs.ui } @@ -259,7 +298,9 @@ let join lhs rhs = 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 + UIThreadDomain.( <= ) ~lhs:lhs.ui ~rhs:rhs.ui + && EventDomain.( <= ) ~lhs:lhs.events ~rhs:rhs.events + && OrderDomain.( <= ) ~lhs:lhs.order ~rhs:rhs.order && LockState.( <= ) ~lhs:lhs.lock_state ~rhs:rhs.lock_state @@ -283,25 +324,28 @@ let add_order_pairs order lock_event acc = 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 +let acquire ({lock_state; events; order} as astate) loc lockid = + let new_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 } + lock_state= LockState.acquire lockid new_event lock_state + ; events= EventDomain.add new_event events + ; order= add_order_pairs lock_state new_event order } -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 ({lock_state; events; order} as astate) = + let new_event = Event.make_blocking_call ~caller ~callee sev loc in + { astate with + events= EventDomain.add new_event events; order= add_order_pairs lock_state new_event order } let release ({lock_state} as astate) lockid = {astate with lock_state= LockState.release lockid lock_state} -let integrate_summary ({lock_state; order; ui} as astate) callee_pname loc callee_summary = +let integrate_summary ({lock_state; events; order; ui} as astate) callee_pname loc callee_summary = let callee_order = callee_summary.order in let callee_ui = callee_summary.ui in + let callee_events = callee_summary.events 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 = @@ -311,7 +355,10 @@ let integrate_summary ({lock_state; order; ui} as astate) callee_pname loc calle let callsite = CallSite.make callee_pname loc in (* add callsite to the "eventually" trace *) let elems = OrderDomain.with_callsite callsite callee_order in - {astate with order= OrderDomain.fold do_elem elems order; ui= UIThreadDomain.join ui callee_ui} + { astate with + events= EventDomain.join events (EventDomain.with_callsite callee_events callsite) + ; order= OrderDomain.fold do_elem elems order + ; ui= UIThreadDomain.join ui callee_ui } let set_on_ui_thread ({ui} as astate) explain = diff --git a/infer/src/concurrency/starvationDomain.mli b/infer/src/concurrency/starvationDomain.mli index 6d5a803f1..1c9363443 100644 --- a/infer/src/concurrency/starvationDomain.mli +++ b/infer/src/concurrency/starvationDomain.mli @@ -29,11 +29,13 @@ module Event : sig val pp_event : F.formatter -> event_t -> unit - type t = private {event: event_t; loc: Location.t; trace: CallSite.t list} + type t = private {elem: event_t; loc: Location.t; trace: CallSite.t list} include PrettyPrintable.PrintableOrderedType with type t := t end +module EventDomain : module type of AbstractDomain.FiniteSet (Event) + (** Represents either - the existence of a program path from the current method to the eventual acquisition of a lock ("eventually"), or, @@ -64,7 +66,11 @@ module LockState : AbstractDomain.WithBottom module UIThreadDomain : AbstractDomain.WithBottom with type astate = string AbstractDomain.Types.bottom_lifted -type astate = {lock_state: LockState.astate; order: OrderDomain.astate; ui: UIThreadDomain.astate} +type astate = + { lock_state: LockState.astate + ; events: EventDomain.astate + ; order: OrderDomain.astate + ; ui: UIThreadDomain.astate } include AbstractDomain.WithBottom with type astate := astate