Skip to content

Commit

Permalink
Enrich treatment of @PolyNull; fixes #3614
Browse files Browse the repository at this point in the history
  • Loading branch information
@mernst
mernst authored Oct 29, 2020
1 parent 38b8ca2 commit 1a0712f
Show file tree
Hide file tree
Showing 8 changed files with 325 additions and 44 deletions.
12 changes: 8 additions & 4 deletions ...ker/src/main/java/org/checkerframework/checker/nullness/NullnessAnnotatedTypeFactory.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -261,8 +261,8 @@ protected Set<Class<? extends Annotation>> createSupportedTypeQualifiers() {

/**
* For types of left-hand side of an assignment, this method replaces {@link PolyNull} with
* {@link Nullable} if the org.checkerframework.dataflow analysis has determined that this is
* allowed soundly. For example:
* {@link Nullable} (or with {@link NonNull} if the org.checkerframework.dataflow analysis has
* determined that this is allowed soundly. For example:
*
* <pre> @PolyNull String foo(@PolyNull String param) {
* if (param == null) {
Expand All @@ -280,8 +280,12 @@ protected Set<Class<? extends Annotation>> createSupportedTypeQualifiers() {
protected void replacePolyQualifier(AnnotatedTypeMirror lhsType, Tree context) {
if (lhsType.hasAnnotation(PolyNull.class)) {
NullnessValue inferred = getInferredValueFor(context);
if (inferred != null && inferred.isPolyNullNull) {
lhsType.replaceAnnotation(NULLABLE);
if (inferred != null) {
if (inferred.isPolyNullNonNull) {
lhsType.replaceAnnotation(NONNULL);
} else if (inferred.isPolyNullNull) {
lhsType.replaceAnnotation(NULLABLE);
}
}
}
}
Expand Down
2 changes: 1 addition & 1 deletion checker/src/main/java/org/checkerframework/checker/nullness/NullnessChecker.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ public class NullnessChecker extends InitializationChecker {
public static final boolean LINT_DEFAULT_NOINITFORMONOTONICNONNULL = false;

/**
* Warn about redundant comparisons of expressions with {@code null}, if the expressions is
* Warn about redundant comparisons of an expression with {@code null}, if the expression is
* known to be non-null.
*/
public static final String LINT_REDUNDANTNULLCOMPARISON = "redundantNullComparison";
Expand Down
57 changes: 49 additions & 8 deletions checker/src/main/java/org/checkerframework/checker/nullness/NullnessStore.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@

import java.util.concurrent.atomic.AtomicLong;
import org.checkerframework.checker.initialization.InitializationStore;
import org.checkerframework.checker.nullness.qual.NonNull;
import org.checkerframework.checker.nullness.qual.Nullable;
import org.checkerframework.checker.nullness.qual.PolyNull;
import org.checkerframework.dataflow.cfg.visualize.CFGVisualizer;
Expand All @@ -11,11 +12,14 @@

/**
* Behaves like {@link InitializationStore}, but additionally tracks whether {@link PolyNull} is
* known to be {@link Nullable}.
* known to be {@link NonNull} or {@link Nullable} (or not known to be either).
*/
public class NullnessStore extends InitializationStore<NullnessValue, NullnessStore>
implements UniqueId {

/** True if, at this point, {@link PolyNull} is known to be {@link NonNull}. */
protected boolean isPolyNullNonNull;

/** True if, at this point, {@link PolyNull} is known to be {@link Nullable}. */
protected boolean isPolyNullNull;

Expand Down Expand Up @@ -44,22 +48,26 @@ public NullnessStore(
CFAbstractAnalysis<NullnessValue, NullnessStore, ?> analysis,
boolean sequentialSemantics) {
super(analysis, sequentialSemantics);
isPolyNullNonNull = false;
isPolyNullNull = false;
}

/**
* Create a NullnessStore (copy constructor).
*
* @param s a store to copy
*/
public NullnessStore(NullnessStore s) {
super(s);
isPolyNullNonNull = s.isPolyNullNonNull;
isPolyNullNull = s.isPolyNullNull;
}

@Override
public NullnessStore leastUpperBound(NullnessStore other) {
NullnessStore lub = super.leastUpperBound(other);
if (isPolyNullNull == other.isPolyNullNull) {
lub.isPolyNullNull = isPolyNullNull;
} else {
lub.isPolyNullNull = false;
}
lub.isPolyNullNonNull = isPolyNullNonNull && other.isPolyNullNonNull;
lub.isPolyNullNull = isPolyNullNull && other.isPolyNullNull;
return lub;
}

Expand All @@ -69,7 +77,8 @@ protected boolean supersetOf(CFAbstractStore<NullnessValue, NullnessStore> o) {
return false;
}
NullnessStore other = (NullnessStore) o;
if (other.isPolyNullNull != isPolyNullNull) {
if ((other.isPolyNullNonNull != isPolyNullNonNull)
|| (other.isPolyNullNull != isPolyNullNull)) {
return false;
}
return super.supersetOf(other);
Expand All @@ -79,13 +88,45 @@ protected boolean supersetOf(CFAbstractStore<NullnessValue, NullnessStore> o) {
protected String internalVisualize(CFGVisualizer<NullnessValue, NullnessStore, ?> viz) {
return super.internalVisualize(viz)
+ viz.getSeparator()
+ viz.visualizeStoreKeyVal("isPolyNonNull", isPolyNullNull);
+ viz.visualizeStoreKeyVal("isPolyNullNonNull", isPolyNullNonNull)
+ viz.getSeparator()
+ viz.visualizeStoreKeyVal("isPolyNullNull", isPolyNullNull);
}

/**
* Returns true if, at this point, {@link PolyNull} is known to be {@link NonNull}.
*
* @return true if, at this point, {@link PolyNull} is known to be {@link NonNull}
*/
public boolean isPolyNullNonNull() {
return isPolyNullNonNull;
}

/**
* Set the value of whether, at this point, {@link PolyNull} is known to be {@link NonNull}.
*
* @param isPolyNullNonNull whether, at this point, {@link PolyNull} is known to be {@link
* NonNull}
*/
public void setPolyNullNonNull(boolean isPolyNullNonNull) {
this.isPolyNullNonNull = isPolyNullNonNull;
}

/**
* Returns true if, at this point, {@link PolyNull} is known to be {@link Nullable}.
*
* @return true if, at this point, {@link PolyNull} is known to be {@link Nullable}
*/
public boolean isPolyNullNull() {
return isPolyNullNull;
}

/**
* Set the value of whether, at this point, {@link PolyNull} is known to be {@link Nullable}.
*
* @param isPolyNullNull whether, at this point, {@link PolyNull} is known to be {@link
* Nullable}
*/
public void setPolyNullNull(boolean isPolyNullNull) {
this.isPolyNullNull = isPolyNullNull;
}
Expand Down
93 changes: 89 additions & 4 deletions checker/src/main/java/org/checkerframework/checker/nullness/NullnessTransfer.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@
import java.util.Set;
import javax.lang.model.element.AnnotationMirror;
import javax.lang.model.element.ExecutableElement;
import javax.lang.model.element.VariableElement;
import javax.lang.model.type.TypeKind;
import javax.lang.model.type.TypeMirror;
import javax.lang.model.util.Elements;
Expand All @@ -29,13 +30,15 @@
import org.checkerframework.dataflow.cfg.node.ReturnNode;
import org.checkerframework.dataflow.cfg.node.ThrowNode;
import org.checkerframework.dataflow.expression.FlowExpressions;
import org.checkerframework.dataflow.expression.LocalVariable;
import org.checkerframework.dataflow.expression.Receiver;
import org.checkerframework.framework.flow.CFAbstractAnalysis;
import org.checkerframework.framework.flow.CFAbstractStore;
import org.checkerframework.framework.type.AnnotatedTypeMirror;
import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedDeclaredType;
import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType;
import org.checkerframework.framework.type.GenericAnnotatedTypeFactory;
import org.checkerframework.framework.type.visitor.SimpleAnnotatedTypeScanner;
import org.checkerframework.framework.util.AnnotatedTypes;
import org.checkerframework.javacutil.AnnotationBuilder;
import org.checkerframework.javacutil.AnnotationUtils;
Expand All @@ -48,10 +51,12 @@
*
* <ol>
* <li>After an expression is compared with the {@code null} literal, then that expression can
* safely be considered {@link NonNull} if the result of the comparison is false.
* safely be considered {@link NonNull} if the result of the comparison is false or {@link
* Nullable} if the result is true.
* <li>If an expression is dereferenced, then it can safely be assumed to non-null in the future.
* If it would not be, then the dereference would have raised a {@link NullPointerException}.
* <li>Tracks whether {@link PolyNull} is known to be {@link Nullable}.
* <li>Tracks whether {@link PolyNull} is known to be {@link NonNull} or {@link Nullable} (or not
* known to be either).
* </ol>
*/
public class NullnessTransfer
Expand All @@ -61,6 +66,8 @@ public class NullnessTransfer
protected final AnnotationMirror NONNULL;
/** The @{@link Nullable} annotation. */
protected final AnnotationMirror NULLABLE;
/** The @{@link PolyNull} annotation. */
protected final AnnotationMirror POLYNULL;

/**
* Java's Map interface.
Expand Down Expand Up @@ -91,6 +98,7 @@ public NullnessTransfer(NullnessAnalysis analysis) {
.getTypeFactoryOfSubchecker(KeyForSubchecker.class);
NONNULL = AnnotationBuilder.fromClass(elements, NonNull.class);
NULLABLE = AnnotationBuilder.fromClass(elements, Nullable.class);
POLYNULL = AnnotationBuilder.fromClass(elements, PolyNull.class);

MAP_TYPE =
(AnnotatedDeclaredType)
Expand Down Expand Up @@ -132,6 +140,7 @@ protected void refineToNonNull(TransferResult<NullnessValue, NullnessStore> resu
protected NullnessValue finishValue(NullnessValue value, NullnessStore store) {
value = super.finishValue(value, store);
if (value != null) {
value.isPolyNullNonNull = store.isPolyNullNonNull();
value.isPolyNullNull = store.isPolyNullNull();
}
return value;
Expand All @@ -142,6 +151,8 @@ protected NullnessValue finishValue(
NullnessValue value, NullnessStore thenStore, NullnessStore elseStore) {
value = super.finishValue(value, thenStore, elseStore);
if (value != null) {
value.isPolyNullNonNull =
thenStore.isPolyNullNonNull() && elseStore.isPolyNullNonNull();
value.isPolyNullNull = thenStore.isPolyNullNull() && elseStore.isPolyNullNull();
}
return value;
Expand Down Expand Up @@ -191,10 +202,19 @@ protected TransferResult<NullnessValue, NullnessStore> strengthenAnnotationOfEqu
if (nullnessTypeFactory.containsSameByClass(secondAnnos, PolyNull.class)) {
thenStore = thenStore == null ? res.getThenStore() : thenStore;
elseStore = elseStore == null ? res.getElseStore() : elseStore;
ExecutableElement methodElem =
TreeUtils.elementFromDeclaration(
analysis.getContainingMethod(secondNode.getTree()));
if (notEqualTo) {
elseStore.setPolyNullNull(true);
if (polyNullIsNonNull(methodElem, thenStore)) {
thenStore.setPolyNullNonNull(true);
}
} else {
thenStore.setPolyNullNull(true);
if (polyNullIsNonNull(methodElem, elseStore)) {
elseStore.setPolyNullNonNull(true);
}
}
}

Expand All @@ -205,6 +225,71 @@ protected TransferResult<NullnessValue, NullnessStore> strengthenAnnotationOfEqu
return res;
}

/**
* Returns true if every formal parameter that is declared as @PolyNull is currently known to be
* non-null.
*
* @param method a method
* @param s a store
* @return true if every formal parameter declared as @PolyNull is non-null
*/
private boolean polyNullIsNonNull(ExecutableElement method, NullnessStore s) {
// No need to check the receiver, which is always non-null.
for (VariableElement var : method.getParameters()) {
AnnotatedTypeMirror varType = atypeFactory.fromElement(var);

if (containsPolyNullNotAtTopLevel(varType)) {
return false;
}

if (varType.hasAnnotation(POLYNULL)) {
NullnessValue v = s.getValue(new LocalVariable(var));
if (!AnnotationUtils.containsSameByName(v.getAnnotations(), NONNULL)) {
return false;
}
}
}
return true;
}

/**
* A scanner that returns true if there is an occurrence of @PolyNull that is not at the top
* level.
*/
private class ContainsPolyNullNotAtTopLevelScanner
extends SimpleAnnotatedTypeScanner<Boolean, Void> {
/**
* True if the top-level type has not yet been processed (by the first call to
* defaultAction).
*/
private boolean isTopLevel = true;

/** Create a ContainsPolyNullNotAtTopLevelScanner. */
ContainsPolyNullNotAtTopLevelScanner() {
super(Boolean::logicalOr, false);
}

@Override
protected Boolean defaultAction(AnnotatedTypeMirror type, Void p) {
if (isTopLevel) {
isTopLevel = false;
return false;
} else {
return type.hasAnnotation(POLYNULL);
}
}
}

/**
* Returns true if there is an occurrence of @PolyNull that is not at the top level.
*
* @param t a type
* @return true if there is an occurrence of @PolyNull that is not at the top level
*/
private boolean containsPolyNullNotAtTopLevel(AnnotatedTypeMirror t) {
return new ContainsPolyNullNotAtTopLevelScanner().visit(t);
}

@Override
public TransferResult<NullnessValue, NullnessStore> visitArrayAccess(
ArrayAccessNode n, TransferInput<NullnessValue, NullnessStore> p) {
Expand Down Expand Up @@ -316,8 +401,8 @@ private boolean hasNullableValueType(AnnotatedDeclaredType mapOrSubtype) {
public TransferResult<NullnessValue, NullnessStore> visitReturn(
ReturnNode n, TransferInput<NullnessValue, NullnessStore> in) {
// HACK: make sure we have a value for return statements, because we
// need to record whether (at this return statement) isPolyNullNull is
// set or not.
// need to record (at this return statement) the values of isPolyNullNotNull and
// isPolyNullNull.
NullnessValue value = createDummyValue();
if (in.containsTwoStores()) {
NullnessStore thenStore = in.getThenStore();
Expand Down
Loading

0 comments on commit 1a0712f

Please sign in to comment.