diff --git a/build.gradle b/build.gradle index 1e430322c0c..3cde7a6a1fe 100644 --- a/build.gradle +++ b/build.gradle @@ -114,7 +114,7 @@ allprojects { currentProj -> // * any new checkers have been added, or // * backward-incompatible changes have been made to APIs or elsewhere. // To make a snapshot release: ./gradlew publish - version '3.44.1-SNAPSHOT' + version '3.44.2-SNAPSHOT' tasks.withType(JavaCompile).configureEach { options.fork = true diff --git a/checker-qual/src/main/java/org/checkerframework/checker/nonempty/qual/EnsuresNonEmpty.java b/checker-qual/src/main/java/org/checkerframework/checker/nonempty/qual/EnsuresNonEmpty.java new file mode 100644 index 00000000000..d997df2fc83 --- /dev/null +++ b/checker-qual/src/main/java/org/checkerframework/checker/nonempty/qual/EnsuresNonEmpty.java @@ -0,0 +1,53 @@ +package org.checkerframework.checker.nonempty.qual; + +import java.lang.annotation.ElementType; +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; +import java.lang.annotation.Target; +import org.checkerframework.framework.qual.InheritedAnnotation; +import org.checkerframework.framework.qual.PostconditionAnnotation; + +/** + * Indicates that a particular expression evaluates to a non-empty value, if the method terminates + * successfully. + * + *

This annotation applies to {@link java.util.Collection}, {@link java.util.Iterator}, {@link + * java.lang.Iterable}, and {@link java.util.Map}, but not {@link java.util.Optional}. + * + *

This postcondition annotation is useful for methods that make a value non-empty by side + * effect: + * + * 


+ *   {@literal @}EnsuresNonEmpty("ids")
+ *   void addId(String id) {
+ *     ids.add(id);
+ *   }
+ *
+ * + * It can also be used for a method that fails if a given value is empty, indicating that the + * argument is non-empty if the method returns normally: + * + * 

+ *   /** Throws an exception if the argument is empty. */
+ *   {@literal @}EnsuresNonEmpty("#1")
+ *   void useTheMap(Map<T, U> arg) { ... }
+ *
+ * + * @see NonEmpty + * @see org.checkerframework.checker.nonempty.NonEmptyChecker + * @checker_framework.manual #non-empty-checker Non-Empty Checker + */ +@Retention(RetentionPolicy.RUNTIME) +@Target({ElementType.METHOD, ElementType.CONSTRUCTOR}) +@PostconditionAnnotation(qualifier = NonEmpty.class) +@InheritedAnnotation +public @interface EnsuresNonEmpty { + /** + * The expression (a collection, iterator, iterable, or map) that is non-empty, if the method + * returns normally. + * + * @return the expression (a collection, iterator, iterable, or map) that is non-empty, if the + * method returns normally + */ + String[] value(); +} diff --git a/checker-qual/src/main/java/org/checkerframework/checker/nonempty/qual/EnsuresNonEmptyIf.java b/checker-qual/src/main/java/org/checkerframework/checker/nonempty/qual/EnsuresNonEmptyIf.java new file mode 100644 index 00000000000..b5af54e90cd --- /dev/null +++ b/checker-qual/src/main/java/org/checkerframework/checker/nonempty/qual/EnsuresNonEmptyIf.java @@ -0,0 +1,87 @@ +package org.checkerframework.checker.nonempty.qual; + +import java.lang.annotation.Documented; +import java.lang.annotation.ElementType; +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; +import java.lang.annotation.Target; +import org.checkerframework.framework.qual.ConditionalPostconditionAnnotation; +import org.checkerframework.framework.qual.InheritedAnnotation; + +/** + * Indicates that the specific expressions are non-empty, if the method returns the given result + * (either true or false). + * + *

Here are ways this conditional postcondition annotation can be used: + * + *

Method parameters: Suppose that a method has a parameter that is a list, and returns + * true if the length of the list is non-zero. You could annotate the method as follows: + * + * 

 @EnsuresNonEmptyIf(result = true, expression = "#1")
+ *  public <T> boolean isLengthGreaterThanZero(List<T> items) { ... }
+ *
+ * + * because, if {@code isLengthGreaterThanZero} returns true, then {@code items} was non-empty. Note + * that you can write more than one {@code @EnsuresNonEmptyIf} annotations on a single method. + * + *

Fields: The value expression can refer to fields, even private ones. For example: + * + * 

 @EnsuresNonEmptyIf(result = true, expression = "this.orders")
+ *  public <T> boolean areOrdersActive() {
+ *    return this.orders != null && this.orders.size() > 0;
+ * }
+ * + * An {@code @EnsuresNonEmptyIf} annotation that refers to a private field is useful for verifying + * that a method establishes a property, even though client code cannot directly affect the field. + * + *

Method postconditions: Suppose that if a method {@code areOrdersActive()} returns true, + * then {@code getOrders()} will return a non-empty Map. You can express this relationship as: + * + * 

 @EnsuresNonEmptyIf(result = true, expression = "this.getOrders()")
+ *  public <T> boolean areOrdersActive() {
+ *    return this.orders != null && this.orders.size() > 0;
+ * }
+ * + * @see NonEmpty + * @see EnsuresNonEmpty + * @checker_framework.manual #non-empty-checker Non-Empty Checker + */ +@Documented +@Retention(RetentionPolicy.RUNTIME) +@Target({ElementType.METHOD, ElementType.CONSTRUCTOR}) +@ConditionalPostconditionAnnotation(qualifier = NonEmpty.class) +@InheritedAnnotation +public @interface EnsuresNonEmptyIf { + + /** + * A return value of the method; when the method returns that value, the postcondition holds. + * + * @return the return value of the method for which the postcondition holds + */ + boolean result(); + + /** + * Returns the Java expressions that are non-empty after the method returns the given result. + * + * @return the Java expressions that are non-empty after the method returns the given result + */ + String[] expression(); + + /** + * A wrapper annotation that makes the {@link EnsuresNonEmptyIf} annotation repeatable. + * + *

Programmers generally do not need to write ths. It is created by Java when a programmer + * writes more than one {@link EnsuresNonEmptyIf} annotation at the same location. + */ + @Retention(RetentionPolicy.RUNTIME) + @Target({ElementType.METHOD, ElementType.CONSTRUCTOR}) + @ConditionalPostconditionAnnotation(qualifier = NonEmpty.class) + @interface List { + /** + * Returns the repeatable annotations. + * + * @return the repeatable annotations + */ + EnsuresNonEmptyIf[] value(); + } +} diff --git a/checker-qual/src/main/java/org/checkerframework/checker/nonempty/qual/NonEmpty.java b/checker-qual/src/main/java/org/checkerframework/checker/nonempty/qual/NonEmpty.java new file mode 100644 index 00000000000..d5a7f8c15d5 --- /dev/null +++ b/checker-qual/src/main/java/org/checkerframework/checker/nonempty/qual/NonEmpty.java @@ -0,0 +1,20 @@ +package org.checkerframework.checker.nonempty.qual; + +import java.lang.annotation.Documented; +import java.lang.annotation.ElementType; +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; +import java.lang.annotation.Target; +import org.checkerframework.framework.qual.SubtypeOf; + +/** + * The {@link java.util.Collection Collection}, {@link java.util.Iterator Iterator}, {@link + * java.lang.Iterable Iterable}, or {@link java.util.Map Map} is definitely non-empty. + * + * @checker_framework.manual #non-empty-checker Non-Empty Checker + */ +@Documented +@Retention(RetentionPolicy.RUNTIME) +@Target({ElementType.TYPE_PARAMETER, ElementType.TYPE_USE}) +@SubtypeOf(UnknownNonEmpty.class) +public @interface NonEmpty {} diff --git a/checker-qual/src/main/java/org/checkerframework/checker/nonempty/qual/PolyNonEmpty.java b/checker-qual/src/main/java/org/checkerframework/checker/nonempty/qual/PolyNonEmpty.java new file mode 100644 index 00000000000..dd538314595 --- /dev/null +++ b/checker-qual/src/main/java/org/checkerframework/checker/nonempty/qual/PolyNonEmpty.java @@ -0,0 +1,20 @@ +package org.checkerframework.checker.nonempty.qual; + +import java.lang.annotation.Documented; +import java.lang.annotation.ElementType; +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; +import java.lang.annotation.Target; +import org.checkerframework.framework.qual.PolymorphicQualifier; + +/** + * A polymorphic qualifier for the Non-Empty type system. + * + * @checker_framework.manual #non-empty-checker Non-Empty Checker + * @checker_framework.manual #qualifier-polymorphism Qualifier polymorphism + */ +@Documented +@Retention(RetentionPolicy.RUNTIME) +@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) +@PolymorphicQualifier(UnknownNonEmpty.class) +public @interface PolyNonEmpty {} diff --git a/checker-qual/src/main/java/org/checkerframework/checker/nonempty/qual/RequiresNonEmpty.java b/checker-qual/src/main/java/org/checkerframework/checker/nonempty/qual/RequiresNonEmpty.java new file mode 100644 index 00000000000..45b46d4233d --- /dev/null +++ b/checker-qual/src/main/java/org/checkerframework/checker/nonempty/qual/RequiresNonEmpty.java @@ -0,0 +1,96 @@ +package org.checkerframework.checker.nonempty.qual; + +import java.lang.annotation.Documented; +import java.lang.annotation.ElementType; +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; +import java.lang.annotation.Target; +import org.checkerframework.framework.qual.PreconditionAnnotation; + +/** + * Indicates a method precondition: the specified expressions that may be a {@link + * java.util.Collection collection}, {@link java.util.Iterator iterator}, {@link java.lang.Iterable + * iterable}, or {@link java.util.Map map} must be non-empty when the annotated method is invoked. + * + *

For example: + * + * 

+ * import java.util.LinkedList;
+ * import java.util.List;
+ * import org.checkerframework.checker.nonempty.qual.NonEmpty;
+ * import org.checkerframework.checker.nonempty.qual.RequiresNonEmpty;
+ * import org.checkerframework.dataflow.qual.Pure;
+ *
+ * class MyClass {
+ *
+ *   List<String> list1 = new LinkedList<>();
+ *   List<String> list2;
+ *
+ *   @RequiresNonEmpty("list1")
+ *   @Pure
+ *   void m1() {}
+ *
+ *   @RequiresNonEmpty({"list1", "list2"})
+ *   @Pure
+ *   void m2() {}
+ *
+ *   @RequiresNonEmpty({"list1", "list2"})
+ *   void m3() {}
+ *
+ *   void m4() {}
+ *
+ *   void test(@NonEmpty List<String> l1, @NonEmpty List<String> l2) {
+ *     MyClass testClass = new MyClass();
+ *
+ *     testClass.m1(); // Compile-time error: m1 requires that list1 is @NonEmpty.
+ *
+ *     testClass.list1 = l1;
+ *     testClass.m1(); // OK
+ *
+ *     testClass.m2(); // Compile-time error: m2 requires that list2 is @NonEmpty
+ *
+ *     testClass.list2 = l2;
+ *     testClass.m2(); // OK
+ *
+ *     testClass.m4();
+ *
+ *     testClass.m2(); // Compile-time error: m4 is not pure and might have assigned a field.
+ *   }
+ * }
+ *
+ * + * This annotation should not be used for formal parameters (instead, give them a {@code @NonEmpty} + * type). The {@code @RequiresNonEmpty} annotation is intended for non-parameter expressions, such + * as field accesses or method calls. + * + * @checker_framework.manual #non-empty-checker Non-Empty Checker + */ +@Documented +@Retention(RetentionPolicy.RUNTIME) +@Target({ElementType.METHOD, ElementType.PARAMETER}) +@PreconditionAnnotation(qualifier = NonEmpty.class) +public @interface RequiresNonEmpty { + + /** + * The Java {@link java.util.Collection collection}, {@link java.util.Iterator iterator}, {@link + * java.lang.Iterable iterable}, or {@link java.util.Map map} that must be non-empty. + * + * @return the Java expression that must be non-empty + */ + String[] value(); + + /** + * A wrapper annotation that makes the {@link RequiresNonEmpty} annotation repeatable. + * + *

Programmers generally do not need to write this. It is created by Java when a programmer + * writes more than one {@link RequiresNonEmpty} annotation at the same location. + */ + @interface List { + /** + * Returns the repeatable annotations. + * + * @return the repeatable annotations + */ + RequiresNonEmpty[] value(); + } +} diff --git a/checker-qual/src/main/java/org/checkerframework/checker/nonempty/qual/UnknownNonEmpty.java b/checker-qual/src/main/java/org/checkerframework/checker/nonempty/qual/UnknownNonEmpty.java new file mode 100644 index 00000000000..65900f7fa12 --- /dev/null +++ b/checker-qual/src/main/java/org/checkerframework/checker/nonempty/qual/UnknownNonEmpty.java @@ -0,0 +1,22 @@ +package org.checkerframework.checker.nonempty.qual; + +import java.lang.annotation.Documented; +import java.lang.annotation.ElementType; +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; +import java.lang.annotation.Target; +import org.checkerframework.framework.qual.DefaultQualifierInHierarchy; +import org.checkerframework.framework.qual.SubtypeOf; + +/** + * The {@link java.util.Collection Collection}, {@link java.util.Iterator Iterator}, {@link + * java.lang.Iterable Iterable}, or {@link java.util.Map Map} may or may not be empty. + * + * @checker_framework.manual #non-empty-checker Non-Empty Checker + */ +@Documented +@Retention(RetentionPolicy.RUNTIME) +@Target({ElementType.TYPE_PARAMETER, ElementType.TYPE_USE}) +@DefaultQualifierInHierarchy +@SubtypeOf({}) +public @interface UnknownNonEmpty {} diff --git a/checker/bin/wpi-many.sh b/checker/bin/wpi-many.sh index 1010a156a51..3c0644f57e0 100755 --- a/checker/bin/wpi-many.sh +++ b/checker/bin/wpi-many.sh @@ -159,7 +159,7 @@ if [ "${has_java8}" = "no" ] && [ "${has_java11}" = "no" ] && [ "${has_java17}" fi if [ "${CHECKERFRAMEWORK}" = "" ]; then - echo "CHECKERFRAMEWORK is not set; it must be set to a locally-built Checker Framework. Please clone and build github.com/typetools/checker-framework" + echo "CHECKERFRAMEWORK is not set; it must be set to a locally-built Checker Framework. Please clone and build https://github.com/typetools/checker-framework" exit 2 fi diff --git a/checker/src/main/java/org/checkerframework/checker/interning/InterningAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/interning/InterningAnnotatedTypeFactory.java index 0a8bacac849..d1b19c4d02a 100644 --- a/checker/src/main/java/org/checkerframework/checker/interning/InterningAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/interning/InterningAnnotatedTypeFactory.java @@ -78,7 +78,7 @@ public class InterningAnnotatedTypeFactory extends BaseAnnotatedTypeFactory { final AnnotationMirrorSet INTERNED_SET = AnnotationMirrorSet.singleton(INTERNED); /** - * Creates a new {@link InterningAnnotatedTypeFactory} that operates on a particular AST. + * Creates a new {@link InterningAnnotatedTypeFactory}. * * @param checker the checker to use */ diff --git a/checker/src/main/java/org/checkerframework/checker/nonempty/NonEmptyAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/nonempty/NonEmptyAnnotatedTypeFactory.java new file mode 100644 index 00000000000..9cedb36f489 --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/nonempty/NonEmptyAnnotatedTypeFactory.java @@ -0,0 +1,61 @@ +package org.checkerframework.checker.nonempty; + +import com.sun.source.tree.ExpressionTree; +import com.sun.source.tree.NewArrayTree; +import java.util.List; +import javax.lang.model.element.AnnotationMirror; +import org.checkerframework.checker.nonempty.qual.NonEmpty; +import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory; +import org.checkerframework.common.basetype.BaseTypeChecker; +import org.checkerframework.framework.type.AnnotatedTypeFactory; +import org.checkerframework.framework.type.AnnotatedTypeMirror; +import org.checkerframework.framework.type.treeannotator.ListTreeAnnotator; +import org.checkerframework.framework.type.treeannotator.TreeAnnotator; +import org.checkerframework.javacutil.AnnotationBuilder; + +/** The type factory for the {@link NonEmptyChecker}. */ +public class NonEmptyAnnotatedTypeFactory extends BaseAnnotatedTypeFactory { + + /** The @{@link NonEmpty} annotation. */ + public final AnnotationMirror NON_EMPTY = AnnotationBuilder.fromClass(elements, NonEmpty.class); + + /** + * Creates a new {@link NonEmptyAnnotatedTypeFactory} that operates on a particular AST. + * + * @param checker the checker to use + */ + public NonEmptyAnnotatedTypeFactory(BaseTypeChecker checker) { + super(checker); + this.sideEffectsUnrefineAliases = true; + this.postInit(); + } + + @Override + protected TreeAnnotator createTreeAnnotator() { + return new ListTreeAnnotator(super.createTreeAnnotator(), new NonEmptyTreeAnnotator(this)); + } + + /** The tree annotator for the Non-Empty Checker. */ + private class NonEmptyTreeAnnotator extends TreeAnnotator { + + /** + * Creates a new {@link NonEmptyTreeAnnotator}. + * + * @param aTypeFactory the type factory for this tree annotator + */ + public NonEmptyTreeAnnotator(AnnotatedTypeFactory aTypeFactory) { + super(aTypeFactory); + } + + @Override + public Void visitNewArray(NewArrayTree tree, AnnotatedTypeMirror type) { + if (!type.hasEffectiveAnnotation(NON_EMPTY)) { + List initializers = tree.getInitializers(); + if (initializers != null && !initializers.isEmpty()) { + type.replaceAnnotation(NON_EMPTY); + } + } + return super.visitNewArray(tree, type); + } + } +} diff --git a/checker/src/main/java/org/checkerframework/checker/nonempty/NonEmptyChecker.java b/checker/src/main/java/org/checkerframework/checker/nonempty/NonEmptyChecker.java new file mode 100644 index 00000000000..380d27ef8e8 --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/nonempty/NonEmptyChecker.java @@ -0,0 +1,17 @@ +package org.checkerframework.checker.nonempty; + +import org.checkerframework.common.basetype.BaseTypeChecker; + +/** + * A type-checker that prevents {@link java.util.NoSuchElementException} in the use of container + * classes. + * + * @checker_framework.manual #non-empty-checker Non-Empty Checker + */ +public class NonEmptyChecker extends BaseTypeChecker { + + /** Creates a NonEmptyChecker. */ + public NonEmptyChecker() { + super(); + } +} diff --git a/checker/src/main/java/org/checkerframework/checker/nonempty/NonEmptyTransfer.java b/checker/src/main/java/org/checkerframework/checker/nonempty/NonEmptyTransfer.java new file mode 100644 index 00000000000..4726f7ac185 --- /dev/null +++ b/checker/src/main/java/org/checkerframework/checker/nonempty/NonEmptyTransfer.java @@ -0,0 +1,369 @@ +package org.checkerframework.checker.nonempty; + +import java.util.List; +import javax.annotation.processing.ProcessingEnvironment; +import javax.lang.model.element.ExecutableElement; +import org.checkerframework.checker.nonempty.qual.NonEmpty; +import org.checkerframework.dataflow.analysis.TransferInput; +import org.checkerframework.dataflow.analysis.TransferResult; +import org.checkerframework.dataflow.cfg.node.CaseNode; +import org.checkerframework.dataflow.cfg.node.EqualToNode; +import org.checkerframework.dataflow.cfg.node.GreaterThanNode; +import org.checkerframework.dataflow.cfg.node.GreaterThanOrEqualNode; +import org.checkerframework.dataflow.cfg.node.IntegerLiteralNode; +import org.checkerframework.dataflow.cfg.node.LessThanNode; +import org.checkerframework.dataflow.cfg.node.LessThanOrEqualNode; +import org.checkerframework.dataflow.cfg.node.MethodAccessNode; +import org.checkerframework.dataflow.cfg.node.MethodInvocationNode; +import org.checkerframework.dataflow.cfg.node.Node; +import org.checkerframework.dataflow.cfg.node.NotEqualNode; +import org.checkerframework.dataflow.expression.JavaExpression; +import org.checkerframework.dataflow.util.NodeUtils; +import org.checkerframework.framework.flow.CFAnalysis; +import org.checkerframework.framework.flow.CFStore; +import org.checkerframework.framework.flow.CFTransfer; +import org.checkerframework.framework.flow.CFValue; +import org.checkerframework.javacutil.AnnotationUtils; +import org.checkerframework.javacutil.TreeUtils; + +/** + * This class implements type rules that cannot be expressed via pre- or post-condition annotations. + */ +public class NonEmptyTransfer extends CFTransfer { + + /** A {@link ProcessingEnvironment} instance. */ + private final ProcessingEnvironment env; + + /** A {@link NonEmptyAnnotatedTypeFactory} instance. */ + protected final NonEmptyAnnotatedTypeFactory aTypeFactory; + + /** The {@link java.util.Collection#size()} method. */ + private final ExecutableElement collectionSize; + + /** The {@link java.util.Map#size()} method. */ + private final ExecutableElement mapSize; + + /** The {@link java.util.List#indexOf(Object)} method. */ + private final ExecutableElement listIndexOf; + + /** + * Create a new {@link NonEmptyTransfer}. + * + * @param analysis the analysis for this transfer function + */ + public NonEmptyTransfer(CFAnalysis analysis) { + super(analysis); + + this.env = analysis.getTypeFactory().getProcessingEnv(); + this.aTypeFactory = (NonEmptyAnnotatedTypeFactory) analysis.getTypeFactory(); + + this.collectionSize = TreeUtils.getMethod("java.util.Collection", "size", 0, this.env); + this.mapSize = TreeUtils.getMethod("java.util.Map", "size", 0, this.env); + this.listIndexOf = TreeUtils.getMethod("java.util.List", "indexOf", 1, this.env); + } + + @Override + public TransferResult visitEqualTo( + EqualToNode n, TransferInput in) { + TransferResult result = super.visitEqualTo(n, in); + + // The equality holds. + strengthenAnnotationSizeEquals( + in, n.getLeftOperand(), n.getRightOperand(), result.getThenStore()); + refineGTE(n.getLeftOperand(), n.getRightOperand(), result.getThenStore()); + refineGTE(n.getRightOperand(), n.getLeftOperand(), result.getThenStore()); + + // The equality does not hold. + refineNotEqual(n.getLeftOperand(), n.getRightOperand(), result.getElseStore()); + refineNotEqual(n.getRightOperand(), n.getLeftOperand(), result.getElseStore()); + + return result; + } + + @Override + public TransferResult visitNotEqual( + NotEqualNode n, TransferInput in) { + TransferResult result = super.visitNotEqual(n, in); + + refineNotEqual(n.getLeftOperand(), n.getRightOperand(), result.getThenStore()); + refineNotEqual(n.getRightOperand(), n.getLeftOperand(), result.getThenStore()); + + strengthenAnnotationSizeEquals( + in, n.getLeftOperand(), n.getRightOperand(), result.getElseStore()); + + return result; + } + + @Override + public TransferResult visitLessThan( + LessThanNode n, TransferInput in) { + TransferResult result = super.visitLessThan(n, in); + + // A < B is equivalent to B > A. + refineGT(n.getRightOperand(), n.getLeftOperand(), result.getThenStore()); + + // This handles the case where n < container.size(). + refineGTE(n.getLeftOperand(), n.getRightOperand(), result.getElseStore()); + + return result; + } + + @Override + public TransferResult visitLessThanOrEqual( + LessThanOrEqualNode n, TransferInput in) { + TransferResult result = super.visitLessThanOrEqual(n, in); + + // A <= B is equivalent to B >= A. + // This handles the case where n <= container.size() + refineGTE(n.getRightOperand(), n.getLeftOperand(), result.getThenStore()); + + refineGT(n.getLeftOperand(), n.getRightOperand(), result.getElseStore()); + + return result; + } + + @Override + public TransferResult visitGreaterThan( + GreaterThanNode n, TransferInput in) { + TransferResult result = super.visitGreaterThan(n, in); + + refineGT(n.getLeftOperand(), n.getRightOperand(), result.getThenStore()); + + return result; + } + + @Override + public TransferResult visitGreaterThanOrEqual( + GreaterThanOrEqualNode n, TransferInput in) { + TransferResult result = super.visitGreaterThanOrEqual(n, in); + + refineGTE(n.getLeftOperand(), n.getRightOperand(), result.getThenStore()); + + return result; + } + + @Override + public TransferResult visitCase( + CaseNode n, TransferInput in) { + TransferResult result = super.visitCase(n, in); + List caseOperands = n.getCaseOperands(); + Node switchOpNode = n.getSwitchOperand().getExpression(); + + refineSwitchStatement(switchOpNode, caseOperands, result.getThenStore(), result.getElseStore()); + + return result; + } + + /** + * Refine the transfer result's store, given the left- and right-hand side of an equality check + * comparing container sizes. + * + * @param in transfer input used to get the types of subnodes of {@code lhs} and {@code rhs}. + * @param lhs a node that may be a method invocation of {@link java.util.Collection size()} or + * {@link java.util.Map size()} + * @param rhs a node that may be a method invocation of {@link java.util.Collection size()} or + * {@link java.util.Map size()} + * @param store the "then" store of the comparison operation + */ + private void strengthenAnnotationSizeEquals( + TransferInput in, Node lhs, Node rhs, CFStore store) { + if (!isSizeAccess(lhs) || !isSizeAccess(rhs)) { + return; + } + + if (isAccessOfNonEmptyCollection(in, (MethodInvocationNode) lhs)) { + store.insertValue(getReceiverJE(rhs), aTypeFactory.NON_EMPTY); + } else if (isAccessOfNonEmptyCollection(in, (MethodInvocationNode) rhs)) { + store.insertValue(getReceiverJE(lhs), aTypeFactory.NON_EMPTY); + } + } + + /** + * Returns true if the receiver of {@code methodAccessNode} is non-empty according to {@code in}. + * + * @param in used to get the type of {@code methodAccessNode}. + * @param methodAccessNode method access + * @return true if the receiver of {@code methodAccessNode} is non-empty according to {@code in}. + */ + private boolean isAccessOfNonEmptyCollection( + TransferInput in, MethodInvocationNode methodAccessNode) { + Node receiver = methodAccessNode.getTarget().getReceiver(); + + return AnnotationUtils.containsSameByClass( + in.getValueOfSubNode(receiver).getAnnotations(), NonEmpty.class); + } + + /** + * Updates the transfer result's store with information from the Non-Empty type system for + * expressions of the form {@code container.size() != n}, {@code n != container.size()}, or {@code + * container.indexOf(Object) != n}. + * + *

This method is always called twice, with the arguments reversed. So, it can do non-symmetric + * checks. + * + *

For example, the type of {@code container} in the "then" branch of a conditional statement + * with the test {@code container.size() != n} where {@code n} is 0 should refine to + * {@code @NonEmpty}. + * + *

This method is also used to refine the "else" store of an equality comparison where {@code + * container.size()} is compared against 0. + * + * @param left the left operand of a binary operation + * @param right the right operand of a binary operation + * @param store the abstract store to update + */ + private void refineNotEqual(Node left, Node right, CFStore store) { + if (!(right instanceof IntegerLiteralNode)) { + return; + } + Integer emptyValue = emptyValue(left); + if (emptyValue == null) { + return; + } + // In case of a size() comparison, refine the store if the value is 0 + // In case of a indexOf(Object) check, refine the store if the value is -1 + IntegerLiteralNode integerLiteralNode = (IntegerLiteralNode) right; + if (integerLiteralNode.getValue() == (int) emptyValue) { + store.insertValue(getReceiverJE(left), aTypeFactory.NON_EMPTY); + } + } + + /** + * Updates the transfer result's store with information from the Non-Empty type system for + * expressions of the form {@code container.size() > n} or {@code container.indexOf(Object) > n}. + * + *

When this method is called, {@link refineGTE} is also called, with the arguments reversed. + * So, this method can do non-symmetric checks. + * + *

For example, the type of {@code container} in the "then" branch of a conditional statement + * with the test {@code container.size() > n} where {@code n >= 0} should be refined to + * {@code @NonEmpty}. + * + * @param left the left operand of a binary operation + * @param right the right operand of a binary operation + * @param store the abstract store to update + */ + private void refineGT(Node left, Node right, CFStore store) { + if (!(right instanceof IntegerLiteralNode)) { + return; + } + Integer emptyValue = emptyValue(left); + if (emptyValue == null) { + return; + } + // In case of a size() comparison, refine the store if the value is 0 + // In case of a indexOf(Object) check, refine the store if the value is -1 + IntegerLiteralNode integerLiteralNode = (IntegerLiteralNode) right; + if (integerLiteralNode.getValue() >= (int) emptyValue) { + store.insertValue(getReceiverJE(left), aTypeFactory.NON_EMPTY); + } + } + + /** + * Updates the transfer result's store with information from the Non-Empty type system for + * expressions of the form {@code container.size() >= n} or {@code container.indexOf(Object) >= + * n}. + * + *

When this method is called, {@link refineGTE} is also called, with the arguments reversed. + * So, this method can do non-symmetric checks. + * + *

For example, the type of {@code container} in the "then" branch of a conditional statement + * with the test {@code container.size() >= n} where {@code n > 0} should be refined to + * {@code @NonEmpty}. + * + *

This method is also used to refine the "then" branch of an equality comparison where {@code + * container.size()} is compared against a non-zero value. + * + * @param left the left operand of a binary operation + * @param right the right operand of a binary operation + * @param store the abstract store to update + */ + private void refineGTE(Node left, Node right, CFStore store) { + if (!(right instanceof IntegerLiteralNode)) { + return; + } + Integer emptyValue = emptyValue(left); + if (emptyValue == null) { + return; + } + // In case of a size() comparison, refine the store if the value is 0 + // In case of a indexOf(Object) check, refine the store if the value is -1 + IntegerLiteralNode integerLiteralNode = (IntegerLiteralNode) right; + if (integerLiteralNode.getValue() > (int) emptyValue) { + store.insertValue(getReceiverJE(left), aTypeFactory.NON_EMPTY); + } + } + + /** + * Updates the transfer result's store with information from the Non-Empty type system for switch + * statements, where the test expression is of the form {@code container.size()} or {@code + * container.indexOf(Object)}. + * + *

For example, the "then" store of any case node with an integer value greater than 0 (or -1, + * in the case of the test expression being a call to {@code container.indexOf(Object)}) should + * refine the type of {@code container} to {@code @NonEmpty}. + * + * @param testNode a node that is the test expression for a {@code switch} statement + * @param caseOperands the operands within each case label + * @param thenStore the "then" store + * @param elseStore the "else" store, corresponding to the "default" case label + */ + private void refineSwitchStatement( + Node testNode, List caseOperands, CFStore thenStore, CFStore elseStore) { + Integer emptyValue = emptyValue(testNode); + if (emptyValue == null) { + return; + } + for (Node caseOperand : caseOperands) { + if (!(caseOperand instanceof IntegerLiteralNode)) { + continue; + } + IntegerLiteralNode caseIntegerLiteral = (IntegerLiteralNode) caseOperand; + JavaExpression receiver = getReceiverJE(testNode); + CFStore storeToUpdate = + caseIntegerLiteral.getValue() > (int) emptyValue ? thenStore : elseStore; + storeToUpdate.insertValue(receiver, aTypeFactory.NON_EMPTY); + } + } + + /** + * Return true if the given node is an invocation of {@link java.util.Collection#size()} or {@link + * java.util.Map#size()}. + * + * @param possibleSizeAccess a node that may be a method call to the {@code size()} method in the + * {@link java.util.Collection} or {@link java.util.Map} types + * @return true if the node is a method call to size() + */ + private boolean isSizeAccess(Node possibleSizeAccess) { + return NodeUtils.isMethodInvocation(possibleSizeAccess, collectionSize, env) + || NodeUtils.isMethodInvocation(possibleSizeAccess, mapSize, env); + } + + /** + * Return the receiver as a {@link JavaExpression} given a method invocation node. + * + * @param node a method invocation + * @return the receiver as a {@link JavaExpression} + */ + private JavaExpression getReceiverJE(Node node) { + MethodAccessNode methodAccessNode = ((MethodInvocationNode) node).getTarget(); + return JavaExpression.fromNode(methodAccessNode.getReceiver()); + } + + /** + * If this is an invocation of a size-dependent method, return the value that the method returns + * ffor an empty container. + * + * @param n a node that might be an invocation of a size-dependent method + * @return the value that the method returns ffor an empty container, or null + */ + private Integer emptyValue(Node n) { + if (isSizeAccess(n)) { + return 0; + } else if (NodeUtils.isMethodInvocation(n, listIndexOf, env)) { + return -1; + } else { + return null; + } + } +} diff --git a/checker/src/test/java/org/checkerframework/checker/test/junit/NonEmptyTest.java b/checker/src/test/java/org/checkerframework/checker/test/junit/NonEmptyTest.java new file mode 100644 index 00000000000..611cbfea5e3 --- /dev/null +++ b/checker/src/test/java/org/checkerframework/checker/test/junit/NonEmptyTest.java @@ -0,0 +1,24 @@ +package org.checkerframework.checker.test.junit; + +import java.io.File; +import java.util.List; +import org.checkerframework.framework.test.CheckerFrameworkPerDirectoryTest; +import org.junit.runners.Parameterized.Parameters; + +/** JUnit tests for the Non-Empty Checker */ +public class NonEmptyTest extends CheckerFrameworkPerDirectoryTest { + + /** + * Create a NonEmptyTest. + * + * @param testFiles the files containing test code to be type-checked + */ + public NonEmptyTest(List testFiles) { + super(testFiles, org.checkerframework.checker.nonempty.NonEmptyChecker.class, "nonempty"); + } + + @Parameters + public static String[] getTestDirs() { + return new String[] {"nonempty", "all-systems"}; + } +} diff --git a/checker/tests/nonempty/Comparisons.java b/checker/tests/nonempty/Comparisons.java new file mode 100644 index 00000000000..20a2dd27e58 --- /dev/null +++ b/checker/tests/nonempty/Comparisons.java @@ -0,0 +1,238 @@ +import java.util.Arrays; +import java.util.List; +import org.checkerframework.checker.nonempty.qual.NonEmpty; + +class Comparisons { + + /**** Tests for EQ ****/ + void testEqZeroWithReturn(List strs) { + if (strs.size() == 0) { + // :: error: (method.invocation) + strs.iterator().next(); + return; + } + strs.iterator().next(); // OK + } + + void testEqZeroFallthrough(List strs) { + if (strs.size() == 0) { + // :: error: (method.invocation) + strs.iterator().next(); + } + // :: error: (method.invocation) + strs.iterator().next(); + } + + void testEqNonZero(List strs) { + if (1 == strs.size()) { + strs.iterator().next(); + } else { + // :: error: (method.invocation) + strs.iterator().next(); + } + } + + void testImplicitNonZero(List strs1, List strs2) { + if (strs1.isEmpty()) { + return; + } + if (strs1.size() == strs2.size()) { + @NonEmpty List strs3 = strs2; // OK + } + // :: error: (assignment) + @NonEmpty List strs4 = strs2; + } + + void testImplicitNonZero2(List strs2) { + if (getNonEmptyList().size() == strs2.size()) { + @NonEmpty List strs3 = strs2; // OK + } + } + + @NonEmpty + List getNonEmptyList() { + return Arrays.asList(new String[] {""}); + } + + void testEqualIndexOfRefinement(List objs, Object obj) { + if (objs.indexOf(obj) == -1) { + // :: error: (assignment) + @NonEmpty List objs2 = objs; + } else { + objs.iterator().next(); + } + } + + /**** Tests for NE ****/ + void t0(List strs) { + if (strs.size() != 0) { + strs.iterator().next(); + } + if (0 != strs.size()) { + strs.iterator().next(); + } + if (1 != strs.size()) { + // :: error: (method.invocation) + strs.iterator().next(); + } + } + + void testNotEqualsRefineElse(List strs1, List strs2) { + if (strs1.size() <= 0) { + return; + } + if (strs1.size() != strs2.size()) { + // :: error: (assignment) + @NonEmpty List strs3 = strs2; + } else { + @NonEmpty List strs4 = strs1; + @NonEmpty List strs5 = strs2; + } + } + + void testNotEqualsRefineIndexOf(List objs, Object obj) { + if (objs.indexOf(obj) != -1) { + @NonEmpty List objs2 = objs; + } else { + // :: error: (method.invocation) + objs.iterator().next(); + } + if (-1 != objs.indexOf(obj)) { + @NonEmpty List objs2 = objs; + } else { + // :: error: (method.invocation) + objs.iterator().next(); + } + } + + /**** Tests for GT ****/ + void t1(List strs) { + if (strs.size() > 10) { + strs.iterator().next(); + } else if (0 > strs.size()) { + // :: error: (method.invocation) + strs.iterator().next(); + } else if (100 > strs.size()) { + // :: error: (method.invocation) + strs.iterator().next(); + } + if (strs.size() > 0) { + strs.iterator().next(); + } else { + // :: error: (method.invocation) + strs.iterator().next(); + } + + if (0 > strs.size()) { + // :: error: (method.invocation) + strs.iterator().next(); + } else { + // :: error: (method.invocation) + strs.iterator().next(); + } + } + + void t2(List strs) { + if (strs.size() > -1) { + // :: error: (method.invocation) + strs.iterator().next(); + } + } + + void testRefineIndexOfGT(List objs, Object obj) { + if (objs.indexOf(obj) > -1) { + @NonEmpty List objs2 = objs; + } else { + // :: error: (method.invocation) + objs.iterator().next(); + } + } + + /**** Tests for GTE ****/ + void t3(List strs) { + if (strs.size() >= 0) { + // :: error: (method.invocation) + strs.iterator().next(); + } else if (strs.size() >= 1) { + strs.iterator().next(); + } + } + + void t4(List strs) { + if (0 >= strs.size()) { + // :: error: (method.invocation) + strs.iterator().next(); + } + } + + void testRefineGTEIndexOf(List strs, String s) { + if (strs.indexOf(s) >= 0) { + strs.iterator().next(); + } else { + // :: error: (assignment) + @NonEmpty List strs2 = strs; + } + } + + /**** Tests for LT ****/ + void t5(List strs) { + if (strs.size() < 10) { + // :: error: (method.invocation) + strs.iterator().next(); + } + if (strs.size() < 1) { + // :: error: (method.invocation) + strs.iterator().next(); + } else { + strs.iterator().next(); // OK + } + } + + void t6(List strs) { + if (0 < strs.size()) { + strs.iterator().next(); // Equiv. to strs.size() > 0 + } else { + // :: error: (method.invocation) + strs.iterator().next(); // Equiv. to strs.size() <= 0 + } + + if (strs.size() < 10) { + // Doesn't tell us a useful fact + // :: error: (method.invocation) + strs.iterator().next(); + } else { + strs.iterator().next(); + } + } + + /**** Tests for LTE ****/ + void t7(List strs) { + if (strs.size() <= 2) { + // :: error: (method.invocation) + strs.iterator().next(); + } + if (strs.size() <= 0) { + // :: error: (method.invocation) + strs.iterator().next(); + } else { + strs.iterator().next(); // OK, since strs must be non-empty + } + } + + void t8(List strs) { + if (1 <= strs.size()) { + strs.iterator().next(); + } else { + // :: error: (method.invocation) + strs.iterator().next(); + } + + if (0 <= strs.size()) { + // :: error: (method.invocation) + strs.iterator().next(); + } else { + // :: error: (method.invocation) + strs.iterator().next(); + } + } +} diff --git a/checker/tests/nonempty/EnsuresNonEmptyIfTest.java b/checker/tests/nonempty/EnsuresNonEmptyIfTest.java new file mode 100644 index 00000000000..f1669b8b90e --- /dev/null +++ b/checker/tests/nonempty/EnsuresNonEmptyIfTest.java @@ -0,0 +1,33 @@ +import java.util.ArrayList; +import org.checkerframework.checker.nonempty.qual.EnsuresNonEmptyIf; +import org.checkerframework.checker.nonempty.qual.NonEmpty; + +class EnsuresNonEmptyIfTest { + + @EnsuresNonEmptyIf(result = true, expression = "#1") + boolean m1(ArrayList l1) { + try { + l1.add("foo"); + return true; + } catch (Exception e) { + // As per the JDK documentation for Collections, an exception is thrown when adding to a + // collection fails + return false; + } + } + + void m2(@NonEmpty ArrayList l1) {} + + void test(ArrayList l1) { + // m2 requires a @NonEmpty collection, l1 has type @UnknownNonEmpty + // :: error: (argument) + m2(l1); + + if (!m1(l1)) { + // :: error: (argument) + m2(l1); + } else { + m2(l1); // OK + } + } +} diff --git a/checker/tests/nonempty/EnsuresNonEmptyTest.java b/checker/tests/nonempty/EnsuresNonEmptyTest.java new file mode 100644 index 00000000000..1c60cae2576 --- /dev/null +++ b/checker/tests/nonempty/EnsuresNonEmptyTest.java @@ -0,0 +1,22 @@ +import java.util.ArrayList; +import org.checkerframework.checker.nonempty.qual.EnsuresNonEmpty; +import org.checkerframework.checker.nonempty.qual.NonEmpty; + +class EnsuresNonEmptyTest { + + @EnsuresNonEmpty("#1") + void m1(ArrayList l1) { + l1.add("foo"); + } + + void m2(@NonEmpty ArrayList l1) {} + + void test(ArrayList l1) { + // m2 requires a @NonEmpty collection, l1 has type @UnknownNonEmpty + // :: error: (argument) + m2(l1); + + m1(l1); + m2(l1); // OK + } +} diff --git a/checker/tests/nonempty/ImmutableListOperations.java b/checker/tests/nonempty/ImmutableListOperations.java new file mode 100644 index 00000000000..1fdb87ad008 --- /dev/null +++ b/checker/tests/nonempty/ImmutableListOperations.java @@ -0,0 +1,18 @@ +import java.util.List; +import org.checkerframework.checker.nonempty.qual.NonEmpty; + +class ImmutableListOperations { + + void testCreateEmptyImmutableList() { + List emptyInts = List.of(); + // Creating a copy of an empty list should also yield an empty list + // :: error: (assignment) + @NonEmpty List copyOfEmptyInts = List.copyOf(emptyInts); + } + + void testCreateNonEmptyImmutableList() { + List nonEmptyInts = List.of(1, 2, 3); + // Creating a copy of a non-empty list should also yield a non-empty list + @NonEmpty List copyOfNonEmptyInts = List.copyOf(nonEmptyInts); // OK + } +} diff --git a/checker/tests/nonempty/ImmutableMapOperations.java b/checker/tests/nonempty/ImmutableMapOperations.java new file mode 100644 index 00000000000..f097a4589f1 --- /dev/null +++ b/checker/tests/nonempty/ImmutableMapOperations.java @@ -0,0 +1,29 @@ +import java.util.Map; +import org.checkerframework.checker.nonempty.qual.NonEmpty; + +// @skip-test until JDK is annotated with Non-Empty type qualifiers + +class ImmutableMapOperations { + + void emptyImmutableMap() { + Map emptyMap = Map.of(); + // :: error: (assignment) + @NonEmpty Map nonEmptyMap = emptyMap; + } + + void nonEmptyImmutableMap() { + Map nonEmptyMap = Map.of("Hello", 1); + @NonEmpty Map m1 = nonEmptyMap; + } + + void immutableCopyEmptyMap() { + Map emptyMap = Map.of(); + // :: error: (assignment) + @NonEmpty Map nonEmptyMap = Map.copyOf(emptyMap); + } + + void immutableCopyNonEmptyMap() { + Map nonEmptyMap = Map.of("Hello", 1, "World", 2); + @NonEmpty Map m2 = Map.copyOf(nonEmptyMap); + } +} diff --git a/checker/tests/nonempty/ImmutableSetOperations.java b/checker/tests/nonempty/ImmutableSetOperations.java new file mode 100644 index 00000000000..02c002cae50 --- /dev/null +++ b/checker/tests/nonempty/ImmutableSetOperations.java @@ -0,0 +1,18 @@ +import java.util.Set; +import org.checkerframework.checker.nonempty.qual.NonEmpty; + +class ImmutableSetOperations { + + void testCreateEmptyImmutableSet() { + Set emptyInts = Set.of(); + // Creating a copy of an empty set should also yield an empty set + // :: error: (assignment) + @NonEmpty Set copyOfEmptyInts = Set.copyOf(emptyInts); + } + + void testCreateNonEmptyImmutableSet() { + Set nonEmptyInts = Set.of(1, 2, 3); + // Creating a copy of a non-empty set should also yield a non-empty set + @NonEmpty Set copyOfNonEmptyInts = Set.copyOf(nonEmptyInts); + } +} diff --git a/checker/tests/nonempty/IndexOfNonNegative.java b/checker/tests/nonempty/IndexOfNonNegative.java new file mode 100644 index 00000000000..1a7b7a91537 --- /dev/null +++ b/checker/tests/nonempty/IndexOfNonNegative.java @@ -0,0 +1,83 @@ +// @skip-test : contains() has a call to a locally-defined indexOf() method, which is hard to verify + +import java.util.AbstractSet; +import java.util.Collection; +import java.util.Iterator; +import org.checkerframework.checker.nonempty.qual.PolyNonEmpty; +import org.checkerframework.dataflow.qual.Pure; +import org.checkerframework.dataflow.qual.SideEffectFree; + +public class IndexOfNonNegative extends AbstractSet { + + @SideEffectFree + public IndexOfNonNegative() {} + + // Query Operations + + @Pure + @Override + public int size() { + return -1; + } + + @Pure + @Override + public boolean isEmpty() { + return size() == 0; + } + + @Pure + private int indexOf(Object value) { + return -1; + } + + @Pure + @Override + public boolean contains(Object value) { + // return indexOf(value) != -1; + if (indexOf(value) != -1) { + return true; + } else { + return false; + } + } + + // Modification Operations + + @Override + public boolean add(E value) { + return false; + } + + @Override + public boolean remove(Object value) { + return true; + } + + // Bulk Operations + + @Override + public boolean addAll(Collection c) { + return false; + } + + @Override + public boolean removeAll(Collection c) { + return true; + } + + // Inherit retainAll() from AbstractCollection. + + @Override + public void clear() {} + + /////////////////////////////////////////////////////////////////////////// + + // iterators + + @Override + // :: error: (override.receiver) + public @PolyNonEmpty Iterator iterator(@PolyNonEmpty IndexOfNonNegative this) { + throw new Error(""); + } +} diff --git a/checker/tests/nonempty/Issue6407.java b/checker/tests/nonempty/Issue6407.java new file mode 100644 index 00000000000..c52697ae253 --- /dev/null +++ b/checker/tests/nonempty/Issue6407.java @@ -0,0 +1,61 @@ +import java.util.LinkedList; +import java.util.List; +import org.checkerframework.checker.nonempty.qual.EnsuresNonEmpty; +import org.checkerframework.checker.nonempty.qual.NonEmpty; +import org.checkerframework.checker.nonempty.qual.UnknownNonEmpty; + +class Issue6407 { + + void usesJdk() { + // items initially has the type @UnknownNonEmpty + List items = new LinkedList<>(); + items.add("hello"); + @NonEmpty List bar = items; // OK + items.remove("hello"); + // :: error: (assignment) + @NonEmpty List baz = items; // I expect an error here + } + + static class MyList { + @SuppressWarnings("contracts.postcondition") // nonfunctional class + @EnsuresNonEmpty("this") + boolean add(E e) { + return true; + } + + boolean remove(@NonEmpty MyList this, E e) { + return true; + } + } + + boolean removeIt(@NonEmpty MyList myl, T e) { + return true; + } + + void noJdk() { + // items initially has the type @UnknownNonEmpty + @UnknownNonEmpty MyList items = new MyList<>(); + items.add("hello"); + @NonEmpty MyList bar = items; // OK + items.remove("hello"); + // :: error: (assignment) + @NonEmpty MyList baz = items; + } + + void noJdk2() { + // items initially has the type @UnknownNonEmpty + @UnknownNonEmpty MyList items = new MyList<>(); + items.add("hello"); + @NonEmpty MyList bar = items; // OK + removeIt(items, "hello"); + // :: error: (assignment) + @NonEmpty MyList baz = items; + } + + void initialRemoval() { + // items initially has the type @UnknownNonEmpty + MyList items = new MyList<>(); + // :: error: (method.invocation) + items.remove("hello"); + } +} diff --git a/checker/tests/nonempty/IteratorOperations.java b/checker/tests/nonempty/IteratorOperations.java new file mode 100644 index 00000000000..a862cbf959c --- /dev/null +++ b/checker/tests/nonempty/IteratorOperations.java @@ -0,0 +1,75 @@ +import java.util.Iterator; +import java.util.List; +import org.checkerframework.checker.nonempty.qual.NonEmpty; + +class IteratorOperations { + + void testPolyNonEmptyIterator(List nums) { + // :: error: (method.invocation) + nums.iterator().next(); + + if (!nums.isEmpty()) { + @NonEmpty Iterator nonEmptyIterator = nums.iterator(); + nonEmptyIterator.next(); + } else { + // :: error: (assignment) + @NonEmpty Iterator unknownEmptyIterator = nums.iterator(); + } + } + + void testSwitchRefinementNoFallthrough(List nums) { + switch (nums.size()) { + case 0: + // :: error: (method.invocation) + nums.iterator().next(); + break; + case 1: + @NonEmpty List nums2 = nums; // OK + break; + default: + @NonEmpty List nums3 = nums; // OK + } + } + + void testSwitchRefinementWithFallthrough(List nums) { + switch (nums.size()) { + case 0: + // :: error: (method.invocation) + nums.iterator().next(); + case 1: + // :: error: (assignment) + @NonEmpty List nums2 = nums; + default: + // :: error: (assignment) + @NonEmpty List nums3 = nums; + } + } + + void testSwitchRefinementNoZero(List nums) { + switch (nums.size()) { + case 1: + nums.iterator().next(); + break; + default: + // :: error: (assignment) + @NonEmpty List nums3 = nums; + } + } + + void testSwitchRefinementIndexOf(List strs, String s) { + switch (strs.indexOf(s)) { + case -1: + // :: error: (method.invocation) + strs.iterator().next(); + break; + case 0: + @NonEmpty List strs2 = strs; + case 2: + case 3: + strs.iterator().next(); + break; + default: + @NonEmpty List strs3 = strs; + } + } +} diff --git a/checker/tests/nonempty/ListOperations.java b/checker/tests/nonempty/ListOperations.java new file mode 100644 index 00000000000..fe0956fec12 --- /dev/null +++ b/checker/tests/nonempty/ListOperations.java @@ -0,0 +1,51 @@ +import java.util.ArrayList; +import java.util.List; +import org.checkerframework.checker.nonempty.qual.NonEmpty; + +class ListOperations { + + // Skip test until we decide whether to handle accesses on empty containers + // void testGetOnEmptyList(List strs) { + // // :: error: (method.invocation) + // strs.get(0); + // } + + // Skip test until we decide whether to handle accesses on empty containers + // void testGetOnNonEmptyList(List strs) { + // if (strs.isEmpty()) { + // // :: error: (method.invocation) + // strs.get(0); + // } else { + // strs.get(0); // OK + // } + // } + + void testAddToEmptyListAndGet() { + List nums = new ArrayList<>(); + nums.add(1); // nums has type @NonEmpty after this line + nums.get(0); // OK + } + + void testAddAllWithEmptyList() { + List nums = new ArrayList<>(); + nums.addAll(List.of()); + // :: error: (assignment) + @NonEmpty List nums2 = nums; + } + + void testAddAllWithNonEmptyList() { + List nums = new ArrayList<>(); + if (nums.addAll(List.of(1, 2, 3))) { + @NonEmpty List nums2 = nums; // OK + } + } + + void testContains(List nums) { + if (nums.contains(11)) { + @NonEmpty List nums2 = nums; // OK + } + // :: error: (assignment) + @NonEmpty List nums2 = nums; + } + // TODO: consider other sequences (e.g., calling get(int) after clear()) +} diff --git a/checker/tests/nonempty/MapOperations.java b/checker/tests/nonempty/MapOperations.java new file mode 100644 index 00000000000..63073baaf6a --- /dev/null +++ b/checker/tests/nonempty/MapOperations.java @@ -0,0 +1,44 @@ +import java.util.Map; +import org.checkerframework.checker.nonempty.qual.NonEmpty; + +class MapOperations { + + // Skip test until we decide whether to handle accesses on empty containers + // void addToMapParam(Map m) { + // // :: error: (method.invocation) + // m.get("hello"); + + // m.put("hello", 1); + + // @NonEmpty Map m2 = m; // OK + // m.get("hello"); // OK + // } + + // Skip test until we decide whether to handle accesses on empty containers + // void clearMap(Map m) { + // m.put("hello", 1); + // m.get("hello"); // OK + + // m.clear(); + // // :: error: (method.invocation) + // m.get("hello"); + // } + + void containsKeyRefinement(Map m, String key) { + if (m.containsKey(key)) { + @NonEmpty Map m2 = m; // OK + } else { + // :: error: (assignment) + @NonEmpty Map m2 = m; // OK + } + } + + void containsValueRefinement(Map m, Integer value) { + if (m.containsValue(value)) { + @NonEmpty Map m2 = m; + } else { + // :: error: (assignment) + @NonEmpty Map m2 = m; + } + } +} diff --git a/checker/tests/nonempty/NonEmptyHierarchyTest.java b/checker/tests/nonempty/NonEmptyHierarchyTest.java new file mode 100644 index 00000000000..a68659d84d7 --- /dev/null +++ b/checker/tests/nonempty/NonEmptyHierarchyTest.java @@ -0,0 +1,15 @@ +import java.util.List; +import org.checkerframework.checker.nonempty.qual.NonEmpty; +import org.checkerframework.checker.nonempty.qual.UnknownNonEmpty; + +class NonEmptyHierarchyTest { + + void testAssignments(@NonEmpty List l1, @UnknownNonEmpty List l2) { + @NonEmpty List l3 = l1; // OK, both are @NonEmpty + + // :: error: (assignment) + @NonEmpty List l4 = l2; + + List l5 = l1; // l5 implicitly has type @UnknownNonEmpty, assigning l1 to it is legal + } +} diff --git a/checker/tests/nonempty/PredicateTestMethod.java b/checker/tests/nonempty/PredicateTestMethod.java new file mode 100644 index 00000000000..8f3f379d2c4 --- /dev/null +++ b/checker/tests/nonempty/PredicateTestMethod.java @@ -0,0 +1,21 @@ +import java.util.ArrayList; +import java.util.Collection; +import java.util.List; +import java.util.function.Predicate; + +@SuppressWarnings( + "nonempty:argument") // Side Effects Only Checker is required to determine that `filter.test` +// does +// not side-effect anything else. +class PredicateTestMethod { + + public static List filter1(Collection coll, Predicate filter) { + List result = new ArrayList<>(); + for (T elt : coll) { + if (filter.test(elt)) { + result.add(elt); + } + } + return result; + } +} diff --git a/checker/tests/nonempty/RequiresNonEmptyTest.java b/checker/tests/nonempty/RequiresNonEmptyTest.java new file mode 100644 index 00000000000..b1fad95613b --- /dev/null +++ b/checker/tests/nonempty/RequiresNonEmptyTest.java @@ -0,0 +1,49 @@ +import java.util.LinkedList; +import java.util.List; +import org.checkerframework.checker.nonempty.qual.NonEmpty; +import org.checkerframework.checker.nonempty.qual.RequiresNonEmpty; +import org.checkerframework.dataflow.qual.Pure; + +class MyClass { + + List list1 = new LinkedList<>(); + List list2; + + @RequiresNonEmpty("list1") + @Pure + void m1() {} + + @RequiresNonEmpty({"list1", "list2"}) + @Pure + void m2() {} + + @RequiresNonEmpty({"list1", "list2"}) + void m3() {} + + void m4() {} + + void test(@NonEmpty List l1, @NonEmpty List l2) { + MyClass testClass = new MyClass(); + + // At this point, we should have an error since m1 requires that list1 is @NonEmpty, which is + // not the case here + // :: error: (contracts.precondition) + testClass.m1(); + + testClass.list1 = l1; + testClass.m1(); // OK + + // A call to m2 is stil illegal here, since list2 is still @UnknownNonEmpty + // :: error: (contracts.precondition) + testClass.m2(); + + testClass.list2 = l2; + testClass.m2(); // OK + + testClass.m4(); + + // No longer OK to call m2, no guarantee that m4() was pure + // :: error: (contracts.precondition) + testClass.m2(); + } +} diff --git a/checker/tests/nonempty/SetOperations.java b/checker/tests/nonempty/SetOperations.java new file mode 100644 index 00000000000..ca8af22822c --- /dev/null +++ b/checker/tests/nonempty/SetOperations.java @@ -0,0 +1,55 @@ +import java.util.HashSet; +import java.util.Set; +import org.checkerframework.checker.nonempty.qual.NonEmpty; + +class SetOperations { + + void testIsEmpty(Set nums) { + if (nums.isEmpty()) { + // :: error: (assignment) + @NonEmpty Set nums2 = nums; + } else { + @NonEmpty Set nums3 = nums; // OK + } + } + + void testContains(Set nums) { + if (nums.contains(1)) { + @NonEmpty Set nums2 = nums; + } else { + // :: error: (assignment) + @NonEmpty Set nums3 = nums; + } + } + + void testAdd(Set nums) { + // :: error: (assignment) + @NonEmpty Set nums2 = nums; // No guarantee that the set is non-empty here + if (nums.add(1)) { + @NonEmpty Set nums3 = nums; + } + } + + void testAddAllEmptySet() { + Set nums = new HashSet<>(); + // :: error: (assignment) + @NonEmpty Set nums2 = nums; + if (nums.addAll(Set.of())) { + // Adding an empty set will always return false, this is effectively dead code + @NonEmpty Set nums3 = nums; + } else { + // :: error: (assignment) + @NonEmpty Set nums3 = nums; + } + } + + void testRemove() { + Set nums = new HashSet<>(); + nums.add(1); + @NonEmpty Set nums2 = nums; + nums.remove(1); + + // :: error: (assignment) + @NonEmpty Set nums3 = nums; + } +} diff --git a/checker/tests/nonempty/SizeInIsEmpty.java b/checker/tests/nonempty/SizeInIsEmpty.java new file mode 100644 index 00000000000..b1182723f0d --- /dev/null +++ b/checker/tests/nonempty/SizeInIsEmpty.java @@ -0,0 +1,75 @@ +import java.util.AbstractSet; +import java.util.Iterator; +import org.checkerframework.checker.nonempty.qual.EnsuresNonEmptyIf; +import org.checkerframework.checker.nonempty.qual.PolyNonEmpty; +import org.checkerframework.dataflow.qual.Pure; +import org.checkerframework.dataflow.qual.SideEffectFree; + +public class SizeInIsEmpty extends AbstractSet { + + @SideEffectFree + public SizeInIsEmpty() {} + + // Query Operations + + @Pure + @Override + public int size() { + return -1; + } + + @Pure + @Override + @EnsuresNonEmptyIf(result = false, expression = "this") + public boolean isEmpty() { + if (size() == 0) { + return true; + } else { + return false; + } + } + + @EnsuresNonEmptyIf(result = false, expression = "this") + public boolean isEmpty2() { + return size() == 0 ? true : false; + } + + @EnsuresNonEmptyIf(result = false, expression = "this") + public boolean isEmpty3() { + return size() == 0; + } + + //// iterators + + @Override + public @PolyNonEmpty Iterator iterator(@PolyNonEmpty SizeInIsEmpty this) { + throw new Error(""); + } + + void testRefineIsEmpty1(SizeInIsEmpty container) { + if (!container.isEmpty()) { + container.iterator().next(); + } else { + // :: error: (method.invocation) + container.iterator().next(); + } + } + + void testRefineIsEmpty2(SizeInIsEmpty container) { + if (!container.isEmpty2()) { + container.iterator().next(); + } else { + // :: error: (method.invocation) + container.iterator().next(); + } + } + + void testRefineIsEmpty3(SizeInIsEmpty container) { + if (!container.isEmpty3()) { + container.iterator().next(); + } else { + // :: error: (method.invocation) + container.iterator().next(); + } + } +} diff --git a/checker/tests/nonempty/Streams.java b/checker/tests/nonempty/Streams.java new file mode 100644 index 00000000000..57ba66e17dd --- /dev/null +++ b/checker/tests/nonempty/Streams.java @@ -0,0 +1,47 @@ +import java.util.List; +import java.util.stream.Stream; +import org.checkerframework.checker.nonempty.qual.NonEmpty; + +class Streams { + + void testSingletonStreamCreation() { + @NonEmpty Stream strm = Stream.of(1); // OK + } + + void testStreamAnyMatch(Stream strStream) { + if (strStream.anyMatch(str -> str.length() > 10)) { + @NonEmpty Stream neStream = strStream; + } else { + // :: error: (assignment) + @NonEmpty Stream err = strStream; + } + } + + void testStreamAllMatch(Stream strStream) { + if (strStream.allMatch(str -> str.length() > 10)) { + @NonEmpty Stream neStream = strStream; + } else { + // :: error: (assignment) + @NonEmpty Stream err = strStream; + } + } + + void testMapNonEmptyStream(@NonEmpty List strs) { + @NonEmpty Stream lens = strs.stream().map(str -> str.length()); + } + + void testMapNonEmptyStream(Stream strs) { + // :: error: (assignment) + @NonEmpty Stream lens = strs.map(str -> str.length()); + } + + void testNoneMatch(Stream strs) { + if (strs.noneMatch(str -> str.length() < 10)) { + // :: error: (assignment) + @NonEmpty Stream err = strs; + } else { + // something matched; meaning that the stream MUST be non-empty + @NonEmpty Stream nonEmptyStrs = strs; + } + } +} diff --git a/checker/tests/nonempty/UnmodifiableTest.java b/checker/tests/nonempty/UnmodifiableTest.java new file mode 100644 index 00000000000..f0b832c38f4 --- /dev/null +++ b/checker/tests/nonempty/UnmodifiableTest.java @@ -0,0 +1,51 @@ +import static java.util.Map.entry; + +import java.util.Collections; +import java.util.List; +import java.util.Map; +import org.checkerframework.checker.nonempty.qual.NonEmpty; + +class UnmodifiableTest { + + void unmodifiableCopy(@NonEmpty List strs) { + @NonEmpty List strsCopy = Collections.unmodifiableList(strs); // OK + } + + void checkNonEmptyThenCopy(List strs) { + if (strs.isEmpty()) { + // :: error: (method.invocation) + Collections.unmodifiableList(strs).iterator().next(); + } else { + Collections.unmodifiableList(strs).iterator().next(); // OK + } + } + + void testVarArgsEmpty() { + // :: error: (assignment) + @NonEmpty List items = List.of(); + } + + void testVarArgsNonEmptyList() { + // Requires more than 10 elements to invoke the varargs version + @NonEmpty List items = List.of(1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12); // OK + } + + void testVarArgsNonEmptyMap() { + // Requires more than 10 elements to invoke the varargs version + @NonEmpty + Map map = + Map.ofEntries( + entry("a", 1), + entry("b", 2), + entry("c", 3), + entry("d", 4), + entry("e", 5), + entry("f", 6), + entry("g", 7), + entry("h", 8), + entry("i", 9), + entry("j", 10), + entry("k", 11), + entry("l", 12)); + } +} diff --git a/docs/manual/advanced-features.tex b/docs/manual/advanced-features.tex index 11722fc7638..7c3e175ab47 100644 --- a/docs/manual/advanced-features.tex +++ b/docs/manual/advanced-features.tex @@ -919,6 +919,10 @@ \item \ahrefloc{index-checker}{Index Checker} for array accesses (see \chapterpageref{index-checker}) +% Uncomment when the Non-Empty Checker is ready to be publicized. +% \item +% \ahrefloc{non-empty-checker}{Non-Empty Checker} to determine whether a +% collection, iterator, iterable, or map is non-empty (see \chapterpageref{non-empty-checker}) \item \ahrefloc{resource-leak-checker}{Resource Leak Checker} for ensuring that resources are disposed of properly (see \chapterpageref{resource-leak-checker}) diff --git a/docs/manual/figures/nonempty-subtyping.svg b/docs/manual/figures/nonempty-subtyping.svg new file mode 100644 index 00000000000..84314d3700c --- /dev/null +++ b/docs/manual/figures/nonempty-subtyping.svg @@ -0,0 +1,157 @@ + + + + + + image/svg+xml + + + + + + + + + + @UnknownNonEmpty + + + + + @NonEmpty + + + + + + + + + diff --git a/docs/manual/introduction.tex b/docs/manual/introduction.tex index 9ec09aa29db..61126bf81de 100644 --- a/docs/manual/introduction.tex +++ b/docs/manual/introduction.tex @@ -49,6 +49,10 @@ \item \ahrefloc{index-checker}{Index Checker} for array accesses (see \chapterpageref{index-checker}) +% TODO: Uncomment when the Non-Empty Checker is ready to be publicized. +% \item +% \ahrefloc{non-empty-checker}{Non-Empty Checker} to determine whether a +% collection, iterator, iterable, or map is non-empty (see \chapterpageref{non-empty-checker}) \item \ahrefloc{regex-checker}{Regex Checker} to prevent use of syntactically invalid regular expressions (see \chapterpageref{regex-checker}) diff --git a/docs/manual/manual.tex b/docs/manual/manual.tex index b608abc89a9..b5aba4b8784 100644 --- a/docs/manual/manual.tex +++ b/docs/manual/manual.tex @@ -58,6 +58,8 @@ \input{tainting-checker.tex} \input{lock-checker.tex} \input{index-checker.tex} +% TODO: Uncomment when the Non-Empty Checker is ready to be publicized. +% \input{non-empty-checker.tex} % These are focused on strings: \input{regex-checker.tex} diff --git a/docs/manual/non-empty-checker.tex b/docs/manual/non-empty-checker.tex new file mode 100644 index 00000000000..f7ff42bb4e2 --- /dev/null +++ b/docs/manual/non-empty-checker.tex @@ -0,0 +1,173 @@ +\htmlhr +\chapterAndLabel{Non-Empty Checker for container classes}{non-empty-checker} + +The Non-Empty Checker tracks whether a container may be empty. +It works on containers such as +\s, \s, \s, and \s, but not \s. + +If the Non-Empty Checker issues no warnings, then your program does not +throw \ as a result of calling methods such as +\, +\, \, \, or +\. + +To run the Non-Empty Checker, run either of these commands: + +\begin{alltt} + javac -processor nonempty \emph{MyJavaFile}.java + javac -processor org.checkerframework.checker.nonempty.NonEmptyChecker \emph{MyJavaFile}.java +\end{alltt} + + +\sectionAndLabel{Non-Empty annotations}{non-empty-annotations} + +These qualifiers make up the Non-Empty type system: + +\begin{description} + +\item[\refqualclass{checker/nonempty/qual}{UnknownNonEmpty}] + The annotated collection, iterator, iterable, or map may or may not be empty. + This is the top type; programmers need not explicitly write it. + +\item[\refqualclass{checker/nonempty/qual}{NonEmpty}] + The annotated collection, iterator, iterable, or map is \emph{definitely} + non-empty. + +\item[\refqualclass{checker/nonempty/qual}{PolyNonEmpty}] + indicates qualifier polymorphism. + For a description of qualifier polymorphism, see + Section~\ref{method-qualifier-polymorphism}. + +\end{description} + +\begin{figure} +\includeimage{nonempty-subtyping}{3.75cm} +\caption{The subtyping relationship of the Non-Empty Checker's qualifiers.} +\label{fig-nonempty-hierarchy} +\end{figure} + +\subsectionAndLabel{Non-Empty method annotations}{non-empty-method-annotations} + +The Non-Empty Checker supports several annotations that specify method +behavior. These are declaration annotations, not type annotations; they +apply to the annotated method itself rather than to some particular type. + +\begin{description} + +\item[\refqualclass{checker/nonempty/qual}{RequiresNonEmpty}] + indicates a method precondition. The annotated method expects the + specified expresssion to be non-empty when the + method is invoked. You could write \<@RequiresNonEmpty($f$)> when field + \<$f$> is sometimes empty, but the annotated method requires + \<$f$> to be non-empty. + +\item[\refqualclass{checker/nonempty/qual}{EnsuresNonEmpty}] + indicates a method postcondition. After the method returns (without + throwing an exception), the given + expression is non-empty. See the Javadoc for examples of its use. + +\item[\refqualclass{checker/nonempty/qual}{EnsuresNonEmptyIf}] + indicates a method postcondition. With \<@EnsuresNonEmpty>, the given + expression is non-empty after the method returns normally. With + \<@EnsuresNonEmptyIf>, if the annotated + method returns the given boolean value (true or false), then the given + expression is non-empty. See the Javadoc for examples of its use. + +\end{description} + + +\sectionAndLabel{Annotating your code with \<@NonEmpty>}{annotating-with-non-empty} + +The default annotation for collections, iterators, iterables, and maps is +\<@UnknownNonEmpty>. +Refinement to the \<@NonEmpty> type occurs in certain cases, such as after +conditional checks for empty/non-emptiness (see Section~\ref{type-refinement} for +more details): + +\begin{Verbatim} + public List getSessionIds() { ... } + ... + List sessionIds = getSessionIds(); // sessionIds has type @UnknownNonEmpty + ... + if (!sessionIds.isEmpty()) { + sessionIds.iterator().next(); // OK, sessionIds has type @NonEmpty + ... + } +\end{Verbatim} + +A programmer can manually annotate code in cases where a collection, +iterator, iterable, or map is always known to be non-empty, but that fact is +unable to be inferred by the type system: + +\begin{Verbatim} + // This call always returns a non-empty map; there is always at least one user in the store + public @NonEmpty Map getUserMapping() { ... } + ... + Map users = getUserMapping(); // users has type @NonEmpty +\end{Verbatim} + +\sectionAndLabel{What the Non-Empty Checker checks}{non-empty-checker-checks} + +The Non-Empty Checker ensures that collections, iterators, iterables, or maps +are non-empty at certain points in a program. +If a program type-checks cleanly under the Non-Empty Checker (i.e., no errors +are issued by the checker), then the program is certified with a compile-time +guarantee of the absence of errors rooted in the use of operations that +rely on whether a collection is non-empty. +For example, calling \ on an iterator that is known to be \<@NonEmpty> +should never fail, or, getting the first element of a \<@NonEmpty> list should +not throw an exception. + +The Non-Empty Checker does \emph{not} provide guarantees about the fixed +length or size of collections, iterators, iterables, or maps, beyond whether +it has a length or size of at least 1 (i.e., it is non-empty). +The Index Checker (\chapterpageref{index-checker}) is a checker that analyzes +array bounds and indices and warns about potential +\s. + +The Non-Empty Checker does \emph{not} provide guarantees about proper use +of \, even though misuse can lead to the same execption, +\. Use the Optional Checker +(\chapterpageref{optional-checker}) instead. + + +\sectionAndLabel{Suppressing non-empty warnings}{suppressing-non-empty-warnings} + +Like any sound static analysis tool, the Non-Empty Checker may issue a warning +for code that is correct. +It is often best to change your code or annotations in this case. +Alternatively, you may choose to suppress the warning. +This does not change the code, but prevents the warning from being presented to +you. +The Checker Framework supplies several mechanisms to suppress warnings (see +\chapterpageref{suppressing-warnings}). +The \<@SuppressWarnings("nonempty")> annotation is specific to warnings raised +by the Non-Empty Checker: + +\begin{Verbatim} +// This method might return an empty list, depending on the argument +List getRegionIds(String region) { ... } + +void parseRegions() { + @SuppressWarnings("nonempty") // We know that `getRegions(x)` returns a non-empty list. + @NonEmpty List regionIds = getRegionIds(x); +} +\end{Verbatim} + +\subsectionAndLabel{Suppressing warnings with assertions}{suppressing-warnings-with-assertions} + +Occasionally, it is inconvenient or verbose to use the \<@SuppressWarnings> +annotation. +For example, Java does not permit annotations such as \<@SuppressWarnings> to +appear on expressions, static initializers, etc. +Here are two ways to suppress a warning in such cases: + +\begin{itemize} +\item + Create a local variable to hold a subexpression, and + suppress a warning on the local variable declaration. +\item + Use the \<@AssumeAssertion> string in + an \ message (see Section~\ref{assumeassertion}). +\end{itemize} + diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java index 92aec12fcd3..d835609da53 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -3652,19 +3652,22 @@ protected void checkArguments( List passedArgs, CharSequence executableName, List paramNames) { - int size = requiredTypes.size(); - assert size == passedArgs.size() - : "size mismatch between required args (" - + requiredTypes - + ") and passed args (" - + passedArgs - + ")"; + int numRequired = requiredTypes.size(); + assert numRequired == passedArgs.size() + : String.format( + "numRequired %d should equal %d in checkArguments(%s, %s, %s, %s)", + numRequired, + passedArgs.size(), + listToString(requiredTypes), + listToString(passedArgs), + executableName, + listToString(paramNames)); int maxParamNamesIndex = paramNames.size() - 1; // Rather weak assertion, due to how varargs parameters are treated. - assert size >= maxParamNamesIndex + assert numRequired >= maxParamNamesIndex : String.format( "mismatched lengths %d %d %d checkArguments(%s, %s, %s, %s)", - size, + numRequired, passedArgs.size(), paramNames.size(), listToString(requiredTypes), @@ -3672,7 +3675,7 @@ protected void checkArguments( executableName, listToString(paramNames)); - for (int i = 0; i < size; ++i) { + for (int i = 0; i < numRequired; ++i) { AnnotatedTypeMirror requiredType = requiredTypes.get(i); ExpressionTree passedArg = passedArgs.get(i); Object paramName = paramNames.get(Math.min(i, maxParamNamesIndex)); diff --git a/framework/src/main/java/org/checkerframework/framework/util/AnnotatedTypes.java b/framework/src/main/java/org/checkerframework/framework/util/AnnotatedTypes.java index 4b20005dbb8..be1b3372ea2 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/AnnotatedTypes.java +++ b/framework/src/main/java/org/checkerframework/framework/util/AnnotatedTypes.java @@ -1019,6 +1019,7 @@ public static List adaptParameters( Tree invok) { List parameters = method.getParameterTypes(); + // Handle anonymous constructors that extend a class with an enclosing type, // as in `new MyClass(){ ... }`. if (method.getElement().getKind() == ElementKind.CONSTRUCTOR diff --git a/framework/tests/all-systems/ForEach.java b/framework/tests/all-systems/ForEach.java index 96d4e6e1063..7a32348fe0f 100644 --- a/framework/tests/all-systems/ForEach.java +++ b/framework/tests/all-systems/ForEach.java @@ -32,6 +32,9 @@ void m4(T p) { } } + @SuppressWarnings( + "nonempty") // TODO: the Non-Empty Checker requires the Side Effects Only checker to eliminate + // the false positive here public static List removeDuplicates(List l) { // There are shorter solutions that do not maintain order. HashSet hs = new HashSet<>(l.size()); diff --git a/framework/tests/all-systems/GenericTest11full.java b/framework/tests/all-systems/GenericTest11full.java index 7e6744a8462..cf5631d093c 100644 --- a/framework/tests/all-systems/GenericTest11full.java +++ b/framework/tests/all-systems/GenericTest11full.java @@ -1,4 +1,7 @@ public class GenericTest11full { + @SuppressWarnings( + "nonempty:method.invocation") // Cannot determine statically whether the getBeans(...) call + // below will return a non-empty container. public void m(BeanManager beanManager) { Bean bean = beanManager.getBeans(GenericTest11full.class).iterator().next(); CreationalContext context = beanManager.createCreationalContext(bean);