Proof caching: use dependency graph to increase hit rate

key.core/src/main/java/de/uka/ilkd/key/java/Comment.java

@@ -5,6 +5,9 @@
 
 import de.uka.ilkd.key.java.visitor.Visitor;
 
+/**
+ * Comment element of Java source code.
+ */
 public class Comment extends JavaSourceElement {
 
     private final String text;

key.core/src/main/java/de/uka/ilkd/key/java/declaration/MethodDeclaration.java

@@ -22,12 +22,35 @@
 public class MethodDeclaration extends JavaDeclaration implements MemberDeclaration,
         TypeReferenceContainer, NamedProgramElement, ParameterContainer, Method, VariableScope {
 
+    /**
+     * The return type of the method.
+     */
     protected final TypeReference returnType;
+    /**
+     * In case of void return type: comments associated with the method.
+     */
     protected final Comment[] voidComments;
+    /**
+     * The name of the method.
+     */
     protected final ProgramElementName name;
+    /**
+     * Parameters of the method.
+     */
     protected final ImmutableArray<ParameterDeclaration> parameters;
+    /**
+     * 'throws' part of the method. Indicates which exceptions the method may throw.
+     * May be null.
+     */
     protected final Throws exceptions;
+    /**
+     * Body of the method.
+     * May be null, in which case the body is referenced in a file using {@link #posInfo}.
+     */
     protected final StatementBlock body;
+    /**
+     * JML modifiers of the referenced method. Includes e.g. {@code pure}.
+     */
     protected final JMLModifiers jmlModifiers;
 
     /**
@@ -53,12 +76,14 @@ public record JMLModifiers(boolean pure, boolean strictlyPure, boolean helper,
     /**
      * Method declaration.
      *
-     * @param children an ExtList of children. May include: a TypeReference (as a reference to the
-     *        return type), a de.uka.ilkd.key.logic.ProgramElementName (as Name of the method),
-     *        several ParameterDeclaration (as parameters of the declared method), a StatementBlock
-     *        (as body of the declared method), several Modifier (taken as modifiers of the
-     *        declaration), a Comment
+     * @param children an ExtList of children. Must include: a TypeReference (as a reference to the
+     *        return type),
+     *        a {@link ProgramElementName} (as Name of the method),
+     *        one or more {@link ParameterDeclaration} (as parameters of the declared method),
+     *        optionally a {@link StatementBlock} (as body of the declared method),
+     *        optionally a {@link Throws} to indicate exceptional behaviour
      * @param parentIsInterfaceDeclaration a boolean set true iff parent is an InterfaceDeclaration
+     * @param voidComments in case of void return type: comments associated with the method
      */
     public MethodDeclaration(ExtList children, boolean parentIsInterfaceDeclaration,
             Comment[] voidComments) {
@@ -266,6 +291,12 @@ public TypeReference getTypeReference() {
     }
 
 
+    /**
+     * Get the "void comments" of this method declaration.
+     * Only non-null if the method has void return type.
+     *
+     * @return the "void comments"
+     */
     public Comment[] getVoidComments() {
         return voidComments;
     }

key.core/src/main/java/de/uka/ilkd/key/java/declaration/Throws.java

@@ -23,7 +23,7 @@ public class Throws extends JavaNonTerminalProgramElement implements TypeReferen
 
 
     /**
-     * Exceptions.
+     * Exceptions thrown.
      */
     protected final ImmutableArray<TypeReference> exceptions;
 

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

@@ -3,6 +3,7 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.logic;
 
+import java.util.Collection;
 import java.util.Iterator;
 
 import org.key_project.util.collection.ImmutableList;
@@ -27,11 +28,10 @@ private Semisequent() {
         seqList = ImmutableSLList.nil();
     }
 
-
     /**
-     * creates a new Semisequent with the Semisequent elements in seqList; the provided list must be
-     * redundancy free, i.e., the created sequent must be exactly the same as when creating the
-     * sequent by subsequently inserting all formulas
+     * Create a new Semisequent from an ordered collection of formulas.
+     * The provided list must be redundancy free, i.e., the created sequent must be exactly
+     * the same as when creating the sequent by subsequently inserting all formulas
      *
      * @param seqList list of sequent formulas
      */
@@ -40,6 +40,33 @@ public Semisequent(ImmutableList<SequentFormula> seqList) {
         this.seqList = seqList;
     }
 
+    /**
+     * Create a new Semisequent from an ordered collection of formulas.
+     * The provided collection must be redundancy free, i.e., the created sequent must be exactly
+     * the same as when creating the sequent by subsequently inserting all formulas
+     *
+     * @param seqList list of sequent formulas
+     */
+    public Semisequent(Collection<SequentFormula> seqList) {
+        assert !seqList.isEmpty();
+        this.seqList = ImmutableList.fromList(seqList);
+    }
+
+    /**
+     * Create a new Semisequent from an ordered collection of formulas (possibly empty).
+     * The provided collection must be redundancy free, i.e., the created sequent must be exactly
+     * the same as when creating the
+     * sequent by subsequently inserting all formulas.
+     *
+     * @param seqList list of sequent formulas
+     */
+    public static Semisequent create(Collection<SequentFormula> seqList) {
+        if (seqList.isEmpty()) {
+            return EMPTY_SEMISEQUENT;
+        }
+        return new Semisequent(seqList);
+    }
+
 
     /**
      * creates a new Semisequent with the Semisequent elements in seqList

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

@@ -22,24 +22,31 @@
 import org.key_project.util.collection.ImmutableArray;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
+import org.key_project.util.collection.ImmutableSet;
 
-import org.slf4j.Logger;
-import org.slf4j.LoggerFactory;
 
 /**
  * The program method represents a (pure) method in the logic. In case of a non-static method the
  * first argument represents the object on which the method is invoked.
+ * <p>
+ * This data is used in
+ * {@link de.uka.ilkd.key.speclang.QueryAxiom#getTaclets(ImmutableSet, Services)}.
  */
 public final class ProgramMethod extends ObserverFunction
         implements ProgramInLogic, IProgramMethod {
 
-    private static final Logger LOGGER = LoggerFactory.getLogger(ProgramMethod.class);
 
+    /**
+     * The referenced method.
+     */
     private final MethodDeclaration method;
     /**
      * Return type of the method. Must not be null. Use KeYJavaType.VOID_TYPE for void methods.
      */
     private final KeYJavaType returnType;
+    /**
+     * Where the method is located in a .java file.
+     */
     private final PositionInfo pi;
 
     // -------------------------------------------------------------------------
@@ -63,6 +70,12 @@ public ProgramMethod(MethodDeclaration method, KeYJavaType container, KeYJavaTyp
     // internal methods
     // -------------------------------------------------------------------------
 
+    /**
+     * Get the java types of the parameters required by the method md.
+     *
+     * @param md some method declaration
+     * @return java types of the parameters required by md
+     */
     private static ImmutableArray<KeYJavaType> getParamTypes(MethodDeclaration md) {
         KeYJavaType[] result = new KeYJavaType[md.getParameterDeclarationCount()];
         for (int i = 0; i < result.length; i++) {
@@ -80,11 +93,6 @@ private static ImmutableArray<KeYJavaType> getParamTypes(MethodDeclaration md) {
     // MethodDeclaration
     // in a direct way
 
-    /*
-     * (non-Javadoc)
-     *
-     * @see de.uka.ilkd.key.logic.op.IProgramMethod#getMethodDeclaration()
-     */
     @Override
     public MethodDeclaration getMethodDeclaration() {
         return method;

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

@@ -465,7 +465,7 @@ public Collection<Node> children() {
     }
 
     /**
-     * @return an iterator for all nodes in the subtree.
+     * @return an iterator for all nodes in the subtree (including this node).
      */
     public Iterator<Node> subtreeIterator() {
         return new SubtreeIterator(this);

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

@@ -6,6 +6,7 @@
 import java.beans.PropertyChangeListener;
 import java.io.File;
 import java.util.*;
+import java.util.function.Consumer;
 import java.util.function.Predicate;
 
 import de.uka.ilkd.key.java.JavaInfo;
@@ -16,8 +17,11 @@
 import de.uka.ilkd.key.proof.event.ProofDisposedListener;
 import de.uka.ilkd.key.proof.init.InitConfig;
 import de.uka.ilkd.key.proof.init.Profile;
+import de.uka.ilkd.key.proof.io.IntermediateProofReplayer;
 import de.uka.ilkd.key.proof.mgt.ProofCorrectnessMgt;
 import de.uka.ilkd.key.proof.mgt.ProofEnvironment;
+import de.uka.ilkd.key.proof.reference.ClosedBy;
+import de.uka.ilkd.key.proof.replay.CopyingProofReplayer;
 import de.uka.ilkd.key.rule.OneStepSimplifier;
 import de.uka.ilkd.key.settings.GeneralSettings;
 import de.uka.ilkd.key.settings.ProofIndependentSettings;
@@ -1254,4 +1258,46 @@ public <T> void deregister(T obj, Class<T> service) {
     public void setMutedProofCloseEvents(boolean mutedProofCloseEvents) {
         this.mutedProofCloseEvents = mutedProofCloseEvents;
     }
+
+    /**
+     * For each branch closed by reference to another proof,
+     * copy the relevant proof steps into this proof.
+     *
+     * @param referencedFrom filter, if not null copy only from that proof
+     * @param callbackTotal callback that gets the total number of branches to complete
+     * @param callbackBranch callback notified every time a branch has been copied
+     */
+    public void copyCachedGoals(Proof referencedFrom, Consumer<Integer> callbackTotal,
+            Runnable callbackBranch) {
+        // first, ensure that all cached goals are copied over
+        List<Goal> goals = closedGoals().toList();
+        List<Goal> todo = new ArrayList<>();
+        for (Goal g : goals) {
+            Node node = g.node();
+            ClosedBy c = node.lookup(ClosedBy.class);
+            if (c == null) {
+                continue;
+            }
+            if (referencedFrom != null && referencedFrom != c.proof()) {
+                continue;
+            }
+            todo.add(g);
+        }
+        if (callbackTotal != null) {
+            callbackTotal.accept(todo.size());
+        }
+        for (Goal g : todo) {
+            reOpenGoal(g);
+            ClosedBy c = g.node().lookup(ClosedBy.class);
+            g.node().deregister(c, ClosedBy.class);
+            try {
+                new CopyingProofReplayer(c.proof(), this).copy(c.node(), g, c.nodesToSkip());
+            } catch (IntermediateProofReplayer.BuiltInConstructionException e) {
+                throw new RuntimeException(e);
+            }
+            if (callbackBranch != null) {
+                callbackBranch.run();
+            }
+        }
+    }
 }

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

@@ -4,6 +4,7 @@
 package de.uka.ilkd.key.proof;
 
 import java.util.Iterator;
+import java.util.NoSuchElementException;
 
 /**
  * Iterator over subtree. Current implementation iteratively traverses the tree depth-first.
@@ -58,6 +59,8 @@ public Node next() {
             Node s = nextSibling(n);
             if (s != null) {
                 n = s;
+            } else {
+                throw new NoSuchElementException();
             }
         } else {
             n = n.child(0);

key.core/src/main/java/de/uka/ilkd/key/proof/reference/ClosedBy.java

@@ -3,15 +3,19 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.proof.reference;
 
+import java.util.Set;
+
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.Proof;
 
 /**
  * Indicates that a branch has been closed by "reference" to another closed proof.
+ * This is always looked up using {@link Node#lookup(Class)} on the node of that branch.
  *
  * @param proof The proof referenced.
  * @param node  The node referenced.
+ * @param nodesToSkip If the referenced proof has dependency graph information: proof steps to skip.
  * @author Arne Keller
  */
-public record ClosedBy(Proof proof, Node node) {
+public record ClosedBy(Proof proof, Node node, Set<Node> nodesToSkip) {
 }

key.core/src/main/java/de/uka/ilkd/key/proof/reference/CopyReferenceResolver.java

@@ -51,7 +51,7 @@ public static void copyCachedGoals(
             ClosedBy c = g.node().lookup(ClosedBy.class);
             g.node().deregister(c, ClosedBy.class);
             try {
-                new CopyingProofReplayer(c.proof(), toComplete).copy(c.node(), g);
+                new CopyingProofReplayer(c.proof(), toComplete).copy(c.node(), g, c.nodesToSkip());
             } catch (IntermediateProofReplayer.BuiltInConstructionException e) {
                 throw new RuntimeException(e);
             }

key.core/src/main/java/de/uka/ilkd/key/proof/replay/CopyingProofReplayer.java

@@ -5,6 +5,7 @@
 
 import java.util.ArrayDeque;
 import java.util.Deque;
+import java.util.Set;
 
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.Node;
@@ -35,24 +36,36 @@ public CopyingProofReplayer(Proof originalProof, Proof proof) {
      *
      * @param originalNode original proof
      * @param newNode open goal in new proof
+     * @param skippedNodes nodes to skip when copying
      * @throws IntermediateProofReplayer.BuiltInConstructionException on error
      */
-    public void copy(Node originalNode, Goal newNode)
+    public void copy(Node originalNode, Goal newNode, Set<Node> skippedNodes)
             throws IntermediateProofReplayer.BuiltInConstructionException {
         newNode.proof().reOpenGoal(newNode);
         newNode.proof().register(this, CopyingProofReplayer.class);
         newNode.proof().setMutedProofCloseEvents(true);
         OneStepSimplifier.refreshOSS(newNode.proof());
+
+        // nodeQueue: nodes in the ORIGINAL proof
         Deque<Node> nodeQueue = new ArrayDeque<>();
+        // queue: nodes in the NEW proof
         Deque<Goal> queue = new ArrayDeque<>();
+
         queue.add(newNode);
         nodeQueue.add(originalNode);
-        while (!nodeQueue.isEmpty()) {
+        while (!nodeQueue.isEmpty() && !queue.isEmpty()) {
             Node nextNode = nodeQueue.pop();
             Goal nextGoal = queue.pop();
             for (int i = nextNode.childrenCount() - 1; i >= 0; i--) {
                 nodeQueue.addFirst(nextNode.child(i));
             }
+            // skip explicitly requested nodes
+            if (skippedNodes.contains(nextNode)) {
+                if (!nextGoal.node().isClosed()) {
+                    queue.addFirst(nextGoal);
+                }
+                continue;
+            }
             // skip nextNode if it is a closed goal
             if (nextNode.getAppliedRuleApp() == null) {
                 continue;

key.core/src/main/java/de/uka/ilkd/key/speclang/QueryAxiom.java

@@ -180,6 +180,7 @@ public ImmutableSet<Taclet> getTaclets(ImmutableSet<Pair<Sort, IObserverFunction
         // create java block
         final ImmutableList<KeYJavaType> sig = ImmutableSLList.<KeYJavaType>nil()
                 .append(target.getParamTypes().toArray(new KeYJavaType[target.getNumParams()]));
+        // get real implementation of program method
         final IProgramMethod targetImpl =
             services.getJavaInfo().getProgramMethod(kjt, target.getName(), sig, kjt);
         final MethodBodyStatement mbs = new MethodBodyStatement(targetImpl, selfProgSV,