[pulse] Suppress reports containing skipped calls

Summary: Adding option to suppress errors involving unknown code. If `--pulse-report-ignore-unknown-java-methods-patterns` is provided, reports containing skipped functions not matching at least one of the given regexps are suppressed.

Reviewed By: jvillard

Differential Revision: D26820575

fbshipit-source-id: b6e1df7b2

infer/man/man1/infer-analyze.txt

@@ -295,6 +295,14 @@ OPTIONS
            Activates: Enable pulse and disable all other checkers
            (Conversely: --no-pulse-only)
 
+       --pulse-report-ignore-unknown-java-methods-patterns +string
+           On Java, issues that are found on program paths that contain calls
+           to unknown methods (those without implementation) are not reported
+           unless all the unknown method names match this pattern. If the
+           empty list is provided or
+           --pulse_report_ignore_unknown_java_methods_patterns-reset, all
+           issues will be reported regardless the presence of unknown code
+
        --purity
            Activates: checker purity: Detects pure (side-effect-free)
            functions. A different implementation of "impurity". (Conversely:

infer/man/man1/infer-full.txt

@@ -1009,6 +1009,15 @@ OPTIONS
            Activates: Enable pulse and disable all other checkers
            (Conversely: --no-pulse-only)           See also infer-analyze(1).
 
+       --pulse-report-ignore-unknown-java-methods-patterns +string
+           On Java, issues that are found on program paths that contain calls
+           to unknown methods (those without implementation) are not reported
+           unless all the unknown method names match this pattern. If the
+           empty list is provided or
+           --pulse_report_ignore_unknown_java_methods_patterns-reset, all
+           issues will be reported regardless the presence of unknown code       
+    See also infer-analyze(1).
+
        --purity
            Activates: checker purity: Detects pure (side-effect-free)
            functions. A different implementation of "impurity". (Conversely:
@@ -1893,6 +1902,10 @@ INTERNAL OPTIONS
            Maximum number of array elements and structure fields to keep
            track of for a given array address.
 
+       --pulse-report-ignore-unknown-java-methods-patterns-reset
+           Set --pulse-report-ignore-unknown-java-methods-patterns to the
+           empty list.
+
        --pulse-report-latent-issues
            Activates: Only use for testing, there should be no need to turn
            this on for regular code analysis. Report latent issues instead of

infer/man/man1/infer.txt

@@ -1009,6 +1009,15 @@ OPTIONS
            Activates: Enable pulse and disable all other checkers
            (Conversely: --no-pulse-only)           See also infer-analyze(1).
 
+       --pulse-report-ignore-unknown-java-methods-patterns +string
+           On Java, issues that are found on program paths that contain calls
+           to unknown methods (those without implementation) are not reported
+           unless all the unknown method names match this pattern. If the
+           empty list is provided or
+           --pulse_report_ignore_unknown_java_methods_patterns-reset, all
+           issues will be reported regardless the presence of unknown code       
+    See also infer-analyze(1).
+
        --purity
            Activates: checker purity: Detects pure (side-effect-free)
            functions. A different implementation of "impurity". (Conversely:

infer/src/base/Config.ml

@@ -1955,6 +1955,17 @@ and pulse_model_skip_pattern =
     "Regex of methods that should be modelled as \"skip\" in Pulse"
 
 
+and pulse_report_ignore_unknown_java_methods_patterns =
+  CLOpt.mk_string_list ~default:[".*<init>.*"]
+    ~long:"pulse-report-ignore-unknown-java-methods-patterns"
+    ~in_help:InferCommand.[(Analyze, manual_generic)]
+    "On Java, issues that are found on program paths that contain calls to unknown methods (those \
+     without implementation) are not reported unless all the unknown method names match this \
+     pattern. If the empty list is provided or \
+     --pulse_report_ignore_unknown_java_methods_patterns-reset, all issues will be reported \
+     regardless the presence of unknown code"
+
+
 and pulse_model_transfer_ownership =
   CLOpt.mk_string_list ~long:"pulse-model-transfer-ownership"
     ~in_help:InferCommand.[(Analyze, manual_generic)]
@@ -3201,6 +3212,14 @@ and pulse_model_return_nonnull = Option.map ~f:Str.regexp !pulse_model_return_no
 
 and pulse_model_skip_pattern = Option.map ~f:Str.regexp !pulse_model_skip_pattern
 
+and pulse_report_ignore_unknown_java_methods_patterns =
+  match RevList.to_list !pulse_report_ignore_unknown_java_methods_patterns with
+  | [] ->
+      None
+  | patts ->
+      Some (Str.regexp (String.concat ~sep:"\\|" patts))
+
+
 and pulse_model_transfer_ownership_namespace, pulse_model_transfer_ownership =
   let models =
     let re = Str.regexp "::" in

infer/src/base/Config.mli

@@ -497,6 +497,8 @@ val pulse_model_return_nonnull : Str.regexp option
 
 val pulse_model_skip_pattern : Str.regexp option
 
+val pulse_report_ignore_unknown_java_methods_patterns : Str.regexp option
+
 val pulse_model_transfer_ownership_namespace : (string * string) list
 
 val pulse_model_transfer_ownership : string list

infer/src/pulse/PulseAbductiveDomain.ml

@@ -582,6 +582,16 @@ let add_skipped_calls new_skipped_calls astate =
   if phys_equal skipped_calls astate.skipped_calls then astate else {astate with skipped_calls}
 
 
+let skipped_calls_match_pattern astate =
+  (* For every skipped function, there needs to be at least one regexp given in --pulse_report_ignore_java_methods_patterns
+     that matches it *)
+  Option.value_map Config.pulse_report_ignore_unknown_java_methods_patterns ~default:true
+    ~f:(fun patt ->
+      SkippedCalls.for_all
+        (fun skipped_proc _ -> Str.string_match patt (Procname.to_string skipped_proc) 0)
+        astate.skipped_calls )
+
+
 let discard_unreachable ({pre; post} as astate) =
   let pre_addresses = BaseDomain.reachable_addresses (pre :> BaseDomain.t) in
   let pre_new =

infer/src/pulse/PulseAbductiveDomain.mli

@@ -184,6 +184,8 @@ val set_path_condition : PathCondition.t -> t -> t
 (** private type to make sure {!summary_of_post} is always called when creating summaries *)
 type summary = private t [@@deriving compare, equal, yojson_of]
 
+val skipped_calls_match_pattern : summary -> bool
+
 val summary_of_post : Tenv.t -> Procdesc.t -> t -> summary SatUnsat.t
 (** trim the state down to just the procedure's interface (formals and globals), and simplify and
     normalize the state *)

infer/src/pulse/PulseReport.ml

@@ -30,13 +30,17 @@ let report_latent_issue proc_desc err_log latent_issue =
   report ~extra_trace proc_desc err_log diagnostic
 
 
-let is_suppressed tenv proc_desc diagnostic =
-  match Procdesc.get_proc_name proc_desc with
-  | Procname.Java jn
-    when (not Config.pulse_nullsafe_report_npe)
+let is_nullsafe_error tenv diagnostic jn =
+  (not Config.pulse_nullsafe_report_npe)
   && IssueType.equal (Diagnostic.get_issue_type diagnostic) IssueType.nullptr_dereference
-    -> (
-    match NullsafeMode.of_java_procname tenv jn with Default -> false | Local _ | Strict -> true )
+  && match NullsafeMode.of_java_procname tenv jn with Default -> false | Local _ | Strict -> true
+
+
+let is_suppressed tenv proc_desc diagnostic astate =
+  match Procdesc.get_proc_name proc_desc with
+  | Procname.Java jn ->
+      is_nullsafe_error tenv diagnostic jn
+      || not (AbductiveDomain.skipped_calls_match_pattern astate)
   | _ ->
       false
 
@@ -44,7 +48,8 @@ let is_suppressed tenv proc_desc diagnostic =
 let report_error tenv proc_desc err_log access_error =
   match LatentIssue.should_report access_error with
   | `ReportNow (astate_summary, diagnostic) ->
-      if not (is_suppressed tenv proc_desc diagnostic) then report proc_desc err_log diagnostic ;
+      if not (is_suppressed tenv proc_desc diagnostic astate_summary) then
+        report proc_desc err_log diagnostic ;
       AbortProgram astate_summary
   | `DelayReport (astate, latent_issue) ->
       if Config.pulse_report_latent_issues then report_latent_issue proc_desc err_log latent_issue ;

infer/tests/codetoanalyze/java/pulse/Makefile

@@ -4,8 +4,7 @@
 # LICENSE file in the root directory of this source tree.
 
 TESTS_DIR = ../../..
-
-INFER_OPTIONS = --pulse-only --debug-exceptions --no-pulse-nullsafe-report-npe --pulse-report-latent-issues
+INFER_OPTIONS = --pulse-only --debug-exceptions --no-pulse-nullsafe-report-npe --pulse-report-latent-issues --pulse-report-ignore-unknown-java-methods-patterns-reset
 INFERPRINT_OPTIONS = --issues-tests
 SOURCES = $(wildcard *.java)