First Phase of RLC inference (#5870)

Co-authored-by: Michael Ernst <mernst@cs.washington.edu> Co-authored-by: Manu Sridharan <msridhar@gmail.com> Co-authored-by: Martin Kellogg <martin.kellogg@njit.edu>

Author: 4 people

checker/build.gradle

@@ -910,7 +910,8 @@ task wpiManyTest(group: 'Verification') {
  '-i', "${project.projectDir}/tests/wpi-many/testin.txt",
  '-o', "${project.projectDir}/build/wpi-many-tests",
  '-s',
- '--', '--checker', 'nullness,interning,lock,regex,signature,calledmethods,resourceleak'
+ '--', '--checker', 'nullness,interning,lock,regex,signature,calledmethods,resourceleak',
+ '--extraJavacArgs=-AenableWpiForRlc'
  }
  } catch (Exception e) {
  println('Failure: Running wpi-many.sh failed with a non-zero exit code.')

checker/src/main/java/org/checkerframework/checker/calledmethods/CalledMethodsTransfer.java

@@ -1,5 +1,6 @@
 package org.checkerframework.checker.calledmethods;
 
+import com.sun.source.tree.Tree;
 import java.util.Arrays;
 import java.util.Collections;
 import java.util.LinkedHashMap;
@@ -11,6 +12,7 @@
 import javax.lang.model.type.TypeMirror;
 import org.checkerframework.checker.calledmethods.qual.EnsuresCalledMethodsVarArgs;
 import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.checker.resourceleak.ResourceLeakChecker;
 import org.checkerframework.common.accumulation.AccumulationStore;
 import org.checkerframework.common.accumulation.AccumulationTransfer;
 import org.checkerframework.common.accumulation.AccumulationValue;
@@ -50,6 +52,12 @@ public class CalledMethodsTransfer extends AccumulationTransfer {
  */
  private final ExecutableElement calledMethodsValueElement;
 
+ /**
+ * True if -AenableWpiForRlc was passed on the command line. See {@link
+ * ResourceLeakChecker#ENABLE_WPI_FOR_RLC}.
+ */
+ private final boolean enableWpiForRlc;
+
  /**
  * Create a new CalledMethodsTransfer.
  *
@@ -59,6 +67,40 @@ public CalledMethodsTransfer(CalledMethodsAnalysis analysis) {
  super(analysis);
  calledMethodsValueElement =
  ((CalledMethodsAnnotatedTypeFactory) atypeFactory).calledMethodsValueElement;
+ enableWpiForRlc = atypeFactory.getChecker().hasOption(ResourceLeakChecker.ENABLE_WPI_FOR_RLC);
+ }
+
+ /**
+ * @param tree a tree
+ * @return false if Resource Leak Checker is running as one of the upstream checkers and the
+ * -AenableWpiForRlc flag (see {@link ResourceLeakChecker#ENABLE_WPI_FOR_RLC}) is not passed
+ * as a command line argument, otherwise returns the result of the super call
+ */
+ @Override
+ protected boolean shouldPerformWholeProgramInference(Tree tree) {
+ if (!isWpiEnabledForRLC()
+ && atypeFactory.getCheckerNames().contains(ResourceLeakChecker.class.getCanonicalName())) {
+ return false;
+ }
+ return super.shouldPerformWholeProgramInference(tree);
+ }
+
+ /**
+ * See {@link ResourceLeakChecker#ENABLE_WPI_FOR_RLC}.
+ *
+ * @param expressionTree a tree
+ * @param lhsTree its element
+ * @return false if Resource Leak Checker is running as one of the upstream checkers and the
+ * -AenableWpiForRlc flag is not passed as a command line argument, otherwise returns the
+ * result of the super call
+ */
+ @Override
+ protected boolean shouldPerformWholeProgramInference(Tree expressionTree, Tree lhsTree) {
+ if (!isWpiEnabledForRLC()
+ && atypeFactory.getCheckerNames().contains(ResourceLeakChecker.class.getCanonicalName())) {
+ return false;
+ }
+ return super.shouldPerformWholeProgramInference(expressionTree, lhsTree);
  }
 
  @Override
@@ -229,4 +271,14 @@ private void handleEnsuresCalledMethodsVarArgs(
 
  return atypeFactory.createAccumulatorAnnotation(newList);
  }
+
+ /**
+ * Checks if WPI is enabled for the Resource Leak Checker inference. See {@link
+ * ResourceLeakChecker#ENABLE_WPI_FOR_RLC}.
+ *
+ * @return returns true if WPI is enabled for the Resource Leak Checker
+ */
+ protected boolean isWpiEnabledForRLC() {
+ return enableWpiForRlc;
+ }
 }

checker/src/main/java/org/checkerframework/checker/mustcall/MustCallAnnotatedTypeFactory.java

@@ -31,6 +31,7 @@
 import org.checkerframework.checker.mustcall.qual.Owning;
 import org.checkerframework.checker.mustcall.qual.PolyMustCall;
 import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.checker.resourceleak.ResourceLeakChecker;
 import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory;
 import org.checkerframework.common.basetype.BaseTypeChecker;
 import org.checkerframework.dataflow.cfg.block.Block;
@@ -116,6 +117,12 @@ public class MustCallAnnotatedTypeFactory extends BaseAnnotatedTypeFactory
  /** True if -AnoLightweightOwnership was passed on the command line. */
  private final boolean noLightweightOwnership;
 
+ /**
+ * True if -AenableWpiForRlc (see {@link ResourceLeakChecker#ENABLE_WPI_FOR_RLC}) was passed on
+ * the command line.
+ */
+ private final boolean enableWpiForRlc;
+
  /**
  * Creates a MustCallAnnotatedTypeFactory.
  *
@@ -132,6 +139,7 @@ public MustCallAnnotatedTypeFactory(BaseTypeChecker checker) {
  addAliasedTypeAnnotation(MustCallAlias.class, POLY);
  }
  noLightweightOwnership = checker.hasOption(MustCallChecker.NO_LIGHTWEIGHT_OWNERSHIP);
+ enableWpiForRlc = checker.hasOption(ResourceLeakChecker.ENABLE_WPI_FOR_RLC);
  this.postInit();
  }
 
@@ -223,6 +231,13 @@ protected void constructorFromUsePreSubstitution(
  */
  private void changeNonOwningParameterTypesToTop(
  ExecutableElement declaration, AnnotatedExecutableType type) {
+ // Formal parameters without a declared owning annotation are disregarded by the RLC _analysis_,
+ // as their @MustCall obligation is set to Top in this method. However, this computation is not
+ // desirable for RLC _inference_ in unannotated programs, where a goal is to infer and add
+ // @Owning annotations to formal parameters.
+ if (getWholeProgramInference() != null && !isWpiEnabledForRLC()) {
+ return;
+ }
  List<AnnotatedTypeMirror> parameterTypes = type.getParameterTypes();
  for (int i = 0; i < parameterTypes.size(); i++) {
  Element paramDecl = declaration.getParameters().get(i);
@@ -416,7 +431,11 @@ public MustCallTreeAnnotator(MustCallAnnotatedTypeFactory mustCallAnnotatedTypeF
  @Override
  public Void visitIdentifier(IdentifierTree tree, AnnotatedTypeMirror type) {
  Element elt = TreeUtils.elementFromUse(tree);
- if (elt.getKind() == ElementKind.PARAMETER
+ // The following changes are not desired for RLC _inference_ in unannotated programs, where a
+ // goal is to infer and add @Owning annotations to formal parameters. Therefore, if WPI is
+ // enabled, they should not be executed.
+ if (getWholeProgramInference() == null
+ && elt.getKind() == ElementKind.PARAMETER
  && (noLightweightOwnership || getDeclAnnotation(elt, Owning.class) == null)) {
  if (!type.hasPrimaryAnnotation(POLY)) {
  // Parameters that are not annotated with @Owning should be treated as bottom
@@ -443,6 +462,16 @@ public Void visitIdentifier(IdentifierTree tree, AnnotatedTypeMirror type) {
  return tempVars.get(node.getTree());
  }
 
+ /**
+ * Checks if WPI is enabled for the Resource Leak Checker inference. See {@link
+ * ResourceLeakChecker#ENABLE_WPI_FOR_RLC}.
+ *
+ * @return returns true if WPI is enabled for the Resource Leak Checker
+ */
+ protected boolean isWpiEnabledForRLC() {
+ return enableWpiForRlc;
+ }
+
  /**
  * Returns true if the given type should never have a must-call obligation.
  *

checker/src/main/java/org/checkerframework/checker/mustcall/MustCallTransfer.java

@@ -3,6 +3,7 @@
 import com.sun.source.tree.ClassTree;
 import com.sun.source.tree.ExpressionTree;
 import com.sun.source.tree.IdentifierTree;
+import com.sun.source.tree.Tree;
 import com.sun.source.tree.VariableTree;
 import com.sun.source.util.TreePath;
 import java.util.List;
@@ -14,6 +15,7 @@
 import org.checkerframework.checker.mustcall.qual.MustCall;
 import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
 import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.checker.resourceleak.ResourceLeakChecker;
 import org.checkerframework.dataflow.analysis.TransferInput;
 import org.checkerframework.dataflow.analysis.TransferResult;
 import org.checkerframework.dataflow.cfg.node.AssignmentNode;
@@ -58,6 +60,12 @@ public class MustCallTransfer extends CFTransfer {
  /** True if -AnoCreatesMustCallFor was passed on the command line. */
  private final boolean noCreatesMustCallFor;
 
+ /**
+ * True if -AenableWpiForRlc was passed on the command line. See {@link
+ * ResourceLeakChecker#ENABLE_WPI_FOR_RLC}.
+ */
+ private final boolean enableWpiForRlc;
+
  /**
  * Create a MustCallTransfer.
  *
@@ -68,6 +76,7 @@ public MustCallTransfer(CFAnalysis analysis) {
  atypeFactory = (MustCallAnnotatedTypeFactory) analysis.getTypeFactory();
  noCreatesMustCallFor =
  atypeFactory.getChecker().hasOption(MustCallChecker.NO_CREATES_MUSTCALLFOR);
+ enableWpiForRlc = atypeFactory.getChecker().hasOption(ResourceLeakChecker.ENABLE_WPI_FOR_RLC);
  ProcessingEnvironment env = atypeFactory.getChecker().getProcessingEnvironment();
  treeBuilder = new TreeBuilder(env);
  }
@@ -175,6 +184,41 @@ private void lubWithStoreValue(CFStore store, JavaExpression expr, AnnotationMir
  store.insertValue(expr, newValue);
  }
 
+ /**
+ * See {@link ResourceLeakChecker#ENABLE_WPI_FOR_RLC}.
+ *
+ * @param tree a tree
+ * @return false if Resource Leak Checker is running as one of the upstream checkers and the
+ * -AenableWpiForRlc flag is not passed as a command line argument, otherwise returns the
+ * result of the super call
+ */
+ @Override
+ protected boolean shouldPerformWholeProgramInference(Tree tree) {
+ if (!isWpiEnabledForRLC()
+ && atypeFactory.getCheckerNames().contains(ResourceLeakChecker.class.getCanonicalName())) {
+ return false;
+ }
+ return super.shouldPerformWholeProgramInference(tree);
+ }
+
+ /**
+ * See {@link ResourceLeakChecker#ENABLE_WPI_FOR_RLC}.
+ *
+ * @param expressionTree a tree
+ * @param lhsTree its element
+ * @return false if Resource Leak Checker is running as one of the upstream checkers and the
+ * -AenableWpiForRlc flag is not passed as a command line argument, otherwise returns the
+ * result of the super call
+ */
+ @Override
+ protected boolean shouldPerformWholeProgramInference(Tree expressionTree, Tree lhsTree) {
+ if (!isWpiEnabledForRLC()
+ && atypeFactory.getCheckerNames().contains(ResourceLeakChecker.class.getCanonicalName())) {
+ return false;
+ }
+ return super.shouldPerformWholeProgramInference(expressionTree, lhsTree);
+ }
+
  @Override
  public TransferResult<CFValue, CFStore> visitObjectCreation(
  ObjectCreationNode node, TransferInput<CFValue, CFStore> input) {
@@ -299,4 +343,14 @@ public void updateStoreWithTempVar(TransferResult<CFValue, CFStore> result, Node
  protected String uniqueName(String prefix) {
  return prefix + "-" + uid.getAndIncrement();
  }
+
+ /**
+ * Checks if WPI is enabled for the Resource Leak Checker inference. See {@link
+ * ResourceLeakChecker#ENABLE_WPI_FOR_RLC}.
+ *
+ * @return returns true if WPI is enabled for the Resource Leak Checker
+ */
+ protected boolean isWpiEnabledForRLC() {
+ return enableWpiForRlc;
+ }
 }

checker/src/main/java/org/checkerframework/checker/mustcall/MustCallVisitor.java

@@ -23,6 +23,7 @@
 import org.checkerframework.checker.mustcall.qual.MustCallAlias;
 import org.checkerframework.checker.mustcall.qual.NotOwning;
 import org.checkerframework.checker.mustcall.qual.Owning;
+import org.checkerframework.checker.mustcall.qual.PolyMustCall;
 import org.checkerframework.common.basetype.BaseTypeChecker;
 import org.checkerframework.common.basetype.BaseTypeVisitor;
 import org.checkerframework.framework.type.AnnotatedTypeMirror;
@@ -232,9 +233,24 @@ public boolean isValidUse(
  // Note that isValidUse does not need to consider component types, on which it should be
  // called separately.
  Element elt = TreeUtils.elementFromTree(tree);
- if (elt != null
- && AnnotationUtils.containsSameByClass(elt.getAnnotationMirrors(), MustCallAlias.class)) {
- return true;
+ if (elt != null) {
+ if (AnnotationUtils.containsSameByClass(elt.getAnnotationMirrors(), MustCallAlias.class)) {
+ return true;
+ }
+ // Need to check the type mirror for ajava-derived annotations and the element itself
+ // for human-written annotations from the source code. Getting to the ajava file directly
+ // at this point is impossible, so we approximate "the ajava file has an @MustCallAlias
+ // annotation" with "there is an @PolyMustCall annotation on the use type, but not in the
+ // source code". This only works because none of our inference techniques infer @PolyMustCall,
+ // so if @PolyMustCall is present but wasn't in the source, it must have been derived from
+ // an @MustCallAlias annotation (which we do infer).
+ boolean ajavaFileHasMustCallAlias =
+ useType.hasPrimaryAnnotation(PolyMustCall.class)
+ && !AnnotationUtils.containsSameByClass(
+ elt.getAnnotationMirrors(), PolyMustCall.class);
+ if (ajavaFileHasMustCallAlias) {
+ return true;
+ }
  }
  return super.isValidUse(declarationType, useType, tree);
  }