[nullsafe] Trust explicitly annotated third party in all modes

Summary:
For Mode.Local this is kind of obvious decision.
But this diff does the same for strict mode as well.
See comment in [ExplicitNonnullThirdParty] for the detailed explanation.

Reviewed By: artempyanykh

Differential Revision: D20140056

fbshipit-source-id: 13c66df81

infer/src/nullsafe/AnnotatedNullability.ml

@@ -24,30 +24,20 @@ type t =
 [@@deriving compare]
 
 and nullable_origin =
-  | AnnotatedNullable  (** The type is expicitly annotated with [@Nullable] in the code *)
+  | AnnotatedNullable
   | AnnotatedPropagatesNullable
-      (** If a function param is annotated as [@PropagatesNullable], this param is automatically
-          nullable *)
   | HasPropagatesNullableInParam
-      (** If a method has at least one param marked as [@PropagatesNullable], return value is
-          automatically nullable *)
-  | ModelledNullable  (** nullsafe knows it is nullable via its internal models *)
+  | ModelledNullable
 [@@deriving compare]
 
-and unchecked_nonnull_origin =
-  | AnnotatedNonnull
-      (** The type is explicitly annotated as non nullable via one of nonnull annotations Nullsafe
-          recognizes *)
-  | ImplicitlyNonnull
-      (** Infer was run in mode where all not annotated (non local) types are treated as non
-          nullable *)
+and unchecked_nonnull_origin = AnnotatedNonnull | ImplicitlyNonnull
 
 and strict_nonnull_origin =
-  | ModelledNonnull  (** nullsafe knows it is non-nullable via its internal models *)
-  | StrictMode  (** under strict mode we consider non-null declarations to be trusted *)
-  | PrimitiveType  (** Primitive types are non-nullable by language design *)
+  | ExplicitNonnullThirdParty
+  | ModelledNonnull
+  | StrictMode
+  | PrimitiveType
   | EnumValue
-      (** Java enum value are statically initialized with non-nulls according to language semantics *)
 [@@deriving compare]
 
 let get_nullability = function
@@ -80,6 +70,8 @@ let pp fmt t =
   in
   let string_of_nonnull_origin nonnull_origin =
     match nonnull_origin with
+    | ExplicitNonnullThirdParty ->
+        "explicit3p"
     | ModelledNonnull ->
         "model"
     | StrictMode ->
@@ -105,20 +97,36 @@ let pp fmt t =
 let of_type_and_annotation ~is_trusted_callee ~nullsafe_mode ~is_third_party typ annotations =
   if not (PatternMatch.type_is_class typ) then StrictNonnull PrimitiveType
   else if Annotations.ia_is_nullable annotations then
+    (* Explicitly nullable always means Nullable *)
     let nullable_origin =
       if Annotations.ia_is_propagates_nullable annotations then AnnotatedPropagatesNullable
       else AnnotatedNullable
     in
     Nullable nullable_origin
   else
+    (* Lack of nullable annotation means non-nullish case, lets specify which exactly. *)
     match nullsafe_mode with
     | NullsafeMode.Strict ->
+        (* In strict mode, not annotated with nullable means non-nullable *)
         StrictNonnull StrictMode
     | NullsafeMode.Local _ ->
+        (* In local mode, not annotated with nullable means non-nullable *)
         LocallyCheckedNonnull
     | NullsafeMode.Default ->
-        if is_third_party then ThirdPartyNonnull
+        (* In default mode, agreements for "not [@Nullable]" depend on where code comes from *)
+        if is_third_party then
+          if Annotations.ia_is_nonnull annotations then
+            (* Third party method explicitly marked as [@Nonnull].
+               This is considered strict - see documentation to [ExplicitNonnullThirdParty]
+               **)
+            StrictNonnull ExplicitNonnullThirdParty
+          else
+            (* Third party might not obey "not annotated hence not nullable" convention.
+               Hence by default we treat is with low level of trust.
+            *)
+            ThirdPartyNonnull
         else
