[nullsafe] Decouple nullsafe mode from issue calculation, DereferenceRule

Summary:
This diff continues work in D20491716.
This time for Dereference Rule.

Reviewed By: jvillard

Differential Revision: D20492296

fbshipit-source-id: ff7f824f9

infer/src/nullsafe/DereferenceRule.ml

@@ -6,109 +6,118 @@
  *)
 open! IStd
 
-type violation = {nullsafe_mode: NullsafeMode.t; nullability: Nullability.t} [@@deriving compare]
+type violation = {nullability: Nullability.t} [@@deriving compare]
 
-type dereference_type =
-  | MethodCall of Procname.t
-  | AccessToField of Fieldname.t
-  | AccessByIndex of {index_desc: string}
-  | ArrayLengthAccess
-[@@deriving compare]
+module ReportableViolation = struct
+  type t = {nullsafe_mode: NullsafeMode.t; violation: violation}
 
-let check ~nullsafe_mode nullability =
-  match nullability with
-  | Nullability.Nullable | Nullability.Null ->
-      Error {nullsafe_mode; nullability}
-  | other when not (Nullability.is_considered_nonnull ~nullsafe_mode other) ->
-      Error {nullsafe_mode; nullability}
-  | _ ->
-      Ok ()
+  type dereference_type =
+    | MethodCall of Procname.t
+    | AccessToField of Fieldname.t
+    | AccessByIndex of {index_desc: string}
+    | ArrayLengthAccess
+  [@@deriving compare]
+
+  let get_origin_opt ~nullable_object_descr origin =
+    let should_show_origin =
+      match nullable_object_descr with
+      | Some object_expression ->
+          not (ErrorRenderingUtils.is_object_nullability_self_explanatory ~object_expression origin)
+      | None ->
+          true
+    in
+    if should_show_origin then Some origin else None
 
 
-let get_origin_opt ~nullable_object_descr origin =
-  let should_show_origin =
-    match nullable_object_descr with
-    | Some object_expression ->
-        not (ErrorRenderingUtils.is_object_nullability_self_explanatory ~object_expression origin)
-    | None ->
-        true
-  in
-  if should_show_origin then Some origin else None
+  let get_description {nullsafe_mode; violation= {nullability}} ~dereference_location
+      dereference_type ~nullable_object_descr ~nullable_object_origin =
+    let module MF = MarkupFormatter in
+    let special_message =
+      if not (NullsafeMode.equal NullsafeMode.Default nullsafe_mode) then
+        ErrorRenderingUtils.mk_special_nullsafe_issue ~nullsafe_mode ~bad_nullability:nullability
+          ~bad_usage_location:dereference_location nullable_object_origin
+      else None
+    in
+    match special_message with
+    | Some desc ->
+        desc
+    | _ ->
+        let what_is_dereferred_str =
+          match dereference_type with
+          | MethodCall _ | AccessToField _ -> (
+            match nullable_object_descr with
+            | None ->
+                "Object"
+            (* Just describe an object itself *)
+            | Some descr ->
+                MF.monospaced_to_string descr )
+          | ArrayLengthAccess | AccessByIndex _ -> (
+            (* In Java, those operations can be applied only to arrays *)
+            match nullable_object_descr with
+            | None ->
+                "Array"
+            | Some descr ->
+                Format.sprintf "Array %s" (MF.monospaced_to_string descr) )
+        in
+        let action_descr =
+          match dereference_type with
+          | MethodCall method_name ->
+              Format.sprintf "calling %s"
+                (MF.monospaced_to_string (Procname.to_simplified_string method_name))
+          | AccessToField field_name ->
+              Format.sprintf "accessing field %s"
+                (MF.monospaced_to_string (Fieldname.to_simplified_string field_name))
+          | AccessByIndex {index_desc} ->
+              Format.sprintf "accessing at index %s" (MF.monospaced_to_string index_desc)
+          | ArrayLengthAccess ->
+              "accessing its length"
+        in
+        let origin_descr =
+          get_origin_opt ~nullable_object_descr nullable_object_origin
+          |> Option.bind ~f:(fun origin -> TypeOrigin.get_description origin)
+          |> Option.value_map ~f:(fun origin -> ": " ^ origin) ~default:""
+        in
+        let alternative_method_description =
+          ErrorRenderingUtils.find_alternative_nonnull_method_description nullable_object_origin
+        in
+        let alternative_recommendation =
+          Option.value_map alternative_method_description
+            ~f:(fun descr ->
+              Format.asprintf " If this is intentional, use %a instead." MF.pp_monospaced descr )
+            ~default:""
+        in
+        let description =
+          match nullability with
+          | Nullability.Null ->
+              Format.sprintf
+                "NullPointerException will be thrown at this line! %s is `null` and is \
+                 dereferenced via %s%s."
+                what_is_dereferred_str action_descr origin_descr
+          | Nullability.Nullable ->
+              Format.sprintf "%s is nullable and is not locally checked for null when %s%s.%s"
+                what_is_dereferred_str action_descr origin_descr alternative_recommendation
+          | other ->
+              Logging.die InternalError
+                "violation_description:: invariant violation: unexpected nullability %a"
+                Nullability.pp other
+        in
+        (description, IssueType.eradicate_nullable_dereference, dereference_location)
 
 
-let violation_description {nullsafe_mode; nullability} ~dereference_location dereference_type
-    ~nullable_object_descr ~nullable_object_origin =
-  let module MF = MarkupFormatter in
-  let special_message =
-    if not (NullsafeMode.equal NullsafeMode.Default nullsafe_mode) then
-      ErrorRenderingUtils.mk_special_nullsafe_issue ~nullsafe_mode ~bad_nullability:nullability
-        ~bad_usage_location:dereference_location nullable_object_origin
-    else None
-  in
-  match special_message with
-  | Some desc ->
-      desc
+  let get_severity {nullsafe_mode} = NullsafeMode.severity nullsafe_mode
+end
+
+let check nullability =
+  match nullability with
+  (* StrictNonnull is the only "real" value that is not null according to type system rules.
+     Other values can not be fully trusted.
+  *)
+  | Nullability.StrictNonnull ->
+      Ok ()
   | _ ->
