OpenJML internal error when using ESC

[itlchriss]

Hi David,
I am using OpenJML to perform static verification on the apache commons collections4. An internal error is returned once the command is used. For more information, please refer to the information attached below.

Version: openjml 0.17.0-alpha-15
Command: openjml -esc --dir=path_to_src
Error message:

error: A catastrophic JML internal error occurred.  Please report the bug with as much information as you can.
  Reason: Unexpected exception: Exception during parsing near ... coll2) {
          if (coll1.size() < coll2.length) {
     java.lang.NullPointerException: Cannot invoke "org.jmlspecs.openjml.IJmlClauseKind$ModifierKind.isTypeAnnotation()" because "ja.kind" is null
java.lang.NullPointerException: Cannot invoke "org.jmlspecs.openjml.IJmlClauseKind$ModifierKind.isTypeAnnotation()" because "ja.kind" is null
	at jdk.compiler/com.sun.tools.javac.parser.JmlParser.extractTypeAnnotations(JmlParser.java:369)
	at jdk.compiler/com.sun.tools.javac.parser.JmlParser.formalParameter(JmlParser.java:385)
	at jdk.compiler/com.sun.tools.javac.parser.JavacParser.formalParameters(JavacParser.java:4546)
	at jdk.compiler/com.sun.tools.javac.parser.JavacParser.formalParameters(JavacParser.java:4526)
	at jdk.compiler/com.sun.tools.javac.parser.JmlParser.formalParameters(JmlParser.java:403)
	at jdk.compiler/com.sun.tools.javac.parser.JavacParser.methodDeclaratorRest(JavacParser.java:4409)
	at jdk.compiler/com.sun.tools.javac.parser.JavacParser.classOrInterfaceOrRecordBodyDeclaration(JavacParser.java:4273)
	at jdk.compiler/com.sun.tools.javac.parser.JmlParser.classOrInterfaceOrRecordBodyDeclaration(JmlParser.java:1196)
	at jdk.compiler/com.sun.tools.javac.parser.JavacParser.classInterfaceOrRecordBody(JavacParser.java:4154)
	at jdk.compiler/com.sun.tools.javac.parser.JmlParser.classInterfaceOrRecordBody(JmlParser.java:615)
	at jdk.compiler/com.sun.tools.javac.parser.JavacParser.classDeclaration(JavacParser.java:3866)
	at jdk.compiler/com.sun.tools.javac.parser.JmlParser.classDeclaration(JmlParser.java:625)
	at jdk.compiler/com.sun.tools.javac.parser.JavacParser.classOrRecordOrInterfaceOrEnumDeclaration(JavacParser.java:3806)
	at jdk.compiler/com.sun.tools.javac.parser.JmlParser.classOrRecordOrInterfaceOrEnumDeclaration(JmlParser.java:443)
	at jdk.compiler/com.sun.tools.javac.parser.JavacParser.typeDeclaration(JavacParser.java:3791)
	at jdk.compiler/com.sun.tools.javac.parser.JavacParser.parseCompilationUnit(JavacParser.java:3635)
	at jdk.compiler/com.sun.tools.javac.parser.JmlParser.parseCompilationUnit(JmlParser.java:265)
	at jdk.compiler/com.sun.tools.javac.main.JavaCompiler.parse(JavaCompiler.java:620)
	at jdk.compiler/com.sun.tools.javac.main.JmlCompiler.parse(JmlCompiler.java:211)
	at jdk.compiler/com.sun.tools.javac.main.JavaCompiler.parseFiles(JavaCompiler.java:1009)
	at jdk.compiler/com.sun.tools.javac.main.JavaCompiler.parseFiles(JavaCompiler.java:996)
	at jdk.compiler/com.sun.tools.javac.main.JavaCompiler.compile(JavaCompiler.java:922)
	at jdk.compiler/com.sun.tools.javac.main.JmlCompiler.compile(JmlCompiler.java:197)
	at jdk.compiler/com.sun.tools.javac.main.Main.compile(Main.java:321)
	at jdk.compiler/org.jmlspecs.openjml.Main.compile(Main.java:534)
	at jdk.compiler/org.jmlspecs.openjml.Main.execute(Main.java:374)
	at jdk.compiler/org.jmlspecs.openjml.Main.execute(Main.java:332)
	at jdk.compiler/org.jmlspecs.openjml.Main.main(Main.java:295)
	at jdk.compiler/com.sun.tools.javac.Main.main(Main.java:53)
1 error

[itlchriss]

Hi David,
I have further divided the whole package verification into many small module verification by analysing their internal dependency.
Such that, I found the above catastrophic error happens in using ESC on

commons-collections4/src/main/java/org/apache/commons/collections4/collection/CompositeCollection.java

The command attached below is the command to generate the exact error message in the issue:

$OPENJML -cp ${THE_CLASSPATH} $FLAG ./src/main/java/org/apache/commons/collections4/collection/CompositeCollection.java ./src/main/java/org/apache/commons/collections4/iterators/IteratorChain.java ./src/main/java/org/apache/commons/collections4/iterators/EmptyIterator.java ./src/main/java/org/apache/commons/collections4/CollectionUtils.java ./src/main/java/org/apache/commons/collections4/list/UnmodifiableList.java -progress

where THE_CLASSPATH is a dynamic classpath holding the dependency of the library.
I hope you can use these information to review the problem.

Thank you very much
Chriss IT. Leong

[davidcok]

Thanks for this report. On my version of apache/commons/collections4, I get many verification errors but no crash.
Which version of commons collection are you using? Perhaps if you zip up the sources, I could debug it further.

[itlchriss]

Hi David,
I have attached the case in this reply. In the zip file, there are source files with dependency to each other. Thereby, I wrote the command with esc in the esc.bash to verify them together. Please check if my command is correct. The error message from my side is recorded in the CompositeCollection.java.log attached in the zip file.

Thank you very much
Chriss IT. Leong

Environment:
OS:
Distributor ID: Ubuntu
Description: Ubuntu 20.04.3 LTS
Release: 20.04
Codename: focal
OpenJML: openjml-ubuntu-20.04-0.17.0-alpha-15.zip

20220816.zip