From 2b53fe543fb2b4a36d2465b09f8faa14b65fdb52 Mon Sep 17 00:00:00 2001
From: Mitya Lyubarskiy <mityal@fb.com>
Date: Fri, 15 Nov 2019 05:10:45 -0800
Subject: [PATCH] [nullsafe] TypeOrigin has a special case for array access

Summary:
This diff is a part of work teaching Nullsafe to explain decisions it's
making.

We used to use default for this, which is both buggy and hard to
diagnose. Now we explicitly document nullsafe behaviour in this case.

Reviewed By: artempyanykh

Differential Revision: D18481220

fbshipit-source-id: 0b0cf8b38
---
 infer/src/nullsafe/typeCheck.ml   |  3 ++-
 infer/src/nullsafe/typeOrigin.ml  | 13 ++++++++++++-
 infer/src/nullsafe/typeOrigin.mli |  1 +
 3 files changed, 15 insertions(+), 2 deletions(-)

diff --git a/infer/src/nullsafe/typeCheck.ml b/infer/src/nullsafe/typeCheck.ml
index 49c5a9908..f3c302081 100644
--- a/infer/src/nullsafe/typeCheck.ml
+++ b/infer/src/nullsafe/typeCheck.ml
@@ -170,7 +170,8 @@ let rec typecheck_expr ~is_strict_mode find_canonical_duplicate visited checks t
           curr_pdesc node instr_ref array_exp
           (DereferenceRule.AccessByIndex {index_desc})
           inferred_nullability loc ;
-      tr_default
+      let typ, _ = tr_default in
+      (typ, InferredNullability.create TypeOrigin.ArrayAccess)
   | _ ->
       tr_default
 
diff --git a/infer/src/nullsafe/typeOrigin.ml b/infer/src/nullsafe/typeOrigin.ml
index 5b38d15f7..33dd0b8b6 100644
--- a/infer/src/nullsafe/typeOrigin.ml
+++ b/infer/src/nullsafe/typeOrigin.ml
@@ -18,6 +18,7 @@ type t =
   | MethodCall of method_call_origin  (** A result of a method call *)
   | New  (** A new object creation *)
   | ArrayLengthResult  (** integer value - result of accessing array.length *)
+  | ArrayAccess  (** Result of accessing an array by index *)
   | InferredNonnull of {previous_origin: t}
       (** The value is inferred as non-null during flow-sensitive type inference
           (most commonly from relevant condition branch or assertion explicitly comparing the value with `null`) *)
@@ -54,6 +55,14 @@ let get_nullability = function
   | New (* In Java `new` always create a non-null object  *)
   | ArrayLengthResult (* integer hence non-nullable *)
   | InferredNonnull _
+  (* WARNING: we trade soundness for usability.
+     In Java, arrays are initialized with null, so accessing array is nullable until it was initialized.
+     However we assume array access is going to always return non-nullable.
+     This is because in real life arrays are often initialized straight away.
+     We currently don't have a nice way to detect initialization, neither automatical nor manual.
+     Hence we make potentially dangerous choice in favor of pragmatism.
+  *)
+  | ArrayAccess
   | OptimisticFallback (* non-null is the most optimistic type *)
   | Undef (* This is a very special case, assigning non-null is a technical trick *) ->
       Nullability.Nonnull
@@ -85,6 +94,8 @@ let rec to_string = function
       "New"
   | ArrayLengthResult ->
       "ArrayLength"
+  | ArrayAccess ->
+      "ArrayAccess"
   | InferredNonnull _ ->
       "InferredNonnull"
   | OptimisticFallback ->
@@ -124,7 +135,7 @@ let get_description origin =
      But for these issues we currently don't print origins in the error string.
      It is a good idea to change this and start printing origins for these origins as well.
   *)
-  | This | New | NonnullConst _ | ArrayLengthResult | InferredNonnull _ ->
+  | This | New | NonnullConst _ | ArrayLengthResult | ArrayAccess | InferredNonnull _ ->
       None
   (* Two special cases - should not really occur in normal code *)
   | OptimisticFallback | Undef ->
diff --git a/infer/src/nullsafe/typeOrigin.mli b/infer/src/nullsafe/typeOrigin.mli
index fa890076c..8386be861 100644
--- a/infer/src/nullsafe/typeOrigin.mli
+++ b/infer/src/nullsafe/typeOrigin.mli
@@ -16,6 +16,7 @@ type t =
   | MethodCall of method_call_origin  (** A result of a method call *)
   | New  (** A new object creation *)
   | ArrayLengthResult  (** integer value - result of accessing array.length *)
+  | ArrayAccess  (** Result of accessing an array by index *)
   | InferredNonnull of {previous_origin: t}
       (** The value is inferred as non-null during flow-sensitive type inference
           (most commonly from relevant condition branch or assertion explicitly comparing the value with `null`) *)