Add ViewpointAdapter (#266)

Co-authored-by: Mier Ta <topnessman@sina.com>
Co-authored-by: Lian Sun <57457122+lnsun@users.noreply.github.com>
Co-authored-by: xingweitian <13183370+xingweitian@users.noreply.github.com>
Co-authored-by: xingweitian <xingweitian@gmail.com>
Co-authored-by: d367wang <d367wang@uwaterloo.ca>
Co-authored-by: Werner Dietl <wdietl@gmail.com>

docs/CHANGELOG.md

@@ -5,6 +5,11 @@ Version 3.22.2-eisop1 (July ?, 2022)
 
 **Implementation details:**
 
+Added support for viewpoint adaptation of types via the added
+ViewpointAdapter interface. This support is experimental and the API
+will change, in particular if the feature is fully integrated with
+the DependentTypesHelper.
+
 Method `AnnotatedTypeFactory.getDeclAnnotations` now returns the
 annotations for a package element. Previously, it returned an empty set
 when parsing another file. (eisop#270)

framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java

@@ -270,6 +270,9 @@ public class AnnotatedTypeFactory implements AnnotationProvider {
     private final @Nullable WholeProgramInference wholeProgramInference;
     */
 
+    /** Viewpoint adapter used to perform viewpoint adaptation or null */
+    protected @Nullable ViewpointAdapter viewpointAdapter;
+
     /**
      * This formatter is used for converting AnnotatedTypeMirrors to Strings. This formatter will be
      * used by all AnnotatedTypeMirrors created by this factory in their toString methods.
@@ -755,6 +758,7 @@ protected void postInit() {
         this.typeHierarchy = createTypeHierarchy();
         this.typeVarSubstitutor = createTypeVariableSubstitutor();
         this.typeArgumentInference = createTypeArgumentInference();
+        this.viewpointAdapter = createViewpointAdapter();
         this.qualifierUpperBounds = createQualifierUpperBounds();
 
         // TODO: is this the best location for declaring this alias?
@@ -1037,6 +1041,16 @@ public final TypeHierarchy getTypeHierarchy() {
         return typeHierarchy;
     }
 
+    /**
+     * Factory method to create a ViewpointAdapter. Subclasses should implement and instantiate a
+     * ViewpointAdapter subclass if viewpoint adaptation is needed for a type system.
+     *
+     * @return viewpoint adapter to perform viewpoint adaptation or null
+     */
+    protected @Nullable ViewpointAdapter createViewpointAdapter() {
+        return null;
+    }
+
     /**
      * TypeVariableSubstitutor provides a method to replace type parameters with their arguments.
      */
@@ -1805,6 +1819,10 @@ public void postAsMemberOf(
             addAnnotationFromFieldInvariant(type, owner, (VariableElement) element);
         }
         addComputedTypeAnnotations(element, type);
+
+        if (viewpointAdapter != null && type.getKind() != TypeKind.EXECUTABLE) {
+            viewpointAdapter.viewpointAdaptMember(owner, element, type);
+        }
     }
 
     /**
@@ -1999,6 +2017,10 @@ public List<AnnotatedTypeParameterBounds> typeVariablesFromUse(
                     typeVarSubstitutor.substitute(typeParamToTypeArg, atv.getLowerBound());
             res.add(new AnnotatedTypeParameterBounds(upper, lower));
         }
+
+        if (viewpointAdapter != null) {
+            viewpointAdapter.viewpointAdaptTypeParameterBounds(type, res);
+        }
         return res;
     }
 
@@ -2319,14 +2341,18 @@ public ParameterizedExecutableType methodFromUse(MethodInvocationTree tree) {
      */
     public ParameterizedExecutableType methodFromUse(
             ExpressionTree tree, ExecutableElement methodElt, AnnotatedTypeMirror receiverType) {
-
         AnnotatedExecutableType memberTypeWithoutOverrides =
                 getAnnotatedType(methodElt); // get unsubstituted type
         AnnotatedExecutableType memberTypeWithOverrides =
                 applyFakeOverrides(receiverType, methodElt, memberTypeWithoutOverrides);
         memberTypeWithOverrides = applyRecordTypesToAccessors(methodElt, memberTypeWithOverrides);
         methodFromUsePreSubstitution(tree, memberTypeWithOverrides);
 
+        // Perform viewpoint adaption before type argument substitution.
+        if (viewpointAdapter != null) {
+            viewpointAdapter.viewpointAdaptMethod(receiverType, methodElt, memberTypeWithOverrides);
+        }
+
         AnnotatedExecutableType methodType =
                 AnnotatedTypes.asMemberOf(
                         types, this, receiverType, methodElt, memberTypeWithOverrides);
@@ -2647,7 +2673,6 @@ protected AnnotatedTypeMirror getIterableElementType(
      *     (inferred) type arguments
      */
     public ParameterizedExecutableType constructorFromUse(NewClassTree tree) {
-
         // Get the annotations written on the new class tree.
         AnnotatedDeclaredType type =
                 (AnnotatedDeclaredType) toAnnotatedType(TreeUtils.typeOf(tree), false);
@@ -2676,6 +2701,10 @@ public ParameterizedExecutableType constructorFromUse(NewClassTree tree) {
         AnnotatedExecutableType con = getAnnotatedType(ctor); // get unsubstituted type
         constructorFromUsePreSubstitution(tree, con);
 
+        if (viewpointAdapter != null) {
+            viewpointAdapter.viewpointAdaptConstructor(type, ctor, con);
+        }
+
         if (tree.getClassBody() != null) {
             // Because the anonymous constructor can't have explicit annotations on its parameters,
             // they are copied from the super constructor invoked in the anonymous constructor. To
@@ -2687,6 +2716,7 @@ public ParameterizedExecutableType constructorFromUse(NewClassTree tree) {
             AnnotatedExecutableType superCon =
                     getAnnotatedType(TreeUtils.getSuperConstructor(tree));
             constructorFromUsePreSubstitution(tree, superCon);
+            // no viewpoint adaptation needed for super invocation
             superCon =
                     AnnotatedTypes.asMemberOf(types, this, type, superCon.getElement(), superCon);
             if (superCon.getParameterTypes().size() == con.getParameterTypes().size()) {

framework/src/main/java/org/checkerframework/framework/type/ViewpointAdapter.java

@@ -0,0 +1,74 @@
+package org.checkerframework.framework.type;
+
+import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedExecutableType;
+
+import java.util.List;
+
+import javax.lang.model.element.Element;
+import javax.lang.model.element.ExecutableElement;
+
+/**
+ * A viewpoint adapter.
+ *
+ * <p>Viewpoint adaptation applies to member/field accesses, constructor invocations, method
+ * invocations, and type parameter bound instantiations.
+ */
+public interface ViewpointAdapter {
+
+    /**
+     * Viewpoint adapts a member/field access.
+     *
+     * <p>Developer notes: When this method is invoked on a member/field with a type given by a type
+     * parameter, the type arguments are correctly substituted, and memberType is already in a good
+     * shape. Only annotations on the memberType should be replaced by the viewpoint adapted ones.
+     *
+     * @param receiverType receiver type through which the member/field is accessed.
+     * @param memberElement element of the accessed member/field.
+     * @param memberType accessed type of the member/field. After the method returns, it will be
+     *     mutated to the viewpoint adapted result.
+     */
+    void viewpointAdaptMember(
+            AnnotatedTypeMirror receiverType,
+            Element memberElement,
+            AnnotatedTypeMirror memberType);
+
+    /**
+     * Viewpoint adapts a constructor invocation. Takes an unsubstituted method invocation type and
+     * performs the viewpoint adaption in place, modifying the parameter.
+     *
+     * @param receiverType receiver type through which a constructor is invoked.
+     * @param constructorElt element of the invoked constructor.
+     * @param constructorType invoked type of the constructor with type variables not substituted.
+     *     After the method returns, it will be mutated to the viewpoint adapted constructor type.
+     */
+    void viewpointAdaptConstructor(
+            AnnotatedTypeMirror receiverType,
+            ExecutableElement constructorElt,
+            AnnotatedExecutableType constructorType);
+
+    /**
+     * Viewpoint adapts a method invocation. Takes an unsubstituted method invocation type and
+     * performs the viewpoint adaption in place, modifying the parameter.
+     *
+     * @param receiverType receiver type through which a method is invoked.
+     * @param methodElt element of the invoked method. Only used to determine whether this type
+     *     should be viewpoint adapted
+     * @param methodType invoked type of the method with type variables not substituted. After the
+     *     method returns, it will be mutated to the viewpoint adapted method type.
+     */
+    void viewpointAdaptMethod(
+            AnnotatedTypeMirror receiverType,
+            ExecutableElement methodElt,
+            AnnotatedExecutableType methodType);
+
+    /**
+     * Viewpoint adapts a type parameter bound when being instantiated.
+     *
+     * @param receiverType receiver type through which the type parameter is instantiated.
+     * @param typeParameterBounds a list of type parameter bounds. After the method returns, it will
+     *     be mutated to the viewpoint adapted type parameter bounds.
+     */
+    void viewpointAdaptTypeParameterBounds(
+            AnnotatedTypeMirror receiverType,
+            List<AnnotatedTypeParameterBounds> typeParameterBounds);
+}

framework/src/test/java/org/checkerframework/framework/test/junit/ViewpointTestCheckerTest.java

@@ -0,0 +1,20 @@
+package tests;
+
+import org.checkerframework.framework.test.CheckerFrameworkPerDirectoryTest;
+import org.junit.runners.Parameterized;
+
+import java.io.File;
+import java.util.List;
+
+public class ViewpointTestCheckerTest extends CheckerFrameworkPerDirectoryTest {
+
+    /** @param testFiles the files containing test code, which will be type-checked */
+    public ViewpointTestCheckerTest(List<File> testFiles) {
+        super(testFiles, viewpointtest.ViewpointTestChecker.class, "viewpointtest");
+    }
+
+    @Parameterized.Parameters
+    public static String[] getTestDirs() {
+        return new String[] {"viewpointtest"};
+    }
+}

framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java

@@ -0,0 +1,39 @@
+package viewpointtest;
+
+import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory;
+import org.checkerframework.common.basetype.BaseTypeChecker;
+import org.checkerframework.framework.type.AbstractViewpointAdapter;
+
+import viewpointtest.quals.A;
+import viewpointtest.quals.B;
+import viewpointtest.quals.Bottom;
+import viewpointtest.quals.PolyVP;
+import viewpointtest.quals.ReceiverDependentQual;
+import viewpointtest.quals.Top;
+
+import java.lang.annotation.Annotation;
+import java.util.Set;
+
+public class ViewpointTestAnnotatedTypeFactory extends BaseAnnotatedTypeFactory {
+
+    public ViewpointTestAnnotatedTypeFactory(BaseTypeChecker checker) {
+        super(checker);
+        this.postInit();
+    }
+
+    @Override
+    protected Set<Class<? extends Annotation>> createSupportedTypeQualifiers() {
+        return getBundledTypeQualifiers(
+                A.class,
+                B.class,
+                Bottom.class,
+                PolyVP.class,
+                ReceiverDependentQual.class,
+                Top.class);
+    }
+
+    @Override
+    protected AbstractViewpointAdapter createViewpointAdapter() {
+        return new ViewpointTestViewpointAdapter(this);
+    }
+}

framework/src/test/java/viewpointtest/ViewpointTestChecker.java

@@ -0,0 +1,5 @@
+package viewpointtest;
+
+import org.checkerframework.common.basetype.BaseTypeChecker;
+
+public class ViewpointTestChecker extends BaseTypeChecker {}

framework/src/test/java/viewpointtest/ViewpointTestViewpointAdapter.java

@@ -0,0 +1,45 @@
+package viewpointtest;
+
+import org.checkerframework.framework.type.AbstractViewpointAdapter;
+import org.checkerframework.framework.type.AnnotatedTypeFactory;
+import org.checkerframework.framework.type.AnnotatedTypeMirror;
+import org.checkerframework.javacutil.AnnotationBuilder;
+import org.checkerframework.javacutil.AnnotationUtils;
+
+import viewpointtest.quals.ReceiverDependentQual;
+import viewpointtest.quals.Top;
+
+import javax.lang.model.element.AnnotationMirror;
+
+public class ViewpointTestViewpointAdapter extends AbstractViewpointAdapter {
+
+    private final AnnotationMirror TOP, RECEIVERDEPENDENTQUAL;
+
+    /**
+     * The class constructor.
+     *
+     * @param atypeFactory
+     */
+    public ViewpointTestViewpointAdapter(AnnotatedTypeFactory atypeFactory) {
+        super(atypeFactory);
+        TOP = AnnotationBuilder.fromClass(atypeFactory.getElementUtils(), Top.class);
+        RECEIVERDEPENDENTQUAL =
+                AnnotationBuilder.fromClass(
+                        atypeFactory.getElementUtils(), ReceiverDependentQual.class);
+    }
+
+    @Override
+    protected AnnotationMirror extractAnnotationMirror(AnnotatedTypeMirror atm) {
+        return atm.getAnnotationInHierarchy(TOP);
+    }
+
+    @Override
+    protected AnnotationMirror combineAnnotationWithAnnotation(
+            AnnotationMirror receiverAnnotation, AnnotationMirror declaredAnnotation) {
+
+        if (AnnotationUtils.areSame(declaredAnnotation, RECEIVERDEPENDENTQUAL)) {
+            return receiverAnnotation;
+        }
+        return declaredAnnotation;
+    }
+}

framework/src/test/java/viewpointtest/quals/A.java

@@ -0,0 +1,15 @@
+package viewpointtest.quals;
+
+import org.checkerframework.framework.qual.SubtypeOf;
+
+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;
+
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
+@SubtypeOf({Top.class})
+public @interface A {}

framework/src/test/java/viewpointtest/quals/B.java

@@ -0,0 +1,15 @@
+package viewpointtest.quals;
+
+import org.checkerframework.framework.qual.SubtypeOf;
+
+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;
+
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
+@SubtypeOf({Top.class})
+public @interface B {}

framework/src/test/java/viewpointtest/quals/Bottom.java

@@ -0,0 +1,18 @@
+package viewpointtest.quals;
+
+import org.checkerframework.framework.qual.DefaultFor;
+import org.checkerframework.framework.qual.SubtypeOf;
+import org.checkerframework.framework.qual.TypeUseLocation;
+
+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;
+
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
+@SubtypeOf({A.class, B.class, ReceiverDependentQual.class})
+@DefaultFor(TypeUseLocation.LOWER_BOUND)
+public @interface Bottom {}

framework/src/test/java/viewpointtest/quals/PolyVP.java

@@ -0,0 +1,15 @@
+package viewpointtest.quals;
+
+import org.checkerframework.framework.qual.PolymorphicQualifier;
+
+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;
+
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
+@PolymorphicQualifier(Top.class)
+public @interface PolyVP {}

framework/src/test/java/viewpointtest/quals/ReceiverDependentQual.java

@@ -0,0 +1,15 @@
+package viewpointtest.quals;
+
+import org.checkerframework.framework.qual.SubtypeOf;
+
+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;
+
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
+@SubtypeOf({Top.class})
+public @interface ReceiverDependentQual {}