-      let what_is_dereferred_str =
-        match dereference_type with
-        | MethodCall _ | AccessToField _ -> (
-          match nullable_object_descr with
-          | None ->
-              "Object"
-          (* Just describe an object itself *)
-          | Some descr ->
-              MF.monospaced_to_string descr )
-        | ArrayLengthAccess | AccessByIndex _ -> (
-          (* In Java, those operations can be applied only to arrays *)
-          match nullable_object_descr with
-          | None ->
-              "Array"
-          | Some descr ->
-              Format.sprintf "Array %s" (MF.monospaced_to_string descr) )
-      in
-      let action_descr =
-        match dereference_type with
-        | MethodCall method_name ->
-            Format.sprintf "calling %s"
-              (MF.monospaced_to_string (Procname.to_simplified_string method_name))
-        | AccessToField field_name ->
-            Format.sprintf "accessing field %s"
-              (MF.monospaced_to_string (Fieldname.to_simplified_string field_name))
-        | AccessByIndex {index_desc} ->
-            Format.sprintf "accessing at index %s" (MF.monospaced_to_string index_desc)
-        | ArrayLengthAccess ->
-            "accessing its length"
-      in
-      let origin_descr =
-        get_origin_opt ~nullable_object_descr nullable_object_origin
-        |> Option.bind ~f:(fun origin -> TypeOrigin.get_description origin)
-        |> Option.value_map ~f:(fun origin -> ": " ^ origin) ~default:""
-      in
-      let alternative_method_description =
-        ErrorRenderingUtils.find_alternative_nonnull_method_description nullable_object_origin
-      in
-      let alternative_recommendation =
-        Option.value_map alternative_method_description
-          ~f:(fun descr ->
-            Format.asprintf " If this is intentional, use %a instead." MF.pp_monospaced descr )
-          ~default:""
-      in
-      let description =
-        match nullability with
-        | Nullability.Null ->
-            Format.sprintf
-              "NullPointerException will be thrown at this line! %s is `null` and is dereferenced \
-               via %s%s."
-              what_is_dereferred_str action_descr origin_descr
-        | Nullability.Nullable ->
-            Format.sprintf "%s is nullable and is not locally checked for null when %s%s.%s"
-              what_is_dereferred_str action_descr origin_descr alternative_recommendation
-        | other ->
-            Logging.die InternalError
-              "violation_description:: invariant violation: unexpected nullability %a"
-              Nullability.pp other
-      in
-      (description, IssueType.eradicate_nullable_dereference, dereference_location)
+      Error {nullability}
 
 
-let violation_severity {nullsafe_mode} = NullsafeMode.severity nullsafe_mode
+let to_reportable_violation nullsafe_mode ({nullability} as violation) =
+  if Nullability.is_considered_nonnull ~nullsafe_mode nullability then None
+  else Some ReportableViolation.{nullsafe_mode; violation}

