Backport of KEY-2.12.1 into main

build.gradle

@@ -32,16 +32,6 @@ idea {
     }
 }
 
-// Helper function that calls "git rev-parse" to
-// find names/SHAs for commits
-static def gitRevParse(String args) {
-    try {
-        return "git rev-parse $args".execute().text.trim()
-    } catch (Exception e) {
-        return ""
-    }
-}
-
 static def getDate() {
     return new Date().format('yyyyMMdd')
 }

key.core/build.gradle

@@ -172,6 +172,7 @@ task generateVersionFiles() {
     def branch = new File(outputFolder, "branch")
     def versionf = new File(outputFolder, "version")
 
+    inputs.files "$project.rootDir/.git/HEAD"
     outputs.files sha1, branch, versionf
 
     def gitRevision = gitRevParse('HEAD')
@@ -184,6 +185,16 @@ task generateVersionFiles() {
     }
 }
 
+// Helper function that calls "git rev-parse" to
+// find names/SHAs for commits
+static def gitRevParse(String args) {
+    try {
+        return "git rev-parse $args".execute().text.trim()
+    } catch (Exception e) {
+        return ""
+    }
+}
+
 // @AW: Say something here. From POV this explain by itself.
 processResources.dependsOn generateVersionFiles
 

key.core/src/main/java/de/uka/ilkd/key/control/KeYEnvironment.java

@@ -318,5 +318,4 @@ public boolean isDisposed() {
     public Pair<String, Location> getProofScript() {
         return proofScript;
     }
-
 }

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

@@ -14,6 +14,7 @@
 import de.uka.ilkd.key.proof.init.InitConfig;
 import de.uka.ilkd.key.proof.init.Profile;
 import de.uka.ilkd.key.proof.mgt.SpecificationRepository;
+import de.uka.ilkd.key.settings.ProofIndependentSettings;
 import de.uka.ilkd.key.util.Debug;
 import de.uka.ilkd.key.util.KeYRecoderExcHandler;
 
@@ -298,6 +299,10 @@ public void setProof(Proof p_proof) {
                 "Services are already owned by another proof:" + proof.name());
         }
         proof = p_proof;
+        if (!ProofIndependentSettings.DEFAULT_INSTANCE.getTermLabelSettings().getUseOriginLabels()
+                || !proof.getSettings().getTermLabelSettings().getUseOriginLabels()) {
+            profile.getTermLabelManager().disableOriginLabelRefactorings();
+        }
     }
 
 

key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabelManager.java

@@ -5,6 +5,8 @@
 
 import java.util.*;
 import java.util.Map.Entry;
+import java.util.Set;
+import java.util.stream.Collectors;
 
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.logic.*;
@@ -16,6 +18,11 @@
 import de.uka.ilkd.key.rule.Rule;
 import de.uka.ilkd.key.rule.RuleApp;
 import de.uka.ilkd.key.rule.label.*;
+import de.uka.ilkd.key.rule.label.ChildTermLabelPolicy;
+import de.uka.ilkd.key.rule.label.OriginTermLabelRefactoring;
+import de.uka.ilkd.key.rule.label.TermLabelMerger;
+import de.uka.ilkd.key.rule.label.TermLabelPolicy;
+import de.uka.ilkd.key.rule.label.TermLabelRefactoring;
 import de.uka.ilkd.key.rule.label.TermLabelRefactoring.RefactoringScope;
 import de.uka.ilkd.key.util.LinkedHashMap;
 import de.uka.ilkd.key.util.Pair;
@@ -2194,4 +2201,14 @@ protected void mergeLabels(SequentChangeInfo currentSequent, Services services,
             }
         }
     }
+
+    /**
+     * Fully disable origin tracking. This will remove the {@link OriginTermLabelRefactoring} from
+     * the manager.
+     */
+    public void disableOriginLabelRefactorings() {
+        allRulesRefactorings = ImmutableList.fromList(
+            allRulesRefactorings.stream().filter(x -> !(x instanceof OriginTermLabelRefactoring))
+                    .collect(Collectors.toList()));
+    }
 }

key.core/src/main/java/de/uka/ilkd/key/macros/ProofMacroFinishedInfo.java

@@ -4,9 +4,11 @@
 package de.uka.ilkd.key.macros;
 
 import java.util.HashMap;
