diff --git a/.gitattributes b/.gitattributes new file mode 100644 index 0000000..097f9f9 --- /dev/null +++ b/.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 + diff --git a/.gitignore b/.gitignore index f1e391e..8624c0b 100644 --- a/.gitignore +++ b/.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* diff --git a/app/build.gradle b/app/build.gradle new file mode 100644 index 0000000..d6a9ede --- /dev/null +++ b/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) diff --git a/app/src/test/java/jspecify/conformance/NullnessJSpecifyConformanceTest.java b/app/src/test/java/jspecify/conformance/NullnessJSpecifyConformanceTest.java new file mode 100644 index 0000000..1fd7296 --- /dev/null +++ b/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 deps; + + /** Options to pass to the checker. */ + private static final ImmutableList 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 analyze( + Path testDir, ImmutableList files, ImmutableList deps) { + ImmutableSet fileInputs = files.stream().map(Path::toFile).collect(toImmutableSet()); + + ImmutableList 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 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; + } +} diff --git a/app/src/test/resources/jspecify-conformance-test-report.txt b/app/src/test/resources/jspecify-conformance-test-report.txt new file mode 100644 index 0000000..e69de29 diff --git a/gradle/wrapper/gradle-wrapper.jar b/gradle/wrapper/gradle-wrapper.jar new file mode 100644 index 0000000..ccebba7 Binary files /dev/null and b/gradle/wrapper/gradle-wrapper.jar differ diff --git a/gradle/wrapper/gradle-wrapper.properties b/gradle/wrapper/gradle-wrapper.properties new file mode 100644 index 0000000..bdc9a83 --- /dev/null +++ b/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 diff --git a/gradlew b/gradlew new file mode 100755 index 0000000..79a61d4 --- /dev/null +++ b/gradlew @@ -0,0 +1,244 @@ +#!/bin/sh + +# +# Copyright © 2015-2021 the original authors. +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# https://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. +# + +############################################################################## +# +# Gradle start up script for POSIX generated by Gradle. +# +# Important for running: +# +# (1) You need a POSIX-compliant shell to run this script. If your /bin/sh is +# noncompliant, but you have some other compliant shell such as ksh or +# bash, then to run this script, type that shell name before the whole +# command line, like: +# +# ksh Gradle +# +# Busybox and similar reduced shells will NOT work, because this script +# requires all of these POSIX shell features: +# * functions; +# * expansions «$var», «${var}», «${var:-default}», «${var+SET}», +# «${var#prefix}», «${var%suffix}», and «$( cmd )»; +# * compound commands having a testable exit status, especially «case»; +# * various built-in commands including «command», «set», and «ulimit». +# +# Important for patching: +# +# (2) This script targets any POSIX shell, so it avoids extensions provided +# by Bash, Ksh, etc; in particular arrays are avoided. +# +# The "traditional" practice of packing multiple parameters into a +# space-separated string is a well documented source of bugs and security +# problems, so this is (mostly) avoided, by progressively accumulating +# options in "$@", and eventually passing that to Java. +# +# Where the inherited environment variables (DEFAULT_JVM_OPTS, JAVA_OPTS, +# and GRADLE_OPTS) rely on word-splitting, this is performed explicitly; +# see the in-line comments for details. +# +# There are tweaks for specific operating systems such as AIX, CygWin, +# Darwin, MinGW, and NonStop. +# +# (3) This script is generated from the Groovy template +# https://github.com/gradle/gradle/blob/HEAD/subprojects/plugins/src/main/resources/org/gradle/api/internal/plugins/unixStartScript.txt +# within the Gradle project. +# +# You can find Gradle at https://github.com/gradle/gradle/. +# +############################################################################## + +# Attempt to set APP_HOME + +# Resolve links: $0 may be a link +app_path=$0 + +# Need this for daisy-chained symlinks. +while + APP_HOME=${app_path%"${app_path##*/}"} # leaves a trailing /; empty if no leading path + [ -h "$app_path" ] +do + ls=$( ls -ld "$app_path" ) + link=${ls#*' -> '} + case $link in #( + /*) app_path=$link ;; #( + *) app_path=$APP_HOME$link ;; + esac +done + +# This is normally unused +# shellcheck disable=SC2034 +APP_BASE_NAME=${0##*/} +APP_HOME=$( cd "${APP_HOME:-./}" && pwd -P ) || exit + +# Add default JVM options here. You can also use JAVA_OPTS and GRADLE_OPTS to pass JVM options to this script. +DEFAULT_JVM_OPTS='"-Xmx64m" "-Xms64m"' + +# Use the maximum available, or set MAX_FD != -1 to use that value. +MAX_FD=maximum + +warn () { + echo "$*" +} >&2 + +die () { + echo + echo "$*" + echo + exit 1 +} >&2 + +# OS specific support (must be 'true' or 'false'). +cygwin=false +msys=false +darwin=false +nonstop=false +case "$( uname )" in #( + CYGWIN* ) cygwin=true ;; #( + Darwin* ) darwin=true ;; #( + MSYS* | MINGW* ) msys=true ;; #( + NONSTOP* ) nonstop=true ;; +esac + +CLASSPATH=$APP_HOME/gradle/wrapper/gradle-wrapper.jar + + +# Determine the Java command to use to start the JVM. +if [ -n "$JAVA_HOME" ] ; then + if [ -x "$JAVA_HOME/jre/sh/java" ] ; then + # IBM's JDK on AIX uses strange locations for the executables + JAVACMD=$JAVA_HOME/jre/sh/java + else + JAVACMD=$JAVA_HOME/bin/java + fi + if [ ! -x "$JAVACMD" ] ; then + die "ERROR: JAVA_HOME is set to an invalid directory: $JAVA_HOME + +Please set the JAVA_HOME variable in your environment to match the +location of your Java installation." + fi +else + JAVACMD=java + which java >/dev/null 2>&1 || die "ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH. + +Please set the JAVA_HOME variable in your environment to match the +location of your Java installation." +fi + +# Increase the maximum file descriptors if we can. +if ! "$cygwin" && ! "$darwin" && ! "$nonstop" ; then + case $MAX_FD in #( + max*) + # In POSIX sh, ulimit -H is undefined. That's why the result is checked to see if it worked. + # shellcheck disable=SC3045 + MAX_FD=$( ulimit -H -n ) || + warn "Could not query maximum file descriptor limit" + esac + case $MAX_FD in #( + '' | soft) :;; #( + *) + # In POSIX sh, ulimit -n is undefined. That's why the result is checked to see if it worked. + # shellcheck disable=SC3045 + ulimit -n "$MAX_FD" || + warn "Could not set maximum file descriptor limit to $MAX_FD" + esac +fi + +# Collect all arguments for the java command, stacking in reverse order: +# * args from the command line +# * the main class name +# * -classpath +# * -D...appname settings +# * --module-path (only if needed) +# * DEFAULT_JVM_OPTS, JAVA_OPTS, and GRADLE_OPTS environment variables. + +# For Cygwin or MSYS, switch paths to Windows format before running java +if "$cygwin" || "$msys" ; then + APP_HOME=$( cygpath --path --mixed "$APP_HOME" ) + CLASSPATH=$( cygpath --path --mixed "$CLASSPATH" ) + + JAVACMD=$( cygpath --unix "$JAVACMD" ) + + # Now convert the arguments - kludge to limit ourselves to /bin/sh + for arg do + if + case $arg in #( + -*) false ;; # don't mess with options #( + /?*) t=${arg#/} t=/${t%%/*} # looks like a POSIX filepath + [ -e "$t" ] ;; #( + *) false ;; + esac + then + arg=$( cygpath --path --ignore --mixed "$arg" ) + fi + # Roll the args list around exactly as many times as the number of + # args, so each arg winds up back in the position where it started, but + # possibly modified. + # + # NB: a `for` loop captures its iteration list before it begins, so + # changing the positional parameters here affects neither the number of + # iterations, nor the values presented in `arg`. + shift # remove old arg + set -- "$@" "$arg" # push replacement arg + done +fi + +# Collect all arguments for the java command; +# * $DEFAULT_JVM_OPTS, $JAVA_OPTS, and $GRADLE_OPTS can contain fragments of +# shell script including quotes and variable substitutions, so put them in +# double quotes to make sure that they get re-expanded; and +# * put everything else in single quotes, so that it's not re-expanded. + +set -- \ + "-Dorg.gradle.appname=$APP_BASE_NAME" \ + -classpath "$CLASSPATH" \ + org.gradle.wrapper.GradleWrapperMain \ + "$@" + +# Stop when "xargs" is not available. +if ! command -v xargs >/dev/null 2>&1 +then + die "xargs is not available" +fi + +# Use "xargs" to parse quoted args. +# +# With -n1 it outputs one arg per line, with the quotes and backslashes removed. +# +# In Bash we could simply go: +# +# readarray ARGS < <( xargs -n1 <<<"$var" ) && +# set -- "${ARGS[@]}" "$@" +# +# but POSIX shell has neither arrays nor command substitution, so instead we +# post-process each arg (as a line of input to sed) to backslash-escape any +# character that might be a shell metacharacter, then use eval to reverse +# that process (while maintaining the separation between arguments), and wrap +# the whole thing up as a single "set" statement. +# +# This will of course break if any of these variables contains a newline or +# an unmatched quote. +# + +eval "set -- $( + printf '%s\n' "$DEFAULT_JVM_OPTS $JAVA_OPTS $GRADLE_OPTS" | + xargs -n1 | + sed ' s~[^-[:alnum:]+,./:=@_]~\\&~g; ' | + tr '\n' ' ' + )" '"$@"' + +exec "$JAVACMD" "$@" diff --git a/gradlew.bat b/gradlew.bat new file mode 100644 index 0000000..93e3f59 --- /dev/null +++ b/gradlew.bat @@ -0,0 +1,92 @@ +@rem +@rem Copyright 2015 the original author or authors. +@rem +@rem Licensed under the Apache License, Version 2.0 (the "License"); +@rem you may not use this file except in compliance with the License. +@rem You may obtain a copy of the License at +@rem +@rem https://www.apache.org/licenses/LICENSE-2.0 +@rem +@rem Unless required by applicable law or agreed to in writing, software +@rem distributed under the License is distributed on an "AS IS" BASIS, +@rem WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +@rem See the License for the specific language governing permissions and +@rem limitations under the License. +@rem + +@if "%DEBUG%"=="" @echo off +@rem ########################################################################## +@rem +@rem Gradle startup script for Windows +@rem +@rem ########################################################################## + +@rem Set local scope for the variables with windows NT shell +if "%OS%"=="Windows_NT" setlocal + +set DIRNAME=%~dp0 +if "%DIRNAME%"=="" set DIRNAME=. +@rem This is normally unused +set APP_BASE_NAME=%~n0 +set APP_HOME=%DIRNAME% + +@rem Resolve any "." and ".." in APP_HOME to make it shorter. +for %%i in ("%APP_HOME%") do set APP_HOME=%%~fi + +@rem Add default JVM options here. You can also use JAVA_OPTS and GRADLE_OPTS to pass JVM options to this script. +set DEFAULT_JVM_OPTS="-Xmx64m" "-Xms64m" + +@rem Find java.exe +if defined JAVA_HOME goto findJavaFromJavaHome + +set JAVA_EXE=java.exe +%JAVA_EXE% -version >NUL 2>&1 +if %ERRORLEVEL% equ 0 goto execute + +echo. +echo ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH. +echo. +echo Please set the JAVA_HOME variable in your environment to match the +echo location of your Java installation. + +goto fail + +:findJavaFromJavaHome +set JAVA_HOME=%JAVA_HOME:"=% +set JAVA_EXE=%JAVA_HOME%/bin/java.exe + +if exist "%JAVA_EXE%" goto execute + +echo. +echo ERROR: JAVA_HOME is set to an invalid directory: %JAVA_HOME% +echo. +echo Please set the JAVA_HOME variable in your environment to match the +echo location of your Java installation. + +goto fail + +:execute +@rem Setup the command line + +set CLASSPATH=%APP_HOME%\gradle\wrapper\gradle-wrapper.jar + + +@rem Execute Gradle +"%JAVA_EXE%" %DEFAULT_JVM_OPTS% %JAVA_OPTS% %GRADLE_OPTS% "-Dorg.gradle.appname=%APP_BASE_NAME%" -classpath "%CLASSPATH%" org.gradle.wrapper.GradleWrapperMain %* + +:end +@rem End local scope for the variables with windows NT shell +if %ERRORLEVEL% equ 0 goto mainEnd + +:fail +rem Set variable GRADLE_EXIT_CONSOLE if you need the _script_ return code instead of +rem the _cmd.exe /c_ return code! +set EXIT_CODE=%ERRORLEVEL% +if %EXIT_CODE% equ 0 set EXIT_CODE=1 +if not ""=="%GRADLE_EXIT_CONSOLE%" exit %EXIT_CODE% +exit /b %EXIT_CODE% + +:mainEnd +if "%OS%"=="Windows_NT" endlocal + +:omega diff --git a/settings.gradle b/settings.gradle new file mode 100644 index 0000000..c2b7926 --- /dev/null +++ b/settings.gradle @@ -0,0 +1,11 @@ +/* + * This file was generated by the Gradle 'init' task. + * + * The settings file is used to specify which projects to include in your build. + * + * Detailed information about configuring a multi-project build in Gradle can be found + * in the user manual at https://docs.gradle.org/8.0.2/userguide/multi_project_builds.html + */ + +rootProject.name = 'jspecify.conformance' +include('app')