JavacExtension does not work with classpath/bootclasspath

[WolframPfeifer]

Description

When a .key/.proof file is loaded which contains a \bootclasspath directive, the Javac extensions crashes.

The bug was originally found by @unp1.

Reproducible

always

Steps to reproduce

1. Load the attached proof bundle bcptest.zip (just change the extension to "zproof").
2. Select the dummy proof, which makes use of the bootclasspath and classpath options.

The Javac extension hangs and never gets out of this state again:

The reason seems to be a wrong parameter that is passed to the Java compiler (-Xbootclasspath):

Exception in thread "AWT-EventQueue-0" java.lang.IllegalArgumentException: error: invalid flag: -Xbootclasspath
	at jdk.compiler/com.sun.tools.javac.main.Arguments.reportDiag(Arguments.java:886)
	at jdk.compiler/com.sun.tools.javac.main.Arguments.doProcessArgs(Arguments.java:396)
	at jdk.compiler/com.sun.tools.javac.main.Arguments.processArgs(Arguments.java:348)
	at jdk.compiler/com.sun.tools.javac.main.Arguments.init(Arguments.java:247)
	at jdk.compiler/com.sun.tools.javac.api.JavacTool.getTask(JavacTool.java:191)
	at jdk.compiler/com.sun.tools.javac.api.JavacTool.getTask(JavacTool.java:119)
	at jdk.compiler/com.sun.tools.javac.api.JavacTool.getTask(JavacTool.java:68)
	at de.uka.ilkd.key.gui.plugins.javac.JavaCompilerCheckFacade.check(JavaCompilerCheckFacade.java:114)
	at de.uka.ilkd.key.gui.plugins.javac.JavacExtension.loadProof(JavacExtension.java:157)
	at de.uka.ilkd.key.gui.plugins.javac.JavacExtension.selectedProofChanged(JavacExtension.java:228)
	at de.uka.ilkd.key.core.KeYSelectionModel.fireSelectedProofChanged(KeYSelectionModel.java:375)
	at de.uka.ilkd.key.core.KeYSelectionModel.setSelectedProof(KeYSelectionModel.java:84)
	at de.uka.ilkd.key.gui.MainWindow.lambda$addProblem$13(MainWindow.java:1190)

If the button is pressed in this state, an NPE is triggered:

Exception in thread "AWT-EventQueue-0" java.lang.NullPointerException: Cannot invoke "java.util.List.isEmpty()" because "data.issues" is null
	at de.uka.ilkd.key.gui.plugins.javac.JavacExtension.lambda$new$0(JavacExtension.java:111)
	at java.desktop/javax.swing.AbstractButton.fireActionPerformed(AbstractButton.java:1972)
	at java.desktop/javax.swing.AbstractButton$Handler.actionPerformed(AbstractButton.java:2314)
	at java.desktop/javax.swing.DefaultButtonModel.fireActionPerformed(DefaultButtonModel.java:407)
	at java.desktop/javax.swing.DefaultButtonModel.setPressed(DefaultButtonModel.java:262)
	at java.desktop/javax.swing.plaf.basic.BasicButtonListener.mouseReleased(BasicButtonListener.java:279)
        ...

Additional information

The issue seems easy to fix at first: When changing "-Xbootclasspath" to "-bootclasspath", at works without error. However, I am not sure if this is the desired behavior: Errors in bootclasspath/classpath can not be detected this way, since with these parameters Java only looks for already compiled classes, and just ignores the .java files (as far as I understand).

What I would expect is that also bootclasspath and classpath directories are checked for compilation errors. However, since we allow Java without method bodies in bootclasspath (and also in classpath, I guess), we can not just run javac on it. This would result in lots of errors. So maybe the only option for now is to ignore bootclasspath/classpath in the extension, and maybe give a warning (at least in the log) that these cannot be checked at the moment.

[WolframPfeifer]

@flo2702 Maybe you can look into this at some point (not urgent in my opinion) ... You changed the relevant lines during #3431. I remember that before this change, many errors were thrown for the classes in bootclasspath. While this was also not a good solution, it indicates that they were just given directly to javac, not via the bootclasspath parameter.

[wadoon]

It is not -Xbootclasspath it is only -bootclasspath.

see https://stackoverflow.com/questions/18270769/javac-bootclasspath-option

---

But this leads to a different question: Java Redux is not compilable with Javac, and I guess that any other "KeY bootclasspath" is also incompilable. (Hint: Methods in classes do not have a body.)

Should we not get rid of the bootclasspath for the Javac extension?

[WolframPfeifer]

I had a discussion with @wadoon about this recently. We agreed that it is not clear at all what we want to have here.
Since JavaRedux is not compilable by javac (missing method bodies), there are multiple options (which all are problematic in one way or another):

