Create gradle project

.gitattributes

@@ -0,0 +1,9 @@
+#
+# https://help.github.com/articles/dealing-with-line-endings/
+#
+# Linux start script should use lf
+/gradlew        text eol=lf
+
+# These are Windows script files and should use crlf
+*.bat           text eol=crlf
+

.gitignore

@@ -1,21 +1,9 @@
-# Compiled class file
-*.class
+# Ignore Gradle project-specific cache directory
+.gradle
 
-# Log file
-*.log
+# Ignore Gradle build output directory
+build
 
-# BlueJ files
-*.ctxt
+# Ignore vscode settings
+.vscode
 
-# Package Files #
-*.jar
-*.war
-*.nar
-*.ear
-*.zip
-*.tar.gz
-*.rar
-
-# virtual machine crash logs, see http://www.java.com/en/download/help/error_hotspot.xml
-hs_err_pid*
-replay_pid*

app/build.gradle

@@ -0,0 +1,152 @@
+/*
+ * This file was generated by the Gradle 'init' task.
+ *
+ * This generated file contains a sample Java application project to get you started.
+ * For more details take a look at the 'Building Java & JVM projects' chapter in the Gradle
+ * User Manual available at https://docs.gradle.org/8.0.2/userguide/building_java_projects.html
+ */
+
+plugins {
+
+
+  id 'java-library'
+
+  // Code formatting; defines targets "spotlessApply" and "spotlessCheck"
+  // Requires JDK 11 or higher; the plugin crashes under JDK 8.
+  id 'com.diffplug.spotless' version '6.25.0'
+
+  // Checker Framework pluggable type-checking
+  id 'org.checkerframework' version '0.6.37'
+}
+
+repositories {
+  // Snapshot repository for JSpecify conformance test framework
+  maven { url 'https://s01.oss.sonatype.org/content/repositories/snapshots'}
+  maven { url 'https://oss.sonatype.org/content/repositories/snapshots/'}
+  // Use Maven Central for resolving dependencies.
+  mavenCentral()
+}
+
+configurations {
+  jSpecifyConformanceTests
+}
+
+dependencies {
+  // Use JUnit Jupiter for testing.
+  testImplementation 'org.junit.jupiter:junit-jupiter:5.9.1'
+  testRuntimeOnly 'org.junit.jupiter:junit-jupiter:5.9.1'
+
+  // This dependency is used by the application.
+  implementation 'com.google.guava:guava:31.1-jre'
+
+  testImplementation 'org.jspecify:jspecify:0.3.0'
+
+  testImplementation 'org.jspecify.conformance:conformance-test-framework:0.0.0-SNAPSHOT'
+  jSpecifyConformanceTests 'org.jspecify.conformance:conformance-tests:0.0.0-SNAPSHOT'
+}
+
+spotless {
+  format 'misc', {
+    // define the files to apply `misc` to
+    target '*.md', '.gitignore'
+
+    // define the steps to apply to those files
+    trimTrailingWhitespace()
+    indentWithSpaces(2)
+    endWithNewline()
+  }
+  java {
+    googleJavaFormat()
+    formatAnnotations()
+  }
+  groovyGradle {
+    target '**/*.gradle'
+    greclipse()  // which formatter Spotless should use to format .gradle files.
+    indentWithSpaces(2)
+    trimTrailingWhitespace()
+    // endWithNewline() // Don't want to end empty files with a newline
+  }
+}
+
+apply plugin: 'org.checkerframework'
+
+dependencies {
+  compileOnly 'io.github.eisop:checker-qual:3.42.0-eisop2'
+  testCompileOnly 'io.github.eisop:checker-qual:3.42.0-eisop2'
+  checkerFramework 'io.github.eisop:checker:3.42.0-eisop2'
+}
+
+checkerFramework {
+  checkers = [
+    // No need to run CalledMethodsChecker, because ResourceLeakChecker does so.
+    // 'org.checkerframework.checker.calledmethods.CalledMethodsChecker',
+    'org.checkerframework.checker.formatter.FormatterChecker',
+    'org.checkerframework.checker.index.IndexChecker',
+    'org.checkerframework.checker.interning.InterningChecker',
+    'org.checkerframework.checker.lock.LockChecker',
+    'org.checkerframework.checker.nullness.NullnessChecker',
+    'org.checkerframework.checker.regex.RegexChecker',
+    'org.checkerframework.checker.resourceleak.ResourceLeakChecker',
+    'org.checkerframework.checker.signature.SignatureChecker',
+    'org.checkerframework.checker.signedness.SignednessChecker',
+    'org.checkerframework.common.initializedfields.InitializedFieldsChecker',
+  ]
+  extraJavacArgs = [
+    '-Werror',
+    '-AcheckPurityAnnotations',
+    '-ArequirePrefixInWarningSuppressions',
+    '-AwarnRedundantAnnotations',
+    '-AwarnUnneededSuppressions',
+    '-AnoJreVersionCheck',
+    '-Aversion',
+  ]
+}
+// To use a locally-built Checker Framework, run gradle with "-PcfLocal".
+if (project.hasProperty('cfLocal')) {
+  def cfHome = String.valueOf(System.getenv('CHECKERFRAMEWORK'))
+  dependencies {
+    compileOnly(files(cfHome + '/checker/dist/checker-qual.jar'))
+    testCompileOnly(files(cfHome + '/checker/dist/checker-qual.jar'))
+    checkerFramework files(cfHome + '/checker/dist/checker.jar')
+  }
+}
+
+tasks.named('test') {
+  // Use JUnit Platform for unit tests.
+  useJUnitPlatform()
+}
+
+// Unzip JSpecify conformance tests using the artifact
+task unzipJSpecifyConformanceTestSuite(type: Copy) {
+  description 'Unzips the JSpecify conformance test suite into the build directory.'
+
+  dependsOn(configurations.jSpecifyConformanceTests)
+  copy {
+    from zipTree(configurations.jSpecifyConformanceTests.singleFile)
+    into "${buildDir}/jspecify-conformance-tests"
+  }
+}
+
+// Run JSpecify conformance tests
+task runJSpecifyConformanceTests(type: Test, group: 'Verification') {
+  description 'Runs the JSpecify conformance tests.'
+  include '**/NullnessJSpecifyConformanceTest.class'
+
+  //shouldRunAfter test
+
+  environment 'JSPECIFY_CONFORMANCE_TEST_MODE', 'WRITE'
+
+  // Conformance tests
+  inputs.files(unzipJSpecifyConformanceTestSuite)
+  inputs.files("${projectDir}/src/test/resources/jspecify-conformance-test-report.txt")
+
+  doFirst {
+    systemProperties([
+      "ConformanceTest.inputs": "${buildDir}/jspecify-conformance-tests/assertions/org/jspecify/conformance/tests",
+      "ConformanceTest.report": "${projectDir}/src/test/resources/jspecify-conformance-test-report.txt",
+      "ConformanceTest.deps"  : fileTree("${buildDir}/jspecify-conformance-tests/deps").join(":")
+    ])
+  }
+}
+
+//test.finalizedBy(runJSpecifyConformanceTests)

