Upgrade from Java 11 to Java 17

.classpath

@@ -30,7 +30,7 @@ SPDX-License-Identifier: Apache-2.0
 	<classpathentry kind="lib" path="lib/java/test/byte-buddy-agent.jar"/>
 	<classpathentry kind="lib" path="lib/java/runtime/failureaccess.jar"/>
 	<classpathentry kind="lib" path="lib/java/test/jspecify.jar"/>
-	<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-11">
+	<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-17">
 		<attributes>
 			<attribute name="module" value="true"/>
 			<attribute name="limit-modules" value="java.compiler,java.instrument,java.logging,java.management,jdk.unsupported"/>

.gitlab-ci.yml

@@ -12,6 +12,6 @@ variables:
   PROJECT_PATH: "sosy-lab/software/java-common-lib"
   GH_REF: "github.com/sosy-lab/java-common-lib"
   # Version of https://gitlab.com/sosy-lab/software/refaster/ to use
-  REFASTER_REPO_REVISION: 26c8309d1023e4dfcb0e8d24dcf7ec12e621314e
+  REFASTER_REPO_REVISION: 861264bfb12353217b4be5646113d560a04b71ed
   # Needs to be synchronized with Error Prone version in lib/ivy.xml
   REFASTER_VERSION: "2.48.0"

.settings/org.eclipse.jdt.core.prefs

@@ -32,9 +32,9 @@ org.eclipse.jdt.core.compiler.annotation.owning=org.eclipse.jdt.annotation.Ownin
 org.eclipse.jdt.core.compiler.annotation.resourceanalysis=disabled
 org.eclipse.jdt.core.compiler.codegen.inlineJsrBytecode=enabled
 org.eclipse.jdt.core.compiler.codegen.methodParameters=do not generate
-org.eclipse.jdt.core.compiler.codegen.targetPlatform=11
+org.eclipse.jdt.core.compiler.codegen.targetPlatform=17
 org.eclipse.jdt.core.compiler.codegen.unusedLocal=preserve
-org.eclipse.jdt.core.compiler.compliance=11
+org.eclipse.jdt.core.compiler.compliance=17
 org.eclipse.jdt.core.compiler.debug.lineNumber=generate
 org.eclipse.jdt.core.compiler.debug.localVariable=generate
 org.eclipse.jdt.core.compiler.debug.sourceFile=generate
@@ -152,7 +152,7 @@ org.eclipse.jdt.core.compiler.problem.unusedWarningToken=info
 org.eclipse.jdt.core.compiler.problem.varargsArgumentNeedCast=warning
 org.eclipse.jdt.core.compiler.processAnnotations=enabled
 org.eclipse.jdt.core.compiler.release=enabled
-org.eclipse.jdt.core.compiler.source=11
+org.eclipse.jdt.core.compiler.source=17
 org.eclipse.jdt.core.formatter.align_fields_grouping_blank_lines=2147483647
 org.eclipse.jdt.core.formatter.align_type_members_on_columns=false
 org.eclipse.jdt.core.formatter.alignment_for_arguments_in_allocation_expression=48

build/build-compile.xml

@@ -21,7 +21,7 @@ SPDX-License-Identifier: Apache-2.0
     -->
 
     <!-- These properties can be overridden from including file. -->
-    <property name="source.release" value="11"/>
+    <property name="source.release" value="17"/>
     <property name="source.dir" value="src"/>
     <property name="source.generated.dir" value=".apt-generated"/>
     <property name="class.dir" value="bin"/>

build/build-documentation.xml

@@ -60,7 +60,7 @@ SPDX-License-Identifier: Apache-2.0
                 <exclude name="**/*Test.java"/>
                 <exclude name="${documentation.javadoc.exclude}"/>
             </fileset>
