@CreatesMustCallFor create an obligation on exceptional successors

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

@@ -0,0 +1,54 @@
+package org.checkerframework.checker.mustcall;
+
+import com.google.common.collect.ImmutableSet;
+import com.sun.tools.javac.code.Type;
+import java.util.Set;
+import javax.lang.model.type.TypeMirror;
+import org.checkerframework.checker.signature.qual.CanonicalName;
+import org.checkerframework.common.basetype.BaseTypeChecker;
+import org.checkerframework.framework.flow.CFAnalysis;
+
+/**
+ * The analysis for the Must Call Checker. The analysis is specialized to ignore certain exception
+ * types; see {@link #isIgnoredExceptionType(TypeMirror)}.
+ */
+public class MustCallAnalysis extends CFAnalysis {
+
+  /**
+   * Constructs an MustCallAnalysis.
+   *
+   * @param checker the checker
+   * @param factory the type factory
+   */
+  public MustCallAnalysis(BaseTypeChecker checker, MustCallAnnotatedTypeFactory factory) {
+    super(checker, factory);
+  }
+
+  /**
+   * The fully-qualified names of the exception types that are ignored by this checker when
+   * computing dataflow stores.
+   */
+  protected static final Set<@CanonicalName String> ignoredExceptionTypes =
+      ImmutableSet.of(
+          // Use the Nullness Checker instead.
+          NullPointerException.class.getCanonicalName(),
+          // Ignore run-time errors, which cannot be predicted statically. Doing
+          // so is unsound in the sense that they could still occur - e.g., the
+          // program could run out of memory - but if they did, the checker's
+          // results would be useless anyway.
+          Error.class.getCanonicalName(),
+          RuntimeException.class.getCanonicalName());
+
+  /**
+   * Ignore exceptional control flow due to ignored exception types.
+   *
+   * @param exceptionType exception type
+   * @return {@code true} if {@code exceptionType} is a member of {@link #ignoredExceptionTypes},
+   *     {@code false} otherwise
+   */
+  @Override
+  protected boolean isIgnoredExceptionType(TypeMirror exceptionType) {
+    return ignoredExceptionTypes.contains(
+        ((Type) exceptionType).tsym.getQualifiedName().toString());
+  }
+}

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

@@ -23,6 +23,8 @@
 import javax.lang.model.element.ElementKind;
 import javax.lang.model.element.ExecutableElement;
 import javax.lang.model.element.TypeElement;
+import javax.lang.model.type.DeclaredType;
+import javax.lang.model.type.TypeKind;
 import javax.lang.model.type.TypeMirror;
 import org.checkerframework.checker.mustcall.qual.CreatesMustCallFor;
 import org.checkerframework.checker.mustcall.qual.InheritableMustCall;
@@ -164,6 +166,11 @@ protected Set<Class<? extends Annotation>> createSupportedTypeQualifiers() {
         Arrays.asList(MustCall.class, MustCallUnknown.class, PolyMustCall.class));
   }
 
