[nullsafe] Introduce Nullability module and make NullsafeRules use it

Summary:
In previous refactoring stages, we operated on AnnotatedNullability
(nullability of a field or method signature together with its origin),
and InferredNullability (nullability of a value in typestate together
with its origin).

Now it is time to extract common Nullability as a type system concept,
together with `<:` and `join` functionality. This was sketched in
`NullsafeRules`, so this diff consolidates this as well.

In follow up diffs, we will reduce/get rid of direct usages of things like
`InferredNullability.is_nullable`. This will simplify introducing
intermediate Nullability types.

Reviewed By: artempyanykh

Differential Revision: D17789599

fbshipit-source-id: f1b9d2dd0

infer/src/nullsafe/AnnotatedNullability.ml

@@ -36,6 +36,13 @@ and nonnull_origin =
   | ModelledNonnull  (** nullsafe knows it is non-nullable via its internal models *)
 [@@deriving compare]
 
+let get_nullability = function
+  | Nullable _ ->
+      Nullability.Nullable
+  | Nonnull _ ->
+      Nullability.Nonnull
+
+
 let pp fmt t =
   let string_of_nullable_origin nullable_origin =
     match nullable_origin with

infer/src/nullsafe/AnnotatedNullability.mli

@@ -38,6 +38,8 @@ and nonnull_origin =
   | ModelledNonnull  (** nullsafe knows it is non-nullable via its internal models *)
 [@@deriving compare]
 