infer/src/nullsafe/DereferenceRule.mli

@@ -11,23 +11,36 @@ open! IStd
 
 type violation [@@deriving compare]
 
-val check : nullsafe_mode:NullsafeMode.t -> Nullability.t -> (unit, violation) result
-
-type dereference_type =
-  | MethodCall of Procname.t
-  | AccessToField of Fieldname.t
-  | AccessByIndex of {index_desc: string}
-  | ArrayLengthAccess
-[@@deriving compare]
-
-val violation_description :
-     violation
-  -> dereference_location:Location.t
-  -> dereference_type
-  -> nullable_object_descr:string option
-  -> nullable_object_origin:TypeOrigin.t
-  -> string * IssueType.t * Location.t
-(** Given context around violation, return error message together with the info where to put this
-    message *)
-
-val violation_severity : violation -> Exceptions.severity
+val check : Nullability.t -> (unit, violation) result
+(** violation of Dereference rule reflects possibility of dereferencing of `null`. Note that this
+    might or might not be severe enough to be reported to the user, depending on the mode
+    agreements. *)
+
+(** Violation that needs to be reported to the user. *)
+module ReportableViolation : sig
+  type t
+
+  type dereference_type =
+    | MethodCall of Procname.t
+    | AccessToField of Fieldname.t
+    | AccessByIndex of {index_desc: string}
+    | ArrayLengthAccess
+  [@@deriving compare]
+
+  val get_severity : t -> Exceptions.severity
+  (** Severity of the violation to be reported *)
+
+  val get_description :
+       t
+    -> dereference_location:Location.t
+    -> dereference_type
+    -> nullable_object_descr:string option
+    -> nullable_object_origin:TypeOrigin.t
+    -> string * IssueType.t * Location.t
+  (** Given context around violation, return error message together with the info where to put this
+      message *)
+end
+
+val to_reportable_violation : NullsafeMode.t -> violation -> ReportableViolation.t option
+(** Depending on the mode, violation might or might not be important enough to be reported to the
+    user. If it should NOT be reported for that mode, this function will return None. *)

infer/src/nullsafe/eradicateChecks.ml

@@ -31,8 +31,7 @@ let is_virtual = function
 let check_object_dereference ~nullsafe_mode tenv find_canonical_duplicate curr_pname node instr_ref
     object_exp dereference_type inferred_nullability loc =
   Result.iter_error
