From 486f6e370a61f72d9db347a10572cfdeb9945ac7 Mon Sep 17 00:00:00 2001 From: Tobias Reinhold Date: Tue, 9 Jan 2024 23:01:12 +0100 Subject: [PATCH 01/28] move utility method from ProofIrrelevancyProperty to new dedicated class EqualityUtils and make it more general --- .../key/logic/equality/EqualityUtils.java | 33 +++++++++++++++++++ .../equality/ProofIrrelevancyProperty.java | 31 ++--------------- 2 files changed, 36 insertions(+), 28 deletions(-) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/logic/equality/EqualityUtils.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/EqualityUtils.java b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/EqualityUtils.java new file mode 100644 index 00000000000..37d80cc1629 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/EqualityUtils.java @@ -0,0 +1,33 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.logic.equality; + +import de.uka.ilkd.key.logic.Term; + +public class EqualityUtils { + + /** + * Computes the hashcode of an iterable of terms modulo a given property using the elements' + * {@link TermEqualsModProperty} implementation. + * + * @param iter iterable of terms + * @return combined hashcode + */ + public static int hashCodeModPropertyOfIterable(TermProperty property, + Iterable iter) { + // adapted from Arrays.hashCode + if (iter == null) { + return 0; + } + + int result = 1; + + for (Term element : iter) { + result = 31 * result + (element == null ? 0 + : element.hashCodeModProperty(property)); + } + + return result; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/ProofIrrelevancyProperty.java b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/ProofIrrelevancyProperty.java index f652c25f1c0..a600ae7aa87 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/ProofIrrelevancyProperty.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/ProofIrrelevancyProperty.java @@ -113,7 +113,9 @@ public int hashCodeModThisProperty(Term term) { // part from TermImpl if (hashcode2 == -1) { // compute into local variable first to be thread-safe. - hashcode2 = Objects.hash(term.op(), hashCodeIterable(term.subs()), + hashcode2 = Objects.hash(term.op(), + EqualityUtils.hashCodeModPropertyOfIterable(PROOF_IRRELEVANCY_PROPERTY, + term.subs()), EqualsModProofIrrelevancyUtil.hashCodeIterable(term.boundVars()), term.javaBlock()); if (hashcode2 == -1) { hashcode2 = 0; @@ -129,32 +131,5 @@ public int hashCodeModThisProperty(Term term) { } } return hashcode2; - // throw new UnsupportedOperationException( - // "Hashing of terms modulo term proof-irrelevancy not yet implemented!"); - } - - // -------------------------- Utility methods --------------------------------- // - - /** - * Compute the hashcode mod proof irrelevancy of an iterable of terms using the elements' - * {@link TermEqualsModProperty} implementation. - * - * @param iter iterable of terms - * @return combined hashcode - */ - public static int hashCodeIterable(Iterable iter) { - // adapted from Arrays.hashCode - if (iter == null) { - return 0; - } - - int result = 1; - - for (Term element : iter) { - result = 31 * result + (element == null ? 0 - : element.hashCodeModProperty(PROOF_IRRELEVANCY_PROPERTY)); - } - - return result; } } From 756d79c820cef5a7410c6bd43e3e47043e0f157a Mon Sep 17 00:00:00 2001 From: Tobias Reinhold Date: Tue, 9 Jan 2024 23:03:25 +0100 Subject: [PATCH 02/28] add implementations to hashCodeModProperty for IrrelevantTermLabelsProperty and TermLabelsProperty --- .../IrrelevantTermLabelsProperty.java | 28 +++++++++++++++++-- .../logic/equality/RenamingTermProperty.java | 6 ++++ .../logic/equality/TermLabelsProperty.java | 22 +++++++++++++-- 3 files changed, 52 insertions(+), 4 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/IrrelevantTermLabelsProperty.java b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/IrrelevantTermLabelsProperty.java index 96d77707260..181cdbe485d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/IrrelevantTermLabelsProperty.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/IrrelevantTermLabelsProperty.java @@ -80,9 +80,33 @@ public Boolean equalsModThisProperty(Term term, Object o) { return true; } + /** + * Computes the hash code of {@code term} while ignoring irrelevant labels. + * + * @param term the term to compute the hash code for + * @return the hash code + */ @Override public int hashCodeModThisProperty(Term term) { - throw new UnsupportedOperationException( - "Hashing of terms modulo irrelevant term labels not yet implemented!"); + // change 5 and 17 not to match TermImpl's implementation too much? + int hashcode = 5; + hashcode = hashcode * 17 + term.op().hashCode(); + hashcode = hashcode * 17 + EqualityUtils + .hashCodeModPropertyOfIterable(IRRELEVANT_TERM_LABELS_PROPERTY, term.subs()); + hashcode = hashcode * 17 + term.boundVars().hashCode(); + hashcode = hashcode * 17 + term.javaBlock().hashCode(); + + for (TermLabel label : term.getLabels()) { + hashcode += (label.isProofRelevant() ? 7 * label.hashCode() : 0); + } + +// final ImmutableArray termLabels = term.getLabels(); +// for (int i = 0, sz = termLabels.size(); i < sz; i++) { +// final TermLabel currentLabel = termLabels.get(i); +// if (currentLabel.isProofRelevant()) { +// hashcode += 7 * currentLabel.hashCode(); +// } +// } + return hashcode; } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingTermProperty.java b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingTermProperty.java index 068e0c1cae5..b1c0441c08c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingTermProperty.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingTermProperty.java @@ -52,6 +52,12 @@ public Boolean equalsModThisProperty(Term term, Object o) { ImmutableSLList.nil(), null); } + /** + * Computes the hash code of {@code term} modulo bound renaming. + * + * @param term the term to compute the hash code for + * @return the hash code + */ @Override public int hashCodeModThisProperty(Term term) { throw new UnsupportedOperationException( diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/TermLabelsProperty.java b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/TermLabelsProperty.java index a6f1ba57c4f..b81958fab38 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/TermLabelsProperty.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/TermLabelsProperty.java @@ -61,9 +61,27 @@ public Boolean equalsModThisProperty(Term term, Object o) { return true; } + /** + * Computes the hash code of {@code term} while ignoring all term labels. + *

+ * Currently, the hash code is computed almost the same way as in TermImpl. This is also the + * case for labeled terms, + * as all term labels are ignored. + * + * @param term the term to compute the hash code for + * @return the hash code + */ @Override public int hashCodeModThisProperty(Term term) { - throw new UnsupportedOperationException( - "Hashing of terms modulo term labels not yet implemented!"); + // change 5 and 17 not to match TermImpl's implementation too much + int hashcode = 5; + hashcode = hashcode * 17 + term.op().hashCode(); + hashcode = hashcode * 17 + + EqualityUtils.hashCodeModPropertyOfIterable(TERM_LABELS_PROPERTY, term.subs()); + hashcode = hashcode * 17 + term.boundVars().hashCode(); + hashcode = hashcode * 17 + term.javaBlock().hashCode(); + + return hashcode; } + } From 8178953b398f1e6eb356783388944560c497dddf Mon Sep 17 00:00:00 2001 From: Tobias Reinhold Date: Tue, 23 Jan 2024 23:38:30 +0100 Subject: [PATCH 03/28] add wrapper of LinkedHashMap that uses equalsModProperty in equals method --- .../IrrelevantTermLabelsProperty.java | 8 - .../logic/equality/LinkedHashMapWrapper.java | 152 ++++++++++++++++++ .../logic/equality/TermLabelsProperty.java | 1 - 3 files changed, 152 insertions(+), 9 deletions(-) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/logic/equality/LinkedHashMapWrapper.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/IrrelevantTermLabelsProperty.java b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/IrrelevantTermLabelsProperty.java index 23c9e46021a..ff455e04078 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/IrrelevantTermLabelsProperty.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/IrrelevantTermLabelsProperty.java @@ -86,7 +86,6 @@ public Boolean equalsModThisProperty(Term term1, Term term2) { */ @Override public int hashCodeModThisProperty(Term term) { - // change 5 and 17 not to match TermImpl's implementation too much? int hashcode = 5; hashcode = hashcode * 17 + term.op().hashCode(); hashcode = hashcode * 17 + EqualityUtils @@ -98,13 +97,6 @@ public int hashCodeModThisProperty(Term term) { hashcode += (label.isProofRelevant() ? 7 * label.hashCode() : 0); } -// final ImmutableArray termLabels = term.getLabels(); -// for (int i = 0, sz = termLabels.size(); i < sz; i++) { -// final TermLabel currentLabel = termLabels.get(i); -// if (currentLabel.isProofRelevant()) { -// hashcode += 7 * currentLabel.hashCode(); -// } -// } return hashcode; } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/LinkedHashMapWrapper.java b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/LinkedHashMapWrapper.java new file mode 100644 index 00000000000..2032a6ef5a1 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/LinkedHashMapWrapper.java @@ -0,0 +1,152 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.logic.equality; + +import java.util.Iterator; + +import de.uka.ilkd.key.logic.Term; +import de.uka.ilkd.key.util.LinkedHashMap; +import de.uka.ilkd.key.util.Pair; + + +public class LinkedHashMapWrapper { + private final LinkedHashMap map; + private final TermProperty property; + + public LinkedHashMapWrapper(TermProperty property) { + this.property = property; + map = new LinkedHashMap<>(); + } + + public LinkedHashMapWrapper(Term key, V value, TermProperty property) { + this(property); + put(key, value); + } + + public LinkedHashMapWrapper(Term[] keys, V[] values, TermProperty property) { + this(property); + putAll(keys, values); + } + + + public LinkedHashMapWrapper(Iterable keys, Iterable values, TermProperty property) { + this(property); + putAll(keys, values); + } + + public int size() { + return map.size(); + } + + public boolean isEmpty() { + return map.isEmpty(); + } + + public boolean containsKey(Term key) { + return map.containsKey(wrapTerm(key)); + } + + public V get(Term key) { + return map.get(wrapTerm(key)); + } + + public V put(Term key, V value) { + return map.put(wrapTerm(key), value); + } + + public void putAll(Term[] keys, V[] vals) { + for (int i = 0; i < keys.length; i++) { + if (i < vals.length) { + put(keys[i], vals[i]); + } else { + put(keys[i], null); + } + } + } + + public void putAll(Iterable keys, Iterable vals) { + Iterator itVals = vals.iterator(); + for (Term key : keys) { + if (itVals.hasNext()) { + put(key, itVals.next()); + } else { + put(key, null); + } + } + } + + public V remove(Term key) { + return map.remove(wrapTerm(key)); + } + + public boolean containsValue(V value) { + return map.containsValue(value); + } + + public Iterator> iterator() { + return new PairIterator<>(map); + } + + private TermWrapper wrapTerm(Term term) { + return new TermWrapper(term, property); + } + + + // ------------- wrapper class for terms + /** + * This class is used to wrap a term and override the {@code equals} and {@code hashCode} methods for use in a + * {@link LinkedHashMap}. + *

+ * The wrapped term is equipped with a {@link TermProperty} that is used for + * {@link TermEqualsModProperty#equalsModProperty(Object, TermProperty)} and + * {@link TermEqualsModProperty#hashCodeModProperty(TermProperty)}. + * + * @param term The term to be wrapped + * @param property The {@link TermProperty} that is used in the {@code equals} and {@code hashCode} methods + */ + private record TermWrapper(Term term, TermProperty property) { + @Override + public boolean equals(Object obj) { + return term.equalsModProperty(obj, property); + } + + @Override + public int hashCode() { + return term.hashCodeModProperty(property); + } + } + + // ------------- class to iterate over internal map and unwrap terms + private static class PairIterator implements Iterator> { + + private final Iterator keyIt; + private final LinkedHashMap map; + private TermWrapper last = null; + + public PairIterator(final LinkedHashMap map) { + this.map = map; + keyIt = map.keySet().iterator(); + } + + @Override + public boolean hasNext() { + return keyIt.hasNext(); + } + + @Override + public Pair next() { + last = keyIt.next(); + return new Pair<>(last.term(), map.get(last)); + } + + @Override + public void remove() { + if (last != null) { + map.remove(last); + last = null; + } + } + + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/TermLabelsProperty.java b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/TermLabelsProperty.java index 1f3e6fda99d..a32070a1196 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/TermLabelsProperty.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/TermLabelsProperty.java @@ -71,7 +71,6 @@ public Boolean equalsModThisProperty(Term term1, Term term2) { */ @Override public int hashCodeModThisProperty(Term term) { - // change 5 and 17 not to match TermImpl's implementation too much int hashcode = 5; hashcode = hashcode * 17 + term.op().hashCode(); hashcode = hashcode * 17 From 0f7c1b5a8ad271ad2d53bec01b955ce0bea68a77 Mon Sep 17 00:00:00 2001 From: Tobias Reinhold Date: Wed, 24 Jan 2024 16:35:18 +0100 Subject: [PATCH 04/28] move EqualityUtils and LinkedHashMapWrapper from equality to util --- .../ilkd/key/logic/equality/IrrelevantTermLabelsProperty.java | 1 + .../uka/ilkd/key/logic/equality/ProofIrrelevancyProperty.java | 1 + .../de/uka/ilkd/key/logic/equality/TermLabelsProperty.java | 1 + .../uka/ilkd/key/logic/{equality => util}/EqualityUtils.java | 4 +++- .../key/logic/{equality => util}/LinkedHashMapWrapper.java | 4 +++- 5 files changed, 9 insertions(+), 2 deletions(-) rename key.core/src/main/java/de/uka/ilkd/key/logic/{equality => util}/EqualityUtils.java (86%) rename key.core/src/main/java/de/uka/ilkd/key/logic/{equality => util}/LinkedHashMapWrapper.java (96%) diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/IrrelevantTermLabelsProperty.java b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/IrrelevantTermLabelsProperty.java index ff455e04078..eb15257aa24 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/IrrelevantTermLabelsProperty.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/IrrelevantTermLabelsProperty.java @@ -5,6 +5,7 @@ import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.label.TermLabel; +import de.uka.ilkd.key.logic.util.EqualityUtils; import org.key_project.util.collection.ImmutableArray; diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/ProofIrrelevancyProperty.java b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/ProofIrrelevancyProperty.java index 436137ac4cd..e0ba0a08699 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/ProofIrrelevancyProperty.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/ProofIrrelevancyProperty.java @@ -8,6 +8,7 @@ import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.label.TermLabel; +import de.uka.ilkd.key.logic.util.EqualityUtils; import org.key_project.util.EqualsModProofIrrelevancy; import org.key_project.util.EqualsModProofIrrelevancyUtil; diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/TermLabelsProperty.java b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/TermLabelsProperty.java index a32070a1196..f00f77b8302 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/TermLabelsProperty.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/TermLabelsProperty.java @@ -4,6 +4,7 @@ package de.uka.ilkd.key.logic.equality; import de.uka.ilkd.key.logic.Term; +import de.uka.ilkd.key.logic.util.EqualityUtils; import org.key_project.util.collection.ImmutableArray; diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/EqualityUtils.java b/key.core/src/main/java/de/uka/ilkd/key/logic/util/EqualityUtils.java similarity index 86% rename from key.core/src/main/java/de/uka/ilkd/key/logic/equality/EqualityUtils.java rename to key.core/src/main/java/de/uka/ilkd/key/logic/util/EqualityUtils.java index 37d80cc1629..e149df04ef4 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/EqualityUtils.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/util/EqualityUtils.java @@ -1,9 +1,11 @@ /* This file is part of KeY - https://key-project.org * KeY is licensed under the GNU General Public License Version 2 * SPDX-License-Identifier: GPL-2.0-only */ -package de.uka.ilkd.key.logic.equality; +package de.uka.ilkd.key.logic.util; import de.uka.ilkd.key.logic.Term; +import de.uka.ilkd.key.logic.equality.TermEqualsModProperty; +import de.uka.ilkd.key.logic.equality.TermProperty; public class EqualityUtils { diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/LinkedHashMapWrapper.java b/key.core/src/main/java/de/uka/ilkd/key/logic/util/LinkedHashMapWrapper.java similarity index 96% rename from key.core/src/main/java/de/uka/ilkd/key/logic/equality/LinkedHashMapWrapper.java rename to key.core/src/main/java/de/uka/ilkd/key/logic/util/LinkedHashMapWrapper.java index 2032a6ef5a1..e2a0bced01b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/LinkedHashMapWrapper.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/util/LinkedHashMapWrapper.java @@ -1,11 +1,13 @@ /* This file is part of KeY - https://key-project.org * KeY is licensed under the GNU General Public License Version 2 * SPDX-License-Identifier: GPL-2.0-only */ -package de.uka.ilkd.key.logic.equality; +package de.uka.ilkd.key.logic.util; import java.util.Iterator; import de.uka.ilkd.key.logic.Term; +import de.uka.ilkd.key.logic.equality.TermEqualsModProperty; +import de.uka.ilkd.key.logic.equality.TermProperty; import de.uka.ilkd.key.util.LinkedHashMap; import de.uka.ilkd.key.util.Pair; From 868dc426ca6f0ececfe779f25b4814153c9b0c44 Mon Sep 17 00:00:00 2001 From: Tobias Reinhold Date: Wed, 24 Jan 2024 18:05:37 +0100 Subject: [PATCH 05/28] add doc to LinkedHashMapWrapper --- .../key/logic/util/LinkedHashMapWrapper.java | 168 +++++++++++++++++- 1 file changed, 165 insertions(+), 3 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/util/LinkedHashMapWrapper.java b/key.core/src/main/java/de/uka/ilkd/key/logic/util/LinkedHashMapWrapper.java index e2a0bced01b..060b6bb4b45 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/util/LinkedHashMapWrapper.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/util/LinkedHashMapWrapper.java @@ -11,52 +11,148 @@ import de.uka.ilkd.key.util.LinkedHashMap; import de.uka.ilkd.key.util.Pair; - +/** + * This class is a wrapper for {@link LinkedHashMap} where the keys are {@link Term}s. + *

+ * Internally, the {@link Term}s are wrapped so that {@link TermEqualsModProperty} can be used for + * equality checks and + * hash codes instead of the usual {@code equals} and {@code hashCode} methods of {@link Term}. + * + * @param the type of the values in the wrapped LinkedHashMap + */ public class LinkedHashMapWrapper { + /** + * The wrapped {@link LinkedHashMap}. + */ private final LinkedHashMap map; + + /** + * The {@link TermProperty} that is used for equality checks and hash codes. + */ private final TermProperty property; + /** + * Constructs a new empty {@link LinkedHashMapWrapper}. + * + * @param property the {@link TermProperty} that is used internally for equality checks and hash + * codes + */ public LinkedHashMapWrapper(TermProperty property) { this.property = property; map = new LinkedHashMap<>(); } + /** + * Constructs a new {@link LinkedHashMapWrapper} and inserts the given key-value pair. + * + * @param key the key to be inserted + * @param value the value corresponding to {@code key} + * @param property the {@link TermProperty} that is used internally for equality checks and hash + * codes + */ public LinkedHashMapWrapper(Term key, V value, TermProperty property) { this(property); put(key, value); } + /** + * Constructs a new {@link LinkedHashMapWrapper} and inserts the given key-value pairs. + *

+ * The first key in {@code keys} is mapped to the first value in {@code values} etc. + * If there are more keys than values, the remaining keys are mapped to {@code null}. + * If there are more values than keys, the remaining values are ignored. + * + * @param keys the array of keys to be inserted + * @param values the array of values corresponding to the keys + * @param property the {@link TermProperty} that is used internally for equality checks and hash + * codes + */ public LinkedHashMapWrapper(Term[] keys, V[] values, TermProperty property) { this(property); putAll(keys, values); } - + /** + * Constructs a new {@link LinkedHashMapWrapper} and inserts the given key-value pairs. + *

+ * The first key in {@code keys} is mapped to the first value in {@code values} etc. + * If there are more keys than values, the remaining keys are mapped to {@code null}. + * If there are more values than keys, the remaining values are ignored. + * + * @param keys the iterable of keys to be inserted + * @param values the iterable of values corresponding to the keys + * @param property the {@link TermProperty} that is used internally for equality checks and hash + * codes + */ public LinkedHashMapWrapper(Iterable keys, Iterable values, TermProperty property) { this(property); putAll(keys, values); } + /** + * Returns the number of key-value pairs in this map. + * + * @return the number of key-value pairs in this map + */ public int size() { return map.size(); } + /** + * Returns true if this map contains no key-value pairs. + * + * @return true if this map contains no key-value pairs + */ public boolean isEmpty() { return map.isEmpty(); } + /** + * Returns true if this map contains a mapping for the specified key. + * + * @param key the key whose presence in this map is to be tested + * @return true if this map contains a mapping for the specified key + */ public boolean containsKey(Term key) { return map.containsKey(wrapTerm(key)); } + /** + * Returns the value to which the specified key is mapped, or {@code null} if this map contains + * no mapping for the key. + * + * @param key the key whose associated value is to be returned + * @return the value to which the specified key is mapped + */ public V get(Term key) { return map.get(wrapTerm(key)); } + /** + * Insert the given key-value pair into this map. + *

+ * If the map previously contained a mapping for the key, the old value is replaced by the given + * value. + * + * @param key the key to be inserted + * @param value the value corresponding to {@code key} + * @return the previous value associated with {@code key}, or {@code null} if there was no + * mapping for {@code key} + */ public V put(Term key, V value) { return map.put(wrapTerm(key), value); } + /** + * Inserts the given key-value pairs into this map. + *

+ * The first key in {@code keys} is mapped to the first value in {@code values} etc. + * If there are more keys than values, the remaining keys are mapped to {@code null}. + * If there are more values than keys, the remaining values are ignored. + * + * @param keys the array of keys to be inserted + * @param vals the array of values corresponding to the keys + */ public void putAll(Term[] keys, V[] vals) { for (int i = 0; i < keys.length; i++) { if (i < vals.length) { @@ -67,6 +163,16 @@ public void putAll(Term[] keys, V[] vals) { } } + /** + * Inserts the given key-value pairs into this map. + *

+ * The first key in {@code keys} is mapped to the first value in {@code values} etc. + * If there are more keys than values, the remaining keys are mapped to {@code null}. + * If there are more values than keys, the remaining values are ignored. + * + * @param keys the iterable of keys to be inserted + * @param vals the iterable of values corresponding to the keys + */ public void putAll(Iterable keys, Iterable vals) { Iterator itVals = vals.iterator(); for (Term key : keys) { @@ -78,18 +184,51 @@ public void putAll(Iterable keys, Iterable vals) { } } + /** + * Removes the mapping for the specified key from this map if present and returns the previously + * associated value. + * + * @param key the key whose mapping is to be removed from the map + * @return the previous value associated with {@code key}, or {@code null} if there was no + * mapping for {@code key} + */ public V remove(Term key) { return map.remove(wrapTerm(key)); } + /** + * Returns true if this map contains a mapping to the specified value. + * + * @param value the value whose presence in this map is to be tested + * @return true if this map contains a mapping to the specified value + */ public boolean containsValue(V value) { return map.containsValue(value); } + /** + * Returns an iterator over the key-value pairs in this map. + *

+ * The pairs in this iterator contain the unwrapped terms. + * + * @return an iterator over the key-value pairs in this map + */ public Iterator> iterator() { return new PairIterator<>(map); } + /** + * This helper method wraps a term in a {@link TermWrapper} with the {@link TermProperty} of + * this map. + *

+ * This is done so that {@link TermEqualsModProperty} can be used for equality checks and hash + * codes instead of the + * usual {@code equals} and {@code hashCode} methods of {@link Term} in the internal + * {@link LinkedHashMap}. + * + * @param term the term to be wrapped + * @return the wrapped term + */ private TermWrapper wrapTerm(Term term) { return new TermWrapper(term, property); } @@ -120,12 +259,35 @@ public int hashCode() { } // ------------- class to iterate over internal map and unwrap terms - private static class PairIterator implements Iterator> { + /** + * This class is used to iterate over the key-value pairs in the {@link LinkedHashMapWrapper}. + *

+ * The terms in the pairs are unwrapped before returning them. + * + * @param the type of the values in the {@link LinkedHashMapWrapper} + */ + private static class PairIterator implements Iterator> { + /** + * The iterator over the keys of the internal map. + */ private final Iterator keyIt; + + /** + * The internal map. + */ private final LinkedHashMap map; + + /** + * The last key-value pair that was returned by {@link #next()}. + */ private TermWrapper last = null; + /** + * Creates a new iterator over the key-value pairs in the {@link LinkedHashMapWrapper}. + * + * @param map the internal map of the {@link LinkedHashMapWrapper} to iterate over + */ public PairIterator(final LinkedHashMap map) { this.map = map; keyIt = map.keySet().iterator(); From a499abd6d831f21aca128ddd6504488faac80240 Mon Sep 17 00:00:00 2001 From: Tobias Reinhold Date: Thu, 25 Apr 2024 18:17:15 +0200 Subject: [PATCH 06/28] fix errors introduced through merge --- .../equality/ProofIrrelevancyProperty.java | 4 +- .../ilkd/key/logic/util/EqualityUtils.java | 16 ++-- .../key/logic/util/LinkedHashMapWrapper.java | 75 ++++++++++--------- 3 files changed, 52 insertions(+), 43 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/ProofIrrelevancyProperty.java b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/ProofIrrelevancyProperty.java index 9e48a23bb98..1172bfd5d87 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/ProofIrrelevancyProperty.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/ProofIrrelevancyProperty.java @@ -14,6 +14,7 @@ import org.key_project.util.EqualsModProofIrrelevancyUtil; import org.key_project.util.collection.ImmutableArray; + /** * A property that can be used in * {@link EqualsModProperty#equalsModProperty(Object, Property, Object[])} for terms. @@ -105,7 +106,8 @@ public boolean equalsModThisProperty(Term term1, Term term2, V... v) { */ @Override public int hashCodeModThisProperty(Term term) { - int hashcode = Objects.hash(term.op(), hashCodeIterable(term.subs()), + int hashcode = Objects.hash(term.op(), + EqualityUtils.hashCodeModPropertyOfIterable(PROOF_IRRELEVANCY_PROPERTY, term.subs()), EqualsModProofIrrelevancyUtil.hashCodeIterable(term.boundVars()), term.javaBlock()); // part from LabeledTermImpl diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/util/EqualityUtils.java b/key.core/src/main/java/de/uka/ilkd/key/logic/util/EqualityUtils.java index e149df04ef4..a737a9d73f9 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/util/EqualityUtils.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/util/EqualityUtils.java @@ -3,21 +3,21 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.logic.util; -import de.uka.ilkd.key.logic.Term; -import de.uka.ilkd.key.logic.equality.TermEqualsModProperty; -import de.uka.ilkd.key.logic.equality.TermProperty; +import de.uka.ilkd.key.logic.equality.EqualsModProperty; +import de.uka.ilkd.key.logic.equality.Property; public class EqualityUtils { /** - * Computes the hashcode of an iterable of terms modulo a given property using the elements' - * {@link TermEqualsModProperty} implementation. + * Computes the hashcode modulo a given property of an iterable of elements that implement + * {@link EqualsModProperty}. * * @param iter iterable of terms * @return combined hashcode */ - public static int hashCodeModPropertyOfIterable(TermProperty property, - Iterable iter) { + public static > int hashCodeModPropertyOfIterable( + Property property, + Iterable iter) { // adapted from Arrays.hashCode if (iter == null) { return 0; @@ -25,7 +25,7 @@ public static int hashCodeModPropertyOfIterable(TermProperty property, int result = 1; - for (Term element : iter) { + for (T element : iter) { result = 31 * result + (element == null ? 0 : element.hashCodeModProperty(property)); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/util/LinkedHashMapWrapper.java b/key.core/src/main/java/de/uka/ilkd/key/logic/util/LinkedHashMapWrapper.java index 060b6bb4b45..98e94a8f9b8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/util/LinkedHashMapWrapper.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/util/LinkedHashMapWrapper.java @@ -6,15 +6,14 @@ import java.util.Iterator; import de.uka.ilkd.key.logic.Term; -import de.uka.ilkd.key.logic.equality.TermEqualsModProperty; -import de.uka.ilkd.key.logic.equality.TermProperty; +import de.uka.ilkd.key.logic.equality.EqualsModProperty; +import de.uka.ilkd.key.logic.equality.Property; import de.uka.ilkd.key.util.LinkedHashMap; -import de.uka.ilkd.key.util.Pair; /** * This class is a wrapper for {@link LinkedHashMap} where the keys are {@link Term}s. *

- * Internally, the {@link Term}s are wrapped so that {@link TermEqualsModProperty} can be used for + * Internally, the {@link Term}s are wrapped so that {@link EqualsModProperty} can be used for * equality checks and * hash codes instead of the usual {@code equals} and {@code hashCode} methods of {@link Term}. * @@ -27,17 +26,18 @@ public class LinkedHashMapWrapper { private final LinkedHashMap map; /** - * The {@link TermProperty} that is used for equality checks and hash codes. + * The {@link Property} that is used for equality checks and hash codes. */ - private final TermProperty property; + private final Property property; /** * Constructs a new empty {@link LinkedHashMapWrapper}. * - * @param property the {@link TermProperty} that is used internally for equality checks and hash + * @param property the {@link Property} that is used internally for equality checks and + * hash * codes */ - public LinkedHashMapWrapper(TermProperty property) { + public LinkedHashMapWrapper(Property property) { this.property = property; map = new LinkedHashMap<>(); } @@ -47,10 +47,11 @@ public LinkedHashMapWrapper(TermProperty property) { * * @param key the key to be inserted * @param value the value corresponding to {@code key} - * @param property the {@link TermProperty} that is used internally for equality checks and hash + * @param property the {@link Property} that is used internally for equality checks and + * hash * codes */ - public LinkedHashMapWrapper(Term key, V value, TermProperty property) { + public LinkedHashMapWrapper(Term key, V value, Property property) { this(property); put(key, value); } @@ -64,10 +65,11 @@ public LinkedHashMapWrapper(Term key, V value, TermProperty property) { * * @param keys the array of keys to be inserted * @param values the array of values corresponding to the keys - * @param property the {@link TermProperty} that is used internally for equality checks and hash + * @param property the {@link Property} that is used internally for equality checks and + * hash * codes */ - public LinkedHashMapWrapper(Term[] keys, V[] values, TermProperty property) { + public LinkedHashMapWrapper(Term[] keys, V[] values, Property property) { this(property); putAll(keys, values); } @@ -81,10 +83,11 @@ public LinkedHashMapWrapper(Term[] keys, V[] values, TermProperty property) { * * @param keys the iterable of keys to be inserted * @param values the iterable of values corresponding to the keys - * @param property the {@link TermProperty} that is used internally for equality checks and hash + * @param property the {@link Property} that is used internally for equality checks and + * hash * codes */ - public LinkedHashMapWrapper(Iterable keys, Iterable values, TermProperty property) { + public LinkedHashMapWrapper(Iterable keys, Iterable values, Property property) { this(property); putAll(keys, values); } @@ -213,15 +216,15 @@ public boolean containsValue(V value) { * * @return an iterator over the key-value pairs in this map */ - public Iterator> iterator() { + public Iterator> iterator() { return new PairIterator<>(map); } /** - * This helper method wraps a term in a {@link TermWrapper} with the {@link TermProperty} of + * This helper method wraps a term in a {@link TermWrapper} with the {@link Property} of * this map. *

- * This is done so that {@link TermEqualsModProperty} can be used for equality checks and hash + * This is done so that {@link EqualsModProperty} can be used for equality checks and hash * codes instead of the * usual {@code equals} and {@code hashCode} methods of {@link Term} in the internal * {@link LinkedHashMap}. @@ -239,27 +242,31 @@ private TermWrapper wrapTerm(Term term) { * This class is used to wrap a term and override the {@code equals} and {@code hashCode} methods for use in a * {@link LinkedHashMap}. *

- * The wrapped term is equipped with a {@link TermProperty} that is used for - * {@link TermEqualsModProperty#equalsModProperty(Object, TermProperty)} and - * {@link TermEqualsModProperty#hashCodeModProperty(TermProperty)}. + * The wrapped term is equipped with a {@link Property} that is used for + * {@link EqualsModProperty#equalsModProperty(Object, Property, Object[])} and + * {@link EqualsModProperty#hashCodeModProperty(Property)} )}. * * @param term The term to be wrapped - * @param property The {@link TermProperty} that is used in the {@code equals} and {@code hashCode} methods + * @param property The {@link Property} that is used in the {@code equals} and {@code hashCode} methods */ - private record TermWrapper(Term term, TermProperty property) { - @Override - public boolean equals(Object obj) { - return term.equalsModProperty(obj, property); - } + private record TermWrapper(Term term, Property property) { - @Override - public int hashCode() { - return term.hashCodeModProperty(property); - } + @Override + public boolean equals(Object obj) { + return term.equalsModProperty(obj, property); } - // ------------- class to iterate over internal map and unwrap terms + @Override + public int hashCode() { + return term.hashCodeModProperty(property); + }} + + // ------------- record for term-value mapping + public record TermPair(Term term, V value) + { + } + // ------------- class to iterate over internal map and unwrap terms /** * This class is used to iterate over the key-value pairs in the {@link LinkedHashMapWrapper}. *

@@ -267,7 +274,7 @@ public int hashCode() { * * @param the type of the values in the {@link LinkedHashMapWrapper} */ - private static class PairIterator implements Iterator> { + private static class PairIterator implements Iterator> { /** * The iterator over the keys of the internal map. */ @@ -299,9 +306,9 @@ public boolean hasNext() { } @Override - public Pair next() { + public TermPair next() { last = keyIt.next(); - return new Pair<>(last.term(), map.get(last)); + return new TermPair<>(last.term(), map.get(last)); } @Override From b14e38f405081163578bc54ef035c14a62dea954 Mon Sep 17 00:00:00 2001 From: Tobias Reinhold Date: Tue, 30 Apr 2024 20:19:07 +0200 Subject: [PATCH 07/28] change LinkedHashMapWrapper to be more general --- .../key/logic/util/LinkedHashMapWrapper.java | 157 ++++++++++-------- 1 file changed, 88 insertions(+), 69 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/util/LinkedHashMapWrapper.java b/key.core/src/main/java/de/uka/ilkd/key/logic/util/LinkedHashMapWrapper.java index 98e94a8f9b8..77825d3aef3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/util/LinkedHashMapWrapper.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/util/LinkedHashMapWrapper.java @@ -10,34 +10,38 @@ import de.uka.ilkd.key.logic.equality.Property; import de.uka.ilkd.key.util.LinkedHashMap; +import org.key_project.util.collection.Pair; + /** - * This class is a wrapper for {@link LinkedHashMap} where the keys are {@link Term}s. - *

- * Internally, the {@link Term}s are wrapped so that {@link EqualsModProperty} can be used for - * equality checks and - * hash codes instead of the usual {@code equals} and {@code hashCode} methods of {@link Term}. + * This class is a wrapper for {@link LinkedHashMap} where the keys are elements that implement + * {@link EqualsModProperty}. * + * @param the type of the keys in the wrapped LinkedHashMap * @param the type of the values in the wrapped LinkedHashMap */ -public class LinkedHashMapWrapper { +public class LinkedHashMapWrapper, V> { + /* + * Internally, the elements are wrapped so that EqualsModProperty can be used for equality + * checks and hash codes instead of the usual equals and hashCode methods. + */ + /** * The wrapped {@link LinkedHashMap}. */ - private final LinkedHashMap map; + private final LinkedHashMap, V> map; /** - * The {@link Property} that is used for equality checks and hash codes. + * The {@link Property} that is used for equality checks and hash codes. */ - private final Property property; + private final Property property; /** * Constructs a new empty {@link LinkedHashMapWrapper}. * * @param property the {@link Property} that is used internally for equality checks and - * hash - * codes + * hash codes */ - public LinkedHashMapWrapper(Property property) { + public LinkedHashMapWrapper(Property property) { this.property = property; map = new LinkedHashMap<>(); } @@ -48,10 +52,9 @@ public LinkedHashMapWrapper(Property property) { * @param key the key to be inserted * @param value the value corresponding to {@code key} * @param property the {@link Property} that is used internally for equality checks and - * hash - * codes + * hash codes */ - public LinkedHashMapWrapper(Term key, V value, Property property) { + public LinkedHashMapWrapper(K key, V value, Property property) { this(property); put(key, value); } @@ -66,10 +69,9 @@ public LinkedHashMapWrapper(Term key, V value, Property property) { * @param keys the array of keys to be inserted * @param values the array of values corresponding to the keys * @param property the {@link Property} that is used internally for equality checks and - * hash - * codes + * hash codes */ - public LinkedHashMapWrapper(Term[] keys, V[] values, Property property) { + public LinkedHashMapWrapper(K[] keys, V[] values, Property property) { this(property); putAll(keys, values); } @@ -84,10 +86,9 @@ public LinkedHashMapWrapper(Term[] keys, V[] values, Property property) { * @param keys the iterable of keys to be inserted * @param values the iterable of values corresponding to the keys * @param property the {@link Property} that is used internally for equality checks and - * hash - * codes + * hash codes */ - public LinkedHashMapWrapper(Iterable keys, Iterable values, Property property) { + public LinkedHashMapWrapper(Iterable keys, Iterable values, Property property) { this(property); putAll(keys, values); } @@ -116,8 +117,8 @@ public boolean isEmpty() { * @param key the key whose presence in this map is to be tested * @return true if this map contains a mapping for the specified key */ - public boolean containsKey(Term key) { - return map.containsKey(wrapTerm(key)); + public boolean containsKey(K key) { + return map.containsKey(wrapKey(key)); } /** @@ -127,8 +128,8 @@ public boolean containsKey(Term key) { * @param key the key whose associated value is to be returned * @return the value to which the specified key is mapped */ - public V get(Term key) { - return map.get(wrapTerm(key)); + public V get(K key) { + return map.get(wrapKey(key)); } /** @@ -142,8 +143,8 @@ public V get(Term key) { * @return the previous value associated with {@code key}, or {@code null} if there was no * mapping for {@code key} */ - public V put(Term key, V value) { - return map.put(wrapTerm(key), value); + public V put(K key, V value) { + return map.put(wrapKey(key), value); } /** @@ -156,7 +157,7 @@ public V put(Term key, V value) { * @param keys the array of keys to be inserted * @param vals the array of values corresponding to the keys */ - public void putAll(Term[] keys, V[] vals) { + public void putAll(K[] keys, V[] vals) { for (int i = 0; i < keys.length; i++) { if (i < vals.length) { put(keys[i], vals[i]); @@ -176,9 +177,9 @@ public void putAll(Term[] keys, V[] vals) { * @param keys the iterable of keys to be inserted * @param vals the iterable of values corresponding to the keys */ - public void putAll(Iterable keys, Iterable vals) { + public void putAll(Iterable keys, Iterable vals) { Iterator itVals = vals.iterator(); - for (Term key : keys) { + for (K key : keys) { if (itVals.hasNext()) { put(key, itVals.next()); } else { @@ -195,8 +196,8 @@ public void putAll(Iterable keys, Iterable vals) { * @return the previous value associated with {@code key}, or {@code null} if there was no * mapping for {@code key} */ - public V remove(Term key) { - return map.remove(wrapTerm(key)); + public V remove(K key) { + return map.remove(wrapKey(key)); } /** @@ -216,86 +217,104 @@ public boolean containsValue(V value) { * * @return an iterator over the key-value pairs in this map */ - public Iterator> iterator() { + public Iterator> iterator() { return new PairIterator<>(map); } /** - * This helper method wraps a term in a {@link TermWrapper} with the {@link Property} of - * this map. + * This helper method wraps an element in an {@link ElementWrapper} with the {@link Property} + * of this map. *

- * This is done so that {@link EqualsModProperty} can be used for equality checks and hash - * codes instead of the - * usual {@code equals} and {@code hashCode} methods of {@link Term} in the internal + * This is done so that {@link EqualsModProperty} can be used for equality checks and hash codes + * instead of the usual {@code equals} and {@code hashCode} methods in the internal * {@link LinkedHashMap}. * - * @param term the term to be wrapped - * @return the wrapped term + * @param key the key to be wrapped + * @return the wrapped key */ - private TermWrapper wrapTerm(Term term) { - return new TermWrapper(term, property); + private ElementWrapper wrapKey(K key) { + return new ElementWrapper(key, property); } - // ------------- wrapper class for terms + // ------------- wrapper class for keys in the internal map /** - * This class is used to wrap a term and override the {@code equals} and {@code hashCode} methods for use in a - * {@link LinkedHashMap}. + * This class is used to wrap an element and override the {@code equals} and {@code hashCode} + * methods for use in a map. *

- * The wrapped term is equipped with a {@link Property} that is used for + * The wrapped element is equipped with a {@link Property} that is used for * {@link EqualsModProperty#equalsModProperty(Object, Property, Object[])} and - * {@link EqualsModProperty#hashCodeModProperty(Property)} )}. + * {@link EqualsModProperty#hashCodeModProperty(Property)} instead of the normal + * {@code equals} implementation. * - * @param term The term to be wrapped - * @param property The {@link Property} that is used in the {@code equals} and {@code hashCode} methods + * @param the type of the wrapped element */ - private record TermWrapper(Term term, Property property) { + private static class ElementWrapper> { + /** + * The wrapped element. + */ + K key; - @Override - public boolean equals(Object obj) { - return term.equalsModProperty(obj, property); - } + /** + * The {@link Property} that is used for equality checks and hash codes. + */ + Property property; - @Override - public int hashCode() { - return term.hashCodeModProperty(property); - }} + /** + * Creates a new wrapper for the given element. + * + * @param key the element to be wrapped + * @param property the {@link Property} that is used for equality checks and hash codes + */ + public ElementWrapper(K key, Property property) { + this.key = key; + this.property = property; + } - // ------------- record for term-value mapping - public record TermPair(Term term, V value) - { + @Override + public boolean equals(Object obj) { + return key.equalsModProperty(obj, property); + } + + @Override + public int hashCode() { + return key.hashCodeModProperty(property); + } } + // ------------- class to iterate over internal map and unwrap terms /** * This class is used to iterate over the key-value pairs in the {@link LinkedHashMapWrapper}. *

- * The terms in the pairs are unwrapped before returning them. + * The keys in the pairs are unwrapped before returning them. * + * @param the type of the keys in the {@link LinkedHashMapWrapper} * @param the type of the values in the {@link LinkedHashMapWrapper} */ - private static class PairIterator implements Iterator> { + private static class PairIterator, V> + implements Iterator> { /** * The iterator over the keys of the internal map. */ - private final Iterator keyIt; + private final Iterator> keyIt; /** * The internal map. */ - private final LinkedHashMap map; + private final LinkedHashMap, V> map; /** * The last key-value pair that was returned by {@link #next()}. */ - private TermWrapper last = null; + private ElementWrapper last = null; /** * Creates a new iterator over the key-value pairs in the {@link LinkedHashMapWrapper}. * * @param map the internal map of the {@link LinkedHashMapWrapper} to iterate over */ - public PairIterator(final LinkedHashMap map) { + public PairIterator(final LinkedHashMap, V> map) { this.map = map; keyIt = map.keySet().iterator(); } @@ -306,9 +325,9 @@ public boolean hasNext() { } @Override - public TermPair next() { + public Pair next() { last = keyIt.next(); - return new TermPair<>(last.term(), map.get(last)); + return new Pair<>(last.key, map.get(last)); } @Override From 5c47fc108dca6972ebcfc398340d407bee02b866 Mon Sep 17 00:00:00 2001 From: Tobias Reinhold Date: Sun, 5 May 2024 14:03:23 +0200 Subject: [PATCH 08/28] add tests for hashCodeModProperty at various spots where equalsModProperty was asserted to be true --- .../java/de/uka/ilkd/key/logic/TestTerm.java | 18 +++++++ .../logic/equality/TestEqualsModProperty.java | 48 +++++++++++++++++-- .../uka/ilkd/key/parser/TestTermParser.java | 3 ++ .../de/uka/ilkd/key/rule/TestApplyTaclet.java | 9 ++++ .../TestApplyUpdateOnRigidCondition.java | 21 ++++++++ .../key/speclang/jml/TestJMLTranslator.java | 18 +++++++ 6 files changed, 113 insertions(+), 4 deletions(-) diff --git a/key.core/src/test/java/de/uka/ilkd/key/logic/TestTerm.java b/key.core/src/test/java/de/uka/ilkd/key/logic/TestTerm.java index 6a8e3319620..a4bb8639218 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/logic/TestTerm.java +++ b/key.core/src/test/java/de/uka/ilkd/key/logic/TestTerm.java @@ -116,10 +116,16 @@ public void testProgramElementEqualsModRenaming() { assertTrue( match1.sub(0).equalsModProperty(match2, RenamingTermProperty.RENAMING_TERM_PROPERTY), "Terms should be equalModRenaming (0)."); + assertEquals(match1.sub(0).hashCodeModProperty(RenamingTermProperty.RENAMING_TERM_PROPERTY), + match2.hashCodeModProperty(RenamingTermProperty.RENAMING_TERM_PROPERTY), + "Hash codes should be equal. (0)"); assertTrue( match1.sub(0).equalsModProperty(match1.sub(1), RenamingTermProperty.RENAMING_TERM_PROPERTY), "Terms should be equalModRenaming (1)."); + assertEquals(match1.sub(0).hashCodeModProperty(RenamingTermProperty.RENAMING_TERM_PROPERTY), + match1.sub(1).hashCodeModProperty(RenamingTermProperty.RENAMING_TERM_PROPERTY), + "Hash codes should be equal. (1)"); Term match3 = TacletForTests.parseTerm("\\<{ int j = 0; }\\>true "); assertNotEquals(match1, match3, "Terms should not be equal."); @@ -131,14 +137,23 @@ public void testEqualsModRenamingWithLabels() { Term match2 = TacletForTests.parseTerm("\\<{ label0:{ label1:{ } } }\\>true"); assertTrue(match1.equalsModProperty(match2, RenamingTermProperty.RENAMING_TERM_PROPERTY), "Terms should be equalModRenaming."); + assertEquals(match1.hashCodeModProperty(RenamingTermProperty.RENAMING_TERM_PROPERTY), + match2.hashCodeModProperty(RenamingTermProperty.RENAMING_TERM_PROPERTY), + "Hash codes should be equal modulo renaming. (0)"); Term match3 = TacletForTests.parseTerm("\\<{ label0:{ label1:{ int i = 0; } } }\\>true"); Term match4 = TacletForTests.parseTerm("\\<{ label0:{ label1:{ int j = 0; } } }\\>true"); assertTrue(match3.equalsModProperty(match4, RenamingTermProperty.RENAMING_TERM_PROPERTY), "Terms should be equalModRenaming."); + assertEquals(match3.hashCodeModProperty(RenamingTermProperty.RENAMING_TERM_PROPERTY), + match4.hashCodeModProperty(RenamingTermProperty.RENAMING_TERM_PROPERTY), + "Hash codes should be equal modulo renaming. (1)"); Term match5 = TacletForTests.parseTerm("\\<{ label0:{ label1:{ int i = 0; } } }\\>true"); Term match6 = TacletForTests.parseTerm("\\<{ label0:{ label1:{ int i = 0; } } }\\>true"); assertTrue(match5.equalsModProperty(match6, RenamingTermProperty.RENAMING_TERM_PROPERTY), "Terms should be equalModRenaming."); + assertEquals(match5.hashCodeModProperty(RenamingTermProperty.RENAMING_TERM_PROPERTY), + match6.hashCodeModProperty(RenamingTermProperty.RENAMING_TERM_PROPERTY), + "Hash codes should be equal modulo renaming. (2)"); } @Test @@ -152,6 +167,9 @@ public void testEqualsModRenaming() { assertTrue(quant1.equalsModProperty(quant2, RenamingTermProperty.RENAMING_TERM_PROPERTY), "Terms " + quant1 + " and " + quant2 + " should be equal mod renaming"); + assertEquals(quant1.hashCodeModProperty(RenamingTermProperty.RENAMING_TERM_PROPERTY), + quant2.hashCodeModProperty(RenamingTermProperty.RENAMING_TERM_PROPERTY), + "Hash codes should be equal modulo renaming."); } diff --git a/key.core/src/test/java/de/uka/ilkd/key/logic/equality/TestEqualsModProperty.java b/key.core/src/test/java/de/uka/ilkd/key/logic/equality/TestEqualsModProperty.java index 03fd1b2b4e2..ef17a3062c9 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/logic/equality/TestEqualsModProperty.java +++ b/key.core/src/test/java/de/uka/ilkd/key/logic/equality/TestEqualsModProperty.java @@ -7,6 +7,7 @@ import de.uka.ilkd.key.java.Comment; import de.uka.ilkd.key.java.NameAbstractionTable; +import de.uka.ilkd.key.java.ProgramElement; import de.uka.ilkd.key.java.expression.literal.StringLiteral; import de.uka.ilkd.key.logic.*; import de.uka.ilkd.key.logic.label.*; @@ -88,6 +89,10 @@ public void renaming() { "Should be true as labels do not matter"); assertTrue(term2.equalsModProperty(term1, RENAMING_TERM_PROPERTY), "Should be true as labels do not matter"); + assertEquals(term1.hashCodeModProperty(RENAMING_TERM_PROPERTY), + term2.hashCodeModProperty(RENAMING_TERM_PROPERTY), + "Hash codes should be equal as labels do not matter (0)"); + labels1 = new ImmutableArray<>(relevantLabel1); term1 = tb.label(term1, labels1); @@ -95,6 +100,9 @@ public void renaming() { "Should be true as labels do not matter"); assertTrue(term2.equalsModProperty(term1, RENAMING_TERM_PROPERTY), "Should be true as labels do not matter"); + assertEquals(term1.hashCodeModProperty(RENAMING_TERM_PROPERTY), + term2.hashCodeModProperty(RENAMING_TERM_PROPERTY), + "Hash codes should be equal as labels do not matter (1)"); ImmutableArray labels2 = new ImmutableArray<>(relevantLabel2); term2 = tb.label(term2, labels2); @@ -102,6 +110,9 @@ public void renaming() { "Should be true as labels do not matter"); assertTrue(term2.equalsModProperty(term1, RENAMING_TERM_PROPERTY), "Should be true as labels do not matter"); + assertEquals(term1.hashCodeModProperty(RENAMING_TERM_PROPERTY), + term2.hashCodeModProperty(RENAMING_TERM_PROPERTY), + "Hash codes should be equal as labels do not matter (2)"); } // equalsModProperty(...) with IRRELEVANT_TERM_LABELS_PROPERTY @@ -142,6 +153,9 @@ public void irrelevantTermLabels() { "Should be true as term1 has no relevant term labels and term2 does not have any labels"); assertTrue(term2.equalsModProperty(term1, IRRELEVANT_TERM_LABELS_PROPERTY), "Should be true as term1 has no relevant term labels and term2 does not have any labels"); + assertEquals(term1.hashCodeModProperty(IRRELEVANT_TERM_LABELS_PROPERTY), + term2.hashCodeModProperty(IRRELEVANT_TERM_LABELS_PROPERTY), + "Hash codes should be equal as term1 has no relevant term labels and term2 does not have any labels (0)"); // ------------ same relevant labels labels1 = new ImmutableArray<>(relevantLabel1, relevantLabel2); @@ -153,6 +167,9 @@ public void irrelevantTermLabels() { "Should be true as both terms have the same relevant term labels"); assertTrue(term2.equalsModProperty(term1, IRRELEVANT_TERM_LABELS_PROPERTY), "Should be true as both terms have the same relevant term labels"); + assertEquals(term1.hashCodeModProperty(IRRELEVANT_TERM_LABELS_PROPERTY), + term2.hashCodeModProperty(IRRELEVANT_TERM_LABELS_PROPERTY), + "Hash codes should be equal as both terms have the same relevant term labels (1)"); // ------------ not the same relevant labels labels1 = new ImmutableArray<>(relevantLabel1, irrelevantLabel); @@ -196,6 +213,9 @@ public void allTermLabels() { "Should be true as underlying terms are equal"); assertTrue(term2.equalsModProperty(term1, TERM_LABELS_PROPERTY), "Should be true as underlying terms are equal"); + assertEquals(term1.hashCodeModProperty(TERM_LABELS_PROPERTY), + term2.hashCodeModProperty(TERM_LABELS_PROPERTY), + "Hash codes should be equal as all term labels are ignored (0)"); // ------------ same relevant labels labels1 = new ImmutableArray<>(relevantLabel1, relevantLabel2); @@ -207,6 +227,9 @@ public void allTermLabels() { "Should be true as underlying terms are equal"); assertTrue(term2.equalsModProperty(term1, TERM_LABELS_PROPERTY), "Should be true as underlying terms are equal"); + assertEquals(term1.hashCodeModProperty(TERM_LABELS_PROPERTY), + term2.hashCodeModProperty(TERM_LABELS_PROPERTY), + "Hash codes should be equal as all term labels are ignored (1)"); // ------------ not the same relevant labels labels1 = new ImmutableArray<>(relevantLabel1, irrelevantLabel); @@ -217,6 +240,9 @@ public void allTermLabels() { "Should be true as underlying terms are equal"); assertTrue(term2.equalsModProperty(term1, TERM_LABELS_PROPERTY), "Should be true as underlying terms are equal"); + assertEquals(term1.hashCodeModProperty(TERM_LABELS_PROPERTY), + term2.hashCodeModProperty(TERM_LABELS_PROPERTY), + "Hash codes should be equal as all term labels are ignored (2)"); } // equalsModProperty(...) with PROOF_IRRELEVANCY_PROPERTY @@ -257,6 +283,9 @@ public void proofIrrelevancy() { "Should be true as term1 has no relevant term labels and term2 does not have any labels"); assertTrue(term2.equalsModProperty(term1, PROOF_IRRELEVANCY_PROPERTY), "Should be true as term1 has no relevant term labels and term2 does not have any labels"); + assertEquals(term1.hashCodeModProperty(PROOF_IRRELEVANCY_PROPERTY), + term2.hashCodeModProperty(PROOF_IRRELEVANCY_PROPERTY), + "Hash codes should be equal as proof irrelevant properties are ignored (0)"); // ------------ same relevant labels labels1 = new ImmutableArray<>(relevantLabel1, relevantLabel2, irrelevantLabel); @@ -268,6 +297,9 @@ public void proofIrrelevancy() { "Should be true as both terms have the same relevant term labels"); assertTrue(term2.equalsModProperty(term1, PROOF_IRRELEVANCY_PROPERTY), "Should be true as both terms have the same relevant term labels"); + assertEquals(term1.hashCodeModProperty(PROOF_IRRELEVANCY_PROPERTY), + term2.hashCodeModProperty(PROOF_IRRELEVANCY_PROPERTY), + "Hash codes should be equal as proof irrelevant properties are ignored (1)"); labels1 = new ImmutableArray<>(relevantLabel1, relevantLabel2, irrelevantLabel); labels2 = new ImmutableArray<>(relevantLabel1, relevantLabel2); @@ -277,6 +309,9 @@ public void proofIrrelevancy() { "Should be true as both terms have the same relevant term labels and irrelevant labels do not matter"); assertTrue(term2.equalsModProperty(term1, PROOF_IRRELEVANCY_PROPERTY), "Should be true as both terms have the same relevant term labels and irrelevant labels do not matter"); + assertEquals(term1.hashCodeModProperty(PROOF_IRRELEVANCY_PROPERTY), + term2.hashCodeModProperty(PROOF_IRRELEVANCY_PROPERTY), + "Hash codes should be equal as proof irrelevant properties are ignored (2)"); // ------------ not the same relevant labels labels1 = new ImmutableArray<>(relevantLabel1); @@ -291,11 +326,16 @@ public void proofIrrelevancy() { @Test public void renamingSourceElements() { - Term match1 = TacletForTests.parseTerm("\\<{ int i; int j; /*Test*/ }\\>true"); - Term match2 = TacletForTests.parseTerm("\\<{ int i; /*Another test*/ int k; }\\>true"); + ProgramElement match1 = TacletForTests.parsePrg("{ int i; int j; /*Test*/ }"); + ProgramElement match2 = TacletForTests.parsePrg("{ int i; /*Another test*/ int k; }"); assertTrue( - match1.equalsModProperty(match2, RenamingTermProperty.RENAMING_TERM_PROPERTY), - "Terms should be equalModRenaming (0)."); + match1.equalsModProperty(match2, RENAMING_SOURCE_ELEMENT_PROPERTY, + new NameAbstractionTable()), + "ProgramElements should be equal modulo renaming (0)."); + assertEquals(match1.hashCodeModProperty(RENAMING_SOURCE_ELEMENT_PROPERTY), + match2.hashCodeModProperty(RENAMING_SOURCE_ELEMENT_PROPERTY), + "Hash codes should be equal as ProgramElements are equal modulo renaming (0)."); + Comment testComment = new Comment("test"); StringLiteral stringLiteral = new StringLiteral("testStringLiteral"); diff --git a/key.core/src/test/java/de/uka/ilkd/key/parser/TestTermParser.java b/key.core/src/test/java/de/uka/ilkd/key/parser/TestTermParser.java index 8337dd79455..609497cdcc9 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/parser/TestTermParser.java +++ b/key.core/src/test/java/de/uka/ilkd/key/parser/TestTermParser.java @@ -260,6 +260,9 @@ public void test13() throws Exception { + "\\<{ int p_y = 1;boolean p_x = 2<1;" + "while(p_x){ int s=3 ;} }\\>" + " true)"); assertTrue(t3.equalsModProperty(t4, RENAMING_TERM_PROPERTY), "Terms should be equalModRenaming"); + assertEquals(t3.hashCodeModProperty(RENAMING_TERM_PROPERTY), + t4.hashCodeModProperty(RENAMING_TERM_PROPERTY), + "Hash codes should be equalModRenaming"); } @Test diff --git a/key.core/src/test/java/de/uka/ilkd/key/rule/TestApplyTaclet.java b/key.core/src/test/java/de/uka/ilkd/key/rule/TestApplyTaclet.java index a1df0325dca..55abf044cb7 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/rule/TestApplyTaclet.java +++ b/key.core/src/test/java/de/uka/ilkd/key/rule/TestApplyTaclet.java @@ -745,6 +745,9 @@ private void doTestCatchList(int p_proof) { "Wrong result. Expected:" + ProofSaver.printAnything(correctFormula, TacletForTests.services()) + " But was:" + ProofSaver.printAnything(resultFormula, TacletForTests.services())); + assertEquals(resultFormula.hashCodeModProperty(RENAMING_TERM_PROPERTY), + correctFormula.hashCodeModProperty(RENAMING_TERM_PROPERTY), + "Hash codes of formulas should be equal modulo renaming"); } private Goal createGoal(Node n, TacletIndex tacletIndex) { @@ -853,6 +856,9 @@ public void testContextAdding() { expected.equalsModProperty(is, RENAMING_SOURCE_ELEMENT_PROPERTY, new NameAbstractionTable()), "Expected:" + expected + "\n but was:" + is); + assertEquals(expected.hashCodeModProperty(RENAMING_SOURCE_ELEMENT_PROPERTY), + is.hashCodeModProperty(RENAMING_SOURCE_ELEMENT_PROPERTY), + "Hash codes of ProgramElements should be equals modulo renaming."); } /** @@ -889,6 +895,9 @@ public void testRemoveEmptyBlock() { expected.equalsModProperty(is, RENAMING_SOURCE_ELEMENT_PROPERTY, new NameAbstractionTable()), "Expected:" + expected + "\n but was:" + is); + assertEquals(expected.hashCodeModProperty(RENAMING_SOURCE_ELEMENT_PROPERTY), + is.hashCodeModProperty(RENAMING_SOURCE_ELEMENT_PROPERTY), + "Hash codes of ProgramElements should be equal modulo renaming."); } @Test diff --git a/key.core/src/test/java/de/uka/ilkd/key/rule/conditions/TestApplyUpdateOnRigidCondition.java b/key.core/src/test/java/de/uka/ilkd/key/rule/conditions/TestApplyUpdateOnRigidCondition.java index 8c2347bbc55..ec338c9d17d 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/rule/conditions/TestApplyUpdateOnRigidCondition.java +++ b/key.core/src/test/java/de/uka/ilkd/key/rule/conditions/TestApplyUpdateOnRigidCondition.java @@ -27,6 +27,9 @@ void updateWithoutVariables() { Term expected = TacletForTests.parseTerm("\\forall int a; {i:=0}(a = i)"); assertTrue(expected.equalsModProperty(result, RENAMING_TERM_PROPERTY), "Update without free variables was not properly applied on formula!"); + assertEquals(expected.hashCodeModProperty(RENAMING_TERM_PROPERTY), + result.hashCodeModProperty(RENAMING_TERM_PROPERTY), + "Terms should be equal modulo renaming. (0)"); term = TacletForTests.parseTerm("{i:=0}(i = 0)"); result = applyUpdateOnFormula(term); @@ -39,6 +42,9 @@ void updateWithoutVariables() { expected = TacletForTests.parseTerm("f({i:=0} const)"); assertTrue(expected.equalsModProperty(result, RENAMING_TERM_PROPERTY), "Update without free variables was not properly applied on term!"); + assertEquals(expected.hashCodeModProperty(RENAMING_TERM_PROPERTY), + result.hashCodeModProperty(RENAMING_TERM_PROPERTY), + "Terms should be equal modulo renaming. (1)"); } @Test @@ -53,6 +59,9 @@ void updateWithVariablesNoClash() { TacletForTests.parseTerm("\\forall int b; \\forall java.lang.Object a; {i:=b} (a = i)"); assertTrue(expected.equalsModProperty(result, RENAMING_TERM_PROPERTY), "Update is not simply pulled over quantification!"); + assertEquals(expected.hashCodeModProperty(RENAMING_TERM_PROPERTY), + result.hashCodeModProperty(RENAMING_TERM_PROPERTY), + "Terms should be equal modulo renaming. (0)"); term = TacletForTests.parseTerm("\\forall int b; {i:=b} (0 = i)"); b = term.boundVars().get(0); @@ -60,6 +69,9 @@ void updateWithVariablesNoClash() { expected = TacletForTests.parseTerm("\\forall int b; {i:=b} 0 = {i:=b} i"); assertTrue(expected.equalsModProperty(result, RENAMING_TERM_PROPERTY), "Update is not simply pulled over equality!"); + assertEquals(expected.hashCodeModProperty(RENAMING_TERM_PROPERTY), + result.hashCodeModProperty(RENAMING_TERM_PROPERTY), + "Terms should be equal modulo renaming. (1)"); term = TacletForTests.parseTerm("\\forall int b; {i:=b} f(const) = 0"); b = term.boundVars().get(0); @@ -67,6 +79,9 @@ void updateWithVariablesNoClash() { expected = TacletForTests.parseTerm("\\forall int b; f({i:=b} const) = 0"); assertTrue(expected.equalsModProperty(result, RENAMING_TERM_PROPERTY), "Update is not simply pulled over function symbol!"); + assertEquals(expected.hashCodeModProperty(RENAMING_TERM_PROPERTY), + result.hashCodeModProperty(RENAMING_TERM_PROPERTY), + "Terms should be equal modulo renaming. (2)"); } @Test @@ -81,6 +96,9 @@ void updateWithVariablesAndClash() { .parseTerm("\\forall int a; \\forall java.lang.Object a1; {i:=a} (a1 = i)"); assertTrue(expected.equalsModProperty(result, RENAMING_TERM_PROPERTY), "Renaming or applying update afterwards !"); + assertEquals(expected.hashCodeModProperty(RENAMING_TERM_PROPERTY), + result.hashCodeModProperty(RENAMING_TERM_PROPERTY), + "Terms should be equal modulo renaming. (0)"); term = TacletForTests.parseTerm( "\\forall int a1; \\forall int a; {i:=a}\\forall java.lang.Object a; i = a1"); @@ -91,6 +109,9 @@ void updateWithVariablesAndClash() { "\\forall int a1; \\forall int a; \\forall java.lang.Object a2; {i:=a} (i = a1)"); assertTrue(expected.equalsModProperty(result, RENAMING_TERM_PROPERTY), "Counter appended to stem was not increased high enough!"); + assertEquals(expected.hashCodeModProperty(RENAMING_TERM_PROPERTY), + result.hashCodeModProperty(RENAMING_TERM_PROPERTY), + "Terms should be equal modulo renaming. (1)"); } @Test diff --git a/key.core/src/test/java/de/uka/ilkd/key/speclang/jml/TestJMLTranslator.java b/key.core/src/test/java/de/uka/ilkd/key/speclang/jml/TestJMLTranslator.java index 10e0bf0b853..0f6d59684a5 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/speclang/jml/TestJMLTranslator.java +++ b/key.core/src/test/java/de/uka/ilkd/key/speclang/jml/TestJMLTranslator.java @@ -188,6 +188,9 @@ public void testForAll() { TB.and(TB.leq(TB.zTerm("0"), TB.var(i)), TB.leq(TB.var(i), TB.zTerm("2147483647"))))); assertTrue(result.equalsModProperty(expected, RENAMING_TERM_PROPERTY), "Result was: " + result + "; \nExpected was: " + expected); + assertEquals(result.hashCodeModProperty(RENAMING_TERM_PROPERTY), + expected.hashCodeModProperty(RENAMING_TERM_PROPERTY), + "Hash codes should be equal modulo renaming."); } @@ -204,6 +207,9 @@ public void testForEx() { TB.and(TB.leq(TB.zTerm("0"), TB.var(i)), TB.leq(TB.var(i), TB.zTerm("2147483647"))))); assertTrue(result.equalsModProperty(expected, RENAMING_TERM_PROPERTY), "Result was: " + result + "; \nExpected was: " + expected); + assertEquals(result.hashCodeModProperty(RENAMING_TERM_PROPERTY), + expected.hashCodeModProperty(RENAMING_TERM_PROPERTY), + "Hash codes should be equal modulo renaming."); } @@ -220,6 +226,9 @@ public void testBsumInt() { Assertions.assertSame(q, result.sub(0).op()); assertTrue(result.equalsModProperty(expected, RENAMING_TERM_PROPERTY), "Result was: " + result + "; \nExpected was: " + expected); + assertEquals(result.hashCodeModProperty(RENAMING_TERM_PROPERTY), + expected.hashCodeModProperty(RENAMING_TERM_PROPERTY), + "Hash codes should be equal modulo renaming."); } @@ -234,6 +243,9 @@ public void testBsumBigInt() { Assertions.assertSame(q, result.op()); assertTrue(result.equalsModProperty(expected, RENAMING_TERM_PROPERTY), "Result was: " + result + "; \nExpected was: " + expected); + assertEquals(result.hashCodeModProperty(RENAMING_TERM_PROPERTY), + expected.hashCodeModProperty(RENAMING_TERM_PROPERTY), + "Hash codes should be equal modulo renaming."); } @Test @@ -251,6 +263,9 @@ public void testInfiniteUnion() { TB.ife(guard, TB.empty(), TB.empty())); assertTrue(result.equalsModProperty(expected, RENAMING_TERM_PROPERTY), "Result was: " + result + "; \nExpected was: " + expected); + assertEquals(result.hashCodeModProperty(RENAMING_TERM_PROPERTY), + expected.hashCodeModProperty(RENAMING_TERM_PROPERTY), + "Hash codes should be equal modulo renaming."); } @Test @@ -269,6 +284,9 @@ public void testInfiniteUnion2() { TB.ife(guard, TB.empty(), TB.empty())); assertTrue(result.equalsModProperty(expected, RENAMING_TERM_PROPERTY), "Result was: " + result + "; \nExpected was: " + expected); + assertEquals(result.hashCodeModProperty(RENAMING_TERM_PROPERTY), + expected.hashCodeModProperty(RENAMING_TERM_PROPERTY), + "Hash codes should be equal modulo renaming."); } From 2c8849317b1425fc58ce0bfb344f8bcce5cfadc2 Mon Sep 17 00:00:00 2001 From: Tobias Reinhold Date: Fri, 10 May 2024 18:29:07 +0200 Subject: [PATCH 09/28] change small things about hashCodeModProperty() when ignoring irrelevant or all term labels --- .../key/logic/equality/IrrelevantTermLabelsProperty.java | 8 ++++++-- .../uka/ilkd/key/logic/equality/TermLabelsProperty.java | 8 ++++---- 2 files changed, 10 insertions(+), 6 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/IrrelevantTermLabelsProperty.java b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/IrrelevantTermLabelsProperty.java index 805f55cd4fc..9c6b0dc8cd6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/IrrelevantTermLabelsProperty.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/IrrelevantTermLabelsProperty.java @@ -98,8 +98,12 @@ public int hashCodeModThisProperty(Term term) { hashcode = hashcode * 17 + term.boundVars().hashCode(); hashcode = hashcode * 17 + term.javaBlock().hashCode(); - for (TermLabel label : term.getLabels()) { - hashcode += (label.isProofRelevant() ? 7 * label.hashCode() : 0); + final ImmutableArray labels = term.getLabels(); + for (int i = 0, sz = labels.size(); i < sz; i++) { + final TermLabel currentLabel = labels.get(i); + if (currentLabel.isProofRelevant()) { + hashcode += 7 * currentLabel.hashCode(); + } } return hashcode; diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/TermLabelsProperty.java b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/TermLabelsProperty.java index 9bce4f5aeb7..d44f9915cc1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/TermLabelsProperty.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/TermLabelsProperty.java @@ -66,16 +66,16 @@ public boolean equalsModThisProperty(Term term1, Term term2, V... v) { /** * Computes the hash code of {@code term} while ignoring all term labels. - *

- * Currently, the hash code is computed almost the same way as in TermImpl. This is also the - * case for labeled terms, - * as all term labels are ignored. * * @param term the term to compute the hash code for * @return the hash code */ @Override public int hashCodeModThisProperty(Term term) { + /* + * Currently, the hash code is computed almost the same way as in TermImpl. This is also the + * case for labeled terms, as all term labels are ignored. + */ int hashcode = 5; hashcode = hashcode * 17 + term.op().hashCode(); hashcode = hashcode * 17 From f3f95339c45c9a1027b0c0476ba10f547c6ebc7e Mon Sep 17 00:00:00 2001 From: Tobias Reinhold Date: Sun, 12 May 2024 15:19:53 +0200 Subject: [PATCH 10/28] start idea for hash codes modulo renaming on SourceElements --- .../RenamingSourceElementProperty.java | 44 +++++++++++++++++-- 1 file changed, 40 insertions(+), 4 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingSourceElementProperty.java b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingSourceElementProperty.java index 82279627ec6..d638d415771 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingSourceElementProperty.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingSourceElementProperty.java @@ -97,11 +97,44 @@ public boolean equalsModThisProperty(SourceElement se1, SourceElement se2, V @Override public int hashCodeModThisProperty(SourceElement sourceElement) { - throw new UnsupportedOperationException( - "Hashing of SourceElements modulo renaming not yet implemented!"); + /* + * Currently, the best approach seems to walk through the sourceElement with a + * JavaASTTreeWalker and sum up hash codes. + */ + JavaASTTreeWalker tw = new JavaASTTreeWalker(sourceElement); + SourceElement next = tw.currentNode(); + + int hashCode = 1; + + while (next != null) { + // Handle special cases of prior equalsModRenaming implementation + if (next instanceof LabeledStatement ls) { + // TODO: decide what to add here; + hashCode = 31 * hashCode + ls.getChildCount(); + } else if (next instanceof VariableSpecification vs) { + hashCode = 31 * hashCode + 5; + } else if (next instanceof ProgramVariable || next instanceof ProgramElementName) { + // TODO: decide what to add here; + hashCode = 31 * hashCode + 37; + } else if (next instanceof JavaNonTerminalProgramElement jnte) { + // TODO: decide what to add here; + hashCode = 31 * hashCode + 43; + } else { + // In the standard case, we just use the default hashCode implementation + hashCode = 31 * hashCode + next.hashCode(); + } + + // walk to the next nodes in the tree + next = tw.nextNode(); + } + + return hashCode; } - /* --------------------- Helper methods for special cases ---------------------- */ + /* + * --------------------- Helper methods for special cases in equalsModThisProperty + * ---------------------- + */ /** * Handles the standard case of comparing two {@link SourceElement}s modulo renaming. * @@ -244,5 +277,8 @@ private boolean handleProgramVariableOrElementName(SourceElement se1, SourceElem } - /* ------------------ End of helper methods for special cases ------------------ */ + /* + * ------------------ End of helper methods for special cases in + * equalsModThisProperty------------------ + */ } From 76f72587323f52b98100e1768e16ef424a76bdc9 Mon Sep 17 00:00:00 2001 From: Tobias Reinhold Date: Thu, 16 May 2024 18:10:03 +0200 Subject: [PATCH 11/28] start implementation of more complex hash function (still has a bug) --- .../RenamingSourceElementProperty.java | 44 ++++++++++++------- 1 file changed, 29 insertions(+), 15 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingSourceElementProperty.java b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingSourceElementProperty.java index d638d415771..bf0517a21f4 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingSourceElementProperty.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingSourceElementProperty.java @@ -3,6 +3,8 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.logic.equality; +import java.util.*; + import de.uka.ilkd.key.java.JavaNonTerminalProgramElement; import de.uka.ilkd.key.java.NameAbstractionTable; import de.uka.ilkd.key.java.SourceElement; @@ -104,21 +106,27 @@ public int hashCodeModThisProperty(SourceElement sourceElement) { JavaASTTreeWalker tw = new JavaASTTreeWalker(sourceElement); SourceElement next = tw.currentNode(); + NameAbstractionMap absMap = new NameAbstractionMap(); + int hashCode = 1; while (next != null) { - // Handle special cases of prior equalsModRenaming implementation + // Handle special cases so that hashCodeModThisProperty fits equalsModThisProperty if (next instanceof LabeledStatement ls) { - // TODO: decide what to add here; hashCode = 31 * hashCode + ls.getChildCount(); + absMap.add(ls); } else if (next instanceof VariableSpecification vs) { - hashCode = 31 * hashCode + 5; + hashCode = 31 * hashCode + vs.getChildCount(); + hashCode = + 31 * hashCode + 17 * ((vs.getType() == null) ? 0 : vs.getType().hashCode()) + + vs.getDimensions(); + absMap.add(vs); } else if (next instanceof ProgramVariable || next instanceof ProgramElementName) { - // TODO: decide what to add here; - hashCode = 31 * hashCode + 37; + // TODO: fix; somehow this returns null, meaning that something must be looked up, + // that is not yet in the map + hashCode = 31 * hashCode + absMap.getDepth(next); } else if (next instanceof JavaNonTerminalProgramElement jnte) { - // TODO: decide what to add here; - hashCode = 31 * hashCode + 43; + hashCode = 31 * hashCode + jnte.getChildCount(); } else { // In the standard case, we just use the default hashCode implementation hashCode = 31 * hashCode + next.hashCode(); @@ -131,10 +139,7 @@ public int hashCodeModThisProperty(SourceElement sourceElement) { return hashCode; } - /* - * --------------------- Helper methods for special cases in equalsModThisProperty - * ---------------------- - */ + /*------------- Helper methods for special cases in equalsModThisProperty --------------*/ /** * Handles the standard case of comparing two {@link SourceElement}s modulo renaming. * @@ -277,8 +282,17 @@ private boolean handleProgramVariableOrElementName(SourceElement se1, SourceElem } - /* - * ------------------ End of helper methods for special cases in - * equalsModThisProperty------------------ - */ + /* ---------- End of helper methods for special cases in equalsModThisProperty ---------- */ + + private static class NameAbstractionMap { + private final Map declarationsMap = new HashMap<>(); + + public void add(SourceElement element) { + declarationsMap.put(element, declarationsMap.size()); + } + + public int getDepth(SourceElement element) { + return declarationsMap.get(element); + } + } } From 7cfdcc2e89fd1467f23b0de68522e927a92b027b Mon Sep 17 00:00:00 2001 From: Tobias Reinhold Date: Thu, 16 May 2024 20:44:21 +0200 Subject: [PATCH 12/28] fix and finish hashCodeModThisProperty for RenamingSourceElementProperty --- .../RenamingSourceElementProperty.java | 42 +++++++++++++++---- 1 file changed, 35 insertions(+), 7 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingSourceElementProperty.java b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingSourceElementProperty.java index bf0517a21f4..233fbdc5a2b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingSourceElementProperty.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingSourceElementProperty.java @@ -122,9 +122,7 @@ public int hashCodeModThisProperty(SourceElement sourceElement) { + vs.getDimensions(); absMap.add(vs); } else if (next instanceof ProgramVariable || next instanceof ProgramElementName) { - // TODO: fix; somehow this returns null, meaning that something must be looked up, - // that is not yet in the map - hashCode = 31 * hashCode + absMap.getDepth(next); + hashCode = 31 * hashCode + absMap.getAbstractName(next); } else if (next instanceof JavaNonTerminalProgramElement jnte) { hashCode = 31 * hashCode + jnte.getChildCount(); } else { @@ -284,15 +282,45 @@ private boolean handleProgramVariableOrElementName(SourceElement se1, SourceElem /* ---------- End of helper methods for special cases in equalsModThisProperty ---------- */ + /** + * A helper class to map {@link SourceElement}s to an abstract name. + *

+ * As names are abstracted from in this property, we need to give named elements abstract names + * for them to be used in the hash code. This approach is similar to + * {@link NameAbstractionTable}, where we collect elements with names in the order they are + * declared. Each element is associated with the number of previously added elements, which is + * then used as the abstract name. + */ private static class NameAbstractionMap { - private final Map declarationsMap = new HashMap<>(); + /** + * The map that associates {@link SourceElement}s with their abstract names. + */ + private final Map map = new HashMap<>(); + /** + * Adds a {@link SourceElement} to the map. + * + * @param element the {@link SourceElement} to be added + */ public void add(SourceElement element) { - declarationsMap.put(element, declarationsMap.size()); + map.put(element, map.size()); } - public int getDepth(SourceElement element) { - return declarationsMap.get(element); + /** + * Returns the abstract name of a {@link SourceElement} or {@code -1} if the element is not + * in the map. + *

+ * A common case for a look-up of an element that is not in the map, is a built-in datatype, + * e.g., the {@link ProgramElementName} {@code int}. + * + * @param element the {@link SourceElement} whose abstract name should be returned + * @return the abstract name of the {@link SourceElement} or {@code -1} if the element is + * not + * in the map + */ + public int getAbstractName(SourceElement element) { + final Integer result = map.get(element); + return result != null ? result : -1; } } } From 09ebe685689d65c60c9d960c8c7c1d6136a3124b Mon Sep 17 00:00:00 2001 From: Tobias Reinhold Date: Fri, 17 May 2024 20:11:20 +0200 Subject: [PATCH 13/28] start implementation of hashCodeModThisProperty for RenamingTermProperty (wip) --- .../RenamingSourceElementProperty.java | 3 +- .../logic/equality/RenamingTermProperty.java | 55 ++++++++++++++++++- 2 files changed, 54 insertions(+), 4 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingSourceElementProperty.java b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingSourceElementProperty.java index 233fbdc5a2b..e71c94759cd 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingSourceElementProperty.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingSourceElementProperty.java @@ -315,8 +315,7 @@ public void add(SourceElement element) { * * @param element the {@link SourceElement} whose abstract name should be returned * @return the abstract name of the {@link SourceElement} or {@code -1} if the element is - * not - * in the map + * not in the map */ public int getAbstractName(SourceElement element) { final Integer result = map.get(element); diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingTermProperty.java b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingTermProperty.java index a8333ab77f4..b5c4d3e7bbb 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingTermProperty.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingTermProperty.java @@ -64,8 +64,8 @@ public boolean equalsModThisProperty(Term term1, Term term2, V... v) { */ @Override public int hashCodeModThisProperty(Term term) { - throw new UnsupportedOperationException( - "Hashing of terms modulo renaming not yet implemented!"); + // Labels can be completely ignored + return helper1(term, ImmutableSLList.nil()); } // equals modulo renaming logic @@ -250,6 +250,14 @@ private boolean descendRecursively(Term t0, Term t1, return true; } + + /** + * Checks if the given {@link NameAbstractionTable} is not null. If it is null, a new + * {@link NameAbstractionTable} is created and returned. + * + * @param nat the {@link NameAbstractionTable} to check + * @return the given {@code nat} if it is not null, a new {@link NameAbstractionTable} otherwise + */ private static NameAbstractionTable checkNat(NameAbstractionTable nat) { if (nat == null) { return new NameAbstractionTable(); @@ -258,4 +266,47 @@ private static NameAbstractionTable checkNat(NameAbstractionTable nat) { } // end of equals modulo renaming logic + /* -------- Helper methods for hashCodeModThisProperty --------- */ + + private int helper1(Term term, ImmutableList list) { + // mirrors the implementation of unifyHelp that is responsible for equality modulo renaming + int hashCode = 1; + hashCode = 17 * hashCode + term.sort().hashCode(); + hashCode = 17 * hashCode + term.arity(); + + final Operator op = term.op(); + if (op instanceof QuantifiableVariable qv) { + hashCode = 17 * hashCode + hashQuantifiableVariable(qv, list); + } else if (op instanceof Modality mod) { + hashCode = 17 * hashCode + mod.kind().hashCode(); + hashCode = 17 * hashCode + hashJavaBlock(mod); + } else if (op instanceof ProgramVariable pv) { + hashCode = 17 * hashCode + pv.hashCodeModProperty(RENAMING_SOURCE_ELEMENT_PROPERTY); + } + + return recursiveHelper(hashCode, list); + } + + private int hashQuantifiableVariable(QuantifiableVariable qv, + ImmutableList list) { + final int index = indexOf(qv, list); + // if the variable is not bound, it can make a big difference + // if the variable is bound, we just need to consider the place it is bound at + return index == -1 ? qv.hashCode() : index; + } + + private int hashJavaBlock(Modality mod) { + final JavaBlock jb = mod.program(); + if (!jb.isEmpty()) { + final JavaProgramElement jpe = jb.program(); + return jpe != null ? jpe.hashCodeModProperty(RENAMING_SOURCE_ELEMENT_PROPERTY) : 0; + } + return 0; + } + + private int recursiveHelper(int hashCode, ImmutableList list) { + return 0; + } + + /* ----- End of helper methods for hashCodeModThisProperty ----- */ } From 3d70ce012aa47ffb3bf47ad2b0d2497041b59e53 Mon Sep 17 00:00:00 2001 From: Tobias Reinhold Date: Tue, 21 May 2024 17:59:57 +0200 Subject: [PATCH 14/28] finish implementation of hashCodeModThisProperty for RenamingTermProperty --- .../logic/equality/RenamingTermProperty.java | 22 ++++++++++++++----- 1 file changed, 16 insertions(+), 6 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingTermProperty.java b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingTermProperty.java index b5c4d3e7bbb..efbfa78d973 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingTermProperty.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingTermProperty.java @@ -65,7 +65,7 @@ public boolean equalsModThisProperty(Term term1, Term term2, V... v) { @Override public int hashCodeModThisProperty(Term term) { // Labels can be completely ignored - return helper1(term, ImmutableSLList.nil()); + return helper1(term, ImmutableSLList.nil(), 1); } // equals modulo renaming logic @@ -268,9 +268,8 @@ private static NameAbstractionTable checkNat(NameAbstractionTable nat) { /* -------- Helper methods for hashCodeModThisProperty --------- */ - private int helper1(Term term, ImmutableList list) { + private int helper1(Term term, ImmutableList list, int hashCode) { // mirrors the implementation of unifyHelp that is responsible for equality modulo renaming - int hashCode = 1; hashCode = 17 * hashCode + term.sort().hashCode(); hashCode = 17 * hashCode + term.arity(); @@ -284,7 +283,7 @@ private int helper1(Term term, ImmutableList list) { hashCode = 17 * hashCode + pv.hashCodeModProperty(RENAMING_SOURCE_ELEMENT_PROPERTY); } - return recursiveHelper(hashCode, list); + return recursiveHelper(term, list, hashCode); } private int hashQuantifiableVariable(QuantifiableVariable qv, @@ -304,8 +303,19 @@ private int hashJavaBlock(Modality mod) { return 0; } - private int recursiveHelper(int hashCode, ImmutableList list) { - return 0; + private int recursiveHelper(Term term, ImmutableList list, int hashCode) { + for (int i = 0; i < term.arity(); i++) { + ImmutableList subBoundVars = list; + + for (int j = 0; j < term.varsBoundHere(i).size(); j++) { + final QuantifiableVariable qVar = term.varsBoundHere(i).get(j); + hashCode = 17 * hashCode + qVar.sort().hashCode(); + subBoundVars = subBoundVars.prepend(qVar); + } + + hashCode = helper1(term.sub(i), subBoundVars, hashCode); + } + return hashCode; } /* ----- End of helper methods for hashCodeModThisProperty ----- */ From 9bda17afd4240d3b5e67489bc664d74eca019d85 Mon Sep 17 00:00:00 2001 From: Tobias Reinhold Date: Wed, 22 May 2024 18:49:10 +0200 Subject: [PATCH 15/28] add doc to RenamingTermProperty --- .../logic/equality/RenamingTermProperty.java | 100 ++++++++++++++++-- 1 file changed, 89 insertions(+), 11 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingTermProperty.java b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingTermProperty.java index efbfa78d973..0931009a9b8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingTermProperty.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingTermProperty.java @@ -65,7 +65,7 @@ public boolean equalsModThisProperty(Term term1, Term term2, V... v) { @Override public int hashCodeModThisProperty(Term term) { // Labels can be completely ignored - return helper1(term, ImmutableSLList.nil(), 1); + return hashTermHelper(term, ImmutableSLList.nil(), 1); } // equals modulo renaming logic @@ -166,6 +166,15 @@ private boolean unifyHelp(Term t0, Term t1, ImmutableList return descendRecursively(t0, t1, ownBoundVars, cmpBoundVars, nat); } + /** + * Handles the case where the first term is a quantifiable variable. + * + * @param t0 the first term + * @param t1 the second term + * @param ownBoundVars variables bound above the current position in {@code t0} + * @param cmpBoundVars variables bound above the current position in {@code t1} + * @return true iff the quantifiable variables are equal modulo renaming + */ private boolean handleQuantifiableVariable(Term t0, Term t1, ImmutableList ownBoundVars, ImmutableList cmpBoundVars) { @@ -180,6 +189,16 @@ && compareBoundVariables((QuantifiableVariable) t0.op(), */ private static final NameAbstractionTable FAILED = new NameAbstractionTable(); + /** + * Checks whether the given {@link JavaBlock}s are equal modulo renaming and returns the updated + * {@link NameAbstractionTable} or {@link #FAILED} if the {@link JavaBlock}s are not equal. + * + * @param jb0 the first {@link JavaBlock} to compare + * @param jb1 the second {@link JavaBlock} to compare + * @param nat the {@link NameAbstractionTable} used for the comparison + * @return the updated {@link NameAbstractionTable} if the {@link JavaBlock}s are equal modulo + * renaming or {@link #FAILED} if they are not + */ private static NameAbstractionTable handleJava(JavaBlock jb0, JavaBlock jb1, NameAbstractionTable nat) { if (!jb0.isEmpty() || !jb1.isEmpty()) { @@ -217,6 +236,17 @@ public static boolean javaBlocksNotEqualModRenaming(JavaBlock jb1, JavaBlock jb2 return true; } + /** + * Recursively descends into the subterms of the given terms and checks if they are equal modulo + * renaming. + * + * @param t0 the first term + * @param t1 the second term + * @param ownBoundVars variables bound above the current position in {@code t0} + * @param cmpBoundVars variables bound above the current position in {@code t1} + * @param nat the {@link NameAbstractionTable} used for the comparison + * @return true iff the subterms are equal modulo renaming + */ private boolean descendRecursively(Term t0, Term t1, ImmutableList ownBoundVars, ImmutableList cmpBoundVars, NameAbstractionTable nat) { @@ -266,16 +296,30 @@ private static NameAbstractionTable checkNat(NameAbstractionTable nat) { } // end of equals modulo renaming logic + /* -------- Helper methods for hashCodeModThisProperty --------- */ - private int helper1(Term term, ImmutableList list, int hashCode) { + /** + * Helps to compute the hash code of a term modulo bound renaming. + *

+ * This method takes care of the top level of the term and calls the recursive helper method + * {@link #recursiveHelper(Term, ImmutableList, int)} to take care of the subterms. + * + * @param term the term to compute the hash code for + * @param nameAbstractionList the list of bound variables that is used to abstract from the + * variable names + * @param hashCode the accumulated hash code (should be 1 for the first call) + * @return the hash code + */ + private int hashTermHelper(Term term, ImmutableList nameAbstractionList, + int hashCode) { // mirrors the implementation of unifyHelp that is responsible for equality modulo renaming hashCode = 17 * hashCode + term.sort().hashCode(); hashCode = 17 * hashCode + term.arity(); final Operator op = term.op(); if (op instanceof QuantifiableVariable qv) { - hashCode = 17 * hashCode + hashQuantifiableVariable(qv, list); + hashCode = 17 * hashCode + hashQuantifiableVariable(qv, nameAbstractionList); } else if (op instanceof Modality mod) { hashCode = 17 * hashCode + mod.kind().hashCode(); hashCode = 17 * hashCode + hashJavaBlock(mod); @@ -283,29 +327,63 @@ private int helper1(Term term, ImmutableList list, int has hashCode = 17 * hashCode + pv.hashCodeModProperty(RENAMING_SOURCE_ELEMENT_PROPERTY); } - return recursiveHelper(term, list, hashCode); + return recursiveHelper(term, nameAbstractionList, hashCode); } + /** + * Computes the hash code of a quantifiable variable modulo bound renaming. + *

+ * If the variable is bound, the hash code is computed based on the index of the variable in the + * list of bound variables. + * If the variable is not bound, the hash code is computed based on the variable itself. + * + * @param qv the {@link QuantifiableVariable} to compute the hash code for + * @param nameAbstractionList the list of bound variables that is used to abstract from the + * variable names + * @return the hash code + */ private int hashQuantifiableVariable(QuantifiableVariable qv, - ImmutableList list) { - final int index = indexOf(qv, list); - // if the variable is not bound, it can make a big difference - // if the variable is bound, we just need to consider the place it is bound at + ImmutableList nameAbstractionList) { + final int index = indexOf(qv, nameAbstractionList); + // if the variable is bound, we just need to consider the place it is bound at and abstract + // from the name return index == -1 ? qv.hashCode() : index; } + /** + * Computes the hash code of a Java block modulo bound renaming. + *

+ * The hash code is computed based on the hash code of the program element of the Java block. + * + * @param mod the {@link Modality} to compute the hash code for + * @return the hash code + */ private int hashJavaBlock(Modality mod) { final JavaBlock jb = mod.program(); if (!jb.isEmpty()) { final JavaProgramElement jpe = jb.program(); return jpe != null ? jpe.hashCodeModProperty(RENAMING_SOURCE_ELEMENT_PROPERTY) : 0; } + // if the Java block is empty, we do not add anything to the hash code return 0; } - private int recursiveHelper(Term term, ImmutableList list, int hashCode) { + /** + * Recursively computes the hash code of a term modulo bound renaming. + *

+ * This method iterates over the subterms of the given term and calls + * {@link #hashTermHelper(Term, ImmutableList, int)} for each subterm. + * + * @param term the term to compute the hash code for + * @param nameAbstractionList the list of bound variables that is used to abstract from the + * variable names + * @param hashCode the accumulated hash code + * @return the hash code + */ + private int recursiveHelper(Term term, ImmutableList nameAbstractionList, + int hashCode) { for (int i = 0; i < term.arity(); i++) { - ImmutableList subBoundVars = list; + ImmutableList subBoundVars = nameAbstractionList; for (int j = 0; j < term.varsBoundHere(i).size(); j++) { final QuantifiableVariable qVar = term.varsBoundHere(i).get(j); @@ -313,7 +391,7 @@ private int recursiveHelper(Term term, ImmutableList list, subBoundVars = subBoundVars.prepend(qVar); } - hashCode = helper1(term.sub(i), subBoundVars, hashCode); + hashCode = hashTermHelper(term.sub(i), subBoundVars, hashCode); } return hashCode; } From 672b6b70977f1f7b7eadbae33d767bd481bd1f29 Mon Sep 17 00:00:00 2001 From: Tobias Reinhold Date: Thu, 13 Jun 2024 15:57:58 +0200 Subject: [PATCH 16/28] move LinkedHashMapWrapper --- .../de/uka/ilkd/key/{logic => }/util/LinkedHashMapWrapper.java | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) rename key.core/src/main/java/de/uka/ilkd/key/{logic => }/util/LinkedHashMapWrapper.java (99%) diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/util/LinkedHashMapWrapper.java b/key.core/src/main/java/de/uka/ilkd/key/util/LinkedHashMapWrapper.java similarity index 99% rename from key.core/src/main/java/de/uka/ilkd/key/logic/util/LinkedHashMapWrapper.java rename to key.core/src/main/java/de/uka/ilkd/key/util/LinkedHashMapWrapper.java index 77825d3aef3..6d2cfd6a18a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/util/LinkedHashMapWrapper.java +++ b/key.core/src/main/java/de/uka/ilkd/key/util/LinkedHashMapWrapper.java @@ -1,14 +1,13 @@ /* This file is part of KeY - https://key-project.org * KeY is licensed under the GNU General Public License Version 2 * SPDX-License-Identifier: GPL-2.0-only */ -package de.uka.ilkd.key.logic.util; +package de.uka.ilkd.key.util; import java.util.Iterator; import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.equality.EqualsModProperty; import de.uka.ilkd.key.logic.equality.Property; -import de.uka.ilkd.key.util.LinkedHashMap; import org.key_project.util.collection.Pair; From e4a563eaeb105ebda70bedabdba88f1ab8398b51 Mon Sep 17 00:00:00 2001 From: Tobias Reinhold Date: Thu, 13 Jun 2024 15:58:21 +0200 Subject: [PATCH 17/28] start tests for LinkedHashMapWrapper --- .../key/util/TestLinkedHashMapWrapper.java | 75 +++++++++++++++++++ 1 file changed, 75 insertions(+) create mode 100644 key.core/src/test/java/de/uka/ilkd/key/util/TestLinkedHashMapWrapper.java diff --git a/key.core/src/test/java/de/uka/ilkd/key/util/TestLinkedHashMapWrapper.java b/key.core/src/test/java/de/uka/ilkd/key/util/TestLinkedHashMapWrapper.java new file mode 100644 index 00000000000..a7590247179 --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/util/TestLinkedHashMapWrapper.java @@ -0,0 +1,75 @@ +package de.uka.ilkd.key.util; + + +import de.uka.ilkd.key.java.Comment; +import de.uka.ilkd.key.java.NameAbstractionTable; +import de.uka.ilkd.key.java.ProgramElement; +import de.uka.ilkd.key.java.expression.literal.StringLiteral; +import de.uka.ilkd.key.logic.*; +import de.uka.ilkd.key.logic.label.*; +import de.uka.ilkd.key.logic.op.*; +import de.uka.ilkd.key.rule.TacletForTests; +import de.uka.ilkd.key.util.HelperClassForTests; + +import org.key_project.util.collection.ImmutableArray; + +import org.junit.jupiter.api.BeforeAll; +import org.junit.jupiter.api.BeforeEach; +import org.junit.jupiter.api.Test; + +import java.util.Arrays; + +import static de.uka.ilkd.key.logic.equality.IrrelevantTermLabelsProperty.IRRELEVANT_TERM_LABELS_PROPERTY; +import static de.uka.ilkd.key.logic.equality.ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY; +import static de.uka.ilkd.key.logic.equality.RenamingSourceElementProperty.RENAMING_SOURCE_ELEMENT_PROPERTY; +import static de.uka.ilkd.key.logic.equality.RenamingTermProperty.RENAMING_TERM_PROPERTY; +import static de.uka.ilkd.key.logic.equality.TermLabelsProperty.TERM_LABELS_PROPERTY; +import static org.junit.jupiter.api.Assertions.*; + +public class TestLinkedHashMapWrapper { + private TermBuilder tb; + + private TermFactory tf; + + final private TermLabel relevantLabel1 = ParameterlessTermLabel.UNDEFINED_VALUE_LABEL; + final private TermLabel relevantLabel2 = ParameterlessTermLabel.SHORTCUT_EVALUATION_LABEL; + private static TermLabel irrelevantLabel = null; + final private static OriginTermLabelFactory factory = new OriginTermLabelFactory(); + + @BeforeAll + public static void setIrrelevantLabel() { + try { + irrelevantLabel = factory.parseInstance(Arrays.stream(new String[] { + "User_Interaction @ node 0 (Test Test)", "[]" }).toList(), + HelperClassForTests.createServices()); + } catch (TermLabelException e) { + fail(e); + } + } + + @BeforeEach + public void setUp() { + tb = TacletForTests.services().getTermBuilder(); + tf = TacletForTests.services().getTermFactory(); + } + + @Test + public void testRenamingProperty() { + + } + + @Test + public void testTermLabelsProperty() { + Term t1 = tb.tt(); + } + + @Test + public void testIrrelevantTermLabelsProperty() { + + } + + @Test + public void testProofIrrelevancyProperty() { + + } +} From c25051653f81585dac74a49dfaa58461452d3e9f Mon Sep 17 00:00:00 2001 From: Tobias Reinhold Date: Mon, 17 Jun 2024 13:43:44 +0200 Subject: [PATCH 18/28] write more tests for LinkedHashMapWrapper (WIP) --- .../key/util/TestLinkedHashMapWrapper.java | 106 +++++++++++++++--- 1 file changed, 92 insertions(+), 14 deletions(-) diff --git a/key.core/src/test/java/de/uka/ilkd/key/util/TestLinkedHashMapWrapper.java b/key.core/src/test/java/de/uka/ilkd/key/util/TestLinkedHashMapWrapper.java index a7590247179..6cbff536800 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/util/TestLinkedHashMapWrapper.java +++ b/key.core/src/test/java/de/uka/ilkd/key/util/TestLinkedHashMapWrapper.java @@ -1,15 +1,16 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.util; -import de.uka.ilkd.key.java.Comment; -import de.uka.ilkd.key.java.NameAbstractionTable; -import de.uka.ilkd.key.java.ProgramElement; -import de.uka.ilkd.key.java.expression.literal.StringLiteral; +import java.util.Arrays; + +import de.uka.ilkd.key.java.SourceElement; import de.uka.ilkd.key.logic.*; import de.uka.ilkd.key.logic.label.*; import de.uka.ilkd.key.logic.op.*; import de.uka.ilkd.key.rule.TacletForTests; -import de.uka.ilkd.key.util.HelperClassForTests; import org.key_project.util.collection.ImmutableArray; @@ -17,8 +18,6 @@ import org.junit.jupiter.api.BeforeEach; import org.junit.jupiter.api.Test; -import java.util.Arrays; - import static de.uka.ilkd.key.logic.equality.IrrelevantTermLabelsProperty.IRRELEVANT_TERM_LABELS_PROPERTY; import static de.uka.ilkd.key.logic.equality.ProofIrrelevancyProperty.PROOF_IRRELEVANCY_PROPERTY; import static de.uka.ilkd.key.logic.equality.RenamingSourceElementProperty.RENAMING_SOURCE_ELEMENT_PROPERTY; @@ -40,8 +39,8 @@ public class TestLinkedHashMapWrapper { public static void setIrrelevantLabel() { try { irrelevantLabel = factory.parseInstance(Arrays.stream(new String[] { - "User_Interaction @ node 0 (Test Test)", "[]" }).toList(), - HelperClassForTests.createServices()); + "User_Interaction @ node 0 (Test Test)", "[]" }).toList(), + HelperClassForTests.createServices()); } catch (TermLabelException e) { fail(e); } @@ -54,22 +53,101 @@ public void setUp() { } @Test - public void testRenamingProperty() { + public void testGeneralMethods() { + // exact property does not matter for these tests + LinkedHashMapWrapper wrappedMap = + new LinkedHashMapWrapper<>(TERM_LABELS_PROPERTY); + assertTrue(wrappedMap.isEmpty()); + assertEquals(0, wrappedMap.size()); + Term t1 = tb.tt(); + Term t2 = tb.ff(); + + // add mapping t1 -> 1 + wrappedMap.put(t1, 1); + assertEquals(1, wrappedMap.size()); + assertFalse(wrappedMap.isEmpty()); + assertTrue(wrappedMap.containsKey(t1)); + assertEquals(1, wrappedMap.get(t1)); + assertTrue(wrappedMap.containsValue(1)); + assertFalse(wrappedMap.containsValue(2)); + + // add mapping t2 -> 2 + wrappedMap.put(t2, 2); + assertEquals(2, wrappedMap.size()); + assertFalse(wrappedMap.isEmpty()); + assertTrue(wrappedMap.containsKey(t2)); + assertEquals(2, wrappedMap.get(t2)); + assertTrue(wrappedMap.containsValue(2)); + assertFalse(wrappedMap.containsValue(3)); + + // remove mapping t1 -> 1 + int t1Val = wrappedMap.remove(t1); + assertEquals(1, wrappedMap.size()); + assertFalse(wrappedMap.containsKey(t1)); + assertEquals(1, t1Val); + assertFalse(wrappedMap.containsValue(1)); + + // remove mapping t2 -> 2 + int t2Val = wrappedMap.remove(t2); + assertEquals(0, wrappedMap.size()); + assertTrue(wrappedMap.isEmpty()); + assertFalse(wrappedMap.containsKey(t2)); + assertEquals(2, t2Val); + assertFalse(wrappedMap.containsValue(2)); } @Test - public void testTermLabelsProperty() { - Term t1 = tb.tt(); + public void testRenamingSourceElementProperty() { + LinkedHashMapWrapper renamingSourceElementMap = + new LinkedHashMapWrapper<>(RENAMING_SOURCE_ELEMENT_PROPERTY); + LinkedHashMap basicMap = new LinkedHashMap<>(); + + } @Test - public void testIrrelevantTermLabelsProperty() { - + public void testTermLabelProperties() { + LinkedHashMap basicMap = new LinkedHashMap<>(); + LinkedHashMapWrapper termLabelsMap = + new LinkedHashMapWrapper<>(TERM_LABELS_PROPERTY); + LinkedHashMapWrapper irrelevantTermLabelsMap = + new LinkedHashMapWrapper<>(IRRELEVANT_TERM_LABELS_PROPERTY); + + + Term noLabelTerm = tb.tt(); + ImmutableArray labels = new ImmutableArray<>(irrelevantLabel); + Term irrelevantLabelTerm = tb.label(noLabelTerm, labels); + labels = new ImmutableArray<>(relevantLabel1); + Term relevantLabelTerm = tb.label(noLabelTerm, labels); } @Test public void testProofIrrelevancyProperty() { + LinkedHashMapWrapper ProofIrrelevancyMap = + new LinkedHashMapWrapper<>(PROOF_IRRELEVANCY_PROPERTY); + + } + + @Test + public void testRenamingTermProperty() { + LinkedHashMapWrapper renamingTermMap = + new LinkedHashMapWrapper<>(RENAMING_TERM_PROPERTY); + + } + + @Test + public void testConstructors() { + + } + + @Test + public void testPutAll() { + + } + + @Test + public void testSpecialCases() { } } From cf76f0bcb48fd1ac902c738dbbc1b700b80a5295 Mon Sep 17 00:00:00 2001 From: Tobias Reinhold Date: Mon, 17 Jun 2024 15:41:32 +0200 Subject: [PATCH 19/28] fix bug where equals() of ElementWrapper did not function properly --- .../main/java/de/uka/ilkd/key/util/LinkedHashMapWrapper.java | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/LinkedHashMapWrapper.java b/key.core/src/main/java/de/uka/ilkd/key/util/LinkedHashMapWrapper.java index 6d2cfd6a18a..801628acfe0 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/util/LinkedHashMapWrapper.java +++ b/key.core/src/main/java/de/uka/ilkd/key/util/LinkedHashMapWrapper.java @@ -272,7 +272,10 @@ public ElementWrapper(K key, Property property) { @Override public boolean equals(Object obj) { - return key.equalsModProperty(obj, property); + if (obj instanceof ElementWrapper other) { + return key.equalsModProperty(other.key, property); + } + return false; } @Override From 25c2d0222cd230c982cda9fdb9a1c5632dfe6d12 Mon Sep 17 00:00:00 2001 From: Tobias Reinhold Date: Tue, 18 Jun 2024 11:11:53 +0200 Subject: [PATCH 20/28] write more tests (WIP) --- .../key/util/TestLinkedHashMapWrapper.java | 71 ++++++++++++++----- 1 file changed, 55 insertions(+), 16 deletions(-) diff --git a/key.core/src/test/java/de/uka/ilkd/key/util/TestLinkedHashMapWrapper.java b/key.core/src/test/java/de/uka/ilkd/key/util/TestLinkedHashMapWrapper.java index 6cbff536800..7778dd906fc 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/util/TestLinkedHashMapWrapper.java +++ b/key.core/src/test/java/de/uka/ilkd/key/util/TestLinkedHashMapWrapper.java @@ -97,15 +97,6 @@ public void testGeneralMethods() { assertFalse(wrappedMap.containsValue(2)); } - @Test - public void testRenamingSourceElementProperty() { - LinkedHashMapWrapper renamingSourceElementMap = - new LinkedHashMapWrapper<>(RENAMING_SOURCE_ELEMENT_PROPERTY); - LinkedHashMap basicMap = new LinkedHashMap<>(); - - - } - @Test public void testTermLabelProperties() { LinkedHashMap basicMap = new LinkedHashMap<>(); @@ -114,12 +105,50 @@ public void testTermLabelProperties() { LinkedHashMapWrapper irrelevantTermLabelsMap = new LinkedHashMapWrapper<>(IRRELEVANT_TERM_LABELS_PROPERTY); + Term noLabelTT = tb.tt(); + Term noLabelFF = tb.ff(); + + Term irrelevantLabelTT = tb.label(noLabelTT, irrelevantLabel); + Term irrelevantLabelFF = tb.label(noLabelFF, irrelevantLabel); + Term relevantLabelTT = tb.label(noLabelTT, relevantLabel1); + Term relevantLabelFF = tb.label(noLabelFF, relevantLabel2); + + // add mappings without labels to all maps + basicMap.put(noLabelTT, 1); + basicMap.put(noLabelFF, 2); + assertEquals(2, basicMap.size()); + + termLabelsMap.put(noLabelTT, 1); + termLabelsMap.put(noLabelFF, 2); + assertEquals(2, termLabelsMap.size()); + + irrelevantTermLabelsMap.put(noLabelTT, 1); + irrelevantTermLabelsMap.put(noLabelFF, 2); + assertEquals(2, irrelevantTermLabelsMap.size()); + + // add mappings with irrelevant labels to all maps + assertNull(basicMap.put(irrelevantLabelTT, 3), "Nothing should be returned as basicMap should not contain the key"); + assertEquals(3, basicMap.size()); + + assertEquals(1, termLabelsMap.put(irrelevantLabelTT, 3), "Old value should be returned as termLabelsMap should already contain the key"); + assertEquals(2, termLabelsMap.size(), "Size should not increase as the key is already in the map"); + assertEquals(3, termLabelsMap.get(noLabelTT), "Checking key without label should return new value"); + + assertEquals(1, irrelevantTermLabelsMap.put(irrelevantLabelTT, 3), "Old value should be returned as irrelevantTermLabelsMap should already contain the key"); + assertEquals(2, irrelevantTermLabelsMap.size(), "Size should not increase as the key is already in the map"); + assertEquals(3, irrelevantTermLabelsMap.get(irrelevantLabelTT), "Checking key without label should return new value"); + + // add mappings with relevant labels to all maps + + assertNull(basicMap.put(relevantLabelTT, 4), "Nothing should be returned as basicMap should not contain the key"); + assertEquals(4, basicMap.size()); + + assertEquals(3, termLabelsMap.put(relevantLabelTT, 4), "Value 3 should be returned as termLabelsMap was previously updated with irrelevantLabelTT"); + assertEquals(3, termLabelsMap.size(), "Size should not increase as the key is already in the map"); + assertEquals(4, termLabelsMap.get(noLabelTT), "Checking key without label should return new value"); + assertEquals(4, termLabelsMap.get(irrelevantLabelTT), "Checking key with irrelevant label should return new value"); + - Term noLabelTerm = tb.tt(); - ImmutableArray labels = new ImmutableArray<>(irrelevantLabel); - Term irrelevantLabelTerm = tb.label(noLabelTerm, labels); - labels = new ImmutableArray<>(relevantLabel1); - Term relevantLabelTerm = tb.label(noLabelTerm, labels); } @Test @@ -137,13 +166,23 @@ public void testRenamingTermProperty() { } @Test - public void testConstructors() { + public void testRenamingSourceElementProperty() { + LinkedHashMapWrapper renamingSourceElementMap = + new LinkedHashMapWrapper<>(RENAMING_SOURCE_ELEMENT_PROPERTY); + LinkedHashMap basicMap = new LinkedHashMap<>(); + } @Test - public void testPutAll() { + public void testConstructors() { + LinkedHashMapWrapper wrappedMap = + new LinkedHashMapWrapper<>(tb.tt(), 1, TERM_LABELS_PROPERTY); + assertFalse(wrappedMap.isEmpty()); + assertEquals(1, wrappedMap.size()); + assertTrue(wrappedMap.containsKey(tb.tt())); + // putAll is also tested with these constructor calls } @Test From e8b44eb703602d2da33512c519f3326a9a1b563a Mon Sep 17 00:00:00 2001 From: Tobias Date: Tue, 18 Jun 2024 12:55:51 +0200 Subject: [PATCH 21/28] write more tests for LinkedHashMapWrapper (still WIP) --- .../key/util/TestLinkedHashMapWrapper.java | 98 +++++++++++++------ 1 file changed, 70 insertions(+), 28 deletions(-) diff --git a/key.core/src/test/java/de/uka/ilkd/key/util/TestLinkedHashMapWrapper.java b/key.core/src/test/java/de/uka/ilkd/key/util/TestLinkedHashMapWrapper.java index 7778dd906fc..daf818a8719 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/util/TestLinkedHashMapWrapper.java +++ b/key.core/src/test/java/de/uka/ilkd/key/util/TestLinkedHashMapWrapper.java @@ -6,12 +6,16 @@ import java.util.Arrays; +import de.uka.ilkd.key.java.ProgramElement; import de.uka.ilkd.key.java.SourceElement; import de.uka.ilkd.key.logic.*; import de.uka.ilkd.key.logic.label.*; import de.uka.ilkd.key.logic.op.*; +import de.uka.ilkd.key.logic.sort.SortImpl; import de.uka.ilkd.key.rule.TacletForTests; +import org.key_project.logic.Name; +import org.key_project.logic.sort.Sort; import org.key_project.util.collection.ImmutableArray; import org.junit.jupiter.api.BeforeAll; @@ -25,7 +29,8 @@ import static de.uka.ilkd.key.logic.equality.TermLabelsProperty.TERM_LABELS_PROPERTY; import static org.junit.jupiter.api.Assertions.*; -public class TestLinkedHashMapWrapper { +public class +TestLinkedHashMapWrapper { private TermBuilder tb; private TermFactory tf; @@ -115,40 +120,41 @@ public void testTermLabelProperties() { // add mappings without labels to all maps basicMap.put(noLabelTT, 1); - basicMap.put(noLabelFF, 2); - assertEquals(2, basicMap.size()); + assertEquals(1, basicMap.size()); termLabelsMap.put(noLabelTT, 1); - termLabelsMap.put(noLabelFF, 2); - assertEquals(2, termLabelsMap.size()); + assertEquals(1, termLabelsMap.size()); irrelevantTermLabelsMap.put(noLabelTT, 1); - irrelevantTermLabelsMap.put(noLabelFF, 2); - assertEquals(2, irrelevantTermLabelsMap.size()); + assertEquals(1, irrelevantTermLabelsMap.size()); // add mappings with irrelevant labels to all maps - assertNull(basicMap.put(irrelevantLabelTT, 3), "Nothing should be returned as basicMap should not contain the key"); - assertEquals(3, basicMap.size()); + assertNull(basicMap.put(irrelevantLabelTT, 2), "Nothing should be returned as basicMap should not contain the key"); + assertEquals(2, basicMap.size()); - assertEquals(1, termLabelsMap.put(irrelevantLabelTT, 3), "Old value should be returned as termLabelsMap should already contain the key"); - assertEquals(2, termLabelsMap.size(), "Size should not increase as the key is already in the map"); - assertEquals(3, termLabelsMap.get(noLabelTT), "Checking key without label should return new value"); + assertEquals(1, termLabelsMap.put(irrelevantLabelTT, 2), "Old value should be returned as termLabelsMap should already contain the key"); + assertEquals(1, termLabelsMap.size(), "Size should not increase as the key is already in the map"); + assertEquals(2, termLabelsMap.get(noLabelTT), "Checking key without label should return new value"); - assertEquals(1, irrelevantTermLabelsMap.put(irrelevantLabelTT, 3), "Old value should be returned as irrelevantTermLabelsMap should already contain the key"); - assertEquals(2, irrelevantTermLabelsMap.size(), "Size should not increase as the key is already in the map"); - assertEquals(3, irrelevantTermLabelsMap.get(irrelevantLabelTT), "Checking key without label should return new value"); + assertEquals(1, irrelevantTermLabelsMap.put(irrelevantLabelTT, 2), "Old value should be returned as irrelevantTermLabelsMap should already contain the key"); + assertEquals(1, irrelevantTermLabelsMap.size(), "Size should not increase as the key is already in the map"); + assertEquals(2, irrelevantTermLabelsMap.get(irrelevantLabelTT), "Checking key without label should return new value"); // add mappings with relevant labels to all maps - assertNull(basicMap.put(relevantLabelTT, 4), "Nothing should be returned as basicMap should not contain the key"); - assertEquals(4, basicMap.size()); - - assertEquals(3, termLabelsMap.put(relevantLabelTT, 4), "Value 3 should be returned as termLabelsMap was previously updated with irrelevantLabelTT"); - assertEquals(3, termLabelsMap.size(), "Size should not increase as the key is already in the map"); - assertEquals(4, termLabelsMap.get(noLabelTT), "Checking key without label should return new value"); - assertEquals(4, termLabelsMap.get(irrelevantLabelTT), "Checking key with irrelevant label should return new value"); + assertNull(basicMap.put(relevantLabelTT, 3), "Nothing should be returned as basicMap should not contain the key"); + assertEquals(3, basicMap.size()); + assertEquals(2, termLabelsMap.put(relevantLabelTT, 3), "Value 3 should be returned as termLabelsMap was previously updated with irrelevantLabelTT"); + assertEquals(1, termLabelsMap.size(), "Size should not increase as the key is already in the map"); + assertEquals(3, termLabelsMap.get(noLabelTT), "Checking key without label should return new value"); + assertEquals(3, termLabelsMap.get(irrelevantLabelTT), "Checking key with irrelevant label should return new value"); + assertNull(irrelevantTermLabelsMap.put(relevantLabelTT, 3), "Nothing should be returned as irrelevantTermLabelsMap should not contain the key"); + assertEquals(2, irrelevantTermLabelsMap.size(), "Size should increase as the key is not in the map"); + assertEquals(2, irrelevantTermLabelsMap.get(irrelevantLabelTT), "Checking key with irrelevant label should return old value"); + assertEquals(2, irrelevantTermLabelsMap.get(noLabelTT), "Checking key without label should return old value"); + assertEquals(3, irrelevantTermLabelsMap.get(relevantLabelTT), "Checking key with relevant label should return new value"); } @Test @@ -162,15 +168,55 @@ public void testProofIrrelevancyProperty() { public void testRenamingTermProperty() { LinkedHashMapWrapper renamingTermMap = new LinkedHashMapWrapper<>(RENAMING_TERM_PROPERTY); - + final Sort sort = new SortImpl(new Name("sort")); + final LogicVariable x = new LogicVariable(new Name("x"), sort); + final LogicVariable y = new LogicVariable(new Name("y"), sort); + Term t1 = tb.all(x, tb.and(tf.createTerm(x), tf.createTerm(x))); + Term t2 = tb.all(y, tb.and(tf.createTerm(y), tf.createTerm(y))); + Term t3 = tb.all(y, tb.and(tf.createTerm(y), tf.createTerm(x))); + + // adding \forall x. x && x + assertEquals(0, renamingTermMap.size(), "Map should be empty"); + renamingTermMap.put(t1, 1); + assertEquals(1, renamingTermMap.size(), "Map should contain one element"); + + // adding \forall y. y && y + assertEquals(1, renamingTermMap.put(t2, 2), "Old value should be returned"); + assertEquals(1, renamingTermMap.size(), "Map should still contain one element"); + assertTrue(renamingTermMap.containsKey(t1), "As renaming is ignored, t1 should be in the map"); + assertTrue(renamingTermMap.containsKey(t2), "As renaming is ignored, t2 should be in the map"); + + // adding \forall y. y && x + assertNull(renamingTermMap.put(t3, 3), "Nothing should be returned as the key is not in the map"); + assertEquals(2, renamingTermMap.size(), "Map should contain two elements"); + assertEquals(2, renamingTermMap.get(t1), "Value for t1 should be 2"); + assertEquals(2, renamingTermMap.get(t2), "Value for t2 should be 2"); + assertEquals(3, renamingTermMap.get(t3), "Value for t3 should be 3"); } @Test public void testRenamingSourceElementProperty() { LinkedHashMapWrapper renamingSourceElementMap = new LinkedHashMapWrapper<>(RENAMING_SOURCE_ELEMENT_PROPERTY); - LinkedHashMap basicMap = new LinkedHashMap<>(); + ProgramElement match1 = TacletForTests.parsePrg("{ int i; int j; /*Test*/ }"); + ProgramElement match2 = TacletForTests.parsePrg("{ int i; /*Another test*/ int k; }"); + ProgramElement match3 = TacletForTests.parsePrg("{ int i = 3; int k; }"); + + // adding { int i; int j; /*Test*/ } + assertNull(renamingSourceElementMap.put(match1, 1)); + assertEquals(1, renamingSourceElementMap.size(), "Map should contain one element"); + + // adding { int i = 3; int k; } + assertNull(renamingSourceElementMap.put(match3, 2), "Nothing should be returned as the key is not in the map"); + assertEquals(2, renamingSourceElementMap.size(), "Map should contain two elements"); + + // adding { int i; /*Another test*/ int k; } + assertEquals(1, renamingSourceElementMap.put(match2, 3), "Old value should be returned"); + assertEquals(2, renamingSourceElementMap.size(), "Map should still contain two elements"); + assertEquals(3, renamingSourceElementMap.get(match1), "Value for match1 should be new value 3"); + assertEquals(3, renamingSourceElementMap.get(match3), "Value for match3 should be 3"); + assertEquals(2, renamingSourceElementMap.get(match2), "Value for match2 should be 2"); } @@ -183,10 +229,6 @@ public void testConstructors() { assertTrue(wrappedMap.containsKey(tb.tt())); // putAll is also tested with these constructor calls - } - - @Test - public void testSpecialCases() { } } From cecf12fc05224943b4d3bfdfbbadbcfd9c59c597 Mon Sep 17 00:00:00 2001 From: Tobias Reinhold Date: Tue, 18 Jun 2024 20:07:19 +0200 Subject: [PATCH 22/28] finish tests for LinkedHashMapWrapper --- .../key/util/TestLinkedHashMapWrapper.java | 191 ++++++++++++------ 1 file changed, 127 insertions(+), 64 deletions(-) diff --git a/key.core/src/test/java/de/uka/ilkd/key/util/TestLinkedHashMapWrapper.java b/key.core/src/test/java/de/uka/ilkd/key/util/TestLinkedHashMapWrapper.java index daf818a8719..4a100c900ea 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/util/TestLinkedHashMapWrapper.java +++ b/key.core/src/test/java/de/uka/ilkd/key/util/TestLinkedHashMapWrapper.java @@ -8,6 +8,7 @@ import de.uka.ilkd.key.java.ProgramElement; import de.uka.ilkd.key.java.SourceElement; +import de.uka.ilkd.key.ldt.JavaDLTheory; import de.uka.ilkd.key.logic.*; import de.uka.ilkd.key.logic.label.*; import de.uka.ilkd.key.logic.op.*; @@ -29,14 +30,12 @@ import static de.uka.ilkd.key.logic.equality.TermLabelsProperty.TERM_LABELS_PROPERTY; import static org.junit.jupiter.api.Assertions.*; -public class -TestLinkedHashMapWrapper { +public class TestLinkedHashMapWrapper { private TermBuilder tb; private TermFactory tf; - final private TermLabel relevantLabel1 = ParameterlessTermLabel.UNDEFINED_VALUE_LABEL; - final private TermLabel relevantLabel2 = ParameterlessTermLabel.SHORTCUT_EVALUATION_LABEL; + final private TermLabel relevantLabel = ParameterlessTermLabel.UNDEFINED_VALUE_LABEL; private static TermLabel irrelevantLabel = null; final private static OriginTermLabelFactory factory = new OriginTermLabelFactory(); @@ -111,12 +110,9 @@ public void testTermLabelProperties() { new LinkedHashMapWrapper<>(IRRELEVANT_TERM_LABELS_PROPERTY); Term noLabelTT = tb.tt(); - Term noLabelFF = tb.ff(); Term irrelevantLabelTT = tb.label(noLabelTT, irrelevantLabel); - Term irrelevantLabelFF = tb.label(noLabelFF, irrelevantLabel); - Term relevantLabelTT = tb.label(noLabelTT, relevantLabel1); - Term relevantLabelFF = tb.label(noLabelFF, relevantLabel2); + Term relevantLabelTT = tb.label(noLabelTT, relevantLabel); // add mappings without labels to all maps basicMap.put(noLabelTT, 1); @@ -129,75 +125,91 @@ public void testTermLabelProperties() { assertEquals(1, irrelevantTermLabelsMap.size()); // add mappings with irrelevant labels to all maps - assertNull(basicMap.put(irrelevantLabelTT, 2), "Nothing should be returned as basicMap should not contain the key"); + assertNull(basicMap.put(irrelevantLabelTT, 2), + "Nothing should be returned as basicMap should not contain the key"); assertEquals(2, basicMap.size()); - assertEquals(1, termLabelsMap.put(irrelevantLabelTT, 2), "Old value should be returned as termLabelsMap should already contain the key"); - assertEquals(1, termLabelsMap.size(), "Size should not increase as the key is already in the map"); - assertEquals(2, termLabelsMap.get(noLabelTT), "Checking key without label should return new value"); + assertEquals(1, termLabelsMap.put(irrelevantLabelTT, 2), + "Old value should be returned as termLabelsMap should already contain the key"); + assertEquals(1, termLabelsMap.size(), + "Size should not increase as the key is already in the map"); + assertEquals(2, termLabelsMap.get(noLabelTT), + "Checking key without label should return new value"); - assertEquals(1, irrelevantTermLabelsMap.put(irrelevantLabelTT, 2), "Old value should be returned as irrelevantTermLabelsMap should already contain the key"); - assertEquals(1, irrelevantTermLabelsMap.size(), "Size should not increase as the key is already in the map"); - assertEquals(2, irrelevantTermLabelsMap.get(irrelevantLabelTT), "Checking key without label should return new value"); + assertEquals(1, irrelevantTermLabelsMap.put(irrelevantLabelTT, 2), + "Old value should be returned as irrelevantTermLabelsMap should already contain the key"); + assertEquals(1, irrelevantTermLabelsMap.size(), + "Size should not increase as the key is already in the map"); + assertEquals(2, irrelevantTermLabelsMap.get(irrelevantLabelTT), + "Checking key without label should return new value"); // add mappings with relevant labels to all maps - assertNull(basicMap.put(relevantLabelTT, 3), "Nothing should be returned as basicMap should not contain the key"); + assertNull(basicMap.put(relevantLabelTT, 3), + "Nothing should be returned as basicMap should not contain the key"); assertEquals(3, basicMap.size()); - assertEquals(2, termLabelsMap.put(relevantLabelTT, 3), "Value 3 should be returned as termLabelsMap was previously updated with irrelevantLabelTT"); - assertEquals(1, termLabelsMap.size(), "Size should not increase as the key is already in the map"); - assertEquals(3, termLabelsMap.get(noLabelTT), "Checking key without label should return new value"); - assertEquals(3, termLabelsMap.get(irrelevantLabelTT), "Checking key with irrelevant label should return new value"); - - assertNull(irrelevantTermLabelsMap.put(relevantLabelTT, 3), "Nothing should be returned as irrelevantTermLabelsMap should not contain the key"); - assertEquals(2, irrelevantTermLabelsMap.size(), "Size should increase as the key is not in the map"); - assertEquals(2, irrelevantTermLabelsMap.get(irrelevantLabelTT), "Checking key with irrelevant label should return old value"); - assertEquals(2, irrelevantTermLabelsMap.get(noLabelTT), "Checking key without label should return old value"); - assertEquals(3, irrelevantTermLabelsMap.get(relevantLabelTT), "Checking key with relevant label should return new value"); + assertEquals(2, termLabelsMap.put(relevantLabelTT, 3), + "Value 3 should be returned as termLabelsMap was previously updated with irrelevantLabelTT"); + assertEquals(1, termLabelsMap.size(), + "Size should not increase as the key is already in the map"); + assertEquals(3, termLabelsMap.get(noLabelTT), + "Checking key without label should return new value"); + assertEquals(3, termLabelsMap.get(irrelevantLabelTT), + "Checking key with irrelevant label should return new value"); + + assertNull(irrelevantTermLabelsMap.put(relevantLabelTT, 3), + "Nothing should be returned as irrelevantTermLabelsMap should not contain the key"); + assertEquals(2, irrelevantTermLabelsMap.size(), + "Size should increase as the key is not in the map"); + assertEquals(2, irrelevantTermLabelsMap.get(irrelevantLabelTT), + "Checking key with irrelevant label should return old value"); + assertEquals(2, irrelevantTermLabelsMap.get(noLabelTT), + "Checking key without label should return old value"); + assertEquals(3, irrelevantTermLabelsMap.get(relevantLabelTT), + "Checking key with relevant label should return new value"); } @Test public void testProofIrrelevancyProperty() { - LinkedHashMapWrapper ProofIrrelevancyMap = + LinkedHashMapWrapper proofIrrelevancyMap = new LinkedHashMapWrapper<>(PROOF_IRRELEVANCY_PROPERTY); - } - - @Test - public void testRenamingTermProperty() { - LinkedHashMapWrapper renamingTermMap = - new LinkedHashMapWrapper<>(RENAMING_TERM_PROPERTY); - final Sort sort = new SortImpl(new Name("sort")); - final LogicVariable x = new LogicVariable(new Name("x"), sort); - final LogicVariable y = new LogicVariable(new Name("y"), sort); - Term t1 = tb.all(x, tb.and(tf.createTerm(x), tf.createTerm(x))); - Term t2 = tb.all(y, tb.and(tf.createTerm(y), tf.createTerm(y))); - Term t3 = tb.all(y, tb.and(tf.createTerm(y), tf.createTerm(x))); - - // adding \forall x. x && x - assertEquals(0, renamingTermMap.size(), "Map should be empty"); - renamingTermMap.put(t1, 1); - assertEquals(1, renamingTermMap.size(), "Map should contain one element"); - - // adding \forall y. y && y - assertEquals(1, renamingTermMap.put(t2, 2), "Old value should be returned"); - assertEquals(1, renamingTermMap.size(), "Map should still contain one element"); - assertTrue(renamingTermMap.containsKey(t1), "As renaming is ignored, t1 should be in the map"); - assertTrue(renamingTermMap.containsKey(t2), "As renaming is ignored, t2 should be in the map"); + Term noLabelTT = tb.tt(); - // adding \forall y. y && x - assertNull(renamingTermMap.put(t3, 3), "Nothing should be returned as the key is not in the map"); - assertEquals(2, renamingTermMap.size(), "Map should contain two elements"); - assertEquals(2, renamingTermMap.get(t1), "Value for t1 should be 2"); - assertEquals(2, renamingTermMap.get(t2), "Value for t2 should be 2"); - assertEquals(3, renamingTermMap.get(t3), "Value for t3 should be 3"); + Term irrelevantLabelTT = tb.label(noLabelTT, irrelevantLabel); + Term relevantLabelTT = tb.label(noLabelTT, relevantLabel); + + // add mapping without label + assertNull(proofIrrelevancyMap.put(noLabelTT, 1), + "Nothing should be returned as proofIrrelevancyMap should not contain the key"); + assertEquals(1, proofIrrelevancyMap.size()); + + // add mapping with irrelevant label + assertEquals(1, proofIrrelevancyMap.put(irrelevantLabelTT, 2), + "Old value should be returned as irrelevantTermLabelsMap should already contain the key"); + assertEquals(1, proofIrrelevancyMap.size(), + "Size should not increase as the key is already in the map"); + assertEquals(2, proofIrrelevancyMap.get(irrelevantLabelTT), + "Checking key without label should return new value"); + + // add mapping with relevant label + assertNull(proofIrrelevancyMap.put(relevantLabelTT, 3), + "Nothing should be returned as irrelevantTermLabelsMap should not contain the key"); + assertEquals(2, proofIrrelevancyMap.size(), + "Size should increase as the key is not in the map"); + assertEquals(2, proofIrrelevancyMap.get(irrelevantLabelTT), + "Checking key with irrelevant label should return old value"); + assertEquals(2, proofIrrelevancyMap.get(noLabelTT), + "Checking key without label should return old value"); + assertEquals(3, proofIrrelevancyMap.get(relevantLabelTT), + "Checking key with relevant label should return new value");; } @Test public void testRenamingSourceElementProperty() { LinkedHashMapWrapper renamingSourceElementMap = - new LinkedHashMapWrapper<>(RENAMING_SOURCE_ELEMENT_PROPERTY); + new LinkedHashMapWrapper<>(RENAMING_SOURCE_ELEMENT_PROPERTY); ProgramElement match1 = TacletForTests.parsePrg("{ int i; int j; /*Test*/ }"); ProgramElement match2 = TacletForTests.parsePrg("{ int i; /*Another test*/ int k; }"); @@ -208,27 +220,78 @@ public void testRenamingSourceElementProperty() { assertEquals(1, renamingSourceElementMap.size(), "Map should contain one element"); // adding { int i = 3; int k; } - assertNull(renamingSourceElementMap.put(match3, 2), "Nothing should be returned as the key is not in the map"); + assertNull(renamingSourceElementMap.put(match3, 2), + "Nothing should be returned as the key is not in the map"); assertEquals(2, renamingSourceElementMap.size(), "Map should contain two elements"); // adding { int i; /*Another test*/ int k; } assertEquals(1, renamingSourceElementMap.put(match2, 3), "Old value should be returned"); assertEquals(2, renamingSourceElementMap.size(), "Map should still contain two elements"); - assertEquals(3, renamingSourceElementMap.get(match1), "Value for match1 should be new value 3"); + assertEquals(3, renamingSourceElementMap.get(match1), + "Value for match1 should be new value 3"); assertEquals(3, renamingSourceElementMap.get(match3), "Value for match3 should be 3"); assertEquals(2, renamingSourceElementMap.get(match2), "Value for match2 should be 2"); } + @Test + public void testRenamingTermProperty() { + LinkedHashMapWrapper renamingTermMap = + new LinkedHashMapWrapper<>(RENAMING_TERM_PROPERTY); + final Sort sort = new SortImpl(new Name("sort")); + final LogicVariable x = new LogicVariable(new Name("x"), sort); + final LogicVariable y = new LogicVariable(new Name("y"), sort); + final Term tx = tf.createTerm(x); + final Term ty = tf.createTerm(y); + final JFunction f = new JFunction(new Name("f"), JavaDLTheory.FORMULA, sort, sort); + final Term t1 = tb.all(x, tf.createTerm(f, tx, tx)); + final Term t2 = tb.all(y, tf.createTerm(f, ty, ty)); + final Term t3 = tb.all(y, tf.createTerm(f, ty, tx)); + + // adding \forall x. x && x + assertEquals(0, renamingTermMap.size(), "Map should be empty"); + renamingTermMap.put(t1, 1); + assertEquals(1, renamingTermMap.size(), "Map should contain one element"); + + // adding \forall y. y && y + assertEquals(1, renamingTermMap.put(t2, 2), "Old value should be returned"); + assertEquals(1, renamingTermMap.size(), "Map should still contain one element"); + assertTrue(renamingTermMap.containsKey(t1), + "As renaming is ignored, t1 should be in the map"); + assertTrue(renamingTermMap.containsKey(t2), + "As renaming is ignored, t2 should be in the map"); + + // adding \forall y. y && x + assertNull(renamingTermMap.put(t3, 3), + "Nothing should be returned as the key is not in the map"); + assertEquals(2, renamingTermMap.size(), "Map should contain two elements"); + assertEquals(2, renamingTermMap.get(t1), "Value for t1 should be 2"); + assertEquals(2, renamingTermMap.get(t2), "Value for t2 should be 2"); + assertEquals(3, renamingTermMap.get(t3), "Value for t3 should be 3"); + } + @Test public void testConstructors() { LinkedHashMapWrapper wrappedMap = - new LinkedHashMapWrapper<>(tb.tt(), 1, TERM_LABELS_PROPERTY); - assertFalse(wrappedMap.isEmpty()); - assertEquals(1, wrappedMap.size()); - assertTrue(wrappedMap.containsKey(tb.tt())); + new LinkedHashMapWrapper<>(tb.tt(), 1, TERM_LABELS_PROPERTY); + assertFalse(wrappedMap.isEmpty(), "Map should not be empty (0)"); + assertEquals(1, wrappedMap.size(), "Map should contain one element"); + assertTrue(wrappedMap.containsKey(tb.tt()), "Map should contain key tt"); // putAll is also tested with these constructor calls - + LinkedHashMapWrapper wrappedMap2 = + new LinkedHashMapWrapper<>(new Term[] { tb.tt(), tb.ff() }, new Integer[] { 1, 2 }, + TERM_LABELS_PROPERTY); + assertFalse(wrappedMap2.isEmpty(), "Map should not be empty (1)"); + assertEquals(2, wrappedMap2.size(), "Map should contain two elements"); + + LinkedHashMapWrapper wrappedMap3 = + new LinkedHashMapWrapper<>(new ImmutableArray<>(tb.tt(), tb.ff(), tb.tt()), + new ImmutableArray<>(1, 2, 3), + TERM_LABELS_PROPERTY); + assertFalse(wrappedMap3.isEmpty(), "Map should not be empty (2)"); + assertEquals(2, wrappedMap3.size(), "Map should contain two elements, as tt is repeated"); + assertFalse(wrappedMap3.containsValue(1), + "Map should not contain value 1 as it should be overwritten by 3"); } } From 7da937c00756fc7cb7b0974f73a0ff19924573f2 Mon Sep 17 00:00:00 2001 From: Tobias Reinhold Date: Tue, 18 Jun 2024 21:16:13 +0200 Subject: [PATCH 23/28] write long comment about hashCodeModThisProperty for SourceElements --- .../logic/equality/RenamingSourceElementProperty.java | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingSourceElementProperty.java b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingSourceElementProperty.java index e71c94759cd..9cffceaf51b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingSourceElementProperty.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingSourceElementProperty.java @@ -97,10 +97,17 @@ public boolean equalsModThisProperty(SourceElement se1, SourceElement se2, V return next1 == null && next2 == null; } + // TODO: hashCodeModThisProperty currently does not take a NameAbstractionTable as an argument. + // This is because the current implementation of hashCodeModThisProperty is not parameterized + // with a vararg. Variables occurring in multiple formulas and JavaBlocks are considered in + // isolation as a newly created NameAbstractionTable that does not contain entries from previous + // JavaBlocks is used. This could possibly lead to more collisions but if this is a concern, the + // method can be changed to also take a generic vararg. That way, the NameAbstractionTable can + // be passed to the method and hash codes can take previous usage of variables into account. @Override public int hashCodeModThisProperty(SourceElement sourceElement) { /* - * Currently, the best approach seems to walk through the sourceElement with a + * Currently, the best approach seems to be to walk through the SourceElement with a * JavaASTTreeWalker and sum up hash codes. */ JavaASTTreeWalker tw = new JavaASTTreeWalker(sourceElement); @@ -111,7 +118,7 @@ public int hashCodeModThisProperty(SourceElement sourceElement) { int hashCode = 1; while (next != null) { - // Handle special cases so that hashCodeModThisProperty fits equalsModThisProperty + // Handle special cases so that hashCodeModThisProperty follows equalsModThisProperty if (next instanceof LabeledStatement ls) { hashCode = 31 * hashCode + ls.getChildCount(); absMap.add(ls); From 6dd07b88ab7de7eaa6e98526ac931874d10c7298 Mon Sep 17 00:00:00 2001 From: Tobias Date: Fri, 21 Jun 2024 10:02:27 +0200 Subject: [PATCH 24/28] add nullable annotations in LinkedHashMapWrapper --- .../de/uka/ilkd/key/util/LinkedHashMapWrapper.java | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/LinkedHashMapWrapper.java b/key.core/src/main/java/de/uka/ilkd/key/util/LinkedHashMapWrapper.java index 801628acfe0..5608b0847a6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/util/LinkedHashMapWrapper.java +++ b/key.core/src/main/java/de/uka/ilkd/key/util/LinkedHashMapWrapper.java @@ -11,6 +11,9 @@ import org.key_project.util.collection.Pair; +import org.jspecify.annotations.Nullable; + + /** * This class is a wrapper for {@link LinkedHashMap} where the keys are elements that implement * {@link EqualsModProperty}. @@ -27,7 +30,7 @@ public class LinkedHashMapWrapper, V> { /** * The wrapped {@link LinkedHashMap}. */ - private final LinkedHashMap, V> map; + private final LinkedHashMap, @Nullable V> map; /** * The {@link Property} that is used for equality checks and hash codes. @@ -127,7 +130,7 @@ public boolean containsKey(K key) { * @param key the key whose associated value is to be returned * @return the value to which the specified key is mapped */ - public V get(K key) { + public @Nullable V get(K key) { return map.get(wrapKey(key)); } @@ -142,7 +145,7 @@ public V get(K key) { * @return the previous value associated with {@code key}, or {@code null} if there was no * mapping for {@code key} */ - public V put(K key, V value) { + public @Nullable V put(K key, @Nullable V value) { return map.put(wrapKey(key), value); } @@ -195,7 +198,7 @@ public void putAll(Iterable keys, Iterable vals) { * @return the previous value associated with {@code key}, or {@code null} if there was no * mapping for {@code key} */ - public V remove(K key) { + public @Nullable V remove(K key) { return map.remove(wrapKey(key)); } @@ -309,7 +312,7 @@ private static class PairIterator, V> /** * The last key-value pair that was returned by {@link #next()}. */ - private ElementWrapper last = null; + private @Nullable ElementWrapper last = null; /** * Creates a new iterator over the key-value pairs in the {@link LinkedHashMapWrapper}. From 93271194cc40e2d97cd5aac462f7a2d4be9c5f18 Mon Sep 17 00:00:00 2001 From: Tobias Reinhold Date: Fri, 21 Jun 2024 10:44:09 +0200 Subject: [PATCH 25/28] add to test case for LinkedHashMapWrapper --- .../uka/ilkd/key/util/TestLinkedHashMapWrapper.java | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/key.core/src/test/java/de/uka/ilkd/key/util/TestLinkedHashMapWrapper.java b/key.core/src/test/java/de/uka/ilkd/key/util/TestLinkedHashMapWrapper.java index 4a100c900ea..6b9a0246d82 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/util/TestLinkedHashMapWrapper.java +++ b/key.core/src/test/java/de/uka/ilkd/key/util/TestLinkedHashMapWrapper.java @@ -5,6 +5,7 @@ import java.util.Arrays; +import java.util.Iterator; import de.uka.ilkd.key.java.ProgramElement; import de.uka.ilkd.key.java.SourceElement; @@ -18,6 +19,7 @@ import org.key_project.logic.Name; import org.key_project.logic.sort.Sort; import org.key_project.util.collection.ImmutableArray; +import org.key_project.util.collection.Pair; import org.junit.jupiter.api.BeforeAll; import org.junit.jupiter.api.BeforeEach; @@ -293,5 +295,16 @@ public void testConstructors() { assertEquals(2, wrappedMap3.size(), "Map should contain two elements, as tt is repeated"); assertFalse(wrappedMap3.containsValue(1), "Map should not contain value 1 as it should be overwritten by 3"); + + Iterator> it = wrappedMap3.iterator(); + it.forEachRemaining(pair -> { + if (pair.first.equals(tb.tt())) { + assertEquals(3, pair.second, "Value for tt should be 3"); + } else if (pair.first.equals(tb.ff())) { + assertEquals(2, pair.second, "Value for ff should be 2"); + } else { + fail("Unexpected key in map"); + } + }); } } From 74af6420c875c4d03e8a3cfa606644fd9664856b Mon Sep 17 00:00:00 2001 From: Tobias Reinhold Date: Fri, 21 Jun 2024 10:57:24 +0200 Subject: [PATCH 26/28] add test for iterator of LinkedHashMapWrapper --- .../uka/ilkd/key/util/TestLinkedHashMapWrapper.java | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/key.core/src/test/java/de/uka/ilkd/key/util/TestLinkedHashMapWrapper.java b/key.core/src/test/java/de/uka/ilkd/key/util/TestLinkedHashMapWrapper.java index 6b9a0246d82..5a7c583100f 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/util/TestLinkedHashMapWrapper.java +++ b/key.core/src/test/java/de/uka/ilkd/key/util/TestLinkedHashMapWrapper.java @@ -296,8 +296,8 @@ public void testConstructors() { assertFalse(wrappedMap3.containsValue(1), "Map should not contain value 1 as it should be overwritten by 3"); - Iterator> it = wrappedMap3.iterator(); - it.forEachRemaining(pair -> { + Iterator> it1 = wrappedMap3.iterator(); + it1.forEachRemaining(pair -> { if (pair.first.equals(tb.tt())) { assertEquals(3, pair.second, "Value for tt should be 3"); } else if (pair.first.equals(tb.ff())) { @@ -306,5 +306,12 @@ public void testConstructors() { fail("Unexpected key in map"); } }); + + Iterator> it2 = wrappedMap2.iterator(); + assertTrue(it2.hasNext(), "Iterator should have next element"); + it2.next(); + assertTrue(it2.hasNext(), "Iterator should have next element"); + it2.next(); + assertFalse(it2.hasNext(), "Iterator should not have next element"); } } From 98f8008d061a274c02da2b159e6ae17b1e96f820 Mon Sep 17 00:00:00 2001 From: Tobias Reinhold Date: Fri, 21 Jun 2024 11:43:30 +0200 Subject: [PATCH 27/28] fix test for LinkedHashMapWrapper --- .../java/de/uka/ilkd/key/util/TestLinkedHashMapWrapper.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/key.core/src/test/java/de/uka/ilkd/key/util/TestLinkedHashMapWrapper.java b/key.core/src/test/java/de/uka/ilkd/key/util/TestLinkedHashMapWrapper.java index 5a7c583100f..3624a8e2fdc 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/util/TestLinkedHashMapWrapper.java +++ b/key.core/src/test/java/de/uka/ilkd/key/util/TestLinkedHashMapWrapper.java @@ -231,8 +231,8 @@ public void testRenamingSourceElementProperty() { assertEquals(2, renamingSourceElementMap.size(), "Map should still contain two elements"); assertEquals(3, renamingSourceElementMap.get(match1), "Value for match1 should be new value 3"); - assertEquals(3, renamingSourceElementMap.get(match3), "Value for match3 should be 3"); - assertEquals(2, renamingSourceElementMap.get(match2), "Value for match2 should be 2"); + assertEquals(2, renamingSourceElementMap.get(match3), "Value for match3 should be 2"); + assertEquals(3, renamingSourceElementMap.get(match2), "Value for match2 should be 3"); } From c04215260bdfd5781ea7ea64793d53104d5b3be6 Mon Sep 17 00:00:00 2001 From: Tobias Reinhold Date: Thu, 27 Jun 2024 16:05:37 +0200 Subject: [PATCH 28/28] use general navigation structure for hashCodeModThisProperty in RenamingSourceElementProperty --- .../equality/RenamingSourceElementProperty.java | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingSourceElementProperty.java b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingSourceElementProperty.java index 3958134f94a..530297d1c41 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingSourceElementProperty.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/RenamingSourceElementProperty.java @@ -113,16 +113,18 @@ public boolean equalsModThisProperty(SourceElement se1, SourceElement se2, V public int hashCodeModThisProperty(SourceElement sourceElement) { /* * Currently, the best approach seems to be to walk through the SourceElement with a - * JavaASTTreeWalker and sum up hash codes. + * SyntaxElementCursor and sum up hash codes. */ - JavaASTTreeWalker tw = new JavaASTTreeWalker(sourceElement); - SourceElement next = tw.currentNode(); NameAbstractionMap absMap = new NameAbstractionMap(); int hashCode = 1; + SyntaxElementCursor c = sourceElement.getCursor(); + SyntaxElement next; - while (next != null) { + do { + // First node can never be null as cursor is initialized with 'this' + next = c.getCurrentNode(); // Handle special cases so that hashCodeModThisProperty follows equalsModThisProperty if (next instanceof LabeledStatement ls) { hashCode = 31 * hashCode + ls.getChildCount(); @@ -134,17 +136,15 @@ public int hashCodeModThisProperty(SourceElement sourceElement) { + vs.getDimensions(); absMap.add(vs); } else if (next instanceof ProgramVariable || next instanceof ProgramElementName) { - hashCode = 31 * hashCode + absMap.getAbstractName(next); + hashCode = 31 * hashCode + absMap.getAbstractName((SourceElement) next); } else if (next instanceof JavaNonTerminalProgramElement jnte) { hashCode = 31 * hashCode + jnte.getChildCount(); } else { // In the standard case, we just use the default hashCode implementation hashCode = 31 * hashCode + next.hashCode(); } - // walk to the next nodes in the tree - next = tw.nextNode(); - } + } while (c.goToNext()); return hashCode; }