diff --git a/infer/src/backend/StarvationGlobalAnalysis.ml b/infer/src/backend/StarvationGlobalAnalysis.ml index b9a3b6193..944b67372 100644 --- a/infer/src/backend/StarvationGlobalAnalysis.ml +++ b/infer/src/backend/StarvationGlobalAnalysis.ml @@ -9,33 +9,38 @@ open! IStd module L = Logging module Domain = StarvationDomain -(* given a scheduled-work item, read the summary of the scheduled method from the disk - and adapt its contents to the thread it was scheduled too *) -let get_summary_of_scheduled_work (work_item : Domain.ScheduledWorkItem.t) = - let astate = {Domain.initial with thread= work_item.thread} in +let iter_scheduled_pair (work_item : Domain.ScheduledWorkItem.t) f = + let open Domain in let callsite = CallSite.make work_item.procname work_item.loc in - let open IOption.Let_syntax in - let* {Summary.payloads= {starvation}} = Summary.OnDisk.get work_item.procname in - let+ callee_astate = starvation in - let ({critical_pairs} : Domain.t) = Domain.integrate_summary callsite astate callee_astate in - critical_pairs + fun pair -> + CriticalPair.with_callsite pair callsite + |> CriticalPair.apply_caller_thread work_item.thread + |> Option.iter ~f + + +let iter_critical_pairs_of_summary f summary = + Domain.fold_critical_pairs_of_summary (fun pair () -> f pair) summary () + + +let iter_critical_pairs_of_scheduled_work f (work_item : Domain.ScheduledWorkItem.t) = + Summary.OnDisk.get work_item.procname + |> Option.bind ~f:(fun (summary : Summary.t) -> summary.payloads.starvation) + |> Option.iter ~f:(iter_critical_pairs_of_summary (iter_scheduled_pair work_item f)) -(* given a summary, do [f work critical_pairs] for each [work] item scheduled in the summary, - where [critical_pairs] are those of the method scheduled, adapted to the thread it's scheduled for *) let iter_summary ~f exe_env (summary : Summary.t) = let open Domain in Payloads.starvation summary.payloads - |> Option.iter ~f:(fun ({scheduled_work; critical_pairs} : summary) -> + |> Option.iter ~f:(fun (payload : summary) -> let pname = Summary.get_proc_name summary in let tenv = Exe_env.get_tenv exe_env pname in if StarvationModels.is_java_main_method pname || ConcurrencyModels.is_android_lifecycle_method tenv pname - then f pname critical_pairs ; + then iter_critical_pairs_of_summary (f pname) payload ; ScheduledWorkDomain.iter - (fun work -> get_summary_of_scheduled_work work |> Option.iter ~f:(f pname)) - scheduled_work ) + (iter_critical_pairs_of_scheduled_work (f pname)) + payload.scheduled_work ) module WorkHashSet = struct @@ -52,9 +57,7 @@ module WorkHashSet = struct include Caml.Hashtbl.Make (T) - let add_pairs work_set caller pairs = - let open Domain in - CriticalPairs.iter (fun pair -> replace work_set (caller, pair) ()) pairs + let add_pair work_set caller pair = replace work_set (caller, pair) () end let report exe_env work_set = @@ -74,19 +77,16 @@ let report exe_env work_set = (Summary.get_proc_desc summary, starvation) ) ) ) tenv pattrs pair acc in - match pair.elem.event with - | LockAcquire {locks} -> - List.fold locks ~init:acc ~f:(fun acc lock -> - let should_report_starvation = - CriticalPair.is_uithread pair && not (Procname.is_constructor procname) - in - WorkHashSet.fold - (fun (other_procname, (other_pair : CriticalPair.t)) () acc -> - Starvation.report_on_parallel_composition ~should_report_starvation tenv - pattrs pair lock other_procname other_pair acc ) - work_set acc ) - | _ -> - acc ) + Event.get_acquired_locks pair.elem.event + |> List.fold ~init:acc ~f:(fun acc lock -> + let should_report_starvation = + CriticalPair.is_uithread pair && not (Procname.is_constructor procname) + in + WorkHashSet.fold + (fun (other_procname, (other_pair : CriticalPair.t)) () acc -> + Starvation.report_on_parallel_composition ~should_report_starvation tenv + pattrs pair lock other_procname other_pair acc ) + work_set acc ) ) in WorkHashSet.fold wrap_report work_set Starvation.ReportMap.empty |> Starvation.ReportMap.store_multi_file @@ -97,7 +97,7 @@ let whole_program_analysis () = let work_set = WorkHashSet.create 1 in let exe_env = Exe_env.mk () in L.progress "Processing on-disk summaries...@." ; - Summary.OnDisk.iter_specs ~f:(iter_summary exe_env ~f:(WorkHashSet.add_pairs work_set)) ; + Summary.OnDisk.iter_specs ~f:(iter_summary exe_env ~f:(WorkHashSet.add_pair work_set)) ; L.progress "Loaded %d pairs@." (WorkHashSet.length work_set) ; L.progress "Reporting on processed summaries...@." ; report exe_env work_set diff --git a/infer/src/concurrency/starvation.ml b/infer/src/concurrency/starvation.ml index 1af657050..c8defc6e6 100644 --- a/infer/src/concurrency/starvation.ml +++ b/infer/src/concurrency/starvation.ml @@ -776,11 +776,11 @@ let report_on_pair ~analyze_ondemand tenv pattrs (pair : Domain.CriticalPair.t) then, report on the parallel composition of the current pair and any pair in these summaries that can indeed run in parallel *) fold_reportable_summaries analyze_ondemand tenv other_class ~init:acc - ~f:(fun acc (other_pname, {critical_pairs}) -> - CriticalPairs.fold + ~f:(fun acc (other_pname, summary) -> + Domain.fold_critical_pairs_of_summary (report_on_parallel_composition ~should_report_starvation tenv pattrs pair lock other_pname) - critical_pairs acc ) ) ) ) + summary acc ) ) ) ) | _ -> report_map @@ -788,10 +788,10 @@ let report_on_pair ~analyze_ondemand tenv pattrs (pair : Domain.CriticalPair.t) let reporting {InterproceduralAnalysis.procedures; file_exe_env; analyze_file_dependency} = if Config.starvation_whole_program then IssueLog.empty else - let report_on_proc tenv proc_desc report_map (payload : Domain.summary) = - Domain.CriticalPairs.fold + let report_on_proc tenv proc_desc report_map payload = + Domain.fold_critical_pairs_of_summary (report_on_pair ~analyze_ondemand:analyze_file_dependency tenv proc_desc) - payload.critical_pairs report_map + payload report_map in let report_procedure report_map procname = analyze_file_dependency procname diff --git a/infer/src/concurrency/starvationDomain.ml b/infer/src/concurrency/starvationDomain.ml index 81bdf23ed..606e46833 100644 --- a/infer/src/concurrency/starvationDomain.ml +++ b/infer/src/concurrency/starvationDomain.ml @@ -62,24 +62,24 @@ module ThreadDomain = struct (** given the current thread state [caller_thread] and the thread state under which a critical pair occurred, [pair_thread], decide whether to throw away the pair (returning [None]) because it cannot occur within a call from the current state, or adapt its thread state appropriately. *) - let apply_to_pair caller_thread pair_thread = - match (caller_thread, pair_thread) with + let apply_caller_thread ~caller ~callee = + match (caller, callee) with | UnknownThread, _ -> (* callee pair knows more than us *) - Some pair_thread + Some callee | AnyThread, UnknownThread -> (* callee pair knows nothing and caller has abstracted away info *) Some AnyThread | AnyThread, _ -> (* callee pair is UI / BG / Any and caller has abstracted away info so use callee's knowledge *) - Some pair_thread + Some callee | UIThread, BGThread | BGThread, UIThread -> (* annotations or assertions are incorrectly used in code, or callee is path-sensitive on thread-identity, just drop the callee pair *) None | _, _ -> (* caller is UI or BG and callee does not disagree, so use that *) - Some caller_thread + Some caller end module Lock = struct @@ -125,6 +125,18 @@ module Lock = struct (lock' :: locks', true) ) in apply_subst_to_list_inner l |> fst + + + let is_recursive tenv lock = + let is_class_and_recursive_lock = function + | {Typ.desc= Tptr ({desc= Tstruct name}, _)} | {desc= Tstruct name} -> + ConcurrencyModels.is_recursive_lock_type name + | typ -> + L.debug Analysis Verbose "Asked if non-struct type %a is a recursive lock type.@." + (Typ.pp_full Pp.text) typ ; + true + in + get_typ tenv lock |> Option.exists ~f:is_class_and_recursive_lock end module AccessExpressionDomain = struct @@ -223,6 +235,14 @@ module Event = struct MonitorWait {monitor_wait with thread} + let apply_caller_thread caller_thread event = + match ThreadDomain.apply_caller_thread ~caller:caller_thread ~callee:(get_thread event) with + | None -> + None + | Some thread -> + Some (with_thread event thread) + + let make_acquire locks thread = LockAcquire {locks; thread} let make_blocking_call callee severity thread = MayBlock {callee; severity; thread} @@ -231,6 +251,8 @@ module Event = struct let make_object_wait lock thread = MonitorWait {lock; thread} + let get_acquired_locks = function LockAcquire {locks} -> locks | _ -> [] + let apply_subst subst event = match event with | MayBlock _ | StrictModeCall _ -> @@ -251,6 +273,10 @@ module Event = struct Some event | locks -> Some (LockAcquire {locks; thread}) ) + + + let has_recursive_lock tenv event = + get_acquired_locks event |> List.exists ~f:(Lock.is_recursive tenv) end (** A lock acquisition with source location and procname in which it occurs. The location & procname @@ -259,7 +285,9 @@ module Acquisition = struct type t = {lock: Lock.t; loc: Location.t [@compare.ignore]; procname: Procname.t [@compare.ignore]} [@@deriving compare] - let pp fmt {lock} = Lock.pp fmt lock + let pp fmt {lock; loc; procname} = + F.fprintf fmt "" Lock.pp lock Location.pp loc Procname.pp procname + let describe fmt {lock} = Lock.pp_locks fmt lock @@ -419,23 +447,6 @@ module CriticalPairElement = struct Some {acquisitions; event} end -let is_recursive_lock event tenv = - let is_class_and_recursive_lock = function - | {Typ.desc= Tptr ({desc= Tstruct name}, _)} | {desc= Tstruct name} -> - ConcurrencyModels.is_recursive_lock_type name - | typ -> - L.debug Analysis Verbose "Asked if non-struct type %a is a recursive lock type.@." - (Typ.pp_full Pp.text) typ ; - true - in - match (event : Event.t) with - | LockAcquire {locks} -> - List.exists locks ~f:(fun lock_path -> - Lock.get_typ tenv lock_path |> Option.exists ~f:is_class_and_recursive_lock ) - | _ -> - false - - module CriticalPair = struct include ExplicitTrace.MakeTraceElem (CriticalPairElement) (ExplicitTrace.DefaultCallPrinter) @@ -444,11 +455,8 @@ module CriticalPair = struct let get_thread {elem} = CriticalPairElement.get_thread elem let may_deadlock tenv ~(lhs : t) ~lhs_lock ~(rhs : t) = - let get_acquired_locks {elem= {event}} = - match event with LockAcquire {locks} -> locks | _ -> [] - in if ThreadDomain.can_run_in_parallel (get_thread lhs) (get_thread rhs) then - get_acquired_locks rhs + Event.get_acquired_locks rhs.elem.event |> List.find ~f:(fun rhs_lock -> (not (Lock.equal_across_threads tenv lhs_lock rhs_lock)) && Acquisitions.lock_is_held_in_other_thread tenv rhs_lock lhs.elem.acquisitions @@ -474,7 +482,7 @@ module CriticalPair = struct let filtered_locks = IList.filter_changed locks ~f:(fun lock -> (not (Acquisitions.lock_is_held lock held_locks)) - || not (is_recursive_lock pair.elem.event tenv) ) + || not (Event.has_recursive_lock tenv pair.elem.event) ) in match filtered_locks with | [] -> @@ -487,22 +495,27 @@ module CriticalPair = struct Some pair - let integrate_summary_opt ?subst ?tenv existing_acquisitions call_site + let apply_caller_thread caller_thread callee_pair = + match Event.apply_caller_thread caller_thread callee_pair.elem.event with + | None -> + None + | Some event when phys_equal event callee_pair.elem.event -> + Some callee_pair + | Some event -> + Some (map ~f:(fun (elem : CriticalPairElement.t) -> {elem with event}) callee_pair) + + + let integrate_summary_opt ~subst ~tenv existing_acquisitions call_site (caller_thread : ThreadDomain.t) (callee_pair : t) = - let substitute_pair subst callee_pair = - match subst with None -> Some callee_pair | Some subst -> apply_subst subst callee_pair - in - substitute_pair subst callee_pair - |> Option.bind ~f:(filter_out_reentrant_relocks tenv existing_acquisitions) - |> Option.bind ~f:(fun callee_pair -> - ThreadDomain.apply_to_pair caller_thread (get_thread callee_pair) - |> Option.map ~f:(fun thread -> - let f (elem : CriticalPairElement.t) = - let acquisitions = Acquisitions.union existing_acquisitions elem.acquisitions in - let event = Event.with_thread elem.event thread in - ({acquisitions; event} : elem_t) - in - with_callsite (map ~f callee_pair) call_site ) ) + apply_subst subst callee_pair + |> Option.bind ~f:(filter_out_reentrant_relocks (Some tenv) existing_acquisitions) + |> Option.bind ~f:(apply_caller_thread caller_thread) + |> Option.map ~f:(fun callee_pair -> + let f (elem : CriticalPairElement.t) = + {elem with acquisitions= Acquisitions.union existing_acquisitions elem.acquisitions} + in + map ~f callee_pair ) + |> Option.map ~f:(fun callee_pair -> with_callsite callee_pair call_site) let get_earliest_lock_or_call_loc ~procname ({elem= {acquisitions}} as t) = @@ -570,13 +583,14 @@ end module CriticalPairs = struct include CriticalPair.FiniteSet - let with_callsite astate ?tenv ?subst lock_state call_site thread = + let with_callsite astate ~tenv ~subst lock_state call_site thread = let existing_acquisitions = LockState.get_acquisitions lock_state in fold (fun critical_pair acc -> - CriticalPair.integrate_summary_opt ?subst ?tenv existing_acquisitions call_site thread + CriticalPair.integrate_summary_opt ~subst ~tenv existing_acquisitions call_site thread critical_pair - |> Option.bind ~f:(CriticalPair.filter_out_reentrant_relocks tenv existing_acquisitions) + |> Option.bind + ~f:(CriticalPair.filter_out_reentrant_relocks (Some tenv) existing_acquisitions) |> Option.value_map ~default:acc ~f:(fun new_pair -> add new_pair acc) ) astate empty end @@ -723,18 +737,18 @@ let leq ~lhs ~rhs = && VarDomain.leq ~lhs:lhs.var_state ~rhs:rhs.var_state -let add_critical_pair ?tenv lock_state event ~loc acc = +let add_critical_pair ~tenv_opt lock_state event ~loc acc = let acquisitions = LockState.get_acquisitions lock_state in let critical_pair = CriticalPair.make ~loc acquisitions event in - CriticalPair.filter_out_reentrant_relocks tenv acquisitions critical_pair + CriticalPair.filter_out_reentrant_relocks tenv_opt acquisitions critical_pair |> Option.value_map ~default:acc ~f:(fun pair -> CriticalPairs.add pair acc) -let acquire ?tenv ({lock_state; critical_pairs} as astate) ~procname ~loc locks = +let acquire ~tenv ({lock_state; critical_pairs} as astate) ~procname ~loc locks = { astate with critical_pairs= (let event = Event.make_acquire locks astate.thread in - add_critical_pair ?tenv lock_state event ~loc critical_pairs ) + add_critical_pair ~tenv_opt:(Some tenv) lock_state event ~loc critical_pairs ) ; lock_state= List.fold locks ~init:lock_state ~f:(fun acc lock -> LockState.acquire ~procname ~loc lock acc ) } @@ -744,7 +758,8 @@ let make_call_with_event new_event ~loc astate = if astate.ignore_blocking_calls then astate else { astate with - critical_pairs= add_critical_pair astate.lock_state new_event ~loc astate.critical_pairs } + critical_pairs= + add_critical_pair ~tenv_opt:None astate.lock_state new_event ~loc astate.critical_pairs } let blocking_call ~callee sev ~loc astate = @@ -850,17 +865,15 @@ let pp_summary fmt (summary : summary) = AttributeDomain.pp summary.attributes -let integrate_summary ?tenv ?lhs ?subst callsite (astate : t) (summary : summary) = +let integrate_summary ~tenv ~lhs ~subst callsite (astate : t) (summary : summary) = let critical_pairs' = - CriticalPairs.with_callsite summary.critical_pairs ?tenv ?subst astate.lock_state callsite + CriticalPairs.with_callsite summary.critical_pairs ~tenv ~subst astate.lock_state callsite astate.thread in { astate with critical_pairs= CriticalPairs.join astate.critical_pairs critical_pairs' ; thread= ThreadDomain.integrate_summary ~caller:astate.thread ~callee:summary.thread - ; attributes= - Option.value_map lhs ~default:astate.attributes ~f:(fun lhs_exp -> - AttributeDomain.add lhs_exp summary.return_attribute astate.attributes ) } + ; attributes= AttributeDomain.add lhs summary.return_attribute astate.attributes } let summary_of_astate : Procdesc.t -> t -> summary = @@ -912,3 +925,6 @@ let remove_dead_vars (astate : t) deadvars = let set_ignore_blocking_calls_flag astate = {astate with ignore_blocking_calls= true} + +let fold_critical_pairs_of_summary f (summary : summary) acc = + CriticalPairs.fold f summary.critical_pairs acc diff --git a/infer/src/concurrency/starvationDomain.mli b/infer/src/concurrency/starvationDomain.mli index 0280e5cea..79938c0fd 100644 --- a/infer/src/concurrency/starvationDomain.mli +++ b/infer/src/concurrency/starvationDomain.mli @@ -64,6 +64,8 @@ module Event : sig [@@deriving compare] val describe : F.formatter -> t -> unit + + val get_acquired_locks : t -> Lock.t list end module LockState : AbstractDomain.WithTop @@ -120,6 +122,10 @@ module CriticalPair : sig val can_run_in_parallel : t -> t -> bool (** can two pairs describe events on two threads that can run in parallel *) + + val with_callsite : t -> CallSite.t -> t + + val apply_caller_thread : ThreadDomain.t -> t -> t option end module CriticalPairs : AbstractDomain.FiniteSetS with type elt = CriticalPair.t @@ -178,7 +184,7 @@ include AbstractDomain.S with type t := t val initial : t (** initial domain state *) -val acquire : ?tenv:Tenv.t -> t -> procname:Procname.t -> loc:Location.t -> Lock.t list -> t +val acquire : tenv:Tenv.t -> t -> procname:Procname.t -> loc:Location.t -> Lock.t list -> t (** simultaneously acquire a number of locks, no-op if list is empty *) val release : t -> Lock.t list -> t @@ -228,9 +234,9 @@ val empty_summary : summary val pp_summary : F.formatter -> summary -> unit val integrate_summary : - ?tenv:Tenv.t - -> ?lhs:HilExp.AccessExpression.t - -> ?subst:Lock.subst + tenv:Tenv.t + -> lhs:HilExp.AccessExpression.t + -> subst:Lock.subst -> CallSite.t -> t -> summary @@ -243,3 +249,5 @@ val summary_of_astate : Procdesc.t -> t -> summary val set_ignore_blocking_calls_flag : t -> t val remove_dead_vars : t -> Var.t list -> t + +val fold_critical_pairs_of_summary : (CriticalPair.t -> 'a -> 'a) -> summary -> 'a -> 'a