diff --git a/infer/src/nullsafe/AssignmentRule.ml b/infer/src/nullsafe/AssignmentRule.ml index fa9ee785c..0103e5106 100644 --- a/infer/src/nullsafe/AssignmentRule.ml +++ b/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) diff --git a/infer/src/nullsafe/DereferenceRule.ml b/infer/src/nullsafe/DereferenceRule.ml index f82819f64..6d245d132 100644 --- a/infer/src/nullsafe/DereferenceRule.ml +++ b/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, diff --git a/infer/src/nullsafe/InferredNullability.ml b/infer/src/nullsafe/InferredNullability.ml index 55a98fbb0..1a566fb51 100644 --- a/infer/src/nullsafe/InferredNullability.ml +++ b/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 - Picking the left one for stability + (* Nullability is not fully determined by neither t1 nor t2 - join both lists *) - 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 diff --git a/infer/src/nullsafe/InferredNullability.mli b/infer/src/nullsafe/InferredNullability.mli index 2690ece70..bc314ccb2 100644 --- a/infer/src/nullsafe/InferredNullability.mli +++ b/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 diff --git a/infer/src/nullsafe/eradicateChecks.ml b/infer/src/nullsafe/eradicateChecks.ml index ff5c45abe..e0b953e1f 100644 --- a/infer/src/nullsafe/eradicateChecks.ml +++ b/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, diff --git a/infer/src/nullsafe/typeCheck.ml b/infer/src/nullsafe/typeCheck.ml index 38b534de5..fc65602a5 100644 --- a/infer/src/nullsafe/typeCheck.ml +++ b/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 diff --git a/infer/src/nullsafe/typeState.ml b/infer/src/nullsafe/typeState.ml index f868e2de0..38317ed66 100644 --- a/infer/src/nullsafe/typeState.ml +++ b/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