Initial support for records (#4802)

build.gradle

@@ -405,6 +405,8 @@ 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"))
                 && details.name.endsWith('.java')) {
             javaFiles.add(details.file)
         }

checker/src/main/java/org/checkerframework/checker/initialization/InitializationVisitor.java

@@ -379,6 +379,14 @@ protected void checkFieldsInitialized(
       return;
     }
 
+    // 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)) {
+      return;
+    }
+
     Pair<List<VariableTree>, List<VariableTree>> uninitializedFields =
         atypeFactory.getUninitializedFields(
             store, getCurrentPath(), staticFields, receiverAnnotations);

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

@@ -0,0 +1,34 @@
+package org.checkerframework.checker.test.junit;
+
+import java.io.File;
+import java.util.List;
+import org.checkerframework.checker.nullness.NullnessChecker;
+import org.checkerframework.framework.test.CheckerFrameworkPerDirectoryTest;
+import org.junit.runners.Parameterized.Parameters;
+
+/** JUnit tests for the Nullness checker with records (JDK16+ only). */
+public class NullnessRecordsTest extends CheckerFrameworkPerDirectoryTest {
+
+  /**
+   * Create a NullnessRecordsTest.
+   *
+   * @param testFiles the files containing test code, which will be type-checked
+   */
+  public NullnessRecordsTest(List<File> testFiles) {
+    super(
+        testFiles,
+        NullnessChecker.class,
+        "nullness-records",
+        "-AcheckPurityAnnotations",
+        "-Anomsgtext",
+        "-Xlint:deprecation");
+  }
+
+  @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[] {"nullness-records"};
+    else return new String[] {};
+  }
+}

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

@@ -0,0 +1,33 @@
+package org.checkerframework.checker.test.junit;
+
+import java.io.File;
+import java.util.List;
+import org.checkerframework.framework.test.CheckerFrameworkPerDirectoryTest;
+import org.junit.runners.Parameterized;
+
+/** Tests for stub parsing with records. */
+public class StubparserRecordTest extends CheckerFrameworkPerDirectoryTest {
+
+  /**
+   * Create a StubparserRecordTest.
+   *
+   * @param testFiles the files containing test code, which will be type-checked
+   */
+  public StubparserRecordTest(List<File> testFiles) {
+    super(
+        testFiles,
+        org.checkerframework.checker.nullness.NullnessChecker.class,
+        "stubparser-records",
+        "-Anomsgtext",
+        "-Astubs=tests/stubparser-records",
+        "-AstubWarnIfNotFound");
+  }
+
+  @Parameterized.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[] {"stubparser-records"};
+    else return new String[] {};
+  }
+}

checker/tests/nullness-records/BasicRecord.java

@@ -0,0 +1,14 @@
+import org.checkerframework.checker.nullness.qual.Nullable;
+
+// @below-java16-jdk-skip-test
+public record BasicRecord(String str) {
+
+  public static BasicRecord makeNonNull(String s) {
+    return new BasicRecord(s);
+  }
+
+  public static BasicRecord makeNull(@Nullable String s) {
+    // :: error: argument
+    return new BasicRecord(s);
+  }
+}

checker/tests/nullness-records/BasicRecordCanon.java

@@ -0,0 +1,16 @@
+import org.checkerframework.checker.nullness.qual.Nullable;
+
+// @below-java16-jdk-skip-test
+public record BasicRecordCanon(String str) {
+
+  public static BasicRecordCanon makeNonNull(String s) {
+    return new BasicRecordCanon(s);
+  }
+
+  public static BasicRecordCanon makeNull(@Nullable String s) {
+    // :: error: argument
+    return new BasicRecordCanon(s);
+  }
+
+  public BasicRecordCanon {}
+}

checker/tests/nullness-records/BasicRecordNullable.java

@@ -0,0 +1,31 @@
+import org.checkerframework.checker.nullness.qual.Nullable;
+
+// @below-java16-jdk-skip-test
+public record BasicRecordNullable(@Nullable String str) {
+
+  public static BasicRecordNullable makeNonNull(String s) {
+    return new BasicRecordNullable(s);
+  }
+
+  public static BasicRecordNullable makeNull(@Nullable String s) {
+    return new BasicRecordNullable(s);
+  }
+
+  public @Nullable String getStringFromField() {
+    return str;
+  }
+
+  public @Nullable String getStringFromMethod() {
+    return str();
+  }
+
+  public String getStringFromFieldErr() {
+    // :: error: return
+    return str;
+  }
+
+  public String getStringFromMethodErr() {
+    // :: error: return
+    return str();
+  }
+}

checker/tests/nullness-records/DefaultQualRecord.java

@@ -0,0 +1,62 @@
+import org.checkerframework.checker.nullness.qual.Nullable;
+import org.checkerframework.framework.qual.DefaultQualifier;
+
+class StandardQualClass {
+  // :: error: assignment
+  public static String s = null;
+  // :: error: initialization.static.field.uninitialized
+  public static String u;
+}
+
+@DefaultQualifier(Nullable.class)
+class DefaultQualClass {
+  public static String s = null;
+  public static String u;
+}
+
+interface StandardQualInterface {
+  // :: error: assignment
+  public static String s = null;
+}
+
+@DefaultQualifier(Nullable.class)
+interface DefaultQualInterface {
+  public static String s = null;
+}
+
+enum StandardQualEnum {
+  DUMMY;
+  // :: error: assignment
+  public static String s = null;
+  // :: error: initialization.static.field.uninitialized
+  public static String u;
+}
+
+@DefaultQualifier(Nullable.class)
+enum DefaultQualEnum {
+  DUMMY;
+  public static String s = null;
+  public static String u;
+}
+
+record StandardQualRecord(String m) {
+  // :: error: assignment
+  public static String s = null;
+  // :: error: initialization.static.field.uninitialized
+  public static String u;
+
+  StandardQualRecord {
+    // :: error: assignment
+    m = null;
+  }
+}
+
+@DefaultQualifier(Nullable.class)
+record DefaultQualRecord(String m) {
+  public static String s = null;
+  public static String u;
+
+  DefaultQualRecord {
+    m = null;
+  }
+}

