diff --git a/checker-qual/src/main/java/org/checkerframework/common/delegation/qual/Delegate.java b/checker-qual/src/main/java/org/checkerframework/common/delegation/qual/Delegate.java new file mode 100644 index 00000000000..f59642d8a83 --- /dev/null +++ b/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. + * + *
Here is a way that this annotation may be used: + * + *
+ * class MyEnumeration<T> implements Enumeration<T> {
+ * {@literal @}Delegate
+ * private Enumeration<T> e;
+ *
+ * public boolean hasMoreElements() {
+ * return e.hasMoreElements();
+ * }
+ * }
+ *
+ *
+ * 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 {}
diff --git a/checker-qual/src/main/java/org/checkerframework/common/delegation/qual/DelegatorMustOverride.java b/checker-qual/src/main/java/org/checkerframework/common/delegation/qual/DelegatorMustOverride.java
new file mode 100644
index 00000000000..5e89bd2026f
--- /dev/null
+++ b/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 must be overridden in order for a
+ * conditional postcondition to hold for a delegating class.
+ *
+ * Here is a way that this annotation may be used: + * + *
Given a class that declares a method with a postcondition annotation: + * + *
+ * class ArrayListVariant<T> {
+ * {@literal @}EnsuresPresentIf(result = true)
+ * {@literal @}DelegatorMustOverride
+ * public boolean hasMoreElements() {
+ * return e.hasMoreElements();
+ * }
+ * }
+ *
+ *
+ * A delegating client must override the method:
+ *
+ *
+ * class MyArrayListVariant<T> extends ArrayListVariant<T> {
+ *
+ * {@literal @}Delegate
+ * private ArrayListVariant<T> myList;
+ *
+ *
+ * {@literal @}Override
+ * {@literal @}EnsuresPresentIf(result = true)
+ * public boolean hasMoreElements() {
+ * return myList.hasMoreElements();
+ * }
+ * }
+ *
+ *
+ * Otherwise, a warning will be raised.
+ *
+ * @checker_framework.manual #non-empty-checker Non-Empty Checker
+ */
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.METHOD})
+public @interface DelegatorMustOverride {}
diff --git a/framework/src/main/java/org/checkerframework/common/delegation/DelegationAnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/common/delegation/DelegationAnnotatedTypeFactory.java
new file mode 100644
index 00000000000..9d03213f98d
--- /dev/null
+++ b/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 SetIt is not a checker for a type system. It enforces the following syntactic checks: + * + *
A delegate method call must fulfill the following properties: its receiver must be the
+ * current field marked with {@link Delegate} in the class, and the name of the method call must
+ * match that of the enclosing method.
+ *
+ * @param enclosingMethodName the name of the enclosing method
+ * @param delegatedMethodCall the delegated method call
+ * @return true if the given method call is a valid delegate call for the enclosing method
+ */
+ private boolean isValidDelegateCall(
+ Name enclosingMethodName, MethodInvocationTree delegatedMethodCall) {
+ assert delegate != null; // This method should only be invoked when delegate is non-null
+ ExpressionTree methodSelectTree = delegatedMethodCall.getMethodSelect();
+ MemberSelectTree fieldAccessTree = (MemberSelectTree) methodSelectTree;
+ VariableElement delegatedField = TreeUtils.asFieldAccess(fieldAccessTree.getExpression());
+ Name delegatedMethodName = TreeUtils.methodName(delegatedMethodCall);
+ // TODO: is there a better way to check? Comparing names seems fragile.
+ return enclosingMethodName.equals(delegatedMethodName)
+ && delegatedField != null
+ && delegatedField.getSimpleName().equals(delegate.getName());
+ }
+
+ /**
+ * Returns the fields of a class marked with a {@link Delegate} annotation.
+ *
+ * @param tree a class
+ * @return the fields of a class marked with a {@link Delegate} annotation
+ */
+ private List This method is used to identify a possible delegate method call. It will check whether a
+ * method has only one statement (a method invocation or a return statement), and return the
+ * expression that is associated with it. Otherwise, it will return null.
+ *
+ * @param tree the method body
+ * @return the last expression in the method body
+ */
+ private @Nullable MethodInvocationTree getLastExpression(BlockTree tree) {
+ List extends StatementTree> stmts = tree.getStatements();
+ if (stmts.size() != 1) {
+ return null;
+ }
+ StatementTree stmt = stmts.get(0);
+ ExpressionTree lastExprInMethod = null;
+ if (stmt instanceof ExpressionStatementTree) {
+ lastExprInMethod = ((ExpressionStatementTree) stmt).getExpression();
+ } else if (stmt instanceof ReturnTree) {
+ lastExprInMethod = ((ReturnTree) stmt).getExpression();
+ }
+ if (!(lastExprInMethod instanceof MethodInvocationTree)) {
+ return null;
+ }
+ return (MethodInvocationTree) lastExprInMethod;
+ }
+
+ /**
+ * Return true if the last (and only) statement of the block throws an exception of the given
+ * class.
+ *
+ * @param tree a block tree
+ * @param clazz a class of exception (usually {@link UnsupportedOperationException})
+ * @return true if the last and only statement throws an exception of the given class
+ */
+ private boolean hasExceptionalExit(BlockTree tree, Class> clazz) {
+ List extends StatementTree> stmts = tree.getStatements();
+ if (stmts.size() != 1) {
+ return false;
+ }
+ StatementTree lastStmt = stmts.get(0);
+ if (!(lastStmt instanceof ThrowTree)) {
+ return false;
+ }
+ ThrowTree throwStmt = (ThrowTree) lastStmt;
+ AnnotatedTypeMirror throwType = atypeFactory.getAnnotatedType(throwStmt.getExpression());
+ Class> exceptionClass = TypesUtils.getClassFromType(throwType.getUnderlyingType());
+ return exceptionClass.equals(clazz);
+ }
+
+ /**
+ * Validate whether a class overrides all declared methods in its superclass.
+ *
+ * This is a basic implementation that naively checks whether all the superclass methods have
+ * been overridden by the subclass. It is unlikely in practice that a delegating subclass needs to
+ * override all the methods in a superclass for postconditions to hold.
+ *
+ * @param tree a class tree
+ */
+ private void checkSuperClassOverrides(ClassTree tree) {
+ TypeElement classTreeElt = TreeUtils.elementFromDeclaration(tree);
+ if (classTreeElt == null || classTreeElt.getSuperclass() == null) {
+ return;
+ }
+ DeclaredType superClassMirror = (DeclaredType) classTreeElt.getSuperclass();
+ if (superClassMirror == null || superClassMirror.getKind() == TypeKind.NONE) {
+ return;
+ }
+ Set