From 2d56b1bff177dc03e6f2c13488b6a33a606da75e Mon Sep 17 00:00:00 2001 From: Gabriela Cunha Sampaio Date: Wed, 10 Mar 2021 06:37:36 -0800 Subject: [PATCH] [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 | 8 ++++++++ infer/man/man1/infer-full.txt | 13 +++++++++++++ infer/man/man1/infer.txt | 9 +++++++++ infer/src/base/Config.ml | 19 +++++++++++++++++++ infer/src/base/Config.mli | 2 ++ infer/src/pulse/PulseAbductiveDomain.ml | 10 ++++++++++ infer/src/pulse/PulseAbductiveDomain.mli | 2 ++ infer/src/pulse/PulseReport.ml | 19 ++++++++++++------- infer/tests/codetoanalyze/java/pulse/Makefile | 3 +-- 9 files changed, 76 insertions(+), 9 deletions(-) diff --git a/infer/man/man1/infer-analyze.txt b/infer/man/man1/infer-analyze.txt index 8a62b6369..ca8322bb3 100644 --- a/infer/man/man1/infer-analyze.txt +++ b/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: diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index ceb0fc146..f258762e9 100644 --- a/infer/man/man1/infer-full.txt +++ b/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 diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index a7078bba6..4158a8ebd 100644 --- a/infer/man/man1/infer.txt +++ b/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: diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 4abde74f3..16a27c318 100644 --- a/infer/src/base/Config.ml +++ b/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:[".*.*"] + ~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 diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 3701c402f..54761209f 100644 --- a/infer/src/base/Config.mli +++ b/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 diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 394cb4cc2..6a37f9313 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/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 = diff --git a/infer/src/pulse/PulseAbductiveDomain.mli b/infer/src/pulse/PulseAbductiveDomain.mli index 5a6959691..ecc816101 100644 --- a/infer/src/pulse/PulseAbductiveDomain.mli +++ b/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 *) diff --git a/infer/src/pulse/PulseReport.ml b/infer/src/pulse/PulseReport.ml index b7f901914..60d2997f9 100644 --- a/infer/src/pulse/PulseReport.ml +++ b/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 = +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 + + +let is_suppressed tenv proc_desc diagnostic astate = match Procdesc.get_proc_name proc_desc with - | Procname.Java jn - when (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 ) + | 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 ; diff --git a/infer/tests/codetoanalyze/java/pulse/Makefile b/infer/tests/codetoanalyze/java/pulse/Makefile index 28408ee27..4ddbdbae2 100644 --- a/infer/tests/codetoanalyze/java/pulse/Makefile +++ b/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)