[nullsafe] Introduce Null nullability type

Summary:
This will allow us tune nullsafe behavior in a more fine-grained way.
See e.g. a follow up diff when we report errors more clearly.

Reviewed By: ngorogiannis

Differential Revision: D18683747

fbshipit-source-id: 7b5c42a03

infer/src/nullsafe/DereferenceRule.ml

@@ -17,7 +17,7 @@ type dereference_type =
 
 let check ~is_strict_mode nullability =
   match nullability with
-  | Nullability.Nullable ->
+  | Nullability.Nullable | Nullability.Null ->
       Error nullability
   | Nullability.DeclaredNonnull ->
       if is_strict_mode then Error nullability else Ok ()

infer/src/nullsafe/InferredNullability.ml

@@ -14,12 +14,10 @@ let create origin = {nullability= TypeOrigin.get_nullability origin; origin}
 let get_nullability {nullability} = nullability
 
 let is_nonnull_or_declared_nonnull {nullability} =
-  match nullability with Nullable -> false | DeclaredNonnull -> true | Nonnull -> true
+  match nullability with Nonnull | DeclaredNonnull -> true | _ -> false
 
 
-let is_nonnull {nullability} =
-  match nullability with Nullable -> false | DeclaredNonnull -> false | Nonnull -> true
-
+let is_nonnull {nullability} = match nullability with Nonnull -> true | _ -> false
 
 let to_string {nullability} = Printf.sprintf "[%s]" (Nullability.to_string nullability)
 
@@ -33,6 +31,10 @@ let join t1 t2 =
   *)
   let joined_origin =
     match (is_equal_to_t1, is_equal_to_t2) with
+    | _ when Nullability.equal t1.nullability Nullability.Null ->
+        t1.origin
+    | _ when Nullability.equal t2.nullability Nullability.Null ->
+        t2.origin
     | true, false ->
         (* Nullability was fully determined by t1. *)
         t1.origin

infer/src/nullsafe/Nullability.ml

@@ -8,6 +8,7 @@
 open! IStd
 
 type t =
+  | Null  (** The only possible value for that type is null *)
   | Nullable  (** No guarantees on the nullability *)
   | DeclaredNonnull
       (** The type comes from a signature that is annotated (explicitly or implicitly according to conventions)
@@ -24,6 +25,10 @@ let top = Nullable
 
 let join x y =
   match (x, y) with
+  | Null, Null ->
+      Null
+  | Null, _ | _, Null ->
+      Nullable
   | Nullable, _ | _, Nullable ->
       Nullable
   | DeclaredNonnull, _ | _, DeclaredNonnull ->
@@ -34,11 +39,9 @@ let join x y =
 
 let is_subtype ~subtype ~supertype = equal (join subtype supertype) supertype
 
-let is_strict_subtype ~subtype ~supertype =
-  is_subtype ~subtype ~supertype && not (equal subtype supertype)
-
-
 let to_string = function
+  | Null ->
+      "Null"
   | Nullable ->
       "Nullable"
   | DeclaredNonnull ->

infer/src/nullsafe/Nullability.mli

@@ -17,6 +17,7 @@ open! IStd
  *)
 
 type t =
+  | Null  (** The only possible value for that type is null *)
   | Nullable  (** No guarantees on the nullability *)
   | DeclaredNonnull
       (** The type comes from a signature that is annotated (explicitly or implicitly according to conventions)
@@ -36,9 +37,6 @@ val is_subtype : subtype:t -> supertype:t -> bool
 (** A is a subtype of B, if all values of A can be represented in B.
     Subtype relation is reflexive: everything is a subtype of itself. *)
 
-val is_strict_subtype : subtype:t -> supertype:t -> bool
-(** The same as subtype, but non-reflexive version. *)
-
 val join : t -> t -> t
 (** Unique upper bound over two types: the most precise type that is a supertype of both.
     Practically, joins occur e.g. when two branches of execution flow are getting merged. *)

infer/src/nullsafe/OverAnnotatedRule.ml

@@ -10,17 +10,18 @@ type violation = {declared_nullability: Nullability.t; can_be_narrowed_to: Nulla
 [@@deriving compare]
 
 let check ~what ~by_rhs_upper_bound =
-  if
-    Nullability.is_strict_subtype ~subtype:by_rhs_upper_bound ~supertype:what
-    && (* Suppress violations for anything apart from Nullable since such
-          issues are not very actionable and/or clear for the user.
-          E.g. we technically can suggest changing [DeclaredNonnull] to [Nonnull],
-          but in practice that requires strictification the code, which is a
-          separate effort.
-       *)
-    Nullability.equal what Nullable
-  then Error {declared_nullability= what; can_be_narrowed_to= by_rhs_upper_bound}
-  else Ok ()
+  match (what, by_rhs_upper_bound) with
+  | Nullability.Nullable, Nullability.Nonnull | Nullability.Nullable, Nullability.DeclaredNonnull ->
+      Error {declared_nullability= what; can_be_narrowed_to= by_rhs_upper_bound}
+  | Nullability.Null, Nullability.Nonnull | Nullability.Null, Nullability.DeclaredNonnull ->
+      (* Null, Nonnull pais is an edge case that we don't expect to arise in practice for two reasons:
+         1. The only way to declare something as Null is to declare it is java.lang.Void, but nullsafe
+         does not know about it just yet.
+         2. Even if it knew, such could should not compile: the only way it could compile if it returns `null` directly.
+      *)
+      Error {declared_nullability= what; can_be_narrowed_to= by_rhs_upper_bound}
+  | _ ->
+      Ok ()
 
 
 type violation_type =

infer/src/nullsafe/typeOrigin.ml

@@ -49,7 +49,7 @@ let equal = [%compare.equal: t]
 
 let get_nullability = function
   | NullConst _ ->
-      Nullability.Nullable
+      Nullability.Null
   | NonnullConst _
   | This (* `this` can not be null according to Java rules *)
   | New (* In Java `new` always create a non-null object  *)