checker/tests/nullness-records/GenericPair.java

@@ -0,0 +1,11 @@
+import org.checkerframework.checker.nullness.qual.Nullable;
+
+// @below-java16-jdk-skip-test
+public record GenericPair<K, V>(K key, V value) {
+
+  public static void foo() {
+    GenericPair<String, @Nullable Integer> p = new GenericPair<>("k", null);
+    // :: error: (dereference.of.nullable)
+    p.value().toString();
+  }
+}

checker/tests/nullness-records/LocalRecords.java

@@ -0,0 +1,12 @@
+import org.checkerframework.checker.nullness.qual.Nullable;
+
+// @below-java16-jdk-skip-test
+public class LocalRecords {
+  public static void foo() {
+    record L(String key, @Nullable Integer value) {}
+    L a = new L("one", 1);
+    L b = new L("i", null);
+    // :: error: (argument)
+    L c = new L(null, 6);
+  }
+}

checker/tests/nullness-records/NestedRecordTest.java

@@ -0,0 +1,98 @@
+import org.checkerframework.checker.nullness.qual.NonNull;
+import org.checkerframework.checker.nullness.qual.Nullable;
+
+// @below-java16-jdk-skip-test
+
+public class NestedRecordTest {
+
+  static @NonNull String nn = "foo";
+  static @Nullable String nble = null;
+  static @NonNull String nn2 = "foo";
+  static @Nullable String nble2 = null;
+
+  public static class Nested {
+    public record NPerson(String familyName, @Nullable String maidenName) {}
+
+    void nclient() {
+      Nested.NPerson np1 = new Nested.NPerson(nn, nn);
+      Nested.NPerson np2 = new Nested.NPerson(nn, nble);
+      // :: error: argument
+      Nested.NPerson np3 = new Nested.NPerson(nble, nn);
+      // :: error: argument
+      Nested.NPerson np4 = new Nested.NPerson(nble, nble);
+      Inner.IPerson ip1 = new Inner.IPerson(nn, nn);
+      Inner.IPerson ip2 = new Inner.IPerson(nn, nble);
+      // :: error: argument
+      Inner.IPerson ip3 = new Inner.IPerson(nble, nn);
+      // :: error: argument
+      Inner.IPerson ip4 = new Inner.IPerson(nble, nble);
+
+      nn2 = np2.familyName();
+      nble2 = np2.familyName();
+      // :: error: assignment
+      nn2 = np2.maidenName();
+      nble2 = np2.maidenName();
+      nn2 = ip2.familyName();
+      nble2 = ip2.familyName();
+      // :: error: assignment
+      nn2 = ip2.maidenName();
+      nble2 = ip2.maidenName();
+    }
+  }
+
+  public class Inner {
+    public record IPerson(String familyName, @Nullable String maidenName) {}
+
+    void iclient() {
+      Nested.NPerson np1 = new Nested.NPerson(nn, nn);
+      Nested.NPerson np2 = new Nested.NPerson(nn, nble);
+      // :: error: argument
+      Nested.NPerson np3 = new Nested.NPerson(nble, nn);
+      // :: error: argument
+      Nested.NPerson np4 = new Nested.NPerson(nble, nble);
+      Inner.IPerson ip1 = new Inner.IPerson(nn, nn);
+      Inner.IPerson ip2 = new Inner.IPerson(nn, nble);
+      // :: error: argument
+      Inner.IPerson ip3 = new Inner.IPerson(nble, nn);
+      // :: error: argument
+      Inner.IPerson ip4 = new Inner.IPerson(nble, nble);
+
+      nn2 = np2.familyName();
+      nble2 = np2.familyName();
+      // :: error: assignment
+      nn2 = np2.maidenName();
+      nble2 = np2.maidenName();
+      nn2 = ip2.familyName();
+      nble2 = ip2.familyName();
+      // :: error: assignment
+      nn2 = ip2.maidenName();
+      nble2 = ip2.maidenName();
+    }
+  }
+
+  void client() {
+    Nested.NPerson np1 = new Nested.NPerson(nn, nn);
+    Nested.NPerson np2 = new Nested.NPerson(nn, nble);
+    // :: error: argument
+    Nested.NPerson np3 = new Nested.NPerson(nble, nn);
+    // :: error: argument
+    Nested.NPerson np4 = new Nested.NPerson(nble, nble);
+    Inner.IPerson ip1 = new Inner.IPerson(nn, nn);
+    Inner.IPerson ip2 = new Inner.IPerson(nn, nble);
+    // :: error: argument
+    Inner.IPerson ip3 = new Inner.IPerson(nble, nn);
+    // :: error: argument
+    Inner.IPerson ip4 = new Inner.IPerson(nble, nble);
+
+    nn2 = np2.familyName();
+    nble2 = np2.familyName();
+    // :: error: assignment
+    nn2 = np2.maidenName();
+    nble2 = np2.maidenName();
+    nn2 = ip2.familyName();
+    nble2 = ip2.familyName();
+    // :: error: assignment
+    nn2 = ip2.maidenName();
+    nble2 = ip2.maidenName();
+  }
+}