[nullsafe][refactor] Store all joinees' origins in InferredNullability

Summary:
The fact that we did not preserve all joins (and used only the first
one) was a shorcut since the origin is used only for reporting, and
reporting the info about left joinee is enough for practical purposes.

Hovewer, to support annotation graph, we need all joinees.

This diff is a no-op since we use only the first one currently.

Reviewed By: artempyanykh

Differential Revision: D24621412

fbshipit-source-id: 8fe1174e7

infer/src/nullsafe/AssignmentRule.ml

@@ -218,7 +218,7 @@ module ReportableViolation = struct
 
 
   let make_nullsafe_issue ~assignment_location assignment_type {nullsafe_mode; violation= {rhs}} =
-    let rhs_origin = InferredNullability.get_origin rhs in
+    let rhs_origin = InferredNullability.get_simple_origin rhs in
     let user_friendly_nullable =
       ErrorRenderingUtils.UserFriendlyNullable.from_nullability
         (InferredNullability.get_nullability rhs)

infer/src/nullsafe/DereferenceRule.ml

@@ -114,7 +114,7 @@ module ReportableViolation = struct
                "get_description:: Dereference violation should not be possible for non-nullable \
                 values" )
     in
-    let nullable_object_origin = InferredNullability.get_origin nullability in
+    let nullable_object_origin = InferredNullability.get_simple_origin nullability in
     match user_friendly_nullable with
     | ErrorRenderingUtils.UserFriendlyNullable.UntrustedNonnull untrusted_kind ->
         (* Attempt to dereference a value which is not explictly declared as nullable,

infer/src/nullsafe/InferredNullability.ml

@@ -7,9 +7,24 @@
 
 open! IStd
 
-type t = {nullability: Nullability.t; origin: TypeOrigin.t} [@@deriving compare]
+type t =
+  { nullability: Nullability.t
+  ; origins: TypeOrigin.t list  (** Origins responsible for this nullability type *) }
+[@@deriving compare]
+
+let rec sanitize_origin = function
+  (* Collapse consecutive chains of InferredNonnull to get rid of infinite chains in loops and
+     hence allowing to reach the fixpoint *)
+  | TypeOrigin.InferredNonnull
+      {previous_origin= TypeOrigin.InferredNonnull {previous_origin= underlying}} ->
+      TypeOrigin.InferredNonnull {previous_origin= underlying} |> sanitize_origin
+  | other ->
+      other
+
+
+let create origin =
+  {nullability= TypeOrigin.get_nullability origin; origins= [sanitize_origin origin]}
 
-let create origin = {nullability= TypeOrigin.get_nullability origin; origin}
 
 let get_nullability {nullability} = nullability
 
@@ -17,6 +32,11 @@ let is_nonnullish {nullability} = Nullability.is_nonnullish nullability
 
 let pp fmt {nullability} = Nullability.pp fmt nullability
 
+(* Join two lists with removing duplicates and preserving the order of join *)
+let join_origins origins1 origins2 =
+  (IList.append_no_duplicates ~cmp:TypeOrigin.compare |> Staged.unstage) origins1 origins2
+
+
 let join t1 t2 =
   let joined_nullability = Nullability.join t1.nullability t2.nullability in
   let is_equal_to_t1 = Nullability.equal t1.nullability joined_nullability in
@@ -25,28 +45,27 @@ let join t1 t2 =
      If nullability is fully determined by one of the arguments, origin should be get from this argument.
      Otherwise we apply heuristics to choose origin either from t1 or t2.
   *)
-  let joined_origin =
+  let joined_origins =
     match (is_equal_to_t1, is_equal_to_t2) with
     | _ when Nullability.equal t1.nullability Nullability.Null ->
-        t1.origin
+        t1.origins
     | _ when Nullability.equal t2.nullability Nullability.Null ->
-        t2.origin
+        t2.origins
     | true, false ->
         (* Nullability was fully determined by t1. *)
-        t1.origin
+        t1.origins
     | false, true ->
         (* Nullability was fully determined by t2 *)
-        t2.origin
+        t2.origins
     | false, false | true, true ->
-        (* Nullability is not fully determined by neither t1 nor t2
+        (* Nullability is not fully determined by neither t1 nor t2 - join both lists
-           Picking the left one for stability
         *)
-        t1.origin
+        join_origins t1.origins t2.origins
   in
-  {nullability= joined_nullability; origin= joined_origin}
+  {nullability= joined_nullability; origins= joined_origins}
 
 
-let get_origin t = t.origin
+let get_simple_origin t = List.nth_exn t.origins 0
 
 let origin_is_fun_defined t =
-  match get_origin t with TypeOrigin.MethodCall {is_defined; _} -> is_defined | _ -> false
+  match get_simple_origin t with TypeOrigin.MethodCall {is_defined; _} -> is_defined | _ -> false

infer/src/nullsafe/InferredNullability.mli

@@ -23,7 +23,7 @@ val create : TypeOrigin.t -> t
 val is_nonnullish : t -> bool
 (** Check whether corresponding [Nullability] is [Nullability.is_nonnullish] *)
 
-val get_origin : t -> TypeOrigin.t
+val get_simple_origin : t -> TypeOrigin.t
 (** The simple explanation of how was nullability inferred. *)
 
 val join : t -> t -> t

infer/src/nullsafe/eradicateChecks.ml

@@ -104,7 +104,7 @@ let check_condition_for_redundancy
        So Condition_redundant should either accept expression, or this should pass a condition.
     *)
     let condition_descr = explain_expr tenv node expr in
