From d373a81b73035bcb1740493c6abb02d485a6cdaf Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Thu, 7 May 2020 02:55:37 -0700 Subject: [PATCH] [pulse] Keep only one disjunct from blacklisted function Summary: This diff gets only one disjunct from blacklisted callee, in order to avoid OOMing in specific cases. Reviewed By: jvillard Differential Revision: D21406023 fbshipit-source-id: f9214c9c6 --- infer/man/man1/infer-analyze.txt | 5 +++++ infer/man/man1/infer-full.txt | 8 ++++++++ infer/man/man1/infer.txt | 5 +++++ infer/src/base/Config.ml | 11 +++++++++++ infer/src/base/Config.mli | 2 ++ infer/src/istd/IContainer.ml | 11 +++++++++++ infer/src/istd/IContainer.mli | 8 ++++++++ infer/src/pulse/PulseOperations.ml | 25 +++++++++++++++++++++---- 8 files changed, 71 insertions(+), 4 deletions(-) diff --git a/infer/man/man1/infer-analyze.txt b/infer/man/man1/infer-analyze.txt index 5581b443c..86e6b8036 100644 --- a/infer/man/man1/infer-analyze.txt +++ b/infer/man/man1/infer-analyze.txt @@ -232,6 +232,11 @@ OPTIONS Activates: [EXPERIMENTAL] C++ lifetime analysis (Conversely: --no-pulse) + --pulse-cut-to-one-path-procedures-pattern string + Regex of methods for which pulse will only explore one path. Can + be used on pathologically large procedures to prevent too-big + states from being produced. + --pulse-model-alloc-pattern string Regex of methods that should be modelled as allocs in Pulse diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 4358c1aa2..d06639173 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -857,6 +857,11 @@ OPTIONS Activates: [EXPERIMENTAL] C++ lifetime analysis (Conversely: --no-pulse) See also infer-analyze(1). + --pulse-cut-to-one-path-procedures-pattern string + Regex of methods for which pulse will only explore one path. Can + be used on pathologically large procedures to prevent too-big + states from being produced. See also infer-analyze(1). + --pulse-model-alloc-pattern string Regex of methods that should be modelled as allocs in Pulse See also infer-analyze(1). @@ -1599,6 +1604,9 @@ INTERNAL OPTIONS conditions. This is intended for Pulse development only and will be removed once the feature is stable. (Conversely: --no-pudge) + --pulse-cut-to-one-path-procedures-pattern-reset + Cancel the effect of --pulse-cut-to-one-path-procedures-pattern. + --pulse-intraprocedural-only Activates: Disable inter-procedural analysis in Pulse. Used for experimentations only. (Conversely: diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index 227fab4a0..99f9bffa8 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -857,6 +857,11 @@ OPTIONS Activates: [EXPERIMENTAL] C++ lifetime analysis (Conversely: --no-pulse) See also infer-analyze(1). + --pulse-cut-to-one-path-procedures-pattern string + Regex of methods for which pulse will only explore one path. Can + be used on pathologically large procedures to prevent too-big + states from being produced. See also infer-analyze(1). + --pulse-model-alloc-pattern string Regex of methods that should be modelled as allocs in Pulse See also infer-analyze(1). diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index ab0b64284..1d287445d 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -1760,6 +1760,13 @@ and pudge = development only and will be removed once the feature is stable." +and pulse_cut_to_one_path_procedures_pattern = + CLOpt.mk_string_opt ~long:"pulse-cut-to-one-path-procedures-pattern" + ~in_help:InferCommand.[(Analyze, manual_generic)] + "Regex of methods for which pulse will only explore one path. Can be used on pathologically \ + large procedures to prevent too-big states from being produced." + + and pulse_recency_limit = CLOpt.mk_int ~long:"pulse-recency-limit" ~default:32 "Maximum number of array elements and structure fields to keep track of for a given array \ @@ -2856,6 +2863,10 @@ and project_root = !project_root and pudge = !pudge +and pulse_cut_to_one_path_procedures_pattern = + Option.map ~f:Str.regexp !pulse_cut_to_one_path_procedures_pattern + + and pulse_recency_limit = !pulse_recency_limit and pulse_intraprocedural_only = !pulse_intraprocedural_only diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index dbeacb476..e8f09d945 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -445,6 +445,8 @@ val project_root : string val pudge : bool +val pulse_cut_to_one_path_procedures_pattern : Str.regexp option + val pulse_recency_limit : int val pulse_intraprocedural_only : bool diff --git a/infer/src/istd/IContainer.ml b/infer/src/istd/IContainer.ml index 18f1e8ef6..9d13b874d 100644 --- a/infer/src/istd/IContainer.ml +++ b/infer/src/istd/IContainer.ml @@ -79,3 +79,14 @@ let fold_of_pervasives_map_fold ~fold collection ~init ~f = let iter_result ~fold collection ~f = Container.fold_result ~fold ~init:() ~f:(fun () item -> f item) collection + + +let fold_result_until ~fold ~init ~f ~finish collection = + with_return (fun {return} -> + Result.map ~f:finish + (Container.fold_result ~fold collection ~init ~f:(fun acc item -> + match (f acc item : _ Continue_or_stop.t) with + | Continue x -> + x + | Stop x -> + return (Result.Ok x) )) ) diff --git a/infer/src/istd/IContainer.mli b/infer/src/istd/IContainer.mli index c044ff177..8ef107eba 100644 --- a/infer/src/istd/IContainer.mli +++ b/infer/src/istd/IContainer.mli @@ -53,3 +53,11 @@ val fold_of_pervasives_map_fold : val iter_result : fold:('t, 'a, unit) Container.fold -> 't -> f:('a -> (unit, 'err) result) -> (unit, 'err) result + +val fold_result_until : + fold:('t, 'a, 'accum) Container.fold + -> init:'accum + -> f:('accum -> 'a -> (('accum, 'err) Result.t, 'final) Continue_or_stop.t) + -> finish:('accum -> 'final) + -> 't + -> ('final, 'err) Result.t diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index d40f342ae..4ea03ff72 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -450,12 +450,29 @@ let call ~callee_data call_loc callee_pname ~ret ~actuals ~formals_opt (astate : Procdesc.get_formals callee_proc_desc |> List.map ~f:(fun (mangled, _) -> Pvar.mk mangled callee_pname |> Var.of_pvar) in + let is_blacklist = + Option.exists Config.pulse_cut_to_one_path_procedures_pattern ~f:(fun regex -> + Str.string_match regex (Procname.to_string callee_pname) 0 ) + in (* call {!AbductiveDomain.PrePost.apply} on each pre/post pair in the summary. *) - List.fold_result exec_states ~init:[] ~f:(fun posts callee_exec_state -> + IContainer.fold_result_until exec_states ~fold:List.fold ~init:[] + ~f:(fun posts callee_exec_state -> (* apply all pre/post specs *) - apply_callee callee_pname call_loc callee_exec_state ~formals ~actuals ~ret astate - >>| function - | None -> (* couldn't apply pre/post pair *) posts | Some post -> post :: posts ) + match + apply_callee callee_pname call_loc callee_exec_state ~formals ~actuals ~ret astate + with + | Ok None -> + (* couldn't apply pre/post pair *) + Continue (Ok posts) + | Ok (Some post) when is_blacklist -> + L.d_printfln "Keep only one disjunct because %a is in blacklist" Procname.pp + callee_pname ; + Stop [post] + | Ok (Some post) -> + Continue (Ok (post :: posts)) + | Error _ as x -> + Continue x ) + ~finish:(fun x -> x) | None -> (* no spec found for some reason (unknown function, ...) *) L.d_printfln "No spec found for %a@\n" Procname.pp callee_pname ;