-            <link href="https://docs.oracle.com/en/java/javase/11/docs/api/"/>
+            <link href="https://docs.oracle.com/en/java/javase/17/docs/api/"/>
             <link href="https://guava.dev/releases/snapshot/api/docs/"/>
             <link href="https://truth.dev/api/latest/"/>
             <link href="https://sosy-lab.github.io/java-common-lib/api/"/>

build/checkstyle.test.xml

@@ -94,6 +94,7 @@ SPDX-License-Identifier: Apache-2.0
       <property name="allowEmptyConstructors" value="true"/>
       <property name="allowEmptyLoops" value="true"/>
       <property name="allowEmptyMethods" value="true"/>
+      <property name="allowEmptySwitchBlockStatements" value="true"/>
       <property name="allowEmptyTypes" value="true"/>
       <property name="allowEmptyLambdas" value="true"/>
       <property name="ignoreEnhancedForColon" value="false"/>

build/checkstyle.xml

@@ -100,6 +100,7 @@ SPDX-License-Identifier: Apache-2.0
       <property name="allowEmptyConstructors" value="true"/>
       <property name="allowEmptyLoops" value="true"/>
       <property name="allowEmptyMethods" value="true"/>
+      <property name="allowEmptySwitchBlockStatements" value="true"/>
       <property name="allowEmptyTypes" value="true"/>
       <property name="allowEmptyLambdas" value="true"/>
       <property name="ignoreEnhancedForColon" value="false"/>

build/gitlab-ci.yml

@@ -18,7 +18,7 @@ stages:
   - deploy
 
 # Default image for non-JDK-specific jobs
-image: ${CI_REGISTRY_IMAGE}/test:jdk-11
+image: ${CI_REGISTRY_IMAGE}/test:jdk-17
 
 variables:
   IVY_CACHE_DIR: "${CI_PROJECT_DIR}/.ivy2"
@@ -52,10 +52,6 @@ build-dependencies:
       - "bin/"
       - "*.jar"
 
-build:jdk-11:
-  <<: *build
-  image: ${CI_REGISTRY_IMAGE}/test:jdk-11
-
 build:jdk-17:
   <<: *build
   image: ${CI_REGISTRY_IMAGE}/test:jdk-17
@@ -119,7 +115,7 @@ javadoc:
   script: "ant $ANT_PROPS_CHECKS javadoc"
   needs:
     - build-dependencies
-    - build:jdk-11
+    - build:jdk-17
   artifacts:
     paths:
       - "Javadoc/"
@@ -131,7 +127,7 @@ spotbugs:
     - 'test \! -f SpotBugs.html'
   needs:
     - build-dependencies
-    - build:jdk-11
+    - build:jdk-17
   artifacts:
     paths:
       - "SpotBugs.html"
@@ -149,13 +145,6 @@ spotbugs:
     reports:
       junit: "junit/TESTS-TestSuites.xml"
 
-unit-tests:jdk-11:
-  <<: *unit-tests
-  needs:
-    - build-dependencies
-    - build:jdk-11
-  image: ${CI_REGISTRY_IMAGE}/test:jdk-11
-
 unit-tests:jdk-17:
   <<: *unit-tests
   needs:
@@ -221,7 +210,7 @@ deploy-gh-pages:
   stage: deploy
   script: "build/deploy-gh-pages.sh"
   needs:
-    - build:jdk-11
+    - build:jdk-17
     - javadoc
   environment: deploy/gh-pages
   rules:
@@ -252,12 +241,6 @@ deploy-gh-pages:
     - if: $CI_PIPELINE_SOURCE == "schedule"
     - if: $CI_PIPELINE_SOURCE == "web"
 
-build-docker:test:jdk-11:
-  extends: .build-docker
-  variables:
-    DOCKERFILE: build/gitlab-ci.Dockerfile.jdk-11
-    IMAGE: /test:jdk-11
-
 build-docker:test:jdk-17:
   extends: .build-docker
   variables:

lib/ivy.xml

