RLC: allow wrapper types to have a differently-named @MustCall method from wrapped type (#6272)

Author: msridhar

checker-qual/src/main/java/org/checkerframework/checker/mustcall/qual/MustCallAlias.java

@@ -11,7 +11,9 @@
  * always be used in pairs. On a method, it is written on some formal parameter type and on the
  * method return type. On a constructor, it is written on some formal parameter type and on the
  * result type. Fulfilling the must-call obligation of one is equivalent to fulfilling the must-call
- * obligation of the other.
+ * obligation of the other. Beyond its impact as a polymorphic annotation on {@code MustCall} types,
+ * the Resource Leak Checker uses {@link MustCallAlias} annotations to more precisely determine when
+ * a must-call obligation has been satisfied.
  *
  * <p>This annotation is useful for wrapper objects. For example, consider the declaration of {@code
  * java.net.Socket#getOutputStream}:
@@ -25,6 +27,25 @@
  * Calling {@code close()} on the returned {@code OutputStream} will close the underlying socket,
  * but the Socket may also be closed directly, which has the same effect.
  *
+ * <h2>Type system semantics</h2>
+ *
+ * Within the Must Call Checker's type system, {@code @MustCallAlias} annotations have a semantics
+ * different from a standard polymorphic annotation, in that the relevant actual parameter type and
+ * return type at a call site are not equated in all cases. Given an actual parameter {@code p}
+ * passed in a {@code @MustCallAlias} position at a call site, the return type of the call is
+ * defined as follows:
+ *
+ * <ul>
+ * <li>If the base return type has a non-empty {@code @InheritableMustCall("m")} annotation on its
+ * declaration, and {@code p} has a non-empty {@code @MustCall} type, then the return type is
+ * {@code @MustCall("m")}.
+ * <li>In all other cases, the return type has the same {@code @MustCall} type as {@code p}.
+ * </ul>
+ *
+ * {@link PolyMustCall} has an identical type system semantics. This special treatment is required
+ * to allow for a wrapper object to have a must-call method with a different name than the must-call
+ * method name for the wrapped object.
+ *
  * <h2>Verifying {@code @MustCallAlias} annotations</h2>
  *
  * Suppose that {@code @MustCallAlias} is written on the type of formal parameter {@code p}.
@@ -47,7 +68,10 @@
  * </ul>
  *
  * When the -AnoResourceAliases command-line argument is passed to the checker, this annotation is
- * treated identically to {@link PolyMustCall}.
+ * treated identically to {@link PolyMustCall}. That is, the annotation still impacts {@link
+ * MustCall} types as a polymorphic annotation (see "Type system semantics" above), but it is not
+ * used by the Resource Leak Checker to more precisely reason about when obligations have been
+ * satisfied.
  *
  * @checker_framework.manual #resource-leak-checker Resource Leak Checker
  * @checker_framework.manual #qualifier-polymorphism Qualifier polymorphism

checker-qual/src/main/java/org/checkerframework/checker/mustcall/qual/PolyMustCall.java

@@ -8,7 +8,9 @@
 import org.checkerframework.framework.qual.PolymorphicQualifier;
 
 /**
- * The polymorphic qualifier for the Must Call type system.
+ * The polymorphic qualifier for the Must Call type system. The semantics of this qualifier differ
+ * from that of a standard polymorphic qualifier; see {@link MustCallAlias} for documentation of its
+ * semantics.
  *
  * @checker_framework.manual #must-call-checker Must Call Checker
  * @checker_framework.manual #qualifier-polymorphism Qualifier polymorphism

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

@@ -22,6 +22,7 @@
 import javax.lang.model.element.Element;
 import javax.lang.model.element.ElementKind;
 import javax.lang.model.element.ExecutableElement;
+import javax.lang.model.element.TypeElement;
 import javax.lang.model.type.TypeMirror;
 import org.checkerframework.checker.mustcall.qual.CreatesMustCallFor;
 import org.checkerframework.checker.mustcall.qual.InheritableMustCall;
@@ -38,19 +39,23 @@
 import org.checkerframework.dataflow.cfg.node.LocalVariableNode;
 import org.checkerframework.dataflow.cfg.node.Node;
 import org.checkerframework.framework.flow.CFStore;
+import org.checkerframework.framework.type.AnnotatedTypeFactory;
 import org.checkerframework.framework.type.AnnotatedTypeMirror;
 import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedArrayType;
 import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType;
 import org.checkerframework.framework.type.GenericAnnotatedTypeFactory;
 import org.checkerframework.framework.type.QualifierHierarchy;
 import org.checkerframework.framework.type.QualifierUpperBounds;
 import org.checkerframework.framework.type.SubtypeIsSubsetQualifierHierarchy;
+import org.checkerframework.framework.type.poly.DefaultQualifierPolymorphism;
+import org.checkerframework.framework.type.poly.QualifierPolymorphism;
 import org.checkerframework.framework.type.treeannotator.ListTreeAnnotator;
 import org.checkerframework.framework.type.treeannotator.TreeAnnotator;
 import org.checkerframework.framework.type.typeannotator.DefaultQualifierForUseTypeAnnotator;
 import org.checkerframework.framework.type.typeannotator.ListTypeAnnotator;
 import org.checkerframework.framework.type.typeannotator.TypeAnnotator;
 import org.checkerframework.javacutil.AnnotationBuilder;
+import org.checkerframework.javacutil.AnnotationMirrorMap;
 import org.checkerframework.javacutil.AnnotationMirrorSet;
 import org.checkerframework.javacutil.AnnotationUtils;
 import org.checkerframework.javacutil.ElementUtils;
@@ -220,6 +225,71 @@ protected void constructorFromUsePreSubstitution(
  super.constructorFromUsePreSubstitution(tree, type);
  }
 
+ /**
+ * Class to implement the customized semantics of {@link MustCallAlias} (and {@link PolyMustCall})
+ * annotations; see the {@link MustCallAlias} documentation for details.
+ */
+ private class MustCallQualifierPolymorphism extends DefaultQualifierPolymorphism {
+ /**
+ * Creates a {@link MustCallQualifierPolymorphism}.
+ *
+ * @param env the processing environment
+ * @param factory the factory for the current checker
+ */
+ public MustCallQualifierPolymorphism(ProcessingEnvironment env, AnnotatedTypeFactory factory) {
+ super(env, factory);
+ }
+
+ @Override
+ protected void replace(
+ AnnotatedTypeMirror type, AnnotationMirrorMap<AnnotationMirror> replacements) {
+ AnnotationMirrorMap<AnnotationMirror> realReplacements = replacements;
+ AnnotationMirror extantPolyAnnoReplacement = null;
+ TypeElement typeElement = TypesUtils.getTypeElement(type.getUnderlyingType());
+ // only customize replacement for type elements
+ if (typeElement != null) {
+ assert replacements.size() == 1 && replacements.containsKey(POLY);
+ extantPolyAnnoReplacement = replacements.get(POLY);
+ if (AnnotationUtils.areSameByName(
+ extantPolyAnnoReplacement, MustCall.class.getCanonicalName())) {
+ List<String> extentReplacementVals =
+ AnnotationUtils.getElementValueArray(
+ extantPolyAnnoReplacement,
+ getMustCallValueElement(),
+ String.class,
+ Collections.emptyList());
+ // replacement only customized when parameter type has a non-empty must-call obligation
+ if (!extentReplacementVals.isEmpty()) {
+ AnnotationMirror inheritableMustCall =
+ getDeclAnnotation(typeElement, InheritableMustCall.class);
+ if (inheritableMustCall != null) {
+ List<String> inheritableMustCallVals =
+ AnnotationUtils.getElementValueArray(
+ inheritableMustCall,
+ inheritableMustCallValueElement,
+ String.class,
+ Collections.emptyList());
+ if (!inheritableMustCallVals.equals(extentReplacementVals)) {
+ // Use the must call values from the @InheritableMustCall annotation instead.
+ // This allows for wrapper types to have a must-call method with a different
+ // name than the must-call method for the wrapped type
+ AnnotationMirror mustCall = createMustCall(inheritableMustCallVals);
+ realReplacements = new AnnotationMirrorMap<>();
+ realReplacements.put(POLY, mustCall);
+ }
+ }
+ }
+ }
+ }
+ super.replace(type, realReplacements);
+ }
+ }
+
+ @Override
+ protected QualifierPolymorphism createQualifierPolymorphism() {
+ return new MustCallQualifierPolymorphism(processingEnv, this);
+ }
+
  /**
  * Changes the type of each parameter not annotated as @Owning to @MustCallUnknown (top). Also
  * replaces the component type of the varargs array, if applicable.

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

@@ -16,6 +16,7 @@
 import java.util.Collections;
 import java.util.Deque;
 import java.util.EnumSet;
+import java.util.HashMap;
 import java.util.HashSet;
 import java.util.IdentityHashMap;
 import java.util.Iterator;
@@ -74,7 +75,6 @@
 import org.checkerframework.framework.flow.CFStore;
 import org.checkerframework.framework.flow.CFValue;
 import org.checkerframework.framework.type.AnnotatedTypeMirror;
-import org.checkerframework.framework.type.QualifierHierarchy;
 import org.checkerframework.framework.util.JavaExpressionParseUtil.JavaExpressionParseException;
 import org.checkerframework.framework.util.StringToJavaExpression;
 import org.checkerframework.javacutil.AnnotationUtils;
@@ -319,35 +319,34 @@ public boolean derivedFromMustCallAlias() {
 
  /**
  * Gets the must-call methods (i.e. the list of methods that must be called to satisfy the
- * must-call obligation) of the resource represented by this Obligation.
+ * must-call obligation) of each resource alias represented by this Obligation.
  *
  * @param rlAtf a Resource Leak Annotated Type Factory
  * @param mcStore a CFStore produced by the MustCall checker's dataflow analysis. If this is
  * null, then the default MustCall type of each variable's class will be used.
- * @return the list of must-call method names, or null if the resource's must-call obligations
- * are unsatisfiable (i.e. its value in the Must Call store is MustCallUnknown)
+ * @return a map from each resource alias of this to a list of its must-call method names, or
+ * null if the must-call obligations are unsatisfiable (i.e. the value of some tracked
+ * resource alias of this in the Must Call store is MustCallUnknown)
  */
- public @Nullable List<String> getMustCallMethods(
+ public @Nullable Map<ResourceAlias, List<String>> getMustCallMethods(
  ResourceLeakAnnotatedTypeFactory rlAtf, @Nullable CFStore mcStore) {
+ Map<ResourceAlias, List<String>> result = new HashMap<>(this.resourceAliases.size());
  MustCallAnnotatedTypeFactory mustCallAnnotatedTypeFactory =
  rlAtf.getTypeFactoryOfSubchecker(MustCallChecker.class);
 
- // Need to get the LUB (ie, union) of the MC values, because if a CreatesMustCallFor
- // method was called on just one of the aliases then they all need to be treated as if
- // they need to call the relevant methods.
- QualifierHierarchy qualHierarchy = mustCallAnnotatedTypeFactory.getQualifierHierarchy();
- AnnotationMirror mcLub = mustCallAnnotatedTypeFactory.BOTTOM;
  for (ResourceAlias alias : this.resourceAliases) {
  AnnotationMirror mcAnno = getMustCallValue(alias, mcStore, mustCallAnnotatedTypeFactory);
- TypeMirror aliasTm = alias.reference.getType();
- mcLub = qualHierarchy.leastUpperBoundShallow(mcLub, aliasTm, mcAnno, aliasTm);
- }
- if (AnnotationUtils.areSameByName(
- mcLub, "org.checkerframework.checker.mustcall.qual.MustCall")) {
- return rlAtf.getMustCallValues(mcLub);
- } else {
- return null;
+ if (!AnnotationUtils.areSameByName(mcAnno, MustCall.class.getCanonicalName())) {
+ // MustCallUnknown; cannot be satisfied
+ return null;
+ }
+ List<String> annoVals = rlAtf.getMustCallValues(mcAnno);
+ // Really, annoVals should never be empty here; we should not have created the obligation in
+ // the first place
+ // TODO: add an assertion that annoVals is non-empty and address any failures
+ result.put(alias, annoVals);
  }
+ return result;
  }
 
  /**
@@ -2324,11 +2323,12 @@ private static boolean varTrackedInObligations(
  private void checkMustCall(
  Obligation obligation, AccumulationStore cmStore, CFStore mcStore, String outOfScopeReason) {
 
- List<String> mustCallValue = obligation.getMustCallMethods(typeFactory, mcStore);
+ Map<ResourceAlias, List<String>> mustCallValues =
+ obligation.getMustCallMethods(typeFactory, mcStore);
 
- // optimization: if mustCallValue is null, always issue a warning (there is no way to satisfy
+ // optimization: if mustCallValues is null, always issue a warning (there is no way to satisfy
  // the check). A null mustCallValue occurs when the type is top (@MustCallUnknown).
- if (mustCallValue == null) {
+ if (mustCallValues == null) {
  // Report the error at the first alias' definition. This choice is arbitrary but
  // consistent.
  ResourceAlias firstAlias = obligation.resourceAliases.iterator().next();
@@ -2345,14 +2345,20 @@ private void checkMustCall(
  }
  return;
  }
- // optimization: if there are no must-call methods, do not need to perform the check
- if (mustCallValue.isEmpty()) {
- return;
+ if (mustCallValues.isEmpty()) {
+ throw new TypeSystemError("unexpected empty must-call values for obligation " + obligation);
  }
 
  boolean mustCallSatisfied = false;
  for (ResourceAlias alias : obligation.resourceAliases) {
 
+ List<String> mustCallValuesForAlias = mustCallValues.get(alias);
+ // optimization when there are no methods to call
+ if (mustCallValuesForAlias.isEmpty()) {
+ mustCallSatisfied = true;
+ break;
+ }
+
  // sometimes the store is null! this looks like a bug in checker dataflow.
  // TODO track down and report the root-cause bug
  AccumulationValue cmValue = cmStore != null ? cmStore.getValue(alias.reference) : null;
@@ -2378,7 +2384,7 @@ private void checkMustCall(
  .getEffectiveAnnotationInHierarchy(typeFactory.top);
  }
 
- if (calledMethodsSatisfyMustCall(mustCallValue, cmAnno)) {
+ if (calledMethodsSatisfyMustCall(mustCallValuesForAlias, cmAnno)) {
  mustCallSatisfied = true;
  break;
  }
@@ -2394,7 +2400,7 @@ private void checkMustCall(
  checker.reportError(
  firstAlias.tree,
  "required.method.not.called",
- formatMissingMustCallMethods(mustCallValue),
+ formatMissingMustCallMethods(mustCallValues.get(firstAlias)),
  firstAlias.stringForErrorMessage(),
  firstAlias.reference.getType().toString(),
  outOfScopeReason);

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

@@ -206,7 +206,7 @@ protected ResourceLeakAnalysis createFlowAnalysis() {
  * Returns the {@link MustCall#value} element/argument of the @MustCall annotation on the class
  * type of {@code element}. If there is no such annotation, returns the empty list.
  *
- * <p>Do not use this method to get the MustCall value of an {@link
+ * <p>Do not use this method to get the MustCall values of an {@link
  * org.checkerframework.checker.resourceleak.MustCallConsistencyAnalyzer.Obligation}. Instead, use
  * {@link
  * org.checkerframework.checker.resourceleak.MustCallConsistencyAnalyzer.Obligation#getMustCallMethods(ResourceLeakAnnotatedTypeFactory,

checker/tests/mustcall/PolyMustCallDifferentNames.java

@@ -0,0 +1,76 @@
+// Tests for @PolyMustCall and @MustCallAlias where the must-call method of the return type has
+// a different name than the must-call method of the parameter type.
+
+import org.checkerframework.checker.calledmethods.qual.EnsuresCalledMethods;
+import org.checkerframework.checker.mustcall.qual.*;
+
+class PolyMustCallDifferentNames {
+
+ @InheritableMustCall("a")
+ static class Wrapped {
+ void a() {}
+ }
+
+ @InheritableMustCall("b")
+ static class Wrapper1 {
+ private final @Owning Wrapped field;
+
+ public @PolyMustCall Wrapper1(@PolyMustCall Wrapped w) {
+ // we get this error since we only have a field-assignment special case for @MustCallAlias,
+ // not @PolyMustCall
+ // :: error: (assignment)
+ this.field = w;
+ }
+
+ @EnsuresCalledMethods(
+ value = {"this.field"},
+ methods = {"a"})
+ void b() {
+ this.field.a();
+ }
+ }
+
+ static @PolyMustCall Wrapper1 getWrapper1(@PolyMustCall Wrapped w) {
+ return new Wrapper1(w);
+ }
+
+ @InheritableMustCall("c")
+ static class Wrapper2 {
+ private final @Owning Wrapped field;
+
+ public @MustCallAlias Wrapper2(@MustCallAlias Wrapped w) {
+ this.field = w;
+ }
+
+ @EnsuresCalledMethods(
+ value = {"this.field"},
+ methods = {"a"})
+ void c() {
+ this.field.a();
+ }
+ }
+
+ static @MustCallAlias Wrapper2 getWrapper2(@MustCallAlias Wrapped w) {
+ return new Wrapper2(w);
+ }
+
+ static void test1() {
+ @MustCall("a") Wrapped x = new Wrapped();
+ @MustCall("b") Wrapper1 w1 = new Wrapper1(x);
+ @MustCall("b") Wrapper1 w2 = getWrapper1(x);
+ // :: error: (assignment)
+ @MustCall("a") Wrapper1 w3 = new Wrapper1(x);
+ // :: error: (assignment)
+ @MustCall("a") Wrapper1 w4 = getWrapper1(x);
+ }
+
+ static void test2() {
+ @MustCall("a") Wrapped x = new Wrapped();
+ @MustCall("c") Wrapper2 w1 = new Wrapper2(x);
+ @MustCall("c") Wrapper2 w2 = getWrapper2(x);
+ // :: error: (assignment)
+ @MustCall("a") Wrapper2 w3 = new Wrapper2(x);
+ // :: error: (assignment)
+ @MustCall("a") Wrapper2 w4 = getWrapper2(x);
+ }
+}