diff --git a/infer/src/nullsafe/DereferenceRule.ml b/infer/src/nullsafe/DereferenceRule.ml index 1fad4fe6c..d84922cd0 100644 --- a/infer/src/nullsafe/DereferenceRule.ml +++ b/infer/src/nullsafe/DereferenceRule.ml @@ -17,7 +17,7 @@ type dereference_type = let check ~is_strict_mode nullability = match nullability with - | Nullability.Nullable -> + | Nullability.Nullable | Nullability.Null -> Error nullability | Nullability.DeclaredNonnull -> if is_strict_mode then Error nullability else Ok () diff --git a/infer/src/nullsafe/InferredNullability.ml b/infer/src/nullsafe/InferredNullability.ml index 761e5bd6f..688c38a2e 100644 --- a/infer/src/nullsafe/InferredNullability.ml +++ b/infer/src/nullsafe/InferredNullability.ml @@ -14,12 +14,10 @@ let create origin = {nullability= TypeOrigin.get_nullability origin; origin} let get_nullability {nullability} = nullability let is_nonnull_or_declared_nonnull {nullability} = - match nullability with Nullable -> false | DeclaredNonnull -> true | Nonnull -> true + match nullability with Nonnull | DeclaredNonnull -> true | _ -> false -let is_nonnull {nullability} = - match nullability with Nullable -> false | DeclaredNonnull -> false | Nonnull -> true - +let is_nonnull {nullability} = match nullability with Nonnull -> true | _ -> false let to_string {nullability} = Printf.sprintf "[%s]" (Nullability.to_string nullability) @@ -33,6 +31,10 @@ let join t1 t2 = *) let joined_origin = match (is_equal_to_t1, is_equal_to_t2) with + | _ when Nullability.equal t1.nullability Nullability.Null -> + t1.origin + | _ when Nullability.equal t2.nullability Nullability.Null -> + t2.origin | true, false -> (* Nullability was fully determined by t1. *) t1.origin diff --git a/infer/src/nullsafe/Nullability.ml b/infer/src/nullsafe/Nullability.ml index f1a992d27..9e71297da 100644 --- a/infer/src/nullsafe/Nullability.ml +++ b/infer/src/nullsafe/Nullability.ml @@ -8,6 +8,7 @@ open! IStd type t = + | Null (** The only possible value for that type is null *) | Nullable (** No guarantees on the nullability *) | DeclaredNonnull (** The type comes from a signature that is annotated (explicitly or implicitly according to conventions) @@ -24,6 +25,10 @@ let top = Nullable let join x y = match (x, y) with + | Null, Null -> + Null + | Null, _ | _, Null -> + Nullable | Nullable, _ | _, Nullable -> Nullable | DeclaredNonnull, _ | _, DeclaredNonnull -> @@ -34,11 +39,9 @@ let join x y = let is_subtype ~subtype ~supertype = equal (join subtype supertype) supertype -let is_strict_subtype ~subtype ~supertype = - is_subtype ~subtype ~supertype && not (equal subtype supertype) - - let to_string = function + | Null -> + "Null" | Nullable -> "Nullable" | DeclaredNonnull -> diff --git a/infer/src/nullsafe/Nullability.mli b/infer/src/nullsafe/Nullability.mli index 03a278936..3f6274457 100644 --- a/infer/src/nullsafe/Nullability.mli +++ b/infer/src/nullsafe/Nullability.mli @@ -17,6 +17,7 @@ open! IStd *) type t = + | Null (** The only possible value for that type is null *) | Nullable (** No guarantees on the nullability *) | DeclaredNonnull (** The type comes from a signature that is annotated (explicitly or implicitly according to conventions) @@ -36,9 +37,6 @@ val is_subtype : subtype:t -> supertype:t -> bool (** A is a subtype of B, if all values of A can be represented in B. Subtype relation is reflexive: everything is a subtype of itself. *) -val is_strict_subtype : subtype:t -> supertype:t -> bool -(** The same as subtype, but non-reflexive version. *) - val join : t -> t -> t (** Unique upper bound over two types: the most precise type that is a supertype of both. Practically, joins occur e.g. when two branches of execution flow are getting merged. *) diff --git a/infer/src/nullsafe/OverAnnotatedRule.ml b/infer/src/nullsafe/OverAnnotatedRule.ml index 4f8e1d36f..2fb1c0c6e 100644 --- a/infer/src/nullsafe/OverAnnotatedRule.ml +++ b/infer/src/nullsafe/OverAnnotatedRule.ml @@ -10,17 +10,18 @@ type violation = {declared_nullability: Nullability.t; can_be_narrowed_to: Nulla [@@deriving compare] let check ~what ~by_rhs_upper_bound = - if - Nullability.is_strict_subtype ~subtype:by_rhs_upper_bound ~supertype:what - && (* Suppress violations for anything apart from Nullable since such - issues are not very actionable and/or clear for the user. - E.g. we technically can suggest changing [DeclaredNonnull] to [Nonnull], - but in practice that requires strictification the code, which is a - separate effort. - *) - Nullability.equal what Nullable - then Error {declared_nullability= what; can_be_narrowed_to= by_rhs_upper_bound} - else Ok () + match (what, by_rhs_upper_bound) with + | Nullability.Nullable, Nullability.Nonnull | Nullability.Nullable, Nullability.DeclaredNonnull -> + Error {declared_nullability= what; can_be_narrowed_to= by_rhs_upper_bound} + | Nullability.Null, Nullability.Nonnull | Nullability.Null, Nullability.DeclaredNonnull -> + (* Null, Nonnull pais is an edge case that we don't expect to arise in practice for two reasons: + 1. The only way to declare something as Null is to declare it is java.lang.Void, but nullsafe + does not know about it just yet. + 2. Even if it knew, such could should not compile: the only way it could compile if it returns `null` directly. + *) + Error {declared_nullability= what; can_be_narrowed_to= by_rhs_upper_bound} + | _ -> + Ok () type violation_type = diff --git a/infer/src/nullsafe/typeOrigin.ml b/infer/src/nullsafe/typeOrigin.ml index 9855ef0f4..a7b97472f 100644 --- a/infer/src/nullsafe/typeOrigin.ml +++ b/infer/src/nullsafe/typeOrigin.ml @@ -49,7 +49,7 @@ let equal = [%compare.equal: t] let get_nullability = function | NullConst _ -> - Nullability.Nullable + Nullability.Null | NonnullConst _ | This (* `this` can not be null according to Java rules *) | New (* In Java `new` always create a non-null object *)