diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 662441f2df..121ed2eb07 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -14,7 +14,7 @@ variables: # Version of https://gitlab.com/sosy-lab/software/refaster/ to use REFASTER_REPO_REVISION: 31cd8ffc4966957e156665dbba76679ade5bb5c9 # Needs to be synchronized with Error Prone version in lib/ivy.xml - REFASTER_VERSION: 2.18.0 + REFASTER_VERSION: 2.19.1 build:jdk-17: variables: diff --git a/src/org/sosy_lab/java_smt/example/NQueens.java b/src/org/sosy_lab/java_smt/example/NQueens.java index 184507e88d..9f8f961693 100644 --- a/src/org/sosy_lab/java_smt/example/NQueens.java +++ b/src/org/sosy_lab/java_smt/example/NQueens.java @@ -181,6 +181,7 @@ private List columnRule(BooleanFormula[][] symbols) { } return rules; } + /** * Rule 4: At most one queen per diagonal transform the field (=symbols) from square shape into a * (downwards/upwards directed) rhombus that is embedded in a rectangle diff --git a/src/org/sosy_lab/java_smt/example/PrettyPrinter.java b/src/org/sosy_lab/java_smt/example/PrettyPrinter.java index 8e9f8c417d..330b2ab537 100644 --- a/src/org/sosy_lab/java_smt/example/PrettyPrinter.java +++ b/src/org/sosy_lab/java_smt/example/PrettyPrinter.java @@ -16,6 +16,7 @@ import java.nio.file.Path; import java.util.ArrayList; import java.util.List; +import java.util.Locale; import java.util.logging.Level; import org.sosy_lab.common.ShutdownNotifier; import org.sosy_lab.common.configuration.Configuration; @@ -63,7 +64,7 @@ public static void main(String... args) if (arg.startsWith("-solver=")) { solver = Solvers.valueOf(arg.substring(8)); } else if (arg.startsWith("-type=")) { - type = Type.valueOf(arg.substring(6).toUpperCase()); + type = Type.valueOf(arg.substring(6).toUpperCase(Locale.getDefault())); } else if (path == null) { path = Path.of(arg); } else { diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaCreator.java index 2c1e7b4429..aae33665fc 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorFormulaCreator.java @@ -50,6 +50,7 @@ public class BoolectorFormulaCreator extends FormulaCreator> ufArgumentsSortMap = new HashMap<>(); + // Possibly we need to split this up into vars, ufs, and arrays BoolectorFormulaCreator(Long btor) { diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorNativeApiTest.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorNativeApiTest.java index 8401fbc9f3..2ba4087fee 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorNativeApiTest.java +++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorNativeApiTest.java @@ -13,6 +13,7 @@ import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableMap; import java.util.Arrays; +import java.util.Locale; import org.junit.After; import org.junit.AssumptionViolatedException; import org.junit.Before; @@ -75,7 +76,9 @@ public void optionNameTest() { // check whether our enum is identical to Boolector's internal enum for (BtorOption option : BtorOption.values()) { String optName = BtorJNI.boolector_get_opt_lng(btor, option.getValue()); - String converted = "BTOR_OPT_" + optName.replace("-", "_").replace(":", "_").toUpperCase(); + String converted = + "BTOR_OPT_" + + optName.replace("-", "_").replace(":", "_").toUpperCase(Locale.getDefault()); assertThat(option.name()).isEqualTo(ALLOWED_DIFFS.getOrDefault(converted, converted)); } } @@ -85,7 +88,7 @@ public void satSolverTest() { // check whether all sat solvers are available for (SatSolver satSolver : SatSolver.values()) { long btor1 = BtorJNI.boolector_new(); - BtorJNI.boolector_set_sat_solver(btor1, satSolver.name().toLowerCase()); + BtorJNI.boolector_set_sat_solver(btor1, satSolver.name().toLowerCase(Locale.getDefault())); long newVar = BtorJNI.boolector_var(btor1, BtorJNI.boolector_bool_sort(btor1), "x"); BtorJNI.boolector_assert(btor1, newVar); int result = BtorJNI.boolector_sat(btor1); 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 2dcd001fb3..6c90828e93 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java +++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java @@ -12,6 +12,7 @@ import com.google.common.base.Splitter; import com.google.common.base.Splitter.MapSplitter; import com.google.common.collect.ImmutableMap; +import java.util.Locale; import java.util.Map; import java.util.Set; import java.util.concurrent.atomic.AtomicBoolean; @@ -227,7 +228,8 @@ private static void setOptions( BoolectorSettings settings = new BoolectorSettings(config); Preconditions.checkNotNull(settings.satSolver); - BtorJNI.boolector_set_sat_solver(btor, settings.satSolver.name().toLowerCase()); + BtorJNI.boolector_set_sat_solver( + btor, settings.satSolver.name().toLowerCase(Locale.getDefault())); // Default Options to enable multiple SAT, auto cleanup on close, incremental mode BtorJNI.boolector_set_opt(btor, BtorOption.BTOR_OPT_MODEL_GEN.getValue(), 2); // Auto memory clean after closing diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApi.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApi.java index c7e0e1c459..33f2fd17ac 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApi.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApi.java @@ -696,6 +696,7 @@ public static native long msat_simplify( public static native String msat_decl_get_name(long d); public static native String msat_term_repr(long t); + /* * Parsing and writing formulas. */ @@ -727,6 +728,7 @@ public static native long msat_simplify( public static native void msat_reset_env(long e); public static native void msat_assert_formula(long e, long formula); + // public static native int msat_add_preferred_for_branching(long e, long termBoolvar); // public static native int msat_clear_preferred_for_branching(long e) private static native int msat_solve(long e) throws InterruptedException; diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2BooleanFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2BooleanFormulaManager.java index f3b3f3c740..322e061ec3 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2BooleanFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2BooleanFormulaManager.java @@ -51,6 +51,7 @@ protected Integer not(Integer pParam1) { protected Integer and(Integer pParam1, Integer pParam2) { return yices_and2(pParam1, pParam2); } + // Causes BooleanFormulaManagerTest/testConjunctionCollector to fail. // @Override // protected Integer andImpl(Collection pParams) { diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaManager.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaManager.java index 5f13512a0b..53aa7b20d4 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaManager.java @@ -25,6 +25,7 @@ import com.google.common.base.Preconditions; import com.google.common.base.Strings; import java.io.IOException; +import java.util.Locale; import java.util.Map; import org.sosy_lab.common.Appender; import org.sosy_lab.common.Appenders; @@ -122,7 +123,7 @@ private String getTypeRepr(int type) { return "(_ BitVec " + yices_bvtype_size(type) + ")"; } String typeRepr = yices_type_to_string(type); - return typeRepr.substring(0, 1).toUpperCase() + typeRepr.substring(1); + return typeRepr.substring(0, 1).toUpperCase(Locale.getDefault()) + typeRepr.substring(1); } }; } diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApi.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApi.java index 2775a99df2..2ea4894d0d 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApi.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApi.java @@ -612,6 +612,7 @@ private Yices2NativeApi() {} // TODO can return up to UINT32_MAX ? /** Returns an array in the form [term,power]. */ public static native int[] yices_product_component(int t, int i); + /* * SAT Checking */ diff --git a/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java b/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java index af7360b322..b99f0e4ab7 100644 --- a/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java @@ -18,6 +18,7 @@ import java.util.ArrayList; import java.util.Collections; import java.util.List; +import java.util.Locale; import java.util.concurrent.BlockingQueue; import java.util.concurrent.ConcurrentLinkedQueue; import java.util.concurrent.CountDownLatch; @@ -113,7 +114,7 @@ protected Solvers solverToUse() { public void checkThatSolverIsAvailable() throws InvalidConfigurationException { initSolver().close(); - if (System.getProperty("os.name").toLowerCase().startsWith("win")) { + if (System.getProperty("os.name").toLowerCase(Locale.getDefault()).startsWith("win")) { assume() .withMessage("MathSAT5 is not reentant on Windows") .that(solver) @@ -194,6 +195,25 @@ public void testBvConcurrencyWithConcurrentContext() { }); } + /** Helperclass to pack a SolverContext together with a Formula. */ + private static class ContextAndFormula { + private final SolverContext context; + private final BooleanFormula formula; + + private ContextAndFormula(SolverContext context, BooleanFormula formula) { + this.context = context; + this.formula = formula; + } + + SolverContext getContext() { + return context; + } + + BooleanFormula getFormula() { + return formula; + } + } + /** * Test translation of formulas used on distinct contexts to a new, unrelated context. Every * thread creates a context, generates a formula, those are collected and handed back to the main @@ -210,24 +230,7 @@ public void testFormulaTranslationWithConcurrentContexts() .withMessage("Solver does not support translation of formulas") .that(solver) .isNoneOf(Solvers.CVC4, Solvers.PRINCESS, Solvers.CVC5); - /** Helperclass to pack a SolverContext together with a Formula */ - class ContextAndFormula { - private final SolverContext context; - private final BooleanFormula formula; - - protected ContextAndFormula(SolverContext context, BooleanFormula formula) { - this.context = context; - this.formula = formula; - } - public SolverContext getContext() { - return context; - } - - public BooleanFormula getFormula() { - return formula; - } - } ConcurrentLinkedQueue contextAndFormulaList = new ConcurrentLinkedQueue<>(); assertConcurrency( @@ -439,24 +442,7 @@ public void continuousRunningThreadFormulaTransferTranslateTest() { .withMessage("Solver does not support translation of formulas") .that(solver) .isNoneOf(Solvers.CVC4, Solvers.CVC5, Solvers.PRINCESS); - /** Helperclass to pack a SolverContext together with a Formula */ - class ContextAndFormula { - private final SolverContext context; - private final BooleanFormula formula; - - protected ContextAndFormula(SolverContext context, BooleanFormula formula) { - this.context = context; - this.formula = formula; - } - public SolverContext getContext() { - return context; - } - - public BooleanFormula getFormula() { - return formula; - } - } // This is fine! We might access this more than once at a time, // but that gives only access to the bucket, which is threadsafe. AtomicReferenceArray> bucketQueue = diff --git a/src/org/sosy_lab/java_smt/test/SolverContextFactoryTest.java b/src/org/sosy_lab/java_smt/test/SolverContextFactoryTest.java index 9e7913530a..9160c6b45f 100644 --- a/src/org/sosy_lab/java_smt/test/SolverContextFactoryTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverContextFactoryTest.java @@ -13,6 +13,7 @@ import com.google.common.base.StandardSystemProperty; import com.google.common.truth.StandardSubjectBuilder; +import java.util.Locale; import org.junit.Before; import org.junit.Test; import org.junit.runner.RunWith; @@ -36,7 +37,7 @@ public class SolverContextFactoryTest { private static final String OS = - StandardSystemProperty.OS_NAME.value().toLowerCase().replace(" ", ""); + StandardSystemProperty.OS_NAME.value().toLowerCase(Locale.getDefault()).replace(" ", ""); private static final boolean IS_WINDOWS = OS.startsWith("windows"); private static final boolean IS_MAC = OS.startsWith("macos"); private static final boolean IS_LINUX = OS.startsWith("linux"); diff --git a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java index 1eaf3fd7f5..2bec3b8a99 100644 --- a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java @@ -19,6 +19,7 @@ import java.util.HashSet; import java.util.LinkedHashSet; import java.util.List; +import java.util.Locale; import java.util.Map; import java.util.Random; import java.util.Set; @@ -928,7 +929,7 @@ public BooleanFormula visitAtom( BooleanFormula pAtom, FunctionDeclaration decl) { if (decl.getKind() == FunctionDeclarationKind.VAR) { // Uppercase all variables. - return bmgr.makeVariable(decl.getName().toUpperCase()); + return bmgr.makeVariable(decl.getName().toUpperCase(Locale.getDefault())); } else { return pAtom; } @@ -936,7 +937,7 @@ public BooleanFormula visitAtom( }); assertThat( mgr.extractVariables(transformed).keySet().stream() - .allMatch(pS -> pS.equals(pS.toUpperCase()))) + .allMatch(pS -> pS.equals(pS.toUpperCase(Locale.getDefault())))) .isTrue(); }