Merge branch 'main' into weigl/jsonrpc

* main: (68 commits)
  fix classcastexception in logic printer
  Spotless changes
  Slight change to tooltip text.
  heap indication (logging and status line)
  replace JSR305 annotations with JSpecify
  Added forgotten test for getFirst
  Remaned methods to better reflect their intention
  Fix bug in refectoring retrieval
  Add comments and test for LabelCollection
  Clean up
  spotless changes and some typo corrections
  clean up
  Some additional optimisations
  Optimized TermLabel processing using a linked hash set for common operations instead of a list
  Refactorings container can use mutable linked sets
  Optimize offline dependency tracker and add tests
  IdentityHashSet collection class
  Contract creation should use correct OriginLabel settings
  Minor polishing
  Simplify TermLabelManager API
  ...

# Conflicts:
#	key.core/src/main/java/de/uka/ilkd/key/proof/Node.java
#	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/RunAllProofsAction.java

Author: wadoon

build.gradle

@@ -57,8 +57,10 @@ subprojects {
     group = rootProject.group
     version = rootProject.version
 
-    sourceCompatibility = 17
-    targetCompatibility = 17
+    java {
+        sourceCompatibility = 17
+        targetCompatibility = 17
+    }
 
     repositories {
         mavenCentral()
@@ -69,20 +71,17 @@ subprojects {
 
     dependencies {
         implementation("org.slf4j:slf4j-api:2.0.9")
-        testImplementation("ch.qos.logback:logback-classic:1.4.11")
-
-        //compile group: 'org.apache.logging.log4j', name: 'log4j-api', version: '2.12.0'
-        //compile group: 'org.apache.logging.log4j', name: 'log4j-core', version: '2.12.0'
-        implementation 'com.google.code.findbugs:jsr305:3.0.2'
 
+        testImplementation("ch.qos.logback:logback-classic:1.4.11")
         testImplementation 'org.junit.jupiter:junit-jupiter-api:5.10.0'
         testImplementation 'org.junit.jupiter:junit-jupiter-params:5.10.0'
+        testImplementation project(':key.util')
+
         testCompileOnly 'junit:junit:4.13.2'
         testRuntimeOnly 'org.junit.vintage:junit-vintage-engine:5.10.0'
         testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.10.0'
 
-
-        testImplementation project(':key.util')
+        implementation("org.jspecify:jspecify:0.3.0")
     }
 
     tasks.withType(JavaCompile) {

gradle/wrapper/gradle-wrapper.properties

@@ -1,5 +1,5 @@
 distributionBase=GRADLE_USER_HOME
 distributionPath=wrapper/dists
-distributionUrl=https\://services.gradle.org/distributions/gradle-8.1.1-bin.zip
+distributionUrl=https\://services.gradle.org/distributions/gradle-8.4-bin.zip
 zipStoreBase=GRADLE_USER_HOME
 zipStorePath=wrapper/dists

key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/reference/DefaultProofReference.java

@@ -10,6 +10,8 @@
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.Proof;
 
+import org.key_project.util.Strings;
+
 /**
  * Default implementation of {@link IProofReference}.
  *
@@ -40,7 +42,7 @@ public class DefaultProofReference<T> implements IProofReference<T> {
      * Constructor
      *
      * @param kind The reference kind as human readable {@link String}.
-     * @param source The source {@link Proof}.
+     * @param node Node to access the source {@link Proof} (or null).
      * @param target The target source member.
      */
     public DefaultProofReference(String kind, Node node, T target) {
@@ -128,15 +130,7 @@ public String toString() {
         sb.append("\"");
         if (!getNodes().isEmpty()) {
             sb.append(" at node(s) ");
-            boolean afterFirst = false;
-            for (Node node : getNodes()) {
-                if (afterFirst) {
-                    sb.append(", ");
-                } else {
-                    afterFirst = true;
-                }
-                sb.append(node.serialNr());
-            }
+            sb.append(Strings.formatAsList(getNodes(), "", ", ", "", Node::serialNr));
         }
         if (getSource() != null) {
             sb.append(" of proof \"");

key.core.rifl/src/main/java/de/uka/ilkd/key/util/rifl/RIFLTransformer.java

@@ -26,7 +26,8 @@
 import recoder.java.JavaProgramFactory;
 import recoder.java.declaration.ClassDeclaration;
 import recoder.java.declaration.MethodDeclaration;
-import recoder.java.declaration.ParameterDeclaration;
+
+import static org.key_project.util.Strings.*;
 
 /**
  * Facet class for interpreting RIFL specifications. The Requirements for Information Flow Language
@@ -194,16 +195,8 @@ public void doTransform(final File riflFilename, final File source, final File s
 
             ClassDeclaration clazz = (ClassDeclaration) cu.getPrimaryTypeDeclaration();
             for (MethodDeclaration mdecl : si.getSpecifiedMethodDeclarations()) {
-
-
-                StringBuilder sb = new StringBuilder();
-                for (ParameterDeclaration p : mdecl.getParameters()) {
-                    sb.append(p.getTypeReference().getName());
-                    sb.append(",");
-                }
-                if (sb.length() > 0) {
-                    sb.deleteCharAt(sb.length() - 1);
-                }
+                final StringBuilder sb = new StringBuilder();
+                sb.append(formatAsList(mdecl.getParameters(), "", ",", ""));
 
                 String poname = clazz.getFullName() + "[" + clazz.getFullName() + "\\\\:\\\\:"
                     + mdecl.getName() + "(" + sb + ")" + "]" + ".Non-interference contract.0";

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/BlockContractValidityTermLabelUpdate.java

@@ -6,22 +6,18 @@
 import java.util.Set;
 
 import de.uka.ilkd.key.java.Services;
-import de.uka.ilkd.key.logic.JavaBlock;
 import de.uka.ilkd.key.logic.Name;
 import de.uka.ilkd.key.logic.PosInOccurrence;
 import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.logic.label.BlockContractValidityTermLabel;
 import de.uka.ilkd.key.logic.label.TermLabel;
 import de.uka.ilkd.key.logic.label.TermLabelState;
-import de.uka.ilkd.key.logic.op.Operator;
-import de.uka.ilkd.key.logic.op.QuantifiableVariable;
 import de.uka.ilkd.key.rule.BlockContractInternalRule;
 import de.uka.ilkd.key.rule.LoopContractInternalRule;
 import de.uka.ilkd.key.rule.Rule;
 import de.uka.ilkd.key.rule.RuleApp;
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;
 
-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.java.CollectionUtil;
@@ -47,9 +43,8 @@ public ImmutableList<Name> getSupportedRuleNames() {
     @Override
     public void updateLabels(TermLabelState state, Services services,
             PosInOccurrence applicationPosInOccurrence, Term applicationTerm, Term modalityTerm,
-            Rule rule, RuleApp ruleApp, Object hint, Term tacletTerm, Operator newTermOp,
-            ImmutableArray<Term> newTermSubs, ImmutableArray<QuantifiableVariable> newTermBoundVars,
-            JavaBlock newTermJavaBlock, Set<TermLabel> labels) {
+            Rule rule, RuleApp ruleApp, Object hint, Term tacletTerm, Term newTerm,
+            Set<TermLabel> labels) {
         if ((rule instanceof BlockContractInternalRule || rule instanceof LoopContractInternalRule)
                 && ((BlockContractInternalRule.BlockContractHint) hint)
                         .getExceptionalVariable() != null

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelRefactoring.java

@@ -8,6 +8,7 @@
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.logic.*;
 import de.uka.ilkd.key.logic.label.FormulaTermLabel;
+import de.uka.ilkd.key.logic.label.LabelCollection;
 import de.uka.ilkd.key.logic.label.TermLabel;
 import de.uka.ilkd.key.logic.label.TermLabelState;
 import de.uka.ilkd.key.proof.Goal;
@@ -28,7 +29,7 @@
  */
 public class FormulaTermLabelRefactoring implements TermLabelRefactoring {
     /**
-     * Key prefix used in {@link TermLabelState} to store that the inner most label was already
+     * Key prefix used in {@link TermLabelState} to store that the innermost label was already
      * refactored on a given {@link Goal}.
      */
     private static final String INNER_MOST_PARENT_REFACTORED_PREFIX =
@@ -37,7 +38,8 @@ public class FormulaTermLabelRefactoring implements TermLabelRefactoring {
     /**
      * Key used in {@link TermLabelState} by the {@link StayOnOperatorTermLabelPolicy} to indicate
      * that a refactoring below an update ({@link RefactoringScope#APPLICATION_BELOW_UPDATES}) is
-     * required performed by {@link #refactorBewlowUpdates(PosInOccurrence, Term, List)}.
+     * required, which will be performed by
+     * {@link #refactorBelowUpdates(PosInOccurrence, Term, LabelCollection)}.
      * <p>
      * This is for instance required for the following rules:
      * <ul>
@@ -61,14 +63,14 @@ public class FormulaTermLabelRefactoring implements TermLabelRefactoring {
      * <li>{@code concrete_or_4}</li>
      * </ul>
      */
-    private static final String UPDATE_REFACTORING_REQUIRED = "updateRefactroingRequired";
+    private static final String UPDATE_REFACTORING_REQUIRED = "updateRefactoringRequired";
 
     /**
      * Key used in {@link TermLabelState} by the {@link FormulaTermLabelUpdate} to indicate that a
      * refactoring of parents
      * ({@link RefactoringScope#APPLICATION_CHILDREN_AND_GRANDCHILDREN_SUBTREE_AND_PARENTS}) is
-     * required performed by
-     * {@link #refactorInCaseOfNewIdRequired(TermLabelState, Goal, Term, Services, List)}.
+     * required, which will be performed by
+     * {@link #refactorInCaseOfNewIdRequired(TermLabelState, Goal, Term, Services, LabelCollection)}.
      * <p>
      * This is for instance required if a rule is applied on a sub term without a
      * {@link FormulaTermLabel} of a parent which has a {@link FormulaTermLabel}. Example rules are:
@@ -82,7 +84,8 @@ public class FormulaTermLabelRefactoring implements TermLabelRefactoring {
     /**
      * Key used in {@link TermLabelState} by the {@link FormulaTermLabelUpdate} to indicate that a
      * refactoring of specified {@link SequentFormula}s ({@link RefactoringScope#SEQUENT}) is
-     * required performed by {@link #refactorSequentFormulas(TermLabelState, Services, Term, List)}.
+     * required, which will be performed by
+     * {@link #refactorSequentFormulas(TermLabelState, Services, Term, LabelCollection)}.
      * <p>
      * This is for instance required if the assumes clause of a rule has a {@link FormulaTermLabel}
      * but the application does not have it. Example rules are:
@@ -110,9 +113,9 @@ public RefactoringScope defineRefactoringScope(TermLabelState state, Services se
             Object hint, Term tacletTerm) {
         if (shouldRefactorSpecificationApplication(rule, goal, hint)) {
             return RefactoringScope.APPLICATION_CHILDREN_AND_GRANDCHILDREN_SUBTREE;
-        } else if (isParentRefactroingRequired(state)) {
+        } else if (isParentRefactoringRequired(state)) {
             return RefactoringScope.APPLICATION_CHILDREN_AND_GRANDCHILDREN_SUBTREE_AND_PARENTS;
-        } else if (isUpdateRefactroingRequired(state)) {
+        } else if (isUpdateRefactoringRequired(state)) {
             return RefactoringScope.APPLICATION_BELOW_UPDATES;
         } else if (containsSequentFormulasToRefactor(state)) {
             return RefactoringScope.SEQUENT;
@@ -131,7 +134,7 @@ public RefactoringScope defineRefactoringScope(TermLabelState state, Services se
      * @param hint The hint to check.
      * @return {@code true} perform refactoring, {@code false} do not perform refactoring.
      */
-    protected boolean shouldRefactorSpecificationApplication(Rule rule, Goal goal, Object hint) {
+    private boolean shouldRefactorSpecificationApplication(Rule rule, Goal goal, Object hint) {
         return TermLabelRefactoring.shouldRefactorOnBuiltInRule(rule, goal, hint);
     }
 
@@ -141,13 +144,13 @@ protected boolean shouldRefactorSpecificationApplication(Rule rule, Goal goal, O
     @Override
     public void refactorLabels(TermLabelState state, Services services,
             PosInOccurrence applicationPosInOccurrence, Term applicationTerm, Rule rule, Goal goal,
-            Object hint, Term tacletTerm, Term term, List<TermLabel> labels) {
+            Object hint, Term tacletTerm, Term term, LabelCollection labels) {
         if (shouldRefactorSpecificationApplication(rule, goal, hint)) {
-            refactorSpecificationApplication(term, goal, services, labels, hint);
-        } else if (isParentRefactroingRequired(state)) {
+            refactorSpecificationApplication(term, services, labels, hint);
+        } else if (isParentRefactoringRequired(state)) {
             refactorInCaseOfNewIdRequired(state, goal, term, services, labels);
-        } else if (isUpdateRefactroingRequired(state)) {
-            refactorBewlowUpdates(applicationPosInOccurrence, term, labels);
+        } else if (isUpdateRefactoringRequired(state)) {
+            refactorBelowUpdates(applicationPosInOccurrence, term, labels);
         } else if (containsSequentFormulasToRefactor(state)) {
             refactorSequentFormulas(state, services, term, labels);
         } else if (SyntacticalReplaceVisitor.SUBSTITUTION_WITH_LABELS_HINT.equals(hint)) {
@@ -159,13 +162,12 @@ public void refactorLabels(TermLabelState state, Services services,
      * Refactors a specification application.
      *
      * @param term The {@link Term} which is now refactored.
-     * @param goal The optional {@link Goal} on which the {@link Term} to create will be used.
      * @param services The {@link Services} used by the {@link Proof} on which a {@link Rule} is
      *        applied right now.
      * @param labels The new labels the {@link Term} will have after the refactoring.
      */
-    protected void refactorSpecificationApplication(Term term, Goal goal, Services services,
-            List<TermLabel> labels, Object hint) {
+    private void refactorSpecificationApplication(Term term, Services services,
+            LabelCollection labels, Object hint) {
         if (TruthValueTracingUtil.isPredicate(term)
                 || (CloseAfterMerge.FINAL_WEAKENING_TERM_HINT.equals(hint)
                         && TruthValueTracingUtil.isLogicOperator(term))) {
@@ -180,7 +182,7 @@ protected void refactorSpecificationApplication(Term term, Goal goal, Services s
     }
 
     /**
-     * Refactors in case that the inner most label needs a new ID.
+     * Refactors in case that the innermost label needs a new ID.
      *
      * @param state The {@link TermLabelState} of the current rule application.
      * @param goal The optional {@link Goal} on which the {@link Term} to create will be used.
@@ -189,8 +191,8 @@ protected void refactorSpecificationApplication(Term term, Goal goal, Services s
      *        applied right now.
      * @param labels The new labels the {@link Term} will have after the refactoring.
      */
-    protected void refactorInCaseOfNewIdRequired(TermLabelState state, Goal goal, Term term,
-            Services services, List<TermLabel> labels) {
+    private void refactorInCaseOfNewIdRequired(TermLabelState state, Goal goal, Term term,
+            Services services, LabelCollection labels) {
         if (goal != null && !isInnerMostParentRefactored(state, goal)) {
             TermLabel existingLabel = term.getLabel(FormulaTermLabel.NAME);
             if (existingLabel instanceof FormulaTermLabel pLabel) {
@@ -212,8 +214,8 @@ protected void refactorInCaseOfNewIdRequired(TermLabelState state, Goal goal, Te
      * @param term The {@link Term} which is now refactored.
      * @param labels The new labels the {@link Term} will have after the refactoring.
      */
-    protected void refactorBewlowUpdates(PosInOccurrence applicationPosInOccurrence, Term term,
-            List<TermLabel> labels) {
+    private void refactorBelowUpdates(PosInOccurrence applicationPosInOccurrence, Term term,
+            LabelCollection labels) {
         Term applicationTerm =
             applicationPosInOccurrence != null ? applicationPosInOccurrence.subTerm() : null;
         FormulaTermLabel applicationLabel = applicationTerm != null
@@ -243,8 +245,8 @@ protected void refactorBewlowUpdates(PosInOccurrence applicationPosInOccurrence,
      * @param term The {@link Term} which is now refactored.
      * @param labels The new labels the {@link Term} will have after the refactoring.
      */
-    protected void refactorSequentFormulas(TermLabelState state, Services services, final Term term,
-            List<TermLabel> labels) {
+    private void refactorSequentFormulas(TermLabelState state, Services services, final Term term,
+            LabelCollection labels) {
         Set<SequentFormula> sequentFormulas = getSequentFormulasToRefactor(state);
         if (CollectionUtil.search(sequentFormulas, element -> element.formula() == term) != null) {
             FormulaTermLabel termLabel = (FormulaTermLabel) term.getLabel(FormulaTermLabel.NAME);
@@ -259,14 +261,14 @@ protected void refactorSequentFormulas(TermLabelState state, Services services,
     }
 
     /**
-     * Refactors the given {@link Term} after a substitiution.
+     * Refactors the given {@link Term} after a substitution.
      *
      * @param term The {@link Term} to refactor.
      * @param tacletTerm The taclet {@link Term} which provides additional labels to be merged with
      *        the other {@link Term}.
      * @param labels The new labels the {@link Term} will have after the refactoring.
      */
-    protected void refactorSubstitution(Term term, Term tacletTerm, List<TermLabel> labels) {
+    private void refactorSubstitution(Term term, Term tacletTerm, LabelCollection labels) {
         FormulaTermLabel tacletLabel =
             (FormulaTermLabel) tacletTerm.getLabel(FormulaTermLabel.NAME);
         if (tacletLabel != null) {
@@ -277,7 +279,7 @@ protected void refactorSubstitution(Term term, Term tacletTerm, List<TermLabel>
             } else {
                 List<String> beforeIds =
                     new ArrayList<>(Arrays.asList(existingLabel.getBeforeIds()));
-                boolean changed = true;
+                boolean changed = false;
                 if (!beforeIds.contains(tacletLabel.getId())) {
                     changed = true;
                     beforeIds.add(tacletLabel.getId());
@@ -298,7 +300,7 @@ protected void refactorSubstitution(Term term, Term tacletTerm, List<TermLabel>
     }
 
     /**
-     * Checks if the inner most parent was already refactored on the given {@link Goal}.
+     * Checks if the innermost parent was already refactored on the given {@link Goal}.
      *
      * @param state The {@link TermLabelState} to read from.
      * @param goal The {@link Goal} to check.
@@ -310,7 +312,7 @@ public static boolean isInnerMostParentRefactored(TermLabelState state, Goal goa
     }
 
     /**
-     * Defines if the inner most parent was already refactored on the given {@link Goal}.
+     * Defines if the innermost parent was already refactored on the given {@link Goal}.
      *
      * @param state The {@link TermLabelState} to read from.
      * @param goal The {@link Goal} to check.
@@ -329,7 +331,7 @@ public static void setInnerMostParentRefactored(TermLabelState state, Goal goal,
      * @param state The {@link TermLabelState} to read from.
      * @return {@code true} refactoring required, {@code false} refactoring is not required.
      */
-    public static boolean isUpdateRefactroingRequired(TermLabelState state) {
+    public static boolean isUpdateRefactoringRequired(TermLabelState state) {
         Map<Object, Object> labelState = state.getLabelState(FormulaTermLabel.NAME);
         Object value = labelState.get(UPDATE_REFACTORING_REQUIRED);
         return value instanceof Boolean && (Boolean) value;
@@ -341,7 +343,7 @@ public static boolean isUpdateRefactroingRequired(TermLabelState state) {
      * @param state The {@link TermLabelState} to modify.
      * @param required {@code true} refactoring required, {@code false} refactoring is not required.
      */
-    public static void setUpdateRefactroingRequired(TermLabelState state, boolean required) {
+    public static void setUpdateRefactoringRequired(TermLabelState state, boolean required) {
         Map<Object, Object> labelState = state.getLabelState(FormulaTermLabel.NAME);
         labelState.put(UPDATE_REFACTORING_REQUIRED, required);
     }
@@ -352,7 +354,7 @@ public static void setUpdateRefactroingRequired(TermLabelState state, boolean re
      * @param state The {@link TermLabelState} to read from.
      * @return {@code true} refactoring required, {@code false} refactoring is not required.
      */
-    public static boolean isParentRefactroingRequired(TermLabelState state) {
+    public static boolean isParentRefactoringRequired(TermLabelState state) {
         Map<Object, Object> labelState = state.getLabelState(FormulaTermLabel.NAME);
         Object value = labelState.get(PARENT_REFACTORING_REQUIRED);
         return value instanceof Boolean && (Boolean) value;
@@ -364,7 +366,7 @@ public static boolean isParentRefactroingRequired(TermLabelState state) {
      * @param state The {@link TermLabelState} to modify.
      * @param required {@code true} refactoring required, {@code false} refactoring is not required.
      */
-    public static void setParentRefactroingRequired(TermLabelState state, boolean required) {
+    public static void setParentRefactoringRequired(TermLabelState state, boolean required) {
         Map<Object, Object> labelState = state.getLabelState(FormulaTermLabel.NAME);
         labelState.put(PARENT_REFACTORING_REQUIRED, required);
     }