Finish records support (#4871)

* Allow method annotations on compact constructors in stubs
* Support automatic transfer from declaration annotations on record components in stubs to the corresponding field, method, and compact canonical constructor parameter. (Outside stubs this is done automatically by javac.)

build.gradle

@@ -405,8 +405,7 @@ List<String> getJavaFilesToFormat(projectName) {
                 && !details.path.contains("calledmethods-delomboked")
                 && !details.path.contains("returnsreceiverdelomboked")
                 && !details.path.contains("build")
-                && (isJava16 || !details.path.contains("nullness-records"))
-                && (isJava16 || !details.path.contains("stubparser-records"))
+                && (isJava16 || !details.path.contains("-records"))
                 && details.name.endsWith('.java')) {
             javaFiles.add(details.file)
         }

checker/src/test/java/org/checkerframework/checker/test/junit/DisbarUseTest.java

@@ -0,0 +1,33 @@
+package org.checkerframework.checker.test.junit;
+
+import java.io.File;
+import java.util.List;
+import org.checkerframework.checker.testchecker.disbaruse.DisbarUseChecker;
+import org.checkerframework.framework.test.CheckerFrameworkPerDirectoryTest;
+import org.junit.runners.Parameterized.Parameters;
+
+public class DisbarUseTest extends CheckerFrameworkPerDirectoryTest {
+
+  /**
+   * Create a DisbarUseTest.
+   *
+   * @param testFiles the files containing test code, which will be type-checked
+   */
+  public DisbarUseTest(List<File> testFiles) {
+    super(
+        testFiles,
+        DisbarUseChecker.class,
+        "disbaruse-records",
+        "-Anomsgtext",
+        "-Astubs=tests/disbaruse-records",
+        "-AstubWarnIfNotFound");
+  }
+
+  @Parameters
+  public static String[] getTestDirs() {
+    // Check for JDK 16+ without using a library:
+    if (System.getProperty("java.version").matches("^(1[6-9]|[2-9][0-9])\\..*"))
+      return new String[] {"disbaruse-records"};
+    else return new String[] {};
+  }
+}

checker/src/test/java/org/checkerframework/checker/test/junit/LockTest.java

@@ -18,6 +18,9 @@ public LockTest(List<File> testFiles) {
 
   @Parameters
   public static String[] getTestDirs() {
-    return new String[] {"lock", "all-systems"};
+    // Check for JDK 16+ without using a library:
+    if (System.getProperty("java.version").matches("^(1[6-9]|[2-9][0-9])\\..*"))
+      return new String[] {"lock", "lock-records", "all-systems"};
+    else return new String[] {"lock", "all-systems"};
   }
 }

checker/src/test/java/org/checkerframework/checker/testchecker/disbaruse/DisbarUseChecker.java

@@ -0,0 +1,9 @@
+package org.checkerframework.checker.testchecker.disbaruse;
+
+import org.checkerframework.common.basetype.BaseTypeChecker;
+
+/**
+ * A checker that issues a "disbar.use" error at any use of fields, methods or parameters whose type
+ * is {@code @DisbarUse}.
+ */
+public class DisbarUseChecker extends BaseTypeChecker {}

checker/src/test/java/org/checkerframework/checker/testchecker/disbaruse/DisbarUseTypeFactory.java

@@ -0,0 +1,22 @@
+package org.checkerframework.checker.testchecker.disbaruse;
+
+import java.lang.annotation.Annotation;
+import java.util.Arrays;
+import java.util.LinkedHashSet;
+import java.util.Set;
+import org.checkerframework.checker.testchecker.disbaruse.qual.DisbarUseBottom;
+import org.checkerframework.checker.testchecker.disbaruse.qual.DisbarUseTop;
+import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory;
+import org.checkerframework.common.basetype.BaseTypeChecker;
+
+public class DisbarUseTypeFactory extends BaseAnnotatedTypeFactory {
+  public DisbarUseTypeFactory(BaseTypeChecker checker) {
+    super(checker);
+    postInit();
+  }
+
+  @Override
+  protected Set<Class<? extends Annotation>> createSupportedTypeQualifiers() {
+    return new LinkedHashSet<>(Arrays.asList(DisbarUseTop.class, DisbarUseBottom.class));
+  }
+}

checker/src/test/java/org/checkerframework/checker/testchecker/disbaruse/DisbarUseVisitor.java

@@ -0,0 +1,69 @@
+package org.checkerframework.checker.testchecker.disbaruse;
+
+import com.sun.source.tree.ExpressionTree;
+import com.sun.source.tree.IdentifierTree;
+import com.sun.source.tree.MemberSelectTree;
+import com.sun.source.tree.MethodInvocationTree;
+import com.sun.source.tree.NewClassTree;
+import javax.lang.model.element.Element;
+import javax.lang.model.element.ElementKind;
+import javax.lang.model.element.ExecutableElement;
+import org.checkerframework.checker.testchecker.disbaruse.qual.DisbarUse;
+import org.checkerframework.common.basetype.BaseTypeChecker;
+import org.checkerframework.common.basetype.BaseTypeVisitor;
+import org.checkerframework.javacutil.TreeUtils;
+
+public class DisbarUseVisitor extends BaseTypeVisitor<DisbarUseTypeFactory> {
+  public DisbarUseVisitor(BaseTypeChecker checker) {
+    super(checker);
+  }
+
+  protected DisbarUseVisitor(BaseTypeChecker checker, DisbarUseTypeFactory typeFactory) {
+    super(checker, typeFactory);
+  }
+
+  @Override
+  protected DisbarUseTypeFactory createTypeFactory() {
+    return new DisbarUseTypeFactory(checker);
+  }
+
+  @Override
+  public Void visitMethodInvocation(MethodInvocationTree node, Void p) {
+    ExecutableElement methodElt = TreeUtils.elementFromUse(node);
+    if (methodElt != null && atypeFactory.getDeclAnnotation(methodElt, DisbarUse.class) != null) {
+      checker.reportError(node, "disbar.use");
+    }
+    return super.visitMethodInvocation(node, p);
+  }
+
+  @Override
+  public Void visitNewClass(NewClassTree node, Void p) {
+    ExecutableElement consElt = TreeUtils.elementFromUse(node);
+    if (consElt != null && atypeFactory.getDeclAnnotation(consElt, DisbarUse.class) != null) {
+      checker.reportError(node, "disbar.use");
+    }
+    return super.visitNewClass(node, p);
+  }
+
+  @Override
+  public Void visitIdentifier(IdentifierTree node, Void p) {
+    MemberSelectTree enclosingMemberSel = enclosingMemberSelect();
+    ExpressionTree[] expressionTrees =
+        enclosingMemberSel == null
+            ? new ExpressionTree[] {node}
+            : new ExpressionTree[] {enclosingMemberSel, node};
+
+    for (ExpressionTree memberSel : expressionTrees) {
+      final Element elem = TreeUtils.elementFromUse(memberSel);
+
+      // We only issue errors for variables that are fields or parameters:
+      if (elem != null && (elem.getKind().isField() || elem.getKind() == ElementKind.PARAMETER)) {
+        if (atypeFactory.getDeclAnnotation(elem, DisbarUse.class) != null) {
+          checker.reportError(memberSel, "disbar.use");
+        }
+      }
+    }
+
+    return super.visitIdentifier(node, p);
+  }
+}

checker/src/test/java/org/checkerframework/checker/testchecker/disbaruse/messages.properties

@@ -0,0 +1 @@
+disbar.use=Use of this element is disbarred

checker/src/test/java/org/checkerframework/checker/testchecker/disbaruse/qual/DisbarUse.java

@@ -0,0 +1,8 @@
+package org.checkerframework.checker.testchecker.disbaruse.qual;
+
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Target;
+
+/** The Disbar Use Checker isses a warning when an expression of this type is used. */
+@Target({ElementType.METHOD, ElementType.CONSTRUCTOR, ElementType.FIELD, ElementType.PARAMETER})
+public @interface DisbarUse {}

checker/src/test/java/org/checkerframework/checker/testchecker/disbaruse/qual/DisbarUseBottom.java

@@ -0,0 +1,12 @@
+package org.checkerframework.checker.testchecker.disbaruse.qual;
+
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Target;
+import org.checkerframework.framework.qual.DefaultFor;
+import org.checkerframework.framework.qual.SubtypeOf;
+import org.checkerframework.framework.qual.TypeUseLocation;
+
+@DefaultFor(TypeUseLocation.LOWER_BOUND)
+@SubtypeOf(DisbarUseTop.class)
+@Target({ElementType.TYPE_USE})
+public @interface DisbarUseBottom {}

checker/src/test/java/org/checkerframework/checker/testchecker/disbaruse/qual/DisbarUseTop.java

@@ -0,0 +1,11 @@
+package org.checkerframework.checker.testchecker.disbaruse.qual;
+
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Target;
+import org.checkerframework.framework.qual.DefaultQualifierInHierarchy;
+import org.checkerframework.framework.qual.SubtypeOf;
+
+@Target({ElementType.TYPE_USE})
+@SubtypeOf({})
+@DefaultQualifierInHierarchy
+public @interface DisbarUseTop {}

checker/tests/disbaruse-records/DisbarredClass.java

@@ -0,0 +1,41 @@
+import org.checkerframework.checker.testchecker.disbaruse.qual.DisbarUse;
+
+class DisbarredClass {
+
+  @DisbarUse String barred;
+  String fine;
+
+  DisbarredClass() {}
+
+  @DisbarUse
+  DisbarredClass(String param) {}
+
+  DisbarredClass(@DisbarUse Integer param) {}
+
+  DisbarredClass(@DisbarUse Long param) {
+    // :: error: (disbar.use)
+    param = 7L;
+    // :: error: (disbar.use)
+    param.toString();
+  }
+
+  @DisbarUse
+  void disbarredMethod() {}
+
+  void invalid() {
+    // :: error: (disbar.use)
+    disbarredMethod();
+    // :: error: (disbar.use)
+    new DisbarredClass("");
+    // :: error: (disbar.use)
+    barred = "";
+    // :: error: (disbar.use)
+    int x = barred.length();
+  }
+
+  void valid() {
+    new DisbarredClass();
+    fine = "";
+    int x = fine.length();
+  }
+}

checker/tests/disbaruse-records/DisbarredRecord.java

@@ -0,0 +1,21 @@
+import org.checkerframework.checker.testchecker.disbaruse.qual.DisbarUse;
+
+record DisbarredRecord(@DisbarUse String barred, String fine) {
+
+  DisbarredRecord {
+    // :: error: (disbar.use)
+    int x = barred.length();
+  }
+
+  void invalid() {
+    // :: error: (disbar.use)
+    barred();
+    // :: error: (disbar.use)
+    int x = barred.length();
+  }
+
+  void valid() {
+    fine();
+    int x = fine.length();
+  }
+}

checker/tests/disbaruse-records/DisbarredRecordByStubs.java

@@ -0,0 +1,19 @@
+record DisbarredRecordByStubs(String barred, String fine) {
+
+  DisbarredRecordByStubs {
+    // :: error: (disbar.use)
+    int x = barred.length();
+  }
+
+  void invalid() {
+    // :: error: (disbar.use)
+    barred();
+    // :: error: (disbar.use)
+    int x = barred.length();
+  }
+
+  void valid() {
+    fine();
+    int x = fine.length();
+  }
+}

checker/tests/disbaruse-records/DisbarredRecordByStubs2.java

@@ -0,0 +1,22 @@
+record DisbarredRecordByStubs2(String barred, String fine) {
+
+  // Annotation isn't copied to explicitly declared constructor parameters:
+  DisbarredRecordByStubs2(String barred, String fine) {
+    int x = barred.length();
+    // :: error: (disbar.use)
+    this.barred = "";
+    this.fine = fine;
+  }
+
+  void invalid() {
+    // :: error: (disbar.use)
+    barred();
+    // :: error: (disbar.use)
+    int x = barred.length();
+  }
+
+  void valid() {
+    fine();
+    int x = fine.length();
+  }
+}

checker/tests/disbaruse-records/disbar.astub

@@ -0,0 +1,6 @@
+import org.checkerframework.checker.testchecker.disbaruse.qual.DisbarUse;
+
+record DisbarredRecordByStubs(@DisbarUse String barred, String fine) {
+}
+record DisbarredRecordByStubs2(@DisbarUse String barred, String fine) {
+}

checker/tests/lock-records/LockRecord.java

@@ -0,0 +1,11 @@
+import java.util.concurrent.locks.ReentrantLock;
+import org.checkerframework.checker.lock.qual.LockingFree;
+
+public record LockRecord(String s, ReentrantLock lock) {
+  @LockingFree
+  // :: error: (method.guarantee.violated)
+  public LockRecord {
+    // :: error: (method.guarantee.violated)
+    lock.lock();
+  }
+}

framework/src/main/java/org/checkerframework/framework/stub/AnnotationFileElementTypes.java

@@ -390,6 +390,44 @@ public Set<AnnotationMirror> getDeclAnnotations(Element elt) {
     String eltName = ElementUtils.getQualifiedName(elt);
     if (annotationFileAnnos.declAnnos.containsKey(eltName)) {
       return annotationFileAnnos.declAnnos.get(eltName);
+    } else {
+      // Handle annotations on record declarations.
+      boolean canTransferAnnotationsToSameName;
+      Element enclosingType; // Do nothing unless this element is a record.
+      switch (elt.getKind()) {
+        case METHOD:
+          // Annotations transfer to zero-arg accessor methods of same name:
+          canTransferAnnotationsToSameName = ((ExecutableElement) elt).getParameters().isEmpty();
+          enclosingType = elt.getEnclosingElement();
+          break;
+        case FIELD:
+          // Annotations transfer to fields of same name:
+          canTransferAnnotationsToSameName = true;
+          enclosingType = elt.getEnclosingElement();
+          break;
+        case PARAMETER:
+          // Annotations transfer to compact canonical constructor parameter of same name:
+          canTransferAnnotationsToSameName =
+              ElementUtils.isCompactCanonicalRecordConstructor(elt.getEnclosingElement())
+                  && elt.getEnclosingElement().getKind() == ElementKind.CONSTRUCTOR;
+          enclosingType = elt.getEnclosingElement().getEnclosingElement();
+          break;
+        default:
+          canTransferAnnotationsToSameName = false;
+          enclosingType = null;
+          break;
+      }
+
+      if (canTransferAnnotationsToSameName && enclosingType.getKind().toString().equals("RECORD")) {
+        AnnotationFileParser.RecordStub recordStub =
+            annotationFileAnnos.records.get(enclosingType.getSimpleName().toString());
+        if (recordStub != null
+            && recordStub.componentsByName.containsKey(elt.getSimpleName().toString())) {
+          RecordComponentStub recordComponentStub =
+              recordStub.componentsByName.get(elt.getSimpleName().toString());
+          return recordComponentStub.getAnnotationsForTarget(elt.getKind());
+        }
+      }
     }
     return Collections.emptySet();
   }