From 5066ea5f85a7afa997c3fe16fbd6f89058fd4264 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Wed, 31 Jan 2024 16:00:11 +0100 Subject: [PATCH 1/3] Fix slicing bug related to Evaluate Query --- .../key/proof/replay/AbstractProofReplayer.java | 9 +++++---- .../main/java/de/uka/ilkd/key/rule/Taclet.java | 3 ++- .../AntecSuccTacletGoalTemplate.java | 9 +++++++++ .../RewriteTacletGoalTemplate.java | 9 +++++++++ .../rule/tacletbuilder/TacletGoalTemplate.java | 17 ++++++++++++++++- 5 files changed, 41 insertions(+), 6 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java index b3dbc7ae429..37e12ba8f90 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java @@ -226,8 +226,8 @@ private TacletApp constructTacletApp(Node originalStep, Goal currGoal) { final String tacletName = originalStep.getAppliedRuleApp().rule().name().toString(); TacletApp originalTacletApp = null; - if (originalStep.getAppliedRuleApp() instanceof TacletApp) { - originalTacletApp = (TacletApp) originalStep.getAppliedRuleApp(); + if (originalStep.getAppliedRuleApp() instanceof TacletApp tacletApp) { + originalTacletApp = tacletApp; } TacletApp ourApp = null; @@ -238,7 +238,7 @@ private TacletApp constructTacletApp(Node originalStep, Goal currGoal) { if (t == null) { // find the correct taclet for (NoPosTacletApp partialApp : currGoal.indexOfTaclets() - .getPartialInstantiatedApps()) { + .allNoPosTacletApps()) { if (partialApp.equalsModProofIrrelevancy(originalTacletApp)) { ourApp = partialApp; break; @@ -249,7 +249,8 @@ private TacletApp constructTacletApp(Node originalStep, Goal currGoal) { } if (ourApp == null) { throw new IllegalStateException( - "proof replayer failed to find dynamically added taclet"); + "proof replayer failed to find dynamically added taclet at original node " + + originalStep.serialNr()); } } else { ourApp = NoPosTacletApp.createNoPosTacletApp(t); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/Taclet.java b/key.core/src/main/java/de/uka/ilkd/key/rule/Taclet.java index e2c385d8c63..ab77b87f6ec 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/Taclet.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/Taclet.java @@ -22,6 +22,7 @@ import de.uka.ilkd.key.rule.tacletbuilder.TacletGoalTemplate; import org.key_project.util.EqualsModProofIrrelevancy; +import org.key_project.util.EqualsModProofIrrelevancyUtil; import org.key_project.util.collection.DefaultImmutableSet; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableMap; @@ -505,7 +506,7 @@ public boolean equalsModProofIrrelevancy(Object o) { return false; } - if (!goalTemplates.equals(t2.goalTemplates)) { + if (!EqualsModProofIrrelevancyUtil.compareImmutableLists(goalTemplates, t2.goalTemplates)) { return false; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/AntecSuccTacletGoalTemplate.java b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/AntecSuccTacletGoalTemplate.java index 7797b5beddd..568641fc61b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/AntecSuccTacletGoalTemplate.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/AntecSuccTacletGoalTemplate.java @@ -80,6 +80,15 @@ public boolean equals(Object o) { return replacewith.equals(other.replacewith); } + @Override + public boolean equalsModProofIrrelevancy(Object obj) { + if (!super.equalsModProofIrrelevancy(obj) + || !(obj instanceof AntecSuccTacletGoalTemplate other)) { + return false; + } + return replacewith.equals(other.replacewith); + } + @Override public int hashCode() { int result = 17; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/RewriteTacletGoalTemplate.java b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/RewriteTacletGoalTemplate.java index aa61c2bc2aa..0c231e0ebf5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/RewriteTacletGoalTemplate.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/RewriteTacletGoalTemplate.java @@ -89,6 +89,15 @@ public boolean equals(Object o) { return replacewith.equals(other.replacewith); } + @Override + public boolean equalsModProofIrrelevancy(Object obj) { + if (!(obj instanceof RewriteTacletGoalTemplate other) + || !super.equalsModProofIrrelevancy(obj)) { + return false; + } + return replacewith.equalsModProofIrrelevancy(other.replacewith); + } + @Override public int hashCode() { int result = 17; diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGoalTemplate.java b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGoalTemplate.java index c68cde1b761..b4c63b06ecb 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGoalTemplate.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGoalTemplate.java @@ -9,6 +9,7 @@ import de.uka.ilkd.key.logic.op.SchemaVariable; import de.uka.ilkd.key.rule.Taclet; +import org.key_project.util.EqualsModProofIrrelevancy; import org.key_project.util.collection.DefaultImmutableSet; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; @@ -19,7 +20,7 @@ * sequents that have to be added, new rules and rule variables. The replacewith-goal is implemented * in subclasses */ -public class TacletGoalTemplate { +public class TacletGoalTemplate implements EqualsModProofIrrelevancy { /** stores sequent that is one of the new goals */ private Sequent addedSeq = Sequent.EMPTY_SEQUENT; @@ -175,4 +176,18 @@ public String toString() { } return result; } + + @Override + public boolean equalsModProofIrrelevancy(Object obj) { + if (!(obj instanceof TacletGoalTemplate)) { + return false; + } + TacletGoalTemplate other = (TacletGoalTemplate) obj; + return addedSeq.equals(other.addedSeq) && addedRules.equals(other.addedRules); + } + + @Override + public int hashCodeModProofIrrelevancy() { + return 0; + } } From 117caceb756ead304027f3941ede4921157399b6 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Fri, 15 Mar 2024 15:15:16 +0100 Subject: [PATCH 2/3] Use equalsModProofIrrelevancy where relevant --- .../de/uka/ilkd/key/logic/Semisequent.java | 17 ++++++++++++++- .../java/de/uka/ilkd/key/logic/Sequent.java | 21 ++++++++++++++++++- .../AntecSuccTacletGoalTemplate.java | 2 +- .../tacletbuilder/TacletGoalTemplate.java | 7 ++++--- 4 files changed, 41 insertions(+), 6 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/Semisequent.java b/key.core/src/main/java/de/uka/ilkd/key/logic/Semisequent.java index 0a210bd3c57..d36e45a6b2e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/Semisequent.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/Semisequent.java @@ -5,6 +5,8 @@ import java.util.Iterator; +import org.key_project.util.EqualsModProofIrrelevancy; +import org.key_project.util.EqualsModProofIrrelevancyUtil; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; @@ -15,7 +17,7 @@ * future versions it can be enhanced to do other simplifications. A sequent and so a semisequent * has to be immutable. */ -public class Semisequent implements Iterable { +public class Semisequent implements Iterable, EqualsModProofIrrelevancy { /** the empty semisequent (using singleton pattern) */ public static final Semisequent EMPTY_SEMISEQUENT = new Empty(); @@ -429,12 +431,25 @@ public boolean equals(Object o) { return seqList.equals(((Semisequent) o).seqList); } + @Override + public boolean equalsModProofIrrelevancy(Object o) { + if (!(o instanceof Semisequent)) { + return false; + } + return EqualsModProofIrrelevancyUtil.compareImmutableLists(seqList, + ((Semisequent) o).seqList); + } + @Override public int hashCode() { return seqList.hashCode(); } + @Override + public int hashCodeModProofIrrelevancy() { + return 0; + } /** @return String representation of this Semisequent */ @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/Sequent.java b/key.core/src/main/java/de/uka/ilkd/key/logic/Sequent.java index 0492f5fdb17..09f8b680611 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/Sequent.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/Sequent.java @@ -10,6 +10,7 @@ import de.uka.ilkd.key.logic.label.TermLabel; import de.uka.ilkd.key.logic.op.QuantifiableVariable; +import org.key_project.util.EqualsModProofIrrelevancy; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; @@ -22,7 +23,7 @@ * {@link Sequent#createSuccSequent} or by inserting formulas directly into * {@link Sequent#EMPTY_SEQUENT}. */ -public class Sequent implements Iterable { +public class Sequent implements Iterable, EqualsModProofIrrelevancy { public static final Sequent EMPTY_SEQUENT = NILSequent.INSTANCE; @@ -283,6 +284,24 @@ public boolean equals(Object o) { return antecedent.equals(o1.antecedent) && succedent.equals(o1.succedent); } + @Override + public boolean equalsModProofIrrelevancy(Object o) { + if (this == o) { + return true; + } + if (!(o instanceof Sequent o1)) { + return false; + } + + return antecedent.equalsModProofIrrelevancy(o1.antecedent) + && succedent.equalsModProofIrrelevancy(o1.succedent); + } + + @Override + public int hashCodeModProofIrrelevancy() { + return 0; + } + /** * Computes the position of the given sequent formula on the proof sequent, starting with one * for the very first sequent formula. diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/AntecSuccTacletGoalTemplate.java b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/AntecSuccTacletGoalTemplate.java index 568641fc61b..e321909f605 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/AntecSuccTacletGoalTemplate.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/AntecSuccTacletGoalTemplate.java @@ -86,7 +86,7 @@ public boolean equalsModProofIrrelevancy(Object obj) { || !(obj instanceof AntecSuccTacletGoalTemplate other)) { return false; } - return replacewith.equals(other.replacewith); + return replacewith.equalsModProofIrrelevancy(other.replacewith); } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGoalTemplate.java b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGoalTemplate.java index b4c63b06ecb..8785ec30cb5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGoalTemplate.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGoalTemplate.java @@ -10,6 +10,7 @@ import de.uka.ilkd.key.rule.Taclet; import org.key_project.util.EqualsModProofIrrelevancy; +import org.key_project.util.EqualsModProofIrrelevancyUtil; import org.key_project.util.collection.DefaultImmutableSet; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; @@ -179,11 +180,11 @@ public String toString() { @Override public boolean equalsModProofIrrelevancy(Object obj) { - if (!(obj instanceof TacletGoalTemplate)) { + if (!(obj instanceof TacletGoalTemplate other)) { return false; } - TacletGoalTemplate other = (TacletGoalTemplate) obj; - return addedSeq.equals(other.addedSeq) && addedRules.equals(other.addedRules); + return addedSeq.equalsModProofIrrelevancy(other.addedSeq) && EqualsModProofIrrelevancyUtil + .compareImmutableLists(addedRules, other.addedRules); } @Override From d19e2d7e4d4eb3338624c608a8c035536c6f3dee Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Thu, 21 Mar 2024 15:26:49 +0100 Subject: [PATCH 3/3] Semisequent hashCodeModProofIrrelevancy impl. --- key.core/src/main/java/de/uka/ilkd/key/logic/Semisequent.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/Semisequent.java b/key.core/src/main/java/de/uka/ilkd/key/logic/Semisequent.java index 0a5e19e9555..d3b72aa9118 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/Semisequent.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/Semisequent.java @@ -475,7 +475,7 @@ public int hashCode() { @Override public int hashCodeModProofIrrelevancy() { - return 0; + return EqualsModProofIrrelevancyUtil.hashCodeImmutableList(seqList); } /** @return String representation of this Semisequent */