Ignore control flow due to NullPointerExceptions in Called Methods Checker

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

@@ -0,0 +1,40 @@
+package org.checkerframework.checker.calledmethods;
+
+import com.sun.tools.javac.code.Type;
+import javax.lang.model.type.TypeMirror;
+import org.checkerframework.common.basetype.BaseTypeChecker;
+import org.checkerframework.framework.flow.CFAnalysis;
+
+/**
+ * The analysis for the Called Methods Checker. The analysis is specialized to ignore certain
+ * exception types; see {@link #isIgnoredExceptionType(TypeMirror)}.
+ */
+public class CalledMethodsAnalysis extends CFAnalysis {
+
+  /**
+   * Creates a new {@code CalledMethodsAnalysis}.
+   *
+   * @param checker the checker
+   * @param factory the factory
+   */
+  protected CalledMethodsAnalysis(
+      BaseTypeChecker checker, CalledMethodsAnnotatedTypeFactory factory) {
+    super(checker, factory);
+  }
+
+  /**
+   * Ignore exceptional control flow due to {@code NullPointerException}s, as this checker assumes
+   * the Nullness Checker will be used to prevent such exceptions.
+   *
+   * @param exceptionType exception type
+   * @return {@code true} if {@code exceptionType} is {@code NullPointerException}, {@code false}
+   *     otherwise
+   */
+  @Override
+  protected boolean isIgnoredExceptionType(TypeMirror exceptionType) {
+    return ((Type) exceptionType)
+        .tsym
+        .getQualifiedName()
+        .contentEquals("java.lang.NullPointerException");
+  }
+}

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

@@ -354,6 +354,11 @@ public Void visitExecutable(AnnotatedTypeMirror.AnnotatedExecutableType t, Void
     }
   }
 
+  @Override
+  protected CalledMethodsAnalysis createFlowAnalysis() {
+    return new CalledMethodsAnalysis(checker, this);
+  }
+
   /**
    * Returns the annotation type mirror for the type of {@code expressionTree} with default
    * annotations applied. As types relevant to Called Methods checking are rarely used inside

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

@@ -22,7 +22,6 @@
 import org.checkerframework.dataflow.cfg.node.Node;
 import org.checkerframework.dataflow.expression.JavaExpression;
 import org.checkerframework.framework.flow.CFAbstractStore;
-import org.checkerframework.framework.flow.CFAnalysis;
 import org.checkerframework.framework.flow.CFStore;
 import org.checkerframework.framework.flow.CFValue;
 import org.checkerframework.framework.type.AnnotatedTypeMirror;
@@ -56,7 +55,7 @@ public class CalledMethodsTransfer extends AccumulationTransfer {
    *
    * @param analysis the analysis
    */
