diff --git a/infer/annotations/src/main/java/com/facebook/infer/annotation/NullsafeStrict.java b/infer/annotations/src/main/java/com/facebook/infer/annotation/NullsafeStrict.java new file mode 100644 index 000000000..0f5b0fae1 --- /dev/null +++ b/infer/annotations/src/main/java/com/facebook/infer/annotation/NullsafeStrict.java @@ -0,0 +1,24 @@ +/* + * 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. + */ + +package com.facebook.infer.annotation; + +import java.lang.annotation.ElementType; +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; +import java.lang.annotation.Target; + +/** + * A class annotated with @NullsafeStrict means more exsaustive checks for nullsafe. The main + * invariant of strict mode is the following: If the function passes @NullsafeStrict check and its + * return value is NOT annotated as @Nullable, then the function does not indeed return nulls, + * subject to unsoundness issues (which should either be fixed, or should rarely happen in + * practice). + */ +@Retention(RetentionPolicy.CLASS) +@Target({ElementType.TYPE, ElementType.FIELD, ElementType.CONSTRUCTOR, ElementType.METHOD}) +public @interface NullsafeStrict {} diff --git a/infer/src/biabduction/Rearrange.ml b/infer/src/biabduction/Rearrange.ml index c1d306138..99141c429 100644 --- a/infer/src/biabduction/Rearrange.ml +++ b/infer/src/biabduction/Rearrange.ml @@ -1489,7 +1489,9 @@ let is_weak_captured_var pdesc var_name = let var_has_annotation ?(check_weak_captured_var = false) pdesc is_annotation pvar = let is_weak_captured_var = is_weak_captured_var pdesc (Pvar.to_string pvar) in - let ann_sig = Models.get_modelled_annotated_signature (Procdesc.get_attributes pdesc) in + let ann_sig = + Models.get_modelled_annotated_signature_for_biabduction (Procdesc.get_attributes pdesc) + in AnnotatedSignature.param_has_annot is_annotation pvar ann_sig || (check_weak_captured_var && is_weak_captured_var) diff --git a/infer/src/checkers/annotations.ml b/infer/src/checkers/annotations.ml index 5fcc4f272..827eba69d 100644 --- a/infer/src/checkers/annotations.ml +++ b/infer/src/checkers/annotations.ml @@ -59,6 +59,8 @@ let no_allocation = "NoAllocation" let nullable = "Nullable" +let nullsafe_strict = "NullsafeStrict" + let mainthread = "MainThread" let nonblocking = "NonBlocking" @@ -124,9 +126,9 @@ let ma_has_annotation_with ({return; params} : Annot.Method.t) (predicate : Anno let annot_ends_with ({class_name} : Annot.t) ann_name = String.is_suffix class_name ~suffix:ann_name && - (* here, [class_name] ends with [ann_name] but it could be that it's just a suffix - of the last dot-component of [class_name], eg [class_name="x.y.z.a.bcd"] and - [ann_name="cd"]; in that case we want to fail the check, so we check that the + (* here, [class_name] ends with [ann_name] but it could be that it's just a suffix + of the last dot-component of [class_name], eg [class_name="x.y.z.a.bcd"] and + [ann_name="cd"]; in that case we want to fail the check, so we check that the character just before the match is indeed a dot (or there is no dot at all). *) let dot_pos = String.(length class_name - length ann_name - 1) in Int.is_negative dot_pos || Char.equal '.' class_name.[dot_pos] @@ -176,6 +178,8 @@ let ia_is_nullable ia = ia_ends_with ia nullable || ia_is_propagates_nullable ia let ia_is_nonnull ia = List.exists ~f:(ia_ends_with ia) [nonnull; notnull; camel_nonnull] +let ia_is_nullsafe_strict ia = ia_ends_with ia nullsafe_strict + let ia_is_false_on_null ia = ia_ends_with ia false_on_null let ia_is_returns_ownership ia = ia_ends_with ia returns_ownership diff --git a/infer/src/checkers/annotations.mli b/infer/src/checkers/annotations.mli index 103040b7c..e6bd8c684 100644 --- a/infer/src/checkers/annotations.mli +++ b/infer/src/checkers/annotations.mli @@ -76,6 +76,8 @@ val ia_is_nonnull : Annot.Item.t -> bool val ia_is_nullable : Annot.Item.t -> bool +val ia_is_nullsafe_strict : Annot.Item.t -> bool + val ia_is_true_on_null : Annot.Item.t -> bool val ia_is_expensive : Annot.Item.t -> bool diff --git a/infer/src/nullsafe/AnnotatedField.ml b/infer/src/nullsafe/AnnotatedField.ml index 214824d43..02bde8fc4 100644 --- a/infer/src/nullsafe/AnnotatedField.ml +++ b/infer/src/nullsafe/AnnotatedField.ml @@ -12,12 +12,23 @@ open! IStd *) type t = {annotation_deprecated: Annot.Item.t; annotated_type: AnnotatedType.t} +let is_class_in_strict_mode tenv typ = + match PatternMatch.type_get_annotation tenv typ with + | Some ia -> + Annotations.ia_is_nullsafe_strict ia + | None -> + false + + let get tenv fn typ = let lookup = Tenv.lookup tenv in + (* We currently don't support field-level strict mode annotation, so fetch it from class *) + let is_strict_mode = is_class_in_strict_mode tenv typ in let type_and_annotation_to_field_type (typ, annotation) = { annotation_deprecated= annotation ; annotated_type= - AnnotatedType.{nullability= AnnotatedNullability.of_annot_item annotation; typ} } + AnnotatedType. + {nullability= AnnotatedNullability.of_annot_item annotation ~is_strict_mode; typ} } in Option.map (Typ.Struct.get_field_type_and_annotation ~lookup fn typ) diff --git a/infer/src/nullsafe/AnnotatedNullability.ml b/infer/src/nullsafe/AnnotatedNullability.ml index 5da5c1a14..c067c031e 100644 --- a/infer/src/nullsafe/AnnotatedNullability.ml +++ b/infer/src/nullsafe/AnnotatedNullability.ml @@ -39,6 +39,7 @@ and declared_nonnull_origin = and nonnull_origin = | ModelledNonnull (** nullsafe knows it is non-nullable via its internal models *) + | StrictMode (** under strict mode we consider non-null declarations to be trusted *) [@@deriving compare] let get_nullability = function @@ -66,7 +67,7 @@ let pp fmt t = match origin with AnnotatedNonnull -> "@" | ImplicitlyNonnull -> "implicit" in let string_of_nonnull_origin nonnull_origin = - match nonnull_origin with ModelledNonnull -> "model" + match nonnull_origin with ModelledNonnull -> "model" | StrictMode -> "strict" in match t with | Nullable origin -> @@ -77,13 +78,14 @@ let pp fmt t = F.fprintf fmt "Nonnull[%s]" (string_of_nonnull_origin origin) -let of_annot_item ia = +let of_annot_item ~is_strict_mode 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 is_strict_mode then Nonnull StrictMode else if Annotations.ia_is_nonnull ia then DeclaredNonnull AnnotatedNonnull (* Currently, we treat not annotated types as nonnull *) else DeclaredNonnull ImplicitlyNonnull diff --git a/infer/src/nullsafe/AnnotatedNullability.mli b/infer/src/nullsafe/AnnotatedNullability.mli index 55b1e42e7..17a460b26 100644 --- a/infer/src/nullsafe/AnnotatedNullability.mli +++ b/infer/src/nullsafe/AnnotatedNullability.mli @@ -42,11 +42,12 @@ and declared_nonnull_origin = and nonnull_origin = | ModelledNonnull (** nullsafe knows it is non-nullable via its internal models *) + | StrictMode (** under strict mode we consider non-null declarations to be trusted *) [@@deriving compare] val get_nullability : t -> Nullability.t -val of_annot_item : Annot.Item.t -> t +val of_annot_item : is_strict_mode:bool -> Annot.Item.t -> t (** 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/AnnotatedSignature.ml b/infer/src/nullsafe/AnnotatedSignature.ml index ee0cdce2f..d72a212f0 100644 --- a/infer/src/nullsafe/AnnotatedSignature.ml +++ b/infer/src/nullsafe/AnnotatedSignature.ml @@ -15,7 +15,8 @@ module L = Logging c. Known method-level annotations. *) -type t = {ret: ret_signature; params: param_signature list} [@@deriving compare] +type t = {is_strict_mode: bool; ret: ret_signature; params: param_signature list} +[@@deriving compare] and ret_signature = {ret_annotation_deprecated: Annot.Item.t; ret_annotated_type: AnnotatedType.t} [@@deriving compare] @@ -27,8 +28,8 @@ and param_signature = [@@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 = AnnotatedNullability.of_annot_item ia in +let nullability_for_return ia ~is_strict_mode ~has_propagates_nullable_in_param = + let nullability = AnnotatedNullability.of_annot_item ~is_strict_mode ia in (* if any param is annotated with propagates nullable, then the result is nullable *) match nullability with | AnnotatedNullability.Nullable _ -> @@ -42,8 +43,10 @@ let nullability_for_return ia ~has_propagates_nullable_in_param = (* 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:AnnotatedNullability.of_annot_item in +let extract_nullability ~is_strict_mode return_annotation param_annotations = + let params_nullability = + List.map param_annotations ~f:(AnnotatedNullability.of_annot_item ~is_strict_mode) + in let has_propagates_nullable_in_param = List.exists params_nullability ~f:(function | AnnotatedNullability.Nullable AnnotatedNullability.AnnotatedPropagatesNullable -> @@ -52,12 +55,12 @@ let extract_nullability return_annotation param_annotations = false ) in let return_nullability = - nullability_for_return return_annotation ~has_propagates_nullable_in_param + nullability_for_return return_annotation ~is_strict_mode ~has_propagates_nullable_in_param in (return_nullability, params_nullability) -let get proc_attributes : t = +let get ~is_strict_mode proc_attributes : t = let Annot.Method.{return= return_annotation; params= original_params_annotation} = proc_attributes.ProcAttributes.method_annotation in @@ -84,7 +87,7 @@ let get proc_attributes : t = in let _, final_params_annotation = List.unzip params_with_annotations in let return_nullability, params_nullability = - extract_nullability return_annotation final_params_annotation + extract_nullability ~is_strict_mode return_annotation final_params_annotation in let ret = { ret_annotation_deprecated= return_annotation @@ -97,7 +100,7 @@ let get proc_attributes : t = ; mangled ; param_annotated_type= AnnotatedType.{nullability; typ} } ) in - {ret; params} + {is_strict_mode; ret; params} let param_has_annot predicate pvar ann_sig = @@ -114,7 +117,9 @@ let pp proc_name fmt annotated_signature = param_annotated_type Mangled.pp mangled in let {ret_annotation_deprecated; ret_annotated_type} = annotated_signature.ret in - F.fprintf fmt "%a%a %a (%a )" pp_ia ret_annotation_deprecated AnnotatedType.pp ret_annotated_type + let mode_as_string = if annotated_signature.is_strict_mode then "Strict" else "Def" in + F.fprintf fmt "[%s] %a%a %a (%a )" mode_as_string pp_ia ret_annotation_deprecated + AnnotatedType.pp ret_annotated_type (Typ.Procname.pp_simplified_string ~withclass:false) proc_name (Pp.comma_seq pp_annotated_param) annotated_signature.params @@ -174,4 +179,6 @@ let set_modelled_nullability proc_name asig (nullability_for_ret, params_nullabi in model_param_nullability asig.params params_nullability in - {ret= set_modelled_nullability_for_ret asig.ret nullability_for_ret; params= final_params} + { asig with + ret= set_modelled_nullability_for_ret asig.ret nullability_for_ret + ; params= final_params } diff --git a/infer/src/nullsafe/AnnotatedSignature.mli b/infer/src/nullsafe/AnnotatedSignature.mli index b3cc94f70..37de004ef 100644 --- a/infer/src/nullsafe/AnnotatedSignature.mli +++ b/infer/src/nullsafe/AnnotatedSignature.mli @@ -9,7 +9,8 @@ open! IStd -type t = {ret: ret_signature; params: param_signature list} [@@deriving compare] +type t = {is_strict_mode: bool; ret: ret_signature; params: param_signature list} +[@@deriving compare] and ret_signature = {ret_annotation_deprecated: Annot.Item.t; ret_annotated_type: AnnotatedType.t} [@@deriving compare] @@ -26,7 +27,7 @@ val param_has_annot : (Annot.Item.t -> bool) -> Pvar.t -> t -> bool val set_modelled_nullability : Typ.Procname.t -> t -> bool * bool list -> t (** Override nullability for a function signature given its modelled nullability (for ret value and params) *) -val get : ProcAttributes.t -> t +val get : is_strict_mode:bool -> ProcAttributes.t -> t (** Get a method signature with annotations from a proc_attributes. *) val pp : Typ.Procname.t -> Format.formatter -> t -> unit diff --git a/infer/src/nullsafe/AssignmentRule.ml b/infer/src/nullsafe/AssignmentRule.ml index 41abeb714..406efae6a 100644 --- a/infer/src/nullsafe/AssignmentRule.ml +++ b/infer/src/nullsafe/AssignmentRule.ml @@ -6,7 +6,8 @@ *) open! IStd -type violation = {lhs: Nullability.t; rhs: Nullability.t} [@@deriving compare] +type violation = {is_strict_mode: bool; lhs: Nullability.t; rhs: Nullability.t} +[@@deriving compare] type assignment_type = | PassingParamToFunction of @@ -17,15 +18,24 @@ type assignment_type = | ReturningFromFunction of Typ.Procname.t [@@deriving compare] -let is_whitelisted_assignment ~lhs ~rhs = - match (lhs, rhs) with Nullability.Nonnull, Nullability.DeclaredNonnull -> true | _ -> false +let is_whitelisted_assignment ~is_strict_mode ~lhs ~rhs = + match (is_strict_mode, lhs, rhs) with + | false, Nullability.Nonnull, Nullability.DeclaredNonnull -> + (* We allow DeclaredNonnull -> Nonnull conversion outside of strict mode for better adoption. + Otherwise using strictified classes in non-strict context becomes a pain because + of extra warnings. + *) + true + | _ -> + false -let check ~lhs ~rhs = +let check ~is_strict_mode ~lhs ~rhs = let is_allowed_assignment = - Nullability.is_subtype ~subtype:rhs ~supertype:lhs || is_whitelisted_assignment ~lhs ~rhs + Nullability.is_subtype ~subtype:rhs ~supertype:lhs + || is_whitelisted_assignment ~is_strict_mode ~lhs ~rhs in - Result.ok_if_true is_allowed_assignment ~error:{lhs; rhs} + Result.ok_if_true is_allowed_assignment ~error:{is_strict_mode; lhs; rhs} let violation_description _ assignment_type ~rhs_origin_descr = diff --git a/infer/src/nullsafe/AssignmentRule.mli b/infer/src/nullsafe/AssignmentRule.mli index 6a77f2b3a..9679ad635 100644 --- a/infer/src/nullsafe/AssignmentRule.mli +++ b/infer/src/nullsafe/AssignmentRule.mli @@ -13,7 +13,8 @@ open! IStd type violation [@@deriving compare] -val check : lhs:Nullability.t -> rhs:Nullability.t -> (unit, violation) result +val check : + is_strict_mode:bool -> lhs:Nullability.t -> rhs:Nullability.t -> (unit, violation) result type assignment_type = | PassingParamToFunction of diff --git a/infer/src/nullsafe/DereferenceRule.ml b/infer/src/nullsafe/DereferenceRule.ml index 28f628574..15f062820 100644 --- a/infer/src/nullsafe/DereferenceRule.ml +++ b/infer/src/nullsafe/DereferenceRule.ml @@ -15,10 +15,13 @@ type dereference_type = | ArrayLengthAccess [@@deriving compare] -let check = function - | Nullability.Nullable as nullability -> +let check ~is_strict_mode nullability = + match nullability with + | Nullability.Nullable -> Error nullability - | Nullability.DeclaredNonnull | Nullability.Nonnull -> + | Nullability.DeclaredNonnull -> + if is_strict_mode then Error nullability else Ok () + | Nullability.Nonnull -> Ok () diff --git a/infer/src/nullsafe/DereferenceRule.mli b/infer/src/nullsafe/DereferenceRule.mli index 8eda8a339..2f6f69ca6 100644 --- a/infer/src/nullsafe/DereferenceRule.mli +++ b/infer/src/nullsafe/DereferenceRule.mli @@ -12,7 +12,7 @@ open! IStd type violation [@@deriving compare] -val check : Nullability.t -> (unit, violation) result +val check : is_strict_mode:bool -> Nullability.t -> (unit, violation) result type dereference_type = | MethodCall of Typ.Procname.t diff --git a/infer/src/nullsafe/Initializers.ml b/infer/src/nullsafe/Initializers.ml index 34af00e74..f53be88cc 100644 --- a/infer/src/nullsafe/Initializers.ml +++ b/infer/src/nullsafe/Initializers.ml @@ -115,7 +115,7 @@ let final_initializer_typestates_lazy tenv curr_pname curr_pdesc get_procs_in_fi PatternMatch.method_is_initializer tenv proc_attributes || let ia = - (Models.get_modelled_annotated_signature proc_attributes).AnnotatedSignature.ret + (Models.get_modelled_annotated_signature tenv proc_attributes).AnnotatedSignature.ret .ret_annotation_deprecated in Annotations.ia_is_initializer ia diff --git a/infer/src/nullsafe/eradicate.ml b/infer/src/nullsafe/eradicate.ml index f535cd01d..cca5d8d02 100644 --- a/infer/src/nullsafe/eradicate.ml +++ b/infer/src/nullsafe/eradicate.ml @@ -113,12 +113,10 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct (!calls_this, None) - let callback2 calls_this checks {Callbacks.summary; exe_env; get_procs_in_file} + let callback2 tenv curr_pname calls_this checks {Callbacks.summary; get_procs_in_file} annotated_signature linereader proc_loc : unit = let curr_pdesc = Summary.get_proc_desc summary in let idenv = Idenv.create curr_pdesc in - let curr_pname = Summary.get_proc_name summary in - let tenv = Exe_env.get_tenv exe_env curr_pname in let find_duplicate_nodes = State.mk_find_duplicate_nodes curr_pdesc in let find_canonical_duplicate node = let duplicate_nodes = find_duplicate_nodes node in @@ -131,7 +129,7 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct (ann_sig, loc, idenv_pn) | None -> let ann_sig = - Models.get_modelled_annotated_signature (Procdesc.get_attributes pdesc) + Models.get_modelled_annotated_signature tenv (Procdesc.get_attributes pdesc) in let loc = Procdesc.get_loc pdesc in (ann_sig, loc, Idenv.create pdesc) @@ -183,6 +181,8 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct let proc_desc = Summary.get_proc_desc summary in let proc_name = Procdesc.get_proc_name proc_desc in let calls_this = ref false in + let curr_pname = Summary.get_proc_name summary in + let tenv = Exe_env.get_tenv callback_args.exe_env curr_pname in let filter_special_cases () = if ( match proc_name with @@ -195,7 +195,7 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct then None else let annotated_signature = - Models.get_modelled_annotated_signature (Procdesc.get_attributes proc_desc) + Models.get_modelled_annotated_signature tenv (Procdesc.get_attributes proc_desc) in Some annotated_signature in @@ -207,7 +207,8 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct let linereader = Printer.LineReader.create () in if Config.eradicate_verbose then L.result "%a@." (AnnotatedSignature.pp proc_name) annotated_signature ; - callback2 calls_this checks callback_args annotated_signature linereader loc ) ; + callback2 tenv curr_pname calls_this checks callback_args annotated_signature linereader + loc ) ; summary end diff --git a/infer/src/nullsafe/eradicateChecks.ml b/infer/src/nullsafe/eradicateChecks.ml index 26c67d557..986eb4acf 100644 --- a/infer/src/nullsafe/eradicateChecks.ml +++ b/infer/src/nullsafe/eradicateChecks.ml @@ -26,10 +26,11 @@ let is_virtual = function false -let check_object_dereference tenv find_canonical_duplicate curr_pname node instr_ref object_exp - dereference_type inferred_nullability loc = +let check_object_dereference ~is_strict_mode tenv find_canonical_duplicate curr_pname node + instr_ref object_exp dereference_type inferred_nullability loc = Result.iter_error - (DereferenceRule.check (InferredNullability.get_nullability inferred_nullability)) + (DereferenceRule.check ~is_strict_mode + (InferredNullability.get_nullability inferred_nullability)) ~f:(fun dereference_violation -> let origin_descr = InferredNullability.descr_origin inferred_nullability in let nullable_object_descr = explain_expr tenv node object_exp in @@ -115,8 +116,8 @@ let check_nonzero tenv find_canonical_duplicate = (** Check an assignment to a field. *) -let check_field_assignment tenv find_canonical_duplicate curr_pdesc node instr_ref typestate - exp_lhs exp_rhs typ loc fname annotated_field_opt typecheck_expr : unit = +let check_field_assignment ~is_strict_mode tenv find_canonical_duplicate curr_pdesc node instr_ref + typestate exp_lhs exp_rhs typ loc fname annotated_field_opt typecheck_expr : unit = let curr_pname = Procdesc.get_proc_name curr_pdesc in let curr_pattrs = Procdesc.get_attributes curr_pdesc in let t_lhs, inferred_nullability_lhs = @@ -140,12 +141,12 @@ let check_field_assignment tenv find_canonical_duplicate curr_pdesc node instr_r in let field_is_in_cleanup_context () = let AnnotatedSignature.{ret_annotation_deprecated} = - (Models.get_modelled_annotated_signature curr_pattrs).ret + (Models.get_modelled_annotated_signature tenv curr_pattrs).ret in Annotations.ia_is_cleanup ret_annotation_deprecated in let assignment_check_result = - AssignmentRule.check + AssignmentRule.check ~is_strict_mode ~lhs:(InferredNullability.get_nullability inferred_nullability_lhs) ~rhs:(InferredNullability.get_nullability inferred_nullability_rhs) in @@ -317,12 +318,13 @@ let check_constructor_initialization tenv find_canonical_duplicate curr_construc () -let check_return_not_nullable tenv find_canonical_duplicate loc curr_pname curr_pdesc - (ret_signature : AnnotatedSignature.ret_signature) ret_inferred_nullability = +let check_return_not_nullable ~is_strict_mode tenv find_canonical_duplicate loc curr_pname + curr_pdesc (ret_signature : AnnotatedSignature.ret_signature) ret_inferred_nullability = (* 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 let rhs = InferredNullability.get_nullability ret_inferred_nullability in - Result.iter_error (AssignmentRule.check ~lhs ~rhs) ~f:(fun assignment_violation -> + Result.iter_error (AssignmentRule.check ~is_strict_mode ~lhs ~rhs) + ~f:(fun assignment_violation -> let rhs_origin_descr = InferredNullability.descr_origin ret_inferred_nullability in report_error tenv find_canonical_duplicate (TypeErr.Bad_assignment @@ -366,8 +368,9 @@ let check_return_annotation tenv find_canonical_duplicate curr_pdesc ret_range | Some (_, ret_inferred_nullability) -> (* TODO(T54308240) Model ret_implicitly_nullable in AnnotatedNullability *) if not ret_implicitly_nullable then - check_return_not_nullable tenv find_canonical_duplicate loc curr_pname curr_pdesc - annotated_signature.ret ret_inferred_nullability ; + check_return_not_nullable ~is_strict_mode:annotated_signature.is_strict_mode tenv + find_canonical_duplicate loc curr_pname curr_pdesc annotated_signature.ret + ret_inferred_nullability ; if Config.eradicate_return_over_annotated then check_return_overrannotated tenv find_canonical_duplicate loc curr_pname curr_pdesc annotated_signature.ret ret_inferred_nullability @@ -376,8 +379,8 @@ let check_return_annotation tenv find_canonical_duplicate curr_pdesc ret_range (** Check the receiver of a virtual call. *) -let check_call_receiver tenv find_canonical_duplicate curr_pdesc node typestate call_params - callee_pname (instr_ref : TypeErr.InstrRef.t) loc typecheck_expr : unit = +let check_call_receiver ~is_strict_mode tenv find_canonical_duplicate curr_pdesc node typestate + call_params callee_pname (instr_ref : TypeErr.InstrRef.t) loc typecheck_expr : unit = match call_params with | ((original_this_e, this_e), typ) :: _ -> let _, this_inferred_nullability = @@ -386,8 +389,9 @@ let check_call_receiver tenv find_canonical_duplicate curr_pdesc node typestate (typ, InferredNullability.create_nonnull TypeOrigin.ONone) loc in - check_object_dereference tenv find_canonical_duplicate curr_pdesc node instr_ref - original_this_e (DereferenceRule.MethodCall callee_pname) this_inferred_nullability loc + check_object_dereference ~is_strict_mode tenv find_canonical_duplicate curr_pdesc node + instr_ref original_this_e (DereferenceRule.MethodCall callee_pname) + this_inferred_nullability loc | [] -> () @@ -399,8 +403,8 @@ type resolved_param = ; is_formal_propagates_nullable: bool } (** Check the parameters of a call. *) -let check_call_parameters tenv find_canonical_duplicate curr_pdesc node callee_attributes - resolved_params loc instr_ref : unit = +let check_call_parameters ~is_strict_mode tenv find_canonical_duplicate curr_pdesc node + callee_attributes resolved_params loc instr_ref : unit = let callee_pname = callee_attributes.ProcAttributes.proc_name in let check {num= param_position; formal; actual= orig_e2, nullability_actual} = let report assignment_violation = @@ -426,7 +430,7 @@ let check_call_parameters tenv find_canonical_duplicate curr_pdesc node callee_a to the formal param *) let lhs = AnnotatedNullability.get_nullability formal.param_annotated_type.nullability in let rhs = InferredNullability.get_nullability nullability_actual in - Result.iter_error (AssignmentRule.check ~lhs ~rhs) ~f:report + Result.iter_error (AssignmentRule.check ~is_strict_mode ~lhs ~rhs) ~f:report in let should_check_parameters = match callee_pname with @@ -537,7 +541,7 @@ let check_overridden_annotations find_canonical_duplicate tenv proc_name proc_de let check_if_base_signature_matches_current base_proc_name = match PatternMatch.lookup_attributes tenv base_proc_name with | Some base_attributes -> - let base_signature = Models.get_modelled_annotated_signature base_attributes in + let base_signature = Models.get_modelled_annotated_signature tenv base_attributes in check_inheritance_rule_for_signature find_canonical_duplicate tenv loc ~base_proc_name ~overridden_proc_name:proc_name ~overridden_proc_desc:proc_desc ~base_signature ~overridden_signature:annotated_signature diff --git a/infer/src/nullsafe/models.ml b/infer/src/nullsafe/models.ml index 856c1ed93..c7c9984d4 100644 --- a/infer/src/nullsafe/models.ml +++ b/infer/src/nullsafe/models.ml @@ -27,10 +27,33 @@ let table_has_procedure table proc_name = with Caml.Not_found -> false +(* This is used outside of nullsafe for biabduction. + If biabduction and nullsafe want to depend on common functionality, this functionality + should be refactored out in a dedicated library. + *) +let get_modelled_annotated_signature_for_biabduction proc_attributes = + let proc_name = proc_attributes.ProcAttributes.proc_name in + let annotated_signature = AnnotatedSignature.get ~is_strict_mode:false proc_attributes in + let proc_id = Typ.Procname.to_unique_id proc_name in + let lookup_models_nullable ann_sig = + try + let modelled_nullability = Hashtbl.find annotated_table_nullability proc_id in + AnnotatedSignature.set_modelled_nullability proc_name ann_sig modelled_nullability + with Caml.Not_found -> ann_sig + in + annotated_signature |> lookup_models_nullable + + (** Return the annotated signature of the procedure, taking into account models. *) -let get_modelled_annotated_signature proc_attributes = +let get_modelled_annotated_signature tenv proc_attributes = let proc_name = proc_attributes.ProcAttributes.proc_name in - let annotated_signature = AnnotatedSignature.get proc_attributes in + let is_strict_mode = + PatternMatch.get_this_type proc_attributes + |> Option.bind ~f:(fun this_class -> PatternMatch.type_get_annotation tenv this_class) + |> Option.exists ~f:(fun annotations_for_this -> + Annotations.ia_is_nullsafe_strict annotations_for_this ) + in + let annotated_signature = AnnotatedSignature.get ~is_strict_mode proc_attributes in let proc_id = Typ.Procname.to_unique_id proc_name in let lookup_models_nullable ann_sig = try diff --git a/infer/src/nullsafe/typeCheck.ml b/infer/src/nullsafe/typeCheck.ml index 14077bf7f..7827120a3 100644 --- a/infer/src/nullsafe/typeCheck.ml +++ b/infer/src/nullsafe/typeCheck.ml @@ -18,7 +18,7 @@ module ComplexExpressions = struct let procname_is_false_on_null tenv pn = match PatternMatch.lookup_attributes tenv pn with | Some proc_attributes -> - let annotated_signature = Models.get_modelled_annotated_signature proc_attributes in + let annotated_signature = Models.get_modelled_annotated_signature tenv proc_attributes in let AnnotatedSignature.{ret_annotation_deprecated} = annotated_signature.ret in Annotations.ia_is_false_on_null ret_annotation_deprecated | None -> @@ -29,7 +29,7 @@ module ComplexExpressions = struct let annotated_true_on_null () = match PatternMatch.lookup_attributes tenv pn with | Some proc_attributes -> - let annotated_signature = Models.get_modelled_annotated_signature proc_attributes in + let annotated_signature = Models.get_modelled_annotated_signature tenv proc_attributes in let AnnotatedSignature.{ret_annotation_deprecated} = annotated_signature.ret in Annotations.ia_is_true_on_null ret_annotation_deprecated | None -> @@ -109,7 +109,7 @@ type find_canonical_duplicate = Procdesc.Node.t -> Procdesc.Node.t type checks = {eradicate: bool; check_ret_type: check_return_type list} (** Typecheck an expression. *) -let rec typecheck_expr find_canonical_duplicate visited checks tenv node instr_ref +let rec typecheck_expr ~is_strict_mode find_canonical_duplicate visited checks tenv node instr_ref (curr_pdesc : Procdesc.t) typestate e tr_default loc : TypeState.range = match e with | _ when Exp.is_null_literal e -> @@ -122,16 +122,16 @@ let rec typecheck_expr find_canonical_duplicate visited checks tenv node instr_r | Exp.Var id -> Option.value (TypeState.lookup_id id typestate) ~default:tr_default | Exp.Exn e1 -> - typecheck_expr find_canonical_duplicate visited checks tenv node instr_ref curr_pdesc - typestate e1 tr_default loc + typecheck_expr ~is_strict_mode find_canonical_duplicate visited checks tenv node instr_ref + curr_pdesc typestate e1 tr_default loc | Exp.Const _ -> let typ, _ = tr_default in (typ, InferredNullability.create_nonnull (TypeOrigin.Const loc)) | Exp.Lfield (exp, field_name, typ) -> let _, _ = tr_default in let _, inferred_nullability = - typecheck_expr find_canonical_duplicate visited checks tenv node instr_ref curr_pdesc - typestate exp + typecheck_expr ~is_strict_mode find_canonical_duplicate visited checks tenv node instr_ref + curr_pdesc typestate exp (* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *) (typ, InferredNullability.create_nonnull TypeOrigin.ONone) loc @@ -147,20 +147,21 @@ let rec typecheck_expr find_canonical_duplicate visited checks tenv node instr_r tr_default in if checks.eradicate then - EradicateChecks.check_object_dereference tenv find_canonical_duplicate curr_pdesc node - instr_ref exp (DereferenceRule.AccessToField field_name) inferred_nullability loc ; + EradicateChecks.check_object_dereference ~is_strict_mode tenv find_canonical_duplicate + curr_pdesc node instr_ref exp (DereferenceRule.AccessToField field_name) + inferred_nullability loc ; tr_new | Exp.Lindex (array_exp, index_exp) -> let _, inferred_nullability = - typecheck_expr find_canonical_duplicate visited checks tenv node instr_ref curr_pdesc - typestate array_exp tr_default loc + typecheck_expr ~is_strict_mode find_canonical_duplicate visited checks tenv node instr_ref + curr_pdesc typestate array_exp tr_default loc in let index_desc = match EradicateChecks.explain_expr tenv node index_exp with Some s -> s | None -> "?" in if checks.eradicate then - EradicateChecks.check_object_dereference tenv find_canonical_duplicate curr_pdesc node - instr_ref array_exp + EradicateChecks.check_object_dereference ~is_strict_mode tenv find_canonical_duplicate + curr_pdesc node instr_ref array_exp (DereferenceRule.AccessByIndex {index_desc}) inferred_nullability loc ; tr_default @@ -170,7 +171,8 @@ let rec typecheck_expr find_canonical_duplicate visited checks tenv node instr_r (** Typecheck an instruction. *) let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_pname curr_pdesc - find_canonical_duplicate curr_annotated_signature instr_ref linereader typestate instr = + find_canonical_duplicate (curr_annotated_signature : AnnotatedSignature.t) instr_ref linereader + typestate instr = (* Handle the case where a field access X.f happens via a temporary variable $Txxx. This has been observed in assignments this.f = exp when exp contains an ifthenelse. Reconstuct the original expression knowing: the origin of $Txxx is 'this'. *) @@ -284,7 +286,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p (* parameter.field *) let name = Pvar.get_name pvar in let filter AnnotatedSignature.{mangled} = Mangled.equal mangled name in - List.exists ~f:filter curr_annotated_signature.AnnotatedSignature.params + List.exists ~f:filter curr_annotated_signature.params in let is_static_field pvar = (* static field *) @@ -397,16 +399,18 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p typestate' ) in (* typecheck_expr with fewer parameters, using a common template for typestate range *) - let typecheck_expr_simple typestate1 exp1 typ1 origin1 loc1 = - typecheck_expr find_canonical_duplicate calls_this checks tenv node instr_ref curr_pdesc - typestate1 exp1 + let typecheck_expr_simple ~is_strict_mode typestate1 exp1 typ1 origin1 loc1 = + typecheck_expr ~is_strict_mode find_canonical_duplicate calls_this checks tenv node instr_ref + curr_pdesc typestate1 exp1 (typ1, InferredNullability.create_nonnull origin1) loc1 in (* check if there are errors in exp1 *) - let typecheck_expr_for_errors typestate1 exp1 loc1 : unit = - ignore (typecheck_expr_simple typestate1 exp1 (Typ.mk Tvoid) TypeOrigin.Undef loc1) + let typecheck_expr_for_errors ~is_strict_mode typestate1 exp1 loc1 : unit = + ignore + (typecheck_expr_simple ~is_strict_mode typestate1 exp1 (Typ.mk Tvoid) TypeOrigin.Undef loc1) in + let is_strict_mode = curr_annotated_signature.is_strict_mode in match instr with | Sil.Metadata (ExitScope (vars, _)) -> List.fold_right vars ~init:typestate ~f:(fun var astate -> @@ -418,23 +422,25 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p | Sil.Metadata (Abstract _ | Nullify _ | Skip | VariableLifetimeBegins _) -> typestate | Sil.Load {id; e; typ; loc} -> - typecheck_expr_for_errors typestate e loc ; + typecheck_expr_for_errors ~is_strict_mode typestate e loc ; let e', typestate' = convert_complex_exp_to_pvar node false e typestate loc in - TypeState.add_id id (typecheck_expr_simple typestate' e' typ TypeOrigin.Undef loc) typestate' + TypeState.add_id id + (typecheck_expr_simple ~is_strict_mode typestate' e' typ TypeOrigin.Undef loc) + typestate' | Sil.Store {e1= Exp.Lvar pvar; e2= Exp.Exn _} when is_return pvar -> (* skip assignment to return variable where it is an artifact of a throw instruction *) typestate | Sil.Store {e1; typ; e2; loc} -> - typecheck_expr_for_errors typestate e1 loc ; + typecheck_expr_for_errors ~is_strict_mode typestate e1 loc ; let e1', typestate1 = convert_complex_exp_to_pvar node true e1 typestate loc in let check_field_assign () = match e1 with | Exp.Lfield (_, fn, f_typ) -> let field_type_opt = AnnotatedField.get tenv fn f_typ in if checks.eradicate then - EradicateChecks.check_field_assignment tenv find_canonical_duplicate curr_pdesc node - instr_ref typestate1 e1' e2 typ loc fn field_type_opt - (typecheck_expr find_canonical_duplicate calls_this checks tenv) + EradicateChecks.check_field_assignment ~is_strict_mode tenv find_canonical_duplicate + curr_pdesc node instr_ref typestate1 e1' e2 typ loc fn field_type_opt + (typecheck_expr ~is_strict_mode find_canonical_duplicate calls_this checks tenv) | _ -> () in @@ -442,7 +448,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p match e1' with | Exp.Lvar pvar -> TypeState.add pvar - (typecheck_expr_simple typestate1 e2 typ TypeOrigin.Undef loc) + (typecheck_expr_simple ~is_strict_mode typestate1 e2 typ TypeOrigin.Undef loc) typestate1 | Exp.Lfield _ -> typestate1 @@ -457,22 +463,24 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p (* new never returns null *) | Sil.Call ((id, _), Exp.Const (Const.Cfun pn), (e, typ) :: _, loc, _) when Typ.Procname.equal pn BuiltinDecl.__cast -> - typecheck_expr_for_errors typestate e loc ; + typecheck_expr_for_errors ~is_strict_mode typestate e loc ; let e', typestate' = convert_complex_exp_to_pvar node false e typestate loc in (* cast copies the type of the first argument *) - TypeState.add_id id (typecheck_expr_simple typestate' e' typ TypeOrigin.ONone loc) typestate' + TypeState.add_id id + (typecheck_expr_simple ~is_strict_mode typestate' e' typ TypeOrigin.ONone loc) + typestate' | Sil.Call ((id, _), Exp.Const (Const.Cfun pn), [(array_exp, t)], loc, _) when Typ.Procname.equal pn BuiltinDecl.__get_array_length -> let _, ta = - typecheck_expr find_canonical_duplicate calls_this checks tenv node instr_ref curr_pdesc - typestate array_exp + typecheck_expr ~is_strict_mode find_canonical_duplicate calls_this checks tenv node + instr_ref curr_pdesc typestate array_exp (* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *) (t, InferredNullability.create_nonnull TypeOrigin.ONone) loc in if checks.eradicate then - EradicateChecks.check_object_dereference tenv find_canonical_duplicate curr_pdesc node - instr_ref array_exp DereferenceRule.ArrayLengthAccess ta loc ; + EradicateChecks.check_object_dereference ~is_strict_mode tenv find_canonical_duplicate + curr_pdesc node instr_ref array_exp DereferenceRule.ArrayLengthAccess ta loc ; TypeState.add_id id (Typ.mk (Tint Typ.IInt), InferredNullability.create_nonnull TypeOrigin.New) typestate @@ -511,13 +519,15 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p let etl = drop_unchecked_params calls_this callee_attributes etl_ in let call_params, typestate1 = let handle_et (e1, t1) (etl1, typestate1) = - typecheck_expr_for_errors typestate e1 loc ; + typecheck_expr_for_errors ~is_strict_mode typestate e1 loc ; let e2, typestate2 = convert_complex_exp_to_pvar node false e1 typestate1 loc in (((e1, e2), t1) :: etl1, typestate2) in List.fold_right ~f:handle_et etl ~init:([], typestate) in - let callee_annotated_signature = Models.get_modelled_annotated_signature callee_attributes in + let callee_annotated_signature = + Models.get_modelled_annotated_signature tenv callee_attributes + in let signature_params = drop_unchecked_signature_params callee_attributes callee_annotated_signature in @@ -669,7 +679,8 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p | Some map_get_str -> let pvar_map_get = Pvar.mk (Mangled.from_string map_get_str) curr_pname in TypeState.add pvar_map_get - (typecheck_expr_simple typestate' exp_value typ_value TypeOrigin.Undef loc) + (typecheck_expr_simple ~is_strict_mode typestate' exp_value typ_value + TypeOrigin.Undef loc) typestate' | None -> typestate' ) @@ -680,8 +691,8 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p let resolve_param i (formal_param, actual_param) = let (orig_e2, e2), t2 = actual_param in let _, inferred_nullability_actual = - typecheck_expr find_canonical_duplicate calls_this checks tenv node instr_ref - curr_pdesc typestate e2 + typecheck_expr ~is_strict_mode find_canonical_duplicate calls_this checks tenv node + instr_ref curr_pdesc typestate e2 (* TODO(T54687014) optimistic default might be an unsoundness issue - investigate *) (t2, InferredNullability.create_nonnull TypeOrigin.ONone) loc @@ -764,12 +775,12 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p let typestate_after_call = if not is_anonymous_inner_class_constructor then ( if cflags.CallFlags.cf_virtual && checks.eradicate then - EradicateChecks.check_call_receiver tenv find_canonical_duplicate curr_pdesc node - typestate1 call_params callee_pname instr_ref loc - (typecheck_expr find_canonical_duplicate calls_this checks) ; + EradicateChecks.check_call_receiver ~is_strict_mode tenv find_canonical_duplicate + curr_pdesc node typestate1 call_params callee_pname instr_ref loc + (typecheck_expr ~is_strict_mode find_canonical_duplicate calls_this checks) ; if checks.eradicate then - EradicateChecks.check_call_parameters tenv find_canonical_duplicate curr_pdesc node - callee_attributes resolved_params loc instr_ref ; + EradicateChecks.check_call_parameters ~is_strict_mode tenv find_canonical_duplicate + curr_pdesc node callee_attributes resolved_params loc instr_ref ; if Models.is_check_not_null callee_pname then match Models.get_check_not_null_parameter callee_pname with | Some index -> @@ -845,7 +856,8 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p let pvar = Pvar.mk (Mangled.from_string e_str) curr_pname in let e1 = Exp.Lvar pvar in let typ, ta = - typecheck_expr_simple typestate e1 (Typ.mk Tvoid) TypeOrigin.ONone loc + typecheck_expr_simple ~is_strict_mode typestate e1 (Typ.mk Tvoid) TypeOrigin.ONone + loc in let range = (typ, ta) in let typestate1 = TypeState.add pvar range typestate in @@ -874,7 +886,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p | Exp.BinOp (Binop.Eq, Exp.Const (Const.Cint i), e) | Exp.BinOp (Binop.Eq, e, Exp.Const (Const.Cint i)) when IntLit.iszero i -> ( - typecheck_expr_for_errors typestate e loc ; + typecheck_expr_for_errors ~is_strict_mode typestate e loc ; let typestate1, e1, from_call = match from_is_true_on_null e with | Some e1 -> @@ -884,7 +896,8 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p in let e', typestate2 = convert_complex_exp_to_pvar node' false e1 typestate1 loc in let typ, inferred_nullability = - typecheck_expr_simple typestate2 e' (Typ.mk Tvoid) TypeOrigin.ONone loc + typecheck_expr_simple ~is_strict_mode typestate2 e' (Typ.mk Tvoid) TypeOrigin.ONone + loc in if checks.eradicate then EradicateChecks.check_zero tenv find_canonical_duplicate curr_pdesc node' e' typ @@ -901,7 +914,7 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p | Exp.BinOp (Binop.Ne, Exp.Const (Const.Cint i), e) | Exp.BinOp (Binop.Ne, e, Exp.Const (Const.Cint i)) when IntLit.iszero i -> ( - typecheck_expr_for_errors typestate e loc ; + typecheck_expr_for_errors ~is_strict_mode typestate e loc ; let typestate1, e1, from_call = match from_instanceof e with | Some e1 -> @@ -917,7 +930,8 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p in let e', typestate2 = convert_complex_exp_to_pvar node' false e1 typestate1 loc in let typ, inferred_nullability = - typecheck_expr_simple typestate2 e' (Typ.mk Tvoid) TypeOrigin.ONone loc + typecheck_expr_simple ~is_strict_mode typestate2 e' (Typ.mk Tvoid) TypeOrigin.ONone + loc in if checks.eradicate then EradicateChecks.check_nonzero tenv find_canonical_duplicate curr_pdesc node e' typ diff --git a/infer/tests/codetoanalyze/java/nullsafe-default/StrictMode.java b/infer/tests/codetoanalyze/java/nullsafe-default/StrictMode.java new file mode 100644 index 000000000..498178050 --- /dev/null +++ b/infer/tests/codetoanalyze/java/nullsafe-default/StrictMode.java @@ -0,0 +1,189 @@ +/* + * 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. + */ + +package codetoanalyze.java.nullsafe_default; + +import com.facebook.infer.annotation.NullsafeStrict; +import javax.annotation.Nonnull; +import javax.annotation.Nullable; + +@NullsafeStrict +class Strict { + + public @Nullable String nullable; + public @Nonnull String nonnull = ""; + + public @Nullable String getNullable() { + return nullable; + } + + public String getNonnull() { + return nonnull; + } + + // 1. Inside the same class, we trust annotations. + + private void sameClass_dereferenceNullableMethodIsBad() { + getNullable().toString(); + } + + private void sameClass_dereferenceNonnullMethodIsOK() { + getNonnull().toString(); + } + + private void sameClass_dereferenceNullableFieldIsBad() { + nullable.toString(); + } + + private void sameClass_dereferenceNonnullFieldIsOK() { + nonnull.toString(); + } + + private String sameClass_convertingNullableToNonnullIsBad() { + return getNullable(); + } + + private String sameClass_convertingNonnullToNonnullIsOK() { + return getNonnull(); + } + + // 2. We trust annotations that came from other classes annotated as strict + + private void strictClass_dereferenceNullableMethodIsBad() { + (new OtherStrict()).getNullable().toString(); + } + + private void strictClass_dereferenceNonnullMethodIsOK() { + (new OtherStrict()).getNonnull().toString(); + } + + private void strictClass_dereferenceNullableFieldIsBad() { + (new OtherStrict()).nullable.toString(); + } + + private void strictClass_dereferenceNonnullFieldIsOK() { + (new OtherStrict()).nonnull.toString(); + } + + private String strictClass_convertingNullableToNonnullIsBad() { + return (new OtherStrict()).getNullable(); + } + + private String strictClass_convertingNonnullToNonnullIsOK() { + return (new OtherStrict()).getNonnull(); + } + + // 3. We DON'T trust annotations that came from other classes NOT annotated as strict + // when it comes to dereferencing or converting them to nullable. + + private void nonStrictClass_dereferenceNullableMethodIsBad() { + (new NonStrict()).getNullable().toString(); + } + + private void nonStrictClass_dereferenceNonnullMethodIsBad() { + // even that it is declared as nonnull, can not dereference it without checking before + (new NonStrict()).getNonnull().toString(); + } + + private void nonStrictClass_dereferenceNullableFieldIsBad() { + (new NonStrict()).nullable.toString(); + } + + private void nonStrictClass_dereferenceNonnullFieldIsBad() { + // even that it is declared as nonnull, can not dereference it without checking before + (new NonStrict()).nonnull.toString(); + } + + private String nonStrictClass_convertingNullableToNonnullIsBad() { + return (new NonStrict()).getNullable(); + } + + private String nonStrictClass_convertingNonnullToNonnullIsBad() { + // even that it is declared as nonnull, can not convert it to nonnull it without checking before + return (new NonStrict()).getNonnull(); + } + + // 4. We don't completely prohibit using non-strict from strict, but we do require extra checks + // or adding defensive annotations. + + private void nonStrictClass_dereferenceNonnullFieldAfterCheckIsOK() { + NonStrict o = new NonStrict(); + if (o.nonnull != null) { + // This works because Nullsafe assumes that the field won't be modified between the calls + // (e.g. in multithreading context) + o.nonnull.toString(); + } + } + + private void nonStrictClass_dereferenceNonnullMethodAfterCheckIsOK() { + NonStrict o = new NonStrict(); + if (o.getNonnull() != null) { + // This works because Nullsafe assumes that all methods are determenistic and side-effect + // free, so the second call won't return null. + o.getNonnull().toString(); + } + } + + private @Nullable String nonStrictClass_convertingNonnullToNullableIsOK() { + return (new NonStrict()).getNonnull(); + } + + // 5. Main promise of strict mode: if the function is not annotated as nullable, + // it won't return null. + // So, if a function is annotated as strict, no extra check on caller's side is required. + // But strict mode DOES NOT guarantee there will be absolutely no NPE in callees: + // a) Even if strict mode calls only strict mode, there can be assertions that will throw NPE. + // b) We allow calling non-strict functions, and they internally can be inconsistent and throw + // NPE. + // c) We even allow passing values obtained from non-strict code, to other parts of non-strict + // code (e.g. we allow glueing 2 non-strict classes together inside a strict class, which might + // potentially lead to NPE if one of annotations is untrusted). + + private void propagatingNonnullFromNonStrictToStrictIsBad() { + NonStrict nonStrict = new NonStrict(); + OtherStrict strict = new OtherStrict(); + nonStrict.nonnull = strict.getNonnull(); + } + + private void propagatingNonnullBetweenTwoNonStrictObjectsIsOK() { + NonStrict nonStrict1 = new NonStrict(); + NonStrict nonStrict2 = new NonStrict(); + // Though getNonnull() is declared as non-nullable, is not strictly checked + // so there is a possibility that it can return null, e.g. if it calls to a third-party + // libraries. this null can leak to `nonnull` field, which might be a bad thing and lead to + // issues. + // This is OK for strict mode. + nonStrict1.nonnull = nonStrict2.getNonnull(); + } +} + +@NullsafeStrict +class OtherStrict { + public @Nullable String nullable; + public String nonnull = ""; + + public @Nullable String getNullable() { + return nullable; + } + + public String getNonnull() { + return nonnull; + } +} + +class NonStrict { + public @Nullable String nullable; + public String nonnull = ""; + + public @Nullable String getNullable() { + return nullable; + } + + public String getNonnull() { + return nonnull; + } +} diff --git a/infer/tests/codetoanalyze/java/nullsafe-default/issues.exp b/infer/tests/codetoanalyze/java/nullsafe-default/issues.exp index e12329132..b8fdbeec7 100644 --- a/infer/tests/codetoanalyze/java/nullsafe-default/issues.exp +++ b/infer/tests/codetoanalyze/java/nullsafe-default/issues.exp @@ -216,3 +216,18 @@ codetoanalyze/java/nullsafe-default/ReturnNotNullable.java, codetoanalyze.java.n codetoanalyze/java/nullsafe-default/ReturnNotNullable.java, codetoanalyze.java.nullsafe_default.ReturnNotNullable.return_null_in_catch():java.lang.String, 0, ERADICATE_RETURN_NOT_NULLABLE, no_bucket, WARNING, [Method `return_null_in_catch()` may return null but it is not annotated with `@Nullable`. (Origin: null constant at line 160)] codetoanalyze/java/nullsafe-default/ReturnNotNullable.java, codetoanalyze.java.nullsafe_default.ReturnNotNullable.return_null_in_catch_after_throw():java.lang.String, 0, ERADICATE_RETURN_NOT_NULLABLE, no_bucket, WARNING, [Method `return_null_in_catch_after_throw()` may return null but it is not annotated with `@Nullable`. (Origin: null constant at line 172)] codetoanalyze/java/nullsafe-default/ReturnNotNullable.java, codetoanalyze.java.nullsafe_default.ReturnNotNullable.tryWithResourcesReturnNullable(java.lang.String):java.lang.Object, 0, ERADICATE_RETURN_NOT_NULLABLE, no_bucket, WARNING, [Method `tryWithResourcesReturnNullable(...)` may return null but it is not annotated with `@Nullable`. (Origin: call to nullToNullableIsOK() at line 142)] +codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_convertingNonnullToNonnullIsBad():java.lang.String, 0, ERADICATE_RETURN_NOT_NULLABLE, no_bucket, WARNING, [Method `nonStrictClass_convertingNonnullToNonnullIsBad()` may return null but it is not annotated with `@Nullable`. (Origin: call to getNonnull() at line 107)] +codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_convertingNonnullToNullableIsOK():java.lang.String, 0, ERADICATE_RETURN_OVER_ANNOTATED, no_bucket, WARNING, [Method `nonStrictClass_convertingNonnullToNullableIsOK()` is annotated with `@Nullable` but never returns null.] +codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_convertingNullableToNonnullIsBad():java.lang.String, 0, ERADICATE_RETURN_NOT_NULLABLE, no_bucket, WARNING, [Method `nonStrictClass_convertingNullableToNonnullIsBad()` may return null but it is not annotated with `@Nullable`. (Origin: call to getNullable() at line 102)] +codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_dereferenceNonnullFieldAfterCheckIsOK():void, 2, ERADICATE_CONDITION_REDUNDANT, no_bucket, WARNING, [The condition NonStrict.nonnull is always true according to the existing annotations.] +codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_dereferenceNonnullFieldIsBad():void, 2, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, WARNING, [`__new(...).nonnull` is nullable and is not locally checked for null when calling `toString()`. (Origin: field NonStrict.nonnull at line 98)] +codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_dereferenceNonnullMethodAfterCheckIsOK():void, 2, ERADICATE_CONDITION_REDUNDANT, no_bucket, WARNING, [The condition lang.String(o)V is always true according to the existing annotations.] +codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_dereferenceNonnullMethodIsBad():void, 2, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, WARNING, [`__new(...).getNonnull()` is nullable and is not locally checked for null when calling `toString()`. (Origin: call to getNonnull() at line 89)] +codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_dereferenceNullableFieldIsBad():void, 1, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, WARNING, [`__new(...).nullable` is nullable and is not locally checked for null when calling `toString()`. (Origin: field NonStrict.nullable at line 93)] +codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_dereferenceNullableMethodIsBad():void, 1, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, WARNING, [`__new(...).getNullable()` is nullable and is not locally checked for null when calling `toString()`. (Origin: call to getNullable() at line 84)] +codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.sameClass_convertingNullableToNonnullIsBad():java.lang.String, 0, ERADICATE_RETURN_NOT_NULLABLE, no_bucket, WARNING, [Method `sameClass_convertingNullableToNonnullIsBad()` may return null but it is not annotated with `@Nullable`. (Origin: call to getNullable() at line 47)] +codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.sameClass_dereferenceNullableFieldIsBad():void, 1, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, WARNING, [`Strict.nullable` is nullable and is not locally checked for null when calling `toString()`. (Origin: field Strict.nullable at line 39)] +codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.sameClass_dereferenceNullableMethodIsBad():void, 1, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, WARNING, [`getNullable()` is nullable and is not locally checked for null when calling `toString()`. (Origin: call to getNullable() at line 31)] +codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.strictClass_convertingNullableToNonnullIsBad():java.lang.String, 0, ERADICATE_RETURN_NOT_NULLABLE, no_bucket, WARNING, [Method `strictClass_convertingNullableToNonnullIsBad()` may return null but it is not annotated with `@Nullable`. (Origin: call to getNullable() at line 73)] +codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.strictClass_dereferenceNullableFieldIsBad():void, 1, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, WARNING, [`__new(...).nullable` is nullable and is not locally checked for null when calling `toString()`. (Origin: field OtherStrict.nullable at line 65)] +codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.strictClass_dereferenceNullableMethodIsBad():void, 1, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, WARNING, [`__new(...).getNullable()` is nullable and is not locally checked for null when calling `toString()`. (Origin: call to getNullable() at line 57)]