diff --git a/infer/src/nullsafe/Nullability.ml b/infer/src/nullsafe/Nullability.ml index 59f2784f8..8837d8776 100644 --- a/infer/src/nullsafe/Nullability.ml +++ b/infer/src/nullsafe/Nullability.ml @@ -15,10 +15,16 @@ type t = occuring in real-world programs. *) [@@deriving compare, equal] +let top = Nullable + let join x y = match (x, y) with Nullable, _ | _, Nullable -> Nullable | Nonnull, Nonnull -> Nonnull 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 Nullable -> "Nullable" | Nonnull -> "Nonnull" diff --git a/infer/src/nullsafe/Nullability.mli b/infer/src/nullsafe/Nullability.mli index 37888db2e..f647b5d61 100644 --- a/infer/src/nullsafe/Nullability.mli +++ b/infer/src/nullsafe/Nullability.mli @@ -24,10 +24,16 @@ type t = occuring in real-world programs. *) [@@deriving compare, equal] +val top : t +(** The most generic type. *) + 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/NullsafeRules.ml b/infer/src/nullsafe/NullsafeRules.ml index 532a84b9b..38a8e5855 100644 --- a/infer/src/nullsafe/NullsafeRules.ml +++ b/infer/src/nullsafe/NullsafeRules.ml @@ -29,3 +29,7 @@ let passes_inheritance_rule type_role ~base ~overridden = (base, overridden) in Nullability.is_subtype ~subtype ~supertype + + +let is_overannotated ~lhs ~rhs_upper_bound = + Nullability.is_strict_subtype ~subtype:rhs_upper_bound ~supertype:lhs diff --git a/infer/src/nullsafe/NullsafeRules.mli b/infer/src/nullsafe/NullsafeRules.mli index 90d495f70..8b5c5cd2b 100644 --- a/infer/src/nullsafe/NullsafeRules.mli +++ b/infer/src/nullsafe/NullsafeRules.mli @@ -39,3 +39,19 @@ val passes_inheritance_rule : type_role -> base:Nullability.t -> overridden:Null NOTE: Rule a) is based on Java covariance rule for the return type. In contrast, rule b) is nullsafe specific as Java does not support type contravariance for method params. *) + +val is_overannotated : lhs:Nullability.t -> rhs_upper_bound:Nullability.t -> bool +(** Check if a type in signature (e.g. return value) can be made more specific. + If an upper bound of `rhs_i` over ALL assignents `lhs = rhs_i` that exist in the program + is a _strict_ subtype of lhs, `lhs`'s type can be narrowed to be that upper bound. + NOTE: This rule is complementatary to assignment rule. + While assignment rule checks a single assignment `lhs = rhs`, this rule + checks checks ALL assignments to `lhs` in the program. + NOTE: Violation of this rule is not a type violation, hence it should never be surfaced as error: + `lhs`'s type can be intentionally made broad by code author + (e.g. to anticipate future changes in the implementation). + Additional heuristits are required to correctly surface overannotated rule to the user. + This rule is useful for some scenarios, especially for nullability code conversions + when it is expected that some signatures were annotated with @Nullable defensively, so + surfacing such cases can improve API and make migration smooth. + *) diff --git a/infer/src/nullsafe/eradicateChecks.ml b/infer/src/nullsafe/eradicateChecks.ml index 1250a1e0f..60461a7df 100644 --- a/infer/src/nullsafe/eradicateChecks.ml +++ b/infer/src/nullsafe/eradicateChecks.ml @@ -162,14 +162,6 @@ let check_field_assignment tenv find_canonical_duplicate curr_pdesc node instr_r (Some instr_ref) loc curr_pdesc -let is_nullable AnnotatedField.{annotated_type} = - match annotated_type.nullability with - | AnnotatedNullability.Nullable _ -> - true - | AnnotatedNullability.Nonnull _ -> - false - - let is_nonnull AnnotatedField.{annotated_type} = match annotated_type.nullability with | AnnotatedNullability.Nullable _ -> @@ -178,14 +170,6 @@ let is_nonnull AnnotatedField.{annotated_type} = true -(* Do we have evidence that the field is annotated as nullable? *) -let is_field_annotated_as_nullable annotated_field_opt = - (* If the field is not present, we optimistically assume it is not nullable. - TODO(T54687014) investigate if this leads to unsoundness issues in practice - *) - Option.exists annotated_field_opt ~f:is_nullable - - (* Do we have evidence that the field is annotated as non-nullable? *) let is_field_annotated_as_nonnull annotated_field_opt = (* If the field is not present, we optimistically assume it is not nullable. @@ -211,9 +195,29 @@ let predicate_holds_for_some_typestate typestate_list field_name ~predicate = List.exists typestate_list ~f:(convert_predicate predicate field_name) -(* Given a list of typestates, does a given predicate about the field hold for all of them? *) -let predicate_holds_for_all_typestates typestate_list field_name ~predicate = - List.for_all typestate_list ~f:(convert_predicate predicate field_name) +(* Given the typestate and the field, what is the upper bound of field nullability in this typestate? + *) +let get_nullability_upper_bound_for_typestate proc_name field_name typestate = + let range_for_field = lookup_field_in_typestate proc_name field_name typestate in + match range_for_field with + | None -> + (* There is no information about the field type in typestate (field was not assigned in all paths). + It gives the most generic upper bound. + *) + Nullability.top + (* We were able to lookup the field. Its nullability gives precise upper bound. *) + | Some (_, inferred_nullability, _) -> + InferredNullability.get_nullability inferred_nullability + + +(* Given the list of typestates (each corresponding to the final result of executing of some function), + and the field, what is the upper bound of field nullability joined over all typestates? + *) +let get_nullability_upper_bound field_name typestate_list = + (* Join upper bounds for all typestates in the list *) + List.fold typestate_list ~init:Nullability.Nonnull ~f:(fun acc (proc_name, typestate) -> + Nullability.join acc + (get_nullability_upper_bound_for_typestate proc_name field_name typestate) ) (** Check field initialization for a given constructor *) @@ -256,11 +260,9 @@ let check_constructor_initialization tenv find_canonical_duplicate curr_construc (* 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, we issue one over-annotated warning per constructor, which does not make a lot of sense. *) - let is_field_assigned_to_nonnull_in_all_constructors () = - predicate_holds_for_all_typestates - (Lazy.force typestates_for_all_constructors_incl_current) field_name - ~predicate:(fun (_, nullability, _) -> InferredNullability.is_nonnull nullability - ) + let field_nullability_upper_bound_over_all_typestates () = + get_nullability_upper_bound field_name + (Lazy.force typestates_for_all_constructors_incl_current) in let should_check_field_initialization = let in_current_class = @@ -283,14 +285,21 @@ let check_constructor_initialization tenv find_canonical_duplicate curr_construc (TypeErr.Field_not_initialized (field_name, curr_constructor_pname)) None loc curr_constructor_pdesc ; (* Check if field is over-annotated. *) - if - Config.eradicate_field_over_annotated - && is_field_annotated_as_nullable annotated_field - && is_field_assigned_to_nonnull_in_all_constructors () - then - report_error tenv find_canonical_duplicate - (TypeErr.Field_over_annotated (field_name, curr_constructor_pname)) - None loc curr_constructor_pdesc ) + match annotated_field with + | None -> + () + | Some annotated_field -> + if + Config.eradicate_field_over_annotated + && NullsafeRules.is_overannotated + ~lhs: + (AnnotatedNullability.get_nullability + annotated_field.annotated_type.nullability) + ~rhs_upper_bound:(field_nullability_upper_bound_over_all_typestates ()) + then + report_error tenv find_canonical_duplicate + (TypeErr.Field_over_annotated (field_name, curr_constructor_pname)) + None loc curr_constructor_pdesc ) in List.iter ~f:do_field fields | None -> @@ -311,18 +320,16 @@ let check_return_not_nullable tenv find_canonical_duplicate loc curr_pname curr_ None loc curr_pdesc -(* TODO(T54308240) Consolidate return over annotated checks in NullsafeRules *) let check_return_overrannotated tenv find_canonical_duplicate loc curr_pname curr_pdesc (ret_signature : AnnotatedSignature.ret_signature) ret_inferred_nullability = - let is_ret_inferred_nonnull = InferredNullability.is_nonnull ret_inferred_nullability in - let is_ret_annotated_nullable = - match ret_signature.ret_annotated_type.nullability with - | AnnotatedNullability.Nonnull _ -> - false - | AnnotatedNullability.Nullable _ -> - true - in - if is_ret_inferred_nonnull && is_ret_annotated_nullable then + (* Returning from a function is essentially an assignment the actual return value to the formal `return` *) + let lhs = AnnotatedNullability.get_nullability ret_signature.ret_annotated_type.nullability in + (* In our CFG implementation, there is only one place where we return from a function + (all execution flow joins are already made), hence inferreed nullability of returns gives us + correct upper bound. + *) + let rhs_upper_bound = InferredNullability.get_nullability ret_inferred_nullability in + if NullsafeRules.is_overannotated ~lhs ~rhs_upper_bound then report_error tenv find_canonical_duplicate (TypeErr.Return_over_annotated curr_pname) None loc curr_pdesc