[nullsafe][TypeOrigin refactor] Get rid of `set_nonnull`

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

This method was the last escape hatch for InferredNullability to
misreport about its origin.

Now each time we change nullability we provide origin that is consistent
with the nullability itself.

Reviewed By: artempyanykh

Differential Revision: D18453567

fbshipit-source-id: 3d9b7fa2e

infer/src/nullsafe/InferredNullability.ml

@@ -21,10 +21,6 @@ let is_nonnull {nullability} =
   match nullability with Nullable -> false | DeclaredNonnull -> false | Nonnull -> true
 
 
-let set_nullability nullability t = {t with nullability}
-
-let set_nonnull = set_nullability Nullability.Nonnull
-
 let descr_origin t =
   let descr_opt = TypeOrigin.get_description t.origin in
   match descr_opt with

infer/src/nullsafe/InferredNullability.mli

@@ -27,8 +27,6 @@ val is_nonnull_or_declared_nonnull : t -> bool
 
 val is_nonnull : t -> bool
 
-val set_nonnull : t -> t
-
 val descr_origin : t -> TypeErr.origin_descr
 (** Human-readable description of the origin of a value.
   (How did nullsafe infer the nullability )

infer/src/nullsafe/typeCheck.ml

@@ -456,10 +456,9 @@ let do_preconditions_check_not_null instr_ref tenv find_canonical_duplicate node
           EradicateChecks.report_error tenv find_canonical_duplicate
             (TypeErr.Condition_redundant (true, EradicateChecks.explain_expr tenv node cond))
             (Some instr_ref) loc curr_pdesc ) ;
-        TypeState.add pvar
-          (* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *)
-          (t, InferredNullability.create TypeOrigin.OptimisticFallback)
-          typestate''
+        let previous_origin = InferredNullability.get_origin nullability in
+        let new_origin = TypeOrigin.InferredNonnull {previous_origin} in
+        TypeState.add pvar (t, InferredNullability.create new_origin) typestate''
     | None ->
         typestate'
   in
@@ -498,11 +497,10 @@ let do_preconditions_check_state instr_ref idenv tenv curr_pname curr_annotated_
   let set_nonnull_to_pvar typestate1 pvar =
     (* handle the annotation flag for pvar *)
     match TypeState.lookup_pvar pvar typestate1 with
-    | Some (t, _) ->
-        TypeState.add pvar
-          (* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *)
-          (t, InferredNullability.create TypeOrigin.OptimisticFallback)
-          typestate1
+    | Some (t, nullability) ->
+        let previous_origin = InferredNullability.get_origin nullability in
+        let new_origin = TypeOrigin.InferredNonnull {previous_origin} in
+        TypeState.add pvar (t, InferredNullability.create new_origin) typestate1
     | None ->
         typestate1
   in
@@ -713,7 +711,11 @@ let rec check_condition_for_sil_prune tenv idenv calls_this find_canonical_dupli
       match TypeState.lookup_pvar pvar typestate' with
       | Some (t, current_nullability) ->
           if not (InferredNullability.is_nonnull current_nullability) then
-            let new_nullability = InferredNullability.set_nonnull current_nullability in
+            let new_origin =
+              TypeOrigin.InferredNonnull
+                {previous_origin= InferredNullability.get_origin current_nullability}
+            in
+            let new_nullability = InferredNullability.create new_origin in
             TypeState.add pvar (t, new_nullability) typestate'
           else typestate'
       | None ->

infer/src/nullsafe/typeOrigin.ml

@@ -18,6 +18,9 @@ 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 *)
+  | 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.
@@ -50,6 +53,7 @@ let get_nullability = function
   | This (* `this` can not be null according to Java rules *)
   | New (* In Java `new` always create a non-null object  *)
   | ArrayLengthResult (* integer hence non-nullable *)
+  | InferredNonnull _
   | OptimisticFallback (* non-null is the most optimistic type *)
   | Undef (* This is a very special case, assigning non-null is a technical trick *) ->
       Nullability.Nonnull
@@ -81,6 +85,8 @@ let rec to_string = function
       "New"
   | ArrayLengthResult ->
       "ArrayLength"
+  | InferredNonnull _ ->
+      "InferredNonnull"
   | OptimisticFallback ->
       "OptimisticFallback"
   | Undef ->
@@ -118,7 +124,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 ->
+  | This | New | NonnullConst _ | ArrayLengthResult | InferredNonnull _ ->
       None
   (* Two special cases - should not really occur in normal code *)
   | OptimisticFallback | Undef ->

infer/src/nullsafe/typeOrigin.mli

@@ -16,6 +16,9 @@ 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 *)
+  | 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.