Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

More general equalsModProperty #3459

Merged
merged 44 commits into from
Jun 27, 2024

Conversation

tobias-rnh
Copy link
Contributor

@tobias-rnh tobias-rnh commented Apr 19, 2024

Intended Change

Building on top of #3386, the interface EqualsModProperty has now been changed so that it can be used not just with Terms but theoretically any class if a proper Property is implemented. The signature of the method has also been slightly modified so that it is able to handle equality checks that utilize additional parameters (like was the case with equalsModRenaming defined on SourceElements that is also refactored with this PR).
To refactor equalsModRenaming of SourceElement, a new Interface TreeWalker and implementing class JavaASTTreeWalker have been introduced that make it possible to move through the tree of SourceElements step by step.
The new general navigation structure is used to move through the tree of SourceElements.

Plan

Direct tests for JavaASTTreeWalker (currently only indirectly tested through tests for equalsModProperty)
Even more doc comments

Type of pull request

  • Refactoring (behaviour should not change or only minimally change)
  • 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

Additional information and contact(s)

EqualsModProperty

The old TermEqualsModProperty

public interface TermEqualsModProperty {
    boolean equalsModProperty(Object o, TermProperty property);
    int hashCodeModProperty(TermProperty property);
}

has now been parameterized with a type T so that it can accommodate other classes than just Term:

public interface EqualsModProperty<T> {
    <V> boolean equalsModProperty(Object o, Property<T> property, V... v);
    int hashCodeModProperty(Property<T> property);
}

equalsModProperty is furthermore parameterized with a type V that can account for additional parameters needed for the equality check.

Properties

public interface TermProperty {
    Boolean equalsModThisProperty(Term term1, Term term2);
    int hashCodeModThisProperty(Term term);
}

is now parameterized with a type T so that it can accommodate other classes than just Term:

public interface Property<T> {
    <V> boolean equalsModThisProperty(T t1, T t2, V... v);
    int hashCodeModThisProperty(T t);
}

equalsModThisProperty is furthermore parameterized with a type V that can account for additional parameters needed for the equality check.

Refactoring of equalsModRenaming

As equals and equalsModRenaming for SourceElements were basically doing the same thing except for a few classes (equals mostly called equalsModRenaming), the idea was that the content of equalsModRenaming is moved to equals entirely. The special cases that did not call equalsModRenaming in equals or made use of the NameAbstractionTable are now handled by a JavaASTTreeWalker.

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

…erty

# Conflicts:
#	key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryBlockComputationMacro.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryLoopComputationMacro.java
#	key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryMethodComputationMacro.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/BoundVariableTools.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/LabeledTermImpl.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/Semisequent.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/Term.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingTermProperty.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabelManager.java
#	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/FocusCommand.java
#	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/InstantiateCommand.java
#	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/RewriteCommand.java
#	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/RuleCommand.java
#	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SelectCommand.java
#	key.core/src/main/java/de/uka/ilkd/key/proof/join/JoinIsApplicable.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/OneStepSimplifier.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ApplyUpdateOnRigidCondition.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/match/legacy/ElementMatcher.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/VMTacletMatcher.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchSchemaVariableInstruction.java
#	key.core/src/main/java/de/uka/ilkd/key/rule/merge/MergeRule.java
#	key.core/src/main/java/de/uka/ilkd/key/smt/AbstractSMTTranslator.java
#	key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SeqDefHandler.java
#	key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SumProdHandler.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalOperationContractImpl.java
#	key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/feature/ContainsTermFeature.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/feature/DependencyContractFeature.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/feature/FocusIsSubFormulaOfInfFlowContractAppFeature.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/PredictCostProver.java
#	key.core/src/main/java/de/uka/ilkd/key/strategy/termfeature/EqTermFeature.java
#	key.core/src/main/java/de/uka/ilkd/key/util/mergerule/MergeRuleUtils.java
#	key.core/src/test/java/de/uka/ilkd/key/logic/TestTerm.java
#	key.core/src/test/java/de/uka/ilkd/key/logic/equality/TestEqualsModProperty.java
#	key.core/src/test/java/de/uka/ilkd/key/parser/TestTermParser.java
#	key.core/src/test/java/de/uka/ilkd/key/rule/TestApplyTaclet.java
#	key.core/src/test/java/de/uka/ilkd/key/rule/conditions/TestApplyUpdateOnRigidCondition.java
#	key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/ProveSMTLemmasTest.java
#	key.core/src/test/java/de/uka/ilkd/key/speclang/jml/TestJMLTranslator.java
@wadoon wadoon added this to the v2.14.0 milestone Apr 20, 2024
@tobias-rnh
Copy link
Contributor Author

