[nullsafe] Enum values can be used as non-null without strictification

Summary:
According to Java semantics, they are always non-null.
Internally they are represented as static fields, so they have
DeclaredNonnull nullability, which means NullsafeStrict mode would
refuse to use them without strictification.

Lets teach nullsafe that these guys are non-nullables.

See also FN in test case.

Reviewed By: ngorogiannis

Differential Revision: D19024547

fbshipit-source-id: 8c120fa50

infer/src/IR/Typ.ml

@@ -1566,6 +1566,8 @@ module Struct = struct
 
   (** If a struct type with field f, return the type of f. If not, return the default *)
   let fld_typ ~lookup ~default fn (typ : T.t) =
+    (* Note: would be nice migrate it to get_field_info
+       (for that one needs to ensure adding Tptr to pattern match does not break thing) *)
     match typ.desc with
     | Tstruct name -> (
       match lookup name with
@@ -1578,20 +1580,37 @@ module Struct = struct
         default
 
 
-  let get_field_type_and_annotation ~lookup fn (typ : T.t) =
+  type field_info = {typ: typ; annotations: Annot.Item.t; is_static: bool}
+
+  let find_field field_list field_name_to_lookup =
+    List.find_map
+      ~f:(fun (field_name, typ, annotations) ->
+        if Fieldname.equal field_name field_name_to_lookup then Some (typ, annotations) else None )
+      field_list
+
+
+  let get_field_info ~lookup field_name_to_lookup (typ : T.t) =
+    let find_field_info field_list ~is_static =
+      find_field field_list field_name_to_lookup
+      |> Option.map ~f:(fun (typ, annotations) -> {typ; annotations; is_static})
+    in
     match typ.desc with
     | Tstruct name | Tptr ({desc= Tstruct name}, _) -> (
       match lookup name with
-      | Some {fields; statics} ->
+      | Some {fields= non_statics; statics} ->
-          List.find_map
+          (* Search in both lists and return the first found *)
-            ~f:(fun (f, t, a) ->
+          find_field_info statics ~is_static:true
-              match Fieldname.equal f fn with true -> Some (t, a) | false -> None )
+          |> IOption.if_none_evalopt ~f:(fun () -> find_field_info non_statics ~is_static:false)
-            (fields @ statics)
       | None ->
           None )
     | _ ->
         None
 
 
+  let get_field_type_and_annotation ~lookup field_name_to_lookup typ =
+    get_field_info ~lookup field_name_to_lookup typ
+    |> Option.map ~f:(fun {typ; annotations} -> (typ, annotations))
+
+
   let is_dummy {dummy} = dummy
 end

infer/src/IR/Typ.mli

@@ -711,6 +711,11 @@ module Struct : sig
   val get_extensible_array_element_typ : lookup:lookup -> typ -> typ option
   (** the element typ of the final extensible array in the given typ, if any *)
 
+  type field_info = {typ: typ; annotations: Annot.Item.t; is_static: bool}
+
+  val get_field_info : lookup:lookup -> Fieldname.t -> typ -> field_info option
+  (** Lookup for info associated with the field [fn]. None if [typ] has no field named [fn] *)
+
   val fld_typ : lookup:lookup -> default:typ -> Fieldname.t -> typ -> typ
   (** If a struct type with field f, return the type of f.
       If not, return the default type if given, otherwise raise an exception *)

infer/src/absint/PatternMatch.ml

@@ -416,6 +416,8 @@ let get_fields_nullified procdesc =
 (** Checks if the class name is a Java exception *)
 let is_throwable tenv typename = is_subtype_of_str tenv typename "java.lang.Throwable"
 
+let is_java_enum tenv typename = is_subtype_of_str tenv typename "java.lang.Enum"
+
 (** tests whether any class attributes (e.g., [@ThreadSafe]) pass check of first argument, including
     for supertypes*)
 let check_class_attributes check tenv = function

infer/src/absint/PatternMatch.mli

@@ -136,6 +136,9 @@ val get_fields_nullified : Procdesc.t -> Typ.Fieldname.Set.t
 val is_throwable : Tenv.t -> Typ.Name.t -> bool
 (** [is_throwable tenv class_name] checks if class_name is of type java.lang.Throwable *)
 
+val is_java_enum : Tenv.t -> Typ.Name.t -> bool
+(** Checks if the type is Java enum (extends java.lang.Enum) *)
+
 val check_class_attributes : (Annot.Item.t -> bool) -> Tenv.t -> Typ.Procname.t -> bool
 (** tests whether any class attributes (e.g., [@ThreadSafe]) pass check of first argument, including
     supertypes*)

infer/src/nullsafe/AnnotatedField.ml

@@ -20,17 +20,50 @@ let is_class_in_strict_mode tenv typ =
       false
 
 
-let get tenv fn typ =
+let rec get_type_name {Typ.desc} =
+  match desc with Typ.Tstruct name -> Some name | Typ.Tptr (t, _) -> get_type_name t | _ -> None
+
+
+(* A heuristic to guess if the field is actually a Java enum value. *)
+let is_enum_value tenv ~class_typ (field_info : Typ.Struct.field_info) =
+  (* It is tricky to get this information with 100% precision, but this works in most of
+     practical cases.
+     In Java, enums are special classes, and enum values are (implicitly generated) static fields in these classes,
+     which are initialized statically via calling the class constructor.
+     Though there can be OTHER (user-defined) static fields in the same enum class,
+     this is a rare case.*)
+  if not field_info.is_static then false
+  else
+    match (get_type_name class_typ, get_type_name field_info.typ) with
+    (* enums values are fields which type is the same as the type of the enum class *)
+    | Some class_name, Some field_type_name
+      when Typ.equal_name class_name field_type_name && PatternMatch.is_java_enum tenv class_name ->
+        true
+    (* Could not fetch one of the class names, or they are different. Should not happen for enum values. *)
+    | _ ->
+        false
+
+
+let get tenv field_name class_typ =
   let lookup = Tenv.lookup tenv in
   (* We currently don't support field-level strict mode annotation, so fetch it from class *)
-  let is_strict_mode = is_class_in_strict_mode tenv typ in
+  let is_strict_mode = is_class_in_strict_mode tenv class_typ in
-  let type_and_annotation_to_field_type (typ, annotation) =
+  Typ.Struct.get_field_info ~lookup field_name class_typ
-    { annotation_deprecated= annotation
+  |> Option.map ~f:(fun (Typ.Struct.{typ= field_typ; annotations} as field_info) ->
-    ; annotated_type=
+         let is_enum_value = is_enum_value tenv ~class_typ field_info in
-        AnnotatedType.
+         let nullability =
-          { nullability= AnnotatedNullability.of_type_and_annotation typ annotation ~is_strict_mode
+           AnnotatedNullability.of_type_and_annotation field_typ annotations ~is_strict_mode
-          ; typ } }
+         in
-  in
+         let corrected_nullability =
-  Option.map
+           match nullability with
-    (Typ.Struct.get_field_type_and_annotation ~lookup fn typ)
+           | AnnotatedNullability.DeclaredNonnull _ when is_enum_value ->
-    ~f:type_and_annotation_to_field_type
+               (* Enum values are the special case - they can not be null. So we can strengten nullability.
+                  Note that if it is nullable, we do NOT change nullability: in this case this is probably
+                  not an enum value, but just a static field annotated as nullable.
+               *)
+               AnnotatedNullability.Nonnull EnumValue
+           | _ ->
+               nullability
+         in
+         let annotated_type = AnnotatedType.{nullability= corrected_nullability; typ= field_typ} in
+         {annotation_deprecated= annotations; annotated_type} )

infer/src/nullsafe/AnnotatedNullability.ml

@@ -43,6 +43,8 @@ and 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 *)
+  | EnumValue
+      (** Java enum value are statically initialized with non-nulls according to language semantics *)
 [@@deriving compare]
 
 let get_nullability = function
@@ -77,6 +79,8 @@ let pp fmt t =
         "strict"
     | PrimitiveType ->
         "primitive"
+    | EnumValue ->
+        "enum"
   in
   match t with
   | Nullable origin ->

infer/src/nullsafe/AnnotatedNullability.mli

@@ -45,6 +45,8 @@ and 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 *)
+  | EnumValue
+      (** Java enum value are statically initialized with non-nulls according to language semantics *)
 [@@deriving compare]
 
 val get_nullability : t -> Nullability.t

