[nullsafe] Support Nullsafe(Local, trust=all/none) mode

Summary:
Add support for nullsafe mode with `trust=all` and `trust=none` a case
with a specific trust list is not supported yet and needs to be
implemented separately.

Tests introduce one unexpected
`ERADICATE_INCONSISTENT_SUBCLASS_PARAMETER_ANNOTATION` issue which
complains about `this` having incorrect nullability; it is a bug and
needs to be fixed separately.

Reviewed By: mityal

Differential Revision: D19662708

fbshipit-source-id: 3bc1e3952

infer/man/man1/infer-full.txt

@@ -412,8 +412,9 @@ OPTIONS
              ERADICATE_PARAMETER_NOT_NULLABLE (enabled by default),
              ERADICATE_RETURN_NOT_NULLABLE (enabled by default),
              ERADICATE_RETURN_OVER_ANNOTATED (enabled by default),
-             ERADICATE_UNCHECKED_NONSTRICT_FROM_STRICT (enabled by default),
-             ERADICATE_UNVETTED_THIRD_PARTY_IN_STRICT (enabled by default),
+             ERADICATE_UNCHECKED_USAGE_IN_NULLSAFE (enabled by default),
+             ERADICATE_UNVETTED_THIRD_PARTY_IN_NULLSAFE (enabled by
+           default),
              EXECUTION_TIME_COMPLEXITY_INCREASE (enabled by default),
              EXECUTION_TIME_COMPLEXITY_INCREASE_COLD_START (enabled by
            default),

infer/man/man1/infer-report.txt

@@ -141,8 +141,9 @@ OPTIONS
              ERADICATE_PARAMETER_NOT_NULLABLE (enabled by default),
              ERADICATE_RETURN_NOT_NULLABLE (enabled by default),
              ERADICATE_RETURN_OVER_ANNOTATED (enabled by default),
-             ERADICATE_UNCHECKED_NONSTRICT_FROM_STRICT (enabled by default),
-             ERADICATE_UNVETTED_THIRD_PARTY_IN_STRICT (enabled by default),
+             ERADICATE_UNCHECKED_USAGE_IN_NULLSAFE (enabled by default),
+             ERADICATE_UNVETTED_THIRD_PARTY_IN_NULLSAFE (enabled by
+           default),
              EXECUTION_TIME_COMPLEXITY_INCREASE (enabled by default),
              EXECUTION_TIME_COMPLEXITY_INCREASE_COLD_START (enabled by
            default),

infer/man/man1/infer.txt

@@ -412,8 +412,9 @@ OPTIONS
              ERADICATE_PARAMETER_NOT_NULLABLE (enabled by default),
              ERADICATE_RETURN_NOT_NULLABLE (enabled by default),
              ERADICATE_RETURN_OVER_ANNOTATED (enabled by default),
-             ERADICATE_UNCHECKED_NONSTRICT_FROM_STRICT (enabled by default),
-             ERADICATE_UNVETTED_THIRD_PARTY_IN_STRICT (enabled by default),
+             ERADICATE_UNCHECKED_USAGE_IN_NULLSAFE (enabled by default),
+             ERADICATE_UNVETTED_THIRD_PARTY_IN_NULLSAFE (enabled by
+           default),
              EXECUTION_TIME_COMPLEXITY_INCREASE (enabled by default),
              EXECUTION_TIME_COMPLEXITY_INCREASE_COLD_START (enabled by
            default),

infer/src/IR/Annot.ml

@@ -45,6 +45,11 @@ let rec has_matching_str_value ~pred = function
       false
 
 
+let find_parameter t ~name =
+  let match_name param = Option.exists param.name ~f:(String.equal name) in
+  List.find t.parameters ~f:match_name |> Option.map ~f:(fun x -> x.value)
+
+
 (** Pretty print an annotation. *)
 let prefix = match Language.curr_language_is Java with true -> "@" | false -> "_"
 

infer/src/IR/Annot.mli

@@ -36,7 +36,9 @@ val final : t
 
 val has_matching_str_value : pred:(string -> bool) -> value -> bool
 (** Check if annotation parameter value contains a string satisfying a predicate. For convenience it
-    works both with raw [Vstr] and [Vstr] inside [Varray]. *)
+    works both with raw [Str] and [Str] inside [Array]. *)
+
+val find_parameter : t -> name:string -> value option
 
 val pp : F.formatter -> t -> unit
 (** Pretty print an annotation. *)

infer/src/base/IssueType.ml

@@ -277,14 +277,14 @@ let eradicate_return_over_annotated =
   register_from_string "ERADICATE_RETURN_OVER_ANNOTATED" ~hum:"Return Over Annotated"
 
 
-let eradicate_forbidden_non_strict_in_strict =
-  register_from_string "ERADICATE_UNCHECKED_NONSTRICT_FROM_STRICT"
-    ~hum:"Strict mode: unchecked usage of a value from non-strict code"
+let eradicate_unchecked_usage_in_nullsafe =
+  register_from_string "ERADICATE_UNCHECKED_USAGE_IN_NULLSAFE"
+    ~hum:"Nullsafe mode: unchecked usage of a value"
 
 
-let eradicate_unvetted_third_party_in_strict =
-  register_from_string "ERADICATE_UNVETTED_THIRD_PARTY_IN_STRICT"
-    ~hum:"Strict mode: unchecked usage of unvetted third-party"
+let eradicate_unvetted_third_party_in_nullsafe =
+  register_from_string "ERADICATE_UNVETTED_THIRD_PARTY_IN_NULLSAFE"
+    ~hum:"Nullsafe mode: unchecked usage of unvetted third-party"
 
 
 let expensive_cost_call ~kind ~is_on_cold_start ~is_on_ui_thread =

infer/src/base/IssueType.mli

@@ -166,9 +166,9 @@ val eradicate_return_not_nullable : t
 
 val eradicate_return_over_annotated : t
 
-val eradicate_unvetted_third_party_in_strict : t
+val eradicate_unvetted_third_party_in_nullsafe : t
 
-val eradicate_forbidden_non_strict_in_strict : t
+val eradicate_unchecked_usage_in_nullsafe : t
 
 val expensive_cost_call : kind:CostKind.t -> is_on_cold_start:bool -> is_on_ui_thread:bool -> t
 

infer/src/checkers/annotations.ml

@@ -63,6 +63,8 @@ let nullable = "Nullable"
 
 let nullsafe_strict = "NullsafeStrict"
 
+let nullsafe = "Nullsafe"
+
 let mainthread = "MainThread"
 
 let nonblocking = "NonBlocking"
@@ -142,6 +144,8 @@ let class_name_matches s ((annot : Annot.t), _) = String.equal s annot.class_nam
 
 let ia_ends_with ia ann_name = List.exists ~f:(fun (a, _) -> annot_ends_with a ann_name) ia
 
+let find_ia_ends_with ia ann_name = List.find ~f:(fun (a, _) -> annot_ends_with a ann_name) ia
+
 let ia_contains ia ann_name = List.exists ~f:(class_name_matches ann_name) ia
 
 let pdesc_get_return_annot pdesc =
