From 91282fbcbe984a7d3d4c20aba2643bec5cf08be0 Mon Sep 17 00:00:00 2001 From: Mitya Lyubarskiy Date: Wed, 13 Nov 2019 10:15:15 -0800 Subject: [PATCH] [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 | 4 ---- infer/src/nullsafe/InferredNullability.mli | 2 -- infer/src/nullsafe/typeCheck.ml | 22 ++++++++++++---------- infer/src/nullsafe/typeOrigin.ml | 8 +++++++- infer/src/nullsafe/typeOrigin.mli | 3 +++ 5 files changed, 22 insertions(+), 17 deletions(-) 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.