Assertions in ifs raise exceptions

mattulbrich commented 1 year ago

Description

Using assertions as ~last~ statement inside an (otherwise empty) if-then-block raises a class cast exception

Reproducible

always.

Steps to reproduce

Try to load:

class A {
    //@ ensures true;
    void m() {        
        if(true) {
            //@ assert true;
        } else {
        }            
    }
}

into KeY. It should load, but it will fail while converting to KeY data structures.

Adding a {} after assertion (like in the old days ...) resolves the problem

Additional information

de.uka.ilkd.key.java.ConvertException: class recoder.java.statement.If cannot be cast to class recoder.java.StatementBlock (recoder.java.statement.If and recoder.java.StatementBlock are in unnamed module of loader 'app')
    at de.uka.ilkd.key.java.Recoder2KeY.reportErrorWithPositionInFile(Recoder2KeY.java:1246)
    at de.uka.ilkd.key.java.Recoder2KeY.reportError(Recoder2KeY.java:1236)
    at de.uka.ilkd.key.java.Recoder2KeY.recoderCompilationUnitsAsFiles(Recoder2KeY.java:393)
    at de.uka.ilkd.key.java.Recoder2KeY.readCompilationUnitsAsFiles(Recoder2KeY.java:292)
    at de.uka.ilkd.key.proof.init.ProblemInitializer.readJava(ProblemInitializer.java:282)
    at de.uka.ilkd.key.proof.init.ProblemInitializer.prepare(ProblemInitializer.java:520)
    at de.uka.ilkd.key.proof.init.ProblemInitializer.prepare(ProblemInitializer.java:455)
    at de.uka.ilkd.key.proof.io.AbstractProblemLoader.createInitConfig(AbstractProblemLoader.java:518)
    at de.uka.ilkd.key.proof.io.AbstractProblemLoader.loadEnvironment(AbstractProblemLoader.java:288)
    at de.uka.ilkd.key.proof.io.AbstractProblemLoader.load(AbstractProblemLoader.java:252)
    at de.uka.ilkd.key.proof.io.ProblemLoader.doWork(ProblemLoader.java:65)
    at de.uka.ilkd.key.proof.io.ProblemLoader$1.doInBackground(ProblemLoader.java:118)
    at de.uka.ilkd.key.proof.io.ProblemLoader$1.doInBackground(ProblemLoader.java:111)
    at java.desktop/javax.swing.SwingWorker$1.call(SwingWorker.java:304)
    at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:264)
    at java.desktop/javax.swing.SwingWorker.run(SwingWorker.java:343)
    at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1128)
    at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:628)
    at java.base/java.lang.Thread.run(Thread.java:829)
Caused by: java.lang.ClassCastException: class recoder.java.statement.If cannot be cast to class recoder.java.StatementBlock (recoder.java.statement.If and recoder.java.StatementBlock are in unnamed module of loader 'app')
    at de.uka.ilkd.key.java.recoderext.JMLTransformer.transformAssertStatement(JMLTransformer.java:388)
    at de.uka.ilkd.key.java.recoderext.JMLTransformer.transformMethodlevelCommentsHelper(JMLTransformer.java:556)
    at de.uka.ilkd.key.java.recoderext.JMLTransformer.transformMethodlevelCommentsHelper(JMLTransformer.java:523)
    at de.uka.ilkd.key.java.recoderext.JMLTransformer.transformMethodlevelCommentsHelper(JMLTransformer.java:523)
    at de.uka.ilkd.key.java.recoderext.JMLTransformer.transformMethodlevelComments(JMLTransformer.java:565)
    at de.uka.ilkd.key.java.recoderext.JMLTransformer.makeExplicit(JMLTransformer.java:684)
    at de.uka.ilkd.key.java.recoderext.RecoderModelTransformer.transform(RecoderModelTransformer.java:222)
    at recoder.kit.TwoPassTransformation.execute(TwoPassTransformation.java:91)
    at de.uka.ilkd.key.java.Recoder2KeY.transformModel(Recoder2KeY.java:829)
    at de.uka.ilkd.key.java.Recoder2KeY.recoderCompilationUnitsAsFiles(Recoder2KeY.java:384)
    ... 16 more

I seem to remember that Alexander @wadoon implemented the improved parsing of JML comments, that's why I initially assign this issue to him.

Commit: ae839323f6c11eb1504dd43934c5d58e86166c9a i.e. current main

EDIT: Corrected the description from "last statement" to "statement inside empty block". Last statement works, see also my comment with ; //@ assert true; below. @lks9

wadoon commented 1 year ago

I think the last one working in this area was @lks9.

I think one problem is, that the JML comments need a node to be attached to. In this case there is node/statement.

We need to add an empty statement ;.

lks9 commented 1 year ago

Ok, now that I am back in europe, I looked into it. The problem seems to be that recorder or KeY simplifies the empty block away. So

if(true) {
            //@ assert true;
        }

becomes

if (true)
            //@ assert true;
        ;

And

if (true)
     //@ assert true;
     x = 0;

gets the same exception. I don't think that the these forms should be supported.

This cannot be handled in the comment attachment code I submitted as the {} removal happens before. So I am unassigning myself.

{} gets simplified to ; and {;} not. So the problem is only indirectly a missing ;.

But the workaround is as @wadoon said:

if(true) {
            ;
            //@ assert true;
        }

KeYProject / key