From 51993acf45c2f1e7fcfcc6b3a1f1c68a05e424e6 Mon Sep 17 00:00:00 2001 From: "renovate[bot]" <29139614+renovate[bot]@users.noreply.github.com> Date: Mon, 27 Nov 2023 07:25:17 -0800 Subject: [PATCH 01/19] Update plugin com.diffplug.spotless to v6.23.0 (#6318) Co-authored-by: renovate[bot] <29139614+renovate[bot]@users.noreply.github.com> --- build.gradle | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/build.gradle b/build.gradle index a61ccffcc4b..9a19f593f80 100644 --- a/build.gradle +++ b/build.gradle @@ -15,7 +15,7 @@ plugins { // Code formatting; defines targets "spotlessApply" and "spotlessCheck". // https://github.com/diffplug/spotless/tags ; see tags starting "gradle/" // Only works on JDK 11+ (even including the plugin crashes Gradle on JDK 8). - id 'com.diffplug.spotless' version '6.22.0' + id 'com.diffplug.spotless' version '6.23.0' } apply plugin: 'de.undercouch.download' From c0d336fa381a2a9b2b4decab60eee396dfed5fa1 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Tue, 28 Nov 2023 08:14:11 -0800 Subject: [PATCH 02/19] Add `@EnsuresNonNull` annotations in stub files (#6316) --- .../checker/nullness/util/NullnessUtil.java | 3 ++- .../checker/nullness/junit-assertions.astub | 3 +++ .../nullness/permit-nullness-assertion-exception.astub | 8 +++++++- 3 files changed, 12 insertions(+), 2 deletions(-) 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 0af1a3c975a..c7f897f601f 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 @@ -81,7 +81,8 @@ private NullnessUtil() { * @param message text to include if this method is misused * @return the argument, casted to have the type qualifier @NonNull */ - public static @EnsuresNonNull("#1") @NonNull T castNonNull( + @EnsuresNonNull("#1") + public static @NonNull T castNonNull( @Nullable T ref, String message) { assert ref != null : "Misuse of castNonNull: called with a null argument: " + message; return (@NonNull T) ref; diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/junit-assertions.astub b/checker/src/main/java/org/checkerframework/checker/nullness/junit-assertions.astub index 90e73ecc01f..3ec501b0bac 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/junit-assertions.astub +++ b/checker/src/main/java/org/checkerframework/checker/nullness/junit-assertions.astub @@ -53,10 +53,13 @@ public class Assertions { public static void assertNull(@Nullable Object actual, Supplier messageSupplier); + @EnsuresNonNull("#1") public static void assertNotNull(Object actual); + @EnsuresNonNull("#1") public static void assertNotNull(Object actual, String message); + @EnsuresNonNull("#1") public static void assertNotNull(Object actual, Supplier messageSupplier); public static void assertEquals(short expected, short actual); diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/permit-nullness-assertion-exception.astub b/checker/src/main/java/org/checkerframework/checker/nullness/permit-nullness-assertion-exception.astub index 46f0d3c81c8..c101d3d4992 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/permit-nullness-assertion-exception.astub +++ b/checker/src/main/java/org/checkerframework/checker/nullness/permit-nullness-assertion-exception.astub @@ -17,7 +17,7 @@ public class Objects { } -// No annotations for com.google.common.base.Preconditions or +// No type annotations for com.google.common.base.Preconditions or // com.google.common.base.Verify are needed because they are annotated with // @CheckForNull and the Checker Framework treats @CheckForNull as @Nullable. @@ -25,8 +25,11 @@ public class Objects { package org.junit; public class Assertions { + @EnsuresNonNull("#1") public static void assertNotNull(@Nullable Object actual); + @EnsuresNonNull("#1") public static void assertNotNull(@Nullable Object actual, String message); + @EnsuresNonNull("#1") public static void assertNotNull(@Nullable Object actual, Supplier messageSupplier); } @@ -34,7 +37,10 @@ public class Assertions { package org.junit.jupiter.api; public class Assertions { + @EnsuresNonNull("#1") public static void assertNotNull(@Nullable Object actual); + @EnsuresNonNull("#1") public static void assertNotNull(@Nullable Object actual, String message); + @EnsuresNonNull("#1") public static void assertNotNull(@Nullable Object actual, Supplier messageSupplier); } From dcb260e03be0df5bae400e0d7336414d9ca1f505 Mon Sep 17 00:00:00 2001 From: James Yoo <24359440+jyoo980@users.noreply.github.com> Date: Tue, 28 Nov 2023 16:06:29 -0800 Subject: [PATCH 03/19] Fix typo in `annotating-libraries.tex` --- docs/manual/annotating-libraries.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/manual/annotating-libraries.tex b/docs/manual/annotating-libraries.tex index 35233c8282a..3d5070294cd 100644 --- a/docs/manual/annotating-libraries.tex +++ b/docs/manual/annotating-libraries.tex @@ -66,7 +66,7 @@ %% Leave out this complication. % This approach is possible with annotated source code. - Then, when check a client of the library, + Then, when checking a client of the library, supply the ``stub file'' textually to the Checker Framework. This approach does not require you to compile the library source From 56cd992b5e337ebee3515b67710262923fc72714 Mon Sep 17 00:00:00 2001 From: Suzanne Millstein Date: Tue, 28 Nov 2023 19:26:10 -0800 Subject: [PATCH 04/19] Correct Java type of conditional expressions in dataflow --- .../checker/nullness/KeyForValue.java | 20 ++++---- .../checker/nullness/NullnessValue.java | 5 +- .../tests/optional/java17/OptionalSwitch.java | 11 ++++ .../dataflow/analysis/AbstractValue.java | 3 ++ docs/CHANGELOG.md | 4 ++ .../accumulation/AccumulationValue.java | 6 ++- .../framework/flow/CFAbstractTransfer.java | 7 ++- .../framework/flow/CFAbstractValue.java | 51 +++++++++++++++++-- 8 files changed, 89 insertions(+), 18 deletions(-) create mode 100644 checker/tests/optional/java17/OptionalSwitch.java diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/KeyForValue.java b/checker/src/main/java/org/checkerframework/checker/nullness/KeyForValue.java index 3ffab217094..9c04223489d 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/KeyForValue.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/KeyForValue.java @@ -84,19 +84,21 @@ public KeyForValue( } @Override - public KeyForValue leastUpperBound(@Nullable KeyForValue other) { - KeyForValue lub = super.leastUpperBound(other); + protected KeyForValue upperBound( + @Nullable KeyForValue other, TypeMirror upperBoundTypeMirror, boolean shouldWiden) { + KeyForValue upperBound = super.upperBound(other, upperBoundTypeMirror, shouldWiden); + if (other == null || other.keyForMaps == null || this.keyForMaps == null) { - return lub; + return upperBound; } // Lub the keyForMaps by intersecting the sets. - lub.keyForMaps = new LinkedHashSet<>(this.keyForMaps.size()); - lub.keyForMaps.addAll(this.keyForMaps); - lub.keyForMaps.retainAll(other.keyForMaps); - if (lub.keyForMaps.isEmpty()) { - lub.keyForMaps = null; + upperBound.keyForMaps = new LinkedHashSet<>(this.keyForMaps.size()); + upperBound.keyForMaps.addAll(this.keyForMaps); + upperBound.keyForMaps.retainAll(other.keyForMaps); + if (upperBound.keyForMaps.isEmpty()) { + upperBound.keyForMaps = null; } - return lub; + return upperBound; } @Override diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessValue.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessValue.java index b2b9663a60d..063ecb75642 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessValue.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessValue.java @@ -41,8 +41,9 @@ public NullnessValue( } @Override - public NullnessValue leastUpperBound(@Nullable NullnessValue other) { - NullnessValue result = super.leastUpperBound(other); + protected NullnessValue upperBound( + @Nullable NullnessValue other, TypeMirror upperBoundTypeMirror, boolean shouldWiden) { + NullnessValue result = super.upperBound(other, upperBoundTypeMirror, shouldWiden); AnnotationMirror resultNullableAnno = analysis.getTypeFactory().getAnnotationByClass(result.annotations, Nullable.class); diff --git a/checker/tests/optional/java17/OptionalSwitch.java b/checker/tests/optional/java17/OptionalSwitch.java new file mode 100644 index 00000000000..ea93f342bbd --- /dev/null +++ b/checker/tests/optional/java17/OptionalSwitch.java @@ -0,0 +1,11 @@ +// @below-java17-jdk-skip-test +public class OptionalSwitch { + public static boolean flag; + + public Object test(int c) { + return switch (c) { + case 3 -> flag ? "" : "obj.getBaseStat();"; + default -> null; + }; + } +} diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/analysis/AbstractValue.java b/dataflow/src/main/java/org/checkerframework/dataflow/analysis/AbstractValue.java index f82685466dc..e503db4ee0a 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/analysis/AbstractValue.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/analysis/AbstractValue.java @@ -16,6 +16,9 @@ public interface AbstractValue> { * more permissive. *
  • Is commutative. * + * + * @param other the other value + * @return the least upper bound of the two values */ V leastUpperBound(V other); } diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md index 2e5ef18e7f2..3e3bed62158 100644 --- a/docs/CHANGELOG.md +++ b/docs/CHANGELOG.md @@ -10,6 +10,10 @@ New command-line options: Added method `isDeterministic()` to the `AnnotationProvider` interface. +`CFAbstractValue#leastUpperBound` and `CFAbstractValue#widenUpperBound` are now +final. Subclasses should override method `CFAbstractValue#upperBound(V, +TypeMirror, boolean)` instead. + **Closed issues:** diff --git a/framework/src/main/java/org/checkerframework/common/accumulation/AccumulationValue.java b/framework/src/main/java/org/checkerframework/common/accumulation/AccumulationValue.java index 8f429916fdc..12d51b25cff 100644 --- a/framework/src/main/java/org/checkerframework/common/accumulation/AccumulationValue.java +++ b/framework/src/main/java/org/checkerframework/common/accumulation/AccumulationValue.java @@ -79,8 +79,10 @@ protected AccumulationValue( } @Override - public AccumulationValue leastUpperBound(AccumulationValue other) { - AccumulationValue lub = super.leastUpperBound(other); + protected AccumulationValue upperBound( + @Nullable AccumulationValue other, TypeMirror upperBoundTypeMirror, boolean shouldWiden) { + AccumulationValue lub = super.upperBound(other, upperBoundTypeMirror, shouldWiden); + if (other == null || other.accumulatedValues == null || this.accumulatedValues == null) { return lub; } 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 ce0a531e23c..b081b50acd1 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java @@ -668,8 +668,13 @@ public TransferResult visitTernaryExpression( V elseValue = p.getValueOfSubNode(n.getElseOperand()); V resultValue = null; if (thenValue != null && elseValue != null) { + // If a conditional expression is a poly expression, then its Java type is the type of its + // context. (For example, the type of the conditional expression in `Object o = b ? "" : "";` + // is `Object`, not `String`.) + // So, use the Java type of the conditional expression and the annotations for each branch. + TypeMirror conditionalType = TreeUtils.typeOf(n.getTree()); // The resulting abstract value is the merge of the 'then' and 'else' branch. - resultValue = thenValue.leastUpperBound(elseValue); + resultValue = thenValue.leastUpperBound(elseValue, conditionalType); } V finishedValue = finishValue(resultValue, thenStore, elseStore); return new ConditionalTransferResult<>(finishedValue, thenStore, elseStore); diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractValue.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractValue.java index c0b560249a6..2348199d701 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractValue.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractValue.java @@ -432,11 +432,34 @@ private final AnnotationMirror lowestQualifier(AnnotationMirror qual1, Annotatio } } + /** + * {@inheritDoc} + * + *

    Subclasses should override {@link #upperBound(CFAbstractValue, TypeMirror, boolean)} instead + * of this method. + */ @Override - public V leastUpperBound(@Nullable V other) { + public final V leastUpperBound(@Nullable V other) { return upperBound(other, false); } + /** + * Compute the least upper bound of two abstract values. The returned value has a Java type of + * {@code typeMirror}. {@code typeMirror} should be an upper bound of the Java types of {@code + * this} an {@code other}, but it does not have be to the least upper bound. + * + *

    Subclasses should override {@link #upperBound(CFAbstractValue, TypeMirror, boolean)} instead + * of this method. + * + * @param other another value + * @param typeMirror the underlying Java type of the returned value, which may or may not be the + * least upper bound + * @return the least upper bound of two abstract values + */ + public final V leastUpperBound(@Nullable V other, TypeMirror typeMirror) { + return upperBound(other, typeMirror, false); + } + /** * Compute an upper bound of two values that is wider than the least upper bound of the two * values. Used to jump to a higher abstraction to allow faster termination of the fixed point @@ -456,10 +479,13 @@ public V leastUpperBound(@Nullable V other) { *

  • Is commutative. * * + * Subclasses should override {@link #upperBound(CFAbstractValue, TypeMirror, boolean)} instead of + * this method. + * * @param previous must be the previous value * @return an upper bound of two values that is wider than the least upper bound of the two values */ - public V widenUpperBound(@Nullable V previous) { + public final V widenUpperBound(@Nullable V previous) { return upperBound(previous, true); } @@ -480,7 +506,24 @@ private V upperBound(@Nullable V other, boolean shouldWiden) { TypeMirror lubTypeMirror = TypesUtils.leastUpperBound( this.getUnderlyingType(), other.getUnderlyingType(), processingEnv); + return upperBound(other, lubTypeMirror, shouldWiden); + } + /** + * Returns an upper bound of {@code this} and {@code other}. The underlying type of the value + * returned is {@code upperBoundTypeMirror}. If {@code shouldWiden} is false, this method returns + * the least upper bound of {@code this} and {@code other}. + * + *

    This is the implementation of {@link #leastUpperBound(CFAbstractValue, TypeMirror)}, {@link + * #leastUpperBound(CFAbstractValue)}, {@link #widenUpperBound(CFAbstractValue)}, and {@link + * #upperBound(CFAbstractValue, boolean)}. Subclasses may override it. + * + * @param other an abstract value + * @param upperBoundTypeMirror the underlying type of the returned value + * @param shouldWiden true if the method should perform widening + * @return an upper bound of this and {@code other} + */ + protected V upperBound(@Nullable V other, TypeMirror upperBoundTypeMirror, boolean shouldWiden) { ValueLub valueLub = new ValueLub(shouldWiden); AnnotationMirrorSet lub = valueLub.combineSets( @@ -488,8 +531,8 @@ private V upperBound(@Nullable V other, boolean shouldWiden) { this.getAnnotations(), other.getUnderlyingType(), other.getAnnotations(), - canBeMissingAnnotations(lubTypeMirror)); - return analysis.createAbstractValue(lub, lubTypeMirror); + canBeMissingAnnotations(upperBoundTypeMirror)); + return analysis.createAbstractValue(lub, upperBoundTypeMirror); } /** From c54834be42dd659fc314cc4ca3abf714945af98d Mon Sep 17 00:00:00 2001 From: Manu Sridharan Date: Wed, 29 Nov 2023 08:50:52 -0800 Subject: [PATCH 05/19] Model try-with-resources semantics during CFG construction (#6273) Co-authored-by: Michael Ernst --- .../MustCallAnnotatedTypeFactory.java | 3 - .../checker/mustcall/MustCallTransfer.java | 25 - .../checker/mustcall/MustCallVisitor.java | 70 --- .../MustCallConsistencyAnalyzer.java | 34 +- .../resourceleak/MustCallInference.java | 2 - .../mustcall/TryWithResourcesSimple.java | 12 +- ....java => TryWithResourcesDeclaration.java} | 13 +- .../TryWithResourcesVariable.java | 124 +++++ .../cfg/builder/CFGTranslationPhaseOne.java | 507 ++++++++++++------ .../javacutil/trees/TreeBuilder.java | 34 ++ 10 files changed, 523 insertions(+), 301 deletions(-) rename checker/tests/resourceleak/{TryWithResourcesSimple.java => TryWithResourcesDeclaration.java} (64%) create mode 100644 checker/tests/resourceleak/TryWithResourcesVariable.java 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 87a1efabe18..5f17b97b885 100644 --- a/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallAnnotatedTypeFactory.java @@ -515,9 +515,6 @@ public Void visitIdentifier(IdentifierTree tree, AnnotatedTypeMirror type) { type.replaceAnnotation(BOTTOM); } } - if (ElementUtils.isResourceVariable(elt)) { - type.replaceAnnotation(withoutClose(type.getPrimaryAnnotationInHierarchy(TOP))); - } return super.visitIdentifier(tree, type); } } 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 6b22b3ed4bf..936d6cf4933 100644 --- a/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallTransfer.java +++ b/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallTransfer.java @@ -12,13 +12,11 @@ import javax.lang.model.element.AnnotationMirror; import javax.lang.model.element.Element; import javax.lang.model.type.TypeMirror; -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; import org.checkerframework.dataflow.cfg.node.LocalVariableNode; import org.checkerframework.dataflow.cfg.node.MethodInvocationNode; import org.checkerframework.dataflow.cfg.node.Node; @@ -31,7 +29,6 @@ import org.checkerframework.framework.flow.CFStore; import org.checkerframework.framework.flow.CFTransfer; import org.checkerframework.framework.flow.CFValue; -import org.checkerframework.javacutil.ElementUtils; import org.checkerframework.javacutil.TreePathUtil; import org.checkerframework.javacutil.TreeUtils; import org.checkerframework.javacutil.TypesUtils; @@ -114,28 +111,6 @@ private AnnotationMirror getDefaultStringType(StringConversionNode n) { return this.defaultStringType; } - @Override - public TransferResult visitAssignment( - AssignmentNode n, TransferInput in) { - TransferResult result = super.visitAssignment(n, in); - // Remove "close" from the type in the store for resource variables. - // The Resource Leak Checker relies on this code to avoid checking that - // resource variables are closed. - if (ElementUtils.isResourceVariable(TreeUtils.elementFromTree(n.getTarget().getTree()))) { - CFStore store = result.getRegularStore(); - JavaExpression expr = JavaExpression.fromNode(n.getTarget()); - CFValue value = store.getValue(expr); - AnnotationMirror withClose = - atypeFactory.getAnnotationByClass(value.getAnnotations(), MustCall.class); - if (withClose == null) { - return result; - } - AnnotationMirror withoutClose = atypeFactory.withoutClose(withClose); - insertIntoStores(result, expr, withoutClose); - } - return result; - } - @Override public TransferResult visitMethodInvocation( MethodInvocationNode n, TransferInput in) { 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 368a8508996..397ee34bd94 100644 --- a/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallVisitor.java @@ -17,7 +17,6 @@ import javax.lang.model.element.ExecutableElement; import javax.lang.model.element.TypeElement; import javax.lang.model.type.TypeMirror; -import org.checkerframework.checker.compilermsgs.qual.CompilerMessageKey; import org.checkerframework.checker.mustcall.qual.InheritableMustCall; import org.checkerframework.checker.mustcall.qual.MustCall; import org.checkerframework.checker.mustcall.qual.MustCallAlias; @@ -267,75 +266,6 @@ protected boolean skipReceiverSubtypeCheck( return true; } - /** - * This boolean is used to communicate between different levels of the common assignment check - * whether a given check is being carried out on a (pseudo-)assignment to a resource variable. In - * those cases, close doesn't need to be considered when doing the check, since close will always - * be called by Java. - * - *

    The check for whether the LHS is a resource variable can only be carried out on the element, - * but the effect needs to happen at the stage where the type is available (i.e. close needs to be - * removed from the type). Thus, this variable is used to communicate that a resource variable was - * detected on the LHS. - */ - private boolean commonAssignmentCheckOnResourceVariable = false; - - /** - * {@inheritDoc} - * - *

    Mark (using the {@code #commonAssignmentCheckOnResourceVariable} field of this class) any - * assignments where the LHS is a resource variable, so that close doesn't need to be considered. - * See {@link #commonAssignmentCheck(AnnotatedTypeMirror, AnnotatedTypeMirror, Tree, String, - * Object...)} for the code that uses and removes the mark. - */ - @Override - protected boolean commonAssignmentCheck( - Tree varTree, - ExpressionTree valueExp, - @CompilerMessageKey String errorKey, - Object... extraArgs) { - Element elt = TreeUtils.elementFromTree(varTree); - if (elt != null && elt.getKind() == ElementKind.RESOURCE_VARIABLE) { - commonAssignmentCheckOnResourceVariable = true; - } - return super.commonAssignmentCheck(varTree, valueExp, errorKey, extraArgs); - } - - /** - * {@inheritDoc} - * - *

    Iff the LHS is a resource variable, then {@code #commonAssignmentCheckOnResourceVariable} - * will be true. This method guarantees that {@code #commonAssignmentCheckOnResourceVariable} will - * be false when it returns. - */ - @Override - protected boolean commonAssignmentCheck( - AnnotatedTypeMirror varType, - AnnotatedTypeMirror valueType, - Tree valueTree, - @CompilerMessageKey String errorKey, - Object... extraArgs) { - - if (commonAssignmentCheckOnResourceVariable) { - commonAssignmentCheckOnResourceVariable = false; - // The LHS has been marked as a resource variable. Skip the standard common assignment - // check; instead do a check that does not include "close". - AnnotationMirror varAnno = varType.getPrimaryAnnotationInHierarchy(atypeFactory.TOP); - AnnotationMirror valueAnno = valueType.getPrimaryAnnotationInHierarchy(atypeFactory.TOP); - if (qualHierarchy.isSubtypeShallow( - atypeFactory.withoutClose(valueAnno), - valueType.getUnderlyingType(), - atypeFactory.withoutClose(varAnno), - varType.getUnderlyingType())) { - return true; - } - // Note that in this case, the rest of the common assignment check should fail (barring - // an exception). Control falls through here to avoid duplicating error-issuing code. - } - // commonAssignmentCheckOnResourceVariable is already false, so no need to set it. - return super.commonAssignmentCheck(varType, valueType, valueTree, errorKey, extraArgs); - } - /** * This method typically issues a warning if the result type of the constructor is not top, * because in top-default type systems that indicates a potential problem. The Must Call Checker 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 f5fd3c0250a..ff6f7d7bf5f 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java @@ -74,7 +74,6 @@ import org.checkerframework.dataflow.util.NodeUtils; import org.checkerframework.framework.flow.CFStore; import org.checkerframework.framework.flow.CFValue; -import org.checkerframework.framework.type.AnnotatedTypeMirror; import org.checkerframework.framework.util.JavaExpressionParseUtil.JavaExpressionParseException; import org.checkerframework.framework.util.StringToJavaExpression; import org.checkerframework.javacutil.AnnotationUtils; @@ -711,8 +710,7 @@ private void checkCreatesMustCallForInvocation( *

  • 2) the expression already has a tracked Obligation (i.e. there is already a resource * alias in some Obligation's resource alias set that refers to the expression), or *
  • 3) the method in which the invocation occurs also has an @CreatesMustCallFor annotation, - * with the same expression, or - *
  • 4) the expression is a resource variable. + * with the same expression. * * * @param obligations the currently-tracked Obligations; this value is side-effected if there is @@ -739,10 +737,6 @@ private boolean isValidCreatesMustCallForExpression( // formal parameters are also represented by LocalVariable in the bodies of methods. // This satisfies case 1. return true; - } else if (ElementUtils.isResourceVariable(elt)) { - // The expression is a resource variable, and therefore will be closed, so we can - // treat it as owning (case 4). - return true; } else { Obligation toRemove = null; Obligation toAdd = null; @@ -1224,16 +1218,6 @@ private void updateObligationsForAssignment( new ResourceAlias(JavaExpression.fromNode(lhs), lhsElement, lhs.getTree())); } } - } else if (lhsElement.getKind() == ElementKind.RESOURCE_VARIABLE && isMustCallClose(rhs)) { - if (rhs instanceof FieldAccessNode) { - // Handling of @Owning fields is a completely separate check. - } else if (rhs instanceof LocalVariableNode) { - removeObligationsContainingVar( - obligations, - (LocalVariableNode) rhs, - MustCallAliasHandling.RETAIN_OBLIGATIONS_DERIVED_FROM_A_MUST_CALL_ALIAS_PARAMETER, - MethodExitKind.ALL); - } } else if (lhs instanceof LocalVariableNode) { LocalVariableNode lhsVar = (LocalVariableNode) lhs; updateObligationsForPseudoAssignment(obligations, assignmentNode, lhsVar, rhs); @@ -1264,22 +1248,6 @@ private boolean hasAtMostOneOwningField(TypeElement element) { return true; } - /** - * Returns true if must-call type of node only contains close. This is a helper method for - * handling try-with-resources statements. - * - * @param node the node - * @return true if must-call type of node only contains close - */ - /*package-private*/ boolean isMustCallClose(Node node) { - MustCallAnnotatedTypeFactory mcAtf = - typeFactory.getTypeFactoryOfSubchecker(MustCallChecker.class); - AnnotatedTypeMirror mustCallAnnotatedType = mcAtf.getAnnotatedType(node.getTree()); - AnnotationMirror mustCallAnnotation = - mustCallAnnotatedType.getPrimaryAnnotation(MustCall.class); - return typeFactory.getMustCallValues(mcAtf.withoutClose(mustCallAnnotation)).isEmpty(); - } - /** * Add a new alias to all Obligations that have {@code var} in their resource-alias set. This * method should be used when {@code var} and {@code newAlias} definitively point to the same 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 2e04ce118b8..506ed69f0c8 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInference.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInference.java @@ -369,8 +369,6 @@ private void analyzeOwnershipTransferAtAssignment( 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); diff --git a/checker/tests/mustcall/TryWithResourcesSimple.java b/checker/tests/mustcall/TryWithResourcesSimple.java index 79ff6497680..8c018db4446 100644 --- a/checker/tests/mustcall/TryWithResourcesSimple.java +++ b/checker/tests/mustcall/TryWithResourcesSimple.java @@ -1,4 +1,4 @@ -// A test that try-with-resources variables are always @MustCall({}). +// A test that try-with-resources variables are always @MustCall({"close"}). import java.io.*; import java.net.*; @@ -7,7 +7,7 @@ public class TryWithResourcesSimple { static void test(String address, int port) { try (Socket socket = new Socket(address, port)) { - @MustCall({}) Object s = socket; + @MustCall({"close"}) Object s = socket; } catch (Exception e) { } @@ -23,7 +23,7 @@ void test_fancy_sock(String address, int port) { // "close", which is the only MC method for Socket itself. try (Socket socket = getFancySocket()) { // :: error: (assignment) - @MustCall({}) Object s = socket; + @MustCall({"close"}) Object s = socket; } catch (Exception e) { } @@ -31,8 +31,8 @@ void test_fancy_sock(String address, int port) { static void test_poly(String address, int port) { try (Socket socket = new Socket(address, port)) { - // getChannel is @MustCallAlias (= poly) with the socket, so it should also be @MC({}) - @MustCall({}) Object s = socket.getChannel(); + // getChannel is @MustCallAlias (= poly) with the socket, so it should also be @MC({"close"}) + @MustCall({"close"}) Object s = socket.getChannel(); } catch (Exception e) { } @@ -41,7 +41,7 @@ static void test_poly(String address, int port) { static void test_two_mca_variables(String address, int port) { try (Socket socket = new Socket(address, port); InputStream in = socket.getInputStream()) { - @MustCall({}) Object s = in; + @MustCall({"close"}) Object s = in; } catch (Exception e) { } diff --git a/checker/tests/resourceleak/TryWithResourcesSimple.java b/checker/tests/resourceleak/TryWithResourcesDeclaration.java similarity index 64% rename from checker/tests/resourceleak/TryWithResourcesSimple.java rename to checker/tests/resourceleak/TryWithResourcesDeclaration.java index c53ccdaab94..b25e22eaaf9 100644 --- a/checker/tests/resourceleak/TryWithResourcesSimple.java +++ b/checker/tests/resourceleak/TryWithResourcesDeclaration.java @@ -1,11 +1,11 @@ -// A simple test that a try-with-resources socket doesn't issue a false positive. +// Tests for try-with-resources that declare local variables in the resource declaration. import java.io.*; import java.net.Socket; import java.nio.channels.*; import java.util.*; -class TryWithResourcesSimple { +class TryWithResourcesDeclaration { static void test(String address, int port) { try (Socket socket = new Socket(address, port)) { @@ -31,4 +31,13 @@ public boolean isPreUpgradableLayout(File oldF) throws IOException { return false; } } + + public void testNestedTryWithResourcesDecls(Properties prop, ClassLoader cl, String propfile) + throws Exception { + try (InputStream in = cl.getResourceAsStream(propfile)) { + try (InputStream fis = new FileInputStream(propfile)) { + prop.load(fis); + } + } + } } diff --git a/checker/tests/resourceleak/TryWithResourcesVariable.java b/checker/tests/resourceleak/TryWithResourcesVariable.java new file mode 100644 index 00000000000..26be08d9a56 --- /dev/null +++ b/checker/tests/resourceleak/TryWithResourcesVariable.java @@ -0,0 +1,124 @@ +// Test for try-with-resources where the resource declaration uses an existing variable + +import java.io.*; +import java.net.*; +import org.checkerframework.checker.calledmethods.qual.*; +import org.checkerframework.checker.mustcall.qual.*; + +class TryWithResourcesVariable { + static void test1() throws Exception { + Socket socket = new Socket("127.0.0.1", 5050); + try (socket) { + + } catch (Exception e) { + + } + } + + static void test2(@Owning Socket socket) { + try (socket) { + + } catch (Exception e) { + + } + } + + static void test3(InetSocketAddress isa) { + Socket socket = new Socket(); + try (socket) { + socket.connect(isa); + } catch (Exception e) { + + } + } + + // :: error: (required.method.not.called) + static void test4(@Owning InputStream i1, @Owning InputStream i2) { + try { + try (i2) {} + // This will not run if i2.close() throws an IOException + i1.close(); + } catch (Exception e) { + + } + } + + static void test4Fixed(@Owning InputStream i1, @Owning InputStream i2) throws IOException { + try { + try (i2) {} + } catch (Exception e) { + } + i1.close(); + } + + @InheritableMustCall("disposer") + static class FinalResourceField { + final @Owning Socket socketField; + + FinalResourceField() { + try { + socketField = new Socket("127.0.0.1", 5050); + } catch (Exception e) { + throw new RuntimeException(e); + } + } + + @EnsuresCalledMethods(value = "this.socketField", methods = "close") + void disposer() { + try (socketField) { + + } catch (Exception e) { + + } + } + } + + static void closeFinalFieldUnsupported() throws Exception { + // This is a false positive (i.e., there is no resource leak), but our checker reports a warning + // since it does not support this coding pattern + // :: error: (required.method.not.called) + FinalResourceField finalResourceField = new FinalResourceField(); + try (finalResourceField.socketField) {} + } + + @InheritableMustCall("disposer") + static class FinalResourceFieldWrapper { + + final @Owning FinalResourceField frField = new FinalResourceField(); + + @EnsuresCalledMethods(value = "this.frField", methods = "disposer") + void disposer() { + this.frField.disposer(); + } + } + + static void closeWrapperUnsupported() throws Exception { + // This is a false positive (i.e., there is no resource leak), but our checker reports a warning + // since it does not support this coding pattern + // :: error: (required.method.not.called) + FinalResourceFieldWrapper finalResourceFieldWrapper = new FinalResourceFieldWrapper(); + try (finalResourceFieldWrapper.frField.socketField) {} + } + + @InheritableMustCall("disposer") + static class TwoFinalResourceFields { + final @Owning Socket socketField1; + final @Owning Socket socketField2; + + TwoFinalResourceFields(@Owning Socket socket1, @Owning Socket socket2) { + socketField1 = socket1; + socketField2 = socket2; + } + + @EnsuresCalledMethods(value = "this.socketField1", methods = "close") + @EnsuresCalledMethods(value = "this.socketField2", methods = "close") + void disposer() { + try (socketField1; + socketField2) { + + } catch (Exception e) { + + } + } + } +} diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java index 6fee5c1095a..b2f13fe473f 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java @@ -1503,15 +1503,7 @@ public MethodInvocationNode visitMethodInvocation(MethodInvocationTree tree, Voi MethodInvocationNode node = new MethodInvocationNode(tree, target, arguments, getCurrentPath()); - List thrownTypes = method.getThrownTypes(); - Set thrownSet = - new LinkedHashSet<>(thrownTypes.size() + uncheckedExceptionTypes.size()); - // Add exceptions explicitly mentioned in the throws clause. - thrownSet.addAll(thrownTypes); - // Add types to account for unchecked exceptions - thrownSet.addAll(uncheckedExceptionTypes); - - ExtendedNode extendedNode = extendWithNodeWithExceptions(node, thrownSet); + ExtendedNode extendedNode = extendWithMethodInvocationNode(method, node); /* Check for the TerminatesExecution annotation. */ boolean terminatesExecution = @@ -1523,6 +1515,27 @@ public MethodInvocationNode visitMethodInvocation(MethodInvocationTree tree, Voi return node; } + /** + * Extends the CFG with a MethodInvocationNode, accounting for potential exceptions thrown by the + * invocation. + * + * @param method the invoked method + * @param node the invocation + * @return an ExtendedNode representing the invocation and its possible thrown exceptions + */ + private ExtendedNode extendWithMethodInvocationNode( + ExecutableElement method, MethodInvocationNode node) { + List thrownTypes = method.getThrownTypes(); + Set thrownSet = + new LinkedHashSet<>(thrownTypes.size() + uncheckedExceptionTypes.size()); + // Add exceptions explicitly mentioned in the throws clause. + thrownSet.addAll(thrownTypes); + // Add types to account for unchecked exceptions + thrownSet.addAll(uncheckedExceptionTypes); + + return extendWithNodeWithExceptions(node, thrownSet); + } + @Override public Node visitAssert(AssertTree tree, Void p) { @@ -3534,9 +3547,7 @@ public Node visitTry(TryTree tree, Void p) { List> catchLabels = CollectionsPlume.mapList( - (CatchTree c) -> { - return IPair.of(TreeUtils.typeOf(c.getParameter().getType()), new Label()); - }, + (CatchTree c) -> IPair.of(TreeUtils.typeOf(c.getParameter().getType()), new Label()), catches); // Store return/break/continue labels, just in case we need them for a finally block. @@ -3568,25 +3579,19 @@ public Node visitTry(TryTree tree, Void p) { tryStack.pushFrame(new TryCatchFrame(types, catchLabels)); - // Must scan the resources *after* we push frame to tryStack. Otherwise we can lose catch - // blocks. - // TODO: Should we handle try-with-resources blocks by also generating code for - // automatically closing the resources? - List resources = tree.getResources(); - for (Tree resource : resources) { - scan(resource, p); - } - extendWithNode( new MarkerNode( tree, "start of try block #" + TreeUtils.treeUids.get(tree), env.getTypeUtils())); - scan(tree.getBlock(), p); + + handleTryResourcesAndBlock(tree, p, tree.getResources()); + extendWithNode( new MarkerNode( tree, "end of try block #" + TreeUtils.treeUids.get(tree), env.getTypeUtils())); extendWithExtendedNode(new UnconditionalJump(firstNonNull(finallyLabel, doneLabel))); + // This pops the try-catch frame tryStack.popFrame(); int catchIndex = 0; @@ -3602,172 +3607,354 @@ public Node visitTry(TryTree tree, Void p) { } if (finallyLabel != null) { - // Reset values before analyzing the finally block! + handleFinally( + tree, + doneLabel, + finallyLabel, + exceptionalFinallyLabel, + () -> scan(finallyBlock, p), + oldReturnTargetLC, + oldBreakTargetLC, + oldBreakLabels, + oldContinueTargetLC, + oldContinueLabels); + } - tryStack.popFrame(); + addLabelForNextNode(doneLabel); - { // Scan 'finallyBlock' for only 'finallyLabel' (a successful path) - addLabelForNextNode(finallyLabel); - extendWithNode( - new MarkerNode( - tree, - "start of finally block #" + TreeUtils.treeUids.get(tree), - env.getTypeUtils())); - scan(finallyBlock, p); - extendWithNode( - new MarkerNode( - tree, "end of finally block #" + TreeUtils.treeUids.get(tree), env.getTypeUtils())); - extendWithExtendedNode(new UnconditionalJump(doneLabel)); - } + return null; + } - if (hasExceptionalPath(exceptionalFinallyLabel)) { - // If an exceptional path exists, scan 'finallyBlock' for 'exceptionalFinallyLabel', - // and scan copied 'finallyBlock' for 'finallyLabel' (a successful path). If there - // is no successful path, it will be removed in later phase. - // TODO: Don't we need a separate finally block for each kind of exception? - addLabelForNextNode(exceptionalFinallyLabel); - extendWithNode( - new MarkerNode( - tree, - "start of finally block for Throwable #" + TreeUtils.treeUids.get(tree), - env.getTypeUtils())); + /** + * A recursive helper method to handle the resource declarations (if any) in a {@link TryTree} and + * its main block. If the {@code resources} list is empty, the method scans the main block of the + * try statement and returns. Otherwise, the first resource declaration in {@code resources} is + * desugared, following the logic in JLS 14.20.3.1. A resource declaration r is desugared + * by adding the nodes for r itself to the CFG, followed by a synthetic nested {@code try} + * block and {@code finally} block. The synthetic {@code try} block contains any remaining + * resource declarations and the original try block (handled via recursion). The synthetic {@code + * finally} block contains a call to {@code close} for r, guaranteeing that on every path + * through the CFG, r is closed. + * + * @param tryTree the original try tree (with 0 or more resources) from the AST + * @param p the value to pass to calls to {@code scan} + * @param resources the remaining resource declarations to handle + */ + private void handleTryResourcesAndBlock(TryTree tryTree, Void p, List resources) { + if (resources.isEmpty()) { + // Either `tryTree` was not a try-with-resources, or this method was called recursively and + // all the resources have been handled. Just scan the main try block. + scan(tryTree.getBlock(), p); + return; + } - scan(finallyBlock, p); + // Handle the first resource declaration in the list. The rest will be handled by a recursive + // call. + Tree resourceDeclarationTree = resources.get(0); - NodeWithExceptionsHolder throwing = - extendWithNodeWithException( - new MarkerNode( - tree, - "end of finally block for Throwable #" + TreeUtils.treeUids.get(tree), - env.getTypeUtils()), - throwableType); + extendWithNode( + new MarkerNode( + resourceDeclarationTree, + "start of try for resource #" + TreeUtils.treeUids.get(resourceDeclarationTree), + env.getTypeUtils())); - throwing.setTerminatesExecution(true); - } + // Store return/break/continue labels. Generating a synthetic finally block for closing the + // resource requires creating fresh return/break/continue labels and then restoring the old + // labels afterward. + LabelCell oldReturnTargetLC = returnTargetLC; + LabelCell oldBreakTargetLC = breakTargetLC; + Map oldBreakLabels = breakLabels; + LabelCell oldContinueTargetLC = continueTargetLC; + Map oldContinueLabels = continueLabels; - if (returnTargetLC.wasAccessed()) { - addLabelForNextNode(returnTargetLC.peekLabel()); - returnTargetLC = oldReturnTargetLC; + // Add nodes for the resource declaration to the CFG. NOTE: it is critical to add these nodes + // *before* pushing a TryFinallyFrame for the finally block that will close the resource. If + // any exception occurs due to code within the resource declaration, the corresponding variable + // or field is *not* automatically closed (as it was never assigned a value). + Node resourceCloseNode = scan(resourceDeclarationTree, p); - extendWithNode( - new MarkerNode( - tree, - "start of finally block for return #" + TreeUtils.treeUids.get(tree), - env.getTypeUtils())); - scan(finallyBlock, p); - extendWithNode( - new MarkerNode( - tree, - "end of finally block for return #" + TreeUtils.treeUids.get(tree), - env.getTypeUtils())); - extendWithExtendedNode(new UnconditionalJump(returnTargetLC.accessLabel())); - } else { - returnTargetLC = oldReturnTargetLC; - } + // Now, set things up for our synthetic finally block that closes the resource. + Label doneLabel = new Label(); + Label finallyLabel = new Label(); + + Label exceptionalFinallyLabel = new Label(); + tryStack.pushFrame(new TryFinallyFrame(exceptionalFinallyLabel)); + + returnTargetLC = new LabelCell(); + + breakTargetLC = new LabelCell(); + breakLabels = new TryFinallyScopeMap(); + + continueTargetLC = new LabelCell(); + continueLabels = new TryFinallyScopeMap(); - if (breakTargetLC.wasAccessed()) { - addLabelForNextNode(breakTargetLC.peekLabel()); - breakTargetLC = oldBreakTargetLC; + extendWithNode( + new MarkerNode( + resourceDeclarationTree, + "start of try block for resource #" + TreeUtils.treeUids.get(resourceDeclarationTree), + env.getTypeUtils())); + // Recursively handle any remaining resource declarations and the main block of the try + handleTryResourcesAndBlock(tryTree, p, resources.subList(1, resources.size())); + extendWithNode( + new MarkerNode( + resourceDeclarationTree, + "end of try block for resource #" + TreeUtils.treeUids.get(resourceDeclarationTree), + env.getTypeUtils())); + + extendWithExtendedNode(new UnconditionalJump(finallyLabel)); + + // Generate the finally block that closes the resource + handleFinally( + resourceDeclarationTree, + doneLabel, + finallyLabel, + exceptionalFinallyLabel, + () -> addCloseCallForResource(resourceDeclarationTree, resourceCloseNode), + oldReturnTargetLC, + oldBreakTargetLC, + oldBreakLabels, + oldContinueTargetLC, + oldContinueLabels); + + addLabelForNextNode(doneLabel); + } + + /** + * Adds a synthetic {@code close} call to the CFG to close some resource variable declared or used + * in a try-with-resources. + * + * @param resourceDeclarationTree the resource declaration + * @param resourceToCloseNode node represented the variable or field on which {@code close} should + * be invoked + */ + private void addCloseCallForResource(Tree resourceDeclarationTree, Node resourceToCloseNode) { + Tree receiverTree = resourceDeclarationTree; + if (receiverTree instanceof VariableTree) { + receiverTree = treeBuilder.buildVariableUse((VariableTree) receiverTree); + handleArtificialTree(receiverTree); + } + + MemberSelectTree closeSelect = + treeBuilder.buildCloseMethodAccess((ExpressionTree) receiverTree); + handleArtificialTree(closeSelect); + + MethodInvocationTree closeCall = treeBuilder.buildMethodInvocation(closeSelect); + handleArtificialTree(closeCall); + + Node receiverNode = resourceToCloseNode; + if (receiverNode instanceof AssignmentNode) { + // variable declaration; use the LHS + receiverNode = ((AssignmentNode) resourceToCloseNode).getTarget(); + } + // TODO do we need to insert some kind of node representing a use of receiverNode + // (which can be either a LocalVariableNode or a FieldAccessNode)? + MethodAccessNode closeAccessNode = new MethodAccessNode(closeSelect, receiverNode); + closeAccessNode.setInSource(false); + extendWithNode(closeAccessNode); + MethodInvocationNode closeCallNode = + new MethodInvocationNode( + closeCall, closeAccessNode, Collections.emptyList(), getCurrentPath()); + closeCallNode.setInSource(false); + extendWithMethodInvocationNode(TreeUtils.elementFromUse(closeCall), closeCallNode); + } + + /** + * Shared logic for CFG generation for a finally block. The block may correspond to a {@link + * TryTree} originally in the source code, or it may be a synthetic finally block used to model + * closing of a resource due to try-with-resources. + * + * @param markerTree tree to reference when creating {@link MarkerNode}s for the finally block + * @param doneLabel label for the normal successor of the try block (no exceptions, returns, + * breaks, or continues) + * @param finallyLabel label for the entry of the finally block for the normal case + * @param exceptionalFinallyLabel label for entry of the finally block for when the try block + * throws an exception + * @param finallyBlockCFGGenerator generates CFG nodes and edges for the finally block + * @param oldReturnTargetLC old return target label cell, which gets restored to {@link + * #returnTargetLC} while handling the finally block + * @param oldBreakTargetLC old break target label cell, which gets restored to {@link + * #breakTargetLC} while handling the finally block + * @param oldBreakLabels old break labels, which get restored to {@link #breakLabels} while + * handling the finally block + * @param oldContinueTargetLC old continue target label cell, which gets restored to {@link + * #continueTargetLC} while handling the finally block + * @param oldContinueLabels old continue labels, which get restored to {@link #continueLabels} + * while handling the finally block + */ + private void handleFinally( + Tree markerTree, + Label doneLabel, + Label finallyLabel, + Label exceptionalFinallyLabel, + Runnable finallyBlockCFGGenerator, + LabelCell oldReturnTargetLC, + LabelCell oldBreakTargetLC, + Map oldBreakLabels, + LabelCell oldContinueTargetLC, + Map oldContinueLabels) { + // Reset values before analyzing the finally block! + + tryStack.popFrame(); + + { // Scan 'finallyBlock' for only 'finallyLabel' (a successful path) + addLabelForNextNode(finallyLabel); + extendWithNode( + new MarkerNode( + markerTree, + "start of finally block #" + TreeUtils.treeUids.get(markerTree), + env.getTypeUtils())); + finallyBlockCFGGenerator.run(); + extendWithNode( + new MarkerNode( + markerTree, + "end of finally block #" + TreeUtils.treeUids.get(markerTree), + env.getTypeUtils())); + extendWithExtendedNode(new UnconditionalJump(doneLabel)); + } + + if (hasExceptionalPath(exceptionalFinallyLabel)) { + // If an exceptional path exists, scan 'finallyBlock' for 'exceptionalFinallyLabel', + // and scan copied 'finallyBlock' for 'finallyLabel' (a successful path). If there + // is no successful path, it will be removed in later phase. + // TODO: Don't we need a separate finally block for each kind of exception? + addLabelForNextNode(exceptionalFinallyLabel); + extendWithNode( + new MarkerNode( + markerTree, + "start of finally block for Throwable #" + TreeUtils.treeUids.get(markerTree), + env.getTypeUtils())); + + finallyBlockCFGGenerator.run(); + + NodeWithExceptionsHolder throwing = + extendWithNodeWithException( + new MarkerNode( + markerTree, + "end of finally block for Throwable #" + TreeUtils.treeUids.get(markerTree), + env.getTypeUtils()), + throwableType); + + throwing.setTerminatesExecution(true); + } + + if (returnTargetLC.wasAccessed()) { + addLabelForNextNode(returnTargetLC.peekLabel()); + returnTargetLC = oldReturnTargetLC; + + extendWithNode( + new MarkerNode( + markerTree, + "start of finally block for return #" + TreeUtils.treeUids.get(markerTree), + env.getTypeUtils())); + finallyBlockCFGGenerator.run(); + extendWithNode( + new MarkerNode( + markerTree, + "end of finally block for return #" + TreeUtils.treeUids.get(markerTree), + env.getTypeUtils())); + extendWithExtendedNode(new UnconditionalJump(returnTargetLC.accessLabel())); + } else { + returnTargetLC = oldReturnTargetLC; + } + + if (breakTargetLC.wasAccessed()) { + addLabelForNextNode(breakTargetLC.peekLabel()); + breakTargetLC = oldBreakTargetLC; + extendWithNode( + new MarkerNode( + markerTree, + "start of finally block for break #" + TreeUtils.treeUids.get(markerTree), + env.getTypeUtils())); + finallyBlockCFGGenerator.run(); + extendWithNode( + new MarkerNode( + markerTree, + "end of finally block for break #" + TreeUtils.treeUids.get(markerTree), + env.getTypeUtils())); + extendWithExtendedNode(new UnconditionalJump(breakTargetLC.accessLabel())); + } else { + breakTargetLC = oldBreakTargetLC; + } + + Map accessedBreakLabels = ((TryFinallyScopeMap) breakLabels).getAccessedNames(); + if (!accessedBreakLabels.isEmpty()) { + breakLabels = oldBreakLabels; + + for (Map.Entry access : accessedBreakLabels.entrySet()) { + addLabelForNextNode(access.getValue()); extendWithNode( new MarkerNode( - tree, - "start of finally block for break #" + TreeUtils.treeUids.get(tree), + markerTree, + "start of finally block for break label " + + access.getKey() + + " #" + + TreeUtils.treeUids.get(markerTree), env.getTypeUtils())); - scan(finallyBlock, p); + finallyBlockCFGGenerator.run(); extendWithNode( new MarkerNode( - tree, - "end of finally block for break #" + TreeUtils.treeUids.get(tree), + markerTree, + "end of finally block for break label " + + access.getKey() + + " #" + + TreeUtils.treeUids.get(markerTree), env.getTypeUtils())); - extendWithExtendedNode(new UnconditionalJump(breakTargetLC.accessLabel())); - } else { - breakTargetLC = oldBreakTargetLC; + extendWithExtendedNode(new UnconditionalJump(breakLabels.get(access.getKey()))); } + } else { + breakLabels = oldBreakLabels; + } - Map accessedBreakLabels = ((TryFinallyScopeMap) breakLabels).getAccessedNames(); - if (!accessedBreakLabels.isEmpty()) { - breakLabels = oldBreakLabels; - - for (Map.Entry access : accessedBreakLabels.entrySet()) { - addLabelForNextNode(access.getValue()); - extendWithNode( - new MarkerNode( - tree, - "start of finally block for break label " - + access.getKey() - + " #" - + TreeUtils.treeUids.get(tree), - env.getTypeUtils())); - scan(finallyBlock, p); - extendWithNode( - new MarkerNode( - tree, - "end of finally block for break label " - + access.getKey() - + " #" - + TreeUtils.treeUids.get(tree), - env.getTypeUtils())); - extendWithExtendedNode(new UnconditionalJump(breakLabels.get(access.getKey()))); - } - } else { - breakLabels = oldBreakLabels; - } + if (continueTargetLC.wasAccessed()) { + addLabelForNextNode(continueTargetLC.peekLabel()); + continueTargetLC = oldContinueTargetLC; + + extendWithNode( + new MarkerNode( + markerTree, + "start of finally block for continue #" + TreeUtils.treeUids.get(markerTree), + env.getTypeUtils())); + finallyBlockCFGGenerator.run(); + extendWithNode( + new MarkerNode( + markerTree, + "end of finally block for continue #" + TreeUtils.treeUids.get(markerTree), + env.getTypeUtils())); + extendWithExtendedNode(new UnconditionalJump(continueTargetLC.accessLabel())); + } else { + continueTargetLC = oldContinueTargetLC; + } - if (continueTargetLC.wasAccessed()) { - addLabelForNextNode(continueTargetLC.peekLabel()); - continueTargetLC = oldContinueTargetLC; + Map accessedContinueLabels = + ((TryFinallyScopeMap) continueLabels).getAccessedNames(); + if (!accessedContinueLabels.isEmpty()) { + continueLabels = oldContinueLabels; + for (Map.Entry access : accessedContinueLabels.entrySet()) { + addLabelForNextNode(access.getValue()); extendWithNode( new MarkerNode( - tree, - "start of finally block for continue #" + TreeUtils.treeUids.get(tree), + markerTree, + "start of finally block for continue label " + + access.getKey() + + " #" + + TreeUtils.treeUids.get(markerTree), env.getTypeUtils())); - scan(finallyBlock, p); + finallyBlockCFGGenerator.run(); extendWithNode( new MarkerNode( - tree, - "end of finally block for continue #" + TreeUtils.treeUids.get(tree), + markerTree, + "end of finally block for continue label " + + access.getKey() + + " #" + + TreeUtils.treeUids.get(markerTree), env.getTypeUtils())); - extendWithExtendedNode(new UnconditionalJump(continueTargetLC.accessLabel())); - } else { - continueTargetLC = oldContinueTargetLC; - } - - Map accessedContinueLabels = - ((TryFinallyScopeMap) continueLabels).getAccessedNames(); - if (!accessedContinueLabels.isEmpty()) { - continueLabels = oldContinueLabels; - - for (Map.Entry access : accessedContinueLabels.entrySet()) { - addLabelForNextNode(access.getValue()); - extendWithNode( - new MarkerNode( - tree, - "start of finally block for continue label " - + access.getKey() - + " #" - + TreeUtils.treeUids.get(tree), - env.getTypeUtils())); - scan(finallyBlock, p); - extendWithNode( - new MarkerNode( - tree, - "end of finally block for continue label " - + access.getKey() - + " #" - + TreeUtils.treeUids.get(tree), - env.getTypeUtils())); - extendWithExtendedNode(new UnconditionalJump(continueLabels.get(access.getKey()))); - } - } else { - continueLabels = oldContinueLabels; + extendWithExtendedNode(new UnconditionalJump(continueLabels.get(access.getKey()))); } + } else { + continueLabels = oldContinueLabels; } - - addLabelForNextNode(doneLabel); - - return null; } /** diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/trees/TreeBuilder.java b/javacutil/src/main/java/org/checkerframework/javacutil/trees/TreeBuilder.java index 7cac9176956..87c3d7047be 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/trees/TreeBuilder.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/trees/TreeBuilder.java @@ -126,6 +126,40 @@ public MemberSelectTree buildIteratorMethodAccess(ExpressionTree iterableExpr) { return iteratorAccess; } + /** + * Build a {@link MemberSelectTree} for accessing the {@code close} method of an expression that + * implements {@link AutoCloseable}. This method is used when desugaring try-with-resources + * statements during CFG construction. + * + * @param autoCloseableExpr the expression + * @return the member select tree + */ + public MemberSelectTree buildCloseMethodAccess(ExpressionTree autoCloseableExpr) { + DeclaredType exprType = + (DeclaredType) TypesUtils.upperBound(TreeUtils.typeOf(autoCloseableExpr)); + assert exprType != null + : "expression must be of declared type AutoCloseable: " + autoCloseableExpr; + + TypeElement exprElement = (TypeElement) exprType.asElement(); + + // Find the close() method + Symbol.MethodSymbol closeMethod = null; + + for (ExecutableElement method : ElementFilter.methodsIn(elements.getAllMembers(exprElement))) { + if (method.getParameters().isEmpty() && method.getSimpleName().contentEquals("close")) { + closeMethod = (Symbol.MethodSymbol) method; + break; + } + } + + assert closeMethod != null + : "@AssumeAssertion(nullness): no close method declared for expression type"; + + JCTree.JCFieldAccess closeAccess = TreeUtils.Select(maker, autoCloseableExpr, closeMethod); + + return closeAccess; + } + /** * Builds an AST Tree to access the hasNext() method of an iterator. * From 0291d63363b985956a97b5532397e74888e07c4e Mon Sep 17 00:00:00 2001 From: Suzanne Millstein Date: Wed, 29 Nov 2023 15:16:40 -0800 Subject: [PATCH 06/19] Copy Enum supertype to avoid infinite loop --- .../framework/util/AnnotatedTypes.java | 10 ++++++++++ framework/tests/all-systems/Issue6319.java | 10 ++++++++++ 2 files changed, 20 insertions(+) create mode 100644 framework/tests/all-systems/Issue6319.java diff --git a/framework/src/main/java/org/checkerframework/framework/util/AnnotatedTypes.java b/framework/src/main/java/org/checkerframework/framework/util/AnnotatedTypes.java index a594fa94ba4..2d7b55ea3cf 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/AnnotatedTypes.java +++ b/framework/src/main/java/org/checkerframework/framework/util/AnnotatedTypes.java @@ -140,6 +140,16 @@ public static T castedAsSuper( return copy; } + Elements elements = atypeFactory.getProcessingEnv().getElementUtils(); + if (supertype != null + && AnnotatedTypes.isEnum(supertype) + && AnnotatedTypes.isDeclarationOfJavaLangEnum(types, elements, supertype)) { + // Don't return the asSuper result because it causes an infinite loop. + @SuppressWarnings("unchecked") + T result = (T) supertype.deepCopy(); + return result; + } + T asSuperType = AnnotatedTypes.asSuper(atypeFactory, subtype, supertype); fixUpRawTypes(subtype, asSuperType, supertype, types); diff --git a/framework/tests/all-systems/Issue6319.java b/framework/tests/all-systems/Issue6319.java new file mode 100644 index 00000000000..eeb4f362b7f --- /dev/null +++ b/framework/tests/all-systems/Issue6319.java @@ -0,0 +1,10 @@ +import java.util.Comparator; +import java.util.List; +import java.util.stream.Collectors; + +class Issue6319 { + void f(List> list) { + for (Enum value : + list.stream().sorted(Comparator.comparing(Enum::name)).collect(Collectors.toList())) {} + } +} From 7b00efaaa1d8033c14cb289a6cc50930b6e2e3c8 Mon Sep 17 00:00:00 2001 From: Suzanne Millstein Date: Wed, 29 Nov 2023 15:49:14 -0800 Subject: [PATCH 07/19] Treat assert methods as assert statements --- .../dataflow/qual/AssertMethod.java | 69 ++ .../src/main/resources/junit-assertions.astub | 600 ++++++++++++++++++ checker/tests/nullness/AssertMethodTest.java | 87 +++ .../cfg/builder/CFGTranslationPhaseOne.java | 129 +++- .../dataflow/cfg/node/AssertionErrorNode.java | 45 +- 5 files changed, 920 insertions(+), 10 deletions(-) create mode 100644 checker-qual/src/main/java/org/checkerframework/dataflow/qual/AssertMethod.java create mode 100644 checker/src/main/resources/junit-assertions.astub create mode 100644 checker/tests/nullness/AssertMethodTest.java diff --git a/checker-qual/src/main/java/org/checkerframework/dataflow/qual/AssertMethod.java b/checker-qual/src/main/java/org/checkerframework/dataflow/qual/AssertMethod.java new file mode 100644 index 00000000000..4dd0ee58614 --- /dev/null +++ b/checker-qual/src/main/java/org/checkerframework/dataflow/qual/AssertMethod.java @@ -0,0 +1,69 @@ +package org.checkerframework.dataflow.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; + +/** + * {@code AssertMethod} is a method annotation that indicates that a method throws an exception if + * the value of a boolean argument is false. This can be used to annotate methods such as JUnit's + * {@code Assertions.assertTrue(...)}. + * + *

    The annotation enables flow-sensitive type refinement to be more precise. For example, if + * {@code Assertions.assertTrue} is annotated as follows: + * + * 

    @AssertMethod(value = AssertionFailedError.class)
+ * public static void assertFalse(boolean condition);
+ *
    + * + * Then, in the code below, the Optional Checker can determine that {@code optional} has a value and + * the call to {@code Optional#get} will not throw an exception. + * + * 
    + * Assertions.assertTrue(optional.isPresent());
+ * Object o = optional.get();
+ *
    + * + *

    This annotation is a trusted annotation, meaning that the Checker Framework does not + * check whether the annotated method really does throw an exception depending on the boolean + * expression. + * + * @checker_framework.manual #type-refinement Automatic type refinement (flow-sensitive type + * qualifier inference) + */ +@Documented +@Retention(RetentionPolicy.RUNTIME) +@Target(ElementType.METHOD) +public @interface AssertMethod { + + /** + * The class of the exception thrown by this method. The default is {@link AssertionError}. + * + * @return class of the exception thrown by this method + */ + Class value() default AssertionError.class; + + /** + * The one-based index of the boolean parameter that is tested. + * + * @return the one-based index of the boolean parameter that is tested + */ + int parameter() default 1; + + /** + * Returns whether this method asserts that the boolean expression is false. + * + *

    For example, Junit's Assertions.assertFalse(...) + * throws an exception if the first argument is false. So it is annotated as follows: + * + * 

    @AssertMethod(value = AssertionFailedError.class, isAssertFalse = true)
+   * public static void assertFalse(boolean condition);
+   *
    + * + * @return the value for {@link #parameter} on which the method throws an exception + */ + boolean isAssertFalse() default false; +} diff --git a/checker/src/main/resources/junit-assertions.astub b/checker/src/main/resources/junit-assertions.astub new file mode 100644 index 00000000000..85340021684 --- /dev/null +++ b/checker/src/main/resources/junit-assertions.astub @@ -0,0 +1,600 @@ +package org.junit.jupiter.api; + +import java.time.Duration; +import java.util.Arrays; +import java.util.Collection; +import java.util.List; +import java.util.Objects; +import java.util.function.BooleanSupplier; +import java.util.function.Supplier; +import java.util.stream.Stream; + +import org.checkerframework.dataflow.qual.AssertMethod; +import org.opentest4j.AssertionFailedError; + +public class Assertions { + + public static V fail(); + + public static V fail(String message); + + public static V fail(String message, Throwable cause); + + public static V fail(Throwable cause); + + public static V fail(Supplier messageSupplier); + + @AssertMethod(AssertionFailedError.class) + public static void assertTrue(boolean condition); + + @AssertMethod(AssertionFailedError.class) + public static void assertTrue(boolean condition, Supplier messageSupplier); + + public static void assertTrue(BooleanSupplier booleanSupplier); + + public static void assertTrue(BooleanSupplier booleanSupplier, String message); + + @AssertMethod(AssertionFailedError.class) + public static void assertTrue(boolean condition, String message); + + public static void assertTrue(BooleanSupplier booleanSupplier, Supplier messageSupplier); + + @AssertMethod(value = AssertionFailedError.class, isAssertFalse = true) + public static void assertFalse(boolean condition); + + @AssertMethod(value = AssertionFailedError.class, isAssertFalse = true) + public static void assertFalse(boolean condition, String message); + + @AssertMethod(value = AssertionFailedError.class, isAssertFalse = true) + public static void assertFalse(boolean condition, Supplier messageSupplier); + + public static void assertFalse(BooleanSupplier booleanSupplier); + + public static void assertFalse(BooleanSupplier booleanSupplier, String message); + + public static void assertFalse(BooleanSupplier booleanSupplier, Supplier messageSupplier); + + public static void assertNull(Object actual); + + public static void assertNull(Object actual, String message); + + public static void assertNull(Object actual, Supplier messageSupplier); + + public static void assertNotNull(Object actual); + + public static void assertNotNull(Object actual, String message); + + public static void assertNotNull(Object actual, Supplier messageSupplier); + + public static void assertEquals(short expected, short actual); + + public static void assertEquals(short expected, Short actual); + + public static void assertEquals(Short expected, short actual); + + public static void assertEquals(Short expected, Short actual); + + public static void assertEquals(short expected, short actual, String message); + + public static void assertEquals(short expected, Short actual, String message); + + public static void assertEquals(Short expected, short actual, String message); + + public static void assertEquals(Short expected, Short actual, String message); + + public static void assertEquals(short expected, short actual, Supplier messageSupplier); + + public static void assertEquals(short expected, Short actual, Supplier messageSupplier); + + public static void assertEquals(Short expected, short actual, Supplier messageSupplier); + + public static void assertEquals(Short expected, Short actual, Supplier messageSupplier); + + public static void assertEquals(byte expected, byte actual); + + public static void assertEquals(byte expected, Byte actual); + + public static void assertEquals(Byte expected, byte actual); + + public static void assertEquals(Byte expected, Byte actual); + + public static void assertEquals(byte expected, byte actual, String message); + + public static void assertEquals(byte expected, Byte actual, String message); + + public static void assertEquals(Byte expected, byte actual, String message); + + public static void assertEquals(Byte expected, Byte actual, String message); + + public static void assertEquals(byte expected, byte actual, Supplier messageSupplier); + + public static void assertEquals(byte expected, Byte actual, Supplier messageSupplier); + + public static void assertEquals(Byte expected, byte actual, Supplier messageSupplier); + + public static void assertEquals(Byte expected, Byte actual, Supplier messageSupplier); + + public static void assertEquals(int expected, int actual); + + public static void assertEquals(int expected, Integer actual); + + public static void assertEquals(Integer expected, int actual); + + public static void assertEquals(Integer expected, Integer actual); + + public static void assertEquals(int expected, int actual, String message); + + public static void assertEquals(int expected, Integer actual, String message); + + public static void assertEquals(Integer expected, int actual, String message); + + public static void assertEquals(Integer expected, Integer actual, String message); + + public static void assertEquals(int expected, int actual, Supplier messageSupplier); + + public static void assertEquals(int expected, Integer actual, Supplier messageSupplier); + + public static void assertEquals(Integer expected, int actual, Supplier messageSupplier); + + public static void assertEquals(Integer expected, Integer actual, Supplier messageSupplier); + + public static void assertEquals(long expected, long actual); + + public static void assertEquals(long expected, Long actual); + + public static void assertEquals(Long expected, long actual); + + public static void assertEquals(Long expected, Long actual); + + public static void assertEquals(long expected, long actual, String message); + + public static void assertEquals(long expected, Long actual, String message); + + public static void assertEquals(Long expected, long actual, String message); + + public static void assertEquals(Long expected, Long actual, String message); + + public static void assertEquals(long expected, long actual, Supplier messageSupplier); + + public static void assertEquals(long expected, Long actual, Supplier messageSupplier); + + public static void assertEquals(Long expected, long actual, Supplier messageSupplier); + + public static void assertEquals(Long expected, Long actual, Supplier messageSupplier); + + public static void assertEquals(float expected, float actual); + + public static void assertEquals(float expected, Float actual); + + public static void assertEquals(Float expected, float actual); + + public static void assertEquals(Float expected, Float actual); + + public static void assertEquals(float expected, float actual, String message); + + public static void assertEquals(float expected, Float actual, String message); + + public static void assertEquals(Float expected, float actual, String message); + + public static void assertEquals(Float expected, Float actual, String message); + + public static void assertEquals(float expected, float actual, Supplier messageSupplier); + + public static void assertEquals(float expected, Float actual, Supplier messageSupplier); + + public static void assertEquals(Float expected, float actual, Supplier messageSupplier); + + public static void assertEquals(Float expected, Float actual, Supplier messageSupplier); + + public static void assertEquals(float expected, float actual, float delta); + + public static void assertEquals(float expected, float actual, float delta, String message); + + public static void assertEquals(float expected, float actual, float delta, Supplier messageSupplier); + + public static void assertEquals(double expected, double actual); + + public static void assertEquals(double expected, Double actual); + + public static void assertEquals(Double expected, double actual); + + public static void assertEquals(Double expected, Double actual); + + public static void assertEquals(double expected, double actual, String message); + + public static void assertEquals(double expected, Double actual, String message); + + public static void assertEquals(Double expected, double actual, String message); + + public static void assertEquals(Double expected, Double actual, String message); + + public static void assertEquals(double expected, double actual, Supplier messageSupplier); + + public static void assertEquals(double expected, Double actual, Supplier messageSupplier); + + public static void assertEquals(Double expected, double actual, Supplier messageSupplier); + + public static void assertEquals(Double expected, Double actual, Supplier messageSupplier); + + public static void assertEquals(double expected, double actual, double delta); + + public static void assertEquals(double expected, double actual, double delta, String message); + + public static void assertEquals(double expected, double actual, double delta, Supplier messageSupplier); + + public static void assertEquals(char expected, char actual); + + public static void assertEquals(char expected, Character actual); + + public static void assertEquals(Character expected, char actual); + + public static void assertEquals(Character expected, Character actual); + + public static void assertEquals(char expected, char actual, String message); + + public static void assertEquals(char expected, Character actual, String message); + + public static void assertEquals(Character expected, char actual, String message); + + public static void assertEquals(Character expected, Character actual, String message); + + public static void assertEquals(char expected, char actual, Supplier messageSupplier); + + public static void assertEquals(char expected, Character actual, Supplier messageSupplier); + + public static void assertEquals(Character expected, char actual, Supplier messageSupplier); + + public static void assertEquals(Character expected, Character actual, Supplier messageSupplier); + + public static void assertEquals(Object expected, Object actual); + + public static void assertEquals(Object expected, Object actual, String message); + + public static void assertEquals(Object expected, Object actual, Supplier messageSupplier); + + public static void assertArrayEquals(boolean [] expected, boolean [] actual); + + public static void assertArrayEquals(boolean [] expected, boolean [] actual, String message); + + public static void assertArrayEquals(boolean [] expected, boolean [] actual, Supplier messageSupplier); + + public static void assertArrayEquals(char [] expected, char [] actual); + + public static void assertArrayEquals(char [] expected, char [] actual, String message); + + public static void assertArrayEquals(char [] expected, char [] actual, Supplier messageSupplier); + + public static void assertArrayEquals(byte [] expected, byte [] actual); + + public static void assertArrayEquals(byte [] expected, byte [] actual, String message); + + public static void assertArrayEquals(byte [] expected, byte [] actual, Supplier messageSupplier); + + public static void assertArrayEquals(short [] expected, short [] actual); + + public static void assertArrayEquals(short [] expected, short [] actual, String message); + + public static void assertArrayEquals(short [] expected, short [] actual, Supplier messageSupplier); + + public static void assertArrayEquals(int [] expected, int [] actual); + + public static void assertArrayEquals(int [] expected, int [] actual, String message); + + public static void assertArrayEquals(int [] expected, int [] actual, Supplier messageSupplier); + + public static void assertArrayEquals(long [] expected, long [] actual); + + public static void assertArrayEquals(long [] expected, long [] actual, String message); + + public static void assertArrayEquals(long [] expected, long [] actual, Supplier messageSupplier); + + public static void assertArrayEquals(float [] expected, float [] actual); + + public static void assertArrayEquals(float [] expected, float [] actual, String message); + + public static void assertArrayEquals(float [] expected, float [] actual, Supplier messageSupplier); + + public static void assertArrayEquals(float[] expected, float[] actual, float delta); + + public static void assertArrayEquals(float[] expected, float[] actual, float delta, String message); + + public static void assertArrayEquals(float[] expected, float[] actual, float delta, + Supplier messageSupplier); + + public static void assertArrayEquals(double [] expected, double [] actual); + + public static void assertArrayEquals(double [] expected, double [] actual, String message); + + public static void assertArrayEquals(double [] expected, double [] actual, Supplier messageSupplier); + + public static void assertArrayEquals(double[] expected, double[] actual, double delta); + + public static void assertArrayEquals(double[] expected, double[] actual, double delta, String message); + + public static void assertArrayEquals(double[] expected, double[] actual, double delta, + Supplier messageSupplier); + + public static void assertArrayEquals(Object [] expected, Object [] actual); + + public static void assertArrayEquals(Object [] expected, Object [] actual, String message); + + public static void assertArrayEquals(Object [] expected, Object [] actual, Supplier messageSupplier); + + public static void assertIterableEquals(Iterable expected, Iterable actual); + + public static void assertIterableEquals(Iterable expected, Iterable actual, String message); + + public static void assertIterableEquals(Iterable expected, Iterable actual, + Supplier messageSupplier); + + public static void assertLinesMatch(List expectedLines, List actualLines); + + public static void assertLinesMatch(List expectedLines, List actualLines, String message); + + public static void assertLinesMatch(List expectedLines, List actualLines, + Supplier messageSupplier); + + public static void assertLinesMatch(Stream expectedLines, Stream actualLines); + + public static void assertLinesMatch(Stream expectedLines, Stream actualLines, String message); + + public static void assertLinesMatch(Stream expectedLines, Stream actualLines, + Supplier messageSupplier); + + public static void assertNotEquals(byte unexpected, byte actual); + + public static void assertNotEquals(byte unexpected, Byte actual); + + public static void assertNotEquals(Byte unexpected, byte actual); + + public static void assertNotEquals(Byte unexpected, Byte actual); + + public static void assertNotEquals(byte unexpected, byte actual, String message); + + public static void assertNotEquals(byte unexpected, Byte actual, String message); + + public static void assertNotEquals(Byte unexpected, byte actual, String message); + + public static void assertNotEquals(Byte unexpected, Byte actual, String message); + + public static void assertNotEquals(byte unexpected, byte actual, Supplier messageSupplier); + + public static void assertNotEquals(byte unexpected, Byte actual, Supplier messageSupplier); + + public static void assertNotEquals(Byte unexpected, byte actual, Supplier messageSupplier); + + public static void assertNotEquals(Byte unexpected, Byte actual, Supplier messageSupplier); + + public static void assertNotEquals(short unexpected, short actual); + + public static void assertNotEquals(short unexpected, Short actual); + + public static void assertNotEquals(Short unexpected, short actual); + + public static void assertNotEquals(Short unexpected, Short actual); + + public static void assertNotEquals(short unexpected, short actual, String message); + + public static void assertNotEquals(short unexpected, Short actual, String message); + + public static void assertNotEquals(Short unexpected, short actual, String message); + + public static void assertNotEquals(Short unexpected, Short actual, String message); + + public static void assertNotEquals(short unexpected, short actual, Supplier messageSupplier); + + public static void assertNotEquals(short unexpected, Short actual, Supplier messageSupplier); + + public static void assertNotEquals(Short unexpected, short actual, Supplier messageSupplier); + + public static void assertNotEquals(Short unexpected, Short actual, Supplier messageSupplier); + + public static void assertNotEquals(int unexpected, int actual); + + public static void assertNotEquals(int unexpected, Integer actual); + + public static void assertNotEquals(Integer unexpected, int actual); + + public static void assertNotEquals(Integer unexpected, Integer actual); + + public static void assertNotEquals(int unexpected, int actual, String message); + + public static void assertNotEquals(int unexpected, Integer actual, String message); + + public static void assertNotEquals(Integer unexpected, int actual, String message); + + public static void assertNotEquals(Integer unexpected, Integer actual, String message); + + public static void assertNotEquals(int unexpected, int actual, Supplier messageSupplier); + + public static void assertNotEquals(int unexpected, Integer actual, Supplier messageSupplier); + + public static void assertNotEquals(Integer unexpected, int actual, Supplier messageSupplier); + + public static void assertNotEquals(Integer unexpected, Integer actual, Supplier messageSupplier); + + public static void assertNotEquals(long unexpected, long actual); + + public static void assertNotEquals(long unexpected, Long actual); + + public static void assertNotEquals(Long unexpected, long actual); + + public static void assertNotEquals(Long unexpected, Long actual); + + public static void assertNotEquals(long unexpected, long actual, String message); + + public static void assertNotEquals(long unexpected, Long actual, String message); + + public static void assertNotEquals(Long unexpected, long actual, String message); + + public static void assertNotEquals(Long unexpected, Long actual, String message); + + public static void assertNotEquals(long unexpected, long actual, Supplier messageSupplier); + + public static void assertNotEquals(long unexpected, Long actual, Supplier messageSupplier); + + public static void assertNotEquals(Long unexpected, long actual, Supplier messageSupplier); + + public static void assertNotEquals(Long unexpected, Long actual, Supplier messageSupplier); + + public static void assertNotEquals(float unexpected, float actual); + + public static void assertNotEquals(float unexpected, Float actual); + + public static void assertNotEquals(Float unexpected, float actual); + + public static void assertNotEquals(Float unexpected, Float actual); + + public static void assertNotEquals(float unexpected, float actual, String message); + + public static void assertNotEquals(float unexpected, Float actual, String message); + + public static void assertNotEquals(Float unexpected, float actual, String message); + + public static void assertNotEquals(Float unexpected, Float actual, String message); + + public static void assertNotEquals(float unexpected, float actual, Supplier messageSupplier); + + public static void assertNotEquals(float unexpected, Float actual, Supplier messageSupplier); + + public static void assertNotEquals(Float unexpected, float actual, Supplier messageSupplier); + + public static void assertNotEquals(Float unexpected, Float actual, Supplier messageSupplier); + + public static void assertNotEquals(float unexpected, float actual, float delta); + + public static void assertNotEquals(float unexpected, float actual, float delta, String message); + + public static void assertNotEquals(float unexpected, float actual, float delta, Supplier messageSupplier); + + public static void assertNotEquals(double unexpected, double actual); + + public static void assertNotEquals(double unexpected, Double actual); + + public static void assertNotEquals(Double unexpected, double actual); + + public static void assertNotEquals(Double unexpected, Double actual); + + public static void assertNotEquals(double unexpected, double actual, String message); + + public static void assertNotEquals(double unexpected, Double actual, String message); + + public static void assertNotEquals(Double unexpected, double actual, String message); + + public static void assertNotEquals(Double unexpected, Double actual, String message); + + public static void assertNotEquals(double unexpected, double actual, Supplier messageSupplier); + + public static void assertNotEquals(double unexpected, Double actual, Supplier messageSupplier); + + public static void assertNotEquals(Double unexpected, double actual, Supplier messageSupplier); + + public static void assertNotEquals(Double unexpected, Double actual, Supplier messageSupplier); + + public static void assertNotEquals(double unexpected, double actual, double delta); + + public static void assertNotEquals(double unexpected, double actual, double delta, String message); + + public static void assertNotEquals(double unexpected, double actual, double delta, + Supplier messageSupplier); + + public static void assertNotEquals(char unexpected, char actual); + + public static void assertNotEquals(char unexpected, Character actual); + + public static void assertNotEquals(Character unexpected, char actual); + + public static void assertNotEquals(Character unexpected, Character actual); + + public static void assertNotEquals(char unexpected, char actual, String message); + + public static void assertNotEquals(char unexpected, Character actual, String message); + + public static void assertNotEquals(Character unexpected, char actual, String message); + + public static void assertNotEquals(Character unexpected, Character actual, String message); + + public static void assertNotEquals(char unexpected, char actual, Supplier messageSupplier); + + public static void assertNotEquals(char unexpected, Character actual, Supplier messageSupplier); + + public static void assertNotEquals(Character unexpected, char actual, Supplier messageSupplier); + + public static void assertNotEquals(Character unexpected, Character actual, Supplier messageSupplier); + + public static void assertNotEquals(Object unexpected, Object actual); + + public static void assertNotEquals(Object unexpected, Object actual, String message); + + public static void assertNotEquals(Object unexpected, Object actual, Supplier messageSupplier); + + public static void assertSame(Object expected, Object actual); + + public static void assertSame(Object expected, Object actual, String message); + + public static void assertSame(Object expected, Object actual, Supplier messageSupplier); + + public static void assertNotSame(Object unexpected, Object actual); + + public static void assertNotSame(Object unexpected, Object actual, String message); + + public static void assertNotSame(Object unexpected, Object actual, Supplier messageSupplier); + + public static void assertAll(Executable... executables) throws MultipleFailuresError; + + public static void assertAll(String heading, Executable... executables) throws MultipleFailuresError; + + public static void assertAll(Collection executables) throws MultipleFailuresError; + + public static void assertAll(String heading, Collection executables) throws MultipleFailuresError; + + public static void assertAll(Stream executables) throws MultipleFailuresError; + + public static void assertAll(String heading, Stream executables) throws MultipleFailuresError; + + public static T assertThrows(Class expectedType, Executable executable); + + public static T assertThrows(Class expectedType, Executable executable, String message); + + public static T assertThrows(Class expectedType, Executable executable, + Supplier messageSupplier); + + public static void assertDoesNotThrow(Executable executable); + + public static void assertDoesNotThrow(Executable executable, String message); + + public static void assertDoesNotThrow(Executable executable, Supplier messageSupplier); + + public static T assertDoesNotThrow(ThrowingSupplier supplier); + + public static T assertDoesNotThrow(ThrowingSupplier supplier, String message); + + public static T assertDoesNotThrow(ThrowingSupplier supplier, Supplier messageSupplier); + + public static void assertTimeout(Duration timeout, Executable executable); + + public static void assertTimeout(Duration timeout, Executable executable, String message); + + public static void assertTimeout(Duration timeout, Executable executable, Supplier messageSupplier); + + public static T assertTimeout(Duration timeout, ThrowingSupplier supplier); + + public static T assertTimeout(Duration timeout, ThrowingSupplier supplier, String message); + + public static T assertTimeout(Duration timeout, ThrowingSupplier supplier, + Supplier messageSupplier); + + public static void assertTimeoutPreemptively(Duration timeout, Executable executable); + + public static void assertTimeoutPreemptively(Duration timeout, Executable executable, String message); + + public static void assertTimeoutPreemptively(Duration timeout, Executable executable, + Supplier messageSupplier); + + public static T assertTimeoutPreemptively(Duration timeout, ThrowingSupplier supplier); + + public static T assertTimeoutPreemptively(Duration timeout, ThrowingSupplier supplier, String message); + + public static T assertTimeoutPreemptively(Duration timeout, ThrowingSupplier supplier, + Supplier messageSupplier); +} diff --git a/checker/tests/nullness/AssertMethodTest.java b/checker/tests/nullness/AssertMethodTest.java new file mode 100644 index 00000000000..fc664332072 --- /dev/null +++ b/checker/tests/nullness/AssertMethodTest.java @@ -0,0 +1,87 @@ +import org.checkerframework.checker.nullness.qual.Nullable; +import org.checkerframework.dataflow.qual.AssertMethod; +import org.checkerframework.dataflow.qual.Pure; +import org.checkerframework.dataflow.qual.SideEffectFree; + +public class AssertMethodTest { + @interface Anno { + Class value(); + } + + @AssertMethod + @SideEffectFree + void assertMethod(boolean b) { + if (!b) { + throw new RuntimeException(); + } + } + + void test1(@Nullable Object o) { + assertMethod(o != null); + o.toString(); + } + + @Nullable Object getO() { + return null; + } + + void test2() { + assertMethod(getO() != null); + // :: error: dereference.of.nullable + getO().toString(); // error + } + + @Pure + @Nullable Object getPureO() { + return ""; + } + + void test3() { + assertMethod(getPureO() != null); + getPureO().toString(); + } + + @Nullable Object field = null; + + void test4() { + assertMethod(field != null); + field.toString(); + } + + String getError() { + field = null; + return "error"; + } + + @AssertMethod(value = RuntimeException.class, parameter = 2) + @SideEffectFree + void assertMethod(Object p, boolean b, Object error) { + if (!b) { + throw new RuntimeException(); + } + } + + void test5() { + assertMethod(getError(), field != null, getError()); + // :: error: dereference.of.nullable + field.toString(); // error + } + + void test5b() { + assertMethod(getError(), field != null, ""); + field.toString(); + } + + @AssertMethod(isAssertFalse = true) + @SideEffectFree + void assertFalse(boolean b) { + if (b) { + throw new RuntimeException(); + } + } + + void test6() { + assertFalse(field == null); + field.toString(); + } +} diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java index b2f13fe473f..8b8dd8b3dad 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java @@ -58,6 +58,7 @@ import com.sun.source.util.TreePath; import com.sun.source.util.TreeScanner; import com.sun.source.util.Trees; +import com.sun.tools.javac.code.Type; import java.util.ArrayList; import java.util.Collections; import java.util.HashMap; @@ -68,6 +69,7 @@ import java.util.Map; import java.util.Set; import javax.annotation.processing.ProcessingEnvironment; +import javax.lang.model.element.AnnotationMirror; import javax.lang.model.element.Element; import javax.lang.model.element.ElementKind; import javax.lang.model.element.ExecutableElement; @@ -161,8 +163,10 @@ import org.checkerframework.dataflow.cfg.node.ValueLiteralNode; import org.checkerframework.dataflow.cfg.node.VariableDeclarationNode; import org.checkerframework.dataflow.cfg.node.WideningConversionNode; +import org.checkerframework.dataflow.qual.AssertMethod; import org.checkerframework.dataflow.qual.TerminatesExecution; import org.checkerframework.javacutil.AnnotationProvider; +import org.checkerframework.javacutil.AnnotationUtils; import org.checkerframework.javacutil.BugInCF; import org.checkerframework.javacutil.ElementUtils; import org.checkerframework.javacutil.SystemUtil; @@ -379,7 +383,18 @@ public class CFGTranslationPhaseOne extends TreeScanner { */ protected final Set newArrayExceptionTypes; + /** The AssertMethod.value argument/element. */ + protected final ExecutableElement assertMethodValueElement; + + /** The AssertMethod.parameter argument/element. */ + protected final ExecutableElement assertMethodParameterElement; + + /** The {@link AssertMethod#isAssertFalse()} argument/element. */ + protected final ExecutableElement assertMethodIsAssertFalseElement; + /** + * Creates {@link CFGTranslationPhaseOne}. + * * @param treeBuilder builder for new AST nodes * @param annotationProvider extracts annotations from AST nodes * @param assumeAssertionsDisabled can assertions be assumed to be disabled? @@ -443,6 +458,11 @@ public CFGTranslationPhaseOne( if (outOfMemoryErrorType != null) { newArrayExceptionTypes.add(outOfMemoryErrorType); } + + assertMethodValueElement = TreeUtils.getMethod(AssertMethod.class, "value", 0, env); + assertMethodParameterElement = TreeUtils.getMethod(AssertMethod.class, "parameter", 0, env); + assertMethodIsAssertFalseElement = + TreeUtils.getMethod(AssertMethod.class, "isAssertFalse", 0, env); } /** @@ -1279,6 +1299,7 @@ protected Node methodInvocationConvert(Node node, TypeMirror formalType) { * list of {@link Node}s representing the arguments converted for a call of the method. This * method applies to both method invocations and constructor calls. * + * @param tree the invocation tree for the call * @param method an ExecutableElement representing a method to be called * @param methodType an ExecutableType representing the type of the method call; the type must be * viewpoint-adapted to the call @@ -1287,6 +1308,7 @@ protected Node methodInvocationConvert(Node node, TypeMirror formalType) { * this method */ protected List convertCallArguments( + ExpressionTree tree, ExecutableElement method, ExecutableType methodType, List actualExprs) { @@ -1298,6 +1320,7 @@ protected List convertCallArguments( int numFormals = formals.size(); ArrayList convertedNodes = new ArrayList<>(numFormals); + AssertMethodTuple assertMethodTuple = getAssertMethodTuple(method); int numActuals = actualExprs.size(); if (method.isVarArgs()) { @@ -1311,6 +1334,9 @@ protected List convertCallArguments( // invocation conversion to all arguments. for (int i = 0; i < numActuals; i++) { Node actualVal = scan(actualExprs.get(i), null); + if (i == assertMethodTuple.booleanParam) { + treatMethodAsAssert((MethodInvocationTree) tree, assertMethodTuple, actualVal); + } if (actualVal == null) { throw new BugInCF( "CFGBuilder: scan returned null for %s [%s]", @@ -1324,6 +1350,9 @@ protected List convertCallArguments( // remaining ones to initialize an array. for (int i = 0; i < lastArgIndex; i++) { Node actualVal = scan(actualExprs.get(i), null); + if (i == assertMethodTuple.booleanParam) { + treatMethodAsAssert((MethodInvocationTree) tree, assertMethodTuple, actualVal); + } convertedNodes.add(methodInvocationConvert(actualVal, formals.get(i))); } @@ -1353,6 +1382,9 @@ protected List convertCallArguments( } else { for (int i = 0; i < numActuals; i++) { Node actualVal = scan(actualExprs.get(i), null); + if (i == assertMethodTuple.booleanParam) { + treatMethodAsAssert((MethodInvocationTree) tree, assertMethodTuple, actualVal); + } convertedNodes.add(methodInvocationConvert(actualVal, formals.get(i))); } } @@ -1360,6 +1392,69 @@ protected List convertCallArguments( return convertedNodes; } + /** + * Returns the AssertMethodTuple for {@code method}. If {@code method} is not an assert method, + * then {@link AssertMethodTuple#NONE} is returned. + * + * @param method a method element that might be an assert method + * @return the AssertMethodTuple for {@code method} + */ + protected AssertMethodTuple getAssertMethodTuple(ExecutableElement method) { + AnnotationMirror assertMethodAnno = + annotationProvider.getDeclAnnotation(method, AssertMethod.class); + if (assertMethodAnno == null) { + return AssertMethodTuple.NONE; + } + + int booleanParam = + AnnotationUtils.getElementValue( + assertMethodAnno, assertMethodParameterElement, Integer.class, 1) + - 1; + TypeMirror exceptionType = + AnnotationUtils.getElementValue( + assertMethodAnno, + assertMethodValueElement, + Type.ClassType.class, + (Type.ClassType) assertionErrorType); + boolean isAssertFalse = + AnnotationUtils.getElementValue( + assertMethodAnno, assertMethodIsAssertFalseElement, Boolean.class, false); + return new AssertMethodTuple(booleanParam, exceptionType, isAssertFalse); + } + + /** Holds the elements of an {@link AssertMethod} annotation. */ + protected static class AssertMethodTuple { + + /** A tuple representing the lack of an {@link AssertMethodTuple}. */ + protected static final AssertMethodTuple NONE = new AssertMethodTuple(-1, null, false); + + /** + * 0-based index of the parameter of the expression that is tested by the assert method. (Or -1 + * if this isn't an assert method.) + */ + public final int booleanParam; + + /** The type of the exception thrown by the assert method. */ + public final TypeMirror exceptionType; + + /** Is this an assert false method? */ + public final boolean isAssertFalse; + + /** + * Creates an AssertMethodTuple. + * + * @param booleanParam 0-based index of the parameter of the expression that is tested by the + * assert method + * @param exceptionType the type of the exception thrown by the assert method + * @param isAssertFalse is this an assert false method + */ + public AssertMethodTuple(int booleanParam, TypeMirror exceptionType, boolean isAssertFalse) { + this.booleanParam = booleanParam; + this.exceptionType = exceptionType; + this.isAssertFalse = isAssertFalse; + } + } + /** * Convert an operand of a conditional expression to the type of the whole expression. * @@ -1496,7 +1591,7 @@ public MethodInvocationNode visitMethodInvocation(MethodInvocationTree tree, Voi // See also BaseTypeVisitor.visitMethodInvocation and QualifierPolymorphism.annotate. arguments = Collections.emptyList(); } else { - arguments = convertCallArguments(method, TreeUtils.typeFromUse(tree), actualExprs); + arguments = convertCallArguments(tree, method, TreeUtils.typeFromUse(tree), actualExprs); } // TODO: lock the receiver for synchronized methods @@ -1511,7 +1606,6 @@ public MethodInvocationNode visitMethodInvocation(MethodInvocationTree tree, Voi if (terminatesExecution) { extendedNode.setTerminatesExecution(true); } - return node; } @@ -1647,6 +1741,35 @@ protected void translateAssertWithAssertionsEnabled(AssertTree tree) { addLabelForNextNode(assertEnd); } + /** + * Translates a method marked as {@link AssertMethod} into CFG nodes corresponding to an {@code + * assert} statement. + * + * @param tree the method invocation tree for a method marked as {@link AssertMethod} + * @param assertMethodTuple the assert method tuple for the method + * @param condition the boolean expression node for the argument that the method tests + */ + protected void treatMethodAsAssert( + MethodInvocationTree tree, AssertMethodTuple assertMethodTuple, Node condition) { + + // all necessary labels + Label thenLabel = new Label(); + Label elseLabel = new Label(); + ConditionalJump cjump = new ConditionalJump(thenLabel, elseLabel); + extendWithExtendedNode(cjump); + + addLabelForNextNode(assertMethodTuple.isAssertFalse ? thenLabel : elseLabel); + AssertionErrorNode assertNode = + new AssertionErrorNode(tree, condition, null, assertMethodTuple.exceptionType); + extendWithNode(assertNode); + NodeWithExceptionsHolder exNode = + extendWithNodeWithException( + new ThrowNode(null, assertNode, env.getTypeUtils()), assertMethodTuple.exceptionType); + exNode.setTerminatesExecution(true); + + addLabelForNextNode(assertMethodTuple.isAssertFalse ? elseLabel : thenLabel); + } + @Override public Node visitAssignment(AssignmentTree tree, Void p) { @@ -3389,7 +3512,7 @@ public Node visitNewClass(NewClassTree tree, Void p) { List actualExprs = tree.getArguments(); List arguments = - convertCallArguments(constructor, TreeUtils.typeFromUse(tree), actualExprs); + convertCallArguments(tree, constructor, TreeUtils.typeFromUse(tree), actualExprs); // TODO: for anonymous classes, don't use the identifier alone. // See https://github.com/typetools/checker-framework/issues/890 . diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/AssertionErrorNode.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/AssertionErrorNode.java index a39079dbb8c..27431a9bad0 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/AssertionErrorNode.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/AssertionErrorNode.java @@ -1,15 +1,18 @@ package org.checkerframework.dataflow.cfg.node; -import com.sun.source.tree.AssertTree; +import com.sun.source.tree.Tree; import java.util.Arrays; import java.util.Collection; +import java.util.Collections; import java.util.Objects; import javax.lang.model.type.TypeMirror; import org.checkerframework.checker.nullness.qual.Nullable; +import org.checkerframework.dataflow.qual.Pure; import org.checkerframework.dataflow.qual.SideEffectFree; /** - * A node for the {@link AssertionError} when an assertion fails. + * A node for the {@link AssertionError} when an assertion fails or when a method call marked {@link + * org.checkerframework.dataflow.qual.AssertMethod} fails. * * 
      *   assert condition : detail ;
@@ -17,11 +20,24 @@
  */
 public class AssertionErrorNode extends Node {
 
-  protected final AssertTree tree;
+  /** Tree for the assert statement or assert method. */
+  protected final Tree tree;
+
+  /** The condition that if it is false, the assertion exception is thrown. */
   protected final Node condition;
-  protected final Node detail;
 
-  public AssertionErrorNode(AssertTree tree, Node condition, Node detail, TypeMirror type) {
+  /** The node for the expression after {@code :} in the assert statement, or null. */
+  protected final @Nullable Node detail;
+
+  /**
+   * Creates an AssertionErrorNode.
+   *
+   * @param tree tree for the assert statement or assert method
+   * @param condition the node of the condition when if false the assertion exception is thrown
+   * @param detail node for the expression after {@code :} in the assert statement, or null
+   * @param type the type of the exception thrown
+   */
+  public AssertionErrorNode(Tree tree, Node condition, @Nullable Node detail, TypeMirror type) {
     // TODO: Find out the correct "type" for statements.
     // Is it TypeKind.NONE?
     super(type);
@@ -30,16 +46,28 @@ public AssertionErrorNode(AssertTree tree, Node condition, Node detail, TypeMirr
     this.detail = detail;
   }
 
+  /**
+   * The node of the condition that if it is false, the assertion exception is thrown.
+   *
+   * @return the node of the condition that if it is false, the assertion exception is thrown
+   */
+  @Pure
   public Node getCondition() {
     return condition;
   }
 
-  public Node getDetail() {
+  /**
+   * The node for the expression after {@code :} in the assert statement, or null.
+   *
+   * @return node for the expression after {@code :} in the assert statement, or null
+   */
+  @Pure
+  public @Nullable Node getDetail() {
     return detail;
   }
 
   @Override
-  public AssertTree getTree() {
+  public Tree getTree() {
     return tree;
   }
 
@@ -71,6 +99,9 @@ public int hashCode() {
   @Override
   @SideEffectFree
   public Collection getOperands() {
+    if (getDetail() == null) {
+      return Collections.singleton(getCondition());
+    }
     return Arrays.asList(getCondition(), getDetail());
   }
 }

From 2545842150dd2d155adb24d83047027632ae5570 Mon Sep 17 00:00:00 2001
From: "renovate[bot]" <29139614+renovate[bot]@users.noreply.github.com>
Date: Thu, 30 Nov 2023 09:02:30 -0800
Subject: [PATCH 08/19] Update dependency gradle to v8.5 (#6325)

Co-authored-by: renovate[bot] <29139614+renovate[bot]@users.noreply.github.com>
---
 gradle/wrapper/gradle-wrapper.properties | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/gradle/wrapper/gradle-wrapper.properties b/gradle/wrapper/gradle-wrapper.properties
index 3fa8f862f75..1af9e0930b8 100644
--- a/gradle/wrapper/gradle-wrapper.properties
+++ b/gradle/wrapper/gradle-wrapper.properties
@@ -1,6 +1,6 @@
 distributionBase=GRADLE_USER_HOME
 distributionPath=wrapper/dists
-distributionUrl=https\://services.gradle.org/distributions/gradle-8.4-bin.zip
+distributionUrl=https\://services.gradle.org/distributions/gradle-8.5-bin.zip
 networkTimeout=10000
 validateDistributionUrl=true
 zipStoreBase=GRADLE_USER_HOME

From f9e275757e0bc46e80c1df172166d76469d9bada Mon Sep 17 00:00:00 2001
From: "renovate[bot]" <29139614+renovate[bot]@users.noreply.github.com>
Date: Thu, 30 Nov 2023 09:03:07 -0800
Subject: [PATCH 09/19] Update plugin com.diffplug.spotless to v6.23.2 (#6324)

Co-authored-by: renovate[bot] <29139614+renovate[bot]@users.noreply.github.com>
---
 build.gradle | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/build.gradle b/build.gradle
index 9a19f593f80..46ac7a51604 100644
--- a/build.gradle
+++ b/build.gradle
@@ -15,7 +15,7 @@ plugins {
   // Code formatting; defines targets "spotlessApply" and "spotlessCheck".
   // https://github.com/diffplug/spotless/tags ; see tags starting "gradle/"
   // Only works on JDK 11+ (even including the plugin crashes Gradle on JDK 8).
-  id 'com.diffplug.spotless' version '6.23.0'
+  id 'com.diffplug.spotless' version '6.23.2'
 }
 apply plugin: 'de.undercouch.download'
 

From 49d97d7ea18562d644a98699acd82825f0e97245 Mon Sep 17 00:00:00 2001
From: "renovate[bot]" <29139614+renovate[bot]@users.noreply.github.com>
Date: Thu, 30 Nov 2023 09:03:31 -0800
Subject: [PATCH 10/19] Update dependency commons-io:commons-io to v2.15.1
 (#6323)

Co-authored-by: renovate[bot] <29139614+renovate[bot]@users.noreply.github.com>
---
 checker/build.gradle | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/checker/build.gradle b/checker/build.gradle
index ac04120c604..cc7f66c7d82 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.15.0'
+  testImplementation 'commons-io:commons-io:2.15.1'
 
   testImplementation group: 'junit', name: 'junit', version: '4.13.2'
   testImplementation project(':framework-test')

From 3bca5e20db2c9cb480d977137403818a4d083d8d Mon Sep 17 00:00:00 2001
From: "renovate[bot]" <29139614+renovate[bot]@users.noreply.github.com>
Date: Fri, 1 Dec 2023 08:23:29 -0800
Subject: [PATCH 11/19] Update dependency com.amazonaws:aws-java-sdk-bom to
 v1.12.603 (#6328)

Co-authored-by: renovate[bot] <29139614+renovate[bot]@users.noreply.github.com>
---
 checker/build.gradle | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/checker/build.gradle b/checker/build.gradle
index cc7f66c7d82..fcda2b65e21 100644
--- a/checker/build.gradle
+++ b/checker/build.gradle
@@ -64,7 +64,7 @@ dependencies {
   testImplementation 'com.amazonaws:aws-java-sdk-ec2'
   testImplementation 'com.amazonaws:aws-java-sdk-kms'
   // The AWS SDK is used for testing the Called Methods Checker.
-  testImplementation platform('com.amazonaws:aws-java-sdk-bom:1.12.581')
+  testImplementation platform('com.amazonaws:aws-java-sdk-bom:1.12.603')
   // 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.

From 43db4471ceca09946aea0947701e7e23454f4b4e Mon Sep 17 00:00:00 2001
From: Suzanne Millstein 
Date: Fri, 1 Dec 2023 14:16:57 -0800
Subject: [PATCH 12/19] Add a new method to handle annotations not on the
 classpath

---
 .../cfg/builder/CFGTranslationPhaseOne.java   | 33 +++++----------
 .../javacutil/AnnotationUtils.java            | 41 ++++++++++++++++++-
 2 files changed, 50 insertions(+), 24 deletions(-)

diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java
index 8b8dd8b3dad..475fd310b10 100644
--- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java
+++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java
@@ -383,15 +383,6 @@ public class CFGTranslationPhaseOne extends TreeScanner {
    */
   protected final Set newArrayExceptionTypes;
 
-  /** The AssertMethod.value argument/element. */
-  protected final ExecutableElement assertMethodValueElement;
-
-  /** The AssertMethod.parameter argument/element. */
-  protected final ExecutableElement assertMethodParameterElement;
-
-  /** The {@link AssertMethod#isAssertFalse()} argument/element. */
-  protected final ExecutableElement assertMethodIsAssertFalseElement;
-
   /**
    * Creates {@link CFGTranslationPhaseOne}.
    *
@@ -458,11 +449,6 @@ public CFGTranslationPhaseOne(
     if (outOfMemoryErrorType != null) {
       newArrayExceptionTypes.add(outOfMemoryErrorType);
     }
-
-    assertMethodValueElement = TreeUtils.getMethod(AssertMethod.class, "value", 0, env);
-    assertMethodParameterElement = TreeUtils.getMethod(AssertMethod.class, "parameter", 0, env);
-    assertMethodIsAssertFalseElement =
-        TreeUtils.getMethod(AssertMethod.class, "isAssertFalse", 0, env);
   }
 
   /**
@@ -1406,19 +1392,20 @@ protected AssertMethodTuple getAssertMethodTuple(ExecutableElement method) {
       return AssertMethodTuple.NONE;
     }
 
+    // Dataflow does not require checker-qual.jar to be on the users classpath, so
+    // AnnotationUtils.getElementValue(...) cannot be used.
+
     int booleanParam =
-        AnnotationUtils.getElementValue(
-                assertMethodAnno, assertMethodParameterElement, Integer.class, 1)
+        AnnotationUtils.getElementValueNotOnClasspath(
+                assertMethodAnno, "parameter", Integer.class, 1)
             - 1;
+
     TypeMirror exceptionType =
-        AnnotationUtils.getElementValue(
-            assertMethodAnno,
-            assertMethodValueElement,
-            Type.ClassType.class,
-            (Type.ClassType) assertionErrorType);
+        AnnotationUtils.getElementValueNotOnClasspath(
+            assertMethodAnno, "value", Type.ClassType.class, (Type.ClassType) assertionErrorType);
     boolean isAssertFalse =
-        AnnotationUtils.getElementValue(
-            assertMethodAnno, assertMethodIsAssertFalseElement, Boolean.class, false);
+        AnnotationUtils.getElementValueNotOnClasspath(
+            assertMethodAnno, "isAssertFalse", Boolean.class, false);
     return new AssertMethodTuple(booleanParam, exceptionType, isAssertFalse);
   }
 
diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationUtils.java b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationUtils.java
index 9046a3f37e5..48525ae3257 100644
--- a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationUtils.java
+++ b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationUtils.java
@@ -553,6 +553,45 @@ public static EnumSet getElementKindsForElementType(ElementType ele
   // Annotation values: inefficient extractors that take an element name
   // **********************************************************************
 
+  /**
+   * Get the element with the name {@code elementName} of the annotation {@code anno}. The result
+   * has type {@code expectedType}. If there is no value for {@code elementName}, {@code
+   * defaultValue} is returned
+   *
+   * 
    This method is intended only for use when the class of the annotation is not on the user's
+   * classpath. This is for users of the Dataflow Framework that do not use the rest of the Checker
+   * Framework. Type-checkers can assume that checker-qual.jar is on the classpath and should use
+   * {@link #getElementValue(AnnotationMirror, ExecutableElement, Class)} or {@link
+   * #getElementValue(AnnotationMirror, ExecutableElement, Class, Object)}.
+   *
+   * @param anno the annotation whose element to access
+   * @param elementName the name of the element to access
+   * @param expectedType the type of the element and the return value
+   * @param defaultValue the value to return if the element is not present
+   * @param  the class of the type
+   * @return the value of the element with the given name
+   */
+  public static  T getElementValueNotOnClasspath(
+      AnnotationMirror anno, CharSequence elementName, Class expectedType, T defaultValue) {
+    Map valmap = anno.getElementValues();
+
+    for (Map.Entry entry :
+        valmap.entrySet()) {
+      ExecutableElement elem = entry.getKey();
+      if (elem.getSimpleName().contentEquals(elementName)) {
+        AnnotationValue val = entry.getValue();
+        try {
+          return expectedType.cast(val.getValue());
+        } catch (ClassCastException e) {
+          throw new BugInCF(
+              "getElementValueNotOnClasspath(%s, %s, %s): val=%s, val.getValue()=%s [%s]",
+              anno, elementName, expectedType, val, val.getValue(), val.getValue().getClass());
+        }
+      }
+    }
+    return defaultValue;
+  }
+
   /**
    * Returns the values of an annotation's elements, including defaults. The method with the same
    * name in JavacElements cannot be used directly, because it includes a cast to
@@ -604,7 +643,7 @@ public static EnumSet getElementKindsForElementType(ElementType ele
    * @deprecated use {@link #getElementValue(AnnotationMirror, ExecutableElement, Class)} or {@link
    *     #getElementValue(AnnotationMirror, ExecutableElement, Class, Object)}
    */
-  @Deprecated // for use only by the framework
+  @Deprecated // for use only by the framework, not by clients
   public static  T getElementValue(
       AnnotationMirror anno, CharSequence elementName, Class expectedType, boolean useDefaults) {
     Map valmap;

From 98da4e5389799b56c3ff910e580ca3cb3ef1a228 Mon Sep 17 00:00:00 2001
From: Michael Ernst 
Date: Sun, 3 Dec 2023 10:00:57 -0800
Subject: [PATCH 13/19] Remove a project

---
 docs/developer/new-contributor-projects.html  | 63 -------------------
 .../new-contributor-projects.html-old         | 63 +++++++++++++++++++
 2 files changed, 63 insertions(+), 63 deletions(-)

diff --git a/docs/developer/new-contributor-projects.html b/docs/developer/new-contributor-projects.html
index 2aad16bbcd1..a2e41147660 100644
--- a/docs/developer/new-contributor-projects.html
+++ b/docs/developer/new-contributor-projects.html
@@ -25,7 +25,6 @@ 
    Projects for new contributors
     
   
  • Evaluate a type system or a Checker Framework feature
     
 
 
-
    Detecting errors in use of the Optional class
    
-
-
-
-
    
-Java 8 introduced the
-Optional
-class, a container that is either empty or contains a non-null value.
-It is intended to solve the problem of null
-pointer exceptions.  However, Optional
-has its
-  own problems, leading
-to extensive
-  advice on when and how to use Optional.  It is difficult for
-programmers to remember all these rules.
-
    
-
-
    
-The goal of this project is to build a tool to check uses of Optional and run it on open-source projects.  The research questions are:
-
    
-
      
-  
    • Is it possible to build a tool that enforces good style in using Optional?
-  
      • 
-  
    • How much effort is is for programmers to use such a tool?
-  
      • 
-  
    • Does real-world code obey the rules about use of Optional, or not?
-  
      • 
-
    
-
-
    
-We have
-a prototype
-    verification tool that checks some but not all rules about use of
-Optional (https://checkerframework.org/manual/#optional-checker).  This
-project will do case studies of it and extend it.
-
    
-
-
    
-The methodology is to find open-source projects that use Optional(you can
-do this by searching GitHub, for example), run the tool on them, and read
-the tool's warnings.  Each warning will lead to either a bug report against
-an open-source project or an improvement to the verification tool.
-
    
-
-
-
-
 
    Preventing mixed signed/unsigned computations
    
 
 
+
+
    
+Java 8 introduced the
+Optional
+class, a container that is either empty or contains a non-null value.
+It is intended to solve the problem of null
+pointer exceptions.  However, Optional
+has its
+  own problems, leading
+to extensive
+  advice on when and how to use Optional.  It is difficult for
+programmers to remember all these rules.
+
    
+
+
    
+The goal of this project is to build a tool to check uses of Optional and run it on open-source projects.  The research questions are:
+
    
+
      
+  
    • Is it possible to build a tool that enforces good style in using Optional?
+  
      • 
+  
    • How much effort is is for programmers to use such a tool?
+  
      • 
+  
    • Does real-world code obey the rules about use of Optional, or not?
+  
      • 
+
    
+
+
    
+We have
+a prototype
+    verification tool that checks some but not all rules about use of
+Optional (https://checkerframework.org/manual/#optional-checker).  This
+project will do case studies of it and extend it.
+
    
+
+
    
+The methodology is to find open-source projects that use Optional(you can
+do this by searching GitHub, for example), run the tool on them, and read
+the tool's warnings.  Each warning will lead to either a bug report against
+an open-source project or an improvement to the verification tool.
+
    
+
+
+
+

From d146eea4a5c2b3fe4842970decb1f26eadced5e6 Mon Sep 17 00:00:00 2001
From: "renovate[bot]" <29139614+renovate[bot]@users.noreply.github.com>
Date: Mon, 4 Dec 2023 00:13:50 +0000
Subject: [PATCH 14/19] Update dependency io.github.classgraph:classgraph to
 v4.8.165 (#6331)

Co-authored-by: renovate[bot] <29139614+renovate[bot]@users.noreply.github.com>
---
 framework/build.gradle | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/framework/build.gradle b/framework/build.gradle
index 4891e1a93e7..b852b1ac7d5 100644
--- a/framework/build.gradle
+++ b/framework/build.gradle
@@ -45,7 +45,7 @@ dependencies {
   implementation "org.plumelib:hashmap-util:${versions.hashmapUtil}"
   implementation "org.plumelib:plume-util:${versions.plumeUtil}"
   implementation "org.plumelib:reflection-util:${versions.reflectionUtil}"
-  implementation 'io.github.classgraph:classgraph:4.8.162'
+  implementation 'io.github.classgraph:classgraph:4.8.165'
 
   testImplementation group: 'junit', name: 'junit', version: '4.13.2'
   testImplementation project(':framework-test')

From 918fa9e0b80487a9081d7a5206f064a104564283 Mon Sep 17 00:00:00 2001
From: Michael Ernst 
Date: Sun, 3 Dec 2023 19:42:44 -0800
Subject: [PATCH 15/19] Don't compute element unless necessary

---
 .../checkerframework/javacutil/ElementUtils.java    | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/ElementUtils.java b/javacutil/src/main/java/org/checkerframework/javacutil/ElementUtils.java
index 099464a546c..bfaaacd68cb 100644
--- a/javacutil/src/main/java/org/checkerframework/javacutil/ElementUtils.java
+++ b/javacutil/src/main/java/org/checkerframework/javacutil/ElementUtils.java
@@ -939,12 +939,19 @@ public static boolean matchesElement(
     return true;
   }
 
-  /** Returns true if the given element is, or overrides, method. */
+  /**
+   * Returns true if the given element is, or overrides, {@code method}.
+   *
+   * @param questioned an element that might override {@code method}
+   * @param method a method that might be overridden
+   * @param env the processing environment
+   * @return true if {@code questioned} is, or overrides, {@code method}
+   */
   public static boolean isMethod(
       ExecutableElement questioned, ExecutableElement method, ProcessingEnvironment env) {
-    TypeElement enclosing = (TypeElement) questioned.getEnclosingElement();
     return questioned.equals(method)
-        || env.getElementUtils().overrides(questioned, method, enclosing);
+        || env.getElementUtils()
+            .overrides(questioned, method, (TypeElement) questioned.getEnclosingElement());
   }
 
   /**

From f80af834cf105b03191c3d9d48cbf441d8aaf8d5 Mon Sep 17 00:00:00 2001
From: Michael Ernst 
Date: Mon, 4 Dec 2023 06:58:08 -0800
Subject: [PATCH 16/19] Use Error Prone 2.23.0 (suppress warning)

---
 build.gradle                                                    | 2 +-
 .../java/org/checkerframework/checker/guieffect/Effect.java     | 1 +
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/build.gradle b/build.gradle
index 46ac7a51604..4dd4be34514 100644
--- a/build.gradle
+++ b/build.gradle
@@ -59,7 +59,7 @@ ext {
     hashmapUtil : '0.0.1',
     reflectionUtil : '1.1.0',
     plumeUtil : '1.8.1',
-    errorprone : '2.22.0',
+    errorprone : '2.23.0',
   ]
 }
 
diff --git a/checker/src/main/java/org/checkerframework/checker/guieffect/Effect.java b/checker/src/main/java/org/checkerframework/checker/guieffect/Effect.java
index c9f9c2e75bd..5a13a9c91c0 100644
--- a/checker/src/main/java/org/checkerframework/checker/guieffect/Effect.java
+++ b/checker/src/main/java/org/checkerframework/checker/guieffect/Effect.java
@@ -108,6 +108,7 @@ public boolean equals(Effect e) {
   }
 
   @Override
+  @SuppressWarnings("SuperEqualsIsObjectEquals") // better style to use the equals() abstraction
   public boolean equals(@Nullable Object o) {
     if (o instanceof Effect) {
       return this.equals((Effect) o);

From 116b2657e3f203bdb8cc9efd9703400f6c392d76 Mon Sep 17 00:00:00 2001
From: "renovate[bot]" <29139614+renovate[bot]@users.noreply.github.com>
Date: Mon, 4 Dec 2023 07:22:00 -0800
Subject: [PATCH 17/19] Update plugin com.diffplug.spotless to v6.23.3

---
 build.gradle | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/build.gradle b/build.gradle
index 4dd4be34514..670dc66feab 100644
--- a/build.gradle
+++ b/build.gradle
@@ -15,7 +15,7 @@ plugins {
   // Code formatting; defines targets "spotlessApply" and "spotlessCheck".
   // https://github.com/diffplug/spotless/tags ; see tags starting "gradle/"
   // Only works on JDK 11+ (even including the plugin crashes Gradle on JDK 8).
-  id 'com.diffplug.spotless' version '6.23.2'
+  id 'com.diffplug.spotless' version '6.23.3'
 }
 apply plugin: 'de.undercouch.download'
 

From 19ae530ffaa29832605e8f9f8f4773d66f16bb5a Mon Sep 17 00:00:00 2001
From: Michael Ernst 
Date: Mon, 4 Dec 2023 07:58:43 -0800
Subject: [PATCH 18/19] Transfer function documentation (#6333)

---
 .../dataflow/cfg/builder/CFGTranslationPhaseOne.java |  8 ++++----
 docs/manual/creating-a-checker.tex                   | 11 ++++++++++-
 .../framework/flow/CFAbstractTransfer.java           |  8 ++++----
 .../org/checkerframework/javacutil/TreePathUtil.java |  4 ++--
 .../org/checkerframework/javacutil/TreeUtils.java    | 12 +++++++++---
 5 files changed, 29 insertions(+), 14 deletions(-)

diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java
index 475fd310b10..ccaa52802dd 100644
--- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java
+++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java
@@ -201,14 +201,14 @@
  * 
    The return type of this scanner is {@link Node}. For expressions, the corresponding node is
  * returned to allow linking between different nodes.
  *
- * 
    However, for statements there is usually no single {@link Node} that is created, and thus no
- * node is returned (rather, null is returned).
+ * 
    However, for statements there is usually no single {@link Node} that is created, and thus null
+ * is returned.
  *
  * 
    Every {@code visit*} method is assumed to add at least one extended node to the list of nodes
  * (which might only be a jump).
  *
- * 
    The entry point to process a single body (e.g., method) is {@link #process(TreePath,
- * UnderlyingAST)}.
+ * 
    The entry point to process a single body (e.g., method, lambda, top-level block) is {@link
+ * #process(TreePath, UnderlyingAST)}.
  */
 @SuppressWarnings("nullness") // TODO
 public class CFGTranslationPhaseOne extends TreeScanner {
diff --git a/docs/manual/creating-a-checker.tex b/docs/manual/creating-a-checker.tex
index bbe48dbfef5..8382f933966 100644
--- a/docs/manual/creating-a-checker.tex
+++ b/docs/manual/creating-a-checker.tex
@@ -1488,7 +1488,16 @@
 named \<\emph{MyChecker}Transfer> that extends
 \refclass{framework/flow}{CFTransfer}.
 
-Leave the class body empty for now.  Your class will add functionality by
+Leave the class body empty for now, except for a constructor:
+
+\begin{Verbatim}
+  public MyCheckerTransfer(CFAnalysis analysis) {
+    super(analysis);
+  }
+\end{Verbatim}
+
+\noindent
+Your class will add functionality by
 overriding methods of \, which performs the default Checker
 Framework type refinement.
 
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 b081b50acd1..dac4e2e19db 100644
--- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java
+++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java
@@ -84,10 +84,10 @@
 import org.checkerframework.javacutil.TreeUtils;
 
 /**
- * The default analysis transfer function for the Checker Framework propagates information through
- * assignments and uses the {@link AnnotatedTypeFactory} to provide checker-specific logic how to
- * combine types (e.g., what is the type of a string concatenation, given the types of the two
- * operands) and as an abstraction function (e.g., determine the annotations on literals).
+ * The default analysis transfer function for the Checker Framework. It propagates information
+ * through assignments. It uses the {@link AnnotatedTypeFactory} to provide checker-specific logic
+ * to combine types (e.g., what is the type of a string concatenation, given the types of the two
+ * operands) and acts as an abstraction function (e.g., determine the annotations on literals).
  *
  * 
    Design note: CFAbstractTransfer and its subclasses are supposed to act as transfer functions.
  * But, since the AnnotatedTypeFactory already existed and performed checker-independent type
diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/TreePathUtil.java b/javacutil/src/main/java/org/checkerframework/javacutil/TreePathUtil.java
index cf54e6a853d..d692fb3d342 100644
--- a/javacutil/src/main/java/org/checkerframework/javacutil/TreePathUtil.java
+++ b/javacutil/src/main/java/org/checkerframework/javacutil/TreePathUtil.java
@@ -30,7 +30,7 @@ private TreePathUtil() {
   }
 
   ///
-  /// Retrieving a path
+  /// Retrieving a path (from another path)
   ///
 
   /**
@@ -84,7 +84,7 @@ private TreePathUtil() {
   }
 
   ///
-  /// Retrieving a tree
+  /// Retrieving a tree (from a path)
   ///
 
   /**
diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java b/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java
index 0cea4c4186c..5420f54ec74 100644
--- a/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java
+++ b/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java
@@ -1223,14 +1223,20 @@ public static boolean isMethodInvocation(
   /**
    * Returns true if the argument is an invocation of one of the given methods, or of any method
    * that overrides them.
+   *
+   * @param tree a tree that might be a method invocation
+   * @param methods the methods to check for
+   * @param processingEnv the processing environment
+   * @return true if the argument is an invocation of one of the given methods, or of any method
+   *     that overrides them
    */
   public static boolean isMethodInvocation(
-      Tree methodTree, List methods, ProcessingEnvironment processingEnv) {
-    if (!(methodTree instanceof MethodInvocationTree)) {
+      Tree tree, List methods, ProcessingEnvironment processingEnv) {
+    if (!(tree instanceof MethodInvocationTree)) {
       return false;
     }
     for (ExecutableElement Method : methods) {
-      if (isMethodInvocation(methodTree, Method, processingEnv)) {
+      if (isMethodInvocation(tree, Method, processingEnv)) {
         return true;
       }
     }

From 2f4073aa5142f7897b3c11b20b0a4b9e33b7f03e Mon Sep 17 00:00:00 2001
From: Suzanne Millstein 
Date: Mon, 4 Dec 2023 08:10:07 -0800
Subject: [PATCH 19/19] Prep for release.

---
 build.gradle      | 2 +-
 docs/CHANGELOG.md | 4 +++-
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/build.gradle b/build.gradle
index 670dc66feab..1f1c823066a 100644
--- a/build.gradle
+++ b/build.gradle
@@ -114,7 +114,7 @@ allprojects {
   //   * any new checkers have been added, or
   //   * backward-incompatible changes have been made to APIs or elsewhere.
   // To make a snapshot release: ./gradlew publish
-  version '3.40.1-SNAPSHOT'
+  version '3.41.0'
 
   tasks.withType(JavaCompile).configureEach {
     options.fork = true
diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md
index 3e3bed62158..eb71eacb68e 100644
--- a/docs/CHANGELOG.md
+++ b/docs/CHANGELOG.md
@@ -1,4 +1,4 @@
-Version 3.40.1 (December 1, 2023)
+Version 3.41.0 (December 4, 2023)
 ---------------------------------
 
 **User-visible changes:**
@@ -16,6 +16,8 @@ TypeMirror, boolean)` instead.
 
 **Closed issues:**
 
+#1497, #3345, #6037, #6204, #6276, #6282, #6290, #6296, #6319, #6327.
+
 
 Version 3.40.0 (November 1, 2023)
 ---------------------------------