-  public CalledMethodsTransfer(final CFAnalysis analysis) {
+  public CalledMethodsTransfer(final CalledMethodsAnalysis analysis) {
     super(analysis);
     calledMethodsValueElement =
         ((CalledMethodsAnnotatedTypeFactory) atypeFactory).calledMethodsValueElement;

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

@@ -2,6 +2,7 @@
 
 import java.util.List;
 import javax.lang.model.element.AnnotationMirror;
+import org.checkerframework.checker.calledmethods.CalledMethodsAnalysis;
 import org.checkerframework.checker.calledmethods.CalledMethodsTransfer;
 import org.checkerframework.checker.mustcall.CreatesMustCallForElementSupplier;
 import org.checkerframework.checker.mustcall.MustCallAnnotatedTypeFactory;
@@ -14,7 +15,6 @@
 import org.checkerframework.dataflow.cfg.node.ObjectCreationNode;
 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.CFValue;
 import org.checkerframework.javacutil.TypesUtils;
@@ -34,7 +34,7 @@ public class ResourceLeakTransfer extends CalledMethodsTransfer {
    * @param analysis the analysis. Its type factory must be a {@link
    *     ResourceLeakAnnotatedTypeFactory}.
    */
-  public ResourceLeakTransfer(final CFAnalysis analysis) {
+  public ResourceLeakTransfer(final CalledMethodsAnalysis analysis) {
     super(analysis);
     this.rlTypeFactory = (ResourceLeakAnnotatedTypeFactory) analysis.getTypeFactory();
   }

checker/tests/calledmethods/EnsuresCalledMethodsIfTest.java

@@ -7,10 +7,10 @@
 class EnsuresCalledMethodsIfTest {
 
   @EnsuresCalledMethods(value = "#1", methods = "close")
-  // The contract is not satisfied.  Suppose `sock` is null.  Then `sock.close()` throws a
-  // NullPointerException before `sock.close()` has a chance to be called.  The exception is caught
-  // and control exits the method without `close()` being called.
-  // :: error: (contracts.postcondition)
+  // If `sock` is null, `sock.close()` will not be called, and the method will exit normally, as the
+  // NullPointerException is caught.  But, the Called Methods Checker
+  // assumes the program is free of NullPointerExceptions, delegating verification of that
+  // property to the Nullness Checker.  So, the postcondition is verified.
   public static void closeSock(EnsuresCalledMethodsIfTest sock) throws Exception {
     if (!sock.isOpen()) {
       return;

checker/tests/calledmethods/Postconditions.java

@@ -96,4 +96,37 @@ static void callWithException(Postconditions p) {
     } catch (java.io.IOException e) {
     }
   }
+
+  @EnsuresCalledMethods(
+      value = {"#1", "#2"},
+      methods = "a")
+  static void callAOnBoth(Postconditions p1, Postconditions p2) {
+    p1.a();
+    p2.a();
+  }
+
+  @EnsuresCalledMethods(
+      value = {"#1", "#2"},
+      methods = "a")
+  static void callAOnBothCatchNPE(Postconditions p1, Postconditions p2) {
+    // postcondition is verified because the checker assumes NullPointerExceptions cannot occur
+    try {
+      p1.a();
+    } catch (NullPointerException e) {
+    }
+    p2.a();
+  }
+
+  @EnsuresCalledMethods(
+      value = {"#1", "#2"},
+      methods = "a")
+  static int callAOnBothFinallyNPE(Postconditions p1, Postconditions p2) {
+    // postcondition is verified because the checker assumes NullPointerExceptions cannot occur
+    try {
+      p1.a();
+    } finally {
+      p2.a();
+      return 0;
+    }
+  }
 }

checker/tests/resourceleak/MultipleMethodParamsMustCallAliasTest.java

@@ -27,8 +27,6 @@ void testMultiMethodParamsCorrect2(@Owning InputStream in1, @Owning InputStream
     }
   }
 
-  // It's a FP, see: https://github.com/typetools/checker-framework/issues/4843
-  // :: error: required.method.not.called
   void testMultiMethodParamsCorrect3(@Owning InputStream in1, @Owning InputStream in2)
       throws IOException {
 

dataflow/src/main/java/org/checkerframework/dataflow/analysis/AbstractAnalysis.java

@@ -11,6 +11,7 @@
 import java.util.PriorityQueue;
 import java.util.Set;
 import javax.lang.model.element.Element;
+import javax.lang.model.type.TypeMirror;
 import org.checkerframework.checker.interning.qual.FindDistinct;
 import org.checkerframework.checker.interning.qual.InternedDistinct;
 import org.checkerframework.checker.nullness.qual.EnsuresNonNull;
@@ -360,6 +361,20 @@ protected final void init(ControlFlowGraph cfg) {
     initInitialInputs();
   }
 
+  /**
+   * Should exceptional control flow for a particular exception type be ignored?
+   *
+   * <p>The default implementation always returns {@code false}. Subclasses should override the
+   * method to implement a different policy.
+   *
+   * @param exceptionType the exception type
+   * @return {@code true} if exceptional control flow due to {@code exceptionType} should be
+   *     ignored, {@code false} otherwise
+   */
+  protected boolean isIgnoredExceptionType(TypeMirror exceptionType) {
+    return false;
+  }
+
   /**
    * Initialize fields of this object based on a given control flow graph. Sub-class may override
    * this method to initialize customized fields.

dataflow/src/main/java/org/checkerframework/dataflow/analysis/BackwardAnalysisImpl.java

@@ -5,6 +5,7 @@
 import java.util.ListIterator;
 import java.util.Map;
 import java.util.Set;
+import javax.lang.model.type.TypeMirror;
 import org.checkerframework.checker.interning.qual.FindDistinct;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.checkerframework.checker.nullness.qual.RequiresNonNull;
@@ -254,7 +255,11 @@ protected void propagateStoresTo(
   protected void addStoreAfter(Block pred, @Nullable Node node, S s, boolean addBlockToWorklist) {
     // If the block pred is an exception block, decide whether the block of passing node is an
     // exceptional successor of the block pred
-    if (isExceptionalSucc(pred, node)) {
+    TypeMirror excSuccType = getSuccExceptionType(pred, node);
+    if (excSuccType != null) {
+      if (isIgnoredExceptionType(excSuccType)) {
+        return;
+      }
       // If the block of passing node is an exceptional successor of Block pred, propagate
       // store to the exceptionStores. Currently it doesn't track the label of an
       // exceptional edge from exception block to its exceptional successors in backward
@@ -283,28 +288,30 @@ protected void addStoreAfter(Block pred, @Nullable Node node, S s, boolean addBl
   }
 
   /**
-   * Checks if the block for a node is an exceptional successor of a predecessor block.
+   * Checks if the block for a node is an exceptional successor of a predecessor block, and if so,
+   * returns the exception type for the control-flow edge.
    *
    * @param pred the predecessor block
    * @param node the successor node
-   * @return {@code true} if {@code pred} is an {@link ExceptionBlock} and the block for {@code
-   *     node} is an exceptional successor of {@code pred}, false otherwise
+   * @return the exception type leading to a control flow edge from {@code pred} to the block for
+   *     {@code node}, if it exists; {@code null} otherwise
    */
-  private boolean isExceptionalSucc(Block pred, @Nullable Node node) {
+  private @Nullable TypeMirror getSuccExceptionType(Block pred, @Nullable Node node) {
     if (pred instanceof ExceptionBlock && node != null) {
       Block block = node.getBlock();
       if (block != null) {
-        for (Set<Block> excSuccBlocks :
-            ((ExceptionBlock) pred).getExceptionalSuccessors().values()) {
-          for (Block excSuccBlock : excSuccBlocks) {
+        Map<TypeMirror, Set<Block>> exceptionalSuccessors =
+            ((ExceptionBlock) pred).getExceptionalSuccessors();
+        for (TypeMirror excType : exceptionalSuccessors.keySet()) {
+          for (Block excSuccBlock : exceptionalSuccessors.get(excType)) {
             if (excSuccBlock.getUid() == block.getUid()) {
-              return true;
+              return excType;
             }
           }
         }
       }
     }
-    return false;
+    return null;
   }
 
   /**

dataflow/src/main/java/org/checkerframework/dataflow/analysis/ForwardAnalysisImpl.java

@@ -159,6 +159,9 @@ public void performAnalysisBlock(Block b) {
           // Propagate store to exceptional successors
           for (Map.Entry<TypeMirror, Set<Block>> e : eb.getExceptionalSuccessors().entrySet()) {
             TypeMirror cause = e.getKey();
+            if (isIgnoredExceptionType(cause)) {
+              continue;
+            }
             S exceptionalStore = transferResult.getExceptionalStore(cause);
             if (exceptionalStore != null) {
               for (Block exceptionSucc : e.getValue()) {