Applying Java 17 refactorings (#3252)

Applies refactorings after the switch to Java 17 for after #3241.

Including:

* Transform immutable data classes to Java records
* Rewrite `instanceof` and casts to Pattern expressions
* Use `.toList()` instead of `.collect(Collectors.toList)`
* Use Text Block Literals (`""" ... """`) on large strings instead of
concatenation cascades.

build.gradle

@@ -21,7 +21,7 @@ plugins {
     // id "com.github.ben-manes.versions" version "0.39.0"
 
     // Code formatting
-    id "com.diffplug.spotless" version "6.16.0"
+    id "com.diffplug.spotless" version "6.20.0"
 }
 
 // Configure this project for use inside IntelliJ:
@@ -335,7 +335,10 @@ subprojects {
             toggleOffOn()
 
             removeUnusedImports()
-            eclipse().configFile("$rootDir/scripts/tools/checkstyle/keyCodeStyle.xml")
+            /* At the moment, we have to ensure that version 4.22 of the eclipse formatter is run, since newer versions
+             * of the formatter crash in SymbolicExecutionTreeBuilder (seems to be a but in the formatter)!
+             */
+            eclipse("4.22").configFile("$rootDir/scripts/tools/checkstyle/keyCodeStyle.xml")
             trimTrailingWhitespace()        // not sure how to set this in the xml file ...
             //googleJavaFormat().aosp().reflowLongStrings()
 

key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/ClassAxiomAndInvariantProofReferencesAnalyst.java

@@ -65,9 +65,8 @@ public LinkedHashSet<IProofReference<?>> computeReferences(Node node, Services s
                         }
                     }
                 }
