diff --git a/infer/src/backend/StarvationGlobalAnalysis.ml b/infer/src/backend/StarvationGlobalAnalysis.ml new file mode 100644 index 000000000..2ff0514e5 --- /dev/null +++ b/infer/src/backend/StarvationGlobalAnalysis.ml @@ -0,0 +1,90 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +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.bottom with thread= work_item.thread} 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 + + +(* 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) -> + let pname = Summary.get_proc_name summary in + let tenv = Exe_env.get_tenv exe_env pname in + if ConcurrencyModels.is_modeled_ui_method tenv pname then f pname critical_pairs ; + ScheduledWorkDomain.iter + (fun work -> get_summary_of_scheduled_work work |> Option.iter ~f:(f pname)) + scheduled_work ) + + +module WorkHashSet = struct + module T = struct + type t = Procname.t * Domain.CriticalPair.t + + (* [compare] for critical pairs ignore various fields, so using a generated equality here would + break the polymorphic hash function. We use [phys_equal] instead and rely on the clients to + not add duplicate items. *) + let equal = phys_equal + + let hash = Hashtbl.hash + end + + 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 +end + +let report exe_env work_set = + let open Domain in + let wrap_report (procname, (pair : CriticalPair.t)) () init = + Summary.OnDisk.get procname + |> Option.fold ~init ~f:(fun acc summary -> + let pdesc = Summary.get_proc_desc summary in + let tenv = Exe_env.get_tenv exe_env procname in + let acc = Starvation.report_on_pair tenv summary pair acc in + match pair.elem.event with + | LockAcquire 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 pdesc + pair lock other_procname other_pair acc ) + work_set acc + | _ -> + acc ) + in + WorkHashSet.fold wrap_report work_set Starvation.ReportMap.empty + |> Starvation.ReportMap.store_multi_file + + +let whole_program_analysis () = + L.progress "Starvation whole program analysis starts.@." ; + let work_set = WorkHashSet.create 1 in + let exe_env = Exe_env.mk () in + L.progress "Processing on-disk summaries...@." ; + SpecsFiles.iter ~f:(iter_summary exe_env ~f:(WorkHashSet.add_pairs 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/backend/StarvationGlobalAnalysis.mli b/infer/src/backend/StarvationGlobalAnalysis.mli new file mode 100644 index 000000000..7479e411c --- /dev/null +++ b/infer/src/backend/StarvationGlobalAnalysis.mli @@ -0,0 +1,10 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd + +val whole_program_analysis : unit -> unit diff --git a/infer/src/concurrency/starvation.ml b/infer/src/concurrency/starvation.ml index dcb355c28..3ba7c04ae 100644 --- a/infer/src/concurrency/starvation.ml +++ b/infer/src/concurrency/starvation.ml @@ -741,82 +741,3 @@ let reporting {Callbacks.procedures; exe_env} = else report_map ) in List.fold procedures ~init:ReportMap.empty ~f:report_procedure |> ReportMap.issue_log_of - - -(* 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.bottom with thread= work_item.thread} in - let callsite = CallSite.make work_item.procname work_item.loc in - Summary.OnDisk.get work_item.procname - |> Option.bind ~f:(fun (summary : Summary.t) -> Payloads.starvation summary.payloads) - |> Option.map ~f:(Domain.integrate_summary callsite astate) - |> Option.map ~f:(fun (astate : Domain.t) -> astate.critical_pairs) - - -(* 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) -> - let pname = Summary.get_proc_name summary in - let tenv = Exe_env.get_tenv exe_env pname in - if ConcurrencyModels.is_modeled_ui_method tenv pname then f pname critical_pairs ; - ScheduledWorkDomain.iter - (fun work -> get_summary_of_scheduled_work work |> Option.iter ~f:(f pname)) - scheduled_work ) - - -module WorkHashSet = struct - module T = struct - type t = Procname.t * Domain.CriticalPair.t - - (* [compare] for critical pairs ignore various fields, so using a generated equality here would - break the polymorphic hash function. We use [phys_equal] instead and rely on the clients to - not add duplicate items. *) - let equal = phys_equal - - let hash = Hashtbl.hash - end - - 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 -end - -let report exe_env work_set = - let open Domain in - let wrap_report (procname, (pair : CriticalPair.t)) () init = - Summary.OnDisk.get procname - |> Option.fold ~init ~f:(fun acc summary -> - let pdesc = Summary.get_proc_desc summary in - let tenv = Exe_env.get_tenv exe_env procname in - let acc = report_on_pair tenv summary pair acc in - match pair.elem.event with - | LockAcquire 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 -> - report_on_parallel_composition ~should_report_starvation tenv pdesc pair lock - other_procname other_pair acc ) - work_set acc - | _ -> - acc ) - in - WorkHashSet.fold wrap_report work_set ReportMap.empty |> ReportMap.store_multi_file - - -let whole_program_analysis () = - L.progress "Starvation whole program analysis starts.@." ; - let work_set = WorkHashSet.create 1 in - let exe_env = Exe_env.mk () in - L.progress "Processing on-disk summaries...@." ; - SpecsFiles.iter ~f:(iter_summary exe_env ~f:(WorkHashSet.add_pairs 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.mli b/infer/src/concurrency/starvation.mli index 67b92d8e4..297553791 100644 --- a/infer/src/concurrency/starvation.mli +++ b/infer/src/concurrency/starvation.mli @@ -11,4 +11,26 @@ val analyze_procedure : Callbacks.proc_callback_t val reporting : Callbacks.file_callback_t -val whole_program_analysis : unit -> unit +module ReportMap : sig + type t + + val empty : t + + val store_multi_file : t -> unit + (** generate and store issue logs for all source files involved in this report map; for use in the + whole-program mode only *) +end + +val report_on_pair : + Tenv.t -> Summary.t -> StarvationDomain.CriticalPair.t -> ReportMap.t -> ReportMap.t + +val report_on_parallel_composition : + should_report_starvation:bool + -> Tenv.t + -> Procdesc.t + -> StarvationDomain.CriticalPair.t + -> StarvationDomain.Lock.t + -> Procname.t + -> StarvationDomain.CriticalPair.t + -> ReportMap.t + -> ReportMap.t diff --git a/infer/src/integration/Driver.ml b/infer/src/integration/Driver.ml index df6be9ae2..6ca0eda5b 100644 --- a/infer/src/integration/Driver.ml +++ b/infer/src/integration/Driver.ml @@ -294,7 +294,7 @@ let analyze_and_report ?suppress_console_report ~changed_files mode = if SourceFiles.is_empty () && Config.capture then error_nothing_to_analyze mode else ( execute_analyze ~changed_files ; - if Config.starvation_whole_program then Starvation.whole_program_analysis () ) ; + if Config.starvation_whole_program then StarvationGlobalAnalysis.whole_program_analysis () ) ; if should_report && Config.report then report ?suppress_console:suppress_console_report ()