+import java.util.List;
 import java.util.Map;
 
 import de.uka.ilkd.key.proof.Goal;
+import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.proof.Statistics;
 import de.uka.ilkd.key.prover.impl.ApplyStrategyInfo;
@@ -70,6 +72,12 @@ public ProofMacroFinishedInfo(ProofMacro macro, ImmutableList<Goal> goals) {
         this(macro, goals, goals.isEmpty() ? null : goals.head().proof(), false);
     }
 
+    public ProofMacroFinishedInfo(ProofMacro macro, ImmutableList<Goal> goals,
+            List<Node> statisticNodes) {
+        this(macro, goals, goals.isEmpty() ? null : goals.head().proof(),
+            statisticNodes.isEmpty() ? null : new Statistics(statisticNodes));
+    }
+
     public ProofMacroFinishedInfo(ProofMacro macro, Proof proof) {
         this(macro, proof.openEnabledGoals(), proof, false);
     }

key.core/src/main/java/de/uka/ilkd/key/macros/StrategyProofMacro.java

@@ -3,9 +3,13 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.macros;
 
+import java.util.List;
+import java.util.stream.Collectors;
+
 import de.uka.ilkd.key.control.UserInterfaceControl;
 import de.uka.ilkd.key.logic.PosInOccurrence;
 import de.uka.ilkd.key.proof.Goal;
+import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.prover.GoalChooser;
 import de.uka.ilkd.key.prover.ProverCore;
@@ -72,6 +76,7 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof,
             // false
             return null;
         }
+        List<Node> nodes = goals.stream().map(Goal::node).collect(Collectors.toList());
 
         final GoalChooser goalChooser =
             proof.getInitConfig().getProfile().getSelectedGoalChooserBuilder().create();
@@ -84,9 +89,9 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof,
             new ProgressBarListener(goals.size(), getMaxSteps(proof), listener);
         applyStrategy.addProverTaskObserver(pml);
         // add a focus manager if there is a focus
