Add Delegation Checker

checker-qual/src/main/java/org/checkerframework/common/delegation/qual/Delegate.java

@@ -0,0 +1,33 @@
+package org.checkerframework.common.delegation.qual;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+/**
+ * This is an annotation that indicates a field is a delegate, fields are not delegates by default.
+ *
+ * <p>Here is a way that this annotation may be used:
+ *
+ * <pre><code>
+ * class MyEnumeration&lt;T&gt; implements Enumeration&lt;T&gt; {
+ *    {@literal @}Delegate
+ *    private Enumeration&lt;T&gt; e;
+ *
+ *    public boolean hasMoreElements() {
+ *      return e.hasMoreElements();
+ *    }
+ * }
+ * </code></pre>
+ *
+ * In the example above, {@code MyEnumeration.hasMoreElements()} delegates a call to {@code
+ * e.hasMoreElements()}.
+ *
+ * @checker_framework.manual #non-empty-checker Non-Empty Checker
+ */
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.FIELD})
+public @interface Delegate {}

checker-qual/src/main/java/org/checkerframework/common/delegation/qual/DelegatorMustOverride.java

@@ -0,0 +1,49 @@
+package org.checkerframework.common.delegation.qual;
+
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+/**
+ * This is an annotation that indicates a method that <i>must</i> be overridden in order for a
+ * conditional postcondition to hold for a delegating class.
+ *
+ * <p>Here is a way that this annotation may be used:
+ *
+ * <p>Given a class that declares a method with a postcondition annotation:
+ *
+ * <pre><code>
+ * class ArrayListVariant&lt;T&gt; {
+ *    {@literal @}EnsuresPresentIf(result = true)
+ *    {@literal @}DelegatorMustOverride
+ *    public boolean hasMoreElements() {
+ *      return e.hasMoreElements();
+ *    }
+ * }
+ * </code></pre>
+ *
+ * A delegating client <i>must</i> override the method:
+ *
+ * <pre><code>
+ * class MyArrayListVariant&lt;T&gt; extends ArrayListVariant&lt;T&gt; {
+ *
+ *    {@literal @}Delegate
+ *     private ArrayListVariant&lt;T&gt; myList;
+ *
+ *
+ *    {@literal @}Override
+ *    {@literal @}EnsuresPresentIf(result = true)
+ *    public boolean hasMoreElements() {
+ *      return myList.hasMoreElements();
+ *    }
+ * }
+ * </code></pre>
+ *
+ * Otherwise, a warning will be raised.
+ *
+ * @checker_framework.manual #non-empty-checker Non-Empty Checker
+ */
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.METHOD})
+public @interface DelegatorMustOverride {}

docs/manual/creating-a-checker.tex

@@ -1872,10 +1872,23 @@
 \end{enumerate}
 
 
-\subsectionAndLabel{Disabling flow-sensitive inference}{creating-dataflow-disable}
-
-In the uncommon case that you wish to disable the Checker Framework's
-built-in flow inference in your checker (this is different than choosing
+\label{creating-dataflow-disable} % temporary label; remove in January 2025
+\subsectionAndLabel{Further customizing flow-sensitive inference}{creating-dataflow-customization}
+
+By default, the Checker Framework assumes that modifications to an object's
+fields do not change its type qualifiers.  This is true for all
+provenance-based type systems (see
+Section~\ref{type-refinement-runtime-tests}), for all value-based type
+systems over immutable values, and for some other type systems.  To
+indicate that \textbf{side effects can change a value's type qualifiers},
+write \<sideEffectsUnrefineAliases = true;> in the type factory
+constructor, before the call to \<this.postInit();>.  Note that this
+setting may lead to large numbers of false positive warnings.  One way to
+reduce the number of false positive warnings would be to improve the side
+effect annotations to be more precise.
+
+In the uncommon case that you wish to \textbf{disable the Checker Framework's
+built-in flow inference} in your checker (this is different than choosing
 not to extend it as described in Section~\ref{creating-dataflow}), put the
 following two lines at the beginning of the constructor for your subtype of
 \refclass{common/basetype}{BaseAnnotatedTypeFactory}:

framework/src/main/java/org/checkerframework/common/delegation/DelegationAnnotatedTypeFactory.java

@@ -0,0 +1,22 @@
+package org.checkerframework.common.delegation;
+
+import java.lang.annotation.Annotation;
+import java.util.Set;
+import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory;
+import org.checkerframework.common.basetype.BaseTypeChecker;
+import org.checkerframework.common.delegation.qual.Delegate;
+
+/** Annotated type factory for the Delegation Checker. */
+public class DelegationAnnotatedTypeFactory extends BaseAnnotatedTypeFactory {
+
+  /** Create the type factory. */
+  public DelegationAnnotatedTypeFactory(BaseTypeChecker checker) {
+    super(checker);
+    this.postInit();
+  }
+
+  @Override
+  protected Set<Class<? extends Annotation>> createSupportedTypeQualifiers() {
+    return getBundledTypeQualifiers(Delegate.class);
+  }
+}

framework/src/main/java/org/checkerframework/common/delegation/DelegationChecker.java

@@ -0,0 +1,20 @@
+package org.checkerframework.common.delegation;
+
+import com.sun.source.tree.*;
+import java.util.*;
+import javax.lang.model.element.*;
+import org.checkerframework.common.basetype.BaseTypeChecker;
+import org.checkerframework.common.delegation.qual.Delegate;
+
+/**
+ * This class enforces checks for the {@link Delegate} annotation.
+ *
+ * <p>It is not a checker for a type system. It enforces the following syntactic checks:
+ *
+ * <ul>
+ *   <li>A class may have up to exactly one field marked with the {@link Delegate} annotation.
+ *   <li>An overridden method's implementation must be exactly a call to the delegate field.
+ *   <li>A class overrides <i>all</i> methods declared in its superclass.
+ * </ul>
+ */
+public class DelegationChecker extends BaseTypeChecker {}