From bb0dcf05884da1ec98b41d0ca296ccf688273d4e Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Fri, 10 Jul 2026 18:49:30 +0200 Subject: [PATCH] Fix broken proof tree after information flow auto pilot (#3713) The Full Information Flow Auto Pilot broke the proof tree view with 'IllegalStateException: abstract tree node without parent: Proof Tree'. Root cause: when the macro creates its auxiliary side proof, the StartSideProofMacro handling in macroFinished re-froze the interface via initiateAutoMode(sideProof), which also broadcasts autoModeStarted for the side proof (with no matching autoModeStopped ever following). The ProofTreeView listener trusted any event source and overwrote its modifiedSubtrees bookkeeping with the side proof's goal nodes. At the final autoModeStopped, those foreign (by then disposed) nodes were fed into the tree model of the displayed proof, where the lazily created parent branch node for the foreign root has no parent and a disposed proof has no root() anymore, defeating the existing root check. The fix prevents the poisoning at both ends: - macroFinished only freezes the interface (stopInterface + setInteractive) instead of broadcasting a spurious autoModeStarted for the side proof, - ProofTreeView ignores auto mode events for proofs it does not display and skips foreign nodes when refreshing modified subtrees. GUIAbstractTreeNode.getParent() keeps failing fast on parent-less nodes so that bookkeeping bugs of this kind surface; the previously unexplained root-instance escape ('why can there be another instance of the root node?') is now documented - it stems from stale instances after cache invalidation and from exactly this kind of foreign-node walk. A regression test pins the fail-fast contract. Created with AI tooling --- .../ilkd/key/gui/prooftree/ProofTreeView.java | 12 +++- .../AbstractMediatorUserInterfaceControl.java | 5 +- .../DisposedProofTreeUpdateTest.java | 65 +++++++++++++++++++ 3 files changed, 79 insertions(+), 3 deletions(-) create mode 100644 key.ui/src/test/java/de/uka/ilkd/key/gui/prooftree/DisposedProofTreeUpdateTest.java diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java index 8b34cc79656..9852ef0119d 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java @@ -1066,6 +1066,13 @@ public synchronized void autoModeStarted(ProofEvent e) { LOGGER.debug("delegateModel is null"); return; } + if (e.getSource() != proof) { + // Auto mode on a proof this view does not display, e.g. an auxiliary side proof + // of the information-flow macros (see #3713). Overwriting modifiedSubtrees with + // the foreign proof's goals would feed its nodes into the displayed proof's tree + // model in autoModeStopped. + return; + } // save goals on which the prover may work modifiedSubtrees = e.getSource().openGoals().map(Goal::node); @@ -1088,7 +1095,10 @@ public synchronized void autoModeStopped(ProofEvent e) { setProof(mediator.getSelectedProof()); if (modifiedSubtrees != null) { for (final Node n : modifiedSubtrees) { - if (proof.openGoals().filter(g -> g.node() == n).isEmpty()) { + // skip nodes of other proofs: the displayed proof may have changed since the + // subtrees were recorded in autoModeStarted (see #3713) + if (n.proof() == proof + && proof.openGoals().filter(g -> g.node() == n).isEmpty()) { delegateModel.updateTree(n); } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/ui/AbstractMediatorUserInterfaceControl.java b/key.ui/src/main/java/de/uka/ilkd/key/ui/AbstractMediatorUserInterfaceControl.java index bf2a9af1aeb..2d371f51113 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/ui/AbstractMediatorUserInterfaceControl.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/ui/AbstractMediatorUserInterfaceControl.java @@ -172,9 +172,10 @@ public void proofDisposed(ProofDisposedEvent e) { }); // stop interface again, because it is activated by the proof // change through startProver; the ProofMacroWorker will activate - // it again at the right time + // it again at the right time. ThreadUtilities.invokeAndWait(() -> { - getMediator().initiateAutoMode(info.getProof(), true, false); + getMediator().stopInterface(true); + getMediator().setInteractive(false); }); } } diff --git a/key.ui/src/test/java/de/uka/ilkd/key/gui/prooftree/DisposedProofTreeUpdateTest.java b/key.ui/src/test/java/de/uka/ilkd/key/gui/prooftree/DisposedProofTreeUpdateTest.java new file mode 100644 index 00000000000..cb4129b5b57 --- /dev/null +++ b/key.ui/src/test/java/de/uka/ilkd/key/gui/prooftree/DisposedProofTreeUpdateTest.java @@ -0,0 +1,65 @@ +/* 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.gui.prooftree; + +import java.nio.file.Path; +import java.util.Objects; +import javax.swing.tree.TreeNode; + +import de.uka.ilkd.key.control.DefaultUserInterfaceControl; +import de.uka.ilkd.key.control.KeYEnvironment; +import de.uka.ilkd.key.proof.Node; +import de.uka.ilkd.key.proof.Proof; + +import org.key_project.util.helper.FindResources; + +import org.junit.jupiter.api.Test; + +import static org.junit.jupiter.api.Assertions.assertThrows; + +/** + * Documents the fail-fast contract of the proof tree model for the constellation behind issue + * #3713: nodes of a foreign (here: already disposed) proof must never be fed into another proof's + * {@link GUIProofTreeModel}. The information-flow auto pilot's side proof used to leak into + * {@code ProofTreeView.modifiedSubtrees} this way; the actual fix prevents the leak in + * {@code ProofTreeView} and {@code AbstractMediatorUserInterfaceControl#macroFinished}. The model + * itself deliberately keeps failing fast when the invariant is violated, so that bookkeeping bugs + * of this kind surface instead of being rendered silently. + */ +public class DisposedProofTreeUpdateTest { + private static final Path exampleDir = + Objects.requireNonNull(FindResources.getExampleDirectory()); + private static final String EXAMPLE_PROOF = + "standard_key/BookExamples/10UsingKeY/andCommutes.proof"; + + @Test + void updatingWithNodeOfForeignDisposedProofFailsFast() throws Exception { + KeYEnvironment env = + KeYEnvironment.load(exampleDir.resolve(EXAMPLE_PROOF)); + Proof displayed = env.getLoadedProof(); + KeYEnvironment env2 = + KeYEnvironment.load(exampleDir.resolve(EXAMPLE_PROOF)); + Proof foreign = env2.getLoadedProof(); + + GUIProofTreeModel model = new GUIProofTreeModel(displayed); + forceExpand((TreeNode) model.getRoot()); + + // keep a node of the foreign proof (Node keeps its proof reference), then dispose it + Node foreignRoot = foreign.root(); + foreign.dispose(); + + assertThrows(IllegalStateException.class, () -> model.updateTree(foreignRoot), + "walking a foreign disposed proof's node must fail fast"); + + env.dispose(); + env2.dispose(); + } + + private static void forceExpand(TreeNode node) { + int count = node.getChildCount(); + for (int i = 0; i < count; i++) { + forceExpand(node.getChildAt(i)); + } + } +}