From d3a3293b583993138e1d9b02a3c293cde3e70fa2 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Fri, 8 Mar 2024 11:07:53 +0100 Subject: [PATCH 1/4] Log dependency analysis failure --- .../de/uka/ilkd/key/proof/reference/ReferenceSearcher.java | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/keyext.caching/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java b/keyext.caching/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java index 14b5265c330..0a62b2e3f5a 100644 --- a/keyext.caching/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java +++ b/keyext.caching/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java @@ -18,6 +18,8 @@ import org.key_project.slicing.DependencyTracker; import org.key_project.slicing.analysis.AnalysisResults; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; /** * Utility class for proof caching. @@ -25,6 +27,8 @@ * @author Arne Keller */ public final class ReferenceSearcher { + public static final Logger LOGGER = LoggerFactory.getLogger(ReferenceSearcher.class); + private ReferenceSearcher() { } @@ -91,8 +95,9 @@ public static ClosedBy findPreviousProof(List previousProofs, Node newNod .noneMatch(x -> x.node().lookup(ClosedBy.class) != null)) { try { results = depTracker.analyze(true, false); - } catch (Exception ignored) { + } catch (Exception e) { // if the analysis for some reason fails, we simply proceed as usual + LOGGER.debug("failed to analyze target proof ", e); } } while (!nodesToCheck.isEmpty()) { From d88c5758222b5af3a3ef289dc1d13cea77c9710b Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Fri, 8 Mar 2024 11:17:01 +0100 Subject: [PATCH 2/4] Allow realizing multiple cached branches at once --- .../caching/actions/CopyReferencedProof.java | 42 ++++++++++++------- .../proof/reference/ReferenceSearcher.java | 1 + 2 files changed, 27 insertions(+), 16 deletions(-) diff --git a/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/CopyReferencedProof.java b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/CopyReferencedProof.java index cd818b55d8c..a2919918652 100644 --- a/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/CopyReferencedProof.java +++ b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/CopyReferencedProof.java @@ -4,6 +4,8 @@ package de.uka.ilkd.key.gui.plugins.caching.actions; import java.awt.event.ActionEvent; +import java.util.ArrayList; +import java.util.List; import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.IssueDialog; @@ -30,37 +32,45 @@ public final class CopyReferencedProof extends KeyAction { */ private final KeYMediator mediator; /** - * The node to copy the steps to. + * The nodes to copy the steps to. */ - private final Node node; + private final List nodes; /** * Construct a new action. * * @param mediator the mediator - * @param node the node + * @param node the node to apply the action on */ public CopyReferencedProof(KeYMediator mediator, Node node) { this.mediator = mediator; - this.node = node; + this.nodes = new ArrayList<>(); setName("Copy referenced proof steps here"); - setEnabled(node.leaf() && node.isClosed() - && node.lookup(ClosedBy.class) != null); + var iter = node.leavesIterator(); + while (iter.hasNext()) { + var goal = iter.next(); + if (goal.isClosed() && goal.lookup(ClosedBy.class) != null) { + nodes.add(goal); + } + } + setEnabled(!nodes.isEmpty()); setMenuPath("Proof Caching"); } @Override public void actionPerformed(ActionEvent e) { - ClosedBy c = node.lookup(ClosedBy.class); - Goal current = node.proof().getClosedGoal(node); - try { - mediator.stopInterface(true); - new CopyingProofReplayer(c.proof(), node.proof()).copy(c.node(), current, - c.nodesToSkip()); - mediator.startInterface(true); - } catch (Exception ex) { - LOGGER.error("failed to copy proof ", ex); - IssueDialog.showExceptionDialog(MainWindow.getInstance(), ex); + for (Node node : nodes) { + ClosedBy c = node.lookup(ClosedBy.class); + Goal current = node.proof().getClosedGoal(node); + try { + mediator.stopInterface(true); + new CopyingProofReplayer(c.proof(), node.proof()).copy(c.node(), current, + c.nodesToSkip()); + mediator.startInterface(true); + } catch (Exception ex) { + LOGGER.error("failed to copy proof ", ex); + IssueDialog.showExceptionDialog(MainWindow.getInstance(), ex); + } } } } diff --git a/keyext.caching/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java b/keyext.caching/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java index 0a62b2e3f5a..89f687c508c 100644 --- a/keyext.caching/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java +++ b/keyext.caching/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java @@ -18,6 +18,7 @@ import org.key_project.slicing.DependencyTracker; import org.key_project.slicing.analysis.AnalysisResults; + import org.slf4j.Logger; import org.slf4j.LoggerFactory; From eb3df1562de5295934a066e8c8221bfc37211cac Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Thu, 21 Mar 2024 14:24:38 +0100 Subject: [PATCH 3/4] Show cache hits in proof caching info dialog --- .../caching/actions/CloseByReference.java | 21 +++++++++++++++---- .../slicing/graph/DependencyGraph.java | 3 +++ 2 files changed, 20 insertions(+), 4 deletions(-) diff --git a/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/CloseByReference.java b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/CloseByReference.java index 7dcafc483f2..3bf96b1cb2e 100644 --- a/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/CloseByReference.java +++ b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/CloseByReference.java @@ -66,11 +66,13 @@ public void actionPerformed(ActionEvent e) { }); } List mismatches = new ArrayList<>(); + List matches = new ArrayList<>(); for (Node n : nodes) { // search other proofs for matching nodes ClosedBy c = ReferenceSearcher.findPreviousProof( mediator.getCurrentlyOpenedProofs(), n); if (c != null) { + matches.add(n.serialNr()); n.proof().closeGoal(n.proof().getOpenGoal(n)); n.register(c, ClosedBy.class); } else { @@ -80,12 +82,23 @@ public void actionPerformed(ActionEvent e) { if (!nodes.isEmpty()) { cachingExtension.updateGUIState(nodes.get(0).proof()); } - if (!mismatches.isEmpty()) { + if (!mismatches.isEmpty() || !matches.isEmpty()) { + var sb = new StringBuilder(); + if (!matches.isEmpty()) { + sb.append("Cache hit found for node(s) "); + sb.append(Arrays.toString(matches.toArray())); + } + if (!mismatches.isEmpty()) { + if (!sb.isEmpty()) { + sb.append('\n'); + } + sb.append("No matching branch found for node(s) "); + sb.append(Arrays.toString(mismatches.toArray())); + } // since e.getSource() is the popup menu, it is better to use the MainWindow // instance here as a parent - JOptionPane.showMessageDialog(MainWindow.getInstance(), - "No matching branch found for node(s) " + Arrays.toString(mismatches.toArray()), - "Proof Caching error", JOptionPane.WARNING_MESSAGE); + JOptionPane.showMessageDialog(MainWindow.getInstance(), sb.toString(), + "Proof Caching", JOptionPane.INFORMATION_MESSAGE); } } } diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java b/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java index 02f109322a2..32873c82268 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java @@ -48,6 +48,9 @@ public class DependencyGraph { */ private final Map> edgeDataReversed = new IdentityHashMap<>(); + /** + * Create a new empty dependency graph. + */ public DependencyGraph() { graph = new EquivalenceDirectedGraph(); } From 545b836e4803ee299a50bcf5dca3975d821ea2d6 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Thu, 21 Mar 2024 14:37:30 +0100 Subject: [PATCH 4/4] Allow pruning cached goals --- .../de/uka/ilkd/key/control/AbstractProofControl.java | 4 ++-- .../main/java/de/uka/ilkd/key/proof/ProofPruner.java | 10 ++++++++++ .../ilkd/key/gui/prooftree/ProofTreePopupFactory.java | 4 ++++ 3 files changed, 16 insertions(+), 2 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/control/AbstractProofControl.java b/key.core/src/main/java/de/uka/ilkd/key/control/AbstractProofControl.java index 0d3fd45622c..80d4b90337e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/control/AbstractProofControl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/control/AbstractProofControl.java @@ -253,8 +253,8 @@ public void applyInteractive(RuleApp app, Goal goal) { /** * Prunes a proof to the given node. * - * @param node - * @see {@link Proof#pruneProof(Node)} + * @param node the node to prune to + * @see Proof#pruneProof(Node) */ public void pruneTo(Node node) { node.proof().pruneProof(node); diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/ProofPruner.java b/key.core/src/main/java/de/uka/ilkd/key/proof/ProofPruner.java index 03f8f392add..13c7a0be3fe 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/ProofPruner.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/ProofPruner.java @@ -7,6 +7,7 @@ import javax.swing.*; import de.uka.ilkd.key.proof.init.InitConfig; +import de.uka.ilkd.key.proof.reference.ClosedBy; import de.uka.ilkd.key.rule.NoPosTacletApp; import de.uka.ilkd.key.rule.merge.MergePartner; import de.uka.ilkd.key.rule.merge.MergeRuleBuiltInRuleApp; @@ -37,6 +38,15 @@ class ProofPruner { */ public ImmutableList prune(final Node cuttingPoint) { + // very special case: prune of cached branch + // (simply reopen the cached branch) + var closedBy = cuttingPoint.lookup(ClosedBy.class); + if (closedBy != null) { + cuttingPoint.deregister(closedBy, ClosedBy.class); + cuttingPoint.proof().reOpenGoal(cuttingPoint.proof().getClosedGoal(cuttingPoint)); + return ImmutableList.of(cuttingPoint); + } + // there is only one leaf containing an open goal that is interesting for pruning the // subtree of node, namely the first leave that is found by a breadth // first search. diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreePopupFactory.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreePopupFactory.java index 3866cf218af..6f8da873e7a 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreePopupFactory.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreePopupFactory.java @@ -32,6 +32,7 @@ import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.delayedcut.DelayedCutListener; import de.uka.ilkd.key.proof.delayedcut.DelayedCutProcessor; +import de.uka.ilkd.key.proof.reference.ClosedBy; import de.uka.ilkd.key.prover.TaskStartedInfo; import de.uka.ilkd.key.prover.impl.DefaultTaskStartedInfo; import de.uka.ilkd.key.rule.OneStepSimplifierRuleApp; @@ -400,6 +401,9 @@ public Prune(ProofTreeContext context) { .getClosedSubtreeGoals(context.invokedNode).size() > 0))) { setEnabled(true); } + if (context.invokedNode.lookup(ClosedBy.class) != null) { + setEnabled(true); + } } }