app/src/test/java/jspecify/conformance/NullnessJSpecifyConformanceTest.java

@@ -0,0 +1,138 @@
+package jspecify.conformance;
+
+import static com.google.common.collect.ImmutableList.toImmutableList;
+import static com.google.common.collect.ImmutableSet.toImmutableSet;
+import static java.util.Objects.requireNonNull;
+
+import com.google.common.base.Splitter;
+import com.google.common.collect.ImmutableList;
+import com.google.common.collect.ImmutableSet;
+import java.io.File;
+import java.io.IOException;
+import java.nio.file.Path;
+import java.nio.file.Paths;
+import org.checkerframework.checker.nullness.NullnessChecker;
+import org.checkerframework.framework.test.TestConfiguration;
+import org.checkerframework.framework.test.TestConfigurationBuilder;
+import org.checkerframework.framework.test.TestUtilities;
+import org.checkerframework.framework.test.TypecheckExecutor;
+import org.checkerframework.framework.test.TypecheckResult;
+import org.jspecify.conformance.ConformanceTestRunner;
+import org.jspecify.conformance.ReportedFact;
+import org.junit.Test;
+
+/** An object to run the conformance tests against the EISOP Checker Framework. */
+public final class NullnessJSpecifyConformanceTest {
+
+  /** Directory of the JSpecify Conformance Tests. */
+  private final Path testDir;
+
+  /** Location of the report. */
+  private final Path reportPath;
+
+  /** JSpecify conformance test dependencies. */
+  private final ImmutableList<Path> deps;
+
+  /** Options to pass to the checker. */
+  private static final ImmutableList<String> TEST_OPTIONS =
+      ImmutableList.of("-AassumePure", "-Adetailedmsgtext");
+
+  /** Create a NullnessJSpecifyConformanceTest. */
+  public NullnessJSpecifyConformanceTest() {
+    System.out.println("HIIII");
+    this.testDir = getSystemPropertyPath("ConformanceTest.inputs");
+    this.reportPath = getSystemPropertyPath("ConformanceTest.report");
+    this.deps =
+        Splitter.on(":").splitToList(System.getProperty("ConformanceTest.deps")).stream()
+            .map(dep -> Paths.get(dep))
+            .collect(toImmutableList());
+  }
+
+  /**
+   * Get an equivalent path from a system property.
+   *
+   * @param propertyName the name of the property.
+   */
+  private Path getSystemPropertyPath(String propertyName) {
+    String path = System.getProperty(propertyName);
+    if (path == null) {
+      throw new IllegalArgumentException("System property " + propertyName + " not set");
+    }
+    return Paths.get(path);
+  }
+
+  /** Run the conformance tests. */
+  @Test
+  public void conformanceTests() throws IOException {
+    ConformanceTestRunner runner =
+        new ConformanceTestRunner(NullnessJSpecifyConformanceTest::analyze);
+    runner.checkConformance(testDir, deps, reportPath);
+  }
+
+  /**
+   * Analyze the conformance tests by comparing reported facts against expected facts.
+   *
+   * @param testDir the directory of the conformance tests.
+   * @param files the files to analyze.
+   * @param deps the dependencies of the conformance tests.
+   */
+  private static ImmutableSet<ReportedFact> analyze(
+      Path testDir, ImmutableList<Path> files, ImmutableList<Path> deps) {
+    ImmutableSet<File> fileInputs = files.stream().map(Path::toFile).collect(toImmutableSet());
+
+    ImmutableList<String> depsAsStrings =
+        deps.stream().map(Path::toString).collect(toImmutableList());
+
+    TestConfiguration testConfig =
+        TestConfigurationBuilder.buildDefaultConfiguration(
+            null,
+            fileInputs,
+            depsAsStrings,
+            ImmutableList.of(NullnessChecker.class.getName()),
+            TEST_OPTIONS,
+            TestUtilities.getShouldEmitDebugInfo());
+    TypecheckExecutor typecheckExecutor = new TypecheckExecutor();
+    TypecheckResult result = typecheckExecutor.runTest(testConfig);
+    ImmutableSet<ReportedFact> reportedFacts =
+        result.getUnexpectedDiagnostics().stream()
+            .map(
+                diagnostic ->
+                    new ReportedFactMessage(
+                        Path.of(diagnostic.getFilename()),
+                        diagnostic.getLineNumber(),
+                        diagnostic.getMessage()))
+            .collect(toImmutableSet());
+    return reportedFacts;
+  }
+}
+
+/** A reported fact with a message as a string. */
+final class ReportedFactMessage extends ReportedFact {
+
+  /** The message that the fact describes. */
+  private final String message;
+
+  /**
+   * Create a ReportedFactMessage.
+   *
+   * @param filename the file that the fact is in.
+   * @param lineNumber the line number of the fact.
+   * @param message the message that the fact describes.
+   */
+  ReportedFactMessage(Path filename, long lineNumber, String message) {
+    super(filename, lineNumber);
+    this.message = requireNonNull(message);
+  }
+
+  /** Indicates if the fact must be an expected fact. */
+  @Override
+  protected boolean mustBeExpected() {
+    return false;
+  }
+
+  /** Get the message that the fact describes. */
+  @Override
+  protected String getFactText() {
+    return message;
+  }
+}

gradle/wrapper/gradle-wrapper.properties

@@ -0,0 +1,6 @@
+distributionBase=GRADLE_USER_HOME
+distributionPath=wrapper/dists
+distributionUrl=https\://services.gradle.org/distributions/gradle-8.0.2-bin.zip
+networkTimeout=10000
+zipStoreBase=GRADLE_USER_HOME
+zipStorePath=wrapper/dists