infer/src/nullsafe/typeOrigin.ml

@@ -78,9 +78,7 @@ let rec to_string = function
   | NonnullConst _ ->
       "Const (nonnull)"
   | Field {object_origin; field_name} ->
-      "Field "
+      "Field " ^ Typ.Fieldname.to_string field_name ^ " (object: " ^ to_string object_origin ^ ")"
-      ^ Typ.Fieldname.to_simplified_string field_name
-      ^ " (object: " ^ to_string object_origin ^ ")"
   | MethodParameter {mangled; param_annotated_type= {nullability}} ->
       Format.asprintf "Param %s <%a>" (Mangled.to_string mangled) AnnotatedNullability.pp
         nullability

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

@@ -141,6 +141,21 @@ class Strict {
     return NonStrict.getPrimitiveTypeValue();
   }
 
+  // We don't require strictifying enums: their values are non-nullables
+  private SomeEnum usingEnumValuesAsNonnullIsOK() {
+    String str = SomeEnum.FIRST_VALUE.toString(); // can dereference
+    SomeEnum.FIRST_VALUE.someMethod(); // can dereference via calling a enum-specific method
+    return SomeEnum.SECOND_VALUE; // can convert to nonnull
+  }
+
+  // FAKE_VALUE is not a value, but just a static fields so should require strictification
+  // (but it does not)
+  private SomeEnum FN_usingNonStrictifiedStaticFieldsInEnumsShouldBeBad() {
+    String str = SomeEnum.FAKE_VALUE.toString(); // should not be able to dereference
+    SomeEnum.FAKE_VALUE.someMethod(); // should not be able to dereference
+    return SomeEnum.FAKE_VALUE; // should not be able to convert to nonnull
+  }
+
   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();
