Removal of the write and read settings using Properties

Author: wadoon

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

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

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

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

key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java

@@ -74,9 +74,8 @@ public static class File extends KeyAst<KeYParser.FileContext> {
             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);

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<String> userLog;
+    public List<String> 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<String> keyVersionLog;
+    public List<String> keyVersionLog = new ArrayList<>();
 
     private long autoModeTime = 0;
 
@@ -167,8 +168,7 @@ 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

key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediatePresentationProofFileParser.java

@@ -3,22 +3,22 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.proof.io;
 
-import java.util.ArrayDeque;
-import java.util.ArrayList;
-import java.util.LinkedList;
-import java.util.List;
-
 import de.uka.ilkd.key.axiom_abstraction.predicateabstraction.AbstractPredicateAbstractionLattice;
 import de.uka.ilkd.key.logic.PosInTerm;
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.proof.io.intermediate.*;
 import de.uka.ilkd.key.settings.ProofSettings;
-
 import org.key_project.logic.Name;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
 import org.key_project.util.collection.Pair;
 
+import java.io.IOException;
+import java.io.StringReader;
+import java.util.ArrayDeque;
+import java.util.LinkedList;
+import java.util.List;
+
 /**
  * Parses a KeY proof file into an intermediate representation. The parsed intermediate result can
  * be processed by {@link IntermediateProofReplayer}. This approach is more flexible than direct
@@ -143,26 +143,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<>();
-            }
-            proof.userLog.add(str);
-        }
-        case KeY_VERSION -> { // Version log
-            if (proof.keyVersionLog == null) {
-                proof.keyVersionLog = new ArrayList<>();
-            }
-            proof.keyVersionLog.add(str);
-        }
+        case KeY_USER -> // UserLog
+                proof.userLog.add(str);
+        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 +319,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.
+        }
     }
 
     /**