From 72dc6c66b1ee5883b501a7f08ef5f6fc269daecf Mon Sep 17 00:00:00 2001
From: Mitya Lyubarskiy <mityal@fb.com>
Date: Wed, 9 Oct 2019 08:11:34 -0700
Subject: [PATCH] [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  |  2 --
 infer/src/nullsafe/InferredNullability.mli |  2 --
 infer/src/nullsafe/NullsafeRules.ml        |  7 +++++++
 infer/src/nullsafe/NullsafeRules.mli       |  4 ++++
 infer/src/nullsafe/eradicateChecks.ml      | 16 ++++++++++++----
 5 files changed, 23 insertions(+), 8 deletions(-)

diff --git a/infer/src/nullsafe/InferredNullability.ml b/infer/src/nullsafe/InferredNullability.ml
index 32665b367..6ab1c54c8 100644
--- a/infer/src/nullsafe/InferredNullability.ml
+++ b/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}
diff --git a/infer/src/nullsafe/InferredNullability.mli b/infer/src/nullsafe/InferredNullability.mli
index 000b4a75c..77a1f41f4 100644
--- a/infer/src/nullsafe/InferredNullability.mli
+++ b/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
diff --git a/infer/src/nullsafe/NullsafeRules.ml b/infer/src/nullsafe/NullsafeRules.ml
index e9d02efe0..532a84b9b 100644
--- a/infer/src/nullsafe/NullsafeRules.ml
+++ b/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 =
diff --git a/infer/src/nullsafe/NullsafeRules.mli b/infer/src/nullsafe/NullsafeRules.mli
index 154c2343f..90d495f70 100644
--- a/infer/src/nullsafe/NullsafeRules.mli
+++ b/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
diff --git a/infer/src/nullsafe/eradicateChecks.ml b/infer/src/nullsafe/eradicateChecks.ml
index 2926a7619..6e7267961 100644
--- a/infer/src/nullsafe/eradicateChecks.ml
+++ b/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