Overhaul of the Configuration (#3031)

The KeY settings are in a *hysterical* and *historic* shape. This PR tries to homogenize the settings to Java POJOs using the JavaBeans standard and mechanism. The measurement include: * Introduction of Getter/Setter * Removal of `SettingsListener` in favour of `PropertyChangeListener` (You can listen on individual configuration changes.) **Most of the changes** results from dependencies to the `SettingsListener`, or the change of field-access to getter and setter. A next PR step will change the settings language in KeY files to a custom type-safe backward compatible language.
KeYProject · Apr 6, 2023 · dd62d03 · dd62d03
2 parents ae71749 + 6505700
commit dd62d03
Show file tree

Hide file tree

Showing 76 changed files with 916 additions and 1,112 deletions.
diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json
diff --git a/key.core.example/src/main/java/org/key_project/Main.java b/key.core.example/src/main/java/org/key_project/Main.java
@@ -1,10 +1,7 @@
 package org.key_project;
 
 import java.io.File;
-import java.util.HashMap;
-import java.util.LinkedList;
-import java.util.List;
-import java.util.Set;
+import java.util.*;
 
 import de.uka.ilkd.key.control.KeYEnvironment;
 import de.uka.ilkd.key.java.abstraction.KeYJavaType;
@@ -69,8 +66,8 @@ private static KeYEnvironment<?> setupEnvironment(File location) throws ProblemL
         }
         // Set Taclet options
         ChoiceSettings choiceSettings = ProofSettings.DEFAULT_SETTINGS.getChoiceSettings();
-        HashMap<String, String> oldSettings = choiceSettings.getDefaultChoices();
-        HashMap<String, String> newSettings = new HashMap<>(oldSettings);
+        Map<String, String> oldSettings = choiceSettings.getDefaultChoices();
+        Map<String, String> newSettings = new HashMap<>(oldSettings);
         newSettings.putAll(MiscTools.getDefaultTacletOptions());
         choiceSettings.setDefaultChoices(newSettings);
         // Load source code

diff --git a/...c/test/java/de/uka/ilkd/key/proof_references/testcase/AbstractProofReferenceTestCase.java b/...c/test/java/de/uka/ilkd/key/proof_references/testcase/AbstractProofReferenceTestCase.java
@@ -1,9 +1,9 @@
 package de.uka.ilkd.key.proof_references.testcase;
 
 import java.io.File;
-import java.util.HashMap;
 import java.util.Iterator;
 import java.util.LinkedHashSet;
+import java.util.Map;
 import java.util.function.Predicate;
 
 import de.uka.ilkd.key.control.KeYEnvironment;
@@ -63,7 +63,8 @@ protected void doReferenceFunctionTest(File baseDir, String javaPathInBaseDir,
             IProofReferencesAnalyst analyst, ExpectedProofReferences... expectedReferences)
             throws Exception {
         doReferenceFunctionTest(baseDir, javaPathInBaseDir, containerTypeName, targetName,
-            useContracts, analyst, null, expectedReferences);
+            useContracts, analyst,
+            null, expectedReferences);
     }
 
     /**
@@ -306,7 +307,7 @@ protected void doProofFunctionTest(File baseDir, String javaPathInBaseDir,
         assertNotNull(tester);
         KeYEnvironment<?> environment = null;
         Proof proof = null;
-        HashMap<String, String> originalTacletOptions = null;
+        Map<String, String> originalTacletOptions = null;
         boolean usePrettyPrinting = ProofIndependentSettings.isUsePrettyPrinting();
         try {
             // Disable pretty printing to make tests more robust against different term
@@ -379,7 +380,7 @@ protected void doProofMethodTest(File baseDir, String javaPathInBaseDir,
         assertNotNull(tester);
         KeYEnvironment<?> environment = null;
         Proof proof = null;
-        HashMap<String, String> originalTacletOptions = null;
+        Map<String, String> originalTacletOptions = null;
         boolean usePrettyPrinting = ProofIndependentSettings.isUsePrettyPrinting();
         try {
             // Disable pretty printing to make tests more robust against different term

diff --git a/key.core.symbolic_execution.example/src/main/java/org/key_project/example/Main.java b/key.core.symbolic_execution.example/src/main/java/org/key_project/example/Main.java
@@ -3,6 +3,7 @@
 import java.io.File;
 import java.util.HashMap;
 import java.util.List;
+import java.util.Map;
 
 import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
 import de.uka.ilkd.key.control.KeYEnvironment;
@@ -61,8 +62,8 @@ public static void main(String[] args) {
             }
             // Set Taclet options
             ChoiceSettings choiceSettings = ProofSettings.DEFAULT_SETTINGS.getChoiceSettings();
-            HashMap<String, String> oldSettings = choiceSettings.getDefaultChoices();
-            HashMap<String, String> newSettings = new HashMap<>(oldSettings);
+            Map<String, String> oldSettings = choiceSettings.getDefaultChoices();
+            Map<String, String> newSettings = new HashMap<>(oldSettings);
             newSettings.putAll(MiscTools.getDefaultTacletOptions());
             newSettings.put("methodExpansion", "methodExpansion:noRestriction");
             choiceSettings.setDefaultChoices(newSettings);

diff --git a/...xecution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java b/...xecution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java
@@ -2782,9 +2782,9 @@ public static String getChoiceSetting(String key) {
      * @param value The new choice value to set.
      */
     public static void setChoiceSetting(String key, String value) {
-        HashMap<String, String> settings =
+        var settings =
             ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().getDefaultChoices();
-        HashMap<String, String> clone = new LinkedHashMap<>(settings);
+        var clone = new LinkedHashMap<>(settings);
         clone.put(key, value);
         ProofSettings.DEFAULT_SETTINGS.getChoiceSettings().setDefaultChoices(clone);
     }

