diff --git a/infer/src/nullsafe/InferredNullability.ml b/infer/src/nullsafe/InferredNullability.ml index 81920cae0..a14724206 100644 --- a/infer/src/nullsafe/InferredNullability.ml +++ b/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 diff --git a/infer/src/nullsafe/InferredNullability.mli b/infer/src/nullsafe/InferredNullability.mli index d38d04b0a..08ba64ef5 100644 --- a/infer/src/nullsafe/InferredNullability.mli +++ b/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 ) diff --git a/infer/src/nullsafe/typeCheck.ml b/infer/src/nullsafe/typeCheck.ml index a820cbe6b..49c5a9908 100644 --- a/infer/src/nullsafe/typeCheck.ml +++ b/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 -> diff --git a/infer/src/nullsafe/typeOrigin.ml b/infer/src/nullsafe/typeOrigin.ml index b4f6abfe3..5b38d15f7 100644 --- a/infer/src/nullsafe/typeOrigin.ml +++ b/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 -> diff --git a/infer/src/nullsafe/typeOrigin.mli b/infer/src/nullsafe/typeOrigin.mli index 99fc3fe6d..fa890076c 100644 --- a/infer/src/nullsafe/typeOrigin.mli +++ b/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.