Add @EnsuresCalledMethodsOnException

checker-qual/src/main/java/org/checkerframework/checker/calledmethods/qual/EnsuresCalledMethods.java

@@ -39,6 +39,7 @@
  * </pre>
  *
  * @see EnsuresCalledMethodsIf
+ * @see EnsuresCalledMethodsOnException
  * @checker_framework.manual #called-methods-checker Called Methods Checker
  */
 @PostconditionAnnotation(qualifier = CalledMethods.class)

checker-qual/src/main/java/org/checkerframework/checker/calledmethods/qual/EnsuresCalledMethodsOnException.java

@@ -0,0 +1,97 @@
+package org.checkerframework.checker.calledmethods.qual;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Repeatable;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+import org.checkerframework.framework.qual.InheritedAnnotation;
+
+/**
+ * Indicates that the method, if it terminates by throwing an {@link Exception}, always invokes the
+ * given methods on the given expressions. This annotation is repeatable, which means that users can
+ * write more than one instance of it on the same method (users should NOT manually write an
+ * {@code @EnsuresCalledMethodsOnException.List} annotation, which the checker will create from
+ * multiple copies of this annotation automatically).
+ *
+ * <p>Consider the following method:
+ *
+ * <pre>
+ * &#64;EnsuresCalledMethodsOnException(value = "#1", methods = "m")
+ * public void callM(T t) { ... }
+ * </pre>
+ *
+ * <p>The <code>callM</code> method promises to always call {@code t.m()} before throwing any kind
+ * of {@link Exception}.
+ *
+ * <p>Note that {@code EnsuresCalledMethodsOnException} only describes behavior for {@link
+ * Exception} (and by extension {@link RuntimeException}, {@link NullPointerException}, etc.) but
+ * not {@link Error} or other throwables.
+ *
+ * @see EnsuresCalledMethods
+ * @checker_framework.manual #called-methods-checker Called Methods Checker
+ */
+@Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
+@Repeatable(EnsuresCalledMethodsOnException.List.class)
+@Retention(RetentionPolicy.RUNTIME)
+@InheritedAnnotation
+public @interface EnsuresCalledMethodsOnException {
+
+  /**
+   * Returns Java expressions that have had the given methods called on them after the method throws
+   * an exception.
+   *
+   * @return an array of Java expressions
+   * @checker_framework.manual #java-expressions-as-arguments Syntax of Java expressions
+   */
+  String[] value();
+
+  // NOTE 2023/10/6: There seems to be a fundamental limitation in the dataflow framework that
+  // prevent us from supporting a custom set of exceptions.  Specifically, in the following code:
+  //
+  //     try {
+  //       m1();
+  //     } finally {
+  //       m2();
+  //     }
+  //
+  // all exceptional edges out of the `m1()` call will flow to the same place: the start of the
+  // `m2()` call in the finally block.  Any information about what `m1()` promised on specific
+  // exception types will be lost.
+  //
+  //  /**
+  //   * Returns the exception types under which the postcondition holds.
+  //   *
+  //   * @return the exception types under which the postcondition holds.
+  //   */
+  //  Class<? extends Throwable>[] exceptions();
+
+  /**
+   * The methods guaranteed to be invoked on the expressions if the result of the method throws an
+   * exception.
+   *
+   * @return the methods guaranteed to be invoked on the expressions if the method throws an
+   *     exception
+   */
+  String[] methods();
+
+  /**
+   * A wrapper annotation that makes the {@link EnsuresCalledMethodsOnException} annotation
+   * repeatable. This annotation is an implementation detail: programmers generally do not need to
+   * write this. It is created automatically by Java when a programmer writes more than one {@link
+   * EnsuresCalledMethodsOnException} annotation at the same location.
+   */
+  @Documented
+  @Retention(RetentionPolicy.RUNTIME)
+  @Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
+  @InheritedAnnotation
+  public static @interface List {
+    /**
+     * Return the repeatable annotations.
+     *
+     * @return the repeatable annotations
+     */
+    EnsuresCalledMethodsOnException[] value();
+  }
+}

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

@@ -6,7 +6,10 @@
 import com.sun.source.tree.Tree;
 import java.util.ArrayList;
 import java.util.Collection;
+import java.util.Collections;
+import java.util.LinkedHashSet;
 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.ExecutableElement;
