diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 773f5c0f4e..ba30afe42b 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -12,6 +12,6 @@ variables: PROJECT_PATH: "sosy-lab/software/java-smt" GH_REF: "github.com/sosy-lab/java-smt" # Version of https://gitlab.com/sosy-lab/software/refaster/ to use - REFASTER_REPO_REVISION: 31cd8ffc4966957e156665dbba76679ade5bb5c9 + REFASTER_REPO_REVISION: 26c8309d1023e4dfcb0e8d24dcf7ec12e621314e # Needs to be synchronized with Error Prone version in lib/ivy.xml - REFASTER_VERSION: 2.21.1 + REFASTER_VERSION: 2.41.0 diff --git a/.settings/org.eclipse.jdt.core.prefs b/.settings/org.eclipse.jdt.core.prefs index a4eb77d2b3..ad7836656b 100644 --- a/.settings/org.eclipse.jdt.core.prefs +++ b/.settings/org.eclipse.jdt.core.prefs @@ -2,11 +2,12 @@ # an API wrapper for a collection of SMT solvers: # https://github.com/sosy-lab/java-smt # -# SPDX-FileCopyrightText: 2020 Dirk Beyer +# SPDX-FileCopyrightText: 2025 Dirk Beyer # # SPDX-License-Identifier: Apache-2.0 eclipse.preferences.version=1 +org.eclipse.jdt.core.builder.annotationPath.allLocations=disabled org.eclipse.jdt.core.codeComplete.argumentPrefixes=p org.eclipse.jdt.core.codeComplete.argumentSuffixes= org.eclipse.jdt.core.codeComplete.fieldPrefixes= @@ -23,9 +24,12 @@ org.eclipse.jdt.core.compiler.annotation.nonnull=javax.annotation.Nonnull org.eclipse.jdt.core.compiler.annotation.nonnull.secondary= org.eclipse.jdt.core.compiler.annotation.nonnullbydefault=org.sosy_lab.common.annotations.FieldsAreNonnullByDefault org.eclipse.jdt.core.compiler.annotation.nonnullbydefault.secondary= +org.eclipse.jdt.core.compiler.annotation.notowning=org.eclipse.jdt.annotation.NotOwning org.eclipse.jdt.core.compiler.annotation.nullable=javax.annotation.Nullable org.eclipse.jdt.core.compiler.annotation.nullable.secondary= org.eclipse.jdt.core.compiler.annotation.nullanalysis=disabled +org.eclipse.jdt.core.compiler.annotation.owning=org.eclipse.jdt.annotation.Owning +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 @@ -36,6 +40,7 @@ org.eclipse.jdt.core.compiler.debug.localVariable=generate org.eclipse.jdt.core.compiler.debug.sourceFile=generate org.eclipse.jdt.core.compiler.doc.comment.support=enabled org.eclipse.jdt.core.compiler.problem.APILeak=warning +org.eclipse.jdt.core.compiler.problem.annotatedTypeArgumentToUnannotated=info org.eclipse.jdt.core.compiler.problem.annotationSuperInterface=ignore org.eclipse.jdt.core.compiler.problem.assertIdentifier=error org.eclipse.jdt.core.compiler.problem.autoboxing=ignore @@ -57,8 +62,10 @@ org.eclipse.jdt.core.compiler.problem.forbiddenReference=error org.eclipse.jdt.core.compiler.problem.hiddenCatchBlock=warning org.eclipse.jdt.core.compiler.problem.includeNullInfoFromAsserts=enabled org.eclipse.jdt.core.compiler.problem.incompatibleNonInheritedInterfaceMethod=warning +org.eclipse.jdt.core.compiler.problem.incompatibleOwningContract=warning org.eclipse.jdt.core.compiler.problem.incompleteEnumSwitch=warning org.eclipse.jdt.core.compiler.problem.indirectStaticAccess=warning +org.eclipse.jdt.core.compiler.problem.insufficientResourceAnalysis=warning org.eclipse.jdt.core.compiler.problem.invalidJavadoc=warning org.eclipse.jdt.core.compiler.problem.invalidJavadocTags=enabled org.eclipse.jdt.core.compiler.problem.invalidJavadocTagsDeprecatedRef=disabled @@ -88,14 +95,14 @@ org.eclipse.jdt.core.compiler.problem.nonExternalizedStringLiteral=ignore org.eclipse.jdt.core.compiler.problem.nonnullParameterAnnotationDropped=warning org.eclipse.jdt.core.compiler.problem.nonnullTypeVariableFromLegacyInvocation=warning org.eclipse.jdt.core.compiler.problem.nullAnnotationInferenceConflict=error -org.eclipse.jdt.core.compiler.problem.nullReference=warning +org.eclipse.jdt.core.compiler.problem.nullReference=error org.eclipse.jdt.core.compiler.problem.nullSpecViolation=error org.eclipse.jdt.core.compiler.problem.nullUncheckedConversion=warning org.eclipse.jdt.core.compiler.problem.overridingPackageDefaultMethod=warning org.eclipse.jdt.core.compiler.problem.parameterAssignment=ignore org.eclipse.jdt.core.compiler.problem.pessimisticNullAnalysisForFreeTypeVariables=warning org.eclipse.jdt.core.compiler.problem.possibleAccidentalBooleanAssignment=warning -org.eclipse.jdt.core.compiler.problem.potentialNullReference=warning +org.eclipse.jdt.core.compiler.problem.potentialNullReference=error org.eclipse.jdt.core.compiler.problem.potentiallyUnclosedCloseable=warning org.eclipse.jdt.core.compiler.problem.rawTypeReference=warning org.eclipse.jdt.core.compiler.problem.redundantNullAnnotation=warning @@ -108,6 +115,7 @@ org.eclipse.jdt.core.compiler.problem.specialParameterHidingField=disabled org.eclipse.jdt.core.compiler.problem.staticAccessReceiver=warning org.eclipse.jdt.core.compiler.problem.suppressOptionalErrors=enabled org.eclipse.jdt.core.compiler.problem.suppressWarnings=enabled +org.eclipse.jdt.core.compiler.problem.suppressWarningsNotFullyAnalysed=ignore org.eclipse.jdt.core.compiler.problem.syntacticNullAnalysisForFields=disabled org.eclipse.jdt.core.compiler.problem.syntheticAccessEmulation=ignore org.eclipse.jdt.core.compiler.problem.terminalDeprecation=warning @@ -115,7 +123,7 @@ org.eclipse.jdt.core.compiler.problem.typeParameterHiding=warning org.eclipse.jdt.core.compiler.problem.unavoidableGenericTypeProblems=enabled org.eclipse.jdt.core.compiler.problem.uncheckedTypeOperation=warning org.eclipse.jdt.core.compiler.problem.unclosedCloseable=warning -org.eclipse.jdt.core.compiler.problem.undocumentedEmptyBlock=ignore +org.eclipse.jdt.core.compiler.problem.undocumentedEmptyBlock=info org.eclipse.jdt.core.compiler.problem.unhandledWarningToken=ignore org.eclipse.jdt.core.compiler.problem.unlikelyCollectionMethodArgumentType=warning org.eclipse.jdt.core.compiler.problem.unlikelyCollectionMethodArgumentTypeStrict=disabled @@ -128,9 +136,10 @@ org.eclipse.jdt.core.compiler.problem.unusedDeclaredThrownException=warning org.eclipse.jdt.core.compiler.problem.unusedDeclaredThrownExceptionExemptExceptionAndThrowable=enabled org.eclipse.jdt.core.compiler.problem.unusedDeclaredThrownExceptionIncludeDocCommentReference=enabled org.eclipse.jdt.core.compiler.problem.unusedDeclaredThrownExceptionWhenOverriding=disabled -org.eclipse.jdt.core.compiler.problem.unusedExceptionParameter=ignore +org.eclipse.jdt.core.compiler.problem.unusedExceptionParameter=info org.eclipse.jdt.core.compiler.problem.unusedImport=warning org.eclipse.jdt.core.compiler.problem.unusedLabel=warning +org.eclipse.jdt.core.compiler.problem.unusedLambdaParameter=warning org.eclipse.jdt.core.compiler.problem.unusedLocal=warning org.eclipse.jdt.core.compiler.problem.unusedObjectAllocation=warning org.eclipse.jdt.core.compiler.problem.unusedParameter=warning @@ -139,7 +148,7 @@ org.eclipse.jdt.core.compiler.problem.unusedParameterWhenImplementingAbstract=di org.eclipse.jdt.core.compiler.problem.unusedParameterWhenOverridingConcrete=disabled org.eclipse.jdt.core.compiler.problem.unusedPrivateMember=warning org.eclipse.jdt.core.compiler.problem.unusedTypeParameter=warning -org.eclipse.jdt.core.compiler.problem.unusedWarningToken=ignore +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 diff --git a/build/build-compile.xml b/build/build-compile.xml index 2aea8b11a6..f284e0479e 100644 --- a/build/build-compile.xml +++ b/build/build-compile.xml @@ -36,9 +36,10 @@ SPDX-License-Identifier: Apache-2.0 - + + + + + + @@ -74,7 +80,7 @@ SPDX-License-Identifier: Apache-2.0 - + @@ -130,11 +136,14 @@ SPDX-License-Identifier: Apache-2.0 - + + + + diff --git a/build/build-documentation.xml b/build/build-documentation.xml index a6572387da..3be66c3ba8 100644 --- a/build/build-documentation.xml +++ b/build/build-documentation.xml @@ -37,7 +37,7 @@ SPDX-License-Identifier: Apache-2.0 - + diff --git a/build/build-ivy.xml b/build/build-ivy.xml index f788938f45..111ba56a77 100644 --- a/build/build-ivy.xml +++ b/build/build-ivy.xml @@ -46,7 +46,7 @@ SPDX-License-Identifier: Apache-2.0 - + diff --git a/build/gitlab-ci.Dockerfile.jdk-11 b/build/gitlab-ci.Dockerfile.jdk-11 index b32cdf6d95..e5dfcaece2 100644 --- a/build/gitlab-ci.Dockerfile.jdk-11 +++ b/build/gitlab-ci.Dockerfile.jdk-11 @@ -6,13 +6,13 @@ # # SPDX-License-Identifier: Apache-2.0 -# This is a Docker image for running the tests. +# This is a container image for running the tests. # It should be pushed to registry.gitlab.com/sosy-lab/software/java-smt/test # and will be used by CI as declared in .gitlab-ci.yml. # # Commands for updating the image: -# docker build --pull -t registry.gitlab.com/sosy-lab/software/java-smt/test:jdk-11 - < build/gitlab-ci.Dockerfile.jdk-11 -# docker push registry.gitlab.com/sosy-lab/software/java-smt/test:jdk-11 +# podman build --pull -t registry.gitlab.com/sosy-lab/software/java-smt/test:jdk-11 - < build/gitlab-ci.Dockerfile.jdk-11 +# podman push registry.gitlab.com/sosy-lab/software/java-smt/test:jdk-11 FROM ubuntu:20.04 diff --git a/build/gitlab-ci.Dockerfile.jdk-17 b/build/gitlab-ci.Dockerfile.jdk-17 index 12a98e9530..f0209f66be 100644 --- a/build/gitlab-ci.Dockerfile.jdk-17 +++ b/build/gitlab-ci.Dockerfile.jdk-17 @@ -6,13 +6,13 @@ # # SPDX-License-Identifier: Apache-2.0 -# This is a Docker image for running the tests. +# This is a container image for running the tests. # It should be pushed to registry.gitlab.com/sosy-lab/software/java-smt/test # and will be used by CI as declared in .gitlab-ci.yml. # # Commands for updating the image: -# docker build --pull -t registry.gitlab.com/sosy-lab/software/java-smt/test:jdk-17 - < build/gitlab-ci.Dockerfile.jdk-17 -# docker push registry.gitlab.com/sosy-lab/software/java-smt/test:jdk-17 +# podman build --pull -t registry.gitlab.com/sosy-lab/software/java-smt/test:jdk-17 - < build/gitlab-ci.Dockerfile.jdk-17 +# podman push registry.gitlab.com/sosy-lab/software/java-smt/test:jdk-17 FROM ubuntu:20.04 diff --git a/build/gitlab-ci.Dockerfile.jdk-21 b/build/gitlab-ci.Dockerfile.jdk-21 index 8b65b101a6..a3cfaccd0b 100644 --- a/build/gitlab-ci.Dockerfile.jdk-21 +++ b/build/gitlab-ci.Dockerfile.jdk-21 @@ -6,13 +6,13 @@ # # SPDX-License-Identifier: Apache-2.0 -# This is a Docker image for running the tests. +# This is a container image for running the tests. # It should be pushed to registry.gitlab.com/sosy-lab/software/java-smt/test # and will be used by CI as declared in .gitlab-ci.yml. # # Commands for updating the image: -# docker build --pull -t registry.gitlab.com/sosy-lab/software/java-smt/test:jdk-21 - < build/gitlab-ci.Dockerfile.jdk-21 -# docker push registry.gitlab.com/sosy-lab/software/java-smt/test:jdk-21 +# podman build --pull -t registry.gitlab.com/sosy-lab/software/java-smt/test:jdk-21 - < build/gitlab-ci.Dockerfile.jdk-21 +# podman push registry.gitlab.com/sosy-lab/software/java-smt/test:jdk-21 FROM ubuntu:20.04 diff --git a/build/gitlab-ci.Dockerfile.jdk-23 b/build/gitlab-ci.Dockerfile.jdk-24 similarity index 64% rename from build/gitlab-ci.Dockerfile.jdk-23 rename to build/gitlab-ci.Dockerfile.jdk-24 index bbac2aac50..b842d03dde 100644 --- a/build/gitlab-ci.Dockerfile.jdk-23 +++ b/build/gitlab-ci.Dockerfile.jdk-24 @@ -6,16 +6,16 @@ # # SPDX-License-Identifier: Apache-2.0 -# This is a Docker image for running the tests. +# This is a container image for running the tests. # It should be pushed to registry.gitlab.com/sosy-lab/software/java-smt/test # and will be used by CI as declared in .gitlab-ci.yml. # # Commands for updating the image: -# docker build --pull -t registry.gitlab.com/sosy-lab/software/java-smt/test:jdk-23 - < build/gitlab-ci.Dockerfile.jdk-23 -# docker push registry.gitlab.com/sosy-lab/software/java-smt/test:jdk-23 +# podman build --pull -t registry.gitlab.com/sosy-lab/software/java-smt/test:jdk-24 - < build/gitlab-ci.Dockerfile.jdk-24 +# podman push registry.gitlab.com/sosy-lab/software/java-smt/test:jdk-24 -# Older Ubuntu versions currently do not have GLIC_2.34 and Java 23 -FROM ubuntu:24.10 +# LTS versions currently do not have Java 24 +FROM ubuntu:25.04 ENV DEBIAN_FRONTEND=noninteractive ENV TZ=UTC @@ -25,9 +25,11 @@ RUN apt-get update && apt-get install -y --no-install-recommends \ curl \ git \ jq \ - openjdk-23-jdk-headless \ + openjdk-24-jdk-headless \ wget \ && rm -rf /var/lib/apt/lists/* +ENV LANG C.UTF-8 + RUN apt-get update && apt-get install -y \ libgomp1 diff --git a/build/gitlab-ci.yml b/build/gitlab-ci.yml index 292167666f..dbfee377d4 100644 --- a/build/gitlab-ci.yml +++ b/build/gitlab-ci.yml @@ -57,7 +57,7 @@ build-dependencies: build:jdk-11: { extends: .build, image: "${CI_REGISTRY_IMAGE}/test:jdk-11" } build:jdk-17: { extends: .build, image: "${CI_REGISTRY_IMAGE}/test:jdk-17" } build:jdk-21: { extends: .build, image: "${CI_REGISTRY_IMAGE}/test:jdk-21" } -build:jdk-23: { extends: .build, image: "${CI_REGISTRY_IMAGE}/test:jdk-23" } +build:jdk-24: { extends: .build, image: "${CI_REGISTRY_IMAGE}/test:jdk-24" } # For checks that need the binaries .binary_check: @@ -78,14 +78,16 @@ build:jdk-23: { extends: .build, image: "${CI_REGISTRY_IMAGE}/test:jdk-23" } build-project-ecj:jdk-17: {extends: .build-project-ecj, image: "${CI_REGISTRY_IMAGE}/test:jdk-17" } build-project-ecj:jdk-21: {extends: .build-project-ecj, image: "${CI_REGISTRY_IMAGE}/test:jdk-21" } -build-project-ecj:jdk-23: {extends: .build-project-ecj, image: "${CI_REGISTRY_IMAGE}/test:jdk-23" } +build-project-ecj:jdk-24: {extends: .build-project-ecj, image: "${CI_REGISTRY_IMAGE}/test:jdk-24" } check-format: extends: .source_check + image: ${CI_REGISTRY_IMAGE}/test:jdk-17 script: "ant $ANT_PROPS_CHECKS format-source && git diff -s --exit-code" checkstyle: extends: .source_check + image: ${CI_REGISTRY_IMAGE}/test:jdk-17 script: - "ant $ANT_PROPS_CHECKS checkstyle" - "ant $ANT_PROPS_CHECKS run-checkstyle -Dcheckstyle.output=plain && cat Checkstyle*.xml && test $(cat Checkstyle*xml | grep -vic audit) -eq 0" @@ -154,10 +156,10 @@ unit-tests:x86_64:jdk-21: extends: .unit-tests needs: [ build-dependencies, build:jdk-21 ] image: "${CI_REGISTRY_IMAGE}/test:jdk-21" -unit-tests:x86_64:jdk-23: +unit-tests:x86_64:jdk-24: extends: .unit-tests - needs: [ build-dependencies, build:jdk-23 ] - image: "${CI_REGISTRY_IMAGE}/test:jdk-23" + needs: [ build-dependencies, build:jdk-24 ] + image: "${CI_REGISTRY_IMAGE}/test:jdk-24" unit-tests:arm64:jdk-11: extends: .unit-tests-quick @@ -171,14 +173,14 @@ unit-tests:arm64:jdk-21: extends: .unit-tests-quick needs: [ build-dependencies, build:jdk-21 ] image: { name: "${CI_REGISTRY_IMAGE}/test:jdk-21-arm64", docker: { platform: linux/arm64 } } -unit-tests:arm64:jdk-23: +unit-tests:arm64:jdk-24: extends: .unit-tests-quick - needs: [ build-dependencies, build:jdk-23 ] - image: { name: "${CI_REGISTRY_IMAGE}/test:jdk-23-arm64", docker: { platform: linux/arm64 } } + needs: [ build-dependencies, build:jdk-24 ] + image: { name: "${CI_REGISTRY_IMAGE}/test:jdk-24-arm64", docker: { platform: linux/arm64 } } refaster: extends: .source_check - image: ${CI_REGISTRY_IMAGE}/test:jdk-11 + image: ${CI_REGISTRY_IMAGE}/test:jdk-17 before_script: - 'test -d refaster || git clone https://gitlab.com/sosy-lab/software/refaster.git' - 'cd refaster' @@ -199,10 +201,8 @@ refaster: - "error-prone.patch" - "rule.refaster" when: on_failure - except: - variables: - - $REFASTER_REPO_REVISION == null # required for job - - $REFASTER_VERSION == null # required for job + rules: + - if: $REFASTER_REPO_REVISION != null && $REFASTER_VERSION != null # required for job # check license declarations etc. @@ -223,13 +223,15 @@ deploy-gh-pages: - build:jdk-11 - javadoc environment: deploy/gh-pages - only: - variables: - - $CI_COMMIT_BRANCH == $CI_DEFAULT_BRANCH # only on default branch - - $CI_PROJECT_PATH == $PROJECT_PATH # not on forks - except: - variables: - - $GH_TOKEN == null # required for job + rules: + # run only if: + # - on default branch + # - not on a fork, + # - GH_TOKEN is present (required for job) + - if: > + $CI_COMMIT_BRANCH == $CI_DEFAULT_BRANCH + && $CI_PROJECT_PATH == $PROJECT_PATH + && $GH_TOKEN != null # Build container images @@ -247,9 +249,9 @@ deploy-gh-pages: - mkdir -p /root/.docker - echo "{\"auths\":{\"$CI_REGISTRY\":{\"username\":\"$CI_REGISTRY_USER\",\"password\":\"$CI_REGISTRY_PASSWORD\"}}}" > /kaniko/.docker/config.json - /kaniko/executor --dockerfile $CI_PROJECT_DIR/$DOCKERFILE --destination $CI_REGISTRY_IMAGE/$IMAGE $EXTRA_ARGS - only: - - schedules - - web + rules: + - if: $CI_PIPELINE_SOURCE == "schedule" + - if: $CI_PIPELINE_SOURCE == "web" .build-docker:arm64: extends: .build-docker @@ -262,9 +264,9 @@ deploy-gh-pages: build-docker:x86_64:jdk-11: { extends: .build-docker, variables: { JDK_VERSION: jdk-11 } } build-docker:x86_64:jdk-17: { extends: .build-docker, variables: { JDK_VERSION: jdk-17 } } build-docker:x86_64:jdk-21: { extends: .build-docker, variables: { JDK_VERSION: jdk-21 } } -build-docker:x86_64:jdk-23: { extends: .build-docker, variables: { JDK_VERSION: jdk-23 } } +build-docker:x86_64:jdk-24: { extends: .build-docker, variables: { JDK_VERSION: jdk-24 } } build-docker:arm64:jdk-11: { extends: .build-docker:arm64, variables: { JDK_VERSION: jdk-11 } } build-docker:arm64:jdk-17: { extends: .build-docker:arm64, variables: { JDK_VERSION: jdk-17 } } build-docker:arm64:jdk-21: { extends: .build-docker:arm64, variables: { JDK_VERSION: jdk-21 } } -build-docker:arm64:jdk-23: { extends: .build-docker:arm64, variables: { JDK_VERSION: jdk-23 } } +build-docker:arm64:jdk-24: { extends: .build-docker:arm64, variables: { JDK_VERSION: jdk-24 } } diff --git a/lib/ivy.xml b/lib/ivy.xml index 0b37f16cfe..b05804a5e1 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -108,10 +108,10 @@ SPDX-License-Identifier: Apache-2.0 - + - + @@ -123,7 +123,7 @@ SPDX-License-Identifier: Apache-2.0 - + @@ -131,7 +131,7 @@ SPDX-License-Identifier: Apache-2.0 - + @@ -140,13 +140,13 @@ SPDX-License-Identifier: Apache-2.0 - - + + - - + + @@ -154,17 +154,17 @@ SPDX-License-Identifier: Apache-2.0 - + - + - + - + diff --git a/src/org/sosy_lab/java_smt/basicimpl/tactics/NNFVisitor.java b/src/org/sosy_lab/java_smt/basicimpl/tactics/NNFVisitor.java index 023a40bc20..43e743d0d8 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/tactics/NNFVisitor.java +++ b/src/org/sosy_lab/java_smt/basicimpl/tactics/NNFVisitor.java @@ -80,7 +80,7 @@ private BooleanFormula rewriteIfThenElse( private class NNFInsideNotVisitor extends BooleanFormulaTransformationVisitor { - protected NNFInsideNotVisitor(FormulaManager pFmgr) { + NNFInsideNotVisitor(FormulaManager pFmgr) { super(pFmgr); } diff --git a/src/org/sosy_lab/java_smt/example/FormulaClassifier.java b/src/org/sosy_lab/java_smt/example/FormulaClassifier.java index e371763f72..569996d98a 100644 --- a/src/org/sosy_lab/java_smt/example/FormulaClassifier.java +++ b/src/org/sosy_lab/java_smt/example/FormulaClassifier.java @@ -88,14 +88,12 @@ public static void main(String... args) List definitions = new ArrayList<>(); for (String line : Files.readAllLines(path)) { // we assume a line-based content - if (Iterables.any( - ImmutableList.of(";", "(push ", "(pop ", "(reset", "(set-logic"), line::startsWith)) { - continue; - } else if (line.startsWith("(assert ")) { + if (line.startsWith("(assert ")) { BooleanFormula bf = context.getFormulaManager().parse(Joiner.on("").join(definitions) + line); formulas.add(bf); - } else { + } else if (!Iterables.any( + ImmutableList.of(";", "(push ", "(pop ", "(reset", "(set-logic"), line::startsWith)) { // it is a definition definitions.add(line); } diff --git a/src/org/sosy_lab/java_smt/example/PrettyPrinter.java b/src/org/sosy_lab/java_smt/example/PrettyPrinter.java index c79dfd4961..7833a09c55 100644 --- a/src/org/sosy_lab/java_smt/example/PrettyPrinter.java +++ b/src/org/sosy_lab/java_smt/example/PrettyPrinter.java @@ -88,14 +88,12 @@ public static void main(String... args) List definitions = new ArrayList<>(); for (String line : Files.readAllLines(path)) { // we assume a line-based content - if (Iterables.any( - ImmutableList.of(";", "(push ", "(pop ", "(reset", "(set-logic"), line::startsWith)) { - continue; - } else if (line.startsWith("(assert ")) { + if (line.startsWith("(assert ")) { BooleanFormula bf = context.getFormulaManager().parse(Joiner.on("").join(definitions) + line); formulas.add(bf); - } else { + } else if (!Iterables.any( + ImmutableList.of(";", "(push ", "(pop ", "(reset", "(set-logic"), line::startsWith)) { // it is a definition definitions.add(line); } diff --git a/src/org/sosy_lab/java_smt/example/SimpleUserPropagator.java b/src/org/sosy_lab/java_smt/example/SimpleUserPropagator.java index 0ae8cb55a5..57e3b4c52d 100644 --- a/src/org/sosy_lab/java_smt/example/SimpleUserPropagator.java +++ b/src/org/sosy_lab/java_smt/example/SimpleUserPropagator.java @@ -193,11 +193,13 @@ public void onDecision(BooleanFormula expr, boolean value) { if (getBackend().propagateNextDecision(disExpr, Optional.of(decisionValue))) { // The above call returns "true" if the provided literal is yet undecided, otherwise // false. - logger.log( + logger.logf( Level.INFO, - String.format( - "User propagator overwrites decision from '%s = %s' to '%s = %s'", - expr, value, disExpr, decisionValue)); + "User propagator overwrites decision from '%s = %s' to '%s = %s'", + expr, + value, + disExpr, + decisionValue); break; } } diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorAbstractProver.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorAbstractProver.java index 1608cc098c..2d9cad5c35 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorAbstractProver.java @@ -33,7 +33,8 @@ abstract class BoolectorAbstractProver extends AbstractProverWithAllSat { private final long btor; private final BoolectorFormulaManager manager; private final BoolectorFormulaCreator creator; - protected boolean wasLastSatCheckSat = false; // and stack is not changed + protected final AtomicBoolean wasLastSatCheckSat = + new AtomicBoolean(false); // and stack is not changed private final TerminationCallback terminationCallback; private final long terminationCallbackHelper; @@ -83,10 +84,10 @@ public void close() { @Override public boolean isUnsat() throws SolverException, InterruptedException { Preconditions.checkState(!closed); - wasLastSatCheckSat = false; + wasLastSatCheckSat.set(false); final int result = BtorJNI.boolector_sat(btor); if (result == BtorJNI.BTOR_RESULT_SAT_get()) { - wasLastSatCheckSat = true; + wasLastSatCheckSat.set(true); return false; } else if (result == BtorJNI.BTOR_RESULT_UNSAT_get()) { return true; @@ -127,7 +128,7 @@ public boolean isUnsatWithAssumptions(Collection pAssumptions) @Override public Model getModel() throws SolverException { Preconditions.checkState(!closed); - Preconditions.checkState(wasLastSatCheckSat, NO_MODEL_HELP); + Preconditions.checkState(wasLastSatCheckSat.get(), NO_MODEL_HELP); checkGenerateModels(); return new CachingModel(getEvaluatorWithoutChecks()); } diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java index 6d2bb3b9d9..e86aecaf0f 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java @@ -63,7 +63,7 @@ private static class BoolectorSettings { private final BoolectorFormulaManager manager; private final BoolectorFormulaCreator creator; private final ShutdownNotifier shutdownNotifier; - private boolean closed = false; + private final AtomicBoolean closed = new AtomicBoolean(false); private final AtomicBoolean isAnyStackAlive = new AtomicBoolean(false); BoolectorSolverContext( @@ -188,8 +188,7 @@ public ImmutableMap getStatistics() { @Override public void close() { - if (!closed) { - closed = true; + if (!closed.getAndSet(true)) { BtorJNI.boolector_delete(creator.getEnv()); } } @@ -197,7 +196,7 @@ public void close() { @SuppressWarnings("resource") @Override protected ProverEnvironment newProverEnvironment0(Set pOptions) { - Preconditions.checkState(!closed, "solver context is already closed"); + Preconditions.checkState(!closed.get(), "solver context is already closed"); return new BoolectorTheoremProver( manager, creator, creator.getEnv(), shutdownNotifier, pOptions, isAnyStackAlive); } diff --git a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtFormulaCreator.java index a1e5403b65..e2600642d6 100644 --- a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtFormulaCreator.java @@ -332,10 +332,10 @@ private FunctionDeclarationKind getDeclarationKind(PTRef f) { public Object convertValue(PTRef value) { Logic logic = getEnv(); if (logic.isTrue(value)) { - return Boolean.TRUE; + return true; } if (logic.isFalse(value)) { - return Boolean.FALSE; + return false; } ArithLogic alogic = (ArithLogic) getEnv(); if (alogic.isIntConst(value)) { diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java index c68dc69578..856701a407 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java @@ -148,7 +148,7 @@ protected void popImpl() { * extend the original model. */ Collection getEvaluatedTerms() { - return Collections.unmodifiableCollection(evaluatedTerms); + return Collections.unmodifiableSet(evaluatedTerms); } /** Track an assignment `term == value` for an evaluated term and its value. */ diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java index f3f933793e..40aeaecb00 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java @@ -369,7 +369,6 @@ public List parseStringToTerms(String s, PrincessFormulaC * Exception at run time. */ @SuppressWarnings("unchecked") - @SuppressFBWarnings("THROWS_METHOD_THROWS_CLAUSE_THROWABLE") private static void throwCheckedAsUnchecked(Throwable e) throws E { throw (E) e; } diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java index d7b470236d..670d2f1521 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java @@ -48,8 +48,8 @@ private PrincessFunctionDeclaration() {} private abstract static class AbstractDeclaration extends PrincessFunctionDeclaration { - /** some object representing the functon declaration. */ - protected final T declarationItem; + /* some object representing the function declaration. */ + final T declarationItem; AbstractDeclaration(T pDeclaration) { declarationItem = pDeclaration; @@ -120,7 +120,7 @@ public IExpression makeApp(PrincessEnvironment env, List args) { } } - /** Check if the expression returns a Rational. */ + /* Check if the expression returns a "Rational". */ private boolean exprIsRational(IExpression arg) { if (arg instanceof IFunApp) { IFunction fun = ((IFunApp) arg).fun(); @@ -140,7 +140,7 @@ private boolean exprIsRational(IExpression arg) { return false; } - /** Checks if the k-th argument of the function is a Rational. */ + /* Checks if the k-th argument of the function is a "Rational". */ private boolean functionTakesRational(Integer index) { // we switch from "int" to "Integer" in the signature to avoid ambiguous types with Scala API. if (declarationItem instanceof MonoSortedIFunction) { diff --git a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaCreator.java index 757b2a61ba..43ba707c08 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaCreator.java @@ -179,15 +179,6 @@ public Object convertValue(Term value) { } } - /** ApplicationTerms can be wrapped with "|". This function removes those chars. */ - public static String dequote(String s) { - int l = s.length(); - if (s.charAt(0) == '|' && s.charAt(l - 1) == '|') { - return s.substring(1, l - 1); - } - return s; - } - @Override public R visit(FormulaVisitor visitor, Formula f, final Term input) { checkArgument( @@ -217,9 +208,9 @@ public R visit(FormulaVisitor visitor, Formula f, final Term input) { if (arity == 0) { if (app.equals(environment.getTheory().mTrue)) { - return visitor.visitConstant(f, Boolean.TRUE); + return visitor.visitConstant(f, true); } else if (app.equals(environment.getTheory().mFalse)) { - return visitor.visitConstant(f, Boolean.FALSE); + return visitor.visitConstant(f, false); } else if (func.getDefinition() == null) { return visitor.visitFreeVariable(f, dequote(input.toString())); } else { diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java index 7d408faf11..18cbdb246d 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java @@ -17,6 +17,7 @@ import java.nio.charset.StandardCharsets; import java.nio.file.Path; import java.util.Set; +import java.util.concurrent.atomic.AtomicBoolean; import java.util.function.Consumer; import java.util.logging.Level; import org.checkerframework.checker.nullness.qual.Nullable; @@ -46,7 +47,7 @@ public final class Z3SolverContext extends AbstractSolverContext { private final ExtraOptions extraOptions; private final Z3FormulaCreator creator; private final Z3FormulaManager manager; - private boolean closed = false; + private final AtomicBoolean closed = new AtomicBoolean(false); private static final String OPT_ENGINE_CONFIG_KEY = "optsmt_engine"; private static final String OPT_PRIORITY_CONFIG_KEY = "priority"; @@ -215,7 +216,7 @@ public static synchronized Z3SolverContext create( @Override protected ProverEnvironment newProverEnvironment0(Set options) { - Preconditions.checkState(!closed, "solver context is already closed"); + Preconditions.checkState(!closed.get(), "solver context is already closed"); final ImmutableMap solverOptions = ImmutableMap.builder() .put(":random-seed", extraOptions.randomSeed) @@ -241,7 +242,7 @@ protected InterpolatingProverEnvironment newProverEnvironmentWithInterpolatio @Override public OptimizationProverEnvironment newOptimizationProverEnvironment0( Set options) { - Preconditions.checkState(!closed, "solver context is already closed"); + Preconditions.checkState(!closed.get(), "solver context is already closed"); final ImmutableMap solverOptions = ImmutableMap.builder() // .put(":random-seed", extraOptions.randomSeed) // not supported here @@ -269,8 +270,7 @@ public Solvers getSolverName() { @Override public void close() { - if (!closed) { - closed = true; + if (!closed.getAndSet(true)) { long context = creator.getEnv(); creator.forceClose(); shutdownNotifier.unregister(interruptListener); diff --git a/src/org/sosy_lab/java_smt/test/BooleanFormulaSubject.java b/src/org/sosy_lab/java_smt/test/BooleanFormulaSubject.java index 3deecae77f..a9dc67113e 100644 --- a/src/org/sosy_lab/java_smt/test/BooleanFormulaSubject.java +++ b/src/org/sosy_lab/java_smt/test/BooleanFormulaSubject.java @@ -19,7 +19,6 @@ import com.google.common.truth.StandardSubjectBuilder; import com.google.common.truth.Subject; import com.google.common.truth.Truth; -import edu.umd.cs.findbugs.annotations.SuppressFBWarnings; import java.util.ArrayList; import java.util.List; import org.sosy_lab.java_smt.api.BooleanFormula; @@ -39,7 +38,6 @@ * {@link StandardSubjectBuilder#about(com.google.common.truth.Subject.Factory)} and set a solver * via the method {@link #booleanFormulasOf(SolverContext)}. */ -@SuppressFBWarnings("EQ_DOESNT_OVERRIDE_EQUALS") public final class BooleanFormulaSubject extends Subject { private final SolverContext context; diff --git a/src/org/sosy_lab/java_smt/test/Fuzzer.java b/src/org/sosy_lab/java_smt/test/Fuzzer.java index 7a5bbd2099..ed581829e1 100644 --- a/src/org/sosy_lab/java_smt/test/Fuzzer.java +++ b/src/org/sosy_lab/java_smt/test/Fuzzer.java @@ -8,7 +8,6 @@ package org.sosy_lab.java_smt.test; -import edu.umd.cs.findbugs.annotations.SuppressFBWarnings; import java.util.Random; import org.sosy_lab.common.UniqueIdGenerator; import org.sosy_lab.java_smt.api.BooleanFormula; @@ -42,7 +41,6 @@ public BooleanFormula fuzz(int formulaSize, BooleanFormula... pVars) { return recFuzz(formulaSize); } - @SuppressFBWarnings(value = "DMI_RANDOM_USED_ONLY_ONCE") private BooleanFormula recFuzz(int formulaSize) { if (formulaSize == 1) { @@ -69,7 +67,6 @@ private BooleanFormula recFuzz(int formulaSize) { } } - @SuppressFBWarnings(value = "DMI_RANDOM_USED_ONLY_ONCE") private BooleanFormula getVar() { return vars[r.nextInt(vars.length)]; } diff --git a/src/org/sosy_lab/java_smt/test/IntegerTheoryFuzzer.java b/src/org/sosy_lab/java_smt/test/IntegerTheoryFuzzer.java index 4b8b2ae26d..d24767a9e8 100644 --- a/src/org/sosy_lab/java_smt/test/IntegerTheoryFuzzer.java +++ b/src/org/sosy_lab/java_smt/test/IntegerTheoryFuzzer.java @@ -8,7 +8,6 @@ package org.sosy_lab.java_smt.test; -import edu.umd.cs.findbugs.annotations.SuppressFBWarnings; import java.util.Random; import java.util.stream.IntStream; import org.sosy_lab.java_smt.api.FormulaManager; @@ -43,7 +42,6 @@ public IntegerFormula fuzz(int formulaSize, int pMaxConstant, IntegerFormula... return recFuzz(formulaSize); } - @SuppressFBWarnings(value = "DMI_RANDOM_USED_ONLY_ONCE") private IntegerFormula recFuzz(int pFormulaSize) { if (pFormulaSize == 1) { @@ -78,12 +76,10 @@ private IntegerFormula recFuzz(int pFormulaSize) { } } - @SuppressFBWarnings(value = "DMI_RANDOM_USED_ONLY_ONCE") private IntegerFormula getConstant() { return ifmgr.makeNumber((long) r.nextInt(2 * maxConstant) - maxConstant); } - @SuppressFBWarnings(value = "DMI_RANDOM_USED_ONLY_ONCE") private IntegerFormula getVar() { return vars[r.nextInt(vars.length)]; } diff --git a/src/org/sosy_lab/java_smt/test/ProverEnvironmentSubject.java b/src/org/sosy_lab/java_smt/test/ProverEnvironmentSubject.java index 95cdca5e36..03bf101f57 100644 --- a/src/org/sosy_lab/java_smt/test/ProverEnvironmentSubject.java +++ b/src/org/sosy_lab/java_smt/test/ProverEnvironmentSubject.java @@ -16,7 +16,6 @@ import com.google.common.truth.FailureMetadata; import com.google.common.truth.StandardSubjectBuilder; import com.google.common.truth.Subject; -import edu.umd.cs.findbugs.annotations.SuppressFBWarnings; import java.util.List; import org.sosy_lab.java_smt.api.BasicProverEnvironment; import org.sosy_lab.java_smt.api.BooleanFormula; @@ -32,7 +31,6 @@ * {@link StandardSubjectBuilder#about(com.google.common.truth.Subject.Factory)} and {@link * #proverEnvironments()}. */ -@SuppressFBWarnings("EQ_DOESNT_OVERRIDE_EQUALS") public final class ProverEnvironmentSubject extends Subject { private final BasicProverEnvironment stackUnderTest; diff --git a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java index 7a21cf12e3..bb78491a2e 100644 --- a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java +++ b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java @@ -14,7 +14,6 @@ import static org.sosy_lab.java_smt.test.ProverEnvironmentSubject.assertThat; import com.google.common.truth.Truth; -import edu.umd.cs.findbugs.annotations.SuppressFBWarnings; import java.util.Collection; import org.checkerframework.checker.nullness.qual.Nullable; import org.junit.After; @@ -86,7 +85,6 @@ *

