diff --git a/checker/build.gradle b/checker/build.gradle index 6b3d702d734..72b7f560471 100644 --- a/checker/build.gradle +++ b/checker/build.gradle @@ -910,7 +910,8 @@ task wpiManyTest(group: 'Verification') { '-i', "${project.projectDir}/tests/wpi-many/testin.txt", '-o', "${project.projectDir}/build/wpi-many-tests", '-s', - '--', '--checker', 'nullness,interning,lock,regex,signature,calledmethods,resourceleak' + '--', '--checker', 'nullness,interning,lock,regex,signature,calledmethods,resourceleak', + '--extraJavacArgs=-AenableWpiForRlc' } } catch (Exception e) { println('Failure: Running wpi-many.sh failed with a non-zero exit code.') diff --git a/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsTransfer.java b/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsTransfer.java index bf05616fe8a..a7174871be0 100644 --- a/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsTransfer.java +++ b/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsTransfer.java @@ -1,5 +1,6 @@ package org.checkerframework.checker.calledmethods; +import com.sun.source.tree.Tree; import java.util.Arrays; import java.util.Collections; import java.util.LinkedHashMap; @@ -11,6 +12,7 @@ import javax.lang.model.type.TypeMirror; import org.checkerframework.checker.calledmethods.qual.EnsuresCalledMethodsVarArgs; import org.checkerframework.checker.nullness.qual.Nullable; +import org.checkerframework.checker.resourceleak.ResourceLeakChecker; import org.checkerframework.common.accumulation.AccumulationStore; import org.checkerframework.common.accumulation.AccumulationTransfer; import org.checkerframework.common.accumulation.AccumulationValue; @@ -50,6 +52,12 @@ public class CalledMethodsTransfer extends AccumulationTransfer { */ private final ExecutableElement calledMethodsValueElement; + /** + * True if -AenableWpiForRlc was passed on the command line. See {@link + * ResourceLeakChecker#ENABLE_WPI_FOR_RLC}. + */ + private final boolean enableWpiForRlc; + /** * Create a new CalledMethodsTransfer. * @@ -59,6 +67,40 @@ public CalledMethodsTransfer(CalledMethodsAnalysis analysis) { super(analysis); calledMethodsValueElement = ((CalledMethodsAnnotatedTypeFactory) atypeFactory).calledMethodsValueElement; + enableWpiForRlc = atypeFactory.getChecker().hasOption(ResourceLeakChecker.ENABLE_WPI_FOR_RLC); + } + + /** + * @param tree a tree + * @return false if Resource Leak Checker is running as one of the upstream checkers and the + * -AenableWpiForRlc flag (see {@link ResourceLeakChecker#ENABLE_WPI_FOR_RLC}) is not passed + * as a command line argument, otherwise returns the result of the super call + */ + @Override + protected boolean shouldPerformWholeProgramInference(Tree tree) { + if (!isWpiEnabledForRLC() + && atypeFactory.getCheckerNames().contains(ResourceLeakChecker.class.getCanonicalName())) { + return false; + } + return super.shouldPerformWholeProgramInference(tree); + } + + /** + * See {@link ResourceLeakChecker#ENABLE_WPI_FOR_RLC}. + * + * @param expressionTree a tree + * @param lhsTree its element + * @return false if Resource Leak Checker is running as one of the upstream checkers and the + * -AenableWpiForRlc flag is not passed as a command line argument, otherwise returns the + * result of the super call + */ + @Override + protected boolean shouldPerformWholeProgramInference(Tree expressionTree, Tree lhsTree) { + if (!isWpiEnabledForRLC() + && atypeFactory.getCheckerNames().contains(ResourceLeakChecker.class.getCanonicalName())) { + return false; + } + return super.shouldPerformWholeProgramInference(expressionTree, lhsTree); } @Override @@ -229,4 +271,14 @@ private void handleEnsuresCalledMethodsVarArgs( return atypeFactory.createAccumulatorAnnotation(newList); } + + /** + * Checks if WPI is enabled for the Resource Leak Checker inference. See {@link + * ResourceLeakChecker#ENABLE_WPI_FOR_RLC}. + * + * @return returns true if WPI is enabled for the Resource Leak Checker + */ + protected boolean isWpiEnabledForRLC() { + return enableWpiForRlc; + } } diff --git a/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallAnnotatedTypeFactory.java index 83a9f4c07d7..564edd8c2ee 100644 --- a/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallAnnotatedTypeFactory.java @@ -31,6 +31,7 @@ import org.checkerframework.checker.mustcall.qual.Owning; import org.checkerframework.checker.mustcall.qual.PolyMustCall; import org.checkerframework.checker.nullness.qual.Nullable; +import org.checkerframework.checker.resourceleak.ResourceLeakChecker; import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory; import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.dataflow.cfg.block.Block; @@ -116,6 +117,12 @@ public class MustCallAnnotatedTypeFactory extends BaseAnnotatedTypeFactory /** True if -AnoLightweightOwnership was passed on the command line. */ private final boolean noLightweightOwnership; + /** + * True if -AenableWpiForRlc (see {@link ResourceLeakChecker#ENABLE_WPI_FOR_RLC}) was passed on + * the command line. + */ + private final boolean enableWpiForRlc; + /** * Creates a MustCallAnnotatedTypeFactory. * @@ -132,6 +139,7 @@ public MustCallAnnotatedTypeFactory(BaseTypeChecker checker) { addAliasedTypeAnnotation(MustCallAlias.class, POLY); } noLightweightOwnership = checker.hasOption(MustCallChecker.NO_LIGHTWEIGHT_OWNERSHIP); + enableWpiForRlc = checker.hasOption(ResourceLeakChecker.ENABLE_WPI_FOR_RLC); this.postInit(); } @@ -223,6 +231,13 @@ protected void constructorFromUsePreSubstitution( */ private void changeNonOwningParameterTypesToTop( ExecutableElement declaration, AnnotatedExecutableType type) { + // Formal parameters without a declared owning annotation are disregarded by the RLC _analysis_, + // as their @MustCall obligation is set to Top in this method. However, this computation is not + // desirable for RLC _inference_ in unannotated programs, where a goal is to infer and add + // @Owning annotations to formal parameters. + if (getWholeProgramInference() != null && !isWpiEnabledForRLC()) { + return; + } List parameterTypes = type.getParameterTypes(); for (int i = 0; i < parameterTypes.size(); i++) { Element paramDecl = declaration.getParameters().get(i); @@ -416,7 +431,11 @@ public MustCallTreeAnnotator(MustCallAnnotatedTypeFactory mustCallAnnotatedTypeF @Override public Void visitIdentifier(IdentifierTree tree, AnnotatedTypeMirror type) { Element elt = TreeUtils.elementFromUse(tree); - if (elt.getKind() == ElementKind.PARAMETER + // The following changes are not desired for RLC _inference_ in unannotated programs, where a + // goal is to infer and add @Owning annotations to formal parameters. Therefore, if WPI is + // enabled, they should not be executed. + if (getWholeProgramInference() == null + && elt.getKind() == ElementKind.PARAMETER && (noLightweightOwnership || getDeclAnnotation(elt, Owning.class) == null)) { if (!type.hasPrimaryAnnotation(POLY)) { // Parameters that are not annotated with @Owning should be treated as bottom @@ -443,6 +462,16 @@ public Void visitIdentifier(IdentifierTree tree, AnnotatedTypeMirror type) { return tempVars.get(node.getTree()); } + /** + * Checks if WPI is enabled for the Resource Leak Checker inference. See {@link + * ResourceLeakChecker#ENABLE_WPI_FOR_RLC}. + * + * @return returns true if WPI is enabled for the Resource Leak Checker + */ + protected boolean isWpiEnabledForRLC() { + return enableWpiForRlc; + } + /** * Returns true if the given type should never have a must-call obligation. * diff --git a/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallTransfer.java b/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallTransfer.java index 0eddccc33d6..6b22b3ed4bf 100644 --- a/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallTransfer.java +++ b/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallTransfer.java @@ -3,6 +3,7 @@ import com.sun.source.tree.ClassTree; import com.sun.source.tree.ExpressionTree; import com.sun.source.tree.IdentifierTree; +import com.sun.source.tree.Tree; import com.sun.source.tree.VariableTree; import com.sun.source.util.TreePath; import java.util.List; @@ -14,6 +15,7 @@ import org.checkerframework.checker.mustcall.qual.MustCall; import org.checkerframework.checker.nullness.qual.MonotonicNonNull; import org.checkerframework.checker.nullness.qual.Nullable; +import org.checkerframework.checker.resourceleak.ResourceLeakChecker; import org.checkerframework.dataflow.analysis.TransferInput; import org.checkerframework.dataflow.analysis.TransferResult; import org.checkerframework.dataflow.cfg.node.AssignmentNode; @@ -58,6 +60,12 @@ public class MustCallTransfer extends CFTransfer { /** True if -AnoCreatesMustCallFor was passed on the command line. */ private final boolean noCreatesMustCallFor; + /** + * True if -AenableWpiForRlc was passed on the command line. See {@link + * ResourceLeakChecker#ENABLE_WPI_FOR_RLC}. + */ + private final boolean enableWpiForRlc; + /** * Create a MustCallTransfer. * @@ -68,6 +76,7 @@ public MustCallTransfer(CFAnalysis analysis) { atypeFactory = (MustCallAnnotatedTypeFactory) analysis.getTypeFactory(); noCreatesMustCallFor = atypeFactory.getChecker().hasOption(MustCallChecker.NO_CREATES_MUSTCALLFOR); + enableWpiForRlc = atypeFactory.getChecker().hasOption(ResourceLeakChecker.ENABLE_WPI_FOR_RLC); ProcessingEnvironment env = atypeFactory.getChecker().getProcessingEnvironment(); treeBuilder = new TreeBuilder(env); } @@ -175,6 +184,41 @@ private void lubWithStoreValue(CFStore store, JavaExpression expr, AnnotationMir store.insertValue(expr, newValue); } + /** + * See {@link ResourceLeakChecker#ENABLE_WPI_FOR_RLC}. + * + * @param tree a tree + * @return false if Resource Leak Checker is running as one of the upstream checkers and the + * -AenableWpiForRlc flag is not passed as a command line argument, otherwise returns the + * result of the super call + */ + @Override + protected boolean shouldPerformWholeProgramInference(Tree tree) { + if (!isWpiEnabledForRLC() + && atypeFactory.getCheckerNames().contains(ResourceLeakChecker.class.getCanonicalName())) { + return false; + } + return super.shouldPerformWholeProgramInference(tree); + } + + /** + * See {@link ResourceLeakChecker#ENABLE_WPI_FOR_RLC}. + * + * @param expressionTree a tree + * @param lhsTree its element + * @return false if Resource Leak Checker is running as one of the upstream checkers and the + * -AenableWpiForRlc flag is not passed as a command line argument, otherwise returns the + * result of the super call + */ + @Override + protected boolean shouldPerformWholeProgramInference(Tree expressionTree, Tree lhsTree) { + if (!isWpiEnabledForRLC() + && atypeFactory.getCheckerNames().contains(ResourceLeakChecker.class.getCanonicalName())) { + return false; + } + return super.shouldPerformWholeProgramInference(expressionTree, lhsTree); + } + @Override public TransferResult visitObjectCreation( ObjectCreationNode node, TransferInput input) { @@ -299,4 +343,14 @@ public void updateStoreWithTempVar(TransferResult result, Node protected String uniqueName(String prefix) { return prefix + "-" + uid.getAndIncrement(); } + + /** + * Checks if WPI is enabled for the Resource Leak Checker inference. See {@link + * ResourceLeakChecker#ENABLE_WPI_FOR_RLC}. + * + * @return returns true if WPI is enabled for the Resource Leak Checker + */ + protected boolean isWpiEnabledForRLC() { + return enableWpiForRlc; + } } diff --git a/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallVisitor.java b/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallVisitor.java index bbc0e5b8a05..368a8508996 100644 --- a/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallVisitor.java @@ -23,6 +23,7 @@ import org.checkerframework.checker.mustcall.qual.MustCallAlias; import org.checkerframework.checker.mustcall.qual.NotOwning; import org.checkerframework.checker.mustcall.qual.Owning; +import org.checkerframework.checker.mustcall.qual.PolyMustCall; import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.common.basetype.BaseTypeVisitor; import org.checkerframework.framework.type.AnnotatedTypeMirror; @@ -232,9 +233,24 @@ public boolean isValidUse( // Note that isValidUse does not need to consider component types, on which it should be // called separately. Element elt = TreeUtils.elementFromTree(tree); - if (elt != null - && AnnotationUtils.containsSameByClass(elt.getAnnotationMirrors(), MustCallAlias.class)) { - return true; + if (elt != null) { + if (AnnotationUtils.containsSameByClass(elt.getAnnotationMirrors(), MustCallAlias.class)) { + return true; + } + // Need to check the type mirror for ajava-derived annotations and the element itself + // for human-written annotations from the source code. Getting to the ajava file directly + // at this point is impossible, so we approximate "the ajava file has an @MustCallAlias + // annotation" with "there is an @PolyMustCall annotation on the use type, but not in the + // source code". This only works because none of our inference techniques infer @PolyMustCall, + // so if @PolyMustCall is present but wasn't in the source, it must have been derived from + // an @MustCallAlias annotation (which we do infer). + boolean ajavaFileHasMustCallAlias = + useType.hasPrimaryAnnotation(PolyMustCall.class) + && !AnnotationUtils.containsSameByClass( + elt.getAnnotationMirrors(), PolyMustCall.class); + if (ajavaFileHasMustCallAlias) { + return true; + } } return super.isValidUse(declarationType, useType, tree); } diff --git a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java index 563f545cbac..7e2170d270f 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java @@ -14,6 +14,7 @@ import java.io.UnsupportedEncodingException; import java.util.ArrayDeque; import java.util.ArrayList; +import java.util.Collection; import java.util.Collections; import java.util.Deque; import java.util.EnumSet; @@ -27,6 +28,7 @@ import java.util.Objects; import java.util.Set; import java.util.StringJoiner; +import java.util.stream.Collectors; import javax.lang.model.SourceVersion; import javax.lang.model.element.AnnotationMirror; import javax.lang.model.element.Element; @@ -839,7 +841,8 @@ private boolean areSame(JavaExpression target, @Nullable JavaExpression enclosin * @param node the invocation node whose result is to be tracked; must be {@link * MethodInvocationNode} or {@link ObjectCreationNode} */ - private void updateObligationsWithInvocationResult(Set obligations, Node node) { + /*package-private*/ void updateObligationsWithInvocationResult( + Set obligations, Node node) { Tree tree = node.getTree(); // Only track the result of the call if there is a temporary variable for the call node // (because if there is no temporary, then the invocation must produce an untrackable value, @@ -1106,7 +1109,7 @@ private void updateObligationsForOwningReturn( * @param node a node * @return the temporary for node, or node if no temporary exists */ - private Node getTempVarOrNode(Node node) { + /*package-private*/ Node getTempVarOrNode(Node node) { Node temp = typeFactory.getTempVarForNode(node); if (temp != null) { return temp; @@ -1274,7 +1277,7 @@ private boolean hasAtMostOneOwningField(TypeElement element) { * @param node the node * @return true if must-call type of node only contains close */ - private boolean isMustCallClose(Node node) { + /*package-private*/ boolean isMustCallClose(Node node) { MustCallAnnotatedTypeFactory mcAtf = typeFactory.getTypeFactoryOfSubchecker(MustCallChecker.class); AnnotatedTypeMirror mustCallAnnotatedType = mcAtf.getAnnotatedType(node.getTree()); @@ -1318,7 +1321,8 @@ private void addAliasToObligationsContainingVar( * @param obligations the set of Obligations to modify * @param var a variable */ - private void removeObligationsContainingVar(Set obligations, LocalVariableNode var) { + /*package-private*/ void removeObligationsContainingVar( + Set obligations, LocalVariableNode var) { removeObligationsContainingVar( obligations, var, MustCallAliasHandling.NO_SPECIAL_HANDLING, MethodExitKind.ALL); } @@ -1404,7 +1408,7 @@ private void removeObligationsContainingVar( * temporary variable (via a call to {@link * ResourceLeakAnnotatedTypeFactory#getTempVarForNode}) */ - private void updateObligationsForPseudoAssignment( + /*package-private*/ void updateObligationsForPseudoAssignment( Set obligations, Node node, LocalVariableNode lhsVar, Node rhs) { // Replacements to eventually perform in Obligations. This map is kept to avoid a // ConcurrentModificationException in the loop below. @@ -1831,7 +1835,7 @@ private Node removeCastsAndGetTmpVarIfPresent(Node node) { * @param node a MethodInvocation or ObjectCreation node * @return the arguments, in order */ - private List getArgumentsOfInvocation(Node node) { + /*package-private*/ List getArgumentsOfInvocation(Node node) { if (node instanceof MethodInvocationNode) { MethodInvocationNode invocationNode = (MethodInvocationNode) node; return invocationNode.getArguments(); @@ -1850,7 +1854,7 @@ private List getArgumentsOfInvocation(Node node) { * @return a list of the declarations of the formal parameters of the method or constructor being * invoked */ - private List getParametersOfInvocation(Node node) { + /*package-private*/ List getParametersOfInvocation(Node node) { ExecutableElement executableElement; if (node instanceof MethodInvocationNode) { MethodInvocationNode invocationNode = (MethodInvocationNode) node; @@ -2301,7 +2305,7 @@ private static boolean varTrackedInObligations( * @return the Obligation in {@code obligations} whose resource alias set contains {@code node}, * or {@code null} if there is no such Obligation */ - private static @Nullable Obligation getObligationForVar( + /*package-private*/ static @Nullable Obligation getObligationForVar( Set obligations, LocalVariableNode node) { for (Obligation obligation : obligations) { if (obligation.canBeSatisfiedThrough(node)) { @@ -2462,7 +2466,7 @@ private void incrementMustCallImpl(TypeMirror type) { * @return true iff cmAnno is a subtype of a called-methods annotation with the same values as * mustCallValues */ - private boolean calledMethodsSatisfyMustCall( + /*package-private*/ boolean calledMethodsSatisfyMustCall( List mustCallValues, AnnotationMirror cmAnno) { // Create this annotation and use a subtype test because there's no guarantee that // cmAnno is actually an instance of CalledMethods: it could be CMBottom or CMPredicate. @@ -2566,7 +2570,7 @@ private static void propagate( * consists of BlockWithObligations objects, each representing the need to handle the set of * dataflow facts reaching the block during analysis. */ - private static class BlockWithObligations { + /*package-private*/ static class BlockWithObligations { /** The block. */ public final Block block; @@ -2602,5 +2606,58 @@ public boolean equals(@Nullable Object o) { public int hashCode() { return Objects.hash(block, obligations); } + + @Override + public String toString() { + return String.format( + "BWO{%s %d, %d obligations %d}", + block.getType(), block.getUid(), obligations.size(), obligations.hashCode()); + } + + /** + * Returns a printed representation of a collection of BlockWithObligations. If a + * BlockWithObligations appears multiple times in the collection, it is printed more succinctly + * after the first time. + * + * @param bwos a collection of BlockWithObligations, to format + * @return a printed representation of a collection of BlockWithObligations + */ + public static String collectionToString(Collection bwos) { + List blocksWithDuplicates = new ArrayList<>(); + for (BlockWithObligations bwo : bwos) { + blocksWithDuplicates.add(bwo.block); + } + List duplicateBlocks = duplicates(blocksWithDuplicates); + StringJoiner result = new StringJoiner(", ", "BWOs[", "]"); + for (BlockWithObligations bwo : bwos) { + ImmutableSet obligations = bwo.obligations; + if (duplicateBlocks.contains(bwo.block)) { + result.add( + String.format( + "BWO{%s %d, %d obligations %s}", + bwo.block.getType(), bwo.block.getUid(), obligations.size(), obligations)); + } else { + result.add( + String.format( + "BWO{%s %d, %d obligations}", + bwo.block.getType(), bwo.block.getUid(), obligations.size())); + } + } + return result.toString(); + } + } + + // TODO: Use from plume-lib's CollectionsPlume once version 1.9.0 is released. + /** + * Returns the elements (once each) that appear more than once in the given collection. + * + * @param the type of elements + * @param c a collection + * @return the elements (once each) that appear more than once in the given collection + */ + public static List duplicates(Collection c) { + // Inefficient (because of streams) but simple implementation. + Set withoutDuplicates = new HashSet<>(); + return c.stream().filter(n -> !withoutDuplicates.add(n)).collect(Collectors.toList()); } } diff --git a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInference.java b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInference.java index edda1b2e08d..1a1e55bf0dd 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInference.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInference.java @@ -1,176 +1,791 @@ package org.checkerframework.checker.resourceleak; +import com.google.common.collect.ImmutableSet; +import com.sun.source.tree.ClassTree; +import com.sun.source.tree.MethodTree; +import com.sun.source.tree.VariableTree; import java.util.ArrayDeque; -import java.util.ArrayList; +import java.util.Arrays; +import java.util.Collections; import java.util.Deque; import java.util.HashSet; +import java.util.LinkedHashMap; +import java.util.LinkedHashSet; import java.util.List; +import java.util.Map; import java.util.Set; import javax.lang.model.element.AnnotationMirror; import javax.lang.model.element.Element; +import javax.lang.model.element.ElementKind; +import javax.lang.model.element.ExecutableElement; +import javax.lang.model.element.Modifier; +import javax.lang.model.element.TypeElement; import javax.lang.model.element.VariableElement; +import javax.lang.model.type.TypeMirror; +import org.checkerframework.checker.calledmethods.qual.EnsuresCalledMethods; +import org.checkerframework.checker.mustcall.qual.InheritableMustCall; import org.checkerframework.checker.mustcall.qual.Owning; +import org.checkerframework.checker.nullness.qual.Nullable; +import org.checkerframework.checker.resourceleak.MustCallConsistencyAnalyzer.BlockWithObligations; +import org.checkerframework.checker.resourceleak.MustCallConsistencyAnalyzer.MethodExitKind; +import org.checkerframework.checker.resourceleak.MustCallConsistencyAnalyzer.Obligation; +import org.checkerframework.checker.resourceleak.MustCallConsistencyAnalyzer.ResourceAlias; +import org.checkerframework.common.accumulation.AccumulationStore; +import org.checkerframework.common.accumulation.AccumulationValue; import org.checkerframework.common.wholeprograminference.WholeProgramInference; import org.checkerframework.dataflow.cfg.ControlFlowGraph; +import org.checkerframework.dataflow.cfg.UnderlyingAST; import org.checkerframework.dataflow.cfg.block.Block; import org.checkerframework.dataflow.cfg.block.ConditionalBlock; import org.checkerframework.dataflow.cfg.block.SingleSuccessorBlock; +import org.checkerframework.dataflow.cfg.node.ArrayCreationNode; +import org.checkerframework.dataflow.cfg.node.AssignmentNode; +import org.checkerframework.dataflow.cfg.node.LocalVariableNode; import org.checkerframework.dataflow.cfg.node.MethodInvocationNode; import org.checkerframework.dataflow.cfg.node.Node; +import org.checkerframework.dataflow.cfg.node.ObjectCreationNode; +import org.checkerframework.dataflow.expression.JavaExpression; +import org.checkerframework.dataflow.expression.LocalVariable; +import org.checkerframework.dataflow.util.NodeUtils; import org.checkerframework.javacutil.AnnotationBuilder; +import org.checkerframework.javacutil.AnnotationUtils; import org.checkerframework.javacutil.BugInCF; +import org.checkerframework.javacutil.TreePathUtil; import org.checkerframework.javacutil.TreeUtils; +import org.checkerframework.javacutil.TypesUtils; +import org.plumelib.util.CollectionsPlume; /** - * This class contains the Resource Leak Checker's annotation inference algorithm. It contains - * inference logic for owning annotations on final owning fields. It adds an @Owning annotation on a - * field if it finds a method that satisfies the @MustCall obligation of the field along some path - * to the regular exit point. + * This class implements the annotation inference algorithm for the Resource Leak Checker. It infers + * annotations such as {@code @}{@link Owning} on owning fields and parameters, {@code @}{@link + * EnsuresCalledMethods} on methods, and {@code @}{@link InheritableMustCall} on class declarations. + * + *

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

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

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

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

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

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

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

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

    + *
  • If a formal parameter is passed as an owning parameter, add an @Owning annotation to that + * formal parameter (see {@link #inferOwningParamsViaOwnershipTransfer}). + *
  • It calls {@link #computeOwningForArgsOrReceiverOfCall} to compute @Owning annotations for + * the receiver or arguments of a call by analyzing the called-methods set after the call. + *
+ * + * @param obligations the set of obligations to search in + * @param invocation the method or constructor invocation + */ + private void computeOwningFromInvocation(Set obligations, Node invocation) { + if (invocation instanceof ObjectCreationNode) { + // If the invocation corresponds to an object creation node, only ownership transfer checking + // is required, as constructor parameters may have an @Owning annotation. We do not handle + // @EnsuresCalledMethods annotations on constructors as we have not observed them in practice. + inferOwningParamsViaOwnershipTransfer(obligations, invocation); + } else if (invocation instanceof MethodInvocationNode) { + inferOwningParamsViaOwnershipTransfer(obligations, invocation); + computeOwningForArgsOrReceiverOfCall(obligations, (MethodInvocationNode) invocation); + } + } - successorBlock.add(ccur.getThenSuccessor()); - successorBlock.add(ccur.getElseSuccessor()); + /** + * Returns the called methods annotation for the given Java expression after the invocation node. + * + * @param invocation the MethodInvocationNode + * @param varJe a Java expression + * @return the called methods annotation for the {@code varJe} after the {@code invocation} node. + */ + private AnnotationMirror getCalledMethodsAnno( + MethodInvocationNode invocation, JavaExpression varJe) { + AccumulationStore cmStoreAfter = resourceLeakAtf.getStoreAfter(invocation); + AccumulationValue cmValue = cmStoreAfter == null ? null : cmStoreAfter.getValue(varJe); - } else { - if (!(cur instanceof SingleSuccessorBlock)) { - throw new BugInCF("BlockImpl is neither a conditional block nor a SingleSuccessorBlock"); + AnnotationMirror cmAnno = null; + + if (cmValue != null) { + // The store contains the lhs. + Set accumulatedValues = cmValue.getAccumulatedValues(); + if (accumulatedValues != null) { // type variable or wildcard type + cmAnno = resourceLeakAtf.createCalledMethods(accumulatedValues.toArray(new String[0])); + } else { + for (AnnotationMirror anno : cmValue.getAnnotations()) { + if (AnnotationUtils.areSameByName( + anno, "org.checkerframework.checker.calledmethods.qual.CalledMethods")) { + cmAnno = anno; + } + } } + } + + if (cmAnno == null) { + cmAnno = resourceLeakAtf.top; + } + + return cmAnno; + } + + /** + * Adds all non-exceptional successors to {@code worklist}. + * + * @param obligations the obligations for the current block + * @param curBlock the block whose successors to add to the worklist + * @param visited block-Obligations pairs already analyzed or already on the worklist + * @param worklist the worklist, which is side-effected by this method + */ + private void addNonExceptionalSuccessorsToWorklist( + Set obligations, + Block curBlock, + Set visited, + Deque worklist) { - Block b = ((SingleSuccessorBlock) cur).getSuccessor(); - if (b != null) { - successorBlock.add(b); + for (Block successor : getNonExceptionalSuccessors(curBlock)) { + // If successor is a special block, it must be the regular exit. + if (successor.getType() != Block.BlockType.SPECIAL_BLOCK) { + BlockWithObligations state = new BlockWithObligations(successor, obligations); + if (visited.add(state)) { + worklist.add(state); + } } } - return successorBlock; + } + + /** + * Returns the non-exceptional successors of a block. + * + * @param cur a block + * @return the successors of the given block + */ + private List getNonExceptionalSuccessors(Block cur) { + if (cur.getType() == Block.BlockType.CONDITIONAL_BLOCK) { + ConditionalBlock ccur = (ConditionalBlock) cur; + return Arrays.asList(ccur.getThenSuccessor(), ccur.getElseSuccessor()); + } + if (!(cur instanceof SingleSuccessorBlock)) { + throw new BugInCF("Not a conditional block nor a SingleSuccessorBlock: " + cur); + } + + Block successor = ((SingleSuccessorBlock) cur).getSuccessor(); + if (successor != null) { + return Collections.singletonList(successor); + } + return Collections.emptyList(); + } + + /** + * Creates an {@code @EnsuresCalledMethods} annotation with the given arguments. + * + * @param value the expressions that will have methods called on them + * @param methods the methods guaranteed to be invoked on the expressions + * @return an {@code @EnsuresCalledMethods} annotation with the given arguments + */ + private AnnotationMirror createEnsuresCalledMethods(String[] value, String[] methods) { + AnnotationBuilder builder = + new AnnotationBuilder(resourceLeakAtf.getProcessingEnv(), EnsuresCalledMethods.class); + builder.setValue("value", value); + builder.setValue("methods", methods); + AnnotationMirror am = builder.build(); + return am; + } + + /** + * Creates an {@code @InheritableMustCall} annotation with the given arguments. + * + * @param methods methods that might need to be called on the expression whose type is annotated + * @return an {@code @InheritableMustCall} annotation with the given arguments + */ + private AnnotationMirror createInheritableMustCall(String[] methods) { + AnnotationBuilder builder = + new AnnotationBuilder(resourceLeakAtf.getProcessingEnv(), InheritableMustCall.class); + Arrays.sort(methods); + builder.setValue("value", methods); + return builder.build(); } } diff --git a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakAnnotatedTypeFactory.java index 00b0244db4a..adf5f107a66 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakAnnotatedTypeFactory.java @@ -36,7 +36,6 @@ import org.checkerframework.framework.type.AnnotatedTypeMirror; import org.checkerframework.framework.type.GenericAnnotatedTypeFactory; import org.checkerframework.javacutil.AnnotationUtils; -import org.checkerframework.javacutil.ElementUtils; import org.checkerframework.javacutil.TreeUtils; import org.checkerframework.javacutil.TypeSystemError; @@ -103,16 +102,14 @@ public ResourceLeakAnnotatedTypeFactory(BaseTypeChecker checker) { } /** - * Is the given element a candidate to be an owning field? A candidate owning field must be final - * and have a non-empty must-call obligation. + * Is the given element a candidate to be an owning field? A candidate owning field must have a + * non-empty must-call obligation. * * @param element a element - * @return true iff the given element is a final field with non-empty @MustCall obligation + * @return true iff the given element is a field with non-empty @MustCall obligation */ - /*package-private*/ boolean isCandidateOwningField(Element element) { - return (element.getKind().isField() - && ElementUtils.isFinal(element) - && !hasEmptyMustCallValue(element)); + /*package-private*/ boolean isFieldWithNonemptyMustCallValue(Element element) { + return element.getKind().isField() && !hasEmptyMustCallValue(element); } @Override @@ -137,11 +134,11 @@ public void postAnalyze(ControlFlowGraph cfg) { new MustCallConsistencyAnalyzer(this, this.analysis); mustCallConsistencyAnalyzer.analyze(cfg); - // Inferring owning annotations for final owning fields + // Inferring owning annotations for @Owning fields/parameters, @EnsuresCalledMethods for + // finalizer methods and @InheritableMustCall annotations for the class declarations. if (getWholeProgramInference() != null) { if (cfg.getUnderlyingAST().getKind() == UnderlyingAST.Kind.METHOD) { - MustCallInference mustCallInferenceLogic = new MustCallInference(this, cfg); - mustCallInferenceLogic.runInference(); + MustCallInference.runMustCallInference(this, cfg, mustCallConsistencyAnalyzer); } } @@ -221,7 +218,7 @@ protected ResourceLeakAnalysis createFlowAnalysis() { * @param element an element * @return the strings in its must-call type */ - /*package-private*/ List getMustCallValue(Element element) { + /*package-private*/ List getMustCallValues(Element element) { MustCallAnnotatedTypeFactory mustCallAnnotatedTypeFactory = getTypeFactoryOfSubchecker(MustCallChecker.class); AnnotatedTypeMirror mustCallAnnotatedType = diff --git a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakChecker.java b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakChecker.java index 47d31715e61..ec55e6d6712 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakChecker.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakChecker.java @@ -23,7 +23,8 @@ ResourceLeakChecker.COUNT_MUST_CALL, MustCallChecker.NO_CREATES_MUSTCALLFOR, MustCallChecker.NO_LIGHTWEIGHT_OWNERSHIP, - MustCallChecker.NO_RESOURCE_ALIASES + MustCallChecker.NO_RESOURCE_ALIASES, + ResourceLeakChecker.ENABLE_WPI_FOR_RLC, }) @StubFiles("IOUtils.astub") public class ResourceLeakChecker extends CalledMethodsChecker { @@ -38,6 +39,15 @@ public ResourceLeakChecker() {} */ public static final String COUNT_MUST_CALL = "countMustCall"; + /** + * Ordinarily, when the -Ainfer flag is used, whole-program inference is run for every checker and + * sub-checker. However, the Resource Leak Checker is different. The -Ainfer flag enables the + * RLC's own (non-WPI) inference mechanism ({@link MustCallInference}). To use WPI in addition to + * this mechanism for its sub-checkers, use the -AenableWpiForRlc flag, which is intended only for + * testing and experiments. + */ + public static final String ENABLE_WPI_FOR_RLC = "enableWpiForRlc"; + /** * The number of expressions with must-call obligations that were checked. Incremented only if the * {@link #COUNT_MUST_CALL} command-line option was supplied. diff --git a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakVisitor.java b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakVisitor.java index b3df56f9b3b..be36474ea9a 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakVisitor.java @@ -50,6 +50,12 @@ public class ResourceLeakVisitor extends CalledMethodsVisitor { /** True if -AnoLightweightOwnership was supplied on the command line. */ private final boolean noLightweightOwnership; + /** + * True if -AenableWpiForRlc was passed on the command line. See {@link + * ResourceLeakChecker#ENABLE_WPI_FOR_RLC}. + */ + private final boolean enableWpiForRlc; + /** * Create the visitor. * @@ -60,6 +66,7 @@ public ResourceLeakVisitor(BaseTypeChecker checker) { rlTypeFactory = (ResourceLeakAnnotatedTypeFactory) atypeFactory; permitStaticOwning = checker.hasOption("permitStaticOwning"); noLightweightOwnership = checker.hasOption("noLightweightOwnership"); + enableWpiForRlc = checker.hasOption(ResourceLeakChecker.ENABLE_WPI_FOR_RLC); } @Override @@ -188,6 +195,11 @@ private void checkOwningOverrides( } } + @Override + protected boolean shouldPerformContractInference() { + return atypeFactory.getWholeProgramInference() != null && isWpiEnabledForRLC(); + } + // Overwritten to check that destructors (i.e. methods responsible for resolving // the must-call obligations of owning fields) enforce a stronger version of // @EnsuresCalledMethods: that the claimed @CalledMethods annotation is true on @@ -381,7 +393,7 @@ private void checkOwningField(Element field) { // This value is side-effected. List unsatisfiedMustCallObligationsOfOwningField = - rlTypeFactory.getMustCallValue(field); + rlTypeFactory.getMustCallValues(field); if (unsatisfiedMustCallObligationsOfOwningField.isEmpty()) { return; @@ -389,7 +401,7 @@ private void checkOwningField(Element field) { String error; Element enclosingElement = field.getEnclosingElement(); - List enclosingMustCallValues = rlTypeFactory.getMustCallValue(enclosingElement); + List enclosingMustCallValues = rlTypeFactory.getMustCallValues(enclosingElement); if (enclosingMustCallValues == null) { error = @@ -454,4 +466,14 @@ private void checkOwningField(Element field) { error); } } + + /** + * Checks if WPI is enabled for the Resource Leak Checker inference. See {@link + * ResourceLeakChecker#ENABLE_WPI_FOR_RLC}. + * + * @return returns true if WPI is enabled for the Resource Leak Checker + */ + protected boolean isWpiEnabledForRLC() { + return enableWpiForRlc; + } } diff --git a/checker/tests/ainfer-resourceleak/non-annotated/ECMInference.java b/checker/tests/ainfer-resourceleak/non-annotated/ECMInference.java index e5e9353d766..7fecb377aa4 100644 --- a/checker/tests/ainfer-resourceleak/non-annotated/ECMInference.java +++ b/checker/tests/ainfer-resourceleak/non-annotated/ECMInference.java @@ -1,3 +1,6 @@ +// @skip-test the test contains no resource types to infer. +// To pass this test, RLC's inference needs to infer CalledMethods annotations for empty must-call +// types, which requires the -AenableWpirForRLC flag. import org.checkerframework.checker.calledmethods.qual.CalledMethods; public class ECMInference { diff --git a/checker/tests/ainfer-resourceleak/non-annotated/EnsuresCalledMethodsTest.java b/checker/tests/ainfer-resourceleak/non-annotated/EnsuresCalledMethodsTest.java new file mode 100644 index 00000000000..65c1fb5cf4b --- /dev/null +++ b/checker/tests/ainfer-resourceleak/non-annotated/EnsuresCalledMethodsTest.java @@ -0,0 +1,29 @@ +import org.checkerframework.checker.calledmethods.qual.*; +import org.checkerframework.checker.mustcall.qual.*; + +class EnsuresCalledMethodsTest { + @InheritableMustCall("a") + static class Foo { + void a() {} + } + + @InheritableMustCall("close") + class ECM { + // :: warning: (required.method.not.called) + @Owning Foo foo; + + private void closePrivate() { + if (foo != null) { + foo.a(); + foo = null; + } + } + + void close() { + if (foo != null) { + foo.a(); + foo = null; + } + } + } +} diff --git a/checker/tests/ainfer-resourceleak/non-annotated/EnsuresCalledMethodsVarArgsTest.java b/checker/tests/ainfer-resourceleak/non-annotated/EnsuresCalledMethodsVarArgsTest.java new file mode 100644 index 00000000000..a8ebf5b0fea --- /dev/null +++ b/checker/tests/ainfer-resourceleak/non-annotated/EnsuresCalledMethodsVarArgsTest.java @@ -0,0 +1,60 @@ +import org.checkerframework.checker.calledmethods.qual.*; +import org.checkerframework.checker.mustcall.qual.*; + +class EnsuresCalledMethodsVarArgsTest { + + @InheritableMustCall("a") + static class Foo { + void a() {} + } + + static class Utils { + @SuppressWarnings("ensuresvarargs.unverified") + @EnsuresCalledMethodsVarArgs("a") + public static void close(Foo... foos) { + for (Foo f : foos) { + if (f != null) { + f.a(); + } + } + } + } + + private class ECMVA { + final Foo foo; + + ECMVA() { + // :: warning: (required.method.not.called) + foo = new Foo(); + } + + void finalyzer() { + Utils.close(foo); + } + + @EnsuresCalledMethods( + value = {"#1"}, + methods = {"a"}) + void closef(Foo f) { + if (f != null) { + Utils.close(f); + } + } + + void owningParam(Foo f) { + Foo foo = f; + Utils.close(foo); + } + + void testOwningParamOnOwningParam() { + // :: warning: (required.method.not.called) + Foo f = new Foo(); + owningParam(f); + } + } + + void testCorrect() { + ECMVA e = new ECMVA(); + e.finalyzer(); + } +} diff --git a/checker/tests/ainfer-resourceleak/non-annotated/OwnershipTransferOnConstructor.java b/checker/tests/ainfer-resourceleak/non-annotated/OwnershipTransferOnConstructor.java new file mode 100644 index 00000000000..96b4382db38 --- /dev/null +++ b/checker/tests/ainfer-resourceleak/non-annotated/OwnershipTransferOnConstructor.java @@ -0,0 +1,28 @@ +import java.io.IOException; +import java.net.*; +import org.checkerframework.checker.calledmethods.qual.*; +import org.checkerframework.checker.mustcall.qual.*; + +class OwnershipTransferOnConstructor { + static class Foo { + Foo(@Owning Socket s) { + try { + s.close(); + } catch (IOException e) { + + } + } + } + + private class Bar { + void baz(Socket s) { + Foo f = new Foo(s); + } + + // :: warning: (required.method.not.called) + void testOwningOnBaz(@Owning Socket s) { + Socket s2 = s; + baz(s2); + } + } +} diff --git a/checker/tests/ainfer-resourceleak/non-annotated/OwningFieldIndirectCall.java b/checker/tests/ainfer-resourceleak/non-annotated/OwningFieldIndirectCall.java new file mode 100644 index 00000000000..7c2c542e9b7 --- /dev/null +++ b/checker/tests/ainfer-resourceleak/non-annotated/OwningFieldIndirectCall.java @@ -0,0 +1,37 @@ +import org.checkerframework.checker.calledmethods.qual.*; +import org.checkerframework.checker.mustcall.qual.*; + +class OwningFieldIndirectCall { + + @InheritableMustCall("a") + static class Foo { + void a() {} + } + + static class Utility { + @EnsuresCalledMethods(value = "#1", methods = "a") + public static void closeStream(Foo f) { + if (f != null) { + f.a(); + } + } + } + + static class DisposeFieldUsingECM { + final Foo f; // expect owning annotation for this field + + DisposeFieldUsingECM() { + // :: warning: (required.method.not.called) + f = new Foo(); + } + + void dispose() { + Utility.closeStream(f); + } + } + + void testCorrect() { + DisposeFieldUsingECM d = new DisposeFieldUsingECM(); + d.dispose(); + } +} diff --git a/checker/tests/ainfer-resourceleak/non-annotated/OwningParams.java b/checker/tests/ainfer-resourceleak/non-annotated/OwningParams.java new file mode 100644 index 00000000000..1c1cd29eeef --- /dev/null +++ b/checker/tests/ainfer-resourceleak/non-annotated/OwningParams.java @@ -0,0 +1,60 @@ +import org.checkerframework.checker.calledmethods.qual.*; +import org.checkerframework.checker.mustcall.qual.*; + +class OwningParams { + @InheritableMustCall("a") + static class Foo { + void a() {} + } + + private class OwningParamsDirectCall { + void passOwnership(Foo f) { + f.a(); + } + + void passOwnershipTest() { + // :: warning: (required.method.not.called) + Foo f = new Foo(); + passOwnership(f); + } + } + + private class OwningParamsIndirectCall { + @EnsuresCalledMethods( + value = {"#1"}, + methods = {"a"}) + void hasECM(Foo f) { + f.a(); + } + + void owningFoo(@Owning Foo f) { + f.a(); + } + + void passOwnership(Foo f1, Foo f2) { + Foo f11 = f1; + hasECM(f11); + Foo f22 = f2; + owningFoo(f22); + } + + void checkAlias(Foo f1) { + Foo f2 = f1; + f2.a(); + } + + void checkAliasTest() { + // :: warning: (required.method.not.called) + Foo f = new Foo(); + checkAlias(f); + } + + void passOwnershipTest() { + // :: warning: (required.method.not.called) + Foo f1 = new Foo(); + // :: warning: (required.method.not.called) + Foo f2 = new Foo(); + passOwnership(f1, f2); + } + } +} diff --git a/docs/manual/resource-leak-checker.tex b/docs/manual/resource-leak-checker.tex index f698954b86f..2f6dfb3c1dc 100644 --- a/docs/manual/resource-leak-checker.tex +++ b/docs/manual/resource-leak-checker.tex @@ -58,6 +58,9 @@ See Section~\ref{resource-leak-owning-fields}. \item[\<-ApermitInitializationLeak>] See Section~\ref{resource-leak-field-initialization}. +%% TODO: Uncomment when the feature is ready to be publicized. +% \item[\<-AenableWpiForRlc>] +% See Section~\ref{resource-leak-checker-inference-algo}. \end{description} If you are running the Resource Leak Checker, then there is no need to run @@ -585,6 +588,19 @@ not possible, the programmer will probably need to suppress a warning and then verify the code using a method other than the Resource Leak Checker. + +%% TODO: Uncomment when the feature is ready to be publicized. +% \sectionAndLabel{Resource Leak Checker Annotation Inference Algorithm}{resource-leak-checker-inference-algo} +% +% We are developing a special inference mechanism to infer annotations for +% the Resource Leak Checker. By default, this mechanism operates when the +% -Ainfer flag is enabled. To utilize the whole-program inference mechanism outlined in +% section \ref{whole-program-inference} in addition to this mechanism for the Resource +% Leak Checker and its sub-checkers, you should provide the \<-AenableWpiForRlc> flag. +% +% The paper \href={https://arxiv.org/pdf/2306.11953.pdf}{Automatic Inference of Resource Leak Specifications}, published at OOPSLA 2023, gives more details on the inference algorithm. Currently, only the first phase of the algorithm described in the paper is available, and the complete implementation will be available soon. + + % LocalWords: de subchecker OutputStream MustCall MustCallUnknown RAII Un % LocalWords: PolyMustCall InheritableMustCall MultiRandSelector callsite % LocalWords: Partitioner CalledMethods AnoLightweightOwnership NotOwning diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java index f790dfe171d..4fcbfd4a15c 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -1024,7 +1024,7 @@ public Void visitMethod(MethodTree tree, Void p) { checkContractsAtMethodDeclaration(tree, methodElement, formalParamNames, abstractMethod); // Infer postconditions - if (atypeFactory.getWholeProgramInference() != null) { + if (shouldPerformContractInference()) { assert ElementUtils.isElementFromSourceCode(methodElement); // TODO: Infer conditional postconditions too. @@ -1046,6 +1046,18 @@ public Void visitMethod(MethodTree tree, Void p) { } } + /** + * Should Whole Program Inference attempt to infer contract annotations? Typically, the answer is + * "yes" whenever WPI is enabled, but this method exists to allow subclasses to customize that + * behavior. + * + * @return true if contract inference should be performed, false if it should be disabled (even + * when WPI is enabled) + */ + protected boolean shouldPerformContractInference() { + return atypeFactory.getWholeProgramInference() != null; + } + /** * Check method purity if needed. Note that overriding rules are checked as part of {@link * #checkOverride(MethodTree, AnnotatedTypeMirror.AnnotatedExecutableType, diff --git a/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceJavaParserStorage.java b/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceJavaParserStorage.java index 0c9cc0665b3..8fc817c8af7 100644 --- a/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceJavaParserStorage.java +++ b/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceJavaParserStorage.java @@ -1905,10 +1905,6 @@ public boolean addDeclarationAnnotation(AnnotationMirror annotation) { * nodes for that field. */ public void transferAnnotations() { - if (type == null) { - return; - } - if (declarationAnnotations != null) { // Don't add directly to the type of the variable declarator, // because declaration annotations need to be attached to the FieldDeclaration diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java index 3b08ed8cbe0..ce0a531e23c 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java @@ -1015,7 +1015,7 @@ public TransferResult visitInstanceOf(InstanceOfNode node, TransferInput