[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

@@ -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
 

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:

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).

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

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

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) )) )

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

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 ;