diff --git a/.github/dependabot.yml b/.github/dependabot.yml index b00c3bd..84865aa 100644 --- a/.github/dependabot.yml +++ b/.github/dependabot.yml @@ -1,6 +1,14 @@ version: 2 updates: - package-ecosystem: "gradle" + directories: + - "/" + - "/linear-checker-qual-android/" + - "/linear-checker-qual/" + schedule: + interval: "daily" + + - package-ecosystem: "github-actions" directory: "/" schedule: interval: "daily" diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index e4b1b60..c703bf4 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -12,7 +12,7 @@ jobs: build: strategy: matrix: - jdk: [ 8, 11, 17 ] + jdk: [ 8, 11, 17, 21, 23 ] runs-on: ubuntu-latest steps: - name: Pull Request Checkout diff --git a/build.gradle b/build.gradle index 26e4951..f217d49 100644 --- a/build.gradle +++ b/build.gradle @@ -1,10 +1,7 @@ buildscript { dependencies { if (JavaVersion.current() >= JavaVersion.VERSION_11) { - // Code formatting; defines targets "spotlessApply" and "spotlessCheck". - // https://github.com/diffplug/spotless/tags ; see tags starting "gradle/" - // Only works on JDK 11+. - classpath 'com.diffplug.spotless:spotless-plugin-gradle:6.22.0' + classpath 'com.diffplug.spotless:spotless-plugin-gradle:7.0.2' } } } @@ -12,10 +9,13 @@ buildscript { plugins { id "java" id "maven-publish" + // https://github.com/tbroyer/gradle-errorprone-plugin + id 'net.ltgt.errorprone' version '4.1.0' } repositories { mavenCentral() + mavenLocal() } configurations { @@ -26,60 +26,73 @@ configurations { } ext { - isJava8 = JavaVersion.current() == JavaVersion.VERSION_1_8 - isJava11plus = JavaVersion.current() >= JavaVersion.VERSION_11 - versions = [ - checkerFramework: "3.32.0-eisop1", + checkerFramework: "3.42.0-eisop5", + errorproneJavacVersion: "9+181-r4173-1", + errorproneCoreVersion: "2.36.0", ] + + // Keep in sync with the same variable in checker-framework/build.gradle compilerArgsForRunningCF = [ - "--add-exports", - "jdk.compiler/com.sun.tools.javac.api=ALL-UNNAMED", - "--add-exports", - "jdk.compiler/com.sun.tools.javac.code=ALL-UNNAMED", - "--add-exports", - "jdk.compiler/com.sun.tools.javac.file=ALL-UNNAMED", - "--add-exports", - "jdk.compiler/com.sun.tools.javac.main=ALL-UNNAMED", - "--add-exports", - "jdk.compiler/com.sun.tools.javac.model=ALL-UNNAMED", - "--add-exports", - "jdk.compiler/com.sun.tools.javac.processing=ALL-UNNAMED", - "--add-exports", - "jdk.compiler/com.sun.tools.javac.tree=ALL-UNNAMED", - "--add-exports", - "jdk.compiler/com.sun.tools.javac.util=ALL-UNNAMED", - "--add-opens", - "jdk.compiler/com.sun.tools.javac.comp=ALL-UNNAMED", + '--add-exports', + 'jdk.compiler/com.sun.tools.javac.api=ALL-UNNAMED', + '--add-exports', + 'jdk.compiler/com.sun.tools.javac.code=ALL-UNNAMED', + '--add-exports', + 'jdk.compiler/com.sun.tools.javac.file=ALL-UNNAMED', + '--add-exports', + 'jdk.compiler/com.sun.tools.javac.main=ALL-UNNAMED', + '--add-exports', + 'jdk.compiler/com.sun.tools.javac.model=ALL-UNNAMED', + '--add-exports', + 'jdk.compiler/com.sun.tools.javac.processing=ALL-UNNAMED', + '--add-exports', + 'jdk.compiler/com.sun.tools.javac.tree=ALL-UNNAMED', + '--add-exports', + 'jdk.compiler/com.sun.tools.javac.util=ALL-UNNAMED', + '--add-opens', + 'jdk.compiler/com.sun.tools.javac.comp=ALL-UNNAMED', ] } -sourceCompatibility = 1.8 +java { + sourceCompatibility = JavaVersion.VERSION_1_8 +} + def checkerframework_local = false // Set this variable to [true] while using local version of checker framework. def CHECKERFRAMEWORK = System.getenv("CHECKERFRAMEWORK") +ext { + isJava11plus = JavaVersion.current() >= JavaVersion.VERSION_11 +} + + dependencies { // This dependency is found on compile classpath of this component and consumers. + // TODO: clean up implementation/localDeps duplication. if (checkerframework_local) { if (CHECKERFRAMEWORK == null) { CHECKERFRAMEWORK = "../checker-framework/" } implementation files("${CHECKERFRAMEWORK}/checker/dist/checker-qual.jar") + implementation files("${CHECKERFRAMEWORK}/checker/dist/checker.jar") localDeps files("${CHECKERFRAMEWORK}/checker/dist/checker.jar") } else { + implementation "io.github.eisop:checker:${versions.checkerFramework}" localDeps "io.github.eisop:checker:${versions.checkerFramework}" + implementation "io.github.eisop:checker-qual:${versions.checkerFramework}" localDeps "io.github.eisop:checker-qual:${versions.checkerFramework}" + implementation "io.github.eisop:checker-util:${versions.checkerFramework}" localDeps "io.github.eisop:checker-util:${versions.checkerFramework}" } - implementation configurations.localDeps - compileOnly "com.google.errorprone:javac:9+181-r4173-1" + errorprone "com.google.errorprone:error_prone_core:${versions.errorproneCoreVersion}" + errorproneJavac "com.google.errorprone:javac:${versions.errorproneJavacVersion}" // Testing testImplementation "junit:junit:4.13.2" testImplementation "io.github.eisop:framework-test:${versions.checkerFramework}" - errorproneJavac "com.google.errorprone:javac:9+181-r4173-1" // https://mvnrepository.com/artifact/org.yaml/snakeyaml implementation 'org.yaml:snakeyaml:2.2' } @@ -106,10 +119,6 @@ sourceSets { } } -tasks.withType(JavaCompile).all { - options.compilerArgs.add("-Xlint:all") -} - if (isJava11plus) { apply plugin: 'com.diffplug.spotless' assemble.dependsOn(":spotlessApply") @@ -121,27 +130,28 @@ if (isJava11plus) { importOrder('com', 'jdk', 'lib', 'lombok', 'org', 'java', 'javax') formatAnnotations().addTypeAnnotation("Unique").addTypeAnnotation("Shared").addTypeAnnotation("Disappear").addTypeAnnotation("Bottom") } + format "misc", { + target '**/*.md', "**/.gitignore" + trimTrailingWhitespace() + leadingSpacesToTabs() + endWithNewline() + } groovyGradle { target '**/*.gradle' greclipse() // which formatter Spotless should use to format .gradle files. - indentWithSpaces(4) + leadingTabsToSpaces(4) trimTrailingWhitespace() // endWithNewline() // Don't want to end empty files with a newline } - format "misc", { - target '**/*.md', "**/.gitignore" - trimTrailingWhitespace() - indentWithTabs() - endWithNewline() - } } } + // Run `./gradlew publishToMavenLocal` to publish your checker to your local Maven repository. publishing { publications { maven(MavenPublication) { - groupId = "org.checkerframework" + groupId = "io.github.eisop" artifactId = "linear-checker" version = "0.1-SNAPSHOT" from components.java @@ -149,7 +159,7 @@ publishing { pom.withXml { def dependenciesNode = asNode().appendNode('dependencies') def dependencyNode = dependenciesNode.appendNode('dependency') - dependencyNode.appendNode("groupId", "org.checkerframework") + dependencyNode.appendNode("groupId", "io.github.eisop") dependencyNode.appendNode("artifactId", "checker") dependencyNode.appendNode("version", "${versions.checkerFramework}") dependencyNode.appendNode("systemPath", projectDir.toString() + "$buildDir/libs/checker.jar") @@ -159,32 +169,28 @@ publishing { } } -test { - if (!isJava8) { - jvmArgs += compilerArgsForRunningCF - } - - if (!JavaVersion.current().java9Compatible) { - jvmArgs "-Xbootclasspath/p:${configurations.errorproneJavac.asPath}" - } -} - test.dependsOn(":assemble") afterEvaluate { // Configure JUnit tests tasks.withType(Test) { + if (!JavaVersion.current().java9Compatible) { + jvmArgs "-Xbootclasspath/p:${configurations.errorproneJavac.asPath}" + } else { + jvmArgs += compilerArgsForRunningCF + } + testLogging { // Always run the tests outputs.upToDateWhen { false } // The following prints out each time a test is passed. events "passed", "skipped", "failed", "standardOut", "standardError" // Show the found unexpected diagnostics and expected diagnostics not found. - exceptionFormat "full" - showExceptions true - showCauses true - showStackTraces true - showStandardStreams true + exceptionFormat = "full" + showExceptions = true + showCauses = true + showStackTraces = true + showStandardStreams = true } // After each test, print a summary. afterSuite { desc, result -> @@ -200,6 +206,43 @@ afterEvaluate { } } } + + // Code adapted from checker-framework: + // https://github.com/eisop/checker-framework/blob/567084f11278273b33289d138d9d2a1b513d3c35/build.gradle#L226 + tasks.withType(JavaCompile) { compilationTask -> + sourceCompatibility = 8 + targetCompatibility = 8 + options.failOnError = true + options.deprecation = true + options.compilerArgs += [ + '-g', + '-Werror', + // -options because source 8 is obsolete on newer JDKs + "-Xlint:all,-options", + ] + options.encoding = 'UTF-8' + options.fork = true + if (JavaVersion.current() == JavaVersion.VERSION_1_8) { + options.forkOptions.jvmArgs += [ + "-Xbootclasspath/p:${configurations.errorproneJavac.asPath}".toString() + ] + options.errorprone.enabled = false + } else { + options.errorprone.enabled = (JavaVersion.current() >= JavaVersion.VERSION_17) + options.forkOptions.jvmArgs += [ + '--add-exports=jdk.compiler/com.sun.tools.javac.api=ALL-UNNAMED', + '--add-exports=jdk.compiler/com.sun.tools.javac.file=ALL-UNNAMED', + '--add-exports=jdk.compiler/com.sun.tools.javac.main=ALL-UNNAMED', + '--add-exports=jdk.compiler/com.sun.tools.javac.model=ALL-UNNAMED', + '--add-exports=jdk.compiler/com.sun.tools.javac.parser=ALL-UNNAMED', + '--add-exports=jdk.compiler/com.sun.tools.javac.processing=ALL-UNNAMED', + '--add-exports=jdk.compiler/com.sun.tools.javac.tree=ALL-UNNAMED', + '--add-exports=jdk.compiler/com.sun.tools.javac.util=ALL-UNNAMED', + '--add-opens=jdk.compiler/com.sun.tools.javac.code=ALL-UNNAMED', + '--add-opens=jdk.compiler/com.sun.tools.javac.comp=ALL-UNNAMED', + ] + } + } } clean.doFirst { diff --git a/gradle/wrapper/gradle-wrapper.jar b/gradle/wrapper/gradle-wrapper.jar index 7454180..a4b76b9 100644 Binary files a/gradle/wrapper/gradle-wrapper.jar and b/gradle/wrapper/gradle-wrapper.jar differ diff --git a/gradle/wrapper/gradle-wrapper.properties b/gradle/wrapper/gradle-wrapper.properties index ae04661..cea7a79 100644 --- a/gradle/wrapper/gradle-wrapper.properties +++ b/gradle/wrapper/gradle-wrapper.properties @@ -1,5 +1,7 @@ distributionBase=GRADLE_USER_HOME distributionPath=wrapper/dists -distributionUrl=https\://services.gradle.org/distributions/gradle-7.5.1-bin.zip +distributionUrl=https\://services.gradle.org/distributions/gradle-8.12-bin.zip +networkTimeout=10000 +validateDistributionUrl=true zipStoreBase=GRADLE_USER_HOME zipStorePath=wrapper/dists diff --git a/gradlew b/gradlew index 1b6c787..f3b75f3 100755 --- a/gradlew +++ b/gradlew @@ -15,6 +15,8 @@ # See the License for the specific language governing permissions and # limitations under the License. # +# SPDX-License-Identifier: Apache-2.0 +# ############################################################################## # @@ -55,7 +57,7 @@ # Darwin, MinGW, and NonStop. # # (3) This script is generated from the Groovy template -# https://github.com/gradle/gradle/blob/master/subprojects/plugins/src/main/resources/org/gradle/api/internal/plugins/unixStartScript.txt +# https://github.com/gradle/gradle/blob/HEAD/platforms/jvm/plugins-application/src/main/resources/org/gradle/api/internal/plugins/unixStartScript.txt # within the Gradle project. # # You can find Gradle at https://github.com/gradle/gradle/. @@ -80,13 +82,11 @@ do esac done -APP_HOME=$( cd "${APP_HOME:-./}" && pwd -P ) || exit - -APP_NAME="Gradle" +# This is normally unused +# shellcheck disable=SC2034 APP_BASE_NAME=${0##*/} - -# 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"' +# Discard cd standard output in case $CDPATH is set (https://github.com/gradle/gradle/issues/25036) +APP_HOME=$( cd -P "${APP_HOME:-./}" > /dev/null && printf '%s\n' "$PWD" ) || exit # Use the maximum available, or set MAX_FD != -1 to use that value. MAX_FD=maximum @@ -133,22 +133,29 @@ 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. + if ! command -v java >/dev/null 2>&1 + then + 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 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=SC2039,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=SC2039,SC3045 ulimit -n "$MAX_FD" || warn "Could not set maximum file descriptor limit to $MAX_FD" esac @@ -193,11 +200,15 @@ if "$cygwin" || "$msys" ; then 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. + +# 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"' + +# Collect all arguments for the java command: +# * DEFAULT_JVM_OPTS, JAVA_OPTS, JAVA_OPTS, and optsEnvironmentVar are not allowed to contain shell fragments, +# and any embedded shellness will be escaped. +# * For example: A user cannot expect ${Hostname} to be expanded, as it is an environment variable and will be +# treated as '${Hostname}' itself on the command line. set -- \ "-Dorg.gradle.appname=$APP_BASE_NAME" \ @@ -205,6 +216,12 @@ set -- \ 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. diff --git a/gradlew.bat b/gradlew.bat index ac1b06f..9b42019 100644 --- a/gradlew.bat +++ b/gradlew.bat @@ -13,8 +13,10 @@ @rem See the License for the specific language governing permissions and @rem limitations under the License. @rem +@rem SPDX-License-Identifier: Apache-2.0 +@rem -@if "%DEBUG%" == "" @echo off +@if "%DEBUG%"=="" @echo off @rem ########################################################################## @rem @rem Gradle startup script for Windows @@ -25,7 +27,8 @@ if "%OS%"=="Windows_NT" setlocal set DIRNAME=%~dp0 -if "%DIRNAME%" == "" set DIRNAME=. +if "%DIRNAME%"=="" set DIRNAME=. +@rem This is normally unused set APP_BASE_NAME=%~n0 set APP_HOME=%DIRNAME% @@ -40,13 +43,13 @@ if defined JAVA_HOME goto findJavaFromJavaHome set JAVA_EXE=java.exe %JAVA_EXE% -version >NUL 2>&1 -if "%ERRORLEVEL%" == "0" goto execute +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. +echo. 1>&2 +echo ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH. 1>&2 +echo. 1>&2 +echo Please set the JAVA_HOME variable in your environment to match the 1>&2 +echo location of your Java installation. 1>&2 goto fail @@ -56,11 +59,11 @@ 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. +echo. 1>&2 +echo ERROR: JAVA_HOME is set to an invalid directory: %JAVA_HOME% 1>&2 +echo. 1>&2 +echo Please set the JAVA_HOME variable in your environment to match the 1>&2 +echo location of your Java installation. 1>&2 goto fail @@ -75,13 +78,15 @@ set CLASSPATH=%APP_HOME%\gradle\wrapper\gradle-wrapper.jar :end @rem End local scope for the variables with windows NT shell -if "%ERRORLEVEL%"=="0" goto mainEnd +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! -if not "" == "%GRADLE_EXIT_CONSOLE%" exit 1 -exit /b 1 +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 diff --git a/linear-checker-qual-android/build.gradle b/linear-checker-qual-android/build.gradle index dbe5c26..6c55d0f 100644 --- a/linear-checker-qual-android/build.gradle +++ b/linear-checker-qual-android/build.gradle @@ -6,13 +6,17 @@ repositories { mavenCentral() } +ext.versions = [ + checkerFramework: "3.42.0-eisop5", +] + dependencies { - implementation 'io.github.eisop:checker:3.25.0-eisop1' - implementation 'io.github.eisop:checker-qual:3.25.0-eisop1' + implementation "io.github.eisop:checker:${versions.checkerFramework}" + implementation "io.github.eisop:checker-qual:${versions.checkerFramework}" } task copySources(type: Copy, dependsOn: ':linear-checker-qual:copySources') { - description 'Copy linear-checker-qual source to linear-checker-qual-android' + description = 'Copy linear-checker-qual source to linear-checker-qual-android' includeEmptyDirs = false doFirst { @@ -24,8 +28,19 @@ task copySources(type: Copy, dependsOn: ':linear-checker-qual:copySources') { into file('src/main') // Not read only because "replaceAnnotations" tasks writes to the files. - fileMode(0666) - dirMode(0777) + filePermissions { + user { + read = true + write = true + } + } + dirPermissions { + user { + read = true + write = true + execute = true + } + } } /** diff --git a/linear-checker-qual/build.gradle b/linear-checker-qual/build.gradle index 43b75a9..0f03183 100644 --- a/linear-checker-qual/build.gradle +++ b/linear-checker-qual/build.gradle @@ -6,9 +6,13 @@ repositories { mavenCentral() } +ext.versions = [ + checkerFramework: "3.42.0-eisop5", +] + dependencies { - implementation 'io.github.eisop:checker:3.25.0-eisop1' - implementation 'io.github.eisop:checker-qual:3.25.0-eisop1' + implementation "io.github.eisop:checker:${versions.checkerFramework}" + implementation "io.github.eisop:checker-qual:${versions.checkerFramework}" } task copySources(type: Copy) { @@ -23,7 +27,12 @@ task copySources(type: Copy) { include '**/org/checkerframework/checker/linear/qual/**' // Make files read only. - fileMode(0444) + filePermissions { + user { + read = true + write = false + } + } into file('src/main/java') } diff --git a/src/main/java/org/checkerframework/checker/linear/LinearAnalysis.java b/src/main/java/org/checkerframework/checker/linear/LinearAnalysis.java index fe7c69a..c5fe0a0 100644 --- a/src/main/java/org/checkerframework/checker/linear/LinearAnalysis.java +++ b/src/main/java/org/checkerframework/checker/linear/LinearAnalysis.java @@ -21,11 +21,11 @@ public class LinearAnalysis extends CFAbstractAnalysis { - private final LinearAnnotatedTypeFactory atypeFactory; + private final LinearAnnotatedTypeFactory linearAtypeFactory; public LinearAnalysis(BaseTypeChecker checker, LinearAnnotatedTypeFactory factory) { super(checker, factory); - this.atypeFactory = factory; + this.linearAtypeFactory = factory; } @Override @@ -36,7 +36,7 @@ public boolean updateNodeValues(Node node, TransferResult tran // TODO: there is a bug, the lhs node should be updated later, think about a way to do it. if (node instanceof AssignmentNode) { - Node rhsNode = ((AssignmentNode) node).getExpression(); + // Node rhsNode = ((AssignmentNode) node).getExpression(); // update lhs value Node lhsNode = ((AssignmentNode) node).getTarget(); @@ -106,10 +106,10 @@ protected boolean canUpdate(Node lhsNode, Node rhsNode, CFValue lhsValue) { atypeFactory.getAnnotationMirror(rhsNode.getTree(), Unique.class); if (lhsAMUnique != null && rhsAMUnique != null && lhsValue != null) { for (AnnotationMirror lhsAnno : lhsValue.getAnnotations()) { - if (AnnotationUtils.areSameByName(atypeFactory.UNIQUE, lhsAnno)) { + if (AnnotationUtils.areSameByName(linearAtypeFactory.UNIQUE, lhsAnno)) { List lhsStatesList = AnnotationUtils.getElementValueArray( - lhsAnno, "value", String.class, true); + lhsAnno, linearAtypeFactory.uniqueValueElement, String.class); // TODO: hard to check if (lhsStatesList.size() > 0) { return true; diff --git a/src/main/java/org/checkerframework/checker/linear/LinearAnnotatedTypeFactory.java b/src/main/java/org/checkerframework/checker/linear/LinearAnnotatedTypeFactory.java index 349fe49..d56310e 100644 --- a/src/main/java/org/checkerframework/checker/linear/LinearAnnotatedTypeFactory.java +++ b/src/main/java/org/checkerframework/checker/linear/LinearAnnotatedTypeFactory.java @@ -2,6 +2,7 @@ import org.checkerframework.checker.linear.qual.Bottom; import org.checkerframework.checker.linear.qual.Disappear; +import org.checkerframework.checker.linear.qual.EnsureUnique; import org.checkerframework.checker.linear.qual.Shared; import org.checkerframework.checker.linear.qual.Unique; import org.checkerframework.common.basetype.BaseTypeChecker; @@ -12,6 +13,7 @@ import org.checkerframework.framework.type.QualifierHierarchy; import org.checkerframework.javacutil.AnnotationBuilder; import org.checkerframework.javacutil.AnnotationUtils; +import org.checkerframework.javacutil.TreeUtils; import org.yaml.snakeyaml.Yaml; import java.io.File; @@ -19,10 +21,12 @@ import java.lang.annotation.Annotation; import java.util.Arrays; import java.util.Collection; +import java.util.Collections; import java.util.List; import java.util.Map; import javax.lang.model.element.AnnotationMirror; +import javax.lang.model.element.ExecutableElement; import javax.lang.model.util.Elements; public class LinearAnnotatedTypeFactory @@ -30,20 +34,30 @@ public class LinearAnnotatedTypeFactory /** The @{@link Bottom} annotation. */ protected final AnnotationMirror BOTTOM = AnnotationBuilder.fromClass(elements, Bottom.class); + /** The @{@link Disappear} annotation. */ protected final AnnotationMirror DISAPPEAR = AnnotationBuilder.fromClass(elements, Disappear.class); + /** The @{@link Unique} annotation. */ protected final AnnotationMirror UNIQUE = AnnotationBuilder.fromClass(elements, Unique.class); + /** The @{@link Shared} annotation. */ protected final AnnotationMirror SHARED = AnnotationBuilder.fromClass(elements, Shared.class); - protected final Map atomoton = parseAtomotan(); + protected final Map automaton = parseAutomaton(); + protected final ExecutableElement sharedValueElement = + TreeUtils.getMethod(Shared.class, "value", 0, processingEnv); + protected final ExecutableElement uniqueValueElement = + TreeUtils.getMethod(Unique.class, "value", 0, processingEnv); + protected final ExecutableElement ensureUniqueValueElement = + TreeUtils.getMethod(EnsureUnique.class, "value", 0, processingEnv); + + @SuppressWarnings("this-escape") public LinearAnnotatedTypeFactory(BaseTypeChecker checker) { super(checker, true); this.postInit(); - parseAtomotan(); } // @Override @@ -58,7 +72,7 @@ public LinearAnnotatedTypeFactory(BaseTypeChecker checker) { // } // } - protected Map parseAtomotan() { + protected Map parseAutomaton() { String atomotansOption = checker.getOption("atomotans"); if (atomotansOption != null) { Yaml yaml = new Yaml(); @@ -68,7 +82,9 @@ protected Map parseAtomotan() { InputStream inputStream = LinearAnnotatedTypeFactory.class.getResourceAsStream(file); if (inputStream != null) { - return (Map) yaml.load(inputStream); + @SuppressWarnings("unchecked") + Map ret = (Map) yaml.load(inputStream); + return ret; } } } @@ -90,13 +106,13 @@ private final class LinearQualifierHierarchy extends ElementQualifierHierarchy { */ public LinearQualifierHierarchy( Collection> qualifierClasses, Elements elements) { - super(qualifierClasses, elements); + super(qualifierClasses, elements, LinearAnnotatedTypeFactory.this); } // 1.@Shared is super type // 2.@Unique({}) is the super type of other @Unique with any elements @Override - public boolean isSubtype(AnnotationMirror subtype, AnnotationMirror supertype) { + public boolean isSubtypeQualifiers(AnnotationMirror subtype, AnnotationMirror supertype) { // for top and bottom // TODO: shared may have elements in it. if (AnnotationUtils.areSameByName(supertype, SHARED) @@ -116,10 +132,16 @@ public boolean isSubtype(AnnotationMirror subtype, AnnotationMirror supertype) { if (AnnotationUtils.areSameByName(subtype, UNIQUE)) { List supertypeElementList = AnnotationUtils.getElementValueArray( - supertype, "value", String.class, true); + supertype, + uniqueValueElement, + String.class, + Collections.emptyList()); List subtypeElementList = AnnotationUtils.getElementValueArray( - subtype, "value", String.class, true); + subtype, + uniqueValueElement, + String.class, + Collections.emptyList()); // @Unique({}) is super if (supertypeElementList.size() == 0) { return true; @@ -136,7 +158,8 @@ public boolean isSubtype(AnnotationMirror subtype, AnnotationMirror supertype) { } @Override - public AnnotationMirror greatestLowerBound(AnnotationMirror a1, AnnotationMirror a2) { + public AnnotationMirror greatestLowerBoundQualifiers( + AnnotationMirror a1, AnnotationMirror a2) { // 1. shared and shared 2.shared and unique 3. shared and disappear 4.shared and btm // 4. unique and unique 5. unique and disappear 6.unique and btm // 7. disappear and disappear 8. disappear and btm 9.btm and btm @@ -154,9 +177,9 @@ public AnnotationMirror greatestLowerBound(AnnotationMirror a1, AnnotationMirror if (AnnotationUtils.areSameByName(a1, UNIQUE) && AnnotationUtils.areSameByName(a2, UNIQUE)) { List a1ElementList = - AnnotationUtils.getElementValueArray(a1, "value", String.class, true); + AnnotationUtils.getElementValueArray(a1, uniqueValueElement, String.class); List a2ElementList = - AnnotationUtils.getElementValueArray(a2, "value", String.class, true); + AnnotationUtils.getElementValueArray(a2, uniqueValueElement, String.class); if (a1ElementList.size() == 0) { return a2; } else if (a2ElementList.size() == 0) { @@ -167,17 +190,18 @@ public AnnotationMirror greatestLowerBound(AnnotationMirror a1, AnnotationMirror } } // TODO: also think about this - if (AnnotationUtils.areSameByName(a1, UNIQUE) - && AnnotationUtils.areSameByName(a2, DISAPPEAR) - || AnnotationUtils.areSameByName(a1, DISAPPEAR) - && AnnotationUtils.areSameByName(a2, UNIQUE)) { + if ((AnnotationUtils.areSameByName(a1, UNIQUE) + && AnnotationUtils.areSameByName(a2, DISAPPEAR)) + || (AnnotationUtils.areSameByName(a1, DISAPPEAR) + && AnnotationUtils.areSameByName(a2, UNIQUE))) { return DISAPPEAR; } return BOTTOM; } @Override - public AnnotationMirror leastUpperBound(AnnotationMirror a1, AnnotationMirror a2) { + public AnnotationMirror leastUpperBoundQualifiers( + AnnotationMirror a1, AnnotationMirror a2) { // 4. unique and unique 5. unique and disappear // 7. disappear and disappear if (AnnotationUtils.areSameByName(a1, SHARED) diff --git a/src/main/java/org/checkerframework/checker/linear/LinearTransfer.java b/src/main/java/org/checkerframework/checker/linear/LinearTransfer.java index 85c8e67..7438fa2 100644 --- a/src/main/java/org/checkerframework/checker/linear/LinearTransfer.java +++ b/src/main/java/org/checkerframework/checker/linear/LinearTransfer.java @@ -1,8 +1,6 @@ package org.checkerframework.checker.linear; -import com.sun.source.tree.ExpressionTree; import com.sun.source.tree.Tree; -import com.sun.tools.javac.code.Symbol; import org.checkerframework.checker.linear.qual.*; import org.checkerframework.dataflow.analysis.RegularTransferResult; @@ -10,20 +8,23 @@ import org.checkerframework.dataflow.analysis.TransferResult; import org.checkerframework.dataflow.cfg.node.*; import org.checkerframework.framework.flow.*; -import org.checkerframework.framework.util.Contract; -import org.checkerframework.framework.util.ContractsFromMethod; import org.checkerframework.javacutil.AnnotationBuilder; import org.checkerframework.javacutil.AnnotationMirrorSet; import org.checkerframework.javacutil.AnnotationUtils; import java.lang.annotation.Annotation; +import java.util.ArrayList; +import java.util.Collections; import java.util.List; -import java.util.Map; import java.util.Set; import javax.annotation.processing.ProcessingEnvironment; import javax.lang.model.element.AnnotationMirror; -import javax.lang.model.element.ExecutableElement; + +// TODO: +// AnnotationUtils.getElementValueArray(..., Element, String.class, Collections.emptyList()) +// should not need the default argument. It should optionally use the default from the +// annotation declaration, like for the version that takes a name. public class LinearTransfer extends CFAbstractTransfer { @@ -94,7 +95,7 @@ public TransferResult visitAssignment( isRhsUnique = true; break; } else if (AnnotationUtils.areSameByName(atypeFactory.DISAPPEAR, rhsAnnoMirror)) { - return new RegularTransferResult(null, store); + return new RegularTransferResult<>(null, store); } } // Determine the lhs value type. As we don't update rhs annotations(i.e., from unique to @@ -112,7 +113,7 @@ public TransferResult visitAssignment( // 1. RHS is Unique if (isRhsUnique) { // Set RHS node value to disappear if it is Unique before assignment - store.updateForAssignment(rhs, buildNewValue(rhs.getTree(), Disappear.class)); + store.updateForAssignment(rhs, buildNewValue(rhs.getTree(), Disappear.class, null)); // Transfer states from rhs to lhs directly if lhs is also unique. if (isLhsUnique) { store.updateForAssignment( @@ -121,20 +122,29 @@ public TransferResult visitAssignment( lhs.getTree(), Unique.class, AnnotationUtils.getElementValueArray( - rhsAnnotationMirror, "value", String.class, true))); + rhsAnnotationMirror, + atypeFactory.uniqueValueElement, + String.class, + Collections.emptyList()))); } if (isLhsShared) { if (lhsAnnotationMirror != null) { // Merge + List merged = new ArrayList<>(); + merged.addAll( + AnnotationUtils.getElementValueArray( + lhsAnnotationMirror, + atypeFactory.sharedValueElement, + String.class, + Collections.emptyList())); + merged.addAll( + AnnotationUtils.getElementValueArray( + rhsAnnotationMirror, + atypeFactory.uniqueValueElement, + String.class, + Collections.emptyList())); store.updateForAssignment( - lhs, - buildNewValue( - lhs.getTree(), - Shared.class, - AnnotationUtils.getElementValueArray( - lhsAnnotationMirror, "value", String.class, true), - AnnotationUtils.getElementValueArray( - rhsAnnotationMirror, "value", String.class, true))); + lhs, buildNewValue(lhs.getTree(), Shared.class, merged)); } else { // Just transfer store.updateForAssignment( @@ -143,7 +153,10 @@ public TransferResult visitAssignment( lhs.getTree(), Shared.class, AnnotationUtils.getElementValueArray( - rhsAnnotationMirror, "value", String.class, true))); + rhsAnnotationMirror, + atypeFactory.uniqueValueElement, + String.class, + Collections.emptyList()))); } } } @@ -152,15 +165,20 @@ public TransferResult visitAssignment( if (lhsAnnotationMirror != null && rhsAnnotationMirror != null && AnnotationUtils.areSameByName(lhsAnnotationMirror, atypeFactory.SHARED)) { - store.updateForAssignment( - lhs, - buildNewValue( - lhs.getTree(), - Shared.class, - AnnotationUtils.getElementValueArray( - lhsAnnotationMirror, "value", String.class, true), - AnnotationUtils.getElementValueArray( - rhsAnnotationMirror, "value", String.class, true))); + List merged = new ArrayList<>(); + merged.addAll( + AnnotationUtils.getElementValueArray( + lhsAnnotationMirror, + atypeFactory.sharedValueElement, + String.class, + Collections.emptyList())); + merged.addAll( + AnnotationUtils.getElementValueArray( + rhsAnnotationMirror, + atypeFactory.sharedValueElement, + String.class, + Collections.emptyList())); + store.updateForAssignment(lhs, buildNewValue(lhs.getTree(), Shared.class, merged)); } else if (lhsAnnotationMirror == null && rhsAnnotationMirror != null) { store.updateForAssignment( lhs, @@ -168,7 +186,9 @@ public TransferResult visitAssignment( lhs.getTree(), Shared.class, AnnotationUtils.getElementValueArray( - rhsAnnotationMirror, "value", String.class, true))); + rhsAnnotationMirror, + atypeFactory.sharedValueElement, + String.class))); } else if (lhsAnnotationMirror != null && AnnotationUtils.areSameByName(lhsAnnotationMirror, atypeFactory.SHARED)) { store.updateForAssignment( @@ -177,9 +197,11 @@ public TransferResult visitAssignment( lhs.getTree(), Shared.class, AnnotationUtils.getElementValueArray( - lhsAnnotationMirror, "value", String.class, true))); + lhsAnnotationMirror, + atypeFactory.sharedValueElement, + String.class))); } - return new RegularTransferResult(null, store); + return new RegularTransferResult<>(null, store); } TransferResult superResult = super.visitAssignment(n, in); @@ -207,16 +229,12 @@ protected void processCommonAssignment( } protected CFValue buildNewValue( - Tree tree, Class anno, List... states) { + Tree tree, Class anno, List states) { AnnotationMirror newAnnoMirror; AnnotationBuilder builder = new AnnotationBuilder(env, anno); // process states - if (states.length > 0) { - List states1 = states[0]; - if (states.length > 1) { - states1.addAll(states[1]); - } - builder.setValue("value", states1); + if (states != null) { + builder.setValue("value", states); } newAnnoMirror = builder.build(); AnnotationMirrorSet newLhsSet = new AnnotationMirrorSet(); @@ -225,18 +243,20 @@ protected CFValue buildNewValue( newLhsSet, atypeFactory.getAnnotatedType(tree).getUnderlyingType()); } + /* @Override protected void processPostconditions( Node n, CFStore store, ExecutableElement executableElement, ExpressionTree tree) { // TODO: if does not match the signature, then return - if (atypeFactory.atomoton == null) { + if (atypeFactory.automaton == null) { super.processPostconditions(n, store, executableElement, tree); return; } + @SuppressWarnings("unchecked") Map>> operations = (Map>>) - atypeFactory.atomoton.get("operations"); + atypeFactory.automaton.get("operations"); // Check operations if (!operations.containsKey( ((Symbol.MethodSymbol) executableElement).baseSymbol().toString())) { @@ -248,23 +268,21 @@ protected void processPostconditions( operations.get(((Symbol.MethodSymbol) executableElement).baseSymbol().toString()); // Whether the postconditions hold ContractsFromMethod contractsUtils = atypeFactory.getContractsFromMethod(); - Contract.Postcondition[] postconditions = - contractsUtils - .getPostconditions(executableElement) - .toArray( - new Contract.Postcondition - [contractsUtils - .getPostconditions(executableElement) - .size()]); - for (int i = 0; i < postconditions.length; i++) { - AnnotationMirror annotationMirror = postconditions[i].annotation; + Set postConditionSet = + contractsUtils.getPostconditions(executableElement); + for (Contract.Postcondition postCondition : postConditionSet) { + AnnotationMirror annotationMirror = postCondition.annotation; List postStates = AnnotationUtils.getElementValueArray( - annotationMirror, "value", String.class, true); + annotationMirror, atypeFactory.ensureUniqueValueElement, String.class); + // TODO: there currently is no example for this error. + // The check does not pass Error Prone - there is a mismatch between what postStates contains + // and what transition.get returns. if (!postStates.contains(transition.get("after"))) { atypeFactory.getChecker().reportError(tree, "typestate.operation.invalid"); } } super.processPostconditions(n, store, executableElement, tree); } + */ } diff --git a/src/main/java/org/checkerframework/checker/linear/LinearVisitor.java b/src/main/java/org/checkerframework/checker/linear/LinearVisitor.java index 00d5f0e..4769c2f 100644 --- a/src/main/java/org/checkerframework/checker/linear/LinearVisitor.java +++ b/src/main/java/org/checkerframework/checker/linear/LinearVisitor.java @@ -17,6 +17,7 @@ import javax.lang.model.element.AnnotationMirror; import javax.lang.model.type.TypeKind; +@SuppressWarnings("VoidUsed") public class LinearVisitor extends BaseTypeVisitor { final boolean STRONG_BOX_BACKED_ENABLE = checker.getLintOption("strongboxbacked", false); @@ -26,8 +27,10 @@ public class LinearVisitor extends BaseTypeVisitor { /** The @{@link Disappear} annotation. */ protected final AnnotationMirror DISAPPEAR = AnnotationBuilder.fromClass(elements, Disappear.class); + /** The @{@link Unique} annotation. */ protected final AnnotationMirror UNIQUUE = AnnotationBuilder.fromClass(elements, Unique.class); + /** The @{@link Shared} annotation. */ protected final AnnotationMirror MAYALIASED = AnnotationBuilder.fromClass(elements, Shared.class); @@ -119,10 +122,10 @@ public Void visitAssignment(AssignmentTree node, Void p) { && AnnotationUtils.areSameByName(lhsAnnotationMirror, DISAPPEAR)) { checker.reportError(lhs, "disappear.assignment.not.allowed"); } - if (rhsAnnotationMirror != null - && AnnotationUtils.areSameByName(rhsAnnotationMirror, DISAPPEAR) - || lhsAnnotationMirror != null - && AnnotationUtils.areSameByName(lhsAnnotationMirror, DISAPPEAR)) { + if ((rhsAnnotationMirror != null + && AnnotationUtils.areSameByName(rhsAnnotationMirror, DISAPPEAR)) + || (lhsAnnotationMirror != null + && AnnotationUtils.areSameByName(lhsAnnotationMirror, DISAPPEAR))) { checker.reportError(rhs, "disappear.assignment.not.allowed"); } return super.visitAssignment(node, p); @@ -135,8 +138,10 @@ protected boolean validateType(Tree tree, AnnotatedTypeMirror type) { type.getAnnotation(Unique.class) != null ? type.getAnnotation(Unique.class) : type.getAnnotation(Shared.class); - if (atypeFactory.atomoton != null && annotationMirror != null) { - List states = (List) atypeFactory.atomoton.get("states"); + if (atypeFactory.automaton != null && annotationMirror != null) { + @SuppressWarnings("unchecked") + List states = (List) atypeFactory.automaton.get("states"); + @SuppressWarnings("deprecation") List presentStates = AnnotationUtils.getElementValueArray( annotationMirror, "value", String.class, true);