Skip to content

Commit

Permalink
Introduce a NullSpecTypeValidator to ensure unspecified type variab…
Browse files Browse the repository at this point in the history
…les are ok (#178)
  • Loading branch information
wmdietl authored Jul 25, 2024
1 parent 39764fb commit e1069a2
Show file tree
Hide file tree
Showing 7 changed files with 90 additions and 5 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -145,6 +145,7 @@ final class NullSpecAnnotatedTypeFactory
new TypeUseLocation[] {
TypeUseLocation.CONSTRUCTOR_RESULT,
TypeUseLocation.EXCEPTION_PARAMETER,
TypeUseLocation.IMPLICIT_LOWER_BOUND,
TypeUseLocation.RECEIVER,
};

Expand All @@ -157,10 +158,6 @@ final class NullSpecAnnotatedTypeFactory

private static final TypeUseLocation[] defaultLocationsUnspecified =
new TypeUseLocation[] {
// Lower bounds could be MinusNull, but all uses in unmarked code would become unspecified
// anyways.
// Revisit once https://github.com/eisop/checker-framework/issues/741 is fixed.
TypeUseLocation.IMPLICIT_LOWER_BOUND,
TypeUseLocation.IMPLICIT_WILDCARD_UPPER_BOUND_NO_SUPER,
TypeUseLocation.TYPE_VARIABLE_USE,
TypeUseLocation.OTHERWISE
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,45 @@
// Copyright 2020 The JSpecify Authors
//
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
// http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.

package com.google.jspecify.nullness;

import javax.lang.model.element.AnnotationMirror;
import org.checkerframework.common.basetype.BaseTypeChecker;
import org.checkerframework.common.basetype.BaseTypeValidator;
import org.checkerframework.framework.type.AnnotatedTypeMirror;

final class NullSpecTypeValidator extends BaseTypeValidator {
private final AnnotationMirror nullnessOperatorUnspecified;

/** Constructor. */
NullSpecTypeValidator(
BaseTypeChecker checker,
NullSpecVisitor visitor,
NullSpecAnnotatedTypeFactory atypeFactory,
Util util) {
super(checker, visitor, atypeFactory);

nullnessOperatorUnspecified = util.nullnessOperatorUnspecified;
}

@Override
public boolean areBoundsValid(AnnotatedTypeMirror upperBound, AnnotatedTypeMirror lowerBound) {
if (upperBound.hasAnnotation(nullnessOperatorUnspecified)
|| lowerBound.hasAnnotation(nullnessOperatorUnspecified)) {
return true;
} else {
return super.areBoundsValid(upperBound, lowerBound);
}
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -71,6 +71,7 @@
import javax.lang.model.type.DeclaredType;
import javax.lang.model.type.TypeMirror;
import org.checkerframework.common.basetype.BaseTypeVisitor;
import org.checkerframework.common.basetype.TypeValidator;
import org.checkerframework.framework.type.AnnotatedTypeMirror;
import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType;
import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType;
Expand Down Expand Up @@ -637,4 +638,9 @@ protected NullSpecAnnotatedTypeFactory createTypeFactory() {
// Reading util this way is ugly but necessary. See discussion in NullSpecChecker.
return new NullSpecAnnotatedTypeFactory(checker, ((NullSpecChecker) checker).util);
}

@Override
protected TypeValidator createTypeValidator() {
return new NullSpecTypeValidator(checker, this, atypeFactory, ((NullSpecChecker) checker).util);
}
}
12 changes: 12 additions & 0 deletions src/test/java/tests/NullSpecTest.java
Original file line number Diff line number Diff line change
Expand Up @@ -54,6 +54,18 @@ public static String[] getTestDirs() {
}
}

/** A small set of strict regression tests. */
public static class RegressionStrict extends NullSpecTest {
public RegressionStrict(List<File> testFiles) {
super(testFiles, true);
}

@Parameters
public static String[] getTestDirs() {
return new String[] {"regression-strict"};
}
}

/** A test that ignores cases where there is limited nullness information. */
public static class Lenient extends NullSpecTest {
public Lenient(List<File> testFiles) {
Expand Down
5 changes: 4 additions & 1 deletion tests/ConformanceTest-report.txt
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
# 90 pass; 24 fail; 114 total; 78.9% score
# 93 pass; 24 fail; 117 total; 79.5% score
PASS: Basic.java:28:test:expression-type:Object?:nullable
PASS: Basic.java:28:test:sink-type:Object!:return
PASS: Basic.java:28:test:cannot-convert:Object? to Object!
Expand Down Expand Up @@ -44,6 +44,7 @@ PASS: irrelevantannotations/notnullmarked/Other.java:Nullable local variable arr
PASS: irrelevantannotations/notnullmarked/Other.java:NonNull local variable array:test:irrelevant-annotation:NonNull
PASS: irrelevantannotations/notnullmarked/Other.java:Nullable exception parameter:test:irrelevant-annotation:Nullable
PASS: irrelevantannotations/notnullmarked/Other.java:NonNull exception parameter:test:irrelevant-annotation:NonNull
PASS: irrelevantannotations/notnullmarked/Other.java:Intrinsically NonNull exception parameter cannot be assigned null:test:cannot-convert:null? to RuntimeException!
PASS: irrelevantannotations/notnullmarked/Other.java:Nullable try-with-resources:test:irrelevant-annotation:Nullable
FAIL: irrelevantannotations/notnullmarked/Other.java:NonNull try-with-resources:test:irrelevant-annotation:NonNull
FAIL: irrelevantannotations/notnullmarked/Other.java:Nullable exception type:test:irrelevant-annotation:Nullable
Expand Down Expand Up @@ -75,6 +76,7 @@ PASS: irrelevantannotations/nullmarked/Other.java:Nullable local variable array:
PASS: irrelevantannotations/nullmarked/Other.java:NonNull local variable array:test:irrelevant-annotation:NonNull
PASS: irrelevantannotations/nullmarked/Other.java:Nullable exception parameter:test:irrelevant-annotation:Nullable
PASS: irrelevantannotations/nullmarked/Other.java:NonNull exception parameter:test:irrelevant-annotation:NonNull
PASS: irrelevantannotations/nullmarked/Other.java:Intrinsically NonNull exception parameter cannot be assigned null:test:cannot-convert:null? to RuntimeException!
PASS: irrelevantannotations/nullmarked/Other.java:Nullable try-with-resources:test:irrelevant-annotation:Nullable
FAIL: irrelevantannotations/nullmarked/Other.java:NonNull try-with-resources:test:irrelevant-annotation:NonNull
FAIL: irrelevantannotations/nullmarked/Other.java:Nullable exception type:test:irrelevant-annotation:Nullable
Expand Down Expand Up @@ -107,6 +109,7 @@ PASS: irrelevantannotations/nullunmarked/Other.java:Nullable local variable arra
PASS: irrelevantannotations/nullunmarked/Other.java:NonNull local variable array:test:irrelevant-annotation:NonNull
PASS: irrelevantannotations/nullunmarked/Other.java:Nullable exception parameter:test:irrelevant-annotation:Nullable
PASS: irrelevantannotations/nullunmarked/Other.java:NonNull exception parameter:test:irrelevant-annotation:NonNull
PASS: irrelevantannotations/nullunmarked/Other.java:Intrinsically NonNull exception parameter cannot be assigned null:test:cannot-convert:null? to RuntimeException!
PASS: irrelevantannotations/nullunmarked/Other.java:Nullable try-with-resources:test:irrelevant-annotation:Nullable
FAIL: irrelevantannotations/nullunmarked/Other.java:NonNull try-with-resources:test:irrelevant-annotation:NonNull
FAIL: irrelevantannotations/nullunmarked/Other.java:Nullable exception type:test:irrelevant-annotation:Nullable
Expand Down
18 changes: 18 additions & 0 deletions tests/regression-strict/Issue177.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
// Copyright 2024 The JSpecify Authors
//
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
// http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.

// Test case for Issue 177:
// https://github.com/jspecify/jspecify-reference-checker/issues/177

class Issue177<T> {}
4 changes: 4 additions & 0 deletions tests/regression/Issue172.java
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,10 @@ class Issue172<E> {
E e() {
return null;
}

void p(E p) {
p = null;
}
}

class Issue172UnmarkedUse {
Expand Down

0 comments on commit e1069a2

Please sign in to comment.