[nulllsafe] Migrate check for field assignment to NullsafeRules

Summary:
This diff also introduces "subtyping function" into NullsafeRule, which
will be the core check for other rules we will introduce in follow up
diffs

Reviewed By: ngorogiannis

Differential Revision: D17500466

fbshipit-source-id: 5821caa6e

infer/src/nullsafe/NullsafeRules.ml

@@ -7,13 +7,46 @@
 
 open! IStd
 
-let is_nonnull annotated_nullability =
+type nullability = Nullable | Nonnull
+
+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 _ ->
-      false
+      Nullable
   | AnnotatedNullability.Nonnull _ ->
-      true
+      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 ~lhs ~rhs =
-  (not (is_nonnull lhs)) || not (InferredNullability.is_nullable rhs)
+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

infer/src/nullsafe/NullsafeRules.mli

@@ -18,7 +18,17 @@ open! IStd
   this module instead of doing things on their own.
   *)
 
-val passes_assignment_rule : lhs:AnnotatedNullability.t -> rhs:InferredNullability.t -> bool
-(** Assignment rule: No expression of nullable type is ever assigned to a location
-    of non-nullable type.
-  *)
+(*******************************************************************************************
+ *** Assignment rule **********************************************************************
+
+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) *)

infer/src/nullsafe/eradicateChecks.ml

@@ -166,9 +166,10 @@ let check_field_assignment tenv find_canonical_duplicate curr_pdesc node instr_r
     Annotations.ia_is_cleanup ret_annotation_deprecated
   in
   let should_report_nullable =
-    (not (AndroidFramework.is_destroy_method curr_pname))
-    && (not (InferredNullability.is_nullable inferred_nullability_lhs))
-    && InferredNullability.is_nullable inferred_nullability_rhs
+    (not
+       (NullsafeRules.passes_assignment_rule_for_inferred_nullability ~lhs:inferred_nullability_lhs
+          ~rhs:inferred_nullability_rhs))
+    && (not (AndroidFramework.is_destroy_method curr_pname))
     && PatternMatch.type_is_class t_lhs
     && (not (Typ.Fieldname.Java.is_outer_instance fname))
     && (not (field_is_injector_readwrite ()))
@@ -266,8 +267,8 @@ let check_return_not_nullable tenv find_canonical_duplicate loc curr_pname curr_
     (ret_signature : AnnotatedSignature.ret_signature) ret_inferred_nullability =
   if
     not
-      (NullsafeRules.passes_assignment_rule ~lhs:ret_signature.ret_annotated_type.nullability
-         ~rhs:ret_inferred_nullability)
+      (NullsafeRules.passes_assignment_rule_for_annotated_nullability
+         ~lhs:ret_signature.ret_annotated_type.nullability ~rhs:ret_inferred_nullability)
   then
     report_error tenv find_canonical_duplicate
       (TypeErr.Return_annotation_inconsistent
@@ -367,8 +368,8 @@ let check_call_parameters tenv find_canonical_duplicate curr_pdesc node callee_a
     if PatternMatch.type_is_class formal.param_annotated_type.typ then
       if
         not
-          (NullsafeRules.passes_assignment_rule ~lhs:formal.param_annotated_type.nullability
-             ~rhs:nullability_actual)
+          (NullsafeRules.passes_assignment_rule_for_annotated_nullability
+             ~lhs:formal.param_annotated_type.nullability ~rhs:nullability_actual)
       then report ()
   in
   let should_check_parameters =