From 695416da3ed22e85543eb00f5a765150c3610e40 Mon Sep 17 00:00:00 2001 From: Nargeshdb Date: Sun, 14 May 2023 21:31:41 -0700 Subject: [PATCH 001/132] first phase --- checker/build.gradle | 8 + .../calledmethods/CalledMethodsTransfer.java | 11 + .../MustCallAnnotatedTypeFactory.java | 11 +- .../checker/mustcall/MustCallTransfer.java | 15 +- .../checker/mustcall/MustCallVisitor.java | 24 +- .../MustCallConsistencyAnalyzer.java | 15 +- .../resourceleak/MustCallInferenceLogic.java | 559 ++++++++++++++++-- .../ResourceLeakAnnotatedTypeFactory.java | 8 +- .../resourceleak/ResourceLeakVisitor.java | 25 +- .../EnsuresCalledMethodsTest.java | 41 ++ .../EnsuresCalledMethodsVarArgsTest.java | 49 ++ .../OwningFieldIndirectCall.java | 37 ++ .../non-annotated/OwningParams.java | 47 ++ .../accumulation/AccumulationTransfer.java | 2 +- .../common/basetype/BaseTypeVisitor.java | 14 +- ...holeProgramInferenceJavaParserStorage.java | 33 +- .../framework/flow/CFAbstractTransfer.java | 4 +- 17 files changed, 810 insertions(+), 93 deletions(-) create mode 100644 checker/tests/ainfer-resourceleak/non-annotated/EnsuresCalledMethodsTest.java create mode 100644 checker/tests/ainfer-resourceleak/non-annotated/EnsuresCalledMethodsVarArgsTest.java create mode 100644 checker/tests/ainfer-resourceleak/non-annotated/OwningFieldIndirectCall.java create mode 100644 checker/tests/ainfer-resourceleak/non-annotated/OwningParams.java diff --git a/checker/build.gradle b/checker/build.gradle index 11a9d86e06f..511e74322cc 100644 --- a/checker/build.gradle +++ b/checker/build.gradle @@ -744,6 +744,14 @@ task ainferResourceLeakGenerateAjava(type: Test) { events 'passed', 'skipped', 'failed' } + // debugOptions { + // enabled = true + // host = 'localhost' + // port = 4455 + // server = true + // suspend = true + // } + doLast { copyNonannotatedToAnnotatedDirectory('ainfer-resourceleak') } 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 0b4d32b3466..35ae46bd3d9 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; @@ -61,6 +62,16 @@ public CalledMethodsTransfer(final CalledMethodsAnalysis analysis) { ((CalledMethodsAnnotatedTypeFactory) atypeFactory).calledMethodsValueElement; } + @Override + protected boolean shouldPerformWholeProgramInference(Tree tree) { + return false; + } + + @Override + protected boolean shouldPerformWholeProgramInference(Tree expressionTree, Tree lhsTree) { + return false; + } + @Override public TransferResult visitMethodInvocation( final MethodInvocationNode node, final TransferInput input) { 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 781bc21e7bd..f69c8832d33 100644 --- a/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallAnnotatedTypeFactory.java @@ -218,6 +218,9 @@ protected void constructorFromUsePreSubstitution( */ private void changeNonOwningParameterTypesToTop( ExecutableElement declaration, AnnotatedExecutableType type) { + if (getWholeProgramInference() != null) { + return; + } List parameterTypes = type.getParameterTypes(); for (int i = 0; i < parameterTypes.size(); i++) { Element paramDecl = declaration.getParameters().get(i); @@ -411,7 +414,13 @@ public MustCallTreeAnnotator(MustCallAnnotatedTypeFactory mustCallAnnotatedTypeF @Override public Void visitIdentifier(IdentifierTree tree, AnnotatedTypeMirror type) { Element elt = TreeUtils.elementFromUse(tree); - if (elt.getKind() == ElementKind.PARAMETER + if (getWholeProgramInference() != null + && elt.getKind() == ElementKind.PARAMETER + && getDeclAnnotation(elt, MustCallAlias.class) != null) { + type.replaceAnnotation(BOTTOM); + } + if (getWholeProgramInference() == null + && elt.getKind() == ElementKind.PARAMETER && (noLightweightOwnership || getDeclAnnotation(elt, Owning.class) == null)) { type.replaceAnnotation(BOTTOM); } 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 2325a84be49..214ac66064e 100644 --- a/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallTransfer.java +++ b/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallTransfer.java @@ -1,9 +1,6 @@ package org.checkerframework.checker.mustcall; -import com.sun.source.tree.ClassTree; -import com.sun.source.tree.ExpressionTree; -import com.sun.source.tree.IdentifierTree; -import com.sun.source.tree.VariableTree; +import com.sun.source.tree.*; import com.sun.source.util.TreePath; import java.util.List; import java.util.concurrent.atomic.AtomicLong; @@ -174,6 +171,16 @@ private void lubWithStoreValue(CFStore store, JavaExpression expr, AnnotationMir store.insertValue(expr, newValue); } + @Override + protected boolean shouldPerformWholeProgramInference(Tree tree) { + return false; + } + + @Override + protected boolean shouldPerformWholeProgramInference(Tree expressionTree, Tree lhsTree) { + return false; + } + @Override public TransferResult visitObjectCreation( ObjectCreationNode node, TransferInput input) { 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 ebe4a847113..8544d0f15e5 100644 --- a/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallVisitor.java @@ -18,10 +18,7 @@ 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; -import org.checkerframework.checker.mustcall.qual.NotOwning; +import org.checkerframework.checker.mustcall.qual.*; import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.common.basetype.BaseTypeVisitor; import org.checkerframework.framework.type.AnnotatedTypeMirror; @@ -189,9 +186,22 @@ 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) { + // 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.hasAnnotation(PolyMustCall.class) + && !AnnotationUtils.containsSameByClass( + elt.getAnnotationMirrors(), PolyMustCall.class); + if (ajavaFileHasMustCallAlias + || AnnotationUtils.containsSameByClass(elt.getAnnotationMirrors(), MustCallAlias.class)) { + 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 a501b1735d9..7ed1d805d56 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java @@ -1021,7 +1021,7 @@ private void updateObligationsForOwningReturn( * @param node a node * @return the temporary for node, or node if no temporary exists */ - private Node getTempVarOrNode(final Node node) { + protected Node getTempVarOrNode(final Node node) { Node temp = typeFactory.getTempVarForNode(node); if (temp != null) { return temp; @@ -1150,7 +1150,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) { + protected boolean isMustCallClose(Node node) { MustCallAnnotatedTypeFactory mcAtf = typeFactory.getTypeFactoryOfSubchecker(MustCallChecker.class); AnnotatedTypeMirror mustCallAnnotatedType = mcAtf.getAnnotatedType(node.getTree()); @@ -1164,7 +1164,8 @@ private boolean isMustCallClose(Node node) { * @param obligations the set of Obligations * @param var a variable */ - private void removeObligationsContainingVar(Set obligations, LocalVariableNode var) { + protected void removeObligationsContainingVar( + Set obligations, LocalVariableNode var) { Obligation obligationForVar = getObligationForVar(obligations, var); while (obligationForVar != null) { obligations.remove(obligationForVar); @@ -1585,7 +1586,7 @@ private Node removeCastsAndGetTmpVarIfPresent(Node node) { * @param node a MethodInvocation or ObjectCreation node * @return the arguments, in order */ - private List getArgumentsOfInvocation(Node node) { + protected List getArgumentsOfInvocation(Node node) { if (node instanceof MethodInvocationNode) { MethodInvocationNode invocationNode = (MethodInvocationNode) node; return invocationNode.getArguments(); @@ -1604,7 +1605,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) { + protected List getParametersOfInvocation(Node node) { ExecutableElement executableElement; if (node instanceof MethodInvocationNode) { MethodInvocationNode invocationNode = (MethodInvocationNode) node; @@ -1987,7 +1988,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( + protected static @Nullable Obligation getObligationForVar( Set obligations, LocalVariableNode node) { for (Obligation obligation : obligations) { if (obligation.canBeSatisfiedThrough(node)) { @@ -2225,7 +2226,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 { + static class BlockWithObligations { /** The block. */ public final Block block; diff --git a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java index 5f073ab6a34..50d3afa1c83 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java @@ -1,25 +1,32 @@ package org.checkerframework.checker.resourceleak; -import java.util.ArrayDeque; -import java.util.ArrayList; -import java.util.Deque; -import java.util.HashSet; -import java.util.List; -import java.util.Set; -import javax.lang.model.element.AnnotationMirror; -import javax.lang.model.element.Element; -import javax.lang.model.element.VariableElement; +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.*; +import javax.lang.model.element.*; +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.Obligation; +import org.checkerframework.checker.resourceleak.MustCallConsistencyAnalyzer.ResourceAlias; 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.MethodInvocationNode; -import org.checkerframework.dataflow.cfg.node.Node; -import org.checkerframework.javacutil.AnnotationBuilder; -import org.checkerframework.javacutil.BugInCF; -import org.checkerframework.javacutil.TreeUtils; +import org.checkerframework.dataflow.cfg.node.*; +import org.checkerframework.dataflow.expression.JavaExpression; +import org.checkerframework.dataflow.expression.LocalVariable; +import org.checkerframework.dataflow.util.NodeUtils; +import org.checkerframework.framework.flow.CFStore; +import org.checkerframework.framework.flow.CFValue; +import org.checkerframework.javacutil.*; /** * This class contains the Resource Leak Checker's annotation inference algorithm. It contains @@ -29,8 +36,8 @@ */ public class MustCallInferenceLogic { - /** The set of owning fields. */ - private final Set owningFields = new HashSet<>(); + /** The set of owning fields that are released within the enMethodElt element. */ + private Set owningFieldToECM = new HashSet<>(); /** * The type factory for the Resource Leak Checker, which is used to access the Must Call Checker. @@ -43,6 +50,15 @@ public class MustCallInferenceLogic { /** The control flow graph. */ private final ControlFlowGraph cfg; + /** TODO */ + private final MustCallConsistencyAnalyzer mcca; + + /** The MethodTree of the cfg. */ + private MethodTree enMethodTree; + + /** The element for the enMethodTree. */ + private ExecutableElement enMethodElt; + /** * Creates a MustCallInferenceLogic. If the type factory has whole program inference enabled, its * postAnalyze method should instantiate a new MustCallInferenceLogic using this constructor and @@ -52,10 +68,15 @@ public class MustCallInferenceLogic { * @param cfg the ControlFlowGraph */ /*package-private*/ MustCallInferenceLogic( - ResourceLeakAnnotatedTypeFactory typeFactory, ControlFlowGraph cfg) { + ResourceLeakAnnotatedTypeFactory typeFactory, + ControlFlowGraph cfg, + MustCallConsistencyAnalyzer mcca) { this.typeFactory = typeFactory; + this.mcca = mcca; this.cfg = cfg; OWNING = AnnotationBuilder.fromClass(this.typeFactory.getElementUtils(), Owning.class); + enMethodTree = ((UnderlyingAST.CFGMethod) cfg.getUnderlyingAST()).getMethod(); + enMethodElt = TreeUtils.elementFromDeclaration(enMethodTree); } /** @@ -63,54 +84,488 @@ public class MustCallInferenceLogic { * *

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 - * must-call obligations were satisfied along one of the checked paths. + * {@link #cfg}, and updates the {@link #owningFieldToECM} set if it discovers an owning field + * whose must-call obligations were satisfied along one of the checked paths. //TODO update the + * document */ /*package-private*/ void runInference() { - Set visited = new HashSet<>(); - Deque worklist = new ArrayDeque<>(); - Block entry = this.cfg.getEntryBlock(); + + 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(); + + Set obligations = new LinkedHashSet<>(current.obligations); - for (Node node : current.getNodes()) { - if (node instanceof MethodInvocationNode) { - checkForMustCallInvocationOnField((MethodInvocationNode) node); + for (Node node : current.block.getNodes()) { + if (node instanceof MethodInvocationNode || node instanceof ObjectCreationNode) { + updateMethodInvocationOrObjectCreationNode(obligations, node); + if (node instanceof MethodInvocationNode) { + checkMethodInvocation(obligations, (MethodInvocationNode) node); + } + } else if (node instanceof AssignmentNode) { + updateObligationsForAssignment(obligations, (AssignmentNode) node); } } - propagateRegPaths(current, visited, worklist); + propagateRegPaths(obligations, current.block, visited, worklist); } } + // TODO add documentation + private Set getNonEmptyMCParams(ControlFlowGraph cfg) { + // TODO what about lambdas? + if (cfg.getUnderlyingAST().getKind() != UnderlyingAST.Kind.METHOD) { + return Collections.emptySet(); + } + Set result = new LinkedHashSet<>(1); + for (VariableTree param : enMethodTree.getParameters()) { + VariableElement paramElement = TreeUtils.elementFromDeclaration(param); + if (typeFactory.declaredTypeHasMustCall(param)) { + result.add( + new Obligation( + ImmutableSet.of(new ResourceAlias(new LocalVariable(paramElement), param)))); + } + } + return result; + } + /** - * 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. + * This function returns a set of all owning fields that have been inferred in the current or + * previous iteration * - * @param mNode the MethodInvocationNode + * @return set of owning fields + */ + private Set getEnclosedOwningFields() { + ClassTree classTree = TreePathUtil.enclosingClass(typeFactory.getPath(enMethodTree)); + TypeElement classElt = TreeUtils.elementFromDeclaration(classTree); + Set enOwningFields = new HashSet<>(); + for (Element memberElt : classElt.getEnclosedElements()) { + if (memberElt.getKind().isField() && typeFactory.hasOwning(memberElt)) { + enOwningFields.add((VariableElement) memberElt); + } + } + for (Element memberElt : owningFieldToECM) { + enOwningFields.add((VariableElement) memberElt); + } + return enOwningFields; + } + + /** + * Given an index, adds an owning annotation to the parameter at the specified index + * + * @param index index of enclosing method's parameter + */ + private void addOwningOnParams(int index) { + WholeProgramInference wpi = typeFactory.getWholeProgramInference(); + wpi.addDeclarationAnnotationToFormalParameter(enMethodElt, index, OWNING); + } + + // TODO + private void isOwningField(@Nullable Node node, MethodInvocationNode mNode) { + if (node == null) { + return; + } + Element nodeElt = TreeUtils.elementFromTree(node.getTree()); + if (nodeElt == null || !nodeElt.getKind().isField()) { + return; + } + if (!getEnclosedOwningFields().contains(nodeElt) + && typeFactory.isCandidateOwningField(nodeElt)) { + node = NodeUtils.removeCasts(node); + JavaExpression target = JavaExpression.fromNode(node); + if (mustCallObligationSatisfied(mNode, nodeElt, target)) { + // This assumes that any MustCall annotation has at most one element. + // TODO: generalize this to MustCall annotations with more than one element. + owningFieldToECM.add((VariableElement) nodeElt); + } + } + } + + // TODO refactor this + private void updateObligationsForAssignment( + 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; + } + + if (lhsElement.getKind() == ElementKind.FIELD) { + if (!getEnclosedOwningFields().contains(lhsElement)) { + return; + } + + if (TreeUtils.isConstructor(enMethodTree)) { + addOwningToParamsIfDisposedAtAssignment(obligations, rhsObligation, rhs); + } else if (!(rhs instanceof NullLiteralNode)) { + if (owningFieldToECM.contains((VariableElement) lhsElement)) { + owningFieldToECM.remove((VariableElement) lhsElement); + } + addOwningToParamsIfDisposedAtAssignment(obligations, rhsObligation, rhs); + } + + } else if (lhsElement.getKind() == ElementKind.RESOURCE_VARIABLE && mcca.isMustCallClose(rhs)) { + if (rhs instanceof LocalVariableNode) { + addOwningToParamsIfDisposedAtAssignment(obligations, rhsObligation, rhs); + } + } else if (lhs instanceof LocalVariableNode) { + LocalVariableNode lhsVar = (LocalVariableNode) lhs; + Obligation lhsObligation = + MustCallConsistencyAnalyzer.getObligationForVar(obligations, lhsVar); + if (lhsObligation == null) { + Set newResourceAliasesForObligation = + new LinkedHashSet<>(rhsObligation.resourceAliases); + newResourceAliasesForObligation.add( + new ResourceAlias(new LocalVariable(lhsVar), lhs.getTree())); + obligations.remove(rhsObligation); + obligations.add(new Obligation(newResourceAliasesForObligation)); + } else { + obligations.remove(rhsObligation); + } + } + } + + private void addOwningToParamsIfDisposedAtAssignment( + Set obligations, Obligation rhsObligation, Node rhs) { + Set rhsAliases = rhsObligation.resourceAliases; + for (ResourceAlias rl : rhsAliases) { + Element rhdElt = rl.reference.getElement(); + List params = enMethodTree.getParameters(); + for (int i = 0; i < params.size(); i++) { + VariableElement paramElt = TreeUtils.elementFromDeclaration(params.get(i)); + if (paramElt.equals(rhdElt)) { + addOwningOnParams(i); + mcca.removeObligationsContainingVar(obligations, (LocalVariableNode) rhs); + break; + } + } + } + } + + /** + * Adds an {@link EnsuresCalledMethods} annotation to the enclosing method for any owning field + * whose must-call obligation is satisfied within the enclosing method. + */ + private void addEnsuresCalledMethods() { + Map> map = new LinkedHashMap<>(); + for (VariableElement owningField : owningFieldToECM) { + List mustCallValues = typeFactory.getMustCallValue(owningField); + assert !mustCallValues.isEmpty() : "Must-call obligation of an owning field is deleted."; + // Assume must-call set has one element + String key = mustCallValues.get(0); + String value = "this." + owningField.getSimpleName().toString(); + + map.computeIfAbsent(key, k -> new HashSet<>()).add(value); + } + + for (String mustCallValue : map.keySet()) { + AnnotationBuilder builder = + new AnnotationBuilder(typeFactory.getProcessingEnv(), EnsuresCalledMethods.class); + builder.setValue("value", map.get(mustCallValue).toArray()); + builder.setValue("methods", new String[] {mustCallValue}); + AnnotationMirror am = builder.build(); + WholeProgramInference wpi = typeFactory.getWholeProgramInference(); + wpi.addMethodDeclarationAnnotation(enMethodElt, am); + } + } + + /** + * Adds the InheritableMustCall annotation on the enclosing class of the current method. If the + * class already has a non-empty MustCall type, if it's inherited from one its superclass, this + * method does nothing. Otherwise, adds the current InheritableMustCall annotation to avoid + * infinite iteration. If the class does not have a MustCall annotation, and the current method is + * not private and satisfies must-call obligation of all the enclosing owning fields, this method + * adds an InheritableMustCall annotation with the current method name to the enclosing class. */ - private void checkForMustCallInvocationOnField(MethodInvocationNode mNode) { + private void addOrUpdateMustCall() { + ClassTree classTree = TreePathUtil.enclosingClass(typeFactory.getPath(enMethodTree)); + TypeElement typeElement = TreeUtils.elementFromDeclaration(classTree); + if (typeElement == null) { + return; + } + + WholeProgramInference wpi = typeFactory.getWholeProgramInference(); + List currentMustCallValues = typeFactory.getMustCallValue(typeElement); + if (!currentMustCallValues.isEmpty()) { + // If the class already has a MustCall annotation which is inherited one from a superclass, + // do nothing + if (typeElement.getSuperclass() != null) { + TypeMirror superType = typeElement.getSuperclass(); + TypeElement superTypeElement = TypesUtils.getTypeElement(superType); + if (superTypeElement != null && !typeFactory.getMustCallValue(superTypeElement).isEmpty()) { + return; + } + } + // add the current @MustCall annotation to guarantee the termination property. This is + // necessary when there are multiple candidates for the must-call obligation. + AnnotationBuilder builder = + new AnnotationBuilder(typeFactory.getProcessingEnv(), InheritableMustCall.class); + String[] methodArray = new String[] {currentMustCallValues.get(0).toString()}; + Arrays.sort(methodArray); + builder.setValue("value", methodArray); + wpi.addClassDeclarationAnnotation(typeElement, builder.build()); + return; + } + + // if the enclosing method is not private and satisfies the must-call obligation of all owning + // fields, add an InheritableMustCall annotation with the current method name + if (!enMethodTree.getModifiers().getFlags().contains(Modifier.PRIVATE)) { + if (!owningFieldToECM.isEmpty() + && owningFieldToECM.size() == getEnclosedOwningFields().size()) { + AnnotationBuilder builder = + new AnnotationBuilder(typeFactory.getProcessingEnv(), InheritableMustCall.class); + String[] methodArray = new String[] {enMethodTree.getName().toString()}; + Arrays.sort(methodArray); + builder.setValue("value", methodArray); + wpi.addClassDeclarationAnnotation(typeElement, builder.build()); + } + } + } + + private void checkArgsOfMethodCall( + Set obligations, + MethodInvocationNode mNode, + List paramsOfEnclosingMethod) { + List arguments = mcca.getArgumentsOfInvocation(mNode); + List parameters = mcca.getParametersOfInvocation(mNode); + if (parameters.isEmpty()) { + return; + } + + // TODO check this again + for (int i = 0; i < arguments.size(); i++) { + Node arg = NodeUtils.removeCasts(arguments.get(i)); + + if (!typeFactory.hasOwning(parameters.get(i))) { + continue; + } + + Set argAliases = getResourceAliasOfArgument(obligations, arg); + for (int j = 0; j < paramsOfEnclosingMethod.size(); j++) { + VariableElement paramElt = TreeUtils.elementFromDeclaration(paramsOfEnclosingMethod.get(j)); + for (ResourceAlias rl : argAliases) { + Element argAliasElt = rl.reference.getElement(); + if (!argAliasElt.equals(paramElt)) { + continue; + } + if (typeFactory.hasOwning(parameters.get(i))) { + addOwningOnParams(j); + break; + } + } + } + } + } + + private void checkReceiverOfMethodCall( + Set obligations, + MethodInvocationNode mNode, + List paramsOfEnclosingMethod) { + Node receiver = mNode.getTarget().getReceiver(); if (receiver.getTree() == null) { return; } Element receiverEl = TreeUtils.elementFromTree(receiver.getTree()); + if (receiverEl != null) { + if (receiverEl.getKind().isField()) { + isOwningField(receiver, mNode); + return; + } + } + + Node receiverTmpVar = mcca.getTempVarOrNode(receiver); + if (!(receiverTmpVar instanceof LocalVariableNode)) { + return; + } + + Obligation receiverObligation = + MustCallConsistencyAnalyzer.getObligationForVar( + obligations, (LocalVariableNode) receiverTmpVar); + if (receiverObligation == null) { + return; + } - if (receiverEl != null && typeFactory.isCandidateOwningField(receiverEl)) { - Element method = TreeUtils.elementFromUse(mNode.getTree()); - List mustCallValues = typeFactory.getMustCallValue(receiverEl); + Set receiverAliases = receiverObligation.resourceAliases; + for (int i = 0; i < paramsOfEnclosingMethod.size(); i++) { + VariableElement paramElt = TreeUtils.elementFromDeclaration(paramsOfEnclosingMethod.get(i)); + + for (ResourceAlias resourceAlias : receiverAliases) { + Element resourceElt = resourceAlias.reference.getElement(); + if (!resourceElt.equals(paramElt)) { + continue; + } + + JavaExpression target = JavaExpression.fromVariableTree(paramsOfEnclosingMethod.get(i)); + if (mustCallObligationSatisfied(mNode, paramElt, target)) { + addOwningOnParams(i); + break; + } + } + } + } + + private void checkIndirectCalls( + Set obligations, + MethodInvocationNode mNode, + List paramsOfEnclosingMethod) { + + List arguments = mcca.getArgumentsOfInvocation(mNode); + List parameters = mcca.getParametersOfInvocation(mNode); + if (parameters.isEmpty()) { + return; + } + + // TODO check this again + for (int i = 0; i < arguments.size(); i++) { + Node arg = NodeUtils.removeCasts(arguments.get(i)); + Element argElt = TreeUtils.elementFromTree(arg.getTree()); + if (argElt == null && arg instanceof ArrayCreationNode) { + ArrayCreationNode arrayCreationNode = (ArrayCreationNode) arg; + List arrays = arrayCreationNode.getInitializers(); + for (Node n : arrays) { + Element nElt = TreeUtils.elementFromTree(n.getTree()); + if (nElt == null) { + continue; + } + if (nElt.getKind().isField()) { + isOwningField(n, mNode); + } + } + } else if (argElt != null && argElt.getKind().isField()) { + isOwningField(arg, mNode); + } + + Set argAliases = getResourceAliasOfArgument(obligations, arg); + for (int j = 0; j < paramsOfEnclosingMethod.size(); j++) { + VariableElement paramElt = TreeUtils.elementFromDeclaration(paramsOfEnclosingMethod.get(i)); + for (ResourceAlias rl : argAliases) { + Element argAliasElt = rl.reference.getElement(); + if (!argAliasElt.equals(paramElt)) { + continue; + } + JavaExpression target = JavaExpression.fromVariableTree(paramsOfEnclosingMethod.get(i)); + if (mustCallObligationSatisfied(mNode, paramElt, target)) { + addOwningOnParams(i); + } + } + } + } + } - // This assumes that any MustCall annotation has at most one element. + private Set getResourceAliasOfArgument(Set obligations, Node arg) { + Node tempVar = mcca.getTempVarOrNode(arg); + if (!(tempVar instanceof LocalVariableNode)) { + return Collections.emptySet(); + } + + Obligation argumentObligation = + MustCallConsistencyAnalyzer.getObligationForVar(obligations, (LocalVariableNode) tempVar); + if (argumentObligation == null) { + return Collections.emptySet(); + } + return argumentObligation.resourceAliases; + } + + /** + * 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 + * #owningFieldToECM} set. + * + * @param mNode the MethodInvocationNode + */ + private void checkMethodInvocation(Set obligations, MethodInvocationNode mNode) { + if (enMethodElt == null) { + return; + } + + List paramsOfEnclosingMethod = enMethodTree.getParameters(); + + checkArgsOfMethodCall(obligations, mNode, paramsOfEnclosingMethod); + checkReceiverOfMethodCall(obligations, mNode, paramsOfEnclosingMethod); + checkIndirectCalls(obligations, mNode, paramsOfEnclosingMethod); + } + + // TODO replace with checkMustCall in mcca + private boolean mustCallObligationSatisfied( + MethodInvocationNode mNode, Element varElt, JavaExpression target) { + + List mustCallValues = typeFactory.getMustCallValue(varElt); + if (mustCallValues.size() != 1) { // TODO: generalize this to MustCall annotations with more than one element. - if (mustCallValues.size() == 1 - && mustCallValues.contains(method.getSimpleName().toString())) { - owningFields.add((VariableElement) receiverEl); + return false; + } + + CFStore cmStoreAfter = typeFactory.getStoreAfter(mNode); + CFValue cmValue = cmStoreAfter == null ? null : cmStoreAfter.getValue(target); + AnnotationMirror cmAnno = null; + if (cmValue != null) { + for (AnnotationMirror anno : cmValue.getAnnotations()) { + if (AnnotationUtils.areSameByName( + anno, "org.checkerframework.checker.calledmethods.qual.CalledMethods")) { + cmAnno = anno; + break; + } + } + } + + if (cmAnno == null) { + cmAnno = typeFactory.top; + } + + AnnotationMirror cmAnnoForMustCallMethods = + typeFactory.createCalledMethods(mustCallValues.toArray(new String[0])); + if (!mustCallValues.isEmpty() + && typeFactory.getQualifierHierarchy().isSubtype(cmAnno, cmAnnoForMustCallMethods)) { + return true; + } + return false; + } + + // probably replace with updateObligationsWithInvocationResult in mcca TODO + private void updateMethodInvocationOrObjectCreationNode(Set obligations, Node node) { + List arguments = mcca.getArgumentsOfInvocation(node); + List parameters = mcca.getParametersOfInvocation(node); + + for (int i = 0; i < arguments.size(); i++) { + Node tempVar = mcca.getTempVarOrNode(arguments.get(i)); + if (!(tempVar instanceof LocalVariableNode)) { + continue; + } + + Obligation obligation = + MustCallConsistencyAnalyzer.getObligationForVar(obligations, (LocalVariableNode) tempVar); + if (obligation == null) { + continue; + } + + Node method = mcca.getTempVarOrNode(node); + if (typeFactory.hasMustCallAlias(parameters.get(i))) { + Set newResourceAliasesForObligation = + new LinkedHashSet<>(obligation.resourceAliases); + newResourceAliasesForObligation.add( + new ResourceAlias(new LocalVariable((LocalVariableNode) method), node.getTree())); + obligations.remove(obligation); + obligations.add(new Obligation(newResourceAliasesForObligation)); } } } @@ -118,29 +573,39 @@ private void checkForMustCallInvocationOnField(MethodInvocationNode mNode) { /** * 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}. + * #owningFieldToECM}. * * @param curBlock the current block * @param visited set of blocks already on the worklist * @param worklist current worklist */ - private void propagateRegPaths(Block curBlock, Set visited, Deque worklist) { + private void propagateRegPaths( + Set obligations, + Block curBlock, + Set visited, + Deque worklist) { List successors = getNormalSuccessors(curBlock); - for (Block b : successors) { + for (Block successor : 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) { + if (successor.getType() == Block.BlockType.SPECIAL_BLOCK) { WholeProgramInference wpi = typeFactory.getWholeProgramInference(); + assert wpi != null : "MustCallInference is running without WPI."; - for (VariableElement fieldElt : owningFields) { + for (VariableElement fieldElt : getEnclosedOwningFields()) { wpi.addFieldDeclarationAnnotation(fieldElt, OWNING); } - } + if (!owningFieldToECM.isEmpty()) { + addEnsuresCalledMethods(); + } - if (visited.add(b)) { - worklist.add(b); + addOrUpdateMustCall(); + } + BlockWithObligations state = new BlockWithObligations(successor, obligations); + if (visited.add(state)) { + worklist.add(state); } } } 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 7d11f449170..2dbde763f93 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; @@ -110,9 +109,7 @@ public ResourceLeakAnnotatedTypeFactory(final BaseTypeChecker checker) { * @return true iff the given element is a final field with non-empty @MustCall obligation */ /*package-private*/ boolean isCandidateOwningField(Element element) { - return (element.getKind().isField() - && ElementUtils.isFinal(element) - && !getMustCallValue(element).isEmpty()); + return (element.getKind().isField() && !getMustCallValue(element).isEmpty()); } @Override @@ -140,7 +137,8 @@ public void postAnalyze(ControlFlowGraph cfg) { // Inferring owning annotations for final owning fields if (getWholeProgramInference() != null) { if (cfg.getUnderlyingAST().getKind() == UnderlyingAST.Kind.METHOD) { - MustCallInferenceLogic mustCallInferenceLogic = new MustCallInferenceLogic(this, cfg); + MustCallInferenceLogic mustCallInferenceLogic = + new MustCallInferenceLogic(this, cfg, mustCallConsistencyAnalyzer); mustCallInferenceLogic.runInference(); } } 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 68bc02adff1..4c77ae6c72e 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakVisitor.java @@ -142,6 +142,12 @@ private void checkCreatesMustCallForOverrides( } } + @Override + protected boolean shouldPerformContractInference() { + // TODO: should be "false whenever running MustCallInferenceLogic", probably + return false; + } + // 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 @@ -335,7 +341,7 @@ private void checkOwningField(Element field) { if (siblingElement.getKind() == ElementKind.METHOD && enclosingMustCallValues.contains(siblingElement.getSimpleName().toString())) { AnnotationMirror ensuresCalledMethodsAnno = - rlTypeFactory.getDeclAnnotation(siblingElement, EnsuresCalledMethods.class); + getEnsuresCalledMethodsForField(siblingElement, field); if (ensuresCalledMethodsAnno != null) { List values = @@ -381,4 +387,21 @@ private void checkOwningField(Element field) { error); } } + + private AnnotationMirror getEnsuresCalledMethodsForField(Element methodElt, Element field) { + AnnotationMirrorSet declAnnos = rlTypeFactory.getDeclAnnotations(methodElt); + for (AnnotationMirror am : declAnnos) { + if (rlTypeFactory.areSameByClass(am, EnsuresCalledMethods.class)) { + List values = + AnnotationUtils.getElementValueArray( + am, rlTypeFactory.ensuresCalledMethodsValueElement, String.class); + for (String value : values) { + if (value.contains(field.getSimpleName().toString())) { + return am; + } + } + } + } + return null; + } } 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..08e7d2bc2fa --- /dev/null +++ b/checker/tests/ainfer-resourceleak/non-annotated/EnsuresCalledMethodsTest.java @@ -0,0 +1,41 @@ +import org.checkerframework.checker.calledmethods.qual.*; +import org.checkerframework.checker.mustcall.qual.*; + +class EnsuresCalledMethodsTest { + @InheritableMustCall("a") + static class Foo { + void a() {} + } + + private class ECM { + Foo foo; + + // private ECM() { + // foo = new Foo(); + // } + + private void closePrivate() { + if (foo != null) { + foo.a(); + foo = null; + } + } + + void close() { + if (foo != null) { + foo.a(); + foo = null; + } + } + } + + // void testECM() { + // ECM e = new ECM(); + // e.close(); + // } + // + // void testECMWrong() { + // // :: warning: (required.method.not.called) + // ECM e = new ECM(); + // } +} 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..eb6fc448817 --- /dev/null +++ b/checker/tests/ainfer-resourceleak/non-annotated/EnsuresCalledMethodsVarArgsTest.java @@ -0,0 +1,49 @@ +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 fff; + + ECMVA() { + // :: warning: (required.method.not.called) + fff = new Foo(); + } + + void finalyzer() { + Utils.close(fff); + } + + @EnsuresCalledMethods( + value = {"#1"}, + methods = {"a"}) + void closef(Foo f) { + if (f != null) { + Utils.close(f); + } + } + } + + void testCorrect() { + ECMVA e = new ECMVA(); + e.finalyzer(); + } +} 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..b65aff7e25a --- /dev/null +++ b/checker/tests/ainfer-resourceleak/non-annotated/OwningParams.java @@ -0,0 +1,47 @@ +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 f111, Foo f2) { + hasECM(f111); + owningFoo(f2); + } + + 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/framework/src/main/java/org/checkerframework/common/accumulation/AccumulationTransfer.java b/framework/src/main/java/org/checkerframework/common/accumulation/AccumulationTransfer.java index 005e5462574..92ab9b64db7 100644 --- a/framework/src/main/java/org/checkerframework/common/accumulation/AccumulationTransfer.java +++ b/framework/src/main/java/org/checkerframework/common/accumulation/AccumulationTransfer.java @@ -22,7 +22,7 @@ *

Subclasses should call the {@link #accumulate(Node, TransferResult, String...)} accumulate} * method to add a string to the estimate at a particular program point. */ -public class AccumulationTransfer extends CFTransfer { +public abstract class AccumulationTransfer extends CFTransfer { /** The type factory. */ protected final AccumulationAnnotatedTypeFactory atypeFactory; 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 487ccea413d..4153781a146 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -980,7 +980,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. @@ -1002,6 +1002,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 e68b242b4e5..92ec6666117 100644 --- a/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceJavaParserStorage.java +++ b/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceJavaParserStorage.java @@ -756,21 +756,24 @@ private void addClass( ClassTree tree, @Nullable @BinaryName String classNameKey, @Nullable TypeDeclaration javaParserNode) { - String className; + String className = null; if (classNameKey == null) { TypeElement classElt = TreeUtils.elementFromDeclaration(tree); - className = ElementUtils.getBinaryName(classElt); - - for (TypeElement supertypeElement : ElementUtils.getSuperTypes(classElt, elements)) { - String supertypeName = ElementUtils.getBinaryName(supertypeElement); - @SuppressWarnings({"signature:assignment", "signature:return"}) // #979? - Set supertypeSet = - supertypesMap.computeIfAbsent(className, k -> new TreeSet<>()); - supertypeSet.add(supertypeName); - @SuppressWarnings({"signature:assignment", "signature:return"}) // #979? - Set subtypeSet = - subtypesMap.computeIfAbsent(supertypeName, k -> new TreeSet<>()); - subtypeSet.add(className); + if (classElt != null) { + className = ElementUtils.getBinaryName(classElt); + + for (TypeElement supertypeElement : + ElementUtils.getSuperTypes(classElt, elements)) { + String supertypeName = ElementUtils.getBinaryName(supertypeElement); + @SuppressWarnings({"signature:assignment", "signature:return"}) // #979? + Set supertypeSet = + supertypesMap.computeIfAbsent(className, k -> new TreeSet<>()); + supertypeSet.add(supertypeName); + @SuppressWarnings({"signature:assignment", "signature:return"}) // #979? + Set subtypeSet = + subtypesMap.computeIfAbsent(supertypeName, k -> new TreeSet<>()); + subtypeSet.add(className); + } } } else { className = classNameKey; @@ -1911,10 +1914,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 76bd227086b..f482bde4b50 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java @@ -998,7 +998,7 @@ public TransferResult visitInstanceOf(InstanceOfNode node, TransferInput Date: Mon, 15 May 2023 10:40:52 -0700 Subject: [PATCH 002/132] Undo wildcard imports --- .../checker/mustcall/MustCallTransfer.java | 6 +++- .../checker/mustcall/MustCallVisitor.java | 6 +++- .../resourceleak/MustCallInferenceLogic.java | 34 ++++++++++++++++--- 3 files changed, 40 insertions(+), 6 deletions(-) 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 214ac66064e..7a615302599 100644 --- a/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallTransfer.java +++ b/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallTransfer.java @@ -1,6 +1,10 @@ package org.checkerframework.checker.mustcall; -import com.sun.source.tree.*; +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; import java.util.concurrent.atomic.AtomicLong; 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 8544d0f15e5..86f29333bdf 100644 --- a/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallVisitor.java @@ -18,7 +18,11 @@ 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.*; +import org.checkerframework.checker.mustcall.qual.InheritableMustCall; +import org.checkerframework.checker.mustcall.qual.MustCall; +import org.checkerframework.checker.mustcall.qual.MustCallAlias; +import org.checkerframework.checker.mustcall.qual.NotOwning; +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; diff --git a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java index 58d562c3507..96da2316b0a 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java @@ -4,8 +4,24 @@ import com.sun.source.tree.ClassTree; import com.sun.source.tree.MethodTree; import com.sun.source.tree.VariableTree; -import java.util.*; -import javax.lang.model.element.*; +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; @@ -20,13 +36,23 @@ 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.*; +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.framework.flow.CFStore; import org.checkerframework.framework.flow.CFValue; -import org.checkerframework.javacutil.*; +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; /** * This class contains the Resource Leak Checker's annotation inference algorithm. It contains From 833231fba28135f8946c35274f5e79679c808b42 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Tue, 16 May 2023 09:18:28 -0700 Subject: [PATCH 003/132] Put shorter clauses first --- .../WholeProgramInferenceJavaParserStorage.java | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) 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 e84027a0d55..14033fd2c72 100644 --- a/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceJavaParserStorage.java +++ b/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceJavaParserStorage.java @@ -756,10 +756,14 @@ private void addClass( ClassTree tree, @Nullable @BinaryName String classNameKey, @Nullable TypeDeclaration javaParserNode) { - String className = null; - if (classNameKey == null) { + String className; + if (classNameKey != null) { + className = classNameKey; + } else { TypeElement classElt = TreeUtils.elementFromDeclaration(tree); - if (classElt != null) { + if (classElt == null) { + className = null; + } else { className = ElementUtils.getBinaryName(classElt); for (TypeElement supertypeElement : @@ -775,8 +779,6 @@ private void addClass( subtypeSet.add(className); } } - } else { - className = classNameKey; } ClassOrInterfaceAnnos typeWrapper = new ClassOrInterfaceAnnos(className, javaParserNode); From 22af6f63d38f2f1f3b02bdc0012bdfd6756bc429 Mon Sep 17 00:00:00 2001 From: Nargeshdb Date: Mon, 22 May 2023 13:20:16 -0700 Subject: [PATCH 004/132] address comments --- checker/build.gradle | 8 +++++ .../calledmethods/CalledMethodsTransfer.java | 35 +++++++++++++++++-- .../MustCallAnnotatedTypeFactory.java | 4 +++ .../resourceleak/MustCallInferenceLogic.java | 4 +-- ...holeProgramInferenceJavaParserStorage.java | 35 +++++++++---------- .../framework/flow/CFAbstractTransfer.java | 12 +++++++ 6 files changed, 76 insertions(+), 22 deletions(-) diff --git a/checker/build.gradle b/checker/build.gradle index 11a9d86e06f..511e74322cc 100644 --- a/checker/build.gradle +++ b/checker/build.gradle @@ -744,6 +744,14 @@ task ainferResourceLeakGenerateAjava(type: Test) { events 'passed', 'skipped', 'failed' } + // debugOptions { + // enabled = true + // host = 'localhost' + // port = 4455 + // server = true + // suspend = true + // } + doLast { copyNonannotatedToAnnotatedDirectory('ainfer-resourceleak') } 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 35ae46bd3d9..74c270371f0 100644 --- a/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsTransfer.java +++ b/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsTransfer.java @@ -62,14 +62,45 @@ public CalledMethodsTransfer(final CalledMethodsAnalysis analysis) { ((CalledMethodsAnnotatedTypeFactory) atypeFactory).calledMethodsValueElement; } + /** + * The Called Methods Checker is one of the sub-checkers of the Resource Leak Checker. When we + * enable -Ainfer for the Resource Leak Checker, whole-program inference (wpi) is performed for + * all the sub-checkers. However, our mechanism for inferring annotations for the resource leak + * checker is different. It relies on pattern matching instead. The wpi results for this inference + * are not useful and only end up slowing down the convergence of the algorithm for Resource Leak + * Inference. + * + * @param tree a tree + * @return false if Resource Leak Checker is running as one of the upstream checkers, otherwise + * returns the result of the super call + */ @Override protected boolean shouldPerformWholeProgramInference(Tree tree) { - return false; + if (isResourceLeakCheckerEnabled()) { + return false; + } + return super.shouldPerformWholeProgramInference(tree); } + /** + * The Called Methods Checker is one of the sub-checkers of the Resource Leak Checker. When we + * enable -Ainfer for the Resource Leak Checker, whole-program inference (wpi) is performed for + * all the sub-checkers. However, our mechanism for inferring annotations for the resource leak + * checker is different. It relies on pattern matching instead. The wpi results for this inference + * are not useful and only end up slowing down the convergence of the algorithm for Resource Leak + * Inference. + * + * @param expressionTree a tree + * @param lhsTree its element + * @return false if Resource Leak Checker is running as one of the upstream checkers, otherwise + * returns the result of the super call + */ @Override protected boolean shouldPerformWholeProgramInference(Tree expressionTree, Tree lhsTree) { - return false; + if (isResourceLeakCheckerEnabled()) { + return false; + } + return super.shouldPerformWholeProgramInference(expressionTree, lhsTree); } @Override 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 f69c8832d33..1fbf22e6fa4 100644 --- a/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallAnnotatedTypeFactory.java @@ -218,6 +218,10 @@ 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 the goal is to infer and add + // @Owning annotations to owning parameters. if (getWholeProgramInference() != null) { return; } diff --git a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java index 96da2316b0a..2f754d14e97 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java @@ -535,13 +535,13 @@ private void checkIndirectCalls( Set argAliases = getResourceAliasOfArgument(obligations, arg); for (int j = 0; j < paramsOfEnclosingMethod.size(); j++) { - VariableElement paramElt = TreeUtils.elementFromDeclaration(paramsOfEnclosingMethod.get(i)); + VariableElement paramElt = TreeUtils.elementFromDeclaration(paramsOfEnclosingMethod.get(j)); for (ResourceAlias rl : argAliases) { Element argAliasElt = rl.reference.getElement(); if (!argAliasElt.equals(paramElt)) { continue; } - JavaExpression target = JavaExpression.fromVariableTree(paramsOfEnclosingMethod.get(i)); + JavaExpression target = JavaExpression.fromVariableTree(paramsOfEnclosingMethod.get(j)); if (mustCallObligationSatisfied(mNode, paramElt, target)) { addOwningOnParams(i); } 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 14033fd2c72..902563d53ab 100644 --- a/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceJavaParserStorage.java +++ b/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceJavaParserStorage.java @@ -761,24 +761,23 @@ private void addClass( className = classNameKey; } else { TypeElement classElt = TreeUtils.elementFromDeclaration(tree); - if (classElt == null) { - className = null; - } else { - className = ElementUtils.getBinaryName(classElt); - - for (TypeElement supertypeElement : - ElementUtils.getSuperTypes(classElt, elements)) { - String supertypeName = ElementUtils.getBinaryName(supertypeElement); - @SuppressWarnings({"signature:assignment", "signature:return"}) // #979? - Set supertypeSet = - supertypesMap.computeIfAbsent(className, k -> new TreeSet<>()); - supertypeSet.add(supertypeName); - @SuppressWarnings({"signature:assignment", "signature:return"}) // #979? - Set subtypeSet = - subtypesMap.computeIfAbsent(supertypeName, k -> new TreeSet<>()); - subtypeSet.add(className); - } + // if (classElt == null) { + // className = null; + // } else { + className = ElementUtils.getBinaryName(classElt); + + for (TypeElement supertypeElement : ElementUtils.getSuperTypes(classElt, elements)) { + String supertypeName = ElementUtils.getBinaryName(supertypeElement); + @SuppressWarnings({"signature:assignment", "signature:return"}) // #979? + Set supertypeSet = + supertypesMap.computeIfAbsent(className, k -> new TreeSet<>()); + supertypeSet.add(supertypeName); + @SuppressWarnings({"signature:assignment", "signature:return"}) // #979? + Set subtypeSet = + subtypesMap.computeIfAbsent(supertypeName, k -> new TreeSet<>()); + subtypeSet.add(className); } + // } } ClassOrInterfaceAnnos typeWrapper = new ClassOrInterfaceAnnos(className, javaParserNode); @@ -1044,7 +1043,7 @@ public void writeResultsToFile(OutputFormat outputFormat, BaseTypeChecker checke for (String path : modifiedFiles) { // This calls deepCopy() because wpiPrepareCompilationUnitForWriting performs side effects // that we don't want to be persistent. - CompilationUnitAnnos root = sourceToAnnos.get(path); + CompilationUnitAnnos root = sourceToAnnos.get(path).deepCopy(); wpiPrepareCompilationUnitForWriting(root); File packageDir; if (!root.compilationUnit.getPackageDeclaration().isPresent()) { 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 f482bde4b50..848a5283560 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java @@ -113,6 +113,9 @@ public abstract class CFAbstractTransfer< /** Indicates that the whole-program inference is on. */ private final boolean infer; + /** Indicates that the resource leak checker is enabled. */ + private final boolean resourceLeakChecker; + /** * Create a CFAbstractTransfer. * @@ -136,6 +139,11 @@ protected CFAbstractTransfer( this.analysis = analysis; this.sequentialSemantics = !(forceConcurrentSemantics || analysis.checker.hasOption("concurrentSemantics")); + this.resourceLeakChecker = + analysis + .checker + .getUpstreamCheckerNames() + .contains("org.checkerframework.checker.resourceleak.ResourceLeakChecker"); this.infer = analysis.checker.hasOption("infer"); } @@ -991,6 +999,10 @@ public TransferResult visitInstanceOf(InstanceOfNode node, TransferInput Date: Tue, 23 May 2023 19:27:34 -0700 Subject: [PATCH 005/132] address feedbacks --- .../checker/resourceleak/MustCallInferenceLogic.java | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java index 2f754d14e97..7f049071b8c 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java @@ -76,7 +76,6 @@ public class MustCallInferenceLogic { /** The control flow graph. */ private final ControlFlowGraph cfg; - /** TODO */ private final MustCallConsistencyAnalyzer mcca; /** The MethodTree of the cfg. */ @@ -91,7 +90,7 @@ public class MustCallInferenceLogic { * then call {@link #runInference()}. * * @param typeFactory the type factory - * @param cfg the ControlFlowGraph + * @param cfg the control flow graph of the method to check */ /*package-private*/ MustCallInferenceLogic( ResourceLeakAnnotatedTypeFactory typeFactory, @@ -690,10 +689,10 @@ private void propagateRegPaths( List successors = getNormalSuccessors(curBlock); - for (Block successor : successors) { + 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 (successor.getType() == Block.BlockType.SPECIAL_BLOCK) { + if (b.getType() == Block.BlockType.SPECIAL_BLOCK) { WholeProgramInference wpi = typeFactory.getWholeProgramInference(); assert wpi != null : "MustCallInference is running without WPI."; @@ -706,7 +705,7 @@ private void propagateRegPaths( addOrUpdateMustCall(); } - BlockWithObligations state = new BlockWithObligations(successor, obligations); + BlockWithObligations state = new BlockWithObligations(b, obligations); if (visited.add(state)) { worklist.add(state); } From ef2ac880977f8b0c92fd0902303360fb80fa0d43 Mon Sep 17 00:00:00 2001 From: Nargeshdb Date: Wed, 24 May 2023 12:08:11 -0700 Subject: [PATCH 006/132] update shouldPerformWholeProgramInference in MustCallTransfer --- .../checker/mustcall/MustCallTransfer.java | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) 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 7a615302599..25b2f3da6dc 100644 --- a/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallTransfer.java +++ b/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallTransfer.java @@ -177,12 +177,18 @@ private void lubWithStoreValue(CFStore store, JavaExpression expr, AnnotationMir @Override protected boolean shouldPerformWholeProgramInference(Tree tree) { - return false; + if (isResourceLeakCheckerEnabled()) { + return false; + } + return super.shouldPerformWholeProgramInference(tree); } @Override protected boolean shouldPerformWholeProgramInference(Tree expressionTree, Tree lhsTree) { - return false; + if (isResourceLeakCheckerEnabled()) { + return false; + } + return super.shouldPerformWholeProgramInference(expressionTree, lhsTree); } @Override From 617a7c71022f15a101930f753ea57291bc633a9e Mon Sep 17 00:00:00 2001 From: Nargeshdb Date: Thu, 25 May 2023 10:05:52 -0700 Subject: [PATCH 007/132] add comments --- .../checker/resourceleak/MustCallInferenceLogic.java | 4 ++++ .../resourceleak/ResourceLeakAnnotatedTypeFactory.java | 3 ++- .../checkerframework/framework/flow/CFAbstractTransfer.java | 5 +++++ 3 files changed, 11 insertions(+), 1 deletion(-) diff --git a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java index 7f049071b8c..f756487a759 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java @@ -76,6 +76,7 @@ public class MustCallInferenceLogic { /** The control flow graph. */ private final ControlFlowGraph cfg; + /** The MustCallConsistencyAnalyzer. */ private final MustCallConsistencyAnalyzer mcca; /** The MethodTree of the cfg. */ @@ -91,6 +92,7 @@ public class MustCallInferenceLogic { * * @param typeFactory the type factory * @param cfg the control flow graph of the method to check + * @param mcca the MustCallConsistencyAnalyzer */ /*package-private*/ MustCallInferenceLogic( ResourceLeakAnnotatedTypeFactory typeFactory, @@ -577,6 +579,7 @@ private Set getResourceAliasOfArgument(Set obligation * satisfies the field's must-call obligation, then adds that field to the {@link * #owningFieldToECM} set. * + * @param obligations the set of obligations to search in * @param mNode the MethodInvocationNode */ private void checkMethodInvocation(Set obligations, MethodInvocationNode mNode) { @@ -677,6 +680,7 @@ private void updateMethodInvocationOrObjectCreationNode(Set obligati * next block is a regular exit point, adds an {@literal @}Owning annotation for fields in {@link * #owningFieldToECM}. * + * @param obligations the set of obligations to update * @param curBlock the current block * @param visited set of blocks already on the worklist * @param worklist current worklist 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 4c57186e04e..35ebf7bfa61 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakAnnotatedTypeFactory.java @@ -134,7 +134,8 @@ 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) { MustCallInferenceLogic mustCallInferenceLogic = 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 45c921b6df0..6b4234d33d2 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java @@ -999,6 +999,11 @@ public TransferResult visitInstanceOf(InstanceOfNode node, TransferInput Date: Thu, 15 Jun 2023 17:16:49 -0700 Subject: [PATCH 008/132] update --- .../checker/calledmethods/CalledMethodsChecker.java | 2 ++ .../checker/calledmethods/CalledMethodsTransfer.java | 12 ++++++------ .../checker/resourceleak/MustCallInferenceLogic.java | 9 +++++---- 3 files changed, 13 insertions(+), 10 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsChecker.java b/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsChecker.java index bc66ba1edc5..e8cd586d7c2 100644 --- a/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsChecker.java +++ b/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsChecker.java @@ -67,6 +67,8 @@ public class CalledMethodsChecker extends AccumulationChecker { /** Never access this boolean directly. Call {@link #isReturnsReceiverDisabled()} instead. */ private @MonotonicNonNull Boolean returnsReceiverDisabled = null; + // public static final String RESOURCE_LEAK_INFERENCE_PATTERN_M + /** * Was the Returns Receiver Checker disabled on the command line? * 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 ecc010b5590..edffe6c8bcb 100644 --- a/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsTransfer.java +++ b/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsTransfer.java @@ -83,12 +83,12 @@ protected boolean shouldPerformWholeProgramInference(Tree tree) { } /** - * The Called Methods Checker is one of the sub-checkers of the Resource Leak Checker. When we - * enable -Ainfer for the Resource Leak Checker, whole-program inference (wpi) is performed for - * all the sub-checkers. However, our mechanism for inferring annotations for the resource leak - * checker is different. It relies on pattern matching instead. The wpi results for this inference - * are not useful and only end up slowing down the convergence of the algorithm for Resource Leak - * Inference. + * The Called Methods Checker is one of the sub-checkers of the Resource Leak Checker. When + * -Ainfer flag is enabled for the Resource Leak Checker, whole-program inference (wpi) is + * performed for all the sub-checkers. However, the mechanism for inferring annotations for the + * resource leak checker is different. It relies on pattern matching instead. The wpi results for + * this inference are not useful and only end up slowing down the convergence of the algorithm for + * Resource Leak Inference. * * @param expressionTree a tree * @param lhsTree its element diff --git a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java index f756487a759..0e2e97a1c70 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java @@ -30,6 +30,8 @@ import org.checkerframework.checker.resourceleak.MustCallConsistencyAnalyzer.BlockWithObligations; 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; @@ -45,8 +47,6 @@ import org.checkerframework.dataflow.expression.JavaExpression; import org.checkerframework.dataflow.expression.LocalVariable; import org.checkerframework.dataflow.util.NodeUtils; -import org.checkerframework.framework.flow.CFStore; -import org.checkerframework.framework.flow.CFValue; import org.checkerframework.javacutil.AnnotationBuilder; import org.checkerframework.javacutil.AnnotationUtils; import org.checkerframework.javacutil.BugInCF; @@ -614,8 +614,9 @@ private boolean mustCallObligationSatisfied( return false; } - CFStore cmStoreAfter = typeFactory.getStoreAfter(mNode); - CFValue cmValue = cmStoreAfter == null ? null : cmStoreAfter.getValue(target); + AccumulationStore cmStoreAfter = typeFactory.getStoreAfter(mNode); + @Nullable AccumulationValue cmValue = + cmStoreAfter == null ? null : cmStoreAfter.getValue(target); AnnotationMirror cmAnno = null; if (cmValue != null) { for (AnnotationMirror anno : cmValue.getAnnotations()) { From 2e87329edefa151e88e92a772e39a73bd402cc5c Mon Sep 17 00:00:00 2001 From: Nargeshdb Date: Thu, 22 Jun 2023 13:02:38 -0700 Subject: [PATCH 009/132] update comments --- .../resourceleak/MustCallInferenceLogic.java | 41 +++++++++++-------- .../EnsuresCalledMethodsTest.java | 14 ------- 2 files changed, 23 insertions(+), 32 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java index 0e2e97a1c70..041933ec20a 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java @@ -55,15 +55,21 @@ import org.checkerframework.javacutil.TypesUtils; /** - * 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 is + * responsible for inferring annotations such as @Owning on owning fields and + * parameters, @EnsuresCalledMethods on methods, and @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 + * fulfilled 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 by this instance. Additionally, if the current method being analyzed + * fulfills the must-call obligation of all the enclosed owning fields, it adds + * a @InheritableMustCall annotation on the enclosing class. */ public class MustCallInferenceLogic { - /** The set of owning fields that are released within the enMethodElt element. */ - private Set owningFieldToECM = new HashSet<>(); + /** The set of owning fields that are released within the CFG currently under analysis. */ + private final Set owningFieldToECM = new HashSet<>(); /** * The type factory for the Resource Leak Checker, which is used to access the Must Call Checker. @@ -151,7 +157,7 @@ public class MustCallInferenceLogic { * Returns a set of obligations representing the non-empty MustCall parameters of the current * method. * - * @param cfg the ControlFlowGraph for the current method + * @param cfg the control flow graph of the method to check * @return a set of obligations representing the non-empty MustCall parameters of the current * method */ @@ -207,7 +213,7 @@ private void addOwningOnParams(int index) { * Checks if the given node is a field and if it is a new Owning field. * * @param node the possible owning field - * @param mNode method invocation node + * @param mNode method invoked on the possible owning field */ private void isOwningField(@Nullable Node node, MethodInvocationNode mNode) { if (node == null) { @@ -291,8 +297,8 @@ private void updateObligationsForAssignment( } /** - * Adds owning fields to the method's parameters, if its alias referred to by the right-hand side - * of the assignment is disposed of during the assignment. + * Adds owning fields to the method's parameters, if the must-call obligation of its alias + * referred to by the right-hand side of the assignment is fulfilled during the assignment. * * @param obligations The set of obligations to update. * @param rhsObligation The obligation associated with the right-hand side of the assignment. @@ -343,12 +349,11 @@ private void addEnsuresCalledMethods() { } /** - * Adds the InheritableMustCall annotation on the enclosing class of the current method. If the - * class already has a non-empty MustCall type, if it's inherited from one its superclass, this - * method does nothing. Otherwise, adds the current InheritableMustCall annotation to avoid - * infinite iteration. If the class does not have a MustCall annotation, and the current method is - * not private and satisfies must-call obligation of all the enclosing owning fields, this method - * adds an InheritableMustCall annotation with the current method name to the enclosing class. + * Adds an InheritableMustCall annotation on the enclosing class. If the class already has a + * non-empty MustCall type, if it's inherited from one of its superclasses, this method does + * nothing to avoid infinite iteration. Otherwise, if the method being analyzed by {@code this} is + * not private and satisfies must-call obligation of all the enclosed owning fields, it adds an + * InheritableMustCall annotation to the enclosing class. */ private void addOrUpdateMustCall() { ClassTree classTree = TreePathUtil.enclosingClass(typeFactory.getPath(enMethodTree)); @@ -381,7 +386,7 @@ private void addOrUpdateMustCall() { } // if the enclosing method is not private and satisfies the must-call obligation of all owning - // fields, add an InheritableMustCall annotation with the current method name + // fields, add an InheritableMustCall annotation with the name of this method if (!enMethodTree.getModifiers().getFlags().contains(Modifier.PRIVATE)) { if (!owningFieldToECM.isEmpty() && owningFieldToECM.size() == getEnclosedOwningFields().size()) { @@ -695,7 +700,7 @@ private void propagateRegPaths( List successors = getNormalSuccessors(curBlock); for (Block b : successors) { - // If b is a special block, it must be the regular exit, since we do not propagate to + // If b is a special block, it must be the regular exit, since it does not propagate to // exceptional successors. if (b.getType() == Block.BlockType.SPECIAL_BLOCK) { WholeProgramInference wpi = typeFactory.getWholeProgramInference(); diff --git a/checker/tests/ainfer-resourceleak/non-annotated/EnsuresCalledMethodsTest.java b/checker/tests/ainfer-resourceleak/non-annotated/EnsuresCalledMethodsTest.java index 08e7d2bc2fa..1b877b2e2d1 100644 --- a/checker/tests/ainfer-resourceleak/non-annotated/EnsuresCalledMethodsTest.java +++ b/checker/tests/ainfer-resourceleak/non-annotated/EnsuresCalledMethodsTest.java @@ -10,10 +10,6 @@ void a() {} private class ECM { Foo foo; - // private ECM() { - // foo = new Foo(); - // } - private void closePrivate() { if (foo != null) { foo.a(); @@ -28,14 +24,4 @@ void close() { } } } - - // void testECM() { - // ECM e = new ECM(); - // e.close(); - // } - // - // void testECMWrong() { - // // :: warning: (required.method.not.called) - // ECM e = new ECM(); - // } } From aae7e30fe7a26c2ad78851b98f6ae0d458a33383 Mon Sep 17 00:00:00 2001 From: Narges Shadab Date: Mon, 26 Jun 2023 09:43:22 -0700 Subject: [PATCH 010/132] address Martin's feedback --- .../calledmethods/CalledMethodsChecker.java | 2 - .../calledmethods/CalledMethodsTransfer.java | 4 +- .../checker/mustcall/MustCallTransfer.java | 4 +- .../MustCallConsistencyAnalyzer.java | 4 +- .../resourceleak/MustCallInferenceLogic.java | 50 +------------------ .../resourceleak/ResourceLeakChecker.java | 1 + .../resourceleak/ResourceLeakVisitor.java | 6 +++ .../non-annotated/ECMInference.java | 1 + .../framework/flow/CFAbstractTransfer.java | 12 ++--- 9 files changed, 20 insertions(+), 64 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsChecker.java b/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsChecker.java index e8cd586d7c2..bc66ba1edc5 100644 --- a/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsChecker.java +++ b/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsChecker.java @@ -67,8 +67,6 @@ public class CalledMethodsChecker extends AccumulationChecker { /** Never access this boolean directly. Call {@link #isReturnsReceiverDisabled()} instead. */ private @MonotonicNonNull Boolean returnsReceiverDisabled = null; - // public static final String RESOURCE_LEAK_INFERENCE_PATTERN_M - /** * Was the Returns Receiver Checker disabled on the command line? * 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 edffe6c8bcb..913d1d3d8b6 100644 --- a/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsTransfer.java +++ b/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsTransfer.java @@ -76,7 +76,7 @@ public CalledMethodsTransfer(CalledMethodsAnalysis analysis) { */ @Override protected boolean shouldPerformWholeProgramInference(Tree tree) { - if (isResourceLeakCheckerEnabled()) { + if (!isWPIEnabledForRLC()) { return false; } return super.shouldPerformWholeProgramInference(tree); @@ -97,7 +97,7 @@ protected boolean shouldPerformWholeProgramInference(Tree tree) { */ @Override protected boolean shouldPerformWholeProgramInference(Tree expressionTree, Tree lhsTree) { - if (isResourceLeakCheckerEnabled()) { + if (!isWPIEnabledForRLC()) { return false; } return super.shouldPerformWholeProgramInference(expressionTree, lhsTree); 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 e6f730b5545..787957f3367 100644 --- a/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallTransfer.java +++ b/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallTransfer.java @@ -177,7 +177,7 @@ private void lubWithStoreValue(CFStore store, JavaExpression expr, AnnotationMir @Override protected boolean shouldPerformWholeProgramInference(Tree tree) { - if (isResourceLeakCheckerEnabled()) { + if (!isWPIEnabledForRLC()) { return false; } return super.shouldPerformWholeProgramInference(tree); @@ -185,7 +185,7 @@ protected boolean shouldPerformWholeProgramInference(Tree tree) { @Override protected boolean shouldPerformWholeProgramInference(Tree expressionTree, Tree lhsTree) { - if (isResourceLeakCheckerEnabled()) { + if (!isWPIEnabledForRLC()) { return false; } return super.shouldPerformWholeProgramInference(expressionTree, lhsTree); 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 611aa4cc67d..84b3c135e41 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java @@ -769,7 +769,7 @@ 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) { + protected 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, @@ -1214,7 +1214,7 @@ private void removeObligationsContainingVarIfNotDerivedFromMustCallAlias( * temporary variable (via a call to {@link * ResourceLeakAnnotatedTypeFactory#getTempVarForNode}) */ - private void updateObligationsForPseudoAssignment( + protected 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. diff --git a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java index 041933ec20a..33d0ea8a4cf 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java @@ -140,7 +140,7 @@ public class MustCallInferenceLogic { for (Node node : current.block.getNodes()) { if (node instanceof MethodInvocationNode || node instanceof ObjectCreationNode) { - updateMethodInvocationOrObjectCreationNode(obligations, node); + mcca.updateObligationsWithInvocationResult(obligations, node); if (node instanceof MethodInvocationNode) { checkMethodInvocation(obligations, (MethodInvocationNode) node); } @@ -281,18 +281,7 @@ private void updateObligationsForAssignment( addOwningToParamsIfDisposedAtAssignment(obligations, rhsObligation, rhs); } else if (lhs instanceof LocalVariableNode) { LocalVariableNode lhsVar = (LocalVariableNode) lhs; - Obligation lhsObligation = - MustCallConsistencyAnalyzer.getObligationForVar(obligations, lhsVar); - if (lhsObligation == null) { - Set newResourceAliasesForObligation = - new LinkedHashSet<>(rhsObligation.resourceAliases); - newResourceAliasesForObligation.add( - new ResourceAlias(new LocalVariable(lhsVar), lhs.getTree())); - obligations.remove(rhsObligation); - obligations.add(new Obligation(newResourceAliasesForObligation)); - } else { - obligations.remove(rhsObligation); - } + mcca.updateObligationsForPseudoAssignment(obligations, assignmentNode, lhsVar, rhs); } } @@ -646,41 +635,6 @@ private boolean mustCallObligationSatisfied( return false; } - /** - * Updates the set of obligations any must-call-alias parameters passed to the given method - * invocation or object creation node. - * - * @param obligations the set of obligations to update - * @param node the node representing the method invocation or object creation - */ - private void updateMethodInvocationOrObjectCreationNode(Set obligations, Node node) { - List arguments = mcca.getArgumentsOfInvocation(node); - List parameters = mcca.getParametersOfInvocation(node); - - for (int i = 0; i < arguments.size(); i++) { - Node tempVar = mcca.getTempVarOrNode(arguments.get(i)); - if (!(tempVar instanceof LocalVariableNode)) { - continue; - } - - Obligation obligation = - MustCallConsistencyAnalyzer.getObligationForVar(obligations, (LocalVariableNode) tempVar); - if (obligation == null) { - continue; - } - - Node method = mcca.getTempVarOrNode(node); - if (typeFactory.hasMustCallAlias(parameters.get(i))) { - Set newResourceAliasesForObligation = - new LinkedHashSet<>(obligation.resourceAliases); - newResourceAliasesForObligation.add( - new ResourceAlias(new LocalVariable((LocalVariableNode) method), node.getTree())); - obligations.remove(obligation); - obligations.add(new Obligation(newResourceAliasesForObligation)); - } - } - } - /** * 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 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 3f084b54b79..f1652166964 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakChecker.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakChecker.java @@ -19,6 +19,7 @@ @SupportedOptions({ "permitStaticOwning", "permitInitializationLeak", + "enableWPIForRLC", ResourceLeakChecker.COUNT_MUST_CALL, MustCallChecker.NO_CREATES_MUSTCALLFOR, MustCallChecker.NO_LIGHTWEIGHT_OWNERSHIP, 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 5a1f42a4e77..068895f5f7e 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakVisitor.java @@ -187,6 +187,12 @@ private void checkOwningOverrides( } } + @Override + protected boolean shouldPerformContractInference() { + // TODO: should be "false whenever running MustCallInferenceLogic", probably + return false; + } + // 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 diff --git a/checker/tests/ainfer-resourceleak/non-annotated/ECMInference.java b/checker/tests/ainfer-resourceleak/non-annotated/ECMInference.java index e5e9353d766..21bdb0d00ef 100644 --- a/checker/tests/ainfer-resourceleak/non-annotated/ECMInference.java +++ b/checker/tests/ainfer-resourceleak/non-annotated/ECMInference.java @@ -1,3 +1,4 @@ +// @skip-test if -AenableWPIForRLC flag is not passed import org.checkerframework.checker.calledmethods.qual.CalledMethods; public class ECMInference { 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 7158be88b53..ab5281d9adb 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java @@ -114,7 +114,7 @@ public abstract class CFAbstractTransfer< private final boolean infer; /** Indicates that the resource leak checker is enabled. */ - private final boolean resourceLeakChecker; + private final boolean enableWPIForRLC; /** * Create a CFAbstractTransfer. @@ -139,11 +139,7 @@ protected CFAbstractTransfer( this.analysis = analysis; this.sequentialSemantics = !(forceConcurrentSemantics || analysis.checker.hasOption("concurrentSemantics")); - this.resourceLeakChecker = - analysis - .checker - .getUpstreamCheckerNames() - .contains("org.checkerframework.checker.resourceleak.ResourceLeakChecker"); + this.enableWPIForRLC = analysis.checker.hasOption("enableWPIForRLC"); this.infer = analysis.checker.hasOption("infer"); } @@ -1003,8 +999,8 @@ public TransferResult visitInstanceOf(InstanceOfNode node, TransferInput Date: Thu, 29 Jun 2023 01:33:25 -0700 Subject: [PATCH 011/132] address comments --- .../resourceleak/MustCallInferenceLogic.java | 91 ++++++++++++------- .../ResourceLeakAnnotatedTypeFactory.java | 10 +- 2 files changed, 62 insertions(+), 39 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java index 33d0ea8a4cf..3082b595191 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java @@ -62,13 +62,23 @@ * representing a method. The algorithm determines if the @MustCall obligation of a field is * fulfilled 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 by this instance. Additionally, if the current method being analyzed - * fulfills the must-call obligation of all the enclosed owning fields, it adds - * a @InheritableMustCall annotation on the enclosing class. + * the method being analyzed by this instance. Additionally, if the method being analyzed fulfills + * 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. This + * limitation should be taken into account while using the class. Must-call set with more than one + * element may also be supported in the future.

+ * + * @see Automatic Inference of Resource Leak + * Specifications */ public class MustCallInferenceLogic { - /** The set of owning fields that are released within the CFG currently under analysis. */ + /** + * The set of owning fields that have been inferred to be released within the CFG currently + * under analysis. + */ private final Set owningFieldToECM = new HashSet<>(); /** @@ -86,15 +96,13 @@ public class MustCallInferenceLogic { private final MustCallConsistencyAnalyzer mcca; /** The MethodTree of the cfg. */ - private MethodTree enMethodTree; + private MethodTree enclosingMethodTree; /** The element for the enMethodTree. */ - private ExecutableElement enMethodElt; + private ExecutableElement enclosingMethodElt; /** - * Creates a MustCallInferenceLogic. If the type factory has whole program inference enabled, its - * postAnalyze method should instantiate a new MustCallInferenceLogic using this constructor and - * then call {@link #runInference()}. + * Creates a MustCallInferenceLogic instance. * * @param typeFactory the type factory * @param cfg the control flow graph of the method to check @@ -108,8 +116,23 @@ public class MustCallInferenceLogic { this.mcca = mcca; this.cfg = cfg; OWNING = AnnotationBuilder.fromClass(this.typeFactory.getElementUtils(), Owning.class); - enMethodTree = ((UnderlyingAST.CFGMethod) cfg.getUnderlyingAST()).getMethod(); - enMethodElt = TreeUtils.elementFromDeclaration(enMethodTree); + enclosingMethodTree = ((UnderlyingAST.CFGMethod) cfg.getUnderlyingAST()).getMethod(); + enclosingMethodElt = TreeUtils.elementFromDeclaration(enclosingMethodTree); + } + + /** + * Creates a MustCallInferenceLogic instance, runs the inference algorithm. If the type factory + * has whole program inference enabled, its postAnalyze method should execute the inference + * algorithm using this method. + * + * @param typeFactory the type factory + * @param cfg the control flow graph of the method to check + * @param mcca the MustCallConsistencyAnalyzer + */ + protected static void runMustCallInferenceLogic( + ResourceLeakAnnotatedTypeFactory typeFactory, ControlFlowGraph cfg, MustCallConsistencyAnalyzer mcca) { + MustCallInferenceLogic mustCallInferenceLogic = new MustCallInferenceLogic(typeFactory, cfg, mcca); + mustCallInferenceLogic.runInference(); } /** @@ -121,7 +144,7 @@ public class MustCallInferenceLogic { * adds @Owning to the formal parameter if it discovers their must-call obligations were satisfied * along one of the checked paths. */ - /*package-private*/ void runInference() { + private void runInference() { Set visited = new HashSet<>(); @@ -154,12 +177,13 @@ public class MustCallInferenceLogic { } /** - * Returns a set of obligations representing the non-empty MustCall parameters of the current - * method. + * Returns a set of obligations representing the non-empty MustCall parameters of the method that + * corresponds to the given cfg, or 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 non-empty MustCall parameters of the current - * method + * @return a set of obligations representing the non-empty MustCall parameters of the method + * corresponding to a CFG. */ private Set getNonEmptyMCParams(ControlFlowGraph cfg) { // TODO what about lambdas? @@ -167,7 +191,7 @@ private Set getNonEmptyMCParams(ControlFlowGraph cfg) { return Collections.emptySet(); } Set result = new LinkedHashSet<>(1); - for (VariableTree param : enMethodTree.getParameters()) { + for (VariableTree param : enclosingMethodTree.getParameters()) { VariableElement paramElement = TreeUtils.elementFromDeclaration(param); if (typeFactory.declaredTypeHasMustCall(param)) { result.add( @@ -179,13 +203,13 @@ private Set getNonEmptyMCParams(ControlFlowGraph cfg) { } /** - * This function returns a set of all owning fields that have been inferred in the current or + * This function returns a set of all owning fields that have been inferred in the current or any * previous iteration * * @return set of owning fields */ private Set getEnclosedOwningFields() { - ClassTree classTree = TreePathUtil.enclosingClass(typeFactory.getPath(enMethodTree)); + ClassTree classTree = TreePathUtil.enclosingClass(typeFactory.getPath(enclosingMethodTree)); TypeElement classElt = TreeUtils.elementFromDeclaration(classTree); Set enOwningFields = new HashSet<>(); for (Element memberElt : classElt.getEnclosedElements()) { @@ -206,16 +230,17 @@ private Set getEnclosedOwningFields() { */ private void addOwningOnParams(int index) { WholeProgramInference wpi = typeFactory.getWholeProgramInference(); - wpi.addDeclarationAnnotationToFormalParameter(enMethodElt, index, OWNING); + wpi.addDeclarationAnnotationToFormalParameter(enclosingMethodElt, index, OWNING); } /** - * Checks if the given node is a field and if it is a new Owning field. + * Infers @Owning annotation for the given node if it is a field and its must-call obligation is + * fulfilled via the given method call. If so, it adds the node to the owningFieldToECM set. * * @param node the possible owning field * @param mNode method invoked on the possible owning field */ - private void isOwningField(@Nullable Node node, MethodInvocationNode mNode) { + private void inferOwningField(@Nullable Node node, MethodInvocationNode mNode) { if (node == null) { return; } @@ -268,7 +293,7 @@ private void updateObligationsForAssignment( return; } - if (TreeUtils.isConstructor(enMethodTree)) { + if (TreeUtils.isConstructor(enclosingMethodTree)) { addOwningToParamsIfDisposedAtAssignment(obligations, rhsObligation, rhs); } else { if (owningFieldToECM.contains((VariableElement) lhsElement)) { @@ -298,7 +323,7 @@ private void addOwningToParamsIfDisposedAtAssignment( Set rhsAliases = rhsObligation.resourceAliases; for (ResourceAlias rl : rhsAliases) { Element rhdElt = rl.reference.getElement(); - List params = enMethodTree.getParameters(); + List params = enclosingMethodTree.getParameters(); for (int i = 0; i < params.size(); i++) { VariableElement paramElt = TreeUtils.elementFromDeclaration(params.get(i)); if (paramElt.equals(rhdElt)) { @@ -333,7 +358,7 @@ private void addEnsuresCalledMethods() { builder.setValue("methods", new String[] {mustCallValue}); AnnotationMirror am = builder.build(); WholeProgramInference wpi = typeFactory.getWholeProgramInference(); - wpi.addMethodDeclarationAnnotation(enMethodElt, am); + wpi.addMethodDeclarationAnnotation(enclosingMethodElt, am); } } @@ -345,7 +370,7 @@ private void addEnsuresCalledMethods() { * InheritableMustCall annotation to the enclosing class. */ private void addOrUpdateMustCall() { - ClassTree classTree = TreePathUtil.enclosingClass(typeFactory.getPath(enMethodTree)); + ClassTree classTree = TreePathUtil.enclosingClass(typeFactory.getPath(enclosingMethodTree)); TypeElement typeElement = TreeUtils.elementFromDeclaration(classTree); if (typeElement == null) { return; @@ -376,12 +401,12 @@ private void addOrUpdateMustCall() { // if the enclosing method is not private and satisfies the must-call obligation of all owning // fields, add an InheritableMustCall annotation with the name of this method - if (!enMethodTree.getModifiers().getFlags().contains(Modifier.PRIVATE)) { + if (!enclosingMethodTree.getModifiers().getFlags().contains(Modifier.PRIVATE)) { if (!owningFieldToECM.isEmpty() && owningFieldToECM.size() == getEnclosedOwningFields().size()) { AnnotationBuilder builder = new AnnotationBuilder(typeFactory.getProcessingEnv(), InheritableMustCall.class); - String[] methodArray = new String[] {enMethodTree.getName().toString()}; + String[] methodArray = new String[] {enclosingMethodTree.getName().toString()}; Arrays.sort(methodArray); builder.setValue("value", methodArray); wpi.addClassDeclarationAnnotation(typeElement, builder.build()); @@ -453,7 +478,7 @@ private void checkReceiverOfMethodCall( Element receiverEl = TreeUtils.elementFromTree(receiver.getTree()); if (receiverEl != null) { if (receiverEl.getKind().isField()) { - isOwningField(receiver, mNode); + inferOwningField(receiver, mNode); return; } } @@ -521,11 +546,11 @@ private void checkIndirectCalls( continue; } if (nElt.getKind().isField()) { - isOwningField(n, mNode); + inferOwningField(n, mNode); } } } else if (argElt != null && argElt.getKind().isField()) { - isOwningField(arg, mNode); + inferOwningField(arg, mNode); } Set argAliases = getResourceAliasOfArgument(obligations, arg); @@ -577,11 +602,11 @@ private Set getResourceAliasOfArgument(Set obligation * @param mNode the MethodInvocationNode */ private void checkMethodInvocation(Set obligations, MethodInvocationNode mNode) { - if (enMethodElt == null) { + if (enclosingMethodElt == null) { return; } - List paramsOfEnclosingMethod = enMethodTree.getParameters(); + List paramsOfEnclosingMethod = enclosingMethodTree.getParameters(); checkArgsOfMethodCall(obligations, mNode, paramsOfEnclosingMethod); checkReceiverOfMethodCall(obligations, mNode, paramsOfEnclosingMethod); 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 36f76512cec..4697c0fb8f1 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakAnnotatedTypeFactory.java @@ -102,11 +102,11 @@ 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() && !getMustCallValue(element).isEmpty()); @@ -138,9 +138,7 @@ public void postAnalyze(ControlFlowGraph cfg) { // finalizer methods and @InheritableMustCall annotations for the class declarations if (getWholeProgramInference() != null) { if (cfg.getUnderlyingAST().getKind() == UnderlyingAST.Kind.METHOD) { - MustCallInferenceLogic mustCallInferenceLogic = - new MustCallInferenceLogic(this, cfg, mustCallConsistencyAnalyzer); - mustCallInferenceLogic.runInference(); + MustCallInferenceLogic.runMustCallInferenceLogic(this,cfg, mustCallConsistencyAnalyzer); } } From d83eb35013fb0ebd66d2fde5db8b7d8179724a27 Mon Sep 17 00:00:00 2001 From: Narges Shadab Date: Thu, 29 Jun 2023 02:33:19 -0700 Subject: [PATCH 012/132] address Martin's comments --- .../calledmethods/CalledMethodsTransfer.java | 14 ++++++++++++++ .../mustcall/MustCallAnnotatedTypeFactory.java | 16 +++++++++++++++- .../checker/mustcall/MustCallTransfer.java | 14 ++++++++++++++ .../resourceleak/MustCallInferenceLogic.java | 17 ++++++++++------- .../ResourceLeakAnnotatedTypeFactory.java | 2 +- .../resourceleak/ResourceLeakChecker.java | 7 +++++-- .../resourceleak/ResourceLeakVisitor.java | 16 ++++++++++++++-- .../framework/flow/CFAbstractTransfer.java | 13 ------------- 8 files changed, 73 insertions(+), 26 deletions(-) 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 913d1d3d8b6..3fa0edfa4b3 100644 --- a/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsTransfer.java +++ b/checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsTransfer.java @@ -12,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; @@ -51,6 +52,9 @@ public class CalledMethodsTransfer extends AccumulationTransfer { */ private final ExecutableElement calledMethodsValueElement; + /** True if -AenableWPIForRLC was passed on the command line. */ + private final boolean enableWPIForRLC; + /** * Create a new CalledMethodsTransfer. * @@ -60,6 +64,7 @@ public CalledMethodsTransfer(CalledMethodsAnalysis analysis) { super(analysis); calledMethodsValueElement = ((CalledMethodsAnnotatedTypeFactory) atypeFactory).calledMethodsValueElement; + enableWPIForRLC = atypeFactory.getChecker().hasOption(ResourceLeakChecker.ENABLE_WPI_FOR_RLC); } /** @@ -268,4 +273,13 @@ private void handleEnsuresCalledMethodsVarArgs( return atypeFactory.createAccumulatorAnnotation(newList); } + + /** + * Checks if wpi is enabled for the Resource Leak Checker inference. + * + * @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 9484cf5e12d..975b4b0300f 100644 --- a/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallAnnotatedTypeFactory.java @@ -28,6 +28,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; @@ -111,6 +112,9 @@ public class MustCallAnnotatedTypeFactory extends BaseAnnotatedTypeFactory /** True if -AnoLightweightOwnership was passed on the command line. */ private final boolean noLightweightOwnership; + /** True if -AenableWPIForRLC was passed on the command line. */ + private final boolean enableWPIForRLC; + /** * Creates a MustCallAnnotatedTypeFactory. * @@ -127,6 +131,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(); } @@ -222,7 +227,7 @@ private void changeNonOwningParameterTypesToTop( // as their @MustCall obligation is set to Top in this method. However, this computation is not // desirable for RLC inference in unannotated programs, where the goal is to infer and add // @Owning annotations to owning parameters. - if (getWholeProgramInference() != null) { + if (getWholeProgramInference() != null && !isWPIEnabledForRLC()) { return; } List parameterTypes = type.getParameterTypes(); @@ -450,4 +455,13 @@ && getDeclAnnotation(elt, MustCallAlias.class) != null) { public @Nullable LocalVariableNode getTempVar(Node node) { return tempVars.get(node.getTree()); } + + /** + * Checks if wpi is enabled for the Resource Leak Checker inference. + * + * @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/MustCallTransfer.java b/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallTransfer.java index 787957f3367..a7dd320de5e 100644 --- a/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallTransfer.java +++ b/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallTransfer.java @@ -15,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; @@ -59,6 +60,9 @@ 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. */ + private final boolean enableWPIForRLC; + /** * Create a MustCallTransfer. * @@ -69,6 +73,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); } @@ -309,4 +314,13 @@ 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. + * + * @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/resourceleak/MustCallInferenceLogic.java b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java index 3082b595191..a454ef73d30 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java @@ -68,16 +68,16 @@ * *

Note: This class makes the assumption that the must-call set has only one element. This * limitation should be taken into account while using the class. Must-call set with more than one - * element may also be supported in the future.

+ * element may also be supported in the future. * * @see Automatic Inference of Resource Leak - * Specifications + * Specifications */ public class MustCallInferenceLogic { /** - * The set of owning fields that have been inferred to be released within the CFG currently - * under analysis. + * The set of owning fields that have been inferred to be released within the CFG currently under + * analysis. */ private final Set owningFieldToECM = new HashSet<>(); @@ -130,8 +130,11 @@ public class MustCallInferenceLogic { * @param mcca the MustCallConsistencyAnalyzer */ protected static void runMustCallInferenceLogic( - ResourceLeakAnnotatedTypeFactory typeFactory, ControlFlowGraph cfg, MustCallConsistencyAnalyzer mcca) { - MustCallInferenceLogic mustCallInferenceLogic = new MustCallInferenceLogic(typeFactory, cfg, mcca); + ResourceLeakAnnotatedTypeFactory typeFactory, + ControlFlowGraph cfg, + MustCallConsistencyAnalyzer mcca) { + MustCallInferenceLogic mustCallInferenceLogic = + new MustCallInferenceLogic(typeFactory, cfg, mcca); mustCallInferenceLogic.runInference(); } @@ -183,7 +186,7 @@ private void runInference() { * * @param cfg the control flow graph of the method to check * @return a set of obligations representing the non-empty MustCall parameters of the method - * corresponding to a CFG. + * corresponding to a CFG. */ private Set getNonEmptyMCParams(ControlFlowGraph cfg) { // TODO what about lambdas? 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 4697c0fb8f1..8f2f5ba6c0e 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakAnnotatedTypeFactory.java @@ -138,7 +138,7 @@ public void postAnalyze(ControlFlowGraph cfg) { // finalizer methods and @InheritableMustCall annotations for the class declarations if (getWholeProgramInference() != null) { if (cfg.getUnderlyingAST().getKind() == UnderlyingAST.Kind.METHOD) { - MustCallInferenceLogic.runMustCallInferenceLogic(this,cfg, mustCallConsistencyAnalyzer); + MustCallInferenceLogic.runMustCallInferenceLogic(this, cfg, mustCallConsistencyAnalyzer); } } 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 f1652166964..df5ef139956 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakChecker.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakChecker.java @@ -19,11 +19,11 @@ @SupportedOptions({ "permitStaticOwning", "permitInitializationLeak", - "enableWPIForRLC", 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 +38,9 @@ public ResourceLeakChecker() {} */ public static final String COUNT_MUST_CALL = "countMustCall"; + /** Command-line option for enabling wpi for the Resource Leak Checker. */ + 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 068895f5f7e..3afb05ed9a0 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakVisitor.java @@ -49,6 +49,9 @@ 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. */ + private final boolean enableWPIForRLC; + /** * Create the visitor. * @@ -59,6 +62,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 @@ -189,8 +193,7 @@ private void checkOwningOverrides( @Override protected boolean shouldPerformContractInference() { - // TODO: should be "false whenever running MustCallInferenceLogic", probably - return false; + return isWPIEnabledForRLC(); } // Overwritten to check that destructors (i.e. methods responsible for resolving @@ -431,4 +434,13 @@ private void checkOwningField(Element field) { error); } } + + /** + * Checks if wpi is enabled for the Resource Leak Checker inference. + * + * @return returns true if wpi is enabled for the Resource Leak Checker + */ + protected boolean isWPIEnabledForRLC() { + return enableWPIForRLC; + } } 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 ab5281d9adb..a3981cb90d6 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java @@ -113,9 +113,6 @@ public abstract class CFAbstractTransfer< /** Indicates that the whole-program inference is on. */ private final boolean infer; - /** Indicates that the resource leak checker is enabled. */ - private final boolean enableWPIForRLC; - /** * Create a CFAbstractTransfer. * @@ -139,7 +136,6 @@ protected CFAbstractTransfer( this.analysis = analysis; this.sequentialSemantics = !(forceConcurrentSemantics || analysis.checker.hasOption("concurrentSemantics")); - this.enableWPIForRLC = analysis.checker.hasOption("enableWPIForRLC"); this.infer = analysis.checker.hasOption("infer"); } @@ -994,15 +990,6 @@ public TransferResult visitInstanceOf(InstanceOfNode node, TransferInput Date: Fri, 4 Aug 2023 14:06:41 -0700 Subject: [PATCH 013/132] update java doc for checkMethodInvocation --- .../resourceleak/MustCallInferenceLogic.java | 32 ++++++++++++------- 1 file changed, 21 insertions(+), 11 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java index a454ef73d30..41d7e3fd9bd 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java @@ -597,23 +597,33 @@ private Set getResourceAliasOfArgument(Set obligation } /** - * 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 - * #owningFieldToECM} set. + * This method performs three checks related to method invocation node and compute @Owning + * annotations to the enclosing formal parameter or fields: + * + *
    + *
  • It calls {@link #checkArgsOfMethodCall} to inspect the arguments of a method invocation + * and identify if any of them are passed as an owning parameter. If found, it adds the + * "owning" attribute to the corresponding parameters of the enclosing method. + *
  • It calls {@link #checkReceiverOfMethodCall} to verify if the receiver of the method + * represented by {@code mNode} qualifies as a candidate owning field, and if the method + * invocation satisfies the field's must-call obligation. If these conditions are met, the + * field is added to the {@link #owningFieldToECM} set. + *
  • It calls {@link #checkIndirectCalls} to inspect the method represented by the given + * MethodInvocationNode for any indirect calls within it. The method analyzes the + * called-methods set of each argument after the call and computes the @Owning annotation to + * the field or parameter passed as an argument to this call. + *
* * @param obligations the set of obligations to search in * @param mNode the MethodInvocationNode */ private void checkMethodInvocation(Set obligations, MethodInvocationNode mNode) { - if (enclosingMethodElt == null) { - return; + if (enclosingMethodElt != null) { + List paramsOfEnclosingMethod = enclosingMethodTree.getParameters(); + checkArgsOfMethodCall(obligations, mNode, paramsOfEnclosingMethod); + checkReceiverOfMethodCall(obligations, mNode, paramsOfEnclosingMethod); + checkIndirectCalls(obligations, mNode, paramsOfEnclosingMethod); } - - List paramsOfEnclosingMethod = enclosingMethodTree.getParameters(); - - checkArgsOfMethodCall(obligations, mNode, paramsOfEnclosingMethod); - checkReceiverOfMethodCall(obligations, mNode, paramsOfEnclosingMethod); - checkIndirectCalls(obligations, mNode, paramsOfEnclosingMethod); } /** From 37cd3e2c1a801c7626c9f1ae34d195e012bd06d1 Mon Sep 17 00:00:00 2001 From: Narges Shadab Date: Fri, 4 Aug 2023 14:20:05 -0700 Subject: [PATCH 014/132] update --- .../MustCallConsistencyAnalyzer.java | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) 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 84b3c135e41..d1849975acb 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java @@ -1455,15 +1455,20 @@ && varTrackedInObligations(obligations, (LocalVariableNode) receiver)) AccumulationStore cmStoreBefore = typeFactory.getStoreBefore(rhs); AccumulationValue cmValue = cmStoreBefore == null ? null : cmStoreBefore.getValue(lhs); AnnotationMirror cmAnno = null; - if (cmValue != null) { - for (AnnotationMirror anno : cmValue.getAnnotations()) { - if (AnnotationUtils.areSameByName( - anno, "org.checkerframework.checker.calledmethods.qual.CalledMethods")) { - cmAnno = anno; - break; + if (cmValue != null) { // When store contains the lhs + Set accumulatedValues = cmValue.getAccumulatedValues(); + if (accumulatedValues != null) { // type variable or wildcard type + cmAnno = typeFactory.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 = typeFactory.top; } From 9e2cc1a8851d4b7c44dcc6c0fe41fbac71a66c09 Mon Sep 17 00:00:00 2001 From: Narges Shadab Date: Fri, 4 Aug 2023 14:29:00 -0700 Subject: [PATCH 015/132] update java doc for checkMethodInvocation --- .../MustCallConsistencyAnalyzer.java | 2 +- .../resourceleak/MustCallInferenceLogic.java | 35 +++++++++---------- 2 files changed, 17 insertions(+), 20 deletions(-) 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 d1849975acb..963bcf98f0d 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java @@ -2178,7 +2178,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( + protected 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. diff --git a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java index 41d7e3fd9bd..e33fcec7b6e 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java @@ -96,10 +96,10 @@ public class MustCallInferenceLogic { private final MustCallConsistencyAnalyzer mcca; /** The MethodTree of the cfg. */ - private MethodTree enclosingMethodTree; + private final MethodTree enclosingMethodTree; /** The element for the enMethodTree. */ - private ExecutableElement enclosingMethodElt; + private final ExecutableElement enclosingMethodElt; /** * Creates a MustCallInferenceLogic instance. @@ -299,9 +299,7 @@ private void updateObligationsForAssignment( if (TreeUtils.isConstructor(enclosingMethodTree)) { addOwningToParamsIfDisposedAtAssignment(obligations, rhsObligation, rhs); } else { - if (owningFieldToECM.contains((VariableElement) lhsElement)) { - owningFieldToECM.remove((VariableElement) lhsElement); - } + owningFieldToECM.remove((VariableElement) lhsElement); addOwningToParamsIfDisposedAtAssignment(obligations, rhsObligation, rhs); } @@ -395,7 +393,7 @@ private void addOrUpdateMustCall() { // necessary when there are multiple candidates for the must-call obligation. AnnotationBuilder builder = new AnnotationBuilder(typeFactory.getProcessingEnv(), InheritableMustCall.class); - String[] methodArray = new String[] {currentMustCallValues.get(0).toString()}; + String[] methodArray = new String[] {currentMustCallValues.get(0)}; Arrays.sort(methodArray); builder.setValue("value", methodArray); wpi.addClassDeclarationAnnotation(typeElement, builder.build()); @@ -650,12 +648,17 @@ private boolean mustCallObligationSatisfied( @Nullable AccumulationValue cmValue = cmStoreAfter == null ? null : cmStoreAfter.getValue(target); AnnotationMirror cmAnno = null; - if (cmValue != null) { - for (AnnotationMirror anno : cmValue.getAnnotations()) { - if (AnnotationUtils.areSameByName( - anno, "org.checkerframework.checker.calledmethods.qual.CalledMethods")) { - cmAnno = anno; - break; + + if (cmValue != null) { // When store contains the lhs + Set accumulatedValues = cmValue.getAccumulatedValues(); + if (accumulatedValues != null) { // type variable or wildcard type + cmAnno = typeFactory.createCalledMethods(accumulatedValues.toArray(new String[0])); + } else { + for (AnnotationMirror anno : cmValue.getAnnotations()) { + if (AnnotationUtils.areSameByName( + anno, "org.checkerframework.checker.calledmethods.qual.CalledMethods")) { + cmAnno = anno; + } } } } @@ -664,13 +667,7 @@ private boolean mustCallObligationSatisfied( cmAnno = typeFactory.top; } - AnnotationMirror cmAnnoForMustCallMethods = - typeFactory.createCalledMethods(mustCallValues.toArray(new String[0])); - if (!mustCallValues.isEmpty() - && typeFactory.getQualifierHierarchy().isSubtype(cmAnno, cmAnnoForMustCallMethods)) { - return true; - } - return false; + return mcca.calledMethodsSatisfyMustCall(mustCallValues, cmAnno); } /** From a958009d9690ddcabdd219cf0fea2cc12b63977c Mon Sep 17 00:00:00 2001 From: Narges Shadab Date: Fri, 28 Apr 2023 14:10:37 -0700 Subject: [PATCH 016/132] add a test case --- .../MustAliasWithDifferentMCSet.java | 34 +++++++++++++++++++ 1 file changed, 34 insertions(+) create mode 100644 checker/tests/resourceleak/MustAliasWithDifferentMCSet.java diff --git a/checker/tests/resourceleak/MustAliasWithDifferentMCSet.java b/checker/tests/resourceleak/MustAliasWithDifferentMCSet.java new file mode 100644 index 00000000000..ed854f5c3c0 --- /dev/null +++ b/checker/tests/resourceleak/MustAliasWithDifferentMCSet.java @@ -0,0 +1,34 @@ +import org.checkerframework.checker.calledmethods.qual.EnsuresCalledMethods; +import org.checkerframework.checker.mustcall.qual.InheritableMustCall; +import org.checkerframework.checker.mustcall.qual.MustCallAlias; +import org.checkerframework.checker.mustcall.qual.Owning; + +class MustAliasWithDifferentMCSet { + + @InheritableMustCall("a") + static class Foo { + void a() {} + } + + @InheritableMustCall("b") + static class FooField { + private final @Owning Foo finalOwningFoo; + + public @MustCallAlias FooField(@MustCallAlias Foo f) { + this.finalOwningFoo = f; + } + + @EnsuresCalledMethods( + value = {"this.finalOwningFoo"}, + methods = {"a"}) + void b() { + this.finalOwningFoo.a(); + } + } + + void testField() { + Foo f = new Foo(); // False Positive for this line + FooField fooField = new FooField(f); + fooField.b(); + } +} From 7e678fb2f279115c91e97f9153f55b007c862196 Mon Sep 17 00:00:00 2001 From: Narges Shadab Date: Fri, 4 Aug 2023 15:05:52 -0700 Subject: [PATCH 017/132] update --- .../checker/resourceleak/MustCallConsistencyAnalyzer.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 611e0b2c417..214c2fb144c 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java @@ -1034,7 +1034,7 @@ private void updateObligationsForOwningReturn( * @param node a node * @return the temporary for node, or node if no temporary exists */ - protected Node getTempVarOrNode(final Node node) { + protected Node getTempVarOrNode(Node node) { Node temp = typeFactory.getTempVarForNode(node); if (temp != null) { return temp; From d32645ef923a25ea082fccf0962919fb21f1bb54 Mon Sep 17 00:00:00 2001 From: Narges Shadab Date: Mon, 7 Aug 2023 20:17:33 -0700 Subject: [PATCH 018/132] fix deprecation warning --- .../org/checkerframework/checker/mustcall/MustCallVisitor.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 e793d5ee751..66553503040 100644 --- a/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/mustcall/MustCallVisitor.java @@ -243,7 +243,7 @@ public boolean isValidUse( // 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.hasAnnotation(PolyMustCall.class) + useType.hasPrimaryAnnotation(PolyMustCall.class) && !AnnotationUtils.containsSameByClass( elt.getAnnotationMirrors(), PolyMustCall.class); if (ajavaFileHasMustCallAlias From ee90781746978e1974882ed136ce507315ecf80e Mon Sep 17 00:00:00 2001 From: Narges Shadab Date: Mon, 7 Aug 2023 21:18:19 -0700 Subject: [PATCH 019/132] remove a MustAliasWithDifferentMCSet.java --- .../MustAliasWithDifferentMCSet.java | 34 ------------------- 1 file changed, 34 deletions(-) delete mode 100644 checker/tests/resourceleak/MustAliasWithDifferentMCSet.java diff --git a/checker/tests/resourceleak/MustAliasWithDifferentMCSet.java b/checker/tests/resourceleak/MustAliasWithDifferentMCSet.java deleted file mode 100644 index ed854f5c3c0..00000000000 --- a/checker/tests/resourceleak/MustAliasWithDifferentMCSet.java +++ /dev/null @@ -1,34 +0,0 @@ -import org.checkerframework.checker.calledmethods.qual.EnsuresCalledMethods; -import org.checkerframework.checker.mustcall.qual.InheritableMustCall; -import org.checkerframework.checker.mustcall.qual.MustCallAlias; -import org.checkerframework.checker.mustcall.qual.Owning; - -class MustAliasWithDifferentMCSet { - - @InheritableMustCall("a") - static class Foo { - void a() {} - } - - @InheritableMustCall("b") - static class FooField { - private final @Owning Foo finalOwningFoo; - - public @MustCallAlias FooField(@MustCallAlias Foo f) { - this.finalOwningFoo = f; - } - - @EnsuresCalledMethods( - value = {"this.finalOwningFoo"}, - methods = {"a"}) - void b() { - this.finalOwningFoo.a(); - } - } - - void testField() { - Foo f = new Foo(); // False Positive for this line - FooField fooField = new FooField(f); - fooField.b(); - } -} From 3bd8772e04a6415fafa9cfba6be09dd2f56f39e3 Mon Sep 17 00:00:00 2001 From: Nargeshdb Date: Tue, 8 Aug 2023 11:37:10 -0700 Subject: [PATCH 020/132] update --- .../non-annotated/EnsuresCalledMethodsVarArgsTest.java | 6 +++--- .../ainfer-resourceleak/non-annotated/OwningParams.java | 4 ++-- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/checker/tests/ainfer-resourceleak/non-annotated/EnsuresCalledMethodsVarArgsTest.java b/checker/tests/ainfer-resourceleak/non-annotated/EnsuresCalledMethodsVarArgsTest.java index eb6fc448817..9d0fc7b28ee 100644 --- a/checker/tests/ainfer-resourceleak/non-annotated/EnsuresCalledMethodsVarArgsTest.java +++ b/checker/tests/ainfer-resourceleak/non-annotated/EnsuresCalledMethodsVarArgsTest.java @@ -21,15 +21,15 @@ public static void close(Foo... foos) { } private class ECMVA { - final Foo fff; + final Foo foo; ECMVA() { // :: warning: (required.method.not.called) - fff = new Foo(); + foo = new Foo(); } void finalyzer() { - Utils.close(fff); + Utils.close(foo); } @EnsuresCalledMethods( diff --git a/checker/tests/ainfer-resourceleak/non-annotated/OwningParams.java b/checker/tests/ainfer-resourceleak/non-annotated/OwningParams.java index b65aff7e25a..7df6c165fcc 100644 --- a/checker/tests/ainfer-resourceleak/non-annotated/OwningParams.java +++ b/checker/tests/ainfer-resourceleak/non-annotated/OwningParams.java @@ -31,8 +31,8 @@ void owningFoo(@Owning Foo f) { f.a(); } - void passOwnership(Foo f111, Foo f2) { - hasECM(f111); + void passOwnership(Foo f1, Foo f2) { + hasECM(f1); owningFoo(f2); } From 74cfa33f5ad7aba81cb21ae97fe53b31b0756b82 Mon Sep 17 00:00:00 2001 From: Nargeshdb Date: Fri, 11 Aug 2023 16:28:55 -0700 Subject: [PATCH 021/132] cleanup --- .../resourceleak/MustCallInferenceLogic.java | 89 +++++++++++++------ .../EnsuresCalledMethodsTest.java | 9 ++ .../EnsuresCalledMethodsVarArgsTest.java | 4 + 3 files changed, 74 insertions(+), 28 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java index e33fcec7b6e..100b7506958 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallInferenceLogic.java @@ -323,11 +323,11 @@ private void addOwningToParamsIfDisposedAtAssignment( Set obligations, Obligation rhsObligation, Node rhs) { Set rhsAliases = rhsObligation.resourceAliases; for (ResourceAlias rl : rhsAliases) { - Element rhdElt = rl.reference.getElement(); + Element rhsElt = rl.reference.getElement(); List params = enclosingMethodTree.getParameters(); for (int i = 0; i < params.size(); i++) { VariableElement paramElt = TreeUtils.elementFromDeclaration(params.get(i)); - if (paramElt.equals(rhdElt)) { + if (paramElt.equals(rhsElt)) { addOwningOnParams(i); mcca.removeObligationsContainingVar(obligations, (LocalVariableNode) rhs); break; @@ -345,6 +345,7 @@ private void addEnsuresCalledMethods() { for (VariableElement owningField : owningFieldToECM) { List mustCallValues = typeFactory.getMustCallValue(owningField); assert !mustCallValues.isEmpty() : "Must-call obligation of an owning field is deleted."; + assert mustCallValues.size() == 1 : "The size of the must-call set is greater than one."; // Assume must-call set has one element String key = mustCallValues.get(0); String value = "this." + owningField.getSimpleName().toString(); @@ -517,8 +518,8 @@ private void checkReceiverOfMethodCall( /** * Checks for indirect calls within the method represented by the given MethodInvocationNode. It - * checks the called-methods set of each argument after the call and adds owning to the field or - * parameter passed as an argument to this call. + * checks the called-methods set of each argument after the call to infer owning annotation for + * the field or parameter passed as an argument to this call. * * @param obligations Set of obligations associated with the current code block. * @param mNode Method invocation node to check. @@ -538,34 +539,66 @@ private void checkIndirectCalls( for (int i = 0; i < arguments.size(); i++) { Node arg = NodeUtils.removeCasts(arguments.get(i)); Element argElt = TreeUtils.elementFromTree(arg.getTree()); - if (argElt == null && arg instanceof ArrayCreationNode) { - ArrayCreationNode arrayCreationNode = (ArrayCreationNode) arg; - List arrays = arrayCreationNode.getInitializers(); - for (Node n : arrays) { - Element nElt = TreeUtils.elementFromTree(n.getTree()); - if (nElt == null) { - continue; - } - if (nElt.getKind().isField()) { - inferOwningField(n, mNode); - } - } + + if (arg instanceof ArrayCreationNode) { + ArrayCreationNode varArgsNode = (ArrayCreationNode) arg; + checkCalledMethodsSetForVarArg(obligations, varArgsNode, mNode, paramsOfEnclosingMethod, i); } else if (argElt != null && argElt.getKind().isField()) { inferOwningField(arg, mNode); } Set argAliases = getResourceAliasOfArgument(obligations, arg); - for (int j = 0; j < paramsOfEnclosingMethod.size(); j++) { - VariableElement paramElt = TreeUtils.elementFromDeclaration(paramsOfEnclosingMethod.get(j)); - for (ResourceAlias rl : argAliases) { - Element argAliasElt = rl.reference.getElement(); - if (!argAliasElt.equals(paramElt)) { - continue; - } - JavaExpression target = JavaExpression.fromVariableTree(paramsOfEnclosingMethod.get(j)); - if (mustCallObligationSatisfied(mNode, paramElt, target)) { - addOwningOnParams(i); - } + processArgAliases(mNode, paramsOfEnclosingMethod, i, argAliases); + } + } + + private void checkCalledMethodsSetForVarArg( + Set obligations, + ArrayCreationNode varArgsNode, + MethodInvocationNode mNode, + List paramsOfEnclosingMethod, + int argIndex) { + + for (Node argNode : varArgsNode.getInitializers()) { + Element varArgElt = TreeUtils.elementFromTree(argNode.getTree()); + + if (varArgElt == null) { + continue; + } + + if (varArgElt.getKind().isField()) { + inferOwningField(argNode, mNode); + } else { + Set argAliases = getResourceAliasOfArgument(obligations, argNode); + processArgAliases(mNode, paramsOfEnclosingMethod, argIndex, argAliases); + } + } + } + + private void processArgAliases( + MethodInvocationNode mNode, + List paramsOfEnclosingMethod, + int argIndex, + Set argAliases) { + + for (int j = 0; j < paramsOfEnclosingMethod.size(); j++) { + VariableElement paramElt = TreeUtils.elementFromDeclaration(paramsOfEnclosingMethod.get(j)); + + for (ResourceAlias rl : argAliases) { + Element argAliasElt = rl.reference.getElement(); + if (!argAliasElt.equals(paramElt)) { + continue; + } + + JavaExpression target = JavaExpression.fromVariableTree(paramsOfEnclosingMethod.get(j)); + if (mustCallObligationSatisfied(mNode, paramElt, target)) { + addOwningOnParams(j); + break; + } + + if (typeFactory.hasOwning(parameters.get(argIndex))) { + addOwningOnParams(j); + break; } } } @@ -601,7 +634,7 @@ private Set getResourceAliasOfArgument(Set obligation *