Support for Java 9

[youk]

As far as I understand, there is no support for upcoming Java 9 as of now. Is this on the roadmap? Or maybe there are workarounds to get going with JDK 9?

[wmdietl]

Half a year ago I worked a bit on this: https://github.com/eisop/checker-framework
Modules changed again since then and I need to update all the repositories.
This is on my to-do list for the next few weeks.

[youk]

Thank you. Do I get this right that annotated JDK 9 is currently non-existent?

[mernst]

That's correct. Many of the existing JDK annotations would transfer over, though the rearrangement of packages/modules makes that a bit harder than when upgrading from (say) JDK 7 to JDK 8.

[Pr0methean]

Since this still isn't fixed, I'm going to have to disable Checker Framework on my project. 😢

[rkraneis]

JDK 9 (and soon 10) support would be very useful.

[mernst]

I agree. It's an important issue for us. If you wish to help, we would welcome assistance.

[avandeursen]

As a work around a possibility is to keep the framework enabled for jdk8, and disable it for jdk9, using maven profiles. See my pom.xml:

SERG-Delft/jpacman-framework@6894f59#diff-600376dffeb79835ede4a0b285078036

[rgoldberg]

What must be updated for Checker to support Java 9 and/or 10?

Is there any large-scale ETA? 1 month, 3 months, 6 months…?

Will Checker then be able to work on multiple Java versions (possibly via a multi-release jar), or just one?

[wmdietl]

We are currently working with a Google Summer of Code student to finish the Java 9 migration.
Our goal is to have a first completely usable version within a month and then finish the migration by the end of summer.

We do not want to maintain multiple versions of the Checker Framework compiler infrastructure.
Most likely by default we will use the Java 9 javac.
If the compiler API doesn't break between versions, that release might continue to be usable with a Java 10/11 compiler.

Please let us know if you want to help with this effort!

[ashishrana160796]

Interested in helping.

[wmdietl]

The version at https://github.com/eisop/checker-framework passes all unit tests: https://travis-ci.org/eisop/checker-framework
The down-stream tests are failing mainly because of configuration issues that should be easy to fix up.
See the Google doc https://docs.google.com/document/d/1mcOJUrYzHDMp2MfPztOmOaaSFjOWZquUN1fO_LCmXuo/edit?usp=sharing for further tasks.

The big blocker currently is producing a version of the annotated JDK that works with Java 9+. @mernst is working on this.
If you do not depend on an annotated JDK (i.e. you do not use the Nullness, Lock, or Index Checkers) it would be great if you could give the eisop version a spin and let us know how things work for your use case.

[ahubold]

If you do not depend on an annotated JDK (i.e. you do not use the Nullness, Lock, or Index Checkers) it would be great if you could give the eisop version a spin and let us know how things work for your use case.

I tried to use it with our custom checker but I run into the following error:

org.checkerframework.javacutil.UserError: The Checker Framework must be run under JDK 8.  You are using version 1.

I'm using Java 11 here - not Java 1, of course ;-)

The test seems to be too strict at

https://github.com/eisop/checker-framework/blob/6c838ec0596409538bc54e52e96b2626cb1760a3/framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java#L453

[wmdietl]

@ahubold I've pushed several changes that now allow me to build with JDK 8, 9, 10, and 11! It was quite a bit more than just this version check, as several APIs changed over the different versions.

All tests pass with JDK 8. For the others the big issue is adding a side-channel for the annotated JDK; however, also a few other things where we interact with the compiler broke, e.g. some expression parsing with packages isn't working right now.

Please take a look and let me know how well this works for you:
https://github.com/eisop/checker-framework

[ahubold]

@wmdietl Thank you! That already looks quite good.

I still got an error when building the Checker Framework with Oracle OpenJDK 11.0.2. I was able to build it with Java 8 and test with Java 11 then. This was the build error with Java 11, in case you're interested:

find ../src/cf-jdk-additions -name "*.java" | xargs javac -d ./jdk-additions-out
../src/cf-jdk-additions/java/util/spi/ToolProvider.java:26: error: package exists in another module: java.base
package java.util.spi;
^
1 error
make: *** [classes] Error 123
Makefile:6: recipe for target 'classes' failed