-    let nonnull_origin = InferredNullability.get_origin inferred_nullability in
+    let nonnull_origin = InferredNullability.get_simple_origin inferred_nullability in
     TypeErr.register_error analysis_data find_canonical_duplicate
       (TypeErr.Condition_redundant {is_always_true; loc; condition_descr; nonnull_origin})
       (Some instr_ref) ~nullsafe_mode
@@ -256,7 +256,7 @@ let check_constructor_initialization
               predicate_holds_for_some_typestate
                 (Lazy.force typestates_for_curr_constructor_and_all_initializer_methods) field_name
                 ~predicate:(fun (_, nullability) ->
-                  is_initialized (InferredNullability.get_origin nullability) )
+                  is_initialized (InferredNullability.get_simple_origin nullability) )
             in
             (* TODO(T54584721) This check is completely independent of the current constuctor we check.
                This check should be moved out of this function. Until it is done,

infer/src/nullsafe/typeCheck.ml

@@ -160,7 +160,7 @@ let rec typecheck_expr ({IntraproceduralAnalysis.tenv; _} as analysis_data) ~nul
               (typ, InferredNullability.create TypeOrigin.OptimisticFallback)
               loc
           in
-          let object_origin = InferredNullability.get_origin inferred_nullability in
+          let object_origin = InferredNullability.get_simple_origin inferred_nullability in
           let tr_new =
             match AnnotatedField.get tenv field_name typ with
             | Some AnnotatedField.{annotated_type= field_type} ->
@@ -207,7 +207,7 @@ let handle_field_access_via_temporary idenv curr_pname typestate exp =
   let pvar_get_origin pvar =
     match TypeState.lookup_pvar pvar typestate with
     | Some (_, inferred_nullability) ->
-        Some (InferredNullability.get_origin inferred_nullability)
+        Some (InferredNullability.get_simple_origin inferred_nullability)
     | None ->
         None
   in
@@ -313,7 +313,7 @@ let convert_complex_exp_to_pvar_and_register_field_in_typestate tenv idenv curr_
             | _ ->
                 None )
             |> Option.value_map
-                 ~f:(fun (_, nullability) -> InferredNullability.get_origin nullability)
+                 ~f:(fun (_, nullability) -> InferredNullability.get_simple_origin nullability)
                  ~default:TypeOrigin.OptimisticFallback
           in
           let exp' = IDEnv.expand_expr_temps idenv original_node exp_ in
@@ -526,9 +526,9 @@ let do_preconditions_check_not_null
                { is_always_true= true
                ; loc
                ; condition_descr= EradicateChecks.explain_expr tenv node cond
-               ; nonnull_origin= InferredNullability.get_origin nullability })
+               ; nonnull_origin= InferredNullability.get_simple_origin nullability })
             (Some instr_ref) ~nullsafe_mode ) ;
-        let previous_origin = InferredNullability.get_origin nullability in
+        let previous_origin = InferredNullability.get_simple_origin nullability in
         let new_origin = TypeOrigin.InferredNonnull {previous_origin} in
         TypeState.add pvar
           (t, InferredNullability.create new_origin)
@@ -577,7 +577,7 @@ let do_preconditions_check_state instr_ref idenv tenv curr_pname curr_annotated_
     (* handle the annotation flag for pvar *)
     match TypeState.lookup_pvar pvar typestate1 with
     | Some (t, nullability) ->
-        let previous_origin = InferredNullability.get_origin nullability in
+        let previous_origin = InferredNullability.get_simple_origin nullability in
         let new_origin = TypeOrigin.InferredNonnull {previous_origin} in
         TypeState.add pvar
           (t, InferredNullability.create new_origin)
@@ -851,7 +851,7 @@ let rec check_condition_for_sil_prune
       | Some (t, current_nullability) ->
           let new_origin =
             TypeOrigin.InferredNonnull
-              {previous_origin= InferredNullability.get_origin current_nullability}
+              {previous_origin= InferredNullability.get_simple_origin current_nullability}
           in
           let new_nullability = InferredNullability.create new_origin in
           TypeState.add pvar (t, new_nullability) typestate' ~descr

infer/src/nullsafe/typeState.ml

@@ -32,7 +32,7 @@ let empty = M.empty
 let pp fmt typestate =
   let pp_one exp (typ, ta) =
     F.fprintf fmt "  %a -> [%s] %a %a@\n" Exp.pp exp
-      (TypeOrigin.to_string (InferredNullability.get_origin ta))
+      (TypeOrigin.to_string (InferredNullability.get_simple_origin ta))
       InferredNullability.pp ta (Typ.pp_full Pp.text) typ
   in
   let pp_map map = M.iter pp_one map in