Renovation of PO loading

wadoon commented 8 months ago

Intended Change

This is an overhaul of the \proofObligation inside of KeY files and some internal api changes.

\proofObligation is migrated from a property string to the new configuration grammar. An entry looks as follows:
```
\proofObligation { 
"class" : "de.uka.ilkd.key.proof.init.FunctionalOperationContractPO",
"contract" : "SITA3[SITA3::rearrange()].JML normal_behavior operation contract.0",
"name" : "SITA3[SITA3::rearrange()].JML normal_behavior operation contract.0"
}
```
Earlier it was a string holding the information as a Properties. This allows in feature to have type-safe PO parameters. This affects the grammar, parser and also the store functionality of each PO class.
Renovation of #loadFrom. Old KeY uses the class information to load this class and invokes the static method #loadFrom(...). This PR replaces this behaviour using the ServiceLoader. This makes adding a new PO (loader) more convenient and type-safe.

A fallback for old \proofObligation is implemented. Reading an old \proofObligation "..."; entry should be translated into the new architecture.

Type of pull request

X Refactoring (behaviour should not change or only minimally change)
X Breaking change (fix or feature that would cause existing functionality to change)
X There are changes to the (Java) code
X Other: KeY-Problem-Files, Grammar

Ensuring quality

X I made sure that introduced/changed code is well documented (javadoc and inline comments).
X I made sure that new/changed end-user features are documented as well as before.
X I have tested the feature as follows: store a proof file

wadoon commented 7 months ago

@unp1 Should be ready if green. To implement a fallback was easier than to add a useful error message. So it should read old files, too.

codecov[bot] commented 7 months ago

Codecov Report

Attention: Patch coverage is 25.00000% with 189 lines in your changes are missing coverage. Please review.

Project coverage is 37.91%. Comparing base (7254776) to head (cde13ae). Report is 96 commits behind head on main.

:exclamation: Current head cde13ae differs from pull request most recent head 89f6c9a. Consider uploading reports for the commit 89f6c9a to get more accurate results

Files	Patch %	Lines
.../proof/init/loader/DependencyContractPOLoader.java	4.16%	19 Missing and 4 partials :warning:
...f/init/loader/FunctionalBlockContractPOLoader.java	4.16%	19 Missing and 4 partials :warning:
...of/init/loader/FunctionalLoopContractPOLoader.java	4.16%	19 Missing and 4 partials :warning:
...ttranslation/lemma/TacletProofObligationInput.java	0.00%	15 Missing :warning:
...init/loader/FunctionOperationContractPOLoader.java	56.25%	9 Missing and 5 partials :warning:
...e/uka/ilkd/key/proof/io/AbstractProblemLoader.java	61.11%	7 Missing and 7 partials :warning:
...a/ilkd/key/proof/init/WellDefinednessPOLoader.java	0.00%	12 Missing :warning:
...ey/informationflow/po/InfFlowContractPOLoader.java	0.00%	11 Missing :warning:
...de/uka/ilkd/key/nparser/builder/ProblemFinder.java	15.38%	9 Missing and 2 partials :warning:
...lation/lemma/TacletProofObligationInputLoader.java	0.00%	11 Missing :warning:
... and 12 more

Additional details and impacted files

```diff @@ Coverage Diff @@ ## main #3379 +/- ## ============================================ + Coverage 37.86% 37.91% +0.04% - Complexity 17079 17083 +4 ============================================ Files 2092 2083 -9 Lines 127596 127058 -538 Branches 21478 21410 -68 ============================================ - Hits 48316 48175 -141 + Misses 73355 72964 -391 + Partials 5925 5919 -6 ```

:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.

wadoon commented 5 months ago

This idles here in a ready state and looking for a review for at least a month now. @mattulbrich @unp1 @WolframPfeifer

mattulbrich commented 4 months ago

There are failing test cases. Is this ready for review?

wadoon commented 4 months ago

There are failing test cases. Is this ready for review? It was green back then. But after auto-merging it became failing.

But it is reviewable. Especially, the discussion on whether we want to let the old proof files be with the string-based properties format for proof obligations. In the history of the PR, a compatibility layer was added.

If this is decided and reviewed, I start fixing the test cases, but running behind failing unit-tests is easier than PR reviewers.

mattulbrich commented 4 months ago

Especially, the discussion on whether we want to let the old proof files be with the string-based properties format for proof obligations. In the history of the PR, a compatibility layer was added. If this is decided and reviewed, I start fixing the test cases, but running behind failing unit-tests is easier than PR reviewers.

I'd would suggest to migrate the old proof file in the repo to the new format (it looks like this has been done ...)

Having the ability to parse Strings does not hurt either for a while. Going from a properties object to a key-value object should also be relatively local.

KeYProject / key