KeY/JSON config for SMT solvers

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")

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]");
     }
 
 }

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<String, Object> 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<Configuration> 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<Pair<String, Configuration>> 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<String> keys() {
+        return this.data.keySet();
+    }
+
     // TODO Add documentation for this.
     /**
      * POJO for metadata of configuration entries.

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,26 +80,26 @@ 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");
     }
 
     /**
      * Returns the path to the file that is used to store recent files.
      *
      * @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;
     }
 

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);
             }

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();

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 {
      * <li>"#newline" in a props file encodes "\n"</li>
      * </ul>
      * <br>
-     *
+     * <p>
      * Note that, in order to guarantee dec(enc(*)) = enc(dec(*)) = id(*), care has to be taken:
      * <ol>
      * <li>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" != "="</li>
      * </ol>
-     *
+     * <p>
      * 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<String> unsupportedPropertiesKeys(
                 .collect(Collectors.toList());
     }
 
+
+    ///
+    public static Collection<String> unsupportedPropertiesKeysInSubSections(
+            Configuration config, String[] supportedKeys) {
+
+        Set<String> supKeys = new HashSet<>(Arrays.asList(supportedKeys));
+
+        List<String> error = new ArrayList<>();
+
+        for (var section : config.getSectionsWithNames()) {
+            Set<String> 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 <T> the enum which the read constant belongs to
+     * @return the value of the read enum constant
      */
     public static <T extends Enum<?>> T read(Properties props, String key, T defaultValue,
             T[] values) {
@@ -459,4 +476,5 @@ public static <T extends Enum<?>> T read(Properties props, String key, T default
     public static <T extends Enum<?>> void store(Properties props, String key, T value) {
         store(props, key, value.ordinal());
     }
+
 }