From d7ed0d17d5c3c828baf266f77cf458e7a7e2da9a Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Mon, 5 May 2025 17:07:40 +0200 Subject: [PATCH 1/3] warn missing SMT solvers if flag is set --- .../de/uka/ilkd/key/smt/SmtTestUtils.java | 58 +++++++++++++++++++ .../de/uka/ilkd/key/smt/TestUnsatCore.java | 12 +--- .../key/smt/newsmt2/MasterHandlerTest.java | 19 +++--- .../uka/ilkd/key/smt/newsmt2/TestSMTMod.java | 18 ++++-- .../de/uka/ilkd/key/smt/test/TestCommons.java | 8 +-- .../de/uka/ilkd/key/util/LineProperties.java | 4 +- 6 files changed, 84 insertions(+), 35 deletions(-) create mode 100644 key.core/src/test/java/de/uka/ilkd/key/smt/SmtTestUtils.java diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/SmtTestUtils.java b/key.core/src/test/java/de/uka/ilkd/key/smt/SmtTestUtils.java new file mode 100644 index 00000000000..84577058448 --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/SmtTestUtils.java @@ -0,0 +1,58 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.smt; + +import de.uka.ilkd.key.smt.solvertypes.SolverTypeImplementation; +import de.uka.ilkd.key.smt.solvertypes.SolverTypes; + +import org.junit.jupiter.api.Assertions; +import org.junit.jupiter.api.Assumptions; + +/** + * @author Alexander Weigl + * @version 1 (5/5/25) + */ +public class SmtTestUtils { + + /// Variable signals whether a missing SMT solver should result into a abortion of the test + /// cases or a failing of the test case. + /// Flag is triggered by the environment variable `failIfSmtSolverIsUnavailable` or + /// `GITHUB_ACTIONS`. + public static final boolean failIfSmtSolverIsUnavailable = + Boolean.parseBoolean(System.getenv("failIfSmtSolverIsUnavailable")) + || Boolean.parseBoolean(System.getenv("GITHUB_ACTIONS")); + + private static final String REQUIRED_SMT_SOLVER_NOT_INSTALLED = + "required SMT solver not installed"; + + + /// Return true if z3 is installed. This means an {@link + /// de.uka.ilkd.key.smt.solvertypes.SolverType} + /// for z3 is available and it returned true for being installed. + /// + /// @see de.uka.ilkd.key.smt.solvertypes.SolverType#isInstalled(boolean) + public static boolean z3Installed() { + return SolverTypes.getSolverTypes().stream() + .filter(it -> it.getClass().equals(SolverTypeImplementation.class) + && it.getName().equals("Z3")) + .findFirst().map(x -> x.isInstalled(true)).orElse(false); + } + + /// Assumes or assert that z3 is installed depending on [#failIfSmtSolverIsUnavailable] + public static void assumeZ3Installed() { + var isInstalled = z3Installed(); + assumeSmtIsInstalled(isInstalled); + } + + /// Assumes or assert that the SMT is not installed depending on [#failIfSmtSolverIsUnavailable] + public static void assumeSmtIsInstalled(boolean isInstalled) { + if (!isInstalled && !failIfSmtSolverIsUnavailable) { + Assumptions.abort(REQUIRED_SMT_SOLVER_NOT_INSTALLED); + } + + if (!isInstalled && failIfSmtSolverIsUnavailable) { + Assertions.fail(REQUIRED_SMT_SOLVER_NOT_INSTALLED); + } + } +} diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/TestUnsatCore.java b/key.core/src/test/java/de/uka/ilkd/key/smt/TestUnsatCore.java index 9036e5aaf57..812e2e47549 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/TestUnsatCore.java +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/TestUnsatCore.java @@ -12,8 +12,6 @@ import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.io.ProblemLoaderException; -import de.uka.ilkd.key.smt.solvertypes.SolverTypeImplementation; -import de.uka.ilkd.key.smt.solvertypes.SolverTypes; import org.key_project.util.collection.ImmutableList; import org.key_project.util.helper.FindResources; @@ -29,9 +27,7 @@ class TestUnsatCore { @Test void testUnsatCore() throws ProblemLoaderException { - if (!z3Installed()) { - return; - } + SmtTestUtils.assumeZ3Installed(); KeYEnvironment env = KeYEnvironment.load(new File(testCaseDirectory, "smt/unsatCore.proof")); @@ -54,10 +50,4 @@ void testUnsatCore() throws ProblemLoaderException { Assertions.assertEquals(4, ifs.size()); } - private static boolean z3Installed() { - return SolverTypes.getSolverTypes().stream() - .filter(it -> it.getClass().equals(SolverTypeImplementation.class) - && it.getName().equals("Z3")) - .findFirst().map(x -> x.isInstalled(true)).orElse(false); - } } diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/MasterHandlerTest.java b/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/MasterHandlerTest.java index bbf0cecb622..7dcb427b8e6 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/MasterHandlerTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/MasterHandlerTest.java @@ -3,11 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.smt.newsmt2; -import java.io.BufferedReader; -import java.io.FileNotFoundException; -import java.io.IOException; -import java.io.OutputStream; -import java.io.StringReader; +import java.io.*; import java.net.URISyntaxException; import java.net.URL; import java.nio.charset.StandardCharsets; @@ -17,7 +13,6 @@ import java.util.ArrayList; import java.util.List; import java.util.Properties; -import java.util.stream.Collectors; import de.uka.ilkd.key.control.DefaultUserInterfaceControl; import de.uka.ilkd.key.control.KeYEnvironment; @@ -27,6 +22,7 @@ import de.uka.ilkd.key.settings.DefaultSMTSettings; import de.uka.ilkd.key.settings.ProofIndependentSettings; import de.uka.ilkd.key.smt.SMTSettings; +import de.uka.ilkd.key.smt.SmtTestUtils; import de.uka.ilkd.key.smt.solvertypes.SolverType; import de.uka.ilkd.key.smt.solvertypes.SolverTypeImplementation; import de.uka.ilkd.key.smt.solvertypes.SolverTypes; @@ -34,6 +30,7 @@ import org.key_project.util.Streams; +import org.jspecify.annotations.NonNull; import org.jspecify.annotations.Nullable; import org.junit.jupiter.api.Assertions; import org.junit.jupiter.api.Assumptions; @@ -89,7 +86,7 @@ public static List data() List files; try (var s = Files.list(directory)) { - files = s.collect(Collectors.toList()); + files = s.toList(); } List result = new ArrayList<>(files.size()); for (Path file : files) { @@ -129,7 +126,7 @@ public record TestData(String name, Path path, LineProperties props, String tran Path srcDir = Files.createTempDirectory("SMT_key_" + name); Path tmpSrc = srcDir.resolve("src.java"); Files.write(tmpSrc, sources); - lines.add(0, "\\javaSource \"" + srcDir + "\";\n"); + lines.addFirst("\\javaSource \"" + srcDir + "\";\n"); } Path tmpKey = Files.createTempFile("SMT_key_" + name, ".key"); @@ -158,7 +155,7 @@ public record TestData(String name, Path path, LineProperties props, String tran } @Override - public String toString() { + public @NonNull String toString() { return name; } } @@ -194,9 +191,9 @@ public static boolean containsModuloSpaces(String haystack, String needle) { @ParameterizedTest @MethodSource("data") public void testZ3(TestData data) throws Exception { + SmtTestUtils.assumeZ3Installed(); + Assumptions.assumeTrue(Z3_SOLVER != null); - Assumptions.assumeTrue(Z3_SOLVER.isInstalled(false), - "Z3 is not installed, this testcase is ignored."); String expectation = data.props.get("expected"); Assumptions.assumeTrue(expectation != null, "No Z3 expectation."); diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/TestSMTMod.java b/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/TestSMTMod.java index 8c84069e5e4..164f521bdb2 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/TestSMTMod.java +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/TestSMTMod.java @@ -10,16 +10,14 @@ import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.io.ProblemLoaderException; -import de.uka.ilkd.key.smt.SMTProblem; -import de.uka.ilkd.key.smt.SMTSolverResult; -import de.uka.ilkd.key.smt.SMTTestSettings; -import de.uka.ilkd.key.smt.SolverLauncher; +import de.uka.ilkd.key.smt.*; import de.uka.ilkd.key.smt.solvertypes.SolverType; import de.uka.ilkd.key.smt.solvertypes.SolverTypeImplementation; import de.uka.ilkd.key.smt.solvertypes.SolverTypes; import org.key_project.util.helper.FindResources; +import org.junit.jupiter.api.Assertions; import org.junit.jupiter.api.Test; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -68,13 +66,21 @@ public void testModSpec() throws ProblemLoaderException { result = checkGoal(g, Z3_SOLVER); assertSame(SMTSolverResult.ThreeValuedTruth.VALID, result.isValid()); } else { - LOGGER.warn("Warning:Z3 solver not installed, tests skipped."); + if (SmtTestUtils.failIfSmtSolverIsUnavailable) { + Assertions.fail("z3 solver not installed"); + } else { + LOGGER.warn("Warning:Z3 solver not installed, tests skipped."); + } } if (CVC4_SOLVER.isInstalled(true)) { result = checkGoal(g, CVC4_SOLVER); assertSame(SMTSolverResult.ThreeValuedTruth.VALID, result.isValid()); } else { - LOGGER.warn("Warning:CVC4 solver not installed, tests skipped."); + if (SmtTestUtils.failIfSmtSolverIsUnavailable) { + Assertions.fail("cvc4 solver not installed"); + } else { + LOGGER.warn("Warning:CVC4 solver not installed, tests skipped."); + } } } finally { env.dispose(); diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/test/TestCommons.java b/key.core/src/test/java/de/uka/ilkd/key/smt/test/TestCommons.java index da1a0422122..cadeef3025c 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/test/TestCommons.java +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/test/TestCommons.java @@ -16,14 +16,10 @@ import de.uka.ilkd.key.proof.init.*; import de.uka.ilkd.key.proof.io.ProblemLoaderException; import de.uka.ilkd.key.rule.Taclet; -import de.uka.ilkd.key.smt.SMTProblem; -import de.uka.ilkd.key.smt.SMTSolverResult; -import de.uka.ilkd.key.smt.SMTTestSettings; -import de.uka.ilkd.key.smt.SolverLauncher; +import de.uka.ilkd.key.smt.*; import de.uka.ilkd.key.smt.solvertypes.SolverType; import de.uka.ilkd.key.util.HelperClassForTests; -import org.junit.jupiter.api.Assumptions; import org.junit.jupiter.api.Tag; import static org.junit.jupiter.api.Assertions.*; @@ -66,7 +62,7 @@ protected TermServices getServices() { protected boolean correctResult(String filepath, boolean isValid) throws ProblemLoaderException { - Assumptions.assumeFalse(toolNotInstalled()); + SmtTestUtils.assumeSmtIsInstalled(!toolNotInstalled()); SMTSolverResult result = checkFile(filepath); // unknown is always allowed. But wrong answers are not allowed return correctResult(isValid, result); diff --git a/key.core/src/test/java/de/uka/ilkd/key/util/LineProperties.java b/key.core/src/test/java/de/uka/ilkd/key/util/LineProperties.java index 62cae7edd65..82597705725 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/util/LineProperties.java +++ b/key.core/src/test/java/de/uka/ilkd/key/util/LineProperties.java @@ -17,6 +17,8 @@ import java.util.Map.Entry; import java.util.Set; +import org.jspecify.annotations.Nullable; + /** * An infrastructure to read string to string maps from files. * @@ -70,7 +72,7 @@ public void read(Reader reader) throws IOException { } - public String get(String key) { + public @Nullable String get(String key) { return map.get(key); } From e13248bad84a9601ccd4e69c1b9b542bc227093a Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Fri, 9 May 2025 17:52:52 +0200 Subject: [PATCH 2/3] added cvc5 tests (for removed CVC4 test) --- .../de/uka/ilkd/key/smt/test/Cvc5Test.java | 97 +++++++++++++++++++ 1 file changed, 97 insertions(+) create mode 100644 key.core/src/test/java/de/uka/ilkd/key/smt/test/Cvc5Test.java diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/test/Cvc5Test.java b/key.core/src/test/java/de/uka/ilkd/key/smt/test/Cvc5Test.java new file mode 100644 index 00000000000..a201a5da772 --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/test/Cvc5Test.java @@ -0,0 +1,97 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.smt.test; + +import de.uka.ilkd.key.smt.solvertypes.SolverType; +import de.uka.ilkd.key.smt.solvertypes.SolverTypeImplementation; +import de.uka.ilkd.key.smt.solvertypes.SolverTypes; +import org.junit.jupiter.params.provider.Arguments; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +import java.util.stream.Stream; + +import static de.uka.ilkd.key.smt.SMTSolverResult.ThreeValuedTruth.UNKNOWN; +import static de.uka.ilkd.key.smt.SMTSolverResult.ThreeValuedTruth.VALID; + +/** + * Tests that some simple .key files are translated to SMT-LIB correctly and cvc5 has a specified + * behavior on them (returns unsat, sat, or unknown/timeout). The test uses the new modular SMT + * translation! + *

+ * Note: The settings for the solver are hard-coded in {@link de.uka.ilkd.key.smt.SMTTestSettings}! + */ +public class Cvc5Test extends SMTSolverTest { + + + public static final String SYSTEM_PROPERTY_SOLVER_PATH = "cvc5SolverPath"; + private static final Logger LOGGER = LoggerFactory.getLogger(Cvc5Test.class); + private static final String SOLVER_NAME = "cvc5"; + + private static final SolverType CVC5_SOLVER = SolverTypes.getSolverTypes().stream() + .filter(it -> it.getClass().equals(SolverTypeImplementation.class) + && it.getName().equals(SOLVER_NAME)) + .findFirst().orElse(null); + + @Override + protected Logger getLogger() { + return LOGGER; + } + + @Override + protected String getSystemPropertySolverPath() { + return SYSTEM_PROPERTY_SOLVER_PATH; + } + + @Override + protected String getSolverName() { + return SOLVER_NAME; + } + + @Override + public SolverType getSolverType() { + SolverType type = CVC5_SOLVER; + String solverPathProperty = System.getProperty(SYSTEM_PROPERTY_SOLVER_PATH); + if (solverPathProperty != null && !solverPathProperty.isEmpty()) { + type.setSolverCommand(solverPathProperty); + } + return type; + } + + @Override + protected final Stream provideTestData() { + return Stream.of( + Arguments.of(UNKNOWN, "andnot.key"), // timeout expected + Arguments.of(VALID, "ornot.key"), + Arguments.of(UNKNOWN, "andornot.key"), // timeout expected + Arguments.of(VALID, "andornot2.key"), + Arguments.of(VALID, "imply.key"), + Arguments.of(VALID, "imply2.key"), + Arguments.of(UNKNOWN, "imply3.key"), // timeout expected + Arguments.of(VALID, "equi1.key"), + Arguments.of(UNKNOWN, "equi2.key"), // timeout expected + Arguments.of(VALID, "allex1.key"), + Arguments.of(UNKNOWN, "allex2.key"), // timeout expected + Arguments.of(UNKNOWN, "allex3.key"), + Arguments.of(VALID, "logicalite1.key"), + Arguments.of(UNKNOWN, "logicalite2.key"), // timeout expected + Arguments.of(VALID, "equal1.key"), + Arguments.of(UNKNOWN, "equal2.key"), // timeout expected + Arguments.of(VALID, "subsort1.key"), + Arguments.of(UNKNOWN, "subsort2.key"), // timeout expected + Arguments.of(VALID, "add1.key"), + Arguments.of(VALID, "bsum1.key"), + Arguments.of(VALID, "bsum2.key"), + Arguments.of(UNKNOWN, "bsum3.key"), // timeout expected + Arguments.of(VALID, "bprod1.key"), + Arguments.of(VALID, "bprod2.key"), + Arguments.of(UNKNOWN, "bprod3.key"), // timeout expected + Arguments.of(UNKNOWN, "binder4.key"), // timeout expected + Arguments.of(UNKNOWN, "binder5.key"), // timeout expected + Arguments.of(VALID, "div1.key"), + Arguments.of(VALID, "div3.key"), + Arguments.of(UNKNOWN, "div5.key"), + Arguments.of(UNKNOWN, "div6.key")); + } +} From 15c9d70915f23ba541effd4cdecca0deaaa568e0 Mon Sep 17 00:00:00 2001 From: Wolfram Pfeifer Date: Fri, 9 May 2025 17:54:08 +0200 Subject: [PATCH 3/3] spotless --- .../src/test/java/de/uka/ilkd/key/smt/test/Cvc5Test.java | 5 +++-- .../test/java/de/uka/ilkd/key/smt/test/SMTTestCommons.java | 2 -- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/test/Cvc5Test.java b/key.core/src/test/java/de/uka/ilkd/key/smt/test/Cvc5Test.java index a201a5da772..a3b8788bc13 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/test/Cvc5Test.java +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/test/Cvc5Test.java @@ -3,15 +3,16 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.smt.test; +import java.util.stream.Stream; + import de.uka.ilkd.key.smt.solvertypes.SolverType; import de.uka.ilkd.key.smt.solvertypes.SolverTypeImplementation; import de.uka.ilkd.key.smt.solvertypes.SolverTypes; + import org.junit.jupiter.params.provider.Arguments; import org.slf4j.Logger; import org.slf4j.LoggerFactory; -import java.util.stream.Stream; - import static de.uka.ilkd.key.smt.SMTSolverResult.ThreeValuedTruth.UNKNOWN; import static de.uka.ilkd.key.smt.SMTSolverResult.ThreeValuedTruth.VALID; diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTTestCommons.java b/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTTestCommons.java index df20de8ce0e..a44fbc1db1c 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTTestCommons.java +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/test/SMTTestCommons.java @@ -13,12 +13,10 @@ import de.uka.ilkd.key.proof.init.*; import de.uka.ilkd.key.proof.io.ProblemLoaderException; import de.uka.ilkd.key.smt.*; -import de.uka.ilkd.key.rule.Taclet; import de.uka.ilkd.key.smt.solvertypes.SolverType; import de.uka.ilkd.key.util.HelperClassForTests; import org.jspecify.annotations.NonNull; -import org.junit.jupiter.api.Assumptions; import org.junit.jupiter.api.Tag; import static org.junit.jupiter.api.Assertions.*;