diff --git a/infer/src/nullsafe/eradicate.ml b/infer/src/nullsafe/eradicate.ml index 4061176f5..e14c3701b 100644 --- a/infer/src/nullsafe/eradicate.ml +++ b/infer/src/nullsafe/eradicate.ml @@ -163,7 +163,9 @@ module MkCallback (Extension : ExtensionT) : CallBackT = struct typecheck_proc in EradicateChecks.check_constructor_initialization tenv find_canonical_duplicate curr_pname - curr_pdesc start_node ~typestates_for_curr_constructor_and_all_initializer_methods + curr_pdesc start_node + ~is_strict_mode:annotated_signature.AnnotatedSignature.is_strict_mode + ~typestates_for_curr_constructor_and_all_initializer_methods ~typestates_for_all_constructors_incl_current proc_loc ; if Config.eradicate_verbose then L.result "Final Typestate@\n%a@." TypeState.pp typestate ) diff --git a/infer/src/nullsafe/eradicateChecks.ml b/infer/src/nullsafe/eradicateChecks.ml index 9f36a47e2..3e0f6836c 100644 --- a/infer/src/nullsafe/eradicateChecks.ml +++ b/infer/src/nullsafe/eradicateChecks.ml @@ -235,7 +235,8 @@ let get_nullability_upper_bound field_name typestate_list = (** Check field initialization for a given constructor *) let check_constructor_initialization tenv find_canonical_duplicate curr_constructor_pname - curr_constructor_pdesc start_node ~typestates_for_curr_constructor_and_all_initializer_methods + curr_constructor_pdesc start_node ~is_strict_mode + ~typestates_for_curr_constructor_and_all_initializer_methods ~typestates_for_all_constructors_incl_current loc : unit = State.set_node start_node ; if Procname.is_constructor curr_constructor_pname then @@ -297,7 +298,8 @@ let check_constructor_initialization tenv find_canonical_duplicate curr_construc && not is_initialized_in_either_constructor_or_initializer then report_error tenv find_canonical_duplicate - (TypeErr.Field_not_initialized field_name) None loc curr_constructor_pdesc ; + (TypeErr.Field_not_initialized {is_strict_mode; field_name}) + None loc curr_constructor_pdesc ; (* Check if field is over-annotated. *) match annotated_field with | None -> diff --git a/infer/src/nullsafe/typeErr.ml b/infer/src/nullsafe/typeErr.ml index 69a0fc28c..5b6d8724f 100644 --- a/infer/src/nullsafe/typeErr.ml +++ b/infer/src/nullsafe/typeErr.ml @@ -64,7 +64,7 @@ type err_instance = ; violation_type: InheritanceRule.violation_type ; base_proc_name: Procname.t ; overridden_proc_name: Procname.t } - | Field_not_initialized of Fieldname.t + | Field_not_initialized of {is_strict_mode: bool; field_name: Fieldname.t} | Over_annotation of { over_annotated_violation: OverAnnotatedRule.violation ; violation_type: OverAnnotatedRule.violation_type } @@ -188,9 +188,9 @@ module Severity = struct None | Over_annotation _ -> None - | Field_not_initialized _ -> + | Field_not_initialized {is_strict_mode} -> (* TODO: show strict mode violations as errors *) - None + Some (if is_strict_mode then Exceptions.Error else Exceptions.Warning) | Bad_assignment {assignment_violation} -> Some (AssignmentRule.violation_severity assignment_violation) | Inconsistent_subclass {inheritance_violation} -> @@ -215,7 +215,7 @@ type st_report_error = let get_field_name_for_error_suppressing = function | Over_annotation {violation_type= OverAnnotatedRule.FieldOverAnnoted field_name} -> Some field_name - | Field_not_initialized field_name -> + | Field_not_initialized {field_name} -> Some field_name | Condition_redundant _ | Over_annotation {violation_type= OverAnnotatedRule.ReturnOverAnnotated _} @@ -241,7 +241,7 @@ let get_error_info err_instance = | OverAnnotatedRule.ReturnOverAnnotated _ -> IssueType.eradicate_return_over_annotated ) , None ) - | Field_not_initialized field_name -> + | Field_not_initialized {field_name} -> ( Format.asprintf "Field %a is declared non-nullable, so it should be initialized in the constructor or in \ an `@Initializer` method" diff --git a/infer/src/nullsafe/typeErr.mli b/infer/src/nullsafe/typeErr.mli index f030ebc38..618fe6948 100644 --- a/infer/src/nullsafe/typeErr.mli +++ b/infer/src/nullsafe/typeErr.mli @@ -40,7 +40,7 @@ type err_instance = ; violation_type: InheritanceRule.violation_type ; base_proc_name: Procname.t ; overridden_proc_name: Procname.t } - | Field_not_initialized of Fieldname.t + | Field_not_initialized of {is_strict_mode: bool; field_name: Fieldname.t} | Over_annotation of { over_annotated_violation: OverAnnotatedRule.violation ; violation_type: OverAnnotatedRule.violation_type } diff --git a/infer/tests/codetoanalyze/java/nullsafe-default/StrictMode.java b/infer/tests/codetoanalyze/java/nullsafe-default/StrictMode.java index d080810de..71980dd0c 100644 --- a/infer/tests/codetoanalyze/java/nullsafe-default/StrictMode.java +++ b/infer/tests/codetoanalyze/java/nullsafe-default/StrictMode.java @@ -14,6 +14,8 @@ import javax.annotation.Nullable; @NullsafeStrict class Strict { + public String notInitializedIsBAD; + public @Nullable String nullable; public @Nonnull String nonnull = ""; diff --git a/infer/tests/codetoanalyze/java/nullsafe-default/issues.exp b/infer/tests/codetoanalyze/java/nullsafe-default/issues.exp index 3e9854deb..eb0c82869 100644 --- a/infer/tests/codetoanalyze/java/nullsafe-default/issues.exp +++ b/infer/tests/codetoanalyze/java/nullsafe-default/issues.exp @@ -220,22 +220,23 @@ 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, [`return_null_in_catch()`: return type is declared non-nullable but the method returns `null`: 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, [`return_null_in_catch_after_throw()`: return type is declared non-nullable but the method returns `null`: 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, [`tryWithResourcesReturnNullable(...)`: return type is declared non-nullable but the method returns a nullable value: call to nullToNullableIsOK() at line 142.] -codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_convertingNonnullToNonnullIsBad():java.lang.String, 0, ERADICATE_UNCHECKED_NONSTRICT_FROM_STRICT, no_bucket, ERROR, [`NonStrict.getNonnull()`: `@NullsafeStrict` mode prohibits using values coming from non-strict classes without a check. Result of this call is used at line 161. Either add a local check for null or assertion, or strictify NonStrict.] +codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.(), 0, ERADICATE_FIELD_NOT_INITIALIZED, no_bucket, ERROR, [Field `notInitializedIsBAD` is declared non-nullable, so it should be initialized in the constructor or in an `@Initializer` method] +codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_convertingNonnullToNonnullIsBad():java.lang.String, 0, ERADICATE_UNCHECKED_NONSTRICT_FROM_STRICT, no_bucket, ERROR, [`NonStrict.getNonnull()`: `@NullsafeStrict` mode prohibits using values coming from non-strict classes without a check. Result of this call is used at line 163. Either add a local check for null or assertion, or strictify NonStrict.] 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, ERROR, [`nonStrictClass_convertingNullableToNonnullIsBad()`: return type is declared non-nullable but the method returns a nullable value: call to getNullable() at line 135.] +codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_convertingNullableToNonnullIsBad():java.lang.String, 0, ERADICATE_RETURN_NOT_NULLABLE, no_bucket, ERROR, [`nonStrictClass_convertingNullableToNonnullIsBad()`: return type is declared non-nullable but the method returns a nullable value: call to getNullable() at line 137.] codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_dereferenceNonnullFieldAfterCheckIsOK():void, 1, 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, 0, ERADICATE_UNCHECKED_NONSTRICT_FROM_STRICT, no_bucket, ERROR, [`NonStrict.nonnull`: `@NullsafeStrict` mode prohibits using values coming from non-strict classes without a check. This field is used at line 131. Either add a local check for null or assertion, or strictify NonStrict.] +codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_dereferenceNonnullFieldIsBad():void, 0, ERADICATE_UNCHECKED_NONSTRICT_FROM_STRICT, no_bucket, ERROR, [`NonStrict.nonnull`: `@NullsafeStrict` mode prohibits using values coming from non-strict classes without a check. This field is used at line 133. Either add a local check for null or assertion, or strictify NonStrict.] codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_dereferenceNonnullMethodAfterCheckIsOK():void, 1, 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, 0, ERADICATE_UNCHECKED_NONSTRICT_FROM_STRICT, no_bucket, ERROR, [`NonStrict.getNonnull()`: `@NullsafeStrict` mode prohibits using values coming from non-strict classes without a check. Result of this call is used at line 113. Either add a local check for null or assertion, or strictify NonStrict.] -codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_dereferenceNonnullStaticMethodIsBad():void, 0, ERADICATE_UNCHECKED_NONSTRICT_FROM_STRICT, no_bucket, ERROR, [`NonStrict.staticNonnull()`: `@NullsafeStrict` mode prohibits using values coming from non-strict classes without a check. Result of this call is used at line 122. Either add a local check for null or assertion, or strictify NonStrict.] +codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_dereferenceNonnullMethodIsBad():void, 0, ERADICATE_UNCHECKED_NONSTRICT_FROM_STRICT, no_bucket, ERROR, [`NonStrict.getNonnull()`: `@NullsafeStrict` mode prohibits using values coming from non-strict classes without a check. Result of this call is used at line 115. Either add a local check for null or assertion, or strictify NonStrict.] +codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_dereferenceNonnullStaticMethodIsBad():void, 0, ERADICATE_UNCHECKED_NONSTRICT_FROM_STRICT, no_bucket, ERROR, [`NonStrict.staticNonnull()`: `@NullsafeStrict` mode prohibits using values coming from non-strict classes without a check. Result of this call is used at line 124. Either add a local check for null or assertion, or strictify NonStrict.] codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_dereferenceNullableFieldIsBad():void, 0, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, ERROR, [`__new(...).nullable` is nullable and is not locally checked for null when calling `toString()`.] codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_dereferenceNullableMethodIsBad():void, 0, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, ERROR, [`__new(...).getNullable()` is nullable and is not locally checked for null when calling `toString()`.] codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.nonStrictClass_dereferenceNullableStaticMethodIsBad():void, 0, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, ERROR, [`staticNullable()` is nullable and is not locally checked for null when calling `toString()`.] -codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.sameClass_convertingNullableToNonnullIsBad():java.lang.String, 0, ERADICATE_RETURN_NOT_NULLABLE, no_bucket, ERROR, [`sameClass_convertingNullableToNonnullIsBad()`: return type is declared non-nullable but the method returns a nullable value: call to getNullable() at line 63.] +codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.sameClass_convertingNullableToNonnullIsBad():java.lang.String, 0, ERADICATE_RETURN_NOT_NULLABLE, no_bucket, ERROR, [`sameClass_convertingNullableToNonnullIsBad()`: return type is declared non-nullable but the method returns a nullable value: call to getNullable() at line 65.] codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.sameClass_dereferenceNullableFieldIsBad():void, 0, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, ERROR, [`Strict.nullable` is nullable and is not locally checked for null when calling `toString()`.] codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.sameClass_dereferenceNullableMethodIsBad():void, 0, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, ERROR, [`getNullable()` is nullable and is not locally checked for null when calling `toString()`.] codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.sameClass_dereferenceNullableStaticMethodIsBad():void, 0, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, ERROR, [`staticNullable()` is nullable and is not locally checked for null when calling `toString()`.] -codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.strictClass_convertingNullableToNonnullIsBad():java.lang.String, 0, ERADICATE_RETURN_NOT_NULLABLE, no_bucket, ERROR, [`strictClass_convertingNullableToNonnullIsBad()`: return type is declared non-nullable but the method returns a nullable value: call to getNullable() at line 97.] +codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.strictClass_convertingNullableToNonnullIsBad():java.lang.String, 0, ERADICATE_RETURN_NOT_NULLABLE, no_bucket, ERROR, [`strictClass_convertingNullableToNonnullIsBad()`: return type is declared non-nullable but the method returns a nullable value: call to getNullable() at line 99.] codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.strictClass_dereferenceNullableFieldIsBad():void, 0, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, ERROR, [`__new(...).nullable` is nullable and is not locally checked for null when calling `toString()`.] codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.strictClass_dereferenceNullableMethodIsBad():void, 0, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, ERROR, [`__new(...).getNullable()` is nullable and is not locally checked for null when calling `toString()`.] codetoanalyze/java/nullsafe-default/StrictMode.java, codetoanalyze.java.nullsafe_default.Strict.strictClass_dereferenceNullableStaticMethodIsBad():void, 0, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, ERROR, [`staticNullable()` is nullable and is not locally checked for null when calling `toString()`.]