We update this list, whenever a new solver or operating system is added. */ - private void requireSupportedOperatingSystem() { - StandardSubjectBuilder assume = - assume() - .withMessage( - "Solver %s is not yet supported in the operating system %s", solverToUse(), OS); + private void requirePlatformSupported() { + assume() + .withMessage( + "Solver %s is not yet supported in the operating system %s with architecture %s", + solverToUse(), OS, ARCH) + .that(isSupportedOperatingSystemAndArchitecture()) + .isTrue(); + } + + private void requirePlatformNotSupported() { + assume() + .withMessage( + "Solver %s is not yet supported in the operating system %s with architecture %s", + solverToUse(), OS, ARCH) + .that(isSupportedOperatingSystemAndArchitecture()) + .isFalse(); + } + + /** + * This method represents the matrix of supported operating systems and architectures, which can + * be tested in our CI. It might be possible that JavaSMT runs on more systems than listed here, + * but we do not explicitly test them in our CI. + */ + private boolean isSupportedOperatingSystemAndArchitecture() { switch (solverToUse()) { case SMTINTERPOL: case PRINCESS: - // any operating system is allowed, Java is already available. - return; + // Any operating system and any architecture is allowed, Java is sufficient + return true; case BOOLECTOR: case CVC4: case YICES2: - assume.that(IS_LINUX).isTrue(); - return; + return IS_LINUX && !IS_ARCH_ARM64; case CVC5: - assume.that(IS_LINUX || IS_WINDOWS).isTrue(); - if (IS_LINUX) { - assume.that(isSufficientVersionOfLibcxx("cvc5jni")).isTrue(); - } - return; + return (IS_LINUX && isSufficientVersionOfLibcxx("cvc5jni")) + || (IS_WINDOWS && !IS_ARCH_ARM64); case OPENSMT: - assume.that(IS_LINUX).isTrue(); - assume.that(isSufficientVersionOfLibcxx("opensmtj")).isTrue(); - return; + return IS_LINUX && isSufficientVersionOfLibcxx("opensmtj"); case BITWUZLA: - assume.that(IS_LINUX).isTrue(); - assume.that(isSufficientVersionOfLibcxx("bitwuzlaj")).isTrue(); - return; + return (IS_LINUX && isSufficientVersionOfLibcxx("bitwuzlaj")) + || (IS_WINDOWS && !IS_ARCH_ARM64); case MATHSAT5: - assume.that(IS_LINUX || IS_WINDOWS).isTrue(); - if (IS_LINUX) { - assume.that(isSufficientVersionOfLibcxx("mathsat5j")).isTrue(); - } - return; + return (IS_LINUX && isSufficientVersionOfLibcxx("mathsat5j")) + || (IS_WINDOWS && !IS_ARCH_ARM64); case Z3: - assume.that(IS_LINUX || IS_WINDOWS || IS_MAC).isTrue(); - if (IS_LINUX) { - assume.that(isSufficientVersionOfLibcxx("z3")).isTrue(); - } - return; + return (IS_LINUX && isSufficientVersionOfLibcxx("z3")) || IS_WINDOWS || IS_MAC; default: throw new AssertionError("unexpected solver: " + solverToUse()); } @@ -149,7 +158,7 @@ private String[] getRequiredLibcxx(String library) { case "z3": return new String[] {"GLIBC_2.34", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29"}; case "bitwuzlaj": - return new String[] {"GLIBCXX_3.4.26", "GLIBCXX_3.4.29"}; + return new String[] {"GLIBC_2.33", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29"}; case "opensmtj": return new String[] {"GLIBC_2.33", "GLIBCXX_3.4.26", "GLIBCXX_3.4.29"}; case "mathsat5j": @@ -168,7 +177,7 @@ public final void initSolver() throws InvalidConfigurationException { @Test public void createSolverContextFactoryWithDefaultLoader() throws InvalidConfigurationException { - requireSupportedOperatingSystem(); + requirePlatformSupported(); SolverContextFactory factory = new SolverContextFactory(config, logger, shutdownManager.getNotifier()); @@ -181,14 +190,14 @@ public void createSolverContextFactoryWithDefaultLoader() throws InvalidConfigur @Test public void createSolverContextFactoryWithSystemLoader() throws InvalidConfigurationException { requireNativeLibrary(); - requireSupportedOperatingSystem(); + requirePlatformSupported(); // we assume that no native solvers are installed on the testing machine by default. SolverContextFactory factory = new SolverContextFactory( config, logger, shutdownManager.getNotifier(), System::loadLibrary); assert_() - .that(assertThrows(InvalidConfigurationException.class, () -> factory.generateContext())) + .that(assertThrows(InvalidConfigurationException.class, factory::generateContext)) .hasCauseThat() .isInstanceOf(UnsatisfiedLinkError.class); } @@ -197,7 +206,7 @@ public void createSolverContextFactoryWithSystemLoader() throws InvalidConfigura public void createSolverContextFactoryWithSystemLoaderForJavaSolver() throws InvalidConfigurationException { requireNoNativeLibrary(); - requireSupportedOperatingSystem(); + requirePlatformSupported(); SolverContextFactory factory = new SolverContextFactory( @@ -207,4 +216,30 @@ public void createSolverContextFactoryWithSystemLoaderForJavaSolver() FormulaManager mgr = context.getFormulaManager(); } } + + /** Negative test for failing to load native library. */ + @Test + public void testFailToLoadNativeLibraryWithInvalidOperatingSystem() + throws InvalidConfigurationException { + requireNativeLibrary(); + requirePlatformNotSupported(); + + SolverContextFactory factory = + new SolverContextFactory(config, logger, shutdownManager.getNotifier()); + + // Verify that creating the context fails with UnsatisfiedLinkError + InvalidConfigurationException thrown = + assertThrows( + "Expected InvalidConfigurationException due to failure in loading native library", + InvalidConfigurationException.class, + factory::generateContext); + assert_().that(thrown).hasCauseThat().isInstanceOf(UnsatisfiedLinkError.class); + assert_() + .that(thrown) + .hasMessageThat() + .startsWith( + String.format( + "The SMT solver %s is not available on this machine because of missing libraries ", + solverToUse())); + } } diff --git a/src/org/sosy_lab/java_smt/test/SolverContextTest.java b/src/org/sosy_lab/java_smt/test/SolverContextTest.java index ae43a00463..bef2574fb3 100644 --- a/src/org/sosy_lab/java_smt/test/SolverContextTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverContextTest.java @@ -144,7 +144,7 @@ public void testCVC5WithValidOptions() throws InvalidConfigurationException { } } - @Test(timeout = 1000) + @Test(timeout = 5000) @SuppressWarnings({"try", "CheckReturnValue"}) public void testCVC5WithValidOptionsTimeLimit() throws InvalidConfigurationException, InterruptedException {