+          (* For non third party code, the agreement is "not annotated with [@Nullable] hence not null" *)
           let preliminary_nullability =
             if Annotations.ia_is_nonnull annotations then UncheckedNonnull AnnotatedNonnull
             else UncheckedNonnull ImplicitlyNonnull

infer/src/nullsafe/AnnotatedNullability.mli

@@ -45,6 +45,16 @@ and unchecked_nonnull_origin =
           nullable *)
 
 and strict_nonnull_origin =
+  | ExplicitNonnullThirdParty
+      (** Third party annotated as [@Nonnull] is considered strict. This is a controversial choice
+          and might be an unsoundness issue. The reason is practical. The best we can do for third
+          party is to register it in third party signature repository. Though this typically
+          requires human review, in practice errors are inevitable. On the other hand, if the
+          library owner explicitly annotated a function as nonnull, we assume this was made for
+          reason. In practice, requiring such methods to be registered in third party folder, will
+          introduce user friction but will not significantly increase safety. So our approach here
+          is optimistic. If some particular method or library is known to contain wrong [@Nonnull]
+          annotations, third party repository is a way to override this. *)
   | ModelledNonnull  (** nullsafe knows it is non-nullable via its internal models *)
   | StrictMode  (** under strict mode we consider non-null declarations to be trusted *)
   | PrimitiveType  (** Primitive types are non-nullable by language design *)

infer/src/nullsafe/AssignmentRule.ml

@@ -69,6 +69,7 @@ let mk_description_for_bad_param_passed
   let nullability_evidence_as_suffix =
     Option.value_map nullability_evidence ~f:(fun evidence -> ": " ^ evidence) ~default:""
   in
+  let annotated_param_nullability = param_signature.param_annotated_type.nullability in
   let module MF = MarkupFormatter in
   let argument_description =
     if String.equal actual_param_expression "null" then "is `null`"
@@ -86,35 +87,39 @@ let mk_description_for_bad_param_passed
       in
       Format.asprintf "%a is %s" MF.pp_monospaced actual_param_expression nullability_descr
   in
-  let suggested_file_to_add_third_party =
-    match model_source with
-    | None ->
-        ThirdPartyAnnotationInfo.lookup_related_sig_file_for_proc
-          (ThirdPartyAnnotationGlobalRepo.get_repo ())
-          function_procname
-    | Some _ ->
-        (* This is a different case:
-           suggestion to add third party is irrelevant (it is already added or modelled internally).
-        *)
-        None
-  in
-  match suggested_file_to_add_third_party with
-  | Some sig_file_name ->
+  match AnnotatedNullability.get_nullability annotated_param_nullability with
+  | Nullability.Null ->
+      Logging.die Logging.InternalError "Unexpected param nullability: Null"
+  | Nullability.Nullable ->
+      Logging.die Logging.InternalError "Passing anything to a nullable param should be allowed"
+  | Nullability.ThirdPartyNonnull ->
       (* 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.
          So we phrase it differently to remain truthful, but as specific as possible.
       *)
+      let suggested_third_party_sig_file =
+        ThirdPartyAnnotationInfo.lookup_related_sig_file_for_proc
+          (ThirdPartyAnnotationGlobalRepo.get_repo ())
+          function_procname
+      in
+      let where_to_add_signature =
+        Option.value_map suggested_third_party_sig_file
+          ~f:(fun sig_file_name ->
+            ThirdPartyAnnotationGlobalRepo.get_user_friendly_third_party_sig_file_name
+              ~filename:sig_file_name )
+            (* this can happen when third party is registered in a deprecated way (not in third party repository) *)
+          ~default:"the third party signature storage"
+      in
       let procname_str = Procname.to_simplified_string ~withclass:true function_procname in
       Format.asprintf
         "Third-party %a is missing a signature that would allow passing a nullable to param #%d%a. \
          Actual argument %s%s. Consider adding the correct signature of %a to %s."
         MF.pp_monospaced procname_str param_position pp_param_name param_signature.mangled
         argument_description nullability_evidence_as_suffix MF.pp_monospaced procname_str