-                if (found instanceof PartialInvAxiom) {
+                if (found instanceof PartialInvAxiom axiom) {
                     // Invariant was applied
-                    PartialInvAxiom axiom = (PartialInvAxiom) found;
                     DefaultProofReference<ClassInvariant> reference =
                         new DefaultProofReference<>(IProofReference.USE_INVARIANT,
                             node, axiom.getInv());

key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/ContractProofReferencesAnalyst.java

@@ -23,9 +23,7 @@ public class ContractProofReferencesAnalyst implements IProofReferencesAnalyst {
      */
     @Override
     public LinkedHashSet<IProofReference<?>> computeReferences(Node node, Services services) {
-        if (node.getAppliedRuleApp() instanceof AbstractContractRuleApp) {
-            AbstractContractRuleApp contractRuleApp =
-                (AbstractContractRuleApp) node.getAppliedRuleApp();
+        if (node.getAppliedRuleApp() instanceof AbstractContractRuleApp contractRuleApp) {
             DefaultProofReference<Contract> reference = new DefaultProofReference<>(
                 IProofReference.USE_CONTRACT, node, contractRuleApp.getInstantiation());
             LinkedHashSet<IProofReference<?>> result = new LinkedHashSet<>();

key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/MethodBodyExpandProofReferencesAnalyst.java

@@ -26,8 +26,7 @@ public class MethodBodyExpandProofReferencesAnalyst implements IProofReferencesA
     public LinkedHashSet<IProofReference<?>> computeReferences(Node node, Services services) {
         if (node.getAppliedRuleApp() != null && node.getNodeInfo() != null) {
             NodeInfo info = node.getNodeInfo();
-            if (info.getActiveStatement() instanceof MethodBodyStatement) {
-                MethodBodyStatement mbs = (MethodBodyStatement) info.getActiveStatement();
+            if (info.getActiveStatement() instanceof MethodBodyStatement mbs) {
                 IProgramMethod pm = mbs.getProgramMethod(services);
                 DefaultProofReference<IProgramMethod> reference =
                     new DefaultProofReference<>(IProofReference.INLINE_METHOD, node,

key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/MethodCallProofReferencesAnalyst.java

@@ -55,8 +55,7 @@ public LinkedHashSet<IProofReference<?>> computeReferences(Node node, Services s
                         new LinkedHashSet<>();
                     result.add(reference);
                     return result;
-                } else if (info.getActiveStatement() instanceof Assignment) {
-                    Assignment assignment = (Assignment) info.getActiveStatement();
+                } else if (info.getActiveStatement() instanceof Assignment assignment) {
                     ExecutionContext context = extractContext(node, services);
                     LinkedHashSet<IProofReference<?>> result =
                         new LinkedHashSet<>();
@@ -110,7 +109,7 @@ protected IProofReference<IProgramMethod> createReference(Node node, Services se
             IProgramMethod pm = mr.method(services, refPrefixType, context);
             return new DefaultProofReference<>(IProofReference.CALL_METHOD, node, pm);
         } else {
-            if (!(node.getAppliedRuleApp() instanceof PosTacletApp)) {
+            if (!(node.getAppliedRuleApp() instanceof PosTacletApp app)) {
                 throw new IllegalArgumentException("PosTacletApp expected.");
             }
             if (!"staticMethodCallStaticWithAssignmentViaTypereference"
@@ -119,7 +118,6 @@ protected IProofReference<IProgramMethod> createReference(Node node, Services se
                     "Rule \"staticMethodCallStaticWithAssignmentViaTypereference\" expected, but is \""
                         + MiscTools.getRuleName(node) + "\".");
             }
-            PosTacletApp app = (PosTacletApp) node.getAppliedRuleApp();
             SchemaVariable methodSV = app.instantiations().lookupVar(new Name("#mn"));
             SchemaVariable typeSV = app.instantiations().lookupVar(new Name("#t"));
             SchemaVariable argsSV = app.instantiations().lookupVar(new Name("#elist"));

key.core.proof_references/src/main/java/de/uka/ilkd/key/proof_references/analyst/ProgramVariableReferencesAnalyst.java

@@ -70,8 +70,7 @@ protected void listReferences(Node node, ProgramElement pe, ProgramVariable arra
                         (ProgramVariable) pe);
                 ProofReferenceUtil.merge(toFill, reference);
             }
-        } else if (pe instanceof FieldReference) {
-            FieldReference fr = (FieldReference) pe;
+        } else if (pe instanceof FieldReference fr) {
             ReferencePrefix ref = fr.getReferencePrefix();
             if (ref != null) {
                 listReferences(node, ref, arrayLength, toFill, includeExpressionContainer);
@@ -82,8 +81,7 @@ protected void listReferences(Node node, ProgramElement pe, ProgramVariable arra
                     new DefaultProofReference<>(IProofReference.ACCESS, node, pv);
                 ProofReferenceUtil.merge(toFill, reference);
             }
-        } else if (includeExpressionContainer && pe instanceof ExpressionContainer) {
-            ExpressionContainer ec = (ExpressionContainer) pe;
+        } else if (includeExpressionContainer && pe instanceof ExpressionContainer ec) {
             for (int i = ec.getChildCount() - 1; i >= 0; i--) {
                 ProgramElement element = ec.getChildAt(i);
                 listReferences(node, element, arrayLength, toFill, includeExpressionContainer);

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

@@ -95,8 +95,7 @@ public Proof getSource() {
      */
     @Override
     public boolean equals(Object obj) {
-        if (obj instanceof IProofReference<?>) {
-            IProofReference<?> other = (IProofReference<?>) obj;
+        if (obj instanceof IProofReference<?> other) {
             return Objects.equals(getKind(), other.getKind())
                     && Objects.equals(getSource(), other.getSource())
                     && Objects.equals(getTarget(), other.getTarget());

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

@@ -23,7 +23,7 @@
  *
  * @author Martin Hentschel
  * @see ProofReferenceUtil
- * @see IProofReferencesAnalyst.
+ * @see IProofReferencesAnalyst
  */
 public interface IProofReference<T> {
     /**

key.core.proof_references/src/test/java/de/uka/ilkd/key/proof_references/testcase/AbstractProofReferenceTestCase.java

@@ -235,10 +235,10 @@ protected void assertReferences(LinkedHashSet<IProofReference<?>> current,
         int i = 0;
         for (IProofReference<?> currentReference : current) {
             ExpectedProofReferences expectedReference = expected[i];
-            assertEquals(expectedReference.getKind(), currentReference.getKind());
-            if (expectedReference.getTarget() != null) {
+            assertEquals(expectedReference.kind(), currentReference.getKind());
+            if (expectedReference.target() != null) {
                 assertNotNull(currentReference.getTarget());
-                assertEquals(expectedReference.getTarget(),
+                assertEquals(expectedReference.target(),
                     currentReference.getTarget().toString());
             } else {
                 assertNull(currentReference.getTarget());
@@ -250,48 +250,40 @@ protected void assertReferences(LinkedHashSet<IProofReference<?>> current,
     /**
      * Defines the values of an expected proof reference.
      *
+     * @param kind   The expected kind.
+     * @param target The expected target.
      * @author Martin Hentschel
      */
-    protected static class ExpectedProofReferences {
-        /**
-         * The expected kind.
-         */
-        private final String kind;
-
-        /**
-         * The expected target.
-         */
-        private final String target;
-
+        protected record ExpectedProofReferences(String kind, String target) {
         /**
          * Constructor.
          *
-         * @param kind The expected kind.
+         * @param kind   The expected kind.
          * @param target The expected target.
          */
-        public ExpectedProofReferences(String kind, String target) {
-            this.kind = kind;
-            this.target = target;
+        public ExpectedProofReferences {
         }
 
-        /**
-         * Returns the expected kind.
-         *
-         * @return The expected kind.
-         */
-        public String getKind() {
-            return kind;
-        }
+            /**
+             * Returns the expected kind.
+             *
+             * @return The expected kind.
+             */
+            @Override
+            public String kind() {
+                return kind;
+            }
 
-        /**
-         * Returns the expected target.
-         *
-         * @return The expected target.
-         */
-        public String getTarget() {
-            return target;
+            /**
+             * Returns the expected target.
+             *
+             * @return The expected target.
+             */
+            @Override
+            public String target() {
+                return target;
+            }
         }
-    }
 
     /**
      * Does some test steps with a {@link Proof}.

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/proof/TermProgramVariableCollectorKeepUpdatesForBreakpointconditions.java

@@ -34,9 +34,7 @@ public void visit(Term t) {
 
     private void addVarsToKeep() {
         for (IBreakpoint breakpoint : breakpointStopCondition.getBreakpoints()) {
-            if (breakpoint instanceof AbstractConditionalBreakpoint) {
-                AbstractConditionalBreakpoint conditionalBreakpoint =
-                    (AbstractConditionalBreakpoint) breakpoint;
+            if (breakpoint instanceof AbstractConditionalBreakpoint conditionalBreakpoint) {
                 if (conditionalBreakpoint.getToKeep() != null) {
                     for (LocationVariable sub : conditionalBreakpoint.getToKeep()) {
                         if (sub instanceof LocationVariable) {

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

@@ -193,8 +193,7 @@ protected void refactorInCaseOfNewIdRequired(TermLabelState state, Goal goal, Te
             Services services, List<TermLabel> labels) {
         if (goal != null && !isInnerMostParentRefactored(state, goal)) {
             TermLabel existingLabel = term.getLabel(FormulaTermLabel.NAME);
-            if (existingLabel instanceof FormulaTermLabel) {
-                FormulaTermLabel pLabel = (FormulaTermLabel) existingLabel;
+            if (existingLabel instanceof FormulaTermLabel pLabel) {
                 int labelID = pLabel.getMajorId();
                 int labelSubID = FormulaTermLabel.newLabelSubID(services, labelID);
                 labels.remove(existingLabel);
@@ -411,7 +410,7 @@ public static void addSequentFormulaToRefactor(TermLabelState state, SequentForm
         Set<SequentFormula> sfSet =
             (Set<SequentFormula>) labelState.get(SEQUENT_FORMULA_REFACTORING_REQUIRED);
         if (sfSet == null) {
-            sfSet = new LinkedHashSet<SequentFormula>();
+            sfSet = new LinkedHashSet<>();
             labelState.put(SEQUENT_FORMULA_REFACTORING_REQUIRED, sfSet);
         }
         sfSet.add(sf);

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

@@ -53,17 +53,15 @@ public void updateLabels(TermLabelState state, Services services,
             Rule rule, RuleApp ruleApp, Object hint, Term tacletTerm, Operator newTermOp,
             ImmutableArray<Term> newTermSubs, ImmutableArray<QuantifiableVariable> newTermBoundVars,
             JavaBlock newTermJavaBlock, Set<TermLabel> labels) {
-        if (hint instanceof TacletLabelHint) {
-            TacletLabelHint tacletHint = (TacletLabelHint) hint;
+        if (hint instanceof TacletLabelHint tacletHint) {
             if ((TacletOperation.ADD_ANTECEDENT.equals(tacletHint.getTacletOperation())
                     || TacletOperation.ADD_SUCCEDENT.equals(tacletHint.getTacletOperation()))
                     && (TruthValueTracingUtil.isPredicate(newTermOp)
                             || TruthValueTracingUtil.isLogicOperator(newTermOp, newTermSubs))) {
                 if (getTermLabel(labels, FormulaTermLabel.NAME) == null) {
                     TermLabel label = TermLabelManager.findInnerMostParentLabel(
                         applicationPosInOccurrence, FormulaTermLabel.NAME);
-                    if (label instanceof FormulaTermLabel) {
-                        FormulaTermLabel oldLabel = (FormulaTermLabel) label;
+                    if (label instanceof FormulaTermLabel oldLabel) {
                         int labelSubID = FormulaTermLabel.newLabelSubID(services, oldLabel);
                         FormulaTermLabel newLabel = new FormulaTermLabel(oldLabel.getMajorId(),
                             labelSubID, Collections.singletonList(oldLabel.getId()));
@@ -75,8 +73,7 @@ public void updateLabels(TermLabelState state, Services services,
                 }
             }
         }
-        if (ruleApp instanceof TacletApp) {
-            TacletApp ta = (TacletApp) ruleApp;
+        if (ruleApp instanceof TacletApp ta) {
             if (ta.ifInstsComplete() && ta.ifFormulaInstantiations() != null) {
                 Map<SequentFormula, FormulaTermLabel> ifLabels =
                     new LinkedHashMap<>();

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

@@ -50,8 +50,7 @@ public TermLabel keepLabel(TermLabelState state, Services services,
             // May change sub ID if logical operators like junctors are used
             boolean newLabelIdRequired = false;
             Set<String> originalLabelIds = new LinkedHashSet<>();
-            if (hint instanceof TacletLabelHint) {
-                TacletLabelHint tacletHint = (TacletLabelHint) hint;
+            if (hint instanceof TacletLabelHint tacletHint) {
                 if (isBelowIfThenElse(tacletHint.getTacletTermStack())) {
                     return null; // Do not label children of if-then-else. They are labeled when a
                                  // rule rewrites them outside of the if-then-else.

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/AbstractUpdateExtractor.java

@@ -175,8 +175,7 @@ protected void fillInitialObjectsToIgnoreRecursively(Term term, Set<Term> toFill
             for (int i = 0; i < term.arity(); i++) {
                 fillInitialObjectsToIgnoreRecursively(term.sub(i), toFill);
             }
-        } else if (term.op() instanceof ElementaryUpdate) {
-            ElementaryUpdate eu = (ElementaryUpdate) term.op();
+        } else if (term.op() instanceof ElementaryUpdate eu) {
             if (eu.lhs() instanceof ProgramVariable) {
                 toFill.add(term.sub(0));
             }
@@ -255,14 +254,12 @@ protected void collectLocationsFromTerm(Term updateTerm,
                 collectLocationsFromTerm(sub, locationsToFill, updateCreatedObjectsToFill,
                     updateValueObjectsToFill, objectsToIgnore);
             }
-        } else if (updateTerm.op() instanceof ElementaryUpdate) {
-            ElementaryUpdate eu = (ElementaryUpdate) updateTerm.op();
+        } else if (updateTerm.op() instanceof ElementaryUpdate eu) {
             if (SymbolicExecutionUtil.isHeapUpdate(getServices(), updateTerm)) {
                 collectLocationsFromHeapUpdate(updateTerm.sub(0), locationsToFill,
                     updateCreatedObjectsToFill, updateValueObjectsToFill);
-            } else if (eu.lhs() instanceof ProgramVariable) {
+            } else if (eu.lhs() instanceof ProgramVariable var) {
                 final HeapLDT heapLDT = getServices().getTypeConverter().getHeapLDT();
-                ProgramVariable var = (ProgramVariable) eu.lhs();
                 if (!SymbolicExecutionUtil.isHeap(var, heapLDT)) {
                     if (!isImplicitProgramVariable(var)
                             && !objectsToIgnore.contains(getServices().getTermBuilder().var(var))
@@ -1047,8 +1044,7 @@ public String toString() {
          */
         @Override
         public boolean equals(Object obj) {
-            if (obj instanceof ExtractLocationParameter) {
-                ExtractLocationParameter other = (ExtractLocationParameter) obj;
+            if (obj instanceof ExtractLocationParameter other) {
                 return Objects.equals(arrayIndex, other.arrayIndex)
                         && stateMember == other.stateMember
                         && Objects.equals(parentTerm, other.parentTerm)
@@ -1784,8 +1780,7 @@ public Node getGoalNode() {
          */
         @Override
         public boolean equals(Object obj) {
-            if (obj instanceof ExecutionVariableValuePair) {
-                ExecutionVariableValuePair other = (ExecutionVariableValuePair) obj;
+            if (obj instanceof ExecutionVariableValuePair other) {
                 return isArrayRange()
                         ? (getArrayStartIndex().equals(other.getArrayStartIndex())
                                 && getArrayEndIndex().equals(other.getArrayEndIndex()))

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/ExecutionNodeSymbolicLayoutExtractor.java

@@ -25,9 +25,9 @@ public class ExecutionNodeSymbolicLayoutExtractor extends SymbolicLayoutExtracto
      */
     public ExecutionNodeSymbolicLayoutExtractor(IExecutionNode<?> executionNode) {
         super(executionNode.getProofNode(), executionNode.getModalityPIO(),
-            executionNode.getSettings().isUseUnicode(),
-            executionNode.getSettings().isUsePrettyPrinting(),
-            executionNode.getSettings().isSimplifyConditions());
+            executionNode.getSettings().useUnicode(),
+            executionNode.getSettings().usePrettyPrinting(),
+            executionNode.getSettings().simplifyConditions());
         this.executionNode = executionNode;
     }