> Task :cloneAndBuildDependencies FAILED

The tests for our custom checker run successfully with Java 11 now 👍 , so I tried to run the checker on our source code and it works! 👍 Except for one subtle case: It throws an error for the following complicated code. This error wasn't thrown with Java 8 and previous versions of the Checker Framework. (I've reduced the example, so the code doesn't really make sense anymore):

import java.util.ArrayList;
import java.util.List;

class Test {

  private static void test(List<?> a, List<?> b) {
    List<Other.Entry<Object>> result = new Other<>(a, b).compute();
  }

  static class Other<T> {
    private List<? extends T> a, b;

    Other(List<? extends T> a, List<? extends T> b) {
      this.a = a;
      this.b = b;
    }

    List<Entry<T>> compute() {
      return new ArrayList<>();
    }

    public static class Entry<T> {
    }
  }
}

The error is:

:-1: other: error: AsSuperVisitor: type is not an erased subtype of supertype.
  type: @NonPersonalData Object
  superType: @NonPersonalData Entry<@NonPersonalData Object>
  Compilation unit: tests/test-files/Test.java
  Last visited tree at line 7 column 5:
      List<Other.Entry<Object>> result = new Other<>(a, b).compute();
  Exception: java.lang.Throwable; Stack trace: org.checkerframework.javacutil.BugInCF.<init>(BugInCF.java:25)
  org.checkerframework.framework.type.AsSuperVisitor.errorTypeNotErasedSubtypeOfSuperType(AsSuperVisitor.java:154)
  org.checkerframework.framework.type.AsSuperVisitor.visitDeclared_Declared(AsSuperVisitor.java:350)
...

I haven't checked if there's a bug in our checker or if this is a general problem. Maybe this is one of the "few other things" that are still open? Anyway, it's easy to workaround by extracting new Other<>(a, b) into a local variable:

    Other<Object> other = new Other<>(a, b);
    List<Other.Entry<Object>> result = other.compute();

We're really looking forward to a CF release that supports Java 11. If the work on the annotated JDK still takes some time, maybe it's an option to build a beta release without that support?

Thank you and keep up the good work! 👍

[wmdietl]

@ahubold Thanks for testing!

1. Nobody has adapted the upstream projects yet. I'll take a look.

2. Thanks for the new test. I didn't find a reason why that would start failing, so I added a work-around that tries to avoid a whole lot of work. Please let me know whether that works for you now.

3. Having a beta release is a good idea to sort out any remaining bugs.

[ahubold]

Please let me know whether that works for you now.

Yes, works for me. Thank you.

[aprantl]

What are you thinking about the beta release? We had to deactivate our checker-framework related validation tasks because it does not work with Java 11. We would use the beta just to turn on the validation again.

[wmdietl]

Sorry about the delay on this. I'll try to get to #2294 and then I can make a release of the framework artifact from https://github.com/eisop/checker-framework
The Nullness Checker and the other checkers that use the annotated JDK are still blocked on finding an alternative format, see #1224 (comment) .

[rgoldberg]

Do you have an ETA for this?

Will there be any limitations for the initial rollout of this? (e.g., Nullness, Lock, & Index Checkers not working)

If Nullness, Lock, & Index Checkers (or any other optional functionality) are holding this back, could you release a version (possibly an alpha or beta) that works on Java 9 for most functionality, and later add support the optional functionality?

What Java versions will be supported besides 9? 8, 10, 11, 12, etc.?

Thanks.

[Pr0methean]

Supporting JDK 11 will greatly expand the pool of potential beta testers. JDK 9 and 10 account for only about 1 in 9 Docker downloads, and less than 1 in 700 standalone downloads, at AdoptOpenJDK (one of the few trusted sources that even builds those versions anymore).

[wmdietl]

I made a release of artifacts that should work with Java 9 to 12:
https://search.maven.org/search?q=io.github.eisop
(Once it syncs to Maven Central...)

Sources for this version continue to be at https://github.com/eisop/checker-framework

The Java 12 preview switch expressions are not supported, tracked at #2373 .
The release adds a new framework-all artifact, which should contain everything needed for a custom type system.
A demo project, under docs/examples, will be added soon.