Test that rely on a theory that not all solvers support should call one of the {@code require} * methods at the beginning. */ -@SuppressFBWarnings(value = "URF_UNREAD_PUBLIC_OR_PROTECTED_FIELD", justification = "test code") public abstract class SolverBasedTest0 { protected Configuration config; diff --git a/src/org/sosy_lab/java_smt/test/SolverTacticsTest.java b/src/org/sosy_lab/java_smt/test/SolverTacticsTest.java index 6402c8c0cb..833f945242 100644 --- a/src/org/sosy_lab/java_smt/test/SolverTacticsTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverTacticsTest.java @@ -228,7 +228,7 @@ private static class CNFChecker implements BooleanFormulaVisitor { boolean containsMoreAnd = false; boolean started = false; - protected CNFChecker(FormulaManager pFmgr) { + CNFChecker(FormulaManager pFmgr) { bfmgr = pFmgr.getBooleanFormulaManager(); } @@ -237,7 +237,7 @@ Void visit(BooleanFormula f) { return bfmgr.visit(f, this); } - public boolean isInCNF() { + boolean isInCNF() { return (startsWithAnd && !containsMoreAnd) || (started && !startsWithAnd); } @@ -334,7 +334,7 @@ private static class NNFChecker implements BooleanFormulaVisitor { boolean wasLastVisitNot = false; boolean notOnlyAtAtoms = true; - protected NNFChecker(FormulaManager pFmgr) { + NNFChecker(FormulaManager pFmgr) { bfmgr = pFmgr.getBooleanFormulaManager(); } @@ -343,7 +343,7 @@ Void visit(BooleanFormula f) { return bfmgr.visit(f, this); } - public boolean isInNNF() { + boolean isInNNF() { return notOnlyAtAtoms; }