[nullsafe][tech debt] Get rid of TypeOrigin.Undef

Summary:
Both TypeOrigin.Undef and TypeOrigin.OptimisticFallback are bad and
should be killed.

Let's start with Undef as the biggest offender, then try to gradually
reduce usage of the second one.

It is super unclear what does Undef even mean, and actually the code that
tries to use it (in a way that I can not fully comprehend) occurred to be "almost" no-op.

"Almost" means that the only place that is affected is
CONDITION_REDUNDANT checks: we have few extra (FP) warnings of his type.

Mostly those correspond to comparing with null result of array member
access: `myArray[i] == null` is marked as redundant. And I even don't
know how come it was not showing up before: we do assume all calls to
array are optimistically non-null (see TypeOrigin.ArrayAccess).

Anyways, we give up on this one: condition redundant is "broken" anyway
(has too many FP to be surfaced to the user); and when/if we want to fix
it, we can easily support array access idiomatically.

Reviewed By: jvillard

Differential Revision: D20248988

fbshipit-source-id: b20f61fd0

infer/src/nullsafe/ErrorRenderingUtils.ml

@@ -57,8 +57,7 @@ let is_object_nullability_self_explanatory ~object_expression (object_origin : T
   | ArrayLengthResult
   | ArrayAccess
   | InferredNonnull _
-  | OptimisticFallback
-  | Undef ->
+  | OptimisticFallback ->
       false
 
 

infer/src/nullsafe/eradicateChecks.ml

@@ -257,9 +257,6 @@ let check_constructor_initialization tenv find_canonical_duplicate curr_construc
             in
             let is_initialized_in_either_constructor_or_initializer =
               let is_initialized = function
-                | TypeOrigin.Undef ->
-                    (* Special case: not really an initialization *)
-                    false
                 | TypeOrigin.Field {object_origin= TypeOrigin.This} ->
                     (* Circular initialization - does not count *)
                     false

infer/src/nullsafe/typeCheck.ml

@@ -226,15 +226,7 @@ let funcall_exp_to_original_pvar_exp tenv curr_pname typestate exp ~is_assignmen
         exp
     | Some exp_str ->
         let pvar = Pvar.mk (Mangled.from_string exp_str) curr_pname in
-        let already_defined_in_typestate =
-          match TypeState.lookup_pvar pvar typestate with
-          | Some (_, inferred_nullability) ->
-              not
-                (TypeOrigin.equal TypeOrigin.Undef
-                   (InferredNullability.get_origin inferred_nullability))
-          | None ->
-              false
-        in
+        let already_defined_in_typestate = Option.is_some (TypeState.lookup_pvar pvar typestate) in
         if is_assignment && already_defined_in_typestate then exp
           (* Don't overwrite pvar representing result of function call. *)
         else Exp.Lvar pvar )
@@ -439,7 +431,7 @@ let typecheck_expr_for_errors ~nullsafe_mode find_canonical_duplicate curr_pdesc
     tenv node instr_ref typestate1 exp1 loc1 : unit =
   ignore
     (typecheck_expr_simple ~nullsafe_mode find_canonical_duplicate curr_pdesc calls_this checks tenv
-       node instr_ref typestate1 exp1 Typ.void TypeOrigin.Undef loc1)
+       node instr_ref typestate1 exp1 Typ.void TypeOrigin.OptimisticFallback loc1)
 
 
 (* Handle Preconditions.checkNotNull. *)
@@ -596,7 +588,8 @@ let do_map_put call_params callee_pname tenv loc node curr_pname curr_pdesc call
           let pvar_map_get = Pvar.mk (Mangled.from_string map_get_str) curr_pname in
           TypeState.add pvar_map_get
             (typecheck_expr_simple ~nullsafe_mode find_canonical_duplicate curr_pdesc calls_this
-               checks tenv node instr_ref typestate' exp_value typ_value TypeOrigin.Undef loc)
+               checks tenv node instr_ref typestate' exp_value typ_value
+               TypeOrigin.OptimisticFallback loc)
             typestate'
       | None ->
           typestate' )
@@ -1079,7 +1072,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
       in
       TypeState.add_id id
         (typecheck_expr_simple ~nullsafe_mode find_canonical_duplicate curr_pdesc calls_this checks
-           tenv node instr_ref typestate' e' typ TypeOrigin.Undef loc)
+           tenv node instr_ref typestate' e' typ TypeOrigin.OptimisticFallback loc)
         typestate'
   | Sil.Store {e1= Exp.Lvar pvar; e2= Exp.Exn _} when is_return pvar ->
       (* skip assignment to return variable where it is an artifact of a throw instruction *)