For simplicity, I didn't include the checker artifact, because the annotated JDK needed for Nullness and other type systems currently doesn't work with Java 9+. A stripped checker artifact could be added, if there is need for one.

One big caveat is that the annotated JDK also contains side-effect information. Without this, flow-sensitive refinement will be a bit coarser. Stub files can still be used to provide such information.
It should be possible to write a script to extract all side-effect information from the annotated JDK into a stand-alone stub file.

Contributions are always very welcome.

[ahubold]

I tried the io.github.eisop:*:3.0.0-b1 release with Java 11 but ran into some issues and did not get it to work with our custom checker.

The Maven POMs have some errors in their dependencies, which I could work around:

1. framework-all does not contain/depend on everything that is needed for a custom checker. I had to manuall add a dependency to io.github.eisop:javacutil so that org.checkerframework.javacutil.AbstractTypeProcessor is available for compilation
2. javacutil has a dependency on org.checkerframework:checker-qual:3.0.0-b1, which does not exist - the groupId should be io.github.eisop.
3. framework-test has a dependency on org.checkerframework:javacutil:3.0.0-b1, which does not exist. - the groupId should be io.github.eisop.

I was then able to compile our custom checker and start its tests (based on framework-test), but got an exception

Caused by: java.lang.ClassCastException: class jdk.internal.loader.ClassLoaders$AppClassLoader cannot be cast to class java.net.URLClassLoader (jdk.internal.loader.ClassLoaders$AppClassLoader and java.net.URLClassLoader are in module java.base of loader 'bootstrap')
	at org.checkerframework.framework.source.SourceChecker.logBugInCF(SourceChecker.java:820)
	at org.checkerframework.framework.source.SourceChecker.typeProcessingStart(SourceChecker.java:875)
	at com.coremedia.common.personaldata.checker.PersonalDataChecker.typeProcessingStart(PersonalDataChecker.java:72)

which is related to a cast of the system class loader to URLClassLoader, which does not work in Java 9 anymore, see for example https://blog.codefx.org/java/java-9-migration-guide/#Casting-To-URL-Class-Loader

The code just tries to output an error, so I debugged into the code and the original error is

java.lang.reflect.InvocationTargetException
	at java.base/jdk.internal.reflect.NativeConstructorAccessorImpl.newInstance0(Native Method)
	at java.base/jdk.internal.reflect.NativeConstructorAccessorImpl.newInstance(NativeConstructorAccessorImpl.java:62)
	at java.base/jdk.internal.reflect.DelegatingConstructorAccessorImpl.newInstance(DelegatingConstructorAccessorImpl.java:45)
	at java.base/java.lang.reflect.Constructor.newInstance(Constructor.java:490)
	at org.checkerframework.common.basetype.BaseTypeChecker.invokeConstructorFor(BaseTypeChecker.java:274)
	at org.checkerframework.common.basetype.BaseTypeChecker.createSourceVisitor(BaseTypeChecker.java:212)
	at org.checkerframework.common.basetype.BaseTypeChecker.createSourceVisitor(BaseTypeChecker.java:84)
	at org.checkerframework.framework.source.SourceChecker.initChecker(SourceChecker.java:896)
	at org.checkerframework.common.basetype.BaseTypeChecker.initChecker(BaseTypeChecker.java:99)
...
Caused by: java.lang.NoClassDefFoundError: org/checkerframework/dataflow/analysis/Analysis
	at java.base/java.lang.ClassLoader.defineClass1(Native Method)
	at java.base/java.lang.ClassLoader.defineClass(ClassLoader.java:1016)
	at java.base/java.security.SecureClassLoader.defineClass(SecureClassLoader.java:174)
	at java.base/jdk.internal.loader.BuiltinClassLoader.defineClass(BuiltinClassLoader.java:802)
	at java.base/jdk.internal.loader.BuiltinClassLoader.findClassOnClassPathOrNull(BuiltinClassLoader.java:700)
	at java.base/jdk.internal.loader.BuiltinClassLoader.loadClassOrNull(BuiltinClassLoader.java:623)
	at java.base/jdk.internal.loader.BuiltinClassLoader.loadClass(BuiltinClassLoader.java:581)
	at java.base/jdk.internal.loader.ClassLoaders$AppClassLoader.loadClass(ClassLoaders.java:178)
	at java.base/java.lang.ClassLoader.loadClass(ClassLoader.java:521)
	at java.base/java.lang.Class.forName0(Native Method)
	at java.base/java.lang.Class.forName(Class.java:315)
	at org.checkerframework.common.basetype.BaseTypeChecker.invokeConstructorFor(BaseTypeChecker.java:263)
	at org.checkerframework.common.basetype.BaseTypeVisitor.createTypeFactory(BaseTypeVisitor.java:261)
	at org.checkerframework.common.basetype.BaseTypeVisitor.<init>(BaseTypeVisitor.java:220)
	at org.checkerframework.common.basetype.BaseTypeVisitor.<init>(BaseTypeVisitor.java:209)
	at com.coremedia.common.personaldata.checker.PersonalDataVisitor.<init>(PersonalDataVisitor.java:16)

