[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

@@ -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
 

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 ->

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`) *)