From 633186c41e9727fe13f284750f51ed2f64f84e90 Mon Sep 17 00:00:00 2001 From: Mitya Lyubarskiy Date: Wed, 18 Sep 2019 08:37:02 -0700 Subject: [PATCH] [nullsafe] Introduce NullsafeType abstraction Summary: This is a central abstraction for coming future unknown nullability support. # Context Annot.ml is a low-level module: - it contains lists of raw (string) annotations - no algebraic datatypes for annotations - it mixes annotations that Nullsafe should be aware of with all sorts of other annotations - some annotations make sense for return values, some make sense for params, and some make sense for methods. But, most importantly, it does not contain information about source of an annotation, making it hard to distinct things like "Nonnull as default" vs "Nonnull as explicitly annotated" vs "Nonnull as modelled". Ditto for nullable. Because of this, it is tricky to introduce unknown nullability in an elegant way. Let's get rid of using Annot.Item.t in nullsafe code in the following way: - Move nullability information associated with the Java type to a dedicated algebraic DT. - Split other annotations that are important for nullsafe into param flags, ret value flags, and method flags, and introduce corresponding datatypes. # This diff This diff introduces NullsafeType and adds this to AnnotatedSignature. It is not used yet, hence the diff is a no-op. In future diffs, we are going to (see also TODOs in the code): - actually use this information instead of accessing Annot.item - add more information to AnnotatedSignature - remove Annot.item from AnnnotatedSignature - when this is done, introduce notion of unknown nullability. Reviewed By: ngorogiannis Differential Revision: D17420595 fbshipit-source-id: b30706d9b --- infer/src/nullsafe/AnnotatedSignature.ml | 80 ++++++++++++++++++---- infer/src/nullsafe/AnnotatedSignature.mli | 4 +- infer/src/nullsafe/NullsafeType.ml | 81 +++++++++++++++++++++++ infer/src/nullsafe/NullsafeType.mli | 42 ++++++++++++ infer/src/nullsafe/eradicate.ml | 9 +-- infer/src/nullsafe/eradicateChecks.ml | 1 + infer/src/nullsafe/typeCheck.ml | 4 +- infer/src/nullsafe/typeErr.ml | 2 +- 8 files changed, 200 insertions(+), 23 deletions(-) create mode 100644 infer/src/nullsafe/NullsafeType.ml create mode 100644 infer/src/nullsafe/NullsafeType.mli 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