diff --git a/build.gradle b/build.gradle index bfd1b8b4725..023e359e010 100644 --- a/build.gradle +++ b/build.gradle @@ -9,7 +9,7 @@ plugins { // https://github.com/tbroyer/gradle-errorprone-plugin id 'net.ltgt.errorprone' version '3.1.0' // https://plugins.gradle.org/plugin/org.ajoberstar.grgit - id 'org.ajoberstar.grgit' version '5.2.0' apply false + id 'org.ajoberstar.grgit' version '5.2.1' apply false id 'groovy' // needed for formatting Gradle files // Code formatting; defines targets "spotlessApply" and "spotlessCheck". diff --git a/checker-qual/src/main/java/org/checkerframework/checker/calledmethods/qual/EnsuresCalledMethods.java b/checker-qual/src/main/java/org/checkerframework/checker/calledmethods/qual/EnsuresCalledMethods.java index 1d7757411e5..000f9bca669 100644 --- a/checker-qual/src/main/java/org/checkerframework/checker/calledmethods/qual/EnsuresCalledMethods.java +++ b/checker-qual/src/main/java/org/checkerframework/checker/calledmethods/qual/EnsuresCalledMethods.java @@ -44,6 +44,7 @@ @PostconditionAnnotation(qualifier = CalledMethods.class) @Target({ElementType.METHOD, ElementType.CONSTRUCTOR}) @Repeatable(EnsuresCalledMethods.List.class) +@InheritedAnnotation public @interface EnsuresCalledMethods { /** * The Java expressions that will have methods called on them. @@ -72,6 +73,7 @@ @Retention(RetentionPolicy.RUNTIME) @Target({ElementType.METHOD, ElementType.CONSTRUCTOR}) @InheritedAnnotation + @PostconditionAnnotation(qualifier = CalledMethods.class) public static @interface List { /** * Return the repeatable annotations. diff --git a/checker-qual/src/main/java/org/checkerframework/checker/calledmethods/qual/RequiresCalledMethods.java b/checker-qual/src/main/java/org/checkerframework/checker/calledmethods/qual/RequiresCalledMethods.java index c47039b8589..ac5ae5e185c 100644 --- a/checker-qual/src/main/java/org/checkerframework/checker/calledmethods/qual/RequiresCalledMethods.java +++ b/checker-qual/src/main/java/org/checkerframework/checker/calledmethods/qual/RequiresCalledMethods.java @@ -2,6 +2,7 @@ import java.lang.annotation.Documented; import java.lang.annotation.ElementType; +import java.lang.annotation.Repeatable; import java.lang.annotation.Retention; import java.lang.annotation.RetentionPolicy; import java.lang.annotation.Target; @@ -22,6 +23,7 @@ @Retention(RetentionPolicy.RUNTIME) @PreconditionAnnotation(qualifier = CalledMethods.class) @Target({ElementType.METHOD, ElementType.CONSTRUCTOR}) +@Repeatable(RequiresCalledMethods.List.class) public @interface RequiresCalledMethods { /** * The Java expressions that must have had methods called on them. @@ -48,6 +50,7 @@ */ @Documented @Retention(RetentionPolicy.RUNTIME) + @PreconditionAnnotation(qualifier = CalledMethods.class) @Target({ElementType.METHOD, ElementType.CONSTRUCTOR}) public static @interface List { /** diff --git a/checker-qual/src/main/java/org/checkerframework/checker/optional/qual/EnsuresPresent.java b/checker-qual/src/main/java/org/checkerframework/checker/optional/qual/EnsuresPresent.java new file mode 100644 index 00000000000..1dd109e37c8 --- /dev/null +++ b/checker-qual/src/main/java/org/checkerframework/checker/optional/qual/EnsuresPresent.java @@ -0,0 +1,49 @@ +package org.checkerframework.checker.optional.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.InheritedAnnotation; +import org.checkerframework.framework.qual.PostconditionAnnotation; + +/** + * Indicates that the expression evaluates to a non-empty Optional, if the method terminates + * successfully. + * + *

This postcondition annotation is useful for methods that construct a non-empty Optional: + * + * 


+ *   {@literal @}EnsuresPresent("optStr")
+ *   void initialize() {
+ *     optStr = Optional.of("abc");
+ *   }
+ *
+ * + * It can also be used for a method that fails if a given Optional value is empty, indicating that + * the argument is null if the method returns normally: + * + * 

+ *   /** Throws an exception if the argument is empty. */
+ *   {@literal @}EnsuresPresent("#1")
+ *   void useTheOptional(Optional<T> arg) { ... }
+ *
+ * + * @see Present + * @see org.checkerframework.checker.optional.OptionalChecker + * @checker_framework.manual #optional-checker Optional Checker + */ +@Documented +@Retention(RetentionPolicy.RUNTIME) +@Target({ElementType.METHOD, ElementType.CONSTRUCTOR}) +@PostconditionAnnotation(qualifier = Present.class) +@InheritedAnnotation +public @interface EnsuresPresent { + /** + * The expression (of Optional type) that is present, if the method returns normally. + * + * @return the expression (of Optional type) that is present, if the method returns normally + */ + String[] value(); +} diff --git a/checker-util/src/main/java/org/checkerframework/checker/nullness/util/NullnessUtil.java b/checker-util/src/main/java/org/checkerframework/checker/nullness/util/NullnessUtil.java index 445c08e1300..0af1a3c975a 100644 --- a/checker-util/src/main/java/org/checkerframework/checker/nullness/util/NullnessUtil.java +++ b/checker-util/src/main/java/org/checkerframework/checker/nullness/util/NullnessUtil.java @@ -48,7 +48,7 @@ private NullnessUtil() { * * // one way to use as a statement: * castNonNull(possiblyNull3); - * possiblyNull3.toString();` + * possiblyNull3.toString(); * * * The {@code castNonNull} method is intended to be used in situations where the programmer diff --git a/checker-util/src/main/java/org/checkerframework/checker/optional/util/OptionalUtil.java b/checker-util/src/main/java/org/checkerframework/checker/optional/util/OptionalUtil.java new file mode 100644 index 00000000000..e6f078b9191 --- /dev/null +++ b/checker-util/src/main/java/org/checkerframework/checker/optional/util/OptionalUtil.java @@ -0,0 +1,75 @@ +package org.checkerframework.checker.optional.util; + +import java.util.Optional; +import org.checkerframework.checker.optional.qual.EnsuresPresent; +import org.checkerframework.checker.optional.qual.MaybePresent; +import org.checkerframework.checker.optional.qual.Present; +import org.checkerframework.framework.qual.AnnotatedFor; + +/** + * This is a utility class for the Optional Checker. + * + *

To avoid the need to write the OptionalUtil class name, do: + * + * 

import static org.checkerframework.checker.optional.util.OptionalUtil.castPresent;
+ * + * or + * + * 
import static org.checkerframework.checker.optional.util.OptionalUtil.*;
+ * + *

Runtime Dependency: If you use this class, you must distribute (or link to) {@code + * checker-qual.jar}, along with your binaries. Or, you can copy this class into your own project. + */ +@SuppressWarnings({ + "optional", // Optional utilities are trusted regarding the Optional type. + "cast" // Casts look redundant if Optional Checker is not run. +}) +@AnnotatedFor("optional") +public final class OptionalUtil { + + /** The OptionalUtil class should not be instantiated. */ + private OptionalUtil() { + throw new AssertionError("do not instantiate"); + } + + /** + * A method that suppresses warnings from the Optional Checker. + * + *

The method takes a possibly-empty Optional reference, unsafely casts it to have the @Present + * type qualifier, and returns it. The Optional Checker considers both the return value, and also + * the argument, to be present after the method call. Therefore, the {@code castPresent} method + * can be used either as a cast expression or as a statement. + * + * 


+   *   // one way to use as a cast:
+   *  {@literal @}Present String s = castPresent(possiblyEmpty1);
+   *
+   *   // another way to use as a cast:
+   *   castPresent(possiblyEmpty2).toString();
+   *
+   *   // one way to use as a statement:
+   *   castPresent(possiblyEmpty3);
+   *   possiblyEmpty3.toString();
+   *
+ * + * The {@code castPresent} method is intended to be used in situations where the programmer + * definitively knows that a given Optional reference is present, but the type system is unable to + * make this deduction. It is not intended for defensive programming, in which a programmer cannot + * prove that the value is not empty but wishes to have an earlier indication if it is. See the + * Checker Framework Manual for further discussion. + * + *

The method throws {@link AssertionError} if Java assertions are enabled and the argument is + * empty. If the exception is ever thrown, then that indicates that the programmer misused the + * method by using it in a circumstance where its argument can be empty. + * + * @param the type of content of the Optional + * @param ref an Optional reference of @MaybePresent type, that is present at run time + * @return the argument, casted to have the type qualifier @Present + */ + @EnsuresPresent("#1") + public static @Present Optional castPresent( + @MaybePresent Optional ref) { + assert ref.isPresent() : "Misuse of castPresent: called with an empty Optional"; + return (@Present Optional) ref; + } +} diff --git a/checker-util/src/test/java/org/checkerframework/checker/optional/util/OptionalUtilTest.java b/checker-util/src/test/java/org/checkerframework/checker/optional/util/OptionalUtilTest.java new file mode 100644 index 00000000000..7deb69f8bcd --- /dev/null +++ b/checker-util/src/test/java/org/checkerframework/checker/optional/util/OptionalUtilTest.java @@ -0,0 +1,23 @@ +package org.checkerframework.checker.optional.util; + +import java.util.Optional; +import org.checkerframework.checker.optional.qual.Present; +import org.junit.Assert; +import org.junit.Test; + +public final class OptionalUtilTest { + + @Test + public void test_castPresent() { + + Optional nonEmptyOpt = Optional.of("non-empty"); + Optional emptyOpt = Optional.empty(); + + Assert.assertFalse(nonEmptyOpt.isEmpty()); + @Present Optional foo = OptionalUtil.castPresent(nonEmptyOpt); + Assert.assertEquals(foo.get(), "non-empty"); + + Assert.assertTrue(emptyOpt.isEmpty()); + Assert.assertThrows(Error.class, () -> OptionalUtil.castPresent(emptyOpt)); + } +} diff --git a/checker/build.gradle b/checker/build.gradle index 6b3d702d734..6a59670c711 100644 --- a/checker/build.gradle +++ b/checker/build.gradle @@ -68,7 +68,7 @@ dependencies { // For the Resource Leak Checker's support for JavaEE. testImplementation 'javax.servlet:javax.servlet-api:4.0.1' // For the Resource Leak Checker's support for IOUtils. - testImplementation 'commons-io:commons-io:2.14.0' + testImplementation 'commons-io:commons-io:2.15.0' testImplementation group: 'junit', name: 'junit', version: '4.13.2' testImplementation project(':framework-test') @@ -910,7 +910,8 @@ task wpiManyTest(group: 'Verification') { '-i', "${project.projectDir}/tests/wpi-many/testin.txt", '-o', "${project.projectDir}/build/wpi-many-tests", '-s', - '--', '--checker', 'nullness,interning,lock,regex,signature,calledmethods,resourceleak' + '--', '--checker', 'nullness,interning,lock,regex,signature,calledmethods,resourceleak', + '--extraJavacArgs=-AenableWpiForRlc' } } catch (Exception e) { println('Failure: Running wpi-many.sh failed with a non-zero exit code.') diff --git a/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsAnnotatedTypeFactory.java index 312d902974b..3aa1c3da044 100644 --- a/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsAnnotatedTypeFactory.java @@ -11,6 +11,7 @@ import javax.lang.model.element.Element; import javax.lang.model.element.ExecutableElement; import javax.lang.model.element.TypeElement; +import javax.lang.model.type.DeclaredType; import javax.lang.model.type.TypeKind; import javax.lang.model.type.TypeMirror; import org.checkerframework.checker.calledmethods.builder.AutoValueSupport; @@ -39,6 +40,7 @@ import org.checkerframework.javacutil.AnnotationUtils; import org.checkerframework.javacutil.ElementUtils; import org.checkerframework.javacutil.TreeUtils; +import org.checkerframework.javacutil.TypesUtils; import org.checkerframework.javacutil.UserError; /** The annotated type factory for the Called Methods Checker. */ @@ -428,4 +430,21 @@ private AnnotationMirror ensuresCMAnno(String[] expressions, List called AnnotationMirror am = builder.build(); return am; } + + /** + * Returns true if the checker should ignore exceptional control flow due to the given exception + * type. + * + * @param exceptionType exception type + * @return {@code true} if {@code exceptionType} is a member of {@link + * CalledMethodsAnalysis#ignoredExceptionTypes}, {@code false} otherwise + */ + @Override + public boolean isIgnoredExceptionType(TypeMirror exceptionType) { + if (exceptionType.getKind() == TypeKind.DECLARED) { + return CalledMethodsAnalysis.ignoredExceptionTypes.contains( + TypesUtils.getQualifiedName((DeclaredType) exceptionType)); + } + return false; + } } diff --git a/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsTransfer.java b/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsTransfer.java index bf05616fe8a..a7174871be0 100644 --- a/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsTransfer.java +++ b/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsTransfer.java @@ -1,5 +1,6 @@ package org.checkerframework.checker.calledmethods; +import com.sun.source.tree.Tree; import java.util.Arrays; import java.util.Collections; import java.util.LinkedHashMap; @@ -11,6 +12,7 @@ import javax.lang.model.type.TypeMirror; import org.checkerframework.checker.calledmethods.qual.EnsuresCalledMethodsVarArgs; import org.checkerframework.checker.nullness.qual.Nullable; +import org.checkerframework.checker.resourceleak.ResourceLeakChecker; import org.checkerframework.common.accumulation.AccumulationStore; import org.checkerframework.common.accumulation.AccumulationTransfer; import org.checkerframework.common.accumulation.AccumulationValue; @@ -50,6 +52,12 @@ public class CalledMethodsTransfer extends AccumulationTransfer { */ private final ExecutableElement calledMethodsValueElement; + /** + * True if -AenableWpiForRlc was passed on the command line. See {@link + * ResourceLeakChecker#ENABLE_WPI_FOR_RLC}. + */ + private final boolean enableWpiForRlc; + /** * Create a new CalledMethodsTransfer. * @@ -59,6 +67,40 @@ public CalledMethodsTransfer(CalledMethodsAnalysis analysis) { super(analysis); calledMethodsValueElement = ((CalledMethodsAnnotatedTypeFactory) atypeFactory).calledMethodsValueElement; + enableWpiForRlc = atypeFactory.getChecker().hasOption(ResourceLeakChecker.ENABLE_WPI_FOR_RLC); + } + + /** + * @param tree a tree + * @return false if Resource Leak Checker is running as one of the upstream checkers and the + * -AenableWpiForRlc flag (see {@link ResourceLeakChecker#ENABLE_WPI_FOR_RLC}) is not passed + * as a command line argument, otherwise returns the result of the super call + */ + @Override + protected boolean shouldPerformWholeProgramInference(Tree tree) { + if (!isWpiEnabledForRLC() + && atypeFactory.getCheckerNames().contains(ResourceLeakChecker.class.getCanonicalName())) { + return false; + } + return super.shouldPerformWholeProgramInference(tree); + } + + /** + * See {@link ResourceLeakChecker#ENABLE_WPI_FOR_RLC}. + * + * @param expressionTree a tree + * @param lhsTree its element + * @return false if Resource Leak Checker is running as one of the upstream checkers and the + * -AenableWpiForRlc flag is not passed as a command line argument, otherwise returns the + * result of the super call + */ + @Override + protected boolean shouldPerformWholeProgramInference(Tree expressionTree, Tree lhsTree) { + if (!isWpiEnabledForRLC() + && atypeFactory.getCheckerNames().contains(ResourceLeakChecker.class.getCanonicalName())) { + return false; + } + return super.shouldPerformWholeProgramInference(expressionTree, lhsTree); } @Override @@ -229,4 +271,14 @@ private void handleEnsuresCalledMethodsVarArgs( return atypeFactory.createAccumulatorAnnotation(newList); } + + /** + * Checks if WPI is enabled for the Resource Leak Checker inference. See {@link + * ResourceLeakChecker#ENABLE_WPI_FOR_RLC}. + * + * @return returns true if WPI is enabled for the Resource Leak Checker + */ + protected boolean isWpiEnabledForRLC() { + return enableWpiForRlc; + } } diff --git a/checker/src/main/java/org/checkerframework/checker/index/samelen/SameLenChecker.java b/checker/src/main/java/org/checkerframework/checker/index/samelen/SameLenChecker.java index 1d8976036e1..97394dd83e5 100644 --- a/checker/src/main/java/org/checkerframework/checker/index/samelen/SameLenChecker.java +++ b/checker/src/main/java/org/checkerframework/checker/index/samelen/SameLenChecker.java @@ -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; /** @@ -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. */ diff --git a/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallAnnotatedTypeFactory.java index 83a9f4c07d7..564edd8c2ee 100644 --- a/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallAnnotatedTypeFactory.java @@ -31,6 +31,7 @@ import org.checkerframework.checker.mustcall.qual.Owning; import org.checkerframework.checker.mustcall.qual.PolyMustCall; import org.checkerframework.checker.nullness.qual.Nullable; +import org.checkerframework.checker.resourceleak.ResourceLeakChecker; import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory; import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.dataflow.cfg.block.Block; @@ -116,6 +117,12 @@ public class MustCallAnnotatedTypeFactory extends BaseAnnotatedTypeFactory /** True if -AnoLightweightOwnership was passed on the command line. */ private final boolean noLightweightOwnership; + /** + * True if -AenableWpiForRlc (see {@link ResourceLeakChecker#ENABLE_WPI_FOR_RLC}) was passed on + * the command line. + */ + private final boolean enableWpiForRlc; + /** * Creates a MustCallAnnotatedTypeFactory. * @@ -132,6 +139,7 @@ public MustCallAnnotatedTypeFactory(BaseTypeChecker checker) { addAliasedTypeAnnotation(MustCallAlias.class, POLY); } noLightweightOwnership = checker.hasOption(MustCallChecker.NO_LIGHTWEIGHT_OWNERSHIP); + enableWpiForRlc = checker.hasOption(ResourceLeakChecker.ENABLE_WPI_FOR_RLC); this.postInit(); } @@ -223,6 +231,13 @@ protected void constructorFromUsePreSubstitution( */ private void changeNonOwningParameterTypesToTop( ExecutableElement declaration, AnnotatedExecutableType type) { + // Formal parameters without a declared owning annotation are disregarded by the RLC _analysis_, + // as their @MustCall obligation is set to Top in this method. However, this computation is not + // desirable for RLC _inference_ in unannotated programs, where a goal is to infer and add + // @Owning annotations to formal parameters. + if (getWholeProgramInference() != null && !isWpiEnabledForRLC()) { + return; + } List parameterTypes = type.getParameterTypes(); for (int i = 0; i < parameterTypes.size(); i++) { Element paramDecl = declaration.getParameters().get(i); @@ -416,7 +431,11 @@ public MustCallTreeAnnotator(MustCallAnnotatedTypeFactory mustCallAnnotatedTypeF @Override public Void visitIdentifier(IdentifierTree tree, AnnotatedTypeMirror type) { Element elt = TreeUtils.elementFromUse(tree); - if (elt.getKind() == ElementKind.PARAMETER + // The following changes are not desired for RLC _inference_ in unannotated programs, where a + // goal is to infer and add @Owning annotations to formal parameters. Therefore, if WPI is + // enabled, they should not be executed. + if (getWholeProgramInference() == null + && elt.getKind() == ElementKind.PARAMETER && (noLightweightOwnership || getDeclAnnotation(elt, Owning.class) == null)) { if (!type.hasPrimaryAnnotation(POLY)) { // Parameters that are not annotated with @Owning should be treated as bottom @@ -443,6 +462,16 @@ public Void visitIdentifier(IdentifierTree tree, AnnotatedTypeMirror type) { return tempVars.get(node.getTree()); } + /** + * Checks if WPI is enabled for the Resource Leak Checker inference. See {@link + * ResourceLeakChecker#ENABLE_WPI_FOR_RLC}. + * + * @return returns true if WPI is enabled for the Resource Leak Checker + */ + protected boolean isWpiEnabledForRLC() { + return enableWpiForRlc; + } + /** * Returns true if the given type should never have a must-call obligation. * diff --git a/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallTransfer.java b/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallTransfer.java index 0eddccc33d6..6b22b3ed4bf 100644 --- a/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallTransfer.java +++ b/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallTransfer.java @@ -3,6 +3,7 @@ import com.sun.source.tree.ClassTree; import com.sun.source.tree.ExpressionTree; import com.sun.source.tree.IdentifierTree; +import com.sun.source.tree.Tree; import com.sun.source.tree.VariableTree; import com.sun.source.util.TreePath; import java.util.List; @@ -14,6 +15,7 @@ import org.checkerframework.checker.mustcall.qual.MustCall; import org.checkerframework.checker.nullness.qual.MonotonicNonNull; import org.checkerframework.checker.nullness.qual.Nullable; +import org.checkerframework.checker.resourceleak.ResourceLeakChecker; import org.checkerframework.dataflow.analysis.TransferInput; import org.checkerframework.dataflow.analysis.TransferResult; import org.checkerframework.dataflow.cfg.node.AssignmentNode; @@ -58,6 +60,12 @@ public class MustCallTransfer extends CFTransfer { /** True if -AnoCreatesMustCallFor was passed on the command line. */ private final boolean noCreatesMustCallFor; + /** + * True if -AenableWpiForRlc was passed on the command line. See {@link + * ResourceLeakChecker#ENABLE_WPI_FOR_RLC}. + */ + private final boolean enableWpiForRlc; + /** * Create a MustCallTransfer. * @@ -68,6 +76,7 @@ public MustCallTransfer(CFAnalysis analysis) { atypeFactory = (MustCallAnnotatedTypeFactory) analysis.getTypeFactory(); noCreatesMustCallFor = atypeFactory.getChecker().hasOption(MustCallChecker.NO_CREATES_MUSTCALLFOR); + enableWpiForRlc = atypeFactory.getChecker().hasOption(ResourceLeakChecker.ENABLE_WPI_FOR_RLC); ProcessingEnvironment env = atypeFactory.getChecker().getProcessingEnvironment(); treeBuilder = new TreeBuilder(env); } @@ -175,6 +184,41 @@ private void lubWithStoreValue(CFStore store, JavaExpression expr, AnnotationMir store.insertValue(expr, newValue); } + /** + * See {@link ResourceLeakChecker#ENABLE_WPI_FOR_RLC}. + * + * @param tree a tree + * @return false if Resource Leak Checker is running as one of the upstream checkers and the + * -AenableWpiForRlc flag is not passed as a command line argument, otherwise returns the + * result of the super call + */ + @Override + protected boolean shouldPerformWholeProgramInference(Tree tree) { + if (!isWpiEnabledForRLC() + && atypeFactory.getCheckerNames().contains(ResourceLeakChecker.class.getCanonicalName())) { + return false; + } + return super.shouldPerformWholeProgramInference(tree); + } + + /** + * See {@link ResourceLeakChecker#ENABLE_WPI_FOR_RLC}. + * + * @param expressionTree a tree + * @param lhsTree its element + * @return false if Resource Leak Checker is running as one of the upstream checkers and the + * -AenableWpiForRlc flag is not passed as a command line argument, otherwise returns the + * result of the super call + */ + @Override + protected boolean shouldPerformWholeProgramInference(Tree expressionTree, Tree lhsTree) { + if (!isWpiEnabledForRLC() + && atypeFactory.getCheckerNames().contains(ResourceLeakChecker.class.getCanonicalName())) { + return false; + } + return super.shouldPerformWholeProgramInference(expressionTree, lhsTree); + } + @Override public TransferResult visitObjectCreation( ObjectCreationNode node, TransferInput input) { @@ -299,4 +343,14 @@ public void updateStoreWithTempVar(TransferResult result, Node protected String uniqueName(String prefix) { return prefix + "-" + uid.getAndIncrement(); } + + /** + * Checks if WPI is enabled for the Resource Leak Checker inference. See {@link + * ResourceLeakChecker#ENABLE_WPI_FOR_RLC}. + * + * @return returns true if WPI is enabled for the Resource Leak Checker + */ + protected boolean isWpiEnabledForRLC() { + return enableWpiForRlc; + } } diff --git a/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallVisitor.java b/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallVisitor.java index bbc0e5b8a05..368a8508996 100644 --- a/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallVisitor.java @@ -23,6 +23,7 @@ import org.checkerframework.checker.mustcall.qual.MustCallAlias; import org.checkerframework.checker.mustcall.qual.NotOwning; import org.checkerframework.checker.mustcall.qual.Owning; +import org.checkerframework.checker.mustcall.qual.PolyMustCall; import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.common.basetype.BaseTypeVisitor; import org.checkerframework.framework.type.AnnotatedTypeMirror; @@ -232,9 +233,24 @@ public boolean isValidUse( // Note that isValidUse does not need to consider component types, on which it should be // called separately. Element elt = TreeUtils.elementFromTree(tree); - if (elt != null - && AnnotationUtils.containsSameByClass(elt.getAnnotationMirrors(), MustCallAlias.class)) { - return true; + if (elt != null) { + if (AnnotationUtils.containsSameByClass(elt.getAnnotationMirrors(), MustCallAlias.class)) { + return true; + } + // Need to check the type mirror for ajava-derived annotations and the element itself + // for human-written annotations from the source code. Getting to the ajava file directly + // at this point is impossible, so we approximate "the ajava file has an @MustCallAlias + // annotation" with "there is an @PolyMustCall annotation on the use type, but not in the + // source code". This only works because none of our inference techniques infer @PolyMustCall, + // so if @PolyMustCall is present but wasn't in the source, it must have been derived from + // an @MustCallAlias annotation (which we do infer). + boolean ajavaFileHasMustCallAlias = + useType.hasPrimaryAnnotation(PolyMustCall.class) + && !AnnotationUtils.containsSameByClass( + elt.getAnnotationMirrors(), PolyMustCall.class); + if (ajavaFileHasMustCallAlias) { + return true; + } } return super.isValidUse(declarationType, useType, tree); } diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessVisitor.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessVisitor.java index 5c8ce1447b3..4a3c971a619 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessVisitor.java @@ -253,6 +253,9 @@ protected boolean commonAssignmentCheck( /** Case 1: Check for null dereferencing. */ @Override public Void visitMemberSelect(MemberSelectTree tree, Void p) { + if (atypeFactory.isUnreachable(tree)) { + return super.visitMemberSelect(tree, p); + } Element e = TreeUtils.elementFromUse(tree); if (e.getKind() == ElementKind.CLASS) { if (atypeFactory.containsNullnessAnnotation(null, tree.getExpression())) { diff --git a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java index dccd3cd0f06..f3685970254 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java @@ -12,6 +12,7 @@ import com.sun.source.util.TreePath; import java.util.ArrayDeque; import java.util.ArrayList; +import java.util.Collection; import java.util.Collections; import java.util.Deque; import java.util.EnumSet; @@ -25,6 +26,7 @@ import java.util.Objects; import java.util.Set; import java.util.StringJoiner; +import java.util.stream.Collectors; import javax.lang.model.SourceVersion; import javax.lang.model.element.AnnotationMirror; import javax.lang.model.element.Element; @@ -834,7 +836,8 @@ private boolean areSame(JavaExpression target, @Nullable JavaExpression enclosin * @param node the invocation node whose result is to be tracked; must be {@link * MethodInvocationNode} or {@link ObjectCreationNode} */ - private void updateObligationsWithInvocationResult(Set obligations, Node node) { + /*package-private*/ void updateObligationsWithInvocationResult( + Set obligations, Node node) { Tree tree = node.getTree(); // Only track the result of the call if there is a temporary variable for the call node // (because if there is no temporary, then the invocation must produce an untrackable value, @@ -1101,7 +1104,7 @@ private void updateObligationsForOwningReturn( * @param node a node * @return the temporary for node, or node if no temporary exists */ - private Node getTempVarOrNode(Node node) { + /*package-private*/ Node getTempVarOrNode(Node node) { Node temp = typeFactory.getTempVarForNode(node); if (temp != null) { return temp; @@ -1269,7 +1272,7 @@ private boolean hasAtMostOneOwningField(TypeElement element) { * @param node the node * @return true if must-call type of node only contains close */ - private boolean isMustCallClose(Node node) { + /*package-private*/ boolean isMustCallClose(Node node) { MustCallAnnotatedTypeFactory mcAtf = typeFactory.getTypeFactoryOfSubchecker(MustCallChecker.class); AnnotatedTypeMirror mustCallAnnotatedType = mcAtf.getAnnotatedType(node.getTree()); @@ -1313,7 +1316,8 @@ private void addAliasToObligationsContainingVar( * @param obligations the set of Obligations to modify * @param var a variable */ - private void removeObligationsContainingVar(Set obligations, LocalVariableNode var) { + /*package-private*/ void removeObligationsContainingVar( + Set obligations, LocalVariableNode var) { removeObligationsContainingVar( obligations, var, MustCallAliasHandling.NO_SPECIAL_HANDLING, MethodExitKind.ALL); } @@ -1399,7 +1403,7 @@ private void removeObligationsContainingVar( * temporary variable (via a call to {@link * ResourceLeakAnnotatedTypeFactory#getTempVarForNode}) */ - private void updateObligationsForPseudoAssignment( + /*package-private*/ void updateObligationsForPseudoAssignment( Set obligations, Node node, LocalVariableNode lhsVar, Node rhs) { // Replacements to eventually perform in Obligations. This map is kept to avoid a // ConcurrentModificationException in the loop below. @@ -1826,7 +1830,7 @@ private Node removeCastsAndGetTmpVarIfPresent(Node node) { * @param node a MethodInvocation or ObjectCreation node * @return the arguments, in order */ - private List getArgumentsOfInvocation(Node node) { + /*package-private*/ List getArgumentsOfInvocation(Node node) { if (node instanceof MethodInvocationNode) { MethodInvocationNode invocationNode = (MethodInvocationNode) node; return invocationNode.getArguments(); @@ -1845,7 +1849,7 @@ private List getArgumentsOfInvocation(Node node) { * @return a list of the declarations of the formal parameters of the method or constructor being * invoked */ - private List getParametersOfInvocation(Node node) { + /*package-private*/ List getParametersOfInvocation(Node node) { ExecutableElement executableElement; if (node instanceof MethodInvocationNode) { MethodInvocationNode invocationNode = (MethodInvocationNode) node; @@ -2296,7 +2300,7 @@ private static boolean varTrackedInObligations( * @return the Obligation in {@code obligations} whose resource alias set contains {@code node}, * or {@code null} if there is no such Obligation */ - private static @Nullable Obligation getObligationForVar( + /*package-private*/ static @Nullable Obligation getObligationForVar( Set obligations, LocalVariableNode node) { for (Obligation obligation : obligations) { if (obligation.canBeSatisfiedThrough(node)) { @@ -2457,7 +2461,7 @@ private void incrementMustCallImpl(TypeMirror type) { * @return true iff cmAnno is a subtype of a called-methods annotation with the same values as * mustCallValues */ - private boolean calledMethodsSatisfyMustCall( + /*package-private*/ boolean calledMethodsSatisfyMustCall( List mustCallValues, AnnotationMirror cmAnno) { // Create this annotation and use a subtype test because there's no guarantee that // cmAnno is actually an instance of CalledMethods: it could be CMBottom or CMPredicate. @@ -2509,7 +2513,7 @@ private static void propagate( * consists of BlockWithObligations objects, each representing the need to handle the set of * dataflow facts reaching the block during analysis. */ - private static class BlockWithObligations { + /*package-private*/ static class BlockWithObligations { /** The block. */ public final Block block; @@ -2545,5 +2549,58 @@ public boolean equals(@Nullable Object o) { public int hashCode() { return Objects.hash(block, obligations); } + + @Override + public String toString() { + return String.format( + "BWO{%s %d, %d obligations %d}", + block.getType(), block.getUid(), obligations.size(), obligations.hashCode()); + } + + /** + * Returns a printed representation of a collection of BlockWithObligations. If a + * BlockWithObligations appears multiple times in the collection, it is printed more succinctly + * after the first time. + * + * @param bwos a collection of BlockWithObligations, to format + * @return a printed representation of a collection of BlockWithObligations + */ + public static String collectionToString(Collection bwos) { + List blocksWithDuplicates = new ArrayList<>(); + for (BlockWithObligations bwo : bwos) { + blocksWithDuplicates.add(bwo.block); + } + List duplicateBlocks = duplicates(blocksWithDuplicates); + StringJoiner result = new StringJoiner(", ", "BWOs[", "]"); + for (BlockWithObligations bwo : bwos) { + ImmutableSet obligations = bwo.obligations; + if (duplicateBlocks.contains(bwo.block)) { + result.add( + String.format( + "BWO{%s %d, %d obligations %s}", + bwo.block.getType(), bwo.block.getUid(), obligations.size(), obligations)); + } else { + result.add( + String.format( + "BWO{%s %d, %d obligations}", + bwo.block.getType(), bwo.block.getUid(), obligations.size())); + } + } + return result.toString(); + } + } + + // TODO: Use from plume-lib's CollectionsPlume once version 1.9.0 is released. + /** + * Returns the elements (once each) that appear more than once in the given collection. + * + * @param the type of elements + * @param c a collection + * @return the elements (once each) that appear more than once in the given collection + */ + public static List duplicates(Collection c) { + // Inefficient (because of streams) but simple implementation. + Set withoutDuplicates = new HashSet<>(); + return c.stream().filter(n -> !withoutDuplicates.add(n)).collect(Collectors.toList()); } } diff --git a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInference.java b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInference.java index edda1b2e08d..1a1e55bf0dd 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInference.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInference.java @@ -1,176 +1,791 @@ package org.checkerframework.checker.resourceleak; +import com.google.common.collect.ImmutableSet; +import com.sun.source.tree.ClassTree; +import com.sun.source.tree.MethodTree; +import com.sun.source.tree.VariableTree; import java.util.ArrayDeque; -import java.util.ArrayList; +import java.util.Arrays; +import java.util.Collections; import java.util.Deque; import java.util.HashSet; +import java.util.LinkedHashMap; +import java.util.LinkedHashSet; import java.util.List; +import java.util.Map; import java.util.Set; import javax.lang.model.element.AnnotationMirror; import javax.lang.model.element.Element; +import javax.lang.model.element.ElementKind; +import javax.lang.model.element.ExecutableElement; +import javax.lang.model.element.Modifier; +import javax.lang.model.element.TypeElement; import javax.lang.model.element.VariableElement; +import javax.lang.model.type.TypeMirror; +import org.checkerframework.checker.calledmethods.qual.EnsuresCalledMethods; +import org.checkerframework.checker.mustcall.qual.InheritableMustCall; import org.checkerframework.checker.mustcall.qual.Owning; +import org.checkerframework.checker.nullness.qual.Nullable; +import org.checkerframework.checker.resourceleak.MustCallConsistencyAnalyzer.BlockWithObligations; +import org.checkerframework.checker.resourceleak.MustCallConsistencyAnalyzer.MethodExitKind; +import org.checkerframework.checker.resourceleak.MustCallConsistencyAnalyzer.Obligation; +import org.checkerframework.checker.resourceleak.MustCallConsistencyAnalyzer.ResourceAlias; +import org.checkerframework.common.accumulation.AccumulationStore; +import org.checkerframework.common.accumulation.AccumulationValue; import org.checkerframework.common.wholeprograminference.WholeProgramInference; import org.checkerframework.dataflow.cfg.ControlFlowGraph; +import org.checkerframework.dataflow.cfg.UnderlyingAST; import org.checkerframework.dataflow.cfg.block.Block; import org.checkerframework.dataflow.cfg.block.ConditionalBlock; import org.checkerframework.dataflow.cfg.block.SingleSuccessorBlock; +import org.checkerframework.dataflow.cfg.node.ArrayCreationNode; +import org.checkerframework.dataflow.cfg.node.AssignmentNode; +import org.checkerframework.dataflow.cfg.node.LocalVariableNode; import org.checkerframework.dataflow.cfg.node.MethodInvocationNode; import org.checkerframework.dataflow.cfg.node.Node; +import org.checkerframework.dataflow.cfg.node.ObjectCreationNode; +import org.checkerframework.dataflow.expression.JavaExpression; +import org.checkerframework.dataflow.expression.LocalVariable; +import org.checkerframework.dataflow.util.NodeUtils; import org.checkerframework.javacutil.AnnotationBuilder; +import org.checkerframework.javacutil.AnnotationUtils; import org.checkerframework.javacutil.BugInCF; +import org.checkerframework.javacutil.TreePathUtil; import org.checkerframework.javacutil.TreeUtils; +import org.checkerframework.javacutil.TypesUtils; +import org.plumelib.util.CollectionsPlume; /** - * This class contains the Resource Leak Checker's annotation inference algorithm. It contains - * inference logic for owning annotations on final owning fields. It adds an @Owning annotation on a - * field if it finds a method that satisfies the @MustCall obligation of the field along some path - * to the regular exit point. + * This class implements the annotation inference algorithm for the Resource Leak Checker. It infers + * annotations such as {@code @}{@link Owning} on owning fields and parameters, {@code @}{@link + * EnsuresCalledMethods} on methods, and {@code @}{@link InheritableMustCall} on class declarations. + * + *

Each instance of this class corresponds to a single control flow graph (CFG), typically + * representing a method. + * + *

The algorithm determines if the @MustCall obligation of a field is satisfied along some path + * leading to the regular exit point of the method. If the obligation is satisfied, it adds + * an @Owning annotation on the field and an @EnsuresCalledMethods annotation on the method being + * analyzed. Additionally, if the method being analyzed satisfies the must-call obligation of all + * the enclosed owning fields, it adds a @InheritableMustCall annotation on the enclosing class. + * + *

Note: This class makes the assumption that the must-call set has only one element. Must-call + * sets with more than one element may be supported in the future. + * + *

See {@link ResourceLeakChecker#ENABLE_WPI_FOR_RLC} for an explanation of the meaning of the + * flags {@code -Ainfer} and {@code -AenableWpiForRlc}. + * + * @see Automatic + * Inference of Resource Leak Specifications */ public class MustCallInference { - /** The set of owning fields. */ + /** + * The fields that have been inferred to be disposed within the CFG (i.e., method) currently under + * analysis. All of the fields in this set when inference finishes will be given an @Owning + * annotation. Note that this set is not monotonically-increasing: fields may be added to this set + * and then removed during inference. For example, if a field's must-call method is called, it is + * added to this set. If, in a later statement in the same method, the same field is re-assigned, + * it will be removed from this set (since the previously-inferred closing of the obligation is + * invalid). + */ + private final Set disposedFields = new HashSet<>(); + + /** + * The fields with written {@code @Owning} annotations at the entry point of the CFG currently + * under analysis in addition to the inferred owning fields in this analysis. This set is a + * superset of the {@code disposedFields} set. + */ private final Set owningFields = new HashSet<>(); /** * The type factory for the Resource Leak Checker, which is used to access the Must Call Checker. */ - private final ResourceLeakAnnotatedTypeFactory typeFactory; + private final ResourceLeakAnnotatedTypeFactory resourceLeakAtf; + + /** The MustCallConsistencyAnalyzer. */ + private final MustCallConsistencyAnalyzer mcca; /** The {@link Owning} annotation. */ protected final AnnotationMirror OWNING; - /** The control flow graph. */ + /** + * The control flow graph of the current method. There is a separate MustCallInference for each + * method. + */ private final ControlFlowGraph cfg; + /** The MethodTree of the current method. */ + private final MethodTree methodTree; + + /** The element for the current method. */ + private final ExecutableElement methodElt; + + /** The ClassTree referring to the enclosing class of the current method. */ + private final ClassTree classTree; + + /** The element referring to the enclosing class of the current method. */ + private final @Nullable TypeElement classElt; + /** - * Creates a MustCallInference. If the type factory has whole program inference enabled, its - * postAnalyze method should instantiate a new MustCallInference using this constructor and then - * call {@link #runInference()}. + * Creates a MustCallInference instance. * - * @param typeFactory the type factory - * @param cfg the ControlFlowGraph + * @param resourceLeakAtf the type factory + * @param cfg the control flow graph of the method to check + * @param mcca the MustCallConsistencyAnalyzer */ /*package-private*/ MustCallInference( - ResourceLeakAnnotatedTypeFactory typeFactory, ControlFlowGraph cfg) { - this.typeFactory = typeFactory; + ResourceLeakAnnotatedTypeFactory resourceLeakAtf, + ControlFlowGraph cfg, + MustCallConsistencyAnalyzer mcca) { + this.resourceLeakAtf = resourceLeakAtf; + this.mcca = mcca; this.cfg = cfg; - OWNING = AnnotationBuilder.fromClass(this.typeFactory.getElementUtils(), Owning.class); + OWNING = AnnotationBuilder.fromClass(this.resourceLeakAtf.getElementUtils(), Owning.class); + methodTree = ((UnderlyingAST.CFGMethod) cfg.getUnderlyingAST()).getMethod(); + methodElt = TreeUtils.elementFromDeclaration(methodTree); + classTree = TreePathUtil.enclosingClass(resourceLeakAtf.getPath(methodTree)); + // elementFromDeclaration() returns null when no element exists for the class tree, which can + // happen for certain kinds of anonymous classes, such as PolyCollectorTypeVar.java in the + // all-systems test suite. + classElt = TreeUtils.elementFromDeclaration(classTree); + + if (classElt != null) { + for (Element memberElt : classElt.getEnclosedElements()) { + if (memberElt.getKind().isField() && resourceLeakAtf.hasOwning(memberElt)) { + owningFields.add((VariableElement) memberElt); + } + } + } } /** - * Runs the inference algorithm on the contents of the {@link #cfg} field. + * Creates a MustCallInference instance and runs the inference algorithm. This method is called by + * the {@link ResourceLeakAnnotatedTypeFactory#postAnalyze} method if Whole Program Inference is + * enabled. * - *

Operationally, it checks method invocations for fields with non-empty @MustCall obligations - * along all paths to the regular exit point in the method body of the method represented by - * {@link #cfg}, and updates the {@link #owningFields} set if it discovers an owning field whose + * @param resourceLeakAtf the type factory + * @param cfg the control flow graph of the method to check + * @param mcca the MustCallConsistencyAnalyzer + */ + /*package-private*/ static void runMustCallInference( + ResourceLeakAnnotatedTypeFactory resourceLeakAtf, + ControlFlowGraph cfg, + MustCallConsistencyAnalyzer mcca) { + MustCallInference mustCallInferenceLogic = new MustCallInference(resourceLeakAtf, cfg, mcca); + mustCallInferenceLogic.runInference(); + } + + /** + * Runs the inference algorithm on the current method (the {@link #cfg} field). It updates the + * {@link #disposedFields} set or adds @Owning to the formal parameter if it discovers their * must-call obligations were satisfied along one of the checked paths. + * + *

Operationally, it checks method invocations for fields and parameters with + * non-empty @MustCall obligations along all paths to the regular exit point. */ - /*package-private*/ void runInference() { - Set visited = new HashSet<>(); - Deque worklist = new ArrayDeque<>(); - Block entry = this.cfg.getEntryBlock(); + private void runInference() { + Set visited = new HashSet<>(); + Deque worklist = new ArrayDeque<>(); + + BlockWithObligations entry = + new BlockWithObligations(cfg.getEntryBlock(), getNonEmptyMCParams(cfg)); worklist.add(entry); visited.add(entry); while (!worklist.isEmpty()) { - Block current = worklist.remove(); + BlockWithObligations current = worklist.remove(); + + // It uses a LinkedHashSet to maintain a deterministic order and prevent any inconsistencies + // between the results of inference in different iterations. + Set obligations = new LinkedHashSet<>(current.obligations); - for (Node node : current.getNodes()) { - if (node instanceof MethodInvocationNode) { - checkForMustCallInvocationOnField((MethodInvocationNode) node); + for (Node node : current.block.getNodes()) { + // The obligation set calculated for RLC differs from the Inference process. In the + // Inference process, it exclusively tracks parameters with non-empty must-call types, + // whether they have the @Owning annotation or not. However, there are some shared + // computations, such as updateObligationsWithInvocationResult, which is used during + // inference and could potentially affect the RLC result if it were called before the + // checking phase. However, calling updateObligationsWithInvocationResult() will not have + // any side effects on the outcome of the Resource Leak Checker. This is because the + // inference occurs within the postAnalyze method of the ResourceLeakAnnotatedTypeFactory, + // once the consistency analyzer has completed its process + if (node instanceof MethodInvocationNode || node instanceof ObjectCreationNode) { + mcca.updateObligationsWithInvocationResult(obligations, node); + computeOwningFromInvocation(obligations, node); + } else if (node instanceof AssignmentNode) { + analyzeOwnershipTransferAtAssignment(obligations, (AssignmentNode) node); } } - propagateRegPaths(current, visited, worklist); + addNonExceptionalSuccessorsToWorklist(obligations, current.block, visited, worklist); + } + + addMemberAndClassAnnotations(); + } + + /** + * Adds inferred {@literal @Owning} annotations to fields, {@literal @EnsuresCalledMethods} + * annotations to the current method, and {@literal @InheritableMustCall} annotation to the + * enclosing class. + */ + private void addMemberAndClassAnnotations() { + WholeProgramInference wpi = resourceLeakAtf.getWholeProgramInference(); + assert wpi != null : "MustCallInference is running without WPI."; + for (VariableElement fieldElt : updateOwningFields()) { + wpi.addFieldDeclarationAnnotation(fieldElt, OWNING); + } + if (!disposedFields.isEmpty()) { + addEnsuresCalledMethods(); + } + + addOrUpdateClassMustCall(); + } + + /** + * Returns a set of obligations representing the formal parameters of the current method that have + * non-empty MustCall annotations. Returns an empty set if the given CFG doesn't correspond to a + * method body. + * + * @param cfg the control flow graph of the method to check + * @return a set of obligations representing the parameters with non-empty MustCall + */ + private Set getNonEmptyMCParams(ControlFlowGraph cfg) { + // TODO what about lambdas? + if (cfg.getUnderlyingAST().getKind() != UnderlyingAST.Kind.METHOD) { + return Collections.emptySet(); + } + Set result = null; + for (VariableTree param : methodTree.getParameters()) { + if (resourceLeakAtf.declaredTypeHasMustCall(param)) { + VariableElement paramElement = TreeUtils.elementFromDeclaration(param); + if (result == null) { + result = new HashSet<>(2); + } + result.add( + new Obligation( + ImmutableSet.of( + new ResourceAlias(new LocalVariable(paramElement), paramElement, param)), + Collections.singleton(MethodExitKind.NORMAL_RETURN))); + } + } + return result != null ? result : Collections.emptySet(); + } + + /** + * Updates the owning fields set for this class to include all fields inferred as owning in this + * iteration. + * + * @return the owning fields, including fields inferred as owning from the current iteration + */ + private Set updateOwningFields() { + owningFields.addAll(disposedFields); + return owningFields; + } + + /** + * Adds an owning annotation to the formal parameter at the given index. + * + * @param index the index of a formal parameter of the current method (1-based) + */ + private void addOwningToParam(int index) { + WholeProgramInference wpi = resourceLeakAtf.getWholeProgramInference(); + wpi.addDeclarationAnnotationToFormalParameter(methodElt, index, OWNING); + } + + /** + * Adds the node to the disposedFields and owningFields sets if it is a field and its must-call + * obligation is satisfied by the given method call. If so, it will be given an @Owning annotation + * later. + * + * @param node possibly an owning field + * @param invocation method invoked on the possible owning field + */ + private void inferOwningField(Node node, MethodInvocationNode invocation) { + Element nodeElt = TreeUtils.elementFromTree(node.getTree()); + if (nodeElt == null || !nodeElt.getKind().isField()) { + return; + } + if (resourceLeakAtf.isFieldWithNonemptyMustCallValue(nodeElt)) { + node = NodeUtils.removeCasts(node); + JavaExpression nodeJe = JavaExpression.fromNode(node); + AnnotationMirror cmAnno = getCalledMethodsAnno(invocation, nodeJe); + List mustCallValues = resourceLeakAtf.getMustCallValues(nodeElt); + if (mcca.calledMethodsSatisfyMustCall(mustCallValues, cmAnno)) { + // This assumes that any MustCall annotation has at most one element. + // TODO: generalize this to MustCall annotations with more than one element. + assert mustCallValues.size() <= 1 : "TODO: Handle larger must-call values sets"; + disposedFields.add((VariableElement) nodeElt); + } } } /** - * If the receiver of {@code mNode} is a candidate owning field and the method invocation - * satisfies the field's must-call obligation, then adds that field to the {@link #owningFields} - * set. + * Analyzes an assignment statement and performs three computations: + * + *

* - * @param mNode the MethodInvocationNode + * @param obligations the set of obligations to update + * @param assignmentNode the assignment statement */ - private void checkForMustCallInvocationOnField(MethodInvocationNode mNode) { - Node receiver = mNode.getTarget().getReceiver(); - if (receiver.getTree() == null) { + private void analyzeOwnershipTransferAtAssignment( + Set obligations, AssignmentNode assignmentNode) { + Node lhs = assignmentNode.getTarget(); + Element lhsElement = TreeUtils.elementFromTree(lhs.getTree()); + // Use the temporary variable for the rhs if it exists. + Node rhs = NodeUtils.removeCasts(assignmentNode.getExpression()); + rhs = mcca.getTempVarOrNode(rhs); + + if (!(rhs instanceof LocalVariableNode)) { + return; + } + Obligation rhsObligation = + MustCallConsistencyAnalyzer.getObligationForVar(obligations, (LocalVariableNode) rhs); + if (rhsObligation == null) { return; } - Element receiverEl = TreeUtils.elementFromTree(receiver.getTree()); + if (lhsElement.getKind() == ElementKind.FIELD) { + if (!updateOwningFields().contains(lhsElement)) { + return; + } - if (receiverEl != null && typeFactory.isCandidateOwningField(receiverEl)) { - Element method = TreeUtils.elementFromUse(mNode.getTree()); - List mustCallValues = typeFactory.getMustCallValue(receiverEl); + // If the owning field is present in the disposedFields set and there is an assignment to the + // field, it must be removed from the set. This is essential since the disposedFields set is + // used for adding @EnsuresCalledMethods annotations to the current method later. Note that + // this removal doesn't affect the owning annotation we inferred for the field, as the + // owningField set is updated before this line through the 'updateOwningFields' method. + if (!TreeUtils.isConstructor(methodTree)) { + disposedFields.remove((VariableElement) lhsElement); + } + addOwningToParamsIfDisposedAtAssignment(obligations, rhsObligation, rhs); + } else if (lhsElement.getKind() == ElementKind.RESOURCE_VARIABLE && mcca.isMustCallClose(rhs)) { + addOwningToParamsIfDisposedAtAssignment(obligations, rhsObligation, rhs); + } else if (lhs instanceof LocalVariableNode) { + LocalVariableNode lhsVar = (LocalVariableNode) lhs; + mcca.updateObligationsForPseudoAssignment(obligations, assignmentNode, lhsVar, rhs); + } + } - // This assumes that any MustCall annotation has at most one element. - // TODO: generalize this to MustCall annotations with more than one element. - if (mustCallValues.size() == 1 - && mustCallValues.contains(method.getSimpleName().toString())) { - owningFields.add((VariableElement) receiverEl); + /** + * If a must-call obligation of some alias of method parameter p is satisfied during the + * assignment, add an @Owning annotation to p, and remove the rhs node from the obligations set, + * since it no longer needs to be tracked. + * + * @param obligations the set of obligations to update + * @param rhsObligation the obligation associated with the right-hand side of the assignment + * @param rhs the right-hand side of the assignment + */ + private void addOwningToParamsIfDisposedAtAssignment( + Set obligations, Obligation rhsObligation, Node rhs) { + Set rhsAliases = rhsObligation.resourceAliases; + if (rhsAliases.isEmpty()) { + return; + } + List paramElts = + CollectionsPlume.mapList(TreeUtils::elementFromDeclaration, methodTree.getParameters()); + for (ResourceAlias rhsAlias : rhsAliases) { + Element rhsElt = rhsAlias.element; + int i = paramElts.indexOf(rhsElt); + if (i != -1) { + addOwningToParam(i + 1); + mcca.removeObligationsContainingVar(obligations, (LocalVariableNode) rhs); + break; } } } /** - * Updates {@code worklist} with the next block along all paths to the regular exit point. If the - * next block is a regular exit point, adds an {@literal @}Owning annotation for fields in {@link - * #owningFields}. + * Adds an {@link EnsuresCalledMethods} annotation to the current method for any owning field + * whose must-call obligation is satisfied within the current method, i.e., the fields in {@link + * #disposedFields}. + */ + private void addEnsuresCalledMethods() { + // The keys are the must-call method names, and the values are the set of fields on which those + // methods should be called. This map is used to create a single @EnsuresCalledMethods + // annotation for fields that share the same must-call obligation. + Map> methodToFields = new LinkedHashMap<>(); + for (VariableElement disposedField : disposedFields) { + List mustCallValues = resourceLeakAtf.getMustCallValues(disposedField); + assert !mustCallValues.isEmpty() + : "Must-call obligation of owning field " + disposedField + " is empty."; + // Currently, this code assumes that the must-call set has only one element. + assert mustCallValues.size() == 1 + : "The must-call set of " + disposedField + "should be a singleton: " + mustCallValues; + String mustCallValue = mustCallValues.get(0); + String fieldName = "this." + disposedField.getSimpleName().toString(); + + methodToFields.computeIfAbsent(mustCallValue, k -> new HashSet<>()).add(fieldName); + } + + for (String mustCallValue : methodToFields.keySet()) { + Set fields = methodToFields.get(mustCallValue); + AnnotationMirror am = + createEnsuresCalledMethods( + fields.toArray(new String[fields.size()]), new String[] {mustCallValue}); + WholeProgramInference wpi = resourceLeakAtf.getWholeProgramInference(); + wpi.addMethodDeclarationAnnotation(methodElt, am); + } + } + + /** + * Possibly adds an InheritableMustCall annotation on the enclosing class. * - * @param curBlock the current block - * @param visited set of blocks already on the worklist - * @param worklist current worklist + *

If the class already has a non-empty MustCall type (that is inherited from one of its + * superclasses), this method does nothing, in order to avoid infinite iteration. Otherwise, if + * the current method is not private and satisfies the must-call obligations of all the owning + * fields, it adds (or updates) an InheritableMustCall annotation to the enclosing class. */ - private void propagateRegPaths(Block curBlock, Set visited, Deque worklist) { + private void addOrUpdateClassMustCall() { + if (classElt == null) { + return; + } - List successors = getNormalSuccessors(curBlock); + WholeProgramInference wpi = resourceLeakAtf.getWholeProgramInference(); + List currentMustCallValues = resourceLeakAtf.getMustCallValues(classElt); + if (!currentMustCallValues.isEmpty()) { + // The class already has a MustCall annotation. - for (Block b : successors) { - // If b is a special block, it must be the regular exit, since we do not propagate to - // exceptional successors. - if (b.getType() == Block.BlockType.SPECIAL_BLOCK) { - WholeProgramInference wpi = typeFactory.getWholeProgramInference(); - assert wpi != null : "MustCallInference is running without WPI."; - for (VariableElement fieldElt : owningFields) { - wpi.addFieldDeclarationAnnotation(fieldElt, OWNING); + // If it is inherited from a superclass, do nothing. + if (classElt.getSuperclass() != null) { + TypeMirror superType = classElt.getSuperclass(); + TypeElement superClassElt = TypesUtils.getTypeElement(superType); + if (superClassElt != null && !resourceLeakAtf.getMustCallValues(superClassElt).isEmpty()) { + return; } } - if (visited.add(b)) { - worklist.add(b); + // If the enclosing class already has a non-empty @MustCall type, either added by programmers + // or inferred in previous iterations (not-inherited), we do not change it in the current + // analysis round to prevent potential inconsistencies and guarantee the termination of the + // inference algorithm. This becomes particularly important when multiple methods could + // satisfy the must-call obligation of the enclosing class. To ensure the existing @MustCall + // annotation is included in the inference result for this iteration, we re-add it. + assert currentMustCallValues.size() == 1 : "TODO: Handle multiple must-call values"; + AnnotationMirror am = createInheritableMustCall(new String[] {currentMustCallValues.get(0)}); + wpi.addClassDeclarationAnnotation(classElt, am); + return; + } + + // If the current method is not private and satisfies the must-call obligation of all owning + // fields, then add (to the class) an InheritableMustCall annotation with the name of this + // method. + if (!methodTree.getModifiers().getFlags().contains(Modifier.PRIVATE)) { + // Since the result of updateOwningFields() is a superset of disposedFields, it is sufficient + // to + // check the equality of their sizes to determine if both sets are equal. + if (!disposedFields.isEmpty() && disposedFields.size() == updateOwningFields().size()) { + AnnotationMirror am = + createInheritableMustCall(new String[] {methodTree.getName().toString()}); + wpi.addClassDeclarationAnnotation(classElt, am); } } } /** - * Returns the non-exceptional successors of the current block. + * Computes ownership transfer at the method call to infer @Owning annotation for the arguments + * passed into the call. * - * @param cur the current block - * @return the successors of this current block + * @param obligations the obligations associated with the current block + * @param invocation the method or constructor invocation */ - private List getNormalSuccessors(Block cur) { - List successorBlock = new ArrayList<>(); + private void inferOwningParamsViaOwnershipTransfer(Set obligations, Node invocation) { + List paramsOfCurrentMethod = methodTree.getParameters(); + if (paramsOfCurrentMethod.isEmpty()) { + return; + } + List calleeParams = mcca.getParametersOfInvocation(invocation); + if (calleeParams.isEmpty()) { + return; + } + List arguments = mcca.getArgumentsOfInvocation(invocation); - if (cur.getType() == Block.BlockType.CONDITIONAL_BLOCK) { + for (int i = 0; i < arguments.size(); i++) { + if (!resourceLeakAtf.hasOwning(calleeParams.get(i))) { + continue; + } + for (int j = 0; j < paramsOfCurrentMethod.size(); j++) { + VariableTree paramOfCurrMethod = paramsOfCurrentMethod.get(j); + if (resourceLeakAtf.hasEmptyMustCallValue(paramOfCurrMethod)) { + continue; + } - ConditionalBlock ccur = (ConditionalBlock) cur; + Node arg = NodeUtils.removeCasts(arguments.get(i)); + VariableElement paramElt = TreeUtils.elementFromDeclaration(paramOfCurrMethod); + if (nodeAndElementResourceAliased(obligations, arg, paramElt)) { + addOwningToParam(j + 1); + break; + } + } + } + } + + /** + * Checks whether the given element is a resource alias of the given node in the provided set of + * obligations. + * + * @param obligations the obligations associated with the current block + * @param node the node + * @param element the element + * @return true if {@code element} is a resource alias of {@code node} + */ + private boolean nodeAndElementResourceAliased( + Set obligations, Node node, VariableElement element) { + Set nodeAliases = getResourceAliasOfNode(obligations, node); + for (ResourceAlias nodeAlias : nodeAliases) { + Element nodeAliasElt = nodeAlias.element; + if (nodeAliasElt.equals(element)) { + return true; + } + } + return false; + } + + /** + * Computes @Owning annotations for the parameters passed in the receiver or arguments position of + * a call. + * + * @param obligations set of obligations associated with the current block + * @param invocation a method invocation node to check + */ + private void computeOwningForArgsOrReceiverOfCall( + Set obligations, MethodInvocationNode invocation) { + Node receiver = invocation.getTarget().getReceiver(); + receiver = NodeUtils.removeCasts(receiver); + if (receiver.getTree() != null) { + computeOwningForArgument(obligations, invocation, receiver); + } + + for (Node argument : mcca.getArgumentsOfInvocation(invocation)) { + Node arg = NodeUtils.removeCasts(argument); + // In the CFG, explicit passing of multiple arguments in the varargs position is represented + // via an ArrayCreationNode. In this case, it checks the called methods set of each argument + // passed in this position. + if (arg instanceof ArrayCreationNode) { + ArrayCreationNode varArgsNode = (ArrayCreationNode) arg; + for (Node varArgNode : varArgsNode.getInitializers()) { + computeOwningForArgument(obligations, invocation, varArgNode); + } + } else { + computeOwningForArgument(obligations, invocation, arg); + } + } + } + + /** + * Computes an @Owning annotation for the {@code arg} that can be a receiver or an argument passed + * into a method call. + * + * @param obligations set of obligations associated with the current block + * @param invocation the method invocation node to check + * @param arg a receiver or an argument passed to the method call + */ + private void computeOwningForArgument( + Set obligations, MethodInvocationNode invocation, Node arg) { + Element argElt = TreeUtils.elementFromTree(arg.getTree()); + // The must-call obligation of a field can be satisfied either through a call where it serves as + // a receiver or within the callee method when it is passed as an argument. + if (argElt != null && argElt.getKind().isField()) { + inferOwningField(arg, invocation); + return; + } + + List paramsOfCurrentMethod = methodTree.getParameters(); + outerLoop: + for (int i = 0; i < paramsOfCurrentMethod.size(); i++) { + VariableTree currentMethodParamTree = paramsOfCurrentMethod.get(i); + if (resourceLeakAtf.hasEmptyMustCallValue(currentMethodParamTree)) { + continue; + } + + VariableElement paramElt = TreeUtils.elementFromDeclaration(currentMethodParamTree); + if (!nodeAndElementResourceAliased(obligations, arg, paramElt)) { + continue; + } + + List mustCallValues = resourceLeakAtf.getMustCallValues(paramElt); + // TODO: generalize this method to MustCall annotations with more than one element. + assert mustCallValues.size() <= 1 : "TODO: Handle larger must-call values sets"; + Set nodeAliases = getResourceAliasOfNode(obligations, arg); + for (ResourceAlias resourceAlias : nodeAliases) { + AnnotationMirror cmAnno = getCalledMethodsAnno(invocation, resourceAlias.reference); + if (mcca.calledMethodsSatisfyMustCall(mustCallValues, cmAnno)) { + addOwningToParam(i + 1); + break outerLoop; + } + } + } + } + + /** + * Returns the set of resource aliases associated with the given node, by looking up the + * corresponding obligation in the given set of obligations. + * + * @param obligations the set of obligations to search in + * @param node the node whose resource aliases are to be returned + * @return the resource aliases associated with the given node, or an empty set if the node has + * none + */ + private Set getResourceAliasOfNode(Set obligations, Node node) { + Node tempVar = mcca.getTempVarOrNode(node); + if (!(tempVar instanceof LocalVariableNode)) { + return Collections.emptySet(); + } + + Obligation argumentObligation = + MustCallConsistencyAnalyzer.getObligationForVar(obligations, (LocalVariableNode) tempVar); + if (argumentObligation == null) { + return Collections.emptySet(); + } + return argumentObligation.resourceAliases; + } + + /** + * Infers @Owning annotations for formal parameters of the enclosing method or fields of the + * enclosing class, as follows: + * + *

    + *
  • If a formal parameter is passed as an owning parameter, add an @Owning annotation to that + * formal parameter (see {@link #inferOwningParamsViaOwnershipTransfer}). + *
  • It calls {@link #computeOwningForArgsOrReceiverOfCall} to compute @Owning annotations for + * the receiver or arguments of a call by analyzing the called-methods set after the call. + *
+ * + * @param obligations the set of obligations to search in + * @param invocation the method or constructor invocation + */ + private void computeOwningFromInvocation(Set obligations, Node invocation) { + if (invocation instanceof ObjectCreationNode) { + // If the invocation corresponds to an object creation node, only ownership transfer checking + // is required, as constructor parameters may have an @Owning annotation. We do not handle + // @EnsuresCalledMethods annotations on constructors as we have not observed them in practice. + inferOwningParamsViaOwnershipTransfer(obligations, invocation); + } else if (invocation instanceof MethodInvocationNode) { + inferOwningParamsViaOwnershipTransfer(obligations, invocation); + computeOwningForArgsOrReceiverOfCall(obligations, (MethodInvocationNode) invocation); + } + } - successorBlock.add(ccur.getThenSuccessor()); - successorBlock.add(ccur.getElseSuccessor()); + /** + * Returns the called methods annotation for the given Java expression after the invocation node. + * + * @param invocation the MethodInvocationNode + * @param varJe a Java expression + * @return the called methods annotation for the {@code varJe} after the {@code invocation} node. + */ + private AnnotationMirror getCalledMethodsAnno( + MethodInvocationNode invocation, JavaExpression varJe) { + AccumulationStore cmStoreAfter = resourceLeakAtf.getStoreAfter(invocation); + AccumulationValue cmValue = cmStoreAfter == null ? null : cmStoreAfter.getValue(varJe); - } else { - if (!(cur instanceof SingleSuccessorBlock)) { - throw new BugInCF("BlockImpl is neither a conditional block nor a SingleSuccessorBlock"); + AnnotationMirror cmAnno = null; + + if (cmValue != null) { + // The store contains the lhs. + Set accumulatedValues = cmValue.getAccumulatedValues(); + if (accumulatedValues != null) { // type variable or wildcard type + cmAnno = resourceLeakAtf.createCalledMethods(accumulatedValues.toArray(new String[0])); + } else { + for (AnnotationMirror anno : cmValue.getAnnotations()) { + if (AnnotationUtils.areSameByName( + anno, "org.checkerframework.checker.calledmethods.qual.CalledMethods")) { + cmAnno = anno; + } + } } + } + + if (cmAnno == null) { + cmAnno = resourceLeakAtf.top; + } + + return cmAnno; + } + + /** + * Adds all non-exceptional successors to {@code worklist}. + * + * @param obligations the obligations for the current block + * @param curBlock the block whose successors to add to the worklist + * @param visited block-Obligations pairs already analyzed or already on the worklist + * @param worklist the worklist, which is side-effected by this method + */ + private void addNonExceptionalSuccessorsToWorklist( + Set obligations, + Block curBlock, + Set visited, + Deque worklist) { - Block b = ((SingleSuccessorBlock) cur).getSuccessor(); - if (b != null) { - successorBlock.add(b); + for (Block successor : getNonExceptionalSuccessors(curBlock)) { + // If successor is a special block, it must be the regular exit. + if (successor.getType() != Block.BlockType.SPECIAL_BLOCK) { + BlockWithObligations state = new BlockWithObligations(successor, obligations); + if (visited.add(state)) { + worklist.add(state); + } } } - return successorBlock; + } + + /** + * Returns the non-exceptional successors of a block. + * + * @param cur a block + * @return the successors of the given block + */ + private List getNonExceptionalSuccessors(Block cur) { + if (cur.getType() == Block.BlockType.CONDITIONAL_BLOCK) { + ConditionalBlock ccur = (ConditionalBlock) cur; + return Arrays.asList(ccur.getThenSuccessor(), ccur.getElseSuccessor()); + } + if (!(cur instanceof SingleSuccessorBlock)) { + throw new BugInCF("Not a conditional block nor a SingleSuccessorBlock: " + cur); + } + + Block successor = ((SingleSuccessorBlock) cur).getSuccessor(); + if (successor != null) { + return Collections.singletonList(successor); + } + return Collections.emptyList(); + } + + /** + * Creates an {@code @EnsuresCalledMethods} annotation with the given arguments. + * + * @param value the expressions that will have methods called on them + * @param methods the methods guaranteed to be invoked on the expressions + * @return an {@code @EnsuresCalledMethods} annotation with the given arguments + */ + private AnnotationMirror createEnsuresCalledMethods(String[] value, String[] methods) { + AnnotationBuilder builder = + new AnnotationBuilder(resourceLeakAtf.getProcessingEnv(), EnsuresCalledMethods.class); + builder.setValue("value", value); + builder.setValue("methods", methods); + AnnotationMirror am = builder.build(); + return am; + } + + /** + * Creates an {@code @InheritableMustCall} annotation with the given arguments. + * + * @param methods methods that might need to be called on the expression whose type is annotated + * @return an {@code @InheritableMustCall} annotation with the given arguments + */ + private AnnotationMirror createInheritableMustCall(String[] methods) { + AnnotationBuilder builder = + new AnnotationBuilder(resourceLeakAtf.getProcessingEnv(), InheritableMustCall.class); + Arrays.sort(methods); + builder.setValue("value", methods); + return builder.build(); } } diff --git a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakAnnotatedTypeFactory.java index d6dba3590c0..e8b16023e6a 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakAnnotatedTypeFactory.java @@ -36,7 +36,6 @@ import org.checkerframework.framework.type.AnnotatedTypeMirror; import org.checkerframework.framework.type.GenericAnnotatedTypeFactory; import org.checkerframework.javacutil.AnnotationUtils; -import org.checkerframework.javacutil.ElementUtils; import org.checkerframework.javacutil.TreeUtils; import org.checkerframework.javacutil.TypeSystemError; @@ -103,16 +102,14 @@ public ResourceLeakAnnotatedTypeFactory(BaseTypeChecker checker) { } /** - * Is the given element a candidate to be an owning field? A candidate owning field must be final - * and have a non-empty must-call obligation. + * Is the given element a candidate to be an owning field? A candidate owning field must have a + * non-empty must-call obligation. * * @param element a element - * @return true iff the given element is a final field with non-empty @MustCall obligation + * @return true iff the given element is a field with non-empty @MustCall obligation */ - /*package-private*/ boolean isCandidateOwningField(Element element) { - return (element.getKind().isField() - && ElementUtils.isFinal(element) - && !hasEmptyMustCallValue(element)); + /*package-private*/ boolean isFieldWithNonemptyMustCallValue(Element element) { + return element.getKind().isField() && !hasEmptyMustCallValue(element); } @Override @@ -137,11 +134,11 @@ public void postAnalyze(ControlFlowGraph cfg) { new MustCallConsistencyAnalyzer(this, (ResourceLeakAnalysis) this.analysis); mustCallConsistencyAnalyzer.analyze(cfg); - // Inferring owning annotations for final owning fields + // Inferring owning annotations for @Owning fields/parameters, @EnsuresCalledMethods for + // finalizer methods and @InheritableMustCall annotations for the class declarations. if (getWholeProgramInference() != null) { if (cfg.getUnderlyingAST().getKind() == UnderlyingAST.Kind.METHOD) { - MustCallInference mustCallInferenceLogic = new MustCallInference(this, cfg); - mustCallInferenceLogic.runInference(); + MustCallInference.runMustCallInference(this, cfg, mustCallConsistencyAnalyzer); } } @@ -221,7 +218,7 @@ protected ResourceLeakAnalysis createFlowAnalysis() { * @param element an element * @return the strings in its must-call type */ - /*package-private*/ List getMustCallValue(Element element) { + /*package-private*/ List getMustCallValues(Element element) { MustCallAnnotatedTypeFactory mustCallAnnotatedTypeFactory = getTypeFactoryOfSubchecker(MustCallChecker.class); AnnotatedTypeMirror mustCallAnnotatedType = diff --git a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakChecker.java b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakChecker.java index 1bdddc3bb62..d26819bfd4a 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakChecker.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakChecker.java @@ -33,7 +33,8 @@ ResourceLeakChecker.IGNORED_EXCEPTIONS, MustCallChecker.NO_CREATES_MUSTCALLFOR, MustCallChecker.NO_LIGHTWEIGHT_OWNERSHIP, - MustCallChecker.NO_RESOURCE_ALIASES + MustCallChecker.NO_RESOURCE_ALIASES, + ResourceLeakChecker.ENABLE_WPI_FOR_RLC, }) @StubFiles("IOUtils.astub") public class ResourceLeakChecker extends CalledMethodsChecker { @@ -105,6 +106,15 @@ public ResourceLeakChecker() {} Pattern.compile( "^\\s*" + "(" + Pattern.quote("=") + "\\s*" + ")?" + "(\\w+(?:\\.\\w+)*)" + "\\s*$"); + /** + * Ordinarily, when the -Ainfer flag is used, whole-program inference is run for every checker and + * sub-checker. However, the Resource Leak Checker is different. The -Ainfer flag enables the + * RLC's own (non-WPI) inference mechanism ({@link MustCallInference}). To use WPI in addition to + * this mechanism for its sub-checkers, use the -AenableWpiForRlc flag, which is intended only for + * testing and experiments. + */ + public static final String ENABLE_WPI_FOR_RLC = "enableWpiForRlc"; + /** * The number of expressions with must-call obligations that were checked. Incremented only if the * {@link #COUNT_MUST_CALL} command-line option was supplied. diff --git a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakVisitor.java b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakVisitor.java index b3df56f9b3b..be36474ea9a 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakVisitor.java @@ -50,6 +50,12 @@ public class ResourceLeakVisitor extends CalledMethodsVisitor { /** True if -AnoLightweightOwnership was supplied on the command line. */ private final boolean noLightweightOwnership; + /** + * True if -AenableWpiForRlc was passed on the command line. See {@link + * ResourceLeakChecker#ENABLE_WPI_FOR_RLC}. + */ + private final boolean enableWpiForRlc; + /** * Create the visitor. * @@ -60,6 +66,7 @@ public ResourceLeakVisitor(BaseTypeChecker checker) { rlTypeFactory = (ResourceLeakAnnotatedTypeFactory) atypeFactory; permitStaticOwning = checker.hasOption("permitStaticOwning"); noLightweightOwnership = checker.hasOption("noLightweightOwnership"); + enableWpiForRlc = checker.hasOption(ResourceLeakChecker.ENABLE_WPI_FOR_RLC); } @Override @@ -188,6 +195,11 @@ private void checkOwningOverrides( } } + @Override + protected boolean shouldPerformContractInference() { + return atypeFactory.getWholeProgramInference() != null && isWpiEnabledForRLC(); + } + // Overwritten to check that destructors (i.e. methods responsible for resolving // the must-call obligations of owning fields) enforce a stronger version of // @EnsuresCalledMethods: that the claimed @CalledMethods annotation is true on @@ -381,7 +393,7 @@ private void checkOwningField(Element field) { // This value is side-effected. List unsatisfiedMustCallObligationsOfOwningField = - rlTypeFactory.getMustCallValue(field); + rlTypeFactory.getMustCallValues(field); if (unsatisfiedMustCallObligationsOfOwningField.isEmpty()) { return; @@ -389,7 +401,7 @@ private void checkOwningField(Element field) { String error; Element enclosingElement = field.getEnclosingElement(); - List enclosingMustCallValues = rlTypeFactory.getMustCallValue(enclosingElement); + List enclosingMustCallValues = rlTypeFactory.getMustCallValues(enclosingElement); if (enclosingMustCallValues == null) { error = @@ -454,4 +466,14 @@ private void checkOwningField(Element field) { error); } } + + /** + * Checks if WPI is enabled for the Resource Leak Checker inference. See {@link + * ResourceLeakChecker#ENABLE_WPI_FOR_RLC}. + * + * @return returns true if WPI is enabled for the Resource Leak Checker + */ + protected boolean isWpiEnabledForRLC() { + return enableWpiForRlc; + } } diff --git a/checker/tests/ainfer-resourceleak/non-annotated/ECMInference.java b/checker/tests/ainfer-resourceleak/non-annotated/ECMInference.java index e5e9353d766..7fecb377aa4 100644 --- a/checker/tests/ainfer-resourceleak/non-annotated/ECMInference.java +++ b/checker/tests/ainfer-resourceleak/non-annotated/ECMInference.java @@ -1,3 +1,6 @@ +// @skip-test the test contains no resource types to infer. +// To pass this test, RLC's inference needs to infer CalledMethods annotations for empty must-call +// types, which requires the -AenableWpirForRLC flag. import org.checkerframework.checker.calledmethods.qual.CalledMethods; public class ECMInference { diff --git a/checker/tests/ainfer-resourceleak/non-annotated/EnsuresCalledMethodsTest.java b/checker/tests/ainfer-resourceleak/non-annotated/EnsuresCalledMethodsTest.java new file mode 100644 index 00000000000..65c1fb5cf4b --- /dev/null +++ b/checker/tests/ainfer-resourceleak/non-annotated/EnsuresCalledMethodsTest.java @@ -0,0 +1,29 @@ +import org.checkerframework.checker.calledmethods.qual.*; +import org.checkerframework.checker.mustcall.qual.*; + +class EnsuresCalledMethodsTest { + @InheritableMustCall("a") + static class Foo { + void a() {} + } + + @InheritableMustCall("close") + class ECM { + // :: warning: (required.method.not.called) + @Owning Foo foo; + + private void closePrivate() { + if (foo != null) { + foo.a(); + foo = null; + } + } + + void close() { + if (foo != null) { + foo.a(); + foo = null; + } + } + } +} diff --git a/checker/tests/ainfer-resourceleak/non-annotated/EnsuresCalledMethodsVarArgsTest.java b/checker/tests/ainfer-resourceleak/non-annotated/EnsuresCalledMethodsVarArgsTest.java new file mode 100644 index 00000000000..a8ebf5b0fea --- /dev/null +++ b/checker/tests/ainfer-resourceleak/non-annotated/EnsuresCalledMethodsVarArgsTest.java @@ -0,0 +1,60 @@ +import org.checkerframework.checker.calledmethods.qual.*; +import org.checkerframework.checker.mustcall.qual.*; + +class EnsuresCalledMethodsVarArgsTest { + + @InheritableMustCall("a") + static class Foo { + void a() {} + } + + static class Utils { + @SuppressWarnings("ensuresvarargs.unverified") + @EnsuresCalledMethodsVarArgs("a") + public static void close(Foo... foos) { + for (Foo f : foos) { + if (f != null) { + f.a(); + } + } + } + } + + private class ECMVA { + final Foo foo; + + ECMVA() { + // :: warning: (required.method.not.called) + foo = new Foo(); + } + + void finalyzer() { + Utils.close(foo); + } + + @EnsuresCalledMethods( + value = {"#1"}, + methods = {"a"}) + void closef(Foo f) { + if (f != null) { + Utils.close(f); + } + } + + void owningParam(Foo f) { + Foo foo = f; + Utils.close(foo); + } + + void testOwningParamOnOwningParam() { + // :: warning: (required.method.not.called) + Foo f = new Foo(); + owningParam(f); + } + } + + void testCorrect() { + ECMVA e = new ECMVA(); + e.finalyzer(); + } +} diff --git a/checker/tests/ainfer-resourceleak/non-annotated/OwnershipTransferOnConstructor.java b/checker/tests/ainfer-resourceleak/non-annotated/OwnershipTransferOnConstructor.java new file mode 100644 index 00000000000..96b4382db38 --- /dev/null +++ b/checker/tests/ainfer-resourceleak/non-annotated/OwnershipTransferOnConstructor.java @@ -0,0 +1,28 @@ +import java.io.IOException; +import java.net.*; +import org.checkerframework.checker.calledmethods.qual.*; +import org.checkerframework.checker.mustcall.qual.*; + +class OwnershipTransferOnConstructor { + static class Foo { + Foo(@Owning Socket s) { + try { + s.close(); + } catch (IOException e) { + + } + } + } + + private class Bar { + void baz(Socket s) { + Foo f = new Foo(s); + } + + // :: warning: (required.method.not.called) + void testOwningOnBaz(@Owning Socket s) { + Socket s2 = s; + baz(s2); + } + } +} diff --git a/checker/tests/ainfer-resourceleak/non-annotated/OwningFieldIndirectCall.java b/checker/tests/ainfer-resourceleak/non-annotated/OwningFieldIndirectCall.java new file mode 100644 index 00000000000..7c2c542e9b7 --- /dev/null +++ b/checker/tests/ainfer-resourceleak/non-annotated/OwningFieldIndirectCall.java @@ -0,0 +1,37 @@ +import org.checkerframework.checker.calledmethods.qual.*; +import org.checkerframework.checker.mustcall.qual.*; + +class OwningFieldIndirectCall { + + @InheritableMustCall("a") + static class Foo { + void a() {} + } + + static class Utility { + @EnsuresCalledMethods(value = "#1", methods = "a") + public static void closeStream(Foo f) { + if (f != null) { + f.a(); + } + } + } + + static class DisposeFieldUsingECM { + final Foo f; // expect owning annotation for this field + + DisposeFieldUsingECM() { + // :: warning: (required.method.not.called) + f = new Foo(); + } + + void dispose() { + Utility.closeStream(f); + } + } + + void testCorrect() { + DisposeFieldUsingECM d = new DisposeFieldUsingECM(); + d.dispose(); + } +} diff --git a/checker/tests/ainfer-resourceleak/non-annotated/OwningParams.java b/checker/tests/ainfer-resourceleak/non-annotated/OwningParams.java new file mode 100644 index 00000000000..1c1cd29eeef --- /dev/null +++ b/checker/tests/ainfer-resourceleak/non-annotated/OwningParams.java @@ -0,0 +1,60 @@ +import org.checkerframework.checker.calledmethods.qual.*; +import org.checkerframework.checker.mustcall.qual.*; + +class OwningParams { + @InheritableMustCall("a") + static class Foo { + void a() {} + } + + private class OwningParamsDirectCall { + void passOwnership(Foo f) { + f.a(); + } + + void passOwnershipTest() { + // :: warning: (required.method.not.called) + Foo f = new Foo(); + passOwnership(f); + } + } + + private class OwningParamsIndirectCall { + @EnsuresCalledMethods( + value = {"#1"}, + methods = {"a"}) + void hasECM(Foo f) { + f.a(); + } + + void owningFoo(@Owning Foo f) { + f.a(); + } + + void passOwnership(Foo f1, Foo f2) { + Foo f11 = f1; + hasECM(f11); + Foo f22 = f2; + owningFoo(f22); + } + + void checkAlias(Foo f1) { + Foo f2 = f1; + f2.a(); + } + + void checkAliasTest() { + // :: warning: (required.method.not.called) + Foo f = new Foo(); + checkAlias(f); + } + + void passOwnershipTest() { + // :: warning: (required.method.not.called) + Foo f1 = new Foo(); + // :: warning: (required.method.not.called) + Foo f2 = new Foo(); + passOwnership(f1, f2); + } + } +} diff --git a/checker/tests/calledmethods/EnsuresCalledMethodsIfRepeatable.java b/checker/tests/calledmethods/EnsuresCalledMethodsIfRepeatable.java new file mode 100644 index 00000000000..10b9990b3a8 --- /dev/null +++ b/checker/tests/calledmethods/EnsuresCalledMethodsIfRepeatable.java @@ -0,0 +1,53 @@ +import java.io.*; +import org.checkerframework.checker.calledmethods.qual.EnsuresCalledMethodsIf; + +public class EnsuresCalledMethodsIfRepeatable { + + @EnsuresCalledMethodsIf(expression = "#1", result = true, methods = "close") + @EnsuresCalledMethodsIf(expression = "#2", result = true, methods = "close") + public boolean close2MissingFirst(Closeable r1, Closeable r2) throws IOException { + r1.close(); + // ::error: (contracts.conditional.postcondition) + return true; + } + + @EnsuresCalledMethodsIf(expression = "#1", result = true, methods = "close") + @EnsuresCalledMethodsIf(expression = "#2", result = true, methods = "close") + public boolean close2MissingSecond(Closeable r1, Closeable r2) throws IOException { + r2.close(); + // ::error: (contracts.conditional.postcondition) + return true; + } + + @EnsuresCalledMethodsIf(expression = "#1", result = true, methods = "close") + @EnsuresCalledMethodsIf(expression = "#2", result = true, methods = "close") + public boolean close2Correct(Closeable r1, Closeable r2) throws IOException { + try { + r1.close(); + } finally { + r2.close(); + } + return true; + } + + @EnsuresCalledMethodsIf(expression = "#1", result = true, methods = "close") + @EnsuresCalledMethodsIf(expression = "#2", result = true, methods = "close") + public boolean close2CorrectViaCall(Closeable r1, Closeable r2) throws IOException { + return close2Correct(r1, r2); + } + + public static class SubclassWrong extends EnsuresCalledMethodsIfRepeatable { + @Override + public boolean close2Correct(Closeable r1, Closeable r2) throws IOException { + // ::error: (contracts.conditional.postcondition) + return true; + } + } + + public static class SubclassRight extends EnsuresCalledMethodsIfRepeatable { + @Override + public boolean close2Correct(Closeable r1, Closeable r2) throws IOException { + return false; + } + } +} diff --git a/checker/tests/calledmethods/EnsuresCalledMethodsIfSubclass.java b/checker/tests/calledmethods/EnsuresCalledMethodsIfSubclass.java new file mode 100644 index 00000000000..fff666b8c04 --- /dev/null +++ b/checker/tests/calledmethods/EnsuresCalledMethodsIfSubclass.java @@ -0,0 +1,28 @@ +import java.io.*; +import org.checkerframework.checker.calledmethods.qual.EnsuresCalledMethodsIf; + +public class EnsuresCalledMethodsIfSubclass { + + public static class Parent { + @EnsuresCalledMethodsIf(expression = "#1", result = true, methods = "close") + public boolean method(Closeable x) throws IOException { + x.close(); + return true; + } + } + + public static class SubclassWrong extends Parent { + @Override + public boolean method(Closeable x) throws IOException { + // ::error: (contracts.conditional.postcondition) + return true; + } + } + + public static class SubclassRight extends Parent { + @Override + public boolean method(Closeable x) throws IOException { + return false; + } + } +} diff --git a/checker/tests/calledmethods/EnsuresCalledMethodsRepeatable.java b/checker/tests/calledmethods/EnsuresCalledMethodsRepeatable.java index 715354e8cb8..800ca64f6ef 100644 --- a/checker/tests/calledmethods/EnsuresCalledMethodsRepeatable.java +++ b/checker/tests/calledmethods/EnsuresCalledMethodsRepeatable.java @@ -1,3 +1,4 @@ +import java.io.*; import org.checkerframework.checker.calledmethods.qual.EnsuresCalledMethods; class EnsuresCalledMethodsRepeatable { @@ -12,4 +13,40 @@ void test(Object obj) { obj.toString(); obj.hashCode(); } + + @EnsuresCalledMethods(value = "#1", methods = "close") + @EnsuresCalledMethods(value = "#2", methods = "close") + // ::error: (contracts.postcondition) + public void close2MissingFirst(Closeable r1, Closeable r2) throws IOException { + r1.close(); + } + + @EnsuresCalledMethods(value = "#1", methods = "close") + @EnsuresCalledMethods(value = "#2", methods = "close") + // ::error: (contracts.postcondition) + public void close2MissingSecond(Closeable r1, Closeable r2) throws IOException { + r2.close(); + } + + @EnsuresCalledMethods(value = "#1", methods = "close") + @EnsuresCalledMethods(value = "#2", methods = "close") + public void close2Correct(Closeable r1, Closeable r2) throws IOException { + try { + r1.close(); + } finally { + r2.close(); + } + } + + @EnsuresCalledMethods(value = "#1", methods = "close") + @EnsuresCalledMethods(value = "#2", methods = "close") + public void close2CorrectViaCall(Closeable r1, Closeable r2) throws IOException { + close2Correct(r1, r2); + } + + public static class Subclass extends EnsuresCalledMethodsRepeatable { + @Override + // ::error: (contracts.postcondition) + public void close2Correct(Closeable r1, Closeable r2) throws IOException {} + } } diff --git a/checker/tests/calledmethods/EnsuresCalledMethodsSubclass.java b/checker/tests/calledmethods/EnsuresCalledMethodsSubclass.java new file mode 100644 index 00000000000..028ba38e428 --- /dev/null +++ b/checker/tests/calledmethods/EnsuresCalledMethodsSubclass.java @@ -0,0 +1,18 @@ +import java.io.*; +import org.checkerframework.checker.calledmethods.qual.EnsuresCalledMethods; + +public class EnsuresCalledMethodsSubclass { + + public static class Parent { + @EnsuresCalledMethods(value = "#1", methods = "close") + public void method(Closeable x) throws IOException { + x.close(); + } + } + + public static class Subclass extends Parent { + @Override + // ::error: (contracts.postcondition) + public void method(Closeable x) throws IOException {} + } +} diff --git a/checker/tests/calledmethods/RequiresCalledMethodsRepeatable.java b/checker/tests/calledmethods/RequiresCalledMethodsRepeatable.java new file mode 100644 index 00000000000..c24e529e5d2 --- /dev/null +++ b/checker/tests/calledmethods/RequiresCalledMethodsRepeatable.java @@ -0,0 +1,32 @@ +import java.io.*; +import org.checkerframework.checker.calledmethods.qual.*; + +public class RequiresCalledMethodsRepeatable { + + @RequiresCalledMethods(value = "#1", methods = "close") + @RequiresCalledMethods(value = "#2", methods = "close") + public void requires2(Closeable r1, Closeable r2) { + @CalledMethods("close") Closeable r3 = r1; + @CalledMethods("close") Closeable r4 = r2; + } + + public void requires2Wrong(Closeable r1, Closeable r2) { + // ::error: (contracts.precondition) + requires2(r1, r2); + } + + @RequiresCalledMethods(value = "#1", methods = "close") + @RequiresCalledMethods(value = "#2", methods = "close") + public void requires2Correct(Closeable r1, Closeable r2) { + requires2(r1, r2); + } + + public static class Subclass extends RequiresCalledMethodsRepeatable { + @Override + public void requires2Correct(Closeable r1, Closeable r2) {} + + public void caller(Closeable r1, Closeable r2) { + requires2Correct(r1, r2); // OK: we override requires2Correct() with a weaker precondition + } + } +} diff --git a/checker/tests/calledmethods/RequiresCalledMethodsSubclass.java b/checker/tests/calledmethods/RequiresCalledMethodsSubclass.java new file mode 100644 index 00000000000..9b8eaabcc30 --- /dev/null +++ b/checker/tests/calledmethods/RequiresCalledMethodsSubclass.java @@ -0,0 +1,24 @@ +import java.io.*; +import org.checkerframework.checker.calledmethods.qual.RequiresCalledMethods; + +public class RequiresCalledMethodsSubclass { + + public static class Parent { + @RequiresCalledMethods(value = "#1", methods = "close") + public void method(Closeable x) throws IOException {} + + public void caller(Closeable x) throws IOException { + // ::error: (contracts.precondition) + method(x); + } + } + + public static class Subclass extends Parent { + @Override + public void method(Closeable x) throws IOException {} + + public void caller(Closeable x) throws IOException { + method(x); // OK: we override method() with a weaker precondition + } + } +} diff --git a/checker/tests/index/SameLenIrrelevant.java b/checker/tests/index/SameLenIrrelevant.java index b440dbaca30..c59ceefe46a 100644 --- a/checker/tests/index/SameLenIrrelevant.java +++ b/checker/tests/index/SameLenIrrelevant.java @@ -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 } diff --git a/checker/tests/nullness/Exceptions.java b/checker/tests/nullness/Exceptions.java index 571a5781e59..c5175034aa1 100644 --- a/checker/tests/nullness/Exceptions.java +++ b/checker/tests/nullness/Exceptions.java @@ -12,9 +12,8 @@ void nonnullExceptionParam(@NonNull Exception m) { void exception(@Nullable Exception m) { try { - + throwException(); } catch (Exception e) { - // Note that this code is dead. e.getClass(); // :: error: (dereference.of.nullable) m.getClass(); // should emit error @@ -38,8 +37,8 @@ void throwException() { void reassignException() { try { + throwException(); } catch (RuntimeException e) { - // Note that this code is dead. // :: error: (assignment) e = null; throw e; diff --git a/checker/tests/nullness/Issue6260.java b/checker/tests/nullness/Issue6260.java new file mode 100644 index 00000000000..d7395cc7c0b --- /dev/null +++ b/checker/tests/nullness/Issue6260.java @@ -0,0 +1,18 @@ +public class Issue6260 { + enum MyE { + FOO; + + MyE getIt() { + return FOO; + } + + String go() { + MyE e = getIt(); + switch (e) { + case FOO: + return "foo"; + } + throw new AssertionError(e); + } + } +} diff --git a/checker/tests/nullness/TryCatch.java b/checker/tests/nullness/TryCatch.java index e6ddbb6362c..8411ddcd1e1 100644 --- a/checker/tests/nullness/TryCatch.java +++ b/checker/tests/nullness/TryCatch.java @@ -23,7 +23,6 @@ void unreachableCatch(String[] xs) { try { } catch (Throwable e) { // Note that this code is dead. - // :: error: (dereference.of.nullable) t.toString(); } } diff --git a/checker/tests/optional/JdkCheck.java b/checker/tests/optional/JdkCheck.java index 39277041e05..fbef1974c01 100644 --- a/checker/tests/optional/JdkCheck.java +++ b/checker/tests/optional/JdkCheck.java @@ -21,12 +21,10 @@ String orElseThrowTest1( } String orElseThrowTest2(Optional mos, Supplier exceptionSupplier) { - // :: error: (method.invocation) return mos.orElseThrow(exceptionSupplier); } String orElseThrowTestFlow(Optional mos, Supplier exceptionSupplier) { - // :: error: (method.invocation) mos.orElseThrow(exceptionSupplier); return mos.get(); } diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/ControlFlowGraph.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/ControlFlowGraph.java index b94b657044a..d122d1a7dc7 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/ControlFlowGraph.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/ControlFlowGraph.java @@ -20,6 +20,8 @@ import java.util.Set; import java.util.StringJoiner; import java.util.concurrent.atomic.AtomicLong; +import java.util.function.Function; +import javax.lang.model.type.TypeMirror; import org.checkerframework.checker.initialization.qual.UnknownInitialization; import org.checkerframework.checker.nullness.qual.Nullable; import org.checkerframework.dataflow.analysis.AnalysisResult; @@ -28,6 +30,7 @@ import org.checkerframework.dataflow.cfg.block.ExceptionBlock; import org.checkerframework.dataflow.cfg.block.RegularBlock; import org.checkerframework.dataflow.cfg.block.SingleSuccessorBlock; +import org.checkerframework.dataflow.cfg.block.SingleSuccessorBlockImpl; import org.checkerframework.dataflow.cfg.block.SpecialBlock; import org.checkerframework.dataflow.cfg.block.SpecialBlockImpl; import org.checkerframework.dataflow.cfg.node.Node; @@ -276,6 +279,74 @@ public List getAllNodes( return result; } + /** + * Returns the set of all basic blocks in this control flow graph, except those that are + * only reachable via an exception whose type is ignored by parameter {@code + * shouldIgnoreException}. + * + * @param shouldIgnoreException returns true if it is passed a {@code TypeMirror} that should be + * ignored + * @return the set of all basic blocks in this control flow graph, except those that are + * only reachable via an exception whose type is ignored by {@code shouldIgnoreException} + */ + public Set getAllBlocks( + @UnknownInitialization(ControlFlowGraph.class) ControlFlowGraph this, + Function shouldIgnoreException) { + // This is the return value of the method. + Set visited = new LinkedHashSet<>(); + // `worklist` is always a subset of `visited`; any block in `worklist` is also in `visited`. + Queue worklist = new ArrayDeque<>(); + Block cur = entryBlock; + visited.add(entryBlock); + + // Traverse the whole control flow graph. + while (cur != null) { + if (cur instanceof ExceptionBlock) { + for (Map.Entry> entry : + ((ExceptionBlock) cur).getExceptionalSuccessors().entrySet()) { + if (!shouldIgnoreException.apply(entry.getKey())) { + for (Block b : entry.getValue()) { + if (visited.add(b)) { + worklist.add(b); + } + } + } + } + Block b = ((SingleSuccessorBlockImpl) cur).getSuccessor(); + if (b != null && visited.add(b)) { + worklist.add(b); + } + + } else { + for (Block b : cur.getSuccessors()) { + if (visited.add(b)) { + worklist.add(b); + } + } + } + cur = worklist.poll(); + } + + return visited; + } + + /** + * Returns the list of all nodes in this control flow graph, except those that are only + * reachable via an exception whose type is ignored by parameter {@code shouldIgnoreException}. + * + * @param shouldIgnoreException returns true if it is passed a {@code TypeMirror} that should be + * ignored + * @return the list of all nodes in this control flow graph, except those that are only + * reachable via an exception whose type is ignored by {@code shouldIgnoreException} + */ + public List getAllNodes( + @UnknownInitialization(ControlFlowGraph.class) ControlFlowGraph this, + Function shouldIgnoreException) { + List result = new ArrayList<>(); + getAllBlocks(shouldIgnoreException).forEach(b -> result.addAll(b.getNodes())); + return result; + } + /** * Returns all basic blocks in this control flow graph, in reversed depth-first postorder. Blocks * may appear more than once in the sequence. diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md index 7367bfa04a4..e854c37f4b8 100644 --- a/docs/CHANGELOG.md +++ b/docs/CHANGELOG.md @@ -1,3 +1,16 @@ +Version 3.40.0 (November 1, 2023) +--------------------------------- + +**User-visible changes:** + +Optional Checker: `checker-qual.jar` defines `OptionalUtil.castPresent()` for +suppressing false positive warnings from the Optional Checker. + +**Implementation details:** + +**Closed issues:** + + Version 3.39.0 (October 2, 2023) -------------------------------- diff --git a/docs/examples/MavenExample/pom.xml b/docs/examples/MavenExample/pom.xml index f6bdbdbdde3..df589f40edc 100644 --- a/docs/examples/MavenExample/pom.xml +++ b/docs/examples/MavenExample/pom.xml @@ -68,7 +68,7 @@ maven-compiler-plugin - 3.10.1 + 3.11.0 true diff --git a/docs/manual/annotating-libraries.tex b/docs/manual/annotating-libraries.tex index f0a8c3d0d61..35233c8282a 100644 --- a/docs/manual/annotating-libraries.tex +++ b/docs/manual/annotating-libraries.tex @@ -439,7 +439,7 @@ can be read by the Checker Framework. This section describes stub files, which are used by programmers and type system designers. -Section~\ref{ajava-files} dscribes ajava files, which are used by +Section~\ref{ajava-files} describes ajava files, which are used by tools, such as type inference. @@ -585,9 +585,10 @@ \subsectionAndLabel{Stub file format}{stub-format} Every Java file is a valid stub file. However, you can omit information -that is not relevant to pluggable type-checking; this makes the stub file +that is not relevant to pluggable type-checking, as explained below; +this makes the stub file smaller and easier for people to read and write. -Also note that the stub file's extension must be \<.astub>, not \<.java>. +The stub file's extension must be \<.astub>, not \<.java>. As an illustration, a stub file for the Interning type system (Chapter~\ref{interning-checker}) could be: @@ -613,8 +614,9 @@ \item{\textbf{Method declarations:}} You only have to specify the methods that you need to annotate. Any method declaration may be omitted, in which case the checker reads - its annotations from library's \<.class> files. (If you are using a stub class, then - typically the library is unannotated.) + its annotations from library's \<.class> files. If you are using a stub class, then + often the library is unannotated, but you can use stub files to override + library annotations. \item{\textbf{Declaration specifiers:}} Declaration specifiers (e.g., \, \, \) @@ -625,19 +627,29 @@ In particular, it is valid to use \ for every method. This simplifies the creation of stub files. -\item{\textbf{Import statements:}} - Imports may appear at the beginning of the file or after any package declaration. - The only required import statements are the ones to import type - annotations. Import statements for types are optional. - \item{\textbf{Multiple classes and packages:}} The stub file format permits having multiple classes and packages. The packages are separated by a package statement: \. Each package declaration may occur only once; in other words, all classes from a package must appear together. +\item{\textbf{Import statements:}} + Imports may appear at the beginning of the file or after any package declaration. + The only required import statements are the ones to import type + annotations. Import statements for types are optional. If you omit an + import statement for an annotation, occurrences of that annotation are + silently ignored; this is a common error in stub files. + \end{description} +When you create a stub file, it is recommended that validate it by copying +the stub file to a file with the \<.java> extension and running the +type-checker. This will ensure that your annotations are syntactically +valid, are written in the correct locations, and are properly imported. +When you run the type-checker on your annotations, there should not be any +stub file that also contains annotations for the class. In particular, if +you are type-checking a stub file for a class in the JDK, then you should +use the\<-Aignorejdkastub> command-line option. \subsectionAndLabel{Creating a stub file}{stub-creating} @@ -651,26 +663,21 @@ The stub file parser silently ignores any annotations that it cannot resolve to a type, so don't forget the \ statement. -Optionally (but highly recommended!), run the type-checker to verify that -your annotations are correct. When you run the type-checker on your -annotations, there should not be any stub file that also contains -annotations for the class. In particular, if you are type-checking the JDK -itself, then you should use the \<-Aignorejdkastub> command-line option. - -This approach retains the original +This copy-and-annotate approach retains the original documentation and source code, making it easier for a programmer to double-check the annotations. It also enables creation of diffs, easing the process of upgrading when a library adds new methods. And, the annotations are in a format that the library maintainers can even incorporate. -The downside of this approach is that the stub files are larger. This can +The downside of the copy-and-annotate approach is that the stub files are +larger. This can slow down the Checker Framework, because it parses the stub files each time it runs. % Furthermore, a programmer must search the stub file % for a given method rather than just skimming a few pages of method signatures. -Alternatively, you can minimize source files to make them more suitable as stub files. +You can minimize source files to speed up parsing them. Use the \ to convert, in-place, all \<.java> files in given directories into minimal stub files. @@ -696,6 +703,49 @@ % That file will contain many non-unique import statements, but that shouldn't be harmful. +\subsubsectionAndLabel{If you do not have access to the Java source code}{stub-creating-without-source} + +If you do not have access to the library source code, you can create a stub +file by hand. + +If you have access to the API documentation for the element you wish to +annotate, it is often easiest to copy--paste names, types, and signatures +from the API documentation. (The API documentation is a \<.html> file that +is sometimes colloquially called the ``Javadoc''.) This avoids common +mistakes when writing stub files by hand, such as typos in the package name +or in a method signature. + + +Here are steps to write a stub file by hand: +\begin{enumerate} +\item Create a file whose name ends in \<.astub>, or use an existing one. +\item Write a package declaration, exactly as if you are +writing a Java file for the target class. (If the file already contains a +declaration for that package, re-use it by doing the rest of your work +under it; don't write a duplicate package declaration in the file.) +Typically, it is easiest to copy--paste the package name from API +documentation or from an import statement in the code that you are +type-checking, to avoid typos. +\item Write a class declaration header: \ followed by the +class name. The stub file format does not care whether the enclosing type +is a class, interface, etc., so you can write ``\'' regardless of +what kind of type it is. + +A common mistake at this stage is that the +target method or field may be defined in a superclass of the static type of +the class that is actually being used in the code you are trying to +analyze. For example, suppose that you are trying to annotate the +\ method of an object whose static +type is \\@. This method is actually defined in the abstract +\ class (which is the superclass of \), so it needs +to appear within the class \ rather than the class \ +in the stub file. +\item Write the element declaration that you wish to annotate, within the class you just created. \\ +For a method, this is the method signature, followed by ``\<;>''. \\ +For a field, this is the type, field name, and ``\<;>'', without an initializer. +\item Annotate the declaration that you just wrote. +\item Add import statements for any annotations you wrote. +\end{enumerate} %% Changes in JDK 11 have broken StubGenerator. % \subsubsectionAndLabel{If you do not have access to the Java source code}{stub-creating-without-source} @@ -900,7 +950,7 @@ can be read by the Checker Framework. Section~\ref{stub} describes stub files, which are used by programmers and type system designers. -This section dscribes ajava files. +This section describes ajava files. Ajava files are read and written by tools, such as whole-program type inference (see Section~\ref{whole-program-inference}). This section about ajava files is primarily of interest to the maintainers of such tools. @@ -1031,7 +1081,7 @@ % LocalWords: CollectionToArrayHeuristics BaseTypeVisitor Xbootclasspath % LocalWords: Interning's UsesObjectEquals ApermitMissingJdk AonlyUses java pre % LocalWords: Aignorejdkastub AstubWarnIfNotFound AstubDebug dont local' -% LocalWords: enableForgroundNdefPush BCEL getopt +% LocalWords: enableForgroundNdefPush BCEL getopt ajava html drawImage % LocalWords: NoAnnotationFileParserWarning CHECKERFRAMEWORK AnnotatedFor regex % LocalWords: AuseConservativeDefaultsForUnannotatedCode buildfile qual % LocalWords: AprintUnannotatedMethods checkername AskipDefs bcel mkdir @@ -1043,4 +1093,7 @@ % LocalWords: AuseConservativeDefaultsForUncheckedCodesource nextInt % LocalWords: AstubWarnIfNotFoundIgnoresClasses AmergeStubsWithSource % LocalWords: AstubWarnIfRedundantWithBytecode JavaStubifier StubFiles -% LocalWords: BaseTypeChecker +% LocalWords: BaseTypeChecker ImageObserver Graphics2D AstubWarnNote +% LocalWords: AstubNoWarnIfNotFound NoStubParserWarning AstubWarn Werror +% LocalWords: Aajava substring outerpackage innerpackage myMethod MyClass +% LocalWords: InsertAjavaAnnotations diff --git a/docs/manual/external-tools.tex b/docs/manual/external-tools.tex index 2117afad4aa..b80dc3385d9 100644 --- a/docs/manual/external-tools.tex +++ b/docs/manual/external-tools.tex @@ -1032,7 +1032,7 @@ maven-compiler-plugin - 3.10.1 + 3.11.0 true diff --git a/docs/manual/inference.tex b/docs/manual/inference.tex index f44283650ee..0242fd84e6b 100644 --- a/docs/manual/inference.tex +++ b/docs/manual/inference.tex @@ -135,7 +135,7 @@ A typical invocation of \ is \begin{Verbatim} - wpi.sh -- --checker nullness + $CHECKERFRAMEWORK/bin/wpi.sh -- --checker nullness \end{Verbatim} The result is a set of log files placed in the \ folder of the diff --git a/docs/manual/introduction.tex b/docs/manual/introduction.tex index 6ca9b007fd4..e411dba47d2 100644 --- a/docs/manual/introduction.tex +++ b/docs/manual/introduction.tex @@ -1300,14 +1300,15 @@ \paragraphAndLabel{Optional example}{annotate-normal-behavior-optional-example} Another example is the Optional Checker (\chapterpageref{optional-checker}) -and the \sunjavadoc{java.base/java/util/Optional.html\#orElseThrow()}{orElseThrow} method. +and the \sunjavadoc{java.base/java/util/Optional.html\#orElseThrow()}{orElseThrow()} method. The goal of the Optional Checker is to ensure that the program does not crash due to use of a non-present Optional value. Therefore, the receiver of -\ is annotated as +\ is annotated as \refqualclass{checker/optional/qual}{Present}, and the Optional Checker issues an error if the client calls -\ on a \refqualclass{checker/optional/qual}{MaybePresent} value. +\ on a \refqualclass{checker/optional/qual}{MaybePresent} value. +(For details, see Section~\ref{optional-guarantees}.) \paragraphAndLabel{Permitting crashes in some called methods}{annotate-normal-behavior-skip-libraries} @@ -1684,3 +1685,6 @@ % LocalWords: AmergeStubsWithSource MyBatis AdumpOnErrors AutoValue % LocalWords: specification'' AwarnUnneededSuppressionsExceptions % LocalWords: requireNonNull ApermitUnsupportedJdkVersion AstubWarnNote +% LocalWords: AwarnRedundantAnnotations AinferOutputOriginal +% LocalWords: AshowPrefixInWarningMessages AstubNoWarnIfNotFound +% LocalWords: AshowWpiFailedInferences diff --git a/docs/manual/manual-style.tex b/docs/manual/manual-style.tex index a2e5cc12851..188af0b0761 100644 --- a/docs/manual/manual-style.tex +++ b/docs/manual/manual-style.tex @@ -189,6 +189,7 @@ %HEVEA \renewcommand{\refwithpageparen}[1]{\ref{#1}} % Use \chapterpageref to reference only chapters, not sections. \newcommand{\chapterpageref}[1]{Chapter~\refwithpage{#1}} +\newcommand{\sectionpageref}[1]{Section~\refwithpage{#1}} \ifhevea diff --git a/docs/manual/nullness-checker.tex b/docs/manual/nullness-checker.tex index 37c786c75da..86e60e133c6 100644 --- a/docs/manual/nullness-checker.tex +++ b/docs/manual/nullness-checker.tex @@ -663,6 +663,7 @@ void myMethod() { @SuppressWarnings("nullness") // with argument x, getObject always returns a non-null value @NonNull Object o2 = getObject(x); + } \end{Verbatim} %BEGIN LATEX \end{smaller} diff --git a/docs/manual/optional-checker.tex b/docs/manual/optional-checker.tex index 38d68345676..367bff152bc 100644 --- a/docs/manual/optional-checker.tex +++ b/docs/manual/optional-checker.tex @@ -1,6 +1,11 @@ \htmlhr \chapterAndLabel{Optional Checker for possibly-present data}{optional-checker} +Use of the Optional Checker guarantees that your program will not suffer +a \ when calling +methods on an expression of \ type. +The Optional Checker also enforces Stuart Marks's style guidelines (see below). + Java 8 introduced the \sunjavadoc{java.base/java/util/Optional.html}{Optional} class, a container that is either empty or contains a non-null value. @@ -46,10 +51,6 @@ Optional Checker in the future.) % They are all AST checks that would be easy to add later. -Use of the Optional Checker guarantees that your program will not suffer a -\ nor a \ when calling -methods on an expression of \ type. - \sectionAndLabel{How to run the Optional Checker}{optional-run-checker} @@ -98,17 +99,26 @@ \sectionAndLabel{What the Optional Checker guarantees}{optional-guarantees} -The Optional Checker guarantees that your code will not throw an exception +The Optional Checker guarantees that your code will not throw a \ exception due to use of an absent \ where a present \ is needed. More specifically, the Optional Checker will issue an error if you call -\sunjavadoc{java.base/java/util/Optional.html\#get() -}{get} +\sunjavadoc{java.base/java/util/Optional.html\#get()}{get} or -\sunjavadoc{java.base/java/util/Optional.html\#orElseThrow(java.util.function.Supplier)}{orElseThrow} +\sunjavadoc{java.base/java/util/Optional.html\#orElseThrow()}{orElseThrow()} on a \<@MaybePresent Optional> receiver, because each of these methods -throws an exception if the receiver is an absent +throws a \ exception if the receiver is a possibly-absent \. +By contrast, the Optional Checker does not issue an error if you call +\sunjavadoc{java.base/java/util/Optional.html\#orElseThrow(java.util.function.Supplier)}{orElseThrow(Supplier)} +with a possibly-absent \. That method call does not +% necessarily +throw \. The Optional Checker assumes that the +programmer has mechanisms in place to handle whatever exception it throws. +If you wish for the Optional Checker to warn about calling +\ on a possibly-absent \, then you can use +a stub file (\sectionpageref{stub}) to annotate its receiver as \<@Present>. + The Optional Checker does not check nullness properties, such as requiring that the argument to \sunjavadoc{java.base/java/util/Optional.html\#of(T)}{of} @@ -120,6 +130,91 @@ As with any checker, the guarantee is subject to certain limitations (see Section~\ref{checker-guarantees}). +\sectionAndLabel{Suppressing optional warnings}{suppressing-warnings-optional} + +It is often best to change the code or annotations when the Optional Checker +reports a warning. +Alternatively, you might choose to suppress the warning. +This does not change the code but prevents the warning from being presented to +you. + +\begin{sloppypar} +The Checker Framework supplies several ways to suppress warnings. +The \<@SuppressWarnings("optional")> annotation is specific to warnings raised +by the Optional Checker. +See Chapter~\ref{suppressing-warnings} for additional usages. +An example use is +\end{sloppypar} + +%BEGIN LATEX +\begin{smaller} +%END LATEX +\begin{Verbatim} + // might return a possibly-empty Optional + Optional wrapWithOptional(...) { ... } + + void myMethod() { + @SuppressWarnings("optional") // with argument x, wrapWithOptional always returns a non-empty Optional + @Present Optional optX = wrapWithOptional(x); + } +\end{Verbatim} +%BEGIN LATEX +\end{smaller} +%END LATEX + +The Optional Checker also permits the use of method calls and assertions to +suppress warnings; see immediately below. + + +\subsectionAndLabel{Suppressing warnings with assertions and method calls}{suppressing-optional-warnings-with-assertions-and-method-calls} + +Occasionally, it is inconvenient or +verbose to use the \<@SuppressWarnings> annotation. For example, Java does +not permit annotations such as \<@SuppressWarnings> to appear on +statements, expressions, static initializers, etc. +Here are three 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}). +\item + Write a call to the + \refmethod{checker/optional/util}{OptionalUtil}{castPresent}{(T)} method. +\end{itemize} + +The rest of this section discusses the \ method. +It is useful if you wish to suppress a warning within an expression. + +The Optional Checker considers both the return value, and also the +argument, to be an instance of a non-empty Optional after the \ +method call. +The Optional Checker issues no warnings in any of the following +code: + +\begin{Verbatim} + // One way to use castPresent as a cast: + @Present Optional optString = castPresent(possiblyEmpty1); + + // Another way to use castPresent as a cast: + castPresent(possiblyEmpty2).toString(); + + // It is possible, but not recommmended, to use castPresent as a statement: + // (It would be better to write an assert statement with @AssumeAssertion + // in its message, instead.) + castPresent(possiblyEmpty3); + possiblyEmpty3.toString(); +\end{Verbatim} + + The \ method throws \ if Java assertions are + enabled and the argument is an empty \. + However, it is not intended for general defensive programming; see + Section~\ref{defensive-programming}. + + To use the \ method, the \ file + must be on the classpath at run time. % LocalWords: isPresent NoSuchElementException MaybePresent PolyPresent %% LocalWords: orElseThrow nullable diff --git a/docs/manual/resource-leak-checker.tex b/docs/manual/resource-leak-checker.tex index 1db785b9cce..f7214791c01 100644 --- a/docs/manual/resource-leak-checker.tex +++ b/docs/manual/resource-leak-checker.tex @@ -60,6 +60,9 @@ See Section~\ref{resource-leak-ignored-exceptions}. \item[\<-ApermitInitializationLeak>] See Section~\ref{resource-leak-field-initialization}. +%% TODO: Uncomment when the feature is ready to be publicized. +% \item[\<-AenableWpiForRlc>] +% See Section~\ref{resource-leak-checker-inference-algo}. \end{description} If you are running the Resource Leak Checker, then there is no need to run @@ -608,6 +611,19 @@ not possible, the programmer will probably need to suppress a warning and then verify the code using a method other than the Resource Leak Checker. + +%% TODO: Uncomment when the feature is ready to be publicized. +% \sectionAndLabel{Resource Leak Checker Annotation Inference Algorithm}{resource-leak-checker-inference-algo} +% +% We are developing a special inference mechanism to infer annotations for +% the Resource Leak Checker. By default, this mechanism operates when the +% -Ainfer flag is enabled. To utilize the whole-program inference mechanism outlined in +% section \ref{whole-program-inference} in addition to this mechanism for the Resource +% Leak Checker and its sub-checkers, you should provide the \<-AenableWpiForRlc> flag. +% +% The paper \href={https://arxiv.org/pdf/2306.11953.pdf}{Automatic Inference of Resource Leak Specifications}, published at OOPSLA 2023, gives more details on the inference algorithm. Currently, only the first phase of the algorithm described in the paper is available, and the complete implementation will be available soon. + + % LocalWords: de subchecker OutputStream MustCall MustCallUnknown RAII Un % LocalWords: PolyMustCall InheritableMustCall MultiRandSelector callsite % LocalWords: Partitioner CalledMethods AnoLightweightOwnership NotOwning diff --git a/framework/build.gradle b/framework/build.gradle index 05b7dba1bd2..0113bb4befc 100644 --- a/framework/build.gradle +++ b/framework/build.gradle @@ -123,6 +123,8 @@ task copyAndMinimizeAnnotatedJdkFiles(dependsOn: cloneTypetoolsJdk, group: 'Buil } javaexec { classpath = sourceSets.main.runtimeClasspath + standardOutput = System.out + errorOutput = System.err mainClass = 'org.checkerframework.framework.stub.JavaStubifier' args outputDir diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeValidator.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeValidator.java index 6bec266d8e0..d08496cb338 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeValidator.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeValidator.java @@ -291,6 +291,12 @@ public Void visitDeclared(AnnotatedDeclaredType type, Tree tree) { } boolean skipChecks = checker.shouldSkipUses(type.getUnderlyingType().asElement()); + if (type.containsUninferredTypeArguments()) { + if (!atypeFactory.ignoreUninferredTypeArguments) { + isValid = true; + } + return null; + } if (checkTopLevelDeclaredOrPrimitiveType && !skipChecks) { // Ensure that type use is a subtype of the element type 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 6f900e062d1..4fcbfd4a15c 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -1024,7 +1024,7 @@ public Void visitMethod(MethodTree tree, Void p) { checkContractsAtMethodDeclaration(tree, methodElement, formalParamNames, abstractMethod); // Infer postconditions - if (atypeFactory.getWholeProgramInference() != null) { + if (shouldPerformContractInference()) { assert ElementUtils.isElementFromSourceCode(methodElement); // TODO: Infer conditional postconditions too. @@ -1046,6 +1046,18 @@ public Void visitMethod(MethodTree tree, Void p) { } } + /** + * Should Whole Program Inference attempt to infer contract annotations? Typically, the answer is + * "yes" whenever WPI is enabled, but this method exists to allow subclasses to customize that + * behavior. + * + * @return true if contract inference should be performed, false if it should be disabled (even + * when WPI is enabled) + */ + protected boolean shouldPerformContractInference() { + return atypeFactory.getWholeProgramInference() != null; + } + /** * Check method purity if needed. Note that overriding rules are checked as part of {@link * #checkOverride(MethodTree, AnnotatedTypeMirror.AnnotatedExecutableType, @@ -4815,7 +4827,9 @@ protected TypeValidator createTypeValidator() { */ protected final boolean shouldSkipUses(ExpressionTree exprTree) { // System.out.printf("shouldSkipUses: %s: %s%n", exprTree.getClass(), exprTree); - + if (atypeFactory.isUnreachable(exprTree)) { + return true; + } Element elm = TreeUtils.elementFromTree(exprTree); return checker.shouldSkipUses(elm); } diff --git a/framework/src/main/java/org/checkerframework/common/value/ValueAnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/common/value/ValueAnnotatedTypeFactory.java index a011bb278a4..c6b9d4f7899 100644 --- a/framework/src/main/java/org/checkerframework/common/value/ValueAnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/common/value/ValueAnnotatedTypeFactory.java @@ -357,7 +357,7 @@ protected TypeHierarchy createTypeHierarchy() { public StructuralEqualityComparer createEqualityComparer() { return new StructuralEqualityComparer(areEqualVisitHistory) { @Override - protected boolean arePrimeAnnosEqual( + protected boolean arePrimaryAnnosEqual( AnnotatedTypeMirror type1, AnnotatedTypeMirror type2) { type1.replaceAnnotation( convertToUnknown( @@ -368,7 +368,7 @@ protected boolean arePrimeAnnosEqual( convertSpecialIntRangeToStandardIntRange( type2.getPrimaryAnnotationInHierarchy(UNKNOWNVAL)))); - return super.arePrimeAnnosEqual(type1, type2); + return super.arePrimaryAnnosEqual(type1, type2); } }; } diff --git a/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceJavaParserStorage.java b/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceJavaParserStorage.java index 53c4a8df117..8fc817c8af7 100644 --- a/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceJavaParserStorage.java +++ b/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceJavaParserStorage.java @@ -1071,11 +1071,10 @@ public void writeResultsToFile(OutputFormat outputFormat, BaseTypeChecker checke private void writeAjavaFile(File outputPath, CompilationUnitAnnos root) { try (Writer writer = new BufferedWriter(new FileWriter(outputPath))) { - // JavaParser can output using lexical preserving printing, which writes the file such - // that its formatting is close to the original source file it was parsed from as - // possible. Currently, this feature is very buggy and crashes when adding annotations - // in certain locations. This implementation could be used instead if it's fixed in - // JavaParser. + // This implementation uses JavaParser's lexical preserving printing, which writes the file + // such that its formatting is close to the original source file it was parsed from as + // possible. It is commented out because, this feature is very buggy and crashes when adding + // annotations in certain locations. // LexicalPreservingPrinter.print(root.declaration, writer); // Do not print invisible qualifiers, to avoid cluttering the output. @@ -1906,10 +1905,6 @@ public boolean addDeclarationAnnotation(AnnotationMirror annotation) { * nodes for that field. */ public void transferAnnotations() { - if (type == null) { - return; - } - if (declarationAnnotations != null) { // Don't add directly to the type of the variable declarator, // because declaration annotations need to be attached to the FieldDeclaration diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java index 3b08ed8cbe0..ce0a531e23c 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java @@ -1015,7 +1015,7 @@ public TransferResult visitInstanceOf(InstanceOfNode node, TransferInput[] classes = relevantJavaTypesAnno.value(); - this.relevantJavaTypes = new HashSet<>(CollectionsPlume.mapCapacity(classes.length)); + Set relevantJavaTypesTemp = + new HashSet<>(CollectionsPlume.mapCapacity(classes.length)); boolean arraysAreRelevantTemp = false; for (Class clazz : classes) { if (clazz == Object[].class) { @@ -374,9 +375,11 @@ protected GenericAnnotatedTypeFactory(BaseTypeChecker checker, boolean useFlow) + this.getClass().getSimpleName()); } else { TypeMirror relevantType = TypesUtils.typeFromClass(clazz, types, elements); - relevantJavaTypes.add(types.erasure(relevantType)); + TypeMirror erased = types.erasure(relevantType); + relevantJavaTypesTemp.add(erased); } } + this.relevantJavaTypes = Collections.unmodifiableSet(relevantJavaTypesTemp); this.arraysAreRelevant = arraysAreRelevantTemp; } @@ -442,6 +445,7 @@ public void setRoot(@Nullable CompilationUnitTree root) { super.setRoot(root); this.scannedClasses.clear(); + this.reachableNodes.clear(); this.flowResult = null; this.regularExitStores.clear(); this.exceptionalExitStores.clear(); @@ -1053,6 +1057,32 @@ public IPair getExpressionAndOffsetFromJavaExpressionStr return value != null ? value.getAnnotations().iterator().next() : null; } + /** + * Returns true if the {@code exprTree} is unreachable. This is a conservative estimate and may + * return {@code false} even though the {@code exprTree} is unreachable. + * + * @param exprTree an expression tree + * @return true if the {@code exprTree} is unreachable + */ + public boolean isUnreachable(ExpressionTree exprTree) { + if (!everUseFlow) { + return false; + } + Set nodes = getNodesForTree(exprTree); + if (nodes == null) { + // Dataflow has no any information about the tree, so conservatively consider the tree + // reachable. + return false; + } + for (Node n : nodes) { + if (n.getTree() != null && reachableNodes.contains(n.getTree())) { + return false; + } + } + // None of the corresponding nodes is reachable, so this tree is dead. + return true; + } + /** * Track the state of org.checkerframework.dataflow analysis scanning for each class tree in the * compilation unit. @@ -1067,6 +1097,16 @@ protected enum ScanState { /** Map from ClassTree to their dataflow analysis state. */ protected final Map scannedClasses = new HashMap<>(); + /** + * A set of trees whose corresponding nodes are reachable. This is not an exhaustive set of + * reachable trees. Use {@link #isUnreachable(ExpressionTree)} instead of this set directly. + * + *

This cannot be a set of Nodes, because two LocalVariableNodes are equal if they have the + * same name but represent different uses of the variable. So instead of storing Nodes, it stores + * the result of {@code Node#getTree}. + */ + private final Set reachableNodes = new HashSet<>(); + /** * The result of the flow analysis. Invariant: * @@ -1261,10 +1301,11 @@ public Store getStoreAfter(Node node) { /** * See {@link org.checkerframework.dataflow.analysis.AnalysisResult#getNodesForTree(Tree)}. * + * @param tree a tree * @return the {@link Node}s for a given {@link Tree} * @see org.checkerframework.dataflow.analysis.AnalysisResult#getNodesForTree(Tree) */ - public Set getNodesForTree(Tree tree) { + public @Nullable Set getNodesForTree(Tree tree) { return flowResult.getNodesForTree(tree); } @@ -1528,7 +1569,13 @@ protected void analyze( boolean isStatic, @Nullable Store capturedStore) { ControlFlowGraph cfg = CFCFGBuilder.build(root, ast, checker, this, processingEnv); - + cfg.getAllNodes(this::isIgnoredExceptionType) + .forEach( + node -> { + if (node.getTree() != null) { + reachableNodes.add(node.getTree()); + } + }); if (isInitializationCode) { Store initStore = !isStatic ? initializationStore : initializationStaticStore; if (initStore != null) { @@ -1607,6 +1654,16 @@ protected void analyze( postAnalyze(cfg); } + /** + * Returns true if {@code typeMirror} is an exception type that should be ignored. + * + * @param typeMirror an exception type + * @return true if {@code typeMirror} is an exception type that should be ignored + */ + public boolean isIgnoredExceptionType(TypeMirror typeMirror) { + return false; + } + /** * Perform any additional operations on a CFG. Called once per CFG, after the CFG has been * analyzed by {@link #analyze(Queue, Queue, UnderlyingAST, List, ClassTree, boolean, boolean, @@ -2393,8 +2450,9 @@ private static void log(String format, Object... args) { * Returns true if users can write type annotations from this type system directly on the given * Java type. * - *

May return false for a compound type (for which it is possible to write type qualifiers on - * elements of the type). + *

For a compound type, returns true only if a programmer may 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. * *

Subclasses should override {@code #isRelevantImpl} instead of this method. * @@ -2403,6 +2461,9 @@ private static void log(String format, Object... args) { * Java type */ public final boolean isRelevant(TypeMirror tm) { + if (relevantJavaTypes == null) { + return true; + } if (tm.getKind() != TypeKind.PACKAGE && tm.getKind() != TypeKind.MODULE) { tm = types.erasure(tm); } @@ -2419,8 +2480,9 @@ public final boolean isRelevant(TypeMirror tm) { * Returns true if users can write type annotations from this type system directly on the given * Java type. * - *

May return false for a compound type (for which it is possible to write type qualifiers on - * elements of the type). + *

For a compound type, returns true only if it a programmer may 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. * *

Subclasses should override {@code #isRelevantImpl} instead of this method. * @@ -2444,7 +2506,11 @@ public final boolean isRelevant(AnnotatedTypeMirror tm) { */ protected boolean isRelevantImpl(TypeMirror tm) { - if (relevantJavaTypes == null || relevantJavaTypes.contains(tm)) { + if (relevantJavaTypes == null) { + return true; + } + + if (relevantJavaTypes.contains(tm)) { return true; } diff --git a/framework/src/main/java/org/checkerframework/framework/type/QualifierHierarchy.java b/framework/src/main/java/org/checkerframework/framework/type/QualifierHierarchy.java index 523148fe1b6..cf985fd4509 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/QualifierHierarchy.java +++ b/framework/src/main/java/org/checkerframework/framework/type/QualifierHierarchy.java @@ -43,9 +43,9 @@ public QualifierHierarchy(GenericAnnotatedTypeFactory atypeFactory) } /** - * Determine whether this is valid. + * Determine whether this QualifierHierarchy is valid. * - * @return true if this is valid + * @return true if this QualifierHierarchy is valid */ public boolean isValid() { return true; diff --git a/framework/src/main/java/org/checkerframework/framework/type/StructuralEqualityComparer.java b/framework/src/main/java/org/checkerframework/framework/type/StructuralEqualityComparer.java index 8209d92778e..56fba92e7e7 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/StructuralEqualityComparer.java +++ b/framework/src/main/java/org/checkerframework/framework/type/StructuralEqualityComparer.java @@ -46,7 +46,7 @@ public StructuralEqualityComparer(StructuralEqualityVisitHistory typeargVisitHis public Boolean defaultAction(AnnotatedTypeMirror type1, AnnotatedTypeMirror type2, Void p) { if (type1.getKind() == TypeKind.NULL || type2.getKind() == TypeKind.NULL) { // If one of the types is the NULL type, compare main qualifiers only. - return arePrimeAnnosEqual(type1, type2); + return arePrimaryAnnosEqual(type1, type2); } if (type1.containsUninferredTypeArguments() || type2.containsUninferredTypeArguments()) { @@ -113,7 +113,7 @@ public boolean areEqualInHierarchy( * @param type2 a type * @return true if type1 and type2 have the same set of annotations */ - protected boolean arePrimeAnnosEqual(AnnotatedTypeMirror type1, AnnotatedTypeMirror type2) { + protected boolean arePrimaryAnnosEqual(AnnotatedTypeMirror type1, AnnotatedTypeMirror type2) { if (currentTop != null) { AnnotationMirror anno1 = type1.getPrimaryAnnotationInHierarchy(currentTop); AnnotationMirror anno2 = type2.getPrimaryAnnotationInHierarchy(currentTop); @@ -187,7 +187,7 @@ protected boolean checkOrAreEqual(AnnotatedTypeMirror type1, AnnotatedTypeMirror */ @Override public Boolean visitArray_Array(AnnotatedArrayType type1, AnnotatedArrayType type2, Void p) { - if (!arePrimeAnnosEqual(type1, type2)) { + if (!arePrimaryAnnosEqual(type1, type2)) { return false; } @@ -213,7 +213,7 @@ public Boolean visitDeclared_Declared( // TODO: same class/interface is not enforced. Why? - if (!arePrimeAnnosEqual(type1, type2)) { + if (!arePrimaryAnnosEqual(type1, type2)) { return false; } // Prevent infinite recursion e.g. in Issue1587b @@ -279,7 +279,7 @@ public Boolean visitDeclared_Declared( @Override public Boolean visitIntersection_Intersection( AnnotatedIntersectionType type1, AnnotatedIntersectionType type2, Void p) { - if (!arePrimeAnnosEqual(type1, type2)) { + if (!arePrimaryAnnosEqual(type1, type2)) { return false; } @@ -298,7 +298,7 @@ public Boolean visitIntersection_Intersection( @Override public Boolean visitPrimitive_Primitive( AnnotatedPrimitiveType type1, AnnotatedPrimitiveType type2, Void p) { - return arePrimeAnnosEqual(type1, type2); + return arePrimaryAnnosEqual(type1, type2); } /** @@ -384,7 +384,7 @@ public Boolean visitDeclared_Primitive( throw new BugInCF(defaultErrorMessage(type1, type2, p)); } - return arePrimeAnnosEqual(type1, type2); + return arePrimaryAnnosEqual(type1, type2); } @Override @@ -394,6 +394,6 @@ public Boolean visitPrimitive_Declared( throw new BugInCF(defaultErrorMessage(type1, type2, p)); } - return arePrimeAnnosEqual(type1, type2); + return arePrimaryAnnosEqual(type1, type2); } } diff --git a/framework/tests/all-systems/Issue6259.java b/framework/tests/all-systems/Issue6259.java new file mode 100644 index 00000000000..fc44acd7190 --- /dev/null +++ b/framework/tests/all-systems/Issue6259.java @@ -0,0 +1,35 @@ +@SuppressWarnings("unchecked") +public class Issue6259 { + public interface A { + interface Builder { + AT build(); + } + } + + public abstract static class B implements C { + public abstract static class Builder implements C.Builder {} + } + + public interface I> {} + + public interface C { + interface Builder {} + } + + public static final class L implements I> {} + + static class S> { + + public static < + ET extends A, E2 extends A.Builder, CT, IT extends C, I2 extends C.Builder> + S assemble(I... xs) { + throw new AssertionError(); + } + } + + void f(L f) { + S> storeStack = S.assemble(f); + var storeStackVar = S.assemble(f); + var storeStackVarExplicit = S., String, B, B.Builder>assemble(f); + } +} diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/TypesUtils.java b/javacutil/src/main/java/org/checkerframework/javacutil/TypesUtils.java index dddb3cb1e5c..61fef95e135 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/TypesUtils.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/TypesUtils.java @@ -171,10 +171,10 @@ public static Class getClassFromType(TypeMirror typeMirror) { } /** - * Returns the simple type name, without annotations. + * Returns the simple type name, without annotations but including array brackets. * * @param type a type - * @return the simple type name, without annotations + * @return the simple type name */ public static String simpleTypeName(TypeMirror type) { switch (type.getKind()) { @@ -218,10 +218,10 @@ public static String simpleTypeName(TypeMirror type) { } /** - * Returns the binary name. + * Returns the binary name of a type. * * @param type a type - * @return the binary name + * @return its binary name */ public static @BinaryName String binaryName(TypeMirror type) { if (type.getKind() != TypeKind.DECLARED) {