-        (ThirdPartyAnnotationGlobalRepo.get_user_friendly_third_party_sig_file_name
-           ~filename:sig_file_name)
-  | None ->
+        where_to_add_signature
+  | Nullability.LocallyCheckedNonnull | Nullability.UncheckedNonnull | Nullability.StrictNonnull ->
       let nonnull_evidence =
         match model_source with
         | None ->

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

@@ -213,5 +213,13 @@ public class NullsafeMode {
     UncheckedParams BAD_passThirdPartyToUnchecked() {
       return new UncheckedParams(ThirdPartyTestClass.getUncheckedLong(42));
     }
+
+    void BAD_dereferenceNotAnnotatedThirdParty() {
+      (new ThirdPartyTestClass()).returnUnspecified().toString();
+    }
+
+    void OK_dereferenceExplicitlyAnnotatedThirdParty() {
+      (new ThirdPartyTestClass()).returnExplicitlyAnnotated().toString();
+    }
   }
 }

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

@@ -152,6 +152,7 @@ codetoanalyze/java/nullsafe-default/NullMethodCall.java, codetoanalyze.java.null
 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$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 175. 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_dereferenceNotAnnotatedThirdParty():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 218. 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/NullsafeMode.java, codetoanalyze.java.nullsafe_default.NullsafeMode$StrictNullsafe.BAD_passThirdPartyToUnchecked():codetoanalyze.java.nullsafe_default.NullsafeMode$UncheckedParams, 0, ERADICATE_UNVETTED_THIRD_PARTY_IN_NULLSAFE, no_bucket, ERROR, [`ThirdPartyTestClass.getUncheckedLong(...)`: `@NullsafeStrict` mode prohibits using values coming from not vetted third party methods without a check. Result of this call is used at line 214. 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/NullsafeMode.java, codetoanalyze.java.nullsafe_default.NullsafeMode$StrictNullsafe.BAD_returnFromNonNullsafe():java.lang.String, 0, ERADICATE_UNCHECKED_USAGE_IN_NULLSAFE, no_bucket, ERROR, [`NullsafeMode$NonNullsafe.returnVal()`: `@NullsafeStrict` mode prohibits using values coming from non-strict classes without a check. Result of this call is used at line 198. Either add a local check for null or assertion, or make NullsafeMode$NonNullsafe nullsafe strict.]
 codetoanalyze/java/nullsafe-default/NullsafeMode.java, codetoanalyze.java.nullsafe_default.NullsafeMode$TrustAllNullsafe.BAD_passThirdPartyToUnchecked():codetoanalyze.java.nullsafe_default.NullsafeMode$UncheckedParams, 0, ERADICATE_UNVETTED_THIRD_PARTY_IN_NULLSAFE, no_bucket, ERROR, [`ThirdPartyTestClass.getUncheckedLong(...)`: `@NullsafeLocal(trust=all)` mode prohibits using values coming from not vetted third party methods without a check. Result of this call is used at line 113. Either add a local check for null or assertion, or add the correct signature to nullsafe-default/third-party-signatures/some.test.pckg.sig.]

infer/tests/codetoanalyze/java/nullsafe-default/third-party-test-code/some/test/pckg/ThirdPartyTestClass.java

@@ -6,6 +6,7 @@
  */
 package some.test.pckg;
 
+import javax.annotation.Nonnull;
 import javax.annotation.Nullable;
 
 /**
@@ -40,6 +41,10 @@ public class ThirdPartyTestClass {
 
   // Return values.
 
+  public @Nonnull String returnExplicitlyAnnotated() {
+    return "";
+  }
+
   // No information in 3rd party repo
   public String returnUnspecified() {
     return "";