org/checkerframework/dataflow/analysis/Analysis is not contained in framework-all but seems to be required for a custom type system. I added a dependency to io.github.eisop:dataflow:3.0.0-b1 then, which has wrong group ids for its dependencies, so I had to exclude its org.checkerframework:checker-qual and org.checkerframework:javacutil dependencies.

I then got the next error

Caused by: java.lang.NoClassDefFoundError: com/github/javaparser/ast/body/TypeDeclaration
	at org.checkerframework.framework.type.AnnotatedTypeFactory.parseStubFiles(AnnotatedTypeFactory.java:3072)
	at org.checkerframework.framework.type.GenericAnnotatedTypeFactory.postInit(GenericAnnotatedTypeFactory.java:247)
	at com.coremedia.common.personaldata.checker.PersonalDataAnnotatedTypeFactory.<init>(PersonalDataAnnotatedTypeFactory.java:25)
	... 63 more
Caused by: java.lang.ClassNotFoundException: com.github.javaparser.ast.body.TypeDeclaration
	at java.base/jdk.internal.loader.BuiltinClassLoader.loadClass(BuiltinClassLoader.java:583)
	at java.base/jdk.internal.loader.ClassLoaders$AppClassLoader.loadClass(ClassLoaders.java:178)
	at java.base/java.lang.ClassLoader.loadClass(ClassLoader.java:521)
	... 66 more

This class was part of the checker.jar (at least in 2.5.7) but I cannot find it in the io.github.eisop release.

So I had to give up here.

@wmdietl Maybe the stripped checker artifact you were talking about contains these classes. Could you provide that one?

[wmdietl]

@ahubold Thanks a lot for your detailed investigation and sorry for the serious mistakes in that first release.
I've made a second version 3.0.0-b2, which should have a working framework-all artifact with all dependencies in it.

There is also a small example using the Value Checker: https://github.com/eisop/checker-framework/tree/master/docs/examples/MavenExample-framework-all
Once the release is promoted this test should pass.

I also release all artifacts under io.github.eisop and integrated in the build process, making the process less error-prone.
There is still some work left to handle all dependencies correctly. framework-all includes everything and should work. framework still needs some additional dependencies (e.g. to the AFU and StubParser) to work - those projects don't have artifacts yet.

Thanks again for the feedback and please let me know if this one works better.

[ahubold]

@wmdietl Thank you.

The io.github.eisop:framework-test still has a transitive dependency to org.checkerframework:checker-qual (wrong groupId) of even different versions as reported by the dependencyConvergence report of the Maven enforcer plugin. But I can simply exclude that dependency.

Dependency convergence error for org.checkerframework:checker-qual:2.6.0 paths to dependency are:
+-...
  +-io.github.eisop:framework-test:3.0.0-b2
    +-io.github.eisop:javacutil:3.0.0-b2
      +-org.plumelib:plume-util:1.0.6
        +-org.checkerframework:checker-qual:2.6.0
and
+-...
  +-io.github.eisop:framework-test:3.0.0-b2
    +-io.github.eisop:javacutil:3.0.0-b2
      +-org.plumelib:plume-util:1.0.6
        +-org.plumelib:reflection-util:0.0.2
          +-org.checkerframework:checker-qual:2.5.5
