diff --git a/infer/src/nullsafe/AnnotatedSignature.ml b/infer/src/nullsafe/AnnotatedSignature.ml index 7485329eb..d0c04959c 100644 --- a/infer/src/nullsafe/AnnotatedSignature.ml +++ b/infer/src/nullsafe/AnnotatedSignature.ml @@ -8,30 +8,81 @@ open! IStd module F = Format module L = Logging -type t = {ret: Annot.Item.t * Typ.t; params: (Mangled.t * Annot.Item.t * Typ.t) list} +(* TODO(T54088319) remove Annot.Item.t from t: + 1. For everything dealing with nullability, use info from NullsafeType instead. + 2. For other annotations guiding Nullsafe behavior, introduce corresponding datatypes: + a. Known ret value annotations (if any) + b. Known param annotations + c. Known method-level annotations. +*) +type t = + {ret: Annot.Item.t * NullsafeType.t; params: (Mangled.t * Annot.Item.t * NullsafeType.t) list} [@@deriving compare] +(* get nullability of method's return type given its annotations and information about its params *) +let nullability_for_return ia ~has_propagates_nullable_in_param = + let nullability = NullsafeType.nullability_of_annot_item ia in + (* if any param is annotated with propagates nullable, then the result is nullable *) + match nullability with + | NullsafeType.Nullable _ -> + nullability (* We already know it is nullable - lets not overwrite the origin *) + | _ when has_propagates_nullable_in_param -> + (* if any params is propagates nullable, the return type can be only nullable *) + NullsafeType.Nullable NullsafeType.HasPropagatesNullableInParam + | _ -> + nullability + + +(* Given annotations for method signature, extract nullability information + for return type and params *) +let extract_nullability return_annotation param_annotations = + let params_nullability = List.map param_annotations ~f:NullsafeType.nullability_of_annot_item in + let has_propagates_nullable_in_param = + List.exists params_nullability ~f:(function + | NullsafeType.Nullable NullsafeType.AnnotatedPropagatesNullable -> + true + | _ -> + false ) + in + let return_nullability = + nullability_for_return return_annotation ~has_propagates_nullable_in_param + in + (return_nullability, params_nullability) + + let get proc_attributes : t = let method_annotation = proc_attributes.ProcAttributes.method_annotation in let formals = proc_attributes.ProcAttributes.formals in let ret_type = proc_attributes.ProcAttributes.ret_type in let Annot.Method.{return; params} = method_annotation in - let natl = - let rec extract ial parl = + (* zip formal params with annotation *) + let params_with_annotations = + let rec zip_params ial parl = match (ial, parl) with - | ia :: ial', (name, typ) :: parl' -> - (name, ia, typ) :: extract ial' parl' - | [], (name, typ) :: parl' -> - (name, Annot.Item.empty, typ) :: extract [] parl' + | ia :: ial', param :: parl' -> + (param, ia) :: zip_params ial' parl' + | [], param :: parl' -> + (* List of annotations exhausted before the list of params - + treat lack of annotation info as an empty annotation *) + (param, Annot.Item.empty) :: zip_params [] parl' | [], [] -> [] | _ :: _, [] -> + (* List of params exhausted before the list of annotations - + this should never happen *) assert false in - List.rev (extract (List.rev params) (List.rev formals)) + List.rev (zip_params (List.rev params) (List.rev formals)) + in + let _, param_annotations = List.unzip params_with_annotations in + let return_nullability, params_nullability = extract_nullability return param_annotations in + let ret = (return, NullsafeType.{nullability= return_nullability; typ= ret_type}) in + let params = + List.zip_exn params_with_annotations params_nullability + |> List.map ~f:(function ((mangled, typ), annot), nullability -> + (mangled, annot, NullsafeType.{nullability; typ}) ) in - let annotated_signature = {ret= (return, ret_type); params= natl} in - annotated_signature + {ret; params} let param_has_annot predicate pvar ann_sig = @@ -43,11 +94,11 @@ let param_has_annot predicate pvar ann_sig = let pp proc_name fmt annotated_signature = let pp_ia fmt ia = if ia <> [] then F.fprintf fmt "%a " Annot.Item.pp ia in - let pp_annotated_param fmt (p, ia, t) = - F.fprintf fmt " %a%a %a" pp_ia ia (Typ.pp_full Pp.text) t Mangled.pp p + let pp_annotated_param fmt (mangled, ia, nullsafe_type) = + F.fprintf fmt " %a%a %a" pp_ia ia NullsafeType.pp nullsafe_type Mangled.pp mangled in - let ia, ret_type = annotated_signature.ret in - F.fprintf fmt "%a%a %s (%a )" pp_ia ia (Typ.pp_full Pp.text) ret_type + let ia, nullsafe_type = annotated_signature.ret in + F.fprintf fmt "%a%a %s (%a )" pp_ia ia NullsafeType.pp nullsafe_type (Typ.Procname.to_simplified_string proc_name) (Pp.comma_seq pp_annotated_param) annotated_signature.params @@ -60,6 +111,7 @@ let mk_ia_nullable ia = let mark_ia_nullability ia x = if x then mk_ia_nullable ia else ia +(* TODO(T54088319) Make this update NullsafeType.t as well*) let mark_nullability proc_name asig (b, bs) = let ia, t = asig.ret in let ret' = (mark_ia_nullability ia b, t) in diff --git a/infer/src/nullsafe/AnnotatedSignature.mli b/infer/src/nullsafe/AnnotatedSignature.mli index e81bb201c..012b74ec0 100644 --- a/infer/src/nullsafe/AnnotatedSignature.mli +++ b/infer/src/nullsafe/AnnotatedSignature.mli @@ -10,8 +10,8 @@ open! IStd type t = - { ret: Annot.Item.t * Typ.t (** Annotated return type. *) - ; params: (Mangled.t * Annot.Item.t * Typ.t) list (** Annotated parameters. *) } + { ret: Annot.Item.t * NullsafeType.t (** Annotated return type. *) + ; params: (Mangled.t * Annot.Item.t * NullsafeType.t) list (** Annotated parameters. *) } [@@deriving compare] val param_has_annot : (Annot.Item.t -> bool) -> Pvar.t -> t -> bool diff --git a/infer/src/nullsafe/NullsafeType.ml b/infer/src/nullsafe/NullsafeType.ml new file mode 100644 index 000000000..c8fbe8f14 --- /dev/null +++ b/infer/src/nullsafe/NullsafeType.ml @@ -0,0 +1,81 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd +module F = Format + +(** Representation of a (non local) type in Java program, with added information about its nullability, + according to the source code. + Nullability information might come either from explicit annotations, or from other sources, + including conventions about defaults. + Note that nullsafe omits Nullability information in types used for local variable declarations: + this information is inferred according to flow-sensitive inferrence rule. +*) + +(* TODO(T52947663) add notion of unknown nullability *) +type nullability = Nullable of nullable_origin | Nonnull of nonnull_origin [@@deriving compare] + +and nullable_origin = + | AnnotatedNullable (** The type is expicitly annotated with @Nullable in the code *) + | AnnotatedPropagatesNullable + (** If a function param is annotated as @PropagatesNullable, this param is automatically nullable *) + | HasPropagatesNullableInParam + (** If a method has at least one param marked as @PropagatesNullable, return value is automatically nullable *) + | ModelledNullable (** nullsafe knows it is nullable via its internal models *) +[@@deriving compare] + +and nonnull_origin = + | AnnotatedNonnull + (** The type is explicitly annotated as non nullable via one of nonnull annotations Nullsafe recognizes *) + | NotAnnotatedHenceNullableMode + (** Infer was run in mode where all not annotated (non local) types are treated as non nullable *) + | ModelledNonnull (** nullsafe knows it is non-nullable via its internal models *) +[@@deriving compare] + +type t = {nullability: nullability; typ: Typ.t} [@@deriving compare] + +let pp fmt {nullability; typ} = + let string_of_nullable_origin nullable_origin = + match nullable_origin with + | AnnotatedNullable -> + "@" + | AnnotatedPropagatesNullable -> + "propagates" + | HasPropagatesNullableInParam -> + "<-propagates" + | ModelledNullable -> + "model" + in + let string_of_nonnull_origin nonnull_origin = + match nonnull_origin with + | AnnotatedNonnull -> + "@" + | NotAnnotatedHenceNullableMode -> + "default" + | ModelledNonnull -> + "model" + in + let pp_nullability fmt nullability = + match nullability with + | Nullable nullable_origin -> + F.fprintf fmt "Nullable[%s]" (string_of_nullable_origin nullable_origin) + | Nonnull nonnull_origin -> + F.fprintf fmt "Nonnull[%s]" (string_of_nonnull_origin nonnull_origin) + in + F.fprintf fmt "%a %a" pp_nullability nullability (Typ.pp_full Pp.text) typ + + +let nullability_of_annot_item ia = + if Annotations.ia_is_nullable ia then + let nullable_origin = + if Annotations.ia_is_propagates_nullable ia then AnnotatedPropagatesNullable + else AnnotatedNullable + in + Nullable nullable_origin + else if Annotations.ia_is_nonnull ia then Nonnull AnnotatedNonnull + (* Currently, we treat not annotated types as nonnull *) + else Nonnull NotAnnotatedHenceNullableMode diff --git a/infer/src/nullsafe/NullsafeType.mli b/infer/src/nullsafe/NullsafeType.mli new file mode 100644 index 000000000..1c6a9ae8d --- /dev/null +++ b/infer/src/nullsafe/NullsafeType.mli @@ -0,0 +1,42 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd + +(** Representation of a type in Java program, but with added information about its nullability. + Nullability information might come either from explicit annotations, or from other sources, + including conventions about defaults. +*) + +type nullability = Nullable of nullable_origin | Nonnull of nonnull_origin [@@deriving compare] + +and nullable_origin = + | AnnotatedNullable (** The type is expicitly annotated with @Nullable in the code *) + | AnnotatedPropagatesNullable + (** If a function param is annotated as @PropagatesNullable, this param is automatically nullable *) + | HasPropagatesNullableInParam + (** If a method has at least one param marked as @PropagatesNullable, return value is automatically nullable *) + | ModelledNullable (** nullsafe knows it is nullable via its internal models *) +[@@deriving compare] + +and nonnull_origin = + | AnnotatedNonnull + (** The type is explicitly annotated as non nullable via one of nonnull annotations Nullsafe recognizes *) + | NotAnnotatedHenceNullableMode + (** Infer was run in mode where all not annotated (non local) types are treated as non nullable *) + | ModelledNonnull (** nullsafe knows it is non-nullable via its internal models *) +[@@deriving compare] + +type t = {nullability: nullability; typ: Typ.t} [@@deriving compare] + +val pp : Format.formatter -> t -> unit + +val nullability_of_annot_item : Annot.Item.t -> nullability +(** Converts the information from the annotation to nullability. + NOTE: it does not take into account models etc., so this is intended to be used + as a helper function for more high-level annotation processing. + *) diff --git a/infer/src/nullsafe/eradicate.ml b/infer/src/nullsafe/eradicate.ml index 4c94a7d5b..91a85e796 100644 --- a/infer/src/nullsafe/eradicate.ml +++ b/infer/src/nullsafe/eradicate.ml @@ -33,7 +33,7 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct let callback1 tenv find_canonical_duplicate calls_this checks idenv curr_pname curr_pdesc annotated_signature linereader proc_loc : bool * TypeState.t option = let mk s = Pvar.mk s curr_pname in - let add_formal typestate (s, ia, typ) = + let add_formal typestate (s, ia, NullsafeType.{typ}) = let pvar = mk s in let ta = let origin = TypeOrigin.Formal s in @@ -48,19 +48,20 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct (* Check the nullable flag computed for the return value and report inconsistencies. *) let check_return find_canonical_duplicate exit_node final_typestate annotated_signature loc : unit = - let _, ret_type = annotated_signature.AnnotatedSignature.ret in + let _, ret_nullsafe_type = annotated_signature.AnnotatedSignature.ret in let ret_pvar = Procdesc.get_ret_var curr_pdesc in let ret_range = TypeState.lookup_pvar ret_pvar final_typestate in let typ_found_opt = match ret_range with Some (typ_found, _, _) -> Some typ_found | None -> None in + (* TODO(T54088319): model this in NullsafeType.nullability *) let ret_implicitly_nullable = - String.equal (PatternMatch.get_type_name ret_type) "java.lang.Void" + String.equal (PatternMatch.get_type_name ret_nullsafe_type.typ) "java.lang.Void" in State.set_node exit_node ; if checks.TypeCheck.check_ret_type <> [] then List.iter - ~f:(fun f -> f curr_pname curr_pdesc ret_type typ_found_opt loc) + ~f:(fun f -> f curr_pname curr_pdesc ret_nullsafe_type.typ typ_found_opt loc) checks.TypeCheck.check_ret_type ; if checks.TypeCheck.eradicate then EradicateChecks.check_return_annotation tenv find_canonical_duplicate curr_pdesc ret_range diff --git a/infer/src/nullsafe/eradicateChecks.ml b/infer/src/nullsafe/eradicateChecks.ml index 2615cbe3a..a3ce7213d 100644 --- a/infer/src/nullsafe/eradicateChecks.ml +++ b/infer/src/nullsafe/eradicateChecks.ml @@ -13,6 +13,7 @@ let get_field_annotation tenv fn typ = let lookup = Tenv.lookup tenv in Typ.Struct.get_field_type_and_annotation ~lookup fn typ + let report_error tenv = TypeErr.report_error tenv (EradicateCheckers.report_error tenv) let explain_expr tenv node e = diff --git a/infer/src/nullsafe/typeCheck.ml b/infer/src/nullsafe/typeCheck.ml index eb2636783..4c877ce23 100644 --- a/infer/src/nullsafe/typeCheck.ml +++ b/infer/src/nullsafe/typeCheck.ml @@ -531,7 +531,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p let is_anonymous_inner_class_constructor = Typ.Procname.Java.is_anonymous_inner_class_constructor callee_pname_java in - let do_return (ret_ta, ret_typ) loc' typestate' = + let do_return (ret_ta, NullsafeType.{typ= ret_typ}) loc' typestate' = let mk_return_range () = (ret_typ, ret_ta, [loc']) in let id = fst ret_id_typ in TypeState.add_id id (mk_return_range ()) typestate' @@ -682,7 +682,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p in let typestate_after_call, resolved_ret = let resolve_param i (sparam, cparam) = - let s1, ia1, t1 = sparam in + let s1, ia1, NullsafeType.{typ= t1} = sparam in let (orig_e2, e2), t2 = cparam in let ta1 = TypeAnnotation.from_item_annotation ia1 (TypeOrigin.Formal s1) in let _, ta2, _ = diff --git a/infer/src/nullsafe/typeErr.ml b/infer/src/nullsafe/typeErr.ml index 57497d611..b960661ac 100644 --- a/infer/src/nullsafe/typeErr.ml +++ b/infer/src/nullsafe/typeErr.ml @@ -178,7 +178,7 @@ module Severity = struct let this_type_get_severity tenv (signature : AnnotatedSignature.t) = match signature.params with - | (p, _, this_type) :: _ when Mangled.is_this p -> + | (p, _, NullsafeType.{typ= this_type}) :: _ when Mangled.is_this p -> Option.bind ~f:get_severity (PatternMatch.type_get_annotation tenv this_type) | _ -> None