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

Author: unp1

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);
                     }
                 }

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);
             });
         }
     }

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<DefaultUserInterfaceControl> env =
+            KeYEnvironment.load(exampleDir.resolve(EXAMPLE_PROOF));
+        Proof displayed = env.getLoadedProof();
+        KeYEnvironment<DefaultUserInterfaceControl> 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));
+        }
+    }
+}