-    (DereferenceRule.check ~nullsafe_mode
-       (InferredNullability.get_nullability inferred_nullability))
+    (DereferenceRule.check (InferredNullability.get_nullability inferred_nullability))
     ~f:(fun dereference_violation ->
       let nullable_object_origin = InferredNullability.get_origin inferred_nullability in
       let nullable_object_descr = explain_expr tenv node object_exp in
@@ -407,7 +406,7 @@ let check_call_receiver ~nullsafe_mode tenv find_canonical_duplicate curr_pdesc
           loc
       in
       check_object_dereference ~nullsafe_mode tenv find_canonical_duplicate curr_pdesc node
-        instr_ref original_this_e (DereferenceRule.MethodCall callee_pname)
+        instr_ref original_this_e (DereferenceRule.ReportableViolation.MethodCall callee_pname)
         this_inferred_nullability loc
   | [] ->
       ()

infer/src/nullsafe/typeCheck.ml

@@ -165,8 +165,9 @@ let rec typecheck_expr ~nullsafe_mode find_canonical_duplicate visited checks te
           in
           if checks.eradicate then
             EradicateChecks.check_object_dereference ~nullsafe_mode tenv find_canonical_duplicate
-              curr_pdesc node instr_ref exp (DereferenceRule.AccessToField field_name)
-              inferred_nullability loc ;
+              curr_pdesc node instr_ref exp
+              (DereferenceRule.ReportableViolation.AccessToField field_name) inferred_nullability
+              loc ;
           tr_new
       | Exp.Lindex (array_exp, index_exp) ->
           let _, inferred_nullability =
@@ -179,7 +180,7 @@ let rec typecheck_expr ~nullsafe_mode find_canonical_duplicate visited checks te
           if checks.eradicate then
             EradicateChecks.check_object_dereference ~nullsafe_mode tenv find_canonical_duplicate
               curr_pdesc node instr_ref array_exp
-              (DereferenceRule.AccessByIndex {index_desc})
+              (DereferenceRule.ReportableViolation.AccessByIndex {index_desc})
               inferred_nullability loc ;
           let typ, _ = tr_default in
           (typ, InferredNullability.create TypeOrigin.ArrayAccess)
@@ -1195,7 +1196,8 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
       in
       if checks.eradicate then
         EradicateChecks.check_object_dereference ~nullsafe_mode tenv find_canonical_duplicate
-          curr_pdesc node instr_ref array_exp DereferenceRule.ArrayLengthAccess ta loc ;
+          curr_pdesc node instr_ref array_exp DereferenceRule.ReportableViolation.ArrayLengthAccess
+          ta loc ;
       TypeState.add_id id
         (Typ.mk (Tint Typ.IInt), InferredNullability.create TypeOrigin.ArrayLengthResult)
         typestate ~descr:"array.length"

infer/src/nullsafe/typeErr.ml

@@ -72,7 +72,7 @@ type err_instance =
   | Nullable_dereference of
       { dereference_violation: DereferenceRule.violation
       ; dereference_location: Location.t
-      ; dereference_type: DereferenceRule.dereference_type
+      ; dereference_type: DereferenceRule.ReportableViolation.dereference_type
       ; nullable_object_descr: string option
       ; nullable_object_origin: TypeOrigin.t }
   | Bad_assignment of
@@ -262,15 +262,15 @@ let get_error_info_if_reportable ~nullsafe_mode err_instance =
       ; nullable_object_descr
       ; dereference_type
       ; nullable_object_origin } ->
+      let+ reportable_violation =
+        DereferenceRule.to_reportable_violation nullsafe_mode dereference_violation
+      in
       let description, issue_type, error_location =
-        DereferenceRule.violation_description ~dereference_location dereference_violation
-          dereference_type ~nullable_object_descr ~nullable_object_origin
+        DereferenceRule.ReportableViolation.get_description reportable_violation
+          ~dereference_location dereference_type ~nullable_object_descr ~nullable_object_origin
       in