@@ -246,3 +261,15 @@ class NonStrict {
     return 0;
   }
 }
+
+enum SomeEnum {
+  FIRST_VALUE,
+  SECOND_VALUE;
+
+  public void someMethod() {}
+
+  // We currently have no way to distinct that guy from enum value.
+  // Using it will lead to NPE, but we won't detect it
+  // This should not occur in practice often, hopefully :)
+  public static SomeEnum FAKE_VALUE;
+}

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

@@ -216,7 +216,7 @@ codetoanalyze/java/nullsafe-default/ReturnNotNullable.java, codetoanalyze.java.n
 codetoanalyze/java/nullsafe-default/ReturnNotNullable.java, codetoanalyze.java.nullsafe_default.ReturnNotNullable.return_null_in_catch():java.lang.String, 0, ERADICATE_RETURN_NOT_NULLABLE, no_bucket, WARNING, [`return_null_in_catch()`: return type is declared non-nullable but the method returns `null`: null constant at line 160.]
 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.nonStrictClass_convertingNonnullToNonnullIsBad():java.lang.String, 2, ERADICATE_UNCHECKED_NONSTRICT_FROM_STRICT, no_bucket, WARNING, [`NonStrict.getNonnull()`: `@NullsafeStrict` mode prohibits using values coming from non-strict classes without a check. Result of this call is used at line 144. 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, 2, ERADICATE_UNCHECKED_NONSTRICT_FROM_STRICT, no_bucket, WARNING, [`NonStrict.getNonnull()`: `@NullsafeStrict` mode prohibits using values coming from non-strict classes without a check. Result of this call is used at line 159. Either add a local check for null or assertion, or strictify NonStrict.]
 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, WARNING, [`nonStrictClass_convertingNullableToNonnullIsBad()`: return type is declared non-nullable but the method returns a nullable value: call to getNullable() at line 135.]
 codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_dereferenceNonnullFieldAfterCheckIsOK():void, 2, ERADICATE_CONDITION_REDUNDANT, no_bucket, WARNING, [The condition NonStrict.nonnull is always true according to the existing annotations.]