and
+-...
  +-io.github.eisop:framework-test:3.0.0-b2
    +-io.github.eisop:javacutil:3.0.0-b2
      +-org.plumelib:plume-util:1.0.6
        +-org.plumelib:require-javadoc:0.1.0
          +-org.checkerframework:checker-qual:2.5.4

Our tests now always show the following error:

tests/test-files/MethodCalls.java:6: warning: [inconsistent.constructor.type] Constructor type (@NonPersonalData) cannot be statically verified.
public class MethodCalls {

The tested class does not have an explicit constructor in the Java source. I'm not quite sure what this means but the behavior seems to have changed here with eisop@04b377e and broke our custom checker. It used to work with Checker Framework 2.5.7.

In our type system, we have the qualifier @PersonalData at the top and @NonPersonalData as subtype. The subtype is the default annotation. The use case here is that we track the usage of personal data in our code and explicitly annotate types that hold personal data.

[wmdietl]

Thanks for testing!

1. The transitive dependency problem probably also exists with the org.checkerframework artifacts - at least there are different versions in the different chains. I don't know what to do about this. Can you file an issue with a simple test?

2. This is a change of behavior that is not specific to Java 9. You can adapt the logic in BaseTypeVisitor::checkConstructorResult to suit your needs:
   https://github.com/typetools/checker-framework/blob/master/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java#L710
   I would suggest opening a separate issue if there are problems with this.

So overall this sounds like things are working as expected.
Are you using Java 11? Or what version are you using?

[ahubold]

wrt 1) You're probably right. I didn't notice the different versions when using the org.checkerframework artifacts because in that case I'd manage the version of checker-qual myself in my project. This just popped up because of the different groupId io.github.eisop

wrt 2) Yes, this really seems to be unrelated. Sadly, even after overriding the mentioned method, our checker reports more false positives. I still need to check that, but will take the discussion elsewhere, if needed.

Yes, I'm using Java 11. I cannot say if it really works now, because I'm still unable to run our checker on our code base - because of the changed behavior of the framework.

[smillst]

The transitive dependency problem will be fixed in the next release of the org.checkerframework artifacts. @wmdietl should be able to use the same fix for the io.github.eisop artifacts. Thanks for the report!

checker-framework/maven-artifacts/release/javacutilReleasePom.xml

Lines 37 to 50 in c57933b

	<dependency>
	<groupId>org.plumelib</groupId>
	<artifactId>plume-util</artifactId>
	<!-- Keep version number in sync with ../../javacutil/build.gradle . -->
	<version>1.0.6</version>
	<type>jar</type>
	<exclusions>
	<exclusion>
	<groupId>org.checkerframework</groupId>
	<artifactId>checker-qual</artifactId>
	</exclusion>
	</exclusions>
	</dependency>
	</dependencies>

[rgoldberg]

is there any ETA, or anticipated release version, for Java 9 support?

How much additional work will be required to support Java 10, 11, 12, 13, etc.?

[mernst]

Version 3.0.0 will support Java 11. (Java 9 isn't supported by Oracle any more.)
We are working very hard on that. We expect it to be released by early September, barring unforeseen difficulties.

If you are willing to help with testing or other tasks, we would gratefully accept assistance.

[rgoldberg]

I haven’t really used Checker that much, so I’m probably not the best person to test it; I was waiting for current Java version support & hopefully improved tooling support, possibly through common annotations. If I get a chance to try it soon, I’ll let you know if I run into any issues.

[mernst]

If you wait for common annotations, you may wait for years.
The testing would be with our development branch.
Feedback by new users is always great -- it tells us what is obvious to us but not to people who haven't used it before.

[Pr0methean]

Lacking annotations for the nullness and initialization checkers probably makes the pool of potential testers very small. For me, those were the entire use case for Checker Framework, and custom checkers are a solution in search of a problem.

[mernst]

1. There do exist annotations for nullness and initialization checkers. (Not standard ones, but that is not stopping anyone.) If you mean "lacking annotations in the JDK", we are working on that.
2. Many users are using other custom checkers. I'm sorry you have not yet discovered a use for them, but this thread is not the place for such a discussion.

[smillst]

Support for JDK 9+ was added in 3.0.0 release of the Checker Framework. JDK annotations for Java 11 are included in checker.jar, too.