[nullsafe] Model nullability of special enum methods

Summary:
These 2 methods are automatically supplied for all enums, with
predefined behavior and nullability: https://www.geeksforgeeks.org/enum-in-java/

(Note that they are not part of java.lang.Enum class).

This will allow using them in unvetted third part and under strict mode.

Reviewed By: artempyanykh

Differential Revision: D21501716

fbshipit-source-id: 104082d15

infer/src/nullsafe/models.ml

@@ -44,6 +44,24 @@ let to_modelled_nullability ThirdPartyMethod.{ret_nullability; param_nullability
   (is_nullable ret_nullability, List.map param_nullability ~f:is_nullable)
 
 
+(* Some methods *)
+let get_special_method_modelled_nullability tenv proc_name =
+  let open IOption.Let_syntax in
+  let* class_name = Procname.get_class_type_name proc_name in
+  if PatternMatch.is_java_enum tenv class_name then
+    match (Procname.get_method proc_name, Procname.get_parameters proc_name) with
+    (* values() is a synthetic enum method that is never null *)
+    | "values", [] ->
+        Some (false, [])
+    (* valueOf() is a synthetic enum method that is never null *)
+    | "valueOf", [Procname.Parameter.JavaParameter param_type_name]
+      when JavaSplitName.equal param_type_name JavaSplitName.java_lang_string ->
+        Some (false, [false])
+    | _ ->
+        None
+  else None
+
+
 (** Return the annotated signature of the procedure, taking into account models. External models
     take precedence over internal ones. *)
 let get_modelled_annotated_signature ~is_callee_in_trust_list tenv proc_attributes =
@@ -55,11 +73,16 @@ let get_modelled_annotated_signature ~is_callee_in_trust_list tenv proc_attribut
   let proc_id = Procname.to_unique_id proc_name in
   (* Look in the infer internal models *)
   let correct_by_internal_models ann_sig =
-    try
+    let modelled_nullability =
-      let modelled_nullability = Hashtbl.find annotated_table_nullability proc_id in
+      (* Look at internal model tables *)
-      AnnotatedSignature.set_modelled_nullability proc_name ann_sig InternalModel
+      Hashtbl.find_opt annotated_table_nullability proc_id
-        modelled_nullability
+      (* Maybe it is a special method whose nullability is predefined *)
-    with Caml.Not_found -> ann_sig
+      |> IOption.if_none_evalopt ~f:(fun () ->
+             get_special_method_modelled_nullability tenv proc_name )
+    in
+    Option.value_map modelled_nullability
+      ~f:(AnnotatedSignature.set_modelled_nullability proc_name ann_sig InternalModel)
+      ~default:ann_sig
   in
   (* Look at external models *)
   let correct_by_external_models ann_sig =

infer/tests/codetoanalyze/java/nullsafe/StrictMode.java

@@ -158,6 +158,16 @@ class Strict {
     return SomeEnum.FAKE_VALUE; // should not be able to convert to nonnull
   }
 
+  private SomeEnum[] enumValuesIsNonnullable() {
+    // values() is a special enum method which is never nullable
+    return SomeEnum.values();
+  }
+
+  private SomeEnum enumValueOfIsNonnullable() {
+    // valueOf() is a special enum method which is never nullable
+    return SomeEnum.valueOf("this will throw but won't return null");
+  }
+
   private String nonStrictClass_convertingNonnullToNonnullIsBad() {
     // even that it is declared as nonnull, can not convert it to nonnull it without checking before
     return (new NonStrict()).getNonnull();

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

@@ -316,11 +316,11 @@ codetoanalyze/java/nullsafe/ReturnNotNullable.java, codetoanalyze.java.nullsafe_
 codetoanalyze/java/nullsafe/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/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/StrictMode.java, Linters_dummy_method, 15, ERADICATE_META_CLASS_NEEDS_IMPROVEMENT, no_bucket, INFO, [], Strict, codetoanalyze.java.nullsafe_default, issues: 17, curr_mode: "Strict"
-codetoanalyze/java/nullsafe/StrictMode.java, Linters_dummy_method, 221, ERADICATE_META_CLASS_IS_NULLSAFE, no_bucket, INFO, [], OtherStrict, codetoanalyze.java.nullsafe_default, issues: 0, curr_mode: "Strict"
+codetoanalyze/java/nullsafe/StrictMode.java, Linters_dummy_method, 231, ERADICATE_META_CLASS_IS_NULLSAFE, no_bucket, INFO, [], OtherStrict, codetoanalyze.java.nullsafe_default, issues: 0, curr_mode: "Strict"
-codetoanalyze/java/nullsafe/StrictMode.java, Linters_dummy_method, 242, ERADICATE_META_CLASS_CAN_BE_NULLSAFE, no_bucket, ADVICE, [Congrats! `NonStrict` is free of nullability issues. Mark it `@Nullsafe(Nullsafe.Mode.LOCAL)` to prevent regressions.], NonStrict, codetoanalyze.java.nullsafe_default, issues: 0, curr_mode: "Default", promote_mode: "LocalTrustAll"
+codetoanalyze/java/nullsafe/StrictMode.java, Linters_dummy_method, 252, ERADICATE_META_CLASS_CAN_BE_NULLSAFE, no_bucket, ADVICE, [Congrats! `NonStrict` is free of nullability issues. Mark it `@Nullsafe(Nullsafe.Mode.LOCAL)` to prevent regressions.], NonStrict, codetoanalyze.java.nullsafe_default, issues: 0, curr_mode: "Default", promote_mode: "LocalTrustAll"
-codetoanalyze/java/nullsafe/StrictMode.java, Linters_dummy_method, 267, ERADICATE_META_CLASS_NEEDS_IMPROVEMENT, no_bucket, INFO, [], SomeEnum, codetoanalyze.java.nullsafe_default, issues: 0, curr_mode: "Default"
+codetoanalyze/java/nullsafe/StrictMode.java, Linters_dummy_method, 277, ERADICATE_META_CLASS_NEEDS_IMPROVEMENT, no_bucket, INFO, [], SomeEnum, codetoanalyze.java.nullsafe_default, issues: 0, curr_mode: "Default"
 codetoanalyze/java/nullsafe/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/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_convertingNonnullToNonnullIsBad():java.lang.String, 2, 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 161. Either add a local check for null or assertion, or make `NonStrict` nullsafe strict.]
+codetoanalyze/java/nullsafe/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_convertingNonnullToNonnullIsBad():java.lang.String, 2, 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 171. Either add a local check for null or assertion, or make `NonStrict` nullsafe strict.]
 codetoanalyze/java/nullsafe/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_convertingNonnullToNullableIsOK():java.lang.String, 0, ERADICATE_RETURN_OVER_ANNOTATED, no_bucket, ADVICE, [Method `nonStrictClass_convertingNonnullToNullableIsOK()` is annotated with `@Nullable` but never returns null.]
 codetoanalyze/java/nullsafe/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/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_dereferenceNonnullFieldAfterCheckIsOK():void, 2, ERADICATE_CONDITION_REDUNDANT, no_bucket, ADVICE, [The condition NonStrict.nonnull might be always true according to the existing annotations.]