diff --git a/infer/src/backend/InferAnalyze.re b/infer/src/backend/InferAnalyze.re index 2f8a8e2db..8ebbc554a 100644 --- a/infer/src/backend/InferAnalyze.re +++ b/infer/src/backend/InferAnalyze.re @@ -150,36 +150,30 @@ let main makefile => { (List.length clusters_to_analyze) (List.length all_clusters) Config.results_dir; - if (makefile != "" || Config.per_procedure_parallelism) { - let is_java () => - List.exists - f::( - fun cl => SourceFile.string_crc_has_extension ext::"java" (DB.source_dir_to_string cl) - ) - all_clusters; - if (not Config.per_procedure_parallelism) { - ClusterMakefile.create_cluster_makefile clusters_to_analyze makefile - } else { - /* per-procedure parallelism */ - if (is_java ()) { - /* Java uses ZipLib which is incompatible with forking */ - L.stderr "Error: option --per-procedure-parallelism not supported with Java@."; - exit 1 - }; - L.stdout "per-procedure parallelism jobs:%d@." Config.jobs; - if (makefile != "") { - ClusterMakefile.create_cluster_makefile [] makefile - }; - /* Prepare tasks one cluster at a time while executing in parallel */ - let runner = Tasks.Runner.create jobs::Config.jobs; - let cluster_start_tasks i cluster => { - let tasks = analyze_cluster_tasks i cluster; - let aggregate_tasks = Tasks.aggregate size::1 tasks; - Tasks.Runner.start runner tasks::aggregate_tasks - }; - List.iteri f::cluster_start_tasks clusters_to_analyze; - Tasks.Runner.complete runner - } + let is_java () => + List.exists + f::(fun cl => SourceFile.string_crc_has_extension ext::"java" (DB.source_dir_to_string cl)) + all_clusters; + if (Config.per_procedure_parallelism && not (is_java ())) { + /* Java uses ZipLib which is incompatible with forking */ + /* per-procedure parallelism */ + L.stdout "per-procedure parallelism jobs:%d@." Config.jobs; + if (makefile != "") { + ClusterMakefile.create_cluster_makefile [] makefile + }; + /* Prepare tasks one cluster at a time while executing in parallel */ + let runner = Tasks.Runner.create jobs::Config.jobs; + let cluster_start_tasks i cluster => { + let tasks = analyze_cluster_tasks i cluster; + let aggregate_tasks = Tasks.aggregate size::Config.procedures_per_process tasks; + Tasks.Runner.start runner tasks::aggregate_tasks + }; + List.iteri f::cluster_start_tasks clusters_to_analyze; + Tasks.Runner.complete runner + } else if ( + makefile != "" + ) { + ClusterMakefile.create_cluster_makefile clusters_to_analyze makefile } else { /* This branch is reached when -j 1 is used */ List.iteri f::analyze_cluster clusters_to_analyze; diff --git a/infer/src/backend/Tasks.ml b/infer/src/backend/Tasks.ml index 876fbb431..e32f854d4 100644 --- a/infer/src/backend/Tasks.ml +++ b/infer/src/backend/Tasks.ml @@ -35,9 +35,10 @@ let empty = { closures = []; continuations = Queue.create () } let aggregate ~size t = let group_to_closure group = fun () -> List.iter ~f:(fun closure -> closure ()) group in - if size > 1 + let group_size = if size > 0 then size else (List.length t.closures) / Config.jobs in + if group_size > 1 then - let groups = List.groupi ~break:(fun n _ _ -> Int.equal (n mod size) 0) t.closures in + let groups = List.groupi ~break:(fun n _ _ -> Int.equal (n mod group_size) 0) t.closures in let closures = List.map ~f:group_to_closure groups in { t with closures } else diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 5d7d12106..15ebf6d80 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -1105,7 +1105,7 @@ and patterns_skip_translation = "Matcher or list of matchers for names of files that should not be analyzed at all.") and per_procedure_parallelism = - CLOpt.mk_bool ~deprecated:["per-procedure-parallelism"] ~long:"per-procedure-parallelism" + CLOpt.mk_bool ~long:"per-procedure-parallelism" ~default:true "Perform analysis with per-procedure parallelism.\n\ Java is not supported." @@ -1130,6 +1130,12 @@ and print_using_diff = CLOpt.mk_bool ~deprecated_no:["noprintdiff"] ~long:"print-using-diff" ~default:true "Highlight the difference w.r.t. the previous prop when printing symbolic execution debug info" +and procedures_per_process = + CLOpt.mk_int ~long:"procedures-per-process" ~default:1000 ~meta:"int" + "Specify the number of procedures to analyze per process when using \ + --per-procedure-parallelism. If 0 is specified, each file is divided into --jobs groups of \ + procedures." + and procs_csv = CLOpt.mk_path_opt ~deprecated:["procs"] ~long:"procs-csv" ~meta:"file" "Write statistics for each procedure in CSV format to a file" @@ -1672,6 +1678,7 @@ and print_logs = !print_logs and print_builtins = !print_builtins and print_types = !print_types and print_using_diff = !print_using_diff +and procedures_per_process = !procedures_per_process and procs_csv = !procs_csv and procs_xml = !procs_xml and quandary = !quandary diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index f95ff7877..0493434ca 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -287,6 +287,7 @@ val print_logs : bool val print_builtins : bool val print_types : bool val print_using_diff : bool +val procedures_per_process : int val procs_csv : string option val procs_xml : string option val project_root : string