@@ -21,6 +24,7 @@
 import org.checkerframework.checker.calledmethods.qual.CalledMethodsBottom;
 import org.checkerframework.checker.calledmethods.qual.CalledMethodsPredicate;
 import org.checkerframework.checker.calledmethods.qual.EnsuresCalledMethods;
+import org.checkerframework.checker.calledmethods.qual.EnsuresCalledMethodsOnException;
 import org.checkerframework.checker.calledmethods.qual.EnsuresCalledMethodsVarArgs;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.checkerframework.common.accumulation.AccumulationAnnotatedTypeFactory;
@@ -74,6 +78,18 @@ public class CalledMethodsAnnotatedTypeFactory extends AccumulationAnnotatedType
   /*package-private*/ final ExecutableElement ensuresCalledMethodsVarArgsValueElement =
       TreeUtils.getMethod(EnsuresCalledMethodsVarArgs.class, "value", 0, processingEnv);
 
+  /** The {@link EnsuresCalledMethodsOnException#value} element/argument. */
+  /*package-private*/ final ExecutableElement ensuresCalledMethodsOnExceptionValueElement =
+      TreeUtils.getMethod(EnsuresCalledMethodsOnException.class, "value", 0, processingEnv);
+
+  /** The {@link EnsuresCalledMethodsOnException#methods} element/argument. */
+  /*package-private*/ final ExecutableElement ensuresCalledMethodsOnExceptionMethodsElement =
+      TreeUtils.getMethod(EnsuresCalledMethodsOnException.class, "methods", 0, processingEnv);
+
+  /** The {@link EnsuresCalledMethodsOnException.List#value} element/argument. */
+  /*package-private*/ final ExecutableElement ensuresCalledMethodsOnExceptionListValueElement =
+      TreeUtils.getMethod(EnsuresCalledMethodsOnException.List.class, "value", 0, processingEnv);
+
   /**
    * Create a new CalledMethodsAnnotatedTypeFactory.
    *
@@ -385,6 +401,17 @@ protected CalledMethodsAnalysis createFlowAnalysis() {
     return builderFrameworkSupports;
   }
 
+  /**
+   * Get the called methods specified by the given {@link CalledMethods} annotation.
+   *
+   * @param calledMethodsAnnotation the annotation
+   * @return the called methods
+   */
+  protected List<String> getCalledMethods(AnnotationMirror calledMethodsAnnotation) {
+    return AnnotationUtils.getElementValueArray(
+        calledMethodsAnnotation, calledMethodsValueElement, String.class, Collections.emptyList());
+  }
+
   @Override
   protected @Nullable AnnotationMirror createRequiresOrEnsuresQualifier(
       String expression,
@@ -393,8 +420,7 @@ protected CalledMethodsAnalysis createFlowAnalysis() {
       Analysis.BeforeOrAfter preOrPost,
       @Nullable List<AnnotationMirror> preconds) {
     if (preOrPost == BeforeOrAfter.AFTER && isAccumulatorAnnotation(qualifier)) {
-      List<String> calledMethods =
-          AnnotationUtils.getElementValueArray(qualifier, calledMethodsValueElement, String.class);
+      List<String> calledMethods = getCalledMethods(qualifier);
       if (!calledMethods.isEmpty()) {
         return ensuresCMAnno(expression, calledMethods);
       }
@@ -447,4 +473,83 @@ public boolean isIgnoredExceptionType(TypeMirror exceptionType) {
     }
     return false;
   }
+
+  /**
+   * Get the exceptional postconditions for the given method from the {@link
+   * EnsuresCalledMethodsOnException} annotations on it.
+   *
+   * @param methodOrConstructor the method to examine
+   * @return the exceptional postconditions on the given method; the return value is newly-allocated
+   *     and can be freely modified by callers
+   */
+  public Set<EnsuresCalledMethodOnExceptionContract> getExceptionalPostconditions(
+      ExecutableElement methodOrConstructor) {
+    Set<EnsuresCalledMethodOnExceptionContract> result = new LinkedHashSet<>();
+
+    parseEnsuresCalledMethodOnExceptionListAnnotation(
+        getDeclAnnotation(methodOrConstructor, EnsuresCalledMethodsOnException.List.class), result);
+
+    parseEnsuresCalledMethodOnExceptionAnnotation(
+        getDeclAnnotation(methodOrConstructor, EnsuresCalledMethodsOnException.class), result);
+
+    return result;
+  }
+
+  /**
+   * Helper for {@link #getExceptionalPostconditions(ExecutableElement)} that parses a {@link
+   * EnsuresCalledMethodsOnException.List} annotation and stores the results in <code>out</code>.
+   *
+   * @param annotation the annotation
+   * @param out the output collection
+   */
+  private void parseEnsuresCalledMethodOnExceptionListAnnotation(
+      @Nullable AnnotationMirror annotation, Set<EnsuresCalledMethodOnExceptionContract> out) {
+    if (annotation == null) {
+      return;
+    }
+
+    List<AnnotationMirror> annotations =
+        AnnotationUtils.getElementValueArray(
+            annotation,
+            ensuresCalledMethodsOnExceptionListValueElement,
+            AnnotationMirror.class,
+            Collections.emptyList());
+
+    for (AnnotationMirror a : annotations) {
+      parseEnsuresCalledMethodOnExceptionAnnotation(a, out);
+    }
+  }
+
+  /**
+   * Helper for {@link #getExceptionalPostconditions(ExecutableElement)} that parses a {@link
+   * EnsuresCalledMethodsOnException} annotation and stores the results in <code>out</code>.
+   *
+   * @param annotation the annotation
+   * @param out the output collection
+   */
+  private void parseEnsuresCalledMethodOnExceptionAnnotation(
+      @Nullable AnnotationMirror annotation, Set<EnsuresCalledMethodOnExceptionContract> out) {
+    if (annotation == null) {
+      return;
+    }
+
+    List<String> expressions =
+        AnnotationUtils.getElementValueArray(
+            annotation,
+            ensuresCalledMethodsOnExceptionValueElement,
+            String.class,
+            Collections.emptyList());
+    List<String> methods =
+        AnnotationUtils.getElementValueArray(
+            annotation,
+            ensuresCalledMethodsOnExceptionMethodsElement,
+            String.class,
+            Collections.emptyList());
+
+    for (String expr : expressions) {
+      for (String method : methods) {
+        out.add(new EnsuresCalledMethodOnExceptionContract(expr, method));
+      }
+    }
+  }
 }

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

@@ -6,10 +6,12 @@
 import java.util.LinkedHashMap;
 import java.util.List;
 import java.util.Map;
+import javax.annotation.processing.ProcessingEnvironment;
 import javax.lang.model.element.AnnotationMirror;
 import javax.lang.model.element.ExecutableElement;
 import javax.lang.model.element.VariableElement;
 import javax.lang.model.type.TypeMirror;
+import javax.lang.model.util.Types;
 import org.checkerframework.checker.calledmethods.qual.EnsuresCalledMethodsVarArgs;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.checkerframework.checker.resourceleak.ResourceLeakChecker;
@@ -26,8 +28,11 @@
 import org.checkerframework.dataflow.expression.JavaExpression;
 import org.checkerframework.framework.flow.CFAbstractStore;
 import org.checkerframework.framework.type.AnnotatedTypeMirror;
+import org.checkerframework.framework.util.JavaExpressionParseUtil;
+import org.checkerframework.framework.util.StringToJavaExpression;
 import org.checkerframework.javacutil.AnnotationMirrorSet;
 import org.checkerframework.javacutil.AnnotationUtils;
+import org.checkerframework.javacutil.ElementUtils;
 import org.checkerframework.javacutil.TreeUtils;
 import org.plumelib.util.CollectionsPlume;
 
@@ -52,6 +57,9 @@ public class CalledMethodsTransfer extends AccumulationTransfer {
    */
   private final ExecutableElement calledMethodsValueElement;
 
+  /** The type mirror for {@link Exception}. */
+  protected final TypeMirror javaLangExceptionType;
+
   /**
    * True if -AenableWpiForRlc was passed on the command line. See {@link
    * ResourceLeakChecker#ENABLE_WPI_FOR_RLC}.
@@ -68,6 +76,10 @@ public CalledMethodsTransfer(CalledMethodsAnalysis analysis) {
     calledMethodsValueElement =
         ((CalledMethodsAnnotatedTypeFactory) atypeFactory).calledMethodsValueElement;
     enableWpiForRlc = atypeFactory.getChecker().hasOption(ResourceLeakChecker.ENABLE_WPI_FOR_RLC);
+
+    ProcessingEnvironment env = atypeFactory.getProcessingEnv();
+    javaLangExceptionType =
+        env.getTypeUtils().getDeclaredType(ElementUtils.getTypeElement(env, Exception.class));
   }
 
   /**
@@ -109,7 +121,11 @@ public TransferResult<AccumulationValue, AccumulationStore> visitMethodInvocatio
     exceptionalStores = makeExceptionalStores(node, input);
     TransferResult<AccumulationValue, AccumulationStore> superResult =
         super.visitMethodInvocation(node, input);
-    handleEnsuresCalledMethodsVarArgs(node, superResult);
+
+    ExecutableElement method = TreeUtils.elementFromUse(node.getTree());
+    handleEnsuresCalledMethodsVarArgs(node, method, superResult);
+    handleEnsuresCalledMethodsOnException(node, method, exceptionalStores);
+
     Node receiver = node.getTarget().getReceiver();
     if (receiver != null) {
       String methodName = node.getTarget().getMethod().getSimpleName().toString();
@@ -196,11 +212,13 @@ private Map<TypeMirror, AccumulationStore> makeExceptionalStores(
    * present.
    *
    * @param node the method invocation node
+   * @param elt the method being invoked
    * @param result the current result
    */
   private void handleEnsuresCalledMethodsVarArgs(
-      MethodInvocationNode node, TransferResult<AccumulationValue, AccumulationStore> result) {
-    ExecutableElement elt = TreeUtils.elementFromUse(node.getTree());
+      MethodInvocationNode node,
+      ExecutableElement elt,
+      TransferResult<AccumulationValue, AccumulationStore> result) {
     AnnotationMirror annot = atypeFactory.getDeclAnnotation(elt, EnsuresCalledMethodsVarArgs.class);
     if (annot == null) {
       return;
@@ -235,6 +253,49 @@ private void handleEnsuresCalledMethodsVarArgs(
     }
   }
 
+  /**
+   * Update the given <code>exceptionalStores</code> for the {@link
+   * org.checkerframework.checker.calledmethods.qual.EnsuresCalledMethodsOnException} annotations
+   * written on the given <code>method</code>.
+   *
+   * @param node a method invocation
+   * @param method the method being invoked
+   * @param exceptionalStores the stores to update
+   */
+  private void handleEnsuresCalledMethodsOnException(
+      MethodInvocationNode node,
+      ExecutableElement method,
+      Map<TypeMirror, AccumulationStore> exceptionalStores) {
+    Types types = atypeFactory.getProcessingEnv().getTypeUtils();
+    for (EnsuresCalledMethodOnExceptionContract postcond :
+        ((CalledMethodsAnnotatedTypeFactory) atypeFactory).getExceptionalPostconditions(method)) {
+      JavaExpression e;
+      try {
+        e =
+            StringToJavaExpression.atMethodInvocation(
+                postcond.getExpression(), node.getTree(), atypeFactory.getChecker());
+      } catch (JavaExpressionParseUtil.JavaExpressionParseException ex) {
+        // This parse error will be reported later. For now, we'll skip this malformed
+        // postcondition and move on to the others.
+        continue;
+      }
+
+      // NOTE: this code is a little inefficient; it creates a single-method annotation and calls
+      // `insertOrRefine` in a loop.  Even worse, this code appears within a loop.  For now we
+      // aren't too worried about it, since the number of EnsuresCalledMethodsOnException
+      // annotations should be small.
+      AnnotationMirror calledMethod =
+          atypeFactory.createAccumulatorAnnotation(postcond.getMethod());
+      for (Map.Entry<TypeMirror, AccumulationStore> successor : exceptionalStores.entrySet()) {
+        TypeMirror caughtException = successor.getKey();
+        if (types.isSubtype(caughtException, javaLangExceptionType)) {
+          AccumulationStore resultStore = successor.getValue();
+          resultStore.insertOrRefine(e, calledMethod);
+        }
+      }
+    }
+  }
+
   /**
    * Extract the current called-methods type from {@code currentType}, and then add each element of
    * {@code methodNames} to it, and return the result. This method is similar to GLB, but should be