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]

I can break down the problem to HeapLDT::getFieldSymbolName in which the field name is only length but something with "ABC::length" is expected:

solved.

[Drodt]

2 errors Wolfram and I noticed:

1. Array creation is wrong, which is a problem for, e.g., the TranslationTest unit test. In CreateArrayMethodBuilder::createArray(ImmutableList<Field>), we try to add a statement like this.<initialized> = false;. But implicit fields like implicit have not been added to the array type yet.
2. The bootClasses of JavaParserFactory are not set in the KeYJavaPipelineTest.

[wadoon]

• Array creation is wrong, which is a problem for, e.g., the TranslationTest unit test. In CreateArrayMethodBuilder::createArray(ImmutableList<Field>), we try to add a statement like this.<initialized> = false;. But implicit fields like implicit have not been added to the array type yet.

Background: During translation, types are already converted from resolved types to KeYJavaType, before the AST of these types are translated. This results in the effect, that java.lang.Object can be found, but not the JavaType part of it on this position in time.

So it is a deeper problem, that the Java translation builds upon name resolution.

[wadoon]

I now think the redux-test is mainly untestable as it is a cycle dependency.

To test whether java.lang.Object is translatable in the pipeline, you need to translate java.lang.Object first. Because the translation requires symbol resolution of java.lang.Object in the KeY-special redux form.