The Removal of Recoder

[wadoon]

This PR replaces recoder by javaparser, or more precisely by key-javaparser.
The special version has support for ProofJava, SchemaJava and Java 17+, all in one grammar.

Notes on the grammar can be found in the key-docs

This MR requires a complete overhaul of the KeY-Infrastructure.

Status:

• Migration of KeY/Java transformations from recoder to javaparser
  • Get compile-error free for testing
  • Check JavaInfo for unused methods and delete them
  • Testing (wip)
    • Currently there is one transformation example
    • JavaRedux is parsed and translated.
    • Tests for translation from JP-AST to KeY-AST
• Reimplementing the old infrastructure on top of Javaparser
• Tests
  • What to do with TestProofJavaParser and TestSchemaJavaParser?
  • TestKeYRecoderMapping
• Activate the new implementation.

[github-actions]

Thank you for your contribution.

The test artifacts are available on Artiweb.
The newest artifact is here.

[wadoon]

@jwiesler Sources of key-javaparser are now available via maven.

[jwiesler]

About NameInfo: How do we find what is actually needed by KeY from this interface, I've checked a few methods and many of them are just used by Recoder.

Edit: Took a look around and I didn't find any usages outside of the XX2KeY-converters.

[wadoon]

contraposition loads again.

Syntax changes to catch #cs were necessary.

[jwiesler]

@wadoon tests are not able to resolve java.lang.Object. Since you wrote this dynamic symbol solver, could you take a look?

Edit: This seems to be the issue everywhere. I'm not sure how to fix this or continue with this error.

[wadoon]

@wadoon tests are not able to resolve java.lang.Object. Since you wrote this dynamic symbol solver, could you take a look?

Is this the error message of

Caused by: UnsolvedSymbolException{context='null', name='$initialized', cause='null'}

This is not caused by unresolving java.lang.Object. It is caused because the wrong java.lang.Object is resolved. It is a ReflectionClassDeclaration and so it is not the Redux class.

And this is correct as useSystemClassLoaderInResolution was set. I think we should disable this option

[jwiesler]

Nope, what I meant is this one (thrown by most tests):

Unsolved symbol in de.uka.ilkd.key.java.JavaParserFactory$DynamicTypeSolver@3856d0cb : java.lang.Object
UnsolvedSymbolException{context='de.uka.ilkd.key.java.JavaParserFactory$DynamicTypeSolver@3856d0cb', name='java.lang.Object', cause='null'}
	at com.github.javaparser.resolution.TypeSolver.solveType(TypeSolver.java:71)
	at de.uka.ilkd.key.java.JP2KeYTypeConverter.getKeYJavaType(JP2KeYTypeConverter.java:125)
	at de.uka.ilkd.key.java.JP2KeYTypeConverter.<init>(JP2KeYTypeConverter.java:89)
	at de.uka.ilkd.key.java.JavaService.<init>(JavaService.java:967)
	at de.uka.ilkd.key.java.JavaService.<init>(JavaService.java:958)

However, I did see the one you mentioned and thought it would be the same error.

[wadoon]

I am stuck at the circular problem:

1. The symbol solver loads CompilationUnits via JavaParserTypeSolver requested upon type resolution.
2. KeY loads Redux in one chunk in parseLibraryClasses0, incl. pre-transformation.

During the pre-transformation in (2), we resolve java.lang.Object which triggers (1), and which resolves into a different java.lang.Object entity.

Options:

1. We hack parseLibraryClasses0 s.t. the JavaParserTypeSolver is replaced with a special type solver, which operates on the list of compilation units.

2. We avoid the ahead-of-time parsing of JavaRedux. Implement our pre-transformation as post-processors for the JavaParser and hope that everything works just-in-time. This would require, that type resolution is used to obtain classes.

   • Disadvantage: Closed-program analyses not possible.
   • Advantage: Speed. Only necessary, reachable parts of JavaRedux are hit.

[wadoon]

Nope, what I meant is this one (thrown by most tests):

Could you point me to one test case?

[jwiesler]

E.g. TestDeclParser::testGenericSortDecl1, TestTermParser::testNotEqual