@@ -1107,7 +1100,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p
         | Exp.Lvar pvar ->
             TypeState.add pvar
               (typecheck_expr_simple ~nullsafe_mode find_canonical_duplicate curr_pdesc calls_this
-                 checks tenv node instr_ref typestate1 e2 typ TypeOrigin.Undef loc)
+                 checks tenv node instr_ref typestate1 e2 typ TypeOrigin.OptimisticFallback loc)
               typestate1
         | Exp.Lfield _ ->
             typestate1

infer/src/nullsafe/typeErr.ml

@@ -225,8 +225,7 @@ let get_nonnull_explanation_for_condition_redudant (nonnull_origin : TypeOrigin.
   | New
   | ArrayAccess
   | InferredNonnull _
-  | OptimisticFallback
-  | Undef ->
+  | OptimisticFallback ->
       " according to the existing annotations"
 
 

infer/src/nullsafe/typeOrigin.ml

@@ -10,28 +10,18 @@ open! IStd
 (** Describe the origin of values propagated by the checker. *)
 
 type t =
-  | NullConst of Location.t  (** A null literal in the source *)
-  | NonnullConst of Location.t  (** A constant (not equal to null) in the source. *)
-  | Field of field_origin  (** A field access (result of expression `some_object.some_field`) *)
-  | MethodParameter of method_parameter_origin  (** A method's parameter *)
-  | This (* `this` object. Can not be null, according to Java rules. *)
-  | MethodCall of method_call_origin  (** A result of a method call *)
+  | NullConst of Location.t
+  | NonnullConst of Location.t
+  | Field of field_origin
+  | MethodParameter of method_parameter_origin
+  | This
+  | MethodCall of method_call_origin
   | CallToGetKnownToContainsKey
-      (** This is a result of accessing a map element that is known to contains this particular key,
-          normally because it was explicitly checked for presense before *)
-  | New  (** A new object creation *)
-  | ArrayLengthResult  (** integer value - result of accessing array.length *)
-  | ArrayAccess  (** Result of accessing an array by index *)
+  | New
+  | ArrayLengthResult
+  | ArrayAccess
   | 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`) *)
-  (* Below are two special values. *)
   | OptimisticFallback
-      (** Something went wrong during typechecking. We fall back to optimistic (not-nullable) type
-          to reduce potential non-actionable false positives. Ideally we should not see these
-          instances. They should be either processed gracefully (and a dedicated type constructor
-          should be added), or fixed. T54687014 tracks unsoundness issues caused by this type. *)
-  | Undef  (** Undefined value before initialization *)
 [@@deriving compare]
 
 and method_parameter_origin = Normal of AnnotatedSignature.param_signature | ObjectEqualsOverride
@@ -67,8 +57,7 @@ let get_nullability = function
      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 *) ->
+  | OptimisticFallback (* non-null is the most optimistic type *) ->
       Nullability.StrictNonnull
   | Field {field_type= {nullability}} ->
       AnnotatedNullability.get_nullability nullability
@@ -109,8 +98,6 @@ let rec to_string = function
       Format.sprintf "InferredNonnull(prev:%s)" (to_string previous_origin)
   | OptimisticFallback ->
       "OptimisticFallback"
-  | Undef ->
-      "Undef"
 
 
 let atline loc = " at line " ^ string_of_int loc.Location.line
@@ -179,18 +166,16 @@ let get_description origin =
   | InferredNonnull _
   | CallToGetKnownToContainsKey ->
       None
-  (* Two special cases - should not really occur in normal code *)
-  | OptimisticFallback | Undef ->
+  (* A technical origin *)
+  | OptimisticFallback ->
       None
 
 
 let join o1 o2 =
   match (o1, o2) with
-  (* left priority *)
-  | Undef, _ | _, Undef ->
-      Undef
   | Field _, (NullConst _ | NonnullConst _ | MethodParameter _ | This | MethodCall _ | New) ->
       (* low priority to Field, to support field initialization patterns *)
       o2
   | _ ->
+      (* left priority *)
       o1

infer/src/nullsafe/typeOrigin.mli

@@ -23,13 +23,13 @@ type t =
   | 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`) *)
-  (* Below are two special values. *)
   | OptimisticFallback
-      (** Something went wrong during typechecking. We fall back to optimistic (not-nullable) type
-          to reduce potential non-actionable false positives. Ideally we should not see these
-          instances. They should be either processed gracefully (and a dedicated type constructor
-          should be added), or fixed. T54687014 tracks unsoundness issues caused by this type. *)
-  | Undef  (** Undefined value before initialization *)
+      (** A special case: technical type variant. Indicates either cases when something went wrong
+          during typechecking, and some cases that should be expressed in a better way than using
+          this type. We fall back to optimistic (not-nullable) type to reduce potential
+          non-actionable false positives. Ideally we should not see these instances. They should be
+          either processed gracefully (and a dedicated type constructor should be added), or fixed.
+          T54687014 tracks unsoundness issues caused by this type. *)
 [@@deriving compare]
 
 and method_parameter_origin = Normal of AnnotatedSignature.param_signature | ObjectEqualsOverride