This time the unit tests for windows fail but they run on my machine.
The CodeQuality checks checkstyle_new and pmd seem to also not be working now, however the error messages seem to not be related to my changes.

@tobias-rnh tobias-rnh marked this pull request as ready for review April 21, 2024 15:37
@wadoon wadoon added the 🛠 Maintenance Code quality and related things w/o functional changes label Apr 21, 2024
@wadoon wadoon requested a review from Drodt April 21, 2024 19:24
@Drodt
Copy link
Member

Drodt commented Jun 7, 2024

3 things to do before merge:

  1. Fix merge conflicts.
  2. Some Classes (e.g., StatementBlock) now have equals methods but no corresponding hash methods. Those would need to be added.
  3. Add default methods to EqualsModProperty interface like equalsModRemaning that call equalsModProperty with the corresponding property.

Copy link

codecov bot commented Jun 12, 2024

Codecov Report

Attention: Patch coverage is 41.42012% with 99 lines in your changes missing coverage. Please review.

Project coverage is 38.09%. Comparing base (a4de274) to head (dd8d2ef).
Report is 5 commits behind head on main.

Files Patch % Lines
.../logic/equality/RenamingSourceElementProperty.java 52.54% 14 Missing and 14 partials ⚠️
...ava/de/uka/ilkd/key/smt/AbstractSMTTranslator.java 0.00% 7 Missing ⚠️
.../ilkd/key/java/statement/TransactionStatement.java 0.00% 2 Missing and 3 partials ⚠️
...de/uka/ilkd/key/util/mergerule/MergeRuleUtils.java 0.00% 4 Missing ⚠️
.../main/java/de/uka/ilkd/key/java/SourceElement.java 25.00% 2 Missing and 1 partial ⚠️
...kd/key/java/expression/literal/BooleanLiteral.java 40.00% 1 Missing and 2 partials ⚠️
...lkd/key/java/expression/literal/DoubleLiteral.java 0.00% 3 Missing ⚠️
...ilkd/key/java/expression/literal/FloatLiteral.java 0.00% 3 Missing ⚠️
.../ilkd/key/java/expression/literal/RealLiteral.java 0.00% 3 Missing ⚠️
...lkd/key/java/expression/literal/StringLiteral.java 0.00% 1 Missing and 2 partials ⚠️
... and 27 more
Additional details and impacted files
@@             Coverage Diff              @@
##               main    #3459      +/-   ##
============================================
+ Coverage     38.04%   38.09%   +0.05%     
- Complexity    17117    17175      +58     
============================================
  Files          2105     2107       +2     
  Lines        127439   127517      +78     
  Branches      21401    21436      +35     
============================================
+ Hits          48487    48581      +94     
+ Misses        72978    72950      -28     
- Partials       5974     5986      +12     

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

@tobias-rnh
Copy link
Contributor Author

3 things to do before merge:

1. Fix merge conflicts.

Done.

2. Some Classes (e.g., `StatementBlock`) now have `equals` methods but no corresponding `hash` methods. Those would need to be added.

Most of the time, this was a false alert. The hashCode() method is not directly overridden, but the method computeHashCode() that does the actual computation in hashCode() is overridden. For some classes, however, I have added implementations of computeHashCode().

3. Add default methods to `EqualsModProperty` interface like `equalsModRemaning` that call `equalsModProperty` with the corresponding property.

As discussed, we do not add default methods. Most of the properties like TermLabelsProperty are only defined for terms, and there are no comparable properties defined for other instances of the generic type T.

Drodt and others added 3 commits June 25, 2024 12:01
# Conflicts:
#	key.core/src/main/java/de/uka/ilkd/key/java/SourceElement.java
#	key.core/src/main/java/de/uka/ilkd/key/logic/Term.java
@tobias-rnh
Copy link
Contributor Author

I have changed equalsModThisProperty in RenamingSourceElementProperty to use the general navigation structure instead of the TreeWalker. Because of this, I have removed the TreeWalker entirely.
This PR could now be merged after all the tests have passed.

@Drodt Drodt added this pull request to the merge queue Jun 27, 2024
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Jun 27, 2024
@Drodt Drodt added this pull request to the merge queue Jun 27, 2024
Merged via the queue into KeYProject:main with commit a3fbc37 Jun 27, 2024
14 of 15 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
🛠 Maintenance Code quality and related things w/o functional changes
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants