diff --git a/gradle/wrapper/gradle-wrapper.properties b/gradle/wrapper/gradle-wrapper.properties index 48c0a02ca41..d6e308a6378 100644 --- a/gradle/wrapper/gradle-wrapper.properties +++ b/gradle/wrapper/gradle-wrapper.properties @@ -1,5 +1,5 @@ distributionBase=GRADLE_USER_HOME distributionPath=wrapper/dists -distributionUrl=https\://services.gradle.org/distributions/gradle-8.7-bin.zip +distributionUrl=https\://services.gradle.org/distributions/gradle-8.12-bin.zip zipStoreBase=GRADLE_USER_HOME zipStorePath=wrapper/dists diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/settings/TestGenerationSettings.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/settings/TestGenerationSettings.java index 00f24ad3c1f..a74896daaf1 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/settings/TestGenerationSettings.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/settings/TestGenerationSettings.java @@ -4,11 +4,12 @@ package de.uka.ilkd.key.settings; import java.io.File; -import java.util.Properties; import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.NullMarked; import org.jspecify.annotations.Nullable; +@NullMarked public class TestGenerationSettings extends AbstractSettings { // region Default Values for option fields private static final boolean DEFAULT_APPLYSYMBOLICEX = false; @@ -85,14 +86,14 @@ public TestGenerationSettings(TestGenerationSettings data) { } /** - * @deprecated weigl: This method seems broken. I would expect: clone() = new TGS(this) + * @deprecated weigl: This method seems broken. I would expect: copy() = new TGS(this) */ @Deprecated(forRemoval = true) - public TestGenerationSettings clone(TestGenerationSettings data) { + public TestGenerationSettings copy(TestGenerationSettings data) { return new TestGenerationSettings(data); } - public TestGenerationSettings clone() { + public TestGenerationSettings copy() { return new TestGenerationSettings(this); } @@ -126,28 +127,6 @@ public boolean includePostCondition() { return includePostCondition; } - @Override - public void readSettings(Properties props) { - var prefix = "[" + CATEGORY + "]"; - setApplySymbolicExecution(SettingsConverter.read(props, - prefix + PROP_APPLY_SYMBOLIC_EXECUTION, DEFAULT_APPLYSYMBOLICEX)); - setMaxUnwinds(SettingsConverter.read(props, prefix + PROP_MAX_UWINDS, DEFAULT_MAXUNWINDS)); - setOutputPath(SettingsConverter.read(props, prefix + PROP_OUTPUT_PATH, DEFAULT_OUTPUTPATH)); - setRemoveDuplicates(SettingsConverter.read(props, - prefix + PROP_REMOVE_DUPLICATES, DEFAULT_REMOVEDUPLICATES)); - setRFL(SettingsConverter.read(props, prefix + PROP_USE_RFL, DEFAULT_USERFL)); - setUseJunit(SettingsConverter.read(props, prefix + PROP_USE_JUNIT, DEFAULT_USEJUNIT)); - setConcurrentProcesses(SettingsConverter.read(props, - prefix + PROP_CONCURRENT_PROCESSES, DEFAULT_CONCURRENTPROCESSES)); - setInvariantForAll(SettingsConverter.read(props, - prefix + PROP_INVARIANT_FOR_ALL, DEFAULT_INVARIANTFORALL)); - setOpenjmlPath( - SettingsConverter.read(props, prefix + PROP_OPENJML_PATH, DEFAULT_OPENJMLPATH)); - setObjenesisPath(SettingsConverter.read(props, PROP_OBJENESIS_PATH, DEFAULT_OBJENESISPATH)); - setIncludePostCondition(SettingsConverter.read(props, - PROP_INCLUDE_POST_CONDITION, DEFAULT_INCLUDEPOSTCONDITION)); - } - public boolean removeDuplicates() { return removeDuplicates; } @@ -234,24 +213,6 @@ public boolean useJunit() { return useJunit; } - - @Override - public void writeSettings(Properties props) { - var prefix = "[" + CATEGORY + "]"; - SettingsConverter.store(props, prefix + PROP_APPLY_SYMBOLIC_EXECUTION, - applySymbolicExecution); - SettingsConverter.store(props, prefix + PROP_CONCURRENT_PROCESSES, concurrentProcesses); - SettingsConverter.store(props, prefix + PROP_INVARIANT_FOR_ALL, invariantForAll); - SettingsConverter.store(props, prefix + PROP_MAX_UWINDS, maxUnwinds); - SettingsConverter.store(props, prefix + PROP_OUTPUT_PATH, outputPath); - SettingsConverter.store(props, prefix + PROP_REMOVE_DUPLICATES, removeDuplicates); - SettingsConverter.store(props, prefix + PROP_USE_RFL, useRFL); - SettingsConverter.store(props, prefix + PROP_USE_JUNIT, useJunit); - SettingsConverter.store(props, prefix + PROP_OPENJML_PATH, openjmlPath); - SettingsConverter.store(props, prefix + PROP_OBJENESIS_PATH, objenesisPath); - SettingsConverter.store(props, prefix + PROP_INCLUDE_POST_CONDITION, includePostCondition); - } - @Override public void readSettings(Configuration props) { var cat = props.getSection(CATEGORY); @@ -290,7 +251,7 @@ public void writeSettings(Configuration props) { } public void set(TestGenerationSettings settings) { - Properties p = new Properties(); + Configuration p = new Configuration(); settings.writeSettings(p); readSettings(p); } diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/AbstractTestGenerator.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/AbstractTestGenerator.java index 2fbfc7b1ce4..98db5330e76 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/AbstractTestGenerator.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/AbstractTestGenerator.java @@ -154,9 +154,9 @@ public void generateTestCases(final StopRequest stopRequest, final TestGeneratio // create special smt settings for test case generation final ProofIndependentSMTSettings piSettings = - ProofIndependentSettings.DEFAULT_INSTANCE.getSMTSettings().clone(); + ProofIndependentSettings.DEFAULT_INSTANCE.getSMTSettings().copy(); piSettings.setMaxConcurrentProcesses(settings.getNumberOfProcesses()); - final ProofDependentSMTSettings pdSettings = proof.getSettings().getSMTSettings().clone(); + final ProofDependentSMTSettings pdSettings = proof.getSettings().getSMTSettings().copy(); final NewSMTTranslationSettings newSettings = new NewSMTTranslationSettings(proof.getSettings().getNewSMTSettings()); pdSettings.setInvariantForall(settings.invariantForAll()); diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ModelGenerator.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ModelGenerator.java index 0b66418b71b..86cbd366679 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ModelGenerator.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ModelGenerator.java @@ -79,7 +79,7 @@ public void launch() { private SolverLauncher prepareLauncher() { final TestGenerationSettings settings = TestGenerationSettings.getInstance(); final ProofIndependentSMTSettings piSettings = - ProofIndependentSettings.DEFAULT_INSTANCE.getSMTSettings().clone(); + ProofIndependentSettings.DEFAULT_INSTANCE.getSMTSettings().copy(); piSettings.setMaxConcurrentProcesses(settings.getNumberOfProcesses()); diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java index 095e3ca921a..9945e666498 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java @@ -74,9 +74,9 @@ public static class File extends KeyAst { ProofSettings settings = new ProofSettings(ProofSettings.DEFAULT_SETTINGS); if (ctx.preferences() != null && ctx.preferences().s != null) { - String text = StringUtil.trim(ctx.preferences().s.getText(), '"') - .replace("\\\\:", ":"); - settings.loadSettingsFromPropertyString(text); + throw new IllegalStateException( + "You try to load a KeY file in an deprecated format. " + + "The settings are not a string of properties anymore. Please rewrite to the JSON-like format."); } else if (ctx.preferences() != null && ctx.preferences().c != null) { var cb = new ConfigurationBuilder(); var c = (Configuration) ctx.preferences().c.accept(cb); diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java b/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java index 1ff5cf7bb34..0742eb82966 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java @@ -115,17 +115,18 @@ public class Proof implements Named { * settings valid independent of a proof */ private final ProofIndependentSettings pis; + /** * when different users load and save a proof this vector fills up with Strings containing the * usernames. */ - public List userLog; + public List userLog = new ArrayList<>(); /** * when load and save a proof with different versions of key this vector fills up with Strings * containing the GIT versions. */ - public List keyVersionLog; + public List keyVersionLog = new ArrayList<>(); private long autoModeTime = 0; @@ -167,8 +168,8 @@ public class Proof implements Named { */ private Proof(Name name, InitConfig initConfig) { this.name = name; - assert initConfig != null : "Tried to create proof without valid services."; - this.initConfig = initConfig; + this.initConfig = + Objects.requireNonNull(initConfig, "Tried to create proof without valid services."); if (initConfig.getSettings() == null) { // if no settings have been assigned yet, take default settings diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediatePresentationProofFileParser.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediatePresentationProofFileParser.java index c3ef8763cc0..07abe204626 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediatePresentationProofFileParser.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediatePresentationProofFileParser.java @@ -3,8 +3,9 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.proof.io; +import java.io.IOException; +import java.io.StringReader; import java.util.ArrayDeque; -import java.util.ArrayList; import java.util.LinkedList; import java.util.List; @@ -143,26 +144,16 @@ public void beginExpr(ProofElementID eid, String str) { TacletInformation tacletInfo = (TacletInformation) ruleInfo; tacletInfo.ifDirectFormulaList = tacletInfo.ifDirectFormulaList.append(str); } - case KeY_USER -> { // UserLog - if (proof.userLog == null) { - proof.userLog = new ArrayList<>(); - } + case KeY_USER -> // UserLog proof.userLog.add(str); - } - case KeY_VERSION -> { // Version log - if (proof.keyVersionLog == null) { - proof.keyVersionLog = new ArrayList<>(); - } + case KeY_VERSION -> // Version log proof.keyVersionLog.add(str); - } case KeY_SETTINGS -> // ProofSettings loadPreferences(str); case BUILT_IN_RULE -> { // BuiltIn rules - { - final AppNodeIntermediate newNode = new AppNodeIntermediate(); - currNode.addChild(newNode); - currNode = newNode; - } + final AppNodeIntermediate newNode = new AppNodeIntermediate(); + currNode.addChild(newNode); + currNode = newNode; ruleInfo = new BuiltinRuleInformation(str); } case CONTRACT -> ((BuiltinRuleInformation) ruleInfo).currContract = str; @@ -329,7 +320,11 @@ private BuiltInAppIntermediate constructBuiltInApp() { */ private void loadPreferences(String preferences) { final ProofSettings proofSettings = new ProofSettings(ProofSettings.DEFAULT_SETTINGS); - proofSettings.loadSettingsFromPropertyString(preferences); + try { + proofSettings.loadSettingsFromJSONStream(new StringReader(preferences)); + } catch (IOException e) { + throw new RuntimeException(e); // no I/O exception on strings. + } } /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/AbstractPropertiesSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/AbstractPropertiesSettings.java index 08a82f320a3..230bb1277c2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/AbstractPropertiesSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/AbstractPropertiesSettings.java @@ -9,6 +9,7 @@ import java.util.stream.Collectors; import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.NullMarked; import org.jspecify.annotations.Nullable; /** @@ -16,6 +17,7 @@ * * @author weigl */ +@NullMarked public abstract class AbstractPropertiesSettings extends AbstractSettings { private static final String SET_DELIMITER = ","; @@ -24,12 +26,6 @@ public abstract class AbstractPropertiesSettings extends AbstractSettings { private static final Function parseBoolean = Boolean::parseBoolean; private static final Function parseDouble = Double::parseDouble; - /** - * Properties stored in this settings object. - * Updated by each {@link PropertyEntry} when a new non-null value is set. - */ - protected Map properties = new TreeMap<>(); - /** * category of this settings w/o brackets, e.g, "View" for "[View]". * This will prefix to every property entry. @@ -83,89 +79,74 @@ private static String stringSetToString(Set set) { .collect(Collectors.joining(SET_DELIMITER)); } - public boolean isInitialized() { - return properties != null; - } - - @Override - public void readSettings(Properties props) { - propertyEntries.forEach(it -> { - String value = props.getProperty(it.getKey()); - if (value != null) { - it.parseFrom(value); - } - }); - } - - @Override - public void writeSettings(Properties props) { - for (PropertyEntry entry : propertyEntries) { - props.setProperty("[" + category + "]" + entry.getKey(), entry.value()); - } - } - - @Override public void readSettings(Configuration props) { var cat = props.getSection(category); if (cat == null) return; - propertyEntries.forEach(it -> { - final var value = it.fromObject(cat.get(it.getKey())); - if (value != null) { - properties.put(it.getKey(), value); - } - }); + + for (PropertyEntry it : propertyEntries) { + it.setValue(cat.get(it.getKey())); + } } @Override public void writeSettings(Configuration props) { var cat = props.getOrCreateSection(category); - propertyEntries.forEach(it -> { + for (PropertyEntry it : propertyEntries) { cat.set(it.getKey(), it.get()); - }); + } } protected PropertyEntry createDoubleProperty(String key, double defValue) { - PropertyEntry pe = - new DefaultPropertyEntry<>(key, defValue, parseDouble, (it) -> (double) it); + PropertyEntry pe = new DirectPropertyEntry<>(key, defValue); propertyEntries.add(pe); return pe; } protected PropertyEntry createIntegerProperty(String key, int defValue) { - PropertyEntry pe = new DefaultPropertyEntry<>(key, defValue, parseInt, - (it) -> Math.toIntExact((Long) it)); + PropertyEntry pe = new DirectPropertyEntry<>(key, defValue) { + @Override + public void setValue(@Nullable Object value) { + if (value instanceof Integer i) { + set(i); + } + if (value instanceof Long i) { + set(i.intValue()); + } + } + }; propertyEntries.add(pe); return pe; } protected PropertyEntry createFloatProperty(String key, float defValue) { - PropertyEntry pe = - new DefaultPropertyEntry<>(key, defValue, parseFloat, (it) -> (float) (double) it); + PropertyEntry pe = new DirectPropertyEntry<>(key, defValue); propertyEntries.add(pe); return pe; } protected PropertyEntry createStringProperty(String key, String defValue) { - PropertyEntry pe = - new DefaultPropertyEntry<>(key, defValue, id -> id, Object::toString); + PropertyEntry pe = new DirectPropertyEntry<>(key, defValue); propertyEntries.add(pe); return pe; } protected PropertyEntry createBooleanProperty(String key, boolean defValue) { - PropertyEntry pe = - new DefaultPropertyEntry<>(key, defValue, parseBoolean, (it) -> (Boolean) it); + PropertyEntry pe = new DirectPropertyEntry<>(key, defValue); propertyEntries.add(pe); return pe; } - protected PropertyEntry> createStringSetProperty(String key, String defValue) { - PropertyEntry> pe = new DefaultPropertyEntry<>(key, parseStringSet(defValue), - AbstractPropertiesSettings::parseStringSet, - AbstractPropertiesSettings::stringSetToString, - (it) -> new LinkedHashSet<>((Collection) it)); + protected PropertyEntry> createStringSetProperty(String key, Set defValue) { + PropertyEntry> pe = new DirectPropertyEntry<>(key, defValue) { + @Override + public void setValue(@Nullable Object value) { + if (value instanceof List seq) { + set(new TreeSet<>((Collection) seq)); + } + } + }; propertyEntries.add(pe); return pe; } @@ -178,54 +159,76 @@ protected PropertyEntry> createStringSetProperty(String key, String * @return returns a {@link PropertyEntry} */ protected PropertyEntry> createStringListProperty(@NonNull String key, - @Nullable String defValue) { - PropertyEntry> pe = new DefaultPropertyEntry<>(key, parseStringList(defValue), - AbstractPropertiesSettings::parseStringList, - AbstractPropertiesSettings::stringListToString, it -> (List) it); + @Nullable List defValue) { + PropertyEntry> pe = new DirectPropertyEntry<>(key, defValue); propertyEntries.add(pe); return pe; } - public interface PropertyEntry { + /// This interface describes properties or options in an [AbstractPropertiesSettings] class. + /// A [PropertyEntry] is parameterize in a type its value holds, additionally it has name (to + /// store and read it + /// from configuration files), often a default. + /// + /// @param + public interface PropertyEntry { + /** + * The name (or key) to find this value inside a configuration file. It should also be the + * key + * in {@link java.beans.PropertyChangeEvent}s. + */ String getKey(); - void parseFrom(String value); - + /** + * Sets this value of this property. Should trigger {@link java.beans.PropertyChangeEvent} + * if necessary. + * + * @param value the new configuration value + */ void set(T value); + /** + * Returns the current configuration value. + */ T get(); - default void update() { - set(get()); - } - - String value(); - T fromObject(@Nullable Object o); + /// This method allows to set the property using an arbitray object which is allowed in + /// the configuration hierarchy. This methods may throw an exception on unexpected value + /// types. + /// + /// Especially, the following should not result into change of the value for a property: + /// ```java + /// setValue(value()) + /// ``` + /// + /// @param value an object of the [Configuration] hierarchy + void setValue(@Nullable Object value); + + /** + * Returns the representation of this configuration value to store it inside a + * {@link Configuration} + * object. + * + * @return an object compatible with {@link #setValue(Object)} + */ + Object value(); + + /// returns true if the property is set. + boolean isSet(); } - - class DefaultPropertyEntry implements PropertyEntry { + /// @param + public abstract class SimplePropertyEntry + implements PropertyEntry { private final String key; private final T defaultValue; - private final Function convert; - private final Function toString; - - private final Function fromObject; + private T currentValue; - private DefaultPropertyEntry(String key, T defaultValue, Function convert, - Function fromObject) { - this(key, defaultValue, convert, Objects::toString, fromObject); - } - - private DefaultPropertyEntry(String key, T defaultValue, Function convert, - Function toString, Function fromObject) { + SimplePropertyEntry(String key, T defaultValue) { this.key = key; this.defaultValue = defaultValue; - this.convert = convert; - this.toString = toString; - this.fromObject = fromObject; } @Override @@ -234,43 +237,86 @@ public String getKey() { } @Override - public void parseFrom(String value) { - set(convert.apply(value)); + public void set(T value) { + var old = currentValue; + currentValue = value; + firePropertyChange(getKey(), old, value); } @Override - public void set(T value) { - T old = get(); - // only store non-null values - if (value != null) { - properties.put(key, value); - firePropertyChange(key, old, value); - } + public T get() { + return currentValue != null ? currentValue : defaultValue; } @Override - public T get() { - var v = properties.getOrDefault(key, defaultValue); - if (v == null) { - return defaultValue; - } else { - return (T) v; + public boolean isSet() { + return currentValue != null; + } + } + + /** + * A base class for any configuration properties which is directly supported by the + * configuration. + * + * @param type of the value, supported by {@link Configuration} + * @see Configuration#allowedValueType(Object) + */ + public class DirectPropertyEntry extends SimplePropertyEntry { + DirectPropertyEntry(String key, T defaultValue) { + super(key, defaultValue); + } + + @Override + public void setValue(@Nullable Object value) { + set((T) value); + } + + @Override + public Object value() { + return get(); + } + } + + /** + * A base class for any configuration properties which are stored into a string representation. + * + * @param the value of the property + */ + public class DefaultPropertyEntry extends SimplePropertyEntry { + private final Function convert; + private final Function toString; + + public DefaultPropertyEntry(String key, T defaultValue, + Function convert, Function toString) { + super(key, defaultValue); + this.convert = convert; + this.toString = toString; + } + + @Override + public void setValue(@Nullable Object value) { + if (value == null) { + set(null); + return; + } + + if (value instanceof String s) { + set(convert.apply(s)); + return; } + + throw new IllegalArgumentException( + "Type %s is not supported for option %s".formatted(value.getClass(), getKey())); } @Override public String value() { var v = get(); if (v == null) { - return toString.apply(defaultValue); + return null; } else { return toString.apply(v); } } - - @Override - public T fromObject(@Nullable Object o) { - return fromObject.apply(o); - } } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/ChoiceSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/ChoiceSettings.java index 48dc7cfa3f2..aa175eedea8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/ChoiceSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/ChoiceSettings.java @@ -12,7 +12,6 @@ import java.util.Properties; import java.util.Set; import java.util.StringTokenizer; -import java.util.stream.Collectors; import de.uka.ilkd.key.logic.Choice; import de.uka.ilkd.key.logic.Namespace; @@ -162,23 +161,6 @@ public void readSettings(Properties props) { } - /** - * implements the method required by the Settings interface. The settings are written to the - * given Properties object. Only entries of - * the form < key > = < value > (,< - * value >)* are allowed. - *

- * * @param props the Properties object where to write the - * settings as (key, value) pair - */ - @Override - public void writeSettings(Properties props) { - var choiceSequence = category2Default.entrySet().stream() - .map(entry -> entry.getKey() + "-" + entry.getValue()) - .collect(Collectors.joining(" , ")); - props.setProperty("[" + CATEGORY + "]" + KEY_DEFAULT_CHOICES, choiceSequence); - } - @Override public void readSettings(Configuration props) { var category = props.getSection(CATEGORY); 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 563ae1a3dfa..086238aa028 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 @@ -366,6 +366,9 @@ public Configuration getSection(String name, boolean createIfNotExists) { } public Object set(String name, Object obj) { + if (!allowedValueType(obj)) { + throw new RuntimeException("Unallowed value type used: " + obj.getClass()); + } return data.put(name, obj); } @@ -419,6 +422,33 @@ public void overwriteWith(Configuration other) { data.putAll(other.data); } + /** + * Predicte for allowed value objects inside the configuration hierarchy and + * can be printed. + * + * @param value an arbitrary {@link Object} + * @return true if the value is allowed in the hierarchy. + */ + public static boolean allowedValueType(@Nullable Object value) { + return value instanceof String + || value instanceof Long + || value instanceof Integer + || value instanceof Double + || value instanceof Float + || value instanceof Short + || value instanceof Byte + || value instanceof Boolean + || value instanceof Collection + || value instanceof Map + || value instanceof Configuration + || value instanceof Enum + || value == null; + } + + public Set getKeys() { + 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/FeatureSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/FeatureSettings.java index b63849ed328..cd3b374dc64 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/FeatureSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/FeatureSettings.java @@ -97,28 +97,6 @@ private boolean isTrue(Object value) { }; } - @Override - public void readSettings(Properties props) { - activatedFeatures.clear(); - var prefix = "[" + CATEGORY + "]"; - for (Map.Entry entries : props.entrySet()) { - final var s = entries.getKey().toString(); - if (s.startsWith(prefix) && isTrue(entries.getValue())) { - final var feature = s.substring(prefix.length()); - activate(feature); - LOGGER.info("Activate feature: {}", feature); - } - } - } - - @Override - public void writeSettings(Properties props) { - var prefix = "[" + CATEGORY + "]"; - for (String activatedFeature : activatedFeatures) { - props.put(prefix + activatedFeature, "true"); - } - } - @Override public void readSettings(@NonNull Configuration props) { activatedFeatures.clear(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/GeneralSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/GeneralSettings.java index 436ec981253..933b2cdaf39 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/GeneralSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/GeneralSettings.java @@ -223,27 +223,6 @@ public void readSettings(Properties props) { } } - /** - * implements the method required by the Settings interface. The settings are written to the - * given Properties object. Only entries of the form - * = (,)* are allowed. - * - * @param props the Properties object where to write the settings as (key, value) pair - */ - @Override - public void writeSettings(Properties props) { - var prefix = "[" + CATEGORY + "]"; - props.setProperty(prefix + TACLET_FILTER, String.valueOf(tacletFilter)); - props.setProperty(prefix + DND_DIRECTION_SENSITIVE_KEY, - String.valueOf(dndDirectionSensitive)); - props.setProperty(prefix + RIGHT_CLICK_MACROS_KEY, String.valueOf(rightClickMacros)); - props.setProperty(prefix + USE_JML_KEY, String.valueOf(useJML)); - props.setProperty(prefix + AUTO_SAVE, String.valueOf(autoSave)); - props.setProperty(prefix + ENSURE_SOURCE_CONSISTENCY, - String.valueOf(ensureSourceConsistency)); - props.setProperty(KEY_JML_ENABLED_KEYS, String.join(",", jmlEnabledKeys)); - } - @Override public void readSettings(Configuration props) { setTacletFilter(props.getBool(TACLET_FILTER)); diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/LemmaGeneratorSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/LemmaGeneratorSettings.java index 0f5cc11c47d..ad0d6992621 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/LemmaGeneratorSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/LemmaGeneratorSettings.java @@ -3,7 +3,6 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.settings; -import java.util.Properties; public class LemmaGeneratorSettings extends AbstractSettings { public static final String CATEGORY = "LemmaGenerator"; @@ -35,22 +34,6 @@ public void setShowDialogUsingAxioms(boolean value) { firePropertyChange(SHOW_DIALOG_USING_AXIOMS, old, showDialogUsingAxioms); } - @Override - public void readSettings(Properties props) { - setShowDialogAddingAxioms(SettingsConverter.read(props, - "[" + CATEGORY + "]" + SHOW_DIALOG_ADDING_AXIOMS, true)); - setShowDialogUsingAxioms(SettingsConverter.read(props, - "[" + CATEGORY + "]" + SHOW_DIALOG_USING_AXIOMS, true)); - } - - @Override - public void writeSettings(Properties props) { - SettingsConverter.store(props, "[" + CATEGORY + "]" + SHOW_DIALOG_ADDING_AXIOMS, - showDialogAddingAxioms); - SettingsConverter.store(props, "[" + CATEGORY + "]" + SHOW_DIALOG_USING_AXIOMS, - showDialogUsingAxioms); - } - @Override public void readSettings(Configuration props) { var cat = props.getSection(CATEGORY); diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/NewSMTTranslationSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/NewSMTTranslationSettings.java index bff40407b29..bde109963c2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/NewSMTTranslationSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/NewSMTTranslationSettings.java @@ -7,6 +7,11 @@ import java.util.*; import java.util.Map.Entry; +import org.jspecify.annotations.NullMarked; +import org.jspecify.annotations.Nullable; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + /** * A collection of settings for the new (= 2021) SMT translation. *

@@ -21,8 +26,10 @@ * * @author Mattias Ulbrich */ +@NullMarked public class NewSMTTranslationSettings extends AbstractSettings { - private static final String PREFIX = "[NewSMT]"; + private static final String CATEGORY = "NewSMT"; + private static final Logger LOGGER = LoggerFactory.getLogger(NewSMTTranslationSettings.class); // Using a linked hash map to make the order deterministic in writing to // file @@ -45,45 +52,29 @@ public NewSMTTranslationSettings(NewSMTTranslationSettings toCopy) { } /** - * Create a clone of this object. s.clone() is equivalent to - * - * 

-     *     new new NewSMTTranslationSettings(s);
-     *
- * - * @return + * Create a deep copy of this object. */ - @Override - public NewSMTTranslationSettings clone() { + public NewSMTTranslationSettings copy() { return new NewSMTTranslationSettings(this); } @Override - public void readSettings(Properties props) { - for (Object k : props.keySet()) { - String key = k.toString(); - if (key.startsWith(PREFIX)) { - map.put(key.substring(PREFIX.length()), props.getProperty(key)); - } - } - } + public void readSettings(Configuration props) { + var newSmt = props.getSection(CATEGORY); - @Override - public void writeSettings(Properties props) { - for (Entry en : map.entrySet()) { - props.put(PREFIX + en.getKey(), en.getValue()); + if (newSmt == null) { + return; } - } - @Override - public void readSettings(Configuration props) { - var newSmt = props.getSection("NewSMT"); - if (newSmt == null) - return; for (var entry : newSmt.getEntries()) { final var value = entry.getValue(); - assert value instanceof String; - map.put(entry.getKey(), value.toString()); + if (value instanceof String s) { + map.put(entry.getKey(), s); + } else { + LOGGER.warn("Settings {} with value {} ignored. Value of type string expected.", + entry.getKey(), + entry.getValue()); + } } } @@ -111,7 +102,7 @@ public Map getMap() { * @param key the key to look up * @return the value for the key, null if not present */ - public String get(String key) { + public @Nullable String get(String key) { return map.get(key); } @@ -122,7 +113,7 @@ public String get(String key) { * @param value the non-null value to set * @return the value that was in the map prior to the call (see {@link Map#put(Object, Object)}. */ - public String put(String key, String value) { + public @Nullable String put(String key, String value) { var old = map.get(key); String result = map.put(Objects.requireNonNull(key), Objects.requireNonNull(value)); firePropertyChange(key, old, value); diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofDependentSMTSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/ProofDependentSMTSettings.java index e45318b4e1a..4f48c5c6cd8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofDependentSMTSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/ProofDependentSMTSettings.java @@ -4,11 +4,11 @@ package de.uka.ilkd.key.settings; -import java.util.Properties; - import de.uka.ilkd.key.taclettranslation.assumptions.SupportedTaclets; +import org.jspecify.annotations.NullMarked; +@NullMarked public class ProofDependentSMTSettings extends AbstractSettings { public static final String CATEGORY = "SMTSettings"; @@ -26,7 +26,6 @@ public class ProofDependentSMTSettings extends AbstractSettings { public static final String INTEGERS_MINIMUM = "integersMinimum"; public static final String INVARIANT_FORALL = "invariantForall"; - public static final String PROP_LEGACY_TRANSLATION = "legacyTranslation"; private static final String PROP_SUPPORTED_TACLETS = "supportedTaclets"; private boolean useExplicitTypeHierarchy = false; @@ -38,10 +37,8 @@ public class ProofDependentSMTSettings extends AbstractSettings { private int maxGenericSorts = 2; private int maxInteger = 2147483645; private int minInteger = -2147483645; - private boolean useLegacyTranslation = false; - - private SupportedTaclets supportedTaclets; + private SupportedTaclets supportedTaclets = SupportedTaclets.REFERENCE; private ProofDependentSMTSettings() { setSupportedTaclets(SupportedTaclets.REFERENCE); @@ -69,62 +66,14 @@ public void copy(ProofDependentSMTSettings data) { private static final ProofDependentSMTSettings DEFAULT_DATA = new ProofDependentSMTSettings(); public static ProofDependentSMTSettings getDefaultSettingsData() { - return DEFAULT_DATA.clone(); + return DEFAULT_DATA.copy(); } - - @Override - public ProofDependentSMTSettings clone() { + public ProofDependentSMTSettings copy() { return new ProofDependentSMTSettings(this); } - @Override - public void readSettings(Properties props) { - var prefix = "[" + CATEGORY + "]"; - setUseExplicitTypeHierarchy( - SettingsConverter.read(props, prefix + EXPLICIT_TYPE_HIERARCHY, - useExplicitTypeHierarchy)); - setUseNullInstantiation( - SettingsConverter.read(props, prefix + INSTANTIATE_NULL_PREDICATES, - useNullInstantiation)); - setUseBuiltInUniqueness( - SettingsConverter.read(props, prefix + USE_BUILT_IN_UNIQUENESS, useBuiltInUniqueness)); - setMaxGenericSorts( - SettingsConverter.read(props, prefix + MAX_GENERIC_SORTS, maxGenericSorts)); - setUseUIMultiplication( - SettingsConverter.read(props, prefix + USE_UNINTERPRETED_MULTIPLICATION, - useUIMultiplication)); - setUseConstantsForIntegers( - SettingsConverter.read(props, prefix + USE_CONSTANTS_FOR_BIGSMALL_INTEGERS, - useConstantsForIntegers)); - - setMaxInteger(SettingsConverter.read(props, prefix + INTEGERS_MAXIMUM, maxInteger)); - setMinInteger(SettingsConverter.read(props, prefix + INTEGERS_MINIMUM, minInteger)); - setInvariantForall( - SettingsConverter.read(props, prefix + INVARIANT_FORALL, invariantForall)); - supportedTaclets.selectTaclets(SettingsConverter.read(props, prefix + TACLET_SELECTION, - supportedTaclets.getNamesOfSelectedTaclets())); - } - - @Override - public void writeSettings(Properties props) { - var prefix = "[" + CATEGORY + "]"; - SettingsConverter.store(props, prefix + EXPLICIT_TYPE_HIERARCHY, useExplicitTypeHierarchy); - SettingsConverter.store(props, prefix + INSTANTIATE_NULL_PREDICATES, useNullInstantiation); - SettingsConverter.store(props, prefix + MAX_GENERIC_SORTS, maxGenericSorts); - SettingsConverter.store(props, prefix + TACLET_SELECTION, - supportedTaclets.getNamesOfSelectedTaclets()); - SettingsConverter.store(props, prefix + USE_BUILT_IN_UNIQUENESS, useBuiltInUniqueness); - SettingsConverter.store(props, prefix + USE_UNINTERPRETED_MULTIPLICATION, - useUIMultiplication); - SettingsConverter.store(props, prefix + USE_CONSTANTS_FOR_BIGSMALL_INTEGERS, - useConstantsForIntegers); - SettingsConverter.store(props, prefix + INTEGERS_MAXIMUM, maxInteger); - SettingsConverter.store(props, prefix + INTEGERS_MINIMUM, minInteger); - SettingsConverter.store(props, prefix + INVARIANT_FORALL, invariantForall); - } - @Override public void readSettings(Configuration props) { props = props.getSection(CATEGORY); @@ -263,14 +212,4 @@ public void setSupportedTaclets(SupportedTaclets supportedTaclets) { this.supportedTaclets = supportedTaclets; firePropertyChange(PROP_SUPPORTED_TACLETS, old, supportedTaclets); } - - public boolean isUseLegacyTranslation() { - return useLegacyTranslation; - } - - public void setUseLegacyTranslation(boolean useLegacyTranslation) { - var old = this.useLegacyTranslation; - this.useLegacyTranslation = useLegacyTranslation; - firePropertyChange(PROP_LEGACY_TRANSLATION, old, useLegacyTranslation); - } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSMTSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSMTSettings.java index 1e2c91fd504..79e9bedc34d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSMTSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSMTSettings.java @@ -12,8 +12,11 @@ import de.uka.ilkd.key.smt.solvertypes.SolverType; import de.uka.ilkd.key.smt.solvertypes.SolverTypes; +import org.jspecify.annotations.NullMarked; + import static de.uka.ilkd.key.settings.FeatureSettings.createFeature; +@NullMarked public final class ProofIndependentSMTSettings extends AbstractSettings { private static final String CATEGORY = "SMTSettings"; public static final String ACTIVE_SOLVER = "ActiveSolver"; @@ -315,7 +318,7 @@ public void copy(ProofIndependentSMTSettings data) { } public static ProofIndependentSMTSettings getDefaultSettingsData() { - return DEFAULT_DATA.clone(); + return DEFAULT_DATA.copy(); } public boolean containsSolver(SolverType type) { @@ -342,7 +345,7 @@ public void setParameters(SolverType type, String parameters) { type.setSolverParameters(parameters); } - public ProofIndependentSMTSettings clone() { + public ProofIndependentSMTSettings copy() { return new ProofIndependentSMTSettings(this); } 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 77a165021de..d0483cfb251 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 @@ -8,7 +8,6 @@ import java.util.Date; import java.util.LinkedList; import java.util.List; -import java.util.Properties; import de.uka.ilkd.key.pp.NotationInfo; @@ -53,7 +52,6 @@ public class ProofIndependentSettings { private final List settings = new LinkedList<>(); private final PropertyChangeListener settingsListener = e -> saveSettings(); - private Properties lastReadedProperties; private Configuration lastReadedConfiguration; private ProofIndependentSettings() { @@ -74,9 +72,6 @@ public void addSettings(Settings settings) { if (!this.settings.contains(settings)) { this.settings.add(settings); settings.addPropertyChangeListener(settingsListener); - if (lastReadedProperties != null) { - settings.readSettings(lastReadedProperties); - } if (lastReadedConfiguration != null) { settings.readSettings(lastReadedConfiguration); } @@ -99,44 +94,14 @@ private void loadSettings() { } private void load(File file) throws IOException { - if (!file.getName().endsWith(".json")) { - try (FileInputStream in = new FileInputStream(file)) { - Properties properties = new Properties(); - properties.load(in); - for (Settings settings : settings) { - settings.readSettings(properties); - } - lastReadedProperties = properties; - } - } else { - this.lastReadedConfiguration = Configuration.load(file); - for (Settings settings : settings) { - settings.readSettings(lastReadedConfiguration); - } + this.lastReadedConfiguration = Configuration.load(file); + for (Settings settings : settings) { + settings.readSettings(lastReadedConfiguration); } } public void saveSettings() { - if (!filename.getName().endsWith(".json")) { - Properties result = new Properties(); - for (Settings settings : settings) { - settings.writeSettings(result); - } - - if (!filename.exists()) { - filename.getParentFile().mkdirs(); - } - - try (var out = new FileOutputStream(filename)) { - result.store(out, "Proof-Independent-Settings-File. Generated " + new Date()); - } catch (IOException e) { - LOGGER.error("Could not store settings to {}", filename, e); - } - } - - Configuration config = new Configuration(); - for (var settings : settings) - settings.writeSettings(config); + Configuration config = asConfiguration(); if (!filename.exists()) { filename.getParentFile().mkdirs(); } @@ -149,6 +114,14 @@ public void saveSettings() { } } + public Configuration asConfiguration() { + Configuration config = new Configuration(); + for (var settings : settings) { + settings.writeSettings(config); + } + return config; + } + public GeneralSettings getGeneralSettings() { return generalSettings; } 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 319df9a2b2e..f5c6cbccc0b 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 @@ -17,28 +17,27 @@ import org.slf4j.Logger; import org.slf4j.LoggerFactory; -/** - * This class is used to load and save settings for proofs such as which data type models are used - * to represent the java types. Which heuristics have to be loaded and so on. The class loads the - * file proofsettings.config from the place where you started key. If the file is not available - * standard settings are used. The loaded file has the following structure: - * // KeY-Configuration file - * ActiveHeuristics=simplify_prog , simplify - * MaximumNumberOfHeuristcsApplications=400 - * number = IntegerLDT.class - * boolean = BooleanLDT.class - * - * - * @see Properties - * @see Settings - */ +/// This class is used to load and save settings for proofs such as which data type models are used +/// to represent the java types. +/// Which heuristics have to be loaded and so on? +/// The class loads the file `proofsettings.config` from the place where you started key. +/// If the file is not available, standard settings are used. +/// The loaded file has the following structure: +/// +/// ``` +/// // KeY-Configuration file +/// ActiveHeuristics=["simplify_prog", "simplify"] +/// MaximumNumberOfHeuristcsApplications=400 +/// number = "IntegerLDT.class" +/// boolean = "BooleanLDT.class" +/// ``` +/// +/// @see Properties +/// @see Settings 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 File PROVER_CONFIG_FILE_NEW = new File(PathConfig.getKeyConfigDir(), "proof-settings.json"); public static final URL PROVER_CONFIG_FILE_TEMPLATE = KeYResourceManager.getManager() @@ -70,11 +69,10 @@ private static ProofSettings loadedSettings() { private final NewSMTTranslationSettings newSMTSettings = new NewSMTTranslationSettings(); private final TermLabelSettings termLabelSettings = new TermLabelSettings(); - private Properties lastLoadedProperties = null; private Configuration lastLoadedConfiguration = null; /** - * create a proof settings object. When you add a new settings object, PLEASE UPDATE THE LIST + * Create a proof settings object. When you add a new settings object, PLEASE UPDATE THE LIST * ABOVE AND USE THOSE CONSTANTS INSTEAD OF USING INTEGERS DIRECTLY */ private ProofSettings() { @@ -86,44 +84,41 @@ private ProofSettings() { } /* - * copy constructor - substitutes .clone() in classes implementing Settings + * copy constructor - substitutes .copy() in classes implementing Settings */ public ProofSettings(ProofSettings toCopy) { this(); - Properties result = new Properties(); - lastLoadedProperties = toCopy.lastLoadedProperties; - for (Settings s : toCopy.settings) { - s.writeSettings(result); - } + lastLoadedConfiguration = toCopy.lastLoadedConfiguration; + Configuration result = toCopy.asConfiguration(); for (Settings s : settings) { s.readSettings(result); } } + public Configuration asConfiguration() { + Configuration result = new Configuration(); + for (Settings s : settings) { + s.writeSettings(result); + } + return result; + } + public void addSettings(Settings settings) { this.settings.add(settings); settings.addPropertyChangeListener(listener); - if (lastLoadedProperties != null) { - settings.readSettings(lastLoadedProperties); - } if (lastLoadedConfiguration != null) { settings.readSettings(lastLoadedConfiguration); } } /** - * @deprecated {@link #getConfiguration} + * Serializes the current hierarchy of settings into a {@link Configuration} object which + * represents + * a tree of {@link java.util.Map}s. + * + * @return the current configuration in form of a {@link Configuration} object. */ - @Deprecated - public Properties getProperties() { - Properties result = new Properties(); - for (Settings s : settings) { - s.writeSettings(result); - } - return result; - } - public Configuration getConfiguration() { var config = new Configuration(); for (Settings s : settings) { @@ -144,12 +139,11 @@ public void settingsToStream(Writer out) { */ public void saveSettings() { try { - if (!PROVER_CONFIG_FILE_NEW.exists()) { - PROVER_CONFIG_FILE.getParentFile().mkdirs(); - } - try (Writer out = new BufferedWriter( - new FileWriter(PROVER_CONFIG_FILE_NEW, StandardCharsets.UTF_8))) { - settingsToStream(out); + if (PROVER_CONFIG_FILE.getParentFile().mkdirs()) { + try (Writer out = new BufferedWriter( + new FileWriter(PROVER_CONFIG_FILE, StandardCharsets.UTF_8))) { + settingsToStream(out); + } } } catch (IOException e) { LOGGER.warn("Could not save proof-settings.", e); @@ -181,61 +175,23 @@ public void loadDefaultJSONSettings() { } /** - * Used by loadSettings() and loadSettingsFromString(...) - * - * @deprecated in favour of {@link #loadSettingsFromJSONStream(Reader)} - */ - @Deprecated - public void loadSettingsFromPropertyStream(Reader in) { - Properties props = new Properties(); - try { - props.load(in); - } catch (IOException e) { - LOGGER.warn("Error on loading proof-settings.", e); - } - lastLoadedProperties = props; - lastLoadedConfiguration = null; - for (Settings s : settings) { - s.readSettings(props); - } - } - - /** - * Loads the former settings from configuration file. + * Loads the former settings from a configuration file. */ 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 fileToUse = isOldFormat ? PROVER_CONFIG_FILE : PROVER_CONFIG_FILE_NEW; + var fileToUse = PROVER_CONFIG_FILE; try (var in = new BufferedReader(new FileReader(fileToUse, StandardCharsets.UTF_8))) { LOGGER.info("Load proof dependent settings from file {}", fileToUse); - if (isOldFormat) { - loadDefaultJSONSettings(); - loadSettingsFromPropertyStream(in); - } else { - loadDefaultJSONSettings(); - loadSettingsFromJSONStream(in); - } + loadDefaultJSONSettings(); + loadSettingsFromJSONStream(in); } catch (IOException e) { LOGGER.warn("No proof-settings could be loaded, using defaults", e); } } } - - /** - * Used to load Settings from a .key file - */ - public void loadSettingsFromPropertyString(String s) { - if (s == null) { - return; - } - StringReader reader = new StringReader(s); - loadSettingsFromPropertyStream(reader); - } - /** * returns the StrategySettings object * @@ -276,18 +232,6 @@ public static boolean isChoiceSettingInitialised() { return !ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().getChoices().isEmpty(); } - /** - * Update the proof settings according to the entries on the properties. - * - * @param props a non-null object with KeY properties. - */ - public void update(Properties props) { - for (Settings s : settings) { - s.readSettings(props); - } - } - - /** * Returns the term label settings from the proof settings. * @@ -298,7 +242,6 @@ public TermLabelSettings getTermLabelSettings() { } public void readSettings(Configuration c) { - lastLoadedProperties = null; lastLoadedConfiguration = c; for (Settings setting : settings) setting.readSettings(c); diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/Settings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/Settings.java index 3ead7fb78b1..04a3919f482 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/Settings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/Settings.java @@ -5,34 +5,16 @@ import java.beans.PropertyChangeListener; import java.beans.PropertyChangeSupport; -import java.util.Properties; -import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.NullMarked; /** * This interface is implemented by classes that are used to store settings for different proposes * (like active heuristics, which LDTs to use etc.) */ +@NullMarked public interface Settings { - /** - * gets a Properties object and has to perform the necessary steps in order to change this - * object in a way that it represents the stored settings - * - * @deprecated Deprecated in favour of {@link #readSettings(Configuration)} - */ - @Deprecated - void readSettings(Properties props); - - /** - * The settings to store are written to the given Properties object. - * - * @param props the Properties object where to write the settings as (key, value) pair - * @deprecated Deprecated in favour of {@link #writeSettings(Configuration)} - */ - @Deprecated - void writeSettings(Properties props); - /** * This method transfers the given configuration information into the local states. The setter * methods are used @@ -42,7 +24,7 @@ public interface Settings { * @param props a non-null references to a configuration object. The state of this object * shall not be changed by the implementations. */ - void readSettings(@NonNull Configuration props); + void readSettings(Configuration props); /** * The internal state is stored in the given configuration object. The stored information must @@ -55,7 +37,7 @@ public interface Settings { * accordingly to the local * internal state. */ - void writeSettings(@NonNull Configuration props); + void writeSettings(Configuration props); /** @@ -64,7 +46,7 @@ public interface Settings { * @param listener a non-null reference * @see java.beans.PropertyChangeSupport#addPropertyChangeListener(PropertyChangeListener) */ - void addPropertyChangeListener(@NonNull PropertyChangeListener listener); + void addPropertyChangeListener(PropertyChangeListener listener); /** * Removes the given listener. @@ -81,8 +63,8 @@ public interface Settings { * @param listener the listener to be added * @see PropertyChangeSupport#addPropertyChangeListener(String, PropertyChangeListener) */ - void addPropertyChangeListener(@NonNull String propertyName, - @NonNull PropertyChangeListener listener); + void addPropertyChangeListener(String propertyName, + PropertyChangeListener listener); /** * Removes the given listener from being triggered by changes of the specified property. @@ -91,6 +73,5 @@ void addPropertyChangeListener(@NonNull String propertyName, * @param listener the listener to be removed * @see PropertyChangeSupport#removePropertyChangeListener(String, PropertyChangeListener) */ - void removePropertyChangeListener(@NonNull String propertyName, - @NonNull PropertyChangeListener listener); + void removePropertyChangeListener(String propertyName, PropertyChangeListener listener); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/TermLabelSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/TermLabelSettings.java index 847d65721dc..9a9d86b215a 100755 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/TermLabelSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/TermLabelSettings.java @@ -3,11 +3,10 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.settings; -import java.util.Properties; - import de.uka.ilkd.key.logic.label.OriginTermLabel; import de.uka.ilkd.key.logic.label.TermLabel; +import org.jspecify.annotations.NullMarked; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -16,6 +15,7 @@ * * @author lanzinger */ +@NullMarked public class TermLabelSettings extends AbstractSettings { private static final Logger LOGGER = LoggerFactory.getLogger(TermLabelSettings.class); @@ -25,28 +25,13 @@ public class TermLabelSettings extends AbstractSettings { private boolean useOriginLabels = true; - @Override - public void readSettings(Properties props) { - String str = props.getProperty("[" + CATEGORY + "]" + USE_ORIGIN_LABELS); - - if (str != null && (str.equals("true") || str.equals("false"))) { - setUseOriginLabels(Boolean.parseBoolean(str)); - } else { - setUseOriginLabels(true); - } - } - - @Override - public void writeSettings(Properties props) { - props.setProperty("[" + CATEGORY + "]" + USE_ORIGIN_LABELS, - Boolean.toString(useOriginLabels)); - } - @Override public void readSettings(Configuration props) { var category = props.getSection(CATEGORY); - if (category == null) + if (category == null) { return; + } + try { setUseOriginLabels(category.getBool(USE_ORIGIN_LABELS)); } catch (Exception e) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/ViewSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/ViewSettings.java index 1acbc33aed4..7134ba4a429 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/ViewSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/ViewSettings.java @@ -5,6 +5,7 @@ import java.util.List; import java.util.Set; +import java.util.TreeSet; import javax.swing.*; /** @@ -13,7 +14,6 @@ * number is exceeded no SchemaVariables get instantiated in the displayed tooltip. 3) whether * intermediate proofsteps should be hidden in the proof tree view * - * @see de.uka.ilkd.key.gui.settings.StandardUISettings * @author unknown * @author weigl */ @@ -21,20 +21,28 @@ public class ViewSettings extends AbstractPropertiesSettings { private static final String CLUTTER_RULES = "clutterRules"; - private static final String CLUTTER_RULES_DEFAULT = "cut_direct_r,cut_direct_l," - + "case_distinction_r,case_distinction_l,local_cut,commute_and_2,commute_or_2," - + "boxToDiamond,pullOut,typeStatic,less_is_total,less_zero_is_total,apply_eq_monomials" - + "eqTermCut,instAll,instEx,divIncreasingPos,divIncreasingNeg,jmodUnique1,jmodeUnique2," - + "jmodjmod,jmodDivisble,jdivAddMultDenom,jmodAltZero,add_non_neq_square,divide_geq," - + "add_greatereq,geq_add_one,leq_add_one,polySimp_addOrder,polySimp_expand,add_lesseq," - + "divide_equation,equal_add_one,add_eq"; + private static final Set CLUTTER_RULES_DEFAULT = + new TreeSet<>(Set.of("cut_direct_r", "cut_direct_l", + "case_distinction_r", "case_distinction_l", "local_cut", "commute_and_2", + "commute_or_2", "boxToDiamond", + "pullOut", "typeStatic", "less_is_total", "less_zero_is_total", "apply_eq_monomials" + + "eqTermCut", + "instAll", "instEx", "divIncreasingPos", "divIncreasingNeg", "jmodUnique1", + "jmodeUnique2", + "jmodjmod", "jmodDivisble", "jdivAddMultDenom", "jmodAltZero", "add_non_neq_square", + "divide_geq", + "add_greatereq", "geq_add_one", "leq_add_one", "polySimp_addOrder", "polySimp_expand", + "add_lesseq", + "divide_equation", "equal_add_one", "add_eq")); private static final String CLUTTER_RULESSETS = "clutterRuleSets"; - private static final String CLUTTER_RULESETS_DEFAULT = "notHumanReadable,obsolete," - + "pullOutQuantifierAll,inEqSimp_commute,inEqSimp_expand,pullOutQuantifierEx," - + "inEqSimp_nonLin_divide,inEqSimp_special_nonLin,inEqSimp_nonLin,polySimp_normalise," - + "polySimp_directEquations"; + private static final Set CLUTTER_RULESETS_DEFAULT = + new TreeSet<>(Set.of("notHumanReadable", "obsolete", + "pullOutQuantifierAll", "inEqSimp_commute", "inEqSimp_expand", "pullOutQuantifierEx", + "inEqSimp_nonLin_divide", + "inEqSimp_special_nonLin", "inEqSimp_nonLin", "polySimp_normalise", + "polySimp_directEquations")); /** * default max number of displayed tooltip lines is 40 @@ -109,10 +117,14 @@ public class ViewSettings extends AbstractPropertiesSettings { private static final String SEQUENT_VIEW_TOOLTIP = "SequentViewTooltips"; - /** this setting enables/disables tool tips in the source view */ + /** + * this setting enables/disables tool tips in the source view + */ private static final String SOURCE_VIEW_TOOLTIP = "SourceViewTooltips"; - /** this setting enables/disables tool tips in the proof tree */ + /** + * this setting enables/disables tool tips in the proof tree + */ private static final String PROOF_TREE_TOOLTIP = "ProofTreeTooltips"; private static final String HIGHLIGHT_ORIGIN = "HighlightOrigin"; @@ -228,7 +240,8 @@ public class ViewSettings extends AbstractPropertiesSettings { * @see #setFolderBookmarks(List) */ private final PropertyEntry> folderBookmarks = - createStringListProperty(USER_FOLDER_BOOKMARKS, System.getProperty("user.home")); + createStringListProperty(USER_FOLDER_BOOKMARKS, + List.of(System.getProperty("user.home"))); public ViewSettings() { super("View"); diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProveTest.java b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProveTest.java index 87d614a794b..719637f39c7 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProveTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProveTest.java @@ -5,6 +5,7 @@ import java.io.File; import java.io.IOException; +import java.io.StringReader; import java.util.List; import de.uka.ilkd.key.control.DefaultUserInterfaceControl; @@ -81,10 +82,11 @@ private void runKey(String file, TestProperty testProperty) throws Exception { LOGGER.info("{}: Run Test: {} with {}", caseId, file, testProperty); // Initialize KeY settings. - ProofSettings.DEFAULT_SETTINGS.loadSettingsFromPropertyString(globalSettings); + ProofSettings.DEFAULT_SETTINGS.loadSettingsFromJSONStream(new StringReader(globalSettings)); if (localSettings != null && !localSettings.isEmpty()) { // local settings must be complete to have desired effect - ProofSettings.DEFAULT_SETTINGS.loadSettingsFromPropertyString(localSettings); + ProofSettings.DEFAULT_SETTINGS + .loadSettingsFromJSONStream(new StringReader(localSettings)); } LOGGER.info("({}) Active Settings: {}", caseId, diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/TestFile.java b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/TestFile.java index af762f4e45a..62053f58dbd 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/TestFile.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/TestFile.java @@ -144,9 +144,9 @@ public TestResult runKey() throws Exception { // Initialize KeY settings. String gks = settings.getGlobalKeYSettings(); - ProofSettings.DEFAULT_SETTINGS.loadSettingsFromPropertyString(gks); + ProofSettings.DEFAULT_SETTINGS.loadSettingsFromJSONStream(new StringReader(gks)); String lks = settings.getLocalKeYSettings(); - ProofSettings.DEFAULT_SETTINGS.loadSettingsFromPropertyString(lks); + ProofSettings.DEFAULT_SETTINGS.loadSettingsFromJSONStream(new StringReader(lks)); // Name resolution for the available KeY file. File keyFile = getKeYFile(); diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/MasterHandlerTest.java b/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/MasterHandlerTest.java index bdd9db8c2fa..76b3610a778 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/MasterHandlerTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/MasterHandlerTest.java @@ -7,7 +7,6 @@ import java.io.FileNotFoundException; import java.io.IOException; import java.io.OutputStream; -import java.io.StringReader; import java.net.URISyntaxException; import java.net.URL; import java.nio.charset.StandardCharsets; @@ -16,12 +15,12 @@ import java.nio.file.Paths; import java.util.ArrayList; import java.util.List; -import java.util.Properties; import java.util.stream.Collectors; import de.uka.ilkd.key.control.DefaultUserInterfaceControl; import de.uka.ilkd.key.control.KeYEnvironment; import de.uka.ilkd.key.logic.Sequent; +import de.uka.ilkd.key.nparser.ParsingFacade; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.io.ProblemLoaderException; import de.uka.ilkd.key.settings.DefaultSMTSettings; @@ -34,6 +33,7 @@ import org.key_project.util.Streams; +import org.antlr.v4.runtime.CharStreams; import org.jspecify.annotations.Nullable; import org.junit.jupiter.api.Assertions; import org.junit.jupiter.api.Assumptions; @@ -145,8 +145,7 @@ public record TestData(String name, Path path, LineProperties props, String tran String updates = props.get("smt-settings"); if (updates != null) { - Properties map = new Properties(); - map.load(new StringReader(updates)); + var map = ParsingFacade.readConfigurationFile(CharStreams.fromString(updates)); settings.getNewSettings().readSettings(map); } diff --git a/key.removegenerics/src/test/java/de/uka/ilkd/key/util/removegenerics/TestMemberReference.java b/key.removegenerics/src/test/java/de/uka/ilkd/key/util/removegenerics/TestMemberReference.java index dc81cfab103..18b3fc7cfdf 100644 --- a/key.removegenerics/src/test/java/de/uka/ilkd/key/util/removegenerics/TestMemberReference.java +++ b/key.removegenerics/src/test/java/de/uka/ilkd/key/util/removegenerics/TestMemberReference.java @@ -14,7 +14,7 @@ protected void setUp() throws Exception { registerCU("package java.lang; public class String {}"); registerCU("package java.lang; public interface Comparator> { }"); registerCU( - "package java.lang; public class Object { public String toString() {}; protected final Object clone(); }"); + "package java.lang; public class Object { public String toString() {}; protected final Object copy(); }"); registerCU("class G { E[][] array; E field; " + "E m() { return null; } " + "E[][] n() { return null; } } " + "class B { void bb(); }"); } @@ -156,10 +156,10 @@ public void testRawType() throws Exception { public void testStortArray() throws Exception { String before = "class Arrays { public static void sort(T[] a, Comparator c) {" - + "T[] aux = (T[])a.clone(); } }"; + + "T[] aux = (T[])a.copy(); } }"; String after = "class Arrays { public static void sort(java.lang.Object[] a, Comparator c) {" - + "java.lang.Object[] aux = (java.lang.Object[])a.clone(); } }"; + + "java.lang.Object[] aux = (java.lang.Object[])a.copy(); } }"; equalCU(before, after); } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SettingsTreeModel.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SettingsTreeModel.java index 2478d14958a..a8f9d39ddcc 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SettingsTreeModel.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SettingsTreeModel.java @@ -3,47 +3,39 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.gui.actions; -import java.util.Arrays; -import java.util.Map.Entry; -import java.util.Properties; +import java.util.Collection; +import java.util.Map; import javax.swing.*; -import javax.swing.table.DefaultTableModel; import javax.swing.tree.DefaultMutableTreeNode; import javax.swing.tree.DefaultTreeModel; +import javax.swing.tree.MutableTreeNode; import de.uka.ilkd.key.gui.smt.OptionContentNode; -import de.uka.ilkd.key.logic.Choice; -import de.uka.ilkd.key.settings.ChoiceSettings; -import de.uka.ilkd.key.settings.ProofIndependentSettings; -import de.uka.ilkd.key.settings.ProofSettings; -import de.uka.ilkd.key.settings.Settings; +import de.uka.ilkd.key.settings.*; /** - * * A swing model for {@link ShowActiveSettingsAction}. * * @author Mihai Herda, 2018 */ public class SettingsTreeModel extends DefaultTreeModel { - - private static final long serialVersionUID = -3282304543262262159L; - private final ProofSettings proofSettings; - private final ProofIndependentSettings independentSettings; - private OptionContentNode tacletOptionsItem; + private DefaultMutableTreeNode tacletOptionsItem; public SettingsTreeModel(ProofSettings proofSettings, ProofIndependentSettings independentSettings) { super(new DefaultMutableTreeNode("All Settings")); + this.proofSettings = proofSettings; this.independentSettings = independentSettings; + generateTree(); } private void generateTree() { - DefaultMutableTreeNode root = (DefaultMutableTreeNode) this.getRoot(); + DefaultMutableTreeNode root = new DefaultMutableTreeNode("All Settings"); if (proofSettings == null) { OptionContentNode proofSettingsNode = @@ -55,69 +47,36 @@ private void generateTree() { "These are the proof dependent settings."); root.add(proofSettingsNode); - // ChoiceSettings choiceSettings = proofSettings.getChoiceSettings(); - ChoiceSettings choiceSettings = proofSettings.getChoiceSettings(); - tacletOptionsItem = generateTableNode("Taclet Options", choiceSettings); - proofSettingsNode.add(tacletOptionsItem); - - Settings strategySettings = proofSettings.getStrategySettings(); - proofSettingsNode.add(generateTableNode("Strategy", strategySettings)); - - Settings smtSettings = proofSettings.getSMTSettings(); - proofSettingsNode.add(generateTableNode("SMT", smtSettings)); + configurationTable(proofSettingsNode, proofSettings.asConfiguration()); } - OptionContentNode independentSettingsNode = generateOptionContentNode( + var independentSettingsNode = generateOptionContentNode( "Proof-Independent Settings", "These are the proof independent settings."); root.add(independentSettingsNode); + configurationTable(independentSettingsNode, independentSettings.asConfiguration()); - Settings generalSettings = independentSettings.getGeneralSettings(); - independentSettingsNode.add(generateTableNode("General", generalSettings)); - Settings lemmaSettings = independentSettings.getLemmaGeneratorSettings(); - independentSettingsNode.add(generateTableNode("Lemma Generator", lemmaSettings)); - Settings indSMTSettings = independentSettings.getSMTSettings(); - independentSettingsNode.add(generateTableNode("SMT", indSMTSettings)); - // Settings testgenSettings =independentSettings.getTestGenerationSettings(); - // independentSettingsNode.add(generateTableNode("Testcase Generation", testgenSettings)); - Settings viewSettings = independentSettings.getViewSettings(); - independentSettingsNode.add(generateTableNode("View", viewSettings)); - Settings termLabelSettings = independentSettings.getTermLabelSettings(); - // Previously, the termLabelSettings were added to the proofSettingsNode, but judging by the - // previous line, - // it should really be added to the independentSettingsNode - independentSettingsNode.add(generateTableNode("Term Labels", termLabelSettings)); + setRoot(root); } - public JComponent getStartComponent() { return generateScrollPane("Here are all settings."); } - - private Properties getChoicesAsProperties(ChoiceSettings settings) { - Properties prop = new Properties(); - - for (Choice choice : settings.getDefaultChoicesAsSet()) { - prop.put(choice.category(), choice.name()); - } - - return prop; + private MutableTreeNode generateTableNode(String title, Settings settings) { + Configuration c = new Configuration(); + settings.writeSettings(c); + var n = new DefaultMutableTreeNode(title); + configurationTable(n, c); + return n; } - private OptionContentNode generateTableNode(String title, Settings settings) { - - Properties props = new Properties(); - settings.writeSettings(props); - - return new OptionContentNode(title, generateJTable(props)); - - } - - private OptionContentNode generateTableNode(String title, ChoiceSettings settings) { - Properties props = getChoicesAsProperties(settings); - return new OptionContentNode(title, generateJTable(props)); - + private DefaultMutableTreeNode generateTableNode(String title, ChoiceSettings settings) { + Configuration c = new Configuration(); + settings.writeSettings(c); + var node = new DefaultMutableTreeNode(title); + configurationTable(node, c); + return node; } @@ -126,50 +85,53 @@ private JComponent generateScrollPane(String text) { ta.append(text); ta.setEditable(false); ta.setBorder(BorderFactory.createEmptyBorder(10, 10, 10, 10)); - JScrollPane scrollpane = new JScrollPane(ta); - return scrollpane; + return new JScrollPane(ta); } - private JComponent generateJTable(Properties properties) { - String[] columnNames = { "Name", "Value" }; - Object[][] data = new Object[properties.entrySet().size()][2]; - - int i = 0; - for (Entry entry : properties.entrySet()) { - data[i][0] = entry.getKey(); - data[i][1] = entry.getValue(); - i++; + private void configurationTable(DefaultMutableTreeNode parent, Object value) { + if (value == null) { + parent.add(new DefaultMutableTreeNode(" ")); + } else if (value instanceof String || value instanceof Long || value instanceof Integer + || value instanceof Double || value instanceof Float + || value instanceof Short || value instanceof Byte + || value instanceof Boolean || value instanceof Enum) { + parent.add(new DefaultMutableTreeNode(value)); + } else if (value instanceof Collection col) { + configurationTable(parent, col); + } else if (value instanceof Map map) { + } else if (value instanceof Configuration map) { + configurationTable(parent, map); } + } - Arrays.sort(data, (a, b) -> a[0].toString().compareToIgnoreCase(b[0].toString())); - - JTable table = new JTable(); + private void configurationTable(DefaultMutableTreeNode parent, Configuration value) { + var names = value.getKeys().stream().sorted().toList(); - DefaultTableModel tableModel = new DefaultTableModel() { - private static final long serialVersionUID = 1L; + for (String name : names) { + var v = value.get(name); - @Override - public boolean isCellEditable(int row, int column) { - // all cells false - return false; + if (v instanceof Collection || v instanceof Map || v instanceof Configuration) { + var newChild = new DefaultMutableTreeNode(name); + parent.add(newChild); + configurationTable(newChild, v); + } else { + parent.add(new DefaultMutableTreeNode(name + ": " + v)); } - }; - - tableModel.setDataVector(data, columnNames); - table.setModel(tableModel); - table.setRowHeight(table.getRowHeight() + 10); - - JScrollPane scrollpane = new JScrollPane(table); - return scrollpane; + } } + private void configurationTable(DefaultMutableTreeNode parent, Collection values) { + for (var value : values) { + configurationTable(parent, value); + } + } private OptionContentNode generateOptionContentNode(String title, String text) { return new OptionContentNode(title, generateScrollPane(text)); } - public OptionContentNode getTacletOptionsItem() { + public DefaultMutableTreeNode getTacletOptionsItem() { return tacletOptionsItem; } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowActiveSettingsAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowActiveSettingsAction.java index 40d266773b2..19af6bb4968 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowActiveSettingsAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowActiveSettingsAction.java @@ -51,7 +51,7 @@ private ViewSettingsDialog showDialog() { public void showAndFocusTacletOptions() { ViewSettingsDialog dialog = showDialog(); SettingsTreeModel model = (SettingsTreeModel) dialog.optionTree.getModel(); - OptionContentNode item = model.getTacletOptionsItem(); + var item = model.getTacletOptionsItem(); dialog.getOptionTree().setSelectionPath(new TreePath(item.getPath())); } 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 d94916bee3f..667525ae978 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 @@ -8,15 +8,14 @@ import java.io.FileWriter; import java.io.IOException; import java.io.Writer; -import java.util.Objects; import java.util.Optional; -import java.util.Properties; import java.util.stream.Stream; import de.uka.ilkd.key.settings.AbstractPropertiesSettings; import de.uka.ilkd.key.settings.Configuration; import de.uka.ilkd.key.settings.PathConfig; +import org.jspecify.annotations.NullMarked; import org.jspecify.annotations.Nullable; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -29,11 +28,13 @@ * @author Alexander Weigl * @version 1 (10.05.19) */ +@NullMarked public class ColorSettings extends AbstractPropertiesSettings { public static final File SETTINGS_FILE_NEW = new File(PathConfig.getKeyConfigDir(), "colors.json"); private static final Logger LOGGER = LoggerFactory.getLogger(ColorSettings.class); - private static ColorSettings INSTANCE; + + private static @Nullable ColorSettings INSTANCE; public ColorSettings(Configuration load) { super(""); @@ -88,7 +89,10 @@ public static Color invert(Color c) { public void save() { LOGGER.info("Save color settings to: {}", SETTINGS_FILE_NEW.getAbsolutePath()); try (Writer writer = new FileWriter(SETTINGS_FILE_NEW)) { - var config = new Configuration(properties); + var config = new Configuration(); + for (PropertyEntry entry : propertyEntries) { + config.set(entry.getKey(), entry.value()); + } config.save(writer, "KeY's Colors"); writer.flush(); } catch (IOException ex) { @@ -115,87 +119,16 @@ public Stream getProperties() { /** * A property for handling colors. */ - public class ColorProperty implements PropertyEntry { - private final String key; + public class ColorProperty extends DefaultPropertyEntry { private final String description; - private Color currentValue; public ColorProperty(String key, String description, Color defaultValue) { - this.key = key; + super(key, defaultValue, ColorSettings::fromHex, ColorSettings::toHex); this.description = description; - if (!properties.containsKey(key)) { - set(defaultValue); - } - } - - @Override - public String value() { - if (currentValue != null) { - return toHex(currentValue); - } - - String v = properties.get(key).toString(); - - try { - return v; - } catch (NumberFormatException e) { - return toHex(Color.MAGENTA); - } - } - - @Override - public Color fromObject(@Nullable Object o) { - return fromHex(o.toString()); - } - - @Override - public void parseFrom(String v) { - final var old = value(); - if (!Objects.equals(old, v)) { - currentValue = fromHex(v); - properties.put(getKey(), v); - firePropertyChange(getKey(), old, currentValue); - } - } - - @Override - public String getKey() { - return key; - } - - @Override - public void set(Color value) { - if (currentValue != value) { - var old = currentValue; - currentValue = value; - properties.put(getKey(), toHex(value)); - firePropertyChange(getKey(), old, value); - } - } - - @Override - public Color get() { - if (currentValue != null) { - return currentValue; - } - - String v = (String) properties.get(key); - - try { - return currentValue = fromHex(v); - } catch (NumberFormatException e) { - LOGGER.error("Failed to parse color, using magenta", e); - return Color.MAGENTA; - } } public String getDescription() { return description; } } - - @Override - public void readSettings(Properties props) { - props.forEach((k, v) -> this.properties.put(k.toString(), v)); - } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/ExtensionSettings.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/ExtensionSettings.java index e60fccd4ede..9902c8d0729 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/ExtensionSettings.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/ExtensionSettings.java @@ -16,7 +16,7 @@ public class ExtensionSettings extends AbstractPropertiesSettings { * Class names of disabled extensions. */ private final PropertyEntry> forbiddenClasses = - createStringSetProperty(KEY_DISABLED, ""); + createStringSetProperty(KEY_DISABLED, new TreeSet<>()); public ExtensionSettings() { super(NAME); 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 b54d9b00823..2d5d6090bcb 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 @@ -9,15 +9,13 @@ import java.io.FileWriter; import java.io.IOException; import java.io.Writer; -import java.nio.charset.StandardCharsets; -import java.util.Map; -import java.util.Properties; -import java.util.TreeMap; +import java.util.*; import javax.swing.*; import de.uka.ilkd.key.gui.actions.*; import de.uka.ilkd.key.gui.settings.SettingsManager; import de.uka.ilkd.key.macros.*; +import de.uka.ilkd.key.nparser.ParsingFacade; import de.uka.ilkd.key.settings.AbstractPropertiesSettings; import de.uka.ilkd.key.settings.Configuration; import de.uka.ilkd.key.settings.PathConfig; @@ -30,27 +28,16 @@ /** * Class for storing and retrieving {@link KeyStroke}s. - * + *

* If possible, define the keyboard shortcuts in the static block here. By that, it is easier to * detect and prevent possible duplicates. In addition, be careful to avoid combinations that are * used by the docking framework, such as Ctrl+E or Ctrl+M. * * @author Alexander Weigl, Wolfram Pfeifer (overhaul, v2) - * @version 1 (09.05.19) * @version 2 (04.08.23) */ public class KeyStrokeSettings extends AbstractPropertiesSettings { - /** - * filename of the properties file - */ - public static final String SETTINGS_FILENAME = "keystrokes.properties"; - - /** - * 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"); private static final Logger LOGGER = LoggerFactory.getLogger(KeyStrokeSettings.class); @@ -59,12 +46,14 @@ public class KeyStrokeSettings extends AbstractPropertiesSettings { /** * singleton instance */ - private static KeyStrokeSettings INSTANCE = null; + public static class KeyStrokeSettingsHolder { + private static KeyStrokeSettings INSTANCE = loadFromConfig(); + } /** * default {@link KeyStroke}s */ - private static Map DEFAULT_KEYSTROKES = new TreeMap<>(); + private static final Map DEFAULT_KEYSTROKES = new TreeMap<>(); // define the default mappings static { @@ -129,14 +118,18 @@ public class KeyStrokeSettings extends AbstractPropertiesSettings { // defineDefault(HelpFacade.ACTION_OPEN_HELP.getClass(), KeyEvent.VK_F1, 0); } - private KeyStrokeSettings(Properties init) { + private final Map properties = new LinkedHashMap<>(); + + private KeyStrokeSettings(Map init) { super(""); // no category, separate file - this.properties.putAll(DEFAULT_KEYSTROKES); - init.forEach((key, value) -> { - if (value != null && !value.toString().isEmpty()) { - this.properties.put(key.toString(), value); + properties.putAll(DEFAULT_KEYSTROKES); + for (Map.Entry entry : init.entrySet()) { + String key = entry.getKey(); + String value = entry.getValue(); + if (value != null && !value.isEmpty()) { + this.properties.put(key, value); } - }); + } save(); Runtime.getRuntime().addShutdownHook(new Thread(this::save)); } @@ -163,28 +156,19 @@ private static void defineDefault(Class clazz, int keyCode, int modifiers } private static KeyStrokeSettings loadFromConfig() { - return new KeyStrokeSettings(SettingsManager.loadProperties(SETTINGS_FILE)); - } - - public static KeyStrokeSettings getInstance() { - - if (INSTANCE == null) { + try { if (SETTINGS_FILE.exists()) { - try { - LOGGER.info("Use new configuration format at {}", SETTINGS_FILE_NEW); - return INSTANCE = new KeyStrokeSettings(Configuration.load(SETTINGS_FILE_NEW)); - } catch (IOException e) { - LOGGER.error("Could not read {}", SETTINGS_FILE_NEW, e); - } + Configuration config = ParsingFacade.readConfigurationFile(SETTINGS_FILE); + return new KeyStrokeSettings(config); } - return INSTANCE = KeyStrokeSettings.loadFromConfig(); + } catch (IOException e) { + throw new RuntimeException(e); } - return INSTANCE; + return new KeyStrokeSettings(new HashMap<>()); } - @Override - public void readSettings(Properties props) { - props.forEach((k, v) -> this.properties.put(k.toString(), v)); + public static KeyStrokeSettings getInstance() { + return KeyStrokeSettingsHolder.INSTANCE; } void setKeyStroke(String key, KeyStroke stroke, boolean override) { @@ -197,7 +181,7 @@ void setKeyStroke(String key, KeyStroke stroke, boolean override) { KeyStroke getKeyStroke(String key, KeyStroke defaultValue) { try { - KeyStroke ks = KeyStroke.getKeyStroke(properties.get(key).toString()); + KeyStroke ks = KeyStroke.getKeyStroke(properties.get(key)); if (ks != null) { return ks; } @@ -208,21 +192,9 @@ 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()); - } - 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)) { - var config = new Configuration(properties); + try (Writer writer = new FileWriter(SETTINGS_FILE)) { + var config = new Configuration(); + properties.forEach(config::set); config.save(writer, "KeY's KeyStrokes"); writer.flush(); } catch (IOException ex) { 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 fe0a410f61c..64ac4288976 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 @@ -8,8 +8,6 @@ import java.io.Serial; import java.util.ArrayList; import java.util.List; -import java.util.Properties; -import java.util.stream.Collectors; import javax.swing.*; import javax.swing.table.AbstractTableModel; import javax.swing.table.TableRowSorter; @@ -17,6 +15,7 @@ import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.settings.SettingsProvider; import de.uka.ilkd.key.gui.settings.SimpleSettingsPanel; +import de.uka.ilkd.key.settings.Configuration; /** * UI for configuring the {@link KeyStroke}s inside KeY. @@ -46,18 +45,19 @@ public String getDescription() { @Override public JPanel getPanel(MainWindow window) { KeyStrokeSettings settings = KeyStrokeManager.getSettings(); - Properties p = new Properties(); - settings.writeSettings(p); - List actionNames = - p.keySet().stream().sorted().map(Object::toString).collect(Collectors.toList()); + var config = new Configuration(); + settings.writeSettings(config); + + List actionNames = config.getKeys().stream().sorted().toList(); // for the view, we hide "pressed" to increase readability - List shortcuts = actionNames.stream().map(p::getProperty) - .map(s -> s.replace("pressed ", "")).collect(Collectors.toList()); + List shortcuts = actionNames.stream() + .map(config::getString) + .map(s -> s.replace("pressed ", "")) + .toList(); - List actions = - actionNames.stream().map(KeyStrokeManager::findAction).collect(Collectors.toList()); + List actions = actionNames.stream().map(KeyStrokeManager::findAction).toList(); modelShortcuts = new ShortcutsTableModel(actionNames, shortcuts, actions); tblShortcuts.setModel(modelShortcuts); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsManager.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsManager.java index 91bb112e251..006c666b014 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsManager.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsManager.java @@ -4,14 +4,9 @@ package de.uka.ilkd.key.gui.settings; import java.awt.event.ActionEvent; -import java.io.File; -import java.io.FileReader; -import java.io.IOException; -import java.nio.charset.StandardCharsets; import java.util.Comparator; import java.util.LinkedList; import java.util.List; -import java.util.Properties; import javax.swing.*; import de.uka.ilkd.key.gui.MainWindow; @@ -100,18 +95,6 @@ public static ChoiceSettings getChoiceSettings(MainWindow window) { */ } - public static Properties loadProperties(File settingsFile) { - Properties props = new Properties(); - if (settingsFile.exists()) { - try (FileReader reader = new FileReader(settingsFile, StandardCharsets.UTF_8)) { - props.load(reader); - } catch (IOException e) { - LOGGER.warn("Failed to load settings", e); - } - } - return props; - } - public void showSettingsDialog(MainWindow mainWindow) { SettingsDialog dialog = createDialog(mainWindow); dialog.setVisible(true); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/StandardUISettings.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/StandardUISettings.java index 9075e9f186d..e7d84b9e77c 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/StandardUISettings.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/StandardUISettings.java @@ -6,6 +6,7 @@ import java.util.ArrayList; import java.util.Arrays; import java.util.List; +import java.util.stream.Collectors; import javax.swing.*; import de.uka.ilkd.key.gui.MainWindow; @@ -147,8 +148,8 @@ public JPanel getPanel(MainWindow window) { ProofIndependentSettings.DEFAULT_INSTANCE.getGeneralSettings(); - txtClutterRules.setText(vs.clutterRules().value().replace(',', '\n')); - txtClutterRuleSets.setText(vs.clutterRuleSets().value().replace(',', '\n')); + txtClutterRules.setText(String.join("\n", vs.clutterRules().get())); + txtClutterRuleSets.setText(String.join("\n", vs.clutterRuleSets().get())); for (int i = 0; i < LAF_CLASSES.size(); i++) { if (LAF_CLASSES.get(i).equals(vs.getLookAndFeel())) { @@ -190,8 +191,10 @@ public void applySettings(MainWindow window) throws InvalidSettingsInputExceptio vs.setUIFontSizeFactor((Double) spFontSizeGlobal.getValue()); vs.setMaxTooltipLines((Integer) txtMaxTooltipLines.getValue()); - vs.clutterRules().parseFrom(txtClutterRules.getText().replace('\n', ',')); - vs.clutterRuleSets().parseFrom(txtClutterRuleSets.getText().replace('\n', ',')); + vs.clutterRules().set( + Arrays.stream(txtClutterRules.getText().split("\n")).collect(Collectors.toSet())); + vs.clutterRuleSets().set( + Arrays.stream(txtClutterRuleSets.getText().split("\n")).collect(Collectors.toSet())); vs.setShowLoadExamplesDialog(chkShowLoadExamplesDialog.isSelected()); vs.setShowWholeTaclet(chkShowWholeTacletCB.isSelected()); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/OptionContentNode.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/OptionContentNode.java index 0b1bdbee515..64f82e90666 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/OptionContentNode.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/OptionContentNode.java @@ -9,13 +9,11 @@ /** * @author Mihai Herda, 2018 */ - public class OptionContentNode extends DefaultMutableTreeNode { private static final long serialVersionUID = 1L; private final JComponent component; public OptionContentNode(String title, JComponent component) { - super(); this.component = component; this.setUserObject(title); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/SMTSettingsProvider.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/SMTSettingsProvider.java index 1cb00ad3d75..f3568a8fc6d 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/SMTSettingsProvider.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/SMTSettingsProvider.java @@ -170,7 +170,7 @@ public String getDescription() { @Override public JPanel getPanel(MainWindow window) { ProofIndependentSMTSettings pi = SettingsManager.getSmtPiSettings(); - setSmtSettings(pi.clone()); + setSmtSettings(pi.copy()); return this; } @@ -178,7 +178,7 @@ public JPanel getPanel(MainWindow window) { public void applySettings(MainWindow window) { ProofIndependentSMTSettings pi = SettingsManager.getSmtPiSettings(); pi.copy(settings); - setSmtSettings(pi.clone()); + setSmtSettings(pi.copy()); } private JSpinner createLocSetBoundField() { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/SolverOptions.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/SolverOptions.java index fdeff38fe19..77dbc32f573 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/SolverOptions.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/SolverOptions.java @@ -177,7 +177,7 @@ public String getDescription() { @Override public JPanel getPanel(MainWindow window) { - setSmtSettings(SettingsManager.getSmtPiSettings().clone()); + setSmtSettings(SettingsManager.getSmtPiSettings().copy()); return this; } @@ -216,7 +216,7 @@ public void applySettings(MainWindow window) { // SettingsManager.getSmtPiSettings().setParameters(solverType, params); window.updateSMTSelectMenu(); - setSmtSettings(SettingsManager.getSmtPiSettings().clone()); // refresh gui + setSmtSettings(SettingsManager.getSmtPiSettings().copy()); // refresh gui } else { throw new IllegalStateException("Could not find solver data for type: " + solverType); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/TacletTranslationOptions.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/TacletTranslationOptions.java index ff0dde1701b..81a6e46ce93 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/TacletTranslationOptions.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/TacletTranslationOptions.java @@ -64,8 +64,8 @@ public String getDescription() { @Override public JPanel getPanel(MainWindow window) { - ProofDependentSMTSettings pdSettings = SettingsManager.getSmtPdSettings(window).clone(); - ProofIndependentSMTSettings piSettings = SettingsManager.getSmtPiSettings().clone(); + ProofDependentSMTSettings pdSettings = SettingsManager.getSmtPdSettings(window).copy(); + ProofIndependentSMTSettings piSettings = SettingsManager.getSmtPiSettings().copy(); maxNumberOfGenerics.setValue(pdSettings.getMaxGenericSorts()); fileChooserPanel.setText(piSettings.getPathForTacletTranslation()); // fileChooserPanel.setEnabled(piSettings.storeTacletTranslationToFile); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/TranslationOptions.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/TranslationOptions.java index 35cf06d5ebe..0de2cada979 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/TranslationOptions.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/TranslationOptions.java @@ -170,7 +170,7 @@ public String getDescription() { @Override public JPanel getPanel(MainWindow window) { - setSmtSettings(SettingsManager.getSmtPdSettings(window).clone()); + setSmtSettings(SettingsManager.getSmtPdSettings(window).copy()); return this; }