From da795f1729c8d6bbe19c7de1ffc50e23c0eb2f1d Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Mon, 9 Mar 2026 15:33:15 +0100 Subject: [PATCH 01/11] Require Java 17 All known users of this library also require Java 17 anyway. --- .classpath | 2 +- .idea/SoSy-Lab Common.iml | 2 +- .idea/misc.xml | 2 +- .settings/org.eclipse.jdt.core.prefs | 6 ++--- build.xml | 4 +++ build/build-compile.xml | 2 +- build/build-documentation.xml | 2 +- build/checkstyle.test.xml | 1 + build/checkstyle.xml | 1 + build/gitlab-ci.Dockerfile.jdk-11 | 17 ------------- build/gitlab-ci.yml | 25 +++---------------- lib/ivy.xml | 5 +--- .../common/ExtendedUrlClassLoader.java | 2 -- 13 files changed, 19 insertions(+), 52 deletions(-) delete mode 100644 build/gitlab-ci.Dockerfile.jdk-11 diff --git a/.classpath b/.classpath index a3304af74..796c9ddcf 100644 --- a/.classpath +++ b/.classpath @@ -30,7 +30,7 @@ SPDX-License-Identifier: Apache-2.0 - + diff --git a/.idea/SoSy-Lab Common.iml b/.idea/SoSy-Lab Common.iml index 7f1d61380..92837f6a2 100644 --- a/.idea/SoSy-Lab Common.iml +++ b/.idea/SoSy-Lab Common.iml @@ -28,7 +28,7 @@ SPDX-License-Identifier: Apache-2.0 - + diff --git a/.idea/misc.xml b/.idea/misc.xml index 6a821144a..1ccfc5516 100644 --- a/.idea/misc.xml +++ b/.idea/misc.xml @@ -50,7 +50,7 @@ SPDX-License-Identifier: Apache-2.0 - + diff --git a/.settings/org.eclipse.jdt.core.prefs b/.settings/org.eclipse.jdt.core.prefs index e1a676ce1..45b8b481f 100644 --- a/.settings/org.eclipse.jdt.core.prefs +++ b/.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 diff --git a/build.xml b/build.xml index d75417964..4e12d31a8 100644 --- a/build.xml +++ b/build.xml @@ -39,6 +39,8 @@ SPDX-License-Identifier: Apache-2.0 - DefaultLocale: TODO: think about whether we want it - AddNullMarkedToPackageInfo: TODO: use JSpecify and apply nullability everywhere - AddNullMarkedToClass: We prefer the annotations in package-info.java + - PatternMatchingInstanceof: TODO + - StatementSwitchToExpressionSwitch: TODO --> diff --git a/build/build-compile.xml b/build/build-compile.xml index cc23beecd..e6a7a21a9 100644 --- a/build/build-compile.xml +++ b/build/build-compile.xml @@ -21,7 +21,7 @@ SPDX-License-Identifier: Apache-2.0 --> - + diff --git a/build/build-documentation.xml b/build/build-documentation.xml index 3be66c3ba..4876c04c6 100644 --- a/build/build-documentation.xml +++ b/build/build-documentation.xml @@ -60,7 +60,7 @@ SPDX-License-Identifier: Apache-2.0 - + diff --git a/build/checkstyle.test.xml b/build/checkstyle.test.xml index a65c94485..2bb9c0116 100644 --- a/build/checkstyle.test.xml +++ b/build/checkstyle.test.xml @@ -94,6 +94,7 @@ SPDX-License-Identifier: Apache-2.0 + diff --git a/build/checkstyle.xml b/build/checkstyle.xml index e3304f22b..a79e4cc59 100644 --- a/build/checkstyle.xml +++ b/build/checkstyle.xml @@ -100,6 +100,7 @@ SPDX-License-Identifier: Apache-2.0 + diff --git a/build/gitlab-ci.Dockerfile.jdk-11 b/build/gitlab-ci.Dockerfile.jdk-11 deleted file mode 100644 index bff0c128c..000000000 --- a/build/gitlab-ci.Dockerfile.jdk-11 +++ /dev/null @@ -1,17 +0,0 @@ -# This file is part of SoSy-Lab Common, -# a library of useful utilities: -# https://github.com/sosy-lab/java-common-lib -# -# SPDX-FileCopyrightText: 2007-2020 Dirk Beyer -# -# SPDX-License-Identifier: Apache-2.0 - -# This is a container image for running the tests. -# It should be pushed to registry.gitlab.com/sosy-lab/software/java-common-lib/test -# and will be used by CI as declared in .gitlab-ci.yml. -# -# Commands for updating the image: -# podman build --pull -t registry.gitlab.com/sosy-lab/software/java-common-lib/test:jdk-11 - < build/gitlab-ci.Dockerfile.jdk-11 -# podman push registry.gitlab.com/sosy-lab/software/java-common-lib/test:jdk-11 - -FROM registry.gitlab.com/sosy-lab/software/java-project-template/test:jdk-11 diff --git a/build/gitlab-ci.yml b/build/gitlab-ci.yml index 5cec552e1..471207259 100644 --- a/build/gitlab-ci.yml +++ b/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: diff --git a/lib/ivy.xml b/lib/ivy.xml index e2cd539a4..a1fca11c5 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -101,10 +101,7 @@ SPDX-License-Identifier: Apache-2.0 - - + diff --git a/src/org/sosy_lab/common/ExtendedUrlClassLoader.java b/src/org/sosy_lab/common/ExtendedUrlClassLoader.java index 5f01670a0..e715a14e4 100644 --- a/src/org/sosy_lab/common/ExtendedUrlClassLoader.java +++ b/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; @@ -55,7 +54,6 @@ static AutoBuilder builder() { abstract static class AutoBuilder extends Classes.ClassLoaderBuilder { AutoBuilder() {} - @SuppressFBWarnings("DP_CREATE_CLASSLOADER_INSIDE_DO_PRIVILEGED") @Override public final URLClassLoader build() { return new ExtendedUrlClassLoader(autoBuild()); From 16f12b64797d8f5ec1fd4e7881c9f879948fe182 Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Mon, 9 Mar 2026 16:07:28 +0100 Subject: [PATCH 02/11] Use pattern-matching instanceof Commit generated automatically with Google Error Prone. --- build.xml | 2 -- src/org/sosy_lab/common/Appenders.java | 8 ++++---- src/org/sosy_lab/common/Classes.java | 4 ++-- src/org/sosy_lab/common/JSON.java | 12 ++++++------ .../sosy_lab/common/configuration/Configuration.java | 4 ++-- .../configuration/converters/ClassTypeConverter.java | 6 ++---- .../converters/IntegerTypeConverter.java | 3 +-- .../converters/TimeSpanTypeConverter.java | 3 +-- src/org/sosy_lab/common/log/BasicLogManager.java | 8 ++++---- src/org/sosy_lab/common/log/ConsoleLogFormatter.java | 4 ++-- .../sosy_lab/common/log/TimestampedLogFormatter.java | 4 ++-- src/org/sosy_lab/common/time/TimeSpan.java | 4 ++-- 12 files changed, 28 insertions(+), 34 deletions(-) diff --git a/build.xml b/build.xml index 4e12d31a8..0efd10337 100644 --- a/build.xml +++ b/build.xml @@ -39,7 +39,6 @@ SPDX-License-Identifier: Apache-2.0 - DefaultLocale: TODO: think about whether we want it - AddNullMarkedToPackageInfo: TODO: use JSpecify and apply nullability everywhere - AddNullMarkedToClass: We prefer the annotations in package-info.java - - PatternMatchingInstanceof: TODO - StatementSwitchToExpressionSwitch: TODO --> diff --git a/src/org/sosy_lab/common/Appenders.java b/src/org/sosy_lab/common/Appenders.java index d39e9c847..8d0eae381 100644 --- a/src/org/sosy_lab/common/Appenders.java +++ b/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)); } diff --git a/src/org/sosy_lab/common/Classes.java b/src/org/sosy_lab/common/Classes.java index 0e9636a61..719a1ca33 100644 --- a/src/org/sosy_lab/common/Classes.java +++ b/src/org/sosy_lab/common/Classes.java @@ -674,8 +674,8 @@ protected Object handleInvocation(Object pProxy, Method pMethod, Object[] pActua } 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 { diff --git a/src/org/sosy_lab/common/JSON.java b/src/org/sosy_lab/common/JSON.java index 930b0f562..72a50cd22 100644 --- a/src/org/sosy_lab/common/JSON.java +++ b/src/org/sosy_lab/common/JSON.java @@ -45,20 +45,20 @@ public static void writeJSONString(@Nullable Object value, Appendable out) throw if (value == null) { out.append("null"); - } else if (value instanceof CharSequence) { + } else if (value instanceof CharSequence charSequence) { out.append('\"'); - escape((CharSequence) value, out); + escape(charSequence, out); out.append('\"'); - } else if (value instanceof Double) { - if (((Double) value).isInfinite() || ((Double) value).isNaN()) { + } else if (value instanceof Double d) { + if (d.isInfinite() || d.isNaN()) { out.append("null"); } else { out.append(value.toString()); } - } else if (value instanceof Float) { - if (((Float) value).isInfinite() || ((Float) value).isNaN()) { + } else if (value instanceof Float f) { + if (f.isInfinite() || f.isNaN()) { out.append("null"); } else { out.append(value.toString()); diff --git a/src/org/sosy_lab/common/configuration/Configuration.java b/src/org/sosy_lab/common/configuration/Configuration.java index 2909b876f..dcaa2b009 100644 --- a/src/org/sosy_lab/common/configuration/Configuration.java +++ b/src/org/sosy_lab/common/configuration/Configuration.java @@ -928,8 +928,8 @@ private void printOptionInfos( if (defaultValue != null) { String defaultStr; - if (defaultValue instanceof Object[]) { - defaultStr = Arrays.deepToString((Object[]) defaultValue); + if (defaultValue instanceof Object[] array) { + defaultStr = Arrays.deepToString(array); } else { defaultStr = defaultValue.toString(); } diff --git a/src/org/sosy_lab/common/configuration/converters/ClassTypeConverter.java b/src/org/sosy_lab/common/configuration/converters/ClassTypeConverter.java index cf00d1b59..7b52dcfbc 100644 --- a/src/org/sosy_lab/common/configuration/converters/ClassTypeConverter.java +++ b/src/org/sosy_lab/common/configuration/converters/ClassTypeConverter.java @@ -37,13 +37,11 @@ public Object convert( // get optional package prefix if (secondaryOption != null) { - if (!(secondaryOption instanceof ClassOption)) { + if (!(secondaryOption instanceof ClassOption classOption)) { throw new UnsupportedOperationException( "Options of type Class may not be annotated with " + secondaryOption); } - packagePrefixes = - FluentIterable.from(packagePrefixes) - .append(((ClassOption) secondaryOption).packagePrefix()); + packagePrefixes = FluentIterable.from(packagePrefixes).append(classOption.packagePrefix()); } // get class object diff --git a/src/org/sosy_lab/common/configuration/converters/IntegerTypeConverter.java b/src/org/sosy_lab/common/configuration/converters/IntegerTypeConverter.java index bd341b2c7..5c95d224b 100644 --- a/src/org/sosy_lab/common/configuration/converters/IntegerTypeConverter.java +++ b/src/org/sosy_lab/common/configuration/converters/IntegerTypeConverter.java @@ -33,11 +33,10 @@ public Object convert( throws InvalidConfigurationException { Class type = pType.getRawType(); - if (!(pOption instanceof IntegerOption)) { + if (!(pOption instanceof IntegerOption option)) { throw new UnsupportedOperationException( "IntegerTypeConverter needs options annotated with @IntegerOption"); } - IntegerOption option = (IntegerOption) pOption; assert type.equals(Integer.class) || type.equals(Long.class); diff --git a/src/org/sosy_lab/common/configuration/converters/TimeSpanTypeConverter.java b/src/org/sosy_lab/common/configuration/converters/TimeSpanTypeConverter.java index 295af3edb..bd382879f 100644 --- a/src/org/sosy_lab/common/configuration/converters/TimeSpanTypeConverter.java +++ b/src/org/sosy_lab/common/configuration/converters/TimeSpanTypeConverter.java @@ -45,11 +45,10 @@ public Object convert( throws InvalidConfigurationException { Class type = pType.getRawType(); - if (!(pOption instanceof TimeSpanOption)) { + if (!(pOption instanceof TimeSpanOption option)) { throw new UnsupportedOperationException( "Time span options need to be annotated with @TimeSpanOption"); } - TimeSpanOption option = (TimeSpanOption) pOption; // find unit in input string @Var int i = valueStr.length() - 1; diff --git a/src/org/sosy_lab/common/log/BasicLogManager.java b/src/org/sosy_lab/common/log/BasicLogManager.java index 34ada676c..dea8d9387 100644 --- a/src/org/sosy_lab/common/log/BasicLogManager.java +++ b/src/org/sosy_lab/common/log/BasicLogManager.java @@ -415,8 +415,8 @@ private String buildAdditionalMessageText(Object... args) { for (int i = 0; i < args.length; i++) { Object o = Objects.requireNonNullElse(args[i], "null"); @Var String arg; - if (o instanceof Appender && truncateSize > 0) { - arg = Appenders.toStringWithTruncation((Appender) o, truncateSize + 1); + if (o instanceof Appender appender && truncateSize > 0) { + arg = Appenders.toStringWithTruncation(appender, truncateSize + 1); } else { arg = o.toString(); } @@ -531,9 +531,9 @@ private static StringBuilder buildUserExceptionLogMessage( } CharSequence exceptionMessage = - e instanceof FileSystemException + e instanceof FileSystemException fileSystemException ? createFileSystemExceptionMessage( - (FileSystemException) e, /* asSuffix= */ additionalMessage.endsWith("file")) + fileSystemException, /* asSuffix= */ additionalMessage.endsWith("file")) : Strings.nullToEmpty(e.getMessage()); if (additionalMessage.isEmpty()) { diff --git a/src/org/sosy_lab/common/log/ConsoleLogFormatter.java b/src/org/sosy_lab/common/log/ConsoleLogFormatter.java index 95cdfb123..23f231fb4 100644 --- a/src/org/sosy_lab/common/log/ConsoleLogFormatter.java +++ b/src/org/sosy_lab/common/log/ConsoleLogFormatter.java @@ -34,8 +34,8 @@ public static Formatter withColorsIfPossible() { @Override protected void format(LogRecord lr, StringBuilder sb) { sb.append(lr.getMessage()).append(" ("); - if (lr instanceof ExtendedLogRecord) { - String component = ((ExtendedLogRecord) lr).getSourceComponentName(); + if (lr instanceof ExtendedLogRecord extendedLogRecord) { + String component = extendedLogRecord.getSourceComponentName(); if (!component.isEmpty()) { sb.append(component).append(':'); } diff --git a/src/org/sosy_lab/common/log/TimestampedLogFormatter.java b/src/org/sosy_lab/common/log/TimestampedLogFormatter.java index 06252a856..6657d9a0e 100644 --- a/src/org/sosy_lab/common/log/TimestampedLogFormatter.java +++ b/src/org/sosy_lab/common/log/TimestampedLogFormatter.java @@ -39,8 +39,8 @@ public void format(LogRecord lr, StringBuilder sb) { DATE_FORMAT.formatTo(lr.getInstant(), sb); sb.append('\t').append(lr.getLevel()).append('\t'); - if (lr instanceof ExtendedLogRecord) { - String component = ((ExtendedLogRecord) lr).getSourceComponentName(); + if (lr instanceof ExtendedLogRecord extendedLogRecord) { + String component = extendedLogRecord.getSourceComponentName(); if (!component.isEmpty()) { sb.append(component).append(':'); } diff --git a/src/org/sosy_lab/common/time/TimeSpan.java b/src/org/sosy_lab/common/time/TimeSpan.java index e030236d7..641c4da71 100644 --- a/src/org/sosy_lab/common/time/TimeSpan.java +++ b/src/org/sosy_lab/common/time/TimeSpan.java @@ -396,10 +396,10 @@ public boolean equals(@Nullable Object obj) { if (obj == this) { return true; } - if (!(obj instanceof TimeSpan)) { + if (!(obj instanceof TimeSpan other)) { return false; } - TimeSpan other = (TimeSpan) obj; + if (unit == other.unit) { return span == other.span; } From 30cfaf1c00696bb7fb2cd5be49366062795397ca Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Mon, 9 Mar 2026 16:18:55 +0100 Subject: [PATCH 03/11] Use pattern-matching instanceof Commit generated automatically with Eclipse. --- src/org/sosy_lab/common/Classes.java | 3 +-- .../sosy_lab/common/collect/PathCopyingPersistentTreeMap.java | 3 +-- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/src/org/sosy_lab/common/Classes.java b/src/org/sosy_lab/common/Classes.java index 719a1ca33..2b8decf20 100644 --- a/src/org/sosy_lab/common/Classes.java +++ b/src/org/sosy_lab/common/Classes.java @@ -393,8 +393,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 "); diff --git a/src/org/sosy_lab/common/collect/PathCopyingPersistentTreeMap.java b/src/org/sosy_lab/common/collect/PathCopyingPersistentTreeMap.java index 82d7418a8..349b1f47a 100644 --- a/src/org/sosy_lab/common/collect/PathCopyingPersistentTreeMap.java +++ b/src/org/sosy_lab/common/collect/PathCopyingPersistentTreeMap.java @@ -1355,8 +1355,7 @@ public Iterator> descendingEntryIterator() { @Override @SuppressWarnings("ReferenceEquality") // comparing nodes with equals would not suffice public boolean equals(@Nullable Object pObj) { - if (pObj instanceof PartialSortedMap) { - PartialSortedMap other = (PartialSortedMap) pObj; + if (pObj instanceof PartialSortedMap other) { if (root == other.root && Objects.equals(fromKey, other.fromKey) && fromInclusive == other.fromInclusive From ee3c558baeabbaa1c9d3d5e4411273428132cca8 Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Tue, 10 Mar 2026 07:41:40 +0100 Subject: [PATCH 04/11] Use switch expression in assignments/return statements Manually refactored. --- src/org/sosy_lab/common/Classes.java | 18 +++++------ .../common/rationals/ExtendedRational.java | 31 +++++++++---------- 2 files changed, 23 insertions(+), 26 deletions(-) diff --git a/src/org/sosy_lab/common/Classes.java b/src/org/sosy_lab/common/Classes.java index 2b8decf20..443fe9be7 100644 --- a/src/org/sosy_lab/common/Classes.java +++ b/src/org/sosy_lab/common/Classes.java @@ -729,8 +729,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"); } @@ -739,14 +739,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\""); + }; } /** diff --git a/src/org/sosy_lab/common/rationals/ExtendedRational.java b/src/org/sosy_lab/common/rationals/ExtendedRational.java index 3d14d17ff..6a5c6a6d7 100644 --- a/src/org/sosy_lab/common/rationals/ExtendedRational.java +++ b/src/org/sosy_lab/common/rationals/ExtendedRational.java @@ -77,18 +77,15 @@ private ExtendedRational(NumberType pType) { *