+val get_nullability : t -> Nullability.t
+
 val of_annot_item : Annot.Item.t -> t
 (** Converts the information from the annotation to nullability.
     NOTE: it does not take into account models etc., so this is intended to be used

infer/src/nullsafe/InferredNullability.ml

@@ -7,15 +7,17 @@
 
 open! IStd
 
-type t = {is_nullable: bool; origin: TypeOrigin.t} [@@deriving compare]
+type t = {nullability: Nullability.t; origin: TypeOrigin.t} [@@deriving compare]
 
 let equal = [%compare.equal: t]
 
-let is_nullable t = t.is_nullable
+let get_nullability {nullability} = nullability
 
-let is_nonnull t = not t.is_nullable
+let is_nullable {nullability} = match nullability with Nullable -> true | Nonnull -> false
 
-let set_nonnull t = {t with is_nullable= false}
+let is_nonnull {nullability} = match nullability with Nullable -> false | Nonnull -> true
+
+let set_nonnull t = {t with nullability= Nullability.Nonnull}
 
 let descr_origin t =
   let descr_opt = TypeOrigin.get_description t.origin in
@@ -26,18 +28,33 @@ let descr_origin t =
       ("(Origin: " ^ str ^ ")", loc_opt, sig_opt)
 
 
-let to_string t = if is_nullable t then " @Nullable" else ""
+let to_string {nullability} = Printf.sprintf "[%s]" (Nullability.to_string nullability)
-
+
-let join ta1 ta2 =
+let join t1 t2 =
-  let nul1, nul2 = (is_nullable ta1, is_nullable ta2) in
+  let joined_nullability = Nullability.join t1.nullability t2.nullability in
-  let choose_left = match (nul1, nul2) with false, true -> false | _ -> true in
+  let is_equal_to_t1 = Nullability.equal t1.nullability joined_nullability in
-  let ta_chosen, ta_other = if choose_left then (ta1, ta2) else (ta2, ta1) in
+  let is_equal_to_t2 = Nullability.equal t2.nullability joined_nullability in
-  let origin =
+  (* Origin complements nullability information. It is the best effort to explain how was the nullability inferred.
-    if Bool.equal nul1 nul2 then TypeOrigin.join ta_chosen.origin ta_other.origin
+     If nullability is fully determined by one of the arguments, origin should be get from this argument.
-    else ta_chosen.origin
+     Otherwise we apply heuristics to choose origin either from t1 or t2.
+    *)
+  let joined_origin =
+    match (is_equal_to_t1, is_equal_to_t2) with
+    | true, false ->
+        (* Nullability was fully determined by t1. *)
+        t1.origin
+    | false, true ->
+        (* Nullability was fully determined by t2 *)
+        t2.origin
+    | false, false | true, true ->
+        (* Nullability is not fully determined by neither t1 nor t2
+           Let TypeOrigin logic to decide what to prefer in this case.
+         *)
+        TypeOrigin.join t1.origin t2.origin
   in
-  let ta' = {ta_chosen with origin} in
+  let result = {nullability= joined_nullability; origin= joined_origin} in
-  if equal ta' ta1 then None else Some ta'
+  (* TODO: make the result return non optional value *)
+  if equal result t1 then None else Some result
 
 
 let get_origin t = t.origin
@@ -50,15 +67,15 @@ let origin_is_fun_library t =
       false
 
 
-let create_nullable origin = {origin; is_nullable= true}
+let create_nullable origin = {origin; nullability= Nullability.Nullable}
 
-let create_nonnull origin = {origin; is_nullable= false}
+let create_nonnull origin = {origin; nullability= Nullability.Nonnull}
 
 let with_origin t o = {t with origin= o}
 
 let of_annotated_nullability annotated_nullability origin =
   match annotated_nullability with
   | AnnotatedNullability.Nullable _ ->
-      {origin; is_nullable= true}
+      {origin; nullability= Nullability.Nullable}
   | AnnotatedNullability.Nonnull _ ->
-      {origin; is_nullable= false}
+      {origin; nullability= Nullability.Nonnull}

infer/src/nullsafe/InferredNullability.mli

@@ -19,6 +19,8 @@ open! IStd
 
 type t [@@deriving compare]
 
+val get_nullability : t -> Nullability.t
+
 val create_nullable : TypeOrigin.t -> t
 
 val create_nonnull : TypeOrigin.t -> t

infer/src/nullsafe/Nullability.ml

@@ -0,0 +1,24 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! IStd
+
+type t =
+  | Nullable  (** No guarantees on the nullability *)
+  | Nonnull
+      (** We believe that this value can not be null. If it is not the case, this is
+          an unsoundness issue for Nullsafe, and we aim to minimize number of such issues
+          occuring in real-world programs. *)
+[@@deriving compare, equal]
+
+let join x y =
+  match (x, y) with Nullable, _ | _, Nullable -> Nullable | Nonnull, Nonnull -> Nonnull
+
+
+let is_subtype ~subtype ~supertype = equal (join subtype supertype) supertype
+
+let to_string = function Nullable -> "Nullable" | Nonnull -> "Nonnull"

infer/src/nullsafe/Nullability.mli

@@ -0,0 +1,35 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+open! IStd
+
+(** Nullability is a central concept for Nullsafe type-checker.
+    Informally, nullability is a "type" - set of values together with some additional context.
+      All nullsafe is interested about if whether a value can be null, and if it can,
+      what are potential causes of leaking the null inside it.
+    Formally, nullability values form a lattice with partial order and upper bound operations.
+    Practically, most of nullsafe core should remain agnostic over exact values of nullability
+    (e.g. pattern-mathching over them should be a rare case. Core of typechecker should deal with subtyping and joins instead.)
+ *)
+
+type t =
+  | Nullable  (** No guarantees on the nullability *)
+  | Nonnull
+      (** We believe that this value can not be null. If it is not the case, this is
+          an unsoundness issue for Nullsafe, and we aim to minimize number of such issues
+          occuring in real-world programs. *)
+[@@deriving compare, equal]
+
+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 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. *)
+
+val to_string : t -> string

infer/src/nullsafe/NullsafeRules.ml

@@ -7,63 +7,18 @@
 
 open! IStd
 
