Caching: make behaviour when reference proof is pruned configurable

key.core/src/main/java/de/uka/ilkd/key/settings/ProofCachingSettings.java

@@ -11,15 +11,21 @@
 public class ProofCachingSettings extends AbstractPropertiesSettings {
     public static final String DISPOSE_COPY = "Copy steps into new proof";
     public static final String DISPOSE_REOPEN = "Reopen proof";
+    public static final String PRUNE_COPY = "Copy steps just before prune";
+    public static final String PRUNE_REOPEN = "Reopen cached goal(s)";
 
     /**
      * Key ID for {@link #enabled}.
      */
     private static final String ENABLED_KEY = "Enabled";
     /**
-     * Key ID for {@link #enabled}.
+     * Key ID for {@link #dispose}.
      */
     private static final String DISPOSE_KEY = "Dispose";
+    /**
+     * Key ID for {@link #prune}.
+     */
+    private static final String PRUNE_KEY = "Prune";
 
 
     /**
@@ -32,6 +38,11 @@ public class ProofCachingSettings extends AbstractPropertiesSettings {
      */
     private final AbstractPropertiesSettings.PropertyEntry<String> dispose =
         createStringProperty(DISPOSE_KEY, "");
+    /**
+     * Behaviour when pruning a proof that is referenced elsewhere.
+     */
+    private final AbstractPropertiesSettings.PropertyEntry<String> prune =
+        createStringProperty(PRUNE_KEY, "");
 
     public ProofCachingSettings() {
         super("ProofCaching");
@@ -63,4 +74,23 @@ public String getDispose() {
     public void setDispose(String operation) {
         dispose.set(operation);
     }
+
+    /**
+     * Returns the current setting for behaviour when pruning into referenced branches.
+     *
+     * @return either an empty string, {@link #PRUNE_REOPEN} or {@link #PRUNE_COPY}
+     */
+    public String getPrune() {
+        return prune.get();
+    }
+
+    /**
+     * Set the operation to be done when a referenced proof is pruned.
+     * Allowed operations: {@link #PRUNE_REOPEN}, {@link #PRUNE_COPY}.
+     *
+     * @param operation the operation
+     */
+    public void setPrune(String operation) {
+        prune.set(operation);
+    }
 }

key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsPanel.java

@@ -179,6 +179,8 @@ protected JTextField addFileChooserPanel(String title, String file, String info,
     }
 
     /**
+     * Adds a new combobox to the panel.
+     *
      * @param title label of the combo box
      * @param info help text
      * @param selectionIndex which item to initially select

keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachingPruneHandler.java

@@ -4,11 +4,19 @@
 package de.uka.ilkd.key.gui.plugins.caching;
 
 import de.uka.ilkd.key.core.KeYMediator;
+import de.uka.ilkd.key.gui.IssueDialog;
+import de.uka.ilkd.key.gui.MainWindow;
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.proof.ProofTreeEvent;
 import de.uka.ilkd.key.proof.ProofTreeListener;
+import de.uka.ilkd.key.proof.io.IntermediateProofReplayer;
 import de.uka.ilkd.key.proof.reference.ClosedBy;
+import de.uka.ilkd.key.proof.replay.CopyingProofReplayer;
+import de.uka.ilkd.key.settings.ProofCachingSettings;
+
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
 
 /**
  * Handles prunes in proofs that are referenced elsewhere.
@@ -18,6 +26,8 @@
  * @author Arne Keller
  */
 public class CachingPruneHandler implements ProofTreeListener {
+    public static final Logger LOGGER = LoggerFactory.getLogger(CachingPruneHandler.class);
+
     /**
      * The KeY mediator.
      */
@@ -34,19 +44,33 @@ public CachingPruneHandler(KeYMediator mediator) {
 
     @Override
     public void proofIsBeingPruned(ProofTreeEvent e) {
+        Proof proofToBePruned = e.getSource();
         // check other proofs for any references to this proof
         for (Proof p : mediator.getCurrentlyOpenedProofs()) {
             for (Goal g : p.closedGoals()) {
                 ClosedBy c = g.node().lookup(ClosedBy.class);
-                if (c == null || c.proof() != e.getNode().proof()) {
+                if (c == null || c.proof() != proofToBePruned) {
                     continue;
                 }
                 var commonAncestor = e.getNode().commonAncestor(c.node());
                 if (commonAncestor == c.node()) {
+                    boolean copySteps = CachingSettingsProvider.getCachingSettings().getPrune()
+                            .equals(ProofCachingSettings.PRUNE_COPY);
                     // proof is now open
                     // => remove caching reference
                     g.node().deregister(c, ClosedBy.class);
                     p.reOpenGoal(g);
+                    if (copySteps) {
+                        // quickly copy the proof before it is pruned
+                        try {
+                            new CopyingProofReplayer(c.proof(), p).copy(c.node(), g,
+                                c.nodesToSkip());
+                        } catch (IntermediateProofReplayer.BuiltInConstructionException ex) {
+                            LOGGER.warn("failed to copy referenced proof that" +
+                                "is about to be pruned", ex);
+                            IssueDialog.showExceptionDialog(MainWindow.getInstance(), ex);
+                        }
+                    }
                 }
             }
         }

keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachingSettingsProvider.java

@@ -15,15 +15,17 @@
 
 import static de.uka.ilkd.key.settings.ProofCachingSettings.DISPOSE_COPY;
 import static de.uka.ilkd.key.settings.ProofCachingSettings.DISPOSE_REOPEN;
+import static de.uka.ilkd.key.settings.ProofCachingSettings.PRUNE_COPY;
+import static de.uka.ilkd.key.settings.ProofCachingSettings.PRUNE_REOPEN;
 
 /**
- * Settings for the proof slicing extension.
+ * Settings for the proof caching extension.
  *
  * @author Arne Keller
  */
 public class CachingSettingsProvider extends SettingsPanel implements SettingsProvider {
     /**
-     * Singleton instance of the slicing settings.
+     * Singleton instance of the caching settings.
      */
     private static final ProofCachingSettings CACHING_SETTINGS = new ProofCachingSettings();
 
@@ -36,14 +38,26 @@ public class CachingSettingsProvider extends SettingsPanel implements SettingsPr
      */
     private static final String STRATEGY_SEARCH =
         "Automatically search for references in auto mode";
+    /**
+     * Label for second option.
+     */
     private static final String DISPOSE_TITLE =
         "Behaviour when disposing referenced proof";
+    private static final String PRUNE_TITLE =
+        "Behaviour when pruning into referenced proof";
 
     /**
      * Checkbox for first option.
      */
     private final JCheckBox strategySearch;
+    /**
+     * Combobox for second option (dispose behaviour).
+     */
     private final JComboBox<String> disposeOption;
+    /**
+     * Combobox for third option (prune behaviour).
+     */
+    private final JComboBox<String> pruneOption;
 
     /**
      * Construct a new settings provider.
@@ -57,6 +71,11 @@ public CachingSettingsProvider() {
             addCheckBox(STRATEGY_SEARCH, "", true, emptyValidator());
         disposeOption = addComboBox(DISPOSE_TITLE, null, 0, x -> {
         }, DISPOSE_COPY, DISPOSE_REOPEN);
+        pruneOption = addComboBox(PRUNE_TITLE, """
+                When a referenced proof is pruned, this is what happens to
+                 all cached branches that reference it.""",
+            0, x -> {
+            }, PRUNE_REOPEN, PRUNE_COPY);
     }
 
     @Override
@@ -77,6 +96,7 @@ public JPanel getPanel(MainWindow window) {
         ProofCachingSettings ss = getCachingSettings();
         strategySearch.setSelected(ss.getEnabled());
         disposeOption.setSelectedItem(ss.getDispose());
+        pruneOption.setSelectedItem(ss.getPrune());
         return this;
     }
 
@@ -85,6 +105,7 @@ public void applySettings(MainWindow window) {
         ProofCachingSettings ss = getCachingSettings();
         ss.setEnabled(strategySearch.isEnabled());
         ss.setDispose(disposeOption.getSelectedItem().toString());
+        ss.setPrune(pruneOption.getSelectedItem().toString());
     }