diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index f91ca7b00..db59ec2d5 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -1805,6 +1805,10 @@ INTERNAL OPTIONS --pulse-model-transfer-ownership-reset Set --pulse-model-transfer-ownership to the empty list. + --no-pulse-nullsafe-report-npe + Deactivates: [Pulse] Suppress NPE reports on files marked + @Nullsafe. (Conversely: --pulse-nullsafe-report-npe) + --pulse-recency-limit int Maximum number of array elements and structure fields to keep track of for a given array address. diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 79dc47625..1c6d93046 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -1947,6 +1947,11 @@ and pulse_widen_threshold = "Under-approximate after $(i,int) loop iterations" +and pulse_nullsafe_report_npe = + CLOpt.mk_bool ~long:"pulse-nullsafe-report-npe" ~default:true + "[Pulse] Suppress NPE reports on files marked @Nullsafe." + + and pure_by_default = CLOpt.mk_bool ~long:"pure-by-default" ~default:false "[Purity]Consider unknown functions to be pure by default" @@ -3164,6 +3169,8 @@ and pulse_report_latent_issues = !pulse_report_latent_issues and pulse_widen_threshold = !pulse_widen_threshold +and pulse_nullsafe_report_npe = !pulse_nullsafe_report_npe + and pure_by_default = !pure_by_default and quandary_endpoints = !quandary_endpoints diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 4484febd6..0e5024184 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -491,6 +491,8 @@ val pulse_recency_limit : int val pulse_widen_threshold : int +val pulse_nullsafe_report_npe : bool + val pure_by_default : bool val quandary_endpoints : Yojson.Basic.t diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml index 2864e6c82..1b42d31e7 100644 --- a/infer/src/pulse/Pulse.ml +++ b/infer/src/pulse/Pulse.ml @@ -22,14 +22,14 @@ let exec_list_of_list_result = function [post] -let report_on_error {InterproceduralAnalysis.proc_desc; err_log} result = - PulseReport.report_error proc_desc err_log result +let report_on_error {InterproceduralAnalysis.proc_desc; tenv; err_log} result = + PulseReport.report_error proc_desc tenv err_log result >>| List.map ~f:(fun post -> ExecutionDomain.ContinueProgram post) |> exec_list_of_list_result -let report_on_error_list {InterproceduralAnalysis.proc_desc; err_log} result = - PulseReport.report_error proc_desc err_log result |> exec_list_of_list_result +let report_on_error_list {InterproceduralAnalysis.proc_desc; tenv; err_log} result = + PulseReport.report_error proc_desc tenv err_log result |> exec_list_of_list_result let report_topl_errors proc_desc err_log summary = @@ -60,14 +60,14 @@ module PulseTransferFunctions = struct AnalysisCallbacks.proc_resolve_attributes pname |> Option.map ~f:ProcAttributes.get_pvar_formals - let interprocedural_call {InterproceduralAnalysis.analyze_dependency; proc_desc; err_log} ret - callee_pname call_exp actuals call_loc astate = + let interprocedural_call {InterproceduralAnalysis.analyze_dependency; proc_desc; tenv; err_log} + ret callee_pname call_exp actuals call_loc astate = match callee_pname with | Some callee_pname when not Config.pulse_intraprocedural_only -> let formals_opt = get_pvar_formals callee_pname in let callee_data = analyze_dependency callee_pname in - PulseOperations.call ~caller_proc_desc:proc_desc err_log ~callee_data call_loc callee_pname - ~ret ~actuals ~formals_opt astate + PulseOperations.call ~caller_proc_desc:proc_desc tenv err_log ~callee_data call_loc + callee_pname ~ret ~actuals ~formals_opt astate | _ -> L.d_printfln "Skipping indirect call %a@\n" Exp.pp call_exp ; let astate = diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index cfcc1c92d..46b816a86 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -217,7 +217,7 @@ module ObjC = struct let dispatch_sync args : model = - fun {analyze_dependency; proc_desc; err_log} ~callee_procname:_ location ~ret astate -> + fun {analyze_dependency; proc_desc; tenv; err_log} ~callee_procname:_ location ~ret astate -> match List.last args with | None -> Ok [ExecutionDomain.ContinueProgram astate] @@ -229,7 +229,7 @@ module ObjC = struct | None -> Ok [ExecutionDomain.ContinueProgram astate] | Some callee_proc_name -> - PulseOperations.call ~caller_proc_desc:proc_desc err_log + PulseOperations.call ~caller_proc_desc:proc_desc tenv err_log ~callee_data:(analyze_dependency callee_proc_name) location callee_proc_name ~ret ~actuals:[] ~formals_opt:None astate ) end @@ -555,7 +555,7 @@ end module StdFunction = struct let operator_call ProcnameDispatcher.Call.FuncArg.{arg_payload= lambda_ptr_hist; typ} actuals : model = - fun {analyze_dependency; proc_desc; err_log} ~callee_procname:_ location ~ret astate -> + fun {analyze_dependency; proc_desc; tenv; err_log} ~callee_procname:_ location ~ret astate -> let havoc_ret (ret_id, _) astate = let event = ValueHistory.Call {f= Model "std::function::operator()"; location; in_call= []} in [PulseOperations.havoc_id ret_id [event] astate] @@ -576,7 +576,7 @@ module StdFunction = struct :: List.map actuals ~f:(fun ProcnameDispatcher.Call.FuncArg.{arg_payload; typ} -> (arg_payload, typ) ) in - PulseOperations.call ~caller_proc_desc:proc_desc err_log + PulseOperations.call ~caller_proc_desc:proc_desc tenv err_log ~callee_data:(analyze_dependency callee_proc_name) location callee_proc_name ~ret ~actuals ~formals_opt:None astate diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml index c24f1516d..f6805e59c 100644 --- a/infer/src/pulse/PulseOperations.ml +++ b/infer/src/pulse/PulseOperations.ml @@ -665,8 +665,8 @@ let conservatively_initialize_args arg_values ({AbductiveDomain.post} as astate) AbstractValue.Set.fold AbductiveDomain.initialize reachable_values astate -let call ~caller_proc_desc err_log ~(callee_data : (Procdesc.t * PulseSummary.t) option) call_loc - callee_pname ~ret ~actuals ~formals_opt (astate : AbductiveDomain.t) = +let call ~caller_proc_desc tenv err_log ~(callee_data : (Procdesc.t * PulseSummary.t) option) + call_loc callee_pname ~ret ~actuals ~formals_opt (astate : AbductiveDomain.t) = let get_arg_values () = List.map actuals ~f:(fun ((value, _), _) -> value) in match callee_data with | Some (callee_proc_desc, exec_states) -> @@ -719,7 +719,7 @@ let call ~caller_proc_desc err_log ~(callee_data : (Procdesc.t * PulseSummary.t) (* couldn't apply pre/post pair *) posts | Sat post -> ( - match PulseReport.report_error caller_proc_desc err_log post with + match PulseReport.report_error caller_proc_desc tenv err_log post with | Error Unsat -> posts | Error (Sat post) | Ok post -> diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli index f07ee12a5..605dcbf14 100644 --- a/infer/src/pulse/PulseOperations.mli +++ b/infer/src/pulse/PulseOperations.mli @@ -159,6 +159,7 @@ val check_address_escape : val call : caller_proc_desc:Procdesc.t + -> Tenv.t -> Errlog.t -> callee_data:(Procdesc.t * PulseSummary.t) option -> Location.t diff --git a/infer/src/pulse/PulseReport.ml b/infer/src/pulse/PulseReport.ml index 41110b5be..8c94a189b 100644 --- a/infer/src/pulse/PulseReport.ml +++ b/infer/src/pulse/PulseReport.ml @@ -31,15 +31,27 @@ let report_latent_issue proc_desc err_log latent_issue = report ~extra_trace proc_desc err_log diagnostic -let report_error proc_desc err_log access_result = +let suppress_error proc_desc tenv diagnostic = + 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 ) + | _ -> + false + + +let report_error proc_desc tenv err_log access_result = let open SatUnsat.Import in Result.map_error access_result ~f:(fun (diagnostic, astate) -> let+ astate_summary = AbductiveDomain.summary_of_post proc_desc astate in + let is_suppressed = suppress_error proc_desc tenv diagnostic in match LatentIssue.should_report_diagnostic astate_summary diagnostic with | `ReportNow -> - report proc_desc err_log diagnostic ; + if not is_suppressed then report proc_desc err_log diagnostic ; ExecutionDomain.AbortProgram astate_summary | `DelayReport latent_issue -> - if Config.pulse_report_latent_issues then + if Config.pulse_report_latent_issues && not is_suppressed then report_latent_issue proc_desc err_log latent_issue ; ExecutionDomain.LatentAbortProgram {astate= astate_summary; latent_issue} ) diff --git a/infer/src/pulse/PulseReport.mli b/infer/src/pulse/PulseReport.mli index 5bbe21d2b..bc8dc94cc 100644 --- a/infer/src/pulse/PulseReport.mli +++ b/infer/src/pulse/PulseReport.mli @@ -12,4 +12,8 @@ open PulseDomainInterface type 'a access_result = ('a, Diagnostic.t * AbductiveDomain.t) result val report_error : - Procdesc.t -> Errlog.t -> 'ok access_result -> ('ok, _ ExecutionDomain.base_t SatUnsat.t) result + Procdesc.t + -> Tenv.t + -> Errlog.t + -> 'ok access_result + -> ('ok, _ ExecutionDomain.base_t SatUnsat.t) result diff --git a/infer/src/pulse/dune b/infer/src/pulse/dune index 4a93d2976..3f3af65fe 100644 --- a/infer/src/pulse/dune +++ b/infer/src/pulse/dune @@ -8,7 +8,7 @@ (public_name infer.Pulselib) (flags (:standard -open Core -open IR -open IStdlib -open IStd -open ATDGenerated - -open IBase -open Absint -open BO -open TOPLlib)) - (libraries core IStdlib ATDGenerated IBase IR Absint BO TOPLlib) + -open IBase -open Absint -open BO -open TOPLlib -open Nullsafe)) + (libraries core IStdlib ATDGenerated IBase IR Absint BO TOPLlib Nullsafe) (preprocess (pps ppx_yojson_conv ppx_compare ppx_variants_conv))) diff --git a/infer/tests/codetoanalyze/java/pulse/Makefile b/infer/tests/codetoanalyze/java/pulse/Makefile index e146b8265..28408ee27 100644 --- a/infer/tests/codetoanalyze/java/pulse/Makefile +++ b/infer/tests/codetoanalyze/java/pulse/Makefile @@ -5,7 +5,7 @@ TESTS_DIR = ../../.. -INFER_OPTIONS = --pulse-only --debug-exceptions --pulse-report-latent-issues +INFER_OPTIONS = --pulse-only --debug-exceptions --no-pulse-nullsafe-report-npe --pulse-report-latent-issues INFERPRINT_OPTIONS = --issues-tests SOURCES = $(wildcard *.java) diff --git a/infer/tests/codetoanalyze/java/pulse/NullSafeExample.java b/infer/tests/codetoanalyze/java/pulse/NullSafeExample.java new file mode 100644 index 000000000..54ab8bb8a --- /dev/null +++ b/infer/tests/codetoanalyze/java/pulse/NullSafeExample.java @@ -0,0 +1,44 @@ +/* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ +import com.facebook.infer.annotation.Nullsafe; + +class OtherClass { + + OtherClass x = null; + + OtherClass canReturnNull() { + return this.x; + } + + String buggyMethodBad() { + OtherClass o = new OtherClass(); + return o.canReturnNull().toString(); + } +} + +/* + * Pulse will not report NPEs on @Nullsafe classes if flag + * --pulse-nullsafe-report-npe is set to false + */ + +@Nullsafe(Nullsafe.Mode.LOCAL) +class NullsafeExampleLocal { + void testingNullsafeLocalMode() { + OtherClass o = new OtherClass(); + o = o.canReturnNull(); + o.getClass(); + } +} + +@Nullsafe(Nullsafe.Mode.STRICT) +class NullsafeExampleStrict { + void testingNullsafeStrictMode() { + OtherClass o = new OtherClass(); + o = o.canReturnNull(); + o.toString(); + } +} diff --git a/infer/tests/codetoanalyze/java/pulse/issues.exp b/infer/tests/codetoanalyze/java/pulse/issues.exp index 92c012143..3769df8d0 100644 --- a/infer/tests/codetoanalyze/java/pulse/issues.exp +++ b/infer/tests/codetoanalyze/java/pulse/issues.exp @@ -53,6 +53,7 @@ codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.Nu codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.someNPEAfterResourceLeak():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `T CloseableAsResourceExample.sourceOfNullWithResourceLeak()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `T CloseableAsResourceExample.sourceOfNullWithResourceLeak()`,return from call to `T CloseableAsResourceExample.sourceOfNullWithResourceLeak()`,assigned,invalid access occurs here] codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.stringConstantEqualsFalseNotNPE_FP():void, 10, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/java/pulse/NullPointerExceptions.java, codetoanalyze.java.infer.NullPointerExceptions.stringVarEqualsFalseNPE():void, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] +codetoanalyze/java/pulse/NullSafeExample.java, OtherClass.buggyMethodBad():java.lang.String, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,when calling `OtherClass.()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `OtherClass.()`,assigned,return from call to `OtherClass.()`,passed as argument to `OtherClass OtherClass.canReturnNull()`,return from call to `OtherClass OtherClass.canReturnNull()`,assigned,invalid access occurs here] codetoanalyze/java/pulse/SuppressLintExample.java, codetoanalyze.java.infer.SuppressAllWarnigsInTheClass.shouldNotReportNPE():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/java/pulse/SuppressLintExample.java, codetoanalyze.java.infer.SuppressLintExample.(), 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/java/pulse/SuppressLintExample.java, codetoanalyze.java.infer.SuppressLintExample.FP_shouldNotReportNPE():void, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here]