diff --git a/build.gradle b/build.gradle index 38d212ea5db..e395696920b 100644 --- a/build.gradle +++ b/build.gradle @@ -97,7 +97,6 @@ subprojects { testImplementation(platform("org.junit:junit-bom:5.14.1")) testImplementation ("org.junit.jupiter:junit-jupiter-api") - testImplementation ("org.junit.jupiter:junit-jupiter-api") testImplementation ("org.junit.jupiter:junit-jupiter-params") testRuntimeOnly ("org.junit.jupiter:junit-jupiter-engine") testRuntimeOnly ("org.junit.platform:junit-platform-launcher") diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBuiltInRuleApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBuiltInRuleApp.java index 922529f64cf..b3c0a794da9 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBuiltInRuleApp.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBuiltInRuleApp.java @@ -125,7 +125,8 @@ public boolean complete() { @Override public String toString() { - return "BuiltInRule: " + rule().name() + " at pos " + pio.subTerm(); + return "BuiltInRule: " + rule().name() + " at pos " + + (pio != null ? pio.subTerm() : "[pio is null]"); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java b/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java index 8efef1a3e1b..7f7888731c5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java @@ -3,15 +3,15 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.settings; -import java.io.File; -import java.io.IOException; -import java.io.PrintWriter; -import java.io.Writer; +import java.io.*; +import java.nio.file.Path; import java.util.*; import de.uka.ilkd.key.nparser.ParsingFacade; import de.uka.ilkd.key.util.Position; +import org.key_project.util.collection.Pair; + import org.antlr.v4.runtime.CharStream; import org.jspecify.annotations.NonNull; import org.jspecify.annotations.Nullable; @@ -43,11 +43,11 @@ public Configuration(Map data) { /** * Loads a configuration using the given file. * - * @param file existsing file path + * @param file existing file path * @return a configuration based on the file contents - * @throws IOException if file does not exists or i/o error + * @throws IOException if file does not exist or i/o error */ - public static Configuration load(File file) throws IOException { + public static Configuration load(Path file) throws IOException { return ParsingFacade.readConfigurationFile(file); } @@ -415,10 +415,41 @@ public void save(Writer writer, String comment) { new ConfigurationWriter(writer).printComment(comment).printMap(this.data); } + @Override + public String toString() { + try (StringWriter sw = new StringWriter()) { + save(sw, ""); + return sw.toString(); + } catch (IOException e) { + throw new RuntimeException(e); + } + } + public void overwriteWith(Configuration other) { data.putAll(other.data); } + /// Returns all section in the current configuration. + public List getSections() { + return this.data.values().stream() + .filter(it -> it instanceof Configuration) + .map(it -> (Configuration) it) + .toList(); + } + + /// Returns all section in the current configuration with their name. + public List> getSectionsWithNames() { + return this.data.entrySet().stream() + .filter(it -> it.getValue() instanceof Configuration) + .map(it -> new Pair<>(it.getKey(), (Configuration) it.getValue())) + .toList(); + } + + /// Returns the set of known keys + public Set keys() { + return this.data.keySet(); + } + // TODO Add documentation for this. /** * POJO for metadata of configuration entries. diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/PathConfig.java b/key.core/src/main/java/de/uka/ilkd/key/settings/PathConfig.java index 03a2372a12b..040aa15ba23 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/PathConfig.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/PathConfig.java @@ -4,6 +4,8 @@ package de.uka.ilkd.key.settings; import java.io.File; +import java.nio.file.Path; +import java.nio.file.Paths; import org.key_project.util.java.IOUtil; @@ -22,7 +24,8 @@ public final class PathConfig { /** - * The Java system property used to indicate that the settings in the KeY directory should not + * The name of the Java system property used to indicate that the settings in the KeY directory + * should not * be consulted at startup. */ public static final String DISREGARD_SETTINGS_PROPERTY = "key.disregardSettings"; @@ -35,22 +38,22 @@ public final class PathConfig { /** * In which file to store the recent files. */ - private static String recentFileStorage; + private static Path recentFileStorage; /** * In which file to store the proof-independent settings. */ - private static String proofIndependentSettings; + private static Path proofIndependentSettings; /** * directory where to find the KeY configuration files */ - private static String keyConfigDir; + private static Path keyConfigDir; /** * Directory in which the log files are stored. */ - private static File logDirectory; + private static Path logDirectory; private PathConfig() { } @@ -67,7 +70,7 @@ private PathConfig() { * * @return The directory. */ - public static String getKeyConfigDir() { + public static Path getKeyConfigDir() { return keyConfigDir; } @@ -77,11 +80,11 @@ public static String getKeyConfigDir() { * @param keyConfigDir The new directory to use. */ public static void setKeyConfigDir(String keyConfigDir) { - PathConfig.keyConfigDir = keyConfigDir; - recentFileStorage = getKeyConfigDir() + File.separator + "recentFiles.json"; - proofIndependentSettings = - getKeyConfigDir() + File.separator + "proofIndependentSettings.props"; - logDirectory = new File(keyConfigDir, "logs"); + PathConfig.keyConfigDir = Paths.get(keyConfigDir); + + recentFileStorage = getKeyConfigDir().resolve("recentFiles.json"); + proofIndependentSettings = getKeyConfigDir().resolve("proofIndependentSettings.props"); + logDirectory = getKeyConfigDir().resolve("logs"); } /** @@ -89,14 +92,14 @@ public static void setKeyConfigDir(String keyConfigDir) { * * @return The path to the file. */ - public static String getRecentFileStorage() { + public static Path getRecentFileStorage() { return recentFileStorage; } /** * */ - public static File getLogDirectory() { + public static Path getLogDirectory() { return logDirectory; } @@ -105,7 +108,7 @@ public static File getLogDirectory() { * * @return The path to the file. */ - public static String getProofIndependentSettings() { + public static Path getProofIndependentSettings() { return proofIndependentSettings; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSettings.java index 0646074f4af..afa3de141b3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSettings.java @@ -29,12 +29,13 @@ public class ProofIndependentSettings { public static final ProofIndependentSettings DEFAULT_INSTANCE; static { - var file = new File(PathConfig.getProofIndependentSettings().replace(".props", ".json")); + var file = new File(PathConfig.getProofIndependentSettings().toString() + .replace(".props", ".json")); if (file.exists()) { DEFAULT_INSTANCE = new ProofIndependentSettings(file); } else { - var old = new File(PathConfig.getProofIndependentSettings()); - DEFAULT_INSTANCE = new ProofIndependentSettings(old); + var old = PathConfig.getProofIndependentSettings(); + DEFAULT_INSTANCE = new ProofIndependentSettings(old.toFile()); } } @@ -109,7 +110,7 @@ private void load(File file) throws IOException { lastReadedProperties = properties; } } else { - this.lastReadedConfiguration = Configuration.load(file); + this.lastReadedConfiguration = Configuration.load(file.toPath()); for (Settings settings : settings) { settings.readSettings(lastReadedConfiguration); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/ProofSettings.java index b06d2307847..550ceaa1ff5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/ProofSettings.java @@ -7,6 +7,8 @@ import java.io.*; import java.net.URL; import java.nio.charset.StandardCharsets; +import java.nio.file.Files; +import java.nio.file.Path; import java.util.LinkedList; import java.util.List; import java.util.Properties; @@ -35,11 +37,11 @@ public class ProofSettings { private static final Logger LOGGER = LoggerFactory.getLogger(ProofSettings.class); - public static final File PROVER_CONFIG_FILE = - new File(PathConfig.getKeyConfigDir(), "proof-settings.props"); + public static final Path PROVER_CONFIG_FILE = + PathConfig.getKeyConfigDir().resolve("proof-settings.props"); - public static final File PROVER_CONFIG_FILE_NEW = - new File(PathConfig.getKeyConfigDir(), "proof-settings.json"); + public static final Path PROVER_CONFIG_FILE_NEW = + PathConfig.getKeyConfigDir().resolve("proof-settings.json"); public static final URL PROVER_CONFIG_FILE_TEMPLATE = KeYResourceManager.getManager() .getResourceFile(ProofSettings.class, "default-proof-settings.json"); @@ -144,11 +146,11 @@ public void settingsToStream(Writer out) { */ public void saveSettings() { try { - if (!PROVER_CONFIG_FILE_NEW.exists()) { - PROVER_CONFIG_FILE.getParentFile().mkdirs(); + if (!Files.exists(PROVER_CONFIG_FILE_NEW)) { + Files.createDirectories(PROVER_CONFIG_FILE.getParent()); } - try (Writer out = new BufferedWriter( - new FileWriter(PROVER_CONFIG_FILE_NEW, StandardCharsets.UTF_8))) { + try (Writer out = + Files.newBufferedWriter(PROVER_CONFIG_FILE_NEW, StandardCharsets.UTF_8)) { settingsToStream(out); } } catch (IOException e) { @@ -207,9 +209,9 @@ public void loadSettings() { if (Boolean.getBoolean(PathConfig.DISREGARD_SETTINGS_PROPERTY)) { LOGGER.warn("The settings in {} are *not* read.", PROVER_CONFIG_FILE); } else { - var isOldFormat = !PROVER_CONFIG_FILE_NEW.exists(); + var isOldFormat = !Files.exists(PROVER_CONFIG_FILE_NEW); var fileToUse = isOldFormat ? PROVER_CONFIG_FILE : PROVER_CONFIG_FILE_NEW; - try (var in = new BufferedReader(new FileReader(fileToUse, StandardCharsets.UTF_8))) { + try (var in = Files.newBufferedReader(fileToUse, StandardCharsets.UTF_8)) { LOGGER.info("Load proof dependent settings from file {}", fileToUse); if (isOldFormat) { loadDefaultJSONSettings(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/SettingsConverter.java b/key.core/src/main/java/de/uka/ilkd/key/settings/SettingsConverter.java index 8ddf8237bd0..8ea1732deb4 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/SettingsConverter.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/SettingsConverter.java @@ -5,9 +5,7 @@ import java.io.IOException; import java.io.InputStream; -import java.util.Arrays; -import java.util.Collection; -import java.util.Properties; +import java.util.*; import java.util.stream.Collectors; import org.key_project.util.Streams; @@ -28,7 +26,7 @@ public final class SettingsConverter { *
  • "#newline" in a props file encodes "\n"
    • * *
    - * + *

    * Note that, in order to guarantee dec(enc(*)) = enc(dec(*)) = id(*), care has to be taken: *

      *
    1. The replacement order needs to be inverted for dec @@ -37,7 +35,7 @@ public final class SettingsConverter { * to change these and vice versa. Otherwise, cases like the following will break: * dec("=") = "="; enc("=") = "#equals" -> enc(dec("=")) = "#equals" != "="
      2. *
    - * + *

    * TODO enc(dec(*)) = id is currently not guaranteed. * 2. is only guaranteed by enc because any occurrence of "#..." will be encoded to * "#hash...". Thus, @@ -63,7 +61,8 @@ public final class SettingsConverter { /** * The class doesn't need to be instantiated as it only contains static methods. */ - private SettingsConverter() {} + private SettingsConverter() { + } /** * Replace occurrences of Strings in {@link #ENCODINGS} by their corresponding encoding String. @@ -206,6 +205,24 @@ public static Collection unsupportedPropertiesKeys( .collect(Collectors.toList()); } + + /// + public static Collection unsupportedPropertiesKeysInSubSections( + Configuration config, String[] supportedKeys) { + + Set supKeys = new HashSet<>(Arrays.asList(supportedKeys)); + + List error = new ArrayList<>(); + + for (var section : config.getSectionsWithNames()) { + Set keys = new TreeSet<>(section.second.keys()); + keys.removeAll(supKeys); + error.addAll(keys.stream().map(it -> section.first + "." + it).toList()); + } + return error; + } + + /** * Read a raw String property without paying attention to {@link #ENCODINGS}s. * The read value will thus be returned without any changes. @@ -434,8 +451,8 @@ public static void store(Properties props, String key, long value) { * @param key the key whose value is the enum constant's ordinal in enum T * @param defaultValue the default enum constant of T to return * @param values the enum values of T from which to choose the value to read - * @return the value of the read enum constant * @param the enum which the read constant belongs to + * @return the value of the read enum constant */ public static > T read(Properties props, String key, T defaultValue, T[] values) { @@ -459,4 +476,5 @@ public static > T read(Properties props, String key, T default public static > void store(Properties props, String key, T value) { store(props, key, value.ordinal()); } + } diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTFocusResults.java b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTFocusResults.java index a78386d5020..ff31facfaf3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/SMTFocusResults.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/SMTFocusResults.java @@ -4,7 +4,8 @@ package de.uka.ilkd.key.smt; import java.util.Arrays; -import java.util.HashSet; +import java.util.Set; +import java.util.TreeSet; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.*; @@ -25,6 +26,7 @@ import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; +import org.jspecify.annotations.Nullable; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -121,7 +123,7 @@ public static boolean focus(SMTProblem smtProblem, Services services) { * @param problem SMT solver results * @return formula collection or null if the solver did not produce an unsat core */ - public static ImmutableList getUnsatCore( + public static @Nullable ImmutableList getUnsatCore( SMTProblem problem) { SMTSolver solver = problem.getSuccessfulSolver(); @@ -135,7 +137,7 @@ public static ImmutableList getUnsatCore( LOGGER.info("Analyzing unsat core: {}", lastLine); - Integer[] numbers; + int[] numbers; if (lastLine.matches("\\(.*\\)")) { // Z3 unsat core format: all labels on one line numbers = parseZ3Format(lastLine); @@ -149,7 +151,9 @@ public static ImmutableList getUnsatCore( Node goalNode = problem.getNode(); - HashSet unsatCore = new HashSet<>(Arrays.asList(numbers)); + Set unsatCore = new TreeSet<>(); + Arrays.stream(numbers).forEach(unsatCore::add); + ImmutableList unsatCoreFormulas = ImmutableSLList.nil(); @@ -183,11 +187,14 @@ public static ImmutableList getUnsatCore( * @param lastLine unsat core line * @return list of labels referenced in the unsat core */ - static Integer[] parseZ3Format(String lastLine) { + static int[] parseZ3Format(String lastLine) { lastLine = lastLine.substring(1, lastLine.length() - 1); + if (lastLine.isBlank()) { + return new int[0]; + } String[] labels = lastLine.trim().split(" +"); - Integer[] numbers = new Integer[labels.length]; + int[] numbers = new int[labels.length]; for (int i = 0; i < numbers.length; i++) { numbers[i] = Integer.parseInt(labels[i].substring(2)); } @@ -207,16 +214,16 @@ static Integer[] parseZ3Format(String lastLine) { * @param lines cvc5 output * @return list of labels referenced in unsat core */ - static Integer[] parseCVC5Format(String[] lines) { + static int[] parseCVC5Format(String[] lines) { for (int i = 0; i < lines.length; i++) { if (lines[i].equals("(")) { - Integer[] numbers = new Integer[lines.length - 2 - i]; + var numbers = new int[lines.length - 2 - i]; for (int j = i + 1; j < lines.length - 1; j++) { numbers[j - i - 1] = Integer.parseInt(lines[j].substring(2)); } return numbers; } } - return null; + return new int[0]; } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/solvertypes/SolverPropertiesLoader.java b/key.core/src/main/java/de/uka/ilkd/key/smt/solvertypes/SolverPropertiesLoader.java index 220f435f3aa..ff871090ded 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/solvertypes/SolverPropertiesLoader.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/solvertypes/SolverPropertiesLoader.java @@ -3,45 +3,62 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.smt.solvertypes; -import java.io.BufferedReader; import java.io.IOException; import java.io.InputStream; -import java.io.InputStreamReader; -import java.net.URL; +import java.net.URI; import java.nio.charset.StandardCharsets; -import java.util.*; +import java.nio.file.Files; +import java.nio.file.Path; +import java.nio.file.Paths; +import java.util.ArrayList; +import java.util.Collection; +import java.util.HashMap; +import java.util.Map; +import de.uka.ilkd.key.nparser.ParsingFacade; +import de.uka.ilkd.key.settings.Configuration; +import de.uka.ilkd.key.settings.PathConfig; import de.uka.ilkd.key.settings.SettingsConverter; import de.uka.ilkd.key.smt.communication.Z3Socket; import de.uka.ilkd.key.smt.newsmt2.ModularSMTLib2Translator; +import org.key_project.util.Streams; import org.key_project.util.reflection.ClassLoaderUtil; +import org.antlr.v4.runtime.CharStreams; +import org.jspecify.annotations.Nullable; import org.slf4j.Logger; import org.slf4j.LoggerFactory; -/** - * Provides static SolverType objects to be reused and saves the properties to .props files. Used to - * create {@link SolverType} (in the form of {@link SolverTypeImplementation}) objects from .props - * files. - * - * @author Alicia Appelhagen - */ +/// This class provides [SolverType] instances based on the current SMT solver definitions in +/// various configuration files. +/// +/// The configuration are in loaded from +/// 1. The current working directory: `./smt-solvers.json` +/// 2. Path from system property : `-P key.smt_solvers=` +/// 3. The KeY user configuration folder: `~/.key/smt-solvers.json` +/// 4. All resources with the name `de/uka/ilkd/key/smt/solvertypes/solvers.key.json` in the +/// classpath. +/// +/// Local configuration overwrites user configuration overwrites classpath configuration. +/// All configuration is overwritten using the {@link +/// de.uka.ilkd.key.settings.ProofIndependentSettings#getSMTSettings()}. +/// +/// Use (1) and (2) rather to add new SMT solvers to KeY. +/// +/// @author Alicia Appelhagen +/// @author Alexander Weigl public class SolverPropertiesLoader { - - /** - * Logger. - */ private static final Logger LOGGER = LoggerFactory.getLogger(SolverPropertiesLoader.class); - /** - * Name of the file containing the names of the SMT properties files to be loaded. - */ - private static final String SOLVER_LIST_FILE = "solvers.txt"; - /** - * Package path of the solvers.txt file. - */ - private static final String PACKAGE_PATH = "de/uka/ilkd/key/smt/solvertypes/"; + /// Name of the file containing the names of the SMT properties files to be loaded. + public static final String SOLVER_LIST_FILE = "smt-solvers.json"; + + /// Package path of the solvers.txt file. + public static final String PACKAGE_PATH = "de/uka/ilkd/key/smt/solvertypes/"; + + /// Java system property key denoting a path for further definitions of SMT solvers. + public static final String SYSTEM_PROPERTY_KEY_SMT_SOLVERS = "key.smt_solvers"; /** * The solvers loaded by this loader. @@ -52,11 +69,6 @@ public class SolverPropertiesLoader { */ private static final Collection EXPERIMENTAL_SOLVERS = new ArrayList<>(2); - /** - * String used to SPLIT list properties such as the delimiter list or the handler list. - */ - private static final String SPLIT = ","; - /** * The default solver NAME, if none is given in the .props file. */ @@ -93,10 +105,6 @@ public class SolverPropertiesLoader { */ private static final String DEFAULT_SOLVER_SOCKET = "de.uka.ilkd.key.smt.communication.Z3Socket"; - /** - * The default message DELIMITERS, if none are given in the .props file. - */ - private static final String[] DEFAULT_DELIMITERS = { "\n", "\r" }; /** * The default solver TIMEOUT, if none is given in the .props file. */ @@ -208,14 +216,14 @@ private static String uniqueName(String name) { */ public Collection getSolvers() { if (SOLVERS.isEmpty()) { - for (Properties solverProp : loadSolvers()) { + for (Configuration solverProp : loadSolvers().getSections()) { SolverType createdType = makeSolver(solverProp); SOLVERS.add(createdType); /* * If the solver is an EXPERIMENTAL solver (only available in experimental mode), * add it to the separate list: */ - if (SettingsConverter.read(solverProp, EXPERIMENTAL, false)) { + if (solverProp.getBool(EXPERIMENTAL, false)) { EXPERIMENTAL_SOLVERS.add(createdType); } } @@ -234,75 +242,61 @@ public Collection getExperimentalSolvers() { /** * Create a {@link SolverTypeImplementation} from a Properties object. */ - private static SolverType makeSolver(Properties props) { - String name; - String command; - String params; - String version; - String info; - String preamble; - String minVersion; - long timeout; + private static SolverType makeSolver(Configuration props) { + String preamble = null; Class solverSocketClass; Class translatorClass; - String[] handlerNames; - String[] handlerOptions; - String[] delimiters; // Read props file to create a SolverTypeImplementation object: // the solver's NAME has to be unique - name = uniqueName( - SettingsConverter.readRawString(props, NAME, DEFAULT_NAME)); + String name = uniqueName(props.getString(NAME, DEFAULT_NAME)); // default solver COMMAND, TIMEOUT, parameters, VERSION parameter, solver INFO (some string) - command = - SettingsConverter.readRawString(props, COMMAND, DEFAULT_COMMAND); - timeout = SettingsConverter.read(props, TIMEOUT, DEFAULT_TIMEOUT); - if (timeout < -1) { - timeout = -1; - } - params = - SettingsConverter.readRawString(props, PARAMS, DEFAULT_PARAMS); - version = - SettingsConverter.readRawString(props, VERSION, DEFAULT_VERSION); - minVersion = SettingsConverter.readRawString(props, MIN_VERSION, - DEFAULT_MINIMUM_VERSION); - info = SettingsConverter.readRawString(props, INFO, DEFAULT_INFO); + String command = props.getString(COMMAND, DEFAULT_COMMAND); + long timeout = Math.max(-1, props.getLong(TIMEOUT, DEFAULT_TIMEOUT)); + + String params = props.getString(PARAMS, DEFAULT_PARAMS); + String version = props.getString(VERSION, DEFAULT_VERSION); + String minVersion = props.getString(MIN_VERSION, DEFAULT_MINIMUM_VERSION); + String info = props.getString(INFO, DEFAULT_INFO); // the solver socket used for communication with the created solver + String socketClassName = props.getString(SOLVER_SOCKET_CLASS, DEFAULT_SOLVER_SOCKET); try { - String socketClassName = SettingsConverter.readRawString(props, SOLVER_SOCKET_CLASS, - DEFAULT_SOLVER_SOCKET); solverSocketClass = ClassLoaderUtil.getClassforName(socketClassName); } catch (ClassNotFoundException e) { + LOGGER.error("Could not find solver socket class {}. Fallback to Z3Socket.class ", + socketClassName, e); solverSocketClass = Z3Socket.class; } // the message DELIMITERS used by the created solver in its stdout - delimiters = SettingsConverter.readRawStringList(props, DELIMITERS, - SPLIT, DEFAULT_DELIMITERS); + String[] delimiters = + props.getStringArray(SolverPropertiesLoader.DELIMITERS, new String[] { "\n", "\r" }); // the smt translator (class SMTTranslator) used by the created solver + String translatorClassName = props.getString(TRANSLATOR_CLASS, DEFAULT_TRANSLATOR); try { - String translatorClassName = - SettingsConverter.readRawString(props, TRANSLATOR_CLASS, DEFAULT_TRANSLATOR); translatorClass = ClassLoaderUtil.getClassforName(translatorClassName); } catch (ClassNotFoundException e) { + LOGGER.error( + "Could not find translator class {}; using ModularSMTLib2Translator.class.", + translatorClassName, e); translatorClass = ModularSMTLib2Translator.class; } // the SMTHandlers used by the created solver // note that this will only take effect when using ModularSMTLib2Translator ... - handlerNames = SettingsConverter.readRawStringList(props, - HANDLER_NAMES, SPLIT, new String[0]); - handlerOptions = SettingsConverter.readRawStringList(props, - HANDLER_OPTIONS, SPLIT, new String[0]); + String[] handlerNames = props.getStringArray(HANDLER_NAMES, new String[0]); + String[] handlerOptions = props.getStringArray(HANDLER_OPTIONS, new String[0]); // the solver specific preamble, may be null - preamble = SettingsConverter.readFile(props, PREAMBLE_FILE, null, - SolverPropertiesLoader.class.getClassLoader()); + String preambleFile = props.getString(PREAMBLE_FILE); + if (preambleFile != null) { + preamble = loadPreamble(preambleFile); + } // create the solver type return new SolverTypeImplementation(name, info, params, command, version, minVersion, @@ -310,64 +304,115 @@ private static SolverType makeSolver(Properties props) { preamble); } + private static @Nullable String loadPreamble(String preambleFile) { + final var FILE_PREFIX = "file:"; + if (preambleFile.startsWith(FILE_PREFIX)) { + preambleFile = preambleFile.substring(FILE_PREFIX.length()); + try { + return Files.readString(Paths.get(preambleFile)); + } catch (IOException e) { + LOGGER.info("Error reading file '{}' as preamble.", preambleFile, e); + return null; + } + } + + final var HTTP_PREFIX = "http:"; + if (preambleFile.startsWith(HTTP_PREFIX)) { + try (InputStream stream = URI.create(preambleFile).toURL().openStream()) { + return Streams.toString(stream); + } catch (IOException e) { + LOGGER.info("Could not read from URL '{}'.", + preambleFile, e); + } + } + + var loader = SolverPropertiesLoader.class.getClassLoader(); + var stream = loader.getResourceAsStream(preambleFile); + if (stream != null) { + try { + return Streams.toString(stream); + } catch (IOException e) { + LOGGER.error("Could not read preamble from classpath '{}.", preambleFile, e); + } + } + return null; + } + /** * Loads the solvers that are specified in .props files in resource packages named * "de/uka/ilkd/key/smt/solvertypes". */ - private static Collection loadSolvers() { - Collection completePropsList = new ArrayList<>(); + static Configuration loadSolvers() { try { - // load single solvers.txt files from the same location everywhere in the classpath - for (Iterator it = SolverPropertiesLoader.class.getClassLoader() - .getResources(PACKAGE_PATH + SOLVER_LIST_FILE).asIterator(); it.hasNext();) { - URL res = it.next(); + var filesInClasspath = + Streams.fromEnumerator(SolverPropertiesLoader.class.getClassLoader() + .getResources(PACKAGE_PATH + SOLVER_LIST_FILE)).toList(); + var solverFiles = new ArrayList<>(filesInClasspath); + + Path user = getUserSmtSolverPath(); + if (Files.exists(user)) { + LOGGER.info("Loading SMT solver definitions from {}", user); + solverFiles.add(user.toUri().toURL()); + } + + Path sysProp = getSystemPropertySmtSolverPath(); + if (sysProp != null && Files.exists(sysProp)) { + LOGGER.info("Loading SMT solver definitions from {}", sysProp); + solverFiles.add(sysProp.toUri().toURL()); + } + + Path local = getLocalSmtSolverPath(); + if (Files.exists(local)) { + LOGGER.info("Loading SMT solver definitions from {}", local); + solverFiles.add(local.toUri().toURL()); + } + + final Configuration solverConfiguration = new Configuration(); + + for (var res : solverFiles) { try (InputStream stream = res.openStream()) { - if (stream == null) { - continue; - } - // load solvers from this single solvers.txt - Collection props = new ArrayList<>(); - BufferedReader reader = - new BufferedReader(new InputStreamReader(stream, StandardCharsets.UTF_8)); - List propsNames = reader.lines().toList(); - for (String fileName : propsNames.stream().filter(n -> n.endsWith(".props")) - .toList()) { - Properties solverProp = new Properties(); - InputStream propsFile = - SolverPropertiesLoader.class.getResourceAsStream(fileName); - try { - solverProp.load(propsFile); - props.add(solverProp); - // Create a warning if unsupported keys occur in the loaded file. - Collection unsupportedKeys = SettingsConverter - .unsupportedPropertiesKeys(solverProp, SUPPORTED_KEYS); - if (!unsupportedKeys.isEmpty()) { - StringBuilder msg = new StringBuilder( - "Properties file " + fileName - + " contains unsupported keys: {"); - for (String key : unsupportedKeys) { - msg.append(key); - msg.append(", "); - } - msg.replace(msg.length() - 2, msg.length(), "}"); - LOGGER.warn(msg.toString()); - } - } catch (Exception e) { - // every possible exception should be caught as loading the files - // should not break key - // if loading the props file does not work for any reason, - // create a warning and continue - LOGGER.warn( - String.format("Solver file %s could not be loaded.", fileName)); - } + var config = ParsingFacade.readConfigurationFile( + CharStreams.fromStream(stream, StandardCharsets.UTF_8)); + + // Create a warning if unsupported keys occur in the loaded file. + Collection unsupportedKeys = SettingsConverter + .unsupportedPropertiesKeysInSubSections(config, SUPPORTED_KEYS); + if (!unsupportedKeys.isEmpty()) { + LOGGER.warn("File {} contains unsupported keys: {}", res, unsupportedKeys); } - completePropsList.addAll(props); + + solverConfiguration.overwriteWith(config); + } catch (IOException ex) { + throw new RuntimeException(ex); } } + return solverConfiguration; } catch (IOException e) { - throw new RuntimeException(e); + throw new RuntimeException("Could not load " + PACKAGE_PATH + SOLVER_LIST_FILE, e); } - return completePropsList; } + + /// Path for local smt solver definitions. Precedence over user and classpath smt solver + /// configs. + public static Path getLocalSmtSolverPath() { + return Paths.get(SOLVER_LIST_FILE); + } + + + /// Path for user-wide smt solver definitions. Precedence over classpath smt solver configs, + /// overwritten by local configs. + public static Path getUserSmtSolverPath() { + return PathConfig.getKeyConfigDir().resolve(SOLVER_LIST_FILE); + } + + + /// Path for smt solver definitions given per Java system properties. + public static @Nullable Path getSystemPropertySmtSolverPath() { + var path = System.getProperty(SYSTEM_PROPERTY_KEY_SMT_SOLVERS); + if (path != null) { + return Paths.get(path); + } + return null; + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/smt/solvertypes/SolverTypeImplementation.java b/key.core/src/main/java/de/uka/ilkd/key/smt/solvertypes/SolverTypeImplementation.java index ce2aa9eca2b..daf261994b2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/smt/solvertypes/SolverTypeImplementation.java +++ b/key.core/src/main/java/de/uka/ilkd/key/smt/solvertypes/SolverTypeImplementation.java @@ -206,7 +206,7 @@ public SolverTypeImplementation(String name, String info, String defaultParams, String defaultCommand, String versionParameter, String minimumSupportedVersion, long defaultTimeout, String[] delimiters, Class translatorClass, String[] handlerNames, String[] handlerOptions, Class solverSocketClass, - String preamble) { + @Nullable String preamble) { this.name = name; this.info = info; this.defaultParams = defaultParams; diff --git a/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/CVC4.props b/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/CVC4.props deleted file mode 100644 index 7e5e1a0f490..00000000000 --- a/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/CVC4.props +++ /dev/null @@ -1,23 +0,0 @@ -experimental=true -params=--no-print-success --produce-models --no-interactive --lang smt2 -timeout=-1 -name=CVC4 -info=CVC4 solver (https://cvc4.github.io/index.html). -command=cvc4 -version=--version -socketClass=de.uka.ilkd.key.smt.communication.CVC4Socket -handlers=de.uka.ilkd.key.smt.newsmt2.BooleanConnectiveHandler,\ -de.uka.ilkd.key.smt.newsmt2.PolymorphicHandler,\ -de.uka.ilkd.key.smt.newsmt2.QuantifierHandler,\ -de.uka.ilkd.key.smt.newsmt2.LogicalVariableHandler,\ -de.uka.ilkd.key.smt.newsmt2.NumberConstantsHandler,\ -de.uka.ilkd.key.smt.newsmt2.IntegerOpHandler,\ -de.uka.ilkd.key.smt.newsmt2.InstanceOfHandler,\ -de.uka.ilkd.key.smt.newsmt2.CastHandler,\ -de.uka.ilkd.key.smt.newsmt2.SumProdHandler,\ -de.uka.ilkd.key.smt.newsmt2.UpdateHandler,\ -de.uka.ilkd.key.smt.newsmt2.FieldConstantHandler,\ -de.uka.ilkd.key.smt.newsmt2.FloatHandler,\ -de.uka.ilkd.key.smt.newsmt2.CastingFunctionsHandler,\ -de.uka.ilkd.key.smt.newsmt2.DefinedSymbolsHandler,\ -de.uka.ilkd.key.smt.newsmt2.UninterpretedSymbolsHandler diff --git a/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/CVC4_legacy.props b/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/CVC4_legacy.props deleted file mode 100644 index e7e3247b88d..00000000000 --- a/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/CVC4_legacy.props +++ /dev/null @@ -1,9 +0,0 @@ -experimental=true -params=--no-print-success --produce-models --no-interactive --lang smt2 -timeout=-1 -name=CVC4 (Legacy Translation) -info=CVC4 solver -command=cvc4 -version=--version -socketClass=de.uka.ilkd.key.smt.communication.CVC4Socket -translatorClass=de.uka.ilkd.key.smt.SmtLib2Translator diff --git a/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/CVC5.props b/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/CVC5.props deleted file mode 100644 index 760e4eb3caf..00000000000 --- a/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/CVC5.props +++ /dev/null @@ -1,23 +0,0 @@ -params=--no-interactive --produce-models --lang smt2 -timeout=-1 -name=cvc5 -info=cvc5 solver (https://cvc5.github.io/). -command=cvc5 -version=--version -socketClass=de.uka.ilkd.key.smt.communication.Cvc5Socket -handlers=de.uka.ilkd.key.smt.newsmt2.BooleanConnectiveHandler,\ -de.uka.ilkd.key.smt.newsmt2.PolymorphicHandler,\ -de.uka.ilkd.key.smt.newsmt2.QuantifierHandler,\ -de.uka.ilkd.key.smt.newsmt2.LogicalVariableHandler,\ -de.uka.ilkd.key.smt.newsmt2.NumberConstantsHandler,\ -de.uka.ilkd.key.smt.newsmt2.IntegerOpHandler,\ -de.uka.ilkd.key.smt.newsmt2.InstanceOfHandler,\ -de.uka.ilkd.key.smt.newsmt2.CastHandler,\ -de.uka.ilkd.key.smt.newsmt2.SumProdHandler,\ -de.uka.ilkd.key.smt.newsmt2.UpdateHandler,\ -de.uka.ilkd.key.smt.newsmt2.FieldConstantHandler,\ -de.uka.ilkd.key.smt.newsmt2.FloatHandler,\ -de.uka.ilkd.key.smt.newsmt2.CastingFunctionsHandler,\ -de.uka.ilkd.key.smt.newsmt2.DefinedSymbolsHandler,\ -de.uka.ilkd.key.smt.newsmt2.UninterpretedSymbolsHandler -handlerOptions=getUnsatCore diff --git a/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/Princess.props b/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/Princess.props deleted file mode 100644 index 4f21c96075c..00000000000 --- a/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/Princess.props +++ /dev/null @@ -1,22 +0,0 @@ -params=+stdin -timeout=-1 -name=Princess -info=Princess solver by Philipp Ruemmer (http://www.philipp.ruemmer.org/princess.shtml). -command=princess -version=+version -minVersion=2021-11-15 -handlers=de.uka.ilkd.key.smt.newsmt2.BooleanConnectiveHandler,\ -de.uka.ilkd.key.smt.newsmt2.PolymorphicHandler,\ -de.uka.ilkd.key.smt.newsmt2.QuantifierHandler,\ -de.uka.ilkd.key.smt.newsmt2.LogicalVariableHandler,\ -de.uka.ilkd.key.smt.newsmt2.NumberConstantsHandler,\ -de.uka.ilkd.key.smt.newsmt2.IntegerOpHandler,\ -de.uka.ilkd.key.smt.newsmt2.InstanceOfHandler,\ -de.uka.ilkd.key.smt.newsmt2.CastHandler,\ -de.uka.ilkd.key.smt.newsmt2.SumProdHandler,\ -de.uka.ilkd.key.smt.newsmt2.UpdateHandler,\ -de.uka.ilkd.key.smt.newsmt2.FieldConstantHandler,\ -de.uka.ilkd.key.smt.newsmt2.FloatHandler,\ -de.uka.ilkd.key.smt.newsmt2.CastingFunctionsHandler,\ -de.uka.ilkd.key.smt.newsmt2.DefinedSymbolsHandler,\ -de.uka.ilkd.key.smt.newsmt2.UninterpretedSymbolsHandler \ No newline at end of file diff --git a/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/Z3.props b/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/Z3.props deleted file mode 100644 index 70bc70fd188..00000000000 --- a/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/Z3.props +++ /dev/null @@ -1,23 +0,0 @@ -params=-in -smt2 -timeout=-1 -name=Z3 -info=Z3 solver by Microsoft. -command=z3 -version=--version -minVersion=Z3 version 4.4.1 -handlers=de.uka.ilkd.key.smt.newsmt2.BooleanConnectiveHandler,\ -de.uka.ilkd.key.smt.newsmt2.PolymorphicHandler,\ -de.uka.ilkd.key.smt.newsmt2.QuantifierHandler,\ -de.uka.ilkd.key.smt.newsmt2.LogicalVariableHandler,\ -de.uka.ilkd.key.smt.newsmt2.NumberConstantsHandler,\ -de.uka.ilkd.key.smt.newsmt2.IntegerOpHandler,\ -de.uka.ilkd.key.smt.newsmt2.InstanceOfHandler,\ -de.uka.ilkd.key.smt.newsmt2.CastHandler,\ -de.uka.ilkd.key.smt.newsmt2.SumProdHandler,\ -de.uka.ilkd.key.smt.newsmt2.UpdateHandler,\ -de.uka.ilkd.key.smt.newsmt2.FieldConstantHandler,\ -de.uka.ilkd.key.smt.newsmt2.FloatHandler,\ -de.uka.ilkd.key.smt.newsmt2.CastingFunctionsHandler,\ -de.uka.ilkd.key.smt.newsmt2.DefinedSymbolsHandler,\ -de.uka.ilkd.key.smt.newsmt2.UninterpretedSymbolsHandler -handlerOptions=getUnsatCore \ No newline at end of file diff --git a/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/Z3_CE.props b/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/Z3_CE.props deleted file mode 100644 index a655591f324..00000000000 --- a/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/Z3_CE.props +++ /dev/null @@ -1,8 +0,0 @@ -params=-in -smt2 -timeout=-1 -name=Z3_CE -info=Z3 solver by Microsoft, used for counterexample generation. -command=z3 -version=--version -translatorClass=de.uka.ilkd.key.smt.SmtLib2Translator -socketClass=de.uka.ilkd.key.smt.communication.Z3CESocket diff --git a/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/Z3_FloatingPoint.props b/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/Z3_FloatingPoint.props deleted file mode 100644 index 22956fd8c96..00000000000 --- a/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/Z3_FloatingPoint.props +++ /dev/null @@ -1,11 +0,0 @@ -params=-in -smt2 -timeout=-1 -name=Z3_FP -info=Z3 solver by Microsoft, translating only floating point formulas. -command=z3 -version=-version -minVersion=Z3 version 4.4.1 -handlers=de.uka.ilkd.key.smt.newsmt2.BooleanConnectiveHandler,\ - de.uka.ilkd.key.smt.newsmt2.FloatHandler,\ - de.uka.ilkd.key.smt.newsmt2.FloatRemainderHandler -handlerOptions=getUnsatCore \ No newline at end of file diff --git a/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/Z3_QF.props b/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/Z3_QF.props deleted file mode 100644 index 1a6a8874eda..00000000000 --- a/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/Z3_QF.props +++ /dev/null @@ -1,22 +0,0 @@ -params=-in -smt2 -timeout=-1 -name=Z3_QF -info=Z3 solver by Microsoft. SMT translation of the sequent excludes quantified terms, making this variant much faster for certain problems. -command=z3 -version=--version -minVersion=Z3 version 4.4.1 -handlers=de.uka.ilkd.key.smt.newsmt2.BooleanConnectiveHandler,\ -de.uka.ilkd.key.smt.newsmt2.PolymorphicHandler,\ -de.uka.ilkd.key.smt.newsmt2.LogicalVariableHandler,\ -de.uka.ilkd.key.smt.newsmt2.NumberConstantsHandler,\ -de.uka.ilkd.key.smt.newsmt2.IntegerOpHandler,\ -de.uka.ilkd.key.smt.newsmt2.InstanceOfHandler,\ -de.uka.ilkd.key.smt.newsmt2.CastHandler,\ -de.uka.ilkd.key.smt.newsmt2.SumProdHandler,\ -de.uka.ilkd.key.smt.newsmt2.UpdateHandler,\ -de.uka.ilkd.key.smt.newsmt2.FieldConstantHandler,\ -de.uka.ilkd.key.smt.newsmt2.FloatHandler,\ -de.uka.ilkd.key.smt.newsmt2.CastingFunctionsHandler,\ -de.uka.ilkd.key.smt.newsmt2.DefinedSymbolsHandler,\ -de.uka.ilkd.key.smt.newsmt2.UninterpretedSymbolsHandler -handlerOptions=getUnsatCore diff --git a/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/Z3_legacy.props b/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/Z3_legacy.props deleted file mode 100644 index bd63ac4b0c0..00000000000 --- a/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/Z3_legacy.props +++ /dev/null @@ -1,9 +0,0 @@ -experimental=true -params=-in -smt2 -timeout=-1 -name=Z3 (Legacy Translation) -info=Z3 solver by Microsoft, using the old SMT translation. -command=z3 -version=--version -translatorClass=de.uka.ilkd.key.smt.SmtLib2Translator - diff --git a/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/smt-solvers.json b/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/smt-solvers.json new file mode 100644 index 00000000000..3147944933c --- /dev/null +++ b/key.core/src/main/resources/de/uka/ilkd/key/smt/solvertypes/smt-solvers.json @@ -0,0 +1,182 @@ +{ + "CVC4": { + "experimental": true, + "params": "--no-print-success --produce-models --no-interactive --lang smt2", + "timeout": -1, + "name": "CVC4", + "info": "CVC4 solver (https://cvc4.github.io/index.html).", + "command": "cvc4", + "version": "--version", + "socketClass": "de.uka.ilkd.key.smt.communication.CVC4Socket", + "handlers": [ + "de.uka.ilkd.key.smt.newsmt2.BooleanConnectiveHandler", + "de.uka.ilkd.key.smt.newsmt2.PolymorphicHandler", + "de.uka.ilkd.key.smt.newsmt2.QuantifierHandler", + "de.uka.ilkd.key.smt.newsmt2.LogicalVariableHandler", + "de.uka.ilkd.key.smt.newsmt2.NumberConstantsHandler", + "de.uka.ilkd.key.smt.newsmt2.IntegerOpHandler", + "de.uka.ilkd.key.smt.newsmt2.InstanceOfHandler", + "de.uka.ilkd.key.smt.newsmt2.CastHandler", + "de.uka.ilkd.key.smt.newsmt2.SumProdHandler", + "de.uka.ilkd.key.smt.newsmt2.UpdateHandler", + "de.uka.ilkd.key.smt.newsmt2.FieldConstantHandler", + "de.uka.ilkd.key.smt.newsmt2.FloatHandler", + "de.uka.ilkd.key.smt.newsmt2.CastingFunctionsHandler", + "de.uka.ilkd.key.smt.newsmt2.DefinedSymbolsHandler", + "de.uka.ilkd.key.smt.newsmt2.UninterpretedSymbolsHandler" + ] + }, + "CVC4Legacy": { + "experimental": true, + "params": "--no-print-success --produce-models --no-interactive --lang smt2", + "timeout": -1, + "name": "CVC4 (Legacy Translation)", + "info": "CVC4 solver", + "command": "cvc4", + "version": "--version", + "socketClass": "de.uka.ilkd.key.smt.communication.CVC4Socket", + "translatorClass": "de.uka.ilkd.key.smt.SmtLib2Translator" + }, + "CVC5": { + "params": "--no-interactive --produce-models --lang smt2", + "timeout": -1, + "name": "cvc5", + "info": "cvc5 solver (https://cvc5.github.io/).", + "command": "cvc5", + "version": "--version", + "socketClass": "de.uka.ilkd.key.smt.communication.Cvc5Socket", + "handlerOptions":["getUnsatCore"], + "handlers": [ + "de.uka.ilkd.key.smt.newsmt2.BooleanConnectiveHandler", + "de.uka.ilkd.key.smt.newsmt2.PolymorphicHandler", + "de.uka.ilkd.key.smt.newsmt2.QuantifierHandler", + "de.uka.ilkd.key.smt.newsmt2.LogicalVariableHandler", + "de.uka.ilkd.key.smt.newsmt2.NumberConstantsHandler", + "de.uka.ilkd.key.smt.newsmt2.IntegerOpHandler", + "de.uka.ilkd.key.smt.newsmt2.InstanceOfHandler", + "de.uka.ilkd.key.smt.newsmt2.CastHandler", + "de.uka.ilkd.key.smt.newsmt2.SumProdHandler", + "de.uka.ilkd.key.smt.newsmt2.UpdateHandler", + "de.uka.ilkd.key.smt.newsmt2.FieldConstantHandler", + "de.uka.ilkd.key.smt.newsmt2.FloatHandler", + "de.uka.ilkd.key.smt.newsmt2.CastingFunctionsHandler", + "de.uka.ilkd.key.smt.newsmt2.DefinedSymbolsHandler", + "de.uka.ilkd.key.smt.newsmt2.UninterpretedSymbolsHandler" + ] + }, + "Princess": { + "params": "+stdin", + "timeout": -1, + "name": "Princess", + "info": "Princess solver by Philipp Ruemmer (http://www.philipp.ruemmer.org/princess.shtml).", + "command": "princess", + "version": "+version", + "minVersion": "2021-11-15", + "handlers": [ + "de.uka.ilkd.key.smt.newsmt2.BooleanConnectiveHandler", + "de.uka.ilkd.key.smt.newsmt2.PolymorphicHandler", + "de.uka.ilkd.key.smt.newsmt2.QuantifierHandler", + "de.uka.ilkd.key.smt.newsmt2.LogicalVariableHandler", + "de.uka.ilkd.key.smt.newsmt2.NumberConstantsHandler", + "de.uka.ilkd.key.smt.newsmt2.IntegerOpHandler", + "de.uka.ilkd.key.smt.newsmt2.InstanceOfHandler", + "de.uka.ilkd.key.smt.newsmt2.CastHandler", + "de.uka.ilkd.key.smt.newsmt2.SumProdHandler", + "de.uka.ilkd.key.smt.newsmt2.UpdateHandler", + "de.uka.ilkd.key.smt.newsmt2.FieldConstantHandler", + "de.uka.ilkd.key.smt.newsmt2.FloatHandler", + "de.uka.ilkd.key.smt.newsmt2.CastingFunctionsHandler", + "de.uka.ilkd.key.smt.newsmt2.DefinedSymbolsHandler", + "de.uka.ilkd.key.smt.newsmt2.UninterpretedSymbolsHandler" + ] + }, + "Z3": { + "params": "-in -smt2", + "timeout": -1, + "name": "Z3", + "info": "Z3 solver by Microsoft.", + "command": "z3", + "version": "--version", + "minVersion": "Z3 version 4.4.1", + "handlers": [ + "de.uka.ilkd.key.smt.newsmt2.BooleanConnectiveHandler", + "de.uka.ilkd.key.smt.newsmt2.PolymorphicHandler", + "de.uka.ilkd.key.smt.newsmt2.QuantifierHandler", + "de.uka.ilkd.key.smt.newsmt2.LogicalVariableHandler", + "de.uka.ilkd.key.smt.newsmt2.NumberConstantsHandler", + "de.uka.ilkd.key.smt.newsmt2.IntegerOpHandler", + "de.uka.ilkd.key.smt.newsmt2.InstanceOfHandler", + "de.uka.ilkd.key.smt.newsmt2.CastHandler", + "de.uka.ilkd.key.smt.newsmt2.SumProdHandler", + "de.uka.ilkd.key.smt.newsmt2.UpdateHandler", + "de.uka.ilkd.key.smt.newsmt2.FieldConstantHandler", + "de.uka.ilkd.key.smt.newsmt2.FloatHandler", + "de.uka.ilkd.key.smt.newsmt2.CastingFunctionsHandler", + "de.uka.ilkd.key.smt.newsmt2.DefinedSymbolsHandler", + "de.uka.ilkd.key.smt.newsmt2.UninterpretedSymbolsHandler" + ], + "handlerOptions": ["getUnsatCore"] + }, + "Z3_QF": { + "params": "-in -smt2", + "timeout": -1, + "name": "Z3_QF", + "info": "Z3 solver by Microsoft. SMT translation of the sequent excludes quantified terms, making this variant much faster for certain problems.", + "command": "z3", + "version": "--version", + "minVersion": "Z3 version 4.4.1", + "handlers": [ + "de.uka.ilkd.key.smt.newsmt2.BooleanConnectiveHandler", + "de.uka.ilkd.key.smt.newsmt2.PolymorphicHandler", + "de.uka.ilkd.key.smt.newsmt2.QuantifierHandler", + "de.uka.ilkd.key.smt.newsmt2.LogicalVariableHandler", + "de.uka.ilkd.key.smt.newsmt2.NumberConstantsHandler", + "de.uka.ilkd.key.smt.newsmt2.IntegerOpHandler", + "de.uka.ilkd.key.smt.newsmt2.InstanceOfHandler", + "de.uka.ilkd.key.smt.newsmt2.CastHandler", + "de.uka.ilkd.key.smt.newsmt2.SumProdHandler", + "de.uka.ilkd.key.smt.newsmt2.UpdateHandler", + "de.uka.ilkd.key.smt.newsmt2.FieldConstantHandler", + "de.uka.ilkd.key.smt.newsmt2.FloatHandler", + "de.uka.ilkd.key.smt.newsmt2.CastingFunctionsHandler", + "de.uka.ilkd.key.smt.newsmt2.DefinedSymbolsHandler", + "de.uka.ilkd.key.smt.newsmt2.UninterpretedSymbolsHandler" + ], + "handlerOptions": ["getUnsatCore"] + }, + "Z3Legacy": { + "experimental": true, + "params": "-in -smt2", + "timeout": -1, + "name": "Z3 (Legacy Translation)", + "info": "Z3 solver by Microsoft, using the old SMT translation.", + "command": "z3", + "version": "--version", + "translatorClass": "de.uka.ilkd.key.smt.SmtLib2Translator" + }, + "Z3_CE": { + "params": "-in -smt2", + "timeout": -1, + "name": "Z3_CE", + "info": "Z3 solver by Microsoft, used for counterexample generation.", + "command": "z3", + "version": "--version", + "translatorClass": "de.uka.ilkd.key.smt.SmtLib2Translator", + "socketClass": "de.uka.ilkd.key.smt.communication.Z3CESocket" + }, + "Z3_FloatingPoint": { + "params": "-in -smt2", + "timeout": -1, + "name": "Z3_FP", + "info": "Z3 solver by Microsoft, translating only floating point formulas.", + "command": "z3", + "version": "--version", + "minVersion": "Z3 version 4.4.1", + "handlers": [ + "de.uka.ilkd.key.smt.newsmt2.BooleanConnectiveHandler", + "de.uka.ilkd.key.smt.newsmt2.FloatHandler", + "de.uka.ilkd.key.smt.newsmt2.FloatRemainderHandler" + ], + "handlerOptions": ["getUnsatCore"] + } +} \ No newline at end of file diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/TestSMTFocusResults.java b/key.core/src/test/java/de/uka/ilkd/key/smt/TestSMTFocusResults.java index 7ef74bb69ff..349a6b3ff2d 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/TestSMTFocusResults.java +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/TestSMTFocusResults.java @@ -3,9 +3,10 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.smt; -import org.junit.jupiter.api.Assertions; import org.junit.jupiter.api.Test; +import static org.assertj.core.api.Assertions.assertThat; + /** * Tests for {@link SMTFocusResults}. */ @@ -13,8 +14,8 @@ class TestSMTFocusResults { @Test void parsesZ3Format() { String z3Output = "(L_1 L_17 L_23)"; - Integer[] result = SMTFocusResults.parseZ3Format(z3Output); - Assertions.assertArrayEquals(new Integer[] { 1, 17, 23 }, result); + var result = SMTFocusResults.parseZ3Format(z3Output); + assertThat(result).containsOnly(1, 17, 23); } @Test @@ -26,7 +27,7 @@ void parsesCvc5Format() { "L_23", ")" }; - Integer[] result = SMTFocusResults.parseCVC5Format(cvc5Output); - Assertions.assertArrayEquals(new Integer[] { 5, 12, 23 }, result); + var result = SMTFocusResults.parseCVC5Format(cvc5Output); + assertThat(result).containsOnly(5, 12, 23); } } 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 37c4ee5db0b..75771e6eb17 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 @@ -4,6 +4,7 @@ package de.uka.ilkd.key.smt; import java.nio.file.Path; +import java.util.Objects; import de.uka.ilkd.key.control.DefaultUserInterfaceControl; import de.uka.ilkd.key.control.KeYEnvironment; @@ -16,14 +17,17 @@ import org.key_project.util.collection.ImmutableList; import org.key_project.util.helper.FindResources; -import org.junit.jupiter.api.Assertions; import org.junit.jupiter.api.Test; +import static org.assertj.core.api.Assertions.assertThat; +import static org.junit.jupiter.api.Assertions.*; + /** * Tests for the unsat core saving infrastructure. */ class TestUnsatCore { - private static final Path testCaseDirectory = FindResources.getTestCasesDirectory(); + private static final Path testCaseDirectory = + Objects.requireNonNull(FindResources.getTestCasesDirectory()); @Test void testUnsatCore() throws ProblemLoaderException { @@ -31,26 +35,23 @@ void testUnsatCore() throws ProblemLoaderException { KeYEnvironment env = KeYEnvironment.load(testCaseDirectory.resolve("smt/unsatCore.proof")); - Assertions.assertNotNull(env.getLoadedProof()); - Assertions.assertTrue(env.getLoadedProof().closed()); + assertNotNull(env.getLoadedProof()); + assertTrue(env.getLoadedProof().closed()); // find the SMT rule app Proof p = env.getLoadedProof(); Node n = p.findAny(node -> node.getAppliedRuleApp() instanceof SMTRuleApp); + assertNotNull(n); SMTRuleApp app = ((SMTRuleApp) n.getAppliedRuleApp()); - Assertions.assertEquals("Z3", app.getSuccessfulSolverName()); + System.out.println(app); + assertEquals("Z3", app.getSuccessfulSolverName()); ImmutableList ifs = app.assumesInsts(); - Assertions.assertTrue( - ifs.contains(PosInOccurrence.findInSequent(n.sequent(), 1, - PosInTerm.getTopLevel()))); - Assertions.assertTrue( - ifs.contains(PosInOccurrence.findInSequent(n.sequent(), 2, - PosInTerm.getTopLevel()))); - Assertions.assertTrue( - ifs.contains(PosInOccurrence.findInSequent(n.sequent(), 3, - PosInTerm.getTopLevel()))); - Assertions.assertTrue( - ifs.contains(PosInOccurrence.findInSequent(n.sequent(), 7, PosInTerm.getTopLevel()))); - Assertions.assertEquals(4, ifs.size()); + var pio1 = PosInOccurrence.findInSequent(n.sequent(), 1, PosInTerm.getTopLevel()); + var pio2 = PosInOccurrence.findInSequent(n.sequent(), 2, PosInTerm.getTopLevel()); + var pio3 = PosInOccurrence.findInSequent(n.sequent(), 3, PosInTerm.getTopLevel()); + var pio7 = PosInOccurrence.findInSequent(n.sequent(), 7, PosInTerm.getTopLevel()); + + assertEquals(4, ifs.size()); + assertThat(ifs).containsExactlyInAnyOrder(pio1, pio2, pio3, pio7); } } diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/solvertypes/SolverPropertiesLoaderTest.java b/key.core/src/test/java/de/uka/ilkd/key/smt/solvertypes/SolverPropertiesLoaderTest.java new file mode 100644 index 00000000000..756c801fa7a --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/solvertypes/SolverPropertiesLoaderTest.java @@ -0,0 +1,241 @@ +/* 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.solvertypes; + +import de.uka.ilkd.key.settings.Configuration; + +import org.junit.jupiter.api.Test; + +import static org.assertj.core.api.Assertions.assertThat; +import static org.junit.jupiter.api.Assertions.*; + +/** + * @author Alexander Weigl + * @version 1 (6/14/25) + */ +class SolverPropertiesLoaderTest { + private Configuration config = SolverPropertiesLoader.loadSolvers(); + + @Test + void loadCVC4() { + var cvc4 = config.getSection("CVC4"); + assertNotNull(cvc4); + assertEquals("de.uka.ilkd.key.smt.communication.CVC4Socket", cvc4.getString("socketClass")); + assertEquals("CVC4", cvc4.getString("name")); + assertTrue(cvc4.getBool("experimental")); + assertEquals("--no-print-success --produce-models --no-interactive --lang smt2", + cvc4.getString("params")); + assertEquals("--version", cvc4.getString("version")); + assertEquals("cvc4", cvc4.getString("command")); + assertEquals(-1, cvc4.getInt("timeout")); + + assertThat(cvc4.getStringList("handlers")) + .containsExactly( + "de.uka.ilkd.key.smt.newsmt2.BooleanConnectiveHandler", + "de.uka.ilkd.key.smt.newsmt2.PolymorphicHandler", + "de.uka.ilkd.key.smt.newsmt2.QuantifierHandler", + "de.uka.ilkd.key.smt.newsmt2.LogicalVariableHandler", + "de.uka.ilkd.key.smt.newsmt2.NumberConstantsHandler", + "de.uka.ilkd.key.smt.newsmt2.IntegerOpHandler", + "de.uka.ilkd.key.smt.newsmt2.InstanceOfHandler", + "de.uka.ilkd.key.smt.newsmt2.CastHandler", + "de.uka.ilkd.key.smt.newsmt2.SumProdHandler", + "de.uka.ilkd.key.smt.newsmt2.UpdateHandler", + "de.uka.ilkd.key.smt.newsmt2.FieldConstantHandler", + "de.uka.ilkd.key.smt.newsmt2.FloatHandler", + "de.uka.ilkd.key.smt.newsmt2.CastingFunctionsHandler", + "de.uka.ilkd.key.smt.newsmt2.DefinedSymbolsHandler", + "de.uka.ilkd.key.smt.newsmt2.UninterpretedSymbolsHandler"); + } + + @Test + void loadCVC4Legacy() { + var cvc4 = config.getSection("CVC4Legacy"); + assertNotNull(cvc4); + assertEquals("de.uka.ilkd.key.smt.communication.CVC4Socket", cvc4.getString("socketClass")); + assertEquals("CVC4 (Legacy Translation)", cvc4.getString("name")); + assertEquals("de.uka.ilkd.key.smt.SmtLib2Translator", cvc4.getString("translatorClass")); + assertTrue(cvc4.getBool("experimental")); + assertEquals("--no-print-success --produce-models --no-interactive --lang smt2", + cvc4.getString("params")); + assertEquals("--version", cvc4.getString("version")); + assertEquals("cvc4", cvc4.getString("command")); + assertEquals(-1, cvc4.getInt("timeout")); + } + + @Test + void loadCVC5() { + var cvc5 = config.getSection("CVC5"); + assertNotNull(cvc5); + assertEquals("de.uka.ilkd.key.smt.communication.Cvc5Socket", cvc5.getString("socketClass")); + assertEquals("cvc5", cvc5.getString("name")); + assertEquals("--no-interactive --produce-models --lang smt2", cvc5.getString("params")); + assertEquals("--version", cvc5.getString("version")); + assertEquals("cvc5", cvc5.getString("command")); + assertEquals(-1, cvc5.getInt("timeout")); + assertThat(cvc5.getStringList("handlerOptions")).containsExactly("getUnsatCore"); + + + assertThat(cvc5.getStringList("handlers")) + .containsExactly( + "de.uka.ilkd.key.smt.newsmt2.BooleanConnectiveHandler", + "de.uka.ilkd.key.smt.newsmt2.PolymorphicHandler", + "de.uka.ilkd.key.smt.newsmt2.QuantifierHandler", + "de.uka.ilkd.key.smt.newsmt2.LogicalVariableHandler", + "de.uka.ilkd.key.smt.newsmt2.NumberConstantsHandler", + "de.uka.ilkd.key.smt.newsmt2.IntegerOpHandler", + "de.uka.ilkd.key.smt.newsmt2.InstanceOfHandler", + "de.uka.ilkd.key.smt.newsmt2.CastHandler", + "de.uka.ilkd.key.smt.newsmt2.SumProdHandler", + "de.uka.ilkd.key.smt.newsmt2.UpdateHandler", + "de.uka.ilkd.key.smt.newsmt2.FieldConstantHandler", + "de.uka.ilkd.key.smt.newsmt2.FloatHandler", + "de.uka.ilkd.key.smt.newsmt2.CastingFunctionsHandler", + "de.uka.ilkd.key.smt.newsmt2.DefinedSymbolsHandler", + "de.uka.ilkd.key.smt.newsmt2.UninterpretedSymbolsHandler"); + } + + @Test + void loadPrincess() { + var princess = config.getSection("Princess"); + + + assertNotNull(princess); + assertEquals("2021-11-15", princess.getString("minVersion")); + assertEquals("Princess", princess.getString("name")); + assertFalse(princess.getBool("experimental", false)); + assertEquals("+stdin", princess.getString("params")); + assertEquals("+version", princess.getString("version")); + assertEquals("princess", princess.getString("command")); + assertEquals(-1, princess.getInt("timeout")); + + assertThat(princess.getStringList("handlers")) + .containsExactly( + "de.uka.ilkd.key.smt.newsmt2.BooleanConnectiveHandler", + "de.uka.ilkd.key.smt.newsmt2.PolymorphicHandler", + "de.uka.ilkd.key.smt.newsmt2.QuantifierHandler", + "de.uka.ilkd.key.smt.newsmt2.LogicalVariableHandler", + "de.uka.ilkd.key.smt.newsmt2.NumberConstantsHandler", + "de.uka.ilkd.key.smt.newsmt2.IntegerOpHandler", + "de.uka.ilkd.key.smt.newsmt2.InstanceOfHandler", + "de.uka.ilkd.key.smt.newsmt2.CastHandler", + "de.uka.ilkd.key.smt.newsmt2.SumProdHandler", + "de.uka.ilkd.key.smt.newsmt2.UpdateHandler", + "de.uka.ilkd.key.smt.newsmt2.FieldConstantHandler", + "de.uka.ilkd.key.smt.newsmt2.FloatHandler", + "de.uka.ilkd.key.smt.newsmt2.CastingFunctionsHandler", + "de.uka.ilkd.key.smt.newsmt2.DefinedSymbolsHandler", + "de.uka.ilkd.key.smt.newsmt2.UninterpretedSymbolsHandler"); + + } + + @Test + void loadZ3() { + var z3 = config.getSection("Z3"); + + + assertNotNull(z3); + assertEquals("Z3 version 4.4.1", z3.getString("minVersion")); + assertEquals("Z3", z3.getString("name")); + assertFalse(z3.getBool("experimental", false)); + assertEquals("-in -smt2", z3.getString("params")); + assertEquals("--version", z3.getString("version")); + assertEquals("z3", z3.getString("command")); + assertEquals(-1, z3.getInt("timeout")); + assertThat(z3.getStringList("handlerOptions")).containsExactly("getUnsatCore"); + + assertThat(z3.getStringList("handlers")).containsExactly( + "de.uka.ilkd.key.smt.newsmt2.BooleanConnectiveHandler", + "de.uka.ilkd.key.smt.newsmt2.PolymorphicHandler", + "de.uka.ilkd.key.smt.newsmt2.QuantifierHandler", + "de.uka.ilkd.key.smt.newsmt2.LogicalVariableHandler", + "de.uka.ilkd.key.smt.newsmt2.NumberConstantsHandler", + "de.uka.ilkd.key.smt.newsmt2.IntegerOpHandler", + "de.uka.ilkd.key.smt.newsmt2.InstanceOfHandler", + "de.uka.ilkd.key.smt.newsmt2.CastHandler", + "de.uka.ilkd.key.smt.newsmt2.SumProdHandler", + "de.uka.ilkd.key.smt.newsmt2.UpdateHandler", + "de.uka.ilkd.key.smt.newsmt2.FieldConstantHandler", + "de.uka.ilkd.key.smt.newsmt2.FloatHandler", + "de.uka.ilkd.key.smt.newsmt2.CastingFunctionsHandler", + "de.uka.ilkd.key.smt.newsmt2.DefinedSymbolsHandler", + "de.uka.ilkd.key.smt.newsmt2.UninterpretedSymbolsHandler"); + } + + @Test + void loadZ3CE() { + var z3 = config.getSection("Z3_CE"); + assertNotNull(z3); + assertEquals("Z3_CE", z3.getString("name")); + assertEquals("de.uka.ilkd.key.smt.communication.Z3CESocket", z3.getString("socketClass")); + assertEquals("de.uka.ilkd.key.smt.SmtLib2Translator", z3.getString("translatorClass")); + assertEquals("-in -smt2", z3.getString("params")); + assertEquals("--version", z3.getString("version")); + assertEquals("z3", z3.getString("command")); + assertEquals(-1, z3.getInt("timeout")); + } + + @Test + void loadZ3FP() { + var z3 = config.getSection("Z3_FloatingPoint"); + + assertNotNull(z3); + assertEquals("Z3_FP", z3.getString("name")); + assertEquals("-in -smt2", z3.getString("params")); + assertEquals("--version", z3.getString("version")); + assertEquals("z3", z3.getString("command")); + assertEquals(-1, z3.getInt("timeout")); + assertThat(z3.getStringList("handlerOptions")).containsExactly("getUnsatCore"); + + assertThat(z3.getStringList("handlers")).containsExactly( + "de.uka.ilkd.key.smt.newsmt2.BooleanConnectiveHandler", + "de.uka.ilkd.key.smt.newsmt2.FloatHandler", + "de.uka.ilkd.key.smt.newsmt2.FloatRemainderHandler"); + } + + @Test + void loadZ3QF() { + var z3 = config.getSection("Z3_QF"); + + + assertNotNull(z3); + assertEquals("Z3_QF", z3.getString("name")); + assertEquals("-in -smt2", z3.getString("params")); + assertEquals("--version", z3.getString("version")); + assertEquals("z3", z3.getString("command")); + assertEquals(-1, z3.getInt("timeout")); + assertThat(z3.getStringList("handlerOptions")).containsExactly("getUnsatCore"); + + assertThat(z3.getStringList("handlers")).containsExactly( + "de.uka.ilkd.key.smt.newsmt2.BooleanConnectiveHandler", + "de.uka.ilkd.key.smt.newsmt2.PolymorphicHandler", + "de.uka.ilkd.key.smt.newsmt2.QuantifierHandler", + "de.uka.ilkd.key.smt.newsmt2.LogicalVariableHandler", + "de.uka.ilkd.key.smt.newsmt2.NumberConstantsHandler", + "de.uka.ilkd.key.smt.newsmt2.IntegerOpHandler", + "de.uka.ilkd.key.smt.newsmt2.InstanceOfHandler", + "de.uka.ilkd.key.smt.newsmt2.CastHandler", + "de.uka.ilkd.key.smt.newsmt2.SumProdHandler", + "de.uka.ilkd.key.smt.newsmt2.UpdateHandler", + "de.uka.ilkd.key.smt.newsmt2.FieldConstantHandler", + "de.uka.ilkd.key.smt.newsmt2.FloatHandler", + "de.uka.ilkd.key.smt.newsmt2.CastingFunctionsHandler", + "de.uka.ilkd.key.smt.newsmt2.DefinedSymbolsHandler", + "de.uka.ilkd.key.smt.newsmt2.UninterpretedSymbolsHandler"); + } + + @Test + void loadZ3Legacy() { + var z3 = config.getSection("Z3Legacy"); + assertNotNull(z3); + assertEquals("Z3 (Legacy Translation)", z3.getString("name")); + assertEquals("de.uka.ilkd.key.smt.SmtLib2Translator", z3.getString("translatorClass")); + assertTrue(z3.getBool("experimental")); + assertEquals("-in -smt2", z3.getString("params")); + assertEquals("--version", z3.getString("version")); + assertEquals("z3", z3.getString("command")); + assertEquals(-1, z3.getInt("timeout")); + + } +} diff --git a/key.ui/src/main/java/de/uka/ilkd/key/core/Log.java b/key.ui/src/main/java/de/uka/ilkd/key/core/Log.java index 97593bbba76..5fd6dd3d249 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/core/Log.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/core/Log.java @@ -71,7 +71,7 @@ public static void configureLogging(@Nullable Integer verbosity) { } private static void cleanOldLogFiles() { - var logDir = PathConfig.getLogDirectory().toPath(); + var logDir = PathConfig.getLogDirectory(); try (var files = Files.list(logDir)) { var duration = Duration.of(14, ChronoUnit.DAYS); var refDate = Instant.now().minus(duration); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java index 2cfc2fa0888..b38d85ef33d 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java @@ -5,6 +5,7 @@ import java.awt.event.ActionListener; import java.io.*; +import java.nio.file.Files; import java.nio.file.Path; import java.nio.file.Paths; import java.util.HashMap; @@ -18,6 +19,7 @@ import de.uka.ilkd.key.settings.Configuration; import de.uka.ilkd.key.settings.PathConfig; +import org.jspecify.annotations.Nullable; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -200,9 +202,9 @@ public JMenu getMenu() { /** * read the recent files from the given properties file */ - public final void loadFrom(String filename) { + public final void loadFrom(Path filename) { try { - var c = Configuration.load(new File(filename)); + var c = Configuration.load(filename); c.getStringList("recentFiles").forEach(this::addRecentFileNoSave); } catch (FileNotFoundException ex) { LOGGER.debug("Could not read RecentFileList. Did not find file {}", filename); @@ -214,6 +216,7 @@ public final void loadFrom(String filename) { /** * @return the absolute path to the most recently opened file (maybe null) */ + @Nullable public String getMostRecent() { return mostRecentFile != null ? mostRecentFile.getAbsolutePath() : null; } @@ -222,15 +225,14 @@ public String getMostRecent() { * write the recent file names to the given properties file. the file will be read (if it * exists) and then re-written so no information will be lost. */ - public void store(String filename) { - File localRecentFiles = new File(filename); + public void store(Path filename) { Configuration c = new Configuration(); var seq = menuItemToRecentFile.values().stream() .map(RecentFileEntry::getAbsolutePath) .collect(Collectors.toList()); c.set("recentFiles", seq); - try (var fin = new BufferedWriter(new FileWriter(localRecentFiles))) { + try (var fin = Files.newBufferedWriter(filename)) { c.save(fin, ""); } catch (IOException ex) { LOGGER.info("Could not write recent files list ", ex); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/colors/ColorSettings.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/colors/ColorSettings.java index 440eede3339..7e91735a109 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/colors/ColorSettings.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/colors/ColorSettings.java @@ -6,10 +6,10 @@ import java.awt.*; import java.beans.PropertyChangeListener; import java.beans.PropertyChangeSupport; -import java.io.File; -import java.io.FileWriter; import java.io.IOException; import java.io.Writer; +import java.nio.file.Files; +import java.nio.file.Path; import java.util.*; import java.util.List; import java.util.stream.Stream; @@ -31,8 +31,8 @@ * @version 1 (10.05.19) */ public class ColorSettings { - public static final File SETTINGS_FILE_NEW = - new File(PathConfig.getKeyConfigDir(), "colors.json"); + public static final Path SETTINGS_FILE_NEW = + PathConfig.getKeyConfigDir().resolve("colors.json"); private static final Logger LOGGER = LoggerFactory.getLogger(ColorSettings.class); private static ColorSettings INSTANCE; @@ -47,7 +47,7 @@ public ColorSettings(Configuration load) { public static ColorSettings getInstance() { if (INSTANCE == null) { - if (SETTINGS_FILE_NEW.exists()) { + if (Files.exists(SETTINGS_FILE_NEW)) { try { LOGGER.info("Load color settings from file {}", SETTINGS_FILE_NEW); INSTANCE = new ColorSettings(Configuration.load(SETTINGS_FILE_NEW)); @@ -94,8 +94,8 @@ public static Color invert(Color c) { * @see #SETTINGS_FILE_NEW */ public void save() { - LOGGER.info("Save color settings to: {}", SETTINGS_FILE_NEW.getAbsolutePath()); - try (Writer writer = new FileWriter(SETTINGS_FILE_NEW)) { + LOGGER.info("Save color settings to: {}", SETTINGS_FILE_NEW.toAbsolutePath()); + try (Writer writer = Files.newBufferedWriter(SETTINGS_FILE_NEW)) { var config = new Configuration(properties); config.save(writer, "KeY's Colors"); writer.flush(); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/colors/ColorSettingsProvider.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/colors/ColorSettingsProvider.java index b0d57638b58..c790935261e 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/colors/ColorSettingsProvider.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/colors/ColorSettingsProvider.java @@ -31,7 +31,7 @@ public ColorSettingsProvider() { super(); setHeaderText(getDescription()); setSubHeaderText( - "Color settings are stored in: " + ColorSettings.SETTINGS_FILE_NEW.getAbsolutePath()); + "Color settings are stored in: " + ColorSettings.SETTINGS_FILE_NEW.toAbsolutePath()); add(new JScrollPane(tblColors)); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingLayout.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingLayout.java index 3c13e2fc612..5f884a87e5c 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingLayout.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingLayout.java @@ -7,8 +7,9 @@ import java.awt.event.ActionEvent; import java.awt.event.InputEvent; import java.awt.event.KeyEvent; -import java.io.File; import java.io.IOException; +import java.nio.file.Files; +import java.nio.file.Path; import java.util.*; import java.util.List; import javax.swing.*; @@ -45,7 +46,7 @@ public final class DockingLayout implements KeYGuiExtension, KeYGuiExtension.Sta private static final Logger LOGGER = LoggerFactory.getLogger(DockingLayout.class); private static final float SIZE_ICON_DOCK = 12f; - private static final File LAYOUT_FILE = new File(PathConfig.getKeyConfigDir(), "layout.xml"); + private static final Path LAYOUT_FILE = PathConfig.getKeyConfigDir().resolve("layout.xml"); private static final String[] LAYOUT_NAMES = { "Default", "Slot 1", "Slot 2" }; private static final int[] LAYOUT_KEYS = { KeyEvent.VK_F10, KeyEvent.VK_F11, KeyEvent.VK_F12 }; @@ -85,8 +86,8 @@ private void installIcons(MainWindow mw) { private static void loadLayouts(CControl globalPort) { try { - if (LAYOUT_FILE.exists()) { - globalPort.readXML(LAYOUT_FILE); + if (Files.exists(LAYOUT_FILE)) { + globalPort.readXML(LAYOUT_FILE.toFile()); } } catch (IOException e) { LOGGER.warn("Failed to load layouts", e); @@ -113,7 +114,7 @@ public void modalDialogClosed(EventObject e) { @Override public void shutDown(EventObject e) { try { - window.getDockControl().writeXML(LAYOUT_FILE); + window.getDockControl().writeXML(LAYOUT_FILE.toFile()); } catch (IOException ex) { LOGGER.warn("Failed to save layouts", ex); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/KeyStrokeSettings.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/KeyStrokeSettings.java index 70d232c1d18..aa280552501 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/KeyStrokeSettings.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/KeyStrokeSettings.java @@ -5,11 +5,11 @@ import java.awt.event.InputEvent; import java.awt.event.KeyEvent; -import java.io.File; -import java.io.FileWriter; import java.io.IOException; import java.io.Writer; import java.nio.charset.StandardCharsets; +import java.nio.file.Files; +import java.nio.file.Path; import java.util.Map; import java.util.Properties; import java.util.TreeMap; @@ -48,10 +48,10 @@ public class KeyStrokeSettings extends AbstractPropertiesSettings { /** * path of the properties file */ - public static final File SETTINGS_FILE = - new File(PathConfig.getKeyConfigDir(), SETTINGS_FILENAME); - private static final File SETTINGS_FILE_NEW = - new File(PathConfig.getKeyConfigDir(), "keystrokes.json"); + public static final Path SETTINGS_FILE = + PathConfig.getKeyConfigDir().resolve(SETTINGS_FILENAME); + private static final Path SETTINGS_FILE_NEW = + PathConfig.getKeyConfigDir().resolve("keystrokes.json"); private static final Logger LOGGER = LoggerFactory.getLogger(KeyStrokeSettings.class); @@ -163,13 +163,13 @@ private static void defineDefault(Class clazz, int keyCode, int modifiers } private static KeyStrokeSettings loadFromConfig() { - return new KeyStrokeSettings(SettingsManager.loadProperties(SETTINGS_FILE)); + return new KeyStrokeSettings(SettingsManager.loadProperties(SETTINGS_FILE.toFile())); } public static KeyStrokeSettings getInstance() { if (INSTANCE == null) { - if (SETTINGS_FILE.exists()) { + if (Files.exists(SETTINGS_FILE)) { try { LOGGER.info("Use new configuration format at {}", SETTINGS_FILE_NEW); return INSTANCE = new KeyStrokeSettings(Configuration.load(SETTINGS_FILE_NEW)); @@ -207,21 +207,22 @@ KeyStroke getKeyStroke(String key, KeyStroke defaultValue) { } public void save() { - LOGGER.info("Save keyboard shortcuts to: {}", SETTINGS_FILE.getAbsolutePath()); - SETTINGS_FILE.getParentFile().mkdirs(); - try (Writer writer = new FileWriter(SETTINGS_FILE, StandardCharsets.UTF_8)) { - Properties props = new Properties(); - for (Map.Entry entry : properties.entrySet()) { - props.setProperty(entry.getKey(), entry.getValue().toString()); + LOGGER.info("Save keyboard shortcuts to: {}", SETTINGS_FILE.toAbsolutePath()); + try { + Files.createDirectories(SETTINGS_FILE.getParent()); + try (Writer writer = Files.newBufferedWriter(SETTINGS_FILE, StandardCharsets.UTF_8)) { + Properties props = new Properties(); + for (Map.Entry entry : properties.entrySet()) { + props.setProperty(entry.getKey(), entry.getValue().toString()); + } + props.store(writer, "KeY's KeyStrokes"); } - props.store(writer, "KeY's KeyStrokes"); - writer.flush(); } catch (IOException ex) { ex.printStackTrace(); } - LOGGER.info("Save keyboard shortcuts to: {}", SETTINGS_FILE_NEW.getAbsolutePath()); - try (Writer writer = new FileWriter(SETTINGS_FILE_NEW)) { + LOGGER.info("Save keyboard shortcuts to: {}", SETTINGS_FILE_NEW.toAbsolutePath()); + try (Writer writer = Files.newBufferedWriter(SETTINGS_FILE_NEW)) { var config = new Configuration(properties); config.save(writer, "KeY's KeyStrokes"); writer.flush(); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/ShortcutSettings.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/ShortcutSettings.java index a5c7f249d30..385dc5f6684 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/ShortcutSettings.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/ShortcutSettings.java @@ -34,7 +34,7 @@ public ShortcutSettings() { super(); setHeaderText("Keyboard Shortcuts"); setSubHeaderText( - "These settings are stored in " + KeyStrokeSettings.SETTINGS_FILE.getAbsolutePath()); + "These settings are stored in " + KeyStrokeSettings.SETTINGS_FILE.toAbsolutePath()); add(new JScrollPane(tblShortcuts)); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/lemmatagenerator/LemmataAutoModeOptions.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/lemmatagenerator/LemmataAutoModeOptions.java index a6a6d32a0bb..fed82eea480 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/lemmatagenerator/LemmataAutoModeOptions.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/lemmatagenerator/LemmataAutoModeOptions.java @@ -74,13 +74,13 @@ public class LemmataAutoModeOptions { * Contains the internal version of KeY. It is needed for saving proofs. */ private final String internalVersion; - private final String homePath; + private final Path homePath; public LemmataAutoModeOptions() { this(KeYConstants.INTERNAL_VERSION, PathConfig.getKeyConfigDir()); } - public LemmataAutoModeOptions(String internalVersion, String homePath) { + public LemmataAutoModeOptions(String internalVersion, Path homePath) { this.internalVersion = internalVersion; this.homePath = homePath; checkForValidity(); @@ -90,7 +90,7 @@ public LemmataAutoModeOptions(String internalVersion, String homePath) { return pathOfDefinitionFile; } - public String getHomePath() { + public Path getHomePath() { return homePath; } diff --git a/key.util/src/main/java/org/key_project/util/Streams.java b/key.util/src/main/java/org/key_project/util/Streams.java index d1eecb6a03d..e1a71e7e632 100644 --- a/key.util/src/main/java/org/key_project/util/Streams.java +++ b/key.util/src/main/java/org/key_project/util/Streams.java @@ -6,20 +6,29 @@ import java.io.ByteArrayOutputStream; import java.io.IOException; import java.io.InputStream; +import java.util.Enumeration; +import java.util.List; +import java.util.Spliterator; +import java.util.Spliterators; +import java.util.stream.Stream; +import java.util.stream.StreamSupport; -public class Streams { - private Streams() { - throw new Error("do not instantiate"); +public abstract class Streams { + public static String toString(InputStream is) throws IOException { + ByteArrayOutputStream out = new ByteArrayOutputStream(); + is.transferTo(out); + return out.toString(); } - public static String toString(InputStream is) throws IOException { - ByteArrayOutputStream baos = new ByteArrayOutputStream(); - byte[] buf = new byte[2048]; - int count; - while ((count = is.read(buf)) >= 0) { - baos.write(buf, 0, count); - } - return baos.toString(); + /// Translates the enumeration into stream. + public static Stream fromEnumerator(Enumeration enumeration) { + return StreamSupport.stream( + Spliterators.spliteratorUnknownSize(enumeration.asIterator(), Spliterator.ORDERED), + false); } + /// Returns a list given the elements in the enumeration. + public static List toList(Enumeration enumeration) { + return fromEnumerator(enumeration).toList(); + } } diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/IsabelleSettingsProvider.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/IsabelleSettingsProvider.java index 4a45d4ef738..8e0a1004d48 100644 --- a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/IsabelleSettingsProvider.java +++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/IsabelleSettingsProvider.java @@ -76,7 +76,7 @@ public IsabelleSettingsProvider() { setHeaderText(getDescription()); setSubHeaderText( "Isabelle settings are stored in: " - + IsabelleTranslationSettings.SETTINGS_FILE_NEW.getAbsolutePath()); + + IsabelleTranslationSettings.SETTINGS_FILE_NEW.toAbsolutePath()); translationPathPanel = createTranslationPathPanel(); isabellePathPanel = createIsabellePathPanel(); timeoutField = createTimeoutField(); diff --git a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/IsabelleTranslationSettings.java b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/IsabelleTranslationSettings.java index 21a0d47eb73..473641e2ca6 100644 --- a/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/IsabelleTranslationSettings.java +++ b/keyext.isabelletranslation/src/main/java/org/key_project/isabelletranslation/IsabelleTranslationSettings.java @@ -27,8 +27,8 @@ public class IsabelleTranslationSettings extends AbstractSettings { /** * the file where settings are stored */ - protected static final File SETTINGS_FILE_NEW = - new File(PathConfig.getKeyConfigDir(), "isabelleSettings.json"); + protected static final Path SETTINGS_FILE_NEW = + PathConfig.getKeyConfigDir().resolve("isabelleSettings.json"); /** * The settings instance */ @@ -69,7 +69,7 @@ public class IsabelleTranslationSettings extends AbstractSettings { * The default path for translations */ private static final Path DEFAULT_TRANSLATION_PATH = - Path.of(PathConfig.getKeyConfigDir(), "IsabelleTranslations"); + PathConfig.getKeyConfigDir().resolve("IsabelleTranslations"); /** * default timeout setting */ @@ -96,7 +96,7 @@ private IsabelleTranslationSettings(Configuration load) { */ public static IsabelleTranslationSettings getInstance() { if (INSTANCE == null) { - if (SETTINGS_FILE_NEW.exists()) { + if (Files.exists(SETTINGS_FILE_NEW)) { try { LOGGER.info("Load Isabelle settings at {}", SETTINGS_FILE_NEW); return INSTANCE = @@ -141,8 +141,8 @@ protected void createSessionFiles() { * Writes the settings to the JSON file */ public void save() { - LOGGER.info("Save Isabelle settings to: {}", SETTINGS_FILE_NEW.getAbsolutePath()); - try (Writer writer = new FileWriter(SETTINGS_FILE_NEW)) { + LOGGER.info("Save Isabelle settings to: {}", SETTINGS_FILE_NEW.toAbsolutePath()); + try (Writer writer = Files.newBufferedWriter(SETTINGS_FILE_NEW)) { var config = new Configuration(); writeSettings(config); config.save(writer, "Isabelle settings");