@@ -101,10 +101,7 @@ SPDX-License-Identifier: Apache-2.0
 
         <!-- Eclipse JDT Compiler
              For additional compiler warnings. -->
-        <!-- Newer versions would not work on Java > 11.
-             In the future we can decide to accept this
-             (only affects developers and CI of this project, not users). -->
-        <dependency org="org.eclipse.jdt.core.compiler" name="ecj" rev="4.32-sosy0" conf="build->default"/>
+        <dependency org="org.eclipse.jdt.core.compiler" name="ecj" rev="4.38" conf="build->default"/>
 
         <!-- google-java-format
              A source-code formatter for Java -->

src/org/sosy_lab/common/Appenders.java

@@ -33,8 +33,8 @@ private Appenders() {}
    * @return an {@link Appender} instance
    */
   public static Appender createAppender(@Nullable Object o) {
-    if (o instanceof Appender) {
-      return (Appender) o;
+    if (o instanceof Appender appender) {
+      return appender;
     } else {
       return fromToStringMethod(o);
     }
@@ -50,8 +50,8 @@ public static Appender createAppender(@Nullable Object o) {
    * @throws IOException If the appendable throws an IOException
    */
   public static void appendTo(Appendable output, @Nullable Object o) throws IOException {
-    if (o instanceof Appender) {
-      ((Appender) o).appendTo(output);
+    if (o instanceof Appender appender) {
+      appender.appendTo(output);
     } else {
       output.append(Objects.toString(o));
     }

src/org/sosy_lab/common/Classes.java

@@ -216,9 +216,8 @@ public static <T, X extends Exception> T createInstance(
         Classes.verifyDeclaredExceptions(ct, exceptionType, InvalidConfigurationException.class);
     if (exception != null) {
       throw new InvalidConfigurationException(
-          String.format(
-              "Invalid %s %s, constructor declares unsupported checked exception %s.",
-              typeName, className, exception));
+          "Invalid %s %s, constructor declares unsupported checked exception %s."
+              .formatted(typeName, className, exception));
     }
 
     // instantiate
@@ -227,9 +226,8 @@ public static <T, X extends Exception> T createInstance(
 
     } catch (InstantiationException e) {
       throw new InvalidConfigurationException(
-          String.format(
-              "Invalid %s %s, class cannot be instantiated (%s).",
-              typeName, className, e.getMessage()),
+          "Invalid %s %s, class cannot be instantiated (%s)."
+              .formatted(typeName, className, e.getMessage()),
           e);
 
     } catch (IllegalAccessException e) {
@@ -393,8 +391,7 @@ public static Type getSingleTypeArgument(Type type) {
    */
   public static Type extractUpperBoundFromType(@Var Type type) {
     checkNotNull(type);
-    if (type instanceof WildcardType) {
-      WildcardType wcType = (WildcardType) type;
+    if (type instanceof WildcardType wcType) {
       if (wcType.getLowerBounds().length > 0) {
         throw new UnsupportedOperationException(
             "Currently wildcard types with a lower bound like \"" + type + "\" are not supported ");
@@ -437,7 +434,9 @@ public static void produceClassLoadingWarning(
       pInput -> pInput.getSimpleName().startsWith("AutoValue_");
 
   /** A builder for class loaders with more features than {@link URLClassLoader}. */
-  public abstract static class ClassLoaderBuilder<B extends ClassLoaderBuilder<B>> {
+  public abstract static sealed class ClassLoaderBuilder<B extends ClassLoaderBuilder<B>>
+      permits ExtendedUrlClassLoader.ExtendedUrlClassLoaderConfiguration.AutoBuilder {
+
     ClassLoaderBuilder() {}
 
     /**
@@ -666,16 +665,15 @@ protected Object handleInvocation(Object pProxy, Method pMethod, Object[] pActua
           Object value = parameterMapping[i] == -1 ? null : pActualArgs[parameterMapping[i]];
           if (value == null && !parameterNullability[i]) {
             throw new NullPointerException(
-                String.format(
-                    "Value null for parameter %d of type %s in %s",
-                    i, interfaceMethod.getGenericParameterTypes()[i], this));
+                "Value null for parameter %d of type %s in %s"
+                    .formatted(i, interfaceMethod.getGenericParameterTypes()[i], this));
           }
           targetArgs[i] = value;
         }
 
         try {
-          if (target instanceof Method) {
-            return ((Method) target).invoke(null, targetArgs);
+          if (target instanceof Method method) {
+            return method.invoke(null, targetArgs);
           } else if (target instanceof Constructor<?>) {
             return ((Constructor<?>) target).newInstance(targetArgs);
           } else {
@@ -730,8 +728,8 @@ private static Executable getInstantiationMethodForClass(Class<?> cls)
             .filter(m -> Modifier.isPublic(m.getModifiers()))
             .filter(m -> !m.isSynthetic())
             .collect(toImmutableList());
-    switch (factoryMethods.size()) {
-      case 0:
+    return switch (factoryMethods.size()) {
+      case 0 -> {
         if (Modifier.isAbstract(cls.getModifiers())) {
           throw new UnsuitedClassException("class is abstract");
         }
@@ -740,14 +738,14 @@ private static Executable getInstantiationMethodForClass(Class<?> cls)
           throw new UnsuitedClassException(
               "class does not have a static method \"create\" nor exactly one public constructor");
         }
-        return constructors[0];
-
-      case 1:
-        return factoryMethods.get(0);
+        yield constructors[0];
+      }
+      case 1 -> factoryMethods.get(0);
 
-      default:
-        throw new UnsuitedClassException("class has more than one static methods named \"create\"");
-    }
+      default ->
+          throw new UnsuitedClassException(
+              "class has more than one static methods named \"create\"");
+    };
   }
 
   /**
@@ -760,7 +758,7 @@ public static final class UnsuitedClassException extends Exception {
 
     @FormatMethod
     UnsuitedClassException(String msg, Object... args) {
-      super(String.format(msg, args));
+      super(msg.formatted(args));
     }
   }
 }

src/org/sosy_lab/common/ExtendedUrlClassLoader.java

@@ -13,7 +13,6 @@
 import com.google.auto.value.AutoValue;
 import com.google.common.collect.ImmutableList;
 import com.google.errorprone.annotations.Var;
-import edu.umd.cs.findbugs.annotations.SuppressFBWarnings;
 import java.net.URL;
 import java.net.URLClassLoader;
 import java.nio.file.Path;
@@ -38,7 +37,9 @@ private ExtendedUrlClassLoader(ExtendedUrlClassLoaderConfiguration pConfig) {
 
   @AutoValue
   @SuppressWarnings("NoFunctionalReturnType")
-  abstract static class ExtendedUrlClassLoaderConfiguration {
+  abstract static sealed class ExtendedUrlClassLoaderConfiguration
+      permits AutoValue_ExtendedUrlClassLoader_ExtendedUrlClassLoaderConfiguration {
+
     abstract Optional<ClassLoader> parent();
 
     abstract ImmutableList<URL> urls();
@@ -52,10 +53,11 @@ static AutoBuilder builder() {
     }
 
     @AutoValue.Builder
-    abstract static class AutoBuilder extends Classes.ClassLoaderBuilder<AutoBuilder> {
+    abstract static sealed class AutoBuilder extends Classes.ClassLoaderBuilder<AutoBuilder>
+        permits AutoValue_ExtendedUrlClassLoader_ExtendedUrlClassLoaderConfiguration.Builder {
+
       AutoBuilder() {}
 
-      @SuppressFBWarnings("DP_CREATE_CLASSLOADER_INSIDE_DO_PRIVILEGED")
       @Override
       public final URLClassLoader build() {
         return new ExtendedUrlClassLoader(autoBuild());