Finish records support

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/main/java/org/checkerframework/checker/initialization/InitializationVisitor.java

@@ -379,11 +379,11 @@ protected void checkFieldsInitialized(
       return;
     }
 
-    // Canonical record constructors do not generate visible assignments in the source,
+    // Compact canonical record constructors do not generate visible assignments in the source,
     // but by definition they assign to all the record's fields so we don't need to
     // check for uninitialized fields in them:
     if (node.getKind() == Tree.Kind.METHOD
-        && TreeUtils.isCanonicalRecordConstructor((MethodTree) node)) {
+        && TreeUtils.isCompactCanonicalRecordConstructor((MethodTree) node)) {
       return;
     }
 

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 an expression 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,78 @@
+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();
+    MemberSelectTree[] memberSelectTrees =
+        enclosingMemberSel == null
+            ? new MemberSelectTree[] {null}
+            : new MemberSelectTree[] {enclosingMemberSel, null};
+
+    for (MemberSelectTree memberSel : memberSelectTrees) {
+      final ExpressionTree tree;
+      final Element elem;
+      if (memberSel == null) {
+        tree = node;
+        elem = TreeUtils.elementFromUse(node);
+      } else {
+        tree = memberSel;
+        elem = TreeUtils.elementFromUse(memberSel);
+      }
+
+      if (elem == null || (!elem.getKind().isField() && elem.getKind() != ElementKind.PARAMETER)) {
+        continue;
+      }
+
+      if (atypeFactory.getDeclAnnotation(elem, DisbarUse.class) != null) {
+        checker.reportError(tree, "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,7 @@
+package org.checkerframework.checker.testchecker.disbaruse.qual;
+
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Target;
+
+@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/ajava/ExpectedTreesVisitor.java

@@ -133,11 +133,12 @@ public void defaultAction(Tree node) {
         if (TreeUtils.isAutoGeneratedRecordMember(member)) {
           member.accept(removeAllVisitor, null);
         } else {
-          // If the user declares a canonical constructor, javac will automatically fill in the
+          // If the user declares a compact canonical constructor, javac will automatically fill in
+          // the
           // parameters.  These trees also don't have a match:
           if (member.getKind() == Tree.Kind.METHOD) {
             MethodTree methodTree = (MethodTree) member;
-            if (TreeUtils.isCanonicalRecordConstructor(methodTree)) {
+            if (TreeUtils.isCompactCanonicalRecordConstructor(methodTree)) {
               for (VariableTree canonicalParameter : methodTree.getParameters()) {
                 canonicalParameter.accept(removeAllVisitor, null);
               }

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

@@ -390,6 +390,42 @@ public Set<AnnotationMirror> getDeclAnnotations(Element elt) {
     String eltName = ElementUtils.getQualifiedName(elt);
     if (annotationFileAnnos.declAnnos.containsKey(eltName)) {
       return annotationFileAnnos.declAnnos.get(eltName);
+    } else {
+      Element enclosingType = null;
+      boolean canTransferAnnotationsToSameName;
+      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;
+          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();
   }