diff --git a/...t/java/de/uka/ilkd/key/symbolic_execution/testcase/AbstractSymbolicExecutionTestCase.java b/...t/java/de/uka/ilkd/key/symbolic_execution/testcase/AbstractSymbolicExecutionTestCase.java
@@ -2012,7 +2012,7 @@ protected SymbolicExecutionEnvironment<DefaultUserInterfaceControl> doSETTest(Fi
             boolean variablesAreOnlyComputedFromUpdates, boolean simplifyConditions)
             throws ProofInputException, IOException, ParserConfigurationException, SAXException,
             ProblemLoaderException {
-        HashMap<String, String> originalTacletOptions = null;
+        Map<String, String> originalTacletOptions = null;
         boolean originalOneStepSimplification = isOneStepSimplificationEnabled(null);
         try {
             // Make sure that parameter are valid.
@@ -2105,7 +2105,7 @@ protected SymbolicExecutionEnvironment<DefaultUserInterfaceControl> doSETTest(Fi
             boolean variablesAreOnlyComputedFromUpdates, boolean truthValueEvaluationEnabled,
             boolean simplifyConditions) throws ProofInputException, IOException,
             ParserConfigurationException, SAXException, ProblemLoaderException {
-        HashMap<String, String> originalTacletOptions = null;
+        Map<String, String> originalTacletOptions = null;
         try {
             // Make sure that parameter are valid.
             assertNotNull(javaPathInBaseDir);
@@ -2195,13 +2195,16 @@ private void internalDoSETTest(File oracleFile,
      * @throws ProblemLoaderException Occurred Exception.
      * @throws ProofInputException Occurred Exception.
      */
-    public static HashMap<String, String> setDefaultTacletOptions(File baseDir,
+    public static Map<String, String> setDefaultTacletOptions(File baseDir,
             String javaPathInBaseDir, String baseContractName)
             throws ProblemLoaderException, ProofInputException {
         if (!SymbolicExecutionUtil.isChoiceSettingInitialised()) {
             SymbolicExecutionEnvironment<DefaultUserInterfaceControl> env =
                 createSymbolicExecutionEnvironment(testCaseDirectory, javaPathInBaseDir,
-                    baseContractName, false, false, false, false, false, false, false, false, false,
+                    baseContractName,
+                    false, false, false,
+                    false, false, false,
+                    false, false, false,
                     false, false);
             env.dispose();
         }
@@ -2219,14 +2222,18 @@ public static HashMap<String, String> setDefaultTacletOptions(File baseDir,
      * @throws ProblemLoaderException Occurred Exception.
      * @throws ProofInputException Occurred Exception.
      */
-    public static HashMap<String, String> setDefaultTacletOptions(File baseDir,
-            String javaPathInBaseDir, String containerTypeName, String methodFullName)
+    public static Map<String, String> setDefaultTacletOptions(File baseDir,
+            String javaPathInBaseDir,
+            String containerTypeName,
+            String methodFullName)
             throws ProblemLoaderException, ProofInputException {
         if (!SymbolicExecutionUtil.isChoiceSettingInitialised()) {
             SymbolicExecutionEnvironment<DefaultUserInterfaceControl> env =
                 createSymbolicExecutionEnvironment(baseDir, javaPathInBaseDir, containerTypeName,
-                    methodFullName, null, false, false, false, false, false, false, false, false,
-                    false, false);
+                    methodFullName,
+                    null, false, false, false,
+                    false, false, false, false,
+                    false, false, false);
             env.dispose();
         }
         return setDefaultTacletOptions();
@@ -2242,7 +2249,7 @@ public static HashMap<String, String> setDefaultTacletOptions(File baseDir,
      * @throws ProblemLoaderException Occurred Exception.
      * @throws ProofInputException Occurred Exception.
      */
-    public static HashMap<String, String> setDefaultTacletOptionsForTarget(File javaFile,
+    public static Map<String, String> setDefaultTacletOptionsForTarget(File javaFile,
             String containerTypeName, final String targetName)
             throws ProblemLoaderException, ProofInputException {
         return HelperClassForTests.setDefaultTacletOptionsForTarget(javaFile, containerTypeName,
@@ -2254,8 +2261,8 @@ public static HashMap<String, String> setDefaultTacletOptionsForTarget(File java
      *
      * @return The original settings which are overwritten.
      */
-    public static HashMap<String, String> setDefaultTacletOptions() {
-        HashMap<String, String> original = HelperClassForTests.setDefaultTacletOptions();
+    public static Map<String, String> setDefaultTacletOptions() {
+        Map<String, String> original = HelperClassForTests.setDefaultTacletOptions();
         ChoiceSettings choiceSettings = ProofSettings.DEFAULT_SETTINGS.getChoiceSettings();
         ImmutableSet<Choice> cs = DefaultImmutableSet.nil();
         cs = cs.add(new Choice("noRestriction", "methodExpansion"));
@@ -2268,7 +2275,7 @@ public static HashMap<String, String> setDefaultTacletOptions() {
      *
      * @param options The taclet options to restore.
      */
-    public static void restoreTacletOptions(HashMap<String, String> options) {
+    public static void restoreTacletOptions(Map<String, String> options) {
         HelperClassForTests.restoreTacletOptions(options);
     }
 

diff --git a/...st/java/de/uka/ilkd/key/symbolic_execution/testcase/TestSymbolicExecutionTreeBuilder.java b/...st/java/de/uka/ilkd/key/symbolic_execution/testcase/TestSymbolicExecutionTreeBuilder.java
@@ -1,8 +1,8 @@
 package de.uka.ilkd.key.symbolic_execution.testcase;
 
 import java.io.File;
-import java.util.HashMap;
 import java.util.Iterator;
+import java.util.Map;
 
 import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
 import de.uka.ilkd.key.control.KeYEnvironment;
@@ -20,6 +20,7 @@
 
 import static org.junit.jupiter.api.Assertions.*;
 
+
 /**
  * Tests for {@link SymbolicExecutionTreeBuilder},
  * {@link ExecutedSymbolicExecutionTreeNodesStopCondition} and {@link SymbolicExecutionGoalChooser}.
@@ -536,7 +537,7 @@ public void testComplexPruning() throws Exception {
     @Test
     public void testSymbolicExecutionCompletionsTest() throws Exception {
         SymbolicExecutionEnvironment<DefaultUserInterfaceControl> env = null;
-        HashMap<String, String> originalTacletOptions = null;
+        Map<String, String> originalTacletOptions = null;
         boolean originalOneStepSimplification = isOneStepSimplificationEnabled(null);
         try {
             String javaPathInBaseDir =

diff --git a/...rc/test/java/de/uka/ilkd/key/symbolic_execution/testcase/TestSymbolicLayoutExtractor.java b/...rc/test/java/de/uka/ilkd/key/symbolic_execution/testcase/TestSymbolicLayoutExtractor.java
@@ -3,9 +3,9 @@
 import java.io.File;
 import java.io.IOException;
 import java.util.ArrayList;
-import java.util.HashMap;
 import java.util.Iterator;
 import java.util.List;
+import java.util.Map;
 
 import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
 import de.uka.ilkd.key.symbolic_execution.SymbolicLayoutExtractor;
@@ -24,6 +24,7 @@
 
 import static org.junit.jupiter.api.Assertions.*;
 
+
 /**
  * Tests {@link SymbolicLayoutExtractor}.
  *
@@ -529,7 +530,7 @@ protected void doTest(String javaPathInkeyRepDirectory, String containerTypeName
             String precondition, int numberOfReturnNodeInMostLeftBranch,
             int expectedNumberOfLayouts, boolean useOperationContracts,
             boolean onReturnStatementNode) throws Exception {
-        HashMap<String, String> originalTacletOptions = null;
+        Map<String, String> originalTacletOptions = null;
         SymbolicExecutionEnvironment<DefaultUserInterfaceControl> env = null;
         boolean originalOneStepSimplification = isOneStepSimplificationEnabled(null);
         try {

diff --git a/...ava/de/uka/ilkd/key/symbolic_execution/testcase/po/TestFunctionalOperationContractPO.java b/...ava/de/uka/ilkd/key/symbolic_execution/testcase/po/TestFunctionalOperationContractPO.java
@@ -1,7 +1,7 @@
 package de.uka.ilkd.key.symbolic_execution.testcase.po;
 
 import java.io.IOException;
-import java.util.HashMap;
+import java.util.Map;
 import javax.xml.parsers.ParserConfigurationException;
 
 import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
@@ -40,7 +40,7 @@ public void testDoubleValue() throws Exception {
     protected void doTest(String javaPathInkeyRepDirectory, String baseContractName,
             String oraclePathInBaseDirFile, String expectedTryContent) throws ProofInputException,
             IOException, ParserConfigurationException, SAXException, ProblemLoaderException {
-        HashMap<String, String> originalTacletOptions = null;
+        Map<String, String> originalTacletOptions = null;
         SymbolicExecutionEnvironment<DefaultUserInterfaceControl> env = null;
         try {
             // Make sure that the correct taclet options are defined.

diff --git a/...ion/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/po/TestProgramMethodPO.java b/...ion/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/po/TestProgramMethodPO.java
@@ -1,7 +1,7 @@
 package de.uka.ilkd.key.symbolic_execution.testcase.po;
 
 import java.io.IOException;
-import java.util.HashMap;
+import java.util.Map;
 import javax.xml.parsers.ParserConfigurationException;
 
 import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
@@ -108,7 +108,7 @@ protected void doTest(String javaPathInkeyRepDirectory, String containerTypeName
             String methodFullName, String oraclePathInBaseDirFile, String precondition,
             String expectedTryContent) throws ProofInputException, IOException,
             ParserConfigurationException, SAXException, ProblemLoaderException {
-        HashMap<String, String> originalTacletOptions = null;
+        Map<String, String> originalTacletOptions = null;
         SymbolicExecutionEnvironment<DefaultUserInterfaceControl> env = null;
         boolean originalOneStepSimplification = isOneStepSimplificationEnabled(null);
         try {

diff --git a/...lic_execution/testcase/strategy/TestExceptionBreakpointStopConditionCaughtOrUncaught.java b/...lic_execution/testcase/strategy/TestExceptionBreakpointStopConditionCaughtOrUncaught.java
@@ -1,7 +1,7 @@
 package de.uka.ilkd.key.symbolic_execution.testcase.strategy;
 
 import java.io.IOException;
-import java.util.HashMap;
+import java.util.Map;
 import javax.xml.parsers.ParserConfigurationException;
 
 import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
@@ -29,7 +29,7 @@ public class TestExceptionBreakpointStopConditionCaughtOrUncaught
     public void testBreakpointStopCondition() throws ProofInputException, IOException,
             ParserConfigurationException, SAXException, ProblemLoaderException {
         SymbolicExecutionEnvironment<DefaultUserInterfaceControl> env = null;
-        HashMap<String, String> originalTacletOptions = null;
+        Map<String, String> originalTacletOptions = null;
         boolean originalOneStepSimplification = isOneStepSimplificationEnabled(null);
         try {
             // Define test settings

diff --git a/...ymbolic_execution/testcase/strategy/TestExceptionBreakpointStopConditionWithHitCount.java b/...ymbolic_execution/testcase/strategy/TestExceptionBreakpointStopConditionWithHitCount.java
@@ -1,7 +1,7 @@
 package de.uka.ilkd.key.symbolic_execution.testcase.strategy;
 
 import java.io.IOException;
-import java.util.HashMap;
+import java.util.Map;
 import javax.xml.parsers.ParserConfigurationException;
 
 import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
@@ -23,7 +23,7 @@ public class TestExceptionBreakpointStopConditionWithHitCount
     @Test
     public void testBreakpointStopCondition() throws ProofInputException, IOException,
             ParserConfigurationException, SAXException, ProblemLoaderException {
-        HashMap<String, String> originalTacletOptions = null;
+        Map<String, String> originalTacletOptions = null;
         boolean originalOneStepSimplification = isOneStepSimplificationEnabled(null);
         SymbolicExecutionEnvironment<DefaultUserInterfaceControl> env = null;
         try {

diff --git a/...bolic_execution/testcase/strategy/TestExceptionBreakpointStopConditionWithSubclasses.java b/...bolic_execution/testcase/strategy/TestExceptionBreakpointStopConditionWithSubclasses.java
@@ -1,7 +1,7 @@
 package de.uka.ilkd.key.symbolic_execution.testcase.strategy;
 
 import java.io.IOException;
-import java.util.HashMap;
+import java.util.Map;
 import javax.xml.parsers.ParserConfigurationException;
 
 import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
@@ -23,7 +23,7 @@ public class TestExceptionBreakpointStopConditionWithSubclasses
     @Test // weigl not prev. activated
     public void testBreakpointStopCondition() throws ProofInputException, IOException,
             ParserConfigurationException, SAXException, ProblemLoaderException {
-        HashMap<String, String> originalTacletOptions = null;
+        Map<String, String> originalTacletOptions = null;
         boolean originalOneStepSimplification = isOneStepSimplificationEnabled(null);
         SymbolicExecutionEnvironment<DefaultUserInterfaceControl> env = null;
         try {

diff --git a/...key/symbolic_execution/testcase/strategy/TestJavaWatchpointStopConditionWithHitCount.java b/...key/symbolic_execution/testcase/strategy/TestJavaWatchpointStopConditionWithHitCount.java
@@ -1,7 +1,7 @@
 package de.uka.ilkd.key.symbolic_execution.testcase.strategy;
 
 import java.io.IOException;
-import java.util.HashMap;
+import java.util.Map;
 import javax.xml.parsers.ParserConfigurationException;
 
 import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
@@ -22,7 +22,7 @@ public class TestJavaWatchpointStopConditionWithHitCount extends AbstractSymboli
     public void testBreakpointStopCondition() throws ProofInputException, IOException,
             ParserConfigurationException, SAXException, ProblemLoaderException {
         SymbolicExecutionEnvironment<DefaultUserInterfaceControl> env = null;
-        HashMap<String, String> originalTacletOptions = null;
+        Map<String, String> originalTacletOptions = null;
         boolean originalOneStepSimplification = isOneStepSimplificationEnabled(null);
         try {
             // Define test settings

diff --git a/...y/symbolic_execution/testcase/strategy/TestKeYWatchpointGlobalVariablesOnSatisfiable.java b/...y/symbolic_execution/testcase/strategy/TestKeYWatchpointGlobalVariablesOnSatisfiable.java
@@ -1,7 +1,7 @@
 package de.uka.ilkd.key.symbolic_execution.testcase.strategy;
 
 import java.io.IOException;
-import java.util.HashMap;
+import java.util.Map;
 import javax.xml.parsers.ParserConfigurationException;
 
 import de.uka.ilkd.key.control.DefaultUserInterfaceControl;
@@ -24,7 +24,7 @@ public class TestKeYWatchpointGlobalVariablesOnSatisfiable
     public void testBreakpointStopCondition() throws ProofInputException, IOException,
             ParserConfigurationException, SAXException, ProblemLoaderException {
         SymbolicExecutionEnvironment<DefaultUserInterfaceControl> env = null;
-        HashMap<String, String> originalTacletOptions = null;
+        Map<String, String> originalTacletOptions = null;
         boolean originalOneStepSimplification = isOneStepSimplificationEnabled(null);
         try {
             // Define test settings