But you're right the remaining tests have the problem with $initialized. The two mentioned classes use a weird setup method, maybe the issue is initialization.

[wadoon]

We have an error in the pre-transformation pipeline. arg0 can not be resolved in the code below. Looking at the generated (excerpt below), we see the generation has produced garbage code: super(...) is only allowed at the beginning of a constructor.

 @($classInitializationInProgress) = true;
        try {
            @(java.lang.RuntimeException.$clinit());
            {
                super();
            }
            {
                super(arg0);
            }
        }//Created by ClassInitializeMethodBuilder.java:188
         catch (java.lang.Error err) {
            //Created by ClassInitializeMethodBuilder.java:148
            @($classInitializationInProgress) = true;
            //Created by ClassInitializeMethodBuilder.java:149
            @($classErroneous) = true;
            throw err;
        } catch (java.lang.Throwable twa) {
            //Created by ClassInitializeMethodBuilder.java:148
            @($classInitializationInProgress) = true;
            //Created by ClassInitializeMethodBuilder.java:149
            @($classErroneous) = true;
            throw new java.lang.ExceptionInInitializerError(twa);
        }

Complete:

package java.lang;

public class ArithmeticException extends java.lang.RuntimeException {

    public ArithmeticException() {
        super();
    }

    public ArithmeticException(java.lang.String arg0) {
        super(arg0);
    }

    @javax.annotation.processing.Generated()
    static private boolean $classInitializationInProgress;

    @javax.annotation.processing.Generated()
    static private boolean $classErroneous;

    @javax.annotation.processing.Generated()
    static private boolean $classInitialized;

    @javax.annotation.processing.Generated()
    static private boolean $classPrepared;

    static private void $clprepare() {
    }

    static public void $clinit() {
        if (!@($classInitialized)) {
            if (!@($classInitializationInProgress)) {
                if (!@(this.$classPrepared)) {
                    //Created by ClassInitializeMethodBuilder.java:213
                    @($clprepare());
                }
                if (@($classErroneous)) {
                    throw new java.lang.NoClassDefFoundError();
                }
                //Created by ClassInitializeMethodBuilder.java:237
                @($classInitializationInProgress) = true;
                try {
                    @(java.lang.RuntimeException.$clinit());
                    {
                        super();
                    }
                    {
                        super(arg0);
                    }
                }//Created by ClassInitializeMethodBuilder.java:188
                 catch (java.lang.Error err) {
                    //Created by ClassInitializeMethodBuilder.java:148
                    @($classInitializationInProgress) = true;
                    //Created by ClassInitializeMethodBuilder.java:149
                    @($classErroneous) = true;
                    throw err;
                } catch (java.lang.Throwable twa) {
                    //Created by ClassInitializeMethodBuilder.java:148
                    @($classInitializationInProgress) = true;
                    //Created by ClassInitializeMethodBuilder.java:149
                    @($classErroneous) = true;
                    throw new java.lang.ExceptionInInitializerError(twa);
                }
                //Created by ClassInitializeMethodBuilder.java:243
                @($classInitializationInProgress) = false;
                //Created by ClassInitializeMethodBuilder.java:245
                @($classErroneous) = false;
                //Created by ClassInitializeMethodBuilder.java:247
                @($classInitialized) = true;
            }
        }
    }

    protected void $prepare() {
    }

    private void $prepareEnter() {
    }

    public ArithmeticException $create() {
        //Created by CreateBuilder.java:53
        this.$initialized = false;
        $prepareEnter();
        return this;
    }

    public static ArithmeticException $createObject() {
        ArithmeticException __NEW__;
        //Created by CreateObjectBuilder.java:67
        __NEW__ = ArithmeticException.$allocate();
        __NEW__.$create()@ArithmeticException
        return __NEW__;
    }
}

[jwiesler]

@wadoon fixed it.

New issues are:

• Lots of duplicate registration of XX that should not happend (many of them are definitely not the same)
• TestJP2KeY: Unsolved symbol java.lang.Object, int (?!) and parsing errors Illegal left hand side of an assignment
• testTypeNotInScopeShouldNotBeFound: Something with type resolution in method frames is corrupt (no idea what the issue is here)
• TestJavaInfo: Some fields are not found, e.g. Did not find locally declared attribute $created. I suspect this is because of my first point.