1. Get rid of .java files in JavaRedux and only ship .jml files only with the contracts (problem: impossible to add new elements such as ghost fields, model methods).
2. Add mock method bodies to the JavaRedux methods, e.g. return 0 or return null (problem: dangerous, could lead to accidentally inlining the bodies).
3. Ignore bootclasspath in the javac check (problem: if user adds custom JavaRedux, syntax errors in it are not reliably detected. A common case is missing return statements in non-void methods, which is not detected by KeY)

[Drodt]

1. Get rid of .java files in JavaRedux and only ship .jml files only with the contracts (problem: impossible to add new elements such as ghost fields, model methods).

.jml files don't support model methods? Could that not be added? If so, that might be the best option, imo.

[wadoon]

JML files should support model methods. Do they also help the more critical ghost methods/fields?

But my understanding is, that everything that is allowed into the class/type-declaration-level is allowed into the .jml file.

But this also leads to other interesting questions. The .jml files are normally descriptive (describing Java things declared somewhere else) and not declarative.

Where is this "somewhere", e.g., from which source, do we use "java.lang.Object"? Using the JRE and Reflection could give us unexpected (new) methods. Can KeY handle these larger Java models?

In other words, our axiomatic Java base is currently a sub-set but well-defined across any JVM.

[WolframPfeifer]

I also favour the idea with the .jml files. I think we should aim at shipping a version of the classes that is closer to the "real" JDK (at least compilable). Maybe we should try to migrate JavaRedux. However, I vaguely remember that the support for .jml files was debated. Does someone know about that?

I am not aware of any publication, examples, or documentation about .jml files, and there are lots of questions that come to my mind about it:

• What is the current status of .jml files? Which constructs are supported? We would need at least all class-level constructs (at least method contracts, invariants, model fields + represents clauses, model methods, ghost fields, dependency contracts).
• Can there be a .jml file and .java file for the same class (which would introduce possible inconsistency problems)? Is the loading order for .jml files clear?
• How are the contracts in .jml files correlated to the method in the classes? How would inconsistencies be handled (e.g., if a method with that signature does not exist)?
• What if we want to prove a contract of an internal method of the JDK (same problem as with System.arraycopy in current JavaRedux)? Do we want to ship the auxiliary specification (loop invariants, maybe proof scripts) somehow with KeY then?
• I don't think that just shipping .jml files without sources would be a good idea, since the .jml files would then silently refer to the JDK that is currently installed on the system. This would introduce a potential for errors, which would be very difficult to understand and debug. So if we ship .jml files, we should at least ship also the relevant .class files, or better the .java files.

If we agree on what we want, it could actually make a really good HacKeYthon topic again.

[wadoon]

The last discussion was here.

What is the current status of .jml files?

Someone needs to heavily use it for finding possible loopholes. But at the moment the problems seems to be cleared.

Which constructs are supported?

All JML specification on CompilationUnit (like model classes, imports), or BodyDeclaration level (contracts, fields, etc.)

We would need at least all class-level constructs (at least method contracts, invariants, model fields + represents clauses, model methods, ghost fields, dependency contracts).

Included.

Can there be a .jml file and .java file for the same class (which would introduce possible inconsistency problems)? Is the loading order for .jml files clear?

The inconsistency is solved in the thread above: The order in the classpath decides. The highest .jml specs wins alone. All lower-order specs are forgotten/not considered.

How are the contracts in .jml files correlated to the method in the classes? How would inconsistencies be handled (e.g., if a method with that signature does not exist)?

Undefined. I think, at this point, the KeY world and OpenJML would collide.

KeY would be liberal and see .jml axiomatic and the method is declared and denotationally defined.

What if we want to prove a contract of an internal method of the JDK (same problem as with System.arraycopy in current JavaRedux)? Do we want to ship the auxiliary specification (loop invariants, maybe proof scripts) somehow with KeY then?

In JML, there are no Java method bodies. Maybe the concept of the model program can be handy here. Bachelor Thesis?!?

I don't think that just shipping .jml files without sources would be a good idea, since the .jml files would then silently refer to the JDK that is currently installed on the system. This would introduce a potential for errors, which would be very difficult to understand and debug. So if we ship .jml files, we should at least ship also the relevant .class files, or better the .java files.

Fully ack... wait I have an idea....

[WolframPfeifer]

We postponed this work, since a clean solution (where we could use the original JDK source files) would require support for generics (postponed after #3120).

[wadoon]

Short description for my idea from above:

A tool that takes the JDKs src.zip, a folder with .jml files, and a list of required classes (calculated from the bytecode compiled subject to be verified). The result will be a customized JavaRedux.