Print real condition in if labels (KeYProject#3222)

This PR modifies the labels in the proof tree to show the actual
condition of ifs instead of the boolean variable introduced by the
unfold taclet. With this change, the branch labels in the proof tree are
much more useful.
|previous|now|
:-------------------------:|:-------------------------:

![Sum_pre](https://github.com/KeYProject/key/assets/12560461/2b274dbe-579f-4b39-82b3-29dc4e989381)
|
![Sum_post](https://github.com/KeYProject/key/assets/12560461/8179dc72-76e1-49e3-8c03-57001ef36aa2)

![Contains_pre](https://github.com/KeYProject/key/assets/12560461/01157e0d-b360-40b7-a519-55cd31be36ad)
|
![Contains_post](https://github.com/KeYProject/key/assets/12560461/c0d5cd54-f453-4cf4-a5d9-da323526d6a9)

Author: WolframPfeifer

key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTCollector.java

@@ -10,8 +10,8 @@
 
 /**
  * Walks through a java AST in depth-left-fist-order. You can set the type of nodes you want to
- * collect and then start the walker. The found nodes of the given type are returned as a
- * IList<JavaProgramElement>
+ * collect and then {@link #start()} the walker. The found nodes of the given type are returned as a
+ * list of {@link ProgramElement}.
  */
 public class JavaASTCollector extends JavaASTWalker {
 

key.core/src/main/java/de/uka/ilkd/key/logic/OpCollector.java

@@ -3,6 +3,7 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.logic;
 
+import java.util.Collections;
 import java.util.HashSet;
 import java.util.LinkedHashSet;
 import java.util.Set;
@@ -15,13 +16,14 @@
  */
 public class OpCollector extends DefaultVisitor {
     /** the found operators */
-    private final HashSet<Operator> ops;
+    protected final HashSet<Operator> ops;
 
     /** creates the Op collector */
     public OpCollector() {
         ops = new LinkedHashSet<>();
     }
 
+    @Override
     public void visit(Term t) {
         ops.add(t.op());
         if (t.op() instanceof ElementaryUpdate) {
@@ -34,6 +36,6 @@ public boolean contains(Operator op) {
     }
 
     public Set<Operator> ops() {
-        return ops;
+        return Collections.unmodifiableSet(ops);
     }
 }

key.core/src/main/java/de/uka/ilkd/key/logic/OpCollectorJavaBlock.java

@@ -0,0 +1,30 @@
+/* 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;
+
+import de.uka.ilkd.key.java.ProgramElement;
+import de.uka.ilkd.key.java.visitor.JavaASTCollector;
+import de.uka.ilkd.key.logic.op.LocationVariable;
+
+/**
+ * Extended {@link OpCollector} that also descends into Java blocks
+ * and collects all {@link LocationVariable} there.
+ *
+ * @author Arne Keller
+ */
+public class OpCollectorJavaBlock extends OpCollector {
+    @Override
+    public void visit(Term t) {
+        super.visit(t);
+        if (t.javaBlock() != JavaBlock.EMPTY_JAVABLOCK) {
+            var collect = new JavaASTCollector(t.javaBlock().program(), LocationVariable.class);
+            collect.start();
+            for (ProgramElement programElement : collect.getNodes()) {
+                if (programElement instanceof LocationVariable locationVariable) {
+                    ops.add(locationVariable);
+                }
+            }
+        }
+    }
+}

key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramVariable.java

@@ -64,7 +64,6 @@ protected ProgramVariable(ProgramElementName name, Sort s, KeYJavaType t,
         assert sort() != Sort.UPDATE;
     }
 
-
     protected ProgramVariable(ProgramElementName name, Sort s, KeYJavaType t,
             KeYJavaType containingType, boolean isStatic, boolean isModel, boolean isGhost) {
         this(name, s, t, containingType, isStatic, isModel, isGhost, false);
@@ -263,6 +262,5 @@ public MatchConditions match(SourceData source, MatchConditions matchCond) {
      * @param name the new name
      * @return equivalent operator with the new name
      */
-    abstract public Operator rename(Name name);
-
+    public abstract Operator rename(Name name);
 }

key.core/src/main/java/de/uka/ilkd/key/proof/NodeInfo.java

@@ -19,6 +19,7 @@
 import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.TermBuilder;
 import de.uka.ilkd.key.logic.label.TermLabelManager;
+import de.uka.ilkd.key.logic.op.LocationVariable;
 import de.uka.ilkd.key.proof.io.ProofSaver;
 import de.uka.ilkd.key.rule.AbstractAuxiliaryContractBuiltInRuleApp;
 import de.uka.ilkd.key.rule.AbstractContractRuleApp;
@@ -30,6 +31,7 @@
 import de.uka.ilkd.key.rule.TacletApp;
 import de.uka.ilkd.key.rule.inst.TermInstantiation;
 
+import org.key_project.proof.LocationVariableTracker;
 import org.key_project.util.collection.ImmutableList;
 
 import org.slf4j.Logger;
@@ -310,8 +312,6 @@ public void setBranchLabel(String s) {
         }
         RuleApp ruleApp = node.parent().getAppliedRuleApp();
         if (ruleApp instanceof TacletApp tacletApp) {
-            // XXX
-
             Pattern p = Pattern.compile("#\\w+");
             Matcher m = p.matcher(s);
             StringBuffer sb = new StringBuffer();
@@ -337,6 +337,18 @@ public void setBranchLabel(String s) {
                         val = TermLabelManager.removeIrrelevantLabels(
                             ((TermInstantiation) val).getInstantiation(),
                             node.proof().getServices());
+                    } else if (val instanceof LocationVariable locVar) {
+                        var originTracker = node.proof().lookup(LocationVariableTracker.class);
+                        if (originTracker != null) {
+                            var origin = originTracker.getCreatedBy(locVar);
+                            if (origin instanceof PosTacletApp posTacletApp) {
+                                var name = posTacletApp.taclet().displayName();
+                                if (name.equals("ifElseUnfold") || name.equals("ifUnfold")) {
+                                    val =
+                                        posTacletApp.instantiations().lookupValue(new Name("#nse"));
+                                }
+                            }
+                        }
                     }
                     res = ProofSaver.printAnything(val, node.proof().getServices());
                 }

key.core/src/main/java/org/key_project/proof/LocationVariableTracker.java

@@ -0,0 +1,72 @@
+/* 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 org.key_project.proof;
+
+import java.util.Map;
+import java.util.WeakHashMap;
+
+import de.uka.ilkd.key.logic.OpCollectorJavaBlock;
+import de.uka.ilkd.key.logic.op.LocationVariable;
+import de.uka.ilkd.key.proof.Proof;
+import de.uka.ilkd.key.proof.ProofEvent;
+import de.uka.ilkd.key.proof.RuleAppListener;
+import de.uka.ilkd.key.rule.RuleApp;
+
+/**
+ * Tracks which rule application introduced each {@link LocationVariable} in a proof.
+ * Currently only checks for {@code ifElseUnfold} rules.
+ *
+ * @author Arne Keller
+ */
+public class LocationVariableTracker implements RuleAppListener {
+    /**
+     * The "origin" of the variables. Used to indicate which
+     * {@link de.uka.ilkd.key.rule.TacletApp} created a new program variable.
+     */
+    private final Map<LocationVariable, RuleApp> createdBy = new WeakHashMap<>();
+
+    /**
+     * Register a new tracker on the provided proof.
+     *
+     * @param proof proof to track
+     */
+    public static void handleProofLoad(Proof proof) {
+        if (proof.lookup(LocationVariableTracker.class) != null) {
+            return;
+        }
+        LocationVariableTracker self = new LocationVariableTracker();
+        proof.register(self, LocationVariableTracker.class);
+        proof.addRuleAppListener(self);
+    }
+
+    /**
+     * @param locationVariable some location variable
+     * @return the rule app that created it, or null
+     */
+    public RuleApp getCreatedBy(LocationVariable locationVariable) {
+        return createdBy.get(locationVariable);
+    }
+
+    @Override
+    public void ruleApplied(ProofEvent e) {
+        var rai = e.getRuleAppInfo();
+        if (rai.getRuleApp().rule().displayName().equals("ifElseUnfold")) {
+            rai.getReplacementNodes().forEach(x -> {
+                var it = x.getNodeChanges();
+                while (it.hasNext()) {
+                    var change = it.next();
+                    var sf = change.getPos().sequentFormula();
+                    var collect = new OpCollectorJavaBlock();
+                    sf.formula().execPreOrder(collect);
+                    for (var op : collect.ops()) {
+                        if (!(op instanceof LocationVariable) || createdBy.containsKey(op)) {
+                            continue;
+                        }
+                        createdBy.put((LocationVariable) op, rai.getRuleApp());
+                    }
+                }
+            });
+        }
+    }
+}

key.ui/src/main/java/de/uka/ilkd/key/core/KeYMediator.java

@@ -53,6 +53,7 @@
 import de.uka.ilkd.key.ui.AbstractMediatorUserInterfaceControl;
 import de.uka.ilkd.key.util.ThreadUtilities;
 
+import org.key_project.proof.LocationVariableTracker;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.lookup.Lookup;
 
@@ -89,6 +90,8 @@ public class KeYMediator {
 
     /**
      * Registered proof load listeners.
+     *
+     * @see #fireProofLoaded(Proof)
      */
     private final Collection<Consumer<Proof>> proofLoadListeners = new ArrayList<>();
 
@@ -129,11 +132,13 @@ public KeYMediator(AbstractMediatorUserInterfaceControl ui) {
         keySelectionModel = new KeYSelectionModel();
 
         ui.getProofControl().addAutoModeListener(proofListener);
+
+        registerProofLoadListener(LocationVariableTracker::handleProofLoad);
     }
 
     /**
      * Register a proof load listener. Will be called whenever a new proof is loaded, but before
-     * it is replayed.
+     * it is replayed. The listener MUST be able to accept the same proof twice!
      *
      * @param listener callback
      */

key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java

@@ -476,6 +476,7 @@ public boolean selectProofObligation(InitConfig initConfig) {
     @Override
     public void registerProofAggregate(ProofAggregate pa) {
         super.registerProofAggregate(pa);
+        getMediator().fireProofLoaded(pa.getFirstProof());
         mainWindow.addProblem(pa);
         mainWindow.setStandardStatusLine();
     }