Renovation of the TestCase generation

[wadoon]

Intended Change

Make test case generation usable again, especially from the CLI in the new verification template.

The test case generation was not used for a long time. It was buggy and unstable, and could only be controlled by the UI. This PR tries to revive it a little bit:

Changes

• Add a CLI + Facade for easy access from the CLI or to integrate it into build tools, e.g., Gradle or Maven.
• Get rid of the old project layout, using shell scripts and manually set paths to JAR files.
  The new layout uses the Maven folder layout, and provides a build.gradle.kts and a pom.xml for building and testing
• Add the test case from the book.
• Robust generation of Java program code using javapoet. Nobody understands pages of StringBuilder foo.
• Using picocli for the Command Line interface, also for the existing interfaces in key.ui, keyext.proofmanagement, ...
• Clean up of old Java (introduction of records, sealed hierarchies, NPE checking, ...)

This is rather an MVP, more options and features can be thought of but first get it running.

Type of pull request

• X Refactoring (behaviour should not change or only minimally change)
• X New feature (non-breaking change which adds functionality)
• X Breaking change (fix or feature that would cause existing functionality to change)
• X There are changes to the (Java) code
• X Renovations

[sonarqubecloud]

Quality Gate passed

Issues
102 New issues
0 Accepted issues

Measures
0 Security Hotspots
0.0% Coverage on New Code
0.0% Duplication on New Code

See analysis details on SonarCloud

[wadoon]

@unp1 @mattulbrich Whoever has more experience with the hell of testgen.

[unp1]

addition

One first observatuion "./gradlew :key.ui:run" terminates without starting KeY

same for using the shadowJar very brief window shown and it terminates then with

SLF4J(W): Class path contains multiple SLF4J providers.
SLF4J(W): Found provider [ch.qos.logback.classic.spi.LogbackServiceProvider@5d5eef3d]
SLF4J(W): Found provider [org.slf4j.simple.SimpleServiceProvider@56f4468b]
SLF4J(W): See https://www.slf4j.org/codes.html#multiple_bindings for an explanation.
SLF4J(I): Actual provider is of type [ch.qos.logback.classic.spi.LogbackServiceProvider@5d5eef3d]

[unp1]

I approve the PR once the problem with starting the version is resolved and I tested it on some small examples. Thanks a lot for the work.

[wadoon]

SLF4J(W): Class path contains multiple SLF4J providers. SLF4J(W): Found provider [ch.qos.logback.classic.spi.LogbackServiceProvider@5d5eef3d] SLF4J(W): Found provider [org.slf4j.simple.SimpleServiceProvider@56f4468b] SLF4J(W): See https://www.slf4j.org/codes.html#multiple_bindings for an explanation. SLF4J(I): Actual provider is of type [ch.qos.logback.classic.spi.LogbackServiceProvider@5d5eef3d]

I have not updated to the recent main. There, it should be fixed by #3639 which was introduced by Isabelle deps.

I check it after rebase.

UPDATE: Not appeared after rebase.

[wadoon]

I approve the PR once the problem with starting the version is resolved and I tested it on some small examples. Thanks a lot for the work.

Starting is resolved: Calling System.exit at the end of main does not work b/c the Swing instantiation is non-blocking.

For fostering the command line, the exit code is a good indicator of failure. We should reconsider the Main logic to respect this at some point.

[unp1]

Thanks. I will complete the review later today

[unp1]

Thanks I can open the UI now!
The following observations:

• claims to have written test but cannot be found

* selecting a folder where to store not possible via the magnifying class as folder cannot be selected and saved (only opened) * The result was different when not starting any proof and instead clicking the checkbox "Apply symbolic execution rules"

not implying that this PR should solve all these issues (in particular 3 might have been not working since longer and we can start the prover separately)

[unp1]

Worked on CMdLine and I could now also find the directory. It was in my home directory (so it seems the GUI info is ignored?)

Maybe we should place it in the directory where it is called by default?

Anyways, I think the issues were present before and now at least the generation can be demoed an dI'll approve the change.

But please check if the mentioned issues should be dhave been resolved or if they fall under known issues.

Thanks!

[unp1]

Thanks. Makes it demoable but see my previous comment about known issues

[wadoon]

• claims to have written test but cannot be found

The test case from the book is here:
https://github.com/KeYProject/key/pull/3388/files#diff-3e5bc1e4d3a7fbee0d470dcd7d0b03e6f272fdd0c5ab1c8c8641023c7fd578e6R27

I tried to get binary search working, but was not so successful.

[wadoon]

Thanks I can open the UI now! The following observations:

I avoided to go into the GUI at all. My user story would rather be the generation from inside of the project management / command line.

Clear is Objenesis and JML are resolved using Maven Central via pom.xml/build.xml/build.gradle.

I am also not sure, how the user story should be for the UI. Because, after the generation you need to leave KeY and go to the terminal.

[wadoon]

Rebased for better history. GUI issues are tracked in #3665