From 199d53f748031972b0659cead5d4f0d119de8a07 Mon Sep 17 00:00:00 2001 From: Mitya Lyubarskiy Date: Wed, 15 Apr 2020 06:23:47 -0700 Subject: [PATCH] [nullsafe] Unsync documentation from Nullability.ml and .mli Summary: Having copypaste is painful to support. Lets make .mli the source of truth. Improved docs a bit, while I was here. Reviewed By: artempyanykh Differential Revision: D20948916 fbshipit-source-id: 1668dbc9c --- infer/src/nullsafe/Nullability.ml | 22 ++-------------------- infer/src/nullsafe/Nullability.mli | 27 +++++++++++++++++---------- 2 files changed, 19 insertions(+), 30 deletions(-) diff --git a/infer/src/nullsafe/Nullability.ml b/infer/src/nullsafe/Nullability.ml index 7c5d367f7..9709cb74d 100644 --- a/infer/src/nullsafe/Nullability.ml +++ b/infer/src/nullsafe/Nullability.ml @@ -9,30 +9,12 @@ open! IStd module F = Format type t = - | Null (** The only possible value for that type is null *) - | Nullable (** No guarantees on the nullability *) + | Null + | Nullable | ThirdPartyNonnull - (** Values coming from third-party methods and fields not explictly annotated as [@Nullable]. - We still consider those as non-nullable but with the least level of confidence. *) | UncheckedNonnull - (** The type comes from a signature that is annotated (explicitly or implicitly according to - conventions) as non-nullable. However, it might still contain null since the truthfulness - of the declaration was not checked. *) | LocallyCheckedNonnull - (** Non-nullable value the comes from a class checked under local mode. Local mode type-checks - files against its dependencies but does not require the dependencies to be transitively - checked. Therefore this type of non-nullable value is differentiated from StrictNonnull. *) | StrictNonnull - (** Non-nullable value with the highest degree of certainty, because it is either: - - - a non-null literal, - - an expression that semantically cannot be null, - - comes from internal code checked under strict mode, - - comes from a third-party method with an appropriate built-in model or user-defined - nullability signature. - - The latter two are potential sources of unsoundness issues for nullsafe, but we need to - strike the balance between the strictness of analysis, convenience, and real-world risk. *) [@@deriving compare, equal] type pair = t * t [@@deriving compare, equal] diff --git a/infer/src/nullsafe/Nullability.mli b/infer/src/nullsafe/Nullability.mli index 6929dbbc2..1bd02e33f 100644 --- a/infer/src/nullsafe/Nullability.mli +++ b/infer/src/nullsafe/Nullability.mli @@ -20,23 +20,30 @@ type t = | Null (** The only possible value for that type is null *) | Nullable (** No guarantees on the nullability *) | ThirdPartyNonnull - (** Values coming from third-party methods and fields not explictly annotated as [@Nullable]. - We still consider those as non-nullable but with the least level of confidence. *) + (** Values coming from third-party methods and fields not explictly annotated neither as + [@Nullable], nor as [@Nonnull]. We still consider those as non-nullable but with the least + level of confidence. *) | UncheckedNonnull (** The type comes from a signature that is annotated (explicitly or implicitly according to - conventions) as non-nullable. Hovewer, it might still contain null since the truthfullness - of the declaration was not checked. *) + conventions) as non-nullable. Hovewer, the class is not checked under [@Nullsafe], so its + actual nullability is not truthworhy, as the class might contain arbitrary number of + nullability issues *) | LocallyCheckedNonnull - (** Non-nullable value that comes from a class checked under local mode. Local mode + (** Non-nullable value that comes from a class checked under [@NullsafeLocal] mode. Local mode type-checks files against its dependencies but does not require the dependencies to be transitively checked. Therefore this type of non-nullable value is differentiated from StrictNonnull. *) | StrictNonnull - (** We believe that this value can not be null because it is either a non-null literal, an - expression that semantically cannot be null, or a non-null value that should not be null - according to typechecking rules. If the latter is not the case, this is an unsoundness - issue for nullsafe, and we aim to minimize number of such issues occuring in real-world - programs. *) + (** Non-nullable value with the highest degree of certainty, because it is either: + + - a non-null literal, + - an expression that semantically cannot be null, + - comes from code checked under [@NullsafeStrict] mode, + - comes from a third-party method with an appropriate built-in model, user-defined + nullability signature, or explicit [@NonNull] annotation. + + The latter two are potential sources of unsoundness issues for nullsafe, but we need to + strike the balance between the strictness of analysis, convenience, and real-world risk. *) [@@deriving compare, equal] type pair = t * t [@@deriving compare, equal]