Map with new equalities

[tobias-rnh]

Related Issue

This pull request depends on PR #3459, which should be merged before reviewing this PR.

Intended Change

This PR adds the new collection LinkedHashMapWrapper that can be used like the LinkedHashMap in key.core/de.uka.ilkd.key.util. The difference is, that elements are wrapped internally so that equalsModProperty() and hashCodeModProperty() are used instead of the normal equals() and hashCode() methods.

For this to work, hashCodeModProperty() is implemented for all properties introduced in #3459.

Plan

Use general navigation structure instead of TreeWalker for hashCodeModThisProperty

Type of pull request

• New feature (non-breaking change which adds functionality)
• There are changes to the (Java) code

Ensuring quality

• I made sure that introduced/changed code is well documented (javadoc and inline comments).
• I added new test case(s) for new functionality.
• I have tested the feature as follows: Already existing and new tests

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

[Drodt]

There are some minor merge errors. Besides that it looks fine

[codecov]

Codecov Report

Attention: Patch coverage is 86.13139% with 19 lines in your changes missing coverage. Please review.

Project coverage is 38.16%. Comparing base (ea0879b) to head (0ebb8b5).
Report is 1 commits behind head on main.

Files	Patch %	Lines
...ava/de/uka/ilkd/key/util/LinkedHashMapWrapper.java	81.48%	7 Missing and 3 partials ⚠️
...java/de/uka/ilkd/key/logic/util/EqualityUtils.java	55.55%	2 Missing and 2 partials ⚠️
.../ilkd/key/logic/equality/RenamingTermProperty.java	88.88%	1 Missing and 2 partials ⚠️
.../logic/equality/RenamingSourceElementProperty.java	92.30%	0 Missing and 2 partials ⚠️

Additional details and impacted files

@@             Coverage Diff              @@
##               main    #3486      +/-   ##
============================================
+ Coverage     38.10%   38.16%   +0.05%     
- Complexity    17181    17222      +41     
============================================
  Files          2107     2109       +2     
  Lines        127519   127643     +124     
  Branches      21437    21458      +21     
============================================
+ Hits          48596    48710     +114     
- Misses        72940    72943       +3     
- Partials       5983     5990       +7     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[unp1]

Nice work. Thanks!

[mi-ki]

Having a quick glance and check after this PR, the changes seem to make the taclet varcond TermLabelCondition non-functional. For example, in well-definedness checks, the according taclets (e.g., wd_Logical_Op_And and wd_Logical_Op_AndSC) are not applicable anymore. Could you maybe have a further look at this?

[tobias-rnh]

Having a quick glance and check after this PR, the changes seem to make the taclet varcond TermLabelCondition non-functional. For example, in well-definedness checks, the according taclets (e.g., wd_Logical_Op_And and wd_Logical_Op_AndSC) are not applicable anymore. Could you maybe have a further look at this?

That is curious as this PR should have only added hash-methods that were not used before and a HashMap wrapper that is also not yet used in any previously existing code.
I am currently away for also the next week, but I will take a look at this once I am back again.

[mi-ki]

Cool, thanks in advance!

[tobias-rnh]

As a starting point for me, is there any specific example or problem you looked at where these taclets were not applicable anymore, but they were previously?

[wadoon]

As a use case, we had for a long time the verification of the hagrid key-server. For this, we only used Integer and the symbolical equality (=) in JavaDL b/c the map theory was restricted to that.

Would it now be possible to extend this example to equalities on String or even .equals() with the new theory?

[mi-ki]

As a starting point for me, is there any specific example or problem you looked at where these taclets were not applicable anymore, but they were previously?

I just re-checked the example from two weeks ago, and apparently cannot reproduce the problem, as it seems to work fine. Hence, sorry for the false alarm, and thanks for the effort!

[tobias-rnh]

As a starting point for me, is there any specific example or problem you looked at where these taclets were not applicable anymore, but they were previously?

I just re-checked the example from two weeks ago, and apparently cannot reproduce the problem, as it seems to work fine. Hence, sorry for the false alarm, and thanks for the effort!

Well that is nice, no problem.

[tobias-rnh]

As a use case, we had for a long time the verification of the hagrid key-server. For this, we only used Integer and the symbolical equality (=) in JavaDL b/c the map theory was restricted to that.

Would it now be possible to extend this example to equalities on String or even .equals() with the new theory?

If I understand your question correctly, then the answer is no. My changes were just meant to finish hashCodeModProperty and wrap the LinkedHashMap to be used as a more efficient cache with equalsModProperty in the future.
So I have not changed things about the map theory.