-type nullability = Nullable | Nonnull
+let passes_assignment_rule ~lhs ~rhs = Nullability.is_subtype ~subtype:rhs ~supertype:lhs
-
-let is_nullable nullability = match nullability with Nullable -> true | Nonnull -> false
-
-let is_nonnull nullability = match nullability with Nullable -> false | Nonnull -> true
-
-(*
-  Subtype in the standard definition of subtyping `<:` operator:
-  S <: T means that any term of type S can be safely used in a context
-  where a term of type T is expected.
-  The key fact is that Nonnull <: Nullable, but not the reverse.
-  *)
-let is_subtype ~subtype ~supertype =
-  (*
-    When it is NOT a subtype? When subtype is nullable and supertype is non-nullable.
-    Everything else is allowed.
-   *)
-  not (is_nullable subtype && is_nonnull supertype)
-
-
-let nullability_of_annotated_nullability annotated_nullability =
-  match annotated_nullability with
-  | AnnotatedNullability.Nullable _ ->
-      Nullable
-  | AnnotatedNullability.Nonnull _ ->
-      Nonnull
-
-
-let nullability_of_inferred_nullability inferred_nullability =
-  (* This needs to be modified in order to support unknown nullability *)
-  if InferredNullability.is_nullable inferred_nullability then Nullable else Nonnull
-
-
-let passes_assignment_rule_for_annotated_nullability ~lhs ~rhs =
-  let lhs_nullability = nullability_of_annotated_nullability lhs in
-  let rhs_nullability = nullability_of_inferred_nullability rhs in
-  is_subtype ~subtype:rhs_nullability ~supertype:lhs_nullability
-
-
-let passes_assignment_rule_for_inferred_nullability ~lhs ~rhs =
-  let lhs_nullability = nullability_of_inferred_nullability lhs in
-  let rhs_nullability = nullability_of_inferred_nullability rhs in
-  is_subtype ~subtype:rhs_nullability ~supertype:lhs_nullability
-
 
 type type_role = Param | Ret
 
 let passes_inheritance_rule type_role ~base ~overridden =
-  let base_nullability = nullability_of_annotated_nullability base in
-  let overridden_nullability = nullability_of_annotated_nullability overridden in
   let subtype, supertype =
     match type_role with
     | Ret ->
         (* covariance for ret *)
-        (overridden_nullability, base_nullability)
+        (overridden, base)
     | Param ->
         (* contravariance for param *)
-        (base_nullability, overridden_nullability)
+        (base, overridden)
   in
-  is_subtype ~subtype ~supertype
+  Nullability.is_subtype ~subtype ~supertype

infer/src/nullsafe/NullsafeRules.mli

@@ -18,29 +18,14 @@ open! IStd
   this module instead of doing things on their own.
   *)
 
-(*******************************************************************************************
+val passes_assignment_rule : lhs:Nullability.t -> rhs:Nullability.t -> bool
- *** Assignment rule **********************************************************************
+(** Assignment rule: No expression of nullable type is ever assigned to a location
-
+    of non-nullable type.
-Assignment rule: No expression of nullable type is ever assigned to a location
-of non-nullable type.
  *)
 
-val passes_assignment_rule_for_annotated_nullability :
-  lhs:AnnotatedNullability.t -> rhs:InferredNullability.t -> bool
-(** Variant of assignment rule where lhs nullability is fully determined by its formal Nullsafe type *)
-
-val passes_assignment_rule_for_inferred_nullability :
-  lhs:InferredNullability.t -> rhs:InferredNullability.t -> bool
-(** Variant of assignment rule where lhs nullability is inferred (e.g. might differ from formal nullability of a corresponding type) *)
-
-(*******************************************************************************************
- *** Inheritance rule **********************************************************************
-  *)
-
 type type_role = Param | Ret
 
-val passes_inheritance_rule :
+val passes_inheritance_rule : type_role -> base:Nullability.t -> overridden:Nullability.t -> bool
-  type_role -> base:AnnotatedNullability.t -> overridden:AnnotatedNullability.t -> bool
 (** Inheritance rule:
   a) Return type for an overridden method is covariant:
        overridden method is allowed to narrow down the return value to a subtype of the one from the

infer/src/nullsafe/eradicateChecks.ml

@@ -151,8 +151,9 @@ let check_field_assignment tenv find_canonical_duplicate curr_pdesc node instr_r
   in
   let should_report_nullable =
     (not
-       (NullsafeRules.passes_assignment_rule_for_inferred_nullability ~lhs:inferred_nullability_lhs
+       (NullsafeRules.passes_assignment_rule
-          ~rhs:inferred_nullability_rhs))
+          ~lhs:(InferredNullability.get_nullability inferred_nullability_lhs)
+          ~rhs:(InferredNullability.get_nullability inferred_nullability_rhs)))
     && (not (AndroidFramework.is_destroy_method curr_pname))
     && PatternMatch.type_is_class t_lhs
     && (not (Typ.Fieldname.Java.is_outer_instance fname))
