[nullsafe] Introduce dereference rule and consolidate its usage

Summary:
This proceeds work on abstracting out operations requiring raw
nullability operations from infer core code. This will simplify coming
introducing of intermediate nullability levels

Reviewed By: artempyanykh

Differential Revision: D17789612

fbshipit-source-id: 9a2bea2ed

infer/src/nullsafe/InferredNullability.ml

@@ -13,8 +13,6 @@ let equal = [%compare.equal: t]
 
 let get_nullability {nullability} = nullability
 
-let is_nullable {nullability} = match nullability with Nullable -> true | Nonnull -> false
-
 let is_nonnull {nullability} = match nullability with Nullable -> false | Nonnull -> true
 
 let set_nonnull t = {t with nullability= Nullability.Nonnull}

infer/src/nullsafe/InferredNullability.mli

@@ -25,8 +25,6 @@ val create_nullable : TypeOrigin.t -> t
 
 val create_nonnull : TypeOrigin.t -> t
 
-val is_nullable : t -> bool
-
 val is_nonnull : t -> bool
 
 val set_nonnull : t -> t

infer/src/nullsafe/NullsafeRules.ml

@@ -9,6 +9,13 @@ open! IStd
 
 let passes_assignment_rule ~lhs ~rhs = Nullability.is_subtype ~subtype:rhs ~supertype:lhs
 
+let passes_dereference_rule = function
+  | Nullability.Nullable ->
+      false
+  | Nullability.Nonnull ->
+      true
+
+
 type type_role = Param | Ret
 
 let passes_inheritance_rule type_role ~base ~overridden =

infer/src/nullsafe/NullsafeRules.mli

@@ -23,6 +23,10 @@ val passes_assignment_rule : lhs:Nullability.t -> rhs:Nullability.t -> bool
     of non-nullable type.
  *)
 
+val passes_dereference_rule : Nullability.t -> bool
+(** Dereference rule: an object can be dereferenced only when it is not nullable (or believed to be so).
+ *)
+
 type type_role = Param | Ret
 
 val passes_inheritance_rule : type_role -> base:Nullability.t -> overridden:Nullability.t -> bool

infer/src/nullsafe/eradicateChecks.ml

@@ -29,7 +29,11 @@ let is_virtual = function
 (** Check an access (read or write) to a field. *)
 let check_field_access tenv find_canonical_duplicate curr_pname node instr_ref exp fname
     inferred_nullability loc : unit =
-  if InferredNullability.is_nullable inferred_nullability then
+  if
+    not
+      (NullsafeRules.passes_dereference_rule
+         (InferredNullability.get_nullability inferred_nullability))
+  then
     let origin_descr = InferredNullability.descr_origin inferred_nullability in
     report_error tenv find_canonical_duplicate
       (TypeErr.Null_field_access (explain_expr tenv node exp, fname, origin_descr, false))
@@ -39,7 +43,11 @@ let check_field_access tenv find_canonical_duplicate curr_pname node instr_ref e
 (** Check an access to an array *)
 let check_array_access tenv find_canonical_duplicate curr_pname node instr_ref array_exp fname
     inferred_nullability loc indexed =
-  if InferredNullability.is_nullable inferred_nullability then
+  if
+    not
+      (NullsafeRules.passes_dereference_rule
+         (InferredNullability.get_nullability inferred_nullability))
+  then
     let origin_descr = InferredNullability.descr_origin inferred_nullability in
     report_error tenv find_canonical_duplicate
       (TypeErr.Null_field_access (explain_expr tenv node array_exp, fname, origin_descr, indexed))
@@ -368,8 +376,8 @@ let check_call_receiver tenv find_canonical_duplicate curr_pdesc node typestate
           (typ, InferredNullability.create_nonnull TypeOrigin.ONone, [])
           loc
       in
-      let null_method_call = InferredNullability.is_nullable this_inferred_nullability in
-      if null_method_call then
+      let this_nullability = InferredNullability.get_nullability this_inferred_nullability in
+      if not (NullsafeRules.passes_dereference_rule this_nullability) then
         let descr = explain_expr tenv node original_this_e in
         let origin_descr = InferredNullability.descr_origin this_inferred_nullability in
         report_error tenv find_canonical_duplicate