-      Some
-        ( description
-        , issue_type
-        , Some error_location
-        , DereferenceRule.violation_severity dereference_violation )
+      let severity = DereferenceRule.ReportableViolation.get_severity reportable_violation in
+      (description, issue_type, Some error_location, severity)
   | Inconsistent_subclass
       {inheritance_violation; violation_type; base_proc_name; overridden_proc_name} ->
       Some

infer/src/nullsafe/typeErr.mli

@@ -48,7 +48,7 @@ type err_instance =
   | Nullable_dereference of
       { dereference_violation: DereferenceRule.violation
       ; dereference_location: Location.t
-      ; dereference_type: DereferenceRule.dereference_type
+      ; dereference_type: DereferenceRule.ReportableViolation.dereference_type
       ; nullable_object_descr: string option
       ; nullable_object_origin: TypeOrigin.t }
   | Bad_assignment of

infer/tests/codetoanalyze/java/nullsafe-default/issues.exp

@@ -139,7 +139,7 @@ codetoanalyze/java/nullsafe-default/InheritanceForStrictMode.java, codetoanalyze
 codetoanalyze/java/nullsafe-default/InheritanceForStrictMode.java, codetoanalyze.java.nullsafe_default.InheritanceForStrictMode$StrictExtendingNonstrict.params(java.lang.String,java.lang.String):void, 0, ERADICATE_INCONSISTENT_SUBCLASS_PARAMETER_ANNOTATION, no_bucket, ERROR, [First parameter `badToRemoveNullableInChildren` of method `InheritanceForStrictMode$StrictExtendingNonstrict.params(...)` is missing `@Nullable` declaration when overriding `InheritanceForStrictMode$NonStrictBase.params(...)`. The parent method declared it can handle `null` for this param, so the child should also declare that.]
 codetoanalyze/java/nullsafe-default/InheritanceForStrictMode.java, codetoanalyze.java.nullsafe_default.InheritanceForStrictMode$StrictExtendingStrict.badToAddNullableInChildren():java.lang.String, 0, ERADICATE_INCONSISTENT_SUBCLASS_RETURN_ANNOTATION, no_bucket, ERROR, [Child method `InheritanceForStrictMode$StrictExtendingStrict.badToAddNullableInChildren()` is not substitution-compatible with its parent: the return type is declared as nullable, but parent method `InheritanceForStrictMode$StrictBase.badToAddNullableInChildren()` is missing `@Nullable` declaration. Either mark the parent as `@Nullable` or ensure the child does not return `null`.]
 codetoanalyze/java/nullsafe-default/InheritanceForStrictMode.java, codetoanalyze.java.nullsafe_default.InheritanceForStrictMode$StrictExtendingStrict.params(java.lang.String,java.lang.String):void, 0, ERADICATE_INCONSISTENT_SUBCLASS_PARAMETER_ANNOTATION, no_bucket, ERROR, [First parameter `badToRemoveNullableInChildren` of method `InheritanceForStrictMode$StrictExtendingStrict.params(...)` is missing `@Nullable` declaration when overriding `InheritanceForStrictMode$StrictBase.params(...)`. The parent method declared it can handle `null` for this param, so the child should also declare that.]
-codetoanalyze/java/nullsafe-default/JunitExample.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_IS_CLEAN, no_bucket, INFO, []
+codetoanalyze/java/nullsafe-default/JunitExample.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_NEEDS_FIXING, no_bucket, INFO, []
 codetoanalyze/java/nullsafe-default/LibraryCalls.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_NEEDS_FIXING, no_bucket, INFO, []
 codetoanalyze/java/nullsafe-default/LibraryCalls.java, codetoanalyze.java.nullsafe_default.LibraryCalls.badAtomicReferenceDereference(java.util.concurrent.atomic.AtomicReference):java.lang.String, 0, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, WARNING, [`ref.get()` is nullable and is not locally checked for null when calling `toString()`: call to AtomicReference.get() at line 35 (nullable according to nullsafe internal models).]
 codetoanalyze/java/nullsafe-default/LibraryCalls.java, codetoanalyze.java.nullsafe_default.LibraryCalls.badPhantomReferenceDereference(java.lang.ref.PhantomReference):java.lang.String, 0, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, WARNING, [`ref.get()` is nullable and is not locally checked for null when calling `toString()`: call to PhantomReference.get() at line 27 (nullable according to nullsafe internal models).]
