Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Don't write irrelevant annotations in .ajava files #6254

Open
wants to merge 9 commits into
base: master
Choose a base branch
from
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
package org.checkerframework.checker.index.samelen;

import org.checkerframework.common.basetype.BaseTypeChecker;
import org.checkerframework.framework.qual.RelevantJavaTypes;
import org.checkerframework.framework.source.SuppressWarningsPrefix;

/**
Expand All @@ -10,7 +9,9 @@
*
* @checker_framework.manual #index-checker Index Checker
*/
@RelevantJavaTypes({CharSequence.class, Object[].class, Object.class})
// This @RelevantJavaTypes annotation is incorrect, because @SameLen can apply to an arbitrary
// user-defined datatype: https://checkerframework.org/manual/#index-annotating-fixed-size .
// @RelevantJavaTypes({CharSequence.class, Object[].class, Object.class})
@SuppressWarningsPrefix({"index", "samelen"})
public class SameLenChecker extends BaseTypeChecker {
/** Create a new SameLenChecker. */
Expand Down
10 changes: 7 additions & 3 deletions checker/tests/index/SameLenIrrelevant.java
Original file line number Diff line number Diff line change
@@ -1,20 +1,24 @@
// Tests that adding an @SameLen annotation to a primitive type is still
// an error.

// All the errors in this test case are disabled. They were issued when `@SameLen` was restricted
// to arrays and CharSequence, but @SameLen can be written on an arbitrary user-defined type:
// https://checkerframework.org/manual/#index-annotating-fixed-size .

import org.checkerframework.checker.index.qual.SameLen;

public class SameLenIrrelevant {
// :: error: (anno.on.irrelevant)
// NO :: error: (anno.on.irrelevant)
public void test(@SameLen("#2") int x, int y) {
// do nothing
}

// :: error: (anno.on.irrelevant)
// NO :: error: (anno.on.irrelevant)
public void test(@SameLen("#2") double x, double y) {
// do nothing
}

// :: error: (anno.on.irrelevant)
// NO :: error: (anno.on.irrelevant)
public void test(@SameLen("#2") char x, char y) {
// do nothing
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -23,9 +23,15 @@
import com.github.javaparser.ast.expr.NormalAnnotationExpr;
import com.github.javaparser.ast.expr.ObjectCreationExpr;
import com.github.javaparser.ast.expr.SingleMemberAnnotationExpr;
import com.github.javaparser.ast.type.ArrayType;
import com.github.javaparser.ast.type.ClassOrInterfaceType;
import com.github.javaparser.ast.type.IntersectionType;
import com.github.javaparser.ast.type.PrimitiveType;
import com.github.javaparser.ast.type.Type;
import com.github.javaparser.ast.type.TypeParameter;
import com.github.javaparser.ast.type.UnionType;
import com.github.javaparser.ast.type.VarType;
import com.github.javaparser.ast.type.WildcardType;
import com.github.javaparser.ast.visitor.CloneVisitor;
import com.github.javaparser.ast.visitor.VoidVisitor;
import com.github.javaparser.printer.DefaultPrettyPrinter;
Expand Down Expand Up @@ -1062,6 +1068,65 @@ public void writeResultsToFile(OutputFormat outputFormat, BaseTypeChecker checke
modifiedFiles.clear();
}

/**
* Returns true if the annotation is relevant (where it appears in the program). This
* implementation is conservative and only returns false if the qualifier is definitely not
* relevant.
*
* @param anno an annotation
* @return true if the annotation might be relevant
*/
boolean annotationIsRelevant(AnnotationExpr anno) {
GenericAnnotatedTypeFactory<?, ?, ?, ?> gatf = (GenericAnnotatedTypeFactory) atypeFactory;
if (gatf.relevantJavaTypes == null) {
return true;
}

// `aname` is a fully-qualified name.
String aName = anno.getNameAsString();
if (!atypeFactory.isSupportedQualifier(aName)) {
// The annotation might be a declaration qualifier, such as a side effect specification.
return true;
}
Node parentNode = anno.getParentNode().get();

if (parentNode instanceof ArrayType) {
return gatf.arraysAreRelevant();
}
if (parentNode instanceof ClassOrInterfaceType) {
ClassOrInterfaceType classType = (ClassOrInterfaceType) parentNode;
String simpleName = classType.getName().toString();
String scopedName = classType.getNameWithScope();
// TODO: Do I need to remove type parameters?
return gatf.isRelevant(simpleName) || gatf.isRelevant(scopedName);
}
if (parentNode instanceof IntersectionType) {
return true; // TODO
}
if (parentNode instanceof Parameter) {
Parameter param = (Parameter) parentNode;
if (param.isVarArgs()) {
return gatf.arraysAreRelevant();
} else {
throw new Error("Unexpected type annotation on non-varargs Parameter: " + param);
}
}
if (parentNode instanceof PrimitiveType) {
return gatf.isRelevant(parentNode.toString());
}
if (parentNode instanceof UnionType) {
return true; // TODO
}
if (parentNode instanceof VarType) {
return gatf.nonprimitivesAreRelevant();
}
if (parentNode instanceof WildcardType) {
return true; // TODO
}

throw new Error("What parent? " + parentNode.getClass().getSimpleName() + " " + parentNode);
}

/**
* Write an ajava file to disk.
*
Expand All @@ -1077,7 +1142,9 @@ private void writeAjavaFile(File outputPath, CompilationUnitAnnos root) {
// annotations in certain locations.
// LexicalPreservingPrinter.print(root.declaration, writer);

// Do not print invisible qualifiers, to avoid cluttering the output.
// To avoid cluttering the output, do not print:
// * invisible qualifiers
// * irrelevant qualifiers.
Set<String> invisibleQualifierNames = getInvisibleQualifierNames(this.atypeFactory);
DefaultPrettyPrinter prettyPrinter =
new DefaultPrettyPrinter() {
Expand All @@ -1090,6 +1157,9 @@ public void visit(MarkerAnnotationExpr n, Void arg) {
if (invisibleQualifierNames.contains(n.getName().toString())) {
return;
}
if (!annotationIsRelevant(n)) {
return;
}
super.visit(n, arg);
}

Expand All @@ -1098,6 +1168,9 @@ public void visit(SingleMemberAnnotationExpr n, Void arg) {
if (invisibleQualifierNames.contains(n.getName().toString())) {
return;
}
if (!annotationIsRelevant(n)) {
return;
}
super.visit(n, arg);
}

Expand All @@ -1106,6 +1179,9 @@ public void visit(NormalAnnotationExpr n, Void arg) {
if (invisibleQualifierNames.contains(n.getName().toString())) {
return;
}
if (!annotationIsRelevant(n)) {
return;
}
super.visit(n, arg);
}
};
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -187,15 +187,25 @@ public abstract class GenericAnnotatedTypeFactory<
* <p>Although a {@code Class<?>} object exists for every element, this does not contain those
* {@code Class<?>} objects because the elements will be compared to TypeMirrors for which Class
* objects may not exist (they might not be on the classpath).
*
* <p>For their names, see {@link #relevantJavaTypeNames}.
*/
public final @Nullable Set<TypeMirror> relevantJavaTypes;

/**
* Whether users may write type annotations on arrays. Ignored unless {@link #relevantJavaTypes}
* is non-null.
* The fully-qualified names <b>and</b> simple names of the types in {@link #relevantJavaTypes}.
*/
public final @Nullable Set<String> relevantJavaTypeNames;

/** Whether users may write type annotations on arrays. */
protected final boolean arraysAreRelevant;

/**
* Whether users may write type annotations on non-primitives (classes, arrays, etc.). This is
* redundant with the value of {@link #relevantJavaTypes} but is included for efficiency.
*/
protected final boolean nonprimitivesAreRelevant;

// Flow related fields

/** Should flow be used by default? */
Expand Down Expand Up @@ -358,17 +368,23 @@ protected GenericAnnotatedTypeFactory(BaseTypeChecker checker, boolean useFlow)
checker.getClass().getAnnotation(RelevantJavaTypes.class);
if (relevantJavaTypesAnno == null) {
this.relevantJavaTypes = null;
this.relevantJavaTypeNames = null;
this.arraysAreRelevant = true;
this.nonprimitivesAreRelevant = true;
} else {
Types types = getChecker().getTypeUtils();
Elements elements = getElementUtils();
Class<?>[] classes = relevantJavaTypesAnno.value();
Set<TypeMirror> relevantJavaTypesTemp =
new HashSet<>(CollectionsPlume.mapCapacity(classes.length));
Set<String> relevantJavaTypeNamesTemp =
new HashSet<>(CollectionsPlume.mapCapacity(classes.length));
boolean arraysAreRelevantTemp = false;
boolean nonprimitivesAreRelevantTemp = false;
for (Class<?> clazz : classes) {
if (clazz == Object[].class) {
arraysAreRelevantTemp = true;
nonprimitivesAreRelevantTemp = true;
} else if (clazz.isArray()) {
throw new TypeSystemError(
"Don't use arrays other than Object[] in @RelevantJavaTypes on "
Expand All @@ -377,10 +393,24 @@ protected GenericAnnotatedTypeFactory(BaseTypeChecker checker, boolean useFlow)
TypeMirror relevantType = TypesUtils.typeFromClass(clazz, types, elements);
TypeMirror erased = types.erasure(relevantType);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

relevantJavaTypesNames, at least, is only used by WPI (i.e., in this PR). That means that most (all?) of this computation is wasted for non-WPI runs of the checker, which makes me a bit uncomfortable: it does not seem reasonable to slow down the checker in the non-WPI case to speed it up in the WPI case. Can we guard some of this work behind a check that WPI is actually running?

I think this will also complicate the specification of relevantJavaTypeNames, which will need to say something like "always null if WPI is not enabled"

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There are 71 instances of extends BaseTypeChecker in the Checker Framework (excluding checkers used only for testing). Of those:

58 have 0 classes in a @RelevantJavaTypes annotation
5 have 1 class in a @RelevantJavaTypes annotation
2 have 3 classes in a @RelevantJavaTypes annotation
1 has 6 classes in a @RelevantJavaTypes annotation
1 has 8 classes in a @RelevantJavaTypes annotation
4 have 10 classes in a @RelevantJavaTypes annotation

So, I don't think this is a heavy cost, either in time to compute the strings nor in space to store the strings.
But if @smillst agrees with the efficiency concern, I will implement it.

relevantJavaTypesTemp.add(erased);
String typeString = erased.toString();
relevantJavaTypeNamesTemp.add(typeString);
if (clazz.isPrimitive()) {
nonprimitivesAreRelevantTemp = true;
} else {
int dotIndex = typeString.lastIndexOf('.');
if (dotIndex != -1) {
// It's a fully-qualified name. Add the simple name as well.
// TODO: This might not handle a user writing a nested class like "Map.Entry".
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Given the TODO comments here and about handling type variables (at WholeProgramInferenceJavaParserStorage line 1100 or so), I think it's clear we need a test case for this change where an annotation's relevant Java types include at least one class like Map.Entry: it has a type parameter, and it is an inner class (and is usually referenced that way).

Probably the easiest way to test that would be to add another annotation to the AinferTestChecker with the appropriate relevant type, and a corresponding test that ensures it can be inferred in the appropriate place.

relevantJavaTypeNamesTemp.add(typeString.substring(dotIndex + 1));
}
}
}
}
this.relevantJavaTypes = Collections.unmodifiableSet(relevantJavaTypesTemp);
this.relevantJavaTypeNames = Collections.unmodifiableSet(relevantJavaTypeNamesTemp);
this.arraysAreRelevant = arraysAreRelevantTemp;
this.nonprimitivesAreRelevant = nonprimitivesAreRelevantTemp;
}

contractsUtils = createContractsFromMethod();
Expand Down Expand Up @@ -2413,9 +2443,9 @@ public final boolean isRelevant(TypeMirror tm) {
if (tm.getKind() != TypeKind.PACKAGE && tm.getKind() != TypeKind.MODULE) {
tm = types.erasure(tm);
}
Boolean cachedResult = isRelevantCache.get(tm);
if (cachedResult != null) {
return cachedResult;
Boolean resultBoxed = isRelevantCache.get(tm);
if (resultBoxed != null) {
return resultBoxed;
}
boolean result = isRelevantImpl(tm);
isRelevantCache.put(tm, result);
Expand Down Expand Up @@ -2447,6 +2477,9 @@ public final boolean isRelevant(AnnotatedTypeMirror tm) {
* <p>Clients should never call this. Call {@link #isRelevant} instead. This is a helper method
* for {@link #isRelevant}.
*
* <p>This should <b>not</b> be called if {@code relevantJavaTypes == null ||
* relevantJavaTypes.contains(tm))}.
*
* @param tm a type
* @return true if users can write type annotations from this type system on the given Java type
*/
Expand Down Expand Up @@ -2536,6 +2569,43 @@ protected boolean isRelevantImpl(TypeMirror tm) {
}
}

/**
* Returns true if users can write type annotations from this type system directly on the given
* Java type.
*
* <p>For a compound type, returns true only if it is permitted to write a type qualifier on the
* top level of the compound type. That is, this method may return false, when it is possible to
* write type qualifiers on elements of the type.
*
* <p>Subclasses should override {@code #isRelevantImpl} instead of this method.
*
* @param type a fully-qualified or simple type; should not be an array (use {@link
* #arraysAreRelevant} instead)
* @return true if users can write type annotations from this type system directly on the given
* Java type
*/
public final boolean isRelevant(String type) {
return relevantJavaTypeNames == null || relevantJavaTypeNames.contains(type);
}

/**
* Returns true if users can write type annotations from this type system on array types.
*
* @return true if users can write type annotations from this type system on array types
*/
public final boolean arraysAreRelevant() {
return arraysAreRelevant;
}

/**
* Returns true if users can write type annotations from this type system on non-primitive types.
*
* @return true if users can write type annotations from this type system on non-primitive types
*/
public final boolean nonprimitivesAreRelevant() {
return nonprimitivesAreRelevant;
}

/** The cached message about relevant types. */
private @MonotonicNonNull String irrelevantExtraMessage = null;

Expand Down