[wadoon]

• Lots of duplicate registration of XX that should not happend (many of them are definitely not the same)

This may arise by two things: (1) I believe that the SchemaJavaParser has not used Recoder2KeY mapping, (2) there might be differences in #equals.

[wadoon]

• TestJP2KeY: Unsolved symbol java.lang.Object, int (?!) and parsing errors Illegal left hand side of an assignment

int problem fixed. Use of wrong class new ClassOrInterfaceType("int"); instead of new PrimitiveType(Primtive.INT).

Test case fails, as it is expected that i in { i = 2; } is the same instance as provided in the creation of the context.

Unknown if this is really required.

[wadoon]

• Illegal left hand side of an assignment

There are some simple checks inside JavaParser, look into CommonValidators.java.
There are some strange expression. How should the precedence?
We have ... && i+=j && i=j && .... The JavaParser interpretes this as
(... && i) += (j && i=j && ...).

Case fixed with parenthesis.

[wadoon]

Progress on TestJP2KeY. The current problem is in

        return new LocalVariableDeclaration(pi, c, modifiers, type, isInInterface, vars);

in JP2KeYConverter.java. Type is given twice, which results into pretty-printing int int i;. It is unclear which type should be erased.

On this corner, the KeY-Java-AST is broken. @unp1 @mattulbrich

[wadoon]

• testTypeNotInScopeShouldNotBeFound: Something with type resolution in method frames is corrupt (no idea what the issue is here)

The KeY file loads typeResolutionInMethodFrame.key which uses a class by its simple name. But this class is inside a package, and therefore it should not be resolved.

The loaded proof looks as follows:

Proof -- UpdatetermTest
Prooftree:

(1) []==>[\<{
  test.test.TestJavaCardDLExtensions test.TestJavaCardDLExtensions
    t = null;
}\> (true)]

Originally, it is \<{ TestJavaCardDLExtensions t = null; }\> true.

The double type declaration is problem of LocalVariableDeclaration (see above). But why/how JavaParser is able to resolve the class... I do not know.

[wadoon]

• TestJavaInfo: Some fields are not found, e.g. Did not find locally declared attribute $created. I suspect this is because of my first point.

No. The patched java.lang.Object is found and in asKeYFields the $created is present.
But this FieldDeclaration has not pass the jp2key converter and therefore the lookup fails.
You have added the following line, which is tirggered:

LOGGER.debug("Field has no KeY equivalent (recoder field): {}", rf);

The problem is that not everything that is visited by jp2key converter is stored in the conversion map.

FIXED

[jwiesler]

Converting ArrayCreationExpr currently fails. The problem is that KeY-ast's NewArray is basically undocumented and the valid array creation expression new int[5][4][][] simply crashes recoder. The only two working cases are new int[5][4][3][2] (all brackets have an expression) and new int[][][][] = expr (initializer). So how should this be represented in KeY-ast?

@mattulbrich @wadoon

[jwiesler]

Furthermore, javaparser does not associate a type to ArrayInitializerExpr (throws an UnsupportedOperationException). I guess this makes sense, since they don't have a specific type on their own.
However, KeY-ast requires a type for them (I don't think it is ever used).

[wadoon]

I guess this makes sense, since they don't have a specific type on their own

Concentrate on the possible things. We do not want to repair the KeY-Java-AST.

I am not sure on the type resolution.

• There are typed array initialization: new int[] {1,2,3}. I guess that JavaParser is able to infer type.

• There are untyped array initialization: int[] x = {1,2,3}. Then the type of the left-hand side is the minimal greatest fixpoint of the types of each expression.

[jwiesler]

Nope, it was the first case (typed array initialization). The code for calculateResolvedType uses a visitor that just throws a UnsupportedOperationException when it is called with a ArrayCreationExpr.

I made possible what was before by unwrapping the element type recursively for all recursive array initializations to provide a type to the ast.