@@ -192,6 +196,8 @@ let ia_is_nonnull ia = List.exists ~f:(ia_ends_with ia) [nonnull; notnull; camel
 
 let ia_is_nullsafe_strict ia = ia_ends_with ia nullsafe_strict
 
+let ia_find_nullsafe ia = Option.map (find_ia_ends_with ia nullsafe) ~f:fst
+
 let ia_is_false_on_null ia = ia_ends_with ia false_on_null
 
 let ia_is_returns_ownership ia = ia_ends_with ia returns_ownership

infer/src/checkers/annotations.mli

@@ -78,6 +78,8 @@ val ia_is_nullable : Annot.Item.t -> bool
 
 val ia_is_nullsafe_strict : Annot.Item.t -> bool
 
+val ia_find_nullsafe : Annot.Item.t -> Annot.t option
+
 val ia_is_true_on_null : Annot.Item.t -> bool
 
 val ia_is_expensive : Annot.Item.t -> bool

infer/src/istd/IList.ml

@@ -216,3 +216,14 @@ let move_last_to_first =
         move_last_to_first_helper tl (hd :: rev_acc)
   in
   fun l -> move_last_to_first_helper l []
+
+
+let traverse_opt xs ~f =
+  List.fold_until xs ~init:[]
+    ~f:(fun acc x ->
+      match f x with
+      | Some r ->
+          Continue_or_stop.Continue (r :: acc)
+      | _ ->
+          Continue_or_stop.Stop None )
+    ~finish:(fun acc -> Some (List.rev acc))

infer/src/istd/IList.mli

@@ -69,3 +69,7 @@ val fold2_result :
   -> ('acc, 'err) result Base.List.Or_unequal_lengths.t
 
 val move_last_to_first : 'a list -> 'a list
+
+val traverse_opt : 'a list -> f:('a -> 'b option) -> 'b list option
+(** Applies [f] to the elements of the list and returns [None] if any application results in [None]
+    otherwise returns [Some list']. *)

infer/src/nullsafe/AnnotatedNullability.ml

@@ -17,6 +17,7 @@ module F = Format
 type t =
   | Nullable of nullable_origin
   | UncheckedNonnull of unchecked_nonnull_origin  (** See {!Nullability.t} for explanation *)
+  | LocallyCheckedNonnull
   | StrictNonnull of strict_nonnull_origin
 [@@deriving compare]
 
@@ -52,6 +53,8 @@ let get_nullability = function
       Nullability.Nullable
   | UncheckedNonnull _ ->
       Nullability.UncheckedNonnull
+  | LocallyCheckedNonnull ->
+      Nullability.LocallyCheckedNonnull
   | StrictNonnull _ ->
       Nullability.StrictNonnull
 
@@ -87,6 +90,8 @@ let pp fmt t =
       F.fprintf fmt "Nullable[%s]" (string_of_nullable_origin origin)
   | UncheckedNonnull origin ->
       F.fprintf fmt "UncheckedNonnull[%s]" (string_of_declared_nonnull_origin origin)
+  | LocallyCheckedNonnull ->
+      F.fprintf fmt "LocallyCheckedNonnull"
   | StrictNonnull origin ->
       F.fprintf fmt "StrictNonnull[%s]" (string_of_nonnull_origin origin)
 
@@ -103,6 +108,8 @@ let of_type_and_annotation ~(nullsafe_mode : NullsafeMode.t) typ annotations =
     match nullsafe_mode with
     | NullsafeMode.Strict ->
         StrictNonnull StrictMode
+    | NullsafeMode.Local _ ->
+        LocallyCheckedNonnull
     | NullsafeMode.Default ->
         if Annotations.ia_is_nonnull annotations then UncheckedNonnull AnnotatedNonnull
           (* Currently, we treat not annotated types as nonnull *)

infer/src/nullsafe/AnnotatedNullability.mli

@@ -19,6 +19,7 @@ open! IStd
 type t =
   | Nullable of nullable_origin
   | UncheckedNonnull of unchecked_nonnull_origin  (** See {!Nullability.t} for explanation *)
+  | LocallyCheckedNonnull
   | StrictNonnull of strict_nonnull_origin
 [@@deriving compare]
 

infer/src/nullsafe/AssignmentRule.ml

@@ -22,26 +22,38 @@ and function_info =
   ; param_position: int
   ; function_procname: Procname.t }
 
-let is_whitelisted_assignment ~nullsafe_mode ~lhs ~rhs =
-  match nullsafe_mode with
-  | NullsafeMode.Default -> (
-    match (lhs, rhs) with
-    | Nullability.StrictNonnull, Nullability.UncheckedNonnull ->
-        (* We allow UncheckedNonnull -> StrictNonnull conversion outside of strict mode for better adoption.
-           Otherwise using strictified classes in non-strict context becomes a pain because
-           of extra warnings.
-        *)
-        true
-    | _ ->
-        false )
+(** For better adoption we allow certain conversions. Otherwise using code checked under different
+    nullsafe modes becomes a pain because of extra warnings. *)
+module AssignmentWhitelist = struct
+  let all_whitelisted =
+    [ (Nullability.StrictNonnull, Nullability.UncheckedNonnull)
+    ; (Nullability.LocallyCheckedNonnull, Nullability.UncheckedNonnull)
+    ; (Nullability.StrictNonnull, Nullability.LocallyCheckedNonnull) ]
+
+
+  let all_whitelisted_in_mode = function
+    | NullsafeMode.Default | NullsafeMode.Local NullsafeMode.Trust.All ->
+        all_whitelisted
+    | NullsafeMode.Local (NullsafeMode.Trust.Only ([] as _classes))
+    | NullsafeMode.Local (NullsafeMode.Trust.Only _classes) ->
+        (* TODO(T61473665): case with specified non-empty classes not supported now, defaulting to trust=none *)
+        [(Nullability.StrictNonnull, Nullability.LocallyCheckedNonnull)]
     | NullsafeMode.Strict ->
-      false
+        []
+
+
+  let is_allowed_in_mode ~nullsafe_mode ~lhs ~rhs =
+    List.exists (all_whitelisted_in_mode nullsafe_mode) ~f:(Nullability.equal_pair (lhs, rhs))
+
 
+  let is_potentially_allowed ~lhs ~rhs =
+    List.exists all_whitelisted ~f:(Nullability.equal_pair (lhs, rhs))
+end
 
 let check ~(nullsafe_mode : NullsafeMode.t) ~lhs ~rhs =
   let is_allowed_assignment =
     Nullability.is_subtype ~subtype:rhs ~supertype:lhs
-    || is_whitelisted_assignment ~nullsafe_mode ~lhs ~rhs
+    || AssignmentWhitelist.is_allowed_in_mode ~nullsafe_mode ~lhs ~rhs
   in
   Result.ok_if_true is_allowed_assignment ~error:{nullsafe_mode; lhs; rhs}
 
@@ -67,7 +79,7 @@ let pp_param_name fmt mangled =
   else Format.fprintf fmt "(%a)" MarkupFormatter.pp_monospaced name
 
 
-let bad_param_description
+let mk_description_for_bad_param_passed
     {model_source; param_signature; actual_param_expression; param_position; function_procname}
     ~param_nullability nullability_evidence =
   let nullability_evidence_as_suffix =
@@ -83,7 +95,9 @@ let bad_param_description
             "`null`"
         | Nullability.Nullable ->
             "nullable"
-        | Nullability.StrictNonnull | Nullability.UncheckedNonnull ->
+        | Nullability.StrictNonnull
+        | Nullability.UncheckedNonnull
+        | Nullability.LocallyCheckedNonnull ->
             Logging.die InternalError "Invariant violation: unexpected nullability"
       in
       Format.asprintf "%a is %s" MF.pp_monospaced actual_param_expression nullability_descr
@@ -102,7 +116,7 @@ let bad_param_description
   in
   match suggested_file_to_add_third_party with
   | Some sig_file_name ->
-      (* This is a special case. While for FB codebase we can assume "not annotated hence not nullable" rule for all signatures,
+      (* This is a special case. While for FB codebase we can assume "not annotated hence not nullable" rule for all_whitelisted signatures,
          This is not the case for third party functions, which can have different conventions,
          So we can not just say "param is declared as non-nullable" like we say for FB-internal or modelled case:
          param can be nullable according to API but it was just not annotated.
@@ -135,18 +149,6 @@ let bad_param_description
         nullability_evidence_as_suffix
 
 
-let is_unchecked_nonnull_to_strict_nonnull ~lhs ~rhs =
-  match (lhs, rhs) with
-  | Nullability.StrictNonnull, Nullability.UncheckedNonnull ->
-      true
-  (* Don't fold those cases into catch-all *)
-  | Nullability.StrictNonnull, _
-  | Nullability.UncheckedNonnull, _
-  | Nullability.Nullable, _
-  | Nullability.Null, _ ->
-      false
-
-
 let get_issue_type = function
   | PassingParamToFunction _ ->
       IssueType.eradicate_parameter_not_nullable
@@ -158,12 +160,12 @@ let get_issue_type = function
 
 let violation_description {nullsafe_mode; lhs; rhs} ~assignment_location assignment_type ~rhs_origin
     =
-  if is_unchecked_nonnull_to_strict_nonnull ~lhs ~rhs then (
-    if not (NullsafeMode.equal nullsafe_mode NullsafeMode.Strict) then
-      Logging.die InternalError "Unexpected situation: should not be a violation not in strict mode" ;
-    (* This type of violation is more subtle than the normal case because, so it should be rendered in a special way *)
-    ErrorRenderingUtils.get_strict_mode_violation_issue ~bad_usage_location:assignment_location
-      rhs_origin )
+  if AssignmentWhitelist.is_potentially_allowed ~lhs ~rhs then
+    (* This type of violation is more subtle than the normal case, so it should
+       be rendered in a special way. An 'impossible case' is checked in the
+       following call and will cause infer to die. *)
+    ErrorRenderingUtils.mk_special_nullsafe_issue ~nullsafe_mode ~bad_nullability:rhs
+      ~bad_usage_location:assignment_location rhs_origin
   else
     let nullability_evidence =
       get_origin_opt assignment_type rhs_origin
@@ -176,30 +178,33 @@ let violation_description {nullsafe_mode; lhs; rhs} ~assignment_location assignm
     let error_message =
       match assignment_type with
       | PassingParamToFunction function_info ->
-          bad_param_description function_info nullability_evidence ~param_nullability:rhs
+          mk_description_for_bad_param_passed function_info nullability_evidence
+            ~param_nullability:rhs
       | AssigningToField field_name ->
           let rhs_description =
+            Nullability.(
               match rhs with
               | Null ->
                   "`null`"
               | Nullable ->
                   "a nullable"
-            | StrictNonnull | UncheckedNonnull ->
-                Logging.die InternalError "Invariant violation: unexpected nullability"
+              | StrictNonnull | UncheckedNonnull | LocallyCheckedNonnull ->
+                  Logging.die InternalError "Invariant violation: unexpected nullability")
           in
           Format.asprintf "%a is declared non-nullable but is assigned %s%s." MF.pp_monospaced
             (Fieldname.get_field_name field_name)
             rhs_description nullability_evidence_as_suffix
       | ReturningFromFunction function_proc_name ->
           let return_description =
+            Nullability.(
               match rhs with
               | Null ->
-                (* Return `null` in all branches *)
+                  (* Return `null` in all_whitelisted branches *)
                   "`null`"
               | Nullable ->
                   "a nullable value"
-            | StrictNonnull | UncheckedNonnull ->
-                Logging.die InternalError "Invariant violation: unexpected nullability"
+              | StrictNonnull | UncheckedNonnull | LocallyCheckedNonnull ->
+                  Logging.die InternalError "Invariant violation: unexpected nullability")
           in
           Format.asprintf "%a: return type is declared non-nullable but the method returns %s%s."
             MF.pp_monospaced

infer/src/nullsafe/DereferenceRule.ml

@@ -21,10 +21,19 @@ let check ~nullsafe_mode nullability =
       Error {nullsafe_mode; nullability}
   | Nullability.UncheckedNonnull -> (
     match nullsafe_mode with
-    | NullsafeMode.Strict ->
+    | NullsafeMode.Strict | NullsafeMode.Local (NullsafeMode.Trust.Only []) ->
+        Error {nullsafe_mode; nullability}
+    | NullsafeMode.Local (NullsafeMode.Trust.Only _typ_names) ->
+        (* TODO(T61473665). For now treat as trust=none.  *)
         Error {nullsafe_mode; nullability}
-    | NullsafeMode.Default ->
+    | NullsafeMode.Local NullsafeMode.Trust.All | NullsafeMode.Default ->
         Ok () )
+  | Nullability.LocallyCheckedNonnull -> (
+    match nullsafe_mode with
+    | NullsafeMode.Default | NullsafeMode.Local _ ->
+        Ok ()
+    | NullsafeMode.Strict ->
+        Error {nullsafe_mode; nullability} )
   | Nullability.StrictNonnull ->
       Ok ()
 
@@ -40,15 +49,15 @@ let get_origin_opt ~nullable_object_descr origin =
   if should_show_origin then Some origin else None
 
 
-let violation_description {nullability} ~dereference_location dereference_type
+let violation_description {nullsafe_mode; nullability} ~dereference_location dereference_type
     ~nullable_object_descr ~nullable_object_origin =
   let module MF = MarkupFormatter in
   match nullability with
-  | Nullability.UncheckedNonnull ->
-      (* This can happen only in strict mode.
-         This type of violation is more subtle than the normal case because, so it should be rendered in a special way *)
-      ErrorRenderingUtils.get_strict_mode_violation_issue ~bad_usage_location:dereference_location
-        nullable_object_origin
+  | Nullability.UncheckedNonnull | Nullability.LocallyCheckedNonnull ->
+      (* These types of violations are possible in non-default nullsafe mode. For them we
+         provide tailored error messages. *)
+      ErrorRenderingUtils.mk_special_nullsafe_issue ~nullsafe_mode ~bad_nullability:nullability
+        ~bad_usage_location:dereference_location nullable_object_origin
   | _ ->
       let what_is_dereferred_str =
         match dereference_type with
@@ -95,7 +104,9 @@ let violation_description {nullability} ~dereference_location dereference_type
         | Nullability.Nullable ->
             Format.sprintf "%s is nullable and is not locally checked for null when %s%s."
               what_is_dereferred_str action_descr suffix
-        | Nullability.UncheckedNonnull | Nullability.StrictNonnull ->
+        | Nullability.UncheckedNonnull
+        | Nullability.LocallyCheckedNonnull
+        | Nullability.StrictNonnull ->
             Logging.die InternalError "Invariant violation: unexpected nullability"
       in
       (description, IssueType.eradicate_nullable_dereference, dereference_location)

infer/src/nullsafe/ErrorRenderingUtils.ml

@@ -83,7 +83,34 @@ let get_field_class_name field_name =
   |> Option.value_map ~f:(fun (classname, _) -> classname) ~default:"the field class"
 
 
-let get_info object_origin =
+let mk_coming_from nullsafe_mode nullability =
+  match (nullsafe_mode, nullability) with
+  | NullsafeMode.Strict, Nullability.UncheckedNonnull ->
+      "non-strict classes"
+  | NullsafeMode.Strict, Nullability.LocallyCheckedNonnull ->
+      "nullsafe-local classes"
+  | NullsafeMode.Local _, Nullability.UncheckedNonnull ->
+      "non-nullsafe classes"
+  | (_ as mode), nullability ->
+      Logging.die InternalError "Unexpected: using %s in %a should not be a violation"
+        (Nullability.to_string nullability)
+        NullsafeMode.pp mode
+
+
+let mk_recommendation nullsafe_mode nullability what =
+  match (nullsafe_mode, nullability) with
+  | NullsafeMode.Strict, Nullability.UncheckedNonnull
+  | NullsafeMode.Strict, Nullability.LocallyCheckedNonnull ->
+      Format.sprintf "make %s nullsafe strict" what
+  | NullsafeMode.Local _, Nullability.UncheckedNonnull ->
+      Format.sprintf "make %s nullsafe" what
+  | (_ as mode), nullability ->
+      Logging.die InternalError "Unexpected: using %s in %a should not be a violation"
+        (Nullability.to_string nullability)
+        NullsafeMode.pp mode
+
+
+let get_info object_origin nullsafe_mode bad_nullability =
   match object_origin with
   | TypeOrigin.MethodCall {pname; call_loc} ->
       let offending_object =
@@ -106,15 +133,15 @@ let get_info object_origin =
         in
         match suggested_third_party_sig_file with
         | None ->
-            ( "non-strict classes"
-            , Format.sprintf "strictify %s" what_to_strictify
-            , IssueType.eradicate_forbidden_non_strict_in_strict )
+            ( mk_coming_from nullsafe_mode bad_nullability
+            , mk_recommendation nullsafe_mode bad_nullability what_to_strictify
+            , IssueType.eradicate_unchecked_usage_in_nullsafe )
         | Some sig_file_name ->
             ( "not vetted third party methods"
             , Format.sprintf "add the correct signature to %s"
                 (ThirdPartyAnnotationGlobalRepo.get_user_friendly_third_party_sig_file_name
                    ~filename:sig_file_name)
-            , IssueType.eradicate_unvetted_third_party_in_strict )
+            , IssueType.eradicate_unvetted_third_party_in_nullsafe )
       in
       { offending_object
       ; object_loc
@@ -131,9 +158,11 @@ let get_info object_origin =
       (* TODO: currently we do not support third-party annotations for fields. Because of this,
          render error like it is a non-stict class. *)
       let what_is_used = "This field" in
-      let coming_from_explanation = "non-strict classes" in
-      let recommendation = Format.sprintf "strictify %s" (get_field_class_name field_name) in
-      let issue_type = IssueType.eradicate_forbidden_non_strict_in_strict in
+      let coming_from_explanation = mk_coming_from nullsafe_mode bad_nullability in
+      let recommendation =
+        mk_recommendation nullsafe_mode bad_nullability (get_field_class_name field_name)
+      in
+      let issue_type = IssueType.eradicate_unchecked_usage_in_nullsafe in
       { offending_object
       ; object_loc
       ; coming_from_explanation
@@ -145,20 +174,20 @@ let get_info object_origin =
         "Invariant violation: unexpected origin of declared non-nullable value"
 
 
-let get_strict_mode_violation_issue ~bad_usage_location object_origin =
+let mk_special_nullsafe_issue ~nullsafe_mode ~bad_nullability ~bad_usage_location object_origin =
   let { offending_object
       ; object_loc
       ; coming_from_explanation
       ; what_is_used
       ; recommendation
       ; issue_type } =
-    get_info object_origin
+    get_info object_origin nullsafe_mode bad_nullability
   in
   let description =
-    Format.sprintf
-      "%s: `@NullsafeStrict` mode prohibits using values coming from %s without a check. %s is \
-       used at line %d. Either add a local check for null or assertion, or %s."
-      offending_object coming_from_explanation what_is_used bad_usage_location.Location.line
-      recommendation
+    Format.asprintf
+      "%s: `@Nullsafe%a` mode prohibits using values coming from %s without a check. %s is used at \
+       line %d. Either add a local check for null or assertion, or %s."
+      offending_object NullsafeMode.pp nullsafe_mode coming_from_explanation what_is_used
+      bad_usage_location.Location.line recommendation
   in
   (description, issue_type, object_loc)

infer/src/nullsafe/ErrorRenderingUtils.mli

@@ -13,9 +13,13 @@ val is_object_nullability_self_explanatory : object_expression:string -> TypeOri
 (** In order to understand why such and such object is nullable (or not nullable), we render its
     origin. In some cases this is redundant and adds extra noise for the user. *)
 
-val get_strict_mode_violation_issue :
-  bad_usage_location:Location.t -> TypeOrigin.t -> string * IssueType.t * Location.t
-(** Situation when we tried to use UncheckedNonnull as StrictNonnull. This is disallowed only in
-    strict mode. Returns a tuple (error message, issue type, error location). NOTE: Location of the
-    error will be NOT in the place when the value is used (that is [bad_usage_location]), but where
-    the value is first obtained from. *)
+val mk_special_nullsafe_issue :
+     nullsafe_mode:NullsafeMode.t
+  -> bad_nullability:Nullability.t
+  -> bad_usage_location:Location.t
+  -> TypeOrigin.t
+  -> string * IssueType.t * Location.t
+(** Situation when we tried to use nonnull values of incompatible modes. This is disallowed in
+    strict and local mode. Returns a tuple (error message, issue type, error location). NOTE:
+    Location of the error will be NOT in the place when the value is used (that is
+    [bad_usage_location]), but where the value is first obtained from. *)

infer/src/nullsafe/Nullability.ml

@@ -14,6 +14,10 @@ type t =
       (** The type comes from a signature that is annotated (explicitly or implicitly according to
           conventions) as non-nullable. However, it might still contain null since the truthfulness
           of the declaration was not checked. *)
+  | LocallyCheckedNonnull
+      (** Non-nullable value the comes from a class checked under local mode. Local mode type-checks
+          files against its dependencies but does not require the dependencies to be transitively
+          checked. Therefore this type of non-nullable value is differentiated from StrictNonnull. *)
   | StrictNonnull
       (** Non-nullable value with the highest degree of certainty, because it is either:
 
@@ -27,6 +31,8 @@ type t =
           strike the balance between the strictness of analysis, convenience, and real-world risk. *)
 [@@deriving compare, equal]
 
+type pair = t * t [@@deriving compare, equal]
+
 let top = Nullable
 
 let join x y =
@@ -39,6 +45,8 @@ let join x y =
       Nullable
   | UncheckedNonnull, _ | _, UncheckedNonnull ->
       UncheckedNonnull
+  | LocallyCheckedNonnull, _ | _, LocallyCheckedNonnull ->
+      LocallyCheckedNonnull
   | StrictNonnull, StrictNonnull ->
       StrictNonnull
 
@@ -52,5 +60,7 @@ let to_string = function
       "Nullable"
   | UncheckedNonnull ->
       "UncheckedNonnull"
+  | LocallyCheckedNonnull ->
+      "LocallyCheckedNonnull"
   | StrictNonnull ->
       "StrictNonnull"

infer/src/nullsafe/Nullability.mli

@@ -22,6 +22,11 @@ type t =
       (** The type comes from a signature that is annotated (explicitly or implicitly according to
           conventions) as non-nullable. Hovewer, it might still contain null since the truthfullness
           of the declaration was not checked. *)
+  | LocallyCheckedNonnull
+      (** Non-nullable value that comes from a class checked under local mode. Local mode
+          type-checks files against its dependencies but does not require the dependencies to be
+          transitively checked. Therefore this type of non-nullable value is differentiated from
+          StrictNonnull. *)
   | StrictNonnull
       (** We believe that this value can not be null because it is either a non-null literal, an
           expression that semantically cannot be null, or a non-null value that should not be null
@@ -30,6 +35,8 @@ type t =
           programs. *)
 [@@deriving compare, equal]
 
+type pair = t * t [@@deriving compare, equal]
+
 val top : t
 (** The most generic type. *)
 

infer/src/nullsafe/NullsafeMode.ml

@@ -8,18 +8,89 @@
 open! IStd
 module F = Format
 
-type t = Default | Strict [@@deriving compare, equal]
+module Trust = struct
+  type t = All | Only of Typ.name list [@@deriving compare, equal]
+
+  let none = Only []
+
+  let extract_trust_list = function
+    | Annot.Array class_values ->
+        (* The only elements of this array can be class names; therefore short-circuit and return None if it's not the case. *)
+        IList.traverse_opt class_values ~f:(fun el ->
+            match el with Annot.Class class_typ -> Typ.name class_typ | _ -> None )
+    | _ ->
+        None
+
+
+  let of_annot annot =
+    let open IOption.Let_syntax in
+    let trust_all = Annot.find_parameter annot ~name:"trustAll" in
+    let* trust_list = Annot.find_parameter annot ~name:"value" in
+    let* trust_classes = extract_trust_list trust_list in
+    match trust_all with
+    | None ->
+        return none
+    | Some (Annot.Bool trust_all') ->
+        if trust_all' then return All else return (Only trust_classes)
+    | _ ->
+        None
+
+
+  let pp fmt t =
+    match t with
+    | All ->
+        F.fprintf fmt "all"
+    | Only [] ->
+        F.fprintf fmt "none"
+    | Only names ->
+        F.fprintf fmt "[%a]" (F.pp_print_list ~pp_sep:F.pp_print_space Typ.Name.pp) names
+end
+
+type t = Default | Local of Trust.t | Strict [@@deriving compare, equal]
+
+let pp fmt t =
+  match t with
+  | Default ->
+      F.fprintf fmt "Def"
+  | Strict ->
+      F.fprintf fmt "Strict"
+  | Local trust ->
+      F.fprintf fmt "Local(trust=%a)" Trust.pp trust
+
+
+let of_annot annot =
+  let open IOption.Let_syntax in
+  let* mode = Annot.find_parameter annot ~name:"value" in
+  match mode with
+  | Annot.Enum {value= "STRICT"} ->
+      return Strict
+  | Annot.Enum {value= "LOCAL"} -> (
+    match Annot.find_parameter annot ~name:"trustOnly" with
+    | None ->
+        (* When trustOnly values is missing, the default is in effect, which is Trust.All *)
+        return (Local Trust.All)
+    | Some (Annot.Annot trustOnly') ->
+        let* trust = Trust.of_annot trustOnly' in
+        return (Local trust)
+    | Some _ ->
+        None )
+  | _ ->
+      None
+
 
 let of_class tenv typ_name =
   match PatternMatch.type_name_get_annotation tenv typ_name with
-  | Some annots ->
-      if Annotations.ia_is_nullsafe_strict annots then Strict else Default
+  | Some annots -> (
+      if Annotations.ia_is_nullsafe_strict annots then Strict
+      else
+        match Annotations.ia_find_nullsafe annots with
+        | Some nullsafe_annot ->
+            Option.value_exn (of_annot nullsafe_annot)
+              ~message:"Unexpected change in @Nullsafe annotation format"
+        | _ ->
+            Default )
   | None ->
       Default
 
 
-let severity = function Strict -> Exceptions.Error | Default -> Exceptions.Warning
-
-let to_string = function Default -> " Def" | Strict -> "Strict"
-
-let pp fmt t = F.fprintf fmt "%s" (to_string t)
+let severity = function Strict | Local _ -> Exceptions.Error | Default -> Exceptions.Warning

infer/src/nullsafe/NullsafeMode.mli

@@ -9,7 +9,25 @@ open! IStd
 
 (** Represents a type-checking mode of nullsafe. *)
 
-type t = Default | Strict [@@deriving compare, equal]
+module Trust : sig
+  [@@@warning "-32"]
+
+  type t = All | Only of Typ.name list [@@deriving compare, equal]
+
+  val none : t
+
+  val of_annot : Annot.t -> t option
+  (** Returns [Trust.t] when provided annotation matches the format of [@TrustList], otherwise
+      [None]. *)
+
+  val pp : Format.formatter -> t -> unit
+end
+
+type t = Default | Local of Trust.t | Strict [@@deriving compare, equal]
+
+val of_annot : Annot.t -> t option
+  [@@warning "-32"]
+(** Returns [t] when provided annotation matches the format of [@Nullsafe], otherwise [None]. *)
 
 val of_class : Tenv.t -> Typ.name -> t
 (** Extracts mode information from class annotations *)

infer/src/nullsafe/eradicateChecks.ml

@@ -172,8 +172,8 @@ let is_declared_nonnull AnnotatedField.{annotated_type} =
   match annotated_type.nullability with
   | AnnotatedNullability.Nullable _ ->
       false
-  | AnnotatedNullability.UncheckedNonnull _ ->
-      true
+  | AnnotatedNullability.UncheckedNonnull _
+  | AnnotatedNullability.LocallyCheckedNonnull
   | AnnotatedNullability.StrictNonnull _ ->
       true
 

infer/src/nullsafe/typeOrigin.ml

@@ -129,7 +129,9 @@ let get_method_ret_description pname call_loc
     match nullability with
     | AnnotatedNullability.Nullable _ ->
         "nullable"
-    | AnnotatedNullability.UncheckedNonnull _ | AnnotatedNullability.StrictNonnull _ ->
+    | AnnotatedNullability.UncheckedNonnull _
+    | AnnotatedNullability.LocallyCheckedNonnull
+    | AnnotatedNullability.StrictNonnull _ ->
         "non-nullable"
   in
   let model_info =

infer/src/unit/IListTests.ml

@@ -23,7 +23,7 @@ let inputs =
   ; ("4", [4]) ]
 
 
-let tests =
+let inter_tests =
   let inter_test input1 input2 _ =
     let using_list = IList.inter ~cmp:Int.compare input1 input2 in
     let using_set =
@@ -31,9 +31,26 @@ let tests =
     in
     assert_equal using_list using_set
   in
-  let tests_ =
   List.concat_map inputs ~f:(fun (name1, input1) ->
       List.map inputs ~f:(fun (name2, input2) ->
           "inter_" ^ name1 ^ "_with_" ^ name2 >:: inter_test input1 input2 ) )
+
+
+let traverse_test =
+  let test_empty _ = assert_equal (Some []) (IList.traverse_opt [] ~f:(fun _ -> None)) in
+  let test_none _ = assert_equal None (IList.traverse_opt [42] ~f:(fun _ -> None)) in
+  let test_none_first _ =
+    assert_equal None (IList.traverse_opt [42; 43] ~f:(fun n -> Option.some_if (Int.equal n 43) n))
+  in
+  let test_none_last _ =
+    assert_equal None (IList.traverse_opt [42; 43] ~f:(fun n -> Option.some_if (Int.equal n 42) n))
   in
-  "IList_tests" >::: tests_
+  let test_some _ = assert_equal (Some [42; 43]) (IList.traverse_opt [42; 43] ~f:Option.some) in
+  [ "traverse_opt_empty" >:: test_empty
+  ; "traverse_opt_none" >:: test_none
+  ; "traverse_opt_none_first" >:: test_none_first
+  ; "traverse_opt_none_last" >:: test_none_last
+  ; "traverse_opt_some" >:: test_some ]
+
+
+let tests = "IList_tests" >::: inter_tests @ traverse_test

infer/tests/codetoanalyze/java/nullsafe-default/NullsafeMode.java

@@ -23,12 +23,28 @@ public class NullsafeMode {
     }
   }
 
-  class NonNullsafe extends VariousMethods {}
+  class NonNullsafe extends VariousMethods {
+    String OK_passUncheckedToLocal(String arg) {
+      return new TrustAllNullsafe().acceptVal(arg);
+    }
+
+    String OK_passUncheckedToStrictMode(String arg) {
+      return new NullsafeWithStrictMode().acceptVal(arg);
+    }
+
+    String OK_passUncheckedToStrict(String arg) {
+      return new StrictNullsafe().acceptVal(arg);
+    }
+  }
 
   class AnotherNonNullsafe extends VariousMethods {}
 
   @Nullsafe(Nullsafe.Mode.LOCAL)
   class TrustAllNullsafe extends VariousMethods {
+    public String acceptVal(String arg) {
+      return arg;
+    }
+
     String OK_returnFromAnyNonNullsafe() {
       String a = new NonNullsafe().returnVal();
       String b = new AnotherNonNullsafe().returnVal();
@@ -38,11 +54,24 @@ public class NullsafeMode {
     String BAD_returnNullFromNonNulsafe() {
       return (new NonNullsafe()).returnNull();
     }
+
+    String OK_passLocalToStrictMode(String arg) {
+      return new NullsafeWithStrictMode().acceptVal(arg);
+    }
+
+    String OK_passLocalToStrict(String arg) {
+      return new StrictNullsafe().acceptVal(arg);
+    }
   }
 
   @Nullsafe(value = Nullsafe.Mode.LOCAL, trustOnly = @Nullsafe.TrustList({NonNullsafe.class}))
   class TrustSomeNullsafe extends VariousMethods {
-    String OK_returnFromNonNullsafe() {
+    @Override
+    public String returnVal() {
+      return "OK";
+    }
+
+    String FP_OK_returnFromNonNullsafe() {
       return new NonNullsafe().returnVal();
     }
 
@@ -73,6 +102,15 @@ public class NullsafeMode {
 
   @Nullsafe(Nullsafe.Mode.STRICT)
   class NullsafeWithStrictMode extends VariousMethods {
+    @Override
+    public String returnVal() {
+      return "OK";
+    }
+
+    public String acceptVal(String arg) {
+      return arg;
+    }
+
     String BAD_returnFromNonStrict() {
       return new TrustNoneNullsafe().returnVal();
     }
@@ -84,6 +122,15 @@ public class NullsafeMode {
 
   @NullsafeStrict
   class StrictNullsafe extends VariousMethods {
+    @Override
+    public String returnVal() {
+      return "OK";
+    }
+
+    public String acceptVal(String arg) {
+      return arg;
+    }
+
     String BAD_returnFromNonNullsafe() {
       return new NonNullsafe().returnVal();
     }

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

@@ -147,11 +147,15 @@ codetoanalyze/java/nullsafe-default/NullMethodCall.java, codetoanalyze.java.null
 codetoanalyze/java/nullsafe-default/NullMethodCall.java, codetoanalyze.java.nullsafe_default.NullMethodCall.testSystemGetenvBad():int, 1, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, WARNING, [`envValue` is nullable and is not locally checked for null when calling `length()`: call to System.getenv(...) at line 240 (nullable according to nullsafe internal models).]
 codetoanalyze/java/nullsafe-default/NullMethodCall.java, codetoanalyze.java.nullsafe_default.NullMethodCall.withConditionalAssignemnt(codetoanalyze.java.nullsafe_default.NullMethodCall$AnotherI,boolean,java.lang.Object,java.lang.Object):void, 0, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, WARNING, [`i` is nullable and is not locally checked for null when calling `withObjectParameter(...)`.]
 codetoanalyze/java/nullsafe-default/NullMethodCall.java, codetoanalyze.java.nullsafe_default.NullMethodCall.withConjuction(codetoanalyze.java.nullsafe_default.NullMethodCall$AnotherI,boolean,boolean):void, 0, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, WARNING, [`i` is nullable and is not locally checked for null when calling `withBooleanParameter(...)`.]
-codetoanalyze/java/nullsafe-default/NullsafeMode.java, codetoanalyze.java.nullsafe_default.NullsafeMode$StrictNullsafe.BAD_returnFromNonNullsafe():java.lang.String, 0, ERADICATE_UNCHECKED_NONSTRICT_FROM_STRICT, no_bucket, ERROR, [`NullsafeMode$VariousMethods.returnVal()`: `@NullsafeStrict` mode prohibits using values coming from non-strict classes without a check. Result of this call is used at line 88. Either add a local check for null or assertion, or strictify NullsafeMode$VariousMethods.]
-codetoanalyze/java/nullsafe-default/NullsafeMode.java, codetoanalyze.java.nullsafe_default.NullsafeMode$StrictNullsafe.OK_returnFromNullsafeWithStrictMode():java.lang.String, 0, ERADICATE_UNCHECKED_NONSTRICT_FROM_STRICT, no_bucket, ERROR, [`NullsafeMode$VariousMethods.returnVal()`: `@NullsafeStrict` mode prohibits using values coming from non-strict classes without a check. Result of this call is used at line 92. Either add a local check for null or assertion, or strictify NullsafeMode$VariousMethods.]
-codetoanalyze/java/nullsafe-default/NullsafeMode.java, codetoanalyze.java.nullsafe_default.NullsafeMode$TrustAllNullsafe.BAD_returnNullFromNonNulsafe():java.lang.String, 0, ERADICATE_RETURN_NOT_NULLABLE, no_bucket, WARNING, [`BAD_returnNullFromNonNulsafe()`: return type is declared non-nullable but the method returns a nullable value: call to returnNull() at line 39.]
-codetoanalyze/java/nullsafe-default/NullsafeMode.java, codetoanalyze.java.nullsafe_default.NullsafeMode$TrustSomeNullsafe.BAD_returnNullFromNonNulsafe():java.lang.String, 0, ERADICATE_RETURN_NOT_NULLABLE, no_bucket, WARNING, [`BAD_returnNullFromNonNulsafe()`: return type is declared non-nullable but the method returns a nullable value: call to returnNull() at line 59.]
+codetoanalyze/java/nullsafe-default/NullsafeMode.java, codetoanalyze.java.nullsafe_default.NullsafeMode$NullsafeWithStrictMode.BAD_returnFromNonStrict():java.lang.String, 0, ERADICATE_UNCHECKED_USAGE_IN_NULLSAFE, no_bucket, ERROR, [`NullsafeMode$VariousMethods.returnVal()`: `@NullsafeStrict` mode prohibits using values coming from non-strict classes without a check. Result of this call is used at line 115. Either add a local check for null or assertion, or make NullsafeMode$VariousMethods nullsafe strict.]
+codetoanalyze/java/nullsafe-default/NullsafeMode.java, codetoanalyze.java.nullsafe_default.NullsafeMode$StrictNullsafe.BAD_returnFromNonNullsafe():java.lang.String, 0, ERADICATE_UNCHECKED_USAGE_IN_NULLSAFE, no_bucket, ERROR, [`NullsafeMode$VariousMethods.returnVal()`: `@NullsafeStrict` mode prohibits using values coming from non-strict classes without a check. Result of this call is used at line 135. Either add a local check for null or assertion, or make NullsafeMode$VariousMethods nullsafe strict.]
+codetoanalyze/java/nullsafe-default/NullsafeMode.java, codetoanalyze.java.nullsafe_default.NullsafeMode$TrustAllNullsafe.BAD_returnNullFromNonNulsafe():java.lang.String, 0, ERADICATE_RETURN_NOT_NULLABLE, no_bucket, ERROR, [`BAD_returnNullFromNonNulsafe()`: return type is declared non-nullable but the method returns a nullable value: call to returnNull() at line 55.]
+codetoanalyze/java/nullsafe-default/NullsafeMode.java, codetoanalyze.java.nullsafe_default.NullsafeMode$TrustNoneNullsafe.BAD_returnFromNonNullsafe():java.lang.String, 0, ERADICATE_UNCHECKED_USAGE_IN_NULLSAFE, no_bucket, ERROR, [`NullsafeMode$VariousMethods.returnVal()`: `@NullsafeLocal(trust=none)` mode prohibits using values coming from non-nullsafe classes without a check. Result of this call is used at line 95. Either add a local check for null or assertion, or make NullsafeMode$VariousMethods nullsafe.]
+codetoanalyze/java/nullsafe-default/NullsafeMode.java, codetoanalyze.java.nullsafe_default.NullsafeMode$TrustSomeNullsafe.BAD_returnFromAnotherNonNullsafe():java.lang.String, 0, ERADICATE_UNCHECKED_USAGE_IN_NULLSAFE, no_bucket, ERROR, [`NullsafeMode$VariousMethods.returnVal()`: `@NullsafeLocal(trust=none)` mode prohibits using values coming from non-nullsafe classes without a check. Result of this call is used at line 79. Either add a local check for null or assertion, or make NullsafeMode$VariousMethods nullsafe.]
+codetoanalyze/java/nullsafe-default/NullsafeMode.java, codetoanalyze.java.nullsafe_default.NullsafeMode$TrustSomeNullsafe.BAD_returnNullFromNonNulsafe():java.lang.String, 0, ERADICATE_RETURN_NOT_NULLABLE, no_bucket, ERROR, [`BAD_returnNullFromNonNulsafe()`: return type is declared non-nullable but the method returns a nullable value: call to returnNull() at line 88.]
+codetoanalyze/java/nullsafe-default/NullsafeMode.java, codetoanalyze.java.nullsafe_default.NullsafeMode$TrustSomeNullsafe.FP_OK_returnFromNonNullsafe():java.lang.String, 0, ERADICATE_UNCHECKED_USAGE_IN_NULLSAFE, no_bucket, ERROR, [`NullsafeMode$VariousMethods.returnVal()`: `@NullsafeLocal(trust=none)` mode prohibits using values coming from non-nullsafe classes without a check. Result of this call is used at line 75. Either add a local check for null or assertion, or make NullsafeMode$VariousMethods nullsafe.]
 codetoanalyze/java/nullsafe-default/NullsafeMode.java, codetoanalyze.java.nullsafe_default.NullsafeMode$TrustSomeNullsafe.OK_returnFromAnotherNonNullsafeAsNullable():java.lang.String, 0, ERADICATE_RETURN_OVER_ANNOTATED, no_bucket, WARNING, [Method `OK_returnFromAnotherNonNullsafeAsNullable()` is annotated with `@Nullable` but never returns null.]
+codetoanalyze/java/nullsafe-default/NullsafeMode.java, codetoanalyze.java.nullsafe_default.NullsafeMode$TrustSomeNullsafe.returnVal():java.lang.String, 0, ERADICATE_INCONSISTENT_SUBCLASS_PARAMETER_ANNOTATION, no_bucket, ERROR, [0th parameter `this` of method `NullsafeMode$TrustSomeNullsafe.returnVal()` is missing `@Nullable` declaration when overriding `NullsafeMode$VariousMethods.returnVal()`. The parent method declared it can handle `null` for this param, so the child should also declare that.]
 codetoanalyze/java/nullsafe-default/ParameterNotNullable.java, codetoanalyze.java.nullsafe_default.ParameterNotNullable$ConstructorCall.<init>(codetoanalyze.java.nullsafe_default.ParameterNotNullable,int), 0, ERADICATE_PARAMETER_NOT_NULLABLE, no_bucket, WARNING, [`ParameterNotNullable$ConstructorCall(...)`: parameter #2(`s`) is declared non-nullable but the argument is `null`.]
 codetoanalyze/java/nullsafe-default/ParameterNotNullable.java, codetoanalyze.java.nullsafe_default.ParameterNotNullable.callNull():void, 1, ERADICATE_PARAMETER_NOT_NULLABLE, no_bucket, WARNING, [`ParameterNotNullable.test(...)`: parameter #1(`s`) is declared non-nullable but the argument `s` is `null`: null constant at line 39.]
 codetoanalyze/java/nullsafe-default/ParameterNotNullable.java, codetoanalyze.java.nullsafe_default.ParameterNotNullable.callNullable(java.lang.String):void, 0, ERADICATE_PARAMETER_NOT_NULLABLE, no_bucket, WARNING, [`ParameterNotNullable.test(...)`: parameter #1(`s`) is declared non-nullable but the argument `s` is nullable.]
@@ -222,14 +226,14 @@ codetoanalyze/java/nullsafe-default/ReturnNotNullable.java, codetoanalyze.java.n
 codetoanalyze/java/nullsafe-default/ReturnNotNullable.java, codetoanalyze.java.nullsafe_default.ReturnNotNullable.return_null_in_catch_after_throw():java.lang.String, 0, ERADICATE_RETURN_NOT_NULLABLE, no_bucket, WARNING, [`return_null_in_catch_after_throw()`: return type is declared non-nullable but the method returns `null`: null constant at line 172.]
 codetoanalyze/java/nullsafe-default/ReturnNotNullable.java, codetoanalyze.java.nullsafe_default.ReturnNotNullable.tryWithResourcesReturnNullable(java.lang.String):java.lang.Object, 0, ERADICATE_RETURN_NOT_NULLABLE, no_bucket, WARNING, [`tryWithResourcesReturnNullable(...)`: return type is declared non-nullable but the method returns a nullable value: call to nullToNullableIsOK() at line 142.]
 codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.<init>(), 0, ERADICATE_FIELD_NOT_INITIALIZED, no_bucket, ERROR, [Field `notInitializedIsBAD` is declared non-nullable, so it should be initialized in the constructor or in an `@Initializer` method]
-codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_convertingNonnullToNonnullIsBad():java.lang.String, 0, ERADICATE_UNCHECKED_NONSTRICT_FROM_STRICT, no_bucket, ERROR, [`NonStrict.getNonnull()`: `@NullsafeStrict` mode prohibits using values coming from non-strict classes without a check. Result of this call is used at line 163. Either add a local check for null or assertion, or strictify NonStrict.]
+codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_convertingNonnullToNonnullIsBad():java.lang.String, 0, ERADICATE_UNCHECKED_USAGE_IN_NULLSAFE, no_bucket, ERROR, [`NonStrict.getNonnull()`: `@NullsafeStrict` mode prohibits using values coming from non-strict classes without a check. Result of this call is used at line 163. Either add a local check for null or assertion, or make NonStrict nullsafe strict.]
 codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_convertingNonnullToNullableIsOK():java.lang.String, 0, ERADICATE_RETURN_OVER_ANNOTATED, no_bucket, WARNING, [Method `nonStrictClass_convertingNonnullToNullableIsOK()` is annotated with `@Nullable` but never returns null.]
 codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_convertingNullableToNonnullIsBad():java.lang.String, 0, ERADICATE_RETURN_NOT_NULLABLE, no_bucket, ERROR, [`nonStrictClass_convertingNullableToNonnullIsBad()`: return type is declared non-nullable but the method returns a nullable value: call to getNullable() at line 137.]
 codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_dereferenceNonnullFieldAfterCheckIsOK():void, 1, ERADICATE_CONDITION_REDUNDANT, no_bucket, ADVICE, [The condition NonStrict.nonnull might be always true according to the existing annotations.]
-codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_dereferenceNonnullFieldIsBad():void, 0, ERADICATE_UNCHECKED_NONSTRICT_FROM_STRICT, no_bucket, ERROR, [`NonStrict.nonnull`: `@NullsafeStrict` mode prohibits using values coming from non-strict classes without a check. This field is used at line 133. Either add a local check for null or assertion, or strictify NonStrict.]
+codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_dereferenceNonnullFieldIsBad():void, 0, ERADICATE_UNCHECKED_USAGE_IN_NULLSAFE, no_bucket, ERROR, [`NonStrict.nonnull`: `@NullsafeStrict` mode prohibits using values coming from non-strict classes without a check. This field is used at line 133. Either add a local check for null or assertion, or make NonStrict nullsafe strict.]
 codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_dereferenceNonnullMethodAfterCheckIsOK():void, 1, ERADICATE_CONDITION_REDUNDANT, no_bucket, ADVICE, [The condition lang.String(o)V might be always true: `NonStrict.getNonnull()` is not annotated as `@Nullable`.]
-codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_dereferenceNonnullMethodIsBad():void, 0, ERADICATE_UNCHECKED_NONSTRICT_FROM_STRICT, no_bucket, ERROR, [`NonStrict.getNonnull()`: `@NullsafeStrict` mode prohibits using values coming from non-strict classes without a check. Result of this call is used at line 115. Either add a local check for null or assertion, or strictify NonStrict.]
-codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_dereferenceNonnullStaticMethodIsBad():void, 0, ERADICATE_UNCHECKED_NONSTRICT_FROM_STRICT, no_bucket, ERROR, [`NonStrict.staticNonnull()`: `@NullsafeStrict` mode prohibits using values coming from non-strict classes without a check. Result of this call is used at line 124. Either add a local check for null or assertion, or strictify NonStrict.]
+codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_dereferenceNonnullMethodIsBad():void, 0, ERADICATE_UNCHECKED_USAGE_IN_NULLSAFE, no_bucket, ERROR, [`NonStrict.getNonnull()`: `@NullsafeStrict` mode prohibits using values coming from non-strict classes without a check. Result of this call is used at line 115. Either add a local check for null or assertion, or make NonStrict nullsafe strict.]
+codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_dereferenceNonnullStaticMethodIsBad():void, 0, ERADICATE_UNCHECKED_USAGE_IN_NULLSAFE, no_bucket, ERROR, [`NonStrict.staticNonnull()`: `@NullsafeStrict` mode prohibits using values coming from non-strict classes without a check. Result of this call is used at line 124. Either add a local check for null or assertion, or make NonStrict nullsafe strict.]
 codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_dereferenceNullableFieldIsBad():void, 0, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, ERROR, [`__new(...).nullable` is nullable and is not locally checked for null when calling `toString()`.]
 codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_dereferenceNullableMethodIsBad():void, 0, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, ERROR, [`__new(...).getNullable()` is nullable and is not locally checked for null when calling `toString()`.]
 codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_dereferenceNullableStaticMethodIsBad():void, 0, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, ERROR, [`staticNullable()` is nullable and is not locally checked for null when calling `toString()`.]
@@ -242,7 +246,7 @@ codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe
 codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.strictClass_dereferenceNullableMethodIsBad():void, 0, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, ERROR, [`__new(...).getNullable()` is nullable and is not locally checked for null when calling `toString()`.]
 codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.strictClass_dereferenceNullableStaticMethodIsBad():void, 0, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, ERROR, [`staticNullable()` is nullable and is not locally checked for null when calling `toString()`.]
 codetoanalyze/java/nullsafe-default/StrictModeForThirdParty.java, codetoanalyze.java.nullsafe_default.StrictModeForThirdParty.dereferenceSpecifiedAsNullableIsBAD():void, 0, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, ERROR, [`StrictModeForThirdParty.obj.returnSpecifiedAsNullable()` is nullable and is not locally checked for null when calling `toString()`: call to ThirdPartyTestClass.returnSpecifiedAsNullable() at line 45 (declared nullable in nullsafe-default/third-party-signatures/some.test.pckg.sig at line 2).]
-codetoanalyze/java/nullsafe-default/StrictModeForThirdParty.java, codetoanalyze.java.nullsafe_default.StrictModeForThirdParty.dereferenceUnspecifiedIsBAD():void, 0, ERADICATE_UNVETTED_THIRD_PARTY_IN_STRICT, no_bucket, ERROR, [`ThirdPartyTestClass.returnUnspecified()`: `@NullsafeStrict` mode prohibits using values coming from not vetted third party methods without a check. Result of this call is used at line 41. Either add a local check for null or assertion, or add the correct signature to nullsafe-default/third-party-signatures/some.test.pckg.sig.]
+codetoanalyze/java/nullsafe-default/StrictModeForThirdParty.java, codetoanalyze.java.nullsafe_default.StrictModeForThirdParty.dereferenceUnspecifiedIsBAD():void, 0, ERADICATE_UNVETTED_THIRD_PARTY_IN_NULLSAFE, no_bucket, ERROR, [`ThirdPartyTestClass.returnUnspecified()`: `@NullsafeStrict` mode prohibits using values coming from not vetted third party methods without a check. Result of this call is used at line 41. Either add a local check for null or assertion, or add the correct signature to nullsafe-default/third-party-signatures/some.test.pckg.sig.]
 codetoanalyze/java/nullsafe-default/StrictModeForThirdParty.java, codetoanalyze.java.nullsafe_default.StrictModeForThirdParty.passingNullableParamToUnspecifiedIsBAD():void, 0, ERADICATE_PARAMETER_NOT_NULLABLE, no_bucket, ERROR, [Third-party `ThirdPartyTestClass.paramUnspecified(...)` is missing a signature that would allow passing a nullable to param #1(`param`). Actual argument `getNullable()` is nullable. Consider adding the correct signature of `ThirdPartyTestClass.paramUnspecified(...)` to nullsafe-default/third-party-signatures/some.test.pckg.sig.]
 codetoanalyze/java/nullsafe-default/StrictModeForThirdParty.java, codetoanalyze.java.nullsafe_default.StrictModeForThirdParty.passingNullableToParamSpecifiedAsNonnullIsBAD():void, 0, ERADICATE_PARAMETER_NOT_NULLABLE, no_bucket, ERROR, [`ThirdPartyTestClass.secondParamSpecifiedAsNonnull(...)`: parameter #2(`specifiedAsNonnull`) is declared non-nullable (see nullsafe-default/third-party-signatures/some.test.pckg.sig at line 3) but the argument `getNullable()` is nullable.]
 codetoanalyze/java/nullsafe-default/SwitchCase.java, codetoanalyze.java.nullsafe_default.SwitchCase.getNullableColor():codetoanalyze.java.nullsafe_default.Color, 0, ERADICATE_RETURN_OVER_ANNOTATED, no_bucket, WARNING, [Method `getNullableColor()` is annotated with `@Nullable` but never returns null.]