+  @Override
+  protected MustCallAnalysis createFlowAnalysis() {
+    return new MustCallAnalysis(checker, this);
+  }
+
   @Override
   protected TreeAnnotator createTreeAnnotator() {
     return new ListTreeAnnotator(super.createTreeAnnotator(), new MustCallTreeAnnotator(this));
@@ -225,6 +232,15 @@ protected void constructorFromUsePreSubstitution(
     super.constructorFromUsePreSubstitution(tree, type);
   }
 
+  @Override
+  public boolean isIgnoredExceptionType(TypeMirror exceptionType) {
+    if (exceptionType.getKind() == TypeKind.DECLARED) {
+      return MustCallAnalysis.ignoredExceptionTypes.contains(
+          TypesUtils.getQualifiedName((DeclaredType) exceptionType));
+    }
+    return false;
+  }
+
   /**
    * Class to implement the customized semantics of {@link MustCallAlias} (and {@link PolyMustCall})
    * annotations; see the {@link MustCallAlias} documentation for details.

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

@@ -6,7 +6,10 @@
 import com.sun.source.tree.Tree;
 import com.sun.source.tree.VariableTree;
 import com.sun.source.util.TreePath;
+import java.util.Collections;
+import java.util.LinkedHashMap;
 import java.util.List;
+import java.util.Map;
 import java.util.concurrent.atomic.AtomicLong;
 import javax.annotation.processing.ProcessingEnvironment;
 import javax.lang.model.element.AnnotationMirror;
@@ -16,8 +19,11 @@
 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.ConditionalTransferResult;
+import org.checkerframework.dataflow.analysis.RegularTransferResult;
 import org.checkerframework.dataflow.analysis.TransferInput;
 import org.checkerframework.dataflow.analysis.TransferResult;
+import org.checkerframework.dataflow.cfg.block.ExceptionBlock;
 import org.checkerframework.dataflow.cfg.node.AssignmentNode;
 import org.checkerframework.dataflow.cfg.node.LocalVariableNode;
 import org.checkerframework.dataflow.cfg.node.MethodInvocationNode;
@@ -27,7 +33,6 @@
 import org.checkerframework.dataflow.cfg.node.SwitchExpressionNode;
 import org.checkerframework.dataflow.cfg.node.TernaryExpressionNode;
 import org.checkerframework.dataflow.expression.JavaExpression;
-import org.checkerframework.framework.flow.CFAnalysis;
 import org.checkerframework.framework.flow.CFStore;
 import org.checkerframework.framework.flow.CFTransfer;
 import org.checkerframework.framework.flow.CFValue;
@@ -60,6 +65,9 @@ public class MustCallTransfer extends CFTransfer {
   /** True if -AnoCreatesMustCallFor was passed on the command line. */
   private final boolean noCreatesMustCallFor;
 
+  /** A set of stores for the exceptional paths */
+  private @Nullable Map<TypeMirror, CFStore> exceptionalStores;
+
   /**
    * True if -AenableWpiForRlc was passed on the command line. See {@link
    * ResourceLeakChecker#ENABLE_WPI_FOR_RLC}.
@@ -71,7 +79,7 @@ public class MustCallTransfer extends CFTransfer {
    *
    * @param analysis the analysis
    */
-  public MustCallTransfer(CFAnalysis analysis) {
+  public MustCallTransfer(MustCallAnalysis analysis) {
     super(analysis);
     atypeFactory = (MustCallAnnotatedTypeFactory) analysis.getTypeFactory();
     noCreatesMustCallFor =
@@ -163,7 +171,54 @@ public TransferResult<CFValue, CFStore> visitMethodInvocation(
           lubWithStoreValue(store, targetExpr, defaultType);
         }
       }
+
+      if (n.getBlock() instanceof ExceptionBlock) {
+        exceptionalStores = makeExceptionalStores(n, result);
+        // Update stores for the exceptional paths to handle cases like:
+        // https://github.com/typetools/checker-framework/issues/6050
+        if (result.containsTwoStores()) {
+          result =
+              new ConditionalTransferResult<>(
+                  result.getResultValue(),
+                  result.getThenStore().copy(),
+                  result.getElseStore().copy(),
+                  exceptionalStores);
+        } else {
+          result =
+              new RegularTransferResult<>(
+                  result.getResultValue(), result.getRegularStore().copy(), exceptionalStores);
+        }
+        exceptionalStores = null;
+      }
     }
+
+    return result;
+  }
+
+  /**
+   * Create a set of stores for the exceptional paths out of the block containing {@code node}. This
+   * allows propagation, along those paths, of the fact that the method being invoked in {@code
+   * node} was definitely called.
+   *
+   * @param node a method invocation
+   * @param input the transfer input associated with the method invocation
+   * @return a map from types to stores. The keys are the same keys used by {@link
+   *     ExceptionBlock#getExceptionalSuccessors()}. The values are copies of the regular store from
+   *     {@code input}.
+   */
+  private Map<TypeMirror, CFStore> makeExceptionalStores(
+      MethodInvocationNode node, TransferResult<CFValue, CFStore> input) {
+    if (!(node.getBlock() instanceof ExceptionBlock)) {
+      // This can happen in some weird (buggy?) cases:
+      // see https://github.com/typetools/checker-framework/issues/3585
+      return Collections.emptyMap();
+    }
+
+    ExceptionBlock block = (ExceptionBlock) node.getBlock();
+    Map<TypeMirror, CFStore> result = new LinkedHashMap<>();
+    block
+        .getExceptionalSuccessors()
+        .forEach((tm, b) -> result.put(tm, input.getRegularStore().copy()));
     return result;
   }
 

checker/src/main/java/org/checkerframework/checker/resourceleak/MustCallConsistencyAnalyzer.java

@@ -2126,7 +2126,6 @@ private void propagateObligationsToSuccessorBlock(
           // an exceptional path.
           continue;
         }
-
         // Which stores from the called-methods and must-call checkers are used in
         // the consistency check varies depending on the context. The rules are:
         // 1. if the current block has no nodes (and therefore the store must come from
