From 6511b2052aedf51d609f35ca8ee4543d422d1279 Mon Sep 17 00:00:00 2001 From: Mitya Lyubarskiy Date: Mon, 21 Oct 2019 04:40:35 -0700 Subject: [PATCH] [nullsafe] Introduce Strict mode Summary: This is the first take on strict mode semantics. 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). This invariant helps the caller in two ways: 1. Dangerous usages of non strict functions are visible, so the caller is enforced to check them (via assertions or conditions), or strictify them. 2. When the function is strict, the caller does not need to worry about being defensive. Biggest known issues so far: 1. Condition redundant and over-annotated warnings don't fully respect strict mode, and this leads to stupid false positives. (There is so much more stupid false positives in condition redundant anyway, so not particularly a big deal for now). 2. Error reporting is not specific to mode. (E.g. we don't distinct real nullables and non-trusted non-nulls, which can be misleading). To be improved as a follow up. Reviewed By: artempyanykh Differential Revision: D17978166 fbshipit-source-id: d6146ad71 --- .../infer/annotation/NullsafeStrict.java | 24 +++ infer/src/biabduction/Rearrange.ml | 4 +- infer/src/checkers/annotations.ml | 10 +- infer/src/checkers/annotations.mli | 2 + infer/src/nullsafe/AnnotatedField.ml | 13 +- infer/src/nullsafe/AnnotatedNullability.ml | 6 +- infer/src/nullsafe/AnnotatedNullability.mli | 3 +- infer/src/nullsafe/AnnotatedSignature.ml | 29 ++- infer/src/nullsafe/AnnotatedSignature.mli | 5 +- infer/src/nullsafe/AssignmentRule.ml | 22 +- infer/src/nullsafe/AssignmentRule.mli | 3 +- infer/src/nullsafe/DereferenceRule.ml | 9 +- infer/src/nullsafe/DereferenceRule.mli | 2 +- infer/src/nullsafe/Initializers.ml | 2 +- infer/src/nullsafe/eradicate.ml | 13 +- infer/src/nullsafe/eradicateChecks.ml | 44 ++-- infer/src/nullsafe/models.ml | 27 ++- infer/src/nullsafe/typeCheck.ml | 110 +++++----- .../java/nullsafe-default/StrictMode.java | 189 ++++++++++++++++++ .../java/nullsafe-default/issues.exp | 15 ++ 20 files changed, 423 insertions(+), 109 deletions(-) create mode 100644 infer/annotations/src/main/java/com/facebook/infer/annotation/NullsafeStrict.java create mode 100644 infer/tests/codetoanalyze/java/nullsafe-default/StrictMode.java 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)]