diff --git a/infer/tests/codetoanalyze/java/nullsafe-default/FieldNullabilityMemoization.java b/infer/tests/codetoanalyze/java/nullsafe-default/FieldNullabilityMemoization.java new file mode 100644 index 000000000..c967c006d --- /dev/null +++ b/infer/tests/codetoanalyze/java/nullsafe-default/FieldNullabilityMemoization.java @@ -0,0 +1,89 @@ +/* + * 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 javax.annotation.Nullable; + +/** + * Nullsafe has a feature: field nullability is memoized within a method. In other words, nullsafe + * assumes: + * + *
NOTE: This feature is unsound, but assumptions a) and b) mostly hold for real codebases, so + * here nullsafe tradeoffs theoretical unsoundness for practical usability. + * + *
This class tests basic properties of this feature.
+ */
+public class FieldNullabilityMemoization {
+ private @Nullable Object nullable;
+
+ void dereferenceIsBAD() {
+ nullable.toString();
+ }
+
+ void dereferenceViaLocalVarIsBAD() {
+ Object a = nullable;
+ a.toString();
+ }
+
+ void dereferenceAfterCheckIsOK() {
+ if (nullable != null) {
+ // Theoretically, a different thread could modify the field right here.
+ // But practically, if such things can happen, we have much bigger problems than nullability.
+ nullable.toString();
+ }
+ }
+
+ void dereferenceAfterCheckViaLocalVarIsOK() {
+ if (nullable != null) {
+ // Theoretically, a different thread could modify the field right here.
+ // But practically, if such things can happen, we have much bigger problems than nullability.
+ Object a = nullable;
+ a.toString();
+ }
+ }
+
+ void dereferenceAfterNonnullAssignmentIsOK() {
+ nullable = "";
+ // Theoretically, a different thread could modify the field right here.
+ // But practically, if such things can happen, we have much bigger problems than nullability.
+ nullable.toString();
+ }
+
+ void dereferenceAfterNonnullAssignmentViaLocalVarIsOK() {
+ nullable = "";
+
+ // Theoretically, a different thread could modify the field right here.
+ // But practically, if such things can happen, we have much bigger problems than nullability.
+
+ Object a = nullable;
+ a.toString();
+ }
+
+ void FN_nullabilityIsPreservedEvenOnMethodCalls() {
+ nullable = "";
+
+ // Calling methods does not invalidate nullability of fields,
+ // even if they theoritically can nullify the field.
+ // In practice, this happens extremely rarely, but in this synthetic example
+ // this will lead to an NPE.
+ nullify();
+
+ // Uncaught NPE
+ nullable.toString();
+ }
+
+ private void nullify() {
+ nullable = null;
+ }
+}
diff --git a/infer/tests/codetoanalyze/java/nullsafe-default/issues.exp b/infer/tests/codetoanalyze/java/nullsafe-default/issues.exp
index b492b882d..3ddc634a1 100644
--- a/infer/tests/codetoanalyze/java/nullsafe-default/issues.exp
+++ b/infer/tests/codetoanalyze/java/nullsafe-default/issues.exp
@@ -67,6 +67,8 @@ codetoanalyze/java/nullsafe-default/FieldNotNullable.java, codetoanalyze.java.nu
codetoanalyze/java/nullsafe-default/FieldNotNullable.java, codetoanalyze.java.nullsafe_default.FieldNotNullable.setNullableToNotNullableIsBAD(java.lang.String):void, 0, ERADICATE_FIELD_NOT_NULLABLE, no_bucket, WARNING, [`notNullable` is declared non-nullable but is assigned `null`: null constant at line 65.]
codetoanalyze/java/nullsafe-default/FieldNotNullable.java, codetoanalyze.java.nullsafe_default.FieldNotNullable.setNullableToNotNullableIsBAD(java.lang.String):void, 1, ERADICATE_FIELD_NOT_NULLABLE, no_bucket, WARNING, [`notNullable` is declared non-nullable but is assigned a nullable: method parameter s.]
codetoanalyze/java/nullsafe-default/FieldNotNullable.java, codetoanalyze.java.nullsafe_default.FieldNotNullable.setNullableToNotNullableIsBAD(java.lang.String):void, 2, ERADICATE_FIELD_NOT_NULLABLE, no_bucket, WARNING, [`notNullable` is declared non-nullable but is assigned a nullable: call to getNullable() at line 67.]
+codetoanalyze/java/nullsafe-default/FieldNullabilityMemoization.java, codetoanalyze.java.nullsafe_default.FieldNullabilityMemoization.dereferenceIsBAD():void, 0, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, WARNING, [`FieldNullabilityMemoization.nullable` is nullable and is not locally checked for null when calling `toString()`.]
+codetoanalyze/java/nullsafe-default/FieldNullabilityMemoization.java, codetoanalyze.java.nullsafe_default.FieldNullabilityMemoization.dereferenceViaLocalVarIsBAD():void, 1, ERADICATE_NULLABLE_DEREFERENCE, no_bucket, WARNING, [`a` is nullable and is not locally checked for null when calling `toString()`: field nullable at line 35.]
codetoanalyze/java/nullsafe-default/FieldOverAnnotated.java, codetoanalyze.java.nullsafe_default.FieldOverAnnotated.