@@ -305,11 +306,10 @@ let check_constructor_initialization tenv find_canonical_duplicate curr_construc
 
 let check_return_not_nullable tenv find_canonical_duplicate loc curr_pname curr_pdesc
     (ret_signature : AnnotatedSignature.ret_signature) ret_inferred_nullability =
-  if
+  (* Returning from a function is essentially an assignment the actual return value to the formal `return` *)
-    not
+  let lhs = AnnotatedNullability.get_nullability ret_signature.ret_annotated_type.nullability in
-      (NullsafeRules.passes_assignment_rule_for_annotated_nullability
+  let rhs = InferredNullability.get_nullability ret_inferred_nullability in
-         ~lhs:ret_signature.ret_annotated_type.nullability ~rhs:ret_inferred_nullability)
+  if not (NullsafeRules.passes_assignment_rule ~lhs ~rhs) then
-  then
     report_error tenv find_canonical_duplicate
       (TypeErr.Return_annotation_inconsistent
          (curr_pname, InferredNullability.descr_origin ret_inferred_nullability))
@@ -406,11 +406,11 @@ let check_call_parameters tenv find_canonical_duplicate curr_pdesc node callee_a
         (Some instr_ref) loc curr_pdesc
     in
     if PatternMatch.type_is_class formal.param_annotated_type.typ then
-      if
+      (* Passing a param to a function is essentially an assignment the actual param value
-        not
+      to the formal param *)
-          (NullsafeRules.passes_assignment_rule_for_annotated_nullability
+      let lhs = AnnotatedNullability.get_nullability formal.param_annotated_type.nullability in
-             ~lhs:formal.param_annotated_type.nullability ~rhs:nullability_actual)
+      let rhs = InferredNullability.get_nullability nullability_actual in
-      then report ()
+      if not (NullsafeRules.passes_assignment_rule ~lhs ~rhs) then report ()
   in
   let should_check_parameters =
     match callee_pname with
@@ -467,15 +467,17 @@ let check_inheritance_rule_for_params find_canonical_duplicate tenv loc ~base_pr
       (* Check the rule for each pair of base and overridden param *)
       List.iteri base_and_overridden_params
         ~f:(fun index
-           ( AnnotatedSignature.{param_annotated_type= {nullability= base_nullability}}
+           ( AnnotatedSignature.{param_annotated_type= {nullability= annotated_nullability_base}}
            , AnnotatedSignature.
                { mangled= overridden_param_name
-               ; param_annotated_type= {nullability= overridden_nullability} } )
+               ; param_annotated_type= {nullability= annotated_nullability_overridden} } )
            ->
           check_inheritance_rule_for_param find_canonical_duplicate tenv loc ~overridden_param_name
             ~base_proc_name ~overridden_proc_name ~overridden_proc_desc
             ~param_position:(if should_index_from_zero then index else index + 1)
-            ~base_nullability ~overridden_nullability )
+            ~base_nullability:(AnnotatedNullability.get_nullability annotated_nullability_base)
+            ~overridden_nullability:
+              (AnnotatedNullability.get_nullability annotated_nullability_overridden) )
   | Unequal_lengths ->
       (* Skip checking.
       TODO (T5280249): investigate why argument lists can be of different length. *)
@@ -494,10 +496,12 @@ let check_inheritance_rule_for_signature find_canonical_duplicate tenv loc ~base
   | Typ.Procname.Java java_pname when not (Typ.Procname.Java.is_external java_pname) ->
       (* Check if return value is consistent with the base *)
       let base_nullability =
-        base_signature.AnnotatedSignature.ret.ret_annotated_type.nullability
+        AnnotatedNullability.get_nullability
+          base_signature.AnnotatedSignature.ret.ret_annotated_type.nullability
       in
       let overridden_nullability =
-        overridden_signature.AnnotatedSignature.ret.ret_annotated_type.nullability
+        AnnotatedNullability.get_nullability
+          overridden_signature.AnnotatedSignature.ret.ret_annotated_type.nullability
       in
       check_inheritance_rule_for_return find_canonical_duplicate tenv loc ~base_proc_name
         ~overridden_proc_name ~overridden_proc_desc ~base_nullability ~overridden_nullability