@@ -2139,17 +2138,7 @@ private void propagateObligationsToSuccessorBlock(
         //        set in the successor store, use the current blocks' CM and MC stores,
         //        which contain whatever information is true before this (empty) block.
         // 2. if the current block has one or more nodes, always use the CM store after
-        //    the last node. To decide which MC store to use:
-        //    2a. if the last node in the block is the invocation of an
-        //        @CreatesMustCallFor method that might throw an exception, and the
-        //        consistency check is for an exceptional path, use the MC store
-        //        immediately before the method invocation, because the method threw an
-        //        exception rather than finishing and therefore did not actually create
-        //        any must-call obligation, so the MC store after might contain
-        //        must-call obligations that do not need to be fulfilled along this
-        //        path.
-        //    2b. in all other cases, use the MC store from after the last node in
-        //        the block.
+        //    the last node.
         CFStore mcStore;
         AccumulationStore cmStore;
         if (currentBlockNodes.size() == 0 /* currentBlock is special or conditional */) {
@@ -2174,18 +2163,12 @@ private void propagateObligationsToSuccessorBlock(
             cmStore = typeFactory.getStoreAfter(last);
             cmStoreAfter.put(last, cmStore);
           }
-          // If this is an exceptional block, check the MC store beforehand to avoid
-          // issuing an error about a call to a CreatesMustCallFor method that might
-          // throw an exception. Otherwise, use the store after.
-          if (exceptionType != null && isInvocationOfCreatesMustCallForMethod(last)) {
-            mcStore = mcAtf.getStoreBefore(last); // 2a. (MC)
+
+          if (mcStoreAfter.containsKey(last)) {
+            mcStore = mcStoreAfter.get(last);
           } else {
-            if (mcStoreAfter.containsKey(last)) {
-              mcStore = mcStoreAfter.get(last);
-            } else {
-              mcStore = mcAtf.getStoreAfter(last); // 2b. (MC)
-              mcStoreAfter.put(last, mcStore);
-            }
+            mcStore = mcAtf.getStoreAfter(last); // 2b. (MC)
+            mcStoreAfter.put(last, mcStore);
           }
         }
 
@@ -2222,21 +2205,6 @@ private boolean aliasInScopeInSuccessor(AccumulationStore successorStore, Resour
     return successorStore.getValue(alias.reference) != null;
   }
 
-  /**
-   * Returns true if node is a MethodInvocationNode of a method with a CreatesMustCallFor
-   * annotation.
-   *
-   * @param node a node
-   * @return true if node is a MethodInvocationNode of a method with a CreatesMustCallFor annotation
-   */
-  private boolean isInvocationOfCreatesMustCallForMethod(Node node) {
-    if (!(node instanceof MethodInvocationNode)) {
-      return false;
-    }
-    MethodInvocationNode miNode = (MethodInvocationNode) node;
-    return typeFactory.hasCreatesMustCallFor(miNode);
-  }
-
   /**
    * Finds {@link Owning} formal parameters for the method corresponding to a CFG.
    *

checker/tests/resourceleak/ACSocketTest.java

@@ -360,10 +360,13 @@ void createNewServerSocket(InetSocketAddress address, boolean b, boolean c) thro
     ServerSocket socket;
 
     if (b) {
+      // :: error: required.method.not.called
       socket = new ServerSocket();
     } else if (c) {
+      // :: error: required.method.not.called
       socket = new ServerSocket();
     } else {
+      // :: error: required.method.not.called
       socket = new ServerSocket();
     }
 

checker/tests/resourceleak/AssignNullInExceptionBlock.java

@@ -0,0 +1,79 @@
+import org.checkerframework.checker.mustcall.qual.*;
+import org.checkerframework.checker.nullness.qual.*;
+
+class AssignNullInExceptionBlock {
+
+  static class Foo {}
+
+  static Foo makeFoo() {
+    return new Foo();
+  }
+
+  static Foo makeFoo1() {
+    throw new UnsupportedOperationException();
+  }
+
+  static Foo makeFoo2() throws UnsupportedOperationException {
+    return new Foo();
+  }
+
+  static Foo makeFoo3() throws UnsupportedOperationException {
+    throw new UnsupportedOperationException();
+  }
+
+  Foo fooField;
+
+  void test1() {
+    try {
+      fooField = makeFoo();
+    } catch (Exception e) {
+      Foo f = null;
+      fooField = f;
+    }
+  }
+
+  void test2() {
+    try {
+      fooField = makeFoo1();
+    } catch (Exception e) {
+      Foo f = null;
+      fooField = f;
+    }
+  }
+
+  void test3() {
+    Foo f = null;
+    try {
+      fooField = makeFoo1();
+    } catch (Exception e) {
+      fooField = f;
+    }
+  }
+
+  void test4() {
+    try {
+      fooField = makeFoo2();
+    } catch (Exception e) {
+      Foo f = null;
+      fooField = f;
+    }
+  }
+
+  void test5() {
+    try {
+      fooField = makeFoo3();
+    } catch (Exception e) {
+      Foo f = null;
+      fooField = f;
+    }
+  }
+
+  void test6() {
+    Foo f = null;
+    try {
+      fooField = makeFoo3();
+    } catch (Exception e) {
+      fooField = f;
+    }
+  }
+}