The method works, because the Java Double class also supports Infinity/-Infinity/NaN. */ public double toDouble() { - switch (numberType) { - case NEG_INFTY: - return Double.NEGATIVE_INFINITY; - case RATIONAL: + return switch (numberType) { + case NEG_INFTY -> Double.NEGATIVE_INFINITY; + case RATIONAL -> { assert rational != null; - return rational.doubleValue(); - case INFTY: - return Double.POSITIVE_INFINITY; - case NaN: - return Double.NaN; - } - throw new UnsupportedOperationException("Unexpected number type"); + yield rational.doubleValue(); + } + case INFTY -> Double.POSITIVE_INFINITY; + case NaN -> Double.NaN; + }; } /** @@ -97,13 +94,13 @@ public double toDouble() { */ @Override public String toString() { - switch (numberType) { - case RATIONAL: + return switch (numberType) { + case RATIONAL -> { assert rational != null; - return rational.toString(); - default: - return Double.toString(toDouble()); - } + yield rational.toString(); + } + default -> Double.toString(toDouble()); + }; } /** From 9928d756193f6264b2e03e47195f5734c8424bb2 Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Mon, 9 Mar 2026 16:10:09 +0100 Subject: [PATCH 05/11] Use switch expression in assignments/return statements Commit generated automatically with Google Error Prone. --- src/org/sosy_lab/common/NativeLibraries.java | 28 ++++++++----------- .../common/rationals/ExtendedRational.java | 16 ++++------- src/org/sosy_lab/common/time/TimeSpan.java | 16 ++++------- src/org/sosy_lab/common/time/Timer.java | 28 ++++++------------- 4 files changed, 32 insertions(+), 56 deletions(-) diff --git a/src/org/sosy_lab/common/NativeLibraries.java b/src/org/sosy_lab/common/NativeLibraries.java index 60d32f6d0..633208430 100644 --- a/src/org/sosy_lab/common/NativeLibraries.java +++ b/src/org/sosy_lab/common/NativeLibraries.java @@ -152,23 +152,17 @@ private static Architecture guessOsArchitecture() { osArch = Ascii.toLowerCase(osArch.replace(" ", "")); - switch (osArch) { - case "i386": - case "i686": - case "x86": - return Architecture.X86; - case "amd64": - case "x86_64": - return Architecture.X86_64; - case "aarch64": - return Architecture.ARM64; - default: - throw new UnsatisfiedLinkError( - "Unknown value for os.arch: '" - + StandardSystemProperty.OS_ARCH.value() - + "'" - + REPORT_MESSAGE); - } + return switch (osArch) { + case "i386", "i686", "x86" -> Architecture.X86; + case "amd64", "x86_64" -> Architecture.X86_64; + case "aarch64" -> Architecture.ARM64; + default -> + throw new UnsatisfiedLinkError( + "Unknown value for os.arch: '" + + StandardSystemProperty.OS_ARCH.value() + + "'" + + REPORT_MESSAGE); + }; } /** Check whether the JVM is executing in 32 bit version. */ diff --git a/src/org/sosy_lab/common/rationals/ExtendedRational.java b/src/org/sosy_lab/common/rationals/ExtendedRational.java index 6a5c6a6d7..cf9ced016 100644 --- a/src/org/sosy_lab/common/rationals/ExtendedRational.java +++ b/src/org/sosy_lab/common/rationals/ExtendedRational.java @@ -120,16 +120,12 @@ public String toString() { * @return New {@link ExtendedRational}. */ public static ExtendedRational ofString(String s) { - switch (s) { - case "Infinity": - return ExtendedRational.INFTY; - case "-Infinity": - return ExtendedRational.NEG_INFTY; - case "NaN": - return ExtendedRational.NaN; - default: - return new ExtendedRational(Rational.ofString(s)); - } + return switch (s) { + case "Infinity" -> ExtendedRational.INFTY; + case "-Infinity" -> ExtendedRational.NEG_INFTY; + case "NaN" -> ExtendedRational.NaN; + default -> new ExtendedRational(Rational.ofString(s)); + }; } @Override diff --git a/src/org/sosy_lab/common/time/TimeSpan.java b/src/org/sosy_lab/common/time/TimeSpan.java index 641c4da71..a3f530adc 100644 --- a/src/org/sosy_lab/common/time/TimeSpan.java +++ b/src/org/sosy_lab/common/time/TimeSpan.java @@ -656,15 +656,11 @@ String formatHumanReadableLarge() { static { String format = Ascii.toUpperCase(System.getProperty(DEFAULT_FORMAT_PROPERTY_NAME, "SIMPLE").trim()); - switch (format) { - case "HUMAN_READABLE_LARGE": - DEFAULT_FORMAT = TimeSpan::formatHumanReadableLarge; - break; - case "SIMPLE": - DEFAULT_FORMAT = TimeSpan::formatSimple; - break; - default: - DEFAULT_FORMAT = TimeSpan::formatSimple; - } + DEFAULT_FORMAT = + switch (format) { + case "HUMAN_READABLE_LARGE" -> TimeSpan::formatHumanReadableLarge; + case "SIMPLE" -> TimeSpan::formatSimple; + default -> TimeSpan::formatSimple; + }; } } diff --git a/src/org/sosy_lab/common/time/Timer.java b/src/org/sosy_lab/common/time/Timer.java index 6d841ba6a..36f7d211c 100644 --- a/src/org/sosy_lab/common/time/Timer.java +++ b/src/org/sosy_lab/common/time/Timer.java @@ -39,25 +39,15 @@ public final class Timer { String clockToUse = Ascii.toUpperCase( System.getProperty(DEFAULT_CLOCK_PROPERTY_NAME, "WALLTIME_MILLIS").trim()); - switch (clockToUse) { - case "WALLTIME_MILLIS": - DEFAULT_CLOCK = Tickers.getWalltimeMillis(); - break; - case "WALLTIME_NANOS": - DEFAULT_CLOCK = Tickers.getWalltimeNanos(); - break; - case "THREAD_CPUTIME": - DEFAULT_CLOCK = Tickers.getCurrentThreadCputime(); - break; - case "PROCESS_CPUTIME": - DEFAULT_CLOCK = Tickers.getProcessCputime(); - break; - case "NONE": - DEFAULT_CLOCK = Tickers.getNullTicker(); - break; - default: - DEFAULT_CLOCK = null; - } + DEFAULT_CLOCK = + switch (clockToUse) { + case "WALLTIME_MILLIS" -> Tickers.getWalltimeMillis(); + case "WALLTIME_NANOS" -> Tickers.getWalltimeNanos(); + case "THREAD_CPUTIME" -> Tickers.getCurrentThreadCputime(); + case "PROCESS_CPUTIME" -> Tickers.getProcessCputime(); + case "NONE" -> Tickers.getNullTicker(); + default -> null; + }; } // Visible for NestedTimer From 42b562badbd63df7127125fc07dda652ed9e9e4e Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Tue, 10 Mar 2026 07:41:07 +0100 Subject: [PATCH 06/11] Rewrite classic switch labels into arrow rules Commit generated automatically with Google Error Prone. --- build.xml | 2 -- src/org/sosy_lab/common/JSON.java | 35 ++++++------------- .../OptionAnnotationProcessor.java | 34 +++++++++--------- .../common/configuration/OptionCollector.java | 12 +++---- .../converters/FileTypeConverter.java | 12 ++----- src/org/sosy_lab/common/time/TimeSpan.java | 28 +++++---------- 6 files changed, 43 insertions(+), 80 deletions(-) diff --git a/build.xml b/build.xml index 0efd10337..d75417964 100644 --- a/build.xml +++ b/build.xml @@ -39,7 +39,6 @@ SPDX-License-Identifier: Apache-2.0 - DefaultLocale: TODO: think about whether we want it - AddNullMarkedToPackageInfo: TODO: use JSpecify and apply nullability everywhere - AddNullMarkedToClass: We prefer the annotations in package-info.java - - StatementSwitchToExpressionSwitch: TODO --> diff --git a/src/org/sosy_lab/common/JSON.java b/src/org/sosy_lab/common/JSON.java index 72a50cd22..ee53aed87 100644 --- a/src/org/sosy_lab/common/JSON.java +++ b/src/org/sosy_lab/common/JSON.java @@ -127,31 +127,15 @@ private static void escape(CharSequence s, Appendable out) throws IOException { for (int i = 0; i < s.length(); i++) { char ch = s.charAt(i); switch (ch) { - case '"': - out.append("\\\""); - break; - case '\\': - out.append("\\\\"); - break; - case '\b': - out.append("\\b"); - break; - case '\f': - out.append("\\f"); - break; - case '\n': - out.append("\\n"); - break; - case '\r': - out.append("\\r"); - break; - case '\t': - out.append("\\t"); - break; - case '/': - out.append("\\/"); - break; - default: + case '"' -> out.append("\\\""); + case '\\' -> out.append("\\\\"); + case '\b' -> out.append("\\b"); + case '\f' -> out.append("\\f"); + case '\n' -> out.append("\\n"); + case '\r' -> out.append("\\r"); + case '\t' -> out.append("\\t"); + case '/' -> out.append("\\/"); + default -> { // Reference: http://www.unicode.org/versions/Unicode5.1.0/ if ((ch <= '\u001F') || (ch >= '\u007F' && ch <= '\u009F') @@ -162,6 +146,7 @@ private static void escape(CharSequence s, Appendable out) throws IOException { } else { out.append(ch); } + } } } } diff --git a/src/org/sosy_lab/common/configuration/OptionAnnotationProcessor.java b/src/org/sosy_lab/common/configuration/OptionAnnotationProcessor.java index edc14e2f1..8005c2daf 100644 --- a/src/org/sosy_lab/common/configuration/OptionAnnotationProcessor.java +++ b/src/org/sosy_lab/common/configuration/OptionAnnotationProcessor.java @@ -235,7 +235,7 @@ private void processOption(Element elem) { } switch (elem.getKind()) { - case FIELD: + case FIELD -> { if (elem.getModifiers().contains(Modifier.FINAL)) { message( ERROR, @@ -243,8 +243,8 @@ private void processOption(Element elem) { "Modifier final on field annotated with @Option is illegal," + " as it will be written via reflection."); } - break; - case METHOD: + } + case METHOD -> { // check signature (parameter count, declared exceptions) ExecutableElement method = (ExecutableElement) elem; if (method.getParameters().size() != 1) { @@ -263,13 +263,13 @@ private void processOption(Element elem) { "Methods annotated with @Option may not throw " + exceptionType + "."); } } - break; - default: - message( - ERROR, - elem, - Option.class, - "Annotation @Option is only allowed for fields and methods."); + } + default -> + message( + ERROR, + elem, + Option.class, + "Annotation @Option is only allowed for fields and methods."); } if (elem.getModifiers().contains(Modifier.STATIC)) { @@ -322,18 +322,18 @@ private void checkOptionDetailAnnotations(Element elem) { // Determine type of option as declared in source. @Var TypeMirror optionType; switch (elem.getKind()) { - case FIELD: - optionType = elem.asType(); - break; - case METHOD: + case FIELD -> optionType = elem.asType(); + case METHOD -> { ExecutableElement method = (ExecutableElement) elem; if (method.getParameters().size() != 1) { continue; // error, already reported above } optionType = method.getParameters().get(0).asType(); - break; - default: - continue; // error, prevented by compiler + } + default -> { + continue; + // error, prevented by compiler + } } // If this option is an array or a collection, get the component type. diff --git a/src/org/sosy_lab/common/configuration/OptionCollector.java b/src/org/sosy_lab/common/configuration/OptionCollector.java index 73b4f194f..9ee371625 100644 --- a/src/org/sosy_lab/common/configuration/OptionCollector.java +++ b/src/org/sosy_lab/common/configuration/OptionCollector.java @@ -88,16 +88,12 @@ public static void main(String[] args) { @Var boolean includeLibraryOptions = false; for (String arg : args) { switch (arg) { - case "-v": - case "-verbose": - verbose = true; - break; - case "-includeLibraryOptions": - includeLibraryOptions = true; - break; - default: + case "-v", "-verbose" -> verbose = true; + case "-includeLibraryOptions" -> includeLibraryOptions = true; + default -> { System.err.println("Unexpected command-line argument: " + arg); System.exit(1); + } } } diff --git a/src/org/sosy_lab/common/configuration/converters/FileTypeConverter.java b/src/org/sosy_lab/common/configuration/converters/FileTypeConverter.java index 93ad47f84..3fb312702 100644 --- a/src/org/sosy_lab/common/configuration/converters/FileTypeConverter.java +++ b/src/org/sosy_lab/common/configuration/converters/FileTypeConverter.java @@ -161,15 +161,9 @@ Path checkSafePath(Path pPath, String optionName) throws InvalidConfigurationExc @Var int depth = 0; for (String component : Splitter.on(File.separator).split(path)) { switch (component) { - case "": - case ".": - break; - case "..": - depth--; - break; - default: - depth++; - break; + case "", "." -> {} + case ".." -> depth--; + default -> depth++; } if (depth < 0) { diff --git a/src/org/sosy_lab/common/time/TimeSpan.java b/src/org/sosy_lab/common/time/TimeSpan.java index a3f530adc..f0e55e258 100644 --- a/src/org/sosy_lab/common/time/TimeSpan.java +++ b/src/org/sosy_lab/common/time/TimeSpan.java @@ -157,41 +157,31 @@ public static TimeSpan valueOf(String input) { String unit = it.next(); switch (unit) { - case "day": - case "days": - case "d": + case "day", "days", "d" -> { if (days != 0) { throw new IllegalArgumentException("Days set twice: " + unit); } days = value; - break; - - case "h": - case "hour": - case "hours": + } + case "h", "hour", "hours" -> { if (hours != 0) { throw new IllegalArgumentException("Hours set twice: " + unit); } hours = value; - break; - - case "min": - case "m": + } + case "min", "m" -> { if (minutes != 0) { throw new IllegalArgumentException("Minutes set twice: " + unit); } minutes = value; - break; - - case "s": + } + case "s" -> { if (seconds != 0) { throw new IllegalArgumentException("Seconds set twice: " + unit); } seconds = value; - break; - - default: - throw new IllegalArgumentException("Unknown unit: " + unit); + } + default -> throw new IllegalArgumentException("Unknown unit: " + unit); } } From 835c587ab80d9798ab46ccc02f9382156e39fd6a Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Tue, 10 Mar 2026 09:13:27 +0100 Subject: [PATCH 07/11] Apply Refaster rule for using String.formatted There were only two cases where https://github.com/google/error-prone/issues/4866 could be a problem, these were checked and handled manually. Any other instances of that bug would be detected by Error Prone, which checks the number of format arguments. --- .gitlab-ci.yml | 2 +- src/org/sosy_lab/common/Classes.java | 17 +++++++--------- src/org/sosy_lab/common/ProcessExecutor.java | 6 +++--- .../common/collect/PersistentSortedMaps.java | 4 ++-- .../common/configuration/Configuration.java | 20 +++++++++---------- .../OptionAnnotationProcessor.java | 9 ++++++--- .../common/configuration/OptionCollector.java | 5 ++--- .../converters/BaseTypeConverter.java | 19 ++++++++---------- .../converters/ClassTypeConverter.java | 10 ++++------ .../converters/FileTypeConverter.java | 8 ++++---- .../converters/IntegerTypeConverter.java | 5 ++--- .../converters/TimeSpanTypeConverter.java | 5 ++--- .../common/io/PathCounterTemplate.java | 4 ++-- src/org/sosy_lab/common/io/PathTemplate.java | 2 +- .../common/log/BasicLogManagerTest.java | 16 +++++++-------- .../sosy_lab/common/log/TestLogManager.java | 2 +- src/org/sosy_lab/common/time/TimeSpan.java | 6 +++--- src/org/sosy_lab/common/time/Timer.java | 20 +++++++++---------- 18 files changed, 75 insertions(+), 85 deletions(-) diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index f112fec03..f9e64faea 100644 --- a/.gitlab-ci.yml +++ b/.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" diff --git a/src/org/sosy_lab/common/Classes.java b/src/org/sosy_lab/common/Classes.java index 443fe9be7..8e482fb16 100644 --- a/src/org/sosy_lab/common/Classes.java +++ b/src/org/sosy_lab/common/Classes.java @@ -216,9 +216,8 @@ public static 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 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) { @@ -665,9 +663,8 @@ 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; } @@ -759,7 +756,7 @@ public static final class UnsuitedClassException extends Exception { @FormatMethod UnsuitedClassException(String msg, Object... args) { - super(String.format(msg, args)); + super(msg.formatted(args)); } } } diff --git a/src/org/sosy_lab/common/ProcessExecutor.java b/src/org/sosy_lab/common/ProcessExecutor.java index c4f7a8c63..5d1d06f81 100644 --- a/src/org/sosy_lab/common/ProcessExecutor.java +++ b/src/org/sosy_lab/common/ProcessExecutor.java @@ -151,14 +151,14 @@ public ProcessExecutor( } } Supplier executingMsgSupplier = - () -> String.format("Executing '%s'", Joiner.on(" ").join(cmd)); + () -> "Executing '%s'".formatted(Joiner.on(" ").join(cmd)); logger.log(Level.FINEST, executingMsgSupplier); Process process = proc.start(); pid = process.pid(); Supplier startedMsgSupplier = - () -> String.format("Started '%s' with pid [%d]", Joiner.on(" ").join(cmd), pid); + () -> "Started '%s' with pid [%d]".formatted(Joiner.on(" ").join(cmd), pid); logger.log(Level.FINEST, startedMsgSupplier); processFuture = @@ -366,7 +366,7 @@ public int join(long timelimit) throws IOException, E, TimeoutException, Interru Throwable t = e.getCause(); Throwables.propagateIfPossible(t, IOException.class, exceptionClass); throw new UnexpectedCheckedException( - String.format("output handling of external process %s[%d]", name, pid), t); + "output handling of external process %s[%d]".formatted(name, pid), t); } finally { // cleanup diff --git a/src/org/sosy_lab/common/collect/PersistentSortedMaps.java b/src/org/sosy_lab/common/collect/PersistentSortedMaps.java index c60552890..e00529ba0 100644 --- a/src/org/sosy_lab/common/collect/PersistentSortedMaps.java +++ b/src/org/sosy_lab/common/collect/PersistentSortedMaps.java @@ -60,8 +60,8 @@ public interface MergeConflictHandler { public static MergeConflictHandler getExceptionMergeConflictHandler() { return (key, value1, value2) -> { throw new IllegalArgumentException( - String.format( - "Conflicting value when merging maps for key %s: %s and %s", key, value1, value2)); + "Conflicting value when merging maps for key %s: %s and %s" + .formatted(key, value1, value2)); }; } diff --git a/src/org/sosy_lab/common/configuration/Configuration.java b/src/org/sosy_lab/common/configuration/Configuration.java index dcaa2b009..1e9c417a0 100644 --- a/src/org/sosy_lab/common/configuration/Configuration.java +++ b/src/org/sosy_lab/common/configuration/Configuration.java @@ -664,9 +664,9 @@ private void setOptionValueForMethod(Object obj, Method method, Options options) // this is an expected exception if the value is wrong, // so create a nice message for the user throw new InvalidConfigurationException( - String.format( - "Invalid value in configuration file: \"%s = %s\"%s", - name, value, (t.getMessage() != null ? " (" + t.getMessage() + ")" : "")), + "Invalid value in configuration file: \"%s = %s\"%s" + .formatted( + name, value, (t.getMessage() != null ? " (" + t.getMessage() + ")" : "")), t); } @@ -850,18 +850,16 @@ private String getOptionSourceForLogging(String optionDeprecatedName) { String[] allowedValues = option.values(); if (allowedValues.length > 0 && !Arrays.asList(allowedValues).contains(valueStr)) { throw new InvalidConfigurationException( - String.format( - "Invalid value in configuration file: \"%s = %s\" (not listed as allowed value)", - name, valueStr)); + "Invalid value in configuration file: \"%s = %s\" (not listed as allowed value)" + .formatted(name, valueStr)); } // check if it matches the specification regexp String regexp = option.regexp(); if (!regexp.isEmpty() && !valueStr.matches(regexp)) { throw new InvalidConfigurationException( - String.format( - "Invalid value in configuration file: \"%s = %s\" (does not match RegExp \"%s\").", - name, valueStr, regexp)); + "Invalid value in configuration file: \"%s = %s\" (does not match RegExp \"%s\")." + .formatted(name, valueStr, regexp)); } return valueStr; @@ -906,8 +904,8 @@ private static void checkApplicability( if (!applicableTypes.isEmpty() && !applicableTypes.contains(optionType.getRawType())) { throw new UnsupportedOperationException( - String.format( - "Annotation %s is not applicable for options of type %s.", annotation, optionType)); + "Annotation %s is not applicable for options of type %s." + .formatted(annotation, optionType)); } } diff --git a/src/org/sosy_lab/common/configuration/OptionAnnotationProcessor.java b/src/org/sosy_lab/common/configuration/OptionAnnotationProcessor.java index 8005c2daf..ad83e53e1 100644 --- a/src/org/sosy_lab/common/configuration/OptionAnnotationProcessor.java +++ b/src/org/sosy_lab/common/configuration/OptionAnnotationProcessor.java @@ -410,9 +410,12 @@ private void checkOptionDetailAnnotations(Element elem) { ERROR, elem, am, - String.format( - "%s %s for annotation %s, this annotation is only for types %s.", - msgPrefix, optionType, annotationName, Joiner.on(", ").join(acceptedTypeNames))); + "%s %s for annotation %s, this annotation is only for types %s." + .formatted( + msgPrefix, + optionType, + annotationName, + Joiner.on(", ").join(acceptedTypeNames))); } } diff --git a/src/org/sosy_lab/common/configuration/OptionCollector.java b/src/org/sosy_lab/common/configuration/OptionCollector.java index 9ee371625..c8c5597ce 100644 --- a/src/org/sosy_lab/common/configuration/OptionCollector.java +++ b/src/org/sosy_lab/common/configuration/OptionCollector.java @@ -218,9 +218,8 @@ private Stream> tryLoadClass(ClassInfo cls) { // actually never occur, e.g., ExceptionInInitializerError and UnsatisfiedLinkError. // Currently no case is known why a LinkageError would occur.. errorMessages.add( - String.format( - "INFO: Could not load '%s' for getting Option annotations: %s: %s", - cls.getResourceName(), e.getClass().getName(), e.getMessage())); + "INFO: Could not load '%s' for getting Option annotations: %s: %s" + .formatted(cls.getResourceName(), e.getClass().getName(), e.getMessage())); return Stream.empty(); } } diff --git a/src/org/sosy_lab/common/configuration/converters/BaseTypeConverter.java b/src/org/sosy_lab/common/configuration/converters/BaseTypeConverter.java index 748c66570..4810ba2b3 100644 --- a/src/org/sosy_lab/common/configuration/converters/BaseTypeConverter.java +++ b/src/org/sosy_lab/common/configuration/converters/BaseTypeConverter.java @@ -84,9 +84,8 @@ public Object convert( return Pattern.compile(valueStr); } catch (PatternSyntaxException e) { throw new InvalidConfigurationException( - String.format( - "Illegal regular expression %s in option %s (%s).", - valueStr, optionName, e.getMessage()), + "Illegal regular expression %s in option %s (%s)." + .formatted(valueStr, optionName, e.getMessage()), e); } } else if (type.equals(Rational.class)) { @@ -94,8 +93,8 @@ public Object convert( return Rational.of(valueStr); } catch (IllegalArgumentException e) { throw new InvalidConfigurationException( - String.format( - "Illegal rational %s in option %s (%s).", valueStr, optionName, e.getMessage()), + "Illegal rational %s in option %s (%s)." + .formatted(valueStr, optionName, e.getMessage()), e); } @@ -126,15 +125,13 @@ public static Object invokeStaticMethod( } catch (NoSuchMethodException | IllegalAccessException e) { throw new AssertionError( - String.format( - "Class %s without usable %s(%s) method.", - type.getSimpleName(), method, paramType.getSimpleName()), + "Class %s without usable %s(%s) method." + .formatted(type.getSimpleName(), method, paramType.getSimpleName()), e); } catch (InvocationTargetException e) { throw new InvalidConfigurationException( - String.format( - "Could not parse \"%s = %s\" (%s).", - optionName, value, e.getTargetException().getMessage()), + "Could not parse \"%s = %s\" (%s)." + .formatted(optionName, value, e.getTargetException().getMessage()), e); } } diff --git a/src/org/sosy_lab/common/configuration/converters/ClassTypeConverter.java b/src/org/sosy_lab/common/configuration/converters/ClassTypeConverter.java index 7b52dcfbc..bab919789 100644 --- a/src/org/sosy_lab/common/configuration/converters/ClassTypeConverter.java +++ b/src/org/sosy_lab/common/configuration/converters/ClassTypeConverter.java @@ -66,9 +66,8 @@ public Object convert( // check type if (!targetType.isSupertypeOf(cls)) { throw new InvalidConfigurationException( - String.format( - "Class %s specified in option %s is not an instance of %s", - value, optionName, targetType)); + "Class %s specified in option %s is not an instance of %s" + .formatted(value, optionName, targetType)); } result = cls; @@ -80,9 +79,8 @@ public Object convert( result = Classes.createFactory(type, cls); } catch (UnsuitedClassException e) { throw new InvalidConfigurationException( - String.format( - "Class %s specified in option %s is invalid (%s)", - value, optionName, e.getMessage())); + "Class %s specified in option %s is invalid (%s)" + .formatted(value, optionName, e.getMessage())); } Classes.produceClassLoadingWarning(logger, cls, type.getRawType()); } diff --git a/src/org/sosy_lab/common/configuration/converters/FileTypeConverter.java b/src/org/sosy_lab/common/configuration/converters/FileTypeConverter.java index 3fb312702..b4b3c8f37 100644 --- a/src/org/sosy_lab/common/configuration/converters/FileTypeConverter.java +++ b/src/org/sosy_lab/common/configuration/converters/FileTypeConverter.java @@ -178,9 +178,9 @@ private static InvalidConfigurationException forbidden( String reason, String optionName, Path path, Object... args) throws InvalidConfigurationException { throw new InvalidConfigurationException( - String.format( - "The option %s specifies the path '%s' that is forbidden in safe mode " + reason + ".", - FluentIterable.of(optionName, path).append(args).toArray(Object.class))); + ("The option %s specifies the path '%s' that is forbidden in safe mode " + reason + ".") + .formatted( + FluentIterable.of(optionName, path).append(args).toArray(Object.class))); } public String getOutputDirectory() { @@ -222,7 +222,7 @@ private static void checkApplicability( path = Path.of(pValue); } catch (InvalidPathException e) { throw new InvalidConfigurationException( - String.format("Invalid file name in option %s: %s", optionName, e.getMessage()), e); + "Invalid file name in option %s: %s".formatted(optionName, e.getMessage()), e); } return handleFileOption( diff --git a/src/org/sosy_lab/common/configuration/converters/IntegerTypeConverter.java b/src/org/sosy_lab/common/configuration/converters/IntegerTypeConverter.java index 5c95d224b..b717144a5 100644 --- a/src/org/sosy_lab/common/configuration/converters/IntegerTypeConverter.java +++ b/src/org/sosy_lab/common/configuration/converters/IntegerTypeConverter.java @@ -51,9 +51,8 @@ public Object convert( : Range.all(); throw new InvalidConfigurationException( - String.format( - "Invalid value in configuration file: \"%s = %s\" (not in range %s).", - optionName, value, bound.intersection(typeBound))); + "Invalid value in configuration file: \"%s = %s\" (not in range %s)." + .formatted(optionName, value, bound.intersection(typeBound))); } return value; diff --git a/src/org/sosy_lab/common/configuration/converters/TimeSpanTypeConverter.java b/src/org/sosy_lab/common/configuration/converters/TimeSpanTypeConverter.java index bd382879f..074faaeaa 100644 --- a/src/org/sosy_lab/common/configuration/converters/TimeSpanTypeConverter.java +++ b/src/org/sosy_lab/common/configuration/converters/TimeSpanTypeConverter.java @@ -82,9 +82,8 @@ public Object convert( if (option.min() > value || value > option.max()) { String codeUnitStr = TIME_UNITS.inverse().get(codeUnit); throw new InvalidConfigurationException( - String.format( - "Invalid value in configuration file: \"%s = %s (not in range [%d %s, %d %s])", - optionName, value, option.min(), codeUnitStr, option.max(), codeUnitStr)); + "Invalid value in configuration file: \"%s = %s (not in range [%d %s, %d %s])" + .formatted(optionName, value, option.min(), codeUnitStr, option.max(), codeUnitStr)); } Object result; diff --git a/src/org/sosy_lab/common/io/PathCounterTemplate.java b/src/org/sosy_lab/common/io/PathCounterTemplate.java index 27d84d9e8..3cad6667e 100644 --- a/src/org/sosy_lab/common/io/PathCounterTemplate.java +++ b/src/org/sosy_lab/common/io/PathCounterTemplate.java @@ -42,7 +42,7 @@ private PathCounterTemplate(String pTemplate) { @SuppressWarnings("ReturnValueIgnored") @SuppressFBWarnings("RV_RETURN_VALUE_IGNORED") private static void checkPatternValidity(String pTemplate) { - String.format(pTemplate, 0); + pTemplate.formatted(0); } /** @@ -63,7 +63,7 @@ public static PathCounterTemplate ofFormatString(String pTemplate) { * template. */ public Path getFreshPath() { - return Path.of(String.format(template, counter.getAndIncrement())); + return Path.of(template.formatted(counter.getAndIncrement())); } /** Returns the raw template of this instance. */ diff --git a/src/org/sosy_lab/common/io/PathTemplate.java b/src/org/sosy_lab/common/io/PathTemplate.java index 1035c9bbe..a2aaa7e07 100644 --- a/src/org/sosy_lab/common/io/PathTemplate.java +++ b/src/org/sosy_lab/common/io/PathTemplate.java @@ -49,7 +49,7 @@ public static PathTemplate ofFormatString(String pTemplate) { public Path getPath(Object... args) { checkArgument(!Arrays.asList(args).contains(null), "Values for PathTemplate may not be null"); - return Path.of(String.format(template, args)); + return Path.of(template.formatted(args)); } /** Returns the raw template of this instance. */ diff --git a/src/org/sosy_lab/common/log/BasicLogManagerTest.java b/src/org/sosy_lab/common/log/BasicLogManagerTest.java index ccc3108b9..8f25c82e1 100644 --- a/src/org/sosy_lab/common/log/BasicLogManagerTest.java +++ b/src/org/sosy_lab/common/log/BasicLogManagerTest.java @@ -122,17 +122,17 @@ private void checkExpectedTruncatedMessage(boolean knownSize) { if (knownSize) { assertThat(records.get(0).getMessage()) .isEqualTo( - String.format( - "| %s... |", - LONG_STRING.substring(0, BasicLogManager.TRUNCATE_REMAINING_SIZE), - LONG_STRING.length())); + "| %s... |" + .formatted( + LONG_STRING.substring(0, BasicLogManager.TRUNCATE_REMAINING_SIZE), + LONG_STRING.length())); } else { assertThat(records.get(0).getMessage()) .isEqualTo( - String.format( - "| %s... = %d CHARACTERS LONG> |", - LONG_STRING.substring(0, BasicLogManager.TRUNCATE_REMAINING_SIZE), - TRUNCATE_SIZE)); + "| %s... = %d CHARACTERS LONG> |" + .formatted( + LONG_STRING.substring(0, BasicLogManager.TRUNCATE_REMAINING_SIZE), + TRUNCATE_SIZE)); } } diff --git a/src/org/sosy_lab/common/log/TestLogManager.java b/src/org/sosy_lab/common/log/TestLogManager.java index 4bb66e302..553526a6b 100644 --- a/src/org/sosy_lab/common/log/TestLogManager.java +++ b/src/org/sosy_lab/common/log/TestLogManager.java @@ -132,7 +132,7 @@ private static void checkLogExceptionBaseParams(Level pPriority, Throwable pE) { @FormatMethod private static void checkFormatParamsNotNull(String pFormat, Object... pArgs) { checkNotNull(pArgs); - checkArgument(!String.format(pFormat, pArgs).isEmpty()); + checkArgument(!pFormat.formatted(pArgs).isEmpty()); } private static void checkObjectArgsConcatenationParams(Object... pArgs) { diff --git a/src/org/sosy_lab/common/time/TimeSpan.java b/src/org/sosy_lab/common/time/TimeSpan.java index f0e55e258..0613a065f 100644 --- a/src/org/sosy_lab/common/time/TimeSpan.java +++ b/src/org/sosy_lab/common/time/TimeSpan.java @@ -612,7 +612,7 @@ String formatHumanReadableLarge() { long hours = getChecked(HOURS) - years * 365 * 24 - days * 24; if (started || hours > 0) { started = true; - result.append(String.format("%02dh ", hours)); + result.append("%02dh ".formatted(hours)); } if (unit.equals(HOURS)) { return result.toString().trim(); @@ -620,7 +620,7 @@ String formatHumanReadableLarge() { long minutes = getChecked(MINUTES) - years * 365 * 24 * 60 - days * 24 * 60 - hours * 60; if (started || minutes > 0) { - result.append(String.format("%02dmin ", minutes)); + result.append("%02dmin ".formatted(minutes)); } if (unit.equals(MINUTES)) { started = true; @@ -633,7 +633,7 @@ String formatHumanReadableLarge() { - days * 24 * 60 * 60 - hours * 60 * 60 - minutes * 60; - result.append(String.format("%02ds", seconds)); + result.append("%02ds".formatted(seconds)); return result.toString(); } diff --git a/src/org/sosy_lab/common/time/Timer.java b/src/org/sosy_lab/common/time/Timer.java index 36f7d211c..68be30864 100644 --- a/src/org/sosy_lab/common/time/Timer.java +++ b/src/org/sosy_lab/common/time/Timer.java @@ -88,10 +88,10 @@ public final class Timer { public Timer() { if (DEFAULT_CLOCK == null) { throw new IllegalArgumentException( - String.format( - "Invalid value \'%s\' for property %s," - + "cannot create Timer without explicitly specified clock.", - System.getProperty(DEFAULT_CLOCK_PROPERTY_NAME), DEFAULT_CLOCK_PROPERTY_NAME)); + ("Invalid value \'%s\' for property %s, " + + "cannot create Timer without explicitly specified clock.") + .formatted( + System.getProperty(DEFAULT_CLOCK_PROPERTY_NAME), DEFAULT_CLOCK_PROPERTY_NAME)); } clock = DEFAULT_CLOCK; } @@ -243,11 +243,11 @@ public String toString() { /** Syntax sugar method: pretty-format the timer output into a string in seconds. */ public String prettyFormat() { TimeUnit t = TimeUnit.SECONDS; - return String.format( - "%s (Max: %s), (Avg: %s), (#intervals = %s)", - getSumTime().formatAs(t), - getMaxTime().formatAs(t), - getAvgTime().formatAs(t), - getNumberOfIntervals()); + return "%s (Max: %s), (Avg: %s), (#intervals = %s)" + .formatted( + getSumTime().formatAs(t), + getMaxTime().formatAs(t), + getAvgTime().formatAs(t), + getNumberOfIntervals()); } } From 56204f4279bad151fa5264ce3f0648da3e853ec2 Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Tue, 10 Mar 2026 09:30:43 +0100 Subject: [PATCH 08/11] Use record instead of AutoValue for data classes in OptionCollector These classes are not public anyway. --- .../common/configuration/OptionCollector.java | 64 ++++++++++--------- 1 file changed, 33 insertions(+), 31 deletions(-) diff --git a/src/org/sosy_lab/common/configuration/OptionCollector.java b/src/org/sosy_lab/common/configuration/OptionCollector.java index c8c5597ce..87261119a 100644 --- a/src/org/sosy_lab/common/configuration/OptionCollector.java +++ b/src/org/sosy_lab/common/configuration/OptionCollector.java @@ -8,9 +8,9 @@ package org.sosy_lab.common.configuration; +import static com.google.common.base.Preconditions.checkNotNull; import static com.google.common.base.Verify.verifyNotNull; -import com.google.auto.value.AutoValue; import com.google.common.base.Splitter; import com.google.common.cache.CacheBuilder; import com.google.common.cache.CacheLoader; @@ -514,36 +514,43 @@ private static String stripSurroundingFunctionCall(String s, String partToBeStri return Collectors.groupingBy(classifier, () -> new TreeMap<>(keyComparator), toSortedList); } - abstract static class AnnotationInfo { + interface AnnotationInfo { /** The annotated element or class. */ - abstract AnnotatedElement element(); + AnnotatedElement element(); /** The name for this annotation. */ - abstract String name(); + String name(); - abstract Class owningClass(); + Class owningClass(); - abstract String description(); + String description(); } - @AutoValue - abstract static class OptionInfo extends AnnotationInfo { + record OptionInfo( + AnnotatedElement element, String name, String description, Class type, String defaultValue) + implements AnnotationInfo { + + OptionInfo { + checkNotNull(element); + checkNotNull(name); + checkNotNull(description); + checkNotNull(type); + checkNotNull(defaultValue); + } static OptionInfo createForField( Field field, Option option, String defaultValue, Options classOption) { String name = Configuration.getOptionName(classOption, field, option); String description = createRegularDescription(field, option); - return new AutoValue_OptionCollector_OptionInfo( - field, name, description, field.getType(), defaultValue); + return new OptionInfo(field, name, description, field.getType(), defaultValue); } static OptionInfo createForMethod(Method method, Option option, Options classOption) { String name = Configuration.getOptionName(classOption, method, option); String description = createRegularDescription(method, option); // methods with @Option have no usable default value - return new AutoValue_OptionCollector_OptionInfo( - method, name, description, method.getReturnType(), ""); + return new OptionInfo(method, name, description, method.getReturnType(), ""); } static OptionInfo createDeprecatedAliasForField( @@ -551,8 +558,7 @@ static OptionInfo createDeprecatedAliasForField( String name = Configuration.getOptionName(classOption, field, option, /* isDeprecated= */ true); String description = createDeprecatedAliasDescription(field, option, classOption); - return new AutoValue_OptionCollector_OptionInfo( - field, name, description, field.getType(), defaultValue); + return new OptionInfo(field, name, description, field.getType(), defaultValue); } static OptionInfo createDeprecatedAliasForMethod( @@ -560,8 +566,7 @@ static OptionInfo createDeprecatedAliasForMethod( String name = Configuration.getOptionName(classOption, method, option, /* isDeprecated= */ true); String description = createDeprecatedAliasDescription(method, option, classOption); - return new AutoValue_OptionCollector_OptionInfo( - method, name, description, method.getReturnType(), ""); + return new OptionInfo(method, name, description, method.getReturnType(), ""); } private static String createRegularDescription(AnnotatedElement element, Option option) { @@ -577,35 +582,32 @@ private static String createDeprecatedAliasDescription( return "deprecated name for " + Configuration.getOptionName(classOption, member, option); } - abstract Class type(); - - abstract String defaultValue(); - @Override - final Class owningClass() { + public Class owningClass() { return ((Member) element()).getDeclaringClass(); } } - @AutoValue - abstract static class OptionsInfo extends AnnotationInfo { + private record OptionsInfo(String name, Options options, Class element) + implements AnnotationInfo { - static OptionsInfo create(Options options, Class c) { - return new AutoValue_OptionCollector_OptionsInfo(options.prefix(), options, c); + OptionsInfo { + checkNotNull(name); + checkNotNull(options); + checkNotNull(element); } - abstract Options options(); - - @Override - abstract Class element(); + static OptionsInfo create(Options options, Class c) { + return new OptionsInfo(options.prefix(), options, c); + } @Override - final Class owningClass() { + public Class owningClass() { return element(); } @Override - String description() { + public String description() { return options().description(); } } From 624df6b641d823d67ac211d64728cb8e5ac9c247 Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Tue, 10 Mar 2026 09:39:23 +0100 Subject: [PATCH 09/11] Make MapsDifference.Entry a record instead of an AutoValue class The disadvantage is that now the constructor is public, but for this class it does not hurt. The change should be binary and source compatible because we keep all public methods, and nobody could inherit from the old class. --- .../common/collect/MapsDifference.java | 36 +++++++++++++------ 1 file changed, 25 insertions(+), 11 deletions(-) diff --git a/src/org/sosy_lab/common/collect/MapsDifference.java b/src/org/sosy_lab/common/collect/MapsDifference.java index 63c014697..1a3e583b1 100644 --- a/src/org/sosy_lab/common/collect/MapsDifference.java +++ b/src/org/sosy_lab/common/collect/MapsDifference.java @@ -10,8 +10,8 @@ import static com.google.common.base.Preconditions.checkNotNull; -import com.google.auto.value.AutoValue; import com.google.errorprone.annotations.Immutable; +import com.google.errorprone.annotations.InlineMe; import java.util.Collection; import java.util.Optional; @@ -113,32 +113,46 @@ public void differingValues(Object pKey, Object pLeftValue, Object pRightValue) * @param The type of the key. * @param The type of the values. */ - @AutoValue @Immutable(containerOf = {"K", "V"}) - public abstract static class Entry { + public record Entry(K key, Optional leftValue, Optional rightValue) { - Entry() {} + public Entry { + checkNotNull(key); + checkNotNull(leftValue); + checkNotNull(rightValue); + } public static Entry forLeftValueOnly(K pKey, V pLeftValue) { - return new AutoValue_MapsDifference_Entry<>(pKey, Optional.of(pLeftValue), Optional.empty()); + return new Entry<>(pKey, Optional.of(pLeftValue), Optional.empty()); } public static Entry forRightValueOnly(K pKey, V pRightValue) { - return new AutoValue_MapsDifference_Entry<>(pKey, Optional.empty(), Optional.of(pRightValue)); + return new Entry<>(pKey, Optional.empty(), Optional.of(pRightValue)); } public static Entry forDifferingValues(K pKey, V pLeftValue, V pRightValue) { - return new AutoValue_MapsDifference_Entry<>( - pKey, Optional.of(pLeftValue), Optional.of(pRightValue)); + return new Entry<>(pKey, Optional.of(pLeftValue), Optional.of(pRightValue)); } /** Returns the map key. */ - public abstract K getKey(); + @Deprecated + @InlineMe(replacement = "this.key()") + public K getKey() { + return key(); + } /** Returns the left value, if present. */ - public abstract Optional getLeftValue(); + @Deprecated + @InlineMe(replacement = "this.leftValue()") + public Optional getLeftValue() { + return leftValue(); + } /** Returns the right value, if present. */ - public abstract Optional getRightValue(); + @Deprecated + @InlineMe(replacement = "this.rightValue()") + public Optional getRightValue() { + return rightValue(); + } } } From aef9ced2eae956b653992893dbb80c70efa36852 Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Tue, 10 Mar 2026 09:41:16 +0100 Subject: [PATCH 10/11] Make AnnotatedValue a record instead of an AutoValue class The disadvantage is that now the constructor is public, but for this class it does not hurt. The change should be binary and source compatible because we keep all public methods, and nobody could inherit from the old class. --- .../common/configuration/AnnotatedValue.java | 21 +++++++++---------- 1 file changed, 10 insertions(+), 11 deletions(-) diff --git a/src/org/sosy_lab/common/configuration/AnnotatedValue.java b/src/org/sosy_lab/common/configuration/AnnotatedValue.java index 019ca67b7..d3ee13eab 100644 --- a/src/org/sosy_lab/common/configuration/AnnotatedValue.java +++ b/src/org/sosy_lab/common/configuration/AnnotatedValue.java @@ -8,30 +8,29 @@ package org.sosy_lab.common.configuration; -import com.google.auto.value.AutoValue; +import static com.google.common.base.Preconditions.checkNotNull; + import com.google.errorprone.annotations.Immutable; import java.util.Optional; /** Immutable container that stores a value and an optional string. */ @Immutable(containerOf = "T") -@AutoValue -public abstract class AnnotatedValue { +public record AnnotatedValue(T value, Optional annotation) { - AnnotatedValue() {} + public AnnotatedValue { + checkNotNull(value); + checkNotNull(annotation); + } public static AnnotatedValue create(T value) { - return new AutoValue_AnnotatedValue<>(value, Optional.empty()); + return new AnnotatedValue<>(value, Optional.empty()); } public static AnnotatedValue create(T value, String annotation) { - return new AutoValue_AnnotatedValue<>(value, Optional.of(annotation)); + return new AnnotatedValue<>(value, Optional.of(annotation)); } public static AnnotatedValue create(T value, Optional annotation) { - return new AutoValue_AnnotatedValue<>(value, annotation); + return new AnnotatedValue<>(value, annotation); } - - public abstract T value(); - - public abstract Optional annotation(); } From 78f0073c40879fc3c3e7895c87a53cd3fd586808 Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Tue, 10 Mar 2026 10:53:56 +0100 Subject: [PATCH 11/11] Make some interfaces and classes "sealed" These are only cases that are not public or where inheritance was already prevented with a private constructor. --- src/org/sosy_lab/common/Classes.java | 4 +++- src/org/sosy_lab/common/ExtendedUrlClassLoader.java | 8 ++++++-- src/org/sosy_lab/common/collect/AbstractImmutableMap.java | 3 ++- .../common/collect/AbstractImmutableSortedMap.java | 7 +++++-- src/org/sosy_lab/common/collect/OurSortedMap.java | 5 ++++- src/org/sosy_lab/common/collect/PackageSanityTest.java | 2 +- .../common/collect/PathCopyingPersistentTreeMap.java | 3 +-- src/org/sosy_lab/common/collect/SortedMapKeySetTest.java | 2 +- .../sosy_lab/common/configuration/OptionCollector.java | 2 +- 9 files changed, 24 insertions(+), 12 deletions(-) diff --git a/src/org/sosy_lab/common/Classes.java b/src/org/sosy_lab/common/Classes.java index 8e482fb16..b2b738162 100644 --- a/src/org/sosy_lab/common/Classes.java +++ b/src/org/sosy_lab/common/Classes.java @@ -434,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> { + public abstract static sealed class ClassLoaderBuilder> + permits ExtendedUrlClassLoader.ExtendedUrlClassLoaderConfiguration.AutoBuilder { + ClassLoaderBuilder() {} /** diff --git a/src/org/sosy_lab/common/ExtendedUrlClassLoader.java b/src/org/sosy_lab/common/ExtendedUrlClassLoader.java index e715a14e4..67564350b 100644 --- a/src/org/sosy_lab/common/ExtendedUrlClassLoader.java +++ b/src/org/sosy_lab/common/ExtendedUrlClassLoader.java @@ -37,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 parent(); abstract ImmutableList urls(); @@ -51,7 +53,9 @@ static AutoBuilder builder() { } @AutoValue.Builder - abstract static class AutoBuilder extends Classes.ClassLoaderBuilder { + abstract static sealed class AutoBuilder extends Classes.ClassLoaderBuilder + permits AutoValue_ExtendedUrlClassLoader_ExtendedUrlClassLoaderConfiguration.Builder { + AutoBuilder() {} @Override diff --git a/src/org/sosy_lab/common/collect/AbstractImmutableMap.java b/src/org/sosy_lab/common/collect/AbstractImmutableMap.java index 008bd4ab4..2bd6ae466 100644 --- a/src/org/sosy_lab/common/collect/AbstractImmutableMap.java +++ b/src/org/sosy_lab/common/collect/AbstractImmutableMap.java @@ -18,7 +18,8 @@ import org.checkerframework.checker.nullness.qual.Nullable; @Immutable(containerOf = {"K", "V"}) -abstract class AbstractImmutableMap implements Map { +abstract sealed class AbstractImmutableMap implements Map + permits AbstractImmutableSortedMap { @Deprecated @Override diff --git a/src/org/sosy_lab/common/collect/AbstractImmutableSortedMap.java b/src/org/sosy_lab/common/collect/AbstractImmutableSortedMap.java index 191b64d64..a76378906 100644 --- a/src/org/sosy_lab/common/collect/AbstractImmutableSortedMap.java +++ b/src/org/sosy_lab/common/collect/AbstractImmutableSortedMap.java @@ -19,8 +19,11 @@ import java.util.SortedMap; import org.checkerframework.checker.nullness.qual.Nullable; -abstract class AbstractImmutableSortedMap - extends AbstractImmutableMap implements OurSortedMap { +abstract sealed class AbstractImmutableSortedMap + extends AbstractImmutableMap implements OurSortedMap + permits OurSortedMap.EmptyImmutableOurSortedMap, + PathCopyingPersistentTreeMap, + PathCopyingPersistentTreeMap.PartialSortedMap { @Override public boolean equals(@Nullable Object pObj) { diff --git a/src/org/sosy_lab/common/collect/OurSortedMap.java b/src/org/sosy_lab/common/collect/OurSortedMap.java index fae50ba94..2cf416b12 100644 --- a/src/org/sosy_lab/common/collect/OurSortedMap.java +++ b/src/org/sosy_lab/common/collect/OurSortedMap.java @@ -24,7 +24,10 @@ * Extension of {@link NavigableMap} that specifies {@link NavigableSet} as type of some collection * views (instead of {@link java.util.Set}). */ -interface OurSortedMap extends NavigableMap { +sealed interface OurSortedMap extends NavigableMap + permits AbstractImmutableSortedMap, + DescendingSortedMap, + PathCopyingPersistentTreeMap.PartialSortedMap { Iterator> entryIterator(); diff --git a/src/org/sosy_lab/common/collect/PackageSanityTest.java b/src/org/sosy_lab/common/collect/PackageSanityTest.java index 10b85f75f..d349efcf9 100644 --- a/src/org/sosy_lab/common/collect/PackageSanityTest.java +++ b/src/org/sosy_lab/common/collect/PackageSanityTest.java @@ -18,7 +18,7 @@ public class PackageSanityTest extends AbstractPackageSanityTests { PersistentLinkedList.class, PersistentLinkedList.of(), PersistentLinkedList.of("test")); @SuppressWarnings("unchecked") OurSortedMap singletonMap = - (OurSortedMap) + (PathCopyingPersistentTreeMap) PathCopyingPersistentTreeMap.of().putAndCopy("test", "test"); setDistinctValues( OurSortedMap.class, OurSortedMap.EmptyImmutableOurSortedMap.of(), singletonMap); diff --git a/src/org/sosy_lab/common/collect/PathCopyingPersistentTreeMap.java b/src/org/sosy_lab/common/collect/PathCopyingPersistentTreeMap.java index 349b1f47a..561e4b2b0 100644 --- a/src/org/sosy_lab/common/collect/PathCopyingPersistentTreeMap.java +++ b/src/org/sosy_lab/common/collect/PathCopyingPersistentTreeMap.java @@ -1203,8 +1203,7 @@ public Map.Entry next() { * @param The type of values. */ @Immutable(containerOf = {"K", "V"}) - private static final class PartialSortedMap< - K extends Comparable, V extends @Nullable Object> + static final class PartialSortedMap, V extends @Nullable Object> extends AbstractImmutableSortedMap implements OurSortedMap, Serializable { static , V> OurSortedMap create( diff --git a/src/org/sosy_lab/common/collect/SortedMapKeySetTest.java b/src/org/sosy_lab/common/collect/SortedMapKeySetTest.java index b48ea5b9b..ae97464da 100644 --- a/src/org/sosy_lab/common/collect/SortedMapKeySetTest.java +++ b/src/org/sosy_lab/common/collect/SortedMapKeySetTest.java @@ -31,7 +31,7 @@ protected SortedSet create(String[] pStrings) { for (String s : pStrings) { map = map.putAndCopy(s, true); } - return new SortedMapKeySet<>((OurSortedMap) map); + return new SortedMapKeySet<>((PathCopyingPersistentTreeMap) map); } } diff --git a/src/org/sosy_lab/common/configuration/OptionCollector.java b/src/org/sosy_lab/common/configuration/OptionCollector.java index 87261119a..0687e0ac3 100644 --- a/src/org/sosy_lab/common/configuration/OptionCollector.java +++ b/src/org/sosy_lab/common/configuration/OptionCollector.java @@ -514,7 +514,7 @@ private static String stripSurroundingFunctionCall(String s, String partToBeStri return Collectors.groupingBy(classifier, () -> new TreeMap<>(keyComparator), toSortedList); } - interface AnnotationInfo { + sealed interface AnnotationInfo { /** The annotated element or class. */ AnnotatedElement element();