-        if (posInOcc != null && goals != null) {
-            AutomatedRuleApplicationManager realManager = null;
-            FocussedRuleApplicationManager manager = null;
+        if (posInOcc != null) {
+            AutomatedRuleApplicationManager realManager;
+            FocussedRuleApplicationManager manager;
             for (Goal goal : goals) {
                 realManager = goal.getRuleAppManager();
                 realManager.clearCache();
@@ -99,7 +104,7 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof,
         Strategy oldStrategy = proof.getActiveStrategy();
         proof.setActiveStrategy(createStrategy(proof, posInOcc));
 
-        ProofMacroFinishedInfo info = new ProofMacroFinishedInfo(this, goals, proof, false);
+        ProofMacroFinishedInfo info;
         try {
             // find the relevant goals
             // and start
@@ -125,7 +130,8 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof,
             }
             final ImmutableList<Goal> resultingGoals =
                 setDifference(proof.openGoals(), ignoredOpenGoals);
-            info = new ProofMacroFinishedInfo(this, resultingGoals);
+            info = new ProofMacroFinishedInfo(this, resultingGoals,
+                nodes);
             proof.setActiveStrategy(oldStrategy);
             doPostProcessing(proof);
             applyStrategy.removeProverTaskObserver(pml);

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

@@ -73,6 +73,78 @@ protected Statistics(int nodes, int branches, int cachedBranches, int interactiv
         this.timePerStepInMillis = timePerStepInMillis;
     }
 
+    public Statistics(List<Node> startNodes) {
+        if (startNodes.isEmpty()) {
+            throw new IllegalArgumentException("can't generate statistics on zero nodes");
+        }
+
+        int nodes = 0;
+        int branches = 0;
+        int cachedBranches = 0;
+        int interactiveSteps = 0;
+        int symbExApps = 0;
+        int quantifierInstantiations = 0;
+        int ossApps = 0;
+        int mergeRuleApps = 0;
+        int totalRuleApps = 0;
+        int smtSolverApps = 0;
+        int dependencyContractApps = 0;
+        int operationContractApps = 0;
+        int blockLoopContractApps = 0;
+        int loopInvApps = 0;
+        long autoModeTimeInMillis = 0;
+        long timeInMillis = 0;
+
+        for (Node startNode : startNodes) {
+            final Iterator<Node> it = startNode.subtreeIterator();
+
+            TemporaryStatistics tmp = new TemporaryStatistics();
+
+            Node node;
+            while (it.hasNext()) {
+                node = it.next();
+                tmp.changeOnNode(node, interactiveAppsDetails);
+            }
+
+            nodes += tmp.nodes;
+            branches = tmp.branches;
+            cachedBranches = tmp.cachedBranches;
+            interactiveSteps = tmp.interactive;
+            symbExApps = tmp.symbExApps;
+            quantifierInstantiations = tmp.quant;
+            ossApps = tmp.oss;
+            mergeRuleApps = tmp.mergeApps;
+            totalRuleApps = tmp.nodes + tmp.ossCaptured - 1;
+            smtSolverApps = tmp.smt;
+            dependencyContractApps = tmp.dep;
+            operationContractApps = tmp.contr;
+            blockLoopContractApps = tmp.block;
+            loopInvApps = tmp.inv;
+            autoModeTimeInMillis = startNode.proof().getAutoModeTime();
+            timeInMillis = (System.currentTimeMillis() - startNode.proof().creationTime);
+        }
+
+        this.nodes = nodes;
+        this.branches = branches;
+        this.cachedBranches = cachedBranches;
+        this.interactiveSteps = interactiveSteps;
+        this.symbExApps = symbExApps;
+        this.quantifierInstantiations = quantifierInstantiations;
+        this.ossApps = ossApps;
+        this.mergeRuleApps = mergeRuleApps;
+        this.totalRuleApps = totalRuleApps;
+        this.smtSolverApps = smtSolverApps;
+        this.dependencyContractApps = dependencyContractApps;
+        this.operationContractApps = operationContractApps;
+        this.blockLoopContractApps = blockLoopContractApps;
+        this.loopInvApps = loopInvApps;
+        this.autoModeTimeInMillis = autoModeTimeInMillis;
+        this.timeInMillis = timeInMillis;
+        this.timePerStepInMillis = nodes <= 1 ? .0f : (autoModeTimeInMillis / (float) (nodes - 1));
+
+        generateSummary(startNodes.get(0).proof());
+    }
+
     Statistics(Node startNode) {
         final Iterator<Node> it = startNode.subtreeIterator();
 

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

@@ -92,7 +92,7 @@ public static ClosedBy findPreviousProof(DefaultListModel<Proof> previousProofs,
                 // for each node, check that the sequent in the reference is
                 // a subset of the new sequent
                 Node n = nodesToCheck.remove();
-                if (checkedNodes.contains(n)) {
+                if (checkedNodes.contains(n) || !n.isClosed()) {
                     continue;
                 }
                 checkedNodes.add(n);

key.core/src/main/java/de/uka/ilkd/key/smt/communication/ExternalProcessLauncher.java

@@ -76,7 +76,9 @@ public void launch(final String[] command) throws IOException {
      */
     public void stop() {
         if (process != null) {
-            process.destroy();
+            // make sure the solver process is properly killed,
+            // otherwise it may consume excessive CPU and RAM
+            process.destroyForcibly();
         }
         // TODO: where to close the pipe?
         // pipe.close();

key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlChecks.java

@@ -81,7 +81,7 @@ private void checkRequires(List<JmlParser.ClauseContext> clauses) {
 
             if (isRequiresClause(clause) && otherClause) {
                 addWarning(clause,
-                    "Diverging Semantics form JML Reference: Requires does not initiate a new contract. "
+                    "Diverging Semantics from JML Reference: Requires does not initiate a new contract. "
                         + "See https://keyproject.github.io/key-docs/user/JMLGrammar/#TODO");
             }
         }

key.core/src/main/java/de/uka/ilkd/key/util/MiscTools.java

@@ -816,9 +816,15 @@ public static URI getURIFromTokenSource(String source) {
         }
 
         try {
-            return new URI(source);
+            URI uri = new URI(source);
+            if (uri.getScheme() != null) {
+                // use this URI only if there is an explicit scheme;
+                // otherwise parse it as a filename
+                return uri;
+            }
         } catch (URISyntaxException ignored) {
         }
+
         return Path.of(source).toUri();
     }
 

key.core/src/test/java/de/uka/ilkd/key/proof/TestOneStepSimplifier.java

@@ -27,5 +27,6 @@ void loadWithRestriction() throws ProblemLoaderException {
             KeYEnvironment.load(new File(testCaseDirectory, "ossRestriction.proof"));
         Assertions.assertNotNull(env.getLoadedProof());
         Assertions.assertTrue(env.getLoadedProof().closed());
+        env.dispose();
     }
 }

key.core/src/test/java/de/uka/ilkd/key/proof/replay/TestCopyingReplayer.java

@@ -51,5 +51,8 @@ void testJavaProof() throws Exception {
         Assertions.assertEquals(proof1.countNodes(), proof2.countNodes());
 
         GeneralSettings.noPruningClosed = true;
+
+        env.dispose();
+        env2.dispose();
     }
 }

key.core/src/test/java/de/uka/ilkd/key/speclang/njml/NJmlTranslatorTests.java

@@ -6,6 +6,7 @@
 import java.io.File;
 import java.net.URI;
 import java.net.URISyntaxException;
+import java.nio.file.Path;
 
 import de.uka.ilkd.key.java.JavaInfo;
 import de.uka.ilkd.key.java.Position;
@@ -79,7 +80,7 @@ public void testIgnoreOpenJML() {
     // }
 
     @Test
-    public void testWarnRequires() throws URISyntaxException {
+    void testWarnRequires() throws URISyntaxException {
         preParser.clearWarnings();
         String contract = "/*@ requires true; ensures true; requires true;";
         ImmutableList<TextualJMLConstruct> result =
@@ -88,8 +89,9 @@ public void testWarnRequires() throws URISyntaxException {
         ImmutableList<PositionedString> warnings = preParser.getWarnings();
         PositionedString message = warnings.head();
         assertEquals(
-            "Diverging Semantics form JML Reference: Requires does not initiate a new contract. "
-                + "See https://keyproject.github.io/key-docs/user/JMLGrammar/#TODO (Test.java, 5/38)",
+            "Diverging Semantics from JML Reference: Requires does not initiate a new contract. "
+                + "See https://keyproject.github.io/key-docs/user/JMLGrammar/#TODO ("
+                + Path.of("Test.java").toUri() + ", 5/38)",
             message.toString());
     }
 

key.core/src/test/java/de/uka/ilkd/key/util/TestEqualsModProofIrrelevancy.java

@@ -57,5 +57,7 @@ void testJavaProof() throws Exception {
                     node1.getAppliedRuleApp().equalsModProofIrrelevancy(node2.getAppliedRuleApp()));
             }
         }
+        env.dispose();
+        env2.dispose();
     }
 }

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

@@ -16,6 +16,7 @@
 import de.uka.ilkd.key.control.ProofControl;
 import de.uka.ilkd.key.gui.GUIListener;
 import de.uka.ilkd.key.gui.InspectorForDecisionPredicates;
+import de.uka.ilkd.key.gui.MainWindow;
 import de.uka.ilkd.key.gui.UserActionListener;
 import de.uka.ilkd.key.gui.actions.useractions.UserAction;
 import de.uka.ilkd.key.gui.notification.events.ExceptionFailureEvent;
@@ -566,6 +567,7 @@ public void interrupt() {
      * @param b true iff interactive mode is to be turned on
      */
     public void setInteractive(boolean b) {
+        MainWindow.getInstance().getAutoModeAction().setEnabled(true);
         if (getSelectedProof() != null) {
             if (b) {
                 getSelectedProof().setRuleAppIndexToInteractiveMode();

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

@@ -775,6 +775,14 @@ public void setStandardStatusLine() {
         ThreadUtilities.invokeOnEventQueue(this::setStandardStatusLineImmediately);
     }
 
+    /**
+     * Hide the progress bar if it is currently visible.
+     */
+    public void hideStatusProgress() {
+        getStatusLine().setProgress(0);
+        statusLine.setProgressPanelVisible(false);
+    }
+
     private void setStatusLineImmediately(String str, int max) {
         // statusLine.reset();
         statusLine.setStatusText(str);

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

@@ -197,7 +197,7 @@ private void taskFinishedInternal(TaskFinishedInfo info) {
             mainWindow.displayResults(info.toString());
         } else if (info != null && info.getSource() instanceof ProofMacro) {
             if (!isAtLeastOneMacroRunning()) {
-                resetStatus(this);
+                mainWindow.hideStatusProgress();
                 assert info instanceof ProofMacroFinishedInfo;
                 Proof proof = info.getProof();
                 if (proof != null && !proof.closed()