@@ -198,7 +198,7 @@ codetoanalyze/java/nullsafe-default/NullMethodCall.java, Linters_dummy_method, 1
 codetoanalyze/java/nullsafe-default/NullMethodCall.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_IS_CLEAN, no_bucket, INFO, []
 codetoanalyze/java/nullsafe-default/NullMethodCall.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_IS_CLEAN, no_bucket, INFO, []
 codetoanalyze/java/nullsafe-default/NullMethodCall.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_IS_CLEAN, no_bucket, INFO, []
-codetoanalyze/java/nullsafe-default/NullMethodCall.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_IS_CLEAN, no_bucket, INFO, []
+codetoanalyze/java/nullsafe-default/NullMethodCall.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_NEEDS_FIXING, no_bucket, INFO, []
 codetoanalyze/java/nullsafe-default/NullMethodCall.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_NEEDS_FIXING, no_bucket, INFO, []
 codetoanalyze/java/nullsafe-default/NullMethodCall.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_NEEDS_FIXING, no_bucket, INFO, []
 codetoanalyze/java/nullsafe-default/NullMethodCall.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_NEEDS_FIXING, no_bucket, INFO, []
@@ -229,7 +229,7 @@ codetoanalyze/java/nullsafe-default/NullMethodCall.java, codetoanalyze.java.null
 codetoanalyze/java/nullsafe-default/NullsafeMode.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_IS_CLEAN, no_bucket, INFO, []
 codetoanalyze/java/nullsafe-default/NullsafeMode.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_IS_CLEAN, no_bucket, INFO, []
 codetoanalyze/java/nullsafe-default/NullsafeMode.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_IS_CLEAN, no_bucket, INFO, []
-codetoanalyze/java/nullsafe-default/NullsafeMode.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_IS_CLEAN, no_bucket, INFO, []
+codetoanalyze/java/nullsafe-default/NullsafeMode.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_NEEDS_FIXING, no_bucket, INFO, []
 codetoanalyze/java/nullsafe-default/NullsafeMode.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_NEEDS_FIXING, no_bucket, INFO, []
 codetoanalyze/java/nullsafe-default/NullsafeMode.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_NEEDS_FIXING, no_bucket, INFO, []
 codetoanalyze/java/nullsafe-default/NullsafeMode.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_NEEDS_FIXING, no_bucket, INFO, []
@@ -373,7 +373,7 @@ codetoanalyze/java/nullsafe-default/TrueFalseOnNull.java, Linters_dummy_method,
 codetoanalyze/java/nullsafe-default/TrueFalseOnNull.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_IS_CLEAN, no_bucket, INFO, []
 codetoanalyze/java/nullsafe-default/TrueFalseOnNull.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_IS_CLEAN, no_bucket, INFO, []
 codetoanalyze/java/nullsafe-default/TrueFalseOnNull.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_IS_CLEAN, no_bucket, INFO, []
-codetoanalyze/java/nullsafe-default/TrueFalseOnNull.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_IS_CLEAN, no_bucket, INFO, []
+codetoanalyze/java/nullsafe-default/TrueFalseOnNull.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_NEEDS_FIXING, no_bucket, INFO, []
 codetoanalyze/java/nullsafe-default/TrueFalseOnNull.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_NEEDS_FIXING, no_bucket, INFO, []
 codetoanalyze/java/nullsafe-default/TrueFalseOnNull.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_NEEDS_FIXING, no_bucket, INFO, []
 codetoanalyze/java/nullsafe-default/TrueFalseOnNull.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_NEEDS_FIXING, no_bucket, INFO, []