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>

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);
   }