diff --git a/infer/src/nullsafe/DereferenceRule.ml b/infer/src/nullsafe/DereferenceRule.ml index 321475637..b10b0082b 100644 --- a/infer/src/nullsafe/DereferenceRule.ml +++ b/infer/src/nullsafe/DereferenceRule.ml @@ -6,109 +6,118 @@ *) open! IStd -type violation = {nullsafe_mode: NullsafeMode.t; nullability: Nullability.t} [@@deriving compare] +type violation = {nullability: Nullability.t} [@@deriving compare] -type dereference_type = - | MethodCall of Procname.t - | AccessToField of Fieldname.t - | AccessByIndex of {index_desc: string} - | ArrayLengthAccess -[@@deriving compare] +module ReportableViolation = struct + type t = {nullsafe_mode: NullsafeMode.t; violation: violation} -let check ~nullsafe_mode nullability = - match nullability with - | Nullability.Nullable | Nullability.Null -> - Error {nullsafe_mode; nullability} - | other when not (Nullability.is_considered_nonnull ~nullsafe_mode other) -> - Error {nullsafe_mode; nullability} - | _ -> - Ok () + type dereference_type = + | MethodCall of Procname.t + | AccessToField of Fieldname.t + | AccessByIndex of {index_desc: string} + | ArrayLengthAccess + [@@deriving compare] + + let get_origin_opt ~nullable_object_descr origin = + let should_show_origin = + match nullable_object_descr with + | Some object_expression -> + not (ErrorRenderingUtils.is_object_nullability_self_explanatory ~object_expression origin) + | None -> + true + in + if should_show_origin then Some origin else None -let get_origin_opt ~nullable_object_descr origin = - let should_show_origin = - match nullable_object_descr with - | Some object_expression -> - not (ErrorRenderingUtils.is_object_nullability_self_explanatory ~object_expression origin) - | None -> - true - in - if should_show_origin then Some origin else None + let get_description {nullsafe_mode; violation= {nullability}} ~dereference_location + dereference_type ~nullable_object_descr ~nullable_object_origin = + let module MF = MarkupFormatter in + let special_message = + if not (NullsafeMode.equal NullsafeMode.Default nullsafe_mode) then + ErrorRenderingUtils.mk_special_nullsafe_issue ~nullsafe_mode ~bad_nullability:nullability + ~bad_usage_location:dereference_location nullable_object_origin + else None + in + match special_message with + | Some desc -> + desc + | _ -> + let what_is_dereferred_str = + match dereference_type with + | MethodCall _ | AccessToField _ -> ( + match nullable_object_descr with + | None -> + "Object" + (* Just describe an object itself *) + | Some descr -> + MF.monospaced_to_string descr ) + | ArrayLengthAccess | AccessByIndex _ -> ( + (* In Java, those operations can be applied only to arrays *) + match nullable_object_descr with + | None -> + "Array" + | Some descr -> + Format.sprintf "Array %s" (MF.monospaced_to_string descr) ) + in + let action_descr = + match dereference_type with + | MethodCall method_name -> + Format.sprintf "calling %s" + (MF.monospaced_to_string (Procname.to_simplified_string method_name)) + | AccessToField field_name -> + Format.sprintf "accessing field %s" + (MF.monospaced_to_string (Fieldname.to_simplified_string field_name)) + | AccessByIndex {index_desc} -> + Format.sprintf "accessing at index %s" (MF.monospaced_to_string index_desc) + | ArrayLengthAccess -> + "accessing its length" + in + let origin_descr = + get_origin_opt ~nullable_object_descr nullable_object_origin + |> Option.bind ~f:(fun origin -> TypeOrigin.get_description origin) + |> Option.value_map ~f:(fun origin -> ": " ^ origin) ~default:"" + in + let alternative_method_description = + ErrorRenderingUtils.find_alternative_nonnull_method_description nullable_object_origin + in + let alternative_recommendation = + Option.value_map alternative_method_description + ~f:(fun descr -> + Format.asprintf " If this is intentional, use %a instead." MF.pp_monospaced descr ) + ~default:"" + in + let description = + match nullability with + | Nullability.Null -> + Format.sprintf + "NullPointerException will be thrown at this line! %s is `null` and is \ + dereferenced via %s%s." + what_is_dereferred_str action_descr origin_descr + | Nullability.Nullable -> + Format.sprintf "%s is nullable and is not locally checked for null when %s%s.%s" + what_is_dereferred_str action_descr origin_descr alternative_recommendation + | other -> + Logging.die InternalError + "violation_description:: invariant violation: unexpected nullability %a" + Nullability.pp other + in + (description, IssueType.eradicate_nullable_dereference, dereference_location) -let violation_description {nullsafe_mode; nullability} ~dereference_location dereference_type - ~nullable_object_descr ~nullable_object_origin = - let module MF = MarkupFormatter in - let special_message = - if not (NullsafeMode.equal NullsafeMode.Default nullsafe_mode) then - ErrorRenderingUtils.mk_special_nullsafe_issue ~nullsafe_mode ~bad_nullability:nullability - ~bad_usage_location:dereference_location nullable_object_origin - else None - in - match special_message with - | Some desc -> - desc + let get_severity {nullsafe_mode} = NullsafeMode.severity nullsafe_mode +end + +let check nullability = + match nullability with + (* StrictNonnull is the only "real" value that is not null according to type system rules. + Other values can not be fully trusted. + *) + | Nullability.StrictNonnull -> + Ok () | _ -> - let what_is_dereferred_str = - match dereference_type with - | MethodCall _ | AccessToField _ -> ( - match nullable_object_descr with - | None -> - "Object" - (* Just describe an object itself *) - | Some descr -> - MF.monospaced_to_string descr ) - | ArrayLengthAccess | AccessByIndex _ -> ( - (* In Java, those operations can be applied only to arrays *) - match nullable_object_descr with - | None -> - "Array" - | Some descr -> - Format.sprintf "Array %s" (MF.monospaced_to_string descr) ) - in - let action_descr = - match dereference_type with - | MethodCall method_name -> - Format.sprintf "calling %s" - (MF.monospaced_to_string (Procname.to_simplified_string method_name)) - | AccessToField field_name -> - Format.sprintf "accessing field %s" - (MF.monospaced_to_string (Fieldname.to_simplified_string field_name)) - | AccessByIndex {index_desc} -> - Format.sprintf "accessing at index %s" (MF.monospaced_to_string index_desc) - | ArrayLengthAccess -> - "accessing its length" - in - let origin_descr = - get_origin_opt ~nullable_object_descr nullable_object_origin - |> Option.bind ~f:(fun origin -> TypeOrigin.get_description origin) - |> Option.value_map ~f:(fun origin -> ": " ^ origin) ~default:"" - in - let alternative_method_description = - ErrorRenderingUtils.find_alternative_nonnull_method_description nullable_object_origin - in - let alternative_recommendation = - Option.value_map alternative_method_description - ~f:(fun descr -> - Format.asprintf " If this is intentional, use %a instead." MF.pp_monospaced descr ) - ~default:"" - in - let description = - match nullability with - | Nullability.Null -> - Format.sprintf - "NullPointerException will be thrown at this line! %s is `null` and is dereferenced \ - via %s%s." - what_is_dereferred_str action_descr origin_descr - | Nullability.Nullable -> - Format.sprintf "%s is nullable and is not locally checked for null when %s%s.%s" - what_is_dereferred_str action_descr origin_descr alternative_recommendation - | other -> - Logging.die InternalError - "violation_description:: invariant violation: unexpected nullability %a" - Nullability.pp other - in - (description, IssueType.eradicate_nullable_dereference, dereference_location) + Error {nullability} -let violation_severity {nullsafe_mode} = NullsafeMode.severity nullsafe_mode +let to_reportable_violation nullsafe_mode ({nullability} as violation) = + if Nullability.is_considered_nonnull ~nullsafe_mode nullability then None + else Some ReportableViolation.{nullsafe_mode; violation} diff --git a/infer/src/nullsafe/DereferenceRule.mli b/infer/src/nullsafe/DereferenceRule.mli index af3f709e5..4619487cc 100644 --- a/infer/src/nullsafe/DereferenceRule.mli +++ b/infer/src/nullsafe/DereferenceRule.mli @@ -11,23 +11,36 @@ open! IStd type violation [@@deriving compare] -val check : nullsafe_mode:NullsafeMode.t -> Nullability.t -> (unit, violation) result - -type dereference_type = - | MethodCall of Procname.t - | AccessToField of Fieldname.t - | AccessByIndex of {index_desc: string} - | ArrayLengthAccess -[@@deriving compare] - -val violation_description : - violation - -> dereference_location:Location.t - -> dereference_type - -> nullable_object_descr:string option - -> nullable_object_origin:TypeOrigin.t - -> string * IssueType.t * Location.t -(** Given context around violation, return error message together with the info where to put this - message *) - -val violation_severity : violation -> Exceptions.severity +val check : Nullability.t -> (unit, violation) result +(** violation of Dereference rule reflects possibility of dereferencing of `null`. Note that this + might or might not be severe enough to be reported to the user, depending on the mode + agreements. *) + +(** Violation that needs to be reported to the user. *) +module ReportableViolation : sig + type t + + type dereference_type = + | MethodCall of Procname.t + | AccessToField of Fieldname.t + | AccessByIndex of {index_desc: string} + | ArrayLengthAccess + [@@deriving compare] + + val get_severity : t -> Exceptions.severity + (** Severity of the violation to be reported *) + + val get_description : + t + -> dereference_location:Location.t + -> dereference_type + -> nullable_object_descr:string option + -> nullable_object_origin:TypeOrigin.t + -> string * IssueType.t * Location.t + (** Given context around violation, return error message together with the info where to put this + message *) +end + +val to_reportable_violation : NullsafeMode.t -> violation -> ReportableViolation.t option +(** Depending on the mode, violation might or might not be important enough to be reported to the + user. If it should NOT be reported for that mode, this function will return None. *) diff --git a/infer/src/nullsafe/eradicateChecks.ml b/infer/src/nullsafe/eradicateChecks.ml index c75820b29..866857a7a 100644 --- a/infer/src/nullsafe/eradicateChecks.ml +++ b/infer/src/nullsafe/eradicateChecks.ml @@ -31,8 +31,7 @@ let is_virtual = function let check_object_dereference ~nullsafe_mode tenv find_canonical_duplicate curr_pname node instr_ref object_exp dereference_type inferred_nullability loc = Result.iter_error - (DereferenceRule.check ~nullsafe_mode - (InferredNullability.get_nullability inferred_nullability)) + (DereferenceRule.check (InferredNullability.get_nullability inferred_nullability)) ~f:(fun dereference_violation -> let nullable_object_origin = InferredNullability.get_origin inferred_nullability in let nullable_object_descr = explain_expr tenv node object_exp in @@ -407,7 +406,7 @@ let check_call_receiver ~nullsafe_mode tenv find_canonical_duplicate curr_pdesc loc in check_object_dereference ~nullsafe_mode tenv find_canonical_duplicate curr_pdesc node - instr_ref original_this_e (DereferenceRule.MethodCall callee_pname) + instr_ref original_this_e (DereferenceRule.ReportableViolation.MethodCall callee_pname) this_inferred_nullability loc | [] -> () diff --git a/infer/src/nullsafe/typeCheck.ml b/infer/src/nullsafe/typeCheck.ml index 176a160a4..b9c9d8ec5 100644 --- a/infer/src/nullsafe/typeCheck.ml +++ b/infer/src/nullsafe/typeCheck.ml @@ -165,8 +165,9 @@ let rec typecheck_expr ~nullsafe_mode find_canonical_duplicate visited checks te in if checks.eradicate then EradicateChecks.check_object_dereference ~nullsafe_mode tenv find_canonical_duplicate - curr_pdesc node instr_ref exp (DereferenceRule.AccessToField field_name) - inferred_nullability loc ; + curr_pdesc node instr_ref exp + (DereferenceRule.ReportableViolation.AccessToField field_name) inferred_nullability + loc ; tr_new | Exp.Lindex (array_exp, index_exp) -> let _, inferred_nullability = @@ -179,7 +180,7 @@ let rec typecheck_expr ~nullsafe_mode find_canonical_duplicate visited checks te if checks.eradicate then EradicateChecks.check_object_dereference ~nullsafe_mode tenv find_canonical_duplicate curr_pdesc node instr_ref array_exp - (DereferenceRule.AccessByIndex {index_desc}) + (DereferenceRule.ReportableViolation.AccessByIndex {index_desc}) inferred_nullability loc ; let typ, _ = tr_default in (typ, InferredNullability.create TypeOrigin.ArrayAccess) @@ -1195,7 +1196,8 @@ let typecheck_instr tenv calls_this checks (node : Procdesc.Node.t) idenv curr_p in if checks.eradicate then EradicateChecks.check_object_dereference ~nullsafe_mode tenv find_canonical_duplicate - curr_pdesc node instr_ref array_exp DereferenceRule.ArrayLengthAccess ta loc ; + curr_pdesc node instr_ref array_exp DereferenceRule.ReportableViolation.ArrayLengthAccess + ta loc ; TypeState.add_id id (Typ.mk (Tint Typ.IInt), InferredNullability.create TypeOrigin.ArrayLengthResult) typestate ~descr:"array.length" diff --git a/infer/src/nullsafe/typeErr.ml b/infer/src/nullsafe/typeErr.ml index b182e0600..b4d662066 100644 --- a/infer/src/nullsafe/typeErr.ml +++ b/infer/src/nullsafe/typeErr.ml @@ -72,7 +72,7 @@ type err_instance = | Nullable_dereference of { dereference_violation: DereferenceRule.violation ; dereference_location: Location.t - ; dereference_type: DereferenceRule.dereference_type + ; dereference_type: DereferenceRule.ReportableViolation.dereference_type ; nullable_object_descr: string option ; nullable_object_origin: TypeOrigin.t } | Bad_assignment of @@ -262,15 +262,15 @@ let get_error_info_if_reportable ~nullsafe_mode err_instance = ; nullable_object_descr ; dereference_type ; nullable_object_origin } -> + let+ reportable_violation = + DereferenceRule.to_reportable_violation nullsafe_mode dereference_violation + in let description, issue_type, error_location = - DereferenceRule.violation_description ~dereference_location dereference_violation - dereference_type ~nullable_object_descr ~nullable_object_origin + DereferenceRule.ReportableViolation.get_description reportable_violation + ~dereference_location dereference_type ~nullable_object_descr ~nullable_object_origin in - Some - ( description - , issue_type - , Some error_location - , DereferenceRule.violation_severity dereference_violation ) + let severity = DereferenceRule.ReportableViolation.get_severity reportable_violation in + (description, issue_type, Some error_location, severity) | Inconsistent_subclass {inheritance_violation; violation_type; base_proc_name; overridden_proc_name} -> Some diff --git a/infer/src/nullsafe/typeErr.mli b/infer/src/nullsafe/typeErr.mli index 2470ab151..983cb7d8d 100644 --- a/infer/src/nullsafe/typeErr.mli +++ b/infer/src/nullsafe/typeErr.mli @@ -48,7 +48,7 @@ type err_instance = | Nullable_dereference of { dereference_violation: DereferenceRule.violation ; dereference_location: Location.t - ; dereference_type: DereferenceRule.dereference_type + ; dereference_type: DereferenceRule.ReportableViolation.dereference_type ; nullable_object_descr: string option ; nullable_object_origin: TypeOrigin.t } | Bad_assignment of diff --git a/infer/tests/codetoanalyze/java/nullsafe-default/issues.exp b/infer/tests/codetoanalyze/java/nullsafe-default/issues.exp index 6a5e8439f..29295a845 100644 --- a/infer/tests/codetoanalyze/java/nullsafe-default/issues.exp +++ b/infer/tests/codetoanalyze/java/nullsafe-default/issues.exp @@ -139,7 +139,7 @@ codetoanalyze/java/nullsafe-default/InheritanceForStrictMode.java, codetoanalyze codetoanalyze/java/nullsafe-default/InheritanceForStrictMode.java, codetoanalyze.java.nullsafe_default.InheritanceForStrictMode$StrictExtendingNonstrict.params(java.lang.String,java.lang.String):void, 0, ERADICATE_INCONSISTENT_SUBCLASS_PARAMETER_ANNOTATION, no_bucket, ERROR, [First parameter `badToRemoveNullableInChildren` of method `InheritanceForStrictMode$StrictExtendingNonstrict.params(...)` is missing `@Nullable` declaration when overriding `InheritanceForStrictMode$NonStrictBase.params(...)`. The parent method declared it can handle `null` for this param, so the child should also declare that.] codetoanalyze/java/nullsafe-default/InheritanceForStrictMode.java, codetoanalyze.java.nullsafe_default.InheritanceForStrictMode$StrictExtendingStrict.badToAddNullableInChildren():java.lang.String, 0, ERADICATE_INCONSISTENT_SUBCLASS_RETURN_ANNOTATION, no_bucket, ERROR, [Child method `InheritanceForStrictMode$StrictExtendingStrict.badToAddNullableInChildren()` is not substitution-compatible with its parent: the return type is declared as nullable, but parent method `InheritanceForStrictMode$StrictBase.badToAddNullableInChildren()` is missing `@Nullable` declaration. Either mark the parent as `@Nullable` or ensure the child does not return `null`.] codetoanalyze/java/nullsafe-default/InheritanceForStrictMode.java, codetoanalyze.java.nullsafe_default.InheritanceForStrictMode$StrictExtendingStrict.params(java.lang.String,java.lang.String):void, 0, ERADICATE_INCONSISTENT_SUBCLASS_PARAMETER_ANNOTATION, no_bucket, ERROR, [First parameter `badToRemoveNullableInChildren` of method `InheritanceForStrictMode$StrictExtendingStrict.params(...)` is missing `@Nullable` declaration when overriding `InheritanceForStrictMode$StrictBase.params(...)`. The parent method declared it can handle `null` for this param, so the child should also declare that.] -codetoanalyze/java/nullsafe-default/JunitExample.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_IS_CLEAN, no_bucket, INFO, [] +codetoanalyze/java/nullsafe-default/JunitExample.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_NEEDS_FIXING, no_bucket, INFO, [] codetoanalyze/java/nullsafe-default/LibraryCalls.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_NEEDS_FIXING, no_bucket, INFO, [] codetoanalyze/java/nullsafe-default/LibraryCalls.java, codetoanalyze.java.nullsafe_default.LibraryCalls.badAtomicReferenceDereference(java.util.concurrent.atomic.AtomicReference):java.lang.String, 0, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, WARNING, [`ref.get()` is nullable and is not locally checked for null when calling `toString()`: call to AtomicReference.get() at line 35 (nullable according to nullsafe internal models).] codetoanalyze/java/nullsafe-default/LibraryCalls.java, codetoanalyze.java.nullsafe_default.LibraryCalls.badPhantomReferenceDereference(java.lang.ref.PhantomReference):java.lang.String, 0, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, WARNING, [`ref.get()` is nullable and is not locally checked for null when calling `toString()`: call to PhantomReference.get() at line 27 (nullable according to nullsafe internal models).] @@ -198,7 +198,7 @@ codetoanalyze/java/nullsafe-default/NullMethodCall.java, Linters_dummy_method, 1 codetoanalyze/java/nullsafe-default/NullMethodCall.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_IS_CLEAN, no_bucket, INFO, [] codetoanalyze/java/nullsafe-default/NullMethodCall.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_IS_CLEAN, no_bucket, INFO, [] codetoanalyze/java/nullsafe-default/NullMethodCall.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_IS_CLEAN, no_bucket, INFO, [] -codetoanalyze/java/nullsafe-default/NullMethodCall.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_IS_CLEAN, no_bucket, INFO, [] +codetoanalyze/java/nullsafe-default/NullMethodCall.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_NEEDS_FIXING, no_bucket, INFO, [] codetoanalyze/java/nullsafe-default/NullMethodCall.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_NEEDS_FIXING, no_bucket, INFO, [] codetoanalyze/java/nullsafe-default/NullMethodCall.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_NEEDS_FIXING, no_bucket, INFO, [] codetoanalyze/java/nullsafe-default/NullMethodCall.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_NEEDS_FIXING, no_bucket, INFO, [] @@ -229,7 +229,7 @@ codetoanalyze/java/nullsafe-default/NullMethodCall.java, codetoanalyze.java.null codetoanalyze/java/nullsafe-default/NullsafeMode.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_IS_CLEAN, no_bucket, INFO, [] codetoanalyze/java/nullsafe-default/NullsafeMode.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_IS_CLEAN, no_bucket, INFO, [] codetoanalyze/java/nullsafe-default/NullsafeMode.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_IS_CLEAN, no_bucket, INFO, [] -codetoanalyze/java/nullsafe-default/NullsafeMode.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_IS_CLEAN, no_bucket, INFO, [] +codetoanalyze/java/nullsafe-default/NullsafeMode.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_NEEDS_FIXING, no_bucket, INFO, [] codetoanalyze/java/nullsafe-default/NullsafeMode.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_NEEDS_FIXING, no_bucket, INFO, [] codetoanalyze/java/nullsafe-default/NullsafeMode.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_NEEDS_FIXING, no_bucket, INFO, [] codetoanalyze/java/nullsafe-default/NullsafeMode.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_NEEDS_FIXING, no_bucket, INFO, [] @@ -373,7 +373,7 @@ codetoanalyze/java/nullsafe-default/TrueFalseOnNull.java, Linters_dummy_method, codetoanalyze/java/nullsafe-default/TrueFalseOnNull.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_IS_CLEAN, no_bucket, INFO, [] codetoanalyze/java/nullsafe-default/TrueFalseOnNull.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_IS_CLEAN, no_bucket, INFO, [] codetoanalyze/java/nullsafe-default/TrueFalseOnNull.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_IS_CLEAN, no_bucket, INFO, [] -codetoanalyze/java/nullsafe-default/TrueFalseOnNull.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_IS_CLEAN, no_bucket, INFO, [] +codetoanalyze/java/nullsafe-default/TrueFalseOnNull.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_NEEDS_FIXING, no_bucket, INFO, [] codetoanalyze/java/nullsafe-default/TrueFalseOnNull.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_NEEDS_FIXING, no_bucket, INFO, [] codetoanalyze/java/nullsafe-default/TrueFalseOnNull.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_NEEDS_FIXING, no_bucket, INFO, [] codetoanalyze/java/nullsafe-default/TrueFalseOnNull.java, Linters_dummy_method, 1, ERADICATE_META_CLASS_NEEDS_FIXING, no_bucket, INFO, []