[pulse] Suppress Pulse NPE reports on @Nullsafe

Summary: Allowing Pulse NPE reports on Nullsafe classes to be suppressed. This is now possible via the optional argument --pulse-nullsafe-report-npe (default: true).

Reviewed By: da319

Differential Revision: D25997321

fbshipit-source-id: 98465df79

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.

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

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

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 =

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
 

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

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

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

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

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

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)
 

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();
+  }
+}

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.<init>()` here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,passed as argument to `OtherClass.<init>()`,assigned,return from call to `OtherClass.<init>()`,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.<init>(), 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]